English
If X is almost everywhere measurable with respect to μ, then the second marginal of the pushforward μ.map(a ↦ (X(a), Y(a))) equals μ.map(Y).
Русский
Если X почти всюду измерима относительно μ, то вторая маргинальная мера образа μ по a ↦ (X(a), Y(a)) равна μ.map(Y).
LaTeX
$$(X is a.e.-measurable) ⇒ snd(μ.map(a ↦ (X(a), Y(a)))) = μ.map Y$$
Lean4
theorem snd_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hX : AEMeasurable X μ) :
(μ.map fun a => (X a, Y a)).snd = μ.map Y :=
by
by_cases hY : AEMeasurable Y μ
· ext1 s hs
rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs),
Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ, univ_inter]
· have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
contrapose! hY
exact measurable_snd.comp_aemeasurable hY
simp [map_of_not_aemeasurable, hY, this]
