Theorems · Theorem · probability

ProbabilityTheory.variance_sum_pi

∀ {ι : Type u_2} [inst : Fintype ι] {Ω : ι → Type u_3} {mΩ : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {X : (i : ι) → Ω i → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 (μ i)) →
    ProbabilityTheory.variance (∑ i, fun ω => X i (ω i)) (MeasureTheory.Measure.pi μ) =
      ∑ i, ProbabilityTheory.variance (X i) (μ i)

Defined in

Mathlib.Probability.Moments.Variance

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeMeasureTheory.IsProbabilityMeasure