Ambient and Intrinsic Covariance Bilinear Forms

Proved

FunctionalInequalities.Covariance.bilin_intrinsic_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This identifies the ambient covariance bilinear form with the intrinsic covariance bilinear form on the affine-support direction space.

Let $E$ be a complete, finite-dimensional, second-countable real inner-product space with its Borel measurable structure. Let $\mu$ be a probability measure on $E$ satisfying

\operatorname{id}\in L^2(\mu).

Let $V$ be the direction of the affine support of $\mu$ , and let $v,w\in V$ . Then

\operatorname{Cov}(\operatorname{intrinsicMeasure}(\mu))(v,w) = \operatorname{Cov}(\mu)(v,w),

where the right-hand side views $v,w$ as vectors in $E$ .

This is the basic covariance identity for intrinsic coordinates and is reusable in comparisons between ambient and affine-support formulations.

Formalization Note The intrinsic law is intrinsicMeasure μ, and the second-moment assumption is the explicit MemLp id 2 hypothesis.

Original Lean declaration header

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

theorem bilin_intrinsic (μ : ProbabilityMeasure E) (hμ : MemLp id 2 (μ : Measure E))
    (v w : (affineSupport μ).direction) :
    covarianceBilin (intrinsicMeasure μ : Measure (affineSupport μ).direction) v w =
      covarianceBilin (μ : Measure E) v w

Module navigation

Module: Probability/Covariance/Intrinsic.

Definition modules: Probability/AffineSupport.

Next: operator_coe_intrinsic.

Source excerpt, lines 106–109 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Intrinsic

open MeasureTheory ProbabilityTheory
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
variable [MeasurableSpace E] [BorelSpace E]
variable [SecondCountableTopology E] [FiniteDimensional ℝ E]
open FunctionalInequalities.Probability

Formal statement


theorem FunctionalInequalities.Covariance.bilin_intrinsic_readable (μ : ProbabilityMeasure E) (hμ : MemLp id 2 (μ : Measure E))
    (v w : (affineSupport μ).direction) :
    covarianceBilin (intrinsicMeasure μ : Measure (affineSupport μ).direction) v w =
      covarianceBilin (μ : Measure E) v w := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Covariance/Intrinsic.lean#L104-L124 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Covariance.Intrinsic`, declaration `FunctionalInequalities.Covariance.bilin_intrinsic`; the repository is private at upload time).

View graph