The Euclidean growth inequality (instantiating the any-norm mod-2 theorem)

Instantiating SimApprox.growth_additive_modTwo at the Euclidean (L²) norm gives the growth inequality for best simultaneous approximations in the Euclidean norm:

q_{n + 2^{d+1}} ≥ 2 q_{n+1} + q_n.

For d = 2 this is q_{n+8} ≥ 2 q_{n+1} + q_n, the denominator-growth input behind the Euclidean five-distance theorem on 𝕋². The Euclidean norm on Fin d → ℝ is obtained by transporting the EuclideanSpace ℝ (Fin d) norm along EuclideanSpace.equiv; its triangle inequality and homogeneity come for free from that being a (continuous) linear equivalence.

Axiom-clean.

noncomputable def ThreeGap.SimApprox.euclNorm (d : ℕ) (x : Fin d → ℝ) : ℝ

The Euclidean (L²) norm on Fin d → ℝ, transported from EuclideanSpace ℝ (Fin d) along EuclideanSpace.equiv. Concretely euclNorm x = √(∑ i, (x i)²).

Equations

• ThreeGap.SimApprox.euclNorm d x = ‖(EuclideanSpace.equiv (Fin d) ℝ).symm x‖

theorem ThreeGap.SimApprox.euclNorm_nonneg {d : ℕ} (x : Fin d → ℝ) : 0 ≤ euclNorm d x

theorem ThreeGap.SimApprox.euclNorm_tri {d : ℕ} (x y : Fin d → ℝ) : euclNorm d (x + y) ≤ euclNorm d x + euclNorm d y

theorem ThreeGap.SimApprox.euclNorm_smul {d : ℕ} (c : ℝ) (x : Fin d → ℝ) : euclNorm d (c • x) = |c| * euclNorm d x

theorem ThreeGap.SimApprox.euclidean_growth_additive {d : ℕ} (α : Fin d → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin d → ℤ) (hmono : StrictMono q) (hattain : ∀ (k : ℕ), euclNorm d (rem α (q k) (p k)) ≤ deltaN (euclNorm d) α (q k)) (hdec : ∀ (k : ℕ), deltaN (euclNorm d) α (q (k + 1)) < deltaN (euclNorm d) α (q k)) (hbest : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q (k + 1) → deltaN (euclNorm d) α (q k) ≤ deltaN (euclNorm d) α m) (n : ℕ) : 2 * q (n + 1) + q n ≤ q (n + 2 ^ (d + 1))

The Euclidean growth inequality (the mod-2 theorem at N = euclNorm). With the Euclidean defect δ = deltaN (euclNorm d) α and the best-approximation record structure, the denominators satisfy 2 q_{n+1} + q_n ≤ q_{n + 2^{d+1}}. For d = 2: q_{n+8} ≥ 2 q_{n+1} + q_n.