English
Let μ be a measure on Ω and ν a measure on Ω′, and let X: Ω → Ω′ be measure-preserving (i.e., ν is the push-forward of μ by X). For every AEMeasurable function f: Ω′ → ℝ, the variance of f∘X with respect to μ equals the variance of f with respect to ν.
Русский
Пусть μ — мера на Ω, ν — мера на Ω′, и X: Ω → Ω′ является отображением, сохраняющим меру (ν — образ μ по X). Для любой AEMeasurable функции f: Ω′ → ℝ дисперсия f∘X по μ равна дисперсии f по ν.
LaTeX
$$$\operatorname{Var}[f\circ X;\, \mu] = \operatorname{Var}[f;\, \nu]$$$
Lean4
theorem _root_.MeasureTheory.MeasurePreserving.variance_fun_comp {Ω' : Type*} {mΩ' : MeasurableSpace Ω'}
{ν : Measure Ω'} {X : Ω → Ω'} (hX : MeasurePreserving X μ ν) {f : Ω' → ℝ} (hf : AEMeasurable f ν) :
Var[fun ω ↦ f (X ω); μ] = Var[f; ν] := by
rw [← hX.map_eq, variance_map (hX.map_eq ▸ hf) hX.aemeasurable, Function.comp_def]
