English
Let t be a measurable set in α×β and suppose κ_a are finite measures for all a. Then the map a ↦ κ_a(Prod.mk a^{-1} t) is measurable.
Русский
Пусть t — измеримое множество в α×β, и пусть для всех a мера κ_a конечна. Тогда отображение a ↦ κ_a(Prod.mk a^{-1} t) измеримо.
LaTeX
$$$ \text{Measurable}\bigl(a \mapsto \kappa a\bigl(\operatorname{Prod.mk} a^{-1}' t\bigr)\bigr) $$$
Lean4
/-- This is an auxiliary lemma for `measurable_kernel_prodMk_left`. -/
theorem measurable_kernel_prodMk_left_of_finite {t : Set (α × β)} (ht : MeasurableSet t)
(hκs : ∀ a, IsFiniteMeasure (κ a)) : Measurable fun a => κ a (Prod.mk a ⁻¹' t) := by
-- `t` is a measurable set in the product `α × β`: we use that the product σ-algebra is generated
-- by boxes to prove the result by induction.
induction t, ht using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
| empty => simp only [preimage_empty, measure_empty, measurable_const]
| basic t ht =>
simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht
classical
simp_rw [mk_preimage_prod_right_eq_if]
have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 :=
by
ext1 a
split_ifs
exacts [rfl, measure_empty]
rw [h_eq_ite]
exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const
| compl t htm
iht =>
have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' tᶜ = Set.univ \ Prod.mk a ⁻¹' t :=
by
intro a
ext1 b
simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]
simp_rw [h_eq_sdiff]
have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) = fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) :=
by
ext1 a
rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
· exact (measurable_prodMk_left htm).nullMeasurableSet
· exact measure_ne_top _ _
rw [this]
exact Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht
| iUnion f h_disj hf_meas
hf =>
have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) :=
by
rw [preimage_iUnion, measure_iUnion]
· exact h_disj.mono fun _ _ ↦ .preimage _
· exact fun i ↦ measurable_prodMk_left (hf_meas i)
simpa only [this] using Measurable.ennreal_tsum hf
