[RemyDegenne]

This PR proves model-based policy evaluation with a generative model over the full range of sample sizes [LWCGC24, Lemma 1], together with its deterministic core [LWCGC24, Lemma 2]. It is ReinforcementLearning Layer 15.4 (b): for a stationary policy π fixed independently of the data, with probability at least 1 - δ, the value of π in the empirical MDP M.empirical N ω is within 3 C √(2 L / (N (1 - γ) ^ 3)) of its value in M, with L = log (4 S log (e / (1 - γ)) / δ), as soon as 18 L ≤ (1 - γ) N.

LMLExplore/Probability/Kernel/Resolvent.lean (+271 lines) adds, for Markov kernels on a general measurable space:

• Kernel.measurable_of_eq_integral_resolvent_sqrt_variance and Kernel.mem_Icc_of_eq_integral_resolvent_sqrt_variance. For 0 ≤ f ≤ C, take the iterated resolvents V 0 = R_γ f, V (l + 1) = R_γ √Var_κ(V l) of the one-step standard deviations, which are the vectors V^(l) of [LWCGC24, (69)]. They are measurable, and 0 ≤ V l ≤ C / ((1 - γ) (γ √(1 - γ)) ^ l), using main's Lemma 11 (integral_sqrt_variance_integral_resolvent_le) at each step ([LWCGC24, (73)]).
• Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le [LWCGC24, Lemma 2]. Suppose κ' deviates from κ by |κ' V l - κ V l| ≤ √(ε Var_κ(V l)) + ε b l on the levels l ≤ m, with log (1 - γ)⁻¹ ≤ m and 9 ε ≤ 1 - γ. Then |R_γ(κ') f - R_γ(κ) f| ≤ 3 C √(ε / (1 - γ) ^ 3). The proof is the level-by-level expansion [LWCGC24, (74)–(81)]: it uses the simulation identity on main and runs a backward induction over the levels.

LMLExplore/ReinforcementLearning/Generative/PolicyEvaluation.lean (new, 360 lines) adds:

• Learning.MDP.measureReal_sqrt_variance_add_le_abs_integral_sub_integral_stateKernel_empirical_le: Bernstein's inequality for the empirical state kernel of a (possibly stochastic) stationary policy, with the variance under the true state kernel. The i-th summand ∑ a, π(a | s) V (ω i (s, a)) is a mixture of independent samples, and Jensen's inequality bounds its variance by Var_{P_π s}(V). The bound is then the shared stream-model Bernstein inequality measureReal_sqrt_add_le_abs_sub_inv_mul_sum_le (see review round 1 below).
• Learning.MDP.le_streamMeasure_forall_abs_value_empirical_sub_value_le [LWCGC24, Lemma 1]. It applies Lemma 2 with ε = 2 L / N and m = ⌈log (1 - γ)⁻¹⌉₊. The bound for each level and state comes from the Bernstein inequality above, since the V l depend only on M and π. A union bound over the (m + 1) S ≤ 2 S log (e / (1 - γ)) levels and states finishes the proof. The case γ = 0 is handled directly.

Differences from the roadmap statement and the source, all of which make the result stronger. [LWCGC24] and the roadmap assume N ≥ 32 e² L / (1 - γ) and prove the constant 6 for rewards in [0, 1] and deterministic policies. Here the hypothesis is 18 L ≤ (1 - γ) N, which N ≥ 32 e² L / (1 - γ) implies. The constant is 3, from the constant 1 (instead of 4) of main's Lemma 11. Rewards may lie in any [0, C], and the policy may be stochastic. Lemma 2 is stated with the a priori bound b l ≥ ‖V^(l)‖∞ in place of the source's ‖V^(l)‖∞, which makes its hypothesis weaker. The instance-dependent first line of [LWCGC24, (31)] is not stated.

Milestone: ReinforcementLearning Layer 15.4 "The full range of accuracies" [LWCGC24]. This PR closes item (b). After it, 15.4 still needs (a), Theorem 4 for finite horizons (which needs the episodic generative model of 14.3), and (c), Theorem 1 for the perturbed plug-in policy. The proof of (c) uses Kernel.abs_integral_resolvent_sub_integral_resolvent_le_of_abs_sub_le (Lemma 2) for a policy that depends on the data, where it supplies the Bernstein-type condition through a decoupling argument.

Self-review against the rubrics. Reuse: I searched Mathlib, Tau Ceti, Statlib, LML and LMLExplore/ for a resolvent comparison of this kind and for a Bernstein bound for mixtures or state kernels, and found neither. The per-key measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empiricalKernel_le only covers deterministic policies. The standard-deviation bound and the finite-sum form of integral_stateKernel are now shared lemmas (see review round 1 below). Generality: the Bernstein lemma assumes [Finite 𝓢] [Finite 𝓐], which are used for integrability and for the action weights. Lemma 1 assumes [Fintype 𝓢] for S. The deterministic lemmas hold on any measurable space. 0 < γ is needed there because the level bounds divide by γ, and Lemma 1 covers γ = 0 separately. Documentation: proof sketches are in comments, not in the theorem docstrings. No public declaration is removed or renamed. No Mathlib material is vendored.

Review round 1 (commit 1650682), all within the topic:

• Probability/Moments/Variance.lean: new ProbabilityTheory.sqrt_variance_le_of_abs_le (|X| ≤ B a.e., 0 ≤ B gives √Var[X; μ] ≤ B), used in Resolvent.lean (twice), Simulation.lean (twice) and sqrt_variance_le_sqrt_variance_add_of_abs_sub_le.
• Probability/Kernel/Resolvent.lean: the Lemma 2 proof is split. The simulation bound Kernel.abs_integral_resolvent_sub_integral_resolvent_le (new, public) gives |R_γ(κ') f - R_γ(κ) f| ≤ γ R_γ(κ') e when |(κ' - κ) R_γ(κ) f| ≤ e. The scalar backward recursion over the levels is the file-local le_three_mul_sqrt_of_le_mul_add.
• Probability/Kernel/Empirical.lean: new LMLExplore.measureReal_sqrt_add_le_abs_sub_inv_mul_sum_le, Bernstein's inequality for the means N⁻¹ ∑_{i < N} Z (ω i) of a bounded function Z of the samples under streamMeasure. The per-key measureReal_sqrt_variance_add_le_abs_integral_sub_integral_empiricalKernel_le and the new state-kernel lemma are both derived from it, so the shared tail is no longer duplicated.
• MarkovDecisionProcess/MarkovPolicy.lean: Learning.MDP.integral_stateKernel_eq_sum is now public here. It is the finite-action form of integral_stateKernel and takes an integrability hypothesis instead of [Finite 𝓢]. The private copy in the new file is removed.
• PolicyEvaluation.lean: the convex combination step uses Convex.sum_mem, the unused imports Mathlib.Analysis.Complex.ExponentialBounds and LMLExplore.Probability.Moments.Bernstein are dropped, and the Lemma 1 docstring now credits the constant 1 to integral_sqrt_variance_integral_resolvent_le, which improves the 4 of [LWCGC24, Lemma 11].

No public declaration is removed or renamed.

Local verification after round 1 (local checks, not CI): scope: scoped: against 42580bf73ba1354d3254a4de5c926dc5fb16c409. The whole-library lake build --iofail succeeded (Build completed successfully (8531 jobs).). local-axioms: checked 6 changed module(s), 167 declaration(s); 0 violation(s). The module-system, header-style and environment-lint checks (6 changed modules, 167 declarations) also passed.

Roadmap: ReinforcementLearning

🤖 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	Lemma 1, Lemma 2, the iterated-resolvent bounds and both Bernstein inequalities state the intended results, with hypotheses no stronger and conclusions no weaker than in [LWCGC24]. The degenerate cases (δ ≥ 1, γ = 0, empty state space, b l = 0) are handled without making any statement vacuous.
✅	reuse	approved	claude/claude-opus-5-5	None of the new declarations (the simulation bound, the iterated-resolvent bounds, Lemma 2, sqrt_variance_le_of_abs_le, and the Bernstein inequalities for stream means and state kernels) has a counterpart in Mathlib or LMLExplore, and the per-key Bernstein inequality is now derived from the shared stream-mean lemma. The PR reuses existing API instead of re-deriving it: the simplex Jensen inequality, Convex.sum_mem, sq_sub_mem_Icc_of_mem_Icc, integral_stateKernel and Lemma 11.
✅	scope	approved	claude/claude-opus-5-5	The PR proves roadmap target ReinforcementLearning 15.4 (b) ([LWCGC24, Lemma 1], README.md:1399) itself; Lemma 2 and the state-kernel Bernstein bound are direct prerequisites used in its proof. The helper lemmas split out in round 1 are used by the new proofs, and the edits to existing call sites only adopt them, so the PR is a single topic.
✅	attribution	approved	claude/claude-opus-5-5	Resolvent.lean and PolicyEvaluation.lean credit [LWCGC24] Lemmas 1, 2 and 11 with full inline citations, link the proof steps to the paper's equations and explain how the constants differ from the paper. The helper lemmas in the other files are routine refactors that follow no particular source, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	New public declarations are general infrastructure (std-dev bound, finite-action stateKernel integral, stream Bernstein, simulation bound, iterated-resolvent bounds) or roadmap products (Lemmas 1–2); the only private helper is the argument-specific scalar recursion. No exposed bodies, compatibility artifacts, or annotation issues.
✅	generality	approved	claude/claude-opus-5-5	The resolvent comparison lemmas (Lemma 2 and the iterated-level bounds) hold for Markov kernels on any measurable space, and both Bernstein variants are derived from the shared stream-model inequality instead of being duplicated. The finiteness, positivity and boundedness assumptions are used and match the existing API conventions.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration sits in its natural home: the general resolvent, variance and stream-Bernstein lemmas in the existing Probability files, integral_stateKernel_eq_sum beside integral_stateKernel, and the MDP results in a new file in the existing Generative/ directory. Every new import is used (ExponentialBounds for Real.exp_one_lt_three; Algebra.Order.Ring.Abs, Convex.Integral and Convex.Simplex for sq_sub_mem_Icc_of_mem_Icc, integral_mem_Icc_of_ae_mem_Icc and sq_dotProduct_le_dotProduct_sq_of_mem_simplex).
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard terminology and match the adjacent measureReal_sqrt_*_le, le_streamMeasure_forall_*, Kernel.*_integral_resolvent_* and variance_le_sq_of_abs_le families; none overstates its statement and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new module and every new public declaration have accurate docstrings that describe the results, and the prior finding about the Lemma 2 overview in Resolvent.lean (missing hypotheses and level count) is fixed in the current text.
✅	proof-quality	approved	claude/claude-opus-5-5	The reusable steps are factored into separate lemmas (the simulation bound, the scalar recursion, the shared Bernstein tail and the √Var bound), and the remaining long proofs have comments explaining their structure. There are no brittle rewrite chains and no undocumented definitional-equality steps across wrappers.

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

_{Reviewing this diff at head 7c86c58. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $5.52.}