Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.996001Formalized record

3 provers on it4 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.999074Formalized record

3 provers on it4 of 4 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.996001Formalized record

3 provers on it4 of 4 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.103205334138Formalized record≤ 2Open frontier

7 provers on it7 of 8 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 80Formalized record

3 provers on it7 of 7 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

35 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Convex Optimization Numerical Analysis Partial Differential Equations·Captain: mikedeng1

Mean Field Games: Numerical Methods for the Planning Problem II: Solutions of the Penalized Scheme Converge to a Solution of the Discrete Planning Scheme as ε → 0Research Paper

Motivation

Mean field games (MFG), introduced by Lasry and Lions and by Huang, Caines and Malhamé, describe Nash equilibria of very large populations of identical rational agents. The equilibrium is a coupled system: a backward Hamilton–Jacobi–Bellman equation for the value function $u$ of a representative agent and a forward Fokker–Planck equation for the density $m$ of the population. In the planning problem, proposed by P.-L. Lions, both the initial density $m_0$ and the final density $m_T$ are prescribed, and one asks for a cost structure under which the population moves from one to the other. This is a mean field analogue of optimal transport.

Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, SIAM J. Control Optim. 2012) propose finite-difference schemes for the planning problem. Mission I of this series treats the existence of a solution of the discrete planning scheme. Since the two boundary conditions on $m$ make the discrete system hard to solve directly, the paper also introduces a penalized scheme, in which the initial condition $M^0 = m_0$ is replaced by a penalty $U^0 = (M^0 - m_0)/\varepsilon$ ; for each $\varepsilon > 0$ this is a standard discrete MFG system with a unique solution. This mission formalizes the paper's §3.2: the penalized solutions converge, as $\varepsilon \to 0$ , to a solution of the planning scheme.

Setting

Fix integers $N_h \ge 1$ , $N_T \ge 1$ , a horizon $T > 0$ and a viscosity $\nu \ge 0$ ; put $h = 1/N_h$ and $\Delta t = T/N_T$ . The grid $\mathbb T^2_h$ consists of the points $x_{i,j}$ , $(i,j) \in (\mathbb Z/N_h\mathbb Z)^2$ (periodic indices). A grid function is a real function on $\mathbb T^2_h$ ; time levels are $n = 0, \dots, N_T$ .

$(D_1^+U)_{i,j} = (U_{i+1,j} - U_{i,j})/h$ , $(D_2^+U)_{i,j} = (U_{i,j+1} - U_{i,j})/h$ , and the discrete gradient is $[D_hU]_{i,j} = ((D_1^+U)_{i,j}, (D_1^+U)_{i-1,j}, (D_2^+U)_{i,j}, (D_2^+U)_{i,j-1}) \in \mathbb R^4$ .
$\Delta_h$ is the five-point Laplacian.
A numerical Hamiltonian $g(x_{i,j}, q)$ , $q \in \mathbb R^4$ , is monotone (G1), $C^1$ (G3), convex (G4) and coercive (G5) in $q$ .
$\mathcal B_{i,j}(U, M)$ is the discrete transport term $\mathrm{div}_h\big(M\,\nabla_q g(\cdot, [D_hU])\big)$ .
$W : \mathbb R \to \mathbb R$ is strictly convex, superlinear and $C^2$ , with $V = W'$ (hypothesis (24)).
$\mathcal K = \{M \ge 0 : h^2\sum_{i,j} M_{i,j} = 1\}$ is the set of discrete probability densities, and $m_0, m_T \in \mathcal K$ with $m_0 > 0$ .

The planning scheme (18) asks for families $(U^n, M^n)$ with, for $n < N_T$ ,

\frac{U^{n+1} - U^n}{\Delta t} - \nu\Delta_hU^{n+1} + g(x, [D_hU^{n+1}]) = V(M^n), \qquad \frac{M^{n+1} - M^n}{\Delta t} + \nu\Delta_hM^n + \mathcal B(U^{n+1}, M^n) = 0,

$M^n \in \mathcal K$ , $M^0 = m_0$ and $M^{N_T} = m_T$ . The penalized scheme (20)–(23) has the same two equations, $M^n \in \mathcal K$ for $n < N_T$ , $M^{N_T} = m_T$ , and $U^0 = (M^0 - m_0)/\varepsilon$ in place of $M^0 = m_0$ .

Formalization targets

Goal: Proposition 4

Under the hypotheses of Theorem 1, for every sequence $\varepsilon_k \downarrow 0$ , every choice of penalized solutions $(U^{\varepsilon_k}, M^{\varepsilon_k})$ , and every limit $M^{\varepsilon_k} \to M$ in $\mathcal K^{N_T+1}$ ,

\exists\, U,\ \text{a subsequence with } U^{\varepsilon_k} \to U, \quad (U, M) \text{ solves (43)–(46)}.

If $g$ is strictly convex, the whole sequence $(U^{\varepsilon_k}, M^{\varepsilon_k})$ converges to the unique solution of (43)–(46) with $\sum_{i,j} U^0_{i,j} = 0$ .

Milestones

(13): (G5) implies $\max_{i,j} g(x_{i,j}, [D_hU]_{i,j}) / \|[D_hU]\|_\infty \to +\infty$ .
Theorem 2: the penalized control problem (50), $\min \Theta^*(M,Z) + \frac{1}{2\varepsilon\Delta t}\sum(M^0 - m_0)^2$ under the discrete Fokker–Planck constraint, has a minimizer whose optimality system is (20)–(23).
Proposition 2: $\max_{i,j}|M^{\varepsilon,0}_{i,j} - (m_0)_{i,j}| \le C\varepsilon^{1/2}$ .
Proposition 3: $\max_{n,i,j}|U^{\varepsilon,n}_{i,j}| \le C$ .
Corollary 1: $\max_{i,j}|M^{\varepsilon,0}_{i,j} - (m_0)_{i,j}| \le C\varepsilon$ .
Proposition 1: uniqueness of $M$ for (18), and of $U$ normalized by $\sum U^0 = 0$ when $g$ is strictly convex.

In 3–5 the constant $C$ depends on $h$ , $\Delta t$ and the data, never on $\varepsilon$ .

Significance

Proposition 4 justifies the penalized scheme as a way to compute solutions of the discrete planning problem. The penalized system has a standard initial–terminal structure that Newton's method (the paper's §4) handles well. The planning system does not, because it prescribes two conditions on $M$ and none on $U$ . The estimates of Propositions 2–3 and Corollary 1 also give a rate: the initial mismatch of the penalized density is $O(\varepsilon)$ .

The results are proved in the paper. None of them has been machine-checked: the platform holds no formalization of mean field games, of their finite-difference schemes, or of the Lasry–Lions monotonicity argument. A complete development would yield a reusable library of the monotone finite-difference operators on the discrete torus, a formal Lasry–Lions uniqueness argument for discrete MFG systems, and a template for compactness-plus-uniqueness convergence proofs in finite dimension.

Difficulty

Compactness of the densities is free, since $\mathcal K^{N_T+1}$ is compact. Passing to the limit in the scheme needs only continuity of $g$ , $\nabla_q g$ and $V$ . The substance lies in the two uniform estimates.

Bounding $U^\varepsilon$ uniformly in $\varepsilon$ (Proposition 3) is the central difficulty. The initial condition $U^{\varepsilon,0} = (M^{\varepsilon,0} - m_0)/\varepsilon$ involves division by $\varepsilon$ , so the obvious bound $|U^{\varepsilon,0}| \le 2/(h^2\varepsilon)$ blows up. The comparison principle for the discrete HJB equation, which is the natural first idea, cannot repair this: it propagates whatever bound $U^0$ has. The HJB equation alone does not bound $U^\varepsilon$ ; the coupling with the Fokker–Planck equation, the coercivity (13), and a lower bound on $M^{\varepsilon,0}$ that is uniform in $\varepsilon$ (which is where Proposition 2 enters) all have to be used.
Proposition 2 compares the penalized problem with the planning problem through the convex duality of Theorem 2. It therefore needs a solution of the planning scheme, which is mission I's goal.
Proposition 1 needs the discrete Lasry–Lions identity, a summation by parts across the coupled system.

Formalization scope

All objects live in the namespace MFGPlanning.Penalized.

Grid points are ZMod Nh × ZMod Nh (periodicity is built in), time levels are Fin (NT + 1), and the four momentum components $q_1, \dots, q_4$ are Fin 4 indices 0, …, 3.
The data structure carries $N_h, N_T \ge 1$ , $T > 0$ and $\nu \ge 0$ .
$g$ is given only at the grid points. (G2), which only defines the continuous Hamiltonian, is not encoded.
"Coercive" in (24) is read as superlinear.
$V_h[M] = V(M_{i,j})$ , as (24) prescribes.
$\Theta^*$ and $(W+\chi)^*$ take values in EReal, so unbounded suprema are $+\infty$ .
Convergence is in the product topology, which on these finite-dimensional spaces is $\max_n \|\cdot\|_\infty$ convergence.
"The unique solution" of (43)–(46) means unique under the normalization $\sum_{i,j} U^0_{i,j} = 0$ , because $U$ is otherwise determined only up to a constant.

Three trivializing formalizations are ruled out. The constants in Propositions 2–3 and Corollary 1 are quantified before $\varepsilon$ and before the solution. The goal quantifies over every sequence $\varepsilon_k \to 0$ and assumes no convergence of $U$ and no limit solution. Its part 2 does not assume convergence of $M$ .

The existence of a solution of the planning scheme (Theorem 1) is posed in mission I and not restated here. A solver of Proposition 2 will need it once mission I's goal is proved. The existence and uniqueness of solutions of (20)–(23) are quoted by the paper from Achdou–Capuzzo-Dolcetta (2010) and are not items. Welcome contributions include discrete summation-by-parts lemmas on the torus, the discrete comparison principle for monotone schemes, and the Poincaré-type inequality $\|W\|_\infty \le c\|[D_hW]\|_\infty$ on zero-mean grid functions.

Selected references

Y. Achdou, F. Camilli, I. Capuzzo-Dolcetta, Mean field games: numerical methods for the planning problem, HAL preprint hal-00465404v1, 2010; SIAM J. Control Optim. 50 (2012). https://hal.science/hal-00465404v1, https://doi.org/10.1137/100790069
Y. Achdou, I. Capuzzo-Dolcetta, Mean field games: numerical methods, SIAM J. Numer. Anal. 48 (2010) 1136–1162. https://doi.org/10.1137/090758477
J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2 (2007) 229–260. https://doi.org/10.1007/s11537-007-0657-8
M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Communications in Information and Systems 6 (2006) 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5

11 thms2 active usersReviewed

Convex Optimization Numerical Analysis Partial Differential Equations·Captain: mikedeng1

Mean Field Games: Numerical Methods for the Planning Problem I: The Discrete Planning Scheme Has a Solution, Given by a Fenchel–Rockafellar Saddle PointResearch Paper

Motivation

Mean field games (Lasry and Lions, 2006–2007; Huang, Malhamé and Caines, 2006) model the limit of a large population of identical rational agents. Each agent solves an optimal control problem whose cost depends on the distribution $m$ of all agents, and the distribution is in turn transported by the agents' optimal feedback. In the continuous setting this gives a coupled system: a backward Hamilton–Jacobi equation for the value function $u$ and a forward Fokker–Planck equation for the density $m$ .

In the usual formulation, $m$ is prescribed at the initial time and $u$ at the final time. The planning problem, introduced by P.-L. Lions in his Collège de France lectures, prescribes instead both the initial density $m_0$ and the final density $m_T$ , and asks for a cost (through $u$ ) that steers the population from one to the other. According to the paper (§1, pp. 2–3), Lions proved existence for the continuous planning problem in mainly two cases: $\nu = 0$ with a smooth, strictly convex, superlinear Hamiltonian; and $\nu > 0$ with $H(p) = c|p|^2$ or close to it. In both cases the coupling is local and the densities are smooth and bounded away from $0$ . Existence for $\nu > 0$ and more general Hamiltonians was then open, and for sublinear $H$ , $m_0\ne m_T$ and short horizons there is no solution.

Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, 2010; SIAM J. Control Optim. 2012) introduced a finite-difference scheme for the planning problem and proved that the discrete system has a solution. The proof writes the scheme as the optimality system of a discrete optimal control problem, a Fokker–Planck equation driven by a control, and obtains a solution from a saddle point given by the Fenchel–Rockafellar duality theorem. This mission formalizes that existence result: Theorem 1 of §3.1 together with the lemmas on which its proof rests.

Setting

Fix integers $N_h, N_T \ge 1$ , a horizon $T > 0$ and a viscosity $\nu \ge 0$ ; let $h = 1/N_h$ and $\Delta t = T/N_T$ . The grid $\mathbb T^2_h$ is the periodic $N_h\times N_h$ grid on the two-dimensional torus, with points $x_{i,j}$ , $(i,j)\in(\mathbb Z/N_h)^2$ . On grid functions $U$ the scheme uses the forward differences $D_1^+$ , $D_2^+$ , the four-component discrete gradient $[D_hU]_{i,j} = ((D_1^+U)_{i,j}, (D_1^+U)_{i-1,j}, (D_2^+U)_{i,j}, (D_2^+U)_{i,j-1})$ , the five-point Laplacian $\Delta_h$ , a discrete divergence $\mathrm{div}_h$ of four-component fields, and the transport operator $\mathcal B(U, M) = \mathrm{div}_h(M\,\nabla_q g(\cdot, [D_hU]))$ .

A numerical Hamiltonian $g(x_{i,j}, q_1,q_2,q_3,q_4)$ is monotone (nonincreasing in $q_1, q_3$ , nondecreasing in $q_2, q_4$ ), $C^1$ , convex, and superlinearly coercive in the directions where monotonicity does not bound it. The coupling is local: $V = W'$ , with $W$ strictly convex, superlinear and $C^2$ . The set $\mathcal K$ consists of the discrete probability densities, $h^2\sum_{i,j}M_{i,j} = 1$ , $M\ge 0$ . The discrete planning scheme (18) asks for $(U^n, M^n)_{0\le n\le N_T}$ with

\frac{U^{n+1}-U^n}{\Delta t} - \nu\Delta_hU^{n+1} + g(x,[D_hU^{n+1}]) = V(M^n),\qquad \frac{M^{n+1}-M^n}{\Delta t} + \nu\Delta_hM^n + \mathcal B(U^{n+1},M^n) = 0,

for $0\le n<N_T$ , with $M^n\in\mathcal K$ , $M^0 = m_0$ and $M^{N_T} = m_T$ .

The duality is set up as follows. With $\chi$ the indicator of $\{m\ge0\}$ , let $\Theta(\alpha,\beta) = \sum_{n,i,j}(W+\chi)^*(\alpha^n_{i,j} + g(x_{i,j},[\beta^n]_{i,j}))$ on dual variables $(\alpha^n,\beta^n)_{1\le n\le N_T}$ . Let $\Lambda(\Psi)$ be the linear map sending $\Psi = (\Psi^n)_{0\le n\le N_T}$ to the discrete Hamilton–Jacobi operator and the discrete gradient of $\Psi^{n+1}$ . Let $\Sigma(\alpha,\beta) = \mathcal F(\Psi)$ if $(\alpha,\beta) = \Lambda(\Psi)$ with $\sum\Psi^0 = 0$ , and $+\infty$ otherwise, where $\mathcal F(\Psi) = \frac1{\Delta t}(\sum m_0\Psi^0 - \sum m_T\Psi^{N_T})$ . The Legendre–Fenchel transforms $\Theta^*$ , $\Sigma^*$ act on primal variables $(M^n, Z^n)_{0\le n<N_T}$ , where $M^n$ is paired with $\alpha^{n+1}$ (Remark 2).

Formalization targets

Goal: Theorem 1

Under (G1), (G3)–(G5), (24), $m_0, m_T\in\mathcal K$ , $m_0 > 0$ , and either $\nu > 0$ or ( $\nu = 0$ and $m_T > 0$ ):

\min_{M,Z}\ \Theta^*(M,Z) + \Sigma^*(-M,-Z) = -\min_{\alpha,\beta}\big(\Theta(\alpha,\beta) + \Sigma(\alpha,\beta)\big)

has a solution $(M,Z)$ , $(\alpha,\beta)$ with a finite common value. Moreover $(\alpha,\beta) = \Lambda(U)$ for some $U$ , and $(U, M)$ , with $M^{N_T} = m_T$ appended, solves the scheme (18), with $Z^{k,n} = M^n\,\partial_{q_k}g(x,[D_hU^{n+1}])$ .

Milestones, in attack order

§3.1, p. 7. $V$ maps $(0,\infty)$ onto $(\lambda,\infty)$ ; $(W+\chi)^*$ is finite, convex, continuous and nondecreasing, with explicit values on and off $\mathcal J_V$ .
Lemma 1. $\Theta$ is convex and continuous, $\Sigma$ is convex and l.s.c., and $\Sigma$ and $\Theta$ are both finite at some point.
Lemma 2. $\Theta^*$ and $\Sigma^*$ are convex and l.s.c., with explicit formulas.
(30). $\Sigma^*(-M,-Z)$ is $0$ on the constraint set of the control problem (26) and $+\infty$ off it.
Lemma 3. If $m_0 > 0$ , some $(M,Z)$ has $\Theta^*$ , $\Sigma^*(-M,-Z)$ finite and $\Theta^*$ finite and continuous near it.
Positivity. A discrete strong maximum principle from the proof of Theorem 1: densities in $\mathcal K$ that solve the discrete Fokker–Planck equation (42) are strictly positive before the final time.

Significance

Theorem 1 is the existence result for the finite-difference planning problem. It is used in the paper's second part (§3.2), where solutions of a penalized scheme, in which the final condition is relaxed into a penalty, are shown to converge to a solution of (18) as the penalty parameter vanishes. The penalized scheme is what is solved numerically. The discrete existence result covers general convex, monotone, coercive numerical Hamiltonians and every $\nu\ge0$ , which includes discretizations of the continuous cases that were still open when the paper was written.

The result has a published proof. What this mission adds is a machine-checked version of it: a complete discrete model of the planning problem (grid, operators, scheme, duality functionals) and the convex-analytic chain that connects it to the Fenchel–Rockafellar theorem. As far as a search of the platform shows, no part of this has been formalized; the series' second mission formalizes the convergence of the penalized scheme on the same model.

Difficulty

Existence for a coupled forward–backward nonlinear system with conditions at both ends of the time interval is not reachable by a fixed-point or time-marching argument: the Hamilton–Jacobi equation runs backward and the Fokker–Planck equation forward, and the final density is imposed rather than computed. The approach goes through duality, and three points are delicate.

All the functionals in the duality take the value $+\infty$ , and Fenchel–Rockafellar needs a qualification condition on each side. Lemma 1 gives it for the dual problem; Lemma 3 gives it for the primal one, and needs $m_0 > 0$ and the coercivity (G5).
The optimality conditions only give a complementarity system: the Hamilton–Jacobi equation holds where $M^n > 0$ and becomes an inequality where $M^n = 0$ . Recovering the scheme (18) needs the strict positivity of $M^n$ , a discrete strong maximum principle. That principle uses the monotonicity (G1) and either diffusion or a positive final density.
The bookkeeping of the time lag between primal and dual variables and of the discrete integration by parts in $\Sigma^*$ must be exact.

Formalization scope

The Lean development lives in the namespace MFGPlanning.Existence. A structure Data carries $N_h, N_T \ge 1$ , $T > 0$ , $\nu\ge0$ , $g$ at the grid points, $W$ , $m_0$ and $m_T$ . Committed conventions:

grid indices are ZMod Nh × ZMod Nh (periodic), and $d = 2$ as in the paper;
the components $q_1,\dots,q_4$ and $Z^1,\dots,Z^4$ are the Fin 4 indices 0..3;
time levels are Fin (NT+1) for $U$ and the scheme, and Fin NT for the duality variables. M k is $M^k$ and α k is $\alpha^{k+1}$ (Remark 2), and Fin.snoc M mT appends $M^{N_T} = m_T$ ;
$(W+\chi)^*$ , $\Theta$ , $\Theta^*$ , $\Sigma$ , $\Sigma^*$ are EReal-valued lattice suprema and infima, so unbounded suprema are $+\infty$ and not a junk value. Convexity of an extended-valued functional is convexity of its epigraph.

Disclosed encodings:

(G2) is not encoded, since it only defines the continuous Hamiltonian;
"coercive" in (24) is read as superlinear growth $W(m)/|m|\to\infty$ , which the paper's own consequence $V((0,\infty)) = (\lambda,\infty)$ requires;
$g$ is given only at grid points;
the optimality conditions (32)–(33) are stated through what Theorem 1 says they are equivalent to: the scheme (18) and the relation (39).

Theorem 1 is not reducible to "the scheme (18) has a solution". The goal also asserts that the primal and dual problems attain their minima, that there is no duality gap with a finite value, and that $(\alpha,\beta) = \Lambda(U)$ . The duality functionals are never real-valued suprema, which would make (30) and (31) hold or fail for junk reasons. A complete development needs finite-dimensional convex analysis on extended-valued functions: conjugates, the Fenchel–Rockafellar theorem with attainment, and subdifferential optimality conditions. These parts are reusable well beyond this mission, and proofs of them as separate theorems are welcome.

Selected references

Y. Achdou, F. Camilli, I. Capuzzo-Dolcetta, Mean field games: numerical methods for the planning problem, preprint hal-00465404v1, 2010. https://hal.science/hal-00465404 ; published in SIAM J. Control Optim. 50(1), 2012. https://doi.org/10.1137/100790069
Y. Achdou, I. Capuzzo-Dolcetta, Mean field games: numerical methods, SIAM J. Numer. Anal. 48(3), 2010. https://doi.org/10.1137/090758477
J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2(1), 2007. https://doi.org/10.1007/s11537-007-0657-8
I. Ekeland, R. Temam, Convex Analysis and Variational Problems, North-Holland, 1976 (SIAM Classics reprint 1999). https://doi.org/10.1137/1.9781611971088

11 thms2 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Optimal Sequencing of a Single Machine Subject to Precedence Constraints: Repeatedly Placing Last a Least-Cost Eligible Job Yields a Minmax Optimal SequenceResearch Paper

Motivation

Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.

Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting $O(n^2)$ procedure is the standard algorithm for the problem written $1\,|\,\mathrm{prec}\,|\,f_{\max}$ in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.

Setting

A finite, nonempty set $J$ of jobs is processed on a single machine, one job at a time and without interruption. Each job $j$ has a processing time $a_j \ge 0$ and a cost function $c_j : \mathbb{R} \to \mathbb{R}$ that is monotone nondecreasing. The value $c_j(t)$ is the cost incurred when $j$ is completed at time $t$ .

The precedence constraints are an arbitrary relation $\prec$ on jobs: $i \prec j$ means that job $i$ is required to precede job $j$ . A sequence $\pi = (\pi_1, \dots, \pi_n)$ lists every job of $J$ once. It observes the precedence constraints if $\pi_q \prec \pi_p$ never holds for positions $p < q$ . The machine starts at time $0$ with no idle time, so the completion time of $\pi_m$ is $C_{\pi_m}(\pi) = a_{\pi_1} + \dots + a_{\pi_m}$ . The maximum incurred cost of $\pi$ is

f_{\max}(\pi) = \max_{j \in J} c_j\bigl(C_j(\pi)\bigr),

