def IsNTimesDiffOn (f : ℝ → ℝ) (n : ℕ) (S : Set ℝ) : Prop

A real-valued function f is n-times differentiable on the set S if S has the unique differentiability property and, for every m < n, the m-th iterated derivative of f within S is itself differentiable on S. Equivalently, the derivatives f', f'', …, f^{(n)} all exist at every point of S.

noncomputable def taylorPolynomial (f : ℝ → ℝ) (x₀ : ℝ) (n : ℕ) (x : ℝ) : ℝ

The n-th order Taylor polynomial of f centered at x₀, evaluated at x: P_n(x) = ∑_{k=0}^{n} f^{(k)}(x₀) / k! · (x - x₀)^k.

theorem taylor_theorem (f : ℝ → ℝ) (n : ℕ) (x₀ x : ℝ) (hx : x₀ < x) (hf : ContDiffOn ℝ (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) : ∃ c ∈ Set.Ioo x₀ x, f x = ∑ k ∈ Finset.range (n + 1), iteratedDerivWithin k f (Set.Icc x₀ x) x₀ / ↑k.factorial * (x - x₀) ^ k + iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) c / ↑(n + 1).factorial * (x - x₀) ^ (n + 1)

Taylor's theorem (Lagrange form of the remainder). Suppose f : ℝ → ℝ is n times continuously differentiable on [x₀, x] and its n-th derivative is differentiable on the open interval (x₀, x). Then there exists c ∈ (x₀, x) such that f(x) = ∑_{k=0}^{n} f^{(k)}(x₀)/k! · (x - x₀)^k + f^{(n+1)}(c)/(n+1)! · (x - x₀)^{n+1}. That is, f(x) equals the n-th order Taylor polynomial at x₀ plus the Lagrange remainder term evaluated at some intermediate point c.

def IsStrictLocalMin (f : ℝ → ℝ) (x₀ : ℝ) : Prop

A function f : ℝ → ℝ has a strict local (relative) minimum at x₀ if f x₀ < f x for all x sufficiently close to but distinct from x₀.

theorem second_derivative_test_min (f : ℝ → ℝ) (x₀ : ℝ) (hf : ContDiffAt ℝ 2 f x₀) (hf1 : deriv f x₀ = 0) (hf2 : 0 < iteratedDeriv 2 f x₀) : IsStrictLocalMin f x₀

Second derivative test for a strict local minimum. If f : ℝ → ℝ is twice continuously differentiable at x₀, with f'(x₀) = 0 and f''(x₀) > 0, then f has a strict relative minimum at x₀.