@[reducible, inline]

abbrev EuclideanTSP.E2 : Type

The two-dimensional Euclidean plane $\mathbb{R}^2$, the ambient space for the Euclidean travelling salesman problem.

noncomputable def EuclideanTSP.tourLength {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : ℝ

Length of the cyclic tour visiting the points $x$ in the order given by the permutation $\sigma$: the sum of distances between consecutive points (mod $n$).

noncomputable def EuclideanTSP.shortestTour {n : ℕ} [NeZero n] (x : Fin n → E2) : ℝ

Length of the shortest tour through the points $x$: the infimum of tourLength x σ over all permutations $\sigma$.

def EuclideanTSP.InUnitSquare (p : E2) : Prop

A point $p \in \mathbb{R}^2$ lies in the unit square $[0,1]^2$.

def EuclideanTSP.AllInUnitSquare {n : ℕ} (x : Fin n → E2) : Prop

All points of the configuration $x$ lie in the unit square $[0,1]^2$.

noncomputable def EuclideanTSP.cert {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) (i : Fin n) : ℝ

Certificate weights $\alpha_i$ in the Rhee–Talagrand TSP concentration argument: twice the sum of the distances from $x_i$ to its successor and predecessor in the tour $\sigma$.

theorem EuclideanTSP.tourLength_nonneg {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : 0 ≤ tourLength x σ

The length of any tour is non-negative, as a sum of non-negative distances.

theorem EuclideanTSP.shortestTour_le_tourLength {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : shortestTour x ≤ tourLength x σ

The shortest tour length is at most the length of any specific tour.

theorem EuclideanTSP.shortestTour_nonneg {n : ℕ} [NeZero n] (x : Fin n → E2) : 0 ≤ shortestTour x

The length of the shortest tour is non-negative.

theorem EuclideanTSP.cert_nonneg {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) (i : Fin n) : 0 ≤ cert x σ i

Each certificate weight $\alpha_i = $ cert x σ i is non-negative.

theorem EuclideanTSP.sum_dist_succ_eq_tourLength {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : ∑ i : Fin n, dist (x i) (x (σ ((Equiv.symm σ) i + 1))) = tourLength x σ

Summing $\mathrm{dist}(x_i, x_{\sigma(\sigma^{-1}(i)+1)})$ over all $i$ recovers the tour length, by reindexing through $\sigma^{-1}$.

theorem EuclideanTSP.sum_dist_pred_eq_tourLength {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : ∑ i : Fin n, dist (x i) (x (σ ((Equiv.symm σ) i - 1))) = tourLength x σ

Analogous to sum_dist_succ_eq_tourLength: the sum of distances from each $x_i$ to its predecessor in the tour also recovers the tour length.

theorem EuclideanTSP.sum_cert_eq_four_mul_tourLength {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : ∑ i : Fin n, cert x σ i = 4 * tourLength x σ

The total certificate weight equals four times the tour length.

theorem EuclideanTSP.tourLength_le_sum_cert {n : ℕ} [NeZero n] (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) : tourLength x σ ≤ ∑ i : Fin n, cert x σ i

The tour length is bounded above by the sum of certificate weights (which equals four times the tour length).

theorem EuclideanTSP.cyclicSucc_eq_add_one {m : ℕ} [NeZero m] (i : Fin m) : SpaceFillingCurve.cyclicSucc i = i + 1

The cyclic successor in Fin m agrees with adding one (mod $m$).

theorem EuclideanTSP.space_filling_curve_heuristic : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ℕ) [inst : NeZero m] (x : Fin m → E2), AllInUnitSquare x → ∃ (σ : Equiv.Perm (Fin m)), ∑ i : Fin m, dist (x (σ i)) (x (σ (i + 1))) ^ 2 ≤ C

Space-filling curve heuristic. There is a universal constant $C$ such that for any point set in $[0,1]^2$ one can find a tour whose squared-edge-lengths sum to at most $C$.

theorem EuclideanTSP.tourLength_excursion_bound {n : ℕ} [NeZero n] (x y : Fin n → E2) (σ : Equiv.Perm (Fin n)) (hne : {i : Fin n | x i ≠ y i} ≠ Finset.univ) : shortestTour x ≤ shortestTour y + ∑ i : Fin n with x i ≠ y i, cert x σ i

Excursion bound: if $x$ and $y$ agree on some coordinate, then the shortest tour of $x$ exceeds that of $y$ by at most the total certificate weight on the disagreement set.

theorem EuclideanTSP.shortestTour_le_shortestTour_add_cert {n : ℕ} [NeZero n] (x y : Fin n → E2) (σ : Equiv.Perm (Fin n)) : shortestTour x ≤ shortestTour y + ∑ i : Fin n with x i ≠ y i, cert x σ i

Unconditional form of the excursion bound: dropping the hypothesis that $x$ and $y$ share a coordinate by using $\sum \alpha_i \ge T(x)$ when they disagree everywhere.

theorem EuclideanTSP.sum_sq_cert_le {n : ℕ} [NeZero n] {C : ℝ} (x : Fin n → E2) (σ : Equiv.Perm (Fin n)) (hσ : ∑ i : Fin n, dist (x (σ i)) (x (σ (i + 1))) ^ 2 ≤ C) : ∑ i : Fin n, cert x σ i ^ 2 ≤ 16 * C

Sum-of-squares control on the certificate weights: if a tour $\sigma$ has bounded squared-edge sum $\le C$, then $\sum_i \alpha_i^2 \le 16 C$.

theorem EuclideanTSP.shortestTour_certificate_exists : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ℕ) [inst : NeZero m] (x : Fin m → E2), AllInUnitSquare x → ∃ (α : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ α i) ∧ (∀ (y : Fin m → E2), AllInUnitSquare y → shortestTour x ≤ shortestTour y + ∑ i : Fin m with x i ≠ y i, α i) ∧ ∑ i : Fin m, α i ^ 2 ≤ C

Theorem 9.6.1 / 9.6.3 (Rhee–Talagrand TSP concentration, certificate form). For every configuration $x$ in the unit square, there exist non-negative weights $\alpha_i$ such that the shortest tour is 1-Lipschitz with respect to changes on a subset of indices bounded by $\sum_{i : x_i \ne y_i} \alpha_i$, and the weights satisfy $\sum_i \alpha_i^2 \le C$ for a universal constant $C$.