All missions

Why calendar-aware, dependent demand

Revenue management systems forecast demand over canonical intervals of time, such as a week, often with a general distribution for each week, and the demand of one week is a signal for the next. The prevalent demand model, a discrete-time approximation to a Poisson process, cannot reproduce this. With one arrival per period, arrival probabilities $\lambda_t$ and $n$ periods, the coefficient of variation of the demand is at most $1/\sqrt{\sum_t\lambda_t}$, so large variability and large volume cannot coexist, and demands over disjoint intervals are independent (Li, Rusmevichientong & Topaloglu 2024, pp. 1–2).

A dynamic program handles such demand exactly but has a high-dimensional state. The question addressed by this source is which fluid approximation is the right one in this model: one that bounds the optimal revenue from above and gives a policy that is asymptotically optimal. Bai et al. (2023) treat a random number of arrivals within one stage; Jiang (2023, technical report, Hong Kong University of Science and Technology) gives a constant-factor guarantee for Markovian-correlated arrivals. This source reports the first asymptotically optimal policy under dependent demands with arbitrary distributions.

Setting

There are finite sets of resources $\mathcal L$ with integer capacities $c_i$, and products $\mathcal J$ with revenues $f_j$ and incidences $a_{ij}\in\{0,1\}$. The horizon has $K$ stages. The number of arrivals $D^k\in\{1,\dots,T\}$ in stage $k$ follows a Markov chain over the stages with arbitrary transition laws, starting from a fixed value $\hat D^0$. A customer at period $t$ of stage $k$ requests product $j$ with probability $\lambda^k_{jt}$, $\sum_j\lambda^k_{jt}=1$. The survival rate is $\theta^k_t(q)=P\{D^k\ge t+1\mid D^k\ge t,D^{k-1}=q\}$. A transition assumption asks that $P\{D^{k+1}=p\mid D^k=q\}\ge\epsilon>0$.

The optimal revenue is $\mathrm{OPT}=J^1_1(c,\hat D^0)$, where $J^k_t(y,q)$ is the value function of the dynamic program on remaining capacities $y$ and previous demand $q$. The fluid approximation uses variables $x^k_{jt}(q)$, the probability of accepting $j$ at period $t$ of stage $k$ given previous demand $q$:

$$\overline Z_{LP}=\max_{x\ge0}\ \sum_{k,t,q,j}f_jP\{D^k\ge t,D^{k-1}=q\}x^k_{jt}(q)$$

subject to $x^k_{jt}(q)\le\lambda^k_{jt}$ and, for all $i,t,q,k$,

$$\sum_{\ell<k}\sum_{s,p,j}a_{ij}P\{D^\ell\ge s,D^{\ell-1}=p\mid D^k\ge t,D^{k-1}=q\}x^\ell_{js}(p)+\sum_{s\le t}\sum_ja_{ij}x^k_{js}(q)\le c_i.$$

The constraints bound the expected consumption up to a period, conditional on reaching that period. The approximate policy solves this program once, and, on a request for $j$ with previous demand $q$, is willing to accept with probability $\gamma x^k_{jt}(q)/\lambda^k_{jt}$; it accepts if it is willing and capacity remains. Its expected revenue is $\mathrm{APX}$. Let $c_{\min}=\min_ic_i$ and $L=\max_j\sum_ia_{ij}$.

Formalization targets

Goal: the performance guarantee (Theorem 4.1)

For a suitable $\gamma$,

$$\frac{\mathrm{APX}}{\mathrm{OPT}}\ge\frac{\mathrm{APX}}{\overline Z_{LP}}\ge\max\Big\{\frac1{4L},\ 1-4\frac{\sqrt{(c_{\min}+\frac1{\epsilon^6}(K-1))\log c_{\min}}}{c_{\min}}-\frac L{c_{\min}}\Big\}.$$

Milestones

In proof order, the milestones are:

1. the upper bound $\overline Z_{LP}\ge\mathrm{OPT}$ (Theorem 3.1), through the relaxed dynamic program (9) and Lemmas B.1–B.3;
2. the revenue decomposition (3) and the availability bound (4);
3. the first term $\mathrm{APX}\ge\gamma(1-L\gamma)\overline Z_{LP}$ (§I);
4. the mixing lemmas J.1–J.3 and the Bernoulli bound J.4;
5. the moment generating function estimates, Lemmas 5.1–5.3:

$$P\Big\{U^{k-1}_i+\sum_{s\le t}N^k_{is}(q)\ge c_i\mid D^{k-1}=q\Big\}\le e^{(c_i+\frac3{\epsilon^6}(k-1))\lambda^2-(1-\gamma)c_i\lambda}.$$

What the result gives

The result. The first term of the guarantee is a constant-factor bound when $L$ is bounded, as in airline networks where itineraries rarely use more than two legs. The second term tends to one when $K$ and $c_{\min}$ grow at the same rate $\theta$, with gap of order $1/\sqrt\theta$, so the policy is asymptotically optimal and the fluid bound asymptotically tight in that regime. The source states that existing fluid approximations also provide upper bounds in this model but not asymptotically optimal policies (p. 5).

Formalizing it. The theorem is proved in the source and is not formalized on the platform. What is open here is the machine-checked proof: a verified fluid bound for a non-stationary Markov demand model, verified concentration along a dependent demand path, and an explicit treatment of the conditional constraints at unreachable states, which the source leaves undefined.

Why it is hard

The obvious argument treats the consumption of a resource as a sum of independent Bernoulli variables and applies a Chernoff bound. This fails because the demand path decides which of these variables count at all, and demands in different stages are dependent. Conditioning on the path restores independence, but then the conditional mean of the consumption is itself random and is not bounded by the capacity, because the fluid constraint only bounds an expectation given the previous stage. The remaining fluctuation has to be controlled along a dependent, non-stationary chain, where the dependence between stages decays only at rate $1-\epsilon$. That is the source of the factor $1/\epsilon^6$.

Formalization scope

Stages, periods and demands are 0-based Fin K, Fin T in Lean. The transition law is primitive, and the survival rate is derived from it. The transition assumption Minorized is literal: it bounds transitions between stages of the horizon and says nothing about $D^1$ given $\hat D^0$, so the goal covers the stronger reading too. There is no sign on $f_j$. Probabilities of demand events are finite sums over paths; a conditional probability on a null event reads $0$, and only concerns states the policy never reaches. A run of the policy (PolicyRun) is any probability space with the demand path, requests and willingness indicators with the stated laws and independence; the capacity path moves only at reached periods. The optimum $\overline Z_{LP}$ is objective x at an optimal x, never a supremum; ratios are stated as products, plus quotients when $\mathrm{OPT}>0$. The goal asserts one $\gamma$ for all optimal x and all runs.

The assumption $T\epsilon\le1$ is added to Lemma 5.1 alone, since at $K=1$ the printed lemma has a counterexample recorded in its statement. The goal cannot hold vacuously: existence of an optimum is one of its clauses, the bound is also asserted as a product where the ratios would read $0$, and PolicyRun is proved inhabited for every feasible $x$ and every instance in the verification file.

The development needs the path law of a non-stationary chain, conditional expectations on finite demand paths, Hoeffding's lemma and a bounded-difference argument. The model and the mixing lemmas are reusable for other staged-demand models. Contributions proving the milestones in any order are welcome; Section D of the source gives a route to Theorem 3.1 that avoids LP duality.

Selected references

