Commit 2025-05-03 01:44 63d94ce7

View on Github →

feat(Asymptotics): define IsBigOTVS (#23756)

Turn IsLittleOTVS into a 1-field structure. We may want to replace the definition with "the ratio of egauges tends to zero". In ENNReal, it's the right definition.
Define IsBigOTVS, prove basic API lemmas.
Prove lemmas about IsLittleOTVS in (indexed) products.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

added theorem Asymptotics.Filter.Tendsto.isBigOTVS_one

added theorem Asymptotics.IsBigOTVS.add

added theorem Asymptotics.IsBigOTVS.comp_tendsto

added theorem Asymptotics.IsBigOTVS.mono

added theorem Asymptotics.IsBigOTVS.prodMk

added theorem Asymptotics.IsBigOTVS.proj

added theorem Asymptotics.IsBigOTVS.trans

added theorem Asymptotics.IsBigOTVS.trans_isLittleOTVS

added structure Asymptotics.IsBigOTVS

modified theorem Asymptotics.IsLittleOTVS.add

added theorem Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul_ennreal

added theorem Asymptotics.IsLittleOTVS.isBigOTVS

added theorem Asymptotics.IsLittleOTVS.prodMk

added theorem Asymptotics.IsLittleOTVS.proj

modified theorem Asymptotics.IsLittleOTVS.trans

added theorem Asymptotics.IsLittleOTVS.trans_isBigOTVS

added structure Asymptotics.IsLittleOTVS

deleted def Asymptotics.IsLittleOTVS

added theorem Asymptotics.isBigOTVS_iff_smallSets

added theorem Asymptotics.isBigOTVS_map

added theorem Asymptotics.isBigOTVS_pi

added theorem Asymptotics.isBigOTVS_prodMk_left

added theorem Asymptotics.isLittleOTVS_iff_tendsto_div

added theorem Asymptotics.isLittleOTVS_pi

added theorem Asymptotics.isLittleOTVS_prodMk_left

added theorem ContinuousLinearMap.isBigOTVS_comp

added theorem ContinuousLinearMap.isBigOTVS_fun_comp

added theorem ContinuousLinearMap.isBigOTVS_id

deleted theorem Filter.HasBasis.isLittleOTVS_iff