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

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

def SpaceFillingCurve.cyclicSucc {n : ℕ} (i : Fin n) : Fin n

Cyclic successor on Fin n: $i \mapsto (i + 1) \bmod n$.

theorem SpaceFillingCurve.hilbertCurve_dyadic_property : ∃ (H : ↑(Set.Icc 0 1) → EuclideanSpace ℝ (Fin 2)), ∃ C_diad > 0, (∀ p ∈ unitSquare, ∃ (t : ↑(Set.Icc 0 1)), H t = p) ∧ ∀ (x y : ↑(Set.Icc 0 1)) (n : ℕ), dist ↑x ↑y ≤ 2 * 4⁻¹ ^ n → dist (H x) (H y) ≤ C_diad * 2⁻¹ ^ n

Existence of a Hilbert-curve-like surjection from $[0,1]$ to the unit square with the dyadic distance bound $\mathrm{dist}(x, y) \le 2 \cdot 4^{-n} \Rightarrow \mathrm{dist}(H(x), H(y)) \le C \cdot 2^{-n}$.

noncomputable def SpaceFillingCurve.hilbertCurve : ↑(Set.Icc 0 1) → EuclideanSpace ℝ (Fin 2)

The Hilbert curve $H : [0,1] \to [0,1]^2$ extracted from hilbertCurve_dyadic_property.

noncomputable def SpaceFillingCurve.C_diad : ℝ

The dyadic constant $C$ extracted from hilbertCurve_dyadic_property.

theorem SpaceFillingCurve.C_diad_pos : C_diad > 0

The dyadic constant $C$ is strictly positive.

theorem SpaceFillingCurve.hilbertCurve_surjective (p : EuclideanSpace ℝ (Fin 2)) : p ∈ unitSquare → ∃ (t : ↑(Set.Icc 0 1)), hilbertCurve t = p

The Hilbert curve is surjective onto the unit square.

theorem SpaceFillingCurve.hilbertCurve_dyadic_bound (x y : ↑(Set.Icc 0 1)) (n : ℕ) (h : dist ↑x ↑y ≤ 2 * 4⁻¹ ^ n) : dist (hilbertCurve x) (hilbertCurve y) ≤ C_diad * 2⁻¹ ^ n

Dyadic bound for the Hilbert curve: if $|x - y| \le 2 \cdot 4^{-n}$, then $\mathrm{dist}(H(x), H(y)) \le C \cdot 2^{-n}$.

theorem SpaceFillingCurve.holderWith_of_dist_bound {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (C r : NNReal) (f : X → Y) (h : ∀ (x y : X), dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r) : HolderWith C r f

A distance bound $\mathrm{dist}(f(x), f(y)) \le C \cdot \mathrm{dist}(x, y)^r$ on a pseudometric space upgrades to the mathlib HolderWith predicate.

theorem SpaceFillingCurve.hilbertCurve_dist_holder (x y : ↑(Set.Icc 0 1)) : dist (hilbertCurve x) (hilbertCurve y) ≤ 2 * C_diad * dist ↑x ↑y ^ (1 / 2)

Hölder-$1/2$ distance bound for the Hilbert curve: $\mathrm{dist}(H(x), H(y)) \le 2 C \cdot |x - y|^{1/2}$.

theorem SpaceFillingCurve.hilbert_curve_holder_half : ∃ (C : NNReal), HolderWith C 2⁻¹ hilbertCurve

Theorem 9.6.7 (Hilbert curve is Hölder-$1/2$). The Hilbert curve $H : [0,1] \to [0,1]^2$ is Hölder continuous of exponent $1/2$.

theorem SpaceFillingCurve.hilbert_curve_exists : ∃ (H : ↑(Set.Icc 0 1) → EuclideanSpace ℝ (Fin 2)) (C : NNReal), (∀ p ∈ unitSquare, ∃ (t : ↑(Set.Icc 0 1)), H t = p) ∧ HolderWith C 2⁻¹ H

Existence of a Hilbert-curve-like map: a surjection from $[0,1]$ onto the unit square that is Hölder continuous of exponent $1/2$.

theorem SpaceFillingCurve.holder_half_sq_bound {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {C : NNReal} {f : X → Y} (hf : HolderWith C 2⁻¹ f) (x y : X) : dist (f x) (f y) ^ 2 ≤ ↑C ^ 2 * dist x y

Squaring the Hölder-$1/2$ bound: $\mathrm{dist}(f(x), f(y))^2 \le C^2 \mathrm{dist}(x, y)$.

theorem SpaceFillingCurve.fin_telescoping_sum (m : ℕ) (f : Fin (m + 1) → ℝ) : ∑ i : Fin m, (f ⟨↑i + 1, ⋯⟩ - f ⟨↑i, ⋯⟩) = f ⟨m, ⋯⟩ - f ⟨0, ⋯⟩

Telescoping sum over Fin m: $\sum_{i=0}^{m-1} (f(i+1) - f(i)) = f(m) - f(0)$.

theorem SpaceFillingCurve.monotone_cyclic_sum_le_two {n : ℕ} (f : Fin n → ℝ) (hf_mono : Monotone f) (hf_lo : ∀ (i : Fin n), 0 ≤ f i) (hf_hi : ∀ (i : Fin n), f i ≤ 1) : ∑ i : Fin n, |f i - f ⟨(↑i + 1) % n, ⋯⟩| ≤ 2

For a monotone sequence valued in $[0,1]$, the total cyclic variation $\sum_i |f(i) - f(i+1 \bmod n)|$ is at most $2$.

theorem SpaceFillingCurve.space_filling_curve_heuristic : ∃ (C : ℝ), ∀ (n : ℕ) (x : Fin n → EuclideanSpace ℝ (Fin 2)), (∀ (i : Fin n), x i ∈ unitSquare) → ∃ (σ : Equiv.Perm (Fin n)), ∑ i : Fin n, ‖x (σ i) - x (σ (cyclicSucc i))‖ ^ 2 ≤ C

Lemma 9.6.9 (space-filling curve heuristic for TSP). There exists an absolute constant $C$ such that for any $n$ points in the unit square one can find a Hamilton cycle (i.e. a permutation $\sigma$) with $\sum_{i=1}^{n} \| x_{\sigma(i)} - x_{\sigma(i+1)} \|^2 \le C$.