Machine Learning

Motivation

Reinforcement learning with large or continuous state spaces relies on function approximation: value functions are represented as functions of a $d$-dimensional feature map instead of tables indexed by states. Before 2019, regret guarantees for exploration with function approximation either needed strong assumptions (deterministic dynamics, a generative model) or applied only to tabular problems. Jin, Yang, Wang and Jordan (arXiv:1907.05388, COLT 2020) showed that in a linear MDP, where transitions and rewards are linear in known features, an optimistic version of least-squares value iteration, LSVI-UCB, has regret $\tilde O(\sqrt{d^3H^3T})$, with no dependence on the number of states or actions (Theorem 3.1).

Exact linearity is rarely satisfied by features chosen in practice. A guarantee that collapses under a small modelling error would say little about real use, and a naive adaptation of linear-bandit methods can break down entirely when the model is wrong. Theorem 3.2 of the same paper addresses this: if the MDP is only $\zeta$-approximately linear, LSVI-UCB with an episode-dependent bonus still has sublinear regret plus an additive term linear in $\zeta T$. This mission formalizes that result. A companion mission formalizes Theorem 3.1.

Setting

An episodic MDP has a measurable state space $\mathcal S$, a finite action set $\mathcal A$, a horizon $H$, and for each step $h\in[H]$ a transition kernel $\mathbb P_h(\cdot\mid x,a)$ and a reward $r_h:\mathcal S\times\mathcal A\to[0,1]$. A policy $\pi$ chooses an action $\pi(x,h)$ at state $x$ and step $h$. Its value functions satisfy the Bellman equation

$$Q^\pi_h(x,a)=r_h(x,a)+\int V^\pi_{h+1}\,\mathrm d\mathbb P_h(\cdot\mid x,a),\qquad V^\pi_h(x)=Q^\pi_h(x,\pi(x,h)),\qquad V^\pi_{H+1}=0,$$

and $V^\star_h(x)=\max_aQ^\star_h(x,a)$ is the optimal value, with $Q^\star$ defined by the same recursion.

A feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ with $\|\phi\|\le1$ makes the MDP $\zeta$-approximately linear (Assumption B) if for every step $h$ there are signed measures $\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ on $\mathcal S$ and a vector $\theta_h$ with

$$\big\|\mathbb P_h(\cdot\mid x,a)-\langle\phi(x,a),\mu_h(\cdot)\rangle\big\|_{\mathrm{TV}}\le\zeta,\qquad|r_h(x,a)-\langle\phi(x,a),\theta_h\rangle|\le\zeta$$

for all $(x,a)$, together with the normalization $\|\theta_h\|\le\sqrt d$ and a $\sqrt d$ bound on the masses of $\mu_h$. At $\zeta=0$ this is a linear MDP.

LSVI-UCB (Algorithm 1) plays $K$ episodes. In episode $k$, with data $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$ from earlier episodes, it computes backwards from $Q^k_{H+1}\equiv0$

$$\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I,\qquad w^k_h=(\Lambda^k_h)^{-1}\sum_{\tau<k}\phi^\tau_h\big[r_h(x^\tau_h,a^\tau_h)+\max_aQ^k_{h+1}(x^\tau_{h+1},a)\big],$$ $$Q^k_h(x,a)=\min\big\{\langle w^k_h,\phi(x,a)\rangle+\beta_k\|\phi(x,a)\|_{(\Lambda^k_h)^{-1}},\,H\big\},$$

and then acts greedily, $a^k_h=\arg\max_aQ^k_h(x^k_h,a)$. An adversary may choose each initial state $x^k_1$. The regret after $K$ episodes is

$$\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],$$

where $\pi_k$ is the greedy policy of episode $k$. Throughout, $T=KH$ and $\iota=\log(2dT/p)$.

Formalization targets

Goal: Theorem 3.2

There are absolute constants $c,C>0$ such that for every $\zeta$-approximately linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta_k=c\,(d\sqrt\iota+\zeta\sqrt{kd})H$, with probability at least $1-p$,

$$\mathrm{Regret}(K)\le C\Big(\sqrt{d^3H^3T\iota^2}+\zeta dHT\sqrt\iota\Big).$$

The constants are not fixed numerically, so improvements of the constants in the proof do not invalidate the target.

Milestones

The milestones follow Appendix C: the approximate linearity of $Q^\pi$ (Lemma C.1) and the bound on its weights (Lemma C.2); the trace inequality D.1 and the adversarial-noise bound C.4; the self-normalized concentration bound D.3 (published) and the concentration event of Lemma C.3; the key estimate C.5; approximate optimism C.6; the recursive formula C.7; and the elliptical potential lemma D.2 (published) with the bonus-sum bound (21)–(24).

Significance

Theorem 3.2 shows that the regret of LSVI-UCB degrades gracefully under misspecification: the extra cost is of order $\zeta dHT\sqrt\iota$, linear in $T$ because of the bias of linear approximation and negligible when $\zeta\lesssim1/\sqrt T$. The paper also converts it into a PAC guarantee with an additive $\tilde O(\zeta dH^2)$ error. It is a reference point for later work on misspecified linear bandits and RL, which asks how far the linear term can be improved.

The result is proved on paper; no machine-checked proof is known. The formalization supplies an episodic MDP on a general measurable state space, LSVI-UCB as a function of the observed data, and its interaction with an adaptive adversary on a filtered probability space. These are shared with the companion mission on Theorem 3.1 and are reusable for other optimistic algorithms with linear function approximation. At $\zeta=0$ the goal specializes to Theorem 3.1 under the same normalization; this is a consistency check, not a dependency.

Difficulty

The central difficulty is that the regression targets $r_h+V^k_{h+1}(x^\tau_{h+1})$ depend on the data through $V^k_{h+1}$, which is computed from all earlier episodes. A martingale concentration bound for a fixed function does not apply. Lemma C.3 needs a bound that holds uniformly over the class of functions LSVI-UCB can produce, which requires a covering-number argument whose size depends on $\beta_k$; that is why the constant $C$ must be independent of $c_\beta$ and $c_\beta$ is chosen afterwards. Under misspecification a second error appears: the deviations $r_h-\langle\phi,\theta_h\rangle$ and $(\mathbb P_h-\langle\phi,\mu_h\rangle)V$ are not mean-zero and can be adversarial, so they cannot be concentrated away. Lemma C.4 absorbs them into the bonus at the price of the $\zeta\sqrt{kd}$ term in $\beta_k$. Optimism then holds only up to an error that accumulates over the horizon (Lemma C.6).

Formalization scope

• Indices are 1-based, as on the page; values and estimates are $0$ outside $1\le h\le H$.
• Values: $V^\pi$ and $V^\star$ are defined by the Bellman recursions (1) and (2), not by $\sup_\pi$.
• Measurability: the state space is a bare measurable space. Features $\phi(\cdot,a)$ are assumed measurable, and lemmas about a policy $\pi$ assume it measurable, so that every integral is meaningful.
• Actions: $\mathcal A$ is finite and nonempty. Argmax ties are broken towards the least action of a fixed linear order on $\mathcal A$.
• Interaction: the run is a process adapted to an arbitrary filtration, with actions given by Algorithm 1 and the next-state law holding conditionally on the past. The initial states are only required to be adapted.
• Probability statements: "with probability $1-p$" is "the bad set has (outer) measure at most $p$".
• Constants: $c$ and $C$ are quantified before all types, dimensions, horizons, $\zeta$, $p$ and runs. The hypotheses $d,H,K\ge1$ and $0\le\zeta\le1$ are stated.
• Assumption B measures the TV distance by the total variation norm $|\nu|(\mathcal S)$. The page's normalization $\|\mu_h(\mathcal S)\|\le\sqrt d$ is replaced by the same bound on the vector of total variations $(|\mu_h^{(i)}|(\mathcal S))_i$, because Lemma C.2 is false under the printed form; the replacement implies the printed condition and holds for tabular MDPs.
• Lemma C.7 carries the $+4H\zeta$ term that its own proof derives; the printed statement omits it. Theorem 3.2 is unaffected.

Lemmas C.3 and C.5 are formalized as printed. Their proofs use $\sup_x|V^k_{h+1}(x)|\le H$, which Algorithm 1 does not enforce from below; a solver may find that one of them needs an additional argument.

A formalization in which the goal assumes the event $\mathfrak E$, the optimism of Lemma C.6 or the recursion of Lemma C.7, or in which the run does not fix the actions to Algorithm 1's, would be trivial or false; the goal assumes none of these. Contributions are welcome on the linear-algebra lemmas (D.1, C.4, (21)–(24)), on measurability of the LSVI-UCB estimates, and on the covering argument behind Lemma C.3.

Selected references

• C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
• Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019; arXiv:1902.04779. https://arxiv.org/abs/1902.04779

Learning prices and inventory from sales

A retailer choosing both a price and an inventory target faces two coupled decisions. A higher price changes customer demand, while a smaller inventory target hides demand that exceeds available stock. The retailer observes sales, but cannot count customers who leave empty-handed. This makes even the realized lost-sales penalty unavailable as a learning signal. Chen, Chao and Shi study this information constraint using a nonparametric demand model and a spline approximation based learning algorithm, SALA (2021, supplied manuscript, §§1–3).

The formalization target is the paper's cumulative regret guarantee, together with the seven numbered supporting results in its argument. The claims retain the source's explicit constants, continuous decision domains and noise distributions. They are statement targets for proof or disproof; compiling their declarations does not establish their truth.

The market and its observations

The demand-price function is a nonincreasing function $\lambda:\mathbb R\to\mathbb R$. At price $p_t$, demand in period $t$ is $D_t(p_t)=\lambda(p_t)+\epsilon_t$. The errors are independent with a common real-valued distribution, zero mean and finite standard deviation $\sigma$. Its differentiable cumulative distribution function is $F$, with density $f$. Demand and errors are not truncated to nonnegative values.

The price interval is $P=[p^l,p^h]$, where $p^l<p^h$. Holding and lost-sales costs are $h>0$ and $b\ge0$, with $b+p>0$ on $P$. Starting inventory is $x_1=0$. After an order-up-to decision $y_t$, the retailer observes only $\min(D_t(p_t),y_t)$, and inventory carried into the next period is $(y_t-D_t(p_t))^+$. Replenishment is instantaneous and there is no purchasing or fixed ordering cost. Here $u^+=\max(u,0)$.

The expected period profit is

$$Q(p,y)=p\lambda(p)-(b+p)\mathbb E[(\lambda(p)+\epsilon-y)^+]-h\mathbb E[(y-\lambda(p)-\epsilon)^+].$$

Inventory optimization ranges over all real target levels. The lower generalized inverse gives $z^*(p)=F^{-1}((b+p)/(b+p+h))$, and the optimized profit is $G(p)=Q(p,\lambda(p)+z^*(p))$. Its maximizing price $p^*$ is interior to $P$; write $y^*=\lambda(p^*)+z^*(p^*)$. The benchmark is $TQ(p^*,y^*)$, with continuous price optimization rather than optimization on the algorithm's grid (§2, pp. 6–9).

Assumption 1 requires positive constants $A,M,\theta_1,\theta_2,\theta_3,\kappa,r,a$. Demand derivatives through order $\max\{3,\lceil\sqrt{\log T}\rceil\}$ exist and are bounded by $M$ on $[p^l-A,p^h+A]$, including the zeroth derivative. The density obeys $f(x)\le\theta_1e^{-\theta_2x}$ for $x\ge\theta_3$ and is at least $r$ within $\kappa$ of each relevant quantile. Finally $G''\le-a$ on $P$. The right-tail condition is preserved literally; it is not replaced by a two-sided moment-generating-function bound.

Formalization targets

SALA uses

$$m=\max\{3,\lceil\sqrt{\log T}\rceil\},\quad L=\lceil T^{1/2+1/(\log T)^{1/3}}\rceil,\quad l=\lceil(\log T)^{3/2}T^{1/(4\sqrt{\log T})}\rceil.$$

It explores $N=L(m+l)m$ periods with inventory target $B=\lceil\log L\log\log L\rceil$. The exploration prices are the nodes of Algorithm 0's explicit divided-difference spline. Block sales averages determine $\widehat\lambda$; sales centered by their own block averages determine the residuals $\eta_t$. Maximizing the resulting sample-average profit over a price grid of spacing $T^{-1/4}$ and real inventory targets gives $(\widehat p,\widehat y)$. Exploitation implements price $\widehat p$ and inventory $\max(x_t,\widehat y)$ (Algorithm 1, pp. 12–13).

The goal is Theorem 2:

$$R^{\mathrm{SALA}}(T)=TQ(p^*,y^*)-\mathbb E\sum_{t=1}^TQ(p_t,y_t) \le(b+p^h+h)T^{1/2+\varepsilon(T)}(\log T)^3\log\log T,$$

