All missions

Motivation

Ride-sharing platforms match passengers who request rides at different times and places. Three features of that problem are hard to separate: two passengers far apart yield a poor match, two requests far apart in time cannot be matched at all, and the platform does not know future demand. Ashlagi, Burq, Dutta, Jaillet, Saberi and Sholley (arXiv:1808.03526v1, published in Mathematics of Operations Research, 2023, as Edge-Weighted Online Windowed Matching) reduce these features to a graph matching problem on an arbitrary, not necessarily bipartite, graph.

The classical online bipartite matching literature takes $d = 0$: a vertex must be matched on arrival. Emek, Kutten and Wattenhofer (STOC 2016) and Huang et al. (STOC 2018) study delayed decisions in other models. The present model fixes a uniform deadline, and the weights are arbitrary.

Setting

A weighted graph has vertices $1, \dots, n$ and weights $v_{ij} \ge 0$ on undirected pairs. Vertices arrive one per period, vertex $i$ in period $\sigma(i)$, and the Adversarial Order setting assumes $\sigma(i) = i$. The weight of a pair is observed only when its later vertex arrives.

For a deadline $d \ge 1$, the online graph $G_{d,\sigma}$ keeps the edge $(i, j)$ exactly when $|\sigma(i) - \sigma(j)| \le d$. Vertex $i$ becomes critical at period $\sigma(i) + d$: the algorithm must match it then or let it depart. The benchmark $\mathrm{OFF}$ is the maximum weight of a matching of $G_{d,\sigma}$. A randomized online algorithm is $c$-competitive if its expected total weight is at least $c \cdot \mathrm{OFF}$.

Postponed Greedy (PG, Algorithm 3) gives each vertex $k$ a virtual seller $s_k$ with price $p(s_k)$ and a virtual buyer $b_k$. On arrival, $b_k$ bids once on the seller $s$ of largest margin $v_{s,b_k} - p(s)$. If the margin is positive, $b_k$ becomes the tentative match $m(s)$, displacing any earlier buyer, and $p(s)$ rises to $v_{s,b_k}$. The maximal margin is $q(b_k)$. When $k$ becomes critical with $m(s_k) = b_l$, a fair coin decides $k$'s status if it is still undetermined. A seller finalizes $(k, l)$ and collects $v_{k,l}$, and in either case $l$ receives the opposite status.

Formalization targets

Goal: Theorem 3.3

The theorem is stated for every $n$, every $d \ge 1$, all $v \ge 0$ and every tie-breaking rule for the $\operatorname{argmax}$, as four clauses. Every finalized pair is an edge of $G_{d,\sigma}$, for every outcome $\omega$ of the coins. The finalized pairs are vertex-disjoint, for every $\omega$. The expected reward satisfies

$$\mathrm{PG} = \frac{1}{2^n} \sum_{\omega} \mathrm{reward}(\omega) \ \ge\ \frac14\, \mathrm{OFF}.$$

And the state after $t$ periods depends only on the weights among vertices arrived by then and on the coins of vertices already critical.

Milestones

The proof of Theorem 3.3 uses no numbered result, so the milestones are its unnumbered claims, in proof order.

1. The virtual run $S, B, p, m, q$ reads no coin.
2. The matches $m^f$ form a collection of disjoint paths in $G_{d,\sigma}$.
3. Statuses alternate along a path, and $(k, l)$ is finalized exactly if $k$ is a seller.
4. A vertex with a final match is a seller with probability exactly $1/2$.
5. $\mathrm{PG} = \tfrac12 \sum_k p^f(s_k)$.
6. $\sum_s p^f(s) = \sum_b q(b)$.
7. $q(b_j) \ge v_{ij} - p(s_i)$ when $j$ arrives, for $i < j$ with $j - i \le d$.
8. $p(s)$ increases over time.
9. $\{p^f(s_k) + q(b_k)\}_k$ is feasible for the dual of the offline matching program.
10. $\mathrm{OFF}$ is at most the value of any feasible dual solution.

Significance

The result. Theorem 3.3 gives a constant competitive ratio for matching on arbitrary graphs with arbitrary non-negative weights and an adversarial arrival order. The paper's Figure 1 shows that no deterministic algorithm achieves a constant ratio, and the paper shows that no algorithm exceeds $1/2$. The same algorithm underlies the paper's extension to stochastic departures.

The formalization. The theorem is proved in the paper, and at the time of writing no machine-checked proof exists on this platform. The mission produces an executable-style specification of a randomized online algorithm, with the word "online" as a theorem clause, not a comment. It also produces a primal-dual argument for general-graph matching in the shape used by auction-style online algorithms. Weak duality for vertex potentials (milestone 10) is stated for every finite simple graph.

Difficulty

The obvious approach, assigning each vertex a seller or buyer role by an independent coin, loses a factor $4$ on each edge and gives only $1/8$ (Corollary 3.2). Postponed Greedy gains the factor $2$ by correlating the roles along paths of the virtual $2$-matching.

That correlation is the central difficulty. Whether $k$ is a seller is not one coin: it is the coin at the head of $k$'s path, flipped once per step along the path, and which vertices form that path depends on prices set after $k$ arrived. The claim "with probability exactly $1/2$" (milestone 4) needs the path structure to be independent of the coins (milestone 1), and it fails for a vertex with no final match. A vertex with no match is never a seller, which the proof's sentence leaves implicit, so milestone 4 is stated only for matched vertices.

Two further points are easy to get wrong. A buyer displaced from a seller never bids again, so the tentative matching need not be a maximum-weight matching of the virtual graph. The price of a seller rises while the seller is present, and the dual constraint for $(i, j)$ reads the price at the moment $j$ arrives, so the constraint at the final prices needs monotonicity (milestone 8).

Formalization scope

Vertices are Fin n, 0-based: vertex $k$ arrives in period $k$ and becomes critical in period $k + d$. Weights are v : Sym2 (Fin n) → ℝ. The run is a fold over the periods $0, \dots, n + d - 1$, with the arrival processed before the criticality within a period. Both choices are forced: processing criticality first makes the theorem false on $n = 2$, $d = 1$, and stopping at period $n$ collects nothing on $n = 2$, $d = 2$. Margins read onlineWeight, which is $0$ off the edges of the online graph, so the seller $s_k$ has margin $0$ for $b_k$. Coins are ω : Fin n → Bool, uniform, and the expectation is $2^{-n} \sum_\omega$. The benchmark reuses the published ProphetMatchingEFGT.optWeight, a finite maximum over matchings of a SimpleGraph.

The tie-breaking rule is a free parameter of the theorem, restricted to choose a maximizer and to see the arriving vertex, the seller set and the margins, but no coin. The reward is a sum over the finalized pairs, not the quantity $\tfrac12 \sum_k p^f(s_k)$, and the benchmark is on $G_{d,\sigma}$ and on no other graph. Each of these excludes a trivializing reading.

A complete development needs invariants of the state machine and no theory beyond Mathlib: finite sums, Finset and Sym2 manipulation, and counting on Fin n → Bool. Milestone 10 is reusable beyond this mission. Contributions to any milestone are welcome, in any order.

Selected references

• I. Ashlagi, M. Burq, C. Dutta, P. Jaillet, A. Saberi, C. Sholley, Maximum Weight Online Matching with Deadlines, arXiv:1808.03526v1, 2018. https://arxiv.org/abs/1808.03526
• J. Feldman, N. Korula, V. Mirrokni, S. Muthukrishnan, M. Pál, Online ad assignment with free disposal, WINE 2009, pp. 374–385. https://doi.org/10.1007/978-3-642-10841-9_34
• Y. Emek, S. Kutten, R. Wattenhofer, Online matching: haste makes waste!, STOC 2016, pp. 333–344. https://doi.org/10.1145/2897518.2897557
• Z. Huang, N. Kang, Z. G. Tang, X. Wu, Y. Zhang, X. Zhu, How to match when all vertices arrive online, STOC 2018, pp. 17–29. https://doi.org/10.1145/3188745.3188858

Motivation

In a coordination game on a graph, every player is a node and chooses a colour, and a node is rewarded for agreeing with its neighbours. These games model the adoption of a common standard, clustering, and the stabilisation of distributed protocols. When the graph is directed, the dynamics change sharply. A node is paid only by its in-neighbours and pays nothing back. Nash equilibria may fail to exist, and even on a single directed cycle, improvement dynamics can cycle forever. Apt, Simon and Wojtczak (arXiv:1910.02693v2, published in Mathematics of Operations Research, 2022) study when, from every starting configuration, some short sequence of profitable unilateral moves reaches a Nash equilibrium. Their two main graph classes come from networking. Simple cycles model token rings. Open chains of cycles model Ethernet ring protection (ITU-T G.8032), in which rings are joined in a sequence and consecutive rings share a single node.

Timeline:

• 2014–2017: Apt, de Keijzer, Rahn, Schäfer and Simon study coordination games on undirected graphs (WINE 2014; International Journal of Game Theory 46(3), 2017).
• 2016: Apt, Simon and Wojtczak, Coordination games on directed graphs (TARK 2015, EPTCS 215, arXiv:1606.07517), and Simon and Wojtczak, Efficient local search in coordination games on graphs (IJCAI 2016), report the first results for the directed case.
• 2019–2022: the journal version (arXiv:1910.02693v2) improves the bounds. It gives polynomial bounds on improvement paths for simple cycles (Theorems 3, 5, 7, 9) and open chains (Theorem 15), and proves NP-completeness of Nash-equilibrium existence in general (Theorem 36). Weighted open chains are not treated here; the paper points to the IJCAI paper for them (p.34).

Setting

Fix a finite set $M$ of colours. A coordination game is given by a directed graph on a finite vertex set $V$ without self-loops, a positive weight $w_{j\to i}$ on each edge, a colour assignment giving every node $i$ a non-empty set $C(i)\subseteq M$, and bonuses $\beta(i,c)\in\mathbb N$. A joint strategy $s$ picks $s_i\in C(i)$ for every node, and the payoff of node $i$ is

$$p_i(s)=\sum_{j\in N_i,\ s_j=s_i} w_{j\to i}+\beta(i,s_i),$$

where $N_i$ is the set of in-neighbours of $i$. Unless stated otherwise, graphs are unweighted ($w=1$) and there are no bonuses ($\beta=0$).

A node plays a best response if no colour in $C(i)$ gives it a higher payoff. A Nash equilibrium is a joint strategy in which every node plays a best response. An improvement step $s\to s'$ changes the colour of a single node to one that strictly increases that node's payoff. A game ensures improvement paths of length at most $X$ if from every joint strategy $s_0$ there are $s_0\to s_1\to\dots\to s_L$, $L\le X$, all improvement steps, with $s_L$ a Nash equilibrium.

A simple cycle is $1\to2\to\dots\to n\to1$. An open chain of $m\ge2$ cycles $\mathcal C_1,\dots,\mathcal C_m$, each with $v\ge3$ nodes, has cycles $\mathcal C_j=[j,1]\to[j,2]\to\dots\to[j,v]\to[j,1]$. For $j\le m-1$ the node $[j,1]$ coincides with the node $[j+1,k_j]$ of the next cycle, for some $k_j\in\{2,\dots,v\}$. No other nodes coincide, so the chain has $vm-(m-1)$ nodes.

Formalization targets

Goal: Theorem 15 (p.20)

For every open chain of $m\ge2$ cycles with $v\ge3$ nodes each, every choice of the attachment positions $k_j$, every colour set $M$ and every colour assignment $C$ with non-empty colour sets, the unweighted coordination game without bonuses on the chain satisfies

$$\text{ensures improvement paths of length}\le 3vm^3 .$$

Milestones

1. Theorem 3 (p.11): a weighted simple cycle with at most one bonus node ensures improvement paths of length $\le 2n-1$.
2. Theorem 7 (p.13): a weighted simple cycle with two bonus nodes ensures improvement paths of length $\le 3n$.
3. Cycle reduction (p.16). Given $s$, the cycle $\mathcal C_j$ behaves like a simple cycle whose link nodes carry a unit bonus $\beta^s_j$ for the colour of their predecessor in the adjacent cycle. Improvement paths of that cycle game lift to the chain.
4. Lemma 10 (p.16): on an open chain, and on a simple cycle with unit bonuses, a node with payoff $\ge1$ plays a best response.
5. Lemma 11 (p.17): once a cycle below the cycle being repaired by Algorithm 1 has grade $\mathrm U{+}$, it keeps that grade and the algorithm never returns to it.
6. Claim 1 (p.37): a sufficient condition for the progress measure $\mu$ to increase.
7. Range of $\mu$ (p.20): $\mathrm{guard}(s)+1\le\mathrm{NBR}(s)\le|\mathrm{prefix}(s)|\le m$ when $s$ is not a Nash equilibrium.
8. Counting (p.20): $\mu$ takes at most $1+m(m+1)(m+5)/6\le m^3$ values.

Significance

The result shows that on open chains of directed cycles, which lack the finite improvement property, short improvement paths always exist. Their length is polynomial in both the ring size and the number of rings. In particular a Nash equilibrium always exists and can be reached by local, one-node-at-a-time improvements, which is the kind of guarantee a distributed protocol needs. The same construction underlies the paper's polynomial-time algorithm for finding a Nash equilibrium on open chains and its bound for coalitional improvement paths (Theorem 23).

Formalizing it adds to the platform coordination games on directed graphs, improvement paths with a length bound, and the open-chain graph class. None of these are on the platform today. The results are proved in the paper. None of them has a machine-checked proof.

Status of the printed proof. A check of Lemmas 12 and 14 (pp.17–20, Appendix pp.35–39) found that both fail for some attachment positions. Lemma 12 claims that one round of Algorithm 1 on $\mathcal C_j$ changes only the grades of $\mathcal C_{j-1},\mathcal C_j,\mathcal C_{j+1}$, and Lemma 14 claims that $\mu$ increases in every round. When $k_{j-2}=2$, the node $[j-1,2]$ is the link node $[j-2,1]$, so recolouring $[j-1,1]$ can change the grade of $\mathcal C_{j-2}$. A concrete chain with $m=3$, $v=4$, $k_1=2$, $k_2=3$ has a round of Algorithm 1 in which $\mu$ drops from $(0,1,0,-3)$ to $(0,0,1,-1)$. These two lemmas are therefore not milestones. Theorem 15 itself is not contradicted: exhaustive search on small chains found improvement paths well within $3vm^3$. A complete proof needs a repaired progress argument or a different one.

Difficulty

The obvious argument fails at the start. Scheduling the nodes round-robin does not terminate on a directed cycle, since a colour can chase itself around the ring forever (Example 2, p.10). Even the cycle bounds need a specific schedule and a specific choice among best responses. On an open chain, repairing one cycle recolours its link nodes and can destroy the equilibrium of the neighbouring cycles. The index of the lowest broken cycle can therefore move down by an arbitrary amount (Figure 9, p.19). Termination needs a progress measure that increases at every round despite this back-and-forth, and the attachment positions $k_j=2$ and $k_j=v$ let a single repair reach two cycles away.

Formalization scope

