English
Pushforward and conditioning commute under a measurable embedding i, almost every ω lies in range i, and S is measurable.
Русский
Перемещение меры и условие коммутируют при измеримой вложенности i, почти наверняка ω лежит в образе range i, и S измеримо.
LaTeX
$$$\\text{comap } i\\, μ[|S] = (\\text{comap } i\\, μ)[|i \\text{ in } S]$ under appropriate hi and measurability assumptions$$
Lean4
theorem comap_cond {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ ω ∂μ, ω ∈ range i) (hs : MeasurableSet s) :
comap i μ[|s] = (comap i μ)[|i in s] := by
ext t ht
change μ (range i)ᶜ = 0 at hi'
rw [cond_apply, comap_apply, cond_apply, comap_apply, comap_apply, image_inter, image_preimage_eq_inter_range,
inter_right_comm, measure_inter_conull hi', measure_inter_conull hi']
all_goals
first
| exact hi.injective
| exact hi.measurableSet_image'
| exact hs
| exact ht
| exact hi.measurable hs
| exact (hi.measurable hs).inter ht
