The Gaussian-Gram Wishart family

The Gaussian-Gram Wishart law TauCeti.Probability.wishartGramMeasure ν S is the law of the Gram sum ∑ r, X r * (X r)ᵀ of ν independent centred multivariate Gaussian vectors with covariance matrix S, carried by the symmetric-matrix subspace of TauCeti.MeasureTheory.Measure.SymmetricMatrix.Basic. It is defined for every natural degree ν and every square matrix S, with no branch on S: Mathlib totalizes multivariateGaussian 0 S to Measure.dirac 0 when S is not positive semidefinite, and the Gram law inherits that totalization. That is what lets this family carry the legitimately singular Wishart laws, which a density definition cannot.

Main definitions

• TauCeti.Probability.wishartGram — the Gram sum of a finite family of Euclidean vectors, bundled into the symmetric-matrix subspace.
• TauCeti.Probability.wishartGramMeasure — the Gaussian-Gram Wishart law.

Main results

• TauCeti.Probability.trace_mul_coe_wishartGram — the trace statistic of a Gram sum is the sum of the quadratic forms of its vectors.
• TauCeti.Probability.isProbabilityMeasure_wishartGramMeasure — it is a probability measure, at every degree and every scale matrix.
• TauCeti.Probability.hasLaw_wishartGram_gaussian — the Gram sum of an independent centred Gaussian family has this law.
• TauCeti.Probability.wishartGramMeasure_of_not_posSemidef — outside the positive-semidefinite cone the law is the Dirac mass at zero.
• TauCeti.Probability.map_symmetricCongruenceLinearMap_wishartGramMeasure — a rectangular congruence carries the law of scale S to the law of scale M * S * Mᵀ, and TauCeti.Probability.wishartGramMeasure_eq_map_sqrt specializes it to the square root of the scale.
• TauCeti.Probability.wishartGramMeasure_conv_wishartGramMeasure — the degrees add under convolution.
• TauCeti.Probability.wishartGramMeasure_setOf_posSemidef — the law is carried by the positive-semidefinite cone.
• TauCeti.Probability.ae_posSemidef_wishartGramMeasure — the sampled matrix is positive semidefinite almost everywhere.
• TauCeti.Probability.wishartGramMeasure_setOf_rank_le — the rank is at most min ν S.rank.
• TauCeti.Probability.ae_rank_le_wishartGramMeasure — the same rank bound holds almost everywhere.
• TauCeti.Probability.mutuallySingular_wishartGramMeasure_symmetricLebesgue — below that rank threshold the law has no density against TauCeti.symmetricLebesgue.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, chapter 3.

The Gram sum of a family of Euclidean vectors

noncomputable def TauCeti.Probability.wishartGram {ι : Type u_1} [Fintype ι] {p : ℕ} (X : ι → EuclideanSpace ℝ (Fin p)) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The Gram sum ∑ r, X r * (X r)ᵀ of a finite family of Euclidean vectors, as an element of the symmetric-matrix subspace. It is the Gram matrix Matrix.gram of the p coordinate columns i ↦ (r ↦ X r i) of the family, and it is the statistic whose law is the Gaussian-Gram Wishart family.

theorem TauCeti.Probability.coe_wishartGram_eq_gram {ι : Type u_1} [Fintype ι] {p : ℕ} (X : ι → EuclideanSpace ℝ (Fin p)) : ↑(wishartGram X) = Matrix.gram ℝ fun (i : Fin p) => WithLp.toLp 2 fun (r : ι) => (X r).ofLp i

The Gram sum is the Gram matrix of the coordinate columns of the family.

@[simp]

theorem TauCeti.Probability.coe_wishartGram {ι : Type u_1} [Fintype ι] {p : ℕ} (X : ι → EuclideanSpace ℝ (Fin p)) : ↑(wishartGram X) = ∑ r : ι, Matrix.vecMulVec (X r).ofLp (X r).ofLp

theorem TauCeti.Probability.trace_mul_coe_wishartGram {ι : Type u_1} [Fintype ι] {p : ℕ} (Θ : Matrix (Fin p) (Fin p) ℝ) (X : ι → EuclideanSpace ℝ (Fin p)) : (Θ * ↑(wishartGram X)).trace = ∑ r : ι, inner ℝ (X r) ((Matrix.toEuclideanLin Θ) (X r))

The trace statistic of a Gram sum is the sum of the quadratic forms of Θ at the vectors. This is what turns a Wishart trace statistic into a sum of Gaussian quadratic forms, one per sampled vector. No symmetry of Θ is needed.

theorem TauCeti.Probability.posSemidef_coe_wishartGram {ι : Type u_1} [Fintype ι] {p : ℕ} (X : ι → EuclideanSpace ℝ (Fin p)) : (↑(wishartGram X)).PosSemidef

The Gram sum of a family of Euclidean vectors is positive semidefinite.

theorem TauCeti.Probability.rank_coe_wishartGram_le {ι : Type u_1} [Fintype ι] {p : ℕ} (X : ι → EuclideanSpace ℝ (Fin p)) : (↑(wishartGram X)).rank ≤ Fintype.card ι

The Gram sum of a family of vectors has rank at most the size of the family.

theorem TauCeti.Probability.wishartGram_toEuclideanLin {ι : Type u_1} [Fintype ι] {p q : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) (X : ι → EuclideanSpace ℝ (Fin p)) : (wishartGram fun (r : ι) => (Matrix.toEuclideanLin M) (X r)) = M.symmetricCongruenceLinearMap (wishartGram X)

A linear image of the vectors congruates their Gram sum.

theorem TauCeti.Probability.continuous_wishartGram {ι : Type u_1} [Fintype ι] {p : ℕ} : Continuous wishartGram

