[RemyDegenne]

This PR completes OnlineLearning Layer 7.2, Optimistic FTRL [Ora, Algorithm 7.8, Theorems 7.47 and 7.48, Lemma 7.49]. It covers the regret of FTRL with hint losses, the stability of minimizers of a strongly convex function under linear perturbations, and the improved bound for linear losses that this stability gives. The prerequisites are Layer 0.3 (regret_le_ftrl) and Layer 5.1 (the strong-convexity stability argument), both on main.

Roadmap: OnlineLearning

New file OnlineLearning/FTRL/Optimistic.lean (normed space E, subgradients within V as in LML's HasSubgradientWithinAt, plays taken as IsMinOn hypotheses as in the other FTRL theorems):

• optimistic_ftrl_stability_le_of_strongConvexOn handles one round. Suppose x t minimizes F t + p over V, where F t = ψ t + ∑ s < t, ℓ s and p is the hint, and g is a subgradient of the prediction error ℓ t - p. Then g is a subgradient of F t + ℓ t, and strong convexity of F t + ℓ t bounds the stability term by g (x t - z) - lam/2 ‖x t - z‖² + ψ t z - ψ (t+1) z. The hint p = 0 gives back ftrl_stability_le_of_strongConvexOn.
• regret_le_optimistic_ftrl_of_strongConvexOn is Theorem 7.47's first inequality, in the roadmap's exact form: ψ (n - 1) u - ψ 0 (x 0) + ∑ t < n, (g t (x t - x (t+1)) - lam t/2 ‖x t - x (t+1)‖²) + ∑ t < n - 1, (ψ t (x (t+1)) - ψ (t+1) (x (t+1))). Here x n only has to do at least as well as u on ψ (n - 1) + ∑ s < n, ℓ s, which is the hint-free last objective (ℓ̃_n = 0). The proof applies regret_le_ftrl to the regularizers ψ (min t (n - 1)), which repeat the last one, and does not telescope the hints. That is why the book's misplaced last hint plays no role. Neither the losses nor the hints need to be convex.
• regret_le_optimistic_ftrl_norm_sq_div_of_strongConvexOn is the second inequality, with ‖g t‖² / (2 lam t). It needs no last point: the first inequality is applied with Function.update x n u. It assumes 0 < n, because at n = 0 it would claim ψ 0 (x 0) ≤ ψ 0 u.
• sum_apply_sub_le_optimistic_ftrl is Theorem 7.48, for linear losses g t and hints p t, regularizers that are lam t-strongly convex and nondecreasing on V, c ≤ ψ 0 on V, and auxiliary hints q t with given auxiliary plays. The bound is ∑ g t (x t - u) ≤ ψ (n - 1) u - c + ∑ (‖g t - q t‖²/(2 lam t) + ‖g t‖ ‖p t - q t‖ / lam t). The book's min_V ψ_1 becomes any lower bound c.
• sum_apply_sub_le_optimistic_ftrl_of_isClosed gives the same bound for all q, in finite dimension, on a closed V, with lower semicontinuous ψ t. The auxiliary plays come from StrongConvexOn.exists_isMinOn_add_continuousLinearMap (Layer 1.1). With q = g this is the bound that the delayed-feedback reduction (7.3) uses.

In Analysis/Convex/Strong.lean:

• StrongConvexOn.mul_norm_sub_le_norm_sub_of_isMinOn_add is Lemma 7.49: minimizers x, y of f + θ₁ and f + θ₂, for an m-strongly convex f, satisfy m * ‖x - y‖ ≤ ‖θ₁ - θ₂‖. It is stated in multiplied form so that it needs no sign condition on m. It is proved from add_mul_norm_sub_sq_le_of_isMinOn.

Reuse: no stability-under-perturbation lemma for minimizers of strongly convex functions exists in Mathlib, Tau Ceti, LML or Statlib. I searched every StrongConvexOn file that also mentions IsMinOn, and Tau Ceti's Analysis/Convex/Strong.lean. No optimistic FTRL exists in LMLExplore (grep -i optimistic). The proofs reuse regret_le_ftrl, regret_congr, HasSubgradientWithinAt.fun_add_isMinOn, StrongConvexOn.add_add_le_of_hasSubgradientWithinAt, apply_sub_sub_mul_norm_sq_le, hasSubgradientWithinAt_linear and exists_isMinOn_add_continuousLinearMap. The closed form of the plays in Example 7.50 (a projection of -(g̃_t + ∑ g_s)/c) is already the case of a single quadratic in isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff, so it is not restated.

Supporting helpers, and the migration of existing code to them (in scope as part of this PR, because the reuse review asked that every inline copy go through the new helper, rather than restating it):

• New module Analysis/Normed/Operator/Basic.lean with ContinuousLinearMap.apply_le_opNorm_mul_norm, f x ≤ ‖f‖ * ‖x‖ for f : E →L[ℝ] ℝ. Lemma 7.49 and the Theorem 7.48 proofs use it. The four existing inline copies of this bound ((le_abs_self _).trans (f.le_opNorm _) or (Real.le_norm_self _).trans (f.le_opNorm _)) now use it as well, as one-line proof rewrites with an added import and no change to any statement:
  • Analysis/Convex/Coercive.lean, in fenchelConjugate_le_of_norm_sub_le;
  • Analysis/Convex/Conjugate.lean, in the private exists_pos_apply_sub_sub_bregDiv_le;
  • Analysis/Convex/Strong.lean, in apply_sub_sub_div_le_of_mul_norm_sq_le;
  • Bandits/UnitBallFTRL.lean, in the private integral_sum_apply_smul_sub_le.
• StrongConvexOn.add_continuousLinearMap (in Analysis/Convex/Strong.lean): adding a continuous linear map keeps m-strong convexity. Lemma 7.49 uses it, and the proof of the existing StrongConvexOn.exists_isMinOn_add_continuousLinearMap now uses it instead of the inline add_convexOn (by simpa using L.toLinearMap.convexOn hf.1).

No public declaration is removed or renamed.

What remains: Layer 7.2 is complete. The remaining items of Layer 7 are 7.3 (delayed feedback, which uses sum_apply_sub_le_optimistic_ftrl_of_isClosed with q = g), 7.4 (variance and gradual-variation bounds, from the second inequality of Theorem 7.47) and 7.1 (optimistic mirror descent).

Local checks only (CI verifies the pushed PR): scope: scoped: against 3af64fae786dd9a2aa021aa47b8e4305858822ed. local-axioms: checked 2 changed module(s), 35 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 (checked 2 changed module(s), 35 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	Lemma 7.49, the one-round optimistic stability bound, both inequalities of Theorem 7.47 and Theorem 7.48 (with given and with constructed auxiliary plays) are stated faithfully, with correct edge cases at n = 0 and m ≤ 0. No content is moved into hypotheses and nothing is vacuous.
✅	reuse	approved	claude/claude-opus-5-5	All four inline copies of the operator-norm bound now go through ContinuousLinearMap.apply_le_opNorm_mul_norm, which fixes the earlier finding. Lemma 7.49 and the optimistic FTRL theorems are new and reuse the existing FTRL stability, regret and existence API.
✅	scope	approved	claude/claude-opus-5-5	The new optimistic FTRL material is OnlineLearning Layer 7.2 (Theorems 7.47 and 7.48, Lemma 7.49), as stated at roadmap OnlineLearning/README.md:625-635. The two new helpers are used by the new proofs, and moving their existing inline copies onto them is part of the same topic, now disclosed in the description.
✅	attribution	approved	claude/claude-opus-5-5	Both new mathematical files credit Orabona (Algorithm 7.8, Theorems 7.47–7.48, Lemma 7.49) at the declarations and in References, and note where the proof departs from the book; the roadmap is credited only in the PR description. The new operator-norm helper is routine and needs no attribution.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is Lemma 7.49, the general StrongConvexOn.add_continuousLinearMap and ContinuousLinearMap.apply_le_opNorm_mul_norm (neither duplicated in Mathlib or the repo, and every in-repo use migrated), and the four optimistic FTRL theorems. It is minimal, exposes no bodies, defines nothing new, and has no compatibility layer.
✅	generality	approved	claude/claude-opus-5-5	Lemma 7.49 and Theorems 7.47/7.48 are stated at the natural level with no unused or too-strong hypotheses, and the new helpers apply_le_opNorm_mul_norm and StrongConvexOn.add_continuousLinearMap have no Mathlib equivalent and replace every former inline use.
✅	placement	approved	claude/claude-opus-5-5	Lemma 7.49 and add_continuousLinearMap sit in the generic strong-convexity file next to the lemmas they build on, the operator-norm helper gets a Mathlib-mirroring home in Analysis/Normed/Operator/Basic.lean that its five users import, and optimistic FTRL joins the existing OnlineLearning/FTRL/ directory with the minimal import FTRL.Stability.
✅	naming	approved	claude/claude-opus-5-5	New names follow the adjacent FTRL conventions (ftrl_stability_le_*, regret_le_ftrl*, sum_apply_sub_le_ftrl) and describe their conclusions without overstating them; StrongConvexOn.mul_norm_sub_le_norm_sub_of_isMinOn_add, StrongConvexOn.add_continuousLinearMap and ContinuousLinearMap.apply_le_opNorm_mul_norm are correctly dot-namespaced, read as their conclusions, and match no existing declaration name in ./mathlib. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Module and declaration docstrings in Optimistic.lean, Strong.lean and the new Operator/Basic.lean match their statements, and the earlier q = p overclaims are fixed. No process or roadmap narrative appears in the module docstrings.
✅	proof-quality	approved	claude/claude-opus-5-5	Shared reasoning is factored into StrongConvexOn.add_continuousLinearMap and ContinuousLinearMap.apply_le_opNorm_mul_norm, and no unmigrated copy of the old operator-norm chain remains in the repository. The new proofs are short, commented and use no change/show or brittle rewrite chains.

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

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