Operations Research

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations stabilizes a hybrid SDE in the sense of mean-square exponential stability when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval $\tau$, and proved $H_\infty$-stability, mean-square asymptotic stability, almost sure asymptotic stability and exponential stability of the controlled system. This mission formalizes the almost sure asymptotic stability result, Theorem 3.4, and the results it is built on.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$, the last observation time up to $t$. The controlled system is

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$. The feedback $u$ sees the state only at the observation times.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Condition35, in the namespace You2015.Asymp; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, and solutions SolvesSampledHybridSDE, in the namespace You2015.Shared shared with the companion mission.

Formalization targets

Goal: Theorem 3.4 (almost sure asymptotic stability)

Under the hypotheses above, every solution of (2.1) satisfies

for all $x_0\in\mathbb R^n$ and $r_0\in S$. No rate is claimed; the statement is the qualitative convergence of almost every path.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (3.23) $\sup_{t\ge0}\mathbb E|x(t)|^2<\infty$.
5. $|\mathbb E|x(t_2)|^2-\mathbb E|x(t_1)|^2|\le C(t_2-t_1)$.
6. Theorem 3.3: $\lim_{t\to\infty}\mathbb E|x(t)|^2=0$.
7. (3.24)–(3.25): $\mathbb E\int_0^\infty|x(t)|^2dt<\infty$ and $\liminf_{t\to\infty}|x(t)|=0$ a.s.
8. (3.28): $\mathbb P(\exists t:|x(t)|\ge h)\le C/h^2$ for $h>|x_0|$.

Significance

The result. Theorem 3.4 says that a controller sampling the state at rate $1/\tau$ makes almost every trajectory of the switching system converge to the equilibrium, with an explicit, checkable bound (3.5) on $\tau$. Mean-square convergence (Theorem 3.3) does not imply almost sure convergence in general, and a single trajectory is what an operator observes, so the pathwise statement is the one relevant to a deployed system. Condition (3.5) is stated in terms of the constants of Assumptions 2.1, 2.2 and 3.1, so for a concrete system (Section 6 of the paper) it gives a numerical bound on the observation interval.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a reusable definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1).

Difficulty

Equation (2.1) is a stochastic differential delay equation with the delay $t-\delta_t$, which is bounded but jumps at every observation time and has derivative $1$ in between. The stability theorems for hybrid delay equations in the literature require a differentiable delay with derivative less than one (Mao–Yuan, p. 285), so they do not apply. Applying $\mathcal LU$ directly to $U(x(t),r(t),t)$ leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval, so a Lyapunov function of the current state alone does not close the argument.

For the goal, the natural first idea, deducing almost sure convergence from $\mathbb E|x(t)|^2\to0$ or from $\int_0^\infty|x(t)|^2dt<\infty$ a.s., fails: both are compatible with paths that make ever shorter excursions away from $0$. The obstacle is to exclude infinitely many excursions of a fixed size, which neither moment statement controls.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5) and (3.21) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation $\mathbb E|\cdot|^2$ and every time integral of a nonnegative quantity is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,\tau$ are data of each statement. The paper's "$C$ denotes a positive constant" is an existential chosen after $x_0$, $r_0$ and the solution, and before the time variables and $h$.
• (3.15) and (3.21) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. Misprints on the page (for example $g(x,i,s)=f(x,i,0)$ on p. 909 and the swapped definitions of $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals (which vanish for non-integrable integrands), the solution notion admits the true solution and requires path continuity, the derivative witnesses of $U$ are tied to $U$, and a sorry-free check shows that the data hypotheses (Assumptions 2.1, 2.2, 3.1, $C^{2,1}$, (3.5)) are satisfiable, for example by $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $\lambda_1=1/4$, $\lambda_2=1$, $\tau=1/10$.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, and Doob's maximal inequality in continuous time. These are reusable far beyond this mission. Section 4 of the paper (exponential stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005

Motivation

Pontryagin's maximum principle gives necessary conditions for optimality in deterministic optimal control: along an optimal trajectory, the optimal control maximizes (or minimizes) a Hamiltonian built from an adjoint process. For a system driven by Brownian noise the analogous statement was open in full generality for two decades. The difficulty appears exactly when the diffusion coefficient depends on the control and the control domain is not convex, the situation of controlled volatility in finance, of controlled noise intensity in engineering, and of any problem whose admissible actions form a discrete or otherwise nonconvex set.

Shige Peng's 1990 paper (SIAM J. Control Optim. 28(4)) closed that case. It introduced the second-order adjoint process and a second-order variational inequality, and it is the starting point of the modern theory of stochastic Hamiltonian systems and of backward stochastic differential equations as a tool in control.

Timeline.

• 1972: Kushner obtains necessary conditions for diffusions whose diffusion coefficient does not depend on the control (SIAM J. Control 10).
• 1973–1978: Bismut introduces the adjoint equation as a linear backward stochastic differential equation and develops duality methods (SIAM Review 20).
• Early 1980s: Bensoussan and Haussmann prove maximum principles for convex control domains or control-independent diffusion, using the first-order adjoint equation only.
• 1990: Peng proves the general principle, with control-dependent diffusion and an arbitrary nonempty control domain (this mission). In the same year Pardoux and Peng prove existence and uniqueness for nonlinear backward SDEs (Systems Control Lett. 14).
• 1999: Yong and Zhou give a textbook account of the theory (Springer).

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space carrying a standard $d$-dimensional Wiener process $B=(B^1,\dots,B^d)$, and let $\mathcal F^t=\sigma\{B(s);0\le s\le t\}$ be its natural filtration. Fix a horizon $T>0$, an initial state $x_0\in\mathbb R^n$ and a nonempty control domain $U\subseteq\mathbb R^k$. The data are

An admissible control $v$ is a progressively measurable $U$-valued process with $\sup_{t\le T}E|v(t)|^m<\infty$ for every $m\ge1$. Its trajectory solves the state equation

and its cost is $J(v)=E\int_0^Tl(x(t),v(t))\,dt+E\,h(x(T))$. A pair $(y,u)$ is optimal when $J(u)\le J(v)$ for every admissible $v$.

Assumption (3): $g,\sigma,l,h$ are $C^2$ in $x$, jointly continuous in $(x,v)$ together with their first and second $x$-derivatives; $g_x,g_{xx},\sigma_x,\sigma_{xx},l_{xx},h_{xx}$ are bounded; and $g,\sigma,l_x,h_x$ grow at most like $C(1+|x|+|v|)$.

The Hamiltonian is $H(x,v,p,K)=l(x,v)+(p,g(x,v))+\sum_j(K_j,\sigma^j(x,v))$. The first-order adjoint process $(p,K)$ solves the backward equation

and the second-order adjoint process $(P,Q)$, symmetric-matrix valued, solves

with all coefficients evaluated along $(y(t),u(t))$ and both solutions adapted to $\mathcal F^t$.

Formalization targets

Goal: Theorem 3 (p. 975)

If $(y,u)$ is optimal, then adjoint processes $(p,K)$ and $(P,Q)$ exist in $L^2_{\mathcal F}$, solving the two equations above, such that for every $v\in U$, for almost every $\tau\in[0,T]$, almost surely,

all evaluated at time $\tau$.

Milestones

1. Lemma 1: the spike-perturbed state equals $y+y_1+y_2$ up to $o(\varepsilon^2)$ in mean square, where $y_1,y_2$ solve the first- and second-order variational equations (5), (6).
2. Lemma 2: the cost expansion (11) is $\ge o(\varepsilon)$ at an optimal control.
3. Eq. (13): existence and uniqueness of $(p,K)$ as a Riesz representer.
4. Eq. (14): the cost expansion in Hamiltonian form is $\ge o(\varepsilon)$.
5. Eq. (17): existence and uniqueness of $(P,Q)$ as a Riesz representer.
6. Eq. (18): the variational inequality for these representers.
7. Eq. (19): $(p,K)$ is the unique solution of the first-order adjoint equation.
8. Eq. (20): $(P,Q)$ solves the second-order adjoint equation.

Significance

The result. Theorem 3 is the necessary condition for optimal control of diffusions in its general form. When $\sigma$ does not depend on the control the trace terms cancel and it reduces to the classical first-order principle. When the control enters the diffusion, the first-order condition is false in general, and the second-order adjoint $P$ is the correction. The theorem underlies stochastic linear-quadratic theory, the verification of optimal portfolio and volatility-control policies, and the relation between the maximum principle and the Hamilton–Jacobi–Bellman equation.

Formalizing it. The theorem is classical and proved; none of it is machine-checked. Mathlib has real Brownian motion but no stochastic integral, no SDE and no backward SDE. This mission produces the first formal statements on the platform of a controlled SDE, of a backward SDE and of the maximum principle, together with a precise definition layer (Itô integral, Itô process, BSDE solution) that later missions can reuse, e.g. for Peng's endpoint-constrained principle (§6 of the paper) or for the existence theory of BSDEs. A formal proof would also pin down the approximation arguments the paper leaves to the reader.

Difficulty

The obvious route perturbs the optimal control convexly, $u+\varepsilon(v-u)$, and differentiates the cost. That needs $U$ convex. For nonconvex $U$ one uses a spike variation on a time interval of length $\varepsilon$. For deterministic systems the state then moves by $O(\varepsilon)$ and a first-order expansion suffices. With control-dependent diffusion the stochastic integral over the spike interval moves the state by order $\sqrt\varepsilon$ in $L^2$, so the first-order variational equation leaves an error of the same order as the effect being measured. Second-order terms in the state enter the cost at order $\varepsilon$, and they are quadratic, so they cannot be handled by a single linear adjoint. The second-order expansion, the matrix-valued adjoint that represents the quadratic term, and the identification of both adjoints with backward SDEs are where the work lies. On the formal side, none of the stochastic calculus exists in Mathlib: the Itô isometry, Itô's formula for matrix-valued processes, moment estimates for linear SDEs and the martingale representation behind the backward equations all have to be built.

Formalization scope

Conventions committed to in Lean:

• States, controls and noise are Fin n → ℝ, Fin k → ℝ, Fin d → ℝ with the sup norm; matrices are Matrix (Fin n) (Fin n) ℝ. Time is ℝ≥0, and time integrals are over [0, t] ⊂ ℝ.
• The Wiener process is $\mathbb R^d$-valued: the paper's "$R^n$-valued standard Wiener process" (p. 967) is a misprint, since $\sigma(x,v)\in\mathcal L(R^d,R^n)$. Coordinates are independent real Brownian motions (Mathlib's IsBrownianReal).
• The filtration is the natural filtration of $B$, not completed, as on p. 967.
• "Adapted", for processes integrated in $dt$, is read as progressively measurable.
• The Itô integral is a relation (an $L^2$ limit of elementary integrals, as in Ikeda–Watanabe), not an operator. SDE and BSDE solutions hold "for every $t$, almost surely", with $\sup_tE|x(t)|^2<\infty$ for forward solutions and $L^2_{\mathcal F}$ membership for backward ones.
• Optimality is among admissible controls of finite cost, and the optimal cost is finite; the paper never states finiteness, and a cost can be $+\infty$ under (3).
• Lemma 1 is stated with $o(\varepsilon^2)$ where the page prints "$\le C\varepsilon^2$" in (4). The proof (via (10)) establishes $o(\varepsilon^2)$, and Lemma 2 needs it. Lemma 1, (13), (17), (19) and (20) are stated for any admissible pair, since their proofs do not use optimality.
• "$\ge o(\varepsilon)$" means: some $r(\varepsilon)=o(\varepsilon)$ as $\varepsilon\to0^+$ bounds the left side from below for small $\varepsilon$. "$\forall v\in U$, a.e., a.s." quantifies $v$ first, then $\tau$, then $\omega$.
• $P$ and $Q_j$ are symmetric-valued ($R^{n,n}$ is the space of symmetric matrices, p. 973). Stochastic integrals against the matrix $\sigma$ or $Q$ are sums over the columns, $\sum_j(\cdot)_j\,dB^j$.

