NRR.EMP.VariableBody.NormalizedWeightContinuity — continuity of the selected weight

For a fixed planar parent body K, a lower area bound A, and a compact metric parameter space X carrying a continuous site family sites : SiteFamily X n, the canonical normalized equal-area weight varies continuously with both the subbody C : BodySpace K A and the parameter x : X.

The argument is purely topological, derived from the closed normalized equal-area relation (isClosed_normalizedWeightGraph), uniqueness (normalizedWeight_unique), and the uniform coordinate bound (normalizedWeight_abs_le); it does not use any pre-existing normalized-weight continuity core.

• normalizedWeightBox — the selected weight, valued in the compact weight box.
• isClosed_graph_normalizedWeightBox — its graph is closed.
• continuous_normalizedWeightBox — the boxed selection is continuous.
• continuous_normalizedWeight_compactFamily — continuity into the ordinary weight space.
• continuous_normalizedWeight_compactFamily_apply — coordinate continuity.
• areaVec_normalizedWeight_eq_target — the selected area vector is the constant target vector.
• continuous_areaVec_normalizedWeight_compactFamily — continuity of the selected area vector.

noncomputable def NRR.EMP.VariableBody.normalizedWeightBox {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) (z : BodySpace K A × X) : WeightBox n (weightBound K sites)

The boxed selected weight: the canonical normalized equal-area weight, packaged with its uniform coordinate bound as an element of the compact weight box.

Equations

• NRR.EMP.VariableBody.normalizedWeightBox sites hA hn z = ⟨NRR.EMP.VariableBody.normalizedWeight hA hn z.1 (sites z.2), ⋯⟩

@[simp]

theorem NRR.EMP.VariableBody.normalizedWeightBox_coe {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) (z : BodySpace K A × X) : ↑(normalizedWeightBox sites hA hn z) = normalizedWeight hA hn z.1 (sites z.2)

theorem NRR.EMP.VariableBody.isClosed_graph_normalizedWeightBox {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) : IsClosed {z : (BodySpace K A × X) × WeightBox n (weightBound K sites) | z.2 = normalizedWeightBox sites hA hn z.1}

The graph of the boxed selected weight is closed. The pullback of the closed normalized equal-area relation along the continuous coordinate inclusion WeightBox → (Fin n → ℝ) is a closed relation that contains the graph (normalizedWeight_isEqualArea, normalizedWeight_normalized) and selects uniquely (normalizedWeight_unique); apply the uniqueness closed-graph criterion.

theorem NRR.EMP.VariableBody.continuous_normalizedWeightBox {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) : Continuous (normalizedWeightBox sites hA hn)

Continuity of the boxed selected weight. The domain BodySpace K A × X is compact Hausdorff, the weight box is compact Hausdorff, and the graph is closed, so the compact closed-graph criterion gives continuity.

theorem NRR.EMP.VariableBody.continuous_normalizedWeight_compactFamily {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) : Continuous fun (z : BodySpace K A × X) => normalizedWeight hA hn z.1 (sites z.2)

Continuity of the selected weight into the ordinary weight space. Compose the boxed continuity with the continuous coordinate inclusion.

theorem NRR.EMP.VariableBody.continuous_normalizedWeight_compactFamily_apply {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) (i : Fin n) : Continuous fun (z : BodySpace K A × X) => normalizedWeight hA hn z.1 (sites z.2) i

Coordinate continuity of the selected weight. Each coordinate of the selected weight is continuous, by composing the vector continuity with the coordinate projection.

theorem NRR.EMP.VariableBody.areaVec_normalizedWeight_eq_target {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (z : BodySpace K A × X) : areaVec hA z.1 (sites z.2) (normalizedWeight hA hn z.1 (sites z.2)) = fun (x : Fin n) => targetArea z.1 n

The selected area vector is the constant target vector. The equal-area property of the selected weight says every cell of the partition realizes the average area targetArea z.1 n.

theorem NRR.EMP.VariableBody.continuous_areaVec_normalizedWeight_compactFamily {X : Type u_1} [MetricSpace X] {n : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (sites : SiteFamily X n) (hA : 0 < A) (hn : 0 < n) : Continuous fun (z : BodySpace K A × X) => areaVec hA z.1 (sites z.2) (normalizedWeight hA hn z.1 (sites z.2))

Continuity of the selected area vector. By the constant-target identity, the selected area vector equals the continuous map z ↦ fun _ => targetArea z.1 n.