Regret bound for online gradient descent

Stream: maths

[Geoffrey Irving]

https://github.com/girving/debate/blob/main/Learn/OGD.lean formalises the regret bound for online gradient descent. That is, gradient descent against online, adversarial convex losses has regret at most

$$\frac{3}{2}GD\sqrt{T}$$

where G, D, T bound subgradient norms, convex set diameter, and timesteps, respectively.