condKernelCountable — Mathlib

English

If each κCond a is a Markov kernel, then condKernelCountable κCond h_atom is a Markov kernel.

Русский

Если каждый κCond a является марковским ядром, то condKernelCountable κCond h_atom является марковским ядром.

LaTeX

$$$\\text{IsMarkovKernel}( \\text{condKernelCountable}(κCond,h_{atom}) )$$$

Lean4

/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.

A conditional kernel for `κ : Kernel α (β × Ω)` where `α` is countable and `Ω` is a measurable
space. -/
noncomputable def condKernelCountable (h_atom : ∀ x y, x ∈ measurableAtom y → κCond x = κCond y) : Kernel (α × β) Ω
    where
  toFun p := κCond p.1 p.2
  measurable' :=
    by
    refine measurable_from_prod_countable_right' (fun a ↦ (κCond a).measurable) fun x y hx hy ↦ ?_
    simpa using DFunLike.congr (h_atom _ _ hy) rfl

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