Isotropy Under a Linear Isometric Equivalence

This statement asserts that isotropy is preserved by a linear isometric equivalence.

Let $E$ and $F$ be finite-dimensional complete real inner product spaces equipped with their Borel measurable structures. Let $\nu$ be an isotropic probability measure on $E$, and let $\varphi:E\to F$ be a surjective linear isometry. Here isotropy (KLS.Isotropic) means finite second moment, zero mean, and identity centered covariance.

The pushforward probability measure is isotropic:

This permits isotropic laws to be transported between isometrically equivalent coordinate spaces.

Formalization Note The pushforward is ProbabilityMeasure.map, using the measurability supplied by continuity of $\varphi$. No positive-dimension assumption is required.

Original Lean declaration header

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

theorem Isotropic.map_linearIsometryEquiv {ν : ProbabilityMeasure E}
    (hν : Isotropic ν) (φ : E ≃ₗᵢ[ℝ] F) :
    Isotropic (ν.map φ.continuous.measurable.aemeasurable)

Module navigation

Module: KLS/Isotropic.

Next: integral_fderiv_mul_fderiv_eq_inner_of_isotropic_map.

Source excerpt, lines 86–88 · Frozen source 408915f.