The multivariate Gamma function as a cone integral

The multivariate Gamma function TauCeti.multivariateGamma p a is the value of the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace A) over the cone of positive-definite symmetric p × p matrices, taken against TauCeti.symmetricLebesgue p. This file proves that identity, for (p - 1) / 2 < a in every dimension and for every a in dimension zero, where the cone is a single point and both sides are 1. It also computes how the integral depends on a scale matrix: weighting the exponential by an inverse positive-definite scale T, so that the integrand becomes (det A) ^ (a - (p + 1) / 2) * exp (-trace (T⁻¹ * A)), multiplies the integral by (det T) ^ a.

The normalization of the reference measure is part of these identities, not a convention that can be changed afterwards, which is why this file, unlike the elementary theory of multivariateGamma, depends on the measure theory of the symmetric matrices: the same integral against a differently scaled reference measure has a different value, and it is this one that the Wishart normalizing constant uses.

The unscaled integral is the Cholesky change of variables, which turns the cone integral into the integral over the positive-diagonal lower-triangular coordinates, where the integrand factorizes into one-dimensional Gamma and Gaussian integrals. Both the lower-integral and the Bochner form are recorded, together with the integrability of the integrand on the cone: a density defined by MeasureTheory.Measure.withDensity is normalized by the first and integrated against by the others.

The scale identity is a congruence change of variables: writing T = C * Cᵀ, the map A ↦ C * A * Cᵀ preserves the cone, carries the plain exponential weight to the weighted one, and contributes the Jacobian |det C| ^ (p + 1); the two determinant powers combine to (det T) ^ a. It is proved for every real a, with no convergence hypothesis on either side. Together with the unscaled integral it fixes the normalizing constant of a Wishart density with scale matrix S, whose exponential weight is exp (-trace (S⁻¹ * A) / 2) and hence has scale 2 • S.

Main results

• TauCeti.integral_posDef_multivariateGamma — the cone integral;
• TauCeti.lintegral_posDef_multivariateGamma — its lower-integral form;
• TauCeti.integrableOn_posDef_det_rpow_mul_exp_neg_trace — integrability on the cone;
• TauCeti.integral_posDef_multivariateGamma_zero — the cone integral in dimension zero, where no hypothesis on the shape parameter is needed;
• Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul and Matrix.PosDef.integral_det_rpow_mul_exp_neg_trace_inv_mul — an inverse positive-definite scale T in the exponential weight multiplies the cone integral by (det T) ^ a;
• Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul_div_two and Matrix.PosDef.integral_det_rpow_mul_exp_neg_trace_inv_mul_div_two — the same statement in the halved form exp (-trace (S⁻¹ * A) / 2) used by the Wishart densities, where the factor is 2 ^ (p * a) * (det S) ^ a;
• Matrix.PosDef.integrableOn_posDef_det_rpow_mul_exp_neg_trace_mul — integrability on the cone of the integrand weighted by an arbitrary positive-definite B.

References

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

theorem TauCeti.integral_posDef_multivariateGamma_zero (a : ℝ) : ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 0) (Fin 0) ℝ)) | (↑A).PosDef}, (↑A).det ^ (a - 1 / 2) * Real.exp (-(↑A).trace) ∂symmetricLebesgue 0 = multivariateGamma 0 a

The cone integral that characterizes Γ_p, in dimension zero: the symmetric 0 × 0 matrices form a single point, which is positive definite and has determinant 1 and trace 0, and symmetricLebesgue 0 is the Dirac measure there. Both sides are 1, so unlike the positive-dimensional identity this one needs no hypothesis on the shape parameter.

theorem TauCeti.lintegral_posDef_multivariateGamma {p : ℕ} {a : ℝ} (ha : (↑p - 1) / 2 < a) : ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, ENNReal.ofReal ((↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace)) ∂symmetricLebesgue p = ENNReal.ofReal (multivariateGamma p a)

The multivariate Gamma integral, in lower-integral form: the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace A) over the positive-definite cone against TauCeti.symmetricLebesgue p is Γ_p(a). This is the form that normalizes a density defined by MeasureTheory.Measure.withDensity.

