Gaussian constructions of chi laws

The norm of a standard Gaussian vector in a finite-dimensional real inner product space has the chi law with degrees of freedom equal to the dimension. Multiplying that norm by a positive scale gives the corresponding scaled chi law. Dimension zero is included and gives a point mass at zero.

The squared radius has the corresponding chi-squared law, also in dimension zero.

For independent centered real Gaussians with common positive variance, the Euclidean norm has scale equal to the square root of that variance. Dimensions one, two, and three give the half-normal, Rayleigh, and Maxwell–Boltzmann constructions, respectively. The scalar absolute-value identity is also provided directly. These identifications allow the density, moments, and quantiles of chi laws to be used for Gaussian radii. The half-normal moment-generating function E[exp (u * |Z|)] = 2 * exp (u ^ 2 / 2) * Φ(u), for a standard Gaussian Z and Φ = cdf (gaussianReal 0 1), is computed from the Gaussian tilting identity gaussianPDFReal_mul_exp_div_mgf.

The proofs reuse map_sum_sq_pi_gaussianReal and Mathlib's orthonormal-basis representation stdGaussian_eq_map_pi_orthonormalBasis.

References

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

@[simp]

theorem TauCeti.Probability.stdGaussian_map_norm (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.Measure.map (fun (x : E) => ‖x‖) (ProbabilityTheory.stdGaussian E) = chiMeasure (↑(Module.finrank ℝ E)) 1

The radius of a standard Gaussian vector has the unit-scale chi law, including in dimension zero.

@[simp]

theorem TauCeti.Probability.stdGaussian_map_const_mul_norm (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : ℝ} (hs : 0 < s) : MeasureTheory.Measure.map (fun (x : E) => s * ‖x‖) (ProbabilityTheory.stdGaussian E) = chiMeasure (↑(Module.finrank ℝ E)) s

A positive multiple of a standard Gaussian radius has the chi law with that scale.

@[simp]

theorem TauCeti.Probability.stdGaussian_map_norm_sq (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.Measure.map (fun (x : E) => ‖x‖ ^ 2) (ProbabilityTheory.stdGaussian E) = chiSquaredMeasure ↑(Module.finrank ℝ E)

The squared norm of a standard Gaussian has chi-squared law with one degree of freedom per dimension, including dimension zero.

@[simp]

theorem TauCeti.Probability.map_norm_pi_gaussianReal {ι : Type u_1} [Fintype ι] {v : NNReal} (hv : v ≠ 0) : MeasureTheory.Measure.map (fun (x : (i : ι) → (fun (x : ι) => ℝ) i) => ‖WithLp.toLp 2 x‖) (MeasureTheory.Measure.pi fun (x : ι) => ProbabilityTheory.gaussianReal 0 v) = chiMeasure ↑(Fintype.card ι) √↑v

The Euclidean norm of independent centered Gaussians with common positive variance has the chi law with one degree per coordinate and scale equal to the standard deviation. In dimensions two and three this is the Rayleigh and Maxwell–Boltzmann construction.

@[simp]

theorem TauCeti.Probability.gaussianReal_map_abs {v : NNReal} (hv : v ≠ 0) : MeasureTheory.Measure.map (fun (x : ℝ) => |x|) (ProbabilityTheory.gaussianReal 0 v) = chiMeasure 1 √↑v

The absolute value of a centered Gaussian with positive variance is half-normal: it has the one-degree chi law with scale equal to the standard deviation.

theorem TauCeti.Probability.integral_exp_mul_abs_gaussianReal (u : ℝ) : ∫ (x : ℝ), Real.exp (u * |x|) ∂ProbabilityTheory.gaussianReal 0 1 = 2 * Real.exp (u ^ 2 / 2) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) u

The moment-generating function of the half-normal law. For a standard Gaussian Z, E[exp (u * |Z|)] = 2 * exp (u ^ 2 / 2) * Φ(u).

theorem ProbabilityTheory.HasLaw.norm_stdGaussian {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} (hX : HasLaw X (stdGaussian E) P) : HasLaw (fun (ω : Ω) => ‖X ω‖) (TauCeti.Probability.chiMeasure (↑(Module.finrank ℝ E)) 1) P

The norm of a standard Gaussian random vector has the unit-scale chi law.

theorem ProbabilityTheory.HasLaw.norm_sq_stdGaussian {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} (hX : HasLaw X (stdGaussian E) P) : HasLaw (fun (ω : Ω) => ‖X ω‖ ^ 2) (TauCeti.Probability.chiSquaredMeasure ↑(Module.finrank ℝ E)) P

The squared norm of a standard Gaussian random vector has chi-squared law.

theorem ProbabilityTheory.HasLaw.const_mul_norm_stdGaussian {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} (hX : HasLaw X (stdGaussian E) P) {s : ℝ} (hs : 0 < s) : HasLaw (fun (ω : Ω) => s * ‖X ω‖) (TauCeti.Probability.chiMeasure (↑(Module.finrank ℝ E)) s) P

A positive multiple of the norm of a standard Gaussian random vector has a scaled chi law.

theorem ProbabilityTheory.iIndepFun.hasLaw_norm_gaussianReal {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] {Y : ι → Ω → ℝ} (hindep : iIndepFun Y P) {v : NNReal} (hv : v ≠ 0) (hlaw : ∀ (i : ι), HasLaw (Y i) (gaussianReal 0 v) P) : HasLaw (fun (ω : Ω) => ‖WithLp.toLp 2 fun (i : ι) => Y i ω‖) (TauCeti.Probability.chiMeasure ↑(Fintype.card ι) √↑v) P

Independent centered Gaussian coordinates of a common positive variance have a chi radius.

theorem ProbabilityTheory.HasLaw.abs_gaussianReal {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {Y : Ω → ℝ} {v : NNReal} (hY : HasLaw Y (gaussianReal 0 v) P) (hv : v ≠ 0) : HasLaw (fun (ω : Ω) => |Y ω|) (TauCeti.Probability.chiMeasure 1 √↑v) P

Taking the absolute value of a centered positive-variance Gaussian gives a half-normal law.