diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean index defe8102..01d032c0 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean @@ -50,6 +50,10 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv * `Real.add_one_mul_log_sub_le_one`: `(m + 1) log (m + 1) - m log m - log (m + 1 / 2) ≤ 1` for `m : ℕ`. * `Real.log_div_le_log_one_div_add_log`: `log (x / δ) ≤ log (1 / δ) + log x` for `δ ∈ (0, 1]`. +* `Real.natCeil_log_inv_one_sub_add_one_le`: `⌈log (1 - γ)⁻¹⌉₊ + 1 ≤ 2 log (e / (1 - γ))` for + `0 ≤ γ < 1`. +* `Real.mul_exp_neg_log_div_le`: `c exp (-log (x / δ)) ≤ δ / n` for `c n ≤ x`, the count of + confidence levels in union bounds over `n` events. * `Real.eventually_log_le_mul_of_isBigO`: if `r n = O(n ^ p)`, then `log (r n) ≤ ε n` for all large `n`, for every `ε > 0`. * `Real.eventually_exists_add_le_mul_and_forall_ofReal_add_lt_mul`: for `1 < κ c` and @@ -420,6 +424,27 @@ theorem log_div_le_log_one_div_add_log (x : ℝ) {δ : ℝ} (hδ : 0 < δ) (hδ1 · rw [log_div hx hδ.ne', one_div, log_inv] linarith +/-- For `0 ≤ γ < 1`, `⌈log (1 - γ)⁻¹⌉₊ + 1 ≤ 2 log (e / (1 - γ))`. The left-hand side counts the +levels `0, …, ⌈log (1 - γ)⁻¹⌉₊` of a recursion run for `log (1 - γ)⁻¹` steps, as in the union +bounds of model-based policy evaluation with a generative model. -/ +theorem natCeil_log_inv_one_sub_add_one_le {γ : ℝ} (hγ₀ : 0 ≤ γ) (hγ : γ < 1) : + (⌈log (1 - γ)⁻¹⌉₊ : ℝ) + 1 ≤ 2 * log (exp 1 / (1 - γ)) := by + have hu : 0 < 1 - γ := sub_pos.2 hγ + have hy : 0 ≤ log (1 - γ)⁻¹ := log_nonneg ((one_le_inv₀ hu).2 (by linarith)) + have h := Nat.ceil_lt_add_one hy + rw [log_div (exp_pos 1).ne' hu.ne', log_exp] + rw [log_inv] at h hy ⊢ + linarith + +/-- For `c, n, δ > 0` with `c n ≤ x`, `c exp (-log (x / δ)) ≤ δ / n`: if each of `n` bad events +has probability at most `c exp (-L)` at the confidence level `L = log (x / δ)`, their union has +probability at most `δ`. -/ +theorem mul_exp_neg_log_div_le {c x n δ : ℝ} (hc : 0 < c) (hn : 0 < n) (hδ : 0 < δ) + (h : c * n ≤ x) : c * exp (-log (x / δ)) ≤ δ / n := by + have hx : 0 < x := (mul_pos hc hn).trans_le h + rw [exp_neg, exp_log (div_pos hx hδ), inv_div, ← mul_div_assoc, div_le_div_iff₀ hx hn] + nlinarith + /-- If `r n = O(n ^ p)`, then `log (r n) ≤ ε n` for all large `n`, for every `ε > 0`. -/ theorem eventually_log_le_mul_of_isBigO {r : ℕ → ℝ} {p : ℝ} (hr : r =O[atTop] fun n ↦ (n : ℝ) ^ p) {ε : ℝ} (hε : 0 < ε) : diff --git a/LMLExplore/MarkovDecisionProcess/MarkovPolicy.lean b/LMLExplore/MarkovDecisionProcess/MarkovPolicy.lean index 8626ba79..808dce4c 100644 --- a/LMLExplore/MarkovDecisionProcess/MarkovPolicy.lean +++ b/LMLExplore/MarkovDecisionProcess/MarkovPolicy.lean @@ -34,7 +34,8 @@ policy `π`, these marginals are given by powers of two kernels: Integrating a function against `M.stateKernel π s` averages over the actions `a` of `π s` its integral against `M.P (s, a)` (`integral_stateKernel`, and `integral_stateKernel_eq_sum` for finitely many actions); integrating a function against `M.saKernel π p` integrates over `M.P p` -its average over the actions of `π` (`integral_saKernel`). +its average over the actions of `π` (`integral_saKernel`). The state kernel of a deterministic +stationary policy `d` is `s ↦ M.P (s, d s)` (`stateKernel_deterministic_apply`). The deterministic stationary policies `policyAlg π hπ` are Markov policies (`policyAlg_eq_markov`). @@ -123,6 +124,14 @@ lemma stateKernel_comp_eq_comp_compProd (μ : Measure 𝓢) [SFinite μ] : lemma stateKernel_apply (s : 𝓢) : M.stateKernel π s = M.P ∘ₘ (Measure.dirac s ⊗ₘ π) := by rw [← stateKernel_comp_eq_comp_compProd, Measure.dirac_bind (Kernel.measurable _)] +/-- The state kernel of the deterministic stationary policy `d` draws the next state from +`M.P (s, d s)`. -/ +@[simp] +lemma stateKernel_deterministic_apply {d : 𝓢 → 𝓐} (hd : Measurable d) (s : 𝓢) : + M.stateKernel (Kernel.deterministic d hd) s = M.P (s, d s) := by + rw [stateKernel_apply, Measure.compProd_deterministic, Measure.map_dirac' (by fun_prop), + Measure.dirac_bind M.P.measurable] + /-- Composing a measure `ν` on state-action pairs with the state-action kernel of `π` draws a next state from `M.P ∘ₘ ν`, then an action from `π`. -/ lemma saKernel_comp_eq_compProd (ν : Measure (𝓢 × 𝓐)) [SFinite ν] : diff --git a/LMLExplore/MarkovDecisionProcess/ReturnVariance.lean b/LMLExplore/MarkovDecisionProcess/ReturnVariance.lean index 4429f1a0..3f90185a 100644 --- a/LMLExplore/MarkovDecisionProcess/ReturnVariance.lean +++ b/LMLExplore/MarkovDecisionProcess/ReturnVariance.lean @@ -33,19 +33,24 @@ model. For a nonnegative reward `r_π`, the bound can be stated in terms of the value rather than of the rewards [LWCGC24, Lemma 11]: if `v^π ≤ B`, the resolvent of the state kernel `P_π` applied to the -standard deviations `√(Var_{P_π}(v^π))` is at most `B / (γ √(1 - γ))`. The theorems of this -file apply only to the value `v^π`. The values `V^(l) = R_γ(P_π) √(Var_{P_π}(V^(l-1)))` of the -successive standard deviations, with `V^(0) = v^π`, are not policy values; the generic form for a -Markov kernel, `ProbabilityTheory.Kernel.integral_sqrt_variance_integral_resolvent_le`, applied -with `f = √(Var_{P_π}(V^(l-2)))` (and `f = r_π` for `l = 1`), so that its resolvent is -`V = V^(l-1)`, bounds each `V^(l)` by `(γ √(1 - γ))⁻¹` times a bound on `V^(l-1)`. +standard deviations `√(Var_{P_π}(v^π))` is at most `B / (γ √(1 - γ))`. The values +`V^(l) = R_γ(P_π) √(Var_{P_π}(V^(l-1)))` of the successive standard deviations, with +`V^(0) = v^π`, are the levels `M.valueLevel γ π l` of [LWCGC24, Lemma 2]; they are not policy +values. The generic form for a Markov kernel, +`ProbabilityTheory.Kernel.integral_sqrt_variance_integral_resolvent_le`, applied with +`f = √(Var_{P_π}(V^(l-2)))` (and `f = r_π` for `l = 1`), so that its resolvent is `V = V^(l-1)`, +bounds each `V^(l)` by `(γ √(1 - γ))⁻¹` times a bound on `V^(l-1)` [LWCGC24, (73)]. This recursion is how [LWCGC24] evaluates a fixed policy with a generative model from sample -sizes of order `(1 - γ)⁻¹`. +sizes of order `(1 - γ)⁻¹`: if the state kernel `P'_π` of a second MDP `M'` with the same rewards +deviates from `P_π` on the first `m ≥ log (1 - γ)⁻¹` levels by a Bernstein-type bound, the values +of `π` in `M` and `M'` are close [LWCGC24, Lemmas 1 and 2]. ## Main definitions * `Learning.MDP.returnVariance M γ π`: the variance `Σ^π (s, a)` of the discounted return of the mean rewards along the state-action chain of `π` started at `(s, a)`. +* `Learning.MDP.valueLevel M γ π l`: the levels `V 0 = v^π` and + `V (l + 1) = R_γ(P_π) √Var_{P_π}(V l)` of [LWCGC24, Lemma 2] for a stationary policy `π`. ## Main statements @@ -64,6 +69,13 @@ sizes of order `(1 - γ)⁻¹`. `Learning.MDP.integral_sqrt_variance_value_stateKernel_resolvent_le`: for `r_π ≥ 0` and `v^π ≤ B`, `γ ^ 2 R_γ(P_π) Var_{P_π}(v^π) ≤ 2 B v^π - (v^π) ^ 2` and `R_γ(P_π) √(Var_{P_π}(v^π)) ≤ B / (γ √(1 - γ))` [LWCGC24, Lemma 11]. +* `Learning.MDP.valueLevel_mem_Icc`: with rewards in `[0, C]`, the level `l` is in + `[0, C / ((1 - γ) (γ √(1 - γ)) ^ l)]` [LWCGC24, (73)]. +* `Learning.MDP.abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le`: the deterministic part + of model-based policy evaluation [LWCGC24, Lemmas 1 and 2], for two MDPs with the same rewards, + with the deviations in the form given by Bernstein's inequality at a level `L` and `ε = 2 L / N`. + It is shared by `ReinforcementLearning/Generative/PolicyEvaluation.lean` [LWCGC24, Lemma 1] and + `ReinforcementLearning/Generative/LeaveOneOut.lean` [LWCGC24, Lemma 5]. ## References @@ -72,7 +84,8 @@ sizes of order `(1 - γ)⁻¹`. * [M. G. Azar, R. Munos and H. J. Kappen, *Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model*, 2013][AMK13] * [G. Li, Y. Wei, Y. Chi, Y. Gu and Y. Chen, *Breaking the sample size barrier in model-based - reinforcement learning with a generative model*, Operations Research, 2024][LWCGC24], Lemma 11 + reinforcement learning with a generative model*, Operations Research, 2024][LWCGC24], Lemmas 1, + 2 and 11 (arXiv:2005.12900) -/ public section @@ -259,3 +272,92 @@ theorem integral_sqrt_variance_value_stateKernel_resolvent_le (hγ₀ : 0 < γ) (abs_policyReward_le hR) hr hvB s end Learning.MDP + +/-! ### The levels of [LWCGC24, Lemma 2] -/ + +namespace Learning.MDP + +open Real (log) + +variable {𝓢 𝓐 : Type*} {m𝓢 : MeasurableSpace 𝓢} {m𝓐 : MeasurableSpace 𝓐} + +/-- The levels of [LWCGC24, Lemma 2] for a stationary policy `π`, with state kernel `P_π`: +`V 0 = R_γ(P_π) r_π`, which is the value `v^π` for bounded rewards and `γ < 1`, and +`V (l + 1) = R_γ(P_π) √Var_{P_π}(V l)`. -/ +noncomputable def valueLevel (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (π : Kernel 𝓢 𝓐) : ℕ → 𝓢 → ℝ + | 0, x => ∫ y, M.policyReward π y ∂(Kernel.resolvent γ (M.stateKernel π) x) + | l + 1, x => + ∫ y, √Var[valueLevel M γ π l; M.stateKernel π y] ∂(Kernel.resolvent γ (M.stateKernel π) x) + +@[simp] +lemma valueLevel_zero (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (π : Kernel 𝓢 𝓐) (x : 𝓢) : + M.valueLevel γ π 0 x = ∫ y, M.policyReward π y ∂(Kernel.resolvent γ (M.stateKernel π) x) := + (rfl) + +@[simp] +lemma valueLevel_succ (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (π : Kernel 𝓢 𝓐) (l : ℕ) (x : 𝓢) : + M.valueLevel γ π (l + 1) x = + ∫ y, √Var[M.valueLevel γ π l; M.stateKernel π y] ∂(Kernel.resolvent γ (M.stateKernel π) x) := + (rfl) + +/-- With rewards in `[0, C]` and `0 < γ < 1`, the level `l` of [LWCGC24, Lemma 2] for a stationary +policy is in `[0, C / ((1 - γ) (γ √(1 - γ)) ^ l)]` [LWCGC24, (73)]. -/ +lemma valueLevel_mem_Icc {M : MDP 𝓢 𝓐 ℝ} {γ : ℝ≥0} (hγ₀ : 0 < γ) (hγ : γ < 1) {C : ℝ} + (hR : ∀ p, ∀ᵐ x ∂(M.R p), x ∈ Set.Icc 0 C) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] (l : ℕ) + (x : 𝓢) : M.valueLevel γ π l x ∈ Set.Icc 0 (C / ((1 - γ) * (γ * √(1 - γ)) ^ l)) := + Kernel.mem_Icc_of_eq_integral_resolvent_sqrt_variance hγ₀ hγ measurable_policyReward + (fun y ↦ (policyReward_mem_Icc hR y).1) (fun y ↦ (policyReward_mem_Icc hR y).2) + (valueLevel_zero M γ π) (valueLevel_succ M γ π) l x + +/-- **The deterministic part of model-based policy evaluation** [LWCGC24, Lemmas 1 and 2]. Let +`M` and `M'` be MDPs with the same rewards, in `[0, C]`, `0 < γ < 1`, and `π` a stationary policy, +with state kernels `P_π` in `M` and `P'_π` in `M'`. Let `V = M.valueLevel γ π` be the levels +`V 0 = v^π` and `V (l + 1) = R_γ(P_π) √Var_{P_π}(V l)` of [LWCGC24, Lemma 2], bounded by +`b l = C / ((1 - γ) (γ √(1 - γ)) ^ l)`, and `log (1 - γ)⁻¹ ≤ m`. Let `L ≥ 0`, `N > 0` and +`18 L ≤ (1 - γ) N`. If `P'_π` deviates from `P_π` on the levels `l ≤ m` by the bound +`√(2 Var_{P_π}(V l) L / N) + b l L / (3 N)` of Bernstein's inequality at the level `L`, then the +value of `π` in `M'` satisfies `|v'^π - v^π| ≤ 3 C √(2 L / (N (1 - γ) ^ 3))`. + +This is `ProbabilityTheory.Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le` +with `ε = 2 L / N`, for the resolvent forms `v^π = R_γ(P_π) r_π` and `v'^π = R_γ(P'_π) r_π` of the +two values. -/ +theorem abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le {M M' : MDP 𝓢 𝓐 ℝ} + (hM' : M'.R = M.R) {γ : ℝ≥0} (hγ₀ : 0 < γ) (hγ : γ < 1) {C : ℝ} + (hR : ∀ p, ∀ᵐ x ∂(M.R p), x ∈ Set.Icc 0 C) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] {m : ℕ} + (hm : log (1 - (γ : ℝ))⁻¹ ≤ m) {N L : ℝ} (hN : 0 < N) (hL : 0 ≤ L) (hNL : 18 * L ≤ (1 - γ) * N) + (h : ∀ l ≤ m, ∀ x, + |∫ y, M.valueLevel γ π l y ∂(M'.stateKernel π x) - + ∫ y, M.valueLevel γ π l y ∂(M.stateKernel π x)| ≤ + √(2 * Var[M.valueLevel γ π l; M.stateKernel π x] * L / N) + + C / ((1 - γ) * (γ * √(1 - γ)) ^ l) * L / (3 * N)) (s : 𝓢) : + |M'.value γ π s - M.value γ π s| ≤ 3 * C * √(2 * L / (N * (1 - γ) ^ 3)) := by + have hRabs (p : 𝓢 × 𝓐) : ∀ᵐ x ∂(M.R p), |x| ≤ C := + (hR p).mono fun x hx ↦ (abs_of_nonneg hx.1).trans_le hx.2 + have hf (y : 𝓢) := policyReward_mem_Icc (π := π) hR y + -- both values are resolvents of the same reward `r_π` + have hfe : M'.policyReward π = M.policyReward π := + funext fun y ↦ by rw [policyReward_def, hM', policyReward_def] + rw [value_eq_integral_resolvent hγ (hM' ▸ hRabs), value_eq_integral_resolvent hγ hRabs, hfe] + -- Lemma 2 with `ε = 2 L / N`, for which `9 ε ≤ 1 - γ` + have hε9 : 9 * (2 * L / N) ≤ 1 - γ := by + rw [← mul_div_assoc, div_le_iff₀ hN] + linarith + refine (Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le + (M'.stateKernel π) hγ₀ hγ measurable_policyReward (fun y ↦ (hf y).1) (fun y ↦ (hf y).2) + (valueLevel_zero M γ π) (valueLevel_succ M γ π) hm (by positivity) hε9 + (fun l hl x ↦ (h l hl x).trans (add_le_add (le_of_eq ?_) ?_)) s).trans_eq ?_ + · congr 1 + ring + · -- the bound `b l` of the level `l` is nonnegative + have hb := valueLevel_mem_Icc hγ₀ hγ hR π l x + have hbL : 0 ≤ C / ((1 - γ) * (γ * √(1 - γ)) ^ l) * L / N := by + have := hb.1.trans hb.2 + positivity + calc C / ((1 - γ) * (γ * √(1 - γ)) ^ l) * L / (3 * N) + = C / ((1 - γ) * (γ * √(1 - γ)) ^ l) * L / N / 3 := by + rw [div_div, mul_comm (3 : ℝ)] + _ ≤ C / ((1 - γ) * (γ * √(1 - γ)) ^ l) * L / N * 2 := by linarith + _ = 2 * L / N * (C / ((1 - γ) * (γ * √(1 - γ)) ^ l)) := by ring + · rw [div_div] + +end Learning.MDP diff --git a/LMLExplore/MarkovDecisionProcess/Value.lean b/LMLExplore/MarkovDecisionProcess/Value.lean index 40a725ba..e683cd1a 100644 --- a/LMLExplore/MarkovDecisionProcess/Value.lean +++ b/LMLExplore/MarkovDecisionProcess/Value.lean @@ -92,6 +92,15 @@ lemma abs_policyReward_le [IsMarkovKernel π] (hR : ∀ p, ∀ᵐ x ∂(M.R p), |M.policyReward π s| ≤ C := abs_integral_le_of_abs_le fun a ↦ abs_meanReward_le hR (s, a) +/-- With rewards in `[0, C]`, the reward of a stationary policy is in `[0, C]`. -/ +lemma policyReward_mem_Icc [IsMarkovKernel π] (hR : ∀ p, ∀ᵐ x ∂(M.R p), x ∈ Set.Icc 0 C) + (s : 𝓢) : M.policyReward π s ∈ Set.Icc 0 C := + ⟨integral_nonneg fun a ↦ by + rw [meanReward_def] + exact integral_nonneg_of_ae ((hR _).mono fun _ hx ↦ hx.1), + (le_abs_self _).trans + (abs_policyReward_le (fun p ↦ (hR p).mono fun _ hx ↦ (abs_of_nonneg hx.1).trans_le hx.2) s)⟩ + /-- The reward of a deterministic stationary policy `d` is the mean reward of the action `d s`. -/ @[simp] lemma policyReward_deterministic {d : 𝓢 → 𝓐} (hd : Measurable d) (s : 𝓢) : @@ -131,6 +140,14 @@ lemma value_def (s : 𝓢) : M.value γ π s = ∑' n, (γ : ℝ) ^ n * ∫ s', M.policyReward π s' ∂((M.stateKernel π ^ n) s) := (rfl) +variable (M π) in +/-- For `γ = 0`, the value of a stationary policy is its reward: `v^π = r_π`. -/ +@[simp] +lemma value_zero [IsSFiniteKernel π] (s : 𝓢) : M.value 0 π s = M.policyReward π s := by + rw [value_def, tsum_eq_single 0 fun n hn ↦ by simp [hn]] + simp [Kernel.one_def, Kernel.id_apply, + integral_dirac' _ _ measurable_policyReward.stronglyMeasurable] + section Value variable [IsMarkovKernel π] diff --git a/LMLExplore/ReinforcementLearning/Generative/Basic.lean b/LMLExplore/ReinforcementLearning/Generative/Basic.lean index c7fce83c..1a1625a4 100644 --- a/LMLExplore/ReinforcementLearning/Generative/Basic.lean +++ b/LMLExplore/ReinforcementLearning/Generative/Basic.lean @@ -109,6 +109,12 @@ lemma empirical_congr (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] {ω ω' : MDP.ext (by rw [empirical_P, empirical_P, empiricalKernel_congr h]) (by rw [empirical_R, empirical_R]) +/-- For `γ = 0`, the value of a stationary policy in the empirical MDP is its value in `M`: both +are its reward. -/ +lemma value_empirical_zero (M : MDP 𝓢 𝓐 ℝ) (N : ℕ) [NeZero N] (ω : ℕ → 𝓢 × 𝓐 → 𝓢) + (π : Kernel 𝓢 𝓐) [IsSFiniteKernel π] : (M.empirical N ω).value 0 π = M.value 0 π := + funext fun s ↦ by rw [value_zero, value_zero, policyReward_def, empirical_R, policyReward_def] + /-- For finite state and action spaces, every function of the empirical MDP is a measurable function of the array of samples: the empirical MDP only depends on the finitely many samples `ω i p`, `i < N`, which take finitely many values. -/ diff --git a/LMLExplore/ReinforcementLearning/Generative/Decoupling.lean b/LMLExplore/ReinforcementLearning/Generative/Decoupling.lean index a1a38dd8..1c0c8f2f 100644 --- a/LMLExplore/ReinforcementLearning/Generative/Decoupling.lean +++ b/LMLExplore/ReinforcementLearning/Generative/Decoupling.lean @@ -6,7 +6,9 @@ Authors: LMLExplore contributors module public import LMLExplore.MarkovDecisionProcess.Absorbing.Basic +public import LMLExplore.MarkovDecisionProcess.Absorbing.StateAction public import LMLExplore.ReinforcementLearning.Generative.Basic +import LMLExplore.Analysis.SpecialFunctions.Log.Basic import LMLExplore.Probability.Moments.Variance import LMLExplore.SequentialLearning.SumRewards import LMLExplore.Topology.UnitInterval @@ -49,11 +51,22 @@ difference, where [AKY20] uses its sup norm; this only changes the absolute cons ## Main statements +* `Learning.MDP.indepFun_comp_redirect_empirical`: every function of the redirection of the + empirical MDP on a set `S` of pairs is independent of the samples of each pair of `S`. * `Learning.MDP.indepFun_comp_absorbing_empirical`: every function of the `s`-absorbing modification of the empirical MDP is independent of the samples of `(s, a)`. +* `Learning.MDP.indepFun_comp_saAbsorbing_empirical`: every function of the `p`-absorbing + modification of the empirical MDP (`MarkovDecisionProcess/Absorbing/StateAction.lean`) is + independent of the samples of `p`, the leave-one-out decoupling of [LWCGC24, §6.3.2]. +* `Learning.MDP.measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_redirect_le`: + Bernstein's inequality at each pair of `S` for the functions of the redirections of the + empirical MDP on `S`. * `Learning.MDP.measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_absorbing_le`: Bernstein's inequality for the values of the absorbing modifications of the empirical MDP [AKY20, Lemma 6]. +* `measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_saAbsorbing_le` (in + `Learning.MDP`): Bernstein's inequality at `p` for the functions of the `p`-absorbing + modifications of the empirical MDP [LWCGC24, (92)]. * `le_streamMeasure_forall_abs_integral_optValue_empirical_sub_integral_optValue_empirical_le` and `le_streamMeasure_forall_abs_integral_value_empirical_sub_integral_value_empirical_le` (in `Learning.MDP`): the Bernstein-type bounds for the optimal value of the empirical MDP and for @@ -63,6 +76,9 @@ difference, where [AKY20] uses its sup norm; this only changes the absolute cons * [A. Agarwal, S. Kakade and L. F. Yang, *Model-based reinforcement learning with a generative model is minimax optimal*, COLT 2020][AKY20], §4.2 +* [G. Li, Y. Wei, Y. Chi, Y. Gu and Y. Chen, *Breaking the sample size barrier in model-based + reinforcement learning with a generative model*, Operations Research, 2024][LWCGC24], §6.3.2 + and (92) (arXiv:2005.12900) -/ public section @@ -80,38 +96,81 @@ section Decoupling variable [Finite 𝓢] [Finite 𝓐] -/-- **Decoupling** [AKY20, §4.2]. Under the generative model of `M`, every function of the -`s`-absorbing modification of the empirical MDP is independent of the samples of the pair -`(s, a)`: the modification is computed from the samples of the pairs at the other states. -/ -theorem indepFun_comp_absorbing_empirical (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] {β : Type*} - [MeasurableSpace β] (F : MDP 𝓢 𝓐 𝓡 → β) (s : 𝓢) (c : 𝓡) (a : 𝓐) : - IndepFun (fun ω ↦ F ((M.empirical N ω).absorbing s c)) (fun ω i ↦ ω i (s, a)) +/-- **Decoupling**. Under the generative model of `M`, every function of the redirection of the +empirical MDP on a measurable set `S` of pairs is independent of the samples of every pair +`p ∈ S`: the redirection is computed from the samples of the pairs outside `S`. -/ +theorem indepFun_comp_redirect_empirical (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] {β : Type*} + [MeasurableSpace β] (F : MDP 𝓢 𝓐 𝓡 → β) {S : Set (𝓢 × 𝓐)} (hS : MeasurableSet S) (s : 𝓢) + (c : 𝓡) {p : 𝓢 × 𝓐} (hp : p ∈ S) : + IndepFun (fun ω ↦ F ((M.empirical N ω).redirect hS s c)) (fun ω i ↦ ω i p) (streamMeasure M.P) := by classical - -- the sample sequences of the pairs at the other states are independent of those of `(s, a)` - have h := (iIndepFun_arm_streamMeasure M.P).indepFun_set {p | p.1 ≠ s} {(s, a)} - (Set.disjoint_singleton_right.2 fun h ↦ h rfl) fun p ↦ by fun_prop - -- the array with the samples of the pairs at the other states, and `s` at the pairs at `s` - let ext : ({p : 𝓢 × 𝓐 | p.1 ≠ s} → ℕ → 𝓢) → ℕ → 𝓢 × 𝓐 → 𝓢 := - fun x i p ↦ if hp : p.1 ≠ s then x ⟨p, hp⟩ i else s + -- the sample sequences of the pairs outside `S` are independent of those of `p` + have h := (iIndepFun_arm_streamMeasure M.P).indepFun_set {q | q ∉ S} {p} + (Set.disjoint_singleton_right.2 fun h ↦ h hp) fun q ↦ by fun_prop + -- the array with the samples of the pairs outside `S`, and `s` at the pairs of `S` + let ext : ({q : 𝓢 × 𝓐 | q ∉ S} → ℕ → 𝓢) → ℕ → 𝓢 × 𝓐 → 𝓢 := + fun x i q ↦ if hq : q ∉ S then x ⟨q, hq⟩ i else s have h_ext : Measurable ext := by - refine Measurable.of_eval fun i ↦ Measurable.of_eval fun p ↦ ?_ - by_cases hp : p.1 ≠ s - · have h₁ : (fun x ↦ ext x i p) = fun x ↦ x ⟨p, hp⟩ i := funext fun x ↦ by simp [ext, hp] + refine Measurable.of_eval fun i ↦ Measurable.of_eval fun q ↦ ?_ + by_cases hq : q ∉ S + · have h₁ : (fun x ↦ ext x i q) = fun x ↦ x ⟨q, hq⟩ i := funext fun x ↦ by simp [ext, hq] rw [h₁] fun_prop - · simp [ext, not_not.1 hp] - have h_eq : (fun ω ↦ F ((M.empirical N ω).absorbing s c)) = - (fun x ↦ F ((M.empirical N (ext x)).absorbing s c)) ∘ fun ω p i ↦ ω i p := by + · simp [ext, not_not.1 hq] + have h_eq : (fun ω ↦ F ((M.empirical N ω).redirect hS s c)) = + (fun x ↦ F ((M.empirical N (ext x)).redirect hS s c)) ∘ fun ω q i ↦ ω i q := by ext ω simp only [Function.comp_apply] congr 1 - refine absorbing_congr c (fun p hp ↦ ?_) fun p _ ↦ by simp + refine redirect_congr hS c (fun q hq ↦ ?_) fun q _ ↦ by simp simp only [empirical_P] - exact empiricalKernel_apply_congr fun i _ ↦ by simp [ext, hp] + exact empiricalKernel_apply_congr fun i _ ↦ by simp [ext, hq] rw [h_eq] - exact h.comp ((measurable_comp_empirical M N fun M' ↦ F (M'.absorbing s c)).comp h_ext) - (measurable_pi_apply ⟨(s, a), Set.mem_singleton _⟩) + exact h.comp ((measurable_comp_empirical M N fun M' ↦ F (M'.redirect hS s c)).comp h_ext) + (measurable_pi_apply ⟨p, Set.mem_singleton _⟩) + +/-- **Decoupling** [AKY20, §4.2]. Under the generative model of `M`, every function of the +`s`-absorbing modification of the empirical MDP is independent of the samples of the pair +`(s, a)`: the modification is computed from the samples of the pairs at the other states. -/ +theorem indepFun_comp_absorbing_empirical (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] {β : Type*} + [MeasurableSpace β] (F : MDP 𝓢 𝓐 𝓡 → β) (s : 𝓢) (c : 𝓡) (a : 𝓐) : + IndepFun (fun ω ↦ F ((M.empirical N ω).absorbing s c)) (fun ω i ↦ ω i (s, a)) + (streamMeasure M.P) := by + simp_rw [absorbing_def] + exact indepFun_comp_redirect_empirical M N F _ s c (p := (s, a)) (Set.mem_singleton s) + +/-- **Leave-one-out decoupling** [LWCGC24, §6.3.2]. Under the generative model of `M`, every +function of the `p`-absorbing modification of the empirical MDP is independent of the samples of +the pair `p`: the modification is computed from the samples of the other pairs. -/ +theorem indepFun_comp_saAbsorbing_empirical (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] {β : Type*} + [MeasurableSpace β] (F : MDP 𝓢 𝓐 𝓡 → β) (p : 𝓢 × 𝓐) (c : 𝓡) : + IndepFun (fun ω ↦ F ((M.empirical N ω).saAbsorbing p c)) (fun ω i ↦ ω i p) + (streamMeasure M.P) := by + simp_rw [saAbsorbing_def] + exact indepFun_comp_redirect_empirical M N F _ p.1 c (Set.mem_singleton p) + +/-- **Bernstein's inequality for the redirections of the empirical MDP.** Under the generative +model of `M`, let `G M'` be a function on the states computed from an MDP `M'`, with values in +`[l, u]`, `l < u`, at the redirections to `s` with reward `c` of the empirical MDPs on a +measurable set `S` of pairs. For `N ≠ 0`, every pair `p ∈ S` and every `x`, the one-step +prediction error `|∫ v dP p - ∫ v dP̂ p|` of `v = G ((M.empirical N ω).redirect hS s c)` is at +least `√(2 Var_{P p}(v) x / N) + (u - l) x / (3 N)` with probability at most `2 exp (-x)`. -/ +theorem measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_redirect_le + (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] (G : MDP 𝓢 𝓐 𝓡 → 𝓢 → ℝ) {l u : ℝ} (hlu : l < u) + {S : Set (𝓢 × 𝓐)} (hS : MeasurableSet S) (s : 𝓢) (c : 𝓡) + (hG : ∀ ω s', G ((M.empirical N ω).redirect hS s c) s' ∈ Set.Icc l u) {p : 𝓢 × 𝓐} + (hp : p ∈ S) (x : ℝ) : + (streamMeasure M.P).real {ω | + √(2 * Var[G ((M.empirical N ω).redirect hS s c); M.P p] * x / N) + + (u - l) * x / (3 * N) ≤ + |∫ s', G ((M.empirical N ω).redirect hS s c) s' ∂(M.P p) - + ∫ s', G ((M.empirical N ω).redirect hS s c) s' ∂((M.empirical N ω).P p)|} ≤ + 2 * exp (-x) := by + simpa only [empirical_P] using + measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empiricalKernel_le_of_indepFun M.P + (measurable_comp_empirical M N fun M' ↦ G (M'.redirect hS s c)) + (indepFun_comp_redirect_empirical M N G hS s c hp) hlu hG N x /-- **Bernstein's inequality for the absorbing modifications of the empirical MDP** [AKY20, Lemma 6]. Under the generative model of `M`, let `G M'` be a function on the states computed from @@ -130,26 +189,32 @@ theorem measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_abs |∫ s', G ((M.empirical N ω).absorbing s c) s' ∂(M.P (s, a)) - ∫ s', G ((M.empirical N ω).absorbing s c) s' ∂((M.empirical N ω).P (s, a))|} ≤ 2 * exp (-x) := by - simpa only [empirical_P] using - measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empiricalKernel_le_of_indepFun M.P - (measurable_comp_empirical M N fun M' ↦ G (M'.absorbing s c)) - (indepFun_comp_absorbing_empirical M N G s c a) hlu hG N x + simp_rw [absorbing_def] at hG ⊢ + exact measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_redirect_le M N G hlu + _ s c hG (p := (s, a)) (Set.mem_singleton s) x -end Decoupling +/-- **Bernstein's inequality for the state-action absorbing modifications of the empirical MDP** +[LWCGC24, (92)]. Under the generative model of `M`, let `G M'` be a function on the states +computed from an MDP `M'` (for instance a value of its greedy optimal policy), with values in +`[l, u]`, `l < u`, at the `p`-absorbing modifications of the empirical MDPs with reward `c`. For +`N ≠ 0` and every `x`, the one-step prediction error `|∫ v dP p - ∫ v dP̂ p|` of +`v = G ((M.empirical N ω).saAbsorbing p c)` is at least +`√(2 Var_{P p}(v) x / N) + (u - l) x / (3 N)` with probability at most `2 exp (-x)`. -/ +theorem measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_saAbsorbing_le + (M : MDP 𝓢 𝓐 𝓡) (N : ℕ) [NeZero N] (G : MDP 𝓢 𝓐 𝓡 → 𝓢 → ℝ) {l u : ℝ} (hlu : l < u) + (p : 𝓢 × 𝓐) (c : 𝓡) (hG : ∀ ω s', G ((M.empirical N ω).saAbsorbing p c) s' ∈ Set.Icc l u) + (x : ℝ) : + (streamMeasure M.P).real {ω | + √(2 * Var[G ((M.empirical N ω).saAbsorbing p c); M.P p] * x / N) + + (u - l) * x / (3 * N) ≤ + |∫ s', G ((M.empirical N ω).saAbsorbing p c) s' ∂(M.P p) - + ∫ s', G ((M.empirical N ω).saAbsorbing p c) s' ∂((M.empirical N ω).P p)|} ≤ + 2 * exp (-x) := by + simp_rw [saAbsorbing_def] at hG ⊢ + exact measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_redirect_le M N G hlu + _ p.1 c hG (Set.mem_singleton p) x -/-- The confidence count of [AKY20, Lemma 9]: for `θ ^ 2 (K + 1) ≤ 3`, the probability -`2 exp (-L)` of each bad event of the Bernstein inequality at the level -`L = log (12 S A / (θ ^ 2 δ))` is at most `δ / 2` divided by the number `S A (K + 1)` of pairs and -points of the net. -/ -private lemma two_mul_exp_neg_log_le {S A K θ δ : ℝ} (hS : 0 < S) (hA : 0 < A) (hK : 0 ≤ K) - (hθ : 0 < θ) (hδ : 0 < δ) (hθK : θ ^ 2 * (K + 1) ≤ 3) : - 2 * Real.exp (-log (12 * S * A / (θ ^ 2 * δ))) ≤ δ / 2 / (S * (A * (K + 1))) := by - rw [Real.exp_neg, Real.exp_log (by positivity), inv_div, div_div, le_div_iff₀ (by positivity)] - calc 2 * (θ ^ 2 * δ / (12 * S * A)) * (2 * (S * (A * (K + 1)))) = θ ^ 2 * (K + 1) * δ / 3 := by - field_simp - ring - _ ≤ 3 * δ / 3 := by gcongr - _ = δ := by ring +end Decoupling /-- The numerical step of [AKY20, Lemma 9]: with `r = √(2 L / N)` and `Λ ≤ r`, the error terms `(2 + r) 2 γ C Λ + 2 C L / (3 (1 - γ) N)` of the approximation by the net and of Bernstein's @@ -283,7 +348,12 @@ private theorem le_streamMeasure_forall_abs_integral_sub_le_of_absorbing {M : MD refine (measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_absorbing_le M N G (neg_lt_self hB) i.1 _ (fun ω ↦ hWb ω i.1 i.2.2) i.2.1 L).trans ?_ simp only [Fintype.card_prod, Fintype.card_fin, Nat.cast_mul, Nat.cast_add, Nat.cast_one] - exact two_mul_exp_neg_log_le (by positivity) (by positivity) (Nat.cast_nonneg K) hθ₀ hδ hK₂ + rw [div_div, show L = log (12 * S * A / θ ^ 2 / δ) by rw [div_div]] + refine Real.mul_exp_neg_log_div_le two_pos (by positivity) hδ + ((le_div_iff₀ (by positivity)).2 ?_) + calc 2 * (2 * (S * (A * (K + 1)))) * θ ^ 2 = 4 * S * A * (θ ^ 2 * (K + 1)) := by ring + _ ≤ 4 * S * A * 3 := by gcongr + _ = 12 * S * A := by ring have h_good : 1 - δ / 2 ≤ μ.real (⋃ i, bad i)ᶜ := one_sub_le_measureReal_compl_iUnion (by positivity) h_bad -- the crude event is measurable, and both events hold with probability at least `1 - δ` diff --git a/LMLExplore/ReinforcementLearning/Generative/LeaveOneOut.lean b/LMLExplore/ReinforcementLearning/Generative/LeaveOneOut.lean new file mode 100644 index 00000000..2f42910a --- /dev/null +++ b/LMLExplore/ReinforcementLearning/Generative/LeaveOneOut.lean @@ -0,0 +1,330 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.ReinforcementLearning.Generative.Decoupling +public import LMLExplore.ReinforcementLearning.Generative.PolicyEvaluation +import LMLExplore.Analysis.SpecialFunctions.Log.Basic + +/-! +# Planning with a generative model: leave-one-out evaluation of the separated plug-in policy + +Let `M` be an MDP with `S` states, `A` actions and rewards in `[0, C]`, `γ < 1`, and +`M̂ = M.empirical N ω` the empirical MDP of `N` samples per state-action pair under the generative +model `Bandits.streamMeasure M.P`. The plug-in policy `π̂` is the greedy optimal policy of `M̂`. It +depends on all the samples, so that the evaluation bound of +`ReinforcementLearning/Generative/PolicyEvaluation.lean` [LWCGC24, Lemma 1], which needs a policy +fixed independently of the data, does not apply to it directly. + +Li, Wei, Chi, Gu and Chen [LWCGC24, Lemma 5] remove this dependence when the optimal action values +of `M̂` are *separated* by `η > 0`: at every state `s`, every action `a ≠ π̂ s` has +`Q̂* (s, a) + η ≤ Q̂* (s, π̂ s)` (the event `B_η` of [LWCGC24, (41)]). Their leave-one-out argument +runs through the state-action absorbing modifications `M̂.saAbsorbing p c` +(`MarkovDecisionProcess/Absorbing/StateAction.lean`): +* the modification at `p` is computed from the samples of the pairs other than `p`, so that every + function of it, such as its greedy optimal policy, is independent of the samples of `p` + (`Learning.MDP.indepFun_comp_saAbsorbing_empirical` in + `ReinforcementLearning/Generative/Decoupling.lean`), and Bernstein's inequality applies at `p` + to every function of the modification; +* under the separation, a uniform grid of rewards `c`, fixed in advance, contains one whose + modification at `p` has the greedy optimal policy `π̂` [LWCGC24, Lemma 4]. + +A union bound over the pairs `p`, the points of the grid and the levels of [LWCGC24, Lemma 2], +`ProbabilityTheory.Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le`, then +gives the Bernstein-type deviations of the empirical state kernel of `π̂` that Lemma 2 needs, in +the form of `Learning.MDP.abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le`. +With `K + 1` grid points, `8 (1 + γ) C / (1 - γ) ≤ (1 - γ) η K`, `δ > 0` and +`L = log (4 S A (K + 1) log (e / (1 - γ)) / δ)`, as soon as `18 L ≤ (1 - γ) N`, with probability +at least `1 - δ`, if `M̂` is separated by `η`, then + +`|v̂^π̂ - v^π̂| ≤ 3 C √(2 L / (N (1 - γ) ^ 3))`. + +Combined with [LWCGC24, Lemma 1] for the greedy optimal policy of `M`, which does not depend on the +samples, and with the optimality of `π̂` in `M̂`, this bounds the suboptimality of the plug-in +policy: with probability at least `1 - δ`, if `M̂` is separated by `η`, then +`v* - v^π̂ ≤ 6 C √(2 L' / (N (1 - γ) ^ 3))`, with `L' = log (8 S A (K + 1) log (e / (1 - γ)) / δ)` +the level of the first bound at `δ / 2`. + +[LWCGC24, Lemma 5] assumes that the separation holds with probability at least `1 - δ` and +concludes with probability at least `1 - 3 δ`. The statements here hold on the separation event, +whatever its probability, so that they combine with any tie-breaking argument. + +The grid size only enters through `log (K + 1)`: for `η` polynomially small in `S`, `A`, +`1 - γ` and `δ`, as produced by the random perturbation of the rewards of [LWCGC24, Lemma 6] +(`MarkovDecisionProcess/TieBreaking.lean`), the bound is of order `√(L / (N (1 - γ) ^ 3))` with a +logarithmic `L`, over the full range of sample sizes `N ≳ L / (1 - γ)`. + +## Main statements + +* `Learning.MDP.le_streamMeasure_forall_abs_value_empirical_sub_value_le_of_separated`: the + evaluation of the separated plug-in policy [LWCGC24, Lemma 5, first claim]. +* `Learning.MDP.le_streamMeasure_forall_optValue_sub_value_le_of_separated`: the suboptimality of + the separated plug-in policy [LWCGC24, Lemma 5, second claim]. + +## References + +* [G. Li, Y. Wei, Y. Chi, Y. Gu and Y. Chen, *Breaking the sample size barrier in model-based + reinforcement learning with a generative model*, Operations Research, 2024][LWCGC24], §6.3.2, + Lemma 5 and its proof in Appendix B.4 (arXiv:2005.12900) +-/ + +public section + +open MeasureTheory ProbabilityTheory LMLExplore Learning Bandits +open Real (log exp) +open scoped NNReal + +namespace Learning.MDP + +variable {𝓢 𝓐 𝓡 : Type*} {m𝓢 : MeasurableSpace 𝓢} {m𝓐 : MeasurableSpace 𝓐} + {m𝓡 : MeasurableSpace 𝓡} [MeasurableSingletonClass 𝓢] [MeasurableSingletonClass 𝓐] + +section Generative + +variable [Fintype 𝓢] [Fintype 𝓐] [Nonempty 𝓢] [Nonempty 𝓐] + +/-- **Evaluation of the separated plug-in policy** [LWCGC24, Lemma 5, first claim]. Under the +generative model of an MDP `M` with `S` states, `A` actions and rewards in `[0, C]`, let `γ < 1`, +`η > 0`, `K > 0` with `8 (1 + γ) C / (1 - γ) ≤ (1 - γ) η K`, `δ > 0` and +`L = log (4 S A (K + 1) log (e / (1 - γ)) / δ)`. If `18 L ≤ (1 - γ) N`, then with probability at +least `1 - δ`, whenever the optimal action values of the empirical MDP `M̂ = M.empirical N ω` are +separated by `η` at its greedy optimal policy `π̂` (`Q̂* (s, a) + η ≤ Q̂* (s, π̂ s)` for every +`a ≠ π̂ s`), the value of `π̂` in `M̂` satisfies `|v̂^π̂ - v^π̂| ≤ 3 C √(2 L / (N (1 - γ) ^ 3))` at +every state. + +For rewards in `[0, 1]`, [LWCGC24] uses the grid of spacing `(1 - γ) η / 4` on +`[-1 / (1 - γ), 1 / (1 - γ)]`, with `K ≤ 8 / ((1 - γ) ^ 2 η)`, assumes +`N ≥ 16 e ^ 2 β₁ / (1 - γ)` for the corresponding `β₁ = 2 L`, and proves the bound with the +constant `6` in place of `3`; the constant `3` comes from the constant `1` of +`ProbabilityTheory.Kernel.integral_sqrt_variance_integral_resolvent_le`. -/ +theorem le_streamMeasure_forall_abs_value_empirical_sub_value_le_of_separated {M : MDP 𝓢 𝓐 ℝ} + {γ : ℝ≥0} (hγ : γ < 1) {C : ℝ} (hR : ∀ p, ∀ᵐ x ∂(M.R p), x ∈ Set.Icc 0 C) {η : ℝ} + (hη : 0 < η) {K : ℕ} (hK : 0 < K) (hKη : 8 * ((1 + γ) * C / (1 - γ)) ≤ (1 - γ) * η * K) + (N : ℕ) [NeZero N] {δ : ℝ} (hδ : 0 < δ) + (hN : 18 * log (4 * Fintype.card 𝓢 * Fintype.card 𝓐 * (K + 1) * log (exp 1 / (1 - γ)) / δ) ≤ + (1 - γ) * N) : + 1 - δ ≤ (streamMeasure M.P).real {ω | + (∀ s a, a ≠ (M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ) s → + (M.empirical N ω).optQValue γ (s, a) + η ≤ + (M.empirical N ω).optQValue γ + (s, (M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ) s)) → + ∀ s, |(M.empirical N ω).value γ (Kernel.deterministic + ((M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ)) + (measurable_of_finite _)) s - + M.value γ (Kernel.deterministic + ((M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ)) + (measurable_of_finite _)) s| ≤ + 3 * C * √(2 * log (4 * Fintype.card 𝓢 * Fintype.card 𝓐 * (K + 1) * + log (exp 1 / (1 - γ)) / δ) / (N * (1 - γ) ^ 3))} := by + -- For every pair `p`, point `k` of the grid and level `l ≤ m = ⌈log (1 - γ)⁻¹⌉₊`, Bernstein's + -- inequality at `p` holds for the `l`-th level `V d l` of [LWCGC24, Lemma 2] of the greedy + -- optimal policy `d` of the `p`-absorbing modification with the `k`-th reward of the grid, which + -- is independent of the samples of `p`. Under the separation, at `p = (s, π̂ s)` one of these + -- policies is `π̂` [LWCGC24, Lemma 4], so that the deviations of the empirical state kernel of + -- `π̂` needed by [LWCGC24, Lemma 2] hold at every state. + rcases le_or_gt 1 δ with hδ1 | hδ1 + · exact (sub_nonpos.2 hδ1).trans measureReal_nonneg + have hN₀ : (0 : ℝ) < N := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne N) + have hu : 0 < 1 - (γ : ℝ) := sub_pos.2 hγ + have hRabs (p : 𝓢 × 𝓐) : ∀ᵐ x ∂(M.R p), |x| ≤ C := + (hR p).mono fun x hx ↦ (abs_of_nonneg hx.1).trans_le hx.2 + have hRe (ω : ℕ → 𝓢 × 𝓐 → 𝓢) : ∀ p, ∀ᵐ x ∂((M.empirical N ω).R p), |x| ≤ C := by + simpa using hRabs + have hC : 0 ≤ C := (abs_nonneg _).trans (abs_meanReward_le hRabs (Classical.arbitrary _)) + -- for `C = 0` all the values vanish, and for `γ = 0` both values are the reward + rcases hC.eq_or_lt with rfl | hC₀ + · refine le_trans ?_ (measureReal_mono (s₁ := Set.univ) (fun ω _ _ s ↦ ?_) (measure_ne_top _ _)) + · rw [probReal_univ] + linarith + · have h₁ := abs_value_le (π := Kernel.deterministic + ((M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ)) (measurable_of_finite _)) + hγ (hRe ω) s + have h₂ := abs_value_le (π := Kernel.deterministic + ((M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ)) (measurable_of_finite _)) + hγ hRabs s + rw [zero_div] at h₁ h₂ + rw [mul_zero, zero_mul] + exact (abs_sub _ _).trans (by linarith) + rcases eq_or_ne γ 0 with rfl | hγ₀ + · refine le_trans ?_ (measureReal_mono (s₁ := Set.univ) (fun ω _ _ s ↦ ?_) (measure_ne_top _ _)) + · rw [probReal_univ] + linarith + · rw [value_empirical_zero, sub_self, abs_zero] + positivity + have hγ₀' : 0 < γ := pos_iff_ne_zero.2 hγ₀ + -- the confidence level `L` and the number `m` of levels + set S : ℝ := (Fintype.card 𝓢 : ℝ) + set A : ℝ := (Fintype.card 𝓐 : ℝ) + set lg : ℝ := log (exp 1 / (1 - γ)) + set L := log (4 * S * A * (K + 1) * lg / δ) + set m := ⌈log (1 - (γ : ℝ))⁻¹⌉₊ + have hm' : (m : ℝ) + 1 ≤ 2 * lg := Real.natCeil_log_inv_one_sub_add_one_le γ.coe_nonneg hγ + have hS : 1 ≤ S := Nat.one_le_cast.2 Fintype.card_pos + have hA : 1 ≤ A := Nat.one_le_cast.2 Fintype.card_pos + have hK₁ : (1 : ℝ) ≤ K + 1 := by linarith [(Nat.cast_nonneg K : (0 : ℝ) ≤ K)] + have hlg1 : 1 ≤ 2 * lg := by linarith [(Nat.cast_nonneg m : (0 : ℝ) ≤ m)] + have hL : 0 ≤ L := Real.log_nonneg (by + rw [le_div_iff₀ hδ, one_mul] + have h₁ : 1 ≤ S * A * (K + 1) := + one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le hS hA) hK₁ + nlinarith) + -- the levels `V d l` of a deterministic policy `d` and their bounds `b l` + set V : (𝓢 → 𝓐) → ℕ → 𝓢 → ℝ := fun d ↦ + M.valueLevel γ (Kernel.deterministic d (measurable_of_finite d)) with hV_def + set b : ℕ → ℝ := fun l ↦ C / ((1 - γ) * (γ * √(1 - γ)) ^ l) + have hbpos (l : ℕ) : 0 < b l := + div_pos hC₀ (mul_pos hu (pow_pos (mul_pos (NNReal.coe_pos.2 hγ₀') (Real.sqrt_pos.2 hu)) _)) + have hVb (d : 𝓢 → 𝓐) : ∀ l y, V d l y ∈ Set.Icc 0 (b l) := valueLevel_mem_Icc hγ₀' hγ hR _ + -- the grid of rewards on `[-B, B]`, with `B` bounding `Q̂* (s, a) - γ v̂* s` + set B := (1 + γ) * C / (1 - γ) + -- the levels of the greedy optimal policies of the absorbing modifications on the grid + set W : (𝓢 × 𝓐) × Fin (K + 1) × Fin (m + 1) → MDP 𝓢 𝓐 ℝ → 𝓢 → ℝ := fun i M' ↦ + V ((M'.saAbsorbing i.1 (-B + 2 * B * (i.2.1 : ℕ) / K)).greedy γ + ((M'.saAbsorbing i.1 (-B + 2 * B * (i.2.1 : ℕ) / K)).optValue γ)) i.2.2 with hW_def + -- the bad events: Bernstein's inequality fails for one of them + set bad : (𝓢 × 𝓐) × Fin (K + 1) × Fin (m + 1) → Set (ℕ → 𝓢 × 𝓐 → 𝓢) := fun i ↦ {ω | + √(2 * Var[W i (M.empirical N ω); M.P i.1] * L / N) + (b i.2.2 - 0) * L / (3 * N) ≤ + |∫ s', W i (M.empirical N ω) s' ∂(M.P i.1) - + ∫ s', W i (M.empirical N ω) s' ∂((M.empirical N ω).P i.1)|} with hbad_def + have h_bad (i : (𝓢 × 𝓐) × Fin (K + 1) × Fin (m + 1)) : + (streamMeasure M.P).real (bad i) ≤ + δ / Fintype.card ((𝓢 × 𝓐) × Fin (K + 1) × Fin (m + 1)) := by + refine (measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_saAbsorbing_le M N + (fun M'' ↦ V (M''.greedy γ (M''.optValue γ)) i.2.2) (hbpos i.2.2) i.1 _ + (fun ω s' ↦ hVb _ _ _) L).trans ?_ + simp only [Fintype.card_prod, Fintype.card_fin, Nat.cast_mul, Nat.cast_add, Nat.cast_one] + refine Real.mul_exp_neg_log_div_le two_pos (by positivity) hδ ?_ + calc 2 * (S * A * ((K + 1) * ((m : ℝ) + 1))) = 2 * S * A * (K + 1) * ((m : ℝ) + 1) := by ring + _ ≤ 2 * S * A * (K + 1) * (2 * lg) := by gcongr + _ = 4 * S * A * (K + 1) * lg := by ring + -- outside the bad events, the deterministic part applies to `π̂` + refine (one_sub_le_measureReal_compl_iUnion hδ.le h_bad).trans + (measureReal_mono fun ω hω ↦ ?_) + simp only [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hω + intro hsep x + set g := (M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ) + refine abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le (empirical_R M N ω) hγ₀' hγ hR + _ (Nat.le_ceil _) hN₀ hL hN (fun l hl y ↦ ?_) x + -- `g` is the greedy optimal policy of a modification at `(y, g y)` on the grid + obtain ⟨k, hk⟩ := exists_greedy_optValue_saAbsorbing_eq (p := (y, g y)) hγ (hRe ω) hη hsep + (abs_optQValue_sub_mul_optValue_le hγ (hRe ω) _) hK hKη + have h := hω ((y, g y), k, ⟨l, Nat.lt_succ_of_le hl⟩) + simp only [hbad_def, hW_def, Set.mem_ofPred_eq, not_le, sub_zero] at h + rw [hk] at h + rw [stateKernel_deterministic_apply, stateKernel_deterministic_apply, abs_sub_comm] + exact h.le + +/-- **Suboptimality of the separated plug-in policy** [LWCGC24, Lemma 5, second claim]. Under the +generative model of an MDP `M` with `S` states, `A` actions and rewards in `[0, C]`, let `γ < 1`, +`η > 0`, `K > 0` with `8 (1 + γ) C / (1 - γ) ≤ (1 - γ) η K`, `δ > 0` and +`L = log (8 S A (K + 1) log (e / (1 - γ)) / δ)`. If `18 L ≤ (1 - γ) N`, then with probability at +least `1 - δ`, whenever the optimal action values of the empirical MDP `M̂ = M.empirical N ω` are +separated by `η` at its greedy optimal policy `π̂` (`Q̂* (s, a) + η ≤ Q̂* (s, π̂ s)` for every +`a ≠ π̂ s`), the value of `π̂` in `M` satisfies `v* - v^π̂ ≤ 6 C √(2 L / (N (1 - γ) ^ 3))` at every +state. + +[LWCGC24] proves the bound with the constant `12` in place of `6`, for rewards in `[0, 1]` and +under its condition on `N`. -/ +theorem le_streamMeasure_forall_optValue_sub_value_le_of_separated {M : MDP 𝓢 𝓐 ℝ} + {γ : ℝ≥0} (hγ : γ < 1) {C : ℝ} (hR : ∀ p, ∀ᵐ x ∂(M.R p), x ∈ Set.Icc 0 C) {η : ℝ} + (hη : 0 < η) {K : ℕ} (hK : 0 < K) (hKη : 8 * ((1 + γ) * C / (1 - γ)) ≤ (1 - γ) * η * K) + (N : ℕ) [NeZero N] {δ : ℝ} (hδ : 0 < δ) + (hN : 18 * log (8 * Fintype.card 𝓢 * Fintype.card 𝓐 * (K + 1) * log (exp 1 / (1 - γ)) / δ) ≤ + (1 - γ) * N) : + 1 - δ ≤ (streamMeasure M.P).real {ω | + (∀ s a, a ≠ (M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ) s → + (M.empirical N ω).optQValue γ (s, a) + η ≤ + (M.empirical N ω).optQValue γ + (s, (M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ) s)) → + ∀ s, M.optValue γ s - M.value γ (Kernel.deterministic + ((M.empirical N ω).greedy γ ((M.empirical N ω).optValue γ)) + (measurable_of_finite _)) s ≤ + 6 * C * √(2 * log (8 * Fintype.card 𝓢 * Fintype.card 𝓐 * (K + 1) * + log (exp 1 / (1 - γ)) / δ) / (N * (1 - γ) ^ 3))} := by + -- `v* - v^π̂ = (v^π* - v̂^π*) + (v̂^π* - v̂^π̂) + (v̂^π̂ - v^π̂)` for the greedy optimal policy + -- `π*` of `M`: the first term is bounded by [LWCGC24, Lemma 1], since `π*` does not depend on + -- the samples, the second one is nonpositive by optimality of `π̂` in `M̂`, and the third one is + -- bounded by the first claim. Each bound holds with probability at least `1 - δ / 2`. + set μ := streamMeasure M.P + have hRabs (p : 𝓢 × 𝓐) : ∀ᵐ x ∂(M.R p), |x| ≤ C := + (hR p).mono fun x hx ↦ (abs_of_nonneg hx.1).trans_le hx.2 + have hRe (ω : ℕ → 𝓢 × 𝓐 → 𝓢) : ∀ p, ∀ᵐ x ∂((M.empirical N ω).R p), |x| ≤ C := by + simpa using hRabs + set S : ℝ := (Fintype.card 𝓢 : ℝ) + set A : ℝ := (Fintype.card 𝓐 : ℝ) + set lg : ℝ := log (exp 1 / (1 - γ)) with hlg_def + set L := log (8 * S * A * (K + 1) * lg / δ) + have hS : 1 ≤ S := Nat.one_le_cast.2 Fintype.card_pos + have hA : 1 ≤ A := Nat.one_le_cast.2 Fintype.card_pos + have hK₁ : (1 : ℝ) ≤ K + 1 := by linarith [(Nat.cast_nonneg K : (0 : ℝ) ≤ K)] + have hlg₀ : 0 < lg := by + rw [hlg_def] + refine Real.log_pos ((one_lt_div (sub_pos.2 (NNReal.coe_lt_one.2 hγ))).2 ?_) + linarith [Real.add_one_le_exp (1 : ℝ), γ.coe_nonneg] + have h8 : 4 * S * A * (K + 1) * lg / (δ / 2) = 8 * S * A * (K + 1) * lg / δ := by + field_simp + ring + -- the level of [LWCGC24, Lemma 1] at `δ / 2` is at most `L` + have hL₀ : log (4 * S * lg / (δ / 2)) ≤ L := by + refine Real.log_le_log (by positivity) ?_ + rw [show 4 * S * lg / (δ / 2) = 8 * S * lg / δ by field_simp; ring] + refine div_le_div_of_nonneg_right ?_ hδ.le + have h₁ : 1 ≤ A * (K + 1) := one_le_mul_of_one_le_of_one_le hA hK₁ + calc 8 * S * lg = 8 * S * lg * 1 := (mul_one _).symm + _ ≤ 8 * S * lg * (A * (K + 1)) := by gcongr + _ = 8 * S * A * (K + 1) * lg := by ring + -- the two events, each of probability at least `1 - δ / 2` + set g : MDP 𝓢 𝓐 ℝ → 𝓢 → 𝓐 := fun M' ↦ M'.greedy γ (M'.optValue γ) + have hg := measurable_greedy (M := M) (γ := γ) (measurable_optValue hγ hRabs) + set E₁ := {ω | (∀ s a, a ≠ g (M.empirical N ω) s → + (M.empirical N ω).optQValue γ (s, a) + η ≤ (M.empirical N ω).optQValue γ + (s, g (M.empirical N ω) s)) → + ∀ s, |(M.empirical N ω).value γ (Kernel.deterministic (g (M.empirical N ω)) + (measurable_of_finite _)) s - + M.value γ (Kernel.deterministic (g (M.empirical N ω)) (measurable_of_finite _)) s| ≤ + 3 * C * √(2 * L / (N * (1 - γ) ^ 3))} + set E₂ := {ω | ∀ s, |(M.empirical N ω).value γ (Kernel.deterministic (g M) hg) s - + M.value γ (Kernel.deterministic (g M) hg) s| ≤ + 3 * C * √(2 * log (4 * S * lg / (δ / 2)) / (N * (1 - γ) ^ 3))} + have h₁ : 1 - δ / 2 ≤ μ.real E₁ := by + have h := le_streamMeasure_forall_abs_value_empirical_sub_value_le_of_separated hγ hR hη hK + hKη N (half_pos hδ) (by rwa [h8]) + rwa [h8] at h + have h₂ : 1 - δ / 2 ≤ μ.real E₂ := + le_streamMeasure_forall_abs_value_empirical_sub_value_le hγ hR _ N (half_pos hδ) + ((mul_le_mul_of_nonneg_left hL₀ (by norm_num)).trans hN) + have hE₂ : MeasurableSet E₂ := + measurableSet_setOfPred.2 (measurable_comp_empirical M N fun M' ↦ ∀ s, + |M'.value γ (Kernel.deterministic (g M) hg) s - M.value γ (Kernel.deterministic (g M) hg) s| ≤ + 3 * C * √(2 * log (4 * S * lg / (δ / 2)) / (N * (1 - γ) ^ 3))) + have h_inter : 1 - δ ≤ μ.real (E₁ ∩ E₂) := by + have h := measureReal_union_add_inter (μ := μ) (s := E₁) hE₂ + have h₃ : μ.real (E₁ ∪ E₂) ≤ 1 := measureReal_le_one + linarith + refine h_inter.trans (measureReal_mono (fun ω ⟨hω₁, hω₂⟩ hsep s ↦ ?_) (measure_ne_top _ _)) + have hv₁ := abs_le.1 (hω₁ hsep s) + have hv₂ := abs_le.1 (hω₂ s) + -- `π*` is optimal in `M`, and `π̂` is optimal in `M̂` + have hopt : M.value γ (Kernel.deterministic (g M) hg) = M.optValue γ := + value_greedy_optValue hγ hRabs hg + have hle : (M.empirical N ω).value γ (Kernel.deterministic (g M) hg) s ≤ + (M.empirical N ω).value γ (Kernel.deterministic (g (M.empirical N ω)) + (measurable_of_finite _)) s := by + exact (value_le_optValue hγ (hRe ω) s).trans_eq + (congrFun (value_greedy_optValue hγ (hRe ω) (measurable_of_finite _)) s).symm + have hC : 0 ≤ C := (abs_nonneg _).trans (abs_meanReward_le hRabs (s, Classical.arbitrary 𝓐)) + have hsq : 3 * C * √(2 * log (4 * S * lg / (δ / 2)) / (N * (1 - γ) ^ 3)) ≤ + 3 * C * √(2 * L / (N * (1 - γ) ^ 3)) := by + have : 0 ≤ (N : ℝ) * (1 - γ) ^ 3 := by + have := sub_pos.2 (NNReal.coe_lt_one.2 hγ) + positivity + gcongr + rw [← hopt] + linarith + +end Generative + +end Learning.MDP diff --git a/LMLExplore/ReinforcementLearning/Generative/PolicyEvaluation.lean b/LMLExplore/ReinforcementLearning/Generative/PolicyEvaluation.lean index 907647a6..8b91c052 100644 --- a/LMLExplore/ReinforcementLearning/Generative/PolicyEvaluation.lean +++ b/LMLExplore/ReinforcementLearning/Generative/PolicyEvaluation.lean @@ -7,6 +7,7 @@ module public import LMLExplore.ReinforcementLearning.Generative.Basic import LMLExplore.Algebra.Order.Ring.Abs +import LMLExplore.Analysis.SpecialFunctions.Log.Basic import LMLExplore.Analysis.Convex.Integral import LMLExplore.Analysis.Convex.Simplex @@ -28,9 +29,11 @@ The accuracy is of order `√(L / (N (1 - γ) ^ 3))` over the whole range of sam The bound has a deterministic part and a probabilistic part. * The **deterministic part** [LWCGC24, Lemma 2], `ProbabilityTheory.Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le` in - `Probability/Kernel/Resolvent.lean`, compares the resolvents `v^π = R_γ(P_π) r_π` and + `Probability/Kernel/Resolvent.lean`, in its MDP form + `Learning.MDP.abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le` in + `MarkovDecisionProcess/ReturnVariance.lean`, compares the resolvents `v^π = R_γ(P_π) r_π` and `v̂^π = R_γ(P̂_π) r_π` of two state kernels when `P̂_π` deviates from `P_π` by a Bernstein-type - bound on the first `m ≥ log (1 - γ)⁻¹` functions `V 0 = v^π` and + bound on the first `m ≥ log (1 - γ)⁻¹` levels `V = M.valueLevel γ π`, with `V 0 = v^π` and `V (l + 1) = R_γ(P_π) √Var_{P_π}(V l)`. * The **probabilistic part** is Bernstein's inequality for the empirical state kernel of `π` (`measureReal_sqrt_variance_add_le_abs_integral_sub_integral_stateKernel_empirical_le`). @@ -188,84 +191,49 @@ theorem le_streamMeasure_forall_abs_value_empirical_sub_value_le [Fintype 𝓢] |(M.empirical N ω).value γ π s - M.value γ π s| ≤ 3 * C * √(2 * log (4 * Fintype.card 𝓢 * log (exp 1 / (1 - γ)) / δ) / (N * (1 - γ) ^ 3))} := by - -- We apply the deterministic comparison of resolvents - -- `Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le` with `ε = 2 L / N` - -- and `m = ⌈log (1 - γ)⁻¹⌉₊` levels. The functions `V l` of the levels only depend on `M` and + -- We apply the deterministic part `abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le` + -- with `m = ⌈log (1 - γ)⁻¹⌉₊` levels. The functions `V l` of the levels only depend on `M` and -- `π`, so that Bernstein's inequality for the empirical state kernel of `π`, with a union bound -- over the `(m + 1) S ≤ 2 S log (e / (1 - γ))` levels and states, gives the deviations it needs. rcases le_or_gt 1 δ with hδ1 | hδ1 · exact (sub_nonpos.2 hδ1).trans measureReal_nonneg have hN₀ : (0 : ℝ) < N := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne N) - have hγ₁ : (γ : ℝ) < 1 := hγ - have hu : 0 < 1 - (γ : ℝ) := sub_pos.2 hγ₁ have hRabs (p : 𝓢 × 𝓐) : ∀ᵐ x ∂(M.R p), |x| ≤ C := - (hR p).mono fun x hx ↦ abs_le.2 ⟨by linarith [hx.1, hx.2], hx.2⟩ - set f := M.policyReward π with hf_def - have hf : Measurable f := .of_discrete - have hf₀ (s : 𝓢) : 0 ≤ f s := by - rw [hf_def, policyReward_def] - exact integral_nonneg fun a ↦ by - rw [meanReward_def] - exact integral_nonneg_of_ae ((hR _).mono fun x hx ↦ hx.1) - have hfC (s : 𝓢) : f s ≤ C := (le_abs_self _).trans (abs_policyReward_le hRabs s) - -- both values are resolvents of the same reward `f = r_π` + (hR p).mono fun x hx ↦ (abs_of_nonneg hx.1).trans_le hx.2 set P := M.stateKernel π with hP_def - have hv (ω : ℕ → 𝓢 × 𝓐 → 𝓢) (s : 𝓢) : - (M.empirical N ω).value γ π s - M.value γ π s = - ∫ y, f y ∂(Kernel.resolvent γ ((M.empirical N ω).stateKernel π) s) - - ∫ y, f y ∂(Kernel.resolvent γ P s) := by - have hfe : (M.empirical N ω).policyReward π = f := - funext fun s ↦ by rw [policyReward_def, empirical_R, hf_def, policyReward_def] - rw [value_eq_integral_resolvent hγ hRabs, value_eq_integral_resolvent hγ (by simpa using hRabs), - hfe] -- for `γ = 0`, both values are the reward rcases eq_or_ne γ 0 with rfl | hγ₀ · calc 1 - δ ≤ (streamMeasure M.P).real Set.univ := by simp [hδ.le] _ ≤ _ := measureReal_mono fun ω _ ↦ by simp only [Set.mem_ofPred_eq] intro s - rw [hv, Kernel.resolvent_zero, Kernel.resolvent_zero, Kernel.id_apply, sub_self, - abs_zero] - have hC : 0 ≤ C := (hf₀ s).trans (hfC s) + have hf := policyReward_mem_Icc (π := π) hR s + have hC : 0 ≤ C := hf.1.trans hf.2 + rw [value_empirical_zero, sub_self, abs_zero] positivity have hγ₀' : 0 < γ := pos_iff_ne_zero.2 hγ₀ - -- the confidence level `L`, the accuracy `ε = 2 L / N` and the number `m` of levels + -- the confidence level `L` and the number `m` of levels set S : ℝ := (Fintype.card 𝓢 : ℝ) with hS_def set lg : ℝ := log (exp 1 / (1 - γ)) with hlg_def - have hlg : lg = 1 + log (1 - γ)⁻¹ := by - rw [hlg_def, Real.log_div (Real.exp_pos 1).ne' hu.ne', Real.log_exp, Real.log_inv] - ring - have hy : 0 ≤ log (1 - (γ : ℝ))⁻¹ := - Real.log_nonneg (one_le_inv₀ hu |>.2 (by linarith [γ.coe_nonneg])) set L := log (4 * S * lg / δ) with hL_def - set ε := 2 * L / N with hε_def set m := ⌈log (1 - (γ : ℝ))⁻¹⌉₊ with hm_def - have hm : log (1 - (γ : ℝ))⁻¹ ≤ m := Nat.le_ceil _ - have hm' : (m : ℝ) + 1 ≤ 2 * lg := by - have := Nat.ceil_lt_add_one hy - rw [hlg] - linarith + have hm' : (m : ℝ) + 1 ≤ 2 * lg := Real.natCeil_log_inv_one_sub_add_one_le γ.coe_nonneg hγ have hS (s : 𝓢) : 1 ≤ S := Nat.one_le_cast.2 (Fintype.card_pos_iff.2 ⟨s⟩) - have hlg1 : 1 ≤ lg := by rw [hlg]; linarith + have hlg1 : 1 ≤ 2 * lg := by linarith [(Nat.cast_nonneg m : (0 : ℝ) ≤ m)] + have hlg₀ : 0 < lg := by linarith have hL (s : 𝓢) : 0 ≤ L := Real.log_nonneg (by rw [le_div_iff₀ hδ]; nlinarith [hS s]) -- the levels `V l` and their bounds `b l` - set V : ℕ → 𝓢 → ℝ := fun l ↦ Nat.rec (fun x ↦ ∫ y, f y ∂(Kernel.resolvent γ P x)) - (fun _ W x ↦ ∫ y, √Var[W; P y] ∂(Kernel.resolvent γ P x)) l with hV_def - have hV₀ (x : 𝓢) : V 0 x = ∫ y, f y ∂(Kernel.resolvent γ P x) := rfl - have hV (l : ℕ) (x : 𝓢) : V (l + 1) x = ∫ y, √Var[V l; P y] ∂(Kernel.resolvent γ P x) := rfl + set V : ℕ → 𝓢 → ℝ := M.valueLevel γ π with hV_def set b : ℕ → ℝ := fun l ↦ C / ((1 - γ) * (γ * √(1 - γ)) ^ l) with hb_def - have hVb : ∀ l y, V l y ∈ Set.Icc 0 (b l) := - Kernel.mem_Icc_of_eq_integral_resolvent_sqrt_variance hγ₀' hγ hf hf₀ hfC hV₀ hV + have hVb : ∀ l y, V l y ∈ Set.Icc 0 (b l) := valueLevel_mem_Icc hγ₀' hγ hR π -- the bad events: a Bernstein deviation fails at some level `l ≤ m` and state `s` set bad : Fin (m + 1) × 𝓢 → Set (ℕ → 𝓢 × 𝓐 → 𝓢) := fun i ↦ {ω | - √(ε * Var[V i.1; P i.2]) + ε * b i.1 < + √(2 * Var[V i.1; P i.2] * L / N) + b i.1 * L / (3 * N) < |∫ y, V i.1 y ∂((M.empirical N ω).stateKernel π i.2) - ∫ y, V i.1 y ∂(P i.2)|} with hbad_def have h_bad (i : Fin (m + 1) × 𝓢) : (streamMeasure M.P).real (bad i) ≤ δ / Fintype.card (Fin (m + 1) × 𝓢) := by have hS := hS i.2 - have hL := hL i.2 - have hpos : 0 < 4 * S * lg / δ := by positivity have hcard : (Fintype.card (Fin (m + 1) × 𝓢) : ℝ) = (m + 1) * S := by simp [hS_def, Fintype.card_prod] have hb₀ : 0 ≤ b i.1 := (hVb i.1 i.2).1.trans (hVb i.1 i.2).2 @@ -276,7 +244,8 @@ theorem le_streamMeasure_forall_abs_value_empirical_sub_value_le [Fintype 𝓢] have h_empty : bad i = ∅ := by ext ω simp only [hbad_def, Set.mem_ofPred_eq, hV0, Pi.zero_apply, integral_zero, sub_self, - abs_zero, ← hb0, mul_zero, add_zero, Set.mem_empty_iff_false, iff_false, not_lt] + abs_zero, ← hb0, zero_mul, zero_div, add_zero, Set.mem_empty_iff_false, iff_false, + not_lt] exact Real.sqrt_nonneg _ rw [h_empty, measureReal_empty] positivity @@ -284,37 +253,20 @@ theorem le_streamMeasure_forall_abs_value_empirical_sub_value_le [Fintype 𝓢] refine le_trans (measureReal_mono (fun ω (hω : _ < _) ↦ ?_) (measure_ne_top _ _)) ((measureReal_sqrt_variance_add_le_abs_integral_sub_integral_stateKernel_empirical_le M π (l := 0) (u := b i.1) (s := i.2) hbpos (fun a ↦ .of_forall (hVb i.1)) N L).trans ?_) - · rw [Set.mem_ofPred_eq, abs_sub_comm] - refine le_trans (add_le_add (le_of_eq ?_) ?_) hω.le - · rw [hε_def] - congr 1 - ring - · have hbL : 0 ≤ b i.1 * L / N := by positivity - calc (b i.1 - 0) * L / (3 * N) = b i.1 * L / N / 3 := by - rw [sub_zero, div_div, mul_comm (3 : ℝ)] - _ ≤ b i.1 * L / N * 2 := by linarith - _ = ε * b i.1 := by rw [hε_def]; ring - · rw [hcard, Real.exp_neg, hL_def, Real.exp_log hpos, inv_div] - calc 2 * (δ / (4 * S * lg)) = δ / (2 * S * lg) := by field_simp; ring - _ ≤ δ / ((m + 1) * S) := - div_le_div_of_nonneg_left hδ.le (by positivity) (by nlinarith) - -- outside the bad events, the deterministic comparison of resolvents applies + · rw [Set.mem_ofPred_eq, abs_sub_comm, sub_zero] + exact hω.le + · rw [hcard, hL_def] + exact Real.mul_exp_neg_log_div_le two_pos (by positivity) hδ (by nlinarith) + -- outside the bad events, the deterministic part applies refine (one_sub_le_measureReal_compl_iUnion hδ.le h_bad).trans (measureReal_mono fun ω hω ↦ ?_) simp only [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hω simp only [Set.mem_ofPred_eq] intro s - have hε₀ : 0 ≤ ε := by have := hL s; positivity - have hε9 : 9 * ε ≤ 1 - γ := by - rw [hε_def, ← mul_div_assoc, div_le_iff₀ hN₀] - linarith - rw [hv] - refine (Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le - ((M.empirical N ω).stateKernel π) hγ₀' hγ hf hf₀ hfC hV₀ hV hm hε₀ hε9 - (fun l hl x ↦ ?_) s).trans_eq ?_ - · have h := hω (⟨l, Nat.lt_succ_of_le hl⟩, x) - simp only [hbad_def, Set.mem_ofPred_eq, not_lt] at h - exact h - · rw [hε_def, div_div] + refine abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le (empirical_R M N ω) hγ₀' hγ hR + π (Nat.le_ceil _) hN₀ (hL s) hN (fun l hl x ↦ ?_) s + have h := hω (⟨l, Nat.lt_succ_of_le hl⟩, x) + simp only [hbad_def, Set.mem_ofPred_eq, not_lt] at h + exact h end Learning.MDP