comp_deterministic_eq_comap — Mathlib

English

If f and g are measurable, then deterministic g hg ∘ₖ deterministic f hf equals deterministic (g ∘ f) with hg.comp hf.

Русский

Если f и g измеримы, то детерминированная композиция равна детерминированной композиции функций.

LaTeX

$$$ (\text{deterministic } g) \circ_K (\text{deterministic } f) = \text{deterministic } (g \circ f)$$$

Lean4

theorem comp_deterministic_eq_comap (κ : Kernel α β) (hg : Measurable g) : κ ∘ₖ deterministic g hg = comap κ g hg :=
  by
  ext a s hs
  simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
    lintegral_dirac' _ (Kernel.measurable_coe κ hs)]

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