Prove2Me

The optimal fractional value OPT∗OPT^* bounds the welfare of every allocation

Proved
ComplementFreeCA.XOSRounding.lp_optimum_ge_welfare

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

combinatorial-auctionslinear-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let v1,…,vnv_1,\dots,v_n be valuations on the bundles of M={1,…,m}M=\{1,\dots,m\} and let xx be an optimal solution of the LP relaxation, with value OPT∗=∑i,Sxi,Svi(S)\mathrm{OPT}^*=\sum_{i,S}x_{i,S}v_i(S). Then for every allocation (O1,…,On)(O_1,\dots,O_n) (pairwise disjoint bundles),

∑ivi(Oi) ≤ OPT∗.\sum_{i} v_i(O_i)\ \le\ \mathrm{OPT}^*.

In particular the optimal fractional value is an upper bound on the value OPT\mathrm{OPT} of the optimal integral allocation.

This is the first link in the chain of the approximation guarantee: the rounding algorithm is compared with OPT∗\mathrm{OPT}^*, and this inequality transfers the guarantee to the integral optimum.

Formalization Note No property of the valuations is needed. The paper states this fact without a label in step (i) of the proof of Theorem 3.1 and uses it again for Theorem 3.2.

Preamble
import Mathlib
import Definitions.Def_ComplementFreeCA_XOSRounding_Model
Formal statement
namespace ComplementFreeCA.XOSRounding

theorem lp_optimum_ge_welfare {n m : ℕ} (v : Fin n → Finset (Fin m) → ℝ)
    (x : Fin n → Finset (Fin m) → ℝ) (hx : IsLPOptimal v x)
    (O : Fin n → Finset (Fin m)) (hO : IsAllocation O) :
    welfare v O ≤ lpValue v x := by sorry

end ComplementFreeCA.XOSRounding
Source
Dobzinski, Nisan, Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Math. Oper. Res. 35(1), 2010, p. 6, §3.1, proof of Theorem 3.1, step (i), first sentence
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