instIsMarkovKernelBorelMarkovFromReal

English

If η is Markov, then borelMarkovFromReal Ω η is Markov.

Русский

Если η является ядром Маркова, то borelMarkovFromReal Ω η — ядро Маркова.

LaTeX

$$$IsMarkovKernel(\\mathrm{borelMarkovFromReal}\\,Ω\\,η)$$$

Lean4

/-- When `η` is a Markov kernel, `borelMarkovFromReal Ω η` is a Markov kernel. -/
instance instIsMarkovKernelBorelMarkovFromReal (η : Kernel α ℝ) [IsMarkovKernel η] :
    IsMarkovKernel (borelMarkovFromReal Ω η) :=
  by
  refine IsMarkovKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) (fun a ↦ ?_)
  classical
  rw [piecewise_apply]
  split_ifs with h
  · rwa [← prob_compl_eq_zero_iff (measurableEmbedding_embeddingReal Ω).measurableSet_range]
  · rw [deterministic_apply]
    simp [(range_nonempty (embeddingReal Ω)).choose_spec]

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