Rational balanced coefficients

Approximation inside the strict caps preserves the exact rational affine equations. The largest centrality keeps the resulting coefficients uniform over every admissible centrality parameter.

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