[RemyDegenne]

This PR completes OnlineLearning Layer 2.1 (constant rates on unbounded sets [Ora, Theorem 2.13, Lemmas 2.12 and 2.31]) and Layer 2.2 (strongly convex losses [Ora, Theorem 4.7, Corollary 4.8, Example 4.11]) of the milestone "Layer 2: Online subgradient descent beyond √n". It also passes the guessing-game completion check that the roadmap sets for item 2.

Roadmap: OnlineLearning

In OnlineLearning/SubgradientDescent.lean (real inner product space, subgradients within K as LML's HasSubgradientWithinAt, plays given by nearest-point hypotheses like the existing onlineSubgradientDescent_regret_le, new bounds stated with Layer 0.1's regret):

• inner_sub_le_of_isMinOn_norm_sub is Lemma 2.12/2.31, one projected step: ⟪g, a - u⟫ ≤ (‖u - a‖² - ‖u - x‖²)/(2η) + η/2 ‖g‖² for x a nearest point of K to a - η • g. It is proved from the mirror-descent one-step inequality IsMirrorDescentStep.apply_sub_le with the potential ‖·‖²/2, together with apply_sub_sub_div_le_of_mul_norm_sq_le.
• onlineSubgradientDescent_regret_le_norm_sub_sq_div is Theorem 2.13 with a constant rate: (‖u - a 0‖² - ‖u - a n‖²)/(2η) + η/2 ∑ ‖g t‖². It needs no diameter and no a 0 ∈ K.
• onlineSubgradientDescent_regret_le_of_antitone is Theorem 2.13 with nonincreasing rates. It keeps -‖u - a n‖²/(2η (n-1)) and assumes only ‖u - a t‖ ≤ D for t < n, not a diameter. It takes 0 < n, without which it would claim ‖u - a 0‖ ≤ D.
• onlineSubgradientDescent_regret_le_sum_norm_sq_div is Theorem 4.7, under strong convexity at the plays (f t (a t) + ⟪g t, v - a t⟫ + μ t/2 ‖v - a t‖² ≤ f t v on K) with rates (∑ s ≤ t, μ s)⁻¹. The bound is ∑ ‖g t‖²/(2 ∑ s ≤ t, μ s). Only the partial sums must be positive; the individual μ t may be negative. The proof telescopes the potential (∑ s < t, μ s)/2 ‖u - a t‖².
• onlineSubgradientDescent_regret_le_of_strongConvexOn is the same bound for μ t-strongly convex losses with subgradients at the plays, through StrongConvexOn.add_add_le_of_hasSubgradientWithinAt (Layer 1.1).
• onlineSubgradientDescent_regret_le_mul_one_add_log is Corollary 4.8: L²/(2μ) (1 + log n) for μ-strongly convex losses with ‖g t‖ ≤ L at the plays, from Real.sum_range_inv_add_one_le.
• onlineSubgradientDescent_regret_sq_sub_le_one_add_log is Example 4.11 and the Layer 2 completion check. Corollary 4.8 with μ = 2, L = 2 gives regret at most 1 + log n on the guessing game (a - y t)² on [0, 1], for the explicit plays x (t+1) = x t - (x t - y t)/(t+1). These are OSD steps that never leave [0, 1]. The follow-the-leader version regret_sq_sub_le_one_add_log (Layer 5.3) instead takes its plays as minimizers. This one comes from the OSD bound, as the roadmap's check asks.

In OnlineLearning/MirrorDescent.lean:

• New sum_apply_sub_le_mirrorDescent_of_antitone: the nonincreasing-rate bound (D - D_F(u, a n))/η (n-1) + ∑ stability terms, keeping the last divergence. It needs neither convexity of F nor a 0 ∈ K. The summation-by-parts estimate that mirrorDescent_regret_le_of_antitone did inline now lives here, and that theorem is re-derived from it with the same statement.
• The existing onlineSubgradientDescent_regret_le (diameter form) is likewise re-proved from the new onlineSubgradientDescent_regret_le_of_antitone, with its statement unchanged.

No public declaration is removed or renamed.

Reuse: I found no projected-step inequality, OSD bound for strongly convex losses, or logarithmic-regret statement in Mathlib, Tau Ceti, LML or Statlib. I grepped for onlineSubgradientDescent, nearest-point IsMinOn (fun b ↦ ‖b - …‖) hypotheses and inner_sub_le_of_isMinOn. Mathlib's norm_eq_iInf_iff_real_inner_le_zero characterizes projections through ⨅, not nearest-point minimizers, so the one-step lemma goes through the existing mirror-descent API instead. The proofs reuse isMirrorDescentStep_norm_sq_div_two_iff, bregDiv_norm_sq_div_two, hasFDerivAt_norm_sq_div_two, sum_apply_sub_le_mirrorDescent, sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt, strongConvexOn_div_two_mul_norm_sub_sq and Real.sum_range_inv_add_one_le. Credit for logarithmic regret goes to [HAK07] in the module docstring, alongside [Ora].

