Theorems · Theorem · global analysis

Real.taylor_tendsto

∀ {f : ℝ → ℝ} {x₀ : ℝ} {n : ℕ} {s : Set ℝ},
  Convex ℝ s →
    x₀ ∈ s →
      ContDiffOn ℝ (↑n) f s →
        Filter.Tendsto (fun x => (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n) (nhdsWithin x₀ s) (nhds 0)

Taylor's theorem as a limit.

Defined in: Mathlib.Analysis.Calculus.Taylor
Cited by: 0 results in Mathlib
Foundations: Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
Filterproof · cited by 8,121
nhdsstatement and proof · cited by 5,554
ENatstatement · cited by 4,985
Filter.Tendstostatement and proof · cited by 3,814
WithTopstatement · cited by 3,754
nhdsWithinstatement and proof · cited by 1,912
Convexstatement and proof · cited by 551
ContDiffOnstatement and proof · cited by 294
div_eq_inv_mulproof · cited by 146
taylorWithinEvalstatement and proof · cited by 27

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.