Trivializing formalizations ruled out. Without adaptedness the backward equations have pathwise solutions with $K=0$ and the goal would be free; every adjoint and every solution is required to be progressive for the natural filtration of $B$. The hypotheses are satisfiable: a sorry-free check shows that the zero problem has an optimal pair and that the Itô relation holds for the zero integrand.

Infrastructure needed, and reusable. The Itô integral and isometry, Itô's formula (vector and matrix forms), existence, uniqueness and moment estimates for linear SDEs with bounded coefficients, Riesz representation in $L^2_{\mathcal F}$, and existence and uniqueness for linear BSDEs (via martingale representation for the Brownian filtration). All of these are reusable well beyond this mission; contributions of any of them, as separate theorems, are welcome. Related platform definitions: the Ethier–Kurtz series (EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE) formalizes an Itô integral by dyadic step approximation and uncontrolled SDEs over a completed filtration. The deterministic Pontryagin principle appears in Vector Space Methods XII and Dynamic Programming and Optimal Control III.

Selected references

• S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4), 966–979, 1990. https://doi.org/10.1137/0328054
• H. J. Kushner, Necessary Conditions for Continuous Parameter Stochastic Optimization Problems, SIAM J. Control 10(3), 550–565, 1972. https://doi.org/10.1137/0310041
• J.-M. Bismut, An Introductory Approach to Duality in Optimal Stochastic Control, SIAM Review 20(1), 62–78, 1978. https://doi.org/10.1137/1020004
• E. Pardoux and S. Peng, Adapted Solution of a Backward Stochastic Differential Equation, Systems & Control Letters 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
• J. Yong and X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

