Lattice points in dilated regions

DefinitionInteger unit cube#✓fully proved

For \(v \in \mathbb{Z}^n\), the integer unit cube at \(v\) is the half-open cube \(Q_v = \prod_i [v_i, v_i + 1) \subseteq \mathbb{R}^n\), the set of \(x \in \mathbb{R}^n\) with \(v_i \le x_i < v_i + 1\) for every coordinate \(i\).

noncomputable def integerUnitCube {n : ℕ} (v : Fin n → ℤ) :
    Set (Fin n → ℝ) :=
  Set.pi Set.univ (fun i => Set.Ico (v i : ℝ) ((v i : ℝ) + 1))

Used by 10

Used byCubical measure sandwich · Finiteness of the outer cube set · Inner cube set · Inner cube indices are outer cube indices · Lattice-point error bound from boundary charts · Membership in the inner cube set · Membership in an integer unit cube · Membership in the outer cube set · Outer cube set · Boundary cubes meet the dilated frontier charts

TheoremMembership in an integer unit cube#✓fully proved

For \(v \in \mathbb{Z}^n\) and \(x \in \mathbb{R}^n\), \(x\) lies in the integer unit cube at \(v\) if and only if \(v_i \le x_i < v_i + 1\) for every coordinate \(i\).

@[simp] theorem mem_integerUnitCube_iff {n : ℕ} {v : Fin n → ℤ}
    {x : Fin n → ℝ} :
    x ∈ integerUnitCube v ↔ ∀ i, (v i : ℝ) ≤ x i ∧ x i < (v i : ℝ) + 1

Uses 1 · Used by 5

Statement usesInteger unit cube

Used byCubical measure sandwich · Finiteness of the outer cube set · Inner cube indices are outer cube indices · Lattice-point error bound from boundary charts · Boundary cubes meet the dilated frontier charts

DefinitionOuter cube set#✓fully proved

For a set \(S \subseteq \mathbb{R}^n\) and a real number \(t\), the outer cube set of \(S\) at scale \(t\) is the set of \(v \in \mathbb{Z}^n\) such that \((x_1/t, \dots, x_n/t) \in S\) for some \(x\) in the integer unit cube \(Q_v = \prod_i [v_i, v_i + 1)\). For \(t > 0\) these are the \(v\) with \(Q_v\) meeting \(tS\); for \(t = 0\) the division is read as \(x_i/0 = 0\).

def outerCubeSet {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) :
    Set (Fin n → ℤ) :=
  {v | ∃ x ∈ integerUnitCube v, (fun i => x i / t) ∈ S}

Uses 1 · Used by 7

Statement usesInteger unit cube

Used byCounting outer cubes by inner cubes and boundary charts · Cubical measure sandwich · Finiteness of the outer cube set · Inner cube indices are outer cube indices · Lattice-point error bound from boundary charts · Membership in the outer cube set · Boundary cubes meet the dilated frontier charts

TheoremMembership in the outer cube set#✓fully proved

For \(S \subseteq \mathbb{R}^n\), \(t \in \mathbb{R}\) and \(v \in \mathbb{Z}^n\), \(v\) belongs to the outer cube set of \(S\) at scale \(t\) if and only if \((x_1/t, \dots, x_n/t) \in S\) for some \(x\) in the integer unit cube at \(v\).

@[simp] theorem mem_outerCubeSet_iff {n : ℕ} {S : Set (Fin n → ℝ)} {t : ℝ}
    {v : Fin n → ℤ} :
    v ∈ outerCubeSet S t ↔ ∃ x ∈ integerUnitCube v, (fun i => x i / t) ∈ S

Uses 2 · Used by 5

Statement usesInteger unit cube · Outer cube set

Used byCubical measure sandwich · Finiteness of the outer cube set · Inner cube indices are outer cube indices · Lattice-point error bound from boundary charts · Boundary cubes meet the dilated frontier charts

DefinitionInner cube set#✓fully proved

For a set \(S \subseteq \mathbb{R}^n\) and a real number \(t\), the inner cube set of \(S\) at scale \(t\) is the set of \(v \in \mathbb{Z}^n\) such that \((x_1/t, \dots, x_n/t) \in S\) for every \(x\) in the integer unit cube \(Q_v = \prod_i [v_i, v_i + 1)\). For \(t > 0\) these are the \(v\) with \(Q_v \subseteq tS\); for \(t = 0\) the division is read as \(x_i/0 = 0\).

def innerCubeSet {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) :
    Set (Fin n → ℤ) :=
  {v | ∀ x ∈ integerUnitCube v, (fun i => x i / t) ∈ S}

Uses 1 · Used by 6

Statement usesInteger unit cube

Used byCounting outer cubes by inner cubes and boundary charts · Cubical measure sandwich · Inner cube indices are outer cube indices · Lattice-point error bound from boundary charts · Membership in the inner cube set · Boundary cubes meet the dilated frontier charts

TheoremMembership in the inner cube set#✓fully proved

For \(S \subseteq \mathbb{R}^n\), \(t \in \mathbb{R}\) and \(v \in \mathbb{Z}^n\), \(v\) belongs to the inner cube set of \(S\) at scale \(t\) if and only if \((x_1/t, \dots, x_n/t) \in S\) for every \(x\) in the integer unit cube at \(v\).

@[simp] theorem mem_innerCubeSet_iff {n : ℕ} {S : Set (Fin n → ℝ)} {t : ℝ}
    {v : Fin n → ℤ} :
    v ∈ innerCubeSet S t ↔ ∀ x ∈ integerUnitCube v, (fun i => x i / t) ∈ S

Uses 2 · Used by 4

Statement usesInner cube set · Integer unit cube

Used byCubical measure sandwich · Inner cube indices are outer cube indices · Lattice-point error bound from boundary charts · Boundary cubes meet the dilated frontier charts

TheoremInner cube indices are outer cube indices#✓fully proved

For every set \(S \subseteq \mathbb{R}^n\) and every real \(t\), the inner cube set of \(S\) at scale \(t\) is contained in the outer cube set of \(S\) at scale \(t\).