theorem TauCeti.integrableOn_posDef_det_rpow_mul_exp_neg_trace {p : ℕ} {a : ℝ} (ha : (↑p - 1) / 2 < a) : MeasureTheory.IntegrableOn (fun (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace)) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef} (symmetricLebesgue p)

For ((p : ℝ) - 1) / 2 < a the integrand (det A) ^ (a - (p + 1) / 2) * exp (-trace A) is integrable over the positive-definite cone against TauCeti.symmetricLebesgue p.

theorem TauCeti.integral_posDef_multivariateGamma {p : ℕ} {a : ℝ} (ha : (↑p - 1) / 2 < a) : ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace) ∂symmetricLebesgue p = multivariateGamma p a

The multivariate Gamma integral. For ((p : ℝ) - 1) / 2 < a, the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace A) over the cone of positive-definite symmetric p × p matrices, against TauCeti.symmetricLebesgue p, is Γ_p(a).

The scale matrix in the cone integral

theorem Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul {p : ℕ} {T : Matrix (Fin p) (Fin p) ℝ} (hT : T.PosDef) (a : ℝ) : ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, ENNReal.ofReal ((↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(T⁻¹ * ↑A).trace)) ∂TauCeti.symmetricLebesgue p = ENNReal.ofReal (T.det ^ a) * ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, ENNReal.ofReal ((↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace)) ∂TauCeti.symmetricLebesgue p

The scale matrix in the cone integral. For a positive-definite T, weighting the exponential in the cone integral by the inverse scale T⁻¹ multiplies the integral by (det T) ^ a. Lower integration is defined for every real a, so the identity carries no convergence hypothesis.

theorem Matrix.PosDef.integral_det_rpow_mul_exp_neg_trace_inv_mul {p : ℕ} {T : Matrix (Fin p) (Fin p) ℝ} (hT : T.PosDef) (a : ℝ) : ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(T⁻¹ * ↑A).trace) ∂TauCeti.symmetricLebesgue p = T.det ^ a * ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace) ∂TauCeti.symmetricLebesgue p

The Bochner form of Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul: an inverse positive-definite scale T in the exponential weight multiplies the cone integral by (det T) ^ a.

theorem Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul_div_two {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (a : ℝ) : ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, ENNReal.ofReal ((↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(S⁻¹ * ↑A).trace / 2)) ∂TauCeti.symmetricLebesgue p = ENNReal.ofReal (2 ^ (↑p * a) * S.det ^ a) * ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, ENNReal.ofReal ((↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace)) ∂TauCeti.symmetricLebesgue p

The halved form of Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul used by the Wishart densities, whose exponential weight is exp (-trace (S⁻¹ * A) / 2): the scale is then 2 • S and the factor is 2 ^ (p * a) * (det S) ^ a.

theorem Matrix.PosDef.integral_det_rpow_mul_exp_neg_trace_inv_mul_div_two {p : ℕ} {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (a : ℝ) : ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(S⁻¹ * ↑A).trace / 2) ∂TauCeti.symmetricLebesgue p = 2 ^ (↑p * a) * S.det ^ a * ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace) ∂TauCeti.symmetricLebesgue p

The Bochner form of Matrix.PosDef.lintegral_det_rpow_mul_exp_neg_trace_inv_mul_div_two.

theorem Matrix.PosDef.integrableOn_posDef_det_rpow_mul_exp_neg_trace_mul {p : ℕ} {B : Matrix (Fin p) (Fin p) ℝ} {a : ℝ} (hB : B.PosDef) (ha : (↑p - 1) / 2 < a) : MeasureTheory.IntegrableOn (fun (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(B * ↑A).trace)) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef} (TauCeti.symmetricLebesgue p)

With a positive-definite weight B in the exponential term, the cone integrand is still integrable in the classical range of the shape parameter; this is the converse of TauCeti.not_integrableOn_posDef_det_rpow_mul_exp_neg_trace_mul. Weighting by B amounts to the scale B⁻¹, so the integral is finite for the same reason the unweighted one is.