Probability

Motivation

In the prophet inequality a gambler observes independent nonnegative random values $V_1,\dots,V_n$ with known laws one at a time and must decide irrevocably, after seeing each one, whether to stop and keep it. Her expected reward is compared with that of a prophet who knows all realizations and earns $\mathbb E(\max_i V_i)$. When the values arrive in a fixed adversarial order the best guarantee is $1/2$ (Krengel, Sucheston and Garling, 1977; Samuel-Cahn, 1984). Prophet inequalities are the stopping-theoretic core of posted-price mechanisms in online auctions, where a guarantee for the gambler translates into a welfare or revenue approximation for sequential pricing.

The prophet secretary problem keeps arbitrary independent laws but lets the values arrive in a uniformly random order, as in the secretary problem.

• 2015: Esfandiari, HajiAghayi, Liaghat and Monemizadeh introduce the problem and give a $1-1/e\approx0.632$ guarantee with $n$ time-dependent thresholds (ESA 2015).
• 2017: Ehsani, Hajiaghayi, Kesselheim and Singla obtain $1-1/e$ with a single threshold, using random tie-breaking (SODA 2018).
• 2018: Azar, Chiplunkar and Kaplan surpass $1-1/e$ by a small margin and give an upper bound of $11/15$ for deterministic distribution-insensitive algorithms (EC 2018).
• 2019: Correa, Saona and Ziliotto break $1-1/e$, proving $0.669$ with blind strategies, and show that no algorithm beats $\sqrt3-1$ (arXiv:1807.07483; Mathematical Programming, doi:10.1007/s10107-020-01544-8). This mission formalizes the $0.669$ guarantee.

Setting

An instance is a list of laws $F_1,\dots,F_n$ of independent nonnegative random variables $V_1,\dots,V_n$, all continuous. A uniformly random permutation $\sigma$ of $[n]=\{1,\dots,n\}$, independent of the values, is the arrival order: at time $j$ the gambler sees $V_{\sigma_j}$.

The time threshold algorithm $\mathrm{TTA}_{\tau_1,\dots,\tau_n}$ stops at the first time $j$ with $V_{\sigma_j}>\tau_j$. Its stopping time is $T=\inf\{j\in[n]:V_{\sigma_j}>\tau_j\}$ and the gambler's reward is $V_{\sigma_T}\mathbf 1_{T<\infty}$, written $V_{\sigma_T}$.

A blind strategy is a nonincreasing function $\alpha:[0,1]\to[0,1]$. Given an instance, draw $u_1,\dots,u_n$ independently and uniformly from $[0,1]$, let $u_{[j]}$ be the $j$-th smallest, and choose thresholds by

$$\mathbb P\big(\max_{i\in[n]}V_i\le\tau_j\big)=\alpha(u_{[j]}).$$

The strategy is called blind because $\alpha$ fixes the levels of the distribution of the maximum at which the gambler stops, independently of the instance and of $n$. The deterministic blind strategy (Definition 3.1) uses $\alpha(j/n)$ in place of $\alpha(u_{[j]})$. A piecewise-constant strategy $\alpha_{\alpha_1,\dots,\alpha_m}(x)=\sum_{j\in[m]}\alpha_j\mathbf 1_{[\frac{j-1}m,\frac jm)}(x)$ uses at most $m$ distinct levels.

Formalization targets

Goal: Theorem 1.1

There is a nonincreasing $\alpha:[0,1]\to[0,1]$ such that, for every $n$ and every continuous instance,

$$\mathbb E(V_{\sigma_T})\;\ge\;0.669\;\mathbb E\big(\max_{i\in[n]}V_i\big),$$

where $T$ is the stopping time of the blind strategy $\alpha$. One $\alpha$ serves every instance.

Milestones, in the order the proof uses them

1. §3, display after Definition 3.1: the blind strategy's value is the limit of the deterministic blind strategy's values on the instance padded with $m$ zeros, as $m\to\infty$.
2. Lemma 3.1: an exact formula for $\mathbb P(V_{\sigma_T}>t)$ for nonincreasing thresholds.
3. Lemma 3.3: $\frac1n\sum_{j\in[k]}(1-\alpha_j)\le\mathbb P(T\le k)\le1-(\prod_{j\le k}\alpha_j)^{1/n}$.
4. Lemma 4.1: $\mathbb P(T\ge k\mid\sigma_k=i)\ge\mathbb P(T>k)\big/\big(1-\frac kn+\frac1n\sum_{l\in[k]}\mathbb P(V_i\le\tau_l)\big)$.
5. Lemma 4.2: a weighted replacement of the union bound $\sum_i\mathbb P(V_i>t)\ge\mathbb P(\max_iV_i>t)$.
6. Lemma 4.3: for $\alpha=\alpha_{\alpha_1,\dots,\alpha_m}$ with $\alpha_m>0$, $\mathbb E(V_{\sigma_T})\ge\min_{j\in[m+1]}f_j(\alpha_1,\dots,\alpha_m)\,\mathbb E(\max_iV_i)$ for explicit functions $f_j$.
7. Corollary 4.4: some $1\ge\alpha_1\ge\dots\ge\alpha_m\ge0$ gives the constant $0.66975$; the paper reports that $m=30$ suffices.

Significance

Theorem 1.1 raised the guarantee for the prophet secretary problem from just above $1-1/e$ to $0.669$, and it separates random-order arrival from adversarial arrival by more than the classical single-threshold analysis. The strategies are distribution-insensitive in a precise sense: the gambler needs only the distribution of the maximum, not the individual laws, and $\alpha$ does not depend on $n$. The milestones are general facts about multi-threshold stopping in random order (Lemmas 3.1, 3.3, 4.1, 4.2) that apply to any nonincreasing thresholds, not only to blind ones.

The result is proved in the paper, with one numerical step: Corollary 4.4 evaluates the bound of Lemma 4.3 at a specific vector $(\alpha_1,\dots,\alpha_{30})$ found by optimization, which the paper does not print. No part of this argument has a machine-checked proof. The formalization would make the reduction from blind to deterministic strategies, the stopping-time estimates and the final numerical certificate explicit and checked. The paper also shows that no blind strategy guarantees more than $0.675$ (Theorem 1.2, outside this mission); any later improvement of the constant leaves this goal, which asserts only $0.669$, intact.

Difficulty

The obvious argument fixes a threshold and bounds the probability that some value exceeds it; with one threshold this cannot beat $1-1/e$, and with time-varying thresholds the events "the gambler has not stopped by time $k$" and "value $i$ arrives at time $k$" are dependent, because the arrival of $i$ at time $k$ removes $i$ from the earlier times. The union bound $\sum_i\mathbb P(V_i>t)\ge\mathbb P(\max_iV_i>t)$ loses exactly the constant one is trying to gain. The analysis must therefore bound the law of the stopping time uniformly over all instances (Lemma 3.3), sharpen the conditional survival probability (Lemma 4.1) and the union bound (Lemma 4.2), and then pass to the limit of large instances. The final constant depends on a numerical optimization over $m=30$ levels, so the closing step is a certified evaluation of an explicit but long expression involving $m$-th roots and logarithms.

Formalization scope

All statements import one definitions file, BlindProphetSec.Blind.Setting.

