comapRight — Mathlib

English

If κ is a Markov kernel and the image of the embedding f carries total mass 1 for every a, then comapRight κ hf is a Markov kernel.

Русский

Если κ — марковское ядро и масса κ(a) на образе f равна 1 для всех a, тогда comapRight κ hf — марковское ядро.

LaTeX

$$$\\text{IsMarkovKernel}(\\kappa\\, hf)$, given $\\forall a, κ(a)(\\mathrm{range}(f)) = 1$$$

Lean4

theorem comapRight (κ : Kernel α β) (hf : MeasurableEmbedding f) (hκ : ∀ a, κ a (Set.range f) = 1) :
    IsMarkovKernel (comapRight κ hf) := by
  refine ⟨fun a => ⟨?_⟩⟩
  rw [comapRight_apply' κ hf a MeasurableSet.univ]
  simp only [Set.image_univ]
  exact hκ a

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