Add randomSampling

LeanMachineLearning.lean

@@ -1,24 +1,25 @@
-module
+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.Online.Bandit.Algorithms.ETC
-public import LeanMachineLearning.Online.Bandit.Algorithms.UCB
+public import LeanMachineLearning.Probability.HasCondDistrib
 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.IonescuTulcea.Traj
 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.RandomSampling
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
 public import LeanMachineLearning.SequentialLearning.Deterministic
 public import LeanMachineLearning.SequentialLearning.FiniteActions

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

LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean

@@ -0,0 +1,79 @@
+/-
+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_action`: Each action follows the distribution μ.
+* `iIndep_action`: Actions are mutually independent across time steps.
+-/
+
+@[expose] public section
+
+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]
+
+open Set in
+/-- 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 _ μ
+  p0 := μ
+
+namespace randomSampling
+
+variable {A : ℕ → Ω → α} {R : ℕ → Ω → β} {env : Environment α β}
+
+/-- Each action follows the distribution μ. -/
+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
+  · 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_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_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
+    exact (condDistrib_eq.comp meas_fst measurable_id).symm
+  · exact (IsAlgEnvSeq.measurable_hist (h.measurable_A) (h.measurable_R) n).aemeasurable
+
+end randomSampling
+
+end Learning