Unit cells around the standard integer lattice

The half-open cells partition real coordinate space, have volume one, and lie within distance one of their lattice corner in the supremum norm.

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

The unit cell attached to an integer lattice point.

Equations

• NairTenenbaum.integerLatticeCell m = Set.univ.pi fun (i : ι) => Set.Ico (↑(m i)) (↑(m i) + 1)

theorem NairTenenbaum.mem_integerLatticeCell {ι : Type u_1} {m : ι → ℤ} {x : ι → ℝ} : x ∈ integerLatticeCell m ↔ ∀ (i : ι), ↑(m i) ≤ x i ∧ x i < ↑(m i) + 1

theorem NairTenenbaum.mem_integerLatticeCell_iff_floor {ι : Type u_1} {m : ι → ℤ} {x : ι → ℝ} : x ∈ integerLatticeCell m ↔ (fun (i : ι) => ⌊x i⌋) = m

theorem NairTenenbaum.mem_integerLatticeCell_floor {ι : Type u_1} (x : ι → ℝ) : x ∈ integerLatticeCell fun (i : ι) => ⌊x i⌋

theorem NairTenenbaum.integerLatticeCell_pairwiseDisjoint {ι : Type u_1} : Pairwise fun (m n : ι → ℤ) => Disjoint (integerLatticeCell m) (integerLatticeCell n)

theorem NairTenenbaum.measurableSet_integerLatticeCell {ι : Type u_1} [Finite ι] (m : ι → ℤ) : MeasurableSet (integerLatticeCell m)

theorem NairTenenbaum.volume_integerLatticeCell {ι : Type u_1} [Fintype ι] (m : ι → ℤ) : MeasureTheory.volume (integerLatticeCell m) = 1

theorem NairTenenbaum.integerLatticeCell_dist_le_one {ι : Type u_1} [Fintype ι] {m : ι → ℤ} {x : ι → ℝ} (hx : x ∈ integerLatticeCell m) : dist x (integerLatticePoint m) ≤ 1

noncomputable def NairTenenbaum.integerLatticeCellUnion {ι : Type u_1} (S : Finset (ι → ℤ)) : Set (ι → ℝ)

The union of the cells attached to the selected integer lattice points.

Equations

• NairTenenbaum.integerLatticeCellUnion S = ⋃ m ∈ S, NairTenenbaum.integerLatticeCell m

theorem NairTenenbaum.volume_integerLatticeCellUnion {ι : Type u_1} [Fintype ι] (S : Finset (ι → ℤ)) : MeasureTheory.volume (integerLatticeCellUnion S) = ↑S.card

theorem NairTenenbaum.volume_real_integerLatticeCellUnion {ι : Type u_1} [Fintype ι] (S : Finset (ι → ℤ)) : MeasureTheory.volume.real (integerLatticeCellUnion S) = ↑S.card

theorem NairTenenbaum.latticeCell_volume_discrepancy_le {ι : Type u_1} [Fintype ι] (I A O : Finset (ι → ℤ)) (hIA : I ⊆ A) (hAO : A ⊆ O) {s : Set (ι → ℝ)} (hinside : integerLatticeCellUnion I ⊆ s) (houtside : s ⊆ integerLatticeCellUnion O) : |↑A.card - MeasureTheory.volume.real s| ≤ ↑(O \ I).card