Commit 2023-07-06 08:30 af0fb7b7

View on Github →

feat: miscellaneous lemmas about asymptotics (#5680)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsBigO.nat_cast_atTop

added theorem Asymptotics.IsLittleO.eventuallyLE

added theorem Asymptotics.IsLittleO.nat_cast_atTop

added theorem Asymptotics.isBigO_iff''

added theorem Asymptotics.isBigO_iff'

Modified Mathlib/Analysis/Asymptotics/Theta.lean

added theorem Asymptotics.IsTheta.add_isLittleO

added theorem Asymptotics.IsTheta.isBigO

added theorem Asymptotics.IsTheta.isBigO_symm

Modified Mathlib/Order/Filter/Archimedean.lean

added theorem Filter.Eventually.int_cast_atBot

added theorem Filter.Eventually.int_cast_atTop

added theorem Filter.Eventually.nat_cast_atTop

added theorem Filter.Eventually.rat_cast_atBot

added theorem Filter.Eventually.rat_cast_atTop

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.Tendsto.eventually_forall_ge_atTop

added theorem Filter.Tendsto.eventually_forall_le_atBot