Commit 2026-02-05 07:38 b7a18497

View on Github →

chore(Calculus/FDeriv): review asymptotics lemmas (#34832)

Generalize some lemmas to the TVS setting.
Use Topology.IsInducing instead of AntilipschitzWith or ContinuousLinearEquiv.
Move the definition of Asymptotics.IsEquivalent to Defs.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

deleted def Asymptotics.IsEquivalent

Modified Mathlib/Analysis/Asymptotics/Defs.lean

added def Asymptotics.IsEquivalent

Modified Mathlib/Analysis/Asymptotics/TVS.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem HasDerivAtFilter.isBigO_sub_rev

added theorem HasDerivAtFilter.isEquivalent_sub

added theorem HasDerivAtFilter.isTheta_sub

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

modified theorem Asymptotics.IsBigO.hasFDerivWithinAt

added theorem DifferentiableAt.isBigOTVS_sub

added theorem DifferentiableAt.isBigO_sub

added theorem DifferentiableWithinAt.isBigOTVS_sub

modified theorem DifferentiableWithinAt.isBigO_sub

added theorem HasFDerivAt.isBigOTVS_sub

added theorem HasFDerivAt.isBigO_sub

added theorem HasFDerivAtFilter.isBigOTVS_sub

added theorem HasFDerivAtFilter.isEquivalent_sub

added theorem HasFDerivAtFilter.isThetaTVS_sub

added theorem HasFDerivAtFilter.isTheta_sub

added theorem HasFDerivWithinAt.isBigOTVS_sub

added theorem HasFDerivWithinAt.isBigO_sub

added theorem HasStrictFDerivAt.isBigOTVS_sub

added theorem HasStrictFDerivAt.isEquivalent_sub

added theorem HasStrictFDerivAt.isThetaTVS_sub

added theorem HasStrictFDerivAt.isTheta_sub

Modified Mathlib/Analysis/Calculus/FDeriv/Const.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

Modified Mathlib/Analysis/SpecialFunctions/Choose.lean

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean