2026-08-17T23:46:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20749 2024-09-02T10:03:24Z ddc:004 open_access

A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL Hirata, Michikazu formalization of mathematics measure theory metric spaces topology Lévy-Prokhorov metric Prokhorov’s theorem Isabelle/HOL The Lévy-Prokhorov metric is a metric between finite measures on a metric space. The metric was introduced to analyze weak convergence of measures. We formalize the Lévy-Prokhorov metric and prove Prokhorov’s theorem in Isabelle/HOL. Prokhorov’s theorem provides a condition for the relative compactness of sets of finite measures and plays essential roles in proofs of the central limit theorem, Sanov’s theorem in large deviation theory, and the existence of optimal coupling in transportation theory. Our formalization includes important results in mathematics such as the Riesz representation theorem, which is a theorem in functional analysis and used to prove Prokhorov’s theorem. We also apply the Lévy-Prokhorov metric to show that the measurable space of finite measures on a standard Borel space is again a standard Borel space. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michikazu Hirata 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.21 urn:nbn:de:0030-drops-207492 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.21 eng https://creativecommons.org/licenses/by/4.0/legalcode