Prove2Me

Shifting lemma: the best of kk shifted optima is a (1−1/k)(1-1/k)-approximation

Proved
WilliamsonShmoys.shifting_bound

by Gabewhigham · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximation-algorithmsindependent-setplanar-graphs

Let GG be a simple graph on a vertex set VV, let w:V→Rw : V \to \mathbb{R} be arbitrary real weights, let k≥1k \ge 1, and let c:V→Nc : V \to \mathbb{N} be any labelling (in Baker's technique, the breadth-first-search level). For 0≤j<k0 \le j < k write Vj={v:c(v)≡j(modk)}V_j = \{v : c(v) \equiv j \pmod k\}. Suppose a finite set A⊆VA \subseteq V has weight at least that of every independent set avoiding some class, i.e.

∑v∈Sw(v)≤∑v∈Aw(v)for every j<k and every independent S with S∩Vj=∅.\sum_{v\in S} w(v) \le \sum_{v \in A} w(v) \quad \text{for every } j<k \text{ and every independent } S \text{ with } S\cap V_j=\emptyset.

Then for every finite independent set SS,

(1−1k)∑v∈Sw(v)≤∑v∈Aw(v).\Bigl(1-\frac1k\Bigr)\sum_{v\in S} w(v) \le \sum_{v\in A} w(v).

This is the averaging argument behind Baker's shifting technique in the proof of Theorem 10.11: the kk sets S∖VjS\setminus V_j are independent and together cover every vertex of SS exactly k−1k-1 times, so their total weight is (k−1)w(S)(k-1)w(S) and one of them has weight at least (1−1/k)w(S)(1-1/k)w(S).

Preamble
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

set_option autoImplicit false
open scoped BigOperators
Formal statement
namespace WilliamsonShmoys
theorem shifting_bound {V : Type} (G : SimpleGraph V) (w : V → ℝ) (c : V → ℕ)
    (k : ℕ) (hk : 0 < k) (A : Finset V)
    (hA : ∀ j < k, ∀ S : Finset V, G.IsIndepSet (S : Set V) →
      (∀ v ∈ S, c v % k ≠ j) → ∑ i ∈ S, w i ≤ ∑ i ∈ A, w i)
    (S : Finset V) (hS : G.IsIndepSet (S : Set V)) :
    (1 - 1 / (k : ℝ)) * ∑ i ∈ S, w i ≤ ∑ i ∈ A, w i := by sorry
end WilliamsonShmoys
Source
David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Section 10.2, proof of Theorem 10.11, pp. 270-272. https://doi.org/10.1017/CBO9780511921735. (the averaging step: some shift loses at most a 1/k fraction of the optimum)

View graph