From 45cc35ec8ab0f5fa08aa39c88f66f5d82d9ccf12 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Nov 2026 14:27:34 +0100 Subject: [PATCH 1/2] Remove concentration duplication --- .../Probability/Moments/SubGaussian.lean | 33 + .../Algorithms/Regret/BayesRegretTS.lean | 139 +---- .../Online/Bandit/Algorithms/Regret/UCB.lean | 111 ++-- .../Online/Bandit/Concentration.lean | 587 ++++++++---------- .../BayesStationaryEnv.lean | 30 + 5 files changed, 409 insertions(+), 491 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/Probability/Moments/SubGaussian.lean b/LeanMachineLearning/ForMathlib/Probability/Moments/SubGaussian.lean index af186692..f798bd7e 100644 --- a/LeanMachineLearning/ForMathlib/Probability/Moments/SubGaussian.lean +++ b/LeanMachineLearning/ForMathlib/Probability/Moments/SubGaussian.lean @@ -11,6 +11,9 @@ public import Mathlib.Probability.Moments.SubGaussian ## Main statements +* `Kernel.HasSubgaussianMGF.mono`, `HasCondSubgaussianMGF.mono`, `HasSubgaussianMGF.mono`: a + sub-Gaussian moment-generating function with parameter `c` is sub-Gaussian with any larger + parameter. * `HasSubgaussianMGF.measure_le_le`, `HasSubgaussianMGF.measure_sum_le_le_of_iIndepFun`: lower tail bounds (**Hoeffding's inequality** for the lower tail). * `HasSubgaussianMGF.measure_sum_le_sum_le`: bound on the probability that a sum of independent @@ -24,11 +27,34 @@ open scoped ENNReal NNReal namespace ProbabilityTheory +namespace Kernel.HasSubgaussianMGF + +variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : Measure Ω'} + {κ : Kernel Ω' Ω} {X : Ω → ℝ} {c c' : ℝ≥0} + +/-- A random variable with a sub-Gaussian moment-generating function with parameter `c` also has +a sub-Gaussian moment-generating function with any larger parameter. -/ +lemma mono (h : Kernel.HasSubgaussianMGF X c κ ν) (hcc' : c ≤ c') : + Kernel.HasSubgaussianMGF X c' κ ν where + integrable_exp_mul := h.integrable_exp_mul + mgf_le := by + filter_upwards [h.mgf_le] with ω' h t + refine (h t).trans ?_ + gcongr + +end Kernel.HasSubgaussianMGF + namespace HasCondSubgaussianMGF variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℝ} {c : ℝ≥0} +/-- A random variable with a conditionally sub-Gaussian moment-generating function with parameter +`c` also has a conditionally sub-Gaussian moment-generating function with any larger parameter. -/ +lemma mono (h : HasCondSubgaussianMGF m hm X c μ) {c' : ℝ≥0} (hcc' : c ≤ c') : + HasCondSubgaussianMGF m hm X c' μ := + Kernel.HasSubgaussianMGF.mono h hcc' + lemma ae_trim_condExp_exp_sub_le_one (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : ∀ᵐ ω' ∂(μ.trim hm), (μ[fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)|m]) ω' ≤ 1 := by have h_le : ∀ᵐ ω' ∂(μ.trim hm), μ[fun ω ↦ exp (t * X ω)|m] ω' ≤ exp (c * t ^ 2 / 2) := @@ -71,6 +97,13 @@ namespace HasSubgaussianMGF variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X Y : Ω → ℝ} {c cX cY : ℝ≥0} +/-- A random variable with a sub-Gaussian moment-generating function with parameter `c` also has +a sub-Gaussian moment-generating function with any larger parameter. -/ +lemma mono (h : HasSubgaussianMGF X c μ) {c' : ℝ≥0} (hcc' : c ≤ c') : + HasSubgaussianMGF X c' μ where + integrable_exp_mul := h.integrable_exp_mul + mgf_le t := (h.mgf_le t).trans (by gcongr) + /-- Chernoff bound on the left tail of a sub-Gaussian random variable. -/ lemma measure_le_le (h : HasSubgaussianMGF X c μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | X ω ≤ -ε} ≤ exp (-ε ^ 2 / (2 * c)) := by diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean index adaf07f5..6a2f168d 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean @@ -29,10 +29,6 @@ and properties are also given in this file. ## Main statements -* `IsBayesAlgEnvSeq.prob_empMean_sub_actionMean_ge_le`, - `IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le`: for sub-Gaussian rewards, the - empirical means of the actions are close to their means with high probability, uniformly in - time. * `TS.integral_regret_le`: if Thompson sampling has the correct prior over environments, in every environment each of the `K` actions has a mean reward between `l` and `u`, and in almost every environment (under the prior) the reward distribution of each action is sub-Gaussian with @@ -46,7 +42,9 @@ and the best action have the same conditional law given the history, the upper c of the two actions have the same expectation, and the Bayesian regret is the sum of the expected differences between the mean of the best action and its upper confidence bound, and between the upper confidence bound and the mean of the action played (`TS.integral_regret_eq_add`). The first -sum is controlled by concentration, the second one by the widths of the confidence intervals. +sum is controlled by concentration +(`IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le`), the second one by the widths of +the confidence intervals. ## References @@ -62,105 +60,6 @@ sum is controlled by concentration, the second one by the widths of the confiden open MeasureTheory ProbabilityTheory Finset Learning open scoped NNReal -/-! ### Concentration of the empirical means in a Bayesian bandit -/ - -namespace Learning.IsBayesAlgEnvSeq - -variable {𝓔 Ω : Type*} [MeasurableSpace 𝓔] [MeasurableSpace Ω] -variable {K : ℕ} [Nonempty (Fin K)] -variable {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × Fin K) ℝ} [IsMarkovKernel κ] -variable {alg : Algorithm Unit (Fin K) ℝ} -variable {E : Ω → 𝓔} {A : ℕ → Ω → (Fin K)} {R : ℕ → Ω → ℝ} -variable {P : Measure Ω} [IsProbabilityMeasure P] - -/-- Auxiliary lemma for `prob_empMean_sub_actionMean_ge_le`. -/ -private lemma sqrt_two_mul_le_sub {k : ℕ} (hk : k ≠ 0) {s μ σ l : ℝ} - (h : √(2 * σ * l / k) ≤ s / k - μ) : √(2 * k * σ * l) ≤ s - k * μ := by - have hkp : (0 : ℝ) < k := by positivity - calc √(2 * k * σ * l) - _ = √(2 * σ * l / k * k ^ 2) := by - field_simp - _ = √(2 * σ * l / k) * k := by - rw [Real.sqrt_mul' _ (sq_nonneg _), Real.sqrt_sq hkp.le] - _ ≤ (s / k - μ) * k := by - nlinarith - _ = s - k * μ := by - field_simp - -lemma prob_empMean_sub_actionMean_ge_le (h : IsBayesAlgEnvSeq Q κ alg E A R P) {σ2 : ℝ≥0} - (hs : ∀ᵐ e ∂Q, ∀ a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a))) - (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) (n : ℕ) : - P {ω | ∃ t < n, ∃ a, pullCount A a t ω ≠ 0 ∧ - √(2 * σ2 * Real.log (1 / δ) / pullCount A a t ω) ≤ empMean A R a t ω - actionMean κ E a ω} - ≤ ENNReal.ofReal (K * (n - 1) * δ) := by - have := h.measurable_param - have := h.measurable_action - have := h.measurable_feedback - let S : Set (𝓔 × (ℕ → Round Unit (Fin K) ℝ)) := - {(e, τ) | ∃ a, ∃ t < n, pullCount IT.action a t τ ≠ 0 ∧ - √(2 * pullCount IT.action a t τ * σ2 * Real.log (1 / δ)) ≤ - sumRewards IT.action IT.feedback a t τ - pullCount IT.action a t τ * actionMean κ id a e} - calc - _ ≤ (P.map (fun ω ↦ (E ω, trajectory (noObs Ω) A R ω))) S := by - rw [Measure.map_apply (by fun_prop) (by measurability)] - apply measure_mono - intro ω ⟨t, ht, a, hpc, hle⟩ - rw [empMean] at hle - exact ⟨a, t, ht, hpc, sqrt_two_mul_le_sub hpc hle⟩ - _ = (P.map E ⊗ₘ condDistrib (trajectory (noObs Ω) A R) E P) S := by - rw [← compProd_map_condDistrib (by fun_prop) (by fun_prop)] - _ = ∫⁻ e, condDistrib (trajectory (noObs Ω) A R) E P e (Prod.mk e ⁻¹' S) ∂(P.map E) := - Measure.compProd_apply (by measurability) - _ ≤ ∫⁻ e, ENNReal.ofReal (Fintype.card (Fin K) * (n - 1) * δ) ∂(P.map E) := by - apply lintegral_mono_ae - rw [h.hasLaw_env.map_eq] - filter_upwards [h.ae_isAlgEnvSeq, hs] with e he hse - exact Bandits.prob_exists_sumRewards_sub_pullCount_mul_ge_le he hse hσ2 hδ - _ = ENNReal.ofReal (K * (n - 1) * δ) := by - simp [Measure.map_apply h.measurable_param] - -/-- Auxiliary lemma for `prob_empMean_bestAction_sub_actionMean_le_le`. -/ -private lemma sub_le_neg_sqrt_two_mul {k : ℕ} (hk : k ≠ 0) {s μ σ l : ℝ} - (h : s / k - μ ≤ -√(2 * σ * l / k)) : s - k * μ ≤ -√(2 * k * σ * l) := by - have : √(2 * k * σ * l) ≤ -s - k * -μ := sqrt_two_mul_le_sub hk (by grind) - linarith - -lemma prob_empMean_bestAction_sub_actionMean_le_le (h : IsBayesAlgEnvSeq Q κ alg E A R P) - {σ2 : ℝ≥0} (hs : ∀ᵐ e ∂Q, ∀ a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a))) - (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) (n : ℕ) : - P {ω | ∃ t < n, pullCount A (bestAction κ E ω) t ω ≠ 0 ∧ - empMean A R (bestAction κ E ω) t ω - actionMean κ E (bestAction κ E ω) ω ≤ - -√(2 * σ2 * Real.log (1 / δ) / (pullCount A (bestAction κ E ω) t ω))} - ≤ ENNReal.ofReal ((n - 1) * δ) := by - have := h.measurable_param - have := h.measurable_action - have := h.measurable_feedback - let S : Set (𝓔 × (ℕ → Round Unit (Fin K) ℝ)) := - {(e, τ) | ∃ t < n, pullCount IT.action (bestAction κ id e) t τ ≠ 0 ∧ - sumRewards IT.action IT.feedback (bestAction κ id e) t τ - - pullCount IT.action (bestAction κ id e) t τ * actionMean κ id (bestAction κ id e) e ≤ - -√(2 * pullCount IT.action (bestAction κ id e) t τ * σ2 * Real.log (1 / δ))} - calc - _ ≤ (P.map (fun ω ↦ (E ω, trajectory (noObs Ω) A R ω))) S := by - rw [Measure.map_apply (by fun_prop) (by measurability)] - apply measure_mono - intro ω ⟨t, ht, hpc, hle⟩ - rw [empMean] at hle - exact ⟨t, ht, hpc, sub_le_neg_sqrt_two_mul hpc hle⟩ - _ = (P.map E ⊗ₘ condDistrib (trajectory (noObs Ω) A R) E P) S := by - rw [← compProd_map_condDistrib (by fun_prop) (by fun_prop)] - _ = ∫⁻ e, condDistrib (trajectory (noObs Ω) A R) E P e (Prod.mk e ⁻¹' S) ∂(P.map E) := - Measure.compProd_apply (by measurability) - _ ≤ ∫⁻ e, ENNReal.ofReal ((n - 1) * δ) ∂(P.map E) := by - apply lintegral_mono_ae - rw [h.hasLaw_env.map_eq] - filter_upwards [h.ae_isAlgEnvSeq, hs] with e he hse - exact Bandits.prob_sumRewards_sub_pullCount_mul_le_le (ν := κ.sectR e) he (hse _) hσ2 hδ - _ = ENNReal.ofReal ((n - 1) * δ) := by - simp [Measure.map_apply h.measurable_param] - -end Learning.IsBayesAlgEnvSeq - open IsBayesAlgEnvSeq (bestAction actionMean) namespace Bandits @@ -437,7 +336,8 @@ lemma integral_sum_range_ucb_action_sub_actionMean_action_le {alg : Algorithm Un gcongr · have : (0 : ℝ) ≤ n - 1 := by simp [Nat.one_le_iff_ne_zero, hn] apply ENNReal.toReal_le_of_le_ofReal (by positivity) - exact h.prob_empMean_sub_actionMean_ge_le hs hσ2 hδ n + exact (h.prob_empMean_sub_actionMean_ge_le hs hσ2 hδ n).trans_eq + (by rw [Fintype.card_fin]) · exact measureReal_le_one _ = _ := by ring @@ -516,12 +416,8 @@ lemma integral_regret_eq_add (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm Q κ) E A R _ = _ := by rw [← integral_finsetSum _ (by fun_prop), ← integral_finsetSum _ (by fun_prop)] -/-- **Bayesian regret of Thompson sampling.** If Thompson sampling has the correct prior over -environments, in every environment each of the `K` actions has a mean reward between `l` and `u`, -and in almost every environment (under the prior) the reward distribution of each action is -sub-Gaussian with variance proxy `σ2` after its mean is subtracted, then the Bayesian regret at -time `n` is at most `(2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n)`. -/ -theorem integral_regret_le (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm Q κ) E A R P) +/-- The bound of `integral_regret_le` for a nonzero variance proxy `σ2`. -/ +private lemma integral_regret_le_of_ne_zero (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm Q κ) E A R P) (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) (hs : ∀ᵐ e ∂Q, ∀ a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a))) (hσ2 : σ2 ≠ 0) (n : ℕ) : @@ -555,6 +451,27 @@ theorem integral_regret_le (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm Q κ) E A R P _ = _ := by ring +open Filter Topology in +/-- **Bayesian regret of Thompson sampling.** If Thompson sampling has the correct prior over +environments, in every environment each of the `K` actions has a mean reward between `l` and `u`, +and in almost every environment (under the prior) the reward distribution of each action is +sub-Gaussian with variance proxy `σ2` after its mean is subtracted, then the Bayesian regret at +time `n` is at most `(2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n)`. -/ +theorem integral_regret_le (h : IsBayesAlgEnvSeq Q κ (tsAlgorithm Q κ) E A R P) + (hm : ∀ e a, (κ (e, a))[id] ∈ (Set.Icc l u)) + (hs : ∀ᵐ e ∂Q, ∀ a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a))) + (n : ℕ) : + P[IsBayesAlgEnvSeq.regret κ E A n] + ≤ (2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n) := by + -- The bound holds for every variance proxy `σ2' > σ2`, which is nonzero, and is continuous in + -- the variance proxy: let `σ2'` tend to `σ2`. + have h_cont : Continuous fun σ2' : ℝ≥0 ↦ + (2 * K + 1) * (u - l) + 8 * √(σ2' * K * n * Real.log n) := by fun_prop + refine ge_of_tendsto (x := 𝓝[>] σ2) ((h_cont.tendsto σ2).mono_left nhdsWithin_le_nhds) ?_ + filter_upwards [self_mem_nhdsWithin] with σ2' hσ2' + exact integral_regret_le_of_ne_zero h hm (hs.mono fun e he a ↦ (he a).mono hσ2'.le) + (pos_of_gt (show σ2 < σ2' from hσ2')).ne' n + end TS end Bandits diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean index 5ac5c0b0..53709671 100644 --- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean +++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/UCB.lean @@ -70,7 +70,7 @@ omit [IsMarkovKernel ν] in /-- If the means of the best arm and of arm `b` lie in their confidence intervals and the UCB index of `b` is at least that of the best arm, then the number of pulls of `b` is at most `8 * c * log (n + 1) / gap ν b ^ 2`. -/ -lemma pullCount_le_of_ucbIndex_le (hc : 0 ≤ c) {b : Fin K} +lemma pullCount_le_of_ucbIndex_le {b : Fin K} (h_best : (ν (bestArm ν))[id] ≤ empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω) (h_arm : empMean A R b n ω - ucbWidth A c b n ω ≤ (ν b)[id]) (h_le : empMean A R (bestArm ν) n ω + ucbWidth A c (bestArm ν) n ω ≤ @@ -86,62 +86,58 @@ lemma pullCount_le_of_ucbIndex_le (hc : 0 ≤ c) {b : Fin K} rw [this] at h2 field_simp at h2 ⊢ grind - · have : 0 ≤ log (n + 1) := by simp [log_nonneg] - positivity + · -- for a negative argument, the square root is `0` and the gap would be nonpositive + by_contra h_neg + rw [sqrt_eq_zero_of_nonpos (not_le.1 h_neg).le] at h_gap_le + linarith + +/-- Auxiliary lemma for `prob_ucbIndex_le` and `prob_lcbIndex_ge`: the bound of +`prob_exists_empMean_sub_le_neg_sqrt_le` at time `n + 1` with `L = c * log (n + 1)` is at most +`1 / (n + 1) ^ (c - 1)`. -/ +private lemma ofReal_mul_exp_neg_mul_log_le (c : ℝ) (n : ℕ) : + ENNReal.ofReal ((↑(n + 1) - 1) * exp (-(c * log (n + 1)))) ≤ 1 / (n + 1) ^ (c - 1) := by + have hn : (0 : ℝ) < n + 1 := by positivity + calc ENNReal.ofReal ((↑(n + 1) - 1) * exp (-(c * log (n + 1)))) + _ ≤ ENNReal.ofReal ((n + 1) ^ (1 - c)) := by + refine ENNReal.ofReal_le_ofReal ?_ + rw [rpow_def_of_pos hn, show log (n + 1) * (1 - c) = log (n + 1) + -(c * log (n + 1)) by ring, + exp_add, exp_log hn] + gcongr + push_cast + linarith + _ = 1 / (n + 1) ^ (c - 1) := by + rw [← ENNReal.ofReal_rpow_of_pos hn, one_div, ← ENNReal.rpow_neg, neg_sub, + ENNReal.ofReal_add (by positivity) zero_le_one, ENNReal.ofReal_natCast, ENNReal.ofReal_one] /-- The probability that the UCB index of arm `a` is below its mean is at most `1 / (n + 1) ^ (c - 1)`. -/ lemma prob_ucbIndex_le {alg : Algorithm Unit (Fin K) ℝ} (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) - (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : Fin K) (n : ℕ) : + (hσ2 : σ2 ≠ 0) (c : ℝ) (a : Fin K) (n : ℕ) : P {ω | 0 < pullCount A a n ω ∧ empMean A R a n ω + ucbWidth A (c * σ2) a n ω ≤ (ν a)[id]} ≤ 1 / (n + 1) ^ (c - 1) := by - have h_le := prob_pullCount_pos_and_le h a n - (p := fun k x ↦ x / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]) - (B := 1 / (n + 1) ^ c) ?_ ?_ - rotate_left - · simp only [Nat.cast_nonneg, sqrt_div', id_eq] - fun_prop - · exact fun k hk ↦ prob_avg_add_sqrt_log_le hν hσ2 hc a n k hk - simp only [mul_assoc] at h_le - simp only [empMean, ucbWidth, mul_assoc] - calc _ ≤ (n : ℝ≥0∞) * (1 / (n + 1) ^ c) := h_le - _ ≤ (n + 1) * (1 : ℝ≥0∞) / (n + 1) ^ c := by - rw [mul_one_div, mul_one] - gcongr - exact le_self_add - _ = 1 / (n + 1) ^ (c - 1) := by - simp only [mul_one, one_div] - rw [ENNReal.rpow_sub _ _ (by simp) (by finiteness), ENNReal.rpow_one, div_eq_mul_inv, - ENNReal.div_eq_inv_mul, ENNReal.mul_inv (by simp) (by simp), inv_inv] + refine le_trans (measure_mono ?_) ((prob_exists_empMean_sub_le_neg_sqrt_le h (hν a) hσ2 + (c * log (n + 1)) (n + 1)).trans (ofReal_mul_exp_neg_mul_log_le c n)) + rintro ω ⟨h_pos, h_le⟩ + refine ⟨n, n.lt_add_one, h_pos.ne', ?_⟩ + rw [ucbWidth, show 2 * (c * σ2) * log (n + 1) = 2 * σ2 * (c * log (n + 1)) by ring] at h_le + linarith /-- The probability that the lower confidence bound of arm `a` is above its mean is at most `1 / (n + 1) ^ (c - 1)`. -/ lemma prob_lcbIndex_ge {alg : Algorithm Unit (Fin K) ℝ} (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) - (hσ2 : σ2 ≠ 0) (hc : 0 ≤ c) (a : Fin K) (n : ℕ) : + (hσ2 : σ2 ≠ 0) (c : ℝ) (a : Fin K) (n : ℕ) : P {ω | 0 < pullCount A a n ω ∧ (ν a)[id] ≤ empMean A R a n ω - ucbWidth A (c * σ2) a n ω} ≤ 1 / (n + 1) ^ (c - 1) := by - have h_le := prob_pullCount_pos_and_le h a n - (p := fun k x ↦ (ν a)[id] ≤ x / k - √(2 * c * σ2 * log (n + 1) / k)) - (B := 1 / (n + 1) ^ c) ?_ ?_ - rotate_left - · simp only [Nat.cast_nonneg, sqrt_div', id_eq] - fun_prop - · exact fun k hk ↦ prob_avg_sub_sqrt_log_ge hν hσ2 hc a n k hk - simp only [mul_assoc] at h_le - simp only [empMean, ucbWidth, mul_assoc] - calc _ ≤ (n : ℝ≥0∞) * (1 / (n + 1) ^ c) := h_le - _ ≤ (n + 1) * (1 : ℝ≥0∞) / (n + 1) ^ c := by - rw [mul_one_div, mul_one] - gcongr - exact le_self_add - _ = 1 / (n + 1) ^ (c - 1) := by - simp only [mul_one, one_div] - rw [ENNReal.rpow_sub _ _ (by simp) (by finiteness), ENNReal.rpow_one, div_eq_mul_inv, - ENNReal.div_eq_inv_mul, ENNReal.mul_inv (by simp) (by simp), inv_inv] + refine le_trans (measure_mono ?_) ((prob_exists_sqrt_le_empMean_sub_le h (hν a) hσ2 + (c * log (n + 1)) (n + 1)).trans (ofReal_mul_exp_neg_mul_log_le c n)) + rintro ω ⟨h_pos, h_le⟩ + refine ⟨n, n.lt_add_one, h_pos.ne', ?_⟩ + rw [ucbWidth, show 2 * (c * σ2) * log (n + 1) = 2 * σ2 * (c * log (n + 1)) by ring] at h_le + linarith omit [IsMarkovKernel ν] in lemma pullCount_le_add_three (a : Fin K) (n C : ℕ) (ω : Ω) : @@ -228,7 +224,7 @@ lemma sum_indicator_good_event_eq_zero Set.mem_ofPred_eq, Pi.one_apply, one_ne_zero, imp_false, not_and, not_le] intro k hn h_arm hC_lt h_le_best by_contra! h_le_arm - have h := pullCount_le_of_ucbIndex_le (b := A k ω) (by positivity : 0 ≤ c * σ2) h_le_best + have h := pullCount_le_of_ucbIndex_le (b := A k ω) h_le_best (by simpa) ?_ ?_ ?_ rotate_left · refine h_le _ ?_ @@ -381,9 +377,9 @@ lemma lintegral_pullCount_le ∑ s ∈ range n, 1 / ((s : ℝ≥0∞) + 1) ^ (c - 1) + ∑ s ∈ range n, 1 / ((s : ℝ≥0∞) + 1) ^ (c - 1) := by gcongr with s hs s hs - · refine (measure_mono ?_).trans (prob_ucbIndex_le h hν hσ2 (by positivity) (bestArm ν) s) + · refine (measure_mono ?_).trans (prob_ucbIndex_le h hν hσ2 c (bestArm ν) s) grind - · refine (measure_mono ?_).trans (prob_lcbIndex_ge h hν hσ2 (by positivity) a s) + · refine (measure_mono ?_).trans (prob_lcbIndex_ge h hν hσ2 c a s) grind _ ≤ ENNReal.ofReal (8 * c * σ2 * log (n + 1) / gap ν a ^ 2 + 1) + 1 + 2 * ENNReal.ofReal (constSum c n) := by @@ -464,9 +460,9 @@ lemma regret_le (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν refine (regret_le' h' hν hσ2 (div_nonneg hc hσ2'.le) n).trans_eq ?_ rw [show (8 : ℝ) * (c / σ2) * σ2 = 8 * c by rw [mul_assoc, div_mul_cancel₀ _ hσ2'.ne']] -/-- Regret bound for the UCB algorithm with exploration parameter `c > 2 * σ2`, for -`σ2`-sub-Gaussian rewards, with an explicit constant. -/ -theorem regret_le_of_gt_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) +/-- The bound of `regret_le_of_gt_two` for a nonzero variance proxy `σ2`. -/ +private lemma regret_le_of_gt_two_of_ne_zero + (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (hc : 2 * σ2 < c) (n : ℕ) : P[regret ν A n] ≤ @@ -480,6 +476,27 @@ theorem regret_le_of_gt_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environme show c / σ2 - 2 = (c - 2 * σ2) / σ2 by rw [sub_div, mul_div_assoc, div_self hσ2'.ne', mul_one], div_div_eq_mul_div] +open Topology in +/-- Regret bound for the UCB algorithm with exploration parameter `c > 2 * σ2`, for +`σ2`-sub-Gaussian rewards, with an explicit constant. -/ +theorem regret_le_of_gt_two (h : IsAlgEnvSeq O A R (ucbAlgorithm K c) (Environment.bandit ν) P) + (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) + (hc : 2 * σ2 < c) (n : ℕ) : + P[regret ν A n] ≤ + ∑ a, (8 * c * log (n + 1) / gap ν a + gap ν a * (4 + 2 * σ2 / (c - 2 * σ2))) := by + -- The bound holds for every variance proxy `σ2' > σ2` close enough to `σ2` that `2 * σ2' < c`, + -- and is continuous in the variance proxy at `σ2`: let `σ2'` tend to `σ2`. + have h_cont : ContinuousAt (fun x : ℝ ↦ + ∑ a, (8 * c * log (n + 1) / gap ν a + gap ν a * (4 + 2 * x / (c - 2 * x)))) σ2 := by + fun_prop (disch := exact (sub_pos.2 hc).ne') + have h_tendsto : Tendsto (fun σ2' : ℝ≥0 ↦ (σ2' : ℝ)) (𝓝[>] σ2) (𝓝 σ2) := + (NNReal.continuous_coe.tendsto σ2).mono_left nhdsWithin_le_nhds + refine ge_of_tendsto (h_cont.tendsto.comp h_tendsto) ?_ + filter_upwards [self_mem_nhdsWithin, (h_tendsto.const_mul 2).eventually_lt_const hc] + with σ2' hσ2' hc' + exact regret_le_of_gt_two_of_ne_zero h (fun a ↦ (hν a).mono (show σ2 < σ2' from hσ2').le) + (pos_of_gt (show σ2 < σ2' from hσ2')).ne' hc' n + end UCB end Bandits diff --git a/LeanMachineLearning/Online/Bandit/Concentration.lean b/LeanMachineLearning/Online/Bandit/Concentration.lean index ef108d57..907ff588 100644 --- a/LeanMachineLearning/Online/Bandit/Concentration.lean +++ b/LeanMachineLearning/Online/Bandit/Concentration.lean @@ -7,7 +7,9 @@ module public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian public import LeanMachineLearning.Online.Bandit.ArrayProbSpace +public import LeanMachineLearning.Online.Bandit.BayesRegret public import LeanMachineLearning.Online.Bandit.Regret +public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv /-! # Concentration of the sums of rewards @@ -20,14 +22,25 @@ algorithm-environment sequence since the joint law of the numbers of pulls and o rewards does not depend on the probability space (`IsAlgEnvSeq.identDistrib_pullCount_sumRewards`). We then specialize those bounds to sub-Gaussian rewards, for the analysis of the ETC, UCB and -Thompson sampling algorithms. +Thompson sampling algorithms, and transfer them to Bayesian bandits by conditioning on the +environment (`IsBayesAlgEnvSeq.measure_mem_le_of_forall_isAlgEnvSeq`). ## Main statements -* `prob_pullCount_prod_sumRewards_mem_le`, `prob_exists_pullCount_eq_and_sumRewards_mem_le`: bounds - on the probability of events about the number of pulls and the sum of rewards of an action. -* `prob_sumRewards_sub_pullCount_mul_ge_le`, `prob_sumRewards_sub_pullCount_mul_le_le`: uniform in - time sub-Gaussian concentration of the sum of rewards of an action. +* `prob_exists_sumRewards_mem_le`: union bound over the number of pulls, uniformly in time. The + probability that at some time `t < n` the sum of rewards of an action lies in a set that depends + on its number of pulls is at most a sum over `m < n` of probabilities of events about the sum of + `m` i.i.d. rewards. +* `prob_exists_sqrt_le_empMean_sub_le`, `prob_exists_empMean_sub_le_neg_sqrt_le`: for sub-Gaussian + rewards with variance proxy `σ2`, the probability that at some time `t < n` the empirical mean of + an action deviates from its mean by at least `√(2 * σ2 * L / pullCount A a t ω)` is at most + `(n - 1) * exp (-L)`. +* `probReal_sum_le_sum_streamMeasure`: for sub-Gaussian rewards, bound on the probability that the + sum of `m` rewards of the best arm is at most the sum of `m` rewards of another arm. +* `IsBayesAlgEnvSeq.prob_empMean_sub_actionMean_ge_le`, + `IsBayesAlgEnvSeq.prob_empMean_bestAction_sub_actionMean_le_le`: in a Bayesian bandit with + sub-Gaussian rewards, the empirical means of the actions are close to their means with high + probability, uniformly in time. ## References @@ -63,51 +76,6 @@ lemma identDistrib_sum_range_snd (a : 𝓐) (k : ℕ) : (ν := streamMeasure ν), Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)] rfl -lemma prob_pullCount_prod_sumRewards_mem_le (a : 𝓐) (n : ℕ) - {s : Set (ℕ × ℝ)} [DecidablePred (· ∈ Prod.fst '' s)] (hs : MeasurableSet s) : - 𝔓 {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤ - ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by - simp_rw [sumRewards_eq] - calc 𝔓 ((fun ω ↦ (pullCount A a n ω, ∑ i ∈ range (pullCount A a n ω), ω.2 i a)) ⁻¹' s) - _ ≤ 𝔓 {ω | ∃ k ≤ n, (k, ∑ i ∈ range k, ω.2 i a) ∈ s} := by - refine measure_mono fun ω hω ↦ ?_ - simp only [Set.mem_ofPred_eq] at hω ⊢ - exact ⟨pullCount A a n ω, pullCount_le _ _ _, hω⟩ - _ = 𝔓 (⋃ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - {ω | (k, ∑ i ∈ range k, ω.2 i a) ∈ s}) := by congr 1; ext; simp; grind - _ ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - 𝔓 {ω | ∑ i ∈ range k, ω.2 i a ∈ Prod.mk k ⁻¹' s} := measure_biUnion_finset_le _ _ - _ = ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by - congr with k - have : (𝔓).map (fun ω ↦ ∑ i ∈ range k, ω.2 i a) = - (streamMeasure ν).map (fun ω ↦ ∑ i ∈ range k, ω i a) := - (identDistrib_sum_range_snd a k).map_eq - rw [Measure.ext_iff] at this - specialize this (Prod.mk k ⁻¹' s) (hs.preimage (by fun_prop)) - rwa [Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop)), - Measure.map_apply (by fun_prop) (hs.preimage (by fun_prop))] at this - -lemma prob_pullCount_mem_and_sumRewards_mem_le (a : 𝓐) (n : ℕ) - {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : - 𝔓 {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤ - ∑ k ∈ (range (n + 1)).filter (· ∈ s), - streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by - classical - rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty - · simp [h_empty] - convert prob_pullCount_prod_sumRewards_mem_le a n (hs.prod hB) (ν := ν) (alg := alg) - with _ _ _ k hk - · rfl - · ext n - have : ∃ x, x ∈ B := h_nonempty - simp [this] - · ext x - simp only [Set.mem_image, Set.mem_prod, Prod.exists, exists_and_right, exists_and_left, - exists_eq_right, mem_filter, mem_range] at hk - simp [hk.2.1] - lemma prob_exists_pullCount_eq_and_sumRewards_mem_le (a : 𝓐) (m : ℕ) {B : Set ℝ} (hB : MeasurableSet B) : 𝔓 {ω | ∃ n, pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤ streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B} := @@ -151,95 +119,13 @@ end ArrayModel variable {𝓐 Ω : Type*} [DecidableEq 𝓐] {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {alg : Algorithm Unit 𝓐 ℝ} {ν : Kernel 𝓐 ℝ} [IsMarkovKernel ν] - {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {n : ℕ} {a : 𝓐} + {O : ℕ → Ω → Unit} {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {a : 𝓐} variable [Nonempty 𝓐] -/-- Union bound over the possible values of the number of pulls: the probability that the number of -pulls and the sum of rewards of `a` at time `n` lie in `s` is at most a sum over `k ≤ n` of the -probabilities that `k` and the sum of `k` i.i.d. rewards of `a` lie in `s`. -/ -lemma prob_pullCount_prod_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) - {s : Set (ℕ × ℝ)} [DecidablePred (· ∈ Prod.fst '' s)] (hs : MeasurableSet s) : - P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤ - ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by - calc P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} - _ = (ArrayModel.arrayMeasure ν) {ω | (pullCount (ArrayModel.action alg) a n ω, - sumRewards (ArrayModel.action alg) (ArrayModel.reward alg) a n ω) ∈ s} := - (h.identDistrib_prodMk_pullCount_sumRewards (ArrayModel.isAlgEnvSeq_arrayMeasure alg ν) a - n).measure_mem_eq hs - _ ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := - ArrayModel.prob_pullCount_prod_sumRewards_mem_le a n hs - -/-- Union bound over the possible values of the number of pulls: the probability that a measurable -property `p` holds for the number of pulls and the sum of rewards of action `a` at time `n`, with at -least one pull, is at most `n` times a uniform bound on the probability of that property for the -sums of `k ∈ [1, n]` i.i.d. rewards. -/ -lemma prob_pullCount_pos_and_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ) - {p : ℕ → ℝ → Prop} (hp : Measurable fun q : ℕ × ℝ ↦ p q.1 q.2) {B : ℝ≥0∞} - (hB : ∀ k, k ≠ 0 → streamMeasure ν {ω | p k (∑ i ∈ range k, ω i a)} ≤ B) : - P {ω | 0 < pullCount A a n ω ∧ p (pullCount A a n ω) (sumRewards A R a n ω)} ≤ n * B := by - classical - let s : Set (ℕ × ℝ) := {q | 0 < q.1 ∧ p q.1 q.2} - have hs : MeasurableSet s := by - simp only [measurableSet_setOfPred, s] - fun_prop - calc P {ω | 0 < pullCount A a n ω ∧ p (pullCount A a n ω) (sumRewards A R a n ω)} - _ ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := - prob_pullCount_prod_sumRewards_mem_le h hs - _ ≤ ∑ k ∈ Icc 1 n, streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by - refine Finset.sum_le_sum_of_subset_of_nonneg (fun m ↦ ?_) fun _ _ _ ↦ by positivity - simp [s] - grind - _ ≤ ∑ k ∈ Icc 1 n, B := by - gcongr with k hk - refine (measure_mono fun ω hω ↦ ?_).trans (hB k (by grind)) - exact hω.2 - _ = n * B := by simp - -lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) - {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : - P {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤ - ∑ k ∈ (range (n + 1)).filter (· ∈ s), - streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by - classical - rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty - · simp [h_empty] - convert prob_pullCount_prod_sumRewards_mem_le h (hs.prod hB) (ν := ν) (alg := alg) with _ _ _ k hk - · rfl - · ext n - have : ∃ x, x ∈ B := h_nonempty - simp [this] - · ext x - simp only [Set.mem_image, Set.mem_prod, Prod.exists, exists_and_right, exists_and_left, - exists_eq_right, mem_filter, mem_range] at hk - simp [hk.2.1] - -lemma prob_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) - {B : Set ℝ} (hB : MeasurableSet B) : - P (sumRewards A R a n ⁻¹' B) ≤ - ∑ k ∈ range (n + 1), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by - classical - have h_le := prob_pullCount_mem_and_sumRewards_mem_le h .univ hB (a := a) (n := n) - simp only [Set.mem_univ, true_and, filter_true] at h_le - convert h_le - rfl - -lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) - {m : ℕ} (hm : m ≤ n) {B : Set ℝ} (hB : MeasurableSet B) : - P {ω | pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤ - streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B} := by - have h_le := prob_pullCount_mem_and_sumRewards_mem_le h (s := {m}) (by simp) hB (a := a) (n := n) - have hm' : m < n + 1 := by lia - simpa [hm'] using h_le - +/-- The probability that the sum of rewards of action `a` lies in `B` at some time at which `a` has +been pulled `m` times is at most the probability that the sum of `m` i.i.d. rewards of `a` lies +in `B`. -/ lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (m : ℕ) {B : Set ℝ} (hB : MeasurableSet B) : @@ -257,6 +143,89 @@ lemma prob_exists_pullCount_eq_and_sumRewards_mem_le [Countable 𝓐] [Measurabl (ArrayModel.isAlgEnvSeq_arrayMeasure alg ν)).measure_mem_eq hs _ ≤ _ := ArrayModel.prob_exists_pullCount_eq_and_sumRewards_mem_le a m hB +/-- **Union bound over the number of pulls**, uniformly in time: the probability that at some time +`t < n` the sum of rewards of action `a` lies in `B (pullCount A a t ω)` is at most the sum over +`m < n` of the probabilities that the sum of `m` i.i.d. rewards of `a` lies in `B m`. -/ +lemma prob_exists_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ) {B : ℕ → Set ℝ} + (hB : ∀ m, MeasurableSet (B m)) : + P {ω | ∃ t < n, sumRewards A R a t ω ∈ B (pullCount A a t ω)} ≤ + ∑ m ∈ range n, streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B m} := + calc + _ ≤ P (⋃ m ∈ range n, {ω | ∃ t, pullCount A a t ω = m ∧ sumRewards A R a t ω ∈ B m}) := by + refine measure_mono ?_ + rintro ω ⟨t, ht, hB⟩ + exact Set.mem_biUnion (mem_range.2 ((pullCount_le a t ω).trans_lt ht)) ⟨t, rfl, hB⟩ + _ ≤ ∑ m ∈ range n, P {ω | ∃ t, pullCount A a t ω = m ∧ sumRewards A R a t ω ∈ B m} := + measure_biUnion_finset_le _ _ + _ ≤ _ := sum_le_sum fun m _ ↦ prob_exists_pullCount_eq_and_sumRewards_mem_le h a m (hB m) + +/-- Union bound over the number of pulls at time `n`: the probability that the number of pulls and +the sum of rewards of action `a` at time `n` lie in `s` is at most the sum over `k ≤ n` of the +probabilities that `k` and the sum of `k` i.i.d. rewards of `a` lie in `s`. -/ +lemma prob_pullCount_prod_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ) {s : Set (ℕ × ℝ)} + (hs : MeasurableSet s) : + P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤ + ∑ k ∈ range (n + 1), streamMeasure ν {ω | (k, ∑ i ∈ range k, ω i a) ∈ s} := by + refine le_trans (measure_mono ?_) (prob_exists_sumRewards_mem_le h a (n + 1) + (B := fun k ↦ Prod.mk k ⁻¹' s) fun _ ↦ measurable_prodMk_left hs) + exact fun _ hω ↦ ⟨n, n.lt_add_one, hω⟩ + +/-- Union bound over the number of pulls at time `n`: the probability that the number of pulls of +action `a` at time `n` lies in `s` and its sum of rewards lies in `B` is at most the sum over +`k ≤ n` with `k ∈ s` of the probabilities that the sum of `k` i.i.d. rewards of `a` lies in `B`. -/ +lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ) (s : Set ℕ) + [DecidablePred (· ∈ s)] {B : Set ℝ} (hB : MeasurableSet B) : + P {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤ + ∑ k ∈ (range (n + 1)).filter (· ∈ s), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by + refine (prob_pullCount_prod_sumRewards_mem_le h a n + (MeasurableSet.of_discrete.prod hB)).trans_eq ?_ + rw [sum_filter] + refine sum_congr rfl fun k _ ↦ ?_ + split_ifs with hk <;> simp [hk] + +/-- Union bound over the number of pulls at time `n`: the probability that the sum of rewards of +action `a` at time `n` lies in `B` is at most the sum over `k ≤ n` of the probabilities that the +sum of `k` i.i.d. rewards of `a` lies in `B`. -/ +lemma prob_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) (n : ℕ) {B : Set ℝ} + (hB : MeasurableSet B) : + P (sumRewards A R a n ⁻¹' B) ≤ + ∑ k ∈ range (n + 1), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by + refine le_trans (measure_mono ?_) + (prob_exists_sumRewards_mem_le h a (n + 1) (B := fun _ ↦ B) fun _ ↦ hB) + exact fun _ hω ↦ ⟨n, n.lt_add_one, hω⟩ + +/-- Union bound over the number of pulls, uniformly in time, for an action that has been pulled: +if, for all `m ≠ 0`, the sum of `m` i.i.d. rewards of action `a` lies in `B m` with probability at +most `δ`, then the probability that at some time `t < n` the action `a` has been pulled and the +sum of its rewards lies in `B (pullCount A a t ω)` is at most `(n - 1) * δ`. -/ +lemma prob_exists_pullCount_ne_zero_and_sumRewards_mem_le [Countable 𝓐] + [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a : 𝓐) + (n : ℕ) {B : ℕ → Set ℝ} (hB : ∀ m, MeasurableSet (B m)) {δ : ℝ} + (h_le : ∀ m, m ≠ 0 → streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B m} ≤ ENNReal.ofReal δ) : + P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ sumRewards A R a t ω ∈ B (pullCount A a t ω)} ≤ + ENNReal.ofReal ((n - 1) * δ) := + calc + _ ≤ ∑ m ∈ range n, streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ {x | m ≠ 0 ∧ x ∈ B m}} := + prob_exists_sumRewards_mem_le h a n (B := fun m ↦ {x | m ≠ 0 ∧ x ∈ B m}) + fun m ↦ (MeasurableSet.const _).inter (hB m) + _ ≤ ∑ m ∈ range n, if m = 0 then 0 else ENNReal.ofReal δ := by + gcongr with m + split_ifs with hm + · simp [hm] + · refine (measure_mono ?_).trans (h_le m hm) + exact fun _ hω ↦ hω.2 + _ ≤ ENNReal.ofReal ((n - 1) * δ) := by + cases n with + | zero => simp + | succ n => simp [sum_range_succ', ENNReal.ofReal_mul] + +/-- The probability that actions `a` and `b` have been pulled `m₁` and `m₂` times at time `n` and +that the sum of rewards of `a` is at most that of `b` is at most the probability that the sum of +`m₁` i.i.d. rewards of `a` is at most the sum of `m₂` i.i.d. rewards of `b`. -/ lemma probReal_sumRewards_le_sumRewards_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) (a b : 𝓐) (n m₁ m₂ : ℕ) : P.real {ω | pullCount A a n ω = m₁ ∧ pullCount A b n ω = m₂ ∧ @@ -299,120 +268,111 @@ lemma prob_sum_range_sub_le_le_of_hasSubgaussianMGF {σ2 : ℝ≥0} · intro _ _ exact h.congr_identDistrib ((identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _) -/-- Auxiliary lemma for `prob_sum_range_sub_*_le_of_hasSubgaussianMGF'`. -/ -private lemma exp_neg_sqrt_sq_div_le {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) (hn : 0 < n) : - Real.exp (-√(2 * n * σ2 * Real.log (1 / δ)) ^ 2 / (2 * n * σ2)) ≤ δ := by - by_cases hd : δ < 1 - · have hl : 0 < Real.log (1 / δ) := Real.log_pos ((one_lt_div hδ).2 hd) - rw [Real.sq_sqrt (by positivity)] - field_simp - simp [Real.exp_log hδ] - · push Not at hd - have hl : Real.log (1 / δ) ≤ 0 := Real.log_nonpos (by positivity) (div_le_one_of_le₀ hd (hδ.le)) - rw [Real.sqrt_eq_zero_of_nonpos (mul_nonpos_of_nonneg_of_nonpos (by positivity) hl)] - simp [hd] - -lemma prob_sum_range_sub_ge_le_of_hasSubgaussianMGF' {σ2 : ℝ≥0} - (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) - (hn : 0 < n) : - streamMeasure ν {ω | √(2 * n * σ2 * Real.log (1 / δ)) ≤ - ∑ k ∈ range n, (ω k a - (ν a)[id])} ≤ ENNReal.ofReal δ := - calc - _ ≤ ENNReal.ofReal (Real.exp (-√(2 * n * σ2 * Real.log (1 / δ)) ^ 2 / (2 * n * σ2))) := - prob_sum_range_sub_ge_le_of_hasSubgaussianMGF h (by positivity) n - _ ≤ ENNReal.ofReal δ := by - gcongr - exact exp_neg_sqrt_sq_div_le hσ2 hδ hn - -lemma prob_sum_range_sub_le_le_of_hasSubgaussianMGF' {σ2 : ℝ≥0} - (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) - (hn : 0 < n) : - streamMeasure ν {ω | ∑ k ∈ range n, (ω k a - (ν a)[id]) ≤ - -√(2 * n * σ2 * Real.log (1 / δ))} ≤ ENNReal.ofReal δ := - calc - _ ≤ ENNReal.ofReal (Real.exp (-√(2 * n * σ2 * Real.log (1 / δ)) ^ 2 / (2 * n * σ2))) := - prob_sum_range_sub_le_le_of_hasSubgaussianMGF h (by positivity) n - _ ≤ ENNReal.ofReal δ := by +/-- Auxiliary lemma for `prob_sqrt_le_sum_range_sub_le` and `prob_sum_range_sub_le_neg_sqrt_le`. -/ +private lemma exp_neg_sqrt_sq_div_le {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) {k : ℕ} (hk : k ≠ 0) (L : ℝ) : + Real.exp (-√(2 * k * σ2 * L) ^ 2 / (2 * k * σ2)) ≤ Real.exp (-L) := by + rcases le_or_gt 0 L with hL | hL + · rw [Real.sq_sqrt (by positivity)] gcongr - exact exp_neg_sqrt_sq_div_le hσ2 hδ hn + field_simp + rfl + · rw [Real.sqrt_eq_zero_of_nonpos (mul_nonpos_of_nonneg_of_nonpos (by positivity) hL.le)] + simpa using hL.le + +/-- Upper tail of the sum of `k` i.i.d. rewards of action `a`: if the rewards are sub-Gaussian with +variance proxy `σ2`, then the sum of the centered rewards is at least `√(2 * k * σ2 * L)` with +probability at most `exp (-L)`. -/ +lemma prob_sqrt_le_sum_range_sub_le {σ2 : ℝ≥0} + (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {k : ℕ} (hk : k ≠ 0) + (L : ℝ) : + streamMeasure ν {ω | √(2 * k * σ2 * L) ≤ ∑ i ∈ range k, (ω i a - (ν a)[id])} ≤ + ENNReal.ofReal (Real.exp (-L)) := + (prob_sum_range_sub_ge_le_of_hasSubgaussianMGF h (by positivity) k).trans + (ENNReal.ofReal_le_ofReal (exp_neg_sqrt_sq_div_le hσ2 hk L)) + +/-- Lower tail of the sum of `k` i.i.d. rewards of action `a`: if the rewards are sub-Gaussian with +variance proxy `σ2`, then the sum of the centered rewards is at most `-√(2 * k * σ2 * L)` with +probability at most `exp (-L)`. -/ +lemma prob_sum_range_sub_le_neg_sqrt_le {σ2 : ℝ≥0} + (h : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {k : ℕ} (hk : k ≠ 0) + (L : ℝ) : + streamMeasure ν {ω | ∑ i ∈ range k, (ω i a - (ν a)[id]) ≤ -√(2 * k * σ2 * L)} ≤ + ENNReal.ofReal (Real.exp (-L)) := + (prob_sum_range_sub_le_le_of_hasSubgaussianMGF h (by positivity) k).trans + (ENNReal.ofReal_le_ofReal (exp_neg_sqrt_sq_div_le hσ2 hk L)) end StreamMeasure -/-- Union bound over the number of pulls: if, for all `m ≠ 0`, the sum of `m` i.i.d. rewards of -action `a` (under `streamMeasure ν`) lies in `B m` with probability at most `δ`, then the -probability that there is a time `t < n` at which `a` has been pulled and the sum of its rewards -lies in `B (pullCount A a t ω)` is at most `(n - 1) * δ`. -/ -lemma prob_exists_sumRewards_mem_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] - (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {B : ℕ → Set ℝ} - (hB : ∀ m, MeasurableSet (B m)) {δ : ℝ} (hδ : 0 ≤ δ) - (h_le : ∀ m, m ≠ 0 → streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B m} ≤ ENNReal.ofReal δ) : - P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ sumRewards A R a t ω ∈ B (pullCount A a t ω)} ≤ - ENNReal.ofReal ((n - 1) * δ) := - calc - _ ≤ P (⋃ m ∈ Icc 1 (n - 1), {ω | ∃ t, t < n ∧ pullCount A a t ω = m ∧ - sumRewards A R a t ω ∈ B m}) := by - apply measure_mono - intro ω ⟨t, ht, hp, hb⟩ - have hm : pullCount A a t ω ∈ Icc 1 (n - 1) := mem_Icc.mpr ⟨Nat.one_le_iff_ne_zero.mpr hp, - (pullCount_le a t ω).trans (Nat.le_sub_one_of_lt ht)⟩ - exact Set.mem_biUnion hm ⟨t, ht, rfl, hb⟩ - _ ≤ ∑ m ∈ Icc 1 (n - 1), P {ω | ∃ t, t < n ∧ pullCount A a t ω = m ∧ - sumRewards A R a t ω ∈ B m} := - measure_biUnion_finset_le _ _ - _ ≤ ∑ m ∈ Icc 1 (n - 1), P {ω | ∃ t, pullCount A a t ω = m ∧ sumRewards A R a t ω ∈ B m} := - sum_le_sum (fun _ _ ↦ measure_mono (fun _ ⟨t, _, hps⟩ ↦ ⟨t, hps⟩)) - _ ≤ ∑ m ∈ Icc 1 (n - 1), streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B m} := - sum_le_sum fun m _ ↦ prob_exists_pullCount_eq_and_sumRewards_mem_le h a m (hB m) - _ ≤ ∑ m ∈ Icc 1 (n - 1), ENNReal.ofReal δ := - sum_le_sum fun m hm ↦ h_le m (Nat.one_le_iff_ne_zero.mp (mem_Icc.mp hm).1) - _ = ENNReal.ofReal ((n - 1) * δ) := by - by_cases hn : n = 0 - · simp [hn, hδ] - · rw [sum_const, Nat.card_Icc, add_tsub_cancel_right, ← ENNReal.ofReal_nsmul, nsmul_eq_mul, - Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hn)] - ring_nf - -lemma prob_sumRewards_sub_pullCount_mul_ge_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] +/-- Auxiliary lemma for `prob_exists_sqrt_le_empMean_sub_le`: a deviation of the mean `s / k` of +`k` values is a deviation of their sum `s`. -/ +private lemma sqrt_le_div_sub_iff {k : ℕ} (hk : k ≠ 0) {s μ σ L : ℝ} : + √(2 * σ * L / k) ≤ s / k - μ ↔ √(2 * k * σ * L) ≤ s - k * μ := by + have hk' : (0 : ℝ) < k := by positivity + have h_sqrt : √(2 * k * σ * L) = √(2 * σ * L / k) * k := + calc √(2 * k * σ * L) + _ = √(2 * σ * L / k * k ^ 2) := by field_simp + _ = √(2 * σ * L / k) * k := by rw [Real.sqrt_mul' _ (sq_nonneg _), Real.sqrt_sq hk'.le] + rw [h_sqrt, show s - k * μ = (s / k - μ) * k by field_simp, mul_le_mul_iff_of_pos_right hk'] + +/-- Auxiliary lemma for `prob_exists_empMean_sub_le_neg_sqrt_le`. -/ +private lemma div_sub_le_neg_sqrt_iff {k : ℕ} (hk : k ≠ 0) {s μ σ L : ℝ} : + s / k - μ ≤ -√(2 * σ * L / k) ↔ s - k * μ ≤ -√(2 * k * σ * L) := by + have h := sqrt_le_div_sub_iff hk (s := -s) (μ := -μ) (σ := σ) (L := L) + rw [neg_div] at h + constructor + · exact fun h' ↦ by linarith [h.1 (by linarith)] + · exact fun h' ↦ by linarith [h.2 (by linarith)] + +/-- Uniform in time concentration of the empirical mean of action `a`, for rewards that are +sub-Gaussian with variance proxy `σ2`: the probability that at some time `t < n` the action `a` +has been pulled and its empirical mean exceeds its mean by at least +`√(2 * σ2 * L / pullCount A a t ω)` is at most `(n - 1) * exp (-L)`. -/ +lemma prob_exists_sqrt_le_empMean_sub_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {σ2 : ℝ≥0} - (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) : - P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤ - sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} ≤ ENNReal.ofReal ((n - 1) * δ) := - prob_exists_sumRewards_mem_le h - (B := fun m ↦ {x | √(2 * m * σ2 * Real.log (1 / δ)) ≤ x - m * (ν a)[id]}) - (fun _ ↦ measurableSet_le (by fun_prop) (by fun_prop)) hδ.le fun m hm ↦ - le_of_eq_of_le (by simp) (StreamMeasure.prob_sum_range_sub_ge_le_of_hasSubgaussianMGF' ha hσ2 hδ - (Nat.pos_of_ne_zero hm)) - -lemma prob_sumRewards_sub_pullCount_mul_le_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] + (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (L : ℝ) (n : ℕ) : + P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ + √(2 * σ2 * L / pullCount A a t ω) ≤ empMean A R a t ω - (ν a)[id]} ≤ + ENNReal.ofReal ((n - 1) * Real.exp (-L)) := by + refine le_trans (measure_mono ?_) (prob_exists_pullCount_ne_zero_and_sumRewards_mem_le h a n + (B := fun m ↦ {x | √(2 * m * σ2 * L) ≤ x - m * (ν a)[id]}) + (fun _ ↦ measurableSet_le (by fun_prop) (by fun_prop)) fun m hm ↦ + le_of_eq_of_le (by simp) (StreamMeasure.prob_sqrt_le_sum_range_sub_le ha hσ2 hm L)) + rintro ω ⟨t, ht, h0, hle⟩ + exact ⟨t, ht, h0, (sqrt_le_div_sub_iff h0).1 hle⟩ + +/-- Uniform in time concentration of the empirical mean of action `a`, for rewards that are +sub-Gaussian with variance proxy `σ2`: the probability that at some time `t < n` the action `a` +has been pulled and its empirical mean is below its mean by at least +`√(2 * σ2 * L / pullCount A a t ω)` is at most `(n - 1) * exp (-L)`. -/ +lemma prob_exists_empMean_sub_le_neg_sqrt_le [Countable 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {σ2 : ℝ≥0} - (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) : + (ha : HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (L : ℝ) (n : ℕ) : P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ - sumRewards A R a t ω - pullCount A a t ω * (ν a)[id] ≤ - -√(2 * pullCount A a t ω * σ2 * Real.log (1 / δ))} ≤ ENNReal.ofReal ((n - 1) * δ) := - prob_exists_sumRewards_mem_le h - (B := fun m ↦ {x | x - m * (ν a)[id] ≤ -√(2 * m * σ2 * Real.log (1 / δ))}) - (fun _ ↦ measurableSet_le (by fun_prop) (by fun_prop)) hδ.le fun m hm ↦ - le_of_eq_of_le (by simp) (StreamMeasure.prob_sum_range_sub_le_le_of_hasSubgaussianMGF' ha hσ2 hδ - (Nat.pos_of_ne_zero hm)) - -/-- Union bound over the actions in `prob_sumRewards_sub_pullCount_mul_ge_le`. -/ -lemma prob_exists_sumRewards_sub_pullCount_mul_ge_le [Fintype 𝓐] [MeasurableSingletonClass 𝓐] + empMean A R a t ω - (ν a)[id] ≤ -√(2 * σ2 * L / pullCount A a t ω)} ≤ + ENNReal.ofReal ((n - 1) * Real.exp (-L)) := by + refine le_trans (measure_mono ?_) (prob_exists_pullCount_ne_zero_and_sumRewards_mem_le h a n + (B := fun m ↦ {x | x - m * (ν a)[id] ≤ -√(2 * m * σ2 * L)}) + (fun _ ↦ measurableSet_le (by fun_prop) (by fun_prop)) fun m hm ↦ + le_of_eq_of_le (by simp) (StreamMeasure.prob_sum_range_sub_le_neg_sqrt_le ha hσ2 hm L)) + rintro ω ⟨t, ht, h0, hle⟩ + exact ⟨t, ht, h0, (div_sub_le_neg_sqrt_iff h0).1 hle⟩ + +/-- Union bound over the actions in `prob_exists_sqrt_le_empMean_sub_le`. -/ +lemma prob_exists_action_sqrt_le_empMean_sub_le [Fintype 𝓐] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A R alg (Environment.bandit ν) P) {σ2 : ℝ≥0} - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) {δ : ℝ} - (hδ : 0 < δ) : + (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) (L : ℝ) + (n : ℕ) : P {ω | ∃ a, ∃ t < n, pullCount A a t ω ≠ 0 ∧ - √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤ - sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} ≤ - ENNReal.ofReal (Fintype.card 𝓐 * (n - 1) * δ) := + √(2 * σ2 * L / pullCount A a t ω) ≤ empMean A R a t ω - (ν a)[id]} ≤ + ENNReal.ofReal (Fintype.card 𝓐 * (n - 1) * Real.exp (-L)) := calc _ ≤ ∑ a, P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧ - √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤ - sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} := by + √(2 * σ2 * L / pullCount A a t ω) ≤ empMean A R a t ω - (ν a)[id]} := by rw [Set.ofPred_exists] exact measure_iUnion_fintype_le _ _ - _ ≤ ∑ a, ENNReal.ofReal ((n - 1) * δ) := - sum_le_sum fun a _ ↦ prob_sumRewards_sub_pullCount_mul_ge_le h (hν a) hσ2 hδ - _ = ENNReal.ofReal (Fintype.card 𝓐 * (n - 1) * δ) := by + _ ≤ ∑ a, ENNReal.ofReal ((n - 1) * Real.exp (-L)) := + sum_le_sum fun a _ ↦ prob_exists_sqrt_le_empMean_sub_le h (hν a) hσ2 L n + _ = ENNReal.ofReal (Fintype.card 𝓐 * (n - 1) * Real.exp (-L)) := by rw [sum_const, Finset.card_univ, ← ENNReal.ofReal_nsmul, nsmul_eq_mul] ring_nf @@ -447,102 +407,63 @@ lemma probReal_sum_le_sum_streamMeasure [Fintype 𝓐] {c : ℝ≥0} field_simp ring -omit [DecidableEq 𝓐] [Nonempty 𝓐] in -lemma prob_sum_le_sqrt_log {σ2 : ℝ≥0} - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) - (hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : 𝓐) (k : ℕ) (hk : k ≠ 0) : - streamMeasure ν - {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * Real.log (n + 1))} ≤ - 1 / (n + 1) ^ c := by - calc - streamMeasure ν - {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * Real.log (n + 1))} - _ ≤ ENNReal.ofReal (Real.exp (-(√(2 * c * k * σ2 * Real.log (n + 1))) ^ 2 / (2 * k * σ2))) := - StreamMeasure.prob_sum_range_sub_le_le_of_hasSubgaussianMGF (hν a) (by positivity) k - _ = 1 / (n + 1) ^ c := by - rw [Real.sq_sqrt] - swap; · exact mul_nonneg (by positivity) (Real.log_nonneg (by simp)) - field_simp - rw [← Real.log_rpow (by positivity), ← Real.log_inv, - Real.exp_log (by positivity), one_div, ENNReal.ofReal_inv_of_pos (by positivity), - ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)] - norm_cast - -omit [DecidableEq 𝓐] [Nonempty 𝓐] in -lemma prob_sum_ge_sqrt_log {σ2 : ℝ≥0} - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) - (hσ2 : σ2 ≠ 0) {c : ℝ} (hc : 0 ≤ c) (a : 𝓐) (k : ℕ) (hk : k ≠ 0) : - streamMeasure ν - {ω | √(2 * c * k * σ2 * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} ≤ - 1 / (n + 1) ^ c := by - calc - streamMeasure ν - {ω | √(2 * c * k * σ2 * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} - _ ≤ ENNReal.ofReal (Real.exp (-(√(2 * c * k * σ2 * Real.log (n + 1))) ^ 2 / (2 * k * σ2))) := - StreamMeasure.prob_sum_range_sub_ge_le_of_hasSubgaussianMGF (hν a) (by positivity) k - _ = 1 / (n + 1) ^ c := by - rw [Real.sq_sqrt] - swap; · exact mul_nonneg (by positivity) (Real.log_nonneg (by simp)) - field_simp - rw [← Real.log_rpow (by positivity), ← Real.log_inv, - Real.exp_log (by positivity), one_div, ENNReal.ofReal_inv_of_pos (by positivity), - ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)] - norm_cast - -open Real - -omit [DecidableEq 𝓐] [Nonempty 𝓐] in -lemma prob_avg_add_sqrt_log_le {σ2 : ℝ≥0} {c : ℝ} - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) - (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) : - streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]} ≤ - 1 / (n + 1) ^ c := by - have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp) - calc - streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]} - _ = streamMeasure ν - {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) / k ≤ - √(2 * c * σ2 * log (n + 1) / k)} := by - congr with ω - field_simp - rw [Finset.sum_sub_distrib] - simp - grind - _ = streamMeasure ν - {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(2 * c * k * σ2 * log (n + 1))} := by - congr with ω - field_simp - congr! 2 - rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt, - mul_assoc (k : ℝ), mul_assoc (k : ℝ), mul_assoc (k : ℝ), - sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm] - _ ≤ 1 / (n + 1) ^ c := prob_sum_le_sqrt_log hν hσ2 hc a k hk - -omit [DecidableEq 𝓐] [Nonempty 𝓐] in -lemma prob_avg_sub_sqrt_log_ge {σ2 : ℝ≥0} {c : ℝ} - (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0) - (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) : - streamMeasure ν - {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(2 * c * σ2 *log (n + 1) / k)} ≤ - 1 / (n + 1) ^ c := by - have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp) - calc - streamMeasure ν {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(2 * c * σ2 * log (n + 1) / k)} - _ = streamMeasure ν - {ω | √(2 * c * σ2 * log (n + 1) / k) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id])) / k} := by - congr with ω - field_simp - rw [Finset.sum_sub_distrib] - simp - grind - _ = streamMeasure ν - {ω | √(2 * c * k * σ2 * log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} := by - congr with ω - field_simp - congr! 1 - rw [sqrt_div (by positivity), ← mul_div_assoc, mul_comm, mul_div_assoc, div_sqrt, - mul_comm _ (k : ℝ), sqrt_mul (x := (k : ℝ)) (by positivity), mul_comm] - _ ≤ 1 / (n + 1) ^ c := prob_sum_ge_sqrt_log hν hσ2 hc a k hk - end Subgaussian end Bandits + +/-! ### Concentration of the empirical means in a Bayesian bandit -/ + +namespace Learning.IsBayesAlgEnvSeq + +variable {𝓔 𝓐 Ω : Type*} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace Ω] + [Fintype 𝓐] [DecidableEq 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] + {Q : Measure 𝓔} [IsProbabilityMeasure Q] {κ : Kernel (𝓔 × 𝓐) ℝ} [IsMarkovKernel κ] + {alg : Algorithm Unit 𝓐 ℝ} {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} + {P : Measure Ω} [IsProbabilityMeasure P] + +/-- Uniform in time concentration of the empirical means in a Bayesian bandit: if for almost every +environment the rewards are sub-Gaussian with variance proxy `σ2`, then the probability that at +some time `t < n` the empirical mean of some action that has been pulled exceeds its mean by at +least `√(2 * σ2 * log (1 / δ) / pullCount A a t ω)` is at most `|𝓐| * (n - 1) * δ`. -/ +lemma prob_empMean_sub_actionMean_ge_le (h : IsBayesAlgEnvSeq Q κ alg E A R P) {σ2 : ℝ≥0} + (hs : ∀ᵐ e ∂Q, ∀ a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a))) + (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) (n : ℕ) : + P {ω | ∃ t < n, ∃ a, pullCount A a t ω ≠ 0 ∧ + √(2 * σ2 * Real.log (1 / δ) / pullCount A a t ω) ≤ empMean A R a t ω - actionMean κ E a ω} + ≤ ENNReal.ofReal (Fintype.card 𝓐 * (n - 1) * δ) := by + let S : Set (𝓔 × (ℕ → Round Unit 𝓐 ℝ)) := + {p | ∃ a, ∃ t < n, pullCount IT.action a t p.2 ≠ 0 ∧ + √(2 * σ2 * Real.log (1 / δ) / pullCount IT.action a t p.2) ≤ + empMean IT.action IT.feedback a t p.2 - actionMean κ id a p.1} + refine le_trans (measure_mono ?_) (h.measure_mem_le_of_forall_isAlgEnvSeq (S := S) + (by measurability) ?_) + · rintro ω ⟨t, ht, a, hpc, hle⟩ + exact ⟨a, t, ht, hpc, hle⟩ + · filter_upwards [hs] with e hse P' _ he + refine (Bandits.prob_exists_action_sqrt_le_empMean_sub_le he hse hσ2 _ n).trans_eq ?_ + simp [Real.exp_log hδ] + +/-- Uniform in time concentration of the empirical mean of the best action in a Bayesian bandit: if +for almost every environment the rewards are sub-Gaussian with variance proxy `σ2`, then the +probability that at some time `t < n` the empirical mean of the best action, if it has been +pulled, is below its mean by at least `√(2 * σ2 * log (1 / δ) / pullCount A a t ω)` is at most +`(n - 1) * δ`. -/ +lemma prob_empMean_bestAction_sub_actionMean_le_le (h : IsBayesAlgEnvSeq Q κ alg E A R P) + {σ2 : ℝ≥0} (hs : ∀ᵐ e ∂Q, ∀ a, HasSubgaussianMGF (fun x ↦ x - (κ (e, a))[id]) σ2 (κ (e, a))) + (hσ2 : σ2 ≠ 0) {δ : ℝ} (hδ : 0 < δ) (n : ℕ) : + P {ω | ∃ t < n, pullCount A (bestAction κ E ω) t ω ≠ 0 ∧ + empMean A R (bestAction κ E ω) t ω - actionMean κ E (bestAction κ E ω) ω ≤ + -√(2 * σ2 * Real.log (1 / δ) / (pullCount A (bestAction κ E ω) t ω))} + ≤ ENNReal.ofReal ((n - 1) * δ) := by + let S : Set (𝓔 × (ℕ → Round Unit 𝓐 ℝ)) := + {p | ∃ t < n, pullCount IT.action (bestAction κ id p.1) t p.2 ≠ 0 ∧ + empMean IT.action IT.feedback (bestAction κ id p.1) t p.2 - + actionMean κ id (bestAction κ id p.1) p.1 ≤ + -√(2 * σ2 * Real.log (1 / δ) / pullCount IT.action (bestAction κ id p.1) t p.2)} + refine h.measure_mem_le_of_forall_isAlgEnvSeq (S := S) (by measurability) ?_ + filter_upwards [hs] with e hse P' _ he + refine (Bandits.prob_exists_empMean_sub_le_neg_sqrt_le (ν := κ.sectR e) (a := bestAction κ id e) + he (hse _) hσ2 _ n).trans_eq ?_ + simp [Real.exp_log hδ] + +end Learning.IsBayesAlgEnvSeq diff --git a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean index db8fc628..4539b20e 100644 --- a/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean +++ b/LeanMachineLearning/SequentialLearning/BayesStationaryEnv.lean @@ -49,6 +49,10 @@ an `alg : Algorithm Unit 𝓐 𝓨`, an algorithm that does not use the observat `Environment.bandit (κ.sectR e)` under `condDistrib (trajectory (noObs Ω) A Y) E P e`, the conditional law of the observable trajectory given `E = e`. This allows transferring results from the `IsAlgEnvSeq` structure to the `IsBayesAlgEnvSeq` structure. +* `IsBayesAlgEnvSeq.measure_mem_le_of_forall_isAlgEnvSeq h`: a bound on the probability of an event + about the parameter and the observable trajectory follows from a bound, for `Q`-almost every `e`, + that holds for every algorithm-environment sequence for `alg` and + `Environment.bandit (κ.sectR e)`. -/ @@ -262,6 +266,32 @@ lemma ae_isAlgEnvSeq (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : exact ⟨IT.measurable_obs, IT.measurable_action, IT.measurable_feedback, fun n ↦ hasCondDistrib_unit (IT.measurable_hist n).aemeasurable _ _, hA, hY⟩ +/-- To bound the probability that the parameter and the observable trajectory lie in a measurable +set `S`, it suffices to bound, for `Q`-almost every `e`, the probability of the section of `S` at +`e` under the law of any algorithm-environment sequence for `alg` and the stationary environment +`Environment.bandit (κ.sectR e)`. -/ +lemma measure_mem_le_of_forall_isAlgEnvSeq (h : IsBayesAlgEnvSeq Q κ alg E A Y P) + {S : Set (𝓔 × (ℕ → Round Unit 𝓐 𝓨))} (hS : MeasurableSet S) {b : ℝ≥0∞} + (hb : ∀ᵐ e ∂Q, ∀ (P' : Measure (ℕ → Round Unit 𝓐 𝓨)) [IsProbabilityMeasure P'], + IsAlgEnvSeq IT.obs IT.action IT.feedback alg (Environment.bandit (κ.sectR e)) P' → + P' (Prod.mk e ⁻¹' S) ≤ b) : + P {ω | (E ω, trajectory (noObs Ω) A Y ω) ∈ S} ≤ b := by + have hτ : Measurable (trajectory (noObs Ω) A Y) := + measurable_trajectory (fun _ ↦ measurable_const) h.measurable_action h.measurable_feedback + calc P {ω | (E ω, trajectory (noObs Ω) A Y ω) ∈ S} + _ = (P.map E ⊗ₘ condDistrib (trajectory (noObs Ω) A Y) E P) S := by + rw [compProd_map_condDistrib h.measurable_param.aemeasurable hτ.aemeasurable, + Measure.map_apply (h.measurable_param.prodMk hτ) hS] + rfl + _ = ∫⁻ e, condDistrib (trajectory (noObs Ω) A Y) E P e (Prod.mk e ⁻¹' S) ∂(P.map E) := + Measure.compProd_apply hS + _ ≤ ∫⁻ _, b ∂Q := by + rw [h.hasLaw_env.map_eq] + refine lintegral_mono_ae ?_ + filter_upwards [h.ae_isAlgEnvSeq, hb] with e he hbe + exact hbe _ he + _ = b := by simp + end IsBayesAlgEnvSeq section IsAlgEnvSeq From 7962935813c9b2d1873d08673f8f8119fb9e96a1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 3 Nov 2026 14:28:41 +0100 Subject: [PATCH 2/2] inline private aux lemma --- .../Online/Bandit/Concentration.lean | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/LeanMachineLearning/Online/Bandit/Concentration.lean b/LeanMachineLearning/Online/Bandit/Concentration.lean index 907ff588..a07ae45a 100644 --- a/LeanMachineLearning/Online/Bandit/Concentration.lean +++ b/LeanMachineLearning/Online/Bandit/Concentration.lean @@ -314,15 +314,6 @@ private lemma sqrt_le_div_sub_iff {k : ℕ} (hk : k ≠ 0) {s μ σ L : ℝ} : _ = √(2 * σ * L / k) * k := by rw [Real.sqrt_mul' _ (sq_nonneg _), Real.sqrt_sq hk'.le] rw [h_sqrt, show s - k * μ = (s / k - μ) * k by field_simp, mul_le_mul_iff_of_pos_right hk'] -/-- Auxiliary lemma for `prob_exists_empMean_sub_le_neg_sqrt_le`. -/ -private lemma div_sub_le_neg_sqrt_iff {k : ℕ} (hk : k ≠ 0) {s μ σ L : ℝ} : - s / k - μ ≤ -√(2 * σ * L / k) ↔ s - k * μ ≤ -√(2 * k * σ * L) := by - have h := sqrt_le_div_sub_iff hk (s := -s) (μ := -μ) (σ := σ) (L := L) - rw [neg_div] at h - constructor - · exact fun h' ↦ by linarith [h.1 (by linarith)] - · exact fun h' ↦ by linarith [h.2 (by linarith)] - /-- Uniform in time concentration of the empirical mean of action `a`, for rewards that are sub-Gaussian with variance proxy `σ2`: the probability that at some time `t < n` the action `a` has been pulled and its empirical mean exceeds its mean by at least @@ -355,6 +346,13 @@ lemma prob_exists_empMean_sub_le_neg_sqrt_le [Countable 𝓐] [MeasurableSinglet (fun _ ↦ measurableSet_le (by fun_prop) (by fun_prop)) fun m hm ↦ le_of_eq_of_le (by simp) (StreamMeasure.prob_sum_range_sub_le_neg_sqrt_le ha hσ2 hm L)) rintro ω ⟨t, ht, h0, hle⟩ + have div_sub_le_neg_sqrt_iff {k : ℕ} (hk : k ≠ 0) {s μ σ L : ℝ} : + s / k - μ ≤ -√(2 * σ * L / k) ↔ s - k * μ ≤ -√(2 * k * σ * L) := by + have h := sqrt_le_div_sub_iff hk (s := -s) (μ := -μ) (σ := σ) (L := L) + rw [neg_div] at h + constructor + · exact fun h' ↦ by linarith [h.1 (by linarith)] + · exact fun h' ↦ by linarith [h.2 (by linarith)] exact ⟨t, ht, h0, (div_sub_le_neg_sqrt_iff h0).1 hle⟩ /-- Union bound over the actions in `prob_exists_sqrt_le_empMean_sub_le`. -/