prod_const_comp — Mathlib

English

Let κ: α → β and η: β → γ be s-finite, μ a finite measure on δ. Then (η ×K (const β μ)) ∘K κ = (η ∘K κ) ×K (const α μ).

Русский

Пусть κ: α → β и η: β → γ — s-finite, μ — конечная мера на δ. Тогда (η ×K (const β μ)) ∘K κ = (η ∘K κ) ×K (const α μ).

LaTeX

$$$\\displaystyle (\\eta \\times_K (\\mathrm{const }\\; \\beta \\; \\mu)) \\circ_K \\kappa = (\\eta \\circ_K \\kappa) \\times_K (\\mathrm{const }\\; \\alpha \\; \\mu)$$$

Lean4

theorem prod_const_comp {δ} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel β γ)
    [IsSFiniteKernel η] (μ : Measure δ) [SFinite μ] : (η ×ₖ (const β μ)) ∘ₖ κ = (η ∘ₖ κ) ×ₖ (const α μ) :=
  by
  ext x s ms
  simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
    lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]

Похожие утверждения