Mean Partial Derivative Energy Drop

This formalizes the first energy-drop estimate associated with Lemma 3.9 of Bizeul–Klartag–Lehec.

Let $V$ be a finite-dimensional real inner-product space, let $\nu$ be a log-concave probability measure with nonempty support interior, and let $m$ be an additive Haar measure. Assume all exponential moments of $\nu$ are integrable. Assume also the covariance-type bound

$$\int \langle v,x\rangle^2\,d\nu(x)\le\|v\|^2\qquad(v\in V).$$

Let $u\in L^2(\nu)$ belong to the domain of the adjoint composition of the closed weighted gradient. Then

$$\sum_j\left(\operatorname{mean}_\nu(\partial_j u)\right)^2 \le \|\operatorname{gen}(u)\|^2,$$

where the sum is over an orthonormal basis, partialDeriv denotes the coordinate derivative of the closed gradient, and gen denotes the generator.

The estimate controls the squared mean gradient by the generator energy and is used as the initial energy inequality in the Poisson-iterate argument.

Formalization Note. The domain condition is an exact domain-membership hypothesis in $L^2(\nu)$; the displayed sum is a finite-dimensional coordinate sum.

Original Lean declaration header

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

theorem sum_mean_partialDeriv_sq_le
    (hcov : ∀ v : V, ∫ x, ⟪v, x⟫ ^ 2 ∂(ν : Measure V) ≤ ‖v‖ ^ 2)
    {u : Lp ℝ 2 (ν : Measure V)} (hu : u ∈ (adjointComp T̄).domain) :
    ∑ j, L2.mean ν (partialDeriv T̄ j u) ^ 2 ≤ ‖gen T̄ u‖ ^ 2

Module navigation

Module: KLS/BKL/PoissonIterate/Taylor.

Definition modules: KLS/BKL/PoissonIterate/Basic, L2/MeanVariance, KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave.

Supporting theorems: exists_toLp_mem_closedWeightedOperator_domain_of_hasTemperateGrowth.

Previous: meanGradSq_eq_norm_taylorField_one_genField.

Source excerpt, lines 356–359 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor

open MeasureTheory
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace ContDiff
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)
  (hexp : ∀ r : ℝ, MeasureTheory.Integrable (fun x => Real.exp (r * ‖x‖)) (ν : MeasureTheory.Measure V))
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
include hexp

theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.sum_mean_partialDeriv_sq_le_readable
    (hcov : ∀ v : V, ∫ x, ⟪v, x⟫ ^ 2 ∂(ν : Measure V) ≤ ‖v‖ ^ 2)
    {u : Lp ℝ 2 (ν : Measure V)} (hu : u ∈ (adjointComp T̄).domain) :
    ∑ j, L2.mean ν (partialDeriv T̄ j u) ^ 2 ≤ ‖gen T̄ u‖ ^ 2 := by sorry