All missions

Motivation

A retailer choosing which products to display, a platform choosing which items to recommend, and a broadcaster choosing which content to stream all face an assortment problem: offer a set of products, observe what customers buy, and earn the revenue of the purchased item. The standard demand model is the multinomial logit (MNL) model, under which the optimal assortment without capacity constraints consists of the most profitable products (Talluri and Van Ryzin, 2004). When the customers' preferences are unknown, the seller must learn them from sales, and the quality of a learning policy is measured by its regret: the cumulative revenue lost relative to an omniscient seller.

When the product catalogue is very large, or products are described by a continuous attribute such as quality, the discrete model becomes a continuum. Peeters, den Boer and Mandjes (arXiv:1807.06497, published in Operations Research, 2022) introduced a continuous analogue of the MNL model and studied learning in it. Their first main result, the goal of this mission, is that a simple stochastic approximation policy has worst-case regret of order $\log T$ over $T$ customers.

• 1951: Robbins and Monro introduce stochastic approximation for finding the root of a function observed with noise (doi:10.1214/aoms/1177729586).
• 2010: Rusmevichientong, Shen and Shmoys give adaptive policies for capacitated MNL assortment (doi:10.1287/opre.1100.0866).
• 2011: Broadie, Cicek and Zeevi give mean-square rates for Kiefer–Wolfowitz type stochastic approximation (doi:10.1287/opre.1110.0970).
• 2019: Agrawal, Avadhanula, Goyal and Zeevi give an $\tilde O(\sqrt{NT})$-regret UCB policy for discrete MNL bandits (doi:10.1287/opre.2018.1832).
• 2021/2022: Peeters, den Boer and Mandjes prove $O(\log T)$ worst-case regret for the continuum model, with a matching $\Omega(\log T)$ lower bound.

Setting

The products are the points $x\in[0,1]$, and the revenue function $w:[0,1]\to[0,1]$ is continuously differentiable with $w'\ge k>0$. An assortment is a Borel set $S\subseteq[0,1]$; $\mathcal S$ is the set of all of them. A customer offered $S$ buys a product in a Borel set $A\subseteq S$, or buys nothing ($\emptyset$), with probabilities

$$\mathbb P(X^S\in A)=\frac{\int_A v(x)\,dx}{1+\int_S v(x)\,dx},\qquad \mathbb P(X^S=\emptyset)=\frac{1}{1+\int_S v(x)\,dx},$$

where the preference function $v$ is unknown to the seller. The expected revenue of $S$ is $r(S,v)=\int_S vw\big/(1+\int_S v)$, and $\varrho^*=\max_{S\in\mathcal S}r(S,v)$.

The class $\mathcal V(\underline v,\overline v,D)$ (Assumption 1) contains the integrable $v$ with $\underline v\le v\le\overline v$ on $[0,1]$ that are differentiable on $(0,1)$ with $|v'|\le D$, where $\overline v>\underline v>0$ and $\overline v>w(0)/\int_0^1(w-w(0))$.

The generalized inverse is $w^{-1}(\varrho)=\min\{x\in[0,1]:w(x)\ge\varrho\}$, and $h(\varrho)=r([w^{-1}(\varrho),1],v)$. The policy SAP$(\alpha,\beta)$ starts at $\varrho_1\in[0,1]$, offers $S_t=[w^{-1}(\varrho_t),1]$ in period $t$, observes the revenue $R_t=w(X_t)\mathbf 1\{X_t\in S_t\}$, and updates

$$\varrho_{t+1}=\varrho_t+\frac{\alpha}{t+\beta}\,(R_t-\varrho_t).$$

Given the history, the purchase $X_t$ has the law of $X^{S_t}$. The regret over $T$ periods is $\Delta_\pi(T,v)=\sum_{t=1}^T\mathbb E_\pi[\varrho^*-r(S_t,v)]$.

Formalization targets

Goal: Theorem 1 (p.12)

For $\alpha\ge\overline v+1$ and $\beta\ge\max\{0,\alpha-1\}$ there is $\overline C>0$ such that for all $T\ge2$

$$\sup_{v\in\mathcal V}\Delta_\pi(T,v)\le\overline C\log T.$$

The constant depends on $w$, the class and the policy, but not on $T$ or $v$.

Milestones, in proof order

1. Well-posedness: an SAP purchase process exists for every horizon.
2. §4.1: the optimum over $\mathcal S$ is attained by an interval $[w^{-1}(\varrho),1]$.
3. Lemma 4: $h(\varrho^*)=\varrho^*$; the drift inequality (23) $(\varrho-\varrho^*)(h(\varrho)-\varrho)\le-(\varrho-\varrho^*)^2/(1+\overline v)$; the derivative $g'=(g-w)\xi$ and the curvature bound (27); the quadratic gap (24) $h(\varrho^*)-h(\varrho)\le C(\varrho-\varrho^*)^2$ with $C$ uniform over $\mathcal V$.
4. The iterates stay in $[0,1]$, and $\mathbb E[R_t\mid\text{history}]=h(\varrho_t)$.
5. The recursion (25) $\delta_{t+1}\le\delta_t\big(1-\frac{2}{1+\overline v}\frac{\alpha}{t+\beta}\big)+\frac{\alpha^2}{(t+\beta)^2}$ for $\delta_t=\mathbb E[(\varrho_t-\varrho^*)^2]$, and Lemma 5, $\delta_t\le\kappa/(t+\beta)$.
6. The regret identity $\Delta_\pi(T,v)=\sum_t\mathbb E[h(\varrho^*)-h(\varrho_t)]$ and $\sum_{t=1}^T(t+\beta)^{-1}\le3\log T$.

Significance

The theorem shows that in the continuum logit model the seller does not need to estimate the preference function: a one-dimensional Robbins–Monro recursion on the observed revenue finds the optimal revenue level, and the loss is logarithmic in the horizon. This is faster than the $\sqrt T$ rates typical of continuum-armed bandits, and the paper's Theorem 2 shows it is optimal. The bound is worst-case over a class of preference functions, which matters when nothing is known about the customers beyond the class.

The result is proved on paper. No part of it is formalized on the platform. The mission adds the platform's first continuum-indexed choice model, a measure-theoretic model of a sequential learning policy whose decisions depend on the full purchase history, and a complete regret analysis for a stochastic approximation policy. The discrete MNL bandit of Agrawal et al. is on the platform as MNLBandit.UCB; it is a related, not a reused, model.

Difficulty

The policy itself is three lines; the difficulty is in the analysis of the map $h$. The obvious route — "$h$ is a contraction, so the iterates converge" — fails: $h$ is not a contraction, and $\varrho\mapsto h(\varrho)$ is flat below $w(0)$ and drops to zero above $w(1)$. The proof instead needs the one-sided drift inequality (23), whose constant must use the upper bound $\overline v$, and the quadratic gap (24), which requires a second-order Taylor expansion of $g(y)=r([y,1],v)$ with a curvature bound (27) that is uniform over the class. The bound (27) needs $v$ differentiable, and the uniformity of $C$ and $\kappa$ over $\mathcal V$ is what turns per-instance bounds into a worst-case one.

