The chi-squared distribution

The chi-squared law with k degrees of freedom is the gamma law of shape k / 2 and rate 1 / 2. This file defines it for every real k, records its three parameter regimes, and transports the elementary theory of the gamma law across the bridge: the density, the cumulative distribution function, the mean k, the variance 2 * k, the exponential-moment domain Set.Iio (1 / 2), the moment- and cumulant-generating functions there, and the characteristic function. It also proves that the family is additive in its degrees of freedom.

The three regimes. Only 0 < k gives a gamma law. At k = 0 the shape would degenerate, and the law is defined to be Measure.dirac 0: that is the value forced by additivity, since a convolution unit must be a point mass at the origin, and it is the law of an empty sum of squared standard Gaussians. Below 0 there is no law at all, and the measure is 0. The boundary at k = 0 is singular with respect to Lebesgue measure, so it carries its own moment and transform formulas rather than a density.

Main definitions

• TauCeti.Probability.chiSquaredPDFReal — the real-valued candidate density formula, x ^ (k / 2 - 1) * exp (-x / 2) / (2 ^ (k / 2) * Γ (k / 2)) on [0, ∞), which is a probability density when 0 < k;
• TauCeti.Probability.chiSquaredPDF — its ℝ≥0∞-valued companion, which is a probability density when 0 < k;
• TauCeti.Probability.chiSquaredMeasure — the law.

Main results

• TauCeti.Probability.chiSquaredMeasure_eq_gammaMeasure — the bridge to the gamma law;
• TauCeti.Probability.isProbabilityMeasure_chiSquaredMeasure — it is a probability measure for every 0 ≤ k, the boundary k = 0 included;
• TauCeti.Probability.chiSquaredMeasure_eq_withDensity, TauCeti.Probability.hasPDF_of_hasLaw_chiSquaredMeasure and TauCeti.Probability.rnDeriv_chiSquaredMeasure — the density, as a withDensity presentation, a MeasureTheory.HasPDF bridge and a Radon–Nikodym derivative;
• TauCeti.Probability.measurable_chiSquaredMeasure — measurability in the degrees of freedom, so the family can be used as a kernel;
• TauCeti.Probability.cdf_chiSquaredMeasure_eq — the cdf is P (k / 2, x / 2);
• TauCeti.Probability.integral_id_chiSquaredMeasure and TauCeti.Probability.variance_id_chiSquaredMeasure — the mean k and the variance 2 * k;
• TauCeti.Probability.integrableExpSet_id_chiSquaredMeasure, TauCeti.Probability.mgf_id_chiSquaredMeasure and TauCeti.Probability.cgf_id_chiSquaredMeasure — for 0 < k the exponential moments exist exactly below 1 / 2; on that half-line the mgf is (1 - 2 * t) ^ (-(k / 2)) for every 0 ≤ k;
• TauCeti.Probability.charFun_chiSquaredMeasure — the characteristic function is (1 - 2 * I * t) ^ (-k / 2), for every real t;
• TauCeti.Probability.integral_id_chiSquaredMeasure_zero, TauCeti.Probability.variance_id_chiSquaredMeasure_zero and TauCeti.Probability.charFun_chiSquaredMeasure_zero — at the Dirac boundary k = 0 the mean and variance vanish and the characteristic function is identically 1;
• TauCeti.Probability.chiSquaredMeasure_conv_chiSquaredMeasure — degrees of freedom add under convolution;
• TauCeti.Probability.chiSquaredMeasure_two — two degrees of freedom give the exponential law of rate 1 / 2.

Implementation

Every positive-parameter statement is the gamma statement of shape k / 2 and rate 1 / 2, read through chiSquaredMeasure_eq_gammaMeasure; nothing is recomputed. The arithmetic that remains is the substitution r = 1 / 2 in the gamma formulas: it turns a / r into k, a / r ^ 2 into 2 * k, and (1 - t / r) ^ (-a) into (1 - 2 * t) ^ (-(k / 2)).

The density is stated in the textbook normalisation 2 ^ (k / 2) * Γ (k / 2) rather than as gammaPDFReal (k / 2) (1 / 2), and chiSquaredPDFReal_eq_gammaPDFReal identifies the two; the only content of that identification is (1 / 2) ^ (k / 2) = (2 ^ (k / 2))⁻¹.

The boundary k = 0 uses the Dirac formulas of TauCeti/Probability/Distributions/Dirac.lean together with Mathlib's ProbabilityTheory.mgf_dirac', ProbabilityTheory.variance_dirac and MeasureTheory.charFun_dirac. Its exponential-moment domain is all of ℝ, strictly larger than the positive-parameter domain Set.Iio (1 / 2), which is why the two regimes cannot share a statement.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 3, the Chi-squared target, together with the chi-squared case of items 1–4 of "What every distribution must provide", and the completion check chiSquaredMeasure 2 = expMeasure (1 / 2).
• Formal declaration scaffold: TauCetiRoadmap/StandardDistributions/Suggested.lean, Layer 3.
• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley (1994), ch. 18.

The density

noncomputable def TauCeti.Probability.chiSquaredPDFReal (k x : ℝ) : ℝ

The candidate density formula for the chi-squared law with k degrees of freedom, in the textbook normalisation: x ^ (k / 2 - 1) * exp (-x / 2) / (2 ^ (k / 2) * Γ (k / 2)) on the nonnegative half-line, and 0 below it. It is a probability density when 0 < k.

noncomputable def TauCeti.Probability.chiSquaredPDF (k x : ℝ) : ENNReal

The ℝ≥0∞-valued companion to chiSquaredPDFReal. It is a probability density when 0 < k.

theorem TauCeti.Probability.chiSquaredPDF_eq_ofReal (k x : ℝ) : chiSquaredPDF k x = ENNReal.ofReal (chiSquaredPDFReal k x)

The extended candidate density is obtained from its real companion.

@[simp]

theorem TauCeti.Probability.chiSquaredPDFReal_of_nonneg {k x : ℝ} (hx : 0 ≤ x) : chiSquaredPDFReal k x = x ^ (k / 2 - 1) * Real.exp (-x / 2) / (2 ^ (k / 2) * Real.Gamma (k / 2))

On the nonnegative half-line, the candidate real-valued chi-squared density is given by its textbook formula.

@[simp]

theorem TauCeti.Probability.chiSquaredPDFReal_of_neg {k x : ℝ} (hx : x < 0) : chiSquaredPDFReal k x = 0

Below zero, the candidate real-valued chi-squared density vanishes.

@[simp]

theorem TauCeti.Probability.chiSquaredPDF_of_nonneg {k x : ℝ} (hx : 0 ≤ x) : chiSquaredPDF k x = ENNReal.ofReal (x ^ (k / 2 - 1) * Real.exp (-x / 2) / (2 ^ (k / 2) * Real.Gamma (k / 2)))

On the nonnegative half-line, the ℝ≥0∞-valued candidate chi-squared density is given by its textbook formula.

@[simp]

theorem TauCeti.Probability.chiSquaredPDF_of_neg {k x : ℝ} (hx : x < 0) : chiSquaredPDF k x = 0

Below zero, the ℝ≥0∞-valued candidate chi-squared density vanishes.

@[simp]

theorem TauCeti.Probability.chiSquaredPDFReal_zero_degree : chiSquaredPDFReal 0 = 0

At zero degrees of freedom the real candidate density vanishes identically.

@[simp]

theorem TauCeti.Probability.chiSquaredPDF_zero_degree : chiSquaredPDF 0 = 0

At zero degrees of freedom the extended candidate density vanishes identically.

theorem TauCeti.Probability.chiSquaredPDFReal_eq_gammaPDFReal (k x : ℝ) : chiSquaredPDFReal k x = ProbabilityTheory.gammaPDFReal (k / 2) (1 / 2) x

