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)
:
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)
: