The covariance matrix of a multivariate Gaussian

This file identifies the generic covariance matrix from TauCeti.Probability.Moments.Covariance with the covariance parameter of Mathlib's multivariate Gaussian, and records the centred multivariate Gaussian as the image of the standard Gaussian under the square root of its matrix parameter. It also records measurability of Gaussian laws with covariance scaled by a precision parameter, covariance under matrix-valued linear maps and characterizes independence of complementary coordinate blocks.

Main results

• TauCeti.Probability.covMatrix_multivariateGaussian recovers the covariance parameter of a multivariate Gaussian law.
• TauCeti.Probability.integral_of_hasLaw_multivariateGaussian gives the Bochner mean of a random variable with a multivariate Gaussian law.
• TauCeti.Probability.multivariateGaussian_zero_eq_map_stdGaussian_sqrt writes the centred law as an image of the standard Gaussian.
• TauCeti.Probability.multivariateGaussian_zero_right identifies the zero-covariance law with the point mass at its mean.
• TauCeti.Probability.measurable_multivariateGaussian_inv_smul shows that the family τ ↦ N(m, τ⁻¹ • S) is measurable in the precision τ.
• TauCeti.Probability.measurable_multivariateGaussian_prodMk_left_apply shows that the Gaussian law with measurable mean and covariance-parameter families, evaluated on a section of a measurable set, is measurable in the parameter.
• TauCeti.Probability.covariance_inner_matrix_multivariateGaussian computes covariance after two matrix maps.
• TauCeti.Probability.indepFun_sumEquivProd_multivariateGaussian_iff characterizes independence of two complementary coordinate blocks.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 5, item 1, Covariance matrices.

@[simp]

theorem TauCeti.Probability.covMatrix_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) : covMatrix (ProbabilityTheory.multivariateGaussian m S) = S

The covariance matrix of a positive-semidefinite multivariate Gaussian is its covariance parameter.

@[simp]

theorem TauCeti.Probability.integral_eval_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) (i : ι) : ∫ (x : EuclideanSpace ℝ ι), x.ofLp i ∂ProbabilityTheory.multivariateGaussian m S = m.ofLp i

Each coordinate of a multivariate Gaussian has as mean the corresponding coordinate of the mean parameter. No hypothesis on the covariance parameter is needed.

theorem TauCeti.Probability.integral_of_hasLaw_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ ι} {m : EuclideanSpace ℝ ι} {S : Matrix ι ι ℝ} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.multivariateGaussian m S) P) : ∫ (ω : Ω), X ω ∂P = m

The Bochner mean of a random variable with a multivariate Gaussian law is its Gaussian mean.

theorem TauCeti.Probability.multivariateGaussian_zero_eq_map_stdGaussian_sqrt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Matrix ι ι ℝ) : ProbabilityTheory.multivariateGaussian 0 S = MeasureTheory.Measure.map (⇑(Matrix.toEuclideanCLM (CFC.sqrt S))) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι))

A centred multivariate Gaussian law is the image of the standard Gaussian under the square root of its matrix parameter. No hypothesis on that parameter is needed.

@[simp]

theorem TauCeti.Probability.multivariateGaussian_zero_right {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) : ProbabilityTheory.multivariateGaussian m 0 = MeasureTheory.Measure.dirac m

A multivariate Gaussian with zero covariance is the point mass at its mean.

theorem TauCeti.Probability.measurable_multivariateGaussian_inv_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) : Measurable fun (τ : ℝ) => ProbabilityTheory.multivariateGaussian m (τ⁻¹ • S)

The Gaussian family τ ↦ N(m, τ⁻¹ • S) is measurable in the precision τ.

theorem TauCeti.Probability.measurable_multivariateGaussian_prodMk_left_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {m : Y → EuclideanSpace ℝ ι} {S : Y → Matrix ι ι ℝ} {g : Y → X} (hm : Measurable m) (hS : Measurable S) (hg : Measurable g) {A : Set (X × EuclideanSpace ℝ ι)} (hA : MeasurableSet A) : Measurable fun (y : Y) => (ProbabilityTheory.multivariateGaussian (m y) (S y)) (Prod.mk (g y) ⁻¹' A)

For measurable mean and covariance-parameter families m and S on a measurable space Y and a measurable map g : Y → X, the law multivariateGaussian (m y) (S y), evaluated on the section at g y of a measurable set A ⊆ X × EuclideanSpace ℝ ι, is measurable in y. The parameter S y need not be positive semidefinite: where it is not, the law is the point mass at m y.

theorem TauCeti.Probability.covariance_inner_matrix_multivariateGaussian {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq γ] (m : EuclideanSpace ℝ γ) {S : Matrix γ γ ℝ} (hS : S.PosSemidef) (L : Matrix α γ ℝ) (K : Matrix β γ ℝ) (x : EuclideanSpace ℝ α) (y : EuclideanSpace ℝ β) : ProbabilityTheory.covariance (fun (z : EuclideanSpace ℝ γ) => inner ℝ x ((Matrix.toEuclideanLin L) z)) (fun (z : EuclideanSpace ℝ γ) => inner ℝ y ((Matrix.toEuclideanLin K) z)) (ProbabilityTheory.multivariateGaussian m S) = x.ofLp ⬝ᵥ (L * S * K.transpose).mulVec y.ofLp

The covariance of scalar inner-product projections after two matrix-valued linear maps of a multivariate Gaussian.

theorem TauCeti.Probability.indepFun_sumEquivProd_multivariateGaussian_iff {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (m : EuclideanSpace ℝ (ι ⊕ κ)) {S : Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ} (hS : S.PosSemidef) : ProbabilityTheory.IndepFun (fun (x : EuclideanSpace ℝ (ι ⊕ κ)) => (EuclideanSpace.sumEquivProd x).1) (fun (x : EuclideanSpace ℝ (ι ⊕ κ)) => (EuclideanSpace.sumEquivProd x).2) (ProbabilityTheory.multivariateGaussian m S) ↔ S.submatrix Sum.inl Sum.inr = 0

The two complementary coordinate blocks of a multivariate Gaussian with positive-semidefinite covariance are independent exactly when their cross-covariance block vanishes.