Include uniformAlgorithm and related files

LeanMachineLearning.lean

@@ -3,6 +3,8 @@ 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.Online.Bandit.Algorithms.ETC
 public import LeanMachineLearning.Online.Bandit.Algorithms.UCB
 public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
@@ -26,6 +28,7 @@ public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
+public import LeanMachineLearning.SequentialLearning.Algorithms.Uniform
 public import LeanMachineLearning.SequentialLearning.Deterministic
 public import LeanMachineLearning.SequentialLearning.EvaluationEnv
 public import LeanMachineLearning.SequentialLearning.FiniteActions

LeanMachineLearning/MeasureTheory/Measure/AbsolutelyContinuous.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Paulo Rauber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paulo Rauber
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
+public import LeanMachineLearning.MeasureTheory.OuterMeasure.Basic
+
+/-!
+# Lemma about measures that assign non-zero probability to every singleton.
+-/
+
+@[expose] public section
+
+variable {α : Type*}
+
+namespace MeasureTheory
+
+variable {mα : MeasurableSpace α} {μ ν : Measure α}
+
+namespace Measure
+
+lemma absolutelyContinuous_of_measure_singleton_ne_zero (h : ∀ a, ν {a} ≠ 0) : μ ≪ ν :=
+  fun s hs ↦ by simp [(measure_null_iff_eq_empty_of_measure_singleton_ne_zero h).1 hs]
+
+end Measure
+
+end MeasureTheory

LeanMachineLearning/MeasureTheory/OuterMeasure/Basic.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Paulo Rauber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paulo Rauber
+-/
+module
+
+public import Mathlib.MeasureTheory.OuterMeasure.Basic
+
+/-!
+# Lemma about measures that assign non-zero probability to every singleton.
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+section OuterMeasureClass
+
+variable {α F : Type*} [FunLike F (Set α) ℝ≥0∞] [OuterMeasureClass F α]
+  {μ : F} {s : Set α}
+
+lemma measure_null_iff_eq_empty_of_measure_singleton_ne_zero (h : ∀ a, μ {a} ≠ 0) :
+    μ s = 0 ↔ s = ∅ := by
+  refine ⟨fun hs ↦ ?_, fun he ↦ by simp [he]⟩
+  apply Set.eq_empty_of_forall_notMem
+  exact fun a ha ↦ h a (measure_mono_null (Set.singleton_subset_iff.mpr ha) hs)
+
+end OuterMeasureClass
+
+end MeasureTheory

LeanMachineLearning/Probability/HasCondDistrib.lean

@@ -253,4 +253,21 @@ lemma HasCondDistrib.prod [IsFiniteMeasure μ] [IsFiniteKernel κ]
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
   rfl
 
+lemma HasCondDistrib.hasCondDistrib_sectR [IsFiniteMeasure μ] [StandardBorelSpace β] [Nonempty β]
+    {W : α → Ω'} {Z : α → γ} {f : Ω' → β} {g : Ω' → Ω} {η : Kernel (γ × β) Ω} (hf : Measurable f)
+    (hg : Measurable g) (hW : AEMeasurable W μ)
+    (hcd : HasCondDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) η μ) :
+    ∀ᵐ z ∂(μ.map Z), HasCondDistrib g f (η.sectR z) (condDistrib W Z μ z) := by
+  have h_eq : condDistrib (g ∘ W) (fun a ↦ (Z a, (f ∘ W) a)) μ
+      =ᵐ[μ.map Z ⊗ₘ (condDistrib W Z μ).map f] η := by
+    rw [← Measure.compProd_congr (condDistrib_comp Z hW hf),
+        compProd_map_condDistrib (hf.comp_aemeasurable hW)]
+    exact hcd.condDistrib_eq
+  filter_upwards [
+    condDistrib_condDistrib_ae_eq_sectR_condDistrib hf hg hW hcd.aemeasurable_snd.fst,
+    Measure.ae_ae_of_ae_compProd h_eq] with z hc ha
+  refine ⟨hg.aemeasurable, hf.aemeasurable, ?_⟩
+  rw [Kernel.map_apply _ hf] at ha
+  filter_upwards [hc, ha] with b hcb hab using hcb.trans hab
+
 end ProbabilityTheory

LeanMachineLearning/Probability/Independence/CondDistrib.lean

@@ -52,6 +52,24 @@ lemma condDistrib_prod_left [StandardBorelSpace β] [Nonempty β]
     AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
   rfl
 
