Centered Generator-Domain Bounds

This formalizes the operator-domain part of Lemma 2.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 7, for bounds (20) and (24).

Let $V$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $m$ be an additive Haar measure on $V$, and let $\nu$ be a log-concave probability measure with nonempty interior support. Suppose that $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ for some $U:V\to\mathbb R$ of class $C^2$. Let $C\in[0,\infty)$ satisfy $C_P(\nu)\le C$, where the inequality is in $[0,\infty]$. If $u$ belongs to the domain of the adjoint composition of the closed weighted operator, and $u$ is centered, then:

$$\|u\|\le C\,\|\bar T^\dagger\bar T u\|,$$ $$\|\bar T u\|^2=\langle \bar T^\dagger\bar T u,u\rangle\le C\,\|\bar T^\dagger\bar T u\|^2,$$

and

$$\|\bar T u\|\le \sqrt C\,\|\bar T^\dagger\bar T u\|.$$

Here the norms and inner product are those of the relevant $L^2(\nu)$ spaces, and the first displayed domain element is interpreted through its underlying $L^2$ class.

This is a technical inverse-operator estimate used to control centered Poisson iterates and their gradient fields.

Formalization Note: The Poincaré constant is an ENNReal value, while $C$ is an NNReal whose coercions appear in the inequalities; the operator is closedWeightedOperator and its adjoint composition is adjointComp. The statement is restricted to finite-dimensional $V$.

Original Lean declaration header

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

theorem centered_adjointComp_bounds {C : NNReal}
    (hC : Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
    (u : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain)
    (hu : L2.mean ν (u : Lp ℝ 2 (ν : Measure V)) = 0) :
    ‖(u : Lp ℝ 2 (ν : Measure V))‖ ≤
        (C : ℝ) * ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u‖ ∧
      ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨(u : Lp ℝ 2 (ν : Measure V)), u.2.2⟩‖ ^ 2 =
        ⟪adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u,
          (u : Lp ℝ 2 (ν : Measure V))⟫ ∧
      ⟪adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u,
          (u : Lp ℝ 2 (ν : Measure V))⟫ ≤
        (C : ℝ) * ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u‖ ^ 2 ∧
      ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨(u : Lp ℝ 2 (ν : Measure V)), u.2.2⟩‖ ≤
        Real.sqrt C * ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u‖

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Inverse.

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

Supporting theorems: norm_le_of_gap, closedWeightedOperator_id_gap_of_literature_le, orthogonal_ker_iff_mean_eq_zero.

Previous: existsUnique_centered_adjointComp_eq.

Source excerpt, lines 166–179 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Inverse

open scoped InnerProductSpace RealInnerProductSpace
open MeasureTheory
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.Semigroup.Generated
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.centered_adjointComp_bounds_readable {C : NNReal}
    (hC : Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
    (u : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain)
    (hu : L2.mean ν (u : Lp ℝ 2 (ν : Measure V)) = 0) :
    ‖(u : Lp ℝ 2 (ν : Measure V))‖ ≤
        (C : ℝ) * ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u‖ ∧
      ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨(u : Lp ℝ 2 (ν : Measure V)), u.2.2⟩‖ ^ 2 =
        ⟪adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u,
          (u : Lp ℝ 2 (ν : Measure V))⟫ ∧
      ⟪adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u,
          (u : Lp ℝ 2 (ν : Measure V))⟫ ≤
        (C : ℝ) * ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u‖ ^ 2 ∧
      ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨(u : Lp ℝ 2 (ν : Measure V)), u.2.2⟩‖ ≤
        Real.sqrt C * ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) u‖ := by sorry