Lebesgue measure on the symmetric subspace

TauCeti.symmetricLebesgue p is the pushforward of product Lebesgue measure on the upper-triangular coordinates along (TauCeti.symmetricCoordinates p).symm. This is the normalization used by the Wishart densities and the multivariate-Gamma integral: the coordinate unit cube has measure one.

The Frobenius volume of measureSpaceOfInnerProductSpace is a Haar measure for the same topology, but a different normalization: the off-diagonal coordinate directions Eᵢⱼ + Eⱼᵢ have Frobenius norm √2, so Frobenius volume is 2 ^ (p * (p - 1) / 4) times symmetricLebesgue p, with a real exponent.

Main declarations

• TauCeti.symmetricLebesgue — Lebesgue measure on the symmetric subspace, normalized by the upper-triangular coordinates.
• TauCeti.measurePreserving_symmetricCoordinates_symm — the coordinate reconstruction is measure preserving.
• TauCeti.symmetricLebesgueIsAddHaarMeasure — symmetricLebesgue p is an additive Haar measure, as required by Mathlib's Jacobian API.
• TauCeti.volume_symmetricMatrix_eq_smul_symmetricLebesgue — comparison with the Frobenius volume.
• TauCeti.symmetricLebesgue_zero — in dimension zero, symmetricLebesgue is the Dirac measure on the unique symmetric matrix.
• TauCeti.measurePreserving_symmetricFinOneEquiv — in dimension one, reading the single entry carries symmetricLebesgue to Lebesgue measure on ℝ.

noncomputable def TauCeti.symmetricLebesgue (p : ℕ) : MeasureTheory.Measure ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

Lebesgue measure on the symmetric subspace: the pushforward of product Lebesgue measure on the upper-triangular coordinates along the coordinate reconstruction. The coordinate unit cube has measure one; this is the normalization used by the Wishart densities.

Equations

• TauCeti.symmetricLebesgue p = MeasureTheory.Measure.map (⇑(TauCeti.symmetricCoordinates p).symm) MeasureTheory.volume

theorem TauCeti.measurePreserving_symmetricCoordinates_symm (p : ℕ) : MeasureTheory.MeasurePreserving (⇑(symmetricCoordinates p).symm) MeasureTheory.volume (symmetricLebesgue p)

The coordinate reconstruction maps product Lebesgue measure to symmetricLebesgue.

theorem TauCeti.measurePreserving_symmetricCoordinates (p : ℕ) : MeasureTheory.MeasurePreserving (⇑(symmetricCoordinates p)) (symmetricLebesgue p) MeasureTheory.volume

The upper-triangular coordinates map symmetricLebesgue to product Lebesgue measure.

instance TauCeti.symmetricLebesgueIsAddHaarMeasure (p : ℕ) : (symmetricLebesgue p).IsAddHaarMeasure

symmetricLebesgue is an additive Haar measure, as required by Mathlib's Jacobian API.

Comparison with the Frobenius volume

The comparison goes through the coordinate basis TauCeti.symmetricBasis p, whose vectors are the symmetric matrices Eᵢⱼ + Eⱼᵢ and Eᵢᵢ. Rescaling the off-diagonal ones by (√2)⁻¹ makes the basis orthonormal for the Frobenius inner product, and the determinant of that rescaling is the ratio of the two normalizations.

theorem TauCeti.volume_symmetricMatrix_eq_smul_symmetricLebesgue (p : ℕ) : MeasureTheory.volume = ENNReal.ofReal (Real.rpow 2 (↑p * (↑p - 1) / 4)) • symmetricLebesgue p

The Frobenius volume of the symmetric subspace is 2 ^ (p * (p - 1) / 4) times symmetricLebesgue, with a real exponent: each of the p * (p - 1) / 2 off-diagonal coordinate directions Eᵢⱼ + Eⱼᵢ has Frobenius norm √2.

theorem TauCeti.symmetricLebesgue_zero : symmetricLebesgue 0 = MeasureTheory.Measure.dirac 0

In dimension zero, the symmetric subspace is a single point and symmetricLebesgue is the Dirac measure there, so the dimension-zero Wishart laws need no special casing.

theorem TauCeti.measurePreserving_symmetricFinOneEquiv : MeasureTheory.MeasurePreserving (⇑symmetricFinOneEquiv) (symmetricLebesgue 1) MeasureTheory.volume

In dimension one, reading the single entry of a symmetric matrix carries symmetricLebesgue to Lebesgue measure on ℝ, so the one-dimensional Wishart densities are ordinary densities on the real line.