Documentation

TauCeti.Probability.Distributions.Wishart.Inverse.Marginal

Diagonal marginals of the inverse-Wishart law #

For a positive-definite scale S, every diagonal entry of an inverse-Wishart matrix of degree n has the inverse-gamma law of shape (n - p + 1) / 2 and scale S i i / 2. Equivalently, if W is Wishart of degree n > p - 1 and scale S⁻¹, the reciprocal of the diagonal entry (W⁻¹) i i — the Schur complement of the complementary principal block of W — is (S i i)⁻¹ times a chi-squared variable with n - p + 1 degrees of freedom. These scalar laws are what the inverse-Wishart family offers to one-dimensional observables. In particular, for degree n > p - 1 the diagonal quantile at an interior level u is (S i i / 2) / inverseRegularizedGamma ((n - p + 1) / 2) (1 - u), with endpoint limits zero and infinity. The identification of ((W⁻¹) i i)⁻¹ with the scalar Schur complement is Matrix.PosDef.inv_inv_apply_self_eq_sub. The general-scale laws extend the standard-scale case TauCeti.Probability.map_coe_apply_inverseWishartMeasure_one.

When the degree is at most p - 1 the inverse-Wishart law is zero, and so is the inverse-gamma law of nonpositive shape, so the inverse-gamma statement needs no hypothesis on the degree.

Main results #

References #

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

The diagonal entries of an inverse-Wishart matrix are inverse gamma. For a positive-definite scale S, the entry (i, i) of an inverse-Wishart matrix of degree n has the inverse-gamma law of shape (n - p + 1) / 2 and scale S i i / 2. For degrees at most p - 1 both sides are the zero measure.

source
theorem TauCeti.Probability.map_inv_inv_apply_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) (i : Fin p) :
MeasureTheory.Measure.map (fun (W : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ((↑W)⁻¹ i i)⁻¹) (nonsingularWishartMeasure n S⁻¹) = MeasureTheory.Measure.map (fun (x : ℝ) => (S i i)⁻¹ * x) (chiSquaredMeasure (n - ↑p + 1))

The reciprocal diagonal entries of an inverted Wishart matrix are scaled chi-squared. If W is Wishart of degree n > p - 1 and positive-definite scale S⁻¹, the reciprocal of the diagonal entry (W⁻¹) i i, which is the Schur complement in W of the principal block away from i (Matrix.PosDef.inv_inv_apply_self_eq_sub), has the law of (S i i)⁻¹ times a chi-squared variable with n - p + 1 degrees of freedom.

Diagonal quantiles #

source
@[simp]
theorem TauCeti.Probability.quantile_map_coe_apply_inverseWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (i : Fin p) {u : ℝ} :
(MeasureTheory.Measure.map (fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ↑B i i) (inverseWishartMeasure n S)).quantile u = S i i / 2 / inverseRegularizedGamma ((n - ↑p + 1) / 2) (1 - u)

The quantile of a diagonal entry of an inverse-Wishart matrix of positive-definite scale S is the inverse-gamma quantile of shape (n - p + 1) / 2 and scale S i i / 2.

source
theorem TauCeti.Probability.tendsto_quantile_map_coe_apply_inverseWishartMeasure_nhdsGT_zero {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) (i : Fin p) :
Filter.Tendsto (fun (u : ℝ) => ↑((MeasureTheory.Measure.map (fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ↑B i i) (inverseWishartMeasure n S)).quantile u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The diagonal quantiles of an inverse-Wishart matrix tend to zero as the level tends to zero from above.

source
theorem TauCeti.Probability.tendsto_quantile_map_coe_apply_inverseWishartMeasure_nhdsLT_one {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (hn : ↑p - 1 < n) (i : Fin p) :
Filter.Tendsto (fun (u : ℝ) => ↑((MeasureTheory.Measure.map (fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ↑B i i) (inverseWishartMeasure n S)).quantile u)) (nhdsWithin 1 (Set.Iio 1)) (nhds ⊤)

The diagonal quantiles of an inverse-Wishart matrix tend to positive infinity as the level tends to one from below.

source
theorem TauCeti.Probability.hasLaw_coe_apply_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) (hS : S.PosDef) (i : Fin p) :
ProbabilityTheory.HasLaw (fun (ω : Ω) => ↑(X ω) i i) (inverseGammaMeasure ((n - ↑p + 1) / 2) (S i i / 2)) P

A diagonal entry of a random inverse-Wishart matrix of positive-definite scale S has the inverse-gamma law of shape (n - p + 1) / 2 and scale S i i / 2.

source
theorem TauCeti.Probability.hasLaw_inv_inv_apply_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {S : Matrix (Fin p) (Fin p) ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {W : Ω → ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hW : ProbabilityTheory.HasLaw W (nonsingularWishartMeasure n S⁻¹) P) (hS : S.PosDef) (hn : ↑p - 1 < n) (i : Fin p) :
ProbabilityTheory.HasLaw (fun (ω : Ω) => ((↑(W ω))⁻¹ i i)⁻¹) (MeasureTheory.Measure.map (fun (x : ℝ) => (S i i)⁻¹ * x) (chiSquaredMeasure (n - ↑p + 1))) P

For a random Wishart matrix W of degree n > p - 1 and positive-definite scale S⁻¹, the reciprocal of the diagonal entry (W⁻¹) i i has the law of (S i i)⁻¹ times a chi-squared variable with n - p + 1 degrees of freedom.