Lemma 3.6 — every allocation's welfare is at most twice the final prices

Proved

ComplementFreeCA.XOSGreedy.optimal_welfare_le_two_final_prices

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

combinatorial-auctionsgreedy-algorithmsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1xos-valuations

Let $v_1,\dots,v_n$ be XOS valuations on the items $M=\{1,\dots,m\}$ given by XOS expressions, and let the greedy price-update algorithm of §3.3 run with any demand oracle and any XOS oracle for this profile, with final prices $p^n$ . Then for every allocation $O_1,\dots,O_n$ (pairwise disjoint bundles),

\sum_{i=1}^n v_i(O_i)\le 2\,p^n(M),\qquad p^n(M)=\sum_{j\in M}p^n_j .

The paper states it for the optimal allocation; holding for every allocation is equivalent and needs no optimal allocation to be named. Combined with Lemma 3.4 it yields Theorem 3.3.

Preamble

import Mathlib
import Definitions.Def_ComplementFreeCA_XOSGreedy_Model
import Definitions.Def_ComplementFreeCA_XOSGreedy_GreedyRun

Formal statement

namespace ComplementFreeCA.XOSGreedy

theorem optimal_welfare_le_two_final_prices {n m : ℕ} (E : Fin n → XOSExpr m)
    (dem : Fin n → (Fin m → ℝ) → Finset (Fin m)) (cl : Fin n → Finset (Fin m) → (Fin m → ℝ))
    (hdem : IsDemandOracle E dem) (hcl : IsXOSOracle E cl)
    (O : Fin n → Finset (Fin m)) (hO : IsAllocation O) :
    welfare E O ≤ 2 * ∑ j, greedyPrices dem cl n j := by sorry

end ComplementFreeCA.XOSGreedy

Source

Dobzinski, Nisan, Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Math. Oper. Res. 35(1), 2010, p. 8, Lemma 3.6 (proof on pp. 8–9)

Human review

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

View graph