All missions

Motivation

Ride-pooling platforms receive trip requests one at a time and must decide, within a short waiting window, which requests to group into a shared vehicle. A request that is not grouped before its window closes is served alone or lost. Online hypergraph matching with delays is the combinatorial core of this decision: requests are vertices that arrive over time, feasible groups of up to $k$ riders are weighted hyperedges, and the platform must commit irrevocably to disjoint groups while every member of a group is still waiting. Pavone, Saberi, Schiffer and Tsao (arXiv:2009.12022, 2020; journal version Technical Note — Online Hypergraph Matching with Delays, Operations Research, 2022) determine the optimal competitive ratio of this problem in the utility-maximization setting. For $k \ge 3$ no online algorithm beats ratio $1/d$, where $d$ is the waiting time (their Theorem 1, via the adversarial secretary problem), and their Theorem 3 achieves $1/d$ with a polynomial-time algorithm for every fixed $k$. This mission formalizes the achievability half.

Setting

Requests $1, \dots, n$ arrive one per time step; request $i$ arrives at time $i$ and disappears at time $i + d$. A hyperedge $e$ is a non-empty set of requests, its diameter is $\mathrm{diam}(e) = \max e - \min e$, and each hyperedge carries a weight $w(e) \ge 0$. A shareability hypergraph with parameters $(n, d, k)$ is a finite edge set $E$ of subsets of $[n] = \{1,\dots,n\}$ with $\mathrm{diam}(e) < d$ and $|e| \le k$ for all $e \in E$ (Definition 1, p. 2). A matching is a set $M \subseteq E$ of pairwise disjoint hyperedges, of weight $w(M) = \sum_{e\in M} w(e)$. In Online-(k, d)-Max-Matching (Definition 2, p. 3) a hyperedge may be chosen only after all its vertices have arrived and before any of them disappears, and choices are irrevocable.

Greedy (Algorithm 5, p. 15) scans a finite edge set in non-increasing order of weight, ties broken arbitrarily, and keeps every edge disjoint from those already kept.

Randomized-Batching (Algorithm 1, p. 5) draws a shift $Z$ uniformly from $\{0, \dots, d-1\}$ and cuts time into windows

$$V_{z,i} = \{v \in [n] : z + id \le v \le z + (i+1)d - 1\}, \qquad i \in \mathbb Z,$$

with batch edges $E_{z,i} = \{e \in E : e \subseteq V_{z,i}\}$ and $E_z = \bigcup_i E_{z,i}$. At the end of each window it runs an offline subroutine on the batch $W_{z,i} = (V_{z,i}, E_{z,i}, w)$ and commits the result $M_{z,i}$; the output is $M_z = \bigcup_i M_{z,i}$.

Depth-k Greedy (Algorithm 2, p. 7) is the subroutine. With $L$ and $R$ the first and last $k$ vertices of the batch, it enumerates the restricted matchings $\mathcal M_{L,R}$ (Definition 18, p. 19), the matchings whose every edge meets both $L$ and $R$; it extends each $M \in \mathcal M_{L,R}$ by Greedy on the edges avoiding the vertices of $M$, and it returns the heaviest extension.

Formalization targets

Goal: Theorem 3, p. 7 (competitive clause)

For every shift $z$, $M_z$ is a matching of $E$ whose edges each lie inside one window, and for every matching $\widetilde M$ of $E$

$$\mathbb E_Z[w(M_Z)] = \frac1d\sum_{z=0}^{d-1} w(M_z) \;\ge\; \frac{w(\widetilde M)}{d}.$$

The statement holds for every weight-sorted tie-breaking of Greedy.

Milestones

With $\widetilde M_\ell = \{e \in \widetilde M : \mathrm{diam}(e) > d - k\}$ and $\widetilde M_s = \widetilde M \setminus \widetilde M_\ell$:

1. Batch decomposition (proof of Theorem 2, p. 6): the windows partition $[n]$, the batches are disjoint, and $w(M_z) = \sum_i w(M_{z,i})$.
2. Observation 1 (p. 6): $\sum_{z=0}^{d-1}\mathbb 1[e\in E_z] \ge d - \mathrm{diam}(e)$.
3. Lemma 4 (p. 14): Greedy returns a matching $G$ with $w(G) \ge \frac1k w(M)$ for every matching $M$ of a rank-$k$ hypergraph.
4. Observation 3 (p. 19): an edge of a window with $\mathrm{diam}(e) > d - k$ meets both $L$ and $R$.
5. Condition (3) for Depth-k Greedy (p. 19): $w(M_{z,i}) \ge w(\widetilde M_\ell\cap E_{z,i}) + \frac1k w(\widetilde M_s \cap E_{z,i})$.
6. Reduction (4) (p. 18): any subroutine satisfying (3) on every batch gives $\frac1d\sum_z\sum_i w(M_{z,i}) \ge w(\widetilde M)/d$.

Significance

Theorem 3 closes the gap left by the general guarantee of Theorem 2 and Lemma 2 (p. 6), under which any $\rho$-competitive offline subroutine yields ratio $\rho/d$. With plain Greedy this gives only $1/(kd)$ (Corollary 1, p. 7), and an exact subroutine gives $1/d$ but is NP-hard for $k \ge 3$. Together with the $1/d$ upper bound of Theorem 1, Theorem 3 settles the optimal competitive ratio of Online-(k, d)-Max-Matching for $k \ge 3$ and shows that it is attained in polynomial time for each fixed $k$. The batching-plus-restricted-enumeration pattern applies to other online problems in which items have a bounded lifetime.

The result is proved in the paper. To our knowledge none of it is machine-checked: no hypergraph matching model, no Greedy guarantee for weighted $k$-set packing, and no batching argument exists on the platform. Lemma 4, the classical $1/k$ guarantee of Greedy for weighted rank-$k$ hypergraph matching, is cited in the paper without proof ([6, 8]); its formalization is reusable on its own.

Difficulty

The natural attempt is to run Greedy inside each batch. It loses the factor $1/k$ on every edge, and the random shift recovers that factor only for edges that survive batching for at least $k$ of the $d$ shifts, that is, edges of diameter at most $d - k$. A long edge, with diameter above $d - k$, lies in $E_z$ for fewer than $k$ shifts, so its $1/k$ loss is never compensated and the bound degrades to $1/(kd)$. Long edges therefore have to be recovered exactly in every batch. The exact optimum is intractable, so a different handle on long edges is needed. The formal work also has to deal with windows truncated at the ends of $[n]$, with the first partial window, and with arbitrary tie-breaking inside Greedy.

Formalization scope

Vertices are natural numbers and $V = [n]$; hyperedges are Finset ℕ, edge sets are Finset (Finset ℕ), and weights are a function Finset ℕ → ℝ, read only on $E$. The definitions file HyperMatchDelay.Batching.Model fixes these conventions:

• Hyperedges are non-empty, an assumption the paper leaves implicit. $d \ge 1$ and $k \ge 1$ are hypotheses.
• Greedy's arbitrary tie-breaking is an ordering oracle $\sigma$ listing each edge set in non-increasing weight order. Every statement about Greedy holds for every such oracle, independently in every call.
• Windows are indexed by $i \in \{-1, 0, \dots, \lfloor n/d\rfloor\}$ and are pairwise disjoint. This replaces the paper's $0 \le i \le n/d$, which misses the first $z$ requests, and Algorithm 1's overlapping last batch.
• Definition 18's condition $L \cap R = \emptyset$ is dropped. It fails for batches with fewer than $2k$ vertices and no argument uses it.
• The maximizer in Depth-k Greedy is a fixed choice; all maximizers have the same weight.
• The expectation over $Z$ is the average $\frac1d\sum_{z=0}^{d-1}$, and the long/short threshold $\mathrm{diam}(e) > d-k$ is compared in $\mathbb Z$.

The running-time clauses of Theorem 3 and Lemma 4 are not formalized, since there is no cost model. The goal does not assume condition (3) as a hypothesis, and its subroutine is Depth-k Greedy as defined, with Greedy inside it. A single batch containing all of $E$, or an exact offline subroutine, would make the statement a different and easier claim, and the formalization rules both out.

Contributions are welcome on every milestone. Lemma 4 and Observation 1 are independent of the rest. Lemma 4 is the most reusable item: a general Greedy guarantee for weighted set packing.

Selected references

