[RemyDegenne]

This PR states the potential lemmas of exponential weights once, in OnlineLearning/ExponentialWeights.lean, and derives the anytime regret bound of exponential weights and AdaHedge's telescoping from them. This is Generalization 1.13 ("Anytime exponential weights"), second bullet: "OnlineLearning/AdaHedge.lean proves the same telescoping of the exponential-weights potential a second time (mixLoss, hedgePotential, mixLoss_softmax, hedgePotential_le_of_le and the private sum_adaHedgeMixLoss_le, already for decreasing rates). State these potential lemmas once, in OnlineLearning/ExponentialWeights.lean; the anytime bound and AdaHedge's regret bound both use them. The stability term of Bandits 6.4, $\langle p,y\rangle+\frac1\eta\log\sum_ap_ae^{-\eta y_a}$, is the mixability gap that mixLoss computes." The first bullet (the local-norm bound softmax_regret_le_of_antitone with softmax_regret_le as its constant case) was already on main.

Roadmap: Generalization

What changes:

• Moved, statements unchanged (AdaHedge.lean → ExponentialWeights.lean): mixLoss, mixLoss_def, mixLoss_le_sum_mul, le_mixLoss, hedgePotential, hedgePotential_def, hedgePotential_eq_mixLoss, mixLoss_softmax, hedgePotential_le, le_hedgePotential, hedgePotential_le_of_le. sum_mul_le_mixLoss_add (Hoeffding's lemma for the mix loss) stays in AdaHedge.lean, its only user, so that ExponentialWeights.lean does not import the sub-Gaussian theory.
• Moved, statements unchanged (Simplex.lean → ExponentialWeights.lean): softmax_regret_le_sum_exp_of_antitone, softmax_regret_le_of_antitone, softmax_regret_le_of_antitone_of_neg_one_le, softmax_regret_le, softmax_regret_le_of_neg_one_le. Their users (Exp3, Exp3-IX, Exp4, linear Exp3) import Simplex.lean, which imports ExponentialWeights.lean, so no import changes.
• New in ExponentialWeights.lean: mixLoss_eq_neg_log_div (the mix loss with the exponent in simp normal form), mixLoss_le_iff and le_mixLoss_iff (for 0 < η, comparing the mix loss with a constant c is comparing log ∑ a, w a * exp (-η * ℓ a) with -η * c; used by mixLoss_le_sum_mul, le_mixLoss and AdaHedge's sum_mul_le_mixLoss_add), hedgePotential_zero_right (@[simp]), hedgePotential_le_sum_mul (the potential is at most ⟨u, L⟩ + log k / η for every u in the simplex), sum_mul_sub_mixLoss_le (the mixability gap is at most (∑ p (exp (-(η y)) - 1 + η y)) / η, from log x ≤ x - 1), add_mixLoss_softmax_le_hedgePotential (one step of the telescoping), sum_mixLoss_softmax_le_of_antitone (with nonincreasing rates the total mix loss of exponential weights is at most hedgePotential (η (n - 1)) (∑ t < n, y t)), and softmax_regret_le_sum_sub_mixLoss_of_antitone (regret ≤ log k / η (n - 1) + the sum of the mixability gaps).
• Re-proved: softmax_regret_le_sum_exp_of_antitone now follows from softmax_regret_le_sum_sub_mixLoss_of_antitone and sum_mul_sub_mixLoss_le. Before, it went through FTRL with the negative entropy (ftrl_regret_succ_le_of_antitone). The four local-norm corollaries keep their proofs. In AdaHedge's private sum_adaHedgeMixLoss_le, the exponential-weights rounds now go through add_mixLoss_softmax_le_hedgePotential. The follow-the-leader rounds (infinite learning rate) keep their own argument, because no exponential weights are played there.
• Restated: isGreatest_sum_sub_mul_sub_sum_mul_log_div_div (Simplex.lean) now gives the maximum of the FTRL stability term as the mixability gap ∑ a, p a * y a - mixLoss η p y, which is the same value as before. sum_sub_mul_sub_sum_mul_log_div_div_le is re-proved through sum_mul_sub_mixLoss_le. Neither had a user outside Simplex.lean.
• No declaration is renamed or deleted. The unused import Mathlib.Analysis.MeanInequalitiesPow moves from AdaHedge.lean to ExponentialWeights.lean, where the power-mean step of hedgePotential_le_of_le now lives. Module docstrings of the four touched files are updated (including a stale cross-reference in ExponentiatedGradient.lean).

What remains: Generalization 1.13 is met once this lands. Target 1.14 (Exp4-IX with learning-rate sequences, after 1.12) can then use softmax_regret_le_sum_exp_of_antitone or the mixability-gap form, and OnlineLearning 10.1 can treat mixLoss and hedgePotential as the finite case of Gibbs mixtures in their new home.

Sources: the telescoping of the mix losses with decreasing learning rates is the argument of de Rooij, van Erven, Grünwald and Koolen, Follow the leader if you can, hedge if you must (JMLR 2014), Section 2, which AdaHedge.lean already cited. It is now cited in ExponentialWeights.lean too, along with [Ora, Section 7.5] and [BCB12]. No Mathlib material is vendored.

Local verification (tauceti-local-checks verify --policy ordinary, local checks, not CI): scope: scoped: against 3af64fae786dd9a2aa021aa47b8e4305858822ed; the whole-library lake build --iofail passed; local-axioms: checked 4 changed module(s), 144 declaration(s); 0 violation(s); module-system, header-style and local-lint (14 environment linters) 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	The new telescoping step, the total mix-loss bound, the regret bound through mixability gaps, the gap bound from log x ≤ x - 1, the potential bound at any u in the simplex, the potential at zero and the mixLoss_le_iff / le_mixLoss_iff pair state the intended results, including at n = 0 and for empty α. The restated isGreatest has the same value as before, and the moved declarations keep their statements.
✅	reuse	approved	claude/claude-opus-5-5	The potential lemmas are stated once in ExponentialWeights.lean and AdaHedge/Simplex now route through them; the new declarations (sum_mul_sub_mixLoss_le, the telescoping lemmas, hedgePotential_le_sum_mul, mixLoss_le_iff/le_mixLoss_iff) have no located counterpart in Mathlib or LMLExplore.
✅	scope	approved	claude/claude-opus-5-5	The PR carries out the second bullet of Generalization 1.13 (roadmap Generalization/README.md:490-495) as one refactor: it states the exponential-weights potential lemmas once in ExponentialWeights.lean, and AdaHedge and the anytime regret bounds both use them. The new lemmas are the telescoping and mixability-gap statements that bullet asks for, and nothing unrelated is bundled in.
✅	attribution	approved	claude/claude-opus-5-5	The telescoping and mixability-gap lemmas cite de Rooij–van Erven–Grünwald–Koolen (JMLR 2014, Section 2), and the moved regret bounds keep their Orabona, Bubeck–Cesa-Bianchi and Lattimore–Szepesvári citations, with matching reference entries in ExponentialWeights.lean, AdaHedge.lean and Simplex.lean. The roadmap is credited only in the PR description and no Mathlib material is vendored.
✅	api-design	approved	claude/claude-opus-5-5	The moved mix-loss and potential definitions keep unexposed bodies with (rfl) _def lemmas, and the new comparison lemmas mixLoss_le_iff/le_mixLoss_iff, the normal-form mixLoss_eq_neg_log_div and the @[simp] lemma hedgePotential_zero_right give enough API to use them without unfolding. No compatibility surface survives, and the remaining private helpers are local rewrites that the public iff lemmas already expose.
✅	generality	approved	claude/claude-opus-5-5	The mix-loss and potential lemmas now live once in ExponentialWeights.lean at the natural level, and the regret bounds, the FTRL stability bound and AdaHedge's step all come from them with no unused or over-strong hypotheses. AdaHedge keeps a separate argument only for its follow-the-leader rounds, where no exponential weights are played.
✅	placement	approved	claude/claude-opus-5-5	The potential, telescoping and regret lemmas of exponential weights now live in ExponentialWeights.lean, and Hoeffding's lemma for the mix loss stays with its only user, AdaHedge. MeanInequalitiesPow moved with hedgePotential_le_of_le, which uses it, and the remaining NegEntropy, PiLp and FTRL imports of Simplex.lean are still used.
✅	naming	approved	claude/claude-opus-5-5	New names (mixLoss_eq_neg_log_div, mixLoss_le_iff, le_mixLoss_iff, hedgePotential_zero_right, hedgePotential_le_sum_mul, sum_mul_sub_mixLoss_le, add_mixLoss_softmax_le_hedgePotential, sum_mixLoss_softmax_le_of_antitone, softmax_regret_le_sum_sub_mixLoss_of_antitone) describe their conclusions, match the strength of their statements (the _iff lemmas are Iffs, the eq lemma is an equality) and are consistent with adjacent mixLoss_le_sum_mul and softmax_regret_le*_of_antitone. Moved declarations keep their names, everything stays in LMLExplore.OnlineLearning, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The moved and new mix-loss, potential and regret declarations are documented accurately in ExponentialWeights.lean, and the module docstrings of AdaHedge, Simplex and ExponentiatedGradient match where the material now lives. A search found no stale cross-references to the old locations.
✅	proof-quality	approved	claude/claude-opus-5-5	The earlier rewrite-chain finding is fixed: sum_mul_le_mixLoss_add now goes through the public le_mixLoss_iff, so the helper content is stated once. The new telescoping proofs are short and factored into reusable lemmas, with no undocumented defeq or brittle chains.

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

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