NRR.EMP.NormalizedAreaDeviation — the deviation map on zero-sum weights

The additive-constant freedom of power weights is removed by restricting to the linear hyperplane of weight vectors whose coordinate sum is zero. The area-deviation vector also has coordinate sum zero, so it defines a continuous self-map of that finite-dimensional hyperplane.

This is the finite-dimensional map to which the eventual degree / outward-pointing argument for existence of equal-area power weights is applied.

@[reducible, inline]

abbrev NRR.EMP.NormalizedWeightSpace (n : ℕ) : Type

The zero-sum weight hyperplane, represented as a subtype of Fin n → ℝ.

Equations

• NRR.EMP.NormalizedWeightSpace n = { w : Fin n → ℝ // NRR.EMP.WeightNormalized w }

theorem NRR.EMP.NormalizedWeightSpace.ext {n : ℕ} {u v : NormalizedWeightSpace n} (h : ↑u = ↑v) : u = v

theorem NRR.EMP.NormalizedWeightSpace.ext_iff {n : ℕ} {u v : NormalizedWeightSpace n} : u = v ↔ ↑u = ↑v

noncomputable def NRR.EMP.NormalizedWeightSpace.zero (n : ℕ) : NormalizedWeightSpace n

The zero weight vector belongs to the normalized weight hyperplane.

Equations

• NRR.EMP.NormalizedWeightSpace.zero n = ⟨fun (x : Fin n) => 0, ⋯⟩

@[simp]

theorem NRR.EMP.NormalizedWeightSpace.coe_zero {n : ℕ} : ↑(zero n) = 0

noncomputable def NRR.EMP.normalizedAreaDeviation {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : NormalizedWeightSpace n) : NormalizedWeightSpace n

The area-deviation vector, regarded as a self-map of the normalized weight hyperplane.

Equations

• NRR.EMP.normalizedAreaDeviation K s hn hs w = ⟨NRR.EMP.areaDeviation K s ↑w, ⋯⟩

@[simp]

theorem NRR.EMP.normalizedAreaDeviation_coe {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : NormalizedWeightSpace n) : ↑(normalizedAreaDeviation K s hn hs w) = areaDeviation K s ↑w

theorem NRR.EMP.continuous_normalizedAreaDeviation {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : Continuous (normalizedAreaDeviation K s hn hs)

The normalized deviation map is continuous.

theorem NRR.EMP.normalizedAreaDeviation_eq_zero_iff {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : NormalizedWeightSpace n) : ↑(normalizedAreaDeviation K s hn hs w) = 0 ↔ IsEqualAreaWeight K s ↑w

A zero of the normalized deviation map is exactly a normalized equal-area weight.

theorem NRR.EMP.exists_equalArea_weights_of_normalizedDeviation_zero {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (hzero : ∃ (w : NormalizedWeightSpace n), ↑(normalizedAreaDeviation K s hn hs w) = 0) : ∃ (w : Fin n → ℝ), IsEqualAreaWeight K s w

Any zero of the normalized deviation map supplies the unrestricted existence theorem.