Equality of Ambient and Intrinsic Covariance Norms

Proved

FunctionalInequalities.Covariance.opNorm_operator_intrinsic_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves equality of the operator norms of the ambient and intrinsic covariance operators.

Let $E$ be a complete, finite-dimensional, second-countable real inner-product space with its Borel measurable structure, and let $\mu$ be a probability measure on $E$ with finite second moment. If $V$ is the direction of the affine support of $\mu$ , then

\left\|\operatorname{Cov}(\operatorname{intrinsicMeasure}(\mu))\right\| = \left\|\operatorname{Cov}(\mu)\right\|.

The intrinsic operator acts on $V$ , while the ambient operator acts on $E$ .

This equality allows operator-norm estimates to be transferred between intrinsic and ambient formulations.

Original Lean declaration header

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

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

Module navigation

Module: Probability/Covariance/Intrinsic.

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

Supporting theorems: operator_coe_intrinsic.

Previous: operator_coe_intrinsic · Next: intrinsic_operator_inner_self_pos.

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

Source

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

View graph