English
For a kernel η with IsSFinite, and a measurable t ⊆ α × β, the map a ↦ ∫⁻ b, t(a,b) dη(a,b) is measurable in a.
Русский
Для ядра η с условием IsSFinite и измеримого t ⊆ α × β отображение a ↦ ∫ t(a,b) dη(a,b) измеримо по a.
LaTeX
$$$\\text{Measurable}\\bigl(a \\mapsto \\int\\!^{⁻} b\, t(a,b) \\, d\\eta(a,b)\\bigr)$$$
Lean4
/-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0∞` which is measurable when seen as a
map from `α × β` (hypothesis `Measurable (uncurry f)`), the integral `a ↦ ∫⁻ b, f a b ∂(κ a)` is
measurable. -/
@[fun_prop]
theorem _root_.Measurable.lintegral_kernel_prod_right {f : α → β → ℝ≥0∞} (hf : Measurable (uncurry f)) :
Measurable fun a => ∫⁻ b, f a b ∂κ a :=
by
let F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
have h : ∀ a, ⨆ n, F n a = uncurry f a := SimpleFunc.iSup_eapprox_apply hf
simp only [Prod.forall, uncurry_apply_pair] at h
simp_rw [← h]
have : ∀ a, (∫⁻ b, ⨆ n, F n (a, b) ∂κ a) = ⨆ n, ∫⁻ b, F n (a, b) ∂κ a :=
by
intro a
rw [lintegral_iSup]
· exact fun n => (F n).measurable.comp measurable_prodMk_left
· exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _
simp_rw [this]
refine .iSup fun n => ?_
refine SimpleFunc.induction (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)
· intro c t ht
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
Set.piecewise_eq_indicator]
exact Kernel.measurable_lintegral_indicator_const (κ := κ) ht c
· intro g₁ g₂ _ hm₁ hm₂
simp only [SimpleFunc.coe_add, Pi.add_apply]
have h_add :
(fun a => ∫⁻ b, g₁ (a, b) + g₂ (a, b) ∂κ a) = (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a :=
by
ext1 a
rw [Pi.add_apply, lintegral_add_left (g₁.measurable.comp' measurable_prodMk_left)]
rw [h_add]
exact Measurable.add hm₁ hm₂