• Instances: μ : Fin n → Measure ℝ with IsProbabilityMeasure, NullSingletonClass (continuity, the paper's standing assumption of §1.2 and §3) and μ i (Set.Iio 0) = 0 (nonnegativity). Independence is built in: the values are the coordinates of Measure.pi μ. Indices and times are 0-based; the paper's time $j$ is j.val + 1.
• Random order: the average over all $n!$ permutations. A conditional probability $\mathbb P(\cdot\mid\sigma_k=i)$ is written $n\,\mathbb P(\cdot,\ \sigma_k=i)$.
• Expectations are lower Lebesgue integrals in $[0,\infty]$, so $\mathbb E(\max_iV_i)=\infty$ is allowed; the paper's ratios are stated multiplied out, $c\,\mathbb E(\max_iV_i)\le\mathbb E(V_{\sigma_T})$. The reward is $0$ if the gambler never stops.
• Thresholds of blind strategies are encoded through their levels: stop at time $j$ iff $\alpha(u_{[j]})<\mathbb P(\max_iV_i\le V_{\sigma_j})$. For continuous laws this agrees almost surely with $V_{\sigma_j}>\tau_j$ when the level is positive; level $1$ means "never stop", and at level $0$, where the paper's threshold is not unique, the encoding takes the largest threshold.
• Pinned hypotheses: $\mathbb E(\max_iV_i)<\infty$ in the §3 limit display; $t\ge0$ in Lemma 3.1 (the printed identity fails for $t<0$ because the reward is $0$ on $\{T=\infty\}$); $\alpha_1<1$ in Lemma 4.3, so that every term of $f_j$ is the paper's and none is a $0/0$ junk value.
• Generalizations: Lemmas 3.1, 4.1 and 4.2 are stated without continuity, and 4.1, 4.2 without nonnegativity, as printed.

A trivializing formalization is ruled out: the strategy $\alpha$ (and the vector $\alpha_1,\dots,\alpha_m$ of Corollary 4.4) is quantified before $n$ and the instance, the constants $0.669$ and $0.66975$ are exact rationals, and expectations cannot collapse to $0$ through non-integrability.

A complete development needs order statistics of uniform samples, exchangeability arguments for uniformly random permutations, convergence of the padded deterministic strategies, and a certified numerical evaluation of $f_j$. The random-order stopping vocabulary is reusable for other prophet secretary results, including the $\sqrt3-1$ upper bound of the companion mission. Contributions to any milestone, including partial results such as Lemma 3.2 ($\mathbb P(T\ge k\mid\sigma_k=i)\ge\mathbb P(T>k)$), are welcome. The PDF used is the arXiv preprint, version 2 (arXiv:1807.07483v2, 12 March 2019); all labels and pages refer to it.

Selected references

• J. Correa, R. Saona, B. Ziliotto, Prophet Secretary Through Blind Strategies, arXiv:1807.07483v2, 2019; Mathematical Programming, 2021. https://arxiv.org/abs/1807.07483, https://doi.org/10.1007/s10107-020-01544-8
• H. Esfandiari, M. Hajiaghayi, V. Liaghat, M. Monemizadeh, Prophet Secretary, Proceedings of ESA 2015, pp. 496–508.
• S. Ehsani, M. Hajiaghayi, T. Kesselheim, S. Singla, Prophet Secretary for Combinatorial Auctions and Matroids, Proceedings of SODA 2018, pp. 700–714.
• Y. Azar, A. Chiplunkar, H. Kaplan, Prophet Secretary: Surpassing the 1 − 1/e Barrier, Proceedings of EC 2018, pp. 303–318.
• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, The Annals of Probability 12(4), pp. 1213–1216.

Motivation

An agent that interacts repeatedly with an unknown Markov decision process must trade exploration against exploitation. The dominant design principle for provably efficient reinforcement learning has been optimism in the face of uncertainty: UCRL2 (Jaksch, Ortner & Auer, 2010) and REGAL (Bartlett & Tewari, 2009) build confidence sets around the unknown model and act according to the most favourable model in them. Computing that optimistic policy can be expensive, and confidence sets built separately for every state–action pair can be loose.

Posterior sampling for reinforcement learning (PSRL), proposed by Strens (2000), replaces optimism by randomization: at the start of each episode it samples one MDP from the posterior distribution and follows the optimal policy of that sample. It is the reinforcement-learning analogue of Thompson sampling for bandits. Osband, Russo & Van Roy (2013) gave the first regret guarantee for PSRL, and with it the first regret guarantee for an RL algorithm not based on optimism. Their argument transfers the Bayesian-regret analysis of Thompson sampling by Russo & Van Roy (2014) from bandits to MDPs.

Timeline:

• 2000: Strens proposes PSRL as a heuristic.
• 2010: Jaksch, Ortner and Auer prove $\tilde O(DS\sqrt{AT})$ regret for UCRL2 in non-episodic MDPs with diameter $D$.
• 2013: Osband, Russo and Van Roy prove the $O(\tau S\sqrt{AT\log(SAT)})$ Bayesian regret bound for PSRL in episodic MDPs, the result of this mission.

Setting

A finite-horizon MDP $M=(\mathcal S,\mathcal A,R^M,P^M,\tau,\rho)$ has $S$ states, $A$ actions and horizon $\tau$. Choosing action $a$ in state $s$ yields a reward drawn from a distribution $R^M_a(s)$ on $[0,1]$, with mean $\overline R^M_a(s)$, and moves the state to $s'$ with probability $P^M_a(s'\mid s)$. Every episode starts from a state drawn from the initial distribution $\rho$. A policy $\mu$ maps a state and a step $i\in\{1,\dots,\tau\}$ to an action, and its value is the expected total mean reward from step $i$ on,

$$V^M_{\mu,i}(s)=\mathbb E_{M,\mu}\Big[\sum_{j=i}^{\tau}\overline R^M_{a_j}(s_j)\,\Big|\,s_i=s\Big].$$

A policy is optimal for $M$ if it maximizes $V^M_{\mu,i}(s)$ for every $s$ and $i$; $\mu^M$ denotes a fixed choice of optimal policy for each $M$.

The true MDP $M^*$ is random with prior $f$. In episode $k$, PSRL samples $M_k$ from the posterior $f(\cdot\mid H_{t_k})$ given the history $H_{t_k}$ of all earlier states, actions and rewards, and follows $\mu_k=\mu^{M_k}$ for $\tau$ steps. With $\mu^*=\mu^{M^*}$, the regret of episode $k$ and the cumulative regret are

$$\Delta_k=\sum_{s}\rho(s)\big(V^{M^*}_{\mu^*,1}(s)-V^{M^*}_{\mu_k,1}(s)\big),\qquad \mathrm{Regret}(T,\pi^{\mathrm{PS}}_\tau)=\sum_{k=1}^{\lceil T/\tau\rceil}\Delta_k .$$

In Lean, MDPs are indexed by a parameter $\theta$ in a measurable space $\Theta$ (MDPFamily), the value is value F θ π j with 0-based steps, and the run is the structure PSRLRun.

Formalization targets

Goal: Theorem 1

There is an absolute constant $C>0$ such that, for all $S,A,\tau\ge1$, every prior $f$, every measurable optimal-policy selector, every PSRL run with $M^*\sim f$ and every $T$,

$$\mathbb E\big[\mathrm{Regret}(T,\pi^{\mathrm{PS}}_\tau)\big]\le C\,\tau S\sqrt{AT\log(SAT)} .$$

This is the paper's $O(\cdot)$ statement. It does not fix the constant, which the paper's appendix computes with errors.

Milestones, in the order of the proof

