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 w : Fin N → ℝ) : have R₀ := 5 * max (dist v 0) (dist w 0); ∀ (i : Fin N), v i ∈ Set.Icc (-R₀) R₀