Real balanced coefficients

The geometric part of balanced rounding: centrality puts the center in the image of a capped simplex. The cap can be selected at the largest centrality, so the resulting coefficients do not depend on the centrality parameter.

theorem EGZ.BalancedCombination.Data.exists_support_ge {d : ℕ} (D : Data d) (ξ : RealCoord d →ᵃ[ℝ] ℝ) : ∃ (q : ↥D.support), ξ D.center.real ≤ ξ (↑q).real

theorem EGZ.BalancedCombination.Data.exists_positive_centrality {d : ℕ} (D : Data d) : ∃ (θ : ℝ), 0 < θ ∧ IsCentral D.support D.weight θ D.center.real

noncomputable def EGZ.BalancedCombination.Data.maxCentrality {d : ℕ} (D : Data d) : ℝ

The largest admissible centrality depends only on the weighted data.

Equations

• D.maxCentrality = sSup {θ : ℝ | EGZ.BalancedCombination.IsCentral D.support D.weight θ D.center.real}

theorem EGZ.BalancedCombination.Data.centrality_le_max {d : ℕ} (D : Data d) {θ : ℝ} (hθ : IsCentral D.support D.weight θ D.center.real) : θ ≤ D.maxCentrality

theorem EGZ.BalancedCombination.Data.maxCentrality_pos {d : ℕ} (D : Data d) : 0 < D.maxCentrality

theorem EGZ.BalancedCombination.Data.isCentral_maxCentrality {d : ℕ} (D : Data d) : IsCentral D.support D.weight D.maxCentrality D.center.real

theorem EGZ.BalancedCombination.Data.maxCentrality_le_one {d : ℕ} (D : Data d) : D.maxCentrality ≤ 1

def EGZ.BalancedCombination.Data.barycenter {d : ℕ} (D : Data d) : (↥D.support → ℝ) →ₗ[ℝ] RealCoord d

The linear barycenter map on all coefficient vectors.

Equations

• D.barycenter = { toFun := fun (β : ↥D.support → ℝ) => ∑ q : ↥D.support, β q • (↑q).real, map_add' := ⋯, map_smul' := ⋯ }

def EGZ.BalancedCombination.Data.cappedSimplex {d : ℕ} (D : Data d) (θ : ℝ) : Set (↥D.support → ℝ)

A simplex with an individual upper bound on each coefficient.

Equations

• D.cappedSimplex θ = (Set.Icc 0 fun (q : ↥D.support) => D.weight q / (θ * ∑ r : ↥D.support, D.weight r)) ∩ {β : ↥D.support → ℝ | ∑ q : ↥D.support, β q = 1}

theorem EGZ.BalancedCombination.Data.cappedSimplex_convex {d : ℕ} (D : Data d) (θ : ℝ) : Convex ℝ (D.cappedSimplex θ)

theorem EGZ.BalancedCombination.Data.cappedSimplex_compact {d : ℕ} (D : Data d) (θ : ℝ) : IsCompact (D.cappedSimplex θ)

theorem EGZ.BalancedCombination.Data.capped_barycenter_exists {d : ℕ} (D : Data d) {θ : ℝ} (hθ : 0 < θ) (hcentral : IsCentral D.support D.weight θ D.center.real) : ∃ (β : ↥D.support → ℝ), (∀ (q : ↥D.support), 0 ≤ β q) ∧ ∑ q : ↥D.support, β q = 1 ∧ ∑ q : ↥D.support, β q • (↑q).real = D.center.real ∧ ∀ (q : ↥D.support), β q ≤ D.weight q / (θ * ∑ r : ↥D.support, D.weight r)

theorem EGZ.BalancedCombination.Data.coefficients_of_mem_convexHull {d : ℕ} (D : Data d) {x : RealCoord d} (hx : x ∈ (convexHull ℝ) (IntCoord.real '' ↑D.support)) : ∃ (β : ↥D.support → ℝ), (∀ (q : ↥D.support), 0 ≤ β q) ∧ ∑ q : ↥D.support, β q = 1 ∧ ∑ q : ↥D.support, β q • (↑q).real = x

theorem EGZ.BalancedCombination.Data.positive_barycenter_exists {d : ℕ} (D : Data d) : ∃ (β : ↥D.support → ℝ), (∀ (q : ↥D.support), 0 < β q) ∧ ∑ q : ↥D.support, β q = 1 ∧ ∑ q : ↥D.support, β q • (↑q).real = D.center.real

theorem EGZ.BalancedCombination.Data.positive_capped_barycenter_exists {d : ℕ} (D : Data d) {η : ℝ} (hη : 0 < η) : ∃ (β : ↥D.support → ℝ), (∀ (q : ↥D.support), 0 < β q) ∧ ∑ q : ↥D.support, β q = 1 ∧ ∑ q : ↥D.support, β q • (↑q).real = D.center.real ∧ ∀ (q : ↥D.support), β q < (1 + η) * D.weight q / (D.maxCentrality * ∑ r : ↥D.support, D.weight r)

Strict positive coefficients with an arbitrarily small relaxation of the optimal cap. Both the coefficients and the cap depend only on D.

theorem EGZ.BalancedCombination.Data.relaxed_max_cap_le {d : ℕ} (D : Data d) {η θ : ℝ} (hη : 0 ≤ η) (hθ : 0 < θ) (hc : IsCentral D.support D.weight θ D.center.real) (q : ↥D.support) : (1 + η) * D.weight q / (D.maxCentrality * ∑ r : ↥D.support, D.weight r) ≤ (1 + η) * D.weight q / (θ * ∑ r : ↥D.support, D.weight r)