Completed

Operations Research Optimization·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management III: Gaussian EMSR Protection Levels and Their SensitivityTextbook

Why protection levels and their inputs matter

An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.

This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.

Setting

Let $r$ be the number of requests for a fare class, a real random variable with law $\mu$ . For a seat level $S \in \mathbb R$ the tail probability is

\bar P(S) = P[r \ge S],

and for the fare $f$ of the class the expected marginal seat revenue is $\mathrm{EMSR}(S) = \bar P(S)\cdot f$ (Eqs. (6.1)–(6.2)).

There are two classes: class 1 with fare $f_1$ and class 2 with fare $f_2$ , where $0 < f_2 < f_1$ . Requests for class 1 are Gaussian with estimated mean $\bar r$ and estimated standard deviation $\hat\sigma > 0$ , written $r_1 \sim N(\bar r, \hat\sigma^2)$ . A real number $S$ is an EMSR protection level for class 1 against class 2 when

\bar P_1(S) = P[r_1 \ge S] = \frac{f_2}{f_1} \qquad \text{(Eq. (6.10))}.

The standardized level $Z$ is the value "which has a probability of $f_2/f_1$ of being exceeded" by a standard normal variable:

P[N(0,1) \ge Z] = \frac{f_2}{f_1}.

In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.

Formalization targets

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$

For $\hat\sigma > 0$ and $0 < f_2 < f_1$ :

Eq. (6.10) has exactly one solution $S$ , and the standard normal equation has exactly one solution $Z$ ;
they satisfy

S = \bar r + Z\hat\sigma \qquad \text{(Eq. (6.12))};

$Z < 0$ if $f_2/f_1 > 1/2$ , $Z > 0$ if $f_2/f_1 < 1/2$ , $Z = 0$ if $f_2/f_1 = 1/2$ (Eq. (6.14)), and $S = \bar r$ in the last case;
if $\hat\sigma' > \hat\sigma$ and $S'$ solves (6.10) for $N(\bar r, \hat\sigma'^2)$ , then $S' < S$ , $S' > S$ or $S' = S$ according as $f_2/f_1$ is above, below or equal to $1/2$ .

The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.

Milestones, in attack order

Eq. (6.1)–(6.2): for any request law, $\bar P$ and $\mathrm{EMSR}$ are non-increasing in $S$ .
Eq. (6.10): the Gaussian protection level exists and is unique.
Eq. (6.11)–(6.12): $S = \bar r + Z\hat\sigma$ .
p. 154: with $\hat\sigma$ and the fares fixed, replacing $\bar r$ by $\bar r + c$ replaces $S$ by $S + c$ .
Eq. (6.14): the sign of $Z$ , and $S = \bar r$ at fare ratio $1/2$ for every $\hat\sigma$ .
p. 154: the effect of $\hat\sigma$ on $S$ (part 4 of the goal on its own).
p. 157: $Z$ and $S$ decrease strictly as the fare ratio $f_2/f_1$ increases.

The dissertation's constant-coefficient-of-variation form, Eq. (6.13), $S = \bar r(1 + Zk)$ with $k = \hat\sigma/\bar r$ , follows from (6.12) by substitution and is not stated separately.

Significance

The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.

All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto $(0,1)$ . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.

Difficulty

Most of the work is in the existence and uniqueness of the two tail solutions. The tail $S \mapsto P[r_1 \ge S]$ must be shown continuous, strictly decreasing, and to take every value in $(0,1)$ . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation $S = \bar r + Z\hat\sigma$ then requires transporting the tail of $N(\bar r,\hat\sigma^2)$ to that of $N(0,1)$ through the affine map $x \mapsto (x - \bar r)/\hat\sigma$ , and the sign of $Z$ requires the symmetry of $N(0,1)$ , namely $P[N(0,1) \ge 0] = 1/2$ . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading $S = \bar r + Z\hat\sigma$ as a definition is ruled out below.

Formalization scope

Continuous seats. Protection levels and $Z$ are real numbers, as in the dissertation's own Gaussian example ( $Z = -0.675$ at fare ratio $0.75$ ). This differs from the first two missions of the series, which count seats in $\mathbb N$ . For a continuous law $P[r \ge S] = P[r > S]$ , so the two definitions of $\bar P$ the dissertation uses (Eq. (5.2) and Eq. (6.2)) coincide here.
Gaussian law. $N(\bar r, \hat\sigma^2)$ is Mathlib's gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes $\hat\sigma > 0$ ; at $\hat\sigma = 0$ the law is a Dirac mass and (6.10) has no solution.
Fares. $0 < f_2 < f_1$ , so $f_2/f_1 \in (0,1)$ . This is the dissertation's " $f_2 < f_1$ " together with positive fares.
Relational sensitivity. The sensitivity statements compare any two solutions of (6.10) under the two input values. Together with uniqueness, this is the same as monotonicity of the solution map. No function is defined by a choice operator.
Tail as a real number. $\bar P(S)$ is the measure of $[S,\infty)$ as a real number. The law is a probability measure, so nothing is truncated.
No trivialization. $S$ is defined only by the tail equation (6.10) for $N(\bar r, \hat\sigma^2)$ , and $Z$ only by the tail equation for $N(0,1)$ . Neither is defined by the formula $S = \bar r + Z\hat\sigma$ , which would make Eq. (6.12) true by definition.
Not covered. The revenue optimality of the level defined by (6.10) belongs to the second mission. The multi-class EMSR rules (5.19)–(5.29) are not optimal for three or more classes and are not stated. The empirical analysis of Sect. 6.1 is out of scope.

Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987. (no DOI; the source PDF of this mission).
P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4:111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

9 thms2 active usersReviewed

Completed

Machine Learning Reinforcement Learning·Captain: mikedeng1

Minimax Regret Bounds for Reinforcement Learning I: High-Probability Regret Bound for UCBVI with a Chernoff–Hoeffding BonusResearch Paper

Motivation

An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from $S$ to $\sqrt S$ in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.

The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon $H$ , state count $S$ , action count $A$ , and total interaction time $T$ . Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.

Setting

The state set $\mathcal S$ and action set $\mathcal A$ are finite and nonempty, with cardinalities $S$ and $A$ . A stationary transition kernel $P(y\mid x,a)$ gives the probability of moving to state $y$ after action $a$ in state $x$ ; each row is nonnegative and sums to one. The known, deterministic reward $R(x,a)$ lies in $[0,1]$ . An episode lasts $H\ge1$ steps. The environment chooses its starting state $x_{k,1}$ before episode $k$ and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.

A policy $\pi$ selects an action from the current state and the step number. Its value $V_h^\pi(x)$ is the expected sum of rewards from step $h$ through step $H$ when starting in state $x$ . The terminal value is $V_{H+1}^\pi=0$ , and $V_h^*(x)$ is the maximum of $V_h^\pi(x)$ over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing $H-h$ rewards uses a shifted terminal convention; this series follows the $H$ reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.

At the start of episode $k$ , UCBVI-CH forms visit counts $N_k(x,a,y)$ and $N_k(x,a)$ from earlier completed transitions. On a visited pair it uses the empirical row $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$ . Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, $Q_{k,h}(x,a)$ is the minimum of the preceding episode's $Q_{k-1,h}(x,a)$ , $H$ , and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, $Q_{k,h}(x,a)=H$ . A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.

Formalization targets

Theorem 1: UCBVI-CH regret

For $K$ episodes and $T=KH$ , regret sums the gap $V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})$ . The goal is the paper's printed bound, with its constants:

\Pr\!\left\{\operatorname{Regret}(K)>20H^{3/2}L\sqrt{SAK}+250H^2S^2AL^2\right\}\le\delta, \qquad L=\ln(5HSAT/\delta),\quad \delta>0.

Algorithm 3 itself uses $L_{\rm alg}=\ln(5SAT/\delta)$ in its bonus $7HL_{\rm alg}/\sqrt{N_k(x,a)}$ . Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.

Supporting results

Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.

Significance

Theorem 1 gives a finite-sample failure probability with explicit dependence on $H,S,A,K$ and $\delta$ . It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is $\widetilde O(H\sqrt{SAT})$ . This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.

Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.

Difficulty

The visit count $N_k(x,a)$ is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's $Q$ estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.

Formalization scope

States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. $V^*$ is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.

Lean uses steps $0,\dots,H-1$ and terminal index $H$ in place of the paper's algorithmic $1,\dots,H+1$ . The appendix sometimes puts the terminal value at $H$ . The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is $4H^2L$ , as required by (34)–(36), whereas Appendix B.1 prints $2H^2L$ . The proof's correction term $c_4$ dominates its other terms under $A\ge2$ , which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and $\delta\le1$ , the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.

The goal retains Theorem 1's constant $20$ . Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.

Selected references

M. G. Azar, I. Osband and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Pinned preprint.

9 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Secretary Problems: Weights and Discounts 4: A Threshold Rule Earns Z/4 for Any Z ≤ E[OPT] in the Discounted Secretary ProblemResearch Paper

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.

Timeline of the setting:

Dynkin (1963) introduced the classical problem; the rule "observe a $1/e$ fraction, then accept the first record" selects the best candidate with probability tending to $1/e$ .
Rasmussen and Pliska (1975/76) and Mahdian, McAfee and Pennock (2008, personal communication cited by the paper) studied secretary problems with specific "well-behaved" discount functions such as $d(t)=\beta^t$ .
Babaioff et al. (2009) treat an arbitrary discount function $d$ . Without prior knowledge, no algorithm is better than $\Omega(\log n/\log\log n)$ -competitive (their Theorem 4.3), and $O(\log n)$ is achievable (Theorem 4.4). If the algorithm knows a good estimate $Z$ of the expected offline optimum, a single threshold rule recovers a constant fraction (Theorem 4.7, headlined as Theorem 1.2). This mission formalizes that last result.

Setting

There are $n\ge1$ elements, indexed by $\mathrm{Fin}\,n$ . Element $e$ has a value $v(e)\ge0$ , and each time $t\in\{1,\dots,n\}$ has a discount $d(t)\ge0$ . The elements arrive in a uniformly random order $\pi$ , a bijection from times to elements: element $\pi(t)$ arrives at time $t$ . Selecting the element that arrives at time $i$ earns $d(i)\,v(\pi(i))$ , and an algorithm selects at most one element.

The offline optimum on the order $\pi$ is $\mathrm{OPT}(\pi)=\max_{i=1}^n d(i)\,v(\pi(i))$ . It is a random variable, and the benchmark is its expectation

\mathbf E[\mathrm{OPT}]=\sum_{\pi\in S_n}\frac1{n!}\max_{i=1}^n\{d(i)\,v(\pi(i))\}.

For a real parameter $Z$ , algorithm $\mathcal A$ selects the first time $j$ at which $d(j)\,v(\pi(j))\ge Z/2$ and earns that product; if no time qualifies, it selects nothing and earns $0$ . It knows $Z$ and $d$ , sees the values one at a time, and never sees the future of $\pi$ . Its expected value is $\mathbf E[\mathcal A]=\sum_{\pi\in S_n}\frac1{n!}\,\mathcal A(\pi)$ .

The proof uses three derived objects:

the accepting permutations $S_{acc}=\{\pi:\max_i d(i)v(\pi(i))\ge Z/2\}$ , on which $\mathcal A$ selects something;
their contribution $L=\sum_{\pi\in S_{acc}}\frac1{n!}\max_i d(i)v(\pi(i))$ to $\mathbf E[\mathrm{OPT}]$ ;
for a time $i$ and an element $j$ , the set $G_{ij}$ of orders on which $\mathcal A$ selects $j$ at time $i$ . These are the orders with $\pi(i)=j$ and $d(k)v(\pi(k))<Z/2$ for every $k<i$ .

Formalization targets

Goal: Theorem 4.7

For every $n\ge1$ , all discounts $d\ge0$ , all values $v\ge0$ and every real $Z$ ,

Z\le\mathbf E[\mathrm{OPT}]\ \Longrightarrow\ \mathbf E[\mathcal A]\ \ge\ \frac Z4.

Taking $Z=\mathbf E[\mathrm{OPT}]$ gives $\mathbf E[\mathrm{OPT}]\le4\,\mathbf E[\mathcal A]$ , a $4$ -competitive algorithm when the expected optimum is known.

Milestones (in the order of the paper's proof, p. 8)

Eq. (4.1). If $Z\le\mathbf E[\mathrm{OPT}]$ then $L\ge Z/2$ .
Eq. (4.3). If $Z\le\mathbf E[\mathrm{OPT}]$ then

\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}\frac1n\,d(i)v(j)\ \ge\ \frac Z2.

Eq. (4.4). $\displaystyle\mathbf E[\mathcal A]=\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}d(i)v(j)\,\frac{|G_{ij}|}{|S_n|}$ .
Claim 4.8. For every $i,j$ with $d(i)v(j)\ge Z/2$ , $n|G_{ij}|\ge|S_n\setminus S_{acc}|$ ; and if $2|S_{acc}|\le n!$ then $2n|G_{ij}|\ge n!$ .

Significance

The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number $\mathbf E[\mathrm{OPT}]$ , or of any lower estimate $Z$ of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, $\mathbf E[\mathrm{OPT}]$ can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than $\sqrt2$ .

Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over $S_n$ as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.

Difficulty

The obvious argument fails when $\mathcal A$ rarely selects. $\mathcal A$ earns at least $Z/2$ whenever it selects anything, so $\mathbf E[\mathcal A]\ge\frac Z2\Pr[\mathcal A\text{ selects}]$ . That settles the case $\Pr[\mathcal A\text{ selects}]\ge1/2$ and nothing else: the probability of selecting can be tiny while $\mathbf E[\mathrm{OPT}]$ is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair $(i,j)$ with $d(i)v(j)\ge Z/2$ must be realized by $\mathcal A$ on a positive fraction of the orders.

Two points need care in a formal proof:

Eq. (4.2) rewrites $L$ as a sum over pairs weighted by the conditional probability that $d(i)v(j)$ is the highest product. It relies on a consistent tie-breaking rule, which the paper leaves implicit.
Claim 4.8 is a counting argument on $S_n$ . A map from the rejecting orders into $G_{ij}$ swaps element $j$ into position $i$ , and must be shown to be at most $n$ -to- $1$ and to land in $G_{ij}$ .

Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.

Formalization scope

Types. Times and elements are Fin n; the paper's time $t$ is the index $t-1$ . An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes $n\ge1$ , so the maximum over times is a genuine maximum (Finset.sup').
Expectations. Expectations over the uniform order are finite averages $\frac1{n!}\sum_\pi$ . No measure theory is used.
Values and constants. Values, discounts and $Z$ are real numbers, and the hypotheses $d\ge0$ , $v\ge0$ are explicit. The constant $1/4$ is the paper's. The bound is stated multiplicatively, $Z/4\le\mathbf E[\mathcal A]$ , never as a ratio.
Thresholds and ties. Every threshold is non-strict ( $\ge Z/2$ ), exactly as on pp. 7–8. $\mathcal A$ selects the first qualifying time, so it needs no tie-breaking. The tie-breaking remark at Eq. (4.2) concerns only the paper's intermediate identity (4.2), which is not a milestone.
Claim 4.8. Both inequalities are stated with cleared denominators. The second carries the proof's case hypothesis $2|S_{acc}|\le n!$ , which the paper uses in the same place ("at most half the permutations are in $S_{acc}$ ").
What is not this theorem. $\mathcal A$ is the online threshold rule with threshold $Z/2$ applied to $\pi$ as it unfolds. An algorithm that inspects the whole order, or that chooses its threshold after seeing the values, would make the bound trivial and is not this theorem.
Contributions welcome. Proofs of each milestone, including the counting argument of Claim 4.8. Lemmas on averages over Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009.
E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR 150:238–240, 1963.
W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3):279–289, 1975/76.
M. Mahdian, P. McAfee, D. Pennock, The secretary problem with durable employment, personal communication, 2008 (cited as [MMP08]).
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443.

6 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Secretary Problems: Weights and Discounts 2: An Ω(log n / log log n) Lower Bound on the Competitive Ratio of the Discounted Secretary ProblemResearch Paper

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least $1/e$ , so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time $t$ is worth $d(t)\,v(e)$ for a known discount function $d$ . Discounts model settings where a sale is worth more at some times than at others. The case $d(t)=\beta^t$ had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary $d$ . Its answer has two sides: an $O(\log n)$ -competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than $\Omega(\log n/\log\log n)$ -competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.

Setting

There are $n$ elements $e\in\{0,\dots,n-1\}$ with values $v(e)\ge 0$ , and a discount function $d$ on the times. The elements arrive in a uniformly random order $\pi$ : element $\pi(t)$ arrives at time $t$ . A randomized online stopping rule $A$ specifies, for each time $t$ and each sequence of values seen so far $h=(v(\pi(0)),\dots,v(\pi(t)))$ , a probability $p_t(h)\in[0,1]$ of stopping at $t$ if it has not stopped yet. Stopping at $t$ selects $\pi(t)$ and earns $d(t)\,v(\pi(t))$ ; the rule selects at most one element and may select none. The rule knows $n$ and $d$ , but it sees only values, only as they arrive, and it is not told which instance it is facing.

The expected value of $A$ is

\mathbb E[A]=\mathbb E_\pi\Bigl[\sum_t d(t)\,v(\pi(t))\,p_t(h_t)\prod_{s<t}\bigl(1-p_s(h_s)\bigr)\Bigr],

and the benchmark is the expected offline optimum

\mathbb E[\mathrm{OPT}]=\mathbb E_\pi\Bigl[\max_t d(t)\,v(\pi(t))\Bigr],

which is itself a random variable averaged over the order. $A$ is $\alpha$ -competitive on an instance when $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$ .

The hard family (§4.1.1 of the paper): fix an integer $c\ge1$ and put $L=c$ , $n=L^{4c}$ , $n_t=L^{2t}$ for $t\le 2c$ , and $K=n^2$ . The step discount is $d(j)=L^{-1}$ on the times $1\le j\le n_1$ and $d(j)=L^{-t}$ on $n_{t-1}<j\le n_t$ . The instance $\mathcal I_1$ has $n/n_1$ elements of value $K$ and the rest $0$ ; $\mathcal I_{t+1}$ is obtained from $\mathcal I_t$ by raising $n/n_{t+1}$ of its values $K^t$ to $K^{t+1}$ , so $\mathcal I_t$ has $n/n_t$ elements of value $K^t$ .

Formalization targets

Goal: Theorem 4.3 in the form its proof establishes

For every integer $c\ge1$ and every randomized online stopping rule $A$ for horizon $n=c^{4c}$ and the step discount,

\exists\,t\in\{1,\dots,2c\}:\qquad c\cdot\mathbb E[A(\mathcal I_t)]\ <\ 10\cdot\mathbb E[\mathrm{OPT}(\mathcal I_t)].

That is, no online rule is $c/10$ -competitive on all of $\mathcal I_1,\dots,\mathcal I_{2c}$ .

Milestones

Lemma 4.1: $\mathbb E[\mathrm{OPT}(\mathcal I_t)]\ge(1-1/e)K^tL^{-t}$ for $1\le t\le 2c$ .
Coupling step of Lemma 4.2's proof: for every rule and $1\le t<2c$ , the probability of stopping among the first $n_t$ arrivals drops by at most $1/L^2$ from $\mathcal I_t$ to $\mathcal I_{t+1}$ .
Lemma 4.2: a rule that is $c/10$ -competitive on $\mathcal I_1,\dots,\mathcal I_{2c}$ stops among the first $n_t$ arrivals of $\mathcal I_t$ with probability at least $t/c$ .
Theorem 4.3, asymptotic form: for $c\ge2$ and $n=c^{4c}$ , every rule has some $\mathcal I_t$ with

\frac1{40}\cdot\frac{\log n}{\log\log n}\cdot\mathbb E[A(\mathcal I_t)]<\mathbb E[\mathrm{OPT}(\mathcal I_t)].

Significance

The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the $e$ -competitive classical rule). Together with the paper's $O(\log n)$ upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between $\log n/\log\log n$ and $\log n$ up to constants, and it motivates the paper's known- $\mathrm{OPT}$ model (§4.2), where an estimate of $\mathbb E[\mathrm{OPT}]$ restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.

The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the $O(\log n)$ upper bound, and the $\sqrt2$ lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.

Difficulty

The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the $2c$ instances against each other. A rule that does well on $\mathcal I_t$ must commit early, within the first $n_t$ steps, yet the rule cannot distinguish $\mathcal I_t$ from $\mathcal I_{t+1}$ during those steps except with probability $L^{-2}$ . Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time $t$ depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on $\mathcal I_{t+1}$ and its late earnings are both small compared with $\mathbb E[\mathrm{OPT}(\mathcal I_{t+1})]$ , which uses $L\ge 2$ and that $K=n^2$ dwarfs $L^{2c}$ .

Formalization scope

Elements and times are Fin n, 0-based: index $j$ is the paper's time $j+1$ , so the paper's block $(n_{t-1},n_t]$ is the index range $[n_{t-1},n_t)$ . The random order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and every expectation over it is the finite average $\frac1{n!}\sum_\pi$ . Values and discounts are real.
Algorithms are the structure StoppingRule n: stopping probabilities $p_t(h)\in[0,1]$ indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that $p_t(h)$ depends only on $h_0,\dots,h_t$ . The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on $n$ and $d$ but not on the instance index.
OPT is $\mathbb E_\pi[\max_t d(t)v(\pi(t))]$ (a supremum over the finite type Fin n), and competitiveness is multiplicative, $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$ , never a quotient.
Constants. The goal uses the paper's constant $10$ (from "if $A$ is $c/10$ -competitive"); the asymptotic form uses $1/40$ , from $\log n/\log\log n\le 4c$ for $c\ge2$ , with the natural logarithm. $K=n^2$ , the value the paper suggests.
The construction ( $n$ , $n_t$ , $d$ , $K$ , $\mathcal I_t$ ) is fixed by explicit formulas in the definition file. A solver cannot choose the discount or the instances, and the goal is not stated for a restricted class of algorithms; a formalization that let the rule see the instance index or future values, or quantified only over threshold rules, would be a different and trivial or weaker theorem. For $c<10$ the goal is immediate, since $\mathbb E[A]\le\mathbb E[\mathrm{OPT}]$ and $\mathbb E[\mathrm{OPT}(\mathcal I_t)]>0$ ; the content lies in $c\ge10$ . The bound is stated only for the horizons $n=c^{4c}$ the paper constructs.
Needed infrastructure: counting arguments over permutations of Fin n (the probability that a set of $m$ elements misses the first $k$ positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135 (authors' full version, the one cited here: https://www.cs.jhu.edu/~mdinitz/papers/secretary.pdf)
E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR, 1963.
W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3), 1976.
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Correlated Equilibrium as an Expression of Bayesian Rationality II: Two-Person Correlated Equilibrium Distributions Are the Solutions of Linear InequalitiesResearch Paper

Motivation

A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.

That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.

Setting

Player 1 has a finite set $S^1$ of actions and player 2 a finite set $S^2$ . For $j \in S^1$ and $k \in S^2$ , $h^1_{jk}$ and $h^2_{jk}$ are the two players' payoffs at the action pair $(j,k)$ .

A correlated strategy pair is a pair of functions $f^1 : \Gamma \to S^1$ , $f^2 : \Gamma \to S^2$ on a finite probability space $(\Gamma, \mu)$ : a finite set $\Gamma$ with nonnegative weights $\mu(\gamma)$ summing to $1$ . Chance draws $\gamma$ and suggests the action $f^i(\gamma)$ to player $i$ . The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every $\varphi : S^1 \to S^1$ ,

\mathbb E\, h^1(\varphi(f^1), f^2) \le \mathbb E\, h^1(f^1, f^2),

and the analogous inequality holds for player 2 and every $\psi : S^2 \to S^2$ .

A distribution is a family $(p_{jk})_{j \in S^1, k \in S^2}$ with $p_{jk} \ge 0$ and $\sum_j \sum_k p_{jk} = 1$ . The distribution of a correlated strategy pair assigns to $(j,k)$ the probability $\mu\{f^1 = j,\ f^2 = k\}$ . A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.

In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k $= h^1_{jk}$ and p j k $= p_{jk}$ .

Formalization targets

Goal: Proposition 2.3

For every distribution $(p_{jk})$ : $(p_{jk})$ is a correlated equilibrium distribution if and only if

\sum_k \big(h^1_{jk} - h^1_{qk}\big)\, p_{jk} \ge 0 \quad \text{for all } j, q \in S^1, \tag{2.4}

\sum_j \big(h^2_{jk} - h^2_{jr}\big)\, p_{jk} \ge 0 \quad \text{for all } k, r \in S^2. \tag{2.5}

Milestones

Identification with distributions (Sect. 2, p. 4). A correlated strategy pair is a correlated equilibrium if and only if its distribution $p$ satisfies $\sum_j\sum_k p_{jk} h^1_{\varphi(j)k} \le \sum_j\sum_k p_{jk} h^1_{jk}$ for all $\varphi$ , and the analogous condition for player 2.
Conditioning on possible suggestions (proof of Prop. 2.3, p. 6). For a distribution, player 1's condition holds if and only if $H^1(q \mid j) \le H^1(j \mid j)$ for every suggestion $j$ of positive probability and every $q$ , where $H^1(q\mid j) = \sum_k h^1_{qk} p_{jk} / \sum_k p_{jk}$ ; likewise for player 2.
Player 1 gives (2.4): player 1's condition on $p$ is equivalent to (2.4).
Player 2 gives (2.5): player 2's condition on $p$ is equivalent to (2.5).

A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff $(5,5)$ .

Significance

The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution $p$ — into finitely many linear inequalities on $p$ alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating $|S^1|^2 + |S^2|^2$ linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".

Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.

Difficulty

The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given $p$ ; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability $\sum_k p_{jk}$ of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of $\gamma$ gives a stronger notion.

Formalization scope

Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs $H^1$ , $H^2$ use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.

A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on $p$ .

No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the $n$ -player generalization the paper alludes to.

Selected references

R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), 1–18. https://doi.org/10.2307/1911154
R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

6 thms2 active usersReviewed

Mathematical Physics·Captain: mikedeng1

The Intermediate Disorder Regime for Directed Polymers in Dimension 1+1: The Rescaled Partition Function Converges in Law to a Wiener ChaosResearch Paper

Motivation

A directed polymer in a random environment is a simple random walk whose paths are reweighted by a random field of energies. It is a basic model of disordered statistical mechanics, and in dimension $1+1$ it belongs to the Kardar–Parisi–Zhang (KPZ) universality class: at fixed temperature the free energy fluctuates on the scale $n^{1/3}$ and is expected to follow Tracy–Widom laws. Comets and Yoshida (Ann. Probab. 34 (2006)) showed that in dimension $1+1$ every positive inverse temperature $\beta$ lies in the strong disorder regime, where the normalised partition function tends to zero. At $\beta=0$ the polymer is simply the random walk.

Alberts, Khanin and Quastel (arXiv:1202.4398, Ann. Probab. 42 (2014)) identified the regime in between. If the inverse temperature is scaled as $\beta n^{-1/4}$ , the partition function neither concentrates nor vanishes: it converges in law to a universal random variable, a Wiener chaos in a space–time white noise. That variable is the solution at time $1$ , integrated in space, of the stochastic heat equation with multiplicative noise, whose logarithm is the Hopf–Cole solution of the KPZ equation. The theorem therefore connects discrete polymers to the continuum KPZ equation under weak, $n$ -dependent disorder, with no assumption on the environment beyond exponential moments.

Setting

The environment is a family $\omega=(\omega(i,x))_{i\ge1,\,x\in\mathbb Z}$ of i.i.d. real random variables on a probability space $(\Omega,Q)$ , with mean $0$ and variance $1$ . Write $\lambda(\beta)=\log Q\,e^{\beta\omega}$ . The polymer is the symmetric simple random walk $S$ on $\mathbb Z$ started at $0$ , independent of $\omega$ , under the uniform measure $\mathbf P$ on the $2^n$ step sequences. The energy of an $n$ -step path is $H_n^\omega(S)=\sum_{i=1}^n\omega(i,S_i)$ , and the point-to-line partition function is

Z_n^\omega(\beta)=\mathbf P\big[e^{\beta H_n^\omega(S)}\big].

The modified partition function replaces $e^{\beta\omega}$ by $1+\beta\omega$ : $\mathfrak z_n^\omega(\beta)=\mathbf P\big[\prod_{i=1}^n(1+\beta\,\omega(i,S_i))\big]$ .

On the continuum side, a white noise on $[0,1]\times\mathbb R$ is a centred Gaussian family $\{W(A)\}$ , indexed by the Borel sets of finite Lebesgue measure, with $E[W(A)W(B)]=|A\cap B|$ . Its multiple stochastic integrals are continuous linear maps $I_k:L^2([0,1]^k\times\mathbb R^k)\to L^2$ with $I_k(\mathbf 1_{A_1\times\dots\times A_k})=\prod_jW(A_j)$ for pairwise disjoint $A_j$ . Let $\varrho(t,x)=e^{-x^2/2t}/\sqrt{2\pi t}$ be the heat kernel and $\Delta_k=\{0=t_0<t_1<\dots<t_k\le1\}$ . Put $\varrho_k(\mathbf t,\mathbf x)=\prod_{j=1}^k\varrho(t_j-t_{j-1},x_j-x_{j-1})$ on $\Delta_k\times\mathbb R^k$ , with $x_0=0$ , and zero elsewhere. The Wiener chaos (7) is

\mathcal Z_\beta=\sum_{k\ge0}\beta^kI_k(\varrho_k)=1+\sum_{k\ge1}\beta^k\int_{\Delta_k}\int_{\mathbb R^k}\prod_{i=1}^kW(t_i,x_i)\,\varrho(t_i-t_{i-1},x_i-x_{i-1})\,dx_i\,dt_i .

The discrete counterpart of $I_k$ is the weighted U-statistic $\mathcal S_k^n(g)$ of (29): a sum of products $\prod_j\omega(i_j,x_j)$ over distinct times, weighted by averages of $g$ over space–time rectangles of size $\frac1n\times\frac2{\sqrt n}$ .

Formalization targets

Goal: Theorem 2.1 (second bullet), proved as Proposition 5.4

If, in addition, $\lambda(b)<\infty$ for all $0<b<\beta_0$ for some $\beta_0>0$ , then for every $\beta>0$

e^{-n\lambda(\beta n^{-1/4})}\,Z_n^\omega(\beta n^{-1/4})\xrightarrow{(d)}\mathcal Z_{\sqrt2\beta}\qquad(n\to\infty).

Modified partition function: Proposition 5.3 (Theorem 2.1, first bullet)

Under mean zero and variance one alone, $\mathfrak z_n^\omega(\beta n^{-1/4})\xrightarrow{(d)}\mathcal Z_{\sqrt2\beta}$ .

Milestones

In the order the proof uses them:

the norm $\|\varrho_k\|^2_{L^2}=1/(2^k\Gamma(k/2+1))$ and the convergence of the chaos series (§3.4, Lemma 3.1);
the $L^2$ structure of $\mathcal S_k^n$ (Lemma 4.1);
an approximation lemma for convergence in law (Lemma 4.2);
convergence of $n^{-3k/4}\mathcal S_k^n(g)$ to $I_k(g)$ , jointly over finitely many orders (Theorem 4.3);
convergence of whole discrete chaos expansions (Lemma 4.4);
the exact expansion $\mathfrak z_n^\omega(\beta)=\sum_{k\le n}2^{k/2}\beta^k\mathcal S_k^n(p_k^n)$ (Lemma 5.2);
a uniform $L^2$ bound on the discretised random walk kernels $n^{k/2}p_k^n$ (Lemma A.1);
Proposition 5.3.

Significance

The theorem gives a universal scaling limit for the partition function in a regime where the polymer still moves diffusively but feels the disorder. As a corollary, $\log Z_n^\omega(\beta n^{-1/4})-n\lambda(\beta n^{-1/4})$ converges in law, so the fluctuation exponent of the free energy is $0$ in this regime. The companion results (point-to-point partition functions, Theorem 2.2) show that the rescaled polymer path measure converges to a continuum directed random polymer. Letting $\beta$ grow then interpolates between Gaussian behaviour and the Tracy–Widom GUE fluctuations of the KPZ class. The U-statistic machinery of Section 4 (discrete chaos expansions in an i.i.d. space–time field converging to multiple Wiener–Itô integrals) applies to other discrete models with polynomial chaos expansions.

The theorem is proved in the paper. To our knowledge it has no machine-checked proof, and Mathlib has no space–time white noise, no multiple Wiener integrals, no Wiener chaos, no Lindeberg–Feller theorem for triangular arrays and no local limit theorem for the simple random walk. A complete formalization would build each of these and check the paper's argument, including two statements that are false as printed (see Formalization scope).

Difficulty

The obvious route is to expand $Z_n^\omega(\beta n^{-1/4})$ in powers of $\beta$ and pass to the limit term by term. Two steps of that route do not go through as stated. First, the $k$ -th term is a degenerate U-statistic of order $k$ in the environment. Its convergence to $I_k$ is not a classical central limit theorem: it needs joint control of all orders and a density argument in $L^2([0,1]^k\times\mathbb R^k)$ , and the space–time discretisation must respect the parity of the walk, which is why the rectangles have spatial length $2/\sqrt n$ . Second, exchanging the limit with the infinite sum over $k$ needs bounds on the discrete kernels $n^{k/2}p_k^n$ that are uniform in $n$ and summable in $k$ . Pointwise convergence from the local limit theorem is not enough. Passing from $\mathfrak z_n$ to $Z_n$ also requires a central limit theorem for a triangular array whose law depends on $n$ .

Formalization scope

The environment is ω : ℕ × ℤ → Ω → ℝ, independent and identically distributed, square integrable, with mean $0$ and variance $1$ . Times $i\ge1$ are read. $Z_n$ and $\mathfrak z_n$ are explicit averages over the $2^n$ step sequences. The white noise lives on $[0,1]\times\mathbb R$ , since only $t\le1$ enters (7). $I_k$ is a family of continuous linear maps on $L^2$ characterised by its values on indicators of products of disjoint sets. Every limit theorem quantifies over all white noises and all such families, and a separate item asserts that one exists. $\mathcal Z_\beta$ and $\mathcal S_k^n$ are sums in $L^2$ ; real powers $n^{-1/4}$ , $n^{-3k/4}$ are Real.rpow; $\lambda$ is Mathlib's cgf; convergence in law is TendstoInDistribution.

Normalisation of $I_k$ . The paper's normalisation of multiple integrals is not consistent (§3.2 and the remark on p. 19 differ by $k!$ ). The formalization follows (7) and the variance computation on p. 6: for $g$ supported on $\Delta_k\times\mathbb R^k$ , $E[I_k(g)^2]=\|g\|^2$ .

Corrected statements. Two milestones are stated in the corrected form that the paper's proof establishes:

Lemma 4.1. The bound $Q[\mathcal S_k^n(g)^2]\le n^{3k/2}\|g\|^2$ is false for general $g$ when $k\ge2$ , because permuted index vectors give the same product of environment variables. It is stated for $g$ vanishing outside $\Delta_k\times\mathbb R^k$ , the only case Section 5 uses. "Mean zero" is stated for $k\ge1$ , since $\mathcal S_0^n(g_0)=g_0$ .
Lemma 4.4. It is stated for Fock vectors whose components vanish outside the simplices, with square-summable norms, so that $\sum_kI_k(g_k)$ converges.

Theorem 4.5 and Lemma 4.6 (perturbed environments) are not part of the milestone list. Theorem 4.5 is false as printed: mean zero and a variance tending to $1$ do not give a central limit theorem for a triangular array, and the Lindeberg condition named in its proof must be added. Lemma A.1 is stated for the point-to-line kernels only.

Trivializations ruled out. The limit is the chaos (7) built from a genuine white noise and its multiple integrals, not any random variable with a prescribed property. $I$ is pinned down by $W$ . Every infinite sum comes with a milestone proving its summability, and the partition function averages over all $2^n$ walk paths.

Infrastructure that would be reusable beyond this mission: space–time white noise and multiple Wiener–Itô integrals with their isometry, a Lindeberg–Feller central limit theorem, the local limit theorem for the simple random walk, and the Cramér–Wold device. Contributions of any of these, or of proofs of the milestones in any order, are welcome.

Selected references

T. Alberts, K. Khanin, J. Quastel, The intermediate disorder regime for directed polymers in dimension 1+1, Ann. Probab. 42 (2014), 1212–1256. arXiv:1202.4398
T. Alberts, K. Khanin, J. Quastel, The continuum directed random polymer, J. Stat. Phys. 154 (2014), 305–326. MR3162542
F. Comets, N. Yoshida, Directed polymers in random environment are diffusive at weak disorder, Ann. Probab. 34 (2006), 1746–1770. MR2271480
S. Janson, Gaussian Hilbert Spaces, Cambridge Tracts in Mathematics 129, Cambridge University Press, 1997. MR1474726
P. Billingsley, Convergence of Probability Measures, Wiley, 1968. MR0233396

12 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Analysis of Thompson Sampling for the Multi-armed Bandit Problem 1: Logarithmic Regret for Two ArmsResearch Paper

Motivation

Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only $o(T)$ regret in time $T$ (Granmo 2010; May, Korda, Lee and Leslie 2011).

Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the $N$ -armed bound, Theorem 2.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least $\big[\sum_i \Delta_i/D(\mu_i\|\mu^*)+o(1)\big]\ln T$ . Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an $O(\sum_i \ln T/\Delta_i)$ finite-time bound. Agrawal and Goyal (2012) proved $O(\ln T/\Delta+1/\Delta^3)$ for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.

Setting

There are two arms. Arm $i\in\{1,2\}$ has a fixed, unknown reward distribution $D_i$ supported in $[0,1]$ , with mean $\mu_i$ . Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, $\mu_1>\mu_2$ , and $\Delta=\mu_1-\mu_2$ is the gap.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$ , a success count $S_i$ and a failure count $F_i$ , both starting at $0$ . In each round $t=1,2,\dots$ it

samples, independently for each arm, $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$ ;
plays $i(t)=\arg\max_i\theta_i(t)$ and observes a reward $\tilde r_t\sim D_{i(t)}$ ;
performs a Bernoulli trial with success probability $\tilde r_t$ , with outcome $r_t\in\{0,1\}$ ;
increments $S_{i(t)}$ if $r_t=1$ and $F_{i(t)}$ otherwise.

$k_i(t)$ is the number of plays of arm $i$ before round $t$ . The expected regret in time $T$ is

\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu_1-\mu_{i(t)})\Big],

the expectation being over the rewards and the algorithm's randomness.

The analysis uses the Beta cdf $F^{beta}_{\alpha,\beta}$ , the binomial cdf $F^B_{n,p}$ , and the random variable $X(j,s,y)$ : the number of independent $\mathrm{Beta}(s+1,j-s+1)$ draws made before one exceeds $y$ .

Formalization targets

Goal: Theorem 1 (p. 3)

There is an absolute constant $C>0$ such that for every two-armed instance with rewards in $[0,1]$ and $\mu_1>\mu_2$ , and every $T\ge 2$ ,

\mathbb E[\mathcal R(T)]\le C\Big(\frac{\ln T}{\Delta}+\frac1{\Delta^3}\Big).

The constant is not fixed numerically: the paper states the theorem in $O(\cdot)$ form (footnote 1), and the explicit display it reports on p. 8, $40\ln T/\Delta+48/\Delta^3+18\Delta$ , is not the formal claim.

Milestones

Fact 1 (p. 12): $F^{beta}_{\alpha,\beta}(y)=1-F^B_{\alpha+\beta-1,y}(\alpha-1)$ for positive integers $\alpha,\beta$ .
Lemma 1 (p. 6): $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$ .
Lemma 6 (p. 13): Hoeffding-type bounds (10)–(11) on binomial cdfs.
Fact 2 (p. 13): every median of $\mathrm{Binomial}(n,p)$ is $\lfloor np\rfloor$ or $\lceil np\rceil$ .
Lemma 2 (p. 7): $\Pr(E_2(t))\ge 1-2/T^2$ , where $E_2(t)=\{\theta_2(t)\le\mu_2+\Delta/2\ \text{or}\ k_2(t)<24\ln T/\Delta^2\}$ .
Lemma 3 (p. 7): a three-case bound on $\mathbb E\big[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]\big]$ for $s(j)\sim\mathrm{Binomial}(j,\mu_1)$ .
Eq. (1) (p. 7): $\mathbb E[k_2(T)]\le C(\ln T/\Delta^2+1/\Delta^4)$ .

Significance

The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in $T$ on every two-armed instance, matching the order in $T$ of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.

Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on $[0,1]$ -valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.

Difficulty

The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after $\Theta(\ln T/\Delta^2)$ plays. Under TS the optimal arm's sample $\theta_1(t)$ is random and, if the arm has been played rarely or its early rewards were poor, it falls below $\mu_2$ with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the $1/\Delta^3$ dependence enters.

Formalization scope

Model. The instance is the platform's StochasticBandit 2 (a probability measure on $\mathbb R$ per arm, mean banditArmMean), with the hypothesis that each reward law gives mass $1$ to $[0,1]$ . Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from $0$ .
Algorithm. Algorithm 2 is realized on one probability space with three independent i.i.d. tables: Beta draws $W(i,t,a,b)\sim\mathrm{Beta}(a+1,b+1)$ , rewards $X(i,t)\sim D_i$ , and uniforms $V(i,t)$ . Round $t$ uses $\theta_i(t)=W(i,t,S_i(t),F_i(t))$ , $\tilde r_t=X(i(t),t)$ and $r_t=\mathbf 1\{V(i(t),t)<\tilde r_t\}$ . Ties in the arg max go to the smaller index (a null event).
Values. Regret and expectations are lower Lebesgue integrals in $[0,\infty]$ . $X(j,s,y)$ is $\mathbb N\cup\{\infty\}$ -valued, so Lemma 1 at $y=1$ reads $\infty=\infty$ , as in the paper.
O(·). The paper's $O(\cdot)$ (footnote 1: $f\le cg$ for $n\ge n_0$ ) is stated with one universal constant $C>0$ , quantified before the instance, the means and the horizon, for all $T\ge 2$ . Eq. (1) is stated the same way, without its printed numerals.
Not trivial. The goal is about Algorithm 2 itself, with fresh Beta samples, fresh rewards and the Bernoulli coin. A statement about "any policy satisfying Lemma 2's event bound", or one whose constant depends on $\Delta$ , the reward laws or $T$ , would not be Theorem 1.
Edge cases. $\mu_1<1$ is assumed only in Lemma 3, where the paper's $R$ and $D$ require it. It is not a hypothesis of the goal.
Infrastructure. A complete proof needs: inverse-transform or order-statistics facts for Beta laws (Fact 1); geometric expectations; Hoeffding's inequality for sums of Bernoulli variables (Mathlib has Hoeffding/Azuma); the binomial median theorem (Jogdeo–Samuels; Kaas–Buhrman); and the coupling from the reward tables to the per-arm i.i.d. output stacks the paper reasons with. Fact 1, Lemma 6 and Fact 2 are reusable beyond this mission. Contributions to any milestone are welcome, and so is a direct proof of the regret bound with an explicit constant.

Selected references

S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3. https://arxiv.org/abs/1111.1797
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933) 285–294. https://doi.org/10.2307/2332286
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6 (1985) 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47 (2002) 235–256. https://doi.org/10.1023/A:1013689704352
K. Jogdeo and S. M. Samuels, Monotone convergence of binomial probabilities and a generalization of Ramanujan's equation, Annals of Mathematical Statistics 39 (1968) 1191–1195. https://doi.org/10.1214/aoms/1177698243
R. Kaas and J. M. Buhrman, Mean, median and mode in binomial distributions, Statistica Neerlandica 34 (1980) 13–18. https://doi.org/10.1111/j.1467-9574.1980.tb00681.x
O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling

11 thms2 active usersReviewed

Completed

Markov Chain Numerical Analysis Operations Research+1·Captain: mikedeng1

Fundamentals of Queueing Theory X: Uniformization of Continuous-Time Markov ChainsTextbook

Motivation

Most Markovian queueing models have no closed-form transient solution. The M/M/1 queue already needs modified Bessel functions (Chapter 2 of the book), and a finite-capacity or multi-class model with state-dependent rates has no closed form at all. What an analyst can always write down is the system of forward equations $p'(t)=p(t)Q$ for the state probabilities. Chapter 8 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), presents two numerical techniques that turn such models into numbers: the randomization (or uniformization) method for the transient distribution of a finite continuous-time Markov chain, and the Fourier-series method for inverting a Laplace transform, as needed for the M/G/1 waiting-time transform (5.33) and the busy-period transform (5.37).

Uniformization goes back to Jensen (1953) and is the standard transient solver in performance-evaluation and reliability tools. Its appeal is that it replaces a matrix exponential, which is numerically delicate, by powers of a stochastic matrix weighted by Poisson probabilities, with an error bound that can be fixed before the computation starts (Grassmann 1977; Gross and Miller 1984). The Fourier-series method with Euler summation is due to Abate and Whitt (Abate and Whitt 1992; Abate, Choudhury and Whitt 1999).

Setting

A continuous-time Markov chain $X(t)$ on the states $\{0,1,\dots,N\}$ is described by its infinitesimal generator $Q=(q_{ij})$ : for $i\ne j$ , $q_{ij}\ge0$ is the rate of jumps from $i$ to $j$ , and the diagonal entry is $-q_i$ with

q_i=\sum_{j\ne i}q_{ij},\qquad i=0,1,\dots,N.

The transient state-probability vector $p(t)=(p_0(t),\dots,p_N(t))$ , $p_n(t)=\Pr\{X(t)=n\}$ , is the solution of the forward equations

p'(t)=p(t)Q\quad(t\ge0),

started from a given probability vector $p(0)$ . Fix a constant $\Lambda>0$ with $\Lambda\ge q_i$ for every $i$ (the book takes $\Lambda=\max_i q_i$ ) and define the uniformized matrix

\tilde P=\frac{Q}{\Lambda}+I,\qquad \tilde p_{in}=\begin{cases}q_{in}/\Lambda&(i\ne n),\\1-q_i/\Lambda&(i=n).\end{cases}

It is the transition matrix of a discrete-time chain $Y_k$ : the state of $X$ after the $k$ -th event of a Poisson process of rate $\Lambda$ that has been thinned. Write $\phi^{(k)}=p(0)\tilde P^{k}$ for its distribution after $k$ steps.

For the second half of the chapter, the Laplace transform of a real function $f$ on $[0,\infty)$ is $\bar f(s)=\int_0^\infty e^{-st}f(t)\,dt$ , and the Fourier-series approximant with parameter $A$ is

f_{A,n}(t)=\frac{e^{A/2}}{2t}\Big[\bar f\Big(\frac{A}{2t}\Big)+2\sum_{k=1}^{n}(-1)^k\,\mathrm{Re}\,\bar f\Big(\frac{A+2k\pi i}{2t}\Big)\Big],

with $f_A(t)=\lim_{n\to\infty}f_{A,n}(t)$ .

Formalization targets

Goal: the randomization formula with its truncation bound (Eqs. (8.9)–(8.12))

The forward equations have a solution, and every solution satisfies, for all $t\ge0$ ,

p(t)=\sum_{k=0}^{\infty}p(0)\tilde P^{(k)}\,\frac{e^{-\Lambda t}(\Lambda t)^k}{k!},

and whenever $\sum_{k=0}^{T}e^{-\Lambda t}(\Lambda t)^k/k!>1-\epsilon$ , every component of the sum truncated at $k=T$ is within $\epsilon$ of $p_n(t)$ .

Milestones

Eq. (8.12): $\tilde P$ has the entries above and is a stochastic matrix.
Eqs. (8.13)–(8.14): $\phi^{(k)}=\phi^{(k-1)}\tilde P$ and each $\phi^{(k)}$ is a probability vector.
p.385: $\phi=\phi\tilde P\iff0=\phi Q$ .
Eqs. (8.27)–(8.28): for bounded Lipschitz $f$ , $A>0$ and $t>0$ ,

f_A(t)-f(t)=\sum_{k=1}^{\infty}e^{-kA}f\big((2k+1)t\big),\qquad |f_A(t)-f(t)|\le\frac{Ce^{-A}}{1-e^{-A}}\ \text{ if } |f(x)|\le C \text{ for } x>3t.

The mission also contains Eqs. (8.7)–(8.8) as a further theorem, outside the milestone list: the transition probabilities satisfy $p_{in}(t)=\sum_k\tilde p^{(k)}_{in}e^{-\Lambda t}(\Lambda t)^k/k!$ , and $p_n(t)=\sum_i p_i(0)p_{in}(t)$ .

Significance

The randomization formula reduces the transient analysis of any finite Markovian queue (finite-buffer, multi-server, with balking, reneging or state-dependent rates) to repeated vector–matrix products with a sparse stochastic matrix. The truncation point is chosen from a Poisson tail alone, independently of $Q$ . Milestone 3 shows that the same matrix gives the stationary equations, so one iteration serves both transient and steady-state computation. The discretization identity (8.27) is what justifies the parameter choice in Algorithm 8.1: the error decays like $e^{-A}$ .

All of these results are classical and proved in the literature. None of them is formalized in Lean or Mathlib as far as a search of the platform and Mathlib shows. Mathlib has the matrix exponential and Poisson summation under decay hypotheses, but no continuous-time Markov chain generators, no uniformization, and no Laplace transform. This mission would add the finite-state link between generators, stochastic matrices and matrix exponentials that later chapters of queueing and reliability theory use, and a verified error formula for a numerical inversion method in wide use.

Difficulty

The book's derivation is probabilistic: it conditions on the number of events of the Poisson( $\Lambda$ ) process and thins them. A formal statement cannot rest on that picture, because $p(t)$ is defined analytically, by the forward equations. The goal therefore contains a uniqueness statement for a linear ODE on $[0,\infty)$ with one-sided derivative at $0$ , which the book never mentions. The componentwise bound then needs $\tilde P$ to be stochastic, so that every $\phi^{(k)}_n$ lies in $[0,1]$ . That is exactly where $\Lambda\ge\max_i q_i$ is used; with a smaller $\Lambda$ the matrix $\tilde P$ has negative diagonal entries and the bound fails.

For (8.27), the book gives no proof. The identity is an aliasing (Poisson-summation) formula for a periodic function assembled from the values of $f$ at all odd multiples of $t$ . The convergence of the conditionally summed series (8.24) is the delicate point: continuity of $f$ at $t$ , the book's only hypothesis, does not guarantee convergence of a Fourier series. Mathlib's Poisson summation theorems require decay of the Fourier transform that the damped, reflected function built from $f$ does not have.

Formalization scope

States are Fin (N+1); a row vector is Fin (N+1) → ℝ; $pQ$ is vecMul. A generator is a real matrix with nonnegative off-diagonal entries and diagonal $-\sum_{j\ne i}q_{ij}$ .
$p(t)$ is not defined as the series. It is any function with $p(0)=p_0$ and one-sided derivative $p(t)Q$ within $[0,\infty)$ at every $t\ge0$ . The goal also asserts that such a function exists, so it cannot hold vacuously, and it asserts the series identity for every solution. Defining $p(t)$ as the series (8.9) would make the goal a tautology and is ruled out.
$\Lambda$ is any real with $\Lambda>0$ and $\Lambda\ge q_i$ for all $i$ (the book takes equality with $\max_i q_i$ ).
The truncation bound is stated componentwise, as on p.384 ("an error bound on $p_n(t)$ of $\epsilon$ "), for an arbitrary real $\epsilon$ and truncation point $T$ .
The series (8.8), (8.9) are stated with HasSum, so convergence is part of the claim.
The Laplace transform is the Lebesgue integral over $(0,\infty)$ at a complex argument. $f_A(t)$ is the limit of the partial sums $f_{A,n}(t)$ , and the convergence is part of milestone 4.
Strengthened hypotheses in milestone 4: $f$ bounded and Lipschitz on $[0,\infty)$ replaces " $t$ is a continuity point of $f$ ", which is not sufficient for convergence.
Corrected misprints: $e^{-\lambda t}$ in (8.9) is $e^{-\Lambda t}$ ; $q_{ij}/\Lambda$ in (8.12) is $q_{in}/\Lambda$ ; $\phi(Q/\Lambda-I)$ on p.385 is $\phi(Q/\Lambda+I)$ .
Not formalized: Theorem 8.1 (Bromwich inversion) and the real form (8.21), which the book states without hypotheses on $f$ ; the limit claim $\lim_k\phi^{(k)}=\lim_t p(t)$ on p.385, which fails when $\tilde P$ is periodic; the Euler-summation approximation (8.26) and the round-off discussion, which are stated with "≈".

Useful infrastructure: the matrix exponential and its derivative (Matrix, NormedSpace.exp), uniqueness for linear ODEs (Grönwall), Fourier series on the circle, and a reusable Laplace transform file. Contributions of general lemmas on generators and stochastic matrices are welcome, as they apply to every finite Markovian model in the series.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§8.1.2–8.2. https://doi.org/10.1002/9781118625651
A. Jensen, "Markoff chains as an aid in the study of Markoff processes", Skandinavisk Aktuarietidskrift 36 (1953) 87–91.
W. K. Grassmann, "Transient solutions in Markovian queueing systems", Computers & Operations Research 4 (1977) 47–53.
D. Gross, D. R. Miller, "The randomization technique as a modeling tool and solution procedure for transient Markov processes", Operations Research 32 (1984) 343–361. https://doi.org/10.1287/opre.32.2.343
J. Abate, W. Whitt, "The Fourier-series method for inverting transforms of probability distributions", Queueing Systems 10 (1992) 5–87. https://doi.org/10.1007/BF01158520
J. Abate, G. L. Choudhury, W. Whitt, "An introduction to numerical transform inversion and its application to probability models", in W. Grassmann (ed.), Computational Probability, Kluwer, 1999, 257–323.

8 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization IV: Nonstationary Optimization and a Convergence Criterion for Nonmonotone SequencesTextbook

Motivation

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$ , and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$ , and the iterates $x^s$ are required to follow the time path of the optimal solutions,

\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$ , nor of $f^0$ . Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ .

The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$ , the unique nearest point of $X$ to $y$ .
A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$ . The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$ .
The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots

with step sizes $\rho_s \ge 0$ .

For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$ ) and a sequence $(x^s)$ , the exit time from the $\varepsilon$ -ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ .
The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$ , the squared distance to $X^*$ .

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$ , $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$ , $\|g_s\| \le C$ , $\rho_s \ge 0$ , $\rho_s \to 0$ and $\sum_s \rho_s = \infty$ . Then the iterates of (6.41) satisfy

F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$ , with $x^*(s)$ a point of $X^*$ nearest to $x^s$ .
p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$ .
p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$ .
Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$ , the sequence leaves every small ball around a subsequential limit outside $X^*$ , and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$ , then $V(x^s)$ converges and all accumulation points lie in $X^*$ .
pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$ :

\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$ . Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$ , not on $f^0$ , so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$ , and only while the iterate stays away from $X^*$ ; near $X^*$ , $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$ , and $F^0(\cdot, s)$ , $f^0$ are convex and continuous on all of $\mathbb R^n$ .
projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$ ; $V$ is Metric.infDist · X* ^ 2.
Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$ , and that is the constant in milestone 2. All other results are qualitative.
Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as " $\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$ ", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$ " is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$ ", and condition (3) is imposed for the same $\varepsilon$ . (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$ ); the right limit is $V(x')$ . (iii) The display on p. 155 prints " $=$ " where the projection gives " $\le$ ". (iv) The proof on p. 155 prints " $x^{s_k} \to x' \in X^*$ " where $x' \notin X^*$ is meant.
Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

Selected references

Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

8 thms2 active usersReviewed

Markov Chain Operations Research Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory I: Foster's Criterion for Positive RecurrenceTextbook

Motivation

Almost every model in queueing theory is analysed through a Markov chain. The number of customers in an M/M/c queue is a continuous-time birth–death chain; the number left behind by departing customers of an M/G/1 queue is a discrete-parameter chain on $\{0,1,2,\dots\}$ (the imbedded Markov chain); networks of queues are chains on vectors of queue lengths. Before any steady-state formula (Erlang's formulas, the Pollaczek–Khintchine formula, product forms) can be used, one has to know that the chain has a steady state at all: that it is positive recurrent, so that a stationary distribution exists and equals the limiting distribution.

Chapter 1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), collects the two ingredients the rest of the book stands on: the Poisson process with its exponential interarrival times (§§1.7–1.8), and the classification theory of discrete-parameter Markov chains (§1.9), ending with Foster's criterion (Theorem 1.2), a sufficient condition for positive recurrence in terms of a drift inequality. The criterion goes back to F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953) (DOI 10.1214/aoms/1177728976), and is the ancestor of the Foster–Lyapunov method used for stability of queueing networks and stochastic systems.

This mission is the first of a series formalizing the book chapter by chapter.

Setting

A homogeneous discrete-parameter Markov chain on $\{0,1,2,\dots\}$ is given by a transition matrix $P=\{p_{ij}\}$ with $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every $i$ . The $m$ -step transition probabilities $p_{ij}^{(m)}$ are the entries of $P^m$ .

The first-passage probability $f_{ij}^{(n)}$ is the probability that the chain started in $i$ enters $j$ for the first time at step $n\ge1$ ; for $i=j$ it is the probability of first return at step $n$ . The return probability is $f_{jj}=\sum_{n\ge1}f_{jj}^{(n)}$ and the mean recurrence time is $m_{jj}=\sum_{n\ge1}n f_{jj}^{(n)}\in[0,\infty]$ . A state is positive recurrent if $f_{jj}=1$ and $m_{jj}<\infty$ ; the chain is positive recurrent if every state is.

The chain is irreducible if for every pair of states $(i,j)$ some $p_{ij}^{(n)}$ is positive, and aperiodic if for every state $k$ the greatest common divisor of $\{n\ge1:p_{kk}^{(n)}>0\}$ is $1$ . A stationary distribution is a probability vector $\pi$ with $\pi=\pi P$ , i.e. $\pi_j=\sum_i\pi_i p_{ij}$ for every $j$ .

For the Poisson part, $T_0,T_1,\dots$ are independent interarrival times, each exponentially distributed with rate $\lambda>0$ ; the arrival epochs are $S_n=T_0+\dots+T_{n-1}$ , and $N(t)=\#\{n\ge1:S_n\le t\}$ counts the arrivals in $[0,t]$ .

Formalization targets

Goal: Theorem 1.2 (Foster's criterion)

An irreducible, aperiodic chain is positive recurrent if there exist $x_j\ge0$ with

\sum_{j=0}^\infty p_{ij}x_j\le x_i-1\quad(i\ne0),\qquad\sum_{j=0}^\infty p_{0j}x_j<\infty .

Milestones: the Markov chain theorems

Theorem 1.1(a). In an irreducible, positive recurrent chain, $\pi_j=1/m_{jj}$ is a stationary distribution, and it is the only one.
Theorem 1.1(c). If moreover the chain is aperiodic and all moments of $\pi$ are finite, then $\lim_{m\to\infty}p_{ij}^{(m)}=\pi_j$ for all $i,j$ .

Milestones: the Poisson process and the exponential distribution

Eqs. (1.11)–(1.14). The unique solution of $p_0'=-\lambda p_0$ , $p_n'=-\lambda p_n+\lambda p_{n-1}$ with $p_0(0)=1$ , $p_n(0)=0$ is $p_n(t)=(\lambda t)^n e^{-\lambda t}/n!$ .
Eq. (1.15). With exponential interarrival times,

\Pr\{N(t)\le n\}=\int_t^\infty\frac{\lambda(\lambda x)^n}{n!}e^{-\lambda x}dx=\sum_{i=0}^n\frac{(\lambda t)^ie^{-\lambda t}}{i!}.

Eq. (1.16). Given $N(L)=k$ , the arrival epochs have density $k!/L^k$ on $\{0<t_1<\dots<t_k<L\}$ .
Eq. (1.17) and its converse (p.21). The exponential law satisfies $\Pr\{T\le t_1\mid T\ge t_0\}=\Pr\{0\le T\le t_1-t_0\}$ , and it is the only continuous distribution on $[0,\infty)$ that does.
Nonhomogeneous Poisson law (p.22). With a continuous rate $\lambda(t)$ the forward equations have the unique solution $p_n(t)=e^{-m(t)}m(t)^n/n!$ , $m(t)=\int_0^t\lambda(s)\,ds$ .

Significance

Foster's criterion reduces positive recurrence, a statement about return times, to exhibiting one test function $x$ with negative drift outside a single state. In the book it is the tool that establishes the existence of steady state for imbedded chains of the M/G/1 and G/M/1 queues (Chapter 5); its generalizations are the standard stability proofs for queueing networks. Theorem 1.1 then supplies what positive recurrence buys: the stationary distribution exists, is unique, equals $1/m_{jj}$ , and is the limit of the transition probabilities. The Poisson results justify the "Markovian" arrivals and services of Chapters 2–4.

All of these results are classical and proved in the literature; the book states Theorems 1.1 and 1.2 without proof. The Prove2Me platform already holds machine-checked versions of related Markov chain theorems in other missions (Levin–Peres–Wilmer's and Durrett's countable-chain convergence theorems), stated with different definitions and hypotheses. What this mission adds is a formal development in the book's own terms — first-passage probabilities $f_{jj}^{(n)}$ , mean recurrence times $m_{jj}$ , gcd periodicity — on which the later missions of the series (imbedded chains, birth–death processes) can build, together with a formal proof of Foster's criterion, which is not on the platform.

Difficulty

For Foster's criterion the natural first step, taking expectations of the drift inequality along the chain, only shows that the expected value of $x$ decreases while the chain stays away from $0$ . Turning that into a bound on the expected return time to $0$ requires an optional-stopping or telescoping argument over a random time, with the value $x$ possibly unbounded, and a separate argument that positive recurrence of state $0$ propagates to all states of an irreducible chain. The book's hypotheses include aperiodicity, which the argument does not use.

For Theorem 1.1, identifying the stationary distribution with $1/m_{jj}$ requires relating the matrix powers $P^n$ to the first-passage probabilities (a renewal decomposition), and uniqueness over countably many states needs care with infinite sums. For the Poisson results, the difficulty is measure-theoretic: the distribution of the sum of $n+1$ exponential variables, and conditioning on the event $\{N(L)=k\}$ for the order-statistics property.

Formalization scope

States are natural numbers; the transition matrix is a real function $p:\mathbb N\times\mathbb N\to\mathbb R$ with nonnegative entries and rows summing to one (as a convergent series). The return probability and the mean recurrence time are valued in $[0,\infty]$ , so null recurrence ( $m_{jj}=\infty$ ) is representable. Irreducibility is the per-pair notion. Stationary equations are stated componentwise with convergent series.

In Foster's criterion the series $\sum_j p_{ij}x_j$ are required to converge for every $i$ , which is the book's condition $\sum_j p_{0j}x_j<\infty$ together with the finiteness implicit in the inequalities for $i\ne0$ ; $x$ is real-valued and nonnegative. Dropping the convergence requirement would let a divergent row series (whose Lean sum is $0$ ) satisfy the inequality vacuously; allowing $x_j=\infty$ would make the hypothesis trivially satisfiable. Neither is permitted.

The closed forms stated explicitly are: $\pi_j=1/m_{jj}$ (Theorem 1.1(a), with both existence and uniqueness), the Poisson probabilities $(\lambda t)^ne^{-\lambda t}/n!$ (1.14), the Erlang tail integral and the Poisson CDF (1.15), the density $k!/L^k$ (1.16), and $e^{-m(t)}m(t)^n/n!$ for the nonhomogeneous law. Equations (1.14) and the nonhomogeneous law are stated as "solves the equations with the initial conditions if and only if equals the closed form", so both existence and uniqueness are asserted.

The Poisson results use random variables on a probability space, with Mathlib's expMeasure for the exponential law and cond for conditional probability. The derivation of the forward equations from the $o(\Delta t)$ axioms of §1.7 is not formalized; the Poisson law is reached from the equations and, separately, from exponential interarrival times.

Not formalized: Theorem 1.1(b) and the word "ergodic" in 1.1(c), which rest on the book's informal notion of ergodicity; Theorem 1.3, whose phrase "for Theorem 1.1 to be valid" for a continuous-time chain is not pinned down.

The Markov chain definitions are reusable by every later mission that studies an imbedded chain. Contributions welcome: proofs of the milestones, and supporting lemmas (Chapman–Kolmogorov, renewal decomposition of $p_{jj}^{(n)}$ , class properties of recurrence).

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976

11 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design XI: Optimal Sequential Screening by Option ContractsTextbook

Motivation

Many sales are contracted before the buyer knows what the good is worth to her. An airline sells a ticket months before the trip, a hotel sells a refundable or non-refundable room before the traveller's plans are settled, and a supplier signs a capacity contract before demand is realised. At the time of contracting the buyer holds some private information about her future valuation (how likely she is to travel), and after contracting she learns more (whether she actually travels). Sequential screening is the mechanism design problem of a seller facing such a buyer.

The chapter formalized here, Daniel Krähmer and Roland Strausz's Dynamic Mechanism Design (Chapter 11 of Börgers' textbook), develops the problem along two lines. The first is dynamic private information: one sale, two rounds of private information. The second is dynamic allocations: repeated sales, one fixed valuation.

Timeline:

Baron and Besanko (1984) show that dynamic allocations with static information produce no real dynamics in the optimal mechanism.
Courty and Li (2000, Review of Economic Studies) solve the sequential screening problem and show that the optimal mechanism is a menu of option contracts.
Esö and Szentes (2007) decompose the buyer's information into initial and additional information, show that the seller can extract the additional information at no cost, and derive the optimal multi-buyer mechanism, the handicap auction.
Krähmer and Strausz (2011, 2014), cited in the chapter's problems (notes 2–3, p.237), show that the conclusions depend on the model's assumptions; with discrete ex ante types the privacy of the additional information can cost the seller (Problem 11.5(c), p.233).

Setting

A seller sells one indivisible good. Before contracting, the buyer privately observes her ex ante type $\tau\in[\underline\tau,\bar\tau]$ , with distribution function $G$ and density $g>0$ . After accepting the mechanism she privately observes her ex post type $\theta\in[\underline\theta,\bar\theta]$ , $0\le\underline\theta<\bar\theta$ , which is her valuation. Conditionally on $\tau$ it has distribution function $F(\theta\mid\tau)$ and density $f(\theta\mid\tau)>0$ . Both $F$ and $f$ are continuously differentiable in $\tau$ , $|\partial F/\partial\tau|<K$ , and higher $\tau$ is good news in the sense of first-order stochastic dominance: $\partial F(\theta\mid\tau)/\partial\tau<0$ for $\theta\in(\underline\theta,\bar\theta)$ .

A direct mechanism is a pair $q(\tau,\theta)\in[0,1]$ , $t(\tau,\theta)\in\mathbb R$ . The buyer first reports $\tau$ , then $\theta$ . Write $u(\tau,\theta)=\theta q(\tau,\theta)-t(\tau,\theta)$ , $\hat U(\tau'\mid\tau)=\int u(\tau',\hat\theta)f(\hat\theta\mid\tau)\,d\hat\theta$ and $U(\tau)=\hat U(\tau\mid\tau)$ . The mechanism is incentive-compatible if truth about $\theta$ is optimal after every report of $\tau$ , and truth about $\tau$ is optimal against every subsequent reporting function $\theta_r$ . It is individually rational if $U(\tau)\ge0$ for all $\tau$ . The seller maximizes expected revenue $\int\!\!\int t\,f\,g$ . The virtual valuation is

\psi(\tau,\theta)=\theta+\frac{1-G(\tau)}{g(\tau)}\,\frac{\partial F(\theta\mid\tau)/\partial\tau}{f(\theta\mid\tau)} ,

and Assumption 11.1 requires $\psi$ to be increasing in $\tau$ and $\theta$ . The exercise price is $p(\tau)=\min\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$ .

Formalization targets

Goal: Proposition 11.8 (optimal sequential screening)

Under Assumption 11.1 the optimal mechanism is

q^*(\tau,\theta)=\mathbf 1[\theta\ge p(\tau)],\qquad t^*(\tau,\theta)=t_0(\tau)+p(\tau)\,\mathbf 1[\theta\ge p(\tau)],

where $t_0$ is the expression of Proposition 11.5 for $q^*$ , and the lowest type pays

t(\underline\tau,\underline\theta)=\int_{p(\underline\tau)}^{\bar\theta}\hat\theta f(\hat\theta\mid\underline\tau)\,d\hat\theta-p(\underline\tau)\bigl[1-F(p(\underline\tau)\mid\underline\tau)\bigr]+\underline\theta q^*(\underline\tau,\underline\theta).

The goal asserts that this mechanism is incentive-compatible, individually rational and optimal. It also characterizes all optimal mechanisms: an incentive-compatible, individually rational mechanism is optimal if and only if $q=q^*$ almost everywhere off $\{\psi=0\}$ and $U(\underline\tau)=0$ . When $\{\psi=0\}$ is null, this becomes $q=q^*$ and $t=t^*$ almost everywhere.

Milestones

The path to the goal, in the book's order:

the dynamic revelation principle (Proposition 11.1);
the reduction of incentive compatibility to two families of inequalities (Proposition 11.2);
the ex post characterization (Proposition 11.3);
monotonicity and absolute continuity of $U$ (Lemma 11.1);
the envelope formula $U'(\tau)=-\int q(\tau,\hat\theta)\,\partial F(\hat\theta\mid\tau)/\partial\tau\,d\hat\theta$ (Proposition 11.4);
the transfer formula (Proposition 11.5);
sufficiency of monotone allocation rules (Proposition 11.6);
individual rationality at $\underline\tau$ (Proposition 11.7).

Three extensions follow. Propositions 11.9 and 11.10 show that the privacy of the additional information $\gamma=F(\theta\mid\tau)$ costs the seller nothing. Proposition 11.11 gives the optimal mechanism with several buyers. Proposition 11.12 shows that with dynamic allocations and a fixed valuation, repeating the static posted price is optimal.

Significance

The result gives a practical rule: sell an option. Ex ante type $\tau$ pays a fee $t_0(\tau)$ for the right to buy later at the exercise price $p(\tau)$ , and $p$ decreases in $\tau$ . This explains refund and cancellation menus in advance-purchase markets. Proposition 11.10 adds that information the buyer receives after contracting generates no rents under Assumption 11.1. A seller therefore gains from contracting early and from disclosing information after contracting. Proposition 11.12 shows that, under full commitment, a monopolist gains nothing from responding to past purchases.

On the formal side, the results are proved in the literature and in the book, but none of them is machine-checked. The mission produces a verified envelope theorem in a two-dimensional type space where incentive compatibility does not imply monotonicity. It also produces a verified revenue-equivalence formula for sequential mechanisms, and the first verified optimal-mechanism results with dynamic information.

Difficulty

The static argument of Chapter 2 does not carry over directly. Incentive compatibility with respect to $\tau$ does not make $q$ increasing in $\tau$ . The buyer's first-period utility is an expectation over a whole schedule $q(\tau',\cdot)$ , so single crossing has no bite. The characterization therefore splits into necessary conditions (the envelope formula in $\tau$ , which needs Lipschitz continuity of $U$ from the bound $K$ ) and a sufficient condition (monotonicity in both arguments, via first-order stochastic dominance), and the two meet only under Assumption 11.1.

Definition 11.2(ii) quantifies over all off-path reporting functions. The revelation principle does not remove them, so Proposition 11.2 is needed before any envelope argument applies.

Pointwise maximization of the virtual surplus pins down $q$ only where $\psi\ne0$ and only almost everywhere. The optimal mechanism is therefore not unique in the pointwise sense the page states.

Formalization scope

Representation. $F(\theta\mid\tau)$ is F θ τ and $q(\tau,\theta)$ is q τ θ. Functions are total on $\mathbb R$ or $\mathbb R^2$ , and conditions quantify over the type intervals only. $\partial F/\partial\tau$ and $\partial f/\partial\tau$ are fields pinned by HasDerivWithinAt on $[\underline\tau,\bar\tau]$ .
Measurability. The book omits all measurability. Here the densities are jointly measurable, mechanisms are admissible (measurable on the type rectangle, $q\in[0,1]$ ), and reporting functions are measurable. In the observable- $\gamma$ model each $\tilde t(\tau,\cdot)$ is integrable on $[0,1]$ , and in the several-buyer model each payment $t_i$ is integrable against the distribution of the type profile, so that expected utilities and expected revenue are genuine integrals.
Revenue and a.e. Revenue is the integral of $t$ against the joint law with density $g(\tau)f(\theta\mid\tau)$ , and "almost everywhere" refers to that law.
Corrected necessity. The page's pointwise "if and only if" in Propositions 11.8 and 11.11 is corrected. The explicit optimal mechanism is kept, with the formulas (11.10), (11.11), (11.12) and $t_0$ of Proposition 11.5. Necessity is stated almost everywhere and off $\{\psi=0\}$ , and, for several buyers, off ties between virtual valuations.
Regularity. Propositions 11.9 and 11.10 assume $f$ and $\partial F/\partial\tau$ continuous in $(\tau,\theta)$ , the regularity the book invokes on p.217 to differentiate $F^{-1}(\gamma\mid\tau)$ .
Exercise price. $p(\tau)$ is the infimum of $\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$ .

Ruled out. Stating only that the cutoff mechanism is incentive-compatible and individually rational, or only that it beats posted prices, would trivialize the goal. The goal asserts optimality among all admissible incentive-compatible, individually rational sequential mechanisms with randomized allocations, together with the explicit fee $t_0$ and (11.12).

Infrastructure. A complete development needs envelope theorems for suprema of equi-differentiable families, integration by parts with absolutely continuous functions, differentiation under the integral sign, and change of variables $\gamma=F(\theta\mid\tau)$ . The single-buyer lemmas (Propositions 11.2–11.7) are reusable for the multi-buyer case through the interim mechanism $(Q_i,T_i)$ . Proofs of any milestone, and sorry-free lemmas on the definitions, are welcome.

Selected references

D. Krähmer and R. Strausz, Dynamic Mechanism Design, Chapter 11 in T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
P. Courty and H. Li, Sequential Screening, Review of Economic Studies 67 (2000) 697–717. https://doi.org/10.1111/1467-937X.00150
P. Eső and B. Szentes, Optimal Information Disclosure in Auctions and the Handicap Auction, Review of Economic Studies 74 (2007) 705–731. https://doi.org/10.1111/j.1467-937X.2007.00438.x
D. P. Baron and D. Besanko, Regulation and Information in a Continuing Relationship, Information Economics and Policy 1 (1984) 267–302.

18 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design X: Robust Mechanism Design — Belief Revelation on Finite Type SpacesTextbook

Motivation

Classical Bayesian mechanism design assumes that the designer knows the agents' beliefs about each other: typically a commonly known prior over independent private values. Wilson's critique (1987) observed that mechanisms tuned to such a prior can depend on details that no designer knows, and a literature on robust mechanism design replaced the fixed prior by a large family of possible beliefs. Chapter 10 of Börgers, An Introduction to the Theory of Mechanism Design (OUP 2015), develops this programme in the framework of Bergemann and Morris (2001, 2005): agents' information is described by a type space, the designer is uncertain which beliefs agents hold, and mechanisms are compared across all type profiles at once.

Timeline of the results formalized here:

1980: Hylland shows that strategy-proof random mechanisms satisfying unanimity conditions are random dictatorships; Dutta, Peters and Sen (2007, 2008) give and correct the cardinal version used in the chapter.
1985: Mertens and Zamir construct the universal type space of belief hierarchies; the space of finite types is emphasized by Dekel, Fudenberg and Morris (2006).
1988: Crémer and McLean show that with correlated types satisfying a spanning condition, beliefs can be elicited at no cost (Proposition 6.4 of the book).
2001–2005: Bergemann and Morris introduce payoff and belief types and prove that on finite type spaces only incentive constraints between types with the same beliefs matter (their Proposition 4.5, the goal of this mission).
2010–2014: Smith, Börgers and Smith study the ranking of mechanisms without a common prior; random dictatorship with compromise comes from Börgers and Smith (2012, 2014).

Setting

There are finitely many agents $i \in I$ , and agent $i$ has a set $\Theta_i$ of payoff types. An outcome $x$ gives agent $i$ the utility $u_i(x,\theta)$ , which may depend on all payoff types. A type space $\mathcal T = (T_i,\hat\theta_i,\hat\beta_i)_{i\in I}$ consists of nonempty sets $T_i$ of types, a payoff type map $\hat\theta_i : T_i \to \Theta_i$ and a belief map $\hat\beta_i : T_i \to \Delta(T_{-i})$ , where $T_{-i} = \prod_{j\ne i}T_j$ . Different types may share a payoff type and differ only in their beliefs, and vice versa. A common prior is a distribution $\mu$ on $T$ from which every type's belief is obtained by conditioning. A type space has a large variety of certainties if for every $\theta_i$ and $\theta_{-i}$ some type with payoff type $\theta_i$ is certain that the others' payoff types are $\theta_{-i}$ . The space of finite types $\mathcal T^+$ collects every infinite hierarchy of beliefs ("I believe that you believe that …") that is generated by a type of some finite type space.

A mechanism $(S_1,\dots,S_N,g)$ has strategy sets $S_i$ and an outcome rule $g : S \to \Delta(X)$ . Strategies $\sigma_i : T_i \to \Delta(S_i)$ form a Bayesian equilibrium if each type maximizes expected utility under its own belief; it is belief-independent if types with equal payoff types play alike, and ex post if each type's choice stays optimal when it becomes certain of the others' types. A direct mechanism asks agents for their types, a reduced direct mechanism only for their payoff types. In the quasi-linear case outcomes are $(a,t_1,\dots,t_N)$ and $u_i = v_i(a,\theta) - t_i$ , with $t_i$ paid by agent $i$ ; a direct mechanism is $(q,t)$ .

Formalization targets

Goal: belief revelation on finite type spaces (Proposition 10.6)

On a finite type space with quasi-linear utilities, suppose that for every agent no belief in $\{\hat\beta_i(\tau_i) : \tau_i\in T_i\}$ is a convex combination of the others, and that in the direct mechanism $(q,t)$ no type wants to imitate another type with the same belief. Then there is a direct mechanism $(\tilde q,\tilde t)$ in which truth telling is a Bayesian equilibrium, with

\tilde q(\tau) = q(\tau)\ \ \forall \tau\in T,\qquad \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\,\tilde t_i(\tau) = \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\, t_i(\tau)\ \ \forall i,\tau_i.

The goal fixes neither the transfers $\tilde t$ nor any bound on them; it asserts the existence of a truthful mechanism with the same alternatives and the same interim payments.

Milestones

The other fourteen numbered results of the chapter: conditional independence of payoff types under a full-support common prior (10.1); three revelation principles (10.2–10.4); existence of Bayesian equilibria of finite mechanisms on $\mathcal T^+$ (10.5); betting between agents with inconsistent beliefs (10.7); ex post implementation of unique equilibrium outcomes and alternatives (10.8, 10.9); emptiness of the set of undominated auctions under interim Pareto welfare and under ex post revenue (10.10, 10.11); Hylland's characterization of random dictatorship (10.12); and three comparisons of random dictatorship with random dictatorship with compromise (10.13–10.15).

Significance

Proposition 10.6 reduces the design problem on a finite type space to incentive constraints among types with the same beliefs: belief types can always be elicited by side payments that leave interim utilities unchanged. With a common prior and Proposition 10.1 this yields optimal mechanisms by solving an independent-types problem for each profile of belief types (§10.8; Farinha Luz 2013 carries this out for auctions). Proposition 10.7 and its consequences 10.10–10.11 show why the same construction cannot be used without a common prior: inconsistent beliefs allow unbounded bets, so interim or revenue criteria admit no undominated mechanism. Propositions 10.12–10.15 show that relaxing belief independence escapes Hylland's impossibility result in the voting problem.

None of these results is formalized elsewhere to our knowledge. The book proves only some of them (10.1, 10.5, 10.8, 10.9, 10.13–10.15 are proved or outlined; 10.6 is sketched; the proofs of 10.2–10.4 are omitted as standard; 10.7 and 10.10–10.12 are stated without proof), so formalization also produces complete proofs of results the book leaves informal. Two printed statements are corrected (see Formalization scope).

Difficulty

The obvious approach to Proposition 10.6 applies the Crémer–McLean construction type by type. This fails because several types may share a belief: a side payment that depends on the reported belief cannot separate them, and the convex-independence condition concerns the set of distinct beliefs rather than the indexed family of types.

For the results on $\mathcal T^+$ , a type is an infinite belief hierarchy, and a strategy must be one function on all finite types simultaneously. Existence (10.5) cannot be obtained by applying Nash's theorem to a single finite type space, because a type belongs to many finite type spaces and must play the same strategy in all of them. Hylland's theorem (10.12) requires a full characterization of strategy-proof random rules on a cardinal preference domain.

Formalization scope

Distributions $\Delta(X)$ are countably supported (PMF X); expected utilities are sums. The book leaves the measure structure of type spaces unspecified (p.179, note 3); finite type spaces, $\mathcal T^+$ and point beliefs are covered exactly. A Bayesian equilibrium requires every type's expected utility to exist (absolute summability) under every mixed strategy.
A type's belief is a distribution on $\prod_{j\ne i}T_j$ . Beliefs in Proposition 10.6 are vectors in $\mathbb R^{T_{-i}}$ , and condition (i) is stated with the convex hull of the other distinct beliefs.
Quasi-linear direct mechanisms are deterministic, $q : T\to A$ , $t_i : T\to\mathbb R$ . Mixed misreports are allowed in every equilibrium notion.
$\mathcal T^+$ is built from belief hierarchies encoded level by level ( $L_0 = \Theta_i$ , $L_{n+1} = \Theta_i\times\Delta(\prod_{j\ne i}L_{n,j})$ ) and the finite type spaces generating them. The universal type space (Definition 10.5) is not needed and not formalized.
§10.11: two agents Fin 2, candidates $\{a,b,c\}$ , strict private vNM utilities with every strict utility attained; mechanisms map to lotteries over candidates; rankings are bijections C ≃ Fin 3.
Corrections of the page: in Proposition 10.7 the signs of the transfers in (v) are reversed on the page relative to the bet described on p.186 and are stated as described; Proposition 10.9 is false under a large variety of certainties alone and is stated under the common-certainty condition that its proof uses, on type spaces whose beliefs have finite support (with countably supported beliefs the reduced mechanism's expected utilities need not exist). Both are explained in the item notes.
The goal is not trivialized by taking $(\tilde q,\tilde t) = (q,t)$ : condition (ii) constrains only types with the same belief, so the original mechanism is in general not incentive-compatible, and the conclusion demands full Bayesian incentive compatibility.

Welcome contributions: a finite Farkas/separation lemma in the form needed for 10.6 (the platform has Polyhedral.farkas_lemma), basic API for PMF-valued type spaces (products of mixed strategies, conditioning), and the hierarchy map of finite type spaces, which all $\mathcal T^+$ milestones share.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 10. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
D. Bergemann, S. Morris, Robust Mechanism Design, Cowles Foundation Discussion Paper 1421, 2001; Econometrica 73 (2005) 1771–1813. https://doi.org/10.1111/j.1468-0262.2005.00638.x
J. Crémer, R. McLean, Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions, Econometrica 56 (1988) 1247–1257. https://doi.org/10.2307/1913096
J.-F. Mertens, S. Zamir, Formulation of Bayesian Analysis for Games with Incomplete Information, International Journal of Game Theory 14 (1985) 1–29. https://doi.org/10.1007/BF01770224
B. Dutta, H. Peters, A. Sen, Strategy-Proof Cardinal Decision Schemes, Social Choice and Welfare 28 (2007) 163–179. https://doi.org/10.1007/s00355-006-0152-4
T. Börgers, D. Smith, Robust Mechanism Design and Dominant Strategy Voting Rules, Theoretical Economics 9 (2014) 339–360. https://doi.org/10.3982/TE1100

19 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design IV: The Myerson–Satterthwaite TheoremTextbook

Motivation

Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.

This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.

Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.

Setting

A seller $S$ owns one indivisible good; a buyer $B$ may buy it. The seller's value $\theta_S$ has distribution $F_S$ with density $f_S > 0$ on $[\underline\theta_S, \overline\theta_S]$ ; the buyer's value $\theta_B$ has distribution $F_B$ with density $f_B > 0$ on $[\underline\theta_B, \overline\theta_B]$ . The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is $t$ if she sells for $t$ and $\theta_S + t$ if she keeps the good and receives $t$ ; the buyer's is $\theta_B - t$ if he buys and pays $t$ , and $-t$ otherwise.

A direct mechanism is a trading rule $q : \Theta \to \{0,1\}$ on $\Theta = [\underline\theta_S, \overline\theta_S] \times [\underline\theta_B, \overline\theta_B]$ and transfers $t_S$ (received by the seller) and $t_B$ (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities $Q_S, Q_B$ , the interim transfers $T_S, T_B$ , and the interim utilities $U_S(\theta_S) = T_S(\theta_S) + (1 - Q_S(\theta_S))\theta_S$ and $U_B(\theta_B) = Q_B(\theta_B)\theta_B - T_B(\theta_B)$ . The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if $U_S(\theta_S) \ge \theta_S$ and $U_B(\theta_B) \ge 0$ for all types, ex post budget balanced if $t_S(\theta) = t_B(\theta)$ for every $\theta$ , and ex ante budget balanced if $\mathbb E[t_S] = \mathbb E[t_B]$ . A first-best trading rule trades when $\theta_B > \theta_S$ and not when $\theta_B < \theta_S$ , with any choice at ties. The seller's virtual cost is $\psi_S = \theta_S + F_S/f_S$ and the buyer's virtual valuation is $\psi_B = \theta_B - (1 - F_B)/f_B$ ; the distributions are regular if both are increasing.

Formalization targets

Goal: Proposition 3.12 (Myerson–Satterthwaite)

An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if

\underline\theta_B \ge \overline\theta_S \quad\text{or}\quad \underline\theta_S \ge \overline\theta_B .

Milestones

Lemmas 3.9–3.11. The pivot mechanism is incentive-compatible and individually rational. Among all such mechanisms that implement a first-best rule, it maximizes $\mathbb E[t_B - t_S]$ . That quantity is negative whenever $\underline\theta_B < \overline\theta_S$ and $\overline\theta_B > \underline\theta_S$ .
Proposition 3.13 (second best). With overlapping supports and regular distributions, the welfare-maximizing incentive-compatible, individually rational, ex ante budget balanced mechanisms are characterized by the trading rule

q(\theta) = 1 \iff \theta_B - \tfrac{\lambda}{1+\lambda}\tfrac{1 - F_B(\theta_B)}{f_B(\theta_B)} \ge \theta_S + \tfrac{\lambda}{1+\lambda}\tfrac{F_S(\theta_S)}{f_S(\theta_S)}

for some $\lambda > 0$ , exact budget balance $\int q\,(\psi_B - \psi_S)\,f = \overline\theta_S - \int \psi_S f$ , and the incentive-compatible payments with binding participation of $\overline\theta_S$ and $\underline\theta_B$ .

Proposition 3.14 (profit maximization). Profit $\mathbb E[t_B - t_S]$ is maximized by trading iff $\psi_B(\theta_B) > \psi_S(\theta_S)$ , with the same payment formulas.
Propositions 3.15–3.16 (uniform values on $[0,1]$ ). The second best trades iff $\theta_B - \theta_S > 1/4$ ; the profit maximizer trades iff $\theta_B - \theta_S > 1/2$ .

Significance

The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.

All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.

Difficulty

The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.

Formalization scope

A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on $\Theta$ with density $f_S(\theta_S) f_B(\theta_B)$ . Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in $\{0,1\}$ on $\Theta$ (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: $q$ , $t_S$ , $t_B$ are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.

Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter $\lambda > 0$ , the exact budget equation of Proposition 3.13 (ii), the payment formulas $T_B(\theta_B) = \theta_B Q_B(\theta_B) - \int_{\underline\theta_B}^{\theta_B} Q_B$ and $T_S(\theta_S) = \overline\theta_S - (1 - Q_S(\theta_S))\theta_S - \int_{\theta_S}^{\overline\theta_S}(1 - Q_S)$ , the profit rule $\psi_B > \psi_S$ , and the thresholds $1/4$ and $1/2$ .

The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality $t_S = t_B$ . Dropping budget balance, weakening it to $t_S \le t_B$ , or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all $\theta$ " characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to $\{\psi_B \ne \psi_S\}$ : under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.

Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.

Selected references

R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
K. Chatterjee and W. Samuelson, Bargaining under incomplete information, Operations Research 31 (1983) 835–851. https://doi.org/10.1287/opre.31.5.835
W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.4. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design III: Impossibility of First-Best Public Goods ProvisionTextbook

Motivation

Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.

This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.

Setting

A community of agents $I = \{1, \dots, N\}$ , $N \ge 2$ , decides whether to produce an indivisible, nonexcludable public good, $g \in \{0,1\}$ , at cost $c > 0$ . Agent $i$ pays a transfer $t_i$ and obtains utility $\theta_i g - t_i$ . Her type $\theta_i$ is private information, drawn independently across agents from a distribution $F_i$ with density $f_i$ , strictly positive on the common support $[\underline\theta, \bar\theta]$ , $0 \le \underline\theta < \bar\theta$ . The type space is $\Theta = [\underline\theta, \bar\theta]^N$ and $f(\theta) = \prod_i f_i(\theta_i)$ .

A direct mechanism is a decision rule $q : \Theta \to \{0,1\}$ and transfer rules $t_i : \Theta \to \mathbb R$ . For agent $i$ reporting $\theta_i$ , $Q_i(\theta_i)$ is the probability of production and $T_i(\theta_i)$ the expected transfer, taken over the other agents' types, and $U_i(\theta_i) = Q_i(\theta_i)\theta_i - T_i(\theta_i)$ . The mechanism is incentive compatible (IC) if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i, \theta_i, \theta_i'$ , and individually rational (IR) if $U_i(\theta_i) \ge 0$ for all $i, \theta_i$ . It is ex post budget balanced if $\sum_i t_i(\theta) \ge c\,q(\theta)$ for every $\theta$ , and ex ante budget balanced if this inequality holds after integrating both sides against $f$ .

Welfare is $(\sum_i \theta_i)\, g - \sum_i t_i$ . The first best decision rule is $q^*(\theta) = 1$ if $\sum_i \theta_i \ge c$ and $0$ otherwise; a first best mechanism uses $q^*$ and transfers that add up to exactly $c\,q^*(\theta)$ in every state. The pivot mechanism uses $q^*$ and

t_i(\theta) = \underline\theta\, q^*(\underline\theta,\theta_{-i}) + \big(q^*(\theta) - q^*(\underline\theta,\theta_{-i})\big)\Big(c - \sum_{j\ne i}\theta_j\Big).

The virtual valuation is $\psi_i(\theta_i) = \theta_i - (1-F_i(\theta_i))/f_i(\theta_i)$ , and $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Proposition 3.7

\exists\ \text{an IC and IR first best mechanism} \iff N\underline\theta \ge c \ \text{ or }\ N\bar\theta \le c .

In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.

Milestones

Proposition 3.6: every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
Lemma 3.6: the pivot mechanism is IC and IR.
Lemma 3.7: among IC and IR mechanisms with decision rule $q^*$ , the pivot mechanism has the largest expected budget surplus.
Lemma 3.8: if $N\underline\theta < c < N\bar\theta$ , the pivot mechanism's expected budget surplus is negative.
Proposition 3.8 (second best): under regularity and $N\underline\theta < c < N\bar\theta$ , an IC, IR, ex ante budget balanced mechanism maximizes expected welfare among such mechanisms iff for some $\lambda > 0$

q(\theta) = 1 \iff \sum_i \theta_i > c + \sum_i \frac{\lambda}{1+\lambda}\,\frac{1-F_i(\theta_i)}{f_i(\theta_i)},

the budget binds, $\int_\Theta q(\theta)\big[\sum_i \psi_i(\theta_i) - c\big] f(\theta)\,d\theta = 0$ , and $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ . 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff $\sum_i \theta_i > c + \sum_i (1-F_i(\theta_i))/f_i(\theta_i)$ , with the same formula for $T_i$ . 7. Proposition 3.10 (Example 3.3: $N=2$ , uniform types on $[0,1]$ , $0<c<2$ ): the second best produces iff $\theta_1+\theta_2 > s$ , where $s$ is the unique root in $[0,1]$ of $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ if $c < 2/3$ , and $s = \tfrac12 + \tfrac34 c$ if $c \ge 2/3$ . 8. Proposition 3.11 (same example): the profit maximizer produces iff $\theta_1+\theta_2 > 1 + \tfrac12 c$ .

Significance

Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.

All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.

Difficulty

The naive argument for the goal fails at the first step: a mechanism that implements $q^*$ with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule $q^*$ to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.

Formalization scope

Agents are Fin N with $N \ge 2$ ; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures $f_i(x)\,dx$ on $[\underline\theta,\bar\theta]$ , which encodes independence. $Q_i$ and $T_i$ integrate the decision and transfer rules against this distribution with agent $i$ 's coordinate overwritten by her report. Decision rules are deterministic, with values in $\{0,1\}$ on $\Theta$ , as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.

The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires $q$ and each $t_i$ to be Borel measurable, each $t_i$ integrable, and each conditional expectation of $t_i$ given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every $\theta$ , is sufficient; necessity holds for almost every $\theta$ , since changing $q$ on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier $\lambda > 0$ and the binding budget identity; $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i$ ; the cubic $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ for $c < 2/3$ ; $s = \tfrac12 + \tfrac34 c$ for $c \ge 2/3$ ; and $s = 1 + \tfrac12 c$ for the profit maximizer.

A trivializing formalization of the goal takes "first best" to mean only the decision rule $q^*$ ; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly $c\,q^*(\theta)$ in every state.

Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.3. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
C. d'Aspremont and L.-A. Gérard-Varet, Incentives and incomplete information, Journal of Public Economics 11 (1979) 25–45. https://doi.org/10.1016/0047-2727(79)90043-4
W. Güth and M. Hellwig, The private supply of a public good, Zeitschrift für Nationalökonomie, Supplement 5 (1986) 121–159.
R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969.

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design II: Myerson's Optimal Single-Unit AuctionTextbook

Why revenue-maximizing auctions matter

A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.

This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.

Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).

Setting

There are $N \ge 2$ potential buyers $i \in I = \{1,\dots,N\}$ . Buyer $i$ values the good at $\theta_i$ ; if he receives it and pays $t_i$ his utility is $\theta_i - t_i$ , and otherwise $-t_i$ . The seller's utility is $\sum_i t_i$ . The valuations $\theta_1,\dots,\theta_N$ are independent; $\theta_i$ has cumulative distribution function $F_i$ and density $f_i$ with $f_i(\theta_i) > 0$ on the common support $[\underline\theta, \bar\theta]$ , where $0 \le \underline\theta < \bar\theta$ . The type space is $\Theta = [\underline\theta,\bar\theta]^N$ and the joint density is $f(\theta) = \prod_i f_i(\theta_i)$ .

A direct mechanism asks buyers to report their types and consists of an allocation rule $q : \Theta \to \Delta$ , where $\Delta = \{(q_1,\dots,q_N) : 0 \le q_i \le 1,\ \sum_i q_i \le 1\}$ , and payment rules $t_i : \Theta \to \mathbb R$ . Its interim quantities are the expected allocation probability, payment and utility of buyer $i$ conditional on his own type:

Q_i(\theta_i) = \int_{\Theta_{-i}} q_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad T_i(\theta_i) = \int_{\Theta_{-i}} t_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad U_i = \theta_i Q_i - T_i.

The mechanism is incentive-compatible if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i,\theta_i,\theta_i'$ (truth-telling is a Bayesian Nash equilibrium) and individually rational if $U_i(\theta_i) \ge 0$ for all $i,\theta_i$ . The virtual valuation of buyer $i$ is

\psi_i(\theta_i) = \theta_i - \frac{1 - F_i(\theta_i)}{f_i(\theta_i)},

and the distribution $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Myerson's optimal auction (Proposition 3.4)

Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue $\mathbb E[\sum_i t_i(\theta)]$ exactly when, for every buyer $i$ ,

q_i(\theta) = \begin{cases}1 & \text{if } \psi_i(\theta_i) > 0 \text{ and } \psi_i(\theta_i) > \psi_j(\theta_j) \text{ for all } j \ne i,\\ 0&\text{otherwise,}\end{cases}\qquad T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx,

the allocation identity holding for almost every $\theta$ ; and such a mechanism exists.

Milestones

Proposition 3.1, the revelation principle: every Bayesian Nash equilibrium of every mechanism is replicated by truth-telling in an incentive-compatible direct mechanism.
Lemmas 3.1–3.4: incentive compatibility makes $Q_i$ increasing and $U_i$ convex with $U_i' = Q_i$ ; payoff equivalence $U_i(\theta_i) = U_i(\underline\theta) + \int_{\underline\theta}^{\theta_i} Q_i$ ; revenue equivalence for $T_i$ .
Proposition 3.2: incentive compatibility holds if and only if every $Q_i$ is increasing and the revenue-equivalence formula holds.
Proposition 3.3: under incentive compatibility, individual rationality is equivalent to $T_i(\underline\theta) \le \underline\theta Q_i(\underline\theta)$ .
Lemma 3.5: an optimal mechanism has $T_i(\underline\theta) = \underline\theta Q_i(\underline\theta)$ .
Eqs. (3.4)–(3.5): expected revenue equals expected virtual surplus $\sum_i \int_\Theta q_i(\theta)\psi_i(\theta_i) f(\theta)\,d\theta$ .
Proposition 3.5: a mechanism maximizes expected welfare $\mathbb E[\sum_i q_i(\theta)\theta_i]$ among incentive-compatible, individually rational mechanisms if and only if it gives the good to the highest value (almost everywhere) and $T_i(\theta_i) \le \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i}Q_i$ .

Significance

The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price $\psi^{-1}(0)$ when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.

The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end $\underline\theta \ge 0$ , Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on $[0,\bar v]$ .

Difficulty

The obvious argument maximizes the virtual surplus $\sum_i q_i(\theta)\psi_i(\theta_i)$ pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every $Q_i$ ; the pointwise maximizer is feasible only because regularity makes $\psi_i$ increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every $\psi_i$ and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of $U_i$ , with care at the endpoints of the type interval.

Formalization scope

Buyers form a finite type with at least two elements. The prior is the measure on $\mathbb R^N$ with density $\prod_i f_i(\theta_i)$ on $\Theta$ and no mass outside it; each $f_i$ is measurable, strictly positive on $[\underline\theta,\bar\theta]$ and integrates to $1$ ; $F_i(\theta_i) = \int_{\underline\theta}^{\theta_i} f_i$ . Allocation and payment rules are total functions whose values on $\Theta$ are constrained, and $Q_i$ , $T_i$ are prior expectations with the $i$ -th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of $\psi_i$ on $[\underline\theta,\bar\theta]$ (Assumption 3.1).

The following conventions are committed to:

Measurability. The book omits measurability throughout. The comparison class for optimality consists of mechanisms with measurable $q_i, t_i$ , integrable $t_i$ , and integrable sections $\theta_{-i}\mapsto t_i(\theta_i,\theta_{-i})$ . Without these hypotheses the Lean integrals would be $0$ and revenue comparisons would be meaningless.
Almost-everywhere characterizations. Propositions 3.4 and 3.5 are printed with "for all $\theta \in \Theta$ ". Changing $q$ on a null set of type vectors changes neither incentives nor revenue nor welfare, so the "only if" directions hold only almost everywhere; they are stated for almost every $\theta$ , and the existence of a mechanism satisfying the allocation rule at every $\theta$ is stated separately. The payment conditions hold for every $\theta_i$ .
Explicit formulas. The goal states Myerson's allocation rule and the payment formula $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ explicitly. Proposition 3.5 states the efficient rule $q_i(\theta) = 1$ iff $\theta_i > \theta_j$ for all $j \ne i$ , and the payment inequality. A statement asserting only that some optimal mechanism exists, or only that the optimal auction is efficient, would not be this theorem.
Revelation principle. A general mechanism has arbitrary measurable message sets and an outcome function giving allocation probabilities in $\Delta$ and expected transfers; equilibria are in pure type-contingent strategies. A version in which the mechanism is already direct would be trivial and is not the statement.
Interim constraints. Incentive compatibility and individual rationality are Bayesian and interim, not dominant-strategy or ex post; the latter are the subject of a later mission.
Endpoints in Lemma 3.2. Differentiability of $U_i$ and $U_i' = Q_i$ are stated at interior points of $[\underline\theta,\bar\theta]$ .

The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.

Selected references

Tilman Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.2, pp. 31–45. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
John G. Riley and William F. Samuelson, Optimal Auctions, American Economic Review 71(3), 381–392, 1981. https://www.jstor.org/stable/1802786
William Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
Partha Dasgupta, Peter Hammond and Eric Maskin, The Implementation of Social Choice Rules: Some General Results on Incentive Compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045

12 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Bellman's Dynamic Programming VI: Optimal Policies for the Continuous Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.

It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.

Setting

Mine A holds $x_0 \ge 0$ units of gold and mine B holds $y_0 \ge 0$ . At time $t$ a proportion $\varphi_1(t) \in [0,1]$ of the machine's effort goes to A and $\varphi_2(t) = 1 - \varphi_1(t)$ to B (Eq. (7.3)). With $x(t), y(t)$ the gold remaining, $p(t)$ the probability that the machine still works and $f(t)$ the expected gold mined, the process is defined by Eq. (7.2):

\frac{dx}{dt} = -\varphi_1 r_1 x,\qquad \frac{dy}{dt} = -\varphi_2 r_2 y,\qquad \frac{dp}{dt} = -p\,(\varphi_1 q_1 + \varphi_2 q_2),\qquad \frac{df}{dt} = p\,(\varphi_1 r_1 x + \varphi_2 r_2 y),

with $x(0) = x_0$ , $y(0) = y_0$ , $p(0) = 1$ , $f(0) = 0$ . The mining rates $r_1, r_2$ and the failure rates $q_1, q_2$ are positive. The objective is the expected total gold $f(\infty) = \int_0^\infty f'(t)\,dt$ .

In the three-choice problem (§ 12) a third decision $C$ removes gold from A at rate $r_3$ and from B at rate $r_4$ , and fails at rate $q_3$ . A control is a triple $\varphi_1, \varphi_2, \varphi_3 \ge 0$ with $\varphi_1 + \varphi_2 + \varphi_3 = 1$ (Eq. (12.2)). For a horizon $T$ , the switching functions $K_1, K_2, K_3$ of Eq. (12.5) are computed along a control. For instance,

K_1(t) = -q_1\int_t^T f'(s)\,ds + r_1\,p(T)\,x(T) - r_1\int_t^T p'(s)\,x(s)\,ds.

They measure the first-order gain from shifting effort towards each decision at time $t$ . The linear forms

C_1 = q_1 r_2 y - q_2 r_1 x,\qquad C_2 = q_1 r_4 y - (q_3 r_1 - q_1 r_3)x,\qquad C_3 = (q_3 r_2 - q_2 r_4) y - q_2 r_3 x

and the quantity $D = q_1 r_2 r_3 + q_2 r_1 r_4 - q_3 r_1 r_2$ (Eqs. (13.2)–(13.3)) organize the analysis.

Formalization targets

Goal: Chapter VIII, Theorem 1

For the two-choice process, the maximum of $f(\infty)$ is attained by the policy

\varphi_1 = 1 \text{ for } q_1 r_2 y < q_2 r_1 x,\qquad \varphi_2 = 1 \text{ for } q_1 r_2 y > q_2 r_1 x,\qquad \varphi_1 = \tfrac{r_2}{r_1+r_2},\ \varphi_2 = \tfrac{r_1}{r_1+r_2} \text{ for } q_1 r_2 y = q_2 r_1 x.

The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes $f(\infty)$ over all measurable controls with values in $[0,1]$ .

Milestones

Eq. (10.1): $f_A(\infty) = r_1 x_0/(q_1 + r_1)$ and $f_B(\infty) = r_2 y_0/(q_2 + r_2)$ for the pure policies.
Lemmas 1–3 (§ 13): for a control that maximizes $f(T)$ , almost everywhere, $K_i > K_j$ forces $\varphi_i = 1$ or $\varphi_j = 0$ ; a strictly largest $K_i$ forces $\varphi_i = 1$ ; a strictly beaten $K_i$ forces $\varphi_i = 0$ .
Lemma 4 (§ 14): if $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant and $D \ne 0$ , no optimal control mixes $A$ , $B$ and $C$ on an interval.
Lemma 5 (§ 14): a mixture of exactly two decisions on an interval keeps the state on $C_1 = 0$ , $C_2 = 0$ or $C_3 = 0$ respectively, with the proportions that hold $y/x$ fixed.
§ 15, Eq. (1) (corrected): $f_C(\infty) = r_3 x_0/(q_3 + r_3) + r_4 y_0/(q_3 + r_4)$ .
"Theorem 8" (§ 16, the chapter's third theorem): if $D < 0$ (with $r_3 > r_4$ and $x_0, y_0 > 0$ ), the three-choice problem is solved by the two-choice rule of Theorem 1, and every optimal control has $\varphi_3 = 0$ almost everywhere.

Significance

Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope $y/x$ , and on the line $q_1 r_2 y = q_2 r_1 x$ it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: $D < 0$ means that $C$ removes gold at a higher failure cost than an equivalent mixture of $A$ and $B$ .

On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.

Difficulty

The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and $B$ is preferred near the $y$ -axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let $\varphi$ be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into " $C_k = 0$ on the interval".

Formalization scope

Process by closed forms. No differential equations are formalized. With $\Phi_i(t) = \int_0^t \varphi_i$ , the definitions are $x = x_0 e^{-r_1\Phi_1 - r_3\Phi_3}$ , $y = y_0 e^{-r_2\Phi_2 - r_4\Phi_3}$ , $p = e^{-\sum_i q_i\Phi_i}$ , $f(T) = \int_0^T f'$ . These are the unique absolutely continuous solutions of (7.2) and (12.1). The two-choice process is the three-choice one with $\varphi_3 = 0$ .
Controls are open-loop and measurable, with $\varphi_i \ge 0$ and $\sum_i \varphi_i = 1$ . Decisions are indexed 0, 1, 2 for $A, B, C$ .
$f(\infty)$ is a lower Lebesgue integral with values in $[0,\infty]$ . It has no junk value, and optimality is compared in $[0,\infty]$ .
Theorem 1's feedback rule is encoded as a predicate on open-loop controls: the rule holds along the control's own trajectory for almost every $t \ge 0$ . The goal also asserts that such a control exists, which rules out the trivializing reading in which no control satisfies the rule and the optimality claim is vacuous.
Horizon of Lemmas 1–5. § 12 considers only $T = \infty$ , but the variation (12.4) and the switching functions (12.5) are written for a general $T$ . Each lemma is formalized for both: every finite horizon $T$ , with $K_i$ built from that horizon, and $T = \infty$ , with $K_i$ given by (12.5) at $T = \infty$ (boundary term $0$ ).
Implicit ranges. All rates $q_1, q_2, q_3, r_1, \dots, r_4$ are taken positive, and $x_0, y_0 \ge 0$ . Lemmas 4–5 and "Theorem 8" take $x_0, y_0 > 0$ , the open quadrant the book analyses. Lemma 4 carries the book's assumption that $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant ( $q_1 r_3 < q_3 r_1$ , $q_2 r_4 < q_3 r_2$ ). "Theorem 8" carries the standing assumption $r_3 > r_4$ of § 15.
Misprint corrected. The value of the pure $C$ -policy in the proof of Lemma 6 (§ 15, Eq. (1), p. 237) is printed $r_3 x_0/(q_2 + r_3) + r_4 y_0/(q_3 + r_4)$ . The first denominator must be $q_3 + r_3$ : for $x_0 = 1$ , $y_0 = 0$ , $q_2 = 1$ , $q_3 = 2$ , $r_3 = 1$ the process yields $1/3$ , not $1/2$ . The corrected identity is stated.
Numbering. The third theorem of the chapter is printed "Theorem 8" and is cited that way.
Left out. Theorem 2 ( $D > 0$ ) specifies its solution only through Fig. 7 and an unspecified line $L$ . Lemmas 6–8, 11 and the two Lemmas 12 describe regions of figures. The finite-horizon analysis of § 11 has no numbered result, and neither does the nonlinear utility of § 18.

Useful infrastructure: the derivative formulas (13.1) for the $K_i$ , a first-variation lemma for $f(T)$ under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter VIII, pp. 222–244. https://doi.org/10.2307/j.ctv1nxcw0f
L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming V: Optimality of a Constant Stock Level for the Optimal Inventory EquationTextbook

Motivation

The optimal inventory problem asks how much of an item to stock when demand is random, ordering costs money, and running short costs more. Arrow, Harris and Marschak formulated it as a sequential decision problem in 1951 (Optimal inventory policy, Econometrica 19), and Dvoretzky, Kiefer and Wolfowitz studied its structure in 1952–53. Chapter V of Richard Bellman's Dynamic Programming (1957) treats the problem through a single functional equation for the minimal expected discounted cost. It shows that when ordering and shortage costs are proportional to quantity, the optimal policy is described by one number, a constant stock level $\bar x$ , computed from the demand distribution alone.

This result is an early form of the base-stock (order-up-to) policy. Base-stock policies are the standard structure in periodic-review inventory theory: Karlin (1958), Scarf's $(s,S)$ theorem (1960) and Veinott (1965) extend it. Chapter V is also a worked example of a point the book makes throughout: the method of successive approximations determines the shape of an optimal policy, and not only its existence.

Setting

A single item is stocked over an unbounded sequence of periods. At the start of a period the stock is $x \ge 0$ . The decision maker orders up to a level $y \ge x$ , at cost $k(y-x)$ with $k > 0$ . A demand $s \ge 0$ then arrives, with probability density $\varphi$ : $\varphi(s) > 0$ for $s > 0$ , $\int_0^\infty \varphi(s)\,ds = 1$ , and $\int_0^\infty s\,\varphi(s)\,ds < \infty$ . If $s \le y$ , the next period starts with stock $y - s$ . If $s > y$ , the excess $s - y$ is bought at the penalty rate $p > 0$ and the next period starts with stock $0$ . Costs one period ahead are multiplied by a discount factor $0 < a < 1$ .

Write $f(x)$ for the minimal expected discounted cost from stock $x$ . Enumerating the cases gives Bellman's equation (5.1):

f(x) = \min_{y \ge x} T(y,x,f),

T(y,x,f) = k(y-x) + a\Big[\int_y^\infty p(s-y)\varphi(s)\,ds + f(0)\int_y^\infty \varphi(s)\,ds + \int_0^y f(y-s)\varphi(s)\,ds\Big].

A policy assigns an order-up-to level $y(x) \ge x$ to each stock $x$ . It is optimal when $y(x)$ attains the minimum. The mission takes the equation itself as the model; no stochastic process is built.

Formalization targets

Goal: Chapter V, Theorem 1 (with (4b) corrected)

The equation has exactly one solution $f$ among measurable functions bounded on $[0,\infty)$ . If $ap > k$ , the equation

k = ap\int_{\bar x}^\infty \varphi(s)\,ds + ak\int_0^{\bar x}\varphi(s)\,ds

has exactly one root $\bar x \ge 0$ , and for every $x \ge 0$ the minimum is attained at

y(x) = \max(x, \bar x).

If $ap \le k$ , the minimum is attained at $y(x) = x$ : never order.

Milestones

Chapter IV, Theorem 6 (proportional costs): existence and uniqueness of a solution bounded on every finite interval, its continuity, and convergence of $f_{n+1}(x) = \min_{y\ge x} T(y,x,f_n)$ from any non-negative continuous $f_0$ .
Eq. (5.8): $\bar x$ is the unique root of $\int_0^{y}\varphi(s)\,ds = (ap-k)/a(p-k)$ .
Appendix, Theorem 9: the renewal equation $u(x) = f(x) + \int_0^x u(x-s)\varphi(s)\,ds$ with $\int_0^\infty|\varphi| < 1$ has a unique locally bounded solution. The solution is the limit of successive approximations, satisfies a derivative identity, and is non-negative when $f, \varphi \ge 0$ .
Theorem 3: in the undiscounted $n$ -stage process with $p > k$ , the optimal policy at each horizon is a constant stock level $\bar x_n$ , and $\bar x_n$ increases with $n$ .
Theorem 4: with a fixed stock-out charge $q$ added to the penalty, the constant-stock-level policy is still optimal when the last minimum of

\psi(y) = ky + a\Big[\int_y^\infty [p(s-y)+q]\varphi(s)\,ds - k\int_0^y (y-s)\varphi(s)\,ds\Big]

is its absolute minimum.

Significance

The theorem reduces an infinite-horizon stochastic control problem to a scalar equation. Rewriting it as $\int_0^{\bar x}\varphi = (ap-k)/a(p-k)$ gives the critical-fractile form familiar from the newsvendor problem, with the discount factor entering the fractile. The level depends on the demand law only through its distribution function, and the policy does not depend on the current stock except through $\max(x,\bar x)$ . This is what makes the policy implementable and its parameters estimable from data, the point Bellman makes in § 1. Theorem 3 shows the same structure over a finite horizon, with levels that rise as more periods remain. Theorem 4 marks where the structure starts to depend on the demand density.

As far as a search of the platform shows (queries recorded in the mission files), none of these results has a machine-checked proof. Base-stock theorems on the platform, Veinott's multi-product theorem and Gallego–Özer's advance-demand model, use discrete periods, different excess-demand conventions and different state spaces. They do not cover a continuous-demand, lost-sales-at-penalty, discounted functional equation. Formalizing Chapter V would produce an explicit solution of a nonlinear integral equation of renewal type, a uniqueness theorem for that equation, and a Lean treatment of the renewal equation that other applied-probability missions can reuse.

Difficulty

Two steps resist the obvious argument. First, the minimization is over the unbounded set $y \ge x$ , and the unknown $f$ enters through a convolution with $\varphi$ . The operator $f \mapsto \min_{y\ge x}T(y,x,f)$ is a contraction on bounded functions, which settles uniqueness in the bounded class. Uniqueness among functions bounded only on finite intervals (Chapter IV's class) is not a contraction statement, because the minimization reaches arbitrarily far to the right. Second, optimality of $\max(x,\bar x)$ for $x > \bar x$ requires $f(y) + ky$ to be nondecreasing on $[\bar x,\infty)$ . There $f$ is defined only implicitly, as the solution of a renewal-type equation, and this monotonicity is a positivity statement about that solution, not a consequence of the first-order condition. Checking that the first-order condition holds at $\bar x$ is not enough, and neither is checking that the candidate function satisfies the equation at the single level $\bar x$ .

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter. Integrals over $(y,\infty)$ are Lebesgue integrals and $\int_0^y$ are interval integrals. The equation is stated with an infimum (IsGLB), as Chapter IV writes it, and every policy statement asserts that the minimum is attained (IsLeast) at the stated level. Uniqueness is asserted on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). Solution classes require measurability. This is the standing convention that makes $\int_0^y f(y-s)\varphi(s)\,ds$ meaningful; without it a non-measurable function would make the integral default to $0$ . " $\varphi(s) > 0$ " is read as positivity on $(0,\infty)$ .

Conventions and corrections, each stated in the items:

Theorem 1, (4b) is printed "for $x \ge \bar x$ , $y = \bar x$ ". Read literally, a stock $x > \bar x$ would be "ordered down" to $\bar x < x$ , which violates $y \ge x$ . The proof (p. 163, "the minimum occurs at $y = x$ ") and Theorem 4's (7) give $y = x$ , which is what the goal states. The printed text reads: "(4) a. for 0 ≤ x ≤ x̄, y = x̄, b. for x ≥ x̄, y = x̄."
The goal's uniqueness class is "uniformly bounded functions over $x \ge 0$ " (p. 164). Chapter IV, Theorem 6 is stated in its own larger class.
Theorem 4 gives no range for $q$ ; $q \ge 0$ is assumed. Its phrase "the last minimum of $\psi$ is the absolute minimum" is read as: $\bar x$ minimizes $\psi$ on $[0,\infty)$ and $\psi$ is nondecreasing on $[\bar x,\infty)$ . The bracket of (6), unbalanced in print, is closed at the end.
Theorem 3 assumes " $p > k$ "; $k > 0$ and the density conditions of Theorem 1 are carried over.
Theorem 9's derivative clause assumes $f$ continuously differentiable, where the book says "differentiable". The derivative identity is asserted for $x > 0$ .

A trivializing formalization is ruled out. The goal does not assume the stated policy is optimal, does not assume $f$ is given, and does not take $\bar x$ as a hypothesis. It asserts the existence of the root, the existence and uniqueness of the solution, and attainment of the minimum at $\max(x,\bar x)$ for every $x \ge 0$ .

Theorems 2 (two items, joint density), 5 (one-period delivery lag) and 6 (strictly convex ordering cost) are not part of this mission. Theorem 2 is printed with a sign error in (6) and garbled marginals. Theorem 5 states no hypotheses. Theorem 6's (9b) contradicts itself at $x = \bar x$ . Welcome contributions include a Lean library for the renewal equation (existence by successive approximation, positivity, differentiation under the convolution), which Theorem 9 needs and which is independent of inventory theory, and the contraction estimate for $\min_{y\ge x}T(y,x,\cdot)$ on bounded measurable functions.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter V and Chapter IV § 9. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, I. Glicksberg, O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
K. J. Arrow, T. Harris, J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906813
A. Dvoretzky, J. Kiefer, J. Wolfowitz, The inventory problem: I. Case of known distributions of demand, Econometrica 20(2), 1952, 187–222. https://doi.org/10.2307/1907847
A. F. Veinott, Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

7 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.

Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.

Setting

Two mines, Anaconda and Bonanza, hold amounts of gold $x \ge 0$ and $y \ge 0$ . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction $r_1$ of the gold there and stays in working order with probability $p_1$ , or is destroyed without mining anything with probability $1 - p_1$ . Bonanza has the corresponding data $p_2$ and $r_2$ . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.

The expected return $f(x, y)$ under an optimal policy satisfies the functional equation

f(x,y) = \max\Big[\,A_f(x,y),\; B_f(x,y)\,\Big], \qquad x, y \ge 0, \tag{5.1}

where $A_f(x,y) = p_1\big[r_1x + f((1-r_1)x,\,y)\big]$ is the return of an A-choice followed by optimal continuation and $B_f(x,y) = p_2\big[r_2y + f(x,\,(1-r_2)y)\big]$ that of a B-choice. The $N$ -stage returns are $f_1(x,y) = \max(p_1r_1x,\ p_2r_2y)$ and $f_{N+1} = \max(A_{f_N}, B_{f_N})$ . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.

In the generalization, a use of mine $i$ has $K$ outcomes: outcome $k$ occurs with probability $p_{ik}$ , yields $c_{ik}x_i$ and leaves $c'_{ik}x_i = (1-c_{ik})x_i$ in the mine, and $1 - \sum_k p_{ik}$ is the probability that the machine is destroyed. With $n$ mines the equation is

f(x_1,\dots,x_n) = \max_i \sum_{k=1}^{K} p_{ik}\big[c_{ik}x_i + f(x_1,\dots,c'_{ik}x_i,\dots,x_n)\big]. \tag{4}

"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle $0 \le x \le \bar X$ , $0 \le y \le \bar Y$ (or every box $0 \le x_i \le \bar X_i$ ), per Bellman's footnote 7.

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Under $p_{ik} \ge 0$ , $\sum_k p_{ik} < 1$ , $0 \le c_{ik} \le 1$ , $c_{ik} + c'_{ik} = 1$ , equation (4) has a unique solution bounded on boxes, and at every state $x$ any index maximizing

D_i(x) = \frac{\sum_{k} p_{ik}c_{ik}}{1-\sum_{k} p_{ik}}\;x_i

attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.

Milestones

Theorem 1: for $|p_i| < 1$ and $0 \le r_i < 1$ , (5.1) has a unique solution bounded in every rectangle, and it is continuous on the closed quadrant.
Theorem 2: for $0 \le p_i < 1$ , $0 \le r_i \le 1$ , the solution takes the A-branch when $p_1r_1x/(1-p_1) > p_2r_2y/(1-p_2)$ , the B-branch when the reverse inequality holds, and both on equality.
Theorem 3: the same rule for two mines with $K$ outcomes per use.
Theorem 5: for each $N$ , the $N$ -stage process has exactly two decision regions: a sector along the $x$ -axis where A is optimal and a sector along the $y$ -axis where B is optimal, separated by a ray through the origin.
Theorem 6: as $N$ grows, the regions of $f_N$ move monotonically, and from some $N_0$ on they coincide with those of $f$ .
Theorem 7: if $g$ solves (5.1) with an added term $h$ , then $|f - g| \le \max_R|h|/q$ on every rectangle $R$ , where $q = \min(1-p_1, 1-p_2)$ .

Significance

The index rule reduces the choice among $n$ mines to computing $n$ numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the $N$ -stage process is a word in $n$ letters whose number of candidates grows like $n^N$ . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite $N_0$ , and the stability theorem bounds how much the solution moves when the equation is perturbed.

Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The $n$ -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.

Difficulty

The equation for the boundary between the regions involves the unknown function $f$ , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of $f_N$ generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.

Formalization scope

Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with $n \ge 1$ added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's $N$ ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most $f(x)$ and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for $n$ mines it is BoundedOnBoxes. The $N$ -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's $f_1$ .

Choices made explicit:

Theorem 1 keeps the book's signed range $|p_i| < 1$ (footnote 2), while Theorems 2, 5, 6 and 7 use the range of § 8 and Theorem 2, $0 \le p_i < 1$ , $0 \le r_i \le 1$ .
The goal asserts existence and uniqueness of the bounded solution of (4) together with the index rule. This is how "the solution" is meant in the book; the extension of Theorem 1 to (4) is not a separate numbered result.
The goal's conclusion is the book's: a maximizer of $D$ is optimal. It does not also assert that the other indices are suboptimal.
Theorem 5's printed statement is only "there are two decision regions". It is formalized as the ray-separation statement its proof establishes, and is titled as the precise reading. Theorem 6's "converge in a monotone fashion" is formalized as monotonicity of the regions as sets, in one of the two directions.
Theorem 7 adds the hypothesis that $h$ is bounded in every rectangle, which is what gives the perturbed equation a solution in the class. $\max_R|h|$ is expressed through any bound $M$ of $|h|$ on $R$ .

A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).

Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.

Selected references

Richard Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter II, pp. 61–80. https://doi.org/10.2307/j.ctv1nxcw0f
Richard Bellman, The theory of dynamic programming, Bulletin of the American Mathematical Society 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society, Series B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VII: The (BOR) Assumptions and Positive Recurrence of Optimal PoliciesTextbook

Motivation

Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.

Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.

According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).

Setting

A Markov decision chain consists of a countable state space $S$ , finite nonempty action sets $A_i$ , nonnegative finite costs $C(i,a)$ and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may use the whole history and randomize. For $\alpha\in(0,1)$ the discount value function is $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$ , the infimum of $\sum_t\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i]$ ; the average cost of $\theta$ is $J_\theta(i)=\limsup_n\frac1nE_\theta[\sum_{t<n}C(X_t,A_t)\mid X_0=i]$ and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)$ . All of these lie in $[0,\infty]$ .