theorem innerCubeSet_subset_outerCubeSet {n : ℕ} (S : Set (Fin n → ℝ))
    (t : ℝ) : innerCubeSet S t ⊆ outerCubeSet S t

Uses 6 · Used by 2

Statement usesInner cube set · Outer cube set

Proof usesInteger unit cube · Membership in the inner cube set · Membership in an integer unit cube · Membership in the outer cube set

Used byCounting outer cubes by inner cubes and boundary charts · Cubical measure sandwich

TheoremFiniteness of the outer cube set#✓fully proved

If \(S \subseteq \mathbb{R}^n\) is bounded and \(t > 0\), then the outer cube set of \(S\) at scale \(t\), the set of \(v \in \mathbb{Z}^n\) whose integer unit cube \(\prod_i [v_i, v_i + 1)\) meets \(tS\), is finite.

theorem finite_outerCubeSet {n : ℕ} (S : Set (Fin n → ℝ))
    (hS : Bornology.IsBounded S) {t : ℝ} (ht : 0 < t) :
    (outerCubeSet S t).Finite

Uses 4 · Used by 2

Statement usesOuter cube set

Proof usesInteger unit cube · Membership in an integer unit cube · Membership in the outer cube set

Used byCubical measure sandwich · Lattice-point error bound from boundary charts

TheoremCubical measure sandwich#✓fully proved

Let \(S \subseteq \mathbb{R}^n\) be bounded, let \(t > 0\), and let \(\mathrm{vol}(S)\) be the Lebesgue (outer) measure of \(S\), which is finite. For \(v \in \mathbb{Z}^n\) let \(Q_v = \prod_i [v_i, v_i + 1)\). Let \(I\) be the inner cube set of \(S\) at scale \(t\), the \(v\) with \(Q_v \subseteq tS\), and \(O\) the outer cube set, the \(v\) with \(Q_v\) meeting \(tS\). Then \(|I| \le \mathrm{vol}(S)\, t^n \le |O|\).

theorem cube_measure_sandwich {n : ℕ} (S : Set (Fin n → ℝ))
    (hS : Bornology.IsBounded S) {t : ℝ} (ht : 0 < t) :
    (Nat.card (innerCubeSet S t) : ℝ) ≤ (volume S).toReal * t ^ n ∧
      (volume S).toReal * t ^ n ≤ (Nat.card (outerCubeSet S t) : ℝ)

Uses 8 · Used by 1

Statement usesInner cube set · Outer cube set

Proof usesFiniteness of the outer cube set · Inner cube indices are outer cube indices · Integer unit cube · Membership in the inner cube set · Membership in an integer unit cube · Membership in the outer cube set

Used byLattice-point error bound from boundary charts

DefinitionThe standard integer lattice#✓fully proved

For \(d \in \mathbb{N}\), the standard integer lattice \(\mathbb{Z}^d\) is the \(\mathbb{Z}\)-submodule of \(\mathbb{R}^d\) (the real-valued functions on \(\{0, \dots, d-1\}\)) spanned by the standard basis vectors \(e_0, \dots, e_{d-1}\).

noncomputable def stdLattice (d : ℕ) : Submodule ℤ (Fin d → ℝ) :=
  Submodule.span ℤ (Set.range (Pi.basisFun ℝ (Fin d)))

Used by 10

Used byThe Ehrhart function agrees with the lattice-point enumerator · Finiteness of the lattice points in a dilate · Finiteness of the lattice points in a translated dilate · The lattice-point count of the empty set vanishes · Lattice points in a dilate · Membership in the standard lattice · Integer points of a dilate · The translated lattice-point count of the empty set is zero · Translated lattice-point set · The origin is a lattice point

TheoremMembership in the standard lattice#✓fully proved

For a natural number \(d\), a vector \(x \in \mathbb{R}^d\) lies in the standard lattice \(\mathbb{Z}^d\), the integer span of the standard basis vectors of \(\mathbb{R}^d\), exactly when every coordinate \(x_i\) of \(x\) is an integer.

theorem mem_stdLattice_iff {d : ℕ} {x : Fin d → ℝ} :
    x ∈ stdLattice d ↔ ∀ i, ∃ z : ℤ, (z : ℝ) = x i

Uses 1 · Used by 2

Statement usesThe standard integer lattice

Used byThe Ehrhart function agrees with the lattice-point enumerator · Integer points of a dilate

DefinitionLattice points in a dilate#✓fully proved

