Positive Definiteness of Intrinsic Covariance

Proved

FunctionalInequalities.Covariance.intrinsic_operator_inner_self_pos_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves positive definiteness of the intrinsic covariance operator on the affine-support direction space.

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

V=\operatorname{direction}(\operatorname{affineSupport}(\mu)).

For every nonzero $v\in V$ ,

0<\left\langle \operatorname{Cov}(\operatorname{intrinsicMeasure}(\mu))v,v \right\rangle.

The theorem supplies strict positivity after restricting the law to its intrinsic affine support, even when the ambient covariance may have null directions.

Formalization Note The finite second moment is expressed by MemLp id 2; no positive-dimensionality assumption is made.

Original Lean declaration header

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

theorem intrinsic_operator_inner_self_pos (μ : ProbabilityMeasure E)
    (hμ : MemLp id 2 (μ : Measure E)) {v : (affineSupport μ).direction} (hv : v ≠ 0) :
    0 < inner ℝ (operator (intrinsicMeasure μ : Measure (affineSupport μ).direction) v) v

Module navigation

Module: Probability/Covariance/Intrinsic.

Definition modules: Probability/Covariance/Basic, Probability/AffineSupport.

Supporting theorems: affineSupport_intrinsicMeasure.

Previous: opNorm_operator_intrinsic.

Source excerpt, lines 183–185 · 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
omit [CompleteSpace E]

Formal statement


theorem FunctionalInequalities.Covariance.intrinsic_operator_inner_self_pos_readable (μ : ProbabilityMeasure E)
    (hμ : MemLp id 2 (μ : Measure E)) {v : (affineSupport μ).direction} (hv : v ≠ 0) :
    0 < inner ℝ (operator (intrinsicMeasure μ : Measure (affineSupport μ).direction) v) v := by sorry

Source

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

View graph