Identification algorithm

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

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

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

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 ι]

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

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

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) 𝓞)