NRR.EMP.VariableBody.WeightBounds — uniform coordinate bounds

For a compact metric parameter space X carrying a continuous site family sites : SiteFamily X n and a fixed planar parent body K, every equal-area (Laguerre) weight for a subbody C : BodySpace K A at a parameter x : X obeys an explicit uniform bound expressed through the compact site and parent radii.

The bound is weightBound K sites = (parentRadius K + siteRadius sites) ^ 2. It is independent of the subbody C, the parameter x, and the individual weight w, and is the compactness input for the closed-graph selection theorem.

Proof outline

Equal area forces every restricted cell to have the positive area C.body.area / n, so each cell is nonempty; a point y of the i-th cell is power-closer to site i than to site j, which rearranges to w j - w i ≤ ‖y - s j‖² - ‖y - s i‖². Dropping the nonpositive term and bounding ‖y - s j‖ ≤ parentRadius K + siteRadius sites (using y ∈ C ⊆ K) gives the pairwise bound; the coordinate bound follows from normalization ∑ j, w j = 0 and the triangle inequality on the finite sum (n : ℝ) * w i = ∑ j, (w i - w j).

noncomputable def NRR.EMP.VariableBody.weightBound {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (sites : SiteFamily X n) : ℝ

Uniform coordinate bound for equal-area weights: the square of the sum of the compact parent and site radii. It is independent of the subbody, the parameter, and the individual weight.

Equations

• NRR.EMP.VariableBody.weightBound K sites = (NRR.EMP.VariableBody.parentRadius K + NRR.EMP.VariableBody.siteRadius sites) ^ 2

theorem NRR.EMP.VariableBody.weightBound_nonneg {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (sites : SiteFamily X n) : 0 ≤ weightBound K sites

theorem NRR.EMP.VariableBody.cast_mul_eq_sum_sub {n : ℕ} {w : Fin n → ℝ} (h : ∑ j : Fin n, w j = 0) (i : Fin n) : ↑n * w i = ∑ j : Fin n, (w i - w j)

Normalized finite-family identity. For a zero-sum weight vector, (n : ℝ) * w i equals the sum over j of the pairwise differences w i - w j. Stated independently of power diagrams.

theorem NRR.EMP.VariableBody.pairwise_weight_sub_le {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) {C : BodySpace K A} {x : X} {w : Fin n → ℝ} (hw : IsEqualAreaWeight hA C (sites x) w) (i j : Fin n) : w j - w i ≤ weightBound K sites

Pairwise weight bound. For any equal-area weight, the difference w j - w i is bounded by the explicit uniform weightBound K sites.

theorem NRR.EMP.VariableBody.abs_weight_sub_le {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) {C : BodySpace K A} {x : X} {w : Fin n → ℝ} (hw : IsEqualAreaWeight hA C (sites x) w) (i j : Fin n) : |w i - w j| ≤ weightBound K sites

Absolute pairwise weight bound. For any equal-area weight, |w i - w j| is bounded by the explicit uniform weightBound K sites.

theorem NRR.EMP.VariableBody.abs_weight_le {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) {C : BodySpace K A} {x : X} {w : Fin n → ℝ} (hw : IsNormalizedEqualAreaWeight hA C (sites x) w) (i : Fin n) : |w i| ≤ weightBound K sites

Coordinate bound for a normalized equal-area weight. Each coordinate of a normalized equal-area weight satisfies |w i| ≤ weightBound K sites.

theorem NRR.EMP.VariableBody.normalizedWeight_abs_le {X : Type u_1} [MetricSpace X] [CompactSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (C : BodySpace K A) (x : X) (i : Fin n) : |normalizedWeight hA hn C (sites x) i| ≤ weightBound K sites

Uniform coordinate bound for the canonical normalized weight. Every coordinate of the canonically selected normalized equal-area weight satisfies the explicit uniform bound.