The k-center problem

Given points with a distance d : V → V → α and a number k, the k-center problem asks for a set S of at most k centers minimizing the largest distance from a point to its nearest center ([WS11], Section 2.2). This module defines the objective and proves the packing lower bound shared by the 2-approximation algorithms.

Model

Distances take values in a linear order α; the bounds additionally use a semiring structure (ℕ, ℚ, ℝ, …) to write 2 * r. No metric axioms are part of the definitions: the results that need them take symmetry d x y = d y x and the triangle inequality d x z ≤ d x y + d y z as hypotheses, so a Mathlib PseudoMetricSpace instantiates them with dist. The distance from a point to a set of centers lives in WithTop α and is ⊤ for the empty set.

The radius and the optimum are defined on a finite nonempty type of points, with centers allowed anywhere among them. The optimum ranges over center sets of at most k points; when k ≤ Fintype.card V some set of exactly k points attains it (exists_card_eq_radius_eq_optRadius), so this is the same optimum as over sets of exactly k points, as in [WS11], because padding a set of centers never increases its radius (radius_anti).

Main definitions

• Cslib.Algorithms.Lean.KCenter.centerDist: the distance d(v, S) from a point to its nearest center.
• Cslib.Algorithms.Lean.KCenter.radius: the radius max_v d(v, S) of a set of centers.
• Cslib.Algorithms.Lean.KCenter.optRadius: the optimal radius over at most k centers.

Main results

• centerDist_le_coe_iff, coe_lt_centerDist_iff, centerDist_lt_coe_iff: d(v, S) compared with a value.
• radius_le_coe_iff, optRadius_le_iff, le_optRadius_iff, exists_radius_eq_optRadius: the radius and the optimum compared with a value; the optimum is attained.
• exists_card_eq_radius_eq_optRadius: for k ≤ |V| the optimum is attained by exactly k centers.
• radius_anti, optRadius_antitone, optRadius_zero, optRadius_lt_top: monotonicity and the degenerate cases.
• length_le_card_of_pairwise_lt: packing: points pairwise farther than 2 r apart need distinct centers within r.
• lt_optRadius_of_pairwise_lt: k + 1 points pairwise farther than 2 r apart force an optimal radius above r.

References

• D. P. Williamson and D. B. Shmoys, The Design of Approximation Algorithms, Section 2.2.

Distance to a set of centers

def Cslib.Algorithms.Lean.KCenter.centerDist {V : Type u_1} {α : Type u_2} [LinearOrder α] (d : V → V → α) (S : Finset V) (v : V) : WithTop α

The distance d(v, S) = min_{c ∈ S} d v c from v to its nearest center in S, in WithTop α. It is ⊤ when S is empty.

theorem Cslib.Algorithms.Lean.KCenter.centerDist_le_coe_iff {V : Type u_1} {α : Type u_2} [LinearOrder α] {d : V → V → α} {S : Finset V} {v : V} {r : α} : centerDist d S v ≤ ↑r ↔ ∃ c ∈ S, d v c ≤ r

d(v, S) ≤ r exactly when some center of S is within r of v.

theorem Cslib.Algorithms.Lean.KCenter.coe_lt_centerDist_iff {V : Type u_1} {α : Type u_2} [LinearOrder α] {d : V → V → α} {S : Finset V} {v : V} {r : α} : ↑r < centerDist d S v ↔ ∀ c ∈ S, r < d v c

r < d(v, S) exactly when every center of S is farther than r from v.

theorem Cslib.Algorithms.Lean.KCenter.centerDist_lt_coe_iff {V : Type u_1} {α : Type u_2} [LinearOrder α] {d : V → V → α} {S : Finset V} {v : V} {r : α} : centerDist d S v < ↑r ↔ ∃ c ∈ S, d v c < r

d(v, S) < r exactly when some center of S is closer than r to v.

theorem Cslib.Algorithms.Lean.KCenter.centerDist_le_of_mem {V : Type u_1} {α : Type u_2} [LinearOrder α] {d : V → V → α} {S : Finset V} {v c : V} (hc : c ∈ S) : centerDist d S v ≤ ↑(d v c)

A point is at most as far from a set as from each of its centers.

theorem Cslib.Algorithms.Lean.KCenter.centerDist_anti {V : Type u_1} {α : Type u_2} [LinearOrder α] {d : V → V → α} {S T : Finset V} (h : S ⊆ T) (v : V) : centerDist d T v ≤ centerDist d S v

Adding centers brings every point closer.

@[simp]

theorem Cslib.Algorithms.Lean.KCenter.centerDist_empty {V : Type u_1} {α : Type u_2} [LinearOrder α] (d : V → V → α) (v : V) : centerDist d ∅ v = ⊤

@[simp]

theorem Cslib.Algorithms.Lean.KCenter.centerDist_singleton {V : Type u_1} {α : Type u_2} [LinearOrder α] (d : V → V → α) (c v : V) : centerDist d {c} v = ↑(d v c)

Packing

theorem Cslib.Algorithms.Lean.KCenter.length_le_card_of_pairwise_lt {V : Type u_1} {α : Type u_2} [LinearOrder α] [Semiring α] [IsOrderedAddMonoid α] {d : V → V → α} (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) {C : Finset V} {r : α} {M : List V} (hcov : ∀ v ∈ M, ∃ c ∈ C, d v c ≤ r) (hM : List.Pairwise (fun (a b : V) => 2 * r < d a b) M) : M.length ≤ C.card