where $\varepsilon(T)=(\log T)^{-1/3}+1/(4\sqrt{\log T})\to0$. A threshold depends on the fixed model primitives and is chosen before the horizon. At each later horizon the required derivative orders remain exactly those of Assumption 1(ii) (Theorem 2 and Remark 1, pp. 14–15).

The supporting targets are Lemma 1's concentration bound for independent centered variables with finite MGFs near zero; Propositions 1–2's simultaneous bounds on the entire price interval for $\widehat\lambda$ and its derivative; Propositions 3–4's pointwise stock and expected-lost-sales bounds; Theorem 1's Euclidean convergence bound; and Proposition 5's expected carryover cost bound. The four estimation constants are respectively $M+\sigma$, $M+\sigma/(p^h-p^l)$, $1/r+\sigma$, and $1/r+\sigma$. Theorem 1 retains the product constant in Remark 1 and the PDF's failure probability $14T^{-4/3}$. Proposition 5 retains $2\max(h,b+p^h)\sqrt T\log T\log\log T$.

What the result would establish

The regret claim bounds the cumulative loss relative to the fixed clairvoyant benchmark using only observable sales. Its rate is sublinear, so the corresponding per-period loss vanishes. The result concerns the actual inventory path, including periods when an inventory target cannot be reached immediately.

The formal development supplies concrete objects for auditing how statistical estimation, continuous optimization and inventory dynamics interact. It also distinguishes claims printed in the source from properties established by a checked proof. The source statements are retained even where the accompanying argument has a documented gap.

Difficulties and source findings

Censoring biases both the fitted demand function and the residual distribution. Residuals within one block share an empirical mean and cannot be treated as independent copies of the original noise. The sampled price objective need not be unimodal, and inventory carryover creates an additional cost after a price and target have been selected (§§1.1 and 4).

There are also literal source issues. The displayed stock selector on page 16 compares an unnormalized empirical count with a probability level, whereas Algorithm 1 optimizes an averaged loss. The two objects are separate definitions here. The non-identical-sequence version of Lemma 1 admits a rare-jump counterexample. Further findings concern the passage from finitely many derivative estimates to a uniform estimate, and the inference of two-sided MGF finiteness from a right-tail density bound. These findings do not authorize stronger hypotheses or altered theorem constants.

Formalization scope

The development uses real prices, inventories and noise, finite sums for observations, measure-theoretic expectations and actual iterated derivatives. Published inventory primitives supply sales and leftover inventory, and published newsvendor definitions supply real-valued population and sample quantiles. The spline's knots, derivative coefficients and basis functions are explicit. No accuracy estimate, favorable-event probability or regret bound appears in the model assumptions.

The upper grid endpoint is included even when the interval length is not a multiple of the mesh. Ties use the least maximizing price and least inventory optimizer. Periods are zero-based internally; the first exploitation index is $N$. Theorems specify the deterministic domain in which exploration fits inside the horizon and all knots lie in the smoothness neighborhood. The final theorem asserts that this domain holds eventually. The printed algorithm is retained on negative-demand paths, including its fixed exploration target; no additional feasibility event removes such paths.

The source calls the goal “average regret,” but equation (3) and its proof use cumulative regret. The formal target follows that equation. Definitions contain no proof placeholders; the eight theorem declarations remain open statements. Contributions may establish or refute these exact claims and develop the supporting probability, spline and optimization theory.

Selected references

• Boxiao Chen, Xiuli Chao and Cong Shi, Nonparametric Learning Algorithms for Joint Pricing and Inventory Control with Lost Sales and Censored Demand, Mathematics of Operations Research (2021), doi:10.1287/moor.2020.1084. Citations use the supplied 44-page artifact with SSRN footers; printed and PDF page numbers coincide. No final journal pagination is inferred.

Motivation

In many sequential decision problems, changing the action is costly or administratively limited: a retailer can revise a posted price only a few times per season, a clinical trial can change its treatment allocation only a few times, and a firm can reconfigure its production line only so often. The multi-armed bandit with switching constraints (BwSC) captures this tension between learning and limited adaptivity: the learner must explore to find a good action, but every change of action consumes a hard budget. Simchi-Levi and Xu (arXiv:1905.10825, Management Science 2023) determine the optimal regret of this problem up to logarithmic factors.

Timeline. Classical bandit theory gives the minimax regret $\Theta(\sqrt{KT})$ for $K$ arms and horizon $T$ with unlimited switching (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020). Cesa-Bianchi, Dekel and Shamir (2013) showed that in adversarial bandits with switching costs the regret is $\widetilde\Theta(T^{2/3})$. For stochastic bandits processed in a fixed number of batches, Perchet, Rigollet, Chassang and Snowberg (2016) and Gao, Han, Ren and Zhou (2019) obtained regret rates of the form $T^{1/(2-2^{1-M})}$ for $M$ batches. Simchi-Levi and Xu (2019, revised 2021) treat a hard budget $S$ on the number of switches and prove matching upper and lower bounds; the lower bound, Theorem 2, is the subject of this mission.

Setting

There are $K>1$ arms and $T$ rounds. In round $t$ the learner picks $a_t\in[K]$ and observes a reward $X_t\sim\mathcal N(\mu_{a_t},1)$ from the unit-variance Gaussian environment with mean vector $\mu\in\mathbb R^K$; admissible environments have mean spread $|\mu_i-\mu_j|\le1$. A policy $\pi$ chooses $a_{t+1}$ by a Markov kernel from the past actions and rewards; $\mathbb P^\pi_\mu$ is the law of the history. The regret is

$$R^\pi_\mu(T)=T\max_i\mu_i-\mathbb E^\pi_\mu\Big[\sum_{t=1}^T X_t\Big].$$

With unit switching costs, the number of switches is $\sum_{t=1}^{T-1}\mathbb 1\{a_t\neq a_{t+1}\}$. For a budget $S\in\mathbb N$, the class $\Pi_S$ of $S$-switch policies consists of the policies whose number of switches is at most $S$ almost surely under every environment.

The budget enters through the phase index $q(S,K)=\lfloor (S-1)/(K-1)\rfloor$ (with $q(0,K)=0$) and the remainder $r(S,K)=S-1-q(S,K)(K-1)$ (so $r(0,K)=-1$). Two rates appear, with $a(q)=1/(2-2^{-q})$:

$$A=\frac{(K-r(S,K))^{2-a(q(S,K))}}{K}\,T^{a(q(S,K))},\qquad B=K^{1-a(q(S,K)+1)}\,T^{a(q(S,K)+1)}.$$

In Lean these are IsSwitchPolicy S T π, qIdx S K, rIdx S K, rateA K S T, rateB K S T, on top of the published BanditPolicy, banditMeasure, banditRegret and gaussianBandit.

