[RemyDegenne]

This PR finishes OnlineLearning Layer 5.2, The FTRL bound for convex losses, with its last bullet, FTRL-Proximal [Ora, Example 7.9]. It also completes Layer 5.3, Follow-the-leader on strongly convex losses [Ora, Corollary 7.25, Algorithm 7.5, Example 7.26], including the Layer 5 completion check (follow-the-leader on the guessing game has regret at most 1 + log n). Both rest on one new statement: the proximal stability lemma [Ora, Lemma 7.7], already on main, summed through the FTRL equality. FTRL-Proximal and follow-the-leader (FTL) on quadratized losses are the same algorithm: FTRL with quadratic terms c / 2 * ‖a - x s‖ ^ 2 centred at the past plays, run on linear losses. So the PR is one topic.

Roadmap: OnlineLearning

In OnlineLearning/FTRL/Stability.lean (normed space, subgradients within V as in LML's HasSubgradientWithinAt):

• regret_le_ftrl_of_isMinOn_sub_of_strongConvexOn [Ora, Lemmas 7.1 and 7.7]. If each play also minimizes ψ (t + 1) - ψ t and F (t + 1) is lam t-strongly convex, then regret ≤ ψ n u - ψ 0 (x 0) + ∑ ‖g t‖² / (2 lam t) + ∑ (ψ t (x t) - ψ (t + 1) (x t)). This is the proximal counterpart of regret_le_ftrl_of_strongConvexOn, with the same hypothesis shapes. It is built from ftrl_stability_le_norm_sq_div_of_isMinOn_sub_of_strongConvexOn.
• regret_le_ftl_of_strongConvexOn (5.3, first bullet). Take μ t-strongly convex losses whose partial sums ∑ s ≤ t, μ s are positive, and let x 0 be any point of V. Then regret ≤ ∑ ‖g t‖² / (2 ∑ s ≤ t, μ s). Individual moduli may be negative. Plays are needed only for t < n, and the comparator is any u ∈ V.

New file OnlineLearning/FTRL/Quadratic.lean (inner product space):

• regret_le_ftrl_proximal (5.2, last bullet). Take convex losses and weights σ t ≥ 0 with positive partial sums, and plays minimizing ∑ s < t, (σ s / 2 * ‖a - x s‖² + ℓ s a). Then regret ≤ ∑ σ t / 2 * ‖u - x t‖² + ∑ ‖g t‖² / (2 ∑ s ≤ t, σ s).
• regret_le_ftl_quadratized (5.3, second bullet, first half). Assume the losses lie above ℓ t (x t) + g t (· - x t) + μ t / 2 * ‖· - x t‖² at the plays. Then FTL on g t a + μ t / 2 * ‖a - x t‖² has the same bound.
• isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff (5.3, second bullet, second half: "its plays are projections of a closed form", [Ora, (7.9)]). It completes the square. The minimizers over any set of ∑ i, (⟪v i, ·⟫ + μ i / 2 * ‖· - x i‖²) with ∑ μ i > 0 are the nearest points to (∑ μ i)⁻¹ • ∑ (μ i • x i - v i). This is the same projection convention as isMirrorDescentStep_norm_sq_div_two_iff.
• regret_sq_sub_le_one_add_log (Layer 5 completion check). FTL on (a - y t)² on [0, 1] has regret at most 1 + log n, against the 4 + 4 log n of [Ora, Theorem 1.3]. It uses Real.sum_range_inv_add_one_le.

Small supporting API, each consumed here:

• StrongConvexOn.fun_sum (Analysis/Convex/Strong.lean): finite sums of m i-strongly convex functions are (∑ m i)-strongly convex. It is used by both FTL and FTRL-Proximal. Mathlib, Tau Ceti, LML and Statlib have only the binary UniformConvexOn.add.
• strongConvexOn_div_two_mul_norm_sub_sq (Analysis/Convex/Bregman/Euclidean.lean): m / 2 * ‖b - c‖² is m-strongly convex for every real m. The existing strongConvexOn_norm_sq_div_two is now derived from it, with an unchanged statement.
• regret_congr (OnlineLearning/Regret.lean): the regret after n rounds depends only on the first n plays. It is the play-side sibling of dynRegret_congr.

No public declaration is removed or renamed.

What remains: Layer 5 now needs only 5.4 (composite losses and the proximal operator). The roadmap's Layer 7.4 variance bound consumes regret_le_ftl_of_strongConvexOn (FTL on ‖x - g t‖²).

Local checks only (CI verifies the pushed PR): scope: scoped: against 04108426374e73cba755bc601e1792d03176b28a. local-axioms: checked 5 changed module(s), 127 declaration(s); 0 violation(s). The whole-library lake build --iofail, the source guards, the module-system audit, the header and style checks (rerun after replacing a combining tilde in a docstring), the environment lint (checked 5 changed module(s), 127 declarations) and the shim-expiry check all passed.

🤖 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	Every new statement matches the cited mathematics of [Ora, Lemma 7.7, Example 7.9, Corollary 7.25, (7.9), Example 7.26], and no hypothesis carries the main content. I checked the completed square in the minimizer characterisation, the ℓ ≤ ℓ' regret transfer, the comparator substitution in FTL, the constants of the guessing game (4/(2·2(t+1)) ≤ 1/(t+1)) and the n = 0 edge case, and all of them hold.
✅	reuse	approved	claude/claude-opus-5-5	The prior duplication finding is fixed: regret_le_ftrl_proximal now follows from regret_le_ftl_of_strongConvexOn instead of copying its padding scaffold. Searches of LMLExplore and Mathlib found no existing match for StrongConvexOn.fun_sum, strongConvexOn_div_two_mul_norm_sub_sq, regret_congr, the completing-the-square lemma or the follow-the-leader bounds.
✅	scope	approved	claude/claude-opus-5-5	Each new theorem matches a named OnlineLearning Layer 5 item (5.2 FTRL-Proximal, both 5.3 bullets, and the Layer 5 completion check), and every supporting lemma is used by them. The PR is one topic: FTRL-Proximal and FTL derived from the summed proximal stability bound.
✅	attribution	approved	claude/claude-opus-5-5	All new results cite their sections of Orabona (Lemmas 7.1/7.7, Example 7.9, Corollary 7.25, Algorithm 7.5, (7.9), Example 7.26, Theorem 1.3) in docstrings and module references; the supporting lemmas are routine and need no further credit.
✅	api-design	approved	claude/claude-opus-5-5	The new public surface is the roadmap's FTRL-Proximal and FTL results plus three small reusable lemmas, each used in this PR and placed in its canonical file, with names that match existing ones (fun_sum; regret_congr alongside dynRegret_congr). There are no definitions, no exposed bodies, no compatibility surface and no missing annotations.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: hypotheses are all used (σ ≥ 0 and μ ≥ 0 are needed for g t to be a subgradient of the quadratized losses; lam > 0 is inherited from the stability lemma), moduli may be negative where the math allows, and every special case (FTRL-Proximal, quadratized FTL, guessing game, norm_sq_div_two) is derived from one general theorem. No generality issues found.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration sits in its natural home: generic convexity lemmas in Analysis/Convex, regret_congr in Regret.lean, normed-space FTRL/FTL bounds in FTRL/Stability.lean, and inner-product material in a new file within the existing FTRL/ directory. The new file's three imports are each used (strongConvexOn_div_two_mul_norm_sub_sq, Real.sum_range_inv_add_one_le, regret_le_ftl_of_strongConvexOn).
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard terminology and match adjacent precedents (dynRegret_congr, isMirrorDescentStep_norm_sq_div_two_iff, Mathlib's fun_sum suffix for expanded sums); StrongConvexOn.fun_sum sits correctly in the Mathlib type's namespace. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both earlier documentation findings are fixed: the Stability module docstring now states the per-loss μ t-strong convexity and positive partial-sum hypotheses, and the References entry cites Lemma 7.1. Every new module and public declaration has a docstring that matches its statement.
✅	proof-quality	approved	claude/claude-opus-5-5	The duplicated padding argument is gone: FTRL-Proximal now reduces to regret_le_ftl_of_strongConvexOn, which holds the only copy, and with one caller it reasonably stays inline. The other proofs are short, commented, use robust automation, and do not rely on undocumented definitional equality.

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

_{Reviewing this diff at head 78c1a70. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.48.}