Chi distributions

The chi law chiMeasure k s is the law of s * √X for a chi-squared variable X with k degrees of freedom. It describes Gaussian radii, with a scale parameter independent of the degrees of freedom. Nonnegative degrees and positive scale give probability measures. Zero degrees give a point mass at zero; negative degrees or nonpositive scale give the zero measure.

This file supplies the measure, its Lebesgue density at positive degrees, parameter measurability, the cumulative distribution function, and the squaring and scaling identities. The density is written in standardized coordinates x / s. The change of variables reuses map_sqrt_chiSquaredMeasure and map_affine_withDensity_volume.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, second edition, Wiley, 1994, chapter 18.

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

The chi law of degree k and scale s: the image of the chi-squared law by s * √· when s > 0, and zero otherwise. Degree zero gives a Dirac law for positive scale.

theorem TauCeti.Probability.chiMeasure_of_scale_pos {k s : ℝ} (hs : 0 < s) : chiMeasure k s = MeasureTheory.Measure.map (fun (x : ℝ) => s * √x) (chiSquaredMeasure k)

The defining square-root pushforward at positive scale.

theorem TauCeti.Probability.chiMeasure_eq_map_gammaMeasure {k s : ℝ} (hk : 0 < k) (hs : 0 < s) : chiMeasure k s = MeasureTheory.Measure.map (fun (x : ℝ) => s * √x) (ProbabilityTheory.gammaMeasure (k / 2) (1 / 2))

At positive degrees and scale, the chi law is the scaled square-root image of a Gamma law.

@[simp]

theorem TauCeti.Probability.chiMeasure_of_scale_nonpos {k s : ℝ} (hs : s ≤ 0) : chiMeasure k s = 0

Nonpositive scale gives the zero measure.

@[simp]

theorem TauCeti.Probability.chiMeasure_of_neg {k s : ℝ} (hk : k < 0) : chiMeasure k s = 0

Negative degrees give the zero measure at every scale.

@[simp]

theorem TauCeti.Probability.chiMeasure_zero {s : ℝ} (hs : 0 < s) : chiMeasure 0 s = MeasureTheory.Measure.dirac 0

At degree zero and positive scale, the chi law is the point mass at zero.

theorem TauCeti.Probability.isProbabilityMeasure_chiMeasure {k s : ℝ} (hk : 0 ≤ k) (hs : 0 < s) : MeasureTheory.IsProbabilityMeasure (chiMeasure k s)

Nonnegative degrees and positive scale give a probability measure.

noncomputable def TauCeti.Probability.chiPDFReal (k s x : ℝ) : ℝ

The real chi density, written in standardized coordinates. It vanishes outside the positive half-line, at degree zero, and at invalid parameters.

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

The extended nonnegative chi density. Degree zero is singular and has no density identity.

theorem TauCeti.Probability.chiPDF_eq_ofReal (k s x : ℝ) : chiPDF k s x = ENNReal.ofReal (chiPDFReal k s x)

The extended chi density is obtained by applying ENNReal.ofReal to the real density.

@[simp]

theorem TauCeti.Probability.chiPDFReal_of_pos {k s x : ℝ} (hk : 0 < k) (hs : 0 < s) (hx : 0 < x) : chiPDFReal k s x = 2 ^ (1 - k / 2) / Real.Gamma (k / 2) * (x / s) ^ (k - 1) * Real.exp (-(x / s) ^ 2 / 2) / s

The chi density on the positive half-line at positive parameters.

theorem TauCeti.Probability.chiPDFReal_of_not_pos {k s x : ℝ} (h : ¬(0 < k ∧ 0 < s ∧ 0 < x)) : chiPDFReal k s x = 0

The density vanishes off the positive-parameter, positive-coordinate domain.

theorem TauCeti.Probability.chiPDF_of_not_pos {k s x : ℝ} (h : ¬(0 < k ∧ 0 < s ∧ 0 < x)) : chiPDF k s x = 0

The extended density vanishes off the positive-parameter, positive-coordinate domain.

@[simp]

theorem TauCeti.Probability.chiPDFReal_of_nonpos {k s x : ℝ} (hx : x ≤ 0) : chiPDFReal k s x = 0

The real chi density vanishes on the nonpositive half-line.

@[simp]

theorem TauCeti.Probability.chiPDF_of_nonpos {k s x : ℝ} (hx : x ≤ 0) : chiPDF k s x = 0

The extended chi density vanishes on the nonpositive half-line.

@[simp]

theorem TauCeti.Probability.chiPDF_of_pos {k s x : ℝ} (hk : 0 < k) (hs : 0 < s) (hx : 0 < x) : chiPDF k s x = ENNReal.ofReal (2 ^ (1 - k / 2) / Real.Gamma (k / 2) * (x / s) ^ (k - 1) * Real.exp (-(x / s) ^ 2 / 2) / s)

