Centered covariance operator

Definition

KLSModular_FunctionalInequalities_Probability_Covariance_Basic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a complete real Hilbert space $E$ with the stated measurable and Borel structures, Covariance.operator μ is the continuous linear operator obtained by Riesz representation of Mathlib's centered covariance bilinear form for a measure $\mu$ . Its defining identity operator_inner is $\langle\operatorname{operator}(\mu)x,y\rangle=\operatorname{covarianceBilin}(\mu)(x,y)$ ; when the second moment is available, this is the centered covariance integral, while measures without the required integrability inherit Mathlib's totalized value.

Original module imports

import Mathlib.Probability.Moments.CovarianceBilin
import Mathlib.Analysis.InnerProductSpace.Dual

Original declaration excerpt

Shown in the original module context.

def operator (μ : Measure E) : E →L[ℝ] E :=
  InnerProductSpace.continuousLinearMapOfBilin (covarianceBilin μ)

Module navigation

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Covariance.Basic · Frozen source 408915f.

Definition code

import Mathlib.Probability.Moments.CovarianceBilin
import Mathlib.Analysis.InnerProductSpace.Dual

noncomputable section
open MeasureTheory ProbabilityTheory
namespace FunctionalInequalities
namespace Covariance
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [MeasurableSpace E] [BorelSpace E]
/-- The centered covariance operator, obtained by Riesz representation of
`ProbabilityTheory.covarianceBilin μ` using `InnerProductSpace.continuousLinearMapOfBilin`.

For a probability measure with `MemLp id 2 μ`, write `m = ∫ x, x ∂μ`. Then
`⟪operator μ u, v⟫ = ∫ x, ⟪u, x - m⟫ * ⟪v, x - m⟫ ∂μ`.
The definition accepts every measure; if `¬ MemLp id 2 μ`, it inherits Mathlib's zero value.

In the pinned Mathlib version, `ProbabilityTheory.covarianceOperator μ` uses the uncentered
second moment. This definition is definitionally equal to
`ProbabilityTheory.covarianceOperator (μ.map (fun x => x - ∫ y, y ∂μ))`. -/
def operator (μ : Measure E) : E →L[ℝ] E :=
  InnerProductSpace.continuousLinearMapOfBilin (covarianceBilin μ)
/-- The defining Riesz identity, from `InnerProductSpace.continuousLinearMapOfBilin_apply`.
For a finite measure with `MemLp id 2 μ`, combine it with
`ProbabilityTheory.covarianceBilin_apply` to obtain the centered integral formula. -/
@[simp]
theorem operator_inner (μ : Measure E) (x y : E) :
    inner ℝ (operator μ x) y = covarianceBilin μ x y := by
  exact InnerProductSpace.continuousLinearMapOfBilin_apply (covarianceBilin μ) x y
end Covariance
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Covariance/Basic.lean#L21-L40 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Covariance.Basic`, definition bundle `KLSModular_FunctionalInequalities_Probability_Covariance_Basic`; the repository is private at upload time).

View graph