Simultaneous Diophantine approximation: the remainder-vector difference inequality

The separation lemma behind the higher-dimensional growth inequality (Lagarias 1980, Ermakov arXiv:1002.2713) splits into an elementary algebraic core and a convex-geometry completion. This file formalizes the algebraic core, faithfully.

For α : Fin n → ℝ and an integer q, the approximation defect is

δ_q = inf over p ∈ ℤⁿ of ‖q • α − p‖,

with r(q) = q • α − p(q) the remainder vector (‖r(q)‖ = δ_q). The crucial elementary fact, used throughout Ermakov's Lemma 2 ("r(qᵢ) − r(qⱼ) is the remainder vector for qᵢ − qⱼ"): the difference of two remainder vectors is itself an approximation remainder for the difference of the denominators, hence its norm is ≥ δ_{qᵢ − qⱼ}:

‖r(qᵢ) − r(qⱼ)‖ ≥ δ_{qᵢ − qⱼ}.

This is delta_diff_le. It is the algebraic input that makes the remainder vectors spread out; the remaining geometric step (their direction angles exceed π/3, so at most K = contact-number many fit) is Ermakov's Lemmas 1–2, the cited geometric completion. Norm-agnostic: holds for every norm (here the sup norm on Fin n → ℝ).

Axiom-clean; elementary.

noncomputable def ThreeGap.SimApprox.rem {n : ℕ} (α : Fin n → ℝ) (q : ℤ) (p : Fin n → ℤ) : Fin n → ℝ

The integer-vector translate of q • α by p, as an element of Fin n → ℝ. Its norm over all p ∈ ℤⁿ is minimised at the best approximation; here we only need the value and its lower bound.

Equations

• ThreeGap.SimApprox.rem α q p = ↑q • α - fun (k : Fin n) => ↑(p k)

noncomputable def ThreeGap.SimApprox.delta {n : ℕ} (α : Fin n → ℝ) (q : ℤ) : ℝ

The approximation defect δ_q = inf_{p ∈ ℤⁿ} ‖q • α − p‖.

Equations

• ThreeGap.SimApprox.delta α q = ⨅ (p : Fin n → ℤ), ‖ThreeGap.SimApprox.rem α q p‖

noncomputable def ThreeGap.SimApprox.deltaN {n : ℕ} (N : (Fin n → ℝ) → ℝ) (α : Fin n → ℝ) (q : ℤ) : ℝ

The approximation defect for an arbitrary norm N: δ^N_q = inf_{p ∈ ℤⁿ} N (q • α − p). (delta is the N = ‖·‖ sup-norm case.)

Equations

• ThreeGap.SimApprox.deltaN N α q = ⨅ (p : Fin n → ℤ), N (ThreeGap.SimApprox.rem α q p)

theorem ThreeGap.SimApprox.deltaN_le {n : ℕ} (N : (Fin n → ℝ) → ℝ) (hN : ∀ (x : Fin n → ℝ), 0 ≤ N x) (α : Fin n → ℝ) (q : ℤ) (p : Fin n → ℤ) : deltaN N α q ≤ N (rem α q p)

For a nonnegative N, the defect δ^N_q is a lower bound on every concrete approximation.

theorem ThreeGap.SimApprox.bddBelow_rem {n : ℕ} (α : Fin n → ℝ) (q : ℤ) : BddBelow (Set.range fun (p : Fin n → ℤ) => ‖rem α q p‖)

The range of p ↦ ‖rem α q p‖ is bounded below (by 0), so the infimum is genuine.

theorem ThreeGap.SimApprox.delta_le {n : ℕ} (α : Fin n → ℝ) (q : ℤ) (p : Fin n → ℤ) : delta α q ≤ ‖rem α q p‖

δ_q is a lower bound for every concrete approximation: δ_q ≤ ‖q • α − p‖ for all p ∈ ℤⁿ.

