[RemyDegenne]

This PR proves [LS, Theorem 28.11], the regret bound 2 √(3 n d log n) of follow the regularized leader with bandit feedback on the unit ball, against an adaptive adversary. It defines the ingredients of [LS, Algorithm 17] on a real inner product space with an orthonormal basis b : OrthonormalBasis ι ℝ E. The randomness of a round is an outcome in Option (ι × Bool), where none means the round does not explore and some (i, s) means it explores in direction b i or -b i. The new definitions are unitBallProb a (the law of the outcome: ‖a‖ for none, (1 - ‖a‖) / (2 d) for each direction), unitBallAction b a o (a / ‖a‖ when not exploring, ± b i when exploring) and unitBallEstimate b a y o, the estimate (28.12) d / (1 - ‖a‖) * y A * ⟪A, ·⟫, which uses only the observed loss y A.

It targets Bandits Layer 10.2 (mirror descent with bandit feedback): "prove [LS, Theorem 28.11] for the unit ball: with ‖y_t‖ ≤ 1, r = 1 - 2ηd and η = √(log(n)/(3dn)), R_n ≤ 2√(3nd log n). The exploration direction U_t is uniform on {±e_1,…,±e_d}". This builds on the Layer 6.5 interface IsUnbiasedRound / integral_sum_apply_sub_le_of_ae_le (#147, #159) and on the full-information bound ftrl_regret_le_of_unitBallPotential (#153).

Main results, in LMLExplore/Bandits/UnitBallFTRL.lean:

• sum_unitBallProb_smul_unitBallAction, sum_unitBallProb_smul_unitBallEstimate: the mean action is the play, and the estimate is unbiased.
• sum_unitBallProb_mul_one_sub_norm_mul_norm_unitBallEstimate_sq: the mean of (1 - ‖a‖) ‖Ŷ‖² is exactly d ‖y‖², through OrthonormalBasis.norm_dual.
• isUnbiasedRound_unitBall: let the play and the loss be m-measurable with ‖a‖ ≤ r < 1, and let the outcome have conditional law unitBallProb a given m. Then the round is an IsUnbiasedRound. integral_one_sub_norm_mul_norm_unitBallEstimate_sq gives the expected variance term d E‖y‖².
• ftrl_integral_regret_le_of_unitBallEstimate: for 0 ≤ r < 1 and η > 0, the expected regret against every u with ‖u‖ ≤ 1 is at most (1 - r) n - log (1 - r) / η + η d n / 2. The stability term is bounded at the base point, as in feat: FTRL on the unit ball with the potential -log(1 - ‖a‖) - ‖a‖ [LS, Section 28.4] #153, so the last term is half of [LS]'s.
• ftrl_integral_regret_le_two_mul_sqrt_of_unitBallEstimate: the book's tuning η = √(log n / (3 d n)), r = 1 - 2 η d gives ≤ 2 √(3 n d log n) for n ≥ 2. The book's statement fails for n = 1, where its bound is 0. The hypothesis 0 ≤ r is needed for the algorithm to be defined; when it fails, the bound exceeds the trivial 2n.

As in Bandits/StochasticMirrorDescent.lean, the interaction is stated round by round relative to σ-algebras m t. The adaptive adversary's loss y t is m t-measurable, and the plays are almost surely FTRL plays on the estimated losses. [LS]'s pseudocode omits the signs of the exploration direction; this PR uses ± b i as the README and the book's text require.

Two general lemmas get their own homes:

• LMLExplore/MeasureTheory/Function/ConditionalExpectation/FiniteValued.lean contains condExp_apply_ae_eq_sum_smul and integral_apply_eq_integral_sum_smul. For X finite-valued with conditional law q o = P⟦X = o | m⟧ and m-measurable g · o, they give P[g(X) | m] = ∑ o, q o • g · o. They also contain integrable_apply_of_measurableSet_preimage.
• LMLExplore/Analysis/InnerProductSpace/Dual.lean contains OrthonormalBasis.sum_apply_smul_innerSL: ∑ i, y (b i) • innerSL 𝕜 (b i) = y. It is the continuous form of Mathlib's Basis.sum_dual_apply_smul_coord, from which it is proved.

With this PR, Theorem 28.11 and Layer 10.2 are complete. Layer 10.1 (Exp3 with exploration, [LS, Theorem 27.1]) is what remains in Layer 10.

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 outcome law, action and estimate match [LS, Algorithm 17] and (28.12); I re-derived unbiasedness, the d‖y‖² variance identity and the 2√(3nd log n) tuning by hand. The hypotheses can be satisfied (exists_ftrl_unitBallPotential) and nothing is moved into assumptions; the extra conditions n ≥ 2, Nonempty ι and the derived 0 ≤ r only exclude degenerate cases.
✅	reuse	approved	claude/claude-opus-5-5	The new declarations (the unit-ball exploration law, action and estimate, the finite-outcome conditional expectation lemmas, and the continuous dual expansion in an orthonormal basis) have no counterpart in Mathlib or LMLExplore. The PR builds on IsUnbiasedRound, integral_sum_apply_sub_le_of_ae_le, ftrl_regret_le_of_unitBallPotential, OrthonormalBasis.norm_dual, Basis.sum_dual_apply_smul_coord, condExp_finsetSum and condExp_smul_of_aestronglyMeasurable_right instead of proving them again.
✅	scope	approved	claude/claude-opus-5-5	The PR proves [LS, Theorem 28.11] on the unit ball, which is exactly Bandits Layer 10.2 (README.md:717-722). The two general lemma files are prerequisites used directly by the main theorem, so the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	The central source [LS, Section 28.4: Algorithm 17, (28.12), Theorems 28.10/28.11] is cited in the module docstring and at each declaration following it, and OrthonormalBasis.sum_apply_smul_innerSL names the Mathlib lemma it derives from (Basis.sum_dual_apply_smul_coord, confirmed at Mathlib/LinearAlgebra/Dual/Basis.lean:112). The roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The new definitions hide their bodies and come with simp equation lemmas, bounds and closed-form mean lemmas, so they can be used without unfolding; the general lemmas are public in their own files and do not duplicate Mathlib. The private helpers are steps specific to this file's proof.
✅	generality	approved	claude/claude-opus-5-5	The statements are at the natural level: the dual-basis and finite-valued conditional-expectation lemmas are general (any RCLike field, any finite outcome type, Banach-valued g), and the tuned Theorem 28.11 is derived from the general (r, η) bound without duplicating its proof. I found no unused, over-strong or speculative hypotheses.
✅	placement	approved	claude/claude-opus-5-5	The bandit-specific material is in Bandits/UnitBallFTRL.lean next to StochasticMirrorDescent with no flat UnitBall* sibling, and the two general lemmas are in generic files mirroring Mathlib paths (Analysis/InnerProductSpace/Dual, MeasureTheory/Function/ConditionalExpectation/FiniteValued) with no roadmap-specific hypotheses. Every import is used and none is broad.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, follow the adjacent ftrl_integral_regret_le/mirrorDescent_integral_regret_le pattern, and do not overstate their statements; OrthonormalBasis.sum_apply_smul_innerSL is placed for dot notation and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The earlier finding is fixed: the module docstring now says the FTRL plays hold almost surely, matching the hftrl hypothesis. All three new files and their public declarations are documented accurately, without overclaiming or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	The redundant 0 ≤ r hypothesis has been removed; it is now derived from hftrl, so both earlier findings are fixed. The proofs use robust automation, the long main proof is split into commented phases, and nothing relies on undocumented definitional equality.

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

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