English
If ν is a finite measure, then the map x ↦ map (Prod.mk x) ν is measurable.
Русский
Если ν — конечная мера, то отображение x ↦ map (Prod.mk x) ν измеримо.
LaTeX
$$$x \\mapsto \\mathrm{map}(\\mathrm{Prod.mk}\,x)\\, ν$ is measurable.$$
Lean4
/-- If `ν` is a finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is
a measurable function. `measurable_measure_prodMk_left` is strictly more general. -/
theorem measurable_measure_prodMk_left_finite [IsFiniteMeasure ν] {s : Set (α × β)} (hs : MeasurableSet s) :
Measurable fun x => ν (Prod.mk x ⁻¹' s) := by
induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
| empty => simp
| basic s hs =>
obtain ⟨s, hs, t, -, rfl⟩ := hs
classical simpa only [mk_preimage_prod_right_eq_if, measure_if] using measurable_const.indicator hs
| compl s hs
ihs =>
simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
exact ihs.const_sub _
| iUnion f hfd hfm
ihf =>
have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) :=
by
rw [preimage_iUnion, measure_iUnion]
exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
simpa only [this] using Measurable.ennreal_tsum ihf
