Covariance matrix

@[simp]

theorem ProbabilityTheory.covarianceBilinDual_self_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] (L : StrongDual ℝ E) : 0 ≤ ((covarianceBilinDual μ) L) L

theorem ProbabilityTheory.isPosSemidef_covarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] : ContinuousBilinForm.IsPosSemidef (covarianceBilinDual μ)

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.

@[simp]

theorem ProbabilityTheory.covInnerBilin_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] : covInnerBilin 0 = 0

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 = ((covarianceBilinDual μ) ((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 μ] (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_real {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x y : ℝ) : ((covInnerBilin μ) x) y = x * y * variance id μ

theorem ProbabilityTheory.covInnerBilin_real_self {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x : ℝ) : ((covInnerBilin μ) x) x = x ^ 2 * variance id μ

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 μ

theorem ProbabilityTheory.covInnerBilin_apply_basisFun {ι : Type u_2} {Ω : Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (i j : ι) : ((covInnerBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) μ)) ((EuclideanSpace.basisFun ι ℝ) i)) ((EuclideanSpace.basisFun ι ℝ) j) = covariance (X i) (X j) μ

theorem ProbabilityTheory.covInnerBilin_apply_basisFun_self {ι : Type u_2} {Ω : Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (i : ι) : ((covInnerBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) μ)) ((EuclideanSpace.basisFun ι ℝ) i)) ((EuclideanSpace.basisFun ι ℝ) i) = variance (X i) μ

theorem ProbabilityTheory.covInnerBilin_apply_pi {ι : Type u_2} {Ω : Type u_3} [Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) (x y : EuclideanSpace ℝ ι) : ((covInnerBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) μ)) x) y = ∑ i : ι, ∑ j : ι, x i * y j * covariance (X i) (X j) μ

theorem ProbabilityTheory.covInnerBilin_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 (ℝ × ℝ)) : ((covInnerBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 (X ω, Y ω)) μ)) x) y = x.1 * y.1 * variance X μ + (x.1 * y.2 + x.2 * y.1) * covariance X Y μ + x.2 * y.2 * variance Y μ

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