A joint strategy is a function $s:V\to M$ with $s_i\in C(i)$. Payoffs are real. An improvement path of length at most $X$ is a list $s_0,\dots,s_L$, $L\le X$, of joint strategies in which each step changes exactly one node's colour to a colour in its set and strictly raises that node's payoff, and whose last element is a Nash equilibrium. Length counts steps. Simple cycles live on Fin n with edges $a\to a+1\pmod n$ and $n\ge2$. An open chain is a structure with $m\ge2$, $v\ge3$, a surjective naming map $(j,i)\mapsto[j+1,i+1]$ from Fin m × Fin v onto $V$, attachment positions with $k_j\ge2$, the link identifications, and nothing else identified. Its edges are exactly the cycle edges. The game on an open chain is unweighted and has no bonuses, as in the paper. Weighted open chains are outside this paper (p.34).

Non-empty colour sets are hypotheses everywhere. Without them there is no joint strategy and every statement would be vacuous. Improvement steps require a strict gain, so constant paths do not count.

The development needs the general strategic-game notions (best response, Nash equilibrium, improvement steps and paths, schedules), coordination games, simple cycles and open chains, and, for the milestones about Algorithm 1, the link bonuses $\beta^s_j$, grades, $\mathrm{NBR}$, $\mathrm{guard}$, $\mathrm{prefix}$, the measure $\mu$ and one round of the algorithm. The strategic-game layer is reusable for any finite game. Contributions are welcome on the cycle theorems, on a repaired progress measure for open chains, or on any other proof of Theorem 15.

Selected references

• K. R. Apt, S. Simon, D. Wojtczak, Coordination Games on Weighted Directed Graphs, arXiv:1910.02693v2, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1910.02693v2
• K. R. Apt, S. Simon, D. Wojtczak, Coordination games on directed graphs, Proc. TARK 2015, EPTCS 215, pp. 67–80, 2016. https://arxiv.org/abs/1606.07517
• S. Simon, D. Wojtczak, Efficient local search in coordination games on graphs, Proc. IJCAI 2016, pp. 482–488, 2016. https://arxiv.org/abs/1604.04809
• K. R. Apt, B. de Keijzer, M. Rahn, G. Schäfer, S. Simon, Coordination games on graphs, International Journal of Game Theory 46(3):851–877, 2017. https://arxiv.org/abs/1501.07388

Motivation

Spare parts, slow-moving retail items and humanitarian relief stock share a demand pattern: most periods see no demand, and a demand arrives only now and then. Planners of such long-tail or intermittent-demand items estimate the inter-arrival distribution from a finite observed history and feed it into an inventory policy. Bi, He and Teo (MSOM 2023) observe that this estimate is biased in a precise, computable way, for the same reason as the "hot hand" selection bias of Miller and Sanjurjo (Econometrica 2018): in a finite sequence of independent trials, the expected proportion of successes that immediately follow a success is strictly smaller than the success probability.

Timeline:

• Rinott and Bar-Hillel (2015), commenting on the working-paper version of Miller and Sanjurjo, give a combinatorial argument for the expected proportion of successes following a success in a finite i.i.d. sequence (SSRN 2642450); Bi, He and Teo adapt it, with an initial arrival at time $0$.
• Miller and Sanjurjo (2018) show that this selection bias is present in the standard measure of conditional dependence for i.i.d. Bernoulli trials, so the "gambler's fallacy" belief is partly a correct reading of finite data.
• Bi, He and Teo (2023) prove the bias for a general Markov chain of demand arrivals (Proposition 1), give a closed form for the expected empirical inter-arrival proportions under i.i.d. arrivals (Theorem 2), and prove that the relative bias is monotone in the arrival probability and in the horizon (Proposition 2).

Setting

Time positions are $0,1,\dots,n$. A demand arrival occurs at position $0$ by assumption, and at each of the positions $1,\dots,n$ independently with probability $p\in(0,1)$; write $q=1-p$ and $B(t)\in\{0,1\}$ for the arrival indicator, so $B(0)=1$.

For a gap length $j\ge1$, the empirical proportion $\hat p_j(n)$ is the number of positions $t\in\{0,\dots,n-1\}$ with $B(t)=1$, $B(t+1)=\dots=B(t+j-1)=0$, $B(t+j)=1$ and $t+j\le n$, divided by the number of arrivals $B(t)=1$ at positions $t\in\{0,\dots,n-1\}$. The denominator is at least $1$ because of the arrival at $0$. The biased estimate is

$$p_j(n)=\mathbb E\big[\hat p_j(n)\big],$$

and the relative bias of the estimate of $p=p_1$ is

$$\frac{p-p_1(n)}{p}.$$

In Lean, a sample path is ω : Fin n → Bool, the arrival indicator is arrival ω t, $\hat p_j(n)$ is empiricalGap n j ω, and $p_j(n)$ is biasedEstimate n j p, the weighted sum of $\hat p_j(n)$ over the $2^n$ paths with weights $\prod_k(p\text{ or }1-p)$.

Formalization targets

Goal: Proposition 2

For every $n\ge2$, the map $p\mapsto(p-p_1(n))/p$ is strictly decreasing on $(0,1)$; and for every $p\in(0,1)$, the map $n\mapsto(p-p_1(n))/p$ is strictly decreasing on $\{n\in\mathbb N:n\ge2\}$:

$$\frac{p-p_1(n)}{p}\ \text{is strictly decreasing in } p\in(0,1)\ \text{and in } n\ge2.$$

The printed proposition says "for all $n$". At $n=1$ the estimate is unbiased ($\hat p_1(1)=B(1)$, so $p_1(1)=p$) and the relative bias is $0$ for every $p$, which is not strictly decreasing in $p$ and is smaller than its value $(1-p)/2$ at $n=2$ (so part (ii) fails at $n=1$ under any reading). The goal is therefore stated for $n\ge2$, the range in which the proof (which divides by $m=n-1$) works. "Decreasing" is read as strict, which is what the proof gives.

Milestones

1. Theorem 2 (closed form). For $n\ge1$, $j\ge1$, $p\in[0,1]$,

$$p_j(n)=\sum_{i=1}^{n-j}\binom{n-1-j}{i-1}p^iq^{n-1-i}\frac{p+i}{i+1}+\mathbf 1[j=n]\,p\,q^{n-1}.$$

The printed theorem lacks the last term; without it the formula fails at $j=n$ (for $n=2$, $j=2$, $p=1/3$: $p_2(2)=2/9$, while the printed sum is empty). 2. EC.2.2 (i), derivative. With $m=n-1\ge1$ and $f(p)=p_1(n)/p$,

$$f'(p)=p^{-1}\Big(\sum_{i=1}^m\binom{m-1}{i-1}p^{i-1}(1-p)^{m-i}\frac{mp+2}{i+1}-1\Big).$$

3. (EC.1). For $m\ge1$, $(mp+2)\sum_{i=1}^m\rho_i/(i+1)>1$ with $\rho_i=\binom{m-1}{i-1}p^{i-1}(1-p)^{m-i}$.
4. (EC.2)–(EC.3), increment. For $m\ge1$,

$$p_1(n+1)-p_1(n)=\frac{pq}{mq}\Big[\sum_{i=0}^m\binom mi p^iq^{m-i}\frac{mp+2}{i+2}-1\Big].$$

The printed chain asserts a strict "$>$" in (EC.2); the two sides are in fact equal (both are $1/81$ at $n=2$, $p=1/3$), and the milestone states the equality. 5. Last inequality of EC.2.2 (ii). $\sum_{i=0}^m\binom mi p^iq^{m-i}\frac{mp+2}{i+2}\ge1$, strictly when $m\ge1$.

Significance

Proposition 2 explains why the finite-horizon effect matters most for long-tail items: the relative under-estimation of the arrival probability is largest when $p$ is small and the observation window is short. In the paper this drives the inventory results of §4: the delay of the delay-ordering policy chosen with the biased estimates, and the staggered base stock policy. Theorem 2 makes the bias computable exactly rather than by simulation.

On the formalization side, nothing in this mission has a machine-checked proof yet. The work is to formalize the paper's argument: the path-counting identity behind Theorem 2 (summing over $2^n$ Bernoulli paths), a derivative computation, and two strict Cauchy–Schwarz type bounds for binomial weights. The definitions of the empirical proportion and the expected estimate are reusable for other results on streaks and the hot-hand selection bias.

