Lean4
/-- If `x` is in the convex hull of some finset `t` whose elements are not affine-independent,
then it is in the convex hull of a strict subset of `t`. -/
theorem mem_convexHull_erase [DecidableEq E] {t : Finset E} (h : ¬AffineIndependent 𝕜 ((↑) : t → E)) {x : E}
(m : x ∈ convexHull 𝕜 (↑t : Set E)) : ∃ y : (↑t : Set E), x ∈ convexHull 𝕜 (↑(t.erase y) : Set E) :=
by
simp only [Finset.convexHull_eq, mem_setOf_eq] at m ⊢
obtain ⟨f, fpos, fsum, rfl⟩ := m
obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h
replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
clear h
let s := {z ∈ t | 0 < g z}
obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i :=
by
apply s.exists_min_image fun z => f z / g z
obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
have hg : 0 < g i₀ := by
rw [mem_filter] at mem
exact mem.2
have hi₀ : i₀ ∈ t := filter_subset _ _ mem
let k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
have hk : k i₀ = 0 := by simp [k, ne_of_gt hg]
have ksum : ∑ e ∈ t.erase i₀, k e = 1 := by
calc
∑ e ∈ t.erase i₀, k e = ∑ e ∈ t, k e := by
conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
_ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) := rfl
_ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
refine ⟨⟨i₀, hi₀⟩, k, ?_, by convert ksum, ?_⟩
· simp only [k, and_imp, sub_nonneg, mem_erase, Ne]
intro e _ het
by_cases hes : e ∈ s
· have hge : 0 < g e := by
rw [mem_filter] at hes
exact hes.2
rw [← le_div_iff₀ hge]
exact w _ hes
·
calc
_ ≤ 0 := by
apply mul_nonpos_of_nonneg_of_nonpos
· apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
· simpa only [s, mem_filter, het, true_and, not_lt] using hes
_ ≤ f e := fpos e het
· rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]
calc
∑ e ∈ t.erase i₀, k e • e = ∑ e ∈ t, k e • e := sum_erase _ (by rw [hk, zero_smul])
_ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e := rfl
_ = t.centerMass f id := by
simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero, centerMass, fsum,
inv_one, one_smul, id]