The chi-squared density is the gamma density of shape k / 2 and rate 1 / 2.

theorem TauCeti.Probability.chiSquaredPDF_eq_gammaPDF (k x : ℝ) : chiSquaredPDF k x = ProbabilityTheory.gammaPDF (k / 2) (1 / 2) x

The ℝ≥0∞-valued chi-squared density is the gamma density of shape k / 2 and rate 1 / 2.

theorem TauCeti.Probability.chiSquaredPDFReal_nonneg {k : ℝ} (hk : 0 ≤ k) (x : ℝ) : 0 ≤ chiSquaredPDFReal k x

The chi-squared density is nonnegative for nonnegative degrees of freedom.

theorem TauCeti.Probability.measurable_chiSquaredPDFReal (k : ℝ) : Measurable (chiSquaredPDFReal k)

The real-valued chi-squared density is measurable.

theorem TauCeti.Probability.measurable_chiSquaredPDF (k : ℝ) : Measurable (chiSquaredPDF k)

The chi-squared density is measurable.

The measure and its three regimes

noncomputable def TauCeti.Probability.chiSquaredMeasure (k : ℝ) : MeasureTheory.Measure ℝ

The chi-squared law with k degrees of freedom: the gamma law of shape k / 2 and rate 1 / 2 for 0 < k, the point mass at the origin for k = 0, and the zero measure for k < 0.

theorem TauCeti.Probability.chiSquaredMeasure_eq_gammaMeasure {k : ℝ} (hk : 0 < k) : chiSquaredMeasure k = ProbabilityTheory.gammaMeasure (k / 2) (1 / 2)

For positive degrees of freedom the chi-squared law is a gamma law.

@[simp]

theorem TauCeti.Probability.chiSquaredMeasure_zero : chiSquaredMeasure 0 = MeasureTheory.Measure.dirac 0

At zero degrees of freedom the chi-squared law is the point mass at the origin.

@[simp]

theorem TauCeti.Probability.chiSquaredMeasure_of_neg {k : ℝ} (hk : k < 0) : chiSquaredMeasure k = 0

There is no chi-squared law with negative degrees of freedom: the measure is zero.

theorem TauCeti.Probability.isProbabilityMeasure_chiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) : MeasureTheory.IsProbabilityMeasure (chiSquaredMeasure k)

The chi-squared law is a probability measure for every nonnegative number of degrees of freedom, the boundary k = 0 included.

theorem TauCeti.Probability.nullSingletonClass_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : MeasureTheory.NullSingletonClass (chiSquaredMeasure k)

A chi-squared law of positive degree has no atoms.

@[simp]

theorem TauCeti.Probability.chiSquaredMeasure_singleton {k : ℝ} (hk : 0 < k) (x : ℝ) : (chiSquaredMeasure k) {x} = 0

A chi-squared law of positive degree gives zero mass to every singleton.

theorem TauCeti.Probability.ae_pos_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : ∀ᵐ (x : ℝ) ∂chiSquaredMeasure k, 0 < x

A chi-squared variable of positive degree is positive almost surely.

theorem TauCeti.Probability.ae_pos_sqrt_div_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : ∀ᵐ (x : ℝ) ∂chiSquaredMeasure k, 0 < √(x / k)

For a chi-squared variable V with k > 0 degrees of freedom, the normalized square root √(V / k), the denominator of Student-type ratios, is positive almost surely.

theorem TauCeti.Probability.ae_nonneg_chiSquaredMeasure (k : ℝ) : ∀ᵐ (x : ℝ) ∂chiSquaredMeasure k, 0 ≤ x

Every chi-squared measure is carried by the nonnegative half-line, including its Dirac and invalid zero-measure cases.

theorem TauCeti.Probability.chiSquaredMeasure_eq_withDensity {k : ℝ} (hk : 0 < k) : chiSquaredMeasure k = MeasureTheory.volume.withDensity (chiSquaredPDF k)

For positive degrees of freedom the chi-squared law has the chi-squared density with respect to Lebesgue measure.

