diff --git a/LMLRoadmaps/ReinforcementLearning/README.md b/LMLRoadmaps/ReinforcementLearning/README.md index b442706..ccfe0dd 100644 --- a/LMLRoadmaps/ReinforcementLearning/README.md +++ b/LMLRoadmaps/ReinforcementLearning/README.md @@ -2,8 +2,9 @@ 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 optimality equations for the finite-horizon, discounted and average-reward criteria, with + ε-optimal deterministic policies for countable action sets and optimal deterministic stationary + policies for finite and compact ones; - 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. @@ -26,17 +27,18 @@ the field's basic questions: - 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; +- order-unit contractions, abstract dynamic programming without attainment of the supremum, span + seminorms and topical maps; +- Markov processes on general measurable spaces: the Markov and strong Markov properties, kernels + as operators and resolvents as the inverses $(1-\gamma P)^{-1}$, 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. +- the keyed-stream model of adaptively collected data and the divergence decomposition regrouped by + keys. `README.md` is the definitive specification; `Suggested.lean` records selected interfaces and is not an exhaustive checklist. @@ -64,8 +66,11 @@ This roadmap owns Markov decision processes and reinforcement learning: | 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`) | +| Chain rule for the KL divergence of stopped histories at a stopping time, for arbitrary pairs of environments [GMS19, §2], and its bandit regrouping; data processing for `klBer` | Identification roadmap, Layers 2.1–2.2 | +| Transfer of every event about the first $s$ rewards of each arm from runs to reward streams | Identification roadmap, Layer 4.1 | +| Conditional MGF domination $\mathbb E[e^{\lambda X}\mid\mathcal F]\le e^{\psi(\lambda)}$, its exponential supermartingale and its time-uniform bound through Ville's inequality | Identification roadmap, Layer 4.2 | +| Wald's identity at a stopping time, for any environment | Identification roadmap, Layer 0.3 | +| Stream model of 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` | @@ -92,7 +97,9 @@ Outside this roadmap: - 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; + unbounded rewards and the weighted sup norms on general spaces they need [P, §6.10]; admissible + action sets $A(s)$ (every action is admissible in every state); 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 @@ -132,19 +139,33 @@ statement and says so. **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. +- The reward and the next state are drawn independently given the state and the action: the model + has these two kernels, not a joint kernel `Kernel (𝓢 × 𝓐) (𝓡 × 𝓢)`. Planning depends on the + rewards only through their means; learning from realized rewards uses their conditional + independence from the next states (Layer 7.1). - 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. + When LML merges its branch, the copy is deleted. The general reward space `𝓡` of `MDP 𝓢 𝓐 𝓡` + serves the environment and the run lemmas of Layer 7.1, which are stated for every `𝓡`; the + planning and learning theory takes `𝓡 = ℝ`. - 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)`. + steps $h\in\mathbb N$, with real rewards. 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)`. That of an episodic MDP is + entropy-mdp's curried `M.meanReward h s a`, defined as `MDP.meanReward (M.reward h) (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. +- Each learning item takes the reward model of its source: + - rewards are stochastic, unknown and observed by the learner in Layers 16.2 (asynchronous + Q-learning in `M.env μ`), 18.5–18.6 (in `episodeEnv`, Layer 7.7) and 21.1 (in `M.env μ`); + - they are observed in the data in Layers 22.1–22.4 and 23.4; + - they are deterministic in Layers 15, 16.1 (synchronous Q-learning), 16.3–16.4, 18.1–18.4, 19, + 21.2–21.3, 22.5 and 23.2–23.3, and known to the learner wherever it uses them; + - Layer 17 uses exact values, which depend on the reward kernel only through its mean, and + Layer 20 uses adversarial losses. **Policies.** - A history-dependent policy is an LML `Algorithm 𝓢 𝓐 ℝ`. @@ -155,17 +176,23 @@ statement and says so. - Episodic deterministic policies are the $H$-step policies `Fin H → 𝓢 → 𝓐` of entropy-mdp. **Criteria.** -- The discount factor is `γ : ℝ≥0` with `γ < 1`. +- The discount factor is `γ : ℝ≥0`, with `γ < 1` for the discounted criterion. The finite-horizon + statements of Layer 8 hold for every `γ`; `γ = 1` is the undiscounted return. - 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. +- Value functions are functions `𝓢 → ℝ`. Operator statements live on the Banach space + `boundedMeasurable 𝓢` of Layer 0.1: kernels act on it by `Kernel.integralCLM` (Layer 1.4), and + the Bellman operators are maps of it and of `boundedMeasurable (𝓢 × 𝓐)` (Layer 9.1). + Contraction rates, resolvent identities and the expansions of Layers 2 and 13 are proved there, + from the abstract results of Layers 0 and 2. Pointwise statements on `𝓢 → ℝ`, with explicit + bounds, are corollaries. - 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 $h0$. 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)$; + - Blackwell's argument is proved once, in the order-unit form. The pointwise bounds on + `𝓢 → ℝ` are its corollaries through `boundedMeasurable 𝓢`; LMLExplore's + `abs_sub_le_of_monotone_of_add_const` repeats the argument and is replaced by them. +3. **Abstract dynamic programming** [Ber22, Chapter 2]. Let $X$ be one of the instances of item 2, + with order unit $e$. Let $\{T_d\}_{d\in\mathcal D}$ be monotone maps of $X$ satisfying + Blackwell's condition with a common $\gamma<1$, and let $T:X\to X$ be their uniform supremum: + - $T_dx\le Tx$ for every $d$ and $x$; + - for every $x$ and $\varepsilon>0$, some $d$ is *ε-greedy* for $x$: $Tx-\varepsilon e\le T_dx$. + + Then $Tx$ is the least upper bound of the $T_dx$ (Mathlib's `IsLUB`), and it need not be + attained. A decision $d$ is *greedy* for $x$ when $T_dx=Tx$. Prove: + - $T$ is monotone and satisfies Blackwell's condition, hence is a γ-contraction; write $x^*$ for + its fixed point; - $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)\le x^*$ for every $d$, and every $d$ ε-greedy for $x^*$ has + $x^*-\frac{\varepsilon}{1-\gamma}e\le\mathrm{fix}(T_d)$; hence $x^*$ is the least upper bound + (`IsLUB`) of the $\mathrm{fix}(T_d)$; + - every greedy $d$ for $x^*$ has $\mathrm{fix}(T_d)=x^*$; for finite $\mathcal D$, a greedy + decision exists for every $x$; + - policy iteration ($d_{k+1}$ greedy for $\mathrm{fix}(T_{d_k})$), whenever these greedy + decisions exist, 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^*\|$. + - modified policy iteration $x_{k+1}=T_{d_{k+1}}^{m_k+1}x_k$, with $d_{k+1}$ greedy for $x_k$ + (whenever these greedy decisions exist) 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. + The hypothesis that $Tx$ is the least upper bound of the $T_dx$ does not replace the ε-greedy + decisions (completion checks). LMLExplore's `Analysis/FixedPoint/DynamicProgramming.lean` + assumes attainment, `IsGreatest (range fun d ↦ T d x) (B x)` for every $x$, which is the case + where every $x$ has a greedy decision. State its results under the two hypotheses above, with + policy iteration and modified policy iteration assuming in addition only the greedy decisions + they use. Layers 9–10 are instances of this item: countable action sets through the + ε-maximizers of item 6, finite ones through greedy policies. 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. + normed spaces), by the oscillation bound of item 2 (LMLExplore's + `IsTopical.orderUnitOsc_sub_le`), 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)$; @@ -332,7 +383,12 @@ General analysis, without probability. Suggested home: `Analysis/FixedPoint/`. 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. +the max-plus map $x\mapsto(\max_jA_{ij}+x_j)_i$ is topical. On `Fin 2 → ℝ`, the maps +$T_a x=(1+\gamma x_2,\gamma x_1)$ and $T_b x=(\gamma x_2,1+\gamma x_1)$ satisfy Blackwell's +condition, and $Tx=\max(T_ax,T_bx)$ is their least upper bound. Its fixed point +$(1-\gamma)^{-1}(1,1)$ exceeds the least upper bound $(1-\gamma^2)^{-1}(1,1)$ of +$\mathrm{fix}(T_a)$ and $\mathrm{fix}(T_b)$: no decision is ε-greedy for it when $\varepsilon<1$, +and the conclusions of item 3 fail. ## Layer 1: Markov processes on general measurable spaces @@ -384,11 +440,17 @@ $\kappa u-\kappa'u$ pointwise. - 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$. + - For $X_t\le b$ with $b>0$ and $\lambda\ge0$, prove the one-step bound + $\mathbb E[\exp(\lambda X_t-\psi_b(\lambda)\mathbb E[X_t^2|\mathcal F_t])|\mathcal F_t]\le1$, + with $\psi_b(\lambda)=(e^{\lambda b}-1-\lambda b)/b^2$, from + $e^{\lambda x}\le1+\lambda x+\psi_b(\lambda)x^2$ for $x\le b$. The increments + $\lambda X_t-\psi_b(\lambda)\mathbb E[X_t^2|\mathcal F_t]$ thereby satisfy the conditional MGF + domination of the Identification roadmap's Layer 4.2 at parameter $1$ with $\psi=0$: $S$ is a + sub-ψ process with variance process $W$ [HRMS20]. The supermartingale + $\exp(\lambda S_n-\psi_b(\lambda)W_n)$ and the time-uniform bounds below come from that layer; + do not build a separate supermartingale argument. - 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. + $P(\exists n,\ S_n\ge\eta W_n+\log(1/\delta)/\eta)\le\delta$. The proof is the domination of + $\eta X_t-\eta^2\mathbb E[X_t^2|\mathcal F_t]$, from $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 @@ -676,23 +750,37 @@ Suggested home: `SequentialLearning/`. - an independent array $Z_{k,j}\sim$ `ηY k ⊗ ηO k`, read at the $j$-th occurrence of key $k$. This generalizes LML's `Bandits.arrayMeasure` and `probSpace`. - - Deduce the transfer: for every event $E_j$ about the first $j$ draws of key $k$, the probability - that $E_j$ holds for the draws seen at some $j\le$ the count of $k$ before round $n$ is at most - the probability that $E_j$ holds for some $j\le n$ under the i.i.d. stream. - - Give the joint form over all keys. The single-arm and joint transfers of LMLExplore's - `Bandits/SumRewards.lean` become the case of the action key: replace their proofs by this one. -2. **Divergence decomposition regrouped by keys** [DMKV21, Lemma 5]. + - Deduce the keyed transfer: for every event $E_j$ about the first $j$ draws of key $k$, the + probability that $E_j$ holds for the draws seen at some $j\le$ the count of $k$ before round + $n$ is at most the probability that $E_j$ holds for some $j\le n$ under the i.i.d. stream. + Give the joint form over all keys. + - For the action key, this is the transfer of events about the first $s$ rewards of each arm + from runs to reward streams, which the Identification roadmap's Layer 4.1 owns. State the + keyed transfer in its statement shape, so that the two agree for the action key. +2. **Divergence decomposition regrouped by keys** [GMS19, §2], [DMKV21, Lemma 5]. + - The chain rule for the KL divergence of stopped histories, + $\mathrm{KL}\le\mathbb E\big[\sum_{t<\tau}\mathrm{KL}(\text{step}_t\,\|\,\text{step}'_t)\big]$ for + a stopping time τ almost surely finite under the first environment, with equality when τ is + also almost surely finite under the second, is the Identification roadmap's Layer 2.1, for + arbitrary pairs of environments. At a fixed horizon it is LML's + `IsAlgEnvSeq.klDiv_map_history_stepKernel`. - For two key-determined environments with the same key maps and the same initial observation - law, prove that KL(histories of length $n$) equals - $\sum_k\mathbb E[N_k(n)]\big(\mathrm{KL}(\eta^Y_k,\eta'^Y_k)+\mathrm{KL}(\eta^O_k,\eta'^O_k)\big)$. - Use LML's `IsAlgEnvSeq.klDiv_map_history_stepKernel`. - - At a stopping time τ, almost surely finite under the first environment, prove the same with - $\le$ and $N_k(\tau)$, with equality when τ is also almost surely finite under the second. + law, prove that the step divergence of round $t$ is + $\mathrm{KL}(\eta^Y_k,\eta'^Y_k)+\mathrm{KL}(\eta^O_k,\eta'^O_k)$ at the key $k$ of round $t$, + by the conditional independence of item 1. + - Regroup by keys, with the keyed form of Wald's identity + $\mathbb E\big[\sum_{t<\tau}f(k_t)\big]=\sum_kf(k)\,\mathbb E[N_k(\tau)]$ for $f\ge0$ (the + Identification roadmap's Layer 0.3): KL(histories of length $n$) equals + $\sum_k\mathbb E[N_k(n)]\big(\mathrm{KL}(\eta^Y_k,\eta'^Y_k)+\mathrm{KL}(\eta^O_k,\eta'^O_k)\big)$, + and at a stopping time τ, almost surely finite under the first environment, the same holds + with $\le$ and $N_k(\tau)$, with equality when τ is also almost surely finite under the + second. - Prove the transportation form: for every event $E$ of the stopped history, - $\mathrm{kl}(P(E),P'(E))\le\sum_k\mathbb E[N_k(\tau)]\big(\mathrm{KL}(\eta^Y_k,\eta'^Y_k)+\mathrm{KL}(\eta^O_k,\eta'^O_k)\big)$. - Use LMLExplore's `klDiv_stoppedHistMeasure_le` and the data processing for `klBer`. - - The stationary-bandit statements of the Identification roadmap's Layer 2.1 are the case of the - action key: replace their proofs by these. + $\mathrm{kl}(P(E),P'(E))\le\sum_k\mathbb E[N_k(\tau)]\big(\mathrm{KL}(\eta^Y_k,\eta'^Y_k)+\mathrm{KL}(\eta^O_k,\eta'^O_k)\big)$, + by the data processing for `klBer` of the Identification roadmap's Layer 2.2. + - For the action key, these are the bandit decompositions of the Identification roadmap's + Layer 2.1. State the keyed forms in their statement shape. Layer 14.6 gives the instance of + MDP runs. Completion checks: for the action key, item 1 is LML's per-arm stream model and item 2 is LML's `IsAlgEnvSeq.klDiv_map_history`. @@ -733,8 +821,14 @@ Completion checks: for the action key, item 1 is LML's per-arm stream model and `M.saKernel π`, acting on functions of the state–action pair. 3. **State–action marginals.** - For every run of every algorithm, prove $\mathrm{law}(S_{n+1})=P\circ_m\mathrm{law}(S_n,A_n)$. - - For a Markov policy, prove $\mathrm{law}(S_n,A_n)=\mu_n\otimes_m\pi_n$, where $\mu_0=\mu$ and - $\mu_{n+1}=P\circ_m(\mu_n\otimes_m\pi_n)$. + - Define the state marginals once, for a sequence of transition kernels + `P : ℕ → Kernel (𝓢 × 𝓐) 𝓢`, a Markov policy π and an initial law μ: `MDP.stateMarginal P π μ`, + with $\mu_0=\mu$ and $\mu_{n+1}=P_n\circ_m(\mu_n\otimes_m\pi_n)$. The marginals of `M` are the + case `fun _ ↦ M.P`, those of an episodic MDP the case `M.trans` (Layer 11.4). LMLExplore + defines them twice, as `MDP.stateMarginal M π μ` and `EpisodicMDP.stateMarginal M π μ`; both + become this definition. + - For a Markov policy, prove $\mathrm{law}(S_n,A_n)=\mu_n\otimes_m\pi_n$ for the marginals of + `fun _ ↦ M.P`. - Every discounted, finite-horizon and Cesàro quantity of Layers 8–13 is a function of these marginals. Prove the marginal formula of each one where it is defined. 4. **Values.** Rewards are bounded: $|x|\le C$ for `M.R p`-almost every $x$ and every $p$. For a @@ -747,8 +841,9 @@ Completion checks: for the action key, item 1 is LML's per-arm stream model and For an algorithm define: - the discounted run value `M.runValue γ alg μ`, the expectation under `trajMeasure` of $\sum_n\gamma^nr(S_n,A_n)$; - - the $N$-step return with terminal reward $u$, `M.runReturn N u alg μ`, the expectation of - $\sum_{n0$, construct a measurable ε-greedy policy from Layer 0.6. - Prove that both operators are monotone and satisfy $T(v+c)=Tv+\gamma c$ for constants $c$. - Deduce that they are γ-contractions for the sup norm by Layer 0.2. - - Prove that they preserve bounded measurable functions, and that `M.greedy γ v` is measurable for - measurable bounded $v$. - - Prove that randomizing does not increase the supremum [P, Proposition 6.2.1]. -2. **Evaluation** [P, Theorem 6.1.1]. Prove that $v^\pi$ is the unique bounded measurable fixed point - of the evaluation operator, and that $v^\pi=R_\gamma(P_\pi)r_\pi$ with the resolvent of - Layer 1.4. This holds for arbitrary `𝓐` and every stationary policy. + - Prove that the evaluation operators, for every `𝓐`, and the optimality operator, for countable + `𝓐`, preserve bounded measurable functions, and that `M.greedy γ v` is measurable for + measurable $v$. + - Prove that randomizing does not increase the supremum: `M.bellmanEval γ π v ≤ M.bellman γ v` + for bounded measurable $v$ and every `𝓐` [P, Proposition 6.2.1]. LMLExplore's + `MDP.bellmanEval_le_bellman` assumes finitely many actions. +2. **Optimality of backward induction** [P, §4.2, Theorems 4.3.2–4.3.4, 4.4.2], [Ber12, Chapter + 1]. Let `𝓐` be countable. Prove: + - for every algorithm and every probability measure μ, + `M.runReturn γ N u alg μ` $\le\int T^Nu\,d\mu$, by telescoping + $\mathbb E\,(T^{N-n}u)(S_n)\ge\mathbb E\,r(S_n,A_n)+\gamma\,\mathbb E\,(T^{N-n-1}u)(S_{n+1})$ + along the marginals of Layer 7.3; no reduction to Markov policies is needed; + - for $\varepsilon_n>0$, the Markov deterministic policy playing at round $n0$, every + measurable policy $d$ ε-greedy for $v^*$ has $v^d\ge v^*-\varepsilon/(1-\gamma)$, so measurable + deterministic stationary ε-optimal policies exist from every initial law; + - a stationary policy is optimal if and only if its value solves the optimality equation; + - $Q^*$ is the unique fixed point of `M.qBellman γ` in `boundedMeasurable (𝓢 × 𝓐)`, and + $v^*(s)=\sup_aQ^*(s,a)$. + + LMLExplore's `bellman_optValue`, `eq_optValue_of_bellman_eq`, `le_optValue_of_le_bellman` and + `eq_optQValue_of_lookahead_iSup_eq` assume finitely many actions; state them for countably + many. +5. **Finite action sets** [P, Theorems 6.2.7, 6.2.9, 6.2.10 (a)]. For finite `𝓐`, prove: - the deterministic stationary policy greedy with respect to $v^*$ is optimal from every initial law; - - $v^*=\max_dv^d$ over measurable deterministic stationary policies; - - a stationary policy is optimal if and only if its value solves the optimality equation; - - $Q^*$ is the unique bounded measurable fixed point of $Q\mapsto r+\gamma P\max_aQ$. -5. **Countable action sets** [P, Theorem 6.2.11]. For countable `𝓐`, prove: - - $T$ preserves bounded measurable functions, and $v^*$ is its unique bounded measurable fixed - point (through items 2 and 3 (a)); - - for $\varepsilon>0$, a measurable deterministic stationary $\varepsilon$-optimal policy exists, - by Layer 0.6. + - $v^*=\max_dv^d$ over measurable deterministic stationary policies. 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)$ @@ -873,17 +1018,23 @@ instance of Layer 0.3 with $T_d$ the evaluation operators of deterministic stati - 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 +(one state, actions $\mathbb N_{\ge1}$, $r(a)=1-1/a$) has no optimal policy but ε-optimal ones +(item 4); 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. +`boundedMeasurable 𝓢` (Layer 0.1). State the first and last bullets of item 1, and item 5, for +countable `𝓐`. Each rate is proved for the operators of Layer 9.1 on `boundedMeasurable 𝓢`, from +Mathlib's `ContractingWith` (item 1) or from Layer 0.3 (items 2–3), and its pointwise form, with +the constants shown, is a corollary. LMLExplore's `PolicyIteration.lean` and +`ModifiedPolicyIteration.lean` prove the rates pointwise; derive them from the abstract +`IsPolicyIteration.norm_sub_le` and `IsModifiedPolicyIteration.norm_sub_le`. 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)$; + - $\|v_n-v^*\|\le\gamma^nB/(1-\gamma)$ (`ContractingWith.apriori_dist_iterate_fixedPoint_le`); - 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)$; @@ -957,9 +1108,10 @@ policy iteration on a two-state, two-action MDP terminates in at most two improv 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. + - Prove all of this from Layers 9.3–9.5 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)$; + - define $d^\pi_h=\mathrm{law}(S_h,A_h)=\mu_h\otimes_m\pi_h$, with the state marginals $\mu_h$ of + Layer 7.3 for the kernels `M.trans`; - 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$. @@ -975,8 +1127,8 @@ dual LP is a bandit's simplex. 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$. +generality. Here $\|\cdot\|$ is the sup norm, and an estimated model $\hat M$ has its own transition +and reward kernels $\hat P$ and $\hat R$, with mean reward $\hat r$. 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 @@ -987,11 +1139,15 @@ $M$. - 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 simulation lemma [AJKS, Lemma 2.2], [KS02], with a reward error: + $Q^\pi_M-Q^\pi_{\hat M}=R_\gamma(\hat P^{\pi}_{SA})\big((r-\hat r)+\gamma(P-\hat P)v^\pi_M\big)$. + Give its episodic form and, for rewards of $M$ in $[0,1]$, the bound + $\|Q^\pi_M-Q^\pi_{\hat M}\|\le(1-\gamma)^{-1}\|r-\hat r\|+\gamma(1-\gamma)^{-2}\sup_{s,a}\mathrm{tvDist}(P(s,a),\hat P(s,a))$. + - The componentwise bounds [AJKS, Lemma 2.5], with a reward error: + $R_\gamma(\hat P^{\hat\pi^*}_{SA})\big((r-\hat r)+\gamma(P-\hat P)v^*\big)\le Q^*-\hat Q^*\le R_\gamma(\hat P^{\pi^*}_{SA})\big((r-\hat r)+\gamma(P-\hat P)v^*\big)$. + - Every statement of LMLExplore's `MarkovDecisionProcess/Simulation.lean` assumes + `meanReward M'.R = meanReward M.R`; state them with the reward error. It serves the perturbed + rewards of Layers 15.4 (c) and 21.3 and the estimated rewards of Layer 21.1. - 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 @@ -1023,7 +1179,8 @@ $M$. 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 +with $\hat P=P$ and $\hat r=r$ is trivial, and with $\hat P=P$ it reduces to +$Q^\pi_M-Q^\pi_{\hat M}=R_\gamma(P^\pi_{SA})(r-\hat r)$; 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 @@ -1039,8 +1196,9 @@ the limiting and deviation matrices of Layer 2 of `M.stateKernel π`. gain (Layer 1.8, with the Poisson solution $D_\pi r_\pi$). - Prove that the bias is the Cesàro limit of the total reward when the gain is zero [P, Proposition 8.2.2]. - - Prove the Laurent expansion of $v^\pi_\gamma$ [P, Theorem 8.2.3] from Layer 2.2, and its - corollaries $v^\pi_\gamma=(1-\gamma)^{-1}g^\pi+h^\pi+o(1)$ and + - Prove the Laurent expansion of $v^\pi_\gamma$ [P, Theorem 8.2.3] from Layer 2.2, with $T$ the + action of $P_\pi$ on `boundedMeasurable 𝓢` and $v^\pi_\gamma=(1-\gamma P_\pi)^{-1}r_\pi$ + (Layer 9.2). Prove its corollaries $v^\pi_\gamma=(1-\gamma)^{-1}g^\pi+h^\pi+o(1)$ and $g^\pi=\lim_{\gamma\uparrow1}(1-\gamma)v^\pi_\gamma$ [P, Corollaries 8.2.4–8.2.5]. - Prove the evaluation equations $(I-P_\pi)g=0$ and $g+(I-P_\pi)h=r_\pi$, the description of all their solutions, and the unichain form [P, Theorem 8.2.6, Corollary 8.2.7]. @@ -1128,12 +1286,14 @@ an item says otherwise. 1. **Counts and empirical kernels.** - In `M.env μ`, counts of state–action pairs are LML's `pullCount` of the pair process $n\mapsto(S_n,A_n)$. - - In `statesEnv`, the episodic counts $N^k_h(s,a)=\#\{i0$ such that, for $\gamma\in[1/2,1)$, $\varepsilon\in(0,1]$, $\delta\in(0,1)$, $T\ge2$, learning rates with @@ -1311,10 +1484,11 @@ and item 3 reduces to averages of i.i.d. samples; TD with tabular features has $ ## 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 +Finite `𝓢`, `𝓐`, exact values unless stated. The reward kernel is any one with rewards in $[0,1]$: +exact values depend on it only through the mean reward $r$, and deterministic rewards are not +assumed. ρ 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]. @@ -1409,9 +1583,12 @@ $\eta/(1-\gamma)$; soft policy iteration is the case $\eta=(1-\gamma)/\tau$ of i ## 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. +Episodic MDPs with stage-dependent transitions, initial law μ and $K$ episodes. Regret is that of +Layer 14.7. Each item takes the reward model of its source: +- in items 1–4, rewards are deterministic in $[0,1]$ and known to the learner (`M.HasRewardFn r`), + and algorithms are algorithms in `statesEnv` (Layer 7.7); +- in items 5–6, rewards are stochastic and unknown, and algorithms are algorithms in `episodeEnv` + (Layer 7.7), which observe them. 1. **UCBVI** [AJKS, Theorem 7.1], corrected. - Define the algorithm: value iteration on the empirical kernel with bonus @@ -1430,12 +1607,15 @@ learner (`M.HasRewardFn r`), initial law μ and $K$ episodes. Algorithms are alg 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)$. + Prove it for algorithms in `statesEnv` and in `episodeEnv`: the hard MDPs have deterministic + rewards, so the rewards observed in `episodeEnv` are functions of the states and actions. 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)$. @@ -1444,11 +1624,16 @@ learner (`M.HasRewardFn r`), initial law μ and $K$ episodes. Algorithms are alg - 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$. + Lemma 12, for the transition event (8) and the reward event (9): + $\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$. For the rewards, the biased sample variance is + at most the empirical mean. 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. + - Setting: nonnegative stochastic rewards whose sum over the $H$ steps of an episode is at most + $H$ almost surely under every policy [ZCLD24, Assumption 1], which contains rewards per step + in $[0,1]$. + - Define [ZCLD24, Algorithm 1], with its empirical rewards and kernels, $c_1=460/9$, + $c_2=2\sqrt2$, $c_3=544/9$ and $\delta'=\delta/(200SAH^2K^2)$. - 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 @@ -1545,20 +1730,24 @@ Completion checks: for $H=1$ and one state, item 1 is exponential weights and it ## 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. + $34DS\sqrt{AT\log(T/\delta)}$. The confidence events for the rewards and the transitions + come from the stream model of Layer 14.2 with Hoeffding's inequality and Layer 3.3, and the + deviation of $\sum_tY_t$ from $\sum_tr(S_t,A_t)$ from Azuma–Hoeffding. 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. + $0.015\sqrt{DSAT}$. Use the change of measure of Layer 14.6. 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$, @@ -1677,9 +1866,14 @@ Every new definition comes with measurability, evaluation and extensionality lem 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$; + - for $\gamma<1$, the finite-horizon values $T^Nu$ of Layer 8.2 converge to $v^*_\gamma$ as + $N\to\infty$, uniformly and for every terminal value $u$; - $(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. +- The pointwise statements of Layers 9–10 are corollaries of the statements on + `boundedMeasurable 𝓢`, and the countable-action statements of Layer 9.4 specialize to the finite + ones of Layer 9.5. +- The lower bound of Layer 18.4, for algorithms in `episodeEnv`, 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 @@ -1698,6 +1892,8 @@ Books and monographs: - [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). +- [Ber12] D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. II, 4th ed., Athena + Scientific (2012). - [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). @@ -1716,6 +1912,8 @@ Books and monographs: - [Rev84] D. Revuz, *Markov Chains*, 2nd ed., North-Holland (1984). Papers: +- [AGP21] A. Al Marjani, A. Garivier and A. Proutière, Navigating to the best policy in Markov + decision processes, NeurIPS 2021, arXiv:2106.02847. - [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. @@ -1741,6 +1939,10 @@ Papers: - [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). +- [GMS19] A. Garivier, P. Ménard and G. Stoltz, Explore first, exploit next: the true shape of + regret in bandit problems, *Math. Oper. Res.* 44 (2019), arXiv:1602.07182. +- [HRMS20] S. R. Howard, A. Ramdas, J. McAuliffe and J. Sekhon, Time-uniform Chernoff bounds via + nonnegative supermartingales, *Probab. Surveys* 17 (2020), arXiv:1808.03204. - [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 @@ -1764,6 +1966,8 @@ Papers: 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). +- [KS02] M. Kearns and S. Singh, Near-optimal reinforcement learning in polynomial time, *Machine + Learning* 49 (2002). - [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 @@ -1777,6 +1981,8 @@ Papers: 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. +- [OPT18] J. Ok, A. Proutière and D. Tranos, Exploration in structured reinforcement learning, + NeurIPS 2018, arXiv:1806.00775. - [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 diff --git a/LMLRoadmaps/ReinforcementLearning/Suggested.lean b/LMLRoadmaps/ReinforcementLearning/Suggested.lean index fd453a5..a2dc341 100644 --- a/LMLRoadmaps/ReinforcementLearning/Suggested.lean +++ b/LMLRoadmaps/ReinforcementLearning/Suggested.lean @@ -48,6 +48,33 @@ theorem lipschitzWith_of_monotone_of_add_const_le {T : (ι → ℝ) → ι → LipschitzWith γ T := sorry +section AbstractDP + +variable {D : Type*} {T : D → (ι → ℝ) → ι → ℝ} {B : (ι → ℝ) → ι → ℝ} {γ : ℝ≥0} + +/-- Abstract dynamic programming without attainment (README Layer 0.3), on `ι → ℝ` with the sup +norm (the README asks for the order-unit form). The maps `T d` are monotone and satisfy Blackwell's +condition, and `B` is their uniform supremum: `T d ≤ B`, and for every `ε > 0` some decision is +`ε`-greedy. Then the fixed point of `B` is the least upper bound of the fixed points of the `T d`. +`IsLUB (Set.range fun d ↦ T d x) (B x)` alone would not suffice. -/ +theorem isLUB_setOf_isFixedPt (hγ : γ < 1) (hT : ∀ d, Monotone (T d)) + (hT_add : ∀ d x (c : ℝ), 0 ≤ c → T d (x + fun _ ↦ c) ≤ T d x + fun _ ↦ γ * c) + (hle : ∀ d x, T d x ≤ B x) (hgreedy : ∀ x, ∀ ε > 0, ∃ d, B x - (fun _ ↦ ε) ≤ T d x) + {x : ι → ℝ} (hx : Function.IsFixedPt B x) : + IsLUB {y | ∃ d, Function.IsFixedPt (T d) y} x := + sorry + +/-- A decision `ε`-greedy for the fixed point `x` of `B` has its fixed point within +`ε / (1 - γ)` of `x` (README Layer 0.3). -/ +theorem abs_sub_le_of_isFixedPt_of_sub_le (hγ : γ < 1) (hT : ∀ d, Monotone (T d)) + (hT_add : ∀ d x (c : ℝ), 0 ≤ c → T d (x + fun _ ↦ c) ≤ T d x + fun _ ↦ γ * c) + (hle : ∀ d x, T d x ≤ B x) {x : ι → ℝ} (hx : Function.IsFixedPt B x) {d : D} {ε : ℝ} + (hd : x - (fun _ ↦ ε) ≤ T d x) {y : ι → ℝ} (hy : Function.IsFixedPt (T d) y) (i : ι) : + |x i - y i| ≤ ε / (1 - γ) := + sorry + +end AbstractDP + /-- 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 @@ -135,6 +162,17 @@ section Concentration variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P] {ℱ : Filtration ℕ mΩ} +/-- The one-step bound behind Freedman's inequality (README Layer 3.1): for `X t ≤ b`, the +increment `l X t - ψ_b(l) E[X t ^ 2 | ℱ t]` has conditional exponential moment at most `1`. This is +the conditional MGF domination of the Identification roadmap (Layer 4.2) at parameter `1` with +`ψ = 0`, whose supermartingale and time-uniform bound give the forms of Freedman's inequality. -/ +theorem condExp_exp_mul_sub_le_one {X : ℕ → Ω → ℝ} {b l : ℝ} (hb : 0 < b) (hl : 0 ≤ l) + (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 ω ≤ b) (t : ℕ) : + P[fun ω ↦ Real.exp (l * X t ω - (Real.exp (l * b) - 1 - l * b) / b ^ 2 * + P[fun ω ↦ X t ω ^ 2 | ℱ t] ω) | ℱ t] ≤ᵐ[P] 1 := + sorry + /-- 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 < δ) @@ -215,6 +253,18 @@ def meanReward (R : Kernel (𝓢 × 𝓐) ℝ) (p : 𝓢 × 𝓐) : ℝ := ∫ x def stateKernel (M : MDP 𝓢 𝓐 ℝ) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] : Kernel 𝓢 𝓢 := M.P ∘ₖ (Kernel.id ×ₖ π) +/-- The state–action kernel of a stationary policy `π`. -/ +def saKernel (M : MDP 𝓢 𝓐 ℝ) (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] : Kernel (𝓢 × 𝓐) (𝓢 × 𝓐) := + (Kernel.id ×ₖ π) ∘ₖ M.P + +/-- The state marginals of the Markov policy `π` from the initial law `μ`, for a sequence `P` of +transition kernels (README Layer 7.3): `μ₀ = μ` and `μₙ₊₁ = P n ∘ₘ (μₙ ⊗ₘ π n)`. The marginals of +an MDP `M` are those of `fun _ ↦ M.P`, those of an episodic MDP those of its kernels `trans`. -/ +def stateMarginal (P : ℕ → Kernel (𝓢 × 𝓐) 𝓢) (π : ℕ → Kernel 𝓢 𝓐) (μ : Measure 𝓢) : + ℕ → Measure 𝓢 + | 0 => μ + | n + 1 => P n ∘ₘ (stateMarginal P π μ n ⊗ₘ π n) + /-- The mean reward of a stationary policy. -/ def policyReward (M : MDP 𝓢 𝓐 ℝ) (π : Kernel 𝓢 𝓐) (s : 𝓢) : ℝ := ∫ a, meanReward M.R (s, a) ∂(π s) @@ -232,18 +282,43 @@ def runValue [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (alg : Algor ℝ := ∫ ω, ∑' n, (γ : ℝ) ^ n * meanReward M.R ((ω n).obs, (ω n).action) ∂(trajMeasure alg (M.env μ)) +/-- The `N`-step return with discount `γ` and terminal value `u` of a run of the algorithm `alg` +from the initial law `μ` (README Layer 7.4), for every `γ`: `γ = 1` is the undiscounted return. -/ +def runReturn [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (N : ℕ) (u : 𝓢 → ℝ) + (alg : Algorithm 𝓢 𝓐 ℝ) (μ : Measure 𝓢) : ℝ := + ∫ ω, (∑ n ∈ range N, (γ : ℝ) ^ n * meanReward M.R ((ω n).obs, (ω n).action) + + (γ : ℝ) ^ N * u (ω N).obs) ∂(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. -/ +/-- The optimal action value `Q* = r + γ P v*`. -/ +def optQValue [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (p : 𝓢 × 𝓐) : ℝ := + meanReward M.R p + γ * ∫ s', M.optValue γ s' ∂(M.P p) + +/-- The Bellman optimality operator (README Layer 8.1), for every discount factor. -/ def bellman (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (v : 𝓢 → ℝ) (s : 𝓢) : ℝ := ⨆ a, (meanReward M.R (s, a) + γ * ∫ s', v s' ∂(M.P (s, a))) +/-- The evaluation operator `v ↦ r_π + γ P_π v` of a stationary policy (README Layer 8.1). -/ +def bellmanEval (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (π : Kernel 𝓢 𝓐) (v : 𝓢 → ℝ) (s : 𝓢) : ℝ := + ∫ a, (meanReward M.R (s, a) + γ * ∫ s', v s' ∂(M.P (s, a))) ∂(π s) + /-- 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 deterministic policy `d` is `ε`-greedy for `v` (README Layer 8.1); `ε = 0` is greediness. +For countably many actions, Layer 0.6 constructs measurable `ε`-greedy policies for `ε > 0`. -/ +def IsApproxGreedy (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (ε : ℝ) (v : 𝓢 → ℝ) (d : 𝓢 → 𝓐) : Prop := + ∀ s, M.bellman γ v s - ε ≤ meanReward M.R (s, d s) + γ * ∫ s', v s' ∂(M.P (s, d s)) + +/-- The Bellman optimality operator on action values (README Layer 9.1), whose fixed point is +`Q*`; Q-learning is a stochastic approximation of it. -/ +def qBellman (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (Q : 𝓢 × 𝓐 → ℝ) (p : 𝓢 × 𝓐) : ℝ := + meanReward M.R p + γ * ∫ s', ⨆ a, Q (s', a) ∂(M.P p) + /-- The discounted state–action occupancy measure of a run (README Layer 11.1). -/ def occupancy [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (alg : Algorithm 𝓢 𝓐 ℝ) (μ : Measure 𝓢) : Measure (𝓢 × 𝓐) := @@ -270,32 +345,72 @@ namespace MDP variable [Nonempty 𝓢] (M : MDP 𝓢 𝓐 ℝ) {γ : ℝ≥0} +/-! ## Layer 8: Bellman operators and the finite horizon -/ + +/-- Backward induction gives the supremum of the `N`-step return over all algorithms, for every +discount factor and countably many actions (README Layer 8.2, [P, Theorem 4.3.2]). -/ +theorem iSup_runReturn_eq_bellman_iterate [Countable 𝓐] [Nonempty 𝓐] + (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) {u : 𝓢 → ℝ} (hu : Measurable u) + (hu_bdd : ∃ C, ∀ s, |u s| ≤ C) (N : ℕ) (s : 𝓢) : + ⨆ alg : Algorithm 𝓢 𝓐 ℝ, M.runReturn γ N u alg (Measure.dirac s) = (M.bellman γ)^[N] u s := + sorry + +/-- For finitely many actions, the Markov policy greedy for `T^[N - n - 1] u` at round `n` attains +the optimal `N`-step return from every initial law (README Layer 8.2, [P, Theorems 4.3.3, +4.4.2]). -/ +theorem runReturn_markov_greedy [Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] + (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) {u : 𝓢 → ℝ} (hu : Measurable u) + (hu_bdd : ∃ C, ∀ s, |u s| ≤ C) (N : ℕ) + (hg : ∀ n, Measurable (M.greedy γ ((M.bellman γ)^[N - n - 1] u))) + (μ : Measure 𝓢) [IsProbabilityMeasure μ] : + M.runReturn γ N u (Algorithm.markov fun n ↦ + Kernel.deterministic (M.greedy γ ((M.bellman γ)^[N - n - 1] u)) (hg n)) μ = + ∫ s, (M.bellman γ)^[N] u s ∂μ := + sorry + /-! ## Layers 9–10: discounted optimality and algorithms -/ -/-- The optimality equation (README Layer 9.4). -/ -theorem bellman_optValue [Fintype 𝓐] [Nonempty 𝓐] [MeasurableSingletonClass 𝓐] +/-- The optimality equation, for countably many actions (README Layer 9.4). -/ +theorem bellman_optValue [Countable 𝓐] [Nonempty 𝓐] (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 𝓐] +/-- Uniqueness of bounded measurable solutions of the optimality equation, for countably many +actions (README Layer 9.4). -/ +theorem eq_optValue_of_bellman_eq [Countable 𝓐] [Nonempty 𝓐] (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). -/ +/-- For countably many actions, `ε`-optimal measurable deterministic stationary policies exist +(README Layer 9.4, [P, Theorem 6.2.11]). -/ +theorem exists_optValue_sub_le_value [Countable 𝓐] [Nonempty 𝓐] (hγ : γ < 1) + (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) {ε : ℝ} (hε : 0 < ε) : + ∃ (d : 𝓢 → 𝓐) (hd : Measurable d), ∀ s, + M.optValue γ s - ε ≤ M.value γ (Kernel.deterministic d hd) s := + sorry + +/-- `Q*` is a fixed point of the action-value optimality operator, for countably many actions +(README Layer 9.4). -/ +theorem qBellman_optQValue [Countable 𝓐] [Nonempty 𝓐] (hγ : γ < 1) + (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) : + M.qBellman γ (M.optQValue γ) = M.optQValue γ := + sorry + +/-- The greedy policy for `v*` is optimal, for finitely many actions (README Layer 9.5). -/ 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 𝓐] +/-- Value iteration, for countably many actions (README Layer 10.1, [P, Theorem 6.3.3 (d)]). -/ +theorem abs_bellman_iterate_sub_optValue_le [Countable 𝓐] [Nonempty 𝓐] (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 : 𝓢) : + (hv_bdd : ∃ C, ∀ s, |v s| ≤ C) {B : ℝ} (hB : ∀ s, |M.bellman γ v s - v s| ≤ B) (n : ℕ) + (s : 𝓢) : |(M.bellman γ)^[n] v s - M.optValue γ s| ≤ γ ^ n * B / (1 - γ) := sorry @@ -324,6 +439,16 @@ theorem runValue_sub_integral_value (hγ : γ < 1) (hR : ∃ C, ∀ p, ∀ᵐ x (1 - γ : ℝ)⁻¹ * ∫ p, (M.qValue γ π p - M.value γ π p.1) ∂(M.occupancy γ alg μ) := sorry +/-- The simulation lemma with a reward error (README Layer 12.2, [AJKS, Lemma 2.2], [KS02]): +`Q^π_M - Q^π_M' = R_γ(P'^π_SA) ((r - r') + γ (P - P') v^π_M)`. -/ +theorem qValue_sub_qValue (M' : MDP 𝓢 𝓐 ℝ) (hγ : γ < 1) + (hR : ∃ C, ∀ p, ∀ᵐ x ∂(M.R p), |x| ≤ C) (hR' : ∃ C, ∀ p, ∀ᵐ x ∂(M'.R p), |x| ≤ C) + (π : Kernel 𝓢 𝓐) [IsMarkovKernel π] (p : 𝓢 × 𝓐) : + M.qValue γ π p - M'.qValue γ π p = + resolvent γ (M'.saKernel π) (fun q ↦ meanReward M.R q - meanReward M'.R q + + γ * (∫ s', M.value γ π s' ∂(M.P q) - ∫ s', M.value γ π s' ∂(M'.P q))) p := + sorry + end MDP /-! ## Layer 13: average reward and sensitive discount optimality -/ @@ -366,10 +491,6 @@ def MDP.empirical (M : MDP 𝓢 𝓐 ℝ) {N : ℕ} (hN : 0 < 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`. -/ @@ -408,9 +529,10 @@ def npgParam (M : MDP 𝓢 𝓐 ℝ) (γ : ℝ≥0) (η : ℝ) : ℕ → 𝓢 (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 < η) +/-- Global convergence of natural policy gradient [AKLM21, Theorem 5.3] (README Layer 17.5), for +every reward kernel with rewards in `[0, 1]`: exact values only see the mean reward. -/ +theorem value_npg_ge (M : MDP 𝓢 𝓐 ℝ) {γ : ℝ≥0} (hγ : γ < 1) + (hR : ∀ p, ∀ᵐ x ∂(M.R p), x ∈ 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 ∂ρ :=