Prove2Me

Inner Product of Centered L2L^2 Functions

Proved
FunctionalInequalities.L2.inner_center_center_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the inner-product identity for centered functions on a probability space.

Let μ\mu be a probability measure on a measurable space and let f,g∈L2(μ)f,g\in L^2(\mu). With center defined by subtracting the respective means,

⟨f−∫f dμ, g−∫g dμ⟩L2(μ)=⟨f,g⟩L2(μ)−(∫f dμ)(∫g dμ).\left\langle f-\int f\,d\mu,\,g-\int g\,d\mu\right\rangle_{L^2(\mu)} =\langle f,g\rangle_{L^2(\mu)}-\left(\int f\,d\mu\right)\left(\int g\,d\mu\right).

This elementary identity is reusable for variance, orthogonality, and centered-gradient calculations.

Original Lean declaration header

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

theorem inner_center_center (μ : ProbabilityMeasure α)
    (f g : Lp ℝ 2 (μ : Measure α)) :
    inner ℝ (center μ f) (center μ g) =
      inner ℝ f g - mean μ f * mean μ g

Module navigation

Module: L2/MeanVariance.

Next: tendsto_variance_finite_linear_combination.

Source excerpt, lines 188–191 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_L2_MeanVariance

open MeasureTheory
variable {α : Type*} [MeasurableSpace α]
Formal statement

theorem FunctionalInequalities.L2.inner_center_center_readable (μ : ProbabilityMeasure α)
    (f g : Lp ℝ 2 (μ : Measure α)) :
    inner ℝ (center μ f) (center μ g) =
      inner ℝ f g - mean μ f * mean μ g := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/L2/MeanVariance.lean#L187-L203 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.L2.MeanVariance`, declaration `FunctionalInequalities.L2.inner_center_center`; the repository is private at upload time).

View graph