Curvature Estimate On The Full Operator Domain

This statement extends the curvature estimate to the full domain of the generator.

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$ satisfy

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

for every $x,v\in V$. Then every $F\in D(A)$ satisfies

$$\rho\,\|\overline{\nabla}F\|^2\le\|AF\|^2,$$

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

The result is the operator-domain version of the curvature bound and is reusable in semigroup energy estimates.

Formalization Note. The domain of $A$ is represented by the domain of adjointComp; the inequality is real-valued and no positivity assumption on $\rho$ is included.

Original Lean declaration header

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

theorem mul_norm_closedWeightedOperator_sq_le {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (F : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain) :
    ρ * ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨F, F.2.2⟩‖ ^ 2 ≤
      ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) F‖ ^ 2

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave.

Supporting theorems: exists_seq_smooth_tendsto_adjointComp_of_localRegularity, mul_norm_closedWeightedOperator_toLp_sq_le, toLp_mul_mem_closedWeightedOperator_domain_of_orthogonal.

Previous: mul_norm_closedWeightedOperator_toLp_sq_le · Next: closedWeightedOperator_center.

Source excerpt, lines 119–123 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
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_sq_le_readable {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (F : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain) :
    ρ * ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨F, F.2.2⟩‖ ^ 2 ≤
      ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) F‖ ^ 2 := by sorry