Smooth Compact-Support Curvature Estimate

This is the curvature estimate on smooth compactly supported functions.

Let $V$, $\nu$, $m$, and $U$ satisfy the heat-model assumptions, with $\nu=m.\operatorname{tilted}(-U)$ and $U\in C^2$. Let $\rho\in\mathbb R$ and assume the Hessian lower bound

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

For every smooth compactly supported $f$, one has

$$\rho\,\|\overline{\nabla}[f]\|^2\le\|A[f]\|^2,$$

where $A=\overline{\nabla}^{\,\dagger}\overline{\nabla}$.

This is the smooth-core form of the curvature inequality and is intended for extension to the whole operator domain.

Formalization Note. The hypothesis does not require $\rho>0$; only the displayed pointwise Hessian inequality is assumed.

Original Lean declaration header

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

theorem mul_norm_closedWeightedOperator_toLp_sq_le {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v) {f : V → ℝ}
    (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    ρ * ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
        ⟨_, hν.toLp_mem_closedWeightedOperator_domain m hi hf hfc⟩‖ ^ 2 ≤
      ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)
        ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU.of_succ hf hfc⟩‖ ^ 2

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, KLS/LogConcave/HeatSemigroup/Generator, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Energy/WeightedGradient/Core.

Supporting theorems: mul_integral_gamma_le, norm_toLp_gradient_sq.

Previous: norm_toLp_gradient_sq · Next: mul_norm_closedWeightedOperator_sq_le.

Source excerpt, lines 78–84 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
include hνU hU

theorem FunctionalInequalities.KLS.LogConcave.mul_norm_closedWeightedOperator_toLp_sq_le_readable {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v) {f : V → ℝ}
    (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    ρ * ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
        ⟨_, hν.toLp_mem_closedWeightedOperator_domain m hi hf hfc⟩‖ ^ 2 ≤
      ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)
        ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU.of_succ hf hfc⟩‖ ^ 2 := by sorry