English
For κ and η as above and a measurable embedding f, comapRight (κ ⊗ η) along id.prodMap f equals κ ⊗ (comapRight η f).
Русский
Для ядер κ и η и измеримого вложения f верно: comapRight(κ ⊗ η) вдоль id.prodMap f равно κ ⊗ (comapRight η f).
LaTeX
$$$$ \\mathrm{comapRight}(κ \\otimes_{\\kern-0.2em} η) (\\mathrm{MeasurableEmbedding.id.prodMap}\, f) \;=\; κ \\otimes_{\\kern-0.2em} (\\mathrm{comapRight} η f). $$$$
Lean4
theorem compProd_apply_univ_le (κ : Kernel α β) (η : Kernel (α × β) γ) [IsFiniteKernel η] (a : α) :
(κ ⊗ₖ η) a Set.univ ≤ κ a Set.univ * η.bound :=
by
by_cases hκ : IsSFiniteKernel κ
swap
· rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
simp
rw [compProd_apply .univ]
let Cη := η.bound
calc
∫⁻ b, η (a, b) Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a := lintegral_mono fun b => measure_le_bound η (a, b) Set.univ
_ = Cη * κ a Set.univ := (MeasureTheory.lintegral_const Cη)
_ = κ a Set.univ * Cη := mul_comm _ _
