From b6f1dde0255028d774d328d411b76bc9a490f9aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Wed, 22 Apr 2026 10:44:49 +0200 Subject: [PATCH 1/5] `randomSampling` --- LeanMachineLearning.lean | 51 +++++++------ .../Probability/HasCondDistrib.lean | 13 ++++ .../Algorithms/RandomSampling.lean | 74 +++++++++++++++++++ 3 files changed, 112 insertions(+), 26 deletions(-) create mode 100644 LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 731b3ebc..72389d67 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,26 +1,25 @@ -module - -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.RoundRobin -public import LeanMachineLearning.SequentialLearning.Deterministic -public import LeanMachineLearning.SequentialLearning.FiniteActions -public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace -public import LeanMachineLearning.SequentialLearning.StationaryEnv +import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax +import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel +import LeanMachineLearning.MeasureTheory.Measurable +import LeanMachineLearning.Online.Bandit.Algorithms.ETC +import LeanMachineLearning.Online.Bandit.Algorithms.UCB +import LeanMachineLearning.Online.Bandit.ArrayProbSpace +import LeanMachineLearning.Online.Bandit.Regret +import LeanMachineLearning.Online.Bandit.RewardByCountMeasure +import LeanMachineLearning.Online.Bandit.SumRewards +import LeanMachineLearning.Probability.HasCondDistrib +import LeanMachineLearning.Probability.Independence.CondDistrib +import LeanMachineLearning.Probability.Independence.CondIndepFun +import LeanMachineLearning.Probability.Independence.IndepFun +import LeanMachineLearning.Probability.Independence.IndepInfinitePi +import LeanMachineLearning.Probability.Integrable +import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj +import LeanMachineLearning.Probability.Kernel.KernelSub +import LeanMachineLearning.Probability.Moments.SubGaussian +import LeanMachineLearning.SequentialLearning.Algorithm +import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling +import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin +import LeanMachineLearning.SequentialLearning.Deterministic +import LeanMachineLearning.SequentialLearning.FiniteActions +import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace +import LeanMachineLearning.SequentialLearning.StationaryEnv diff --git a/LeanMachineLearning/Probability/HasCondDistrib.lean b/LeanMachineLearning/Probability/HasCondDistrib.lean index 5c293946..3b400bab 100644 --- a/LeanMachineLearning/Probability/HasCondDistrib.lean +++ b/LeanMachineLearning/Probability/HasCondDistrib.lean @@ -220,4 +220,17 @@ lemma HasCondDistrib.prod [IsFiniteMeasure μ] [IsFiniteKernel κ] AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] rfl +lemma hasLaw_of_hasCondDistrib_const [IsProbabilityMeasure μ] {Q : Measure Ω} [SFinite Q] + (h : HasCondDistrib Y X (Kernel.const _ Q) μ) : HasLaw Y Q μ := by + obtain ⟨hY, hX, h⟩ := h + refine ⟨hY, ?_⟩ + have h_snd : (μ.map (fun ω => (X ω, Y ω))).snd = Q := by + have h_map : μ.map (fun ω => (X ω, Y ω)) = (μ.map X) ⊗ₘ (Kernel.const _ Q) := + have h_map : μ.map (fun ω => (X ω, Y ω)) = (μ.map X) ⊗ₘ (condDistrib Y X μ) := + (compProd_map_condDistrib hY).symm + h_map.trans (Measure.compProd_congr h) + rw [h_map, MeasureTheory.Measure.snd_compProd] + simp [MeasureTheory.Measure.map_apply_of_aemeasurable hX] + rwa [Measure.snd_map_prodMk₀ hX] at h_snd + end ProbabilityTheory diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean new file mode 100644 index 00000000..5381d78e --- /dev/null +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 Gaëtan Serré. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gaëtan Serré +-/ +module + +public import LeanMachineLearning.Probability.Independence.IndepFun +public import LeanMachineLearning.SequentialLearning.Algorithm + +/-! +# Random Sampling + +Implementation of the _Random Sampling_ algorithm, which samples from a fixed probability +measure at each iteration. + +## Main definitions + +* `randomSampling`: The random sampling algorithm that samples from a fixed distribution at +each iteration. + +## Main statements + +* `hasLaw_actions`: Each action follows the distribution μ. +* `iIndep_actions`: Actions are mutually independent across time steps. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Learning Finset ENNReal Filter + +open scoped Topology + +variable {α β Ω : Type*} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [Nonempty α] + [StandardBorelSpace β] [Nonempty β] {μ : Measure α} [IsProbabilityMeasure μ] [MeasurableSpace Ω] + {P : Measure Ω} [IsProbabilityMeasure P] + +open Set in +/-- The Pure Random Search algorithm. -/ +@[simps] +noncomputable def randomSampling (μ : Measure α) [IsProbabilityMeasure μ] : Algorithm α β where + policy _ := Kernel.const _ μ + p0 := μ + +namespace randomSampling + +variable {A : ℕ → Ω → α} {R : ℕ → Ω → β} {f : α → β} (hf : Measurable f) + +/-- Each action follows the distribution μ. -/ +lemma hasLaw_actions {env : Environment α β} + (h : IsAlgEnvSeq A R (randomSampling μ) env P) (n : ℕ) : HasLaw (A n) μ P := by + by_cases hn : n = 0 + · rw [hn] + exact h.hasLaw_action_zero + · push Not at hn + obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn + exact hasLaw_of_hasCondDistrib_const <| h.hasCondDistrib_action k + +/-- Actions are mutually independent. -/ +lemma iIndep_actions {env : Environment α β} + (h : IsAlgEnvSeq A R (randomSampling μ) env P) : iIndepFun A P := by + have hA := h.measurable_A + rw [iIndepFun_nat_iff_forall_indepFun (by fun_prop)] + intro n + have condDistrib_eq := (h.hasCondDistrib_action n).condDistrib_eq + simp only [randomSampling_policy] at condDistrib_eq + have law_eq := (hasLaw_actions h (n + 1)).map_eq + rw [← law_eq, ← indepFun_iff_condDistrib_eq_const ?_ (by fun_prop)] at condDistrib_eq + · have meas_fst : Measurable (fun (f : Iic n → α × β) ↦ (fun i ↦ (f i).1)) := by + fun_prop + exact (condDistrib_eq.comp meas_fst measurable_id).symm + · exact (IsAlgEnvSeq.measurable_hist (h.measurable_A) (h.measurable_R) n).aemeasurable + +end randomSampling From 6da1c6193f5d95e4810f6e0edf4700cf3fcf4208 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= <56162277+gaetanserre@users.noreply.github.com> Date: Thu, 23 Apr 2026 10:59:05 +0200 Subject: [PATCH 2/5] Update LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Rémy Degenne --- .../SequentialLearning/Algorithms/RandomSampling.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean index 5381d78e..368b69ae 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -44,7 +44,7 @@ noncomputable def randomSampling (μ : Measure α) [IsProbabilityMeasure μ] : A namespace randomSampling -variable {A : ℕ → Ω → α} {R : ℕ → Ω → β} {f : α → β} (hf : Measurable f) +variable {A : ℕ → Ω → α} {R : ℕ → Ω → β} /-- Each action follows the distribution μ. -/ lemma hasLaw_actions {env : Environment α β} From 815c3f218856e48a7ab6b9b821611f4edcd2975c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Thu, 23 Apr 2026 11:01:36 +0200 Subject: [PATCH 3/5] suggestions --- .../Algorithms/RandomSampling.lean | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean index 368b69ae..d864091f 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -21,8 +21,8 @@ each iteration. ## Main statements -* `hasLaw_actions`: Each action follows the distribution μ. -* `iIndep_actions`: Actions are mutually independent across time steps. +* `hasLaw_action`: Each action follows the distribution μ. +* `iIndep_action`: Actions are mutually independent across time steps. -/ @[expose] public section @@ -31,6 +31,8 @@ open MeasureTheory ProbabilityTheory Learning Finset ENNReal Filter open scoped Topology +namespace Learning + variable {α β Ω : Type*} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace β] [Nonempty β] {μ : Measure α} [IsProbabilityMeasure μ] [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] @@ -44,11 +46,11 @@ noncomputable def randomSampling (μ : Measure α) [IsProbabilityMeasure μ] : A namespace randomSampling -variable {A : ℕ → Ω → α} {R : ℕ → Ω → β} +variable {A : ℕ → Ω → α} {R : ℕ → Ω → β} {env : Environment α β} /-- Each action follows the distribution μ. -/ -lemma hasLaw_actions {env : Environment α β} - (h : IsAlgEnvSeq A R (randomSampling μ) env P) (n : ℕ) : HasLaw (A n) μ P := by +lemma hasLaw_action (h : IsAlgEnvSeq A R (randomSampling μ) env P) (n : ℕ) : + HasLaw (A n) μ P := by by_cases hn : n = 0 · rw [hn] exact h.hasLaw_action_zero @@ -57,14 +59,14 @@ lemma hasLaw_actions {env : Environment α β} exact hasLaw_of_hasCondDistrib_const <| h.hasCondDistrib_action k /-- Actions are mutually independent. -/ -lemma iIndep_actions {env : Environment α β} - (h : IsAlgEnvSeq A R (randomSampling μ) env P) : iIndepFun A P := by +lemma iIndep_action (h : IsAlgEnvSeq A R (randomSampling μ) env P) : + iIndepFun A P := by have hA := h.measurable_A rw [iIndepFun_nat_iff_forall_indepFun (by fun_prop)] intro n have condDistrib_eq := (h.hasCondDistrib_action n).condDistrib_eq simp only [randomSampling_policy] at condDistrib_eq - have law_eq := (hasLaw_actions h (n + 1)).map_eq + have law_eq := (hasLaw_action h (n + 1)).map_eq rw [← law_eq, ← indepFun_iff_condDistrib_eq_const ?_ (by fun_prop)] at condDistrib_eq · have meas_fst : Measurable (fun (f : Iic n → α × β) ↦ (fun i ↦ (f i).1)) := by fun_prop @@ -72,3 +74,5 @@ lemma iIndep_actions {env : Environment α β} · exact (IsAlgEnvSeq.measurable_hist (h.measurable_A) (h.measurable_R) n).aemeasurable end randomSampling + +end Learning From a8669a125db567471acc9a97724ab333ae7f8673 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Thu, 23 Apr 2026 11:04:27 +0200 Subject: [PATCH 4/5] `lake exe mk_all --module` --- LeanMachineLearning.lean | 52 +++++++++++++++++++++------------------- 1 file changed, 27 insertions(+), 25 deletions(-) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 72389d67..48b50f1e 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,25 +1,27 @@ -import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax -import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel -import LeanMachineLearning.MeasureTheory.Measurable -import LeanMachineLearning.Online.Bandit.Algorithms.ETC -import LeanMachineLearning.Online.Bandit.Algorithms.UCB -import LeanMachineLearning.Online.Bandit.ArrayProbSpace -import LeanMachineLearning.Online.Bandit.Regret -import LeanMachineLearning.Online.Bandit.RewardByCountMeasure -import LeanMachineLearning.Online.Bandit.SumRewards -import LeanMachineLearning.Probability.HasCondDistrib -import LeanMachineLearning.Probability.Independence.CondDistrib -import LeanMachineLearning.Probability.Independence.CondIndepFun -import LeanMachineLearning.Probability.Independence.IndepFun -import LeanMachineLearning.Probability.Independence.IndepInfinitePi -import LeanMachineLearning.Probability.Integrable -import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj -import LeanMachineLearning.Probability.Kernel.KernelSub -import LeanMachineLearning.Probability.Moments.SubGaussian -import LeanMachineLearning.SequentialLearning.Algorithm -import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling -import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin -import LeanMachineLearning.SequentialLearning.Deterministic -import LeanMachineLearning.SequentialLearning.FiniteActions -import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace -import LeanMachineLearning.SequentialLearning.StationaryEnv +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.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.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 +public import LeanMachineLearning.SequentialLearning.Deterministic +public import LeanMachineLearning.SequentialLearning.FiniteActions +public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace +public import LeanMachineLearning.SequentialLearning.StationaryEnv From 92f106256c3915b067910ab4e21bd7bc677c784e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Thu, 23 Apr 2026 11:12:06 +0200 Subject: [PATCH 5/5] docstring --- .../SequentialLearning/Algorithms/RandomSampling.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean index d864091f..f6a35718 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -38,7 +38,8 @@ variable {α β Ω : Type*} [MeasurableSpace α] [MeasurableSpace β] [StandardB {P : Measure Ω} [IsProbabilityMeasure P] open Set in -/-- The Pure Random Search algorithm. -/ +/-- The _Random Sampling_ algorithm, which samples from a fixed probability +measure at each iteration. -/ @[simps] noncomputable def randomSampling (μ : Measure α) [IsProbabilityMeasure μ] : Algorithm α β where policy _ := Kernel.const _ μ