The nonsingular Wishart family

The nonsingular Wishart law TauCeti.Probability.nonsingularWishartMeasure n S is the law on the symmetric-matrix subspace whose density against TauCeti.symmetricLebesgue is (det A) ^ ((n - p - 1) / 2) * exp (-trace (S⁻¹ * A) / 2), normalized by 2 ^ (n p / 2) * (det S) ^ (n / 2) * Γ_p(n / 2) and supported on the positive-definite cone. Its degree n is a real parameter, restricted to p - 1 < n, which in positive dimension is the range where the density is integrable; its scale S is positive definite, since a singular positive-semidefinite scale concentrates the law on a proper subspace, where it has no density at all. Outside those two parameter conditions the definition sets the measure to zero.

The normalization is the one attached to TauCeti.symmetricLebesgue, whose coordinate unit cube has measure one; no other Haar normalization of the symmetric matrices produces the classical Wishart constants.

Dimension zero needs no separate definition: the symmetric space is then a single point, TauCeti.symmetricLebesgue 0 is a Dirac mass, and the empty determinants, trace and normalizing constant leave the density equal to 1, so for -1 < n the law is that Dirac mass.

Main definitions

• TauCeti.Probability.nonsingularWishartPDFReal and TauCeti.Probability.nonsingularWishartPDF — the Wishart density, real- and ℝ≥0∞-valued.
• TauCeti.Probability.nonsingularWishartMeasure — the nonsingular Wishart law.

Main results

• TauCeti.Probability.nonsingularWishartPDFReal_pos_iff — at a valid degree and scale the density is positive exactly on the positive-definite cone.
• TauCeti.Probability.nonsingularWishartMeasure_of_posDef — at a valid degree and scale the law is the density against TauCeti.symmetricLebesgue, while TauCeti.Probability.nonsingularWishartMeasure_of_not_posDef and TauCeti.Probability.nonsingularWishartMeasure_of_le describe the two invalid branches.
• TauCeti.Probability.ae_posDef_nonsingularWishartMeasure — the sampled matrix is positive definite almost everywhere, so by TauCeti.Probability.map_subtype_val_comap_nonsingularWishartMeasure the law is recovered from its lift to the cone.
• TauCeti.Probability.hasPDF_of_hasLaw_nonsingularWishartMeasure and TauCeti.Probability.rnDeriv_nonsingularWishartMeasure — a Wishart random matrix has a density against TauCeti.symmetricLebesgue, and at a valid degree and scale the law's Radon–Nikodym derivative is TauCeti.Probability.nonsingularWishartPDF.
• TauCeti.Probability.nonsingularWishartMeasure_zero — in dimension zero the law is the Dirac mass at the unique symmetric matrix, hence a probability measure.
• TauCeti.Probability.measurable_nonsingularWishartMeasure — the law is measurable jointly in its real degree and every coordinate of its scale matrix, and TauCeti.Probability.measurable_nonsingularWishartMeasure_selfAdjoint is the form with the scale ranging over the symmetric-matrix carrier.

References

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

The density

noncomputable def TauCeti.Probability.nonsingularWishartPDFReal {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ℝ

The nonsingular Wishart density of degree n and scale S, as a real-valued function of a symmetric matrix: on the positive-definite cone it is (det A) ^ ((n - p - 1) / 2) * exp (-trace (S⁻¹ * A) / 2) divided by the Wishart constant 2 ^ (n p / 2) * (det S) ^ (n / 2) * Γ_p(n / 2), and it vanishes off the cone.

theorem TauCeti.Probability.nonsingularWishartPDFReal_def {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : nonsingularWishartPDFReal n S A = if (↑A).PosDef then (↑A).det ^ ((n - ↑p - 1) / 2) * Real.exp (-(S⁻¹ * ↑A).trace / 2) / (2 ^ (n * ↑p / 2) * S.det ^ (n / 2) * multivariateGamma p (n / 2)) else 0

The defining branch expression of the real-valued Wishart density.

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDFReal_of_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : (↑A).PosDef) : nonsingularWishartPDFReal n S A = (↑A).det ^ ((n - ↑p - 1) / 2) * Real.exp (-(S⁻¹ * ↑A).trace / 2) / (2 ^ (n * ↑p / 2) * S.det ^ (n / 2) * multivariateGamma p (n / 2))

On the positive-definite cone the Wishart density is its defining formula.

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDFReal_of_not_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : ¬(↑A).PosDef) : nonsingularWishartPDFReal n S A = 0

Off the positive-definite cone the Wishart density vanishes.