• M. Pavone, A. Saberi, M. Schiffer, M. W. Tsao, Online Hypergraph Matching with Delays, arXiv:2009.12022v1, 2020. https://arxiv.org/abs/2009.12022 (page and theorem numbers in this mission refer to this version; page numbers equal PDF page indices).
• M. Pavone, A. Saberi, M. Schiffer, M. W. Tsao, Technical Note — Online Hypergraph Matching with Delays, Operations Research, 2022 (journal version; not consulted for this mission).
• P. Berman, A d/2 approximation for maximum weight independent set in d-claw free graphs, Nordic Journal of Computing 7(3), 178–184, 2000 (reference [6] of the paper, cited for Lemma 4).
• B. Chandra, M. M. Halldórsson, Greedy local improvement and weighted set packing approximation, Journal of Algorithms 39(2), 223–240, 2001 (reference [8] of the paper, cited for Lemma 4).

Motivation

Double auctions match buy and sell orders at a common price. Stock exchanges, commodity markets and electricity markets use them at their opening and closing auctions and to trade multi-asset portfolios. Economists have long asked how efficient the resulting allocations are. Laboratory work starting with Smith (1962) found that repeated double auctions with few traders reach competitive outcomes quickly (Smith 1962). Since then the phenomenon has been documented in many experimental studies, but it had remained largely unexplained by theory (Pennanen, §1).

Pennanen (arXiv:2001.02071v2, Mathematics of Operations Research 2022) takes agents who bid their indifference prices in a multi-asset double auction, and shows that repeating the auction drives the economy to an efficient allocation. The total surplus left on the table decays like $1/t$.

Setting

A finite nonempty set $I$ of agents trades a finite set $J$ of assets. Agent $i$ holds a portfolio $x_i\in\mathbb R^J$, and an allocation is $x\in\mathbb R^{I\times J}$. Short positions are allowed and there is no free disposal. Agent $i$ has a utility $u_i:\mathbb R^J\to[-\infty,+\infty]$ with effective domain $\operatorname{dom}u_i=\{x_i\mid u_i(x_i)>-\infty\}$. All prices are quoted in a numeraire portfolio $g\in\mathbb R^J$, for example cash.

Assumption 1 holds throughout: each $u_i$ is upper semicontinuous and concave (its hypograph is convex), and $u_i(x_i+rg)>u_i(x_i)$ for $x_i\in\operatorname{dom}u_i$ and $r>0$.

At the endowment $x^0_i$, agent $i$ bids the indifference price

$$D_i(x_i)=\sup\{r\in\mathbb R\mid u_i(x^0_i+x_i-rg)\ge u_i(x^0_i)\},$$

the most the agent would pay for $x_i$ without losing utility. The auctioneer solves the market clearing problem

$$\text{maximize }\sum_{i\in I}D_i(x_i)\quad\text{subject to}\quad\sum_{i\in I}x_i=0,\qquad(P)$$

whose optimum value $CS(x^0)$ is the total consumer surplus available at $x^0$. A market clearing price is a vector $p$ that is a supergradient of every $D_i$ at a solution $\bar x$. Agent $i$ then receives $\bar x_i$ and pays $p\cdot\bar x_i$ units of $g$. An allocation with $CS(x)=0$ is a double auction equilibrium.

In the repeated auction the agents re-bid from their new positions:

$$x^t_i=x^{t-1}_i+\bar x^t_i-(p^t\cdot\bar x^t_i)g,$$

where $\bar x^t$ and $p^t$ clear the $t$-th auction, whose indifference prices are built from $x^{t-1}$.

Two further conditions are used. Assumption 3: no nonzero $x$ with $\sum_ix_i=0$ has every $x_i$ a direction of recession of $u_i$. Assumption 5: for every $r>0$ there is $\delta_i>0$ with $u_i(x_i+rg)\ge u_i(x_i)+\delta_ir$ on the ball $\mathbb B(r)$. Assumption 4, which is needed only for Pareto efficiency, says that an agent who is not at the lowest possible utility can give away a little of $g$ and stay in $\operatorname{dom}u_i$.

Formalization targets

Goal: Theorem 16

Under Assumptions 1, 3 and 5:

1. the iterates $(x^t)$ are bounded;
2. $CS(x^t)$ decreases to $0$, with

$$CS(x^t)\le\frac1t\sum_{i\in I}\frac{u_i(x^t_i)-u_i(x^0_i)}{\delta_i};$$

3. every cluster point $\bar x$ is a double auction equilibrium and is individually rational, $u_i(\bar x_i)\ge u_i(x^0_i)$;
4. under Assumption 4, every cluster point is also Pareto efficient.

The constants $\delta_i$ are those of Assumption 5 at one radius $R$ that is large enough for the whole sequence. The statement holds for every admissible choice of them.

Milestones

The milestones are the results that the proof of Theorem 16 uses, in attack order:

• Lemma 2: regularity of $D_i$.
• Theorem 4: market clearing prices are Lagrange multipliers.
• Remark 6: every auction is a Pareto improvement.
• Lemma 9: (P) recast in terms of utilities.
• Monotonicity of CS along individually rational reallocations.
• Boundedness of the set of feasible individually rational allocations.
• The radius reduction in Assumption 5.
• The per-auction utility gain $u_i(x^t_i)\ge u_i(x^{t-1}_i)+\delta_iCS_i(x^{t-1})$.
• Theorem 11: Pareto allocations coincide with double auction equilibria.

Significance

Theorem 16 is a welfare theorem for a mechanism that is actually used. Agents bid myopically, nobody computes a Walrasian equilibrium, and the allocation still becomes efficient. The result also gives a convergence rate. Together with Theorem 11 it identifies the limits of the mechanism with the Pareto allocations, so studying where repeated auctions end up comes down to studying Pareto efficiency.

The theorem is proved in the paper. No part of it, and none of its model, has a machine-checked proof. The formalization would check an argument that runs entirely in extended-real convex analysis, with utilities that may take the value $-\infty$, such as Cobb–Douglas utilities on the positive orthant. It would also settle points the printed proof leaves implicit. One is the radius at which Assumption 5 is applied. Another is that the endowments must lie in the utility domains, which some lemmas need explicitly.

Difficulty

The obvious route bounds each agent's gain per auction by $\delta_i$ times the agent's surplus and then telescopes. That route needs a single constant $\delta_i$ valid along the whole sequence, which in turn needs the iterates and the surpluses to be bounded in advance. Boundedness is the step a newcomer cannot get from compactness or from Lipschitz estimates. It comes from recession analysis of the superlevel sets of upper semicontinuous concave extended-real functions, through Rockafellar's characterization of bounded closed convex sets. Mathlib has none of this.

A second difficulty is attainment. Several steps use $u_i(x^0_i+\bar x_i-D_i(\bar x_i)g)\ge u_i(x^0_i)$, so the supremum defining $D_i$ must be attained. Attainment comes from upper semicontinuity, not from the definition. The cluster-point claims also need upper semicontinuity, in order to pass the monotone utilities to the limit.

Formalization scope

Utilities are functions (J → ℝ) → EReal, with I, J finite types and I nonempty. Concavity is convexity of the real hypograph, which is Rockafellar's definition. Mathlib's ConcaveOn does not apply because EReal is not a module. The indifference price and $CS$ are EReal suprema. A supergradient requires $D(\bar x)$ to be finite, which is Rockafellar's convention. Without that requirement a bid of $+\infty$ would satisfy (4) vacuously and the goal would be trivial.

$u_i^\infty(d)\ge0$ is encoded as the property that $\lambda\mapsto u_i(x+\lambda d)$ is nondecreasing for every $x\in\operatorname{dom}u_i$, which the paper quotes from Rockafellar's Theorem 8.6. $\mathbb B(r)$ is the closed sup-norm ball. The paper fixes no norm, and Assumptions 2 and 5 are unaffected by the choice.

The sequence in Theorem 16 is any sequence the mechanism generates: purchases and prices satisfying the market clearing conditions at the current allocation. Existence of solutions and prices is not part of the goal. The rate is stated with the real values of $u_i(x^t_i)$ and $u_i(x^0_i)$. Proving these values finite is part of the proof, and nothing in the statement assumes it.

The goal must not be trivialized. Bounded iterates, finite utilities along the sequence and $CS(x^t)\to0$ are conclusions, not hypotheses. The constants $\delta_i$ are universally quantified at a radius whose existence is claimed, not chosen existentially.

The following additions are disclosed on the items concerned. Lemma 2, the boundedness milestone and the first half of Theorem 11 assume $x_i\in\operatorname{dom}u_i$, without which they fail. Lemma 9's solution correspondence assumes a finite optimum value.

