Pulling a convex combination back through a split

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

Suppose (z, β) belongs to the convex hull of the support of split (3 • w) P and β ≥ 1 / 3. The pullback lemma gives a sign e such that z + e • w belongs to the convex hull of the support of P.

For points with last coordinate 0, choose one of the points x ± 3 • w in the support of P. For points with last coordinate 1, use a convex combination of both. The coefficients are chosen so that the change in the first coordinate is e • w.

theorem Komlos.exists_sign_mul_add_eq {β a : ℝ} (hβ : 3⁻¹ ≤ β) (ha : |a| ≤ 1 - β) : ∃ (e : ℝ) (c : ℝ), (e = 1 ∨ e = -1) ∧ |c| ≤ 1 ∧ c * β + a = e / 3

If β ≥ 1 / 3 and |a| ≤ 1 - β, some c ∈ [-1, 1] satisfies c * β + a = ±1 / 3.

theorem Komlos.add_smul_mem_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Set E} {x v : E} (h₁ : x - v ∈ s) (h₂ : x + v ∈ s) {c : ℝ} (hc : |c| ≤ 1) : x + c • v ∈ (convexHull ℝ) s

A point of the segment between x - v and x + v lies in the convex hull of any set containing both endpoints.

theorem Komlos.pullback {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P : E →₀ ℝ} (hP : IsDist P) (w : E) {β : ℝ} (hβ : 3⁻¹ ≤ β) {z : E} (hmem : (z, β) ∈ (convexHull ℝ) ↑(split (3 • w) P).support) : ∃ (e : ℝ), (e = 1 ∨ e = -1) ∧ z + e • w ∈ (convexHull ℝ) ↑P.support

If (z, β) belongs to the convex hull of the support of split (3 • w) P and β ≥ 1 / 3, then z + e • w belongs to the convex hull of the support of P for some sign e.