Prove2Me

Lemma 4.2 (facility cost): costf(S)≤costf(O)+2 costs(O)\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2\,\mathrm{cost}_s(O)

Proved
LocalSearchFL.UFL.facility_cost_lemma_4_2

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

facility-locationlocal-searchp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let CC and FF be the clients and facilities of a metric instance, and let fi≥0f_i \ge 0 be the opening cost of facility ii. Let S⊆FS \subseteq F be a nonempty set of facilities that is locally optimum for the add/drop/swap neighbourhood (4). Then for every nonempty set O⊆FO \subseteq F,

costf(S)≤costf(O)+2⋅costs(O).\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2 \cdot \mathrm{cost}_s(O).

Together with Lemma 4.1 this gives the locality gap 3 of Theorem 4.3; the asymmetry between the coefficients of the two lemmas is what the scaling argument of Theorem 4.4 exploits.

Formalization Note No assumption that clients exist is made: with no clients the statement reduces to costf(S)≤costf(O)\mathrm{cost}_f(S) \le \mathrm{cost}_f(O), which the drop and swap moves still give.

Preamble
import Mathlib
import Definitions.Def_LocalSearchFL_UFL_captures
Formal statement
namespace LocalSearchFL.UFL

/-- Lemma 4.2 (facility cost), p. 555. If `S` is a locally optimum solution for the
add/drop/swap neighbourhood (4), then for every solution `O`:
`cost_f(S) ≤ cost_f(O) + 2 · cost_s(O)`. -/
theorem facility_cost_lemma_4_2 {Cl Fa : Type} [Fintype Cl] [DecidableEq Cl]
    [Fintype Fa] [DecidableEq Fa]
    (I : MetricInstance Cl Fa) (f : Fa → ℝ) (hf : ∀ i, 0 ≤ f i)
    (S : Finset Fa) (hS : S.Nonempty) (hloc : IsUFLLocalOpt I f S hS)
    (O : Finset Fa) (hO : O.Nonempty) :
    costF f S ≤ costF f O + 2 * costS I O hO := by sorry

end LocalSearchFL.UFL
Source
Arya, Garg, Khandekar, Meyerson, Munagala, Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3), 2004, p. 555, Lemma 4.2 (proof pp. 555–556)
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Let C\mathcal C (clients) and F\mathcal F (facilities) be finite types with decidable equality. Let II be a metric instance: dd on pairs of points of C⊔F\mathcal C\sqcup\mathcal F, nonnegative, symmetric, triangle inequality, self-distance not assumed zero. Write cji=d(j,i)c_{ji}=d(j,i). Let f:F→Rf:\mathcal F\to\mathbb R satisfy fi≥0f_i\ge0 for all ii. For finite A⊆FA\subseteq\mathcal F, write costf(A)=∑i∈Afi\mathrm{cost}_f(A)=\sum_{i\in A}f_i. For nonempty AA, write

costs(A)=∑j∈Cmin⁡i∈Acji,cost(A)=costf(A)+costs(A).\mathrm{cost}_s(A)=\sum_{j\in\mathcal C}\min_{i\in A}c_{ji}, \qquad \mathrm{cost}(A)=\mathrm{cost}_f(A)+\mathrm{cost}_s(A).

Hypotheses. SS is a nonempty set of facilities that is locally optimal:

  • cost(S)≤cost(S∪{s′})\mathrm{cost}(S)\le\mathrm{cost}(S\cup\{s'\}) for every facility s′s';
  • cost(S)≤cost(S∖{s})\mathrm{cost}(S)\le\mathrm{cost}(S\setminus\{s\}) for every s∈Ss\in S with S∖{s}≠∅S\setminus\{s\}\ne\emptyset;
  • cost(S)≤cost((S∖{s})∪{s′})\mathrm{cost}(S)\le\mathrm{cost}((S\setminus\{s\})\cup\{s'\}) for all s∈Ss\in S and all facilities s′s'.

Conclusion. For every nonempty set OO of facilities:

costf(S)≤costf(O)+2 costs(O).\mathrm{cost}_f(S)\le\mathrm{cost}_f(O)+2\,\mathrm{cost}_s(O).

Degenerate cases.

  • If C=∅\mathcal C=\emptyset, all service costs are 00. The claim becomes ∑i∈Sfi≤∑i∈Ofi\sum_{i\in S}f_i\le\sum_{i\in O}f_i for every nonempty OO, whenever SS is locally optimal for the facility costs alone.
  • If F\mathcal F has one element, S=OS=O and the claim is fi≤fi+2 costs(O)f_i\le f_i+2\,\mathrm{cost}_s(O).
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph