Quantitative lattice counting for a finite Lipschitz boundary

A bounded subset of real coordinate space whose boundary is covered by finitely many m-parameter Lipschitz charts has lattice discrepancy O(t^m) under dilation by t. All chart and boundedness hypotheses are explicit.

noncomputable def NairTenenbaum.integerLatticeCount {ι : Type u_1} (s : Set (ι → ℝ)) : ℕ

The number of integer lattice points in a set.

Equations

• NairTenenbaum.integerLatticeCount s = Nat.card { m : ι → ℤ // NairTenenbaum.integerLatticePoint m ∈ s }

theorem NairTenenbaum.integerLatticeCount_eq_card {ι : Type u_1} {s : Set (ι → ℝ)} (A : Finset (ι → ℤ)) (hA : ∀ (m : ι → ℤ), m ∈ A ↔ integerLatticePoint m ∈ s) : integerLatticeCount s = A.card

theorem NairTenenbaum.volume_real_smul_coordinate_set {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : 0 ≤ t) (s : Set (ι → ℝ)) : MeasureTheory.volume.real (t • s) = t ^ Fintype.card ι * MeasureTheory.volume.real s

theorem NairTenenbaum.exists_lipschitz_boundary_lattice_discrepancy {ι : Type u_1} {κ : Type u_2} {J : Type u_3} [Fintype ι] [Fintype κ] [Finite J] {s : Set (ι → ℝ)} (hs : Bornology.IsBounded s) (f : J → (κ → ℝ) → ι → ℝ) (L : J → NNReal) (hf : ∀ (j : J), LipschitzOnWith (L j) (f j) (Set.Icc (fun (x : κ) => 0) fun (x : κ) => 1)) (hcover : ∀ y ∈ frontier s, ∃ (j : J), ∃ x ∈ Set.Icc (fun (x : κ) => 0) fun (x : κ) => 1, f j x = y) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ), 1 ≤ t → |↑(integerLatticeCount (t • s)) - t ^ Fintype.card ι * MeasureTheory.volume.real s| ≤ C * t ^ Fintype.card κ