Squares of Gaussian variables

This file identifies the square of a standard real Gaussian variable with the chi-squared law of one degree of freedom. It then combines this identification with independence to prove that the sum of the squares of a finite independent standard Gaussian family has the chi-squared law whose degrees of freedom are the cardinality of the family. The empty family is included: both the empty sum and chiSquaredMeasure 0 are the point mass at zero.

It also computes the exponential-integrability domain and the moment-generating function of a weighted square w * x ^ 2 of a standard Gaussian variable, and of a weighted sum of squares ∑ j, w j * c j ^ 2 of finitely many independent ones, which is the form a Gaussian quadratic statistic takes in eigen-coordinates.

These laws identify Gaussian quadratic statistics with chi-squared distributions. In particular, they provide the scalar foundation for distributional results about Gaussian norms and Gaussian Gram matrices.

For a unit-variance Gaussian with arbitrary mean m, the squared variable has mgf (1 - 2 * t) ^ (-1 / 2) * exp (m ^ 2 * t / (1 - 2 * t)) for t < 1 / 2. This also supplies the exponential moments used to identify noncentral Gaussian-square laws.

Main results

• TauCeti.Probability.gaussianReal_map_sq — the square of the standard Gaussian measure is chiSquaredMeasure 1;
• TauCeti.Probability.iIndepFun.hasLaw_sum_sq_gaussian — a finite sum of independent squared standard Gaussian variables has the corresponding chi-squared law;
• TauCeti.Probability.map_sum_sq_pi_gaussianReal — the same statement at the level of measures and for an arbitrary common variance v: the sum of squares of the coordinates of a product of gaussianReal 0 v laws is the chi-squared law scaled by v;
• TauCeti.Probability.mem_integrableExpSet_mul_sq_gaussianReal_iff and TauCeti.Probability.mgf_mul_sq_gaussianReal — the exponential moments of w * x ^ 2 are finite exactly when 2 * t * w < 1, where the moment-generating function is (1 - 2 * t * w) ^ (-1 / 2);
• TauCeti.Probability.mem_integrableExpSet_sum_mul_sq_pi_gaussianReal_iff and TauCeti.Probability.mgf_sum_mul_sq_pi_gaussianReal — the same for a weighted sum of squares of independent standard Gaussian coordinates, with the product of the one-dimensional values.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley (1994), ch. 18; vol. 2, 2nd ed., Wiley (1995), ch. 29.

@[simp]

theorem TauCeti.Probability.gaussianReal_map_sq : MeasureTheory.Measure.map (fun (x : ℝ) => x ^ 2) (ProbabilityTheory.gaussianReal 0 1) = chiSquaredMeasure 1

The image of the standard Gaussian law under squaring is the chi-squared law with one degree of freedom.

@[simp]

theorem TauCeti.Probability.mgf_sq_gaussianReal_one (m : ℝ) {t : ℝ} (ht : t < 2⁻¹) : ProbabilityTheory.mgf (fun (x : ℝ) => x ^ 2) (ProbabilityTheory.gaussianReal m 1) t = (1 - 2 * t) ^ (-1 / 2) * Real.exp (m ^ 2 * t / (1 - 2 * t))

The moment-generating function of the square of a unit-variance Gaussian, allowing an arbitrary mean.

@[simp]

theorem TauCeti.Probability.mem_integrableExpSet_mul_sq_gaussianReal_iff (w t : ℝ) : t ∈ ProbabilityTheory.integrableExpSet (fun (x : ℝ) => w * x ^ 2) (ProbabilityTheory.gaussianReal 0 1) ↔ 2 * t * w < 1

The exponential moment of order t of w * x ^ 2 under the standard Gaussian is finite exactly when 2 * t * w < 1.

@[simp]

theorem TauCeti.Probability.mgf_mul_sq_gaussianReal {w t : ℝ} (ht : 2 * t * w < 1) : ProbabilityTheory.mgf (fun (x : ℝ) => w * x ^ 2) (ProbabilityTheory.gaussianReal 0 1) t = (1 - 2 * t * w) ^ (-1 / 2)

The moment-generating function of w * x ^ 2 under the standard Gaussian is (1 - 2 * t * w) ^ (-1 / 2) on its domain 2 * t * w < 1.

@[simp]

theorem TauCeti.Probability.mem_integrableExpSet_sum_mul_sq_pi_gaussianReal_iff {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (t : ℝ) : t ∈ ProbabilityTheory.integrableExpSet (fun (c : ι → ℝ) => ∑ j : ι, w j * c j ^ 2) (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1) ↔ ∀ (j : ι), 2 * t * w j < 1

The exponential moment of order t of the weighted sum of squares ∑ j, w j * c j ^ 2 of independent standard Gaussian coordinates is finite exactly when 2 * t * w j < 1 for every j.

@[simp]

theorem TauCeti.Probability.mgf_sum_mul_sq_pi_gaussianReal {ι : Type u_1} [Fintype ι] {w : ι → ℝ} {t : ℝ} (ht : ∀ (j : ι), 2 * t * w j < 1) : ProbabilityTheory.mgf (fun (c : ι → ℝ) => ∑ j : ι, w j * c j ^ 2) (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 1) t = ∏ j : ι, (1 - 2 * t * w j) ^ (-1 / 2)

The moment-generating function of the weighted sum of squares ∑ j, w j * c j ^ 2 of independent standard Gaussian coordinates is ∏ j, (1 - 2 * t * w j) ^ (-1 / 2) on its domain.

theorem TauCeti.Probability.iIndepFun.hasLaw_sum_sq_gaussian {Omega : Type u_1} {iota : Type u_2} [MeasurableSpace Omega] [Fintype iota] {P : MeasureTheory.Measure Omega} {X : iota → Omega → ℝ} (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : iota), ProbabilityTheory.HasLaw (X i) (ProbabilityTheory.gaussianReal 0 1) P) : ProbabilityTheory.HasLaw (fun (omega : Omega) => ∑ i : iota, X i omega ^ 2) (chiSquaredMeasure ↑(Fintype.card iota)) P

A finite sum of squares of independent standard Gaussian variables has the chi-squared law with one degree of freedom per variable. This includes an empty index type, when both sides are the point mass at zero.

theorem TauCeti.Probability.map_sum_sq_pi_gaussianReal {ι : Type u_3} [Fintype ι] (v : NNReal) : MeasureTheory.Measure.map (fun (y : ι → ℝ) => ∑ i : ι, y i ^ 2) (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 v) = MeasureTheory.Measure.map (fun (x : ℝ) => ↑v * x) (chiSquaredMeasure ↑(Fintype.card ι))

The law of a sum of squared centred Gaussian coordinates of common variance. Pushing a finite product of gaussianReal 0 v laws forward by the sum of the squared coordinates gives the chi-squared law with one degree of freedom per coordinate, scaled by v. For an empty index type both sides are the point mass at zero.