@[reducible, inline]

abbrev RheeTalagrand.Point : Type

A point in the plane $\mathbb{R}^2$, represented as a function $\mathrm{Fin}\,2 \to \mathbb{R}$.

def RheeTalagrand.unitSquare : Set Point

The unit square $[0,1]^2 \subseteq \mathbb{R}^2$.

noncomputable def RheeTalagrand.tspTourLength (n : ℕ) (points : Fin n → Point) : ℝ

The TSP tour length $L_n$: the infimum over permutations $σ$ of $\mathrm{Fin}\,n$ of $\sum_i \mathrm{dist}(\mathit{points}_{σ(i)}, \mathit{points}_{σ(i+1 \bmod n)})$. Returns $0$ when $n = 0$.

def RheeTalagrand.IsIIDUniformUnitSquare (n : ℕ) (μ : MeasureTheory.Measure (Fin n → Point)) : Prop

The measure $μ$ on $(\mathbb{R}^2)^n$ corresponds to $n$ i.i.d.\ uniformly random points in the unit square.

noncomputable def RheeTalagrand.tspTourLengthOnUnitSquare (n : ℕ) (x : Fin n → ↑unitSquare) : ℝ

TSP tour length specialized to points in the unit square, viewed as a function of the subtype-valued configuration $x : \mathrm{Fin}\,n \to \mathit{unitSquare}$.

theorem RheeTalagrand.tsp_has_weighted_certificates : ∃ (K : ℝ), 0 < K ∧ ∀ (n : ℕ), 1 ≤ n → TalagrandWeightedCertificates.HasWeightedCertificates (tspTourLengthOnUnitSquare n) K

Lemma 9.6.11: the TSP tour length on the unit square admits weighted certificates with a uniform constant $K > 0$, allowing Talagrand's weighted certificates inequality to be applied to $L_n$.

theorem RheeTalagrand.rhee_talagrand_1989 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (μ : MeasureTheory.Measure (Fin n → Point)), IsIIDUniformUnitSquare n μ → MeasureTheory.IsProbabilityMeasure μ → ∀ (t : ℝ), 0 < t → μ {x : Fin n → Point | t ≤ |tspTourLength n x - ∫ (y : Fin n → Point), tspTourLength n y ∂μ|} ≤ ENNReal.ofReal (Real.exp (-c * t ^ 2))

Theorem 9.6.3 (Rhee–Talagrand 1989): for $n$ i.i.d.\ uniform points in the unit square, the TSP tour length $L_n$ is $O(1)$-sub-Gaussian about its mean, i.e.\ there exists $c > 0$ such that for all $t > 0$, $\mu(\{x : |L_n(x) - \mathbb{E} L_n| \geq t\}) \leq e^{-c t^2}$.