diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 4f59f7d8..1f86e0cd 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -8,6 +8,7 @@ public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.M
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
+public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
@@ -29,6 +30,7 @@ public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.Meas
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian
 public import LeanMachineLearning.ForMathlib.Probability.WithDensity
@@ -57,9 +59,11 @@ public import LeanMachineLearning.SequentialLearning.DivergenceDecomposition
 public import LeanMachineLearning.SequentialLearning.EvaluationEnv
 public import LeanMachineLearning.SequentialLearning.FeedbackMartingale
 public import LeanMachineLearning.SequentialLearning.FiniteActions
+public import LeanMachineLearning.SequentialLearning.IdentificationAlg
 public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 public import LeanMachineLearning.SequentialLearning.Means
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
+public import LeanMachineLearning.SequentialLearning.StoppedHistory
 public import LeanMachineLearning.SequentialLearning.SumRewards
 public import LeanMachineLearning.Tactic.EqLift
 public import LeanMachineLearning.Tactic.EqLift.ForMathlib.Kernel
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean
new file mode 100644
index 00000000..a41b1f2b
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/MeasurableSpace/Sigma.lean
@@ -0,0 +1,101 @@
+/-
+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 Mathlib.MeasureTheory.MeasurableSpace.Embedding
+public import Mathlib.MeasureTheory.Measure.Map
+
+/-!
+# Measurability of functions on a sigma type
+
+A function on `Σ a, β a` is measurable as soon as each of its restrictions `f ∘ Sigma.mk a` is.
+We also record measurability facts about the first projection of `Σ n : ℕ, β n`.
+-/
+
+@[expose] public section
+
+open MeasurableSpace MeasureTheory
+
+variable {α γ : Type*} {β : α → Type*} [∀ a, MeasurableSpace (β a)] [MeasurableSpace γ]
+
+@[fun_prop]
+lemma measurable_sigma_mk (a : α) : Measurable (Sigma.mk a : β a → Σ a, β a) :=
+  fun _ hs ↦ measurableSet_iInf.1 hs a
+
+/-- A function on a sigma type is measurable if all its restrictions to the fibers are. -/
+lemma measurable_sigma_of_measurable_comp_mk {f : (Σ a, β a) → γ}
+    (h : ∀ a, Measurable (f ∘ Sigma.mk a)) : Measurable f :=
+  fun _ hs ↦ measurableSet_iInf.2 fun a ↦ (h a) hs
+
+/-- A set in a sigma type is measurable iff its trace on every fiber is. -/
+lemma measurableSet_sigma_iff {s : Set (Σ a, β a)} :
+    MeasurableSet s ↔ ∀ a, MeasurableSet (Sigma.mk a ⁻¹' s) :=
+  measurableSet_iInf
+
+lemma measurable_sigma_iff {f : (Σ a, β a) → γ} :
+    Measurable f ↔ ∀ a, Measurable (f ∘ Sigma.mk a) :=
+  ⟨fun hf a ↦ hf.comp (measurable_sigma_mk a), measurable_sigma_of_measurable_comp_mk⟩
+
+/-- The first projection of a sigma type is measurable (it is constant on every fiber). -/
+lemma measurable_sigma_fst [MeasurableSpace α] : Measurable (Sigma.fst : (Σ a, β a) → α) :=
+  measurable_sigma_of_measurable_comp_mk fun _ ↦ measurable_const
+
+/-- `x ↦ ⟨n x, f (n x) x⟩` is measurable when the index `n x` ranges over a countable type with
+measurable singletons and each `f i` is measurable. -/
+lemma Measurable.sigmaMk [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α]
+    {n : γ → α} (hn : Measurable n) {f : (a : α) → γ → β a} (hf : ∀ a, Measurable (f a)) :
+    Measurable fun x ↦ (⟨n x, f (n x) x⟩ : Σ a, β a) := by
+  intro s hs
+  have : (fun x ↦ (⟨n x, f (n x) x⟩ : Σ a, β a)) ⁻¹' s =
+      ⋃ a, n ⁻¹' {a} ∩ f a ⁻¹' (Sigma.mk a ⁻¹' s) := by
+    ext x
+    simp only [Set.mem_preimage, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_singleton_iff]
+    constructor
+    · intro h
+      exact ⟨n x, rfl, h⟩
+    · rintro ⟨a, rfl, h⟩
+      exact h
+  rw [this]
+  exact MeasurableSet.iUnion fun a ↦
+    (hn (measurableSet_singleton a)).inter (hf a (measurableSet_sigma_iff.1 hs a))
+
+/-- `Sigma.mk a` is a measurable embedding. -/
+lemma measurableEmbedding_sigma_mk (a : α) :
+    MeasurableEmbedding (Sigma.mk a : β a → Σ a, β a) where
+  injective := sigma_mk_injective
+  measurable := measurable_sigma_mk a
+  measurableSet_image' s hs := by
+    rw [measurableSet_sigma_iff]
+    intro b
+    by_cases hab : a = b
+    · subst hab
+      rwa [sigma_mk_preimage_image_eq_self]
+    · rw [sigma_mk_preimage_image' hab]
+      exact MeasurableSet.empty
+
+section Nat
+
+variable {X : ℕ → Type*} [∀ n, MeasurableSpace (X n)] {M : ℕ}
+
+/-- The set of elements of `Σ n : ℕ, X n` with first component at most `M` is measurable. -/
+lemma measurableSet_sigma_fst_le (M : ℕ) : MeasurableSet {x : Σ n, X n | x.1 ≤ M} :=
+  measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iic M))
+
+/-- The set of elements of `Σ n : ℕ, X n` with first component less than `M` is measurable. -/
+lemma measurableSet_sigma_fst_lt (M : ℕ) : MeasurableSet {x : Σ n, X n | x.1 < M} :=
+  measurable_sigma_fst (MeasurableSet.of_discrete (s := Set.Iio M))
+
+/-- The image of a measure on `X (M + 1)` by `Sigma.mk (M + 1)` gives measure zero to the elements
+of `Σ n : ℕ, X n` with first component at most `M`. -/
+lemma MeasureTheory.Measure.map_sigmaMk_succ_apply_fst_le (μ : Measure (X (M + 1))) :
+    (μ.map (Sigma.mk (M + 1))) {x : Σ n, X n | x.1 ≤ M} = 0 := by
+  rw [Measure.map_apply (measurable_sigma_mk (M + 1)) (measurableSet_sigma_fst_le M)]
+  have : Sigma.mk (M + 1) ⁻¹' {x : Σ n, X n | x.1 ≤ M} = ∅ := by
+    ext x
+    simp
+  rw [this, measure_empty]
+
+end Nat
diff --git a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
index 93e9c492..99a6fd94 100644
--- a/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean
@@ -377,4 +377,44 @@ lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpa
   rw [Kernel.map_apply _ hf] at ha
   filter_upwards [hc, ha] with b hcb hab using hcb.trans hab
 
+/-- The restriction of `μ ⊗ₘ κ` to `s ×ˢ univ` is `μ.restrict s ⊗ₘ κ`. -/
+lemma _root_.MeasureTheory.Measure.restrict_compProd_prod_univ (μ : Measure α) [SFinite μ]
+    (κ : Kernel α β) [IsSFiniteKernel κ] {s : Set α} (hs : MeasurableSet s) :
+    (μ ⊗ₘ κ).restrict (s ×ˢ Set.univ) = μ.restrict s ⊗ₘ κ := by
+  ext t ht
+  rw [Measure.restrict_apply ht, Measure.compProd_apply (ht.inter (hs.prod MeasurableSet.univ)),
+    Measure.compProd_apply ht, ← lintegral_indicator hs]
+  refine lintegral_congr fun a ↦ ?_
+  by_cases ha : a ∈ s
+  · have : Prod.mk a ⁻¹' (t ∩ s ×ˢ Set.univ) = Prod.mk a ⁻¹' t := by ext b; simp [ha]
+    simp [Set.indicator, ha, this]
+  · have : Prod.mk a ⁻¹' (t ∩ s ×ˢ Set.univ) = ∅ := by ext b; simp [ha]
+    simp [Set.indicator, ha, this]
+
+omit [StandardBorelSpace Ω] [Nonempty Ω] in
+/-- A conditional law given `X` is a conditional law given `X` under the restriction of `P` to an
+event determined by `X`. -/
+lemma HasCondDistrib.restrict_preimage [SFinite μ] [IsSFiniteKernel κ]
+    (hX : Measurable X) (hY : Measurable Y)
+    (h : HasCondDistrib Y X κ μ) {s : Set β} (hs : MeasurableSet s) :
+    HasCondDistrib Y X κ (μ.restrict (X ⁻¹' s)) := by
+  refine ⟨(hX.prodMk hY).aemeasurable, ?_⟩
+  have h1 : (fun ω ↦ (X ω, Y ω)) ⁻¹' (s ×ˢ Set.univ) = X ⁻¹' s := by ext; simp
+  calc (μ.restrict (X ⁻¹' s)).map (fun ω ↦ (X ω, Y ω))
+      = (μ.map (fun ω ↦ (X ω, Y ω))).restrict (s ×ˢ Set.univ) := by
+        rw [Measure.restrict_map (hX.prodMk hY) (hs.prod MeasurableSet.univ), h1]
+    _ = (μ.map X ⊗ₘ κ).restrict (s ×ˢ Set.univ) := by rw [h.map_eq]
+    _ = (μ.map X).restrict s ⊗ₘ κ := Measure.restrict_compProd_prod_univ _ _ hs
+    _ = (μ.restrict (X ⁻¹' s)).map X ⊗ₘ κ := by rw [Measure.restrict_map hX hs]
+
+omit [StandardBorelSpace Ω] [Nonempty Ω] in
+/-- A conditional law given `X` is a conditional law given `X` under the restriction of `P` to an
+event determined by `X`, that is, measurable for the σ-algebra generated by `X`. -/
+lemma HasCondDistrib.restrict_of_measurableSet_comap [SFinite μ] [IsSFiniteKernel κ]
+    (hX : Measurable X) (hY : Measurable Y)
+    (h : HasCondDistrib Y X κ μ) {s : Set α} (hs : MeasurableSet[mβ.comap X] s) :
+    HasCondDistrib Y X κ (μ.restrict s) := by
+  obtain ⟨t, ht, rfl⟩ := MeasurableSpace.measurableSet_comap.1 hs
+  exact h.restrict_preimage hX hY ht
+
 end ProbabilityTheory
diff --git a/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean b/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean
index b8c69102..7e333267 100644
--- a/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/HasLaw.lean
@@ -29,6 +29,38 @@ lemma _root_.AEMeasurable.hasLaw_map {X : Ω → 𝓧} (hX : AEMeasurable X P) :
 lemma _root_.Measurable.hasLaw_map {X : Ω → 𝓧} (hX : Measurable X) (P : Measure Ω) :
     HasLaw X (P.map X) P := ⟨hX.aemeasurable, rfl⟩
 
+section Restrict
+
+variable {X : Ω → 𝓧} {μ ν : Measure 𝓧}
+
+/-- If a random variable with law `μ` almost surely does not belong to a measurable set `T`, then
+`μ T = 0`. -/
+lemma HasLaw.measure_eq_zero_of_ae_notMem (h : HasLaw X μ P) {T : Set 𝓧} (hT : MeasurableSet T)
+    (hXT : ∀ᵐ ω ∂P, X ω ∉ T) :
+    μ T = 0 := by
+  rw [← h.map_eq, Measure.map_apply_of_aemeasurable h.aemeasurable hT,
+    measure_eq_zero_iff_ae_notMem]
+  exact hXT
+
+/-- If `X` has law `μ` under the restriction of `P` to a measurable set `s` and law `ν` under the
+restriction of `P` to `sᶜ`, then `X` has law `μ + ν` under `P`. -/
+lemma HasLaw.add_of_restrict_compl {s : Set Ω} (hs : MeasurableSet s)
+    (hμ : HasLaw X μ (P.restrict s)) (hν : HasLaw X ν (P.restrict sᶜ)) :
+    HasLaw X (μ + ν) P := by
+  have hX : AEMeasurable X P := by
+    rw [← Measure.restrict_add_restrict_compl (μ := P) hs, aemeasurable_add_measure_iff]
+    exact ⟨hμ.aemeasurable, hν.aemeasurable⟩
+  refine ⟨hX, ?_⟩
+  calc P.map X = (P.restrict s + P.restrict sᶜ).map (hX.mk X) := by
+        rw [Measure.restrict_add_restrict_compl hs, Measure.map_congr hX.ae_eq_mk]
+    _ = (P.restrict s).map X + (P.restrict sᶜ).map X := by
+        rw [Measure.map_add _ _ hX.measurable_mk,
+          Measure.map_congr (ae_restrict_of_ae (s := s) hX.ae_eq_mk),
+          Measure.map_congr (ae_restrict_of_ae (s := sᶜ) hX.ae_eq_mk)]
+    _ = μ + ν := by rw [hμ.map_eq, hν.map_eq]
+
+end Restrict
+
 section Cond
 
 variable {ι : Type*} [Countable ι] {mι : MeasurableSpace ι} [MeasurableSingletonClass ι]
diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean
new file mode 100644
index 00000000..373f7b64
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/Sigma.lean
@@ -0,0 +1,44 @@
+/-
+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 LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma
+public import Mathlib.Probability.Kernel.Composition.MapComap
+
+/-!
+# Kernels on a sigma type
+
+`Kernel.sigma κ` is the kernel on `Σ a, β a` which is `κ a` on the fiber `β a`.
+-/
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace ProbabilityTheory.Kernel
+
+variable {α γ : Type*} {β : α → Type*} [∀ a, MeasurableSpace (β a)] {mγ : MeasurableSpace γ}
+
+/-- The kernel on `Σ a, β a` which is `κ a` on the fiber `β a`. -/
+def sigma (κ : (a : α) → Kernel (β a) γ) : Kernel (Σ a, β a) γ where
+  toFun x := κ x.1 x.2
+  measurable' := measurable_sigma_of_measurable_comp_mk fun a ↦ (κ a).measurable
+
+@[simp]
+lemma sigma_apply (κ : (a : α) → Kernel (β a) γ) (x : Σ a, β a) : sigma κ x = κ x.1 x.2 := rfl
+
+lemma sigma_apply_mk (κ : (a : α) → Kernel (β a) γ) (a : α) (b : β a) :
+    sigma κ ⟨a, b⟩ = κ a b := rfl
+
+lemma comap_sigma_mk (κ : (a : α) → Kernel (β a) γ) (a : α) :
+    (sigma κ).comap (Sigma.mk a) (measurable_sigma_mk a) = κ a := by
+  ext b : 1
+  rw [comap_apply, sigma_apply_mk]
+
+instance (κ : (a : α) → Kernel (β a) γ) [∀ a, IsMarkovKernel (κ a)] : IsMarkovKernel (sigma κ) :=
+  ⟨fun x ↦ (IsMarkovKernel.isProbabilityMeasure (κ := κ x.1) x.2)⟩
+
+end ProbabilityTheory.Kernel
diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index bfd28276..6c09c653 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -305,6 +305,18 @@ lemma history_succ (n : ℕ) :
   · simp [history, step]
   · simp [history]
 
+/-- If the history of the first `n` rounds has law `μ` and the round at time `n` has conditional
+law `κ` given this history, then the history of the first `n + 1` rounds has law the image of
+`μ ⊗ₘ κ` by the identification of `Hist 𝓞 𝓐 𝓨 n × Round 𝓞 𝓐 𝓨` with `Hist 𝓞 𝓐 𝓨 (n + 1)`. -/
+lemma hasLaw_history_succ {P : Measure Ω} {n : ℕ} {μ : Measure (Hist 𝓞 𝓐 𝓨 n)}
+    {κ : Kernel (Hist 𝓞 𝓐 𝓨 n) (Round 𝓞 𝓐 𝓨)}
+    (hμ : HasLaw (history O A Y n) μ P) (hκ : HasCondDistrib (step O A Y n) (history O A Y n) κ P) :
+    HasLaw (history O A Y (n + 1))
+      ((μ ⊗ₘ κ).map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) n).symm) P := by
+  rw [history_succ]
+  exact (hasLaw_map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) n).symm.measurable.aemeasurable).comp
+    (hμ.prodMk_of_hasCondDistrib hκ)
+
 /-- An algorithm-environment sequence: a sequence of observations, actions and feedbacks generated
 by an algorithm interacting with an environment. -/
 structure IsAlgEnvSeq
diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
index 66784d36..8fa01ae2 100644
--- a/LeanMachineLearning/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -39,6 +39,8 @@ measurable functions.
   The initial action is `fun o ↦ nextA 0 (default, o)`.
 * `detEnvironment obs f hf`: a deterministic environment with observation kernels `obs`, that gives
   feedback according to the measurable function `f` (with proof of measurability `hf`).
+* `fixedDesignAlg x`: the deterministic algorithm that plays the fixed sequence of actions `x`,
+  whatever the history and the observations (a *fixed design*).
 
 -/
 
@@ -266,6 +268,20 @@ lemma actionZero_detAlgorithm [MeasurableSpace.SeparatesPoints 𝓐] :
   unfold actionZero
   rw [nextAction_detAlgorithm]
 
+/-- The deterministic algorithm that plays the fixed sequence of actions `x : ℕ → 𝓐`, whatever
+the history and the observations (a *fixed design*). -/
+noncomputable def fixedDesignAlg (x : ℕ → 𝓐) : Algorithm 𝓞 𝓐 𝓨 :=
+  detAlgorithm (fun n _ ↦ x n) fun _ ↦ measurable_const
+
+@[simp]
+lemma fixedDesignAlg_policy (x : ℕ → 𝓐) (n : ℕ) :
+    (fixedDesignAlg (𝓞 := 𝓞) (𝓨 := 𝓨) x).policy n =
+      Kernel.deterministic (fun _ ↦ x n) measurable_const := rfl
+
+instance (x : ℕ → 𝓐) :
+    IsDeterministicAlg (fixedDesignAlg (m𝓞 := m𝓞) (m𝓐 := m𝓐) (m𝓨 := m𝓨) x) :=
+  inferInstanceAs (IsDeterministicAlg (detAlgorithm _ _))
+
 /-- A deterministic environment, where the feedback is given by evaluating
 fixed measurable functions. -/
 noncomputable def detEnvironment (obs : (n : ℕ) → Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞)
diff --git a/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean
new file mode 100644
index 00000000..d12fba26
--- /dev/null
+++ b/LeanMachineLearning/SequentialLearning/IdentificationAlg.lean
@@ -0,0 +1,237 @@
+/-
+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 LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma
+public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.StoppedHistory
+
+/-!
+# Identification algorithms: sampling rule, stopping rule, output rule
+
+An *identification algorithm* `A : IdentAlg 𝓞 𝓐 𝓨 𝓓` with outputs in `𝓓` is a sampling rule
+`A.alg : Algorithm 𝓞 𝓐 𝓨` together with
+
+* a *stopping rule* `A.stopSet`, a measurable set of histories of variable length: the algorithm
+  stops after `n` rounds if the history of these `n` rounds belongs to `A.stopSet`;
+* an *output rule* `A.output`, a Markov kernel from histories of variable length to `𝓓`: the
+  distribution of the output given the history of the rounds played.
+
+A *run* of the algorithm in an environment `env`, on a probability space `(Ω, P)`, consists of
+observation, action and feedback processes `O, X, Y` forming an algorithm-environment sequence
+for `A.alg` and `env` (`IsAlgEnvSeq`) and an output `out : Ω → 𝓓` whose conditional law given the
+history at the stopping time is the output rule (`IdentAlg.IsRun`). The stopping time
+`IdentAlg.stoppingTime A O X Y` is the stopping time `Learning.stoppingTime` of the stopping rule
+`A.stopSet` (the hitting time, Mathlib `hittingAfter`, of the stopping rule by the process of
+histories), a stopping time of the history filtration, and the history at the stopping time is
+`IdentAlg.stoppedHist A O X Y` (`Learning.stoppedHist`, the stopped value of the process of
+histories). If the algorithm never stops, the history at the stopping time is the history of an
+arbitrary, unspecified number of rounds, and the output is then drawn from the output rule at that
+history.
+
+The law of the output of a run is determined by `A` and `env`: it is `A.outputMeasure env`, the
+law of the output on the canonical probability space of the interaction (`trajMeasure`), see
+`IdentAlg.IsRun.hasLaw_output`. Properties of the algorithm are stated in terms of this law: `A`
+is *PAC at level `δ`* (`IdentAlg.IsPAC`) for a family of environments `env θ` and a goodness
+predicate `good θ` if, for every `θ`, the output in `env θ` is `good θ` with probability at least
+`1 - δ`. `IdentAlg.IsPAC.measureReal_good_of_isRun` transfers this bound to any run of `A`.
+
+Examples: best-arm identification (`𝓓 = 𝓐`, output = recommended arm), hypothesis tests
+(`𝓓 = Bool`), estimation (`𝓓 = ℝ`).
+
+A *fixed-budget* algorithm is the special case where the stopping rule is "stop after exactly
+`T` rounds" (`IsFixedBudget A T`; constructor `fixedBudget alg T ρ`); a *fixed-confidence*
+algorithm stops adaptively. A *fixed-design* algorithm (`IsFixedDesign A`) is one whose sampling
+rule plays a fixed sequence of actions (`fixedDesignAlg x`).
+
+## Main definitions
+
+* `IdentAlg 𝓞 𝓐 𝓨 𝓓`: the structure.
+* `IdentAlg.stoppingTime A O X Y : Ω → ℕ∞`: the number of rounds played, a hitting time.
+* `IdentAlg.stoppedHist A O X Y : Ω → Σ n, Hist 𝓞 𝓐 𝓨 n`: the history at the stopping time.
+* `IdentAlg.IsRun A env O X Y out P`: `(O, X, Y, out)` is a run of `A` in `env` on `(Ω, P)`.
+* `IdentAlg.outputMeasure A env : Measure 𝓓`: the law of the output of `A` in `env`.
+* `IdentAlg.IsPAC A env good δ`: for every parameter `θ`, the output of `A` in `env θ` is
+  `good θ` with probability at least `1 - δ`.
+* `IdentAlg.IsFixedBudget A T`, `IdentAlg.fixedBudget alg T ρ`: fixed-budget algorithms.
+* `IdentAlg.IsFixedDesign A`: the sampling rule of `A` is `fixedDesignAlg x` for some `x`.
+
+Time is `0`-indexed: after `n` rounds the actions `a_0, …, a_{n-1}` have been played.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory
+
+open scoped ENat
+
+namespace Learning
+
+variable {𝓞 𝓐 𝓨 𝓓 Ω : Type*} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐}
+  {m𝓨 : MeasurableSpace 𝓨} {m𝓓 : MeasurableSpace 𝓓} {mΩ : MeasurableSpace Ω}
+
+/-- An identification algorithm with outputs in `𝓓`: a sampling rule `alg`, a stopping rule
+`stopSet` (the algorithm stops after `n` rounds if the history of these rounds, as a history of
+variable length, belongs to `stopSet`) and an output rule `output`, a Markov kernel giving the
+distribution of the output given the history of the rounds played. -/
+structure IdentAlg (𝓞 𝓐 𝓨 𝓓 : Type*) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐]
+    [MeasurableSpace 𝓨] [MeasurableSpace 𝓓] where
+  /-- The sampling rule. -/
+  alg : Algorithm 𝓞 𝓐 𝓨
+  /-- The stopping rule: the algorithm stops after `n` rounds if the history of these rounds
+  belongs to `stopSet`. -/
+  stopSet : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)
+  /-- The stopping rule is measurable. -/
+  measurableSet_stopSet : MeasurableSet stopSet
+  /-- The output rule: distribution of the output given the history of the rounds played. -/
+  output : Kernel (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) 𝓓
+  /-- The output rule is a Markov kernel. -/
+  [isMarkovKernel_output : IsMarkovKernel output]
+
+namespace IdentAlg
+
+variable (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
+
+instance : IsMarkovKernel A.output := A.isMarkovKernel_output
+
+/-- The stopping time of `A` on the observation, action and feedback processes `O`, `X`, `Y`: the
+number of rounds played, that is the first `n` such that the history of the first `n` rounds
+belongs to the stopping rule `A.stopSet` (`⊤` if there is none). -/
+noncomputable def stoppingTime : Ω → ℕ∞ := Learning.stoppingTime O X Y A.stopSet
+
+lemma stoppingTime_def : A.stoppingTime O X Y = Learning.stoppingTime O X Y A.stopSet := rfl
+
+/-- The history of the rounds played by `A`, as a history of variable length: the history stopped
+at `A.stoppingTime O X Y` (the history of an arbitrary number of rounds if `A` never stops). -/
+noncomputable def stoppedHist : Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n :=
+  Learning.stoppedHist O X Y (A.stoppingTime O X Y)
+
+lemma stoppedHist_def :
+    A.stoppedHist O X Y = Learning.stoppedHist O X Y (A.stoppingTime O X Y) := rfl
+
+/-- The law of the output of `A` in the environment `env`: the output rule applied to the law of
+the history at the stopping time. This is the law of the output of any run of `A` in `env`
+(`IsRun.hasLaw_output`). -/
+noncomputable def outputMeasure (env : Environment 𝓞 𝓐 𝓨) : Measure 𝓓 :=
+  A.output ∘ₘ stoppedHistMeasure A.alg env A.stopSet
+
+instance (env : Environment 𝓞 𝓐 𝓨) : IsProbabilityMeasure (A.outputMeasure env) := by
+  unfold outputMeasure
+  infer_instance
+
+/-- `(O, X, Y, out)` is a *run* of the identification algorithm `A` in the environment `env` on
+the probability space `(Ω, P)`: the observation, action and feedback processes `O`, `X`, `Y` form
+an algorithm-environment sequence for the sampling rule `A.alg` and `env`, and the output `out` has
+conditional law `A.output` given the history at the stopping time (the history of an arbitrary
+number of rounds if `A` never stops). -/
+structure IsRun (env : Environment 𝓞 𝓐 𝓨) (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
+    (out : Ω → 𝓓) (P : Measure Ω) [IsFiniteMeasure P] : Prop where
+  /-- The actions and feedbacks are generated by the sampling rule in the environment. -/
+  isAlgEnvSeq : IsAlgEnvSeq O X Y A.alg env P
+  /-- The output is drawn from the output rule applied to the history at the stopping time. -/
+  hasCondDistrib_output : HasCondDistrib out (A.stoppedHist O X Y) A.output P
+
+/-- `A` is *PAC at level `δ`* for the family of environments `env : Θ → Environment 𝓞 𝓐 𝓨` and
+the goodness predicate `good : Θ → 𝓓 → Prop` if, for every `θ`, the output of `A` in `env θ` is
+`good θ` with probability at least `1 - δ`. See `IsPAC.measureReal_good_of_isRun` for the
+corresponding statement about any run of `A`. -/
+def IsPAC {Θ : Type*} (env : Θ → Environment 𝓞 𝓐 𝓨) (good : Θ → 𝓓 → Prop) (δ : ℝ) : Prop :=
+  ∀ θ, 1 - δ ≤ (A.outputMeasure (env θ)).real {d | good θ d}
+
+/-- `A` is a *fixed-budget* algorithm with budget `T` if its stopping rule is "stop after exactly
+`T` rounds". -/
+def IsFixedBudget (T : ℕ) : Prop := A.stopSet = {h | h.1 = T}
+
+/-- `A` is a *fixed-design* algorithm if its sampling rule plays a fixed sequence of actions,
+whatever the history and the observations. -/
+def IsFixedDesign : Prop := ∃ x : ℕ → 𝓐, A.alg = fixedDesignAlg x
+
+variable {A O X Y} {env : Environment 𝓞 𝓐 𝓨} {out : Ω → 𝓓} {P : Measure Ω}
+
+/-- The stopping time of an identification algorithm is a stopping time of the history
+filtration of any algorithm-environment sequence `O`, `X`, `Y`. -/
+lemma isStoppingTime_stoppingTime (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) {alg : Algorithm 𝓞 𝓐 𝓨}
+    [IsFiniteMeasure P] (h : IsAlgEnvSeq O X Y alg env P) :
+    IsStoppingTime h.filtration (A.stoppingTime O X Y) :=
+  h.isStoppingTime_stoppingTime A.measurableSet_stopSet
+
+/-- When the stopping time is finite, the history at the stopping time belongs to the stopping
+rule. -/
+lemma stoppedHist_mem_stopSet_of_ne_top {ω : Ω} (h : A.stoppingTime O X Y ω ≠ ⊤) :
+    A.stoppedHist O X Y ω ∈ A.stopSet :=
+  Learning.stoppedHist_mem_of_ne_top h
+
+/-- The history at the stopping time of any run of `A` in `env` has law
+`stoppedHistMeasure A.alg env A.stopSet`. -/
+lemma IsRun.hasLaw_stoppedHist [IsProbabilityMeasure P] (h : A.IsRun env O X Y out P) :
+    HasLaw (A.stoppedHist O X Y) (stoppedHistMeasure A.alg env A.stopSet) P :=
+  h.isAlgEnvSeq.hasLaw_stoppedHist_stoppingTime A.measurableSet_stopSet
+
+/-- The output of any run of `A` in `env` has law `A.outputMeasure env`. -/
+lemma IsRun.hasLaw_output [IsProbabilityMeasure P] (h : A.IsRun env O X Y out P) :
+    HasLaw out (A.outputMeasure env) P := by
+  have h_comp := h.hasCondDistrib_output.hasLaw_comp
+  rw [h.hasLaw_stoppedHist.map_eq] at h_comp
+  exact h_comp
+
+/-- For a PAC algorithm at level `δ`, the output of any run in `env θ` is `good θ` with
+probability at least `1 - δ`. -/
+lemma IsPAC.measureReal_good_of_isRun {Θ : Type*} {env : Θ → Environment 𝓞 𝓐 𝓨}
+    {good : Θ → 𝓓 → Prop} {δ : ℝ} (hA : A.IsPAC env good δ) {θ : Θ}
+    (hgood : MeasurableSet {d | good θ d}) [IsProbabilityMeasure P]
+    (h : A.IsRun (env θ) O X Y out P) :
+    1 - δ ≤ P.real {ω | good θ (out ω)} := by
+  rw [h.hasLaw_output.measureReal_eq hgood]
+  exact hA θ
+
+section FixedBudget
+
+variable [Nonempty 𝓓] (alg : Algorithm 𝓞 𝓐 𝓨) (T : ℕ) (ρ : Kernel (Hist 𝓞 𝓐 𝓨 T) 𝓓)
+  [IsMarkovKernel ρ]
+
+/-- The output rule of a fixed-budget algorithm with output kernel `ρ` on histories of length
+`T`: `ρ` on histories of length `T`, an arbitrary constant (never used) on other lengths. -/
+noncomputable def fixedBudgetOutput (n : ℕ) : Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓓 :=
+  if h : n = T then ρ.comap (fun x i ↦ x (Fin.cast h.symm i)) (by fun_prop)
+  else Kernel.const _ (Measure.dirac (Classical.arbitrary 𝓓))
+
+instance (n : ℕ) : IsMarkovKernel (fixedBudgetOutput T ρ n) := by
+  unfold fixedBudgetOutput
+  by_cases h : n = T <;> simp only [h, ↓reduceDIte] <;> infer_instance
+
+omit [IsMarkovKernel ρ] in
+@[simp]
+lemma fixedBudgetOutput_self : fixedBudgetOutput T ρ T = ρ := by
+  simp only [fixedBudgetOutput, ↓reduceDIte, Fin.cast_eq_self]
+  ext y u _
+  simp
+
+/-- The fixed-budget identification algorithm with sampling rule `alg`, budget `T` and output
+kernel `ρ` on histories of length `T`. -/
+noncomputable def fixedBudget : IdentAlg 𝓞 𝓐 𝓨 𝓓 where
+  alg := alg
+  stopSet := {h | h.1 = T}
+  measurableSet_stopSet := measurable_sigma_fst (MeasurableSet.of_discrete (s := {T}))
+  output := Kernel.sigma (fixedBudgetOutput T ρ)
+
+@[simp] lemma alg_fixedBudget : (fixedBudget alg T ρ).alg = alg := rfl
+
+@[simp] lemma stopSet_fixedBudget : (fixedBudget alg T ρ).stopSet = {h | h.1 = T} := rfl
+
+@[simp] lemma output_fixedBudget :
+    (fixedBudget alg T ρ).output = Kernel.sigma (fixedBudgetOutput T ρ) := rfl
+
+lemma isFixedBudget_fixedBudget : (fixedBudget alg T ρ).IsFixedBudget T := rfl
+
+/-- The output rule of `fixedBudget alg T ρ` on a history of length `T` is `ρ`. -/
+lemma output_fixedBudget_mk (h : Hist 𝓞 𝓐 𝓨 T) : (fixedBudget alg T ρ).output ⟨T, h⟩ = ρ h := by
+  simp
+
+end FixedBudget
+
+end IdentAlg
+
+end Learning
diff --git a/LeanMachineLearning/SequentialLearning/StoppedHistory.lean b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean
new file mode 100644
index 00000000..c7f6fa39
--- /dev/null
+++ b/LeanMachineLearning/SequentialLearning/StoppedHistory.lean
@@ -0,0 +1,429 @@
+/-
+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 LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma
+public import LeanMachineLearning.ForMathlib.Probability.HasLaw
+public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+public import Mathlib.Probability.Process.HittingTime
+
+/-!
+# Stopping rules, stopping times and stopped histories
+
+A *stopping rule* is a measurable set `S : Set (Σ n, Hist 𝓞 𝓐 𝓨 n)` of histories of variable
+length: the interaction stops after `n` rounds if the history of these `n` rounds belongs to
+`S`. Its *stopping time* `stoppingTime O X Y S : Ω → ℕ∞` is the number of rounds played, the
+hitting time (Mathlib `hittingAfter`) of `S` by the process `sigmaHistory O X Y` of the histories
+seen as histories of variable length. For a random time `τ : Ω → ℕ∞`, `stoppedHist O X Y τ` is
+the history of the first `τ` rounds, as a history of variable length: the stopped value (Mathlib
+`stoppedValue`) of the process `sigmaHistory O X Y` at `τ` (when `τ = ⊤`, this is the history of
+an arbitrary, unspecified number of rounds). The history of the first `min τ M` rounds is the
+stopped process (Mathlib `stoppedProcess`) `stoppedProcess (sigmaHistory O X Y) τ M`.
+
+* `stoppingTime_le_iff`, `lt_stoppingTime_iff`, `stoppingTime_eq_coe_iff`,
+  `stoppingTime_eq_top_iff`: characterizations of the stopping time;
+* `stoppedHist_mem_of_ne_top`: the stopped history belongs to `S` when the stopping time is
+  finite; `notMem_of_lt_stoppingTime`: the history of `n < τ` rounds does not;
+* `measurable_stoppingTime`, `measurable_stoppedHist`;
+* `measurableSet_comap_history_lt_stoppingTime`, `measurableSet_comap_history_stoppingTime_le`:
+  the events `{n < stoppingTime O X Y S}` and `{stoppingTime O X Y S ≤ n}` are determined by the
+  first `n` rounds; `IsAlgEnvSeq.isStoppingTime_stoppingTime`: `stoppingTime O X Y S` is a
+  stopping time of the history filtration of an algorithm-environment sequence;
+* `hasLaw_stoppedProcess_sigmaHistory_add`, `hasLaw_stoppedProcess_sigmaHistory_succ_add`: the
+  laws of the histories stopped at `min τ M` and `min τ (M + 1)` split according to whether
+  `τ ≤ M`;
+* `IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime` (and `obs`, `action`, `feedback`):
+  on the event `{M < τ}`, which is determined by the first `M` rounds, the round at time `M` keeps
+  its conditional laws; `IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime`: on this
+  event, the law of the first `M + 1` rounds is the composition-product of the law of the first
+  `M` rounds with the step kernel;
+* `stoppedHistMeasure alg env S`, `IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime`: the law of the
+  history stopped by `S` is determined by the algorithm and the environment.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Finset
+
+open scoped ENat
+
+namespace Learning
+
+variable {𝓞 𝓐 𝓨 Ω : Type*} {mΩ : MeasurableSpace Ω}
+
+/-- The history of the first `n` rounds, as a history of variable length: the process
+`n ↦ ⟨n, history O X Y n⟩`, of which the stopping time of a stopping rule is a hitting time. -/
+def sigmaHistory (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) :
+    Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n :=
+  ⟨n, history O X Y n ω⟩
+
+/-- The stopping time of the stopping rule `S` on the observation, action and feedback processes
+`O`, `X`, `Y`: the number of rounds played, that is the first `n` such that the history of the
+first `n` rounds belongs to `S` (`⊤` if there is none). -/
+noncomputable def stoppingTime (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
+    (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) : Ω → ℕ∞ :=
+  hittingAfter (sigmaHistory O X Y) S 0
+
+/-- The history of the first `τ ω` rounds, as a history of variable length: the stopped value of
+the process `sigmaHistory O X Y` at the random time `τ`. When `τ ω = ⊤`, this is the history of an
+arbitrary, unspecified number of rounds. -/
+noncomputable def stoppedHist (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (τ : Ω → ℕ∞) :
+    Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n :=
+  stoppedValue (sigmaHistory O X Y) τ
+
+variable {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)}
+  {τ : Ω → ℕ∞} {ω : Ω} {n M : ℕ}
+
+lemma sigmaHistory_apply (n : ℕ) (ω : Ω) :
+    sigmaHistory O X Y n ω = ⟨n, history O X Y n ω⟩ := rfl
+
+lemma fst_sigmaHistory (n : ℕ) (ω : Ω) : (sigmaHistory O X Y n ω).1 = n := rfl
+
+lemma stoppedHist_def (τ : Ω → ℕ∞) :
+    stoppedHist O X Y τ = stoppedValue (sigmaHistory O X Y) τ := rfl
+
+section stoppingTime
+
+lemma stoppingTime_le_iff :
+    stoppingTime O X Y S ω ≤ n ↔ ∃ j ≤ n, sigmaHistory O X Y j ω ∈ S :=
+  (hittingAfter_le_iff (u := sigmaHistory O X Y) (s := S) (n := 0) (i := n) (ω := ω)).trans
+    (by simp)
+
+lemma lt_stoppingTime_iff :
+    (n : ℕ∞) < stoppingTime O X Y S ω ↔ ∀ j ≤ n, sigmaHistory O X Y j ω ∉ S := by
+  rw [← not_le, stoppingTime_le_iff]
+  simp
+
+lemma stoppingTime_eq_top_iff :
+    stoppingTime O X Y S ω = ⊤ ↔ ∀ n, sigmaHistory O X Y n ω ∉ S :=
+  (hittingAfter_eq_top_iff (u := sigmaHistory O X Y) (s := S) (n := 0) (ω := ω)).trans (by simp)
+
+lemma notMem_of_lt_stoppingTime (h : (n : ℕ∞) < stoppingTime O X Y S ω) :
+    sigmaHistory O X Y n ω ∉ S :=
+  notMem_of_lt_hittingAfter h (Nat.zero_le n)
+
+lemma stoppingTime_eq_coe_iff :
+    stoppingTime O X Y S ω = n ↔
+      sigmaHistory O X Y n ω ∈ S ∧ ∀ j < n, sigmaHistory O X Y j ω ∉ S := by
+  constructor
+  · intro h
+    refine ⟨?_, fun j hj ↦ notMem_of_lt_stoppingTime (h ▸ ENat.natCast_lt_natCast.2 hj)⟩
+    obtain ⟨j, hjn, hjS⟩ := stoppingTime_le_iff.1 h.le
+    rcases hjn.lt_or_eq with hjn | rfl
+    · exact absurd hjS (notMem_of_lt_stoppingTime (h ▸ ENat.natCast_lt_natCast.2 hjn))
+    · exact hjS
+  · rintro ⟨h1, h2⟩
+    refine le_antisymm (hittingAfter_le_of_mem (Nat.zero_le n) h1) (not_lt.1 fun hlt ↦ ?_)
+    obtain ⟨j, hj, hjS⟩ := hittingAfter_lt_iff.1 hlt
+    exact h2 j hj.2 hjS
+
+/-- The empty stopping rule never stops. -/
+lemma stoppingTime_empty : stoppingTime O X Y (∅ : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) = fun _ ↦ ⊤ :=
+  hittingAfter_empty 0
+
+lemma stoppedHist_congr (τ τ' : Ω → ℕ∞) (h : τ ω = τ' ω) :
+    stoppedHist O X Y τ ω = stoppedHist O X Y τ' ω := by
+  simp only [stoppedHist, stoppedValue, h]
+
+lemma stoppedHist_coe (M : ℕ) (ω : Ω) :
+    stoppedHist O X Y (fun _ ↦ (M : ℕ∞)) ω = sigmaHistory O X Y M ω := rfl
+
+/-- The stopped history belongs to the stopping rule when the stopping time is finite. -/
+lemma stoppedHist_mem_of_ne_top (h : stoppingTime O X Y S ω ≠ ⊤) :
+    stoppedHist O X Y (stoppingTime O X Y S) ω ∈ S :=
+  hittingAfter_mem_set_of_ne_top h
+
+/-! The history of the first `min τ M` rounds is `stoppedProcess (sigmaHistory O X Y) τ M`: it
+is the history of the first `M` rounds if `M ≤ τ` (`stoppedProcess_eq_of_le`) and the history
+stopped at `τ` otherwise (`stoppedProcess_eq_of_ge`). -/
+
+/-- The history of the first `min τ M` rounds has length at most `M`. -/
+lemma fst_stoppedProcess_sigmaHistory_le :
+    (stoppedProcess (sigmaHistory O X Y) τ M ω).1 ≤ M :=
+  (WithTop.untopA_le_iff (ne_top_of_le_ne_top (ENat.natCast_ne_top M) (min_le_left _ _))).2
+    (min_le_left _ _)
+
+/-- The history of the first `min τ 0` rounds is the empty history. -/
+lemma stoppedProcess_sigmaHistory_zero (τ : Ω → ℕ∞) :
+    stoppedProcess (sigmaHistory O X Y) τ 0 = fun _ ↦ ⟨0, default⟩ :=
+  funext fun ω ↦ (stoppedProcess_eq_of_le (zero_le : (0 : ℕ∞) ≤ τ ω)).trans
+    (congrArg (Sigma.mk 0) (Subsingleton.elim _ _))
+
+end stoppingTime
+
+section natCast
+
+omit mΩ in
+lemma compl_setOf_le_natCast (τ : Ω → ℕ∞) (M : ℕ) :
+    {ω | τ ω ≤ M}ᶜ = {ω | (M : ℕ∞) < τ ω} := by
+  ext ω
+  simp
+
+/-- Every subset of `ℕ∞` is measurable, hence so is `{τ ≤ M}` for a measurable `τ`. -/
+lemma measurableSet_le_natCast (hτ : Measurable τ) (M : ℕ) : MeasurableSet {ω | τ ω ≤ M} :=
+  hτ (MeasurableSet.of_discrete (s := Set.Iic (M : ℕ∞)))
+
+lemma measurableSet_natCast_lt (hτ : Measurable τ) (M : ℕ) :
+    MeasurableSet {ω | (M : ℕ∞) < τ ω} :=
+  hτ (MeasurableSet.of_discrete (s := Set.Ioi (M : ℕ∞)))
+
+end natCast
+
+variable {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
+
+/-- The history of the first `min τ 0` rounds has law the Dirac mass at the empty history. -/
+lemma hasLaw_stoppedProcess_sigmaHistory_zero (P : Measure Ω) [IsProbabilityMeasure P]
+    (τ : Ω → ℕ∞) :
+    HasLaw (stoppedProcess (sigmaHistory O X Y) τ 0)
+      (Measure.dirac (⟨0, default⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) P := by
+  rw [stoppedProcess_sigmaHistory_zero]
+  exact hasLaw_dirac_of_ae_eq (ae_eq_refl _)
+
+section measurability
+
+variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n))
+include hO hX hY
+
+lemma measurable_sigmaHistory (n : ℕ) : Measurable (sigmaHistory O X Y n) :=
+  (measurable_sigma_mk n).comp (measurable_history hO hX hY n)
+
+lemma measurable_stoppingTime (hS : MeasurableSet S) : Measurable (stoppingTime O X Y S) := by
+  refine measurable_to_countable' fun x ↦ ?_
+  induction x using ENat.recTopCoe with
+  | top =>
+    have : stoppingTime O X Y S ⁻¹' {⊤} = ⋂ n, sigmaHistory O X Y n ⁻¹' Sᶜ := by
+      ext ω
+      simp [stoppingTime_eq_top_iff]
+    rw [this]
+    exact MeasurableSet.iInter fun n ↦ measurable_sigmaHistory hO hX hY n hS.compl
+  | coe n =>
+    have : stoppingTime O X Y S ⁻¹' {(n : ℕ∞)} =
+        sigmaHistory O X Y n ⁻¹' S ∩ ⋂ j < n, sigmaHistory O X Y j ⁻¹' Sᶜ := by
+      ext ω
+      simp [stoppingTime_eq_coe_iff]
+    rw [this]
+    exact (measurable_sigmaHistory hO hX hY n hS).inter
+      (MeasurableSet.biInter (Set.to_countable _) fun j _ ↦
+        measurable_sigmaHistory hO hX hY j hS.compl)
+
+lemma measurable_stoppedHist (hτ : Measurable τ) : Measurable (stoppedHist O X Y τ) :=
+  Measurable.sigmaMk (measurable_from_top.comp hτ) (measurable_history hO hX hY)
+
+lemma measurable_stoppedProcess_sigmaHistory (hτ : Measurable τ) (M : ℕ) :
+    Measurable (stoppedProcess (sigmaHistory O X Y) τ M) :=
+  measurable_stoppedHist hO hX hY
+    ((measurable_from_top (f := fun t : ℕ∞ ↦ min (M : ℕ∞) t)).comp hτ)
+
+end measurability
+
+section comap
+
+/-- The event `{n < stoppingTime O X Y S}` is determined by the history of the first `n` rounds:
+it is measurable for the σ-algebra generated by `history O X Y n`. -/
+lemma measurableSet_comap_history_lt_stoppingTime (hS : MeasurableSet S) (n : ℕ) :
+    MeasurableSet[MeasurableSpace.comap (history O X Y n) inferInstance]
+      {ω | (n : ℕ∞) < stoppingTime O X Y S ω} := by
+  refine MeasurableSpace.measurableSet_comap.2 ⟨⋂ j, ⋂ (hj : j ≤ n),
+    {h | (⟨j, fun i ↦ h (Fin.castLE hj i)⟩ : Σ n, Hist 𝓞 𝓐 𝓨 n) ∉ S}, ?_, ?_⟩
+  · refine MeasurableSet.iInter fun j ↦ MeasurableSet.iInter fun hj ↦ ?_
+    exact ((measurable_sigma_mk j).comp (Measurable.of_eval fun _ ↦ measurable_pi_apply _))
+      hS.compl
+  · ext ω
+    simp only [Set.mem_preimage, Set.mem_iInter, Set.mem_ofPred_eq, lt_stoppingTime_iff]
+    exact ⟨fun h j hj ↦ h j hj, fun h j hj ↦ h j hj⟩
+
+/-- The event `{stoppingTime O X Y S ≤ n}` is determined by the history of the first `n`
+rounds: it is measurable for the σ-algebra generated by `history O X Y n`. -/
+lemma measurableSet_comap_history_stoppingTime_le (hS : MeasurableSet S) (n : ℕ) :
+    MeasurableSet[MeasurableSpace.comap (history O X Y n) inferInstance]
+      {ω | stoppingTime O X Y S ω ≤ n} := by
+  rw [← compl_compl {ω | stoppingTime O X Y S ω ≤ n}, compl_setOf_le_natCast]
+  exact (measurableSet_comap_history_lt_stoppingTime hS n).compl
+
+end comap
+
+section law
+
+variable {P : Measure Ω}
+
+/-- The law of the history of the first `min τ M` rounds splits according to whether `τ ≤ M`:
+on `{τ ≤ M}` it is the law of the history stopped at `τ` (or equivalently of the first `min τ M`
+rounds), on `{M < τ}` it is the law of the history of the first `M` rounds. -/
+lemma hasLaw_stoppedProcess_sigmaHistory_add (hτ : Measurable τ)
+    {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {ν : Measure (Hist 𝓞 𝓐 𝓨 M)}
+    (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) μ (P.restrict {ω | τ ω ≤ M}))
+    (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < τ ω})) :
+    HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) (μ + ν.map (Sigma.mk M)) P := by
+  refine hμ.add_of_restrict_compl (measurableSet_le_natCast hτ M) ?_
+  rw [compl_setOf_le_natCast]
+  refine (((measurable_sigma_mk M).hasLaw_map ν).comp hν).congr
+    ((ae_restrict_iff' (measurableSet_natCast_lt hτ M)).2
+      (Filter.Eventually.of_forall fun ω hω ↦ ?_))
+  exact stoppedProcess_eq_of_le hω.le
+
+/-- The law of the history of the first `min τ (M + 1)` rounds splits according to whether
+`τ ≤ M`: on `{τ ≤ M}` it is the law of the history of the first `min τ M` rounds, on `{M < τ}` it
+is the law of the history of the first `M + 1` rounds. -/
+lemma hasLaw_stoppedProcess_sigmaHistory_succ_add (hτ : Measurable τ)
+    {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} {ν : Measure (Hist 𝓞 𝓐 𝓨 (M + 1))}
+    (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) μ (P.restrict {ω | τ ω ≤ M}))
+    (hν : HasLaw (history O X Y (M + 1)) ν (P.restrict {ω | (M : ℕ∞) < τ ω})) :
+    HasLaw (stoppedProcess (sigmaHistory O X Y) τ (M + 1)) (μ + ν.map (Sigma.mk (M + 1))) P := by
+  refine HasLaw.add_of_restrict_compl (measurableSet_le_natCast hτ M) ?_ ?_
+  · refine hμ.congr ((ae_restrict_iff' (measurableSet_le_natCast hτ M)).2
+      (Filter.Eventually.of_forall fun ω hω ↦ ?_))
+    rw [stoppedProcess_eq_of_ge hω, stoppedProcess_eq_of_ge
+      (hω.trans (by exact_mod_cast M.le_succ : (M : ℕ∞) ≤ ((M + 1 : ℕ) : ℕ∞)))]
+  · rw [compl_setOf_le_natCast]
+    refine (((measurable_sigma_mk (M + 1)).hasLaw_map ν).comp hν).congr
+      ((ae_restrict_iff' (measurableSet_natCast_lt hτ M)).2
+        (Filter.Eventually.of_forall fun ω hω ↦ ?_))
+    have hω' : (M : ℕ∞) < τ ω := hω
+    have h_succ : ((M + 1 : ℕ) : ℕ∞) ≤ τ ω := by exact_mod_cast Order.add_one_le_of_lt hω'
+    exact stoppedProcess_eq_of_le h_succ
+
+/-- The history of the first `min τ M` rounds has length at most `M`: its law gives measure zero
+to the histories of length `> M`. -/
+lemma _root_.ProbabilityTheory.HasLaw.stoppedProcess_sigmaHistory_apply_compl_fst_le
+    {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)}
+    (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) τ M) μ P) :
+    μ {h | h.1 ≤ M}ᶜ = 0 :=
+  hμ.measure_eq_zero_of_ae_notMem (measurableSet_sigma_fst_le M).compl
+    (ae_of_all _ fun _ h ↦ h fst_stoppedProcess_sigmaHistory_le)
+
+variable (hO : ∀ n, Measurable (O n)) (hX : ∀ n, Measurable (X n)) (hY : ∀ n, Measurable (Y n))
+  (hS : MeasurableSet S)
+include hO hX hY hS
+
+/-- On `{τ ≤ M}`, the history of the first `min τ M` rounds belongs to the stopping rule: its
+law under the restriction of `P` to `{τ ≤ M}` gives measure zero to `Sᶜ`. -/
+lemma _root_.ProbabilityTheory.HasLaw.stoppedProcess_sigmaHistory_stoppingTime_apply_compl
+    {μ : Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)}
+    (hμ : HasLaw (stoppedProcess (sigmaHistory O X Y) (stoppingTime O X Y S) M) μ
+      (P.restrict {ω | stoppingTime O X Y S ω ≤ M})) :
+    μ Sᶜ = 0 := by
+  refine hμ.measure_eq_zero_of_ae_notMem hS.compl
+    ((ae_restrict_iff' (measurableSet_le_natCast (measurable_stoppingTime hO hX hY hS) M)).2
+      (Filter.Eventually.of_forall fun ω hω h ↦ h ?_))
+  rw [stoppedProcess_eq_of_ge hω]
+  exact stoppedHist_mem_of_ne_top (ne_top_of_le_ne_top (ENat.natCast_ne_top M) hω)
+
+/-- On `{M < τ}`, the history of the first `M` rounds does not belong to the stopping rule: if it
+has law `ν` under the restriction of `P` to `{M < τ}`, the image of `ν` by `Sigma.mk M` gives
+measure zero to `S`. -/
+lemma _root_.ProbabilityTheory.HasLaw.history_restrict_lt_stoppingTime_map_sigmaMk_apply
+    {ν : Measure (Hist 𝓞 𝓐 𝓨 M)}
+    (hν : HasLaw (history O X Y M) ν (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) :
+    (ν.map (Sigma.mk M)) S = 0 :=
+  (((measurable_sigma_mk M).hasLaw_map ν).comp hν).measure_eq_zero_of_ae_notMem hS
+    ((ae_restrict_iff' (measurableSet_natCast_lt (measurable_stoppingTime hO hX hY hS) M)).2
+      (Filter.Eventually.of_forall fun _ hω ↦ notMem_of_lt_stoppingTime hω))
+
+end law
+
+section filtration
+
+variable {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : Measure Ω} [IsFiniteMeasure P]
+
+lemma IsAlgEnvSeq.adapted_sigmaHistory (h : IsAlgEnvSeq O X Y alg env P) :
+    Adapted h.filtration (sigmaHistory O X Y) :=
+  fun n ↦ (measurable_sigma_mk n).comp (h.adapted_history n)
+
+/-- The stopping time of a stopping rule is a stopping time of the history filtration of any
+algorithm-environment sequence. -/
+lemma IsAlgEnvSeq.isStoppingTime_stoppingTime (h : IsAlgEnvSeq O X Y alg env P)
+    (hS : MeasurableSet S) :
+    IsStoppingTime h.filtration (stoppingTime O X Y S) :=
+  h.adapted_sigmaHistory.isStoppingTime_hittingAfter hS
+
+/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the round at time `M`
+keeps its conditional law given the first `M` rounds. -/
+lemma IsAlgEnvSeq.hasCondDistrib_step_restrict_lt_stoppingTime
+    (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) :
+    HasCondDistrib (step O X Y M) (history O X Y M) (stepKernel alg env M)
+      (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) :=
+  (h.hasCondDistrib_step M).restrict_of_measurableSet_comap (h.measurable_history M)
+    (h.measurable_step M) (measurableSet_comap_history_lt_stoppingTime hS M)
+
+/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the observation at time
+`M` keeps its conditional law given the first `M` rounds. -/
+lemma IsAlgEnvSeq.hasCondDistrib_obs_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P)
+    (hS : MeasurableSet S) (M : ℕ) :
+    HasCondDistrib (O M) (history O X Y M) (env.obs M)
+      (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) :=
+  (h.hasCondDistrib_obs M).restrict_of_measurableSet_comap (h.measurable_history M)
+    (h.measurable_obs M) (measurableSet_comap_history_lt_stoppingTime hS M)
+
+/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the action at time `M`
+keeps its conditional law given the first `M` rounds and the observation at time `M`. -/
+lemma IsAlgEnvSeq.hasCondDistrib_action_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P)
+    (hS : MeasurableSet S) (M : ℕ) :
+    HasCondDistrib (X M) (fun ω ↦ (history O X Y M ω, O M ω)) (alg.policy M)
+      (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) :=
+  (h.hasCondDistrib_action M).restrict_of_measurableSet_comap
+    ((h.measurable_history M).prodMk (h.measurable_obs M)) (h.measurable_action M)
+    (measurable_iff_comap_le.mp (h.measurable_history_filtrationObs M) _
+      (measurableSet_comap_history_lt_stoppingTime hS M))
+
+/-- On the event `{M < τ}`, which is determined by the first `M` rounds, the feedback at time `M`
+keeps its conditional law given the first `M` rounds, the observation and the action at time
+`M`. -/
+lemma IsAlgEnvSeq.hasCondDistrib_feedback_restrict_lt_stoppingTime
+    (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) (M : ℕ) :
+    HasCondDistrib (Y M) (fun ω ↦ ((history O X Y M ω, O M ω), X M ω)) (env.feedback M)
+      (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) :=
+  (h.hasCondDistrib_feedback M).restrict_of_measurableSet_comap
+    (((h.measurable_history M).prodMk (h.measurable_obs M)).prodMk (h.measurable_action M))
+    (h.measurable_feedback M)
+    (measurable_iff_comap_le.mp (h.measurable_history_filtrationAction M) _
+      (measurableSet_comap_history_lt_stoppingTime hS M))
+
+/-- On the event `{M < τ}`, if the first `M` rounds have law `μ`, the first `M + 1` rounds have
+law the composition-product of `μ` with the step kernel. -/
+lemma IsAlgEnvSeq.hasLaw_history_succ_restrict_lt_stoppingTime (h : IsAlgEnvSeq O X Y alg env P)
+    (hS : MeasurableSet S) {μ : Measure (Hist 𝓞 𝓐 𝓨 M)}
+    (hμ : HasLaw (history O X Y M) μ (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω})) :
+    HasLaw (history O X Y (M + 1))
+      ((μ ⊗ₘ stepKernel alg env M).map (MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) M).symm)
+      (P.restrict {ω | (M : ℕ∞) < stoppingTime O X Y S ω}) :=
+  hasLaw_history_succ hμ (h.hasCondDistrib_step_restrict_lt_stoppingTime hS M)
+
+end filtration
+
+section trajMeasure
+
+/-! ### The law of the stopped history
+
+The stopping time and the stopped history are functions of the trajectory, whose law is
+determined by the algorithm and the environment (`IsAlgEnvSeq.hasLaw_trajectory`). Hence the law
+of the stopped history is determined by the algorithm and the environment: it is the law
+`stoppedHistMeasure alg env S` of the stopped history on the canonical space `trajMeasure`. -/
+
+variable {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨}
+
+/-- The law of the history stopped by the stopping rule `S`, for the algorithm `alg` in the
+environment `env`: the law of the stopped history on the canonical space `trajMeasure alg env`.
+This is the law of the stopped history for any algorithm-environment sequence
+(`IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime`). -/
+noncomputable def stoppedHistMeasure (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨)
+    (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) :
+    Measure (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) :=
+  (trajMeasure alg env).map
+    (stoppedHist IT.obs IT.action IT.feedback (stoppingTime IT.obs IT.action IT.feedback S))
+deriving IsProbabilityMeasure
+
+/-- The law of the history stopped by `S` under any algorithm-environment sequence for `alg` and
+`env` is `stoppedHistMeasure alg env S`. -/
+lemma IsAlgEnvSeq.hasLaw_stoppedHist_stoppingTime {P : Measure Ω} [IsProbabilityMeasure P]
+    (h : IsAlgEnvSeq O X Y alg env P) (hS : MeasurableSet S) :
+    HasLaw (stoppedHist O X Y (stoppingTime O X Y S)) (stoppedHistMeasure alg env S) P :=
+  ((measurable_stoppedHist IT.measurable_obs IT.measurable_action IT.measurable_feedback
+    (measurable_stoppingTime IT.measurable_obs IT.measurable_action IT.measurable_feedback
+      hS)).hasLaw_map _).comp h.hasLaw_trajectory
+
+end trajMeasure
+
+end Learning