Operations Research

Motivation

A mathematical program with complementarity constraints (MPCC, also called MPEC, mathematical program with equilibrium constraints) is a nonlinear optimization problem in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such constraints model equilibria inside an optimization problem: bilevel programs whose lower level is replaced by its optimality conditions, Stackelberg games, traffic and electricity market equilibria, contact problems in mechanics. See Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996), doi:10.1017/CBO9780511983658.

The complementarity constraints make the standard theory fail. At every feasible point the Mangasarian–Fromovitz constraint qualification is violated, so the Karush–Kuhn–Tucker conditions are not necessary for optimality, and standard NLP solvers lose their convergence guarantees. A common remedy is relaxation: replace the MPEC by a family of ordinary nonlinear programs depending on a parameter $t>0$, solve them for $t\downarrow0$, and study the limits of their stationary points.

The first relaxation scheme, and the reference point for all later ones, is due to Scholtes (Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001), doi:10.1137/S1052623499361233). Scholtes showed that limits of stationary points of the relaxed programs are C-stationary when MPEC-LICQ holds at the limit. Hoheisel, Kanzow and Schwartz (Preprint 299, University of Würzburg, 2010; later Math. Program. 137 (2013), doi:10.1007/s10107-011-0488-5) compare five relaxation schemes and weaken the constraint qualification in each convergence theorem. For Scholtes' scheme, their Theorem 3.1 replaces MPEC-LICQ by the weaker MPEC-MFCQ. This mission formalizes that theorem.

Setting

The MPEC (1) is

$$\min f(x)\ \ \text{s.t.}\ \ g_i(x)\le0\ (i\le m),\ \ h_i(x)=0\ (i\le p),\ \ G_i(x)\ge0,\ \ H_i(x)\ge0,\ \ G_i(x)H_i(x)=0\ (i\le l),$$

with continuously differentiable $f,g_i,h_i,G_i,H_i:\mathbb R^n\to\mathbb R$ and feasible set $X$. For a point $x^*$ the paper uses the index sets $I_g=\{i\mid g_i(x^*)=0\}$, $I_{0+}=\{i\mid G_i(x^*)=0<H_i(x^*)\}$, $I_{00}=\{i\mid G_i(x^*)=H_i(x^*)=0\}$ and $I_{+0}=\{i\mid G_i(x^*)>0=H_i(x^*)\}$.

A standard nonlinear program has constraints $g_i\le0$, $h_j=0$. Its point $x$ satisfies the Mangasarian–Fromovitz constraint qualification (MFCQ) if the gradients $\nabla h_j(x)$ are linearly independent and some direction $d$ has $\nabla g_i(x)^Td<0$ for all active $i$ and $\nabla h_j(x)^Td=0$ for all $j$. A stationary point is the $x$-part of a KKT point: $x$ is feasible and there are $\lambda\ge0$, $\mu$ with $\lambda_ig_i(x)=0$ and $\nabla f(x)+\sum\lambda_i\nabla g_i(x)+\sum\mu_j\nabla h_j(x)=0$.

The tightened program TNLP$(x^*)$ keeps $g_i\le0$, $h_i=0$ and imposes $G_i=0,\ H_i\ge0$ on $I_{0+}$, $G_i\ge0,\ H_i=0$ on $I_{+0}$, and $G_i=H_i=0$ on $I_{00}$. MPEC-MFCQ holds at $x^*$ if MFCQ holds at $x^*$ for TNLP$(x^*)$.

A feasible $x^*$ is weakly stationary if there are multipliers $\lambda\in\mathbb R^m$, $\mu\in\mathbb R^p$, $\gamma,\nu\in\mathbb R^l$ with

$$\nabla f(x^*)+\sum_{i=1}^m\lambda_i\nabla g_i(x^*)+\sum_{i=1}^p\mu_i\nabla h_i(x^*)-\sum_{i=1}^l\gamma_i\nabla G_i(x^*)-\sum_{i=1}^l\nu_i\nabla H_i(x^*)=0,$$

$\lambda\ge0$, $\lambda_ig_i(x^*)=0$, $\gamma_i=0$ on $I_{+0}$ and $\nu_i=0$ on $I_{0+}$. It is C-stationary if such multipliers can be chosen with, in addition, $\gamma_i\nu_i\ge0$ for all $i\in I_{00}$.

Scholtes' relaxed program $R^S(t)$ replaces $G_i(x)H_i(x)=0$ by $G_i(x)H_i(x)\le t$ and keeps all other constraints of (1). The notation $\{t_k\}\downarrow0$ means a sequence of positive parameters decreasing to $0$.

Formalization targets

Goal: Theorem 3.1

Let $\{t_k\}\downarrow0$, let $x^k$ be a stationary point of $R^S(t_k)$, and let $x^k\to x^*$ with MPEC-MFCQ at $x^*$. Then

$$x^*\ \text{is a C-stationary point of the MPEC (1).}$$

No feasibility of $x^*$ is assumed; it is part of the conclusion.

Milestones

1. Remark 2.2: for a feasible point of a standard NLP, MFCQ holds if and only if the active inequality gradients together with all equality gradients are positive-linearly independent.
2. §2.2, pp. 6–7: MPEC-MFCQ written out explicitly, i.e. linear independence of $\nabla h_i$, $\nabla G_i$ ($I_{00}\cup I_{0+}$) and $\nabla H_i$ ($I_{00}\cup I_{+0}$), plus a direction $d$.
3. Proof of Theorem 3.2, p. 11: MPEC-MFCQ implies positive-linear independence of $\{\nabla g_i(x^*)\}_{I_g}\cup\{\{\nabla h_i\}\cup\{\nabla G_i\}_{I_{00}\cup I_{0+}}\cup\{\nabla H_i\}_{I_{00}\cup I_{+0}}\}$.
4. Proof of Theorem 3.1, p. 9: for large $k$, $I_g(x^k)\subseteq I_g$, $I_G(x^k)\subseteq I_{00}\cup I_{0+}$, $I_H(x^k)\subseteq I_{00}\cup I_{+0}$.
5. Proof of Theorem 3.1, pp. 10–11: under the goal's hypotheses, $x^*$ is weakly stationary.

Significance

