Documentation

BrownianMotion.Gaussian.CovMatrix

Covariance matrix #

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

E →L[ℝ ] E →L[ℝ ] ℝ

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

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_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.covInnerBilin_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] [CompleteSpace E] [CompleteSpace 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)

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 μ = Matrix.of fun (i j : Fin (Module.finrank ℝ E)) => ((ProbabilityTheory.covInnerBilin μ) ((stdOrthonormalBasis ℝ E) i)) ((stdOrthonormalBasis ℝ E) j)

Instances For

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.posSemidef_covMatrix {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [IsGaussian μ] :

(covMatrix μ).PosSemidef