For a distinguished state $z$ the relative value is $h_\alpha(i)=V_\alpha(i)-V_\alpha(z)$ . The (SEN) assumptions are: (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded on $(0,1)$ ; (SEN2) $h_\alpha\le M$ for a finite function $M\ge0$ ; (SEN3) $h_\alpha\ge-L$ for a finite constant $L\ge0$ . Under (SEN), $J=\lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ is a finite constant, and a limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some $\beta_n\to1^-$ . The ACOI and ACOE read

J+h(i)\ \ge\ (\text{resp. }=)\ \min_{a\in A_i}\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\qquad i\in S.

For a nonempty set $G$ the first passage time is $T=\min\{n\ge1:X_n\in G\}$ . The class $\Re(i,G)$ consists of the policies that, from $i$ , enter $G$ with probability one in finite expected time $m_{iG}(\theta)$ ; $\Re^*(i,G)$ adds a finite expected first passage cost $c_{iG}(\theta)=E_\theta[\sum_{t<T}C(X_t,A_t)]$ . A (randomized) stationary policy $d$ is $z$ standard if the Markov chain it induces has $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ ; it then has a single positive recurrent class $R_d\ni z$ and a finite constant average cost $J_d$ .

Formalization targets

Goal: Theorem 7.5.6

Assume (BOR): (BOR1) a $z$ standard policy $d$ exists; (BOR2) for some $\varepsilon>0$ the set $D=\{i: C(i,a)\le J_d+\varepsilon\text{ for some }a\}$ is finite; (BOR3) every $i\in D-R_d$ can be reached from $z$ by some $\theta_i\in\Re^*(z,i)$ . Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy $e$ has a positive recurrent state in

D(e)=\{i: C(i,e)\le J+\varepsilon\},

at most $|D(e)|$ positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies $e\in\Re^*(i,D(e)\cap R(e))$ for every $i$ .

Milestones

Lemma 7.4.1: $h_\alpha(i)\le c_{iz}(\theta_i)$ for $\theta_i\in\Re^*(i,z)$ , hence (SEN2).
Lemma 7.4.2: $h(i)\le c_{iG}(\theta)-Jm_{iG}(\theta)+E_\theta[h(X_T)]$ for $\theta\in\Re(i,G)$ under an integrability condition.
Theorem 7.4.3: four sufficient conditions for equality in the ACOI at a state.
Lemma 7.5.2: $J_d=(1-\alpha)\sum_{i\in R}\pi_i(d)V_{d,\alpha}(i)$ for a $z$ standard $d$ .
Proposition 7.5.3: a $z$ standard policy gives (SEN1–2).
Corollary 7.5.4: on $S=\{0,1,\dots\}$ , increasing $V_\alpha$ plus a $0$ standard policy gives (SEN), with nonnegative increasing limit functions.
Proposition 7.5.5: an optimal stationary policy has a positive recurrent state of cost at most $J+\varepsilon$ , reachable from $i$ , when (7.33) holds.
Corollaries 7.5.9 and 7.5.10: the (CAV) and (CAV*) conditions imply (BOR).

Significance

Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.

The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.

Difficulty

The obvious approach to the ACOE is to pass to the limit $\alpha\to1^-$ in the discount optimality equation. Exchanging this limit with $\sum_jP_{ij}(a)h_\alpha(j)$ requires a dominating function, and (SEN2) only gives a pointwise bound $M$ whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy $\Phi$ vanishes along them, which in turn needs finiteness of $c_{iG}$ that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set $D$ is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.

Formalization scope

States form a countable type $S$ ; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, $m_{iG}$ , $c_{iG}$ , $P_\theta(X_T=j)$ , $Q^{(n)}_{ij}$ ) are computed from the history probabilities of the process. $V_\alpha$ , $J_\theta$ , $m_{iG}$ and $c_{iG}$ take values in $[0,\infty]$ ; $m_{iG}=\infty$ when $G$ is missed with positive probability; the first passage time satisfies $T\ge1$ . $h_\alpha$ and $\sum_jP_{ij}(a)h(j)$ are in the extended reals, with the book's convention that a function bounded below has an expectation in $(-\infty,+\infty]$ . Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities $\pi_j=(m_{jj})^{-1}$ are the notions for the chain induced by a (randomized) stationary policy. $J_d$ is the average cost of $d$ from $z$ .

