The standard Wishart density in Cholesky coordinates

A positive-definite symmetric p × p matrix A is L * Lᵀ for a unique lower-triangular L with positive diagonal. This file shows that the standard Wishart density of real degree n,

(det A) ^ ((n - p - 1) / 2) * exp (-trace A / 2) / (2 ^ (n * p / 2) * Γ_p (n / 2))

against TauCeti.symmetricLebesgue p on the positive-definite cone, becomes a product density in the entries of L. Precisely, assume (p : ℝ) - 1 < n, so that every n - i with i < p is positive, and take independent real coordinates indexed by the on-or-below diagonal positions (i, j), j ≤ i, of a p × p matrix, where

• the diagonal coordinate (i, i) has the chi density with n - i degrees of freedom, 2 ^ (1 - k / 2) / Γ (k / 2) * t ^ (k - 1) * exp (-t ^ 2 / 2) on t > 0 with k = n - i, and
• a strictly lower coordinate has the standard Gaussian law gaussianReal 0 1.

Then the random symmetric matrix L * Lᵀ built from these coordinates has the standard Wishart density, which is the law TauCeti.Probability.nonsingularWishartMeasure n 1. Since L ↦ L * Lᵀ is the inverse of the Cholesky factorization on the positive-definite cone, reading the implication backwards gives the Bartlett decomposition: lift the Wishart law to the cone, factor, and the on-or-below-diagonal entries of the Cholesky factor are independent, the diagonal entry T i i having (T i i) ^ 2 chi-squared with n - i degrees of freedom and each strictly lower entry standard Gaussian.

In the coordinates of L the determinant of L * Lᵀ is the square of the product of the diagonal entries and its trace is the sum of the squares of all entries, so, multiplied by the Jacobian 2 ^ p * ∏ i, (L i i) ^ (p - i) of the Cholesky change of variables TauCeti.map_cholesky_symmetricLebesgue, the Wishart density becomes one factor per coordinate.

Main declarations

• TauCeti.Probability.bartlettCoordinateMeasure — the coordinate measure of one Cholesky coordinate; for (p : ℝ) - 1 < n it is the chi or standard Gaussian law of that coordinate.
• TauCeti.Probability.map_lowerTriangleGram_pi_bartlettCoordinateMeasure — the Gram matrix of independent coordinates with these laws has the standard Wishart density.
• TauCeti.Probability.map_sq_bartlettCoordinateMeasure_of_eq and TauCeti.Probability.isProbabilityMeasure_bartlettCoordinateMeasure — the square of a diagonal coordinate is chi-squared, and every coordinate law is normalized.
• TauCeti.Probability.map_diagonal_sq_pi_bartlettCoordinateMeasure — the diagonal squares of independent Bartlett coordinates have the product of their chi-squared laws.
• TauCeti.Probability.nonsingularWishartMeasure_one_eq_map_lowerTriangleGram — the standard Wishart law is the Gram image of the product of the coordinate laws.
• TauCeti.Probability.map_choleskyLowerCoordinates_comap_nonsingularWishartMeasure — the Cholesky coordinates of the lifted standard Wishart law are that product, the Bartlett decomposition at the level of measures.
• TauCeti.Probability.bartlett_nonsingularWishartMeasure — its random-variable form: independence of the Cholesky entries together with their chi-squared and standard Gaussian laws.

References

• M. S. Bartlett, On the theory of statistical regression, Proc. Roy. Soc. Edinburgh 53 (1933), 260–283.
• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, Section 3.2.

noncomputable def TauCeti.Probability.bartlettCoordinateMeasure {p : ℕ} (n : ℝ) (ij : lowerTriangle p) : MeasureTheory.Measure ℝ

