map_comp — Mathlib

English

For a kernel κ, a measure μ on α, and a measurable map f: β → γ, the pushforward of the composition equals the composition of pushforwards: (κ ∘ₘ μ).map f = (κ.map f) ∘ₘ μ.

Русский

Для ядра κ, меры μ на α и измеримого отображения f: β → γ выполняется: (κ ∘ₘ μ).map f = (κ.map f) ∘ₘ μ.

LaTeX

$$$\\text{Measurable } f \\;\\Rightarrow\\; (\\kappa \\circ_{m} \\mu).map f = (\\kappa.map f) \\circ_{m} \\mu$$$

Lean4

theorem map_comp (μ : Measure α) (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : (κ ∘ₘ μ).map f = (κ.map f) ∘ₘ μ :=
  by
  ext s hs
  rw [Measure.map_apply hf hs, Measure.bind_apply (hf hs) κ.aemeasurable, Measure.bind_apply hs (Kernel.aemeasurable _)]
  simp_rw [Kernel.map_apply' _ hf _ hs]

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