The inverse-Wishart density and measure

The inverse-Wishart law TauCeti.Probability.inverseWishartMeasure n S is the image of the Wishart law of the inverted scale, TauCeti.Probability.nonsingularWishartMeasure n S⁻¹, under matrix inversion. Inversion is totalized to zero on singular matrices, which is harmless: the source law lives on the positive-definite cone, where inversion is a bijection.

Reading the density off the source law is the change of variables TauCeti.map_symmetricInv_symmetricLebesgue, whose Jacobian weight (det B) ^ (-(p + 1)) combines with the Wishart exponent (n - p - 1) / 2 at the inverted determinant to give the exponent -((n + p + 1) / 2), while the scale determinant moves from the denominator of the Wishart constant to the numerator.

Since the source law is zero outside the classical parameter range — a scale that is not positive definite, or a degree at most p - 1 — so is the inverse-Wishart law, and positive definiteness of S and of S⁻¹ are equivalent, so the two families are invalid on exactly the same parameters.

Main definitions

• TauCeti.Probability.inverseWishartPDFReal and TauCeti.Probability.inverseWishartPDF — the inverse-Wishart density, real- and ℝ≥0∞-valued.
• TauCeti.Probability.inverseWishartMeasure — the inverse-Wishart law.

Main results

• TauCeti.Probability.inverseWishartMeasure_of_posDef — at a valid degree and scale the law is the density against TauCeti.symmetricLebesgue, while TauCeti.Probability.inverseWishartMeasure_of_not_posDef and TauCeti.Probability.inverseWishartMeasure_of_le describe the two invalid branches.
• TauCeti.Probability.isProbabilityMeasure_inverseWishartMeasure — at those parameters the law has total mass one.
• TauCeti.Probability.hasPDF_of_hasLaw_inverseWishartMeasure and TauCeti.Probability.rnDeriv_inverseWishartMeasure — an inverse-Wishart random matrix has a density against TauCeti.symmetricLebesgue, and at those parameters the law's Radon–Nikodym derivative is TauCeti.Probability.inverseWishartPDF.
• TauCeti.Probability.ae_posDef_inverseWishartMeasure — the sampled matrix is positive definite almost everywhere.
• TauCeti.Probability.map_symmetricCongruence_inverseWishartMeasure — congruence by an invertible matrix carries the law of scale S to the law of scale C * S * Cᵀ.
• TauCeti.Probability.inverseWishartMeasure_zero — in dimension zero the law is the Dirac mass at the unique symmetric matrix, hence a probability measure.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, chapters 2 and 3.

The density

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

The inverse-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 S) ^ (n / 2) * (det B) ^ (-((n + p + 1) / 2)) * exp (-trace (S * B⁻¹) / 2) divided by the constant 2 ^ (n p / 2) * Γ_p(n / 2), and it vanishes off the cone.

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

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

@[simp]

theorem TauCeti.Probability.inverseWishartPDFReal_of_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hB : (↑B).PosDef) : inverseWishartPDFReal n S B = S.det ^ (n / 2) * (↑B).det ^ (-((n + ↑p + 1) / 2)) * Real.exp (-(S * (↑B)⁻¹).trace / 2) / (2 ^ (n * ↑p / 2) * multivariateGamma p (n / 2))

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

@[simp]

theorem TauCeti.Probability.inverseWishartPDFReal_of_not_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hB : ¬(↑B).PosDef) : inverseWishartPDFReal n S B = 0

Off the positive-definite cone the inverse-Wishart density vanishes.

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

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

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

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

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

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

theorem TauCeti.Probability.inverseWishartPDF_def {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : inverseWishartPDF n S B = ENNReal.ofReal (inverseWishartPDFReal n S B)

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

@[simp]

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

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

@[simp]

theorem TauCeti.Probability.inverseWishartPDF_of_not_posDef {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) {B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hB : ¬(↑B).PosDef) : inverseWishartPDF n S B = 0

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

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

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

@[simp]

theorem TauCeti.Probability.inverseWishartPDF_ne_top {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : inverseWishartPDF n S B ≠ ⊤

The inverse-Wishart density is finite.

theorem TauCeti.Probability.toReal_inverseWishartPDF {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (inverseWishartPDF n S B).toReal = inverseWishartPDFReal n S B

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

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

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

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

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

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

The ℝ≥0∞-valued inverse-Wishart density is measurable in the point.

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

The ℝ≥0∞-valued inverse-Wishart density is measurable jointly in its degree, its scale matrix and the point.

The measure

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

The inverse-Wishart law of real degree n and positive-definite scale S: the image of the Wishart law of the inverted scale under matrix inversion. Mathlib's totalized inverse, which is zero on singular matrices, is kept; the source law is carried by the positive-definite cone, on which inversion is a bijection. Outside the classical parameter range the source law, and hence this one, is zero.

theorem TauCeti.Probability.inverseWishartMeasure_def {p : ℕ} (n : ℝ) (S : Matrix (Fin p) (Fin p) ℝ) : inverseWishartMeasure n S = MeasureTheory.Measure.map symmetricInv (nonsingularWishartMeasure n S⁻¹)

The defining expression of the inverse-Wishart law.

@[simp]

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

At a scale that is not positive definite the inverse-Wishart law is zero: the inverted scale is then not positive definite either, so the source Wishart law already vanishes.

@[simp]

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

At a degree at most p - 1 the inverse-Wishart law is zero, as the source Wishart law is.

@[simp]

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

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

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

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

The density theorem

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

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

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

The inverse-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.

The density of an inverse-Wishart random matrix

theorem TauCeti.Probability.hasPDF_of_hasLaw_inverseWishartMeasure {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 (inverseWishartMeasure n S) P) : MeasureTheory.HasPDF X P (symmetricLebesgue p)

A random symmetric matrix with an inverse-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_inverseWishartPDF_of_hasLaw_inverseWishartMeasure {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 (inverseWishartMeasure n S) P) : MeasureTheory.pdf X P (symmetricLebesgue p) =ᵐ[symmetricLebesgue p] inverseWishartPDF n S

The density against TauCeti.symmetricLebesgue of a random symmetric matrix with an inverse-Wishart law is TauCeti.Probability.inverseWishartPDF.

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

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

Congruence

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

Congruence carries the inverse-Wishart law of scale S to the one of scale C * S * Cᵀ. On the Wishart side the same change of scale is the congruence by the inverse transpose of C, and inverting exchanges the two congruences.

Dimension zero

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

In dimension zero every valid inverse-Wishart law is the Dirac mass at the unique symmetric matrix, the image under inversion of the Dirac Wishart law there.

@[simp]

theorem TauCeti.Probability.inverseWishartPDFReal_zero (n : ℝ) (S : Matrix (Fin 0) (Fin 0) ℝ) (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ))) : inverseWishartPDFReal n S B = 1

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

@[simp]

theorem TauCeti.Probability.inverseWishartPDF_zero (n : ℝ) (S : Matrix (Fin 0) (Fin 0) ℝ) (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ))) : inverseWishartPDF n S B = 1

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

theorem TauCeti.Probability.isProbabilityMeasure_inverseWishartMeasure_zero {n : ℝ} (hn : -1 < n) (S : Matrix (Fin 0) (Fin 0) ℝ) : MeasureTheory.IsProbabilityMeasure (inverseWishartMeasure n S)

In dimension zero every valid inverse-Wishart law is a probability measure.