Centering Leaves The Closed Gradient Unchanged

Proved

FunctionalInequalities.KLS.LogConcave.closedWeightedOperator_center_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement identifies the action of the closed weighted gradient on a centered function.

Let $V$ be a finite-dimensional real inner-product space, let $\nu$ be log-concave with nonempty support interior, and let $m$ be an additive Haar measure. For any element $u$ of the domain of the closed weighted operator, let $\operatorname{center}_\nu u=u-\operatorname{mean}_\nu(u)$ denote its $L^2$ centering. Then

\overline{\nabla}(\operatorname{center}_\nu u)=\overline{\nabla}u.

The result records that constants are annihilated by the closed gradient and allows centered representatives to be substituted without changing their gradient energy.

Formalization Note. The centered element is accompanied by a separately constructed domain proof; equality is equality of the resulting $L^2(\nu)$ classes.

Original Lean declaration header

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

theorem closedWeightedOperator_center
    (u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) :
    hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
        ⟨L2.center ν (u : Lp ℝ 2 (ν : Measure V)),
          center_mem_closedWeightedOperator_domain m hν hi u⟩ =
      hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi u

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave, L2/MeanVariance.

Supporting theorems: closedWeightedOperator_one_eq_zero.

Previous: mul_norm_closedWeightedOperator_sq_le · Next: norm_center_sq_sub_le.

Source excerpt, lines 233–238 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open MeasureTheory Filter Topology InnerProductSpace
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)

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.closedWeightedOperator_center_readable
    (u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) :
    hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
        ⟨L2.center ν (u : Lp ℝ 2 (ν : Measure V)),
          center_mem_closedWeightedOperator_domain m hν hi u⟩ =
      hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi u := by sorry

Source

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

View graph