Integral kernels against the Bombieri–Vaaler bound

For an integer matrix A with p independent rows and n columns, Bombieri and Vaaler bound small integral solutions of A x = 0 by the quotient √det (A Aᵀ) / g, where g is the gcd of the maximal minors of A. The integral kernel has a ℤ-basis whose product of sup norms is at most k! / 2 ^ (k - 1) times this quotient, where k = n - p (Matrix.exists_basis_ker_mulVecLin_prod_norm_le). The quotient depends only on the rational row space of A. Siegel's classical bound (n · max 1 ‖A‖) ^ (p / k) (Mathlib's Int.Matrix.exists_ne_zero_int_vec_norm_le) depends on the entries of A. This file computes both bounds, and the integral kernel itself, on two examples where k = 1. In each one the kernel is a line ℤ ∙ v, so its only bases are v and -v.

• Rescaling a row. The rows (1, 1) and (2, 2) have Gram determinants 2 and 8 and minor gcds 1 and 2, so both quotients are √2. Both integral kernels are generated by (1, -1), of sup norm 1 ≤ √2.
• A unimodular shear. The matrix A with rows (1, 0, -1) and (0, 1, -1) has Gram determinant 3 and minor gcd 1, so its quotient is √3. The shear U with rows (1, 1) and (0, 1) gives U A, with rows (1, 1, -2) and (0, 1, -1), and the same quotient √3. Both integral kernels are generated by (1, 1, 1), of sup norm 1 ≤ √3. Siegel's bound moves from (3 · 1) ^ 2 = 9 for A to (3 · 2) ^ 2 = 36 for U A. In the names below, diff refers to A, whose rows compute the differences x 0 - x 2 and x 1 - x 2, and shear_mul_diff to U A.

Main results

• TauCeti.IntegralKernelExample.ker_mulVecLin_one_one and TauCeti.IntegralKernelExample.ker_mulVecLin_two_two: both kernels are ℤ ∙ (1, -1).
• TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_one_one and TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_two_two: both quotients are √2.
• TauCeti.IntegralKernelExample.ker_mulVecLin_diff and TauCeti.IntegralKernelExample.ker_mulVecLin_shear_mul_diff: both kernels are ℤ ∙ (1, 1, 1).
• TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_diff and TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_shear_mul_diff: both quotients are √3.
• TauCeti.IntegralKernelExample.norm_one_neg_one_le_sqrt_det_div_minorGcd_two_two and TauCeti.IntegralKernelExample.norm_one_one_one_le_sqrt_det_div_minorGcd_shear_mul_diff: the generators meet the bound.
• TauCeti.IntegralKernelExample.card_mul_max_one_norm_diff_rpow and TauCeti.IntegralKernelExample.card_mul_max_one_norm_shear_mul_diff_rpow: Siegel's bounds 9 and 36.

References

• E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32, Theorems 1 and 2.

Rescaling a row

theorem TauCeti.IntegralKernelExample.minorGcd_one_one : !![1, 1].minorGcd = 1

The row (1, 1) has minor gcd 1.

theorem TauCeti.IntegralKernelExample.det_one_one : (!![1, 1] * !![1, 1].transpose).det = 2

The row (1, 1) has Gram determinant 2.

theorem TauCeti.IntegralKernelExample.ker_mulVecLin_one_one : !![1, 1].mulVecLin.ker = ℤ ∙ ![1, -1]

The integral kernel of the row (1, 1) is the line through (1, -1).

theorem TauCeti.IntegralKernelExample.ker_mulVecLin_two_two : !![2, 2].mulVecLin.ker = ℤ ∙ ![1, -1]

The integral kernel of the row (2, 2) is the line through (1, -1), as for (1, 1).

theorem TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_one_one : √↑(!![1, 1] * !![1, 1].transpose).det / ↑!![1, 1].minorGcd = √2

The Bombieri–Vaaler quotient of the row (1, 1) is √2.

theorem TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_two_two : √↑(!![2, 2] * !![2, 2].transpose).det / ↑!![2, 2].minorGcd = √2

The Bombieri–Vaaler quotient of the row (2, 2) is √2, as for (1, 1): rescaling the row by 2 multiplies the square root of the Gram determinant and the minor gcd by 2.

theorem TauCeti.IntegralKernelExample.norm_one_neg_one : ‖![1, -1]‖ = 1

The generator (1, -1) of both kernels has sup norm 1.

theorem TauCeti.IntegralKernelExample.norm_one_neg_one_le_sqrt_det_div_minorGcd_two_two : ‖![1, -1]‖ ≤ √↑(!![2, 2] * !![2, 2].transpose).det / ↑!![2, 2].minorGcd

The generator (1, -1) of the kernel of the row (2, 2) meets the Bombieri–Vaaler bound.

A unimodular shear

