Markov kernel¶
Markov kernel は，状態 a : α ごとに測度 κ a : Measure β を返す可測な写像です．
Mathlib では Kernel α β が kernel を表し，その各値が確率測度であることを IsMarkovKernel κ で表します．
参照論文では，Mathlib の確率論ライブラリが Markov kernel を広く使っていることが説明されています． 条件付き分布，posterior distribution，独立性・条件付き独立性の統一的な定義，sub-Gaussian random variables，entropy，Kullback-Leibler divergence などで kernel が中心的な役割を持ちます． この章では入口だけを見ます．
section MarkovKernels
variable {α β : Type*}
variable [MeasurableSpace α] [MeasurableSpace β]
#check Kernel
#check IsMarkovKernel
#check IsFiniteKernel
#check IsSFiniteKernel
#check Kernel.measurable
#check Kernel.bound
#check Kernel.deterministic
#check condDistrib
example (κ : Kernel α β) : Measurable κ := by
exact κ.measurable
example (κ : Kernel α β) [IsMarkovKernel κ] (a : α) : κ a univ = 1 := by
simp
example : IsFiniteKernel (0 : Kernel α β) := by
infer_instance
variable {f : α → β} (hf : Measurable f)
example : IsMarkovKernel (Kernel.deterministic f hf) := by
infer_instance
example (a : α) : Kernel.deterministic f hf a = Measure.dirac (f a) := by
exact Kernel.deterministic_apply hf a
end MarkovKernels
演習問題¶
deterministic kernel が Dirac 測度を返すことを確認してください．