A Formalization of the Lévy-Prokhorov Metric inIsabelle/HOL
Michikazu Hirata
Tokyo Institute of Technology

ITP2024,
September 12, 2024

Lévy-Prokhorov Metric
The Lévy-Prokhorov Metric= A metric between finite measures on a metric space.
A measure µ on X
µ : ⌃X ! [0, 1]
X : set,⌃ X ✓ 2X :-algebra on X.

Intuitively, µ(A) = the size of A
(finite measure () µ(X) < 1)
Ex.
The Lebesgue measure ⌫ on Rn⌫ ((ai , bi ]n ) = (bi ai )ninfinite measure (⌫(Rn ) = 1)

A probability measureP (E) = probability E happens
finite measure (P (sample space) = 1)

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

2 / 25

Motivation
Let P(M ) = {all finite measures on M }.
6= power set
X is a Polish space =) So is P(X)
M is a standard Borel space =) So is P(M )A

Polish space
topologicalis aspace with certain good properties.
standard Borel spacemeasurable

R
Topology on P(X)( µ. f dµ) continuous 8f 2 Cb (X).
is the least one making-algebra on P(M )( µ. µ(A)) measurable 8A 2 ⌃M .
(Cb (X) = {f : X ! R, f is bounded countinuous})

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

3 / 25

Why Polish and Standard Borel Spaces?
X : topological space, M : measurable spacedef

X is a Polish space () X is separable and completely metrizabledef

M is a standard Borel space () 9S : Polish space s.t. S generates M
Ex. R, N, and their countable products are Polish (thus standard Borel spaces).
PropertiesA Polish space is embedded into a compact space.
A standard Borel space M is either
countable discrete space orM⇠
= R.

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

4 / 25

Large deviation theory

Transportation theory

Disintegration theorem

Quasi-Borel spaces

Jean-Dominique Deuschel and Daniel W. Stroock, Large Deviations, 1989.

Cédric Villani, Optimal Transport: Old and New., 2008.

Baccelli et al, Random Measures, Point Processes, and Stochastic Geometry, 2020

[Heunen+, LICS2017]
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

5 / 25Lévy-Prokhorov Metric
X is Polish space =) So is P(X)
M is a standard Borel space =) So is P(M )Need to give a metric on P(X).
“Metrics” on measures (or distributions)Lévy-Prokhorov metric
Wasserstein metric
Relative entropyetc.
The Lévy-Prokhorov metricalways being a metric in the mathematical sense
Detailed lecture notes by Gaans (2002/2003)
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

6 / 25

Contribution : Polishness of P(X)
X is Polish space =) So is P(X)def

X is a Polish space () X is separable and completely metrizable
Step 1. Separability of P(X)

Step 2. Completeness of (P(X), dP(X) ) Tough!!
– Prokhorov’s theorem– Riesz representation theorem (2.1K lines of proofs)– Alaoglu’s theorem

Step 3. (P(X), dP(X) ) metrizes P(X)
M is a standard Borel space =) So is P(M )def

M is a standard Borel space () 9S : Polish space s.t. S generates M
Show (P(M ), dP(M ) ) generates P(M )We construct the proof
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

7 / 25

Contribution : Prokhorov’s Theorem
Prokhorov’s Theorem
X : a Polish space✓ P(X) \ {µ. µ(X)  r} for some r < 1.
is compact in P(X) ()is tight: i.e.,8" > 0. 9K : compact in X , s.t.8µ 2 . µ(XK)  "Used for
Completeness of the Lévy-Prokhorov metricCentral limit theorem
Sanov’s theorem in large deviation theory
Existence of optimal coupling in transportation theory
depending on
Riesz representation theorem
Alaoglu’s theorem
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

8 / 25

Results
Formalization in Isabelle/HOL ofLévy-Prokhorov metricweak convergence
Portmanteau theorem
separability and completeness

Prokhorov’s theorem
a special case of Alaoglu’s theorem
Riesz representation theorem

P(M ) is a Polish and standard Borel spaceequivalence of measurable spaces of finite measures

Archive of formal proofs
The Lévy-Prokhorov Metric, June 2024 (6.6K lines)
The Riesz representation theorem, June 2024 (4.4K lines)

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

9 / 25

Results
Formalization in Isabelle/HOL ofLévy-Prokhorov metricweak convergence
Portmanteau theorem
separability and completeness

