Dirichlet's theorem for systems of linear forms

Let A be a real m × n matrix, viewed as a system of m linear forms in n variables. Dirichlet's theorem says that for every Q > 1 there is a nonzero integer vector y with ‖y‖∞ ≤ Q such that every coordinate of A y lies within Q ^ (-n / m) of an integer. Specializing to a single column gives simultaneous approximation of m real numbers by rationals with a common denominator, and to a single row gives small values of one linear form. Under the condition that no nonzero integer vector is sent to an integer vector, the same bounds hold with Q replaced by ‖y‖∞ for infinitely many solutions; these are the lower bounds behind exponents of approximation.

Main results

• Matrix.exists_int_abs_sum_mul_sub_le: for P, δ ≥ 0 with δ < 1 and P ^ n δ ^ m ≥ 1 there is a nonzero y ∈ ℤⁿ with |yⱼ| ≤ P and x ∈ ℤᵐ with |(A y)ᵢ - xᵢ| ≤ δ.
• Matrix.dirichlet_linearForms: Dirichlet's theorem with the bounds Q and Q ^ (-n / m).
• Matrix.dirichlet_linearForms_infinite: if A y is never an integer vector for nonzero integral y, there are infinitely many solutions of |(A y)ᵢ - xᵢ| ≤ ‖y‖∞ ^ (-n / m).
• TauCeti.simultaneous_dirichlet: for α ∈ ℝᵐ and Q > 1 there are integers x and 0 < y ≤ Q ^ m with |xᵢ - αᵢ y| ≤ Q⁻¹.
• TauCeti.dirichlet_linearForm_infinite: the case of a single linear form.
• Real.infinite_setOf_mul_abs_mul_sub_round_le_one: for every real α, infinitely many q ≥ 1 satisfy q ‖q α‖ ≤ 1, where ‖x‖ = |x - round x|.
• Real.infinite_setOf_mul_le_one: for every pair of reals α, β, infinitely many q ≥ 1 satisfy q ‖q α‖ ‖q β‖ ≤ 1.

Implementation notes

The proof applies Minkowski's convex body theorem (MeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume) to the integer lattice in ℝ^(κ ⊕ ι) and the preimage of a box under the integral shear (y, x) ↦ (y, A y - x), an involution of determinant ±1.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes, Chapter 1, Theorems 1.1, 1.3 and 1.4, and Chapter 2, Corollaries 2.6 and 2.7 and Exercise 2.6.
• W. M. Schmidt, Diophantine Approximation, Lecture Notes in Mathematics 785, Chapter II.

theorem Matrix.exists_int_abs_sum_mul_sub_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [Nonempty κ] (A : Matrix ι κ ℝ) {P δ : ℝ} (hP : 0 ≤ P) (hδ₀ : 0 ≤ δ) (hδ₁ : δ < 1) (h : 1 ≤ P ^ Fintype.card κ * δ ^ Fintype.card ι) : ∃ (y : κ → ℤ) (x : ι → ℤ), y ≠ 0 ∧ (∀ (j : κ), |↑(y j)| ≤ P) ∧ ∀ (i : ι), |∑ j : κ, A i j * ↑(y j) - ↑(x i)| ≤ δ

Dirichlet's theorem for linear forms, with general bounds. Let A be a real matrix with rows indexed by ι and columns indexed by the nonempty type κ. If P, δ ≥ 0, δ < 1 and P ^ |κ| δ ^ |ι| ≥ 1, then there are a nonzero integer vector y with |yⱼ| ≤ P and an integer vector x with |∑ⱼ Aᵢⱼ yⱼ - xᵢ| ≤ δ for every i.

