All missions

Motivation

In a strategic game, players may repeatedly change their own choices when a change raises their payoff. This gives a simple model of decentralized adjustment: each move uses the current profile and one player's immediate incentive. The central question is whether such adjustment can continue forever. Monderer and Shapley introduced the finite improvement property (FIP) to state that every sequence of strict unilateral improvements ends. Their 1996 paper, pp. 128–130, relates that dynamic property to a real-valued function on the game's strategy profiles.

An ordinal potential records each player's strict preference between two of their strategies when the other players' strategies are fixed. Such a function is useful because it assigns one common direction to the players' individual choices. The paper gives a two-player game $G_1$ that has the FIP but no ordinal potential, then introduces a weaker, generalized ordinal potential and proves that it captures exactly the finite games with the FIP (Monderer and Shapley, pp. 129–130). This mission isolates that characterization from the paper's other results about exact potentials and congestion games.

Setting

Let $N$ be a finite set of players. Player $i\in N$ has a strategy set $Y^i$, and a strategy profile $y\in Y=\prod_{i\in N}Y^i$ selects one strategy for each player. The payoff function $u^i:Y\to\mathbb R$ gives player $i$'s payoff at a profile. Write $(y^{-i},x)$ for the profile obtained by replacing player $i$'s strategy in $y$ by $x\in Y^i$. A finite game has finite $Y^i$ for every player. These are the paper's conventions at the start of §2 (p. 127).

A path is a sequence of profiles in which each step changes exactly one player's strategy to a different strategy. It is an improvement path when the moving player strictly increases their payoff at every step. The game has the FIP if no infinite improvement path exists. Thus the property concerns paths of any length and every allowed choice of deviator, rather than the behavior of one selected update rule (p. 128).

An ordinal potential $P:Y\to\mathbb R$ satisfies

$$u^i(y^{-i},x)>u^i(y^{-i},z)\quad\Longleftrightarrow\quad P(y^{-i},x)>P(y^{-i},z)$$

for every player $i$, opponents' profile $y^{-i}$, and $x,z\in Y^i$. A generalized ordinal potential replaces this equivalence by the forward implication only. The two notions are distinct, as the game $G_1$ on p. 129 shows (equations (2.1) and (2.3), pp. 127, 129).

Formalization targets

Goal: Lemma 2.5

For every finite game $\Gamma$,

$$\Gamma\text{ has the FIP}\quad\Longleftrightarrow\quad \Gamma\text{ admits a generalized ordinal potential}.$$

This is Lemma 2.5, p. 129. It specifies a precise characterization rather than choosing a particular potential or a particular update schedule.

Supporting statements

The milestone list follows the paper's statements: Lemma 2.3 says a finite ordinal potential game has the FIP; the proof of Lemma 2.5 says the finite-improvement reachability relation is transitive under the FIP; and it concludes that the whole strategy-profile set can be represented by a real function increasing along that relation (pp. 128–130). Corollary 2.6 and the explicit game $G_1$ record the boundary between ordinal and generalized ordinal potentials: under its distinct-payoff condition a finite game with the FIP has an ordinal potential, while $G_1$ shows that condition cannot simply be omitted (pp. 129–130). Lemma 2.1 and Corollary 2.2 concern equilibria: an ordinal potential game has the same pure equilibria as the game in which every player receives the potential, so a maximizer of the potential is an equilibrium, and every finite ordinal potential game has a pure-strategy equilibrium (p. 128).

Significance

The goal connects a property of all possible strict improvement paths to the existence of a single real-valued certificate on profiles. In a finite game, such a certificate describes a common direction for unilateral payoff gains, regardless of which improving player moves next. The distinction between ordinary and generalized ordinal potentials matters: an ordinary potential must also preserve indifference, whereas the FIP alone does not require that (Monderer and Shapley, p. 129).

The characterization is proved in the paper; the remaining work in this mission is a Lean proof of its faithful finite-game statement. The local platform index used for this proposal has no published theorem expressing this characterization. The definitions of improvement paths and improvement reachability can also support other formal results about game dynamics. The game $G_1$ serves as a concrete check on the strict distinction between the two potential notions.

Difficulty

The payoff vector itself does not give an immediate numerical order on whole profiles: each step compares one player's payoff, and the next step may involve another player. Finiteness rules out an endlessly increasing sequence only after a suitable profile-level ordering has been established. The converse direction therefore requires more than observing that each individual move helps its deviator. The paper's $G_1$ also rules out replacing the generalized potential in the goal with an ordinary ordinal one (p. 129).

Formalization scope

Players form a finite Lean type ι with decidable equality; each player's strategies form a type Y i. A theorem about a finite game additionally assumes every Y i is finite. These types may be empty: in that case there is no strategy profile, and the corresponding FIP and potential statements retain their ordinary quantified meaning. No nonemptiness assumption is inserted into Lemma 2.5. Corollary 2.2 alone assumes every strategy set nonempty, which the page takes for granted: without it there is no profile and no equilibrium. An equilibrium point is a pure Nash equilibrium in the sense of the published definition AGT.IsPureNash (no player gains strictly by a unilateral deviation), and "P admits a maximal value in Y" in Lemma 2.1 is read as "P attains its maximum on Y". The finite player assumption follows the standing convention on p. 127; the finite strategy assumption is added only where the source says “finite game.”

The expression $(y^{-i},x)$ is Function.update y i x. IsStep requires one coordinate to change to a different value. HasFIP forbids an infinite natural-number-indexed path of strict payoff improvements, so it cannot be satisfied merely because each separately described finite path has finite length. A finite path stores its deviator at each step; the genuine-step condition determines that deviator uniquely. The same path bundle contains the paper's path sum and closed-path predicates for consistency across this paper's missions, although only finite improvement paths are used here. The relation ImprovesTo u x y means that a finite strict improvement path leads from $y$ to a distinct $x$.

The necessary development comprises the two potential predicates, path and FIP definitions, the finite improvement relation, the transitivity and representation milestones, and the goal characterization. Contributions that prove these statements or simplify their proof dependencies are within scope. A definition that checks only finite paths, allows null steps, or confuses the one-way condition (2.3) with the two-way condition (2.1) would change the result.

Selected references

• Dov Monderer and Lloyd S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143, doi:10.1006/game.1996.0044.

Motivation