For a natural number \(d\), a set \(P \subseteq \mathbb{R}^d\) and a real number \(t\), this is the set \((tP) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the dilate \(tP = \{tp : p \in P\}\).

The source only uses this set for \(t > 0\).

noncomputable def latticePointSet (d : ℕ) (P : Set (Fin d → ℝ)) (t : ℝ) :
    Set (Fin d → ℝ) :=
  (t • P) ∩ (stdLattice d : Set (Fin d → ℝ))

Uses 1 · Used by 7

Statement usesThe standard integer lattice

Used byThe Ehrhart function agrees with the lattice-point enumerator · Integer count of a dilate · Finiteness of the lattice points in a dilate · Lattice-point count of a real dilate · The lattice-point count of the empty set vanishes · Lattice points in a positive dilate · Integer points of a dilate

DefinitionLattice-point count of a real dilate#✓fully proved

For a natural number \(d\), a set \(P \subseteq \mathbb{R}^d\) and a real number \(t\), this is the number of elements of the set \((tP) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the dilate \(tP = \{tp : p \in P\}\), where an infinite set is assigned the value \(0\).

For unbounded \(P\) the set can be infinite, so the value \(0\) is a convention and not a count; the lattice-point enumerator for bounded \(P\) and \(t > 0\) is the faithful count.

noncomputable def latticeEnumerator (d : ℕ) (P : Set (Fin d → ℝ)) (t : ℝ) : ℕ :=
  Set.ncard (latticePointSet d P t)

Uses 1 · Used by 6

Statement usesLattice points in a dilate

Used byThe Ehrhart function agrees with the lattice-point enumerator · Integer count of a dilate · The lattice-point count of the empty set vanishes · Lattice-point enumerator · Lattice-point count of a dilate with boundary error · Lattice-point error bound from boundary charts

DefinitionTranslated lattice-point set#✓fully proved

For \(d \in \mathbb{N}\), a set \(P \subseteq \mathbb{R}^d\), a real \(t\) and \(x \in \mathbb{R}^d\), the translated lattice-point set is \(((t \cdot P) + x) \cap \mathbb{Z}^d\), the set of points of the standard integer lattice \(\mathbb{Z}^d\) in the dilate \(t \cdot P\) translated by \(x\).

The dilation comes first: in general this set differs from \((t \cdot (P + x)) \cap \mathbb{Z}^d\).

noncomputable def translatedLatticePointSet (d : ℕ) (P : Set (Fin d → ℝ))
    (t : ℝ) (x : Fin d → ℝ) : Set (Fin d → ℝ) :=
  ((t • P) + {x}) ∩ (stdLattice d : Set (Fin d → ℝ))

Sources

• Rocha-Neves, arXiv:2608.11078v1, lines 62-67.

Uses 1 · Used by 4

Statement usesThe standard integer lattice

Used byFiniteness of the lattice points in a translated dilate · Translated lattice-point count for arbitrary sets · The translated lattice-point count of the empty set is zero · Translated lattice-point set at a positive dilation

DefinitionTranslated lattice-point count for arbitrary sets#✓fully proved

For \(d \in \mathbb{N}\), a set \(P \subseteq \mathbb{R}^d\), a real \(t\) and \(x \in \mathbb{R}^d\), the translated lattice-point count is the number of elements of the translated lattice-point set \(((t \cdot P) + x) \cap \mathbb{Z}^d\), taken to be \(0\) when this set is infinite.

noncomputable def translatedLatticeEnumerator (d : ℕ) (P : Set (Fin d → ℝ))
    (t : ℝ) (x : Fin d → ℝ) : ℕ :=
  Set.ncard (translatedLatticePointSet d P t x)

Uses 1 · Used by 2

Statement usesTranslated lattice-point set

Used byThe translated lattice-point count of the empty set is zero · Translated lattice-point enumerator of a bounded set

DefinitionLattice points in a positive dilate#✓fully proved

For a natural number \(d\), a set \(P \subseteq \mathbb{R}^d\) and a real number \(t > 0\), this is the set \((tP) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the dilate \(tP = \{tp : p \in P\}\).

No boundedness of \(P\) is assumed.

noncomputable def latticePointSetPos (d : ℕ) (P : Set (Fin d → ℝ))
    (t : {t : ℝ // 0 < t}) : Set (Fin d → ℝ) :=
  latticePointSet d P t.val

Uses 1 · Used by 1

Statement usesLattice points in a dilate

Used byFiniteness of the lattice points in a positive dilate

DefinitionLattice-point enumerator#✓fully proved

For a natural number \(d\), a bounded set \(P \subseteq \mathbb{R}^d\) and a real number \(t > 0\), the lattice-point enumerator \(L_P(t)\) is the number of points of the integer lattice \(\mathbb{Z}^d\) in the dilate \(tP = \{tp : p \in P\}\), that is, \(L_P(t) = |(tP) \cap \mathbb{Z}^d|\).

Since \(P\) is bounded, the set \((tP) \cap \mathbb{Z}^d\) is finite, so \(L_P(t)\) is its actual number of elements.

noncomputable def latticeEnumeratorPos (d : ℕ) (P : Set (Fin d → ℝ))
    (_hb : Bornology.IsBounded P) (t : {t : ℝ // 0 < t}) : ℕ :=
  latticeEnumerator d P t.val

Sources

• Rocha-Neves, A Fourier-analytic Uniqueness Theorem for Lattice-point Enumerators, arXiv:2608.11078v1, lines 24-31.

Uses 1

Statement usesLattice-point count of a real dilate

DefinitionTranslated lattice-point set at a positive dilation#✓fully proved

For \(d \in \mathbb{N}\), a set \(P \subseteq \mathbb{R}^d\), a real \(t > 0\) and \(x \in \mathbb{R}^d\), this is the set \(((t \cdot P) + x) \cap \mathbb{Z}^d\) of points of the standard integer lattice \(\mathbb{Z}^d\) in the dilate \(t \cdot P\) translated by \(x\). No boundedness of \(P\) is assumed.

noncomputable def translatedLatticePointSetPos (d : ℕ) (P : Set (Fin d → ℝ))
    (t : {t : ℝ // 0 < t}) (x : Fin d → ℝ) : Set (Fin d → ℝ) :=
  translatedLatticePointSet d P t.val x

Uses 1 · Used by 1

Statement usesTranslated lattice-point set

Used byFiniteness of the lattice points in a translated positive dilate

DefinitionTranslated lattice-point enumerator of a bounded set#✓fully proved

Let \(d \in \mathbb{N}\), let \(P \subseteq \mathbb{R}^d\) be a bounded set, let \(t > 0\) be real and let \(x \in \mathbb{R}^d\). The translated lattice-point enumerator is \(F_{t,P}(x) = |((t \cdot P) + x) \cap \mathbb{Z}^d|\), the number of points of the standard integer lattice \(\mathbb{Z}^d\) in the dilate \(t \cdot P\) translated by \(x\).

noncomputable def translatedLatticeEnumeratorPos (d : ℕ) (P : Set (Fin d → ℝ))
    (_hb : Bornology.IsBounded P) (t : {t : ℝ // 0 < t}) (x : Fin d → ℝ) : ℕ :=
  translatedLatticeEnumerator d P t.val x

Sources

• Rocha-Neves, arXiv:2608.11078v1, lines 62-67.

Uses 1

Statement usesTranslated lattice-point count for arbitrary sets

TheoremThe origin is a lattice point#✓fully proved

For every \(d \in \mathbb{N}\), the origin of \(\mathbb{R}^d\) lies in the standard integer lattice \(\mathbb{Z}^d\).

theorem zero_mem_stdLattice (d : ℕ) : (0 : Fin d → ℝ) ∈ stdLattice d

Uses 1

Statement usesThe standard integer lattice

TheoremThe lattice-point count of the empty set vanishes#✓fully proved

For every natural number \(d\) and every real number \(t\), the lattice-point count of the empty set \(\emptyset \subseteq \mathbb{R}^d\) at the dilate \(t\) is \(0\).

@[simp]
theorem latticeEnumerator_empty (d : ℕ) (t : ℝ) :
    latticeEnumerator d ∅ t = 0

Uses 3

Statement usesLattice-point count of a real dilate

Proof usesLattice points in a dilate · The standard integer lattice

TheoremThe translated lattice-point count of the empty set is zero#✓fully proved

For every \(d \in \mathbb{N}\), every real \(t\) and every \(x \in \mathbb{R}^d\), the translated lattice-point count \(|((t \cdot \emptyset) + x) \cap \mathbb{Z}^d|\) is \(0\).

@[simp]
theorem translatedLatticeEnumerator_empty (d : ℕ) (t : ℝ) (x : Fin d → ℝ) :
    translatedLatticeEnumerator d ∅ t x = 0

Uses 3

Statement usesTranslated lattice-point count for arbitrary sets

Proof usesThe standard integer lattice · Translated lattice-point set

TheoremFiniteness of the lattice points in a dilate#✓fully proved

For a natural number \(d\), a bounded set \(P \subseteq \mathbb{R}^d\) and any real number \(t\), the set \((tP) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the dilate \(tP = \{tp : p \in P\}\) is finite.

No positivity of \(t\) is needed.

theorem finite_latticePointSet (d : ℕ) (P : Set (Fin d → ℝ)) (t : ℝ)
    (hb : Bornology.IsBounded P) :
    Set.Finite (latticePointSet d P t)

Uses 2 · Used by 1

Statement usesLattice points in a dilate

Proof usesThe standard integer lattice

Used byFiniteness of the lattice points in a positive dilate

TheoremFiniteness of the lattice points in a positive dilate#✓fully proved

For a natural number \(d\), a bounded set \(P \subseteq \mathbb{R}^d\) and a real number \(t > 0\), the set \((tP) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the dilate \(tP = \{tp : p \in P\}\) is finite.

theorem finite_latticePointSetPos (d : ℕ) (P : Set (Fin d → ℝ))
    (t : {t : ℝ // 0 < t}) (hb : Bornology.IsBounded P) :
    Set.Finite (latticePointSetPos d P t)

Uses 2

Statement usesLattice points in a positive dilate

Proof usesFiniteness of the lattice points in a dilate

TheoremFiniteness of the lattice points in a translated dilate#✓fully proved

For a natural number \(d\), a bounded set \(P \subseteq \mathbb{R}^d\), any real number \(t\) and a vector \(x \in \mathbb{R}^d\), the set \((tP + x) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the translated dilate \(tP + x = \{tp + x : p \in P\}\) is finite.

theorem finite_translatedLatticePointSet (d : ℕ) (P : Set (Fin d → ℝ))
    (t : ℝ) (x : Fin d → ℝ) (hb : Bornology.IsBounded P) :
    Set.Finite (translatedLatticePointSet d P t x)

Uses 2 · Used by 1

Statement usesTranslated lattice-point set

Proof usesThe standard integer lattice

Used byFiniteness of the lattice points in a translated positive dilate

TheoremFiniteness of the lattice points in a translated positive dilate#✓fully proved

For a natural number \(d\), a bounded set \(P \subseteq \mathbb{R}^d\), a real number \(t > 0\) and a vector \(x \in \mathbb{R}^d\), the set \((tP + x) \cap \mathbb{Z}^d\) of points of the integer lattice \(\mathbb{Z}^d\) in the translated dilate \(tP + x = \{tp + x : p \in P\}\) is finite.

theorem finite_translatedLatticePointSetPos (d : ℕ) (P : Set (Fin d → ℝ))
    (t : {t : ℝ // 0 < t}) (x : Fin d → ℝ) (hb : Bornology.IsBounded P) :
    Set.Finite (translatedLatticePointSetPos d P t x)

Uses 2

Statement usesTranslated lattice-point set at a positive dilation

Proof usesFiniteness of the lattice points in a translated dilate

DefinitionThe unit cube#✓fully proved

For a natural number \(d\), the closed unit cube \([0, 1]^d\) is the set of points \(x \in \mathbb{R}^d\) with \(0 \le x_i \le 1\) for every coordinate \(i\).

def unitCube (d : ℕ) : Set (Fin d → ℝ) :=
  Set.Icc 0 1

Used by 16

Used byCounting integer cubes met by a dilated Lipschitz image · Counting outer cubes by inner cubes and boundary charts · Dilated Lipschitz images meet \(O(t^d)\) integer cubes · Dilated Lipschitz images meet finitely many integer cubes · Lipschitz images of Lipschitz parametrizable sets · Integer cube set · Lipschitz parametrizable sets · Finsets are Lipschitz parametrizable · The empty set is Lipschitz parametrizable · Singletons are Lipschitz parametrizable · Lattice-point count of a dilate with boundary error · Lattice-point error bound from boundary charts · Membership in the integer cube set · Boundary cubes meet the dilated frontier charts · Dilated Lipschitz maps vary by at most \(K\) on cells of size \(1/T\) · The origin lies in the unit cube

DefinitionLipschitz parametrizable sets#✓fully proved

Let \(X\) be a metric space and \(d\) a natural number. A set \(B \subseteq X\) is \(d\)-Lipschitz parametrizable if there are a natural number \(n\) (possibly \(0\)) and Lipschitz maps \(f_1, \dots, f_n : [0, 1]^d \to X\) out of the closed unit cube \([0, 1]^d \subseteq \mathbb{R}^d\) such that \(B\) equals the union of their images, \(B = f_1([0, 1]^d) \cup \dots \cup f_n([0, 1]^d)\).

def IsLipschitzParametrizable {X : Type*} [MetricSpace X] (d : ℕ) (B : Set X) : Prop :=
  ∃ (n : ℕ) (f : Fin n → (↥(unitCube d) → X)),
    (∀ i, ∃ K : NNReal, LipschitzWith K (f i)) ∧ B = ⋃ i, Set.range (f i)

Uses 1 · Used by 6

Statement usesThe unit cube

Used byLipschitz images of Lipschitz parametrizable sets · Finite sets are Lipschitz parametrizable · Finsets are Lipschitz parametrizable · The empty set is Lipschitz parametrizable · Singletons are Lipschitz parametrizable · Lattice-point count of a dilate with boundary error

TheoremThe origin lies in the unit cube#✓fully proved

For every natural number \(d\), the origin of \(\mathbb{R}^d\) lies in the closed unit cube \([0, 1]^d\).

theorem unitCube_zero_mem (d : ℕ) : (0 : Fin d → ℝ) ∈ unitCube d

Uses 1 · Used by 3

Statement usesThe unit cube

Used byDilated Lipschitz images meet finitely many integer cubes · Finsets are Lipschitz parametrizable · Singletons are Lipschitz parametrizable

TheoremThe empty set is Lipschitz parametrizable#✓fully proved

Let \(X\) be a metric space. For every natural number \(d\), the empty subset of \(X\) is \(d\)-Lipschitz parametrizable, via the empty family of maps.

theorem isLipschitzParametrizable_empty {X : Type*} [MetricSpace X] (d : ℕ) :
    IsLipschitzParametrizable d (∅ : Set X)

Uses 2

Statement usesLipschitz parametrizable sets

Proof usesThe unit cube

TheoremSingletons are Lipschitz parametrizable#✓fully proved

Let \(X\) be a metric space. For every natural number \(d\) and every point \(x \in X\), the set \(\lbrace x \rbrace\) is \(d\)-Lipschitz parametrizable, via a single constant map.

theorem isLipschitzParametrizable_singleton {X : Type*} [MetricSpace X] (d : ℕ)
    (x : X) : IsLipschitzParametrizable d ({x} : Set X)

Uses 3

Statement usesLipschitz parametrizable sets

Proof usesThe unit cube · The origin lies in the unit cube

TheoremFinsets are Lipschitz parametrizable#✓fully proved

Let \(X\) be a metric space and \(d\) a natural number. Every finite set \(s\) of points of \(X\), given as a finset, is \(d\)-Lipschitz parametrizable.

theorem isLipschitzParametrizable_coe {X : Type*} [MetricSpace X] (d : ℕ)
    (s : Finset X) : IsLipschitzParametrizable d (↑s : Set X)

Uses 3 · Used by 1

Statement usesLipschitz parametrizable sets

Proof usesThe unit cube · The origin lies in the unit cube

Used byFinite sets are Lipschitz parametrizable

TheoremFinite sets are Lipschitz parametrizable#✓fully proved

Let \(X\) be a metric space. Every finite set \(B \subseteq X\) is \(d\)-Lipschitz parametrizable for every natural number \(d\).

theorem Finite.isLipschitzParametrizable {X : Type*} [MetricSpace X] {B : Set X}
    (hB : B.Finite) (d : ℕ) : IsLipschitzParametrizable d B

Uses 2

Statement usesLipschitz parametrizable sets

Proof usesFinsets are Lipschitz parametrizable

TheoremLipschitz images of Lipschitz parametrizable sets#✓fully proved

Let \(X\) and \(Y\) be metric spaces, let \(d\) be a natural number and let \(f : X \to Y\) be a Lipschitz map. If a set \(B \subseteq X\) is \(d\)-Lipschitz parametrizable, then its image \(f(B) \subseteq Y\) is \(d\)-Lipschitz parametrizable.

theorem IsLipschitzParametrizable.image_lipschitzWith {X Y : Type*}
    [MetricSpace X] [MetricSpace Y] {d : ℕ} {B : Set X}
    (hB : IsLipschitzParametrizable d B) {f : X → Y} {K : NNReal}
    (hf : LipschitzWith K f) : IsLipschitzParametrizable d (f '' B)

Uses 2

Statement usesLipschitz parametrizable sets

Proof usesThe unit cube

DefinitionInteger cube set#✓fully proved

Let \(f\) be a map from the unit cube \([0, 1]^d\) to \(\mathbb{R}^n\) and let \(t\) be a real number. The integer cube set of \(f\) at scale \(t\) is the set of integer vectors \(v \in \mathbb{Z}^n\) for which some point \(y\) of the unit cube satisfies \(v_i \le t f(y)_i < v_i + 1\) for every coordinate \(i\), that is, the set of integer vectors whose half-open unit cube \(\prod_i [v_i, v_i + 1)\) meets the dilate \(t \cdot f([0, 1]^d)\).

def integerCubeSet {n d : ℕ} (f : ↥(unitCube d) → (Fin n → ℝ)) (t : ℝ) :
    Set (Fin n → ℤ) :=
  {v | ∃ y : ↥(unitCube d),
    ∀ i, (v i : ℝ) ≤ t * (f y) i ∧ t * (f y) i < (v i : ℝ) + 1}

Uses 1 · Used by 8

Statement usesThe unit cube

Used byCounting integer cubes met by a dilated Lipschitz image · Counting outer cubes by inner cubes and boundary charts · Dilated Lipschitz images meet \(O(t^d)\) integer cubes · Dilated Lipschitz images meet finitely many integer cubes · Lattice-point count of a dilate with boundary error · Lattice-point error bound from boundary charts · Membership in the integer cube set · Boundary cubes meet the dilated frontier charts

TheoremMembership in the integer cube set#✓fully proved

Let \(f\) be a map from the unit cube \([0, 1]^d\) to \(\mathbb{R}^n\), let \(t\) be a real number and let \(v \in \mathbb{Z}^n\). Then \(v\) belongs to the integer cube set of \(f\) at scale \(t\) if and only if some point \(y\) of the unit cube satisfies \(v_i \le t f(y)_i < v_i + 1\) for every coordinate \(i\).

theorem mem_integerCubeSet_iff {n d : ℕ} {f : ↥(unitCube d) → (Fin n → ℝ)}
    {t : ℝ} {v : Fin n → ℤ} :
    v ∈ integerCubeSet f t ↔ ∃ y : ↥(unitCube d),
      ∀ i, (v i : ℝ) ≤ t * (f y) i ∧ t * (f y) i < (v i : ℝ) + 1

Uses 2 · Used by 2

Statement usesInteger cube set · The unit cube

Used byCounting integer cubes met by a dilated Lipschitz image · Dilated Lipschitz images meet finitely many integer cubes

TheoremFloor differences are bounded by a ceiling#✓fully proved

For real numbers \(a\), \(b\) and \(D\) with \(|a - b| \le D\), the integers \(\lfloor a \rfloor\) and \(\lfloor b \rfloor\) satisfy \(|\lfloor a \rfloor - \lfloor b \rfloor| \le \lceil D \rceil\).

theorem abs_floor_sub_le_ceil {a b D : ℝ} (hab : |a - b| ≤ D) :
    |⌊a⌋ - ⌊b⌋| ≤ ⌈D⌉

Used by 1

Used byCounting integer cubes met by a dilated Lipschitz image

TheoremDilated Lipschitz maps vary by at most \(K\) on cells of size \(1/T\)#✓fully proved

Let \(K \ge 0\), let \(f\) be a \(K\)-Lipschitz map from the unit cube \([0, 1]^d\) to \(\mathbb{R}^n\), both carrying the sup distance, and let \(t\) and \(T\) be real numbers with \(0 < t \le T\). If \(y\) and \(y'\) are points of the unit cube at distance at most \(1/T\), then \(|t f(y)_i - t f(y')_i| \le K\) for every coordinate \(i\).

theorem scaled_coord_abs_le {n d : ℕ} {f : ↥(unitCube d) → (Fin n → ℝ)}
    {K : ℝ≥0} (hf : LipschitzWith K f) {y y' : ↥(unitCube d)}
    {t T : ℝ} (ht_pos : 0 < t) (hT_pos : 0 < T) (ht_le : t ≤ T)
    (hdist : dist y y' ≤ 1 / T) (i : Fin n) :
    |t * (f y) i - t * (f y') i| ≤ (K : ℝ)

Uses 1 · Used by 1

Statement usesThe unit cube

Used byCounting integer cubes met by a dilated Lipschitz image

TheoremCounting integer cubes met by a dilated Lipschitz image#✓fully proved

Let \(d\) and \(n\) be natural numbers, let \(K \ge 0\), and let \(f\) be a \(K\)-Lipschitz map from the unit cube \([0, 1]^d\) to \(\mathbb{R}^n\), both carrying the sup distance. For every real \(t \ge 1\), the cardinality of the integer cube set of \(f\) at scale \(t\), taken as a natural number, is at most \(\lceil t \rceil^d \, (2 \lceil K \sqrt{d} \rceil + 3)^n\).

The proof puts \(T = \lceil t \rceil\), partitions the cube into \(T^d\) cells with lower-corner representatives, bounds every floor-coordinate offset from the representative by \(L = \lceil K \sqrt{d} \rceil\), and encodes each met integer cube injectively by its cell and an offset in \(\{0, \dots, 2L + 2\}^n\).

theorem card_integerCubeSet_le {n d : ℕ} (f : ↥(unitCube d) → (Fin n → ℝ))
    (K : ℝ≥0) (hf : LipschitzWith K f) (t : ℝ) (ht : 1 ≤ t) :
    Nat.card (integerCubeSet f t) ≤
      ⌈t⌉₊ ^ d * (2 * ⌈(K : ℝ) * Real.sqrt d⌉₊ + 3) ^ n

Uses 5 · Used by 1

Statement usesInteger cube set · The unit cube

Proof usesFloor differences are bounded by a ceiling · Membership in the integer cube set · Dilated Lipschitz maps vary by at most \(K\) on cells of size \(1/T\)

Used byDilated Lipschitz images meet \(O(t^d)\) integer cubes

TheoremDilated Lipschitz images meet finitely many integer cubes#✓fully proved

Let \(d\) and \(n\) be natural numbers, let \(K \ge 0\), and let \(f\) be a \(K\)-Lipschitz map from the unit cube \([0, 1]^d\) to \(\mathbb{R}^n\), both carrying the sup distance. For every real \(t \ge 1\), the integer cube set of \(f\) at scale \(t\) is finite.

The image of \(f\) is bounded, since each coordinate of \(f(y)\) differs from the corresponding coordinate of \(f(0)\) by at most \(K \sqrt{d}\), so every met cube index lies in an explicit finite box.

theorem finite_integerCubeSet {n d : ℕ} (f : ↥(unitCube d) → (Fin n → ℝ))
    (K : ℝ≥0) (hf : LipschitzWith K f) (t : ℝ) (ht : 1 ≤ t) :
    (integerCubeSet f t).Finite

Uses 4 · Used by 1

Statement usesInteger cube set · The unit cube

Proof usesMembership in the integer cube set · The origin lies in the unit cube

Used byLattice-point count of a dilate with boundary error

TheoremDilated Lipschitz images meet \(O(t^d)\) integer cubes#✓fully proved

Let \(d\) and \(n\) be natural numbers, let \(K \ge 0\), and let \(f\) be a \(K\)-Lipschitz map from the unit cube \([0, 1]^d\) to \(\mathbb{R}^n\), both carrying the sup distance. Then there is a real number \(C > 0\) such that for every real \(t \ge 1\), the cardinality of the integer cube set of \(f\) at scale \(t\), taken as a natural number, is at most \(C t^d\).

The proof takes \(C = 2^d M^n\) with \(M = 2 \lceil K \sqrt{d} \rceil + 3\), which depends on \(f\) only through \(K\), and on \(n\) and \(d\), but not on \(t\); it uses \(\lceil t \rceil \le 2t\) for \(t \ge 1\).

theorem exists_cubeCount_le_const_mul_pow {n d : ℕ}
    (f : ↥(unitCube d) → (Fin n → ℝ)) (K : ℝ≥0) (hf : LipschitzWith K f) :
    ∃ C : ℝ, 0 < C ∧ ∀ t : ℝ, 1 ≤ t →
      (Nat.card (integerCubeSet f t) : ℝ) ≤ C * t ^ d

Uses 3 · Used by 1

Statement usesInteger cube set · The unit cube

Proof usesCounting integer cubes met by a dilated Lipschitz image

Used byLattice-point count of a dilate with boundary error

TheoremBoundary cubes meet the dilated frontier charts#✓fully proved

Let \(S \subseteq \mathbb{R}^n\), let \(f_1, \dots, f_m : [0,1]^d \to \mathbb{R}^n\) be maps whose ranges together cover the frontier of \(S\), and let \(t\) be a real number. For \(v \in \mathbb{Z}^n\) write \(Q_v\) for the half-open unit cube \(\prod_i [v_i, v_i + 1)\). If \(v\) lies in the outer cube set of \(S\) at scale \(t\) (some \(x \in Q_v\) has \(x / t \in S\), coordinatewise, with \(x / 0 = 0\)) but not in the inner cube set (not every \(x \in Q_v\) has \(x / t \in S\)), then \(v\) lies in the integer cube set of some \(f_i\) at scale \(t\): there is \(y \in [0,1]^d\) with \(t f_i(y) \in Q_v\).

theorem outer_diff_inner_subset_iUnion_integerCubeSet
    {n d numMaps : ℕ} (S : Set (Fin n → ℝ))
    (maps : Fin numMaps → (↥(unitCube d) → (Fin n → ℝ)))
    (hCover : frontier S ⊆ ⋃ i, Set.range (maps i))
    {t : ℝ} :
    outerCubeSet S t \ innerCubeSet S t ⊆
      ⋃ i, integerCubeSet (maps i) t

Uses 9 · Used by 1

Statement usesInner cube set · Outer cube set · Integer cube set · The unit cube

Proof usesA preconnected set meets the frontier of every set it crosses · Integer unit cube · Membership in the inner cube set · Membership in an integer unit cube · Membership in the outer cube set

Used byCounting outer cubes by inner cubes and boundary charts

TheoremCounting outer cubes by inner cubes and boundary charts#✓fully proved

Let \(S \subseteq \mathbb{R}^n\), let \(f_1, \dots, f_m : [0,1]^d \to \mathbb{R}^n\) be maps whose ranges together cover the frontier of \(S\), and let \(t\) be a real number. Let \(O\) and \(I\) be the outer and inner cube sets of \(S\) at scale \(t\): the \(v \in \mathbb{Z}^n\) for which some, respectively every, point \(x\) of the half-open unit cube \(\prod_i [v_i, v_i + 1)\) has \(x / t \in S\) (coordinatewise, with \(x / 0 = 0\)). Let \(C_i\) be the integer cube set of \(f_i\) at scale \(t\): the \(v\) whose half-open unit cube contains \(t f_i(y)\) for some \(y \in [0,1]^d\). If \(O\) and every \(C_i\) are finite, then \(|O| \le |I| + \sum_{i=1}^m |C_i|\).

theorem card_outer_le_card_inner_add_sum
    {n d numMaps : ℕ} (S : Set (Fin n → ℝ))
    (maps : Fin numMaps → (↥(unitCube d) → (Fin n → ℝ)))
    (hCover : frontier S ⊆ ⋃ i, Set.range (maps i))
    {t : ℝ}
    (hFinOuter : (outerCubeSet S t).Finite)
    (hFinMaps : ∀ i, (integerCubeSet (maps i) t).Finite) :
    Nat.card (outerCubeSet S t) ≤
      Nat.card (innerCubeSet S t) +
        ∑ i, Nat.card (integerCubeSet (maps i) t)

Uses 6 · Used by 1

Statement usesInner cube set · Outer cube set · Integer cube set · The unit cube

Proof usesBoundary cubes meet the dilated frontier charts · Inner cube indices are outer cube indices

Used byLattice-point error bound from boundary charts

DefinitionInteger points of a dilate#✓fully proved

Let \(S \subseteq \mathbb{R}^n\) and \(t > 0\). Viewing an integer vector as a real vector gives a bijection from the set of \(x \in \mathbb{Z}^n\) with \(x / t \in S\) onto the lattice point set \(tS \cap \mathbb{Z}^n\).

LatticePointAsymptotics.rawSubtypeEquivCanonicalPointSet · 50 lines

noncomputable def rawSubtypeEquivCanonicalPointSet {n : ℕ}
    (S : Set (Fin n → ℝ)) {t : ℝ} (ht : 0 < t) :
    {x : Fin n → ℤ | (fun i => (x i : ℝ) / t) ∈ S} ≃
      ↥(LatticePointEnumerator.latticePointSet n S t) :=
  Equiv.ofBijective
    (fun x => ⟨fun i => ((x.val i : ℤ) : ℝ), by
      have htne : t ≠ 0 := ht.ne'
      have hmemDil : (fun i => ((x.val i : ℤ) : ℝ)) ∈ t • S :=
        ⟨(fun i => ((x.val i : ℤ) : ℝ) / t), x.property, by
          funext i
          simp only [Pi.smul_apply, smul_eq_mul]
          exact mul_div_cancel₀ _ htne⟩
      have hmemLat : (fun i => ((x.val i : ℤ) : ℝ)) ∈
          LatticePointEnumerator.stdLattice n := by
        show _ ∈ LatticePointEnumerator.stdLattice n
        rw [LatticePointEnumerator.mem_stdLattice_iff]
        exact fun i => ⟨x.val i, rfl⟩
      exact ⟨hmemDil, hmemLat⟩⟩)
    ⟨by
      intro a b hab
      apply Subtype.ext
      funext i
      have h := congrArg Subtype.val hab
      have hi : ((a.val i : ℤ) : ℝ) = ((b.val i : ℤ) : ℝ) := congrFun h i
      exact Int.cast_injective hi,
    by
      intro y
      obtain ⟨hmemDil, hmemLat⟩ := y.property
      have hInt' : ∀ i, ∃ z : ℤ, (z : ℝ) = y.val i := by
        show ∀ i, ∃ z : ℤ, (z : ℝ) = y.val i
        exact LatticePointEnumerator.mem_stdLattice_iff.mp hmemLat
      choose z hz using hInt'
      have htne : t ≠ 0 := ht.ne'
      obtain ⟨s, hsS, hsEq⟩ := hmemDil
      have hmem : (fun i => ((z i : ℤ) : ℝ) / t) ∈ S := by
        have hEq : (fun i => ((z i : ℤ) : ℝ) / t) = s := by
          funext i
          have hyi : y.val i = t * s i := by
            have h := congrFun hsEq i
            simp only [Pi.smul_apply, smul_eq_mul] at h
            rw [h]
          rw [hz i, hyi]
          field_simp
        rw [hEq]
        exact hsS
      refine ⟨⟨z, hmem⟩, ?_⟩
      apply Subtype.ext
      funext i
      change ((z i : ℤ) : ℝ) = y.val i
      exact hz i⟩

Uses 3 · Used by 1

Statement usesLattice points in a dilate · Membership in the standard lattice · The standard integer lattice

Used byInteger count of a dilate

TheoremInteger count of a dilate#✓fully proved

Let \(S \subseteq \mathbb{R}^n\) and \(t > 0\). The number of integer vectors \(x \in \mathbb{Z}^n\) with \(x / t \in S\) equals the lattice enumerator of \(S\) at \(t\), the number of points of \(\mathbb{Z}^n\) in the dilate \(tS\); here an infinite set is counted as \(0\).

theorem card_raw_eq_latticeEnumerator {n : ℕ} (S : Set (Fin n → ℝ))
    {t : ℝ} (ht : 0 < t) :
    Nat.card {x : Fin n → ℤ | (fun i => (x i : ℝ) / t) ∈ S} =
      LatticePointEnumerator.latticeEnumerator n S t

Uses 3 · Used by 1

Statement usesLattice-point count of a real dilate

Proof usesInteger points of a dilate · Lattice points in a dilate

Used byLattice-point error bound from boundary charts

TheoremLattice-point error bound from boundary charts#✓fully proved

Let \(S \subseteq \mathbb{R}^n\) be bounded, let \(f_1, \dots, f_m\) be maps from the unit cube \([0,1]^d\) to \(\mathbb{R}^n\) whose ranges cover the boundary \(\partial S\), and let \(t > 0\). For each \(i\), let \(N_i(t)\) be the number of \(v \in \mathbb{Z}^n\) such that \(t f_i(y)\) lies in the half-open cube \(\prod_j [v_j, v_j + 1)\) for some \(y \in [0,1]^d\), and assume each of these sets of \(v\) is finite. Then the lattice enumerator \(L_S(t)\), the number of points of \(\mathbb{Z}^n\) in \(tS\), satisfies \(|L_S(t) - \operatorname{vol}(S)\, t^n| \le N_1(t) + \dots + N_m(t)\), where \(\operatorname{vol}\) is Lebesgue (outer) measure.

theorem lattice_point_count_error_bound
    {n d numMaps : ℕ} (S : Set (Fin n → ℝ))
    (hS : Bornology.IsBounded S)
    (maps : Fin numMaps → (↥(unitCube d) → (Fin n → ℝ)))
    (hCover : frontier S ⊆ ⋃ i, Set.range (maps i))
    {t : ℝ} (ht : 0 < t)
    (hFinMaps : ∀ i, (integerCubeSet (maps i) t).Finite) :
    ‖(LatticePointEnumerator.latticeEnumerator n S t : ℝ) -
      (MeasureTheory.volume S).toReal * t ^ n‖ ≤
      ∑ i, (Nat.card (integerCubeSet (maps i) t) : ℝ)

Uses 13 · Used by 1

Statement usesLattice-point count of a real dilate · Integer cube set · The unit cube

Proof usesInteger count of a dilate · Counting outer cubes by inner cubes and boundary charts · Cubical measure sandwich · Finiteness of the outer cube set · Inner cube set · Integer unit cube · Membership in the inner cube set · Membership in an integer unit cube · Membership in the outer cube set · Outer cube set

Used byLattice-point count of a dilate with boundary error

TheoremLattice-point count of a dilate with boundary error#✓fully proved

Let \(S \subseteq \mathbb{R}^n\) be bounded, and suppose its boundary \(\partial S\) is \((n-1)\)-Lipschitz parametrizable: it is the union of the ranges of finitely many Lipschitz maps from the unit cube \([0,1]^{n-1}\), where \(n - 1\) is read as \(0\) when \(n = 0\). Then there is a real constant \(C\) such that for all sufficiently large real \(t\), the lattice enumerator \(L_S(t)\), the number of points of \(\mathbb{Z}^n\) in \(tS\), satisfies \(|L_S(t) - \operatorname{vol}(S)\, t^n| \le C\, t^{n-1}\), where \(\operatorname{vol}\) is Lebesgue (outer) measure.

theorem lattice_point_count_asymptotics
    {n : ℕ} (S : Set (Fin n → ℝ))
    (hS : Bornology.IsBounded S)
    (hS_bdry : IsLipschitzParametrizable (n - 1) (frontier S)) :
    ∃ C : ℝ, ∀ᶠ t in Filter.atTop,
      ‖(LatticePointEnumerator.latticeEnumerator n S t : ℝ) -
        (MeasureTheory.volume S).toReal * t ^ n‖ ≤ C * t ^ (n - 1)

Uses 7

Statement usesLipschitz parametrizable sets · Lattice-point count of a real dilate

Proof usesLattice-point error bound from boundary charts · Dilated Lipschitz images meet \(O(t^d)\) integer cubes · Dilated Lipschitz images meet finitely many integer cubes · Integer cube set · The unit cube

47 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.