Isabelle/HOL による Levy-Prokhorov 距離の形式化
平田 路和
東京工業大学

1. 概要

4. Levy-Prokhorov 距離

Levy-Prokhorov 距離: 距離空間上の有限測度間の距離
弱収束の “距離づけ”(X, d) を距離空間，P = {X 上の有限測度 }，µ, ν ∈ PdP (µ, ν) = inf{α > 0. ∀A ∈ ΣX . µ(A) ≤ ν(Aα) + α ∧ν(A) ≤ µ(Aα) + α}∪
ただし，Aα = x∈A ball(x, α)．(P, dP ) は距離空間となる．
Aα
A

本研究の形式化▶ 測度の弱収束 (フィルターで一般化された Portmanteau 定理)▶ 測度の弱収束位相空間▶ Levy-Prokhorov 距離とその性質▶ Prokhorov の定理と必要な補題: Riesz の表現定理，Alaoglu の定理▶ Prokhorov の定理: 測度列に対する収束部分列の存在性の証明に用いられる
中心極限定理，最適カップリングの存在定理 (最適輸送理論)，Sanov の定理等
▶ Riesz の表現定理: 正線型汎函数を積分表示
本の証明 [Rudin, 1987]: 9 ページ，Isabelle: 約 2,100 行▶ 標準ボレル空間上の有限測度がなす可測空間が標準ボレル空間▶ よい性質を持つ可測空間のクラス
準ボレル空間理論，Disintegration 定理などで用いられる

2. 準備
Isabelle/HOL での距離空間▶ 型クラス版 [Hölzl et.al.,ITP2013]: 型全体上の距離▶ 集合版 [Paulson,2023]: 集合+距離関数
本研究は集合版を利用
Isabelle/HOL での収束フィルターによる一般化(□ −→ □) □ in □ :: (α ⇒ β) ⇒ β ⇒ α f ilter ⇒ β topology ⇒ boollim xn = x ⇐⇒ (xn −→ x) sequentially in Rn→∞lim f (x) = L ⇐⇒ (f −→ L) (at a) in Rx→a(位相空間が明らかな場合は in 以降を省略)

3. 測度の弱収束フィルターで一般化．証明は F = sequentially の時と同じ流れ測度の弱収束)(∫∫def(µi ⇒wc µ) F ⇐⇒ ∀f ∈ Cb(X). f dµi −→ f dµ F
弱収束の同値な条件 (Portmanteau の定理) を形式化した．
測度の弱収束位相∫: Owc∀f ∈ Cb(X).(λµ. f dµ) : P → R が連続になるような最弱の位相定理: (µi −→ µ) F in (P, Owc) ⇐⇒ (µi ⇒wc µ) F定理: (µi −→ µ) F in (P, OdP ) =⇒ (µi ⇒wc µ) F定理: X が可分の時，(µi ⇒wc µ) F =⇒ (µi −→ µ) F in (P, OdP )系: X が可分の時，(P, OdP ) = (P, Owc)収束の同値性をフィルターで一般化したので，開 (閉) 集合の収束による特徴づけを使うことができる．
定理: X が可分なら (P, OdP ) も可分
定理: X が可分完備なら (P, OdP ) も可分完備 (要 Prokhorov の定理)

5. Prokhorov の定理
defΓ(⊆ P) が緊密 ⇐⇒ ∀ε > 0. ∃K : compact. ∀µ ∈ Γ. µ(X − K) < εr ≥ 0, Pr = P ∩ {µ. µ(X) ≤ r}, Γ ⊆ Pr とする
Prokhorov の定理: X が可分完備の時以下は同値
1. Γ が相対コンパクト
2. Γ が緊密「2 ならば 1」は以下の形で使える．(完備性必要なし){µn}n∈N(⊆ Pr ) が緊密 ⇒∃µnk : 部分列, ∃µ. (µnk ⇒wc µ) sequentially(1)必要な補題: Riesz の表現定理
X: コンパクトハウスドルフ，正線型汎函数: φ : C(X) → X
i.e. φ(αf + βg) = αφ(f ) + βφ(g) ∧ (f ≥ 0 =⇒ φ(f ) ≥ 0)とすると一意な測度 ν があって以下が成立．
∫∀f ∈ C(X). φ(f ) =f dν

必要な補題: Alaoglu の定理
Y : 内積ベクトル空間，Y ∗: 双対空間
B ∗ = {φ ∈ Y ∗, ∥φ∥ ≤ r} は弱*-コンパクト
欲しい形の証明には集合版ベクトル空間が必要
Isabelle/HOL の集合版ベクトル空間ライブラリは小さい
Y = C(X) の場合のみ証明

6. 標準ボレル空間
P 上の σ-代数:ΣP∀A ∈ ΣX . (λµ. µ(A)) : P → R が可測になるような最弱の σ-代数
Psprob = P ∩ { 劣確率測度 }, Pprob = P ∩ { 確率測度 }Psprob や Pprob は (劣) マルコフ核の定義でも使われる
定理: X が可分完備なら ΣP = σ[Owc]Levy-Prokhorov 距離を用いた証明を与えた
系: X が標準ボレル空間なら P, Psprob, Pprob も標準ボレル空間
標準ボレル空間: 可分で完備な距離づけ可能位相空間に生成されるボレル空間

7. 関連研究・参考文献▶ Isabelle/HOL
R 上確率測度列についての弱収束
R 上の確率測度について Prokhorov の定理 (1) の形▶ Lean弱収束，弱収束位相, Riesz の表現定理
Levy-Prokhorov 距離は現在形式化されている最中▶ PVS, Mizar
Riesz の表現定理 (の原型バージョン)

1. W.Rudin, Real and Complex Analysis, McGraw Hill; 3rd edition, 1987.
2. J.Hölzl, F.Immler, B. Huﬀman, Type Classes and Filters for Mathematical Analysis in Isabelle/HOL,
ITP2013, Springer Berlin Heidelberg.
3. L.C.Paulson, Porting the HOL Light metric space library,https://lawrencecpaulson.github.io/2023/07/12/Metric spaces.html, 2023, Accessed:
December 31. 2023.
4. O.Gaans, Probability Measures on Metric Space,https://www.math.leidenuniv.nl/~vangaans/jancol1.pdf, Accessed: March 2. 2023.
5. C.E.Heil, Alaoglu’s Theorem,
https://heil.math.gatech.edu/6338/summer08/section9f.pdf, Lecture note on MATH 6338
(Real Analysis II) at Gerogia Insisute of Technology, 2008, Accessed: January 5, 2024
謝辞: 本研究は JSPS 科研費 23KJ0905 の助成を受けたものです．