theorem TauCeti.Probability.measurable_chiSquaredMeasure : Measurable fun (k : ℝ) => chiSquaredMeasure k

The chi-squared family is measurable in its degrees of freedom, so it can be used as a kernel.

Densities of random variables

theorem TauCeti.Probability.hasPDF_of_hasLaw_chiSquaredMeasure {k : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hk : 0 < k) (hX : ProbabilityTheory.HasLaw X (chiSquaredMeasure k) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A variable with a chi-squared law of positive degrees of freedom has a density.

theorem TauCeti.Probability.pdf_eq_chiSquaredPDF_of_hasLaw_chiSquaredMeasure {k : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hk : 0 < k) (hX : ProbabilityTheory.HasLaw X (chiSquaredMeasure k) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] chiSquaredPDF k

The density of a chi-squared law of positive degrees of freedom is chiSquaredPDF.

theorem TauCeti.Probability.rnDeriv_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : (chiSquaredMeasure k).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] chiSquaredPDF k

The Radon–Nikodym derivative of a chi-squared law of positive degrees of freedom is chiSquaredPDF.

The cumulative distribution function

@[simp]

theorem TauCeti.Probability.cdf_chiSquaredMeasure_eq {k : ℝ} (hk : 0 < k) (x : ℝ) : ↑(ProbabilityTheory.cdf (chiSquaredMeasure k)) x = regularizedGamma (k / 2) (x / 2)

The cumulative distribution function of a chi-squared law with positive degrees of freedom is the regularized lower incomplete gamma function P (k / 2, x / 2).

theorem TauCeti.Probability.cdf_chiSquaredMeasure_zero (x : ℝ) : ↑(ProbabilityTheory.cdf (chiSquaredMeasure 0)) x = if 0 ≤ x then 1 else 0

At zero degrees of freedom the cumulative distribution function is the unit step at the origin.

Moments

theorem TauCeti.Probability.integral_id_chiSquaredMeasure_zero : ∫ (x : ℝ), x ∂chiSquaredMeasure 0 = 0

At zero degrees of freedom the mean is 0.

theorem TauCeti.Probability.variance_id_chiSquaredMeasure_zero : ProbabilityTheory.variance id (chiSquaredMeasure 0) = 0

At zero degrees of freedom the variance is 0.

@[simp]

theorem TauCeti.Probability.integral_id_chiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) : ∫ (x : ℝ), x ∂chiSquaredMeasure k = k

The mean of a chi-squared law with nonnegative degrees of freedom is its number of degrees of freedom.

@[simp]

theorem TauCeti.Probability.variance_id_chiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) : ProbabilityTheory.variance id (chiSquaredMeasure k) = 2 * k

The variance of a chi-squared law with nonnegative degrees of freedom is twice its number of degrees of freedom.

@[simp]

theorem TauCeti.Probability.integrable_rpow_chiSquaredMeasure_iff {k : ℝ} (hk : 0 < k) (q : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ q) (chiSquaredMeasure k) ↔ -(k / 2) < q

A real power is integrable under a positive-degree chi-squared law exactly when its exponent is greater than minus half the number of degrees of freedom.

theorem TauCeti.Probability.integral_rpow_chiSquaredMeasure {k q : ℝ} (hk : 0 < k) (hq : -(k / 2) < q) : ∫ (x : ℝ), x ^ q ∂chiSquaredMeasure k = 2 ^ q * Real.Gamma (k / 2 + q) / Real.Gamma (k / 2)

The real-power moment of a positive-degree chi-squared law, on its exact integrability domain.

theorem TauCeti.Probability.integrable_prod_rpow_pi_chiSquaredMeasure_iff {ι : Type u_2} [Fintype ι] {k : ι → ℝ} (hk : ∀ (i : ι), 0 < k i) (q : ℝ) : MeasureTheory.Integrable (fun (x : ι → ℝ) => ∏ i : ι, x i ^ q) (MeasureTheory.Measure.pi fun (i : ι) => chiSquaredMeasure (k i)) ↔ ∀ (i : ι), -(k i / 2) < q

