Covariance bilinear form

theorem ProbabilityTheory.covarianceBilin_comm {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : NormedSpace.Dual ℝ E) : ((covarianceBilin μ) L₁) L₂ = ((covarianceBilin μ) L₂) L₁

theorem ProbabilityTheory.covarianceBilin_apply' {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : NormedSpace.Dual ℝ E) : ((covarianceBilin μ) L₁) L₂ = ∫ (x : E), L₁ (x - ∫ (x : E), id x ∂μ) * L₂ (x - ∫ (x : E), id x ∂μ) ∂μ

theorem ProbabilityTheory.covarianceBilin_apply'' {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : NormedSpace.Dual ℝ E) : ((covarianceBilin μ) L₁) L₂ = covariance (⇑L₁) (⇑L₂) μ