Rebrand

.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

.gitignore

@@ -37,3 +37,7 @@ blueprint/src/web.pdf
 *.synctex.gz
 *.synctex.gz(busy)
 *.pdfsync
+## Verso
+/verso/.lake/
+/verso/html/
+/home_page/verso

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.

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

LeanBandits/Bandit/Bandit.lean → 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]

LeanBandits/Bandit/Regret.lean → 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