and a feasible $\pi$ is minmax optimal if $f_{\max}(\pi) \le f_{\max}(\pi')$ for every feasible $\pi'$ .

For a set $P$ of jobs, $S(P)$ is the set of jobs of $P$ that are not required to precede any other job of $P$ , and $T_P = \sum_{j \in P} a_j$ . Lawler's rule builds a sequence from the last position to the first. With $P$ the jobs not yet placed, it chooses $k \in S(P)$ with $c_k(T_P) = \min_{j \in S(P)} c_j(T_P)$ , places $k$ in the latest open position and removes it from $P$ . Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible ( $S$ ), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.

Formalization targets

Goal: the rule is optimal

Every sequence $\pi$ that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies

f_{\max}(\pi) \;\le\; f_{\max}(\pi') \qquad \text{for every sequence } \pi' \text{ of } J \text{ observing the precedence constraints.}

This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.

Milestones

§2 proof, third paragraph. Moving a job of $S(J)$ to the end of a feasible sequence keeps it feasible.
§2 proof, fourth paragraph, first sentence. After that move, no job other than $k$ completes later, and $k$ completes at $T = \sum_{j \in J} a_j$ .
§2 proof, fourth paragraph. If $c_k(T) \le c_{k'}(T)$ , where $k'$ is the last job of the feasible sequence, the move does not raise $f_{\max}$ .
THEOREM (§2), p. 544. If some feasible sequence exists and $k \in S(J)$ minimizes $c_j(T)$ over $S(J)$ , then some minmax optimal sequence has $k$ last.
§3, the reduction. A minmax optimal sequence of $J \setminus \{k\}$ , followed by $k$ , is minmax optimal for $J$ .
§3, the procedure never stalls. If a feasible sequence exists, the rule produces a complete sequence. This shows the goal is not vacuous.

Significance

The result shows that $1\,|\,\mathrm{prec}\,|\,f_{\max}$ is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the $n$ partial sums $T_P$ along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for $f_{\max}$ objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.

The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets $S(P)$ and times $T_P$ to be the correct ones at each stage, which the definitions fix.

Difficulty

The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set $S(P)$ and the time $T_P$ must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.

A first attempt often proves only the Theorem, that some optimal sequence has $k$ last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of $J$ with $k$ last need not restrict to an optimal sequence of $J \setminus \{k\}$ . Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.

Formalization scope

Jobs form a type ι with decidable equality, and the job set is J : Finset ι.
Processing times are a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.
A sequence is a duplicate-free list whose elements are exactly J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).
The relation prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in $S$ (the "others" of the page exclude the job itself).

The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing $c_j$ for $j \in J$ , and $J$ nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative ( $a_j \ge 0$ ), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.

The rule is the property IsLawlerSequence of a finished sequence. At each position $m$ , the job there lies in $S$ of the jobs in positions $0..m$ and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.

The $n^2$ operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.

Selected references

E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5):544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544
J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
E. L. Lawler and J. M. Moore, A Functional Equation and its Application to Resource Allocation and Sequencing Problems, Management Science 16(1):77–84, 1969. https://doi.org/10.1287/mnsc.16.1.77
J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
R. L. Graham, E. L. Lawler, J. K. Lenstra and A. H. G. Rinnooy Kan, Optimization and Approximation in Deterministic Sequencing and Scheduling: a Survey, Annals of Discrete Mathematics 5:287–326, 1979. https://doi.org/10.1016/S0167-5060(08)70356-X

13 thms2 active usersReviewed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Variance-based Regularization with Convex Objectives II: A Covering-Number Certificate and Oracle Inequality for the Robust MinimizerResearch Paper

Motivation

Empirical risk minimization (ERM) chooses, from a class $\mathcal F$ of loss functions, the one with the smallest average loss on a sample $X_1,\dots,X_n$ . Its standard guarantees bound the excess population risk by a term of order $1/\sqrt n$ , whatever the variance of the losses. When good functions in $\mathcal F$ have small variance, a better trade-off is available in principle: minimize the empirical risk plus a standard-deviation penalty $\sqrt{2\rho\,\mathrm{Var}_{\widehat P_n}(f)/n}$ . Maurer and Pontil (COLT 2009) showed that this sample variance penalization enjoys faster rates, but the penalized objective is non-convex even for convex losses, so it cannot be minimized efficiently in general.

Duchi and Namkoong (arXiv:1610.02581v3, 2017; NIPS 2017) replace the variance penalty by a distributionally robust objective: the worst-case average loss over all reweightings of the sample within a $\chi^2$ -divergence ball of radius $\rho/n$ . This objective is convex whenever the loss is convex, and it equals the empirical risk plus the standard-deviation penalty up to an error of order $1/n$ . Theorem 3 of the paper turns this into a guarantee for the minimizer of the robust objective, using covering numbers of the class. This mission formalizes Theorem 3 and the lemmas its proof rests on.

Setting

Let $\mathcal X$ be a measurable space, $P$ a probability measure on it, and $X_1,\dots,X_n$ ( $n\ge1$ ) an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$ . Let $\mathcal F$ be a nonempty class of measurable functions $f:\mathcal X\to[M_0,M_1]$ , and set $M = M_1-M_0$ . Write $\mathbb E[f]=\int f\,dP$ , $\mathrm{Var}(f)$ for the variance of $f(X)$ , and

\mathbb E_{\widehat P_n}[f] = \frac1n\sum_{i=1}^n f(X_i),\qquad \mathrm{Var}_{\widehat P_n}(f) = \frac1n\sum_{i=1}^n f(X_i)^2 - \big(\mathbb E_{\widehat P_n}[f]\big)^2 .

For $\rho\ge0$ , the $\chi^2$ ball $\mathcal P_n$ is the set of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$ , $\sum_i p_i = 1$ and $\frac12\sum_i (np_i-1)^2\le\rho$ : the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$ . The robust risk of $f$ is

R_n(f) = \sup_{P:\,D_\phi(P\|\widehat P_n)\le \rho/n}\mathbb E_P[f(X)] = \max_{p\in\mathcal P_n}\sum_{i=1}^n p_i f(X_i),

and a robust minimizer is any $\widehat f\in\operatorname{argmin}_{f\in\mathcal F} R_n(f)$ .

Complexity is measured by empirical $\ell_\infty$ covering numbers. For $V\subset\mathbb R^m$ , $N(V,\epsilon,\|\cdot\|_\infty)$ is the least number of points $v_1,\dots,v_N\in V$ such that every $v\in V$ lies within sup-distance $\epsilon$ of some $v_i$ . For $x\in\mathcal X^m$ let $\mathcal F(x)=\{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}$ , and

N_\infty(\mathcal F,\epsilon,m) = \sup_{x\in\mathcal X^m} N\big(\mathcal F(x),\epsilon,\|\cdot\|_\infty\big)\in\mathbb N\cup\{\infty\}.

Formalization targets

Goal: the oracle inequality (16)

Let $n\ge 8M^2/t$ , $t\ge\log 12$ , $\epsilon>0$ and $\rho\ge 9t$ . With probability at least $1-2(3N_\infty(\mathcal F,\epsilon,2n)+1)e^{-t}$ , every robust minimizer $\widehat f$ satisfies

\mathbb E[\widehat f(X)] \le \inf_{f\in\mathcal F}\left\{\mathbb E[f] + 2\sqrt{\frac{2\rho}{n}\mathrm{Var}(f)}\right\} + \frac{19M\rho}{3n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .

The certificate (15)

Under the same hypotheses and with the same probability, simultaneously for all $f\in\mathcal F$ ,

\mathbb E[f(X)] \le R_n(f) + \frac{11}{3}\frac{M\rho}{n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .

Supporting results (milestones)

Theorem 1, inequality (10): for every vector $z\in[M_0,M_1]^n$ , the robust mean minus the sample mean lies between $\big(\sqrt{2\rho s_n^2/n}-2M\rho/n\big)_+$ and $\sqrt{2\rho s_n^2/n}$ .
Lemma C.1: a uniform empirical Bernstein bound over $\mathcal F$ with probability $1-6N_\infty(\mathcal F,\epsilon,2n)e^{-t}$ .
Lemma A.1, first bound: $\mathbb P(s_n\ge\sqrt{\mathbb E s_n^2}+t)\le\exp(-nt^2/(2M^2))$ .
Bernstein's inequality for one fixed $f$ , as displayed in the proof (p. 38).
The certificate (15).

Significance

Inequality (15) says the robust risk is a uniform upper confidence bound on the population risk, with an $O(1/n)$ slack instead of the $O(1/\sqrt n)$ slack of the empirical risk. Inequality (16) says the robust minimizer competes with the best variance-penalized population risk in the class. When some $f\in\mathcal F$ has small risk and small variance, the excess risk of $\widehat f$ is of order $1/n$ up to the covering term, a rate ERM does not achieve in general (§3.3 of the paper gives an example). For a parametric class with $N_\infty(\mathcal F,\epsilon,2n)$ polynomial in $1/\epsilon$ , choosing $\epsilon=M/n$ gives Corollaries 3.1 and 3.2 of the paper.

The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission's output is a formal proof of Theorem 3 and its ingredients: a deterministic analysis of the $\chi^2$ -constrained linear program (Theorem 1 (10)), a covering-number empirical Bernstein inequality (Lemma C.1, from Maurer and Pontil), concentration of the sample standard deviation (Lemma A.1), and the scalar Bernstein inequality in the form used. Each of these is reusable outside distributionally robust optimization.

Difficulty

The deterministic part, (10), is a short analysis of a quadratically constrained linear program. The main obstacle is Lemma C.1. A union bound over a cover of $\mathcal F$ fails directly: the cover depends on the sample, and a population-level cover of $\mathcal F$ need not be finite. The standard route goes through a ghost sample of size $n$ (hence covering at $2n$ points), a symmetrization that must preserve the sample variance rather than only the mean, and a concentration bound for the sample variance itself. Lemma A.1 needs concentration of $s_n$ , a non-linear and non-smooth function of the sample, at the sub-Gaussian rate $M/\sqrt n$ . Finally, the oracle inequality (16) holds for an infimum over the whole class, while the concentration step for the comparison function is only proved for one fixed $f$ at a time.

Formalization scope

The sample is the coordinate process of the product measure $P^{\otimes n}$ on $\mathcal X^n$ (Measure.pi). Each probability statement bounds the probability of the bad event, the set of samples where the inequality fails for some $f$ (or some minimizer). This set need not be measurable, and its measure is then the outer measure, as is standard in empirical-process theory. Probability bounds are computed in $[0,\infty]$ , and the covering number is valued in $\mathbb N\cup\{\infty\}$ , so an infinite covering number makes the bound trivial rather than collapsing to zero. Covering numbers are internal (centres in $\mathcal F(x)$ ) and use closed sup-norm balls, as on p. 9; this is Mathlib's Metric.coveringNumber. The empirical variance is normalized by $1/n$ . The $\chi^2$ ball is encoded as weight vectors on the sample points; with tied sample values this gives the same supremum as the paper's distributions on the sample. Statement (16) is formalized for every minimizer of the robust risk, and the event is empty if no minimizer exists. The infimum ranges over the nonempty class $\mathcal F$ , on which every term is at least $M_0$ . Population moments are those of bounded measurable functions, hence finite.

Deviations from the printed text:

Lemma A.1 is stated only for its first (upper-tail) bound. The paper derives the second bound from Lemma A.4, which is false as printed; the second bound is not stated. $M>0$ is assumed because $M^2$ is a denominator.
Lemma C.1 is the paper's restatement of Maurer and Pontil's Theorem 6, with a general radius $\epsilon$ . It is formalized as printed, with the implicit assumption $\epsilon>0$ made explicit.
$n\ge1$ is assumed throughout. The hypothesis $n\ge 8M^2/t$ is kept as printed.

A trivializing formalization is ruled out: the bound is not taken over all functions, a probability bound is not formed from the real part of an infinite covering number, and the minimizer is not a hypothesis that can fail to exist for the given sample.

Needed infrastructure: product-measure concentration (Bernstein, and a bounded-difference or convex-Lipschitz inequality for $s_n$ ), symmetrization with a ghost sample, and finite union bounds over a cover. Contributions are welcome on any milestone, in particular a general covering-number empirical Bernstein inequality, which is reusable on its own.

Selected references

J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017 (NIPS 2017; JMLR 20, 2019). https://arxiv.org/abs/1610.02581
A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Price of Stability for Network Design with Fair Cost Allocation III: Weighted Games in Which Each Edge Serves at Most Two Players Have a Potential and a Nash EquilibriumResearch Paper

Motivation

In a network design game each of $k$ players must connect its own terminals in a shared graph, and the cost of every edge that is bought is split among the players who use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008) studied the fair (Shapley) split, in which the $x_e$ users of an edge each pay $c_e/x_e$ . That game is a congestion game in the sense of Rosenthal (Networks 1973), so it has an exact potential function and pure Nash equilibria always exist.

When players carry different amounts of traffic, the natural rule is to split an edge's cost in proportion to weight: a player of weight $w_i$ on an edge whose users have total weight $W_e$ pays $(w_i/W_e)\,c_e$ . The paper notes that this rule is analogous to weighted generalizations of the Shapley value (Monderer and Samet, Variations of the Shapley Value, Handbook of Game Theory III, 2002). The weighted model leaves Rosenthal's framework: the share depends on which players use an edge, not only on how many, and Chen and Roughgarden (SPAA 2006) showed that weighted games with three or more players need not have a pure Nash equilibrium at all. Section 6 of the paper identifies structural conditions under which equilibria do exist. This mission covers the first of them.

Timeline. Rosenthal (1973): every congestion game has a pure Nash equilibrium, via an exact potential. Monderer and Shapley (GEB 1996): potential and weighted potential games, and the equivalence of exact potential games with congestion games. Anshelevich et al. (FOCS 2004, journal 2008): Theorem 6.1, existence when every resource is shared by at most two players, and Theorem 6.3, existence when all players share a source and a sink. Chen and Roughgarden (2006): weighted network design games with three or more players may have no pure equilibrium.

Setting

A weighted cost-sharing game $G$ consists of a finite set of players, a finite ground set $E$ of edges (resources), and for each player $i$ :

a finite family $\Sigma_i$ of feasible strategies, each a subset of $E$ ;
a weight $w_i \ge 1$ ;

together with a fixed edge cost $c_e \ge 0$ for every $e \in E$ . A profile $S = (S_i)_i$ picks $S_i \in \Sigma_i$ for every player. For an edge $e$ , $W_e$ is the total weight of the players with $e \in S_i$ , and player $i$ 's payment is

C_i(S) = \sum_{e \in S_i} \frac{w_i}{W_e}\, c_e .

A profile is a pure Nash equilibrium when no player $i$ has a $T \in \Sigma_i$ with $C_i(S_{-i}, T) < C_i(S)$ , where $(S_{-i}, T)$ is the profile in which $i$ plays $T$ and everyone else keeps their strategy.

The strategy space of player $i$ is the set of edges that occur in at least one strategy of $\Sigma_i$ . The hypothesis of Theorem 6.1 is that every edge lies in the strategy spaces of at most two players: no edge can ever be shared by three players, whatever they choose.

The network design game is the instance in which $E$ is the edge set of a graph and $\Sigma_i$ is the set of edge sets of paths connecting player $i$ 's source $s_i$ to its sink $t_i$ .

The paper's proof uses an explicit function $\Phi(S) = \sum_e \Phi_e(S)$ with $\Phi_e(S) = 0$ when $e$ is unused, $c_e w_i$ when $i$ alone uses $e$ , and $c_e\theta_{ij}$ when $i$ and $j$ both use it, where $\theta_{ij} = w_i + w_j - w_i w_j/(w_i + w_j)$ . It is part of the definitions of this mission.

Formalization targets

Goal: Theorem 6.1

If every edge lies in the strategy spaces of at most two players, there is a weighted potential: a real function $\Phi$ on profiles with

\Phi(S_{-i}, T) - \Phi(S) = w_i\,\bigl(C_i(S_{-i}, T) - C_i(S)\bigr) \quad\text{for every profile } S,\ \text{player } i,\ T \in \Sigma_i ,

and, if every $\Sigma_i$ is nonempty, a pure Nash equilibrium exists. The goal asserts the existence of such a $\Phi$ rather than fixing the paper's formula, so it remains valid for any other weighted potential.

Milestones

Joining a shared edge (proof of Theorem 6.1): when $i$ joins an edge already used by exactly one other player $j$ , $\Phi_e$ rises by $c_e w_i^2/(w_i + w_j)$ , which is $w_i$ times $i$ 's new share of $e$ .
The identity for the explicit potential: the displayed identity holds for the paper's $\Phi$ .
From a weighted potential to an equilibrium: in any weighted game with positive weights and nonempty strategy sets, a function satisfying the identity forces a pure Nash equilibrium to exist.

An extra item states Corollary 6.2: every two-player weighted game with nonempty strategy sets has a pure Nash equilibrium.

Significance

The result. Theorem 6.1 is one of the two existence results the paper proves for weighted cost sharing, a game that in general has no pure equilibrium. It shows that the obstruction found by Chen and Roughgarden needs resources shared by three or more players: whenever sharing is limited to pairs, the game is a weighted potential game, so improving moves cannot cycle and equilibria exist. Corollary 6.2 makes the two-player case unconditional, and the paper notes that the same potential gives a (weak) bound on the price of stability.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a reusable Lean model of weight-proportional cost sharing (shared in form with the companion mission on single-source single-sink weighted games), an explicit weighted potential, and the general step from a weighted potential to a pure equilibrium, which applies to any finite game with positive weights.

Difficulty

The obvious approach, reusing Rosenthal's potential from the unweighted game, fails: the paper observes that in a weighted game improving moves can increase it. A player's share of an edge depends on the weights of the specific co-users, so no function of the edge loads alone can track all players' costs. The identity must therefore hold for every unilateral move, including moves that leave some edges and join others at the same time, and for every pair of possible co-users of an edge. The statement fails without the at-most-two hypothesis, so any argument has to use it in an essential way. The existence step needs the identity on all profiles reachable by feasible deviations, not only along a single path of moves.

Formalization scope

Lean namespace PriceOfStability.WeightedPotential. Players form a Fintype ι and edges a Fintype E; a game is a structure with strategies : ι → Finset (Finset E), weight : ι → ℝ and edgeCost : E → ℝ. Standing assumptions wᵢ ≥ 1 and c_e ≥ 0 are the predicate IsStandard. Profiles are functions ι → Finset E with the feasibility predicate IsProfile; every deviation is to a feasible strategy, via Function.update. Nash equilibria are pure and in cost form. The strategy-space hypothesis is a bound on the number of players whose strategy space (the union of their strategies) contains each edge — not a bound on the users in one profile, which would be a different statement. Φ_e is computed from the current users of e; its value with three or more users is a placeholder that never arises under the hypothesis. Strategies are arbitrary subsets of the ground set, as the paper's remark after the proof allows, so the network game is a special case.

The goal is not satisfiable trivially: the function Φ must satisfy the weighted identity for every feasible unilateral deviation from every profile, and an exact (unweighted) potential is not what is asserted. Nonempty strategy sets are added explicitly for the existence part, since without a profile there is no equilibrium.

Needed infrastructure: finite sums over filtered Finsets, the improvement-path argument over the finite set of profiles. The improvement-path lemma (milestone 3) is reusable for any weighted potential game. Contributions of proofs for any milestone are welcome.

Selected references

E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
R. W. Rosenthal, The network equilibrium problem in integers, Networks 3:53–59, 1973. https://doi.org/10.1002/net.3230030104
D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14:124–143, 1996. https://doi.org/10.1006/game.1996.0044
H.-L. Chen, T. Roughgarden, Network design with weighted players, Proc. 18th ACM SPAA, 28–37, 2006. https://doi.org/10.1145/1148109.1148114

5 thms2 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance I: Quadratic Potential Functions Bound Mean Response Times in Open NetworksResearch Paper

Motivation

Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.

Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).

Timeline:

1980–1988: Coffman and Mitrani, then Federgruen and Groenevelt — the achievable performance vectors of a single-station multiclass queue form a polytope described by conservation laws.
Early 1990s: Kumar (reference [Kuma] of the paper), using a potential-function argument he attributes to Meyn, derives a single lower bound on the mean number in system for re-entrant lines with deterministic routing (described on p. 16 of the paper).
1992–1994: Bertsimas, Paschalidis and Tsitsiklis — parametric families of linear bounds for general open networks with Markovian routing (Theorem 4.1), and the nonparametric polyhedron (Theorems 4.2–4.4), shown to be at least as tight.

Setting

A network has $N$ single-server stations and $R$ job classes. Class $r$ is served at station $\sigma(r)$ , and $C_i$ is the set of classes served at station $i$ . Class- $r$ jobs arrive from outside as a Poisson stream of rate $\lambda_{0r}$ , service times are exponential with rate $\mu_r$ , and after service a class- $r$ job becomes a class- $s$ job with probability $p_{rs}$ or leaves with probability $p_{r0}=1-\sum_s p_{rs}$ . The traffic equations

\lambda_r=\lambda_{0r}+\sum_{r'}\lambda_{r'}p_{r'r}\qquad(15)

have a unique solution $\lambda$ (the network is open), and $\sum_{r\in C_i}\lambda_r/\mu_r<1$ at every station.

The state $\vec n=(n_1,\dots,n_R)$ counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write $B_r$ for the event that station $\sigma(r)$ serves class $r$ , and $B_{0i}$ for the event that station $i$ is idle. Under such a policy $\vec n(t)$ is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution $\pi$ and that $E_\pi[n_r^2]<\infty$ for all $r$ . Let $\bar n_r=E_\pi[n_r]$ , which equals $\lambda_rx_r$ with $x_r$ the mean response time of class $r$ (Little's law), and define

I_{rr'}=E_\pi[1\{B_r\}n_{r'}],\qquad N_{ir'}=E_\pi[1\{B_{0i}\}n_{r'}].

For a set $S$ of classes, f-parameters are reals $f(r)\ge 0$ for $r\in S$ such that $\mu_r\big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))+\sum_{r'\notin S}p_{rr'}f(r)\big]$ is nonnegative and the same for all $r\in C_i\cap S$ ; that common value is $f_i$ , and $f_i=0$ when $C_i\cap S=\emptyset$ (restriction (17)). The sums over $r'\notin S$ include the exit $r'=0$ .

