diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index d4aa0eca..c8f890c9 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,26 +1,26 @@ module -public import LeanMachineLearning.Bandit.Bandit -public import LeanMachineLearning.Bandit.Regret -public import LeanMachineLearning.Bandit.RewardByCountMeasure -public import LeanMachineLearning.Bandit.SumRewards -public import LeanMachineLearning.BanditAlgorithms.AuxSums -public import LeanMachineLearning.BanditAlgorithms.ETC -public import LeanMachineLearning.BanditAlgorithms.RoundRobin -public import LeanMachineLearning.BanditAlgorithms.UCB -public import LeanMachineLearning.ForMathlib.CondDistrib -public import LeanMachineLearning.ForMathlib.CondIndepFun -public import LeanMachineLearning.ForMathlib.HasCondDistrib -public import LeanMachineLearning.ForMathlib.IndepFun -public import LeanMachineLearning.ForMathlib.IndepInfinitePi -public import LeanMachineLearning.ForMathlib.Integrable -public import LeanMachineLearning.ForMathlib.KernelSub -public import LeanMachineLearning.ForMathlib.Measurable -public import LeanMachineLearning.ForMathlib.MeasurableArgMax -public import LeanMachineLearning.ForMathlib.StandardBorel -public import LeanMachineLearning.ForMathlib.SubGaussian -public import LeanMachineLearning.ForMathlib.Traj +public import LeanMachineLearning.Online.Bandit.ArrayProbSpace +public import LeanMachineLearning.Online.Bandit.Regret +public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure +public import LeanMachineLearning.Online.Bandit.SumRewards +public import LeanMachineLearning.Online.Bandit.Algorithms.ETC +public import LeanMachineLearning.Online.Bandit.Algorithms.UCB +public import LeanMachineLearning.Probability.Independence.CondDistrib +public import LeanMachineLearning.Probability.Independence.CondIndepFun +public import LeanMachineLearning.Probability.HasCondDistrib +public import LeanMachineLearning.Probability.Independence.IndepFun +public import LeanMachineLearning.Probability.Independence.IndepInfinitePi +public import LeanMachineLearning.Probability.Integrable +public import LeanMachineLearning.Probability.Kernel.KernelSub +public import LeanMachineLearning.MeasureTheory.Measurable +public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax +public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel +public import LeanMachineLearning.Probability.Moments.SubGaussian +public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj public import LeanMachineLearning.SequentialLearning.Algorithm +public import LeanMachineLearning.SequentialLearning.Algorithms.AuxSums +public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin public import LeanMachineLearning.SequentialLearning.Deterministic public import LeanMachineLearning.SequentialLearning.FiniteActions public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace diff --git a/LeanMachineLearning/ForMathlib/MeasurableArgMax.lean b/LeanMachineLearning/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/MeasurableArgMax.lean rename to LeanMachineLearning/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean diff --git a/LeanMachineLearning/ForMathlib/StandardBorel.lean b/LeanMachineLearning/MeasureTheory/Constructions/Polish/StandardBorel.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/StandardBorel.lean rename to LeanMachineLearning/MeasureTheory/Constructions/Polish/StandardBorel.lean diff --git a/LeanMachineLearning/ForMathlib/Measurable.lean b/LeanMachineLearning/MeasureTheory/Measurable.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/Measurable.lean rename to LeanMachineLearning/MeasureTheory/Measurable.lean diff --git a/LeanMachineLearning/BanditAlgorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean similarity index 98% rename from LeanMachineLearning/BanditAlgorithms/ETC.lean rename to LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean index 413c8003..5d52c849 100644 --- a/LeanMachineLearning/BanditAlgorithms/ETC.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean @@ -5,9 +5,9 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.Bandit.SumRewards -public import LeanMachineLearning.BanditAlgorithms.RoundRobin -public import LeanMachineLearning.ForMathlib.MeasurableArgMax +public import LeanMachineLearning.Online.Bandit.SumRewards +public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin +public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax /-! # The Explore-Then-Commit Algorithm diff --git a/LeanMachineLearning/BanditAlgorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean similarity index 99% rename from LeanMachineLearning/BanditAlgorithms/UCB.lean rename to LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean index 3eaf2812..e7eeb81d 100644 --- a/LeanMachineLearning/BanditAlgorithms/UCB.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean @@ -5,9 +5,9 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.Bandit.SumRewards -public import LeanMachineLearning.BanditAlgorithms.RoundRobin -public import LeanMachineLearning.ForMathlib.MeasurableArgMax +public import LeanMachineLearning.Online.Bandit.SumRewards +public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin +public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax /-! # UCB algorithm diff --git a/LeanMachineLearning/Bandit/Bandit.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean similarity index 99% rename from LeanMachineLearning/Bandit/Bandit.lean rename to LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index 8101f908..8ada014a 100644 --- a/LeanMachineLearning/Bandit/Bandit.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -5,11 +5,11 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.ForMathlib.CondIndepFun -public import LeanMachineLearning.ForMathlib.IndepFun -public import LeanMachineLearning.ForMathlib.IndepInfinitePi -public import LeanMachineLearning.ForMathlib.Integrable -public import LeanMachineLearning.ForMathlib.StandardBorel +public import LeanMachineLearning.Probability.Independence.CondIndepFun +public import LeanMachineLearning.Probability.Independence.IndepFun +public import LeanMachineLearning.Probability.Independence.IndepInfinitePi +public import LeanMachineLearning.Probability.Integrable +public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel public import LeanMachineLearning.SequentialLearning.FiniteActions public import LeanMachineLearning.SequentialLearning.StationaryEnv public import Mathlib.Probability.Independence.Integration diff --git a/LeanMachineLearning/Bandit/Regret.lean b/LeanMachineLearning/Online/Bandit/Regret.lean similarity index 100% rename from LeanMachineLearning/Bandit/Regret.lean rename to LeanMachineLearning/Online/Bandit/Regret.lean diff --git a/LeanMachineLearning/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean similarity index 99% rename from LeanMachineLearning/Bandit/RewardByCountMeasure.lean rename to LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean index ed0d182d..70c2c047 100644 --- a/LeanMachineLearning/Bandit/RewardByCountMeasure.lean +++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.Bandit.Bandit +public import LeanMachineLearning.Online.Bandit.ArrayProbSpace /-! # Laws of `stepsUntil` and `rewardByCount` -/ diff --git a/LeanMachineLearning/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean similarity index 99% rename from LeanMachineLearning/Bandit/SumRewards.lean rename to LeanMachineLearning/Online/Bandit/SumRewards.lean index 8026bdab..b59606fd 100644 --- a/LeanMachineLearning/Bandit/SumRewards.lean +++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean @@ -5,9 +5,9 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.Bandit.Bandit -public import LeanMachineLearning.Bandit.Regret -public import LeanMachineLearning.ForMathlib.SubGaussian +public import LeanMachineLearning.Online.Bandit.ArrayProbSpace +public import LeanMachineLearning.Online.Bandit.Regret +public import LeanMachineLearning.Probability.Moments.SubGaussian /-! # Law of the sum of rewards -/ diff --git a/LeanMachineLearning/ForMathlib/HasCondDistrib.lean b/LeanMachineLearning/Probability/HasCondDistrib.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/HasCondDistrib.lean rename to LeanMachineLearning/Probability/HasCondDistrib.lean index 2d12fefe..5c293946 100644 --- a/LeanMachineLearning/ForMathlib/HasCondDistrib.lean +++ b/LeanMachineLearning/Probability/HasCondDistrib.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.ForMathlib.CondDistrib +public import LeanMachineLearning.Probability.Independence.CondDistrib public import Mathlib.Probability.HasLaw /-! diff --git a/LeanMachineLearning/ForMathlib/CondDistrib.lean b/LeanMachineLearning/Probability/Independence/CondDistrib.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/CondDistrib.lean rename to LeanMachineLearning/Probability/Independence/CondDistrib.lean index 2f35a721..be0e2d38 100644 --- a/LeanMachineLearning/ForMathlib/CondDistrib.lean +++ b/LeanMachineLearning/Probability/Independence/CondDistrib.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.ForMathlib.KernelSub +public import LeanMachineLearning.Probability.Kernel.KernelSub public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure public import Mathlib.Probability.Independence.Basic public import Mathlib.Probability.Independence.Conditional diff --git a/LeanMachineLearning/ForMathlib/CondIndepFun.lean b/LeanMachineLearning/Probability/Independence/CondIndepFun.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/CondIndepFun.lean rename to LeanMachineLearning/Probability/Independence/CondIndepFun.lean diff --git a/LeanMachineLearning/ForMathlib/IndepFun.lean b/LeanMachineLearning/Probability/Independence/IndepFun.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/IndepFun.lean rename to LeanMachineLearning/Probability/Independence/IndepFun.lean diff --git a/LeanMachineLearning/ForMathlib/IndepInfinitePi.lean b/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/IndepInfinitePi.lean rename to LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean diff --git a/LeanMachineLearning/ForMathlib/Integrable.lean b/LeanMachineLearning/Probability/Integrable.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/Integrable.lean rename to LeanMachineLearning/Probability/Integrable.lean diff --git a/LeanMachineLearning/ForMathlib/Traj.lean b/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/Traj.lean rename to LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean index 107e6bb3..c2b1e190 100644 --- a/LeanMachineLearning/ForMathlib/Traj.lean +++ b/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.ForMathlib.HasCondDistrib +public import LeanMachineLearning.Probability.HasCondDistrib public import Mathlib.Probability.Kernel.IonescuTulcea.Traj public import Mathlib.Probability.Process.FiniteDimensionalLaws diff --git a/LeanMachineLearning/ForMathlib/KernelSub.lean b/LeanMachineLearning/Probability/Kernel/KernelSub.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/KernelSub.lean rename to LeanMachineLearning/Probability/Kernel/KernelSub.lean diff --git a/LeanMachineLearning/ForMathlib/SubGaussian.lean b/LeanMachineLearning/Probability/Moments/SubGaussian.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/SubGaussian.lean rename to LeanMachineLearning/Probability/Moments/SubGaussian.lean diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index db2172f3..aafe1dd2 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithm.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean @@ -5,8 +5,8 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.ForMathlib.Measurable -public import LeanMachineLearning.ForMathlib.Traj +public import LeanMachineLearning.MeasureTheory.Measurable +public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj /-! # Algorithms and environments @@ -312,13 +312,6 @@ lemma IsAlgEnvSeq.filtrationAction_eq_comap end IsAlgEnvSeq -/-- Kernel sending a partial trajectory of the bandit Seq `Iic n → α × ℝ` to a measure -on `ℕ → α × ℝ`, supported on full trajectories that start with the partial one. -/ -noncomputable def traj (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : - Kernel (Iic n → α × R) (ℕ → α × R) := - Kernel.traj (X := fun _ ↦ α × R) (stepKernel alg env) n -deriving IsMarkovKernel - /-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/ noncomputable def trajMeasure (alg : Algorithm α R) (env : Environment α R) : diff --git a/LeanMachineLearning/BanditAlgorithms/AuxSums.lean b/LeanMachineLearning/SequentialLearning/Algorithms/AuxSums.lean similarity index 100% rename from LeanMachineLearning/BanditAlgorithms/AuxSums.lean rename to LeanMachineLearning/SequentialLearning/Algorithms/AuxSums.lean diff --git a/LeanMachineLearning/BanditAlgorithms/RoundRobin.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean similarity index 95% rename from LeanMachineLearning/BanditAlgorithms/RoundRobin.lean rename to LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean index 0be8be67..09d1694b 100644 --- a/LeanMachineLearning/BanditAlgorithms/RoundRobin.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RoundRobin.lean @@ -5,14 +5,15 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.BanditAlgorithms.AuxSums +public import LeanMachineLearning.SequentialLearning.Algorithms.AuxSums public import LeanMachineLearning.SequentialLearning.Deterministic public import LeanMachineLearning.SequentialLearning.FiniteActions public import LeanMachineLearning.SequentialLearning.StationaryEnv /-! # Round-Robin algorithm -That algorithm pulls each arm in a round-robin fashion. +That algorithm pulls each action in a round-robin fashion. +That is, if there are `K` actions, then at time `n`, it pulls the action `n % K`. -/ diff --git a/tutorial/Manual/Pages/DefiningAlgorithm.lean b/tutorial/Manual/Pages/DefiningAlgorithm.lean index 9dba638f..76669dd5 100644 --- a/tutorial/Manual/Pages/DefiningAlgorithm.lean +++ b/tutorial/Manual/Pages/DefiningAlgorithm.lean @@ -135,7 +135,7 @@ To define the algorithm, we first define the exploration bonus and the next acti 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, `measurableArgmax`. -```anchor UCB_def (module := LeanMachineLearning.BanditAlgorithms.UCB) +```anchor UCB_def (module := LeanMachineLearning.Online.Bandit.Algorithms.UCB) /-- The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval. -/ noncomputable def ucbWidth' (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) (a : Fin K) : ℝ := @@ -171,7 +171,7 @@ The last argument `⟨0, hK⟩` is the first action of the algorithm, which is 0 We can now state a theorem about the regret of UCB in a stochastic bandit environment (which we won't prove here). Let's first define the regret, which for stochastic bandits is the difference between the mean rewar that the algorithm would have obtained if it played always the best action, and the sum of mean rewards of the actions played. -```anchor regret (module := LeanMachineLearning.Bandit.Regret) +```anchor regret (module := LeanMachineLearning.Online.Bandit.Regret) def regret (ν : Kernel α ℝ) (A : ℕ → Ω → α) (t : ℕ) (ω : Ω) : ℝ := t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (A s ω))[id] ``` @@ -179,7 +179,7 @@ The quantity `(ν a)[id]` is the mean reward of action `a` in the environment de We can now state the regret bound for UCB. -```anchor UCB.regret_le (module := LeanMachineLearning.BanditAlgorithms.UCB) +```anchor UCB.regret_le (module := LeanMachineLearning.Online.Bandit.Algorithms.UCB) lemma regret_le [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))