Orthogonality to the Closed-Gradient Kernel Equivalent to Zero Mean

Proved

FunctionalInequalities.KLS.LogConcave.orthogonal_ker_iff_mean_eq_zero_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement identifies the orthogonal complement of the closed unit-gradient kernel with the mean-zero subspace of $L^2$ .

Let $V$ be a finite-dimensional complete real inner product space with its Borel measurable structure and a second-countable topology. Assume:

$m$ is an additive Haar measure.
$\nu$ is a log-concave probability measure with nonempty interior of its support.
$U:V\to\mathbb R$ is $C^2$ and $\nu=m.\operatorname{tilted}(-U)$ (Measure.tilted).

Let $T=$ KLS.LogConcave.closedWeightedOperator for $m$ and the identity weight. For every $y\in L^2(\nu)$ ,

\left(\forall k\in D(T),\ Tk=0\ \Longrightarrow\ \langle y,k\rangle_{L^2(\nu)}=0\right) \quad\Longleftrightarrow\quad \operatorname{mean}_\nu(y)=0.

Here the mean is L2.mean. This connects the abstract kernel-orthogonality condition to centering in inverse and generator statements.

Formalization Note The vector $y$ is arbitrary in $L^2(\nu)$ ; it is not required to lie in the form domain $D(T)$ . No Poincaré or positive-curvature assumption is present.

Original Lean declaration header

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

theorem orthogonal_ker_iff_mean_eq_zero
    (y : Lp ℝ 2 (ν : Measure V)) :
    (∀ k : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
        hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi k = 0 →
          ⟪y, (k : Lp ℝ 2 (ν : Measure V))⟫ = 0) ↔ L2.mean ν y = 0

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Inverse.

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

Supporting theorems: closedWeightedOperator_eq_zero_iff, closedWeightedOperator_one_eq_zero.

Next: existsUnique_centered_adjointComp_eq.

Source excerpt, lines 40–44 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Inverse

open scoped InnerProductSpace RealInnerProductSpace
open MeasureTheory
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.orthogonal_ker_iff_mean_eq_zero_readable
    (y : Lp ℝ 2 (ν : Measure V)) :
    (∀ k : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
        hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi k = 0 →
          ⟪y, (k : Lp ℝ 2 (ν : Measure V))⟫ = 0) ↔ L2.mean ν y = 0 := by sorry

Source

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

View graph