Time complexity of the Analyst’s Traveling Salesman algorithm

ANTHONY RAMIREZ and VYRON VELLIS

We prove for any N the n = 2 version of the statement on page 3 containing the phrase "it is clear that".

theorem clear {N : ℕ} (v : Fin N → ℝ) (w : Fin N → ℝ) : let R₀ := 5 * max (dist v 0) (dist w 0); ∀ (i : Fin N), v i ∈ Set.Icc (-R₀) R₀

theorem nat_to_int_eq (a : ℕ) (b : ℕ) : a = b → ↑a = ↑b

theorem flip_neg (a : ℤ) (b : ℤ) : a = -b ↔ -a = b

def neg_fit_part (z : ℤ) : ℕ

Equations

• neg_fit_part 0 = 0
• neg_fit_part 1 = 0
• neg_fit_part (-1) = 1
• neg_fit_part z = 2

def neg_fit (z : ℤ) : ℕ

Equations

• neg_fit z = neg_fit_part z.sign

theorem neg_fit_eq_zero_or_one (z : ℤ) : neg_fit z = 0 ∨ neg_fit z = 1

theorem sign_nonneg_iff_natAbs_eq (z : ℤ) : ↑z.natAbs = z ↔ z.sign = 0 ∨ z.sign = 1

theorem neg_fit_iff_pos (z : ℤ) : ↑z.natAbs = z ↔ neg_fit z = 0

def spread_fun (z : ℤ) : ℕ

Equations

• spread_fun z = 2 * z.natAbs + neg_fit z

theorem spread_fun_inj : Function.Injective spread_fun

theorem spread_fun_inj_explicit (a : ℤ) (b : ℤ) : spread_fun a = spread_fun b → a = b

theorem int_countable (B : Set ℤ) : B.Countable

theorem infant_Gauss (n : ℕ) : 2 * ∑ x ∈ Finset.range (n + 1), x = n * (n + 1)

def diag_fun (a : ℕ × ℕ) : ℕ

Equations

• diag_fun a = ∑ x ∈ Finset.range (a.1 + a.2 + 1), x + a.2

theorem mul_2_both_sides (a : ℕ) (b : ℕ) : a = b → 2 * a = 2 * b

theorem n_sq_add_n_monotone (m : ℕ) (n : ℕ) : m ≤ n ↔ m * (m + 1) ≤ n * (n + 1)

theorem n_sq_add_n_monotone_strict (m : ℕ) (n : ℕ) : m < n ↔ m * (m + 1) < n * (n + 1)

theorem pred_legit (c : ℕ) : c > 0 → ∃ (a : ℕ), c = a + 1

theorem range_lem (b : ℕ) (c : ℕ) : c * (c + 1) < b * (b + 1) + 2 * c → c ≤ b

theorem sum_range (a : ℕ) (c : ℕ) : a * (a + 1) ≤ 2 * ∑ x ∈ Finset.range (c + 1), x ∧ 2 * ∑ x ∈ Finset.range (c + 1), x < a * (a + 1) + 2 * c → a = c

theorem sum_range_simp (a : ℕ) (c : ℕ) : a ≤ c ∧ c * (c + 1) < a * (a + 1) + 2 * c → a = c

theorem lemma1 (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) : a + b = c + d ∧ a ≤ c → b ≥ d

theorem lemma2 (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) : a + b = c + d ∧ a ≥ c → b ≤ d

theorem lemma2_le (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) : a + b ≤ c + d ∧ a ≥ c → b ≤ d

theorem lt_if_lt_add_right (a : ℕ) (b : ℕ) (c : ℕ) : a + c < b + c → a < b

theorem diag_fun_inj : Function.Injective diag_fun

theorem nat_prod_countable (C : Set (ℕ × ℕ)) : C.Countable

theorem diag_fun_inj_explicit (a : ℕ × ℕ) (b : ℕ × ℕ) : diag_fun a = diag_fun b → a = b

theorem proj_fst (a : ℕ × ℕ) (b : ℕ × ℕ) : a = b → a.1 = b.1

theorem proj_snd (a : ℕ × ℕ) (b : ℕ × ℕ) : a = b → a.2 = b.2

def diag3_fun (a : ℕ × ℕ × ℕ) : ℕ

Equations

• diag3_fun a = diag_fun (diag_fun (a.2.1, a.2.2), a.1)

theorem diag3_fun_inj : Function.Injective diag3_fun

theorem nat_trip_prod_countable (D : Set (ℕ × ℕ × ℕ)) : D.Countable

def rat_fun (q : ℚ) : ℕ

Equations

• rat_fun q = diag_fun (spread_fun q.num, q.den)

theorem rat_fun_inj : Function.Injective rat_fun

theorem rat_fun_inj_explicit (a : ℚ) (b : ℚ) : rat_fun a = rat_fun b → a = b

theorem rat_countable (A : Set ℚ) : A.Countable

def rat_prod_fun (s : ℚ × ℚ) : ℕ

Equations

• rat_prod_fun s = diag_fun (rat_fun s.1, rat_fun s.2)

theorem rat_prod_fun_inj : Function.Injective rat_prod_fun

theorem rat_prod_countable (E : Set (ℚ × ℚ)) : E.Countable