The induction in the proof of Lemma 5 multiplies by $1-2\alpha/((1+\overline v)(t+\beta))$, which is negative for small $t$ when $\overline v$ is small; the printed $\kappa=\max\{1+\beta,\alpha(1+\overline v)\}$ does not follow from the printed step there, although the lemma's statement (some $\kappa>0$) remains true.

Formalization scope

Products are reals and purchases live in ℝ ⊕ Unit (Sum.inr () is no-purchase). $w,v:\mathbb R\to\mathbb R$ carry hypotheses only on $[0,1]$ and $(0,1)$. $\mathcal S$ is the measurable subsets of $[0,1]$ (the uncapacitated case $c=1$), and $\varrho^*$ is a supremum (sSup), shown to be a maximum in a milestone. The paper's $\min\{x:w(x)\ge\varrho\}$ is empty for $\varrho>w(1)$, which SAP can reach since $\varrho_1\in[0,1]$ is arbitrary; there $w^{-1}(\varrho):=1$, so the offered assortment $\{1\}$ is a null set. Lean's sInf ∅ = 0 would instead offer $[0,1]$ and break (23). The class has a fixed derivative bound $D$, since Assumption 1(ii)'s supremum over all admissible $v$ is otherwise infinite.

Time is 0-based ($n=t-1$). A horizon-$T$ process is a probability space with measurable purchases $X_0,\dots,X_{T-1}$ whose conditional law given the history is the choice law of the offered assortment, written as an identity of measures on history events. A Lean proof that the SAP iterate is a measurable function of the history exists, so the expectations in the regret are genuine integrals. The goal quantifies over all such processes, and a milestone asserts that one exists, so the goal is not vacuous.

A complete development needs: second-order calculus for parameter integrals $y\mapsto\int_y^1$; the construction of a process from a history-dependent kernel (Ionescu–Tulcea, ProbabilityTheory.Kernel.traj, or an iterated Measure.bind); and conditional expectations given a history σ-algebra. The mean-square recursion and the harmonic-sum bound are reusable for other Robbins–Monro analyses. Contributions to any milestone are welcome, in any order; milestones 2–3 and 6 are independent of the process construction.

Selected references

• Y. Peeters, A. V. den Boer, M. Mandjes, Continuous Assortment Optimization with Logit Choice Probabilities under Incomplete Information, arXiv:1807.06497v4, 2021; Operations Research, 2022. https://arxiv.org/abs/1807.06497
• H. Robbins, S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22(3), 1951. https://doi.org/10.1214/aoms/1177729586
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
• M. Broadie, D. Cicek, A. Zeevi, General Bounds and Finite-Time Improvement for the Kiefer-Wolfowitz Stochastic Approximation Algorithm, Operations Research 59(5), 2011. https://doi.org/10.1287/opre.1110.0970
• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://doi.org/10.1287/opre.2018.1832

Motivation

An online experiment has two audiences. The experimenter who cares about welfare wants to stop assigning people to inferior treatments as quickly as possible; the statistician wants an accurate estimate of how much better one treatment is than another. A multi-armed bandit policy serves the first and starves the second: an arm that is played rarely is estimated badly. A randomized controlled trial does the opposite, at the price of regret linear in the sample size. Simchi-Levi and Wang (SSRN 4224969, published in Management Science, 2024) study this trade-off for stochastic bandits and give a design, EXP3EG, whose single parameter $\alpha\in[0,1]$ moves along it. This mission formalizes the finite-sample inference guarantee of that design.

Setting

There are $K\ge2$ arms. Pulling arm $a$ yields a reward with law $P_a$ on $[-1,1]$ and mean $\mu_a$. The treatment effect of arm $i$ against arm $j$ is $\Delta^{(i,j)}=\mu_i-\mu_j$.

EXP3EG (Algorithm 2) takes inputs $\alpha\in[0,1]$ and $\delta$, and sets $C=(4K^2(e^2+1)+2)^2(\log(2/\delta))^2$, $\varepsilon_t=1/\sqrt{Ct}$ and $\alpha_t=1/(Kt^\alpha)$. It keeps an active set $\mathcal A_t$, starting from all arms, and inverse-propensity-weighted cumulative estimates $\hat R_t(a)$, starting from $0$. In round $t$, each arm outside $\mathcal A_t$ gets probability $\pi_t(a)=\alpha_t$ (forced exploration), and the remaining mass $1-|\mathcal A_t^c|\alpha_t$ is split over $\mathcal A_t$ in proportion to $e^{\varepsilon_{t-1}\hat R_{t-1}(a)}$. The arm $A_t\sim\pi_t$ is pulled, the reward $R_t$ is observed, and

$$\hat R_t(a)=\hat R_{t-1}(a)+\frac{R_t}{\pi_t(a)}\mathbb I_{a=A_t},\qquad\mathcal A_{t+1}=\mathcal A_t\setminus\{a:\hat R_t^{\max}-\hat R_t(a)>2\sqrt{Ct}\}.$$

The estimate of the treatment effect is $\hat\Delta_t^{(i,j)}=(\hat R_t(i)-\hat R_t(j))/t$, and its error is $e(n,\hat\Delta^{(i,j)})=\mathbb E|\Delta^{(i,j)}-\hat\Delta_n^{(i,j)}|$.

Formalization targets

Goal: Theorem 7

For every $\alpha\in[0,1]$, $\delta\in(0,2/e)$, instance with rewards in $[-1,1]$, $i\ne j$ and $t\ge1$, with probability at least $1-\delta$,

$$\big|\hat\Delta_t^{(i,j)}-\Delta^{(i,j)}\big|\le\frac{4(2+2K^2(1+e^2))\log(2/\delta)}{\sqrt{t^{1-\alpha}}},$$

and there is $c$ depending only on $K$ such that, with $\delta=1/(2n^2)$,

$$\max_{i<j\le K}e(n,\hat\Delta^{(i,j)})\le\frac c{\sqrt{n^{1-\alpha}}}\quad\text{for all }n\ge1,\ \alpha\in[0,1]\text{ and all instances}.$$

Milestones

In the order the paper's proof uses them: the propensity bound (EC.7); the martingale $\hat R_t(a)-t\mu_a$; unbiasedness of $\hat\Delta_t^{(i,j)}$; the increment bound; the conditional second-moment bound (EC.11); the bound $V_t^{(i,j)}\le(2C'+1)(t+1)^{1+\alpha}$ on the variance proxy, with $C'=K^2(1+e^2)$; the real inequality (EC.12); and Bernstein's inequality for martingales (Theorem EC.1).

Significance

Theorem 7 is the only result of the paper about EXP3EG with explicit constants. Together with the paper's regret bound $\tilde O(n^{1-\alpha})$, it says that one design attains error $O(1/\sqrt{n^{1-\alpha}})$ at every point of the trade-off, for every pair of arms and without a gap assumption. The paper's headline, a characterization of Pareto optimality (Theorem 8), is not the goal here: Pareto optimality there compares quantities only by their order in $n$, ignoring constants and logarithms, so it has no fixed formal content. Theorem 7 is the precise statement underneath it.

