[RemyDegenne]

This PR adds the state-action absorbing modifications M.saAbsorbing p c of an MDP and proves the two decoupling lemmas of [LWCGC24] that they serve: Lemma 3 (with reward Q* p - γ v* s the modification keeps v* and Q*) and Lemma 4 (when the optimal policy of M is separated by ω > 0, a uniform grid of rewards fixed in advance contains one whose modification has the same greedy optimal policy). Lemma 4 goes through the Lipschitz bound (88) of the optimal action values in the absorbing reward.

Roadmap target: ReinforcementLearning, Layer 15.4 (c), "Theorem 1, perturbed plug-in" [LWCGC24, Theorem 1]. The proof of Theorem 1 runs Lemma 6 (tie-breaking, merged in #377, MarkovDecisionProcess/TieBreaking.lean), then Lemma 4 to replace the data-dependent optimal policy π̂* of the perturbed empirical MDP by the optimal policy of one of finitely many (s, a)-absorbing modifications, each independent of the samples at (s, a), then Lemma 5 (Bernstein on these fixed modifications plus a union bound over the pairs and the grid). After this PR, what remains for 15.4 (c) is Lemma 5 and the final assembly of Theorem 1 (Fubini over streamMeasure M.P and the law of the perturbation). The (s, a)-version is needed because the state-absorbing modifications of MarkovDecisionProcess/Absorbing.lean [AKY20] change every action at s, so they do not preserve the greedy policy at s.

Roadmap: ReinforcementLearning

Contents:

• MarkovDecisionProcess/Absorbing/StateAction.lean (new): Learning.MDP.saAbsorbing and its apply lemmas, saAbsorbing_congr (the modification only depends on the rows outside p), lookahead_saAbsorbing_of_eq, Lemma 3 for optimal values (optValue_saAbsorbing_optQValue, optQValue_saAbsorbing_optQValue) and for a stationary policy (value_saAbsorbing_qValue, qValue_saAbsorbing_qValue), the |c - c'| / (1 - γ) Lipschitz bounds for optQValue, optValue, qValue, value, abs_optQValue_sub_optQValue_saAbsorbing_le, the separation transfer optQValue_saAbsorbing_add_le (ω becomes ω / 2, [LWCGC24, (91)]), greedy_optValue_saAbsorbing_eq, and Lemma 4 exists_greedy_optValue_saAbsorbing_eq on the grid -B + 2 B k / K, k ≤ K, with 8 B ≤ (1 - γ) ω K. The grid comes from the existing LMLExplore.exists_abs_sub_grid_le.
• MarkovDecisionProcess/Optimality.lean: greedy_optValue_eq_of_forall_optQValue_lt. If d s is the strict maximiser of Q* (s, ·) at every state, then d is the greedy policy for v*.
• MarkovDecisionProcess/RunValue.lean: abs_optQValue_sub_mul_optValue_le, |Q* (s, a) - γ v* s| ≤ (1 + γ) C / (1 - γ). This gives a bound B for Lemma 4, since Q* p - γ v* s is the reward of Lemma 3.

Statement shape: Lemma 4 is stated for any deterministic policy d separated in the paper's sense (the event B_ω of (41): Q* (s', a') + ω ≤ Q* (s', d s') for a' ≠ d s'). By greedy_optValue_eq_of_forall_optQValue_lt, such a d is the greedy optimal policy of M. The separation produced by Lemma 6 in TieBreaking.lean (pairwise gaps > ω) implies this form through optQValue_add_lt_optValue_of_forall_lt_abs_optQValue_sub. The paper takes u ∈ [-1/(1-γ), 1/(1-γ)] for rewards in [0, 1]. Here any bound B on |Q* p - γ v* s| works.

File move (the new file shares the Absorbing prefix, so the two files now live in a directory; only the module path and one import change, no declaration is renamed):

old module	new module
LMLExplore.MarkovDecisionProcess.Absorbing	LMLExplore.MarkovDecisionProcess.Absorbing.Basic

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, Lemmas 3–4, Appendices B.2–B.3. The file credits it in its module docstring and in its docstrings.

Local checks (not CI): tauceti-local-checks verify --policy ordinary exited 0; scope: full: deleted module: LMLExplore/MarkovDecisionProcess/Absorbing.lean; whole-library lake build --iofail succeeded; local-axioms: checked 5 changed module(s), 168 declaration(s); 0 violation(s).

🤖 Prepared with Claude Code