Finite covers of Lipschitz images of a cube

A mesh with denominator N covers the unit cube within distance 1/N. This supplies explicit covering cardinalities for the boundary charts used in quantitative lattice counting.

noncomputable def NairTenenbaum.cubeGridPoint {ι : Type u_1} (N : ℕ) (j : ι → Fin (N + 1)) : ι → ℝ

The grid point associated with an index in the subdivision of the unit cube.

Equations

• NairTenenbaum.cubeGridPoint N j i = ↑↑(j i) / ↑N

theorem NairTenenbaum.cubeGridPoint_mem {ι : Type u_1} {N : ℕ} (hN : 0 < N) (j : ι → Fin (N + 1)) : cubeGridPoint N j ∈ Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1

theorem NairTenenbaum.exists_cubeGridPoint_dist_le {ι : Type u_1} [Fintype ι] {N : ℕ} (hN : 0 < N) {x : ι → ℝ} (hx : x ∈ Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1) : ∃ (j : ι → Fin (N + 1)), dist x (cubeGridPoint N j) ≤ 1 / ↑N

theorem NairTenenbaum.exists_finset_lipschitz_cube_cover {ι : Type u_1} [Fintype ι] {E : Type u_2} [PseudoMetricSpace E] {f : (ι → ℝ) → E} {L : NNReal} (hf : LipschitzOnWith L f (Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1)) {N : ℕ} (hN : 0 < N) : ∃ (S : Finset E), S.card ≤ (N + 1) ^ Fintype.card ι ∧ (↑S ⊆ f '' Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1) ∧ ∀ y ∈ f '' Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1, ∃ z ∈ S, dist y z ≤ ↑L / ↑N

theorem NairTenenbaum.exists_finset_scaled_lipschitz_cube_cover {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : (ι → ℝ) → E} {L : NNReal} (hf : LipschitzOnWith L f (Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1)) {t : ℝ} (ht : 1 ≤ t) : ∃ (S : Finset E), ↑S.card ≤ (3 * t) ^ Fintype.card ι ∧ (↑S ⊆ (fun (x : ι → ℝ) => t • f x) '' Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1) ∧ ∀ y ∈ (fun (x : ι → ℝ) => t • f x) '' Set.Icc (fun (x : ι) => 0) fun (x : ι) => 1, ∃ z ∈ S, dist y z ≤ ↑L