English
Lebesgue integral against the composition-product equals the iterated integral with curry/uncurry transformation.
Русский
Лебегова интеграл против композиции-произведения равен очередному интегралу с преобразованием карри/анкари.
LaTeX
$$$$ \int f \; d(κ \otimes_k η) a = \int f(b,c) \; dη(a,b) dκ(a) $$$$
Lean4
theorem ae_kernel_lt_top (a : α) (h2s : (κ ⊗ₖ η) a s ≠ ∞) : ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' s) < ∞ :=
by
let t := toMeasurable ((κ ⊗ₖ η) a) s
have : ∀ b : β, η (a, b) (Prod.mk b ⁻¹' s) ≤ η (a, b) (Prod.mk b ⁻¹' t) := fun b =>
measure_mono (Set.preimage_mono (subset_toMeasurable _ _))
have ht : MeasurableSet t := measurableSet_toMeasurable _ _
have h2t : (κ ⊗ₖ η) a t ≠ ∞ := by rwa [measure_toMeasurable]
have ht_lt_top : ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' t) < ∞ :=
by
rw [Kernel.compProd_apply ht] at h2t
exact ae_lt_top (Kernel.measurable_kernel_prodMk_left' ht a) h2t
filter_upwards [ht_lt_top] with b hb
exact (this b).trans_lt hb