The extended chi density on the positive half-line at positive parameters.

theorem TauCeti.Probability.chiPDFReal_nonneg (k s x : ℝ) : 0 ≤ chiPDFReal k s x

The real chi density is nonnegative for every parameter value.

theorem TauCeti.Probability.chiPDFReal_pos_iff {k s x : ℝ} (hk : 0 < k) (hs : 0 < s) : 0 < chiPDFReal k s x ↔ 0 < x

The positivity set of a valid positive-degree chi density is the positive half-line.

@[simp]

theorem TauCeti.Probability.toReal_chiPDF (k s x : ℝ) : (chiPDF k s x).toReal = chiPDFReal k s x

The extended density has the stated real density as its real value.

theorem TauCeti.Probability.measurable_uncurry_chiPDFReal : Measurable fun (p : (ℝ × ℝ) × ℝ) => chiPDFReal p.1.1 p.1.2 p.2

The chi density is jointly measurable in degrees, scale, and coordinate.

theorem TauCeti.Probability.measurable_chiPDFReal (k s : ℝ) : Measurable (chiPDFReal k s)

The real chi density is measurable in its coordinate.

theorem TauCeti.Probability.measurable_uncurry_chiPDF : Measurable fun (p : (ℝ × ℝ) × ℝ) => chiPDF p.1.1 p.1.2 p.2

The extended chi density is jointly measurable in degrees, scale, and coordinate.

theorem TauCeti.Probability.measurable_chiPDF (k s : ℝ) : Measurable (chiPDF k s)

The chi density is measurable in its coordinate.

theorem TauCeti.Probability.chiMeasure_eq_withDensity {k s : ℝ} (hk : 0 < k) : chiMeasure k s = MeasureTheory.volume.withDensity (chiPDF k s)

At positive degrees the chi law has its named Lebesgue density, at every scale (both sides vanish at nonpositive scale).

theorem TauCeti.Probability.measurable_chiMeasure : Measurable fun (p : ℝ × ℝ) => chiMeasure p.1 p.2

The chi family is jointly Giry measurable, including its invalid and Dirac branches.

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

A random variable with a positive-degree chi law has a density.

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

The canonical density of a chi variable agrees almost everywhere with chiPDF.

theorem TauCeti.Probability.rnDeriv_chiMeasure {k s : ℝ} (hk : 0 < k) : (chiMeasure k s).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] chiPDF k s

The Radon–Nikodym derivative of a positive-degree chi law is its named density.

theorem TauCeti.Probability.ae_pos_chiMeasure {k s : ℝ} (hk : 0 < k) : ∀ᵐ (x : ℝ) ∂chiMeasure k s, 0 < x

Positive-degree chi laws are carried by the positive half-line.

@[simp]

theorem TauCeti.Probability.chiMeasure_map_const_mul {k s c : ℝ} (hc : 0 < c) : MeasureTheory.Measure.map (fun (x : ℝ) => c * x) (chiMeasure k s) = chiMeasure k (c * s)

Positive scaling multiplies the chi scale in every parameter regime.

theorem TauCeti.Probability.hasLaw_chiMeasure_of_hasLaw_chiSquaredMeasure {k s : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hs : 0 < s) (hX : ProbabilityTheory.HasLaw X (chiSquaredMeasure k) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => s * √(X ω)) (chiMeasure k s) P

Taking a scaled square root of a chi-squared variable gives the chi law.

theorem TauCeti.Probability.chiMeasure_map_sq {k s : ℝ} (hs : 0 < s) : MeasureTheory.Measure.map (fun (x : ℝ) => x ^ 2) (chiMeasure k s) = MeasureTheory.Measure.map (fun (x : ℝ) => s ^ 2 * x) (chiSquaredMeasure k)

Squaring a chi variable gives the squared scale times a chi-squared variable.

@[simp]

theorem TauCeti.Probability.cdf_chiMeasure_eq {k s : ℝ} (hk : 0 < k) (hs : 0 < s) (x : ℝ) : ↑(ProbabilityTheory.cdf (chiMeasure k s)) x = if x < 0 then 0 else regularizedGamma (k / 2) ((x / s) ^ 2 / 2)

The chi cdf is the regularized lower incomplete Gamma function on the nonnegative half-line and zero below it.

theorem TauCeti.Probability.cdf_chiMeasure_zero {s : ℝ} (hs : 0 < s) (x : ℝ) : ↑(ProbabilityTheory.cdf (chiMeasure 0 s)) x = if 0 ≤ x then 1 else 0

The cdf at the degree-zero boundary is the unit step at zero.