[RemyDegenne]

This PR proves the FTRL equality [Ora, Lemma 7.1] for arbitrary losses, regularizers and points on an arbitrary type, together with the consequences that OnlineLearning Layer 0.3 asks for, and re-derives LMLExplore's sum_apply_sub_le_ftrl from it.

Roadmap: OnlineLearning

Milestone: OnlineLearning Layer 0, item 3 ("The FTRL equality" [Ora, Lemma 7.1, Remarks 7.3–7.4, Lemma 1.2]). The structure-free results are in the new module LMLExplore/OnlineLearning/FTRL/Equality.lean (namespace LMLExplore.OnlineLearning), which imports only OnlineLearning.Regret and Order.Filter.Extr. They are stated on the regret of OnlineLearning/Regret.lean (Layer 0.1, #281):

• regret_eq_ftrl ψ ℓ x z u n: with F t = ψ t + ∑ s < t, ℓ s, the regret of z against u equals ψ n u - ψ 0 (x 0) + ∑ t < n, (F t (x t) - F (t+1) (x (t+1)) + ℓ t (z t)) + (F n (x n) - F n u). Taking z = x gives Lemma 7.1. Taking any other z gives Remark 7.4, where the losses of other points stand on both sides.
• regret_le_ftrl: the inequality form, which holds when F n (x n) ≤ F n u.
• Remark 7.3 (adding a constant to the regularizer changes no play) is the general isMinOn_add_const_iff (with its filter form isMinFilter_add_const_iff), in the new LMLExplore/Order/Filter/Extr.lean, for any [Add β] [Preorder β] [AddRightMono β] [AddRightReflectLE β]. The Equality module doc explains how it applies to FTRL.
• sum_le_of_isMinOn_sum: the be-the-leader lemma [Ora, Lemma 1.2, Remark 15.32], on a set V, deduced from regret_le_ftrl with no regularizer.
• regret_le_sum_sub_of_isMinOn_sum: the roadmap's completion check. The regret of follow-the-leader is at most ∑ t < n, (ℓ t (x t) - ℓ t (x (t+1))) [Ora, proof of Theorem 1.3].
• sum_apply_sub_le_ftrl keeps its statement, but is now proved as the linear-loss case of regret_le_ftrl, as the roadmap's "derive it from this item" asks. No declaration is removed or renamed.

Module moved (no forwarding module): LMLExplore.OnlineLearning.FTRL → LMLExplore.OnlineLearning.FTRL.Basic, which imports FTRL.Equality. All declarations in it keep their names. MirrorDescent, Simplex and UnitBallPotential now import FTRL.Basic, and the docstrings that cited the module are updated.

After this PR, Layer 0 lacks only item 2, the online learners. Layer 5's derivative-free stability lemma (ftrl_stability_le) will sum its one-round bounds through regret_eq_ftrl.

The citations were checked against the text of [Ora] arXiv v10 (Lemma 1.2, Lemma 7.1, Remarks 7.3, 7.4 and 15.32). No Mathlib material is vendored. LML and Tau Ceti were searched for an existing FTRL equality or be-the-leader lemma, and neither has one.

🤖 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.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	All new statements are correct: the FTRL equality telescopes to regret ℓ z u n for arbitrary ψ, ℓ, x, z, u, and the inequality, be-the-leader, follow-the-leader and constant-shift statements match [Ora, Lemma 7.1, Remarks 7.3–7.4, Lemma 1.2, proof of Thm 1.3] with the needed membership hypotheses. sum_apply_sub_le_ftrl keeps its statement.
✅	reuse	approved	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration states the FTRL equality, be-the-leader, the follow-the-leader regret bound or the constant-shift invariance of minimizers (grep of Mathlib for an add-const/shift form of IsMinOn/IsMinFilter finds nothing). The PR reuses regret_eq_sum_sub_sum, regret_eq_sum_apply_sub, sum_range_sub' and isMinOn_iff, and re-derives sum_apply_sub_le_ftrl from regret_le_ftrl instead of keeping a duplicate telescoping proof.
✅	scope	approved	claude/claude-opus-5-5	The PR delivers OnlineLearning Layer 0 item 3 in full (the equality, the inequality, Remarks 7.3–7.4, be-the-leader and the follow-the-leader completion check) and re-derives sum_apply_sub_le_ftrl from it, as roadmap README lines 275–291 require. The Order/Filter/Extr.lean helper (Remark 7.3) and the FTRL → FTRL/Basic move are part of that same topic.
✅	attribution	approved	claude/claude-opus-5-5	Every new declaration cites the Orabona result it follows (Lemma 1.2, Lemma 7.1, Remarks 7.3/7.4/15.32, proof of Theorem 1.3), and both FTRL modules list [Ora] in their References and credit the LMLPapers telescoping adaptation. Nothing is vendored, the Extr lemmas are routine, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds only theorems: the FTRL equality and inequality, be-the-leader, the follow-the-leader regret bound, and the general constant-shift lemmas for minima, which are public in their own home LMLExplore/Order/Filter/Extr.lean. The move from FTRL to FTRL.Basic leaves no forwarding module or alias, and the old path is gone from the code.
✅	generality	approved	claude/claude-opus-5-5	The FTRL equality is stated once on an arbitrary type with ℝ-valued losses, which matches the existing regret. The inequality, be-the-leader, follow-the-leader and linear-loss results are all derived from it, and the constant-shift lemma uses standard typeclasses with no Mathlib duplicate.
✅	placement	approved	claude/claude-opus-5-5	The structure-free FTRL equality, be-the-leader and follow-the-leader results live in OnlineLearning/FTRL/Equality.lean, next to the moved FTRL/Basic.lean, and the generic add-const minimum lemmas live at the Mathlib-mirroring Order/Filter/Extr.lean. The module move updates every in-repo reference with no forwarding module, and no import is unused or overly broad.
✅	naming	approved	claude/claude-opus-5-5	New names (regret_eq_ftrl, regret_le_ftrl, sum_le_of_isMinOn_sum, regret_le_sum_sub_of_isMinOn_sum, isMinOn_add_const_iff, isMinFilter_add_const_iff) describe their conclusions, match adjacent sum_apply_sub_le_ftrl/regret_eq_sum_sub_sum conventions and Mathlib's *_add_const_iff pattern, and are no stronger than their statements; no notation is introduced and no Mathlib name collides (grep for isMinOn_add_const|isMinFilter_add_const|IsMinOn.add_const in ./mathlib/Mathlib found nothing).
✅	documentation	approved	claude/claude-opus-5-5	The new module docstrings and theorem docstrings in FTRL/Equality.lean and Order/Filter/Extr.lean match their statements, and the Implementation notes in FTRL/Basic.lean now correctly restrict this file to linear losses on a subset of a normed space. No stale references to the old module name LMLExplore.OnlineLearning.FTRL remain.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and robust (telescoping closed by ring/linarith, single simp only/rw steps), with no change/show; the only definitional unfolding is IsMinOn to IsMinFilter on the principal filter, which is how IsMinOn is defined. The index shift in the be-the-leader proof is explained in comments, and sum_apply_sub_le_ftrl is now a clean specialization of regret_le_ftrl.

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

_{Reviewing this diff at head 0d50ce1. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.70.}