Commit 2025-01-09 16:34 efd3027b

View on Github →

feat(Asymptotics): add IsBigO.of_norm_eventuallyLE (#20415) .. and .of_norm_le. Also use of_bound' instead of of_bound 1.

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/RadiusLiminf.lean

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsBigO.of_norm_eventuallyLE

added theorem Asymptotics.IsBigO.of_norm_le

Modified Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

Modified Mathlib/Analysis/Asymptotics/Theta.lean

added theorem Asymptotics.IsTheta.of_norm_eventuallyEq

added theorem Asymptotics.IsTheta.of_norm_eventuallyEq_norm

deleted theorem Asymptotics.isTheta_of_norm_eventuallyEq'

deleted theorem Asymptotics.isTheta_of_norm_eventuallyEq

Modified Mathlib/Analysis/Complex/PhragmenLindelof.lean

Modified Mathlib/Analysis/SpecialFunctions/CompareExp.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean