[RemyDegenne]

This PR adds the pessimistic decomposition of an episodic MDP [JYW21, Theorem 4.2, deterministic part]. It is the item "The pessimistic decomposition [JYW21, Theorem 4.2, deterministic part]" of the milestone Layer 12.2 (Corollaries) of the ReinforcementLearning roadmap. The new file LMLExplore/MarkovDecisionProcess/Episodic/Pessimism.lean builds on the value-difference identity integral_sub_integral_value (PR #136) and proves:

• integral_value_sub_integral_value_eq_sum_add_sum_sub_sum, the decomposition of suboptimality [JYW21, Lemma 3.1]. For estimates Q̂_h with V̂_h = ∫ Q̂_h dπ̂_h and V̂_H = 0, the gap ∫ V^π_0 dμ - ∫ V^π̂_0 dμ is the optimization error, plus the model evaluation errors ι_h = r_h + P_h V̂_{h+1} - Q̂_h along π, minus the same errors along π̂. This holds for any comparator Markov policy π.
• integral_value_sub_integral_value_le_sum: if π̂ is greedy (Q̂_h ≤ V̂_h) and the estimates are pessimistic (ι_h ≥ 0), the suboptimality is at most ∑_h ∫ ι_h dd^π_h.
• integral_value_sub_integral_value_le_two_mul_sum: for the estimates of pessimistic value iteration, Q̂_h = min (T̂_h - Γ_h, H - h)⁺, with rewards in [0, 1] and |T̂_h - (r_h + P_h V̂_{h+1})| ≤ Γ_h, we get 0 ≤ ι_h ≤ 2 Γ_h [JYW21, Lemma 5.1], hence ∫ V^π_0 dμ - ∫ V^π̂_0 dμ ≤ 2 ∑_h ∫ Γ_h dd^π_h for every Markov comparator π.
• integral_optValue_sub_integral_value_le_two_mul_sum: the case π = π* (the greedy optimal policy optPolicy), i.e. the roadmap statement V*_0 - V^π̂_0 ≤ 2 ∑_h E^{π*}[Γ_h(S_h, A_h)].

Following the roadmap's "deterministic part", the statements take the PEVI recursion as hypotheses on Q̂, V̂ and π̂, with arbitrary estimated backups T̂_h and penalties Γ_h. They do not define an algorithm, so Layer 22.3 (where T̂_h, Γ_h come from data and the bound holds on the event of the ξ-uncertainty quantifier) and the linear PEVI of Layer 23.4 can use them directly. The initial state has an arbitrary law μ (a Dirac mass in [JYW21]), and the spaces are general measurable spaces.

After this PR, the remaining item of Layer 12.2 is the policy-mixture lemma [AJKS, Lemma 14.1]. Its sibling items (performance difference, simulation, componentwise, greedy and optimistic bounds) are already on main.

Source: Y. Jin, Z. Yang and Z. Wang, Is pessimism provably efficient for offline RL?, ICML 2021, arXiv:2012.15085 (Algorithm 1, Lemma 3.1, Theorem 4.2, Lemma 5.1). No Mathlib material is vendored.

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.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The decomposition, the pessimism bound and the PEVI bounds faithfully state [JYW21, Lemma 3.1, Lemma 5.1, Theorem 4.2], with the comparator and initial law generalized; 0 ≤ ι ≤ 2Γ was checked by hand (Γ ≥ 0 follows from hTΓ), the hypotheses are satisfiable non-degenerately, and value_optPolicy correctly ties the π* case to optValue.
✅	reuse	approved	claude/claude-opus-5-5	The decomposition, the greedy-pessimism bound and the PEVI bounds have no existing counterpart: integral_integral_sub_integral_value assumes Q H = 0 rather than V H = 0, and integral_sub_integral_value_le is the optimistic direction. The new helpers measurable_of_eq_integral and abs_le_abs_of_eq_integral were extracted from local haves in integral_integral_sub_integral_value and are used in both files, and the proofs reuse integral_sub_integral_value, meanReward_add_integral_mem_Icc, value_optPolicy and Convex.integral_mem.
✅	scope	approved	claude/claude-opus-5-5	Adds the pessimistic decomposition item of ReinforcementLearning Layer 12.2 (README.md:1003), and the final theorem is the roadmap statement. The PerformanceDifference.lean edit only pulls out two helpers that the new file needs, so the PR is a single topic.
✅	attribution	approved	claude/claude-opus-5-5	The file credits its central source, [JYW21] (arXiv:2012.15085), naming Algorithm 1, Lemma 3.1, Theorem 4.2 and Lemma 5.1 in the module references and in each main theorem's docstring, and it states how it departs from the paper. Its formal dependency, integral_sub_integral_value, is already in the repository and credited to [JYW21, Lemma A.1]; the helper lemmas are routine refactors, nothing is copied from Mathlib, and the roadmap is not credited in the file.
✅	api-design	approved	claude/claude-opus-5-5	The four public theorems are the roadmap's Layer 12.2 pessimistic-decomposition products, the two helpers moved to PerformanceDifference.lean are reasonably public shared infrastructure, and the one private helper is specific to the clipped-estimate argument. No definitions, annotations or compatibility surface are introduced.
✅	generality	approved	claude/claude-opus-5-5	The decomposition and pessimism bounds hold for any Markov comparator, any initial law and general measurable spaces, and the optimal-policy case is derived from the general theorem rather than re-proved. Each hypothesis is used and none is stronger than [JYW21] or the existing value-difference API needs; the two extracted helpers are shared by the old and new proofs instead of being duplicated.
✅	placement	approved	claude/claude-opus-5-5	Episodic/Pessimism.lean belongs in the existing Episodic/ directory, and the two factored-out helpers (measurable_of_eq_integral, abs_le_abs_of_eq_integral) sit in PerformanceDifference.lean, where they were first used. Every import is used and none is too broad; Mathlib.Analysis.Convex.Integral is needed for Convex.integral_mem and other files import it only privately.
✅	naming	approved	claude/claude-opus-5-5	New theorem names describe their conclusions consistently with the sibling integral_sub_integral_value/integral_value_sub_integral_value lemmas, with _eq/_le matching statement strength. Declarations sit in the existing Learning.MDP.Episodic.EpisodicMDP namespace and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring of Pessimism.lean and every public theorem docstring accurately describe their statements, including the generalisations beyond [JYW21] (any Markov comparator, any initial law, general measurable spaces), without overclaiming or project-process text. The two new public helper lemmas in PerformanceDifference.lean are documented correctly.
✅	proof-quality	approved	claude/claude-opus-5-5	The previously duplicated measurability and boundedness arguments for V h = ∫ Q h dπ'_h are now the shared public lemmas measurable_of_eq_integral and abs_le_abs_of_eq_integral, used by both integral_integral_sub_integral_value and the new decomposition. The remaining proofs are short, commented where they are not obvious, rely on robust automation (linarith, ring, simp), and contain no change/show or undocumented defeq.

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

_{Reviewing this diff at head 233dcef. rubrics @ 32ce206. CLI @ 32ce206. Review spend: $5.59.}