# Covariance matrix #

source
theorem ProbabilityTheory.isPosSemidef_covarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} :
ContinuousBilinForm.IsPosSemidef (covarianceBilinDual μ)
source
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.

Instances For

source
@[simp]
theorem ProbabilityTheory.covInnerBilin_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] :
covInnerBilin 0 = 0
source
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)
source
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 ∂μ) ∂μ
source
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 ∂μ) ∂μ
source
theorem ProbabilityTheory.covInnerBilin_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} (x y : E) :
((covInnerBilin μ) x) y = ((covInnerBilin μ) y) x
source
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) μ
source
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) μ
source
theorem ProbabilityTheory.covInnerBilin_real {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x y : ℝ) :
((covInnerBilin μ) x) y = x * y * variance id μ
source
theorem ProbabilityTheory.covInnerBilin_real_self {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (x : ℝ) :
((covInnerBilin μ) x) x = x ^ 2 * variance id μ
source
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
source
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
source
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
source
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)
source
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 μ
source
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) μ
source
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) μ
source
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.ofLp i * y.ofLp j * covariance (X i) (X j) μ
source
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.fst * y.fst * variance X μ + (x.fst * y.snd + x.snd * y.fst) * covariance X Y μ + x.snd * y.snd * variance Y μ
source
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

Instances For

source
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)
source
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)
source
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)
source
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).ofLp ⬝ᵥ (covMatrix μ).mulVec ((stdOrthonormalBasis ℝ E).repr y).ofLp
source
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
source
theorem ProbabilityTheory.posSemidef_covMatrix {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [IsGaussian μ] :
(covMatrix μ).PosSemidef