deterministic_comp_eq_map — Mathlib

English

For hf measurable and κ a kernel, the composition of the deterministic kernel with κ equals the map κ maps: deterministic f hf ∘ₖ κ = map κ f.

Русский

Для измеримого hf и ядра κ композиция детерминированного ядра с κ равна отображению, которое задаёт κ: deterministic f hf ∘ₖ κ = map κ f.

LaTeX

$$$ (\text{deterministic } f hf) \circ_K \kappa = \kappa \map f $$$

Lean4

theorem deterministic_comp_eq_map {f : α → β} (hf : Measurable f) : Kernel.deterministic f hf ∘ₘ μ = μ.map f :=
  Measure.bind_dirac_eq_map μ hf

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