Skip to content

Bandits: online linear optimization on normed spaces, losses in the dual #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 1 commit into from
Nov 1, 2026
Merged

Bandits: online linear optimization on normed spaces, losses in the dual #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 19 additions & 7 deletions LMLRoadmaps/Bandits/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ dependency versions used to check the interfaces (LML `53be244`, Mathlib `2e318f
| KL divergence | Mathlib `InformationTheory.klDiv`, `klDiv_compProd_eq_add`, `klDiv_map_le`; LML [`ChainRule.lean`][lml-chain] (`klDiv_compProd_right_eq_lintegral`); Tau Ceti [`Pinsker.lean`][tc-pinsker] (`two_mul_sq_measureReal_sub_le_klDiv`) and [`Variational.lean`][tc-dv] |
| Sub-Gaussian concentration and martingales | Mathlib [`SubGaussian.lean`][ml-subg] (`HasSubgaussianMGF`, `HasCondSubgaussianMGF`, `hasSubgaussianMGF_of_mem_Icc`, `measure_sum_ge_le_of_iIndepFun`, `measure_sum_ge_le_of_hasCondSubgaussianMGF`), [`OptionalStopping.lean`][ml-os] (`maximal_ineq`), `Supermartingale` |
| Laws | Mathlib `gaussianReal`, `bernoulliMeasure`, `multivariateGaussian`; Tau Ceti [`Gaussian/Cdf.lean`][tc-gauss] (`measureReal_Ioi_gaussianReal`) |
| Convex analysis | LML [`Bregman/Basic.lean`][lml-breg] (`bregDiv`, notation `D_[f](x, y, J)`, `bregDiv_three_point`), [`Subgradient/`][lml-subgrad]; Tau Ceti [`Conjugate.lean`][tc-conj] (`fenchelConjugate`), [`Strong.lean`][tc-strong] (`StrongConvexOn.add_add_le_of_hasFDerivWithinAt`); Mathlib `stdSimplex`, `StrongConvexOn` |
| Convex analysis | LML [`Bregman/Basic.lean`][lml-breg] (`bregDiv`, notation `D_[f](x, y, J)`, `bregDiv_three_point`), [`Subgradient/`][lml-subgrad]; Tau Ceti [`Conjugate.lean`][tc-conj] (`fenchelConjugate`, for a bilinear pairing), [`Strong.lean`][tc-strong] (`StrongConvexOn.add_add_le_of_hasFDerivWithinAt`); Mathlib `StrongConvexOn`, `PiLp`; LMLExplore `simplex` (`Analysis/Convex/Simplex.lean`) |
| Linear algebra | Mathlib `ContinuousLinearMap.IsPositive` and its Loewner order, `LinearMap.det`, `Matrix.det_one_add_replicateCol_mul_replicateRow`, `Matrix.add_mul_mul_inv_eq_sub`; Tau Ceti [`Frame.lean`][tc-frame] (`frameOperator`) and [`AffineNormalization.lean`][tc-affine] (`IsCompact.exists_affineBasis_abs_coord_le_one`) |

The [Kiefer–Wolfowitz formalization in `colt-2026-83`][kw] (Apache-2.0, no `sorry`) proves the
Expand Down Expand Up @@ -328,7 +328,14 @@ a prior over environments); do not restate its results.

## Layer 6: Convex analysis and online linear optimization

Work in a finite-dimensional real inner product space `E`. Losses are minimized.
Work in a finite-dimensional real normed space `E`, paired with its dual `E →L[ℝ] ℝ` by
`(x, y) ↦ y x`; this is the bilinear pairing that Tau Ceti's `fenchelConjugate` takes. Losses and
gradients live in the dual: the loss of a play `a` under the loss `y` is `y a`, and the regret
against `u` after `n` rounds is $\sum_{t<n}y_t(a_t-u)$. Strong convexity refers to the norm of `E`
(Mathlib's `StrongConvexOn`), and the norm of a loss is its operator norm, the dual norm. Losses
are minimized. Statements whose proofs do not use the dimension, such as the FTRL bounds of item 3,
are stated without it. The merged FTRL development of LMLExplore is restated in this generality by
the [Refactors](../Refactors/README.md) roadmap, Layer 0.1.

1. **Legendre functions.** For a convex function $F$ with domain $D$ (represent it as `F : E → ℝ`
with a convex set `D`, or as `E → EReal`; choose one representation and give conversions to
Expand All @@ -348,11 +355,16 @@ Work in a finite-dimensional real inner product space `E`. Losses are minimized.
directional derivatives, and [LS, Corollary 28.8]. The bounds hold for losses chosen adaptively
from past actions.
4. **Two instances.** Prove [LS, Proposition 28.6] (unit ball, $F=\tfrac12\|a\|^2$,
$\eta=n^{-1/2}$: $R_n\le\sqrt n$) and [LS, Proposition 28.7] (simplex, unnormalized negative
entropy, $\eta=\sqrt{2\log(d)/n}$: $R_n\le\sqrt{2n\log d}$). Identify the latter with exponential
weights over a finite set, stated on `α → ℝ` with `stdSimplex`.

Generalization: an inner product space rather than $\mathbb R^d$; the instances are corollaries.
$\eta=n^{-1/2}$: $R_n\le\sqrt n$) on a real inner product space, with the losses
`InnerProductSpace.toDual ℝ E g` of vectors of norm at most `1`. Prove [LS, Proposition 28.7]
(simplex, unnormalized negative entropy, $\eta=\sqrt{2\log(d)/n}$: $R_n\le\sqrt{2n\log d}$)
on `E = PiLp 1 (fun _ : α ↦ ℝ)`, whose dual norm is the sup norm, from the `1`-strong convexity
of the negative entropy on the simplex for the `ℓ¹` norm (Pinsker's inequality). Identify the
latter with exponential weights over a finite set, stated on `α → ℝ` with LMLExplore's
`simplex α`.

Generalization: a normed space with losses in its dual, rather than $\mathbb R^d$ with the
Euclidean pairing; the instances are corollaries.

## Layer 7: Adversarial bandits with finitely many arms and expert advice

Expand Down
24 changes: 13 additions & 11 deletions LMLRoadmaps/Bandits/Suggested.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -237,17 +237,19 @@ theorem lai_robbins_gaussian {alg : Algorithm Unit α ℝ} {σ2 : ℝ≥0}

section OnlineLinear

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

/-- The regret bound of follow-the-regularized-leader [LS, Theorem 28.5], for a potential that is
differentiable at the iterates; `a t` minimizes `η ⟪·, ∑_{s<t} y s⟫ + F` over `K`. -/
theorem ftrl_regret_le {F : E → ℝ} {K : Set E} (hK : Convex ℝ K) (hF : ConvexOn ℝ K F)
{η : ℝ} (hη : 0 < η) (y a : ℕ → E)
(ha : ∀ t, IsMinOn (fun b ↦ η * ∑ s ∈ range t, ⟪b, y s⟫_ℝ + F b) K (a t))
(hdiff : ∀ t, DifferentiableAt ℝ F (a t)) {u : E} (hu : u ∈ K) (n : ℕ) :
∑ t ∈ range n, ⟪a t - u, y t⟫_ℝ ≤
(F u - F (a 0)) / η + ∑ t ∈ range n, ⟪a t - a (t + 1), y t⟫_ℝ -
(∑ t ∈ range n, bregDiv F (a (t + 1)) (a t) (fderiv ℝ F (a t))) / η :=
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

/-- The regret bound of follow-the-regularized-leader [LS, Theorem 28.5], on a normed space with
losses `y t` in the dual, for a potential with a derivative `F' t` within `K` at each play; each
play `a t ∈ K` minimizes `b ↦ η ∑_{s<t} y s b + F b` over `K`. -/
theorem ftrl_regret_le {F : E → ℝ} {K : Set E} (hK : Convex ℝ K) {η : ℝ} (hη : 0 < η)
(y : ℕ → E →L[ℝ] ℝ) (a : ℕ → E) {n : ℕ} (ha_mem : ∀ t ≤ n, a t ∈ K)
(ha : ∀ t ≤ n, IsMinOn (fun b ↦ η * ∑ s ∈ range t, y s b + F b) K (a t))
(F' : ℕ → E →L[ℝ] ℝ) (hF' : ∀ t < n, HasFDerivWithinAt F (F' t) K (a t)) {u : E}
(hu : u ∈ K) :
∑ t ∈ range n, y t (a t - u) ≤
(F u - F (a 0)) / η + ∑ t ∈ range n, y t (a t - a (t + 1)) -
(∑ t ∈ range n, bregDiv F (a (t + 1)) (a t) (F' t)) / η :=
sorry

end OnlineLinear
Expand Down
Loading