English
Affine combinations of centers of mass equal the center of mass of the corresponding affine combination of weights and points.
Русский
Аффинные комбинации центров масс равны центру массы соответствующей аффинной комбинации весов и точек.
LaTeX
$$t.affineCombination R p w = centerMass t w p$$
Lean4
theorem convex_iff_sum_mem :
Convex R s ↔
∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → (∑ x ∈ t, w x • x) ∈ s :=
by
classical
refine ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩
intro h x hx y hy a b ha hb hab
by_cases h_cases : x = y
· rw [h_cases, ← add_smul, hab, one_smul]
exact hy
· convert h { x, y } (fun z => if z = y then b else a) _ _ _
· simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
· grind
· simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
· intro i hi
simp only [Finset.mem_singleton, Finset.mem_insert] at hi
cases hi <;> subst i <;> assumption