The development needs extended-real concave analysis: upper semicontinuous concave functions, their recession cones, and attainment of suprema. This layer is reusable beyond this mission. Contributions are welcome on any milestone. The recession-cone boundedness and Lemma 9 are good entry points.

Selected references

• T. Pennanen, Efficient allocations in double auction markets, Mathematics of Operations Research, 2022; arXiv:2001.02071v2. https://arxiv.org/abs/2001.02071v2
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• V. L. Smith, An experimental study of competitive market behavior, Journal of Political Economy 70 (1962). https://doi.org/10.1086/258609
• G. Debreu, Valuation equilibrium and Pareto optimum, Proceedings of the National Academy of Sciences 40 (1954). https://doi.org/10.1073/pnas.40.7.588

Motivation

A trader who quotes an exotic option written on several underlying assets (a basket call, a spread option, a best-of option) needs a price range that does not rest on a particular stochastic model. What is observed in the market is a finite set of liquid derivatives (vanilla calls and puts on each asset, and possibly some traded basket options), each with a bid price and an ask price. A model-free price bound for the exotic payoff is the range of prices consistent with these quotes and with the absence of arbitrage. Its upper end can be computed in two ways: as the cheapest static portfolio in the traded derivatives that dominates the payoff in every state of the world, or as the largest expected payoff over all probability measures that price the traded derivatives inside their bid–ask spreads.

The equality of these two numbers is a superhedging duality. For a single asset with exact (zero-spread) prices it goes back to the model-independent pricing literature of Hobson and others; Bouchard and Nutz (2015) proved a one-period duality and a fundamental theorem in a nondominated framework without spreads. Neufeld, Papapantoleon and Xiang (arXiv:2006.14288, Management Science 2023) extend the one-period result to a market where the derivatives are traded with bid–ask spreads and the payoffs are arbitrary Borel functions on a Polish state space, and then use the minimisation side to compute bounds exactly by cutting-plane algorithms.

Setting

Let $\Omega$ be a Polish space with its Borel $\sigma$-algebra, and let $\mathcal P(\Omega)$ be the set of all Borel probability measures on $\Omega$; there is no reference measure. Fix $m\in\mathbb N$ traded derivatives with Borel payoffs $g_1,\dots,g_m:\Omega\to\mathbb R$, collected in $g:\Omega\to\mathbb R^m$, with bid prices $\underline\pi_j$ and ask prices $\overline\pi_j$, $\underline\pi_j\le\overline\pi_j$.

A static position $y\in\mathbb R^m$ pays $\langle y,g\rangle(\omega)=\sum_j y_jg_j(\omega)$ and costs

$$\pi(y)=\sum_{j=1}^m y_j^+\,\overline\pi_j-y_j^-\,\underline\pi_j ,$$

since long positions are bought at the ask and short positions sold at the bid. The cost $\pi$ is sublinear, not linear.

No-arbitrage (Assumption 2.1): for every $y\in\mathbb R^m$, if $\langle y,g\rangle(\omega)-\pi(y)\ge0$ for every $\omega\in\Omega$, then $\langle y,g\rangle(\omega)-\pi(y)=0$ for every $\omega\in\Omega$.

For a Borel payoff $f:\Omega\to\mathbb R$, the superhedging price is

$$\phi(f)=\inf\{c+\pi(y):c\in\mathbb R,\ y\in\mathbb R^m,\ c+\langle y,g\rangle\ge f\ \text{on }\Omega\}\in[-\infty,\infty],$$

and the set of pricing measures is

$$\mathcal Q=\Big\{\mu\in\mathcal P(\Omega):\underline\pi_j\le\int_\Omega g_j\,d\mu\le\overline\pi_j,\ j=1,\dots,m\Big\}.$$

The proofs also use the box $\Delta=\prod_j[\underline\pi_j,\overline\pi_j]$ and the set $\mathcal C=\{\langle y,g\rangle-\pi(y):y\in\mathbb R^m\}-\mathcal L^0_+$ of payoffs super-replicable at zero cost, where $\mathcal L^0_+$ is the set of nonnegative Borel functions.

Formalization targets

Goal: the superhedging duality (Theorem 2.4(iii))

Under Assumption 2.1, for every Borel $f:\Omega\to\mathbb R$,

$$\phi(f)=\sup_{\mu\in\mathcal Q}\int_\Omega f\,d\mu .$$

The identity is stated in $[-\infty,\infty]$ and covers the case $\phi(f)=+\infty$ of payoffs that no static portfolio dominates.

Milestones

In the order of the proof in Appendix EC.4:

1. the support-function identity $\pi(y)=\max_{q\in\Delta}\langle y,q\rangle$;
2. Lemma EC.4.1: under Assumption 2.1, $\mathcal C$ is closed under pointwise convergence;
3. Theorem 2.4(i): $\phi(f)>-\infty$;
4. Theorem 2.4(ii): there is $y$ with $\phi(f)+\langle y,g\rangle-\pi(y)\ge f$, so the infimum is attained when $\phi(f)<\infty$;
5. Lemma EC.4.2: $\Delta\cap\operatorname{relint}(\Gamma_\nu)\ne\emptyset$ for every $\nu\in\mathcal P(\Omega)$, where $\Gamma_\nu$ is the set of moment vectors $\int g\,d\mu$ of measures $\mu\gg\nu$ integrating $|f|+\sum_j|g_j|$; in particular $\Delta\cap\operatorname{relint}(\Gamma)\ne\emptyset$;
6. the duality for $f$ bounded from above;
7. weak duality $\phi(f)\ge\sup_{\mu\in\mathcal Q}\int f\,d\mu$, which needs no no-arbitrage assumption.

Significance

The duality turns a maximisation over an infinite-dimensional set of probability measures into a minimisation over $\mathbb R\times\mathbb R^m$, a finite-dimensional problem with infinitely many constraints. This is what makes the exact computation of model-free bounds in the paper possible: for continuous piecewise affine payoffs, the minimisation side is solved by cutting-plane algorithms whose subproblems are linear and mixed-integer programs. Parts (i) and (ii) say that the upper bound is never $-\infty$ under no-arbitrage and that it is realised by an actual static hedge. Lemma EC.4.2 also yields the paper's fundamental theorem (Theorem 2.3), which characterises no-arbitrage by the existence of pricing measures dominating any given probability measure.

The result is proved in the paper; it has no machine-checked proof. A formalization would also give a checked version of the closedness lemma for cones of super-replicable payoffs, which is the step most often adapted from Bouchard–Nutz in later work on one-period robust pricing, and a reusable statement of the extended-valued duality with an explicit convention for non-integrable payoffs.

Difficulty

The obvious route is finite-dimensional linear programming duality. It fails because the constraint $c+\langle y,g\rangle\ge f$ is indexed by every $\omega$ in an uncountable Polish space and the dual variables are measures; the paper uses a semi-infinite Fenchel duality theorem (Borwein–Lewis), whose constraint qualification is exactly the relative-interior condition of Lemma EC.4.2. Proving that condition requires constructing, from any $\nu$, an equivalent-type measure with finite moments, and separating a polyhedron from a convex set properly. A second difficulty is the passage to unbounded $f$: it rests on the closedness of $\mathcal C$ under pointwise limits (Lemma EC.4.1), proved by an induction on the number of coordinates along which the hedge positions $y_n$ diverge; compactness of the unit sphere alone does not suffice because the bid–ask cost $\pi$ is not linear.

Formalization scope

The Lean development lives in the namespace ModelFreeBounds.Duality, with one definition file Market. Conventions:

