All missions

Motivation

Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the $n$-player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?

The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.

Setting

Let $G$ be a finite simple graph on vertex set $\{1,\dots,n\}$ with adjacency matrix $A_G$ and degree matrix $D_G$. Its Laplacian is $L_G = D_G^{-1}A_G - I$. $G$ is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree $\delta(G)$, and $L_G$ is then symmetric with eigenvalues $\lambda^G_1,\dots,\lambda^G_n\in[-2,0]$. The empirical eigenvalue distribution is $\mu_G = \frac1n\sum_i\delta_{\lambda^G_i}$.

Fix a horizon $T>0$, a volatility $\sigma>0$ and a weight $c>0$. Player $v$ controls the state

$$dX_v(t) = \alpha_v(t,\boldsymbol X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],$$

driven by independent Brownian motions, with Markovian feedback controls $\alpha_v$, and pays

$$J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2dt + c\,\Big|X_v(T) - \tfrac1{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].$$

On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with $Q_G(x) = \det(I - xL_G)^{1/n}$ and $f_G$ the solution of $f_G' = c\,Q_G'(f_G)$, $f_G(0) = 0$ on $[0,T]$, the feedback is $\alpha^G_i(t,\boldsymbol x) = -e_i^\top P_G(t)\boldsymbol x$ with $P_G(t) = -f_G'(T-t)L_G(I - f_G(T-t)L_G)^{-1}$. The resulting equilibrium state process $\boldsymbol X^G$ is Gaussian, and the value is $\mathrm{Val}(G) = \frac1n\sum_v J_v$.

For a probability measure $\mu$ define $Q_\mu(x) = \exp\int_{[-2,0]}\log(1-x\lambda)\,\mu(d\lambda)$, so that $Q_{\mu_G} = Q_G$.

Formalization targets

Goal: Theorem 2.6

Let $(G_n)$ be finite transitive graphs without isolated vertices, $|G_n|\to\infty$, with $\boldsymbol X^{G_n}(0) = 0$, and suppose $\mu_{G_n}\to\mu$ weakly for a probability measure $\mu$. Then (1) the ODE $f_\mu' = c\,Q_\mu'(f_\mu)$, $f_\mu(0) = 0$ has a unique solution on $[0,T]$; (2) for every vertex sequence $k_n$ and $t\in[0,T]$,

$$\mathrm{Law}\big(X^{G_n}_{k_n}(t)\big)\to\mathcal N\big(0,V_\mu(t)\big),\qquad V_\mu(t) = \sigma^2\int_0^t\int_{[-2,0]}\Big(\frac{1-\lambda f_\mu(T-t)}{1-\lambda f_\mu(T-s)}\Big)^2\mu(d\lambda)\,ds;$$

(3) the empirical measure $\frac1{|G_n|}\sum_i\delta_{X^{G_n}_i(t)}$ converges weakly in probability to $\mathcal N(0,V_\mu(t))$; (4)

$$\lim_{n\to\infty}\mathrm{Val}(G_n) = -\frac{\sigma^2}2\log\int_{[-2,0]}\frac{-\lambda}{1-\lambda f_\mu(T)}\,\mu(d\lambda).$$

Milestones

The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of $f_\mu$ in $\mu$ (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of $f_\mu$ (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.

Significance

Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs $\mu = \delta_{-1}$ and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, $\mu$ is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.

The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.

Difficulty

Parts (2) and (4) follow from the finite-graph formulas once $f_{G_n}\to f_\mu$ uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.

Formalization scope

The Lean development lives in namespace GraphLQGame.Asymptotics.

• Vertices $\{1,\dots,n\}$ are Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with $N_k\to\infty$.
• $L_G$ is the random-walk Laplacian above, not Mathlib's lapMatrix. $\mu_G$ is built from the real roots of the characteristic polynomial of $L_G$, with multiplicity.
• Weak convergence of measures on $\mathbb R$ is convergence of $\int h\,d\mu_k$ for every bounded continuous $h$. Weak convergence in probability of the empirical measure is convergence in probability of $\int h\,dm^{G_n}(t)$ for every bounded continuous $h$.
• A state process is a pathwise strong solution of (2.1) on its own probability space, driven by a standard Brownian motion and adapted to its completed filtration. Statements about several graphs are statements about laws.
• Costs are $[0,\infty]$-valued lower integrals; the value is computed after asserting finiteness.
• In $P_G$, $f_G'(T-t)$ is written as its ODE value $c\,Q_G'(f_G(T-t))$. ODE solutions are constrained on $[0,T]$ (or on $\mathbb R_+$ for Propositions 3.2 and 3.3), with uniqueness stated on that domain.
• The Gaussian law $\mathcal N(0,V)$ is gaussianReal 0 V.toNNReal; $V_\mu(t)\ge0$.

The goal quantifies over every solution $f_{G_n}$, $f_\mu$ and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for $u = v$, where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.

Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; published in Math. Oper. Res., 2022, https://doi.org/10.1287/moor.2021.1179. https://arxiv.org/abs/2005.14102
• F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 3.20, Gaussian Poincaré inequality). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6

Why mean field approximations on graphs need a threshold

Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate $O(1/\sqrt n)$ (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.

Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.

Setting

Let $G$ be a finite simple graph on the vertex set $V=\{1,\dots,n\}$; $u\sim v$ means $u$ and $v$ are adjacent and $\deg_G(v)$ is the number of neighbours of $v$. Fix a horizon $T>0$, a volatility $\sigma>0$ and a cost weight $c>0$. Each player $v\in V$ controls a real state $X_v$ through

$$dX_v(t)=\alpha_v(t,\boldsymbol X(t))\,dt+\sigma\,dW_v(t),\qquad t\in[0,T],$$

where $W_1,\dots,W_n$ are independent standard Brownian motions and $\boldsymbol X=(X_u)_{u\in V}$. A Markovian control $\alpha_v\in\mathcal A_G$ is a Borel function of time and the full state $\boldsymbol X(t)\in\mathbb R^V$, of linear growth. The cost of player $v$ under a profile $\boldsymbol\alpha=(\alpha_u)_{u\in V}$ is

$$J_v(\boldsymbol\alpha)=\frac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2\,dt+c\,\Big|X_v(T)-\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big],$$

and $\frac12\mathbb E[\int_0^T|\alpha_v|^2dt+c|X_v(T)|^2]$ for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector $\boldsymbol\varepsilon\in\mathbb R^V_+$, a profile is a Markovian $\boldsymbol\varepsilon$-Nash equilibrium if no player $v$ can lower its cost by more than $\varepsilon_v$ by switching unilaterally to another control $\beta\in\mathcal A_G$, written $(\beta,\boldsymbol\alpha^{-v})$.

The mean-field control is

$$\alpha^{\mathrm{MF}}(t,y)=\frac{-cy}{1+c(T-t)},\qquad \alpha^{\mathrm{MF}}_v(t,\boldsymbol x)=\alpha^{\mathrm{MF}}(t,x_v):$$

each player looks only at its own state, as if its neighbours' average were frozen at its mean.

Formalization targets

Goal: Theorem 2.11

Define $\epsilon^G_v=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{\deg_G(v)}}$ if $\deg_G(v)\ge1$ and $\epsilon^G_v=0$ if $\deg_G(v)=0$, and with the minimal degree $\delta(G)=\min_v\deg_G(v)$,

