Lattice points near an expanding Lipschitz chart

A chart with m real parameters has O(t^m) integer lattice points within a fixed distance of its dilation by t. This is the boundary-cell estimate needed for quantitative lattice counting.

theorem NairTenenbaum.card_integerLattice_near_scaled_chart_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {f : (ι → ℝ) → κ → ℝ} {L : NNReal} (hf : LipschitzOnWith L f (Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1)) {R t : ℝ} (hR : 0 ≤ R) (ht : 1 ≤ t) (A : Finset (κ → ℤ)) (hA : ∀ m ∈ A, ∃ x ∈ Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1, dist (integerLatticePoint m) (t • f x) ≤ R) : ↑A.card ≤ (3 * t) ^ Fintype.card ι * ↑(⌈2 * (R + ↑L)⌉₊ + 1) ^ Fintype.card κ

theorem NairTenenbaum.exists_integerLattice_near_scaled_chart_bound {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {f : (ι → ℝ) → κ → ℝ} {L : NNReal} (hf : LipschitzOnWith L f (Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1)) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), 1 ≤ t → ∀ (A : Finset (κ → ℤ)), (∀ m ∈ A, ∃ x ∈ Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1, dist (integerLatticePoint m) (t • f x) ≤ R) → ↑A.card ≤ C * t ^ Fintype.card ι