• $\Omega$ carries [TopologicalSpace Ω] [PolishSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]. Indices are Fin m and vectors in $\mathbb R^m$ are functions Fin m → ℝ; $\operatorname{relint}$ is intrinsicInterior ℝ.
• The standing assumptions (Borel $g_j$, $\underline\pi_j\le\overline\pi_j$) form the structure Market.Standing.
• Assumption 2.1, the superhedging constraint, $\mathcal L^0_+$ and the convergence in Lemma EC.4.1 are all pointwise on every $\omega$, not almost sure.
• $\phi(f)$ is an infimum in EReal with $\inf\emptyset=+\infty$; the right-hand side of (2.3) is a supremum in EReal over the subset $\mathcal Q$ of measures, equal to $-\infty$ when $\mathcal Q=\emptyset$.
• $\int_\Omega f\,d\mu$ for a Borel $f$ that need not be integrable is $\int f^+d\mu-\int f^-d\mu$ with $\infty-\infty=-\infty$. The paper fixes no convention; the duality holds under either choice.
• $\mathcal Q$ includes $\mu$-integrability of every $g_j$, which the real bounds on $\int g_j\,d\mu$ presuppose. Integrability of $|f|+\sum_j|g_j|$ in $\Gamma_\nu$ and $\Gamma$ is written as integrability of $f$ and of each $g_j$.
• $\Omega$ is assumed nonempty only in Theorem 2.4(i), Theorem 2.4(ii) and the "in particular" part of Lemma EC.4.2, which are false for $\Omega=\emptyset$ (there $\phi(f)=-\infty$ and $\Gamma=\emptyset$); the goal holds for $\Omega=\emptyset$ with both sides $-\infty$.

The following formalizations would trivialise the statement and are excluded: a real-valued $\phi$ (where an unbounded infimum becomes $0$), the Bochner integral for $f$ (which is $0$ on non-integrable $f$), $\mathcal Q$ without the integrability of the $g_j$, no-arbitrage stated almost surely under a fixed measure, $\mathcal Q$ over sub-probability or arbitrary measures, and a finite $\Omega$.

A complete development needs: semi-infinite or infinite-dimensional Fenchel duality for linear maps into $\mathbb R^{m+1}$ (Mathlib has finite-dimensional separation theorems but not this duality), proper separation of a polyhedron from a convex set in $\mathbb R^m$, and the measure-theoretic construction of measures with prescribed null sets and finite moments on a Polish space. The closedness lemma and the support-function identity are independent of the duality and are natural first contributions. Contributions of any milestone, of alternative proofs of the goal, or of reusable infrastructure (extended-valued integrals, relative-interior constraint qualifications) are welcome.

Selected references

• A. Neufeld, A. Papapantoleon, Q. Xiang, Model-free bounds for multi-asset options using option-implied information and their exact computation, Management Science 69(4), 2023. https://doi.org/10.1287/mnsc.2022.4456 ; arXiv:2006.14288v3. https://arxiv.org/abs/2006.14288
• B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Annals of Applied Probability 25(2), 2015. https://doi.org/10.1214/14-AAP1011
• J. M. Borwein, A. S. Lewis, Partially finite convex programming, Part I: Quasi relative interiors and duality theory, Mathematical Programming 57, 1992. https://doi.org/10.1007/BF01581072
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

US equities trade on many exchanges at once. Each exchange keeps its own limit order book, and at the national best bid the same price is offered in several queues that differ in the rebate the exchange pays a liquidity provider and in how long a resting order waits to be filled. An investor who posts a limit order chooses an exchange, or decides to cross the spread with a market order instead, by trading rebate against expected delay. Maglaras, Moallemi and Zheng (Operations Research 69(4), 2021) model this routing game as a queueing system with heterogeneous, delay-sensitive investors, and show that its equilibria are governed by a single scalar, the workload. Their empirical section, on trade-and-quote data for 30 stocks in September 2011, finds the queue lengths across exchanges in agreement with the predicted collapse.

