[RemyDegenne]

Adds LMLRoadmaps/ReinforcementLearning/: a roadmap for Markov decision processes and reinforcement learning theory, with README.md, Suggested.lean and metadata.toml (topic = "math.OC"). The PR touches only that directory.

Structure

• Layers 0–6: prerequisites, each stated in the generality of its own field.
  • order-unit contractions, abstract dynamic programming, span seminorms and topical maps;
  • Markov processes on general measurable spaces: Markov and strong Markov properties for a general totally ordered index, resolvents, Dobrushin coefficient, mixing, Poisson equation, total variance;
  • Yosida's mean ergodic theorem, group inverses and finite chains;
  • concentration: Freedman, empirical Bernstein, ℓ¹ and KL deviations of empirical laws, covering numbers;
  • stochastic approximation: Robbins–Siegmund, Robbins–Monro, Tsitsiklis's asynchronous SA;
  • smooth optimization and Bregman proximal steps on products of simplices;
  • keyed streams and the divergence decomposition for general LML environments.
• Layers 7–13: MDP planning, mainly after Puterman. Finite horizon, discounted optimality and algorithms, occupancy measures and LPs, the value-difference calculus, average reward and Blackwell optimality.
• Layers 14–23: learning.
  • generative model (Azar–Munos–Kappen, Agarwal–Kakade–Yang, Li et al.);
  • Q-learning and TD;
  • policy gradient, natural policy gradient and policy mirror descent;
  • episodic exploration: UCBVI, UCB-H, MVP and Zhang–Chen–Lee–Du, with the Domingues et al. lower bounds;
  • reward-free exploration and best policy identification;
  • adversarial MDPs, UCRL2, offline RL, linear function approximation.

Design choices for review

• MDP model. It follows the shapes of LML's unmerged mdp branch: MDP 𝓢 𝓐 𝓡 with kernels P, R, and MDP.env with the state as observation and the reward as feedback. LMLExplore copies them, and deletes the copy when LML merges.
• Episodic MDPs. They follow entropy-mdp: ℕ-indexed kernels, the time-augmented MDP, and the episode-level statesEnv. Learning algorithms choose an H-step policy at the start of each episode.
• Corrected sources. Statements correct the errors found in the sources and say so:
  • the UCBVI constant of AJKS Theorem 7.1 is 20, not 10;
  • Puterman's (6.6.9) is false for m ≥ 1;
  • the lower-bound family of Azar–Munos–Kappen lets samples be pooled; the roadmap uses a product family instead;
  • also corrected: the AKLM log-barrier smoothness constant, the AJKS least-squares lemma and the CPI iteration count.
• Dependencies on other roadmaps.
  • The Bandits roadmap: Ville, FTRL and mirror descent, self-normalized bounds, Kiefer–Wolfowitz.
  • The Identification roadmap's change of measure.
  • Tau Ceti's MarkovChainsAndRenewal roadmap: names for the countable-state theory.
• Out of scope (listed explicitly in the README): DEC and eluder dimension, the ODE method, constrained and robust MDPs, RLHF, and others.

lake build passes locally.

AI assistance

Claude Opus 5.5 (Claude Code) drafted the roadmap and the Lean signatures. Five research subagents surveyed Puterman, the RL theory monographs, recent COLT/NeurIPS/ICML/ICLR papers, the pinned Lean dependencies, and the general form of the prerequisites. Three reviewer subagents then checked the draft against the source PDFs, and their findings were applied.

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1