[RemyDegenne]

This PR defines causal deterministic online learners and their runs, the closed-loop run, the regret-guarantee predicate, the operations used by the reductions (restart, the coordinatewise product, the sum of plays, and post-composition of plays, which gives translation), and the FTRL learner as an instance. This is the milestone OnlineLearning Layer 0.2 ("Online learners") of LMLRoadmaps, together with the second completion check of Layer 0 (the regret of a learner restarted at round s over [s, s + τ) is the regret of the original learner over [0, τ) on the shifted feedback).

New modules:

• LMLExplore/OnlineLearning/Learner/Basic.lean defines OnlineLearner C G X (@[ext] structure with one field, play : (t : ℕ) → (Fin t → C × G) → C → X, following the signature in Suggested.lean) and run. It proves causality (run_congr, run_congr_feedback) and that a learner is determined by its runs (ext_run, given [Nonempty G]). It defines closedLoopFeedback, by well-founded recursion on the round, and characterises it as the unique fixed point of g ↦ fun t ↦ φ t (A.run c g t) (closedLoopFeedback_eq, eq_closedLoopFeedback_of_forall_lt, closedLoopFeedback_unique, closedLoopFeedback_congr). It also defines HasRegretBound A L adm U B, with hasRegretBound_iff, HasRegretBound.regret_le and HasRegretBound.mono. The predicate takes a general loss evaluation L : G → X → ℝ and is stated through the existing regret, so it covers linear losses (L y x = y x) as well as expert losses.
• LMLExplore/OnlineLearning/Learner/Operations.lean covers the four operations:
  • restart, with run_restart_add, run_restart_of_lt, restart_zero, intervalRegret_run_restart (the completion check) and HasRegretBound.intervalRegret_run_restart_le;
  • pi, for any index type, with run_pi, regret_run_pi and HasRegretBound.pi for separable losses ∑ i, L i (g i) (x i), the form AdaGrad (Layer 2.4) consumes;
  • OnlineLearner.sum, with run_sum, regret_run_sum and regret_run_sum_le [Ora, Theorem 13.11], stated as the inequality for every decomposition, as the roadmap's Layer 13.3 correction asks;
  • map, with run_map, map_id, map_map, regret_run_map, and the translation statements regret_run_map_add_left and HasRegretBound.map_add_left [Ora, Proposition 13.10].
• LMLExplore/OnlineLearning/FTRL/Learner.lean defines OnlineLearner.ftrl K F η x₀. At each round it plays a chosen minimizer of the FTRL objective when one exists, and x₀ otherwise. Its runs satisfy IsFTRLPlay (isFTRLPlay_run_ftrl, and isFTRLPlay_run_ftrl_of_isCompact via exists_ftrl). With a strongly convex potential that is differentiable within K, it satisfies HasRegretBound (hasRegretBound_ftrl_of_strongConvexOn, from the existing ftrl_regret_le_of_strongConvexOn_of_antitone, [Ora, Corollary 7.6]). This is a non-degenerate witness of the new predicate.

On reuse: LML's Learning.Algorithm.deterministic is the measurable, kernel-based counterpart for stochastic environments. It requires measurable spaces and measurable policies, and its history contains the learner's own actions. The roadmap's Layer 0.2 asks for a measure-free causal learner whose play is a function of the past contexts and feedback, and Layers 6.5 and 12–16 compose such learners, so a separate structure is needed. The module docstring points to the LML counterpart. No existing declaration is removed or renamed.

After this PR, Layer 0.2 still needs:

• the skip-zero wrapper (Layer 13.2);
• the mirror-descent and projected online subgradient descent learners, whose runs satisfy IsMirrorDescentStep.

Roadmap: OnlineLearning

🤖 Prepared with Claude Code