{"id":"palomar/PALOMAR-2026-08-31-000009","url":"https://github.com/MaxWellApexLab/BicausalOT-palomar/tree/66fbfd2fcf10f570d43946aafbd8731ef0dc127f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000009-v1.json","repo":"https://github.com/MaxWellApexLab/BicausalOT-palomar","tags":["math.LO","math.CA","math.PR","math.GN","math.OC","msc:28A12","msc:28A05","msc:03E15","msc:54H05","msc:31C15"],"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 results registered by this Comparator configuration are Choquet capacitability for analytic sets in its finite-measure form, and its immediate corollary, the universal measurability of analytic sets. Concretely: for a Polish space X carrying its Borel sigma-algebra, a finite Borel measure mu on X, and an analytic (not necessarily Borel) set A contained in X, the outer measure of A is the supremum of mu K over the compact subsets K of…","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"}]}