Counting bounded integral points by the integer values of a linear form. Deleting a coordinate with nonzero coefficient is injective on each level and preserves the box radius.

def CCDN.integerLinearLevel {n : ℕ} (a x : IntPoint n) : ℤ

The value ∑ a i * x i of the integer linear form with coefficients a at the point x.

Equations

• CCDN.integerLinearLevel a x = ∑ i : Fin n, a i * x i

def CCDN.deleteIntegerCoordinate {n : ℕ} (j : Fin (n + 1)) (x : IntPoint (n + 1)) : IntPoint n

The projection of an integer point in n + 1 coordinates to n coordinates by deleting coordinate j.

Equations

• CCDN.deleteIntegerCoordinate j x i = x (j.succAbove i)

noncomputable def CCDN.integerSlicePoints {n : ℕ} (X : Set (RatPoint n)) (B : ℝ) (a : IntPoint n) (k : ℤ) : Finset (IntPoint n)

The integral points of X of height at most B on the level set ∑ a i * x i = k of the integer linear form with coefficients a.

Equations

• CCDN.integerSlicePoints X B a k = {x ∈ CCDN.integralPoints X B | CCDN.integerLinearLevel a x = k}

theorem CCDN.count_le_of_integer_hyperplane_slices {n : ℕ} (X : Set (RatPoint (n + 1))) (a : IntPoint (n + 1)) (j : Fin (n + 1)) (hj : a j ≠ 0) (Y : ℤ → Set (RatPoint n)) {H B K : ℝ} (hH : 0 ≤ H) (hB : 0 ≤ B) (hK : 0 ≤ K) (ha : InBox a H) (hmap : ∀ (k : ℤ), ∀ x ∈ integerSlicePoints X B a k, rationalPoint (deleteIntegerCoordinate j x) ∈ Y k) (hcount : ∀ (k : ℤ), ↑(count (Y k) B) ≤ K) : ↑(count X B) ≤ (2 * ↑(n + 1) * H * B + 1) * K

Assembly over the levels of the integral point set. The sets Y k can be the zero loci of the constructed hyperplane restrictions.