comp_assoc — Mathlib

English

The discard operation after composition equals a kernel sending a to κ(a, Set.univ) scaled by a dirac measure on units.

Русский

Операция отброса после композиции равна ядру, отправляющему a в κ(a, Set.univ) умноженное на диракову меру на единицах.

LaTeX

$$$(\\text{discard } β) \\circ \\kappa = \\{ toFun\\ a := \\kappa(a, \\mathrm{Set.univ}) \\cdot \\mathrm{dirac}(())\\; \\text{measurable'} \\}$$$

Lean4

/-- Composition of kernels is associative. -/
theorem comp_assoc {δ : Type*} {mδ : MeasurableSpace δ} (ξ : Kernel γ δ) (η : Kernel β γ) (κ : Kernel α β) :
    ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ) := by
  refine ext_fun fun a f hf => ?_
  simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel]

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