The scale of the nonsingular Wishart law

Congruence A ↦ C * A * Cᵀ by an invertible matrix carries the nonsingular Wishart law of scale S to the one of scale C * S * Cᵀ, because the density and the congruence Jacobian cancel exactly. Substituting C⁻¹ B C⁻ᵀ for the argument multiplies the determinant factor (det A) ^ ((n - p - 1) / 2) of the density by |det C| ^ (p + 1 - n), and reading the density at the scale S rather than at C * S * Cᵀ multiplies it by a further |det C| ^ n, since the scale enters the normalizing constant through (det S) ^ (n / 2). Their product |det C| ^ (p + 1) is exactly the factor by which congruence rescales TauCeti.symmetricLebesgue.

This makes the scale parameter inessential where the law is not the zero measure: a nonsingular Wishart law of positive-definite scale is a congruence image of the standard one, whose scale is the identity matrix, so any property preserved by congruence pushforward transfers from the standard scale to every positive-definite one. The total mass is such a property. At the scale 2⁻¹ • 1 the exponential weight of the density is exp (-trace A) and the normalizing constant collapses to Γ_p (n / 2), so the mass is the multivariate Gamma integral TauCeti.lintegral_posDef_multivariateGamma divided by that constant, namely 1, and congruence spreads this to every positive-definite scale.

Main results

• TauCeti.Probability.map_symmetricCongruence_nonsingularWishartMeasure — congruence by an invertible matrix carries the law of scale S to the law of scale C * S * Cᵀ;
• TauCeti.Probability.map_symmetricCongruenceLinearMap_nonsingularWishartMeasure_of_det_ne_zero — the same statement for the unbundled congruence map of a matrix of nonzero determinant;
• TauCeti.Probability.nonsingularWishartMeasure_eq_map_sqrt — a nonsingular Wishart law of positive-definite scale is the standard one transported by the congruence with the square root of that scale;
• TauCeti.Probability.isProbabilityMeasure_nonsingularWishartMeasure — the law is a probability measure at exactly the parameters where a density defines it.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, chapters 2 and 3.
• M. L. Eaton, Multivariate Statistics: A Vector Space Approach, IMS Lecture Notes 53, chapter 8.

Congruence

theorem TauCeti.Probability.map_symmetricCongruence_nonsingularWishartMeasure {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (C : GL (Fin p) ℝ) : MeasureTheory.Measure.map (⇑C.symmetricCongruence) (nonsingularWishartMeasure n S) = nonsingularWishartMeasure n (↑C * S * (↑C).transpose)

Congruence carries the nonsingular Wishart law of scale S to the one of scale C * S * Cᵀ. No hypothesis is needed: congruence by an invertible matrix preserves positive definiteness, so the two sides are zero together outside the classical parameter range.

theorem TauCeti.Probability.map_symmetricCongruenceLinearMap_nonsingularWishartMeasure_of_det_ne_zero {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {C : Matrix (Fin p) (Fin p) ℝ} (hC : C.det ≠ 0) : MeasureTheory.Measure.map (⇑C.symmetricCongruenceLinearMap) (nonsingularWishartMeasure n S) = nonsingularWishartMeasure n (C * S * C.transpose)

Congruence by a matrix of nonzero determinant carries the nonsingular Wishart law of scale S to the one of scale C * S * Cᵀ. This is TauCeti.Probability.map_symmetricCongruence_nonsingularWishartMeasure for the unbundled congruence map Matrix.symmetricCongruenceLinearMap, which is the form that composes with the congruences by rectangular matrices.

The standard scale

Reduction to a scalar scale

theorem TauCeti.Probability.nonsingularWishartMeasure_eq_map_sqrt {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} (n : ℝ) (hS : S.PosDef) : nonsingularWishartMeasure n S = MeasureTheory.Measure.map (⇑(CFC.sqrt S).symmetricCongruenceLinearMap) (nonsingularWishartMeasure n 1)

A nonsingular Wishart law of positive-definite scale is the standard one transported by a congruence. The congruence with the square root of the scale carries the law of scale 1 to the law of scale S. This is the density-family analogue of TauCeti.Probability.wishartGramMeasure_eq_map_sqrt.

theorem TauCeti.Probability.isProbabilityMeasure_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) : MeasureTheory.IsProbabilityMeasure (nonsingularWishartMeasure n S)

The nonsingular Wishart law is a probability measure at exactly the parameters where a density defines it: a positive-definite scale and a degree above p - 1.