A product of real powers of independent positive-degree chi-squared coordinates is integrable exactly when the exponent is greater than minus half of every coordinate's degrees of freedom.

Exponential moments and transforms

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : ProbabilityTheory.integrableExpSet id (chiSquaredMeasure k) = Set.Iio (1 / 2)

The exponential moments of a chi-squared law with positive degrees of freedom are exactly those of rate t < 1 / 2.

@[simp]

theorem TauCeti.Probability.mgf_id_chiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) {t : ℝ} (ht : t < 2⁻¹) : ProbabilityTheory.mgf id (chiSquaredMeasure k) t = (1 - 2 * t) ^ (-(k / 2))

The moment-generating function of a chi-squared law with nonnegative degrees of freedom on the half-line t < 2⁻¹.

@[simp]

theorem TauCeti.Probability.cgf_id_chiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) {t : ℝ} (ht : t < 2⁻¹) : ProbabilityTheory.cgf id (chiSquaredMeasure k) t = -(k / 2) * Real.log (1 - 2 * t)

The cumulant-generating function of a chi-squared law with nonnegative degrees of freedom on the half-line t < 2⁻¹. It is the real logarithm of TauCeti.Probability.mgf_id_chiSquaredMeasure.

theorem TauCeti.Probability.charFun_chiSquaredMeasure_zero (t : ℝ) : MeasureTheory.charFun (chiSquaredMeasure 0) t = 1

At zero degrees of freedom the characteristic function is identically 1.

@[simp]

theorem TauCeti.Probability.charFun_chiSquaredMeasure {k : ℝ} (hk : 0 ≤ k) (t : ℝ) : MeasureTheory.charFun (chiSquaredMeasure k) t = (1 - 2 * Complex.I * ↑t) ^ (-↑k / 2)

The characteristic function of a chi-squared law with nonnegative degrees of freedom, at every real t. The base has real part 1, so the principal power does not meet the branch cut.

theorem TauCeti.Probability.integrableExpSet_id_chiSquaredMeasure_zero : ProbabilityTheory.integrableExpSet id (chiSquaredMeasure 0) = Set.univ

At zero degrees of freedom every exponential moment exists.

theorem TauCeti.Probability.mgf_id_chiSquaredMeasure_zero (t : ℝ) : ProbabilityTheory.mgf id (chiSquaredMeasure 0) t = 1

At zero degrees of freedom the moment-generating function is identically 1.

theorem TauCeti.Probability.cgf_id_chiSquaredMeasure_zero (t : ℝ) : ProbabilityTheory.cgf id (chiSquaredMeasure 0) t = 0

At zero degrees of freedom the cumulant-generating function is identically 0.

Additivity and the exponential law

theorem TauCeti.Probability.chiSquaredMeasure_conv_chiSquaredMeasure {k l : ℝ} (hk : 0 ≤ k) (hl : 0 ≤ l) : (chiSquaredMeasure k).conv (chiSquaredMeasure l) = chiSquaredMeasure (k + l)

Degrees of freedom add under convolution, including at the boundary k = 0, where the chi-squared law is the convolution unit.

theorem TauCeti.Probability.iIndepFun.hasLaw_sum_chiSquared {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {Y : ι → Ω → ℝ} {k : ι → ℝ} (hindep : ProbabilityTheory.iIndepFun Y P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (Y i) (chiSquaredMeasure (k i)) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => ∑ i : ι, Y i ω) (chiSquaredMeasure (∑ i : ι, k i)) P

A finite sum of independent chi-squared variables has the chi-squared law whose degrees of freedom are the sum of the individual degrees of freedom.

theorem TauCeti.Probability.chiSquaredMeasure_two : chiSquaredMeasure 2 = ProbabilityTheory.expMeasure (1 / 2)

Two degrees of freedom give the exponential law of rate 1 / 2.