Formalization targets

Goal: Theorem 4.1

For every policy satisfying Assumption A, every $S$ and every f-parameters satisfying (17),

\sum_{r\in S}\lambda_rf(r)x_r\ \ge\ \frac{N'(S)}{D'(S)},

where

N'(S)=\sum_{r\in S}\lambda_{0r}f^2(r)+\sum_{r\notin S}\lambda_r\sum_{r'\in S}p_{rr'}f^2(r')+\sum_{r\in S}\lambda_r\Big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))^2+\sum_{r'\notin S}p_{rr'}f^2(r)\Big],

D'(S)=2\Big[\sum_{i=1}^Nf_i-\sum_{r\in S}\lambda_{0r}f(r)\Big].

The formal goal is the product form $N'(S)\le D'(S)\sum_{r\in S}f(r)\bar n_r$ .

Milestones

The utilization identity $E_\pi[1\{B_r\}]=\lambda_r/\mu_r$ (pp. 16 and 19).
Theorem 4.2: the linear equalities (24), (25) between $\bar n_r$ and $I_{rr'}$ .
Theorem 4.3: $\sum_{r\in C_i}I_{rr'}+N_{ir'}=\bar n_{r'}$ (28).
Theorem 4.4: any nonnegative $(x,I,N)$ satisfying (24), (25), (28), with $\bar n_r=\lambda_rx_r$ in those equalities, satisfies every inequality of Theorem 4.1. This statement is deterministic.

Significance

Theorem 4.1 gives, for each choice of $S$ and $f$ , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost $\sum_r c_rx_r$ subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables $(\bar n,I,N)$ implies all of these inequalities at once, so the parametric search over $f$ is unnecessary.

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.

Difficulty

Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions ( $n_r$ , $n_rn_{r'}$ ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending $\sum_n\pi(n)(\mathcal Gg)(n)=0$ to quadratic $g$ needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify $\mu_rE_\pi[1\{B_r\}]$ with $\lambda_r$ . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because $f\ge0$ on $S$ , $f_i\ge0$ and at most one class per station is in service.

Formalization scope

Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs $\tau_k$ of the paper are not built: the paper notes that its expectations at $\tau_k$ are expectations under the invariant distribution of $\vec n(t)$ .

Conventions fixed in Lean:

$\lambda_rx_r$ appears only as the mean number in system $\bar n_r$ (Little's law, used by the paper on pp. 11 and 20); response times are not formalized.
Sums over $r'\notin S$ include the exit $r'=0$ (p. 15).
f-parameters are nonnegative on $S$ (p. 9).
The network is open: (15) has a unique solution, and $\lambda$ is an input constrained by (15), never defined from the policy.
(18) is stated multiplied by $D'(S)$ , which avoids Lean's $x/0=0$ and is (18) whenever $D'(S)>0$ .

A quotient-form statement of (18) would be trivially true when $D'(S)=0$ , and defining $\lambda_r$ as $\mu_rE_\pi[1\{B_r\}]$ would make the utilization identity hold by definition; both are excluded.

Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.

Selected references

D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan WP #3509-92-MSA, 1992; Ann. Appl. Probab. 4(1), 1994. https://doi.org/10.1214/aoap/1177005200
C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queuing network control, Math. Oper. Res. 24(2), 1999. https://doi.org/10.1287/moor.24.2.293

8 thms2 active usersReviewed

Operations Research Probability Stochastic Systems+1·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 2: The Triple-Balancing Policy Costs at Most Three Times the Optimum for Stochastic Lot-SizingResearch Paper

Motivation

Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of $T$ periods, decides whether to place an order, pays a fixed cost $K$ for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.

Timeline:

Scarf (1960) proved that $(s,S)$ policies are optimal for independent demands with fixed costs; with correlated demand the optimal policy is a state-dependent $(s_t(f_t), S_t(f_t))$ rule that is hard to compute.
Levi, Pál, Roundy and Shmoys (2007) gave the dual-balancing 2-approximation for the model without fixed costs (§4) and the triple-balancing 3-approximation for the stochastic lot-sizing problem (§6, Theorem 6.1), both for arbitrarily correlated demand.

Setting

There are periods $t=1,\dots,T$ on a probability space $(\Omega,\mathcal F,\mu)$ with a filtration $(\mathcal F_t)$ : $\mathcal F_t$ is the information available at the beginning of period $t$ . The data are a fixed ordering cost $K\ge0$ , per-unit holding costs $h_t\ge0$ , per-unit backlogging penalties $p_t\ge0$ , an initial inventory level $x_1\in\mathbb R$ , and nonnegative demands $D_t$ . The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that $D_t$ is $\mathcal F_t$ -measurable: the demand of a period is known when the period begins. For every period $s$ there is a conditional joint distribution $I_s$ of the demands given $\mathcal F_s$ , under which every conditional mean $E[D_t\mid f_s]$ is finite.

A feasible policy is an order process $Q=(Q_t)$ with $Q_t\ge0$ and $Q_t$ determined by $\mathcal F_t$ . Its inventory levels are $x_t=x_1+\sum_{j<t}(Q_j-D_j)$ before ordering and $y_t=x_t+Q_t$ after ordering, and its cost is

\mathcal C(Q)=\sum_{t=1}^T\Bigl(K\,\mathbb 1(Q_t>0)+h_t(y_t-D_t)^++p_t(D_t-y_t)^+\Bigr).

The triple-balancing policy TB uses two rules. Let $s^*$ be the last period before $s$ in which TB ordered ( $s^*=0$ if none). Rule 1: TB orders in period $s$ if and only if, without an order in $s$ , the accumulated backlogging cost over $(s^*,s]$ would exceed $K$ . Rule 2: when it orders in $s<T$ , it orders

q_s^B=\max\{q\ge0:\ E[H_s^B(q)\mid f_s]\le K\},\qquad H_s^B(q)=\sum_{j=s}^T h_j\bigl(q-(D_{[s,j]}-x_s)^+\bigr)^+,

the largest quantity whose expected marginal holding cost over $[s,T]$ is at most $K$ . When it orders in period $T$ , it orders exactly enough to clear the backorders and meet $D_T$ . Let $N$ be the number of orders TB places.

Formalization targets

Goal: Theorem 6.1

For every instance, the triple-balancing policy TB and every feasible policy $P$ satisfy

E[\mathcal C(TB)]\le 3\,E[\mathcal C(P)].

The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.

Milestones

§6.1, Rule 2 observation. In a period where TB orders, $D_s\le y_s^{TB}$ : no backorders remain at the end of the period.
Lemma 6.1. $K\cdot E[N]\le E[\mathcal C(P)]$ for every feasible $P$ .
Lemma 6.2. $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\cdot E[N]$ for every feasible $P$ .

Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when $h_T>0$ .

Significance

The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).

The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event $N=0$ . It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.

Difficulty

The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.

Formalization scope

Periods are natural numbers $1,\dots,T$ , demands and orders are real-valued, and data at indices outside $1,\dots,T$ are unused.
Information is a MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and " $D_t$ known at the start of period $t$ " means $D_t$ is $\mathcal F_t$ -measurable.
The conditional distributions $I_s$ are model data: Markov kernels to demand paths that are $\mathcal F_s$ -measurable regular conditional distributions of the demand path. At every outcome they make $D_s$ deterministic, demands nonnegative and the conditional means $E[D_t\mid f_s]$ finite.
Expected costs, $E[N]$ and the conditional expectation in Rule 2 are lower Lebesgue integrals in $[0,\infty]$ . Lemma 6.2 is stated additively, $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\,E[N]$ , which is the paper's inequality whenever the expectations are finite.
The comparison policy is an arbitrary feasible policy, not an optimal one. The paper's proofs use only feasibility, and this form implies the paper's whenever an optimum exists, without any existence hypothesis.
TB is the predicate "feasible and satisfies Rules 1 and 2 at every period and outcome". The rules determine the policy uniquely. Rule 1 uses a strict "exceeds $K$ ", and the period- $T$ order is $D_T-x_T$ .

Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every $q$ , because it uses kernel integrals in $[0,\infty]$ . Infinite expected costs cannot be read as $0$ . The policy class is not empty, because a separate theorem gives existence under $h_T>0$ (without some positive holding cost on $[s,T]$ the maximum in Rule 2 does not exist).

Contributions welcome: proofs of the existence theorems (measurable selection of $q_s^B$ , versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.

Selected references

R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. https://doi.org/10.1287/moor.1060.0205
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.

7 thms2 active usersReviewed

Analysis Convex Optimization Operations Research+1·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems II: The Łojasiewicz Inequality for Convex Subanalytic Functions on Bounded SetsResearch Paper

Motivation

The Łojasiewicz inequality states that near a critical point $a$ of a real-analytic function $f$ there are $\theta\in[0,1)$ and $C$ with $|f(x)-f(a)|^{\theta}\le C\,\|\nabla f(x)\|$ . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow $\dot x=-\nabla f(x)$ has finite length and converges to a single critical point, a conclusion that fails for general $C^\infty$ functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.

Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing $\|\nabla f\|$ by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to $+\infty$ and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.

Setting

Work in $\mathbb R^n$ with the Euclidean norm, and let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$ .

A set $A\subseteq\mathbb R^n$ is semianalytic if near every point it is a finite union of finite intersections of sets $\{f_{ij}=0,\ g_{ij}>0\}$ with $f_{ij},g_{ij}$ real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of $\mathbb R^n\times\mathbb R^m$ . A function is subanalytic when its graph $\{(x,\lambda): f(x)=\lambda\}$ is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.

The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\ne x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge 0$ , for $x\in\operatorname{dom} f$ , and is empty otherwise. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $(x_k,f(x_k))\to(x,f(x))$ . The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|:x^*\in\partial f(x)\}$ , equal to $+\infty$ when $\partial f(x)=\emptyset$ , and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points. For lower semicontinuous convex $f$ , $\partial f$ is the subdifferential of convex analysis and $\operatorname{crit} f$ is the set of minimizers. Write $\min f$ for the minimum value and $d_S(x)$ for the distance from $x$ to $S=\operatorname{crit} f$ . The epigraphical sum $g(x)=\inf_u\{f(u)+\tfrac12\|x-u\|^2\}$ is the Moreau envelope of $f$ .

Ratios follow the paper's conventions $0^0=1$ and $\infty/\infty=0/0=0$ .

Formalization targets

Goal: Theorem 3.3

Let $f$ be lower semicontinuous, convex and subanalytic with $\operatorname{crit} f\ne\emptyset$ . For every bounded set $K$ there is $\theta\in[0,1)$ such that

\frac{|f-\min f|^{\theta}}{m_f}\quad\text{is bounded on }K.

The exponent may depend on $K$ ; neither $\theta$ nor the bound is fixed.

Milestones

Eq. (5): $\partial f=\hat\partial f=$ the convex subdifferential, for lsc convex $f$ .
Section 3.2: $\operatorname{crit} f$ is closed, convex and equal to the set of minimizers.
Inequality (16): $|f(x)-\min f|\le\|x^*\|\,d_S(x)$ for all $x^*\in\partial f(x)$ .
Remark 3.6: $|f-\min f|/m_f$ is bounded around every critical point, without subanalyticity.
Proposition 2.9: the epigraphical sum $g$ is $C^1$ and subanalytic when $\inf f\in\mathbb R$ .
Properties (a)–(c): $g$ is finite and $C^1$ , $g\le f$ , $\operatorname{crit} g=\operatorname{crit} f$ , $\inf g=\inf f$ .
Proposition 2.13(ii): $\operatorname{crit} f$ is subanalytic for subanalytic $f$ that is relatively bounded on its domain.
Section 2.1: the distance to a subanalytic set is subanalytic.
The Łojasiewicz factorization lemma on compact sets (recalled from Bierstone–Milman).
Inequality (15): $d_S(x)\le c^{-1/r}|f(x)-\min f|^{1/r}$ on $K$ , with $r>1$ , $c>0$ .
Remark 3.5: the growth condition $|f-\min f|\ge c\,d_S^{\,r}$ on a compact $K$ alone yields a Łojasiewicz inequality at critical points interior to $K$ .

Significance

Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of $f$ on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow $\dot x\in-\partial f(x)$ of such functions. The intermediate inequality (15) is a Hölderian error bound, $d_S\le C|f-\min f|^{1/r}$ , of the kind that drives linear and sublinear rate analyses of first-order methods.

The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.

Difficulty

The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to $f-\min f$ and $d_S$ , fails: $f$ is neither continuous nor finite, and its domain need not be subanalytic even when $f$ is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of $\operatorname{crit} g$ and of $d_S$ rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never $-\infty$ " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves $\mathbb R^n$ and its products; global subanalyticity is not defined. $\min f$ is written $\inf_y f(y)$ in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " $|f(x)-\min f|^{\theta}\le C\|x^*\|$ for every $x\in K$ and every $x^*\in\partial f(x)$ ", with real powers (Real.rpow, $0^0=1$ ). Inequalities (15) and (17) are imposed only where $f(x)<+\infty$ , since Lean sends $+\infty$ to $0$ under toReal.

Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where $0\cdot\infty=0$ would make the ratio vacuous, and $\theta$ remains existential in $[0,1)$ with the quantifier order "for every $K$ there is $\theta$ ", so that $\theta=0$ is excluded at critical points in $K$ by $0^0=1$ .

A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on $\mathbb R^n$ and its $C^1$ property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
E. Bierstone, P. D. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, Éditions du CNRS, Paris, 1963, 87–89.
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146 (2014) 459–494. https://doi.org/10.1007/s10107-013-0701-9

18 thms2 active usersReviewed

Combinatorics Functional Analysis Machine Learning·Captain: mikedeng1

The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network II: Fat-Shattering Bound for Bounded-Weight NetworksResearch Paper

Motivation

In the mid-1990s, neural networks trained by gradient descent were observed to generalize well even when the number of weights far exceeded the number of training examples. The classical theory could not explain this: VC-dimension bounds for networks grow with the number of parameters, so for large networks they are vacuous. Bartlett's paper (IEEE Trans. Inform. Theory 44 (1998)) showed that, for classification with a margin, what controls generalization is the size of the weights, not the size of the network. Its two main technical results are a margin bound in terms of the fat-shattering dimension (Theorem 2, the subject of mission I of this series) and a bound on the fat-shattering dimension of networks with bounded weights (Theorem 17, the subject of this mission). The same idea of weight-norm capacity control underlies much of the later theory of margins, boosting and kernel methods.

Timeline. Kearns and Schapire (1994) introduced the fat-shattering dimension. Alon, Ben-David, Cesa-Bianchi and Haussler (1997) bounded ℓ∞ covering numbers by it. Bartlett, Kulkarni and Posner (1997) gave the matching lower bound on ℓ1 covering numbers used here as Lemma 19. Maurey's approximation lemma (reported by Pisier, 1981) was used by Jones (1992) and Barron (1993) for approximation by networks, and by Lee, Bartlett and Williamson (1996) for covering numbers of convex hulls. Bartlett (1998) combined these into Theorem 17.

Setting

Let $X$ be a set and $H$ a class of functions $X\to\mathbb R$ . For $\gamma>0$ , a sequence $x=(x_1,\dots,x_m)\in X^m$ is $\gamma$ -shattered by $H$ if there is $r\in\mathbb R^m$ such that for every $b\in\{-1,1\}^m$ some $h\in H$ satisfies $(h(x_i)-r_i)b_i\ge\gamma$ for all $i$ . The fat-shattering dimension is

\operatorname{fat}_H(\gamma)=\max\{m:\ H\ \gamma\text{-shatters some }x\in X^m\}\in\mathbb N\cup\{\infty\}.

A cover of a class $F$ at scale $\varepsilon$ for a pseudometric $\rho$ on functions is a set $T$ of functions such that every $f\in F$ has some $t\in T$ with $\rho(t,f)<\varepsilon$ ; $\mathcal N(F,\varepsilon,\rho)$ is the least size of a cover. For a sample $x\in X^m$ the pseudometrics $d_{\ell_\infty(x)}$ , $d_{\ell_1(x)}$ , $d_{\ell_2(x)}$ are the maximum, the mean, and the root mean square of $|f(x_i)-g(x_i)|$ over $i$ , and the uniform covering numbers are $\mathcal N_p(F,\varepsilon,m)=\max_{x\in X^m}\mathcal N(F,\varepsilon,d_{\ell_p(x)})$ .

The hidden units form a nonempty class $F$ of functions $X\to[-M/2,M/2]$ . For $A>0$ the two-layer network class with ℓ1-bounded output weights is

H=\Big\{\sum_{i=1}^Nw_if_i:\ N\in\mathbb N,\ f_i\in F,\ \sum_{i=1}^N|w_i|\le A\Big\}.

In Lean these are BartlettNN.Margin.fat, BartlettNN.Margin.coverNum and BartlettNN.Margin.Ninf (shared with mission I), and BartlettNN.FatNet.N1, BartlettNN.FatNet.N2 and BartlettNN.FatNet.combos F A.

Formalization targets

Goal: Theorem 17

There is a universal constant $c$ such that for every $X$ , $F$ , $M$ , $A>0$ and $\gamma>0$ with $d=\operatorname{fat}_F(\gamma/(32A))\ge1$ ,

\operatorname{fat}_H(\gamma)\le\frac{cM^2A^2d}{\gamma^2}\ln^2\Big(\frac{MAd}{\gamma}\Big).

The constant is left unspecified, as in the paper, so that the goal survives any improvement of the numerical constants.

Milestones (in the order the proof uses them)

Lemma 19 (cited from Bartlett–Kulkarni–Posner): for $[0,1]$ -valued $F$ with $\operatorname{fat}_F(4\gamma)\ge d$ , $\log_2\mathcal N_1(F,\gamma,d)\ge d/32$ .
Lemma 20, (5): for $d=\operatorname{fat}_F(\gamma/4)$ and $m\ge2+2d\log_2(32M/\gamma)$ , $\log_2\mathcal N_2(F,\gamma,m)<1+d\log_2(4emM/(d\gamma))\log_2(9mM^2/\gamma^2)$ .
Lemma 21 (Maurey): in a Hilbert space, a point of the closed convex hull of a set of norm at most $b$ is within $\sqrt{c/k}$ of an average of $k$ points of the set, for every $c>b^2-\|h\|^2$ .
Lemma 22: $\log_2\mathcal N_2(H,\gamma,m)\le(2M^2A^2/\gamma^2)\log_2(2\mathcal N_2(F,\gamma/(2A),m)+1)$ .
Inequality (6): if $m=\operatorname{fat}_H(4\gamma)\ge2+2d\log_2(64MA/\gamma)$ with $d=\operatorname{fat}_F(\gamma/(8A))$ , then $m\le(64M^2A^2/\gamma^2)(3+d\log_2(8emMA/\gamma)\log_2(36mM^2A^2/\gamma^2))$ .

Significance

Theorem 17 bounds the capacity of a network class without reference to the number of hidden units $N$ . With Theorem 2 (mission I) it gives misclassification bounds for networks with small weights that hold for networks of any size, and by iteration it yields the bounds for deep sigmoid networks of Theorem 28 (mission III). Its method — upper-bound ℓ2 covering numbers through Maurey's lemma and compare with a lower bound in terms of fat-shattering — is a template for bounding the fat-shattering dimension of convex hulls in general.

The results are proved in the paper (Lemmas 19 and 21 by citation). None of them is formalized: the platform has no fat-shattering dimension, no uniform sample covering numbers of function classes, and only a finite-dimensional, diameter-based form of Maurey's lemma (HighDimProb.Appetizer.approx_caratheodory), which is not Lemma 21. This mission produces machine-checked statements of all five ingredients and of the theorem.

Difficulty

The obvious route would bound $\operatorname{fat}_H$ through a VC-type count of the network's parameters, which fails because $N$ is unbounded. The paper's route needs a lower bound on covering numbers by the fat-shattering dimension (Lemma 19, a combinatorial packing argument not proved in the paper), an upper bound by the fat-shattering dimension at a finer scale (Lemma 20, which goes through the Alon et al. scale-sensitive Sauer lemma and a quantization argument), and a probabilistic approximation argument in the empirical $L_2$ space (Lemmas 21 and 22). The final step solves a transcendental inequality (6) for $m$ , with care at the boundary where the logarithm is small.

Formalization scope

Functions are maps X → ℝ; fat is valued in ℕ∞, so an unbounded shattering is $\infty$ , not a junk $0$ . Labels $\pm1$ are Bool read through pm (true ↦ 1); sequences are indexed by Fin m (0-based).
Covers are external (finite sets of arbitrary functions $X\to\mathbb R$ ) with the strict inequality of Definition 3; the covering number is $\infty$ when no finite cover exists. The ℓ1 and ℓ2 distances carry the factor $1/m$ . Mathlib's Metric.coveringNumber (closed balls, metric types) is not used.
Bounds of the form " $\log_2\mathcal N\le B$ " are stated for every finite value of $\mathcal N$ , and where the paper's bound implies finiteness (Lemmas 20, 22, Theorem 17) finiteness is part of the conclusion.
The constant $c$ of Theorem 17 is quantified before $X$ , $F$ , $M$ , $A$ , $\gamma$ and $d$ ; a constant chosen after them would make the statement trivially true.
Corrections of the printed statement. Theorem 17 is stated for $\gamma>0$ (printed $\gamma\ge0$ , under which the bound is meaningless) and $A>0$ (printed $A\ge0$ , under which $\gamma/(32A)$ is undefined). Implicit positivity ( $M>0$ , $\gamma>0$ , $A>0$ ) in Lemmas 20, 22 and (6) is stated as hypotheses. Inequality (6) is copied as printed, with $\log_2(8emMA/\gamma)$ .
In Theorem 17 the logarithm is natural (the base is absorbed by $c$ ); (5) and (6) use $\log_2$ .
Lemma 21 is stated in a complete real inner product space, with "convex closure" read as the closure of the convex hull.

Contributions welcome: proofs of the five milestones and of the goal, and reusable infrastructure on fat-shattering and covering numbers of function classes.

Selected references

P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Trans. Inform. Theory 44(2), 1998, 525–536. https://doi.org/10.1109/18.661502
N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, J. ACM 44(4), 1997, 615–631. https://doi.org/10.1145/263867.263927
P. L. Bartlett, S. R. Kulkarni, S. E. Posner, Covering numbers for real-valued function classes, IEEE Trans. Inform. Theory 43(5), 1997, 1721–1724. https://doi.org/10.1109/18.623181
M. J. Kearns, R. E. Schapire, Efficient distribution-free learning of probabilistic concepts, J. Comput. Syst. Sci. 48(3), 1994, 464–497. https://doi.org/10.1016/S0022-0000(05)80062-5
W. S. Lee, P. L. Bartlett, R. C. Williamson, Efficient agnostic learning of neural networks with bounded fan-in, IEEE Trans. Inform. Theory 42(6), 1996, 2118–2132. https://doi.org/10.1109/18.556601
A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inform. Theory 39(3), 1993, 930–945. https://doi.org/10.1109/18.256500

11 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 5: The Maximum Likelihood Estimator Exists with Probability Tending to One and Is Consistent and Asymptotically NormalResearch Paper

Motivation

The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative $i$ with probability proportional to $e^{z_i\theta}$ , where $z_i$ is a vector of observed attributes and $\theta$ an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate $\theta$ by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.

Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.

Setting

Observations are indexed serially, $m = 0, 1, 2, \dots$ , as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation $m$ offers $J_m \ge 1$ alternatives, and alternative $i$ carries a vector $z_{im} \in \mathbb R^K$ of independent variables. For a parameter $\theta \in \mathbb R^K$ the selection probabilities are

P_{im}(\theta) = \frac{e^{z_{im}\theta}}{\sum_{j=1}^{J_m} e^{z_{jm}\theta}}, \qquad \bar z_m(\theta) = \sum_{i} P_{im}(\theta)\, z_{im}.

The data are generated at a true parameter $\theta^0$ : the chosen alternatives $Y_0, Y_1, \dots$ are independent random variables with $\Pr(Y_m = i) = P_{im}(\theta^0)$ . The log-likelihood of the first $q$ observations is $L^q(\theta) = \sum_{m<q}\log P_{Y_m m}(\theta)$ . The moment matrix of observation $m$ is

\Omega_m = \sum_{i} P_{im}(\theta^0)\,(z_{im}-\bar z_m)(z_{im}-\bar z_m)', \qquad \bar z_m = \bar z_m(\theta^0).

Axiom 7 asks that $J_m \le J_*$ and $|z_{im}| \le M$ uniformly, and that $\frac1q\sum_{m<q}\Omega_m$ converge to a positive definite matrix $\Omega$ . Axiom 6, for a given sample, asks that no nonzero $\gamma$ satisfy $(z_{jm} - z_{Y_m m})\gamma \le 0$ for all observed $m$ and all $j$ . A maximum likelihood estimator $\hat\theta^q$ is a measurable choice of a maximizer of $L^q$ , wherever one exists.

Formalization targets

Goal: Lemma 6

\hat\theta^q \xrightarrow{\Pr} \theta^0 \quad\text{and}\quad \sqrt q\,\Omega^{1/2}(\hat\theta^q - \theta^0) \xrightarrow{d} N(0, I_K) \qquad (q \to \infty).

Milestones

Axiom 7 implies Axiom 5 (the full-rank condition) in all sufficiently large samples.
Equation (42): $P_{im}(\theta) \ge 1/(J_* e^{2M|\theta|})$ .
Lemma 5: $\Pr(\text{Axiom 6 holds and } L^q \text{ attains its maximum}) \to 1$ .
Equation (43): the first three derivatives of $\log P_{im}$ are bounded by $2M$ , $4M^2$ , $8M^3$ .
Equation (46): each score $\nabla\log P_{Y_m m}(\theta^0)$ has mean zero.
Equation (47): each expected Hessian equals $-\Omega_m$ .
Consistency of $\hat\theta^q$ .
Equation (58): $q^{-1/2}\,\Omega^{-1/2}\sum_{m<q}\nabla\log P_{Y_m m}(\theta^0) \xrightarrow{d} N(0, I_K)$ .

Significance

The result. Lemma 6 is what licenses reading $\hat\theta^q$ as approximately $N(\theta^0, q^{-1}\Omega^{-1})$ , so that the diagonal of the inverse information matrix estimates the sampling variances and $q(\hat\theta^q-\theta^0)'\Omega(\hat\theta^q-\theta^0)$ is asymptotically $\chi^2_K$ . Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction $\gamma$ of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.

Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization $1/q$ in (58), which must be $1/\sqrt q$ , and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.

Difficulty

The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around $\theta^0$ , controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances $\Omega_m$ that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin K); $z\theta$ is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.
The paper's $N$ trials with $R_n$ repetitions are the special case of the serial indexing in which consecutive observations repeat their data; the sample size $\sum_n R_n$ is $q$ .
Axiom 7's limit (27) is taken in its serial form (48), with $P$ evaluated at $\theta^0$ .
The estimator is any measurable selection that maximizes $L^q$ whenever $L^q$ has a maximum, and is unconstrained otherwise. Requiring a maximizer for every sample would be unsatisfiable, since Axiom 6 fails with positive probability, and would make the goal vacuous; this convention rules that out.
Consistency is TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. $\Omega^{1/2}$ is the positive semidefinite square root CFC.sqrt.
Needed infrastructure: derivatives of log-sum-exp, a law of large numbers for bounded independent vectors, and a multivariate Lindeberg–Feller theorem. Mathlib provides the one-dimensional i.i.d. central limit theorem only. Contributions of these general results as separate theorems are welcome.

Selected references

D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142.
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966 (Lindeberg–Feller theorem, pp. 256–258).
C. R. Rao, Linear Statistical Inference and Its Applications, Wiley (cited by McFadden as Rao (1968), pp. 347–351, for the asymptotic $\chi^2$ test).

10 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 4: Existence of the Maximum Likelihood Estimate Is Decided by a Quadratic ProgramResearch Paper

Why a likelihood maximum needs a diagnostic

The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.

The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.

Choice experiments and weighted differences

There are $N\geq1$ trials. Trial $n$ offers $J_n$ alternatives, indexed by $i$ and $j$ . Alternative $i$ has an attribute vector $z_{in}\in\mathbb R^K$ , and $S_{in}$ counts how many times it was selected in that trial. Each trial has at least two alternatives and $R_n=\sum_iS_{in}>0$ observations. The vector $\theta\in\mathbb R^K$ is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative $i$ a probability proportional to $\exp(z_{in}\cdot\theta)$ , with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).

For the test, define the weighted difference

w_{nij}=S_{in}(z_{jn}-z_{in})\in\mathbb R^K.

It is indexed by every trial and every ordered pair of alternatives, including $i=j$ and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.

Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank $K$ . Equivalently, the vectors $z_{jn}-z_{in}$ span $\mathbb R^K$ ; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction $\gamma\in\mathbb R^K$ satisfies $w_{nij}\cdot\gamma\leq0$ for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.

Formalization targets

Lemma 4: a quadratic-programming test

Let $Q$ be the set of feasible vectors

Q=\left\{y=\sum_{n=1}^{N}\sum_{i,j=1}^{J_n}\alpha_{ijn}w_{nij}: \alpha_{ijn}\geq1\text{ for all }n,i,j\right\}.

The mission's goal is the equivalence in Lemma 4:

\text{Axiom 6 holds} \quad\Longleftrightarrow\quad \min_{y\in Q}y\cdot y=0.

The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the $w_{nij}$ gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).

What the result provides

Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.

The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.

Why the equivalence is delicate

The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints $\alpha_{ijn}\geq1$ in equation (22). Both conditions must appear in their proper places.

The full-rank condition alone does not ensure that the vectors $w_{nij}$ span the attribute space if a trial has no observed choices. The section describes $R_n$ repetitions of each trial, and the formal data require $R_n>0$ . This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.

Formalization scope

Lean represents a nonempty set of trials by Fin N, alternatives in trial $n$ by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count $R_n$ is the sum of observed choice counts. The model requires $J_n\geq2$ and $R_n>0$ for each trial. There is no extra assumption that $K>0$ : the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.

Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every $n,i,j$ from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.

The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.

Selected references

Daniel McFadden, “Conditional Logit Analysis of Qualitative Choice Behavior,” in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142; especially pp. 113–117, Axioms 5–6, Lemmas 3–4, and equation (22). Book catalog search.

5 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Certified Adversarial Robustness via Randomized Smoothing 2: The Certified ℓ2 Radius Cannot Be EnlargedResearch Paper

Motivation

Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point $x$ does not change for any perturbation $\delta$ in a stated set, typically an $\ell_2$ ball $\|\delta\|_2<R$ . Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$ (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.

Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.

Setting

Inputs live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$ ; classes form a set $\mathcal Y$ . A base classifier is a map $f:\mathbb R^d\to\mathcal Y$ with Borel decision regions. For a noise level $\sigma>0$ , write $\mathcal N(x,\sigma^2I)$ for the isotropic Gaussian law of $x+\varepsilon$ with $\varepsilon\sim\mathcal N(0,\sigma^2I)$ . The class probability of $c$ at $x$ is $\mathbb P(f(x+\varepsilon)=c)$ , and the smoothed classifier is

g(x)=\arg\max_{c\in\mathcal Y}\ \mathbb P(f(x+\varepsilon)=c).

Let $\Phi$ be the standard Gaussian CDF and $\Phi^{-1}$ its inverse on $(0,1)$ . A classifier $f$ is consistent with the observed class probabilities (6) for a top class $c_A$ and numbers $\underline{p_A}\ge\overline{p_B}$ if

\mathbb P(f(x+\varepsilon)=c_A)\ \ge\ \underline{p_A}\ \ge\ \overline{p_B}\ \ge\ \max_{c\ne c_A}\mathbb P(f(x+\varepsilon)=c).

The certified radius is $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$ . In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces $A=\{z:\delta^T(z-x)\le\sigma\|\delta\|\Phi^{-1}(\underline{p_A})\}$ and $B=\{z:\delta^T(z-x)\ge\sigma\|\delta\|\Phi^{-1}(1-\overline{p_B})\}$ of the paper's Appendix A are setA and setB.

Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.

Formalization targets

Goal: Theorem 2 (corrected)

Assume $0<\overline{p_B}\le\underline{p_A}<1$ , $\underline{p_A}+\overline{p_B}\le1$ , and that some finite set $s$ of classes other than $c_A$ satisfies $1\le\underline{p_A}+|s|\,\overline{p_B}$ . Then for every $\delta$ with $\|\delta\|_2>R$ there is a base classifier $f^*$ consistent with (6) and a class $c\ne c_A$ with

\mathbb P(f^*(x+\delta+\varepsilon)=c_A)\ <\ \mathbb P(f^*(x+\delta+\varepsilon)=c),

so that $g(x+\delta)\ne c_A$ under any tie-breaking. The classifier may depend on $\delta$ .

The class-capacity hypothesis is a correction. As printed, with only $\underline{p_A}+\overline{p_B}\le1$ , the theorem fails for two classes: with $\mathcal Y=\{c_A,c_B\}$ , $\underline{p_A}=0.6$ , $\overline{p_B}=0.1$ and $\sigma=\|\delta\|_2=1$ , one has $R\approx0.767<1$ , yet every consistent $f$ gives $c_A$ probability at least $0.9$ , and Theorem 1 then certifies radius $\Phi^{-1}(0.9)\approx1.28$ .

Milestones

The milestones are the steps the paper itself states, in its order: the Claims $\mathbb P(X\in A)=\underline{p_A}$ and $\mathbb P(X\in B)=\overline{p_B}$ for $X\sim\mathcal N(x,\sigma^2I)$ ; the disjointness of $A$ and $B$ (corrected to "null" when $\underline{p_A}+\overline{p_B}=1$ ); equations (13) and (14) for $Y\sim\mathcal N(x+\delta,\sigma^2I)$ ,

\mathbb P(Y\in A)=\Phi\Big(\Phi^{-1}(\underline{p_A})-\tfrac{\|\delta\|}{\sigma}\Big),\qquad \mathbb P(Y\in B)=\Phi\Big(\Phi^{-1}(\overline{p_B})+\tfrac{\|\delta\|}{\sigma}\Big);

the equivalence $\mathbb P(Y\in A)<\mathbb P(Y\in B)\iff\|\delta\|_2>R$ ; and the existence of the worst-case classifier $f^*$ satisfying (6) with equalities.

Significance

Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about $f$ , the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open $\ell_2$ ball of radius $R$ . It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.

The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim $A\cap B=\emptyset$ fails at $\underline{p_A}+\overline{p_B}=1$ . To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.

Difficulty

Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on $\mathbb R^d$ under a linear functional $z\mapsto\delta^T z$ is the one-dimensional Gaussian with variance $\|\delta\|^2$ , and $\Phi$ is a continuous strictly increasing bijection $\mathbb R\to(0,1)$ with $\Phi^{-1}(1-p)=-\Phi^{-1}(p)$ . The construction of $f^*$ has a further step the paper leaves informal: the region between $A$ and $B$ , of mass $1-\underline{p_A}-\overline{p_B}$ , must be shared among "other classes" with none exceeding $\overline{p_B}$ , which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $\mathcal N(x,\sigma^2I)$ is the pushforward of Mathlib's stdGaussian under $z\mapsto x+\sigma z$ , with $\sigma>0$ a binder. $\Phi$ is cdf (gaussianReal 0 1); $\Phi^{-1}(p)$ is the generalized inverse $\inf\{t:p\le\Phi(t)\}$ , which is the true inverse on $(0,1)$ and the junk value $0$ at the endpoints, so every statement that evaluates it assumes $0<p<1$ ; at $\overline{p_B}=0$ or $\underline{p_A}=1$ the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of $c_A$ to be a strict unique argmax.

A formalization in which the junk endpoint value of $\Phi^{-1}$ makes $R$ negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.

Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on $(0,1)$ . Contributions of general Mathlib-style lemmas (the law of $\delta^T X$ for $X\sim\mathcal N(x,\sigma^2I)$ , properties of $\Phi^{-1}$ ) are welcome.

Selected references

J. M. Cohen, E. Rosenfeld, J. Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML 2019; arXiv:1902.02918v2. https://arxiv.org/abs/1902.02918v2
M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, S. Jana, Certified Robustness to Adversarial Examples with Differential Privacy, IEEE S&P 2019. https://arxiv.org/abs/1802.03471
B. Li, C. Chen, W. Wang, L. Carin, Certified Adversarial Robustness with Additive Noise, NeurIPS 2019. https://arxiv.org/abs/1809.03113
J. Neyman, E. S. Pearson, On the Problem of the Most Efficient Tests of Statistical Hypotheses, Phil. Trans. R. Soc. A 231, 1933. https://doi.org/10.1098/rsta.1933.0009

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability+1·Captain: mikedeng1

Secretary Problems: Weights and Discounts 1: An (8+3e)-Competitive Algorithm for the Weighted Secretary ProblemResearch Paper

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$ , each with a nonnegative value $v(e)$ , and $K$ goods indexed in decreasing order of nonnegative weight:

w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$ . Its value is $\sum_{k=1}^K v(s(k))w(k)$ . Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$ , chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$ , assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$ , the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$ , observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$ . A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$ .

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$ , which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$ :

\mathrm{OPT}\le(8+3e)\,\mathbb E[A].

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$ . Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class- $i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$ , the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$ . The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$ . It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$ . An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$ , so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

7 thms2 active usersReviewed

Probability Statistics·Captain: mikedeng1

Weighted Sums of Certain Dependent Random Variables 3: Reversed Weighted Sums of Bounded Martingale Differences Obey a Strong LawResearch Paper

Motivation

A martingale difference sequence is the standard model of a "fair" sequence of observations whose terms may depend on the past: each new term has conditional mean zero given everything observed before it. Laws of large numbers for such sequences underlie the analysis of stochastic approximation, sequential estimation and online learning, where the noise terms are dependent but conditionally centred.

Classical strong laws concern averages in which every observation keeps the same weight as the sample grows. Kazuoki Azuma's 1967 paper Weighted sums of certain dependent random variables (Tôhoku Math. J. 19) studies weighted sums of dependent variables, and is best known for the exponential moment bound that is now called the Azuma inequality (its display (2.4) together with Remark 1). Its Theorem 3 uses that bound to prove a strong law for weighted averages in which the weights are applied in reverse order, so that the oldest observation always receives the newest, largest weight.

Timeline:

1960s: Y. S. Chow (Ann. Math. Statist. 37, 1966) introduces a conditional exponential-moment condition close to Azuma's property [G] in a convergence theorem for independent variables.
1967: Azuma proves the moment bound (2.4) for conditionally sub-Gaussian martingale differences, a law of the iterated logarithm for direct weighted sums (Theorem 2), and the strong law for reversed weighted sums (Theorem 3), the subject of this mission.

Setting

Let $(\Omega,\mathfrak A,P)$ be a probability space and $(\mathfrak A_n)_{n\ge0}$ an increasing family of sub- $\sigma$ -fields of $\mathfrak A$ . A sequence $(x_n)_{n\ge1}$ of real random variables is a sequence of martingale differences if, for every $n\ge1$ , $x_n$ is $\mathfrak A_n$ -measurable and integrable and $E\{x_n\mid\mathfrak A_{n-1}\}=0$ almost surely. Theorem 3 assumes moreover $|x_n|\le1$ almost surely for every $n$ .

Let $(a_n)_{n\ge1}$ be positive increasing weights: $a_n>0$ and $a_n\le a_{n+1}$ . Put

A_n = a_1+a_2+\dots+a_n,\qquad \bar S_n = a_nx_1 + a_{n-1}x_2+\dots+a_1x_n=\sum_{j=1}^n a_{n-j+1}x_j .

The sums $\bar S_n$ are the reversed weighted sums. In passing from $\bar S_n$ to $\bar S_{n+1}$ every existing term changes its weight, so $(\bar S_n)$ is in general not a martingale. In the Lean development, $A_n$ is A a n, $\bar S_n(\omega)$ is Sbar a x n ω, and the martingale-difference property is IsMartingaleDiff μ ℱ x.

Formalization targets

Goal: Theorem 3, (4.9)–(4.10)

If $(x_n)$ is a sequence of martingale differences with $|x_n|\le1$ a.s., $(a_n)$ is positive and nondecreasing, and

\frac{a_n}{A_n}=o\Big(\frac{1}{\log\log A_n}\Big)\qquad(n\to\infty),\tag{4.9}

then

\frac{\bar S_n}{A_n}\longrightarrow0\quad\text{almost surely}.\tag{4.10}

Milestones

The milestones follow the paper's proof, in attack order.

Remark 1 (p. 358): if $|x_n|\le K_n$ a.s., then $E\{\exp(tx_n)\mid\mathfrak A_{n-1}\}\le\cosh(tK_n)\le\exp(t^2K_n^2/2)$ a.s.
The tail step of (4.16) (p. 366): for $|x_n|\le1$ , real $c_1,\dots,c_N$ with $\sum c_j^2>0$ and $\lambda\ge0$ ,

P\Big\{\sum_{j=1}^Nc_jx_j>\lambda\Big\}\le\exp\Big(-\frac{\lambda^2}{2\sum_{j=1}^Nc_j^2}\Big).

The blocks (4.11)–(4.14) (pp. 364–365): for every $\varepsilon>0$ there are indices $n_1<n_2<\cdots$ with $A_{n_1}>2(3+\varepsilon)/(6+\varepsilon)$ , $a_n/A_n<\varepsilon/(6+\varepsilon)$ and $a_n\log\log A_n/A_n<\varepsilon^2/64$ for $n>n_1$ , and $A_{n_{k-1}}<A_{n_k}\le(1+\varepsilon/3)A_{n_{k-1}}<A_{n_k+1}$ .
The maximal inequality (4.15) (p. 365): if $A_{N_1}\le(1+\varepsilon/3)A_{N_0}$ with $1\le N_0<N_1$ , then

2P\{\bar S_{N_1}>(\varepsilon/2)A_{N_0}\}\ge P\Big\{\max_{N_0<n\le N_1}\bar S_n>\varepsilon A_{N_0}\Big\}.

Block growth (p. 366): (4.11), (4.12) and (4.14) give $A_{n_k}>(2(3+\varepsilon)/(6+\varepsilon))^{k-1}$ .

Significance

The result. Theorem 3 shows that reversed weighting does not destroy the strong law, under a growth condition on the weights that is strictly weaker than the condition $a_n^2/\sum_{j\le n}a_j^2\to0$ of the paper's Theorem 2: the paper reproduces an example of T. Tsuchikura satisfying (4.9) but not that condition. The condition allows rapidly growing weights, provided no single weight carries more than an $o(1/\log\log A_n)$ share of the total. Milestone 2 is the one-sided Azuma inequality in the paper's conditional-expectation form, a tool used throughout probability, combinatorics and learning theory. Milestone 4 is a maximal inequality for a process that is not a martingale, where Doob's inequality cannot be used.

Formalizing it. The theorem is proved in the paper; this mission produces a machine-checked proof. Mathlib contains sub-Gaussian moment-generating-function bounds for martingale differences in a kernel formulation (HasCondSubgaussianMGF, which assumes a standard Borel space), and the Prove2Me platform has two-sided Azuma–Hoeffding inequalities under the same assumption. Neither states Remark 1 or the one-sided tail bound in the paper's conditional-expectation form on an arbitrary probability space, and no strong law for reversed weighted sums is formalized.

Difficulty

The obvious route to a strong law for a martingale, Doob's maximal inequality applied along a geometric subsequence, fails at the first step: $(\bar S_n)$ is not a martingale, because each new step reweights all earlier terms. The maximum of $\bar S_n$ over a block of indices therefore needs a separate maximal inequality, and it is there that the monotonicity of the weights is indispensable. A second difficulty is quantitative: the exponential tail bound must be summable over blocks whose growth is controlled only through (4.9), which is weaker than the variance-type condition of Theorem 2, so the block sizes and the constants $\varepsilon/(6+\varepsilon)$ , $\varepsilon^2/64$ and $1+\varepsilon/3$ have to be chosen to fit together.

Formalization scope

Conventions committed to in Lean:

Indices start at $1$ : sums run over Finset.Icc 1 n, and $a_0$ , $x_0$ are never used. Every hypothesis on $a$ and $x$ is quantified over $n\ge1$ .
The filtration is a Mathlib Filtration ℕ. Its first $\sigma$ -field plays the role of $\mathfrak A_0$ and is arbitrary rather than trivial; the paper's $\mathfrak A_0=\{\emptyset,\Omega\}$ is a special case, so the formal statements are at least as general.
"Positive increasing" is read as $a_n>0$ and $a_n\le a_{n+1}$ (nondecreasing), the weaker hypothesis.
(4.9) is stated literally as a little- $o$ relation (IsLittleO along atTop). $A_n\to\infty$ is not a hypothesis, since it follows from positivity and monotonicity.
The conclusion is convergence of the real sequence $\bar S_n(\omega)/A_n$ to $0$ for almost every $\omega$ , which contains both the upper and the lower tail; a statement giving only $\limsup\le0$ is not the goal. No real-valued limsup is used anywhere.
Probabilities are real-valued (μ.real); conditional expectations are Mathlib's μ[f | ℱ n].

A formalization of the goal that replaces $\bar S_n$ by the direct sums $a_1x_1+\dots+a_nx_n$ , drops the monotonicity of the weights, or strengthens (4.9) to $a_n/A_n=o(1/\log A_n)$ or to $a_n^2/\sum_{j\le n}a_j^2\to0$ states a different theorem and does not count.

A complete development needs the Azuma moment bound in conditional-expectation form, conditional Chebyshev arguments on events, the Borel–Cantelli lemma (in Mathlib) and elementary real analysis of the blocks. The one-sided Azuma inequality and the maximal inequality (4.15) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. https://doi.org/10.2748/tmj/1178243286
Y. S. Chow, Some convergence theorems for independent random variables, Annals of Mathematical Statistics 37 (1966), 1482–1493.
J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

8 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Discrete Dynamic Programming 2: A Stationary Policy Is Nearly Optimal as the Discount Factor Tends to 1 Exactly When It Maximizes x(g) and, Among Those, y(g)Research Paper

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4(e)

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

x(f_0) \ge x(g)\ \ \forall g \in F;\qquad \exists f^* \in F^* := \{g : x(g) = x(f_0)\}\ \text{with}\ y(f^*) \ge y(g)\ \forall g \in F^*;

g^{(\infty)} \text{ is nearly optimal} \iff x(g) = x(f^*) \text{ and } y(g) = y(f^*).

Milestones and intermediate results

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

The mission also states, as intermediate results:

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 2: Given α ≥ c(C_OPT), the Weighted Potential-Function Algorithm Never Fails and Pays at Most (6+o(1)) α log m log nResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3.4

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

10 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 3: Every Deterministic Online Algorithm Has Competitive Ratio at Least kr on the Block FamilyResearch Paper

Motivation

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

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

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

Setting

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

Two families are used.

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

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

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

Formalization targets

Goal: Proposition 4.2

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

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

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

6 thms2 active usersReviewed

Completed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

The Online Set Cover Problem 1: A Deterministic O(log m log n)-Competitive Algorithm for Unweighted Online Set CoverResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

When the adversary gives an element $j$ :

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

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

Formalization targets

Goal: Theorem 2.3

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

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

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

Milestones

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

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

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

\Phi_e\le\Phi_s,

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

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

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

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

Selected references

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

7 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 1: Independence of Irrelevant Alternatives with a Universal Benchmark Yields Logit Selection ProbabilitiesResearch Paper

Motivation

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

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

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

Setting

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

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

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

Formalization targets

Goal: footnote 3 with Equation (12)

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

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

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

Milestones, in the paper's order

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

7 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 1: Deterministic Double Greedy Achieves 1/3 of the OptimumResearch Paper

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$ . Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$ , a randomized local search achieving $2/5$ , and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$ .
Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$ -approximation (this mission) and a randomized linear-time $1/2$ -approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ , and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$ . In iteration $i = 1, \dots, n$ it computes

a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$ , $Y_i = Y_{i-1}$ ; otherwise $X_i = X_{i-1}$ , $Y_i = Y_{i-1} \setminus \{u_i\}$ . A tie adds $u_i$ . After $n$ iterations $X_n = Y_n$ , which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$ , which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$ . In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$ ,

X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).

Milestones

Lemma II.1. For every $1 \le i \le n$ , $a_i + b_i \ge 0$ .
The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$ .
Lemma II.2. For every $1 \le i \le n$ ,

f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].

