English
A short-form result for deterministic function application inside compProd, using indicator of membership in s.
Русский
Сокращённый результат детерминированного отображения внутри compProd через индикатор принадлежности к s.
LaTeX
$$$$ (κ \otimes_k deterministic f) x s = κ x \{ b \mid (b, f(x,b)) \in s \}. $$$$
Lean4
/-- Lebesgue integral against the composition-product of two kernels. -/
theorem lintegral_compProd' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
{f : β → γ → ℝ≥0∞} (hf : Measurable (Function.uncurry f)) :
∫⁻ bc, f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c, f b c ∂η (a, b) ∂κ a :=
by
let F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
have h : ∀ a, ⨆ n, F n a = Function.uncurry f a := SimpleFunc.iSup_eapprox_apply hf
simp only [Prod.forall, Function.uncurry_apply_pair] at h
simp_rw [← h]
have h_mono : Monotone F := fun i j hij b => SimpleFunc.monotone_eapprox (Function.uncurry f) hij _
rw [lintegral_iSup (fun n => (F n).measurable) h_mono]
have : ∀ b, ∫⁻ c, ⨆ n, F n (b, c) ∂η (a, b) = ⨆ n, ∫⁻ c, F n (b, c) ∂η (a, b) :=
by
intro a
rw [lintegral_iSup]
· exact fun n => (F n).measurable.comp measurable_prodMk_left
· exact fun i j hij b => h_mono hij _
simp_rw [this]
have h_some_meas_integral : ∀ f' : SimpleFunc (β × γ) ℝ≥0∞, Measurable fun b => ∫⁻ c, f' (b, c) ∂η (a, b) :=
by
intro f'
have : (fun b => ∫⁻ c, f' (b, c) ∂η (a, b)) = (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by ext1 ab;
rfl
rw [this]
fun_prop
rw [lintegral_iSup]
rotate_left
· exact fun n => h_some_meas_integral (F n)
· exact fun i j hij b => lintegral_mono fun c => h_mono hij _
congr
ext1 n
refine SimpleFunc.induction ?_ ?_ (F n)
· intro c s hs
simp +unfoldPartialApp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
SimpleFunc.coe_zero, Set.piecewise_eq_indicator, Function.const, lintegral_indicator_const hs]
rw [compProd_apply hs, ← lintegral_const_mul c _]
swap
· exact (measurable_kernel_prodMk_left ((measurable_fst.snd.prodMk measurable_snd) hs)).comp measurable_prodMk_left
congr
ext1 b
rw [lintegral_indicator_const_comp measurable_prodMk_left hs]
· intro f f' _ hf_eq hf'_eq
simp_rw [SimpleFunc.coe_add, Pi.add_apply]
change ∫⁻ x, (f : β × γ → ℝ≥0∞) x + f' x ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c : γ, f (b, c) + f' (b, c) ∂η (a, b) ∂κ a
rw [lintegral_add_left (SimpleFunc.measurable _), hf_eq, hf'_eq, ← lintegral_add_left]
swap
· exact h_some_meas_integral f
congr with b
rw [lintegral_add_left]
exact (SimpleFunc.measurable _).comp measurable_prodMk_left
