English
Let κ be a finite kernel from α to β and η a finite kernel from β to δ, and let μ be a finite measure on γ. Then the product of the constant-μ kernel on β with η, composed with κ, equals the product of the constant-μ kernel on α with the composition of η with κ. Symbolically, ((const_β μ) ×_κ η) ∘_κ κ = (const_α μ) ×_κ (η ∘_κ κ).
Русский
Пусть κ — конечное ядро из α в β, η — конечное ядро из β в δ, и μ — конечная мера на γ. Тогда произведение константного μ-ядра на β с η, составленное с κ, равно произведению константного μ-ядра на α с η, композицию η ∘ κ. То есть ((const_β μ) ×_κ η) ∘_κ κ = (const_α μ) ×_κ (η ∘_κ κ).
LaTeX
$$$$\\bigl((\\mathrm{const}_{\\beta} \\mu) \\times_{\\kappa} \\eta\\bigr) \\circ_{\\kappa} \\kappa = \\bigl(\\mathrm{const}_{\\alpha} \\mu\\bigr) \\times_{\\kappa} (\\eta \\circ_{\\kappa} \\kappa). $$$$
Lean4
theorem const_prod_comp {δ} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (μ : Measure γ) [SFinite μ]
(η : Kernel β δ) [IsSFiniteKernel η] : ((const β μ) ×ₖ η) ∘ₖ κ = (const α μ) ×ₖ (η ∘ₖ κ) :=
by
ext x s ms
simp_rw [comp_apply' _ _ _ ms, prod_apply, Measure.prod_apply_symm ms, const_apply,
lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)]
