Abstract
We formalize the Lévy-Prokhorov metric, a metric on finite measures,
mainly following the lecture notes by Gaans.
This entry includes the following formalization.
- Characterizations of closed sets, open sets, and topology by limit.
- A special case of Alaoglu's theorem.
- Weak convergence and the Portmanteau theorem.
- The Lévy-Prokhorov metric and its completeness and separability.
- The equivalence of the topology of weak convergence and the topology generated by the Lévy-Prokhorov metric.
- Prokhorov's theorem.
- Equality of two $\sigma$-algebras on the space of finite measures. One is the Borel algebra of the Lévy-Prokhorov metric and the other is the least $\sigma$-algebra that makes $(\lambda\mu.\: \mu(A))$ measurable for all measurable sets $A$.
- The space of finite measures on a standard Borel space is also a standard Borel space.