Second Difference Expansion Along a Direction

This is a technical one-dimensional second-difference lemma for a quadratic second-order expansion.

Let $n\in\mathbb N$, let $u:\mathbb R^n\to\mathbb R$, let $x,v,g\in\mathbb R^n$, and let $B$ be a real $n\times n$ matrix, with the space represented by EuclideanSpace ℝ (Fin n). Assume that for every $\varepsilon>0$, the function $u$ satisfies near $x$

for almost every $y$ in some neighborhood of $x$, where quadraticAt is the quadratic test function used in the formalization. Then, as $t\to0$ through positive real values,

This auxiliary result extracts the quadratic coefficient from a viscosity-style second-order expansion and is reusable whenever such expansions are available.

Original Lean declaration header

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

private lemma expansion_secondDifference {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} {x g : EuclideanSpace ℝ (Fin n)}
    {B : Matrix (Fin n) (Fin n) ℝ}
    (h : ∀ ε > 0, ∀ᶠ y in 𝓝 x,
      |u y - quadraticAt B x g (u x) y| ≤ ε * ‖y - x‖ ^ 2)
    (v : EuclideanSpace ℝ (Fin n)) :
    Tendsto (fun t : ℝ =>
      (u (x + t • v) + u (x - t • v) - 2 * u x) / t ^ 2)
      (𝓝[>] 0) (𝓝 ⟪v, Matrix.toEuclideanLin B v⟫)

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/Convex/Alexandrov.

Previous: posDef_and_det_eq_of_quadratic_expansion · Next: convolution_hessian_integral.

Source excerpt, lines 992–1000 · Frozen source 408915f.