+lemma condDistrib_condDistrib_ae_eq_sectR_condDistrib [StandardBorelSpace β] [Nonempty β]
+    {f : Ω' → β} {g : Ω' → Ω} (hf : Measurable f) (hg : Measurable g) (hZ : AEMeasurable Z μ)
+    (hT : AEMeasurable T μ) :
+    ∀ᵐ t ∂(μ.map T),
+      condDistrib g f (condDistrib Z T μ t) =ᵐ[(condDistrib Z T μ t).map f]
+        (condDistrib (g ∘ Z) (fun a ↦ (T a, (f ∘ Z) a)) μ).sectR t := by
+  filter_upwards [
+    condDistrib_prod_left (hf.comp_aemeasurable hZ) (hg.comp_aemeasurable hZ) hT,
+    condDistrib_comp T hZ (hf.prodMk hg), condDistrib_comp T hZ hf] with t h_prod h_pair h_fst
+  rw [condDistrib_ae_eq_iff_measure_eq_compProd f hg.aemeasurable]
+  calc (condDistrib Z T μ t).map (fun ω' ↦ (f ω', g ω'))
+  _ = condDistrib (fun a ↦ ((f ∘ Z) a, (g ∘ Z) a)) T μ t := by
+      rw [← Kernel.map_apply _ (hf.prodMk hg)]
+      exact h_pair.symm
+  _ = (condDistrib Z T μ t).map f
+        ⊗ₘ (condDistrib (g ∘ Z) (fun a ↦ (T a, (f ∘ Z) a)) μ).sectR t := by
+      rw [h_prod, Kernel.compProd_apply_eq_compProd_sectR, h_fst, Kernel.map_apply _ hf]
+
 lemma condDistrib_prod_self_left [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace γ]
     [Nonempty γ]
     (hX : AEMeasurable X μ) (hT : AEMeasurable T μ) :

LeanMachineLearning/SequentialLearning/AlgorithmDensity.lean

@@ -79,6 +79,8 @@ lemma measurable_density [MeasurableSpace.CountablyGenerated 𝓐] (alg alg₀ :
 
 end Algorithm
 
+open scoped Algorithm
+
 namespace IsAlgEnvSeq
 
 variable {Ω : Type*} [MeasurableSpace Ω]
@@ -92,8 +94,6 @@ variable {alg₀ : Algorithm 𝓐 𝓨}
 variable {A₀ : ℕ → Ω₀ → 𝓐} {Y₀ : ℕ → Ω₀ → 𝓨}
 variable {P₀ : Measure Ω₀} [IsProbabilityMeasure P₀]
 
-open scoped Algorithm
-
 lemma absolutelyContinuous_map_hist (h : IsAlgEnvSeq A Y alg env P)
     (h₀ : IsAlgEnvSeq A₀ Y₀ alg₀ env P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
     P.map (IsAlgEnvSeq.hist A Y n) ≪ P₀.map (IsAlgEnvSeq.hist A₀ Y₀ n) := by

LeanMachineLearning/SequentialLearning/Algorithms/Uniform.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Paulo Rauber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paulo Rauber, Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.MeasureTheory.Measure.AbsolutelyContinuous
+public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
+public import LeanMachineLearning.SequentialLearning.Algorithms.RandomSampling
+
+/-! # The Uniform algorithm
+
+An algorithm that chooses actions uniformly at random in every situation.
+
+## Main definitions
+
+* `uniformAlgorithm`: a uniform algorithm with actions in a finite non-empty type `𝓐`.
+
+## Main results
+
+* `absolutelyContinuous_uniformAlgorithm`: every algorithm with actions in `𝓐` is absolutely
+  continuous with respect to the uniform algorithm with the same type of feedback.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Learning
+
+open scoped Algorithm
+
+namespace Learning
+
+variable {𝓐 𝓨 : Type*} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
+
+/-- The Uniform algorithm: actions are chosen uniformly at random. -/
+noncomputable
+def uniformAlgorithm [Finite 𝓐] [Nonempty 𝓐] : Algorithm 𝓐 𝓨 := randomSampling (uniformOn Set.univ)
+
+lemma absolutelyContinuous_uniformAlgorithm [Finite 𝓐] [Nonempty 𝓐] {alg : Algorithm 𝓐 𝓨} :
+    alg ≪ₐ uniformAlgorithm where
+  p0 := Measure.absolutelyContinuous_of_measure_singleton_ne_zero
+    (by simp [uniformAlgorithm, uniformOn, ← pos_iff_ne_zero, cond_pos_of_inter_ne_zero])
+  policy n h := Measure.absolutelyContinuous_of_measure_singleton_ne_zero
+    (by simp [uniformAlgorithm, uniformOn, ← pos_iff_ne_zero, cond_pos_of_inter_ne_zero])
+
+end Learning