AcceptedProposition · Statement with omitted proof

Exact positive and negative chi-square moments

Gamma-function identities give positive and negative moments of a chi-square variable.

Halko, Martinsson & Tropp ↗
Source label: prop:chisq-moment-exact

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Gamma-function identities give positive and negative moments of a chi-square variable.

\mathbb E\Xi^q=\frac{2^q\Gamma(k/2+q)}{\Gamma(k/2)},\qquad \mathbb E\Xi^{-q}=\frac{\Gamma(k/2-q)}{2^q\Gamma(k/2)}

Assumptions & context

Ξ has k degrees of freedom and 0 ≤ q < k/2.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:chisq-moment-exact

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem chisq_moment_exact {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (k : ℕ) (Xi : Ω → ℝ)
    (hXi : ProbabilityTheory.HasLaw Xi
      (ProbabilityTheory.gammaMeasure ((k : ℝ) / 2) (1 / 2)) P)
    (q : ℝ) (hq0 : 0 ≤ q) (hqk : q < (k : ℝ) / 2) :
    (∫ ω, Xi ω ^ q ∂P) =
        (2 : ℝ) ^ q * Real.Gamma ((k : ℝ) / 2 + q) / Real.Gamma ((k : ℝ) / 2) ∧
    (∫ ω, Xi ω ^ (-q) ∂P) =
        Real.Gamma ((k : ℝ) / 2 - q) / ((2 : ℝ) ^ q * Real.Gamma ((k : ℝ) / 2)) := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.HMT2011.ChisqMomentExact

/-- HMT (prop:chisq-moment-exact). Let `Ξ` be a `χ²` variate with `k` degrees of freedom.
The chi-square law with `k` degrees of freedom is the Gamma law with shape `k/2` and rate
`1/2`, i.e. `ProbabilityTheory.gammaMeasure (k/2) (1/2)`. When `0 ≤ q < k/2`,
`E(Ξ^q) = 2^q Γ(k/2+q) / Γ(k/2)` and `E(Ξ^{-q}) = Γ(k/2-q) / (2^q Γ(k/2))`.
Powers are real powers (`Real.rpow`); `Ξ` is almost surely positive under this law.
Expectation is the Bochner integral against the sample measure `P`. -/
theorem chisq_moment_exact {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (k : ℕ) (Xi : Ω → ℝ)
    (hXi : ProbabilityTheory.HasLaw Xi
      (ProbabilityTheory.gammaMeasure ((k : ℝ) / 2) (1 / 2)) P)
    (q : ℝ) (hq0 : 0 ≤ q) (hqk : q < (k : ℝ) / 2) :
    (∫ ω, Xi ω ^ q ∂P) =
        (2 : ℝ) ^ q * Real.Gamma ((k : ℝ) / 2 + q) / Real.Gamma ((k : ℝ) / 2) ∧
    (∫ ω, Xi ω ^ (-q) ∂P) =
        Real.Gamma ((k : ℝ) / 2 - q) / ((2 : ℝ) ^ q * Real.Gamma ((k : ℝ) / 2)) := by
  sorry

end RNLAPhaseB.HMT2011.ChisqMomentExact

How to read the formalization

The common range ensures the stated inverse moment is within its admissible regime; both identities are retained.

← Back to all statements