Commit 2023-05-08 05:55 3c742941

View on Github →

feat: port Analysis.SpecificLimits.Normed (#3419)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecificLimits/Normed.lean

added theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero

added theorem Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded

added theorem Antitone.tendsto_alternating_series_of_tendsto_zero

added theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero

added theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded

added theorem Monotone.tendsto_alternating_series_of_tendsto_zero

added theorem NormedAddCommGroup.cauchy_series_of_le_geometric''

added theorem NormedAddCommGroup.cauchy_series_of_le_geometric'

added theorem NormedField.continuousAt_inv

added theorem NormedField.continuousAt_zpow

added theorem NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop

added theorem NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop

added theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded

added theorem NormedRing.summable_geometric_of_norm_lt_1

added theorem NormedRing.tsum_geometric_of_norm_lt_1

added theorem Real.summable_pow_div_factorial

added theorem Real.tendsto_pow_div_factorial_atTop

added theorem TFAE_exists_lt_isLittleO_pow

added theorem cauchySeq_finset_of_geometric_bound

added theorem cauchy_series_of_le_geometric

added theorem dist_partial_sum'

added theorem dist_partial_sum

added theorem dist_partial_sum_le_of_le_geometric

added theorem geom_series_mul_neg

added theorem hasSum_coe_mul_geometric_of_norm_lt_1

added theorem hasSum_geometric_of_abs_lt_1

added theorem hasSum_geometric_of_norm_lt_1

added theorem isBigO_pow_pow_of_le_left

added theorem isLittleO_coe_const_pow_of_one_lt

added theorem isLittleO_pow_const_const_pow_of_one_lt

added theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt

added theorem isLittleO_pow_pow_of_abs_lt_left

added theorem isLittleO_pow_pow_of_lt_left

added theorem mul_neg_geom_series

added theorem norm_sub_le_of_geometric_bound_of_hasSum

added theorem norm_sum_neg_one_pow_le

added theorem not_summable_of_ratio_norm_eventually_ge

added theorem not_summable_of_ratio_test_tendsto_gt_one

added theorem summable_geometric_iff_norm_lt_1

added theorem summable_geometric_of_abs_lt_1

added theorem summable_geometric_of_norm_lt_1

added theorem summable_norm_pow_mul_geometric_of_norm_lt_1

added theorem summable_of_absolute_convergence_real

added theorem summable_of_ratio_norm_eventually_le

added theorem summable_of_ratio_test_tendsto_lt_one

added theorem summable_pow_mul_geometric_of_norm_lt_1

added theorem tendsto_norm_atTop_atTop

added theorem tendsto_norm_zero'

added theorem tendsto_pow_atTop_nhds_0_of_abs_lt_1

added theorem tendsto_pow_atTop_nhds_0_of_norm_lt_1

added theorem tendsto_pow_const_div_const_pow_of_one_lt

added theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one

added theorem tendsto_pow_const_mul_const_pow_of_lt_one

added theorem tendsto_self_mul_const_pow_of_abs_lt_one

added theorem tendsto_self_mul_const_pow_of_lt_one

added theorem tsum_coe_mul_geometric_of_norm_lt_1

added theorem tsum_geometric_of_abs_lt_1

added theorem tsum_geometric_of_norm_lt_1