NRR.EMP.VariableBody.CompactSiteFamily — uniform bounds and separation

For a compact metric parameter space X carrying a continuous configuration family sites : SiteFamily X n, every site position is uniformly bounded, and any two distinct sites are uniformly separated. We also record a radius bound for the fixed planar parent body K.

These uniform quantities are the geometric inputs to the later continuity arguments of the variable-body power partition: they let one work inside a fixed ball and with a fixed minimal gap, independently of the parameter.

theorem NRR.EMP.VariableBody.exists_siteRadius {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) : ∃ (R : ℝ), 0 ≤ R ∧ ∀ (x : X) (i : Fin n), ‖(sites x).pts i‖ ≤ R

Uniform site radius. Over a compact parameter space, every labelled site of a continuous configuration family stays inside a common ball; no assumption 0 < n is needed.

theorem NRR.EMP.VariableBody.exists_parentRadius (K : Geometry.ConvexBody Geometry.Plane) : ∃ (R : ℝ), 0 ≤ R ∧ ∀ y ∈ K.carrier, ‖y‖ ≤ R

Parent radius. The fixed planar parent body, being compact, is contained in a ball.

theorem NRR.EMP.VariableBody.exists_uniformSiteSeparation {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (x : X) (i j : Fin n), i ≠ j → δ ≤ dist ((sites x).pts i) ((sites x).pts j)

Uniform site separation. Over a compact parameter space, any two distinct labelled sites of a continuous configuration family stay at least a fixed positive distance apart.

noncomputable def NRR.EMP.VariableBody.siteRadius {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) : ℝ

The canonical uniform site radius of a continuous site family over a compact space.

Equations

• NRR.EMP.VariableBody.siteRadius sites = ⋯.choose

noncomputable def NRR.EMP.VariableBody.parentRadius (K : Geometry.ConvexBody Geometry.Plane) : ℝ

The canonical parent radius of a fixed planar parent body.

Equations

• NRR.EMP.VariableBody.parentRadius K = ⋯.choose

noncomputable def NRR.EMP.VariableBody.siteSeparation {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) : ℝ

The canonical uniform site separation of a continuous site family over a compact space.

Equations

• NRR.EMP.VariableBody.siteSeparation sites = ⋯.choose

theorem NRR.EMP.VariableBody.siteRadius_nonneg {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) : 0 ≤ siteRadius sites

theorem NRR.EMP.VariableBody.norm_site_le_siteRadius {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) (x : X) (i : Fin n) : ‖(sites x).pts i‖ ≤ siteRadius sites

theorem NRR.EMP.VariableBody.parentRadius_nonneg (K : Geometry.ConvexBody Geometry.Plane) : 0 ≤ parentRadius K

theorem NRR.EMP.VariableBody.norm_mem_parent_le_parentRadius (K : Geometry.ConvexBody Geometry.Plane) {y : Geometry.Plane} (hy : y ∈ K.carrier) : ‖y‖ ≤ parentRadius K

theorem NRR.EMP.VariableBody.siteSeparation_pos {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) : 0 < siteSeparation sites

theorem NRR.EMP.VariableBody.siteSeparation_le_dist {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (sites : SiteFamily X n) (x : X) {i j : Fin n} (hij : i ≠ j) : siteSeparation sites ≤ dist ((sites x).pts i) ((sites x).pts j)