Covariances and covariance matrices

Covariance is unchanged by almost-everywhere changes to either observable. This file also packages the coordinate covariances of a measure on a finite-dimensional Euclidean space as a matrix and connects that matrix to Mathlib's basis-free covarianceBilin.

The MemLp id 2 μ hypothesis in the comparison theorem is essential. Mathlib deliberately sets covarianceBilin μ to zero when this hypothesis fails, whereas its scalar covariance is totalized coordinate by coordinate.

Main results

• TauCeti.covMatrix is the matrix of coordinate covariances of a measure.
• TauCeti.covarianceBilin_eq_covMatrix identifies the matrix and bilinear-form views of covariance when the measure has a finite second moment.
• TauCeti.posSemidef_covMatrix proves that covariance matrices are positive semidefinite under the same moment hypotheses.
• TauCeti.integral_inner_toEuclideanLin_sub_integral_eq_trace_mul_covMatrix computes the mean of a quadratic form of the centred variable as a trace against the covariance matrix.
• TauCeti.integral_inner_toEuclideanLin_sub_integral_eq_trace_mul_covMatrix_map is the same identity for a square-integrable random vector and the covariance matrix of its law.
• TauCeti.integral_norm_sub_sq_eq_norm_integral_sub_sq_add_trace_covMatrix decomposes the second moment about a point into the squared distance from the mean to that point and the trace of the covariance matrix.
• TauCeti.covarianceBilin_eq_smul_innerSL shows that a law invariant under every linear isometry has covariance equal to its second moment divided by the dimension, times the inner product.

References

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

theorem TauCeti.covariance_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X X' Y Y' : Ω → ℝ} (hX : X =ᵐ[μ] X') (hY : Y =ᵐ[μ] Y') : ProbabilityTheory.covariance X Y μ = ProbabilityTheory.covariance X' Y' μ

Covariance is unchanged by almost-everywhere changes to either observable.

noncomputable def TauCeti.covMatrix {ι : Type u_1} (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) : Matrix ι ι ℝ

The covariance matrix of a measure on a finite-dimensional Euclidean space. Its (i, j) entry is the scalar covariance of the ith and jth coordinate projections.

@[simp]

theorem TauCeti.covMatrix_apply {ι : Type u_1} (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) (i j : ι) : covMatrix μ i j = ProbabilityTheory.covariance (fun (z : EuclideanSpace ℝ ι) => z.ofLp i) (fun (z : EuclideanSpace ℝ ι) => z.ofLp j) μ

An entry of covMatrix is the covariance of the corresponding coordinate projections.

theorem TauCeti.covMatrix_apply_comm {ι : Type u_1} (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) (i j : ι) : covMatrix μ i j = covMatrix μ j i

Covariance matrices are symmetric.

theorem TauCeti.isHermitian_covMatrix {ι : Type u_1} (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) : (covMatrix μ).IsHermitian

A covariance matrix is Hermitian (equivalently, symmetric over ℝ).

theorem TauCeti.covarianceBilin_eq_covMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.MemLp id 2 μ) (x y : EuclideanSpace ℝ ι) : ((ProbabilityTheory.covarianceBilin μ) x) y = inner ℝ x ((Matrix.toEuclideanLin (covMatrix μ)) y)

For a finite measure with finite second moment, the entrywise covariance matrix represents Mathlib's basis-free covariance bilinear form.

theorem TauCeti.posSemidef_covMatrix {ι : Type u_1} [Fintype ι] (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [MeasureTheory.IsFiniteMeasure μ] (hμ : MeasureTheory.MemLp id 2 μ) : (covMatrix μ).PosSemidef

The covariance matrix of a finite measure with finite second moment is positive semidefinite.

theorem TauCeti.integral_inner_toEuclideanLin_sub_integral_eq_trace_mul_covMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.MemLp id 2 μ) (B : Matrix ι ι ℝ) : ∫ (x : EuclideanSpace ℝ ι), inner ℝ ((Matrix.toEuclideanLin B) (x - ∫ (y : EuclideanSpace ℝ ι), y ∂μ)) (x - ∫ (y : EuclideanSpace ℝ ι), y ∂μ) ∂μ = (B * covMatrix μ).trace

The mean of the quadratic form of a matrix B on the centred variable of a Euclidean-valued probability measure with finite second moment is the trace of B times the covariance matrix.

theorem TauCeti.integral_inner_toEuclideanLin_sub_integral_eq_trace_mul_covMatrix_map {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → EuclideanSpace ℝ ι} (hX : MeasureTheory.MemLp X 2 P) (B : Matrix ι ι ℝ) : ∫ (ω : Ω), inner ℝ ((Matrix.toEuclideanLin B) (X ω - ∫ (ω' : Ω), X ω' ∂P)) (X ω - ∫ (ω' : Ω), X ω' ∂P) ∂P = (B * covMatrix (MeasureTheory.Measure.map X P)).trace

The mean of the quadratic form of a matrix B on the centred variable of a square-integrable Euclidean-valued random vector X is the trace of B times the covariance matrix of the law of X.

theorem TauCeti.integral_norm_sub_sq_eq_norm_integral_sub_sq_add_trace_covMatrix {ι : Type u_1} [Fintype ι] (μ : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [MeasureTheory.IsProbabilityMeasure μ] (hμ : MeasureTheory.MemLp id 2 μ) (c : EuclideanSpace ℝ ι) : ∫ (x : EuclideanSpace ℝ ι), ‖x - c‖ ^ 2 ∂μ = ‖∫ (x : EuclideanSpace ℝ ι), x ∂μ - c‖ ^ 2 + (covMatrix μ).trace

The second moment of a Euclidean-valued probability measure about a point c is the squared distance from its mean to c plus the trace of its covariance matrix.

theorem TauCeti.covarianceBilin_eq_smul_innerSL {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (f : E ≃ₗᵢ[ℝ] E), MeasureTheory.Measure.map (⇑f) μ = μ) : ProbabilityTheory.covarianceBilin μ = ((∫ (x : E), ‖x‖ ^ 2 ∂μ) / ↑(Module.finrank ℝ E)) • innerSL ℝ

Covariance of an isotropic law. A finite measure on a finite-dimensional real inner product space that is invariant under every linear isometry has covariance a multiple of the inner product, the multiple being the second moment divided by the dimension. No moment hypothesis is needed: without a finite second moment both sides vanish.