Covariance in Hilbert spaces

Given a measure μ defined over a Banach space E, one can consider the associated covariance bilinear form which maps L₁ L₂ : StrongDual ℝ E to cov[L₁, L₂; μ]. This is called covarianceBilinDual μ and is defined in the CovarianceBilinDual file.

In the special case where E is a Hilbert space, each L : StrongDual ℝ E can be represented as the scalar product against some element of E. This motivates the definition of covarianceBilin, which is a continuous bilinear form mapping x y : E to cov[⟪x, ·⟫, ⟪y, ·⟫; μ].

Main definitions

• covarianceBilin μ: the continuous bilinear form over E representing the covariance of a measure over E.
• covarianceOperator μ: the bounded operator over E such that ⟪covarianceOperator μ x, y⟫ = ∫ z, ⟪x, z⟫ * ⟪y, z⟫ ∂μ.

Tags

covariance, Hilbert space, bilinear form

noncomputable def ProbabilityTheory.covarianceBilin {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.

@[simp]

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

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

@[simp]

theorem ProbabilityTheory.covarianceBilin_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} (h : ¬MeasureTheory.MemLp id 2 μ) : covarianceBilin μ = 0

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) x) y = ∫ (z : E), inner ℝ x (z - ∫ (x : E), id x ∂μ) * inner ℝ y (z - ∫ (x : E), id x ∂μ) ∂μ

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

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) x) x = variance (fun (u : E) => inner ℝ x u) μ

theorem ProbabilityTheory.covarianceBilin_apply_eq_cov {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) : ((covarianceBilin μ) x) y = covariance (fun (u : E) => inner ℝ x u) (fun (u : E) => inner ℝ y u) μ

theorem ProbabilityTheory.covarianceBilin_real {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (x y : ℝ) : ((covarianceBilin μ) x) y = x * y * variance id μ

theorem ProbabilityTheory.covarianceBilin_real_self {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (x : ℝ) : ((covarianceBilin μ) x) x = x ^ 2 * variance id μ

@[simp]

theorem ProbabilityTheory.covarianceBilin_self_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} (x : E) : 0 ≤ ((covarianceBilin μ) x) x

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

theorem ProbabilityTheory.covarianceBilin_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] [SecondCountableTopology F] [CompleteSpace F] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L : E →L[ℝ] F) (u v : F) : ((covarianceBilin (MeasureTheory.Measure.map (⇑L) μ)) u) v = ((covarianceBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)

theorem ProbabilityTheory.covarianceBilin_map_const_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsProbabilityMeasure μ] (c : E) : covarianceBilin (MeasureTheory.Measure.map (fun (x : E) => c + x) μ) = covarianceBilin μ

theorem ProbabilityTheory.covarianceBilin_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 : ι) : ((covarianceBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) μ)) ((EuclideanSpace.basisFun ι ℝ) i)) ((EuclideanSpace.basisFun ι ℝ) j) = covariance (X i) (X j) μ

theorem ProbabilityTheory.covarianceBilin_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 : ι) : ((covarianceBilin (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) μ)) ((EuclideanSpace.basisFun ι ℝ) i)) ((EuclideanSpace.basisFun ι ℝ) i) = variance (X i) μ

theorem ProbabilityTheory.covarianceBilin_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 ℝ ι) : ((covarianceBilin (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) μ

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

The covariance operator of the measure μ. This is the bounded operator F : E →L[ℝ] E associated to the continuous bilinear form B : E →L[ℝ] E →L[ℝ] ℝ such that B x y = ∫ z, ⟪x, z⟫ * ⟪y, z⟫ ∂μ (see covarianceOperator_inner). Namely we have B x y = ⟪F x, y⟫.

Note that the bilinear form B is the uncentered covariance bilinear form associated to the measure µ, which is not to be confused with the covariance bilinear form defined earlier in this file as covarianceBilin μ.

@[simp]

theorem ProbabilityTheory.covarianceOperator_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E] : covarianceOperator 0 = 0

@[simp]

theorem ProbabilityTheory.covarianceOperator_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] (hμ : ¬MeasureTheory.MemLp id 2 μ) : covarianceOperator μ = 0

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

theorem ProbabilityTheory.covarianceOperator_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] (hμ : MeasureTheory.MemLp id 2 μ) (x : E) : (covarianceOperator μ) x = ∫ (y : E), inner ℝ x y • y ∂μ

theorem ProbabilityTheory.isPositive_covarianceOperator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] : (↑(covarianceOperator μ)).IsPositive