Packing ([WS11], proof of Theorem 2.3): if every entry of a list M is within r of a center of C, and the entries of M are pairwise farther than 2 r apart, then M has at most |C| entries. By the triangle inequality, two points within r of the same center are at most 2 r apart.

Radius and optimum on a finite space

def Cslib.Algorithms.Lean.KCenter.radius {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] (d : V → V → α) (S : Finset V) : WithTop α

The radius max_v d(v, S) of a set S of centers in a finite space: the largest distance from a point to its nearest center. It is ⊤ exactly when S is empty.

def Cslib.Algorithms.Lean.KCenter.optRadius {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] (d : V → V → α) (k : ℕ) : WithTop α

The optimal k-center radius min_{|S| ≤ k} radius S of a finite space. It is ⊤ exactly when k = 0.

theorem Cslib.Algorithms.Lean.KCenter.radius_le_iff {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S : Finset V} {r : WithTop α} : radius d S ≤ r ↔ ∀ (v : V), centerDist d S v ≤ r

theorem Cslib.Algorithms.Lean.KCenter.radius_le_coe_iff {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S : Finset V} {r : α} : radius d S ≤ ↑r ↔ ∀ (v : V), ∃ c ∈ S, d v c ≤ r

The radius of S is at most r exactly when every point is within r of a center.

theorem Cslib.Algorithms.Lean.KCenter.radius_lt_iff {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S : Finset V} {r : WithTop α} : radius d S < r ↔ ∀ (v : V), centerDist d S v < r

theorem Cslib.Algorithms.Lean.KCenter.centerDist_le_radius {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S : Finset V} (v : V) : centerDist d S v ≤ radius d S

theorem Cslib.Algorithms.Lean.KCenter.radius_anti {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S T : Finset V} (h : S ⊆ T) : radius d T ≤ radius d S

Adding centers never increases the radius.

@[simp]

theorem Cslib.Algorithms.Lean.KCenter.radius_empty {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] (d : V → V → α) : radius d ∅ = ⊤

theorem Cslib.Algorithms.Lean.KCenter.radius_lt_top {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S : Finset V} (hS : S.Nonempty) : radius d S < ⊤

A nonempty set of centers has finite radius.

theorem Cslib.Algorithms.Lean.KCenter.optRadius_le_radius {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {S : Finset V} {k : ℕ} (hS : S.card ≤ k) : optRadius d k ≤ radius d S

theorem Cslib.Algorithms.Lean.KCenter.exists_radius_eq_optRadius {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] (d : V → V → α) (k : ℕ) : ∃ (S : Finset V), S.card ≤ k ∧ radius d S = optRadius d k

Some set of at most k centers attains the optimal radius.

theorem Cslib.Algorithms.Lean.KCenter.optRadius_le_iff {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {k : ℕ} {r : WithTop α} : optRadius d k ≤ r ↔ ∃ (S : Finset V), S.card ≤ k ∧ radius d S ≤ r

theorem Cslib.Algorithms.Lean.KCenter.le_optRadius_iff {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {k : ℕ} {r : WithTop α} : r ≤ optRadius d k ↔ ∀ (S : Finset V), S.card ≤ k → r ≤ radius d S

theorem Cslib.Algorithms.Lean.KCenter.exists_card_eq_radius_eq_optRadius {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {k : ℕ} (d : V → V → α) (hk : k ≤ Fintype.card V) : ∃ (S : Finset V), S.card = k ∧ radius d S = optRadius d k

Exactly k centers suffice: when k ≤ |V|, some set of exactly k centers attains the optimal radius over at most k centers, since padding a set of centers never increases its radius (radius_anti). So optRadius agrees with the optimum over sets of exactly k points used in [WS11], Section 2.2.

theorem Cslib.Algorithms.Lean.KCenter.optRadius_antitone {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] (d : V → V → α) : Antitone (optRadius d)

Allowing more centers never increases the optimal radius.

@[simp]

theorem Cslib.Algorithms.Lean.KCenter.optRadius_zero {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] (d : V → V → α) : optRadius d 0 = ⊤

Without centers, the radius is ⊤.

theorem Cslib.Algorithms.Lean.KCenter.optRadius_lt_top {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {k : ℕ} (hk : 0 < k) : optRadius d k < ⊤

With at least one center, the optimal radius is finite.

theorem Cslib.Algorithms.Lean.KCenter.lt_optRadius_of_pairwise_lt {V : Type u_1} {α : Type u_2} [Fintype V] [Nonempty V] [LinearOrder α] {d : V → V → α} {k : ℕ} [Semiring α] [IsOrderedAddMonoid α] (hsymm : ∀ (x y : V), d x y = d y x) (htri : ∀ (x y z : V), d x z ≤ d x y + d y z) {r : α} {M : List V} (hM : List.Pairwise (fun (a b : V) => 2 * r < d a b) M) (hk : k < M.length) : ↑r < optRadius d k

A lower bound on the optimum ([WS11], proof of Theorem 2.3): if more than k points are pairwise farther than 2 r apart, every set of at most k centers has radius greater than r.