[RemyDegenne]

This PR proves [LWCGC24, Lemma 5], the leave-one-out evaluation of the plug-in policy when its optimal action values are separated. Let M̂ = M.empirical N ω be the empirical MDP of a generative model and π̂ its greedy optimal policy. Assume M̂ is separated by η > 0 at π̂, that is Q̂* (s, a) + η ≤ Q̂* (s, π̂ s) for a ≠ π̂ s (the event B_η of [LWCGC24, (41)]). Then, with probability at least 1 - δ, |v̂^π̂ - v^π̂| ≤ 3 C √(2 L / (N (1 - γ) ^ 3)) (first claim), and v* - v^π̂ ≤ 6 C √(2 L' / (N (1 - γ) ^ 3)) (second claim). Here L = log (4 S A (K + 1) log (e / (1 - γ)) / δ), K + 1 is the size of the reward grid of Lemma 4, and L' is L at δ / 2.

Roadmap target: ReinforcementLearning, Layer 15.4 (c), "Theorem 1, perturbed plug-in" [LWCGC24, Theorem 1]. Lemmas 1–2 (#372), 3–4 (#382), 6 (#377) and 11 (#279) are already merged. #382 said that only Lemma 5 and the final assembly were left. This PR supplies Lemma 5: it combines Lemma 4 (exists_greedy_optValue_saAbsorbing_eq), Bernstein at each pair for the fixed (s, a)-absorbing modifications, a union bound over pairs, grid points and levels, and Lemma 2 (Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le). The second claim adds Lemma 1 for the greedy optimal policy of M. After this PR, only the assembly of Theorem 1 remains for 15.4 (c): Lemma 6 for ofDet P̂ (r + ζ), plus this lemma for each fixed perturbation ζ, combined by Fubini over streamMeasure M.P and the law of ζ, plus the ξ / (1 - γ) comparison of perturbed and unperturbed values.

Roadmap: ReinforcementLearning

Contents:

• ReinforcementLearning/Generative/LeaveOneOut.lean (new):
  • le_streamMeasure_forall_abs_value_empirical_sub_value_le_of_separated: Lemma 5, first claim. It only keeps its own union bound, over pairs, grid points and levels, and then applies the shared deterministic lemma below.
  • le_streamMeasure_forall_optValue_sub_value_le_of_separated: Lemma 5, second claim.
  • Everything is in Learning.MDP.
• ReinforcementLearning/Generative/PolicyEvaluation.lean:
  • the new definition valueLevel M γ π l names the levels V 0 = R_γ(P_π) r_π, V (l + 1) = R_γ(P_π) √Var_{P_π}(V l) of [LWCGC24, Lemma 2], with the @[simp] equations valueLevel_zero, valueLevel_succ and the bound valueLevel_mem_Icc [LWCGC24, (73)];
  • the new abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le is the deterministic part of Lemma 1, stated for these levels. It covers two MDPs with the same rewards in [0, C], deviations in Bernstein form at level L on the levels l ≤ m, and 18 L ≤ (1 - γ) N. Lemma 1 (le_streamMeasure_forall_abs_value_empirical_sub_value_le, same statement) and the first claim of Lemma 5 are now both proved from it.
• ReinforcementLearning/Generative/Decoupling.lean:
  • the new general indepFun_comp_redirect_empirical covers every function of a redirection M̂.redirect hS s c on a set S of pairs, which is independent of the samples of each p ∈ S;
  • the new measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_redirect_le is Bernstein's inequality at each p ∈ S for these functions;
  • the existing indepFun_comp_absorbing_empirical and measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_absorbing_le keep their names and statements and are now one-line corollaries;
  • the new indepFun_comp_saAbsorbing_empirical and measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empirical_saAbsorbing_le [LWCGC24, (92)] are corollaries of the same kind.
• MarkovDecisionProcess/MarkovPolicy.lean: the @[simp] lemma stateKernel_deterministic_apply, M.stateKernel (Kernel.deterministic d hd) s = M.P (s, d s).
• MarkovDecisionProcess/Value.lean: policyReward_mem_Icc, which says that with rewards in [0, C] the reward of a stationary policy is in [0, C], and the @[simp] lemma value_zero, M.value 0 π s = M.policyReward π s.
• ReinforcementLearning/Generative/Basic.lean: value_empirical_zero, (M.empirical N ω).value 0 π = M.value 0 π, used by the γ = 0 cases of Lemmas 1 and 5.
• Analysis/SpecialFunctions/Log/Basic.lean: Real.natCeil_log_inv_one_sub_add_one_le, ⌈log (1 - γ)⁻¹⌉₊ + 1 ≤ 2 log (e / (1 - γ)). This is the level count used by both union bounds.

Statement shape and constants:

• The statements hold on the separation event: 1 - δ ≤ P {ω | B_η(ω) → bound(ω)}. [LWCGC24] instead assumes P(B_η) ≥ 1 - δ and concludes with probability 1 - 3δ. The event form fits any tie-breaking argument, in particular the Fubini step of Theorem 1, where the separation is a probability over ζ for each fixed ω.
• The grid is a parameter K > 0 with 8 (1 + γ) C / (1 - γ) ≤ (1 - γ) η K. This is exactly the hypothesis of Lemma 4 as merged, with B = (1 + γ) C / (1 - γ) from abs_optQValue_sub_mul_optValue_le.
• Rewards are in [0, C] rather than [0, 1]. The condition on N is 18 L ≤ (1 - γ) N, which is implied by the paper's N ≥ 16 e² β₁ / (1 - γ). The constants are 3 and 6 instead of the paper's 6 and 12, because Lemma 11 was merged with constant 1.

No public declaration is removed or renamed.

Source: 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 (arXiv:2005.12900), §6.3.2, Lemma 5 and its proof in Appendix B.4. The new file credits it in its module docstring and in each docstring. No Mathlib material was vendored.

Local checks, not CI: tauceti-local-checks verify --policy ordinary passed; scope: scoped: against 137597eb095e141e43856956fdfdb990b81ab838; the whole-library lake build --iofail completed (8591 jobs); local-axioms: checked 7 changed module(s), 192 declaration(s); 0 violation(s); module-system, header-style and changed-module lint all passed.

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	Both claims of Lemma 5, valueLevel and the shared deterministic lemma faithfully formalize [LWCGC24, Lemmas 2 and 5]: the grid depends only on C and γ and so is fixed independently of the samples, the levels use the true kernel at the leave-one-out policies, and the event form implies the paper's probability statement.
✅	reuse	approved	claude/claude-opus-5-5	New declarations (redirect decoupling and Bernstein lemmas, valueLevel, the deterministic evaluation lemma, Lemma 5 and the small helper lemmas) have no counterparts in LMLExplore or Mathlib, and the PR replaces the old absorbing-specific proofs, the private two_mul_exp_neg_log_le and the inline Lemma 1 plumbing with shared lemmas instead of duplicating them. value_zero is unconditional, so value_eq_policyReward_add (which needs γ < 1 and bounded rewards) does not replace it.
✅	scope	approved	claude/claude-opus-5-5	Lemma 5 of LWCGC24 is a direct step toward the confirmed roadmap target ReinforcementLearning 4 (c), Theorem 1 (perturbed plug-in) (README.md:1402), and after it only the target's final assembly remains. The extraction of the shared deterministic lemma from Lemma 1, the generalization of the decoupling lemmas to redirect, and the small log/value helper lemmas are all used by the new file, so the PR is a single topic.
✅	attribution	approved	claude/claude-opus-5-5	All new material (LeaveOneOut.lean, valueLevel and the deterministic Lemma 1/2 wrapper, the redirect/saAbsorbing decoupling and Bernstein lemmas) credits [LWCGC24] at the specific lemma, equation, section and appendix it follows, with the arXiv id. The remaining helpers are routine, existing [AKY20] credit is kept, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The new surface (valueLevel with its (rfl) simp equations and bound, the redirect/saAbsorbing decoupling and Bernstein lemmas, and the general log/exp, stateKernel and value lemmas) is minimal, keeps definition bodies hidden and lives in the right modules. The former private helper became a public general lemma, and no compatibility layer remains.
✅	generality	approved	claude/claude-opus-5-5	Redirect decoupling and Bernstein are proved in general with the absorbing and pair-absorbing versions derived from them, the deterministic Lemma 1/2 step is stated once and shared by Lemmas 1 and 5, and the private count helper is replaced by a general log lemma. Every hypothesis checked is used and needed, and none is stronger than convention.
✅	placement	approved	claude/claude-opus-5-5	The prior placement findings are resolved: valueLevel, its simp lemmas, valueLevel_mem_Icc and abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le now live in MarkovDecisionProcess/ReturnVariance.lean, and all other new declarations and imports are in fitting homes and used.
✅	naming	approved	claude/claude-opus-5-5	New names (valueLevel, valueLevel_mem_Icc, abs_value_sub_value_le_of_abs_integral_stateKernel_sub_le, the redirect/saAbsorbing decoupling and Bernstein lemmas, ..._of_separated, and the Real. helpers) describe their conclusions and match adjacent Lemma 1 and absorbing-decoupling naming. Namespaces are appropriate and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new module LeaveOneOut.lean and all new public declarations (valueLevel, the shared deterministic Lemma 1/2 part, the redirect and saAbsorbing decoupling and Bernstein lemmas, and the log helpers) have accurate docstrings that credit [LWCGC24] and state where they differ from the paper (event form, constants, reward range). Every cross-reference resolves, including TieBreaking.lean and exists_greedy_optValue_saAbsorbing_eq, and no docstring overclaims, describes the proof, or still mentions the removed two_mul_exp_neg_log_le.
✅	proof-quality	approved	claude/claude-opus-5-5	Shared reasoning (the deterministic part of Lemma 1, the confidence count and the level count) is factored into reusable lemmas and used everywhere it applies. The long Lemma 5 proofs explain their structure in comments and do not rely on undocumented definitional equality.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 22f859d. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.21.}