Commit 2025-03-31 15:28 6d323eaa

feat(Analysis/Asymptotics/ExpGrowth): Exponential growth and composition (#22703) This PR adds lemmas about the exponential growth of a composition u ∘ v depending on the exponential growth of u and the linear growth of v. Most new stuff is in Analysis.Asymptotics.ExpGrowth (mostly sections Composition and Monotone sequences). I also slightly modified the four lemmas expGrowthInf_le_iff, le_expGrowthInf_iff, etc. to use large inequalities instead of strict inequalities (it's more comfortable for me). In Data.Real.EReal: A new lemma (the inversion is antitone on the positives), and a small tweak to three lemmas (exists_lt_mul_left_of_nonneg...), making them slightly stronger; their old use is not impacted, and the improvement makes some new proofs slightly nicer. In Order.LiminfLimsup: A few new lemmas about: liminf and limsup of compositions, versions with large inequalities of limsup_le_iff and friends, and a way to compare liminf & limsup of two functions. I've also squeezed some life out of isBoundedUnder_le_mul_of_nonneg by replacing an eventual condition with a frequent condition; the new version is not strictly more general, but the cases which are not covered anymore don't seem really interesting (empty filter or weird structures), so the trade-off feels favorable. In Topology.Algebra.Order.LiminfLimsup: Again, some eventual conditions are replaced by frequent conditions (about the limsup of a product on the reals). In Topology.Instances.EReal.Lemmas: Again, some eventual conditions are replaced by frequent conditions (about the limsup of a product on the extended reals).