Theorems · Theorem · probability

ProbabilityTheory.covarianceBilinDual_apply

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E),
      ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ =
        ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

Defined in

Mathlib.Probability.Moments.CovarianceBilinDual

Cited by

2 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceBorelSpaceCompleteSpaceMeasureTheory.IsFiniteMeasure