独立性と同分布

独立性も，関数・集合・可測空間に対してそれぞれ定義されています． 確率変数 X : Ω → E と Y : Ω → F の独立性は IndepFun X Y P と書きます． 集合の独立性は IndepSet s t P，族の独立性は iIndepFun や iIndepSet です． 同分布は IdentDistrib X Y P Q で表します．

まずは定義を展開して使うより，定理の仮定に現れる型を読めることが重要です．

section Independence

variable {Ω E F : Type*}
variable [MeasurableSpace Ω] [MeasurableSpace E] [MeasurableSpace F]
variable {P : Measure Ω}
variable {X : Ω → E} {Y : Ω → F}

#check IndepFun
#check iIndepFun
#check IndepSet
#check iIndepSet
#check IdentDistrib

example (h : IndepFun X Y P) : IndepFun Y X P := by
  exact h.symm

end Independence

演習問題

独立性の対称性を使ってください．

example {Ω E F : Type*} [MeasurableSpace Ω] [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (h : IndepFun X Y P) : IndepFun Y X P := by
  sorry