{"id":"palomar/PALOMAR-2026-08-31-000011","url":"https://github.com/MaxWellApexLab/BicausalOT-palomar/tree/3fe500ff64a75d7ab71b474d0c656d5471f62992","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000011-v1.json","repo":"https://github.com/MaxWellApexLab/BicausalOT-palomar","tags":["math.LO","math.GN","math.PR","math.OC","msc:03E15","msc:54H05","msc:28A05","msc:28B20","msc:54C65","descriptive-set-theory"],"score":0,"title":"MaxWellApexLab/BicausalOT-palomar","trust":"high","domain":"math.LO","source":"palomar","authors":["KT. Wu"],"reviews":0,"subject":"math.LO","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 Jankov-von Neumann uniformization theorem: for Polish spaces X and Y and a nonempty analytic (Sigma-1-1) set P in X x Y, there is a function phi : X -> Y that uniformizes P on its projection, (x, phi x) in P for every x in proj_X(P), and that is sigma(Sigma-1-1)-measurable, meaning that phi-preimages of Borel subsets of Y lie in the sigma-algebra generated by the analytic…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"Classical Descriptive Set Theory","identifier":"ISBN 978-0-387-94374-9 (Graduate Texts in Mathematics 156, Springer, 1995)","relationship":"adapts"},{"title":"Stochastic Optimal Control: The Discrete Time Case","identifier":"ISBN 978-1-886529-03-3 (Athena Scientific, 1996; originally Academic Press, 1978)","relationship":"adapts"}]}