Theorems · Theorem · probability

ProbabilityTheory.variance_map

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω},
  AEMeasurable X (MeasureTheory.Measure.map Y μ) →
    AEMeasurable Y μ →
      ProbabilityTheory.variance X (MeasureTheory.Measure.map Y μ) = ProbabilityTheory.variance (X ∘ Y) μ

Defined in

Mathlib.Probability.Moments.Variance

Cited by

11 results in Mathlib

Foundations

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