Identification algorithms

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,8 +30,10 @@ 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.Process.HittingTime
 public import LeanMachineLearning.ForMathlib.Probability.WithDensity
 public import LeanMachineLearning.ForMathlib.Topology.Instances.ENNReal.Lemmas
 public import LeanMachineLearning.Online.Bandit.Algorithms.ETC
@@ -57,9 +60,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,102 @@
+/-
+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. -/
+@[fun_prop]
+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/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/ForMathlib/Probability/Process/HittingTime.lean

@@ -0,0 +1,35 @@
+/-
+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.Probability.Process.HittingTime
+
+/-!
+# Hitting times
+-/
+
+@[expose] public section
+
+namespace MeasureTheory
+
+variable {Ω β ι : Type*} [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι]
+  {u : ι → Ω → β} {s : Set β} {n i : ι} {ω : Ω}
+
+lemma hittingAfter_eq_coe_iff :
+    hittingAfter u s n ω = i ↔ n ≤ i ∧ u i ω ∈ s ∧ ∀ j ∈ Set.Ico n i, u j ω ∉ s := by
+  constructor
+  · intro h
+    have h_le := le_hittingAfter (u := u) (s := s) (n := n) ω
+    have h_mem := hittingAfter_mem_set_of_ne_top (u := u) (s := s) (n := n) (ω := ω) (by simp [h])
+    rw [h] at h_le h_mem
+    exact ⟨mod_cast h_le, h_mem,
+      fun j hj ↦ notMem_of_lt_hittingAfter (h ▸ mod_cast hj.2) hj.1⟩
+  · rintro ⟨hni, his, h⟩
+    refine le_antisymm (hittingAfter_le_of_mem hni his) (not_lt.1 fun hlt ↦ ?_)
+    obtain ⟨j, hj, hjs⟩ := hittingAfter_lt_iff.1 hlt
+    exact h j hj hjs
+
+end MeasureTheory

LeanMachineLearning/SequentialLearning/IdentificationAlg.lean

@@ -0,0 +1,166 @@
+/-
+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.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 law of the output of a run is determined by `A` and `env`: it is `A.outputMeasure env`, 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 badness
+predicate `bad θ` if, for every `θ`, the output in `env θ` is `bad θ` with probability at most `δ`.
+
+## 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 bad δ`: for every parameter `θ`, the output of `A` in `env θ` is
+  `bad θ` with probability at most `δ`.
+
+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 Ω}
+  {O : ℕ → Ω → 𝓞} {X : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
+
+/-- 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 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 𝓞 𝓐 𝓨 𝓓} {env : Environment 𝓞 𝓐 𝓨} {out : Ω → 𝓓} {P : Measure Ω}
+
+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 (A : IdentAlg 𝓞 𝓐 𝓨 𝓓)
+    (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) :
+    Ω → ℕ∞ :=
+  hittingAfter (sigmaHistory O X Y) A.stopSet 0
+
+lemma stoppingTime_def : A.stoppingTime O X Y = hittingAfter (sigmaHistory O X Y) A.stopSet 0 := rfl
+
+/-- The history of the rounds played by an identification algorithm `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 (A : IdentAlg 𝓞 𝓐 𝓨 𝓓)
+    (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) :
+    Ω → Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n :=
+  stoppedValue (sigmaHistory O X Y) (A.stoppingTime O X Y)
+
+lemma stoppedHist_def :
+    A.stoppedHist O X Y = stoppedValue (sigmaHistory O X Y) (A.stoppingTime O X Y) := rfl
+
+/-- The law of the output of an identification algorithm in an environment. -/
+noncomputable def outputMeasure (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Environment 𝓞 𝓐 𝓨) : Measure 𝓓 :=
+  A.output ∘ₘ stoppedHistMeasure A.alg env A.stopSet
+deriving IsProbabilityMeasure
+
+/-- `(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. -/
+structure IsRun (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Environment 𝓞 𝓐 𝓨)
+    (O : ℕ → Ω → 𝓞) (X : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (out : Ω → 𝓓)
+    (P : Measure Ω := by volume_tac) [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
+
+/-- The stopping time of an identification algorithm `A` is a stopping time of the history
+filtration of any algorithm-environment sequence `O`, `X`, `Y`.
+Most often used with `alg = A.alg`. -/
+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.adapted_sigmaHistory.isStoppingTime_hittingAfter A.measurableSet_stopSet
+
+lemma stoppedHist_mem_stopSet_of_ne_top {ω : Ω} (h : A.stoppingTime O X Y ω ≠ ⊤) :
+    A.stoppedHist O X Y ω ∈ A.stopSet :=
+  hittingAfter_mem_set_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_stoppedValue_sigmaHistory 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
+  rwa [h.hasLaw_stoppedHist.map_eq] at h_comp
+
+section IsPAC
+
+/-- `A` is *PAC at level `δ`* for the family of environments `env : Θ → Environment 𝓞 𝓐 𝓨` and
+the predicate `bad : Θ → 𝓓 → Prop` if, for every `θ`, the output of `A` in `env θ` is
+`bad θ` with probability at most `δ`.
+See `IsPAC.measureReal_not_good_of_isRun` for the corresponding statement about any run of `A`. -/
+def IsPAC {Θ : Type*} (A : IdentAlg 𝓞 𝓐 𝓨 𝓓) (env : Θ → Environment 𝓞 𝓐 𝓨)
+    (bad : Θ → 𝓓 → Prop) (δ : ℝ) : Prop :=
+  ∀ θ, (A.outputMeasure (env θ)).real {d | bad θ d} ≤ δ
+
+/-- For a PAC algorithm at level `δ`, the output of any run in `env θ` is `bad θ` with
+probability at most `δ`. -/
+lemma IsPAC.measureReal_bad_of_isRun {Θ : Type*} {env : Θ → Environment 𝓞 𝓐 𝓨}
+    {bad : Θ → 𝓓 → Prop} {δ : ℝ} [IsProbabilityMeasure P]
+    (hA : A.IsPAC env bad δ) {θ : Θ} (hbad : MeasurableSet {d | bad θ d})
+    (h : A.IsRun (env θ) O X Y out P) :
+    P.real {ω | bad θ (out ω)} ≤ δ := by
+  rw [h.hasLaw_output.measureReal_eq hbad]
+  exact hA θ
+
+end IsPAC
+
+end IdentAlg
+
+end Learning