From 9f3306af95bfd881b228fa71f61752ba4d50e2f3 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 2 Nov 2026 10:13:05 +0100 Subject: [PATCH] Add the ReinforcementLearning roadmap Markov decision processes and reinforcement learning theory: general prerequisites (Layers 0-6), MDP planning following Puterman (Layers 7-13), and the sample-complexity and regret theory of reinforcement learning (Layers 14-23). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1 --- LMLRoadmaps/ReinforcementLearning/README.md | 1812 +++++++++++++++++ .../ReinforcementLearning/Suggested.lean | 421 ++++ .../ReinforcementLearning/metadata.toml | 1 + 3 files changed, 2234 insertions(+) create mode 100644 LMLRoadmaps/ReinforcementLearning/README.md create mode 100644 LMLRoadmaps/ReinforcementLearning/Suggested.lean create mode 100644 LMLRoadmaps/ReinforcementLearning/metadata.toml diff --git a/LMLRoadmaps/ReinforcementLearning/README.md b/LMLRoadmaps/ReinforcementLearning/README.md new file mode 100644 index 0000000..b442706 --- /dev/null +++ b/LMLRoadmaps/ReinforcementLearning/README.md @@ -0,0 +1,1812 @@ +# Roadmap: Markov decision processes and reinforcement learning theory + +Develop the theory of Markov decision processes and of learning to control them. On the planning +side, the headline results are: +- the optimality equations and the existence of optimal deterministic stationary policies for the + finite-horizon, discounted and average-reward criteria; +- the convergence of value iteration, policy iteration and their variants; +- the linear programs of discounted MDPs and their occupancy measures; +- the Laurent expansion of discounted values and the existence of Blackwell-optimal policies. + +On the learning side, the headline results are the sample complexity and regret bounds that settled +the field's basic questions: +- planning with a generative model: Azar–Munos–Kappen, Agarwal–Kakade–Yang, and Li–Wei–Chi–Gu–Chen + over the full range of accuracies; +- the tight analysis of Q-learning, and finite-time temporal-difference learning with linear + features; +- the convergence of policy gradient, natural policy gradient and policy mirror descent, including + linear rates and their optimality; +- the minimax regret of episodic exploration, from UCBVI and optimistic Q-learning to the + horizon-free MVP and the settling bound of Zhang–Chen–Lee–Du, matched by the lower bounds of + Domingues–Ménard–Kaufmann–Valko; +- reward-free exploration and best policy identification; +- adversarial MDPs; +- UCRL2 and average-reward sample complexity; +- pessimism in offline reinforcement learning; +- least-squares value iteration with linear function approximation. + +Build every prerequisite as a library in its own field, at the generality other fields need: +- order-unit contractions, abstract dynamic programming, span seminorms and topical maps; +- Markov processes on general measurable spaces: the Markov and strong Markov properties, + resolvents, the Dobrushin coefficient, mixing, the Poisson equation and the total-variance + identity; +- Yosida's mean ergodic theorem and group inverses, with finite Markov chains; +- Freedman's inequality, empirical Bernstein, $\ell^1$ and KL deviations of empirical laws, + covering numbers; +- the Robbins–Siegmund theorem, Robbins–Monro and asynchronous stochastic approximation; +- smooth nonconvex optimization and Bregman proximal steps on products of simplices; +- the keyed-stream model of adaptively collected data and the divergence decomposition of general + environments. + +`README.md` is the definitive specification; `Suggested.lean` records selected interfaces and is +not an exhaustive checklist. + +Suggested homes: +- `LMLExplore/MarkovDecisionProcess/` for planning; +- `LMLExplore/ReinforcementLearning/` for learning; +- the mathematical home named in each prerequisite layer. + +## Scope and dependencies + +This roadmap owns Markov decision processes and reinforcement learning: +- the planning theory of MDPs (Layers 7–13); +- learning in MDPs (Layers 14–23), with a generative model, online, adversarially, offline and with + linear function approximation; +- the prerequisites of Layers 0–6, where no other roadmap specifies them. + +| Material | Owner and interface consumed here | +| --- | --- | +| Interaction protocol, runs, trajectory measure, environments, identification algorithms | LML `SequentialLearning/`: `Algorithm`, `Environment`, `IsAlgEnvSeq`, `trajMeasure`, `stationaryEnv`, `obliviousEnv`, `IdentAlg`, `pullCount`, `streamMeasure` | +| MDPs and their environment | LML's `mdp` branch, not at the pinned version: `MDP 𝓢 𝓐 𝓡` with fields `P : Kernel (𝓢 × 𝓐) 𝓢` and `R : Kernel (𝓢 × 𝓐) 𝓡`, `MDP.env`, `MDP.policyAlg`, `MDP.meanReward`. Follow its names and shapes (Layer 7.1) | +| Episodic MDPs, episodes as rounds | entropy-mdp (Existing formalizations): `EpisodicMDP`, `augmented`, `Policy`, `statesEnv`, `BPIAlg` | +| Kernels, Ionescu–Tulcea, invariant measures, total variation | Mathlib `Probability/Kernel/`, `Kernel.traj`, `condExp_traj`, `Kernel.Invariant`, `tvDist` | +| Path laws of Markov chains; countable-state classification, recurrence, period, coupling | Tau Ceti `Probability/Process/MarkovChain.lean` (`markovChainLaw`) and the MarkovChainsAndRenewal roadmap: follow its names, and cite it for the countable-state theory | +| Ville's inequality, time-uniform sub-Gaussian bounds, method of mixtures, binary relative entropy, Bretagnolle–Huber | Bandits roadmap, Layers 0–1 and 4 (in LMLExplore) | +| FTRL, mirror descent, exponential weights, Legendre functions; implicit exploration | Bandits roadmap, Layers 6–7 | +| Design operators, ridge regression, self-normalized bounds, elliptical potential, Kiefer–Wolfowitz | Bandits roadmap, Layer 8 | +| Change of measure at stopping times for bandits, data processing for `klBer` | Identification roadmap, Layer 2 | +| Run-to-stream transfer for bandits; probability vectors | LML `Online/Bandit/ArrayProbSpace.lean`; LMLExplore `Bandits/SumRewards.lean`, `Analysis/Convex/Simplex.lean` (`simplex`) | +| Independent Bernstein inequality | built here (Layer 3.1) in the statement shape of Tau Ceti's RandomMatrices roadmap, Layer 2.1; LML `HasSubexponentialMGF` | +| KL divergence, chain rule, Pinsker, Donsker–Varadhan | Mathlib, LML `ForMathlib/InformationTheory/`, Tau Ceti `InformationTheory/KullbackLeibler/` | +| Contractions, Neumann series, Cesàro means, covering numbers, stochastic matrices, suprema over compact sets | Mathlib `ContractingWith`, `geom_series_eq_inverse`, `birkhoffAverage`, `coveringNumber`, `Matrix.rowStochastic`, `Matrix.IsIrreducible`, `Matrix.IsPrimitive`, `IsCompact.continuous_sSup` | +| Measurable selection of minimizers of jointly continuous functions | Tau Ceti `Continuous.exists_measurable_isMinOn` | + +Build missing material in this roadmap where it is listed as a target, and consume existing +implementations directly. + +Outside this roadmap: +- general function approximation: eluder dimension, Bellman rank, Bellman–eluder dimension, the + decision–estimation coefficient, and the algorithms built on them; +- policy optimization with function approximation (Q-NPG, log-linear policies), actor–critic + methods, the ODE method and two-timescale stochastic approximation; +- finite-time stochastic approximation through Moreau envelopes, linear stochastic approximation + with Markov noise beyond the TD bounds of Layer 16, rates for Robbins–Monro, asynchronous + stochastic approximation with delays or vanishing bias, variance-reduced Q-learning; +- model-free algorithms with optimal regret (UCB-Advantage, Q-EarlySettled-Advantage), UCBVI with + Bernstein bonuses [AOM17] (superseded by Layer 18), LSVI-UCB++, and optimal average-reward regret + beyond UCRL2; +- instance-dependent sample complexity of PAC learning and best policy identification, and best + policy identification algorithms other than reward-free exploration (BPI-UCBVI); +- the regret upper bound for linear mixture MDPs (UCRL-VTR+), whose source states it only up to + logarithmic factors; +- constrained, robust and risk-sensitive MDPs, preference-based RL, imitation learning, partially + observable MDPs, Markov games, Bayesian RL and Gittins indices; +- positive, negative and total-reward models and stochastic shortest paths [P, Chapter 7]; + unbounded rewards; semi-Markov and continuous-time models; +- average-reward linear programs and sensitive optimality equations [P, §§8.8–8.9, 9.3, 10.2–10.4]; + strongly polynomial bounds for policy iteration; +- optimal policies on general state spaces with infinite action sets beyond Layers 8.3 and 9.6 + (Kuratowski–Ryll-Nardzewski selection, [P, Theorem 6.2.12 (a), (d)]); +- general linear programming duality: the MDP linear programs are proved from the Bellman + equations; +- Harris recurrence, geometric drift conditions, the pointwise ergodic theorem for Markov chains, + the Markov-chain central limit theorem, general Perron–Frobenius theory, the construction of + continuous-time Markov processes and their strong Markov property at general stopping times; +- Fano's and Assouad's methods; Maurer–Pontil's empirical Bernstein inequality (Layer 3.2 replaces + it); Lyapunov's theorem for Hurwitz matrices. + +## Conventions + +**Sources and numbering.** Statements cite: +- Puterman, *Markov Decision Processes* (Wiley, 1994) as [P]; +- Agarwal, Jiang, Kakade and Sun, *Reinforcement Learning: Theory and Algorithms*, version of + 31 January 2022, as [AJKS]; +- Lattimore and Szepesvári, *Bandit Algorithms* (2020) as [LS]; +- papers by the keys of the References, with the theorem numbers of the arXiv version listed there. + +Puterman numbers decision epochs from 1 and writes λ for the discount factor. Lean rounds and steps +are numbered from 0: epoch $t$ of [P] is round $t-1$, and its λ is γ here. The first reward is +undiscounted in both. Where a source's statement contains an error, the roadmap states the corrected +statement and says so. + +**Spaces.** +- States and actions live in measurable spaces `𝓢` and `𝓐`, and every definition is made in that + generality. +- A finite action set is `[Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐]`, with + `[DecidableEq 𝓐]` where needed. Countable and standard Borel action sets are stated with + `[Countable 𝓐]` and `[StandardBorelSpace 𝓐]`. +- The learning layers 14–23 assume `[Fintype 𝓢] [Nonempty 𝓢] [MeasurableSingletonClass 𝓢]` as + well, and write $S$ = `Fintype.card 𝓢` and $A$ = `Fintype.card 𝓐`. +- Never specialize to `Fin n`. + +**Models.** +- An MDP is LML's `MDP 𝓢 𝓐 ℝ` from the `mdp` branch: a transition kernel `M.P : Kernel (𝓢 × 𝓐) 𝓢` + and a reward kernel `M.R : Kernel (𝓢 × 𝓐) ℝ`, both Markov. +- Its environment `M.env μ`, for `[Nonempty 𝓢]`, has the current state as observation and the + reward as feedback. The next state is drawn by the observation kernel from the last state and + action. +- Define these in LMLExplore with the branch's fields, names and namespaces (`MDP`, `Learning.MDP`). + When LML merges its branch, the copy is deleted. +- An episodic MDP is entropy-mdp's `EpisodicMDP 𝓢 𝓐`: transition and reward kernels indexed by + steps $h\in\mathbb N$. The horizon $H$ is an argument of every quantity that depends on it. +- The mean reward is $r(s,a)$ = `MDP.meanReward M.R (s, a)`. +- Rewards are bounded where values are defined: $|x|\le C$ for `M.R p`-almost every $x$ and every + $p$. Rewards in $[0,1]$ means `∀ p, ∀ᵐ x ∂(M.R p), x ∈ Set.Icc 0 1`. Deterministic rewards are + `M.R = Kernel.deterministic r _`, or `M.HasRewardFn r` in the episodic case. +- Learning algorithms know deterministic rewards in Layers 15–21, 22.5 and 23.2–23.3, as in the + sources. In Layers 22.1–22.4 and 23.4, rewards are observed in the data. + +**Policies.** +- A history-dependent policy is an LML `Algorithm 𝓢 𝓐 ℝ`. +- A Markov policy is `π : ℕ → Kernel 𝓢 𝓐` with Markov kernels, run as `Algorithm.markov π`. +- A stationary policy is a Markov kernel `π : Kernel 𝓢 𝓐`. +- A deterministic stationary policy is a function `π : 𝓢 → 𝓐` with a separate measurability + hypothesis, run as `MDP.policyAlg π hπ`. +- Episodic deterministic policies are the $H$-step policies `Fin H → 𝓢 → 𝓐` of entropy-mdp. + +**Criteria.** +- The discount factor is `γ : ℝ≥0` with `γ < 1`. +- Rewards are maximized. Sources stated with costs (policy mirror descent) are translated once in + Layer 17. +- Value functions are functions `𝓢 → ℝ`, and statements about them are pointwise with explicit + bounds. +- The sup norm is $\|v\|=\sup_s|v(s)|$: the norm of Layer 0.1 on a general space, Mathlib's sup + norm on `𝓢 → ℝ` for finite `𝓢`. +- "Bounded measurable" means measurable with $\sup_s|v(s)|<\infty$. + +**Episodes.** +- Steps $h 0, ∀ …`, with `C` + quantified before every problem parameter ($S$, $A$, $H$, $K$, $d$, γ, δ, ε and the MDP). +- Write logarithmic factors exactly as the source's proof gives them; never write Õ. +- Asymptotic statements are eventual inequalities, as in the Bandits roadmap. + +**Generality.** +- Each prerequisite is stated at the generality of its own field: + - Markov processes on measurable spaces, with a general totally ordered index where the + statement does not need ℕ; + - martingale inequalities for filtrations indexed by ℕ; + - operators on ordered or Banach spaces. +- A result that a source states on finite spaces is stated on measurable spaces when its proof + allows. Each layer says where it generalizes its sources. + +**Namespaces.** +- MDP definitions and their API live in the namespaces of their upstream shapes: `Learning.MDP` + (dot notation on `M`) and entropy-mdp's `Learning.MDP.Episodic`. +- Learning algorithms live in `LMLExplore.ReinforcementLearning`. +- General tools live in `LMLExplore` or in the namespace of the type they act on. +- LML's definitions keep their names. + +## Existing library and design guidance + +Consume these modules and extend their APIs rather than restating them. The pinned versions are LML +`53be244`, Mathlib `2e318fae` and Tau Ceti `cebc9b6`. + +| Foundation | Existing source | +| --- | --- | +| Law of a run, uniqueness, filtrations | LML `IonescuTulceaSpace.lean` (`trajMeasure`, `IsAlgEnvSeq.map_trajectory`, `IT.isAlgEnvSeq_trajMeasure`), `Algorithm.lean` (`IsAlgEnvSeq.filtration`, `filtrationObs`, `filtrationAction`), `Means.lean` (`IsAlgEnvSeq.condExp_feedback_comp`) | +| Divergence of runs | LML `DivergenceDecomposition.lean` (`IsAlgEnvSeq.klDiv_map_history_stepKernel`, valid for all pairs of algorithms and environments), `StoppedHistory.lean`, `IdentificationAlg.lean`; LMLExplore `SequentialLearning/DivergenceDecomposition.lean`, `SequentialLearning/BretagnolleHuber.lean` | +| Streams of samples | LML `Online/Bandit/ArrayProbSpace.lean` (`streamMeasure`), `FiniteActions.lean` (`pullCount`, `rewardByCount`); LMLExplore `Bandits/SumRewards.lean` | +| Ionescu–Tulcea and Markov chains | Mathlib `Probability/Kernel/IonescuTulcea/Traj.lean` (`Kernel.traj`, `traj_comp_partialTraj`, `condExp_traj`, `trajMeasure`), `Kernel.Invariant`, `Kernel.IsIrreducible`; Tau Ceti `markovChainLaw`, `markovChainLaw_map_eval_succ` | +| Fixed points | Mathlib `ContractingWith` (`efixedPoint'`, `apriori_dist_iterate_fixedPoint_le`, `fixedPoint_lipschitz_in_map`), `OrderHom.lfp` | +| Measurable argmax over a finite type | LML `ForMathlib/MeasureTheory/Order/MeasurableArg.lean` (`argmax`, `measurable_argmax`, root namespace; not Mathlib's `Function.argmax`) | +| Martingales and concentration | Mathlib `measure_sum_ge_le_of_hasCondSubgaussianMGF`, martingale convergence; LML `SubExponential.lean` (`measure_sum_ge_le_of_hasCondSubexponentialMGF`); LMLExplore `Probability/Martingale/Ville.lean`, `SubGaussian.lean`, `Mixture.lean`, `SelfNormalized.lean` | +| Linear algebra for linear MDPs | LMLExplore `Analysis/InnerProductSpace/DesignOperator.lean`, `EllipticalPotential.lean`, `Ridge.lean` | +| Online learning | LMLExplore `OnlineLearning/FTRL.lean`, `Bandits/WeightAlgorithm.lean`; LML `Bregman/Basic.lean` (`bregDiv_three_point`) | + +LML's history-dependent environments already give the Markov structure of runs: the observation +kernel at round $n+1$ sees the whole history. The roadmap adds the identification of state processes +with Tau Ceti's `markovChainLaw` (Layer 7.2) and the Markov property of chains (Layer 1.1). + +## Existing formalizations + +These are sources to adapt, not dependencies: +- **entropy-mdp** (Apache-2.0, `github.com/RemyDegenne/entropy-mdp`), a formalization of [EV26] + that contains: + - `EpisodicMDP`, the time-augmented MDP, $H$-step policies, `statesEnv` and `BPIAlg`; + - values, occupancy measures and Bellman recursions; + - the visit structure (`Visits.lean`) and concentration at visits; + - empirical models; + - the method of types and the time-uniform KL concentration of empirical distributions; + - self-normalized Bernstein inequalities; + - the change of measure for identification algorithms. + + Layers 3.4, 6, 7, 8, 11.4, 14 and 19 can adapt it. +- **brownian-motion** (Apache-2.0, `github.com/RemyDegenne/brownian-motion`): + - `Continuity/CoveringNumber.lean` proves the volumetric bound `coveringNumber_closedEBall_le` + of Layer 3.5; + - its stopping-time API serves Layer 1.2. + + Its reflection principle (`IsBrownianReal.reflection`) needs the strong Markov corollary for + independent increments of Layer 1.2. +- **rl-theory-in-lean** (MIT, `github.com/ShangtongZhang/rl-theory-in-lean`) [Zha25] proves the + almost-sure convergence of Q-learning and of linear TD through Robbins–Siegmund on Mathlib. It is + a source for Layers 4.1–4.3 and 16.2–16.4. + +## Layers and dependencies + +| Layer | Content | Prerequisites | +| --- | --- | --- | +| 0 | Order units, contractions and fixed points | Mathlib | +| 1 | Markov processes on general measurable spaces | Layer 0; Tau Ceti `markovChainLaw` | +| 2 | Mean ergodic theory and finite Markov chains | Layers 0–1 | +| 3 | Concentration | Bandits roadmap, Layer 1 | +| 4 | Stochastic approximation | Mathlib martingale convergence | +| 5 | Optimization | Bandits roadmap, Layer 6 | +| 6 | Sequential-learning tools: keyed streams, divergence decomposition | LML; Identification roadmap, Layer 2 | +| 7 | MDPs, policies and values | Layers 0–1, 6 | +| 8 | Finite horizon and backward induction | Layers 0, 7 | +| 9 | Discounted optimality | Layers 0–1, 7; Tau Ceti selection | +| 10 | Discounted algorithms | Layers 0–1, 9 | +| 11 | Occupancy measures and linear programming | Layers 1, 9 | +| 12 | Value-difference calculus and variance identities | Layers 1, 9, 11 | +| 13 | Average reward and sensitive discount optimality | Layers 0–2, 9–10 | +| 14 | Learning infrastructure | Layers 3, 6, 7 | +| 15 | Planning with a generative model | Layers 3, 12, 14 | +| 16 | Q-learning and temporal-difference learning | Layers 1.7, 2, 4, 9, 14 | +| 17 | Policy optimization | Layers 5, 11–12 | +| 18 | Online episodic exploration | Layers 3, 6, 12, 14 | +| 19 | Reward-free exploration and best policy identification | Layers 3.4, 18 | +| 20 | Adversarial MDPs | Layers 3.2–3.3, 7.7, 11.4, 14; Bandits roadmap, Layers 6–7 | +| 21 | Average-reward learning | Layers 3.3, 6.2, 13, 14, 15 | +| 22 | Offline reinforcement learning | Layers 3, 11, 12, 14, 15 | +| 23 | Linear function approximation | Layers 3.5, 12, 14, 18, 22; Bandits roadmap, Layer 8 | + +## Layer 0: Order units, contractions and fixed points + +General analysis, without probability. Suggested home: `Analysis/FixedPoint/`. + +1. **Bounded measurable functions.** + - Prove that the measurable functions form a closed subset of Mathlib's + `lp (fun _ : 𝓢 ↦ ℝ) ∞`, hence a complete metric space. Its norm is $\sup_s|f(s)|$ + (`lp.norm_eq_ciSup`). + - Bellman operators on a general measurable space are contractions on this space. Do not + introduce a separate bundled type. +2. **Order units and Blackwell's conditions** [Bla65], [GG04, §1]. + - Setting: an ordered real vector space $E$ with an order unit $e$: for every $x$ there is $c$ with + $-ce\le x\le ce$. Define $\|x\|_e=\inf\{c\ge0:-ce\le x\le ce\}$. + - If $T:E\to E$ is monotone and $T(x+ce)\le Tx+\gamma ce$ for all $x$ and $c\ge0$, prove + $\|Tx-Ty\|_e\le\gamma\|x-y\|_e$. + - Call $T$ *topical* if it is monotone and $T(x+ce)=Tx+ce$ for all $c\in\mathbb R$. Prove that a + topical map is nonexpansive for $\|\cdot\|_e$ and for $\mathrm{osc}_e(x)=\inf\{b-a:ae\le x\le be\}$. + - Instances, where $\|\cdot\|_e$ is the norm, so that Mathlib's `ContractingWith` applies: + - `ι → ℝ` with `[Fintype ι]`, pointwise order, $e=1$; + - the bounded measurable functions of item 1 with the pointwise order (to be defined on the + subset of `lp`) and $e=1$. + - The weighted sup norm $\max_i|x_i|/w_i$ is $\|\cdot\|_w$ for $e=w>0$. State the γ-Lipschitz + bound for it; a metric instance is not needed here. +3. **Abstract dynamic programming** [Ber22, Chapter 2]. Let $X$ be one of the instances of item 2. + Let $\{T_d\}_{d\in\mathcal D}$ be monotone maps of $X$ satisfying Blackwell's condition with a + common $\gamma<1$, and $Tx=\sup_dT_dx$ (pointwise), attained by a greedy $d$ for every $x$. Prove: + - $T$ is a γ-contraction whose fixed point is $x^*=\sup_d\mathrm{fix}(T_d)$; + - $x\ge Tx\Rightarrow x\ge x^*$ and $x\le Tx\Rightarrow x\le x^*$; + - every greedy $d$ for $x^*$ has $\mathrm{fix}(T_d)=x^*$; + - policy iteration ($d_{k+1}$ greedy for $\mathrm{fix}(T_{d_k})$) satisfies + $\mathrm{fix}(T_{d_{k+1}})\ge T\,\mathrm{fix}(T_{d_k})\ge\mathrm{fix}(T_{d_k})$ and + $\|\mathrm{fix}(T_{d_k})-x^*\|\le\gamma^k\|\mathrm{fix}(T_{d_0})-x^*\|$; + - for finite $\mathcal D$, $\mathrm{fix}(T_{d_k})=x^*$ for some $k\le|\mathcal D|$; + - modified policy iteration $x_{k+1}=T_{d_{k+1}}^{m_k+1}x_k$, with $d_{k+1}$ greedy for $x_k$ and + $Tx_0\ge x_0$, satisfies $T^kx_0\le x_k\le x^*$, hence $\|x_k-x^*\|\le\gamma^k\|x_0-x^*\|$. + + Layers 9–10 are instances of this item. +4. **The span seminorm** [P, Theorem 6.6.2, §8.5]. + - Setting: $X$ is `ι → ℝ` with `ι` finite, or the bounded measurable functions of item 1. + $\mathrm{osc}(x)=\sup x-\inf x$, and $T$ is topical with + $\mathrm{osc}(T^Jx-T^Jy)\le\alpha\,\mathrm{osc}(x-y)$ for some $J\ge1$ and $\alpha<1$. + - Prove that $T$ descends to a nonexpansive map of the quotient by constants (Mathlib's quotient + normed spaces) whose $J$-th iterate is an α-contraction. + - Deduce that there are $g\in\mathbb R$ and $h$ with $Th=h+g$. + - For relative value iteration $x_{n+1}=Tx_n-(Tx_n)(s_0)$, with $h(s_0)=0$, prove for $n\ge1$: + - $\|x_n-h\|\le\alpha^{\lfloor n/J\rfloor}\mathrm{osc}(x_0-h)$; + - $\|Tx_n-x_n-g\|\le2\alpha^{\lfloor n/J\rfloor}\mathrm{osc}(x_0-h)$. +5. **Vanishing discount for topical maps** [Koh80], [LS, Theorem 38.2]. Let $T$ be topical on + `ι → ℝ` with `ι` finite, and $v_\gamma$ the fixed point of $x\mapsto T(\gamma x)$ for $\gamma<1$. If + $\sup_\gamma\mathrm{osc}(v_\gamma)<\infty$, prove: + - there are $g,h$ with $Th=h+g$ and $\mathrm{osc}(h)\le\sup_\gamma\mathrm{osc}(v_\gamma)$; + - $(1-\gamma)v_\gamma\to g$ as $\gamma\uparrow1$; + - $\|T^nx-ng\|\le\|x-h\|+\|h\|$. +6. **Measurable maximizers.** + - For a finite index type, consume LML's `argmax`, `measurable_argmax`. + - For `ℕ` as index type, let $f_i$ be measurable functions with $\sup_jf_j(x)<\infty$ for every + $x$, and let $\varepsilon>0$. Prove that $x\mapsto\min\{i:f_i(x)>\sup_jf_j(x)-\varepsilon\}$ is + measurable. Transport it to countable types through an enumeration. + +Completion checks: the Bellman operator of a two-state, two-action MDP satisfies item 2 with $e=1$; +the max-plus map $x\mapsto(\max_jA_{ij}+x_j)_i$ is topical. + +## Layer 1: Markov processes on general measurable spaces + +Suggested homes: `Probability/Markov/` and `Probability/Kernel/`. These results need no countability +of the state space. Tau Ceti's MarkovChainsAndRenewal roadmap specifies the countable-state theory +(classification, recurrence, period, coupling). Follow its names and statement shapes: +- `markovChainLaw ν κ`; +- the path-law kernel $x\mapsto\mathbb P_x$; +- `WithTop ℕ` stopping times with `hittingAfter`; +- Mathlib's `tvDist` (values in $[0,2]$) and `Kernel.Invariant`. + +Notation. A kernel acts on bounded measurable functions by $(\kappa f)(x)=\int f\,d\kappa(x)$ and on +measures by `μ.bind κ`. Operator products are read as operators on functions: $\kappa\eta$ is +`η ∘ₖ κ` (Mathlib's monoid product `η * κ`). For kernels, $(\kappa-\kappa')u$ means +$\kappa u-\kappa'u$ pointwise. + +1. **Markov processes and the Markov property** [Kal21, Lemma 11.1, Proposition 11.2]. + - Let a process $X$ be indexed by a totally ordered type and adapted to a filtration + $\mathcal F$. Define $X$ to be $\mathcal F$-Markov with transition kernels $\kappa_{s,t}$ + ($s\le t$), satisfying Chapman–Kolmogorov, by + $\mathbb E[f(X_t)|\mathcal F_s]=(\kappa_{s,t}f)(X_s)$ almost surely for bounded measurable $f$. + - Prove that the conditional law given $\mathcal F_s$ of $(X_{t_1},\dots,X_{t_n})$, for + $s\le t_1\le\dots\le t_n$, is the iterated kernel product started at $X_s$. + - The homogeneous case is a semigroup $\kappa_t$ indexed by ℕ or `ℝ≥0`. + - Index ℕ: + - $\nu$`.bind (κ ^ n)` is the time-$n$ law of `markovChainLaw ν κ`; + - $x\mapsto\mathbb P_x$ is a Markov kernel with $\mathbb P_\nu=\nu$`.bind` $\mathbb P$; + - the shifted path $\theta_nX$ has conditional law $\mathbb P_{X_n}$ given $\mathcal F_n$, with + event and bounded-test-function forms; + - a process is Markov for its natural filtration with initial law ν if and only if its law is + `markovChainLaw ν κ`. + - Build on Mathlib's `Kernel.traj`, `condExp_traj` and `traj_comp_partialTraj`. Construct path + laws only for the index ℕ. +2. **Strong Markov property** [Kal21, Proposition 11.9]. + - For a homogeneous Markov process indexed by ℕ or `ℝ≥0` and a stopping time with countably + many values, prove: on $\{\tau<\infty\}$ and conditionally on $\mathcal F_\tau$, the + finite-dimensional laws of $(X_{\tau+t})_t$ are those of the process started at $X_\tau$. The + values of $X_\tau$ outside that event do not matter. + - Index ℕ: give the path-valued form. + - For a process with independent and stationary increments in an additive group (Mathlib's + `HasIndepIncrements`), prove that $(X_{\tau+t}-X_\tau)_t$ is independent of $\mathcal F_\tau$ + and has the law of $(X_t-X_0)_t$. +3. **First-step analysis** [Nor97, Theorems 1.3.2, 1.3.5]. Let $A$ be measurable and + $H_A=\inf\{n\ge0:X_n\in A\}$. Prove: + - $x\mapsto\mathbb P_x(H_A<\infty)$ is the minimal nonnegative solution of $h=1$ on $A$, + $h=\kappa h$ off $A$; + - $x\mapsto\mathbb E_x[H_A]\in[0,\infty]$ is the minimal solution `𝓢 → ℝ≥0∞` of $k=0$ on $A$, + $k=1+\kappa k$ off $A$; + - for measurable $f\ge0$ and $\gamma\in[0,1]$, $x\mapsto\mathbb E_x\sum_{t0$ and $\lambda\ge0$, prove that $\exp(\lambda S_n-\psi_b(\lambda)W_n)$ + is a supermartingale, with $\psi_b(\lambda)=(e^{\lambda b}-1-\lambda b)/b^2$. + - Deduce, through Ville, for $a\ge0$: + $P(\exists n,\ S_n\ge a\wedge W_n\le\sigma^2)\le\exp(-a^2/(2(\sigma^2+ab/3)))$. + - Fixed-η form: for $\eta>0$ with $\eta X_t\le1$ and $\delta\in(0,1]$, + $P(\exists n,\ S_n\ge\eta W_n+\log(1/\delta)/\eta)\le\delta$. The proof is + $e^x\le1+x+x^2$ for $x\le1$ and Ville. + - Peeled form: for $|X_t|\le b$, $N\ge1$, $K=\lceil\log_4N\rceil+1$, $\delta\in(0,1)$ and + $\ell=\max(1,\log(K/\delta))$, with probability at least $1-\delta$, for all $n\le N$: + $S_n\le3\sqrt{W_n\ell}+2b\ell$. Prove it by applying the fixed-η form to + $\eta_j=2^{-j}/b$, $j0$, mean μ and biased sample variance $V_n$, and + $x>0$, prove that with probability at least $1-3e^{-x}$, + $|\bar X_n-\mu|\le\sqrt{2V_nx/n}+3bx/n$. + - Derive it from item 1 applied to $X$ and $(X-\mu)^2$. + - The variance-aware analyses of Layers 18 and 20 use this form in place of Maurer and Pontil's. +3. **$\ell^1$ deviation of empirical laws** [WOSVW03, Theorem 2.1], [LS, Exercise 5.17]. Let ν be a + probability measure, take a measurable partition into $m$ cells, $n\ge1$ i.i.d. draws with + empirical measure $\hat\nu_n$, and $\varepsilon>0$. + - Prove $P\big(\sum_A|\hat\nu_n(A)-\nu(A)|\ge\varepsilon\big)\le(2^m-2)e^{-n\varepsilon^2/2}$. + - Prove that with probability at least $1-\delta$, + $\sum_A|\hat\nu_n(A)-\nu(A)|<\sqrt{2(\log(1/\delta)+m\log2)/n}$. + + The second form follows from the first; [LS, (5.12)] prints $m\log2$ without the factor 2. +4. **Types and categorical KL bounds** [CT06, Theorems 11.1.1, 11.1.3, 11.1.4], [JKMDLV20, + Proposition 1]. On a set of size $m\ge2$: + - there are at most $(n+1)^m$ types, and $P(\mathrm{KL}(\hat p_n,p)>\varepsilon)\le(n+1)^me^{-n\varepsilon}$; + - the likelihood ratio of every predictable sequential predictor against $p$ is a nonnegative + mean-one martingale. Laplace's predictor $q_t(i)=(N_i(t)+1)/(t+m)$ gives, by Ville, + $P\big(\exists n\ge1,\ n\,\mathrm{KL}(\hat p_n,p)>\log(1/\delta)+(m-1)\log(e(1+n/(m-1)))\big)\le\delta$. +5. **Covering numbers and uniform deviations.** + - In a real normed space of dimension $d$, for $r\ge0$ and $\varepsilon>0$, prove that the closed + ball of radius $r$ has ε-covering number at most $(1+2r/\varepsilon)^d$, with Mathlib's + `coveringNumber`. + - Prove that the image of an ε/L-cover under an $L$-Lipschitz map is an ε-cover. + - Uniform Hoeffding: let $\mathcal V$ be a class of functions with values in $[0,B]$ with an + ε-cover of cardinality $N_\varepsilon$ in the sup norm. For $n$ i.i.d. samples, prove that with + probability at least $1-\delta$, simultaneously for all $V\in\mathcal V$: + $|\frac1n\sum_iV(Y_i)-\mathbb EV|\le B\sqrt{\log(2N_\varepsilon/\delta)/(2n)}+2\varepsilon$. +6. **Least squares over a finite class** [AJKS, Lemma A.11]. + - Setting: a finite class $\mathcal F$ of functions with values in $[0,B]$; $n$ i.i.d. pairs + $(x_i,y_i)$ with $x_i\sim\nu$ and $y_i\in[0,B]$; the regression function $f^*$; and + $\varepsilon_{\mathrm{approx}}=\min_{f\in\mathcal F}\|f-f^*\|_{2,\nu}^2$. + - Prove that with probability at least $1-\delta$ the empirical risk minimizer satisfies + $\|\hat f-f^*\|^2_{2,\nu}\le20B^2\log(2|\mathcal F|/\delta)/n+3\,\varepsilon_{\mathrm{approx}}$. + - The version of 31 January 2022 states $22Y^2\log(|\mathcal F|/\delta)/n+20\varepsilon_{\mathrm{approx}}$, + but its proof bounds a second moment with the wrong range. The constants here are those of + the current draft of the book. + +Completion checks: Freedman's bound with $W_n\le nb^2$ recovers the Azuma–Hoeffding exponent up to +the constant; the KL bound for $m=2$ is a time-uniform Bernoulli bound. + +## Layer 4: Stochastic approximation + +Suggested home: `Probability/StochasticApproximation/` (`Probability/Martingale/` for item 1). + +1. **Robbins–Siegmund** [RS71, Theorem 1]. + - Let $V,a,b,c$ be adapted processes with values in `ℝ≥0`, and let + $\mathbb E[V_{n+1}|\mathcal F_n]+c_n\le(1+a_n)V_n+b_n$, with Mathlib's `condLExp` of the + coercions to `ℝ≥0∞`. + - Prove that on $\{\sum a<\infty,\sum b<\infty\}$, $V_n$ converges almost surely to a finite + limit and $\sum c_n<\infty$. +2. **Robbins–Monro** [RM51], [KY03, Chapter 5]. In a finite-dimensional real inner product space, + let $x_{n+1}=x_n-\alpha_n(h(x_n)+\xi_{n+1})$, with: + - deterministic $\alpha_n\ge0$, $\sum\alpha=\infty$ and $\sum\alpha^2<\infty$; + - $\mathbb E\|x_0-x^*\|^2<\infty$; + - martingale-difference noise with $\mathbb E[\|\xi_{n+1}\|^2|\mathcal F_n]\le A+B\|x_n-x^*\|^2$; + - $\|h(x)\|\le C(1+\|x-x^*\|)$ and $\langle x-x^*,h(x)\rangle>0$ for $x\ne x^*$, uniformly on + annuli: $\inf\{\langle x-x^*,h(x)\rangle:\varepsilon\le\|x-x^*\|\le1/\varepsilon\}>0$ for every + $\varepsilon\in(0,1)$. + + Prove $x_n\to x^*$ almost surely, from item 1. +3. **Asynchronous stochastic approximation** [Tsi94, Theorems 1, 3]. On a finite index `ι`, let + $x_i(t+1)=x_i(t)+\alpha_i(t)(F_i(x(t))-x_i(t)+w_i(t))$, with: + - $\alpha_i(t)\in[0,1]$ adapted, $\sum_t\alpha_i(t)=\infty$ almost surely, and + $\sum_t\alpha_i(t)^2\le C$ for a deterministic $C$; + - $w_i(t)$ $\mathcal F(t+1)$-measurable with $\mathbb E[w_i(t)|\mathcal F(t)]=0$ and + $\mathbb E[w_i(t)^2|\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$; + - $F$ a pseudo-contraction for a weighted sup norm, with fixed point $x^*$: + $\|F(x)-x^*\|_w\le\beta\|x-x^*\|_w$ with $\beta<1$. + + Prove that $x(t)$ is almost surely bounded and converges almost surely to $x^*$. + +Completion checks: Robbins–Monro for the sample mean is the strong law; item 3 with $F$ constant is +a family of independent averaging recursions. + +## Layer 5: Optimization + +Suggested homes: `Optimization/`, `Analysis/SpecialFunctions/`, `OnlineLearning/`. + +1. **Softmax.** On a finite type define: + - `softmax θ` $=\exp\theta/\sum\exp\theta$, with values in LMLExplore's `simplex`; + - `logSumExp`. + + Prove the Jacobian $\mathrm{diag}(\pi)-\pi\pi^\top$, the convexity of `logSumExp`, its gradient + `softmax`, and the Gibbs variational formula on a finite type (the finite case of Tau Ceti's + Donsker–Varadhan). +2. **Smooth optimization** [Nes18, Lemma 1.2.3], [KNS16, Theorem 1], [AKLM21, Proposition B.1, + Theorem E.1], [MXSS20, Lemmas 7–8]. In a real inner product space, prove: + - the descent lemma for $L$-smooth functions; + - for $L$-smooth $f$ satisfying the Polyak–Łojasiewicz inequality + $\frac12\|\nabla f\|^2\ge\mu(f^*-f)$, gradient ascent with step $1/L$ gives + $f^*-f(x_k)\le(1-\mu/L)^k(f^*-f(x_0))$; + - for $a\ge0$ and $\delta_k\ge0$, the recursion $\delta_{k+1}\le\delta_k-a\delta_k^2$ gives + $\delta_k\le\delta_0/(1+a\delta_0k)$; + - projected gradient ascent on a closed convex set $C$, with $G_\eta(x)=(P_C(x+\eta\nabla f(x))-x)/\eta$: + for $\eta=1/L$, $\min_{t0$, a measurable deterministic stationary $\varepsilon$-optimal policy exists, + by Layer 0.6. +6. **Compact action sets.** + - (a) [P, Theorem 6.2.10 (c)]. Prove the existence of an optimal deterministic stationary policy + for countable `𝓢` with measurable singletons and compact metrizable `𝓐`, with $r(s,\cdot)$ + upper semicontinuous and $P(s,\cdot)\{s'\}$ lower semicontinuous. + - (b) Prove the same for a topological `𝓢` with open sets measurable and a compact Polish `𝓐`, + when $r$ is continuous and $P$ is weakly continuous (Feller): + $(s,a)\mapsto\int f\,dP(s,a)$ is continuous for bounded continuous $f$. + - $T$ maps bounded continuous functions to bounded continuous functions; for the supremum over + a compact set use Mathlib's `IsCompact.continuous_sSup`. + - The fixed point is continuous. + - A measurable greedy selector exists by Tau Ceti's `Continuous.exists_measurable_isMinOn`. + +Completion checks: for $\gamma=0$ the optimal policy is myopic; the example of [P, Example 6.2.2] +(one state, actions $\mathbb N_{\ge1}$, $r(a)=1-1/a$) has no optimal policy; in a two-state MDP +whose optimal policy depends on γ, compute $v^*$ in closed form on both sides of the threshold. + +## Layer 10: Discounted algorithms + +Throughout, $0\le\gamma<1$, `𝓐` is finite, $T$ is `M.bellman γ`, and $\|\cdot\|$ is the sup norm of +Layer 0.1. Statements are pointwise inequalities with the constants shown. + +1. **Value iteration** [P, Theorem 6.3.1, Proposition 6.3.2, Theorem 6.3.3]. Let $v_n=T^nv_0$ and + $B=\|v_1-v_0\|$. Prove: + - $\|v_n-v^*\|\le\gamma^nB/(1-\gamma)$; + - if $2\gamma\|v_{n+1}-v_n\|<\varepsilon(1-\gamma)$, the policy greedy for $v_{n+1}$ is + $\varepsilon$-optimal and $\|v_{n+1}-v^*\|<\varepsilon/2$; + - the policy greedy for $v_n$ satisfies $\|v^{d_n}-v^*\|\le2\gamma^nB/(1-\gamma)$; + - the iterates are monotone from the first $n$ with $Tv_n\le v_n$ (resp. $\ge$). +2. **Policy iteration** [P, Proposition 6.4.1, Theorem 6.4.2, Propositions 6.4.3–6.4.4, Lemma 6.4.5, + Theorem 6.4.6]. Derive from Layer 0.3: + - policy iteration, with ties kept at the current action, improves monotonically; + - $T^nv^{d_0}\le v^{d_n}\le v^*$, so $\|v^{d_n}-v^*\|\le\gamma^n\|v^{d_0}-v^*\|$; + - for finite `𝓢`, it reaches an optimal policy after at most $|\mathcal A|^{|\mathcal S|}$ + improvements. + + Prove the Newton form $v_{n+1}=v_n+(I-\gamma P_{d_{n+1}})^{-1}(Tv_n-v_n)$ and the support + inequality $Tu-u\ge Tv-v+(\gamma P_{d_v}-I)(u-v)$. +3. **Modified policy iteration** [P, §6.5, Proposition 6.5.1]. + - Derive from Layer 0.3 the convergence of $v_{n+1}=(T_{d_{n+1}})^{m_n+1}v_n$, with $d_{n+1}$ + greedy for $v_n$, from any $v_0$ with $Tv_0\ge v_0$, for example + $v_0=(1-\gamma)^{-1}\inf_{s,a}r(s,a)$. + - Prove the expansion $v_{n+1}=v_n+\sum_{k\le m_n}(\gamma P_{d_{n+1}})^k(Tv_n-v_n)$. +4. **Bounds and stopping** [P, Theorem 6.6.3, Corollary 6.6.4, Proposition 6.6.5]. For bounded + measurable $v$, $d$ greedy for $v$ and $m\ge-1$, prove: + $$v+\sum_{k=0}^m(\gamma P_d)^k(Tv-v)+\frac{\gamma^{m+1}}{1-\gamma}\inf(Tv-v)\le v^d\le v^*\le + T^{m+1}v+\frac{\gamma^{m+1}}{1-\gamma}\sup(Tv-v).$$ + - For $m\in\{-1,0\}$ this is [P, Corollary 6.6.4]. + - For $m\ge1$, the upper bound of [P, (6.6.9)], with $\sum_k(\gamma P_d)^k$ in place of + $T^{m+1}$, is false. A two-state counterexample with $\gamma=1/2$ and a tie in the greedy choice + shows it; the corrected bound is stated here. + + Prove the stopping rule of [P, Proposition 6.6.5] in the form + $\gamma\,\mathrm{sp}(Tv-v)<(1-\gamma)\varepsilon$. +5. **Span contraction** [P, Proposition 6.6.1, Theorem 6.6.6, Corollary 6.6.7]. + - Let $\delta_M=\sup_{(s,a),(s',a')}\mathrm{tvDist}(P(s,a),P(s',a'))/2$. Prove + $\mathrm{sp}(Tu-Tv)\le\gamma\,\delta_M\,\mathrm{sp}(u-v)$ on general `𝓢`. + - Prove $\mathrm{sp}(T^2v-Tv)\le\gamma\,\delta_M\,\mathrm{sp}(Tv-v)$. +6. **Action elimination** [P, Proposition 6.7.1, Corollary 6.7.2, Proposition 6.7.3]. + - If $Q^*(s,a') 0 with $\sum\alpha=1$. + - The primal is: minimize $\sum_s\alpha(s)v(s)$ subject to + $v(s)\ge r(s,a)+\gamma\sum_{s'}P(s'|s,a)v(s')$. + - The dual is: maximize $(1-\gamma)^{-1}\sum r\,x$ over the probability measures $x$ satisfying the + flow equation of item 1 with μ = α. + - Prove: primal feasibility is $v\ge Tv$; $v^*$ is the unique primal optimum; both optimal values + equal $\langle\alpha,v^*\rangle$. + - Prove that dual optima are exactly the occupancy measures of optimal stationary policies + [P, Theorem 6.9.4]. + - Prove that the extreme points of the flow polytope (Mathlib's `Set.extremePoints`) are exactly + the occupancy measures of deterministic stationary policies [P, Proposition 6.9.3]. + - Prove that the set of optimal deterministic policies does not depend on α [P, Proposition + 6.9.5]. + - Prove all of this from Layers 9.3–9.4 and 11.2, without a general LP duality theorem. +4. **Episodic occupancy.** For an episodic MDP and a Markov policy: + - define $d^\pi_h=\mathrm{law}(S_h,A_h)$; + - prove the flow $\sum_ad_{h+1}(\cdot,a)=P_h\circ_md_h$ with $d_0=\mu\otimes_m\pi_0$; + - prove $\mathbb E_\pi\sum_hf_h(S_h,A_h)=\sum_h\langle d^\pi_h,f_h\rangle$. + + For standard Borel `𝓐`, prove that every sequence of probability measures $d_h$ on `𝓢 × 𝓐` + satisfying the flow, with the first marginal of $d_0$ equal to μ, is realized by the Markov policy + obtained by disintegrating $d_h$ (for finite spaces $\pi_h(a|s)=d_h(s,a)/d_h(s)$). For finite + spaces, the occupancy polytope of an episodic MDP is the domain of Layer 20. + +Completion checks: for $\gamma=0$ the occupancy measure is $\mu\otimes\pi$; in a one-state MDP the +dual LP is a bandit's simplex. + +## Layer 12: Value-difference calculus and variance identities + +These identities hold on measurable spaces with bounded functions. Items involving optimal or greedy +policies assume `𝓐` finite. Where the source states them for finite spaces, state them in this +generality. Here $\|\cdot\|$ is the sup norm, and an estimated model $\hat M$ has the mean reward of +$M$. + +1. **The extended value-difference identity** [JYW21, Lemma A.1]. + - Let $\hat Q_h$ be bounded measurable, let $\hat\pi,\pi$ be Markov policies, and set + $\hat V_h(s)=\int\hat Q_h(s,a)\,\hat\pi_h(da|s)$ with $\hat V_H=0$. Prove + $$\hat V_0(s)-V^\pi_0(s)=\sum_h\mathbb E^\pi_s\big[\langle\hat Q_h(S_h,\cdot),\hat\pi_h(\cdot|S_h)-\pi_h(\cdot|S_h)\rangle\big]+\sum_h\mathbb E^\pi_s\big[(\hat Q_h-r_h-P_h\hat V_{h+1})(S_h,A_h)\big].$$ + - State the discounted analogue, with $(1-\gamma)^{-1}$ and the occupancy measure of Layer 11.1. +2. **Corollaries.** The first two are instances of Layer 1.5. + - The performance difference lemma [AJKS, Lemma 1.16], for every algorithm and stationary + $\pi'$: `M.runValue γ alg μ` $-\int v^{\pi'}d\mu=(1-\gamma)^{-1}\int A^{\pi'}\,d\,$`occupancy`. + Give its episodic form. + - The simulation lemma [AJKS, Lemma 2.2]: $Q^\pi_M-Q^\pi_{\hat M}=\gamma R_\gamma(\hat P^{\pi}_{SA})(P-\hat P)v^\pi_M$. + Give its episodic form and, for rewards in $[0,1]$, the bound + $\|Q^\pi_M-Q^\pi_{\hat M}\|\le\gamma(1-\gamma)^{-2}\sup_{s,a}\mathrm{tvDist}(P(s,a),\hat P(s,a))$. + - The componentwise bounds [AJKS, Lemma 2.5]: + $\gamma R_\gamma(\hat P^{\hat\pi^*}_{SA})(P-\hat P)v^*\le Q^*-\hat Q^*\le\gamma R_\gamma(\hat P^{\pi^*}_{SA})(P-\hat P)v^*$. + - The greedy bound [AJKS, Lemma 1.11]: the policy greedy for $Q$ has + $v^{\pi_Q}\ge v^*-2\|Q-Q^*\|/(1-\gamma)$. + - The episodic greedy bound [AJKS, Lemma 3.4]: if + $\|\hat Q_h-r_h-P_h\max\hat Q_{h+1}\|\le\varepsilon$ for all $h$, then + $\|\hat Q_h-Q^*_h\|\le(H-h)\varepsilon$ and $V^{\hat\pi}_0\ge V^*_0-2H^2\varepsilon$. + - The optimistic decomposition: if $\hat V_H=0$, $\hat V_h(s)\le\int\hat Q_h(s,a)\,\hat\pi_h(da|s)$ + and $\hat Q_h\le r_h+b_h+\hat P_h\hat V_{h+1}$, then + $\hat V_0-V^{\hat\pi}_0\le\sum_h\mathbb E^{\hat\pi}[(b_h+(\hat P_h-P_h)\hat V_{h+1})(S_h,A_h)]$. + - The pessimistic decomposition [JYW21, Theorem 4.2, deterministic part]. Let pessimistic value + iteration be $\hat Q_h=\min(\hat B_h\hat V_{h+1}-\Gamma_h,H-h)^+$ and $\hat V_h=\max_a\hat Q_h$, + with arbitrary estimates $\hat B_h$ and greedy policy $\hat\pi$. If + $|\hat B_h\hat V_{h+1}-B_h\hat V_{h+1}|\le\Gamma_h$ pointwise, prove + $V^*_0-V^{\hat\pi}_0\le2\sum_h\mathbb E^{\pi^*}[\Gamma_h(S_h,A_h)]$. + - The policy-mixture lemma [AJKS, Lemma 14.1]: for $\pi'=(1-\alpha)\pi+\alpha\pi''$, the state + marginals of the occupancy measures from μ satisfy `tvDist` $\le2\alpha\gamma/(1-\gamma)$. The + state–action occupancy measures satisfy `tvDist` $\le2\alpha/(1-\gamma)$. +3. **Variance identities.** These are instances of Layer 1.9. + - [AJKS, Lemma 2.11], for a deterministic stationary π: the variance $\Sigma^\pi(s,a)$ of the + discounted return started from $(s,a)$ satisfies + $\Sigma^\pi=\gamma^2\mathrm{Var}_P(v^\pi)+\gamma^2P^\pi_{SA}\Sigma^\pi$. For rewards in $[0,1]$, + $\|\Sigma^\pi\|\le\gamma^2/(1-\gamma)^2$. For randomized π, state the corollary of Layer 1.9 on + the state–action chain, with $\mathrm{Var}_{P^\pi_{SA}}(Q^\pi)$ in place of $\mathrm{Var}_P(v^\pi)$. + - The total-variance lemma [AJKS, Lemma 2.12]: for rewards in $[0,1]$ and every stationary π, + $\|R_\gamma(P^\pi_{SA})\sqrt{\mathrm{Var}_P(v^\pi)}\|\le\sqrt{2/(1-\gamma)^3}$. + - Its sharpening [LWCGC24, Lemma 11]: for $0<\gamma<1$ and $r_\pi\ge0$, + $\|R_\gamma(P_\pi)\sqrt{\mathrm{Var}_{P_\pi}(v^\pi)}\|\le4\|v^\pi\|/(\gamma\sqrt{1-\gamma})$. + - The episodic law of total variance: for a Markov policy, rewards in $[0,1]$ and every initial + state $s$, $\mathbb E^\pi_s\sum_h\mathrm{Var}_{P_h(S_h,A_h)}(V^\pi_{h+1})\le\mathrm{Var}^\pi_s\big(\sum_hr_h(S_h,A_h)\big)\le H^2$, + with equality in the first inequality for deterministic policies. + +Completion checks: the performance difference of a policy with itself is zero; the simulation lemma +with $\hat P=P$ is trivial; the total-variance bound is attained up to constants by a two-state +chain with an absorbing rewarding state. + +## Layer 13: Average reward and sensitive discount optimality + +Throughout, `𝓢` and `𝓐` are finite unless an item says otherwise, and $P_\pi^*$ and $D_\pi$ are +the limiting and deviation matrices of Layer 2 of `M.stateKernel π`. + +1. **Markov reward processes** [P, §8.2]. + - Define the gain `M.gain π` $=P^*_\pi r_\pi$ and the bias `M.bias π` $=D_\pi r_\pi$. + - Prove that the gain is the Cesàro limit of $\frac1N\sum_{n0$ such that, + for all MDPs and all $\delta\in(0,1)$, with probability at least $1-\delta$, + $$\|Q^*-\hat Q^*\|\le\gamma\sqrt{\frac{C\log(CSA/\delta)}{(1-\gamma)^3N}}+\frac{C\gamma\log(CSA/\delta)}{(1-\gamma)^3N}.$$ + The proof runs through Bernstein for $(P-\hat P)v^*$, a variance comparison, and Layer 12.3 under + the empirical MDP. +3. **The plug-in policy is minimax optimal** [AKY20, Theorem 1]. + - Statement: there is $C>0$ such that, for $\gamma\ge1/2$, $\varepsilon\in(0,(1-\gamma)^{-1/2}]$ + and $N\ge C\gamma\log(CSA/((1-\gamma)\delta))/((1-\gamma)^3\varepsilon^2)$, with probability at + least $1-\delta$, every policy $\hat\pi$ with $\|\hat Q^{\hat\pi}-\hat Q^*\|\le\varepsilon_{\mathrm{opt}}$ + satisfies $Q^{\hat\pi}\ge Q^*-\varepsilon-9\varepsilon_{\mathrm{opt}}/(1-\gamma)$. + - Build the absorbing-MDP API it needs: replace the row of one state by an absorbing transition + with reward $(1-\gamma)u$, compare values, and use a finite net of values $u$. The independence + of Layer 14.3 across keys gives the decoupling. +4. **The full range of accuracies** [LWCGC24]. + - (a) Theorem 4, finite horizon, with the episodic generative model of Layer 14.3: there is + $C>0$ such that, for $\varepsilon\in(0,H]$ and $N\ge CH^3\log(HSA/\delta)/\varepsilon^2$ + samples per $(h,s,a)$, with probability at least $1-\delta$, the optimal policy of the + empirical episodic MDP is $\varepsilon$-optimal at every step. + - (b) Lemma 1, policy evaluation, for a policy π fixed independently of the data: if + $N\ge32e^2(1-\gamma)^{-1}\log(4S\log(e/(1-\gamma))/\delta)$, then with probability at least + $1-\delta$, $\|\hat v^\pi-v^\pi\|\le6\sqrt{2\log(4S\log(e/(1-\gamma))/\delta)/(N(1-\gamma)^3)}$. + - (c) Theorem 1, perturbed plug-in. Let $r_p=r+\zeta$ with $\zeta(s,a)$ i.i.d. uniform on + $[0,\xi]$ and $\xi=c_1(1-\gamma)\varepsilon/(S^5A^5)$, independent of the samples; here the + probability is over `streamMeasure M.P` and the law of ζ. Prove: there are $c_0,c_1>0$ such + that, for $\varepsilon\in(0,1/(1-\gamma)]$ and + $N\ge c_0\log(SA/((1-\gamma)\varepsilon\delta))/((1-\gamma)^3\varepsilon^2)$, the optimal + policy $\hat\pi_p$ of $(\hat P,r_p)$ satisfies $V^{\hat\pi_p}\ge V^*-\varepsilon$ and + $Q^{\hat\pi_p}\ge Q^*-\gamma\varepsilon$ with probability at least $1-\delta$. +5. **Lower bound** [AMK13, Theorem 3], corrected. + - [AMK13] uses a family of two MDPs with a common self-loop probability. Samples at different + pairs then carry information about one another, and the proof's independence claim fails. + - Use the product family instead: the self-loop probability of each hard pair is chosen + independently in $\{p,p+\alpha\}$, with the source's $p$ and α. + - With one action set for all states, the source's class has $K$ states with $A$ actions and + $2KA$ states whose actions all behave alike, so $S=K(1+2A)$ and there are $KA$ hard pairs. + - Prove: there are $C,\varepsilon_0,\delta_0>0$ such that, for $\gamma\ge2/5$, + $\varepsilon\in(0,\varepsilon_0]$ and $\delta\in(0,\delta_0/(KA))$, every algorithm querying + `stationaryEnv M.P` adaptively for $T$ rounds whose estimate of $Q^*$ is ε-accurate with + probability at least $1-\delta$ on every MDP of the family has + $T\ge KA\log(KA/(C\delta))/(C(1-\gamma)^3\varepsilon^2)$. + - Use the change of measure of Layer 6.2 at the fixed budget $T$. + +Completion check: item 4 (a) for $H=1$ is a statement about one-step rewards. + +## Layer 16: Q-learning and temporal-difference learning + +1. **Definitions.** Rewards are deterministic, as in Layer 15. + - Synchronous Q-learning on the generative model, for $t\ge1$: + $Q_t=(1-\eta_t)Q_{t-1}+\eta_t(r+\gamma\max_aQ_{t-1}(X_t(\cdot),a))$, with $X_t(s,a)$ the $t$-th + sample and $0\le Q_0\le1/(1-\gamma)$. + - Asynchronous Q-learning along a run of any algorithm in `M.env μ`: the learning rate + $\alpha_t(s,a)$ is measurable for LML's `filtrationAction` at round $t$ (the history through + $(S_t,A_t)$), and vanishes off $(S_t,A_t)$. + - Tabular TD(0) is the case of one action. +2. **Almost-sure convergence** [Tsi94, Theorem 4 (a)]. + - For asynchronous Q-learning with learning rates in $[0,1]$, $\sum_t\alpha_t(s,a)=\infty$ + almost surely and $\sum_t\alpha_t(s,a)^2\le C$ for a deterministic $C$ and every pair, prove + that $Q_t\to Q^*$ almost surely. + - Use Layer 4.3 with the γ-contraction of Layer 9.4 in the sup norm. The source minimizes costs; + translate. +3. **The sample complexity of Q-learning** [LCCWC24]. All constants are in "∃ C" form. + - (a) Theorem 2: there are $c_1,c_2,C>0$ such that, for $\gamma\in[1/2,1)$, $\varepsilon\in(0,1]$, + $\delta\in(0,1)$, $T\ge2$, learning rates with + $1/(1+c_1(1-\gamma)T/\log^3T)\le\eta_t\le1/(1+c_2(1-\gamma)t/\log^3T)$ and + $T\ge C\log^4T\log(SAT/\delta)/((1-\gamma)^4\varepsilon^2)$, $\|Q_T-Q^*\|\le\varepsilon$ with + probability at least $1-\delta$. + - (b) Theorem 1, TD: the same with $\log^2T$ in the learning-rate window and + $T\ge C\log^3T\log(ST/\delta)/((1-\gamma)^3\varepsilon^2)$. + - (c) Theorem 3: there is $C>0$ such that, for every $\gamma\in[3/4,1)$, there is a four-state, + two-action MDP such that, for every $T\ge C/(1-\gamma)^2$, Q-learning from $Q_0=0$ with + $\eta_t=1/(1+c_\eta(1-\gamma)t)$, or with a constant $\eta\in(0,1)$, has + $\max_s\mathbb E(V_T(s)-V^*(s))^2\ge1/(C(1-\gamma)^4T\log^2T)$. +4. **TD with linear function approximation.** Let $(P_\pi,r_\pi)$ be the Markov reward process of a + stationary policy on finite `𝓢`, with invariant law ν (Layer 2) and $D=\mathrm{diag}(\nu)$. Let + $\varphi:\mathcal S\to E$ map into a finite-dimensional inner product space, with $\|\varphi\|\le1$ + and $\sum_s\nu(s)\varphi(s)\varphi(s)^\top\succeq\omega I$, $\omega>0$. + - Projected Bellman geometry [TVR97, Lemmas 1, 4, 6, Theorem 1 and footnote 1], [BRS18, (5)]: + - $P_\pi$ is a nonexpansion of $\|\cdot\|_D$; + - the projected Bellman operator is a contraction with a unique fixed point $\theta^*$; + - $\|\Phi\theta^*-v\|_D\le(1-\gamma^2)^{-1/2}\|\Pi v-v\|_D$. + - Mean-path TD [BRS18, Lemmas 3–4, Theorem 1]: + - $(\theta^*-\theta)^\top\bar g(\theta)\ge(1-\gamma)\|V_{\theta^*}-V_\theta\|_D^2$; + - $\|\bar g(\theta)\|\le2\|V_\theta-V_{\theta^*}\|_D$; + - with step $(1-\gamma)/4$: $\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le4\|\theta^*-\theta_0\|^2/(T(1-\gamma)^2)$ + and $\|\theta^*-\theta_T\|^2\le e^{-(1-\gamma)^2\omega T/4}\|\theta^*-\theta_0\|^2$. + - i.i.d. observations [BRS18, Theorem 2], with $\sigma^2=\mathbb E\|g_t(\theta^*)\|^2$: + - (a) for $T\ge64/(1-\gamma)^2$ and step $1/\sqrt T$, + $\mathbb E\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le(\|\theta^*-\theta_0\|^2+2\sigma^2)/(\sqrt T(1-\gamma))$; + - (b) for a constant step $\alpha_0\le\omega(1-\gamma)/8$, + $\mathbb E\|\theta^*-\theta_T\|^2\le e^{-\alpha_0(1-\gamma)\omega T}\|\theta^*-\theta_0\|^2+2\alpha_0\sigma^2/((1-\gamma)\omega)$; + - (c) for steps $\beta/(\lambda+t)$ with $\beta=2/((1-\gamma)\omega)$ and + $\lambda=16/((1-\gamma)^2\omega)$, $\mathbb E\|\theta^*-\theta_T\|^2\le\kappa/(\lambda+T)$ with + $\kappa=\max\{8\sigma^2/((1-\gamma)^2\omega^2),16\|\theta^*-\theta_0\|^2/((1-\gamma)^2\omega)\}$. + - Almost-sure convergence of TD(0) with i.i.d. observations and steps with $\sum\alpha=\infty$, + $\sum\alpha^2<\infty$, from Layer 4.2 [Zha25]. + - Markovian observations [BRS18, Theorem 3]: projected TD started from the invariant law, with + projection radius $R\ge\|\theta^*\|$, $G=r_{\max}+2R$ and the geometric mixing of Layer 1.7. Prove + the bounds (a)–(c) of the source with $\tau_{\mathrm{mix}}(\varepsilon)=\min\{t:m\rho^t\le\varepsilon\}$. + +Completion checks: with one state, Q-learning is a stochastic approximation of a scalar fixed point +and item 3 reduces to averages of i.i.d. samples; TD with tabular features has $\theta^*=v^\pi$. + +## Layer 17: Policy optimization + +Finite `𝓢`, `𝓐`, exact values unless stated. ρ is the evaluation law, μ the starting law of the +optimization, and $d^\pi_\rho$ the state marginal of the occupancy measure. Mismatch coefficients +$\|d^{\pi^*}_\rho/\mu\|_\infty$ and $\|1/\mu\|_\infty$ are taken in `ℝ≥0∞`, or the items assume μ +of full support. Iterates are indexed from 0. Sources stated with costs are translated by +$r\mapsto1-r$, which leaves the constants unchanged. + +1. **Policy gradient theorem** [AJKS, Theorem 11.4]. + - For a parametrization $\theta\mapsto\pi_\theta$ differentiable on an open set of a + finite-dimensional real normed space, prove + $\nabla V^{\pi_\theta}(\mu)=(1-\gamma)^{-1}\mathbb E_{s\sim d^{\pi_\theta}_\mu}\sum_a\nabla\pi_\theta(a|s)\,Q^{\pi_\theta}(s,a)$, + from the derivative of $(I-\gamma P_\pi)^{-1}$. + - Derive the advantage form, and for $\pi_\theta>0$ the REINFORCE form in its causal version + $\mathbb E\sum_t\gamma^tr_t\sum_{t'\le t}\nabla\log\pi_\theta(A_{t'}|S_{t'})$. +2. **Direct parametrization** [AKLM21, Lemma 4.1, Lemma D.3, Theorem 4.1]. Values are + differentiated within the product of simplices (`HasFDerivWithinAt`). For $0<\gamma<1$: + - gradient domination: + $V^*(\rho)-V^\pi(\rho)\le(1-\gamma)^{-1}\|d^{\pi^*}_\rho/\mu\|_\infty\max_{\bar\pi}(\bar\pi-\pi)^\top\nabla_\pi V^\pi(\mu)$; + - smoothness with constant $2\gamma A/(1-\gamma)^3$; + - projected gradient ascent with step $(1-\gamma)^3/(2\gamma A)$ has + $\min_{t64\gamma SA\|d^{\pi^*}_\rho/\mu\|^2_\infty/((1-\gamma)^6\varepsilon^2)$. +3. **Softmax parametrization** [MXSS20], [AKLM21, Theorem 5.1]. Prove: + - the gradient formula + $\partial_{\theta_{s,a}}V^{\pi_\theta}(\mu)=(1-\gamma)^{-1}d^{\pi_\theta}_\mu(s)\pi_\theta(a|s)A^{\pi_\theta}(s,a)$; + - smoothness with constant $8/(1-\gamma)^3$ [MXSS20, Lemma 7]; + - the non-uniform Łojasiewicz inequality [MXSS20, Lemma 8]; + - asymptotic convergence [AKLM21, Theorem 5.1]: for μ of full support and step at most + $(1-\gamma)^3/8$, $V^{(t)}(s)\to V^*(s)$ for every $s$. + + Assume that every state has a unique optimal action $a^*(s)$. Prove: + - $c=\inf_{t,s}\pi_t(a^*(s)|s)>0$ [MXSS20, Lemma 9]; + - with step $(1-\gamma)^3/8$, for $t\ge1$, + $V^*(\rho)-V^{\pi_t}(\rho)\le16S\|d^{\pi^*}_\mu/\mu\|^2_\infty\|1/\mu\|_\infty/(c^2(1-\gamma)^6t)$ + [MXSS20, Theorem 4]; + - the eventual lower bound [MXSS20, Theorem 10]; + - the bandit case [MXSS20, Theorems 3, 9]. +4. **Log-barrier regularization** [AKLM21, Theorem 5.2, Corollary 5.1], corrected. + - The objective is $L_\lambda(\theta)=V^{\pi_\theta}(\mu)+\frac\lambda{SA}\sum_{s,a}\log\pi_\theta(a|s)$. + - If $\|\nabla L_\lambda(\theta)\|\le\lambda/(2SA)$, then + $V^*(\rho)-V^{\pi_\theta}(\rho)\le2\lambda\|d^{\pi^*}_\rho/\mu\|_\infty/(1-\gamma)$. + - With $\theta_0=0$, $\varepsilon\le1/(1-\gamma)$, + $\lambda=\varepsilon(1-\gamma)/(2\|d^{\pi^*}_\rho/\mu\|_\infty)$, step $1/\beta_\lambda$ and + $\beta_\lambda=8/(1-\gamma)^3+2\lambda/S$, gradient ascent has + $\min_{t0$ and $T\ge1$: + $V^{(T)}(\rho)\ge V^*(\rho)-\log A/(\eta T)-1/((1-\gamma)^2T)$. +6. **Policy mirror descent.** + - [Xiao22, Theorems 8, 10]. For a Legendre mirror map on the simplex in every state (Bandits + roadmap, Layer 6) and $D^*_0=\sum_sd_\rho(\pi^*)(s)D(\pi^*_s,\pi^{(0)}_s)$: + - with a constant step η, + $V^*_\rho-V_\rho(\pi^{(k)})\le\frac1{k+1}\big(\frac{D_0^*}{\eta(1-\gamma)}+\frac1{(1-\gamma)^2}\big)$; + - if $\pi^{(0)}$ lies in the relative interior and $\eta_{k+1}\ge\eta_k\vartheta_\rho/(\vartheta_\rho-1)$ + with $\vartheta_\rho=\|d_\rho(\pi^*)/\rho\|_\infty/(1-\gamma)$, then + $V^*_\rho-V_\rho(\pi^{(k)})\le(1-1/\vartheta_\rho)^k\big(V^*_\rho-V_\rho(\pi^{(0)})+D^*_0/(\eta_0\gamma)\big)$. + - [JPR23, Theorems 4.1, 4.2]. With steps + $\eta_k\ge c_k^{-1}\max_s\min_{p\in\Delta(\arg\max Q^k(s,\cdot))}D(p,\pi^k_s)$: + $\|v^*-v^k\|\le\gamma^k\big(\|v^*-v^0\|+\sum_{i=1}^k\gamma^{-i}c_{i-1}\big)$. For every $n$ there + are MDPs with $2n+1$ states and an initial policy on which every positive step sequence gives + $\|v^*-v^k\|\ge\frac12\gamma^k\|v^*-v^0\|$ for $k 0. Define the entropy $\mathcal H(\rho,\pi)=(1-\gamma)^{-1}\mathbb E_{d^\pi_\rho}\sum_a\pi\log(1/\pi)$, + the soft value $V^\pi_\tau=V^\pi+\tau\mathcal H(\rho,\pi)$ and the soft Bellman operator. + - Prove that the soft Bellman operator is a γ-contraction whose fixed point $Q^*_\tau$ gives the + soft-optimal policy $\pi^*_\tau\propto\exp(Q^*_\tau/\tau)$. + - Define the update $\pi^{(t+1)}\propto(\pi^{(t)})^{1-\eta\tau/(1-\gamma)}\exp(\eta Q^{(t)}_\tau/(1-\gamma))$, + from $\pi^{(0)}>0$. + - For $0<\eta\le(1-\gamma)/\tau$ and + $C_1=\|Q^*_\tau-Q^{(0)}_\tau\|+2\tau(1-\eta\tau/(1-\gamma))\|\log\pi^*_\tau-\log\pi^{(0)}\|$, prove + $\|Q^*_\tau-Q^{(t+1)}_\tau\|\le C_1\gamma(1-\eta\tau)^t$ and + $\|\log\pi^*_\tau-\log\pi^{(t+1)}\|\le2C_1\tau^{-1}(1-\eta\tau)^t$. + - With soft Q-values estimated within δ and $C_2=(2\delta/(1-\gamma))(1+\gamma/(\eta\tau))$, prove + the bounds $\gamma((1-\eta\tau)^tC_1+C_2)$ and $2\tau^{-1}((1-\eta\tau)^tC_1+C_2)$. +8. **Conservative policy iteration** [AJKS, §14.1, Theorems 14.2–14.4]. For $\gamma\in[1/5,1)$: + - CPI mixes $\pi_{t+1}=(1-\alpha)\pi_t+\alpha\pi'_t$, where $\pi'_t$ is returned by an + ε-greedy oracle over a policy class Π; + - $\mathbb A_t=\mathbb E_{s\sim d^{\pi_t}_\mu}A^{\pi_t}(s,\pi'_t(s))$, and $\varepsilon_\Pi$ is + the class approximation error of the source. + + Prove: + - $V^{\pi_{t+1}}_\mu-V^{\pi_t}_\mu\ge\frac\alpha{1-\gamma}(\mathbb A_t-\frac{2\alpha\gamma}{(1-\gamma)^2})$ + for $\alpha\in[0,1]$; + - $\alpha=\mathbb A_t(1-\gamma)^2/(4\gamma)$ gives improvement $\mathbb A_t^2(1-\gamma)/(8\gamma)$; + - CPI stops ($\mathbb A_t\le\varepsilon$) within $8\gamma/(\varepsilon^2(1-\gamma)^2)$ iterations. + The source prints $8\gamma/\varepsilon^2$; + - the output satisfies $V^*-V^\pi\le(2\varepsilon+\varepsilon_\Pi)(1-\gamma)^{-2}\|d^{\pi^*}/\mu\|_\infty$. + +Completion checks: for a one-state MDP, NPG is the exponential-weights (Hedge) update with step +$\eta/(1-\gamma)$; soft policy iteration is the case $\eta=(1-\gamma)/\tau$ of item 7. + +## Layer 18: Online episodic exploration + +Episodic MDPs with stage-dependent transitions, deterministic rewards in $[0,1]$ known to the +learner (`M.HasRewardFn r`), initial law μ and $K$ episodes. Algorithms are algorithms in +`statesEnv` (Layer 7.7). Regret is that of Layer 14.7. + +1. **UCBVI** [AJKS, Theorem 7.1], corrected. + - Define the algorithm: value iteration on the empirical kernel with bonus + $2H\sqrt{L/\max(1,N^k_h(s,a))}$, $L=\log(SAH^2K^2)$, and values clipped at $H$. + - Prove that its expected regret is at most $20H^2S\sqrt{AKL}+2$. The $+2$ comes from failure + probability $1/(KH)$. The source prints the constant 10, but the last line of the proof of its + Lemma 7.5 drops a factor 2. +2. **Refined analysis** [AJKS, Theorem 7.6], corrected. Prove the expected regret bound + $8eH^2\sqrt{SAKL}+2eH^3S^2A(2+\log K)L+2$, with the per-entry Bernstein bound proved through the + stream model of Layer 14.2. The source omits the $+2$ and bounds the harmonic sum by $\log K$. +3. **Optimistic Q-learning** [JABJ18, Theorem 1]. + - Define UCB-H: $Q$ initialized at $H$, learning rates $(H+1)/(H+t)$, bonuses $c\sqrt{H^3\iota/t}$, + and $V_h=\min\{H,\max_aQ_h\}$, with $\iota=\log(SAKH/p)$. + - Prove: there are $c,C>0$ such that, with probability at least $1-p$, the regret is at most + $C\sqrt{H^5SAK\iota}$. +4. **Minimax lower bound** [DMKV21, Theorem 9]. Let $S\ge6$, $A\ge2$, $S=3+(A^d-1)/(A-1)$ for an + integer $d$, $H\ge3d$ and $K\ge HSA$. Prove that every algorithm has, on some episodic MDP with + these sizes and a Dirac initial law, expected regret at least $\sqrt{H^3SAK}/(48\sqrt6)$. +5. **Horizon-free regret** [ZJD21, Theorem 1]. + - Setting: stationary transitions, pooled counts, and rewards with $\sum_{h0$ such that, with probability at least $1-\delta$, + $\mathrm{Regret}(K)\le C(\sqrt{SAK\ell\iota}+S^2A\ell\iota)$, with $\ell=\log_2(KH)+2$ and + $\iota=\log(24S^2AH\ell^2/\delta)$. + - Prove the ingredients: + - the monotone bonus lemma [ZJD21, Lemma 14]; + - the higher-moment recursion [ZJD21, Lemma 2]; + - the bound $SA(\log_2(KH)+1)$ on the number of update epochs. + - The empirical Bernstein inequality of Layer 3.2 replaces Maurer and Pontil's in the source's + Lemma 12 and eq. (8): $\sqrt{2\hat Vx/n}+3x/n\le2\sqrt{\hat V\iota/n}+14\iota/(3n)$ for + $x=\log(3/\delta')$, $\iota=\log(2/\delta')$ and $\delta'\le9/10$. +6. **Settling the minimax regret** [ZCLD24, Theorem 1]. + - Define [ZCLD24, Algorithm 1] with known rewards: $c_1=460/9$, $c_3=544/9$, + $\delta'=\delta/(200SAH^2K^2)$, and no reward term. + - Prove the profile union bound [ZCLD24, Lemma 5] for $K\ge SAH\log_2K$. + - Prove: there is $C>0$ such that, for $K\ge2$ a power of two and $\delta\in(0,1)$, with + probability at least $1-\delta$, $\mathrm{Regret}(K)\le C\min\{\sqrt{B\,SAH^3K},HK\}$, with + $B=4000(\log_2K)^3\log(3SAH)\log(1/\delta')$. + - Layer 3.2 replaces Maurer–Pontil in [ZCLD24, Lemma 19]; the constant $C$ absorbs the change. + - Together with item 4, this settles the minimax regret up to logarithmic factors. + +Completion checks: with $H=1$, items 1–3 specialize to contextual bandits with the initial law as +the context distribution; the smallest instance admitted by item 4 has $A=2$, $d=2$, $S=6$ and +$H\ge6$. + +## Layer 19: Reward-free exploration and best policy identification + +1. **Problems.** + - A best policy identification algorithm is an LML identification algorithm (`IdentAlg`) in + `statesEnv` with an $H$-step policy as output (entropy-mdp's `BPIAlg`). Its stopping time τ + counts episodes. It is $(\varepsilon,\delta)$-PAC if the output is ε-optimal with probability + at least $1-\delta$ on every MDP. + - A reward-free exploration algorithm is an identification algorithm in `statesEnv` whose output + is a stage-dependent kernel $(\hat P_h)_{h0$ such that, for $A\ge2$, + $S\ge C\log_2A$, $H\ge C\log_2S$, $\varepsilon\le\min\{1/4,H/48\}$ and $\delta\le1/2$, every + $(\varepsilon,\delta)$-PAC reward-free algorithm has $\mathbb E[\tau]\ge cS^2AH^2/\varepsilon^2$ + on some MDP. + +Completion checks: for $H=1$ best policy identification is ε-best-arm identification for every +context; the threshold β of RF-Express follows from Layer 3.4 and a union bound. + +## Layer 20: Adversarial MDPs + +Episodic MDPs with known horizon and unknown fixed stage-dependent transitions. This layer uses +losses $\ell_k:\mathrm{Fin}\,H\to\mathcal S\times\mathcal A\to[0,1]$, chosen as an oblivious +sequence, as in the Bandits roadmap. + +- The environment is LML's `obliviousEnv` whose round-$k$ kernel maps an $H$-step policy to the law + of the state sequence together with $\ell_k$ (full information), or together with the losses + $\ell_{k,h}(S_h,A_h)$ along the trajectory (bandit feedback). +- The regret against the best Markov policy is $\max_\pi\sum_{k0$ such that UOB-REPS with $\eta=\gamma=\sqrt{L\log(L|X|A/\delta)/(K|X|A)}$ + has, with probability at least $1-9\delta$, regret at most $C\,L|X|\sqrt{AK\log(K|X|A/\delta)}$. + - Layer 3.2 replaces Maurer–Pontil in the confidence sets [JJLSY20, (5)–(6)]. + +Completion checks: for $H=1$ and one state, item 1 is exponential weights and item 3 is Exp3-IX. + +## Layer 21: Average-reward learning + +1. **UCRL2** [JOA10, Theorem 2]. + - For a communicating MDP with $S\ge2$ and diameter $D$, define UCRL2 with known rewards in + `M.env μ`. The regret after $n$ rounds is the random variable $n\rho^*-\sum_{t1$, the regret is at most + $34DS\sqrt{AT\log(T/\delta)}$. The reward terms of the source's (22) are nonnegative and + vanish when rewards are known; rerun its §4 without them. +2. **Lower bound** [JOA10, Theorem 5]. For $S,A\ge10$, $D\ge20\log_AS$, $D\ge12$ and $T\ge DSA$, + prove that every algorithm has, on some MDP with diameter at most $D$, expected regret at least + $0.015\sqrt{DSAT}$. Use Layer 6.2. +3. **Generative model** [ZC24, Theorems 1, 2]. For a weakly communicating MDP with + $\mathrm{sp}(h^*)\le\mathsf H$ and deterministic rewards in $[0,1]$: + - Theorem 1: for a γ-discounted MDP with $\mathsf H\le1/(1-\gamma)$ and $\varepsilon\le\mathsf H$, + there is $C>0$ such that $N\ge C\mathsf H/((1-\gamma)^2\varepsilon^2)\log(SA/((1-\gamma)\delta\varepsilon))$ + samples per pair give, with probability at least $1-\delta$, $\|v^*_\gamma-v^{\hat\pi}_\gamma\|\le\varepsilon$. + Here $\hat\pi$ is the optimal policy of the empirical MDP with rewards perturbed as in + Layer 15.4 (c), with level $\xi=(1-\gamma)\varepsilon/6$. + - Theorem 2: there is $C>0$ such that, for $\varepsilon,\delta\in(0,1)$ and + $N\ge C(\mathsf H/\varepsilon^2)\log(SA\mathsf H/(\delta\varepsilon))$, the reduction with + $\gamma=1-\varepsilon/(12\mathsf H)$ and discounted accuracy $\mathsf H$ returns, with + probability at least $1-\delta$, a policy with $\rho^*-\rho^{\hat\pi}\le\varepsilon$. + - The probability is over `streamMeasure M.P` and the perturbation. The proofs go through + Layers 13.5, 13.8 and 15. + +Completion check: the diameter of a deterministic cycle of length $S$ is $S-1$. + +## Layer 22: Offline reinforcement learning + +1. **Data.** Each item fixes one of these data measures: + - $n$ i.i.d. tuples $(s,a,y,s')$: `Measure.pi` of $\nu\otimes_m(R\times P)$, with $(s,a)\sim\nu$, + reward $y\sim R(s,a)$ and next state $s'\sim P(s,a)$; + - a compliant dataset [JYW21, Definition 2.1] of $K$ episodes of the episodic MDP. For every + step $h$ and episode τ, given the state–action pairs of step $h$ of episodes $j\le\tau$ and the + rewards and next states of step $h$ of episodes $j<\tau$, the pair $(r^\tau_h,x^\tau_{h+1})$ has + conditional law $R_h\otimes P_h$ at $(x^\tau_h,a^\tau_h)$. + + Rewards are observed in the data here; they are not known. +2. **Concentrability and fitted Q-iteration** [AJKS, Assumptions 4.1–4.2, Lemma 4.4, Theorem 4.3]. + - Define the concentrability coefficient $C_{\mathrm{conc}}$ as the supremum over nonstationary + policies of $\|d/\nu\|_\infty$, with $d$ the occupancy measures of Layer 11.1 (in `ℝ≥0∞`). + Define the inherent Bellman error $\varepsilon_{\mathrm{approx}}$ of a finite function class + $\mathcal F$. + - Prove the error propagation of [AJKS, Lemma 4.4]. + - Prove the fitted Q-iteration guarantee from Layer 3.6 with $B=1/(1-\gamma)$: there is $C>0$ + such that, with probability at least $1-\delta$, + $V^*(\mu)-V^{\pi_K}(\mu)\le(1-\gamma)^{-2}\big(\sqrt{C\,C_{\mathrm{conc}}\log(|\mathcal F|^2K/\delta)/((1-\gamma)^2n)}+\sqrt{C\,C_{\mathrm{conc}}\,\varepsilon_{\mathrm{approx}}}\big)+\gamma^K/(1-\gamma)^2$. +3. **Pessimism** [JYW21, Definition 4.1, Theorem 4.2]. On measurable `𝓢`: + - Define a ξ-uncertainty quantifier: functions $\Gamma_h$ such that, with probability at least + $1-\xi$, $|\hat B_h\hat V_{h+1}-B_h\hat V_{h+1}|\le\Gamma_h$ for all $h$. + - Define pessimistic value iteration as in Layer 12.2. + - Prove that on the event of the quantifier, + $V^*_0(s)-V^{\hat\pi}_0(s)\le2\sum_h\mathbb E^{\pi^*}_s[\Gamma_h(S_h,A_h)]$. +4. **Offline bandits** [RZMJR21, eq. (9), Theorem 2]. For $A\ge2$ arms and i.i.d. data + $a_i\sim\mu$, $r_i\sim R(a_i)$ in $[0,1]$: + - Define the lower confidence bound algorithm, with + $b(a)=\sqrt{\log(2A/\delta)/(2N(a))}$, and $\hat r(a)=0$, $b(a)=1$ when $N(a)=0$. + - Prove: if $N\ge8C^*\log(1/\delta)$, then with probability at least $1-2\delta$, + $r(a^*)-r(\hat a)\le\min(1,2\sqrt{C^*\log(2A/\delta)/N})$. + - Prove the matching lower bound for $C^*\ge2$ in "∃ c" form. +5. **Model-based offline RL** [LSCCW24, Theorems 5, 2]. Rewards are known and deterministic, and the + data are the transitions of item 1. + - Define the clipped concentrability + $C^*_{\mathrm{clipped}}=\max_{s,a}\min\{d^*(s,a),1/S\}/d^b(s,a)$. + - Define VI-LCB with the penalty + $b(s,a;V)=\min\{\max\{\sqrt{c_b\log(N/((1-\gamma)\delta))\mathrm{Var}_{\hat P}(V)/N(s,a)},\ 2c_b\log(N/((1-\gamma)\delta))/((1-\gamma)N(s,a))\},\ 1/(1-\gamma)\}+5/N$. + Prove that the pessimistic operator is a γ-contraction. + - Theorem 5: for $\gamma\in[1/2,1)$, $c_b\ge144$ and any $\hat Q$ within $1/N$ of the + pessimistic fixed point, with probability at least $1-2\delta$, + $V^*(\rho)-V^{\hat\pi}(\rho)\le120\sqrt{\frac{c_bSC^*_{\mathrm{clipped}}L}{(1-\gamma)^3N}}+\frac{3464c_bSC^*_{\mathrm{clipped}}L}{(1-\gamma)^2N}$, + with $L=\log(NS/((1-\gamma)\delta))$. + - Theorem 2, the lower bound: for $\gamma\ge2/3$, $S\ge2$, $C^*_{\mathrm{clipped}}\ge8\gamma/S$ and + $\varepsilon\le1/(42(1-\gamma))$, every estimator errs by more than ε with probability at + least $1/8$ when $N\le SC^*_{\mathrm{clipped}}/(25088(1-\gamma)^3\varepsilon^2)$. + +Completion check: with full coverage ($\nu$ uniform), $C_{\mathrm{conc}}\le SA$. + +## Layer 23: Linear function approximation + +Features $\varphi:\mathcal S\times\mathcal A\to E$ in a finite-dimensional real inner product space +of dimension $d$, with $\|\varphi\|\le1$. + +1. **Models.** + - Linear Bellman completeness [AJKS, Definition 3.1]. + - Linear MDPs [JYWJ20, Assumption A]: $P_h(\cdot|s,a)=\langle\varphi(s,a),\mu_h(\cdot)\rangle$ + and $r_h=\langle\varphi,\theta_h\rangle$, with $\|\theta_h\|\le\sqrt d$ and + $\||\mu_h|(\mathcal S)\|\le\sqrt d$. The source bounds the signed masses; the total-variation + normalization is the one its proof needs. + - Linear mixture MDPs [ZGS21, §3]: $P_h(s'|s,a)=\langle\phi(s'|s,a),\theta_h\rangle$ with + $\|\theta_h\|\le B$ and $\|\sum_{s'}\phi(s'|s,a)V(s')\|\le1$ for $V:\mathcal S\to[0,1]$. +2. **Least-squares value iteration with a D-optimal design** [AJKS, Theorem 3.3], corrected. + - Setting: linear Bellman completeness with the episodic generative model, $\varepsilon\in(0,1)$, + $N=\lceil64H^6d^2\log(H/\delta)/\varepsilon^2\rceil$, and $\lceil\rho(s,a)N\rceil$ samples at + each support point $(s,a)$ of the Kiefer–Wolfowitz design ρ (Bandits roadmap, Layer 8.6) at + every step. + - Prove that with probability at least $1-\delta$ the output policy is ε-optimal from μ. + - The source prints $\log(1/\delta)$; its union bound over steps needs $\log(H/\delta)$. +3. **LSVI-UCB** [JYWJ20, Theorem 3.1]. `𝓢` is finite here because algorithms act in `statesEnv`. + - Prove the uniform self-normalized bound over the class of clipped linear value functions, with + an ε-net (Layer 3.5) [JYWJ20, Lemmas D.4–D.6]. + - Prove: there are $c,C>0$ such that, with $\lambda=1$, $\beta=c\,dH\sqrt\iota$ and + $\iota=\log(2dKH/p)$, with probability at least $1-p$, + $\mathrm{Regret}(K)\le C\sqrt{d^3H^4K\iota^2}$. +4. **Pessimism for linear MDPs** [JYW21, Theorem 4.4]. On measurable `𝓢`, prove: there are $c>0$ + and $\zeta=\log(2dHK/\xi)$ such that, with $\beta=c\,dH\sqrt\zeta$, the penalty + $\beta\|\varphi\|_{\Lambda_h^{-1}}$ is a ξ-uncertainty quantifier (Layer 22.3). Hence + $V^*_0-V^{\hat\pi}_0\le2\beta\sum_h\mathbb E^{\pi^*}[\|\varphi(S_h,A_h)\|_{\Lambda_h^{-1}}]$. +5. **Linear mixture MDPs** [ZGS21]. + - Theorem 4.1, the Bernstein self-normalized bound. Hypotheses: + - $y_t=\langle\mu^*,x_t\rangle+\eta_t$, with $x_t$ $\mathcal G_t$-measurable and $\eta_t$ + $\mathcal G_{t+1}$-measurable; + - $|\eta_t|\le R$, $\mathbb E[\eta_t|\mathcal G_t]=0$ and $\mathbb E[\eta_t^2|\mathcal G_t]\le\sigma^2$; + - $\|x_t\|\le L$ and $Z_t=\lambda I+\sum_{i\le t}x_ix_i^\top$. + + Prove that with probability at least $1-\delta$, for all $t$: + $\|\sum_{i\le t}x_i\eta_i\|_{Z_t^{-1}}\le\beta_t=8\sigma\sqrt{d\log(1+tL^2/(d\lambda))\log(4t^2/\delta)}+4R\log(4t^2/\delta)$. + Deduce the corollary $\|\hat\mu_t-\mu^*\|_{Z_t}\le\beta_t+\sqrt\lambda\|\mu^*\|$. Place it next to + the Bandits roadmap's Layer 8 self-normalized bound. + - Theorem 5.6, the lower bound: for $B>1$, $d\ge4$, $H\ge3$ and + $K\ge\max\{(d-1)^2H/2,(d-1)/(32H(B-1))\}$, prove: there is $c>0$ such that every algorithm + has, on some linear mixture MDP, expected regret at least $c\,dH\sqrt{KH}$. + +Completion check: tabular MDPs are linear MDPs with $d=SA$ and indicator features. +## Completion checks + +Every new definition comes with measurability, evaluation and extensionality lemmas. Every algorithm +comes with its run lemma, the conditional law of its action given the history, so that the +theorems apply to all runs. Check in particular: +- The optimality equations of Layers 8, 9 and 13 agree: + - finite horizon $N\to\infty$ with discounting recovers $v^*_\gamma$; + - $(1-\gamma)v^*_\gamma\to g^*$ for unichain models. +- The lower bound of Layer 18.4 matches the upper bound of Layer 18.6 up to logarithmic factors. +- Layer 19.3's best policy identification bound and Layer 19.2 differ by a factor $S$ and + logarithmic factors; Layer 21.2 and Layer 21.1 differ by $\sqrt{DS}$ and logarithmic factors. +- A one-state MDP turns Layers 15, 17 and 18 into the corresponding bandit statements, and these + agree with the Bandits roadmap. +- Layers 1 and 2 restricted to countable state spaces agree with the definitions of Tau Ceti's + MarkovChainsAndRenewal roadmap where both exist. + +Compilation of the suggested signatures checks their types, not the truth of their admitted +theorems or the completion of these milestones. + +## References + +Books and monographs: +- [P] M. L. Puterman, *Markov Decision Processes: Discrete Stochastic Dynamic Programming*, Wiley + (1994). +- [AJKS] A. Agarwal, N. Jiang, S. M. Kakade and W. Sun, *Reinforcement Learning: Theory and + Algorithms*, version of 31 January 2022, rltheorybook.github.io. +- [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press (2020). +- [Ber22] D. P. Bertsekas, *Abstract Dynamic Programming*, 3rd ed., Athena Scientific (2022). +- [BLM13] S. Boucheron, G. Lugosi and P. Massart, *Concentration Inequalities*, Oxford University + Press (2013). +- [CT06] T. M. Cover and J. A. Thomas, *Elements of Information Theory*, 2nd ed., Wiley (2006). +- [Kal21] O. Kallenberg, *Foundations of Modern Probability*, 3rd ed., Springer (2021). +- [Kre85] U. Krengel, *Ergodic Theorems*, de Gruyter (1985). +- [KY03] H. J. Kushner and G. G. Yin, *Stochastic Approximation and Recursive Algorithms and + Applications*, 2nd ed., Springer (2003). +- [LPW17] D. A. Levin, Y. Peres and E. L. Wilmer, *Markov Chains and Mixing Times*, 2nd ed., AMS + (2017). +- [MT09] S. Meyn and R. L. Tweedie, *Markov Chains and Stochastic Stability*, 2nd ed., Cambridge + University Press (2009). +- [Nes18] Y. Nesterov, *Lectures on Convex Optimization*, 2nd ed., Springer (2018). +- [Nor97] J. R. Norris, *Markov Chains*, Cambridge University Press (1997). +- [Ora23] F. Orabona, *A Modern Introduction to Online Learning*, arXiv:1912.13213 (version 10). +- [Rev84] D. Revuz, *Markov Chains*, 2nd ed., North-Holland (1984). + +Papers: +- [AKLM21] A. Agarwal, S. M. Kakade, J. D. Lee and G. Mahajan, On the theory of policy gradient + methods: optimality, approximation, and distribution shift, *JMLR* 22 (2021), COLT 2020, + arXiv:1908.00261. +- [AKY20] A. Agarwal, S. Kakade and L. F. Yang, Model-based reinforcement learning with a generative + model is minimax optimal, COLT 2020, arXiv:1906.03804. +- [AMK13] M. G. Azar, R. Munos and H. J. Kappen, Minimax PAC bounds on the sample complexity of + reinforcement learning with a generative model, *Machine Learning* 91 (2013). +- [AMS09] J.-Y. Audibert, R. Munos and Cs. Szepesvári, Exploration–exploitation tradeoff using + variance estimates in multi-armed bandits, *Theoretical Computer Science* 410 (2009). +- [AOM17] M. G. Azar, I. Osband and R. Munos, Minimax regret bounds for reinforcement learning, + ICML 2017, arXiv:1703.05449. +- [Bla65] D. Blackwell, Discounted dynamic programming, *Ann. Math. Statist.* 36 (1965). +- [BRS18] J. Bhandari, D. Russo and R. Singal, A finite time analysis of temporal difference learning + with linear function approximation, COLT 2018, arXiv:1806.02450. +- [CCCWC22] S. Cen, C. Cheng, Y. Chen, Y. Wei and Y. Chi, Fast global convergence of natural policy + gradient methods with entropy regularization, *Operations Research* 70 (2022), arXiv:2007.06558. +- [DMKV21] O. D. Domingues, P. Ménard, E. Kaufmann and M. Valko, Episodic reinforcement learning in + finite MDPs: minimax lower bounds revisited, ALT 2021, arXiv:2010.03531. +- [Dob56] R. L. Dobrushin, Central limit theorem for nonstationary Markov chains, *Theory Probab. + Appl.* 1 (1956). +- [EV26] A. Essakine and C. Vernade, Tight sample complexity bounds for entropic best policy + identification, COLT 2026, arXiv:2605.13717. +- [Fre75] D. A. Freedman, On tail probabilities for martingales, *Ann. Probab.* 3 (1975). +- [GG04] S. Gaubert and J. Gunawardena, The Perron–Frobenius theorem for homogeneous, monotone + functions, *Trans. AMS* 356 (2004). +- [JABJ18] C. Jin, Z. Allen-Zhu, S. Bubeck and M. I. Jordan, Is Q-learning provably efficient?, + NeurIPS 2018, arXiv:1807.03765. +- [JJLSY20] C. Jin, T. Jin, H. Luo, S. Sra and T. Yu, Learning adversarial Markov decision processes + with bandit feedback and unknown transition, ICML 2020, arXiv:1912.01192. +- [JKMDLV20] A. Jonsson, E. Kaufmann, P. Ménard, O. D. Domingues, E. Leurent and M. Valko, Planning + in Markov decision processes with gap-dependent sample complexity, NeurIPS 2020, + arXiv:2006.05879. +- [JKSY20] C. Jin, A. Krishnamurthy, M. Simchowitz and T. Yu, Reward-free exploration for + reinforcement learning, ICML 2020, arXiv:2002.02794. +- [JOA10] T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, + *JMLR* 11 (2010). +- [JPR23] E. Johnson, C. Pike-Burke and P. Rebeschini, Optimal convergence rate for exact policy + mirror descent in discounted Markov decision processes, NeurIPS 2023, arXiv:2302.11381. +- [JS21] Y. Jin and A. Sidford, Towards tight bounds on the sample complexity of average-reward + MDPs, ICML 2021, arXiv:2106.07046. +- [JYW21] Y. Jin, Z. Yang and Z. Wang, Is pessimism provably efficient for offline RL?, ICML 2021, + arXiv:2012.15085. +- [JYWJ20] C. Jin, Z. Yang, Z. Wang and M. I. Jordan, Provably efficient reinforcement learning with + linear function approximation, COLT 2020, arXiv:1907.05388. +- [KNS16] H. Karimi, J. Nutini and M. Schmidt, Linear convergence of gradient and proximal-gradient + methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016, arXiv:1608.04636. +- [Koh80] E. Kohlberg, Invariant half-lines of nonexpansive piecewise-linear transformations, + *Math. Oper. Res.* 5 (1980). +- [Lan23] G. Lan, Policy mirror descent for reinforcement learning: linear convergence, new sampling + complexity, and generalized problem classes, *Math. Program.* 198 (2023), arXiv:2102.00135. +- [LCCWC24] G. Li, C. Cai, Y. Chen, Y. Wei and Y. Chi, Is Q-learning minimax optimal? A tight sample + complexity analysis, *Operations Research* (2024), arXiv:2102.06548. +- [LSCCW24] G. Li, L. Shi, Y. Chen, Y. Chi and Y. Wei, Settling the sample complexity of model-based + offline reinforcement learning, *Ann. Statist.* (2024), arXiv:2204.05275. +- [LWCGC24] 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), + NeurIPS 2020, arXiv:2005.12900. +- [MDJKLV21] P. Ménard, O. D. Domingues, A. Jonsson, E. Kaufmann, E. Leurent and M. Valko, Fast + active learning for pure exploration in reinforcement learning, ICML 2021, arXiv:2007.13442. +- [MXSS20] J. Mei, C. Xiao, Cs. Szepesvári and D. Schuurmans, On the global convergence rates of + softmax policy gradient methods, ICML 2020, arXiv:2005.06392. +- [RM19] A. Rosenberg and Y. Mansour, Online convex optimization in adversarial Markov decision + processes, ICML 2019, arXiv:1905.07773. +- [RM51] H. Robbins and S. Monro, A stochastic approximation method, *Ann. Math. Statist.* 22 + (1951). +- [RS71] H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales + and some applications, in *Optimizing Methods in Statistics*, Academic Press (1971). +- [RZMJR21] P. Rashidinejad, B. Zhu, C. Ma, J. Jiao and S. Russell, Bridging offline reinforcement + learning and imitation learning: a tale of pessimism, NeurIPS 2021, arXiv:2103.12021. +- [Sob82] M. J. Sobel, The variance of discounted Markov decision processes, *J. Appl. Probab.* 19 + (1982). +- [Tsi94] J. N. Tsitsiklis, Asynchronous stochastic approximation and Q-learning, *Machine Learning* + 16 (1994). +- [TVR97] J. N. Tsitsiklis and B. Van Roy, An analysis of temporal-difference learning with function + approximation, *IEEE Trans. Automat. Control* 42 (1997). +- [WOSVW03] T. Weissman, E. Ordentlich, G. Seroussi, S. Verdú and M. J. Weinberger, Inequalities for + the L1 deviation of the empirical distribution, HP Labs technical report HPL-2003-97 (2003). +- [WJLSJ20] C.-Y. Wei, M. Jafarnia-Jahromi, H. Luo, H. Sharma and R. Jain, Model-free reinforcement + learning in infinite-horizon average-reward Markov decision processes, ICML 2020, + arXiv:1910.07072. +- [WWY22] J. Wang, M. Wang and L. F. Yang, Near sample-optimal reduction-based policy learning for + average reward MDP, arXiv:2212.00603. +- [Xiao22] L. Xiao, On the convergence rates of policy gradient methods, *JMLR* 23 (2022), + arXiv:2201.07443. +- [ZC24] M. Zurek and Y. Chen, Span-based optimal sample complexity for weakly communicating and + general average reward MDPs, NeurIPS 2024, arXiv:2403.11477. +- [ZCLD24] Z. Zhang, Y. Chen, J. D. Lee and S. S. Du, Settling the sample complexity of online + reinforcement learning, COLT 2024, arXiv:2307.13586. +- [Zha25] S. Zhang, Towards formalizing reinforcement learning theory: a Robbins–Siegmund approach, + arXiv:2511.03618. +- [ZGS21] D. Zhou, Q. Gu and Cs. Szepesvári, Nearly minimax optimal reinforcement learning for + linear mixture Markov decision processes, COLT 2021, arXiv:2012.08507. +- [ZJD21] Z. Zhang, X. Ji and S. S. Du, Is reinforcement learning more difficult than bandits? A + near-optimal algorithm escaping the curse of horizon, COLT 2021, arXiv:2009.13503. diff --git a/LMLRoadmaps/ReinforcementLearning/Suggested.lean b/LMLRoadmaps/ReinforcementLearning/Suggested.lean new file mode 100644 index 0000000..fd453a5 --- /dev/null +++ b/LMLRoadmaps/ReinforcementLearning/Suggested.lean @@ -0,0 +1,421 @@ +import Mathlib.Analysis.Normed.Lp.lpSpace +import Mathlib.LinearAlgebra.Matrix.Stochastic +import Mathlib.MeasureTheory.Function.ConditionalLExpectation +import Mathlib.MeasureTheory.Measure.TotalVariation.Defs +import Mathlib.Probability.Kernel.Composition.Prod +import Mathlib.Probability.Kernel.Invariance +import Mathlib.Probability.Moments.SubGaussian +import Mathlib.Probability.Martingale.Basic +import Mathlib.Topology.MetricSpace.Contracting +import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg +import LeanMachineLearning.Online.Bandit.ArrayProbSpace +import LeanMachineLearning.SequentialLearning.Deterministic +import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace +import LeanMachineLearning.SequentialLearning.StationaryEnv +import TauCeti.Probability.Process.MarkovChain + +/-! +# Markov decision processes and reinforcement learning theory: suggested target signatures + +**This file is not the roadmap and is not exhaustive.** The definitive document is `README.md`. +The statements here suggest Lean forms for particular milestones, so that contributors and +reviewers converge on names and signatures; discharging all of them finishes neither a milestone +nor the roadmap. The admitted proofs are targets, not claimed implementations. Admitted +definitions (algorithms, iterates) are targets too: their docstrings and the README specify them. + +`MDP` copies the structure of LML's `mdp` branch (fields `P`, `R`, `MDP.env`), and `EpisodicMDP` +the one of entropy-mdp, so that adopting the upstream versions is a deletion. The other names of +the LML framework are those of the LML version pinned by LMLExplore. +-/ + +noncomputable section + +open MeasureTheory ProbabilityTheory Learning Filter Finset +open scoped ENNReal NNReal Topology + +namespace LMLRoadmaps.ReinforcementLearning + +/-! ## Layer 0: order units, contractions and fixed points -/ + +section FixedPoint + +variable {ι : Type*} [Fintype ι] + +/-- Blackwell's sufficient conditions, on `ι → ℝ` with the sup norm (README Layer 0.2; the README +asks for the order-unit form on ordered vector spaces). -/ +theorem lipschitzWith_of_monotone_of_add_const_le {T : (ι → ℝ) → ι → ℝ} {γ : ℝ≥0} + (hT : Monotone T) (h : ∀ x (c : ℝ), 0 ≤ c → T (x + fun _ ↦ c) ≤ T x + fun _ ↦ γ * c) : + LipschitzWith γ T := + sorry + +/-- The oscillation (span seminorm) of a function on a finite type. -/ +def osc [Nonempty ι] (x : ι → ℝ) : ℝ := (Finset.univ.sup' Finset.univ_nonempty x) - + Finset.univ.inf' Finset.univ_nonempty x + +/-- Vanishing discount for topical maps (README Layer 0.5). -/ +theorem exists_add_eigenvector_of_topical [Nonempty ι] {T : (ι → ℝ) → ι → ℝ} (hT : Monotone T) + (h_top : ∀ x (c : ℝ), T (x + fun _ ↦ c) = T x + fun _ ↦ c) + (v : ℝ≥0 → ι → ℝ) (hv : ∀ γ < 1, v γ = T ((γ : ℝ) • v γ)) + (h_bdd : BddAbove (Set.range fun γ : {γ : ℝ≥0 // γ < 1} ↦ osc (v γ))) : + ∃ (g : ℝ) (h : ι → ℝ), T h = h + fun _ ↦ g := + sorry + +end FixedPoint + +/-! ## Layer 1: Markov processes on general measurable spaces -/ + +section Markov + +variable {α β Ω ι : Type*} [MeasurableSpace α] [MeasurableSpace β] {mΩ : MeasurableSpace Ω} + +/-- A process indexed by a preorder is Markov for the filtration `𝓕` with transition kernels +`κ s t`, `s ≤ t` (README Layer 1.1). -/ +structure IsMarkovProcess [Preorder ι] (X : ι → Ω → α) (𝓕 : Filtration ι mΩ) + (κ : ι → ι → Kernel α α) (P : Measure Ω) : Prop where + measurable : ∀ i, Measurable[𝓕 i] (X i) + condExp_comp : ∀ s t, s ≤ t → ∀ f : α → ℝ, Measurable f → (∃ C, ∀ x, |f x| ≤ C) → + P[f ∘ X t | 𝓕 s] =ᵐ[P] fun ω ↦ ∫ y, f y ∂(κ s t (X s ω)) + +/-- The Dobrushin coefficient of a kernel (README Layer 1.6), with Mathlib's `tvDist` in +`[0, 2]`. -/ +def dobrushinCoeff (κ : Kernel α β) : ℝ := ⨆ x, ⨆ y, tvDist (κ x) (κ y) / 2 + +theorem tvDist_bind_le_dobrushinCoeff_mul (κ : Kernel α β) [IsMarkovKernel κ] + (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : + tvDist (μ.bind κ) (ν.bind κ) ≤ dobrushinCoeff κ * tvDist μ ν := + sorry + +/-- Doeblin: a power with Dobrushin coefficient below one gives a unique invariant probability +and uniform geometric convergence (README Layer 1.6). -/ +theorem exists_unique_invariant_of_dobrushinCoeff_pow_lt_one [Nonempty α] (κ : Kernel α α) + [IsMarkovKernel κ] + {m : ℕ} (hm : 0 < m) (h : dobrushinCoeff (κ ^ m) < 1) : + ∃! π : Measure α, IsProbabilityMeasure π ∧ κ.Invariant π ∧ + ∀ n x, tvDist ((κ ^ n) x) π ≤ 2 * dobrushinCoeff (κ ^ m) ^ (n / m) := + sorry + +/-- The resolvent of a kernel acting on a function (README Layer 1.4). -/ +def resolvent (γ : ℝ≥0) (κ : Kernel α α) (f : α → ℝ) (x : α) : ℝ := + ∑' n, (γ : ℝ) ^ n * ∫ y, f y ∂((κ ^ n) x) + +end Markov + +/-! ## Layer 2: mean ergodic theory and finite Markov chains -/ + +section FiniteChains + +variable {S : Type*} [Fintype S] [DecidableEq S] + +/-- The limiting matrix `P*` of a matrix: the limit of its Cesàro means (README Layer 2.4). -/ +def limitingMatrix (P : Matrix S S ℝ) : Matrix S S ℝ := + limUnder atTop fun n : ℕ ↦ (n : ℝ)⁻¹ • ∑ k ∈ range n, P ^ k + +theorem tendsto_cesaro_limitingMatrix {P : Matrix S S ℝ} (hP : P ∈ Matrix.rowStochastic ℝ S) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • ∑ k ∈ range n, P ^ k) atTop (𝓝 (limitingMatrix P)) := + sorry + +theorem mul_limitingMatrix {P : Matrix S S ℝ} (hP : P ∈ Matrix.rowStochastic ℝ S) : + P * limitingMatrix P = limitingMatrix P ∧ limitingMatrix P * P = limitingMatrix P := + sorry + +/-- The deviation matrix `(I - P + P*)⁻¹ - P*` (README Layer 2.2). -/ +def deviationMatrix (P : Matrix S S ℝ) : Matrix S S ℝ := + (1 - P + limitingMatrix P)⁻¹ - limitingMatrix P + +theorem isUnit_one_sub_add_limitingMatrix {P : Matrix S S ℝ} (hP : P ∈ Matrix.rowStochastic ℝ S) : + IsUnit (1 - P + limitingMatrix P) := + sorry + +end FiniteChains + +/-! ## Layer 3: concentration -/ + +section Concentration + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] + {ℱ : Filtration ℕ mΩ} + +/-- Freedman's inequality, fixed-`η` time-uniform form (README Layer 3.1). `X t` is +`ℱ (t + 1)`-measurable, with conditional mean at most zero given `ℱ t`, and `η X t ≤ 1`. -/ +theorem measure_exists_sum_ge_le_freedman {X : ℕ → Ω → ℝ} {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ) + (hδ₁ : δ ≤ 1) + (h_meas : ∀ t, Measurable[ℱ (t + 1)] (X t)) (h_int : ∀ t, Integrable (fun ω ↦ X t ω ^ 2) P) + (h_mean : ∀ t, P[X t | ℱ t] ≤ᵐ[P] 0) (h_bdd : ∀ t ω, η * X t ω ≤ 1) : + P {ω | ∃ n, η * ∑ t ∈ range n, P[fun ω ↦ X t ω ^ 2 | ℱ t] ω + Real.log (1 / δ) / η ≤ + ∑ t ∈ range n, X t ω} ≤ ENNReal.ofReal δ := + sorry + +/-- The `ℓ¹` deviation of the empirical law on a finite type [WOSVW03] (README Layer 3.3). -/ +theorem measure_sum_abs_empirical_sub_ge_le {α : Type*} [Fintype α] [DecidableEq α] + [MeasurableSpace α] [MeasurableSingletonClass α] (p : Measure α) [IsProbabilityMeasure p] + {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) : + (Measure.pi fun _ : Fin n ↦ p).real + {x | ε ≤ ∑ a, |(n : ℝ)⁻¹ * (Finset.univ.filter fun i ↦ x i = a).card - p.real {a}|} ≤ + (2 ^ Fintype.card α - 2) * Real.exp (-n * ε ^ 2 / 2) := + sorry + +end Concentration + +/-! ## Layer 4: stochastic approximation -/ + +/-- **Robbins–Siegmund** (README Layer 4.1), for processes with values in `ℝ≥0`. -/ +theorem robbinsSiegmund {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} + [IsProbabilityMeasure P] {ℱ : Filtration ℕ mΩ} {V a b c : ℕ → Ω → ℝ≥0} + (hV : ∀ n, Measurable[ℱ n] (V n)) (ha : ∀ n, Measurable[ℱ n] (a n)) + (hb : ∀ n, Measurable[ℱ n] (b n)) (hc : ∀ n, Measurable[ℱ n] (c n)) + (h : ∀ n, P⁻[fun ω ↦ (V (n + 1) ω : ℝ≥0∞) | ℱ n] + (fun ω ↦ (c n ω : ℝ≥0∞)) + ≤ᵐ[P] fun ω ↦ (((1 + a n ω) * V n ω + b n ω : ℝ≥0) : ℝ≥0∞)) : + ∀ᵐ ω ∂P, (Summable fun n ↦ a n ω) → (Summable fun n ↦ b n ω) → + (∃ l : ℝ≥0, Tendsto (fun n ↦ V n ω) atTop (𝓝 l)) ∧ Summable fun n ↦ c n ω := + sorry + +/-! ## Layer 5: optimization -/ + +/-- The softmax of a vector on a finite type (README Layer 5.1). -/ +def softmax {α : Type*} [Fintype α] (θ : α → ℝ) (a : α) : ℝ := + Real.exp (θ a) / ∑ b, Real.exp (θ b) + +/-! ## Layer 7: Markov decision processes, policies and values -/ + +/-- A Markov decision process: a transition kernel `P` and a reward kernel `R`. This copies the +structure of LML's `mdp` branch. -/ +structure MDP (𝓢 𝓐 𝓡 : Type*) [MeasurableSpace 𝓢] [MeasurableSpace 𝓐] [MeasurableSpace 𝓡] where + /-- The transition kernel. -/ + P : Kernel (𝓢 × 𝓐) 𝓢 + [hP : IsMarkovKernel P] + /-- The reward kernel. -/ + R : Kernel (𝓢 × 𝓐) 𝓡 + [hR : IsMarkovKernel R] + +variable {𝓢 𝓐 : Type*} [MeasurableSpace 𝓢] [MeasurableSpace 𝓐] + +namespace MDP + +instance (M : MDP 𝓢 𝓐 ℝ) : IsMarkovKernel M.P := M.hP +instance (M : MDP 𝓢 𝓐 ℝ) : IsMarkovKernel M.R := M.hR + +open Classical in +/-- The environment of `M` from the initial law `μ₀`: observation = state, feedback = reward +(as on LML's `mdp` branch). -/ +protected def env [h𝓢 : Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (μ₀ : Measure 𝓢) : Environment 𝓢 𝓐 ℝ where + obs + | 0 => Kernel.const _ (if IsProbabilityMeasure μ₀ then μ₀ else Measure.dirac h𝓢.some) + | n + 1 => M.P.comap (fun h ↦ ((h (Fin.last n)).obs, (h (Fin.last n)).action)) (by fun_prop) + feedback := fun _ ↦ M.R.comap (fun p ↦ (p.1.2, p.2)) (by fun_prop) + isMarkovKernel_obs n := by + cases n + · dsimp only + split_ifs <;> infer_instance + · infer_instance + +/-- The mean reward `r (s, a)`. -/ +def meanReward (R : Kernel (𝓢 × 𝓐) ℝ) (p : 𝓢 × 𝓐) : ℝ := ∫ x, x ∂(R p) + +/-- The state kernel of a stationary policy `π`. -/ +def stateKernel (M : MDP 𝓢 𝓐 ℝ) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] : Kernel 𝓢 𝓢 := + M.P ∘ₖ (Kernel.id ×ₖ π) + +/-- The mean reward of a stationary policy. -/ +def policyReward (M : MDP 𝓢 𝓐 ℝ) (π : Kernel 𝓢 𝓐) (s : 𝓢) : ℝ := + ∫ a, meanReward M.R (s, a) ∂(π s) + +/-- The discounted value `v^π = ∑ γⁿ Pπⁿ rπ` of a stationary policy. -/ +def value (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] (s : 𝓢) : ℝ := + ∑' n, (γ : ℝ) ^ n * ∫ s', M.policyReward π s' ∂((M.stateKernel π ^ n) s) + +/-- The action value `Q^π = r + γ P v^π`. -/ +def qValue (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] (p : 𝓢 × 𝓐) : ℝ := + meanReward M.R p + γ * ∫ s', M.value γ π s' ∂(M.P p) + +/-- The discounted value of a run of the algorithm `alg` from the initial law `μ`. -/ +def runValue [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (alg : Algorithm 𝓢 𝓐 ℝ) (μ : Measure 𝓢) : + ℝ := + ∫ ω, ∑' n, (γ : ℝ) ^ n * meanReward M.R ((ω n).obs, (ω n).action) ∂(trajMeasure alg (M.env μ)) + +/-- The optimal discounted value. -/ +def optValue [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (s : 𝓢) : ℝ := + ⨆ alg : Algorithm 𝓢 𝓐 ℝ, M.runValue γ alg (Measure.dirac s) + +/-- The Bellman optimality operator. -/ +def bellman (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (v : 𝓢 → ℝ) (s : 𝓢) : ℝ := + ⨆ a, (meanReward M.R (s, a) + γ * ∫ s', v s' ∂(M.P (s, a))) + +/-- The greedy action for `v`, with LML's measurable `argmax`. -/ +def greedy [Fintype 𝓐] [Nonempty 𝓐] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (v : 𝓢 → ℝ) (s : 𝓢) : 𝓐 := + argmax fun a ↦ meanReward M.R (s, a) + γ * ∫ s', v s' ∂(M.P (s, a)) + +/-- The discounted state–action occupancy measure of a run (README Layer 11.1). -/ +def occupancy [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (alg : Algorithm 𝓢 𝓐 ℝ) + (μ : Measure 𝓢) : Measure (𝓢 × 𝓐) := + (1 - γ : ℝ≥0∞) • Measure.sum fun n ↦ ((γ : ℝ≥0∞) ^ n) • + (trajMeasure alg (M.env μ)).map fun ω ↦ ((ω n).obs, (ω n).action) + +end MDP + +/-- A Markov policy as an algorithm: it plays `π n` at the current observation. -/ +def _root_.Learning.Algorithm.markov {𝓞 𝓨 : Type*} [MeasurableSpace 𝓞] [MeasurableSpace 𝓨] + (π : ℕ → Kernel 𝓞 𝓐) [∀ n, IsMarkovKernel (π n)] : Algorithm 𝓞 𝓐 𝓨 where + policy n := (π n).comap Prod.snd measurable_snd + +/-- A finite-horizon MDP with ℕ-indexed transition and reward kernels (entropy-mdp). -/ +structure EpisodicMDP (𝓢 𝓐 : Type*) [MeasurableSpace 𝓢] [MeasurableSpace 𝓐] where + /-- The transition kernel at step `h`. -/ + trans : ℕ → Kernel (𝓢 × 𝓐) 𝓢 + [isMarkovKernel_trans : ∀ h, IsMarkovKernel (trans h)] + /-- The reward kernel at step `h`. -/ + reward : ℕ → Kernel (𝓢 × 𝓐) ℝ + [isMarkovKernel_reward : ∀ h, IsMarkovKernel (reward h)] + +namespace MDP + +variable [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) {γ : ℝ≥0} + +/-! ## Layers 9–10: discounted optimality and algorithms -/ + +/-- The optimality equation (README Layer 9.4). -/ +theorem bellman_optValue [Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] + (hγ : γ < 1) (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) : + M.bellman γ (M.optValue γ) = M.optValue γ := + sorry + +/-- Uniqueness of bounded measurable solutions of the optimality equation (README Layer 9.4). -/ +theorem eq_optValue_of_bellman_eq [Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] + (hγ : γ < 1) (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) {v : 𝓢 → ℝ} (hv : Measurable v) + (hv_bdd : ∃ C, ∀ s, |v s| ≤ C) (h : M.bellman γ v = v) : + v = M.optValue γ := + sorry + +/-- The greedy policy for `v*` is optimal (README Layer 9.4). -/ +theorem value_greedy_optValue [Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] + (hγ : γ < 1) (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) + (hg : Measurable (M.greedy γ (M.optValue γ))) : + M.value γ (Kernel.deterministic (M.greedy γ (M.optValue γ)) hg) = M.optValue γ := + sorry + +/-- Value iteration (README Layer 10.1, [P, Theorem 6.3.3 (d)]). -/ +theorem abs_bellman_iterate_sub_optValue_le [Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] + (hγ : γ < 1) (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) {v : 𝓢 → ℝ} (hv : Measurable v) + {B : ℝ} (hB : ∀ s, |M.bellman γ v s - v s| ≤ B) (n : ℕ) (s : 𝓢) : + |(M.bellman γ)^[n] v s - M.optValue γ s| ≤ γ ^ n * B / (1 - γ) := + sorry + +/-! ## Layers 11–12: occupancy measures and the value-difference calculus -/ + +/-- The value of a run is the integral of the mean reward against the occupancy measure +(README Layer 11.1). -/ +theorem runValue_eq_integral_occupancy (hγ : γ < 1) + (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) (alg : Algorithm 𝓢 𝓐 ℝ) (μ : Measure 𝓢) + [IsProbabilityMeasure μ] : + M.runValue γ alg μ = (1 - γ : ℝ)⁻¹ * ∫ p, meanReward M.R p ∂(M.occupancy γ alg μ) := + sorry + +/-- The flow equation of occupancy measures (README Layer 11.1). -/ +theorem occupancy_map_fst (hγ : γ < 1) (alg : Algorithm 𝓢 𝓐 ℝ) (μ : Measure 𝓢) + [IsProbabilityMeasure μ] : + (M.occupancy γ alg μ).map Prod.fst = + (1 - γ : ℝ≥0∞) • μ + (γ : ℝ≥0∞) • (M.occupancy γ alg μ).bind M.P := + sorry + +/-- The performance difference lemma (README Layer 12.2, [AJKS, Lemma 1.16]). -/ +theorem runValue_sub_integral_value (hγ : γ < 1) (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) + (alg : Algorithm 𝓢 𝓐 ℝ) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] (μ : Measure 𝓢) + [IsProbabilityMeasure μ] : + M.runValue γ alg μ - ∫ s, M.value γ π s ∂μ = + (1 - γ : ℝ)⁻¹ * ∫ p, (M.qValue γ π p - M.value γ π p.1) ∂(M.occupancy γ alg μ) := + sorry + +end MDP + +/-! ## Layer 13: average reward and sensitive discount optimality -/ + +namespace MDP + +variable [Fintype 𝓢] [Nonempty 𝓢] [MeasurableSingletonClass 𝓢] [Fintype 𝓐] [Nonempty 𝓐] + [MeasurableSingletonClass 𝓐] (M : MDP 𝓢 𝓐 ℝ) + +/-- The gain of a stationary policy: the Cesàro limit of the expected rewards +(README Layer 13.1). -/ +def gain (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] (s : 𝓢) : ℝ := + limUnder atTop fun N : ℕ ↦ (N : ℝ)⁻¹ * + ∑ n ∈ range N, ∫ s', M.policyReward π s' ∂((M.stateKernel π ^ n) s) + +/-- Existence of a deterministic stationary Blackwell-optimal policy (README Layer 13.7, +[P, Theorem 10.1.4]). -/ +theorem exists_blackwell_optimal : + ∃ d : 𝓢 → 𝓐, ∃ γ₀ : ℝ≥0, γ₀ < 1 ∧ ∀ γ : ℝ≥0, γ₀ ≤ γ → γ < 1 → + ∀ s, M.value γ (Kernel.deterministic d (measurable_of_finite d)) s = M.optValue γ s := + sorry + +end MDP + +/-! ## Layer 15: planning with a generative model -/ + +section Generative + +variable [Fintype 𝓢] [Nonempty 𝓢] [MeasurableSingletonClass 𝓢] [Fintype 𝓐] [Nonempty 𝓐] + [MeasurableSingletonClass 𝓐] + +/-- The empirical transition kernel of `N` samples per pair of the generative model `ω` +(README Layer 14.3). -/ +def empiricalKernel (N : ℕ) (ω : ℕ → 𝓢 × 𝓐 → 𝓢) : Kernel (𝓢 × 𝓐) 𝓢 := + Kernel.ofFunOfCountable fun p ↦ (N : ℝ≥0∞)⁻¹ • ∑ i ∈ range N, Measure.dirac (ω i p) + +/-- The empirical MDP, with the rewards of `M`. -/ +def MDP.empirical (M : MDP 𝓢 𝓐 ℝ) {N : ℕ} (hN : 0 < N) (ω : ℕ → 𝓢 × 𝓐 → 𝓢) : MDP 𝓢 𝓐 ℝ where + P := empiricalKernel N ω + hP := sorry + R := M.R + +/-- The optimal action value `Q* = r + γ P v*`. -/ +def MDP.optQValue (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (p : 𝓢 × 𝓐) : ℝ := + MDP.meanReward M.R p + γ * ∫ s', M.optValue γ s' ∂(M.P p) + +/-- The plug-in policy is minimax optimal [AKY20, Theorem 1] (README Layer 15.3): with probability +at least `1 - δ`, every `εopt`-optimal stationary policy of the empirical MDP is +`(ε + 9 εopt / (1 - γ))`-optimal in `M`. -/ +theorem exists_const_qValue_ge_of_empirical : + ∃ C > 0, ∀ (M : MDP 𝓢 𝓐 ℝ) (r : 𝓢 × 𝓐 → ℝ) (hr : Measurable r), + M.R = Kernel.deterministic r hr → (∀ p, r p ∈ Set.Icc 0 1) → + ∀ (γ : ℝ≥0), 1 / 2 ≤ γ → γ < 1 → ∀ δ ε εopt : ℝ, 0 < δ → δ < 1 → 0 < ε → + ε ≤ Real.sqrt (1 / (1 - γ)) → ∀ (N : ℕ) (hN : 0 < N), + C * γ * Real.log (C * Fintype.card 𝓢 * Fintype.card 𝓐 / ((1 - γ) * δ)) / + ((1 - γ) ^ 3 * ε ^ 2) ≤ N → + 1 - δ ≤ (Bandits.streamMeasure M.P).real {ω | ∀ (π : Kernel 𝓢 𝓐) [IsMarkovKernel π], + (∀ p, |(M.empirical hN ω).qValue γ π p - (M.empirical hN ω).optQValue γ p| ≤ εopt) → + ∀ p, M.optQValue γ p - ε - 9 * εopt / (1 - γ) ≤ M.qValue γ π p} := + sorry + +end Generative + +/-! ## Layer 17: policy optimization -/ + +section PolicyOptimization + +variable [Fintype 𝓢] [Nonempty 𝓢] [MeasurableSingletonClass 𝓢] [Fintype 𝓐] [Nonempty 𝓐] + [MeasurableSingletonClass 𝓐] + +/-- The softmax policy of parameters `θ`. -/ +def softmaxPolicy (θ : 𝓢 → 𝓐 → ℝ) : Kernel 𝓢 𝓐 := + Kernel.ofFunOfCountable fun s ↦ ∑ a, ENNReal.ofReal (softmax (θ s) a) • Measure.dirac a + +instance (θ : 𝓢 → 𝓐 → ℝ) : IsMarkovKernel (softmaxPolicy θ) := sorry + +/-- The natural policy gradient iterates with step `η` from `θ₀ = 0`: in every state, the +multiplicative-weights update on `A^{π_t} / (1 - γ)` [AKLM21, Lemma 5.1] (README Layer 17.5). -/ +def npgParam (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (η : ℝ) : ℕ → 𝓢 → 𝓐 → ℝ + | 0 => 0 + | t + 1 => fun s a ↦ npgParam M γ η t s a + η / (1 - γ) * + (M.qValue γ (softmaxPolicy (npgParam M γ η t)) (s, a) - + M.value γ (softmaxPolicy (npgParam M γ η t)) s) + +/-- Global convergence of natural policy gradient [AKLM21, Theorem 5.3] (README Layer 17.5). -/ +theorem value_npg_ge (M : MDP 𝓢 𝓐 ℝ) {γ : ℝ≥0} (hγ : γ < 1) (r : 𝓢 × 𝓐 → ℝ) (hr : Measurable r) + (hMR : M.R = Kernel.deterministic r hr) (hr01 : ∀ p, r p ∈ Set.Icc 0 1) {η : ℝ} (hη : 0 < η) + (ρ : Measure 𝓢) [IsProbabilityMeasure ρ] {T : ℕ} (hT : 0 < T) : + ∫ s, M.optValue γ s ∂ρ - Real.log (Fintype.card 𝓐) / (η * T) - 1 / ((1 - γ) ^ 2 * T) ≤ + ∫ s, M.value γ (softmaxPolicy (npgParam M γ η T)) s ∂ρ := + sorry + +end PolicyOptimization + +end LMLRoadmaps.ReinforcementLearning diff --git a/LMLRoadmaps/ReinforcementLearning/metadata.toml b/LMLRoadmaps/ReinforcementLearning/metadata.toml new file mode 100644 index 0000000..3452649 --- /dev/null +++ b/LMLRoadmaps/ReinforcementLearning/metadata.toml @@ -0,0 +1 @@ +topic = "math.OC"