1. Lemma 1: given $H_{t_k}$, $M^*$ and $M_k$ have the same conditional law.
2. Theorem 2, (4): $\mathbb E[\sum_{k\le m}\Delta_k]=\mathbb E[\sum_{k\le m}\tilde\Delta_k]$, where $\tilde\Delta_k=\sum_s\rho(s)(V^{M_k}_{\mu_k,1}(s)-V^{M^*}_{\mu_k,1}(s))$.
3. Lemma 2, (5): the dynamic programming equation $V^M_{\mu,i}=\mathcal T^M_{\mu(\cdot,i)}V^M_{\mu,i+1}$.
4. (6): $\mathbb E[\tilde\Delta_k\mid M^*,M_k]$ equals the expected sum of one-step Bellman errors along the visited states.
5. (7): the pathwise split of $\sum_k\tilde\Delta_k$ on the event $\{M_k,M^*\in\mathcal M_k\}$.
6. $\mathbb P(M^*\notin\mathcal M_k)\le1/m$ for the paper's confidence sets (Lemma 17 of Jaksch et al.).
7. (8): $\mathbb E[\sum_k\tilde\Delta_k]\le(\tau+1)\,\mathbb E[\sum_k\sum_i\min\{\beta_k(s_{k,i},a_{k,i}),1\}]+2\tau$.
8. Appendix B: $\sum_k\sum_i\mathbf 1(N_{t_k}(s_{k,i},a_{k,i})\le\tau)\le2\tau SA$.
9. Appendix B: $\sum_k\sum_i\sqrt{\mathbf 1(N_{k,i}>\tau)/N_{k,i}}\le\sqrt{8SAm\tau}$.

Significance

Theorem 1 holds for every prior, with no assumption on the MDP class beyond finiteness and bounded rewards. It shows that a single posterior sample per episode, rather than an optimistic search over a confidence set, already achieves the $\sqrt T$ rate of the optimistic algorithms. The reduction it rests on (Lemma 1 and Theorem 2) applies to any problem in which the agent can sample from the posterior.

The theorem has a paper proof but, as far as is known, no machine-checked proof. A formalization adds three things. First, an exact model of the episodic Bayesian setting, with posterior sampling stated as a conditional law. Second, corrected versions of two steps: the factor in (8), which the page's argument does not justify as printed, and the square-root sum of Appendix B, which is false as printed. Third, reusable pieces: a path-defined finite-horizon value with its dynamic programming equation, a conditional-expectation form of the posterior-sampling identity, and deterministic counting lemmas for visit counts.

Difficulty

The proof combines three kinds of argument, each with its own obstacle in Lean.

• Conditioning. Lemma 1 and Theorem 2 identify conditional laws given the history. The history is a random element whose length grows with $k$, and the posterior-sampling assumption only speaks about indicators of $M_k$. Extending it to functions of $(M,H_{t_k})$ and applying the tower property needs care with sub-$\sigma$-algebras. The same issue appears in (8): the confidence event depends on $H_{t_k}$, so it is not measurable with respect to $\sigma(M^*,M_k)$, the $\sigma$-algebra on which (6) conditions. The working argument conditions on $(M^*,M_k,H_{t_k})$ instead.
• Concentration over adaptive counts. The bound $\mathbb P(M^*\notin\mathcal M_k)\le1/m$ needs an $L^1$ deviation inequality for empirical transition distributions (Weissman et al.) and Hoeffding's inequality for rewards. Both must hold uniformly over the random number of visits, which the agent's own behaviour determines. Applying the inequalities at a fixed number of samples is not valid, because the sample size is random.
• Counting. The appendix sums $N^{-1/2}$ along the visited pairs; the paper's chain loses a factor of $2$ at its integral comparison.

Formalization scope

• Model. States and actions are Fin S and Fin A. Steps and episodes are 0-based: Lean step j is the paper's step $j+1$, and Lean episode k is the paper's episode $k+1$, with $t_k=k\tau+1$. MDPs are a measurable family over a parameter space Θ: transition rows satisfy the published IsTransitionKernel, and reward laws are Markov kernels supported on $[0,1]$. The initial distribution $\rho$ is fixed. The value is defined from the state laws along the trajectory, not by the Bellman recursion.

• The run. PSRLRun consists of measurable random elements on a probability space. Posterior sampling, the reset from $\rho$, rewards and transitions are stated as conditional expectations of indicators. Three assumptions the paper leaves implicit are made explicit:

  • the state is reset from $\rho$ at every episode start;
  • the state reached after the last action of an episode is observed;
  • the sampling step uses fresh randomness.

  The optimal-policy selector is any measurable map that is optimal at every step.

• Constants and corrections. $O(\cdot)$ is one absolute constant, quantified before every other object; a constant that depends on $S$, $A$, $\tau$, the prior or $T$ would make the goal trivial, because the regret is at most $\lceil T/\tau\rceil\tau$. Milestone 7 uses the factor $\tau+1$, which the page's chain proves, where the page prints $\tau$, and milestone 9 uses $\sqrt{8SAm\tau}$ where the page prints the false bound $\sqrt{2SAT}$; both corrections are disclosed in the statements.

• Ruled out. The value is not defined by the recursion, which would make Lemma 2 definitional. Measurability is required, so the expectations are not junk zeros. The posterior-sampling clause concerns indicators of $M_k$ only, so it does not already contain Lemma 1.

• Needed infrastructure. Conditional expectations with respect to $\sigma$-algebras generated by random elements; finite-horizon Markov chain laws; Weissman's $L^1$ inequality and Hoeffding's inequality at random sample sizes; elementary bounds on $\sum_j j^{-1/2}$. The counting milestones (8, 9) and Lemma 2 are self-contained and a good place to start. Proofs of the conditioning steps (milestones 1, 2, 4) are reusable for any posterior-sampling analysis.

Selected references

• I. Osband, D. Russo, B. Van Roy, (More) Efficient Reinforcement Learning via Posterior Sampling, NIPS 2013; arXiv:1306.0940v5. https://arxiv.org/abs/1306.0940
• T. Jaksch, R. Ortner, P. Auer, Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11, 2010. https://jmlr.org/papers/v11/jaksch10a.html
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014; arXiv:1301.2609. https://arxiv.org/abs/1301.2609
• M. Strens, A Bayesian Framework for Reinforcement Learning, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000 (reference [16] of the paper).
• P. L. Bartlett, A. Tewari, REGAL: A Regularization Based Algorithm for Reinforcement Learning in Weakly Communicating MDPs, UAI 2009; arXiv:1205.2661. https://arxiv.org/abs/1205.2661
• T. Weissman, E. Ordentlich, G. Seroussi, S. Verdú, M. J. Weinberger, Inequalities for the L1 Deviation of the Empirical Distribution, HP Labs Technical Report HPL-2003-97, 2003.

Motivation

Stochastic dual dynamic programming (SDDP) and its relatives are the standard algorithms for multistage stochastic programs: hydro-thermal scheduling, energy storage and long-horizon capacity planning are solved with them in industry. They approximate each future cost function from below by a maximum of affine cuts, compute new cuts only at a few randomly chosen nodes of the scenario tree, and use the current approximations to simulate decisions forward. Whether such sampled cutting-plane schemes converge, and in what sense, decides whether their bounds can be trusted.

• Pereira and Pinto (1991) introduced SDDP for multistage stochastic linear programs.
• Chen and Powell (1999) proposed CUPPS, which samples a single scenario per iteration.
• Philpott and Guan (2008) proved almost-sure convergence in finitely many iterations of DOASA and SDDP-type methods for linear stage problems with stagewise independent data, using the finiteness of the set of possible cuts.
• Girardeau, Leclère and Philpott (2015) removed linearity: stage problems are convex with compact feasible sets, the data need not be stagewise independent, and the node selection is any τ-admissible random process. Convergence is then asymptotic, not finite.

This mission formalizes the stochastic part (§3) of the 2015 paper. Mission 1 of the series covers its deterministic part (§2).

Setting

A finite scenario tree has nodes $\mathcal N$, root $0$, parent map $p$, children $r(n)$, leaves $\mathcal L$, and node probabilities $\Phi_n>0$ with $\Phi_0=1$ and $\Phi_n=\sum_{m\in r(n)}\Phi_m$. Every node $m\neq0$ carries a control multifunction $\mathcal U_m:\mathbb R^d\rightrightarrows\mathbb R^p$, a cost $C_m(x,u)\in\mathbb R\cup\{+\infty\}$ and linear dynamics $x_m=f_m(x_{p(m)},u_m)$; every node carries a compact convex stock set $\mathcal X_n$; leaves carry final costs $V_m$. The future cost functions are defined backwards by (20):

