The multivariate Gamma function in Cholesky coordinates

Every positive-definite symmetric p × p matrix is L * Lᵀ for a unique lower-triangular L with positive diagonal, and reading off the on-or-below-diagonal entries of L turns the positive-definite cone into the region TauCeti.posDiagLowerRegion p of TauCeti.lowerTriangle p → ℝ whose diagonal coordinates are positive. This file evaluates, in those coordinates, the integral whose value is TauCeti.multivariateGamma p a when (p - 1) / 2 < a (a condition only in positive dimension):

∫ (det (L * Lᵀ)) ^ (a - (p + 1) / 2) * exp (-trace (L * Lᵀ)) * (2 ^ p * ∏ i, (L i i) ^ (p - i))

over that region, the last factor being the Jacobian of L ↦ L * Lᵀ computed in TauCeti/LinearAlgebra/Matrix/Cholesky/Jacobian.lean. The point of the coordinates is that the integrand factorizes: the determinant and the trace of L * Lᵀ are a product and a sum over the entries of L, so Fubini reduces the integral to one-dimensional Gamma and Gaussian integrals, one for each entry. The p diagonal entries produce the Gamma factors Γ(a - i / 2) and the p (p - 1) / 2 strictly lower entries produce the powers of √π.

Transported by the Cholesky change of variables, this integral is the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace A) over the cone of positive-definite symmetric matrices against TauCeti.symmetricLebesgue p, which is the normalizing constant of the Wishart density.

Main results

• TauCeti.integral_lowerTriangle_det_rpow_mul_exp_neg_trace — the value of the integral;
• TauCeti.integrableOn_lowerTriangle_det_rpow_mul_exp_neg_trace — its integrand is integrable on the region.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Theorem 2.1.14.
• M. L. Eaton, Multivariate Statistics: A Vector Space Approach, Chapter 5.

theorem TauCeti.integral_lowerTriangle_det_rpow_mul_exp_neg_trace {p : ℕ} {a : ℝ} (ha : 0 < p → (↑p - 1) / 2 < a) : ∫ (x : lowerTriangle p → ℝ) in posDiagLowerRegion p, ((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).det ^ (a - (↑p + 1) / 2) * Real.exp (-((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).trace) * (2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i)) = multivariateGamma p a

The multivariate Gamma integral in Cholesky coordinates. Over the region of lower-triangular coordinates with positive diagonal, the Wishart integrand (det A) ^ (a - (p + 1) / 2) * exp (-trace A) pulled back along L ↦ L * Lᵀ and weighted by the Jacobian 2 ^ p * ∏ i, (L i i) ^ (p - i) integrates to Γ_p(a) when (p - 1) / 2 < a. The bound is needed only in positive dimension: for p = 0 the coordinate space is a point, where the integrand is 1 = Γ₀(a) for every a.

theorem TauCeti.integrableOn_lowerTriangle_det_rpow_mul_exp_neg_trace {p : ℕ} {a : ℝ} (ha : 0 < p → (↑p - 1) / 2 < a) : MeasureTheory.IntegrableOn (fun (x : lowerTriangle p → ℝ) => ((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).det ^ (a - (↑p + 1) / 2) * Real.exp (-((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).trace) * (2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i))) (posDiagLowerRegion p) MeasureTheory.volume

For ((p : ℝ) - 1) / 2 < a (a condition only in positive dimension), the Jacobian-weighted Wishart integrand (det (L * Lᵀ)) ^ (a - (p + 1) / 2) * exp (-trace (L * Lᵀ)) * (2 ^ p * ∏ i, (L i i) ^ (p - i)) is integrable over the region of lower-triangular coordinates with positive diagonal.