The phenomenon is a static form of state space collapse, a notion that comes from heavy-traffic queueing theory, where a multi-dimensional queue-length process is shown to concentrate near a low-dimensional set (Bramson, 1998; the paper's §1 reviews this literature). Here the collapse is exact and holds at equilibrium, not only in a diffusion limit.

Setting

There are $N$ exchanges. Dedicated limit orders arrive to exchange $i$ at rate $\lambda_i \ge 0$; optimizing limit-order investors arrive at total rate $\Lambda > 0$; market orders arrive at aggregate rate $\mu > 0$. Routing option $i \in \{1,\dots,N\}$ means posting at exchange $i$, and option $0$ means trading with a market order. Each option has an effective rebate $\tilde r_i \in \mathbb R$.

Given queue lengths $Q \in \mathbb R^N_+$, the workload is $W = \beta^\top Q = \sum_{i=1}^N \beta_i Q_i$ with attraction coefficients $\beta_i > 0$. Market orders are split across exchanges in proportion to attraction:

$$\mu_i(Q) = \mu\,\frac{\beta_i Q_i}{\beta^\top Q},$$

and the expected delay at exchange $i$ is $\mathrm{ED}_i = Q_i/\mu_i(Q)$, with $\mathrm{ED}_0 = 0$.

An investor of type $\gamma \ge 0$, drawn from a distribution $F$, values option $i$ at $\gamma\tilde r_i - \mathrm{ED}_i$. A routing decision $\pi \in \mathcal P$ assigns to every type a probability vector $\pi(\gamma) = (\pi_0(\gamma),\dots,\pi_N(\gamma))$, measurably in $\gamma$. An equilibrium (Definition 1) is a pair $(\pi^*, Q^*)$ such that (i) almost every type's $\pi^*(\gamma)$ maximizes $\pi_0\gamma\tilde r_0 + \sum_i \pi_i(\gamma\tilde r_i - \mathrm{ED}_i(Q^*))$ over the simplex, and (ii) each exchange's flow balances:

$$\lambda_i + \Lambda\int_0^\infty \pi^*_i(\gamma)\,dF(\gamma) = \mu_i(Q^*).$$

Formalization targets

Goal: Theorem 1 (State Space Collapse)

For $W^* > 0$, if $\pi^*$ maximizes

$$\int_0^\infty \Big\{\pi_0(\gamma)\gamma\tilde r_0 + \sum_{i=1}^N \pi_i(\gamma)\Big(\gamma\tilde r_i - \frac{W^*}{\mu\beta_i}\Big)\Big\}\,dF(\gamma) \qquad (13)$$

over $\mathcal P$ and $\sum_{i=1}^N\big(\lambda_i + \Lambda\int_0^\infty\pi^*_i\,dF\big) = \mu$ (14), then $(\pi^*, Q^*)$ is an equilibrium for the lifting map

$$Q^*_i = \Big(\lambda_i + \Lambda\int_0^\infty \pi^*_i(\gamma)\,dF(\gamma)\Big)\frac{W^*}{\mu\beta_i}. \qquad (15)$$

Conversely, every equilibrium $(\pi^*, Q^*)$ satisfies (13)–(14) with $W^* = \beta^\top Q^*$.

Milestones

1. (12): at any state with positive workload, $\mathrm{ED}_i = W/(\mu\beta_i)$ for every $i$.
2. (16): the lifted state has workload $W^*$, hence delays $W^*/(\mu\beta_i)$.
3. Separability of (13) in $\gamma$: for any fixed delays, $\pi$ maximizes the integrated payoff over $\mathcal P$ if and only if $\pi(\gamma)$ is a best response for $F$-almost every $\gamma$.
4. The lifted state satisfies the flow balance (11).
5. In equilibrium $Q^* = \text{lift}(\pi^*, \beta^\top Q^*)$: the workload determines the queue lengths.

Significance

The theorem replaces an $N$-dimensional fixed-point problem, coupled through the attraction model, by a one-dimensional search over the workload $W^*$, with the queue lengths recovered by (15). The rest of the paper builds on it: the threshold characterization of equilibria (Theorem 2), uniqueness (Theorem 3), and the empirical prediction that queue lengths across exchanges are pinned down by one number. The lifting map is a Little's-law identity: each queue equals its arrival rate times the common workload-implied delay.

The result is proved in the paper, in a short argument; it has not been formalized. Formalizing it adds (a) a corrected statement, since the printed one is false in two corner cases (below), (b) a reusable Lean model of a routing equilibrium with a continuum of investor types, and (c) the measure-theoretic separability lemma, which the paper takes for granted and which carries the real content of the proof.

Difficulty

The algebra of (12), (15) and (16) is routine. The difficulty sits in the sentence "the optimization problem in (i) is separable with respect to $\gamma$". Passing from optimality of an integral over the set $\mathcal P$ of measurable routing decisions to pointwise optimality requires constructing a measurable pointwise best response, to compare against on any set of types where $\pi^*$ is suboptimal, and controlling integrability of the payoff, which grows linearly in $\gamma$. The naive reading, that integral optimality forces rationality for every type, is false: changing $\pi^*$ at a single type does not change the integral. Conversely, passing from almost-everywhere pointwise optimality back to optimality of the integral needs the payoff of every competing routing decision to be integrable.

Formalization scope

Everything lives in the namespace FragLOB.Collapse. Parameters are a structure Market N with a predicate Market.Standing ($\lambda_i \ge 0$, $\Lambda, \mu, \beta_i > 0$); rebates are unconstrained. Exchanges are Fin N, routing options Fin (N+1) with 0 the market order. The type distribution is a probability measure F on ℝ with F (Set.Iio 0) = 0, so $\int_0^\infty\cdots dF$ is written ∫ γ, … ∂F, and with finite mean.

Three changes to the printed Theorem 1 are committed to, each needed for truth:

• Individual rationality holds $F$-almost everywhere. As printed (for all $\gamma \ge 0$), the forward direction is false: with $N = 1$, $\lambda_1 = 0$, $\Lambda = 2$, $\mu = \beta_1 = 1$, $\tilde r = (-1,1)$ and $F$ exponential, the policy "post iff $\gamma > \ln 2$" with $W^* = 2\ln 2$ satisfies (13)–(14); redefining it to "market order" at $\gamma = 5$ keeps (13)–(14) but violates (10) there. The paper reads Theorem 2 the same way.
• $W^* > 0$ in the forward direction and $\beta^\top Q^* > 0$ in an equilibrium. With $\Lambda = \mu = 1$ in the same example, $W^* = 0$ satisfies (13)–(14) but (15) gives $Q^* = 0$, where (4) is $0/0$.
• $F$ has finite mean, so that the objective of (13) is a genuine integral for every routing decision.

The paper's differentiable CDF with continuous density is not used by Theorem 1 and is dropped (a generalization). At an empty exchange, where (1) reads $0/0$, the delay is defined as $W/(\mu\beta_i)$, the value (12) gives; elsewhere it is $Q_i/\mu_i(Q)$ as in (1).

Trivializing encodings are ruled out: the delay is not defined as $W/(\mu\beta_i)$ outright, routing decisions must be measurable and are compared only against measurable alternatives, the equilibrium is phrased through queue lengths and $\mu_i(Q)$ rather than the workload, and all integrals are against a probability measure with integrable payoffs.

Solvers will need: measurable selection of a best response from finitely many affine functions of $\gamma$, integrability bounds of the form $C(1+|\gamma|)$, and Finset sum algebra. The separability lemma is reusable for any finite-action game with a continuum of types. Proofs of any milestone are welcome; the excluded results (Lemma 1, Theorems 2–3, the fluid model) are natural follow-up missions.

Selected references

• C. Maglaras, C. C. Moallemi, H. Zheng, Queueing Dynamics and State Space Collapse in Fragmented Limit Order Book Markets, Operations Research 69(4):1324–1348, 2021. https://doi.org/10.1287/opre.2020.1989
• M. Bramson, State space collapse with applications to heavy-traffic limits for multiclass queueing networks, Queueing Systems 30:89–148, 1998. https://doi.org/10.1023/A:1019160803783

Motivation

Markowitz's mean-variance problem trades off the expected terminal wealth of a portfolio against its risk. Over several periods the scalarized form of this problem is time inconsistent: a strategy that is optimal today for a fixed risk-aversion parameter is generally no longer optimal tomorrow for the same parameter, so the investor would deviate from her own plan (Björk & Murgoci 2014; Björk, Murgoci & Zhou 2014). The literature has responded by redefining optimality (equilibrium strategies) or by searching for a time- and state-dependent risk aversion that restores consistency (Karnam, Ma & Zhang, Annals of Applied Probability 27, 2017). Dynamic convex risk measures and their time consistency are developed in Detlefsen & Scandolo 2005 and Riedel 2004.

Kováčová and Rudloff (arXiv:1806.10981, Operations Research 2021) take a different route. They keep both objectives, measure risk by a time consistent dynamic convex risk measure, and treat the dynamic mean-risk problem as a family of vector optimization problems. They show that this family is time consistent with respect to weak minimizers and that its value functions, the upper images, satisfy a set-valued Bellman principle. This mission formalizes that Bellman principle.

Setting

Fix a horizon $T$ and a finite probability space $(\Omega,\mathcal F,\mathbb P)$ with a filtration $(\mathcal F_t)_{t=0}^T$, $\mathcal F_0$ trivial, $\mathcal F_T=\mathcal F$, and $\mathbb P(A)>0$ for every nonempty event $A$. $L_t(D)$ denotes the $\mathcal F_t$-measurable random vectors with values in $D$; orders between random vectors are pointwise and componentwise.

A market has $d$ assets with adapted discounted prices $S_s\in L_s(\mathbb R^d)$. An investor holds positions $\psi_s\in L_s(\mathbb R^d)$ on $[s,s+1)$, subject to closed, conditionally convex constraint sets $\Phi_s\subseteq L_s(\mathbb R^d)$. With wealth $v_t\in L_t$ at time $t$, the feasible portfolios are

$$\Psi_t(v_t)=\{(\psi_s)_{s=t}^{T-1}\mid S_t^\top\psi_t=v_t,\ \psi_t\in\Phi_t,\ S_s^\top\psi_{s-1}=S_s^\top\psi_s,\ \psi_s\in\Phi_s,\ s=t+1,\dots,T-1\},$$

that is, self-financing strategies with initial value $v_t$ that respect the constraints. The terminal wealth is $v_T=S_T^\top\psi_{T-1}$ and $V_T(\psi)=(v_T,v_T)$.

Risk is measured by a dynamic convex risk measure $(\rho_t)_{t=0}^T$: each $\rho_t:L_T\to L_t$ is normalized, conditionally translation invariant, monotone (decreasing) and conditionally convex. It is time consistent: $\rho_{t+1}(X)=\rho_{t+1}(Y)$ implies $\rho_t(X)=\rho_t(Y)$. The mean-risk function is

$$\Gamma_t(X)=\big(-\mathbb E_t(X_1),\ \rho_t(X_2)\big),\qquad X\in L_T(\mathbb R^2),$$

and the mean-risk problem $D_t(v_t)$ minimizes $\Gamma_t(V_T(\psi))$ over $\psi\in\Psi_t(v_t)$ with respect to the cone $L_t(\mathbb R^2_+)$. Its upper image is

$$\mathcal P_t(v_t)=\operatorname{cl}\big(\Gamma_t(\Psi_t(v_t))+L_t(\mathbb R^2_+)\big),\qquad t<T,$$

and at the terminal time $\mathcal P_T(v_T)=\{(-v_T,-v_T)\}+L_T(\mathbb R^2_+)$ (5.2).

Formalization targets

Goal: Theorem 5.1 (set-valued Bellman equation)

For every $t=0,\dots,T-1$ and every $\mathcal F_t$-measurable $v_t$,

$$\mathcal P_t(v_t)=\operatorname{cl}\left\{\Gamma_t(-x)\ \middle|\ S_t^\top\psi_t=v_t,\ \psi_t\in\Phi_t,\ x\in\mathcal P_{t+1}\big(S_{t+1}^\top\psi_t\big)\right\}.$$

The right side has a closure and no ordering cone.

Milestones

1. Lemma 2.1 (second and third bullets): time consistency is equivalent to recursiveness $\rho_t(X)=\rho_t(-\rho_{t+1}(X))$; a convex risk measure on a finite space is continuous.
2. Lemma 3.1: $\psi\in\Psi_t(v_t)$ iff $S_t^\top\psi_t=v_t$, $\psi_t\in\Phi_t$ and $(\psi_s)_{s\ge t+1}\in\Psi_{t+1}(S_{t+1}^\top\psi_t)$.
3. Lemma B.1: $\Gamma_t$ is conditionally translation invariant, monotone, conditionally convex, recursive ($\Gamma_t(X)=\Gamma_t(-\Gamma_{t+1}(X))$), local and continuous; upper images are monotone with respect to their cone.
4. Lemma B.2: $\Gamma_t(\Psi_t(v_t))$ equals the image of the auxiliary problem $\bar D_t(v_t)$, in which $x$ ranges over $\Gamma_{t+1}(\Psi_{t+1}(S_{t+1}^\top\psi_t))$.
5. Lemma 5.2: the upper image $\tilde{\mathcal P}_t(v_t)$ of the one-time-step problem $\tilde D_t(v_t)$, in which $x$ ranges over $\mathcal P_{t+1}(S_{t+1}^\top\psi_t)$, equals $\mathcal P_t(v_t)$.

Significance

The upper image is the infimum of $D_t(v_t)$ in the complete lattice of closed upper sets, so it is the natural value function of a vector optimization problem. Theorem 5.1 expresses the value function at time $t$ through the value functions at time $t+1$ by a one-period problem, exactly as a scalar Bellman equation does. Computationally this is what makes the problem tractable: one solves a convex one-period vector optimization problem per node, backwards in time, and recovers the whole efficient frontier at every node and an efficient strategy forward along the realized path (Sections 6 and 7 of the paper do this for 2,500 periods). Conceptually, it shows that the mean-risk problem is time consistent in the set-valued sense without computing the moving scalarization in advance.

The paper proves Theorem 5.1; no machine-checked version exists. Formalizing it produces a Lean development of dynamic convex risk measures on finite filtrations, of conditional vector optimization in $L_t(\mathbb R^2)$, and of upper images, none of which is currently on the platform beyond the static conditional convex risk measure reused here.

Difficulty

The equality has two halves of different character. Replacing the image $\Gamma_{t+1}(\Psi_{t+1})$ by the upper image $\mathcal P_{t+1}$ enlarges the feasible set of the one-period problem, and the new points must be shown to be limits of points already attained: this needs monotonicity of $\Gamma_t$ together with its continuity, which holds only because $\Omega$ is finite. Removing the cone from the right-hand side needs translation invariance of $\Gamma_t$ with an $\mathcal F_t$-measurable shift and the monotonicity of $\mathcal P_{t+1}$ with respect to the larger cone $L_{t+1}(\mathbb R^2_+)$. Both closures matter: without them the identity fails in general, since the image of a closed set under $\Gamma_t$ need not be closed. The natural first idea, to define $\mathcal P_t$ recursively, proves nothing: the content of the theorem is that the upper image built from whole multi-period strategies agrees with the recursion.

Formalization scope

• $\Omega$ is a Fintype with an ambient σ-algebra $\mathcal F$; the filtration is a Mathlib Filtration ℕ with $\mathcal F_T=\mathcal F$ and $\mathcal F_0=\bot$; $\mathbb P$ is a probability measure with $\mathbb P(A)>0$ for every nonempty measurable $A$.
• Each $\rho_t$, $t\le T$, satisfies the published CondConvexRisk.Representation.IsCondConvexRiskMeasure with respect to $\mathcal F_t$ (axioms a.s. on $L^\infty$); time consistency is stated pointwise for measurable arguments. On a finite space with positive probabilities, a.s. equality of measurable functions is equality, so all of the mission's own statements are pointwise.
• Random vectors in $\mathbb R^2$ are functions $\Omega\to\mathbb R\times\mathbb R$; the cone $L_t(\mathbb R^2_+)$ is the set of nonnegative $\mathcal F_t$-measurable ones; closures are in the product topology. $\mathbb E_t$ is Mathlib's condExp.
• Strategies are sequences indexed by $\mathbb N$; only the indices $t,\dots,T-1$ are constrained or read.
• Assumption 2.2 item 3 ($\Psi_0(v_0)\neq\emptyset$) is not assumed by any statement; Theorem 5.1 holds for empty feasible sets as well.
• $\mathcal P_t$ for $t<T$ is the closure of the image of whole strategies plus the cone; only $\mathcal P_T$ is given by (5.2). A recursive definition of $\mathcal P_t$, or a cone on the right of (5.1), would make the goal trivial or turn it into Lemma 5.2, and is ruled out.
• Not formalized here: Theorem 3.2 (time consistency w.r.t. weak minimizers), the scalarization results of §4, the coherent case of §6, and the node-wise algorithms of Appendix A.

A complete development needs: conditional expectation on finite filtrations (tower property, pull-out of $\mathcal F_t$-measurable factors), continuity of convex functions on finite-dimensional spaces, and elementary closure arguments in $\Omega\to\mathbb R\times\mathbb R$. The results on dynamic risk measures (Lemma 2.1) and on $\Gamma_t$ (Lemma B.1) are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• G. Kováčová, B. Rudloff, Time consistency of the mean-risk problem, Operations Research, 2021. Preprint arXiv:1806.10981v2. https://arxiv.org/abs/1806.10981
• A. H. Hamel, F. Heyde, A. Löhne, B. Rudloff, C. Schrage, Set optimization — a rather short introduction, in Set Optimization and Applications, Springer, 2015. https://doi.org/10.1007/978-3-662-48670-2_3
• A. Löhne, Vector Optimization with Infimum and Supremum, Springer, 2011. https://doi.org/10.1007/978-3-642-18351-5
• K. Detlefsen, G. Scandolo, Conditional and dynamic convex risk measures, Finance and Stochastics 9(4), 2005. https://doi.org/10.1007/s00780-005-0159-6
• F. Riedel, Dynamic coherent risk measures, Stochastic Processes and their Applications 112(2), 2004. https://doi.org/10.1016/j.spa.2004.03.004
• T. Björk, A. Murgoci, A theory of Markovian time-inconsistent stochastic control in discrete time, Finance and Stochastics 18(3), 2014. https://doi.org/10.1007/s00780-013-0227-1
• T. Björk, A. Murgoci, X. Y. Zhou, Mean-variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• C. Karnam, J. Ma, J. Zhang, Dynamic approaches for some time-inconsistent optimization problems, Annals of Applied Probability 27, 3435–3477, 2017.

Motivation

Repeated games model long-run relationships: the same players meet stage after stage, observe what was played, and can condition today's behavior on the past. The folk theorem describes what such relationships can sustain. When players are patient, every payoff vector that is feasible and gives each player at least what the others can force on them is the payoff of an equilibrium, and the equilibrium can be chosen subgame perfect, so that every threatened punishment is itself credible. Economics, operations research and computer science use the result to explain cooperation and collusion and to reason about long-term contracts and repeated auctions.

The classical statement assumes stationary discounting: a payoff at stage $t$ is worth $\delta^{t-1}$ of a payoff today, and "patient" means $\delta\to1$. Experimental and behavioral evidence points instead to discount rates that change over time (hyperbolic and quasi-hyperbolic discounting), and planning problems with a finite or decaying horizon have weights that are not geometric at all. X. Li (later with D. Kim) asks whether the perfect folk theorem survives when the weight of stage $t$ is an arbitrary decreasing sequence, and gives a patience condition under which it does.

Timeline.

• 1986. Fudenberg and Maskin prove the perfect folk theorem for discounted repeated games with at least three players under a full-dimensionality condition on the feasible and individually rational set (Econometrica 54).
• 1986. Sorin shows that any feasible payoff can be written as a discounted sum of pure-action payoffs once $\delta$ is large, which removes the need for public randomization on the equilibrium path (Math. Oper. Res. 11).
• 1991. Fudenberg and Maskin use such decompositions to dispense with public randomization in the perfect folk theorem.
• 2019–2021. Li (SSRN 3407197) and Kim and Li (Math. Oper. Res., 2021) extend the asymptotic perfect folk theorem to time-dependent discounting.

The repeated game with time-dependent discounting

A finite set $I$ of players plays a stage game repeatedly. Player $i$ has a finite action set $A^i$, $A=\prod_iA^i$, and $g=(g^i)_{i\in I}:A\to\mathbb R^I$ gives the stage payoffs. At each stage $t\ge1$ every player observes the past actions $(a_1,\dots,a_{t-1})$ and chooses an action, possibly at random. A behavior strategy $\sigma^i$ assigns a mixed action to every finite history, and a profile $\sigma$ determines a distribution over infinite plays.

An evaluation is a sequence $\theta=(\theta_t)_{t\ge1}$ in $[0,1]$ that is decreasing and sums to one; the payoff of $\sigma$ is

$$\gamma_\theta(\sigma)=\mathbb E_\sigma\Big[\sum_{t\ge1}\theta_t\,g(a_t)\Big].$$

Stationary discounting is $\theta_t=(1-\delta)\delta^{t-1}$. After a history of $T-1$ stages the remaining game is evaluated by the continuation evaluation $\theta_t[T]=\theta_{T-1+t}/\sum_{s\ge T}\theta_s$; unlike the stationary case, $\theta[T]$ depends on $T$. A profile is a subgame perfect equilibrium of $\Gamma_\theta$ if, after every history $h_T$, the induced profile is a Nash equilibrium of the subgame $\Gamma_{\theta[T]}(h_T)$. $E_\theta\subseteq\mathbb R^I$ is the set of subgame perfect equilibrium payoffs.

The minmax level of player $i$ is

$$v^i=\min_{s\in\prod_{j\ne i}\Delta(A^j)}\ \max_{a^i\in A^i}\ \sum_{a^{-i}}s(a^{-i})\,g^i(a^i,a^{-i}),$$

the lowest payoff the others can hold $i$ to by mixing independently. $S=\operatorname{co}\{g(a):a\in A\}$ is the set of feasible payoffs and $\mathcal F=\{x\in S:x^i\ge v^i\ \forall i\}$ the set of feasible and individually rational payoffs.

A sequence of evaluations $(\theta^k)_{k\ge1}$ is patient if $\theta^k_t/\theta^k_{t+1}\to1$ as $k\to\infty$, uniformly in $t$.

Formalization targets

Goal: Theorem 3.1 (Asymptotic Perfect Folk Theorem)

If $\operatorname{int}\mathcal F\ne\emptyset$ and $(\theta^k)$ is patient, then

$$E_{\theta^k}\xrightarrow[k\to\infty]{}\mathcal F\quad\text{in the Hausdorff distance.}$$

The goal fixes no rate and no constants; it asserts only the limit.

Milestones

• Lemma 4.1: patience is equivalent to $\sum_{t=T}^{T+T_1}\theta^k_t\big/\sum_{t=T}^{T+T_2}\theta^k_t\to(T_1+1)/(T_2+1)$ uniformly in $T$.
• Lemma 4.2: for patient $(\theta^k)$, $\theta^k_1[T]\to0$ and $\theta^k_t[T]/\theta^k_{t+1}[T]\to1$, uniformly in $T$ and $t$.
• Claim 7.1 and Lemma 4.4: a perturbed decomposition $x=\sum_m\theta^k_m x'_{\varphi(m)}$ with each $x'_{\varphi(m)}$ near a vertex.
• Proposition 4.3, and its form for the continuation evaluations $\theta^k[T]$: every $x\in\mathcal F$ is the $\theta^k$-payoff of a pure path along which all continuation payoffs stay within $\eta$ of $x$.
• (5.1), Lemma 5.1, Lemma 5.2: the punishment length and the bounds that make punishments and rewards consistent.
• The one-shot deviation principle under general discounting (§5.1 Part C, footnote 12).
• Interior payoffs are equilibrium payoffs: every $x\in\operatorname{int}\mathcal F$ lies in $E_{\theta^k}$ for all large $k$.

Significance

The result. The theorem says that the set of credible long-run outcomes is the same under any patient time-dependent discounting as under stationary discounting with $\delta\to1$. Quasi-hyperbolic $(\beta,\delta)$ preferences with $\beta,\delta\to1$ and discount factors that vary by stage are special cases. Patience is stated through ratios of consecutive weights. The paper notes that this condition does not cover $T$-stage averages with $T\to\infty$, where the folk theorem is known to need extra assumptions. The equilibria use pure paths, with no public randomization.

Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission builds a reusable Lean model of discounted repeated games with perfect monitoring: behavior strategies, the induced distribution over finite histories, continuation games, subgame perfection, minmax levels and the feasible and individually rational set. It then states the theorem and the lemmas of its proof. The one-shot deviation principle under general discounting and the pure-path decomposition (Proposition 4.3) are standard tools that the literature usually cites without proof, and both are useful well beyond this paper.

Difficulty

The stationary proof relies on the fact that every subgame looks like the original game: $\theta[T]=\theta$. Under time-dependent discounting the continuation evaluation changes with the starting stage. A punishment phase of fixed length therefore carries a different weight depending on when it starts, and the number of stages needed to deter a deviation depends on the stage. Two consequences make the obvious adaptation fail. First, a deviation during a punishment starts a new punishment whose length differs from the remaining length of the old one, so the incentive check splits into cases (Lemma 5.2). Second, the pure paths that deliver the reward payoffs have to work for every continuation evaluation at once, which needs the uniformity statements of Lemma 4.2 and the perturbed decomposition of Lemma 4.4. Replacing each continuation evaluation by a geometric one does not work, because nothing forces the weights of a patient sequence to be close to geometric.

Formalization scope

All declarations live in the namespace TimeDepFolk.Asymptotic. Stages are 0-based: Lean stage $s$ is the paper's $t=s+1$, a history of $n$ played stages is Fin n → (∀ i, A i), and cont θ n is the paper's $\theta[n+1]$, which is $0$ when the tail sum vanishes. Mixed actions are lotteries (AGT.IsLottery) and the minmax level uses AGT.expectedPayoff from the published definition agt_games, with independent mixing by the others. Action sets are finite, so expectations are finite sums over histories and the payoff is the series $\sum_s\theta_s\,\mathbb E_\sigma[g(a_s)]$; no measure theory is needed. Payoff vectors live in I → ℝ with the sup norm. Subgame perfection quantifies over all histories, the empty history included, and over all behavior-strategy deviations; the one-shot reduction is a milestone to prove, not part of the definition. The player set and every action set are finite and nonempty. "$\operatorname{int}\mathcal F$ nonempty and fully dimensional" is (interior (F g)).Nonempty.

The goal uses the extended-valued Hausdorff distance Metric.hausdorffEDist. The real-valued Metric.hausdorffDist is $0$ when one set is empty, so a goal stated with it would hold vacuously for every $k$ at which no equilibrium is known; the extended version makes nonemptiness of $E_{\theta^k}$ part of the claim. Stating the goal for a single payoff, with Nash instead of subgame perfect equilibrium, or with Theorem 3.2's discount factors in place of evaluations would each prove a different and weaker theorem.

A complete development needs the probability of finite histories under behavior strategies, the decomposition of the payoff into the first stage and the continuation, the one-shot deviation principle, Carathéodory's theorem (in Mathlib), and the barycentric sensitivity of Claim 7.1. The repeated-game layer and the one-shot deviation principle can be reused for any discounted repeated game with perfect monitoring. Contributions to any milestone, and alternative proofs of the decomposition results, are welcome.

Selected references

• X. Li, The folk theorem for repeated games with time-dependent discounting, SSRN Working Paper 3407197, version of August 16, 2019. https://ssrn.com/abstract=3407197
• D. Kim and X. Li, The folk theorem for repeated games with time-dependent discounting, Mathematics of Operations Research, 2021. https://doi.org/10.1287/moor.2021.1183
• D. Fudenberg and E. Maskin, The folk theorem in repeated games with discounting or with incomplete information, Econometrica 54(3), 1986. https://doi.org/10.2307/1911307
• S. Sorin, On repeated games with complete information, Mathematics of Operations Research 11(1), 1986. https://doi.org/10.1287/moor.11.1.147
• G. J. Mailath and L. Samuelson, Repeated Games and Reputations: Long-Run Relationships, Oxford University Press, 2006. https://doi.org/10.1093/acprof:oso/9780195300796.001.0001

Motivation

Retailers that sell many products set prices against one another, and the demand for each product depends on the prices of all of them. Affine demand models, $q(p)=a-Rp$, are the standard starting point for this kind of multi-product price competition in operations management and industrial organization. Two questions follow once an equilibrium is known to exist. Can the firms reach it, and does it matter where they start? A Nash equilibrium that the firms cannot find by adjusting their prices tells little about what prices will actually be observed.

Federgruen and Hu (Operations Research 69(1), 2021; submitted manuscript at SSRN 3010503) answer this for a general multi-firm, multi-product model with an arbitrary number of firms and arbitrary product assortments. The game has features that defeat the usual tools. Once the affine demands are extended so that no demand turns negative, the game is in general not supermodular. Example 1 of the paper, after McGuire and Staelin (1983/2008), is a duopoly that is not supermodular and has a continuum of equilibria. Earlier work (Federgruen and Hu, Operations Research 63(3), 2015) characterized the equilibria. One of them, the special equilibrium $(p^*|w)$, has a closed form. The 2021 paper shows that this equilibrium is reached from any starting price vector when every firm repeatedly plays a robust best response.

Setting

A finite set $\mathcal N$ of products is partitioned among firms. Firm $i$ sells the products $\mathcal N(i)$. The foundational demands are

$$q(p)=a-Rp,\qquad a\ge 0,$$

where $R$ is an $\mathcal N\times\mathcal N$ price-sensitivity matrix subject to three assumptions:

1. (P) $R$ is positive definite in the quadratic-form sense: $x^\top Rx>0$ for all $x\ne 0$. $R$ need not be symmetric.
2. (Z) $R$ is a Z-matrix: $R_{lm}\le 0$ for $l\ne m$, so the products are substitutes.
3. (IS) $R$ is symmetric within each firm: $R_{lm}=R_{ml}$ when $l,m\in\mathcal N(i)$.

Each firm has a cost vector, $w\in\mathbb R^{\mathcal N}_{++}$. Let $T(R)$ be the block-diagonal matrix of the transposed firm blocks $R^\top_{\mathcal N(i),\mathcal N(i)}$, and let $\Psi(R)=T(R)[R+T(R)]^{-1}$ and $Q(w')=\Psi(R)a-\Psi(R)Rw'$. The cost projection $w'=\Theta(w)$ solves the linear complementarity problem

$$w'\le w,\qquad Q(w')^\top(w-w')=0,\qquad Q(w')\ge 0,$$

and the special equilibrium is

$$(p^*|w)=w'+[R+T(R)]^{-1}(a-Rw').$$