$$V_n(x)=\sum_{m\in r(n)}\frac{\Phi_m}{\Phi_n}\min_{u\in\mathcal U_m(x)}\underbrace{C_m(x,u)+V_m\big(f_m(x,u)\big)}_{W_m(x,u)},\qquad x\in\mathcal X_n .$$

Assumptions $(H_2)$ ask for convex, lower semicontinuous, proper costs, convex compact-valued convex multifunctions $\mathcal U_m$, Lipschitz final costs, and an extended relatively complete recourse condition: feasibility and finite cost on a $\delta$-neighbourhood of every $\mathcal X_n$.

The algorithm keeps approximations $V^{k}_n$, starting from $V^{-1}_n\equiv-\infty$. At iteration $k$ it simulates the whole tree with $V^{k-1}$, producing stocks $x^k_n$ and controls $u^k_m$. Cuts $\theta^k_n+\langle\beta^k_n,\cdot-x^k_n\rangle$ are computed at the selected nodes by solving the stage problems (21) at their children and averaging optimal values and Lagrange multipliers with weights $\Phi_m/\Phi_n$. Every approximation is then updated by (22), $V^k_n=\max(V^{k-1}_n,\text{cut})$. The selections $y^k_n\in\{0,1\}$ form a random process. It is τ-admissible (Definition 1) when, inside each block of $\tau$ iterations, cuts are computed backwards along the tree, and when the block indicators $\tilde y^k_n=\max_{\kappa<\tau}y^{k\tau+\kappa}_n$ are i.i.d. in $k$, independent of the past, and equal to $1$ with positive probability.

Formalization targets

Goal: Theorem 3.1

Under $(H_2)$ and a τ-admissible selection process, almost surely, for every non-leaf node $n$ and every node $n$ respectively,

$$\lim_{k\to\infty}\sum_{m\in r(n)}\frac{\Phi_m}{\Phi_n}W_m\big(x^{k\tau}_n,u^{k\tau}_m\big)-V_n\big(x^{k\tau}_n\big)=0,\qquad \lim_{k\to\infty}V_n\big(x^{k\tau}_n\big)-V^{k\tau}_n\big(x^{k\tau}_n\big)=0 .$$

The decisions become optimal for the true problem and the approximations become exact at the visited stocks. Nothing is claimed about exactness elsewhere in the state space.

Milestones

• (26): every new cut is tight at the stock where it is computed.
• Lemma 3.1 (i)–(iii): the $V_n$ are convex and Lipschitz on $\mathcal X_n$; the approximations are lower bounds; finite approximations are uniformly Lipschitz.
• Lemma 3.2: exact approximations at the children make the decisions at a node asymptotically optimal.
• Lemma 5.3: under Definition 1 (i), a node selected inside a block is visited at the stock and with the approximation it had at the start of the block.
• Lemma 5.4: the terms of an i.i.d. sequence selected by a predictable rule are again i.i.d. with the same law.
• (32): exactness along the iterations at which a node is selected.

Significance

The theorem covers in one statement CUPPS (1-admissible), DOASA and SDDP ($(T-1)$-admissible), and many other sampling schemes, for stage problems that are convex rather than linear and for scenario trees without stagewise independence. It shows that the lower bound produced by these methods converges to the optimal value along the simulated trajectories.

The result is proved on paper. It is not formalized anywhere: no proof assistant library contains SDDP-type algorithms for convex stage problems. This mission makes the algorithm, the τ-admissibility notion and the convergence statement precise. Formalizing them corrects slips of the printed statements: the lower-bound property holds on the affine hull of $\mathcal X_n$ only, the boundedness of the cut slopes concerns finite cuts only, and the theorem's two limits concern different node sets. The rest of the work is the formalization of the published proof.

Difficulty

The deterministic argument (mission 1) shows exactness at stage $t$ from exactness at stage $t+1$ along the whole iteration sequence. In the stochastic case a node is updated only at the random iterations at which it is selected, while its stock $x^{k\tau}_n$ moves at every iteration. Exactness along the selected iterations (32) does not transfer to the others: a selection rule that updated a node only when its stock lay in a given region would leave the approximation inexact elsewhere. The proof has to show that the iterations at which the approximation is still $\varepsilon$-inexact are, by independence, selected with positive frequency. This requires the event "$k$ is $\varepsilon$-inexact" to be measurable with respect to the past selections, so the algorithm's choices among multiple minimisers and multipliers must be deterministic (footnote 6). It also requires the optional-skipping Lemma 5.4 and the strong law of large numbers. The first idea of conditioning on the stocks directly fails because the stocks depend on all past selections.

Formalization scope

• Spaces and values. Stocks in EuclideanSpace ℝ (Fin d), controls in EuclideanSpace ℝ (Fin p). Costs and value functions take values in EReal; convexity is epigraph convexity; $V_n=+\infty$ off $\mathcal X_n$; the initial approximation is $-\infty$. Limits are EReal limits, so convergence to $0$ forces the differences to be finite eventually.
• Tree. The platform definition StochasticProg.Multistage.Tree (a finite rooted tree with stages) is referenced; leaves, ascendents and node probabilities are defined on it. Costs are indexed by the child node as in (19a) and (20).
• Standing assumptions, all disclosed in the items: $(H_2)(1)$–$(6)$ clause by clause, with the full ball $B(\delta)$ of $(H_2)(6)$ as printed; $x_0\in\mathcal X_0$; $\Phi$ are node probabilities.
• Algorithm. A run is a predicate on the generated data (stocks, controls, cut values and slopes, approximations). Minimisers, Lagrange multipliers and subgradients are chosen by fixed rules, functions of the stage problem only (footnote 6), so a run is determined by its selection path. Lagrange multipliers of (21b) are encoded by the subgradient inequality of the optimal value of (21) on $\operatorname{Aff}(\mathcal X_n)$, with the multiplier in its direction space. The Lean index is shifted: Vc k is the paper's $V^{k-1}$.
• Selections. $y^k$ are measurable Bool-valued maps on a probability space; Definition 1 (i) holds on every path; (ii) is per node, i.i.d. in $k$ and independent of $\sigma(y^{k'}:k'<k\tau)$, with no independence across nodes.
• Ruling out trivializations. The goal's hypotheses are only $(H_2)$, the choice rules, a run on every sample path, measurable selections and τ-admissibility. The companion statement run_exists shows that runs exist for every selection path, and a sanity check shows $(H_2)$ and τ-admissibility are satisfiable, so the goal is not vacuous. Its conclusion mentions none of the proof's auxiliary objects.
• Infrastructure. The development needs marginal functions of convex problems over convex multifunctions, subdifferentiability of finite convex functions on affine hulls, Lipschitz bounds for maxima of affine functions, and the optional-skipping Lemma 5.4. Lemma 5.4 is a self-contained probability statement and is reusable on its own. Lemma 5.2 of the paper (a Dini-type lemma) is posed in mission 1. Proofs of any milestone, and of auxiliary lemmas on EReal-valued convex functions, are welcome.

Selected references

• P. Girardeau, V. Leclère, A. B. Philpott, On the Convergence of Decomposition Methods for Multistage Stochastic Convex Programs, Mathematics of Operations Research 40(1), 2015. https://doi.org/10.1287/moor.2014.0664 (author's version: https://hal.science/hal-01208295v1)
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4), 2008. https://doi.org/10.1016/j.orl.2008.01.013
• Z. L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, Journal of Optimization Theory and Applications 102(3), pp. 497–524, 1999 (reference [1] of the paper).
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895

