Local Second-Order Taylor Remainder

Proved

FunctionalInequalities.Analysis.local_taylor_two_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a local Taylor estimate in finite-dimensional Euclidean space.

Let $\psi:\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))\to\mathbb R$ be twice continuously differentiable at $x_0$ , and let $\varepsilon>0$ . Then there exists $r>0$ such that every $x$ with $\|x-x_0\|<r$ satisfies

\left|\psi(x)-\left(\psi(x_0)+D\psi(x_0)(x-x_0)+\frac12D^2\psi(x_0)[x-x_0,x-x_0]\right)\right| \le \varepsilon\|x-x_0\|^2.

The result supplies a quantitative second-order remainder bound near one point and is used as a technical ingredient in touching-test arguments.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private lemma local_taylor_two
    {n : ℕ} {ψ : EuclideanSpace ℝ (Fin n) → ℝ}
    {x₀ : EuclideanSpace ℝ (Fin n)}
    (hψ : ContDiffAt ℝ 2 ψ x₀) {ε : ℝ} (hε : 0 < ε) :
    ∃ r > 0, ∀ x ∈ ball x₀ r,
      |ψ x - (ψ x₀ + fderiv ℝ ψ x₀ (x - x₀) +
        (1 / 2 : ℝ) *
          (fderiv ℝ (fderiv ℝ ψ) x₀ (x - x₀)) (x - x₀))| ≤
        ε * ‖x - x₀‖ ^ 2

Module navigation

Module: Analysis/Convex/Viscosity.

Previous: hessianMatrix_quadratic · Next: le_det_hessianMatrix_of_upper_touch.

Source excerpt, lines 261–269 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Viscosity

open Set Metric Filter

Formal statement

 lemma FunctionalInequalities.Analysis.local_taylor_two_readable
    {n : ℕ} {ψ : EuclideanSpace ℝ (Fin n) → ℝ}
    {x₀ : EuclideanSpace ℝ (Fin n)}
    (hψ : ContDiffAt ℝ 2 ψ x₀) {ε : ℝ} (hε : 0 < ε) :
    ∃ r > 0, ∀ x ∈ ball x₀ r,
      |ψ x - (ψ x₀ + fderiv ℝ ψ x₀ (x - x₀) +
        (1 / 2 : ℝ) *
          (fderiv ℝ (fderiv ℝ ψ) x₀ (x - x₀)) (x - x₀))| ≤
        ε * ‖x - x₀‖ ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Viscosity.lean#L261-L383 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Viscosity`, declaration `_private.FunctionalInequalities.Analysis.Convex.Viscosity.0.FunctionalInequalities.Analysis.local_taylor_two`; the repository is private at upload time).

View graph