Reorganize

LeanBandits.lean

@@ -1,15 +1,17 @@
-import LeanBandits.Algorithm
 import LeanBandits.AlgorithmAndRandomVariables
 import LeanBandits.AlgorithmBuilding
-import LeanBandits.Bandit
-import LeanBandits.ETC
+import LeanBandits.Bandit.Bandit
+import LeanBandits.Bandit.Regret
+import LeanBandits.BanditAlgorithms.ETC
+import LeanBandits.BanditAlgorithms.UCB
 import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.IdentDistrib
 import LeanBandits.ForMathlib.IndepFun
 import LeanBandits.ForMathlib.KernelSub
 import LeanBandits.ForMathlib.Measurable
+import LeanBandits.ForMathlib.MeasurableArgMax
 import LeanBandits.ForMathlib.SubGaussian
 import LeanBandits.ForMathlib.Traj
-import LeanBandits.Regret
 import LeanBandits.RewardByCountMeasure
-import LeanBandits.UCB
+import LeanBandits.SequentialLearning.Algorithm
+import LeanBandits.SequentialLearning.Deterministic

LeanBandits/AlgorithmAndRandomVariables.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import LeanBandits.Regret
+import LeanBandits.Bandit.Regret
 import LeanBandits.AlgorithmBuilding
 
 /-!

LeanBandits/AlgorithmBuilding.lean

@@ -3,86 +3,17 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import LeanBandits.Bandit
+import Mathlib.Analysis.Normed.Ring.Basic
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+import Mathlib.Topology.Compactness.PseudometrizableLindelof
 
 /-! # Tools to build bandit algorithms
 
 -/
 
-open MeasureTheory ProbabilityTheory Finset
+open MeasureTheory Finset
 open scoped ENNReal NNReal
 
