Integer approximation with an exact affine barycenter

A rational affine combination and an integer affine combination of weight one produce integer combinations of every sufficiently large weight. The integer correction depends only on the remainder modulo one common denominator, and therefore has uniformly bounded error.

theorem EGZ.BalancedCombination.exists_common_denominator {I : Type u_1} [Finite I] (β : I → ℚ) : ∃ (m : ℕ), 0 < m ∧ ∃ (b : I → ℤ), ∀ (i : I), ↑(b i) = ↑m * ↑(β i)

A common denominator for any finite rational family, expressed using real casts for later quantitative estimates.

theorem EGZ.BalancedCombination.Data.exists_integer_affine_coefficients {d : ℕ} (D : Data d) : ∃ (z : ↥D.support → ℤ), ∑ q : ↥D.support, z q = 1 ∧ ∑ q : ↥D.support, z q • ↑q = D.center

theorem EGZ.BalancedCombination.Data.exists_integer_approximation {d : ℕ} (D : Data d) (β : ↥D.support → ℚ) (hsum : ∑ q : ↥D.support, β q = 1) (hvec : ∀ (i : Fin d), ∑ q : ↥D.support, β q * ↑(↑q i) = ↑(D.center i)) : ∃ (A : ℕ → ↥D.support → ℤ) (E : ℝ), 0 ≤ E ∧ ∀ (n : ℕ), ∑ q : ↥D.support, A n q = ↑n ∧ ∑ q : ↥D.support, A n q • ↑q = ↑n • D.center ∧ ∀ (q : ↥D.support), |↑(A n q) - ↑n * ↑(β q)| ≤ E

Exact integer affine combinations approximate n * β with a bounded error independent of n. Positivity is not needed for this algebraic step.

theorem EGZ.BalancedCombination.Data.exists_coefficients_of_rational {d : ℕ} (D : Data d) (ε : ℝ) (hε : 0 < ε) (β : ↥D.support → ℚ) (hβ : ∀ (q : ↥D.support), 0 < β q) (hsum : ∑ q : ↥D.support, β q = 1) (hvec : ∀ (i : Fin d), ∑ q : ↥D.support, β q * ↑(↑q i) = ↑(D.center i)) (hcap : ∀ (θ : ℝ), 0 < θ → IsCentral D.support D.weight θ D.center.real → ∀ (q : ↥D.support), ↑(β q) ≤ (1 + ε / 2) * D.weight q / (θ * ∑ r : ↥D.support, D.weight r)) : ∃ (μ : ℝ) (N : ℕ), 0 < μ ∧ ∀ (θ : ℝ), 0 < θ → IsCentral D.support D.weight θ D.center.real → ∀ (n : ℕ), N < n → Nonempty (Coefficients D ε θ μ n)

A single positive rational affine combination satisfying all the relaxed caps yields the balanced integer combinations, with constants independent of the centrality parameter.