Coercivity gauge for the augmented equal-area deviation field

The normalized area-deviation map lives on the zero-sum hyperplane. To apply the Euclidean outward-field theorem without choosing a basis of that hyperplane, we add back the constant direction: the augmented field is the area deviation of the mean-subtracted weights plus the weight mean in every coordinate.

A continuous homogeneous gauge detects both components. Its restriction to the Euclidean unit sphere has a positive minimum, giving a uniform outward radius.

@[reducible, inline]

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

Euclidean coordinates for the weight gauge and its unit sphere.

Equations

• NRR.EMP.WeightE n = EuclideanSpace ℝ (Fin n)

noncomputable def NRR.EMP.positiveWeightMass {n : ℕ} (w : Fin n → ℝ) : ℝ

Sum of positive coordinates of a weight vector.

Equations

• NRR.EMP.positiveWeightMass w = ∑ i : Fin n, max (w i) 0

theorem NRR.EMP.positiveWeightMass_nonneg {n : ℕ} (w : Fin n → ℝ) : 0 ≤ positiveWeightMass w

noncomputable def NRR.EMP.weightCoercivityGauge {n : ℕ} (w : Fin n → ℝ) : ℝ

A homogeneous gauge separating the normalized and constant directions.

Equations

• NRR.EMP.weightCoercivityGauge w = NRR.EMP.positiveWeightMass (NRR.EMP.normalizeWeight w) + |NRR.EMP.weightMean w|

theorem NRR.EMP.continuous_weightCoercivityGauge {n : ℕ} : Continuous fun (w : WeightE n) => weightCoercivityGauge fun (i : Fin n) => w.ofLp i

theorem NRR.EMP.weightCoercivityGauge_nonneg {n : ℕ} (w : Fin n → ℝ) : 0 ≤ weightCoercivityGauge w

theorem NRR.EMP.normalizeWeight_add_mean {n : ℕ} (w : Fin n → ℝ) (i : Fin n) : normalizeWeight w i + weightMean w = w i

theorem NRR.EMP.weightCoercivityGauge_pos_of_ne_zero {n : ℕ} (hn : 0 < n) (w : Fin n → ℝ) (hw : w ≠ 0) : 0 < weightCoercivityGauge w

theorem NRR.EMP.weightCoercivityGauge_smul {n : ℕ} {r : ℝ} (hr : 0 ≤ r) (w : Fin n → ℝ) : (weightCoercivityGauge fun (i : Fin n) => r * w i) = r * weightCoercivityGauge w

theorem NRR.EMP.exists_positive_gauge_lower_bound_on_sphere {n : ℕ} (hn : 0 < n) : ∃ (c : ℝ), 0 < c ∧ ∀ (x : WeightE n), ‖x‖ = 1 → c ≤ weightCoercivityGauge fun (i : Fin n) => x.ofLp i

The coercivity gauge has a positive lower bound on the Euclidean unit sphere.

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

The augmented deviation field on the full Euclidean weight space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NRR.EMP.augmentedAreaDeviation_apply {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : WeightE n) (i : Fin n) : (augmentedAreaDeviation K s w).ofLp i = areaDeviation K s (normalizeWeight fun (j : Fin n) => w.ofLp j) i + weightMean fun (j : Fin n) => w.ofLp j

theorem NRR.EMP.continuous_augmentedAreaDeviation {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hs : Function.Injective s) : Continuous (augmentedAreaDeviation K s)

theorem NRR.EMP.augmentedPairing_eq {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : WeightE n) : inner ℝ w (augmentedAreaDeviation K s w) = deviationPairing K s (normalizeWeight fun (i : Fin n) => w.ofLp i) + ↑n * (weightMean fun (i : Fin n) => w.ofLp i) ^ 2

theorem NRR.EMP.augmentedAreaDeviation_zero_gives_equalArea {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : WeightE n) (hw : augmentedAreaDeviation K s w = 0) : IsEqualAreaWeight K s (normalizeWeight fun (i : Fin n) => w.ofLp i)

@[reducible, inline]

abbrev NRR.EMP.WeightE' (n : ℕ) : Type

Euclidean weight coordinates used in the compact-sphere lower-bound argument.

Equations

• NRR.EMP.WeightE' n = EuclideanSpace ℝ (Fin n)

theorem NRR.EMP.max_normalized_weight_nonneg {n : ℕ} (hn : 0 < n) (w : Fin n → ℝ) (k : Fin n) (hk : ∀ (i : Fin n), w i ≤ w k) (hw : WeightNormalized w) : 0 ≤ w k

theorem NRR.EMP.positiveWeightMass_le_card_mul_max {n : ℕ} (hn : 0 < n) (w : Fin n → ℝ) (k : Fin n) (hk : ∀ (i : Fin n), w i ≤ w k) (hw : WeightNormalized w) : positiveWeightMass w ≤ ↑n * w k

theorem NRR.EMP.augmentedPairing_pos_of_gauge_large {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (w : WeightE' n) (hlarge : ↑n * (powerGapBound K s + 1) + (powerGapBound K s * K.area + 1) < weightCoercivityGauge fun (i : Fin n) => w.ofLp i) : 0 < inner ℝ w (augmentedAreaDeviation K s w)

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

A radius on which the augmented area-deviation field is strictly outward.

Equations

• NRR.EMP.equalAreaOutwardRadius K s hn = (↑n * (NRR.EMP.powerGapBound K s + 1) + (NRR.EMP.powerGapBound K s * K.area + 1) + 1) / Classical.choose ⋯

theorem NRR.EMP.equalAreaOutwardRadius_pos {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) : 0 < equalAreaOutwardRadius K s hn

theorem NRR.EMP.augmentedAreaDeviation_outward_on_radius {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) (x : WeightE' n) (hx : ‖x‖ = 1) : 0 < inner ℝ x (augmentedAreaDeviation K s (equalAreaOutwardRadius K s hn • x))