Prokhorov’s theorem
a special case of Alaoglu’s theoremRiesz representation theorem

P(M ) is a Polish and standard Borel spaceequivalence of measurable spaces of finite measures

Archive of formal proofs
The Lévy-Prokhorov Metric, June 2024 (6.6K lines)
The Riesz representation theorem, June 2024 (4.4K lines)

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

9 / 25Lévy-Prokhorov Metric
Let X be a metric space.
The Lévy-Prokhorov metric dP(X) on P(X)dP(X) (µ, ⌫) = inf{" > 0 | 8A 2 ⌃X . µ(A)  ⌫(A" ) + "^ ⌫(A)  µ(A" ) + "}.

A"A

A" =S

x2A ballX (x, ")Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

10 / 25

Lévy-Prokhorov Metric
Weak Convergence
For {µn }n2N ✓ P(X) and µ 2 P(X),defµn )wc µ () 8f : X ! R bounded continuous,ZZf dµn ! f dµ

The Lévy-Prokhorov metric metrizes weak convergence.

Theorem
1. µn ! µ in (P(X), dP(X) ) implies µn )wc µ

2. If X is separable, then µn ! µ in (P(X), dP(X) ) i↵ µn )wc µ

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

11 / 25

Lévy-Prokhorov Metric in Isabelle/HOL
Metric spaces in Isabelle/HOL
Type-based (class) by [Hölzl+, ITP2013]
work better in automation
carrier sets must be UNIV (all elements of the type)
Ex. Metric on
R, N[0, 1], Cb (X) (bounded continuous functions)Set-based (locale, typedef) by Paulson⇤ since Isabelle2023
Any carrier sets

We use the set-based library because
P(X) = {µ. µ is a finite measures on X} =6 U N IV .

⇤Lawrence C. Paulson, Porting the HOL Light metric space library,https://lawrencecpaulson.github.io/2023/07/12/Metric_spaces.html
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

12 / 25

Set-Based Metric Spaces in Isabelle/HOL
HOL/Analysis/Abstract Metric Spaces.thylocale Metric-space =00fixes M :: 0a set andV d :: a ) a ) realassumes nonneg: xVy. 0  d x yassumes commute:x y. d x y = d y xVassumes zero: x Vy. [[x 2 M; y 2 M]] =) d x y = 0 ! x=y
assumes triangle: x y z. [[x 2 M; y 2 M; z 2 M]] =) d x z  d x y + d y z(M,d) forms a metric space.

Non-negativity and commutativity must hold on the whole type.

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

13 / 25Set-Based Metric Spaces in Isabelle/HOL
HOL/Analysis/Abstract Metric Spaces.thylocale Metric-space =00fixes M :: 0a set andV d :: a ) a ) realassumes nonneg: xVy. 0  d x yassumes commute:x y. d x y = d y x
Vassumes zero: x Vy. [[x 2 M; y 2 M]] =) d x y = 0 ! x=y
assumes triangle: x y z. [[x 2 M; y 2 M; z 2 M]] =) d x z  d x y + d y z(M,d) forms a metric space.

Non-negativity and commutativity must hold on the whole type.

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

13 / 25

Lévy-Prokhorov Metric in Isabelle/HOL
locale Levy-Prokhorov = Metric-space
begin
N is a measure on (M, d)definition P ⌘ {N. sets N = sets (borel-of mtopology) ^ finite-measure N}
definition LPm :: 0a measure ) 0a measure ) real where
LPm N L ⌘if N d2 P ^ L 2 P then( {e. e > 0 ^ (8 A2sets (borel-of mtopology).Smeasure N A  measure L (S a2A. mball a e) + e ^measure L A  measure N ( a2A. mball a e) + e)})Vdelse 0for x y. 0  d x y (because ; = ?)sublocale LPm: Metric-space P LPm
hproofiendc.f.
dP(X) (µ, ⌫) = inf{" > 0 | 8A 2 ⌃X . µ(A)  ⌫(A" ) + " ^ ⌫(A)  µ(A" ) + "},S
where A" = a2A ballX (a, ").

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

14 / 25

Convergence w.r.t. FiltersLimit is defined using filters in Isabelle/HOL.

Fseq : a filter on N,xnn!1f (x)x!a! x () (xn ! x) Fseq in R! L () (f ! L) (at a) in R

(at a) : a filter on R

