@[reducible, inline]

abbrev TSPConcentration.Point : Type

A point in the Euclidean plane $\mathbb{R}^2$.

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

The length $L_n$ of the optimal Travelling Salesman tour through the $n$ points $\mathit{points}_0, \dots, \mathit{points}_{n-1}$: the infimum over permutations $σ$ of the total cyclic distance $\sum_i \mathrm{dist}(\mathit{points}_{σ(i)}, \mathit{points}_{σ(i+1 \bmod n)})$. Returns $0$ when $n = 0$.

def TSPConcentration.IsSubGaussianAboutMean {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (K : ℝ) (μ : MeasureTheory.Measure Ω) : Prop

The random variable $X$ is $K$-sub-Gaussian about its mean under $μ$: for every $t \geq 0$, $μ(\{ω : |X(ω) - \mathbb{E}_μ X| \geq t\}) \leq 2 e^{-t^2 / K^2}$.

theorem TSPConcentration.sum_inv_sub_le_log (n : ℕ) : ∑ i ∈ Finset.range n, 1 / ↑(n - i) ≤ 1 + Real.log ↑n

Harmonic-sum bound: $\sum_{i=0}^{n-1} \frac{1}{n - i} = H_n \leq 1 + \log n$.

theorem TSPConcentration.azuma_variance_bound (n : ℕ) (C : ℝ) : ∑ i ∈ Finset.range n, (C / √↑(n - i)) ^ 2 ≤ C ^ 2 * (1 + Real.log ↑n)

The Azuma variance sum for the TSP martingale differences is bounded by $C^2 (1 + \log n)$: $\sum_{i=0}^{n-1} \bigl(C / \sqrt{n - i}\bigr)^2 \leq C^2 (1 + \log n)$.

theorem TSPConcentration.rhee_talagrand_tsp_concentration {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (hn : 2 ≤ n) (L : Ω → ℝ) (C : ℝ) (hC : 0 < C) (hAzuma : ∀ (t : ℝ), 0 ≤ t → μ {ω : Ω | t ≤ |L ω - ∫ (ω' : Ω), L ω' ∂μ|} ≤ ENNReal.ofReal (2 * Real.exp (-(t ^ 2 / (2 * ∑ i ∈ Finset.range n, (C / √↑(n - i)) ^ 2))))) : IsSubGaussianAboutMean L (√(2 * C ^ 2 * (1 + Real.log ↑n))) μ

Theorem 9.6.1 (Rhee–Talagrand 1987): given an Azuma-type bound on the deviations of $L$ with martingale-difference variance summing to $2 \sum_i (C / \sqrt{n-i})^2$, the TSP tour length $L$ is $\sqrt{2 C^2 (1 + \log n)}$-sub-Gaussian about its mean, hence $O(\sqrt{\log n})$-sub-Gaussian.