In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper first studies binary predictions and then allows real predictions and labels in the unit interval. The continuous version matters when the distance between a prediction and a label carries information that a binary mistake count discards. The formal target here is the paper's total absolute-loss guarantee for that continuous master, WMC (Littlestone and Warmuth 1994, §5).

The result is part of the paper's generalized analysis, which also covers a binary master WMG and a randomized master WMR. These algorithms share a range of allowed weight updates, but their predictions and losses differ. This mission isolates WMC's deterministic, continuous-label theorem and the numbered lemmas on which its statement rests. The finite-sequence convention is explicit in the paper's notations and assumptions (Littlestone and Warmuth 1994, p. 220).

Setting

Fix a finite nonempty pool of $n$ forecasters and a finite sequence of $t$ trials. At trial $j$, expert $i$ predicts $x_i^{(j)}\in[0,1]$, and after the master predicts, a label $\rho^{(j)}\in[0,1]$ is revealed. Expert $i$ has weight $w_i^{(j)}$ before that trial. Every initial weight is positive, and weights remain nonnegative. The total weight and weighted mean prediction are

$$s^{(j)}=\sum_{i=1}^{n}w_i^{(j)},\qquad \gamma^{(j)}=\frac{\sum_{i=1}^{n}w_i^{(j)}x_i^{(j)}}{s^{(j)}}.$$

WMC predicts $\gamma^{(j)}$. Its loss on the trial is the absolute error $|\gamma^{(j)}-\rho^{(j)}|$, and its total absolute loss is $m=\sum_{j=1}^{t}|\gamma^{(j)}-\rho^{(j)}|$. Write $w_{\mathrm{init}}=s^{(1)}$ and $w_{\mathrm{fin}}=s^{(t+1)}$ for total weight before the first and after the final update (Littlestone and Warmuth 1994, pp. 232–233).

WMC updates on every trial. For $0\le\beta<1$, it multiplies each weight by a factor $F_i^{(j)}$ in the interval

$$\beta^{|x_i^{(j)}-\rho^{(j)}|}\le F_i^{(j)}\le 1-(1-\beta)|x_i^{(j)}-\rho^{(j)}|, \qquad w_i^{(j+1)}=F_i^{(j)}w_i^{(j)}.$$

The factor may depend on both trial and expert. The paper permits any choice in this interval, so WMC denotes a class of runs rather than one fixed recurrence. Its convention $0^0=1$ is used when $\beta=0$ and an expert has zero error (Littlestone and Warmuth 1994, p. 233, eq. (5.1)).

Formalization targets

Theorem 5.2: WMC total loss

For every run with positive final total weight, the target is the paper's explicit inequality

$$m\le\frac{\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})}{1-\beta}.$$

The bound uses the run's actual initial and final weights, so it applies whether the upper or lower permitted update factor was selected, or a factor between them. The finite-valued statement assumes $w_{\mathrm{fin}}>0$; the paper regards the bound as vacuous when the denominator of the logarithm is zero (Littlestone and Warmuth 1994, p. 236, Theorem 5.2).

Supporting numbered results

Lemma 5.1 states $\beta^r\le1+r(\beta-1)$ for $\beta\ge0$ and $0\le r\le1$, ensuring the update interval is nonempty. Lemma 5.2 states the logarithmic potential estimate under only the update's upper inequality, including the special case in which $\beta=0$ and a master's unit loss forces the final total weight to zero. Lemma 5.3 turns those same conditions into the displayed total-loss bound. Each is a separate milestone with the paper's statement and page provenance (Littlestone and Warmuth 1994, pp. 233–236).

Significance

The theorem controls the master's accumulated real-valued prediction error by an observable change in the total pool weight. It requires no distributional assumption on the trial sequence and no single choice of update factor. That breadth lets the same estimate be used for different update rules within the allowed range, while the explicit $1/(1-\beta)$ constant records the dependence on the algorithm's parameter. The paper also uses Lemma 5.3 in its analysis of WMR's expected loss (Littlestone and Warmuth 1994, pp. 236, 240).

The paper proves these results; this mission asks for machine-checked proofs of their exact Lean statements. Its definition of a permitted continuous run and its upper-update potential conditions can also support subsequent formalizations of WMG and WMR. Lemma 5.1, the potential estimate, and the final loss bound remain distinct proof targets so that a solver can use or improve the underlying analytic infrastructure without changing the goal.

Difficulty

A binary mistake indicator cannot express the magnitude of an error between two unit-interval values. The generalized update contains a real exponent, absolute values, and a range of legal factors. An argument that handles only a selected endpoint of that range would leave permitted WMC runs uncovered. A further boundary occurs at $\beta=0$: an allowed update can reduce a positive weight to zero, and real logarithms in Lean have a defined value at zero although the paper's logarithmic bound is infinite there. The formal statements therefore distinguish the zero-final-weight clause from the finite-logarithm clause.

Formalization scope

The pool is Fin n with $n>0$ and the trials are Fin t; an empty sequence of trials is allowed. Lean's trial index starts at zero, so w 0 represents $w^{(1)}$ and w t represents the weights after all $t$ trials. The inputs are the prediction array and label array. Instances are not stored separately because the theorem refers to them only through expert predictions. Values, factors, totals, and losses are real numbers. The run predicate requires positive initial weights, nonnegative weights, predictions and labels in $[0,1]$, $0\le\beta<1$, and a permitted factor for every expert on every trial.

The theorem quantifies over every permitted run. A sorry-free local example exhibits a one-trial run with positive final weight, ruling out a globally empty run predicate. For positive final weight, the update conditions ensure earlier total weights are positive, so every weighted mean used in the loss has its intended denominator. The finite logarithmic conclusions assume positive final weight because Real.log 0 would otherwise introduce an unrelated total-function value. The definition layer supplies total weight, weighted mean, loss, base conditions, the upper-update conditions, and WMC runs; the proof development needs finite-sum and real logarithm inequalities from Mathlib. Contributions that establish the three numbered lemmas or the goal under this interface are in scope.

Selected references

• Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

Motivation

Bounds on the upper tail $P(S_n\ge x)$ of a sum $S_n=X_1+\dots+X_n$ of independent random variables are used throughout probability, statistics, queueing and risk theory: they control ruin probabilities, the error of empirical averages, and the size of the largest deviations of random walks. The classical exponential inequalities (Bernstein, Hoeffding, Bennett) require the summands to be bounded or to have finite exponential moments of a fixed order. The polynomial bounds of Fuk and Nagaev only require finite power moments, at the price of a power-law rate.

