Global Second-Difference Bound from Penalized Maxima

This formalizes the algebraic second-difference estimate used in the weak Letwin route.

Let $E$ be finite-dimensional, let $u,V:E\to\mathbb R$ be differentiable, and assume:

1. $u$ is convex and bounded below by $m$;
2. $\kappa>0$ and $V(y)-\frac\kappa2\|y\|^2$ is convex;
3. $|DV(\nabla u(x))[\nabla u(x)]|\leq C$ for every $x$;
4. for every $\eta>0$, there exists $x_0$ such that the penalized second difference $\Delta_h^2u(y)-\eta u(y)$ is maximized at $x_0$, and

Then for every $x,h\in E$,

The result is a reusable global estimate once penalized maximizers with the stated comparison are available.

Original Lean declaration header

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

theorem secondDifference_le_of_penalized_maxima {u V : E → ℝ} (hconv : ConvexOn ℝ univ u)
    (hu : Differentiable ℝ u) (hV : Differentiable ℝ V) {κ : ℝ} (hκ : 0 < κ)
    (hstrong : ConvexOn ℝ univ (fun y => V y - (κ / 2) * ‖y‖ ^ 2)) {C : ℝ}
    (hC : ∀ x, |fderiv ℝ V (gradient u x) (gradient u x)| ≤ C) {m : ℝ} (hm : ∀ x, m ≤ u x)
    (n : ℕ) (h : E)
    (hmax : ∀ η > 0, ∃ x₀ : E,
      (∀ y, u (y + h) + u (y - h) - 2 * u y - η * u y ≤
        u (x₀ + h) + u (x₀ - h) - 2 * u x₀ - η * u x₀) ∧
      (V (gradient u (x₀ + h)) - u (x₀ + h)) + (V (gradient u (x₀ - h)) - u (x₀ - h)) -
        2 * (V (gradient u x₀) - u x₀) ≤ η * n) :
    ∀ x, u (x + h) + u (x - h) - 2 * u x ≤ 4 * ‖h‖ ^ 2 / κ

Module navigation

Module: Analysis/Convex/SecondDifference.

Supporting theorems: sd_penalized_estimate.

Previous: sd_penalized_estimate · Next: centeredDifference_contDiff_lipschitz_gradient.

Source excerpt, lines 693–703 · Frozen source 408915f.