Skip to content

Commit f1bfb7d

Browse files
RemyDegenneRemyDegenne
committed
move files to new folders
1 parent 4e687d4 commit f1bfb7d

23 files changed

Lines changed: 46 additions & 52 deletions

File tree

‎LeanMachineLearning.lean‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,26 @@
11
module
22

3-
public import LeanMachineLearning.Bandit.Bandit
4-
public import LeanMachineLearning.Bandit.Regret
5-
public import LeanMachineLearning.Bandit.RewardByCountMeasure
6-
public import LeanMachineLearning.Bandit.SumRewards
7-
public import LeanMachineLearning.BanditAlgorithms.AuxSums
8-
public import LeanMachineLearning.BanditAlgorithms.ETC
9-
public import LeanMachineLearning.BanditAlgorithms.RoundRobin
10-
public import LeanMachineLearning.BanditAlgorithms.UCB
11-
public import LeanMachineLearning.ForMathlib.CondDistrib
12-
public import LeanMachineLearning.ForMathlib.CondIndepFun
13-
public import LeanMachineLearning.ForMathlib.HasCondDistrib
14-
public import LeanMachineLearning.ForMathlib.IndepFun
15-
public import LeanMachineLearning.ForMathlib.IndepInfinitePi
16-
public import LeanMachineLearning.ForMathlib.Integrable
17-
public import LeanMachineLearning.ForMathlib.KernelSub
18-
public import LeanMachineLearning.ForMathlib.Measurable
19-
public import LeanMachineLearning.ForMathlib.MeasurableArgMax
20-
public import LeanMachineLearning.ForMathlib.StandardBorel
21-
public import LeanMachineLearning.ForMathlib.SubGaussian
22-
public import LeanMachineLearning.ForMathlib.Traj
3+
public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
4+
public import LeanMachineLearning.Online.Bandit.Regret
5+
public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
6+
public import LeanMachineLearning.Online.Bandit.SumRewards
7+
public import LeanMachineLearning.Online.Bandit.Algorithms.ETC
8+
public import LeanMachineLearning.Online.Bandit.Algorithms.UCB
9+
public import LeanMachineLearning.Probability.Independence.CondDistrib
10+
public import LeanMachineLearning.Probability.Independence.CondIndepFun
11+
public import LeanMachineLearning.Probability.HasCondDistrib
12+
public import LeanMachineLearning.Probability.Independence.IndepFun
13+
public import LeanMachineLearning.Probability.Independence.IndepInfinitePi
14+
public import LeanMachineLearning.Probability.Integrable
15+
public import LeanMachineLearning.Probability.Kernel.KernelSub
16+
public import LeanMachineLearning.MeasureTheory.Measurable
17+
public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
18+
public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel
19+
public import LeanMachineLearning.Probability.Moments.SubGaussian
20+
public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj
2321
public import LeanMachineLearning.SequentialLearning.Algorithm
22+
public import LeanMachineLearning.SequentialLearning.Algorithms.AuxSums
23+
public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
2424
public import LeanMachineLearning.SequentialLearning.Deterministic
2525
public import LeanMachineLearning.SequentialLearning.FiniteActions
2626
public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace

LeanMachineLearning/ForMathlib/MeasurableArgMax.lean renamed to LeanMachineLearning/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean

File renamed without changes.

LeanMachineLearning/ForMathlib/StandardBorel.lean renamed to LeanMachineLearning/MeasureTheory/Constructions/Polish/StandardBorel.lean

File renamed without changes.

LeanMachineLearning/ForMathlib/Measurable.lean renamed to LeanMachineLearning/MeasureTheory/Measurable.lean

File renamed without changes.

LeanMachineLearning/BanditAlgorithms/ETC.lean renamed to LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ Authors: Rémy Degenne
55
-/
66
module
77

8-
public import LeanMachineLearning.Bandit.SumRewards
9-
public import LeanMachineLearning.BanditAlgorithms.RoundRobin
10-
public import LeanMachineLearning.ForMathlib.MeasurableArgMax
8+
public import LeanMachineLearning.Online.Bandit.SumRewards
9+
public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
10+
public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
1111

1212
/-! # The Explore-Then-Commit Algorithm
1313

LeanMachineLearning/BanditAlgorithms/UCB.lean renamed to LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ Authors: Rémy Degenne
55
-/
66
module
77

8-
public import LeanMachineLearning.Bandit.SumRewards
9-
public import LeanMachineLearning.BanditAlgorithms.RoundRobin
10-
public import LeanMachineLearning.ForMathlib.MeasurableArgMax
8+
public import LeanMachineLearning.Online.Bandit.SumRewards
9+
public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
10+
public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
1111

1212
/-!
1313
# UCB algorithm

LeanMachineLearning/Bandit/Bandit.lean renamed to LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@ Authors: Rémy Degenne, Paulo Rauber
55
-/
66
module
77

8-
public import LeanMachineLearning.ForMathlib.CondIndepFun
9-
public import LeanMachineLearning.ForMathlib.IndepFun
10-
public import LeanMachineLearning.ForMathlib.IndepInfinitePi
11-
public import LeanMachineLearning.ForMathlib.Integrable
12-
public import LeanMachineLearning.ForMathlib.StandardBorel
8+
public import LeanMachineLearning.Probability.Independence.CondIndepFun
9+
public import LeanMachineLearning.Probability.Independence.IndepFun
10+
public import LeanMachineLearning.Probability.Independence.IndepInfinitePi
11+
public import LeanMachineLearning.Probability.Integrable
12+
public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel
1313
public import LeanMachineLearning.SequentialLearning.FiniteActions
1414
public import LeanMachineLearning.SequentialLearning.StationaryEnv
1515
public import Mathlib.Probability.Independence.Integration

LeanMachineLearning/Bandit/Regret.lean renamed to LeanMachineLearning/Online/Bandit/Regret.lean

File renamed without changes.

LeanMachineLearning/Bandit/RewardByCountMeasure.lean renamed to LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Rémy Degenne
55
-/
66
module
77

8-
public import LeanMachineLearning.Bandit.Bandit
8+
public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
99

1010
/-! # Laws of `stepsUntil` and `rewardByCount`
1111
-/

LeanMachineLearning/Bandit/SumRewards.lean renamed to LeanMachineLearning/Online/Bandit/SumRewards.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ Authors: Rémy Degenne
55
-/
66
module
77

8-
public import LeanMachineLearning.Bandit.Bandit
9-
public import LeanMachineLearning.Bandit.Regret
10-
public import LeanMachineLearning.ForMathlib.SubGaussian
8+
public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
9+
public import LeanMachineLearning.Online.Bandit.Regret
10+
public import LeanMachineLearning.Probability.Moments.SubGaussian
1111

1212
/-! # Law of the sum of rewards
1313
-/

0 commit comments

Comments
 (0)