{"id":"palomar/PALOMAR-2026-08-31-000010","url":"https://github.com/MaxWellApexLab/BicausalOT-palomar/tree/66fbfd2fcf10f570d43946aafbd8731ef0dc127f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000010-v1.json","repo":"https://github.com/MaxWellApexLab/BicausalOT-palomar","tags":["math.PR","math.GN","math.LO","msc:60B05","msc:60B10","msc:28A33","msc:54E50","msc:54E35","msc:68V20","probability"],"score":0,"title":"MaxWellApexLab/BicausalOT-palomar","trust":"high","domain":"math.PR","source":"palomar","authors":["KT. Wu"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 formalization of the Bellman value representation for bicausal optimal transport, together with the descriptive-set-theoretic library it requires. The result registered by this Comparator configuration is the Polish-space structure of the space of probability measures: if X is a Polish space carrying its Borel sigma-algebra, then the space of Borel probability measures on X, with the topology of weak convergence, is again Polish — its topology is second countable and admits a complete compatible metric. Mathlib at the pinned revision already supplies the Levy-Prokhorov metric, the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"Probability Measures on Metric Spaces","identifier":"ISBN 978-0-8218-3889-1 (AMS Chelsea Publishing 352, 2005; originally Academic Press, New York, 1967)","relationship":"adapts"}]}