Delone sets

A Delone set D ⊆ X in a metric space is a set which is both:

• Uniformly Discrete: there exists packingRadius > 0 such that distinct points of D are separated by a distance strictly greater than packingRadius;
• Relatively Dense: there exists coveringRadius > 0 such that every point of X lies within distance coveringRadius of some point of D.

The DeloneSet structure stores the set together with explicit radii witnessing these properties. The definitions use metric entourages so that the theory fits naturally into the uniformity framework.

Delone sets appear in discrete geometry, crystallography, aperiodic order, and tiling theory.

Main definitions

• Delone.DeloneSet X: The main structure representing a Delone set in a metric space X.
• DeloneSet.mapBilipschitz: Transports a Delone set along a bilipschitz equivalence, scaling the radii.
• DeloneSet.mapIsometry Preserves the packing and covering radii exactly.

Basic properties

• packingRadius_lt_dist_of_mem_ne : Distinct points in a Delone set are further apart than the packing radius.
• exists_dist_le_coveringRadius : Every point of the space lies within the covering radius of the set.
• subset_ball_singleton : Any ball of sufficiently small radius contains at most one point of the set.

Implementation notes

• Bundled Structure: DeloneSet is bundled as a structure rather than a predicate (e.g., IsDelone). This facilitates dynamical systems constructions like hulls and patches by ensuring operations automatically preserve the required properties, eliminating the need to manually pass around proofs that the set remains Delone.
• Explicit Data: Since radii are stored as explicit data, the map from DeloneSet X to Set X is not injective. We provide a Membership instance and mem_carrier to allow the convenience of ∈ notation while ensuring radii remain bundled, computationally accessible, and tracked by extensionality.

structure Delone.DeloneSet (X : Type u_3) [MetricSpace X] : Type u_3

A Delone set consists of a set together with explicit radii witnessing uniform discreteness and relative denseness.

• carrier : Set X

  The underlying set.

• packingRadius : NNReal

  Radius such that distinct points of carrier are separated by more than r.

• packingRadius_pos : 0 < self.packingRadius
• isSeparated_packingRadius : Metric.IsSeparated (↑self.packingRadius) self.carrier
• coveringRadius : NNReal

  Radius such that every point of the space is within R of carrier.

• coveringRadius_pos : 0 < self.coveringRadius
• isCover_coveringRadius : Metric.IsCover self.coveringRadius Set.univ self.carrier

theorem Delone.DeloneSet.ext {X : Type u_3} {inst✝ : MetricSpace X} {x y : DeloneSet X} (carrier : x.carrier = y.carrier) (packingRadius : x.packingRadius = y.packingRadius) (coveringRadius : x.coveringRadius = y.coveringRadius) : x = y

theorem Delone.DeloneSet.ext_iff {X : Type u_3} {inst✝ : MetricSpace X} {x y : DeloneSet X} : x = y ↔ x.carrier = y.carrier ∧ x.packingRadius = y.packingRadius ∧ x.coveringRadius = y.coveringRadius

def Delone.DeloneSet.toSet {X : Type u_1} [MetricSpace X] (D : DeloneSet X) : Set X

The underlying set of points of a Delone set.

instance Delone.DeloneSet.instCoeSet {X : Type u_1} [MetricSpace X] : Coe (DeloneSet X) (Set X)

instance Delone.DeloneSet.instMembership {X : Type u_1} [MetricSpace X] : Membership X (DeloneSet X)

@[simp]

theorem Delone.DeloneSet.mem_coe {X : Type u_1} [MetricSpace X] {D : DeloneSet X} {x : X} : x ∈ ↑D ↔ x ∈ D

@[simp]

theorem Delone.DeloneSet.mem_carrier {X : Type u_1} [MetricSpace X] {D : DeloneSet X} {x : X} : x ∈ D.carrier ↔ x ∈ D

theorem Delone.DeloneSet.nonempty {X : Type u_1} [MetricSpace X] [Nonempty X] (D : DeloneSet X) : (↑D).Nonempty

def Delone.DeloneSet.copy {X : Type u_1} [MetricSpace X] (D : DeloneSet X) (carrier : Set X) (packingRadius coveringRadius : NNReal) (h_carrier : carrier = D.carrier) (h_packing : packingRadius = D.packingRadius) (h_covering : coveringRadius = D.coveringRadius) : DeloneSet X

Copy of a Delone set with new fields equal to the old ones. Useful to fix definitional equalities.

theorem Delone.DeloneSet.copy_eq {X : Type u_1} [MetricSpace X] (D : DeloneSet X) (carrier : Set X) (packingRadius coveringRadius : NNReal) (h_carrier : carrier = D.carrier) (h_packing : packingRadius = D.packingRadius) (h_covering : coveringRadius = D.coveringRadius) : D.copy carrier packingRadius coveringRadius h_carrier h_packing h_covering = D

theorem Delone.DeloneSet.packingRadius_lt_dist_of_mem_ne {X : Type u_1} [MetricSpace X] (D : DeloneSet X) {x y : X} (hx : x ∈ D) (hy : y ∈ D) (hne : x ≠ y) : ↑D.packingRadius < dist x y

