[RemyDegenne]

This PR completes OnlineLearning Layer 5.4, Composite losses [Ora, §7.8, Example 7.24]. With it, every item of Layer 5 (FTRL for convex losses) is on main. Bullet 1 is FTRL with a fixed known part r of the losses kept exact. Bullets 2–3 cover the proximal steps that compute such plays, read through Tau Ceti's moreauYosidaResolvent, and soft thresholding for the ℓ¹ penalty. It is one topic: the algorithm, its regret, and the closed form of its plays.

Roadmap: OnlineLearning

New file OnlineLearning/FTRL/Composite.lean (bullet 1, normed space, subgradients within V as in LML's HasSubgradientWithinAt):

• regret_le_ftrl_composite_of_strongConvexOn. Each play x t minimizes over V the objective ψ t + (t + 1) * r + ∑ s < t, ℓ s, which anticipates the current round's r (the book's λ t ‖x‖₁ at book round t is Lean round t - 1). g t is a subgradient of ℓ t alone, and ψ t + (t + 1) * r + ∑ s ≤ t, ℓ s is lam t-strongly convex. If x n does at least as well as u on the non-anticipating last objective ψ n + n * r + ∑ s < n, ℓ s, then regret (ℓ + r) ≤ ψ n u - ψ 0 (x 0) + ∑ ‖g t‖² / (2 lam t) + ∑ (ψ t (x (t+1)) - ψ (t+1) (x (t+1))). This is the bound of item 2 (regret_le_ftrl_of_strongConvexOn) for the composite losses. r is never differentiated and need not be convex, and r = 0 gives back regret_le_ftrl_of_strongConvexOn. The proof is the FTRL equality regret_le_ftrl for the non-anticipating objectives plus ftrl_stability_le_norm_sq_div_of_strongConvexOn for the anticipating regularizers ψ t + (t + 1) * r. The r terms then cancel exactly, which is how [Ora] avoids the boundary term by "setting ψ_{T+1} = ψ_T".
• regret_le_ftrl_linearized_composite_of_strongConvexOn. This is the roadmap's form, "FTRL on ∑ s < t, g s + t r + ψ t": the plays minimize ψ t + (t + 1) * r + ∑ s < t, g s, where g s are subgradients of convex losses f s. If ψ t + (t + 1) * r is lam t-strongly convex, the same bound holds for f t + r. It is derived from the previous theorem and the linearization lemma sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt.
• isMinOn_norm_sq_div_add_mul_sum_abs_add_inner_iff [Ora, Example 7.24]. On EuclideanSpace ℝ α, the unique minimizer of ‖x‖² / (2η) + c ∑ |x a| + ⟪θ, x⟫ has coordinates η * softThreshold c (-θ a). These are the unconstrained plays of the linearized composite FTRL with ψ t = ‖·‖² / (2 η t) and r = lam ‖·‖₁, so they are sparse.

New file Analysis/Convex/Proximal.lean (bullets 2 and 3):

• mem_moreauYosidaResolvent_ite_iff. Restrict r : E → ℝ to a nonempty V with Tau Ceti's convention if x ∈ V then (r x : EReal) else ⊤ (TauCeti.mem_subdifferential_ite_iff, EffectiveDomain.lean). For η > 0 its resolvent J_η z is {y ∈ V | IsMinOn (η * r + ‖· - z‖² / 2) V y}. mem_moreauYosidaResolvent_coe_iff is the unconstrained case: the proximal step is the minimizer of η r(x) + ½‖x − z‖².
• mem_moreauYosidaResolvent_ite_zero_iff. For the indicator of a nonempty K, the resolvent is the set of points of K nearest to z. This is the projection convention of isMirrorDescentStep_norm_sq_div_two_iff. exists_moreauYosidaResolvent_ite_zero_eq_singleton adds that on a nonempty complete convex set of a real inner product space (e.g. closed convex in a Hilbert space) the resolvent is a single point.
• softThreshold c z = Real.sign z * max (|z| - c) 0 (the book's formula), with softThreshold_def, _of_abs_le, _of_lt, _of_lt_neg, _neg and _mul (positive homogeneity). mul_abs_softThreshold_add_le shows it minimizes c |x| + (x − z)² / 2 with quadratic growth. isMinOn_mul_sum_abs_add_norm_sub_sq_iff and moreauYosidaResolvent_mul_sum_abs show that the proximal step of lam ∑ |x a| on EuclideanSpace ℝ α (that is, PiLp 2, so that ‖x − z‖ is Euclidean, as the roadmap's coordinate convention allows) is the single point given by coordinatewise soft thresholding at level η * lam.

Reuse:

