Prove2Me

Centering Does Not Change Pairings With Mean-Zero Classes

Proved
FunctionalInequalities.KLS.LogConcave.inner_center_left_of_mean_zero_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem is a Hilbert-space identity for centered L2L^2 classes.

Let ν\nu be any probability measure on a measurable space, and let F,w∈L2(ν)F,w\in L^2(\nu) with

mean⁡ν(w)=0.\operatorname{mean}_\nu(w)=0.

Then

⟨F−const⁡ν(mean⁡νF),w⟩=⟨F,w⟩.\left\langle F-\operatorname{const}_\nu(\operatorname{mean}_\nu F),w\right\rangle =\langle F,w\rangle.

The left-hand side is L2.center ν F, and the constant class is L2.const. This elementary identity is useful when replacing a function by its centered version in variational estimates.

Original Lean declaration header

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

theorem inner_center_left_of_mean_zero
    (ν : ProbabilityMeasure α) (F w : Lp ℝ 2 (ν : Measure α))
    (hw : FunctionalInequalities.L2.mean ν w = 0) :
    ⟪FunctionalInequalities.L2.center ν F, w⟫ = ⟪F, w⟫

Module navigation

Module: KLS/LogConcave/BrascampLieb.

Definition modules: L2/MeanVariance.

Previous: norm_sq_le_of_mem_closure_quadratic_bound · Next: compact_pairing_identity.

Source excerpt, lines 77–80 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_BrascampLieb

open MeasureTheory Filter Topology Set InnerProductSpace
open scoped ContDiff RealInnerProductSpace
variable {α : Type*} [MeasurableSpace α]
Formal statement

theorem FunctionalInequalities.KLS.LogConcave.inner_center_left_of_mean_zero_readable
    (ν : ProbabilityMeasure α) (F w : Lp ℝ 2 (ν : Measure α))
    (hw : FunctionalInequalities.L2.mean ν w = 0) :
    ⟪FunctionalInequalities.L2.center ν F, w⟫ = ⟪F, w⟫ := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/BrascampLieb.lean#L75-L93 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.BrascampLieb`, declaration `FunctionalInequalities.KLS.LogConcave.inner_center_left_of_mean_zero`; the repository is private at upload time).

View graph