instIsCondKernel — Mathlib

English

Under countability, κCond conditions imply κIsCondKernel via condKernelCountable.

Русский

При счетности условия κCond порождают κIsCondKernel через condKernelCountable.

LaTeX

$$$\\kappa^{\\text{Cond}}\\;\\Rightarrow\\; κIsCondKernel(condKernelCountable(κCond,h_{atom}))$$$

Lean4

instance instIsCondKernel [∀ a, IsMarkovKernel (κCond a)] (h_atom : ∀ x y, x ∈ measurableAtom y → κCond x = κCond y)
    (κ : Kernel α (β × Ω)) [IsSFiniteKernel κ] [∀ a, (κ a).IsCondKernel (κCond a)] :
    κ.IsCondKernel (condKernelCountable κCond h_atom) :=
  by
  constructor
  ext a s hs
  conv_rhs => rw [← (κ a).disintegrate (κCond a)]
  simp_rw [compProd_apply hs, condKernelCountable_apply, Measure.compProd_apply hs]
  congr

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