Motivation

A retailer who sells several products from shared, non-replenishable inventory over a finite season must set prices without knowing how demand responds to them. Every price posted is both a sale and an experiment. This is the network revenue management problem with demand learning, and it sits between two literatures: dynamic pricing with inventory, where demand is known and the fluid linear program of Gallego and van Ryzin (1997) is the standard benchmark, and multi-armed bandits, where learning is the whole problem but there are no resource constraints.

Ferreira, Simchi-Levi and Wang (Oper. Res. 2018) combine Thompson sampling with a linear-programming step: sample a demand model from the posterior, solve the fluid LP for that model, and randomize prices according to its solution. The same paper extends the scheme to continuous price sets, contextual pricing and bandits with knapsacks.

Timeline of the relevant results:

• 1997: Gallego and van Ryzin introduce the fluid LP upper bound for network revenue management with known demand.
• 2012: Besbes and Zeevi give a non-Bayesian network pricing algorithm with worst-case regret $O(K^{5/3}T^{2/3}\sqrt{\log T})$.
• 2013: Badanidiyuru, Kleinberg and Slivkins (bandits with knapsacks) give worst-case regret $O(\sqrt{KT\log T})$.
• 2013–2014: Bubeck and Liu and Russo and Van Roy give prior-free Bayesian regret bounds for Thompson sampling in unconstrained bandits.
• 2018: Ferreira, Simchi-Levi and Wang prove the $O(\sqrt{TK\log K})$ Bayesian regret bound for TS-fixed (Theorem 1), the target of this mission.

Setting

There are $N$ products and $M$ resources. One unit of product $i$ consumes $a_{ij}\ge0$ units of resource $j$, and resource $j$ starts with inventory $I_j\ge0$ that is never replenished. The season has $T$ periods. In each period the retailer posts one of $K$ price vectors $p_k=(p_{1k},\dots,p_{Nk})$ or a shut-off price $p_\infty$ under which demand is zero.

Given the posted price $p_k$, the demand vector $D(t)\in\mathbb R^N_+$ has law $F(\cdot\,;p_k,\theta)$, where $\theta\in\Theta$ is unknown and drawn from a known, arbitrary prior $\mu_0$. Demand is independent of the past given the posted price and $\theta$, and is bounded: $D_i(t)\in[0,\bar d_i]$. Write $d_{ik}(\rho)$ for the mean demand of product $i$ under $p_k$ and parameter $\rho$, and $d=d(\theta)$.

