Kronecker's approximation theorem

Let α₁, …, αₙ be real numbers such that 1, α₁, …, αₙ are linearly independent over ℚ, that is, x₀ + ∑ i, xᵢ αᵢ = 0 with integers xᵢ only for x = 0. Kronecker's theorem says that the points (y αᵢ - xᵢ)ᵢ, for y ∈ ℤ and x ∈ ℤⁿ, are dense in ℝⁿ: the integer multiples of α are dense in the torus ℝⁿ / ℤⁿ. Hence for every target θ ∈ ℝⁿ and every ε > 0 the inhomogeneous system |y αᵢ - xᵢ - θᵢ| ≤ ε has infinitely many integer solutions, even with the multiplier y a positive integer as large as we please.

This is the inhomogeneous companion of Dirichlet's theorem (TauCeti.simultaneous_dirichlet), which approximates the target θ = 0 with an explicit rate and needs no hypothesis on α.

Main results

• TauCeti.denseRange_mul_sub_intCast: Kronecker's theorem in density form.
• TauCeti.kronecker_approximation: infinitely many integer solutions of |y αᵢ - xᵢ - θᵢ| ≤ ε.
• TauCeti.kronecker_approximation_nat: infinitely many natural numbers n for which |n αᵢ - xᵢ - θᵢ| ≤ ε has an integer solution x.

Implementation notes

The density follows from AddSubgroup.dense_iff_forall_dual_eq_zero: a real linear functional f taking integer values on the points y α - x takes integer values kᵢ = f eᵢ on the standard basis and m = f α = ∑ i, kᵢ αᵢ on α, an integer relation between 1, α₁, …, αₙ, so k = 0 and f = 0.

The positive form kronecker_approximation_nat follows by symmetry: the solutions of the homogeneous system (θ = 0) are closed under (x, y) ↦ (-x, -y), so their multipliers y are unbounded above, and adding one with a large multiplier to a single solution for θ gives a solution with a large positive multiplier.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes, Chapter 2, Theorem 2.22.
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, Chapter XXIII, Theorem 442.

theorem TauCeti.denseRange_mul_sub_intCast {ι : Type u_1} [Fintype ι] {α : ι → ℝ} (hα : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i : ι, ↑(x.2 i) * α i = 0 → x = 0) : DenseRange fun (p : (ι → ℤ) × ℤ) (i : ι) => α i * ↑p.2 - ↑(p.1 i)

Kronecker's theorem, density form. If 1 and the real numbers αᵢ satisfy no nontrivial integer relation, that is, if they are linearly independent over ℚ, then the points (y αᵢ - xᵢ)ᵢ, for y ∈ ℤ and x ∈ ℤ^ι, are dense in ℝ^ι.

theorem TauCeti.kronecker_approximation {ι : Type u_1} [Fintype ι] {α : ι → ℝ} (hα : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i : ι, ↑(x.2 i) * α i = 0 → x = 0) (θ : ι → ℝ) {ε : ℝ} (hε : 0 < ε) : {p : (ι → ℤ) × ℤ | ∀ (i : ι), |α i * ↑p.2 - ↑(p.1 i) - θ i| ≤ ε}.Infinite

Kronecker's approximation theorem. If 1 and the real numbers αᵢ satisfy no nontrivial integer relation, that is, if they are linearly independent over ℚ, then for every θ ∈ ℝ^ι and ε > 0 there are infinitely many integer pairs (x, y), x ∈ ℤ^ι, y ∈ ℤ, with |y αᵢ - xᵢ - θᵢ| ≤ ε for every i.

theorem TauCeti.kronecker_approximation_nat {ι : Type u_1} [Fintype ι] {α : ι → ℝ} (hα : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i : ι, ↑(x.2 i) * α i = 0 → x = 0) (θ : ι → ℝ) {ε : ℝ} (hε : 0 < ε) : {n : ℕ | ∃ (x : ι → ℤ), ∀ (i : ι), |α i * ↑n - ↑(x i) - θ i| ≤ ε}.Infinite

Kronecker's approximation theorem with positive multipliers. If 1 and the real numbers αᵢ satisfy no nontrivial integer relation, that is, if they are linearly independent over ℚ, then for every θ ∈ ℝ^ι and ε > 0 there are infinitely many natural numbers n, hence arbitrarily large positive ones, each with some x ∈ ℤ^ι such that |n αᵢ - xᵢ - θᵢ| ≤ ε for every i.