[RemyDegenne]

Adds LMLRoadmaps/Generalization/, a roadmap of refactors of merged LMLExplore code. It restates existing developments in the generality that the amended Identification (#10), Bandits (#11) and ReinforcementLearning (#12) roadmaps specify. Each target is one PR that restates one development and keeps every result. This is the same design as the completed Refactors roadmap (Completed/Refactors/). Contributor PRs carry Roadmap: Generalization.

Why. About fifty items of the three amended roadmaps say that a merged LMLExplore declaration becomes an instance or a corollary of a general form. Examples:

• baiTask with a mean functional;
• Wald's identity and the chain rule at a stopping time for any environment;
• GLR thresholds that read the history;
• Exp3, Exp3-IX and Exp4 as instances of Exp4-IX;
• dynamic programming without attainment;
• runReturn with a discount.

Workers will not do these restatements on their own. They pick the next unmet item, and skip any item that a merged PR already covers. Most amended items already have a merged narrow version, so they look done, and new work keeps building on the narrow code. As targets of a roadmap of their own, the restatements become visible and ordered. A worker choosing between a target and an item it unblocks takes the target first. The Conventions also say that a merged narrow version does not cover a target, and that adding a general version beside the narrow one does not meet it.

Contents (only LMLRoadmaps/Generalization/)

• Scope and relation to the other roadmaps.

  • The area roadmaps specify the mathematics. Each target points to the area item that specifies its general form and adds no item of those roadmaps.
  • Where a target needs unmerged general material, it lists that area item as a prerequisite. Examples: Identification 0.5 (phased elimination), 1.1 (IdentTask.comap, the model of all bandits) and 3.6 (Gaussian costs of half-spaces); ReinforcementLearning 0.6 and 8.1 (measurable ε-greedy policies).
  • A list of restatements the area roadmaps own. These are items whose general form is new mathematics, so the PR that builds the item derives the narrow code. Examples: klucb/ucbF from KL-UCB for exponential families (Bandits 3), gaussianTS (Bandits 5.1), the Gaussian GLR thresholds (Identification 4.2), backward induction and EpisodicMDP.value_le_optValue (ReinforcementLearning 8.2, 8.4).

• Layer 0, generalizations that new work builds on (16 targets):

  • Identification: best arm and ε-best arm identification with a mean functional; the other classical tasks, including sphereTask.
  • Sequential learning: Wald's identity for every environment; the event transfer for every event about the observations of each arm (real observations); the chain rule at a stopping time for any two algorithm–environment pairs.
  • GLR and Track-and-Stop: GLR thresholds β n h; plug-in GLR statistics and Track-and-Stop for any estimator; forced exploration in event form.
  • Bandits and online learning: pseudo-regret and random regret against any environment; importance-weighted estimators against any environment; FTRL with time-varying regularizers; designOp V₀.
  • Dynamic programming: abstract DP without attainment; PI/MPI assuming only the greedy decisions they use; Bellman operators for every action set; runReturn γ and one stateMarginal.

• Layer 1, consolidation (24 targets):

  • Identification: guarantees of LUCB, KL-LUCB, successive and median elimination on classes of bandits, so that the auxiliary family ν : (α → ℝ) → Kernel α ℝ disappears; successive rejects, median elimination and successive elimination through the phased-elimination constructor; transportation costs under per-arm divergence hypotheses, in three PRs; Gaussian costs with arm-dependent variances, in two PRs; one sample-complexity reduction for D- and C-tracking.
  • Bandits and online learning: Exp4-IX as the single algorithm; anytime exponential weights, with AdaHedge's duplicate telescoping merged; Exp4-IX with rate sequences; pseudo-regret and high-probability bounds against any environment; mirror descent with nonincreasing rates; the self-normalized bound with V₀; dInf for exponential families.
  • Dynamic programming: the resolvent as (1 − γκ)⁻¹; bellmanEvalOp through Kernel.integralCLM, with Blackwell's argument proved once; PI/MPI rates from the abstract lemmas; discounted optimality for countable actions; the simulation lemma with a reward error.

• Layer 2, material Tau Ceti provides (4 targets). LMLExplore's overlap scan covers Mathlib only, so these duplicates went unflagged:

  • tilts and generating functions of the Gaussian, Poisson and exponential laws (mgf_tilted_mul and others);
  • powers of kernels;
  • two elementary analysis lemmas;
  • real-valued total-variation and finite-Pinsker re-proofs.

• Completion checks and References.

• Suggested.lean: the restated signatures where the signature is the point:

  • baiTask ν mean, thresholdingTask ν mean γ, and the identity with comap;
  • IdentTask.glrt with thresholds (n : ℕ) → Hist Unit α 𝓨 n → ℝ≥0∞, and isDeltaPAC_glrt;
  • the plug-in cost that replaces empCost;
  • IsUniformSup with the restated DP lemmas (order-unit form);
  • exp4IX with exp3, exp3IX and exp4 as instances.

  General forms already suggested in the area files (Wald, event transfer, chain rule, pseudo-regret, time-varying FTRL, designOp V₀, runReturn γ, stateMarginal, IsApproxGreedy) are cited by name, not repeated.

Points to check

• Target 1.13 (anytime exponential weights). Bandits 6.4 says the bound follows "by item 3" (FTRL). The target asks instead for the exponential-weights potential lemmas of OnlineLearning/AdaHedge.lean to be stated once, in ExponentialWeights.lean, and for both bounds to use them. This removes the duplicate telescoping. The stability term of 6.4 is AdaHedge's mixability gap.
• Target 1.5 (per-arm divergences). It adds openness of the per-arm mean sets S a to the hypotheses of Identification 1.4 (continuity, zero exactly on the diagonal, monotone on each side), because the merged proofs use expFamilyMeans_mem_nhds.
• Target 1.21. It makes MDP.abs_bellman_sub_le a corollary of the boundedMeasurable contraction, as ReinforcementLearning 0.2 asks. The finite-action version for unbounded integrable v is lost; it has no users.
• Target 1.4. It replaces the index-policy construction of successive elimination by the phased algorithm of Identification 7.1. Its results are re-proved, not only restated.
• Target 0.4. It restates SumRewards.lean for real observations only. LML's hasLaw_rewardByCount_infinitePi is stated for real rewards, so observations in any 𝓨 stay with Identification 4.1. That item will restate the same statements once more, generalizing only the observation space.
• Target 0.3. It follows the merged proof of Wald's identity (conditional means on {t < τ}), not the "stopped martingale" proof that Identification 0.3 describes. Both are valid.
• Target 0.2. It renames Task/MeanVector.lean to Task/Classical.lean.
• Not included:
  • weightedMeasure and Tau Ceti's categoricalMeasure: not a duplicate (real vectors in simplex against StdSimplex); switching would be a design change.
  • The unused ContinuousLinearMap.leftInverse_ringInverse / rightInverse_ringInverse: more general than Tau Ceti's pointwise forms.
  • Gaussian special cases (integral_sub_sq_gaussianReal and others) that generalize Tau Ceti lemmas.
• The area roadmaps have stale names, to fix in a separate update:
  • LMLExplore's LML pin uses Environment.bandit, Environment.evalSeq and Environment.feedbackKernel; the area READMEs and Suggested.lean files use stationaryEnv, onlineEvalEnv and env.measure, from LMLRoadmaps' older pin.
  • Bandits Layer 6 and Identification 1.2 still say that the completed Refactors roadmap "restates" FTRL and exponential families; that work is merged.
  • The Bandits Suggested.lean exp4IX takes adv : 𝓞 → β → α → ℝ, which a weight-based policy cannot use. Here it is adv : 𝓞 → β → simplex α, as in the merged exp4.
• Open LMLExplore PRs:
  • #159 edits Bandits/StochasticMirrorDescent.lean, a user of ftrl_regret_le; target 0.11 keeps that name.
  • #160 edits Bandits/AsymptoticOptimality.lean, where target 2.3 migrates isLittleO_sub_mul_of_tendsto_div.
• How the targets were checked. Every declaration and file named was checked by grep against LMLExplore origin/main (bacf8f7), and the Tau Ceti and LML names at LMLExplore's pins. The claims about how existing proofs generalize come from reading the code; nothing was compiled.

Suggested.lean builds.

Drafted with Claude Opus 5.5 at the request of the code owner, from a target-by-target check of the merged code.

🤖 Generated with Claude Code