Noncentral chi-squared laws as Poisson mixtures

The noncentral chi-squared law of degree k ≥ 0 and noncentrality l ≥ 0 mixes the central chi-squared laws of degrees k + 2 * n against Poisson weights of rate l / 2. Negative degrees give the zero measure. This construction includes the mixed degree-zero law: its atom at zero has mass exp (-l / 2), and the remaining components have positive degrees.

This file proves normalization, joint parameter measurability, the central specialization, the atomic decomposition at degree zero, and exact topological support. The Poisson series also supplies set-evaluation and nonnegative-integration formulas for subsequent calculations.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, second edition, Wiley, 1995, chapter 29.

noncomputable def TauCeti.Probability.noncentralChiSquaredMeasure (k : ℝ) (l : NNReal) : MeasureTheory.Measure ℝ

The noncentral chi-squared measure with real degree k and nonnegative noncentrality l. For nonnegative degree it is a Poisson mixture of central chi-squared laws; negative degree gives the zero measure.

theorem TauCeti.Probability.noncentralChiSquaredMeasure_of_nonneg {k : ℝ} (hk : 0 ≤ k) (l : NNReal) : noncentralChiSquaredMeasure k l = (ProbabilityTheory.poissonMeasure (l / 2)).bind fun (n : ℕ) => chiSquaredMeasure (k + 2 * ↑n)

The defining Poisson mixture at nonnegative degree.

@[simp]

theorem TauCeti.Probability.noncentralChiSquaredMeasure_of_neg {k : ℝ} (hk : k < 0) (l : NNReal) : noncentralChiSquaredMeasure k l = 0

Negative degrees give the zero measure, even at zero noncentrality.

theorem TauCeti.Probability.isProbabilityMeasure_noncentralChiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) (l : NNReal) : MeasureTheory.IsProbabilityMeasure (noncentralChiSquaredMeasure k l)

Every nonnegative degree and noncentrality gives a probability law, including degree zero.

theorem TauCeti.Probability.noncentralChiSquaredMeasure_eq_sum {k : ℝ} (hk : 0 ≤ k) (l : NNReal) : noncentralChiSquaredMeasure k l = MeasureTheory.Measure.sum fun (n : ℕ) => (ProbabilityTheory.poissonMeasure (l / 2)) {n} • chiSquaredMeasure (k + 2 * ↑n)

The Poisson-weighted sum presentation of a noncentral chi-squared law.

theorem TauCeti.Probability.noncentralChiSquaredMeasure_apply {k : ℝ} (hk : 0 ≤ k) (l : NNReal) (s : Set ℝ) : (noncentralChiSquaredMeasure k l) s = ∑' (n : ℕ), (ProbabilityTheory.poissonMeasure (l / 2)) {n} * (chiSquaredMeasure (k + 2 * ↑n)) s

Set evaluation as an extended-real Poisson series; the formula holds for every set.

theorem TauCeti.Probability.lintegral_noncentralChiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) (l : NNReal) (f : ℝ → ENNReal) : ∫⁻ (x : ℝ), f x ∂noncentralChiSquaredMeasure k l = ∑' (n : ℕ), (ProbabilityTheory.poissonMeasure (l / 2)) {n} * ∫⁻ (x : ℝ), f x ∂chiSquaredMeasure (k + 2 * ↑n)

Nonnegative integration can be performed component by component, without finiteness or integrability assumptions on the observable.

@[simp]

theorem TauCeti.Probability.noncentralChiSquaredMeasure_zero_noncentrality (k : ℝ) : noncentralChiSquaredMeasure k 0 = chiSquaredMeasure k

At zero noncentrality, the law is the central chi-squared law, including invalid degrees.

theorem TauCeti.Probability.measurable_noncentralChiSquaredMeasure : Measurable fun (p : ℝ × NNReal) => noncentralChiSquaredMeasure p.1 p.2

The full totalized family is jointly measurable in degree and noncentrality.

theorem TauCeti.Probability.ae_nonneg_noncentralChiSquaredMeasure (k : ℝ) (l : NNReal) : ∀ᵐ (x : ℝ) ∂noncentralChiSquaredMeasure k l, 0 ≤ x

A noncentral chi-squared variable is nonnegative almost surely.

theorem TauCeti.Probability.ae_pos_noncentralChiSquaredMeasure {k : ℝ} (hk : 0 < k) (l : NNReal) : ∀ᵐ (x : ℝ) ∂noncentralChiSquaredMeasure k l, 0 < x

Positive degree makes a noncentral chi-squared variable strictly positive almost surely.

theorem TauCeti.Probability.nullSingletonClass_noncentralChiSquaredMeasure {k : ℝ} (hk : 0 < k) (l : NNReal) : MeasureTheory.NullSingletonClass (noncentralChiSquaredMeasure k l)

At positive degree the noncentral law has no atoms.

theorem TauCeti.Probability.noncentralChiSquaredMeasure_zero_degree (l : NNReal) : noncentralChiSquaredMeasure 0 l = ENNReal.ofReal (Real.exp (-↑l / 2)) • MeasureTheory.Measure.dirac 0 + MeasureTheory.Measure.sum fun (n : ℕ) => (ProbabilityTheory.poissonMeasure (l / 2)) {n + 1} • chiSquaredMeasure (2 * (↑n + 1))

At degree zero, the Poisson count zero contributes the atom and every positive count contributes a positive-degree central law.

@[simp]

theorem TauCeti.Probability.noncentralChiSquaredMeasure_zero_degree_mass (l : NNReal) : (noncentralChiSquaredMeasure 0 l) {0} = ENNReal.ofReal (Real.exp (-↑l / 2))

The atom of the degree-zero law has mass exp (-l / 2), including mass one at l = 0.

@[simp]

theorem TauCeti.Probability.noncentralChiSquaredMeasure_singleton_of_ne_zero {x : ℝ} (hx : x ≠ 0) (k : ℝ) (l : NNReal) : (noncentralChiSquaredMeasure k l) {x} = 0

Zero is the only possible atom, for every degree and noncentrality.

theorem TauCeti.Probability.exists_smul_chiSquaredMeasure_le_noncentralChiSquaredMeasure {k : ℝ} {l : NNReal} (hk : 0 ≤ k) (hne : k ≠ 0 ∨ l ≠ 0) : ∃ (n : ℕ), 0 < k + 2 * ↑n ∧ (ProbabilityTheory.poissonMeasure (l / 2)) {n} ≠ 0 ∧ (ProbabilityTheory.poissonMeasure (l / 2)) {n} • chiSquaredMeasure (k + 2 * ↑n) ≤ noncentralChiSquaredMeasure k l

Every valid law other than the double-zero Dirac law dominates a positive-weight central chi-squared component of positive degree.

@[simp]

theorem TauCeti.Probability.support_noncentralChiSquaredMeasure (k : ℝ) (l : NNReal) : (noncentralChiSquaredMeasure k l).support = if k < 0 then ∅ else if k = 0 ∧ l = 0 then {0} else Set.Ici 0

The support is empty for negative degree, the singleton zero at zero degree and noncentrality, and [0, ∞) in every other valid case.