Formalization targets

Goal: Theorem 2 (p. 21)

There is an absolute constant $C>0$ such that for all $K>1$, $S\in\mathbb N$, $T\ge2K$ and every $\pi\in\Pi_S$, some admissible Gaussian environment $\mu$ satisfies

$$R^\pi_\mu(T)\ \ge\ \frac{C}{\log T}\max\{A,\ B\}.$$

The constant is not fixed: the goal asserts the shape of the bound, which survives any improvement of constants.

Milestones

The proof in Appendix J (pp. 59–75) reduces to the regime $q(S,K)+2\le\log_2\log_2(T/K)$ (p. 59, two bounds by $O(\sqrt{KT})$ outside it) and then runs a five-step program on two families of environments:

1. the localized Pinsker inequality (Lemma 5) and the generalized reverse Fano inequality (Proposition 5, (35));
2. counting bounds on risky events under a single environment (Lemmas 6–7, Corollary 4);
3. bad-event regret bounds under alternative environments and the reduction to bad-event probabilities (Lemmas 8–11);
4. divergence bounds for restricted measures (property 1 of p. 72, Lemmas 12–13);
5. the final probability bounds (46)–(47).

Significance

The result. Theorem 2, together with the AdaLS upper bound (Theorem 1), shows that the optimal regret is $\widetilde\Theta(\max\{A,B\})$ for every $K$, $S$ and $T$. In particular, for fixed $K$ the regret as a function of $T$ is $\widetilde\Theta(T^{1/(2-2^{-q(S,K)})})$: it changes only when $S$ crosses a multiple of $K-1$, a phase transition in the switching budget, and $\Theta(\log\log T)$ switches suffice for the classical $\sqrt T$ rate. The lower bound holds for all randomized adaptive policies, not only batched ones.

Formalizing it. The result is proved on paper but has no machine-checked proof. Formalizing the lower bound adds a reusable change-of-measure toolkit for adaptively collected data: a reverse Fano-type inequality over families of measure spaces, stopping-time-based counting arguments on switching patterns, and divergence bounds for censored histories. Three printed steps needed repair (see Formalization scope), so the formal development also certifies a corrected version of the argument.

Difficulty

The obvious argument fails at the counting step. A naive choice of risky events (arms unobserved in fixed time windows) only gives a sum of probabilities of at least $K-1-\lfloor S/(q+1)\rfloor$, which vanishes when $S$ is at the end of a phase; this loses the floor $\lfloor (S-1)/(K-1)\rfloor$ in the exponent. The paper's events in the last window are defined through the stopping time at which the switching budget is exhausted, and they interact with the measure-change step: the restricted measures must hide enough information about the tested arm to make divergences small, while still deciding the stopping-time event. A second difficulty is that the policy is adaptive and randomized, so all events and measures are path-dependent.

Formalization scope

• Model. Histories are the published canonical bandit histories Fin T → Fin K × ℝ; rounds are 1-based in every statement (entry $s$ is round $s+1$). Environments are unit-variance Gaussian (gaussianBandit), which is all the proof uses (p. 59).
• Admissible policies. IsSwitchPolicy S T π asks the budget to hold almost surely under every unit-variance Gaussian environment, a weaker requirement than the paper's "for all sub-Gaussian $\mathcal D$", so the goal covers at least the paper's policy class. The regret lower bound is witnessed by one Gaussian instance with mean spread at most $1$, which implies the paper's bound on the supremum.
• Conventions. $S\in\mathbb N$ and unit costs (§3, p. 14); $q(0,K)=0$ and $r(0,K)=-1$ by the paper's convention $\lfloor x\rfloor=0$ for $x<0$; $\tau=\infty$ is encoded as $T+1$; divergences are Mathlib's klDiv in $[0,\infty]$, and the reverse KL is $D_{\rm re}(\mathbb P\|\mathbb Q)=\mathrm{KL}(\mathbb Q\|\mathbb P)$; conditional expectations in Lemmas 8 and 10 are stated in product form.
• Repairs. (i) Lemma 8's integrand is the regret $T\mu^*-\sum_t\mu_{a_t}$; the printed integrand is non-positive for $j=q+2$. (ii) The artificial measures (45) are replaced by records stopped at the first pull of the tested arm in the window; the printed measures do not have the claimed divergence. (iii) The p. 59 bound $\sqrt{2KT}$ is corrected to $2\sqrt{KT}$, and the companion bound for the first term, which the page omits, is a separate milestone. The first-class lemmas assume $q(S,K)\ge1$, where the page's construction is defined; the goal does not.
• Ruled out. A constant $C$ depending on $K$, $S$ or $T$; dropping the mean-spread condition; restricting to deterministic or batched policies; a switching constraint only in expectation; or stating the theorem for one fixed $(K,S)$ — each makes the statement trivial or different, and none is used.
• Infrastructure. Reused: the published canonical bandit model, the Bernoulli divergence ExploreFirst.FundIneq.klBer, the first half of Lemma 5 (ExploreFirst.Collective.lemma_6) and the classical bound BanditAlgorithm.bandit_minimax_lower_bound. Needed and reusable beyond this mission: the divergence decomposition for stopped histories, joint convexity and data processing for KL across different spaces, and the KL divergence of unit-variance Gaussians. Proofs of any milestone, and of the Gaussian-instance reduction, are welcome.

Selected references

• D. Simchi-Levi and Y. Xu, Phase Transitions in Bandits with Switching Constraints, Management Science, 2023; arXiv:1905.10825v4. https://arxiv.org/abs/1905.10825
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
• N. Cesa-Bianchi, O. Dekel and O. Shamir, Online Learning with Switching Costs and Other Adaptive Adversaries, NeurIPS 2013. https://arxiv.org/abs/1302.4387
• V. Perchet, P. Rigollet, S. Chassang and E. Snowberg, Batched Bandit Problems, Annals of Statistics, 2016. https://arxiv.org/abs/1505.00369
• Z. Gao, Y. Han, Z. Ren and Z. Zhou, Batched Multi-armed Bandits Problem, NeurIPS 2019. https://arxiv.org/abs/1904.01763
• S. Gerchinovitz, P. Ménard and G. Stoltz, Fano's Inequality for Random Variables, Statistical Science, 2020. https://arxiv.org/abs/1702.05985

Motivation

