Covariance matrix

theorem ProbabilityTheory.IsGaussian.covarianceBilin_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] [SecondCountableTopology E] [CompleteSpace E] (x y : E) : ((covarianceBilin μ) x) y = ∫ (z : E), inner ℝ x (z - ∫ (x : E), id x ∂μ) * inner ℝ y (z - ∫ (x : E), id x ∂μ) ∂μ

theorem ProbabilityTheory.covarianceBilin_apply_prod {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X Y : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (x y : WithLp 2 (ℝ × ℝ)) : ((covarianceBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 (X ω, Y ω)) μ)) x) y = x.fst * y.fst * variance X μ + (x.fst * y.snd + x.snd * y.fst) * covariance X Y μ + x.snd * y.snd * variance Y μ

theorem ProbabilityTheory.isSymm_covarianceBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} : (covarianceBilin μ).toBilinForm.IsSymm

noncomputable def ProbabilityTheory.covMatrix {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) : Matrix (Fin (Module.finrank ℝ E)) (Fin (Module.finrank ℝ E)) ℝ

Covariance matrix of a measure on a finite dimensional inner product space.

Equations

• ProbabilityTheory.covMatrix μ = (LinearMap.BilinForm.toMatrix (stdOrthonormalBasis ℝ E).toBasis) (ProbabilityTheory.covarianceBilin μ).toBilinForm

theorem ProbabilityTheory.covMatrix_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) (i j : Fin (Module.finrank ℝ E)) : covMatrix μ i j = ((covarianceBilin μ) ((stdOrthonormalBasis ℝ E) i)) ((stdOrthonormalBasis ℝ E) j)

theorem ProbabilityTheory.covMatrix_mulVec {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] (x : Fin (Module.finrank ℝ E) → ℝ) : (covMatrix μ).mulVec x = fun (i : Fin (Module.finrank ℝ E)) => ((covarianceBilin μ) ((stdOrthonormalBasis ℝ E) i)) (∑ j : Fin (Module.finrank ℝ E), x j • (stdOrthonormalBasis ℝ E) j)

theorem ProbabilityTheory.dotProduct_covMatrix_mulVec {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] (x y : Fin (Module.finrank ℝ E) → ℝ) : x ⬝ᵥ (covMatrix μ).mulVec y = ((covarianceBilin μ) (∑ j : Fin (Module.finrank ℝ E), x j • (stdOrthonormalBasis ℝ E) j)) (∑ j : Fin (Module.finrank ℝ E), y j • (stdOrthonormalBasis ℝ E) j)

theorem ProbabilityTheory.covarianceBilin_eq_dotProduct_covMatrix_mulVec {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] (x y : E) : ((covarianceBilin μ) x) y = ((stdOrthonormalBasis ℝ E).repr x).ofLp ⬝ᵥ (covMatrix μ).mulVec ((stdOrthonormalBasis ℝ E).repr y).ofLp

theorem ProbabilityTheory.covMatrix_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L : E →L[ℝ] F) (i j : Fin (Module.finrank ℝ F)) : covMatrix (MeasureTheory.Measure.map (⇑L) μ) i j = ((stdOrthonormalBasis ℝ E).repr ((ContinuousLinearMap.adjoint L) ((stdOrthonormalBasis ℝ F) i))).ofLp ⬝ᵥ (covMatrix μ).mulVec ((stdOrthonormalBasis ℝ E).repr ((ContinuousLinearMap.adjoint L) ((stdOrthonormalBasis ℝ F) j))).ofLp

theorem ProbabilityTheory.posSemidef_covMatrix {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] : (covMatrix μ).PosSemidef