diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index 20bc433d..8c38ee74 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -49,7 +49,12 @@ jobs:
with:
build: true
lint: false
- mk_all-check: true
+ mk_all-check: false
+
+ - name: Build Verso Documentation
+ run: |
+ cd verso
+ ./build_manual.sh
- name: Compile blueprint and documentation
uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
diff --git a/.gitignore b/.gitignore
index 527ef1d1..2e362158 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,3 +37,7 @@ blueprint/src/web.pdf
*.synctex.gz
*.synctex.gz(busy)
*.pdfsync
+## Verso
+/verso/.lake/
+/verso/html/
+/home_page/verso
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 45745151..9ccd0410 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -1,7 +1,13 @@
-# Contributing to [Project]
+# Contributing to Lean Machine Learning
-Thank you for your interest in contributing to [Project]! We welcome contributions from the
-community and appreciate your efforts to improve the project. Please follow the guidelines below
-to ensure a smooth contribution process.
+Thank you for your interest in contributing to Lean Machine Learning! We welcome contributions from the community and appreciate your efforts to improve the project. Please follow the guidelines below to ensure a smooth contribution process.
-[ADD CONTENTS HERE]
+[In Construction]
+
+## Code quality and LLM policy
+
+The strength of the library lies in carefully designed and reviewed definitions.
+The standard is reusable code, not merely code that compiles.
+We want to build the basis on which others can base their research efforts.
+
+LLM use is not discouraged, but their output should be carefully reviewed for code quality before submitting pull requests.
diff --git a/LeanBandits.lean b/LeanBandits.lean
deleted file mode 100644
index 1bf5134c..00000000
--- a/LeanBandits.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import LeanBandits.Bandit.Bandit
-import LeanBandits.Bandit.Regret
-import LeanBandits.Bandit.RewardByCountMeasure
-import LeanBandits.Bandit.SumRewards
-import LeanBandits.BanditAlgorithms.AuxSums
-import LeanBandits.BanditAlgorithms.ETC
-import LeanBandits.BanditAlgorithms.RoundRobin
-import LeanBandits.BanditAlgorithms.UCB
-import LeanBandits.ForMathlib.CondDistrib
-import LeanBandits.ForMathlib.CondIndepFun
-import LeanBandits.ForMathlib.HasCondDistrib
-import LeanBandits.ForMathlib.IndepFun
-import LeanBandits.ForMathlib.IndepInfinitePi
-import LeanBandits.ForMathlib.Integrable
-import LeanBandits.ForMathlib.KernelRepresentation
-import LeanBandits.ForMathlib.KernelSub
-import LeanBandits.ForMathlib.Measurable
-import LeanBandits.ForMathlib.MeasurableArgMax
-import LeanBandits.ForMathlib.StandardBorel
-import LeanBandits.ForMathlib.SubGaussian
-import LeanBandits.ForMathlib.Traj
-import LeanBandits.SequentialLearning.Algorithm
-import LeanBandits.SequentialLearning.Deterministic
-import LeanBandits.SequentialLearning.FiniteActions
-import LeanBandits.SequentialLearning.IonescuTulceaSpace
-import LeanBandits.SequentialLearning.StationaryEnv
diff --git a/LeanBandits/ForMathlib/KernelRepresentation.lean b/LeanBandits/ForMathlib/KernelRepresentation.lean
deleted file mode 100644
index aebf144b..00000000
--- a/LeanBandits/ForMathlib/KernelRepresentation.lean
+++ /dev/null
@@ -1,154 +0,0 @@
-/-
-Copyright (c) 2025 Gaëtan Serré. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gaëtan Serré, Rémy Degenne
--/
-
-import Mathlib.Analysis.SpecialFunctions.Sigmoid
-import Mathlib.MeasureTheory.Constructions.UnitInterval
-import Mathlib.Order.CompletePartialOrder
-import Mathlib.Probability.CDF
-
--- copied from PR #30112
-
-/-!
-# Representation of kernels
-
-This file contains results about isolation of kernels randomness. In particular, it shows that,
-when the target space is a standard Borel space, any Markov kernel can be represented as the image
-of the uniform measure on `[0,1]` by a deterministic map. It corresponds to Lemma 4.22 in
-"Foundations of Modern Probability" by Olav Kallenberg, 2021.
-
-## Statements
-
-* `ProbabilityTheory.Kernel.unitInterval_representation`:
- for a Markov kernel `κ : Kernel α I`, there exists a jointly measurable function
- `f : α → I → I` such that for all `a : α`, `volume.map (f a) = κ a`.
-
-* `ProbabilityTheory.Kernel.embedding_representation`:
- for a measurable embedding `g : β → I` and a Markov kernel `κ : Kernel α β`,
- there exists a jointly measurable function `f : α → I → β` such that for all `a : α`,
- `volume.map (f a) = κ a`.
-
-* `ProbabilityTheory.Kernel.representation`:
- for a Markov kernel `κ : Kernel α β` with `β` a standard Borel space,
- there exists a jointly measurable function `f : α → I → β` such that for all `a : α`,
- `volume.map (f a) = κ a`.
- This is a consequence of `ProbabilityTheory.Kernel.embedding_representation` and the fact that
- any standard Borel space can be embedded in `ℝ`, and then composed with `unitInterval.sigmoid`.
--/
-
-open MeasureTheory ProbabilityTheory Set ENNReal unitInterval Filter Topology Function
-
-namespace ProbabilityTheory.Kernel
-
-variable {α : Type*} [MeasurableSpace α]
-
-lemma unitInterval_representation (κ : Kernel α I) [IsMarkovKernel κ] :
- ∃ (f : α → I → I), Measurable (uncurry f) ∧ ∀ a, volume.map (f a) = κ a := by
- let f := fun s (t : I) ↦ sSup {x | (κ s).real (Icc 0 x) < t}
- have measurable_f : Measurable (uncurry f) := by
- refine measurable_of_Ioi fun a ↦ ?_
- simp only [preimage, uncurry, mem_Ioi]
- have h_monotone s : Monotone (fun x ↦ (κ s).real (Icc 0 x)) := by
- intro x y hxy
- suffices h : Icc 0 x ⊆ Icc 0 y from measureReal_mono h
- exact Icc_subset_Icc_right hxy
- have sSup_eq_iUnion_rat : {x : α × I | a < f x.1 x.2} = ⋃ (q : ℚ), ⋃ (hqI : ↑q ∈ I),
- ⋃ (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc 0 ⟨q, hqI⟩) < e.2} := by
- ext e
- simp only [f]
- constructor
- · intro (he : a < sSup {x | (κ e.1).real (Icc 0 x) < e.2})
- simp_rw [Set.mem_iUnion]
- rw [lt_sSup_iff] at he
- obtain ⟨y, y_mem, (hy : a.1 < y.1)⟩ := he
- obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy
- have q_in_I : (q : ℝ) ∈ I := ⟨a.2.1.trans hqa.le, hqy.le.trans y.2.2⟩
- refine ⟨q, q_in_I, hqa, ?_⟩
- exact lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)
- · intro he
- simp_all only [lt_sSup_iff, Set.mem_iUnion]
- obtain ⟨q, q_in_I, hqa, h⟩ := he
- exact ⟨⟨q, q_in_I⟩, h, hqa⟩
- rw [sSup_eq_iUnion_rat]
- refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
- (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))
- refine measurableSet_lt ?_ measurable_snd.subtype_val
- simp_rw [measureReal_def]
- have hκ := κ.measurable_coe (s := Icc 0 ⟨b, bI⟩) measurableSet_Icc
- fun_prop
- refine ⟨f, measurable_f, fun a ↦ (volume.map (f a)).ext_of_Iic (κ a) fun x ↦ ?_⟩
- rw [volume.map_apply measurable_f.of_uncurry_left measurableSet_Iic, preimage]
- simp only [mem_Iic]
- have Iic_to_Icc : Iic x = Icc 0 x := by ext; simp
- rw [Iic_to_Icc]
- clear Iic_to_Icc
- rw [← ofReal_measureReal (measure_ne_top (κ a) _)]
- have κ_in_I : ((κ a).real (Icc 0 x)) ∈ I := ⟨measureReal_nonneg, measureReal_le_one⟩
- rw [← volume_Iic ⟨_, κ_in_I⟩]
- congr with ξ
- constructor
- swap
- · intro (hξ : ξ ≤ (κ a).real (Icc 0 x))
- simp only [sSup_le_iff, f]
- intro c hc
- have le1 := lt_of_le_of_lt' hξ hc
- by_contra h
- push_neg at h
- have le2 : (κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c) := by
- suffices h : Icc 0 x ⊆ Icc 0 c from measureReal_mono h
- refine (Icc_subset_Icc_iff unitInterval.nonneg').mpr ?_
- exact ⟨nonneg', h.le⟩
- linarith
- · intro (hξ : f a ξ ≤ x)
- change ξ ≤ (κ a).real (Icc 0 x)
- by_cases hx : x = 1
- · simp [hx, ← univ_eq_Icc, ξ.2.2]
- let g := fun y ↦ (κ a).real (Icc 0 y)
- letI nebot : NeBot (𝓝[>] x) := by
- refine nhdsGT_neBot_of_exists_gt ?_
- use 1
- exact lt_of_le_of_ne x.2.2 hx
- refine le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_
- · let h := cdf ((κ a).map Subtype.val)
- have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous x)
- simp_rw [g, ← unitInterval.cdf_eq_real (κ a)]
- exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy)
- · apply eventually_nhdsWithin_of_forall
- intro y hy
- by_contra h
- push_neg at h
- simp only [sSup_le_iff, f] at hξ
- specialize hξ y h
- replace hξ : y.1 ≤ x.1 := hξ
- have : y.1 > x.1 := hy
- linarith
-
-lemma embedding_representation {β : Type*} [Nonempty β] [MeasurableSpace β] {g : β → I}
- (hg : MeasurableEmbedding g) (κ : Kernel α β) [IsMarkovKernel κ] :
- ∃ (f : α → I → β), Measurable (uncurry f) ∧ ∀ a, volume.map (f a) = κ a := by
- have hκg : IsMarkovKernel (κ.map g) := Kernel.IsMarkovKernel.map κ hg.measurable
- classical
- have hg'κ : κ = (κ.map g).map hg.invFun := by
- rw [← Kernel.map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
- Kernel.map_id]
- obtain ⟨f', hf', hf'κ⟩ := (κ.map g).unitInterval_representation
- refine ⟨fun a u ↦ hg.invFun (f' a u), by fun_prop, fun a ↦ ?_⟩
- rw [hg'κ, Kernel.map_apply _ (by fun_prop), ← hf'κ, Measure.map_map (by fun_prop) (by fun_prop)]
- rfl
-
-theorem representation {β : Type*} [Nonempty β] [MeasurableSpace β] [StandardBorelSpace β]
- (κ : Kernel α β) [IsMarkovKernel κ] :
- ∃ (f : α → I → β), Measurable (uncurry f) ∧ ∀ a, volume.map (f a) = κ a :=
- κ.embedding_representation (measurableEmbedding_sigmoid_comp_embeddingReal β)
-
-end ProbabilityTheory.Kernel
-
-theorem ProbabilityTheory.representation_measure {β : Type*} {mβ : MeasurableSpace β}
- [Nonempty β] [StandardBorelSpace β]
- (μ : Measure β) [IsProbabilityMeasure μ] :
- ∃ (f : I → β), Measurable f ∧ volume.map f = μ := by
- obtain ⟨f, hf_meas, hf_map⟩ := Kernel.representation (Kernel.const Unit μ)
- specialize hf_map ⟨⟩
- exact ⟨f ⟨⟩, by fun_prop, by simpa⟩
diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
new file mode 100644
index 00000000..d4aa0eca
--- /dev/null
+++ b/LeanMachineLearning.lean
@@ -0,0 +1,27 @@
+module
+
+public import LeanMachineLearning.Bandit.Bandit
+public import LeanMachineLearning.Bandit.Regret
+public import LeanMachineLearning.Bandit.RewardByCountMeasure
+public import LeanMachineLearning.Bandit.SumRewards
+public import LeanMachineLearning.BanditAlgorithms.AuxSums
+public import LeanMachineLearning.BanditAlgorithms.ETC
+public import LeanMachineLearning.BanditAlgorithms.RoundRobin
+public import LeanMachineLearning.BanditAlgorithms.UCB
+public import LeanMachineLearning.ForMathlib.CondDistrib
+public import LeanMachineLearning.ForMathlib.CondIndepFun
+public import LeanMachineLearning.ForMathlib.HasCondDistrib
+public import LeanMachineLearning.ForMathlib.IndepFun
+public import LeanMachineLearning.ForMathlib.IndepInfinitePi
+public import LeanMachineLearning.ForMathlib.Integrable
+public import LeanMachineLearning.ForMathlib.KernelSub
+public import LeanMachineLearning.ForMathlib.Measurable
+public import LeanMachineLearning.ForMathlib.MeasurableArgMax
+public import LeanMachineLearning.ForMathlib.StandardBorel
+public import LeanMachineLearning.ForMathlib.SubGaussian
+public import LeanMachineLearning.ForMathlib.Traj
+public import LeanMachineLearning.SequentialLearning.Algorithm
+public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.FiniteActions
+public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+public import LeanMachineLearning.SequentialLearning.StationaryEnv
diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanMachineLearning/Bandit/Bandit.lean
similarity index 98%
rename from LeanBandits/Bandit/Bandit.lean
rename to LeanMachineLearning/Bandit/Bandit.lean
index 67b8f986..e195a42a 100644
--- a/LeanBandits/Bandit/Bandit.lean
+++ b/LeanMachineLearning/Bandit/Bandit.lean
@@ -3,19 +3,24 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.ForMathlib.CondIndepFun
-import LeanBandits.ForMathlib.IndepFun
-import LeanBandits.ForMathlib.IndepInfinitePi
-import LeanBandits.ForMathlib.Integrable
-import LeanBandits.ForMathlib.KernelRepresentation
-import LeanBandits.ForMathlib.StandardBorel
-import LeanBandits.SequentialLearning.FiniteActions
-import LeanBandits.SequentialLearning.StationaryEnv
+module
+
+public import LeanMachineLearning.ForMathlib.CondIndepFun
+public import LeanMachineLearning.ForMathlib.IndepFun
+public import LeanMachineLearning.ForMathlib.IndepInfinitePi
+public import LeanMachineLearning.ForMathlib.Integrable
+public import LeanMachineLearning.ForMathlib.StandardBorel
+public import LeanMachineLearning.SequentialLearning.FiniteActions
+public import LeanMachineLearning.SequentialLearning.StationaryEnv
+public import Mathlib.Probability.Independence.Integration
+public import Mathlib.Probability.Kernel.Representation
/-!
# Bandit
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset Learning
open scoped ENNReal NNReal
@@ -128,29 +133,28 @@ variable [Nonempty α] [StandardBorelSpace α]
/-- The initial action is the image of a uniform random variable by this function. -/
noncomputable
def initAlgFunction (alg : Algorithm α R) : I → α :=
- (representation_measure alg.p0).choose
+ (Measure.exists_measurable_map_eq alg.p0).choose
lemma initAlgFunction_map (alg : Algorithm α R) : volume.map (initAlgFunction alg) = alg.p0 :=
- (representation_measure alg.p0).choose_spec.2
+ (Measure.exists_measurable_map_eq alg.p0).choose_spec.2
@[fun_prop]
lemma measurable_initAlgFunction (alg : Algorithm α R) :
- Measurable (initAlgFunction alg) := (representation_measure alg.p0).choose_spec.1
-
+ Measurable (initAlgFunction alg) := (Measure.exists_measurable_map_eq alg.p0).choose_spec.1
/-- The next action is the image of the history and a uniform random variable by this function. -/
noncomputable
def algFunction (alg : Algorithm α R) (n : ℕ) :
(Iic n → α × R) → I → α :=
- (Kernel.representation (alg.policy n)).choose
+ (Kernel.exists_measurable_map_eq_unitInterval (alg.policy n)).choose
lemma algFunction_map (alg : Algorithm α R) (n : ℕ) (h : Iic n → α × R) :
volume.map (algFunction alg n h) = alg.policy n h :=
- (Kernel.representation (alg.policy n)).choose_spec.2 h
+ (Kernel.exists_measurable_map_eq_unitInterval (alg.policy n)).choose_spec.2 h
@[fun_prop]
lemma measurable_algFunction (alg : Algorithm α R) (n : ℕ) :
Measurable (Function.uncurry (algFunction alg n)) :=
- (Kernel.representation (alg.policy n)).choose_spec.1
+ (Kernel.exists_measurable_map_eq_unitInterval (alg.policy n)).choose_spec.1
end ProbabilitySpace
@@ -524,7 +528,9 @@ lemma measurable_pullCount_action_add_one_hist (alg : Algorithm α R) (n : ℕ)
simp_rw [pullCount_eq_sum]
refine measurable_sum _ fun i hi ↦ Measurable.ite ?_ (by fun_prop) (by fun_prop)
refine measurableSet_eq_fun ?_ (measurable_comp_comap _ measurable_fst)
+ rw [measurable_iff_comap_le]
simp_rw [hist_eq _ _ n]
+ rw [← measurable_iff_comap_le]
unfold action
refine Measurable.fst (mγ := inferInstance) ?_
have : (hist alg · i ⟨i, by grind⟩) =
@@ -875,8 +881,8 @@ lemma indepFun_snd_hist_cond [Countable α] (alg : Algorithm α R)
pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1)) ⁻¹' {1}]]
fun ω ↦ (ω.1, fun k b ↦ if b = a then if m ≠ 0 then ω.2 (min k (m - 1)) b
else Nonempty.some inferInstance else ω.2 k b) by
- convert this
- ext ω
+ convert this using 1
+ congr with ω
simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply,
Set.mem_setOf_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
Classical.not_imp, Decidable.not_not, and_congr_right_iff]
diff --git a/LeanBandits/Bandit/Regret.lean b/LeanMachineLearning/Bandit/Regret.lean
similarity index 97%
rename from LeanBandits/Bandit/Regret.lean
rename to LeanMachineLearning/Bandit/Regret.lean
index 932d3cfb..0d4a6c29 100644
--- a/LeanBandits/Bandit/Regret.lean
+++ b/LeanMachineLearning/Bandit/Regret.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.SequentialLearning.FiniteActions
+module
+
+public import LeanMachineLearning.SequentialLearning.FiniteActions
/-!
# Regret, gap, best arm
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset Learning
open scoped ENNReal NNReal
@@ -23,7 +27,9 @@ variable {α Ω : Type*} [DecidableEq α] {mα : MeasurableSpace α} {mΩ : Meas
/-- Gap of an action `a`: difference between the highest mean of the actions and the mean of `a`. -/
noncomputable
+-- ANCHOR: gap
def gap (ν : Kernel α ℝ) (a : α) : ℝ := (⨆ i, (ν i)[id]) - (ν a)[id]
+-- ANCHOR_END: gap
omit [DecidableEq α] in
lemma gap_nonneg [Finite α] : 0 ≤ gap ν a := by
@@ -32,8 +38,10 @@ lemma gap_nonneg [Finite α] : 0 ≤ gap ν a := by
/-- Regret of a sequence of pulls `k : ℕ → α` at time `t` for the reward kernel `ν ; Kernel α ℝ`. -/
noncomputable
+-- ANCHOR: regret
def regret (ν : Kernel α ℝ) (A : ℕ → Ω → α) (t : ℕ) (ω : Ω) : ℝ :=
t * (⨆ a, (ν a)[id]) - ∑ s ∈ range t, (ν (A s ω))[id]
+-- ANCHOR_END: regret
omit [DecidableEq α] in
lemma regret_eq_sum_gap : regret ν A t ω = ∑ s ∈ range t, gap ν (A s ω) := by
diff --git a/LeanBandits/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Bandit/RewardByCountMeasure.lean
similarity index 99%
rename from LeanBandits/Bandit/RewardByCountMeasure.lean
rename to LeanMachineLearning/Bandit/RewardByCountMeasure.lean
index b8dae4dd..ed0d182d 100644
--- a/LeanBandits/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Bandit/RewardByCountMeasure.lean
@@ -3,12 +3,15 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.Bandit.Bandit
-import Mathlib.Probability.IdentDistribIndep
+module
+
+public import LeanMachineLearning.Bandit.Bandit
/-! # Laws of `stepsUntil` and `rewardByCount`
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Finset Learning
open scoped ENNReal NNReal
@@ -89,7 +92,7 @@ lemma condIndepFun_reward_stepsUntil_action' [StandardBorelSpace Ω]
by_cases hn : n = 0
· have h_indep : R 0 ⟂ᵢ[A 0, hA 0; P] A 0 :=
condIndepFun_self_right (by fun_prop) (by fun_prop)
- simp only [hn, CharP.cast_eq_zero]
+ simp only [hn]
refine h_indep.of_measurable_right (hX := hA 0) ?_
exact measurable_comap_indicator_stepsUntil_eq_zero a m
· have h_indep : R n ⟂ᵢ[A n, hA n; P] fun ω ↦ (IsAlgEnvSeq.hist A R (n - 1) ω, A n ω) :=
diff --git a/LeanBandits/Bandit/SumRewards.lean b/LeanMachineLearning/Bandit/SumRewards.lean
similarity index 99%
rename from LeanBandits/Bandit/SumRewards.lean
rename to LeanMachineLearning/Bandit/SumRewards.lean
index 64d071f9..8026bdab 100644
--- a/LeanBandits/Bandit/SumRewards.lean
+++ b/LeanMachineLearning/Bandit/SumRewards.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.Bandit.Bandit
-import LeanBandits.Bandit.Regret
-import LeanBandits.ForMathlib.SubGaussian
+module
+
+public import LeanMachineLearning.Bandit.Bandit
+public import LeanMachineLearning.Bandit.Regret
+public import LeanMachineLearning.ForMathlib.SubGaussian
/-! # Law of the sum of rewards
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Finset Learning
open scoped ENNReal NNReal
diff --git a/LeanBandits/BanditAlgorithms/AuxSums.lean b/LeanMachineLearning/BanditAlgorithms/AuxSums.lean
similarity index 91%
rename from LeanBandits/BanditAlgorithms/AuxSums.lean
rename to LeanMachineLearning/BanditAlgorithms/AuxSums.lean
index 3ba38d6c..69b104a0 100644
--- a/LeanBandits/BanditAlgorithms/AuxSums.lean
+++ b/LeanMachineLearning/BanditAlgorithms/AuxSums.lean
@@ -3,15 +3,19 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.Algebra.BigOperators.Intervals
-import Mathlib.Algebra.BigOperators.Ring.Finset
-import Mathlib.Tactic.Ring.RingNF
+module
+
+public import Mathlib.Algebra.BigOperators.Intervals
+public import Mathlib.Algebra.BigOperators.Ring.Finset
+public import Mathlib.Tactic.Ring.RingNF
/-!
# Lemmas about sums of indicators
-/
+@[expose] public section
+
open Finset
lemma sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
diff --git a/LeanBandits/BanditAlgorithms/ETC.lean b/LeanMachineLearning/BanditAlgorithms/ETC.lean
similarity index 98%
rename from LeanBandits/BanditAlgorithms/ETC.lean
rename to LeanMachineLearning/BanditAlgorithms/ETC.lean
index 12b4693b..03b9f9e6 100644
--- a/LeanBandits/BanditAlgorithms/ETC.lean
+++ b/LeanMachineLearning/BanditAlgorithms/ETC.lean
@@ -3,14 +3,18 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.Bandit.SumRewards
-import LeanBandits.BanditAlgorithms.RoundRobin
-import LeanBandits.ForMathlib.MeasurableArgMax
+module
+
+public import LeanMachineLearning.Bandit.SumRewards
+public import LeanMachineLearning.BanditAlgorithms.RoundRobin
+public import LeanMachineLearning.ForMathlib.MeasurableArgMax
/-! # The Explore-Then-Commit Algorithm
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Finset Learning
open scoped ENNReal NNReal
diff --git a/LeanBandits/BanditAlgorithms/RoundRobin.lean b/LeanMachineLearning/BanditAlgorithms/RoundRobin.lean
similarity index 93%
rename from LeanBandits/BanditAlgorithms/RoundRobin.lean
rename to LeanMachineLearning/BanditAlgorithms/RoundRobin.lean
index 07d5961c..0be8be67 100644
--- a/LeanBandits/BanditAlgorithms/RoundRobin.lean
+++ b/LeanMachineLearning/BanditAlgorithms/RoundRobin.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.BanditAlgorithms.AuxSums
-import LeanBandits.SequentialLearning.Deterministic
-import LeanBandits.SequentialLearning.FiniteActions
-import LeanBandits.SequentialLearning.StationaryEnv
+module
+
+public import LeanMachineLearning.BanditAlgorithms.AuxSums
+public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.FiniteActions
+public import LeanMachineLearning.SequentialLearning.StationaryEnv
/-! # Round-Robin algorithm
@@ -14,6 +16,8 @@ That algorithm pulls each arm in a round-robin fashion.
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Finset Learning
open scoped ENNReal NNReal
diff --git a/LeanBandits/BanditAlgorithms/UCB.lean b/LeanMachineLearning/BanditAlgorithms/UCB.lean
similarity index 98%
rename from LeanBandits/BanditAlgorithms/UCB.lean
rename to LeanMachineLearning/BanditAlgorithms/UCB.lean
index 806a2a12..3eaf2812 100644
--- a/LeanBandits/BanditAlgorithms/UCB.lean
+++ b/LeanMachineLearning/BanditAlgorithms/UCB.lean
@@ -3,15 +3,19 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.Bandit.SumRewards
-import LeanBandits.BanditAlgorithms.RoundRobin
-import LeanBandits.ForMathlib.MeasurableArgMax
+module
+
+public import LeanMachineLearning.Bandit.SumRewards
+public import LeanMachineLearning.BanditAlgorithms.RoundRobin
+public import LeanMachineLearning.ForMathlib.MeasurableArgMax
/-!
# UCB algorithm
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset Learning
open scoped ENNReal NNReal
@@ -22,6 +26,7 @@ variable {K : ℕ}
section Algorithm
+-- ANCHOR: UCB_def
/-- The exploration bonus of the UCB algorithm, which corresponds to the width of
a confidence interval. -/
noncomputable def ucbWidth' (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) (a : Fin K) : ℝ :=
@@ -47,7 +52,7 @@ lemma UCB.measurable_nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) : Measurable (next
noncomputable
def ucbAlgorithm (hK : 0 < K) (c : ℝ) : Algorithm (Fin K) ℝ :=
detAlgorithm (UCB.nextArm hK c) (by fun_prop) ⟨0, hK⟩
-
+-- ANCHOR_END: UCB_def
end Algorithm
namespace UCB
@@ -447,6 +452,7 @@ lemma constSum_lt_top (c : ℝ) (n : ℕ) : constSum c n < ∞ := by
simp only [one_div, ENNReal.inv_lt_top]
positivity
+set_option backward.isDefEq.respectTransparency false in
/-- Bound on the expectation of the number of pulls of each arm by the UCB algorithm. -/
lemma expectation_pullCount_le' [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
@@ -568,12 +574,14 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
ring
/-- Regret bound for the UCB algorithm. -/
+-- ANCHOR: UCB.regret_le
lemma regret_le [Nonempty (Fin K)]
(h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
(hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
(hσ2 : σ2 ≠ 0) (hc : 0 < c) (n : ℕ) :
P[regret ν A n] ≤
∑ a, (8 * c * σ2 * log (n + 1) / gap ν a + gap ν a * (2 + 2 * (constSum c n).toReal)) := by
+-- ANCHOR_END: UCB.regret_le
refine (integral_regret_le_of_forall_integral_pullCount_le h
(fun a h_gap ↦ expectation_pullCount_le h hν hσ2 hc a
(lt_of_le_of_ne' gap_nonneg h_gap) n)).trans_eq ?_
diff --git a/LeanBandits/ForMathlib/CondDistrib.lean b/LeanMachineLearning/ForMathlib/CondDistrib.lean
similarity index 98%
rename from LeanBandits/ForMathlib/CondDistrib.lean
rename to LeanMachineLearning/ForMathlib/CondDistrib.lean
index 9d57f6de..2f35a721 100644
--- a/LeanBandits/ForMathlib/CondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/CondDistrib.lean
@@ -3,10 +3,14 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.ForMathlib.KernelSub
-import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
-import Mathlib.Probability.Independence.Basic
-import Mathlib.Probability.Independence.Conditional
+module
+
+public import LeanMachineLearning.ForMathlib.KernelSub
+public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+public import Mathlib.Probability.Independence.Basic
+public import Mathlib.Probability.Independence.Conditional
+
+@[expose] public section
open MeasureTheory ProbabilityTheory Finset
open scoped ENNReal NNReal
@@ -210,7 +214,7 @@ instance : CanonicallyOrderedAdd (FiniteMeasure α) where
instance : OrderedSub (FiniteMeasure α) where
tsub_le_iff_right μ ν ξ := by
simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_sub, FiniteMeasure.toMeasure_add]
- exact Measure.sub_le_iff_add
+ exact Measure.sub_le_iff_le_add
lemma Kernel.prodMkLeft_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated α β]
{κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η]
@@ -411,7 +415,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
(hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
(κ : Kernel (β × Ω') Ω) [IsFiniteKernel κ]
(h_cond : ∀ b, μ (Z ⁻¹' {b}) ≠ 0 → condDistrib Y X μ[|Z ⁻¹' {b}] =ᵐ[μ[|Z ⁻¹' {b}].map X]
- (κ.comap (fun ω ↦ (ω, b)) (by fun_prop))) :
+ (κ.comap (fun ω ↦ (ω, b)) (by fun_prop) : Kernel β Ω)) :
condDistrib Y (fun ω ↦ (X ω, Z ω)) μ =ᵐ[μ.map (fun ω ↦ (X ω, Z ω))] κ := by
refine condDistrib_ae_eq_of_measure_eq_compProd _ (by fun_prop) ?_
ext s hs
diff --git a/LeanBandits/ForMathlib/CondIndepFun.lean b/LeanMachineLearning/ForMathlib/CondIndepFun.lean
similarity index 95%
rename from LeanBandits/ForMathlib/CondIndepFun.lean
rename to LeanMachineLearning/ForMathlib/CondIndepFun.lean
index ee7efa2b..fd6941de 100644
--- a/LeanBandits/ForMathlib/CondIndepFun.lean
+++ b/LeanMachineLearning/ForMathlib/CondIndepFun.lean
@@ -3,9 +3,13 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.MeasureTheory.Function.FactorsThrough
-import Mathlib.Probability.Independence.Basic
-import Mathlib.Probability.Independence.Conditional
+module
+
+public import Mathlib.MeasureTheory.Function.FactorsThrough
+public import Mathlib.Probability.Independence.Basic
+public import Mathlib.Probability.Independence.Conditional
+
+@[expose] public section
/-! # Laws of `stepsUntil` and `rewardByCount`
-/
diff --git a/LeanBandits/ForMathlib/HasCondDistrib.lean b/LeanMachineLearning/ForMathlib/HasCondDistrib.lean
similarity index 97%
rename from LeanBandits/ForMathlib/HasCondDistrib.lean
rename to LeanMachineLearning/ForMathlib/HasCondDistrib.lean
index a151124e..2d12fefe 100644
--- a/LeanBandits/ForMathlib/HasCondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/HasCondDistrib.lean
@@ -3,13 +3,17 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.ForMathlib.CondDistrib
-import Mathlib.Probability.HasLaw
+module
+
+public import LeanMachineLearning.ForMathlib.CondDistrib
+public import Mathlib.Probability.HasLaw
/-!
# A predicate for having a specified conditional distribution
-/
+@[expose] public section
+
open MeasureTheory
namespace ProbabilityTheory
@@ -73,7 +77,7 @@ lemma HasCondDistrib.snd {Y : α → Ω × Ω'} {κ : Kernel β (Ω × Ω')} [Is
lemma HasCondDistrib.comp_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : HasCondDistrib Y X κ μ)
(f : β ≃ᵐ γ) :
- HasCondDistrib Y (f ∘ X) (κ.comap f.symm (by fun_prop)) μ := by
+ HasCondDistrib Y (f ∘ X) (κ.comap f.symm (by fun_prop) : Kernel γ Ω) μ := by
have hY := h.aemeasurable_fst
have hX := h.aemeasurable_snd
refine ⟨h.aemeasurable_fst, by fun_prop, ?_⟩
@@ -141,7 +145,7 @@ lemma HasCondDistrib.prod_right [IsFiniteMeasure μ] [IsFiniteKernel κ] (h : Ha
change Measure.map (Prod.map (fun x ↦ (x, f x)) id) ((Measure.dirac b).prod (κ b)) =
(Measure.dirac (b, f b)).prod (κ b)
rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
- Measure.map_dirac (by fun_prop)]
+ Measure.map_dirac' (by fun_prop)]
_ = μ.map (fun a ↦ (X a, f (X a))) ⊗ₘ κ.prodMkRight γ := by
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
congr
@@ -180,7 +184,7 @@ lemma hasCondDistrib_prod_right_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] (X
Kernel.id_apply]
change Measure.map (Prod.map (fun x ↦ x.1) id) ((Measure.dirac (b, f b)).prod (κ b)) = _
rw [← Measure.map_prod_map _ _ (by fun_prop) (by fun_prop), Measure.map_id,
- Measure.map_dirac (by fun_prop)]
+ Measure.map_dirac' (by fun_prop)]
lemma HasLaw.prod_of_hasCondDistrib {P : Measure β} [IsFiniteMeasure μ] [IsSFiniteKernel κ]
(h1 : HasLaw X P μ) (h2 : HasCondDistrib Y X κ μ) :
diff --git a/LeanBandits/ForMathlib/IndepFun.lean b/LeanMachineLearning/ForMathlib/IndepFun.lean
similarity index 96%
rename from LeanBandits/ForMathlib/IndepFun.lean
rename to LeanMachineLearning/ForMathlib/IndepFun.lean
index d0834089..e2413171 100644
--- a/LeanBandits/ForMathlib/IndepFun.lean
+++ b/LeanMachineLearning/ForMathlib/IndepFun.lean
@@ -1,5 +1,9 @@
-import Mathlib.Probability.IdentDistrib
-import Mathlib.Probability.Independence.InfinitePi
+module
+
+public import Mathlib.Probability.IdentDistrib
+public import Mathlib.Probability.Independence.InfinitePi
+
+@[expose] public section
open MeasureTheory Finset
@@ -23,7 +27,7 @@ lemma indepFun_cond_of_indepFun {α β γ : Type*} {mα : MeasurableSpace α} {m
by_cases h_zero : μ[|Y ⁻¹' s] = 0
· simp [h_zero]
rw [cond_eq_zero] at h_zero
- push_neg at h_zero -- `h_zero : μ (Y ⁻¹' s) ≠ ⊤ ∧ μ (Y ⁻¹' s) ≠ 0`
+ push Not at h_zero -- `h_zero : μ (Y ⁻¹' s) ≠ ⊤ ∧ μ (Y ⁻¹' s) ≠ 0`
rw [indepFun_iff_measure_inter_preimage_eq_mul] at hXY ⊢
intro u t hu ht
rw [cond_apply (hs.preimage hY), cond_apply (hs.preimage hY), cond_apply (hs.preimage hY)]
diff --git a/LeanBandits/ForMathlib/IndepInfinitePi.lean b/LeanMachineLearning/ForMathlib/IndepInfinitePi.lean
similarity index 93%
rename from LeanBandits/ForMathlib/IndepInfinitePi.lean
rename to LeanMachineLearning/ForMathlib/IndepInfinitePi.lean
index b18bd4ba..d55780c7 100644
--- a/LeanBandits/ForMathlib/IndepInfinitePi.lean
+++ b/LeanMachineLearning/ForMathlib/IndepInfinitePi.lean
@@ -1,4 +1,8 @@
-import Mathlib.Probability.Independence.InfinitePi
+module
+
+public import Mathlib.Probability.Independence.InfinitePi
+
+@[expose] public section
open MeasureTheory Measure ProbabilityTheory Set Function
diff --git a/LeanBandits/ForMathlib/Integrable.lean b/LeanMachineLearning/ForMathlib/Integrable.lean
similarity index 89%
rename from LeanBandits/ForMathlib/Integrable.lean
rename to LeanMachineLearning/ForMathlib/Integrable.lean
index 5a366cf3..1e77f126 100644
--- a/LeanBandits/ForMathlib/Integrable.lean
+++ b/LeanMachineLearning/ForMathlib/Integrable.lean
@@ -3,7 +3,11 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.Probability.IdentDistrib
+module
+
+public import Mathlib.Probability.IdentDistrib
+
+@[expose] public section
open ProbabilityTheory
diff --git a/LeanBandits/ForMathlib/KernelSub.lean b/LeanMachineLearning/ForMathlib/KernelSub.lean
similarity index 53%
rename from LeanBandits/ForMathlib/KernelSub.lean
rename to LeanMachineLearning/ForMathlib/KernelSub.lean
index cb0c3461..244af920 100644
--- a/LeanBandits/ForMathlib/KernelSub.lean
+++ b/LeanMachineLearning/ForMathlib/KernelSub.lean
@@ -3,13 +3,18 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.Probability.Kernel.RadonNikodym
+module
+
+public import Mathlib.MeasureTheory.Measure.SubFinite
+public import Mathlib.Probability.Kernel.RadonNikodym
/-!
# Kernels substraction
-/
+@[expose] public section
+
open MeasureTheory MeasurableSpace
open scoped ENNReal
@@ -17,117 +22,6 @@ namespace MeasureTheory.Measure
variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν ξ : Measure α}
-lemma sub_le_iff_add_of_le [IsFiniteMeasure ν] (h_le : ν ≤ μ) : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
- refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
- rw [Measure.le_iff] at h ⊢
- intro s hs
- specialize h s hs
- simp only [Measure.coe_add, Pi.add_apply]
- rwa [Measure.sub_apply hs h_le, tsub_le_iff_right] at h
-
-lemma sub_le_iff_add [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ - ν ≤ ξ ↔ μ ≤ ξ + ν := by
- refine ⟨fun h ↦ ?_, Measure.sub_le_of_le_add⟩
- obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
- suffices μ.restrict s ≤ ξ.restrict s + ν.restrict s
- ∧ μ.restrict sᶜ ≤ ξ.restrict sᶜ + ν.restrict sᶜ by
- have h_eq_restrict (μ : Measure α) : μ = μ.restrict s + μ.restrict sᶜ := by
- rw [Measure.restrict_add_restrict_compl hs.measurableSet]
- rw [h_eq_restrict μ, h_eq_restrict ξ, h_eq_restrict ν]
- suffices μ.restrict s + μ.restrict sᶜ
- ≤ ξ.restrict s + ν.restrict s + (ξ.restrict sᶜ + ν.restrict sᶜ) by
- refine this.trans_eq ?_
- abel
- gcongr
- · exact this.1
- · exact this.2
- constructor
- · have h_le := hs.le_on
- refine h_le.trans ?_
- exact Measure.le_add_left le_rfl
- · have h_le := hs.ge_on_compl
- have h' : μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ := by
- rw [← Measure.restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]
- exact Measure.restrict_mono subset_rfl h
- exact (Measure.sub_le_iff_add_of_le h_le).mp h'
-
-lemma add_sub_of_mutuallySingular (h : μ ⟂ₘ ξ) : μ + (ν - ξ) = μ + ν - ξ := by
- let s := h.nullSet
- have hs : MeasurableSet s := h.measurableSet_nullSet
- suffices μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
- ∧ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ by
- calc μ + (ν - ξ)
- _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
- rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
- _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
- _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
- (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [this.1, this.2]
- _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
- simp [restrict_sub_eq_restrict_sub_restrict hs,
- restrict_sub_eq_restrict_sub_restrict hs.compl]
- _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
- constructor
- · rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
- simp
- · rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
- simp
-
-lemma withDensity_sub_aux {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)]
- (hg : Measurable g) (hgf : g ≤ᵐ[μ] f) :
- (μ.withDensity f - μ.withDensity g) = μ.withDensity (f - g) := by
- refine le_antisymm ?_ ?_
- · refine sub_le_of_le_add ?_
- rw [← withDensity_add_right _ hg]
- refine withDensity_mono (ae_of_all _ fun x ↦ ?_)
- simp only [Pi.add_apply, Pi.sub_apply]
- exact le_tsub_add
- · rw [sub_def, le_sInf_iff]
- intro ξ hξ
- simp only [Set.mem_setOf_eq] at hξ
- rw [le_iff] at hξ ⊢
- intro s hs
- specialize hξ s hs
- simp only [coe_add, Pi.add_apply] at hξ
- simp_rw [withDensity_apply _ hs] at hξ ⊢
- simp only [Pi.sub_apply]
- rw [lintegral_sub hg]
- · rwa [tsub_le_iff_right]
- · rw [← withDensity_apply _ hs]
- simp
- · exact ae_restrict_of_ae hgf
-
-lemma withDensity_sub {f g : α → ℝ≥0∞} [IsFiniteMeasure (μ.withDensity g)]
- (hf : Measurable f) (hg : Measurable g) :
- (μ.withDensity f - μ.withDensity g) = μ.withDensity (f - g) := by
- refine le_antisymm ?_ ?_
- · refine sub_le_of_le_add ?_
- rw [← withDensity_add_right _ hg]
- refine withDensity_mono (ae_of_all _ fun x ↦ ?_)
- simp only [Pi.add_apply, Pi.sub_apply]
- exact le_tsub_add
- · let t := {x | f x ≤ g x}
- have ht : MeasurableSet t := measurableSet_le hf hg
- rw [← restrict_add_restrict_compl (μ := μ.withDensity (f - g)) ht,
- ← restrict_add_restrict_compl (μ := μ.withDensity f - μ.withDensity g) ht]
- have h_zero : (μ.withDensity (f - g)).restrict t = 0 := by
- simp only [restrict_eq_zero]
- rw [withDensity_apply _ ht, lintegral_eq_zero_iff (by fun_prop)]
- refine ae_restrict_of_forall_mem ht fun x hx ↦ ?_
- simpa [tsub_eq_zero_iff_le]
- rw [h_zero, zero_add]
- suffices (μ.withDensity (f - g)).restrict tᶜ
- ≤ (μ.withDensity f - μ.withDensity g).restrict tᶜ by
- refine this.trans ?_
- exact Measure.le_add_left le_rfl
- rw [restrict_sub_eq_restrict_sub_restrict ht.compl]
- simp_rw [restrict_withDensity ht.compl]
- have : IsFiniteMeasure ((μ.restrict tᶜ).withDensity g) := by
- rw [← restrict_withDensity ht.compl]
- infer_instance
- rw [withDensity_sub_aux hg]
- refine ae_restrict_of_forall_mem ht.compl fun x hx ↦ ?_
- simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le, t] at hx
- exact hx.le
-
lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) :
(μ - ν) s = ν.withDensity (fun a ↦ μ.rnDeriv ν a - 1) s + μ.singularPart ν s := by
have hμ : μ = ν.withDensity (fun a ↦ μ.rnDeriv ν a) + μ.singularPart ν := by
@@ -140,7 +34,7 @@ lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasur
exact mutuallySingular_singularPart μ ν
simp only [coe_add, Pi.add_apply]
have : IsFiniteMeasure (ν.withDensity 1) := by simp only [withDensity_one]; infer_instance
- rw [add_comm, withDensity_sub (by fun_prop) (by fun_prop)]
+ rw [add_comm, ← withDensity_sub (by fun_prop) (by fun_prop)]
congr
end MeasureTheory.Measure
diff --git a/LeanBandits/ForMathlib/Measurable.lean b/LeanMachineLearning/ForMathlib/Measurable.lean
similarity index 67%
rename from LeanBandits/ForMathlib/Measurable.lean
rename to LeanMachineLearning/ForMathlib/Measurable.lean
index 5a36cdb4..65faf0fc 100644
--- a/LeanBandits/ForMathlib/Measurable.lean
+++ b/LeanMachineLearning/ForMathlib/Measurable.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.Analysis.Normed.Ring.Basic
-import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
+module
+
+public import Mathlib.Analysis.Normed.Ring.Basic
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-!
# Measurability lemmas
-/
+@[expose] public section
+
open Finset
namespace MeasureTheory
@@ -29,25 +33,6 @@ lemma measurable_comp_comap (f : α → β) {g : β → γ} (hg : Measurable g)
rw [← measurable_iff_comap_le]
exact hg
-lemma MeasurableSet.imp {p q : α → Prop}
- (hs : MeasurableSet {x | p x}) (ht : MeasurableSet {x | q x}) :
- MeasurableSet {x | p x → q x} := by
- have h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x} := by
- ext x
- grind
- rw [h_eq]
- exact MeasurableSet.union hs.compl ht
-
-lemma MeasurableSet.iff {p q : α → Prop}
- (hs : MeasurableSet {x | p x}) (ht : MeasurableSet {x | q x}) :
- MeasurableSet {x | p x ↔ q x} := by
- have h_eq : {x | p x ↔ q x} = ({x | p x}ᶜ ∪ {x | q x}) ∩ ({x | q x}ᶜ ∪ {x | p x}) := by
- ext x
- simp only [Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_union, Set.mem_compl_iff]
- grind
- rw [h_eq]
- exact (MeasurableSet.union hs.compl ht).inter (MeasurableSet.union ht.compl hs)
-
@[fun_prop]
lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) :
Measurable (fun a ↦ (f a : ℕ∞)) := Measurable.comp (by fun_prop) hf
@@ -56,11 +41,6 @@ lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) :
lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat) :=
Measurable.comp (by fun_prop) hf
-lemma Measure.trim_comap_apply {X : α → β} (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) :
- μ.trim hX.comap_le (X ⁻¹' s) = μ.map X s := by
- rw [trim_measurableSet_eq, Measure.map_apply (by fun_prop) hs]
- exact ⟨s, hs, rfl⟩
-
lemma measurable_sum_range_of_le {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
(hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i)) (hg : Measurable g) :
Measurable (fun a ↦ ∑ i ∈ range (g a), f i a) := by
diff --git a/LeanBandits/ForMathlib/MeasurableArgMax.lean b/LeanMachineLearning/ForMathlib/MeasurableArgMax.lean
similarity index 97%
rename from LeanBandits/ForMathlib/MeasurableArgMax.lean
rename to LeanMachineLearning/ForMathlib/MeasurableArgMax.lean
index 0769a25d..96399e2b 100644
--- a/LeanBandits/ForMathlib/MeasurableArgMax.lean
+++ b/LeanMachineLearning/ForMathlib/MeasurableArgMax.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
+module
+
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-! # Measurable argmax function
-/
+@[expose] public section
+
open MeasureTheory Finset
open scoped ENNReal NNReal
diff --git a/LeanBandits/ForMathlib/StandardBorel.lean b/LeanMachineLearning/ForMathlib/StandardBorel.lean
similarity index 79%
rename from LeanBandits/ForMathlib/StandardBorel.lean
rename to LeanMachineLearning/ForMathlib/StandardBorel.lean
index e31407b7..ba3cf26f 100644
--- a/LeanBandits/ForMathlib/StandardBorel.lean
+++ b/LeanMachineLearning/ForMathlib/StandardBorel.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.MeasureTheory.Constructions.Polish.Basic
+module
+
+public import Mathlib.MeasureTheory.Constructions.Polish.Basic
/-!
# Properties of standard Borel spaces
-/
+@[expose] public section
+
open MeasureTheory
variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
diff --git a/LeanBandits/ForMathlib/SubGaussian.lean b/LeanMachineLearning/ForMathlib/SubGaussian.lean
similarity index 98%
rename from LeanBandits/ForMathlib/SubGaussian.lean
rename to LeanMachineLearning/ForMathlib/SubGaussian.lean
index c8585c41..68965f0e 100644
--- a/LeanBandits/ForMathlib/SubGaussian.lean
+++ b/LeanMachineLearning/ForMathlib/SubGaussian.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import Mathlib.Probability.Moments.SubGaussian
+module
+
+public import Mathlib.Probability.Moments.SubGaussian
+
+@[expose] public section
open MeasureTheory Real
open scoped ENNReal NNReal
diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanMachineLearning/ForMathlib/Traj.lean
similarity index 96%
rename from LeanBandits/ForMathlib/Traj.lean
rename to LeanMachineLearning/ForMathlib/Traj.lean
index 8d71107a..107e6bb3 100644
--- a/LeanBandits/ForMathlib/Traj.lean
+++ b/LeanMachineLearning/ForMathlib/Traj.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.ForMathlib.HasCondDistrib
-import Mathlib.Probability.Kernel.IonescuTulcea.Traj
-import Mathlib.Probability.Process.FiniteDimensionalLaws
+module
+
+public import LeanMachineLearning.ForMathlib.HasCondDistrib
+public import Mathlib.Probability.Kernel.IonescuTulcea.Traj
+public import Mathlib.Probability.Process.FiniteDimensionalLaws
+
+@[expose] public section
open Filter Finset Function MeasurableEquiv MeasurableSpace MeasureTheory Preorder ProbabilityTheory
@@ -59,6 +63,7 @@ lemma MeasurableEquiv.coe_prodCongr {α β γ δ : Type*}
lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} :
(MeasurableEquiv.refl α : α → α) = id := rfl
+set_option backward.isDefEq.respectTransparency false in
theorem hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)]
{Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ}
(h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
diff --git a/LeanBandits/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
similarity index 97%
rename from LeanBandits/SequentialLearning/Algorithm.lean
rename to LeanMachineLearning/SequentialLearning/Algorithm.lean
index b38a7047..e813da49 100644
--- a/LeanBandits/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -3,13 +3,17 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.ForMathlib.Measurable
-import LeanBandits.ForMathlib.Traj
+module
+
+public import LeanMachineLearning.ForMathlib.Measurable
+public import LeanMachineLearning.ForMathlib.Traj
/-!
# Algorithms
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset
open scoped ENNReal NNReal
@@ -19,6 +23,7 @@ namespace Learning
variable {α R Ω : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω}
/-- A stochastic, sequential algorithm. -/
+-- ANCHOR: Algorithm
structure Algorithm (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where
/-- Policy or sampling rule: distribution of the next action. -/
policy : (n : ℕ) → Kernel (Iic n → α × R) α
@@ -26,11 +31,13 @@ structure Algorithm (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] wher
/-- Distribution of the first action. -/
p0 : Measure α
[hp0 : IsProbabilityMeasure p0]
+-- ANCHOR_END: Algorithm
instance (alg : Algorithm α R) (n : ℕ) : IsMarkovKernel (alg.policy n) := alg.h_policy n
instance (alg : Algorithm α R) : IsProbabilityMeasure alg.p0 := alg.hp0
/-- A stochastic environment. -/
+-- ANCHOR: Environment
structure Environment (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] where
/-- Distribution of the next observation as function of the past history. -/
feedback : (n : ℕ) → Kernel ((Iic n → α × R) × α) R
@@ -38,6 +45,7 @@ structure Environment (α R : Type*) [MeasurableSpace α] [MeasurableSpace R] wh
/-- Distribution of the first observation given the first action. -/
ν0 : Kernel α R
[hp0 : IsMarkovKernel ν0]
+-- ANCHOR_END: Environment
instance (env : Environment α R) (n : ℕ) : IsMarkovKernel (env.feedback n) := env.h_feedback n
instance (env : Environment α R) : IsMarkovKernel env.ν0 := env.hp0
@@ -93,6 +101,7 @@ lemma IsAlgEnvSeq.snd_eval_comp_hist (n : ℕ) :
/-- An algorithm-environment sequence: a sequence of actions and rewards generated
by an algorithm interacting with an environment. -/
+-- ANCHOR: IsAlgEnvSeq
structure IsAlgEnvSeq
[StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
(A : ℕ → Ω → α) (R' : ℕ → Ω → R) (alg : Algorithm α R) (env : Environment α R)
@@ -106,6 +115,7 @@ structure IsAlgEnvSeq
hasCondDistrib_reward n :
HasCondDistrib (R' (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω))
(env.feedback n) P
+-- ANCHOR_END: IsAlgEnvSeq
/-- An algorithm-environment sequence: a sequence of actions and rewards generated
by an algorithm interacting with an environment. -/
@@ -323,9 +333,11 @@ lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
/-- The law of the sequence of actions and observations generated by an algorithm-environment pair
is unique: it does not depend on the probability space used. -/
+-- ANCHOR: isAlgEnvSeq_unique
theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
(h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
+-- ANCHOR_END: isAlgEnvSeq_unique
rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2]
theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
diff --git a/LeanBandits/SequentialLearning/Deterministic.lean b/LeanMachineLearning/SequentialLearning/Deterministic.lean
similarity index 97%
rename from LeanBandits/SequentialLearning/Deterministic.lean
rename to LeanMachineLearning/SequentialLearning/Deterministic.lean
index 91ef55e2..78fc3532 100644
--- a/LeanBandits/SequentialLearning/Deterministic.lean
+++ b/LeanMachineLearning/SequentialLearning/Deterministic.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
-import LeanBandits.SequentialLearning.IonescuTulceaSpace
+module
+
+public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
/-!
# Deterministic algorithms
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset
open scoped ENNReal NNReal
@@ -20,11 +24,13 @@ variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
/-- A deterministic algorithm, which chooses the action given by the function `nextAction`. -/
@[simps]
noncomputable
+-- ANCHOR: detAlgorithm
def detAlgorithm (nextAction : (n : ℕ) → (Iic n → α × R) → α)
(h_next : ∀ n, Measurable (nextAction n)) (action0 : α) :
Algorithm α R where
policy n := Kernel.deterministic (nextAction n) (h_next n)
p0 := Measure.dirac action0
+-- ANCHOR_END: detAlgorithm
variable {nextAction : (n : ℕ) → (Iic n → α × R) → α} {h_next : ∀ n, Measurable (nextAction n)}
{action0 : α} {env : Environment α R}
diff --git a/LeanBandits/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
similarity index 97%
rename from LeanBandits/SequentialLearning/FiniteActions.lean
rename to LeanMachineLearning/SequentialLearning/FiniteActions.lean
index b46415be..2e22a6a6 100644
--- a/LeanBandits/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -3,9 +3,11 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.SequentialLearning.Algorithm
-import Mathlib.Order.CompletePartialOrder
-import Mathlib.Probability.Martingale.BorelCantelli
+module
+
+public import LeanMachineLearning.SequentialLearning.Algorithm
+public import Mathlib.Order.CompletePartialOrder
+public import Mathlib.Probability.Martingale.BorelCantelli
/-!
# Bookkeeping definitions for finite action space sequential learning problems
@@ -20,6 +22,8 @@ be seen as a stochastic process indexed by time `t` on the measurable space `ℕ
-/
+@[expose] public section
+
open MeasureTheory Finset Learning
namespace Learning
@@ -212,7 +216,9 @@ lemma adapted_pullCount_add_one [MeasurableSingletonClass α]
(IsAlgEnvSeq.hist A R' n) := by
ext
exact pullCount_add_one_eq_pullCount'
+ rw [measurable_iff_comap_le]
simp_rw [IsAlgEnvSeq.filtration, this]
+ rw [← measurable_iff_comap_le]
exact measurable_comp_comap _ (measurable_pullCount' n a)
lemma isPredictable_pullCount [MeasurableSingletonClass α]
@@ -255,6 +261,7 @@ lemma exists_pullCount_eq (h' : stepsUntil A a m ω ≠ ⊤) :
rw [← stepsUntil_eq_top_iff] at h_contra
simp [h_contra] at h'
+set_option backward.isDefEq.respectTransparency false in
lemma stepsUntil_zero_of_ne (hka : A 0 ω ≠ a) : stepsUntil A a 0 ω = 0 := by
unfold stepsUntil
simp_rw [← bot_eq_zero, sInf_eq_bot, bot_eq_zero]
@@ -270,6 +277,7 @@ lemma stepsUntil_zero_of_eq (hka : A 0 ω = a) : stepsUntil A a 0 ω = ⊤ := by
rw [← hka, ← zero_add 1, pullCount_action_eq_pullCount_add_one]
simp
+set_option backward.isDefEq.respectTransparency false in
lemma stepsUntil_eq_dite (a : α) (m : ℕ) (ω : Ω)
[Decidable (∃ s, pullCount A a (s + 1) ω = m)] :
stepsUntil A a m ω =
@@ -282,11 +290,12 @@ lemma stepsUntil_eq_dite (a : α) (m : ℕ) (ω : Ω)
· simp only [le_sInf_iff, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂, Nat.cast_le, Nat.find_le_iff]
exact fun n hn ↦ ⟨n, le_rfl, hn⟩
- · push_neg at h'
+ · push Not at h'
suffices {s | pullCount A a (s + 1) ω = m} = ∅ by simp [this]
ext s
simpa using (h' s)
+set_option backward.isDefEq.respectTransparency false in
-- todo: this is in ℝ because of the limited def of leastGE
lemma stepsUntil_eq_leastGE (a : α) (hm : m ≠ 0) :
stepsUntil A a m = leastGE (fun n (ω : Ω) ↦ pullCount A a (n + 1) ω) m := by
@@ -294,7 +303,7 @@ lemma stepsUntil_eq_leastGE (a : α) (hm : m ≠ 0) :
ext ω
rw [stepsUntil_eq_dite]
unfold leastGE hittingAfter
- simp only [zero_le, Set.mem_Ici, Nat.cast_le, true_and, ENat.some_eq_coe]
+ simp only [Nat.bot_eq_zero, zero_le, Set.mem_Ici, true_and, ENat.some_eq_coe]
have h_iff : (∃ s, pullCount A a (s + 1) ω = m) ↔ (∃ s, m ≤ pullCount A a (s + 1) ω) := by
refine ⟨fun ⟨s, hs⟩ ↦ ⟨s, hs.ge⟩, fun ⟨s, hs⟩ ↦ ?_⟩
exact exists_pullCount_eq_of_le hs hm
@@ -321,18 +330,14 @@ lemma stepsUntil_mono (a : α) (ω : Ω) {n m : ℕ} (hn : n ≠ 0) (hnm : n ≤
stepsUntil A a n ω ≤ stepsUntil A a m ω := by
rw [stepsUntil_eq_leastGE a hn, stepsUntil_eq_leastGE a (by lia)]
simp_rw [leastGE]
- have h_Ici_subset : Set.Ici (m : ℝ) ⊆ Set.Ici (n : ℝ) := by
- intro x hx
- simp only [Set.mem_Ici] at hx ⊢
- refine le_trans ?_ hx
- exact mod_cast hnm
- exact hittingAfter_anti (fun n ω ↦ (pullCount A a (n + 1) ω : ℝ)) 0 h_Ici_subset ω
+ exact hittingAfter_anti (fun n ω ↦ (pullCount A a (n + 1) ω)) 0 (fun x ↦ by grind) ω
lemma stepsUntil_pullCount_le (ω : Ω) (a : α) (t : ℕ) :
stepsUntil A a (pullCount A a (t + 1) ω) ω ≤ t := by
rw [stepsUntil]
exact csInf_le (OrderBot.bddBelow _) ⟨t, rfl, rfl⟩
+set_option backward.isDefEq.respectTransparency false in
lemma stepsUntil_pullCount_eq (ω : Ω) (t : ℕ) :
stepsUntil A (A t ω) (pullCount A (A t ω) (t + 1) ω) ω = t := by
apply le_antisymm (stepsUntil_pullCount_le ω (A t ω) t)
@@ -348,6 +353,7 @@ lemma stepsUntil_one_of_eq (hka : A 0 ω = a) : stepsUntil A a 1 ω = 0 := by
have h_le := stepsUntil_pullCount_le (A := A) ω a 0
simpa [h_pull] using h_le
+set_option backward.isDefEq.respectTransparency false in
lemma stepsUntil_eq_zero_iff :
stepsUntil A a m ω = 0 ↔ (m = 0 ∧ A 0 ω ≠ a) ∨ (m = 1 ∧ A 0 ω = a) := by
classical
@@ -414,6 +420,7 @@ lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s +
swap; · simpa [stepsUntil_eq_top_iff]
grind
+set_option backward.isDefEq.respectTransparency false in
lemma pullCount_lt_of_le_stepsUntil (a : α) {n m : ℕ} (ω : Ω)
(h_exists : ∃ s, pullCount A a (s + 1) ω = m) (hn : n < stepsUntil A a m ω) :
pullCount A a (n + 1) ω < m := by
@@ -449,6 +456,7 @@ lemma pullCount_add_one_eq_of_stepsUntil_eq_coe {ω : Ω}
rw [this, pullCount_stepsUntil_add_one]
exact exists_pullCount_eq (by simp [h])
+set_option backward.isDefEq.respectTransparency false in
lemma stepsUntil_eq_iff {ω : Ω} (n : ℕ) :
stepsUntil A a m ω = n ↔
pullCount A a (n + 1) ω = m ∧ (∀ k < n, pullCount A a (k + 1) ω < m) := by
@@ -542,6 +550,7 @@ lemma measurable_stepsUntil' [MeasurableSingletonClass α]
Measurable (fun ω : Ω × (ℕ → α → R) ↦ stepsUntil A a m ω.1) :=
(measurable_stepsUntil hA a m).comp measurable_fst
+set_option backward.isDefEq.respectTransparency false in
lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass α]
(hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (m n : ℕ) :
Measurable[MeasurableSpace.comap
@@ -550,7 +559,8 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass α]
by_cases hm : m = 0
· simp only [hm]
by_cases hn : n = 0
- · simp only [hn, CharP.cast_eq_zero, stepsUntil_eq_zero_iff, ne_eq, true_and, zero_ne_one,
+ · subst hn
+ simp only [CharP.cast_eq_zero, stepsUntil_eq_zero_iff, ne_eq, true_and, zero_ne_one,
false_and, or_false]
refine Measurable.indicator measurable_const ?_
refine (measurableSet_singleton _).compl.preimage ?_
@@ -626,7 +636,8 @@ theorem isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass α]
IsStoppingTime (IsAlgEnvSeq.filtrationAction hA hR') (stepsUntil A a m) := by
refine isStoppingTime_of_measurableSet_eq fun n ↦ ?_
by_cases hn : n = 0
- · simp only [hn, IsAlgEnvSeq.filtrationAction_zero_eq_comap, WithTop.coe_zero]
+ · subst hn
+ simp only [WithTop.coe_zero]
exact measurableSet_stepsUntil_eq_zero a m
· rw [IsAlgEnvSeq.filtrationAction_eq_comap _ hn]
exact measurableSet_stepsUntil_eq hA hR' a m n
@@ -652,7 +663,9 @@ lemma rewardByCount_eq_ite (a : α) (m : ℕ) (ω : Ω × (ℕ → α → R)) :
rewardByCount A R' a m ω =
if (stepsUntil A a m ω.1) = ⊤ then ω.2 m a else R' (stepsUntil A a m ω.1).toNat ω.1 := by
unfold rewardByCount
- cases stepsUntil A a m ω.1 <;> simp
+ cases stepsUntil A a m ω.1
+ · simp; rfl
+ · simp
lemma rewardByCount_eq_add [AddMonoid R] (a : α) (m : ℕ) :
rewardByCount A R' a m =
@@ -741,13 +754,17 @@ def sumRewards' (n : ℕ) (h : Iic n → α × ℝ) (a : α) :=
/-- Empirical mean reward obtained when pulling action `a` up to time `t` (exclusive). -/
noncomputable
+-- ANCHOR: empMean
def empMean (A : ℕ → Ω → α) (R' : ℕ → Ω → ℝ) (a : α) (t : ℕ) (ω : Ω) : ℝ :=
sumRewards A R' a t ω / pullCount A a t ω
+-- ANCHOR_END: empMean
/-- Empirical mean of arm `a` at time `n`. -/
noncomputable
+-- ANCHOR: empMean'
def empMean' (n : ℕ) (h : Iic n → α × ℝ) (a : α) :=
(sumRewards' n h a) / (pullCount' n h a)
+-- ANCHOR_END: empMean'
@[simp]
lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0 := by ext; simp [sumRewards]
diff --git a/LeanBandits/SequentialLearning/IonescuTulceaSpace.lean b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
similarity index 99%
rename from LeanBandits/SequentialLearning/IonescuTulceaSpace.lean
rename to LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
index 7d403cc8..e0aab116 100644
--- a/LeanBandits/SequentialLearning/IonescuTulceaSpace.lean
+++ b/LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.SequentialLearning.Algorithm
+module
+
+public import LeanMachineLearning.SequentialLearning.Algorithm
/-!
# Algorithms
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset
open scoped ENNReal NNReal
@@ -185,8 +189,8 @@ lemma filtrationAction_le_filtration {m n : ℕ} (h : m ≤ n) :
lemma measurable_action_filtrationAction (n : ℕ) :
Measurable[filtrationAction α R n] (action n) := by
- simp only [filtrationAction]
rw [measurable_iff_comap_le]
+ simp only [filtrationAction]
split_ifs with hn
· simp [hn]
· exact le_sup_of_le_right le_rfl
diff --git a/LeanBandits/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
similarity index 96%
rename from LeanBandits/SequentialLearning/StationaryEnv.lean
rename to LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index a52b4a0c..874cd9a0 100644
--- a/LeanBandits/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -3,12 +3,16 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Paulo Rauber
-/
-import LeanBandits.SequentialLearning.IonescuTulceaSpace
+module
+
+public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
/-!
# Stationary environments
-/
+@[expose] public section
+
open MeasureTheory ProbabilityTheory Filter Real Finset
open scoped ENNReal NNReal
@@ -20,9 +24,11 @@ variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R}
/-- A stationary environment, in which the distribution of the next reward depends only on the last
action. -/
@[simps]
+-- ANCHOR: stationaryEnv
def stationaryEnv (ν : Kernel α R) [IsMarkovKernel ν] : Environment α R where
feedback _ := ν.prodMkLeft _
ν0 := ν
+-- ANCHOR_END: stationaryEnv
variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
[StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
diff --git a/README.md b/README.md
index b1a5780a..f5dc7b98 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# Bandit algorithms in Lean
+# Lean Machine Learning
This repository contains a Lean formalization of regret bounds for several stochastic bandit algorithms.
diff --git a/ROADMAP.md b/ROADMAP.md
new file mode 100644
index 00000000..437766dd
--- /dev/null
+++ b/ROADMAP.md
@@ -0,0 +1 @@
+# Roadmap
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
index 4445c547..2ecf7ed1 100644
--- a/blueprint/src/print.tex
+++ b/blueprint/src/print.tex
@@ -24,7 +24,7 @@
\input{macros/common}
\input{macros/print}
-\title{LeanBandits\\ \Large{A Lean package for bandit algorithms}}
+\title{Lean Machine Learning\\ \Large{A Lean package for machine learning algorithms}}
\author{Rémy Degenne, Paulo Rauber}
\begin{document}
diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex
index 8f3ac506..866281c3 100644
--- a/blueprint/src/web.tex
+++ b/blueprint/src/web.tex
@@ -20,14 +20,14 @@
\github{https://github.com/RemyDegenne/lean-bandits}
\dochome{https://RemyDegenne.github.io/lean-bandits/docs}
-\title{LeanBandits}
+\title{Lean Machine Learning}
\author{Rémy Degenne, Paulo Rauber}
\begin{document}
\maketitle
\begin{center}
- \Large{A Lean package for bandit algorithms}
+ \Large{A Lean package for machine learning algorithms}
\end{center}
\input{content}
diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
index 7ac449c4..cddfcc16 100644
--- a/docbuild/lakefile.toml
+++ b/docbuild/lakefile.toml
@@ -4,7 +4,7 @@ version = "0.1.0"
packagesDir = "../.lake/packages"
[[require]]
-name = "LeanBandits"
+name = "LeanMachineLearning"
path = "../"
[[require]]
diff --git a/home_page/_config.yml b/home_page/_config.yml
index 114d6db8..fe31b78c 100644
--- a/home_page/_config.yml
+++ b/home_page/_config.yml
@@ -18,9 +18,9 @@
# You can create any custom variable you would like, and they will be accessible
# in the templates via {{ site.myvariable }}.
-title: LeanBandits
+title: Lean Machine Learning
#email: your-email@example.com
-description: A Lean formalization of bandit algorithms by Remy Degenne and Paulo Rauber
+description: A Lean formalization of machine learning algorithms by Remy Degenne and Paulo Rauber
baseurl: "" # the subpath of your site, e.g. /blog
url: "https://RemyDegenne.github.io/lean-bandits" # the base hostname & protocol for your site, e.g. http://example.com
twitter_username:
diff --git a/home_page/_layouts/default.html b/home_page/_layouts/default.html
index 51305743..702ad836 100644
--- a/home_page/_layouts/default.html
+++ b/home_page/_layouts/default.html
@@ -29,6 +29,7 @@ {{ page.description | default: site.description | de
}}
Blueprint (web)
Blueprint (pdf)
+ Tutorials
Documentation
{% if site.github.is_project_page %}
GitHub
@@ -47,4 +48,4 @@ {{ page.description | default: site.description | de
-