diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 7d539fc3..d7965792 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -3,12 +3,18 @@ module -- shake: keep-all public import LeanMachineLearning.MeasureTheory.Constructions.BorelSpace.MeasurableArgMax public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel public import LeanMachineLearning.MeasureTheory.Measurable +public import LeanMachineLearning.MeasureTheory.Order.Lattice public import LeanMachineLearning.Online.Bandit.Algorithms.ETC public import LeanMachineLearning.Online.Bandit.Algorithms.UCB public import LeanMachineLearning.Online.Bandit.ArrayProbSpace 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.Optimization.Algorithms.Utils.Tuple +public import LeanMachineLearning.Optimization.ENNReal public import LeanMachineLearning.Probability.HasCondDistrib public import LeanMachineLearning.Probability.Independence.CondDistrib public import LeanMachineLearning.Probability.Independence.CondIndepFun diff --git a/LeanMachineLearning/MeasureTheory/Order/Lattice.lean b/LeanMachineLearning/MeasureTheory/Order/Lattice.lean new file mode 100644 index 00000000..f4a5b703 --- /dev/null +++ b/LeanMachineLearning/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₂ α] + +@[measurability] +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/Optimization/Algorithms/Decision.lean b/LeanMachineLearning/Optimization/Algorithms/Decision.lean new file mode 100644 index 00000000..f7a60041 --- /dev/null +++ b/LeanMachineLearning/Optimization/Algorithms/Decision.lean @@ -0,0 +1,69 @@ +/- +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.Utils.Tuple +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..ff827d17 --- /dev/null +++ b/LeanMachineLearning/Optimization/Algorithms/LIPO.lean @@ -0,0 +1,67 @@ +/- +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 + +/-! +# 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. +-/ + +@[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 | Tuple.max (fun i ↦ (data i).2) ≤ Tuple.min (fun i ↦ (data i).2 + κ * dist (data i).1 x)} + +lemma measurableSet_potential_max_prod : + MeasurableSet {p : (Iic n → α × ℝ) × α | p.2 ∈ potential_max κ p.1} := by + unfold potential_max + simp only [Set.mem_setOf_eq, measurableSet_setOf] + 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..4414715b --- /dev/null +++ b/LeanMachineLearning/Optimization/Algorithms/RankOpt.lean @@ -0,0 +1,120 @@ +/- +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 + +/-! +# 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. +-/ + +@[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 <| Tuple.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_setOf_eq, measurableSet_setOf] + 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 <| Tuple.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 → α × β ↦ Tuple.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 diff --git a/LeanMachineLearning/Optimization/Algorithms/Utils/Tuple.lean b/LeanMachineLearning/Optimization/Algorithms/Utils/Tuple.lean new file mode 100644 index 00000000..5cc5810d --- /dev/null +++ b/LeanMachineLearning/Optimization/Algorithms/Utils/Tuple.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 Mathlib.Analysis.Normed.Order.Lattice +public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic +public import Mathlib.MeasureTheory.Order.Lattice +public import LeanMachineLearning.MeasureTheory.Order.Lattice + +@[expose] public section + +open Finset + +namespace Tuple + +variable {ι α : Type*} [LinearOrder α] [Fintype ι] [Nonempty ι] (f : ι → α) + +/-- 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) + +instance {n : ℕ} : Nonempty (Iic n) := ⟨0, insert_eq_self.mp rfl⟩ + +variable {n : ℕ} (u : ι → α) + +lemma exists_argmax : ∃ i, u i = max u := by + obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_sup' (by simp : Finset.univ.Nonempty) u + exact ⟨i, hi.symm⟩ + +/-- The index of the maximum value of a tuple. -/ +noncomputable def argmax := (exists_argmax u).choose + +lemma argmax_spec : u (argmax u) = max u := + (exists_argmax u).choose_spec + +lemma le_argmax (x : ι) : u x ≤ u (argmax u) := by + rw [argmax_spec u] + exact le_max u x + +lemma exists_argmin : ∃ i, u i = min u := by + obtain ⟨i, _, hi⟩ := Finset.exists_mem_eq_inf' (by simp : Finset.univ.Nonempty) u + exact ⟨i, hi.symm⟩ + +/-- The index of the minimum value of a tuple. -/ +noncomputable def argmin := (exists_argmin u).choose + +lemma argmin_spec : u (argmin u) = min u := + (exists_argmin u).choose_spec + +lemma argmin_le (x : ι) : u (argmin u) ≤ u x := by + rw [argmin_spec u] + exact min_le u x + +lemma neg_max_eq_min_neg [AddGroup α] [AddLeftMono α] [AddRightMono α] (u : ι → α) : + -(max u) = min (-u) := 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 u, le_argmax u⟩ + +variable [MeasurableSpace α] + +@[fun_prop] +lemma measurable_max [MeasurableSup₂ α] : Measurable (fun (t : ι → α) => max t) := by + suffices (fun (t : ι → α) => max t) = (univ.sup' univ_nonempty fun i t => t i) by + rw [this] + exact measurable_sup' univ_nonempty (fun i _ => measurable_pi_apply i) + ext t; simp [max] + +@[fun_prop] +lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂ α] : + Measurable fun (u : ι → α) ↦ argmax u := by + refine measurable_to_countable' fun i ↦ ?_ + simp only [Set.preimage, Set.mem_singleton_iff] + let Maximizers (u : ι → α) : Set ι := {i | u i = max u} + have : {u : ι → α | argmax u = i} = ⋃ (S) + (hS : ∀ x, Maximizers x = S → argmax x = i), {u | Maximizers u = S} := by + ext u + simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right'] + constructor + · intro hu x hx + rw [← hu] + exact Classical.choose.congr_simp hx (exists_argmax x) + · intro h + exact h u rfl + rw [this] + refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_) + refine measurableSet_eq_fun (by fun_prop) measurable_const + +@[fun_prop] +lemma measurable_min [MeasurableInf₂ α] : Measurable (fun (t : ι → α) => min t) := by + suffices (fun (t : ι → α) => min t) = (univ.inf' univ_nonempty fun i t => t i) by + rw [this] + exact measurable_inf' univ_nonempty (fun i _ => measurable_pi_apply i) + ext t; simp [min] + +@[fun_prop] +lemma measurable_argmin [MeasurableSpace ι] [MeasurableEq α] [MeasurableInf₂ α] : + Measurable fun (u : ι → α) ↦ argmin u := by + refine measurable_to_countable' fun i ↦ ?_ + simp only [Set.preimage, Set.mem_singleton_iff] + let Minimizers (u : ι → α) : Set ι := {i | u i = Tuple.min u} + have : {u : ι → α | argmin u = i} = ⋃ (S) + (hS : ∀ x, Minimizers x = S → argmin x = i), {u | Minimizers u = S} := by + ext u + simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right'] + constructor + · intro hu x hx + rw [← hu] + exact Classical.choose.congr_simp hx (exists_argmin x) + · intro h + exact h u rfl + rw [this] + refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_) + exact measurableSet_eq_fun (by fun_prop) measurable_const + +end Tuple diff --git a/LeanMachineLearning/Optimization/ENNReal.lean b/LeanMachineLearning/Optimization/ENNReal.lean new file mode 100644 index 00000000..894aa2f1 --- /dev/null +++ b/LeanMachineLearning/Optimization/ENNReal.lean @@ -0,0 +1,20 @@ +/- +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.Analysis.Normed.Group.Basic + +@[expose] public section + +open ENNReal Filter + +open scoped Topology + +lemma ENNReal.tendsto_zero_le {α : Type*} {f g : α → ℝ≥0∞} {ι : Filter α} + (hg : Tendsto g ι (𝓝 0)) (h : f ≤ g) : Tendsto f ι (𝓝 0) := by + refine tendsto_of_tendsto_of_tendsto_of_le_of_le (g := fun _ ↦ 0) tendsto_const_nhds hg ?_ h + intro + simp diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean index 7e6e2410..2f1b6a83 100644 --- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean +++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling.lean @@ -5,8 +5,10 @@ Authors: Gaëtan Serré -/ module +public import LeanMachineLearning.Optimization.ENNReal public import LeanMachineLearning.Probability.Independence.IndepFun -public import LeanMachineLearning.SequentialLearning.Algorithm +public import LeanMachineLearning.Optimization.Algorithms.Utils.Tuple +public import LeanMachineLearning.SequentialLearning.EvaluationEnv /-! # Random Sampling @@ -21,8 +23,19 @@ each iteration. ## Main statements -* `hasLaw_action`: Each action follows the distribution μ. -* `iIndep_action`: Actions are mutually independent across time steps. +The main results about the random sampling algorithm are stated using the `evalEnv` evaluation +environment, which rewards actions using a measurable function `f`. + +- `hasLaw_actions`: Each action follows the distribution μ. +- `hasLaw_rewards`: Each reward follows the distribution μ.map f. +- `iIndep_actions`: Actions are mutually independent across time steps. +- `iIndep_rewards`: Rewards are mutually independent across time steps. +- `actions_tendsto_any`: The minimum distance from sampled actions to any point in α tends to zero + in measure. +- `rewards_tendsto_any`: The minimum distance from rewards to any value of `f` tends to zero in + measure. +- `tendsto_min`: The minimum reward converges in measure to the global minimum value. +- `tendsto_max`: The maximum reward converges in measure to the global maximum value. -/ @[expose] public section @@ -48,6 +61,7 @@ noncomputable def randomSampling (μ : Measure 𝓐) [IsProbabilityMeasure μ] : namespace randomSampling variable {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {env : Environment 𝓐 𝓨} + {f : 𝓐 → 𝓨} {hf : Measurable f} /-- Each action follows the distribution μ. -/ lemma hasLaw_action (h : IsAlgEnvSeq A Y (randomSampling μ) env P) (n : ℕ) : @@ -59,6 +73,14 @@ lemma hasLaw_action (h : IsAlgEnvSeq A Y (randomSampling μ) env P) (n : ℕ) : obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn exact hasLaw_of_hasCondDistrib_const <| h.hasCondDistrib_action k +/-- Each reward follows the distribution μ.map f. -/ +lemma hasLaw_rewards (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hf) P) (n : ℕ) : + HasLaw (Y n) (μ.map f) P := by + refine HasLaw.congr ?_ (feedback_evalEnv_ae_eq_eval_action h n) + have hA := h.measurable_action n + refine ⟨by fun_prop, ?_⟩ + rw [← Measure.map_map hf hA, (hasLaw_action h n).map_eq] + /-- Actions are mutually independent. -/ lemma iIndep_action (h : IsAlgEnvSeq A Y (randomSampling μ) env P) : iIndepFun A P := by @@ -74,6 +96,160 @@ lemma iIndep_action (h : IsAlgEnvSeq A Y (randomSampling μ) env P) : exact (condDistrib_eq.comp meas_fst measurable_id).symm · exact (IsAlgEnvSeq.measurable_hist (h.measurable_action) (h.measurable_feedback) n).aemeasurable +/-- Rewards are mutually independent. -/ +lemma iIndep_rewards (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hf) P) : + iIndepFun Y P := + have (n : ℕ) : f ∘ A n =ᵐ[P] Y n := + (feedback_evalEnv_ae_eq_eval_action h n).symm + iIndepFun.congr this <| (iIndep_action h).comp _ (fun _ ↦ hf) + +variable [PseudoMetricSpace 𝓐] [SecondCountableTopology 𝓐] [OpensMeasurableSpace 𝓐] + [μ.IsOpenPosMeasure] + +/-- The minimum distance from sampled actions to any point tends to zero. -/ +theorem actions_tendsto_any (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hf) P) (a : 𝓐) : + ∀ ε, 0 < ε → Tendsto (fun i => P + {x | ε ≤ Tuple.min (fun (j : Iic i) ↦ dist (A j.1 x) a)}) atTop (𝓝 0) := by + set randomSampling_alg := randomSampling (𝓨 := 𝓨) μ + intro ε hε + refine tendsto_zero_le (g := fun n ↦ P (⋂ i ∈ Iic n, {x | ε ≤ dist (A i x) a})) ?_ ?_ + · have inter_prod (n : ℕ) : P (⋂ j ∈ Iic n, {x | ε ≤ dist (A j x) a}) = + ∏ j ∈ Iic n, P {x | ε ≤ dist (A j x) a} := by + refine iIndepSet.meas_biInter ?_ _ + rw [iIndepSet_iff_meas_biInter fun i ↦ ?_] + · intro s + have iIndep_actions := randomSampling.iIndep_action h + rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at iIndep_actions + have meas_dist : ∀ i ∈ s, MeasurableSet {x | ε ≤ dist x a} := by + intro i hs + measurability + specialize iIndep_actions s meas_dist + simpa only [Set.preimage] using iIndep_actions + · have hAi := h.measurable_action i + measurability + simp_rw [inter_prod] + have prod_law (n : ℕ) : ∏ j ∈ Iic n, P {x | ε ≤ dist (A j x) a} = + ∏ j ∈ Iic n, μ {x | ε ≤ dist x a} := by + refine prod_congr rfl fun j hj ↦ ?_ + have hlaw (n : ℕ) : HasLaw (A n) μ P := randomSampling.hasLaw_action h n + rw [← (hlaw j).map_eq, P.map_apply] + · simp + · exact h.measurable_action j + · measurability + simp_rw [prod_law] + simp only [prod_const, Nat.card_Iic] + refine tendsto_pow_atTop_nhds_zero_of_lt_one ?_ |> Tendsto.comp <| tendsto_add_atTop_nat 1 + have compl : {x | ε ≤ dist x a} = {x | dist x a < ε}ᶜ := by + ext a + simp + rw [compl, measure_compl (by measurability) (by simp), measure_univ] + refine ENNReal.sub_lt_self (by simp) (by simp) ?_ + exact (Metric.measure_ball_pos μ a hε).ne' + · intro n + refine measure_mono ?_ + simp only [mem_Iic, Set.subset_iInter_iff, Set.setOf_subset_setOf] + intro i hi ω (hω : ε ≤ Tuple.min (fun (j : Iic n) ↦ dist (A j.1 ω) a)) + simp_all only [univ_eq_attach, le_inf'_iff, mem_attach, forall_const, Subtype.forall, mem_Iic] + +variable [PseudoMetricSpace 𝓨] [BorelSpace 𝓨] (hfc : Continuous f) + +/-- The minimum distance from image of actions to any value tends to zero. -/ +lemma image_actions_tendsto_any + (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hfc.measurable) P) + (a : 𝓐) : ∀ ε, 0 < ε → Tendsto (fun i => P + {x | ε ≤ Tuple.min (fun (j : Iic i) ↦ dist (f (A j.1 x)) (f a))}) atTop (𝓝 0) := by + intro ε hε + have hf := hfc.measurable + rw [Metric.continuous_iff] at hfc + obtain ⟨δ, hδ, hfc⟩ := hfc a ε hε + refine actions_tendsto_any h a δ hδ |> tendsto_zero_le <| ?_ + intro n + refine measure_mono ?_ + simp only [Set.setOf_subset_setOf] + intro ω hω + rw [← Tuple.argmin_spec] + set j := Tuple.argmin (fun (i : Iic n) ↦ dist (A i.1 ω) a) + by_contra! h_contra + specialize hfc (A j.1 ω) h_contra + have := Tuple.min_le (fun (j : Iic n) ↦ dist (f (A (j) ω)) (f a)) j + linarith + +/-- The minimum distance from rewards to any value tends to zero. -/ +lemma rewards_tendsto_any (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hfc.measurable) P) + (a : 𝓐) : ∀ ε, 0 < ε → Tendsto (fun i => P + {x | ε ≤ Tuple.min (fun (j : Iic i) ↦ dist (Y j.1 x) (f a))}) atTop (𝓝 0) := by + intro ε hε + convert image_actions_tendsto_any hfc h a ε hε using 2 with n + refine measure_congr ?_ + let g : ((Iic n) → 𝓨) → ℝ := fun r ↦ Tuple.min (fun i ↦ dist (r i) (f a)) + filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h g] with ω hω + simp only [eq_iff_iff] + change ε ≤ Tuple.min (fun (j : Iic n) ↦ dist (Y j ω) (f a)) ↔ + ε ≤ Tuple.min (fun (j : Iic n) ↦ dist (f (A j ω)) (f a)) + simp [g, hω] + +variable {R : ℕ → Ω → ℝ} {f : 𝓐 → ℝ} (hfc : Continuous f) {a : 𝓐} + +/-- The minimum function value converges to the global minimum. -/ +lemma tendsto_min₀ (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.measurable) P) + (hf_min : ∀ x, f a ≤ f x) : TendstoInMeasure P (fun n ω ↦ + Tuple.min (fun (i : Iic n) ↦ f (A i.1 ω))) atTop (fun _ ↦ f a) := by + rw [tendstoInMeasure_iff_dist] + intro ε hε + refine image_actions_tendsto_any hfc h a ε hε |> tendsto_zero_le <| ?_ + intro n + refine measure_mono ?_ + simp only [Set.setOf_subset_setOf] + intro ω hω + rw [← Tuple.argmin_spec] + set j := Tuple.argmin (fun (i : Iic n) ↦ dist (f (A i ω)) (f a)) + refine hω.trans ?_ + rw [← Tuple.argmin_spec] + set k := Tuple.argmin (fun (i : Iic n) ↦ f (A i ω)) + have := hf_min (A k ω) + have : f (A k ω) ≤ f (A j ω) := + Tuple.argmin_le (fun (i : Iic n) ↦ f (A i ω)) j + simp [Real.dist_eq] + grind + +/-- The minimum reward converges to the global minimum value. -/ +lemma tendsto_min (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.measurable) P) + (hf_min : ∀ x, f a ≤ f x) : TendstoInMeasure P (fun n ω ↦ + Tuple.min (fun (i : Iic n) ↦ R i.1 ω)) atTop (fun _ ↦ f a) := by + refine TendstoInMeasure.congr_left (fun n ↦ ?_) <| tendsto_min₀ hfc h hf_min + filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h Tuple.min] with ω hω + rw [← hω] + +/-- The maximum function value converges to the global maximum. -/ +lemma tendsto_max₀ (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.measurable) P) + (hf_max : ∀ x, f x ≤ f a) : TendstoInMeasure P (fun n ω ↦ + Tuple.max (fun (i : Iic n) ↦ f (A i.1 ω))) atTop (fun _ ↦ f a) := by + rw [tendstoInMeasure_iff_dist] + intro ε hε + refine image_actions_tendsto_any hfc h a ε hε |> tendsto_zero_le <| ?_ + intro n + refine measure_mono ?_ + simp only [Set.setOf_subset_setOf] + intro ω hω + rw [← Tuple.argmin_spec] + set j := Tuple.argmin (fun (i : Iic n) ↦ dist (f (A i ω)) (f a)) + refine hω.trans ?_ + rw [← Tuple.argmax_spec] + set k := Tuple.argmax (fun (i : Iic n) ↦ f (A i ω)) + have := hf_max (A k ω) + have : f (A j ω) ≤ f (A k ω) := + Tuple.le_argmax (fun (i : Iic n) ↦ f (A i ω)) j + simp [Real.dist_eq] + grind + +/-- The maximum reward converges to the global maximum value. -/ +lemma tendsto_max (h : IsAlgEnvSeq A R (randomSampling μ) (evalEnv f hfc.measurable) P) + (hf_max : ∀ x, f x ≤ f a) : + TendstoInMeasure P (fun n ω ↦ Tuple.max (fun (i : Iic n) ↦ R i.1 ω)) atTop (fun _ ↦ f a) := by + refine TendstoInMeasure.congr_left (fun n ↦ ?_) <| tendsto_max₀ hfc h hf_max + filter_upwards [feedback_evalEnv_ae_eq_eval_action_comp h Tuple.max] with ω hω + rw [← hω] + end randomSampling end Learning