Theorems · Theorem · probability

ProbabilityTheory.covarianceBilin_apply_pi

∀ {ι : Type u_2} {Ω : Type u_3} [inst : Fintype ι] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    ∀ (x y : EuclideanSpace ℝ ι),
      ((ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun ω => WithLp.toLp 2 fun x => X x ω) μ)) x) y =
        ∑ i, ∑ j, x.ofLp i * y.ofLp j * ProbabilityTheory.covariance (X i) (X j) μ

Defined in

Mathlib.Probability.Moments.CovarianceBilin

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeMeasureTheory.IsFiniteMeasure