The result is proved on paper, not previously formalized. This mission adds a machine-checked model of an adaptive design whose estimators are inverse-propensity weighted, on top of the published BanditAlgorithm canonical bandit model.

Two statements are deliberately not the printed ones. "With probability at least $1-\delta$, for all $t\in[n]$" in Theorem 7, and the same clause in Theorem EC.1, are false as uniform-in-time claims: with $K=2$, $\alpha=0$, $\delta=1/2$ and arms taking values $\pm1$ with means $\pm1/2$, the law of the iterated logarithm for martingales (Stout 1970) makes the bound fail infinitely often almost surely, and for Theorem EC.1 i.i.d. $\pm1$ steps do the same. Both are stated for each fixed $t$. The paper's $O(\cdot)$ clause is pinned as above; it is true, but it does not follow by integrating the high-probability bound, which leaves a factor $\log n$.

Difficulty

The natural martingale has increments of size $1/\pi_t(a)$, and forced exploration makes these grow like $Kt^\alpha$ for eliminated arms. So neither Azuma–Hoeffding with a fixed range nor a fixed-variance Bernstein bound applies directly. The range and the variance both grow with $t$, and they must be controlled along the adaptive run by a deterministic sequence, separately for active and eliminated arms, before any concentration inequality can be invoked. The active-arm bound (EC.7) depends on the interplay of the elimination threshold $2\sqrt{Ct}$ and the learning rate, not on any property of the reward laws.

Formalization scope

The bandit is the published BanditAlgorithm.StochasticBandit K, a policy the published BanditPolicy K, and the law of $n$ rounds the published banditMeasure, the canonical law of the observed history. Only the observed history matters, so the joint law of the rewards of different arms is not modelled. Rewards in $[-1,1]$ are a hypothesis (RewardsBounded), not part of the bandit.

EXP3EG is a deterministic recursion on the observed history in the module BanditExpDesign.EXP3EG: $\hat R_t$ is computed by the update above and is never defined from the means. Conventions: arms are Fin K; rounds are numbered from $1$, and a history of $n$ rounds is a function on Fin n; the logarithm is natural; $t^\alpha$ is Real.rpow; $\varepsilon_0=0$, which is irrelevant since $\hat R_0=0$; and $\hat R_t^{\max}$ is the maximum over the active set. The paper's p.13 writes the maximum over all arms, under which the active set can empty and $\pi_t$ stops being a probability vector; its proofs use the active-set maximum. The module proves that $\mathcal A_t\ne\emptyset$, that $\pi_t>0$ and $\sum_a\pi_t(a)=1$, and that the kernel is measurable.

A trivializing reading is excluded: expectations come with integrability in the statements where the Bochner integral's junk value could otherwise hide the claim.

A complete development needs a martingale concentration library around Theorem EC.1, conditional expectations under banditMeasure, and a one-step disintegration of the law of the history; these are reusable for other adaptive-experiment results. Contributions to any milestone are welcome.

Selected references

• D. Simchi-Levi, C. Wang, Multi-armed Bandit Experimental Design: Online Decision-making and Adaptive Inference, SSRN 4224969. https://ssrn.com/abstract=4224969; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.00492
• D. A. Freedman, On tail probabilities for martingales, Annals of Probability 3(1), 100–118, 1975. https://doi.org/10.1214/aop/1176996452
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 48–77, 2002. https://doi.org/10.1137/S0097539701398375
• W. F. Stout, A martingale analogue of Kolmogorov's law of the iterated logarithm, Zeitschrift für Wahrscheinlichkeitstheorie 15, 279–290, 1970. https://doi.org/10.1007/BF00534922

Why error bounds for conic feasibility

The conic feasibility problem asks for a point of $(\mathcal L+a)\cap\mathcal K$, where $\mathcal K$ is a closed convex cone in a finite dimensional Euclidean space, $\mathcal L$ is a subspace and $a$ is a point. An error bound estimates the distance from a trial point $x$ to that intersection using only the two individual distances $\operatorname{dist}(x,\mathcal K)$ and $\operatorname{dist}(x,\mathcal L+a)$. Such estimates control how far an approximately feasible point is from a truly feasible one, and they enter convergence rate analysis of first-order methods (Liu and Lourenço, arXiv:2008.12968) and the computation of Kurdyka–Łojasiewicz exponents.

The history for one family of cones runs as follows. For the $p$-cones $\mathcal K_p^{n+1}=\{(x_0,\bar x):x_0\ge\|\bar x\|_p\}$, the cases $p=1,\infty$ are polyhedral, so Lipschitzian bounds hold by Hoffman's lemma (1952). For $p=2$ the exponent $\frac12$ follows from the Luo–Sturm analysis of second-order cones. Lourenço (Amenable cones, 2021) introduced facial residual functions and conjectured exponent $\frac1p$ for every $p$-cone. Lindstrom, Lourenço and Pong (2022) extended the framework to non-amenable cones. The paper formalized here, arXiv:2109.11729v4, determines the optimal exponents for all $p\in(1,\infty)$, and they differ from the conjecture.

The setting

Fix a finite dimensional Euclidean space $\mathcal E$. Write $\operatorname{dist}(x,C)=\inf_{y\in C}\|x-y\|$ and $P_C$ for the projection onto $C$. Two closed convex sets $C_1,C_2$ with $C_1\cap C_2\ne\emptyset$ satisfy a uniform Hölderian error bound with exponent $\gamma\in(0,1]$ if for every bounded $B$ there is $\kappa_B>0$ with

$$\operatorname{dist}(x,C_1\cap C_2)\le\kappa_B\max\{\operatorname{dist}(x,C_1),\operatorname{dist}(x,C_2)\}^\gamma\qquad\forall x\in B.$$

The case $\gamma=1$ is Lipschitzian. The partial-polyhedral Slater condition is a constraint qualification under which a Lipschitzian bound holds.

For $z\in\mathcal K^*$, the set $\mathcal F=\mathcal K\cap\{z\}^\perp$ is an exposed face. A one-step facial residual function (1-FRF) $\psi$ bounds $\operatorname{dist}(x,\mathcal F)$ by $\psi(\epsilon,\|x\|)$ whenever $\operatorname{dist}(x,\mathcal K)\le\epsilon$ and $\langle x,z\rangle\le\epsilon$. A consistent error bound function $\Phi$ is a monotone function with $\Phi(0,b)=0$ that bounds $\operatorname{dist}(x,\bigcap_iC_i)$ by $\Phi(\max_i\operatorname{dist}(x,C_i),\|x\|)$; this notion covers Hölderian bounds and more general ones.

For $p,q\in(1,\infty)$ with $\frac1p+\frac1q=1$, the dual of $\mathcal K_p^{n+1}$ is $\mathcal K_q^{n+1}$. For $z=(z_0,\bar z)$ put $J_z=\{i:\bar z_i\ne0\}$ and

$$\alpha_z=\begin{cases}\frac12&|J_z|=n,\\\frac1p&|J_z|=1,\ p<2,\\\min\{\frac12,\frac1p\}&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 4.3