Between these two regimes lie summands whose right tails decay like $e^{-g(u)}$ for a function $g$ growing faster than a logarithm — Weibull-type and other subexponential or superexponential tails. For such summands the natural size parameter is not a power moment but a generalized moment $b_{gj}=E[e^{g(X_j)};X_j\ge 0]$. Section 2 of S. V. Nagaev's survey Large deviations of sums of independent random variables (Ann. Probab. 7, 1979, doi:10.1214/aop/1176994938) develops bounds on $P(S_n\ge x)$ in terms of these quantities. Theorem 2.5 of that section, attributed to S. K. Sakoyan and Nagaev, treats the case where $g$ has a positive nondecreasing derivative — the case $\liminf_{x\to\infty}g(x)/x>0$ of the paper — and gives a bound in product form whose exponential order is $e^{-ng(x/n)}$.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1,\dots,X_n$ independent real random variables with distribution functions $F_j(u)=P(X_j<u)$. Write

$$S_n=X_1+\dots+X_n .$$

Let $g:\mathbb R\to\mathbb R$ be differentiable with a derivative $g'$ that is positive and nondecreasing; in particular $g$ is convex and increasing, and $g(u)\to\infty$ as $u\to\infty$.

For each summand define the generalized moment

$$b_{gj}=\int_{u\ge 0}e^{g(u)}\,dF_j(u)=E\big[e^{g(X_j)};\,X_j\ge 0\big],$$

and, for a real $s$, the negative-part factor

$$b_j(s)=e^{g(0)}\int_{u<0}e^{g'(s)u}\,dF_j(u)=e^{g(0)}E\big[e^{g'(s)X_j};\,X_j<0\big].$$

The factor $b_j(s)$ is always finite, since its integrand lies in $(0,1]$; $b_{gj}$ may be infinite, and the theorem is meaningful only when every $b_{gj}$ is finite. In Lean these objects are S n X, bg P X g j and bj P X g g' j s in the namespace NagaevLD.GenMoment.

Formalization targets

Goal: Theorem 2.5, (2.44), p. 767

For every $x>0$,

$$P(S_n\ge x)\ \le\ \prod_{j=1}^n\big(b_j(x/n)+b_{gj}\big)\exp\{-ng(x/n)\}.$$

The statement holds for every $n$, every distribution of the summands with finite $b_{gj}$, and every admissible $g$; no constant is hidden.

Milestones

The proof of the paper passes through the following displays, all on pp. 767–768, with $h=g'(x/n)$ where indicated:

1. (2.45) the exponential Chebyshev bound $P(S_n\ge x)\le e^{-hx}\prod_{j}Ee^{hX_j}$ for $h\ge 0$;
2. (2.46) the exact split of $Ee^{hX_j}$ at zero and the bound $Ee^{hX_j}\le\int_{u<0}e^{hu}\,dF_j(u)+b_{gj}\sup_{u\ge 0}e^{hu-g(u)}$;
3. (2.47) for $h=g'(x/n)$, $\sup_{u\ge 0}e^{hu-g(u)}=e^{hx/n-g(x/n)}$;
4. the convexity step $g'(x/n)x/n\ge g(x/n)-g(0)$, hence $e^{hx/n-g(x/n)}\ge e^{-g(0)}$;
5. (2.48) $\int_{u<0}e^{hu}\,dF_j(u)\le\exp\{g(0)+hx/n-g(x/n)\}\int_{u<0}e^{hu}\,dF_j(u)$;
6. the per-factor bound $Ee^{hX_j}\le(b_j(x/n)+b_{gj})\exp\{hx/n-g(x/n)\}$.

Significance

The bound separates the tail of $S_n$ into a product of one-summand quantities. For fixed $n$ and $x\to\infty$ one has $\prod_j(b_j(x/n)+b_{gj})\to\prod_j b_{gj}$, so $P(S_n\ge x)<(1+\varepsilon)\prod_j b_{gj}\,e^{-ng(x/n)}$ for large $x$ (the paper's (2.49)); compared with the elementary lower bound $P(S_n\ge x)\ge\prod_j P(X_j\ge x/n)$ (2.50), this shows the exponential order $e^{-ng(x/n)}$ is the right one when the right tails of the summands are of order $b_{gj}e^{-g}$. The only case where the right side does not depend on $n$ is $g(u)=Tu$, the classical Chernoff regime, of which the theorem is a generalization.

The result is a published theorem with a complete half-page proof; it is not open. As far as a search of the Prove2Me catalogue shows, no part of it has been machine-checked: the catalogue contains single-variable Chernoff bounds (Mathlib's measure_ge_le_exp_mul_mgf) but no bound in terms of generalized moments. The mission produces a formal proof of the theorem and, along the way, reusable statements about tilted truncated moments of independent sums.

Difficulty

Each step of the argument is short; the work is in carrying it through real-valued measure theory. The exponential Chebyshev step requires the moment generating function of a sum of independent variables to factor, which needs the integrability of every $e^{hX_j}$ — a fact that here must be derived from the finiteness of $b_{gj}$ and the bound on $e^{hu-g(u)}$, not assumed. The supremum in (2.46) has to be identified as a maximum attained at $x/n$, which rests on the convexity of $g$ on $[0,\infty)$ obtained from a monotone derivative. Finally the split of $Ee^{hX_j}$ at $0$ must match the definition of $b_{gj}$ exactly: a mismatch at the single point $u=0$ breaks the theorem.

Formalization scope

The summands are X : Fin n → Ω → ℝ on a probability space, each measurable and jointly independent (iIndepFun); index $j$ in Lean is the paper's $j+1$. Integrals $\int\cdot\,dF_j(u)$ over a set of $u$ are written as expectations restricted to the corresponding event, so no distribution functions appear. Probabilities are P.real, and $P(S_n\ge x)$ is P.real {ω | x ≤ S n X ω}.

Committed conventions and disclosed additions:

• $b_{gj}$ over $u\ge 0$. The paper defines $b_{gi}=\int_{0+}^{\infty}e^{g(u)}\,dF_i(u)$ (p. 759), over $u>0$. The proof splits at $0-$ and bounds the whole part on $u\ge 0$ by $b_{gj}$; with the $u>0$ reading the theorem is false (two summands with $P(X_j=1)=0.1$, $P(X_j=0)=0.9$, $g(u)=u$, $x=1$ give $P(S_2\ge 1)=0.19$ against a bound of about $0.027$). The formalization integrates over $u\ge 0$.
• Finiteness of $b_{gj}$ is an explicit integrability hypothesis. The paper treats $b_{gj}$ as a finite factor; Lean's integral of a non-integrable function is $0$, which would turn the bound into a false statement rather than a trivial one. This rules out the trivializing reading in which a junk $b_{gj}=0$ is used.
• Hypotheses on $g$ — differentiability, $g'>0$, $g'$ nondecreasing — are imposed on $[0,\infty)$ only, the region where $g$ and $g'$ are evaluated; the paper's global hypothesis implies them. They also give §2's standing assumption that $g$ is nondecreasing with $g(u)\to\infty$, which is therefore not stated separately.
• Suprema in (2.46)–(2.47) are never real sSup: (2.46) is stated for every upper bound $M$ of $e^{hu-g(u)}$ on $u\ge 0$, and (2.47) as IsGreatest.
• The convexity step is stated with "$\ge$"; the page prints "$>$", which fails for $g(u)=Tu$.
• $n\ge1$ is explicit in the theorem statements, matching the paper's sum $X_1+\dots+X_n$ and avoiding Lean's $x/0=0$ value.
• (2.45) assumes the finiteness of each $Ee^{hX_j}$, which the page takes for granted.
• (2.46) assumes $h\ge0$, as used in the proof, so its negative-part expectation is finite; the finite $b_{gj}$ and an upper bound on $e^{hu-g(u)}$ make its positive part finite.

A complete development needs the factorization of exponential moments of independent sums (available in Mathlib as iIndepFun.mgf_sum), Markov's inequality, splitting a Bochner integral over an event and its complement, and the tangent-line inequality for a function with monotone derivative. Proofs of the milestones, alternative arguments, and lemmas on truncated exponential moments are all welcome.

Selected references

• S. V. Nagaev, Large deviations of sums of independent random variables, Annals of Probability 7(5), 745–789, 1979. doi:10.1214/aop/1176994938
• D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory of Probability and Its Applications 16(4), 643–660, 1971. doi:10.1137/1116071
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23(4), 493–507, 1952. doi:10.1214/aoms/1177729330

Motivation

Congestion games model situations in which agents choose sets of shared resources and the payoff of each resource depends only on how many agents use it: drivers choosing routes through road segments, jobs choosing machines, flows choosing links in a network. Rosenthal (A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2, 1973) showed that every such game has a pure-strategy Nash equilibrium, by exhibiting a single real function on strategy profiles whose changes track every player's unilateral payoff changes.

Monderer and Shapley (Potential Games, Games Econ. Behav. 14, 1996) isolated that property and called games having it potential games. Their Section 3 shows that the property characterizes congestion games: Rosenthal's argument gives Theorem 3.1 (every congestion game is a potential game), and Theorem 3.2 gives the converse up to a renaming of strategies. Potential games have since become a standard tool in algorithmic game theory (convergence of best-response dynamics, price of stability bounds, learning in games), and Theorem 3.2 is the reason that results proved for congestion games apply to all finite potential games.

Setting

A game in strategic form $\Gamma$ has a finite set of players $N = \{1, \dots, n\}$, for each player $i$ a strategy set $Y^i$, the profile set $Y = \times_{i\in N} Y^i$, and payoff functions $u^i : Y \to \mathbb{R}$. For a profile $y$ and $x \in Y^i$, $(y^{-i}, x)$ is $y$ with player $i$'s strategy replaced by $x$. The game is finite if every $Y^i$ is finite.

A function $P : Y \to \mathbb{R}$ is a potential for $\Gamma$ (condition (2.2) with unit weights) if

$$u^i(y^{-i}, x) - u^i(y^{-i}, z) = P(y^{-i}, x) - P(y^{-i}, z) \qquad \text{for all } i,\ y^{-i},\ x, z \in Y^i,$$

and $\Gamma$ is a potential game if it has a potential (IsPotential, IsPotentialGame).

A congestion model $C(N, M, (\Sigma^i)_{i\in N}, (c_j)_{j\in M})$ has players $N$, a finite set of facilities $M$, for every player a set $\Sigma^i$ of strategies, each a nonempty subset of $M$, and for every facility $j$ a vector $c_j$, where $c_j(k)$ is the payoff to each user of $j$ when exactly $k$ players use it. The associated congestion game has strategy sets $\Sigma^i$ and payoffs

$$v^i(A) = \sum_{j\in A^i} c_j\big(\sigma_j(A)\big), \qquad \sigma_j(A) = \#\{i \in N : j \in A^i\}. \tag{3.1}$$

Two games with the same players are isomorphic (IsIsomorphic) if there are bijections $g^i : Y^i_1 \to Y^i_2$ with $u^i_1(y) = u^i_2(g^1(y^1), \dots, g^n(y^n))$ for every player $i$ and profile $y$.

Formalization targets

Goal: Theorem 3.2

$$\text{Every finite potential game is isomorphic to a congestion game.}$$

Formally: for every finite set of players, finite strategy sets $Y^i$ and payoffs $u$ admitting a potential, there are $m \in \mathbb{N}$ and a congestion model on the facilities $\{1, \dots, m\}$, all of whose strategies are nonempty facility sets, whose congestion game is isomorphic to $\Gamma$.

Milestones

The milestones follow Appendix B of the paper.

1. Lemma B.1 (p. 139): with $x^r(j) = c_j(r)$ and $x(B) = \sum_{j\in B} x(j)$, $v^i(A) = x^1(A(i)\cap A(-i)^c) + x^2\big(\bigcup_{k\neq i}[A(i)\cap A(k)\cap A(-\{i,k\})^c]\big) + \cdots + x^n\big(\bigcap_{k} A(k)\big)$.
2. The invariance of $u^i - P$ (p. 141): $u^i(a^{-i}, a^i) - P(a^{-i}, a^i)$ does not depend on $a^i$.
3. The $M_1$ identity and (B.2) (p. 141): on the facility set $M = \times_i \{0,1\}^{K(i)}$, $A^1_{m_1}\cap\cdots\cap A^n_{m_n}\cap M_1 = \{\varepsilon(m)\}$, so $x^n(A^1_{m_1}\cap\cdots\cap A^n_{m_n}) = P(a^1_{m_1}, \dots, a^n_{m_n})$.
4. (B.6) (p. 141): $x^1(A^i_{m_i}\cap A(-i)^c) = x^1(\varepsilon(m^i)) = u^i(a) - P(a)$.

Significance

Theorems 3.1 and 3.2 together say that, up to renaming strategies, the finite potential games and the congestion games are the same class. Consequently any statement about finite congestion games that is invariant under isomorphism (existence of pure equilibria, convergence of improvement dynamics, the structure of equilibrium sets) holds for all finite potential games, and conversely any potential game can be realized as a resource-sharing model. The representation is also the starting point of the later literature on the number of facilities needed to represent potential games, which the paper itself begins with a remark at the end of Appendix B.

Theorem 3.1 is already machine-checked on the platform, as Rosenthal's potential identity PriceOfStability.Harmonic.rosenthal_potential_change (Proved); it is included in this mission as a reference item. Theorem 3.2 is proved in the paper but has no machine-checked proof that we know of. The mission adds a formal statement of the theorem, of isomorphism of games, of congestion games as games in strategic form, and of the explicit construction of Appendix B; and, once proved, a verified converse to Rosenthal's theorem.

Difficulty

The theorem is an explicit construction, and its difficulty is bookkeeping rather than a single hard idea. The facility set is a product of Boolean cubes, one per player; each player's strategy is the set of facilities with a 1 in a given coordinate; and the facility payoffs are defined only at load $1$ and load $n$, by two auxiliary vectors whose definitions involve a choice of representative. Showing that the resulting congestion game reproduces every payoff requires identifying, for every profile, exactly which facilities are used by one player and which by all players, and showing that the "load 1" facilities pick up precisely the part of $u^i$ that player $i$ cannot influence. The paper leaves the two key set identities as "it can be verified"; they are the milestones.

The construction as printed does not cover one player: with $n = 1$ the vectors $x^1$ and $x^n$ are the same vector, defined twice. The theorem is still true for one player, and the formal goal does not exclude it, so a complete proof must treat that case separately.

Formalization scope

• Players form a finite type ι with decidable equality; strategy sets are types Y i, finite in the goal ([∀ i, Fintype (Y i)]). $(y^{-i}, x)$ is Function.update y i x. No nonemptiness of the strategy sets and no lower bound on the number of players is assumed.
• The congestion model is the published CongestionPoA.AsymSum.CongestionGame ι M (reference item): strategies i is the finite family $\Sigma^i$ and latency j k is the paper's $c_j(k)$, an arbitrary real number. No sign change is made; the published names "latency" and "cost" are only names. Values of latency at $0$ and above $n$ never enter (3.1).
• The congestion game as a game in strategic form is congestionPayoff G, whose strategy set for player $i$ is the subtype of G.strategies i. Because the isomorphism maps onto that subtype, the strategies of a player are distinct facility sets.
• In the goal the facility set is Fin m for an existentially quantified $m$, and nonemptiness of every strategy, which is part of the definition of a congestion model on p. 133 but not of the published structure, is a separate conjunct. Dropping it, or replacing "congestion game" by an arbitrary game whose payoffs equal $u$, would make the goal a different, weaker statement; the formal goal does neither.
• The Appendix B construction (FacilityConstruction) indexes the coordinates of player $i$ by $Y^i$ itself instead of $K(i) = \{1, \dots, k(i)\}$; $m^i = (m_k)_{k\neq i}$ is passed as a full profile whose $i$-th coordinate is ignored; $x^n$ and $x^1$ select a representative by choice, the chosen $i$-th coordinate playing the role of the arbitrary $a^i$ in (B.4).
• Misprints corrected: in Lemma B.1, $x^r(j) = c_j(m)$ is read $c_j(r)$, and the "$\cdots$" as the general term $x^r(\bigcup_{S\ni i, |S| = r}[\bigcap_{k\in S}A(k)\cap A(-S)^c])$; in (B.6), $A(-i)$ is read $A(-i)^c$ and $P^i(a)$ as $P(a)$.

Contributions welcome: proofs of the milestones, a proof of the goal (by the paper's construction, with the one-player case handled separately, or by any other construction), and general lemmas about transporting potentials along isomorphisms.

Selected references

• D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2 (1973), 65–67. https://doi.org/10.1007/BF01737559
• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler and T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38 (2008), 1602–1623. https://doi.org/10.1137/070680096 (source of the platform's Rosenthal potential identity)

Motivation

The method of multipliers (augmented Lagrangian method) solves a constrained convex program by alternating an unconstrained minimization in the primal variables with an explicit update of the Lagrange multipliers. Rockafellar showed in 1976 that the classical quadratic version is the proximal point algorithm applied to the dual problem, and that a variant which also adds a proximal term in the primal variables, the proximal method of multipliers, is the proximal point algorithm applied to the saddle operator of the Lagrangian (Rockafellar 1976, Math. Oper. Res.). The primal proximal term makes each subproblem strictly convex, so its minimizer is unique, and the theory gives convergence of the primal and dual iterates together.

Penalty functions other than the quadratic one, such as the exponential multiplier method, were used in practice and studied by Bertsekas, Kort and Tseng, but their convergence theory was separate from the proximal point framework. Eckstein's 1993 paper (Math. Oper. Res. 18(1), 202–226) replaces the squared distance in the proximal point algorithm by the D-function of a Bregman function. Its §5 obtains the first nonquadratic generalization of the proximal method of multipliers and proves that it converges to a saddle point. This mission formalizes that theorem, Theorem 8.

• 1967: Bregman introduces D-functions for convex feasibility (Bregman 1967).
• 1976: Rockafellar proves convergence of the quadratic method of multipliers and the proximal method of multipliers via the proximal point algorithm.
• 1990–1992: Censor and Zenios propose the proximal minimization algorithm with D-functions.
• 1993: Eckstein proves convergence of the Bregman proximal point algorithm for maximal monotone operators (Theorem 1) and derives nonquadratic multiplier methods (Theorems 6–8).

Setting

A convex program of the form (10) is

$$\min f(x)\quad\text{subject to}\quad g_i(x)\le0\ (i=1,\dots,m),\ x\in C,$$

where $C\subseteq\mathbb R^n$ is closed, nonempty and convex, and $f,g_1,\dots,g_m:\mathbb R^n\to(-\infty,+\infty]$ are proper lower semicontinuous convex functions, finite on $C$. Write $g(x)=(g_1(x),\dots,g_m(x))$ and $\overline{\Omega^+}=\{p\in\mathbb R^m:p\ge0\}$. The Lagrangian is $l(x,p)=f(x)+\sum_ip_ig_i(x)$ for $x\in C$, $p\ge0$; $l(x,p)=-\infty$ for $x\in C$, $p\not\ge0$; $l(x,p)=+\infty$ for $x\notin C$. A saddle pair $(x^*,p^*)$ satisfies $l(x^*,p)\le l(x^*,p^*)\le l(x,p^*)$ for all $x,p$; the paper calls these optimal solution–Lagrange multiplier pairs. The saddle operator on $\mathbb R^{n+m}$ is $K(x,p)=\partial_xl(x,p)\times(-\hat\partial_pl(x,p))$, where $\partial_x$ is the subdifferential of the convex function $l(\cdot,p)$ and $\hat\partial_p$ the set of supergradients of the concave function $l(x,\cdot)$.

For a differentiable $h$, the D-function is $D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle$. A Bregman function with open zone $S$ is a function $h:\overline S\to\mathbb R$, continuously differentiable on $S$, strictly convex and continuous on $\overline S$, whose partial level sets of $D_h$ are bounded, and which satisfies two sequential conditions relating $D_h\to0$ to convergence (Definition 1). For $h:\mathbb R^m\to\mathbb R$, the monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$.

Given Bregman functions $h_x$ on $\mathbb R^n$ and $h_p$ on $\mathbb R^m$ and step sizes $c_k>0$, the nonquadratic proximal method of multipliers (12) is

$$x^{k+1}=\arg\min_{x\in C}\Big\{f(x)+\tfrac1{c_k}h_p^{*+}\big(\nabla h_p(p^k)+c_kg(x)\big)+\tfrac1{c_k}D_{h_x}(x,x^k)\Big\},\qquad p^{k+1}=\nabla h_p^{*+}\big(\nabla h_p(p^k)+c_kg(x^{k+1})\big).$$

Formalization targets

Goal: Theorem 8

Assume $c_k$ positive and bounded away from zero, $h_x$ a Bregman function with zone $S_x\supseteq C$, $h_p$ a Bregman function with zone $S_p\supseteq\overline{\Omega^+}$ and $\operatorname{im}\nabla h_p=\mathbb R^m$, and $\{(x^k,p^k)\}$ conforming to (12). Then

$$\exists\text{ saddle pair}\ \Longrightarrow\ (x^k,p^k)\to(x^*,p^*)\ \text{for some saddle pair }(x^*,p^*),$$ $$\nexists\text{ saddle pair}\ \Longrightarrow\ \{x^k\}\text{ or }\{p^k\}\text{ is unbounded}.$$

Existence clause

For the same step-size assumption, if in addition $\operatorname{im}\nabla h_x=\mathbb R^n$, a sequence conforming to (12) exists from every $(x^0,p^0)\in C\times\overline{\Omega^+}$. This is the third sentence of Theorem 8, stated as a separate item.

Milestones

Lemma 2 (four descriptions of $h^{*+}$, monotonicity), Lemma 3 ($h^{*+}$ finite and differentiable), Lemma A4 (a subdifferential chain rule), (14) (the $x$-step is a Bregman proximal step on $\partial_xl$), the formula $\hat\partial_pl(x,p)=\{g(x)\}-\partial\delta^+(p)$, maximal monotonicity of $K$, saddle pairs $=$ zeros of $K$, $h_x\oplus h_p$ is a Bregman function with zone $S_x\times S_p\supseteq\overline{\operatorname{dom}K}$, the identity (13), Theorem 1 restated on $\mathbb R^{n+m}$, Theorem 4 restated, and the existence clause.

Significance

Theorem 8 gives a family of primal–dual methods for convex programs, parametrized by two Bregman functions, each with the convergence guarantee of the quadratic proximal method of multipliers: convergence of both sequences to a saddle point when one exists, and divergence otherwise. Choosing $h_p$ to match the orthant (for instance entropy-like functions) yields exponential-type multiplier updates, and choosing $h_x$ to match $C$ adapts the primal regularization to the feasible set. The uniqueness of the primal minimizer, which the dual method of §4.2 lacks, is what allows convergence of the primal iterates without further assumptions.

The result is proved in the paper, with some steps asserted rather than proved (that $h_x\oplus h_p$ is a Bregman function; the maximality of $K$, cited from Rockafellar). No machine-checked proof of Theorem 8, of Theorem 1, or of the monotone-conjugate lemmas is known. A formalization would check the reduction of (12) to (13) carefully, including the extended-value conventions of the Lagrangian, and would provide reusable statements about Bregman functions on product spaces and about saddle operators of convex programs.

Difficulty

The reduction of Theorem 8 to Theorem 1 is short on the page but uses several nontrivial facts. The $x$-step is a constrained minimization of a composite function; turning its optimality condition into the inclusion (14) in $\partial_xl(x^{k+1},p^{k+1})$ needs a chain rule for a nondecreasing differentiable outer function composed with extended-valued convex functions (Lemma A4), together with properties of the monotone conjugate (Lemmas 2 and 3) that rest on recession arguments in the Appendix. The $p$-step requires identifying $\partial[h_p^{*+}]^*$ with $\nabla h_p+\partial\delta^+$, which uses $S_p\supseteq\overline{\Omega^+}$. Maximal monotonicity of $K$ is a theorem about closed saddle functions, not a consequence of monotonicity alone. Theorem 1 itself is the main theorem of the paper and depends on all six conditions of Definition 1.

A natural first idea, applying Theorem 1 to $K$ directly with an arbitrary Bregman function on $\mathbb R^{n+m}$, does not describe (12): the method is the specific instance $h=h_x\oplus h_p$, and the identification of its steps with $(\nabla h+c_kK)^{-1}$ is the content of (13).

Formalization scope

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k); $\mathbb R^{n+m}$ is WithLp 2 (E n × E m), which carries the Euclidean inner product. The §2 objects (Bregman function, $D_h$, runs of (3) written through the equivalent inclusion (4)) are defined over any finite-dimensional real inner product space so that Theorem 1 applies on $\mathbb R^{n+m}$.
• Extended-real functions are EReal-valued; properness, convexity (of the epigraph) and subgradients use published definitions. $h_p^{*+}$ is EReal-valued; the recursion (12) uses its real value and the gradient of that real function, which is exact because Lemma 3, a milestone, proves finiteness and differentiability.
• "Optimal solution–Lagrange multiplier pair" is the saddle inequality, as identified on p. 220. "Converges to one" means both sequences converge, to the two components of one saddle pair; "unbounded" means the range is not bounded.
• The $x$-step is a minimality predicate over $C$ rather than $\arg\min$ (equivalent; the minimizer is unique). A run requires $x^0\in S_x$, not $x^0\in C$, and $p^k\in S_p$, so that every gradient in (12) is defined.
• Corrected typos: the page's "$S_p\supset\overline{\Omega^+}$" is read as $\supseteq$; in Lemma A4, "Lemma 5" is Lemma 2 and "$f(x)\in\mathbb R^n$" is $\mathbb R^m$; Theorem 1's "monontone" is monotone; the supergradient formula's "$\delta^+(p)$" denotes $\partial\delta^+(p)$; the existence clause's extra parenthesis is dropped. In Lemma A4 a term $y_i\partial f_i(x^0)$ with $y_i=0$ is $\{0\}$, following the proof.
• The §4.2 assumption that the dual functional is not everywhere $-\infty$ is not assumed; §5 does not use it.
• A trivializing formalization is ruled out: the goal's hypotheses are satisfiable (with $h_x=h_p=\frac12\|\cdot\|^2$, $C=\mathbb R$, $f(x)=x^2$, $g_1(x)=x-1$ there is a saddle pair, checked in Lean), $h^{*+}$ is not replaced by a real supremum with junk values, and the saddle predicate quantifies over all of $\mathbb R^n\times\mathbb R^m$.
• Infrastructure a full development needs: Bregman functions on products, the monotone conjugate and its smoothness, a subdifferential sum and chain rule for extended-valued functions, maximal monotonicity of saddle operators, and Theorem 1. The monotone conjugate lemmas and Theorem 1 are shared with the companion missions of this series. Contributions to any milestone are welcome, including proofs of the restated Theorems 1 and 4 independent of the companion missions.

Selected references

• J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 1993, 202–226. https://doi.org/10.1287/moor.18.1.202
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2), 1976, 97–116. https://doi.org/10.1287/moor.1.2.97
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3), 1967, 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• Y. Censor and S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3), 1992, 451–464. https://doi.org/10.1007/BF00940051

Motivation

Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.

Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).

Setting

Let $X$ be a lattice: a partially ordered set in which every two elements $x, y$ have a least upper bound $x \vee y$ (join) and a greatest lower bound $x \wedge y$ (meet). Examples are $\mathbb{R}^n$ and products of finite chains, ordered componentwise.

A function $f : X \to \mathbb{R}$ is supermodular on a set $S \subseteq X$ if

$$f(x) + f(y) \le f(x \vee y) + f(x \wedge y) \qquad \text{for all } x, y \in S.$$

It is quasisupermodular (p. 162) if for all $x, y \in X$

1. $f(x) \ge f(x \wedge y)$ implies $f(x \vee y) \ge f(y)$, and
2. $f(x) > f(x \wedge y)$ implies $f(x \vee y) > f(y)$.

A function $h : \mathbb{R} \to \mathbb{R}$ is strictly increasing if $r < s$ implies $h(r) < h(s)$. A function $f$ is supermodularizable if $h \circ f$ is supermodular on $X$ for some strictly increasing $h$.

For $x_1, x_2 \in X$ the set $\{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}$ is closed under $\vee$ and $\wedge$; it is the sublattice generated by $x_1$ and $x_2$ and has at most four points.

Quasisupermodularity depends only on the order of the values of $f$, so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.

Formalization targets

Goal: Theorem 8 (p. 165)

$f : X \to \mathbb{R}$ is quasisupermodular if and only if there is $g : \mathbb{R} \times X \times X \to \mathbb{R}$ such that (i) $r \mapsto g(r, x_1, x_2)$ is strictly increasing for every $(x_1, x_2) \in X^2$, and (ii) for every $x_1, x_2 \in X$,

$$x \mapsto g(f(x), x_1, x_2) \ \text{ is supermodular on } \{x_1, x_2, x_1 \vee x_2, x_1 \wedge x_2\}.$$

Milestones

1. Invariance (p. 164): if $f$ is quasisupermodular and $g$ strictly increasing, $g \circ f$ is quasisupermodular.
2. Supermodularizable implies quasisupermodular (pp. 164–165): if $h$ is strictly increasing and $h \circ f$ is supermodular on $X$, then $f$ is quasisupermodular.
3. Lemma (p. 165): if $f$ is quasisupermodular on $L = \{x, x', x \vee x', x \wedge x'\}$, then $h \circ f$ is supermodular on $L$ for some strictly increasing $h : \mathbb{R} \to \mathbb{R}$.
4. Example 1 (p. 165): the function on $\{0,1\} \times \{0,1,2,3\}$ with rows $(1,2,2,1)$ and $(3,4,5,3)$ is quasisupermodular but not supermodularizable.

The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on $(x_1, x_2)$.

Significance

Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.

On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of $\mathbb{R}$ that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.

Difficulty

The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values $a, b, c, d$ of $f$ at $x, x \vee x', x \wedge x', x'$ need not satisfy $a + d \le b + c$, and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing $h$ of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which $x$ and $x'$ are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair $(x, x')$.

Formalization scope

• Lattices are Mathlib's Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.
• Quasisupermodularity is a draft definition QuasiSupermodularOn g S, relativized to a set $S$; the paper's notion on $X$ is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of $S$.
• Supermodularity is the published definition Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.
• "Strictly increasing" is StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.
• The transformation $g : \mathbb{R} \times X \times X \to \mathbb{R}$ of Theorem 8 is curried, g : ℝ → X → X → ℝ; it may depend on $(x_1, x_2)$ but not on $x$. Transformations are defined on all of $\mathbb{R}$, as printed, not only on the values of $f$.
• The Lemma's four-point lattice is formalized as the subset $\{x, x', x \vee x', x \wedge x'\}$ of an ambient lattice, with both notions relativized to it; the subset is closed under join and meet, so this is the page's statement, including the degenerate cases.
• Example 1's domain is Fin 2 × Fin 4 with the product order.

Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps $\mathbb{R} \to \mathbb{R}$ with prescribed values on finitely many points.

Selected references

• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 305–321, 1978. https://doi.org/10.1287/opre.26.2.305
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• M. Li Calzi, Generalized Symmetric Supermodular Functions, Working Paper, Stanford University, 1990 (listed so in the paper's references; the text on p. 165 cites it as Li Calzi (1991)).

Motivation

The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues $1=\beta_0>\beta_1\ge\dots\ge\beta_{m-1}\ge-1$, the distance to stationarity after $n$ steps is governed by $\beta_*^{\,n}$, where $\beta_*=\max(\beta_1,|\beta_{m-1}|)$ (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue $\beta_1$ are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue $\beta_{\min}=\beta_{m-1}$: a chain whose smallest eigenvalue is close to $-1$ oscillates almost periodically and mixes slowly whatever $\beta_1$ is. A chain is aperiodic exactly when $\beta_{\min}>-1$, but that qualitative fact gives no rate.

Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on $\beta_{\min}$ uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.

Timeline:

• 1988–1989, Jerrum and Sinclair: conductance (Cheeger-type) bounds on $\beta_1$ for chains on combinatorial structures.
• 1991, Diaconis and Stroock: path bounds for $\beta_1$ (Proposition 1, the Poincaré inequality $\beta_1\le1-1/\kappa$) and for $\beta_{\min}$ (Proposition 2, this mission), with the specializations to random walks on graphs (Corollaries 1 and 2).

Setting

Let $X$ be a finite set and $P(x,y)$ the transition matrix of an irreducible Markov chain on $X$, reversible with respect to a probability distribution $\pi$:

$$Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)\qquad(x,y\in X).$$

The operator $(P\varphi)(x)=\sum_yP(x,y)\varphi(y)$ is self-adjoint on $L^2(\pi)$, with inner product $\langle\varphi,\psi\rangle_{L^2(\pi)}=\sum_x\varphi(x)\psi(x)\pi(x)$, so its eigenvalues are real. Write $E(\varphi^2)=\sum_x\varphi(x)^2\pi(x)$ and let $\beta_{\min}$ be the smallest eigenvalue of $P$.

The graph of the chain has vertex set $X$, an edge from $x$ to $y$ when $Q(x,y)>0$, and a self-loop at $x$ when $Q(x,x)>0$. An odd closed path $\sigma_x$ at $x$ is a sequence of edges from $x$ back to $x$, with an odd number of edges, in which no directed edge is traversed twice. Its length is

$$|\sigma_x|_Q=\sum_{e\in\sigma_x}Q(e)^{-1}.$$

A system of odd paths $\Sigma=(\sigma_x)_{x\in X}$ chooses one such path for every point, and its load is

$$\iota=\iota(\Sigma)=\max_e\sum_{\sigma_x\ni e}|\sigma_x|_Q\,\pi(x),$$

the maximum over directed edges $e$ of the weighted length of the paths through $e$ (display (1.7) of the paper).

For the random walk on a graph $G=(X,E)$, $P(x,y)=1/d(x)$ when $\{x,y\}\in E$, with $d(x)$ the degree, and $\pi(x)=d(x)/2|E|$. There $d_*$ is the maximum degree, $\sigma_*$ the largest number of edges of a path in $\Sigma$, and $b_*=\max_e\sharp\{\sigma\in\Sigma:e\in\sigma\}$.

Formalization targets

Goal: Proposition 2

For an irreducible, aperiodic, reversible chain and every system $\Sigma$ of odd closed paths,

$$\beta_{\min}\ge-1+\frac{2}{\iota(\Sigma)}.$$

Milestones (the steps of the paper's proof)

1. The identity (1.8): $\tfrac12\sum_{x,y}(\varphi(x)+\varphi(y))^2Q(x,y)=E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}$.
2. Along an odd closed path $x,y,w,\dots,z,x$: $\varphi(x)=\tfrac12\{(\varphi(x)+\varphi(y))-(\varphi(y)+\varphi(w))+\dots+(\varphi(z)+\varphi(x))\}$.
3. For every $\varphi$: $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$.
4. Every eigenvalue $\beta$ of $P$ satisfies $\beta\ge-1+2/\iota$.

Companions

• Corollary 2. For the random walk on a connected, non-bipartite graph and any system $\Sigma$ of odd paths, $\beta_{\min}\ge-1+\dfrac{2}{d_*\sigma_*b_*}$.
• Remark 1.3. With odd paths $\sigma_{xy}$ for every ordered pair and $\tilde\iota=\max_e\sum_{\sigma_{xy}\ni e}|\sigma_{xy}|_Q\pi(x)\pi(y)$: $\beta_{\min}\ge-1+1/\tilde\iota$.

Significance

Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds $\beta_1\le1-1/\kappa$ through paths between pairs of points, it bounds the absolute spectral gap $1-\beta_*$ entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.

Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the $L^2(\pi)$ inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that $-1$ is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.

Difficulty

Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while $\iota$ counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs $(x,y)$, including $x=y$, in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels $\varphi(x)$ instead of doubling it.

The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small $\iota$, and the choice of $\Sigma$ is part of every application.

Formalization scope

The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that $\pi$ is a probability vector) and DetailedBalance. $Q$ is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). $\beta_{\min}$ is the infimum of the real eigenvalues of $P$, a minimum for a stochastic matrix on a nonempty set.

Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with $Q>0$. The paper defines $|\sigma_x|_Q$ "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. $\iota$ is a real supremum over the finite set of directed edges with $Q>0$, and it is $0$ only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to $\beta_{\min}\ge-1$ by $2/0=0$. The system $\Sigma$ is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption $|X|\ge2$ is made.

Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, $b_*$ counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.

Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.

Selected references

• P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
• A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82(1):93–133, 1989. https://doi.org/10.1016/0890-5401(89)90067-9
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (2nd ed. 2017). https://doi.org/10.1090/mbk/107