Step (iii): the best layer has welfare at least OPT*/(3k)

Proved

ComplementFreeCA.CFRounding.best_layer_bound

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

approximation-algorithmscombinatorial-auctionsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1subadditive-valuations

Let $v_1,\dots,v_n$ be normalized, complement-free valuations, let $x$ be any point with LP value $L=\sum_{i,S}x_{i,S}v_i(S)$ , and let $k\ge1$ . Let $\sigma=(S_1,\dots,S_n)$ be a preallocation in which every item appears in at most $k$ bundles and

\sum_i v_i(S_i)\ge \tfrac13 L.

If $r$ with $1\le r\le k$ maximizes $\sum_i v_i(S_i^r)$ over $1\le r\le k$ , then

\sum_i v_i(S_i^r)\ \ge\ \frac{L}{3k}.

With $x$ optimal, $L=OPT^*$ , and this is the bound $\sum_i v_i(S^r_i)\ge OPT^*/(3k)$ of step (iii) of the proof of Theorem 3.1: the best layer is a feasible allocation within a factor $3k$ of the fractional optimum.

Formalization Note The statement holds for any $x$ whose value $L$ satisfies the displayed hypothesis; optimality of $x$ is not needed for this step.

Preamble

import Mathlib
import Definitions.Def_ComplementFreeCA_CFRounding_Auction
import Definitions.Def_ComplementFreeCA_CFRounding_LP
import Definitions.Def_ComplementFreeCA_CFRounding_Algorithm

Formal statement

namespace ComplementFreeCA.CFRounding

theorem best_layer_bound {n m : ℕ} (v : Fin n → Finset (Fin m) → ℝ)
    (hnorm : ∀ i, IsNormalized (v i)) (hsub : ∀ i, IsSubadditive (v i))
    (x : Fin n → Finset (Fin m) → ℝ) (σ : Fin n → Finset (Fin m)) (k : ℕ) (hk : 1 ≤ k)
    (hcount : ∀ j, count σ j ≤ k) (hval : lpValue v x / 3 ≤ welfare v σ)
    (r : ℕ) (hr : IsBestLayer v σ k r) :
    lpValue v x / (3 * k) ≤ welfare v (fun i => layer σ i r) := by sorry

end ComplementFreeCA.CFRounding

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 (iii)

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