English
Under a measurable map Y: Ω' → Ω, Var[X; μ.map Y] equals Var[X ∘ Y; μ], i.e., variance is preserved under pushforward.
Русский
При измеримом отображении Y: Ω' → Ω дисперсия сохраняется: Var[X; μ.map Y] = Var[X ∘ Y; μ].
LaTeX
$$$$ \mathrm{variance}(X; \mu.map Y) = \mathrm{variance}(X \circ Y; \mu). $$$$
Lean4
theorem variance_map {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ : Measure Ω'} {Y : Ω' → Ω}
(hX : AEMeasurable X (μ.map Y)) (hY : AEMeasurable Y μ) : Var[X; μ.map Y] = Var[X ∘ Y; μ] :=
by
rw [variance_eq_integral hX, integral_map hY, variance_eq_integral (hX.comp_aemeasurable hY), integral_map hY]
· congr
· exact hX.aestronglyMeasurable
· refine AEStronglyMeasurable.pow ?_ _
exact AEMeasurable.aestronglyMeasurable (by fun_prop)
