Theorems · Theorem · probability

ProbabilityTheory.covarianceBilin_apply_eq_cov

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (x y : E),
      ((ProbabilityTheory.covarianceBilin μ) x) y =
        ProbabilityTheory.covariance (fun u => inner ℝ x u) (fun u => inner ℝ y u) μ

Defined in

Mathlib.Probability.Moments.CovarianceBilin

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceCompleteSpaceMeasureTheory.IsFiniteMeasure