Difficulty

The main step is Theorem 2: converting an expectation of a ratio of two random counts into a binomial sum. The obvious route, linearity of expectation, fails because the denominator (the number of arrivals) is random and correlated with the numerator. The paper conditions on the number $i$ of arrivals among periods $1,\dots,n-1$ and counts the positions where a gap of length $j$ can sit, including the gap that closes exactly at the horizon. That case split is where the printed formula loses the $j=n$ term.

The monotonicity steps are elementary but require strictness throughout: both (EC.1) and the last inequality are of the form $\mathbb E[Y]\,\mathbb E[1/Y]>1$, and they are strict only because the binomial variable is non-degenerate for $m\ge1$ and $p\in(0,1)$.

Formalization scope

• Paths are Fin n → Bool for the periods $1,\dots,n$; the arrival at position $0$ is built into arrival, so the denominator of $\hat p_j(n)$ is at least $1$ for $n\ge1$ by construction, not by hypothesis.
• The expectation is a finite weighted sum over all $2^n$ paths; it equals the expectation under the i.i.d. Bernoulli($p$) product law.
• The estimate $p_j(n)$ is defined from the paths, not by the closed form of Theorem 2; defining it by the closed form would make Theorem 2 trivial and turn the goal into a statement about a polynomial chosen by hand.
• Milestones 2–5 use $m=n-1$ as a natural number with the horizon written $m+1$, so there is no truncated subtraction in the horizon.
• Monotonicity is StrictAntiOn, on Set.Ioo 0 1 in $p$ and on {n | 2 ≤ n} in $n$.

Welcome contributions: a proof of Theorem 2 by induction on $n$ or by conditioning on the number of arrivals; general lemmas on sums over Fin n → Bool against product Bernoulli weights; and the strict inequality $\mathbb E[X+c]\,\mathbb E[1/(X+c)]>1$ for non-degenerate binomial $X$.

Selected references

• S. Bi, L. He, C.-P. Teo, Taming the Long Tail: The Gambler's Fallacy in Intermittent Demand Management, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1217
• J. B. Miller, A. Sanjurjo, Surprised by the Hot Hand Fallacy? A Truth in the Law of Small Numbers, Econometrica 86(6), 2019–2047, 2018. https://doi.org/10.3982/ECTA14943
• Y. Rinott, M. Bar-Hillel, Comments on a "Hot Hand" Paper by Miller and Sanjurjo (2015), SSRN working paper 2642450, 2015. https://ssrn.com/abstract=2642450

Motivation

Electric utilities run demand-response programs to cut peak load during supply shortages: when an event is called, a participating customer is paid a rebate for every unit by which its consumption falls below a baseline. The utility sees consumption, not demand, so the baseline is its estimate of what the customer would have consumed without the event. In practice the baseline is the customer's average historical consumption in non-event periods (the "normal-use" baseline used by PEPCO and BG&E). This creates a measurement problem. A customer whose demand happens to be low is paid for reductions it never made, and a customer whose demand is high has to cut a lot before it is paid anything.

Agrawal and Yücel (Management Science, 2022, doi:10.1287/mnsc.2021.4278) model this as a game between a utility and its customers. They ask how the utility should set the baseline and the rebate, and whether moving the baseline away from normal use helps or hurts the environment. Their headline finding is that the cost-optimal baseline can reduce the actual demand reduction and raise emissions, against the intuition that paying more effectively must buy more reduction. This mission formalizes that finding, Proposition 4 of the authors' manuscript of May 26, 2021, together with the chain of results it rests on.

Setting

Peak demand in an event (probability $\rho\in(0,1]$) is $\omega$, uniform on $[0,2\Omega]$. Without an event it is $\lambda$, uniform on $[0,2\Lambda]$ with $\Lambda<\Omega$. Off-peak demand $\varphi$ is uniform on $[0,2\Phi]$. The utility buys power at marginal cost $c^h_p$ in an event and $c^l_p<c^h_p$ otherwise, and $\Delta c=c^h_p-c^l_p$.

Given a baseline $b\ge0$ and a rebate $r\ge0$, a customer with demand $\omega$ shifts $s\le\omega$ units to the off-peak period. Its consumption is $\omega-s$, the estimated reduction is $S(s)=(b-(\omega-s))^+$, and the customer maximizes

$$C_c(s)=r\,S(s)-\frac{c_s}{2}s^2,\qquad s\le\omega .$$

A best-response selection $s^*(b,r\mid\omega)$ picks a maximizer for every $(b,r,\omega)$. The utility's expected net cost savings are

$$C(b,r)=\rho\,\mathbb E_\omega\bigl[\Delta c\,s^*-r\,S(s^*)\bigr],$$

and its total cost is $C_u=\bar C-C$ with $\bar C$ independent of $(b,r)$. The expected actual demand reduction is $X(b,r)=\rho\,\mathbb E_\omega[s^*]$. Total expected emissions are $E_u=\bar E-\Delta e\,X$, with emission intensities $e^h_g>e^l_g$ and $\Delta e=e^h_g-e^l_g$. Two regimes are compared:

• normal-use baseline: $b=\Lambda$, and the rebate $r_0$ maximizes $C(\Lambda,\cdot)$;
• optimized baseline: $(b^*,r^*)$ maximizes $C$ over $b,r\ge0$. When this maximizer is not unique, $(b^*,r^*)$ is the one with the least rebate.

The firm inflates the baseline if $b^*>\Lambda$ and deflates it if $b^*<\Lambda$.

Formalization targets

Goal: Proposition 4 (p.19)

For $0<\Lambda<\Omega$ and $c_s>0$ there are thresholds $c_D<c_I$, depending only on $(\Omega,\Lambda,c_s)$, such that

$$b^*>\Lambda:\quad X(b^*,r^*)\le X(\Lambda,r_0)\iff\Delta c\ge c_I,\qquad b^*<\Lambda:\quad X(b^*,r^*)\ge X(\Lambda,r_0)\iff\Delta c\le c_D,$$

and the same with total emissions $E_u$ in place of $X$, with the inequalities reversed. The goal pins the thresholds down: $c_D=\kappa\Lambda c_s$ with $\kappa\approx0.7941$ the root of $9\kappa^3+15\kappa^2-175\kappa+125$ in $(1/2,1)$, and $c_I=\tfrac12(4+\sqrt2)\Omega c_s$ when $\Lambda\le\frac{4+\sqrt2}{6}\Omega$, or the root of an explicit equation in $[\tfrac52\Omega c_s,3\Lambda c_s]$ otherwise.

Milestones, in proof order

1. Proposition 1: the customer's response has three regimes (no, partial, full shift).
2. Lemma 1: the reduction is overestimated iff $\omega<b$.
3. Closed form of $X(b,r)$ (p.OA1).
4. Lemma 2: monotonicity of $X$, of the overestimation $X_o$ and of the underestimation $X_u$.
5. $C_u=\bar C-C$ and $C=(\Delta c-r)X-rX_o+rX_u$.
6. Closed form of $r_0$, which is unique (p.OA2).
7. Lemma 3: at $b=\Lambda$ the program is offered iff $\Delta c>\Lambda c_s/2$, and $r_0$ increases in $\Delta c$.
8. Closed form of $(b^*,r^*)$ and of the whole maximizer set (pp.OA2–OA3).
9. Lemma 4: with both instruments the program is always offered, and $r^*$ increases in $\Delta c$.
10. Proposition 2: $b^*$ increases in $\Delta c$ up to $\tfrac52\Omega c_s$ and decreases after.
11. Proposition 3: inflate and lower the rebate iff $\Delta c>\tfrac53\Lambda c_s$.
12. Cases 1–4 of the proof of Proposition 4: $X(b^*,r^*)$ against $X(\Lambda,r_0)$.
13. $E_u=\bar E-\Delta e\,X$.

