diff --git a/LMLExplore/OnlineLearning/FTRL/Learner.lean b/LMLExplore/OnlineLearning/FTRL/Learner.lean
new file mode 100644
index 0000000..15df838
--- /dev/null
+++ b/LMLExplore/OnlineLearning/FTRL/Learner.lean
@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LMLExplore.OnlineLearning.FTRL.Basic
+public import LMLExplore.OnlineLearning.Learner.Basic
+
+/-!
+# The FTRL learner
+
+Follow the regularized leader is specified in `LMLExplore.OnlineLearning.FTRL.Basic` by the
+predicate `IsFTRLPlay` on its plays, and its regret bounds take the plays as hypotheses. This file
+constructs the algorithm as an online learner (`OnlineLearner`) for online linear optimization: the
+learner `OnlineLearner.ftrl K F η x₀` plays at round `t` a minimizer over `K` of the FTRL objective
+`b ↦ η t * ∑ s < t, y s b + F b` of the past linear losses, chosen among the minimizers when there
+is one, and the default point `x₀` when there is none.
+
+* Its plays are FTRL plays at every round where a minimizer exists (`isFTRLPlay_run_ftrl`), in
+  particular at every round when `K` is compact and nonempty and `F` is continuous on `K`
+  (`isFTRLPlay_run_ftrl_of_isCompact`).
+* With a strongly convex potential, differentiable within `K`, and positive nonincreasing learning
+  rates, it has the anytime regret bound of [Ora, Corollary 7.6]
+  `(F u - F (x 0)) / η (n - 1) + ∑ t < n, η t / (2 m) * ‖y t‖ ^ 2` against every `u ∈ K`, for every
+  sequence of linear losses (`hasRegretBound_ftrl_of_strongConvexOn`).
+
+## Main definitions
+
+* `LMLExplore.OnlineLearning.OnlineLearner.ftrl K F η x₀`: the FTRL learner.
+
+## Main statements
+
+* `OnlineLearner.isFTRLPlay_run_ftrl`: the plays of the FTRL learner are FTRL plays.
+* `OnlineLearner.hasRegretBound_ftrl_of_strongConvexOn`: the regret guarantee of the FTRL
+  learner with a strongly convex potential.
+
+## References
+
+* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*,
+  arXiv:1912.13213v10, 2026.
+-/
+
+public section
+
+open Finset
+
+namespace LMLExplore.OnlineLearning
+
+namespace OnlineLearner
+
+variable {C E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {F : E → ℝ}
+  {η : ℕ → ℝ} {x₀ : E}
+
+open Classical in
+/-- The **FTRL learner** on `K` with potential `F`, learning rates `η` and default play `x₀`, for
+online linear optimization: at round `t`, it plays a minimizer over `K` of the FTRL objective
+`b ↦ η t * ∑ s < t, y s b + F b` of the past linear losses `y s` when one exists, and `x₀`
+otherwise. It ignores the contexts. -/
+noncomputable def ftrl (K : Set E) (F : E → ℝ) (η : ℕ → ℝ) (x₀ : E) :
+    OnlineLearner C (E →L[ℝ] ℝ) E where
+  play t h _ :=
+    if hx : ∃ x ∈ K, IsMinOn (fun b ↦ η t * ∑ s, (h s).2 b + F b) K x then hx.choose else x₀
+
+/-- **The FTRL learner plays FTRL.** At every round where the FTRL objective has a minimizer over
+`K`, the play of the FTRL learner is a play of FTRL (`IsFTRLPlay`). -/
+theorem isFTRLPlay_run_ftrl (c : ℕ → C) (y : ℕ → E →L[ℝ] ℝ) {t : ℕ}
+    (h : ∃ x, IsFTRLPlay K F (η t) y t x) :
+    IsFTRLPlay K F (η t) y t ((ftrl K F η x₀).run c y t) := by
+  have h_obj : (fun b ↦ η t * ∑ s : Fin t, y s b + F b) =
+      fun b ↦ η t * ∑ s ∈ range t, y s b + F b := by
+    funext b
+    rw [Fin.sum_univ_eq_sum_range (fun s ↦ y s b) t]
+  have hx : ∃ x ∈ K, IsMinOn (fun b ↦ η t * ∑ s : Fin t, y s b + F b) K x := by
+    obtain ⟨x, hx⟩ := h
+    exact ⟨x, hx.mem, h_obj ▸ hx.isMinOn⟩
+  rw [run_def]
+  simp only [ftrl, hx, dite_true]
+  exact ⟨hx.choose_spec.1, h_obj ▸ hx.choose_spec.2⟩
+
+/-- On a nonempty compact set `K`, with a potential `F` continuous on `K`, every play of the FTRL
+learner is a play of FTRL. -/
+theorem isFTRLPlay_run_ftrl_of_isCompact (hK : IsCompact K) (hK_ne : K.Nonempty)
+    (hF : ContinuousOn F K) (c : ℕ → C) (y : ℕ → E →L[ℝ] ℝ) (t : ℕ) :
+    IsFTRLPlay K F (η t) y t ((ftrl K F η x₀).run c y t) :=
+  isFTRLPlay_run_ftrl c y <| by
+    obtain ⟨a, ha⟩ := exists_ftrl hK hK_ne hF (η t) y
+    exact ⟨a t, ha t⟩
+
+/-- **Regret guarantee of the FTRL learner** [Ora, Corollary 7.6]. Let `K` be compact, let the
+potential `F` be continuous on `K`, `m`-strongly convex on `K` (so that `K` is convex) for the
+norm of `E` with `m > 0` and differentiable within `K` at every point of `K`, and let the learning
+rates `η t > 0` be nonincreasing. Then for every sequence of linear losses `y`, every horizon `n`
+and every `u ∈ K`, the plays `x` of the FTRL learner satisfy
+`∑ t < n, y t (x t - u) ≤ (F u - F (x 0)) / η (n - 1) + ∑ t < n, η t / (2 m) * ‖y t‖ ^ 2`,
+where `x 0` minimizes `F` over `K` and `‖y t‖` is the dual norm. -/
+theorem hasRegretBound_ftrl_of_strongConvexOn (hK : IsCompact K) (hF_cont : ContinuousOn F K)
+    {m : ℝ} (hF : StrongConvexOn K m F) (hm : 0 < m)
+    (hF_diff : ∀ x ∈ K, DifferentiableWithinAt ℝ F K x) (hη : ∀ t, 0 < η t)
+    (hη_anti : Antitone η) :
+    (ftrl (C := C) K F η x₀).HasRegretBound (fun y x ↦ y x) (fun _ _ ↦ True) K
+      (fun n c y u ↦ (F u - F ((ftrl K F η x₀).run c y 0)) / η (n - 1) +
+        ∑ t ∈ range n, η t / (2 * m) * ‖y t‖ ^ 2) := by
+  refine hasRegretBound_iff.mpr fun c y n _ u hu ↦ ?_
+  have ha (t : ℕ) := isFTRLPlay_run_ftrl_of_isCompact (η := η) (x₀ := x₀) hK ⟨u, hu⟩ hF_cont c y t
+  rw [regret_eq_sum_apply_sub]
+  exact ftrl_regret_le_of_strongConvexOn_of_antitone hF hm hη hη_anti y _ (ha 0)
+    (fun t _ ↦ ha t) _ (fun t _ ↦ (hF_diff _ (ha t).mem).hasFDerivWithinAt) hu
+
+end OnlineLearner
+
+end LMLExplore.OnlineLearning
diff --git a/LMLExplore/OnlineLearning/Learner/Basic.lean b/LMLExplore/OnlineLearning/Learner/Basic.lean
new file mode 100644
index 0000000..5a34823
--- /dev/null
+++ b/LMLExplore/OnlineLearning/Learner/Basic.lean
@@ -0,0 +1,220 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LMLExplore.OnlineLearning.Regret
+
+/-!
+# Online learners
+
+A deterministic online learner plays, at each round `t = 0, 1, …`, a point of a type `X`. Before
+its play it sees a context in a type `C` (the set of active experts, a hint, …), and after its play
+it receives a feedback in a type `G` (a loss function, a subgradient, a coin outcome, …). The play
+of round `t` is a function of the contexts and feedback of the rounds `s < t` and of the context of
+round `t`: an `OnlineLearner C G X` is this function. This file defines learners, their runs and a
+predicate for their regret guarantees [Ora, Chapter 1]. The structures of the reductions of
+[Ora, Chapters 12–14] compose learners; the operations that they use are in
+`LMLExplore.OnlineLearning.Learner.Operations`.
+
+* The **run** `A.run c g` of a learner against sequences of contexts `c` and feedback `g` is the
+  sequence of its plays. The play of round `t` depends only on the contexts of the rounds `s ≤ t`
+  and on the feedback of the rounds `s < t` (`run_congr`), and a learner is determined by its runs
+  when `G` is nonempty (`ext_run`).
+* In the **closed-loop run**, the feedback of round `t` is a given function `φ t` of the play of
+  round `t`, as for the surrogate losses of a reduction, or the subgradients of convex losses at
+  the plays. The feedback sequence `A.closedLoopFeedback c φ` is defined by recursion on the
+  rounds; it is the unique sequence `g` with `g t = φ t (A.run c g t)` for every `t`
+  (`closedLoopFeedback_eq`, `closedLoopFeedback_unique`), and the closed-loop plays are the run
+  `A.run c (A.closedLoopFeedback c φ)`.
+* A **regret guarantee** `A.HasRegretBound L adm U B` says that, against every sequence of
+  feedback whose first `n` values are admissible (`adm`) for their contexts, the regret after `n`
+  rounds of the plays of `A` for the losses `L (g t)` against every comparator `u ∈ U` is at most
+  `B n c g u` (`HasRegretBound.regret_le`). Since the bound holds for every sequence of feedback,
+  it holds in particular for the feedback `A.closedLoopFeedback c φ` of the closed-loop runs, that
+  is, against adaptive adversaries.
+
+The learners of this file are deterministic and use no measurability: LML's
+`Learning.Algorithm.deterministic` is the measurable counterpart, used for stochastic environments.
+
+## Main definitions
+
+* `LMLExplore.OnlineLearning.OnlineLearner C G X`: a causal online learner.
+* `LMLExplore.OnlineLearning.OnlineLearner.run A c g`: the plays of `A` against the contexts `c`
+  and the feedback `g`.
+* `LMLExplore.OnlineLearning.OnlineLearner.closedLoopFeedback A c φ`: the feedback of the
+  closed-loop run, in which the feedback of round `t` is `φ t` of the play of round `t`.
+* `LMLExplore.OnlineLearning.OnlineLearner.HasRegretBound A L adm U B`: the regret guarantee.
+
+## Main statements
+
+* `OnlineLearner.run_congr`: causality of the runs.
+* `OnlineLearner.ext_run`: a learner with nonempty feedback type is determined by its runs.
+* `OnlineLearner.closedLoopFeedback_eq`, `OnlineLearner.eq_closedLoopFeedback_of_forall_lt`,
+  `OnlineLearner.closedLoopFeedback_unique`: the closed-loop feedback is the unique fixed point of
+  `g ↦ fun t ↦ φ t (A.run c g t)`, also on a finite horizon.
+
+## References
+
+* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*,
+  arXiv:1912.13213v10, 2026.
+-/
+
+public section
+
+namespace LMLExplore.OnlineLearning
+
+/-- A causal deterministic **online learner** with contexts in `C`, feedback in `G` and plays in
+`X`: the play `A.play t h c` of round `t`, from the history `h` of the contexts and feedback of the
+rounds `s < t` and the context `c` of round `t`. The context of a round is revealed before the
+play (for example the set of active experts, or a hint), and the feedback after it (for example a
+loss function, or a subgradient of the loss at the play). -/
+@[ext]
+structure OnlineLearner (C G X : Type*) where
+  /-- The play of round `t`, from the contexts and feedback of the rounds `s < t` and the context
+  of round `t`. -/
+  play : (t : ℕ) → (Fin t → C × G) → C → X
+
+namespace OnlineLearner
+
+variable {C G X : Type*} (A : OnlineLearner C G X)
+
+section Run
+
+/-- The **run** of the learner `A` against the contexts `c` and the feedback `g`: the play of
+round `t` is the play of `A` from the contexts and feedback of the rounds `s < t` and the context
+of round `t`. -/
+def run (c : ℕ → C) (g : ℕ → G) (t : ℕ) : X :=
+  A.play t (fun s ↦ (c s, g s)) (c t)
+
+lemma run_def (c : ℕ → C) (g : ℕ → G) (t : ℕ) :
+    A.run c g t = A.play t (fun s ↦ (c s, g s)) (c t) := (rfl)
+
+/-- The first play of a run depends only on the first context. -/
+lemma run_zero (c : ℕ → C) (g : ℕ → G) : A.run c g 0 = A.play 0 Fin.elim0 (c 0) := by
+  rw [run_def]
+  congr
+  exact funext fun s ↦ s.elim0
+
+/-- **Causality** of the runs: the play of round `t` depends only on the contexts of the rounds
+`s ≤ t` and on the feedback of the rounds `s < t`. -/
+lemma run_congr {c c' : ℕ → C} {g g' : ℕ → G} {t : ℕ} (hc : ∀ s ≤ t, c s = c' s)
+    (hg : ∀ s < t, g s = g' s) : A.run c g t = A.run c' g' t := by
+  rw [run_def, run_def, hc t le_rfl]
+  congr
+  exact funext fun s ↦ by rw [hc s s.2.le, hg s s.2]
+
+/-- The play of round `t` does not depend on the feedback of the rounds `s ≥ t`. -/
+lemma run_congr_feedback (c : ℕ → C) {g g' : ℕ → G} {t : ℕ} (hg : ∀ s < t, g s = g' s) :
+    A.run c g t = A.run c g' t :=
+  A.run_congr (fun _ _ ↦ rfl) hg
+
+/-- Every play of a learner from a history and a context is the play of round `t` of a run: the
+run against sequences extending the history, with the context `c₀` at round `t`. -/
+lemma exists_run_eq_play [Nonempty G] (t : ℕ) (h : Fin t → C × G) (c₀ : C) :
+    ∃ (c : ℕ → C) (g : ℕ → G), ∀ B : OnlineLearner C G X, B.run c g t = B.play t h c₀ := by
+  classical
+  obtain ⟨g₀⟩ := ‹Nonempty G›
+  refine ⟨fun s ↦ if hs : s < t then (h ⟨s, hs⟩).1 else c₀,
+    fun s ↦ if hs : s < t then (h ⟨s, hs⟩).2 else g₀, fun B ↦ ?_⟩
+  simp only [run_def, lt_irrefl, dite_false]
+  congr
+  exact funext fun s ↦ by simp [s.2]
+
+/-- A learner with a nonempty type of feedback is determined by its runs. -/
+lemma ext_run [Nonempty G] {A B : OnlineLearner C G X}
+    (h : ∀ (c : ℕ → C) (g : ℕ → G) (t : ℕ), A.run c g t = B.run c g t) : A = B := by
+  ext t hist c₀
+  obtain ⟨c, g, hcg⟩ := exists_run_eq_play t hist c₀
+  rw [← hcg A, ← hcg B, h]
+
+end Run
+
+section ClosedLoop
+
+/-- The feedback of the **closed-loop run** of the learner `A` against the contexts `c` with the
+feedback functions `φ`: the feedback of round `t` is `φ t` applied to the play of round `t`, which
+is the play of `A` from the contexts and the closed-loop feedback of the rounds `s < t` and the
+context of round `t`. The closed-loop plays are `A.run c (A.closedLoopFeedback c φ)`
+(`closedLoopFeedback_eq`). -/
+def closedLoopFeedback (c : ℕ → C) (φ : ℕ → X → G) (t : ℕ) : G :=
+  φ t (A.play t (fun s ↦ (c s, closedLoopFeedback c φ s)) (c t))
+termination_by t
+decreasing_by exact s.isLt
+
+/-- The feedback of round `t` of the closed-loop run is `φ t` applied to the play of round `t`. -/
+lemma closedLoopFeedback_eq (c : ℕ → C) (φ : ℕ → X → G) (t : ℕ) :
+    A.closedLoopFeedback c φ t = φ t (A.run c (A.closedLoopFeedback c φ) t) := by
+  rw [closedLoopFeedback, run_def]
+
+/-- **Uniqueness of the closed-loop feedback on a finite horizon.** A sequence `g` whose value at
+each round `t < n` is `φ t` applied to the play of round `t` of the run against `g` agrees with the
+closed-loop feedback on the rounds `t < n`. -/
+lemma eq_closedLoopFeedback_of_forall_lt {c : ℕ → C} {φ : ℕ → X → G} {g : ℕ → G} {n : ℕ}
+    (hg : ∀ t < n, g t = φ t (A.run c g t)) {t : ℕ} (ht : t < n) :
+    g t = A.closedLoopFeedback c φ t := by
+  induction t using Nat.strong_induction_on with
+  | _ t ih =>
+    rw [hg t ht, closedLoopFeedback_eq,
+      A.run_congr_feedback c fun s hs ↦ ih s hs (hs.trans ht)]
+
+/-- **Uniqueness of the closed-loop feedback.** The closed-loop feedback is the unique sequence `g`
+whose value at each round is `φ t` applied to the play of round `t` of the run against `g`. -/
+lemma closedLoopFeedback_unique {c : ℕ → C} {φ : ℕ → X → G} {g : ℕ → G}
+    (hg : ∀ t, g t = φ t (A.run c g t)) : g = A.closedLoopFeedback c φ :=
+  funext fun t ↦ A.eq_closedLoopFeedback_of_forall_lt (n := t + 1) (fun s _ ↦ hg s) t.lt_succ_self
+
+/-- The closed-loop feedback of the rounds `t < n` depends only on the contexts and on the feedback
+functions of the rounds `t < n`. -/
+lemma closedLoopFeedback_congr {c c' : ℕ → C} {φ φ' : ℕ → X → G} {n : ℕ}
+    (hc : ∀ t < n, c t = c' t) (hφ : ∀ t < n, φ t = φ' t) {t : ℕ} (ht : t < n) :
+    A.closedLoopFeedback c φ t = A.closedLoopFeedback c' φ' t := by
+  refine A.eq_closedLoopFeedback_of_forall_lt (fun s hs ↦ ?_) ht
+  rw [closedLoopFeedback_eq, hφ s hs,
+    A.run_congr (fun r hr ↦ hc r (hr.trans_lt hs)) fun _ _ ↦ rfl]
+
+end ClosedLoop
+
+section HasRegretBound
+
+/-- The learner `A` has the **regret bound** `B` for the losses `L`, the admissible feedback `adm`
+and the comparators `U`: for all contexts `c`, feedback `g` and horizons `n` such that the feedback
+`g t` of each round `t < n` is admissible for the context `c t`, the regret after `n` rounds of the
+plays of `A` for the losses `L (g t)` against every comparator `u ∈ U` is at most `B n c g u`.
+
+For online linear optimization, the feedback is a linear loss `y t` and `L y x = y x`; for
+prediction with expert advice, it is the vector of the losses of the experts. The bound may depend
+on the horizon, on the contexts and feedback, and on the comparator. -/
+def HasRegretBound (L : G → X → ℝ) (adm : C → G → Prop) (U : Set X)
+    (B : ℕ → (ℕ → C) → (ℕ → G) → X → ℝ) : Prop :=
+  ∀ (c : ℕ → C) (g : ℕ → G) (n : ℕ), (∀ t < n, adm (c t) (g t)) →
+    ∀ u ∈ U, regret (fun t ↦ L (g t)) (A.run c g) u n ≤ B n c g u
+
+variable {A} {L : G → X → ℝ} {adm adm' : C → G → Prop} {U U' : Set X}
+  {B B' : ℕ → (ℕ → C) → (ℕ → G) → X → ℝ}
+
+lemma hasRegretBound_iff : A.HasRegretBound L adm U B ↔
+    ∀ (c : ℕ → C) (g : ℕ → G) (n : ℕ), (∀ t < n, adm (c t) (g t)) →
+      ∀ u ∈ U, regret (fun t ↦ L (g t)) (A.run c g) u n ≤ B n c g u := Iff.rfl
+
+/-- The regret inequality of a regret guarantee. It applies to every run, in particular to the
+closed-loop runs, with `g = A.closedLoopFeedback c φ`. -/
+lemma HasRegretBound.regret_le (hA : A.HasRegretBound L adm U B) {c : ℕ → C} {g : ℕ → G} {n : ℕ}
+    (hg : ∀ t < n, adm (c t) (g t)) {u : X} (hu : u ∈ U) :
+    regret (fun t ↦ L (g t)) (A.run c g) u n ≤ B n c g u :=
+  hA c g n hg u hu
+
+/-- A regret guarantee holds for fewer admissible feedback, fewer comparators and larger bounds. -/
+lemma HasRegretBound.mono (hA : A.HasRegretBound L adm U B)
+    (hadm : ∀ c g, adm' c g → adm c g) (hU : U' ⊆ U)
+    (hB : ∀ n c g u, (∀ t < n, adm' (c t) (g t)) → u ∈ U' → B n c g u ≤ B' n c g u) :
+    A.HasRegretBound L adm' U' B' := fun c g n hg u hu ↦
+  (hA.regret_le (fun t ht ↦ hadm _ _ (hg t ht)) (hU hu)).trans (hB n c g u hg hu)
+
+end HasRegretBound
+
+end OnlineLearner
+
+end LMLExplore.OnlineLearning
diff --git a/LMLExplore/OnlineLearning/Learner/Operations.lean b/LMLExplore/OnlineLearning/Learner/Operations.lean
new file mode 100644
index 0000000..04688a7
--- /dev/null
+++ b/LMLExplore/OnlineLearning/Learner/Operations.lean
@@ -0,0 +1,287 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LMLExplore.OnlineLearning.Learner.Basic
+
+/-!
+# Operations on online learners
+
+The reductions of online learning [Ora, Chapters 12–14] build learners from other learners: they
+restart copies of a learner, run learners coordinatewise, add the plays of several learners, and
+transform the plays of a learner. This file defines these operations on `OnlineLearner`, computes
+their runs, and transfers regret guarantees (`OnlineLearner.HasRegretBound`) through them.
+
+* `A.restart s` plays from round `s` on as a fresh copy of `A` started at round `s`: its play of
+  round `s + t` is the play of round `t` of `A` against the contexts and feedback shifted by `s`
+  (`run_restart_add`). Its regret on the interval of rounds `[s, s + τ)` is therefore the regret
+  after `τ` rounds of `A` on the shifted feedback (`intervalRegret_run_restart`), and a regret
+  guarantee of `A` bounds the interval regrets of its restarts
+  (`HasRegretBound.intervalRegret_run_restart_le`). This is how the strongly adaptive algorithms
+  of [Ora, Chapter 14] use black-box learners.
+* `OnlineLearner.pi A`, for a family of learners `A i` sharing the contexts, plays the family of
+  their plays and feeds the coordinate `g i` of the feedback to `A i` (`run_pi`). For losses that
+  are sums of losses of the coordinates, such as linear losses on `ι → ℝ`, its regret is the sum of
+  the regrets of the coordinates (`regret_run_pi`, `HasRegretBound.pi`): this is how AdaGrad
+  [Ora, Section 4.2] and coordinatewise coin betting [Ora, Section 13.3] are built from
+  one-dimensional learners.
+* `OnlineLearner.sum A`, for a finite family of learners receiving the same feedback, plays the sum
+  of their plays (`run_sum`). For linear losses, its regret against `∑ i, v i` is the sum of the
+  regrets of the learners `A i` against `v i` (`regret_run_sum`, `regret_run_sum_le`)
+  [Ora, Theorem 13.11].
+* `A.map f` plays the images by `f` of the plays of `A` (`run_map`). For a translation
+  `f = (x₀ + ·)` and linear losses, the regret against `u` is the regret of `A` against `u - x₀`
+  (`regret_run_map_add_left`, `HasRegretBound.map_add_left`) [Ora, Proposition 13.10].
+
+## Main definitions
+
+* `LMLExplore.OnlineLearning.OnlineLearner.restart A s`: `A` restarted at round `s`.
+* `LMLExplore.OnlineLearning.OnlineLearner.pi A`: the coordinatewise product of a family of
+  learners.
+* `LMLExplore.OnlineLearning.OnlineLearner.sum A`: the sum of the plays of a finite family of
+  learners.
+* `LMLExplore.OnlineLearning.OnlineLearner.map A f`: the images by `f` of the plays of `A`.
+
+## Main statements
+
+* `OnlineLearner.intervalRegret_run_restart`: the regret of a learner restarted at round `s` on the
+  rounds `[s, s + τ)` is the regret after `τ` rounds of the learner on the shifted feedback.
+* `OnlineLearner.HasRegretBound.pi`: the regret guarantee of a coordinatewise product.
+* `OnlineLearner.regret_run_sum_le`: the regret of a sum of learners is at most the sum of their
+  regret bounds, for every decomposition of the comparator.
+* `OnlineLearner.HasRegretBound.map_add_left`: the regret guarantee of a translated learner.
+
+## References
+
+* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*,
+  arXiv:1912.13213v10, 2026.
+-/
+
+public section
+
+open Finset
+
+namespace LMLExplore.OnlineLearning
+
+namespace OnlineLearner
+
+variable {C G X Y : Type*}
+
+section Restart
+
+variable (A : OnlineLearner C G X)
+
+/-- The play of round `t` from a history read off a sequence `F` depends on `t` only through its
+value. -/
+private lemma play_comp_val_congr (F : ℕ → C × G) {t t' : ℕ} (h : t = t') (c : C) :
+    A.play t (fun i ↦ F i) c = A.play t' (fun i ↦ F i) c := by
+  subst h
+  rfl
+
+/-- The learner `A` **restarted at round `s`**: from round `s` on, it plays as a fresh copy of `A`
+started at round `s`, from the contexts and feedback of the rounds `s, s + 1, …` only; before
+round `s`, it plays as `A` at its first round, from the current context. -/
+def restart (s : ℕ) : OnlineLearner C G X where
+  play t h c :=
+    if hst : s ≤ t then A.play (t - s) (fun i ↦ h ⟨s + i, by omega⟩) c else A.play 0 Fin.elim0 c
+
+/-- From round `s` on, the plays of `A` restarted at round `s` are the plays of `A` against the
+contexts and feedback shifted by `s`. -/
+lemma run_restart_add (s : ℕ) (c : ℕ → C) (g : ℕ → G) (t : ℕ) :
+    (A.restart s).run c g (s + t) = A.run (fun r ↦ c (s + r)) (fun r ↦ g (s + r)) t := by
+  simp only [run_def, restart, Nat.le_add_right, dite_true]
+  exact A.play_comp_val_congr (fun r ↦ (c (s + r), g (s + r))) (Nat.add_sub_cancel_left ..) _
+
+/-- Before round `s`, the plays of `A` restarted at round `s` are the first play of `A` from the
+current context. -/
+lemma run_restart_of_lt {s t : ℕ} (hts : t < s) (c : ℕ → C) (g : ℕ → G) :
+    (A.restart s).run c g t = A.play 0 Fin.elim0 (c t) := by
+  simp [run_def, restart, Nat.not_le.mpr hts]
+
+/-- A learner restarted at round `0` is the learner itself. -/
+@[simp]
+lemma restart_zero : A.restart 0 = A := by
+  ext t h c
+  simp only [restart, Nat.zero_le, dite_true]
+  exact congrArg (A.play t · c) (funext fun i ↦ congrArg h (Fin.ext (zero_add _)))
+
+variable {L : G → X → ℝ} {c : ℕ → C} {g : ℕ → G}
+
+/-- **Regret of a restarted learner.** The regret of `A` restarted at round `s` on the rounds
+`[s, s + τ)` is the regret after `τ` rounds of `A` against the contexts and feedback shifted by
+`s`. -/
+lemma intervalRegret_run_restart (L : G → X → ℝ) (s : ℕ) (c : ℕ → C) (g : ℕ → G) (u : X)
+    (τ : ℕ) :
+    intervalRegret (fun t ↦ L (g t)) ((A.restart s).run c g) u s τ =
+      regret (fun t ↦ L (g (s + t))) (A.run (fun t ↦ c (s + t)) (fun t ↦ g (s + t))) u τ := by
+  rw [intervalRegret_eq_regret]
+  simp only [run_restart_add]
+
+variable {A} {adm : C → G → Prop} {U : Set X} {B : ℕ → (ℕ → C) → (ℕ → G) → X → ℝ}
+
+/-- A regret guarantee of `A` bounds the regret of `A` restarted at round `s` on the rounds
+`[s, s + τ)` by the bound of `τ` rounds on the shifted contexts and feedback. -/
+lemma HasRegretBound.intervalRegret_run_restart_le (hA : A.HasRegretBound L adm U B) (s : ℕ)
+    {τ : ℕ} (hg : ∀ t < τ, adm (c (s + t)) (g (s + t))) {u : X} (hu : u ∈ U) :
+    intervalRegret (fun t ↦ L (g t)) ((A.restart s).run c g) u s τ ≤
+      B τ (fun t ↦ c (s + t)) (fun t ↦ g (s + t)) u := by
+  rw [intervalRegret_run_restart]
+  exact hA.regret_le hg hu
+
+end Restart
+
+section Pi
+
+variable {ι : Type*} {G X : ι → Type*}
+
+/-- The **coordinatewise product** of a family of learners `A i` sharing the contexts: it plays the
+family of the plays of the learners, and feeds the coordinate `g i` of each feedback to `A i`. -/
+def pi (A : ∀ i, OnlineLearner C (G i) (X i)) : OnlineLearner C (∀ i, G i) (∀ i, X i) where
+  play t h c i := (A i).play t (fun s ↦ ((h s).1, (h s).2 i)) c
+
+variable (A : ∀ i, OnlineLearner C (G i) (X i))
+
+/-- The plays of the coordinatewise product are the plays of the learners against the coordinates
+of the feedback. -/
+@[simp]
+lemma run_pi (c : ℕ → C) (g : ℕ → ∀ i, G i) (t : ℕ) (i : ι) :
+    (pi A).run c g t i = (A i).run c (fun s ↦ g s i) t := by
+  rw [run_def, run_def]
+  rfl
+
+variable [Fintype ι]
+
+/-- **Regret of a coordinatewise product.** For losses that are sums `∑ i, L i (g i) (x i)` of
+losses of the coordinates, the regret of the coordinatewise product against `u` is the sum of the
+regrets of the learners `A i` against `u i`. -/
+lemma regret_run_pi (L : ∀ i, G i → X i → ℝ) (c : ℕ → C) (g : ℕ → ∀ i, G i) (u : ∀ i, X i)
+    (n : ℕ) :
+    regret (fun t x ↦ ∑ i, L i (g t i) (x i)) ((pi A).run c g) u n =
+      ∑ i, regret (fun t ↦ L i (g t i)) ((A i).run c fun s ↦ g s i) (u i) n := by
+  simp only [regret_def, run_pi, ← sum_sub_distrib]
+  exact sum_comm
+
+variable {A} {L : ∀ i, G i → X i → ℝ} {adm : ∀ i, C → G i → Prop} {U : ∀ i, Set (X i)}
+  {B : ∀ i, ℕ → (ℕ → C) → (ℕ → G i) → X i → ℝ}
+
+/-- **Regret guarantee of a coordinatewise product.** If each learner `A i` has the regret bound
+`B i` for the losses `L i`, then their coordinatewise product has the regret bound
+`∑ i, B i n c (fun t ↦ g t i) (u i)` for the losses `∑ i, L i (g i) (x i)`, the feedback whose
+coordinates are admissible and the comparators in the product of the sets `U i`. -/
+theorem HasRegretBound.pi (hA : ∀ i, (A i).HasRegretBound (L i) (adm i) (U i) (B i)) :
+    (pi A).HasRegretBound (fun g x ↦ ∑ i, L i (g i) (x i)) (fun c g ↦ ∀ i, adm i c (g i))
+      (Set.univ.pi U) (fun n c g u ↦ ∑ i, B i n c (fun t ↦ g t i) (u i)) := by
+  refine hasRegretBound_iff.mpr fun c g n hg u hu ↦ ?_
+  rw [regret_run_pi]
+  exact sum_le_sum fun i _ ↦
+    (hA i).regret_le (fun t ht ↦ hg t ht i) (Set.mem_univ_pi.mp hu i)
+
+end Pi
+
+section Sum
+
+variable {ι : Type*} [Fintype ι] [AddCommMonoid X]
+
+/-- The **sum** of a finite family of learners receiving the same contexts and feedback: it plays
+the sum of their plays. -/
+protected def sum (A : ι → OnlineLearner C G X) : OnlineLearner C G X where
+  play t h c := ∑ i, (A i).play t h c
+
+variable (A : ι → OnlineLearner C G X)
+
+/-- The plays of the sum of learners are the sums of their plays. -/
+@[simp]
+lemma run_sum (c : ℕ → C) (g : ℕ → G) (t : ℕ) :
+    (OnlineLearner.sum A).run c g t = ∑ i, (A i).run c g t := by
+  simp only [run_def]
+  rfl
+
+variable {X : Type*} [AddCommGroup X] {F : Type*} [FunLike F X ℝ] [AddMonoidHomClass F X ℝ]
+  (A : ι → OnlineLearner C F X)
+
+/-- **Regret of a sum of learners** [Ora, Theorem 13.11]. For linear losses, the regret of the sum
+of learners against `∑ i, v i` is the sum of the regrets of the learners `A i` against `v i`. -/
+lemma regret_run_sum (c : ℕ → C) (y : ℕ → F) (v : ι → X) (n : ℕ) :
+    regret (fun t ↦ y t) ((OnlineLearner.sum A).run c y) (∑ i, v i) n =
+      ∑ i, regret (fun t ↦ y t) ((A i).run c y) (v i) n := by
+  simp only [regret_eq_sum_apply_sub, run_sum, ← sum_sub_distrib, map_sum]
+  exact sum_comm
+
+variable {A} {adm : C → F → Prop} {U : ι → Set X} {B : ι → ℕ → (ℕ → C) → (ℕ → F) → X → ℝ}
+
+/-- **Regret guarantee of a sum of learners** [Ora, Theorem 13.11]. If each learner `A i` has the
+regret bound `B i` for linear losses against the comparators in `U i`, then for every
+decomposition `∑ i, v i` of the comparator with `v i ∈ U i`, the regret of the sum of the learners
+against `∑ i, v i` is at most `∑ i, B i n c y (v i)`. [Ora] states an equality with the minimum
+over the decompositions; the regret is at most this infimum. -/
+theorem regret_run_sum_le (hA : ∀ i, (A i).HasRegretBound (fun y x ↦ y x) adm (U i) (B i))
+    {c : ℕ → C} {y : ℕ → F} {n : ℕ} (hy : ∀ t < n, adm (c t) (y t)) {v : ι → X}
+    (hv : ∀ i, v i ∈ U i) :
+    regret (fun t ↦ y t) ((OnlineLearner.sum A).run c y) (∑ i, v i) n ≤
+      ∑ i, B i n c y (v i) := by
+  rw [regret_run_sum]
+  exact sum_le_sum fun i _ ↦ (hA i).regret_le hy (hv i)
+
+end Sum
+
+section Map
+
+variable (A : OnlineLearner C G X)
+
+/-- The learner playing the images by `f` of the plays of `A`. -/
+def map (f : X → Y) : OnlineLearner C G Y where
+  play t h c := f (A.play t h c)
+
+/-- The plays of `A.map f` are the images by `f` of the plays of `A`. -/
+@[simp]
+lemma run_map (f : X → Y) (c : ℕ → C) (g : ℕ → G) (t : ℕ) :
+    (A.map f).run c g t = f (A.run c g t) := by
+  rw [run_def, run_def]
+  rfl
+
+@[simp]
+lemma map_id : A.map id = A := (rfl)
+
+@[simp]
+lemma map_map {Z : Type*} (f : X → Y) (f' : Y → Z) : (A.map f).map f' = A.map (f' ∘ f) := (rfl)
+
+/-- The regret of `A.map f` against `f v` is the regret of `A` against `v` for the losses composed
+with `f`. -/
+lemma regret_run_map (L : G → Y → ℝ) (f : X → Y) (c : ℕ → C) (g : ℕ → G) (v : X) (n : ℕ) :
+    regret (fun t ↦ L (g t)) ((A.map f).run c g) (f v) n =
+      regret (fun t x ↦ L (g t) (f x)) (A.run c g) v n := by
+  simp [regret_def]
+
+variable {X : Type*} [AddCommGroup X] {F : Type*} [FunLike F X ℝ] [AddMonoidHomClass F X ℝ]
+  (A : OnlineLearner C F X)
+
+/-- **Regret of a translated learner.** For linear losses, the regret of the learner playing
+`x₀ + x t` against `u` is the regret of the learner playing `x t` against `u - x₀`. -/
+lemma regret_run_map_add_left (x₀ : X) (c : ℕ → C) (y : ℕ → F) (u : X) (n : ℕ) :
+    regret (fun t ↦ y t) ((A.map (x₀ + ·)).run c y) u n =
+      regret (fun t ↦ y t) (A.run c y) (u - x₀) n := by
+  simp only [regret_eq_sum_apply_sub, run_map]
+  exact sum_congr rfl fun t _ ↦ by
+    congr 1
+    abel
+
+variable {A} {adm : C → F → Prop} {U : Set X} {B : ℕ → (ℕ → C) → (ℕ → F) → X → ℝ}
+
+/-- **Regret guarantee of a translated learner** [Ora, Proposition 13.10]. If `A` has the regret
+bound `B` for linear losses against the comparators in `U`, then the learner playing `x₀ + x t`
+has the regret bound `B n c y (u - x₀)` against the comparators `u` with `u - x₀ ∈ U`. -/
+theorem HasRegretBound.map_add_left (hA : A.HasRegretBound (fun y x ↦ y x) adm U B) (x₀ : X) :
+    (A.map (x₀ + ·)).HasRegretBound (fun y x ↦ y x) adm ((· - x₀) ⁻¹' U)
+      (fun n c y u ↦ B n c y (u - x₀)) := by
+  refine hasRegretBound_iff.mpr fun c y n hy u hu ↦ ?_
+  rw [regret_run_map_add_left]
+  exact hA.regret_le hy hu
+
+end Map
+
+end OnlineLearner
+
+end LMLExplore.OnlineLearning