The coordinate measure at the on-or-below-diagonal position ij of the Cholesky factor of a standard Wishart matrix of real degree n. At a diagonal position (i, i) it is Lebesgue measure on the positive half-line with the chi density formula for n - i degrees of freedom, and at a strictly lower position it is the standard Gaussian law. The definition places no condition on n: the diagonal measure is the chi probability law only when 0 < n - i, which holds for every i < p under the nonzero-dimensional hypothesis (p : ℝ) - 1 < n of TauCeti.Probability.map_lowerTriangleGram_pi_bartlettCoordinateMeasure.

@[simp]

theorem TauCeti.Probability.bartlettCoordinateMeasure_of_eq {p : ℕ} (n : ℝ) {ij : lowerTriangle p} (h : (↑ij).1 = (↑ij).2) : bartlettCoordinateMeasure n ij = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 ^ (1 - (n - ↑↑(↑ij).1) / 2) / Real.Gamma ((n - ↑↑(↑ij).1) / 2) * t ^ (n - ↑↑(↑ij).1 - 1) * Real.exp (-t ^ 2 / 2))

At a diagonal position (i, i) the coordinate measure is Lebesgue measure on the positive half-line with the chi density formula for n - i degrees of freedom; it is the chi law when 0 < n - i.

@[simp]

theorem TauCeti.Probability.bartlettCoordinateMeasure_of_ne {p : ℕ} (n : ℝ) {ij : lowerTriangle p} (h : (↑ij).1 ≠ (↑ij).2) : bartlettCoordinateMeasure n ij = ProbabilityTheory.gaussianReal 0 1

A strictly lower Cholesky coordinate is standard Gaussian.

instance TauCeti.Probability.instSigmaFiniteRealBartlettCoordinateMeasure {p : ℕ} (n : ℝ) (ij : lowerTriangle p) : MeasureTheory.SigmaFinite (bartlettCoordinateMeasure n ij)

Every Bartlett coordinate measure is sigma-finite, enabling their product over the lower-triangular coordinates to be formed with Measure.pi.