theorem TauCeti.Probability.nonsingularWishartPDFReal_nonneg {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : 0 ≤ nonsingularWishartPDFReal n S A

At a valid degree and scale the Wishart density is nonnegative.

theorem TauCeti.Probability.nonsingularWishartPDFReal_pos_iff {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} : 0 < nonsingularWishartPDFReal n S A ↔ (↑A).PosDef

At a valid degree and scale the Wishart density is positive exactly on the positive-definite cone.

noncomputable def TauCeti.Probability.nonsingularWishartPDF {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ENNReal

The ℝ≥0∞-valued Wishart density, the one that defines the measure.

theorem TauCeti.Probability.nonsingularWishartPDF_def {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : nonsingularWishartPDF n S A = ENNReal.ofReal (nonsingularWishartPDFReal n S A)

The ℝ≥0∞-valued Wishart density is ENNReal.ofReal of the real-valued one.

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDF_of_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : (↑A).PosDef) : nonsingularWishartPDF n S A = ENNReal.ofReal ((↑A).det ^ ((n - ↑p - 1) / 2) * Real.exp (-(S⁻¹ * ↑A).trace / 2) / (2 ^ (n * ↑p / 2) * S.det ^ (n / 2) * multivariateGamma p (n / 2)))

On the positive-definite cone the ℝ≥0∞-valued Wishart density is its defining formula.

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDF_of_not_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : ¬(↑A).PosDef) : nonsingularWishartPDF n S A = 0

Off the positive-definite cone the ℝ≥0∞-valued Wishart density vanishes.

theorem TauCeti.Probability.nonsingularWishartPDF_pos_iff {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} : 0 < nonsingularWishartPDF n S A ↔ (↑A).PosDef

At a valid degree and scale the ℝ≥0∞-valued Wishart density is positive exactly on the positive-definite cone.

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDF_ne_top {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : nonsingularWishartPDF n S A ≠ ⊤

The Wishart density is finite.

theorem TauCeti.Probability.toReal_nonsingularWishartPDF {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (nonsingularWishartPDF n S A).toReal = nonsingularWishartPDFReal n S A

At a valid degree and scale the ℝ≥0∞-valued density carries the real one.

theorem TauCeti.Probability.measurable_nonsingularWishartPDFReal {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : Measurable (nonsingularWishartPDFReal n S)

The real-valued Wishart density is measurable in the point.

theorem TauCeti.Probability.measurable_uncurry_nonsingularWishartPDFReal (p : ℕ) : Measurable fun (q : (ℝ × Matrix (Fin p) (Fin p) ℝ) × ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => nonsingularWishartPDFReal q.1.1 q.1.2 q.2

The real-valued Wishart density is measurable jointly in its degree, its scale matrix and the point.

theorem TauCeti.Probability.measurable_nonsingularWishartPDF {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : Measurable (nonsingularWishartPDF n S)

The Wishart density is measurable in the point.

theorem TauCeti.Probability.measurable_uncurry_nonsingularWishartPDF (p : ℕ) : Measurable fun (q : (ℝ × Matrix (Fin p) (Fin p) ℝ) × ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => nonsingularWishartPDF q.1.1 q.1.2 q.2

The Wishart density is measurable jointly in its degree, its scale matrix and the point.

The measure

noncomputable def TauCeti.Probability.nonsingularWishartMeasure {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : MeasureTheory.Measure ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The nonsingular Wishart law of real degree n and positive-definite scale S: the density TauCeti.Probability.nonsingularWishartPDF against TauCeti.symmetricLebesgue. Outside the classical parameter range — a scale that is not positive definite, or a degree at most p - 1, which in positive dimension is where the density stops being integrable — the definition sets the measure to zero.

theorem TauCeti.Probability.nonsingularWishartMeasure_def {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : nonsingularWishartMeasure n S = if S.PosDef ∧ ↑p - 1 < n then (symmetricLebesgue p).withDensity (nonsingularWishartPDF n S) else 0

The defining branch expression of the Wishart law.

theorem TauCeti.Probability.nonsingularWishartMeasure_of_posDef {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) : nonsingularWishartMeasure n S = (symmetricLebesgue p).withDensity (nonsingularWishartPDF n S)

In the classical parameter range the Wishart law is its density against TauCeti.symmetricLebesgue.

@[simp]

theorem TauCeti.Probability.nonsingularWishartMeasure_of_not_posDef {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} (n : ℝ) (hS : ¬S.PosDef) : nonsingularWishartMeasure n S = 0

At a scale that is not positive definite there is no Wishart density to normalize, and the law is zero.

@[simp]

theorem TauCeti.Probability.nonsingularWishartMeasure_of_le {p : ℕ} {n : ℝ} (S : Matrix (Fin p) (Fin p) ℝ) (hn : n ≤ ↑p - 1) : nonsingularWishartMeasure n S = 0

At a degree at most p - 1 the Wishart law is zero by definition; in positive dimension this is the range where the density is not integrable.

@[simp]

theorem TauCeti.Probability.nonsingularWishartMeasure_compl_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : (nonsingularWishartMeasure n S) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}ᶜ = 0

The Wishart law gives no mass to the complement of the positive-definite cone.

theorem TauCeti.Probability.ae_posDef_nonsingularWishartMeasure {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : ∀ᵐ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) ∂nonsingularWishartMeasure n S, (↑A).PosDef

A matrix sampled from the Wishart law is almost surely positive definite.

@[simp]

theorem TauCeti.Probability.map_subtype_val_comap_nonsingularWishartMeasure {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val (nonsingularWishartMeasure n S)) = nonsingularWishartMeasure n S

The Wishart law read on the positive-definite cone. Mapping the lift (nonsingularWishartMeasure n S).comap Subtype.val back along the inclusion of the cone returns the law itself, because the cone carries all of its mass. This is the form in which the Cholesky equivalence, which is defined on the cone, acts on a Wishart matrix.

The density of a Wishart random matrix

theorem TauCeti.Probability.hasPDF_of_hasLaw_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hX : ProbabilityTheory.HasLaw X (nonsingularWishartMeasure n S) P) : MeasureTheory.HasPDF X P (symmetricLebesgue p)

A random symmetric matrix with a nonsingular Wishart law has a density against TauCeti.symmetricLebesgue, at every degree and scale: outside the classical parameter range the law is zero, which trivially has one.

theorem TauCeti.Probability.pdf_eq_nonsingularWishartPDF_of_hasLaw_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hS : S.PosDef) (hn : ↑p - 1 < n) (hX : ProbabilityTheory.HasLaw X (nonsingularWishartMeasure n S) P) : MeasureTheory.pdf X P (symmetricLebesgue p) =ᵐ[symmetricLebesgue p] nonsingularWishartPDF n S

The density against TauCeti.symmetricLebesgue of a random symmetric matrix with a nonsingular Wishart law is TauCeti.Probability.nonsingularWishartPDF.

theorem TauCeti.Probability.rnDeriv_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) : (nonsingularWishartMeasure n S).rnDeriv (symmetricLebesgue p) =ᵐ[symmetricLebesgue p] nonsingularWishartPDF n S

The Radon–Nikodym derivative of the nonsingular Wishart law against TauCeti.symmetricLebesgue is the Wishart density.

Dimension zero

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDFReal_zero (n : ℝ) (S : Matrix (Fin 0) (Fin 0) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ))) : nonsingularWishartPDFReal n S A = 1

In dimension zero the symmetric space is a single point and the real-valued Wishart density is 1 there.

@[simp]

theorem TauCeti.Probability.nonsingularWishartPDF_zero (n : ℝ) (S : Matrix (Fin 0) (Fin 0) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ))) : nonsingularWishartPDF n S A = 1

In dimension zero the symmetric space is a single point and the Wishart density is 1 there.

theorem TauCeti.Probability.nonsingularWishartMeasure_zero {n : ℝ} (hn : -1 < n) (S : Matrix (Fin 0) (Fin 0) ℝ) : nonsingularWishartMeasure n S = MeasureTheory.Measure.dirac 0

In dimension zero every valid Wishart law is the Dirac mass at the unique symmetric matrix. The general definition already gives this: TauCeti.symmetricLebesgue 0 is that Dirac mass and the density is identically 1.

Parameter measurability

theorem TauCeti.Probability.measurable_nonsingularWishartMeasure {p : ℕ} : Measurable fun (q : ℝ × (Fin p → Fin p → ℝ)) => nonsingularWishartMeasure q.1 (Matrix.of q.2)

Parameter measurability of the nonsingular Wishart law. The law is measurable jointly in its real degree and every coordinate of its scale matrix, which is what a Wishart kernel with a random degree and scale needs.

theorem TauCeti.Probability.measurable_nonsingularWishartMeasure_selfAdjoint {p : ℕ} : Measurable fun (q : ℝ × ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => nonsingularWishartMeasure q.1 ↑q.2

The nonsingular Wishart law is measurable jointly in its real degree and a scale ranging over the symmetric-matrix carrier. This is the form used to build a kernel with a random symmetric scale.