Skip to content

Move files about Mathlib objects to a ForMathlib folder #110

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 4 commits into from
Jun 16, 2026
Merged

Move files about Mathlib objects to a ForMathlib folder #110

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
5f12965
move files about Mathlib objects to a ForMathlib folder
RemyDegenne May 21, 2026
40ceab0
Merge remote-tracking branch 'origin/main' into cleanup
RemyDegenne Jun 16, 2026
1124969
lake exe mk_all
RemyDegenne Jun 16, 2026
a67d8a1
fix
RemyDegenne Jun 16, 2026
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
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
36 changes: 18 additions & 18 deletions LeanMachineLearning.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
0 ...ructions/BorelSpace/MeasurableArgMax.lean → ...ructions/BorelSpace/MeasurableArgMax.lean
View file
Open in desktop
File renamed without changes.
0 ...y/Constructions/Polish/StandardBorel.lean → ...y/Constructions/Polish/StandardBorel.lean
View file
Open in desktop
File renamed without changes.
0 ...ineLearning/MeasureTheory/Measurable.lean → .../ForMathlib/MeasureTheory/Measurable.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion ...eTheory/Measure/AbsolutelyContinuous.lean → ...eTheory/Measure/AbsolutelyContinuous.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
0 ...ing/MeasureTheory/OuterMeasure/Basic.lean → ...lib/MeasureTheory/OuterMeasure/Basic.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion ...eLearning/Probability/HasCondDistrib.lean → ...orMathlib/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.Probability.Independence.CondDistrib
public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib
public import Mathlib.Probability.HasLaw

/-!
Expand Down
2 changes: 1 addition & 1 deletion ...Probability/Independence/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.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
Expand Down
0 ...robability/Independence/CondIndepFun.lean → ...robability/Independence/CondIndepFun.lean
View file
Open in desktop
File renamed without changes.
0 ...ng/Probability/Independence/IndepFun.lean → ...ib/Probability/Independence/IndepFun.lean
View file
Open in desktop
File renamed without changes.
0 ...ability/Independence/IndepInfinitePi.lean → ...ability/Independence/IndepInfinitePi.lean
View file
Open in desktop
File renamed without changes.
0 ...chineLearning/Probability/Integrable.lean → ...ng/ForMathlib/Probability/Integrable.lean
View file
Open in desktop
File renamed without changes.
0 ...ineLearning/Probability/Kernel/Basic.lean → .../ForMathlib/Probability/Kernel/Basic.lean
View file
Open in desktop
File renamed without changes.
0 ...bability/Kernel/Composition/MapComap.lean → ...bability/Kernel/Composition/MapComap.lean
View file
Open in desktop
File renamed without changes.
0 ...y/Kernel/Composition/MeasureCompProd.lean → ...y/Kernel/Composition/MeasureCompProd.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion ...robability/Kernel/IonescuTulcea/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.Probability.HasCondDistrib
public import LeanMachineLearning.ForMathlib.Probability.HasCondDistrib
public import Mathlib.Probability.Kernel.IonescuTulcea.Traj
public import Mathlib.Probability.Process.FiniteDimensionalLaws

Expand Down
0 ...earning/Probability/Kernel/KernelSub.lean → ...Mathlib/Probability/Kernel/KernelSub.lean
View file
Open in desktop
File renamed without changes.
0 ...ning/Probability/Moments/SubGaussian.lean → ...hlib/Probability/Moments/SubGaussian.lean
View file
Open in desktop
File renamed without changes.
0 ...hineLearning/Probability/WithDensity.lean → ...g/ForMathlib/Probability/WithDensity.lean
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions LeanMachineLearning/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.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
Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/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.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
Expand Down
4 changes: 2 additions & 2 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.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
Expand Down
4 changes: 2 additions & 2 deletions LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/SequentialLearning/Deterministic.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.Probability.Kernel.Basic
public import LeanMachineLearning.ForMathlib.Probability.Kernel.Basic
public import LeanMachineLearning.SequentialLearning.Algorithm

/-!
Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/SequentialLearning/EvaluationEnv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion LeanMachineLearning/SequentialLearning/StationaryEnv.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.Probability.Kernel.Composition.MapComap
public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap
public import LeanMachineLearning.SequentialLearning.Algorithm

/-!
Expand Down
Loading