theorem TauCeti.IntegralKernelExample.minorGcd_diff : !![1, 0, -1; 0, 1, -1].minorGcd = 1

The matrix with rows (1, 0, -1) and (0, 1, -1) has minor gcd 1.

theorem TauCeti.IntegralKernelExample.det_diff : (!![1, 0, -1; 0, 1, -1] * !![1, 0, -1; 0, 1, -1].transpose).det = 3

The matrix with rows (1, 0, -1) and (0, 1, -1) has Gram determinant 3.

theorem TauCeti.IntegralKernelExample.ker_mulVecLin_diff : !![1, 0, -1; 0, 1, -1].mulVecLin.ker = ℤ ∙ ![1, 1, 1]

The integral kernel of the matrix with rows (1, 0, -1) and (0, 1, -1) is the line through (1, 1, 1).

theorem TauCeti.IntegralKernelExample.shear_mul_diff : !![1, 1; 0, 1] * !![1, 0, -1; 0, 1, -1] = !![1, 1, -2; 0, 1, -1]

The shear with rows (1, 1) and (0, 1) sends the matrix with rows (1, 0, -1) and (0, 1, -1) to the matrix with rows (1, 1, -2) and (0, 1, -1).

theorem TauCeti.IntegralKernelExample.ker_mulVecLin_shear_mul_diff : !![1, 1, -2; 0, 1, -1].mulVecLin.ker = ℤ ∙ ![1, 1, 1]

The integral kernel of the matrix with rows (1, 1, -2) and (0, 1, -1) is the line through (1, 1, 1), as for the matrix with rows (1, 0, -1) and (0, 1, -1).

theorem TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_diff : √↑(!![1, 0, -1; 0, 1, -1] * !![1, 0, -1; 0, 1, -1].transpose).det / ↑!![1, 0, -1; 0, 1, -1].minorGcd = √3

The Bombieri–Vaaler quotient of the matrix with rows (1, 0, -1) and (0, 1, -1) is √3.

theorem TauCeti.IntegralKernelExample.sqrt_det_div_minorGcd_shear_mul_diff : √↑(!![1, 1, -2; 0, 1, -1] * !![1, 1, -2; 0, 1, -1].transpose).det / ↑!![1, 1, -2; 0, 1, -1].minorGcd = √3

The Bombieri–Vaaler quotient of the matrix with rows (1, 1, -2) and (0, 1, -1) is √3, unchanged by the shear.

theorem TauCeti.IntegralKernelExample.norm_one_one_one : ‖![1, 1, 1]‖ = 1

The generator (1, 1, 1) of both kernels has sup norm 1.

theorem TauCeti.IntegralKernelExample.norm_one_one_one_le_sqrt_det_div_minorGcd_shear_mul_diff : ‖![1, 1, 1]‖ ≤ √↑(!![1, 1, -2; 0, 1, -1] * !![1, 1, -2; 0, 1, -1].transpose).det / ↑!![1, 1, -2; 0, 1, -1].minorGcd

The generator (1, 1, 1) of the kernel of the sheared matrix with rows (1, 1, -2) and (0, 1, -1) meets the Bombieri–Vaaler bound.

theorem TauCeti.IntegralKernelExample.norm_diff : ‖!![1, 0, -1; 0, 1, -1]‖ = 1

The matrix with rows (1, 0, -1) and (0, 1, -1) has largest entry 1 in absolute value.

theorem TauCeti.IntegralKernelExample.norm_shear_mul_diff : ‖!![1, 1, -2; 0, 1, -1]‖ = 2

The matrix with rows (1, 1, -2) and (0, 1, -1) has largest entry 2 in absolute value.

theorem TauCeti.IntegralKernelExample.card_mul_max_one_norm_diff_rpow : (↑(Fintype.card (Fin 3)) * max 1 ‖!![1, 0, -1; 0, 1, -1]‖) ^ (↑(Fintype.card (Fin 2)) / (↑(Fintype.card (Fin 3)) - ↑(Fintype.card (Fin 2)))) = 9

Siegel's bound (n · max 1 ‖A‖) ^ (p / (n - p)) of Int.Matrix.exists_ne_zero_int_vec_norm_le for the matrix with rows (1, 0, -1) and (0, 1, -1) is 9.

theorem TauCeti.IntegralKernelExample.card_mul_max_one_norm_shear_mul_diff_rpow : (↑(Fintype.card (Fin 3)) * max 1 ‖!![1, 1, -2; 0, 1, -1]‖) ^ (↑(Fintype.card (Fin 2)) / (↑(Fintype.card (Fin 3)) - ↑(Fintype.card (Fin 2)))) = 36

Siegel's bound for the matrix with rows (1, 1, -2) and (0, 1, -1) is 36: the shear moves it, while it leaves the Bombieri–Vaaler quotient and the integral kernel unchanged.