def TSPHelper.unitSquare : Set (EuclideanSpace ℝ (Fin 2))

The unit square $[0,1]^2 \subseteq \mathbb{R}^2$ as a subset of Euclidean space.

noncomputable def TSPHelper.uniformOnSquare : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))

The uniform probability measure on the unit square, obtained by restricting Lebesgue measure on $\mathbb{R}^2$ to $[0,1]^2$.

noncomputable def TSPHelper.iidUniformOnSquare (k : ℕ) : MeasureTheory.Measure (Fin k → EuclideanSpace ℝ (Fin 2))

The product measure on $(\mathbb{R}^2)^k$ corresponding to $k$ i.i.d.\ uniform points in the unit square.

theorem TSPHelper.volume_unitSquare : MeasureTheory.volume unitSquare = 1

The Lebesgue volume of the unit square $[0,1]^2$ is $1$.

instance TSPHelper.uniformOnSquare_isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure uniformOnSquare

The uniform measure on the unit square is a probability measure.

instance TSPHelper.iidUniformOnSquare_isProbabilityMeasure (k : ℕ) : MeasureTheory.IsProbabilityMeasure (iidUniformOnSquare k)

The product measure of $k$ i.i.d.\ uniform points in the unit square is a probability measure.

theorem TSPHelper.tail_bound_infDist (k : ℕ) (hk : 0 < k) (y : EuclideanSpace ℝ (Fin 2)) (hy : y ∈ unitSquare) (t : ℝ) (ht : 0 < t) : (iidUniformOnSquare k).real {S : Fin k → EuclideanSpace ℝ (Fin 2) | t < Metric.infDist y (Set.range S)} ≤ Real.exp (-(1 / 4 * ↑k) * t ^ 2)

Tail bound for the distance from a fixed $y \in [0,1]^2$ to a uniform sample of $k$ points: for $t > 0$, the probability that $\operatorname{dist}(y, S) > t$ is at most $e^{-(k/4) t^2}$.

theorem TSPHelper.infDist_integrable (k : ℕ) (hk : 0 < k) (y : EuclideanSpace ℝ (Fin 2)) (hy : y ∈ unitSquare) : MeasureTheory.Integrable (fun (S : Fin k → EuclideanSpace ℝ (Fin 2)) => Metric.infDist y (Set.range S)) (iidUniformOnSquare k)

The map $S \mapsto \operatorname{dist}(y, S)$ is integrable with respect to the uniform i.i.d.\ measure on $k$-tuples of points in the unit square.

theorem TSPHelper.tail_integrableOn (k : ℕ) (hk : 0 < k) (y : EuclideanSpace ℝ (Fin 2)) (hy : y ∈ unitSquare) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (iidUniformOnSquare k).real {a : Fin k → EuclideanSpace ℝ (Fin 2) | t < Metric.infDist y (Set.range a)}) (Set.Ioi 0) MeasureTheory.volume

The tail function $t \mapsto \mathbb{P}(\operatorname{dist}(y, S) > t)$ is integrable on $(0, \infty)$, which justifies the layer-cake representation of $\mathbb{E}[\operatorname{dist}(y, S)]$.

theorem TSPHelper.expected_infDist_le_div_sqrt : ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℕ), 0 < k → ∀ y ∈ unitSquare, ∫ (S : Fin k → EuclideanSpace ℝ (Fin 2)), Metric.infDist y (Set.range S) ∂iidUniformOnSquare k ≤ C / √↑k

Lemma 9.6.2: there is a constant $C > 0$ such that for all $k \geq 1$ and any $y \in [0,1]^2$, the expected distance from $y$ to a uniform sample of $k$ i.i.d.\ points in the unit square satisfies $\mathbb{E}[\operatorname{dist}(y, S)] \leq C / \sqrt{k}$.