[RemyDegenne]

This PR adds the full-information part of [LS, Theorem 28.11] (adversarial linear bandits on the unit ball): the potential unitBallPotential a = -log (1 - ‖a‖) - ‖a‖ of [LS, Section 28.4] on a real inner product space, its derivative (1 - ‖a‖)⁻¹ • innerSL ℝ a on the open unit ball (including at 0), its nonnegativity and the diameter bound -log (1 - r) on the closed ball of radius r < 1, and the regret bound for FTRL with this potential on a convex subset of that ball:
∑ t < n, y t (a t - u) ≤ -log (1 - r) / η + η / 2 * ∑ t < n, (1 - ‖a t‖) * ‖y t‖ ^ 2 (ftrl_regret_le_unitBallPotential), plus existence of the plays in a proper space (the "well defined" clause of Theorem 28.11).

The key step is norm_sub_sq_div_le_bregDiv_unitBallPotential: ‖b - a‖ ^ 2 / (2 (1 - ‖a‖)) ≤ D_F(b, a) for all a, b in the open ball. It follows from splitting the divergence into the divergence of the radial profile φ s = -log (1 - s) - s plus (‖b - a‖² - (‖b‖ - ‖a‖)²) / (2 (1 - ‖a‖)), and a one-variable monotonicity argument for φ. This replaces the book's route (Hessian at a point Z_t of the segment, Theorem 26.13, and the stability estimate (1 - ‖Z_t‖) ≤ 2 (1 - ‖Ā_t‖) derived from the closed form (28.13)). So the bound holds for all losses, with no condition η ‖Ŷ_t‖ ≤ 1/2, and it saves a factor 2 in the stability term. The losses are continuous linear functionals with their operator norm, as in ftrl_regret_le_of_strongConvexOn, so the bound plugs directly into ftrl_integral_regret_le from Bandits/StochasticMirrorDescent.lean.

Milestone: Bandits Layer 10.2, [LS, Theorem 28.11] (unit ball, ‖y_t‖ ≤ 1, r = 1 - 2ηd, η = √(log n / (3dn)), R_n ≤ 2√(3nd log n)). Layer 10.2's first half, Theorem 28.10, landed in #147. What remains after this PR: define the sampling rule (exploration with probability 1 - ‖Ā_t‖ along U_t uniform on {±e_i}) and the estimator (28.12), prove that they make each round an IsUnbiasedRound with E[(1 - ‖Ā_t‖) ‖Ŷ_t‖²] ≤ d ‖y_t‖², and combine them with this bound through ftrl_integral_regret_le and the tuning of r and η.

New file: LMLExplore/OnlineLearning/UnitBallPotential.lean (289 lines). Nothing is vendored. The development follows [LS, Section 28.4], which the file cites.

Roadmap: Bandits

🤖 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	The derivative, nonnegativity and diameter bounds, the Bregman lower bound ‖b−a‖²/(2(1−‖a‖)) (checked via the exact radial-plus-angular identity and the sign of g'), the variable-modulus stability lemma, and the FTRL regret and existence theorems all state the intended mathematics under appropriate hypotheses. I tried to break each new statement and could not.
✅	reuse	approved	claude/claude-opus-5-5	The prior finding is resolved: the unit-ball stability sum now calls sum_apply_sub_sub_bregDiv_le_of_mul_norm_sq_le, and the square completion is factored into apply_sub_sub_div_le_of_mul_norm_sq_le, which both callers share. No Mathlib or LMLExplore declaration replaces the new potential, its derivative, or the Bregman lower bound.
✅	scope	approved	claude/claude-opus-5-5	New material proves the full-information half of [LS, Theorem 28.11], the named Bandits Layer 10.2 target (README.md:470-472), and feeds the merged ftrl_integral_regret_le; the description states the remaining steps. The FTRL.lean change pulls out the per-round stability step that the new file needs and lets its modulus vary, so the PR is one coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The new file credits its central informal source [LS, Section 28.4, Theorem 28.11] in the module docstring, the main docstrings and a References entry, and says where its proof departs from the book's route. No formal material is vendored, the only formal material drawn on is the project's own FTRL lemmas, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The surface is minimal: unitBallPotential keeps its body hidden behind a (rfl) _def lemma, and its characteristic API (derivative, continuity, nonnegativity, diameter bound, divergence lower bound, stability and regret bounds, existence of plays) is complete. The new general stability lemmas are public in FTRL.lean, the only private helper is specific to this potential's one-variable profile, and there is no compatibility layer.
✅	generality	approved	claude/claude-opus-5-5	The earlier duplication is fixed: the unit-ball stability sum now uses the general variable-modulus lemma sum_apply_sub_sub_bregDiv_le_of_mul_norm_sq_le, and the constant-modulus version is derived from it. All statements sit at the natural level with no unused or too-strong assumptions.
✅	placement	approved	claude/claude-opus-5-5	UnitBallPotential.lean belongs in OnlineLearning/ next to the other potential-specific files, and the two new general stability lemmas sit in FTRL.lean just before the strong-convexity lemma that now uses them. Both new imports (Log.Deriv for the log derivative, Sqrt for HasFDerivAt.sqrt) are used and specific.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard terms, consistent with the adjacent ftrl_regret_le_of_negEntropy/_of_strongConvexOn, exists_ftrl and apply_sub_sub_bregDiv_div_le_of_bregDiv_eq; every _le name proves a ≤ statement. The PR adds no notation and no namespace problems.
✅	documentation	approved	claude/claude-opus-5-5	The new module docstring, the FTRL.lean docstring update and every new public declaration are documented accurately and mathematically, with no overclaiming and no roadmap or process content. The cross-reference to ftrl_integral_regret_le and the Hessian remark both check out.
✅	proof-quality	approved	claude/claude-opus-5-5	The square-completion step is factored into apply_sub_sub_div_le_of_mul_norm_sq_le and reused by both stability theorems, and the algebra goes through field_simp/ring/linarith. No change/show, no undocumented defeq, and no proof over 50 lines; the two longest have comments on their structure.

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

_{Reviewing this diff at head d6cb3de. rubrics @ 32ce206. CLI @ 32ce206. Review spend: $8.35.}