Outward estimates for the equal-area deviation map

This module supplies the coercive estimate needed by the finite-dimensional existence argument. For a normalized weight vector, let M be its largest coordinate. Every restricted power cell with positive area belongs to an index whose weight is at least M - C, where C is an explicit body/site bound. Consequently the scalar pairing of the weight vector with its area-deviation vector is at least (M - C) * K.area.

noncomputable def NRR.EMP.finiteSiteRadius {n : ℕ} (s : Fin n → Geometry.Plane) : ℝ

A finite upper bound for the norms of all sites.

Equations

• NRR.EMP.finiteSiteRadius s = ∑ i : Fin n, ‖s i‖

theorem NRR.EMP.finiteSiteRadius_nonneg {n : ℕ} (s : Fin n → Geometry.Plane) : 0 ≤ finiteSiteRadius s

theorem NRR.EMP.norm_site_le_finiteSiteRadius {n : ℕ} (s : Fin n → Geometry.Plane) (i : Fin n) : ‖s i‖ ≤ finiteSiteRadius s

noncomputable def NRR.EMP.powerGapBound {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) : ℝ

Uniform power-distance gap bound on the compact body.

Equations

• NRR.EMP.powerGapBound K s = (NRR.EMP.VariableBody.parentRadius K + NRR.EMP.finiteSiteRadius s) ^ 2

theorem NRR.EMP.powerGapBound_nonneg {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) : 0 ≤ powerGapBound K s

theorem NRR.EMP.weight_sub_le_powerGapBound_of_bodyCellSet_nonempty {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) {i : Fin n} (hi : (PowerDiagram.bodyCellSet K s w i).Nonempty) (j : Fin n) : w j - w i ≤ powerGapBound K s

If the i-th restricted cell is nonempty, no other weight exceeds w i by more than the uniform geometric gap bound.

theorem NRR.EMP.bodyCellSet_nonempty_of_areaVec_ne_zero {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) (hi : areaVec K s w i ≠ 0) : (PowerDiagram.bodyCellSet K s w i).Nonempty

A nonzero restricted-cell area implies that the restricted cell is nonempty.

theorem NRR.EMP.areaVec_nonneg {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : 0 ≤ areaVec K s w i

Restricted power-cell areas are nonnegative.

noncomputable def NRR.EMP.deviationPairing {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) : ℝ

Pairing of weights with the area-deviation vector.

Equations

• NRR.EMP.deviationPairing K s w = ∑ i : Fin n, w i * NRR.EMP.areaDeviation K s w i

theorem NRR.EMP.deviationPairing_eq_weightedArea_of_normalized {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (hw : WeightNormalized w) : deviationPairing K s w = ∑ i : Fin n, w i * areaVec K s w i

For normalized weights, the target part of the pairing vanishes.

theorem NRR.EMP.deviationPairing_lower_bound_of_max {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : Fin n → ℝ) (hw : WeightNormalized w) (k : Fin n) : (w k - powerGapBound K s) * K.area ≤ deviationPairing K s w

Coercive lower bound for the deviation pairing in terms of a maximal weight coordinate.

theorem NRR.EMP.deviationPairing_pos_of_max_gt {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : Fin n → ℝ) (hw : WeightNormalized w) (k : Fin n) (hlarge : powerGapBound K s < w k) : 0 < deviationPairing K s w

In particular, once a maximal normalized weight exceeds the geometric gap bound, the weight/deviation pairing is strictly positive.