The OR Formalization Drive

Motivation

In the secretary problem, $n$ candidates with arbitrary values arrive one at a time in a uniformly random order, and an online decision maker must accept or reject each candidate on arrival, irrevocably, keeping at most one. The rule that observes the first $n/e$ candidates and then accepts the first one better than everything seen so far selects the best candidate with probability about $1/e$ (Dynkin, 1963). The problem is a basic model of online selection and, read economically, of posted-price mechanisms for agents who arrive in random order: a rule that compares each agent only against a threshold set by earlier agents is truthful.

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study a variant in which time costs value. Selecting the candidate who arrives at time $t$ earns that candidate's value multiplied by a discount $d(t)$, for an arbitrary non-negative discount function $d$ known in advance. Earlier work treated only specific discount shapes, such as geometric discounting $d(t)=\beta^t$ (Rasmussen and Pliska, 1976). For a general $d$ the classical rule can fail badly: if all the discount mass sits in the first few time steps, a rule that waits through a sample of size $n/e$ earns nothing. The paper shows that the best competitive ratio for arbitrary discounts lies between $\Omega(\log n/\log\log n)$ (its Theorem 4.3) and $O(\log n)$ (its Theorem 4.4). This mission formalizes the upper bound.

Setting

There are $n\ge1$ elements, indexed $\{0,\dots,n-1\}$, with values $v(e)\ge 0$, and $n$ times with discounts $d(t)\ge0$. A uniformly random permutation $\pi$ fixes the order of arrivals: element $\pi(t)$ arrives at time $t$. An algorithm knows $d$ but not $v$; it sees each value on arrival and may select the current element, irrevocably, earning $d(t)\,v(\pi(t))$. Expectations over $\pi$ are exact averages over the $n!$ orders.

The offline optimum on order $\pi$ is $\mathsf{OPT}(\pi)=\max_t d(t)\,v(\pi(t))$; it is a random variable, and the benchmark is its expectation $\mathbb E_\pi[\mathsf{OPT}]$ (p. 4 of the paper).

Let $d_{\max}=\max_t d(t)$ and $v_{\max}=\max_e v(e)$. For $c\ge1$ the $c$-th discount class is the set of times

$$P_c=\{\,i : 2^{-c}d_{\max}<d(i)\le 2^{-(c-1)}d_{\max}\,\}.$$

The quantity $\mathsf{OPT}_c$ is the part of $\mathbb E_\pi[\mathsf{OPT}]$ earned when the optimal time (the smallest time attaining the maximum) lies in $P_c$.

The classical secretary rule on $m$ arrivals observes the first $\lfloor m/e\rfloor$ and then selects the first arrival that ranks above every earlier arrival. Ranks use a fixed tie-break order: larger value first, and smaller element index among equal values.

The algorithm $\mathcal A$ sets $M=3\lceil\log_2 n\rceil+2$, draws $c\in\{1,\dots,M\}$ uniformly, and runs the classical rule on the subsequence of arrivals at the times of $P_c$, ignoring all other arrivals.

Formalization targets

Goal: Theorem 4.4 with its explicit constant

$$\mathbb E_\pi[\mathsf{OPT}]\;\le\;4e\,\bigl(3\lceil\log_2 n\rceil+2\bigr)\;\mathbb E[\mathcal A]\qquad(n\ge1,\ d\ge0,\ v\ge0).$$

The paper states $\mathbb E[\mathsf{OPT}]/\mathbb E[\mathcal A]\le O(\log n)$; the constant $4e$ is the one its proof yields.

Milestones

1. The classical secretary rule selects the top-ranked of $m\ge1$ elements with probability at least $1/e$ (§2, p. 4).
2. $\mathsf{OPT}_1\ge v_{\max}d_{\max}/n$ (proof of Theorem 4.4, p. 7).
3. $\mathsf{OPT}_c\le 2^{-c}\,2n^2d_{\max}v_{\max}$ for every $c\ge1$ (p. 7).
4. $\sum_{c=1}^{3\lceil\log_2 n\rceil+1}\mathsf{OPT}_c\ge\tfrac12\mathbb E_\pi[\mathsf{OPT}]$ (p. 7).
5. $\mathbb E[\mathcal A_c]\ge\mathsf{OPT}_c/2e$ for every $c\ge1$, where $\mathcal A_c$ is the classical rule on $P_c$ (p. 7).

Significance

The theorem shows that a general discount function costs only a logarithmic factor against the offline benchmark, and that one algorithm achieves this without any knowledge of the values. Together with the lower bound of Theorem 4.3 it pins the competitive ratio of the discounted secretary problem between $\log n/\log\log n$ and $\log n$. The same scale-splitting idea, stated in the paper as Theorem 4.5 without full proof, extends the bound to the weighted discounted problem.

The result is proved in the paper; to our knowledge it has not been formalized. A complete development would also produce a machine-checked proof of the classical secretary guarantee for the rule with sample size exactly $\lfloor m/e\rfloor$ at every finite $m$, with an explicit tie-break, which is reusable by every secretary-type mission. Milestone 1 is that statement. Sharper constants or a smaller class range are welcome as additional statements but do not replace the goal, which is about this algorithm with this $M$.

Difficulty

The obvious argument, running the classical rule on all $n$ arrivals, fails because the discounts can be concentrated at times the rule spends sampling. Splitting by discount scale fixes this but creates two problems. First, there are unboundedly many scales, and one has to show that the offline optimum's mass outside the top $O(\log n)$ of them is negligible against $\mathbb E[\mathsf{OPT}]$, a random quantity rather than a fixed maximum. Second, the classical rule on a class sees only a random subset of the elements, in random order, and the guarantee must be transferred to this subsequence, conditioning on which elements land in $P_c$. Neither step is deep, but both require careful bookkeeping of permutations, and the classical $1/e$ bound at finite $m$ with a floor in the sample size is itself a nontrivial estimate.

Formalization scope

Elements and times are Fin n, an order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and the paper's time $t=1,\dots,n$ is index $t-1$. Values and discounts are Fin n → ℝ with non-negativity hypotheses. Every expectation is the finite average $\frac1{n!}\sum_\pi$; the algorithm's random class is the explicit average $\frac1M\sum_{c=1}^M$. Maxima are suprema over the finite index set. The logarithm is base 2, $\lceil\log_2 n\rceil$ is Nat.clog 2 n, and the sample size is Nat.floor (m / Real.exp 1). Ties are broken by the order on Lex (ℝ × (Fin n)ᵒᵈ) (larger value, then smaller index); distinct values are not assumed. The optimal time is the smallest maximizing time, so that the $\mathsf{OPT}_c$ add up to $\mathbb E[\mathsf{OPT}]$. Competitiveness is stated multiplicatively, never as a quotient, so $\mathbb E[\mathcal A]=0$ is not a loophole.

The goal is a statement about the specific algorithm $\mathcal A$, not "there exists an algorithm": an existential over unrestricted algorithms is witnessed by a clairvoyant rule that reads the values in advance. $\mathcal A$ sees the values only through comparisons among arrivals that have already occurred, and $\mathbb E[\mathsf{OPT}]$ is the expected offline maximum over the same random order, not $d_{\max}v_{\max}$.

Needed infrastructure: averages over permutations and the fact that the elements landing at a fixed set of times form a uniformly random subset in uniformly random order; the finite-$m$ analysis of the classical rule; and elementary estimates on geometric sums. Contributions of general lemmas about uniform permutations are welcome and reusable.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.139
• E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Math. Doklady 4, 1963.
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
• L. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2, 1976. https://doi.org/10.1007/BF01458209
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007. https://dl.acm.org/doi/10.5555/1283383.1283429

Why airlines allocate seats by fare class

An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.

This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).

Setting

A leg has capacity $n$ seats (the thesis also writes $C$). There are finitely many fare classes $i$. Class $i$ has an average fare $f_i \ge 0$ and receives a random number of requests $r_i \in \{0,1,2,\dots\}$, with law $p_i$. The seats are split into allocations $S_i \in \mathbb{N}$, one per class.

With $S$ seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are

$$b = \min(r, S), \qquad l = (r - S)^+ \qquad \text{(Eq. (5.3))}.$$

The expected revenue of class $i$ is $\bar R_i(S_i) = f_i \cdot \bar b_i(S_i)$ with $\bar b_i(S_i) = E[\min(r_i,S_i)]$, and the leg's expected revenue is $\bar R = \sum_i \bar R_i(S_i)$ (Eq. (5.9)). Write

$$\bar P_i(S) = P[r_i \ge S], \qquad \mathrm{EMSR}_i(S) = f_i \cdot \bar P_i(S) \qquad \text{(Eqs. (5.11), (6.1), (6.2))},$$

the expected marginal seat revenue of the $S$-th seat of class $i$. The value of the $k$-th seat of class $i$ in the integer program of p. 90 is $m_i(k) = \mathrm{EMSR}_i(k)$, $k = 1, \dots, n$.

Formalization targets

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)

Let $T$ be any set of $n$ pairs $(i,k)$, $1 \le k \le n$, such that every $m_i(k)$ with $(i,k) \in T$ is at least every $m_j(l)$ with $(j,l) \notin T$, and let $S^T_i = \#\{k : (i,k) \in T\}$. Then $\sum_i S^T_i = n$ and

$$\sum_i f_i\, E[\min(r_i, S_i)] \;\le\; \sum_i f_i\, E[\min(r_i, S^T_i)] \qquad \text{for every } S \text{ with } \textstyle\sum_i S_i \le n .$$

The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.

Milestones

1. Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
2. Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$.
3. Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$.
4. Eq. (4.5): the 0–1 vector equal to $1$ on a set of $n$ largest $m_i(k)$ is an optimal solution of the linear program $\max \sum_{i,k} X_{ik} m_i(k)$ subject to $\sum X_{ik} \le n$, $0 \le X_{ik} \le 1$.
5. Eq. (5.13), discrete form: an allocation of exactly $C$ seats maximises $\bar R$ among such allocations if and only if some $\lambda$ satisfies $\mathrm{EMSR}_i(S_i) \ge \lambda$ whenever $S_i \ge 1$ and $\mathrm{EMSR}_i(S_i + 1) \le \lambda$, for all $i$.

Significance

The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting $n \times (\text{number of classes})$ numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.

These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.

Difficulty

The thesis argues with continuous densities and derivatives, setting $\partial \bar R / \partial S_i$ equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be $P[r \ge S]$ rather than the $P[r > S]$ of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the $n$ largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment $\{1, \dots, S_i\}$.

Formalization scope

All declarations live in the namespace SeatInventory.Distinct. Conventions:

• Integer demand. The law of class $i$'s requests is d i : PMF ℕ; expectations are series over $\mathbb{N}$. The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).
• Tail convention. $\bar P(S) = P[r \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11) ("the probability of selling $S_i$ or more seats"), not the $P[r > S]$ of Eq. (5.2).
• Seat numbers start at 1, and the pairs $(i,k)$ range over $k \in \{1, \dots, n\}$, as the 600 variables of a 150-seat, four-class problem on p. 90 indicate.
• Nonnegative fares $f_i \ge 0$ are assumed in every statement that needs them; with a negative fare the capacity constraint $\sum S_i \le n$ would not bind and the claims fail.
• Finite mean of the requests is assumed explicitly for Eq. (5.6); the thesis assumes it silently. Expected bookings are bounded and need no assumption.
• Capacity. The goal and the LP compare against allocations with $\sum_i S_i \le n$ (the LP's constraint); milestone 5 compares allocations of exactly $C$ seats (Eq. (5.8)).
• No independence assumption. Expected revenue of distinct inventories depends only on each class's marginal law, so the statements take one law per class.
• "Decreasing" is non-increasing. The thesis's justification in Sect. 6.1.1 gives only monotonicity; strict decrease fails for bounded demand.
• LP integrality. "The solution will be integer" is stated as: the indicator of every set of $n$ largest values is optimal. With ties the LP also has fractional optima.

The expected revenue in the goal is computed from the booking rule $\min(r_i, S_i)$; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of $\bar R$. Either shortcut would make the goal a tautology and is ruled out.

Needed infrastructure: tail sums of a PMF ℕ, telescoping of $E[\min(r, S)]$, and a finite exchange argument for sums of the $n$ largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of $n$ largest values, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• P. P. Belobaba, Airline yield management: an overview of seat inventory control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
• P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134

Why airlines protect seats

An airline sells the seats of one flight in several fare classes at different prices, all drawn from one shared cabin. Discount fares are bought early, under advance-purchase restrictions, while most high-fare requests arrive close to departure. Accepting every early low-fare request fills the aircraft with cheap passengers and turns away late high-fare passengers; refusing too many leaves seats empty. Seat inventory control decides how many seats to keep away from the low fare. Peter Belobaba's 1987 MIT thesis (Flight Transportation Laboratory Report R87-7) introduced the expected marginal seat revenue (EMSR) model for this decision, and EMSR-type rules remain the basis of the booking-limit logic in airline revenue management systems.

Timeline. Littlewood (1972, AGIFORS Symposium Proceedings; reprinted 2005) proposed accepting a low-fare request as long as its fare is at least the high fare times the probability of selling all remaining seats to high-fare passengers. Analysts at Trans World Airlines (1973) and Richter at Lufthansa (1982) gave equivalent formulations for the dynamic case. Belobaba (1987, Ch. 5) restated the two-class rule as a static protection level for nested inventories and extended it heuristically to many classes. Brumelle and McGill (Operations Research 41, 1993) and Curry (Transportation Science 24, 1990) later proved optimality of nested protection levels for any number of classes under low-to-high arrivals, and showed that Belobaba's multi-class EMSR levels are not optimal for three or more classes. This mission concerns only the two-class result, which is correct.

Setting

A single flight leg has capacity $C \in \mathbb N$. Class 1 has fare $f_1$, class 2 has fare $f_2$, with $0 \le f_2 \le f_1$. The numbers of requests for the two classes are random variables $r_1, r_2$ with values in $\mathbb N$, defined on a probability space $(\Omega, \mu)$ and independent. There are no cancellations, no no-shows, and a refused request is lost.

The inventory is nested: a class-1 request is accepted as long as any seat is unsold. A protection level $S \in \{0, \dots, C\}$ is the number of seats reserved for class 1; it sets the class-2 booking limit $BL_2 = C - S$. All class-2 requests arrive before any class-1 request. Class 2 therefore books $\min(r_2, C - S)$ seats and class 1 books $\min(r_1, C - \min(r_2, C-S))$, and the realised revenue is

$$R_S = f_2 \min(r_2, C - S) + f_1 \min\bigl(r_1,\, C - \min(r_2, C - S)\bigr).$$

The expected revenue is $\bar R(S) = \mathbb E[R_S]$.

The tail probability of class 1 is $\bar P_1(S) = P[r_1 \ge S]$, the probability of receiving $S$ or more class-1 requests, and the expected marginal seat revenue of the $S$-th class-1 seat is

$$\mathrm{EMSR}_1(S) = f_1 \cdot \bar P_1(S).$$

For a single class with $S$ seats the expected revenue is $f_1\,\mathbb E[\min(r_1, S)]$, and $\mathrm{EMSR}_1(S)$ is its increment from $S-1$ to $S$ seats. The EMSR protection level $S_2^1$ is the largest integer $S \in \{0, \dots, C\}$ with

$$\mathrm{EMSR}_1(S) \ge f_2 .$$

In Lean these objects are nestedRevenue, expectedNestedRevenue, tailProb, classRevenue, emsr and emsrProtectionLevel in SeatInventory.Nested.

Formalization targets

Goal: Eqs. (5.15)–(5.16), optimality of the EMSR protection level

$$\bar R(S) \le \bar R(S_2^1) \qquad \text{for all } S \in \{0, \dots, C\}.$$

The goal fixes no distribution: it holds for every pair of independent $\mathbb N$-valued demands, and $S_2^1$ depends only on $f_2/f_1$ and the law of $r_1$.

Milestones

1. Eq. (5.11). $f_1\mathbb E[\min(r_1,S)] - f_1\mathbb E[\min(r_1,S-1)] = f_1 P[r_1 \ge S]$ for $S \ge 1$.
2. Eqs. (6.1)–(6.2). $\bar P_1$ and, for $f_1 \ge 0$, $\mathrm{EMSR}_1$ are non-increasing in $S$.
3. Eq. (4.8), Littlewood's rule, already on the platform as RevenueManagement.littlewood_marginal_value (Talluri and van Ryzin's Eq. (2.1), proved).
4. Sect. 5.2, p. 112. $\bar R(S) \le \bar R(S_2^1)$ for $S_2^1 \le S \le C$: a smaller booking limit for class 2 cannot raise expected revenue.
5. Sect. 5.2, p. 114. With the same class-2 limit $C - S$, the expected nested revenue is at least the expected revenue of two distinct inventories with $S$ and $C - S$ seats, strictly if $f_1 > 0$ and $P[r_2 < C - S,\ r_1 > S] > 0$.

Significance

The two-class result says that, for a static booking limit set once before sales open and low-fare demand arriving first, the airline needs only the high-fare demand distribution and the fare ratio to set the optimal limit; the low-fare forecast is irrelevant. This is the rule that the thesis then applies class by class in multi-class nested systems, and it is the base case against which the later exact multi-class theory (Brumelle–McGill, Curry) is checked. Milestone 5 makes precise why nested inventories dominate the distinct-inventory allocation of the thesis's Sect. 5.1 with the same class-2 limit.

The result is classical and proved, in the sense that the optimality of a two-class threshold policy follows from Littlewood's argument and from the dynamic-programming treatment in Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004, Ch. 2). On Prove2Me, Littlewood's marginal rule and the dynamic-programming optimality of nested protection levels (RevenueManagement.static_optimal_controls) are formalized, but in Bellman form: there the protection level is defined through the value function of a dynamic program. What is not formalized is the statement in Belobaba's form, where the protection level is the explicit threshold of $f_1 P[r_1 \ge S]$ against $f_2$ and the objective is the explicit expected revenue of a booking limit. Connecting the two forms, and the comparison with distinct inventories, is the work of this mission.

Difficulty

The expected revenue couples the two demands through the capacity left by class 2, so $\bar R$ is not a sum of single-class revenues and is not separately concave in an obvious way. The step that requires care is the increment $\bar R(S) - \bar R(S-1)$: it is not $\mathrm{EMSR}_1(S) - f_2$, as the thesis's sentence after the milestone on p. 112 suggests, because the extra protected seat matters only on the event that class 2 would have reached its limit. Independence of $r_1$ and $r_2$ is what makes that event's probability factor out; without independence the threshold rule is not optimal. The discrete reading matters too: with $P[r_1 > S]$ in place of $P[r_1 \ge S]$ the rule is off by one seat and the claim fails.

Formalization scope

Conventions the Lean statements commit to:

• Demands are $\mathbb N$-valued measurable random variables r₁ r₂ : Ω → ℕ on a probability space μ; the goal and milestone 4 assume IndepFun r₁ r₂ μ. The thesis writes continuous densities (Eqs. (5.1)–(5.5)) but requires integer seat counts; the discrete model is used throughout.
• $\bar P_1(S) = P[r_1 \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11), not $P[r_1 > S]$ as in Eq. (5.2).
• The EMSR protection level is the largest $S \in \{0,\dots,C\}$ with $f_1 P[r_1 \ge S] \ge f_2$ (Eq. (5.15)); Eq. (5.16)'s equality is the continuous idealisation and is not stated.
• Booking order: all class-2 requests precede all class-1 requests (pp. 108, 112). This order is built into the revenue formula, not assumed separately.
• Fares satisfy $0 \le f_2 \le f_1$; the thesis has $f_1 > f_2$, and the statements also cover equality.
• Expectations are Bochner integrals of bounded revenues, probabilities are μ.real; seat counts use truncated subtraction only where $S \le C$.

A trivializing formalization is ruled out: $S_2^1$ is defined by the threshold of (5.15), never as an argmax of expected revenue, and the expected revenue is computed from the realised revenue of the booking process, not postulated as a sum of marginal terms.

The multi-class EMSR levels of Eqs. (5.19)–(5.29) and the dynamic revision of Eqs. (5.31)–(5.32) are out of scope. Proofs need the discrete expectation identity $\mathbb E[\min(r,S)] - \mathbb E[\min(r,S-1)] = P[r \ge S]$ and expectation of products of independent bounded functions, both in Mathlib's reach and reusable for other single-leg revenue models. Proofs of any milestone, and a proof of the goal from milestones 1, 2 and 4 plus the matching lower-half argument, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41, 1993. https://doi.org/10.1287/opre.41.1.127
• R. E. Curry, Optimal airline seat allocation with fare classes nested by origins and destinations, Transportation Science 24, 1990. https://doi.org/10.1287/trsc.24.3.193
• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Why protection levels and their inputs matter

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

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

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

Milestones, in attack order

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

An on-line algorithm must answer each request as it arrives, without knowing the requests to come; paging, caching, the $k$-server problem and metrical task systems are standard examples. Its quality is measured by competitive analysis: its cost is compared with the cost of an optimal off-line solution that knows the whole request sequence. For randomized on-line algorithms the comparison depends on how much the adversary producing the requests is allowed to see. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; conference version STOC 1990) introduced the three standard adversaries — oblivious, adaptive on-line and adaptive off-line — and related the competitive ratios achievable against each.

Their Theorem 2.2 (manuscript p. 10) shows that if a randomized algorithm is $\alpha$-competitive against adaptive on-line adversaries and some randomized algorithm is $\beta$-competitive against oblivious adversaries, then the first algorithm is $\alpha\beta$-competitive against adaptive off-line adversaries. This mission formalizes the paper's claim (manuscript p. 11) that this product bound cannot be improved in general, together with the explicit construction on pp. 12–13 that proves it.

Setting

A request-answer game consists of a request set $R$, a finite answer set $A$, and cost functions $f_n : R^n \times A^n \to \mathbb R$. For a request sequence $\underline r \in R^n$, the off-line optimum is $c(\underline r) = \min_{\underline a \in A^n} f_n(\underline r, \underline a)$. A deterministic on-line algorithm $G$ answers the $i$-th request with $a_i = g_i(r_1, \dots, r_i)$; a randomized one is a probability distribution over deterministic algorithms $G_x$, $x$ being the coin tosses.

An adaptive off-line adversary $Q$ chooses each request $r_{i+1} = q_i(a_1, \dots, a_i)$ from the answers given so far, stops after at most $d_Q$ requests, and pays the off-line optimum $c_Q(G) = c(\underline r)$ of the requests it made; the algorithm pays $c_G(Q) = f_n(\underline r, \underline a)$. An adaptive on-line adversary $S$ must in addition answer each request itself, before the algorithm does, with $b_{i+1} = p_i(a_1, \dots, a_i)$, and pays $c_S(G) = f_n(\underline r, \underline b)$. An oblivious adversary fixes $\underline r$ in advance and pays $c(\underline r)$. A randomized $G$ is $\alpha$-competitive against oblivious adversaries if $\mathbb E_x[c_{G_x}(\underline r)] \le \alpha\, c(\underline r)$ for all $\underline r$, and against adaptive on-line adversaries if $\mathbb E_x[c_{G_x}(S)] \le \mathbb E_x[\alpha\, c_S(G_x)]$ for all $S$.

The construction uses the mates game: $R = A$ is a set of $2t$ elements split into $t$ pairs of mates, and for $n \ge 2$ the cost depends only on the first answer $a_1$ and the second request $r_2$: it is $1$ if $a_1 = r_2$, $M$ if $a_1$ is the mate of $r_2$, and $m$ otherwise. The algorithm $G$ draws $a_1$ uniformly at random. The parameters solve

$$\beta = \frac{(2t-2)m + M + 1}{2t}, \qquad \alpha = \frac{1 + (2t-1)M}{2 + (2t-2)m}.$$

Formalization targets

Goal: tightness of Theorem 2.2

For $1 < \beta \le \alpha$ (or $\alpha = \beta = 1$) and every $C < \alpha\beta$, there are a game and a randomized algorithm $G$ such that

$$G \text{ is } \alpha\text{-competitive against adaptive on-line adversaries}, \qquad G \text{ is } \beta\text{-competitive against oblivious adversaries},$$

and for every randomized algorithm $K$ some adaptive off-line adversary $Q$ achieves

$$\mathbb E[c_Q(K)] > 0, \qquad \mathbb E[c_K(Q)] \ge C\cdot \mathbb E[c_Q(K)].$$

Milestones (pp. 12–13)

1. The closed forms $m(t)$, $M(t)$ are the unique solution of the two equations.
2. $m(t) \to \beta$ and $M(t) \to \alpha\beta$ as $t \to \infty$.
3. For all large $t$: $M(t) \ge \max(m(t)^2, C)$, $1 \le m(t) \le M(t)$, $\alpha(m(t)-1) \le M(t) - m(t)$.
4. $G$ is $\beta$-competitive against oblivious adversaries in the mates game.
5. $G$ is $\alpha$-competitive against adaptive on-line adversaries in the mates game.
6. An adaptive off-line adversary makes every algorithm pay $M$ while paying $1$.

Significance

The result. Together with Theorem 2.2, the claim pins down exactly how much the adaptive off-line adversary can gain over the other two: the product $\alpha\beta$ is an upper bound for every game and is approached by a single game for every admissible pair $(\alpha, \beta)$. It shows that no general argument relating the three adversary models can give a bound better than the product, so any improvement for a specific problem (paging, $k$-server) must use the structure of that problem. The paging example cited on p. 11 (RANDOM against the three adversaries) gives one instance of tightness; the mates game gives tightness for every admissible pair.

Formalizing it. The result is proved in the paper, in about one page, with two steps left to the reader ("by inspection of the equations", "a simple case analysis"). No machine-checked proof of this or of any statement about adaptive adversaries is known to us. The formalization makes the model of §2 precise (sequences, stopping, the order in which adversary and algorithm commit, expectations over coins), checks the asymptotics of the parameters, and verifies the case analysis, which on inspection needs an inequality the page does not state. Two printed formulas on p. 12 contain typos; the formal statements carry the correct values.

Difficulty

The construction is explicit, but each competitiveness claim quantifies over all adversaries, which may adapt their requests to the algorithm's random answers, stop at any time, and (for the on-line adversary) commit to their own answers in advance. The algebra of $\alpha$-competitiveness is tight: the adversary's best expected advantage is exactly zero, so every case of its best reply must be checked with no slack. The page's condition $M \ge m^2$ does not suffice for this: when $a_1$ is neither the adversary's first answer nor its mate, the reply "mate of $a_1$" beats the reply "the adversary's own answer" only when $\alpha(m-1) \le M - m$, which holds for the solved parameters but is not implied by $M \ge m^2$. At $\beta = 1 < \alpha$ the solved parameter $m$ is below $1$ for every $t$, and the oblivious bound fails.

Formalization scope

All declarations live in OnlineRandomization.Tightness. The conventions:

• Costs are real-valued; the paper allows $+\infty$, so the game class is a special case.
• Answer sets are nonempty finite types; request sets are arbitrary types.
• Sequences are Lean lists, oldest first; cost r a is $f_n$ on lists of equal length $n$.
• Adversaries return none for "stop" and carry a depth bound $d_Q$; an on-line adversary's answer $b_{i+1}$ depends only on $a_1, \dots, a_i$.
• Randomized algorithms are a probability space of coins with a deterministic algorithm per coin and measurable answers; expectations are Bochner integrals, with $\alpha$ applied inside the expectation. In the goal, coin spaces range over Type.
• Competitiveness uses the ratio functions $x \mapsto \alpha x$ and $x \mapsto \beta x$, with no additive constant.
• The mates game is on Fin t × Bool, with mate $(i, b) \mapsto (i, \lnot b)$. The paper leaves the costs of plays with fewer than two requests undefined; the formalization sets $f_0 = 0$ and $f_1 \equiv 1$ (with $f_1 \equiv 0$ the algorithm would not be $\alpha$-competitive).
• Range. The goal assumes $1 < \beta \le \alpha$ or $\alpha = \beta = 1$; the page's case $\beta = 1 < \alpha$ is not covered by its construction and is left out. In fact the claim is false there for $1 < C < \alpha$: an algorithm that is $1$-competitive against oblivious adversaries answers optimally, almost surely, on every request sequence (its cost is never below the optimum and its expected cost does not exceed it), and an adaptive off-line adversary reaches only finitely many request sequences, so against $K = G$ every adversary has $\mathbb E[c_G(Q)] = \mathbb E[c_Q(G)]$, a ratio of $1 < C$.

The positivity requirement $\mathbb E[c_Q(K)] > 0$ in the goal is essential: without it the adversary that asks nothing satisfies $\mathbb E[c_K(Q)] \ge C \cdot 0$ for every $K$, and the third clause would hold vacuously.

A complete development needs: finite expectations over a uniform coin, the evaluation of the play of an adversary against a constant algorithm, and limit and eventual-inequality arguments for rational functions of $t$. The model of §2 is shared with the other missions of this series and is reusable for any request-answer formulation of an on-line problem. Proofs of individual milestones are welcome.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994) 2–14. https://doi.org/10.1007/BF01294260 (cited from the authors' manuscript, manuscript pp. 7–13).
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5.
• P. Raghavan, M. Snir, Memory versus randomization in on-line algorithms, IBM Journal of Research and Development 38 (1994) 683–707. https://doi.org/10.1147/rd.386.0683

Why randomization matters in online algorithms

An online algorithm must answer each request before it sees the next one. Its performance is compared with an optimum that may choose all its answers after seeing the complete request string. Randomization can improve an online algorithm's guarantee when the request string is fixed in advance. The comparison changes when an adversary chooses later requests after seeing the algorithm's earlier answers. Ben-David, Borodin, Karp, Tardos and Wigderson studied these choices of adversary in a common request-answer model and proved a general relation between their competitive guarantees (Ben-David et al., 1994, manuscript §§2–3).

The paper distinguishes three adversaries. An oblivious adversary fixes the request string before the algorithm's random choices affect any answer. An adaptive off-line adversary chooses the next request from previous answers but serves the resulting request string optimally after the play. An adaptive on-line adversary also chooses its own answer as each request arrives. The ability to react to answers makes the latter two adversaries materially different from the oblivious one for randomized algorithms (Ben-David et al., 1994, manuscript pp. 7–9).

Request-answer games and competitive cost

A request-answer game has a request set $R$, a finite nonempty answer set $A$, and a real cost $f_n(r,a)$ for a request string $r\in R^n$ and an answer string $a\in A^n$. The off-line optimum for $r$ is $c(r)=\min_{a\in A^n}f_n(r,a)$. A deterministic online algorithm $D$ returns its $i$th answer from the first $i$ requests alone; it has no access to the rest of $r$ or to the eventual stopping time. Its cost on $r$ is $c_D(r)=f_n(r,D(r))$.

A randomized online algorithm is a distribution over deterministic online algorithms. With coins $\omega$, write $G_\omega$ for the resulting deterministic algorithm. For a fixed request string $r$, $G$ is $\beta$-competitive against oblivious adversaries when $\mathbb E_\omega[c_{G_\omega}(r)]\leq\beta(c(r))$. The paper calls a transformation “linear” when it has the affine form $x\mapsto ux+v$ (Ben-David et al., 1994, manuscript p. 7).

An adaptive off-line adversary $Q$ has a rule from prior answer strings to either the next request or a stop signal, together with a common finite upper bound on play length. Let $r(G_\omega,Q)$ denote its request string and $c_Q(G_\omega)=c(r(G_\omega,Q))$. Its competitiveness condition places the transformation inside the expectation: $\mathbb E_\omega[c_{G_\omega}(Q)]\leq\mathbb E_\omega[\alpha(c_Q(G_\omega))]$. An adaptive on-line adversary $S$ has the same request rule and an additional answer rule; its own cost is $c_S(G_\omega)$, and the corresponding condition uses $\mathbb E_\omega[\alpha(c_S(G_\omega))]$ on the right (Ben-David et al., 1994, manuscript pp. 8–9).

Formalization targets

Randomization against adaptive off-line adversaries

The first target is Theorem 2.1: if some randomized algorithm is $\alpha$-competitive against every adaptive off-line adversary, a deterministic algorithm has that same guarantee on every request string:

$$\exists G\;\forall Q,\quad \mathbb E[c_G(Q)]\leq\mathbb E[\alpha(c_Q(G))]\quad\Longrightarrow\quad\exists D\;\forall r,\quad c_D(r)\leq\alpha(c(r)).$$

Composition of two guarantees

Theorem 2.2 takes an $\alpha$ guarantee for $G$ against adaptive on-line adversaries and a $\beta$ guarantee for another randomized algorithm against oblivious adversaries. It concludes that $G$ has the composed guarantee against adaptive off-line adversaries:

$$\mathbb E[c_G(Q)]\leq\mathbb E[(\alpha\circ\beta)(c_Q(G))]\qquad\text{for every }Q.$$

The mission goal is Corollary 2.1, the deterministic consequence of these two results:

$$\exists D\;\forall r,\qquad c_D(r)\leq(\alpha\circ\beta)(c(r)).$$

The milestones follow the paper's two theorems and the stated claims in their proofs, including the finite-horizon winning-position formulation and the adversary that simulates a fixed online algorithm (Ben-David et al., 1994, manuscript pp. 9–13).

What the result supplies

The corollary turns the existence of two randomized guarantees under different information rules into the existence of a deterministic online strategy with an explicit composed cost transformation. It is an existence result: it does not say that the deterministic strategy can be computed efficiently from the randomized algorithms. The paper itself notes that such a construction is unavailable in full generality and then examines settings where constructive versions are possible (Ben-David et al., 1994, manuscript p. 13).

The mathematical results were proved in the 1994 paper; this mission asks for machine-checked Lean proofs of the abstract model, the intermediate claims, and Corollary 2.1. The local draft currently contains compiled statements with proof placeholders, so it does not yet provide checked proofs. A completed development would make the adversary distinctions and the exact placement of expectations available for reuse in later online-algorithm formalizations.

Why the proof is difficult

The apparent shortcut is to treat an adaptive request sequence as fixed and apply a guarantee against oblivious adversaries directly. That loses the dependence of later requests on the algorithm's earlier answers. For Theorem 2.1, a winning request strategy must have one finite horizon that works for every answer path; separate finite horizons for each branch do not suffice when the answer set is infinite. For Theorem 2.2, the simulated adversary must make its own answers before the algorithm answers the current request, while still matching a fixed online benchmark along every resulting play. The expectation inequalities must remain valid when the request string itself depends on the algorithm's coins (Ben-David et al., 1994, manuscript pp. 9–11).

Formalization scope

Lean represents requests and answers as oldest-first lists. List index zero is request one in the paper. The general game is a separate definition; the algorithm, adversary, and competitiveness definitions build on it. An off-line adversary's rule returns Option R, where none is the stop signal, and has a uniform finite depth bound. A randomized algorithm consists of a coin probability space and a deterministic prefix algorithm for each coin; its answer events are measurable. Finiteness of $A$ and bounded play depth make the cost of each fixed adversarial play take finitely many values, so its real expectation is an ordinary integrable expectation.

The formal game uses real-valued costs, a deliberate restriction of the paper's $\mathbb R\cup\{\infty\}$ costs. The answer set is finite and nonempty, while the request set may be infinite. The transformations $\alpha$ and $\beta$ are affine. Theorem 2.2 and the goal assume $\alpha$ is monotone: the paper applies $\alpha$ to an inequality in its proof, and its competitive-ratio examples have positive slope. Theorem 2.1 does not need this added assumption. The two randomized algorithms may have different coin spaces, each an arbitrary Lean type at the declaration's universe level. The off-line and on-line adaptive comparisons retain $\alpha$ inside the expectation.

The target ranges over every equal-length request and answer play generated by these rules, including an adversary that stops without a request. It does not allow the deterministic algorithm to see future requests or choose a different policy for each adversary. Reusable contributions include the game interface, bounded adaptive plays, measurable randomized algorithms, and finite-horizon winning positions. The statements of all three principal results, their intervening claims, and proofs of those statements are within scope.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos and A. Wigderson, On the Power of Randomization in On-Line Algorithms, Algorithmica 11, 1994. DOI: 10.1007/BF01294260. The local source is the authors' 20-page manuscript; citations above use its page numbers.

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$. It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$, local search achieves $1/3$ and $2/5$, and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$.
• Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$-approximation and a randomized $1/2$-approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$. The function $f$ is submodular if

$$f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .$$

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

$$F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],$$

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$. A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$, and $\{u\}$ also denotes the unit vector at $u$. For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$). In iteration $i = 1, \dots, n$ compute

$$a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),$$

set $a_i' = \max\{a_i, 0\}$, $b_i' = \max\{b_i, 0\}$, and update

$$x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},$$

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$. The output is the random set $R(x_n)$. Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$.

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

$$x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].$$

Milestones, in the order the proof uses them

1. $a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
2. Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$, and $OPT_n = x_n = y_n$.
3. (4) and (5): if $a_i \ge 0$ and $b_i > 0$, then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$.
4. (6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$, whether or not $u_i \in OPT$.
5. Lemma A.2: for every $1 \le i \le n$,

$$F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].$$

6. Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$.

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$, and $F$ restricted to characteristic vectors is $f$. These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$. Second, inequality (6) is written out only for $u_i \notin OPT$, and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$, and that every state stays in $[0,1]^{\mathcal N}$, where the antitonicity applies.

Formalization scope

• The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$.
• The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$, and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$. Statements hold for every such order.
• The footnote's convention $a_i'/(a_i'+b_i') = 1$, $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$.
• Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$; "$f : \mathcal N \to \mathbb R^+$" means $f : 2^{\mathcal N} \to \mathbb R^+$; "$F(x) \triangleq \mathbb E[R(x)]$" means $\mathbb E[f(R(x))]$; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
• Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$, whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$-approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$, would not be this theorem.
• Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
• G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6), 2011, 1740–1766. https://doi.org/10.1137/080733991