Integral points in real-radius boxes

Coordinates are integers; membership in the locus is tested after casting to rational numbers. The definition works for real radii, including the boundary B = 1 in CCDN Theorem 3. InBox x B states that every coordinate of x has absolute value at most B; for points of ℤⁿ it is membership in the finite box integerBox n B (mem_integerBox). The counted sets are typically zero loci zeroLocus f of rational polynomials.

@[reducible, inline]

abbrev CCDN.IntPoint (n : ℕ) : Type

Integer points of affine n-space, as vectors Fin n → ℤ.

Equations

• CCDN.IntPoint n = (Fin n → ℤ)

@[reducible, inline]

abbrev CCDN.RatPoint (n : ℕ) : Type

Rational points of affine n-space, as vectors Fin n → ℚ.

Equations

• CCDN.RatPoint n = (Fin n → ℚ)

def CCDN.rationalPoint {n : ℕ} (x : IntPoint n) : RatPoint n

The integer point x, regarded as a rational point by casting each coordinate.

Equations

• CCDN.rationalPoint x i = ↑(x i)

@[reducible, inline]

abbrev CCDN.InBox {ι : Type u_1} (x : ι → ℤ) (B : ℝ) : Prop

Every coordinate of the integer vector x has absolute value at most B.

Equations

• CCDN.InBox x B = ∀ (i : ι), |↑(x i)| ≤ B

noncomputable def CCDN.integerBox (n : ℕ) (B : ℝ) : Finset (IntPoint n)

The finite box of integer points of ℤⁿ all of whose coordinates have absolute value at most the real radius B.

Equations

• CCDN.integerBox n B = Fintype.piFinset fun (x : Fin n) => Finset.Icc (-⌊B⌋) ⌊B⌋

theorem CCDN.mem_integerBox {n : ℕ} {B : ℝ} {x : IntPoint n} : x ∈ integerBox n B ↔ InBox x B

An integer point lies in integerBox n B exactly when all its coordinates have absolute value at most B.

noncomputable def CCDN.integralPoints {n : ℕ} (X : Set (RatPoint n)) (B : ℝ) : Finset (IntPoint n)

The integer points of absolute value at most B whose rational image lies in the set X.

Equations

• CCDN.integralPoints X B = {x ∈ CCDN.integerBox n B | CCDN.rationalPoint x ∈ X}

noncomputable def CCDN.count {n : ℕ} (X : Set (RatPoint n)) (B : ℝ) : ℕ

The number of integer points with all coordinates of absolute value at most B whose rational image lies in the set X.

Equations

• CCDN.count X B = (CCDN.integralPoints X B).card

theorem CCDN.mem_integralPoints {n : ℕ} {X : Set (RatPoint n)} {B : ℝ} {x : IntPoint n} : x ∈ integralPoints X B ↔ InBox x B ∧ rationalPoint x ∈ X

An integer point belongs to integralPoints X B exactly when it lies in the box of radius B and its rational image lies in X.

theorem CCDN.count_mono {n : ℕ} {X Y : Set (RatPoint n)} {B C : ℝ} (hXY : X ⊆ Y) (hBC : B ≤ C) : count X B ≤ count Y C

The integral point count is monotone in both the locus and the box radius.

theorem CCDN.count_union_le {n : ℕ} (X Y : Set (RatPoint n)) (B : ℝ) : count (X ∪ Y) B ≤ count X B + count Y B

The integral point count of a union is at most the sum of the counts.

def CCDN.zeroLocus {n : ℕ} (f : MvPolynomial (Fin n) ℚ) : Set (RatPoint n)

The rational zeros of a polynomial with rational coefficients.

Equations

• CCDN.zeroLocus f = {x : CCDN.RatPoint n | (MvPolynomial.eval x) f = 0}