Theorems · Theorem · global analysis

taylor_isLittleO

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ},
  Convex ℝ s →
    x₀ ∈ s →
      ContDiffOn ℝ (↑n) f s → (fun x => f x - taylorWithinEval f n s x₀ x) =o[nhdsWithin x₀ s] fun x => (x - x₀) ^ n

Taylor's theorem using little-o notation.

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace