離散確率と PMF¶
離散確率では，可測性が問題にならないことが多いです．
Mathlib では [DiscreteMeasurableSpace Ω] が「すべての集合が可測である」ことを表します．
その場合，任意の関数 X : Ω → E は可測関数になります．
確率質量関数は PMF Ω で表されます．
p : PMF Ω から測度 p.toMeasure : Measure Ω を作ることができ，これは確率測度です．
有限集合上の一様分布や Bernoulli 分布も PMF として用意されています．
section DiscreteProbability
variable {Ω E : Type*}
variable [MeasurableSpace Ω] [DiscreteMeasurableSpace Ω]
variable [MeasurableSpace E]
#check DiscreteMeasurableSpace
#check MeasurableSet.of_discrete
#check Measurable.of_discrete
#check PMF
#check PMF.toMeasure
#check PMF.uniformOfFintype
#check PMF.bernoulli
example (s : Set Ω) : MeasurableSet s := by
exact MeasurableSet.of_discrete
example (X : Ω → E) : Measurable X := by
exact Measurable.of_discrete
example (p : PMF Ω) : IsProbabilityMeasure p.toMeasure := by
infer_instance
example (p : PMF Ω) : p.toMeasure univ = 1 := by
simp
end DiscreteProbability
演習問題¶
-
離散可測空間では任意の集合が可測であることを確認してください．
-
PMFから作った測度が確率測度であることを確認してください．