Chi-square distribution
DefinitionChi-square distribution#✓fully proved
For a natural number \(p\), the chi-square law with \(p\) degrees of freedom is the gamma law on \(\mathbb{R}\) with shape \(p/2\) and rate \(1/2\) (equivalently, scale \(2\)): the measure with density \(x \mapsto \frac{(1/2)^{p/2}}{\Gamma(p/2)} x^{p/2 - 1} e^{-x/2}\) for \(x > 0\) and \(0\) for \(x < 0\) with respect to Lebesgue measure.
For \(p = 0\) the definition is degenerate: \(\Gamma(0)\) is taken to be \(0\) and division by \(0\) gives \(0\), so the density vanishes and the measure is the zero measure rather than a point mass.
noncomputable def chiSquareMeasure (p : ℕ) : Measure ℝ :=
gammaMeasure ((p : ℝ) / 2) (1 / 2)Used by 21
χ²₁ when the reference LD is right · The square of a standard normal variable is chi-square with one degree of freedom · Exponential moments of the chi-square distribution · Moment generating function of the chi-square distribution · Chi-square moment generating functions multiply by adding degrees · Cochran (1954) · Fisher's method for combining p-values · Law of the positive part squared of a standard normal variable · Squared normalized Gaussian is chi-square with one degree of freedom · Rao's score test, known information · Rao's score test with an estimated information · Wilks' theorem, supremum form · Wilks' theorem (simple null) · Likelihood ratio on the boundary · Wald's test · Wald's test with an estimated information · Cochran's theorem · Sum of squares of independent standard normals is chi-square · Cochran's theorem · Squared orthonormal coordinates of a standard Gaussian are chi-square · Student's t lawTheoremMoment generating function of the square of a standard normal#✓fully proved
Let \(\gamma\) be the standard Gaussian measure on \(\mathbb{R}\) (mean \(0\), variance \(1\)). For every real \(t\), \(\int_{\mathbb{R}} e^{t x^2} \, d\gamma(x) = 1/\sqrt{1 - 2t}\).
For \(t \ge 1/2\) the integral diverges; the identity still holds there with the conventions that the integral of a non-integrable function is \(0\), that \(\sqrt{s} = 0\) for \(s \le 0\) and that \(1/0 = 0\), which make both sides \(0\).
theorem mgf_sq_stdGaussian (t : ℝ) :
mgf (fun x : ℝ => x ^ 2) (gaussianReal 0 1) t =
(Real.sqrt (1 - 2 * t))⁻¹TheoremExponential moments of the square of a standard normal#✓fully proved
Let \(\gamma\) be the standard Gaussian measure on \(\mathbb{R}\) (mean \(0\), variance \(1\)). For every real \(t < 1/2\), the function \(x \mapsto e^{t x^2}\) is integrable with respect to \(\gamma\).
theorem integrable_exp_mul_sq_stdGaussian {t : ℝ} (ht : t < 1 / 2) :
Integrable (fun x : ℝ => Real.exp (t * x ^ 2)) (gaussianReal 0 1)TheoremExponential moments of the law of the square of a standard normal#✓fully proved
Let \(\gamma\) be the standard Gaussian measure on \(\mathbb{R}\) (mean \(0\), variance \(1\)) and let \(\nu\) be its image under \(x \mapsto x^2\). For every real \(t < 1/2\), the function \(y \mapsto e^{t y}\) is integrable with respect to \(\nu\).
theorem Iio_subset_integrableExpSet_map_sq_stdGaussian :
Iio (1 / 2 : ℝ) ⊆
integrableExpSet id ((gaussianReal 0 1).map fun x : ℝ => x ^ 2)Uses 1 · Used by 1
TheoremMoment generating function of the law of the square of a standard normal#✓fully proved
Let \(\gamma\) be the standard Gaussian measure on \(\mathbb{R}\) (mean \(0\), variance \(1\)) and let \(\nu\) be its image under \(x \mapsto x^2\). For every real \(t\), \(\int_{\mathbb{R}} e^{t y} \, d\nu(y) = 1/\sqrt{1 - 2t}\).
For \(t \ge 1/2\) the integral diverges; the identity still holds there with the conventions that the integral of a non-integrable function is \(0\), that \(\sqrt{s} = 0\) for \(s \le 0\) and that \(1/0 = 0\), which make both sides \(0\).
theorem mgf_id_map_sq_stdGaussian (t : ℝ) :
mgf id ((gaussianReal 0 1).map fun x : ℝ => x ^ 2) t =
(Real.sqrt (1 - 2 * t))⁻¹Uses 1 · Used by 1
TheoremMoment generating function of the gamma law with shape and rate one half#✓fully proved
Let \(\mu\) be the gamma law on \(\mathbb{R}\) with shape \(1/2\) and rate \(1/2\). For every real \(t < 1/2\), \(\int_{\mathbb{R}} e^{t x} \, d\mu(x) = 1/\sqrt{1 - 2t}\).
This is the moment generating function of the square of a standard normal variable.
theorem mgf_gammaMeasure_half_half_eq_sqrt {t : ℝ} (ht : t < 1 / 2) :
mgf id (gammaMeasure (1 / 2) (1 / 2)) t =
(Real.sqrt (1 - 2 * t))⁻¹Uses 1 · Used by 1
TheoremMoment generating function of the chi-square distribution#✓fully proved
Let \(p\) be a positive integer and let \(\chi^2_p\) be the chi-square law with \(p\) degrees of freedom. For every real \(t < 1/2\), \(\int_{\mathbb{R}} e^{t x} \, d\chi^2_p(x) = \left(\frac{1/2}{1/2 - t}\right)^{p/2}\).
theorem mgf_chiSquareMeasure_of_lt {p : ℕ} (hp : 0 < p) {t : ℝ}
(ht : t < 1 / 2) :
mgf id (chiSquareMeasure p) t
= ((1 / 2 : ℝ) / (1 / 2 - t)) ^ ((p : ℝ) / 2)noncomputable def chiSquareMeasure (p : ℕ) : Measure ℝ :=
gammaMeasure ((p : ℝ) / 2) (1 / 2)MathlibExt/Probability/Distributions/ChiSquare.lean:31
Uses 2 · Used by 2
TheoremExponential moments of the chi-square distribution#✓fully proved
Let \(p\) be a positive integer and let \(\chi^2_p\) be the chi-square law with \(p\) degrees of freedom. For every real \(t < 1/2\), the function \(x \mapsto e^{t x}\) is integrable with respect to \(\chi^2_p\).
theorem integrable_exp_mul_chiSquareMeasure {p : ℕ} (hp : 0 < p) {t : ℝ}
(ht : t < 1 / 2) :
Integrable (fun x : ℝ => Real.exp (t * x)) (chiSquareMeasure p)noncomputable def chiSquareMeasure (p : ℕ) : Measure ℝ :=
gammaMeasure ((p : ℝ) / 2) (1 / 2)MathlibExt/Probability/Distributions/ChiSquare.lean:31
Uses 2
TheoremThe square of a standard normal variable is chi-square with one degree of freedom#✓fully proved
The square of a standard normal variable is chi-square with one degree of freedom, as
an identity of measures on ℝ. (Moved here from the likelihood-ratio development so that
both that development and Cochran's theorem reuse one declaration.)
theorem gaussianReal_map_sq :
(gaussianReal 0 1).map (fun x : ℝ => x ^ 2) = chiSquareMeasure 1noncomputable def chiSquareMeasure (p : ℕ) : Measure ℝ :=
gammaMeasure ((p : ℝ) / 2) (1 / 2)MathlibExt/Probability/Distributions/ChiSquare.lean:31
Uses 5 · Used by 3
TheoremChi-square moment generating functions multiply by adding degrees#✓fully proved
Chi-square MGFs multiply by adding degrees, below 1/2. Requires a
nonempty index set so the summed degree stays positive.
theorem prod_mgf_chiSquareMeasure_eq_mgf_sum {ι : Type*} {s : Finset ι}
{p : ι → ℕ} (hs : s.Nonempty) (hp : ∀ i ∈ s, 0 < p i) {t : ℝ}
(ht : t < 1 / 2) :
∏ i ∈ s, mgf id (chiSquareMeasure (p i)) t
= mgf id (chiSquareMeasure (∑ i ∈ s, p i)) tnoncomputable def chiSquareMeasure (p : ℕ) : Measure ℝ :=
gammaMeasure ((p : ℝ) / 2) (1 / 2)MathlibExt/Probability/Distributions/ChiSquare.lean:31
Uses 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.