Theorems · Definition · global analysis

taylorWithin

{E : Type u_2} →
  [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → (ℝ → E) → ℕ → Set ℝ → ℝ → PolynomialModule ℝ E

The Taylor polynomial with derivatives inside of a set s. The Taylor polynomial is given by $$∑_{k=0}^n \frac{(x - x₀)^k}{k!} f^{(k)}(x₀),$$ where $f^{(k)}(x₀)$ denotes the iterated derivative in the set s.

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace