NRR.EMP.VariableBody.EqualAreaRelation — closedness of the equal-area relation

Using the joint continuity of the area vector, the relation "the weight w is an equal-area weight for the sites s inside the variable body C" is a finite intersection of zero sets and hence closed, and adding the normalization ∑ i, w i = 0 keeps it closed. Composing with a continuous site family yields the closed normalized-weight graph over any topological parameter space.

• isClosed_isEqualAreaWeight — the equal-area relation is closed.
• isClosed_isNormalizedEqualAreaWeight — the normalized equal-area relation is closed.
• NormalizedWeightGraph, isClosed_normalizedWeightGraph — the closed graph over a continuous site family.

theorem NRR.EMP.VariableBody.isEqualAreaWeight_iff_emp {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) : IsEqualAreaWeight hA C s w ↔ EMP.IsEqualAreaWeight (solidBody hA C) s.pts w

The variable-body equal-area predicate is exactly the fixed-body predicate of EMP applied to the solid body of C.

theorem NRR.EMP.VariableBody.isEqualAreaWeight_iff_areaVec {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) : IsEqualAreaWeight hA C s w ↔ ∀ (i : Fin n), areaVec hA C s w i = targetArea C n

The equal-area predicate as a componentwise equality of the area vector with the target area.

theorem NRR.EMP.VariableBody.weightNormalized_iff_sum {n : ℕ} (w : Fin n → ℝ) : WeightNormalized w ↔ ∑ i : Fin n, w i = 0

The normalization predicate as vanishing of the weight sum.

theorem NRR.EMP.VariableBody.isClosed_isEqualAreaWeight {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) : IsClosed {z : BodySpace K A × Config n × (Fin n → ℝ) | IsEqualAreaWeight hA z.1 z.2.1 z.2.2}

The equal-area relation is closed. The set of triples (C, s, w) for which w is an equal-area weight for s in C is closed, being the finite intersection over the sites of the zero sets of the continuous functions areaVec hA C s w i - targetArea C n.

theorem NRR.EMP.VariableBody.isClosed_isNormalizedEqualAreaWeight {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) : IsClosed {z : BodySpace K A × Config n × (Fin n → ℝ) | IsNormalizedEqualAreaWeight hA z.1 z.2.1 z.2.2}

The normalized equal-area relation is closed. Intersect the closed equal-area relation with the closed normalization locus ∑ i, w i = 0.

def NRR.EMP.VariableBody.NormalizedWeightGraph {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [TopologicalSpace X] (sites : C(X, Config n)) (hA : 0 < A) : Set ((BodySpace K A × X) × (Fin n → ℝ))

The normalized-weight graph over a topological parameter space X carrying a continuous site family sites : C(X, Config n): the set of pairs ((C, x), w) for which w is a normalized equal-area weight for the sites sites x inside the variable body C.

Equations

• NRR.EMP.VariableBody.NormalizedWeightGraph sites hA = {z : (NRR.BodySpace K A × X) × (Fin n → ℝ) | NRR.EMP.VariableBody.IsNormalizedEqualAreaWeight hA z.1.1 (sites z.1.2) z.2}

theorem NRR.EMP.VariableBody.isClosed_normalizedWeightGraph {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [TopologicalSpace X] (sites : C(X, Config n)) (hA : 0 < A) : IsClosed (NormalizedWeightGraph sites hA)

The normalized-weight graph is closed. It is the preimage of the closed normalized equal-area relation under the continuous reparameterization ((C, x), w) ↦ (C, sites x, w).