• softThreshold, proximal/projection characterizations of moreauYosidaResolvent: no hits in Mathlib, Tau Ceti, LML, Statlib or LMLExplore (searched threshold, shrink, prox, proximal, and every moreauYosidaResolvent lemma outside MoreauYosida/Basic.lean). The proofs use Tau Ceti's mem_moreauYosidaResolvent_iff_isMinOn and coe_edist_sq_div_eq_coe_dist_sq_div.
• Projection: existence comes from Mathlib's exists_norm_eq_iInf_of_complete_convex. Uniqueness comes from strongConvexOn_div_two_mul_norm_sub_sq and StrictConvexOn.eq_of_isMinOn. Tau Ceti's PenalizedConvex.subsingleton_moreauYosidaResolvent would first need penalized convexity of the indicator along CAT(0) geodesics, which is longer than this two-line argument.
• The new Tau Ceti import TauCeti.Analysis.GradientFlow.MoreauYosida.Basic is light: it and its four new dependencies build in about 4 s.

No public declaration is removed or renamed.

What remains: Layer 5 is complete. The next consumers are Layer 7.2 (optimistic FTRL, from Layers 0.3 and 5.1) and Layer 13.5, which uses the kept regularizer increments of item 2.

Local checks only (CI verifies the pushed PR): scope: scoped: against 278c9ec81caf4b9f07ee007af57df29ce0d0151b. local-axioms: checked 2 changed module(s), 26 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), 26 declarations; 1 documentation checks; 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 composite and linearized-composite FTRL bounds are correct: the r terms cancel exactly in the per-round stability, and the (t+1) r indexing matches Ora §7.8 and the roadmap. The proximal, projection and soft-thresholding characterizations agree with Example 7.24, and all assumptions they need are present.
✅	reuse	approved	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration covers soft thresholding, the proximal or projection characterizations of the resolvent, or the composite FTRL bounds; the proofs reuse the existing FTRL equality, stability and linearization lemmas, Mathlib's convex projection existence and LMLExplore's strong convexity of the squared distance. Tau Ceti sources were not in the checkout, so a Tau Ceti resolvent duplicate could not be grepped.
✅	scope	approved	claude/claude-opus-5-5	The PR implements exactly the three bullets of OnlineLearning Layer 5.4 (composite-loss FTRL regret, proximal step and projection via moreauYosidaResolvent, and ℓ¹ soft thresholding) as one coherent topic. Using EuclideanSpace ℝ α (PiLp 2) instead of α → ℝ is permitted by the roadmap's coordinate convention (README.md:127-128).
✅	attribution	approved	claude/claude-opus-5-5	Both new modules cite Orabona [Ora, Section 7.8, Example 7.24] in their module docstrings and main theorem docstrings, in the repo's standard reference format, and the central formal dependencies (Tau Ceti's moreauYosidaResolvent API and the in-repo FTRL regret and stability lemmas) are named. No uncredited source was found.
✅	api-design	approved	claude/claude-opus-5-5	Both earlier findings are fixed: softThreshold_neg is now @[simp], and softThreshold_zero_right covers softThreshold c 0 = 0 for every c. The body of softThreshold stays hidden behind softThreshold_def := (rfl), the proximal, projection and composite-FTRL surface has no duplicates or compatibility leftovers, and the characteristic API is complete.
✅	generality	approved	claude/claude-opus-5-5	The statements sit at the natural level: each hypothesis is needed, and the special cases (unconstrained step, projection, ℓ¹ resolvent, linearized composite FTRL, closed-form plays) are derived from the general lemmas. The composite regret theorem cannot simply be derived from the existing regret_le_ftrl_of_strongConvexOn because of the boundary term, so it is not a duplicate.
✅	placement	approved	claude/claude-opus-5-5	Proximal.lean fits under Analysis/Convex/ and Composite.lean joins the existing FTRL/ directory, with its closed-form play lemma matching the precedent in FTRL/Quadratic.lean. Every import supplies something the code uses, and none is a broad import Mathlib.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, consistent with adjacent FTRL lemmas (regret_le_ftrl_of_strongConvexOn, regret_le_ftrl_proximal); every _iff is a genuine equivalence, _eq_singleton is an equality, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both new modules open with module docstrings stating their content and purpose, and every public definition and main theorem is documented accurately against its statement and hypotheses. No process or roadmap narrative appears in the files.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and use robust automation (simp, linarith, nlinarith, linear_combination, field_simp, gcongr), with reusable growth inequalities factored out and the composite bound built from the existing FTRL lemmas. The only definitional step (Iff.rfl across instance paths to the EuclideanSpace norm) is commented and benign.

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

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