Motivation

Systems of many particles that interact through a singular pair potential and are subject to independent noise appear in plasma physics (Coulomb interactions), in vortex models of fluids, in models of collective behaviour and in the analysis of training dynamics of wide neural networks. When the number of particles $N$ is large, the empirical measure of the system is expected to follow a deterministic nonlinear partial differential equation, the mean-field limit. For singular interactions the classical coupling arguments, which need Lipschitz forces, do not apply. The modulated-energy method of Serfaty (Duke Math. J. 2020) and its extensions by Duerinckx, Nguyen, Rosenzweig and Serfaty (NRS21, arXiv:2107.02592) give quantitative convergence for Riesz-type potentials $|x|^{-s}$, but with rates that degrade exponentially in time.

M. Rosenzweig and S. Serfaty (arXiv:2108.09878v1, 2021) show that additive noise improves this: the expected modulated energy grows at most polynomially in time for sub-Coulombic potentials (their Theorem 1.1, the subject of the first mission of this series), and stays bounded uniformly in time when the potential is globally superharmonic (their Theorem 1.2, the subject of this mission). Uniform-in-time propagation of chaos had been known for smooth or convex interactions; this result covers singular, non-gradient interactions on the whole space.

Setting

Fix $d\ge3$, an exponent $0\le s<d-2$, a diffusion strength $\sigma>0$ and a $d\times d$ matrix $\mathbb M$ with $\mathbb M\xi\cdot\xi\le0$ for all $\xi$. The particle system is

$$dx^t_i=\frac1N\sum_{j\ne i}\mathbb M\nabla\mathsf g(x^t_i-x^t_j)\,dt+\sqrt{2\sigma}\,dW^t_i,\qquad i=1,\dots,N,$$

started from pairwise distinct points $x^0_N=(x^0_1,\dots,x^0_N)$ and driven by independent standard Brownian motions $W_1,\dots,W_N$ in $\mathbb R^d$. The potential $\mathsf g$ is admissible: it satisfies ten assumptions (i)–(x) on symmetry, blow-up at $0$, superharmonicity near $0$, derivative bounds of order $|x|^{-s-k}$, a doubling property, a Fourier transform comparable to $|\xi|^{-(d-s)}$, an extension to $\mathbb R^{d+m}$ when $d-4<s$, a Calderón–Zygmund property in the cases $s=d-2k$, and $\mathbb M:\nabla^{\otimes2}\mathsf g\ge0$. The model case is $\mathsf g(x)=|x|^{-s}$.

The mean-field equation is

$$\partial_t\mu=-\operatorname{div}(\mu\,\mathbb M\nabla\mathsf g*\mu)+\sigma\Delta\mu,\qquad\mu|_{t=0}=\mu^0,$$

for a probability density $\mu^0\in L^\infty$, solved in the mild (Duhamel) sense in $C([0,\infty);L^1\cap L^\infty)$. Closeness of the empirical measure $\mu_N^t=\frac1N\sum_i\delta_{x^t_i}$ to $\mu^t$ is measured by the modulated energy

$$F_N(x_N,\mu)=\int_{(\mathbb R^d)^2\setminus\triangle}\mathsf g(x-y)\,d\Big(\frac1N\sum_{i=1}^N\delta_{x_i}-\mu\Big)^{\otimes2}(x,y),$$

where the diagonal $\triangle$ is removed. The potential is globally superharmonic if $\Delta\mathsf g\le0$ on all of $\mathbb R^d\setminus\{0\}$ ("$r_0=\infty$" in assumption (iii)).

Formalization targets

Goal: Theorem 1.2 for $0<s<d-2$

For globally superharmonic admissible $\mathsf g$ and every $d/(s+2)<p\le\infty$ there are $\beta_p>0$ (depending on $s,d,p$), $C>0$ (depending on $s,d,\sigma,\mathbb M,\mathsf g,\|\mu^0\|_{L^\infty}$), $C_p>0$ and $N_0$ such that for all $t\ge0$ and $N\ge N_0$,

$$\mathbb E\big(|F_N(x^t_N,\mu^t)|\big)\le C\big(|F_N(x^0_N,\mu^0)|+C_pN^{-\beta_p}\big).$$

The right side does not depend on $t$. The case $s=0$ of the paper's display (1.19) is not part of the goal (see Formalization scope).

Milestones

The proof combines an inequality for the time derivative of the expected modulated energy (Proposition 6.3), lower bounds for the energy and for the diffusion term (Remarks 5.10, 5.11, Proposition 5.12, Remark 5.13, Corollary 5.14), a commutator estimate for the transport term (Proposition 5.15), and decay of $\|\mu^t\|_{L^p}$ (Remark 3.4, Proposition 3.8), with the potential estimates of Lemma 2.3 and Remark 2.5.

Significance

A uniform-in-time bound means that the mean-field description is valid on time scales that do not shrink as the accuracy requirement grows. Combined with the control of negative Sobolev norms by the modulated energy, it yields uniform-in-time convergence in law of the empirical measure and, for chaotic initial data, uniform-in-time propagation of chaos at an explicit rate, for singular interactions such as sub-Coulombic Riesz gases with dissipative or conservative dynamics.

The result is proved in the paper. No part of it, nor of the modulated-energy method, is formalized in any proof assistant. A formalization would produce a reusable library: Riesz potentials and their $L^1$–$L^p$ interpolation, heat-type decay of nonlinear Fokker–Planck equations, smeared potentials and electric-energy lower bounds, renormalized commutator estimates, and a pathwise treatment of interacting diffusions with additive noise. The milestones are independent statements and can be proved separately.

Difficulty

The obvious Gronwall argument on the modulated energy fails twice. First, $F_N$ is not nonnegative; it is bounded below only up to errors involving $\|\mu\|_{L^\infty}$, and the lower bounds near the singularity need the smearing of point charges on spheres. Second, the error terms produced when the commutator and diffusion terms are bounded must be integrable on $[0,\infty)$; with the estimates of the general (local superharmonicity) case they grow linearly in time. Global superharmonicity removes an $\eta^2$ error term and lets every error carry a power of $\|\mu^t\|_{L^\infty}$, which decays like $(\sigma t)^{-d/2}$ by the Carlen–Loss method; for $s=0$ long-range effects still produce growth, which is why that case is excluded. Itô's formula cannot be applied directly to the singular energy and requires a truncation, whose stochastic integrals are removed in expectation only in the limit.

Formalization scope

All objects live in the Lean namespace RieszMF.Global and in one definitions module. Space is EuclideanSpace ℝ (Fin d); derivatives are iteratedFDeriv (operator norm), gradient and the Laplacian of Mathlib. The committed conventions:

1. Fourier conditions (vi) and (1.17) are read away from the origin: a function $\hat{\mathsf g}$ with $\int\mathsf g\,\mathcal F\varphi=\int\hat{\mathsf g}\varphi$ for Schwartz $\varphi$ vanishing near $0$.
2. Assumption (iv) has a constant $C_k$ for each $k$; quantities singular at $0$ are required for $x\neq0$ only; (ix) is stated componentwise with an $L^2$-bounded operator represented by the kernel off the support.
3. Global superharmonicity is $\Delta\mathsf g\le0$ on $\mathbb R^d\setminus\{0\}$, together with (1.15)–(1.16) on all of $\mathbb R^{d+m}\setminus\{0\}$ when $d-4<s$; (v) and (vii) keep a finite radius.
4. Doubling condition (vii) for $s>0$ is read as $\mathsf g(y)<c_s\mathsf g(x)$ whenever $|y|\ge2|x|$, $x\ne0$, with $c_s<1$. The page prints $\mathsf g(x)<c_s\mathsf g(y)$, which contradicts the blow-up (ii) and would leave no admissible potential, so the goal would hold vacuously. The model potential $|x|^{-s}$ satisfies the reading used here.
5. The particle system is the pathwise integral equation (no Itô integral is needed for additive noise), with continuous paths and no collisions almost surely; the Brownian family is $N\cdot d$ jointly independent standard real Brownian motions.
6. The mild formulation of (1.5) requires every integral to converge absolutely and continuity in $L^1\cap L^\infty$.
7. Expectations of $|F_N|$ are lower Lebesgue integrals, and Proposition 6.3 moves positive and negative parts across the inequality, so no integrability is presupposed and no $\infty-\infty$ arises.
8. Constants are quantified after exactly the objects they may depend on: $\beta_p$ after $s,d,p$; $C$ after $\sigma,\mathbb M,\mathsf g$ and $\|\mu^0\|_{L^\infty}$; $C_p$ and $N_0$ after $p$; all before $\mu^0$, $N$, the configuration, the probability space and $t$.

