Cutoff Hessian Entry Difference-Quotient Bound

This formalizes a supporting component of Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $u,V,\chi:\mathbb R^n\to\mathbb R$. Assume $u,V\in C^1$ are convex, $\nabla u$ is Lipschitz, $-u+V\circ\nabla u$ is Lipschitz, and for some $K>0$ the almost-everywhere Hessian data satisfy $H_u\succ0$, $\log\det H_u=-u+V(\nabla u)$, and $KI-H_u\succeq0$. Assume also that $u(x+h)+u(x-h)-2u(x)\le D\|h\|^2$ for all $x,h$, and that $\chi\in C_c^1$. For every $i,j$ and $v$, there exists $C\ge0$ such that, whenever $t\ne0$ and $|t|\le1$,

This is a global $L^2$ difference-quotient estimate for cutoff Hessian entries.

Original Lean declaration header

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

theorem exists_hessian_cutoff_sq_difference_bound {n : ℕ}
    {u V χ : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) (hconv : ConvexOn ℝ univ u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V) (hVc : ConvexOn ℝ univ V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    {K : ℝ} (hK : 0 < K)
    (hdata : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).PosDef ∧
      Real.log (hessianMatrix u x).det = -u x + V (gradient u x) ∧
      (K • (1 : Matrix (Fin n) (Fin n) ℝ) - hessianMatrix u x).PosSemidef)
    {D : ℝ} (hw : ∀ x h, u (x + h) + u (x - h) - 2 * u x ≤ D * ‖h‖ ^ 2)
    (hχ : ContDiff ℝ 1 χ) (hχc : HasCompactSupport χ)
    (i j : Fin n) (v : EuclideanSpace ℝ (Fin n)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ t : ℝ, t ≠ 0 → |t| ≤ 1 →
      (∫ x, (χ (x + t • v) * hessianMatrix u (x + t • v) i j -
        χ x * hessianMatrix u x i j) ^ 2) ≤ C * t ^ 2

Module navigation

Module: Analysis/Convex/HessianIncrement.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Operator/Coordinates.

Supporting theorems: exists_smooth_compact_translate_majorant, integrable_hessian_increment_energy, integral_mul_hessian_increment_le, memLp_cutoff_mul_hessianMatrix_entry, norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Previous: integral_mul_hessian_increment_le.

Source excerpt, lines 267–282 · Frozen source 408915f.