theorem ThreeGap.SimApprox.delta_nonneg {n : ℕ} (α : Fin n → ℝ) (q : ℤ) : 0 ≤ delta α q

δ_q ≥ 0.

theorem ThreeGap.SimApprox.rem_sub {n : ℕ} (α : Fin n → ℝ) (qi qj : ℤ) (pi pj : Fin n → ℤ) : rem α qi pi - rem α qj pj = rem α (qi - qj) (pi - pj)

The remainder-vector difference is an approximation remainder for the difference of denominators. Algebraically, (qᵢ • α − pᵢ) − (qⱼ • α − pⱼ) = (qᵢ − qⱼ) • α − (pᵢ − pⱼ).

theorem ThreeGap.SimApprox.rem_two_smul {n : ℕ} (α : Fin n → ℝ) (q : ℤ) (p : Fin n → ℤ) : (rem α (2 * q) fun (k : Fin n) => 2 * p k) = 2 • rem α q p

Halving homogeneity. r(2q, 2p) = 2 · r(q, p) — doubling both the denominator and the integer translate doubles the remainder vector. Used in the mod-2 pigeonhole growth argument, where two best approximations agreeing mod 2 produce a half-integer combination.

theorem ThreeGap.SimApprox.delta_diff_le {n : ℕ} (α : Fin n → ℝ) (qi qj : ℤ) (pi pj : Fin n → ℤ) : delta α (qi - qj) ≤ ‖rem α qi pi - rem α qj pj‖

The separation core (Ermakov Lemma 2, algebraic part). The distance between two remainder vectors is at least the approximation defect of the difference of their denominators:

δ_{qᵢ − qⱼ} ≤ ‖r(qᵢ) − r(qⱼ)‖.

Combined with the best-approximation property (every nonzero denominator below qₖ₊₁ has defect ≥ δ_{qₖ}), this makes the remainder vectors r(qₖ), …, r(qₖ₊ₖ) pairwise ≥ δ_{qₖ} apart — the input to the convex-geometry/contact-number count that yields the growth inequality.

theorem ThreeGap.SimApprox.window_separation {n : ℕ} (α : Fin n → ℝ) (q : ℕ → ℤ) (p : ℕ → Fin n → ℤ) (hmono : StrictMono q) (hbest : ∀ (k : ℕ) (m : ℤ), 0 < m → m < q (k + 1) → delta α (q k) ≤ delta α m) {K k i j : ℕ} (hk : k ≤ j) (hj : j < i) (hi : i ≤ k + K) (hwin : q (k + K) < q (k + 1) + q k) : delta α (q k) ≤ ‖rem α (q i) (p i) - rem α (q j) (p j)‖

Window separation (the fully-proven elementary half of Ermakov's separation lemma). Let q be strictly increasing with the best-approximation property hbest (every positive denominator below q (k+1) has defect ≥ δ_{q k}). In a doubling window q (k+K) < q (k+1) + q k, any two of the remainder vectors r(q k), …, r(q (k+K)) are at least δ_{q k} apart:

δ_{q k} ≤ ‖r(qᵢ) − r(qⱼ)‖ for k ≤ j < i ≤ k+K.

Proof: 0 < qᵢ − qⱼ < q (k+1) (the window keeps the index gap below q (k+1)), so hbest gives δ_{q k} ≤ δ_{qᵢ − qⱼ}, and delta_diff_le gives δ_{qᵢ − qⱼ} ≤ ‖r(qᵢ) − r(qⱼ)‖.

Since the remainder lengths ‖r(q i)‖ = δ_{q i} decrease, these are K+1 vectors of norm ≤ δ_{q k} that are pairwise ≥ δ_{q k} apart. The geometric completion — their normalised directions are pairwise > π/3, so at most K = contact-number many exist — is Ermakov's Lemmas 1–2, the one remaining cited input (ThreeGap.growth_of_separation's hypothesis).