Centering in the closed-gradient domain

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a full-dimensional log-concave law and the unit-weight closed gradient, center_mem_closedWeightedOperator_domain states that if $u$ belongs to the operator domain, then its centered class $u-\int u\,d\nu$ also belongs to that domain. The hypotheses include an explicit tilted representation $\nu=m.\operatorname{tilted}(-U)$ with $U\in C^2$ , although the displayed conclusion concerns only domain stability under subtraction of a constant.

Original module imports

import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Decay
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity
import FunctionalInequalities.KLS.LogConcave.WeightedGradient.Poincare
import FunctionalInequalities.Analysis.BakryEmery.Curvature
import FunctionalInequalities.Analysis.Semigroup.Generated.Curvature
import FunctionalInequalities.Analysis.Semigroup.Generated.Convergence
import FunctionalInequalities.KLS.LogConcave.WeightedGradient.Kernel
import FunctionalInequalities.KLS.LogConcave.Density.Tilted

Original declaration excerpt

Shown in the original module context. Body omitted.

theorem center_mem_closedWeightedOperator_domain
    (u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) :
    L2.center ν (u : Lp ℝ 2 (ν : Measure V)) ∈
      (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain

Module navigation

Direct project imports: KLS/LogConcave/HeatSemigroup/Decay, KLS/LogConcave/HeatSemigroup/InteriorRegularity, KLS/LogConcave/WeightedGradient/Poincare, Analysis/BakryEmery/Curvature, Analysis/Semigroup/Generated/Curvature, Analysis/Semigroup/Generated/Convergence, KLS/LogConcave/WeightedGradient/Kernel, KLS/LogConcave/Density/Tilted.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Curvature · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Decay
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Poincare
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Curvature
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Curvature
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Convergence
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Kernel
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_Tilted

noncomputable section
open MeasureTheory Filter Topology InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : ProbabilityMeasure V} (m : Measure V) [m.IsAddHaarMeasure] (hν : LogConcave ν)
  (hi : (interior (ν : Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
/-- Centering stays in the domain of the closed gradient: `center u ∈ D(T̄)` for `u ∈ D(T̄)`. -/
theorem center_mem_closedWeightedOperator_domain
    (u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) :
    L2.center ν (u : Lp ℝ 2 (ν : Measure V)) ∈
      (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain := by
  let T := hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
  have hconst :
      L2.const ν (L2.mean ν (u : Lp ℝ 2 (ν : Measure V))) ∈ T.domain := by
    have hone :
        L2.const ν 1 ∈ T.domain :=
      one_mem_domain_closedWeightedOperator m
        (ContinuousLinearMap.id ℝ V) hν hi
    have hsmul :
        L2.mean ν (u : Lp ℝ 2 (ν : Measure V)) • L2.const ν 1 ∈ T.domain :=
      T.domain.smul_mem
        (L2.mean ν (u : Lp ℝ 2 (ν : Measure V))) hone
    rw [← mul_one (L2.mean ν (u : Lp ℝ 2 (ν : Measure V))),
      L2.const_smul]
    exact hsmul
  have hsub :
      (u : Lp ℝ 2 (ν : Measure V)) -
          L2.const ν (L2.mean ν (u : Lp ℝ 2 (ν : Measure V))) ∈ T.domain :=
    T.domain.sub_mem u.2 hconst
  simpa [T, L2.center] using hsub
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Curvature.lean#L207-L230 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Curvature`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature`; the repository is private at upload time).

View graph