When inventory covers all demand, all demand is sold. Otherwise the satisfied demand $\tilde D(t)$ satisfies $0\le\tilde D_i(t)\le D_i(t)$, leaves every inventory nonnegative, and leaves at least one resource at zero; no other rule is imposed. Revenue is $\mathrm{Rev}(T)=\sum_t\sum_i\tilde D_i(t)P_i(t)$.

For a mean-demand matrix $d$ and capacities $c_j=I_j/T$, the linear program $\mathrm{LP}(d)$ is

with optimal value $\mathrm{OPT}(d)$.

TS-fixed (Algorithm 1): in each period, sample $\theta(t)$ from the posterior of $\theta$ given the history of posted prices and observed demands; let $x(t)$ be an optimal solution of $\mathrm{LP}(d(\theta(t)))$; post $p_k$ with probability $x_k(t)$ and $p_\infty$ with the remaining probability; observe demand and update the posterior.

Finally $p_{\max}=\max_k\sum_ip_{ik}\bar d_i$ and $p^j_{\max}=\max_{i:a_{ij}\neq0,\,k}p_{ik}/a_{ij}$.

Formalization targets

Goal: Theorem 1 against the LP benchmark

For $K\ge2$, $T\ge1$, every prior, every bounded demand family, every admissible fulfilment rule and every run of TS-fixed,

The paper prints this bound for $\mathrm{BayesRegret}(T)=\mathbb E[\mathrm{Rev}^*(T)]-\mathbb E[\mathrm{Rev}(T)]$, where $\mathrm{Rev}^*$ is the revenue of the optimal policy that knows $\theta$; see Formalization scope for why the LP benchmark is stated instead.

Milestones

The article states Theorem 1 and says that its proof is in the online appendix (Supplemental Material at the DOI). The article itself contains no numbered lemma. The milestone list is therefore empty; the appendix's lemmas will be added as milestones once the appendix is held.

Significance

The bound is prior-free and has explicit constants that depend only on prices, consumption rates and demand bounds. Its dependence on $T$ matches the $\Omega(\sqrt{KT})$ lower bound for Bayesian regret in unconstrained bandits with rewards in $[0,1]$, a special case of the model with no inventory constraints (Bubeck and Cesa-Bianchi 2012, Theorem 3.5). It shows that the posterior-sampling principle survives the addition of resource constraints, lost sales and randomized LP-based pricing, and it is the template for the paper's later results (TS-update, contextual pricing, bandits with knapsacks).

The theorem is proved on paper but, as far as a platform search shows, not formalized anywhere. The platform has a formal proof of the unconstrained Bayesian Thompson sampling bound $\sqrt{kn\log k/2}$ (BanditAlgorithm.thompson_sampling_bayesian_regret, Lattimore–Szepesvári Theorem 36.5) and an open single-product deterministic upper bound in revenue management (RevenueManagement.deterministic_upper_bound). Neither has inventory, an LP subroutine, or lost sales. A formal proof here would supply the first machine-checked analysis of Thompson sampling under resource constraints and would check the paper's constants.

Difficulty

In an unconstrained bandit, Thompson sampling's regret reduces to a sum of per-period gaps between an upper confidence bound and the sampled reward, because the sampled optimal arm and the true optimal arm are identically distributed given the history. Here the action is a randomized mixture $x(t)$ from an LP, the reward is not additive in the prices chosen, and revenue is lost when inventory runs out. Two quantities must be controlled: the revenue the algorithm would collect if all demand could be served, and the revenue lost to stock-outs. The second depends on the random time at which each resource is exhausted under a pricing rule that was optimized for a sampled, not the true, demand, and on an arbitrary fulfilment rule once some resource is empty. Standard bandit arguments do not bound such lost sales, which are a nonlinear function of the whole trajectory.

Formalization scope

