# 有限ドメインの確率論のCoq実装を読む
## 一般的な確率空間の話
**標本空間**と呼ばれる集合 $Ω$，**事象** (*event*) のなす集合族 $\mathcal{B} ⊆ 2^Ω$，**確率測度** $P : \mathcal{B} → [0, 1]$ からなる $(Ω, \mathcal{B}, P)$ で
- $P(Ω) = 1$
- 可算加法性： $∀(A : \mathbf{N} → 2^Ω). (∀i∀j ∈ \mathbf{N}. i ≠ j ⇒ A_i ∩ A_j = ∅) ⇒ P(⋃_{i ∈ \mathbf{N}} A_i) = ∑_{i = 1}^{∞} P(A_i)$
を満たすものを**確率空間**と呼ぶ．
$Ω$ が有限の場合は簡単．例えばサイコロの場合は $Ω := \{1, 2, 3, 4, 5, 6\}$，$\mathcal{B} := 2^Ω$，$P(A) := |A|/6$ で，「出た目が偶数である」ことに対応する事象が $A_{\mathrm{even}} := \{2, 4, 6\}$ で，$P(A_{\mathrm{even}}) = 1/2$．
写像 $X : Ω → \mathbf{R} ∪ \{+∞, -∞\}$ が $∀r ∈ \mathbf{R}. \{ω ∈ Ω | X(ω) > r\} ∈ \mathcal{B}$ を満たすとき，$X$ を**確率変数** (*random variable*) と呼ぶ．$Ω$ が有限の場合は簡単で，例えばサイコロの目の大きさなら単に $X(n) := n$ でよい．
確率変数 $X$ に対して，$\mathrm{E}[X]$ で $X$ の**期待値**を表す．$Ω$ が有限の場合は簡単に定義でき，$\mathrm{E}[X] := ∑_{ω ∈ Ω} P(\{ω\}) \cdot X(ω)$ という具合．例えばサイコロの場合，目の大きさの期待値は $\mathrm{E}[X] = (1 + 2 + 3 + 4 + 5 + 6)/6 = 7/2$．
また，$\mathrm{V}[X]$ で $X$ の**分散** (*variance*) を表す．これも有限の場合は定義が簡単で，$\mathrm{V}[X] := ∑_{ω ∈ Ω} (X(ω) - \mathrm{E}[X])^2$．
確率は，記法として $P[X = a] := P(\{ω ∈ Ω | X(ω) = a\})$ などと拡張される．
## 記法
- ``E `* F``： 直積 $E × F$
- ``E `*T``： $E × T$（T は何かしらの台集合らしい？）
- ``T`* F``： $T × F$
- `Pr d E`： 分布 `d` に於ける事象 `E` の確率
* 分布というものの実体はまだよくわからない．
- `{RV P -> T}`： `T : eqType` 型の値をとる，**ambient distribution** `P` 上を動く確率変数の型
* ambient distributionという用語はよくわからない．何らかの私訳？
- `` `p_X``： `X : {RV P -> R}` なる `P`
- `` `Pr[ X = a ]``： 確率変数 `X` が `a` をとる確率（一般的な記法と同じ）
- `` `Pr_P [ A | B ]``： 事象に対する条件つき確率
- `Z \= X @+ Y`： 「確率変数 `Z` は `X` と `Y` の和である」という命題
- `X \=sum Xs`： 「確率変数 `X` は独立な確率変数列 `Xs` の和である」という命題
- `` `E X``： 確率変数 `X` の期待値（一般的な記法 $\mathrm{E}[X]$ と同じ）
- `` `E_[ X | F ]``： 事象 `F` を前提とする確率変数 `X` の条件つき期待値
- `` `V X``： 確率変数 `X` の分散（一般的な記法 $\mathrm{V}[X]$ と同じ）
- `X _|_ Y | Z`： `Z` の下で `X` と `Y` は条件つき独立（一般的な記法に近い）．P(X, Y | Z) = P(X | Z) P(Y | Z)
- `P |= X _|_ Y`： 確率変数 `X` と `Y` は独立である
## 定理
### 期待値の線型性
```coq
Lemma E_sum_2 : X \= X1 @+ X2 -> `E X = `E X1 + `E X2.
```
和の期待値は期待値の和に等しい．
### 独立な確率変数の分散の線型性
```coq
Lemma V_sum_2 : X \= X1 @+ X2 -> P |= X1' _|_ X2' -> `V X = `V X1 + `V X2.
```
### 分散の平均
```coq
Lemma Var_average n (X : {RV (P `^ n) -> R}) Xs (sum_Xs : X \=sum Xs) :
forall sigma2, (forall i, `V (Xs ``_ i) = sigma2) ->
n%:R * `V (X `/ n) = sigma2.
```
- ``P `^ n`` は何か？ 分布 `P` の確率変数が `n` 個独立に動いたときの分布？
- ``` ``_``` は何か？ 列に対する添字アクセス？
- `e %: T` は型強制っぽい？
$∀σ_2. (∀i. V[\boldsymbol{X}_i] = σ_2) ⇒ n \cdot V[X / n] = σ_2$
分散が全て $σ_2$ であるような確率変数の列に対し，その相加平均の分散を取った確率変数は分散が $σ / n$．要するに “平均を取ると散らばり具合が低減する”．
### 事象集合に対する確率に関する不等式
```coq
Lemma Pr_bigcup (B : finType) (p : pred B) F :
Pr (\bigcup_(i | p i) F i) <= \sum_(i | p i) Pr (F i).
```
$P(⋃_{i ∈ \{n | p(n)\}} F_i) \leq ∑_{i ∈ \{n | p(n)\}} P(F_i)$
わりと自明．
### 「Booleの等式」
```coq
Lemma Boole_eq (I : finType) (F : I -> {set A}) :
(forall i j, i != j -> [disjoint F i & F j]) ->
Pr (\bigcup_(i in I) F i) = \sum_(i in I) Pr (F i).
```
$(∀i∀j. i ≠ j ⇒ F_i ∩ F_j = ∅) ⇒ P(⋃_{i ∈ I} F_i) = ∑_{i ∈ I} P(F_i)$
これもわりと自明．要するにどの2者も排反な事象の集合の確率はそれぞれの確率の和になる．
### 事象集合の分割に関する等式
```coq
Lemma total_prob (I : finType) (E : {set A}) (F : I -> {set A}) :
(forall i j, i != j -> [disjoint F i & F j]) ->
cover (F @: I) = [set: A] ->
Pr E = \sum_(i in I) Pr (E :&: F i).
```
- `{set A}` や `[set: A]` は何か？
* mathcompの記法らしい？： https://math-comp.github.io/htmldoc/mathcomp.ssreflect.finset.html
> [set: T] or setT == the full set (the A containing all x : T).
- `{set A}` は有限型 `A` に対しその要素からなる集合全体につく型．気持ちとしては冪集合的なものらしい．要するにここでは $E ⊆ A$．
- `cover` や `@:` は何か？
* 上記ページに以下の記述あり：
> `f @: A == the image set of the collective predicate A by f.`
像 $f[A]$ らしい．
> `Definition cover P := \bigcup_(B in P) B.`
- `:&:` は何か？
> A :&: B == the intersection of A and B.
$(∀i∀j. i ≠ j ⇒ F_i ∩ F_j = ∅) ⇒ ⋃_{B ∈ F[I]} B = A ⇒ P(E) = ∑_{i ∈ I} P(E ∩ F_i)$
$⋃_{B ∈ F[I]} B$ はつまり $⋃_{i ∈ I} F_i$．前件は要するに $\{F_i\}_{i ∈ I}$ が $A$ を分割した商集合であると言っている．命題自体は，直観的にはわりと自明そう．
### 条件つき確率が満たす性質
```coq
Section bayes_extended.
Variables (I : finType) (E : {set A}) (F : I -> {set A}).
Hypothesis dis : forall i j, i != j -> [disjoint F i & F j].
Hypothesis cov : cover (F @: I) = [set: A].
Lemma total_prob_cond :
Pr d E = \sum_(i in I) `Pr_[E | F i] * Pr d (F i).
（中略）
End bayes_extended.
```
$(∀i∀j. i ≠ j ⇒ F_i ∩ F_j = ∅)$ と $⋃_{i ∈ I} F_i$ を前提し，$P_d(E) = ∑_{i ∈ I} P[E | F_i] \cdot P_d(F_i)$ を示している．
前節とよく似たことを条件つき確率として言ったもの．
### Bayesの定理
```coq
Lemma Bayes (E F : {set A}) : `Pr_[E | F] = `Pr_[F | E] * Pr d E / Pr d F.
```
一般的なBayesの定理．$P(E | F) = \frac{P(F | E) P(E)}{P(F)}$
条件つき確率は $P(E | F) := \frac{P(E ∩ F)}{P(F)}$ で定められ，“事象 $F$ が成立しているときに $E$ も成立している確率” のこと．
したがって上記補題は単に $P(E | F) P(F) = P(E ∩ F) = P(F | E) P(E)$ の両辺を $P(F) ≠ 0$ なる $P(F)$ で割ると出てくる．
### Bayesの定理の拡張
```coq
Section bayes_extended.
Variables (I : finType) (E : {set A}) (F : I -> {set A}).
Hypothesis dis : forall i j, i != j -> [disjoint F i & F j].
Hypothesis cov : cover (F @: I) = [set: A].
（中略）
Lemma Bayes_extended j :
`Pr_[F j | E] = `Pr_[E | F j] * Pr d (F j) / \sum_(i in I) `Pr_[E | F i] * Pr d (F i).
（中略）
End bayes_extended.
```
$P(F_j | E) = \frac{P(E | F_j) P(F_j)}{∑_{i ∈ I} P(E | F_i) P(F_i)}$
ここに端的な説明があった：
- https://bellcurve.jp/statistics/course/6444.html
### `Pr_bigcup_incl_excl`
```coq
Let SumPrCap (n : nat) (S : 'I_n -> {set A}) (k : nat) :=
\sum_(J in {set 'I_n} | #|J| == k) Pr P (\bigcap_(j in J) S j).
（中略）
Theorem Pr_bigcup_incl_excl n (S : 'I_n -> {set A}) :
Pr P (\bigcup_(i < n) S i) = \sum_(1 <= k < n.+1) ((-1)^(k-1) * SumPrCap S k).
```
- `'I_n` はおそらく $\{1, …, n\}$ のこと？ → $\{0, …, n - 1\}$ だった．$\mathbf{I}_n$ と書くことにしよう：
* https://math-comp.github.io/htmldoc/mathcomp.ssreflect.fintype.html
> 'I_n, ordinal n == the finite subType of integers i < n, whose
> enumeration is {0, ..., n.-1}. 'I_n coerces to nat,
> so all the integer arithmetic functions can be used
> with 'I_n.
$\mathit{SumPrCap}(S, k)$ は，族 $\{S_i\}_{i ∈ \mathbf{I}_n}$ のうち $k$ 個の共通部分をとってできる事象の確率の総和をとったもの：
$\mathit{SumPrCap}(S, k) := ∑_{J ∈ \{J ⊆ \mathbf{I}_n | \#J = k\}} P(⋂_{j ∈ J} S_j)$
定理は $P(⋃_{i ∈ \mathbf{I}_n} S_i) = ∑_{k = 1}^{n} (-1)^{k - 1} \mathit{SumPrCap}(S, k)$ という主張．少なくとも自明ではなさそう．
$n = 1$ の場合は $P(S_0) = (-1)^0 \mathit{SumPrCap}(S, 1) = P(S_0)$ なので明らか．
$n = 2$ の場合は $P(S_0 ∪ S_1) = \mathit{SumPrCap}(S, 1) - \mathit{SumPrCap}(S, 2) = (P(S_0) + P(S_1)) - P(S_0 ∩ S_1)$ でこれはたしかにそのとおり．
要するに “ヴェン図の外縁部以外の部分の大きさ” の話をしているらしい．
### `reasoning_by_cases`
```coq
Lemma reasoning_by_cases (U : finType) (P : fdist U)
(A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}) E :
`Pr[ X \in E ] = \sum_(b <- fin_img Y) `Pr[ [% X, Y] \in (E `* [set b])].
```
`fin_img` はどこで定義されているのか調べてもわからなかったが，おそらく単に写像のつくる像だろう．つまり $f$ に対して $\mathop{\mathrm{img}} f := \{f(x) | x ∈ \mathop{\mathrm{dom}} f\}$ を返す．
`[% X, Y]` については記法が以下のように定められている．要するに $ω ↦ (X(ω), Y(ω))$ で定義される確率変数のようだ．
```coq
Section pair_of_RVs.
Variables (U : finType) (P : fdist U).
Variables (A : eqType) (X : {RV P -> A}) (B : eqType) (Y : {RV P -> B}).
Definition RV2 : {RV P -> A * B} := fun x => (X x, Y x).
End pair_of_RVs.
Notation "'[%' x , y , .. , z ']'" := (RV2 .. (RV2 x y) .. z).
```
$P[X ∈ E] = ∑_{b ∈ \mathop{\mathrm{img}} Y} P[(X, Y) ∈ E × \{b\}]$
<!-- $P[X \in E] = P(\{\omega \in \Omega | X(\omega) \in E\})$
$\Omega = \{1, \ldots, 6\}, X(n) := n, E_{\mathrm{even}} = \{2, 4, 6\}$ -->
というわけでわりと直観的には自明そうだ．
### Markovの不等式
```coq
Section markov_inequality.
Variables (U : finType) (P : {fdist U}) (X : {RV P -> R}).
Hypothesis X_ge0 : forall u, 0 <= X u.
（中略）
Lemma markov (r : R) : 0 < r -> `Pr[ X >= r ] <= `E X / r.
（中略）
End markov_inequality.
```
$(∀ω ∈ Ω. X(ω) ≥ 0) ⇒ ∀r ∈ \mathbf{R_{+}}. P[X ≥ r] ≤ \mathrm{E}[X] / r$．
ここに簡潔な説明がある：
- https://manabitimes.jp/math/937
> つまりマルコフの不等式 $P(|X| ≥ a) ≤ \dfrac{E[|X|]}{a}$ は，$∣X∣$ の期待値が大きくなければ $∣X∣$ が大きくなる確率はそんなに高くないことを表しています。
* 実は学部生の頃に所属していた研究室の2年上の先輩による記事．
### Chebyshevの不等式
```coq
Section chebyshev.
Variables (U : finType) (P : fdist U) (X : {RV P -> R}).
Lemma chebyshev_inequality epsilon : 0 < epsilon ->
`Pr[ (Rabs `o (X `-cst `E X)) >= epsilon] <= `V X / epsilon ^ 2.
（中略）
End chebyshev.
```
$P[|X - \mathrm{E}[X]| ≥ ε] ≤ \mathrm{V}[X] / ε^2$．こちらも簡潔に言えば “$X$ が平均から逸脱する確率は，$X$ の分散が大きくなければそれほど大きくはならない” という具合．
### 事象の独立性
```coq
Definition inde_events (E F : {set A}) := Pr d (E :&: F) = Pr d E * Pr d F.
```
事象 $E$ と事象 $F$ が**独立**であるとは，$P(E ∩ F) = P(E) P(F)$ が成り立つことを言う．
### 事象の条件つき独立性
```coq
Definition cinde_events (E F G : {set A}) :=
`Pr_d[ E :&: F | G] = `Pr_d[E | G] * `Pr_d[F | G].
```
事象 $E$ と事象 $F$ が $G$ の下で**条件つき独立**であるとは，$P(E ∩ F | G) = P(E | G) P(F | G)$ が成り立つことを言う．
### `weak_law_of_large_numbers`
```coq
Section weak_law_of_large_numbers.
Local Open Scope vec_ext_scope.
Variables (A : finType) (P : {fdist A}) (n : nat).
Variable Xs : 'rV[{RV P -> R}]_n.+1.
Variable miu : R.
Hypothesis E_Xs : forall i, `E (Xs ``_ i) = miu.
Variable sigma2 : R.
Hypothesis V_Xs : forall i, `V (Xs ``_ i) = sigma2.
Variable X : {RV (P `^ n.+1) -> R}.
Variable X_Xs : X \=sum Xs.
Lemma wlln epsilon :
0 < epsilon ->
`Pr[ (Rabs `o ((X `/ n.+1) `-cst miu)) >= epsilon ] <= sigma2 / (n.+1%:R * epsilon ^ 2).
（中略）
End weak_law_of_large_numbers.
```
有限型 $A$，$A$ の分布 $P$，$(n + 1)$ 個の $P$ 上の確率変数の列 $\boldsymbol{X}$ が
- $∀i. \mathrm{E}[\boldsymbol{X}_i] = μ$
- $∀i. \mathrm{V}[\boldsymbol{X}_i] = σ^2$
とどの要素も相等しい平均 $μ$ と分散 $σ^2$ をもつとき，$X(ω) := ∑_{i = 1}^{n + 1} \boldsymbol{X}_i(ω)$ で確率変数 $X$ を定めると，
$0 < ε ⇒ P[|X / (n + 1) - μ| ≥ ε] ≤ σ^2 / ((n + 1) * ε^2)$
が成り立つという主張．要するにChebyshevの不等式を列に拡張したもので，“同一分布の確率変数の平均をとるとより逸脱しにくくなる” ことを言っていると見ればよさそう．
Sign in with Wallet
Connect another wallet