noncomputable def taylorPolynomial (f : ℝ → ℝ) (x0 : ℝ) (n : ℕ) : Polynomial ℝ

Definition 4.3.1: For an n-times differentiable function f near x0 ∈ ℝ, the nth-order Taylor polynomial at x0 is P_n^{x0}(x) = ∑_{k=0}^n f^(k)(x0) / k! * (x - x0)^k.

Equations

• taylorPolynomial f x0 n = ∑ k ∈ Finset.range (n + 1), Polynomial.C (iteratedDeriv k f x0 / ↑k.factorial) * (Polynomial.X - Polynomial.C x0) ^ k

theorem iteratedDerivWithin_eq_iteratedDeriv_Icc {f : ℝ → ℝ} {x0 x c : ℝ} {k n : ℕ} (hx0x : x0 < x) (hc : c ∈ Set.Ioo x0 x) (hcont : ContDiffOn ℝ (↑n + 1) f (Set.Icc x0 x)) (hk : k ≤ n + 1) : iteratedDerivWithin k f (Set.Icc x0 x) c = iteratedDeriv k f c

On an interior point of Icc x₀ x, within-iterated derivatives agree with ordinary ones.

theorem taylorWithinEval_eq_taylorPolynomial {f : ℝ → ℝ} {x0 x : ℝ} {n : ℕ} (hx0x : x0 < x) (hcontAt : ContDiffAt ℝ (↑n + 1) f x0) : taylorWithinEval f n (Set.Icc x0 x) x0 x = Polynomial.eval x (taylorPolynomial f x0 n)

Identify taylorWithinEval on an interval with the explicit Taylor polynomial.

theorem taylor_with_remainder_pos {f : ℝ → ℝ} {x0 x : ℝ} {n : ℕ} (hx0x : x0 < x) (hcont : ContDiffOn ℝ (↑n + 1) f (Set.Icc x0 x)) (hcontAt : ContDiffAt ℝ (↑n + 1) f x0) : ∃ c ∈ Set.Icc x0 x, f x = Polynomial.eval x (taylorPolynomial f x0 n) + iteratedDeriv (n + 1) f c / ↑(n + 1).factorial * (x - x0) ^ (n + 1)

Taylor's theorem on a positively oriented interval.

theorem taylor_with_remainder_neg {f : ℝ → ℝ} {x0 x : ℝ} {n : ℕ} (hx0x : x < x0) (hcont : ContDiffOn ℝ (↑n + 1) f (Set.Icc x x0)) (hcontAt : ContDiffAt ℝ (↑n + 1) f x0) : ∃ c ∈ Set.Icc x x0, f x = Polynomial.eval x (taylorPolynomial f x0 n) + iteratedDeriv (n + 1) f c / ↑(n + 1).factorial * (x - x0) ^ (n + 1)

Taylor's theorem on a negatively oriented interval, obtained by reflection.

theorem taylor_with_remainder {f : ℝ → ℝ} {a b x0 x : ℝ} {n : ℕ} (hx0 : x0 ∈ Set.Ioo a b) (hx : x ∈ Set.Icc a b) (hx0x : x0 ≠ x) (hcont : ContDiffOn ℝ (↑n + 1) f (Set.Icc a b)) : ∃ c ∈ Set.Icc (min x0 x) (max x0 x), f x = Polynomial.eval x (taylorPolynomial f x0 n) + iteratedDeriv (n + 1) f c / ↑(n + 1).factorial * (x - x0) ^ (n + 1)

Theorem 4.3.2 (Taylor): If f : ℝ → ℝ has n continuous derivatives on [a, b] and the (n+1)st derivative exists on (a, b), then for distinct points x₀, x ∈ [a, b] there is a point c between them such that f x = Pₙ^{x₀}(x) + f^{(n+1)}(c) / (n+1)! * (x - x₀)^{n+1}.

theorem abs_sub_le_of_mem_interval {x x0 y : ℝ} (hy : y ∈ Set.Icc (min x x0) (max x x0)) : |y - x0| ≤ |x - x0|

If y lies between x and x₀, then the distance from y to x₀ is bounded by the distance from x to x₀.

theorem interval_subset_Ioo_of_abs_sub_lt {a b x0 x : ℝ} (hx0 : x0 ∈ Set.Ioo a b) (hx : |x - x0| < min (x0 - a) (b - x0)) : Set.Icc (min x x0) (max x x0) ⊆ Set.Ioo a b

Points sufficiently close to x₀ stay inside (a, b), and the whole interval between them and x₀ also lies in (a, b).

theorem second_derivative_test {f : ℝ → ℝ} {a b x0 : ℝ} (hx0 : x0 ∈ Set.Ioo a b) (hcont : ContDiffOn ℝ 2 f (Set.Ioo a b)) (hderiv_zero : deriv f x0 = 0) (hpos : deriv (deriv f) x0 > 0) : ∃ ε > 0, ∀ {x : ℝ}, x ∈ Set.Ioo a b → x ≠ x0 → |x - x0| < ε → f x0 < f x

Proposition 4.3.3 (Second derivative test). If f : (a, b) → ℝ is twice continuously differentiable, x0 ∈ (a, b), f' x0 = 0, and f'' x0 > 0, then x0 is a strict relative minimum of f.