feat: tie-breaking of optimal action values by random rewards [LWCGC24, Lemma 6]

LMLExplore/MarkovDecisionProcess/ActionElimination.lean

@@ -151,8 +151,7 @@ theorem optQValue_lt_optValue_of_lookahead_lt (hγ : γ < 1) (hR : ∀ p, ∀ᵐ
     (hL : vL s ≤ M.optValue γ s) (h : M.lookahead γ vU (s, a) < vL s) :
     M.optQValue γ (s, a) < M.optValue γ s := by
   rw [optQValue_eq_lookahead]
-  exact ((lookahead_mono (integrable_of_abs_le (measurable_optValue hγ hR)
-    (abs_optValue_le hγ hR) _) hU_int hU).trans_lt h).trans_le hL
+  exact ((lookahead_mono (integrable_optValue hγ hR _) hU_int hU).trans_lt h).trans_le hL
 
 /-- **The action elimination test** for deterministic policies [P, Proposition 6.7.3]: with
 finitely many actions, bounded rewards and `γ < 1`, let `vU` be an upper bound of `v*`, integrable

LMLExplore/MarkovDecisionProcess/Basic.lean

@@ -44,6 +44,7 @@ the dot notation `M.env` when the namespace `Learning` is open.
 * `Learning.MDP.policyMeasure M π hπ s`: the law of the trajectory of `π` started at `s`.
 * `Learning.MDP.stateLaw M π hπ s`: the law of the state-action trajectory of `π` from `s`.
 * `Learning.MDP.meanReward R p`: the mean reward of the state-action pair `p`.
+* `Learning.MDP.ofDet P r hr`: the MDP with transition kernel `P` and deterministic rewards `r`.
 
 ## Main statements
 
@@ -116,6 +117,40 @@ lemma norm_meanReward_le (R : Kernel (𝓢 × 𝓐) 𝓡) [IsMarkovKernel R] {p
 
 end MeanReward
 
+/-! ### Deterministic rewards -/
+
+/-- The MDP with transition kernel `P` and the deterministic reward `r p` at every state-action
+pair `p`. -/
+noncomputable def ofDet (P : Kernel (𝓢 × 𝓐) 𝓢) [IsMarkovKernel P] (r : 𝓢 × 𝓐 → 𝓡)
+    (hr : Measurable r) : MDP 𝓢 𝓐 𝓡 where
+  P := P
+  R := Kernel.deterministic r hr
+
+@[simp]
+lemma ofDet_P (P : Kernel (𝓢 × 𝓐) 𝓢) [IsMarkovKernel P] (r : 𝓢 × 𝓐 → 𝓡) (hr : Measurable r) :
+    (ofDet P r hr).P = P :=
+  (rfl)
+
+@[simp]
+lemma ofDet_R (P : Kernel (𝓢 × 𝓐) 𝓢) [IsMarkovKernel P] (r : 𝓢 × 𝓐 → 𝓡) (hr : Measurable r) :
+    (ofDet P r hr).R = Kernel.deterministic r hr :=
+  (rfl)
+
+/-- The mean reward of the deterministic reward kernel of a function `r` is `r`. It gives the mean
+reward of `ofDet P r hr`. -/
+@[simp]
+lemma meanReward_deterministic [NormedAddCommGroup 𝓡] [NormedSpace ℝ 𝓡] [CompleteSpace 𝓡]
+    [MeasurableSingletonClass 𝓡] (r : 𝓢 × 𝓐 → 𝓡) (hr : Measurable r) :
+    meanReward (Kernel.deterministic r hr) = r := by
+  ext p
+  simp [meanReward_def, Kernel.deterministic_apply]
+
+/-- Deterministic rewards bounded by `C` are almost surely bounded by `C`. -/
+lemma ae_abs_ofDet_R_le (P : Kernel (𝓢 × 𝓐) 𝓢) [IsMarkovKernel P] {r : 𝓢 × 𝓐 → ℝ}
+    (hr : Measurable r) {C : ℝ} (hC : ∀ p, |r p| ≤ C) (p : 𝓢 × 𝓐) :
+    ∀ᵐ x ∂((ofDet P r hr).R p), |x| ≤ C := by
+  simpa [Kernel.deterministic_apply, ae_dirac_eq] using hC p
+
 /-! ### Deterministic stationary policies and their trajectory laws -/
 
 /-- The deterministic stationary policy `π` as an algorithm: it plays `π s` in the current

LMLExplore/MarkovDecisionProcess/Optimality.lean

@@ -38,7 +38,8 @@ here on a general measurable state space.
 ## Main statements
 
 * `Learning.MDP.bellman_optValue`: `T v* = v*` [P, Theorem 6.2.5 (a)];
-  `Learning.MDP.measurable_optValue`: `v*` is measurable.
+  `Learning.MDP.measurable_optValue`, `Learning.MDP.integrable_optValue`: `v*` is measurable,
+  and integrable for every finite measure.
 * `Learning.MDP.value_greedy_optValue`: the greedy policy for `v*` has value `v*`
   [P, Theorem 6.2.7 (b)].
 * `Learning.MDP.optValueBM`, `Learning.MDP.isFixedPt_bellmanOp_optValueBM`: `v*` is the fixed point
@@ -96,6 +97,12 @@ theorem measurable_optValue (hγ : γ < 1) (hR : ∀ p, ∀ᵐ x ∂(M.R p), |x|
   obtain ⟨u, hu, huB, hu_eq⟩ := exists_bellman_eq (M := M) hγ hR
   rwa [← eq_optValue_of_bellman_eq hγ hR hu huB hu_eq]
 
+/-- With finitely many actions, bounded rewards and `γ < 1`, the optimal value is integrable for
+every finite measure on the states. -/
+theorem integrable_optValue (hγ : γ < 1) (hR : ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) (μ : Measure 𝓢)
+    [IsFiniteMeasure μ] : Integrable (M.optValue γ) μ :=
+  integrable_of_abs_le (measurable_optValue hγ hR) (abs_optValue_le hγ hR) μ
+
 /-- With finitely many actions, bounded rewards and `γ < 1`, the discounted value of every
 algorithm from the probability measure `μ` is at most `∫ v* dμ`. -/
 theorem runValue_le_integral_optValue {μ : Measure 𝓢} [IsProbabilityMeasure μ] (hγ : γ < 1)
@@ -286,8 +293,7 @@ theorem qValue_le_optQValue (hγ : γ < 1) (hR : ∀ p, ∀ᵐ x ∂(M.R p), |x|
     M.qValue γ π ≤ M.optQValue γ := fun p ↦ by
   rw [qValue_eq_lookahead, optQValue_eq_lookahead]
   exact lookahead_mono (integrable_of_abs_le (measurable_value hγ hR) (abs_value_le hγ hR) _)
-    (integrable_of_abs_le (measurable_optValue hγ hR) (abs_optValue_le hγ hR) _)
-    (value_le_optValue hγ hR)
+    (integrable_optValue hγ hR _) (value_le_optValue hγ hR)
 
 /-- With finitely many actions, bounded rewards and `γ < 1`, a stationary policy whose value is
 within `ε` of the optimal value, `v* - v^π ≤ ε`, has action values within `γ ε` of the optimal
@@ -296,7 +302,7 @@ theorem optQValue_sub_qValue_le_of_optValue_sub_value_le (hγ : γ < 1)
     (hR : ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) {ε : ℝ} (hπ : ∀ s, M.optValue γ s - M.value γ π s ≤ ε)
     (p : 𝓢 × 𝓐) :
     M.optQValue γ p - M.qValue γ π p ≤ γ * ε := by
-  have hv := integrable_of_abs_le (measurable_optValue hγ hR) (abs_optValue_le hγ hR) (M.P p)
+  have hv := integrable_optValue hγ hR (M.P p)
   have hv' := integrable_of_abs_le (measurable_value (π := π) hγ hR) (abs_value_le hγ hR) (M.P p)
   rw [optQValue_def, qValue_eq_lookahead, lookahead_def, add_sub_add_left_eq_sub, ← mul_sub,
     ← integral_sub hv hv']

LMLExplore/MarkovDecisionProcess/Simulation.lean

@@ -41,7 +41,9 @@ bound compares `Q*_M - Q*_M'` with the solution of the resolvent equation of `P'
 supersolution, because `π'*` is suboptimal in `M`. Only the fixed function `v*` of `M` enters the
 transition error, so that a reward error of at most `δ` and an error of at most `ε` in the
 one-step predictions of `v*` result in an error of at most `δ / (1 - γ) + γ ε / (1 - γ)` in the
-optimal action values and the optimal values.
+optimal action values and the optimal values. When the two MDPs have the same transition kernel,
+the lower bound shows that the optimal action values and the optimal values are monotone in the
+mean rewards.
 
 When the transition kernels are within `η` in total variation, `tvDist (P (s, a)) (P' (s, a)) ≤ η`
 (Mathlib's `tvDist`, with values in `[0, 2]`), and the rewards of `M` satisfy `|r| ≤ C`, the
@@ -89,6 +91,9 @@ plug-in policy of a generative model.
   models differ by at most `δ / (1 - γ) + γ ε / (1 - γ)`.
 * `Learning.MDP.optQValue_sub_optQValue_le`, `Learning.MDP.le_optQValue_sub_optQValue`:
   **the componentwise bounds** [AJKS, Lemma 2.5] on `Q*_M - Q*_M'`, with a reward error.
+* `Learning.MDP.optQValue_le_optQValue_of_meanReward_le`,
+  `Learning.MDP.optValue_le_optValue_of_meanReward_le`: for two MDPs with the same transition
+  kernel, the optimal action values and the optimal values are monotone in the mean rewards.
 * `Learning.MDP.abs_optQValue_sub_optQValue_le`, `Learning.MDP.abs_optValue_sub_optValue_le`: if
   `|r - r'| ≤ δ` and `|(P - P') v*| ≤ ε`, the optimal action values and the optimal values of the
   two models differ by at most `δ / (1 - γ) + γ ε / (1 - γ)`.
@@ -278,6 +283,31 @@ theorem le_optQValue_sub_optQValue (hγ : γ < 1) (hR : ∀ p, ∀ᵐ x ∂(M.R
   simp only [Pi.add_apply, Pi.sub_apply]
   linarith
 
+/-- For two MDPs with finitely many actions, bounded rewards, the same transition kernel and
+`γ < 1`, if the mean rewards of `M'` are at least those of `M`, so are its optimal action values. -/
+theorem optQValue_le_optQValue_of_meanReward_le (hγ : γ < 1) (hR : ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C)
+    (hR' : ∀ p, ∀ᵐ x ∂(M'.R p), |x| ≤ C') (hP : M'.P = M.P)
+    (hr : ∀ q, meanReward M.R q ≤ meanReward M'.R q) :
+    M.optQValue γ ≤ M'.optQValue γ := fun p ↦ by
+  have := Fintype.ofFinite 𝓐
+  -- the componentwise lower bound, with the greedy optimal policy of `M`
+  have hg := measurable_greedy (M := M) (γ := γ) (measurable_optValue hγ hR)
+  have h := le_optQValue_sub_optQValue (M := M') (M' := M) hγ hR' hR
+    (value_greedy_optValue hγ hR hg) p
+  simp only [hP, sub_self, mul_zero, add_zero] at h
+  linarith [integral_nonneg (μ := Kernel.resolvent γ (M.saKernel (Kernel.deterministic _ hg)) p)
+    fun q ↦ sub_nonneg.2 (hr q)]
+
+/-- For two MDPs with finitely many actions, bounded rewards, the same transition kernel and
+`γ < 1`, if the mean rewards of `M'` are at least those of `M`, so are its optimal values. -/
+theorem optValue_le_optValue_of_meanReward_le (hγ : γ < 1) (hR : ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C)
+    (hR' : ∀ p, ∀ᵐ x ∂(M'.R p), |x| ≤ C') (hP : M'.P = M.P)
+    (hr : ∀ q, meanReward M.R q ≤ meanReward M'.R q) :
+    M.optValue γ ≤ M'.optValue γ := fun s ↦ by
+  rw [← iSup_optQValue hγ hR s, ← iSup_optQValue hγ hR' s]
+  exact ciSup_mono (Finite.bddAbove_range _) fun a ↦
+    optQValue_le_optQValue_of_meanReward_le hγ hR hR' hP hr (s, a)
+
 /-- For two MDPs `M` and `M'` with finitely many actions, bounded rewards and `γ < 1`, if the mean
 rewards differ by at most `δ` and the one-step predictions of the optimal value `v*` of `M` differ
 by at most `ε`, `|∫ v* dP (s, a) - ∫ v* dP' (s, a)| ≤ ε`, then the optimal action values of the two