Significance

The result separates two things a regulator might expect to move together. Optimizing the baseline always raises the utility's savings. Proposition 4 says exactly when it also lowers the actual reduction of peak demand, and with it the environmental benefit that motivates these programs. For a large cost gap the inflated baseline comes with a lower rebate, and the lower rebate dominates. For a small cost gap the deflated baseline comes with a higher rebate, and the reduction rises. The thresholds are explicit functions of the model's primitives, so the regions can be located for any calibration, such as the Maryland one of the paper's Figure 3.

The paper proves the result by hand through a case analysis over the $(b,r)$ quadrant. Machine-checking it fixes several printed details that the formal statements had to correct. The emissions clause compares the emissions reduction $E$ where total emissions $E_u$ are meant. The proof's $c_I$ switches form at $\Lambda\approx0.9553\,\Omega$ instead of $\Lambda=\frac{4+\sqrt2}{6}\Omega\approx0.9024\,\Omega$. One display of Case 3 has the wrong sign. Three clauses of Proposition 1 fail at boundary cases. Each correction is recorded on its item with a counterexample. None of these results has a machine-checked proof yet.

Difficulty

The customer's objective is the maximum of two parabolas. It is not concave, so the best response jumps with $\omega$, and ties occur at isolated demand levels. The firm's objective $C(b,r)$ therefore has different closed forms on several regions of the quadrant, separated by curves such as $b=r/(2c_s)$, $b=2\Omega-r/(2c_s)$ and $rb=2\Omega^2c_s$. The maximum has to be global over all of them. The natural approach, setting the gradient to zero on the region that contains the paper's optimum, does not certify a global maximum. For $\Delta c\ge4\Omega c_s$ the savings are constant along the ridge $rb=2\Omega^2c_s$, so the maximizer is a curve rather than a point. The comparison of $X(b^*,r^*)$ with $X(\Lambda,r_0)$ then needs single-crossing arguments between a polynomial and a square-root expression, and the threshold changes form with $\Lambda/\Omega$.

Formalization scope

All quantities are real numbers. Expectations are interval integrals with the uniform densities written out, and the two-period expectations are iterated integrals. The customer's best response is an arbitrary selection s : ℝ → ℝ → ℝ → ℝ with IsBestResponse, never a closed formula. Selections differ only on null sets, so every expectation is the paper's. The firm's domain is $b\ge0$, $r\ge0$, and the customer's feasible set is $s\le\omega$. Optimality of $(b^*,r^*)$ and of $r_0$ is defined by maximizing $C$. The closed forms are milestones, not definitions. $X_o$ integrates the density only up to $2\Omega$, and $X_u$ is a set integral over $\{b\le\omega\le\omega_1\}$, so both make sense for $b>2\Omega$.

Defining $s^*$, $r_0$ or $(b^*,r^*)$ by their closed forms would make the goal a statement about formulas rather than about optimization, and placing the threshold quantifiers after $\Delta c$ would make the equivalences empty. The statements do neither.

Mathlib's interval integrals, Real.sqrt and max are the only infrastructure needed. Proofs of any milestone are welcome, as are alternative proofs of the firm's global optimum that avoid the full case analysis.

Selected references

• V. V. Agrawal, Ş. Yücel, Design of Electricity Demand-Response Programs, Management Science, 2022 (manuscript of May 26, 2021, with Online Appendix). https://doi.org/10.1287/mnsc.2021.4278
• FERC, Measurement and Verification for Demand Response, Federal Energy Regulatory Commission, 2013. https://perma.cc/C248-DJ72

Motivation

Many combinatorial optimization problems ask for a maximum-weight set that is "independent" in two different senses at once: a bipartite matching is a set of edges that uses each left node at most once and each right node at most once; a branching in a digraph is a forest that enters each node at most once. Each of these is a common independent set of two matroids. Edmonds (1970) showed that the weighted version of this problem has a clean linear description: the convex hull of the common independent sets is cut out by the rank inequalities of the two matroids. The result is one of the central examples in polyhedral combinatorics, and Chapter 8 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), proves it in §8.5 with the tools of Chapter 6 (integral polytopes and total dual integrality).

Timeline:

• 1957: Rado proves that the greedy algorithm finds a maximum-weight independent set of a matroid.
• 1970: Edmonds proves the matroid polytope theorem, the matroid intersection theorem and the matroid intersection polytope theorem, with the dual (weight-splitting) optimality conditions.
• 1974: Hoffman characterizes integral polytopes through integral optimal values.
• 1977: Edmonds and Giles introduce total dual integrality and show that a TDI system with integral right-hand side defines an integral polyhedron.

Setting

A matroid $M=(S,\mathcal I)$ is a finite set $S$ with a family $\mathcal I$ of subsets, the independent sets, such that $\emptyset\in\mathcal I$, subsets of independent sets are independent, and for every $A\subseteq S$ all maximal independent subsets of $A$ have the same size. That size is the rank $r(A)$. For $J\subseteq S$ the characteristic vector $\chi_J\in\mathbb R^S$ has $1$ on $J$ and $0$ elsewhere, and $x(A)=\sum_{e\in A}x_e$.

Given two matroids $M_1=(S,\mathcal I_1)$, $M_2=(S,\mathcal I_2)$ with rank functions $r_1,r_2$, the matroid intersection system is

$$x(A)\le r_1(A),\quad x(A)\le r_2(A)\quad\text{for all }A\subseteq S,\qquad x_e\ge0\quad\text{for all }e\in S.\qquad(8.7)$$

Its linear-programming dual for an objective $c\in\mathbb R^S$ is

$$\min\Big\{\sum_{A\subseteq S}\big(r_1(A)y^1_A+r_2(A)y^2_A\big) : \sum_{A\ni e}(y^1_A+y^2_A)\ge c_e\ (e\in S),\ y^1,y^2\ge0\Big\}.\qquad(8.8)$$

A rational system $Ax\le b$ is totally dual integral (TDI) if for every integral $w$ for which $\max\{w^Tx : Ax\le b\}=\min\{y^Tb : y^TA=w^T,\ y\ge0\}$ has optima, the minimum is attained by an integral $y$. A rational polyhedron is integral if every nonempty face contains an integral vector.

Formalization targets

Goal: Theorem 8.20 (Matroid Intersection Polytope Theorem)

$$\operatorname{conv}\{\chi_J : J\in\mathcal I_1\cap\mathcal I_2\}=\{x\in\mathbb R^S : x \text{ satisfies } (8.7)\}.$$

Milestones

• Theorem 8.4. For one matroid, the characteristic vector of any set produced by the Greedy Algorithm maximizes $c^Tx$ subject to $x(A)\le r(A)$ for all $A$, $x\ge0$ (the system (8.1)).
• Theorem 6.22. A rational polytope is integral if and only if $\max\{w^Tx : x\in P\}$ is an integer for every integral $w$.
• Theorem 6.29. If $Ax\le b$ is TDI, $b$ is integral and $\{x : Ax\le b\}$ is a polytope, then that polytope is integral.
• Proposition 8.21. If $(\bar y^1,\bar y^2)$ is optimal for (8.8), $c^1_e=\sum_{A\ni e}\bar y^1_A$ and $c^2=c-c^1$, then $\bar y^i$ is optimal for the single-matroid dual (8.2) of $(M_i,c^i)$, and conversely any pair of optimal single-matroid duals is optimal for (8.8).
• Theorem 8.23. The system (8.7) is totally dual integral.
• Theorem 8.19. For every $c\in\mathbb R^S$ some common independent set $J$ has $\chi_J$ maximizing $c^Tx$ over (8.7).
• Corollary 8.22. There are a common independent set $J$ and $c=c^1+c^2$ such that $J$ is a maximum $c^i$-weight independent set of $M_i$ for $i=1,2$.