A retailer selling one product over $T$ periods must choose a price each period without knowing how demand responds to price. Charging different prices reveals the demand curve but costs revenue, and in practice every price change has its own cost: relabelling, customer goodwill, contractual limits on repricing. Dynamic pricing with learning asks for policies whose cumulative revenue loss against the best fixed price, the regret, grows slowly in $T$, and recent work also asks that the policy change its price rarely.

The paper's literature review (pp. 3–5) frames the gap. For parametric demand, Broder (2011) gives an MLE-based policy with $\tilde O(\sqrt T)$ regret and $O(\log T)$ price changes, and Cheung, Simchi-Levi and Wang (2017) study limited price changes when demand is one of finitely many known curves. Non-parametric policies such as Besbes and Zeevi (2015) and the continuum-armed bandit algorithm of Agarwal et al. (2011) do not control price changes and incur at least $O(\log T)$ of them. Perakis and Singhvi (SSRN 3336949; published in Operations Research, doi:10.1287/opre.2020.0445) show that, under a two-point bandit feedback assumption borrowed from online convex optimisation (Agarwal and Dekel 2010, Nesterov 2011), a non-parametric policy can keep $\tilde O(\sqrt T)$ regret while changing its price only $O(\log\log T)$ times.

Setting

Prices lie in $[0,1]$. In period $t$ the retailer charges $p_t$ and observes demand

$$Y_t=d(p_t)+\epsilon_t,$$

where $d$ is an unknown smooth non-increasing demand curve and $\epsilon_t$ is noise. The revenue is $r(p)=p\,d(p)$, maximised on $[0,1]$ at a unique interior price $p^*$. The two performance measures are

$$\mathcal R(T)=\sum_{t=1}^T\big(r(p^*)-r(p_t)\big),\qquad LPC(T)=1+\big|\{2\le t\le T:\ p_t\ne p_{t-1}\}\big|.$$

Assumption 1 asks for $\kappa>0$ with $d(p^*)-\kappa(p-p^*)^2\le-d'(p)\,p^*$; Assumption 2 asks that among the observations at two charged prices there is one pair with identical noise, and that the policy can identify it. $K_1$ bounds $|d^{(k)}|$ for $k\le3$.

The SLPE policy (Algorithm 1) runs in rounds $i=1,2,\dots$ with half-widths $\Delta_1=\tfrac12$, $\Delta_{i+1}=\mu\Delta_i^2$. Round $i$ charges $p^L_i=p^M_i-\Delta_i$, $p^M_i$ and $p^H_i=p^M_i+\Delta_i$ for $n_i=2\rho^4\log T/\Delta_i^4$ periods each, starting from $p^M_1=\tfrac12$. It fits a two-piece linear demand estimate whose level is the average demand $\bar D_{n_i}(p^M_i)$ and whose slopes are finite differences of the two identical-noise pairs, maximises the estimated revenue on $[p^L_i,p^H_i]$ to obtain $\tilde p^*_i$, and recentres: $p^M_{i+1}=\tilde p^*_i$.

Formalization targets

Goal: Theorem 1 and Corollary 1

Under Assumption 1, the gradient condition $|d'(p^*)|\ge(K_1/24+\kappa/4)\tfrac14+c/2$ with $c>0$, and

$$2>\mu\ge M=\tfrac1c\big(\tfrac1{\rho^2}+\tfrac{K_1}6+\tfrac\kappa4\big)+\tfrac{K_1}{12}+4\kappa,$$

there are constants $C_1,C_2,C_3$ independent of $T$ such that for every $T\ge3$, every noise realisation and every choice of the policy's tie-breaking and pair selection,

$$LPC^{SLPE}(T)\le C_3+3\log_2(\log T),$$

and, on every realisation where Assumption 2 and the concentration event $|\bar D_{n_i}(p^M_i)-d(p^M_i)|\le\Delta_i^2/\rho^2$ hold in each used round,

$$\mathcal R^{SLPE}(T)\le\big(C_1+C_2\log(\log T)\big)\sqrt T\log T .$$

Milestones

1. Lemma 1 (p. 10): Assumption 1 gives $p^*(d'(p)-d'(p^*))\le\kappa(p-p^*)^2$.
2. Lemma 2 (p. 11): $d''(p^*)=0$ with Lipschitz $r''$ and $d'$ gives the same inequality with $\kappa=\Psi+\bar\Psi+2K_1$.
3. Lemma 3 (p. 17): the identical-noise finite differences of round $i$ are within $\tfrac12K_1\Delta_i^2/12$ of $d'$ at the midpoints.
4. Hoeffding step (pp. 19–20): $\mathbb P(|\bar X_n|>\Delta^2/\rho^2)\le1/T^2$ for $n\ge2\rho^4\log T/\Delta^4$ and sub-Gaussian noise with variance proxy at most $1/3$.
5. Lemma 4 (p. 17): $|p^*-\tilde p^*_i|\le M\Delta_i^2$ on the good event of rounds $1,\dots,i$.
6. Containment (p. 17): $p^L_i\le p^*\le p^H_i$ on the good event of earlier rounds.
7. Round count (p. 24): at most $C+\log_2(\log T)$ rounds start before $T$.

Significance

The result gives a non-parametric pricing policy whose number of price changes is doubly logarithmic, the same order as the number of batches needed in batched multi-armed bandits, while its regret is within $\log T\log\log T$ of the $\Omega(\sqrt T)$ lower bound of Keskin and Zeevi (2014). Its key estimate, Lemma 4, is a perturbation bound for the maximiser of a piecewise linear surrogate of a smooth revenue function; it applies wherever an optimum is located from noisy function values with matched-noise finite differences.

The theorem is proved on paper and, to the extent that can be determined, has no machine-checked proof. Formalizing it adds a continuum-armed pricing policy with an explicit price-change bound, and a checked version of an argument whose printed proof has gaps: a high-probability step that is false as printed, an inequality used two-sidedly that is assumed one-sidedly, and a logarithm base that does not match. Lemma 4 is posed as printed. It is supported numerically but its printed proof is incomplete, so a formal proof, or a counterexample, is itself new information.

Difficulty

The obvious argument for Lemma 4 compares the first-order condition of the surrogate with that of the true revenue. It fails as written: the surrogate's maximiser may sit at an endpoint of $[p^L_i,p^H_i]$ or at the kink $p^M_i$, where no first-order condition holds, and the comparison needs a two-sided bound on $d'(p)-d'(p^*)$ while Assumption 1 is one-sided and weighted by $p^*$. The regret bound then needs the induction that keeps $p^*$ inside every round's range, a careful treatment of the last round, which the horizon truncates, and the conversion of the doubly exponential decay of $\Delta_i$ into a $\log_2\log T$ round count.

Formalization scope

Periods are 0-based and rounds 1-based. The demand is d : ℝ → ℝ, and $p^*$ is a parameter satisfying hypotheses, not a defined argmax. The noise is a single realisation ε : ℕ → ℝ, and the regret and the price-change count are numbers on it, with no expectation. The policy receives only $T,\mu,\rho$, an argmax selector (any rule returning a maximiser of a continuous function on an interval), a pair selector (four periods per round), and the observations $d(p)+\epsilon_t$ at the prices it charges. $n_i$ is rounded up. The concentration event's probability is the separate Hoeffding milestone.

The following hypotheses and repairs are added and disclosed in each item:

• Assumption 1 and the bound $K_1$ are imposed on $[-1,2]$, because SLPE can charge prices outside $[0,1]$.
• $p^*<1$, so that the optimum is interior.
• Assumption 2 is a property of the realisation, not an almost-sure statement, because under i.i.d. continuous noise it has probability zero.
• The Hoeffding step carries $\sigma^2\le1/3$ and $T\ge2$, since the printed $1-1/T^2$ is false for $\sigma\ge1$.
• The round count and Corollary 1 use $\log_2\log T$; the printed natural-log bounds fail numerically (19 price changes against a printed bound of 15.8 at $T=10^6$).
• The inner $\log(T/(2\mu\rho^4\log T))$ is replaced by $\log T$, which only changes the constants.
• Lemma 1 is posed with Assumption 1's own $\kappa$, since the printed "$\forall p\,\exists\kappa$" is trivial.

Four formalizations would make the goal trivial, and the statements rule each out: a policy that reads $d$ or $p^*$, constants allowed to depend on $T$ or on the realisation, an argmax or pair oracle not tied to the observations, and an Assumption 2 that no realisation can satisfy (zero noise with in-block pairs satisfies it, and a sanity check exhibits a full instance).

Theorem 2 (the relaxed Assumption 2A and Algorithm 2) is not part of the mission. A complete development needs Taylor's theorem with remainder, sub-Gaussian tail bounds (available as Mathlib's HasSubgaussianMGF and the platform theorem BanditAlgorithm.subgaussian_sample_mean_tail_bound), and bookkeeping for the round schedule. The schedule lemmas and the finite-difference bound are reusable beyond this paper. Proofs of any milestone are welcome, as is a counterexample to Lemma 4's constant.

Selected references

• G. Perakis and D. Singhvi, Dynamic Pricing with Unknown Non-Parametric Demand and Limited Price Changes, SSRN 3336949 (PDF of 2020-07-03); published in Operations Research. https://ssrn.com/abstract=3336949, https://doi.org/10.1287/opre.2020.0445
• O. Besbes and A. Zeevi, On the (Surprising) Sufficiency of Linear Models for Dynamic Pricing with Demand Learning, Management Science 61(4), 2015. https://doi.org/10.1287/mnsc.2014.2031
• W. C. Cheung, D. Simchi-Levi and H. Wang, Dynamic Pricing and Demand Learning with Limited Price Experimentation, Operations Research 65(6), 2017. https://doi.org/10.1287/opre.2017.1629
• N. B. Keskin and A. Zeevi, Dynamic Pricing with an Unknown Demand Model: Asymptotically Optimal Semi-Myopic Policies, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1294
• A. Agarwal, D. P. Foster, D. Hsu, S. M. Kakade and A. Rakhlin, Stochastic Convex Optimization with Bandit Feedback, NeurIPS 2011. https://arxiv.org/abs/1107.1744
• V. Perchet, P. Rigollet, S. Chassang and E. Snowberg, Batched Bandit Problems, Annals of Statistics 44(2), 2016. https://arxiv.org/abs/1505.00369

Motivation

Reinforcement learning with a generative model (a simulator that returns an independent next state for any queried state–action pair) is the standard setting for measuring how many samples are needed to plan in an unknown Markov decision process. The simplest algorithm is model-based planning: query each pair $N$ times, build the empirical transition kernel, and plan in the resulting empirical MDP. Azar, Munos and Kappen (2013) showed that $\widetilde O\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^3\varepsilon^2}\big)$ total samples suffice and are necessary, but only for $\varepsilon \le 1/\sqrt{(1-\gamma)|\mathcal S|}$. Agarwal, Kakade and Yang (2020) extended the range to $\varepsilon \le 1/\sqrt{1-\gamma}$. A sample size barrier remained: for larger $\varepsilon$, no algorithm was known to be minimax optimal with fewer than $\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^2}$ samples.

Li, Wei, Chi and Chen (arXiv:2005.12900v8, Operations Research, 2024) remove the barrier: the sample size is minimax optimal over the full range $0 < \varepsilon \le 1/(1-\gamma)$. They give two planners. The first (Theorem 1) perturbs the rewards slightly at random. The second, the subject of this mission, leaves the rewards unchanged and instead chooses among near-optimal actions by a randomized but structured rule.

Timeline:

• 2013: Azar–Munos–Kappen, minimax sample complexity of model-based planning for $\varepsilon \le 1/\sqrt{(1-\gamma)|\mathcal S|}$.
• 2018: Sidford, Wang, Wu, Yang and Ye, a model-free variance-reduced method, minimax for $\varepsilon \le 1$.
• 2020: Agarwal–Kakade–Yang, model-based planning minimax for $\varepsilon \le 1/\sqrt{1-\gamma}$, via absorbing MDPs.
• 2020 (v1) – 2024: Li–Wei–Chi–Chen, the full range $\varepsilon \le 1/(1-\gamma)$ (this paper).

Setting

A finite discounted MDP $\mathcal M = (\mathcal S,\mathcal A,P,r,\gamma)$ has states $\mathcal S$, actions $\mathcal A = \{1,\dots,|\mathcal A|\}$, a transition kernel $P(\cdot\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in(0,1)$. A deterministic policy $\pi:\mathcal S\to\mathcal A$ has value $V^\pi(s)$, the expected discounted sum of rewards from $s$, and Q-function $Q^\pi(s,a) = r(s,a) + \gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$. The optimal value is $V^\star(s) = \max_\pi V^\pi(s)$ and $Q^\star = r + \gamma P V^\star$.

The data are $N$ independent next states $s^i_{s,a}\sim P(\cdot\mid s,a)$ for every pair, and the empirical kernel is $\widehat P(s'\mid s,a) = \frac1N\sum_i \mathbb 1\{s^i_{s,a} = s'\}$. The empirical MDP $\widehat{\mathcal M} = (\mathcal S,\mathcal A,\widehat P,r,\gamma)$ has optimal functions $\widehat Q^\star$ and $\widehat V^\star$.

The conservative planner (Algorithm 2) draws a threshold $\varsigma\sim\mathrm{Unif}(0,\xi)$ independently of the data and plays

$$\widehat\pi_{\mathrm c}(s) := \min\{a\in\mathcal A : \widehat Q^\star(s,a) > \widehat V^\star(s) - \varsigma\},$$

the smallest-indexed action whose empirical Q-value is within $\varsigma$ of optimal.

Formalization targets

Goal: Theorem 2

There are universal constants $c_0, c_1 > 0$ such that, for every MDP as above, every $\delta > 0$ and $0 < \varepsilon \le \frac1{1-\gamma}$, with $\xi = \frac{c_1(1-\gamma)\varepsilon}{|\mathcal S|^5|\mathcal A|^5}$ and

$$N \ge \frac{c_0\log\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)\varepsilon\delta}\big)}{(1-\gamma)^3\varepsilon^2},$$

with probability at least $1-\delta$ over the data and $\varsigma$,

$$\forall (s,a):\qquad V^{\widehat\pi_{\mathrm c}}(s)\ge V^\star(s)-\varepsilon \quad\text{and}\quad Q^{\widehat\pi_{\mathrm c}}(s,a)\ge Q^\star(s,a)-\gamma\varepsilon.$$

The constants are left unspecified, as in the paper.

Milestones

The paper's own steps, in the order of §6.4:

1. Lemma 7: $\widehat V^{\pi^\star} - \widehat V^{\widehat\pi_{\mathrm c}} \le \frac{\xi}{1-\gamma}\mathbf 1$.
2. Lemma 3 and (88): the $(s,a)$-absorbing MDPs reproduce $Q^\star$ at the right reward and depend Lipschitz-continuously on it.
3. (56): a point of a finite net gives an absorbing MDP within $\omega$ of $\widehat Q^\star$.
4. Lemma 8: with probability $1-\delta$ over $\varsigma$, the near-optimal action sets are unchanged by any perturbation of size $\frac{\xi\delta}{8|\mathcal S||\mathcal A|}$.
5. (57): consequently $\widehat\pi_{\mathrm c}$ coincides with the conservative policy of every nearby absorbing MDP.
6. Lemmas 2 and 1: the policy-evaluation bounds used for the remaining terms of (53).

Significance

Theorem 2 shows that the minimax sample size $\widetilde O\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^3\varepsilon^2}\big)$ is reachable over the whole range of $\varepsilon$ without altering the reward function: a planner can keep the model it estimated and only change how it breaks near-ties. The guarantee covers both value and Q-function suboptimality, and with a sample size proportional to $1/(1-\gamma)$ rather than $1/(1-\gamma)^2$ in the large-$\varepsilon$ regime it allows a coarse but correct policy to be computed from very few samples.

None of these results is formalized. The mission produces a machine-checked account of the decoupling argument for data-dependent policies (absorbing MDPs, nets, stability of the tie-breaking rule), which the companion missions on Theorems 1 and 3 share. The paper omits the last step of the proof of Theorem 2 ("follows from an identical argument as in the proof of Theorem 1"); a formal proof has to supply it, including the analogue of Lemma 5 for $\widehat\pi_{\mathrm c}$, which the paper does not state.

Difficulty

The policy $\widehat\pi_{\mathrm c}$ depends on all the data, so the standard concentration argument for a fixed policy (Lemma 1) does not apply to $\widehat V^{\widehat\pi_{\mathrm c}} - V^{\widehat\pi_{\mathrm c}}$. A union bound over all $|\mathcal A|^{|\mathcal S|}$ deterministic policies costs a factor $|\mathcal S|$ in the sample size, which is exactly the barrier. The leave-one-out construction removes the samples of one pair $(s,a)$ from the policy; it works only if the policy is stable under the small change of $\widehat Q^\star$ that this causes. The greedy policy is not stable when two actions nearly tie. The conservative rule is stable with high probability over $\varsigma$ (Lemma 8), but only because it takes the smallest near-optimal action: the set $\{a : \widehat Q^\star(s,a) > \widehat V^\star(s)-\varsigma\}$ is stable, and a rule that picked an arbitrary member of it would not be.

Formalization scope

All declarations live in the namespace BreakingSample.Conservative. The MDP layer reuses the platform's FoundationsML.ReinforcementLearning definitions (IsTransitionKernel, PolicyValue, QFunction); deterministic policies enter as point-mass stochastic policies, and $V^\star$ is the maximum over the finite set of maps $\mathcal S\to\mathcal A$. Norms are sup norms on finite function types. The order on $\mathcal A$ is an arbitrary linear order on a finite type.

Probability: a data set is a map $\mathcal S\times\mathcal A\times\mathrm{Fin}\,N\to\mathcal S$ with the product law, so probabilities of data events are finite sums. The threshold $\varsigma$ has the uniform law on $[0,\xi]$; joint probabilities are $\sum_x \mathbb P(x)\,\mathrm{Unif}(0,\xi)\{\varsigma : (x,\varsigma)\in E\}$, with the outer measure for non-measurable sections. "With probability at least $1-\delta$" is stated as an upper bound $\delta$ on the probability of the failure event. Because the policy defined by (10) is a predicate on policies, the conclusion is stated for every policy satisfying (10). The universal constants are quantified before all types and parameters. The goal adds $N>0$, the standing assumption of (3); "the same assumptions of Theorem 1" is formalized with the goal's own constants $c_0, c_1$.

A trivializing formalization is ruled out: $\widehat\pi_{\mathrm c}$ is the smallest-index rule of (10), not an arbitrary policy within $\varsigma$ of optimal, and $\varsigma$ is random, not fixed.

Infrastructure that a complete development needs and that is reusable: Bellman optimality for finite MDPs with deterministic policies and real rewards, the resolvent identities, Bernstein's inequality for the empirical kernel, the absorbing-MDP construction, and the analogue of Lemma 5 for the conservative policy. Proofs of any milestone, and of the policy-evaluation lemmas, are welcome.

Selected references

• G. Li, Y. Wei, Y. Chi, Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8. https://arxiv.org/abs/2005.12900
• M. G. Azar, R. Munos, H. J. Kappen, Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model, Machine Learning 91, 2013. https://doi.org/10.1007/s10994-013-5368-1
• A. Agarwal, S. Kakade, L. F. Yang, Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal, COLT 2020. https://arxiv.org/abs/1906.03804
• A. Sidford, M. Wang, X. Wu, L. F. Yang, Y. Ye, Near-Optimal Time and Sample Complexities for Solving Markov Decision Processes with a Generative Model, NeurIPS 2018. https://arxiv.org/abs/1806.01492

