Height-Cutoff Generator Defect Bound

This is a quantitative cutoff estimate supporting the weak inverse-Hessian height cutoffs.

Let $u,V:\mathbb R^n\to\mathbb R$ satisfy the stated $C^1$ and Lipschitz assumptions, the Lipschitz Monge–Ampère exponent, the a.e. determinant identity, a.e. positive definiteness of $\nabla^2u$, and the normalization

$$\int e^{-u}=1.$$

Assume every sublevel set $\{x:u(x)\le t\}$ is compact. Let $D\ge0$ satisfy

$$\left|n-\nabla V(\nabla u(x))\cdot\nabla u(x)\right|\le D$$

for every $x$, and fix $c\in\mathbb R$.

Then there exists $C\ge0$ such that for every $R\ge1$, with

$$\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,$$

$L\chi_R$ multiplied by $e^{-u}$ is integrable and

$$\int |L\chi_R|e^{-u}\le \frac{C}{R}.$$

This estimate supplies the decay rate for the generator defect.

Original Lean declaration header

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

private theorem exists_C1_height_generator_defect_bound {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {G LF : NNReal}
    (hu : ContDiff ℝ 1 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)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) = 1)
    (hsub : ∀ t : ℝ, IsCompact {x | u x ≤ t})
    {D : ℝ} (hD : 0 ≤ D)
    (hdrift : ∀ x, |(n : ℝ) - fderiv ℝ V (gradient u x) (gradient u x)| ≤ D)
    (c : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ R : ℝ, 1 ≤ R →
      let χ := fun x => Real.smoothTransition (2 - (u x - c) / R)
      let Lχ := fun x => ((hessianMatrix u x)⁻¹ * hessianMatrix χ x).trace -
        fderiv ℝ V (gradient u x) (gradient χ x)
      Integrable (fun x => Lχ x * Real.exp (-u x))
        (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
      (∫ x, |Lχ x| * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) ≤ C / R

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_majorant_abs_deriv_deriv_smoothTransition_two_sub, inv_mul_intervalIntegral_div_three_cutoff, smoothTransition_two_sub_cutoff, ae_hessianMatrix_comp_profile.

Previous: ae_hessianMatrix_comp_profile · Next: exists_scaled_weak_inverse_hessian_cutoffs.

Source excerpt, lines 614–635 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_WeakCutoff

open MeasureTheory Filter Set Metric Matrix
open FunctionalInequalities.Probability.Stein

 theorem FunctionalInequalities.Analysis.exists_C1_height_generator_defect_bound_readable {n : ℕ}
    {u V : EuclideanSpace ℝ (Fin n) → ℝ} {G LF : NNReal}
    (hu : ContDiff ℝ 1 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)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) = 1)
    (hsub : ∀ t : ℝ, IsCompact {x | u x ≤ t})
    {D : ℝ} (hD : 0 ≤ D)
    (hdrift : ∀ x, |(n : ℝ) - fderiv ℝ V (gradient u x) (gradient u x)| ≤ D)
    (c : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ R : ℝ, 1 ≤ R →
      let χ := fun x => Real.smoothTransition (2 - (u x - c) / R)
      let Lχ := fun x => ((hessianMatrix u x)⁻¹ * hessianMatrix χ x).trace -
        fderiv ℝ V (gradient u x) (gradient χ x)
      Integrable (fun x => Lχ x * Real.exp (-u x))
        (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
      (∫ x, |Lχ x| * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) ≤ C / R := by sorry