Theorem 3.1 says that Scholtes' scheme, run to the limit, produces C-stationary points under a constraint qualification strictly weaker than the one in Scholtes' original result. MPEC-MFCQ is the natural assumption here: under it the KKT multipliers of the relaxed programs need not converge, and the theorem shows that a convergent subsequence of suitably modified multipliers still exists. The result is the first of a family of convergence theorems in the paper (the schemes of Lin–Fukushima, Kadrani–Dussault–Benchakroun and Steffensen–Ulbrich follow the same pattern) and the baseline against which those schemes are compared.

The theorem is proved in the paper; it is not open. To the extent a search of the Prove2Me catalog shows, no MPEC stationarity concept, MPEC constraint qualification or relaxation result has been formalized there, and Mathlib has no theory of constraint qualifications for nonlinear programs. The mission produces a machine-checked proof of Theorem 3.1 and, along the way, reusable statements of Definition 2.1, MFCQ, KKT points and the MFCQ/positive-linear-independence equivalence for general nonlinear programs.

Difficulty

The obvious argument takes a limit of the KKT multipliers of $R^S(t_k)$. That fails twice. First, under MPEC-MFCQ the multiplier sequence need not be bounded, so there may be nothing to take a limit of; boundedness has to be recovered from MPEC-MFCQ through positive-linear independence, a theorem of the alternative. Second, the multiplier $\delta^k$ of the product constraint $G_iH_i\le t_k$ multiplies $H_i\nabla G_i+G_i\nabla H_i$, which is not a multiplier of $\nabla G_i$ or $\nabla H_i$ alone; how it is redistributed depends on whether $i$ lies in $I_{0+}$, $I_{+0}$ or $I_{00}$, and the sign condition on $I_{00}$ comes from the support disjointness between $\delta^k$ and the multipliers of $G_i\ge0$, $H_i\ge0$, which uses $t_k>0$. Compactness, index-set bookkeeping along a subsequence and continuity of all gradients have to be combined.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), gradients are Mathlib's gradient, and $\nabla g(x)^Td$ is the inner product. Constraint indices are Fin m, Fin p, Fin l (0-based); $m,p,l$ may be $0$.
• The paper's standing assumption that all data are continuously differentiable (p. 1) is the explicit hypothesis P.IsC1 (ContDiff ℝ 1 for each function) of the goal and of milestones 4 and 5. Milestones 1–3 are pointwise linear algebra and assume no smoothness.
• "Stationary point of $R^S(t_k)$" is a KKT point of $R^S(t_k)$ viewed as a standard NLP with inequality constraints $g_i\le0$, $-G_i\le0$, $-H_i\le0$, $G_iH_i-t\le0$: feasibility, nonnegative multipliers and complementary slackness are included (p. 5).
• "$\{t_k\}\downarrow0$" is $t_k>0$ for all $k$, $(t_k)$ nonincreasing, and $t_k\to0$.
• Families of gradients are indexed families (repeated vectors count as dependent); in MPEC-MFCQ an index of $I_{00}$ contributes both $\nabla G_i$ and $\nabla H_i$. TNLP$(x^*)$ has constraints indexed by subtypes of the index sets; absent constraints are not padded by zero functions, which would make MPEC-MFCQ fail everywhere.
• Definition 2.3(a) is printed with two misprints ("$\mu_ih_i(x^*)$", "$i=1,\dots,l$" for the complementarity of $\lambda$); the formalization uses $\mu_i\nabla h_i(x^*)$ and $i=1,\dots,m$. C-stationarity requires feasibility and one multiplier tuple satisfying both the weak-stationarity conditions and the sign condition on $I_{00}$.
• A "stationary point" that is merely a feasible point or a critical point of $f$, or a C-stationarity whose sign condition refers to multipliers other than those of the weak-stationarity equation, would make the goal false or empty; neither reading is used. The hypotheses of the goal are jointly satisfiable (checked on the paper's Example 3.6 instance).
• Infrastructure needed: theorems of the alternative (Motzkin/Farkas) for finite families in $\mathbb R^n$, compactness of normalised multiplier sequences, continuity of gradients of $C^1$ maps. The NLP layer (positive-linear dependence, MFCQ, KKT points, Remark 2.2) is reusable for any constraint-qualification development. Contributions of proofs of the milestones, of general NLP lemmas, and of the goal are welcome.

Selected references

• T. Hoheisel, C. Kanzow, A. Schwartz, Theoretical and numerical comparison of relaxation methods for mathematical programs with complementarity constraints, Preprint 299, Institute of Mathematics, University of Würzburg, September 2010; published in Math. Program. 137 (2013) 257–288. doi:10.1007/s10107-011-0488-5
• S. Scholtes, Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001) 918–936. doi:10.1137/S1052623499361233
• Z.-Q. Luo, J.-S. Pang, D. Ralph, Mathematical Programs with Equilibrium Constraints, Cambridge University Press, 1996. doi:10.1017/CBO9780511983658

Motivation

Large service systems such as call centers and hospital wards are modelled as many-server queues: $N$ identical servers, customers arriving according to a general process, service requirements drawn independently from a general distribution $G$, and a single first-come-first-served queue. When $G$ is not exponential the number of customers in system is not Markov, and a tractable state must keep track of how long each customer in service has been served. Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011)) take as state the number in system together with the age measure, the point measure of the ages of the customers in service, and prove a functional law of large numbers: scaled by $N$, these processes converge to the unique solution of a deterministic system, the fluid equations. Earlier fluid and diffusion analyses of the $G/GI/N$ queue worked with other state descriptors (Reed, Ann. Appl. Probab. 19 (2009); Whitt, Oper. Res. 54 (2006)); the measure-valued description records the elapsed service time of every customer in service, which is the information a non-exponential service distribution requires.

This mission covers the deterministic half of that result: the fluid equations are well posed, and their solution is given in closed form.

Setting

Service requirements have a density $g$ that vanishes on $(-\infty,0)$, $G(x)=\int_{(-\infty,x]}g$, and the mean is normalized to one, $\int x\,g(x)\,dx=1$. Let $M=\sup\{x\ge0: G(x)<1\}\in(0,\infty]$ and let $h=g/(1-G)$ be the hazard rate on $[0,M)$; $h$ is locally integrable on $[0,M)$ but not integrable on it. For a measure $\mu$ and a function $f$ write $\langle f,\mu\rangle=\int f\,d\mu$, and $\mathbf 1$ for the constant one.

The data are a triple $(\bar E,\bar X(0),\bar\nu_0)$ in

$$\mathcal S_0=\{(f,x,\mu): f \text{ nondecreasing càdlàg}, f(0)=0;\ x\ge0;\ \mu \text{ a measure on }[0,M),\ \langle\mathbf 1,\mu\rangle\le1,\ 1-\langle\mathbf 1,\mu\rangle=[1-x]^+\},$$

where $\bar E$ is the cumulative arrival process, $\bar X(0)$ the initial number in system and $\bar\nu_0$ the initial age measure (per server, so the total capacity is one). A càdlàg pair $(\bar X,\bar\nu)$, with $\bar\nu_t$ a sub-probability measure on $[0,M)$ in the weak topology, solves the fluid equations if for every $t\ge0$: $\int_0^t\langle h,\bar\nu_s\rangle ds<\infty$ (3.4); for every test function $\varphi\in\mathcal C_c^{1,1}([0,M)\times\mathbb R_+)$

$$\langle\varphi(\cdot,t),\bar\nu_t\rangle=\langle\varphi(\cdot,0),\bar\nu_0\rangle+\int_0^t\langle\varphi_x+\varphi_s,\bar\nu_s\rangle ds-\int_0^t\langle h\varphi(\cdot,s),\bar\nu_s\rangle ds+\int_{[0,t]}\varphi(0,s)\,d\bar K(s)\quad(3.5);$$

$\bar X(t)=\bar X(0)+\bar E(t)-\bar D(t)$ (3.6); and the nonidling condition $1-\langle\mathbf 1,\bar\nu_t\rangle=[1-\bar X(t)]^+$ (3.7). Here $\bar D(t)=\int_0^t\langle h,\bar\nu_s\rangle ds$ is the cumulative departure process and $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\bar D(t)$ the cumulative entry into service. Equation (3.5) is a weak form of a transport equation: mass moves to the right at unit speed, is killed at rate $h$, and enters at age $0$ at rate $d\bar K$.

Formalization targets

Goal: Theorem 3.5

For every $(\bar E,\bar X(0),\bar\nu_0)\in\mathcal S_0$:

1. the fluid equations have at most one solution;
2. under (3.4) and the path conditions, $(\bar X,\bar\nu)$ is a solution if and only if it satisfies (3.6), (3.7) and, for every bounded continuous $f$ and $t\ge0$,

$$\langle f,\bar\nu_t\rangle=\int_{[0,M)}f(x+t)\frac{1-G(x+t)}{1-G(x)}\,\bar\nu_0(dx)+\int_{[0,t]}f(t-s)\big(1-G(t-s)\big)\,d\bar K(s);\quad(3.11)$$

3. if $\bar E$ has a density $\bar\lambda$, then $\bar K$ has a density $\bar\kappa$ equal a.e. to $\bar\lambda$ where $\bar X<1$, to $\bar\lambda\wedge\langle h,\bar\nu_t\rangle$ where $\bar X=1$, and to $\langle h,\bar\nu_t\rangle$ where $\bar X>1$ (3.12);
4. if moreover $\bar\nu_0$ is absolutely continuous, so is every $\bar\nu_t$.

Milestones

• Remark 4.3, (4.4): integration by parts for the entry term of (4.3).
• (4.55): the integrated hazard in closed form, $\psi_h(x,t)=(1-G(x))/(1-G(x-t))$ or $1-G(x)$.
• Theorem 4.1: for a Radon-measure-valued path satisfying the hazard bound (4.1), the age equation (4.2), which is (3.5) with an arbitrary Radon measure $\upsilon_0$ and an arbitrary $Z$ of bounded variation in place of $\bar\nu_0$ and $\bar K$, holds if and only if the representation (4.3) holds.
• Proof of Corollary 4.4: $\bar K$ is nondecreasing.
• Corollary 4.4, (4.5): $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\int\frac{G(x+t)-G(x)}{1-G(x)}\bar\nu_0(dx)+\int_0^tg(t-s)\bar K(s)ds$.
• Lemma 4.5: $\|\langle f,\bar\nu^2_s\rangle-\langle f,\bar\nu^1_s\rangle\|_T\le\|f\|_M|\Delta\upsilon_0|_{TV}+(2\|f\|_T+\|f'\|_T)\|\Delta Z\|_T$.
• Theorem 4.6: with equal initial measures, $\|\Delta\bar K\|_T\vee\|\Delta\bar D\|_T\le|\Delta\bar X(0)|+\|\Delta\bar E\|_T$, together with (4.8) and (4.10).

Significance

Uniqueness of the fluid solution is what turns tightness of the scaled $N$-server processes into convergence: every subsequential limit solves the fluid equations, so all coincide (the paper's Theorem 3.7). The representation (3.11) reduces the measure-valued equation to the scalar process $\bar K$, and the continuity estimate of Theorem 4.6 says the fluid solution is a Lipschitz function of the arrival process. Both are used in the paper's study of long-time behaviour, where $\bar\nu_t$ converges to the measure with density $1-G$, and (3.12) is the form of the entry rate used there.

The results are proved in the paper. None of them, and no part of the measure-valued fluid model, has a machine-checked proof. Formalizing them produces a checked weak-solution theory for a transport equation with an unbounded killing rate and a measure-valued boundary input, which is a reusable piece of infrastructure for other age- and residual-time-based queueing models.

Difficulty

The central step is Theorem 4.1. The naive approach treats (4.2) as a first-order PDE and integrates along characteristics, but the solution is only a càdlàg path of measures, $h$ is merely locally integrable and blows up near $M$, and $Z$ may jump, so classical characteristics are not available; the test functions must not vanish on the boundary $x=0$, since that is where the entry term lives. The second difficulty is in Theorem 4.6: the entry process $\bar K$ is defined implicitly through the nonidling condition, and comparing two solutions requires a first-crossing argument that distinguishes whether the system is below, at or above capacity at that time.

Formalization scope

The service law is its density $g$ (ServiceLaw), with $g=0$ below $0$, $\int g=1$ and mean one. Time is $\mathbb R$ read on $[0,\infty)$; every condition is stated for $t\ge0$. Measures of the fluid model are FiniteMeasure ℝ carried by $[0,M)$, whose topology is weak convergence, so càdlàg paths are càdlàg in $\mathcal M_F[0,M)$ with the weak topology. The paths of Theorem 4.1 and Lemma 4.5 are ℝ → Measure ℝ with values Radon on $[0,M)$ (possibly infinite) and càdlàg in the vague topology. $M\in[0,\infty]$ is an extended number. The integral in (3.4) is a lower integral in $[0,\infty]$, and $\bar D$, $\bar K$ are its real value. $d\bar K$ is the Lebesgue–Stieltjes measure of $\bar K$, with no atom at $0$. A function $Z$ of bounded variation is a difference $Z_1-Z_2$ of nondecreasing càdlàg functions vanishing at $0$.

Explicit choices: compact support of test functions is relative to $[0,M)\times\mathbb R_+$, so $\varphi(0,s)$ need not vanish (with supports taken in $\mathbb R^2$ the entry term of (3.5) would vanish identically); $\bar\nu(0)=\bar\nu_0$ and $\bar X(0)$ equal to the datum are clauses of the fluid equations, but not of the age equation, where $\upsilon_0$ is arbitrary; functions in $\mathcal C_b(\mathbb R_+)$, $\mathcal C_c(\mathbb R_+)$ and $\mathcal C^1_b(\mathbb R_+)$ are represented by functions on $\mathbb R$ of the same class, of which only values on $[0,\infty)$ are read; norms in Lemma 4.5 are computed in $[0,\infty]$, since $|\Delta\upsilon_0|_{TV}$ may be infinite. Two printed statements are corrected: in Theorem 3.5 the paper's right-hand side of the equivalence lists (3.6) and (3.11); the nonidling condition (3.7), part of the fluid equations on the left, is kept on the right, as the proof requires. In (4.10), $\Delta\bar X(0)$ is replaced by $|\Delta\bar X(0)|$, which is what Lemma 4.5 and (4.9) give.

A fluid solution is defined by the weak transport equation (3.5), never by the representation (3.11) or by a formula for $\bar\nu$ in terms of $\bar K$; with such a definition the equivalence of the goal would be an unfolding of definitions.

A complete development needs Lebesgue–Stieltjes integration by parts for càdlàg functions of bounded variation, the Riesz description of the vague topology, and uniqueness for weak solutions of transport equations; these are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 3.5 separately, are welcome. The paper's Section 4.3 machinery (the abstract and simplified age equations, Lemmas 4.12–4.13, Propositions 4.15–4.16) is not posed here and may be formalized as supporting lemmas.

Selected references

• H. Kaspi and K. Ramanan, Law of large numbers limits for many-server queues, Ann. Appl. Probab. 21(1) (2011), 33–114. https://doi.org/10.1214/09-AAP662
• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6) (2009), 2211–2269. https://doi.org/10.1214/09-AAP609
• W. Whitt, Fluid models for multiserver queues with abandonments, Oper. Res. 54(1) (2006), 37–54. https://doi.org/10.1287/opre.1050.0227
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

Motivation

Robust dynamic programming replaces the single transition law of a Markov decision process by a set of laws, and values a policy by its worst-case expected reward over that set. Iyengar (Robust dynamic programming, CORC Tech Report TR-2002-07, 2004; Math. Oper. Res. 30(2), 2005) and Nilim and El Ghaoui (Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5), 2005) showed that under a rectangularity assumption the robust value satisfies a robust Bellman equation. Each step of that equation solves, for every state–action pair, an inner problem

$$\inf_{p\in\mathcal P}\ \mathbf E^p[v],$$

the worst-case expectation of a value vector $v$ over the ambiguity set $\mathcal P$. Robust value iteration is only as practical as this inner problem is cheap.

The ambiguity sets of interest come from statistics: when transition probabilities are estimated from data, natural sets are confidence regions around the empirical distribution. Section 4 of Iyengar's report studies three such families: relative-entropy balls (Lemma 4), a χ² approximation of them (Lemma 5), and an $L_1$ outer approximation (Lemma 6). This mission formalizes the χ² case. The relative-entropy case is already posed on the platform as RobustMDP.EntropyInner.kl_ball_inner_problem_dual (Nilim–El Ghaoui series), up to the sign change $v\to -v$.

Setting

Let $\mathcal S$ be a finite set of states and let $\mathcal M(\mathcal S)=\{p:\mathcal S\to\mathbb R:\ p\ge 0,\ \sum_s p(s)=1\}$ be the probability measures on $\mathcal S$. For $p\in\mathcal M(\mathcal S)$ and $x:\mathcal S\to\mathbb R$ write

$$\mathbf E^p[x]=\sum_{s}p(s)x(s),\qquad \mathbf{Var}^q[x]=\sum_s q(s)\big(x(s)-\mathbf E^q[x]\big)^2 .$$

Fix a centre $q\in\mathcal M(\mathcal S)$ with $q(s)>0$ for every $s$ (in the paper $q$ is the empirical next-state distribution of one state–action pair) and a radius $t\ge 0$. The χ² set (46) is

$$\mathcal P=\Big\{p\in\mathcal M(\mathcal S):\ \sum_{s\in\mathcal S}\frac{(p(s)-q(s))^2}{q(s)}\le t\Big\}.$$

Since $\log(1+x)\le x$, the relative entropy $D(p\|q)=\sum_s p(s)\log(p(s)/q(s))$ is at most the χ² distance, so $\mathcal P$ lies inside the relative-entropy ball of radius $t$: it is a conservative approximation of it. The Lean development names these objects expect, variance, chiSqDist, chiSqSet, relEntropy and the dual objective dualObj q t v μ $=\mathbf E^q[v-\mu]-\sqrt{t\,\mathbf{Var}^q[v-\mu]}$, all in the namespace RobustDP.ChiSquare.

Formalization targets

Goal: Lemma 5 (p. 18)

For every value vector $v:\mathcal S\to\mathbb R$,

$$\min_{p\in\mathcal P}\ \mathbf E^p[v]\;=\;\max_{\mu\ge 0}\Big\{\mathbf E^q[v-\mu]-\sqrt{t\,\mathbf{Var}^q[v-\mu]}\Big\},$$

where $\mu$ ranges over vectors $\mu:\mathcal S\to\mathbb R$ with $\mu\ge 0$ componentwise. Both extrema are attained. The lemma's complexity claim, $\mathcal O(|\mathcal S|\log|\mathcal S|)$ for (48), is a statement about an algorithm and is not part of the mission.

Milestones (the steps of the paper's proof)

1. (49) With $y=p-q$, the value of the primal problem is $\mathbf E^q[v]$ plus the minimum of $\sum_s y(s)v(s)$ over $\sum_s y(s)^2/q(s)\le t$, $\sum_s y(s)=0$, $y\ge -q$.
2. (50) For fixed multipliers $\mu$ and $\gamma\in\mathbb R$, the minimum of the Lagrangian over the ellipsoid $\{y:\sum_s y(s)^2/q(s)\le t\}$ is $\mathbf E^q[v-\mu]-\sqrt{t\sum_s q(s)(v(s)-\mu(s)-\gamma)^2}$, attained at an explicit $y^*$.
3. (51) Maximizing over $\gamma$ replaces the sum of squares by $\mathbf{Var}^q[v-\mu]$, attained at $\gamma=\mathbf E^q[v-\mu]$.
4. (52)–(53) Some optimal multiplier has the form $\mu^*(s)=(v(s)-\alpha)^+$ with $\alpha\ge\min_s v(s)$, so the dual is a one-dimensional problem.

Two further results stand on the same definitions: the inequality $D(p\|q)\le\sum_s(p(s)-q(s))^2/q(s)$ of Section 4.2, and the $L_1$ analogue of Lemma 5 established in the proof of Lemma 6 (p. 20):

$$\min_{\substack{p\in\mathcal M(\mathcal S)\\ \|p-q\|_1\le c}}\mathbf E^p[v]=\max_{\mu\ge0}\Big\{\mathbf E^q[v-\mu]-\tfrac12 c\big(\max_s(v-\mu)(s)-\min_s(v-\mu)(s)\big)\Big\},\qquad c=\sqrt{2\ln(2)\,t}.$$

Significance

The result. Lemma 5 reduces a worst-case expectation over a curved convex set of probability vectors to a concave problem in one scalar, which the paper solves by sorting. This makes robust value iteration with χ² ambiguity sets about as expensive as nominal value iteration, up to a logarithmic factor. The identity also explains the shape of the answer: a mean minus a standard-deviation penalty, applied to a value vector truncated from above at the level $\alpha$. The truncation comes from the constraint $p\ge 0$.

Formalizing it. The result is proved in the paper; no machine-checked proof is known. A complete formalization gives a verified finite-dimensional duality theorem for a quadratic constraint combined with polyhedral constraints, which is the computational core of χ²-ambiguity robust MDPs and of χ²-divergence distributionally robust optimization in general. Lemma 6's printed formula (57) is false (see below); the mission poses the corrected identity that the paper's proof establishes.

Difficulty

The obvious argument drops the constraint $p\ge 0$. Without it, the minimum of the linear function $\mathbf E^p[v]$ over the ellipsoid $\{\sum_s p(s)=1,\ \chi^2(p,q)\le t\}$ follows from Cauchy–Schwarz and equals $\mathbf E^q[v]-\sqrt{t\,\mathbf{Var}^q[v]}$. The page notes (p. 19) that earlier work solved only this relaxed problem. With $p\ge 0$ the minimizer of the relaxation can leave the simplex, so the problem has an ellipsoidal constraint, a polyhedral constraint and an equality at once. The multiplier $\mu$ of $p\ge 0$ is what Lemma 5 has to handle. Equality of the primal minimum with the dual supremum needs a duality theorem that is not in Mathlib in this form. Attainment of the dual maximum over the unbounded cone $\mu\ge 0$ needs an additional argument, namely that an optimal multiplier has the truncation form (53).

Formalization scope

• $\mathcal S$ is a Fintype; vectors are functions S → ℝ; $\mathcal M(\mathcal S)$ is Mathlib's stdSimplex ℝ S. Nonemptiness of $\mathcal S$ follows from $\sum_s q(s)=1$. Finiteness is the standing restriction of Section 4 (p. 15).
• $q(s)>0$ for every $s$ is a hypothesis of every χ² statement. The page divides by $q(s)$; in Lean $x/0=0$ would silently drop a coordinate from the constraint.
• $t\ge 0$ is assumed. The page puts no sign condition on $t$. At $t=0$ the set is $\{q\}$ and both sides equal $\mathbf E^q[v]$.
• Minimum and maximum are IsLeast and IsGreatest of image sets, so the goal asserts attainment on both sides, as the page's "minimize" and "max" do.
• $\mu\ge 0$ is a vector inequality (0 ≤ μ). The multiplier $\gamma$ of the equality $\sum_s y(s)=0$ ranges over $\mathbb R$. The page's "$\gamma\ge 0$" in (50) is a misprint: the proof of Lemma 6 writes $\gamma\in\mathbb R$, and the optimal $\gamma=\mathbf E^q[v-\mu]$ may be negative.
• The relative entropy uses the natural logarithm, as in (35), with $0\log 0=0$.
• Lemma 6 is posed only as established in its proof. The printed (57) is false: taking $\mu=v-\min_s v(s)$ makes the bracket vanish, so (57) always equals $\mathbf E^q[v]$. For $q=(\frac12,\frac12)$, $v=(0,1)$ and $c=\frac12$ the true minimum is $\frac14$. The set (55) is also restricted to $p\in\mathcal M(\mathcal S)$, which its proof uses.
• Ruled out: a formalization of Lemma 5 whose feasible set omits $p\ge 0$ (or that takes $\mu=0$) states the easier relaxed identity above and is not this mission's goal. Likewise a χ² set whose centre may vanish, or a dual written as ⨆ over an unbounded set, would make the statement junk.
• All complexity claims (Lemmas 5 and 6, the sorting argument, (54)) are excluded. So are the Pinsker step of Section 4.3, whose constant $1/(2\ln 2)$ is wrong for the natural logarithm, and the asymptotic confidence statements (33)–(39).
• Reusable infrastructure: Lagrangian duality for a linear objective over an ellipsoid intersected with a polyhedron, and Cauchy–Schwarz minimization of a linear function over a weighted ellipsoid. Proofs of the milestones, alternative proofs of the goal, and a formalization of the paper's sorting algorithm on top of (52)–(53) are welcome.

Selected references

• G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, IEOR Department, Columbia University, revised May 4, 2004; published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991. https://doi.org/10.1002/0471200611

Motivation

The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a $1/e$ fraction, then take the first item better than everything seen) selects the best item with probability about $1/e$, and no rule does better. Many allocation problems are not single-choice: a seller with $k$ identical goods facing bidders who arrive over time, an advertiser with a budget of $k$ impressions, an employer with $k$ openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when $k$ selections are allowed?

Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least $(1 - 5/\sqrt k)$ times the sum of the $k$ largest values, so the ratio tends to $1$ as $k$ grows, and stated a matching $1 - \Omega(\sqrt{1/k})$ upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling $k$ identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).

Timeline. Dynkin (1963) and the classical literature settle $k = 1$ with ratio $1/e$. Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves $1 - O(1/\sqrt k)$ for $k$ selections, with the explicit constant $5$. Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.

Setting

Let $S$ be a finite set of $n$ distinct non-negative real numbers. The elements of $S$ are revealed in a uniformly random order: each of the $n!$ orders has probability $1/n!$. After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most $k \ge 1$ elements may be selected. Write $T$ for the set of the $k$ largest elements of $S$ (all of $S$ if $k > n$) and

$$v = \sum_{x \in T} x$$

for their sum, the best total any rule could collect knowing $S$ in advance.

Kleinberg's algorithm $\mathcal A_k$ is defined by recursion on $k$:

1. If $k = 1$, use the classical rule: observe the first $\lfloor n/e \rfloor$ arrivals, then select the first later arrival that exceeds all earlier ones, if there is one.
2. If $k \ge 2$, draw $m$ from the binomial distribution $B(n, 1/2)$. Apply $\mathcal A_\ell$, with $\ell = \lfloor k/2 \rfloor$, to the first $m$ arrivals. Let $y_1 > y_2 > \dots > y_m$ be those $m$ values in decreasing order. After the $m$-th arrival, select every arrival exceeding $y_\ell$, until $k$ elements have been selected in total or the sequence ends.

The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.

Formalization targets

Goal: Theorem 2.1

$$\mathbb E\Big[\sum_{x \text{ selected by } \mathcal A_k} x\Big] \;\ge\; \Big(1 - \frac{5}{\sqrt k}\Big)\, v \qquad \text{for every } S \subset \mathbb R_{\ge 0} \text{ finite and every } k \ge 1.$$

The statement is uniform in $n$ and $k$; it says nothing beyond the explicit constant $5$ printed in the paper.

Milestones: the claims of the proof sketch

The paper proves the theorem by induction on $k$. Its sketch introduces $Y$, the set of the first $m$ arrivals, $Z = S \setminus Y$, the modified value of a set (the sum of its elements lying in $T$), and $q$, the number of elements of $Z$ exceeding $y_\ell$. The milestones are its stated claims, in order:

1. $Y$ is uniformly distributed on the $2^n$ subsets of $S$.
2. $|Y \cap T|$ has the distribution $B(k, 1/2)$.
3. Conditional on $|Y \cap T| = r$, the expected modified value of $Y$ is $(r/k)v$.
4. The displayed bound $\sum_{r=1}^{k}\Pr(|Y\cap T| = r)\,\frac{\min(r,\ell)}{k}\,v \ge \big(1 - \frac{1}{2\sqrt k}\big)\frac v2$ with $\ell = k/2$.
5. The top $\ell = k/2$ elements of $Y$ have expected modified value at least $\big(1 - \frac{1}{2\sqrt k}\big)\frac v2$.
6. $\mathbb E\,|q - \ell| \le \sqrt k$.
7. The elements the algorithm selects from $Z$ have expected modified value at least $\big(\frac12 - \sqrt{1/k}\big)v$.
8. The closing computation $\big(1 - \frac{5}{\sqrt{k/2}}\big)\big(1 - \frac{1}{2\sqrt k}\big)\frac12 + \frac12 - \sqrt{\frac1k} > 1 - \frac{5}{\sqrt k}$.

Significance

The result. Theorem 2.1 shows that random arrival order costs only a $1 - O(1/\sqrt k)$ factor when many items are sold, against the constant $1/e$ for a single item. With the paper's matching upper bound, it pins down the optimal rate for the $k$-choice problem. It is the base of the paper's strategyproof online auction for $k$ identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.

Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than $\ell$ elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.

Difficulty

The obvious argument fixes $m = n/2$ and treats the threshold $y_\ell$ as if it split the remaining elements exactly. Both steps fail. With a fixed $m$, the first $m$ arrivals are not a uniform subset of $S$ and $|Y \cap T|$ is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of $m$ is what makes $Y$ uniform. And the number $q$ of later elements beyond $y_\ell$ fluctuates by order $\sqrt k$: the second phase may run out of budget before reaching all of $T \cap Z$, or accept elements outside $T$. Controlling this fluctuation, while the cap of $k$ also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.

Formalization scope

The Lean development fixes these conventions.

• $S$ is a Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time $t$ (0-based) under the order $\pi \in \mathrm{Perm}(\mathrm{Fin}\, n)$ is the $\pi(t)$-th smallest element of $S$, and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.
• The algorithm is a PMF over sets of selected positions, defined by well-founded recursion on $k$. The base case is the published SecretaryWD.DiscUpper.classicalSecretary. $B(n, 1/2)$ is Mathlib's PMF.binomial (1/2). At $k = 0$ the algorithm selects nothing, for totality only; all statements assume $k \ge 1$.
• When the first phase has seen fewer than $\ell$ arrivals ($m < \ell$), $y_\ell$ is taken to be $-\infty$: every later arrival is selected until the cap. The page does not specify this case; under the reading "select nothing", the theorem fails when $n$ is much smaller than $k$.
• The cap of $k$ counts the selections of both phases. A cap applied to the second phase alone would let the algorithm select up to $k + \ell$ elements and is excluded.
• The goal mentions only the algorithm, the order, $S$, $k$ and $v$. It does not mention $Y$, $Z$, $q$ or the modified value, which appear only in milestones, so the goal cannot be discharged by assuming any part of the sketch.
• Three milestone hypotheses are added and disclosed: $k \le n$ for milestones 2, 3, 5 and 6 (for $n < k$ the law of $|Y \cap T|$ is $B(n, 1/2)$, and milestone 6 fails); $k$ even for milestone 5 (the sketch writes $\ell = k/2$; for odd $k$ with $\ell = \lfloor k/2\rfloor$ the bound fails at $k = 3$). Milestone 4 uses the real number $\ell = k/2$, as printed; with $\lfloor k/2\rfloor$ it fails for odd $k$.

A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.

Selected references

• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, Proceedings of the 16th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2005.
• M. T. Hajiaghayi, R. Kleinberg, D. C. Parkes, Adaptive limited-supply online auctions, Proceedings of the 5th ACM Conference on Electronic Commerce (EC), 2004, pp. 71–80. https://doi.org/10.1145/988772.988784
• E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Mathematics Doklady 4, 1963.
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Online auctions and generalized secretary problems, ACM SIGecom Exchanges, 2008. https://doi.org/10.1145/1399589.1399596

Motivation

Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance $\Sigma$; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.

The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value $1 + \gamma^{-1}$, is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.

Timeline:

• 2000, Johansson: equal rates; the geometric and exponential last passage time has the law of the largest Laguerre eigenvalue (his Proposition 1.4 is the case $\pi_1 = \cdots = \pi_N$ of (307)).
• 2001, Baryshnikov and, independently, Gravner, Tracy and Widom: the tandem-queue and GUE-minor descriptions of the same object.
• 2005, Baik, Ben Arous and Péché: row-dependent rates $\pi_i$ (Proposition 6.1), via the Robinson–Schensted–Knuth (RSK) formula for geometric weights (310) and a scaling limit.

Setting

Last passage time. Attach a real weight $X(i,j)$ to every site of the grid $\{1,\ldots,N\}\times\{1,\ldots,M\}$. An up/right path from $(1,1)$ to $(N,M)$ is a sequence of $N+M-1$ sites starting at $(1,1)$, ending at $(N,M)$, each step adding $(1,0)$ or $(0,1)$. The last passage time is

$$L(N,M) = \max_{\pi:(1,1)\nearrow(N,M)} \sum_{(i,j)\in\pi} X(i,j). \qquad (306)$$

Exponential environment. Given positive numbers $\pi_1,\ldots,\pi_N$, the $X(i,j)$ are independent and $X(i,j)$ is exponential of mean $1/(\pi_iM)$, i.e. density $\pi_iMe^{-\pi_iMx}$ on $x\ge0$. All $M$ sites of row $i$ share one rate.

Sample covariance matrix. Let $g_{kj}$, $1\le k\le M$, $1\le j\le N$, be independent standard complex Gaussians (real and imaginary parts independent $N(0,1/2)$). For a unitary $U$ and $\ell_j = \pi_j^{-1}$ (308), the samples $\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_j})\,g_k$ are mean-zero complex Gaussian vectors with covariance $\Sigma = U\,\mathrm{diag}(\ell)\,U^*$, and

$$S = \frac1M\sum_{k=1}^M \vec y_k\vec y_k^{\,*}, \qquad \lambda_1 = \text{largest eigenvalue of } S.$$

Schur functions and geometric weights. For a partition $\lambda$, the Schur function $s_\lambda(x)$ is the sum over semistandard Young tableaux $T$ of shape $\lambda$ of $\prod_{c}x_{T(c)}$. A geometric variable of parameter $q\in[0,1)$ has $\mathbb P(Y = k) = (1-q)q^k$.

Formalization targets

Goal: Proposition 6.1

For $1\le N\le M$, positive $\pi_1,\ldots,\pi_N$ and every unitary $U$,

$$\mathbb P\big(L(N,M)\le x\big) = \mathbb P\big(\lambda_1(M,N)\le x\big) \qquad \text{for all } x\in\mathbb R. \qquad (309)$$

The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.

Milestones

1. The recurrence (313): for every array of weights and every site with $a, b\ge2$,

$$L(a,b) = \max\{L(a-1,b), L(a,b-1)\} + X(a,b).$$

2. The Cauchy identity (311): $\sum_\lambda s_\lambda(x)s_\lambda(y) = \prod_{i,j}(1-x_iy_j)^{-1}$ for $x_i,y_j\ge0$, $x_iy_j<1$.
3. The geometric formula (310): for independent geometric weights $Y(i,j)$ of parameter $x_iy_j$, $x_i,y_j\in[0,1)$,

$$\mathbb P\big(G(N,M)\le n\big) = \prod_{i,j}(1-x_iy_j)\sum_{\lambda:\lambda_1\le n}s_\lambda(x)s_\lambda(y).$$

4. The exponential formula (307): for $M\ge N$ and distinct $\pi_i$,

$$\mathbb P\big(L(N,M)\le x\big) = \frac1C\int_{[0,x]^N}\frac{\det(e^{-M\pi_i\xi_j})}{V(\pi)}V(\xi)\prod_{j}\xi_j^{M-N}\,d\xi.$$

Significance

The proposition makes every distributional statement about $\lambda_1$ in the paper a statement about last passage percolation with row-dependent rates: the $F_k$ (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of $M$ customers from $N$ exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.

These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.

Difficulty

The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit $x_i = 1 - M\pi_i/L$, $n = xL$, $L\to\infty$, in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general $\Sigma$, which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.

Formalization scope

The development lives in the namespace SpikedWishart.LastPassage. Conventions:

• Sites and indices are 0-based; the paper's $(1,1)$ and $(N,M)$ are $(0,0)$ and $(N-1,M-1)$, and $N, M\ge1$.
• $L$ is defined as the maximum over paths (306), never by the recurrence (313), so (313) is a genuine statement.
• The exponential law is Mathlib's expMeasure with rate $\pi_iM$.
• The sample model is mean zero, uncentred, with factor $1/M$ and $\mathbb E|g|^2 = 1$; this is the model of (59), (61) and (307), and the page's centring by the sample mean and $S = (1/N)XX^*$ are printed slips. The covariance is $U\,\mathrm{diag}(\pi^{-1})U^*$ for every unitary $U$; specialising to diagonal $\Sigma$ would prove a special case.
• $N\le M$ is a disclosed addition to the goal, matching the page's "for $M\ge N$" in (307).
• Proposition 6.1 prints $L(M,N)$; the object is (306)'s $L(N,M)$.
• Schur functions are the tableau sum with variables extended by zero. The Cauchy identity is stated with the exponent $-1$ that the page omits. In (307) the constant $C$ is the integral of the same integrand over $(0,\infty)^N$, and the $\pi_i$ are distinct so that $V(\pi)\ne0$; the goal has no distinctness hypothesis.

A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of $\lambda_1$.

Selected references

• J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5):1643–1697, 2005. https://doi.org/10.1214/009117905000000233
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209:437–476, 2000. https://doi.org/10.1007/s002200050027
• Y. Baryshnikov, GUEs and queues, Probab. Theory Related Fields 119:256–274, 2001. https://doi.org/10.1007/PL00008760
• J. Gravner, C. A. Tracy, H. Widom, Limit theorems for height fluctuations in a class of discrete space and time growth models, J. Stat. Phys. 102:1085–1132, 2001. https://doi.org/10.1023/A:1004879725949
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Cambridge University Press, 1999 (the paper's reference [36] for the Cauchy identity). https://doi.org/10.1017/CBO9780511609589

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.

Setting

A finite game has a finite set of players $\mathcal M$; each player $m$ has a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements, and a utility $u^m : E \to \mathbb R$ on the set of strategy profiles $E = \prod_m E^m$. For a profile $p$, $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$.

A profile $p$ is an $\epsilon$-equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m}) - \epsilon$ for every player $m$ and strategy $q^m$ (equation (2) of the paper). A game is a potential game if there is $\varphi : E \to \mathbb R$ with $\varphi(p^m, p^{-m}) - \varphi(q^m, p^{-m}) = u^m(p^m, p^{-m}) - u^m(q^m, p^{-m})$ for all $m$, $p^m$, $q^m$, $p^{-m}$ (Definition 2.1).

A game is identified with its tuple of utilities, an element of $C_0^M$ where $C_0 = \{f : E \to \mathbb R\}$. The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator $D_m$ sends $u^m$ to its differences along the edges where player $m$ deviates, $D = \sum_m D_m$, $\delta_0$ is the gradient of the game graph, $\Pi_m = D_m^\dagger D_m$, and $\dagger$ is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces

$$\mathcal P = \{u = \Pi u,\ Du \in \operatorname{im}\delta_0\},\qquad \mathcal H = \{u = \Pi u,\ Du \in \ker\delta_0^*\},\qquad \mathcal N = \ker D ,$$

and a harmonic game is a game in $\mathcal H \oplus \mathcal N$.

Section 6 introduces the weighted inner product and norm

$$\langle G, \hat G\rangle_{M,E} = \sum_{m} h_m \sum_{p \in E} u^m(p)\,\hat u^m(p), \qquad \|G\|_{M,E}^2 = \langle G, G\rangle_{M,E} .$$

A closest potential game to $G$ is a potential game $\hat G$ with $\|G - \hat G\|_{M,E} \le \|G - G'\|_{M,E}$ for every potential game $G'$; a closest harmonic game is defined in the same way.

Formalization targets

Goal: Theorem 6.3

Let $\hat G$ be the closest potential game to $G$ and $\alpha = \|G - \hat G\|_{M,E}$. Then for every $\epsilon_1$, every $\epsilon_1$-equilibrium of $\hat G$ is an $\epsilon$-equilibrium of $G$, and every $\epsilon_1$-equilibrium of $G$ is an $\epsilon$-equilibrium of $\hat G$, where

$$\epsilon = \max_{m \in \mathcal M} \frac{2\alpha}{\sqrt{h_m}} + \epsilon_1 .$$

Milestones

1. Lemma 2.1. If $|u^m(p) - \hat u^m(p)| \le \epsilon_0$ for all $m$ and $p$, every $\epsilon_1$-equilibrium of one game is a $(2\epsilon_0 + \epsilon_1)$-equilibrium of the other.
2. Theorem 5.1. The set of potential games is the subspace $\mathcal P \oplus \mathcal N$.
3. Theorem 6.1. Under $\langle\cdot,\cdot\rangle_{M,E}$ the subspaces $\mathcal P$, $\mathcal H$, $\mathcal N$ are pairwise orthogonal.
4. Theorem 6.2. With $\varphi = \delta_0^\dagger D u$, the closest potential game to $G$ has utilities $\Pi_m \varphi + (I - \Pi_m)u^m$, and the closest harmonic game has utilities $u^m - \Pi_m\varphi$.

Significance

The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.

Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections $\Pi_m$), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for $\epsilon$-equilibria.

Difficulty

Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into $\mathcal P$, $\mathcal H$, $\mathcal N$) and properties of pseudoinverses of the operators $D_m$ and $\delta_0$ that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality $\mathcal P \perp \mathcal H$ under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the $h_m$ differ, so the standard orthogonal-complement machinery cannot be applied to $C_0^M$ with its default inner product.

Formalization scope

Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product $\tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$ of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.

Hypotheses made explicit: every strategy set is nonempty (the paper's $E^m = \{1,\dots,h_m\}$), so $h_m \ge 1$; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an $\epsilon$-equilibrium for some $\epsilon \le B$" is stated as "a $B$-equilibrium", which is equivalent because (2) is monotone in $\epsilon$. Both directions of Lemma 2.1 and Theorem 6.3 are included.

The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance $\alpha$ would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.

Contributions welcome: the Penrose identities for the pseudoinverse, the identities $D^\dagger D = \Pi$ and $\Delta_{0,m} = h_m \Pi_m$, and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Math. Oper. Res. 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games Econ. Behav. 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044