Given the other firms' prices $p_{-\mathcal N(i)}$, firm $i$ sees the residual intercept $\alpha=a_{\mathcal N(i)}-R_{\mathcal N(i),-\mathcal N(i)}p_{-\mathcal N(i)}$. Its robust best response maximizes

$$(x-w_{\mathcal N(i)})^\top(\alpha-R_{\mathcal N(i),\mathcal N(i)}x)\quad\text{over } x\ge 0,\ \alpha-R_{\mathcal N(i),\mathcal N(i)}x\ge 0.$$

Prices are restricted to keep the firm's own affine demands nonnegative, so the firm needs only its own demand and cost data. Collecting all firms gives the map $RB$, and $RB^{(n)}$ is its $n$-fold iterate. Finally, $\Lambda(R)=I-[T(R)]^{-1}R$.

Formalization targets

Goal: Theorem 3 (global robust stability)

There exist a norm $\|\cdot\|$ on $\mathbb R^{\mathcal N}$ and a constant $0<\gamma<1$ such that

$$\|RB(\hat p)-RB(\tilde p)\|\le\gamma\|\hat p-\tilde p\|\quad(\hat p,\tilde p\ge 0),$$ $$\|RB^{(n)}(p)-(p^*|w)\|\le\gamma^n\|p-(p^*|w)\|,\qquad \lim_{n\to\infty}RB^{(n)}(p)=(p^*|w)\quad(p\ge 0).$$

