The multivariate Gamma function

The multivariate Gamma function of dimension p is

Γ_p(a) = π ^ (p * (p - 1) / 4) * ∏_{i < p} Γ(a - i / 2).

It is the normalizing constant of the Wishart density, because for (p - 1) / 2 < a it is 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. That integral identity is the subject of TauCeti/Analysis/SpecialFunctions/MultivariateGamma/Integral.lean, which proves its dimension-zero case and is where the symmetric-matrix measure theory enters.

The exponent of π is real, not the truncated natural-number quotient p * (p - 1) / 4, and so is the shift i / 2 in each Gamma factor; Γ_p interpolates the classical constants in half steps. Outside the range (p - 1) / 2 < a the definition still makes sense and takes the value 0 exactly when some factor sits at a pole of Γ (TauCeti.multivariateGamma_eq_zero_iff), which is the behaviour the totalized Wishart laws inherit.

Main definitions

• TauCeti.multivariateGamma — the multivariate Gamma function.

Main results

• TauCeti.multivariateGamma_add — the dimensions add, Γ_{p + q}(a) = π ^ (p * q / 2) * Γ_p(a) * Γ_q(a - p / 2), with the classical one-step recursion TauCeti.multivariateGamma_succ as a special case;
• TauCeti.multivariateGamma_eq_prod — Γ_p(a) as a product of one factor π ^ (i / 2) * Γ(a - i / 2) per row;
• TauCeti.multivariateGamma_one — dimension one recovers Real.Gamma;
• TauCeti.multivariateGamma_pos — positivity on the classical range (p - 1) / 2 < a;
• TauCeti.multivariateGamma_eq_zero_iff — the vanishing locus outside that range;
• TauCeti.measurable_multivariateGamma — measurability in the parameter, as the parameter measurability of the Wishart laws needs.

References

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

noncomputable def TauCeti.multivariateGamma (p : ℕ) (a : ℝ) : ℝ

The multivariate Gamma function of dimension p, Γ_p(a) = π ^ (p * (p - 1) / 4) * ∏_{i < p} Γ(a - i / 2). Both the exponent of π and the shifts of the Gamma factors are real, so this is not the truncated natural-number quotient.

Equations

• TauCeti.multivariateGamma p a = Real.pi ^ (↑p * (↑p - 1) / 4) * ∏ i : Fin p, Real.Gamma (a - ↑↑i / 2)

theorem TauCeti.multivariateGamma_def (p : ℕ) (a : ℝ) : multivariateGamma p a = Real.pi ^ (↑p * (↑p - 1) / 4) * ∏ i : Fin p, Real.Gamma (a - ↑↑i / 2)

The defining formula of the multivariate Gamma function.

@[simp]

theorem TauCeti.multivariateGamma_zero (a : ℝ) : multivariateGamma 0 a = 1

In dimension zero there are no Gamma factors and the constant is 1.

@[simp]

theorem TauCeti.multivariateGamma_one (a : ℝ) : multivariateGamma 1 a = Real.Gamma a

In dimension one the multivariate Gamma function is Euler's.

theorem TauCeti.multivariateGamma_add (p q : ℕ) (a : ℝ) : multivariateGamma (p + q) a = Real.pi ^ (↑p * ↑q / 2) * multivariateGamma p a * multivariateGamma q (a - ↑p / 2)

Splitting the dimension: the first p Gamma factors assemble into Γ_p(a) and the last q into Γ_q(a - p / 2), at the cost of the cross term π ^ (p * q / 2) in the exponent.

theorem TauCeti.multivariateGamma_succ (p : ℕ) (a : ℝ) : multivariateGamma (p + 1) a = Real.pi ^ (↑p / 2) * multivariateGamma p a * Real.Gamma (a - ↑p / 2)

The classical one-step recursion of the multivariate Gamma function.

theorem TauCeti.multivariateGamma_eq_prod (p : ℕ) (a : ℝ) : multivariateGamma p a = ∏ i : Fin p, Real.pi ^ (↑↑i / 2) * Real.Gamma (a - ↑↑i / 2)

The multivariate Gamma function as a product over its rows: row i contributes the Gamma factor Γ(a - i / 2) together with the share π ^ (i / 2) of the power of π.

theorem TauCeti.multivariateGamma_pos {p : ℕ} {a : ℝ} (ha : (↑p - 1) / 2 < a) : 0 < multivariateGamma p a

On the classical range of the shape parameter every Gamma factor is evaluated to the right of its rightmost pole, so Γ_p(a) is positive. This is the range on which it normalizes a Wishart density.

theorem TauCeti.multivariateGamma_ne_zero {p : ℕ} {a : ℝ} (ha : (↑p - 1) / 2 < a) : multivariateGamma p a ≠ 0

Γ_p does not vanish on the classical range of its shape parameter.

theorem TauCeti.multivariateGamma_eq_zero_iff (p : ℕ) (a : ℝ) : multivariateGamma p a = 0 ↔ ∃ (i : Fin p) (m : ℕ), a - ↑↑i / 2 = -↑m

Off the classical range, Γ_p(a) vanishes exactly when one of its Gamma factors sits at a pole, that is, when a - i / 2 is a nonpositive integer for some i < p.

theorem TauCeti.measurable_multivariateGamma (p : ℕ) : Measurable (multivariateGamma p)

Γ_p is Borel measurable in its shape parameter, including at the poles of its factors. The Wishart laws need this to be measurable in their degree parameter.