Restriction. The goal is Theorem 1.2 for $0<s<d-2$ only, where the paper's time factor $1+(t^{1/\sigma}\log(1+t))\mathbf 1_{s=0}$ equals $1$. For $s=0$ the proof yields a factor of order $t^{C/\sigma}$ rather than the printed $t^{1/\sigma}\log(1+t)$; the logarithmic case is covered by the first mission of this series.

Excluded trivializations. A statement in which $C$ is chosen after $\mu^0$, $N$ or the configuration, in which a divergent integral is read as $0$, in which the solution classes are empty, or which uses $N=0$ or a division by zero is not a formalization of the theorem; the statements here avoid each of these.

Contributions are welcome on any milestone, on the existence of solutions in the classes used (which shows the hypotheses are satisfiable), and on general infrastructure (Riesz potentials, sphere averages, heat-kernel estimates) that other missions can reuse.

Selected references

• M. Rosenzweig, S. Serfaty, Global-in-time mean-field convergence for singular Riesz-type diffusive flows, arXiv:2108.09878v1, 2021; Ann. Appl. Probab. 33(2), 2023. https://arxiv.org/abs/2108.09878
• Q.-H. Nguyen, M. Rosenzweig, S. Serfaty, Mean-field limits of Riesz-type singular flows, Ars Inveniendi Analytica, 2022. https://arxiv.org/abs/2107.02592
• S. Serfaty, Mean field limit for Coulomb-type flows, Duke Math. J. 169(15), 2020. https://doi.org/10.1215/00127094-2020-0019
• M. Duerinckx, Mean-field limits for some Riesz interaction gradient flows, SIAM J. Math. Anal. 48(3), 2016. https://doi.org/10.1137/15M1042620
• E. A. Carlen, M. Loss, Optimal smoothing and decay estimates for viscously damped conservation laws, with applications to the 2-D Navier–Stokes equation, Duke Math. J. 81(1), 1995. https://doi.org/10.1215/S0012-7094-95-08110-1

Motivation

Hotel rooms, rental cars, cloud servers, operating rooms and rental equipment are reusable resources: a customer occupies capacity for a fixed service time, and the capacity returns to the firm afterwards. Many of these settings also allow advance reservation, where a request made today is for a service that starts later. Lei and Jasin study dynamic pricing in this setting. Prices are posted period by period, demand is non-stationary, and the firm wants revenue close to the best achievable while never booking more units than it owns.

Classical network revenue management, where capacity is sold once and never returns, has an extensive asymptotic theory. In that literature, controls that re-solve or adjust a fluid (deterministic) plan are known to lose a vanishing fraction of the optimal revenue as demand and capacity grow (Gallego and van Ryzin 1997; Jasin 2014). Reusable resources break the standard argument, because each sale removes capacity for a window of time and not for the rest of the horizon. Lei and Jasin give the first control for reusable resources with non-stationary arrivals, deterministic service times and advance reservation whose average loss is $o(\theta^{-1/2})$ in the scale parameter $\theta$ (Lei and Jasin, Operations Research 2020).

Setting

A firm manages $I$ resource types with integer capacities $C_i \ge 1$ and sells $K \ge 1$ service types over periods $t = 1, \dots, T$. At most one request arrives per period. A type-$k$ request made at the beginning of period $t$ uses $a_{ik} \in \{0,1\}$ units of resource $i$ during periods $t+\ell_k, \dots, t+\ell_k+n_k-1$. Here $n_k$ is the service time and $\ell_k$ the reservation lead time.

In each period the firm chooses a demand-rate vector $\lambda^t \in \Omega_\lambda = [0,\lambda_U]^K$, which is equivalent to choosing prices. A type-$k$ request then arrives with probability $\lambda^t_k$, independently of the past given $\lambda^t$, and the expected revenue rate is $r^t(\lambda^t)$. The deterministic relaxation DET-H maximizes $\sum_{t=1}^T r^t(\lambda^t)$ over $\lambda^t \in \Omega_\lambda$, subject to

$$\sum_{k=1}^K \sum_{s \,:\, s+\ell_k \le t \le s+\ell_k+n_k-1} a_{ik}\lambda^s_k \le C_i \qquad \text{for every resource } i \text{ and period } t \le T.$$

Its optimal value $J^D_H$ bounds the optimal expected revenue, and the average loss of a control $\pi$ is $\mathcal{L}(\pi) = (J^D_H - \mathbf{E}[R^\pi])/T$. Let $\lambda^D$ be an optimal solution of DET-H. The quantity $\underline{n}_k$ is the smallest number of periods with $\lambda^{t,D}_k > 0$ inside any service cycle of type $k$ that carries positive demand.

The control DPC-B$(m,\epsilon)$ splits the horizon, for each type $k$, into adjacent batches $\mathcal{T}_k^b$, each with $m_k$ positive-rate periods. In period $t$ it posts

$$\lambda^t_k = \mathrm{Proj}_{[0,\lambda_U]}\Bigl[\lambda^{t,D}_k - \Bigl(\frac{\epsilon_k}{\underline{n}_k} + \frac{1}{m_k}\sum_{s \in \mathcal{T}_k^{\beta_k(t)-1}} (D^s_k - \lambda^s_k)\Bigr)\mathbf{1}\{\lambda^{t,D}_k > 0\}\Bigr],$$

where $\beta_k(t)$ is the batch containing $t$. The rate is set to $0$ when fewer than $a_{ik}$ units of some resource $i$ are free at the service start $t+\ell_k$. The buffer $\epsilon_k$ protects capacity, and the batch term corrects for the demand surprises of the previous batch.

Formalization targets

Goal: Theorem 3, display (8)

There is a constant $M_3>0$, depending only on $K$, the curvature constant $\Psi$ of Assumption A5 and a bound $R$ on $|r^t|$, such that for every instance, every valid batch partition with $m_k \le \underline{n}_k$ and every $\epsilon_k$ in the stated range,

$$\mathcal{L}(\text{DPC-B}(m,\epsilon)) \le M_3 \sum_{k=1}^K \Bigl[\frac{\epsilon_k}{\underline{n}_k} + \frac{1}{m_k} + \frac{T}{m_k}\exp\Bigl\{-\frac{(\min_j\epsilon_j-1)^2}{256K^2\min\{\max_i C_i, m_k\}}\Bigr\}\Bigr].$$

The constant is uniform in $T$, $C$, $n_k$, $\ell_k$, $m_k$ and $\epsilon_k$, which is what makes the bound informative.

Milestones