Let $n\ge2$, $p\in(1,\infty)$, $\frac1p+\frac1q=1$, and $(\mathcal L+a)\cap\mathcal K_p^{n+1}\ne\emptyset$. If this intersection is $\{0\}$ or meets $\operatorname{ri}\mathcal K_p^{n+1}$, a Lipschitzian bound holds. Otherwise a vector $z\in\partial\mathcal K_q^{n+1}\cap\mathcal L^\perp\cap\{a\}^\perp$, $z\ne0$, exists, and every such $z$ gives a uniform Hölderian error bound with exponent $\alpha_z\ge\min\{\frac12,\frac1p\}$. Moreover, for every $z\in\partial\mathcal K_q^{n+1}\setminus\{0\}$, every consistent error bound function $\Phi$ for $\mathcal K_p^{n+1},\{z\}^\perp$ and every $\hat\eta>0$,

$$s^{\alpha_z}\le\hat\kappa\,\Phi(\hat\kappa s,\hat\eta)\qquad\forall s\in[0,s_0],$$

for some $\hat\kappa,s_0>0$, and no Hölderian exponent $\hat\alpha\in(\alpha_z,1]$ is possible.

Milestones

• General framework: Proposition 2.1, Lemma 2.3, Lemma 2.5, Theorem 2.2, Theorem 3.1, Theorem 3.2, Corollary 3.1. These hold for any closed convex cone.
• The $p$-cone: the basic facts of §4, the exposing vector of the proof of Theorem 4.3, the face formula (4.5), Lemma 4.1, Theorem 4.1, Lemmas 4.2 and 4.3, Theorem 4.2.

What the result gives

The theorem gives the sharp behaviour of feasibility residuals over every $p$-cone with no constraint qualification. In the source it yields Kurdyka–Łojasiewicz exponents for $p$-norm regularized least squares, and a short proof that most $p$-cones are neither self-dual nor homogeneous. The optimality statement is stronger than a claim about exponents, since it compares against all consistent error bound functions.

The paper's result is proved, and a search of the platform found no machine-checked proof of it. This mission states the results at full strength. The formal work is the proof of these statements, and a library of error bounds for sets. The platform currently has Hoffman's theorem as a proved result, and nothing on facial residual functions.

Where the difficulty lies

Without a constraint qualification, the first natural step, estimating $\operatorname{dist}(x,(\mathcal L+a)\cap\mathcal K)$ by a compactness argument, gives no rate: the constant degenerates exactly near the face where $\mathcal L+a$ touches $\mathcal K$. The obvious guess, one exponent $\frac1p$ for all faces, fails because the local shape of $\partial\mathcal K_p^{n+1}$ near an extreme ray depends on the zero pattern of the exposing vector. Near a nonzero entry of the ray the boundary has order two, and near a zero entry it has order $p$. The two directions then have to be combined along every possible approach to the face, and the matching lower bound needs an explicit curve for each case, and the list of cases differs between $n=2$ and $n\ge3$.

Formalization scope

$\mathbb R^{n+1}$ is EuclideanSpace ℝ (Fin (n + 1)), with $x_0$ = x 0 and $\bar x_i$ = x i.succ. The $p$-norm is an explicit sum of real powers. Distances are Metric.infDist on nonempty sets, the dual cone is ProperCone.innerDual, $\operatorname{ri}$ is intrinsicInterior ℝ, and $\partial$ is frontier, the topological boundary, also for lower-dimensional cones. Projections are the predicate IsProj. The quantity $\gamma_{z,\eta}$ lies in ENNReal, with the empty infimum equal to $+\infty$. Functions on $\mathbb R_+$ are functions on ℝ with their conditions on Set.Ici 0. Definition 2.1 keeps "for every bounded $B$ there is $\kappa_B$" in that order: a single global constant would be a different, false claim for $\alpha_z<1$. The optimality clause quantifies over consistent functions, which exist, so it is not vacuous.

