Theorems · Theorem · probability

ProbabilityTheory.covarianceBilin_apply_basisFun_self

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

Defined in

Mathlib.Probability.Moments.CovarianceBilin

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeMeasureTheory.IsFiniteMeasure