1. Lemma EC.3: on the good event $\mathcal{G}(\epsilon,m,\delta)$, the free capacity satisfies $C^t \succeq e$ and the corrected rates stay inside $(0,\lambda_U)$.
2. (EC.22): on $\mathcal{G}$, the posted rate equals the unprojected corrected rate.
3. Lemma EC.4, as proved in (EC.23): $\mathbf{P}(\bar{\mathcal{G}}) \le \sum_k \frac{4T}{m_k}\exp\{\min\{\max_i C_i, m_k\}\gamma_k^2 - \frac{\min_j\epsilon_j-1}{8K}\gamma_k\}$ for all $\gamma_k \in (0,1]$.
4. $\mathbf{E}[(\sum_{s\in\mathcal{T}_k^b}\Delta^s_k)^2] \le m_k$ for every batch.
5. $\mathbf{E}([\nabla r^t(\lambda^{t,D})]^\top(\eta^t_\delta\odot\eta^t_e)) = 0$.

A companion item states Lemma 2 in this setting: stretching $\lambda^D$ in time solves DET-H for the $\theta$-th system of display (7).

Significance

Along the scaling (7), Theorem 3 with $m_k \approx \underline{n}_k^{2/3}$ gives an average loss of $O(\theta^{-2/3}\log^{1/2}\theta)$. The non-adaptive control DPC of the same paper achieves $O(\theta^{-1/2}\log^{1/2}\theta)$ (its Theorem 1). The result shows that batch-level feedback improves on the square-root barrier for reusable resources, and it does so with heterogeneous service times and advance reservation, which cover car rental and hotel bookings.

Theorem 3 and its lemmas are proved in the paper's e-companion. No machine-checked proof of them, and no formal model of reusable-resource revenue management, is known. The mission produces a Lean model of the setting: capacity windows with lead times, the availability table $\tilde C(t,s)$, an adapted control on finite sample paths, and its exact path law. On top of that model it states the paper's main bound in full. Several printed steps need repair (see the scope section), so a formal proof would also settle the exact constants.

Difficulty

The obvious route bounds each period's loss by a Taylor expansion around $\lambda^{t,D}$ and controls the deviations by a martingale inequality. That route needs the control to coincide with the unprojected corrected rate for the whole horizon, that is, no capacity shortfall and no clipping. Capacity is a moving window of overlapping services with different lengths and lead times, so a shortfall at one period depends on requests made up to $n_k+\ell_k$ periods earlier, in other batches and other types. The batch correction makes the rates depend on past errors, so the errors are martingale differences, not independent variables. The concentration bound must hold uniformly over batches whose number grows with $T$, with a variance proxy $\min\{\max_i C_i, m_k\}$ that is not the batch length. The early periods, before any service of type $k$ has completed, need a separate threshold (the two cases of (EC.17)).

Formalization scope

All objects are defined in the namespace ReusablePricing.DPCB. The conventions are fixed as follows.

• Periods are $1,\dots,T$. A sample path is a function Fin T → Option (Fin K), recording no request or one request of a type in each period. Expectations are finite sums against the exact path law: the product over periods of the one-period law, whose probabilities are the rates posted given the past. The demand law is never left as a hypothesis.
• Decisions are rates. A turn-off is rate $0$. Prices and A1–A3 do not appear. The bound $R$ on $|r^t|$ over $\Omega_\lambda$ replaces the proofs' $r^u$. $K\lambda_U \le 1$ is assumed, as implied by at most one request per period.
• Capacity windows are empty for $t \le \ell_k$. $C^t = \tilde C(t,t)$, and $\tilde C$ is defined by its defining sentence on p. 18, not by the update rule of Step 2a, whose indices do not match its own explanation. Admission is tested for services starting within the horizon.
• $\underline{n}$ in (EC.17) is $\min_k\underline{n}_k$. The events of (EC.16) are read over the batches $\mathcal{T}_k^b$. Statements "on $\mathcal{G}$" are made on paths of positive probability.
• Lemma EC.4 is stated with the $8K$ that its proof establishes, not the printed $4K$.
• Goal statements carry every standing hypothesis of Section 6: optimality of $\lambda^D$, the convention $\lambda^{t,D}_k\in\{0\}\cup(0,\lambda_U)$, A4, A5, and the existence of a demand-carrying cycle for every type, which $\underline{n}_k$ presupposes. The sanity check exhibits instances, with and without lead time, where all hypotheses of Theorem 3 hold and the $\epsilon$-range is nonempty.

The constant $M_3$ is quantified before the instance, after only $K$, $\Psi$ and $R$. Choosing it after the instance would make the bound trivial, because the loss never exceeds $2R$.

A complete development needs Freedman- or Doob-type inequalities for bounded martingale differences on finite path spaces, second-order Taylor bounds for $C^2$ functions on boxes in $\mathbb{R}^K$, and window-counting lemmas for capacity. The first two are reusable well beyond this mission. Contributions of any of the milestones, of general martingale tools for finite adapted processes, or of a proof of the companion Lemma 2 are welcome.

Selected references

