{"id":"palomar/PALOMAR-2026-08-31-000007","url":"https://github.com/MaxWellApexLab/BicausalOT-palomar/tree/06488da9a8379c66bc8d9065e6279d4d36f29d99","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000007-v1.json","repo":"https://github.com/MaxWellApexLab/BicausalOT-palomar","tags":["math.LO","math.PR","math.GN","math.OC","msc:28B20","msc:54C65","msc:54H05","msc:03E15","msc:28A20","msc:68V20"],"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 Kuratowski–Ryll-Nardzewski measurable selection theorem: for an arbitrary measurable space (alpha, A) and a Polish space Y, a multifunction Phi : alpha -> Set Y with nonempty closed values that is weakly measurable (the hit set {a | Phi a meets U} lies in A for every open U) admits an A-to-Borel measurable selection f with f a in Phi a for every a. The statement is measure-free…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"A general theorem on selectors","identifier":"Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 13 (1965), 397–403","relationship":"formalizes"},{"title":"Classical Descriptive Set Theory","identifier":"ISBN 978-0-387-94374-9 (Graduate Texts in Mathematics 156, Springer, 1995)","relationship":"adapts"},{"title":"A Course on Borel Sets","identifier":"ISBN 978-0-387-98412-4 (Graduate Texts in Mathematics 180, Springer, 1998)","relationship":"adapts"}]}