Closest pair of points problem

DefinitionSquared distance in the plane#✓fully proved

Let \(K\) be a linearly ordered field. The squared distance between points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of \(K^2\) is \((p_1 - q_1)^2 + (p_2 - q_2)^2\).

def dist2 (p q : 𝕜 × 𝕜) : 𝕜 := (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2

Used by 16

Used byCost of the brute-force closest-pair scan · Divide and conquer agrees with brute force · The closest-pair algorithm returns no value exactly on fewer than two points · The closest-pair algorithm returns the answer · Correctness of divide-and-conquer closest pair · The closest-pair recursion is correct on lists sorted by first coordinate · Running time of the closest-pair recursion · Closest-pair answer · Least pairwise squared distance · Packing bound for the strip · Least squared distance from a point to a list · The nearest-point scan returns the least squared distance · Same-side points far apart · Strip scan from a point · Cost of the scan from one strip point · The strip scan bounds every pair with a small vertical gap

DefinitionLeast pairwise squared distance#✓fully proved

Let \(K\) be a linearly ordered field, and write \(d(p, q) = (p_1 - q_1)^2 + (p_2 - q_2)^2\) for the squared distance between points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of \(K^2\). For a list \(c_1, \dots, c_n\) of points of \(K^2\), an element \(\delta\) of \(K\) is the least pairwise squared distance of the list when \(\delta = d(c_i, c_j)\) for some \(i < j\) and \(\delta \le d(c_i, c_j)\) for all \(i < j\).

def IsMinPairDist2 (ps : List (𝕜 × 𝕜)) (δ : 𝕜) : Prop :=
  (∃ p q, [p, q] <+ ps ∧ dist2 p q = δ) ∧ ∀ p q, [p, q] <+ ps → δ ≤ dist2 p q

Uses 1 · Used by 2

Statement usesSquared distance in the plane

Used byThe closest-pair algorithm returns no value exactly on fewer than two points · Correctness of divide-and-conquer closest pair

DefinitionLeast squared distance from a point to a list#✓fully proved

Let \(K\) be a linearly ordered field, and write \(d(p, q) = (p_1 - q_1)^2 + (p_2 - q_2)^2\) for the squared distance between points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of \(K^2\). For a point \(p\) and a list \(c_1, \dots, c_m\) of points of \(K^2\), the least squared distance from \(p\) to the list is no value if \(m = 0\) and \(\min_{1 \le k \le m} d(p, c_k)\) otherwise. Computing it is charged one unit of cost per point of the list, \(m\) units in total.

def minDistFrom (p : 𝕜 × 𝕜) : List (𝕜 × 𝕜) → TimeM ℕ (Option 𝕜)
  | [] => pure none
  | q :: qs => do
      ✓
      let r ← minDistFrom p qs
      pure (omin (some (dist2 p q)) r)

Uses 2 · Used by 5

Statement usesSquared distance in the plane · Option minimum

Used byBrute-force closest pair · Cost of the brute-force closest-pair scan · Divide and conquer agrees with brute force · The closest-pair recursion is correct on lists sorted by first coordinate · The nearest-point scan returns the least squared distance

DefinitionBrute-force closest pair#✓fully proved

Let \(K\) be a field with a linear order, and write \(d(p, q) = (x - x')^2 + (y - y')^2\) for the squared distance between points \(p = (x, y)\) and \(q = (x', y')\) of \(K^2\). On a list \(c_1, \dots, c_n\) of points in \(K^2\), the brute-force scan returns no value if \(n < 2\), and otherwise returns \(\min_{i < j} d(c_i, c_j)\): for each \(i\) it computes the least squared distance from \(c_i\) to the later points \(c_{i+1}, \dots, c_n\), and takes the least of these minima. It is charged one unit of cost per squared distance computed.

def bruteMin : List (𝕜 × 𝕜) → TimeM ℕ (Option 𝕜)
  | [] => pure none
  | p :: ps => do
      let a ← minDistFrom p ps
      let b ← bruteMin ps
      pure (omin a b)

Uses 2 · Used by 5

Statement usesLeast squared distance from a point to a list · Option minimum

Used byCost of the brute-force closest-pair scan · Divide and conquer agrees with brute force · Closest-pair recursion · The closest-pair recursion is correct on lists sorted by first coordinate · Running time of the closest-pair recursion

DefinitionStrip scan from a point#✓fully proved

Let \(K\) be a linearly ordered field, and write \(d(p, q) = (p_1 - q_1)^2 + (p_2 - q_2)^2\) for the squared distance between points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of \(K^2\). Let \(\delta \in K\), let \(p = (p_1, p_2)\) be a point of \(K^2\) and \(c_1, \dots, c_m\) a list of points \(c_l = (x_l, y_l)\) of \(K^2\), and let \(k \le m\) be largest such that \((y_l - p_2)^2 < \delta\) for all \(1 \le l \le k\). The scan from \(p\) with threshold \(\delta\) returns no value if \(k = 0\) and \(\min_{1 \le l \le k} d(p, c_l)\) otherwise. It is charged one unit of cost per point \(c_1, \dots, c_k\): it stops at the first point whose squared vertical gap to \(p\) is at least \(\delta\), without computing its distance.

def scanFrom (δ : 𝕜) (p : 𝕜 × 𝕜) : List (𝕜 × 𝕜) → TimeM ℕ (Option 𝕜)
  | [] => pure none
  | q :: qs =>
      if (q.2 - p.2) ^ 2 < δ then do
        ✓
        let r ← scanFrom δ p qs
        pure (omin (some (dist2 p q)) r)
      else pure none

Uses 2 · Used by 5

Statement usesSquared distance in the plane · Option minimum

Used byThe closest-pair recursion is correct on lists sorted by first coordinate · Cost of the scan from one strip point · Closest-pair strip scan · The strip scan bounds every pair with a small vertical gap · Cost of the strip scan

DefinitionClosest-pair strip scan#✓fully proved

Let \(K\) be a linearly ordered field, \(\delta \in K\) and \(c_1, \dots, c_n\) a list of points of \(K^2\). For each \(i\), the strip scan runs the strip scan from \(c_i\) with threshold \(\delta\) on the later points \(c_{i+1}, \dots, c_n\). It returns the least of the values these scans return, or no value if none of them returns a value, and its cost is the sum of their costs.

def stripScan (δ : 𝕜) : List (𝕜 × 𝕜) → TimeM ℕ (Option 𝕜)
  | [] => pure none
  | p :: ps => do
      let a ← scanFrom δ p ps
      let b ← stripScan δ ps
      pure (omin a b)

Uses 2 · Used by 5

Statement usesStrip scan from a point · Option minimum

Used byClosest-pair recursion · The closest-pair recursion is correct on lists sorted by first coordinate · Running time of the closest-pair recursion · The strip scan bounds every pair with a small vertical gap · Cost of the strip scan

DefinitionClosest-pair recursion#✓fully proved

Let \(K\) be a linearly ordered field and \(c_1, \dots, c_n\) a list of points \(c_i = (x_i, y_i)\) of \(K^2\). If \(n \le 3\), the recursion returns the brute-force scan of the list. Otherwise let \(m = \lfloor n/2 \rfloor\), and run the recursion on \(c_1, \dots, c_m\) and on \(c_{m+1}, \dots, c_n\). If neither call returns a value, it returns no value. Otherwise let \(\delta\) be the least of the returned values, let \(T\) be the list of the points \(c_i\) with \((x_i - x_m)^2 < \delta\) in their original order, sorted by second coordinate with a stable merge sort, and run the strip scan with threshold \(\delta\) on \(T\). The recursion returns \(\min(\delta, s)\) if the strip scan returns a value \(s\), and \(\delta\) otherwise. In the base case its cost is that of the brute-force scan; otherwise it is the sum of the costs of the two recursive calls and of the strip scan when it is run, and splitting, filtering and sorting are free.

Cslib.Algorithms.Lean.Geometry.closestRec · 19 lines

def closestRec (xs : List (𝕜 × 𝕜)) : TimeM ℕ (Option 𝕜) :=
  if _h : xs.length ≤ 3 then bruteMin xs
  else do
    let L := xs.take (xs.length / 2)
    let R := xs.drop (xs.length / 2)
    let dl ← closestRec L
    let dr ← closestRec R
    match omin dl dr with
    | none => pure none
    | some δ =>
        let xmid := (L.getLast?.map Prod.fst).getD 0
        let strip := xs.filter fun p => (p.1 - xmid) ^ 2 < δ
        let ys := strip.mergeSort fun a b => a.2 ≤ b.2
        let s ← stripScan δ ys
        pure (omin (some δ) s)
termination_by xs.length
decreasing_by
  all_goals simp only [List.length_take, List.length_drop]
  all_goals omega

Uses 3 · Used by 5

Statement usesBrute-force closest pair · Closest-pair strip scan · Option minimum

Used byDivide-and-conquer closest pair · The closest-pair algorithm returns the answer · Running time of the closest-pair algorithm · The closest-pair recursion is correct on lists sorted by first coordinate · Running time of the closest-pair recursion

DefinitionDivide-and-conquer closest pair#✓fully proved

Let \(K\) be a field with a linear order. Given a list of points in \(K^2\), the closest-pair algorithm sorts the points by first coordinate (merge sort, at no cost) and runs the closest-pair recursion on the sorted list. It returns a squared distance or no value, and is charged one unit of cost per squared distance computed.

This is CLRS CLOSEST-PAIR (Section 33.4), with distances compared squared.

def closestPair (ps : List (𝕜 × 𝕜)) : TimeM ℕ (Option 𝕜) :=
  closestRec (ps.mergeSort fun a b => a.1 ≤ b.1)

Uses 1 · Used by 5

Statement usesClosest-pair recursion

Used byDivide and conquer agrees with brute force · The closest-pair algorithm returns no value exactly on fewer than two points · The closest-pair algorithm returns the answer · Correctness of divide-and-conquer closest pair · Running time of the closest-pair algorithm

StructureClosest-pair answer#✓fully proved

Let \(K\) be a linearly ordered field, and write \(d(p, q) = (p_1 - q_1)^2 + (p_2 - q_2)^2\) for the squared distance between points \(p = (p_1, p_2)\) and \(q = (q_1, q_2)\) of \(K^2\). For a list \(c_1, \dots, c_n\) of points of \(K^2\), an optional value \(r\) (an element of \(K\) or no value) is an answer for the list when every value \(\delta\) that \(r\) holds equals \(d(c_i, c_j)\) for some \(i < j\), and when for all \(i < j\), \(r\) holds a value \(\delta\) with \(\delta \le d(c_i, c_j)\).

structure IsAnswer (ps : List (𝕜 × 𝕜)) (r : Option 𝕜) : Prop where
  attained : ∀ δ, r = some δ → ∃ p q, [p, q] <+ ps ∧ dist2 p q = δ
  lower : ∀ p q, [p, q] <+ ps → ∃ δ, r = some δ ∧ δ ≤ dist2 p q

Uses 1 · Used by 6

Statement usesSquared distance in the plane

Used byDivide and conquer agrees with brute force · The closest-pair algorithm returns no value exactly on fewer than two points · The closest-pair algorithm returns the answer · Correctness of divide-and-conquer closest pair · The closest-pair recursion is correct on lists sorted by first coordinate · Running time of the closest-pair recursion

TheoremThe nearest-point scan returns the least squared distance#✓fully proved

Let \(K\) be a linearly ordered field, write \(d(u, v) = (x - x')^2 + (y - y')^2\) for the squared distance between points \(u = (x, y)\) and \(v = (x', y')\) of \(K^2\), let \(p \in K^2\), and let \(qs\) be a list of points in \(K^2\). If the scan for the least squared distance from \(p\) to the entries of \(qs\) returns a value \(\delta\), then \(\delta = d(p, q)\) for some entry \(q\) of \(qs\). For every entry \(q\) of \(qs\), the scan returns a value \(\delta\) with \(\delta \le d(p, q)\).

theorem minDistFrom_spec (p : 𝕜 × 𝕜) (qs : List (𝕜 × 𝕜)) :
    (∀ δ, (minDistFrom p qs).ret = some δ → ∃ q ∈ qs, dist2 p q = δ) ∧
      ∀ q ∈ qs, ∃ δ, (minDistFrom p qs).ret = some δ ∧ δ ≤ dist2 p q

Uses 3 · Used by 2

Statement usesSquared distance in the plane · Least squared distance from a point to a list

Proof usesOption minimum

Used byDivide and conquer agrees with brute force · The closest-pair recursion is correct on lists sorted by first coordinate

TheoremThe strip scan bounds every pair with a small vertical gap#✓fully proved

Let \(K\) be a linearly ordered field, write \(d(p, q) = (x - x')^2 + (y - y')^2\) for the squared distance between points \(p = (x, y)\) and \(q = (x', y')\) of \(K^2\), and let \(\delta \in K\). Let \(ys\) be a list of points in \(K^2\) sorted by second coordinate: whenever an entry precedes another, its second coordinate is at most the other's. If \(a = (a_1, a_2)\) and \(b = (b_1, b_2)\) are entries of \(ys\) at positions \(i < j\) respectively and \((b_2 - a_2)^2 < \delta\), then the strip scan with threshold \(\delta\) on \(ys\) returns a value \(e\) with \(e \le d(a, b)\).

theorem stripScan_lower (δ : 𝕜) (ys : List (𝕜 × 𝕜)) (hs : ys.Pairwise fun a b => a.2 ≤ b.2)
    (a b : 𝕜 × 𝕜) (hab : [a, b] <+ ys) (hgap : (b.2 - a.2) ^ 2 < δ) :
    ∃ d, (stripScan δ ys).ret = some d ∧ d ≤ dist2 a b

Uses 4 · Used by 1

Statement usesSquared distance in the plane · Closest-pair strip scan

Proof usesStrip scan from a point · Option minimum

Used byThe closest-pair recursion is correct on lists sorted by first coordinate

TheoremThe closest-pair recursion is correct on lists sorted by first coordinate#✓fully proved

Let \(K\) be a linearly ordered field, write \(d(u, v) = (x - x')^2 + (y - y')^2\) for the squared distance between points \(u = (x, y)\) and \(v = (x', y')\) of \(K^2\), and let \(xs\) be a list of points in \(K^2\) sorted by first coordinate: whenever an entry precedes another, its first coordinate is at most the other's. If the closest-pair recursion returns a value \(\delta\) on \(xs\), then \(\delta = d(p, q)\) for some entries \(p\), \(q\) of \(xs\) at different positions. For any two entries \(p\), \(q\) of \(xs\) at different positions, the recursion returns a value \(\delta\) with \(\delta \le d(p, q)\).

theorem closestRec_isAnswer (xs : List (𝕜 × 𝕜)) (hs : xs.Pairwise fun a b => a.1 ≤ b.1) :
    IsAnswer xs (closestRec xs).ret

Uses 10 · Used by 2

Statement usesClosest-pair answer · Closest-pair recursion

Proof usesBrute-force closest pair · Squared distance in the plane · Least squared distance from a point to a list · The nearest-point scan returns the least squared distance · Strip scan from a point · Closest-pair strip scan · The strip scan bounds every pair with a small vertical gap · Option minimum

Used byThe closest-pair algorithm returns the answer · Running time of the closest-pair recursion

TheoremThe closest-pair algorithm returns the answer#✓fully proved

Let \(K\) be a linearly ordered field, write \(d(p, q) = (x - x')^2 + (y - y')^2\) for the squared distance between points \(p = (x, y)\) and \(q = (x', y')\) of \(K^2\), and let \(ps\) be a list of points in \(K^2\). If the divide-and-conquer closest-pair algorithm returns a value \(\delta\) on \(ps\), then \(\delta = d(p, q)\) for some entries \(p\), \(q\) of \(ps\) at different positions. For any two entries \(p\), \(q\) of \(ps\) at different positions, the algorithm returns a value \(\delta\) with \(\delta \le d(p, q)\).

theorem closestPair_isAnswer (ps : List (𝕜 × 𝕜)) : IsAnswer ps (closestPair ps).ret

Uses 5 · Used by 3

Statement usesClosest-pair answer · Divide-and-conquer closest pair

Proof usesClosest-pair recursion · The closest-pair recursion is correct on lists sorted by first coordinate · Squared distance in the plane

Used byDivide and conquer agrees with brute force · The closest-pair algorithm returns no value exactly on fewer than two points · Correctness of divide-and-conquer closest pair

TheoremCorrectness of divide-and-conquer closest pair#✓fully proved

Let \(K\) be a linearly ordered field and let \(ps\) be a list of at least two points in \(K^2\). Then the divide-and-conquer closest-pair algorithm returns a value \(\delta\), and \(\delta\) is the least squared distance between two entries of \(ps\) at different positions: some two entries at different positions have squared distance \(\delta\), and any two entries at different positions have squared distance at least \(\delta\).

This is the correctness of CLRS Section 33.4, with distances compared squared.

theorem closestPair_spec (ps : List (𝕜 × 𝕜)) (hps : 2 ≤ ps.length) :
    ∃ δ, (closestPair ps).ret = some δ ∧ IsMinPairDist2 ps δ

Uses 5 · Used by 1

Statement usesLeast pairwise squared distance · Divide-and-conquer closest pair

Proof usesClosest-pair answer · The closest-pair algorithm returns the answer · Squared distance in the plane

Used byThe closest-pair algorithm returns no value exactly on fewer than two points

TheoremThe closest-pair algorithm returns no value exactly on fewer than two points#✓fully proved

Let \(K\) be a linearly ordered field. For every list of points in \(K^2\), the divide-and-conquer closest-pair algorithm returns no value if and only if the list has fewer than two entries.

theorem closestPair_eq_none_iff (ps : List (𝕜 × 𝕜)) :
    (closestPair ps).ret = none ↔ ps.length < 2

Uses 6

Statement usesDivide-and-conquer closest pair

Proof usesClosest-pair answer · Least pairwise squared distance · The closest-pair algorithm returns the answer · Correctness of divide-and-conquer closest pair · Squared distance in the plane

TheoremDivide and conquer agrees with brute force#✓fully proved

Let \(K\) be a linearly ordered field. For every list of points in \(K^2\), the divide-and-conquer closest-pair algorithm returns the same value as the brute-force scan (their costs may differ).

theorem closestPair_eq_bruteMin (ps : List (𝕜 × 𝕜)) :
    (closestPair ps).ret = (bruteMin ps).ret

Uses 8

Statement usesBrute-force closest pair · Divide-and-conquer closest pair

Proof usesClosest-pair answer · The closest-pair algorithm returns the answer · Squared distance in the plane · Least squared distance from a point to a list · The nearest-point scan returns the least squared distance · Option minimum

TheoremCost of the brute-force closest-pair scan#✓fully proved

Let \(K\) be a field with a linear order and let \(ps\) be a list of \(n\) points in \(K^2\). Counting one unit of cost per squared distance computed, twice the cost of the brute-force scan on \(ps\) equals \(n(n-1)\); that is, the scan computes exactly \(n(n-1)/2\) squared distances.

theorem bruteMin_time (ps : List (𝕜 × 𝕜)) :
    2 * (bruteMin ps).time = ps.length * (ps.length - 1)

Uses 4 · Used by 1

Statement usesBrute-force closest pair

Proof usesSquared distance in the plane · Least squared distance from a point to a list · Option minimum

Used byRunning time of the closest-pair recursion

AbbreviationSide-tagged points#✓fully proved

A tagged point is a pair \((p, s)\) of a point \(p \in \mathbb{R}^2\) and a Boolean \(s\), read as the side of the dividing line on which \(p\) lies: false for left, true for right.

abbrev Tagged := (ℝ × ℝ) × Bool

Used by 5

Used byRunning time of the closest-pair recursion · Strip points · Packing bound for the strip · Same-side points far apart · Cost of the strip scan

DefinitionSame-side points far apart#✓fully proved

For a real \(\delta\), two tagged points \(a\) and \(b\) are same-side far apart when, if \(a\) and \(b\) carry the same side, the squared distance between their points is at least \(\delta\).

def SameSideFar (δ : ℝ) (a b : Tagged) : Prop := a.2 = b.2 → δ ≤ dist2 a.1 b.1

Uses 2 · Used by 3

Statement usesSide-tagged points · Squared distance in the plane

Used byRunning time of the closest-pair recursion · Packing bound for the strip · Cost of the strip scan

DefinitionStrip points#✓fully proved

Given reals \(\delta\) and \(x_{\mathrm{mid}}\), a tagged point \(((x, y), s)\) lies in the strip when \((x - x_{\mathrm{mid}})^2 < \delta\), and moreover \(x \le x_{\mathrm{mid}}\) if its side \(s\) is left (\(s\) false) and \(x_{\mathrm{mid}} \le x\) if its side \(s\) is right (\(s\) true).

def InStrip (δ xmid : ℝ) (a : Tagged) : Prop :=
  (a.1.1 - xmid) ^ 2 < δ ∧ (a.2 = false → a.1.1 ≤ xmid) ∧ (a.2 = true → xmid ≤ a.1.1)

Uses 1 · Used by 3

Statement usesSide-tagged points

Used byRunning time of the closest-pair recursion · Packing bound for the strip · Cost of the strip scan

TheoremPacking bound for the strip#✓fully proved

Let \(\delta\) and \(x_{\mathrm{mid}}\) be reals, \(p\) a tagged point, \(Z\) a list of tagged points, and \(L\) the list \(p\) followed by \(Z\); write \(y_a\) for the \(y\)-coordinate of a tagged point \(a\). Suppose every point of \(L\) lies in the strip for \(\delta\) and \(x_{\mathrm{mid}}\), any two points of \(L\) at different positions with the same side are at squared distance at least \(\delta\), and every point \(a\) of \(Z\) satisfies \(y_p \le y_a\) and \((y_a - y_p)^2 < \delta\). Then \(Z\) has at most \(7\) entries.

theorem length_le_seven {δ xmid : ℝ} (p : Tagged) (Z : List Tagged)
    (hpair : (p :: Z).Pairwise (SameSideFar δ))
    (hstrip : ∀ a ∈ p :: Z, InStrip δ xmid a)
    (hy : ∀ a ∈ Z, p.1.2 ≤ a.1.2 ∧ (a.1.2 - p.1.2) ^ 2 < δ) :
    Z.length ≤ 7

Sources

• CLRS, third edition, Section 33.4, the packing argument.

Uses 4 · Used by 1

Statement usesStrip points · Same-side points far apart · Side-tagged points

Proof usesSquared distance in the plane

Used byCost of the strip scan

TheoremCost of the scan from one strip point#✓fully proved

Let \(\delta\) be a real, \(q = (q_1, q_2)\) a point of \(\mathbb{R}^2\) and \(L\) a list of points of \(\mathbb{R}^2\). The cost of the scan from \(q\) over \(L\) with threshold \(\delta\), one unit per squared distance computed, equals the length of the longest initial segment of \(L\) all of whose points \(r = (r_1, r_2)\) satisfy \((r_2 - q_2)^2 < \delta\).

theorem scanFrom_time (δ : ℝ) (q : ℝ × ℝ) (L : List (ℝ × ℝ)) :
    (scanFrom δ q L).time = (L.takeWhile fun r => decide ((r.2 - q.2) ^ 2 < δ)).length

Uses 3 · Used by 1

Statement usesStrip scan from a point

Proof usesSquared distance in the plane · Option minimum

Used byCost of the strip scan

TheoremCost of the strip scan#✓fully proved

Let \(\delta\) and \(x_{\mathrm{mid}}\) be reals and \(Y\) a list of tagged points that is sorted by nondecreasing \(y\)-coordinate, whose points all lie in the strip for \(\delta\) and \(x_{\mathrm{mid}}\), and in which any two points at different positions with the same side are at squared distance at least \(\delta\). Then the strip scan with parameter \(\delta\) over the underlying points of \(Y\) (tags forgotten) computes at most \(7m\) squared distances, where \(m\) is the length of \(Y\).

theorem stripScan_time_le (δ xmid : ℝ) (Y : List Tagged)
    (hsorted : Y.Pairwise fun a b => a.1.2 ≤ b.1.2) (hpair : Y.Pairwise (SameSideFar δ))
    (hstrip : ∀ a ∈ Y, InStrip δ xmid a) :
    (stripScan δ (Y.map Prod.fst)).time ≤ 7 * Y.length

Uses 8 · Used by 1

Statement usesStrip points · Same-side points far apart · Side-tagged points · Closest-pair strip scan

Proof usesPacking bound for the strip · Strip scan from a point · Cost of the scan from one strip point · Option minimum

Used byRunning time of the closest-pair recursion

TheoremRunning time of the closest-pair recursion#✓fully proved

For every list of \(n\) points in \(\mathbb{R}^2\) sorted by nondecreasing \(x\)-coordinate, the divide-and-conquer recursion of the closest-pair algorithm computes at most \(7 n \lceil \log_2 n \rceil + n\) squared distances, where \(\lceil \log_2 0 \rceil\) is read as \(0\).

theorem closestRec_time_le (xs : List (ℝ × ℝ)) (hs : xs.Pairwise fun a b => a.1 ≤ b.1) :
    (closestRec xs).time ≤ 7 * xs.length * Nat.clog 2 xs.length + xs.length

Uses 12 · Used by 1

Statement usesClosest-pair recursion

Proof usesStrip points · Closest-pair answer · Same-side points far apart · Side-tagged points · Brute-force closest pair · Cost of the brute-force closest-pair scan · The closest-pair recursion is correct on lists sorted by first coordinate · Squared distance in the plane · Closest-pair strip scan · Cost of the strip scan · Option minimum

Used byRunning time of the closest-pair algorithm

TheoremRunning time of the closest-pair algorithm#✓fully proved

For every list of \(n\) points in \(\mathbb{R}^2\), the closest-pair algorithm computes at most \(7 n \lceil \log_2 n \rceil + n\) squared distances, where \(\lceil \log_2 0 \rceil\) is read as \(0\). In particular it computes \(O(n \log n)\) distances.

theorem closestPair_time_le (ps : List (ℝ × ℝ)) :
    (closestPair ps).time ≤ 7 * ps.length * Nat.clog 2 ps.length + ps.length

Sources

• CLRS, third edition, Section 33.4.

Uses 3

Statement usesDivide-and-conquer closest pair

Proof usesClosest-pair recursion · Running time of the closest-pair recursion

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.