A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which $|D(e)|$ is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.

A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at $T$ ); Abelian limits of $\sum_t\alpha^tP(T=t)$ ; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. doi:10.1002/9780470317037
V. S. Borkar, "On minimum cost per unit time control of Markov chains", SIAM J. Control Optim. 22 (1984), 965–978.
V. S. Borkar, "Control of Markov chains with long-run average cost criterion: the dynamic programming equations", SIAM J. Control Optim. 27 (1989), 642–657.
V. S. Borkar, Topics in Controlled Markov Chains, Pitman Research Notes in Mathematics 240, Longman, 1991.
R. Cavazos-Cadena, "Weak conditions for the existence of optimal stationary policies in average Markov decision chains with unbounded costs", Kybernetika 25 (1989), 145–156.
R. Cavazos-Cadena and L. I. Sennott, "Comparing recent assumptions for the existence of average optimal stationary policies", Oper. Res. Letters 11 (1992), 33–37.
L. I. Sennott, "The average cost optimality equation and critical number policies", Prob. Eng. Inform. Sci. 7 (1993).
L. I. Sennott, "Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs", Operations Research 37 (1989), 626–633. doi:10.1287/opre.37.4.626
K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967.

15 thms2 active usersReviewed

Dynamic Programming Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VI: The (SEN) Assumptions and the Average Cost Optimality InequalityTextbook

Motivation

Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.

Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ , for each state $i$ a finite nonempty action set $A_i$ , a nonnegative finite cost $C(i,a)$ , and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$ . A policy $\theta$ chooses the action at time $n$ at random according to a distribution that may depend on the whole history $(X_0, A_0, \dots, X_n)$ ; a stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$ .

For an initial state $i$ , the $n$ -horizon cost is $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t) \mid X_0 = i]$ , the average cost is $J_\theta(i) = \limsup_{n} v_{\theta,n}(i)/n$ , and the minimum average cost is $J(i) = \inf_\theta J_\theta(i)$ over all policies. A policy is average cost optimal if $J_\theta \equiv J$ . For $\alpha \in (0,1)$ the discounted value function is $V_\alpha(i) = \inf_\theta \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i]$ . All these quantities lie in $[0,\infty]$ .

Fix a distinguished state $z$ and put $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ . The (SEN) assumptions are:

(SEN1) $(1-\alpha)V_\alpha(z)$ is bounded for $\alpha \in (0,1)$ ;
(SEN2) there is a nonnegative finite function $M$ with $h_\alpha(i) \le M(i)$ for all $i$ and $\alpha$ ;
(SEN3) there is a nonnegative finite constant $L$ with $-L \le h_\alpha(i)$ for all $i$ and $\alpha$ .

A limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some sequence $\beta_n \to 1^-$ . If $f_\alpha$ is a stationary policy realizing the discount optimality equation $V_\alpha(i) = \min_a \{C(i,a) + \alpha\sum_j P_{ij}(a)V_\alpha(j)\}$ , a limit point $f$ is a stationary policy with $f_{\beta_n}(i) = f(i)$ for large $n$ , for each $i$ , along some $\beta_n \to 1^-$ .

Formalization targets

Goal: Theorem 7.2.3

Under (SEN), there is a finite constant $J = \lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ independent of $i$ ; limit functions exist, satisfy $-L \le h \le M$ and the average cost optimality inequality (ACOI)

J + h(i) \ge \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)h(j)\Big\}, \qquad i \in S;

every stationary policy realizing the minimum is average cost optimal with $J_e \equiv J$ and $E_e[h(X_n)]/n \to 0$ ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.

Milestones

Proposition 7.1.1: finitely many initial transitions with finite cost do not change $J_\theta$ .
Lemma 7.2.1: a bounded-below solution $(J,h)$ of the ACOI inequality for a stationary $e$ gives $J_e \le J$ .
Proposition B.6: a sequence of functions squeezed between $-L$ and $M$ on a countable set has a pointwise convergent subsequence.
Proposition 7.2.4: (SEN) does not depend on the choice of $z$ .
Proposition 7.7.1: (SEN) $\Rightarrow$ (H*) $\Rightarrow$ (H).
Proposition 7.7.2: the conclusions of Theorem 7.2.3 hold under (H), with a state-dependent lower bound $L(i)$ .

Significance

Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.

The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.

Difficulty

On a finite state space the relative value functions are bounded and the Abelian limit $(1-\alpha)V_\alpha$ can be controlled directly. Here $h_\alpha$ is bounded above only by a function $M$ that may be unbounded, so passing to the limit in the discounted optimality equation $\sum_j P_{ij}(a)h_\alpha(j)$ cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of $E_e[h(X_n)]/n$ for a function $h$ that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.

Formalization scope

The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost $0$ , as the chapter prescribes.

The relative value $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ is computed in EReal, never through a truncated real subtraction: a state with $V_\alpha(i) = \infty$ gives $h_\alpha(i) = +\infty$ , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces $V_\alpha(z) < \infty$ . Sums $\sum_j P_{ij}(a)h(j)$ and expectations $E[h(X_n)]$ of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to $0$ when not summable. The limit $\alpha \to 1^-$ is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences $\alpha_n \to 1^-$ in $(0,1)$ , and the (SEN), (H), (H*) sets are predicates carrying their witnesses $M$ and $L$ .

