Commit 2026-02-11 11:43 dec6b934

View on Github →

feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to Tendsto f atTop l (#34403) Prove lemmas we use in compute_asymptotics to reduce various asymptotic goals to the case Tendsto f atTop l.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

added theorem Asymptotics.IsLittleO.of_tendsto_div_atBot

added theorem Asymptotics.IsLittleO.of_tendsto_div_atTop

added theorem Asymptotics.isBigOWith_of_div_tendsto_nhds

added theorem Asymptotics.isBigO_of_div_tendsto_nhds_of_ne_zero

Modified Mathlib/Analysis/Asymptotics/Theta.lean

added theorem Asymptotics.isTheta_of_div_tendsto_nhds_ne_zero

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

Modified Mathlib/Order/Filter/AtTopBot/Group.lean

added theorem Filter.tendsto_comp_inv_atBot_iff

added theorem Filter.tendsto_comp_inv_atTop_iff

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean

added theorem Tactic.ComputeAsymptotics.isBigOWith_of_tendsto_bot

added theorem Tactic.ComputeAsymptotics.isBigOWith_of_tendsto_top

added theorem Tactic.ComputeAsymptotics.isBigO_of_div_tendsto_atBot

added theorem Tactic.ComputeAsymptotics.isBigO_of_div_tendsto_atTop

added theorem Tactic.ComputeAsymptotics.tendsto_nhdsGT_of_tendsto_atTop

added theorem Tactic.ComputeAsymptotics.tendsto_nhdsLT_of_tendsto_atTop

added theorem Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop

added theorem Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem Filter.inv_nhdsGT

added theorem Filter.inv_nhdsLT

added theorem Filter.inv_nhdsNE

added theorem Filter.map_mul_left_nhdsGT

added theorem Filter.map_mul_left_nhdsLT

added theorem Filter.map_mul_left_nhdsNE

added theorem Filter.map_mul_right_nhdsGT

added theorem Filter.map_mul_right_nhdsLT

added theorem Filter.map_mul_right_nhdsNE

Modified Mathlib/Topology/Algebra/Order/Field.lean

added theorem tendsto_nhdsGT_zero_of_comp_inv_tendsto_atTop

added theorem tendsto_nhdsLT_zero_of_comp_inv_tendsto_atBot