Minkowski's linear forms theorem

Let n ≥ 1, let A be an invertible real n × n matrix, read as n linear forms x ↦ ∑ⱼ Aᵢⱼ xⱼ in n variables, and let a₀, …, aₙ₋₁ ≥ 0 with ∏ᵢ aᵢ ≥ |det A|. Minkowski's linear forms theorem says that some nonzero integer vector z has |∑ⱼ Aᵢⱼ zⱼ| ≤ aᵢ for every i. All the inequalities are non-strict, including when ∏ᵢ aᵢ = |det A|. The hypothesis n ≥ 1 cannot be dropped: for n = 0 both det A and ∏ᵢ aᵢ are 1, but the only integer vector is zero. The theorem is the basic tool for producing small values of linear forms at integer points, as in Dirichlet's approximation theorem.

The region {x | ∀ i, |(A *ᵥ x) i| ≤ aᵢ} is compact, convex and symmetric about the origin, and has volume 2 ^ n * (∏ᵢ aᵢ) / |det A| ≥ 2 ^ n by Matrix.volume_setOf_forall_abs_mulVec_le. Minkowski's convex body theorem for the integer lattice (MeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume) gives the integer point.

Main results

• Matrix.exists_ne_zero_int_abs_sum_mul_le: Minkowski's linear forms theorem, for a matrix indexed by a nonempty finite type.

References

• J.-H. Evertse, Diophantine approximation, Chapter 2: Geometry of numbers, §2.2, Corollary 2.6 and its proof, printed p.20: https://pub.math.leidenuniv.nl/~evertsejh/dio19-2.pdf.

theorem Matrix.exists_ne_zero_int_abs_sum_mul_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (A : Matrix ι ι ℝ) (hA : A.det ≠ 0) {a : ι → ℝ} (ha : 0 ≤ a) (h : |A.det| ≤ ∏ i : ι, a i) : ∃ (z : ι → ℤ), z ≠ 0 ∧ ∀ (i : ι), |∑ j : ι, A i j * ↑(z j)| ≤ a i

Minkowski's linear forms theorem. Let A be an invertible real square matrix indexed by a nonempty finite type ι, and let a i ≥ 0 be bounds whose product is at least |det A|. Then some nonzero integer vector z satisfies |∑ j, A i j * z j| ≤ a i for every i.