English
If η and κ are finite kernels, then η ∘ₖ κ is finite, with bound ≤ κ.bound × η.bound; in particular, the total mass is finite and the bound is the product of bounds.
Русский
Если η и κ – конечные ядра, то их композиция η ∘ₖ κ тоже конечна, причём bound(η ∘ₖ κ) ≤ bound(κ) × bound(η).
LaTeX
$$$ (\eta \circ_K \kappa) \text{ is finite with bound } ≤ (\kappa.\text{bound})(\cdot) (\eta.\text{bound})(\cdot)$$$
Lean4
instance comp (η : Kernel β γ) [IsFiniteKernel η] (κ : Kernel α β) [IsFiniteKernel κ] : IsFiniteKernel (η ∘ₖ κ) :=
by
refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩
calc
(η ∘ₖ κ) a Set.univ
_ ≤ κ a Set.univ * η.bound := (comp_apply_univ_le κ η a)
_ ≤ κ.bound * η.bound := mul_le_mul (measure_le_bound κ a Set.univ) le_rfl zero_le' zero_le'