A development that bounds only $h_\alpha$ as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in $J(i)$ , proves a different and weaker theorem and does not count.

Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality $\limsup(1-\alpha)\sum\alpha^t c_t \le \limsup \frac1n\sum_{t<n}c_t$ (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Chapter 7 (pp. 127–166) and Appendix B. https://doi.org/10.1002/9780470317037
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37 (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, The average cost optimality equation and critical number policies, Probability in the Engineering and Informational Sciences 7 (1993). (Cited in the book's bibliography, p. 321.)
L. I. Sennott, Another set of conditions for average optimality in Markov control processes, Systems & Control Letters 24 (1995) 147–151. (Cited in the book's bibliography.)
R. Cavazos-Cadena, A counterexample on the optimality equation in Markov decision chains with the average cost criterion, Systems & Control Letters 16 (1991) 387–392. (Cited in the book's bibliography.)
S. M. Ross, Non-discounted denumerable Markovian decision models, Annals of Mathematical Statistics 39 (1968) 412–423. (Cited in the book's bibliography.)
H. M. Taylor, Markovian sequential replacement processes, Annals of Mathematical Statistics 36 (1965) 1677–1694. (Cited in the book's bibliography.)
E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control; formalized on Prove2Me in the mission of the same name (Borel state spaces, a different model).

12 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VII: Palm's Theorem for Nonstationary DemandTextbook

Motivation

Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate $\lambda$ and each demanded unit spends an independent, identically distributed resupply time with mean $\bar\tau$ in the pipeline, the number of units in resupply is Poisson with mean $\lambda\bar\tau$ in steady state. Stock levels, backorders and fill rates are all computed from that distribution.

Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time $t$ , the distribution of units in repair at the depot of a two-echelon system.

Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.

Setting

A single item is stocked at one location, and every demand is for one unit.

Demand rate $\lambda(s) \ge 0$ , integrable on bounded intervals, with mean function $m(t) = \int_0^t \lambda(s)\,ds$ .
Demand process: a nonstationary Poisson process with mean function $m$ , with $N(0) = 0$ . $N(t)$ counts demands in $[0,t]$ and $T_0 < T_1 < \cdots$ are the demand epochs.
Resupply times: a unit demanded at time $s$ is resupplied within $w$ time units with probability $G_s(w)$ . Resupply times are nonnegative, have finite expectations, are independent from unit to unit, and are independent of the demand process.
$X(t)$ is the number of units in resupply at time $t$ : demands in $[0,t]$ whose resupply is not complete at $t$ .

The mean of $X(t)$ is

\alpha(t) = \int_0^t \bigl(1 - G_s(t-s)\bigr)\lambda(s)\,ds.

In the compound version (Section 9.2), orders arrive as above and each order is for $Q \ge 1$ units, with a time-stationary law $u_j = P(Q = j)$ . All units of an order share its resupply time, $Y(t)$ counts units demanded in $[0,t]$ , and $u^{(n)}_k$ is the $n$ -fold convolution of $(u_j)$ .

In the two-echelon version (Section 9.3), base $i$ has failure rate $\lambda_i$ . A failure is repaired at the base with probability $r_i$ and at the depot otherwise. Depot repair of a failure occurring at time $u$ takes a deterministic time $D(u)$ with $D(t) + t \ge D(s) + s$ for $s < t$ (no crossing). Write $\tilde t = \inf\{u \ge 0 : D(u) + u > t\}$ .

Formalization targets

Goal: Theorem 13 (p. 216)

For every $t \ge 0$ ,

P\{X(t) = k\} = e^{-\alpha(t)}\frac{\alpha(t)^k}{k!}, \qquad k = 0,1,2,\dots

This is an exact statement at each finite time, not a limit. With constant $\lambda$ and $G_s = G$ it reduces to the finite-time step of Palm's theorem.

Milestones

$E[N(t)] = m(t)$ (Section 9.1, p. 216).
Theorem 12 (p. 216): given $N(t) = n$ , the epochs $T_0, \dots, T_{n-1}$ are distributed as the order statistics of $n$ i.i.d. variables with distribution function $F(x) = m(x)/m(t)$ on $[0,t)$ .
The binomial step of the proof of Theorem 13 (pp. 216–217): $P\{X(t) = k \mid N(t) = n\} = \binom nk p^k(1-p)^{n-k}$ , with $p = \int_0^t (1 - G_s(t-s))\lambda(s)/m(t)\,ds$ .
Section 9.2 (p. 218): $E[Y(t)] = m(t)E[Q]$ and $\operatorname{Var}[Y(t)] = m(t)E[Q^2]$ .
Theorem 14 (p. 218): $P[X(t) = k] = \sum_{n\ge1} u^{(n)}_k e^{-\alpha(t)}\alpha(t)^n/n!$ for $k \ge 1$ , and $e^{-\alpha(t)}$ at $k = 0$ .
Section 9.3.2 (p. 221): $P\{X_0(t) = k\} = e^{-m_0(\tilde t,t)} m_0(\tilde t,t)^k/k!$ with $m_0(\tilde t,t) = \int_{\tilde t}^t \sum_i \lambda_i(u)(1-r_i)\,du$ .

A plain supporting item states that $N(t)$ is Poisson with mean $m(t)$ , the factor the proof of Theorem 13 uses.

Significance

Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, $\sum_{x > s(t)} (x - s(t)) P\{X(t) = x\}$ , and fill rates $P\{X(t) < s(t)\}$ follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.

These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.

Difficulty

The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the $n$ demands in $[0,t]$ " as $n$ independent draws from $F$ and assigns each an independent resupply time with law $G_{\text{draw}}$ . Making this rigorous requires identifying the conditional joint law of the epochs given $N(t) = n$ . The resupply time of the $j$ -th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density $n!/t^n$ on the simplex. Here the density involves $\lambda$ , which may vanish on intervals, and $m$ need not be invertible.

Formalization scope

Demand process. The nonstationary Poisson process is constructed, not postulated. With i.i.d. exponential(1) gaps and unit-rate points $\Gamma_k = A_0 + \cdots + A_k$ , the $k$ -th demand occurs at $T_k = \inf\{s \ge 0 : m(s) \ge \Gamma_k\}$ , and $N(t) = \#\{k : \Gamma_k \le m(t)\}$ .
Resupply times. Resupply times are $\rho(T_k, U_k)$ for a jointly measurable $\rho \ge 0$ and i.i.d. marks $U_k$ independent of the gaps, with $G_s(w) = \nu\{\rho(s,\cdot) \le w\}$ . Every measurable family $G_s$ arises this way, and joint measurability makes $\alpha(t)$ a genuine integral. Independence of resupply times from the demand process is not written in Theorem 12 or 13 but is used in the proof; it is part of the model.
Pinnings and conventions.
- " $\lambda$ integrable" is read as integrable on bounded intervals.
- Time is $t \ge 0$ .
- Theorem 12 assumes $m(t) > 0$ , since $F$ is $0/0$ otherwise, and sets $F = 0$ on $(-\infty,0)$ .
- Conditional probabilities are written as joint probabilities.
- $E[Y(t)]$ is stated in $[0,\infty]$ ; the variance identity assumes $E[Q^2] < \infty$ .
- $\tilde t$ is an infimum over $u \ge 0$ , and $D \ge 0$ .
- Counts are cardinalities, and are $0$ on the null event where they would be infinite.
Corrections. Theorem 14's printed sum starts at $n = 1$ , which gives $P[X(t) = 0] = 0$ . The statement keeps the book's formula for $k \ge 1$ and adds $P[X(t) = 0] = e^{-\alpha(t)}$ . The depot's Poisson demand stream with rate $\sum_i \lambda_i(1-r_i)$ is generated from the bases' processes and independent repair-location choices, not assumed.
Not stated.
- Eqs. (9.1)–(9.2), the FCFS depot backorders owed to base $i$ : the derivation on p. 221 is informal, and (9.1) prints the exponent $s_0(t-1)$ for $s_0(t)-1$ .
- The base analysis of Section 9.3.3.
- The compound law of $Y(t)$ on p. 217, which has the same $n = 0$ omission.
Trivialization ruled out. $X(t)$ is computed from the demand epochs and resupply times, not defined by its law, and resupply times cannot depend on the demand epochs except through the prescribed $G_s$ . Either shortcut would make the goal empty or false.
Infrastructure. The time-changed Poisson construction, its count law, the order-statistics property and marked thinning are reusable well beyond this chapter: in queueing ( $M_t/G_t/\infty$ ), in reliability, and in the stationary Palm mission of this series. Contributions of these general lemmas are welcome.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 9, pp. 215–222. https://doi.org/10.1007/b138879
C. Palm, "Analysis of the Erlang traffic formulae for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
G. J. Feeney and C. C. Sherbrooke, "The (s−1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
R. J. Hillestad and M. J. Carrillo, Models and techniques for recoverable item stockage when demand and the repair processes are nonstationary — Part I: Performance measurement, Report N-1482-AF, RAND Corporation, 1980.
G. B. Crawford, Palm's theorem for nonstationary processes, Report R-2750-RC, RAND Corporation, 1981.
M. J. Carrillo, Generalizations of Palm's theorem and Dyna-METRIC's demand and pipeline variability, Report R-3698-AF, RAND Corporation, 1989.

11 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains IV: Backorder Convexity and Everett's TheoremTextbook

Motivation

Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the $(s-1, s)$ policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level $s$ . A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.

The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson $(s-1,s)$ model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.

Setting

A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate $\lambda > 0$ . An order is for $j$ units with probability $u_j$ , where $u_0 = 0$ and the mean order size $\bar u = \sum_j j u_j$ is finite (compound Poisson demand; simple Poisson demand is $u_1 = 1$ ). Resupply times have mean $\bar\tau > 0$ . The steady-state probability that $x$ units are in resupply is

p(0 \mid \lambda\bar\tau) = e^{-\lambda\bar\tau}, \qquad p(x \mid \lambda\bar\tau) = \sum_{j \ge 1} e^{-\lambda\bar\tau}\frac{(\lambda\bar\tau)^j}{j!}\,u^{(j)}_x \quad (x \ge 1),

where $u^{(j)}_x$ is the probability that $j$ orders total $x$ units. In this mission $p(\cdot \mid \lambda\bar\tau)$ is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is $\mu = \lambda\bar\tau\bar u$ , and the book also writes $p(x \mid \mu)$ .

For a stock level $s \in \{0, 1, 2, \dots\}$ :

the ready rate is $R(s) = \sum_{x \le s} p(x \mid \lambda\bar\tau)$ ;
the expected backorders are $B(s) = \sum_{x > s}(x - s)\,p(x \mid \lambda\bar\tau)$ ;
the expected on-hand inventory is $\sum_{x \le s}(s - x)\,p(x \mid \lambda\bar\tau)$ ;
under simple Poisson demand the fill rate is $F(s) = \sum_{x < s} p(x \mid \lambda\bar\tau)$ .

Forward differences are $\Delta f(s) = f(s+1) - f(s)$ and $\Delta^2 f(s) = \Delta f(s+1) - \Delta f(s)$ ; discrete convexity means $\Delta^2 f \ge 0$ .

With $n$ items, unit costs $c_i > 0$ and budget $b$ , Problem 4 (3.40) is

\min \sum_i B_i(s_i) \quad \text{s.t.} \quad \sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le b,\quad s_i \in \{0,1,\dots\}.

For a multiplier $\theta > 0$ , the item-wise criterion defines $s_i^*(\theta)$ as the least $s$ with $\sum_{x \le s} p(x \mid \mu_i) \ge 1/(1 + \theta c_i)$ , and $C(\theta) = \sum_i c_i\,[s_i^*(\theta) - \mu_i + B_i(s_i^*(\theta))]$ .

Formalization targets

Goal: the Lagrangian stock levels solve Problem 4

For every $\theta > 0$ , each $s_i^*(\theta)$ exists and

\sum_i c_i\,[s_i - \mu_i + B_i(s_i)] \le C(\theta) \ \Longrightarrow\ \sum_i B_i(s_i^*(\theta)) \le \sum_i B_i(s_i)

for every vector $s$ of nonnegative integer stock levels. That is, $s^*(\theta)$ is optimal for Problem 4 at budget $b = C(\theta)$ . This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.

Milestones

Section 3.3, p. 53: $\Delta F(s) = p(s \mid \lambda\bar\tau)$ and $\Delta^2 F(s) = p(s \mid \lambda\bar\tau)\,(\lambda\bar\tau/(s+1) - 1)$ , so under simple Poisson demand $F$ is discretely concave exactly on $s \ge \lfloor\lambda\bar\tau\rfloor$ (resp. $s \ge \lambda\bar\tau - 1$ for integer $\lambda\bar\tau$ ).
Section 3.3, p. 55: $\Delta B(s) = -(1 - R(s))$ and $\Delta^2 B(s) = p(s+1 \mid \lambda\bar\tau)$ .
Theorem 10 (Everett), p. 57.
Section 3.4.2, p. 60: $E[\text{On-hand}] = s - \lambda\bar\tau\bar u + B(s)$ .
Section 3.4.2, p. 61: the least $s$ with $R(s) \ge 1/(1+\theta c)$ minimizes $f(s) = (1 + \theta c)B(s) + \theta c s$ .
Section 3.4.2, p. 61: $s^*(\theta)$ and $C(\theta)$ are nonincreasing in $\theta$ .
Section 3.4.2, p. 63: at $\theta_{\max} = \max_i c_i^{-1}(1/p(0 \mid \mu_i) - 1)$ every $s_i^*(\theta_{\max}) = 0$ .
Section 3.4.3, p. 65: every solution produced by the greedy marginal-analysis rule for Problem 5 (3.41), maximum average fill rate subject to $\sum_i c_i s_i \le b$ and $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ , is optimal at the budget it uses.

Significance

The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, $s \ge \lfloor\lambda\bar\tau\rfloor$ , is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.

All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.

Difficulty

The algebra of first differences is elementary; the difficulties are elsewhere. $B(s)$ is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying $\sum_x x\,p(x \mid \lambda\bar\tau)$ with $\lambda\bar\tau\bar u$ , requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of $s^*(\theta)$ requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every $F_i$ is concave; dropping the floor constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ makes it false.

Formalization scope

Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields $\lambda, \bar\tau > 0$ , an order-size distribution $u$ with $u_0 = 0$ , $u_j \ge 0$ , $\sum_j u_j = 1$ , and summable $j u_j$ (the finite mean is added: without it $B$ is infinite). Expected on-hand inventory is the finite sum $E[(s - X)^+]$ . Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).

Pinnings and deviations, each stated in the item's Formalization Note:

$\theta > 0$ and $c > 0$ . The book allows $\theta \ge 0$ in (3.38); at $\theta = 0$ the threshold $1$ is never reached and $f = B$ has no minimizer.
Theorem 10 without convexity and for an arbitrary set $S$ : the book assumes $f, g$ convex, but its proof does not use it and the applications are to integer vectors (labelled generalization).
$B$ 's identities for compound Poisson demand. The book derives them under simple Poisson demand and uses them for compound demand on p. 61; strict convexity and strict decrease are stated only for simple Poisson demand, as in the book.
Optimality is always against every feasible vector, never an infimum; the greedy procedure is a relation on sequences, covering every tie-breaking rule.
Problem 5 keeps the constraints $s_i \ge \lfloor\lambda_i\bar\tau_i\rfloor$ .

A trivializing formalization is ruled out: the goal is stated for the book's own backorder function $B$ built from the compound Poisson law, not for an arbitrary convex function nor for a $B$ defined through its differences.

Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 3, pp. 47–65. https://doi.org/10.1007/b138879
H. Everett III, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Operations Research 11(3):399–417, 1963. https://doi.org/10.1287/opre.11.3.399
B. L. Fox and D. M. Landi, Searching for the multiplier in one-constraint optimization problems, Operations Research 18(2):253–262, 1970. https://doi.org/10.1287/opre.18.2.253
G. J. Feeney and C. C. Sherbrooke, The (s−1, s) inventory policy under compound Poisson demand, Management Science 12(5):391–411, 1966. https://doi.org/10.1287/mnsc.12.5.391

13 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Introduction to the Scenario Approach II: Violation Guarantees after Discarding k ConstraintsTextbook

Motivation

Decisions under uncertainty are often required to satisfy a constraint $\theta \in \Theta_\delta$ that depends on a random parameter $\delta$ , and requiring it for every possible $\delta$ is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of $\delta$ by $N$ independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.

Enforcing all $N$ sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards $k$ of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.

Setting

A decision $\theta$ ranges over $\mathbb R^d$ (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain $\Theta$ and a linear cost $c^{\mathsf T}\theta$ . An uncertain parameter $\delta$ takes values in a measurable space $\Delta$ with probability $\mathbb P$ , and each $\delta$ determines a closed convex constraint set $\Theta_\delta$ . The violation probability of a decision is

V(\theta) = \mathbb P\{\delta \in \Delta : \theta \notin \Theta_\delta\}.

Given independent samples $\delta_1,\dots,\delta_N$ with joint law $\mathbb P^N$ , the scenario program minimizes $c^{\mathsf T}\theta$ over $\theta \in \Theta \cap \bigcap_{i=1}^N \Theta_{\delta_i}$ . For a set $I$ of indexes, the program without the constraints in $I$ minimizes the same cost over $\Theta \cap \bigcap_{i \notin I} \Theta_{\delta_i}$ ; its solution is written $\theta^*_I$ . A removal procedure selects, as a function of the whole sample, a set of $k$ indexes, and $\theta^*_k$ denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the $k$ removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that $\Theta$ and every $\Theta_\delta$ are convex and closed, and Assumption 3.6, that for every sample size $m$ and every sample the scenario program has exactly one solution.

Formalization targets

Goal: Theorem 3.9

For $N \ge d$ , under Assumptions 3.4 and 3.6, for every removal procedure and every $\varepsilon \in [0,1]$ ,

\mathbb P^N\{V(\theta^*_k) > \varepsilon\} \le \binom{k+d-1}{k} \sum_{i=0}^{k+d-1} \binom Ni \varepsilon^i (1-\varepsilon)^{N-i}.

The bound depends on the problem only through $d$ , and on the removal procedure not at all. For $k = 0$ it is Theorem 3.7.

Milestones

Theorem 3.7 (no removal): $\mathbb P^N\{V(\theta^*) > \varepsilon\} \le \sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ , used for the program with the $N-k$ kept constraints.
Eq. (5.11): up to a zero probability set, the event $\{V(\theta^*_k) > \varepsilon\}$ is contained in the union over all $k$ -element index sets $I$ of the events " $\theta^*_I$ violates all constraints in $I$ and $V(\theta^*_I) > \varepsilon$ ".
Eq. (5.13): for a fixed $I$ , the probability of that event equals $\int_{(\varepsilon,1]} \alpha^k F_V(d\alpha)$ , where $F_V$ is the law of $V(\theta^*_I)$ .
Eq. (5.14) and Theorem 3.9 for $d = 2$ : the book's complete proof in the plane.
Eqs. (3.15)–(3.17) and the conclusion of Section 3.3.1: with the explicit level $\varepsilon_k$ of (1.9), the right-hand side of (3.13) is at most $\beta$ .
Theorem 1.2: with probability at least $1-\beta$ , $V(\theta^*_k) \le \varepsilon_k$ , where

\varepsilon_k = \frac{k}{N} + \left[\frac{\sqrt k}{N} + \frac{\sqrt k+1}{N}\left((d-1)\ln(k+d-1) + \frac{d-1}{\sqrt k} + \ln\frac1\beta\right)\right].

Significance

Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of $k$ before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when $k/N$ is held fixed, the violation exceeds the empirical risk $k/N$ by a margin of order $\ln N/\sqrt N$ , only slightly worse than the $1/\sqrt N$ rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).

Theorem 3.9 is proved in the literature for general $d$ (Campi and Garatti, 2011); the textbook proves it for $d = 2$ . To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.

Difficulty

The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to $\theta^*_k$ directly. The argument must pass through all $\binom Nk$ fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor $\binom Nk$ and does not give (3.13). For a fixed index set, the probability that the $k$ removed scenarios are all violated involves the distribution of $V(\theta^*_I)$ , which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function $\alpha \mapsto \alpha^k$ is needed. In general dimension the combinatorial constant $\binom{k+d-1}{k}$ comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin d), samples of size $m$ are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:

$d \ge 1$ , $d \le N$ , $k \le N$ and $\varepsilon \in [0,1]$ ;
Assumption 3.6 for every $m$ , including $m = 0$ , and for every sample (not almost every);
the removed constraints are violated with probability one (∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for $1 \le k < N$ (on a sample with all $\delta_i$ equal a kept constraint coincides with a removed one) and would make the results vacuous;
measurability, which the book glosses over (p. 33): the constraint relation $\{(\theta,\delta) : \theta \in \Theta_\delta\}$ is jointly measurable, the solution map of the scenario program with $m$ constraints is measurable for every $m$ , and $\theta^*_k$ is measurable;
for Theorem 1.2 and Section 3.3.1: $k \ge 1$ (formula (1.9) divides by $\sqrt k$ ), $N \ge 1$ , $\beta \in (0,1)$ ; Section 3.3.1 additionally assumes $\varepsilon_k \le 1$ , the range in which its chain of inequalities holds.

Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for $d = 2$ only, as in the book.

A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict $V(\theta^*_k) > \varepsilon$ ; a statement for one fixed rule, or with $\theta^*_k$ unconstrained, would be a different theorem.

A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size $N-k$ , the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general- $d$ counting argument of the cited paper, are welcome.

Selected references

M. C. Campi and S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
M. C. Campi and S. Garatti, A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality, Journal of Optimization Theory and Applications 148(2), 257–280, 2011. https://doi.org/10.1007/s10957-010-9754-6
M. C. Campi and S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 1211–1230, 2008. https://doi.org/10.1137/07069821X
G. C. Calafiore and M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

13 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Introduction to the Scenario Approach IV: The FAST Algorithm Keeps the Beta Bound and Adds a Factor (1−ε)^{N₂}Textbook

Motivation

The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample $N$ instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in $N$ and in the number $d$ of optimization variables. To reach a failure level $\varepsilon$ with confidence $1-\beta$ , the number of scenarios grows roughly like $\frac{2}{\varepsilon}\big(\ln\frac1\beta+d-1\big)$ (Theorem 1.1 of the book). The product of $d$ and $1/\varepsilon$ is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.

FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number $N_1$ of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers $N_2$ further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.

Timeline:

2006, Calafiore and Campi: violation bounds for the solution of convex scenario programs.
2008, Campi and Garatti: the exact binomial bound, tight for fully supported problems (Theorem 3.7 of the book).
2014, Carè, Garatti and Campi: FAST and its two-stage bound, Eq. (8.5).
2018, Campi and Garatti's textbook, §8.3, the source of this mission.

Setting

Let $\Delta$ be a measurable space carrying a probability measure $\mathbb P$ , and let $\ell(\nu,\delta)$ be a real loss of a decision $\nu\in\mathbb R^{d-1}$ under the uncertain parameter $\delta\in\Delta$ . As a standing assumption of the book, $\ell(\cdot,\delta)$ is convex for every $\delta$ .

Given scenarios $\delta_1,\dots,\delta_m$ drawn independently from $\mathbb P$ , the scenario program (1.4) is

\min_{\nu\in\mathbb R^{d-1}}\ \Big[\max_{i=1,\dots,m}\ \ell(\nu,\delta_i)\Big].

Its solution is $\nu^*$ and its optimal value $\ell^*$ . Assumption 3.6 requires that for every $m$ and every sample the solution exist and be unique. The pair $(\nu,\ell)$ has $d$ components, and $d$ is the number that enters every bound.

The risk (Definition 8.2) of a decision $\nu$ with cost level $\ell$ is

R(\nu,\ell)=\mathbb P\{\delta\in\Delta:\ \ell(\nu,\delta)>\ell\},

the probability that a new instance costs more than promised. It is the violation $V(\nu,\ell)$ of the epigraphic constraint $\ell\ge\ell(\nu,\delta)$ .

FAST takes $N_1+N_2$ independent scenarios. It solves (1.4) with the first $N_1$ of them, obtaining $\nu^*_{N_1}$ . In the detuning step it then sets

\ell^*_F=\max_{i=1,\dots,N_1+N_2}\ \ell(\nu^*_{N_1},\delta_i),

the smallest level that covers every scenario seen. The output is $(\nu^*_F,\ell^*_F)$ with $\nu^*_F=\nu^*_{N_1}$ .

Formalization targets

Goal: Theorem 8.5, Eq. (8.5)

For every $\varepsilon\in[0,1]$ ,

\mathbb P^{N_1+N_2}\{V(\nu^*_F,\ell^*_F)>\varepsilon\}\ \le\ (1-\varepsilon)^{N_2}\sum_{i=0}^{d-1}\binom{N_1}{i}\varepsilon^i(1-\varepsilon)^{N_1-i}.

No relation between $N_1$ and $d$ is required. When $N_1<d$ the sum equals $1$ and the bound reads $(1-\varepsilon)^{N_2}$ .

Milestone: Theorem 3.7 for program (1.4)

The first stage is an ordinary scenario program with $N_1$ scenarios. For $N\ge d$ ,

\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\ \le\ \sum_{i=0}^{d-1}\binom{N}{i}\varepsilon^i(1-\varepsilon)^{N-i},

that is, $R(\nu^*,\ell^*)$ is dominated by a $B(d,N-d+1)$ distribution (recalled on p. 90).

Milestone: the $N_2$ rule

For $\varepsilon,\beta\in(0,1)$ , $N_2\ge\frac1\varepsilon\ln\frac1\beta$ makes the right-hand side of (8.5) at most $\beta$ (p. 95).

Significance

The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With $N_1=Kd$ (the book suggests $K\approx20$ ) and $N_2\ge\frac1\varepsilon\ln\frac1\beta$ , the total number of scenarios is $Kd+\frac1\varepsilon\ln\frac1\beta$ . This is additive in $d$ and $1/\varepsilon$ rather than multiplicative, and the added $N_2$ scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: $\ell^*_F$ is in general higher than the value a classical scenario program with the same confidence would return.

Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The $N_2$ rule is an elementary but explicit sample-size certificate.

Difficulty

The obvious route treats the detuning step as a fresh scenario program with $N_1+N_2$ scenarios and applies Theorem 3.7 to it. That fails: $\nu^*_F$ is not the solution of that program, and Theorem 3.7 with $N_1+N_2$ scenarios gives a bound that is not of the product form (8.5). The level $\ell^*_F$ depends on all $N_1+N_2$ scenarios at once, including those that determined $\nu^*_{N_1}$ , and the map $c\mapsto R(\nu,c)$ is monotone but need not be continuous, so the event $V(\nu^*_F,\ell^*_F)>\varepsilon$ is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.

Formalization scope

Lean representation:

The decision space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin n); the book's $d$ is written $n+1$ , never with natural-number subtraction.
A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same $\mathbb P$ defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.
The maximum in (1.4) and in $\ell^*_F$ is Finset.sup' over a nonempty index set. $\ell^*_F$ runs over all $N_1+N_2$ scenarios, not over the $N_2$ new ones only.
The risk is (P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event $V>\varepsilon$ of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.
The first-stage solution is a map νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.

Hypotheses the book leaves implicit, stated explicitly:

$\ell(\cdot,\delta)$ is convex for every $\delta$ (standing assumption, p. 6).
Existence and uniqueness of the solution (Assumption 3.6) for every $m\ge1$ and every sample. The program with no scenario has no minimum, so $m=0$ is excluded.
$N_1\ge1$ , since the first stage needs a scenario.
$\varepsilon\in[0,1]$ ; for $\varepsilon>1$ the factor $(1-\varepsilon)^{N_2}$ can be negative.
The loss is jointly measurable in $(\nu,\delta)$ and the first-stage solution map is measurable. The book glosses over measurability (p. 6, footnote 1; p. 33).

A formalization that bounds only the $N_2$ new scenarios is ruled out, because $\ell^*_F$ is defined as a maximum over all $N_1+N_2$ scenarios. So is one that takes $\ell^*_F$ as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.

A complete development needs the scenario program in loss form, product-measure conditioning on $\Delta^{N_1}\times\Delta^{N_2}$ , and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018, §8.3 and Theorem 3.7. https://doi.org/10.1137/1.9781611975444
A. Carè, S. Garatti, M. C. Campi, FAST—Fast Algorithm for the Scenario Technique, Operations Research 62(3):662–671, 2014. https://doi.org/10.1287/opre.2014.1257
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3):1211–1230, 2008. https://doi.org/10.1137/07069821X
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5):742–753, 2006. https://doi.org/10.1109/TAC.2006.875041

6 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory IV: PASTA and the Formulas of Palm CalculusTextbook

PASTA and the Formulas of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.

The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.

The goal

Theorem 3.3.1 (p.211) is the one that says when the two views coincide.

This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the θ_t-framework.

E⁰_A[f(Z(0))] = E[f(Z(0))]                                                            (3.3.1)

for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f, whenever A admits the constant F_t-intensity λ; and, under ergodicity,

lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds .                       (3.3.2)

The "some care" is the word predictable. PASTA is false without it: an arrival that changes the state it then observes does not see the time average, and that is exactly what predictability — measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a — rules out.

The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two are equivalent, but that equivalence is a remark on the page and not part of this theorem.

Why it earns its place: Pollaczek–Khinchin

§3.4 derives formulas from conservation equations. Applying the rate conservation principle of Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula

iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) ,                (3.4.44)

an identity between a stationary expectation and a Palm expectation of the workload just before an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and

E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) ,                                   (3.4.45)

the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.

The rest of the chapter

§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.

§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by thinnings of the entrance processes of two disjoint sets.

§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.

What this mission provides

Nothing here is on the platform or in Mathlib. The nearest platform item, queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the Palm identity for a stationary ergodic marked point process, derived from the inversion formula (1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a pathwise limit. Different framework, different hypotheses, and neither implies the other.

Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.

Formalization scope

PASTA carries both displays. (3.3.1) is an equality in [0, ∞] for every non-negative measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one common limit, so both limits exist. Predictability is measurability for the predictable σ-field P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis, because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity, E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".
Takács (3.4.44) and Pollaczek–Khinchin (3.4.45) are stated for every real u, and for u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for {W(t−)}, and it asserts that its denominator is non-zero.
Lemma 3.2.1 asserts both closed forms of E_α R. The chain is irreducible, F is non-empty, and hitting times are counted from time 0.
Theorem 3.2.1 asserts the equality in (3.2.43), the convergence to 1, and E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.
Lemmas 3.5.1 and 3.5.2 are stated for the full on-off model of §3.5.3. The on-off point processes are independent, their on periods, off periods and fluid functions are i.i.d. and independent, P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞]. Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.

A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.

14 thms2 active usersReviewed

Probability

Missions

Air Travel Demand and Airline Seat Inventory Management III: Gaussian EMSR Protection Levels and Their SensitivityTextbook

Why protection levels and their inputs matter

Setting

Formalization targets

Goal: the Gaussian protection level and its sensitivity to σ^\hat\sigmaσ^

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Minimax Regret Bounds for Reinforcement Learning I: High-Probability Regret Bound for UCBVI with a Chernoff–Hoeffding BonusResearch Paper

Motivation

Setting

Formalization targets

Theorem 1: UCBVI-CH regret

Supporting results

Significance

Difficulty

Formalization scope

Selected references

Secretary Problems: Weights and Discounts 4: A Threshold Rule Earns Z/4 for Any Z ≤ E[OPT] in the Discounted Secretary ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.7

Milestones (in the order of the paper's proof, p. 8)

Significance

Difficulty

Formalization scope

Selected references

Secretary Problems: Weights and Discounts 2: An Ω(log n / log log n) Lower Bound on the Competitive Ratio of the Discounted Secretary ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.3 in the form its proof establishes

Milestones

Significance

Difficulty

Formalization scope

Selected references

Correlated Equilibrium as an Expression of Bayesian Rationality II: Two-Person Correlated Equilibrium Distributions Are the Solutions of Linear InequalitiesResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Intermediate Disorder Regime for Directed Polymers in Dimension 1+1: The Rescaled Partition Function Converges in Law to a Wiener ChaosResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 (second bullet), proved as Proposition 5.4

Modified partition function: Proposition 5.3 (Theorem 2.1, first bullet)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Analysis of Thompson Sampling for the Multi-armed Bandit Problem 1: Logarithmic Regret for Two ArmsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 3)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fundamentals of Queueing Theory X: Uniformization of Continuous-Time Markov ChainsTextbook

Motivation

Setting

Formalization targets

Goal: the randomization formula with its truncation bound (Eqs. (8.9)–(8.12))

Milestones

Significance

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$