Time complexity of the Analyst’s Traveling Salesman algorithm

by ANTHONY RAMIREZ 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₀