Covariance Under Continuous Linear Equivalences

Proved

FunctionalInequalities.Covariance.operator_map_continuousLinearEquiv_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This describes covariance under a continuous linear equivalence.

Let $V_1$ and $V_2$ be real inner-product spaces with Borel measurable structures, assume the required completeness and second-countability conditions on $V_2$ , let $\nu$ be a finite measure on $V_1$ , and let

T:V_1\overset{\sim}{\longrightarrow}V_2

be a continuous linear equivalence. Then the covariance operator of the pushforward measure satisfies

\operatorname{Cov}(T_\#\nu) =T\circ\operatorname{Cov}(\nu)\circ T^*.

No finite-second-moment assumption is required: when the relevant second moment is absent, the covariance operators are zero by the underlying convention.

The result is the operator conjugation law used for linear changes of variables.

Original Lean declaration header

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

theorem Covariance.operator_map_continuousLinearEquiv
    (ν : Measure V₁) [IsFiniteMeasure ν] (T : V₁ ≃L[ℝ] V₂) :
    Covariance.operator (ν.map T) =
      ((T : V₁ →L[ℝ] V₂).comp (Covariance.operator ν)).comp (T : V₁ →L[ℝ] V₂).adjoint

Module navigation

Module: Probability/Transport.

Definition modules: Probability/Covariance/Basic.

Previous: Probability.tilted_smul_pos · Next: Probability.affineSupport_mapContinuousLinearEquiv.

Source excerpt, lines 296–299 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport

open MeasureTheory Filter Topology InnerProductSpace
universe u v
variable {V₁ : Type u} [NormedAddCommGroup V₁] [InnerProductSpace ℝ V₁]
  [MeasurableSpace V₁] [BorelSpace V₁]
variable {V₂ : Type v} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂]
  [MeasurableSpace V₂] [BorelSpace V₂]
variable [CompleteSpace V₁] [SecondCountableTopology V₁] [CompleteSpace V₂] [SecondCountableTopology V₂]
omit [SecondCountableTopology V₁]

Formal statement


theorem FunctionalInequalities.Covariance.operator_map_continuousLinearEquiv_readable
    (ν : Measure V₁) [IsFiniteMeasure ν] (T : V₁ ≃L[ℝ] V₂) :
    Covariance.operator (ν.map T) =
      ((T : V₁ →L[ℝ] V₂).comp (Covariance.operator ν)).comp (T : V₁ →L[ℝ] V₂).adjoint := by sorry

Source

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

View graph