English
If X, Y, f are a.e. measurable with respect to ν, then condDistrib Y X (ν) equals the pushforward kernel under f of condDistrib (Y∘f) (X∘f) ν.
Русский
Если X, Y, f а.е. измеримы относительно ν, то condDistrib Y X (ν) равняется отображению через f для condDistrib (Y∘f) (X∘f) ν.
LaTeX
$$$$ \\mathrm{condDistrib}(Y,X,ν) =_{a.e.} \\mathrm{condDistrib}(Y\\circ f, X\\circ f, ν). $$$$
Lean4
theorem condDistrib_comp {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace Ω'] [Nonempty Ω'] (X : α → β)
(hY : AEMeasurable Y μ) {f : Ω → Ω'} (hf : Measurable f) :
condDistrib (f ∘ Y) X μ =ᵐ[μ.map X] (condDistrib Y X μ).map f :=
by
by_cases hX : AEMeasurable X μ
swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_
calc
μ.map (fun x ↦ (X x, (f ∘ Y) x))
_ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) :=
by
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
rfl
_ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY]
_ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf]
