確率変数，分布，期待値¶
確率変数は，測度空間から可測空間への可測関数です．
Lean では関数 X : Ω → E と可測性の仮定 hX : Measurable X を分けて持ちます．
確率変数 X の分布は，測度の push-forward P.map X です．
期待値は積分で，∫ ω, X ω ∂P と書けます．
確率論スコープでは P[X] という記法も使えます．
section RandomVariables
variable {Ω E : Type*}
variable [MeasurableSpace Ω] [MeasurableSpace E]
variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
variable {P : Measure Ω} [IsProbabilityMeasure P]
variable {X Y : Ω → E}
#check Measurable
#check Measure.map
#check (P.map X)
#check (fun X : Ω → ℝ => P[X])
example {X : Ω → E} (hX : AEMeasurable X P) : IsProbabilityMeasure (P.map X) := by
exact Measure.isProbabilityMeasure_map hX
example (c : E) : ∫ _ : Ω, c ∂P = c := by
simp
example {X Y : Ω → E} (hX : Integrable X P) (hY : Integrable Y P) :
∫ ω, X ω + Y ω ∂P = ∫ ω, X ω ∂P + ∫ ω, Y ω ∂P := by
exact integral_add hX hY
end RandomVariables
P[X] は Bochner 積分の記法です．
したがって値域 E にはノルム空間の構造が必要です．
ℝ≥0∞ 値の非負関数を積分するときは，前章で見た Lebesgue 積分 ∫⁻ を使います．
この点は紙の確率論では同じ「期待値」と呼ばれがちですが，Mathlib では型によって使う積分が分かれます．
演習問題¶
定数確率変数の期待値を計算してください．