theorem Matrix.dirichlet_linearForms {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [Nonempty ι] [Nonempty κ] (A : Matrix ι κ ℝ) {Q : ℝ} (hQ : 1 < Q) : ∃ (y : κ → ℤ) (x : ι → ℤ), y ≠ 0 ∧ (∀ (j : κ), |↑(y j)| ≤ Q) ∧ ∀ (i : ι), |∑ j : κ, A i j * ↑(y j) - ↑(x i)| ≤ Q ^ (-↑(Fintype.card κ) / ↑(Fintype.card ι))

Dirichlet's theorem for systems of linear forms. Let A be a real matrix with m = |ι| ≥ 1 rows and n = |κ| ≥ 1 columns, and let Q > 1. There are a nonzero integer vector y with |yⱼ| ≤ Q and an integer vector x with |∑ⱼ Aᵢⱼ yⱼ - xᵢ| ≤ Q ^ (-n / m) for every i.

theorem Matrix.dirichlet_linearForms_infinite {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [Nonempty κ] (A : Matrix ι κ ℝ) (hA : ∀ (y : κ → ℤ), (∀ (i : ι), ∃ (k : ℤ), ∑ j : κ, A i j * ↑(y j) = ↑k) → y = 0) : {p : (κ → ℤ) × (ι → ℤ) | p.1 ≠ 0 ∧ ∀ (i : ι), |∑ j : κ, A i j * ↑(p.1 j) - ↑(p.2 i)| ≤ ‖p.1‖ ^ (-↑(Fintype.card κ) / ↑(Fintype.card ι))}.Infinite

Dirichlet's theorem for systems of linear forms, infinitely many solutions. Let A be a real matrix with m = |ι| rows and n = |κ| ≥ 1 columns such that A y is an integer vector for an integer vector y only when y = 0. Then infinitely many pairs of integer vectors (y, x) with y ≠ 0 satisfy |∑ⱼ Aᵢⱼ yⱼ - xᵢ| ≤ ‖y‖ ^ (-n / m) for every i, where ‖y‖ is the sup norm.

theorem TauCeti.simultaneous_dirichlet {ι : Type u_1} [Fintype ι] (α : ι → ℝ) {Q : ℝ} (hQ : 1 < Q) : ∃ (x : ι → ℤ) (y : ℤ), 0 < y ∧ ↑y ≤ Q ^ Fintype.card ι ∧ ∀ (i : ι), |↑(x i) - α i * ↑y| ≤ Q⁻¹

Simultaneous Dirichlet approximation. For real numbers αᵢ, i ∈ ι, and Q > 1 there are integers xᵢ and 0 < y ≤ Q ^ |ι| with |xᵢ - αᵢ y| ≤ Q⁻¹ for every i.

theorem TauCeti.dirichlet_linearForm_infinite {κ : Type u_2} [Fintype κ] [Nonempty κ] (α : κ → ℝ) (hα : ∀ (y : κ → ℤ), (∃ (k : ℤ), ∑ j : κ, α j * ↑(y j) = ↑k) → y = 0) : {p : ℤ × (κ → ℤ) | p.2 ≠ 0 ∧ |∑ j : κ, α j * ↑(p.2 j) - ↑p.1| ≤ ‖p.2‖ ^ (-↑(Fintype.card κ))}.Infinite

Dirichlet's theorem for one linear form, infinitely many solutions. Let αⱼ, j ∈ κ, be real numbers, n = |κ| ≥ 1, such that ∑ⱼ αⱼ yⱼ is an integer for an integer vector y only when y = 0. Then infinitely many pairs (x, y) with y ≠ 0 satisfy |∑ⱼ αⱼ yⱼ - x| ≤ ‖y‖ ^ (-n), where ‖y‖ is the sup norm.

theorem Rat.abs_den_mul_sub_round_eq_zero (r : ℚ) (n : ℕ) : |↑(n * r.den) * ↑r - ↑(round (↑(n * r.den) * ↑r))| = 0

A rational number times a multiple of its denominator is an integer, so it has distance 0 from the nearest integer.

theorem Real.infinite_setOf_mul_abs_mul_sub_round_le_one (α : ℝ) : {q : ℕ | 0 < q ∧ ↑q * |↑q * α - ↑(round (↑q * α))| ≤ 1}.Infinite

Dirichlet's theorem, nearest-integer form. For every real α, infinitely many natural numbers q ≥ 1 satisfy q ‖q α‖ ≤ 1.

theorem Real.infinite_setOf_mul_le_one (α β : ℝ) : {y : ℕ | 0 < y ∧ ↑y * |↑y * α - ↑(round (↑y * α))| * |↑y * β - ↑(round (↑y * β))| ≤ 1}.Infinite

For all real α, β, infinitely many y ≥ 1 satisfy y ‖y α‖ ‖y β‖ ≤ 1.