Adversarial bandit convex optimisation with regret d^(3/2) sqrt(n) up to logarithms

This is AI-generated research: the results, proofs and code were found and written by AI. Credit goes to all the humans whose work it builds on. In adversarial bandit convex optimisation a learner plays $n$ rounds in a convex body of $\mathbb R^d$ against convex losses in $[0,1]$, seeing only its loss. Bubeck, Eldan and Lee conjectured that some learner whose rounds take time polynomial in $d$ and $\ln n$ on polytopes with polynomially many rational constraints has regret $d^{3/2}\sqrt n$ up to logarithms, and that none does better. In their game, against an adaptive adversary, we prove the first on their polytopes, timed on a real RAM with square root, exponential, logarithm, Gaussian draws and spectral functions: a learner has upper expected regret at most a constant times $d^{3/2}\sqrt n\,\ln^5(2dn)$. We prove the second on the unit ball: for $d\ge4\cdot10^6$, $n\ge d^{10}$ every learner has expected regret at least $7\cdot10^{-9}d^{3/2}\sqrt n/\ln d$ against some adversary. For fixed losses on bodies of diameter $D$ containing a unit ball, an explicit learner has expected regret $O(d^{3/2}\sqrt n\,\ln^{3/2}(nD))$. The conjecture is Conjecture 1 of Bubeck, Eldan and Lee, Kernel-based methods for bandit convex optimization, J. ACM 68 (2021); arXiv:1607.03084. Theorems 1.1, 1.3, 1.4 and 1.5, Remark 1.2, Corollaries 8.6 and 1.6, Proposition 2.2, Theorem 3.1 and Lemma 7.13 are proved in Lean 4 with Mathlib, from statements written out from the definitions of the paper, with only the standard axioms; Comparator checks the statements, and nanoda, a second implementation of the Lean kernel, checks the proofs again. Every other numbered statement of the paper is a step of these proofs, stated as the formal proof proves it. Code, Lean proofs and the TeX source: github.com/mt0-svg/adversarial-bco