English
For a ∈ α and a measurable set s ⊆ β × γ, the left-hand side integral is bounded above by (κ ⊗ₖ η) a s.
Русский
Для фиксированного a и измеримого s ⊆ β × γ имеем неравенство: ∫ η(a,b)({c:(b,c)∈s}) dκ(a)(b) ≤ (κ ⊗ₖ η) a s.
LaTeX
$$$$\int_{\beta} η(a,b)\{c : (b,c) \in s\}\; dκ(a)(b) \le (κ \otimes_k η) a s.$$$$
Lean4
theorem le_compProd_apply (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
(s : Set (β × γ)) : ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂κ a ≤ (κ ⊗ₖ η) a s :=
calc
∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂κ a ≤ ∫⁻ b, η (a, b) {c | (b, c) ∈ toMeasurable ((κ ⊗ₖ η) a) s} ∂κ a :=
lintegral_mono fun _ => measure_mono fun _ h_mem => subset_toMeasurable _ _ h_mem
_ = (κ ⊗ₖ η) a (toMeasurable ((κ ⊗ₖ η) a) s) := (compProd_apply (measurableSet_toMeasurable _ _) κ η a).symm
_ = (κ ⊗ₖ η) a s := measure_toMeasurable s
