Theorems · Theorem · probability

ProbabilityTheory.variance_map_equiv

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

Defined in

Mathlib.Probability.Moments.Variance

Cited by

1 results in Mathlib

Foundations

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