The OR Formalization Drive

Motivation

The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form $P(x\mid s,B) = e^{v(s,x)}/\sum_{y\in B} e^{v(s,y)}$. Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.

That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" $v(s,x)$ shared by all alternative sets.

Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes $s$, the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.

Setting

Let $X$ be the universe of objects of choice and $S$ the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set $B\subseteq X$; a designated family of finite sets is the family of possible alternative sets. The selection probability $P(x\mid s,B)$ is the probability that an individual drawn at random from the population, with attributes $s$ and facing $B$, chooses $x\in B$. For every $s$ and possible $B$, $x\mapsto P(x\mid s,B)$ is a probability vector on $B$. Whenever $x\neq y$ belong to a possible set, the pair $\{x,y\}$ is possible too, so binary choices are defined.

• Axiom 1 (IIA). For all possible $B$, all $s$ and all $x,y\in B$: $P(x\mid s,\{x,y\})P(y\mid s,B) = P(y\mid s,\{x,y\})P(x\mid s,B)$.
• Axiom 2 (Positivity). $P(x\mid s,B)>0$ for all possible $B$, all $s$, all $x\in B$.
• Binary probabilities. $p_{xy}=P(x\mid s,\{x,y\})$ for $x\neq y$, and $p_{xx}=\tfrac12$ by definition.
• The function $V$. $V(s,x,z)=\log(p_{xz}/p_{zx})$.
• Universal benchmark. An alternative $z$ such that $B\cup\{z\}$ is possible whenever $B$ is.

In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.

Formalization targets

Goal: footnote 3 with Equation (12)

Under Axioms 1 and 2 and a universal benchmark $z$, with $v(s,x)=V(s,x,z)$, for every $s$, every possible $B$ (containing $z$ or not) and every $x\in B$:

$$P(x\mid s,B) = \frac{e^{v(s,x)}}{\sum_{y\in B} e^{v(s,y)}}.$$

The function $v$ is the same for all alternative sets; this is what distinguishes the goal from Equation (10).

Milestones, in the paper's order

1. Equation (5): for $x\neq y$ in $B$ with $P(x\mid s,B)>0$, Axiom 1 gives $P(x\mid s,\{x,y\})>0$ and $\dfrac{P(y\mid s,\{x,y\})}{P(x\mid s,\{x,y\})}=\dfrac{P(y\mid s,B)}{P(x\mid s,B)}$.
2. Equations (6)–(7): $P(y\mid s,B)=\dfrac{p_{yx}}{p_{xy}}P(x\mid s,B)$ and $1=\Big(\sum_{y\in B}\dfrac{p_{yx}}{p_{xy}}\Big)P(x\mid s,B)$.
3. Equation (8): $P(x\mid s,B)=1\big/\sum_{y\in B}(p_{yx}/p_{xy})$.
4. Equation (9): $\dfrac{p_{yx}}{p_{xy}}=\dfrac{p_{yz}/p_{zy}}{p_{xz}/p_{zx}}$ for $x,y,z$ in a possible set.
5. Equation (10): for a benchmark $z\in B$, $P(x\mid s,B)=e^{V(s,x,z)}\big/\sum_{y\in B}e^{V(s,y,z)}$.

Significance

The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification $v(s,x)=\theta'z(s,x)$ estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.

Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.

Difficulty

The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick $z\in B$ as benchmark" produces a function $V(s,x,z)$ that depends on the set through the choice of $z$. The goal requires a single $v$ for all sets, including sets that do not contain $z$, where neither Equation (10) nor the axioms on $B$ alone say anything about $z$. A second subtlety is the diagonal: $\{x,x\}=\{x\}$, so $p_{xx}$ is set to $\tfrac12$ by definition rather than read off a singleton choice.

Formalization scope

Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.

The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit $v(s,x)=V(s,x,z)$, never as "for each $B$ there is a $v$", which would only restate (10).

Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, New York, 1959. https://doi.org/10.1037/14396-000

Motivation

Set cover asks for the fewest sets from a family $\mathcal S$ of $m$ subsets of a ground set $X$ of $n$ elements whose union contains $X$. It is NP-hard, and the best ratio achievable in polynomial time is $\Theta(\log n)$ (Feige 1998, doi:10.1145/285055.285059).

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance $(X,\mathcal S)$ is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set $X'\subseteq X$ of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.

The question is how much an algorithm loses against an offline adversary who knows $X'$ and covers it with a family $\mathcal C_{OPT}$. This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor $O(\log m\log n)$ of $|\mathcal C_{OPT}|$. Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.

Setting

An instance consists of a finite ground set $X$ with $n=|X|$ elements and a finite family $\mathcal S$ of $m=|\mathcal S|$ sets. For an element $j$, $\mathcal S_j$ is the collection of sets containing $j$. Every set has cost $1$, so the cost of a family is its number of members.

The adversary gives a sequence $\sigma$ of elements (the given elements form $X'$). A family $\mathcal C_{OPT}\subseteq\mathcal S$ covers $\sigma$ if each element of $\sigma$ lies in some member of it.

The algorithm keeps a weight $w_S>0$ for every set, initially $w_S=1/(2m)$, and a cover $\mathcal C$, initially empty. The weight of an element is $w_j=\sum_{S\in\mathcal S_j}w_S$, and $C$ is the set of elements covered by members of $\mathcal C$. The potential is

$$\Phi=\sum_{j\notin C}n^{2w_j}.$$

When the adversary gives an element $j$:

1. if $w_j\ge1$, nothing changes;
2. otherwise a weight augmentation is performed: (a) $k$ is the minimal integer with $2^k w_j>1$; (b) every $S\in\mathcal S_j$ gets the weight $2^k w_S$; (c) at most $4\log n$ sets from $\mathcal S_j$ are added to $\mathcal C$, so that $\Phi$ does not exceed its value before the augmentation.

Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on $\sigma$ is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.

Formalization targets

Goal: Theorem 2.3

For $n\ge2$, every arrival sequence $\sigma$, and every family $\mathcal C_{OPT}$ covering $\sigma$: a run of the algorithm on $\sigma$ exists, and every run ends with a cover $\mathcal C$ that covers every element of $\sigma$ and satisfies

$$|\mathcal C|\;\le\;\lceil 4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2).$$

The paper states $|\mathcal C|=O(|\mathcal C_{OPT}|\log m\log n)$; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.

Milestones

Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most

$$|\mathcal C_{OPT}|\cdot(\log_2 m+2).$$

Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family $F\subseteq\mathcal S_j$ with $|F|\le\lceil4\ln n\rceil$ such that

$$\Phi_e\le\Phi_s,$$

where $\Phi_s$ is the potential before the iteration and $\Phi_e$ the potential after it, computed with the augmented weights and the cover $\mathcal C\cup F$.

Significance

The theorem shows that online set cover over a known instance admits a deterministic $O(\log m\log n)$-competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves $o\!\left(\frac{\log m\log n}{\log\log m+\log\log n}\right)$ over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.

The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.

Difficulty

The central step is Lemma 2.2: a family of at most $\lceil4\ln n\rceil$ sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of $\mathcal S_j$ can exceed the cardinality bound, since $\mathcal S_j$ may contain up to $m$ sets. Adding nothing, or a single set, can increase $\Phi$: every uncovered element sharing a set with $j$ has its weight raised, and its term $n^{2w}$ grows by a factor up to $n^{2\delta}$. The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of $n$.

The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs $n\ge2$ and a careful treatment of the initial potential, which is at most $n^2$ and equals $n^2$ when every element lies in every set.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight ($w_j$) and coveredBy ($j\in C$). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. $n=|E|$ and $m=|T|$. Weights are real numbers; $n^{2w_j}$ is the real power.

The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.

Explicit forms of the paper's asymptotic and unspecified quantities:

• the paper's "$4\log n$" sets per augmentation is $\lceil 4\ln n\rceil$ (natural logarithm, rounded up: the proof repeats a random choice that many times and needs $(1-\delta/2)^{4\log n}\le n^{-2\delta}$);
• Lemma 2.1's $\log m+2$ is $\log_2 m+2=\log_2(4m)$ (weights grow from $1/(2m)$ to at most $2$ by factors at least $2$);
• Theorem 2.3's $O(|\mathcal C_{OPT}|\log m\log n)$ is $\lceil4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2)$;
• $k$ ranges over natural numbers; for $w_j<1$ the minimal integer with $2^kw_j>1$ is one;
• the paper's remark "(Clearly, $2^k\cdot w_j<2$.)" is not encoded; the correct bound is $\le2$ ($w_j=1/2$ gives $k=2$) and is not a hypothesis anywhere.

The goal adds the hypothesis $n\ge2$, which the paper's $\log n$ assumes tacitly: for $n=1$ no set may be added and the element is never covered.

Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.

A complete development needs elementary real analysis (Real.rpow, Real.log, $1-x\le e^{-x}$), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• U. Feige, A Threshold of ln n for Approximating Set Cover, J. ACM 45(4):634–652, 1998. https://doi.org/10.1145/285055.285059
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

Motivation

In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.

The paper gives a deterministic online algorithm whose cost is within a factor $O(\log m \log n)$ of the offline optimum, where $n$ is the number of elements and $m$ the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of $m$ and $n$, every deterministic online algorithm has competitive ratio $\Omega\big(\log n \log m / (\log\log m + \log\log n)\big)$. The lower bound is the reason the $\log m \log n$ product, rather than the $\ln n$ of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.

This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.

Setting

A ground set $X$ and a family $\mathcal F$ of distinct subsets of $X$ are fixed and known to the algorithm; $m = |\mathcal F|$. An adversary presents elements $x_1, x_2, \dots$ of $X$ one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm $A$, on the arrival of $x_t$, sees the earlier arrivals $(x_1, \dots, x_{t-1})$ and $x_t$, and adds a finite family $A\big((x_1,\dots,x_{t-1}), x_t\big) \subseteq \mathcal F$ of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of $\mathcal F$, that element lies in a chosen set. After an arrival sequence $\sigma$ the chosen collection is $\mathcal C_A(\sigma)$, and since every set has unit cost, the cost is $|\mathcal C_A(\sigma)|$. The offline optimum $\mathrm{OPT}(\sigma)$ is the least number of members of $\mathcal F$ covering the elements of $\sigma$. The competitive ratio of $A$ is at least $\rho$ when some arrival sequence $\sigma$ has $\mathrm{OPT}(\sigma) \ge 1$ and $|\mathcal C_A(\sigma)| \ge \rho\,\mathrm{OPT}(\sigma)$.

Two families are used.

• The bit family: $X = \{0, \dots, 2^k - 1\}$ and $F_i = \{ j : \text{bit } i \text{ of } j \text{ is on}\}$ for $1 \le i \le k$.
• The block family: $k r^2$ disjoint blocks $X_1, \dots, X_{kr^2}$ of $2^k$ elements each; $X_b(t)$ is the set of elements of block $X_b$ whose $t$th bit is on. For an $r$-set $R = \{b_1 < \dots < b_r\}$ of blocks and bit locations $I = (i_1, \dots, i_r)$,

$$F_{R,I} = \bigcup_{t=1}^r X_{b_t}(i_t),$$

and the family consists of all $F_{R,I}$; it has $m = \binom{kr^2}{r} k^r$ members.

Formalization targets

Goal: Proposition 4.2

For all positive integers $k, r$ and all $n, m$ with

$$n \ge 2^{k+1} k r^2, \qquad 2^{2^k k r^2} \ge m \ge \binom{kr^2}{r} k^r,$$

there is a family $\mathcal F$ of exactly $m$ distinct subsets of an $n$-element set such that for every valid deterministic online algorithm $A$ there is a nonempty arrival sequence $\sigma$, covered by a single member of $\mathcal F$, with

$$|\mathcal C_A(\sigma)| \ge kr = kr \cdot \mathrm{OPT}(\sigma).$$

The goal leaves the instance existential, as the paper does, and keeps both bounds on $m$ and the bound on $n$ exactly as printed.

Milestones

1. Proposition 4.1. On the bit family, $|\mathcal F| = k$; every valid deterministic algorithm can be forced to cost $k$ on a sequence with $\mathrm{OPT} = 1$; and some valid algorithm has cost at most $k \cdot |C|$ for every offline cover $C$. So the best deterministic competitive ratio is exactly $k = \log_2 n$.
2. The adversary claim of Section 4 (p. 369). On the block family, every valid deterministic algorithm can be forced to choose $kr$ sets by at most $kr$ arrivals that a single set covers.

A supporting item (not a milestone) records the count $|\mathcal F| = \binom{kr^2}{r} k^r$ of the block family.

Significance

The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing $r$ of order $\log m / (\log\log m + \log\log n)$ and $k$ of order $\log n$ turns it into the asymptotic bound $\Omega\big(\log n \log m/(\log\log m + \log\log n)\big)$, which shows that the paper's $O(\log m \log n)$ algorithm is optimal among deterministic algorithms up to a $\log\log m + \log\log n$ factor. Without it, the gap between the $\ln n$ achievable offline and the $\log m \log n$ achieved online would be unexplained. Proposition 4.1 alone gives the matching bound $\log_2 n$ when $m = \log_2 n$.

Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.

Difficulty

The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only $k$ sets. To force $kr$ sets with $\mathrm{OPT} = 1$, the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most $1 + (r-1)k$ blocks after $k$ steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly $n$ elements and exactly $m$ distinct sets without creating sets that help cover the adversary's elements.

Formalization scope

The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit $i$ (1-based) of $j$ is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).

The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set ($\mathrm{OPT} = 1$), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies $\text{cost} \ge kr \cdot \mathrm{OPT}$ as $0 \ge 0$.

The statements contain no $O(\cdot)$: every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of $r$ and $k$, is excluded, as are the remarks on the trivial ratio-$m$ and $O(\sqrt n)$ algorithms.

Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The online set cover problem, Proc. 35th ACM STOC, 2003, pp. 100–105. https://doi.org/10.1145/780542.780558
• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4):634–652, 1998. https://doi.org/10.1145/285055.285059
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

Motivation

Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).

The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio $O(\log m \log n)$, where $n$ is the number of elements and $m$ the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).

This mission formalizes the core of the weighted result: the algorithm that is given a value $\alpha$ at least the optimal cost, and its guarantee (Theorem 3.4).

Setting

The ground set $X$ has $n = |X|$ elements and the family $\mathcal S$ has $m = |\mathcal S|$ sets; every set $S$ has a cost $c_S > 0$. Both are known to the algorithm in advance. For an element $j$, $\mathcal S_j$ denotes the sets containing $j$. Elements of an unknown subset of $X$ arrive one at a time in a sequence $\sigma$; on arrival each must be covered by a chosen set. The chosen family $\mathcal C$ can only grow. $\mathcal C_{OPT}$ is any family covering every arriving element, and $c(\mathcal C_{OPT}) = \sum_{S \in \mathcal C_{OPT}} c_S$.

The algorithm is given $\alpha \ge c(\mathcal C_{OPT})$. It discards sets costing more than $\alpha$, buys sets costing at most $\alpha/m$ outright, and rescales costs; on the resulting normalized instance $1 \le c_S \le m$ and $c_S \le \alpha$ for every set (p. 365).

The algorithm keeps a weight $w_S > 0$ for every set, initially $w_S = 1/m^2$; the weight of an element is $w_j = \sum_{S \in \mathcal S_j} w_S$. With $C$ the set of covered elements and $\chi_{\mathcal C}$ the indicator of $\mathcal C$, the potential is

$$\Phi = \sum_{j \notin C} n^{2 w_j} + n \cdot \exp\Big(\frac{1}{2\alpha} \sum_{S \in \mathcal S} \big(c_S \chi_{\mathcal C}(S) - 3 w_S c_S \log n\big)\Big),$$

with natural logarithms throughout. When $j$ arrives with $w_j \ge 1$ nothing happens; otherwise the algorithm performs weight augmentation steps while $w_j < 1$. In a step, for each $S \in \mathcal S_j$: (a) $w_S \leftarrow w_S (1 + \frac{1}{n c_S})$; (b) if $S \notin \mathcal C$, add $S$ to $\mathcal C$ when $\Phi$ does not exceed its value before (a); (c) if $\Phi$ has increased, return FAIL.

In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.

Formalization targets

Goal: Theorem 3.4

On the normalized instance, with $\mathcal C_{OPT}$ covering $\sigma$, $c(\mathcal C_{OPT}) \le \alpha$, and $n \cdot n^{2/m} + n < n^2$, every reachable configuration is a running state (never FAIL) in which (i) every $j \in X$ with $w_j \ge 1$ is covered, and (ii)

$$\sum_{S \in \mathcal C} c_S \le 3 \log n \Big(1 + \Big(1 + \frac1n\Big)\alpha \log\Big(m^2\Big(1+\frac1n\Big)\Big)\Big) + 2\alpha \log n = (6 + o(1))\,\alpha \log m \log n.$$

Milestones

• Lemma 3.1 (p. 365): the number $N$ of augmentation steps satisfies $N \le \sum_{S \in \mathcal C_{OPT}} (n c_S + 1)\log(m^2(1 + 1/n)) \le (n+1)\alpha\log(m^2(1+1/n))$.
• Lemma 3.2 (p. 366): throughout, $\sum_S w_S c_S \le 1 + N/n \le 1 + (1 + 1/n)\alpha\log(m^2(1+1/n))$.
• Lemma 3.3 (p. 366): a per-set step with $c_S \le \alpha$ never increases $\Phi$; in particular the algorithm never fails.

The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant $\Phi < n^2$ assumed) is included as a supporting reference.

Significance

Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of $\alpha$ described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic $O(\log m \log n)$-competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.

The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant $\Phi < n^2$ to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis $c_S \le \alpha$. Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the $o(1)$ terms replaced by explicit expressions.

Difficulty

The cost bound in the last step is short once two facts about the run are available: that $\Phi$ stays below $n^2$, and that the fractional cost $\sum_S w_S c_S$ stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add $S$ or not) does not increase $\Phi$; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most $\alpha$. The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers $n^{2 w_j}$, where the initial bound $\Phi < n^2$ is a genuine size condition on $n$ and $m$.

Formalization scope

The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits $\mathcal S_j$ is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by $\mathcal C_{OPT}$.

Conventions: costs, weights and $\alpha$ are real; $n$ and $m$ are the cardinalities of the finite types cast to $\mathbb R$; $\log$ is Real.log; $n^{2 w_j}$ and $n^{2/m}$ are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:

• Lemma 3.1: $(2 + o(1)) n\alpha\log m$ becomes $(n+1)\alpha\log(m^2(1+1/n))$;
• Lemma 3.2: $(2 + o(1))\alpha\log m$ becomes $1 + (1+1/n)\alpha\log(m^2(1+1/n))$, together with the intermediate bound $1 + N/n$;
• Theorem 3.4 (ii): $(6 + o(1))\alpha\log m\log n$ becomes $3\log n\,(1 + (1+1/n)\alpha\log(m^2(1+1/n))) + 2\alpha\log n$;
• "n and m large" becomes the hypothesis $n \cdot n^{2/m} + n < n^2$ used for the initial potential (it holds, for instance, when $n \ge 4$ and $m \ge 3$).

The goal is a statement about the configurations the algorithm actually reaches from $w_S = 1/m^2$ and the empty cover. Taking the invariant $\Phi < n^2$ or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown $\alpha$ is not part of this mission.

A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

Motivation

When many self-interested users share resources whose cost grows with use (links of a network, servers, machines), each user picks the option that is cheapest for them given what the others do, and the resulting equilibrium can be worse for the group than a centrally planned allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures this loss as the worst ratio between the social cost of an equilibrium and the optimal social cost. Congestion games (Rosenthal 1973) are the standard finite model of such resource sharing: they always have pure Nash equilibria, and they cover atomic routing, load balancing and many network design questions.

Timeline of the linear-latency case:

• 2002: Roughgarden and Tardos (J. ACM) bound the price of anarchy of nonatomic selfish routing with linear latencies by $4/3$.
• 2005: Awerbuch, Azar and Epstein (STOC 2005) and, independently, Christodoulou and Koutsoupias (STOC 2005) show that for atomic (finite) congestion games with linear latencies the pure price of anarchy of the total cost is $5/2$. Awerbuch, Azar and Epstein also obtain $(3+\sqrt5)/2 \approx 2.618$ for weighted players.
• 2005: Christodoulou and Koutsoupias observe that their argument for $5/2$ extends to mixed Nash equilibria, at the price of the larger constant $(3+\sqrt5)/2$ (their Theorem 14, the goal of this mission).

Setting

A congestion game consists of a finite set $N$ of players, a finite set $E$ of facilities, for each player $i$ a collection $\Sigma_i$ of pure strategies, each a subset of $E$, and for each facility $e$ a latency function $f_e : \mathbb N \to \mathbb R$. In a pure profile $A = (A_1, \dots, A_n)$, $A_i \in \Sigma_i$, the load $n_e(A)$ is the number of players whose set contains $e$, and player $i$ pays

$$c_i(A) = \sum_{e \in A_i} f_e\bigl(n_e(A)\bigr).$$

The social cost of a pure profile is $\mathrm{SUM}(A) = \sum_{i\in N} c_i(A)$ ($N$ times the average cost). Latencies are linear: $f_e(k) = a_e k + b_e$ with $a_e, b_e \ge 0$.

A mixed strategy $p_i$ of player $i$ is a probability distribution on $\Sigma_i$. The players randomize independently, so the pure profile $s$ occurs with probability $\Pr(s) = \prod_j p_j(s_j)$. Player $i$'s expected cost is $\mathbb E[c_i] = \sum_s \Pr(s)\, c_i(s)$, and the expected load of $e$ is $\mathbb E[n_e] = \sum_s \Pr(s)\, n_e(s)$. A mixed profile is a mixed Nash equilibrium if no player can lower their expected cost by switching unilaterally to another distribution on their strategies. The social cost of a mixed profile is the sum of the expected costs, $\mathrm{SUM}(p) = \sum_i \mathbb E[c_i]$.

In Lean: CongestionGame ι E with fields strategies and latency, load, cost, IsProfile, sumCost, IsLinear, expCost, expLoad, mixedSumCost and IsMixedNash, all in the namespace CongestionPoA.Mixed; lotteries and independent randomization come from the platform definition agt_games (AGT.IsLottery, AGT.profileProb, AGT.IsMixedNash).

Formalization targets

Goal: Theorem 14

For every congestion game with linear latencies, every mixed Nash equilibrium $p$ and every pure profile $P$ with $P_i \in \Sigma_i$,

$$\sum_{i\in N} \mathbb E[c_i] \;\le\; \frac{3+\sqrt5}{2}\,\mathrm{SUM}(P).$$

Taking $P$ optimal, the mixed price of anarchy of the average social cost is at most $(3+\sqrt5)/2$.

Milestones

1. Lemma 3 (corrected). For real $x \ge 0$ and integer $y \ge 0$, $y(x+1) \le \frac{\sqrt5-1}{4}x^2 + \frac{\sqrt5+5}{4}y^2$.
2. Deviation inequality (Theorem 1's proof, mixed). At a mixed Nash equilibrium, for every player $i$,

$$\mathbb E[c_i] \le \sum_{e\in P_i}\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).$$

3. Summing step (Theorem 1's proof, mixed).

$$\sum_i \mathbb E[c_i] \le \sum_{e\in E} n_e(P)\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).$$

Significance

The bound says that randomization by the players cannot make linear congestion games much worse than pure play: the loss stays within a constant factor independent of the number of players and facilities. Mixed equilibria matter because they always exist in every finite game and because they model populations of users whose individual choices are not known in advance. The same authors report (PDF p. 2) extending these bounds to correlated equilibria with the same values, which places the mixed bound in a hierarchy of equilibrium notions whose worst cases coincide.

The result is proved in the paper, in one sentence that defers to the proof of Theorem 1. The work here is a complete machine-checked version: the expected-cost layer for congestion games on top of agt_games, the deviation and summing inequalities under product distributions, and the corrected Lemma 3. The paper prints Lemma 3 for all nonnegative reals $x, y$, where it is false (at $x = 0$, $y = 1/10$ the left side is $0.1$ and the right side about $0.018$); the formal statement keeps $y$ an integer, which is how the lemma is used. No formalization of congestion-game price-of-anarchy bounds was on the platform when this mission was drafted.

Difficulty

The pure proof compares $n_e(P)(n_e(A)+1)$ with $n_e(A)^2$ and $n_e(P)^2$ through an integer inequality (Lemma 1). Under a mixed equilibrium the equilibrium side is an expectation, so the cost of a facility is no longer a function of one integer load, and Lemma 1's constant $1/3$ is not available for real arguments: a real-variable version is needed, and the constant degrades from $5/2$ to $(3+\sqrt5)/2$. A second obstacle is bookkeeping: the deviating player's load changes only on their own deviation, while the other players' randomization stays independent, and the expected cost of a player has to be related to expected facility loads, which uses linearity of the latencies in an essential way. The naive idea of applying Theorem 1 to each pure profile in the support of the equilibrium fails, because those profiles are not themselves Nash equilibria.

Formalization scope

Players and facilities are finite types ι and E; profiles are functions ι → Finset E, with feasibility IsProfile a separate predicate. Latencies are real-valued on natural-number loads, and "linear" means affine with nonnegative coefficients, $f_e(k) = a_e k + b_e$; the paper displays only the identity latency $f_e(k)=k$ and states that its proofs extend. Mixed strategies are real weight functions on the finite strategy type $\Sigma_i$; independence is built into AGT.profileProb; Nash deviations range over all lotteries, which is equivalent to pure deviations. agt_games maximizes payoffs, so the game is passed to it with payoff $-c_i$. The goal is stated against every feasible pure profile rather than as a ratio, so no division by an optimum that may be $0$ occurs. The social cost is the expected sum of the players' costs; the paper's second option, $\sum_e \mathbb E[n_e^2]$, is not part of this mission. A version with correlated distributions on profiles, or one that bounds the cost of an "averaged" profile instead of the expected cost, is a different statement and does not discharge the goal.

A complete development needs elementary finite-sum manipulation of product distributions (marginals of AGT.profileProb, expectations of loads), and a Jensen-type inequality $(\mathbb E[n_e])^2 \le \mathbb E[n_e^2]$ for finite distributions. The expectation lemmas for congestion games are reusable for the other mixed results of the literature (weighted games, polynomial latencies). Proofs of the milestones, of the expectation layer, and alternative arguments are all welcome.

Selected references

• G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, STOC 2005, pp. 67–73. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, STOC 2005, pp. 57–66. https://doi.org/10.1145/1060590.1060599
• E. Koutsoupias, C. Papadimitriou, Worst-case Equilibria, STACS 1999, LNCS 1563, pp. 404–413. https://doi.org/10.1007/3-540-49116-3_38
• R. W. Rosenthal, A Class of Games Possessing Pure-Strategy Nash Equilibria, International Journal of Game Theory 2 (1973), pp. 65–67. https://doi.org/10.1007/BF01737559
• T. Roughgarden, É. Tardos, How Bad Is Selfish Routing?, Journal of the ACM 49 (2002), pp. 236–259. https://doi.org/10.1145/506147.506153

Motivation

A group of $m$ individuals each hold a subjective probability distribution over the same $n$ outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.

The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.

The variational problem the paper introduces, maximizing $\sum_i b_i \log(\text{utility}_i)$, is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.

Setting

There are $m$ bettors $B_1,\dots,B_m$ and $n$ horses $H_1,\dots,H_n$.

• The subjective probability matrix $P=(p_{ij})$ is $m\times n$; $p_{ij}$ is the probability, in the opinion of $B_i$, that $H_j$ wins. Each row is a probability distribution: $p_{ij}\ge 0$ and $\sum_j p_{ij}=1$.
• Bettor $B_i$ has a budget $b_i>0$, with the unit of money chosen so that $\sum_i b_i=1$.
• Each column of $P$ contains at least one positive entry (a horse nobody believes in can be removed).

Unknowns are Greek. $\pi_j$ is the track probability of $H_j$ and $\beta_{ij}$ is the amount $B_i$ bets on $H_j$. Nonnegative $\pi_j,\beta_{ij}$ are equilibrium probabilities and bets when

$$\text{(1)}\ \sum_{j=1}^n\beta_{ij}=b_i,\qquad \text{(2)}\ \sum_{i=1}^m\beta_{ij}=\pi_j,\qquad \text{(3)}\ \text{if } \mu_i=\max_s\frac{p_{is}}{\pi_s}\text{ and }\beta_{ij}>0,\text{ then }\mu_i=\frac{p_{ij}}{\pi_j}.$$

(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation $p_{ij}/\pi_j$.

The paper's variational problem is

$$\varphi(\xi)=\sum_{i=1}^m b_i\log\sum_{j=1}^n p_{ij}\xi_{ij}\quad\text{on}\quad D=\Big\{\xi:\ \xi_{ij}\ge0,\ \sum_{i=1}^m\xi_{ij}=1\ \text{for all } j\Big\},$$

with $\varphi=-\infty$ where an inner sum vanishes. From a maximizer $\bar\xi$ it builds $\pi_j=\max_i b_ip_{ij}/\sum_s p_{is}\bar\xi_{is}$ (6) and $\beta_{ij}=\bar\xi_{ij}\pi_j$ (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and $\varphi$, $D$, the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

$$\exists!\,\pi\in\mathbb R^n\ \ \exists\,\beta\in\mathbb R^{m\times n}:\ (\pi,\beta)\ \text{are equilibrium probabilities and bets}.$$

Only $\pi$ is unique; the paper notes that equilibrium bets need not be.

Milestones

1. $\varphi$ attains its maximum on $D$ at a point with every inner sum positive (p. 167).
2. $\partial\varphi/\partial\xi_{ij}=b_ip_{ij}/\sum_s p_{is}\xi_{is}$ wherever the inner sums are positive (p. 167).
3. (8): at a maximizer, $\bar\xi_{ij}>0$ implies $\pi_j=\partial\varphi/\partial\bar\xi_{ij}$ (p. 167).
4. Every $\pi_j$ of (6) is positive (p. 167).
5. EXISTENCE THEOREM: for every maximizer $\bar\xi$, (6)–(7) are equilibrium probabilities and bets (p. 167).
6. Every equilibrium has $\pi_j>0$ (p. 168).
7. For two equilibria, $\sum_k\bar\pi_k\bar\pi_k/\pi_k\le 1$ (p. 168).
8. If $\pi>0$, $\bar\pi\ge0$, both sum to 1 and $\sum_k\bar\pi_k^2/\pi_k\le1$, then $\bar\pi=\pi$ (p. 168).
9. UNIQUENESS THEOREM: equilibrium probabilities are unique (p. 168).

A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is $(\tfrac12,\tfrac12)$, the equilibrium probabilities are $(\tfrac12,\tfrac12)$ whatever the second bettor believes.

Significance

The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.

The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of $\log 0=-\infty$, and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.

Difficulty

The existence statement, as the paper proves it, has two delicate points. $\varphi$ is $-\infty$ on part of the boundary of $D$, so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.

For uniqueness, the natural first idea, strict concavity of $\varphi$, fails: $\varphi$ is concave but not strictly concave in $\xi$, and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all $\pi_j$, which the paper uses without proof.

Formalization scope

• Bettors are Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of $P$ are probability vectors, no zero column, $b_i>0$, $\sum_i b_i=1$) is a field of Market; $m\ge1$ follows from $\sum_ib_i=1$.
• Condition (3) is written multiplied out: $\beta_{ij}>0\Rightarrow p_{is}\pi_j\le p_{ij}\pi_s$ for all $s$. This equals (3) when $\pi>0$ and encodes the paper's $p/0=+\infty$ when some $\pi_s=0$. Positivity of $\pi$ is not part of the definition of equilibrium; it is milestone 6.
• $D$ has column sums one, as in (5).
• $\varphi$ is real-valued. A maximizer is a point of $D$ with positive inner sums that dominates every point of $D$ with positive inner sums; the excluded points have $\varphi=-\infty$ on the page. The max in (6) is Finset.sup' over the nonempty set of bettors.
• Ruled out: a version of (3) with real division ($x/0=0$) admits spurious equilibria with $\pi_s=0$ and makes uniqueness false; a maximizer defined with the raw real $\varphi$ ($\log0=0$) changes the set of maximizers; adding $\pi>0$ or $\sum_j\pi_j=1$ to the equilibrium definition weakens the goal.
• Needed infrastructure: compactness of $D$ and an argument handling the $-\infty$ boundary, one-variable derivatives of $\log$ of linear forms, and the equality case of the Cauchy–Schwarz inequality. Milestones 7–9 use no analysis and can be attacked independently of 1–5. Proofs of any milestone, and reusable lemmas on the Eisenberg–Gale program, are welcome.

Selected references

• E. Eisenberg and D. Gale, Consensus of subjective probabilities: the pari-mutuel method, The Annals of Mathematical Statistics 30(1):165–168, 1959. https://doi.org/10.1214/aoms/1177706369
• V. V. Vazirani and M. Yannakakis, Market equilibrium under separable, piecewise-linear, concave utilities, Journal of the ACM 58(3), 2011. https://doi.org/10.1145/1970392.1970394

Motivation

A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor $\beta$ tends to $1$ the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats $\beta = 1$ as a limit of $\beta < 1$: it expands the discounted return of a stationary policy in powers of $1-\beta$ and reads off which policies remain good as $\beta \to 1$. The two leading coefficients of that expansion, the gain $x(f)$ and the bias $y(f)$, became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).

Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all $\beta$ near $1$ (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through $x$ and $y$. Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders ($n$-discount optimality).

Setting

There are finitely many states $s \in S$ and a finite nonempty set $A$ of actions. Action $a$ in state $s$ pays an income $i(s,a) \in \mathbb R$ and moves the system to $s'$ with probability $q(s' \mid s,a)$. $F$ is the finite set of decision rules $f : S \to A$. A policy is a sequence $\pi = \{f_1, f_2, \dots\}$ of decision rules; $f^{(\infty)}$ uses $f$ every day, and $(g, \pi)$ uses $g$ first and then $\pi$. For $f \in F$, $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s' \mid s,f(s)))_{s,s'}$. The discounted return of $\pi$ is the vector

$$V_\beta(\pi) = \sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\, r(f_{n+1}), \qquad 0 \le \beta < 1,$$

and $V_\beta(f)$ abbreviates $V_\beta(f^{(\infty)})$. Vectors are compared coordinatewise; $w_1 > w_2$ means $w_1 \ge w_2$ and $w_1 \neq w_2$. A policy is β-optimal if its return dominates that of every policy, and $U(\beta)$ is the return of a β-optimal policy. It is optimal if it is β-optimal for all $\beta$ sufficiently near $1$, and nearly optimal if $U(\beta) - V_\beta(\pi) \to 0$ as $\beta \to 1$.

For any Markov matrix $Q$, the limit matrix $Q^*$ is the limit of $(I + Q + \cdots + Q^N)/(N+1)$, and the deviation matrix is $H = (I - Q + Q^*)^{-1} - Q^*$. For a rule $f$, $Q^*(f)$ and $H(f)$ are those of $Q(f)$, and

$$x(f) = Q^*(f)\, r(f), \qquad y(f) = H(f)\, r(f).$$

With $p(s,a)w = \sum_{s'} q(s' \mid s,a) w_{s'}$, the set $G(s,f)$ consists of the actions $a$ with $p(s,a)x(f) > x_s(f)$, or with $p(s,a)x(f) = x_s(f)$ and $i(s,a) + p(s,a)y(f) > x_s(f) + y_s(f)$; $E(s,f)$ consists of those with equality in both.

Formalization targets

Goal: Theorem 4(e)

For any $f_0$ with $G(s,f_0) = \varnothing$ for all $s$:

$$x(f_0) \ge x(g)\ \ \forall g \in F;\qquad \exists f^* \in F^* := \{g : x(g) = x(f_0)\}\ \text{with}\ y(f^*) \ge y(g)\ \forall g \in F^*;$$ $$g^{(\infty)} \text{ is nearly optimal} \iff x(g) = x(f^*) \text{ and } y(g) = y(f^*).$$

Milestones and intermediate results

Milestones: Lemma 1(b) ($\operatorname{rank}(I-Q) + \operatorname{rank} Q^* = S$), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).

The mission also states, as intermediate results:

• Lemma 1(a), (c), (d): for every Markov matrix, convergence of the Cesàro means to a Markov $Q^*$ with $QQ^* = Q^*Q = Q^*Q^* = Q^*$; unique solvability of $Qx = x$, $Q^*x = Q^*c$; nonsingularity of $I - Q + Q^*$, $\sum_n \beta^n (Q^n - Q^*) \to H$ and the identities for $H$.
• Theorem 4(a): $V_\beta(f) = x(f)/(1-\beta) + y(f) + o(1)$, with $x(f), y(f)$ the unique solutions of their linear systems; display (2), the same expansion for $(g, f^{(\infty)})$.
• Theorem 3 and its Corollary for fixed $\beta < 1$, and the first assertion of 4(e).

Significance

Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income $x$, then of the bias $y$. It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.

The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.

Difficulty

Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where $Q^n$ does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single $f^*$ whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through $U(\beta)$.

Formalization scope

States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's $f_1$. $V_\beta$ is a real tsum. $Q^*$ is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; $H(\beta)$ is a matrix tsum, whose summability for $0 \le \beta < 1$ is part of Lemma 1(d); $H$ uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). $x(f)$ and $y(f)$ are defined by the closed forms $Q^*(f)r(f)$ and $H(f)r(f)$ from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along $\beta \to 1^-$. "Nearly optimal" is encoded without $U$: for every $\varepsilon > 0$, for all β in some interval $(\beta_0, 1)$, every policy's return is at most $V_\beta(\pi) + \varepsilon$ in every coordinate; this is equivalent to $U(\beta) - V_\beta(\pi) \to 0$ because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set $G(s,f)$.

A formalization in which optimality or near optimality is tested only against stationary policies, or in which $Q^*$ is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.

Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• B. L. Miller and A. F. Veinott, Discrete Dynamic Programming with a Small Interest Rate, Ann. Math. Statist. 40(2):366–370, 1969.
• A. F. Veinott, Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887