From 5f1296502be424725c4e66f63dc1321419113f02 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 21 May 2026 12:56:48 +0200 Subject: [PATCH 1/3] move files about Mathlib objects to a ForMathlib folder --- CONTRIBUTING.md | 2 +- LeanMachineLearning.lean | 28 +++++++++---------- .../BorelSpace/MeasurableArgMax.lean | 0 .../Constructions/Polish/StandardBorel.lean | 0 .../MeasureTheory/Measurable.lean | 0 .../Probability/HasCondDistrib.lean | 2 +- .../Probability/Independence/CondDistrib.lean | 2 +- .../Independence/CondIndepFun.lean | 0 .../Probability/Independence/IndepFun.lean | 0 .../Independence/IndepInfinitePi.lean | 0 .../Probability/Integrable.lean | 0 .../Probability/Kernel/Basic.lean | 0 .../Kernel/Composition/MapComap.lean | 0 .../Kernel/IonescuTulcea/Traj.lean | 2 +- .../Probability/Kernel/KernelSub.lean | 0 .../Probability/Moments/SubGaussian.lean | 0 .../Online/Bandit/Algorithms/ETC.lean | 2 +- .../Online/Bandit/Algorithms/UCB.lean | 2 +- .../Online/Bandit/ArrayProbSpace.lean | 10 +++---- .../Online/Bandit/SumRewards.lean | 2 +- .../SequentialLearning/Algorithm.lean | 4 +-- .../Algorithms/RandomSampling.lean | 2 +- .../SequentialLearning/Deterministic.lean | 2 +- .../SequentialLearning/EvaluationEnv.lean | 2 +- .../SequentialLearning/StationaryEnv.lean | 2 +- 25 files changed, 32 insertions(+), 32 deletions(-) rename LeanMachineLearning/{ => ForMathlib}/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/MeasureTheory/Constructions/Polish/StandardBorel.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/MeasureTheory/Measurable.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/HasCondDistrib.lean (99%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Independence/CondDistrib.lean (99%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Independence/CondIndepFun.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Independence/IndepFun.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Independence/IndepInfinitePi.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Integrable.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Kernel/Basic.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Kernel/Composition/MapComap.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Kernel/IonescuTulcea/Traj.lean (99%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Kernel/KernelSub.lean (100%) rename LeanMachineLearning/{ => ForMathlib}/Probability/Moments/SubGaussian.lean (100%) 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 7d539fc3..cce57503 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,25 +1,25 @@ module -- shake: keep-all -public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax -public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel -public import LeanMachineLearning.MeasureTheory.Measurable +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.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.IonescuTulcea.Traj +public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub +public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian 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.IonescuTulcea.Traj -public import LeanMachineLearning.Probability.Kernel.KernelSub -public import LeanMachineLearning.Probability.Moments.SubGaussian public import LeanMachineLearning.SequentialLearning.Algorithm public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin 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/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 d4fdf44f..782d6d79 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 98b6f974..ffc35e9d 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/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 c2b1e190..ba0c373e 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/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean index 054ff2d1..f6a204ab 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 4ec80488..3a3c1ffa 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 466eb7f4..64ec7cd8 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 140d762c..412d7df7 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 2662ecf6..70fc5376 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/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/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean index 4411541d..9606712f 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 6a658c93..fc17c43b 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 /-! From 11249690714bfec2ba518accde4435fda47161cd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 16 Jun 2026 17:16:21 +0200 Subject: [PATCH 2/3] lake exe mk_all --- LeanMachineLearning.lean | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 1716f3d2..9f0ad402 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,9 +1,10 @@ module -- shake: keep-all --deprecated_module: ignore - 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 @@ -12,28 +13,17 @@ public import LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfin 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 From a67d8a13801e8e7bf7df8394c77bf2422ef75dff Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 16 Jun 2026 17:18:36 +0200 Subject: [PATCH 3/3] fix --- .../MeasureTheory/Measure/AbsolutelyContinuous.lean | 2 +- LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean | 4 ++-- .../SequentialLearning/Algorithms/Uniform.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean index 41b0522d..2a6cfaa5 100644 --- a/LeanMachineLearning/ForMathlib/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/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/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