Documentation

TauCeti.Probability.Distributions.Wishart.Inverse.Moments

Moments of the inverse-Wishart family #

At the standard scale, each diagonal entry has an inverse-gamma law. The proof uses Cholesky coordinates of the source Wishart matrix. Orthogonal congruence transports this law to every diagonal entry. It also makes the off-diagonal means vanish. Congruence by a square root carries the standard mean to a positive-definite scale.

For a positive-definite scale S and degree above the threshold p + 1, the mean is (n - p - 1)⁻¹ • S. This threshold is sharp within the valid family: for a positive-definite scale in positive dimension, the matrix is not integrable when p - 1 < n ≤ p + 1.

Main results #

References #

The law of a diagonal entry at the standard scale #

The mean #

source
theorem TauCeti.Probability.map_coe_apply_inverseWishartMeasure_one {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) (i : Fin p) :
MeasureTheory.Measure.map (fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ↑B i i) (inverseWishartMeasure n 1) = inverseGammaMeasure ((n - ↑p + 1) / 2) (1 / 2)

Every diagonal entry of an inverse-Wishart matrix of standard scale is inverse gamma, with shape (n - p + 1) / 2 and scale 1 / 2. Equivalently, the reciprocal of a diagonal entry is chi-squared with n - p + 1 degrees of freedom.

source
theorem TauCeti.Probability.integrable_id_inverseWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p + 1 < n) :
MeasureTheory.Integrable (fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => B) (inverseWishartMeasure n S)

An inverse-Wishart matrix is integrable above the degree threshold p + 1.

source
theorem TauCeti.Probability.integral_id_inverseWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p + 1 < n) :
∫ (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))), B ∂inverseWishartMeasure n S = (n - ↑p - 1)⁻¹ • ⟨S, ⋯⟩

The mean of an inverse-Wishart law of degree n and positive-definite scale S is (n - p - 1)⁻¹ • S, for a degree above the threshold p + 1; in positive dimension, at a valid degree at or below the threshold the identity is no longer integrable.

source
theorem TauCeti.Probability.not_integrable_id_inverseWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hp : 0 < p) (hS : S.PosDef) (hn : ↑p - 1 < n) (hn' : n ≤ ↑p + 1) :
¬MeasureTheory.Integrable (fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => B) (inverseWishartMeasure n S)

Below the degree threshold p + 1 an inverse-Wishart matrix is not integrable, in every positive dimension, as long as the degree is that of a genuine member of the family: a diagonal entry then has an inverse-gamma law of shape at most one. Below the valid range the law is zero and the statement fails for want of any mass.

source
theorem TauCeti.Probability.integrable_id_inverseWishartMeasure_zero {n : ℝ} (hn : -1 < n) (S : Matrix (Fin 0) (Fin 0) ℝ) :
MeasureTheory.Integrable id (inverseWishartMeasure n S)

In dimension zero the identity is integrable against every valid inverse-Wishart law, the whole mass sitting at a single point.

source
theorem TauCeti.Probability.integral_id_inverseWishartMeasure_zero {n : ℝ} (hn : -1 < n) (S : Matrix (Fin 0) (Fin 0) ℝ) :
∫ (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ))), B ∂inverseWishartMeasure n S = 0

In dimension zero every valid inverse-Wishart law has mean zero, the unique symmetric matrix.