Signed sums from a distribution with small shift distance

Adapted for Lean Pool by changing module paths and selecting explicit imports.

Lemma 1.4 of Karingula–Lovett: if shiftDist P (6 • v i) ≤ 1 / 3 for every i, there is a colouring ε such that mean P + ∑ i, ε i • v i belongs to the convex hull of the support of P.

The proof is by induction on the number of vectors. Split in the direction of the last vector, apply the induction hypothesis in E × ℝ, and use the pullback lemma.

theorem Komlos.exists_isColouring_mean_add_sum_mem_convexHull (n : ℕ) {E : Type u} [AddCommGroup E] [Module ℝ E] (P : E →₀ ℝ) : IsDist P → ∀ (v : Fin n → E), (∀ (i : Fin n), shiftDist P (6 • v i) ≤ 3⁻¹) → ∃ (ε : Fin n → ℝ), IsColouring ε ∧ mean P + ∑ i : Fin n, ε i • v i ∈ (convexHull ℝ) ↑P.support

Lemma 1.4: if shiftDist P (6 • v i) ≤ 1 / 3 for every i, some colouring ε satisfies mean P + ∑ i, ε i • v i ∈ convexHull ℝ (P.support : Set E).