Compactly Cutoff Hessian Entries Are Global $L^2$

This formalizes a technical weak-Hessian integrability statement associated with Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $u,\chi:\mathbb R^n\to\mathbb R$, assume that $\nabla u$ is globally Lipschitz, and let $i,j\in\mathrm{Fin}\ n$. If $\chi$ is continuous and compactly supported, then the function $x\mapsto\chi(x)\,\operatorname{hessianMatrix}(u)(x)_{ij}$ belongs to $L^2$ with respect to Lebesgue volume:

This provides a global $L^2$ cutoff interface for a Hessian entry that is controlled locally by the Lipschitz gradient assumption.

Original Lean declaration header

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

theorem memLp_cutoff_mul_hessianMatrix_entry {n : ℕ}
    {u χ : EuclideanSpace ℝ (Fin n) → ℝ} {G : NNReal}
    (hG : LipschitzWith G (gradient u)) (i j : Fin n)
    (hχ : Continuous χ) (hχc : HasCompactSupport χ) :
    MemLp (fun x => χ x * hessianMatrix u x i j) 2
      (volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/BakryEmery/WeakHessian.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Previous: norm_hessianMatrix_entry_le_of_lipschitz_gradient · Next: chain_coordinate_of_differentiableAt_gradient.

Source excerpt, lines 451–456 · Frozen source 408915f.