Bounding lattice discrepancy by cells meeting the boundary

For every bounded set, the difference between its volume and its number of integer lattice points is at most the number of mixed unit cells. Each such cell contains a boundary point within distance one of its lattice corner.

theorem NairTenenbaum.integerLatticePoint_mem_cell {ι : Type u_1} (m : ι → ℤ) : integerLatticePoint m ∈ integerLatticeCell m

theorem NairTenenbaum.integerLatticeCell_isPreconnected {ι : Type u_1} (m : ι → ℤ) : IsPreconnected (integerLatticeCell m)

theorem NairTenenbaum.integerLatticeCell_inter_frontier {ι : Type u_1} {s : Set (ι → ℝ)} {m : ι → ℤ} (hin : (integerLatticeCell m ∩ s).Nonempty) (hout : ¬integerLatticeCell m ⊆ s) : (integerLatticeCell m ∩ frontier s).Nonempty

theorem NairTenenbaum.exists_finset_integerLattice_outer_cells {ι : Type u_1} [Finite ι] {s : Set (ι → ℝ)} (hs : Bornology.IsBounded s) : ∃ (O : Finset (ι → ℤ)), ∀ (m : ι → ℤ), m ∈ O ↔ (integerLatticeCell m ∩ s).Nonempty

theorem NairTenenbaum.exists_integerLattice_boundary_error {ι : Type u_1} [Fintype ι] {s : Set (ι → ℝ)} (hs : Bornology.IsBounded s) : ∃ (A : Finset (ι → ℤ)) (B : Finset (ι → ℤ)), (∀ (m : ι → ℤ), m ∈ A ↔ integerLatticePoint m ∈ s) ∧ |↑A.card - MeasureTheory.volume.real s| ≤ ↑B.card ∧ ∀ m ∈ B, ∃ x ∈ frontier s, dist (integerLatticePoint m) x ≤ 1