Lean representation. Products, resources and price vectors are indexed by Fin N, Fin M, Fin K; the posted price is an Option (Fin K) with none the shut-off price. Periods are 0-based ($t=0,\dots,T-1$ stands for the paper's $1,\dots,T$). $\Theta$ is a standard Borel space with a probability measure $\mu_0$; demand is a Markov kernel $F$ from $\Theta\times$Fin K to $\mathbb R^N$, bounded in $[0,\bar d_i]$ for every parameter. A run of TS-fixed is a family of random variables on a probability space satisfying, almost surely and via conditional expectations: $\theta\sim\mu_0$; the posterior-sampling property of $\theta(t)$ given everything before period $t$; the price draw with probabilities $x(\theta(t))$ for a measurable optimal LP selection $x$; the demand law given the past, $\theta(t)$ and the posted price; and fulfilment rules (a)/(b). The logarithm is natural. Prices, consumption and inventory are nonnegative (implicit in the paper). $\mathrm{OPT}(d)$ is a supremum over a nonempty bounded feasible set, so it has no junk value.

Corrections to the printed statement.

1. $K\ge2$ is added. At $K=1$ the printed right-hand side is $0$, yet on a one-price instance with Bernoulli$(0.8)$ demand, $I=T/2$ and a point-mass prior, TS-fixed loses about $0.2p\sqrt T$ in expectation.
2. The LP benchmark replaces $\mathbb E[\mathrm{Rev}^*(T)]$. Section 3.1.1 bounds $\mathbb E[\mathrm{Rev}^*(T)\mid d]$ by $\mathrm{OPT}(d)\cdot T$, citing Gallego–van Ryzin. Under the paper's fulfilment rule this fails when products use disjoint resources: with two products, $I=(T,1)$, $p_1=(1,0)$, $p_2=(1/2,0)$ and deterministic demand $(1,1)$, the known-$\theta$ policy earns at least $T$ while $\mathrm{OPT}(d)\cdot T=1$. The paper states that its proof bounds the gap to "the LP benchmark defined in Section 3.1.1" (p. 1594), and the last display of Section 3.1.1 bounds $\mathrm{BayesRegret}(T)$ by exactly $\mathbb E[\mathrm{OPT}(d)]\cdot T-\mathbb E[\mathrm{Rev}(T)]$. Wherever the Gallego–van Ryzin bound holds, the corrected goal implies the printed one.

Ruled out. A bound for the "ideal" revenue $\sum_iD_i(t)P_i(t)$ instead of the satisfied revenue, or for an arbitrary policy whose prices are merely close to the LP solution, is not Theorem 1; the goal carries the full TS-fixed run and the lost-sales accounting.

Infrastructure needed. Posterior-sampling identities for general (standard Borel) priors, a Hoeffding/Azuma-type concentration for bounded demand along the price-selection process, LP sensitivity with respect to the mean-demand matrix, and a pathwise bound on lost sales under an arbitrary fulfilment rule. The LP and fluid-benchmark definitions are reusable for later missions on TS-update (Theorem 2), contextual pricing (Theorem 4) and bandits with knapsacks (Theorem 5). Contributions welcome: proofs of the goal, and formal statements of the online appendix's lemmas.

Selected references

• K. J. Ferreira, D. Simchi-Levi, H. Wang, Online Network Revenue Management Using Thompson Sampling, Operations Research 66(6):1586–1602, 2018. https://doi.org/10.1287/opre.2018.1755
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
• O. Besbes, A. Zeevi, Blind Network Revenue Management, Operations Research 60(6):1537–1550, 2012. https://doi.org/10.1287/opre.1120.1057
• A. Badanidiyuru, R. Kleinberg, A. Slivkins, Bandits with Knapsacks, FOCS 2013. https://arxiv.org/abs/1305.2545
• S. Bubeck, C.-Y. Liu, Prior-free and Prior-dependent Regret Bounds for Thompson Sampling, NeurIPS 2013. https://arxiv.org/abs/1311.0466
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 36. https://doi.org/10.1017/9781108571401

Motivation

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the $k$-server problem all fit into this framework. The paper's first main result is that every deterministic on-line algorithm on an $n$-state metrical task system has competitive ratio at least $2n-1$, and that $2n-1$ is attained. The lower bound comes from an adversary that always charges the state the algorithm currently occupies. That adversary needs to know the algorithm's state, which suggests that randomization can help.

Section 7 of the paper makes this precise for the simplest system, the uniform task system, in which all transitions cost $1$. There the randomized competitive ratio against an oblivious adversary is between $H(n)$ and $2H(n)$, where $H(n)=1+\tfrac12+\cdots+\tfrac1n$ is between $\ln n$ and $1+\ln n$. This was the first logarithmic bound for a task system.

Timeline:

• 1985: Sleator and Tarjan introduce competitive analysis for list update and paging (CACM 28(2)).
• 1987/1992: Borodin, Linial and Saks define metrical task systems, prove the deterministic ratio $2n-1$, and prove $H(n)\le\bar w\le 2H(n)$ for the uniform system (conference version STOC 1987; journal version cited above).
• 1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the analogous $2H_k$ upper bound for randomized paging (J. Algorithms 12(4)).

Setting

A task system $(S,d)$ is a finite set $S$ of $n$ states with a transition-cost matrix $d$: $d(i,i)=0$, $d(i,j)>0$ for $i\ne j$, and $d(i,k)\le d(i,j)+d(j,k)$. In the uniform task system, $d(i,j)=1$ for all $i\neq j$. A task is a vector $T\in\mathbb R_{\ge0}^S$ of processing costs. Given an initial state $s_0$ and tasks $\mathbf T=T^1\cdots T^m$, a schedule is $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$, of cost

The off-line optimum $c_0(\mathbf T)$ is the least cost over all schedules.

A deterministic on-line algorithm chooses $\sigma(i)$ from $s_0$ and $T^1,\dots,T^i$. A randomized on-line algorithm $R$ chooses $\sigma(i)$ at random, with a distribution that depends on $s_0$, on $T^1,\dots,T^i$ and on the states $\sigma(0),\dots,\sigma(i-1)$ already visited. The task sequence is fixed before any random choice is made (an oblivious adversary). With $\mathrm{pr}(\sigma\mid\mathbf T)$ the probability that $R$ follows $\sigma$, the expected cost is $\bar c_R(\mathbf T)=\sum_\sigma c(\mathbf T;\sigma)\,\mathrm{pr}(\sigma\mid\mathbf T)$. For $w>0$, $R$ is expected $w$-competitive if there is a constant $K$ with

for every finite task sequence and every initial state. The randomized competitive ratio $\bar w(S,d)$ is the infimum of all such $w$ over all $R$.

Formalization targets

Goal: Theorem 7.1

For the uniform task system on $n\ge1$ states,

Milestones

1. Upper bound (p. 759). Some randomized on-line algorithm is expected $2H(n)$-competitive on the uniform task system.
2. Lemma 7.2 (p. 759). Let $D$ be a distribution on infinite task sequences over a finite task alphabet, with $E(c_0(\mathbf T^j))\to\infty$, and let $m_j=\inf_A E(c_A(\mathbf T^j))$ over deterministic on-line algorithms. Then every achievable $w$ satisfies

3. $m_j\ge j/n$ (p. 760) when the tasks are independent uniformly random unit elementary tasks $U_s$ (cost $1$ in $s$, $0$ elsewhere).
4. Coupon collector (p. 760). For i.i.d. uniform states on $S$, the expected number of draws until every state has appeared is $nH(n)$.
5. Off-line cost (p. 760). Under the same distribution, $E(c_0(\mathbf T^j))\le j/(nH(n))+C$ for a constant $C$ independent of $j$.

Significance

The theorem shows that randomization reduces the competitive ratio of the uniform task system from $2n-1$ to $\Theta(\log n)$. That is an exponential improvement, and it identifies the adversary's knowledge of the algorithm's state as the source of the deterministic lower bound. Lemma 7.2 is a form of Yao's principle adapted to the additive-constant definition of competitiveness. It is the standard tool for randomized lower bounds in on-line computation, and the same argument shape reappears for paging and $k$-server lower bounds.

On the formalization side, the result is proved but, as far as is known, has not been machine-checked. A complete development yields a reusable model of randomized on-line algorithms with oblivious adversaries, a Yao-type lemma usable for other on-line problems, and a coupon-collector expectation in the product-measure setting. The upper half additionally needs the continuous-time reduction of the paper's Lemma 3.1 in randomized form, or a direct discrete-time algorithm.

Difficulty

For the upper bound, the natural algorithm is continuous-time. It proceeds in phases, and inside a phase it stays in a state until that state has accumulated cost $1$. A discrete task can saturate several states at once and straddle a phase boundary. So a discrete algorithm must either simulate the continuous one or be analyzed directly, and the expected transition count per phase must be controlled with the first phase starting in a deterministic state.

For the lower bound, the first obstacle is that the natural statement "$\bar w\ge\limsup m_j/E(c_0)$" silently assumes that a randomized algorithm's expected cost, averaged over random inputs, is at least that of the best deterministic algorithm. With the behavioural (kernel) definition used here, this requires converting a kernel into a mixture of deterministic algorithms, which is Kuhn's theorem on each finite horizon. The second obstacle is that the paper's claim $E(c_0(\mathbf T^j))\le j/(nH(n))+O(1)$ is supported only by the elementary renewal theorem, which gives a limit of ratios; the additive bound needs a sharper renewal estimate. Mathlib has no renewal theory. The hypothesis $E(c_0(\mathbf T^j))\to\infty$ of Lemma 7.2 must also be established for the uniform distribution; the paper does not prove it separately.

Formalization scope

• States form a finite nonempty type S, and $n$ = Fintype.card S; no $n\ge2$ assumption is made (at $n=1$ the goal reads $1\le\bar w\le2$, and $\bar w=1$). $H(n)$ is Mathlib's harmonic n, cast to $\mathbb R$. The uniform system has unit transition cost.
• Tasks are finite and nonnegative. The paper also allows $+\infty$ entries; these are excluded. Task sequences are Fin m → S → ℝ and schedules are Fin (m+1) → S with σ 0 = s₀. $c_0$ is a finite minimum.
• A randomized algorithm is a kernel S → List (S → ℝ) → List S → PMF S. This is the paper's scheduler–taskmaster description (p. 758), equivalent to a distribution over deterministic algorithms on every finite task sequence. $\mathrm{pr}(\sigma\mid\mathbf T)$ is the product of kernel probabilities, and $\bar c_R$ is a finite sum. That $\mathrm{pr}(\cdot\mid\mathbf T)$ sums to $1$ has been checked locally.
• $\bar w(S,d)$ is the real sInf of $\{w : \exists R,\ R \text{ expected } w\text{-competitive}\}$. On the empty set this would be $0$, so the upper bound is stated as the existence of an expected $2H(n)$-competitive algorithm, and Lemma 7.2 is stated for every achievable $w$. The goal's lower half forces the set to be nonempty. Statements of the form "$\bar w\le c$" alone are therefore not acceptable substitutes for milestones 1 and 2.
• Lemma 7.2 is restricted to task sequences over a finite alphabet, with the product $\sigma$-algebra and measurable singletons. This makes every $E(c_A(\mathbf T^j))$ a genuine integral for every deterministic $A$, and it covers the paper's application. The $\limsup$ of Lemma 7.2 is taken in EReal.
• The coupon-collector time takes values in $[0,\infty]$ and its expectation is a lower Lebesgue integral. Milestone 5 renders the paper's $O(1)$ as an explicit constant $C$ chosen before $j$.

Contributions welcome: proofs of any milestone; a discrete-time randomized phase algorithm; a general Kuhn-type conversion from kernels to mixtures of deterministic algorithms; renewal-theoretic lemmas.

Selected references

• A. Borodin, N. Linial, M. Saks, An Optimal On-Line Algorithm for Metrical Task System, J. ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Commun. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• A. C.-C. Yao, Probabilistic Computations: Toward a Unified Measure of Complexity, FOCS 1977, 222–227. https://doi.org/10.1109/SFCS.1977.24
• S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970 (the elementary renewal theorem cited as [20] in the paper).

Motivation

The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The subtour-elimination relaxation (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the integrality gap of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$; the best proven upper bound sits just barely below $3/2$. The 4/3 conjecture — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades.