From 17a3eb0de1451bcbd358195d913515563f4c19b3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 12:39:54 +0200
Subject: [PATCH 01/10] Add LIPO and RankOpt algorithms

---
 .../Optimization/Algorithms/Decision.lean     |  68 ++++++++++
 .../Optimization/Algorithms/LIPO.lean         |  75 +++++++++++
 .../Optimization/Algorithms/RankOpt.lean      | 127 ++++++++++++++++++
 3 files changed, 270 insertions(+)
 create mode 100644 LeanMachineLearning/Optimization/Algorithms/Decision.lean
 create mode 100644 LeanMachineLearning/Optimization/Algorithms/LIPO.lean
 create mode 100644 LeanMachineLearning/Optimization/Algorithms/RankOpt.lean

diff --git a/LeanMachineLearning/Optimization/Algorithms/Decision.lean b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
new file mode 100644
index 00000000..fa39188d
--- /dev/null
+++ b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
@@ -0,0 +1,68 @@
+/-
+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.SequentialLearning.Algorithm
+
+/-!
+# Decision-based Optimization Algorithms
+
+An interface for decision-based optimization algorithms, which sample points satisfying a
+user-defined decision rule at each iteration. These algorithms are defined by a sequence of
+decision rules that determine from which set to sample at each iteration, based on the observed
+data. The `Decision` algorithm is a special case of the `Algorithm` structure, where the Markov
+kernel is defined through the decision rules.
+
+## Main definitions
+
+* `decision_kernel`: The Markov kernel that samples from the decision set rules according to a
+given measure `μ`.
+* `Decision`: The Decision algorithm that starts by sampling from the initial measure `μ` and then
+samples points satisfying the decision rules at each iteration using the defined kernel.
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Finset Learning
+
+variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
+  (μ : Measure α) [IsProbabilityMeasure μ] {decision : (n : ℕ) → ((Iic n) → α × β) → Set α}
+  (measurableSet_decision_prod :
+    ∀ n, MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ decision n p.1}) {n : ℕ}
+
+include measurableSet_decision_prod in
+lemma measurable_decision_inter {s : Set α} (hs : MeasurableSet s) :
+    Measurable (fun data : Iic n → α × β ↦ μ (decision n data ∩ s)) := by
+  set E := {p : (Iic n → α × β) × α | p.2 ∈ decision n p.1 ∩ s}
+  have hE_meas : MeasurableSet E :=
+    (measurableSet_decision_prod n).inter
+      <| measurableSet_preimage measurable_snd hs
+  exact measurable_measure_prodMk_left hE_meas
+
+/-- The Markov kernel that samples from the decision set according to a given
+measure `μ`. -/
+noncomputable def decision_kernel : Kernel (Iic n → α × β) α := by
+  refine ⟨fun data ↦ cond μ <| decision n data, ?_⟩
+  rw [Measure.measurable_measure]
+  intro s hs
+  simp only [ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]
+  refine Measurable.mul ?_ ?_
+  · refine Measurable.inv ?_
+    convert measurable_decision_inter μ measurableSet_decision_prod (MeasurableSet.univ)
+    simp [Set.inter_univ]
+  · simp_rw [μ.restrict_apply hs]
+    convert measurable_decision_inter μ measurableSet_decision_prod hs using 1
+    simp [Set.inter_comm]
+
+/- We need that the decisions has non-zero measure at each iteration,
+ensuring that the algorithm can sample from it. -/
+variable (h : ∀ n (data : Iic n → α × β), μ (decision n data) ≠ 0)
+
+/-- The interface for decision-based optimization algorithms. -/
+noncomputable def Decision : Algorithm α β where
+  policy _ := decision_kernel μ measurableSet_decision_prod
+  p0 := μ
+  h_policy n := ⟨fun data ↦ cond_isProbabilityMeasure (h n data)⟩
diff --git a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
new file mode 100644
index 00000000..75af6cb9
--- /dev/null
+++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
@@ -0,0 +1,75 @@
+/-
+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.Optimization.Algorithms.Decision
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
+public import LeanMachineLearning.ForMathlib.Order.Interval.Finset
+
+/-!
+# LIPO: Lipschitz Optimization
+
+Implementation of the _LIPO_ algorithm
+[(_Global optimization of Lipschitz functions_,
+Malherbe et al. 2017)](https://arxiv.org/abs/1703.02628)
+defined on a measurable space with a metric. The algorithm samples from an arbitrary
+probability measure on the set of potential maximizers of the function at each iteration.
+It is defined as a special case of the `Decision` algorithm.
+
+## Main definitions
+
+* `potential_max`: The set of potential maximizers for the LIPO algorithm.
+* `LIPO`: The LIPO algorithm that samples from the set of potential maximizers using a given
+  probability measure at each iteration.
+
+## References
+
+* [(_Global optimization of Lipschitz functions_,
+Malherbe et al. 2017)](https://arxiv.org/abs/1703.02628)
+
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Finset NNReal Learning
+
+variable {α : Type*} [PseudoMetricSpace α] [MeasurableSpace α] [BorelSpace α]
+  [SecondCountableTopology α] (μ : Measure α) [IsProbabilityMeasure μ] {n : ℕ} (κ : ℝ≥0)
+  (data : Iic n → α × ℝ)
+
+namespace LIPO
+
+/-- The set of potential maximizers for the LIPO algorithm.
+Given observed data points and function values, this set contains all points `x` where
+the maximum observed value is at most the minimum Lipschitz upper bound across all observations.
+The upper bound at `x` from observation `i` is `f(xᵢ) + κ · d(xᵢ, x)`, where `κ` is the
+Lipschitz constant. -/
+def potential_max :=
+  {x | (fun i ↦ (data i).2).max ≤ (fun i ↦ (data i).2 + κ * dist (data i).1 x).min}
+
+lemma measurableSet_potential_max_prod :
+    MeasurableSet {p : (Iic n → α × ℝ) × α | p.2 ∈ potential_max κ p.1} := by
+  unfold potential_max
+  simp only [Set.mem_ofPred_eq, measurableSet_setOfPred]
+  refine Measurable.le' ?_ ?_
+  · fun_prop
+  · fun_prop
+
+end LIPO
+
+open LIPO
+
+/- We need that the set of potential maximizers has non-zero measure at each iteration,
+ensuring that the algorithm can sample from it. -/
+variable (h : ∀ n (data : Iic n → α × ℝ), μ (potential_max κ data) ≠ 0)
+
+/-- The LIPO (LIPschitz Optimization) algorithm for global optimization.
+This algorithm optimizes an unknown function assuming only that it has a finite Lipschitz
+constant `κ`. It starts with an arbitrary probability measure `μ` as initial distribution and
+iteratively samples from the set of potential maximizers, ensuring consistency and convergence to
+the global optimum [(Malherbe et al., 2017)](https://arxiv.org/abs/1703.02628). -/
+noncomputable def LIPO : Algorithm α ℝ :=
+  Decision μ (fun _ ↦ measurableSet_potential_max_prod κ) h
diff --git a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
new file mode 100644
index 00000000..722de297
--- /dev/null
+++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
@@ -0,0 +1,127 @@
+/-
+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.Optimization.Algorithms.Decision
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
+public import LeanMachineLearning.ForMathlib.Order.Interval.Finset
+
+/-!
+# RankOpt: A Ranking Approach to Global Optimization
+
+Implementation of the _RankOpt_ algorithm
+[(_A Ranking Approach to Global Optimization_,
+Malherbe et al. 2017)](https://arxiv.org/abs/1603.04381)
+defined on a measurable space. The algorithm samples from an arbitrary probability measure
+on the set of potential maximizers of the function at each iteration. It is defined as a special
+case of the `Decision` algorithm.
+
+## Main definitions
+
+* `RankRule`: A rank rule is a measurable function that compares pairs of points.
+  It returns 1 if the first point is ranked higher, -1 if lower, and 0 if equal.
+* `potential_max`: The set of potential maximizers for the RankOpt algorithm.
+* `RankOpt`: The RankOpt algorithm that samples from the set of potential maximizers using a given
+  probability measure at each iteration.
+
+## References
+
+* [(_A Ranking Approach to Global Optimization_,
+Malherbe et al. 2017)](https://arxiv.org/abs/1603.04381)
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Finset NNReal Learning
+
+section RankRule
+
+/-- A rank rule is a measurable function that compares pairs of points.
+It returns 1 if the first point is ranked higher, -1 if lower, and 0 if equal. -/
+def RankRule (α : Type*) [MeasurableSpace α] :=
+  {f : α → α → ({-1, 0, 1} : Set ℝ) // Measurable <| Function.uncurry f}
+
+end RankRule
+
+variable {α β : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ] {n : ℕ}
+  [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β]
+  [SecondCountableTopology β] [OpensMeasurableSpace β] [OrderClosedTopology β]
+  (data : Iic n → α × β)
+
+namespace RankOpt
+
+/-- Computes the ranking from observed function values.
+Returns 1 if `y₁ > y₂`, 0 if `y₁ = y₂`, and -1 if `y₁ < y₂`. -/
+noncomputable def ranking_data (y₁ y₂ : β) := if y₂ < y₁ then 1 else if y₂ = y₁ then 0 else -1
+
+/-- Indicator function checking if two rankings agree.
+Returns 1 if both values are equal, 0 otherwise. -/
+noncomputable abbrev rindicator (r₁ r₂ : ℝ) := if r₁ = r₂ then (1 : ℝ) else 0
+
+/-- Computes the ranking loss for a rank rule.
+Measures the agreement between a candidate rule `r` and the rankings induced by the observed
+function values on all pairs of data points, normalized by the number of pairs. -/
+noncomputable def ranking_loss (r : RankRule α) :=
+  2 * (n * (n + 1) : ℝ)⁻¹ * ∑ ij ∈ {(i, j) : Iic n × Iic n | i ≤ j},
+    rindicator (r.1 (data ij.1).1 (data ij.2).1) (ranking_data (data ij.1).2 (data ij.2).2)
+
+/-- The point in the observed data with the maximum function value. -/
+noncomputable abbrev argmax_f := (data <| argmax (fun i ↦ (data i).2)).1
+
+/-- The set of potential maximizers for the RankOpt algorithm.
+Contains all points `x` for which there exists a ranking rule `r` in the hypothesis class `𝓡`
+that: (1) has zero ranking loss (perfectly consistent with the observed data),
+and (2) ranks `x` at least as high as the current best observed point. -/
+def potential_max (𝓡 : Set (RankRule α)) :=
+    {x | ∃ (r : 𝓡), ranking_loss data r = 0 ∧ 0 ≤ (r.1.1 x (argmax_f data)).1}
+
+lemma measurableSet_potential_max_prod {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable) :
+    MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ potential_max p.1 𝓡} := by
+  simp only [potential_max, Set.mem_ofPred_eq, measurableSet_setOfPred]
+  have : Countable (𝓡) := h𝓡.to_subtype
+  refine Measurable.exists fun r ↦ (.and ?_ ?_)
+  · simp only [ranking_loss]
+    refine Measurable.eq ?_ measurable_const
+    refine Measurable.const_mul (measurable_sum _ fun i hi ↦ ?_) _
+    simp only [rindicator]
+    refine Measurable.ite (measurableSet_eq_fun ?_ ?_) measurable_const measurable_const
+    · have := r.1.2
+      fun_prop
+    · simp only [ranking_data]
+      have : Measurable (fun (z : ℤ) ↦ (z : ℝ)) := by fun_prop
+      refine this.comp ?_
+      refine Measurable.ite ?_ measurable_const <| .ite ?_ measurable_const measurable_const
+      · measurability
+      · measurability
+  · refine Measurable.le' measurable_const ?_
+    have : Measurable (fun x : ({-1, 0, 1} : Set ℝ) ↦ (x : ℝ)) := by fun_prop
+    refine this.comp (r.1.2.comp (measurable_snd.prodMk ?_))
+    suffices Measurable (fun p : Iic n → α × β ↦ (p <| argmax (fun i ↦ (p i).2)).1) by
+      exact this.comp measurable_fst
+    have h_eval : Measurable (fun p : (Iic n → α × β) × Iic n ↦ (p.1 p.2).1) := by
+      suffices Measurable (fun p : (Iic n → α × β) × Iic n ↦ p.1 p.2) by
+        fun_prop
+      exact measurable_from_prod_countable_left fun i ↦ measurable_pi_apply i
+    refine h_eval.comp (Measurable.prodMk (by fun_prop) ?_)
+    change Measurable (fun p : Iic n → α × β ↦ argmax (fun i ↦ (p i).2))
+    fun_prop
+
+end RankOpt
+
+open RankOpt
+
+/- We need that the set of potential maximizers has non-zero measure at each iteration,
+ensuring that the algorithm can sample from it. -/
+variable {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable)
+  (h : ∀ n (data : Iic n → α × β), μ (potential_max data 𝓡) ≠ 0)
+
+/-- The RankOpt algorithm for global optimization.
+This algorithm uses a ranking approach to optimize an unknown function. It maintains a hypothesis
+class `𝓡` of ranking rules. It starts with an arbitrary probability measure `μ` as initial
+distribution and samples from the set of points that could be optimal according to ranking rules
+consistent with the observed data [(Malherbe et al., 2017)](https://arxiv.org/abs/1603.04381). -/
+noncomputable def RankOpt : Algorithm α β :=
+  Decision μ (fun n ↦ measurableSet_potential_max_prod (n := n) h𝓡) h

From e36d4b52cc9a09f2d8c1bba41a570f309ad08fb3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 12:41:39 +0200
Subject: [PATCH 02/10] Implicit args

---
 LeanMachineLearning/Optimization/Algorithms/LIPO.lean    | 2 +-
 LeanMachineLearning/Optimization/Algorithms/RankOpt.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
index 75af6cb9..53a4c2e4 100644
--- a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
@@ -64,7 +64,7 @@ open LIPO
 
 /- We need that the set of potential maximizers has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
-variable (h : ∀ n (data : Iic n → α × ℝ), μ (potential_max κ data) ≠ 0)
+variable (h : ∀ ⦃n⦄ ⦃data : Iic n → α × ℝ⦄, μ (potential_max κ data) ≠ 0)
 
 /-- The LIPO (LIPschitz Optimization) algorithm for global optimization.
 This algorithm optimizes an unknown function assuming only that it has a finite Lipschitz
diff --git a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
index 722de297..649ddfe4 100644
--- a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
@@ -116,7 +116,7 @@ open RankOpt
 /- We need that the set of potential maximizers has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
 variable {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable)
-  (h : ∀ n (data : Iic n → α × β), μ (potential_max data 𝓡) ≠ 0)
+  (h : ∀ ⦃n⦄ ⦃data : Iic n → α × β⦄, μ (potential_max data 𝓡) ≠ 0)
 
 /-- The RankOpt algorithm for global optimization.
 This algorithm uses a ranking approach to optimize an unknown function. It maintains a hypothesis

From 4b40e0aafe7f0d13631fab127b7510cd871d3908 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 12:43:58 +0200
Subject: [PATCH 03/10] Update `LeanMachineLearning.lean`

---
 LeanMachineLearning.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 9bc9ac39..2d466972 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -29,6 +29,9 @@ public import LeanMachineLearning.Online.Bandit.BayesRegret
 public import LeanMachineLearning.Online.Bandit.Regret
 public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
 public import LeanMachineLearning.Online.Bandit.SumRewards
+public import LeanMachineLearning.Optimization.Algorithms.Decision
+public import LeanMachineLearning.Optimization.Algorithms.LIPO
+public import LeanMachineLearning.Optimization.Algorithms.RankOpt
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes

From 5d0167ad45b2f378d7b74d7fdb7d6fa9db7f471d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 12:48:00 +0200
Subject: [PATCH 04/10] Better syntax for decision kernel

---
 .../Optimization/Algorithms/Decision.lean     | 25 ++++++++++---------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/LeanMachineLearning/Optimization/Algorithms/Decision.lean b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
index fa39188d..e1193a83 100644
--- a/LeanMachineLearning/Optimization/Algorithms/Decision.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
@@ -44,18 +44,19 @@ lemma measurable_decision_inter {s : Set α} (hs : MeasurableSet s) :
 
 /-- The Markov kernel that samples from the decision set according to a given
 measure `μ`. -/
-noncomputable def decision_kernel : Kernel (Iic n → α × β) α := by
-  refine ⟨fun data ↦ cond μ <| decision n data, ?_⟩
-  rw [Measure.measurable_measure]
-  intro s hs
-  simp only [ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]
-  refine Measurable.mul ?_ ?_
-  · refine Measurable.inv ?_
-    convert measurable_decision_inter μ measurableSet_decision_prod (MeasurableSet.univ)
-    simp [Set.inter_univ]
-  · simp_rw [μ.restrict_apply hs]
-    convert measurable_decision_inter μ measurableSet_decision_prod hs using 1
-    simp [Set.inter_comm]
+noncomputable def decision_kernel : Kernel (Iic n → α × β) α where
+  toFun data := cond μ <| decision n data
+  measurable' := by
+    rw [Measure.measurable_measure]
+    intro s hs
+    simp only [ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]
+    refine Measurable.mul ?_ ?_
+    · refine Measurable.inv ?_
+      convert measurable_decision_inter μ measurableSet_decision_prod (MeasurableSet.univ)
+      simp [Set.inter_univ]
+    · simp_rw [μ.restrict_apply hs]
+      convert measurable_decision_inter μ measurableSet_decision_prod hs using 1
+      simp [Set.inter_comm]
 
 /- We need that the decisions has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/

From 3d72bb7385c7c3b3f9037c3d1c33d610820c3d8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 12:58:29 +0200
Subject: [PATCH 05/10] Linter

---
 .../Optimization/Algorithms/Decision.lean     |  6 ++--
 .../Optimization/Algorithms/LIPO.lean         | 14 +++++-----
 .../Optimization/Algorithms/RankOpt.lean      | 28 +++++++++----------
 3 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/LeanMachineLearning/Optimization/Algorithms/Decision.lean b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
index e1193a83..f92e3f68 100644
--- a/LeanMachineLearning/Optimization/Algorithms/Decision.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
@@ -18,7 +18,7 @@ kernel is defined through the decision rules.
 
 ## Main definitions
 
-* `decision_kernel`: The Markov kernel that samples from the decision set rules according to a
+* `decisionKernel`: The Markov kernel that samples from the decision set rules according to a
 given measure `μ`.
 * `Decision`: The Decision algorithm that starts by sampling from the initial measure `μ` and then
 samples points satisfying the decision rules at each iteration using the defined kernel.
@@ -44,7 +44,7 @@ lemma measurable_decision_inter {s : Set α} (hs : MeasurableSet s) :
 
 /-- The Markov kernel that samples from the decision set according to a given
 measure `μ`. -/
-noncomputable def decision_kernel : Kernel (Iic n → α × β) α where
+noncomputable def decisionKernel : Kernel (Iic n → α × β) α where
   toFun data := cond μ <| decision n data
   measurable' := by
     rw [Measure.measurable_measure]
@@ -64,6 +64,6 @@ variable (h : ∀ n (data : Iic n → α × β), μ (decision n data) ≠ 0)
 
 /-- The interface for decision-based optimization algorithms. -/
 noncomputable def Decision : Algorithm α β where
-  policy _ := decision_kernel μ measurableSet_decision_prod
+  policy _ := decisionKernel μ measurableSet_decision_prod
   p0 := μ
   h_policy n := ⟨fun data ↦ cond_isProbabilityMeasure (h n data)⟩
diff --git a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
index 53a4c2e4..e987f3e2 100644
--- a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
@@ -21,7 +21,7 @@ It is defined as a special case of the `Decision` algorithm.
 
 ## Main definitions
 
-* `potential_max`: The set of potential maximizers for the LIPO algorithm.
+* `potentialMax`: The set of potential maximizers for the LIPO algorithm.
 * `LIPO`: The LIPO algorithm that samples from the set of potential maximizers using a given
   probability measure at each iteration.
 
@@ -47,12 +47,12 @@ Given observed data points and function values, this set contains all points `x`
 the maximum observed value is at most the minimum Lipschitz upper bound across all observations.
 The upper bound at `x` from observation `i` is `f(xᵢ) + κ · d(xᵢ, x)`, where `κ` is the
 Lipschitz constant. -/
-def potential_max :=
+def potentialMax :=
   {x | (fun i ↦ (data i).2).max ≤ (fun i ↦ (data i).2 + κ * dist (data i).1 x).min}
 
-lemma measurableSet_potential_max_prod :
-    MeasurableSet {p : (Iic n → α × ℝ) × α | p.2 ∈ potential_max κ p.1} := by
-  unfold potential_max
+lemma measurableSetPotentialMaxProd :
+    MeasurableSet {p : (Iic n → α × ℝ) × α | p.2 ∈ potentialMax κ p.1} := by
+  unfold potentialMax
   simp only [Set.mem_ofPred_eq, measurableSet_setOfPred]
   refine Measurable.le' ?_ ?_
   · fun_prop
@@ -64,7 +64,7 @@ open LIPO
 
 /- We need that the set of potential maximizers has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
-variable (h : ∀ ⦃n⦄ ⦃data : Iic n → α × ℝ⦄, μ (potential_max κ data) ≠ 0)
+variable (h : ∀ ⦃n⦄ ⦃data : Iic n → α × ℝ⦄, μ (potentialMax κ data) ≠ 0)
 
 /-- The LIPO (LIPschitz Optimization) algorithm for global optimization.
 This algorithm optimizes an unknown function assuming only that it has a finite Lipschitz
@@ -72,4 +72,4 @@ constant `κ`. It starts with an arbitrary probability measure `μ` as initial d
 iteratively samples from the set of potential maximizers, ensuring consistency and convergence to
 the global optimum [(Malherbe et al., 2017)](https://arxiv.org/abs/1703.02628). -/
 noncomputable def LIPO : Algorithm α ℝ :=
-  Decision μ (fun _ ↦ measurableSet_potential_max_prod κ) h
+  Decision μ (fun _ ↦ measurableSetPotentialMaxProd κ) h
diff --git a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
index 649ddfe4..78abb6e5 100644
--- a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
@@ -23,7 +23,7 @@ case of the `Decision` algorithm.
 
 * `RankRule`: A rank rule is a measurable function that compares pairs of points.
   It returns 1 if the first point is ranked higher, -1 if lower, and 0 if equal.
-* `potential_max`: The set of potential maximizers for the RankOpt algorithm.
+* `potentialMax`: The set of potential maximizers for the RankOpt algorithm.
 * `RankOpt`: The RankOpt algorithm that samples from the set of potential maximizers using a given
   probability measure at each iteration.
 
@@ -55,42 +55,42 @@ namespace RankOpt
 
 /-- Computes the ranking from observed function values.
 Returns 1 if `y₁ > y₂`, 0 if `y₁ = y₂`, and -1 if `y₁ < y₂`. -/
-noncomputable def ranking_data (y₁ y₂ : β) := if y₂ < y₁ then 1 else if y₂ = y₁ then 0 else -1
+noncomputable def rankingData (y₁ y₂ : β) := if y₂ < y₁ then 1 else if y₂ = y₁ then 0 else -1
 
 /-- Indicator function checking if two rankings agree.
 Returns 1 if both values are equal, 0 otherwise. -/
-noncomputable abbrev rindicator (r₁ r₂ : ℝ) := if r₁ = r₂ then (1 : ℝ) else 0
+noncomputable abbrev rIndicator (r₁ r₂ : ℝ) := if r₁ = r₂ then (1 : ℝ) else 0
 
 /-- Computes the ranking loss for a rank rule.
 Measures the agreement between a candidate rule `r` and the rankings induced by the observed
 function values on all pairs of data points, normalized by the number of pairs. -/
-noncomputable def ranking_loss (r : RankRule α) :=
+noncomputable def rankingLoss (r : RankRule α) :=
   2 * (n * (n + 1) : ℝ)⁻¹ * ∑ ij ∈ {(i, j) : Iic n × Iic n | i ≤ j},
-    rindicator (r.1 (data ij.1).1 (data ij.2).1) (ranking_data (data ij.1).2 (data ij.2).2)
+    rIndicator (r.1 (data ij.1).1 (data ij.2).1) (rankingData (data ij.1).2 (data ij.2).2)
 
 /-- The point in the observed data with the maximum function value. -/
-noncomputable abbrev argmax_f := (data <| argmax (fun i ↦ (data i).2)).1
+noncomputable abbrev argmaxF := (data <| argmax (fun i ↦ (data i).2)).1
 
 /-- The set of potential maximizers for the RankOpt algorithm.
 Contains all points `x` for which there exists a ranking rule `r` in the hypothesis class `𝓡`
 that: (1) has zero ranking loss (perfectly consistent with the observed data),
 and (2) ranks `x` at least as high as the current best observed point. -/
-def potential_max (𝓡 : Set (RankRule α)) :=
-    {x | ∃ (r : 𝓡), ranking_loss data r = 0 ∧ 0 ≤ (r.1.1 x (argmax_f data)).1}
+def potentialMax (𝓡 : Set (RankRule α)) :=
+    {x | ∃ (r : 𝓡), rankingLoss data r = 0 ∧ 0 ≤ (r.1.1 x (argmaxF data)).1}
 
 lemma measurableSet_potential_max_prod {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable) :
-    MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ potential_max p.1 𝓡} := by
-  simp only [potential_max, Set.mem_ofPred_eq, measurableSet_setOfPred]
+    MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ potentialMax p.1 𝓡} := by
+  simp only [potentialMax, Set.mem_ofPred_eq, measurableSet_setOfPred]
   have : Countable (𝓡) := h𝓡.to_subtype
   refine Measurable.exists fun r ↦ (.and ?_ ?_)
-  · simp only [ranking_loss]
+  · simp only [rankingLoss]
     refine Measurable.eq ?_ measurable_const
     refine Measurable.const_mul (measurable_sum _ fun i hi ↦ ?_) _
-    simp only [rindicator]
+    simp only [rIndicator]
     refine Measurable.ite (measurableSet_eq_fun ?_ ?_) measurable_const measurable_const
     · have := r.1.2
       fun_prop
-    · simp only [ranking_data]
+    · simp only [rankingData]
       have : Measurable (fun (z : ℤ) ↦ (z : ℝ)) := by fun_prop
       refine this.comp ?_
       refine Measurable.ite ?_ measurable_const <| .ite ?_ measurable_const measurable_const
@@ -116,7 +116,7 @@ open RankOpt
 /- We need that the set of potential maximizers has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
 variable {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable)
-  (h : ∀ ⦃n⦄ ⦃data : Iic n → α × β⦄, μ (potential_max data 𝓡) ≠ 0)
+  (h : ∀ ⦃n⦄ ⦃data : Iic n → α × β⦄, μ (potentialMax data 𝓡) ≠ 0)
 
 /-- The RankOpt algorithm for global optimization.
 This algorithm uses a ranking approach to optimize an unknown function. It maintains a hypothesis

From bfdfcdb72b93f48c859f6b1d249fbf00c577f7ad Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 18:20:45 +0200
Subject: [PATCH 06/10] Add `Kernel.cond`

---
 .../ForMathlib/Probability/Kernel/Cond.lean   | 65 +++++++++++++++++++
 .../Optimization/Algorithms/Decision.lean     | 41 +++---------
 .../Optimization/Algorithms/LIPO.lean         | 10 +--
 .../Optimization/Algorithms/RankOpt.lean      | 19 +++---
 4 files changed, 91 insertions(+), 44 deletions(-)
 create mode 100644 LeanMachineLearning/ForMathlib/Probability/Kernel/Cond.lean

diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/Cond.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/Cond.lean
new file mode 100644
index 00000000..891d9051
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/Cond.lean
@@ -0,0 +1,65 @@
+/-
+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
+
+/-! # Definition of conditional Markov kernels
+-/
+
+@[expose] public section
+
+open MeasureTheory
+
+namespace ProbabilityTheory.Kernel
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+  {κ : Kernel α β} {A : α → Set β}
+
+/-- If the graph `{p | p.2 ∈ A p.1}` of the set-valued map `A` is measurable, then
+`x ↦ κ x (s ∩ A x)` is measurable for every measurable set `s`. -/
+lemma measurable_apply_inter [IsSFiniteKernel κ]
+    (hA : MeasurableSet {p : α × β | p.2 ∈ A p.1}) {s : Set β} (hs : MeasurableSet s) :
+    Measurable fun x ↦ κ x (s ∩ A x) := by
+  have h (x : α) : s ∩ A x = Prod.mk x ⁻¹' (Prod.snd ⁻¹' s ∩ {p : α × β | p.2 ∈ A p.1}) := rfl
+  simp_rw [h]
+  exact measurable_kernel_prodMk_left <| (measurable_snd hs).inter hA
+
+variable (κ) [IsSFiniteKernel κ]
+
+/-- The kernel `x ↦ (κ x)[|A x]`, obtained by conditioning `κ x` on the set `A x`. -/
+noncomputable def cond (hA : MeasurableSet {p : α × β | p.2 ∈ A p.1}) : Kernel α β where
+  toFun x := (κ x)[|A x]
+  measurable' := by
+    rw [Measure.measurable_measure]
+    intro t ht
+    simp only [ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]
+    refine Measurable.mul (.inv ?_) ?_
+    · simpa using measurable_apply_inter hA MeasurableSet.univ
+    · simp_rw [fun b ↦ (κ b).restrict_apply (s := A b) ht]
+      exact measurable_apply_inter hA ht
+
+variable {hA : MeasurableSet {p : α × β | p.2 ∈ A p.1}}
+
+@[simp]
+lemma cond_apply (x : α) : cond κ hA x = (κ x)[|A x] := rfl
+
+/-- `cond κ hA` is always a finite kernel, bounded by `1`: each `(κ x)[|A x]` is either the zero
+measure (when `κ x (A x)` is `0` or `∞`) or a probability measure. -/
+instance : IsFiniteKernel (cond κ hA) :=
+  ⟨1, ENNReal.one_lt_top, fun x ↦ by rw [cond_apply]; exact prob_le_one⟩
+
+/-- `cond κ hA` is a Markov kernel as soon as every `A x` has positive and finite measure
+under `κ x`. -/
+lemma isMarkovKernel_cond_of_finite (h₀ : ∀ x, κ x (A x) ≠ 0) (htop : ∀ x, κ x (A x) ≠ ⊤) :
+    IsMarkovKernel (cond κ hA) :=
+  ⟨fun x ↦ cond_isProbabilityMeasure_of_finite (h₀ x) (htop x)⟩
+
+lemma isMarkovKernel_cond [IsFiniteKernel κ] (h₀ : ∀ x, κ x (A x) ≠ 0) :
+    IsMarkovKernel (cond κ hA) :=
+  isMarkovKernel_cond_of_finite κ h₀ fun x ↦ measure_ne_top (κ x) (A x)
+
+end ProbabilityTheory.Kernel
diff --git a/LeanMachineLearning/Optimization/Algorithms/Decision.lean b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
index f92e3f68..7c98fed0 100644
--- a/LeanMachineLearning/Optimization/Algorithms/Decision.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/Decision.lean
@@ -6,6 +6,7 @@ Authors: Gaëtan Serré
 module
 
 public import LeanMachineLearning.SequentialLearning.Algorithm
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Cond
 
 /-!
 # Decision-based Optimization Algorithms
@@ -18,8 +19,6 @@ kernel is defined through the decision rules.
 
 ## Main definitions
 
-* `decisionKernel`: The Markov kernel that samples from the decision set rules according to a
-given measure `μ`.
 * `Decision`: The Decision algorithm that starts by sampling from the initial measure `μ` and then
 samples points satisfying the decision rules at each iteration using the defined kernel.
 -/
@@ -29,41 +28,19 @@ samples points satisfying the decision rules at each iteration using the defined
 open MeasureTheory ProbabilityTheory Finset Learning
 
 variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
-  (μ : Measure α) [IsProbabilityMeasure μ] {decision : (n : ℕ) → ((Iic n) → α × β) → Set α}
+  (μ : Measure α) [IsProbabilityMeasure μ]
+  (κs : (n : ℕ) → Kernel ((Iic n) → α × β) α) [∀ n, IsSFiniteKernel (κs n)]
+  {decision : (n : ℕ) → ((Iic n) → α × β) → Set α}
   (measurableSet_decision_prod :
-    ∀ n, MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ decision n p.1}) {n : ℕ}
-
-include measurableSet_decision_prod in
-lemma measurable_decision_inter {s : Set α} (hs : MeasurableSet s) :
-    Measurable (fun data : Iic n → α × β ↦ μ (decision n data ∩ s)) := by
-  set E := {p : (Iic n → α × β) × α | p.2 ∈ decision n p.1 ∩ s}
-  have hE_meas : MeasurableSet E :=
-    (measurableSet_decision_prod n).inter
-      <| measurableSet_preimage measurable_snd hs
-  exact measurable_measure_prodMk_left hE_meas
-
-/-- The Markov kernel that samples from the decision set according to a given
-measure `μ`. -/
-noncomputable def decisionKernel : Kernel (Iic n → α × β) α where
-  toFun data := cond μ <| decision n data
-  measurable' := by
-    rw [Measure.measurable_measure]
-    intro s hs
-    simp only [ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]
-    refine Measurable.mul ?_ ?_
-    · refine Measurable.inv ?_
-      convert measurable_decision_inter μ measurableSet_decision_prod (MeasurableSet.univ)
-      simp [Set.inter_univ]
-    · simp_rw [μ.restrict_apply hs]
-      convert measurable_decision_inter μ measurableSet_decision_prod hs using 1
-      simp [Set.inter_comm]
+    ∀ ⦃n⦄, MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ decision n p.1}) {n : ℕ}
 
 /- We need that the decisions has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
-variable (h : ∀ n (data : Iic n → α × β), μ (decision n data) ≠ 0)
+variable (h₀ : ∀ n (data : Iic n → α × β), κs n data (decision n data) ≠ 0)
+  (htop : ∀ n (data : Iic n → α × β), κs n data (decision n data) ≠ ⊤)
 
 /-- The interface for decision-based optimization algorithms. -/
 noncomputable def Decision : Algorithm α β where
-  policy _ := decisionKernel μ measurableSet_decision_prod
+  policy n := (κs n).cond <| measurableSet_decision_prod (n := n)
   p0 := μ
-  h_policy n := ⟨fun data ↦ cond_isProbabilityMeasure (h n data)⟩
+  h_policy n := Kernel.isMarkovKernel_cond_of_finite _ (h₀ n) (htop n)
diff --git a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
index e987f3e2..b159c1b0 100644
--- a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
@@ -50,7 +50,7 @@ Lipschitz constant. -/
 def potentialMax :=
   {x | (fun i ↦ (data i).2).max ≤ (fun i ↦ (data i).2 + κ * dist (data i).1 x).min}
 
-lemma measurableSetPotentialMaxProd :
+lemma measurableSetPotentialMaxProd (n : ℕ) :
     MeasurableSet {p : (Iic n → α × ℝ) × α | p.2 ∈ potentialMax κ p.1} := by
   unfold potentialMax
   simp only [Set.mem_ofPred_eq, measurableSet_setOfPred]
@@ -64,12 +64,14 @@ open LIPO
 
 /- We need that the set of potential maximizers has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
-variable (h : ∀ ⦃n⦄ ⦃data : Iic n → α × ℝ⦄, μ (potentialMax κ data) ≠ 0)
+variable (h₀ : ∀ n (data : Iic n → α × ℝ), μ (potentialMax κ data) ≠ 0)
 
 /-- The LIPO (LIPschitz Optimization) algorithm for global optimization.
 This algorithm optimizes an unknown function assuming only that it has a finite Lipschitz
 constant `κ`. It starts with an arbitrary probability measure `μ` as initial distribution and
 iteratively samples from the set of potential maximizers, ensuring consistency and convergence to
 the global optimum [(Malherbe et al., 2017)](https://arxiv.org/abs/1703.02628). -/
-noncomputable def LIPO : Algorithm α ℝ :=
-  Decision μ (fun _ ↦ measurableSetPotentialMaxProd κ) h
+noncomputable def LIPO : Algorithm α ℝ := by
+  refine Decision μ (fun n↦ Kernel.const _ μ) (measurableSetPotentialMaxProd κ) ?_ ?_
+  · simp [h₀]
+  · simp
diff --git a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
index 78abb6e5..d42adad6 100644
--- a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
@@ -49,7 +49,7 @@ end RankRule
 variable {α β : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ] {n : ℕ}
   [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder β]
   [SecondCountableTopology β] [OpensMeasurableSpace β] [OrderClosedTopology β]
-  (data : Iic n → α × β)
+  (𝓡 : Set (RankRule α)) (data : Iic n → α × β)
 
 namespace RankOpt
 
@@ -75,11 +75,13 @@ noncomputable abbrev argmaxF := (data <| argmax (fun i ↦ (data i).2)).1
 Contains all points `x` for which there exists a ranking rule `r` in the hypothesis class `𝓡`
 that: (1) has zero ranking loss (perfectly consistent with the observed data),
 and (2) ranks `x` at least as high as the current best observed point. -/
-def potentialMax (𝓡 : Set (RankRule α)) :=
+def potentialMax :=
     {x | ∃ (r : 𝓡), rankingLoss data r = 0 ∧ 0 ≤ (r.1.1 x (argmaxF data)).1}
 
-lemma measurableSet_potential_max_prod {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable) :
-    MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ potentialMax p.1 𝓡} := by
+variable {𝓡}
+
+lemma measurableSet_potential_max_prod (h𝓡 : 𝓡.Countable) (n : ℕ) :
+    MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ potentialMax 𝓡 p.1} := by
   simp only [potentialMax, Set.mem_ofPred_eq, measurableSet_setOfPred]
   have : Countable (𝓡) := h𝓡.to_subtype
   refine Measurable.exists fun r ↦ (.and ?_ ?_)
@@ -115,13 +117,14 @@ open RankOpt
 
 /- We need that the set of potential maximizers has non-zero measure at each iteration,
 ensuring that the algorithm can sample from it. -/
-variable {𝓡 : Set (RankRule α)} (h𝓡 : 𝓡.Countable)
-  (h : ∀ ⦃n⦄ ⦃data : Iic n → α × β⦄, μ (potentialMax data 𝓡) ≠ 0)
+variable {𝓡} (h𝓡 : 𝓡.Countable) (h₀ : ∀ ⦃n⦄ ⦃data : Iic n → α × β⦄, μ (potentialMax 𝓡 data) ≠ 0)
 
 /-- The RankOpt algorithm for global optimization.
 This algorithm uses a ranking approach to optimize an unknown function. It maintains a hypothesis
 class `𝓡` of ranking rules. It starts with an arbitrary probability measure `μ` as initial
 distribution and samples from the set of points that could be optimal according to ranking rules
 consistent with the observed data [(Malherbe et al., 2017)](https://arxiv.org/abs/1603.04381). -/
-noncomputable def RankOpt : Algorithm α β :=
-  Decision μ (fun n ↦ measurableSet_potential_max_prod (n := n) h𝓡) h
+noncomputable def RankOpt : Algorithm α β := by
+  refine Decision μ (fun n↦ Kernel.const _ μ) (measurableSet_potential_max_prod h𝓡) ?_ ?_
+  · simp [h₀]
+  · simp

From 12269419121f457983cd6ccb3157ecc21ed3cda4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Thu, 20 Aug 2026 18:36:56 +0200
Subject: [PATCH 07/10] Update LeanMachineLearning.lean

---
 LeanMachineLearning.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 2d466972..7029d861 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -15,6 +15,7 @@ public import LeanMachineLearning.ForMathlib.Probability.Integrable
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Basic
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MeasureCompProd
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Cond
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian

From 7b4f1a96cb829328b3d584333d13bd33e904c8ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Mon, 24 Aug 2026 15:59:18 +0200
Subject: [PATCH 08/10] Update
 LeanMachineLearning/Optimization/Algorithms/RankOpt.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>
---
 LeanMachineLearning/Optimization/Algorithms/RankOpt.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
index d42adad6..d2c8f976 100644
--- a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
@@ -125,6 +125,6 @@ class `𝓡` of ranking rules. It starts with an arbitrary probability measure `
 distribution and samples from the set of points that could be optimal according to ranking rules
 consistent with the observed data [(Malherbe et al., 2017)](https://arxiv.org/abs/1603.04381). -/
 noncomputable def RankOpt : Algorithm α β := by
-  refine Decision μ (fun n↦ Kernel.const _ μ) (measurableSet_potential_max_prod h𝓡) ?_ ?_
+  refine Decision μ (fun n ↦ Kernel.const _ μ) (measurableSet_potential_max_prod h𝓡) ?_ ?_
   · simp [h₀]
   · simp

From 3d24b716d5eb861e90f368d8a63ef838e7dda773 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <56162277+gaetanserre@users.noreply.github.com>
Date: Mon, 24 Aug 2026 16:01:25 +0200
Subject: [PATCH 09/10] Update
 LeanMachineLearning/Optimization/Algorithms/LIPO.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>
---
 LeanMachineLearning/Optimization/Algorithms/LIPO.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
index b159c1b0..01ccdf3d 100644
--- a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
@@ -50,7 +50,7 @@ Lipschitz constant. -/
 def potentialMax :=
   {x | (fun i ↦ (data i).2).max ≤ (fun i ↦ (data i).2 + κ * dist (data i).1 x).min}
 
-lemma measurableSetPotentialMaxProd (n : ℕ) :
+lemma measurableSet_potentialMax_prod (n : ℕ) :
     MeasurableSet {p : (Iic n → α × ℝ) × α | p.2 ∈ potentialMax κ p.1} := by
   unfold potentialMax
   simp only [Set.mem_ofPred_eq, measurableSet_setOfPred]

From bd1ae3096c2eba3e8902bb9a4066ce0437e91d02 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?=
 <gaetan.serre@ens-paris-saclay.fr>
Date: Mon, 24 Aug 2026 16:02:26 +0200
Subject: [PATCH 10/10] `measurableSet_potentialMax_prod`

---
 LeanMachineLearning/Optimization/Algorithms/LIPO.lean    | 2 +-
 LeanMachineLearning/Optimization/Algorithms/RankOpt.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
index 01ccdf3d..aa229b33 100644
--- a/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean
@@ -72,6 +72,6 @@ constant `κ`. It starts with an arbitrary probability measure `μ` as initial d
 iteratively samples from the set of potential maximizers, ensuring consistency and convergence to
 the global optimum [(Malherbe et al., 2017)](https://arxiv.org/abs/1703.02628). -/
 noncomputable def LIPO : Algorithm α ℝ := by
-  refine Decision μ (fun n↦ Kernel.const _ μ) (measurableSetPotentialMaxProd κ) ?_ ?_
+  refine Decision μ (fun n↦ Kernel.const _ μ) (measurableSet_potentialMax_prod κ) ?_ ?_
   · simp [h₀]
   · simp
diff --git a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
index d2c8f976..d26de5d5 100644
--- a/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
+++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean
@@ -80,7 +80,7 @@ def potentialMax :=
 
 variable {𝓡}
 
-lemma measurableSet_potential_max_prod (h𝓡 : 𝓡.Countable) (n : ℕ) :
+lemma measurableSet_potentialMax_prod (h𝓡 : 𝓡.Countable) (n : ℕ) :
     MeasurableSet {p : (Iic n → α × β) × α | p.2 ∈ potentialMax 𝓡 p.1} := by
   simp only [potentialMax, Set.mem_ofPred_eq, measurableSet_setOfPred]
   have : Countable (𝓡) := h𝓡.to_subtype
@@ -125,6 +125,6 @@ class `𝓡` of ranking rules. It starts with an arbitrary probability measure `
 distribution and samples from the set of points that could be optimal according to ranking rules
 consistent with the observed data [(Malherbe et al., 2017)](https://arxiv.org/abs/1603.04381). -/
 noncomputable def RankOpt : Algorithm α β := by
-  refine Decision μ (fun n ↦ Kernel.const _ μ) (measurableSet_potential_max_prod h𝓡) ?_ ?_
+  refine Decision μ (fun n ↦ Kernel.const _ μ) (measurableSet_potentialMax_prod h𝓡) ?_ ?_
   · simp [h₀]
   · simp