Commit 2025-01-18 20:11 95878d00

View on Github →

chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785) This was a long file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

Renamed Mathlib/Analysis/Asymptotics/Asymptotics.lean to Mathlib/Analysis/Asymptotics/Defs.lean

deleted theorem Asymptotics.IsBigO.comp_summable_norm

deleted theorem Asymptotics.IsBigO.const_smul_left

deleted theorem Asymptotics.IsBigO.const_smul_self

deleted theorem Asymptotics.IsBigO.eq_zero_of_norm_pow

deleted theorem Asymptotics.IsBigO.eq_zero_of_norm_pow_within

deleted theorem Asymptotics.IsBigO.finsetProd

deleted theorem Asymptotics.IsBigO.isBoundedUnder_le

deleted theorem Asymptotics.IsBigO.listProd

deleted theorem Asymptotics.IsBigO.multisetProd

deleted theorem Asymptotics.IsBigO.natCast_atTop

deleted theorem Asymptotics.IsBigO.of_pow

deleted theorem Asymptotics.IsBigO.smul

deleted theorem Asymptotics.IsBigO.smul_isLittleO

deleted theorem Asymptotics.IsBigO.trans_tendsto

deleted theorem Asymptotics.IsBigO.trans_tendsto_nhds

deleted theorem Asymptotics.IsBigOWith.const_smul_left

deleted theorem Asymptotics.IsBigOWith.const_smul_self

deleted theorem Asymptotics.IsBigOWith.exists_eq_mul

deleted theorem Asymptotics.IsBigOWith.right_le_add_of_lt_one

deleted theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one

deleted theorem Asymptotics.IsBigOWith.smul

deleted theorem Asymptotics.IsLittleO.const_smul_left

deleted theorem Asymptotics.IsLittleO.finsetProd

deleted theorem Asymptotics.IsLittleO.listProd

deleted theorem Asymptotics.IsLittleO.multisetProd

deleted theorem Asymptotics.IsLittleO.natCast_atTop

deleted theorem Asymptotics.IsLittleO.right_isBigO_add'

deleted theorem Asymptotics.IsLittleO.right_isBigO_add

deleted theorem Asymptotics.IsLittleO.right_isBigO_sub

deleted theorem Asymptotics.IsLittleO.smul

deleted theorem Asymptotics.IsLittleO.smul_isBigO

deleted theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero

deleted theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero

deleted theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto

deleted theorem Asymptotics.IsLittleO.trans_tendsto

deleted theorem Asymptotics.bound_of_isBigO_cofinite

deleted theorem Asymptotics.bound_of_isBigO_nat_atTop

deleted theorem Asymptotics.continuousAt_iff_isLittleO

deleted theorem Asymptotics.div_isBoundedUnder_of_isBigO

deleted theorem Asymptotics.isBigOWith_const_one

deleted theorem Asymptotics.isBigOWith_iff_exists_eq_mul

deleted theorem Asymptotics.isBigOWith_of_eq_mul

deleted theorem Asymptotics.isBigOWith_pi

deleted theorem Asymptotics.isBigOWith_principal

deleted theorem Asymptotics.isBigOWith_top

deleted theorem Asymptotics.isBigO_atTop_iff_eventually_exists

deleted theorem Asymptotics.isBigO_atTop_iff_eventually_exists_pos

deleted theorem Asymptotics.isBigO_cofinite_iff

deleted theorem Asymptotics.isBigO_const_iff

deleted theorem Asymptotics.isBigO_const_left_iff_pos_le_norm

deleted theorem Asymptotics.isBigO_const_of_ne

deleted theorem Asymptotics.isBigO_const_of_tendsto

deleted theorem Asymptotics.isBigO_const_one

deleted theorem Asymptotics.isBigO_const_smul_left

deleted theorem Asymptotics.isBigO_const_smul_right

deleted theorem Asymptotics.isBigO_iff_div_isBoundedUnder

deleted theorem Asymptotics.isBigO_iff_exists_eq_mul

deleted theorem Asymptotics.isBigO_iff_isBoundedUnder_le_div

deleted theorem Asymptotics.isBigO_mul_iff_isBigO_div

deleted theorem Asymptotics.isBigO_nat_atTop_iff

deleted theorem Asymptotics.isBigO_of_div_tendsto_nhds

deleted theorem Asymptotics.isBigO_one_iff

deleted theorem Asymptotics.isBigO_one_nat_atTop_iff

deleted theorem Asymptotics.isBigO_one_nhds_ne_iff