Significance

The theorem turns the weighted matroid intersection problem $\max\{c(J): J\in\mathcal I_1\cap\mathcal I_2\}$ into a linear program with an explicit constraint system, and its dual gives a certificate of optimality: a weight splitting $c=c^1+c^2$ under which $J$ is optimal in each matroid separately. Specializations include the bipartite matching polytope (two partition matroids), the arborescence and branching polytopes (a graphic and a partition matroid), and König–Egerváry-type min-max theorems. Total dual integrality of (8.7) also yields an integral min-max formula for every integral weight vector.

All results here are classical and fully proved in the book. As far as a search of the platform shows, none of them is formalized there: no matroid polytope, matroid intersection polytope, TDI or Hoffman-type integrality statement exists on Prove2Me. Mathlib has matroids but no matroid polytopes. The mission therefore produces a first machine-checked path from LP duality to an integral polytope theorem for matroids, with Hoffman's criterion and the Edmonds–Giles implication as standalone, reusable results.

Difficulty

The inclusion of the convex hull in (8.7) is immediate: $\chi_J(A)=|J\cap A|\le r_i(A)$. The content is the reverse inclusion, i.e. that every vertex of (8.7) is integral. The obvious idea, intersecting two integral polytopes, fails: the intersection of two integral polytopes generally has fractional vertices, so the integrality of each single matroid polytope (Theorem 8.5) says nothing about (8.7) on its own. What makes the two rank systems compatible is a property of the pair, and stating and using it requires linear-programming duality, faces and vertices of polytopes, and integrality criteria (Theorems 6.22 and 6.29) that are not in Mathlib in this form.

Formalization scope

• Matroids follow the book's axioms (M0)–(M2) on a finite type S, with subsets as Finset S (structure FinMatroid), not Mathlib's Matroid. The rank r(A) is the largest size of an independent subset of A, a natural number.
• Vectors in $\mathbb R^S$ are functions S → ℝ; the dual variables of (8.2) and (8.8) are functions on Finset S.
• The Greedy Algorithm is a predicate on its output: every run, with any tie-breaking, is covered.
• Polyhedra are $\{x : Ax\le b\}$ with rational A, b and rows and columns indexed by finite types; a polytope is a polyhedron with $l\le x\le u$ on it; faces follow §6.2 (supporting hyperplanes, plus $\emptyset$ and $P$).
• TDI is stated for the system (8.7) written row by row: one row for each pair $(i,A)$ with $i\in\{1,2\}$ and $A\subseteq S$, and one row $-x_e\le0$ for each $e$. "The optima exist" means both the primal maximum and the dual minimum are attained.
• Theorem 8.20 is an equality of sets in $\mathbb R^S$, so both inclusions are required. A formalization that took the convex hull as the definition of the feasible set, or that dropped either rank system, would not be this theorem.

Useful infrastructure, reusable beyond this mission: LP duality and complementary slackness for finite systems (Prove2Me has MatousekLP.Duality.duality_theorem), vertices of polytopes and the representation of a polytope as the convex hull of its vertices, totally unimodular matrices, and the dual Greedy Algorithm. Contributions to any milestone are welcome, as is a direct proof of Theorem 8.20 by another route.

Selected references

• W. J. Cook, W. H. Cunningham, W. R. Pulleyblank, A. Schrijver, Combinatorial Optimization, Wiley-Interscience, 1998, §§6.4, 6.6, 8.1, 8.5. https://doi.org/10.1002/9781118033142
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 2003. https://doi.org/10.1007/3-540-36478-1_2
• A. J. Hoffman, A generalization of max flow–min cut, Mathematical Programming 6 (1974), 352–359. https://doi.org/10.1007/BF01580250
• J. Edmonds, R. Giles, A min-max relation for submodular functions on graphs, Annals of Discrete Mathematics 1 (1977), 185–204. https://doi.org/10.1016/S0167-5060(08)70734-9
• R. Rado, Note on independence functions, Proceedings of the London Mathematical Society (3) 7 (1957), 300–320. https://doi.org/10.1112/plms/s3-7.1.300

Motivation

Value iteration computes the optimal cost-to-go vector $J^*$ of a Markov decision problem as the fixed point of the Bellman operator $T$, by iterating $J_{n+1}=TJ_n$. In reinforcement learning $T$ is rarely available exactly. It is replaced by an approximate Bellman operator (a regression model or a neural network fitted to $TJ_n$), which is biased, and it is evaluated from simulated transitions, which are noisy. The resulting scheme, approximate value iteration (AVI), is a stochastic approximation whose errors do not vanish: the approximation error stays of the order of the fitting accuracy forever.

Ramaswamy and Bhatnagar (arXiv:1709.04673v5; Mathematics of Operations Research, 2022) ask what AVI does under these conditions: whether the iterates stay bounded, and where they end up, when the error is only asymptotically bounded by a fixed $\epsilon>0$ in a weighted max-norm and the sampling noise is a martingale difference sequence whose conditional variance may grow with the iterate. Classical stochastic-approximation results (Tsitsiklis, Machine Learning 1994; Borkar and Meyn, SIAM J. Control Optim. 2000) assume errors that vanish asymptotically, so they do not cover this regime.

Setting

Fix $d\ge1$ states, a weight vector $\nu=(\nu_1,\dots,\nu_d)$ with $\nu_i>0$, and the weighted max-norm

$$\|x\|_\nu=\max_{1\le i\le d}\frac{|x_i|}{\nu_i}.$$

Write $\|x\|$ for the Euclidean norm. AVI is the recursion (5) of the paper,

$$J_{n+1}=J_n+a(n)\big[TJ_n-J_n+\epsilon_n+M_{n+1}\big],\qquad n\ge0,$$

where $a(n)$ are step sizes, $\epsilon_n$ is the approximation error at stage $n$ and $M_{n+1}$ is sampling noise, on a probability space with a filtration $(\mathcal F_n)$. The assumptions are:

• (AV1) $\|Tx-Ty\|_\nu\le\alpha\|x-y\|_\nu$ for some $0<\alpha<1$; $J^*$ is the fixed point of $T$.
• (AV3) almost surely $\limsup_n\|\epsilon_n\|_\nu\le\epsilon$ for a fixed $\epsilon>0$.
• (AV4) $a(n)\ge0$, $\sum_na(n)=\infty$, $\sum_na(n)^2<\infty$.
• (AV5) $M_{n+1}$ is a square-integrable martingale difference with $E[\|M_{n+1}\|^2\mid\mathcal F_n]\le K(1+\|J_n\|^2)$.

(AV2), which asks that $J^*$ be the globally asymptotically stable equilibrium of $\dot J=TJ-J$, follows from (AV1). The paper's analysis passes through the perturbed Bellman operator $\tilde Tx=Tx+B^\epsilon$, with $B^\epsilon=\{y:\|y\|_\nu\le\epsilon\}$, a set-valued map, and the differential inclusion $\dot J\in\tilde TJ-J$.

Formalization targets

Goal: Theorem 2, corrected

Almost surely,

$$\sup_n\|J_n\|<\infty\qquad\text{and}\qquad\limsup_{n\to\infty}\|J_n-J^*\|_\nu\le\frac{\epsilon}{1-\alpha}.$$

