Square roots of gamma variables

A positive variable whose square is gamma has a density of its own: substituting x = t ^ 2 in the gamma density and multiplying by the Jacobian 2 * t turns r ^ a / Γ a * x ^ (a - 1) * exp (-(r * x)) into 2 * r ^ a / Γ a * t ^ (2 * a - 1) * exp (-(r * t ^ 2)) on the positive half-line. This file proves that correspondence in both directions: squaring carries the latter law to gammaMeasure, and taking square roots carries gammaMeasure back.

At shape k / 2 and rate 1 / 2 the source law is the chi law with k degrees of freedom, whose density is 2 ^ (1 - k / 2) / Γ (k / 2) * t ^ (k - 1) * exp (-t ^ 2 / 2), and the target law is TauCeti.Probability.chiSquaredMeasure k. That is the shape in which a triangular factorisation meets a chi-squared law: the diagonal entries of a Cholesky factor carry the chi density directly, and it is their squares that are chi-squared.

Main results

• TauCeti.Probability.map_sq_withDensity_eq_gammaMeasure — squaring sends the root-gamma law to gammaMeasure a r;
• TauCeti.Probability.map_sqrt_gammaMeasure — the inverse correspondence, the image of gammaMeasure a r under Real.sqrt;
• TauCeti.Probability.map_sq_withDensity_eq_chiSquaredMeasure and TauCeti.Probability.map_sqrt_chiSquaredMeasure — the same pair for the chi and chi-squared laws;
• TauCeti.Probability.isProbabilityMeasure_withDensity_rootGamma and TauCeti.Probability.isProbabilityMeasure_withDensity_chi — both source laws are normalised.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley, 1994, ch. 18 (the chi distribution) and ch. 17 (the gamma family).

theorem TauCeti.Probability.map_sq_withDensity_eq_gammaMeasure (a r : ℝ) : MeasureTheory.Measure.map (fun (t : ℝ) => t ^ 2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 * r ^ a / Real.Gamma a * t ^ (2 * a - 1) * Real.exp (-(r * t ^ 2)))) = ProbabilityTheory.gammaMeasure a r

The square of a root-gamma variable is gamma. On the positive half-line the density 2 * r ^ a / Γ a * t ^ (2 * a - 1) * exp (-(r * t ^ 2)) is carried by squaring to the gamma law of shape a and rate r.

theorem TauCeti.Probability.map_sqrt_gammaMeasure (a r : ℝ) : MeasureTheory.Measure.map Real.sqrt (ProbabilityTheory.gammaMeasure a r) = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 * r ^ a / Real.Gamma a * t ^ (2 * a - 1) * Real.exp (-(r * t ^ 2)))

The square root of a gamma variable has the root-gamma density. This inverts TauCeti.Probability.map_sq_withDensity_eq_gammaMeasure.

theorem TauCeti.Probability.isProbabilityMeasure_withDensity_rootGamma {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure ((MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 * r ^ a / Real.Gamma a * t ^ (2 * a - 1) * Real.exp (-(r * t ^ 2))))

The root-gamma density is normalised: for a positive shape and rate it carries total mass one, which is what makes the constant 2 * r ^ a / Γ a the right one.

theorem TauCeti.Probability.map_sq_withDensity_eq_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : MeasureTheory.Measure.map (fun (t : ℝ) => t ^ 2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 ^ (1 - k / 2) / Real.Gamma (k / 2) * t ^ (k - 1) * Real.exp (-t ^ 2 / 2))) = chiSquaredMeasure k

The square of a chi variable is chi-squared. On the positive half-line the chi density 2 ^ (1 - k / 2) / Γ (k / 2) * t ^ (k - 1) * exp (-t ^ 2 / 2) is carried by squaring to the chi-squared law with k degrees of freedom.

theorem TauCeti.Probability.map_sqrt_chiSquaredMeasure {k : ℝ} (hk : 0 < k) : MeasureTheory.Measure.map Real.sqrt (chiSquaredMeasure k) = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 ^ (1 - k / 2) / Real.Gamma (k / 2) * t ^ (k - 1) * Real.exp (-t ^ 2 / 2))

The square root of a chi-squared variable has the chi density. This inverts TauCeti.Probability.map_sq_withDensity_eq_chiSquaredMeasure.

theorem TauCeti.Probability.isProbabilityMeasure_withDensity_chi {k : ℝ} (hk : 0 < k) : MeasureTheory.IsProbabilityMeasure ((MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (t : ℝ) => ENNReal.ofReal (2 ^ (1 - k / 2) / Real.Gamma (k / 2) * t ^ (k - 1) * Real.exp (-t ^ 2 / 2)))

The chi density is normalised: for positive degrees of freedom it carries total mass one, which is what makes the constant 2 ^ (1 - k / 2) / Γ (k / 2) the right one.