Proof of Theorem 5.1 — a CF valuation is at most |T| times its best single item

Proved

ComplementFreeCA.ValueQuery.cf_le_card_mul_max_singleton

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

combinatorial-auctionsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1subadditive-valuations

Let $v$ be a normalized, monotone, complement-free valuation on bundles of $M=\{1,\dots,m\}$ , let $T\subseteq M$ and let $c\in T$ be an item maximizing $v(\{j\})$ over $j\in T$ . Then

v(T)\;\le\;\sum_{j\in T} v(\{j\})\;\le\;|T|\cdot v(\{c\}).

This is the step " $v_i(\{c_i\})\ge v_i(T_i)/|T_i|$ " of the second case of the proof of Theorem 5.1: a subadditive bidder's value for a small bundle is recovered, up to the bundle's size, by its most valuable single item.

Formalization Note The division by $|T|$ of the paper is avoided by stating the multiplied form; $c\in T$ makes $T$ nonempty.

Preamble

import Mathlib
import Definitions.Def_ComplementFreeCA_ValueQuery_Basic

open Finset

Formal statement

namespace ComplementFreeCA.ValueQuery

/-- Proof of Theorem 5.1 (p. 12): for a CF valuation and an item `c` of `T` maximizing
`v({j})` over `j ∈ T`, `|T| · v({c}) ≥ ∑_{j ∈ T} v({j}) ≥ v(T)`. -/
theorem cf_le_card_mul_max_singleton {m : ℕ} (v : Finset (Fin m) → ℝ) (hv : IsCFValuation v)
    (T : Finset (Fin m)) (c : Fin m) (hc : c ∈ T) (hmax : ∀ j ∈ T, v {j} ≤ v {c}) :
    v T ≤ ∑ j ∈ T, v {j} ∧ ∑ j ∈ T, v {j} ≤ (T.card : ℝ) * v {c} := by sorry

end ComplementFreeCA.ValueQuery

Source

Dobzinski, Nisan, Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Math. Oper. Res. 35(1), 2010, p. 12, proof of Theorem 5.1, second case, parenthetical 'this is because of the CF property …'

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