Rework the algorithm/environment classes and constructors

LMLTutorial/Pages/DefiningAlgorithm.lean

@@ -61,14 +61,14 @@ The `policy` field contains for each time `n` a kernel from that history togethe
 That is, it maps every possible history and current observation to a random action at time `n` (and that map is measurable).
 The `isMarkovKernel_policy` field records that the measure describing the action is a probability measure (and it is in square brackets to tell Lean to infer it automatically whenever possible).
 At time `0` the history is empty: `Hist 𝓞 𝓐 𝓨 0` has a unique element, and the distribution of the first action given the first observation is `policy 0` applied to that element.
-That kernel is called `Algorithm.p0`.
+That kernel is called `Algorithm.policyZero`.
 
 Many settings have no observations at all: the algorithm sees only the past rounds. Those are described by taking `𝓞 = Unit`, and we write `noObs Ω` for the corresponding (constant) observation process.
 
-If the algorithms actions are not random, we can use the `detAlgorithm` definition to build an algorithm from the data of a measurable function for the action at each time, as a function of the history before that time and of the current observation.
+If the algorithms actions are not random, we can use the `Algorithm.deterministic` definition to build an algorithm from the data of a measurable function for the action at each time, as a function of the history before that time and of the current observation.
 The first action is the value of that function at time `0` on the empty history.
 
-{docstring detAlgorithm}
+{docstring Algorithm.deterministic}
 
 We can see here that we did not need to prove that the kernels are `IsMarkovKernel`.
 Lean knows that deterministic kernels are Markov.
@@ -79,19 +79,21 @@ The `Environment` structure is the mirror of the `Algorithm` structure, with a k
 
 `obs n` gives the distribution of the observation at time `n` given the history before `n`.
 `feedback n` gives the distribution of the feedback at time `n` given the history before `n`, the observation and the action at time `n`.
-The distribution of the first observation is `obs 0` applied to the empty history; it is called `Environment.obs0`.
-The distribution of the first feedback given the first observation and action is `feedback 0` applied to the empty history; it is called `Environment.ν0`.
+The distribution of the first observation is `obs 0` applied to the empty history; it is called `Environment.obsZero`.
+The distribution of the first feedback given the first observation and action is `feedback 0` applied to the empty history; it is called `Environment.feedbackZero`.
 
-In many applications there is no observation and the feedback depends only on the last action, not on the prior history.
-We provide an `obliviousEnv` definition that builds an environment for those cases.
+In many applications neither the observation nor the feedback depends on the prior history: the observation at time `n` has a fixed law, and the feedback depends only on the current observation and action.
+We provide an `Environment.oblivious` definition that builds an environment for those cases from a sequence of observation laws and a sequence of feedback kernels.
 
-{docstring obliviousEnv}
+{docstring Environment.oblivious}
 
-`(ν n).prodMkLeft _` is the kernel `ν n` seen as a `Kernel ((Hist Unit 𝓐 𝓨 n × Unit) × 𝓐) 𝓨` by ignoring the history and the observation.
+If furthermore those sequences do not change with time, we can use the `Environment.stationary` definition to build the environment.
 
-If furthermore the feedback kernel does not change with time, we can use the `stationaryEnv` definition to build the environment.
+{docstring Environment.stationary}
 
-{docstring stationaryEnv}
+When there is no observation (`𝓞 = Unit`), the feedback depends only on the last action. `Environment.banditSeq` builds such an environment from a sequence of kernels `ν : ℕ → Kernel 𝓐 𝓨`, and `Environment.bandit` from a single kernel `ν : Kernel 𝓐 𝓨` used at every time.
+
+{docstring Environment.bandit}
 
 
 # Sequences of actions and feedback, probability space
@@ -120,14 +122,14 @@ We now illustrate the use of `Algorithm`, `Environment`, and `IsAlgEnvSeq` by de
 
 In a stochastic bandit, an algorithm chooses at each time an action from a finite set (here `Fin K`, the type of natural numbers less than `K`) and receives a reward drawn from a distribution that depends only on the action, not on the prior history.
 
-The environment is thus simply `stationaryEnv ν` for some kernel `ν : Kernel (Fin K) ℝ`.
+The environment is thus simply `Environment.bandit ν` for some kernel `ν : Kernel (Fin K) ℝ`.
 
 ## Algorithm
 
 The UCB algorithm chooses at time `n` the action that maximizes the sum of the empirical mean reward and an exploration bonus.
 It starts by choosing each action once and then chooses $`\arg\max_a (\hat{\mu}_{n,a} + \sqrt{\frac{2c \log (n + 1)}{N_{n,a}}})`, in which $`\hat{\mu}_{n,a}` is the empirical mean reward of action `a` before time `n` (`empMean'` in the code), $`N_{n,a}` is the number of times action `a` has been chosen before time `n` (`pullCount'` in the code), and `c` is a parameter of the algorithm.
 
