English
For sfinite μ, the map y ↦ map (λ x. (x,y)) μ is measurable.
Русский
Пусть μ σ-вфинитe; отображение y ↦ map (λ x. (x,y)) μ измеримо.
LaTeX
$$$y \\mapsto \\mathrm{map}(\\lambda x. (x,y))\\, μ$ is measurable.$$
Lean4
/-- If `ν` is an s-finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }`
is a measurable function.
Not true without the s-finite assumption: on `ℝ × ℝ` with the product sigma-algebra, let `s` be the
diagonal and let `ν` be an uncountable sum of Dirac measures (all Dirac measures for points in a
set `t`). Then `ν (Prod.mk x ⁻¹' s) = ν {x} = if x ∈ t then 1 else 0`. If `t` is chosen
non-measurable, this will not be measurable. -/
theorem measurable_measure_prodMk_left [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
Measurable fun x => ν (Prod.mk x ⁻¹' s) := by
rw [← sum_sfiniteSeq ν]
simp_rw [Measure.sum_apply_of_countable]
exact Measurable.ennreal_tsum (fun i ↦ measurable_measure_prodMk_left_finite hs)
