Ambient Covariance Operator on Intrinsic Directions

Proved

FunctionalInequalities.Covariance.operator_coe_intrinsic_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This states that the ambient covariance operator restricts to the intrinsic covariance operator 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 with finite second moment, let

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

and let $v\in V$ . Then, after coercing the intrinsic vector and intrinsic covariance output into $E$ ,

\operatorname{Cov}(\mu)(v) = \operatorname{Cov}(\operatorname{intrinsicMeasure}(\mu))(v).

This is the operator-level form of the ambient–intrinsic covariance correspondence and supports norm and positivity comparisons.

Original Lean declaration header

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

theorem operator_coe_intrinsic (μ : ProbabilityMeasure E) (hμ : MemLp id 2 (μ : Measure E))
    (v : (affineSupport μ).direction) :
    operator (μ : Measure E) v =
      (operator (intrinsicMeasure μ : Measure (affineSupport μ).direction) v : E)

Module navigation

Module: Probability/Covariance/Intrinsic.

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

Supporting theorems: bilin_intrinsic.

Previous: bilin_intrinsic · Next: opNorm_operator_intrinsic.

Source excerpt, lines 128–131 · 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.operator_coe_intrinsic_readable (μ : ProbabilityMeasure E) (hμ : MemLp id 2 (μ : Measure E))
    (v : (affineSupport μ).direction) :
    operator (μ : Measure E) v =
      (operator (intrinsicMeasure μ : Measure (affineSupport μ).direction) v : E) := by sorry

Source

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

View graph