Theorem 9, p. 15 — no randomized online algorithm for b-matching has competitive ratio better than 1 − 1/e, uniformly in the budget b
ProvedAdWordsMSVV.LowerBound.theorem_9Consider online b-matching: bidders, each with the same integer budget , bidding or on each of queries that arrive online.
For every there is such that for every , every budget and every randomized online algorithm for instances with bidders and queries, there exist an instance and an offline allocation with
Thus no randomized online algorithm achieves a competitive ratio better than for b-matching, and this holds for every budget , in particular for large , where the deterministic algorithm BALANCE attains in the limit. The case is the online bipartite matching lower bound of Karp, Vazirani and Vazirani.
Formalization Note "Competitive ratio better than " is negated as: for every some instance has expected revenue at most times its optimum; the optimum is witnessed by (no allocation can exceed , since each of the bidders is capped at ). The algorithm is quantified before the instance. "For large " is rendered by quantifying over every with a threshold independent of , which implies the statement for all large . The paper's instance with budget and bids is the same instance scaled by .
import Mathlib import Definitions.Def_AdWordsMSVV_LowerBound_Setting
namespace AdWordsMSVV.LowerBound
theorem theorem_9 :
∀ δ : ℝ, 0 < δ → ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → ∀ B : ℕ, 1 ≤ B →
∀ A : RandAlg N (N * B), ∃ (I : Instance N (N * B)) (τ : Fin (N * B) → Option (Fin N)),
offlineRevenue B I τ = N * B ∧
expectedRevenue B I A ≤ (1 - Real.exp (-1) + δ) * ((N : ℝ) * B) := by sorry
end AdWordsMSVV.LowerBound
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.