The first conclusion, stability, is the paper's. The second replaces the printed convergence clause, which states that $J_n$ converges to some point of $\mathcal A=\{J:\|TJ-J\|_\nu\le\epsilon\}$. That clause is false. Take two states with swapped deterministic transitions, discount $\gamma=0.9$ (so $TJ=(\gamma J_2,\gamma J_1)$, $\nu=(1,1)$, $\alpha=\gamma$), $\epsilon=1$, $a(n)=(n+1)^{-0.51}$, $M\equiv0$, and errors that switch between $(1,1)$ and $(1,-1)$ on the clock $t_n=\sum_{m<n}a(m)$. Every assumption holds, yet $\|TJ_n-J_n\|_\infty\approx1.8>\epsilon$ infinitely often. The bound $\epsilon/(1-\alpha)$ is what the paper's proof actually reaches (convergence to the global attractor of $\dot J\in\tilde TJ-J$), and it is sharp: for $TJ=J^*+\alpha(J-J^*)$ and constant errors $e$ with $\|e\|_\nu\le\epsilon$, $J_n\to J^*+e/(1-\alpha)$.

Milestones

1. Lemma 1: $B^\epsilon$ is convex and compact.
2. Claim 2, (11): $\nu_{\min}\|z\|_\nu\le\|z\|_\infty\le\|z\|\le\sqrt d\,\nu_{\max}\|z\|_\nu$.
3. Lemma 2: $\tilde T$ is a Marchaud map.
4. Claim 1, (10): $H_\nu(\tilde Tx,\tilde Ty)$ is attained, and $\|x_0-y_0\|_\nu\le2\epsilon+H_\nu(\tilde Tx,\tilde Ty)$ for $x_0\in\tilde Tx$, $y_0\in\tilde Ty$.
5. The equilibrium set (§5, p.15): $J\in\tilde TJ$ iff $\|TJ-J\|_\nu\le\epsilon$, and $\mathcal A$ is a closed neighbourhood of $J^*$.
6. (14): the coupling bound $\|J_n-\hat J_n\|_\nu\le\|J_N-\hat J_N\|_\nu\vee\frac{2\epsilon}{1-\alpha}$ between AVI and a copy driven by the same noise, under $0\le a(n)\le1$.
7. Lemma 3: the interpolation identity $X^n_l(t)=X^n_l(0)+\int_0^tY^n_c(\tau)\,d\tau+W^n_l(t)+G^n_c(t)$.
8. Lemma 7: block sums $\big\|\sum_{i=m(n)}^{l(n)-1}a(i)M_{i+1}\big\|$ exceed $c$ only finitely often.

Significance

Stability is the precondition for any statement about the limit of a stochastic approximation, and for AVI it is not automatic: with errors that never vanish and noise variance that grows with $\|J_n\|$, a single large excursion can feed itself. The goal says that a fixed fitting accuracy $\epsilon$ cannot make AVI diverge, and that the asymptotic loss $\limsup\|J_n-J^*\|_\nu$ is at most $\epsilon/(1-\alpha)$, the same amplification factor as in the deterministic error analysis of approximate dynamic programming. It thereby gives a sample-path guarantee for value iteration with function approximation and simulation noise.

The paper's result has not been machine-checked. The mission also documents that the printed convergence clause is false and states a corrected, sharp version. The milestones build reusable substrate: weighted max-norms, Marchaud maps, Hausdorff distances of set-valued maps, and the interpolation and noise-control lemmas of the ODE method for stochastic approximation.

Difficulty

The obvious argument writes $J_n-J^*$ as a contracting part plus a weighted sum of errors and noise, and bounds the sum. It fails because the noise is controlled only relative to $\|J_n\|$: without first knowing that $J_n$ is bounded, $\sum a(n)M_{n+1}$ need not converge. Stability must therefore be established first, without any a priori bound on the noise sum. The limit bound is then a statement about the differential inclusion $\dot J\in\tilde TJ-J$ measured in the weighted max-norm. The paper's sharpening to convergence into $\mathcal A$ is exactly the step that fails: the limit sets of a stochastic approximation of a differential inclusion are internally chain transitive sets, and these need not consist of equilibria.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with states indexed from $0$. Mathlib's norm on that type is the max-norm, so the Euclidean norm is a separate definition euclNorm; wNorm ν x is $\|x\|_\nu$. Probability is Mathlib's: a probability measure μ, a Filtration ℕ, conditional expectation μ[·|ℱ n], square integrability as MemLp _ 2 μ. $T$ is any map satisfying (AV1); the Bellman operator (3) is an instance. The filtration is arbitrary, with $J_0$ and $\epsilon_n$ $\mathcal F_n$-measurable and $M_{n+1}$ $\mathcal F_{n+1}$-measurable. Each $\limsup\le b$ is stated as "for every $\delta>0$, eventually $\le b+\delta$", which avoids the junk value of a real limsup on an unbounded sequence. Hausdorff distances take values in $[0,\infty]$.

No hypothesis of the goal is vacuous: the deterministic instance $T\equiv0$, $J\equiv\epsilon_n\equiv M\equiv0$, $a(n)=1/(n+1)$ satisfies all of them (checked in a verification file). The goal assumes nothing about $\epsilon_n$ beyond the limsup bound (no uniform bound), nothing about the noise beyond (AV5) (no bounded noise), and nothing about the step sizes beyond (AV4) (no $a(n)\le1$).

Contributions welcome: proofs of the milestones; a stability proof by either route; the Lyapunov bound for the limsup clause; and general lemmas on almost-sure convergence of $\sum a(n)M_{n+1}$ under (AV5)-type conditional variance bounds, which are reusable across stochastic approximation.

Selected references

• A. Ramaswamy and S. Bhatnagar, Analyzing Approximate Value Iteration Algorithms, arXiv:1709.04673v5, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1709.04673v5
• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16, 1994. https://doi.org/10.1007/BF00993306
• V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38, 2000. https://doi.org/10.1137/S0363012997331639
• M. Benaïm, J. Hofbauer and S. Sorin, Stochastic Approximations and Differential Inclusions, SIAM J. Control Optim. 44, 2005. https://doi.org/10.1137/S0363012904439301
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.

Motivation

In a two-stage stochastic linear program, a simple recourse constraint penalizes the gap between a first-stage quantity $z$ (for example a production level $t^{\mathrm T}x$) and a random demand $\tilde\xi$ at constant unit costs: a surplus $z>\tilde\xi$ costs $\beta$ per unit and a shortage $z<\tilde\xi$ costs $\alpha$ per unit. Its expected cost has a closed form in the distribution function of $\tilde\xi$. Because of this, simple recourse is the most tractable class of recourse models, and it is used both as a model in its own right and as an approximation tool inside general recourse algorithms (Kall and Mayer 2005, Ch. 3 §2.2).

Constant marginal costs are often unrealistic. Overtime, outsourcing or emergency purchases usually become more expensive the larger the shortfall. Klein Haneveld (1986) extended the simple recourse function to the multiple simple recourse function, in which the marginal surplus and shortage costs increase at fixed breakpoints (Kall and Mayer, p.235). Van der Vlerk (2002) showed that a multiple simple recourse problem is an ordinary simple recourse problem with a modified distribution, based on a statement proved in Klein Haneveld, Stougie and van der Vlerk (1995) (Kall and Mayer, p.241). That reduction is the goal of this mission, in the form given by Kall and Mayer (Theorem 2.8, p.242).

Setting

Let $\tilde\xi$ be a real random variable with law $\mathbb P_{\tilde\xi}$, distribution function $F_{\tilde\xi}$ and finite mean $\mu$. Write $x^+=\max\{x,0\}$ and $x^-=\max\{-x,0\}$.

For real $\alpha,\beta,\gamma$ with $\alpha+\beta\ge0$, the SRT function is $\varphi(z,\xi)=\alpha[\xi-z]^++\beta[\xi-z]^--\gamma$ and the expected SRT function is $\Phi(z)=\mathbb E[\varphi(z,\tilde\xi)]$ (srt, expectedSRT). For an interval $I$ with $\mathbb P_{\tilde\xi}(I)>0$, $\mu_{|I}$ and $\Phi_{|I}$ are the conditional mean and conditional expected SRT function given $\tilde\xi\in I$.

