Divergence of the Wishart cone integral off the positive-definite cone

Consider the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace (B * A)) over the cone of positive-definite symmetric p × p matrices. For the identity weight B = 1 and (p - 1) / 2 < a, its value is the multivariate Gamma function (TauCeti.integral_posDef_multivariateGamma). This file treats the opposite situation: when the symmetric weight B is not positive definite, the integral is infinite, and the integrand is not integrable on the cone.

This is the necessary direction for the domain on which a trace statistic of a Wishart density has finite exponential moments: tilting the density exp (-trace (S⁻¹ * A) / 2) by exp (t * trace (Θ * A)) produces the weight B = S⁻¹ / 2 - t • Θ, and the moment is infinite whenever that weight is not positive definite. The sufficient direction, finiteness for an arbitrary positive-definite weight, is not proved here.

The proof uses a direction v with v ⬝ᵥ B *ᵥ v ≤ 0, along which the weight does not decay. Translating a small closed ball K inside the cone by the multiples k • v vᵀ, k : ℕ, gives pairwise disjoint subsets of the cone, since adding a positive-semidefinite matrix preserves positive definiteness. By translation invariance of TauCeti.symmetricLebesgue, the integral over the k-th translate is the integral over K of the translated integrand. On K the exponential factor stays bounded below, because trace (B * (A + k • v vᵀ)) = trace (B * A) + k * (v ⬝ᵥ B *ᵥ v), and the determinant det A * (1 + k * (v ⬝ᵥ A⁻¹ *ᵥ v)) grows at most linearly in k. Since the exponent a - (p + 1) / 2 is at least -1, the translates contribute a multiple of the harmonic series.

Main results

• TauCeti.lintegral_posDef_det_rpow_mul_exp_neg_trace_mul_eq_top_of_dotProduct_mulVec_nonpos — the integral is infinite as soon as some nonzero v has v ⬝ᵥ B *ᵥ v ≤ 0;
• TauCeti.lintegral_posDef_det_rpow_mul_exp_neg_trace_mul_eq_top — the integral is infinite for every symmetric weight that is not positive definite;
• TauCeti.not_integrableOn_posDef_det_rpow_mul_exp_neg_trace_mul — the corresponding non-integrability statement.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, Section 2.1 and Theorem 3.2.3.

theorem TauCeti.lintegral_posDef_det_rpow_mul_exp_neg_trace_mul_eq_top_of_dotProduct_mulVec_nonpos {p : ℕ} {a : ℝ} {B : Matrix (Fin p) (Fin p) ℝ} {v : Fin p → ℝ} (hv : v ≠ 0) (hvB : v ⬝ᵥ B.mulVec v ≤ 0) (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 (-(B * ↑A).trace)) ∂symmetricLebesgue p = ⊤

The Wishart cone integral diverges along a non-decaying direction. If a nonzero vector v satisfies v ⬝ᵥ B *ᵥ v ≤ 0 and (p - 1) / 2 ≤ a, then the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace (B * A)) over the positive-definite cone against TauCeti.symmetricLebesgue p is infinite.

theorem TauCeti.lintegral_posDef_det_rpow_mul_exp_neg_trace_mul_eq_top {p : ℕ} {a : ℝ} {B : Matrix (Fin p) (Fin p) ℝ} (hB : B.IsHermitian) (hBpd : ¬B.PosDef) (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 (-(B * ↑A).trace)) ∂symmetricLebesgue p = ⊤

The Wishart cone integral diverges off the positive-definite cone. For a symmetric weight B that is not positive definite and (p - 1) / 2 ≤ a, the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace (B * A)) over the positive-definite cone against TauCeti.symmetricLebesgue p is infinite.

theorem TauCeti.not_integrableOn_posDef_det_rpow_mul_exp_neg_trace_mul {p : ℕ} {a : ℝ} {B : Matrix (Fin p) (Fin p) ℝ} (hB : B.IsHermitian) (hBpd : ¬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} (symmetricLebesgue p)

For a symmetric weight B that is not positive definite and (p - 1) / 2 ≤ a, the integrand (det A) ^ (a - (p + 1) / 2) * exp (-trace (B * A)) is not integrable over the positive-definite cone against TauCeti.symmetricLebesgue p.