Centered Functions Are Orthogonal To Gradient Kernel Elements

Proved

FunctionalInequalities.KLS.LogConcave.inner_center_eq_zero_of_closedWeightedOperator_eq_zero_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement identifies the orthogonality of centered data to the kernel of the closed weighted gradient.

Let $V$ , $\nu$ , $m$ , and $U$ satisfy the heat-model assumptions, with $U\in C^2$ . For any $u\in L^2(\nu)$ and any $k$ in the domain of the closed weighted operator, assume

\overline{\nabla}k=0.

Then

\left\langle\operatorname{center}_\nu u,k\right\rangle_{L^2(\nu)}=0.

The result is a technical orthogonality fact used to establish decay of centered heat evolution.

Formalization Note. The kernel characterization used by the declaration identifies such $k$ with a constant $L^2$ class; the conclusion is an equality in the real Hilbert-space inner product.

Original Lean declaration header

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

theorem inner_center_eq_zero_of_closedWeightedOperator_eq_zero (u : Lp ℝ 2 (ν : Measure V))
    (k : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain)
    (hk : hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi k = 0) :
    ⟪L2.center ν u, (k : Lp ℝ 2 (ν : Measure V))⟫ = 0

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

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

Supporting theorems: closedWeightedOperator_eq_zero_iff.

Previous: closedWeightedOperator_eq_zero_iff · Next: tendsto_norm_center_apply.

Source excerpt, lines 540–543 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open MeasureTheory Filter Topology InnerProductSpace
open scoped ContDiff RealInnerProductSpace
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

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.inner_center_eq_zero_of_closedWeightedOperator_eq_zero_readable (u : Lp ℝ 2 (ν : Measure V))
    (k : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain)
    (hk : hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi k = 0) :
    ⟪L2.center ν u, (k : Lp ℝ 2 (ν : Measure V))⟫ = 0 := by sorry

Source

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

View graph