comp_right — Mathlib

English

If μ ≪ ν, then κ ∘ₘ μ ≪ κ ∘ₘ ν for any kernel κ.

Русский

Если μ ⪯ ν, то κ ∘ μ ⪯ κ ∘ ν для любого ядра κ.

LaTeX

$$$\\mu \\ll \\nu \\Rightarrow (\\kappa \\circ_{m} \\mu) \\ll (\\kappa \\circ_{m} \\nu)$$$

Lean4

theorem comp_right (hμν : μ ≪ ν) (κ : Kernel α γ) : κ ∘ₘ μ ≪ κ ∘ₘ ν :=
  by
  refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
  rw [Measure.bind_apply hs (Kernel.aemeasurable _), lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢
  exact hμν.ae_eq hs_zero

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