diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 5b083852..a1b3036b 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -27,7 +27,7 @@ We generally follow the [Mathlib style for coding and documentation](https://lea We place new material about machine learning in the `Learning` namespace, in an appropriate folder (e.g. `Online/Bandit` for bandits). -For results about definitions from Mathlib, we place them in the same namespace as the original definition (typically `MeasureTheory` or `ProbabilityTheory`), and in a folder that corresponds to where they would be if added to Mathlib (e.g. `Probability/Independence` for results about independence). +For results about definitions from Mathlib, we place them in the same namespace as the original definition (typically `MeasureTheory` or `ProbabilityTheory`), and in a subfolder of the `ForMathlib` folder that corresponds to where they would be if added to Mathlib (e.g. `ForMathlib/Probability/Independence` for results about independence). The `Tutorial` folder is reserved for material used in the tutorial, and should not be used for general contributions. diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 684e4461..9f0ad402 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,29 +1,29 @@ module -- shake: keep-all --deprecated_module: ignore -public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax -public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel -public import LeanMachineLearning.MeasureTheory.Measurable -public import LeanMachineLearning.MeasureTheory.Measure.AbsolutelyContinuous -public import LeanMachineLearning.MeasureTheory.OuterMeasure.Basic +public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax +public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel +public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable +public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous +public import LeanMachineLearning.ForMathlib.MeasureTheory.OuterMeasure.Basic +public import LeanMachineLearning.ForMathlib.Probability.HasCondDistrib +public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib +public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun +public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun +public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi +public import LeanMachineLearning.ForMathlib.Probability.Integrable +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Basic +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MeasureCompProd +public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj +public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub +public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian +public import LeanMachineLearning.ForMathlib.Probability.WithDensity public import LeanMachineLearning.Online.Bandit.Algorithms.ETC public import LeanMachineLearning.Online.Bandit.Algorithms.UCB 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.Probability.HasCondDistrib -public import LeanMachineLearning.Probability.Independence.CondDistrib -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.Probability.Kernel.Basic -public import LeanMachineLearning.Probability.Kernel.Composition.MapComap -public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd -public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj -public import LeanMachineLearning.Probability.Kernel.KernelSub -public import LeanMachineLearning.Probability.Moments.SubGaussian -public import LeanMachineLearning.Probability.WithDensity public import LeanMachineLearning.SequentialLearning.Algorithm public import LeanMachineLearning.SequentialLearning.AlgorithmDensity public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling diff --git a/LeanMachineLearning/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean similarity index 100% rename from LeanMachineLearning/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean rename to LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean diff --git a/LeanMachineLearning/MeasureTheory/Constructions/Polish/StandardBorel.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/Polish/StandardBorel.lean similarity index 100% rename from LeanMachineLearning/MeasureTheory/Constructions/Polish/StandardBorel.lean rename to LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/Polish/StandardBorel.lean diff --git a/LeanMachineLearning/MeasureTheory/Measurable.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Measurable.lean similarity index 100% rename from LeanMachineLearning/MeasureTheory/Measurable.lean rename to LeanMachineLearning/ForMathlib/MeasureTheory/Measurable.lean diff --git a/LeanMachineLearning/MeasureTheory/Measure/AbsolutelyContinuous.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean similarity index 89% rename from LeanMachineLearning/MeasureTheory/Measure/AbsolutelyContinuous.lean rename to LeanMachineLearning/ForMathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean index 41b0522d..2a6cfaa5 100644 --- a/LeanMachineLearning/MeasureTheory/Measure/AbsolutelyContinuous.lean +++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean @@ -6,7 +6,7 @@ Authors: Paulo Rauber module public import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous -public import LeanMachineLearning.MeasureTheory.OuterMeasure.Basic +public import LeanMachineLearning.ForMathlib.MeasureTheory.OuterMeasure.Basic /-! # Lemma about measures that assign non-zero probability to every singleton. diff --git a/LeanMachineLearning/MeasureTheory/OuterMeasure/Basic.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/OuterMeasure/Basic.lean similarity index 100% rename from LeanMachineLearning/MeasureTheory/OuterMeasure/Basic.lean rename to LeanMachineLearning/ForMathlib/MeasureTheory/OuterMeasure/Basic.lean diff --git a/LeanMachineLearning/Probability/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean similarity index 99% rename from LeanMachineLearning/Probability/HasCondDistrib.lean rename to LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean index ab497f48..0ab08b0c 100644 --- a/LeanMachineLearning/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/HasCondDistrib.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.Probability.Independence.CondDistrib +public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib public import Mathlib.Probability.HasLaw /-! diff --git a/LeanMachineLearning/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean similarity index 99% rename from LeanMachineLearning/Probability/Independence/CondDistrib.lean rename to LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean index 18a015e9..90d24c0f 100644 --- a/LeanMachineLearning/Probability/Independence/CondDistrib.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.Probability.Kernel.KernelSub +public import LeanMachineLearning.ForMathlib.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/Probability/Independence/CondIndepFun.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondIndepFun.lean similarity index 100% rename from LeanMachineLearning/Probability/Independence/CondIndepFun.lean rename to LeanMachineLearning/ForMathlib/Probability/Independence/CondIndepFun.lean diff --git a/LeanMachineLearning/Probability/Independence/IndepFun.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean similarity index 100% rename from LeanMachineLearning/Probability/Independence/IndepFun.lean rename to LeanMachineLearning/ForMathlib/Probability/Independence/IndepFun.lean diff --git a/LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/IndepInfinitePi.lean similarity index 100% rename from LeanMachineLearning/Probability/Independence/IndepInfinitePi.lean rename to LeanMachineLearning/ForMathlib/Probability/Independence/IndepInfinitePi.lean diff --git a/LeanMachineLearning/Probability/Integrable.lean b/LeanMachineLearning/ForMathlib/Probability/Integrable.lean similarity index 100% rename from LeanMachineLearning/Probability/Integrable.lean rename to LeanMachineLearning/ForMathlib/Probability/Integrable.lean diff --git a/LeanMachineLearning/Probability/Kernel/Basic.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/Basic.lean similarity index 100% rename from LeanMachineLearning/Probability/Kernel/Basic.lean rename to LeanMachineLearning/ForMathlib/Probability/Kernel/Basic.lean diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/Composition/MapComap.lean similarity index 100% rename from LeanMachineLearning/Probability/Kernel/Composition/MapComap.lean rename to LeanMachineLearning/ForMathlib/Probability/Kernel/Composition/MapComap.lean diff --git a/LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/Composition/MeasureCompProd.lean similarity index 100% rename from LeanMachineLearning/Probability/Kernel/Composition/MeasureCompProd.lean rename to LeanMachineLearning/ForMathlib/Probability/Kernel/Composition/MeasureCompProd.lean diff --git a/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean similarity index 99% rename from LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean rename to LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean index d63260e3..9cc32932 100644 --- a/LeanMachineLearning/Probability/Kernel/IonescuTulcea/Traj.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/IonescuTulcea/Traj.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.Probability.HasCondDistrib +public import LeanMachineLearning.ForMathlib.Probability.HasCondDistrib public import Mathlib.Probability.Kernel.IonescuTulcea.Traj public import Mathlib.Probability.Process.FiniteDimensionalLaws diff --git a/LeanMachineLearning/Probability/Kernel/KernelSub.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean similarity index 100% rename from LeanMachineLearning/Probability/Kernel/KernelSub.lean rename to LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean diff --git a/LeanMachineLearning/Probability/Moments/SubGaussian.lean b/LeanMachineLearning/ForMathlib/Probability/Moments/SubGaussian.lean similarity index 100% rename from LeanMachineLearning/Probability/Moments/SubGaussian.lean rename to LeanMachineLearning/ForMathlib/Probability/Moments/SubGaussian.lean diff --git a/LeanMachineLearning/Probability/WithDensity.lean b/LeanMachineLearning/ForMathlib/Probability/WithDensity.lean similarity index 100% rename from LeanMachineLearning/Probability/WithDensity.lean rename to LeanMachineLearning/ForMathlib/Probability/WithDensity.lean diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean index ae0cb0b5..6d93ccc6 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean @@ -7,7 +7,7 @@ module public import LeanMachineLearning.Online.Bandit.SumRewards public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin -public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax +public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax /-! # The Explore-Then-Commit Algorithm diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean index 95c19210..94adc7c3 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean @@ -7,7 +7,7 @@ module public import LeanMachineLearning.Online.Bandit.SumRewards public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin -public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax +public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax /-! # UCB algorithm diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean index b8467ae4..392c1453 100644 --- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean +++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean @@ -5,11 +5,11 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.MeasureTheory.Constructions.Polish.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.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel +public import LeanMachineLearning.ForMathlib.Probability.Independence.CondIndepFun +public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun +public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi +public import LeanMachineLearning.ForMathlib.Probability.Integrable public import LeanMachineLearning.SequentialLearning.FiniteActions public import LeanMachineLearning.SequentialLearning.StationaryEnv public import Mathlib.Probability.Independence.Integration diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean index 48b7e0ba..78d8024f 100644 --- a/LeanMachineLearning/Online/Bandit/SumRewards.lean +++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean @@ -5,9 +5,9 @@ Authors: Rémy Degenne -/ module +public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian public import LeanMachineLearning.Online.Bandit.ArrayProbSpace public import LeanMachineLearning.Online.Bandit.Regret -public import LeanMachineLearning.Probability.Moments.SubGaussian public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace /-! # Law of the sum of rewards diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean index 90057837..65095fce 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.MeasureTheory.Measurable -public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj +public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable +public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj /-! # Algorithms and environments diff --git a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean index 4812c94a..50a5ef43 100644 --- a/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean +++ b/LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean @@ -5,8 +5,8 @@ Authors: Paulo Rauber -/ module -public import LeanMachineLearning.Probability.Kernel.Composition.MeasureCompProd -public import LeanMachineLearning.Probability.WithDensity +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MeasureCompProd +public import LeanMachineLearning.ForMathlib.Probability.WithDensity public import LeanMachineLearning.SequentialLearning.Algorithm /-! diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean index 324d2979..63c69644 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -5,7 +5,7 @@ Authors: Gaëtan Serré -/ module -public import LeanMachineLearning.Probability.Independence.IndepFun +public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepFun public import LeanMachineLearning.SequentialLearning.Algorithm /-! diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean b/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean index e9b60f3f..7194d61a 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean @@ -5,7 +5,7 @@ Authors: Paulo Rauber, Rémy Degenne -/ module -public import LeanMachineLearning.MeasureTheory.Measure.AbsolutelyContinuous +public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous public import LeanMachineLearning.SequentialLearning.AlgorithmDensity public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling diff --git a/LeanMachineLearning/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index 17bd24df..60f4929b 100644 --- a/LeanMachineLearning/SequentialLearning/Deterministic.lean +++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne -/ module -public import LeanMachineLearning.Probability.Kernel.Basic +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Basic public import LeanMachineLearning.SequentialLearning.Algorithm /-! diff --git a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean index 2a339656..bca3e668 100644 --- a/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean +++ b/LeanMachineLearning/SequentialLearning/EvaluationEnv.lean @@ -7,7 +7,7 @@ module public import LeanMachineLearning.SequentialLearning.Deterministic public import LeanMachineLearning.SequentialLearning.StationaryEnv -public import LeanMachineLearning.Probability.Independence.CondDistrib +public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib /-! # Function evaluation environments diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean index 048e35bf..a479ca1e 100644 --- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean +++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean @@ -5,7 +5,7 @@ Authors: Rémy Degenne, Paulo Rauber -/ module -public import LeanMachineLearning.Probability.Kernel.Composition.MapComap +public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap public import LeanMachineLearning.SequentialLearning.Algorithm /-!