A filter F on I : F ✓ 2I satisfying certain conditions.
In Isabelle/HOL, limit istendsto (type-based topological spaces)
limitin (set-based topological spaces)

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

15 / 25

Weak Convergence with Filters
Weak Convergence
For {µn }n2N ✓ P(X), µ 2 P(X),µn )wc µdef() 8f : X ! R bounded continuous,ZZf dµn ! f dµThe Lévy-Prokhorov metric metrizes weak convergence.

Theorem
1.

µn ! µin (P(X), dP(X) ) implies µn )wc µ

2. If X is separable, thenµn ! µin (P(X), dP(X) ) i↵ µn )wc µ

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

16 / 25

Weak Convergence with Filters
Weak Convergence
For {µi }i2I ✓ P(X), µ 2 P(X), and a filter F on I,def(µi )wc µ) F () 8f : X ! R bounded continuous,✓Z◆
Zf dµi ! f dµ F in RThe Lévy-Prokhorov metric metrizes weak convergence.

Theorem
1. (µi ! µ) F in (P(X), dP(X) ) implies (µi )wc µ) F
2. If X is separable, then(µi ! µ) F in (P(X), dP(X) ) i↵ (µi )wc µ) F

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

16 / 25

Topology of Weak Convergence
Topology of Weak Convergence
The topology of weak convergence OWC(X) on RP(X)OWC(X) = the coarsest topology making ( µ. f dµ) continuous 8f 2 Cb (X).

Lemma(µi ! µ) F in (P(X), OWC(X) ) i↵ (µi )wc µ) F.

Proposition
If X is a separable metric space, then(P(X), OWC(X) ) = (P(X), OdP(X) )This proposition is a well-known result, but few books contain its proof.
Our new proof uses limit w.r.t. filters.
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

17 / 25

Metrizability of Topology of Weak Convergence
Proposition
If X is a separable metric space, then(P(X), OWC(X) ) = (P(X), OdP(X) )ClaimO, O0 : topologies on X
O = O0 () (8F. convergence in O w.r.t. F = convergence in O0 w.r.t. F)(=)) trivial, ((=) this work
Proof of Proposition: For any filter F,
convergence in OWC(X) w.r.t. F = weak convergence w.r.t. F= convergence in (P(X), dP(X) ) w.r.t. F

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

18 / 25

Metrizability of Topology of Weak Convergence
Proposition
If X is a separable metric space, then(P(X), OWC(X) ) = (P(X), OdP(X) )The textbook by Billingsley (1968)
By examining neighborhoods
The textbook by Deuschel and Stroock (1989)
By showing
convergence in OWC(X) w.r.t. Fseq = convergence in (P(X), dP(X) ) w.r.t. Fseq

(sequences are on N)

Need to show the first-countability of (P(X), OWC(X) )Our proof

By using equivalence of limit w.r.t. filters

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

19 / 25

Related Works
In Isabelle/HOL by Avigad et al. (2017)
weak convergence for probability measures on R
finite measures
any topological spacesa special case of Prokhorov’s theorem
the general form
applied them to prove the central limit theorem
In Lean by Kytölä (ongoing, 2023–)
weak convergence on finite measures using filterssame as ours
X is a pseudometric space =) The Lévy-Prokhorov metric is a pseudometric
X is a metric space =) The Lévy-Prokhorov metric is a metric“finer” than our work
metric = pseudometric + (d(x, y) = 0 () x = y)
The Lévy-Prokhorov metric on probability measures metrizes the topology ofweak convergence
finite measures+ more results (e.g. Prokhorov’s theorem)
Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

21 / 25E↵orts
Limit using filters=) Similar to the sequential cases
Sequential (8n N1 . xn < "/2) ^ (8n N2 . yn < "/2)=) 8n max{N1 , N2 }. xn + yn < "Filter eventually xi < "/2 w.r.t. F ^ eventually yi < "/2 w.r.t. F=) eventually xi + yi < " w.r.t. F
Riesz representation theorem
9 pages in the book by Rudin “Real and Complex Analysis” (1987)
2.1K– lines in Isabelle/HOL

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

22 / 25

Conclusion
We formalizedLévy-Prokhorov metric
Prokhorov’s theorem
P(M ) is a Polish and standard Borel spacein Isabelle/HOL
Future Works

Large deviation theory
Transportation theory
Point process

Michikazu Hirata (Tokyo Institute of Technology) A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL ITP2024, September 12, 2024

23 / 25