{"id":"palomar/PALOMAR-2026-09-20-000001","url":"https://github.com/Arthur742Ramos/blackwell-approachability-lean/tree/42b9d7c77e77fc158d44cb31ef320798c3c73492/rate-preserving-reduction","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-20-000001-v1.json","repo":"https://github.com/Arthur742Ramos/blackwell-approachability-lean","tags":["cs.GT","cs.LG","msc:91A26","msc:68T05","game-theory","online-learning","lean","regret"],"score":0,"title":"Finite tight Blackwell approachability-to-improper phi-regret reduction in Lean","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos","Ruy Jose Guerra Barretto de Queiroz","David Barros Hulak"],"reviews":0,"subject":"cs.GT","summary":"A Mathlib-only nonempty finite-simplex, algorithmic specialization of Theorem 4 in Dann, Mansour, Mohri, Schneider, and Sivan (COLT 2025). It realizes the tensor action space as a joint simplex, defines the source improper comparator by adding a mixed-constraint tensor of the canonical action marginal, proves that comparator escapes the action set, and proves exact finite-horizon equality between approachability loss and improper phi-regret under explicit causal strategy translations in both directions. It also proves that every joint action is a mixture of at most one rank-one tensor per…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-20","reactions":{},"formalized":true,"formalizes":[{"title":"Rate-Preserving Reductions for Blackwell Approachability","identifier":"https://proceedings.mlr.press/v291/dann25a.html","relationship":"formalizes"}]}