Covariance matrix

noncomputable def ProbabilityTheory.covInnerBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) : ContinuousBilinForm ℝ E

Covariance of a measure on an inner product space, as a continuous bilinear form.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.covInnerBilin_eq_covarianceBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} (x y : E) : ((covInnerBilin μ) x) y = ((covarianceBilin μ) ((InnerProductSpace.toDualMap ℝ E) x)) ((InnerProductSpace.toDualMap ℝ E) y)

theorem ProbabilityTheory.covInnerBilin_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x y : E) : ((covInnerBilin μ) x) y = ∫ (z : E), inner ℝ x (z - ∫ (x : E), id x ∂μ) * inner ℝ y (z - ∫ (x : E), id x ∂μ) ∂μ

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

theorem ProbabilityTheory.covInnerBilin_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x y : E) : ((covInnerBilin μ) x) y = ((covInnerBilin μ) y) x

theorem ProbabilityTheory.covInnerBilin_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x : E) : ((covInnerBilin μ) x) x = variance (fun (u : E) => inner ℝ x u) μ

theorem ProbabilityTheory.covInnerBilin_apply_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x y : E) : ((covInnerBilin μ) x) y = covariance (fun (u : E) => inner ℝ x u) (fun (u : E) => inner ℝ y u) μ

theorem ProbabilityTheory.covInnerBilin_self_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x : E) : 0 ≤ ((covInnerBilin μ) x) x

theorem ProbabilityTheory.isPosSemidef_covInnerBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) : (covInnerBilin μ).IsPosSemidef

theorem ProbabilityTheory.IsGaussian.isPosSemidef_covInnerBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [SecondCountableTopology E] [CompleteSpace E] [IsGaussian μ] : (covInnerBilin μ).IsPosSemidef

theorem ProbabilityTheory.covInnerBilin_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [CompleteSpace E] [FiniteDimensional ℝ F] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L : E →L[ℝ] F) (u v : F) : ((covInnerBilin (MeasureTheory.Measure.map (⇑L) μ)) u) v = ((covInnerBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)

theorem ProbabilityTheory.covInnerBilin_map_const_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsProbabilityMeasure μ] (c : E) (h : MeasureTheory.MemLp id 2 μ) : covInnerBilin (MeasureTheory.Measure.map (fun (x : E) => c + x) μ) = covInnerBilin μ

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 μ = (ProbabilityTheory.covInnerBilin μ).toMatrix (stdOrthonormalBasis ℝ E).toBasis

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 = ((covInnerBilin μ) ((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)) => ((covInnerBilin μ) ((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 = ((covInnerBilin μ) (∑ j : Fin (Module.finrank ℝ E), x j • (stdOrthonormalBasis ℝ E) j)) (∑ j : Fin (Module.finrank ℝ E), y j • (stdOrthonormalBasis ℝ E) j)

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

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)) ⬝ᵥ (covMatrix μ).mulVec ((stdOrthonormalBasis ℝ E).repr ((ContinuousLinearMap.adjoint L) ((stdOrthonormalBasis ℝ F) j)))

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