The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$ .
Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$ .

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$ , is the template the paper then refines into the randomized $1/2$ -approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$ , which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$ , not against $OPT$ . For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$ ") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$ .
The tie rule is line 5's $a_i \ge b_i$ : ties add $u_i$ .
Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$ , because $f(OPT)$ may be $0$ .
Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$ -approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$ , without which $f \equiv 0$ would satisfy it.
Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$ . A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$ " would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

9 thms2 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Weighted Sums of Certain Dependent Random Variables 1: Weighted Sums of Bounded Multiplicative Systems Grow at Most Like √(2Bₙ² log n)Research Paper

Motivation

Weighted sums of dependent random variables occur when the weights change with the observation horizon. Even if each random variable is bounded and centered, allowing the weights in row $n$ to be chosen anew makes an almost-sure statement about all large $n$ different from a bound on a single finite sum. Kazuo Azuma's 1967 paper treats this situation under a finite-product moment condition called class [M]. Its first main theorem bounds every row of an arbitrary real triangular array at the scale given by that row's Euclidean norm and $\log n$ .

The condition is useful because it allows dependence. The paper notes that bounded martingale differences provide examples, but Theorem 1 is stated directly for class [M], without introducing a filtration in the result. The conclusion therefore records the property of the random variables actually used by this part of the paper, rather than restricting the mission to one familiar source of examples. Azuma, §1 and Theorem 1.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$ . Let $x_1,x_2,\ldots$ be real measurable random variables. They form a bounded multiplicative system with unit bounds if $|x_k|\le1$ almost surely for every $k\ge1$ , and

E\!\left[\prod_{k\in S}x_k\right]=0 \quad\text{for every nonempty finite }S\subseteq\{1,2,\ldots\}.

The indices in $S$ are distinct. Taking a singleton shows $E[x_k]=0$ ; taking sets of two, three, or more indices imposes the full condition used in the paper. Pairwise zero correlations by themselves do not state class [M]. All bounds and moment conditions are for the positive indices, so $x_0$ is outside the mathematical sequence. Azuma, p. 357, property [M].

For each $n\ge1$ , choose real coefficients $a_{n1},\ldots,a_{nn}$ . There is no relation required between different rows. Define the weighted sum $T_n$ and its weight norm $B_n$ by

T_n=\sum_{k=1}^{n}a_{nk}x_k, \qquad B_n=\left(\sum_{k=1}^{n}a_{nk}^{2}\right)^{1/2}.

Both definitions use the source's 1-based indices. A row of zero weights has $B_n=0$ and $T_n=0$ almost surely; such rows remain within the theorem. Azuma, p. 359, §3.

Formalization targets

The goal is Theorem 1, display (3.1): for every bounded multiplicative system and every real triangular array,

\limsup_{n\to\infty} \frac{|T_n|}{\sqrt{2B_n^2\log n}}\le1 \qquad P\text{-almost surely}.

The normalizing constant is exactly $2$ , and the upper bound is exactly $1$ . The mission does not assume that $B_n$ grows, converges, or stays positive. In Lean, the target is stated as the equivalent operational bound: for each $\delta>0$ , almost every outcome eventually satisfies $|T_n|\le(1+\delta)\sqrt{2B_n^2\log n}$ . This includes zero-weight rows without assigning a meaning to a real quotient $0/0$ .

The milestone list follows results displayed in the paper: the corrected convexity inequality (2.2), Lemma 1's exponential moment estimate (2.1), the exponential estimate in the proof of Theorem 1 with its factor $2$ , and the almost-sure finite exponential series on the next page. Lemma 1 gives, for arbitrary real $b_1,\ldots,b_n$ and $t\in\mathbb R$ ,

E\exp\!\left(t\sum_{k=1}^{n}b_kx_k\right) \le \exp\!\left(\frac{t^2}{2}\sum_{k=1}^{n}b_k^2\right).

The paper prints (2.2) with a missing factor $b_{nk}$ in its linear term. The mission records the printed text as provenance and states the corrected inequality in Lean; the printed version fails already when $b_{nk}=2$ and $x_k=t=1$ . Azuma, pp. 357–360.

Significance

Theorem 1 turns an exponential moment bound for each finite weighted sum into a single almost-sure assertion along an entire triangular array. It gives a scale that adapts to the actual coefficients in each row: two arrays with different row norms receive different bounds, while no regularity across rows is required. The result is also the starting point for the weighted strong-law corollaries that follow it in the paper. Azuma, Theorem 1 and Corollary 1.

The mathematical theorem has been proved since 1967. This mission's remaining work is a machine-checked Lean proof of the exact theorem and its listed intermediate statements. A complete development would add reusable formal statements for bounded multiplicative systems and for their finite exponential moments. Those objects could support later work on dependent sums without importing a filtration or a stronger independence assumption. The proposal statements compile as open goals; compilation alone does not supply proofs.

Difficulty

The usual first step for independent bounded variables is to factor the exponential moment into one-variable expectations. Class [M] does not assume independence, so that factorization is unavailable. The condition controls every product with distinct indices, while allowing other dependence. The almost-sure conclusion must also hold when the coefficients change arbitrarily with $n$ : bounds that depend on one fixed row do not by themselves settle what happens for all sufficiently large rows. Finally, rows with $B_n=0$ require a statement that preserves the theorem rather than excluding them by an added positivity hypothesis.

Formalization scope

The Lean development represents the probability law by a measure $\mu$ with IsProbabilityMeasure μ, and a random sequence by $x:\mathbb N\to\Omega\to\mathbb R$ . It uses measurable variables and states the unit bound almost surely at every positive index. The class [M] predicate quantifies over every nonempty finite set of positive indices; no conditional expectations, filtration, symmetry, or independence hypotheses enter Theorem 1. Finite products and finite weighted sums use ordinary real multiplication and Finset.Icc 1 n. The triangular weights have type $\mathbb N\to\mathbb N\to\mathbb R$ , and only entries with $1\le k\le n$ contribute.

The norm $B_n$ is the nonnegative real square root of the sum of squared weights. Real.log is zero at $n=0$ and $n=1$ in Lean, but the target is eventually quantified, so its asymptotic content concerns large $n$ . The exponential estimate is stated for $n\ge1$ . If $B_n=0$ , Lean's total division returns zero in the exponent's quotient; all weights in that row are zero, making this extension valid. In the almost-sure series, the term at index zero is set to zero. The source's limsup is represented by eventual inequalities for every positive excess, avoiding a real-valued limsup default on unbounded sequences.

The definition of class [M] includes every finite product, including singletons; replacing it by pairwise orthogonality would change the theorem. Measurability and the almost-sure unit bounds ensure that the finite products and the exponential functions in Lemma 1 are integrable, so their Lean integrals represent expectations. Contributions toward proofs of the corrected convexity bound, the moment estimate, the exponential series, and the final almost-sure step are all within scope. The finite-product predicate and the exponential estimate are reusable beyond this mission.

Selected references

Kazuo Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. DOI: 10.2748/tmj/1178243286.

7 thms2 active usersReviewed

Convex Optimization Machine Learning Probability+1·Captain: mikedeng1

Stability and Generalization 4: Relative-Entropy Regularization of Mixtures Has Uniform Stability M²/(λm)Research Paper

Motivation

A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size $m$ changes the loss of the output at every point by at most $\beta$ , the generalization error exceeds the empirical error by roughly $2\beta + (4m\beta + M)\sqrt{\ln(1/\delta)/(2m)}$ with probability $1-\delta$ (their Theorem 12). The bound is useful only when $\beta = O(1/m)$ , and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.

Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate $1/(\lambda m)$ . The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.

Setting

Let $\Theta$ be a measurable space with a reference measure $\nu$ , and write $d\theta$ for integration against $\nu$ . A base class $\mathcal H = \{h_\theta : \theta \in \Theta\}$ is indexed by $\Theta$ , and $r(h_\theta, z) \in [0, M]$ is the loss of the base hypothesis $h_\theta$ at an example $z \in Z$ .

The algorithm outputs a density $g$ with respect to $\nu$ : a measurable, nonnegative, integrable $g : \Theta \to \mathbb R$ with $\int_\Theta g\,d\theta = 1$ . $F$ denotes the set of all densities. A density is scored by the averaged loss

\ell(g, z) = \int_\Theta r(h_\theta, z)\, g(\theta)\, d\theta \qquad (28),

the expected loss of a randomized predictor that draws $h_\theta$ from $g$ . The relative entropy of $g$ to $g'$ is

K(g, g') = \int_\Theta g(\theta) \ln \frac{g(\theta)}{g'(\theta)}\, d\theta \in [0, \infty],

