Theorems · Theorem · real analysis

tendsto_apply_add_mul_sq_div_sub

∀ {f : ℝ → ℝ} {x a c d : ℝ} {l : Filter ℝ},
  l ≤ nhdsWithin x {x}ᶜ →
    Filter.Tendsto (fun y => (f y - d) / (y - x)) l (nhds a) →
      Filter.Tendsto (fun y => y + c * (y - x) ^ 2) l l →
        Filter.Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (nhds a)

If (f y - f x) / (y - x) converges to a limit as y tends to x, then the same goes if y is shifted a little bit, i.e., f (y + (y-x)^2) - f x) / (y - x) converges to the same limit. This lemma contains a slightly more general version of this statement (where one considers convergence along some subfilter, typically 𝓝[<] x or 𝓝[>] x) tailored to the application to almost everywhere differentiability of monotone functions.

Defined in

Mathlib.Analysis.Calculus.Monotone

Cited by

2 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound