Integrated Bochner Curvature Inequality

This formalizes the curvature inequality associated with Equation (16) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), used in Lemma 3.4.

Let $E$ be a finite-dimensional real inner-product Banach space, let $m$ be an additive Haar measure on $E$, and let $V,f:E\to\mathbb R$. Assume:

1. $V$ has temperate growth.
2. For every $r\in\mathbb R$, the function $x\mapsto e^{r\|x\|}$ is integrable with respect to the tilted measure $m.\operatorname{tilted}(-V)$.
3. $f$ has temperate growth.
4. There is $\rho\in\mathbb R$ such that, for every $x,v\in E$,

$$\rho\|v\|^2\le D^2V(x)[v,v].$$

Then, with hessianSqStdBasis denoting the squared Hilbert–Schmidt norm of the Hessian and weightedLaplacian the weighted Laplacian,

$$\int \operatorname{hessianSqStdBasis}(f)(x)\,d\mu(x)+\rho\int\|\nabla f(x)\|^2\,d\mu(x)\le \int\bigl(\operatorname{weightedLaplacian}(V,f)(x)\bigr)^2\,d\mu(x),$$

where $\mu=m.\operatorname{tilted}(-V)$.

This is an integrated Bochner-type estimate under a pointwise Hessian lower bound and is reusable in curvature and energy arguments for temperate functions.

Formalization Note. All integrals are real-valued integrals against the tilted measure; the statement is finite-dimensional and uses the exact temperate-growth and exponential-integrability hypotheses shown above.

Original Lean declaration header

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

theorem integral_hessianSq_add_le_of_hasTemperateGrowth {V f : E → ℝ} (hV : V.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (m.tilted (-V)))
    (hf : f.HasTemperateGrowth) {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ V x v v) :
    ∫ x, hessianSqStdBasis f x ∂(m.tilted (-V)) + ρ * ∫ x, ‖gradient f x‖ ^ 2 ∂(m.tilted (-V)) ≤
      ∫ x, weightedLaplacian V f x ^ 2 ∂(m.tilted (-V))

Module navigation

Module: Analysis/BakryEmery/Bochner/Temperate.

Definition modules: Analysis/BakryEmery/Bochner/Basic, Analysis/BakryEmery/Laplacian.

Supporting theorems: integrable_of_norm_le_pow, integral_weightedLaplacian_sq_eq_of_hasTemperateGrowth.

Previous: integral_weightedLaplacian_sq_eq_of_hasTemperateGrowth.

Source excerpt, lines 227–232 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Bochner_Temperate

open MeasureTheory Filter Topology
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
variable (m : MeasureTheory.Measure E) [m.IsAddHaarMeasure]

theorem FunctionalInequalities.Analysis.BakryEmery.integral_hessianSq_add_le_of_hasTemperateGrowth_readable {V f : E → ℝ} (hV : V.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (m.tilted (-V)))
    (hf : f.HasTemperateGrowth) {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ V x v v) :
    ∫ x, hessianSqStdBasis f x ∂(m.tilted (-V)) + ρ * ∫ x, ‖gradient f x‖ ^ 2 ∂(m.tilted (-V)) ≤
      ∫ x, weightedLaplacian V f x ^ 2 ∂(m.tilted (-V)) := by sorry