Commit 2023-04-17 06:46 de1c73a0

View on Github →

feat: port Analysis.Asymptotics.AsymptoticEquivalent (#3417)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

added theorem Asymptotics.IsEquivalent.add_isLittleO

added theorem Asymptotics.IsEquivalent.congr_left

added theorem Asymptotics.IsEquivalent.congr_right

added theorem Asymptotics.IsEquivalent.div

added theorem Asymptotics.IsEquivalent.exists_eq_mul

added theorem Asymptotics.IsEquivalent.inv

added theorem Asymptotics.IsEquivalent.isBigO_symm

added theorem Asymptotics.IsEquivalent.isLittleO

added theorem Asymptotics.IsEquivalent.mul

added theorem Asymptotics.IsEquivalent.neg

added theorem Asymptotics.IsEquivalent.refl

added theorem Asymptotics.IsEquivalent.smul

added theorem Asymptotics.IsEquivalent.sub_isLittleO

added theorem Asymptotics.IsEquivalent.symm

added theorem Asymptotics.IsEquivalent.tendsto_atBot

added theorem Asymptotics.IsEquivalent.tendsto_atBot_iff

added theorem Asymptotics.IsEquivalent.tendsto_atTop

added theorem Asymptotics.IsEquivalent.tendsto_atTop_iff

added theorem Asymptotics.IsEquivalent.tendsto_const

added theorem Asymptotics.IsEquivalent.tendsto_nhds

added theorem Asymptotics.IsEquivalent.tendsto_nhds_iff

added theorem Asymptotics.IsEquivalent.trans

added def Asymptotics.IsEquivalent

added theorem Asymptotics.IsLittleO.add_isEquivalent

added theorem Asymptotics.IsLittleO.isEquivalent

added theorem Asymptotics.isEquivalent_const_iff_tendsto

added theorem Asymptotics.isEquivalent_iff_exists_eq_mul

added theorem Asymptotics.isEquivalent_iff_tendsto_one

added theorem Asymptotics.isEquivalent_of_tendsto_one'

added theorem Asymptotics.isEquivalent_of_tendsto_one

added theorem Asymptotics.isEquivalent_zero_iff_eventually_zero

added theorem Asymptotics.isEquivalent_zero_iff_isBigO_zero

added theorem Filter.EventuallyEq.isEquivalent