Affine images of Gaussian measures

An affine map on the real line transforms a Gaussian's mean and variance by m ↦ a + b * m and v ↦ b ^ 2 * v, including zero slopes and zero variances.

This file also proves that a multivariate Gaussian measure is carried by a rectangular affine map to the multivariate Gaussian with the transformed mean and covariance. Rectangular matrices are allowed, so the result applies both to embeddings and to possibly singular projections.

Main results

• TauCeti.Probability.gaussianReal_map_const_add_const_mul: the affine pushforward formula for a real Gaussian measure.
• TauCeti.Probability.gaussianReal_map_linear_combination: orthogonal combinations of two independent standard Gaussians remain standard Gaussian.
• TauCeti.Probability.map_affine_multivariateGaussian: the affine pushforward formula for a multivariate Gaussian measure.
• TauCeti.Probability.map_add_smul_multivariateGaussian: scaling by a real number followed by a translation.
• TauCeti.Probability.map_comp_multivariateGaussian: reindexing the coordinates along a map of index types.
• TauCeti.Probability.multivariateGaussian_one_eq_map_pi: the identity-covariance law as a product of its Gaussian coordinate laws.

References

• M. L. Eaton, Multivariate Statistics: A Vector Space Approach.
• TauCetiRoadmap/StandardDistributions/README.md, Layer 5, item 3, Affine maps of Gaussian laws.

theorem TauCeti.Probability.gaussianReal_map_linear_combination (a b : ℝ) (hab : a ^ 2 + b ^ 2 = 1) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)) = ProbabilityTheory.gaussianReal 0 1

An orthogonal combination of two independent standard Gaussians is standard Gaussian.

@[simp]

theorem TauCeti.Probability.gaussianReal_map_const_add_const_mul (m : ℝ) (v : NNReal) (a b : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) (ProbabilityTheory.gaussianReal m v) = ProbabilityTheory.gaussianReal (a + b * m) (NNReal.mk (b ^ 2) ⋯ * v)

The affine image of a real Gaussian has mean a + b * m and variance b ^ 2 * v. This includes zero slopes and zero variances.

@[simp]

theorem TauCeti.Probability.map_affine_multivariateGaussian {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (m : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (L : Matrix κ ι ℝ) (c : EuclideanSpace ℝ κ) : MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ ι) => (Matrix.toEuclideanLin L) x + c) (ProbabilityTheory.multivariateGaussian m S) = ProbabilityTheory.multivariateGaussian ((Matrix.toEuclideanLin L) m + c) (L * S * L.transpose)

The image of a multivariate Gaussian under a rectangular affine map is the multivariate Gaussian with the corresponding transformed mean and covariance.

theorem TauCeti.Probability.map_add_smul_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m₀ : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (m : EuclideanSpace ℝ ι) (c : ℝ) : MeasureTheory.Measure.map (fun (z : EuclideanSpace ℝ ι) => m + c • z) (ProbabilityTheory.multivariateGaussian m₀ S) = ProbabilityTheory.multivariateGaussian (m + c • m₀) (c ^ 2 • S)

Scaling a multivariate Gaussian vector by c and then translating it by m gives the multivariate Gaussian with mean m + c • m₀ and covariance c ^ 2 • S.

theorem TauCeti.Probability.map_comp_multivariateGaussian {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (m : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (f : κ → ι) : MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ ι) => WithLp.toLp 2 fun (k : κ) => x.ofLp (f k)) (ProbabilityTheory.multivariateGaussian m S) = ProbabilityTheory.multivariateGaussian (WithLp.toLp 2 fun (k : κ) => m.ofLp (f k)) (S.submatrix f f)

Reading the coordinates of a multivariate Gaussian vector along a map of index types gives the multivariate Gaussian with the reindexed mean and covariance. The map need not be injective, so coordinates may be repeated or omitted.

theorem TauCeti.Probability.multivariateGaussian_one_eq_map_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) : ProbabilityTheory.multivariateGaussian m 1 = MeasureTheory.Measure.map (WithLp.toLp 2) (MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.gaussianReal (m.ofLp i) 1)

An identity-covariance Gaussian is the product of its unit-variance Gaussian coordinate laws, transported to Euclidean space.