Motivation

Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution $P_{s,a}$ from the transitions they have observed out of the state–action pair $(s,a)$. Their regret analyses then need to know how far the empirical distribution $\hat p$ can be from the true one $p$. The standard tool is an $\ell_1$ bound on $\hat p-p$, as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order $\sqrt S$ in the number of states $S$. What the analysis actually uses, however, is the deviation along one direction: the projection $(\hat p-p)^Th$ onto a bias (or value) vector $h$ whose entries differ by at most the MDP's diameter $D$.

S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order $\tilde O(D\sqrt{SAT})$ for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on $(\hat p-p)^Th$ whose leading term is governed by a variance of $h$ under $p$, written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.

Setting

Fix a number of states $S$ and order them $1,\dots,S$. A probability vector $p\in\Delta^S$ has $p_i\ge0$ and $\sum_ip_i=1$. A multinoulli trial with parameter $p$ is a random state $X$ with $\mathbb P(X=i)=p_i$. Draw $n$ independent trials $X_1,\dots,X_n$ and let

$$\hat p_i=\frac{\#\{t: X_t=i\}}{n}$$

be the empirical probability vector, the average of the one-hot outcomes. For $p$ and a vector $h\in\mathbb R^S$ define the stick-breaking quantities

$$\gamma_i=\frac{p_i(p_{i+1}+\cdots+p_S)}{p_i+\cdots+p_S},\qquad H_{i+1}=\frac{1}{\sum_{j=i+1}^Sp_j}\sum_{j=i+1}^Sh_jp_j,\qquad c_i=h_i-H_{i+1}.$$

Thus $H_{i+1}$ is the mean of $h$ under $p$ conditioned on the states after $i$, and $c_i$ compares $h_i$ with it. The sum $\sum_{i<S}\gamma_ic_i^2$ equals the variance of $h(X)$ for $X\sim p$. In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of $n$ trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.

Formalization targets

Goal: Proposition 5.2 (p. 9)

Let $h\in\mathbb R^S$ satisfy $|h_i-h_{i'}|\le D$ for all $i,i'$, let $n\ge96$ and $\rho\in(0,1)$. Then, with probability at least $1-\rho$,

$$\big|(\hat p-p)^Th\big|\le2\sqrt{\log(n/\rho)\sum_{i<S}\frac{\gamma_ic_i^2}{n}}+3D\,\frac{\log(2/\rho)}{n}.$$

Milestones

1. Fact 1 (p. 17), a deterministic identity: for probability vectors $\tilde p,\bar p$ with stick-breaking ratios $\tilde y_i=\tilde p_i/(\tilde p_i+\cdots+\tilde p_S)$ and $\bar y_i$,

$$(\tilde p-\bar p)^Th=\sum_i(\tilde y_i-\bar y_i)(h_i-\tilde H_{i+1})(\bar p_i+\cdots+\bar p_S)=\sum_i(\tilde y_i-\bar y_i)(h_i-\bar H_{i+1})(\tilde p_i+\cdots+\tilde p_S).$$

2. The projection as a sum of martingale differences (proof, p. 21): with $Z_{t,i}=c_i\mathbb 1(X_t=i)-c_i\frac{p_i}{p_i+\cdots+p_S}\mathbb 1(X_t\ge i)$ and $Z_t=\sum_iZ_{t,i}$,

$$\frac1n\sum_{t=1}^nZ_t=(\hat p-p)^Th,$$

together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): $\mathbb E[Z_{t,i}Z_{t,j}]=0$ for $i\ne j$. 4. The predictable variance (proof, p. 21): $\sum_{t=1}^n\mathbb E[Z_t^2]=\sum_ic_i^2\,n\,\gamma_i$. 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance $V_n$: for $n\ge96$, $\delta\in(0,1)$, with probability greater than $1-\delta$,

$$|M_n|\le2\sqrt{V_n\ln(n/\delta)}+3K\ln(n/\delta).$$

Significance

The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along $h$ with constant probability. Because the bound is stated along a single direction and is weighted by the variance of $h$ rather than by $D$ alone, it avoids the $\sqrt S$ loss that an $\ell_1$ bound would incur, which is part of how the paper's regret bound improves on UCRL2's $\tilde O(DS\sqrt{AT})$. The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.

Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in $O(\cdot)$ and its algorithm's parameters are given as $\Theta(\cdot)$. Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.

Difficulty

Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as $\mathrm{Var}_p(h)$; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.

A known subtlety: the paper's proof, through Corollary B.1, yields the second term $3D\log(n/\rho)/n$, while the statement prints the smaller $3D\log(2/\rho)/n$. The printed statement is still true for $n$ iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.

Formalization scope

• States are Fin S with its natural order, 0-based; the paper's range $i<S$ is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.
• Probability vectors are p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to $0$ (Lean's convention), which gives the values the identities need; no positivity of $p$ is assumed.
• One trial has law cat p $=\sum_ip_i\delta_i$; $n$ trials have the product law trialsLaw n p $=$ Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability $1-\rho$" is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than $1-\delta$" is strict. $\log$ is Real.log.
• The proof displays (milestones 2–4) are stated in the iid reading of the proposition: the paper writes them for transitions of an MDP out of a fixed $(s,a)$, with an indicator $\mathbb 1(s_{t-1}=s,a_{t-1}=a)$ and a random count $\tau$; here the indicator is one and $\tau=n$, and the conditional expectations are expectations under one draw of law $p$. Milestone 2 assumes every drawn state has positive probability (true almost surely), which the page's intermediate sum over $i\le S-1$ needs.
• Corollary B.1 is posed for a general filtered probability space, with $Z_i$ $\mathcal F_i$-measurable, $|Z_i|\le K$ almost surely and $\mathbb E[Z_i\mid\mathcal F_{i-1}]=0$.

The goal cannot be satisfied by a degenerate reading: $\hat p$ is built from the sample, the measure is the $n$-fold product of the categorical law $p$, the event is the good event itself (not a complement bound), and the variance term is not identically zero (for $S=2$, $p=(\tfrac12,\tfrac12)$ it equals $(h_1-h_2)^2/4$).

Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• Y. Seldin, F. Laviolette, N. Cesa-Bianchi, J. Shawe-Taylor and P. Auer, PAC-Bayesian inequalities for martingales, IEEE Transactions on Information Theory 58(12), 2012. https://doi.org/10.1109/TIT.2012.2211334