English
AEStronglyMeasurable f μ is equivalent to AEStronglyMeasurable (λ x => f x.snd) under the map ω ↦ (X ω, ω).
Русский
AEStronglyMeasurable f μ эквивалентно AEStronglyMeasurable (λx, f x.snd) под отображением ω ↦ (X ω, ω).
LaTeX
$$$$ \\text{AEStronglyMeasurable}(f, μ) \\iff \\text{AEStronglyMeasurable}(λx, f x.2, μ.map ω ↦ (X ω, ω)). $$$$
Lean4
theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk {Ω F} {mΩ : MeasurableSpace Ω} (X : Ω → β)
{μ : Measure Ω} [TopologicalSpace F] {f : Ω → F} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) :=
by
refine ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩
suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω ↦ (X ω, ω)) μ from
Measure.QuasiMeasurePreserving.ae_eq h hf.ae_eq_mk
refine ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => ?_⟩
rw [Measure.map_apply _ hs]
swap; · exact measurable_snd
by_cases hX : AEMeasurable X μ
· rw [Measure.map_apply_of_aemeasurable]
· rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id']
exact hμs
· exact hX.prodMk aemeasurable_id
· exact measurable_snd hs
· rw [Measure.map_of_not_aemeasurable]
· simp
· contrapose! hX; exact measurable_fst.comp_aemeasurable hX