theorem TauCeti.Probability.map_lowerTriangleGram_pi_bartlettCoordinateMeasure {p : ℕ} {n : ℝ} (hn : p = 0 ∨ ↑p - 1 < n) : MeasureTheory.Measure.map (lowerTriangleGram p) (MeasureTheory.Measure.pi (bartlettCoordinateMeasure n)) = ((symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}).withDensity fun (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ENNReal.ofReal ((↑A).det ^ ((n - ↑p - 1) / 2) * Real.exp (-(↑A).trace / 2) / (2 ^ (n * ↑p / 2) * multivariateGamma p (n / 2)))

The standard Wishart law in Cholesky coordinates. Let the on-or-below-diagonal entries of a lower-triangular p × p matrix L be independent, the diagonal entry L i i with the chi density with n - i degrees of freedom and each strictly lower entry standard Gaussian. If p = 0, the equality below holds for every n; otherwise assume (p : ℝ) - 1 < n. Then the symmetric matrix L * Lᵀ has the standard Wishart density of degree n, (det A) ^ ((n - p - 1) / 2) * exp (-trace A / 2) / (2 ^ (n * p / 2) * Γ_p (n / 2)) on the positive-definite cone, against TauCeti.symmetricLebesgue p.

The coordinate laws

theorem TauCeti.Probability.map_sq_bartlettCoordinateMeasure_of_eq {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) {ij : lowerTriangle p} (h : (↑ij).1 = (↑ij).2) : MeasureTheory.Measure.map (fun (t : ℝ) => t ^ 2) (bartlettCoordinateMeasure n ij) = chiSquaredMeasure (n - ↑↑(↑ij).1)

The square of a diagonal Bartlett coordinate is chi-squared with n - i degrees of freedom: squaring carries the chi density to the chi-squared density.

theorem TauCeti.Probability.isProbabilityMeasure_bartlettCoordinateMeasure {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) (ij : lowerTriangle p) : MeasureTheory.IsProbabilityMeasure (bartlettCoordinateMeasure n ij)

Every Bartlett coordinate law is a probability measure: the chi density is normalized at positive degrees of freedom, and the strictly lower coordinates are standard Gaussian.

theorem TauCeti.Probability.map_diagonal_sq_pi_bartlettCoordinateMeasure {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) : MeasureTheory.Measure.map (fun (x : lowerTriangle p → ℝ) (i : Fin p) => x ⟨(i, i), ⋯⟩ ^ 2) (MeasureTheory.Measure.pi (bartlettCoordinateMeasure n)) = MeasureTheory.Measure.pi fun (i : Fin p) => chiSquaredMeasure (n - ↑↑i)

The diagonal squares of independent Bartlett coordinates form a product of chi-squared laws, with the degrees decreasing along the diagonal.

theorem TauCeti.Probability.pi_bartlettCoordinateMeasure_compl_posDiagLowerRegion {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) : (MeasureTheory.Measure.pi (bartlettCoordinateMeasure n)) (posDiagLowerRegion p)ᶜ = 0

The product of the coordinate laws gives no mass to a nonpositive diagonal coordinate.

The Bartlett decomposition

theorem TauCeti.Probability.nonsingularWishartMeasure_one_eq_map_lowerTriangleGram {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) : nonsingularWishartMeasure n 1 = MeasureTheory.Measure.map (lowerTriangleGram p) (MeasureTheory.Measure.pi (bartlettCoordinateMeasure n))

The standard Wishart law is the Gram image of the Bartlett coordinates. This is TauCeti.Probability.map_lowerTriangleGram_pi_bartlettCoordinateMeasure with the density on the right recognised as TauCeti.Probability.nonsingularWishartMeasure n 1: at the scale 1 both the inverse scale in the exponential weight and the scale determinant in the normalizing constant disappear.

theorem TauCeti.Probability.map_choleskyLowerCoordinates_comap_nonsingularWishartMeasure {p : ℕ} {n : ℝ} (hn : ↑p - 1 < n) : MeasureTheory.Measure.map (choleskyLowerCoordinates p) (MeasureTheory.Measure.comap Subtype.val (nonsingularWishartMeasure n 1)) = MeasureTheory.Measure.pi (bartlettCoordinateMeasure n)

The Bartlett decomposition of the standard Wishart law. Lift TauCeti.Probability.nonsingularWishartMeasure n 1 to the positive-definite cone, where Cholesky factorization is defined, and read the on-or-below-diagonal entries of the factor: the resulting law is the product of the Bartlett coordinate laws. Cholesky factorization inverts the Gram map of TauCeti.Probability.map_lowerTriangleGram_pi_bartlettCoordinateMeasure, and the product law lives on the positive-diagonal region where that inversion is valid.

theorem TauCeti.Probability.bartlett_nonsingularWishartMeasure {p : ℕ} {n : ℝ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (hn : ↑p - 1 < n) {A : Ω → PosDefMatrix p} (hA : ProbabilityTheory.HasLaw A (MeasureTheory.Measure.comap Subtype.val (nonsingularWishartMeasure n 1)) P) : ProbabilityTheory.iIndepFun (fun (ij : lowerTriangle p) (ω : Ω) => ↑(cholesky (A ω)) (↑ij).1 (↑ij).2) P ∧ (∀ (i : Fin p), ProbabilityTheory.HasLaw (fun (ω : Ω) => ↑(cholesky (A ω)) i i ^ 2) (chiSquaredMeasure (n - ↑↑i)) P) ∧ ∀ (i j : Fin p), j < i → ProbabilityTheory.HasLaw (fun (ω : Ω) => ↑(cholesky (A ω)) i j) (ProbabilityTheory.gaussianReal 0 1) P

The Bartlett decomposition. Let A be a random positive-definite symmetric matrix whose law is the standard Wishart law of degree n read on the cone, and let T be its Cholesky factor. Then the on-or-below-diagonal entries of T are independent, the square of the i-th diagonal entry is chi-squared with n - i degrees of freedom, and every strictly lower entry is standard Gaussian. The degrees of freedom decrease along the diagonal because the zero-based index i counts the coordinates already consumed by the preceding rows.