Commit 2024-06-04 18:12 574e5dab

View on Github →

feat: Limits under division by a positive/negative number (#12693) and rename a few lemmas to make clear that neg refers to < 0, not to -.

Estimated changes

Modified Mathlib/Algebra/QuadraticDiscriminant.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean

Modified Mathlib/Analysis/SpecialFunctions/Polynomials.lean

Modified Mathlib/MeasureTheory/Integral/ExpDecay.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

Modified Mathlib/Order/Filter/Archimedean.lean

added theorem Filter.Tendsto.atBot_mul_const_of_neg'

deleted theorem Filter.Tendsto.atBot_mul_neg_const'

added theorem Filter.Tendsto.atTop_mul_const_of_neg'

deleted theorem Filter.Tendsto.atTop_mul_neg_const'

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.Tendsto.atBot_mul_const_of_neg

deleted theorem Filter.Tendsto.atBot_mul_neg_const

added theorem Filter.Tendsto.atTop_div_const_of_neg

added theorem Filter.Tendsto.atTop_mul_const_of_neg

deleted theorem Filter.Tendsto.atTop_mul_neg_const

added theorem Filter.Tendsto.const_mul_atBot_of_neg

added theorem Filter.Tendsto.const_mul_atTop_of_neg

deleted theorem Filter.Tendsto.neg_const_mul_atBot

deleted theorem Filter.Tendsto.neg_const_mul_atTop

added theorem Filter.tendsto_div_const_atBot_iff

added theorem Filter.tendsto_div_const_atBot_iff_neg

added theorem Filter.tendsto_div_const_atBot_iff_pos

added theorem Filter.tendsto_div_const_atBot_of_neg

added theorem Filter.tendsto_div_const_atBot_of_pos

added theorem Filter.tendsto_div_const_atTop_iff

added theorem Filter.tendsto_div_const_atTop_iff_neg

added theorem Filter.tendsto_div_const_atTop_of_neg