-To define the algorithm, we first define the exploration bonus and the next action function, and then we use `detAlgorithm` to build the algorithm.
+To define the algorithm, we first define the exploration bonus and the next action function, and then we use `Algorithm.deterministic` to build the algorithm.
 We also need to prove that the next action function is measurable, which is done by the `measurable_nextArm` lemma.
 Note that we are careful to use a measurable version of the argmax function, `argmax`.
 
@@ -139,7 +141,7 @@ Note that we are careful to use a measurable version of the argmax function, `ar
 
 {docstring Bandits.ucbAlgorithm}
 
-The last line builds the algorithm using `detAlgorithm` and the function `UCB.nextArm`.
+The last line builds the algorithm using `Algorithm.deterministic` and the function `UCB.nextArm`.
 Its measurability is proved by the `fun_prop` tactic, which proves measurability of functions by using lemmas tagged with `@[fun_prop]`.
 The first action of the algorithm is `UCB.nextArm K c 0` applied to the empty history, which is 0 as an element of `Fin K`.
 

LeanMachineLearning.lean

@@ -54,6 +54,7 @@ public import LeanMachineLearning.SequentialLearning.ActionIndicator
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes
+public import LeanMachineLearning.SequentialLearning.Algorithms.Markov
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling.Basic
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling.Tendsto
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin

LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean

@@ -48,7 +48,7 @@ variable (K) in
 to `ETC.nextArm`. -/
 noncomputable
 def etcAlgorithm [NeZero K] (m : ℕ) : Algorithm Unit (Fin K) ℝ :=
-  detAlgorithm (fun n p ↦ ETC.nextArm K m n p.1) (by fun_prop)
+  Algorithm.deterministic (fun n p ↦ ETC.nextArm K m n p.1) (by fun_prop)
 
 end AlgorithmDefinition
 
@@ -61,43 +61,44 @@ variable [NeZero K] {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
 
 /-- Before round `K * m`, the ETC algorithm behaves like the Round-Robin algorithm. -/
 lemma isAlgEnvSeqUntil_roundRobinAlgorithm
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) :
-    IsAlgEnvSeqUntil O A R (roundRobinAlgorithm K) (stationaryEnv ν) P (K * m) := by
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P) :
+    IsAlgEnvSeqUntil O A R (roundRobinAlgorithm K) (Environment.bandit ν) P (K * m) := by
   refine h.isAlgEnvSeqUntil_of_policy_eq fun n hn ↦ ?_
-  simp only [roundRobinAlgorithm, detAlgorithm_policy, etcAlgorithm]
+  simp only [roundRobinAlgorithm, Algorithm.deterministic_policy, etcAlgorithm]
   congr 1 with p
   simp [ETC.nextArm, hn]
 
 section AlgorithmBehavior
 
-lemma arm_ae_eq_nextArm (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) (n : ℕ) :
+lemma arm_ae_eq_nextArm (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
+    (n : ℕ) :
     A n =ᵐ[P] fun ω ↦ nextArm K m n (history O A R n ω) :=
-  h.action_detAlgorithm_ae_eq n
+  h.action_deterministic_ae_eq n
 
 /-- For `n < K * m`, the arm pulled at time `n` is the arm `n % K`. -/
-lemma arm_of_lt (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma arm_of_lt (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     {n : ℕ} (hn : n < K * m) :
     A n =ᵐ[P] fun _ ↦ RoundRobin.nextAction K n :=
   RoundRobin.action_ae_eq n ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono hn)
 
 /-- The arm pulled at time `K * m` is the arm with the highest empirical mean after the exploration
 phase. -/
 lemma arm_mul
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) :
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P) :
     A (K * m) =ᵐ[P] fun ω ↦ argmax (empMean' (K * m) (history O A R (K * m) ω)) := by
   filter_upwards [arm_ae_eq_nextArm h (K * m)] with ω hn_eq
   rw [hn_eq, nextArm, dite_eq_right (by simp), dite_eq_left rfl]
 
 /-- For `n ≥ K * m`, the arm pulled at time `n + 1` is the same as the arm pulled at time `n`. -/
-lemma arm_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma arm_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     {n : ℕ} (hn : K * m ≤ n) :
     A (n + 1) =ᵐ[P] fun ω ↦ A n ω := by
   filter_upwards [arm_ae_eq_nextArm h (n + 1)] with ω hn_eq
   rw [hn_eq, nextArm, dite_eq_right (by grind), dite_eq_right (by grind)]
   rfl
 
 /-- For `n ≥ K * m`, the arm pulled at time `n` is the same as the arm pulled at time `K * m`. -/
-lemma arm_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma arm_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     {n : ℕ} (hn : K * m ≤ n) :
     A n =ᵐ[P] A (K * m) := by
   have h_ae n : K * m ≤ n → A (n + 1) =ᵐ[P] fun ω ↦ A n ω := arm_add_one_of_ge h
@@ -108,11 +109,12 @@ lemma arm_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
   | succ n hmn h_ind => rw [h_ae n hmn, h_ind]
 
 /-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/
-lemma pullCount_mul (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) (a : Fin K) :
+lemma pullCount_mul (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
+    (a : Fin K) :
     pullCount A a (K * m) =ᵐ[P] fun _ ↦ m :=
   RoundRobin.pullCount_mul m (isAlgEnvSeqUntil_roundRobinAlgorithm h) a
 
-lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (a : Fin K) {n : ℕ} (hn : K * m ≤ n) :
     pullCount A a (n + 1)
       =ᵐ[P] fun ω ↦ pullCount A a n ω + {ω' | A (K * m) ω' = a}.indicator 1 ω := by
@@ -122,7 +124,7 @@ lemma pullCount_add_one_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (station
 
 /-- For `n ≥ K * m`, the number of pulls of each arm `a` at time `n` is equal to `m` plus
 `n - K * m` if arm `a` is the best arm after the exploration phase. -/
-lemma pullCount_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma pullCount_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (a : Fin K) {n : ℕ} (hn : K * m ≤ n) :
     pullCount A a n
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator 1 ω := by
@@ -142,7 +144,7 @@ lemma pullCount_of_ge (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv 
 /-- If at time `K * m` the algorithm chooses arm `a`, then the total reward obtained by pulling
 arm `a` is at least the total reward obtained by pulling the best arm. -/
 lemma sumRewards_bestArm_le_of_arm_mul_eq
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P) (a : Fin K) (hm : m ≠ 0) :
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P) (a : Fin K) (hm : m ≠ 0) :
     ∀ᵐ ω ∂P, A (K * m) ω = a → sumRewards A R (bestArm ν) (K * m) ω ≤
       sumRewards A R a (K * m) ω := by
   filter_upwards [arm_mul h, pullCount_mul h a, pullCount_mul h (bestArm ν)]

LeanMachineLearning/Online/Bandit/Algorithms/Regret/ETC.lean

@@ -26,7 +26,7 @@ variable {K : ℕ} [NeZero K] {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKerne
   {σ2 : ℝ≥0}
 
 lemma probReal_sumRewards_le_sumRewards_le
-    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+    (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K) :
     P.real {ω | sumRewards A R (bestArm ν) (K * m) ω ≤ sumRewards A R a (K * m) ω} ≤
       Real.exp (-↑m * gap ν a ^ 2 / (4 * σ2)) := by
@@ -42,7 +42,7 @@ lemma probReal_sumRewards_le_sumRewards_le
 
 /-- The probability that at time `K * m` the ETC algorithm chooses arm `a` is at most
 `exp(- m * Δ_a^2 / (4 * σ2))`. -/
-lemma prob_arm_mul_eq_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma prob_arm_mul_eq_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (a : Fin K)
     (hm : m ≠ 0) :
     P.real {ω | A (K * m) ω = a} ≤ Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2)) := by
@@ -57,7 +57,7 @@ lemma prob_arm_mul_eq_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEn
   exact h_le.trans (probReal_sumRewards_le_sumRewards_le h hν a)
 
 /-- Bound on the expectation of the number of pulls of each arm by the ETC algorithm. -/
-lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
     P[fun ω ↦ (pullCount A a n ω : ℝ)]
@@ -85,7 +85,7 @@ lemma expectation_pullCount_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (statio
   · exact (measurableSet_singleton _).preimage (by fun_prop)
 
 /-- Regret bound for the ETC algorithm. -/
-theorem regret_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (stationaryEnv ν) P)
+theorem regret_le (h : IsAlgEnvSeq O A R (etcAlgorithm K m) (Environment.bandit ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hm : m ≠ 0)
     (n : ℕ) (hn : K * m ≤ n) :
     P[regret ν A n] ≤