Uniform bounds for integer lattice points in balls

The ambient norm on a finite product of real lines is the supremum norm. Each coordinate lies in an integer interval of uniformly bounded length.

theorem NairTenenbaum.card_integer_interval_le {a b R : ℝ} (_hR : 0 ≤ R) (hab : b - a ≤ R) : (Finset.Icc ⌈a⌉ ⌊b⌋).card ≤ ⌈R⌉₊ + 1

noncomputable def NairTenenbaum.integerLatticePoint {ι : Type u_1} (m : ι → ℤ) : ι → ℝ

The ambient real point associated with integer lattice coordinates.

Equations

• NairTenenbaum.integerLatticePoint m i = ↑(m i)

theorem NairTenenbaum.card_integerLattice_ball_le {ι : Type u_1} [Fintype ι] (S : Finset (ι → ℤ)) (c : ι → ℝ) {R : ℝ} (hR : 0 ≤ R) (hS : ∀ m ∈ S, dist (integerLatticePoint m) c ≤ R) : S.card ≤ (⌈2 * R⌉₊ + 1) ^ Fintype.card ι

theorem NairTenenbaum.card_integerLattice_near_cover_le {ι : Type u_1} [Fintype ι] (A : Finset (ι → ℤ)) (S : Finset (ι → ℝ)) {R : ℝ} (hR : 0 ≤ R) (hcover : ∀ m ∈ A, ∃ c ∈ S, dist (integerLatticePoint m) c ≤ R) : A.card ≤ S.card * (⌈2 * R⌉₊ + 1) ^ Fintype.card ι