From 8908b268186767f40e4b40ff674efc12bb51848f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Wed, 24 Jun 2026 19:04:12 +0200
Subject: [PATCH 01/16] replace `measurableArgmax`

---
 .../BorelSpace/MeasurableArgMax.lean          |  88 ------------
 .../MeasureTheory/Order/Lattice.lean          |  23 +++
 .../MeasureTheory/Order/MeasurableArg.lean    | 135 ++++++++++++++++++
 .../Online/Bandit/Algorithms/ETC.lean         |  14 +-
 .../Online/Bandit/Algorithms/UCB.lean         |   9 +-
 .../Online/Bandit/BayesRegret.lean            |  11 +-
 6 files changed, 175 insertions(+), 105 deletions(-)
 delete mode 100644 LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean
 create mode 100644 LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
 create mode 100644 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean
deleted file mode 100644
index 96399e2b..00000000
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Constructions/BorelSpace/MeasurableArgMax.lean
+++ /dev/null
@@ -1,88 +0,0 @@
-/-
-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
--/
-module
-
-public import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
-
-/-! # Measurable argmax function
-
--/
-
-@[expose] public section
-
-open MeasureTheory Finset
-open scoped ENNReal NNReal
-
-section MeasurableArgmax -- copied from PR #27579 (and changed from argmin to argmax)
-
-lemma measurable_encode {α : Type*} {_ : MeasurableSpace α} [Encodable α]
-    [MeasurableSingletonClass α] :
-    Measurable (Encodable.encode (α := α)) := by
-  refine measurable_to_nat fun a ↦ ?_
-  have : Encodable.encode ⁻¹' {Encodable.encode a} = {a} := by ext; simp
-  rw [this]
-  exact measurableSet_singleton _
-
-lemma measurableEmbedding_encode (α : Type*) {_ : MeasurableSpace α} [Encodable α]
-    [MeasurableSingletonClass α] :
-    MeasurableEmbedding (Encodable.encode (α := α)) where
-  injective := Encodable.encode_injective
-  measurable := measurable_encode
-  measurableSet_image' _ _ := .of_discrete
-
-section Finite
-
-variable {𝓧 𝓨 α : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨}
-  {mα : MeasurableSpace α} [TopologicalSpace α] [LinearOrder α]
-  [OpensMeasurableSpace α] [OrderClosedTopology α] [SecondCountableTopology α]
-
-lemma measurableSet_isMax [Countable 𝓨]
-    {f : 𝓧 → 𝓨 → α} (hf : ∀ y, Measurable (fun x ↦ f x y)) (y : 𝓨) :
-    MeasurableSet {x | ∀ z, f x z ≤ f x y} := by
-  rw [show {x | ∀ y', f x y' ≤ f x y} = ⋂ y', {x | f x y' ≤ f x y} by ext; simp]
-  exact MeasurableSet.iInter fun z ↦ measurableSet_le (by fun_prop) (by fun_prop)
-
-lemma exists_isMaxOn' {α : Type*} [LinearOrder α]
-    [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] (f : 𝓧 → 𝓨 → α) (x : 𝓧) :
-    ∃ n : ℕ, ∃ y, n = Encodable.encode y ∧ ∀ z, f x z ≤ f x y := by
-  obtain ⟨y, h⟩ := Finite.exists_max (f x)
-  exact ⟨Encodable.encode y, y, rfl, h⟩
-
-/-- A measurable argmax function. -/
-noncomputable
-def measurableArgmax [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
-    (f : 𝓧 → 𝓨 → α)
-    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
-    (x : 𝓧) :
-    𝓨 :=
-  (measurableEmbedding_encode 𝓨).invFun (Nat.find (exists_isMaxOn' f x))
-
-lemma measurable_measurableArgmax [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
-    {f : 𝓧 → 𝓨 → α}
-    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
-    (hf : ∀ y, Measurable (fun x ↦ f x y)) :
-    Measurable (measurableArgmax f) := by
-  refine (MeasurableEmbedding.measurable_invFun (measurableEmbedding_encode 𝓨)).comp ?_
-  refine measurable_find _ fun n ↦ ?_
-  have : {x | ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y}
-      = ⋃ y, ({x | n = Encodable.encode y} ∩ {x | ∀ z, f x z ≤ f x y}) := by ext; simp
-  rw [this]
-  refine MeasurableSet.iUnion fun y ↦ (MeasurableSet.inter (by simp) ?_)
-  exact measurableSet_isMax (by fun_prop) y
-
-lemma isMaxOn_measurableArgmax {α : Type*} [LinearOrder α]
-    [Nonempty 𝓨] [Finite 𝓨] [Encodable 𝓨] [MeasurableSingletonClass 𝓨]
-    (f : 𝓧 → 𝓨 → α)
-    [∀ x, DecidablePred fun n ↦ ∃ y, n = Encodable.encode y ∧ ∀ (z : 𝓨), f x z ≤ f x y]
-    (x : 𝓧) (z : 𝓨) :
-    f x z ≤ f x (measurableArgmax f x) := by
-  obtain ⟨y, h_eq, h_le⟩ := Nat.find_spec (exists_isMaxOn' f x)
-  refine le_trans (h_le z) (le_of_eq ?_)
-  rw [measurableArgmax, h_eq,
-    MeasurableEmbedding.leftInverse_invFun (measurableEmbedding_encode 𝓨) y]
-
-end Finite
-end MeasurableArgmax
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
new file mode 100644
index 00000000..7ff66f06
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
@@ -0,0 +1,23 @@
+/-
+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 Mathlib.MeasureTheory.Order.Lattice
+
+/-! # Measurable inf of a finite set
+
+-/
+
+@[expose] public section
+
+open Finset
+
+variable {δ α : Type*} [MeasurableSpace δ] [SemilatticeInf α] [MeasurableSpace α] [MeasurableInf₂ α]
+
+@[fun_prop]
+theorem Finset.measurable_inf' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}
+    (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f) :=
+  Finset.inf'_induction hs _ (fun _f hf _g hg => hf.inf hg) fun n hn => hf n hn
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
new file mode 100644
index 00000000..c8b4390f
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -0,0 +1,135 @@
+/-
+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.ForMathlib.MeasureTheory.Order.Lattice
+public import Mathlib
+
+@[expose] public section
+
+open Finset
+
+variable {ι α : Type*} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α)
+
+namespace Function
+
+/-- The maximum value of a tuple. -/
+abbrev max : α := univ.sup' (by simp) f
+
+/-- The minimum value of a tuple. -/
+abbrev min : α := univ.inf' (by simp) f
+
+lemma le_max (x : ι) : f x ≤ max f := le_sup' _ (by simp)
+
+lemma min_le (x : ι) : min f ≤ f x := inf'_le _ (by simp)
+
+end Function
+
+section Argmax
+
+lemma exists_argmax : ∃ i, f i = f.max := by
+  obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
+  exact ⟨i, hi.symm⟩
+
+/-- The index of the maximum value of a tuple. -/
+noncomputable def measurableArgmax := (exists_argmax f).choose
+
+lemma argmax_spec : f (measurableArgmax f) = f.max := (exists_argmax f).choose_spec
+
+lemma isMaxOn_measurableArgmax (x : ι) : f x ≤ f (measurableArgmax f) := by
+  rw [argmax_spec f]
+  exact f.le_max x
+
+end Argmax
+
+section Argmin
+
+lemma exists_argmin : ∃ i, f i = f.min := by
+  obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_inf' (by simp : Finset.univ.Nonempty) f
+  exact ⟨i, hi.symm⟩
+
+/-- The index of the minimum value of a tuple. -/
+noncomputable def measurableArgmin := (exists_argmin f).choose
+
+lemma argmin_spec : f (measurableArgmin f) = f.min := (exists_argmin f).choose_spec
+
+lemma isMinOn_measurableArgmin (x : ι) : f (measurableArgmin f) ≤ f x := by
+  rw [argmin_spec f]
+  exact f.min_le x
+
+end Argmin
+
+lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] :
+    -f.max = (-f).min := by
+  refine le_antisymm ?_ ?_
+  · simp; grind
+  · simp only [inf'_le_iff, mem_univ, Pi.neg_apply, neg_le_neg_iff, sup'_le_iff, forall_const,
+      true_and]
+    exact ⟨measurableArgmax f, isMaxOn_measurableArgmax f⟩
+
+variable [MeasurableSpace α]
+
+section MeasurableArgmax
+
+@[fun_prop]
+lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => t.max) := by
+  suffices (fun f : ι → α ↦ f.max) = (univ.sup' univ_nonempty fun i f => f i) by
+    rw [this]
+    exact measurable_sup' univ_nonempty (fun i _ => measurable_pi_apply i)
+  ext; simp [Function.max]
+
+@[fun_prop]
+lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] :
+    Measurable fun f : ι → α ↦ measurableArgmax f := by
+  refine measurable_to_countable' fun i ↦ ?_
+  simp only [Set.preimage, Set.mem_singleton_iff]
+  let Maximizers (f : ι → α) : Set ι := {i | f i = f.max}
+  suffices {f : ι → α | measurableArgmax f = i} = ⋃ (S)
+      (hS : ∀ x, Maximizers x = S → measurableArgmax x = i), {f | Maximizers f = S} by
+    rw [this]
+    refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
+    exact measurableSet_eq_fun (by fun_prop) measurable_const
+  ext f
+  simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
+  constructor
+  · intro hf x hx
+    rw [← hf]
+    exact Classical.choose.congr_simp hx (exists_argmax x)
+  · intro h
+    exact h f rfl
+
+end MeasurableArgmax
+
+section MeasurableArgmin
+
+@[fun_prop]
+lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (f : ι → α) => f.min) := by
+  suffices (fun f : ι → α ↦ f.min) = (univ.inf' univ_nonempty fun i f => f i) by
+    rw [this]
+    exact measurable_inf' univ_nonempty (fun i _ => measurable_pi_apply i)
+  ext; simp [Function.min]
+
+@[fun_prop]
+lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂ α] :
+    Measurable fun f : ι → α ↦ measurableArgmin f := by
+  refine measurable_to_countable' fun i ↦ ?_
+  simp only [Set.preimage, Set.mem_singleton_iff]
+  let Minimizers (f : ι → α) : Set ι := {i | f i = f.min}
+  suffices {f : ι → α | measurableArgmin f = i} = ⋃ (S)
+      (hS : ∀ x, Minimizers x = S → measurableArgmin x = i), {f | Minimizers f = S} by
+    rw [this]
+    refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
+    exact measurableSet_eq_fun (by fun_prop) measurable_const
+  ext f
+  simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
+  constructor
+  · intro hf x hx
+    rw [← hf]
+    exact Classical.choose.congr_simp hx (exists_argmin x)
+  · intro h
+    exact h f rfl
+
+end MeasurableArgmin
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 9bdda650..77d49941 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -7,7 +7,7 @@ module
 
 public import LeanMachineLearning.Online.Bandit.SumRewards
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 
 /-! # The Explore-Then-Commit Algorithm
 
@@ -33,7 +33,7 @@ def ETC.nextArm (hK : 0 < K) (m n : ℕ) (h : Iic n → Fin K × ℝ) : Fin K :=
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   if hn : n < K * m - 1 then RoundRobin.nextAction hK n
   else
-    if hn_eq : n = K * m - 1 then measurableArgmax (empMean' n) h
+    if hn_eq : n = K * m - 1 then measurableArgmax (empMean' n h)
     else (h ⟨n, by simp⟩).1
 
 /-- The next arm pulled by ETC is chosen in a measurable way. -/
@@ -44,7 +44,7 @@ lemma ETC.measurable_nextArm (hK : 0 < K) (m n : ℕ) : Measurable (nextArm hK m
   simp only [dite_eq_ite]
   refine Measurable.ite (by simp) (by fun_prop) ?_
   refine Measurable.ite (by simp) ?_ (by fun_prop)
-  exact measurable_measurableArgmax fun a ↦ by fun_prop
+  fun_prop
 
 /-- The Explore-Then-Commit algorithm: deterministic algorithm that chooses the next arm according
 to `ETC.nextArm`. -/
@@ -100,8 +100,8 @@ lemma arm_of_lt [Nonempty (Fin K)]
 phase. -/
 lemma arm_mul [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (hm : m ≠ 0) :
-    A (K * m) =ᵐ[P] fun ω ↦ measurableArgmax (empMean' (K * m - 1))
-      (history A R (K * m - 1) ω) := by
+    A (K * m) =ᵐ[P]
+      fun ω ↦ measurableArgmax (empMean' (K * m - 1) (history A R (K * m - 1) ω)) := by
   have : K * m = (K * m - 1) + 1 := by
     have : 0 < K * m := Nat.mul_pos hK hm.bot_lt
     grind
@@ -176,8 +176,8 @@ lemma sumRewards_bestArm_le_of_arm_mul_eq [Nonempty (Fin K)]
       sumRewards A R a (K * m) h := by
   filter_upwards [arm_mul h hm, pullCount_mul h a, pullCount_mul h (bestArm ν)]
     with h h_arm ha h_best h_eq
-  have h_max := isMaxOn_measurableArgmax (empMean' (K * m - 1)) (history A R (K * m - 1) h)
-    (bestArm ν)
+  have h_max := isMaxOn_measurableArgmax
+    (empMean' (K * m - 1) (history A R (K * m - 1) h)) (bestArm ν)
   rw [← h_arm, h_eq] at h_max
   rw [sumRewards_eq_pullCount_mul_empMean, sumRewards_eq_pullCount_mul_empMean, ha, h_best]
   · gcongr
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 2d1e2fb7..d82014d1 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -7,7 +7,7 @@ module
 
 public import LeanMachineLearning.Online.Bandit.SumRewards
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 
 /-!
 # UCB algorithm
@@ -37,13 +37,12 @@ noncomputable
 def UCB.nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) : Fin K :=
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   if n < K - 1 then RoundRobin.nextAction hK n else
-  measurableArgmax (fun h a ↦ empMean' n h a + ucbWidth' c n h a) h
+  measurableArgmax (fun a ↦ empMean' n h a + ucbWidth' c n h a)
 
 @[fun_prop]
 lemma UCB.measurable_nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) : Measurable (nextArm hK c n) := by
   refine Measurable.ite (by simp) (by fun_prop) ?_
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
-  refine measurable_measurableArgmax fun a ↦ ?_
   unfold ucbWidth'
   fun_prop
 
@@ -125,8 +124,8 @@ lemma ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   simp_rw [h_arm, empMean_eq_empMean' (by grind : n ≠ 0),
     ucbWidth_eq_ucbWidth' (A := A) (R := R) _ _ _ _ (by grind : n ≠ 0)]
-  exact isMaxOn_measurableArgmax (fun h a ↦ empMean' (n - 1) h a + ucbWidth' c (n - 1) h a)
-    (history A R (n - 1) h) a
+  exact isMaxOn_measurableArgmax (fun a ↦ empMean' (n - 1) (history A R (n - 1) h) a
+    + ucbWidth' c (n - 1) (history A R (n - 1) h) a) _
 
 lemma forall_arm_eq_mod_of_lt [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
diff --git a/LeanMachineLearning/Online/Bandit/BayesRegret.lean b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
index 981f1c70..85e7d971 100644
--- a/LeanMachineLearning/Online/Bandit/BayesRegret.lean
+++ b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
@@ -5,7 +5,7 @@ Authors: Paulo Rauber, Rémy Degenne
 -/
 module
 
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 public import LeanMachineLearning.Online.Bandit.Regret
 
 /-!
@@ -70,12 +70,13 @@ lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonCl
 noncomputable
 def bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
     (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 :=
-  measurableArgmax (fun ω' a ↦ actionMean κ E a ω') ω
+  measurableArgmax (fun a ↦ actionMean κ E a ω)
 
 @[fun_prop]
 lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
-    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) : Measurable (bestAction κ E) :=
-  measurable_measurableArgmax (by fun_prop)
+    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) : Measurable (bestAction κ E) := by
+  unfold bestAction
+  fun_prop
 
 /-- A random variable that gives the gap at time `n`. -/
 noncomputable
@@ -100,7 +101,7 @@ lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSing
   rw [gap, Bandits.gap]
   congr
   apply le_antisymm
-  · exact ciSup_le (isMaxOn_measurableArgmax (fun ω' a ↦ actionMean κ E a ω') ω)
+  · exact ciSup_le <| isMaxOn_measurableArgmax (fun a ↦ actionMean κ E a ω)
   · exact Finite.le_ciSup (fun a ↦ actionMean κ E a ω) _
 
 @[fun_prop]

From d01de987d13194f8e0aae1c7bfd43943faf54b59 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Wed, 24 Jun 2026 19:08:00 +0200
Subject: [PATCH 02/16] refactor

---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean          | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index c8b4390f..0d2a322d 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -62,8 +62,7 @@ lemma isMinOn_measurableArgmin (x : ι) : f (measurableArgmin f) ≤ f x := by
 
 end Argmin
 
-lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] :
-    -f.max = (-f).min := by
+lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] : -f.max = (-f).min := by
   refine le_antisymm ?_ ?_
   · simp; grind
   · simp only [inf'_le_iff, mem_univ, Pi.neg_apply, neg_le_neg_iff, sup'_le_iff, forall_const,

From 6f6250fa6ad70db9c28957d012c1f494466583d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Wed, 24 Jun 2026 19:11:43 +0200
Subject: [PATCH 03/16] refactor

---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index 0d2a322d..bb14f081 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -31,7 +31,7 @@ end Function
 section Argmax
 
 lemma exists_argmax : ∃ i, f i = f.max := by
-  obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
+  obtain ⟨i, -, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
   exact ⟨i, hi.symm⟩
 
 /-- The index of the maximum value of a tuple. -/
@@ -48,7 +48,7 @@ end Argmax
 section Argmin
 
 lemma exists_argmin : ∃ i, f i = f.min := by
-  obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_inf' (by simp : Finset.univ.Nonempty) f
+  obtain ⟨i, -, hi⟩ := Finset.exists_mem_eq_inf' (by simp : Finset.univ.Nonempty) f
   exact ⟨i, hi.symm⟩
 
 /-- The index of the minimum value of a tuple. -/

From cf020b107e753955308996b7957ba196a003d9de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Wed, 24 Jun 2026 19:12:17 +0200
Subject: [PATCH 04/16] mk_all

---
 LMLTutorial.lean         | 18 ++++++++++--------
 LeanMachineLearning.lean |  3 ++-
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/LMLTutorial.lean b/LMLTutorial.lean
index 6872a6d1..605cd0d5 100644
--- a/LMLTutorial.lean
+++ b/LMLTutorial.lean
@@ -1,8 +1,10 @@
-import LMLTutorial.Front
-import LMLTutorial.Pages.BasicProbability
-import LMLTutorial.Pages.DefiningAlgorithm
-import LMLTutorial.Pages.Installation
-import LMLTutorial.Pages.MarkovKernels
-import LMLTutorial.Pages.Martingales
-import LMLTutorial.References
-import LMLTutorial.Tutorial
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import LMLTutorial.Front
+public import LMLTutorial.Pages.BasicProbability
+public import LMLTutorial.Pages.DefiningAlgorithm
+public import LMLTutorial.Pages.Installation
+public import LMLTutorial.Pages.MarkovKernels
+public import LMLTutorial.Pages.Martingales
+public import LMLTutorial.References
+public import LMLTutorial.Tutorial
diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 12be32f8..ce81269a 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -1,9 +1,10 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
-public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Constructions.Polish.StandardBorel
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 public import LeanMachineLearning.ForMathlib.MeasureTheory.OuterMeasure.Basic
 public import LeanMachineLearning.ForMathlib.Probability.HasCondDistrib
 public import LeanMachineLearning.ForMathlib.Probability.Independence.CondDistrib

From 42a054fb6c5d94cffad481d696e46451bdb093f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Wed, 24 Jun 2026 19:17:27 +0200
Subject: [PATCH 05/16] imports and name

---
 LMLTutorial/Pages/DefiningAlgorithm.lean      |  2 +-
 .../MeasureTheory/Order/MeasurableArg.lean    | 42 +++++++++++--------
 .../Online/Bandit/Algorithms/ETC.lean         |  6 +--
 .../Online/Bandit/Algorithms/UCB.lean         |  4 +-
 .../Online/Bandit/BayesRegret.lean            |  4 +-
 5 files changed, 32 insertions(+), 26 deletions(-)

diff --git a/LMLTutorial/Pages/DefiningAlgorithm.lean b/LMLTutorial/Pages/DefiningAlgorithm.lean
index bc9387d4..bcf9b60c 100644
--- a/LMLTutorial/Pages/DefiningAlgorithm.lean
+++ b/LMLTutorial/Pages/DefiningAlgorithm.lean
@@ -105,7 +105,7 @@ It starts by choosing each action once and then chooses $`\arg\max_a (\hat{\mu}_
 
 To define the algorithm, we first define the exploration bonus and the next action function, and then we use `detAlgorithm` to build the algorithm.
 We also need to prove that the next action function is measurable, which is done by the `measurable_nextArm` lemma.
-Note that we are careful to use a measurable version of the argmax function, `measurableArgmax`.
+Note that we are careful to use a measurable version of the argmax function, `argmax`.
 
 {docstring Bandits.ucbWidth'}
 
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index bb14f081..f4db8385 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -6,7 +6,13 @@ Authors: Gaëtan Serré
 module
 
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice
-public import Mathlib
+public import Mathlib.CategoryTheory.Countable
+public import Mathlib.MeasureTheory.Constructions.Polish.Basic
+public import Mathlib.Order.CompletePartialOrder
+
+/-! # Measurable argmax and argmin functions
+
+-/
 
 @[expose] public section
 
@@ -35,11 +41,11 @@ lemma exists_argmax : ∃ i, f i = f.max := by
   exact ⟨i, hi.symm⟩
 
 /-- The index of the maximum value of a tuple. -/
-noncomputable def measurableArgmax := (exists_argmax f).choose
+noncomputable def argmax := (exists_argmax f).choose
 
-lemma argmax_spec : f (measurableArgmax f) = f.max := (exists_argmax f).choose_spec
+lemma argmax_spec : f (argmax f) = f.max := (exists_argmax f).choose_spec
 
-lemma isMaxOn_measurableArgmax (x : ι) : f x ≤ f (measurableArgmax f) := by
+lemma isMaxOn_argmax (x : ι) : f x ≤ f (argmax f) := by
   rw [argmax_spec f]
   exact f.le_max x
 
@@ -52,11 +58,11 @@ lemma exists_argmin : ∃ i, f i = f.min := by
   exact ⟨i, hi.symm⟩
 
 /-- The index of the minimum value of a tuple. -/
-noncomputable def measurableArgmin := (exists_argmin f).choose
+noncomputable def argmin := (exists_argmin f).choose
 
-lemma argmin_spec : f (measurableArgmin f) = f.min := (exists_argmin f).choose_spec
+lemma argmin_spec : f (argmin f) = f.min := (exists_argmin f).choose_spec
 
-lemma isMinOn_measurableArgmin (x : ι) : f (measurableArgmin f) ≤ f x := by
+lemma isMinOn_argmin (x : ι) : f (argmin f) ≤ f x := by
   rw [argmin_spec f]
   exact f.min_le x
 
@@ -67,11 +73,11 @@ lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] : -f.m
   · simp; grind
   · simp only [inf'_le_iff, mem_univ, Pi.neg_apply, neg_le_neg_iff, sup'_le_iff, forall_const,
       true_and]
-    exact ⟨measurableArgmax f, isMaxOn_measurableArgmax f⟩
+    exact ⟨argmax f, isMaxOn_argmax f⟩
 
 variable [MeasurableSpace α]
 
-section MeasurableArgmax
+section argmax
 
 @[fun_prop]
 lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => t.max) := by
@@ -82,12 +88,12 @@ lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) =>
 
 @[fun_prop]
 lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] :
-    Measurable fun f : ι → α ↦ measurableArgmax f := by
+    Measurable fun f : ι → α ↦ argmax f := by
   refine measurable_to_countable' fun i ↦ ?_
   simp only [Set.preimage, Set.mem_singleton_iff]
   let Maximizers (f : ι → α) : Set ι := {i | f i = f.max}
-  suffices {f : ι → α | measurableArgmax f = i} = ⋃ (S)
-      (hS : ∀ x, Maximizers x = S → measurableArgmax x = i), {f | Maximizers f = S} by
+  suffices {f : ι → α | argmax f = i} = ⋃ (S)
+      (hS : ∀ x, Maximizers x = S → argmax x = i), {f | Maximizers f = S} by
     rw [this]
     refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
     exact measurableSet_eq_fun (by fun_prop) measurable_const
@@ -100,9 +106,9 @@ lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂
   · intro h
     exact h f rfl
 
-end MeasurableArgmax
+end argmax
 
-section MeasurableArgmin
+section argmin
 
 @[fun_prop]
 lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (f : ι → α) => f.min) := by
@@ -113,12 +119,12 @@ lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (f : ι → α) =>
 
 @[fun_prop]
 lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂ α] :
-    Measurable fun f : ι → α ↦ measurableArgmin f := by
+    Measurable fun f : ι → α ↦ argmin f := by
   refine measurable_to_countable' fun i ↦ ?_
   simp only [Set.preimage, Set.mem_singleton_iff]
   let Minimizers (f : ι → α) : Set ι := {i | f i = f.min}
-  suffices {f : ι → α | measurableArgmin f = i} = ⋃ (S)
-      (hS : ∀ x, Minimizers x = S → measurableArgmin x = i), {f | Minimizers f = S} by
+  suffices {f : ι → α | argmin f = i} = ⋃ (S)
+      (hS : ∀ x, Minimizers x = S → argmin x = i), {f | Minimizers f = S} by
     rw [this]
     refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
     exact measurableSet_eq_fun (by fun_prop) measurable_const
@@ -131,4 +137,4 @@ lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂
   · intro h
     exact h f rfl
 
-end MeasurableArgmin
+end argmin
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 77d49941..da305e65 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -33,7 +33,7 @@ def ETC.nextArm (hK : 0 < K) (m n : ℕ) (h : Iic n → Fin K × ℝ) : Fin K :=
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   if hn : n < K * m - 1 then RoundRobin.nextAction hK n
   else
-    if hn_eq : n = K * m - 1 then measurableArgmax (empMean' n h)
+    if hn_eq : n = K * m - 1 then argmax (empMean' n h)
     else (h ⟨n, by simp⟩).1
 
 /-- The next arm pulled by ETC is chosen in a measurable way. -/
@@ -101,7 +101,7 @@ phase. -/
 lemma arm_mul [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (hm : m ≠ 0) :
     A (K * m) =ᵐ[P]
-      fun ω ↦ measurableArgmax (empMean' (K * m - 1) (history A R (K * m - 1) ω)) := by
+      fun ω ↦ argmax (empMean' (K * m - 1) (history A R (K * m - 1) ω)) := by
   have : K * m = (K * m - 1) + 1 := by
     have : 0 < K * m := Nat.mul_pos hK hm.bot_lt
     grind
@@ -176,7 +176,7 @@ lemma sumRewards_bestArm_le_of_arm_mul_eq [Nonempty (Fin K)]
       sumRewards A R a (K * m) h := by
   filter_upwards [arm_mul h hm, pullCount_mul h a, pullCount_mul h (bestArm ν)]
     with h h_arm ha h_best h_eq
-  have h_max := isMaxOn_measurableArgmax
+  have h_max := isMaxOn_argmax
     (empMean' (K * m - 1) (history A R (K * m - 1) h)) (bestArm ν)
   rw [← h_arm, h_eq] at h_max
   rw [sumRewards_eq_pullCount_mul_empMean, sumRewards_eq_pullCount_mul_empMean, ha, h_best]
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index d82014d1..8183b0f8 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -37,7 +37,7 @@ noncomputable
 def UCB.nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) (h : Iic n → Fin K × ℝ) : Fin K :=
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   if n < K - 1 then RoundRobin.nextAction hK n else
-  measurableArgmax (fun a ↦ empMean' n h a + ucbWidth' c n h a)
+  argmax (fun a ↦ empMean' n h a + ucbWidth' c n h a)
 
 @[fun_prop]
 lemma UCB.measurable_nextArm (hK : 0 < K) (c : ℝ) (n : ℕ) : Measurable (nextArm hK c n) := by
@@ -124,7 +124,7 @@ lemma ucbIndex_le_ucbIndex_arm [Nonempty (Fin K)]
   have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK
   simp_rw [h_arm, empMean_eq_empMean' (by grind : n ≠ 0),
     ucbWidth_eq_ucbWidth' (A := A) (R := R) _ _ _ _ (by grind : n ≠ 0)]
-  exact isMaxOn_measurableArgmax (fun a ↦ empMean' (n - 1) (history A R (n - 1) h) a
+  exact isMaxOn_argmax (fun a ↦ empMean' (n - 1) (history A R (n - 1) h) a
     + ucbWidth' c (n - 1) (history A R (n - 1) h) a) _
 
 lemma forall_arm_eq_mod_of_lt [Nonempty (Fin K)]
diff --git a/LeanMachineLearning/Online/Bandit/BayesRegret.lean b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
index 85e7d971..aaa582e1 100644
--- a/LeanMachineLearning/Online/Bandit/BayesRegret.lean
+++ b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
@@ -70,7 +70,7 @@ lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonCl
 noncomputable
 def bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
     (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 :=
-  measurableArgmax (fun a ↦ actionMean κ E a ω)
+  argmax (fun a ↦ actionMean κ E a ω)
 
 @[fun_prop]
 lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
@@ -101,7 +101,7 @@ lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSing
   rw [gap, Bandits.gap]
   congr
   apply le_antisymm
-  · exact ciSup_le <| isMaxOn_measurableArgmax (fun a ↦ actionMean κ E a ω)
+  · exact ciSup_le <| isMaxOn_argmax (fun a ↦ actionMean κ E a ω)
   · exact Finite.le_ciSup (fun a ↦ actionMean κ E a ω) _
 
 @[fun_prop]

From c7a2a0dfb4ccbfc39262ff21a8e01adc0468400a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 14:54:00 +0200
Subject: [PATCH 06/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean         | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index f4db8385..c39a2ead 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -10,7 +10,9 @@ public import Mathlib.CategoryTheory.Countable
 public import Mathlib.MeasureTheory.Constructions.Polish.Basic
 public import Mathlib.Order.CompletePartialOrder
 
-/-! # Measurable argmax and argmin functions
+/-! # Argmax and argmin functions on finite sets
+
+We prove in particular that those functions are measurable.
 
 -/
 

From 5164171e07f3e1fe47ac5c477410b9bc24656491 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 14:54:16 +0200
Subject: [PATCH 07/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean          | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index c39a2ead..a2464cc9 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -86,7 +86,8 @@ lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) =>
   suffices (fun f : ι → α ↦ f.max) = (univ.sup' univ_nonempty fun i f => f i) by
     rw [this]
     exact measurable_sup' univ_nonempty (fun i _ => measurable_pi_apply i)
-  ext; simp [Function.max]
+  ext
+  simp [Function.max]
 
 @[fun_prop]
 lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] :

From 02d245011850d119b2f4bee5cb23c5f8c151f678 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 14:54:22 +0200
Subject: [PATCH 08/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean          | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index a2464cc9..08d12d91 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -118,7 +118,8 @@ lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (f : ι → α) =>
   suffices (fun f : ι → α ↦ f.min) = (univ.inf' univ_nonempty fun i f => f i) by
     rw [this]
     exact measurable_inf' univ_nonempty (fun i _ => measurable_pi_apply i)
-  ext; simp [Function.min]
+  ext
+  simp [Function.min]
 
 @[fun_prop]
 lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂ α] :

From dca752a146197237609e936ad6bc1de7768f2b78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 14:54:31 +0200
Subject: [PATCH 09/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean    | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index 08d12d91..132db1a1 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -25,15 +25,12 @@ variable {ι α : Type*} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι →
 namespace Function
 
 /-- The maximum value of a tuple. -/
-abbrev max : α := univ.sup' (by simp) f
-
-/-- The minimum value of a tuple. -/
-abbrev min : α := univ.inf' (by simp) f
+@[to_dual /-- The minimum value of a tuple. -/]
+abbrev max : α := univ.sup' univ_nonempty f
 
+@[to_dual min_le]
 lemma le_max (x : ι) : f x ≤ max f := le_sup' _ (by simp)
 
-lemma min_le (x : ι) : min f ≤ f x := inf'_le _ (by simp)
-
 end Function
 
 section Argmax

From 5344af47949c5203238dcf3958536e308539f642 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Fri, 26 Jun 2026 15:09:03 +0200
Subject: [PATCH 10/16] Use `to_dual`

---
 .../MeasureTheory/Order/MeasurableArg.lean    | 45 +++++--------------
 1 file changed, 12 insertions(+), 33 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index 132db1a1..e52fb6b8 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -35,49 +35,25 @@ end Function
 
 section Argmax
 
+@[to_dual exists_argmin]
 lemma exists_argmax : ∃ i, f i = f.max := by
   obtain ⟨i, -, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) f
   exact ⟨i, hi.symm⟩
 
 /-- The index of the maximum value of a tuple. -/
+@[to_dual argmin /-- The index of the minimum value of a tuple. -/]
 noncomputable def argmax := (exists_argmax f).choose
 
+@[to_dual argmin_spec]
 lemma argmax_spec : f (argmax f) = f.max := (exists_argmax f).choose_spec
 
+@[to_dual isMinOn_argmin]
 lemma isMaxOn_argmax (x : ι) : f x ≤ f (argmax f) := by
   rw [argmax_spec f]
   exact f.le_max x
 
-end Argmax
-
-section Argmin
-
-lemma exists_argmin : ∃ i, f i = f.min := by
-  obtain ⟨i, -, hi⟩ := Finset.exists_mem_eq_inf' (by simp : Finset.univ.Nonempty) f
-  exact ⟨i, hi.symm⟩
-
-/-- The index of the minimum value of a tuple. -/
-noncomputable def argmin := (exists_argmin f).choose
-
-lemma argmin_spec : f (argmin f) = f.min := (exists_argmin f).choose_spec
-
-lemma isMinOn_argmin (x : ι) : f (argmin f) ≤ f x := by
-  rw [argmin_spec f]
-  exact f.min_le x
-
-end Argmin
-
-lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] : -f.max = (-f).min := by
-  refine le_antisymm ?_ ?_
-  · simp; grind
-  · simp only [inf'_le_iff, mem_univ, Pi.neg_apply, neg_le_neg_iff, sup'_le_iff, forall_const,
-      true_and]
-    exact ⟨argmax f, isMaxOn_argmax f⟩
-
 variable [MeasurableSpace α]
 
-section argmax
-
 @[fun_prop]
 lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => t.max) := by
   suffices (fun f : ι → α ↦ f.max) = (univ.sup' univ_nonempty fun i f => f i) by
@@ -106,10 +82,6 @@ lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂
   · intro h
     exact h f rfl
 
-end argmax
-
-section argmin
-
 @[fun_prop]
 lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (f : ι → α) => f.min) := by
   suffices (fun f : ι → α ↦ f.min) = (univ.inf' univ_nonempty fun i f => f i) by
@@ -138,4 +110,11 @@ lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂
   · intro h
     exact h f rfl
 
-end argmin
+end Argmax
+
+lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] : -f.max = (-f).min := by
+  refine le_antisymm ?_ ?_
+  · simp; grind
+  · simp only [inf'_le_iff, mem_univ, Pi.neg_apply, neg_le_neg_iff, sup'_le_iff, forall_const,
+      true_and]
+    exact ⟨argmax f, isMaxOn_argmax f⟩

From 3c58c1efe00f781c074c10e111b581973e5e96c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Fri, 26 Jun 2026 15:09:12 +0200
Subject: [PATCH 11/16] Add pointer to `Finset.measurable_sup'`

---
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
index 7ff66f06..71605742 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
@@ -17,6 +17,7 @@ open Finset
 
 variable {δ α : Type*} [MeasurableSpace δ] [SemilatticeInf α] [MeasurableSpace α] [MeasurableInf₂ α]
 
+/-- Dual version of `Finset.measurable_sup'`. -/
 @[fun_prop]
 theorem Finset.measurable_inf' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}
     (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f) :=

From 939927c56e44f8bbf7689c523abdedd3462d30de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 21:52:51 +0200
Subject: [PATCH 12/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/Lattice.lean            | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
index 71605742..2552702e 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/Lattice.lean
@@ -15,10 +15,13 @@ public import Mathlib.MeasureTheory.Order.Lattice
 
 open Finset
 
-variable {δ α : Type*} [MeasurableSpace δ] [SemilatticeInf α] [MeasurableSpace α] [MeasurableInf₂ α]
+variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α}
+  [MeasurableInf₂ α]
+
+attribute [to_dual existing] MeasurableInf₂
 
 /-- Dual version of `Finset.measurable_sup'`. -/
-@[fun_prop]
+@[to_dual existing (attr := fun_prop)]
 theorem Finset.measurable_inf' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}
     (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f) :=
   Finset.inf'_induction hs _ (fun _f hf _g hg => hf.inf hg) fun n hn => hf n hn

From 77bb9c4446b993c5f62d04bf4762ad64541b47e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 21:52:58 +0200
Subject: [PATCH 13/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean           | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index e52fb6b8..0b952d5c 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -62,7 +62,7 @@ lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) =>
   ext
   simp [Function.max]
 
-@[fun_prop]
+@[to_dual (attr := fun_prop)]
 lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] :
     Measurable fun f : ι → α ↦ argmax f := by
   refine measurable_to_countable' fun i ↦ ?_

From 9e4a3ff46ce1f8f937802eba5b6de62158ccb4e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Fri, 26 Jun 2026 21:53:03 +0200
Subject: [PATCH 14/16] Update
 LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 .../ForMathlib/MeasureTheory/Order/MeasurableArg.lean           | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index 0b952d5c..bec0ada0 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -54,7 +54,7 @@ lemma isMaxOn_argmax (x : ι) : f x ≤ f (argmax f) := by
 
 variable [MeasurableSpace α]
 
-@[fun_prop]
+@[to_dual (attr := fun_prop)]
 lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => t.max) := by
   suffices (fun f : ι → α ↦ f.max) = (univ.sup' univ_nonempty fun i f => f i) by
     rw [this]

From 6429de73d0b06ba4f889c04b1cc0cf8a719b22f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Fri, 26 Jun 2026 21:52:12 +0200
Subject: [PATCH 15/16] Unused args

---
 LeanMachineLearning/Online/Bandit/BayesRegret.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/LeanMachineLearning/Online/Bandit/BayesRegret.lean b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
index aaa582e1..00210b41 100644
--- a/LeanMachineLearning/Online/Bandit/BayesRegret.lean
+++ b/LeanMachineLearning/Online/Bandit/BayesRegret.lean
@@ -68,13 +68,12 @@ lemma integrable_uncurry_actionMean_comp [Countable 𝓐] [MeasurableSingletonCl
 
 /-- A random variable that gives the action with the highest mean feedback. -/
 noncomputable
-def bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
-    (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 :=
+def bestAction [Nonempty 𝓐] [Fintype 𝓐] (κ : Kernel (𝓔 × 𝓐) ℝ) (E : Ω → 𝓔) (ω : Ω) : 𝓐 :=
   argmax (fun a ↦ actionMean κ E a ω)
 
 @[fun_prop]
-lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
-    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} (hE : Measurable E) : Measurable (bestAction κ E) := by
+lemma measurable_bestAction [Nonempty 𝓐] [Fintype 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔}
+    (hE : Measurable E) : Measurable (bestAction κ E) := by
   unfold bestAction
   fun_prop
 
@@ -95,9 +94,9 @@ lemma gap_le_of_mem_Icc [Nonempty 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω
   Bandits.gap_le_of_mem_Icc (h (E ω))
 
 omit [MeasurableSpace Ω] in
-lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] [Encodable 𝓐] [MeasurableSingletonClass 𝓐]
-    {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {n : ℕ} {ω : Ω} :
-    gap κ E A n ω = actionMean κ E (bestAction κ E ω) ω - actionMean κ E (A n ω) ω := by
+lemma gap_eq_sub [Nonempty 𝓐] [Fintype 𝓐] {κ : Kernel (𝓔 × 𝓐) ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐}
+    {n : ℕ} {ω : Ω} : gap κ E A n ω =
+      actionMean κ E (bestAction κ E ω) ω - actionMean κ E (A n ω) ω := by
   rw [gap, Bandits.gap]
   congr
   apply le_antisymm

From 53440ea51f96ae05ddb05cfcb8026777ef74d37f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Fri, 26 Jun 2026 22:02:06 +0200
Subject: [PATCH 16/16] fix `to_dual` naming

---
 .../MeasureTheory/Order/MeasurableArg.lean    | 30 +------------------
 1 file changed, 1 insertion(+), 29 deletions(-)

diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index bec0ada0..7c7bf9af 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -62,7 +62,7 @@ lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) =>
   ext
   simp [Function.max]
 
-@[to_dual (attr := fun_prop)]
+@[to_dual (attr := fun_prop) measurable_argmin]
 lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] :
     Measurable fun f : ι → α ↦ argmax f := by
   refine measurable_to_countable' fun i ↦ ?_
@@ -82,34 +82,6 @@ lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂
   · intro h
     exact h f rfl
 
-@[fun_prop]
-lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (f : ι → α) => f.min) := by
-  suffices (fun f : ι → α ↦ f.min) = (univ.inf' univ_nonempty fun i f => f i) by
-    rw [this]
-    exact measurable_inf' univ_nonempty (fun i _ => measurable_pi_apply i)
-  ext
-  simp [Function.min]
-
-@[fun_prop]
-lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂ α] :
-    Measurable fun f : ι → α ↦ argmin f := by
-  refine measurable_to_countable' fun i ↦ ?_
-  simp only [Set.preimage, Set.mem_singleton_iff]
-  let Minimizers (f : ι → α) : Set ι := {i | f i = f.min}
-  suffices {f : ι → α | argmin f = i} = ⋃ (S)
-      (hS : ∀ x, Minimizers x = S → argmin x = i), {f | Minimizers f = S} by
-    rw [this]
-    refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
-    exact measurableSet_eq_fun (by fun_prop) measurable_const
-  ext f
-  simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
-  constructor
-  · intro hf x hx
-    rw [← hf]
-    exact Classical.choose.congr_simp hx (exists_argmin x)
-  · intro h
-    exact h f rfl
-
 end Argmax
 
 lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] : -f.max = (-f).min := by