The Lévy-Prokhorov Metric

Michikazu Hirata 📧

June 4, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Levy_Prokhorov_Metric