[RemyDegenne]

This PR adds OnlineLearning Layer 2.3, adaptive rates and L⋆ bounds [Ora, Theorems 4.14 and 4.30], to the milestone "Layer 2: Online subgradient descent beyond √n". It also adds the self-bounded part of Layer 1.3 (smoothness and self-bounded functions [Ora, Definition 4.26, Remark 4.27]), which the L⋆ bound of Layer 2.3 consumes through onlineSubgradientDescent_regret_le_of_selfBoundedOn. After this PR, the milestone still needs Layer 2.4 (AdaGrad). Layer 1.3 still needs its last bullet, "a self-bounded function on a convex set is convex".

Roadmap: OnlineLearning

New file LMLExplore/OnlineLearning/AdaptiveRate.lean:

• mirrorDescent_regret_le_two_mul_sqrt is the first bullet of 2.3. Take mirror descent with an m-strongly convex potential, D_F(u, a t) ≤ B, and the rates η t = √(m B / ∑ s ≤ t, ‖y s‖²). Then ∑ t < n, y t (a t - u) ≤ 2 √(B ∑ ‖y t‖² / m). The roadmap says "no step while the sum is 0". Lean's division makes that rate 0, and a mirror-descent step for the rate 0 is a Bregman projection of the current play, so the algorithm stays put. No separate case is needed in the hypotheses. The proof freezes the rates at the first round t₀ with a nonzero loss; before t₀ the steps are unchanged because the loss is 0. It then applies the existing mirrorDescent_regret_le_of_strongConvexOn_of_antitone and Layer 1.7's Real.sum_div_sqrt_le_two_mul_sqrt. The degenerate cases n = 0, all losses zero and B = 0 are handled. No sign hypothesis on B is needed.
• onlineSubgradientDescent_regret_le_mul_sqrt_sum is Theorem 4.14: projected OSD with η t = D / √(2 ∑ s ≤ t, ‖g s‖²) has regret at most D √(2 ∑ ‖g t‖²). As in the existing onlineSubgradientDescent_regret_le_of_antitone, it only assumes ‖u - a t‖ ≤ D at the plays, which is weaker than a diameter bound.
• onlineSubgradientDescent_regret_le_of_norm_sq_le is the L⋆ bound 4 s D² + 2 D √(s ∑ t < n, f t u), for subgradients with ‖g t‖² ≤ 2 s f t (a t) at the plays. It solves the implicit inequality with Layer 1.7's Real.le_add_add_sqrt_of_sub_sqrt_le.
• onlineSubgradientDescent_regret_le_of_selfBoundedOn is the roadmap's statement for nonnegative s-self-bounded losses, as a corollary. Convexity is used only through the subgradients at the plays.
• A private helper, mirrorDescent_regret_le_two_mul_sqrt_of_ne_zero, holds the positive-rate case so that no proof exceeds 50 lines.

In LMLExplore/Analysis/Convex/Smooth.lean, next to the existing SmoothOn and the descent lemma:

• SelfBoundedOn V s f is the roadmap's definition: bounded below on V, and ‖g‖² ≤ 2 s (f x - sInf (f '' V)) for every subgradient g within V at x ∈ V, using LML's HasSubgradientWithinAt. s : ℝ≥0 matches SmoothOn.
• SmoothOn.norm_fderiv_sq_le: if f is s-smooth on E and bounded below, then ‖fderiv ℝ f x‖² ≤ 2 s (f x - ⨅ y, f y). The proof applies the descent lemma along each direction and then Mathlib's discrim_le_zero. It works in any normed space, with no attainment of the dual norm.
• SmoothOn.selfBoundedOn_univ: a smooth function bounded below is self-bounded. The roadmap states this for convex functions, but uniqueness of the subgradient at a differentiable point (LML's HasFDerivAt.eq_of_hasSubgradientWithinAt) makes convexity unnecessary. Bounded below is required, since it is part of the definition.
• SelfBoundedOn.weaken and SelfBoundedOn.norm_sq_le_of_nonneg (‖g‖² ≤ 2 s f x for nonnegative f).

In LMLExplore/OnlineLearning/MirrorDescent.lean: new @[simp] isMirrorDescentStep_zero_iff. A step for the zero loss is a Bregman projection of the current play, whatever the learning rate.

No public declaration is removed or renamed.

Reuse: I grepped Mathlib, Tau Ceti, LML and Statlib at the pinned versions for SelfBounded/self-bounded, for gradient bounds of the form ‖fderiv ℝ f x‖ ^ 2 ≤ 2 * s * (f x - …), and for adaptive learning rates. The only near hits are unrelated Tau Ceti PDE estimates (norm_fderiv_sq_le_of_norm_fderiv_le). The new proofs reuse the merged mirror-descent and OSD API (mirrorDescent_regret_le_of_strongConvexOn_of_antitone, isMirrorDescentStep_norm_sq_div_two_iff, bregDiv_norm_sq_div_two, sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt) and the Layer 1.7 numerical lemmas from #379.

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

🤖 Prepared with Claude Code

[RemyDegenne]

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

The new isMirrorDescentStep_zero_iff re-proves from scratch a special case of the existing isMirrorDescentStep_iff_isMinOn_bregDiv; the rest of the PR (self-bounded functions, the smooth-gradient bound, the adaptive-rate and L⋆ bounds) is new and reuses the merged mirror-descent, subgradient-descent and Layer 1.7 API.

• LMLExplore/OnlineLearning/MirrorDescent.lean:119 — isMirrorDescentStep_zero_iff restates isMirrorDescentStep_iff_isMinOn_bregDiv with loss 0 and base point a (G = F' - η • 0 = F'), and proves it again by hand with simpa. Fix: Keep the @[simp] statement but prove it as isMirrorDescentStep_iff_isMinOn_bregDiv (by simp) a a x. Alternatively, delete it and use that lemma at its one call site in AdaptiveRate.lean (the ha' step).

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 · 46s · 304.6k in (285.8k cache read, 18.8k cache write) / 3.7k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

Proofs are well structured and commented, but one rewrite chain for √(c² · X) = c · √X is repeated three times instead of being factored into a lemma, and one step relies on the iInf/sInf definitional equality where Mathlib's sInf_range is available.

• LMLExplore/OnlineLearning/AdaptiveRate.lean:233 — The same brittle chain show … = c ^ 2 * X by ring, Real.sqrt_mul (sq_nonneg _), Real.sqrt_sq _ that rewrites √(c² · X) as c · √X is repeated at lines 233, 266 and 272. The same pattern already appears elsewhere in the repo. Fix: Add a small lemma such as Real.sqrt_sq_mul (hc : 0 ≤ c) : √(c ^ 2 * x) = c * √x (next to the other Layer 1.7 lemmas in LMLExplore/Analysis/Real/Sqrt.lean) and use it at all three sites.
• LMLExplore/Analysis/Convex/Smooth.lean:289 — exact hf.norm_fderiv_sq_le hbdd x closes a goal stated with sInf (range f) using a lemma stated with ⨅ y, f y, so it relies on the definitional unfolding of iInf. A comment notes this, but an explicit lemma is available. Fix: Rewrite with sInf_range (add it after image_univ in the rw) and drop the comment.

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 · 38s · 125.2k in (117.3k cache read, 7.9k cache write) / 3.6k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[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	Definitions and theorems match [Ora, Def. 4.26, Thms 4.14, 4.30] and the roadmap's Layer 2.3 and 1.3 bullets; the PR drops convexity where it is unneeded, which only generalizes the roadmap's statements. SelfBoundedOn has both a consumer and a non-trivial witness, and the L⋆ algebra (4sD² + 2D√(sU)) checks out.
✅	reuse	approved	claude/claude-opus-5-5	The new self-bounded API, the smooth-gradient bound, the zero-loss mirror-descent step and the adaptive-rate and L⋆ theorems have no existing counterparts in Mathlib or LMLExplore, and they reuse the merged mirror-descent and OSD API, the Layer 1.7 numerical lemmas and Mathlib's discrim_le_zero. The private balancing helper is close to Real.div_sqrt_add_sqrt_mul_div_two but uses a different parametrization, so switching to it would not simplify the proof.
✅	scope	approved	claude/claude-opus-5-5	The PR implements OnlineLearning Layer 2.3 (all three bullets) and the Layer 1.3 self-bounded bullets that Layer 2.3 directly cites as its prerequisite, as one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	The new material follows Orabona's notes, which are cited in both changed files' References and by result number in the docstrings. The roadmap is credited only in the PR description, and no uncredited formal source is followed.
✅	api-design	approved	claude/claude-opus-5-5	The new surface (SelfBoundedOn with its weaken/norm_sq_le_of_nonneg API, SmoothOn.norm_fderiv_sq_le and selfBoundedOn_univ, the @[simp] isMirrorDescentStep_zero_iff, and the four Layer 2.3 theorems) is minimal and matches the roadmap. The private helpers are proof-specific, no bodies are exposed, and there is no compatibility layer.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: the general mirror-descent adaptive bound is proved first and the OSD and self-bounded L⋆ results are derived from it, with no visibly unused or over-strong hypotheses. The univ-only restriction of SmoothOn.selfBoundedOn_univ is required by the argument, and weaken matches the existing SmoothOn.weaken.
✅	placement	approved	claude/claude-opus-5-5	New declarations sit in their canonical homes (Layer 1.3 self-bounded material in Analysis/Convex/Smooth.lean, the zero-loss step iff in MirrorDescent.lean, Layer 2.3 in a new OnlineLearning/AdaptiveRate.lean), and every added import is used and specific.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions and match adjacent conventions (*_regret_le_*, SmoothOn.weaken/SelfBoundedOn.weaken, isMirrorDescentStep_zero_iff is a genuine iff); namespaces are correct and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new module and every new public declaration have docstrings that accurately describe their statements, including the zero-rate behaviour and the no-convexity claim for smooth functions. No overclaiming or process narrative was found.
✅	proof-quality	approved	claude/claude-opus-5-5	The proofs are well structured and commented. The positive-rate case of the adaptive bound is split into a private helper, the zero-loss steps are reconciled through the explicit isMirrorDescentStep_zero_iff rather than by definitional unfolding, and nothing goes past 50 lines or relies on an undocumented change, show or defeq.

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

_{Reviewing this diff at head 1907755. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.44.}