• Y. Lei and S. Jasin, Real-Time Dynamic Pricing for Revenue Management with Reusable Resources, Advance Reservation, and Deterministic Service Time Requirements, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1906 (author manuscript: SSRN 2816718, https://ssrn.com/abstract=2816718)
• G. Gallego and G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1276

Motivation

Hotel rooms, rental cars, cloud servers, hospital beds and event spaces are reusable resources: a customer occupies a unit for a while and then returns it. Pricing them differs from classical revenue management, where a sold unit is gone for good. A sale now blocks capacity only for the length of the service, so the binding constraint is how many services overlap at once. Lei and Jasin (Oper. Res. 2020) study dynamic pricing in this setting with deterministic service times and, in the general model, advance reservations. They measure a pricing control by its average loss against a deterministic (fluid) benchmark.

The paper has two main results. Theorem 1 bounds the loss of a static heuristic, the Deterministic Price Control DPC($\epsilon$). Theorem 3 bounds the loss of an adaptive variant and is treated in the companion mission (II). This mission formalizes Theorem 1, the lemmas its proof rests on (Lemmas EC.1–EC.2 and the displays (EC.14), (EC.15) of the e-companion), and two structural lemmas of the model: the fluid upper bound $J^* \le J^D$ (Lemma 1) and the scaling of the fluid solution (Lemma 2).

Setting

A firm manages $I$ resource types with integer capacities $C = (C_i) \succeq e$ and offers $J$ service types over periods $t = 1, \dots, T$. At most one request arrives per period. A type-$j$ request uses $a_{ij} \in \{0,1\}$ units of resource $i$ for $n$ consecutive periods (a service cycle), and $n$ divides $T$.

The firm posts a demand-rate vector $\lambda^t \in \Omega_\lambda = [0,\lambda_U]^J$ with $\lambda_U \le 1$. A type-$j$ request then arrives with probability $\lambda^t_j$, independently of earlier periods given the posted rates, and the firm earns the revenue rate $r^t(\lambda^t)$. Writing $D^s_j \in \{0,1\}$ for realized arrivals and $(x)^+ = \max\{1,x\}$, the capacity free at the beginning of period $t$ is

$$C^t = C - \sum_{s=(t-n+1)^+}^{t-1} A D^s .$$

The deterministic relaxation is

$$\mathbf{DET}:\quad J^D = \max\Big\{\sum_{t=1}^T r^t(\lambda^t) : \lambda^t \in \Omega_\lambda,\ \sum_{s=(t-n+1)^+}^{t} A\lambda^s \preceq C \ \ \forall t \le T\Big\},$$

with optimal solution $\lambda^D = (\lambda^{t,D})$. The revenue rates are strictly concave, bounded by $R$ in absolute value, and have interior maximizers (A4). Near $\lambda^{t,D}$ their gradients and Hessians are bounded by $\Psi$ (A5, with margins $\varphi_L, \varphi_U$).

The quantity $\underline n$ of display (2) is the smallest number of periods with $\lambda^{s,D}_j > 0$ in any service cycle that carries positive demand for some type $j$.

DPC($\epsilon$) posts, in period $t$, the rate $\lambda^{t,D}_j - (\epsilon/\underline n)\mathbf 1\{\lambda^{t,D}_j > 0\}$, clamped to $[0,\lambda_U]$, for every type $j$ with $C^t \succeq A^j$. It turns off every other type (rate $0$). The average loss of a control $\pi$ is $\mathcal L(\pi) = (J^D - \mathbf E[R^\pi])/T$.

Formalization targets

Goal: Theorem 1 (p. 13)

For $\epsilon \in \big(1, \min\{\min\{\varphi_L,\varphi_U\}\underline n,\ 6\min\{\max_i C_i, n\} + 1\}\big]$,

$$\mathcal L(DPC(\epsilon)) \le M_1\Big[\frac{\epsilon}{\underline n} + \frac{T}{n}\exp\Big\{-\frac{(\epsilon-1)^2}{36\min\{\max_i C_i, n\}}\Big\}\Big],$$

with $M_1 > 0$ depending only on $J$, $\Psi$ and $R$, and not on $T$, $C$, $n$, $\epsilon$ or the other data.

Milestones (EC.3)

1. Lemma EC.1. On the event $\mathcal G(\epsilon,\delta)$ that cumulative demand errors stay below $\delta = (\underline n-1)(\epsilon-1)/(3\underline n)$ within every cycle, $C^t \succeq e$ and $\lambda^{t,D}_j - \epsilon/\underline n \in (0,\lambda_U)$.
2. (EC.14). On $\mathcal G(\epsilon,\delta)$, DPC posts exactly $\lambda^{t,D}_j - (\epsilon/\underline n)\mathbf 1\{\lambda^{t,D}_j>0\}$.
3. (EC.15). $\mathbf E[\exp\{\pm\gamma\sum_{s\in\text{cycle }b}\Delta^s_j\}] \le \exp\{\min\{\max_i C_i,n\}\gamma^2\}$ for $\gamma \in (0,1]$.
4. Lemma EC.2. $\mathbf P(\bar{\mathcal G}(\epsilon,\delta)) \le (2JT/n)\exp\{\min\{\max_i C_i,n\}\gamma^2 - \delta\gamma\}$.
5. Step 2. $J^D - \mathbf E[R^{DPC(\epsilon)}] \le T\big(\Psi J\epsilon/\underline n + (4RJT/n)\exp\{\min\{\max_i C_i,n\}\gamma^2 - \delta\gamma\}\big)$.

Companion statements: Lemma 1 ($J^* \le J^D$ for every feasible non-anticipating control) and Lemma 2 (for integer $\theta \ge 1$, $\lambda^{\lceil t/\theta\rceil,D}$ solves the DET of the $\theta$-th system $T^{(\theta)} = \theta T$, $C^{(\theta)} = \theta C$, $n^{(\theta)} = \theta n$).

Significance

Along the scaling (1), choosing $\epsilon$ of order $\sqrt{\theta\log\theta}$ in Theorem 1 gives an average loss of $O(\theta^{-1/2}\log^{1/2}\theta)$. A control computed entirely before the selling horizon is therefore asymptotically optimal for reusable resources, with an explicit rate. This bound is the baseline against which the paper's adaptive control (Theorem 3, rate $O(\theta^{-2/3}\log^{1/2}\theta)$) is measured.

The proof shows a pattern common to fluid-based revenue management: a high-probability event on which the heuristic follows the fluid plan exactly, a martingale maximal inequality bounding the complement, and a Taylor bound for the cost of the buffer. Reusable resources add one ingredient: capacity is checked over sliding windows of length $n$.

The results are proved on paper; none is machine-checked. The formalization would provide a checked version of the model (sliding-window capacity, at most one arrival per period, turn-off), of the high-probability analysis, and of the uniform constant. The printed proof has slips that a checked proof must repair. In particular, the exponent obtained by EC.3's choice of $\gamma$ is $-\frac{\underline n-2}{\underline n}\cdot\frac{(\epsilon-1)^2}{36\min\{\cdot\}}$; it differs from the printed one by an amount that a larger $M_1$ absorbs.

Difficulty

The obvious argument says that DPC keeps an $\epsilon$ buffer, so it rarely runs out of capacity. The difficulty is that "rarely" has to hold uniformly over every sliding window of $n$ periods. The rates DPC posts are themselves random, because a type is turned off whenever the realized free capacity is short.

Lemma EC.1 breaks this circularity by induction over periods on a fixed event. A capacity window of length $n-1$ straddles two consecutive cycles, which costs a factor $3$ in $\delta$, and only the periods with positive deterministic demand carry a buffer, which is why $\underline n$ appears. The demand errors form a martingale-difference sequence with predictable, path-dependent rates, so (EC.15) needs a pathwise bound on the cumulative rate within a cycle. That bound comes from the DET constraint, not from independence.

Finally, the constant $M_1$ must not depend on the instance. A bound in which $M_1$ may depend on $T$ or $C$ is trivial, since the loss never exceeds $2R$.

Formalization scope

Everything is stated in demand rates, as the paper does for DET and in all its proofs. Prices, A1–A3 and the price-derivative part of A5 do not appear. A turned-off type has rate $0$.

A sample path is a function from $\{1,\dots,T\}$ to "no request" or "one request of type $j$". Its probability is the product of the per-period probabilities under the rates the control posts, so expectations are finite sums. Expected revenue is $\mathbf E[\sum_t r^t(\lambda^t)]$, the tower-property form of the proofs. Periods are $1,\dots,T$, and window sums whose upper limit falls below the lower limit are empty.

The standing hypotheses, bundled as Standing φL φU Ψ R n̲, are:

• $I, J, n, T \ge 1$, $n \mid T$, $a_{ij} \in \{0,1\}$ with a $1$ in every column, $C \succeq e$, $\lambda_U \in (0,1]$;
• $J\lambda_U \le 1$ (added: one arrival per period on all of $\Omega_\lambda$);
• $\lambda^D$ optimal for DET, with $\lambda^{t,D}_j \in \{0\} \cup (0,\lambda_U)$;
• A4 with the explicit bound $R$ on $|r^t|$, which replaces the paper's $r^u$;
• A5, with the Hessian condition as a bound on the quadratic form;
• $\underline n$ as in (2), stated as an attained minimum, so $\underline n \ge 1$;
• the cycle assumption of p. 11.

The statements "on $\mathcal G(\epsilon,\delta)$" are claimed for every path of positive probability in the event. Theorem 1 quantifies $M_1$ after $J$, $\Psi$, $R$ and before everything else. This rules out the trivial reading in which $M_1$ is chosen per instance. Step 2 uses $\underline n$ where the printed line has $n$, and $R$ for $r^u$. $\theta$ in Lemma 2 is an integer.

Two definition files carry the model: ReusablePricing.DPC.Model holds the instance, DET, A4–A5, $\underline n$ and the $\theta$-th system; ReusablePricing.DPC.Control holds the path law, DPC, loss, events and general controls. A complete proof needs a finite-path martingale toolkit: a Doob-type maximal inequality for exponential submartingales on a finite product space, and the Bernoulli moment-generating-function bound. It also needs a multivariate mean-value or Taylor estimate on a box and an induction over sliding capacity windows. The martingale tools are reusable beyond this mission. Contributions of those general lemmas, of proofs of individual milestones, and of the optional asymptotic corollary (4) are welcome.

Selected references

• Y. Lei and S. Jasin, Real-Time Dynamic Pricing for Revenue Management with Reusable Resources, Advance Reservation, and Deterministic Service Time Requirements, Operations Research 68(3), 2020. https://doi.org/10.1287/opre.2019.1906 (author manuscript: SSRN 2816718, https://ssrn.com/abstract=2816718)
• G. Gallego and G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1294
• D. Williams, Probability with Martingales, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9780511813658