$$\epsilon_G=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{1\vee\delta(G)}}.$$

Then, with zero initial states, the state equation for $(\alpha^{\mathrm{MF}}_v)_{v\in V}$ has a solution, and

$$(\alpha^{\mathrm{MF}}_v)_{v\in V}\ \text{is an } \epsilon^G\text{-Nash equilibrium and an } \epsilon_G\text{-Nash equilibrium on } G.$$

Milestones

1. Lemma 7.2: $\alpha^{\mathrm{MF}}$ is optimal for the one-player problem $\min\frac12\mathbb E[\int_0^T\beta^2dt+c|Y(T)|^2]$, $dY=\beta\,dt+\sigma dW$, over all progressively measurable $\beta$.
2. Isolated vertices (p. 40): $J_v(\boldsymbol\alpha)=\inf_\beta J_v(\beta,\boldsymbol\alpha^{-v})$ when $\deg_G(v)=0$.
3. (7.7): under $\alpha^{\mathrm{MF}}$, $(X_u(T))_u$ are i.i.d. $N(0,\sigma^2T/(1+cT))$, so the neighbour average has second moment $\sigma^2T/(\deg_G(v)(1+cT))$.
4. Steps (1), (2), (3) (p. 41): a lower bound on $J_v(\beta,\boldsymbol\alpha^{-v})$, an energy bound for deviations no worse than the zero control, and the comparison with $J_v(\boldsymbol\alpha^{\mathrm{MF}})$.
5. (7.5): for $\deg_G(v)\ge1$ and every admissible $\beta$, $J_v(\beta,\boldsymbol\alpha^{-v})\ge J_v(\boldsymbol\alpha)-\epsilon^G_v$.

Significance

The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control $\alpha^{\mathrm{MF}}$ is an $\epsilon_{G_n}$-Nash equilibrium with $\epsilon_{G_n}\to0$, and the vector form says more: if the average of $(1\vee\deg_{G_n}(v))^{-1/2}$ over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate $\deg_G(v)^{-1/2}$ quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.

Difficulty

The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player $v$ couples its terminal state with the neighbours' average through a cross term $\mathbb E[\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\,Y_v(T)]$, and the deviation $\beta(t,\boldsymbol Y(t))$ may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.

Formalization scope

The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:

