English
For X : α → β and Y : α → γ with μ-measurable Y, (μ.map a ↦ (X a, Y a)).fst = μ.map X.
Русский
Для X: α→β и Y: α→γ, если Y измерима по μ, то (μ.map a ↦ (X a, Y a)).fst = μ.map X.
LaTeX
$$$$ (\\mu.\\mathrm{map}\\ (\\lambda a, (X a, Y a))).fst = \\mu.\\mathrm{map} X $$$$
Lean4
theorem fst_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hY : AEMeasurable Y μ) :
(μ.map fun a => (X a, Y a)).fst = μ.map X :=
by
by_cases hX : AEMeasurable X μ
· ext1 s hs
rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs),
Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ, inter_univ]
· have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
contrapose! hX
exact measurable_fst.comp_aemeasurable hX
simp [map_of_not_aemeasurable, hX, this]