Multiple simple recourse. Constants $\alpha_k,\beta_k,u_k,l_k$, $k=0,\dots,K-1$, are admissible (IsMSRTData) if $\alpha_0+\beta_0\ge0$, $\alpha_k,\beta_k\ge0$ for $k\ge1$, $W:=\sum_k(\alpha_k+\beta_k)>0$, $u_0=0<u_1<\dots<u_{K-1}$ and $l_0=0<l_1<\dots<l_{K-1}$. The MSRT function and its expectation are

$$\psi(z,\xi)=\sum_{k=0}^{K-1}\bigl\{\alpha_k[\xi-z-u_k]^++\beta_k[\xi-z+l_k]^-\bigr\}-\gamma,\qquad \Psi(z)=\mathbb E[\psi(z,\tilde\xi)]$$

(msrt, expectedMSRT). The mixture distribution function and the constant are

$$G(\xi)=\frac{\sum_k\alpha_kF_{\tilde\xi}(\xi+u_k)+\sum_k\beta_kF_{\tilde\xi}(\xi-l_k)}{W},\qquad C=\frac{\bigl(\sum_k\alpha_k\bigr)\sum_k\beta_kl_k+\bigl(\sum_k\beta_k\bigr)\sum_k\alpha_ku_k}{W}$$

(mixtureCdf, mixtureConst). The optimization problem is (2.59): $\min\{c^{\mathrm T}x+\Psi(z)\mid Ax=b,\ t^{\mathrm T}x-z=0,\ x\ge0\}$ (IsOptimal259).

Formalization targets

Goal: Theorem 2.8

$G$ is the distribution function of a probability measure, and for every $z\in\mathbb R$

$$\sum_{k=0}^{K-1}\alpha_k\!\int(\xi-z)^+dF_{\tilde\xi}(\xi+u_k)+\sum_{k=0}^{K-1}\beta_k\!\int(\xi-z)^-dF_{\tilde\xi}(\xi-l_k)=\Bigl(\sum_k\alpha_k\Bigr)\!\int(\xi-z)^+dG+\Bigl(\sum_k\beta_k\Bigr)\!\int(\xi-z)^-dG-C .$$

Consequently $\Psi$ equals the right-hand side minus $\gamma$, and (2.59) with $\Psi$ has the same optimal solutions as (2.59) with the expected SRT function of $G$.

Milestones

1. Lemma 2.10 (convexity of $\varphi$ in each argument and of $\Phi$). Lemma 2.11 ($\Phi$ has the branches of $\varphi(\cdot,\mu)$ as asymptotes, and equals them outside the support).
2. Lemmas 2.12–2.13 (conditional Jensen bound; exactness outside the conditioning interval).
3. (2.53)–(2.54) (Jensen and Edmundson–Madansky bounds on a bounded support). Lemmas 2.14–2.16 (a two-interval partition refines the Jensen bound, is exact at the partition points, and has error at most $\tfrac12p_\kappa(\alpha+\beta)(a_\kappa-a_{\kappa-1})/2$).
4. (2.57)–(2.58) ($\Psi+\gamma$ as a combination of SRT integrals against shifted laws; $G$ is a distribution function).
5. (2.64)–(2.65) (for finite discrete $\tilde\xi$ with $N$ realizations, $G$ is the explicit discrete law (2.65) with at most $N(2K-1)$ atoms).

Significance

Theorem 2.8 means that every algorithm, bound and closed-form formula for simple recourse applies to multiple simple recourse unchanged, after the distribution of $\tilde\xi$ is replaced by the mixture $G$. In particular, (2.64)–(2.65) show that a finite discrete $\tilde\xi$ yields a finite discrete $G$, so the multiple simple recourse problem becomes a linear program of the special simple-recourse form (2.52). Lemmas 2.10–2.16 are the approximation theory of the expected SRT function: convexity, exactness outside the support, and the partition bounds with a distribution-free error estimate. Via Theorem 2.8 they transfer to the multiple case.

All results are proved in the book, and Theorem 2.8 also in van der Vlerk (2002). No machine-checked version of any of them is known. On the platform, only finite-scenario simple recourse formulas from other sources exist (for example NumStochOpt.Bounds.eq_2_51_simple_recourse_expected_cost, MulticutLShaped.SimpleRecourse). This mission formalizes the general-distribution statements.

Difficulty

The identity of Theorem 2.8 is elementary once the right objects are in place, and the obstacle is measure-theoretic bookkeeping. $G$ is defined as a function. To integrate against $dG$ one needs the probability measure with distribution function $G$, and must show that it is the mixture $W^{-1}\bigl[(\alpha_0+\beta_0)\mathbb P_{\tilde\xi}+\sum_{k\ge1}\alpha_k\,\mathrm{law}(\tilde\xi-u_k)+\sum_{k\ge1}\beta_k\,\mathrm{law}(\tilde\xi+l_k)\bigr]$. The obvious formula $\sum_k(\alpha_k/W)\,\mathrm{law}(\tilde\xi-u_k)+\sum_k(\beta_k/W)\,\mathrm{law}(\tilde\xi+l_k)$ is not a measure, because $\alpha_0$ or $\beta_0$ may be negative. Only the combined $k=0$ term is nonnegative, which needs $u_0=l_0=0$.

For the partition lemmas, the conditional laws on $I_1=[a_0,a_1]$ (closed) and $I_2=(a_1,a_2]$ (half-open) must be handled separately at the boundary points. The error bound of Lemma 2.15 is uniform over all conditional distributions on the interval, so it cannot be read off any single distribution.

Formalization scope

The random variable is represented by its law $P$, a probability measure on $\mathbb R$, and $F_{\tilde\xi}$ is Mathlib's cdf P. "Finite mean" is Integrable (fun ξ => ξ) P. $\int\dots dF_{\tilde\xi}(\xi+u_k)$ is the integral against P.map (· - u k), whose distribution function is $F_{\tilde\xi}(\cdot+u_k)$ (stated in eq_2_57_2_58). $\int\dots dG$ is the integral against any probability measure $\nu$ with cdf ν = G; the goal asserts that such a $\nu$ exists. Conditional quantities use P[|I]. Supports use Measure.support. Index base is $0$, as in the book. The sums printed as $\sum_{k=k}^{K-1}$ in (2.61) are read as $\sum_{k=0}^{K-1}$.

$G$ is defined by formula (2.62), not as "a distribution making (2.61) hold". Defining it that way would make the goal trivial.

Needed infrastructure: distribution functions of pushforwards under translations, finite mixtures of probability measures and their distribution functions, uniqueness of a measure given its distribution function (MeasureTheory.Measure.ext_of_Iic), and integrals of $(\xi-z)^\pm$ under conditional laws. The mixture and translation lemmas are reusable for any recourse model with shifted distributions. Contributions of proofs of any milestone, and of general lemmas on mixtures of laws on $\mathbb R$, are welcome.

Selected references

• P. Kall, J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, Kluwer Academic Publishers / Springer, International Series in Operations Research & Management Science, 2005, ISBN 0-387-23385-7; Chapter 3, §2.2, pp.226–243.
• M. H. van der Vlerk, On multiple simple recourse models, Research report, Dept. Econometrics & OR, University of Groningen, Stochastic Programming E-Print Series, 2002 (Kall–Mayer [298]). http://www.speps.info
• W. K. Klein Haneveld, L. Stougie, M. H. van der Vlerk, On the convex hull of the simple integer recourse objective function, Annals of Operations Research 56 (1995) 209–224 (Kall–Mayer [168]).
• W. K. Klein Haneveld, Duality in Stochastic Linear and Dynamic Programming, Springer-Verlag, 1986 (Kall–Mayer [167]).
• P. Kall, D. Stoyan, Solving stochastic programming problems with recourse including error bounds, Math. Operationsforsch. Statist., Ser. Optimization 13 (1982) 431–447 (Kall–Mayer [151]; source of Lemma 2.13).