Skip to content

Move files to new folders #88

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 1 commit into from
Apr 19, 2026
Merged

Move files to new folders #88

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 20 additions & 20 deletions LeanMachineLearning.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
0 ...Learning/ForMathlib/MeasurableArgMax.lean → ...ructions/BorelSpace/MeasurableArgMax.lean
View file
Open in desktop
File renamed without changes.
0 ...ineLearning/ForMathlib/StandardBorel.lean → ...y/Constructions/Polish/StandardBorel.lean
View file
Open in desktop
File renamed without changes.
0 ...achineLearning/ForMathlib/Measurable.lean → ...ineLearning/MeasureTheory/Measurable.lean
View file
Open in desktop
File renamed without changes.
6 changes: 3 additions & 3 deletions ...MachineLearning/BanditAlgorithms/ETC.lean → ...earning/Online/Bandit/Algorithms/ETC.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 3 additions & 3 deletions ...MachineLearning/BanditAlgorithms/UCB.lean → ...earning/Online/Bandit/Algorithms/UCB.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions LeanMachineLearning/Bandit/Bandit.lean → ...earning/Online/Bandit/ArrayProbSpace.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
0 LeanMachineLearning/Bandit/Regret.lean → ...MachineLearning/Online/Bandit/Regret.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion ...Learning/Bandit/RewardByCountMeasure.lean → ...g/Online/Bandit/RewardByCountMeasure.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`
-/
Expand Down
6 changes: 3 additions & 3 deletions LeanMachineLearning/Bandit/SumRewards.lean → ...ineLearning/Online/Bandit/SumRewards.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
-/
Expand Down
2 changes: 1 addition & 1 deletion ...neLearning/ForMathlib/HasCondDistrib.lean → ...eLearning/Probability/HasCondDistrib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
2 changes: 1 addition & 1 deletion ...chineLearning/ForMathlib/CondDistrib.lean → ...Probability/Independence/CondDistrib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
0 ...hineLearning/ForMathlib/CondIndepFun.lean → ...robability/Independence/CondIndepFun.lean
View file
Open in desktop
File renamed without changes.
0 LeanMachineLearning/ForMathlib/IndepFun.lean → ...ng/Probability/Independence/IndepFun.lean
View file
Open in desktop
File renamed without changes.
0 ...eLearning/ForMathlib/IndepInfinitePi.lean → ...ability/Independence/IndepInfinitePi.lean
View file
Open in desktop
File renamed without changes.
0 ...achineLearning/ForMathlib/Integrable.lean → ...chineLearning/Probability/Integrable.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion LeanMachineLearning/ForMathlib/Traj.lean → ...robability/Kernel/IonescuTulcea/Traj.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
0 ...MachineLearning/ForMathlib/KernelSub.lean → ...earning/Probability/Kernel/KernelSub.lean
View file
Open in desktop
File renamed without changes.
0 ...chineLearning/ForMathlib/SubGaussian.lean → ...ning/Probability/Moments/SubGaussian.lean
View file
Open in desktop
File renamed without changes.
11 changes: 2 additions & 9 deletions LeanMachineLearning/SequentialLearning/Algorithm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) :
Expand Down
0 ...ineLearning/BanditAlgorithms/AuxSums.lean → ...equentialLearning/Algorithms/AuxSums.lean
View file
Open in desktop
File renamed without changes.
5 changes: 3 additions & 2 deletions ...Learning/BanditAlgorithms/RoundRobin.lean → ...entialLearning/Algorithms/RoundRobin.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

-/

Expand Down
6 changes: 3 additions & 3 deletions tutorial/Manual/Pages/DefiningAlgorithm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) : ℝ :=
Expand Down Expand Up @@ -171,15 +171,15 @@ 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]
```
The quantity `(ν a)[id]` is the mean reward of action `a` in the environment defined by `ν`.

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))
Expand Down
Loading