A complete development needs: projections onto cones and hyperplanes, the Bauschke–Borwein–Li bound for Proposition 2.1 (the polyhedral case can use Hoffman's theorem, already proved on the platform), Hölder equality analysis, and separation for the exposing vector. The general framework is reusable for other cones, and contributions to it are welcome separately from the $p$-cone part. Theorem 4.4 and the applications of §5 are out of scope.

Selected references

• S. B. Lindstrom, B. F. Lourenço, T. K. Pong, Optimal error bounds in the absence of constraint qualifications with applications to the p-cones and beyond, arXiv:2109.11729v4, 2024. https://arxiv.org/abs/2109.11729
• S. B. Lindstrom, B. F. Lourenço, T. K. Pong, Error bounds, facial residual functions and applications to the exponential cone, Mathematical Programming 200, 2022. https://doi.org/10.1007/s10107-022-01883-8
• B. F. Lourenço, Amenable cones: error bounds without constraint qualifications, Mathematical Programming 186, 2021. https://doi.org/10.1007/s10107-019-01439-3
• T. Liu, B. F. Lourenço, Convergence analysis under consistent error bounds, arXiv:2008.12968. https://arxiv.org/abs/2008.12968
• B. F. Lourenço, M. Muramatsu, T. Tsuchiya, Facial reduction and partial polyhedrality, SIAM Journal on Optimization 28(3), 2018. https://doi.org/10.1137/15M1051634
• H. H. Bauschke, J. M. Borwein, W. Li, Strong conical hull intersection property, bounded linear regularity, Jameson's property (G), and error bounds in convex optimization, Mathematical Programming 86(1), 1999. https://doi.org/10.1007/s101070050083

Motivation

Dynamic programs in operations research and economics are routinely used to ask comparative statics questions: when a parameter of the model increases, does the optimal decision increase? For Markov decision processes the classical answer, going back to Topkis (1978) and his book Supermodularity and Complementarity (1998, cited by the paper as Topkis (2011)), concerns the policy function $g(s)$, the decision taken in a given state. In a stochastic model the decision maker's future states are random, so the decision in a future period is a random variable from the point of view of period 1. Light (2021) asks the stochastic version of the question: does the expected decision in every future period increase with the parameter? The same quantity is the aggregate decision of a continuum of agents facing idiosyncratic shocks, which is the object of interest in stationary equilibrium and mean field models.

Timeline. Monotone optimal policies in Markov decision processes via increasing differences: Topkis (1978); Lovejoy (1987) and Hopenhayn and Prescott (1992) prove that the maximum over an ascending feasible set preserves increasing differences and use it for stochastic monotonicity of dynamic economies. Comparison of Markov chains in integral stochastic orders: Müller and Stoyan (2002, Chapter 5). Light (arXiv 2019, Mathematics of Operations Research 2021) combines the two to derive comparative statics of expected future decisions from the primitives of the model, including the first general result that the policy increases with the discount factor.

Setting

A discounted dynamic program is a tuple $(S,A,\Gamma,p,r,\beta)$. The state space $S$ is a measurable space with a partial order $\le$. The action space is $A\subseteq\mathbb R$, and $\Gamma(s)\subseteq A$ is the non-empty set of feasible actions in state $s$. The transition probability $p(s,a,\cdot)$ is the law of the next state, $r(s,a)$ is the single-period payoff, and $0<\beta<1$ is the discount factor. For $f:S\to\mathbb R$,

$$h(s,a,f)=r(s,a)+\beta\int_S f(s')\,p(s,a,ds'),\qquad Tf(s)=\max_{a\in\Gamma(s)}h(s,a,f).$$

The value function $V$ satisfies $TV=V$ and is the uniform limit of the iterates $T^n0$. The optimal policy correspondence is $G(s)=\{a\in\Gamma(s):V(s)=h(s,a,V)\}$ and the policy function is $g(s)=\max G(s)$.

Starting from $s(1)$ and following $g$, the state of period $t$ has law $\mu^t$: $\mu^1=\delta_{s(1)}$ and $\mu^{t+1}(B)=\int_S p(s,g(s),B)\,\mu^t(ds)$. The expected decision in period $t$ is $\mathbb E^t(g)=\int_S g\,d\mu^t$.

A function $f(x,e)$ has increasing differences if $f(x_2,e_2)-f(x_2,e_1)\ge f(x_1,e_2)-f(x_1,e_1)$ whenever $x_1\le x_2$ and $e_1\preceq e_2$. The transition $p$ is monotone if $\int f\,dp(s,a,\cdot)$ is increasing in $(s,a)$ for every increasing $f$, and has stochastically increasing differences if $p(s,a,B)$ has increasing differences for every upper set $B$. A correspondence $\Gamma$ is ascending if $s_1\le s_2$, $b\in\Gamma(s_1)$, $b'\in\Gamma(s_2)$ imply $\min\{b,b'\}\in\Gamma(s_1)$ and $\max\{b,b'\}\in\Gamma(s_2)$. Assumption 1 asks that $r$ be increasing in $s$ with increasing differences in $(s,a)$, that $p$ be monotone with stochastically increasing differences, and that $\Gamma(s_1)\subseteq\Gamma(s_2)$ for $s_1\le s_2$.

Formalization targets

Goal: Theorem 3

Under Assumption 1 with $\Gamma$ ascending:

1. for $0<\beta_1\le\beta_2<1$,

$$g(s,\beta_2)\ge g(s,\beta_1)\ \ \forall s,\qquad \mathbb E^t_2(g(\beta_2))\ge\mathbb E^t_1(g(\beta_1))\ \ \forall t\in\mathbb N,\ \forall s(1);$$

2. for a payoff $r(s,a,c)$ with increasing differences in $(a,c)$ and in $(s,c)$ and $c_2\succeq c_1$,

$$g(s,c_2)\ge g(s,c_1)\ \ \forall s,\qquad \mathbb E^t_2(g(c_2))\ge\mathbb E^t_1(g(c_1))\ \ \forall t\in\mathbb N,\ \forall s(1).$$

Milestones

• Theorem 1: if $P_2$ is $D$-preserving and $P_2(s,\cdot)\succeq_D P_1(s,\cdot)$ for all $s$, then $\mu_2^t\succeq_D\mu_1^t$ for all $t$.
• Corollary 1: if $g_1\le g_2$, $g_2$ is increasing and $p$ is monotone, then $\mathbb E^t_2(g_2)\ge\mathbb E^t_1(g_1)$ for all $t$ and every initial state.
• Proposition 5: $h(\cdot,\cdot,f)$ has increasing differences for increasing $f$; with $\Gamma$ ascending, $G$ is ascending and $g$ increasing; $Tf$ and $V$ are increasing.
• Proposition 6: the maximum over an ascending $\Gamma$ of a function with pairwise increasing differences in $(s,a)$, $(s,e)$, $(a,e)$ has increasing differences in $(s,e)$.
• Proof of Theorem 3, p.21: $h(s,a,\beta,f)$ has increasing differences in $(a,\beta)$ and $(s,\beta)$.
• Proof of Theorem 3, pp.21–22: $V(s,\beta)$ has increasing differences in $(s,\beta)$ and is increasing in $s$.

Significance

The theorem gives sign predictions for the whole future path of decisions, not only for the current one: a more patient decision maker, or one whose payoff rewards higher actions more, invests, saves or prices higher now and in expectation in every later period. In aggregate models this is the comparative statics of the cross-sectional mean decision, which the applications of the paper (capital accumulation with adjustment costs, reference-price dynamic pricing, controlled random walks) use directly.

The result is proved in the paper; nothing here is open mathematics. The paper's proofs of Propositions 5 and 6 are citations, and the proof of part (ii) of Theorem 3 is omitted. As far as is known, none of these statements has a machine-checked proof. The platform has Topkis's finite-horizon monotonicity theorem and the argmax monotonicity theorem in published form; this mission adds the infinite-horizon fixed-point argument and the Markov-chain comparison.

Difficulty

The first idea, applying Topkis's monotonicity theorem to $h(s,a,\beta,V)$ in $(a,\beta)$, needs increasing differences of $V$ in $(s,\beta)$, and $V$ is only known as a fixed point. Increasing differences must be carried through every value iterate, which needs Proposition 6, and that needs $\Gamma$ ascending; Assumption 1(iii) alone does not suffice (Proposition 5(ii) as printed fails without it, see the milestone). The stochastic part has its own obstacle: the policy comparison $g_1\le g_2$ alone does not order the future state distributions, because the distributions are generated by different policies; the comparison needs $g_2$ increasing and $p$ monotone so that the transition under $g_2$ preserves increasing functions, and then an induction over periods with unbounded integrands.

Formalization scope

The state space is any measurable space with a partial order; the paper's Borel $S\subseteq\mathbb R^n$ with the componentwise order is an instance. Actions are reals in $A$, and $p$ is a Markov kernel on $S\times\mathbb R$; hypotheses on $p$ and $r$ are imposed for $a\in A$. The maximum in $T$ is sSup with its attainment assumed explicitly, since sSup of an unbounded set is $0$ in Lean. The standing assumptions of p.6 are hypotheses: $T^n0\to V$ uniformly, $V=TV$ with the maximum attained, attainment along the iterates, and measurability and integrability of the iterates and of $V$ (footnote 9). The policy $g$ is the greatest element of $G(s)$ and measurable, and the Lean period index starts at $0$. Integrals are Bochner integrals, so every integrand carries its integrability hypothesis; without them the comparison of expected decisions could hold for the trivial reason that both integrals are $0$. Proposition 5(ii) carries the added hypothesis "$\Gamma$ ascending".

Increasing differences and the induced set order are the published definitions Supermodularity.Monotonicity.IncreasingDifferencesOn and Supermodularity.Lattices.InducedSetOrder. A complete development needs the layer-cake formula for integrals of increasing functions against measures with stochastically increasing differences, integration against Measure.bind, monotone and dominated convergence for truncations of unbounded increasing functions, and uniform limits of functions with increasing differences. The chain comparison (Theorem 1) and Proposition 6 are reusable for other monotone dynamic programs. Proofs of any milestone, and alternative proofs of Theorem 3(ii), are welcome.

Selected references

• Bar Light, Stochastic Comparative Statics in Markov Decision Processes, arXiv:1904.05481v2, 2020; Mathematics of Operations Research 46(2), 2021. https://arxiv.org/abs/1904.05481
• Donald M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 1978. https://doi.org/10.1287/opre.26.2.305
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998 (paperback 2011). https://doi.org/10.1515/9781400822539
• William S. Lovejoy, Ordered Solutions for Dynamic Programs, Mathematics of Operations Research 12(2), 1987. https://doi.org/10.1287/moor.12.2.269
• Hugo A. Hopenhayn and Edward C. Prescott, Stochastic Monotonicity and Stationary Distributions for Dynamic Economies, Econometrica 60(6), 1992. https://doi.org/10.2307/2951541
• Alfred Müller and Dietrich Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002, ISBN 978-0-471-49446-1.

Motivation

Sequential experiments choose which treatment to try next from the outcomes seen so far. Multi-armed bandit algorithms such as Thompson sampling, tempered greedy rules and Luce's rule are the standard examples, and they are used in clinical trials, online platforms and adaptive A/B testing. Their behaviour is usually studied either in the large-signal regime, where arms are well separated and regret grows like $\log n$ (Lai and Robbins, Asymptotically efficient adaptive allocation rules, 1985), or by worst-case minimax bounds. Neither describes the regime that matters most in practice: arm differences of the order of the statistical noise, $1/\sqrt n$ after $n$ samples.

Kuang and Wager (Weak signal asymptotics for sequentially randomized experiments, arXiv:2101.09855v7, 2023; Management Science, 2024) study this weak signal regime. Their first main result, Theorem 1, shows that in this regime the whole sample path of a broad class of experiments converges to the solution of a stochastic differential equation. The paper then uses this limit to compare algorithms: Lipschitz experiments have regret bounded away from zero for large signals (Theorem 7), while undersmoothed Thompson sampling does not (Theorem 9). Fan and Glynn (arXiv:2105.09232, 2021) independently obtained related limits.

Setting

There are $K$ arms. In the $n$-th problem, pulling arm $k$ returns a reward drawn from a distribution $P^n_k$ on $\mathbb R$ with mean $\mu^n_k$ and variance $(\sigma^n_k)^2$. At periods $i=1,\dots,n$ an agent chooses an arm $A_i$ and observes the reward $Y_i$. The state after $i$ periods is the vector of pull counts and cumulative rewards,

$$Q_{k,i}=\sum_{j\le i}\mathbf 1\{A_j=k\},\qquad S_{k,i}=\sum_{j\le i}\mathbf 1\{A_j=k\}\,Y_j,\qquad Q_{k,0}=S_{k,0}=0.$$

• Sequentially randomized Markov experiment. A measurable sampling function $\psi^n:\mathbb R^K\times\mathbb R^K\to\Delta^K$ (the unit simplex) chooses $A_i$ with probabilities $\psi^n(Q_{i-1},S_{i-1})$; conditionally on $A_i$, the reward $Y_i$ is drawn from $P^n_{A_i}$ independently of the past.
• Weak signal regime. $\sqrt n\,\mu^n_k\to\mu_k$ and $(\sigma^n_k)^2\to\sigma_k^2$.
• Scaling. $Q^n_{k,i}=Q_{k,i}/n$ and $S^n_{k,i}=S_{k,i}/\sqrt n$. The process $(\bar Q^n_t,\bar S^n_t)_{t\in[0,1]}$ interpolates them linearly between the times $i/n$, so it is a random element of $\mathcal C=C([0,1],\mathbb R^{2K})$ with the uniform metric.
• Convergent sampling functions. $\bar\psi^n(q,s)=\psi^n(nq,\sqrt n\,s)$ converges to a limit $\psi$ uniformly on compact subsets of $D=[0,1]^K\times\mathbb R^K$.
• The limit diffusion (3.1).

$$dQ_{k,t}=\psi_k(Q_t,S_t)\,dt,\qquad dS_{k,t}=\mu_k\psi_k(Q_t,S_t)\,dt+\sigma_k\sqrt{\psi_k(Q_t,S_t)}\,dB_{k,t},\qquad (Q_0,S_0)=0.$$

In the Lean development the state space is State K, the Euclidean space on Fin K ⊕ Fin K (Sum.inl k is $q_k$, Sum.inr k is $s_k$). The experiment is IsSRMExperiment, the path is banditPath, the regime and convergence conditions are IsWeakSignal, HasBoundedFourthMoments and IsConvergentSampling, and the laws of solutions of (3.1) are IsDiffusionLaw (limitDiff σ ψ) (limitDrift μ ψ) 0.

Formalization targets

Goal: Theorem 1 (pp.12–13)

Let $\mu\in\mathbb R^K$ and $\sigma\in\mathbb R^K_+$. Assume the rewards are in the weak signal regime with uniformly bounded fourth moments, the sampling functions are convergent, the limit $\psi$ is Lipschitz on $D$, and (3.1) is unique in law from $0$. Then (3.1) has a unique solution law $P$ on $\mathcal C$, and for every realization of the experiments

$$(\bar Q^n,\bar S^n)\Rightarrow P\ \text{ in }\mathcal C,\qquad \lim_{n\to\infty}\mathbb E\,f(\bar Q^n_t,\bar S^n_t)=\mathbb E_P\,f(Q_t,S_t)\quad(t\in[0,1],\ f\in C_b(\mathbb R^{2K})).$$

The goal leaves $K$, $\mu$, $\sigma$, the reward laws and the sampling rule unrestricted beyond these hypotheses. All three clauses (unique limit, weak convergence of paths, convergence of marginals) are part of it.

The uniqueness hypothesis is a correction. As printed, with $\psi$ Lipschitz alone, the theorem is false. For $K=2$, $\mu=0$, $\sigma=(1,1)$ and $\psi_1(q,s)=\min(1,|q_1|+|s_1|)$, $\psi_2=1-\psi_1$, equation (3.1) has two solution laws from $0$: one that never pulls arm 1, and one with $Q_1=X$, where $X$ solves $X'=\psi_1(X,W_X)$, $X_t>0$ for $t>0$, and $W$ is a Brownian motion. The docstring of theorem_1 gives the details. The conclusion of the theorem implies the added hypothesis, so nothing weaker repairs it, and the hypothesis holds for instance when every $\sqrt{\psi_k}$ is Lipschitz on $D$.

Milestones

1. Theorem 11 (p.32). The Stroock–Varadhan diffusion approximation: if the truncated drift and covariance of $K^n=n\Pi^n$ converge locally uniformly to bounded Lipschitz $b$ and $a$, long jumps vanish, and the limit equation is unique in law (a correction: the printed theorem omits this, and it is false without it), the interpolated chains converge weakly in $\mathcal C$ to the unique solution of $dZ=b\,dt+\eta\,dB$, $\eta\eta^\top=a$.
2. Lemma 12 (p.33). Convergence of $p$-th moments ($p\ge2$) and of the untruncated characteristics implies the truncated conditions of Theorem 11.
3. (A.14) (p.33). The scaled bandit state is a Markov chain with kernel $\Pi^n((q,s),(q+e_k/n,\,s+e_k\,ds/\sqrt n))=\bar\psi^n_k(q,s)P^n_k(ds)$.
4. (A.18) (p.33). $\sup_z m^n_4(z)\to0$.
5. (A.19)–(A.20) (p.34). $\tilde b^n\to b=(\psi_k,\ \psi_k\mu_k)$ uniformly on compact subsets of $D$.
6. (A.21)–(A.25) (pp.34–35). $\tilde a^n\to a=\operatorname{diag}_{I_S}(\psi_k\sigma_k^2)$ uniformly on compact subsets of $D$.
7. Closing step (p.35). Weak convergence in $\mathcal C$ implies convergence of the time-$t$ marginals.

Significance

Theorem 1 turns questions about finite-sample adaptive experiments into questions about one SDE. Regret, the distribution of pull counts, and the behaviour of estimators computed from adaptively collected data all become functionals of $(Q_t,S_t)$. The paper's lower bound for Lipschitz experiments (Theorem 7) and its analysis of Thompson sampling (Theorems 9 and 10) are statements about this limit, and Corollary 2 gives the $\sqrt n$ scaling of expected regret. Theorem 3 rewrites the limit as a random time change of Brownian motion; it is derived from Theorem 1.

The result is proved in the paper, with the convergence argument delegated to the Stroock–Varadhan theory. No machine-checked version exists. This mission produces a formal statement of the model and the limit, and a decomposition of the proof into its computational part (moments of the kernel (A.14)) and its probabilistic part (Theorem 11). Theorem 11 is a general diffusion-approximation theorem and is reusable well beyond bandits, for queueing heavy-traffic limits and MCMC scaling limits.

Difficulty

The kernel computations (A.18)–(A.25) are elementary. The difficulty lies in Theorem 11 and in the uniqueness of the limit. Proving Theorem 11 requires tightness of the interpolated chains in $\mathcal C$ and identification of every limit point as a solution of the martingale problem; uniqueness of that solution is a hypothesis of the corrected statement. Mathlib has weak convergence of measures and Prokhorov-type tools, but no Itô integral, no martingale-problem theory and no tightness criteria in $\mathcal C$.

Uniqueness is where the paper's argument breaks. The diffusion coefficient $\sigma_k\sqrt{\psi_k}$ need not be Lipschitz when $\psi$ is, because $\psi_k$ may vanish, and the paper's reference, Karatzas and Shreve, assumes Lipschitz dispersion coefficients. The counterexample above shows that the gap is real, so the goal and Theorem 11 assume uniqueness in law.

A second gap is the domain. The bandit's characteristics are only controlled on $D=[0,1]^K\times\mathbb R^K$, where $\psi$ lives. Theorem 11 asks for convergence on whole balls of $\mathbb R^{2K}$, so connecting the milestones needs an extension or localization argument.

Formalization scope

• Representation. $\mathbb R^{2K}$ is EuclideanSpace ℝ (Fin K ⊕ Fin K). Paths are C(unitInterval, ·) with the Borel σ-algebra. Arms are Fin K, and Lean period $i$ is the paper's period $i+1$.
• SDE. (3.1) and (A.10) are encoded by their martingale problems on $[0,1]$. The test functions are all smooth compactly supported $f$, and the martingale property is checked against finite products of bounded measurable functions of past values. "Unique solution" means uniqueness in law, which the goal and Theorem 11 assume as a declared correction of the page.
• Experiments. Definitions 1–2 are encoded by two conditional laws: the law of $A_i$ given the history, and the law of $Y_i$ given the history and $A_i$. They are imposed for periods $1,\dots,n$, and the theorem quantifies over every probability space that carries them.
• Limit sampling function. $\psi$ is only constrained on $D$, and the coefficients of (3.1) read $\psi$ at the projection onto $D$.
• Weak convergence. Convergence of $\int F$ for every bounded continuous $F$ on $\mathcal C$. The verification file proves that the interpolated path is measurable.
• Trivializations ruled out. The verification file proves that the experiment predicate is satisfiable and that a solution of the martingale problem exists in a one-armed case. It also proves that the zero path is not a solution, and that the generator has the drift of (3.1).

Contributions are welcome on Theorem 11 (tightness and identification of limits), on sufficient conditions for uniqueness in law of (3.1), and on the kernel computations (A.18)–(A.25), which are self-contained.

Selected references

• X. Kuang, S. Wager, Weak signal asymptotics for sequentially randomized experiments, arXiv:2101.09855v7, 2023; Management Science, 2024. https://arxiv.org/abs/2101.09855v7
• D. W. Stroock, S. R. S. Varadhan, Multidimensional Diffusion Processes, Springer, 2007 (reprint of 1979). https://doi.org/10.1007/3-540-28999-2
• R. Durrett, Stochastic Calculus: A Practical Introduction, CRC Press, 1996. https://doi.org/10.1201/9780203738283
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• L. Fan, P. W. Glynn, Diffusion approximations for Thompson sampling, arXiv:2105.09232, 2021. https://arxiv.org/abs/2105.09232

Motivation

Offline reinforcement learning asks for a good policy in a Markov decision process using only logged transitions, without further interaction. A common family of methods (fitted $Q$-iteration, Bellman residual minimization) first estimates the optimal action-value function $Q^*$ by some $\hat f$ and then acts greedily with respect to $\hat f$. Standard analyses bound the regret of the greedy policy by a multiple of the estimation error, which gives regret of order $1/\sqrt n$ from $n$ samples. Empirically the regret of such methods often decays much faster, for instance like $1/n$ in linear MDPs.

Hu, Kallus and Uehara (arXiv:2102.00479v2, later published in Mathematics of Operations Research, 2025) explain this by a margin condition, borrowed from classification (Audibert and Tsybakov, 2007) and contextual bandits: if few states have a small but positive gap between the best and second-best action values, then the regret of the greedy policy is the estimation rate raised to a power larger than one.

Setting

A discounted MDP has a measurable state space $\mathcal S$, a finite nonempty action set $\mathcal A$, a transition kernel $P_s(\cdot\mid s,a)$, a reward distribution $P_r(\cdot\mid s,a)$ with mean $r(s,a)$, an initial distribution $\mu$ and a discount factor $0<\gamma<1$. A policy is a Markov kernel $\pi(a\mid s)$; a deterministic policy is a measurable map $\pi:\mathcal S\to\mathcal A$. For a policy $\pi$,

$$Q^\pi(s,a)=\mathbb E^\pi\Big[\sum_{t\ge0}\gamma^tr(s_t,a_t)\,\Big|\,s_0=s,a_0=a\Big],\qquad V^\pi(s)=\mathbb E_{a\sim\pi(\cdot\mid s)}Q^\pi(s,a),\qquad V^\pi=\mathbb E_{s_0\sim\mu}V^\pi(s_0),$$

and the average state occupancy is $d^\pi=(1-\gamma)\sum_{t\ge0}\gamma^t\,\mathbb P^\pi(s_t\in\cdot)$. The optimal quantities are $Q^*(s,a)=\sup_\pi Q^\pi(s,a)$ and $V^*=\sup_\pi V^\pi$, and $\pi^*$ denotes any deterministic policy with $\pi^*(s)\in\arg\max_aQ^*(s,a)$. A policy $\pi_f$ is greedy for $f$ if $\pi_f(s)\in\arg\max_af(s,a)$, with any tie-breaking.

The margin at $s$ is $\Delta(s)=\max_aQ^*(s,a)-\max_{a\notin\arg\max Q^*(s,\cdot)}Q^*(s,a)$, and $\Delta(s)=0$ when every action is optimal. For a class $\Pi$ of deterministic policies:

• Condition 1 (margin). $\delta_0>0$, $\alpha\in[0,\infty]$, and $\sup_{\pi\in\Pi}\mathbb P_{s\sim d^\pi}(0<\Delta(s)\le\delta)\le(\delta/\delta_0)^\alpha$ for all $\delta>0$, where $x^\infty$ is $0$, $1$, $\infty$ for $x<1$, $x=1$, $x>1$.
• Condition 2 (uniform error bound, corrected). The data is a probability space $(\Omega,\mathbb P_{\mathcal D})$, $C>0$, $a_n>0$, and for every $\delta\ge a_n$ there is an event $E$ with $\mathbb P_{\mathcal D}(E)\le C\exp(-\delta^2/a_n^2)$ off which $|\hat f(s,a)-Q^*(s,a)|<\delta$ for every $\pi\in\Pi$, $d^\pi$-almost every $s$ and every action $a$.

Formalization targets

Goal: Theorem 1 (corrected)

Let $\hat\pi=\pi_{\hat f}$ lie in $\Pi$ almost surely, assume Conditions 1 and 2 and $\|Q^*\|_\infty\le Q_{\max}$, fix $\delta_1\ge\delta_0$ with $\delta_1>2a_n$, and let $i_{\max}$ be the largest integer with $2^{i_{\max}+1}a_n<\delta_1$. Then

$$\mathbb E_{\mathcal D}\big[V^*-V^{\hat\pi}\big]\le\frac{2^{\alpha+1}}{(1-\gamma)\delta_0^{\alpha}}\Big(1+C\sum_{i=1}^{i_{\max}}e^{-2^{2i-2}}2^{(\alpha+1)i+1}\Big)a_n^{\alpha+1}+\frac{2Q_{\max}C}{1-\gamma}e^{-\delta_1^2/(4a_n)^2}.$$

The statement keeps the printed constants and every $\alpha\in[0,\infty]$. Because the printed expression is undefined at $\alpha=\infty$, the Lean statement writes the first term in the equivalent factored form $2a_n(2a_n/\delta_0)^\alpha+\sum_iCe^{-2^{2i-2}}2^{i+2}a_n(2^{i+1}a_n/\delta_0)^\alpha$, with the $x^\infty$ convention.

Milestones

In the order of the proof (pp.16–18):

1. the existence of a measurable $Q^*$-greedy $\pi^*$, and $V^*=V^{\pi^*}$, $Q^*=Q^{\pi^*}$ (p.3);
2. the performance difference identity $(1-\gamma)(V^*-V^{\pi})=\mathbb E_{d^{\pi}}[Q^*(s,\pi^*(s))-Q^*(s,\pi(s))]$ (Eq. (4));
3. the peeling of this gap into the shells $B_0$, $B_i$ ($1\le i\le i_{\max}$) and $B'$ (Eq. (5), with $2Q_{\max}$);
4. the bounds on the three kinds of shell: by the margin alone for $B_0$, by a pointwise indicator inequality plus Conditions 1 and 2 for $B_i$, and by Condition 2 for $B'$.

Significance

With $a_n=n^{-1/2}$, the rate that the paper proves for linear fitted $Q$-iteration, the regret is $O(n^{-(1+\alpha)/2})$. Continuous state spaces typically give $\alpha=1$ and regret $O(1/n)$; tabular MDPs give $\alpha=\infty$ and exponentially small regret. The theorem separates estimation from decision making: any estimator with a uniform sub-Gaussian error bound inherits the fast rate.

The printed theorem is false. Its Condition 2 bounds the error at each state-action pair separately, but the greedy policy depends on the data and can steer its occupancy measure to exactly the states where this dataset erred. A root state with many actions leading to leaves whose estimates err independently satisfies every printed hypothesis, yet its regret stays above $1-1/e$ while the printed bound tends to $0$. The mission states the theorem under the uniform error event above, which is the weakest form the paper's proof uses. It follows from the uniform-convergence bound the paper itself proves for linear fitted $Q$-iteration (Theorem 8), so the paper's applications are unaffected. A second, smaller slip is corrected in Eq. (5): the gap on $B'$ is bounded by $2Q_{\max}$, not $Q_{\max}$. The goal keeps the printed constant $2Q_{\max}C/(1-\gamma)$ because, under the uniform event, the mass of $B'$ is at most $C$ times the exponential instead of the printed $2C$.

No part of this argument has, as far as a search of the platform shows, a machine-checked proof. The performance difference lemma is formalized there only for finite MDPs.

Difficulty

The algebra of the shells is elementary. The work is in the measure theory of MDPs on a general state space:

• Bellman optimality for suprema over stochastic Markov policies, the measurability of $Q^*$, and the existence of a measurable greedy selector;
• the performance difference lemma for occupancy measures defined as series of iterated kernels.

The step that fails in the paper's own argument is moving the probability over the data inside the expectation over $d^{\hat\pi}$, as if $\hat\pi$ did not depend on the data. Any proof must use the uniform event to avoid this exchange.

Formalization scope

The MDP is the published structure OffPolicyDRL.CrossFit.MDP (a transition kernel and a reward kernel), with its $Q^\pi$, $V^\pi(s)$ and occupancy measure discVisitation. Its bundled IsBounded and policyValue are not used. The kernels are Markov and the mean reward is bounded; the paper's $\|Q^*\|_\infty\le Q_{\max}$ forces the latter.

Further conventions:

• $Q^*$, $V^*$ are suprema over Markov kernels.
• Deterministic policies are measurable maps used as Dirac kernels.
• The data is an arbitrary probability space, and nothing about the sampling scheme is assumed.
• $\mathbb E_{\mathcal D}$ is a lower Lebesgue integral valued in $[0,\infty]$.
• $i_{\max}$ is encoded by $2^{i_{\max}+1}a_n<\delta_1\le2^{i_{\max}+2}a_n$.

Taking $Q^*$ as a free function, the occupancy measure without its normalization, or only $2^{i_{\max}+1}a_n<\delta_1$ for $i_{\max}$ would trivialize or falsify the statement. The definitions rule all three out.

Contributions are welcome on all milestones. The general-state Bellman optimality and performance difference results are reusable for any discounted MDP mission built on the same structure.

Selected references

• Y. Hu, N. Kallus, M. Uehara, Fast Rates for the Regret of Offline Reinforcement Learning, arXiv:2102.00479v2, 2023; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2102.00479
• A. Agarwal, N. Jiang, S. M. Kakade, W. Sun, Reinforcement Learning: Theory and Algorithms, 2020 (performance difference lemma, Lemma 1.16). https://rltheorybook.github.io/
• J.-Y. Audibert, A. B. Tsybakov, Fast learning rates for plug-in classifiers, Annals of Statistics 35(2), 2007. https://doi.org/10.1214/009053606000001217
• D. Ernst, P. Geurts, L. Wehenkel, Tree-based batch mode reinforcement learning, JMLR 6, 2005 (fitted $Q$-iteration). https://www.jmlr.org/papers/v6/ernst05a.html