What remains on this milestone after this PR: Layer 2.3 (adaptive rates and L* bounds, which also need the Layer 1.7 numerical lemmas in flight in #379 and Layer 1.3's self-bounded functions) and Layer 2.4 (AdaGrad).

Local checks only (CI verifies the pushed PR): scope: scoped: against 7fc78707241a5393aa85a7751e472cf1cb45fca9. local-axioms: checked 2 changed module(s), 80 declaration(s); 0 violation(s). The whole-library lake build --iofail, source guards, module-system audit, header check and environment lint (checked 2 changed module(s), 80 declarations; 14 environment linters) passed, and the verify script exited 0.

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The new one-step, constant-rate, nonincreasing-rate, strongly-convex, logarithmic and guessing-game statements faithfully formalize Ora Lemma 2.12/2.31, Theorem 2.13, Theorem 4.7, Corollary 4.8 and Example 4.11. The generalizations (a 0 need not be in K, partial-sum positivity, a distance bound in place of the diameter, the kept last term) are sound and non-vacuous, and the refactored theorems keep their statements.
✅	reuse	approved	claude/claude-opus-5-5	The new projected-step, constant-rate, keep-last-distance, strongly convex and logarithmic-regret bounds have no counterpart in LMLExplore and are built on the existing mirror-descent, Bregman, strong-convexity and harmonic-bound API. The squared-loss facts are factored into shared lemmas used by both the FTL and OSD guessing-game proofs, and the summation-by-parts estimate now lives in one place.
✅	scope	approved	claude/claude-opus-5-5	New material implements OnlineLearning Layer 2 items 1 (constant and nonincreasing rates without a diameter bound, from the mirror-descent bound with potential ‖·‖²/2) and 2 (Theorem 4.7, Corollary 4.8), plus the guessing-game completion check, exactly as stated at roadmap/LMLRoadmaps/OnlineLearning/README.md:381-393 and 413-414. The MirrorDescent factoring and the squared-loss lemmas extracted from FTRL/Quadratic.lean are used directly by the new theorems, so the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	New results cite Orabona by precise lemma, theorem, corollary and example numbers, HAK07 is credited for logarithmic regret, and Zin03 is retained. The extracted squared-loss lemmas and the summation-by-parts refactor are internal code moves, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The squared-loss lemmas now live in Analysis/Convex/Bregman/Euclidean.lean and both online-learning files use them, so the FTRL import is gone and the earlier finding is fixed. The new surface is theorems only (roadmap products and reusable one-step and antitone mirror-descent bounds), with no compatibility artifacts and no new definitions needing characteristic API.
✅	generality	approved	claude/claude-opus-5-5	The general bounds (one-step projected inequality, nonincreasing-rate mirror-descent bound keeping the last divergence, strong convexity at the plays) are proved first, and the diameter, StrongConvexOn, log-regret and guessing-game forms are short reductions with no duplicated proofs. Hypotheses are minimal and used: partial-sum positivity, distances to u, 0 < n, and a 0 ∈ K only where play membership is needed.
✅	placement	approved	claude/claude-opus-5-5	The squared-loss lemmas were moved to Analysis/Convex/Bregman/Euclidean.lean next to strongConvexOn_div_two_mul_norm_sub_sq, which resolves the prior FTRL-import finding. Every new declaration is in its natural home and every added import is used.
✅	naming	approved	claude/claude-opus-5-5	Each new name (strongConvexOn_sq_sub, hasSubgradientWithinAt_sq_sub, inner_sub_sub_norm_sq_div_le, inner_sub_le_of_isMinOn_norm_sub, sum_apply_sub_le_mirrorDescent_of_antitone and the onlineSubgradientDescent_regret_le_* family) describes its conclusion and follows the naming patterns of neighbouring declarations; none overstates its statement. No notation is introduced, and everything sits in the correct LMLExplore namespace, with no clashing duplicates found by grep.
✅	documentation	approved	claude/claude-opus-5-5	The new public theorems in SubgradientDescent.lean, MirrorDescent.lean and Euclidean.lean all have docstrings that match their statements, including the rates, the 0 < n and partial-sum hypotheses, and the assumptions they say are not needed (a 0 ∈ K, nonnegative μ t, convexity of F). The module docstrings list the new material, credit [Ora] and [HAK07] in the file, and contain no roadmap or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	Shared facts (one-step stability bound, squared-loss strong convexity and subgradient, the antitone summation-by-parts estimate) are factored into reusable lemmas and reused across the file and in FTRL/Quadratic. Proofs are short, commented at their key steps, free of change/show or defeq reliance, and close with linarith/field_simp/positivity rather than brittle rewrite chains.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 6e2f873. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.56.}