Taylor polynomials: sign of the remainder and the derivatives of f(x) / x

Two facts about Mathlib's Taylor polynomials taylorWithinEval f n s x₀ x.

• Sign of the remainder. As a function of the expansion point, the derivative of x₀ ↦ taylorWithinEval f n s x₀ x is (x - x₀)ⁿ / n! · f⁽ⁿ⁺¹⁾(x₀). If (-1)ⁿ f⁽ⁿ⁺¹⁾ ≥ 0 on (x, y), this derivative is nonnegative there, so the Taylor polynomial of order n expanded at y and evaluated at the left endpoint x dominates f x: the Taylor remainder has a sign.

• Derivatives of f(x) / x. By the Leibniz rule and dᵐ/dxᵐ x⁻¹ = (-1)ᵐ m! x⁻ᵐ⁻¹,

  dⁿ/dtⁿ (f(t) / t) = (-1)ⁿ n! t⁻ⁿ⁻¹ · Σ_{k ≤ n} f⁽ᵏ⁾(t) (0 - t)ᵏ / k!,

  the last factor being the Taylor polynomial of order n of f expanded at t and evaluated at 0.

Combined, they show that the iterated derivatives of f(t) / t alternate in sign whenever f is nonnegative and the derivatives of f' alternate in sign — the statement that a Bernstein function divided by its parameter is completely monotone.

Main declarations

• TauCeti.le_taylorWithinEval_of_neg_one_pow_mul_iteratedDerivWithin_nonneg: if (-1)ⁿ f⁽ⁿ⁺¹⁾ ≥ 0 on (x, y), then f x is at most the Taylor polynomial of order n at y, evaluated at x.
• TauCeti.iteratedDeriv_div_id: the formula for the n-th derivative of t ↦ f t / t.

theorem TauCeti.le_taylorWithinEval_of_neg_one_pow_mul_iteratedDerivWithin_nonneg {f : ℝ → ℝ} {s : Set ℝ} {n : ℕ} {x y : ℝ} (hs : IsOpen s) (hxy : x ≤ y) (hsub : Set.Icc x y ⊆ s) (hf : ContDiffOn ℝ (↑n + 1) f s) (hsign : ∀ z ∈ Set.Ioo x y, 0 ≤ (-1) ^ n * iteratedDerivWithin (n + 1) f s z) : f x ≤ taylorWithinEval f n s y x

The Taylor remainder has a sign. Let f be C^(n+1) on an open set s containing [x, y], with (-1)ⁿ f⁽ⁿ⁺¹⁾ ≥ 0 on (x, y). Then the Taylor polynomial of order n of f expanded at y and evaluated at x is at least f x.

theorem TauCeti.iteratedDeriv_div_id {f : ℝ → ℝ} {s : Set ℝ} {n : ℕ} {t : ℝ} (hs : IsOpen s) (ht : t ∈ s) (ht0 : t ≠ 0) (hf : ContDiffOn ℝ (↑n) f s) : iteratedDeriv n (fun (x : ℝ) => f x / x) t = (-1) ^ n * ↑n.factorial * (t ^ (n + 1))⁻¹ * taylorWithinEval f n s t 0

The derivatives of f(t) / t. If f is C^n on an open set s containing t ≠ 0, then dⁿ/dtⁿ (f(t) / t) = (-1)ⁿ n! t⁻ⁿ⁻¹ · T(0), where T is the Taylor polynomial of order n of f expanded at t.