Commit 2025-05-20 14:06 819e8e59

View on Github →

feat(Analysis/Asymptotics): add LinearGrowth (#24442) This new file is about the linear growth of sequences of extended real numbers, expressed using liminf and limsups. The documentation, names, lemmas and their proofs are directly ported from Asymptotics.ExpGrowth. Some auxiliary lemmas in ExpGrowth are moved to LinGrowth. ExpGrowthInf and ExpGrowthSup can be expressed using LinearGrowthInf and LinearGrowthSup. Any proof longer than four lines in ExpGrowth, and which has a linear equivalent, uses this strategy.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/ExpGrowth.lean

deleted theorem ExpGrowth.EReal.eventually_atTop_exists_nat_between

deleted theorem ExpGrowth.Real.eventually_atTop_exists_int_between

deleted theorem ExpGrowth.Real.eventually_atTop_exists_nat_between

added theorem ExpGrowth.expGrowthInf_def

added theorem ExpGrowth.expGrowthSup_def

deleted theorem ExpGrowth.linGrowthInf_nonneg

deleted theorem ExpGrowth.tendsto_atTop_of_linGrowthInf_pos

modified theorem Monotone.expGrowthInf_comp_mul

modified theorem Monotone.expGrowthSup_comp

modified theorem Monotone.expGrowthSup_comp_mul

Created Mathlib/Analysis/Asymptotics/LinearGrowth.lean

added theorem Eventually.le_linearGrowthInf

added theorem Eventually.linearGrowthSup_le

added theorem Frequently.le_linearGrowthSup

added theorem Frequently.linearGrowthInf_le

added theorem LinearGrowth.EReal.eventually_atTop_exists_nat_between

added theorem LinearGrowth.Real.eventually_atTop_exists_int_between

added theorem LinearGrowth.Real.eventually_atTop_exists_nat_between

added theorem LinearGrowth.eventually_le_mul

added theorem LinearGrowth.eventually_mul_le

added theorem LinearGrowth.frequently_le_mul

added theorem LinearGrowth.frequently_mul_le

added theorem LinearGrowth.le_linearGrowthInf_add

added theorem LinearGrowth.le_linearGrowthInf_comp

added theorem LinearGrowth.le_linearGrowthInf_iff

added theorem LinearGrowth.le_linearGrowthSup_add'

added theorem LinearGrowth.le_linearGrowthSup_add

added theorem LinearGrowth.le_linearGrowthSup_iff

added theorem LinearGrowth.linearGrowthInf_add_le'

added theorem LinearGrowth.linearGrowthInf_add_le

added theorem LinearGrowth.linearGrowthInf_biInf

added theorem LinearGrowth.linearGrowthInf_bot

added theorem LinearGrowth.linearGrowthInf_comp_nonneg

added theorem LinearGrowth.linearGrowthInf_congr

added theorem LinearGrowth.linearGrowthInf_const

added theorem LinearGrowth.linearGrowthInf_const_mul_self

added theorem LinearGrowth.linearGrowthInf_eventually_monotone

added theorem LinearGrowth.linearGrowthInf_iInf

added theorem LinearGrowth.linearGrowthInf_inf

added theorem LinearGrowth.linearGrowthInf_le_iff

added theorem LinearGrowth.linearGrowthInf_le_linearGrowthSup

added theorem LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le

added theorem LinearGrowth.linearGrowthInf_le_of_eventually_le

added theorem LinearGrowth.linearGrowthInf_monotone

added theorem LinearGrowth.linearGrowthInf_natCast_nonneg

added theorem LinearGrowth.linearGrowthInf_neg

added theorem LinearGrowth.linearGrowthInf_top

added theorem LinearGrowth.linearGrowthInf_zero

added theorem LinearGrowth.linearGrowthSup_add_le

added theorem LinearGrowth.linearGrowthSup_biSup

added theorem LinearGrowth.linearGrowthSup_bot

added theorem LinearGrowth.linearGrowthSup_comp_le

added theorem LinearGrowth.linearGrowthSup_comp_nonneg

added theorem LinearGrowth.linearGrowthSup_congr

added theorem LinearGrowth.linearGrowthSup_const

added theorem LinearGrowth.linearGrowthSup_const_mul_self

added theorem LinearGrowth.linearGrowthSup_eventually_monotone

added theorem LinearGrowth.linearGrowthSup_iSup

added theorem LinearGrowth.linearGrowthSup_inv

added theorem LinearGrowth.linearGrowthSup_le_iff

added theorem LinearGrowth.linearGrowthSup_le_of_eventually_le

added theorem LinearGrowth.linearGrowthSup_monotone

added theorem LinearGrowth.linearGrowthSup_sup

added theorem LinearGrowth.linearGrowthSup_top

added theorem LinearGrowth.linearGrowthSup_zero

added theorem LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos

added theorem LinearGrowth.tendsto_atTop_of_linearGrowthInf_pos

added theorem Monotone.le_linearGrowthSup_comp

added theorem Monotone.linearGrowthInf_comp

added theorem Monotone.linearGrowthInf_comp_le

added theorem Monotone.linearGrowthInf_comp_mul

added theorem Monotone.linearGrowthInf_nonneg

added theorem Monotone.linearGrowthSup_comp

added theorem Monotone.linearGrowthSup_comp_mul

added theorem Monotone.linearGrowthSup_nonneg

Modified Mathlib/Order/BoundedOrder/Basic.lean

added theorem Pi.bot_comp

added theorem Pi.top_comp