Commit 2023-08-05 11:50 944ee07e

View on Github →

feat: characterizations of IsBigO along atTop (#6198) This PR adds a way to characterize IsBigO along the atTop filter, for cases where we want the constant to depend on a "starting point" n₀. It also adds the lemma tendsto_nhds_of_eventually_eq.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.isBigO_atTop_iff_eventually_exists

added theorem Asymptotics.isBigO_atTop_iff_eventually_exists_pos

Modified Mathlib/Order/BoundedOrder.lean

added theorem Antitone.exists

added theorem Monotone.exists

added theorem forall_ge_iff

added theorem forall_le_iff

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.exists_eventually_atBot

added theorem Filter.exists_eventually_atTop

Modified Mathlib/Topology/Basic.lean

added theorem tendsto_nhds_of_eventually_eq