theorem Delone.DeloneSet.exists_dist_le_coveringRadius {X : Type u_1} [MetricSpace X] (D : DeloneSet X) (x : X) : ∃ y ∈ D, dist x y ≤ ↑D.coveringRadius

theorem Delone.DeloneSet.eq_of_mem_ball {X : Type u_1} [MetricSpace X] (D : DeloneSet X) {r : NNReal} (hr : r ≤ D.packingRadius / 2) {x y z : X} (hx : x ∈ D) (hy : y ∈ D) (hxz : x ∈ Metric.ball z ↑r) (hyz : y ∈ Metric.ball z ↑r) : x = y

theorem Delone.DeloneSet.subset_ball_singleton {X : Type u_1} [MetricSpace X] (D : DeloneSet X) : ∃ r > 0, ∀ {x y z : X}, x ∈ D → y ∈ D → x ∈ Metric.ball z r → y ∈ Metric.ball z r → x = y

There exists a radius r > 0 such that any ball of radius r centered at a point of D contains at most one point of D.

noncomputable def Delone.DeloneSet.mapBilipschitz {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : DeloneSet X) : DeloneSet Y

Bilipschitz maps send Delone sets to Delone sets.

@[simp]

theorem Delone.DeloneSet.mapBilipschitz_carrier {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : DeloneSet X) : (mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D).carrier = ⇑f '' D.carrier

@[simp]

theorem Delone.DeloneSet.mapBilipschitz_packingRadius {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : DeloneSet X) : (mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D).packingRadius = D.packingRadius / K₁

@[simp]

theorem Delone.DeloneSet.mapBilipschitz_coveringRadius {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : DeloneSet X) : (mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D).coveringRadius = K₂ * D.coveringRadius

@[simp]

theorem Delone.DeloneSet.mapBilipschitz_refl {X : Type u_1} [MetricSpace X] (D : DeloneSet X) (hK1 hK2 : 0 < 1) (hA : AntilipschitzWith 1 ⇑(Equiv.refl X)) (hL : LipschitzWith 1 ⇑(Equiv.refl X)) : mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D

theorem Delone.DeloneSet.mapBilipschitz_trans {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {Z : Type u_3} [MetricSpace Z] (D : DeloneSet X) (f : X ≃ Y) (g : Y ≃ Z) (K₁f K₂f K₁g K₂g : NNReal) (hf₁_pos : 0 < K₁f) (hf₂_pos : 0 < K₂f) (hg₁_pos : 0 < K₁g) (hg₂_pos : 0 < K₂g) (hf_anti : AntilipschitzWith K₁f ⇑f) (hf_lip : LipschitzWith K₂f ⇑f) (hg_anti : AntilipschitzWith K₁g ⇑g) (hg_lip : LipschitzWith K₂g ⇑g) : mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) = mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D

noncomputable def Delone.DeloneSet.mapIsometry {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) : DeloneSet X ≃ DeloneSet Y

The image of a Delone set under an isometry. This is a specialization of DeloneSet.mapBilipschitz where the packing and covering radii are preserved because the Lipschitz constants are both 1.

@[simp]

theorem Delone.DeloneSet.mapIsometry_symm_apply_carrier {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) (D : DeloneSet Y) : ((mapIsometry f).symm D).carrier = ⇑f.symm '' D.carrier

@[simp]

theorem Delone.DeloneSet.mapIsometry_apply_coveringRadius {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) (D : DeloneSet X) : ((mapIsometry f) D).coveringRadius = D.coveringRadius

@[simp]

theorem Delone.DeloneSet.mapIsometry_apply_packingRadius {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) (D : DeloneSet X) : ((mapIsometry f) D).packingRadius = D.packingRadius

@[simp]

theorem Delone.DeloneSet.mapIsometry_symm_apply_packingRadius {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) (D : DeloneSet Y) : ((mapIsometry f).symm D).packingRadius = D.packingRadius

@[simp]

theorem Delone.DeloneSet.mapIsometry_symm_apply_coveringRadius {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) (D : DeloneSet Y) : ((mapIsometry f).symm D).coveringRadius = D.coveringRadius

@[simp]

theorem Delone.DeloneSet.mapIsometry_apply_carrier {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) (D : DeloneSet X) : ((mapIsometry f) D).carrier = ⇑f '' D.carrier

@[simp]

theorem Delone.DeloneSet.mapIsometry_refl {X : Type u_1} [MetricSpace X] (D : DeloneSet X) : (mapIsometry (IsometryEquiv.refl X)) D = D

theorem Delone.DeloneSet.mapIsometry_symm {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X ≃ᵢ Y) : (mapIsometry f).symm = mapIsometry f.symm

theorem Delone.DeloneSet.mapIsometry_trans {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {Z : Type u_3} [MetricSpace Z] (D : DeloneSet X) (f : X ≃ᵢ Y) (g : Y ≃ᵢ Z) : (mapIsometry (f.trans g)) D = (mapIsometry g) ((mapIsometry f) D)