-section MeasurableArgmax -- copied from PR #27579 (and changed from argmin to argmax)
-
-lemma measurable_encode {α : Type*} {_ : MeasurableSpace α} [Encodable α]
-    [MeasurableSingletonClass α] :
-    Measurable (Encodable.encode (α := α)) := by
-  refine measurable_to_nat fun a ↦ ?_
-  have : Encodable.encode ⁻¹' {Encodable.encode a} = {a} := by ext; simp
-  rw [this]
-  exact measurableSet_singleton _
-
-lemma measurableEmbedding_encode (α : Type*) {_ : MeasurableSpace α} [Encodable α]
-    [MeasurableSingletonClass α] :
-    MeasurableEmbedding (Encodable.encode (α := α)) where
-  injective := Encodable.encode_injective
-  measurable := measurable_encode
-  measurableSet_image' _ _ := .of_discrete
-
-section Finite
-
-variable {𝓧 𝓨 α : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨}
-  {mα : MeasurableSpace α} [TopologicalSpace α] [LinearOrder α]
-  [OpensMeasurableSpace α] [OrderClosedTopology α] [SecondCountableTopology α]
-
-lemma measurableSet_isMax [Countable 𝓨]
-    {f : 𝓧 → 𝓨 → α} (hf : ∀ y, Measurable (fun x ↦ f x y)) (y : 𝓨) :
-    MeasurableSet {x | ∀ z, f x z ≤ f x y} := by
-  rw [show {x | ∀ y', f x y' ≤ f x y} = ⋂ y', {x | f x y' ≤ f x y} by ext; simp]
-  exact MeasurableSet.iInter fun z ↦ measurableSet_le (by fun_prop) (by fun_prop)
-
-lemma exists_isMaxOn' {α : Type*} [LinearOrder α]
-    [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] (f : 𝓧 → 𝓨 → α) (x : 𝓧) :
-    ∃ n : ℕ, ∃ y, n = Encodable.encode y ∧ ∀ z, f x z ≤ f x y := by
-  obtain ⟨y, h⟩ := Finite.exists_max (f x)
-  exact ⟨Encodable.encode y, y, rfl, h⟩
-
-/-- A measurable argmax function. -/
-noncomputable
-def measurableArgmax [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
-    (f : 𝓧 → 𝓨 → α)
-    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
-    (x : 𝓧) :
-    𝓨 :=
-  (measurableEmbedding_encode 𝓨).invFun (Nat.find (exists_isMaxOn' f x))
-
-lemma measurable_measurableArgmax [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
-    {f : 𝓧 → 𝓨 → α}
-    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
-    (hf : ∀ y, Measurable (fun x ↦ f x y)) :
-    Measurable (measurableArgmax f) := by
-  refine (MeasurableEmbedding.measurable_invFun (measurableEmbedding_encode 𝓨)).comp ?_
-  refine measurable_find _ fun n ↦ ?_
-  have : {x | ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y}
-      = ⋃ y, ({x | n = Encodable.encode y} ∩ {x | ∀ z, f x z ≤ f x y}) := by ext; simp
-  rw [this]
-  refine MeasurableSet.iUnion fun y ↦ (MeasurableSet.inter (by simp) ?_)
-  exact measurableSet_isMax (by fun_prop) y
-
-lemma isMaxOn_measurableArgmax {α : Type*} [LinearOrder α]
-    [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
-    (f : 𝓧 → 𝓨 → α)
-    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
-    (x : 𝓧) (z : 𝓨) :
-    f x z ≤ f x (measurableArgmax f x) := by
-  obtain ⟨y, h_eq, h_le⟩ := Nat.find_spec (exists_isMaxOn' f x)
-  refine le_trans (h_le z) (le_of_eq ?_)
-  rw [measurableArgmax, h_eq,
-    MeasurableEmbedding.leftInverse_invFun (measurableEmbedding_encode 𝓨) y]
-
-end Finite
-end MeasurableArgmax
-
 namespace Bandits
 
 variable {α : Type*} [DecidableEq α] [MeasurableSpace α]

LeanBandits/Bandit.lean → LeanBandits/Bandit/Bandit.lean

@@ -3,10 +3,9 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Paulo Rauber
 -/
-import Mathlib
-import LeanBandits.Algorithm
-import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.Traj
+import LeanBandits.SequentialLearning.Deterministic
+import Mathlib.Probability.IdentDistrib
+import Mathlib.Probability.Independence.InfinitePi
 
 /-!
 # Bandit

LeanBandits/Regret.lean → LeanBandits/Bandit/Regret.lean

@@ -3,8 +3,9 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Paulo Rauber
 -/
-import Mathlib
-import LeanBandits.Bandit
+import LeanBandits.Bandit.Bandit
+import Mathlib.Data.ENat.Lattice
+import Mathlib.Order.CompletePartialOrder
 
 /-!
 # Regret

LeanBandits/ETC.lean → LeanBandits/BanditAlgorithms/ETC.lean

@@ -3,11 +3,9 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.Probability.Moments.SubGaussian
 import LeanBandits.AlgorithmAndRandomVariables
-import LeanBandits.AlgorithmBuilding
+import LeanBandits.ForMathlib.MeasurableArgMax
 import LeanBandits.ForMathlib.SubGaussian
-import LeanBandits.Regret
 import LeanBandits.RewardByCountMeasure
 
 /-! # The Explore-Then-Commit Algorithm

LeanBandits/UCB.lean → LeanBandits/BanditAlgorithms/UCB.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import LeanBandits.AlgorithmBuilding
-import LeanBandits.Regret
+import LeanBandits.Bandit.Regret
+import LeanBandits.ForMathlib.MeasurableArgMax
 
 /-!
 # UCB algorithm

LeanBandits/ForMathlib/CondDistrib.lean

@@ -3,12 +3,10 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
+import LeanBandits.ForMathlib.KernelSub
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.Probability.Independence.Basic
 import Mathlib.Probability.Independence.Conditional
-import Mathlib.Probability.Kernel.CompProdEqIff
-import Mathlib.Probability.Kernel.Composition.Lemmas
-import LeanBandits.ForMathlib.KernelSub
 
 open MeasureTheory ProbabilityTheory Finset
 open scoped ENNReal NNReal

LeanBandits/ForMathlib/IndepFun.lean

@@ -1,4 +1,5 @@
-import Mathlib
+import Mathlib.Probability.IdentDistrib
+import Mathlib.Probability.Independence.InfinitePi
 
 open MeasureTheory Finset
 

LeanBandits/ForMathlib/Measurable.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib
+import Mathlib.MeasureTheory.MeasurableSpace.Basic
 
 /-!
 # Measurability lemmas

LeanBandits/ForMathlib/MeasurableArgMax.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
+
+/-! # Measurable argmax function
+
+-/
+
+open MeasureTheory Finset
+open scoped ENNReal NNReal
+
+section MeasurableArgmax -- copied from PR #27579 (and changed from argmin to argmax)
+
+lemma measurable_encode {α : Type*} {_ : MeasurableSpace α} [Encodable α]
+    [MeasurableSingletonClass α] :
+    Measurable (Encodable.encode (α := α)) := by
+  refine measurable_to_nat fun a ↦ ?_
+  have : Encodable.encode ⁻¹' {Encodable.encode a} = {a} := by ext; simp
+  rw [this]
+  exact measurableSet_singleton _
+
+lemma measurableEmbedding_encode (α : Type*) {_ : MeasurableSpace α} [Encodable α]
+    [MeasurableSingletonClass α] :
+    MeasurableEmbedding (Encodable.encode (α := α)) where
+  injective := Encodable.encode_injective
+  measurable := measurable_encode
+  measurableSet_image' _ _ := .of_discrete
+
+section Finite
+
+variable {𝓧 𝓨 α : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨}
+  {mα : MeasurableSpace α} [TopologicalSpace α] [LinearOrder α]
+  [OpensMeasurableSpace α] [OrderClosedTopology α] [SecondCountableTopology α]
+
+lemma measurableSet_isMax [Countable 𝓨]
+    {f : 𝓧 → 𝓨 → α} (hf : ∀ y, Measurable (fun x ↦ f x y)) (y : 𝓨) :
+    MeasurableSet {x | ∀ z, f x z ≤ f x y} := by
+  rw [show {x | ∀ y', f x y' ≤ f x y} = ⋂ y', {x | f x y' ≤ f x y} by ext; simp]
+  exact MeasurableSet.iInter fun z ↦ measurableSet_le (by fun_prop) (by fun_prop)
+
+lemma exists_isMaxOn' {α : Type*} [LinearOrder α]
+    [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] (f : 𝓧 → 𝓨 → α) (x : 𝓧) :
+    ∃ n : ℕ, ∃ y, n = Encodable.encode y ∧ ∀ z, f x z ≤ f x y := by
+  obtain ⟨y, h⟩ := Finite.exists_max (f x)
+  exact ⟨Encodable.encode y, y, rfl, h⟩
+
+/-- A measurable argmax function. -/
+noncomputable
+def measurableArgmax [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
+    (f : 𝓧 → 𝓨 → α)
+    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
+    (x : 𝓧) :
+    𝓨 :=
+  (measurableEmbedding_encode 𝓨).invFun (Nat.find (exists_isMaxOn' f x))
+
+lemma measurable_measurableArgmax [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
+    {f : 𝓧 → 𝓨 → α}
+    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
+    (hf : ∀ y, Measurable (fun x ↦ f x y)) :
+    Measurable (measurableArgmax f) := by
+  refine (MeasurableEmbedding.measurable_invFun (measurableEmbedding_encode 𝓨)).comp ?_
+  refine measurable_find _ fun n ↦ ?_
+  have : {x | ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y}
+      = ⋃ y, ({x | n = Encodable.encode y} ∩ {x | ∀ z, f x z ≤ f x y}) := by ext; simp
+  rw [this]
+  refine MeasurableSet.iUnion fun y ↦ (MeasurableSet.inter (by simp) ?_)
+  exact measurableSet_isMax (by fun_prop) y
+
+lemma isMaxOn_measurableArgmax {α : Type*} [LinearOrder α]
+    [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
+    (f : 𝓧 → 𝓨 → α)
+    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
+    (x : 𝓧) (z : 𝓨) :
+    f x z ≤ f x (measurableArgmax f x) := by
+  obtain ⟨y, h_eq, h_le⟩ := Nat.find_spec (exists_isMaxOn' f x)
+  refine le_trans (h_le z) (le_of_eq ?_)
+  rw [measurableArgmax, h_eq,
+    MeasurableEmbedding.leftInverse_invFun (measurableEmbedding_encode 𝓨) y]
+
+end Finite
+end MeasurableArgmax

LeanBandits/RewardByCountMeasure.lean

@@ -3,10 +3,10 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import LeanBandits.Bandit
+import LeanBandits.Bandit.Bandit
+import LeanBandits.Bandit.Regret
 import LeanBandits.ForMathlib.IdentDistrib
 import LeanBandits.ForMathlib.IndepFun
-import LeanBandits.Regret
 
 /-! # Laws of `stepsUntil` and `rewardByCount`
 -/

LeanBandits/Algorithm.lean → LeanBandits/SequentialLearning/Algorithm.lean

@@ -3,13 +3,12 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Paulo Rauber
 -/
-import Mathlib
-import LeanBandits.ForMathlib.CondDistrib
 import LeanBandits.ForMathlib.Measurable
 import LeanBandits.ForMathlib.Traj
+import Mathlib.Probability.HasLaw
 
 /-!
-# Bandit
+# Algorithms
 -/
 
 open MeasureTheory ProbabilityTheory Filter Real Finset
@@ -235,46 +234,6 @@ lemma condDistrib_reward_zero [StandardBorelSpace R] [Nonempty R]
   have h_action := (hasLaw_action_zero alg env).map_eq
   rwa [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop), h_action]
 
-section DetAlgorithm
-
-/-- A deterministic algorithm. -/
-@[simps]
-noncomputable
-def detAlgorithm (nextaction : (n : ℕ) → (Iic n → α × R) → α)
-    (h_next : ∀ n, Measurable (nextaction n)) (action0 : α) :
-    Algorithm α R where
-  policy n := Kernel.deterministic (nextaction n) (h_next n)
-  p0 := Measure.dirac action0
-
-variable {nextaction : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextaction n)}
-  {action0 : α} {env : Environment α R}
-
-local notation "𝔓" => trajMeasure (detAlgorithm nextaction h_next action0) env
-
-lemma HasLaw_action_zero_detAlgorithm : HasLaw (action 0) (Measure.dirac action0) 𝔓 where
-  map_eq := (hasLaw_action_zero _ _).map_eq
-
-lemma action_zero_detAlgorithm [MeasurableSingletonClass α] : action 0 =ᵐ[𝔓] fun _ ↦ action0 := by
-  have h_eq : ∀ᵐ x ∂((𝔓).map (action 0)), x = action0 := by
-    rw [(hasLaw_action_zero _ _).map_eq]
-    simp [detAlgorithm]
-  exact ae_of_ae_map (by fun_prop) h_eq
-
-lemma action_detAlgorithm_ae_eq
-    [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
-    (n : ℕ) :
-    action (n + 1) =ᵐ[𝔓] fun h ↦ nextaction n (fun i ↦ h i) := by
-  have h := condDistrib_action (detAlgorithm nextaction h_next action0) env n
-  simp only [detAlgorithm_policy] at h
-  sorry
-
-example [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] :
-    ∀ᵐ h ∂𝔓, action 0 h = action0 ∧ ∀ n, action (n + 1) h = nextaction n (fun i ↦ h i) := by
-  rw [eventually_and, ae_all_iff]
-  exact ⟨action_zero_detAlgorithm, action_detAlgorithm_ae_eq⟩
-
-end DetAlgorithm
-
 section stationaryEnv
 
 /-- A stationary environment, in which the distribution of the next reward depends only on the last