[RemyDegenne]

Adds LMLRoadmaps/Refactors/, a roadmap of refactors of merged LMLExplore code. It restates existing developments in the generality that the later layers of the Bandits and Identification roadmaps build on, and moves them to the topic where their users are. Each target is a refactor that keeps every result it replaces. Workers in auto mode pick this area like any other. The README tells them to do a Layer 0 target before any item it unblocks.

Layer 0: generalizations that later layers build on

1. FTRL on normed spaces, with losses in the dual E →L[ℝ] ℝ. [LS, Corollary 28.8] then holds for every norm, so exponential weights ([LS, Proposition 28.7]) becomes the case PiLp 1. Unblocks Bandits 6.3, 6.4, 7 and 10.
2. Exponential families with a sufficient statistic T on any measurable space: ρ.expFamily T η = ρ.tilted (fun x ↦ η * T x), with natExpFamily and its siblings renamed. Unblocks Identification 1.2 (instances), 3.4, 4.2 and 5.
3. Chernoff bounds for variables whose mgf is dominated by an exponential-family member. The exact-law bounds and the [0, 1]/klBerReal bounds become corollaries, through the Bernoulli family, leaving one Chernoff proof instead of two. Unblocks Bandits 3.2 and Identification 4.2.
4. The run-to-stream transfer moves from Bandits/ to SequentialLearning/, and gains a version for events about all arms at once. Unblocks Identification 4 and 7.

Layer 1: consolidation. Wald's identities in one file; weight policies stated with simplex; the general sub-Gaussian lemmas move out of Bandits/Concentration.lean.

Suggested.lean compiles against the pinned dependencies (5 admitted statements: the normed-space FTRL bounds, the two dominated Chernoff bounds, the joint transfer). It spells out the exponential-family notions through Mathlib's tilted, cgf and klDiv, because the pin does not include current LMLExplore.

Companion PRs, needed to keep the roadmaps consistent: the Bandits Layer 6 amendment (normed spaces, losses in the dual) and the Identification Layer 1.2 amendment (exponential families with a statistic). Each roadmap PR touches only its own directory.

Not included, because no roadmap item uses them yet: general V₀ regularization for least squares, per-arm Gaussian variances, a general upper confidence level for any divergence, and change of measure for non-stationary environments.

Drafted with Claude Opus 5.5 at the request of the code owner, from a concept-level generality review of LMLExplore.

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1