Inequality (8) — the facility cost of a bad facility

Proved

LocalSearchFL.UFL.bad_facility_inequality_8

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

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

Let $f_i \ge 0$ be facility opening costs on a metric instance, let $S$ be a nonempty set of facilities that is locally optimum for the add/drop/swap neighbourhood (4), and let $O$ be any solution. Let $\sigma_S$ , $\sigma_O$ be nearest-facility assignments for $S$ and $O$ , write $S_j = c_{j\sigma_S(j)}$ and $O_j = c_{j\sigma_O(j)}$ , and let $\pi$ be a permutation of the clients satisfying the three conditions of the mapping of the proof of Lemma 4.2.

If $s \in S$ is bad, and $P \subseteq O$ is the set of facilities of $O$ that $s$ captures, then

\sum_{o' \in P} f_{o'} - f_s + \sum_{\substack{j \in N_S(s)\\ \pi(j) \neq j}} \bigl(O_j + O_{\pi(j)} + S_{\pi(j)} - S_j\bigr) + 2 \sum_{\substack{j \in N_S(s)\\ \pi(j) = j}} O_j \ \ge\ 0.

It is the counterpart for bad facilities of inequality (5): adding (5) over the good facilities, (8) over the bad ones, and $f_o \ge 0$ over the facilities of $O$ captured by no one yields Lemma 4.2.

Preamble

import Mathlib
import Definitions.Def_LocalSearchFL_UFL_captures

Formal statement

namespace LocalSearchFL.UFL

/-- Inequality (8), p. 556. Let `S` be a locally optimum solution for the neighbourhood (4), `O`
any solution, `σS`, `σO` nearest-facility assignments, `π` the mapping of the proof of
Lemma 4.2. If `s ∈ S` is bad and `P ⊆ O` is the set of facilities that `s` captures, then
`∑_{o' ∈ P} f_{o'} − f_s + ∑_{j ∈ N_S(s), π(j) ≠ j} (O_j + O_{π(j)} + S_{π(j)} − S_j)
  + 2 ∑_{j ∈ N_S(s), π(j) = j} O_j ≥ 0`. -/
theorem bad_facility_inequality_8 {Cl Fa : Type} [Fintype Cl] [DecidableEq Cl]
    [Fintype Fa] [DecidableEq Fa]
    (I : MetricInstance Cl Fa) (f : Fa → ℝ) (hf : ∀ i, 0 ≤ f i)
    (S O : Finset Fa) (hS : S.Nonempty) (hloc : IsUFLLocalOpt I f S hS)
    (σS σO : Cl → Fa) (hσS : IsNearestAssignment I S σS) (hσO : IsNearestAssignment I O σO)
    (π : Equiv.Perm Cl) (hπ : IsRefinedPi σS σO π)
    (s : Fa) (hs : s ∈ S) (hbad : ¬ IsGood σS σO O s) :
    0 ≤ ∑ o' ∈ O.filter (fun o' => captures σS σO s o'), f o' - f s +
      ∑ j ∈ (nbhd σS s).filter (fun j => π j ≠ j),
        (I.c j (σO j) + I.c (π j) (σO (π j)) + I.c (π j) (σS (π j)) - I.c j (σS j)) +
      2 * ∑ j ∈ (nbhd σS s).filter (fun j => π j = j), I.c j (σO j) := 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. 556, eq. (8) (from eq. (6) and eq. (7))

Read-back

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

Setting. Let $\mathcal C$ (clients) and $\mathcal F$ (facilities) be finite types with decidable equality. Let $I$ be a metric instance: $d$ on pairs of points of $\mathcal C\sqcup\mathcal F$ , nonnegative, symmetric, triangle inequality, self-distance not assumed zero. Write $c_{ji}=d(j,i)$ . Let $f:\mathcal F\to\mathbb R$ satisfy $f_i\ge0$ for all $i$ . For nonempty $A\subseteq\mathcal F$ , write $\mathrm{cost}(A)=\sum_{i\in A}f_i+\sum_{j\in\mathcal C}\min_{i\in A}c_{ji}$ .

Hypotheses.

$S,O$ are finite sets of facilities, and $S$ is nonempty.
$S$ is locally optimal:
- $\mathrm{cost}(S)\le\mathrm{cost}(S\cup\{s'\})$ for every facility $s'$ ;
- $\mathrm{cost}(S)\le\mathrm{cost}(S\setminus\{s\})$ for every $s\in S$ with $S\setminus\{s\}\ne\emptyset$ ;
- $\mathrm{cost}(S)\le\mathrm{cost}((S\setminus\{s\})\cup\{s'\})$ for all $s\in S$ and all facilities $s'$ .
$\sigma_S,\sigma_O:\mathcal C\to\mathcal F$ are nearest-facility assignments:
- for every $j$ : $\sigma_S(j)\in S$ with $c_{j\sigma_S(j)}\le c_{ji}$ for all $i\in S$ ;
- for every $j$ : $\sigma_O(j)\in O$ with $c_{j\sigma_O(j)}\le c_{ji}$ for all $i\in O$ .
Write $S_j=c_{j\sigma_S(j)}$ and $O_j=c_{j\sigma_O(j)}$ .
Write $N_S(s)=\{j:\sigma_S(j)=s\}$ , $N_O(o)=\{j:\sigma_O(j)=o\}$ and $N^o_s=N_O(o)\cap N_S(s)$ . Say that $s$ captures $o$ when $|N_O(o)|<2|N^o_s|$ .
$\pi$ is a permutation of $\mathcal C$ satisfying all three of:
- (i) $\sigma_O(\pi(j))=\sigma_O(j)$ for all $j$ ;
- (ii) for all facilities $s,o$ with $s$ not capturing $o$ : $j\in N^o_s\Rightarrow\pi(j)\notin N^o_s$ ;
- (iii) for all facilities $s,o$ with $s$ capturing $o$ : $j,\pi(j)\in N^o_s\Rightarrow\pi(j)=j$ .
$s\in S$ is bad: it is not the case that $s$ captures no $o\in O$ . In other words, $s$ captures at least one $o\in O$ .

Conclusion. Let $P=\{o'\in O: s \text{ captures } o'\}$ . Then

0\le \sum_{o'\in P}f_{o'}-f_s+\sum_{\substack{j\in N_S(s)\\ \pi(j)\ne j}}\big(O_j+O_{\pi(j)}+S_{\pi(j)}-S_j\big)+2\sum_{\substack{j\in N_S(s)\\ \pi(j)=j}}O_j,

where $O_{\pi(j)}=c_{\pi(j)\sigma_O(\pi(j))}$ and $S_{\pi(j)}=c_{\pi(j)\sigma_S(\pi(j))}$ . The first sum ranges over $P$ only. The subtraction of $f_s$ and the other two sums lie outside it.

Degenerate cases. Badness forces $P\ne\emptyset$ and some $|N^o_s|\ge1$ . So $\mathcal C$ and $O$ are nonempty, and $N_S(s)\ne\emptyset$ .

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