Penalized Maximum Second-Difference Estimate

This is a technical estimate at a penalized maximum of a convex function's second difference.

Let $E$ be finite-dimensional, let $u,V:E\to\mathbb R$ be differentiable, let $u$ be convex, and let $\kappa>0$. Assume that $V(y)-\frac\kappa2\|y\|^2$ is convex. Suppose there is $C\in\mathbb R$ such that

for every $x$. For $\eta>0$, $x_0,h\in E$, assume that the penalized second difference at $x_0$ dominates that at every $y$, and that the corresponding comparison for $V\circ\nabla u-u$ is at most $\eta n$. Then

where $\Delta_h^2u(x)=u(x+h)+u(x-h)-2u(x)$. This auxiliary estimate is the algebraic maximum-principle step before letting $\eta\downarrow0$.

Original Lean declaration header

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

set_option maxHeartbeats 800000 in
private lemma sd_penalized_estimate {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)
    (n : ℕ) (h x₀ : E) {η : ℝ} (hη : 0 < η)
    (hmaximum : ∀ y, u (y + h) + u (y - h) - 2 * u y - η * u y ≤
      u (x₀ + h) + u (x₀ - h) - 2 * u x₀ - η * u x₀)
    (hcomparison :
      (V (gradient u (x₀ + h)) - u (x₀ + h)) +
        (V (gradient u (x₀ - h)) - u (x₀ - h)) -
        2 * (V (gradient u x₀) - u x₀) ≤ η * n) :
    u (x₀ + h) + u (x₀ - h) - 2 * u x₀ ≤
      4 * ‖h‖ ^ 2 / κ + 2 * ‖h‖ * Real.sqrt (η * (n + C) / κ)

Module navigation

Module: Analysis/Convex/SecondDifference.

Previous: lipschitzWith_gradient_of_second_difference_le · Next: secondDifference_le_of_penalized_maxima.

Source excerpt, lines 586–600 · Frozen source 408915f.