Neither the norm nor $\gamma$ is fixed, because the paper asserts only that they exist.

Milestones

The milestones follow the paper's own proof:

• Lemma 1: $RB$ is well defined.
• The proof of Theorem 2: the projection LCP has a unique, nonnegative solution.
• Theorem 2: $(p^*|w)$ is a fixed point of $RB$.
• Lemma B.1(a), (c), (e), (f), (g): the M-matrix lemmas.
• Lemma 2: the per-firm comparison of robust best responses.
• Three claims from the proof of Theorem 3(a):
  • the componentwise bound $|RB(\hat p)-RB(\tilde p)|\le\Lambda(R)|\hat p-\tilde p|$;
  • $\Lambda(R)\ge 0$ with spectral radius $\rho(\Lambda(R))<1$;
  • for every $\varepsilon>0$, an absolute norm whose induced norm satisfies $\|\Lambda(R)\|\le\rho(\Lambda(R))+\varepsilon$.

Significance

Theorem 3 makes the special equilibrium an operational prediction. Firms that adjust prices myopically, each using only its own demand and cost information, converge to $(p^*|w)$ from any start. The convergence is geometric, so the number of rounds needed to come within $\epsilon$ grows only logarithmically in the initial distance. This holds although the game is not supermodular and can have infinitely many equilibria, so the lattice-theoretic stability results that cover supermodular games do not apply. Theorem 2 also identifies which of the possibly many equilibria the dynamics select.

The result is proved in the paper, but it has not been formalized. A machine-checked version has two parts: a model layer (affine multi-product demand, the cost projection, robust best responses), and an M-matrix layer (Lemma B.1: inverse-positivity, Schur complements of inverse M-matrices, spectral radius bounds). Mathlib has neither. The proof also rests on results that the paper cites without proof: Propositions 2 and 3 of Federgruen and Hu (2015), and Theorem 4(b) and Lemma B.2(d) of Federgruen and Hu (2016). A formalization has to supply them. In one place the proof cites Horn and Johnson (1985, Lemma 5.6.10) for an absolute norm close to the spectral radius. As stated there, that lemma does not give absoluteness for general matrices: $\begin{pmatrix}1&1\\-1&-1\end{pmatrix}$ has spectral radius $0$, but every absolute norm gives it induced norm at least $1$. The claim holds for the nonnegative matrix $\Lambda(R)$, and the corresponding milestone is stated for that matrix only.

Difficulty

The obvious route is to show that $RB$ is a contraction in the sup norm and invoke Banach's fixed-point theorem. This fails: $\|\Lambda(R)\|_\infty$ can exceed $1$ even though $\rho(\Lambda(R))<1$, and the bound $|RB(\hat p)-RB(\tilde p)|\le\Lambda(R)|\hat p-\tilde p|$ is all the structure gives. The norm must be adapted to $\Lambda(R)$ and must also be absolute, so that the componentwise bound transfers. The per-firm estimate behind that bound (Lemma 2) is itself not a Lipschitz estimate for an explicit formula. The robust best response is the solution of a constrained quadratic program whose active set changes with the competitors' prices, and the comparison goes through a componentwise minimum $\check p=\min\{\hat p,\tilde p\}$ and monotonicity in the intercept. Separately, the fixed-point property needs the cost projection $\Theta(w)$, an LCP whose unique solvability and nonnegativity depend on (IS).

Formalization scope

Products form a finite type ι and firms a type F, with firm : ι → F assigning each product to its firm. Vectors are ι → ℝ with the pointwise order. Matrices are Matrix ι ι ℝ, and every matrix inequality is entrywise. The commitments are:

• (P) is ∀ x ≠ 0, 0 < x ⬝ᵥ R *ᵥ x, not Mathlib's Matrix.PosDef, which would add global symmetry.
• The special equilibrium $(p^*|w)$ is written through any solution $w'$ of the LCP (12)–(14). The paper says this form is valid for all $w>0$. A milestone proves that the solution exists, is unique, and is nonnegative.
• The robust best response is a relation, "$q$ is a robust best response to $p$", with the feasibility constraint of (8) built in. Lemma 1 makes it single-valued. Part (b) of the goal is stated for every robust best-response sequence started at $p^0\ge 0$.
• "A norm on $\mathbb R^{\mathcal N}$" is a seminorm that vanishes only at $0$.
• The spectral radius is that of the matrix viewed over $\mathbb C$, so complex eigenvalues count.
• Matrix inverses use Mathlib's ⁻¹. Every inverted matrix is invertible under the hypotheses.

No trivializing reading is available. The norm must be definite, the robust best response keeps its feasibility constraint and is never defined by a closed form, and the convergence statement holds for every iterate. A sorry-free sanity check confirms that the standing assumptions, the cost projection and the fixed-point relation are all satisfiable on a two-firm example.

The following results are not formalized here:

• Theorem 1 and Proposition 1, which characterize the set of Nash equilibria and the existence of $(p^*|w)$ under the full LCP-extended demand. They are independent of the goal.
• Example 1, Lemma B.2, Lemma C.1 and Proposition 2 of Appendix D.

Contributions that would be reusable beyond this mission include:

• a general M-matrix library (inverse-positivity, Schur complements, Perron–Frobenius bounds);
• uniqueness for P-matrix LCPs;
• the existence of absolute norms close to the spectral radius for nonnegative matrices.

Selected references

• A. Federgruen, M. Hu, Technical Note—Global Robust Stability in a General Price and Assortment Competition Model, Operations Research 69(1) 164–174, 2021. https://doi.org/10.1287/opre.2020.2001 (submitted manuscript: https://ssrn.com/abstract=3010503)
• A. Federgruen, M. Hu, Multi-Product Price and Assortment Competition, Operations Research 63(3) 572–584, 2015.
• A. Federgruen, M. Hu, Sequential Multiproduct Price Competition in Supply Chain Networks, Operations Research 64(1) 135–149, 2016.
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985; Topics in Matrix Analysis, Cambridge University Press, 1991.
• I. N. Imam, The Schur complement and the inverse M-matrix problem, Linear Algebra and its Applications 62 235–240, 1984.
• T. W. McGuire, R. Staelin, An industry equilibrium analysis of downstream vertical integration, Marketing Science 27(1) 115–130, 2008 (reprint of Marketing Science 2(2), 1983).