[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]

🟡 reuse — request_changes claude/claude-opus-5-5

The new OSD bounds (projected one-step inequality, constant and antitone rate bounds, strongly convex and logarithmic regret) add material I could not find elsewhere, but the guessing-game proof copies the strong-convexity and subgradient facts already proved in FTRL/Quadratic.lean, and one membership proof redoes mem_of_isMirrorDescentStep.

• LMLExplore/OnlineLearning/SubgradientDescent.lean:428 — In onlineSubgradientDescent_regret_sq_sub_le_one_add_log, hf (2-strong convexity of (a - y t)^2 on [0,1]) copies hℓ in regret_sq_sub_le_one_add_log verbatim, and hg (line 432) repeats that theorem's subgradient proof with innerSL instead of toSpanSingleton. Fix: Factor public lemmas next to regret_sq_sub_le_one_add_log in FTRL/Quadratic.lean, e.g. strongConvexOn_sq_sub (y : ℝ) : StrongConvexOn (Set.Icc 0 1) 2 fun a ↦ (a - y) ^ 2 and the subgradient 2 * (x - y) at x, and use them in both theorems.
• LMLExplore/OnlineLearning/SubgradientDescent.lean:362 — In onlineSubgradientDescent_regret_le_of_strongConvexOn, h_mem repeats the pattern-match proof of mem_of_isMirrorDescentStep (| 0, _ => ha0 | t + 1, ht => ...). Fix: Use mem_of_isMirrorDescentStep ha0 (fun t ht ↦ isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht)) t ht.le, as onlineSubgradientDescent_regret_le already does at line 223.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 40s · 203.1k in (160.9k cache read, 42.2k cache write) / 3.6k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

The proofs are well structured, commented and mostly robust. The stability bound for the potential ‖·‖²/2 is proved inline twice with ad hoc coercion and mul_one patches instead of being factored or taken from the existing quadratic helper.

• LMLExplore/OnlineLearning/SubgradientDescent.lean:133 — inner_sub_le_of_isMinOn_norm_sub (L133) and onlineSubgradientDescent_regret_le_of_antitone (L195) both rebuild the bound ⟪g, a - b⟫ - ‖b - a‖²/2/η ≤ η/2 * ‖g‖² inline. Each calls apply_sub_sub_div_le_of_mul_norm_sq_le one_pos … with a le_of_eq (by ring) hypothesis, and the first also patches η / (2 * 1) with h_eq' … rw [mul_one]. Fix: Factor one lemma, e.g. inner_sub_sub_norm_sq_div_le (hη : 0 < η) : ⟪g, a - b⟫ - ‖b - a‖ ^ 2 / 2 / η ≤ η / 2 * ‖g‖ ^ 2, derived from apply_sub_sub_mul_norm_sq_le, and use it at both sites so that h_eq' and the le_of_eq (by ring) casts disappear.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 43s · 136k in (123.5k cache read, 12.5k cache write) / 3.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

AI review — changes requested

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-regret and guessing-game statements faithfully formalize Ora Lemma 2.12, Theorems 2.13 and 4.7, Corollary 4.8 and Example 4.11, using the repo's regret and the Mathlib strong-convexity convention; the generalizations (no a 0 ∈ K, possibly negative μ t with positive partial sums, a distance bound instead of a diameter) are sound and none is vacuous.
🟡	reuse	changes requested	claude/claude-opus-5-5	The new OSD bounds (projected one-step inequality, constant and antitone rate bounds, strongly convex and logarithmic regret) add material I could not find elsewhere, but the guessing-game proof copies the strong-convexity and subgradient facts already proved in FTRL/Quadratic.lean, and one membership proof redoes mem_of_isMirrorDescentStep.
✅	scope	approved	claude/claude-opus-5-5	New material implements OnlineLearning Layer 2 items 1 (constant/nonincreasing rates on unbounded sets) and 2 (strongly convex losses, log regret, Example 4.11) as stated in the roadmap at README.md:381-394. The MirrorDescent factoring is the prerequisite item 1's nonincreasing-rate form needs, so the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	New results cite Orabona's book by specific lemma/theorem/corollary/example numbers, with HAK07 added for logarithmic regret and Zin03 retained. The roadmap is credited only in the PR description, and the summation-by-parts refactor is internal code that needs no external credit.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds only public theorems that are roadmap products (Ora 2.12/2.13/4.7/4.8/4.11) or a reusable one-step inequality, with no compatibility artifacts, no new definitions and no duplicate names. The guessing-game theorem's hypotheses differ from the existing FTRL regret_sq_sub_le_one_add_log, so it is not a duplicate.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: general mirror-descent and at-the-plays bounds come first, and the diameter, StrongConvexOn, log-regret and guessing-game forms are derived from them with no repeated proofs. Every hypothesis (0 < n, a 0 ∈ K only where needed, partial-sum positivity rather than μ t ≥ 0, distances to u rather than diameter) is used and minimal.
✅	placement	approved	claude/claude-opus-5-5	The general nonincreasing-rate mirror descent bound sits in MirrorDescent.lean next to the theorem it now feeds, and the subgradient-descent-specific step, regret and guessing-game results sit in SubgradientDescent.lean. Both new imports (Harmonic.Bounds for Real.sum_range_inv_add_one_le, Regret for regret/regret_def) are used.
✅	naming	approved	claude/claude-opus-5-5	The new names describe their conclusions and match the patterns already used in the files (sum_apply_sub_le_mirrorDescent, mirrorDescent_regret_le_bregDiv_div, regret_sq_sub_le_one_add_log). The PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	Both module docstrings and all new public theorem docstrings accurately describe the statements, including their hypotheses, rates, and the explicitly non-required assumptions; references [Ora] and [HAK07] are credited in-file with no process or roadmap narrative.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The proofs are well structured, commented and mostly robust. The stability bound for the potential ‖·‖²/2 is proved inline twice with ad hoc coercion and mul_one patches instead of being factored or taken from the existing quadratic helper.

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

_{Reviewing this diff at head 279e1f9. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.25.}