LEMMA 7.2 (as applied in the proof of LEMMA 8.3) — prices of an $n^{-5}$ -equilibrium of $D(\mathcal C)$ are positive and within a factor 2

Proved

PLCMarkets.ExactCover.lemma_7_2_prices_within_factor_two

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximate-equilibriumarrow-debreumarket-equilibriump2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $n>35$ be a multiple of $3$ and let $\mathcal C=(C_1,\dots,C_n)$ be a family of $3$ -element subsets of $X=\{x_1,\dots,x_n\}$ whose union is $X$ . If $p$ is an $\epsilon$ -approximate market equilibrium of the Arrow–Debreu market $D(\mathcal C)$ with $\epsilon=n^{-5}$ , then all prices are positive and within a factor $2$ of each other:

p(j)>0\quad\text{and}\quad p(j)\le 2\,p(k)\qquad\text{for all goods } j,k .

This is the price-regulation property enforced by agent $0$ , whose endowment dominates the market; the proof of Lemma 8.3 starts from it.

Formalization Note. Lemma 7.2 of the paper (p. 10:17) reads: "In any 0.9-approximate price equilibrium for this Fisher market instance F, the prices of all the goods are positive and are within a factor 2 of each other." It is stated for the Fisher instance of §7, which is built on a black-box market of Chen et al.; the proof of Lemma 8.3 (p. 10:21) applies it to the §8 markets with $\epsilon=n^{-5}$ . This item states that application, for the market $D(\mathcal C)$ , not the §7 lemma.

Preamble

import Mathlib
import Definitions.Def_PLCMarkets_ExactCover_X3C
import Definitions.Def_PLCMarkets_ExactCover_MarketD

Formal statement

namespace PLCMarkets.ExactCover

theorem lemma_7_2_prices_within_factor_two (n : ℕ) (C : Fin n → Finset (Fin n))
    (hcard : ∀ i, (C i).card = 3) (hdiv : 3 ∣ n) (hn : 35 < n)
    (hcover : ∀ x : Fin n, ∃ i, x ∈ C i)
    (p : Good n → ℝ)
    (hp : (marketD C).IsApproxEquilibrium (((n : ℝ) ^ 5)⁻¹) p) :
    (∀ j, 0 < p j) ∧ ∀ j k, p j ≤ 2 * p k := by sorry

end PLCMarkets.ExactCover

Source

Vazirani and Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, J. ACM 58(3), Article 10, 2011, p. 10:17, LEMMA 7.2, as invoked on p. 10:21 in the proof of LEMMA 8.3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $n\in\mathbb{N}$ and let $C=(C_i)_{i<n}$ be a family of subsets of $\{0,\dots,n-1\}$ . Assume:

$|C_i|=3$ for every $i$ ;
$3\mid n$ ;
$n>35$ ;
every element lies in some $C_i$ .

Let $p$ be any real price vector on the $2n+1$ goods of $D(C)$ that is a $\tfrac1{n^5}$ -approximate equilibrium of $D(C)$ (the market is described below). That means:

$p\ge 0$ and $\sum p=1$ ;
there is an allocation $x$ giving every agent an optimal bundle, in the sense spelled out below;
for every good $j$ ,

\Bigl|\sum_i x_{ij}-s_j\Bigr|\le \frac{1}{n^5}\,s_j,

where $s_j$ is the total endowment of good $j$ .

Conclusion. Every price is strictly positive, and for all goods $j,k$ ,

p_j\le 2\,p_k.

The market $D(C)$ .

Goods: $0$ , $C_i$ , $x_j$ .
Agents: a regulator, $C_i$ , $x_j$ , and an extra agent $E$ .
Endowments: the regulator owns $n^3$ of every good; $C_i$ owns $1$ of good $C_i$ ; $x_j$ owns $\tfrac16$ of good $x_j$ ; $E$ owns $\tfrac n2$ of good $0$ .
Utilities: for $y\ge 0$ $y \geq 0$ , " $(c,a)$ $(c, a)$ " means the utility $c\min(y,a)$ $c min (y, a)$ , with no utility beyond $a$ $a$ .
- Regulator, every good: $2\min(y,n^3)+\max(y-n^3,0)$ .
- $C_i$ : $(1,\tfrac12)$ on good $0$ , $(\tfrac13,\tfrac16)$ on each $x_j$ with $j\in C_i$ , $(\tfrac19,\tfrac14)$ on its own good $C_i$ , and $0$ elsewhere.
- $x_j$ : $(1,\tfrac1{12})$ on good $0$ only.
- $E$ : $(1,\tfrac34)$ on each good $C_i$ only.

Optimal bundle. A bundle is optimal for an agent if:

it is nonnegative;
it is affordable at income $\sum_j p_jw_{ij}$ ;
no nonnegative affordable bundle gives more utility;
it holds no more of a good with final slope $0$ than that utility's total piece length, so $0$ of every good valued flat.

Degenerate cases. Since $n\ge 36$ , $\tfrac1{n^5}$ is a well-defined positive number. The statement is conditional: if no approximate equilibrium exists for a given $C$ , it holds vacuously for that $C$ . It does not assert that one exists. Repeated sets $C_i=C_k$ with $i\ne k$ are allowed.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

LEMMA 7.2 (as applied in the proof of LEMMA 8.3) — prices of an n−5n^{-5}n−5-equilibrium of D(C)D(\mathcal C)D(C) are positive and within a factor 2

LEMMA 7.2 (as applied in the proof of LEMMA 8.3) — prices of an $n^{-5}$ -equilibrium of $D(\mathcal C)$ are positive and within a factor 2