Covariance Relaxation Under Linear Equivalence

This proves covariance-relaxation invariance under a continuous linear equivalence.

Let $V_1,V_2$ be complete real inner-product spaces with Borel measurable structures, let $\nu$ be a probability measure on $V_1$, let

be a continuous linear equivalence, and let $f\in L^2(T_\#\nu)$. Then

where $T^*f$ denotes the pullback of $f$ through the induced $L^2$ equivalence, represented in Lean by L2.ContinuousLinearEquiv.pullbackEquiv ν T.

The statement expresses covariance-energy invariance under arbitrary invertible linear coordinate changes.

Formalization Note Finite-dimensionality and second-countability of the source are not required by the declaration; the target has the stated second-countability assumption.

Original Lean declaration header

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

theorem relaxation_mapContinuousLinearEquiv (f : Lp ℝ 2 (Probability.mapContinuousLinearEquiv ν T : Measure V₂)) :
    relaxation (Probability.mapContinuousLinearEquiv ν T) f = relaxation ν (L2.ContinuousLinearEquiv.pullbackEquiv ν T f)

Module navigation

Module: Energy/CovarianceGradient/LinearEquiv.

Definition modules: L2/Transport, Energy/Form/Functional, Probability/Transport, Energy/CovarianceGradient/Basic.

Supporting theorems: Covariance.operator_map_continuousLinearEquiv.

Source excerpt, lines 151–152 · Frozen source 408915f.