• vertices are Fin n (the paper's $\{1,\dots,n\}$ become $\{0,\dots,n-1\}$), the state space is EthierKurtz.SDEState n, and $G$ is any SimpleGraph (Fin n); isolated vertices are allowed;
• controls are Borel with linear growth on $[0,T]$ only; their values at other times are never used, and the formula for $\alpha^{\mathrm{MF}}$ outside $[0,T]$ is evaluated with Lean's total division;
• a solution of the state equation is a pathwise strong solution carrying its own probability space and an $n$-dimensional standard Brownian motion; costs are $[0,\infty]$-valued lower Lebesgue integrals, and the Nash inequality is required for every solution of the profile and of each deviation (faithful by strong uniqueness);
• $T,\sigma,c>0$ are the standing assumptions of §2.1;
• initial states are zero. The printed theorem does not mention $X(0)$; the paper fixes non-random initial states that are "in many cases" zero, and the whole proof is for $X(0)=0$. With non-zero initial states the claim fails in general, so this is a disclosed hypothesis;
• the goal also asserts that the state equation for $\alpha^{\mathrm{MF}}$ has a solution, so the Nash property cannot hold vacuously; Lemma 7.2 is stated over every continuous adapted solution of its SDE, and Step (2) carries, as an explicit hypothesis, the comparison with the zero control that its proof uses.

A formalization in which $\alpha^{\mathrm{MF}}$ is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.

Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47 (2022). https://arxiv.org/abs/2005.14102
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications II, Springer, 2018. https://doi.org/10.1007/978-3-319-56436-4
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6 (2006), 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• H. Pham, Continuous-time Stochastic Control and Optimization with Financial Applications, Springer, 2009 (verification theorem, Theorem 3.5.2). https://doi.org/10.1007/978-3-540-89500-8

Motivation

The circumference $c(G)$ of a graph $G$ is the length of a longest cycle. Extremal graph theory asks how many edges force a long cycle. The Erdős–Gallai theorem (1959) states that every $n$-vertex graph has at most $c(G)(n-1)/2$ edges. Bondy (1971) strengthened it by counting only the edges near a longest cycle: if $C$ is a longest cycle of length $c$, the number of edges with at most one endpoint in $C$ is at most $\tfrac c2(n-c)$, and at most $\lfloor c/2\rfloor (n-c)$ when $G$ is 2-connected. Since $V(C)$ spans at most $\binom c2$ edges, this implies the Erdős–Gallai bound.

A stability result complements an extremal one: a graph close to the extremal bound must be close in structure to the extremal graphs. Jie Ma and Bo Ning (Combinatorica, 2020; arXiv:1708.00704) proved stability versions of Kopylov's edge theorem for 2-connected graphs of given circumference and of Bondy's theorem above. This mission formalizes their stability version of Bondy's theorem, Theorem 1.12. In the paper it is also one of the two halves of the proof of the main stability theorem; the other half is a separate mission in this series.

Timeline (as recorded in §1 of the paper). Dirac (1952): every 2-connected graph has $c(G)\ge\min\{2\delta(G),|V(G)|\}$. Erdős and Gallai (1959): $e(G)\le c(G)(n-1)/2$. Bondy (1971): the bound on edges with at most one endpoint on a longest cycle, and the degree theorem stated here as Theorem 2.1. Woodall (1976): $e(G)\le f(n,\lfloor c/2\rfloor,c)$ for 2-connected $G$ with circumference $c\le(2n+2)/3$. Kopylov (1977): $e(G)\le\max\{f(n,2,c),f(n,\lfloor c/2\rfloor,c)\}$ for 2-connected $G$ with circumference $c\le n-1$; another proof by Fan, Lv and Wang (2004). Fan (1990): an improved version of Bondy's bound for 2-connected graphs, and average-degree bounds on long paths. Füredi, Kostochka and Verstraëte (2016): stability for Kopylov's theorem when $n\ge 3\lfloor c/2\rfloor$; Füredi, Kostochka, Luo and Verstraëte (2018): the complete stability version, with the families $\mathcal X_{n,c}$, $\mathcal Y_{n,c}$. Ma and Ning (2017 preprint, 2020): the results of this mission.

Setting

All graphs are finite and simple, on the vertex set $\{0,\dots,n-1\}$. A path or cycle of length $k$ has $k$ edges. A graph is 2-connected if it has at least three vertices, is connected, and remains connected after deleting any one vertex. A cycle $C$ is a longest cycle if no cycle of $G$ has more edges; $V(C)$ is its vertex set and $c$ its length.

For a longest cycle $C$, write $e(G-C)+e(G-C,C)$ for the number of edges with at most one endpoint in $C$. A vertex $u$ is an isolated vertex of $G-C$ if $u\notin V(C)$ and every neighbour of $u$ lies on $C$; $d_C(u)$ is its number of neighbours on $C$.

The extremal graphs are:

• $W_{n,k,c}$: a clique $K_{c-k+1}$ together with $n-(c-k+1)$ further vertices, each adjacent to the same $k$ vertices of the clique and to nothing else.
• $\mathcal X_{n,c}$: graphs on $A\cup B\cup X$ with $A$ a clique of size $\lfloor c/2\rfloor$, $B$ and $X$ stable, $A$ completely joined to $B$, and two vertices $a\in A$, $b\in B$ such that $N(x)=\{a,b\}$ for all $x\in X$.
• $\mathcal Y_{n,c}$: graphs on $A\cup B\cup Y$ with $A$ a clique of size $\lfloor c/2\rfloor$, $B$ stable, $A$ completely joined to $B$, $G[Y]$ a star forest with at least two stars each having an edge, and two distinct $a,b\in A$ such that each star $S$ has exactly $\{a,b\}$ as outside neighbourhood and, if $|V(S)|\ge 3$, its leaves have degree $2$ and a common neighbour in $\{a,b\}$.

$G\subseteq W$ means that $G$ is isomorphic to a subgraph of $W$.

Formalization targets

Goal: Theorem 1.12

Let $G$ be 2-connected on $n$ vertices and $C$ a longest cycle of length $c$ with $10\le c\le n-1$. If

$$e(G-C)+e(G-C,C) > \left(\left\lfloor \tfrac c2\right\rfloor-1\right)(n-c),$$

then $G\subseteq W_{n,\lfloor c/2\rfloor,c}$, or $c$ is odd and $G$ is a subgraph of a member of $\mathcal X_{n,c}\cup\mathcal Y_{n,c}$.

Milestones

1. Theorem 2.1 (Bondy): all but one vertex of degree $\ge k$ in a 2-connected graph give $c(G)\ge\min\{n,2k\}$.
2. Theorem 2.2 (Fan), first assertion: a longest $(x,y)$-path is at least as long as the average degree of the other vertices.
3. Lemma 2.3: a 2-connected component $H$ of $G-C$ with average degree $r$ satisfies $c\ge 2r$, with equality only for a clique attached to two common vertices of $C$.
4. Theorem 3.2: without connectivity and for $4\le c\le n-1$, the same edge condition gives $c\in\{6,7,9\}$, or a vertex off $C$ with $\lfloor c/2\rfloor$ neighbours on $C$, or a cycle $C'$ meeting $C$ in at most one vertex with $|C'|\ge 2\lfloor c/2\rfloor-3$ (disjoint) or $\ge 2\lfloor c/2\rfloor-1$ (one common vertex).
5. Theorem 3.1: for 2-connected $G$ and $10\le c\le n-1$, an isolated vertex $u$ of $G-C$ with $d_C(u)=\lfloor c/2\rfloor$.
6. Lemma 3.3: such a vertex forces $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ when $c$ is even, and $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ or $G$ in a member of $\mathcal X_{n,c}\cup\mathcal Y_{n,c}$ when $c\ge 9$ is odd.

Significance

In $W_{n,\lfloor c/2\rfloor,c}$ every one of the $n-c$ vertices off a longest cycle sends $\lfloor c/2\rfloor$ edges to the cycle, so Bondy's bound $\lfloor c/2\rfloor(n-c)$ is attained. Theorem 1.12 says that exceeding $(\lfloor c/2\rfloor-1)(n-c)$ already leaves only three structures: a subgraph of $W_{n,\lfloor c/2\rfloor,c}$, or for odd $c$ a subgraph of a member of $\mathcal X_{n,c}$ or $\mathcal Y_{n,c}$. In the paper it is one of the two cases of the proof of the main stability theorem (Theorem 1.9): a graph with many edges and a longest cycle $C$ has either many edges with at most one endpoint on $C$, handled here, or many edges inside $V(C)$, handled by the closure argument of the companion mission.

The result is proved in the paper; none of it, nor Bondy's or Fan's theorems, is formalized on the platform or in Mathlib. The mission produces machine-checked statements of the goal, of the cited tools (Bondy's Theorem 2.1, Fan's Theorem 2.2, Lemma 2.3), and of the steps Theorems 3.1, 3.2 and Lemma 3.3, together with reusable definitions of 2-connectivity, longest cycles and the extremal families.

Difficulty

The obvious approach counts edges at the vertices off $C$: each such vertex has at most $\lfloor c/2\rfloor$ neighbours on $C$, since otherwise two consecutive cycle vertices would let the cycle be extended. This bound is far from enough. The edge count also includes edges between vertices off $C$, and components of $G-C$ can be large, 2-connected, and attached to $C$ in complicated ways. The bound $(\lfloor c/2\rfloor-1)(n-c)$ has to be beaten by every such configuration at once, and Theorem 3.2 states exceptional small cycle lengths $c\in\{6,7,9\}$ for which the analysis does not close. A second difficulty is the passage from one vertex of degree $\lfloor c/2\rfloor$ to a global description of $G$: in the odd case, the structure of every component of $G-C$ has to be determined, which is where the families $\mathcal X_{n,c}$ and $\mathcal Y_{n,c}$ appear.

Formalization scope

Graphs are SimpleGraph (Fin n) with decidable adjacency. A cycle is a closed walk C : G.Walk u u with C.IsCycle; its length is C.length and its vertex set C.support.toFinset. "Longest cycle" is the predicate that every cycle of $G$ is at most as long as $C$; no supremum of cycle lengths is used. 2-connectivity is: at least three vertices, connected, and connected after deleting any one vertex. It is stated for an arbitrary finite vertex type so that it applies to the induced subgraph $G[H]$ in Lemma 2.3. The edge count off $C$ is the number of edges with an endpoint outside $V(C)$, and $\lfloor c/2\rfloor$ is natural-number division; under the stated bounds every natural-number subtraction is exact.

$W_{n,k,c}$ is defined on fixed labels (clique $\{0,\dots,c-k\}$, hubs $\{0,\dots,k-1\}$), and "$G\subseteq W$" is a graph embedding G ⊑ W. Membership in $\mathcal X_{n,c}$ and $\mathcal Y_{n,c}$ are predicates on labelled graphs, closed under relabelling, and "$G$ is a subgraph of a member" is G ≤ H for some member $H$. No hypothesis is added to any statement. Fan's Theorem 2.2 is stated without its equality characterization.

Trivializing formalizations are ruled out explicitly: the alternative "$c$ is odd and …" is a conjunction, never an implication; the circumference is never a junk supremum; containment in $W$ is up to isomorphism, never ≤ on fixed labels; and 2-connectivity excludes $K_2$ and disconnected graphs.

The definitions are reusable for any work on circumference, longest cycles and Bondy–Erdős–Gallai-type problems. Contributions of proofs of the cited tools (Bondy's and Fan's theorems) are especially welcome, as is a proof of Erdős–Gallai's edge theorem, which the proof of Theorem 3.2 uses and which is posed elsewhere on the platform.

Selected references

• J. Ma and B. Ning, Stability results on the circumference of a graph, Combinatorica 40 (2020); arXiv:1708.00704v2. https://arxiv.org/abs/1708.00704 , https://doi.org/10.1007/s00493-019-3843-4
• J. A. Bondy, Large cycles in graphs, Discrete Mathematics 1 (1971/72), no. 2, 121–132.
• G. Fan, Long cycles and the codiameter of a graph, I, Journal of Combinatorial Theory, Series B 49 (1990) 151–180.
• P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Mathematica Academiae Scientiarum Hungaricae 10 (1959) 337–356.
• G. Fan, X. Lv, P. Wang, Cycles in 2-connected graphs, Journal of Combinatorial Theory, Series B 92 (2004) 379–394.
• Z. Füredi, A. Kostochka, J. Verstraëte, Stability in the Erdős–Gallai theorems on cycles and paths, Journal of Combinatorial Theory, Series B 121 (2016) 197–228.
• Z. Füredi, A. Kostochka, R. Luo, J. Verstraëte, Stability in the Erdős–Gallai theorem on cycles and paths, II, Discrete Mathematics 341 (2018) 1253–1263.
• G. N. Kopylov, Maximal paths and cycles in a graph, Soviet Mathematics Doklady 18 (1977) 593–596.
• D. R. Woodall, Maximal circuits of graphs I, Acta Mathematica Academiae Scientiarum Hungaricae 28 (1976) 77–80.

Motivation

Distributionally robust stochastic optimization (DRSO) chooses a decision $x$ to minimize the worst expected loss $\sup_{\mu\in\mathfrak M}\mathbb E_\mu[\Psi(x,\xi)]$ over an ambiguity set $\mathfrak M$ of probability distributions, instead of the expectation under one estimated distribution. When $\mathfrak M$ is a ball around a nominal distribution $\nu$ (often the empirical distribution of data) in the Wasserstein distance, the set contains distributions with supports different from that of $\nu$, and the worst case is driven by how far mass can be moved and how fast the loss grows along the way. This makes Wasserstein balls a standard choice in data-driven optimization, statistical learning and operations research.

The inner problem, a supremum over an infinite-dimensional set of measures, is not directly computable. Gao and Kleywegt (arXiv:1604.02199v3) show that it equals a minimization over a single scalar multiplier, for an arbitrary Polish space and nominal distribution and a merely measurable loss.

Timeline. Esfahani and Kuhn (2018, doi:10.1007/s10107-017-1172-1) proved a strong duality for $p=1$ and empirical $\nu$ on $\mathbb R^m$, giving finite convex reformulations for piecewise-affine losses. Blanchet and Murthy (2019, doi:10.1287/moor.2018.0936) proved duality for general optimal transport costs on Polish spaces under upper semicontinuity of the loss, with a dual over pairs $(\lambda,\varphi)$. Gao and Kleywegt's result, first posted in 2016 and published in Mathematics of Operations Research (2023, doi:10.1287/moor.2022.1275), covers every order $p\in[1,\infty)$, every nominal $\nu$ and every measurable loss with finite growth rate, with a dual in one variable.

Setting

Let $(\Xi,d)$ be a Polish space (complete, separable metric) with its Borel $\sigma$-algebra, $\mathcal P(\Xi)$ the Borel probability measures, $p\in[1,\infty)$ and $\theta>0$. The decision variable is suppressed: $\Psi:\Xi\to\mathbb R$ is a Borel measurable loss with $\Psi\in L^1(\nu)$ for a fixed nominal distribution $\nu\in\mathcal P(\Xi)$.

The Wasserstein distance of order $p$ is given by

$$W_p^p(\mu,\nu)=\inf\Big\{\int_{\Xi\times\Xi}d^p(\xi,\zeta)\,\gamma(d\xi,d\zeta):\ \gamma\in\mathcal P(\Xi\times\Xi),\ \pi^1_\#\gamma=\mu,\ \pi^2_\#\gamma=\nu\Big\}.$$

The primal value is the worst-case expectation over the Wasserstein ball,

$$v_P=\sup_{\mu\in\mathcal P(\Xi)}\Big\{\int_\Xi\Psi\,d\mu:\ W_p(\mu,\nu)\le\theta\Big\}.$$

The regularization operator is $\Phi(\lambda,\zeta)=\inf_{\xi\in\Xi}\{\lambda d^p(\xi,\zeta)-\Psi(\xi)\}\in\mathbb R\cup\{-\infty\}$, the dual objective is $h(\lambda)=\lambda\theta^p-\int_\Xi\Phi(\lambda,\zeta)\,\nu(d\zeta)$, and the dual value is $v_D=\inf_{\lambda\ge0}h(\lambda)$. The growth rate of $\Psi$ is

$$\kappa=\inf\Big\{\lambda\ge0:\int_\Xi\Phi(\lambda,\zeta)\,\nu(d\zeta)>-\infty\Big\}\in[0,\infty],$$

with $\kappa=\infty$ if no $\lambda$ qualifies. The lemmas also use the near-optimal distances $\overline D(\lambda,\zeta)$ and $\underline D(\lambda,\zeta)$, the limits as $\varepsilon\downarrow0$ of the largest and smallest $d^p(\xi,\zeta)$ over $\varepsilon$-minimizers $\xi$ of $\lambda d^p(\cdot,\zeta)-\Psi$.

In Lean these objects are DRSOWass.Duality.wassPow, vP, Phi, dualObj, vD, growthRate, DUpper, DLower.

Formalization targets

Goal: Theorem 1 (p. 17)

If $\kappa<\infty$, then

$$v_P=v_D<\infty.$$

This is the printed theorem: an equality of values together with finiteness. It fixes no constant and needs no regularity of $\Psi$ beyond measurability and integrability.

Milestones

1. Proposition 1, weak duality $v_P\le v_D$ (no growth condition).
2. Lemma 3(i), (ii), (v): $\nu$-measurability of $\Phi(\lambda,\cdot)$, $\overline D$, $\underline D$, $\overline D_0$, $\underline D_0$, and $\nu$-measurable selections of near-optimal and far points.
3. Lemma 4(i)–(iii): monotonicity, upper semicontinuity and concavity of $\Phi(\cdot,\zeta)$, the bound $(\lambda_2-\lambda_1)\overline D(\lambda_2,\zeta)\le-\Psi(\zeta)-\Phi(\lambda_1,\zeta)$, and one-sided derivative bounds.
4. Lemma 5: $h$ is $\infty$ on $[0,\kappa)$, finite on $(\kappa,\infty)$, convex, lower semicontinuous, coercive, and has a minimizer $\lambda^*\in[\kappa,\infty)$.
5. Lemmas 6 and 7: explicit $\varepsilon$-optimal distributions in the ball, built from push-forwards of $\nu$, in the cases $\lambda^*>\kappa$, $\lambda^*=\kappa=0$ and $\lambda^*=\kappa>0$.

Significance

The result. Strong duality turns the worst-case expectation over a Wasserstein ball into a convex problem in one scalar, $\min_{\lambda\ge0}\{\lambda\theta^p-\int\Phi(\lambda,\zeta)\,\nu(d\zeta)\}$, where $\Phi$ is a Moreau–Yosida-type regularization of $-\Psi$. For finite-supported $\nu$ this yields finite-dimensional reformulations of DRSO; the paper derives from it the structure of worst-case distributions (Corollaries 1 and 2) and applications to two-stage problems, point processes and Gaussian nominal distributions. The growth rate $\kappa$ separates the finite case (this theorem) from the case $v_P=\infty$ (Proposition 2).

Formalizing it. The theorem is proved in the paper; to the best of current knowledge none of it is machine-checked. The mission produces a formal statement of the duality on general Polish spaces, together with reusable pieces: extended-valued integrals, the regularization operator and its one-sided derivatives, measurable selection on Polish spaces, and push-forward constructions of near-optimal measures. Formal proofs of Lemma 3 also give measurable-selection tools that Mathlib does not yet provide in this form.

Difficulty

Weak duality is a one-line Lagrangian argument. The difficulty is attainment from the primal side: one must construct, for every $\varepsilon>0$, a distribution in the ball whose expectation is within $\varepsilon$ of $v_D$. A worst-case distribution need not exist (when $\lambda^*=\kappa>0$ mass escapes to infinity), so a compactness argument on $\mathcal P(\Xi)$ fails; and $\Psi$ is only measurable, so the infimum defining $\Phi(\lambda,\zeta)$ cannot be reduced to a countable one, and the measurability of $\Phi(\lambda,\cdot)$ and of near-optimal transport maps needs projection and measurable-selection theorems for analytic sets. The case analysis on whether the dual minimizer exceeds $\kappa$ is forced by the possible non-differentiability of $h$ at $\kappa$.

Formalization scope

• $\Xi$ carries MetricSpace, CompleteSpace, SecondCountableTopology and BorelSpace instances; $\nu$ is a probability measure; $d^p$ is dist ξ ζ ^ p with real $p\ge1$.
• $\Psi$ is assumed Borel measurable in addition to $\Psi\in L^1(\nu)$; the paper's p. 5 states the theorem for a measurable $\Psi$, and $\int\Psi\,d\mu$ for $\mu\ne\nu$ requires it.
• $W_p^p$ is the published RWPI.SqrtLasso.transportCost with cost $d^p$, an infimum over probability couplings in $[0,\infty]$; $W_p(\mu,\nu)\le\theta$ is written $W_p^p(\mu,\nu)\le\theta^p$.
• Integrals that may be infinite are the published ModelRiskOT.Duality.extIntegral, $\int\varphi^+-\int\varphi^-$ in $[-\infty,\infty]$ (with $\infty-\infty=-\infty$). $\Phi$, $h$, $v_P$, $v_D$ are EReal-valued; $\kappa$, $\overline D$, $\underline D$ are ENNReal-valued, so $\kappa=\infty$ is representable and the empty infimum is $\infty$.
• $\limsup_{\varepsilon\downarrow0}$ and $\liminf_{\varepsilon\downarrow0}$ in $\overline D$, $\underline D$ are written as the monotone infimum and supremum over $\varepsilon>0$. $\nu$-measurability is null-measurability for functions and almost-everywhere measurability for maps $\Xi\to\Xi$.
• Repaired or adjusted statements: Lemma 4(i)'s sup inequality is stated for $\varepsilon>0$ (the printed $\varepsilon=0$ case fails when an arg min is empty); in Lemma 6, (7)'s weights $p_1,p_2$ are read as $p_1^\varepsilon,p_2^\varepsilon$; Lemma 5(v) carries $\kappa<\infty$; Lemma 4(iii)'s right derivative is a limit in $(-\infty,\infty]$.
• A trivializing formalization is ruled out: integrals are not Bochner integrals (which would give a non-integrable $\mu$ the value $0$), $\kappa$ is not a real infimum (which would give $0$ when no $\lambda$ qualifies), and the supremum in $v_P$ ranges over probability measures in the ball only, which is nonempty because it contains $\nu$.

A complete development needs couplings and gluing in Mathlib's measure theory, the measurable projection theorem and a measurable selection theorem on Polish spaces, and one-sided derivatives of concave extended-valued functions; the first three are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal (e.g. through the Blanchet–Murthy dual), and the companion result Proposition 2 ($\kappa=\infty\Rightarrow v_P=v_D=\infty$) are welcome.

Selected references

• R. Gao, A. J. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, arXiv:1604.02199v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1604.02199
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Why trade credit terms matter

Most business-to-business sales are not paid in cash on delivery. The supplier lets the buyer pay later, which is trade credit, and often offers a discount for paying early. In the classic "2/10 net 30" the buyer gets 2% off for paying within 10 days and otherwise owes the full price in 30 days. Trade credit is a major source of short-term finance for firms. Empirical work documents both forms of contract: net terms, with one price and no discount, and two-part terms, with an early-payment discount. The discounts are large, and they vary a lot from one buyer to another (Petersen and Rajan 1997; Klapper, Laeven and Rajan 2012). The implied interest rate on a forgone discount is often far above a bank loan's. This raises two questions: why do cash-poor buyers use trade credit at all, and when should a supplier offer a discount?

Yang and Birge (Management Science 2018) answer this in a supplier–retailer model with a financially constrained retailer, who can finance inventory with a bank loan, with trade credit, or with both. Their answer is risk sharing. Trade credit is repaid out of realized sales, so the supplier bears part of the demand risk. She can therefore induce a larger order than a price-only contract does. The model builds on the selling-to-the-newsvendor model of Lariviere and Porteus (2001), and it complements the supplier-versus-bank analysis of Kouvelis and Zhao (2012). This mission formalizes the paper's main result on the structure of the optimal contract.

The model

A retailer buys a single good from a supplier at unit cost $c$ and sells it at unit price $p=1$. Demand is random with density $f$ on $[0,\infty)$. Its distribution function is $F(x)=\int_0^x f$, the complementary distribution function is $\bar F=1-F$, the failure rate is $h=f/\bar F$, and the generalized failure rate is $g(x)=x\,h(x)$. Demand has an increasing failure rate (IFR). The retailer has cash $K>0$.

The supplier offers a cash price $w_c$ and a credit price $w_t$, with $c\le w_c\le w_t\le 1$. The early-payment discount is $d_t=1-w_c/w_t$. If the retailer's cash does not cover his cash purchases, he borrows from a competitive bank. The bank loan is senior to trade credit. A bank and a supplier recovering a defaulted claim lose fractions $\alpha_b$ and $\alpha_t$ of what they recover, with $\alpha_b,\alpha_t\in[0,1]$.

Default is described by two thresholds. The bank-loan default threshold $\theta_b$ is the demand below which the bank is not repaid in full, and it equals the amount owed to the bank. The trade-credit default threshold $\theta_t\ge\theta_b$ is the demand below which the supplier is not repaid in full. The retailer uses a bank loan iff $\theta_b>0$, and uses trade credit iff $\theta_t>\theta_b$.

The paper shows (p. 13) that the supplier's problem can be written in the thresholds alone. Let

$$\hat F_b(x)=\bar F(x)[1-\alpha_b g(x)],\qquad C(\theta)=\frac{K+\int_0^\theta\hat F_b}{\hat F_b(\theta)}-\theta,$$ $$Q(\theta_b,\theta_t)=\min\{q\ge0:\ q\bar F(q)=[\theta_t+C(\theta_b)]\bar F(\theta_t)\}.$$

The retailer orders $Q$, the prices are $w_t=\bar F(Q)/\bar F(\theta_t)$ and $w_c=\hat F_b(\theta_b)w_t$, and the discount is $d_t=1-\hat F_b(\theta_b)$. The supplier's expected profit is

$$\Pi_s=K+\int_0^{\theta_t}\bar F(x)\,dx-c\,Q(\theta_b,\theta_t)-\Big[\alpha_b\int_0^{\theta_b}x\,dF(x)+\alpha_t\int_{\theta_b}^{\theta_t}(x-\theta_b)\,dF(x)\Big].$$

She maximizes $\Pi_s$ over a domain $\Theta$ of thresholds. A maximizer is an optimal trade credit contract. Net terms correspond to $\theta_b^*=0$, which is $d_t^*=0$. Two-part terms correspond to $\theta_b^*>0$.

Formalization targets

Goal: Proposition 3 (p. 15)

For every optimal contract $(\theta_b^*,\theta_t^*)$:

$$\theta_t^*>0\ \Longrightarrow\ \theta_b^*<\theta_t^*\qquad(\text{trade credit is always used}).$$

If $\alpha_t=0$, or if $K$ is sufficiently large, then $\theta_b^*=0$ and $d_t^*=0$ (net terms, no bank loan). If $\alpha_t>0$ and $K$ is sufficiently small, then

$$0<\theta_b^*<\theta_t^*,\qquad d_t^*>0\qquad(\text{two-part terms, both bank loan and trade credit}).$$

"Sufficiently large" and "sufficiently small" are existential thresholds on $K$ that depend on the data $(f,c,\alpha_b,\alpha_t)$, not on the contract.

Milestones

They are listed in the order the proof uses them:

1. Lemma C.4: $C$ is increasing, and convex when $\alpha_b=0$.
2. Corollary 3: $Q$ increases in $\theta_b$ and in $\theta_t$.
3. Lemma C.8: at $\alpha_b=0$, $\Pi_s$ is concave in $\theta_b$.
4. Lemma C.7: $Q$ increases in $\alpha_b$ and $K$.
5. Lemma C.9: $\Pi_s$ is concave in $\theta_t$.
6. Proposition 6, first sentence: $\Pi_s^*$ decreases in $\alpha_b$ and $\alpha_t$.

Significance

Proposition 3 is the paper's prediction about inventory financing portfolios. Once the supplier sets the terms, a retailer who needs external financing always uses trade credit. Early-payment discounts appear only when supplier default is costly and the retailer is cash-poor. A discount is then the supplier's way of moving part of the financing to the bank. The paper uses this to explain why discounts go to small, risky buyers, as observed by Klapper et al. (2012). The comparative statics of §5 (Propositions 4–6) are built on the same reduced problem.

The result is proved on paper but has not been formalized. The appendix lemmas it rests on (C.4, C.7, C.8, C.9) are stated without proof ("available upon request"). A machine-checked development would therefore settle whether these lemmas hold on the domain where the paper uses them. It would also produce a reusable library: IFR demand with failure rates, the bank-loan pricing kernel $\hat F_b$, and the implicit order quantity $Q$.

Difficulty

The order quantity $Q$ is defined implicitly, as the smaller root of a unimodal equation, and the paper's arguments differentiate through it with the implicit function theorem. Every derivative of $\Pi_s$ therefore involves $1/(\bar F(Q)[1-g(Q)])$, which blows up at the edge of $\Theta$ where $Q=g^{-1}(1)$. The density is only assumed continuous, so $\hat F_b$ and $C$ need not be differentiable when $\alpha_b>0$. Monotonicity and concavity have to be argued from the integral forms, or under a smoothness assumption the paper does not state.

The obvious argument for "sufficiently large $K$" also fails. It perturbs the optimum at $K$ just below $M^*=g^{-1}(1)\bar F(g^{-1}(1))$, but there the domain shrinks to a sliver near $\theta_t=0$, and the derivative of $\Pi_s$ in $\theta_t$ at $\theta_t=0$ can be negative. For exponential demand it tends to $-\infty$ as $K\to M^*$. The proof's claim that $\theta_t^*>0$ there is not part of the theorem. Part 1 for general $\alpha_b$ is reduced to $\alpha_b=0$ through Proposition 6, which requires comparing optima over domains that themselves depend on $\alpha_b$.

Formalization scope

All objects live in TradeCredit.Terms.Model.

Demand. Demand is a density $f:\mathbb R\to\mathbb R$ that is continuous on $[0,\infty)$, positive on $[0,\infty)$, zero on $(-\infty,0)$, integrable with total mass $1$, and has a weakly increasing failure rate on $[0,\infty)$. $F$ is the interval integral of $f$ from $0$. The normalizations are $p=1$ and $s=0$. The parameters satisfy $0<c<1$, $\alpha_b,\alpha_t\in[0,1]$ and $K>0$.

Domain. $\Theta$ is the printed set of Corollary 3 ($\theta_t\ge\theta_b\ge0$ and $[\theta_t+C(\theta_b)]\bar F(\theta_t)\le M^*$) plus two pinned constraints: $\theta_t\le Q(\theta_b,\theta_t)$ (that is, $w_t\le1$) and $c\le w_c$. These are the image under (11) of §3.1's $c\le w_c\le w_t\le 1$, which the printed $\Theta$ omits.

Statements. $Q$ is the infimum of the nonnegative roots. "The optimal contract" means every maximizer of $\Pi_s$ on $\Theta$. Existence of a maximizer is not asserted; the paper does not prove it. Monotonicity is weak, and concavity is Mathlib's ConcaveOn on the sections of $\Theta$. Proposition 6 is stated by comparing attained values with $\Pi_s^*=\sup_\Theta\Pi_s$.

Not in scope. The retailer's best response (Proposition 1) and the bijection between thresholds and contracts are not formalized. The goal is about the paper's own reduced problem. Lemma 1's first-order conditions are not a milestone: as printed they fail at a corner optimum $\theta_b^*=\theta_t^*=0$, and they need $C'$, which is not defined under a merely continuous density.

Ruling out trivialization. The large-$K$ clause quantifies over $K\in[\underline K,M^*)$ with $\underline K<M^*$. For $K\ge M^*$ the domain $\Theta$ has no point with $\theta_t>0$ and every "for every optimal contract" statement holds vacuously, so a large-$K$ clause that reached only those values would be empty.

Welcome contributions. Lemmas on IFR densities (positivity of $\bar F$, finiteness of the mean, monotonicity of $g$ and existence of $g^{-1}(1)$), the root structure of $q\bar F(q)$, and boundedness of $\Pi_s$ on $\Theta$ are reusable beyond this paper.

Source. The source PDF is the authors' accepted manuscript (LBS Research Online, eprint 801). All page numbers are the manuscript's.

Selected references

• S. A. Yang, J. R. Birge, Trade Credit, Risk Sharing, and Inventory Financing Portfolios, Management Science 64(8), 2018. https://doi.org/10.1287/mnsc.2017.2799
• M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4), 2001. https://doi.org/10.1287/msom.3.4.293.9971
• P. Kouvelis, W. Zhao, Financing the Newsvendor: Supplier vs. Bank, and the Structure of Optimal Trade Credit Contracts, Operations Research 60(3), 2012. https://doi.org/10.1287/opre.1120.1040
• M. A. Petersen, R. G. Rajan, Trade Credit: Theories and Evidence, Review of Financial Studies 10(3), 1997. https://doi.org/10.1093/rfs/10.3.661
• L. Klapper, L. Laeven, R. Rajan, Trade Credit Contracts, Review of Financial Studies 25(3), 2012. https://doi.org/10.1093/rfs/hhr122

Motivation

DC programming is the minimization of a function $f = g - h$ that is a difference of two convex functions. The class contains every $C^2$ function on a compact convex set and most nonconvex models of sparse learning, clustering, combinatorial relaxations and robust optimization, and its standard method, the DC Algorithm (DCA), replaces $h$ by its affine minorant at the current iterate and solves a convex program at each step. DCA was introduced by Pham Dinh Tao in 1985 and developed jointly with Le Thi Hoai An from 1994 on (Pham Dinh & Le Thi 1998); the survey of Le Thi & Pham Dinh 2018 collects thirty years of that work.

DCA is guaranteed to reach critical or strongly critical points, notions that depend on the chosen decomposition $g - h$, while a decomposition-free notion, directional (d-)stationarity of $f$ itself, is what a user of a nonconvex model usually wants. Ahn, Pang & Xin 2017 warned that DC criticality can be much weaker than d-stationarity. Theorem 1 of the 2018 survey (p. 9) states when the two coincide. Its proof is omitted in the paper ("can be easily deduced … It is omitted here").

Setting

Let $X = \mathbb R^n$ with the canonical inner product $\langle\cdot,\cdot\rangle$. Functions take values in $\mathbb R\cup\{\pm\infty\}$. The effective domain of $\varphi$ is $\operatorname{dom}\varphi = \{x : \varphi(x) < +\infty\}$, and $\Gamma_0(X)$ is the set of proper, lower semicontinuous, convex functions $X \to \mathbb R\cup\{+\infty\}$.

The standard DC program is

$$(P_{dc})\qquad \alpha = \inf\{f(x) := g(x) - h(x) : x\in X\},\qquad g, h\in\Gamma_0(X),$$

with the convention $+\infty - (+\infty) = +\infty$, and $\alpha$ is assumed finite. Finiteness of $\alpha$ forces $\operatorname{dom} g\subset\operatorname{dom} h$, so $\operatorname{dom} f = \operatorname{dom} g$.

The subdifferential of $\varphi$ at $x$ is

$$\partial\varphi(x) = \{y\in X : \varphi(x) < +\infty,\ \varphi(v) \ge \varphi(x) + \langle y, v - x\rangle\ \ \forall v\in X\}.$$

A point $x$ is strongly critical for $f = g - h$ if $\emptyset \ne \partial h(x)\subset\partial g(x)$.

The directional derivative of $\varphi$ at $x\in\operatorname{dom}\varphi$ in direction $u$ is $\varphi'(x;u) = \lim_{t\downarrow 0}(\varphi(x+tu) - \varphi(x))/t$. For convex $\varphi$ it equals $\inf_{t>0}(\varphi(x+tu)-\varphi(x))/t$. A point $x\in\operatorname{dom} f$ is d-stationary for $f$ if $f'(x;u)\ge 0$ for every $u\in X$. The support function of $C\subset X$ is $\chi^*_C(u) = \sup_{y\in C}\langle u, y\rangle$, with $\chi^*_\emptyset \equiv -\infty$. Finally, $\operatorname{ri} C$ is the relative interior of $C$, its interior inside the affine hull $\operatorname{aff} C$.

Formalization targets

Goal: Theorem 1(iii)

For $x\in\operatorname{ri}(\operatorname{dom} g)\cap\operatorname{ri}(\operatorname{dom} h)$,

$$x \text{ is d-stationary for } f \iff \emptyset\ne\partial h(x)\subset\partial g(x).$$

Milestones

1. Theorem 1(i): for $x\in\operatorname{dom} g$ with $\partial h(x)\ne\emptyset$,

$$f'(x;u) = g'(x;u) - h'(x;u)\qquad \forall u\in X.$$

2. Theorem 1(ii), first sentence: under the same hypotheses, $x$ is d-stationary iff $g'(x;u)\ge h'(x;u)$ for all $u$.
3. Theorem 1(iv): for $x\in\operatorname{ri}(\operatorname{dom} g)$ with $\partial h(x)\ne\emptyset$, d-stationarity implies strong criticality.
4. Theorem 1(v): for $x\in\operatorname{ri}(\operatorname{dom} h)$, strong criticality implies d-stationarity.

Companion statements

• Theorem 1(ii), second sentence: for $x\in\operatorname{dom} g$, if $g'(x;\cdot) = \chi^*_{\partial g(x)}$ and $h'(x;\cdot) = \chi^*_{\partial h(x)}$, then d-stationarity and strong criticality coincide.
• Theorem 1(vi): if $\operatorname{aff}(\operatorname{dom} g) = \operatorname{aff}(\operatorname{dom} h)$, then $\operatorname{ri}(\operatorname{dom} g)\subset\operatorname{ri}(\operatorname{dom} h)$ and the equivalence holds on $\operatorname{ri}(\operatorname{dom} g)$.

Part (iii) is the goal because it is the equivalence the paper uses to justify DCA, stated under a hypothesis symmetric in $g$ and $h$; (vi) is the more general companion.

Significance

The theorem connects the output of DCA with a stationarity notion intrinsic to $f$. Without it, the strong criticality certified by DCA would be a property of a decomposition rather than of the problem, and different decompositions of the same $f$ could certify different points. With it, at points in the relative interiors of the domains, every strongly critical point is d-stationary, and conversely no d-stationary point is missed by the criticality test.

Parts (i) and (ii) are stated in the paper without proof, and so is the rest of Theorem 1; none of it has a machine-checked proof. The mission produces a formal statement of all six parts with the extended-real conventions made explicit. Three of the printed parts are false as stated without the nonemptiness of $\partial h(x)$; the formal versions add that hypothesis and record a counterexample for each, so the formalization also corrects the printed statement.

Difficulty

The obvious argument writes $f'(x;u) = g'(x;u) - h'(x;u)$ and reads off both directions from $g'\ge h'$. Two steps of it fail. First, the difference can be $-\infty - (-\infty)$ or $+\infty - (+\infty)$, and the limit defining $f'$ need not be the difference of the limits; the nonemptiness of $\partial h(x)$ is exactly what rules out the first case. Second, passing from "$g'(x;\cdot)\ge h'(x;\cdot)$" to "$\partial h(x)\subset\partial g(x)$" needs $h'(x;\cdot)$ to equal the support function of $\partial h(x)$, which holds in the relative interior of $\operatorname{dom} h$ but fails on its relative boundary, where $h'(x;\cdot)$ need not be lower semicontinuous. The relative interior, not the interior, is essential: the domains may be lower-dimensional.

Formalization scope

$X$ is EuclideanSpace ℝ (Fin n), and every function maps into EReal. The published definitions TaoAnDCA.GlobalOpt.Setting supply $\operatorname{dom}$ (effDom), the DC objective with $+\infty - (+\infty) = +\infty$ (dcSub), the subdifferential (subdiff) and $\alpha$ (primalValue); $\Gamma_0(X)$ is the published IsProperClosedConvex. Every statement carries the standing assumptions of Theorem 1 as binders: $g, h\in\Gamma_0(X)$, $\alpha\ne-\infty$ and $\alpha\ne+\infty$. The mission's definitions are:

• convDirDeriv: the convex directional derivative by the paper's infimum formula, in EReal;
• HasDirDerivE: the predicate that the one-sided limit along $t\downarrow 0$ exists in EReal and equals a given value;
• IsDStationary: $x\in\operatorname{dom}\varphi$ and, for every direction, the limit exists and is $\ge 0$;
• IsStronglyCritical: both $\partial h(x)\ne\emptyset$ and $\partial h(x)\subset\partial g(x)$;
• supportFn: the extended-real support function, $-\infty$ on $\emptyset$.

The relative interior is Mathlib's intrinsicInterior ℝ, the affine hull is affineSpan ℝ. The subgradient inequality has the standard sign; display (1) of the paper prints the opposite sign, a slip. The only hypothesis added to the page is $\partial h(x)\ne\emptyset$, in parts (i), (ii) first sentence and (iv), each of which is false without it; parts (ii) second sentence, (iii), (v) and (vi) are stated as printed.

The statement admits trivializing formalizations, which this one rules out. Strong criticality without the nonemptiness of $\partial h(x)$ is vacuous wherever $\partial h(x) = \emptyset$. A d-stationarity defined through limUnder, a real-valued derivative, or "every limit is nonnegative" holds vacuously where the limit does not exist. And $g - h$ written in raw EReal would give $+\infty - (+\infty) = -\infty$.

A complete development needs the monotonicity of convex difference quotients in EReal, limit arithmetic for extended reals, and the formula $\varphi'(x;\cdot) = \chi^*_{\partial\varphi(x)}$ for $\varphi\in\Gamma_0(\mathbb R^n)$ at points of $\operatorname{ri}(\operatorname{dom}\varphi)$ (Rockafellar 1970, Theorem 23.4), together with the nonemptiness of $\partial\varphi$ there. These results on extended-real convex functions are reusable well beyond DC programming, and contributions of them as separate theorems are welcome.

Selected references

• H. A. Le Thi, T. Pham Dinh, DC programming and DCA: thirty years of developments, Mathematical Programming Ser. B 169 (2018), 5–68. https://doi.org/10.1007/s10107-018-1235-y
• T. Pham Dinh, H. A. Le Thi, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM Journal on Optimization 8 (1998), 476–505. https://doi.org/10.1137/S1052623494274313
• M. Ahn, J.-S. Pang, J. Xin, Difference-of-convex learning: directional stationarity, optimality, and sparsity, SIAM Journal on Optimization 27 (2017), 1637–1665. https://doi.org/10.1137/16M1084754
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173