• W. Li, P. Rusmevichientong, H. Topaloglu, Technical Note – Revenue Management with Calendar-Aware and Dependent Demands: Asymptotically Tight Fluid Approximations, arXiv:2409.02637v2, 2024; Operations Research, 2025. https://arxiv.org/abs/2409.02637
• Y. Bai, O. El Housni, B. Jin, P. Rusmevichientong, H. Topaloglu, D. P. Williamson, Fluid Approximations for Revenue Management under High-Variance Demand, Management Science 69(7), 2023. https://doi.org/10.1287/mnsc.2023.4769
• D. Adelman, A. J. Mersereau, Relaxations of Weakly Coupled Stochastic Dynamic Programs, Operations Research 56(3), 2008. https://doi.org/10.1287/opre.1070.0445
• D. P. Dubhashi, A. Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511581274
• D. A. Levin, Y. Peres, Markov Chains and Mixing Times, American Mathematical Society, 2017. https://doi.org/10.1090/mbk/107

Why overlapping routes

A distributor that serves the same customers every day with a fleet of capacitated vehicles faces a vehicle routing problem with stochastic demand: the customers are fixed, but their daily demands are random. Re-solving the vehicle routing problem every morning (reoptimization) gives the cheapest routes, but it is expensive to compute and changes every driver's route every day. The classical alternative is dedicated routing: each vehicle is assigned a fixed set of customers in advance and only adapts by returning to the depot when it runs out (Bertsimas 1992). Dedicated routes waste capacity: a vehicle whose customers ask for little returns half empty while its neighbour makes an extra trip.

Ledvina, Qin, Simchi-Levi and Wei (SSRN 3656374, 2022; published in Operations Research, doi:10.1287/opre.2022.2304) borrow from process flexibility, where a "long chain" of plants that each can make two adjacent products recovers most of the benefit of full flexibility (Jordan & Graves 1995). Their adjacent overlapping (AO) strategy lets each vehicle's route overlap the next vehicle's route, and they compute the exact asymptotic cost of the resulting strategy relative to reoptimization. This mission formalizes that computation, Theorem 1 of the paper.

Setting

A depot sits at $x_0\in\mathbb R^2$. There are $M$ vehicles of integer capacity $Q\ge1$ and $N=N'M$ customers at locations $x_1,\dots,x_N$, with $c_i=\|x_0-x_i\|_2$. Each customer's daily demand is an independent copy of an integer random variable $D$ with values in $\{0,\dots,u\}$, mean $\mu$ and probability mass function $p$; all demands are known before the vehicles leave. Demand is splittable: a customer may be served by several visits. A trip leaves the depot, serves customers and returns, delivering at most $Q$ units; the number of trips is not limited.

Reoptimization. For one day's demand vector $d$, $\mathrm{VRP}^*(d)$ is the least total length of a list of trips that delivers exactly $d_i$ to every customer. Its expectation over the demands is $Z^*$. $L^*$ is the length of the shortest closed tour through all customers.

Adjacent overlapping. The customers are labelled $1,\dots,N$ along a closed tour of length at most $\alpha L^*$ (an α-optimal labelling). Vehicle $j$ owns the primary route $\mathcal N_j=[(j-1)N'+1,\dots,jN']$ and the extended route $\mathcal E_j=\mathcal N_j\cup\mathcal N_{j+1}$ ($\mathcal E_M=\mathcal N_M$). Each day, Algorithm 1 runs the vehicles in order: vehicle $j$ first serves whatever vehicle $j-1$ left of $\mathcal N_j$, refilling at the depot whenever it runs dry, and then spends the remaining capacity of its last trip on the start of $\mathcal N_{j+1}$. With $\bar d_j=\sum_{i\in\mathcal N_j}d_i$ this is the recursion

$$e_0=0,\qquad w_j=(\bar d_j-e_{j-1})^+,\qquad r_j=\lceil w_j/Q\rceil,\qquad e_j=Qr_j-w_j ,$$

where $r_j$ is the number of trips of vehicle $j$. $Z^{AO(\alpha)}$ is the expected total length of the routes Algorithm 1 drives, $R_j$ the random trip count, and $r_{avg}=\frac1M\sum_{j=1}^M\mathbb E[R_j]$.

Formalization targets

Goal: Theorem 1

Let the customer locations be i.i.d. random points with compact support $\mathcal A$. Then $r^\infty_{avg}=\lim_{M\to\infty}r_{avg}$ exists and, almost surely, for every sequence of α-optimal labellings,