with $K(g, g') = +\infty$ when $g\,\nu$ is not absolutely continuous with respect to $g'\,\nu$ or the integrand is not integrable.

Fix a prior $f_0 \in F$ , a parameter $\lambda > 0$ , and a training set $S = (z_1, \dots, z_m)$ . The algorithm returns a minimizer over $F$ of

R_r(g) = \frac1m \sum_{j=1}^m \ell(g, z_j) + \lambda K(g, f_0) \qquad (29).

For an index $i$ , the truncated objective is $R_r^{\setminus i}(g) = \frac1m \sum_{j \ne i} \ell(g, z_j) + \lambda K(g, f_0)$ , and $f^{\setminus i}$ denotes one of its minimizers over $F$ .

Formalization targets

Goal: Theorem 24

For every minimizer $f$ of (29), every minimizer $f^{\setminus i}$ of the truncated objective, and every example $z$ ,

|\ell(f, z) - \ell(f^{\setminus i}, z)| \le \frac{M^2}{\lambda m}.

Milestones

$M$ -admissibility of (28) (§5.2.3, p. 518): $|\ell(g,z) - \ell(g',z)| \le M \int_\Theta |g - g'|\,d\theta$ .
Pinsker's inequality, $L^1$ form (proof of Theorem 24): $\tfrac12 \bigl(\int_\Theta |g - g'|\,d\theta\bigr)^2 \le K(g, g')$ for densities $g, g'$ .
Lemma 21 (p. 513): for a differentiable convex regularizer $N$ on a vector space and a $\sigma$ -admissible loss,

d_N(f, f^{\setminus i}) + d_N(f^{\setminus i}, f) \le \frac{1}{\lambda m}\Bigl(\ell(f^{\setminus i}, z_i) - \ell(f, z_i) - d_{\ell(\cdot, z_i)}(f^{\setminus i}, f)\Bigr) \le \frac{\sigma}{\lambda m}|\Delta f(x_i)|.

Bregman divergence of the relative entropy (proof of Theorem 24): $d_{K(\cdot, f_0)}(g, g') = K(g, g')$ .
$L^1$ displacement bound (proof of Theorem 24):

\int_\Theta |f - f^{\setminus i}|\,d\theta \le \frac{M}{\lambda m}.

Significance

Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order $M^2/(\lambda m) + (M^2/\lambda + M)\sqrt{\ln(1/\delta)/m}$ . The proof also yields the $L^1$ bound $\int |f - f^{\setminus i}| \le M/(\lambda m)$ , which by itself gives classification stability $M/(\lambda m)$ for base hypotheses with values in $\{-1, 1\}$ (remark after Theorem 24, p. 518).

The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in $L^1$ form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.

Difficulty

The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy $K(\cdot, f_0)$ is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity $d_{K(\cdot,f_0)} = K$ needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the $+\infty$ values of $K$ . Pinsker's inequality itself requires a separate argument at the level of general measures.

Formalization scope

Densities are IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral $d\theta$ is always against ν, never Lebesgue measure.
The base loss is r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).
$K$ is InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts $K$ to a real number with toReal would send $K = +\infty$ to $0$ and make the worst densities minimizers; that reading is excluded.
The minimizers are given as hypotheses: f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.
Corrected reading of the algorithm on $S^{\setminus i}$ . The goal is stated in the pairwise form of the paper's proof: $f^{\setminus i}$ minimizes the truncated objective with factor $1/m$ , the analogue of (20), not (29) run on the $m-1$ points of $S^{\setminus i}$ with factor $1/(m-1)$ .
Corrected display. The objective displayed before Theorem 24 has $\ell(g, z)$ inside the sum; (29) has $\ell(g, z_i)$ , which is used.
Lemma 21 is stated as printed, in its differentiable case, on a real normed space whose elements act as functions on $X$ through a linear map; the goal does not instantiate it. The Bregman identity is stated with the explicit gradient $\ln(g'/f_0) + 1$ , for $f_0, g' > 0$ , finite $K(g, f_0)$ , $K(g', f_0)$ , and integrable $g \ln(g'/f_0)$ .

Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.

Selected references

O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Pinsker's inequality). https://doi.org/10.1002/0471200611
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Bregman divergences, Appendix C of the paper). https://doi.org/10.1515/9781400873173

11 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Stability and Generalization 2: Exponential Generalization Bounds for Uniformly Stable AlgorithmsResearch Paper

Motivation

A learning algorithm is judged by its generalization error: the expected loss of the hypothesis it outputs on a fresh example. That quantity depends on an unknown distribution, so it is estimated from the training data, by the empirical error (the average loss on the training set) or the leave-one-out error (the average loss on each training point of the hypothesis trained without it). Classical learning theory controls the gap between these estimates and the true error uniformly over a hypothesis class, through its VC dimension or covering numbers. Such bounds say nothing useful about algorithms that search very large or infinite-dimensional spaces, such as support vector machines and regularization networks in a reproducing kernel Hilbert space.

Bousquet and Elisseeff (JMLR 2 (2002) 499–526) replaced the capacity of the class by a property of the algorithm, its stability: how much its output changes when one training example is removed. Their exponential bound for uniformly stable algorithms is the starting point of the stability approach to generalization, which was later used for stochastic gradient descent (Hardt, Recht and Singer, 2016) and differential privacy, and sharpened by Feldman and Vondrák (2019) and Bousquet, Klochkov and Zhivotovskiy (2020).

Timeline. Rogers and Wagner (1978) and Devroye and Wagner (1979) bounded the leave-one-out error of local rules such as k-nearest neighbours through their stability. McDiarmid (1989) proved the bounded-differences inequality. Lugosi and Pawlak (1994) combined it with smoothed error estimates. Kearns and Ron (1999) named hypothesis and error stability and related them to the VC dimension. Bousquet and Elisseeff (2002) introduced uniform stability and proved the exponential bounds this mission formalizes.

Setting

Let $Z = X \times Y$ be a measurable space of labelled examples with an unknown probability distribution $D$ . A training set $S = (z_1, \dots, z_m)$ is drawn from $D^m$ . A learning algorithm $A$ maps a training set to a hypothesis $A_S : X \to Y'$ . It is deterministic and symmetric: it depends on the training set only as a multiset, so it is a function Multiset (X × Y) → (X → Y'), defined for training sets of every size. For a cost $c$ , the loss of a hypothesis $f$ at $z = (x, y)$ is $\ell(f, z) = c(f(x), y)$ .

Given $S$ , write $S^{\setminus i}$ for $S$ with its $i$ -th example removed, and $S^i$ for $S$ with $z_i$ replaced by an independent draw $z_i' \sim D$ . The three errors are

R = \mathbb E_{z \sim D}[\ell(A_S, z)], \qquad R_{\mathrm{emp}} = \frac1m \sum_{i=1}^m \ell(A_S, z_i), \qquad R_{\mathrm{loo}} = \frac1m \sum_{i=1}^m \ell(A_{S^{\setminus i}}, z_i).

An algorithm has uniform stability $\beta$ at sample size $m$ (Definition 6) if for every $S \in Z^m$ , every $i$ and every $z \in Z$ ,

|\ell(A_S, z) - \ell(A_{S^{\setminus i}}, z)| \le \beta .

As a function of the sample size this constant is written $\beta_m$ .

Formalization targets

Goal: Theorem 12

If $A$ has uniform stability $\beta$ and $0 \le \ell(A_S, z) \le M$ for all $z$ and all training sets $S$ , then for every $m \ge 1$ and $\delta \in (0,1)$ , each of the following holds, separately, with probability at least $1 - \delta$ over $S \sim D^m$ :

R \le R_{\mathrm{emp}} + 2\beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}, \qquad (11)

R \le R_{\mathrm{loo}} + \beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}. \qquad (12)

Milestones

McDiarmid's inequality (Theorem 2): for measurable $F : Z^m \to \mathbb R$ with $|F(S) - F(S^i)| \le c_i$ , $P_S[F - \mathbb E_S F \ge \epsilon] \le e^{-2\epsilon^2/\sum_i c_i^2}$ .
Uniform stability $\beta$ implies $|\ell(A_S, z) - \ell(A_{S^i}, z)| \le 2\beta$ (p. 504).
Lemma 7: the bias identities for $\mathbb E_S[R - R_{\mathrm{emp}}]$ , $\mathbb E_S[R(A,S^{\setminus i}) - R_{\mathrm{loo}}]$ and $\mathbb E_S[R - R_{\mathrm{loo}}]$ .
$R - R_{\mathrm{emp}}$ and $R - R_{\mathrm{loo}}$ have bounded differences $c_i = 4\beta + M/m$ .
$\mathbb E_S[R - R_{\mathrm{emp}}] \le 2\beta$ and $\mathbb E_S[R - R_{\mathrm{loo}}] \le \beta$ .
The tail bounds $P_S[R - R_{\mathrm{emp}} > \epsilon + 2\beta] \le \exp(-2m\epsilon^2/(4m\beta+M)^2)$ and the leave-one-out analogue.

Significance

When $\beta = O(1/m)$ both bounds are $O(1/\sqrt m)$ , with constants that do not depend on any capacity of the hypothesis space. Later sections of the paper show that Tikhonov regularization in a reproducing kernel Hilbert space has $\beta = O(1/(\lambda m))$ , so the theorem gives generalization bounds for support vector regression, kernel ridge regression and, through a smoothed loss, soft-margin classification. The theorem is also the template for later stability bounds: the decomposition into a bias term controlled by stability and a deviation term controlled by a concentration inequality recurs throughout the literature.

The result has been proved since 2002, and replace-one variants appear in textbooks (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Theorem 14.2; Shalev-Shwartz and Ben-David, Chapter 13). On Prove2Me the replace-one textbook version is not formalized, and Mathlib at the platform's environment has no McDiarmid inequality. This mission asks for a machine-checked proof of the paper's remove-one version with its exact constants, and a reusable McDiarmid inequality with per-coordinate constants.

Difficulty

The deterministic steps (the bias identity and the bounded-differences estimates) are short on paper. The central difficulty is McDiarmid's inequality itself: it needs a martingale argument along the coordinates of a product measure, or an equivalent tensorization of conditional sub-Gaussian bounds, with the Doob martingale $\mathbb E[F \mid z_1, \dots, z_k]$ expressed through partial integration over Measure.pi. Hoeffding's inequality for sums, which Mathlib has, does not apply directly: $R - R_{\mathrm{emp}}$ is not a sum of independent terms. A second, bookkeeping difficulty is Lemma 7: the identities rest on exchanging $z_i$ with $z_i'$ and on the symmetry of $A$ , which in Lean means measure-preserving coordinate permutations of $D^m \otimes D$ and multiset equalities such as $S^{i\,\setminus i} = S^{\setminus i}$ .

Formalization scope

Conventions committed to by the Lean statements:

An algorithm is a function of a multiset; this is how symmetry is encoded. Samples are Fin m → X × Y, and $S^i$ is Function.update.
The law of $S$ is Measure.pi (fun _ => D) with D a probability measure; $z_i'$ and $z$ are independent draws, integrated against the product (Measure.pi fun _ => D).prod D.
The paper's standing assumption that all functions are measurable is one hypothesis: $(S, z) \mapsto \ell(A_S, z)$ is measurable for every sample size. With the bound $0 \le \ell(A_T, z) \le M$ for training sets $T$ of every size, every expectation is a genuine integral, so no bound can hold because a non-integrable expectation defaults to $0$ .
Uniform stability quantifies over every sample, every index and every point, not almost every one.
"With probability at least $1 - \delta$ " means the $D^m$ -measure of the failure set is at most $\delta$ . The two bounds (11) and (12) are separate statements, joined by a conjunction; they are not claimed for one joint event.
The paper assumes $\beta_m$ is non-increasing in $m$ and bounds $\beta_{m-1}$ by $\beta_m$ (p. 504). The leave-one-out bound (12) and its milestones carry the explicit hypothesis of uniform stability $\beta$ at size $m-1$ ; the empirical bound (11) does not.
McDiarmid's inequality sums $c_i^2$ over $i = 1, \dots, m$ ; the paper's printed upper index $n$ is a slip.
When a displayed tail bound has a zero denominator, its formal statement uses the limiting bound $0$ . In McDiarmid's inequality this is the constant-function case; in the stability tails the loss is identically zero.

The stability notion is the paper's remove-one notion. A formalization with replace-one stability would prove a different theorem with different constants, and the published FoundationsML_Stability_UniformlyStable (replace-one) is therefore not used.

The development needs the published loss, empirical-error and generalization-error definitions from Foundations of Machine Learning, a McDiarmid inequality on product measures (reusable for any bounded-differences argument), and the coordinate-exchange lemmas for Measure.pi behind Lemma 7. Contributions of a general McDiarmid inequality, of exchangeability lemmas for product measures, and of proofs of any milestone are welcome.

Selected references

O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989) 148–188. https://doi.org/10.1017/CBO9781107359949.008
L. Devroye and T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Trans. Inform. Theory 25 (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087
M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11 (1999) 1427–1453. https://doi.org/10.1162/089976699300016304
M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240
V. Feldman and J. Vondrák, High probability generalization bounds for uniformly stable algorithms with nearly optimal rate, COLT 2019. https://arxiv.org/abs/1902.10710
O. Bousquet, Y. Klochkov and N. Zhivotovskiy, Sharper bounds for uniformly stable algorithms, COLT 2020. https://arxiv.org/abs/1910.07833
M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.

13 thms2 active usersReviewed

Machine Learning Probability Reinforcement Learning·Captain: mikedeng1

Minimax Regret Bounds for Reinforcement Learning II: High-Probability Regret Bound for UCBVI with a Bernstein–Freedman BonusResearch Paper

Why finite-horizon reinforcement learning needs a variance-sensitive bound

An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.

Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.

The MDP, interaction, and algorithm

Let $\mathcal S$ and $\mathcal A$ be nonempty finite state and action sets with cardinalities $S$ and $A$ . A stationary transition kernel $P(y\mid x,a)$ is a probability distribution on next states $y$ for every current state $x$ and action $a$ . The reward $R(x,a)$ is deterministic, known to the learner, and lies in $[0,1]$ . These are the conditions of Assumption 1 and §2. Episodes have $H\ge1$ steps; $K$ episodes comprise $T=KH$ interactions.

A policy $\pi$ chooses an action for each state and step. Its value $V_h^\pi(x)$ is the expected reward from step $h$ through the final step when the state at $h$ is $x$ ; the terminal value is $V_{H+1}^\pi=0$ . The optimal value $V_h^*(x)=\sup_\pi V_h^\pi(x)$ ranges over all deterministic policies of this form. At the start of episode $k$ , the environment may choose the initial state using the completed episodes. The learner then fixes a policy $\pi_k$ , observes transitions during the episode, and updates counts for the next episode. Its regret is

\operatorname{Regret}(K)=\sum_{k=1}^{K}\bigl(V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})\bigr).

For each state-action pair, $N_k(x,a,y)$ counts transitions to $y$ in episodes before $k$ , and $N_k(x,a)=\sum_yN_k(x,a,y)$ . When the latter is positive, $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$ . The count $N'_{k,h}(y)$ records previous episodes whose state at step $h$ was $y$ . Algorithms 2 and 4 compute optimistic $Q_{k,h}$ backward from zero terminal value, take a minimum with the previous episode's $Q$ estimate and with $H$ , and choose a maximizing action at every state. Previously unseen pairs receive $Q_{k,h}=H$ . The Bernstein–Freedman bonus uses the empirical variance of $V_{k,h+1}$ under $\widehat P_k$ and an additional term based on $N'_{k,h+1}$ ; the algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$ .

Formalization targets

The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every $\delta>0$ , write $L=\ln(5HSAT/\delta)$ . The target is the exact bad-event form of the printed high-probability bound:

\Pr\!\left\{\operatorname{Regret}(K)>30HL\sqrt{SAK}+2500H^2S^2AL^2+4H^{3/2}\sqrt{KL}\right\}\le\delta.

The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's $\ell_1$ error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.

What the result and its formalization supply

The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in $K$ in the leading term, with explicit dependence on $S$ , $A$ , and $H$ . The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.

A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.

Where the difficulty lies

The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.

Formalization scope and conventions

The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining $V^*$ ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.

Lean indexes the $H$ steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index $H+1$ . At $N'_{k,h+1}(y)=0$ , Algorithm 4's quotient is interpreted as infinite and the capped term is $H^2$ ; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$ , while Theorem 2's bound uses $L=\ln(5HSAT/\delta)$ . For Eq. (26), the appendix ends its sums at $H-1$ under a shifted terminal convention; the local statement includes all $H$ reward steps and the terminal value $V_{H+1}=0$ used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of $2$ under the square root present in that display.

Theorem 2 retains its printed $2500H^2S^2AL^2$ term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.

Selected references

M. G. Azar, I. Osband, and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Preprint.

13 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

WordRAM to Turing machines: polynomial simulation for NP proofsResearch Paper

References:

Mean Field Games: Numerical Methods for the Planning Problem II: Solutions of the Penalized Scheme Converge to a Solution of the Discrete Planning Scheme as ε → 0Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Mean Field Games: Numerical Methods for the Planning Problem I: The Discrete Planning Scheme Has a Solution, Given by a Fenchel–Rockafellar Saddle PointResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Optimal Sequencing of a Single Machine Subject to Precedence Constraints: Repeatedly Placing Last a Least-Cost Eligible Job Yields a Minmax Optimal SequenceResearch Paper

Motivation

Setting

Formalization targets

Goal: the rule is optimal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Variance-based Regularization with Convex Objectives II: A Covering-Number Certificate and Oracle Inequality for the Robust MinimizerResearch Paper

Motivation

Setting

Formalization targets

Goal: the oracle inequality (16)

The certificate (15)

Supporting results (milestones)

Significance

Difficulty

Formalization scope

Selected references

The Price of Stability for Network Design with Fair Cost Allocation III: Weighted Games in Which Each Edge Serves at Most Two Players Have a Potential and a Nash EquilibriumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance I: Quadratic Potential Functions Bound Mean Response Times in Open NetworksResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Approximation Algorithms for Stochastic Inventory Control Models 2: The Triple-Balancing Policy Costs at Most Three Times the Optimum for Stochastic Lot-SizingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems II: The Łojasiewicz Inequality for Convex Subanalytic Functions on Bounded SetsResearch Paper