Commit 2025-01-13 09:34 6ee88ac3

View on Github →

feat: more results about IsLittleOTVS (#20220) It will be cleaner to generalize the results for fderiv after writing a few more of these lemmas, rather than shuffling everything around.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

added theorem Asymptotics.IsLittleOTVS.bot

added theorem Asymptotics.IsLittleOTVS.comp_tendsto

added theorem Asymptotics.IsLittleOTVS.congr'

added theorem Asymptotics.IsLittleOTVS.congr

added theorem Asymptotics.IsLittleOTVS.congr_left

added theorem Asymptotics.IsLittleOTVS.congr_right

added theorem Asymptotics.IsLittleOTVS.insert

added theorem Asymptotics.IsLittleOTVS.mono

added theorem Asymptotics.IsLittleOTVS.sup

modified theorem Asymptotics.IsLittleOTVS.tendsto_inv_smul

added theorem Asymptotics.IsLittleOTVS.trans

added theorem Asymptotics.IsLittleOTVS.zero

added theorem Asymptotics.isLittleOTVS_congr

added theorem Asymptotics.isLittleOTVS_iff_smallSets

added theorem Asymptotics.isLittleOTVS_insert

modified theorem Asymptotics.isLittleOTVS_map

modified theorem Asymptotics.isLittleOTVS_one

added theorem Asymptotics.isLittleOTVS_sup

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

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

Modified Mathlib/Analysis/Convex/EGauge.lean

added theorem egauge_union

added theorem le_egauge_inter

Modified Mathlib/Order/Filter/Bases.lean

added theorem Filter.eventually_prod_self_iff'