Add the LIPO and RankOpt global optimization algorithms

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
@@ -29,6 +30,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

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

LeanMachineLearning/Optimization/Algorithms/Decision.lean

@@ -0,0 +1,46 @@
+/-
+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
+public import LeanMachineLearning.ForMathlib.Probability.Kernel.Cond
+
+/-!
+# 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`: 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 μ]
+  (κ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 : ℕ}
+
+/- 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 → α × β), κ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 n := (κs n).cond <| measurableSet_decision_prod (n := n)
+  p0 := μ
+  h_policy n := Kernel.isMarkovKernel_cond_of_finite _ (h₀ n) (htop n)

LeanMachineLearning/Optimization/Algorithms/LIPO.lean

@@ -0,0 +1,77 @@
+/-
+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
+
+* `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.
+
+## 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 potentialMax :=
+  {x | (fun i ↦ (data i).2).max ≤ (fun i ↦ (data i).2 + κ * dist (data i).1 x).min}
+
+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]
+  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 → α × ℝ), μ (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 α ℝ := by
+  refine Decision μ (fun n↦ Kernel.const _ μ) (measurableSet_potentialMax_prod κ) ?_ ?_
+  · simp [h₀]
+  · simp

LeanMachineLearning/Optimization/Algorithms/RankOpt.lean

@@ -0,0 +1,130 @@
+/-
+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.
+* `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.
+
+## 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 β]
+  (𝓡 : Set (RankRule α)) (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 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
+
+/-- 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 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) (rankingData (data ij.1).2 (data ij.2).2)
+
+/-- The point in the observed data with the maximum function value. -/
+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 potentialMax :=
+    {x | ∃ (r : 𝓡), rankingLoss data r = 0 ∧ 0 ≤ (r.1.1 x (argmaxF data)).1}
+
+variable {𝓡}
+
+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
+  refine Measurable.exists fun r ↦ (.and ?_ ?_)
+  · simp only [rankingLoss]
+    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 [rankingData]
+      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 {𝓡} (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 α β := by
+  refine Decision μ (fun n ↦ Kernel.const _ μ) (measurableSet_potentialMax_prod h𝓡) ?_ ?_
+  · simp [h₀]
+  · simp