deleted theorem Asymptotics.isBigO_pi

deleted theorem Asymptotics.isBigO_principal

deleted theorem Asymptotics.isBigO_top

deleted theorem Asymptotics.isLittleO_const_const_iff

deleted theorem Asymptotics.isLittleO_const_id_atBot

deleted theorem Asymptotics.isLittleO_const_id_atTop

deleted theorem Asymptotics.isLittleO_const_id_cobounded

deleted theorem Asymptotics.isLittleO_const_iff

deleted theorem Asymptotics.isLittleO_const_iff_isLittleO_one

deleted theorem Asymptotics.isLittleO_const_left

deleted theorem Asymptotics.isLittleO_const_left_of_ne

deleted theorem Asymptotics.isLittleO_const_smul_left

deleted theorem Asymptotics.isLittleO_const_smul_right

deleted theorem Asymptotics.isLittleO_id_const

deleted theorem Asymptotics.isLittleO_id_one

deleted theorem Asymptotics.isLittleO_iff_exists_eq_mul

deleted theorem Asymptotics.isLittleO_iff_tendsto'

deleted theorem Asymptotics.isLittleO_iff_tendsto

deleted theorem Asymptotics.isLittleO_norm_pow_id

deleted theorem Asymptotics.isLittleO_norm_pow_norm_pow

deleted theorem Asymptotics.isLittleO_one_iff

deleted theorem Asymptotics.isLittleO_one_left_iff

deleted theorem Asymptotics.isLittleO_pi

deleted theorem Asymptotics.isLittleO_pow_id

deleted theorem Asymptotics.isLittleO_pow_pow

deleted theorem Asymptotics.isLittleO_pow_sub_pow_sub

deleted theorem Asymptotics.isLittleO_pow_sub_sub

deleted theorem Asymptotics.isLittleO_principal

deleted theorem Asymptotics.isLittleO_pure

deleted theorem Asymptotics.isLittleO_top

deleted theorem Filter.IsBoundedUnder.isBigO_const

deleted theorem Filter.Tendsto.isBigO_one

deleted theorem Homeomorph.isBigOWith_congr

deleted theorem Homeomorph.isBigO_congr

deleted theorem Homeomorph.isLittleO_congr

deleted theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded

deleted theorem PartialHomeomorph.isBigOWith_congr

deleted theorem PartialHomeomorph.isBigO_congr

deleted theorem PartialHomeomorph.isLittleO_congr

deleted theorem summable_of_isBigO

deleted theorem summable_of_isBigO_nat

Created Mathlib/Analysis/Asymptotics/Lemmas.lean

added theorem Asymptotics.IsBigO.comp_summable_norm

added theorem Asymptotics.IsBigO.const_smul_left

added theorem Asymptotics.IsBigO.const_smul_self

added theorem Asymptotics.IsBigO.eq_zero_of_norm_pow

added theorem Asymptotics.IsBigO.eq_zero_of_norm_pow_within

added theorem Asymptotics.IsBigO.finsetProd

added theorem Asymptotics.IsBigO.isBoundedUnder_le

added theorem Asymptotics.IsBigO.listProd

added theorem Asymptotics.IsBigO.multisetProd

added theorem Asymptotics.IsBigO.natCast_atTop

added theorem Asymptotics.IsBigO.of_pow

added theorem Asymptotics.IsBigO.smul

added theorem Asymptotics.IsBigO.smul_isLittleO

added theorem Asymptotics.IsBigO.trans_tendsto

added theorem Asymptotics.IsBigO.trans_tendsto_nhds

added theorem Asymptotics.IsBigOWith.const_smul_left

added theorem Asymptotics.IsBigOWith.const_smul_self

added theorem Asymptotics.IsBigOWith.exists_eq_mul

added theorem Asymptotics.IsBigOWith.right_le_add_of_lt_one

added theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one

added theorem Asymptotics.IsBigOWith.smul

added theorem Asymptotics.IsLittleO.const_smul_left

added theorem Asymptotics.IsLittleO.finsetProd

added theorem Asymptotics.IsLittleO.listProd

added theorem Asymptotics.IsLittleO.multisetProd

added theorem Asymptotics.IsLittleO.natCast_atTop

added theorem Asymptotics.IsLittleO.right_isBigO_add'

added theorem Asymptotics.IsLittleO.right_isBigO_add

added theorem Asymptotics.IsLittleO.right_isBigO_sub

added theorem Asymptotics.IsLittleO.smul

added theorem Asymptotics.IsLittleO.smul_isBigO

added theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero

added theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero

added theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto

added theorem Asymptotics.IsLittleO.trans_tendsto

added theorem Asymptotics.bound_of_isBigO_cofinite

added theorem Asymptotics.bound_of_isBigO_nat_atTop

added theorem Asymptotics.continuousAt_iff_isLittleO

added theorem Asymptotics.div_isBoundedUnder_of_isBigO

added theorem Asymptotics.isBigOWith_const_one

added theorem Asymptotics.isBigOWith_iff_exists_eq_mul

added theorem Asymptotics.isBigOWith_of_eq_mul

added theorem Asymptotics.isBigOWith_pi

added theorem Asymptotics.isBigOWith_principal

added theorem Asymptotics.isBigOWith_top

added theorem Asymptotics.isBigO_atTop_iff_eventually_exists

added theorem Asymptotics.isBigO_atTop_iff_eventually_exists_pos

added theorem Asymptotics.isBigO_cofinite_iff

added theorem Asymptotics.isBigO_const_iff

added theorem Asymptotics.isBigO_const_left_iff_pos_le_norm

added theorem Asymptotics.isBigO_const_of_ne

added theorem Asymptotics.isBigO_const_of_tendsto

added theorem Asymptotics.isBigO_const_one

added theorem Asymptotics.isBigO_const_smul_left

added theorem Asymptotics.isBigO_const_smul_right

added theorem Asymptotics.isBigO_iff_div_isBoundedUnder

added theorem Asymptotics.isBigO_iff_exists_eq_mul

added theorem Asymptotics.isBigO_iff_isBoundedUnder_le_div

added theorem Asymptotics.isBigO_mul_iff_isBigO_div

added theorem Asymptotics.isBigO_nat_atTop_iff

added theorem Asymptotics.isBigO_of_div_tendsto_nhds

added theorem Asymptotics.isBigO_one_iff

added theorem Asymptotics.isBigO_one_nat_atTop_iff

added theorem Asymptotics.isBigO_one_nhds_ne_iff

added theorem Asymptotics.isBigO_pi

added theorem Asymptotics.isBigO_principal

added theorem Asymptotics.isBigO_top

added theorem Asymptotics.isLittleO_const_const_iff

added theorem Asymptotics.isLittleO_const_id_atBot

added theorem Asymptotics.isLittleO_const_id_atTop

added theorem Asymptotics.isLittleO_const_id_cobounded

added theorem Asymptotics.isLittleO_const_iff

added theorem Asymptotics.isLittleO_const_iff_isLittleO_one

added theorem Asymptotics.isLittleO_const_left

added theorem Asymptotics.isLittleO_const_left_of_ne

added theorem Asymptotics.isLittleO_const_smul_left

added theorem Asymptotics.isLittleO_const_smul_right

added theorem Asymptotics.isLittleO_id_const

added theorem Asymptotics.isLittleO_id_one

added theorem Asymptotics.isLittleO_iff_exists_eq_mul

added theorem Asymptotics.isLittleO_iff_tendsto'

added theorem Asymptotics.isLittleO_iff_tendsto

added theorem Asymptotics.isLittleO_norm_pow_id

added theorem Asymptotics.isLittleO_norm_pow_norm_pow

added theorem Asymptotics.isLittleO_one_iff

added theorem Asymptotics.isLittleO_one_left_iff

added theorem Asymptotics.isLittleO_pi

added theorem Asymptotics.isLittleO_pow_id

added theorem Asymptotics.isLittleO_pow_pow

added theorem Asymptotics.isLittleO_pow_sub_pow_sub

added theorem Asymptotics.isLittleO_pow_sub_sub

added theorem Asymptotics.isLittleO_principal

added theorem Asymptotics.isLittleO_pure

added theorem Asymptotics.isLittleO_top

added theorem Filter.IsBoundedUnder.isBigO_const

added theorem Filter.Tendsto.isBigO_one

added theorem Homeomorph.isBigOWith_congr

added theorem Homeomorph.isBigO_congr

added theorem Homeomorph.isLittleO_congr

added theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded

added theorem PartialHomeomorph.isBigOWith_congr

added theorem PartialHomeomorph.isBigO_congr

added theorem PartialHomeomorph.isLittleO_congr

added theorem summable_of_isBigO

added theorem summable_of_isBigO_nat

Modified Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Modified Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

Modified Mathlib/Analysis/Asymptotics/TVS.lean

Modified Mathlib/Analysis/Asymptotics/Theta.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Asymptotics.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean