[RemyDegenne]

Amends the Bandits roadmap, Layer 6, so that online linear optimization works in a finite-dimensional real normed space paired with its dual, instead of an inner product space. Companion to #5 (the Refactors roadmap, Layer 0.1, which restates the merged FTRL code in this generality).

Why. In an inner product space, strong convexity and the dual norm can only refer to the Euclidean norm. The standard bound for exponential weights, [LS, Proposition 28.7], uses the 1-strong convexity of the negative entropy for the ℓ¹ norm (Pinsker's inequality), with dual norm ℓ∞. With losses y : E →L[ℝ] ℝ on a normed space, [LS, Corollary 28.8] holds for every norm by the choice of E, and Proposition 28.7 is the case E = PiLp 1 (fun _ : α ↦ ℝ).

Changes (only LMLRoadmaps/Bandits/):

• Layer 6 convention. Work in a finite-dimensional real normed space, paired with its dual by (x, y) ↦ y x. This is the pairing Tau Ceti's fenchelConjugate takes, so items 6.1–6.2 fit unchanged. The regret is ∑ y t (a t - u). Strong convexity uses the norm of E, and the norm of a loss is its operator norm. Results whose proofs don't use the dimension, such as the FTRL bounds, drop that assumption. The convention points to Refactors Layer 0.1 for the merged code.
• 6.4. Proposition 28.6 stays on inner product spaces, with losses InnerProductSpace.toDual ℝ E g. Proposition 28.7 is on PiLp 1, stated on α → ℝ with LMLExplore's simplex α instead of the deprecated stdSimplex.
• The "Generalization" line of Layer 6, and the convex-analysis row of the dependency table (simplex, PiLp, and the bilinear-pairing form of fenchelConjugate).
• Suggested.lean. ftrl_regret_le is restated on a normed space with dual losses and a derivative within K. The convexity and global differentiability assumptions are dropped, since the proof doesn't use them.

Suggested.lean builds.

Drafted with Claude Opus 5.5 at the request of the code owner.

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1