The Gram sum is continuous in the family of vectors.

theorem TauCeti.Probability.measurable_wishartGram {ι : Type u_1} [Fintype ι] {p : ℕ} : Measurable wishartGram

The Gram sum is measurable in the family of vectors.

The Gaussian-Gram Wishart law

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

The Gaussian-Gram Wishart law of degree ν and scale S: the law of the Gram sum of ν independent centred multivariate Gaussian vectors with covariance S. When S is not positive semidefinite Mathlib's multivariateGaussian 0 S is Measure.dirac 0, and this law is then Measure.dirac 0 too.

theorem TauCeti.Probability.wishartGramMeasure_eq_map_pi {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : wishartGramMeasure ν S = MeasureTheory.Measure.map wishartGram (MeasureTheory.Measure.pi fun (x : Fin ν) => ProbabilityTheory.multivariateGaussian 0 S)

The Gaussian-Gram law is the image under the Gram sum of the product of its ν independent Gaussian factors. Transporting a statistic of the law along this identity rewrites it as a statistic of that product measure, where the ν factors are handled one at a time.

instance TauCeti.Probability.isProbabilityMeasure_wishartGramMeasure {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : MeasureTheory.IsProbabilityMeasure (wishartGramMeasure ν S)

@[simp]

theorem TauCeti.Probability.wishartGramMeasure_zero {p : ℕ} (S : Matrix (Fin p) (Fin p) ℝ) : wishartGramMeasure 0 S = MeasureTheory.Measure.dirac 0

At degree zero the Gaussian-Gram law is the Dirac mass at the zero matrix.

@[simp]

theorem TauCeti.Probability.wishartGramMeasure_of_not_posSemidef {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} (ν : ℕ) (hS : ¬S.PosSemidef) : wishartGramMeasure ν S = MeasureTheory.Measure.dirac 0

With a scale matrix outside the positive-semidefinite cone, Mathlib totalizes the Gaussian factor to a Dirac mass, and the Gaussian-Gram law is then the Dirac mass at the zero matrix.

theorem TauCeti.Probability.hasLaw_wishartGram_gaussian {p ν : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} {Ω : Type u_2} {x✝ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Fin ν → Ω → EuclideanSpace ℝ (Fin p)} (hX : ∀ (r : Fin ν), ProbabilityTheory.HasLaw (X r) (ProbabilityTheory.multivariateGaussian 0 S) P) (hindep : ProbabilityTheory.iIndepFun X P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => wishartGram fun (r : Fin ν) => X r ω) (wishartGramMeasure ν S) P

The Gram sum of an independent centred Gaussian family is Gaussian-Gram Wishart.

Congruence

theorem TauCeti.Probability.map_symmetricCongruenceLinearMap_wishartGramMeasure {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} {q : ℕ} (ν : ℕ) (M : Matrix (Fin q) (Fin p) ℝ) (hS : S.PosSemidef) : MeasureTheory.Measure.map (⇑M.symmetricCongruenceLinearMap) (wishartGramMeasure ν S) = wishartGramMeasure ν (M * S * M.transpose)

Congruence by a rectangular matrix carries the Gaussian-Gram law of scale S to the one of scale M * S * Mᵀ. No rank hypothesis on M is needed.

theorem TauCeti.Probability.wishartGramMeasure_eq_map_sqrt {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} (ν : ℕ) (hS : S.PosSemidef) : wishartGramMeasure ν S = MeasureTheory.Measure.map (⇑(CFC.sqrt S).symmetricCongruenceLinearMap) (wishartGramMeasure ν 1)

The Gaussian-Gram law of a positive-semidefinite scale S is the standard Gaussian-Gram law pushed forward by the congruence with CFC.sqrt S.

Support, rank and singularity

theorem TauCeti.Probability.wishartGramMeasure_setOf_posSemidef {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : (wishartGramMeasure ν S) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosSemidef} = 1

The Gaussian-Gram law is carried by the positive-semidefinite cone.

theorem TauCeti.Probability.ae_posSemidef_wishartGramMeasure {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : ∀ᵐ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) ∂wishartGramMeasure ν S, (↑A).PosSemidef

A Gaussian-Gram Wishart matrix is positive semidefinite almost everywhere.

theorem TauCeti.Probability.wishartGramMeasure_setOf_rank_le {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : (wishartGramMeasure ν S) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).rank ≤ min ν S.rank} = 1

The Gaussian-Gram law of degree ν has rank at most min ν S.rank. With fewer Gaussian samples than dimensions, or a singular scale matrix, the law lives on singular matrices.

theorem TauCeti.Probability.ae_rank_le_wishartGramMeasure {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : ∀ᵐ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) ∂wishartGramMeasure ν S, (↑A).rank ≤ min ν S.rank

A Gaussian-Gram Wishart matrix has rank at most min ν S.rank almost everywhere.

theorem TauCeti.Probability.mutuallySingular_wishartGramMeasure_symmetricLebesgue {p : ℕ} (ν : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) (hrank : min ν S.rank < p) : (wishartGramMeasure ν S).MutuallySingular (symmetricLebesgue p)

Below the rank threshold the Gaussian-Gram law has no density. It is then carried by the singular symmetric matrices, which are TauCeti.symmetricLebesgue-null.

Convolution

theorem TauCeti.Probability.wishartGramMeasure_conv_wishartGramMeasure {p : ℕ} (ν₁ ν₂ : ℕ) (S : Matrix (Fin p) (Fin p) ℝ) : (wishartGramMeasure ν₁ S).conv (wishartGramMeasure ν₂ S) = wishartGramMeasure (ν₁ + ν₂) S

The degrees of the Gaussian-Gram family add under convolution.