Scaled Weak Inverse-Hessian Height Cutoffs

This is the weak $C^1$ cutoff construction associated with Lemma A.4 of Letwin (arXiv:2607.24164v1), and is used in the proof architecture surrounding Theorem 2.5.

Let $u,V:\mathbb R^n\to\mathbb R$ satisfy the stated $C^1$ regularity, Lipschitzness of $u$ and $\nabla u$, Lipschitzness of $-u+V\circ\nabla u$, the a.e. Monge–Ampère identity, and a.e. positive definiteness of $\nabla^2u$. Assume $u$ is convex and normalized by $\int e^{-u}=1$.

Then there exist $c,C\in\mathbb R$ with $C\ge0$ and $u(x)-c\ge1$ for every $x$ such that, writing

$$\chi_R(x)=\operatorname{smoothTransition}\left(2-\frac{u(x)-c}{R}\right),$$

and

$$L\chi_R=\operatorname{tr}\bigl((\nabla^2u)^{-1}\nabla^2\chi_R\bigr)-\nabla V(\nabla u)\cdot\nabla\chi_R,$$

for every $R\ge1$, $\chi_R$ is $C^1$, compactly supported, has a Lipschitz gradient, and satisfies $0\le\chi_R\le1$. For each $x$, $R\mapsto\chi_R(x)$ is monotone on $[1,\infty)$ and tends to $1$. Moreover, $L\chi_R$ is integrable with respect to the tilted measure $e^{-u}dx$, and

$$\int |L\chi_R|\,d(e^{-u}dx)\le\frac{C}{R}.$$

The same integral tends to $0$ as $R\to\infty$. This is an existence statement for a cutoff family, not an estimate for arbitrary cutoffs.

Original Lean declaration header

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

theorem exists_scaled_weak_inverse_hessian_cutoffs {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {L G LF : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u) (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V)
    (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (hPD : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), (hessianMatrix u x).PosDef)
    (hconv : ConvexOn ℝ univ u)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) = 1) :
    ∃ c C : ℝ, 0 ≤ C ∧ (∀ x, 1 ≤ u x - c) ∧
      let χ := fun R x => Real.smoothTransition (2 - (u x - c) / R)
      let Lχ := fun R x => ((hessianMatrix u x)⁻¹ * hessianMatrix (χ R) x).trace -
        fderiv ℝ V (gradient u x) (gradient (χ R) x)
      (∀ R : ℝ, 1 ≤ R → ContDiff ℝ 1 (χ R) ∧ HasCompactSupport (χ R) ∧
        (∃ K : NNReal, LipschitzWith K (gradient (χ R))) ∧
        ∀ x, 0 ≤ χ R x ∧ χ R x ≤ 1) ∧
      (∀ x, MonotoneOn (fun R => χ R x) (Ici 1)) ∧
      (∀ x, Tendsto (fun R => χ R x) atTop (𝓝 1)) ∧
      (∀ R : ℝ, 1 ≤ R → Integrable (Lχ R)
        ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) ∧
      (∀ R : ℝ, 1 ≤ R → (∫ x, |Lχ R x|
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) ≤ C / R) ∧
      Tendsto (fun R : ℝ => ∫ x, |Lχ R x|
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) atTop (𝓝 0)

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/InverseHessian/WeakCutoff.

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

Selected supporting theorems: deriv_comp_sub_div_and_deriv_deriv, exists_forall_le_and_isCompact_sublevel_of_convexOn_integrable_exp_neg, inv_mul_intervalIntegral_div_three_cutoff, monotoneOn_and_tendsto_smoothTransition_two_sub_div, smoothTransition_two_sub_cutoff.

Previous: exists_C1_height_generator_defect_bound · Next: integral_rough_mul_generator_eq_neg_energy_of_contDiff_one.

Source excerpt, lines 773–797 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_WeakCutoff

open MeasureTheory Filter Set Metric Matrix
open FunctionalInequalities.Probability.Stein
open scoped ContDiff Topology RealInnerProductSpace

theorem FunctionalInequalities.Analysis.exists_scaled_weak_inverse_hessian_cutoffs_readable {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {L G LF : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u) (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V)
    (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (hPD : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), (hessianMatrix u x).PosDef)
    (hconv : ConvexOn ℝ univ u)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) = 1) :
    ∃ c C : ℝ, 0 ≤ C ∧ (∀ x, 1 ≤ u x - c) ∧
      let χ := fun R x => Real.smoothTransition (2 - (u x - c) / R)
      let Lχ := fun R x => ((hessianMatrix u x)⁻¹ * hessianMatrix (χ R) x).trace -
        fderiv ℝ V (gradient u x) (gradient (χ R) x)
      (∀ R : ℝ, 1 ≤ R → ContDiff ℝ 1 (χ R) ∧ HasCompactSupport (χ R) ∧
        (∃ K : NNReal, LipschitzWith K (gradient (χ R))) ∧
        ∀ x, 0 ≤ χ R x ∧ χ R x ≤ 1) ∧
      (∀ x, MonotoneOn (fun R => χ R x) (Ici 1)) ∧
      (∀ x, Tendsto (fun R => χ R x) atTop (𝓝 1)) ∧
      (∀ R : ℝ, 1 ≤ R → Integrable (Lχ R)
        ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) ∧
      (∀ R : ℝ, 1 ≤ R → (∫ x, |Lχ R x|
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) ≤ C / R) ∧
      Tendsto (fun R : ℝ => ∫ x, |Lχ R x|
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u))) atTop (𝓝 0) := by sorry