$$\lim_{M\to\infty}\frac{Z^{AO(\alpha)}}{Z^*}=\frac{Q\,r^\infty_{avg}}{N'\mu}.$$

The goal asserts the shape of the limit; it fixes no numerical constant.

Milestones

The milestones follow the proof. Display (3) ties Algorithm 1's routes to the trip count $r_j$. Lemmas 1 and 2 bound $Z^*$:

$$\frac{2\mu}{Q}\sum_i c_i\ \le\ Z^*\ \le\ \frac{2\mu}{Q}\sum_i c_i+\Big(1-\frac1Q\Big)(L^*+2c_{\max}).$$

Lemma 3 bounds $Z^{AO(\alpha)}$ by $2\sum_j\mathbb E[R_j](\frac MN\sum_{i\in\mathcal N_j}c_i+L_j)+3\alpha L^*$. Lemma 7 writes $\mathbb E[R_j]=s^0P^{j-1}\pi$ for a fixed $(Q+1)\times(Q+1)$ stochastic matrix $P$. Lemma 4 and Corollary 1 control the deviations $\mathbb E[R_j]-r_{avg}$. Proposition 1 and Lemma 5 then give

$$\Big|Z^{AO(\alpha)}-\frac{2Mr_{avg}}{N}\sum_i c_i\Big|\ \le\ 2\Gamma_3c_{\max}+\alpha(2r_{avg}+2\Gamma_3+3)L^* .$$

Lemma 6 gives $\mathbb E[R_j]\le\mathbb E[R_1]$, and the last milestone states that the error terms divided by $\frac{2\mu}{Q}\sum_ic_i$ vanish almost surely.

Three printed statements are corrected. Lemma 7's exponent is $j-1$, not $j$. Lemma 4 ($|\mathbb E[R_j]-r_{avg}|\le\Gamma_1\gamma^j+\Gamma_2/M$) and Corollary 1 ($\sum_j|\mathbb E[R_j]-r_{avg}|\le\Gamma_3$) hold as printed when $\mathbb P[D=0]>0$, which the literal support $\{0\}\cup[u]$ gives. They fail for laws with $\mathbb P[D=0]=0$ whose excess chain is periodic: for $N'=1$, $Q=3$, $D\equiv2$ the trip counts are $1,1,0,1,1,0,\dots$. For every law they are complemented by bounded cumulative deviations, $|\sum_{k\le j}\mathbb E[R_k]-jr^\infty|\le\Gamma$ and $|\sum_{k\le j}(\mathbb E[R_k]-r_{avg})|\le\Gamma_3$. Proposition 1 and Lemma 5 hold with every constant of the printed Corollary 1, and for every law with some constant $\Gamma_0$ independent of $M$, $N$ and the locations.

Significance

The theorem reduces the comparison between two routing policies, each involving geometry and randomness, to a single number: the long-run average number of trips per vehicle, which depends on $D$, $Q$ and $N'$ only and is computable from the matrix $P$ of Lemma 7. The geometry cancels. This is what makes the AO strategy analysable at all, and the paper's numerical tables (ratios within 2% of 1 for $N'\ge5$ and $Q\le N'\mu$) are evaluations of this formula. It also shows why AO beats dedicated routing: the overlap lowers the average number of trips, and nothing else matters asymptotically.

The result is proved in the paper. It has no machine-checked proof. A formalization adds a precise definition of Algorithm 1 and of the route it drives, the split-delivery reoptimization benchmark, the corrected forms of Lemmas 4 and 7 and Corollary 1 (whose printed forms fail, Lemma 7 always and the other two for some laws), and an almost sure asymptotic statement uniform over labellings.

Difficulty

There are three hard steps. First, the geometry of Algorithm 1: the bounds of Lemma 3 and Lemma 5 require tracking where each trip starts and ends (every departure goes to the primary route, at most one return comes from the overlap segment) and that no stretch of the tour is driven twice. Second, the trip counts form a finite Markov chain that may be periodic. The paper's exponential-convergence argument assumes aperiodicity "without loss of generality", which is not true; the corrected statements need bounded Cesàro deviations for an arbitrary finite stochastic matrix, and Proposition 1 and Lemma 5 then need summation by parts instead of a sum of absolute deviations. Third, the tour length $L^*$ must be negligible against $\sum_ic_i$: this needs $L^*=o(N)$ for points in a bounded planar set and the strong law of large numbers for $\sum_i\|x_0-X_i\|$. The paper cites Beardwood–Halton–Hammersley, which is much stronger than needed.

Formalization scope

Points are EuclideanSpace ℝ (Fin 2). The demand law is any probability mass function on $\{0,\dots,u\}$ with $\mu>0$, and every expectation over demands is a finite sum over demand vectors. $Z^*$ is the expectation of the infimum of the total trip length over split-delivery solutions with real delivered amounts. $Z^{AO(\alpha)}$ is the expected length of the routes Algorithm 1 actually drives: units delivered in label order, chunked into trips of $Q$ (refill exactly at a stock-out), zero-demand customers skipped. The labelling is a permutation; labels are 0-based and vehicles 1-based. The $M$-th instance uses the first $N'M$ points of one i.i.d. sequence, "compact support" means the points lie almost surely in a compact set, and $\mathbb P(X_0\ne x_0)>0$ excludes the $0/0$ case. The limit is almost sure, and the labellings may be chosen after the locations.

A trivializing encoding would define the AO cost as $2r_j$ times a radial term. That turns Lemmas 3 and 5 into definitions. Display (3) is a milestone so that the trip count is proved about the driven route, not assumed.

A complete development needs Euclidean tour bounds ($L^*=O(\sqrt N)$ in a bounded set, or any $o(N)$ bound), the iterated tour partitioning bound for split demand, the radial bound, finite Markov chain Cesàro estimates, and the strong law of large numbers (in Mathlib). The tour bounds and the Cesàro estimates are reusable beyond this mission. Proofs of individual milestones are welcome in any order.

Selected references

• K. Ledvina, H. Qin, D. Simchi-Levi, Y. Wei, A New Approach for Vehicle Routing with Stochastic Demand: Combining Route Assignment with Process Flexibility, SSRN 3656374, 2022. https://ssrn.com/abstract=3656374 (Operations Research, 2022, https://doi.org/10.1287/opre.2022.2304)
• J. Beardwood, J. H. Halton, J. M. Hammersley, The shortest path through many points, Proc. Cambridge Philos. Soc. 55, 1959. https://doi.org/10.1017/S0305004100034095
• M. Haimovich, A. H. G. Rinnooy Kan, Bounds and heuristics for capacitated routing problems, Mathematics of Operations Research 10(4), 1985. https://doi.org/10.1287/moor.10.4.527
• W. C. Jordan, S. C. Graves, Principles on the benefits of manufacturing process flexibility, Management Science 41(4), 1995. https://doi.org/10.1287/mnsc.41.4.577
• D. J. Bertsimas, A vehicle routing problem with stochastic demand, Operations Research 40(3), 1992. https://doi.org/10.1287/opre.40.3.574

Why budgeted buyers and liquid welfare

Most online advertising is sold through sequential auctions: one impression at a time, millions of times a day, and since 2019 increasingly by first-price rules (Won21). The advertisers who bid are budget-constrained, and they do not compute equilibria; their bids are set by learning algorithms that adjust a shading or pacing multiplier from round to round. Two questions follow for a platform designer: how much welfare such a system loses, and how to measure welfare at all when buyers cannot pay their full value.

The standard measure for budgeted buyers is liquid welfare (Dobzinski–Paes Leme, ICALP 2014): a buyer's value counts only up to her budget. Earlier price-of-anarchy bounds for liquid welfare assume equilibrium play (pacing equilibria, Bayes–Nash equilibria) or that every buyer runs one specific algorithm. G. Fikioris and É. Tardos (arXiv:2210.07502v4, EC'23 and Mathematics of Operations Research, 2025) replace both by a behavioural assumption that each buyer can guarantee herself: her utility is within a factor $\gamma$ and an additive regret of the best fixed shading multiplier in hindsight. Their Theorem 4.2 shows that this alone makes sequential first-price auctions efficient, with a price of anarchy of $\gamma+1/2+O(1/\gamma)$, about $2.41$ for no-regret buyers.

Timeline:

• 2014: liquid welfare introduced for budgeted buyers (Dobzinski–Paes Leme).
• 2013: composable mechanisms, with welfare compared to liquid ("effective") welfare at equilibrium (Syrgkanis–Tardos, STOC 2013).
• 2019: budget pacing with no regret against the best sequence of bids, for second-price auctions (Balseiro–Gur, Management Science 2019).
• 2022: Gaitonde et al. (arXiv:2205.08674) show that in sequential budgeted second-price auctions no-regret players can have arbitrarily bad liquid welfare; Fikioris–Tardos prove the first-price bound formalized here (arXiv 2022, EC'23).

Setting

There are $n$ players and $T$ rounds, one item per round. Player $i$ has value $v_{it}\in[0,1]$ for the item of round $t$ and a budget $B_i\ge0$. In every round each player submits a bid $b_{it}\ge0$; a highest bidder $w_t$ wins and pays her bid, so the price is $p_t=\max_j b_{jt}$. Player $i$'s value and payment are $V_i=\sum_{t:w_t=i}v_{it}$ and $P_i=\sum_{t:w_t=i}p_t$. Her budgeted quasi-linear utility is $U_i=V_i-P_i$ if $P_i\le B_i$ and $-\infty$ otherwise.

The liquid welfare of the outcome is $\mathrm{LW}=\sum_i\min\{B_i,V_i\}$, and the optimal liquid welfare $\mathrm{LW}^*$ is the largest value of $\sum_i\min\{B_i,\sum_{t\in O_i}v_{it}\}$ over allocations of the items into disjoint bundles $O_1,\dots,O_n$.

The benchmark is defined against the highest competing bid $d_{it}=\max_{j\ne i}b_{jt}$ that player $i$ actually faced. For a shading multiplier $\lambda\in[0,1]$, the budget-capped bid is

$$\hat b_{it}(\lambda)=\min\Big\{\lambda v_{it},\ B_i-\sum_{\tau<t}\hat b_{i\tau}(\lambda)\,\mathbb 1[\hat b_{i\tau}\text{ wins against }d_{i\tau}]\Big\},$$

and $\hat U_i(\lambda)=\sum_t(v_{it}-\hat b_{it}(\lambda))\,\mathbb 1[\hat b_{it}\text{ wins against }d_{it}]$, for any tie-breaking rule. Player $i$ has competitive ratio at most $\gamma\ge1$ and regret at most $\mathrm{Reg}$ if

$$U_i\ \ge\ \frac{\sup_{\lambda\in[0,1]}\hat U_i(\lambda)-\mathrm{Reg}}{\gamma}.$$

Finally $c(\lambda)=-1/\ln(1-\lambda)$, $\lambda_1=1/\sqrt{1+\gamma}$, $\lambda_2=\gamma W(-e^{-2/\gamma}/\gamma)+1$ with $W$ the principal Lambert $W$ function, and $\gamma_0\approx1.725$ is the root of $1+1/\lambda_1=\gamma/(c(\lambda_1)\lambda_1)$.

Formalization targets

Goal: Theorem 4.2

There are absolute constants $C,K\ge0$ such that, for every $n$, $T$, $\gamma\ge1$, $\mathrm{Reg}\ge-1$ and $\delta\ge0$: if every player has competitive ratio at most $\gamma$ and regret at most $\mathrm{Reg}$ except with probability $\delta$, then

$$\mathrm{LW}\ \ge\ \frac{\mathrm{LW}^*-C\,n\,(\mathrm{Reg}+1)}{\gamma+\tfrac12+K/\gamma}$$

except with probability $n\delta$. The constants are not fixed, only their existence; the exact $1/2$ is.

Milestones

1. Lemma 4.1: $\sup_\mu\hat U_i(\mu)\ge\min\{\frac{1-\lambda}{\lambda}\mathrm{LW}^*_i,\ c(\lambda)\lambda\mathrm{LW}^*_i-c(\lambda)\sum_{t\in O_i}p_t\}-1$ for $\lambda\in(0,1)$.
2. Inequality (2): the per-player value bound on the competitive-ratio event.
3. Payment bound: $0\le P_i\le\mathrm{LW}_i+\mathrm{Reg}^+/\gamma$.
4. Aggregated inequality (p.9): $\mathrm{LW}^*$ minus regret terms is at most $\max\{1+\frac1\lambda,\frac{\gamma\lambda}{1-\lambda},\frac{\gamma}{c(\lambda)\lambda}\}\,\mathrm{LW}$, for every $\lambda\in(0,1)$.
5. Appendix A, in order: $\lambda_2\in(0,1)$; $1+1/\lambda_2=\gamma/(c(\lambda_2)\lambda_2)$; the $\lambda_1$ branch and the threshold $\gamma_0$; $d\lambda_2/d\gamma<0$; inequality (12) for $\gamma\ge\gamma_0$; $1+1/\lambda_2=\gamma+1/2+O(1/\gamma)$; the regret factor is $O(1)$.

Significance

The theorem gives a welfare guarantee that needs no equilibrium, no common prior and no specific algorithm: any learning rule that is $\gamma$-competitive against fixed shading multipliers, which Fikioris–Tardos show is achievable for budgeted buyers facing adversarial competition (their Theorem 6.3), suffices. It also separates the two common auction formats: for second-price auctions no such bound exists (their Theorem 5.1), and Theorems 5.2–5.3 show the first-price bound is asymptotically tight. The result therefore supports the industry's move to first-price auctions on efficiency grounds.

The result is proved on paper, but parts of the proof are computer-algebra claims: the monotonicity of the function defining $\gamma_0$, the derivative of $\lambda_2$, and the expansion $1+1/\lambda_2=\gamma+1/2+O(1/\gamma)$ are justified in the paper by "can be proved in Mathematica". A formal proof replaces these by checked arguments about the Lambert $W$ function, which Mathlib does not yet have. No part of the result has been machine-checked before.

Difficulty

The welfare argument (milestones 1–4) is elementary but delicate. Lemma 4.1 needs a random multiplier drawn from the density $c(\lambda)/(1-\mu)$ on $[0,\lambda]$ and an argument that a player who is not budget-constrained at $\lambda$ is not constrained at any smaller multiplier, which must hold for every tie-breaking rule. The aggregation partitions players by whether their value exceeds their budget and by which branch of Lemma 4.1 is active, and it uses that the bundles of the optimal allocation are disjoint.

The analytic part is where the obvious approach stops. Choosing the single multiplier $\lambda_1$ for all $\gamma$ gives a price of anarchy of $\gamma+\Theta(\sqrt\gamma)$, not $\gamma+1/2$; the $\gamma+1/2$ comes only from switching to the Lambert-$W$ multiplier $\lambda_2$ at the exact threshold $\gamma_0$, and the printed "$\gamma\le1.73$" is not the right switch (the inequality it asserts fails between $\gamma_0=1.72511\ldots$ and $1.73$). Every remaining step is an inequality between transcendental functions on an unbounded interval.

Formalization scope

Players are Fin n and rounds Fin T. An outcome carries values in $[0,1]$, nonnegative bids and a winner that is any highest bidder; budgets are a separate nonnegative vector. $d_{it}=0$ when $n=1$. The tie rule of the benchmark is a free predicate (bids above $d_{it}$ win, below lose), and every statement holds for every such rule. $\mathrm{LW}^*$ is a maximum over maps from rounds to Option (Fin n). The benchmark is an iSup over $[0,1]$ of a family bounded in $[0,T]$.

Probabilities are failure probabilities of Mathlib's measure on arbitrary sets: no measurability and no independence across players are assumed, and values, bids, winners and the tie rule may all be random. The constants $C$ and $K$ are quantified before every other variable. The printed theorem places no sign condition on $\mathrm{Reg}$; it is false for $\mathrm{Reg}<-1$ (an explicit two-player family drives $U_i-\sup\hat U_i$ to infinity), so the goal assumes $\mathrm{Reg}\ge-1$, the exact condition the aggregation needs. The payment bound and the aggregated inequality use $\mathrm{Reg}^+=\max\{\mathrm{Reg},0\}$ in the term the text derives under $\mathrm{Reg}\ge0$.

The Lambert $W$ function is defined locally as the principal branch: for $x\ge-1/e$, the unique $y\ge-1$ with $ye^y=x$. $\gamma_0$ is defined as the exact root, never as $1.73$. A formalization that fixed $\gamma$, fixed $n$, let $C$ or $K$ depend on $\gamma$, or replaced $\gamma+1/2+K/\gamma$ by a cruder denominator would be a different and weaker theorem.

Contributions are welcome at every level. Reusable pieces are the Lambert $W$ branch with its monotonicity, derivative and range on $(-1/e,0)$; the integral identity $\int_0^\lambda c(\lambda)/(1-\mu)\,d\mu=1$; and the sequential-auction model with its budget-capped counterfactual bids.

Selected references

• G. Fikioris, É. Tardos, Liquid Welfare Guarantees for No-Regret Learning in Sequential Budgeted Auctions, arXiv:2210.07502v4, 2024; EC'23; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2210.07502v4
• S. Dobzinski, R. Paes Leme, Efficiency Guarantees in Auctions with Budgets, ICALP 2014. https://doi.org/10.1007/978-3-662-43948-7_33
• V. Syrgkanis, É. Tardos, Composable and Efficient Mechanisms, STOC 2013. https://doi.org/10.1145/2488608.2488635
• S. Balseiro, Y. Gur, Learning in Repeated Auctions with Budgets: Regret Minimization and Equilibrium, Management Science 65(9), 2019. https://doi.org/10.1287/mnsc.2018.3174
• J. Gaitonde, Y. Li, B. Light, B. Lucier, A. Slivkins, Budget Pacing in Repeated Auctions: Regret and Efficiency without Convergence, arXiv:2205.08674, 2022. https://arxiv.org/abs/2205.08674

Matching requests to resources that come back

Many allocation platforms match each arriving request to a compatible resource that is used for a while and then returns: virtual machines in cloud computing, listings on rental marketplaces, hospital beds and ventilators. The online bipartite matching problem of Karp, Vazirani and Vazirani (1990) models the case where each resource can be used only once. Its reusable variant, online bipartite matching with reusable resources (OBMRR), was introduced by Gong et al. (2021) and studied by Feng et al. and Goyal et al. for fractional allocations or large inventories. This mission concerns the integral problem with one unit of each resource, where no online algorithm was known to beat the greedy ratio $1/2$.

Timeline:

• 1990: Karp, Vazirani and Vazirani give RANKING, which is $(1-1/e)$-competitive for non-reusable unweighted matching.
• 2011: Aggarwal, Goel, Karande and Mehta extend it to vertex weights with the Perturbed Greedy algorithm, again $(1-1/e)$.
• 2013: Devanur, Jain and Kleinberg give the randomized primal-dual analysis that this mission follows.
• 2019–2021: Feng et al. and Goyal, Iyengar and Udwani obtain $(1-1/e)$ for fractional reusable allocation, or for large inventories.
• 2021/2022: Delong, Farhadi, Niazadeh, Sivan and Udwani show that Periodic Reranking is about $0.589$-competitive for integral OBMRR (arXiv:2110.07084), the first ratio above $1/2$.

Setting

An instance consists of a finite set $V$ of resources, arrivals $0,1,\dots,n-1$ in this order, an edge set $E\subseteq V\times\{0,\dots,n-1\}$, a weight $r_i\ge0$ for every resource and a usage duration $d\ge1$. When resource $i$ is matched to arrival $j$ it earns $r_i$, is unavailable at arrivals $j+1,\dots,j+d-1$, and is available again at $j+d$. A feasible reusable matching is a set of edges in which every arrival appears at most once and two edges on the same resource are at least $d$ arrivals apart. $\mathrm{OPT}$ is the largest total weight of a feasible reusable matching.

Periodic Reranking (Algorithm 1) splits the arrivals into periods of $d$ consecutive arrivals, starting with the first, and gives every resource $i$ an independent seed $y_i^k$, uniform on $[0,1]$, in every period $k$. With the trade-off function $g(x)=e^{\beta(x-1)}$, resource $v$ has reduced price $r_v\bigl(1-g(y_v^{k(t)})\bigr)$ at an arrival $t$ of period $k(t)$. Each arrival is matched to an available neighbour of largest reduced price (ties to a fixed priority order), or left unmatched if it has none. A small seed means a high priority, and a resource that returns from a match finds a fresh seed.

Formalization targets

Goal: Theorem 1

For every instance and $\beta=0.89$, the output of Periodic Reranking is a feasible reusable matching for every seed vector, the algorithm is online, and

$$\mathbb E_Y\Bigl[\sum_{(i,t)\in\mathrm{PR}(Y)} r_i\Bigr]\ \ge\ 0.5893\cdot \mathrm{OPT}.$$

The theorem prints "$\Gamma\approx0.589$"; its proof establishes $0.5893$, which is the constant stated.

Milestones

The analysis is a randomized dual fitting. With $\beta_j(Y)=r_i(1-g(y_i^{k(j)}))$ and $\alpha_{i,j}(Y)=r_i\,g(y_i^{k(j)})$ on every matched pair $(i,j)$:

• Lemma 1: reverse weak duality and $\Gamma$-approximate dual feasibility give $P\ge\Gamma\cdot\mathrm{OPT}$;
• Lemma 2: the expected duals satisfy reverse weak duality;
• Lemma 3: a conditional bound (3), averaged only over the two seeds $y^1=y_i^{k(j)-1}$, $y^2=y_i^{k(j)}$ of an edge $(i,j)$, gives dual feasibility;
• Lemmas 4–8: bounds on $\beta_j$ and $\sum_t\alpha_{i,t}$ through the critical threshold $y^c_j(y^1)$, and the three regimes of $y^1$;
• Lemma 9: $\mathbb E_{y^1,y^2}[\beta_j+\sum_t\alpha_{i,t}]\ge r_i\,f(z_1,z_2,y^c_j(1))$ for some $0\le z_1\le z_2\le1$;
• the proof of Theorem 1: at $\beta=0.89$,

$$f(z_1,z_2,x)=G(z_2)-G(z_1)+(1-g(x))(1-z_1)+(1-z_2)\bigl(G(x)-G(0)\bigr)+z_1\bigl(1-g(0)\bigr)\ >\ 0.5893$$

for all $0\le z_1\le z_2\le1$, $x\in[0,1]$, with $G=g/\beta$.

Lemma 8(b) is stated with one extra hypothesis: no resource other than $i$ has seed exactly $1$ in period $k(j)-1$. As printed it fails at a tie between zero reduced prices; the counterexample is in the statement of that milestone.

Significance

Theorem 1 separates integral online algorithms for reusable resources from deterministic ones, which cannot beat $1/2$ even without reuse. It shows that reranking on a fixed schedule, every $d$ arrivals, keeps the correlation that makes RANKING work within one usage window while decoupling decisions that are $d$ arrivals apart. For $d\ge n$ the algorithm is Perturbed Greedy, so the analysis also reproves a non-reusable special case with a weaker constant.

The result is proved on paper. To the knowledge of this mission it has not been formalized. A complete development produces a machine-checked model of reusable matching, an explicit online algorithm with its randomness, and a dual-fitting argument that is reusable for other ranking-type algorithms. Lemma 8(b) as printed is false at probability-zero seeds, so a checked proof also settles exactly which hypotheses the conditional analysis needs.

Difficulty

The obvious route is to copy the RANKING analysis per edge, fixing all seeds except the one of $i$ in the period of $j$. That fails: for some values of the previous seed $y^1$, resource $i$ is matched just before the period of $j$ and is blocked at $j$ for every $y^2$, so no bound conditioned on $y^1$ alone exceeds $0$. The analysis must average over two seeds of the same resource in consecutive periods. Lemmas 6–8 control how the run in period $k(j)-1$ changes with $y^1$. They compare runs that differ in one seed, arrival by arrival, which is where the tie-breaking and zero-price cases matter. The final bound has a margin of about $1.3\times10^{-5}$ ($\min f\approx0.58931$), so the numerical step needs bounds on $e^{x}$ to about six digits.

Formalization scope

Arrivals are Fin n, numbered from $0$. Arrival $t$ lies in period $t/d+1$, and period $0$ is a dummy period before the first arrival. A seed vector is a function $V\times\{0,\dots,n\}\to[0,1]$ (unitInterval), and the seed law is the product of uniform measures (seedMeasure). Expectations are Bochner integrals. Ties go to the least maximizer for a linear order on $V$. The type and its order are arbitrary, so every fixed priority order is covered. An arrival with an available neighbour is matched even at reduced price $0$. $\mathrm{OPT}$ is the integral offline optimum, a finite maximum over feasible reusable matchings, not the LP value. The two-seed runs $\mathrm{PR}(y^1,y^2)$ overwrite the coordinates $(i,k(j)-1)$ and $(i,k(j))$ of a full seed vector. The critical threshold is a supremum over $[0,1]$, with $0$ for an empty set. Lemmas 4–9 hold for every seed vector, since the paper fixes an arbitrary $Y_{-i,j}$.

The goal cannot be met trivially. $\mathrm{OPT}$ maximizes over the same feasibility predicate that the output satisfies, the reward counts matched pairs rather than duals, and the online clause rules out reading future edges or seeds.

A complete development needs the run of the algorithm and its measurability in the seeds, Fubini for the two seeds of one resource, the run-comparison arguments of Lemmas 4, 6 and 8, LP weak duality for Lemma 1, and certified exponential bounds for the last step. The definitions of the model, OPT and the algorithm are reusable for other reusable-resource algorithms. Proofs of any milestone and alternative arguments are welcome.

Selected references

• S. Delong, A. Farhadi, R. Niazadeh, B. Sivan, R. Udwani, Online Bipartite Matching with Reusable Resources, arXiv:2110.07084v2, 2022; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2110.07084
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• G. Aggarwal, G. Goel, C. Karande, A. Mehta, Online vertex-weighted bipartite matching and single-bid budgeted allocations, SODA 2011. https://arxiv.org/abs/1007.1271
• N. R. Devanur, K. Jain, R. D. Kleinberg, Randomized primal-dual analysis of RANKING for online bipartite matching, Proceedings of SODA 2013, 101–107 (as cited in arXiv:2110.07084v2).
• X. Y. Gong, V. Goyal, G. N. Iyengar, D. Simchi-Levi, R. Udwani, S. Wang, Online assortment optimization with reusable resources, Management Science, 2021 (as cited in arXiv:2110.07084v2).
• V. Goyal, G. Iyengar, R. Udwani, Online allocation of reusable resources: Achieving optimal competitive ratio, arXiv:2002.02430, 2020. https://arxiv.org/abs/2002.02430

Motivation

Matching platforms rarely decide on one request at a time. A ride-hailing marketplace clears requests in short windows, an ad exchange serves a video session's slots together, and cloud and retail systems process demand in rounds. Between the fully offline problem and the online model of Karp, Vazirani and Vazirani (STOC 1990) lies a question with an operational reading: how much is it worth to act $K$ times rather than once for each arrival?

Feng and Niazadeh (arXiv:2211.16581v1) answer it exactly for fractional vertex weighted matching. They design a convex-programming algorithm, PR-MWM, with competitive ratio $\Gamma(K)=1-(1-1/K)^K$, and they show that no $K$-stage algorithm does better. The curve runs from $\Gamma(1)=1$ through $\Gamma(2)=3/4$ and $\Gamma(3)=19/27$ down to $1-1/e$.

Timeline. Karp, Vazirani and Vazirani (1990) introduced online bipartite matching with ratio $1-1/e$ for RANKING. Aggarwal, Goel, Karande and Mehta (SODA 2011) extended that ratio to vertex weights. Feng, Niazadeh and Saberi (SSRN, 2020) gave the optimal $3/4$-competitive algorithm for two stages, with a simpler decomposition for the first stage. Feng and Niazadeh (2022) settled the $K$-stage ratio.

Setting

An instance is a bipartite graph $(U,V,E)$ with offline vertices $V$, weights $w_j\ge 0$ and capacities $n_j>0$. Online vertices arrive in $K$ batches $U_1,\dots,U_K$, revealing the edge sets $E_k$. At stage $k$ an algorithm irrevocably allocates $x_{k,ij}\ge 0$ along $E_k$, each online vertex using at most one unit and each $j$ at most its remaining capacity. Its value is the total weight allocated, $\mathrm{ALG}=\sum_k\sum_{E_k}w_jx_{k,ij}$. The benchmark $\mathrm{OPT}$ is the optimal value of the fractional offline LP.

The regularizers are $f_K=\mathbb I\{x=1\}$ and, for $k<K$, $f_k(x)=(1-\tfrac{1-x}{K-k})^{K-k}$, with $F_k(x)=\int_0^xf_k$. They solve the backward recursion $f_k(x)=\max_{y\in[0,1-x]}(1-y)f_{k+1}(x+y)$. PR-MWM keeps levels $y^{(k)}_j$, with $y^{(0)}=0$, and at stage $k$ solves

$$\max_{x\ge 0}\ \sum_{E_k}w_jx_{ij}-\sum_{j}n_jw_jF_k\Bigl(y^{(k-1)}_j+\sum_i\frac{x_{ij}}{n_j}\Bigr) \quad\text{s.t.}\quad\sum_jx_{ij}\le 1,\ \ \sum_ix_{ij}\le n_j\bigl(1-y^{(k-1)}_j\bigr),$$

then updates the levels by $y^{(k)}_j=y^{(k-1)}_j+\sum_ix_{k,ij}/n_j$. A run is any sequence of optimal solutions of these programs.

Formalization targets

Goal: Theorem 1

For every $K\ge 1$ and every finite instance, a run exists, and every run satisfies

$$\Bigl(1-\bigl(1-\tfrac1K\bigr)^K\Bigr)\cdot\mathrm{OPT}\le\mathrm{ALG}.$$

Milestones

Proposition 1 (the recursion, the closed form, and $\min_y 1-(1-y)f_1(y)=\Gamma(K)$); feasibility of a run in the offline LP; the primal-dual certificate; Proposition 3 (KKT for the stage program); Proposition 2 (the structural decomposition, corrected); Step i (dual objective equals $\mathrm{ALG}$); Lemma 1; the bound $f_s(x)\ge x$; and inequality (1) (approximate dual feasibility on each edge).

Significance

The result. Theorem 1 gives the exact value of batching for this class of matching algorithms. It says that the regularizer should hedge hard in early stages and not at all in the last, and it specifies the polynomial that does so, in place of a heuristic discount. Together with the paper's Theorem 3, which is outside this mission, it shows that the ratio is optimal. The same polynomials and Lemma 1 carry over to the paper's configuration allocation model.

Formalizing it. The result is proved on paper in arXiv:2211.16581v1, and no machine-checked proof is known. A formalization yields three reusable pieces: the stage-wise decomposition derived from KKT, a statement of a convex program whose optimum may be non-unique, and the recursive primal-dual argument. It also covers cases the paper passes over: its Saturation claim in Proposition 2 fails as printed on unmatched online vertices and on zero-weight components, and this mission states the corrected form.

Difficulty

The obvious primal-dual argument splits each edge's weight between its endpoints through a fixed function of the final level, as in water-filling. With batches this fails: within one stage, the allocation is decided simultaneously, and an online vertex's dual must be read off the program's own optimum. The step that carries the argument is therefore not a single inequality but the graph decomposition, which turns the KKT multipliers of each stage program into groups of equal price with no edge from a cheaper online group to a dearer offline group. The other delicate point is that the telescoping in Lemma 1 must match the recursion exactly, including the last stage, whose regularizer vanishes and whose dual comes from an LP rather than from the decomposition.

Formalization scope

The namespace is MultiStageAlloc. Stages are natural numbers with $1\le k\le K$. An allocation is a function on $U\times V$ vanishing off $E_k$. Finite $U$ and $V$; batches may be empty; weights may be zero; capacities are positive reals, and $n\equiv1$ gives the printed program. The goal quantifies over every choice of optimal solution, because the optimum is not unique in general, and it asserts that a run exists. The ratio is stated in the multiplicative form $\Gamma(K)\,\mathrm{OPT}\le\mathrm{ALG}$, and $\mathrm{OPT}$ is the LP value, a real supremum over a nonempty bounded set.

A statement about an arbitrary allocation in place of a run would be false, and an existence claim alone would be empty; the goal has both clauses. Proposition 3 uses a $C^1$ convex extension of $F_k$ to all of $\mathbb R$ so that the unconstrained $\max_x$ has a meaning; the extension agrees with $F_k$ on $[0,1]$. The decomposition is a construction on the connected components of the induced support graph, not an arbitrary partition.

A complete development needs KKT conditions for a concave differentiable objective over a polyhedron without Slater's condition, strong duality for the last-stage LP, and elementary calculus for the polynomials. The KKT layer, the LP duality layer and the $\Gamma(K)$ polynomials are reusable beyond this mission. The paper's Theorem 2 (configuration allocation) and Theorem 3 (optimality of $\Gamma(K)$) are not formalized here and are welcome as follow-up missions.

Selected references

• Y. Feng and R. Niazadeh, Batching and Optimal Multi-stage Bipartite Allocations, arXiv:2211.16581v1, 2022. https://arxiv.org/abs/2211.16581
• R. M. Karp, U. V. Vazirani and V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• G. Aggarwal, G. Goel, C. Karande and A. Mehta, Online vertex-weighted bipartite matching and single-bid budgeted allocations, SODA 2011. https://doi.org/10.1137/1.9781611973082.95
• Y. Feng, R. Niazadeh and A. Saberi, Two-stage stochastic matching and pricing with applications to ride hailing, SSRN, 2020; the source's Feng et al. (2020b). https://doi.org/10.2139/ssrn.3613755

Motivation

For a quantum system split into parts, the entanglement entropy $S(A)$ of a region $A$ is the von Neumann entropy of the reduced density matrix of $A$. Every such entropy obeys strong subadditivity (Lieb–Ruskai, 1973): for regions $A$ and $B$,

$$S(A)+S(B)\ \ge\ S(A\cup B)+S(A\cap B),\qquad S(A)+S(B)\ \ge\ S(A\setminus B)+S(B\setminus A).$$

It is the basic structural inequality of quantum information theory, and any proposed formula for entanglement entropy must satisfy it.

In 2006 Ryu and Takayanagi proposed a geometric formula for the entanglement entropy of a quantum field theory that has a gravity dual in one more dimension: the entropy of a region $A$ on the boundary is the area of the minimal bulk hypersurface ending on $\partial A$, divided by $4G_N$. Whether this formula obeys strong subadditivity was a consistency test of the proposal. Hirata and Takayanagi checked it in a range of examples; Headrick and Takayanagi (arXiv:0704.3719, 2007) gave a general argument by cutting and regluing minimal surfaces. This mission formalizes that argument's statement, at the generality the argument supports.

Timeline:

• 1973 — Lieb and Ruskai prove strong subadditivity of the von Neumann entropy.
• 2006 — Ryu and Takayanagi propose the holographic formula (hep-th/0603001); Fursaev derives it in the static case and adds the homology requirement.
• 2007 — Headrick and Takayanagi prove strong subadditivity for the static formula with the homology rule.

Setting

Fix a constant-time slice of a static bulk spacetime, cut off at a finite value of the holographic coordinate. In the formalization this is a topological space $X$, with a subset $\Gamma\subseteq X$, the conformal boundary (the cutoff surface) on which the field theory lives. A boundary region is a set $A\subseteq\Gamma$. The area of a hypersurface is given by a measure $\mu$ on $X$ for which every open set is measurable; for a Riemannian slice it is a constant multiple of the $(d-1)$-dimensional Hausdorff measure.

A bulk region is a member of a class $\mathcal R$ of subsets of $X$. The surface $\partial r$ of a region $r$ is its topological frontier in $X$. Fursaev's homology rule requires the bulk hypersurface $m$ for $A$ to bound, together with $A$, a bulk region: $\partial r=A\cup m$. In the formalization this is $r\cap\Gamma=A$, and the surface charged is $\partial r$.

With $G>0$ Newton's constant, the holographic entanglement entropy is

$$S(A)=\frac{1}{4G}\,\inf\bigl\{\mu(\partial r)\;:\;r\in\mathcal R,\ r\cap\Gamma=A\bigr\}\in[0,\infty],$$

the Lean definition HolographicSSA.holographicEntropy Γ μ G 𝓡 A.

Formalization targets

Goal: both inequalities of (3.1)

For every $X$, $\Gamma$, $\mu$, $G>0$, $\mathcal R$ and all $A,B\subseteq X$:

$$\mathcal R \text{ closed under }\cup,\cap\ \Longrightarrow\ S(A)+S(B)\ \ge\ S(A\cup B)+S(A\cap B),$$ $$\mathcal R \text{ closed under }\setminus\ \Longrightarrow\ S(A)+S(B)\ \ge\ S(A\setminus B)+S(B\setminus A).$$

The two inequalities are also milestones on their own.

Milestones (in proof order)

1. Footnote 3, inclusion. For all $r,s\subseteq X$: $\partial(r\cup s)\cup\partial(r\cap s)\subseteq\partial r\cup\partial s$ and $\partial(r\cup s)\cap\partial(r\cap s)\subseteq\partial r\cap\partial s$.
2. Footnote 3, area inequality. $\mu(\partial(r\cup s))+\mu(\partial(r\cap s))\le\mu(\partial r)+\mu(\partial s)$.
3. The rearranged regions are competitors (p.6, with (3.2)–(3.3)). If $r\cap\Gamma=A$, $s\cap\Gamma=B$ and $r\cup s\in\mathcal R$, then $4G\,S(A\cup B)\le\mu(\partial(r\cup s))$; likewise for $r\cap s$ and $A\cap B$.
4. (3.1), first inequality.
5. (3.1), second inequality.

Significance

The theorem says that the Ryu–Takayanagi prescription, with the homology rule, satisfies the defining inequality of entanglement entropy for every static bulk geometry, not only in computed examples. It was one of the early pieces of evidence that the formula is an entropy, and the cut-and-reglue technique it introduced is the template for later holographic entropy inequalities, such as the monogamy of mutual information (Hayden, Headrick, Maloney, 2011).

The result is proved in the paper, in a few lines and in the generic case. It has not been formalized. A formal version fixes what "region", "surface" and "area" have to mean for the argument to go through, separates the generic-case equality (3.4) from the inequality that actually holds, and supplies the second inequality, which the paper leaves as an exercise. The definition of the holographic entropy is reusable for other holographic inequalities stated in the same setting.

Difficulty

The informal proof says the surfaces of $r_A\cup r_B$ and $r_A\cap r_B$ are "simply rearrangements" of $m_A$ and $m_B$, so their total area is the same. That equality is false without a genericity condition the paper does not define: two unit squares in the plane that touch along a side have perimeters $6+1<4+4$. What holds is an inequality, and it needs more than the printed inclusion $\partial(r\cup s)\cup\partial(r\cap s)\subseteq\partial r\cup\partial s$: a point counted on both new surfaces must lie on both old ones. The second inequality is not proved in the paper at all. Finally, the minima in (2.1) need not be attained, and entropies can be infinite, so the argument has to be run with infima in $[0,\infty]$ rather than with chosen minimal surfaces.

Formalization scope

Conventions committed to in Lean:

• $X$ is any topological space with [MeasurableSpace X] [OpensMeasurableSpace X]; $\Gamma$ is any subset. No metric, Riemannian structure, compactness or finiteness of $\mu$ is assumed.
• The surface of a region is frontier r in $X$ (not the part off $\Gamma$). The homology rule is the equality r ∩ Γ = A.
• The entropy is ENNReal.ofReal (1 / (4 * G)) * ⨅ r ∈ 𝓡, ⨅ (_ : r ∩ Γ = A), μ (frontier r) in ℝ≥0∞, with 0 < G; it is ∞ when no admissible region is homologous to $A$.
• The closure hypotheses on $\mathcal R$ are separate: $\cup$ and $\cap$ for the first inequality, $\setminus$ for the second.
• $A$ and $B$ are arbitrary subsets of $X$; outside $\Gamma$ the entropy is $\infty$.

Trivializing encodings are ruled out: charging only frontier r \ Γ, or relaxing the homology rule to an inclusion, makes $S\equiv0$, and a vanishing constant does the same; the definition uses the full frontier, the equality and $0<G$. Signed functionals, such as the Gauss–Bonnet corrected area (2.2), are not covered.

Infrastructure needed: frontier and closure algebra, additivity of measures on closed sets, and infimum manipulation in ℝ≥0∞, all in Mathlib. Proofs of the milestones, and alternative arguments for the second inequality, are welcome.

Selected references

• M. Headrick, T. Takayanagi, A holographic proof of the strong subadditivity of entanglement entropy, arXiv:0704.3719v1, 2007; Phys. Rev. D 76, 106013 (2007). https://arxiv.org/abs/0704.3719
• S. Ryu, T. Takayanagi, Holographic derivation of entanglement entropy from AdS/CFT, Phys. Rev. Lett. 96, 181602 (2006). https://arxiv.org/abs/hep-th/0603001
• D. V. Fursaev, Proof of the holographic formula for entanglement entropy, JHEP 0609:018 (2006). https://arxiv.org/abs/hep-th/0606184
• T. Hirata, T. Takayanagi, AdS/CFT and strong subadditivity of entanglement entropy, JHEP 0702:042 (2007). https://arxiv.org/abs/hep-th/0608213
• E. H. Lieb, M. B. Ruskai, Proof of the strong subadditivity of quantum-mechanical entropy, J. Math. Phys. 14, 1938 (1973). https://doi.org/10.1063/1.1666274
• P. Hayden, M. Headrick, A. Maloney, Holographic mutual information is monogamous, Phys. Rev. D 87, 046003 (2013). https://arxiv.org/abs/1107.2940

Motivation

The classical secretary problem asks a player to stop on the best of $n$ items that arrive one at a time; with a uniformly random order the optimal success probability is $1/e$, and with an adversarial order nothing nontrivial is possible. Much recent work in online algorithms and mechanism design asks how much prior information restores good guarantees. Kaplan, Naori and Raz (SODA 2020, reference [17] of the paper) let the player first see a sample of the items. Correa, Cristi, Feuilloley, Oosterwijk and Tsigonias-Dimitriadis (arXiv:2011.07869, 2020; later in Management Science, 2025) replace the fixed-size sample by independent sampling: each item is revealed in advance independently with probability $p$. This model handles instances of unknown size and has simpler probabilities, and the paper determines the optimal guarantee exactly when the remaining items arrive in adversarial order.

The optimal stopping problem the paper uses as a tool, stopping on the last $0$ of a random bit string, is related to Bruss's last-success problem (Ann. Probab. 2000), with the difference that the player knows the number of ones and not the length.

Setting

There are $n$ elements with distinct values $v_1,\dots,v_n$. Each element is sampled independently with probability $p\in(0,1)$; the sampled set $S$ is shown to the player, and the remaining online elements $V$ arrive one by one in an order chosen by an adversary who knows the values and $S$. On each arrival the player stops (and keeps it) or continues; she wins if she stops on $\max_{x\in V}v_x$, and by convention she wins if $V=\emptyset$. This is the adversarial order secretary problem with $p$-sampling (AOSp). The success probability of an algorithm is its winning probability, averaged over $S$ with weight $p^{|S|}(1-p)^{n-|S|}$; the success guarantee is its infimum over $n$, the values and the orders.

Algorithms are ordinal: when the $i$-th online element arrives the player knows $n$, $|S|$, and for each online element so far the number of samples and of earlier online elements above it, i.e. the relative ranking of everything seen; she may randomize. The $k$-max algorithm sets the $k$-th largest sample as threshold ($-\infty$ if $|S|<k$) and accepts the first online element above it, with

$$k=\lfloor 1/(1-p)\rfloor,\qquad c(p)=k\,p^{k}(1-p).$$

The proof works in the last zero problem: a random string of $n$ bits, each $1$ with probability $p$; the player knows its number of ones but not $n$, sees the bits in turn, and must stop on the last $0$. Two strings conflict when they have the same number of ones and agree up to the last $0$ of the shorter one; the conflict graph joins conflicting strings whose lengths differ by one.

Formalization targets

Goal: Theorem 1

For every $p\in(0,1)$:

$$\forall n,\ \forall v\ \text{injective},\ \forall\ \text{orders } \sigma(S):\quad \Pr[k\text{-max wins}]\ \ge\ k\,p^{k}(1-p),$$

and for every ordinal randomized algorithm $A$, which may use $n$ and $p$, and every $\varepsilon>0$ there are $n$ and injective $v$ with

$$\Pr[A \text{ wins}] < k\,p^{k}(1-p)+\varepsilon$$

when the online elements arrive in index order.

Milestones

• Lemma 1 (corrected): $\ge c(p)$ for $n\le k$; $\ge c(p)+p^n$ for $n\ge k+1$, with equality for increasing order.
• Lemmas 7–10, 12, 13 and the remark after Lemma 13: the structure and weights of the conflict graph, and why the selection probabilities of any strategy sum to at most $1$ along a monotone path.
• Lemmas 20, 17, 18, 19: local operators, optimality of the fill-in strategy in every window of sizes $[n,n+t]$, and its near-identity with $k$-max.
• Proposition 4: the bound for the last zero problem without knowledge of $n$.
• Proposition 6 and Theorem 4: the colored last zero problem, which carries the bound to players who know $n$.

Significance

The theorem gives an exact answer: the optimal guarantee for AOSp is $k p^k(1-p)$, attained by a single-threshold rule. It equals $1/4$ at $p=1/2$ and tends to $1/e$ as $p\to1$, the value of the full-information adversarial-order problem of Allaart and Islas and of Esfandiari et al. Its negative half holds even for a player who knows $n$ and against an order fixed before sampling, so the sample-dependent adversary is not what makes the problem hard.

The proof is published only on paper. Its positive half is a short counting argument; its negative half rests on the conflict graph, a window-averaging argument, and for known $n$ a proof sketch ("with high probability … the modified conflict graph is (almost) the same", p.27). A machine-checked proof would settle that sketch, and the conflict graph and fill-in machinery formalized here are reusable for other last-success and sampling problems. The formalization also corrects four statements of the preprint (Lemmas 1, 9, 19 and operator 2 of Lemma 20), each with a counterexample recorded in the milestone.

Difficulty

The positive half is elementary. The negative half is not: an upper bound must hold for every randomized ordinal algorithm, including ones that know $n$. The obvious attack, a comparison size by size, fails because the moves that improve a strategy at one size lower it at another; the paper averages over a window of sizes instead and loses $2/(t+1)$ at the window's ends. For known $n$ the window argument must be redone on a colored conflict graph whose weights only concentrate around those of the plain graph, which needs a concentration bound and careful control of the error terms; the paper gives this step as a sketch.

Formalization scope

• Elements are Fin n, values v : Fin n → ℝ injective. The sampled set is summed over all S : Finset (Fin n) with weight $p^{|S|}(1-p)^{n-|S|}$, so every probability is a finite sum and no measure theory is involved.
• An algorithm is A : ℕ → ℕ → List (ℕ × ℕ) → ℝ with values in $[0,1]$: the stopping probability given $n$, $|S|$ and the ordinal history. It sees no values, indices or future elements. In the goal's half (b) it may depend on $n$, and the order is the index order.
• Bit strings are List Bool with true = 1 = sampled. The all-ones string, and in the colored problem a string with no red $0$, is a win by vacuity, as in AOSp when everything is sampled.
• $k$ is ⌊1/(1−p)⌋₊; the guarantee is stated as two quantified inequalities, not as a real infimum, which would be $0$ on an empty or unbounded family.
• A trivializing reading would let the algorithm see the values or the maximum's position, which makes half (b) false, or deny it $n$, which makes half (b) Proposition 4 only. Both are excluded by the history type.

Contributions are welcome at every level: proofs of the structural lemmas (Lemmas 8–10, 12) by induction on strings, of the window lemmas, and of Theorem 4, which needs a binomial concentration bound.

Selected references

• J. Correa, A. Cristi, L. Feuilloley, T. Oosterwijk, A. Tsigonias-Dimitriadis, The Secretary Problem with Independent Sampling, arXiv:2011.07869v1, 2020. https://arxiv.org/abs/2011.07869v1
• H. Kaplan, D. Naori, D. Raz, Competitive Analysis with a Sample and the Secretary Problem, Proceedings of SODA 2020 (reference [17] of arXiv:2011.07869v1).
• F. T. Bruss, Sum the odds to one and stop, Annals of Probability 28(3), 2000. https://doi.org/10.1214/aop/1019160340
• P. Allaart, J. A. Islas, A sharp lower bound for choosing the maximum of an independent sequence, Journal of Applied Probability 53, 1041–1051 (reference [1] of arXiv:2011.07869v1).
• H. Esfandiari, M. HajiAghayi, B. Lucier, M. Mitzenmacher, Prophets, Secretaries, and Maximizing the Probability of Choosing the Best, AISTATS 2020. https://arxiv.org/abs/1910.03798