variance_map_equiv — Mathlib

English

Let X: Ω → ℝ and Y: Ω′ ≃ᵐ Ω be a measurable equivalence. Then the variance of X with respect to μ.map Y equals the variance of X∘Y with respect to μ.

Русский

Пусть X: Ω → ℝ и Y: Ω′ ≃ᵐ Ω — меромонообразование. Тогда дисперсия X по мере μ.map Y равна дисперсии X∘Y по мере μ.

LaTeX

$$$\operatorname{Var}[X;\, \mu.map Y] = \operatorname{Var}[X\circ Y;\, \mu]$$$

Lean4

theorem variance_map_equiv {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ : Measure Ω'} (X : Ω → ℝ) (Y : Ω' ≃ᵐ Ω) :
    Var[X; μ.map Y] = Var[X ∘ Y; μ] := by
  simp_rw [variance, evariance, lintegral_map_equiv, integral_map_equiv, Function.comp_apply]

Похожие утверждения