「与えられた２つの確率分布を(計算量的に)識別出来ない」という概念を数学的に定義します。
安永先生著：
をお持ちの方はp40, 第４章「擬似ランダム」の冒頭部分を参考にしてください。以下の定義は同書からの引用です。
定義4.1 確率分布X, Yが(t,ε)-識別不可能であるとは、計算量t以下の任意のアルゴリズムAに対して、
| Pr[(A(X)=1] - Pr[A(Y)=1] | ≦ ε
を満たすことである。
念のためのですが、Pr[A(X)=1]はPr[x←X, y←A(x) : y=1]の省略記法です。つまりXから1つxを選びそれを関数（この場合はアルゴリズム) Aに食わせた結果が1になる確率のことです。もしA(X)=1の確率とA(Y)=1の確率がεより大きくできるようなAがあればそのAは確率分布XとYを識別出来たということです。
ちなみにLean4でかくとこんな感じです。上記のアルゴリズムAを識別者Dと書いている点に注意してください。
/-- A helper definition to represent the probability that a distinguisher D
outputs 1 given an input from distribution X. -/
noncomputable def PrDX_one (X : PMF α) (D : α → PMF Bit) : ℝ :=
(Pr (do let a ← (X >>= D); PMF.pure (a == 1))).toReal/-- Definition 4.1: (t, ε)-Computational Indistinguishability of distributions.
Probability distributions X and Y over α are (t, ε)-indistinguishable if
for every algorithm A with complexity tA ≤ t,
|Pr[x ← X; A x = 1] - Pr[y ← Y; A y = 1]| ≤ ε. -/
def DistIndistinguishable
(X Y : PMF α) (t : ℕ) (ε : NNReal) : Prop :=
∀ (D : α → PMF Bit) (tD : ℕ),
tD ≤ t → |PrDX_one X D - PrDX_one Y D| ≤ (ε : ℝ)
Lean4のコードでも略記法が使われていますね。PrDX_oneの定義でa ← (X >>= D)と書かれていますが、これはa' ← X, a ← D a'の略記法です。
これで２つの確率分布が与えられた時にそれらをアルゴリズムで識別出来る、識別出来ない、という議論ができるようになりました。
「確率分布の計算量的識別不可能」については２つの便利な性質があります。閉包性と推移性です。
命題4.1 閉包性：任意の確率分布X,Yが(t+tA, ε)-識別不可能ならば、計算量tA以下のアルゴリズムAに対してA(X)とA(Y)は(t, ε)-識別不可能である。
theorem closure
(X Y : PMF α)
(A : α → PMF β)
(t tA : ℕ) (ε : NNReal)
(hind : DistIndistinguishable X Y (t + tA) ε) :
DistIndistinguishable (X >>= A) (Y >>= A) t ε := by命題4.3 推移性：確率分布$X_0,\dots,X_l$が$i = 0,\dots,l-1$に対して、$X_i$と$X_{i+1}$が(t, e/l)-識別不可能ならば$X_0$と$X_l$は(t, e)-識別不可能である。
/-- The transitivity property of distinguishability. -/
theorem transitivity
(X : ℕ → PMF α) (l : ℕ) (t : ℕ) (ε : NNReal)
(hl : l > 0)
(h_adjacent : ∀ i < l, DistIndistinguishable (X i) (X (i + 1)) t (ε / l)) :
DistIndistinguishable (X 0) (X l) t ε := by
この２つの命題は確率分布に関する証明をする際の道具になります。
今回の定義や命題のLean4による形式化および命題の形式証明は以下のレポジトリにあります。
DistInd.leanというファイルをご覧ください。
