Commit 2023-04-06 15:04 26479b00

View on Github →

feat: port Analysis.SpecificLimits.Basic (#3242)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecificLimits/Basic.lean

added theorem ENNReal.exists_pos_sum_of_countable'

added theorem ENNReal.exists_pos_sum_of_countable

added theorem ENNReal.exists_pos_tsum_mul_lt_of_countable

added theorem ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1

added theorem ENNReal.tsum_geometric

added theorem NNReal.exists_pos_sum_of_countable

added theorem NNReal.hasSum_geometric

added theorem NNReal.summable_geometric

added theorem NNReal.tendsto_const_div_atTop_nhds_0_nat

added theorem NNReal.tendsto_inverse_atTop_nhds_0_nat

added theorem NNReal.tendsto_pow_atTop_nhds_0_of_lt_1

added theorem Nat.tendsto_pow_atTop_atTop_of_one_lt

added theorem Set.Countable.exists_pos_forall_sum_le

added theorem Set.Countable.exists_pos_hasSum_le

added theorem aux_hasSum_of_le_geometric

added theorem cauchySeq_of_edist_le_geometric

added theorem cauchySeq_of_edist_le_geometric_two

added theorem cauchySeq_of_le_geometric

added theorem cauchySeq_of_le_geometric_two

added theorem dist_le_of_le_geometric_of_tendsto

added theorem dist_le_of_le_geometric_of_tendsto₀

added theorem dist_le_of_le_geometric_two_of_tendsto

added theorem dist_le_of_le_geometric_two_of_tendsto₀

added theorem edist_le_of_edist_le_geometric_of_tendsto

added theorem edist_le_of_edist_le_geometric_of_tendsto₀

added theorem edist_le_of_edist_le_geometric_two_of_tendsto

added theorem edist_le_of_edist_le_geometric_two_of_tendsto₀

added theorem factorial_tendsto_atTop

added theorem geom_le

added theorem geom_lt

added theorem hasSum_geometric_of_lt_1

added theorem hasSum_geometric_two'

added theorem hasSum_geometric_two

added theorem le_geom

added theorem lt_geom

added def posSumOfEncodable

added theorem sum_geometric_two_le

added theorem summable_geometric_of_lt_1

added theorem summable_geometric_two'

added theorem summable_geometric_two

added theorem summable_geometric_two_encode

added theorem summable_one_div_pow_of_le

added theorem tendsto_add_one_pow_atTop_atTop_of_pos

added theorem tendsto_atTop_of_geom_le

added theorem tendsto_coe_nat_div_add_atTop

added theorem tendsto_const_div_atTop_nhds_0_nat

added theorem tendsto_factorial_div_pow_self_atTop

added theorem tendsto_inverse_atTop_nhds_0_nat

added theorem tendsto_nat_ceil_div_atTop

added theorem tendsto_nat_ceil_mul_div_atTop

added theorem tendsto_nat_floor_atTop

added theorem tendsto_nat_floor_div_atTop

added theorem tendsto_nat_floor_mul_div_atTop

added theorem tendsto_one_div_add_atTop_nhds_0_nat

added theorem tendsto_pow_atTop_atTop_of_one_lt

added theorem tendsto_pow_atTop_nhdsWithin_0_of_lt_1

added theorem tendsto_pow_atTop_nhds_0_of_lt_1

added theorem tsum_geometric_inv_two

added theorem tsum_geometric_inv_two_ge

added theorem tsum_geometric_nNReal

added theorem tsum_geometric_of_lt_1

added theorem tsum_geometric_two'

added theorem tsum_geometric_two

added theorem uniformity_basis_dist_pow_of_lt_1