Gaussian constructions of noncentral chi-squared laws

A sum of squares of independent unit-variance real Gaussians has noncentral chi-squared law. Its degree is the number of coordinates and its noncentrality is the sum of squared means. Equivalently, the squared norm of a Gaussian vector with identity covariance has noncentrality equal to the squared norm of its mean. The empty coordinate type gives the point mass at zero. In one dimension, the square of a unit-variance Gaussian with mean m has degree one and noncentrality m ^ 2.

The identification uses the Gaussian-square moment-generating function and TauCeti.Measure.ext_of_mgf. The product-law equality also yields the construction for an independent family of random variables.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, second edition, Wiley, 1995, chapter 29.

@[simp]

theorem TauCeti.Probability.map_sum_sq_pi_gaussianReal_noncentral {ι : Type u_1} [Fintype ι] (m : ι → ℝ) : MeasureTheory.Measure.map (fun (x : ι → ℝ) => ∑ i : ι, x i ^ 2) (MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.gaussianReal (m i) 1) = noncentralChiSquaredMeasure (↑(Fintype.card ι)) (∑ i : ι, ‖m i‖₊ ^ 2)

The sum of squares of independent unit-variance Gaussian coordinates has noncentral chi-squared law, including the empty family.

theorem TauCeti.Probability.gaussianReal_map_sq_noncentral (m : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => x ^ 2) (ProbabilityTheory.gaussianReal m 1) = noncentralChiSquaredMeasure 1 (‖m‖₊ ^ 2)

The square of a unit-variance real Gaussian with mean m has noncentral chi-squared law with degree one and noncentrality m ^ 2.

@[simp]

theorem TauCeti.Probability.map_norm_sq_multivariateGaussian_noncentral {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) : MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ ι) => ‖x‖ ^ 2) (ProbabilityTheory.multivariateGaussian m 1) = noncentralChiSquaredMeasure (↑(Fintype.card ι)) (‖m‖₊ ^ 2)

The squared norm of an identity-covariance Gaussian has noncentral chi-squared law with noncentrality the squared norm of its mean. Dimension zero is included.

theorem ProbabilityTheory.iIndepFun.hasLaw_sum_sq_gaussianReal_noncentral {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] {X : ι → Ω → ℝ} {m : ι → ℝ} (hindep : iIndepFun X P) (hlaw : ∀ (i : ι), HasLaw (X i) (gaussianReal (m i) 1) P) : HasLaw (fun (ω : Ω) => ∑ i : ι, X i ω ^ 2) (TauCeti.Probability.noncentralChiSquaredMeasure (↑(Fintype.card ι)) (∑ i : ι, ‖m i‖₊ ^ 2)) P

A finite independent family of unit-variance Gaussians gives a noncentral chi-squared sum of squares.

theorem ProbabilityTheory.HasLaw.norm_sq_multivariateGaussian {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Ω → EuclideanSpace ℝ ι} {m : EuclideanSpace ℝ ι} (hX : HasLaw X (multivariateGaussian m 1) P) : HasLaw (fun (ω : Ω) => ‖X ω‖ ^ 2) (TauCeti.Probability.noncentralChiSquaredMeasure (↑(Fintype.card ι)) (‖m‖₊ ^ 2)) P

The squared norm of an identity-covariance Gaussian random vector has noncentral chi-squared law.