theorem mem_convexHull_image {ι : Type u_1} {R : Type u_2} {E : Type u_3} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] {s : Finset ι} {f : ι → E} {x : E} : x ∈ (convexHull R) (f '' ↑s) ↔ ∃ (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ s.centerMass w f = x

theorem centerMass_congr {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {v w : ι → 𝕜} {x y : ι → V} (hst : s = t) (hvw : ∀ i ∈ t, v i = w i) (hxy : ∀ i ∈ t, x i = y i) : s.centerMass v x = t.centerMass w y

theorem centerMass_union {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {w : ι → 𝕜} {x : ι → V} [DecidableEq ι] (hst : Disjoint s t) (hs : (∀ i ∈ s, w i = 0) ∨ ∑ i ∈ s, w i ≠ 0) (ht : (∀ i ∈ t, w i = 0) ∨ ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) : (s ∪ t).centerMass w x = (∑ i ∈ s, w i) • s.centerMass w x + (∑ i ∈ t, w i) • t.centerMass w x

theorem centerMass_union_of_ne_zero {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {w : ι → 𝕜} {x : ι → V} [DecidableEq ι] (hst : Disjoint s t) (hs : ∑ i ∈ s, w i ≠ 0) (ht : ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) : (s ∪ t).centerMass w x = (∑ i ∈ s, w i) • s.centerMass w x + (∑ i ∈ t, w i) • t.centerMass w x

theorem lineMap_centerMass_centerMass {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {w : ι → 𝕜} {x : ι → V} [DecidableEq ι] (hst : Disjoint s t) (hs : (∀ i ∈ s, w i = 0) ∨ ∑ i ∈ s, w i ≠ 0) (ht : (∀ i ∈ t, w i = 0) ∨ ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) : (AffineMap.lineMap (s.centerMass w x) (t.centerMass w x)) (∑ i ∈ t, w i) = (s ∪ t).centerMass w x

theorem lineMap_centerMass_centerMass_of_ne_zero {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {w : ι → 𝕜} {x : ι → V} [DecidableEq ι] (hst : Disjoint s t) (hs : ∑ i ∈ s, w i ≠ 0) (ht : ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) : (AffineMap.lineMap (s.centerMass w x) (t.centerMass w x)) (∑ i ∈ t, w i) = (s ∪ t).centerMass w x

theorem lineMap_centerMass_sdiff {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Finset ι} {w : ι → 𝕜} {x : ι → V} {i : ι} [DecidableEq ι] (hi : i ∈ s) (hi₀ : w i ≠ 0) (hi₁ : w i ≠ 1) (hw₁ : ∑ i ∈ s, w i = 1) : (AffineMap.lineMap ((s \ {i}).centerMass w x) (x i)) (w i) = s.centerMass w x

theorem centerMass_sdiff_of_weight_eq_zero {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Finset ι} {w : ι → 𝕜} {x : ι → V} {i : ι} [DecidableEq ι] (hi : i ∈ s) (hi₀ : w i = 0) : (s \ {i}).centerMass w x = s.centerMass w x

theorem lineMap_centerMass_sdiff_singleton_of_ne_one {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Finset ι} {w : ι → 𝕜} {x : ι → V} {i : ι} [DecidableEq ι] (hi : i ∈ s) (hi₁ : w i ≠ 1) (hw₁ : ∑ j ∈ s, w j = 1) : (AffineMap.lineMap ((s \ {i}).centerMass w x) (x i)) (w i) = s.centerMass w x

theorem centerMass_union_of_nonneg {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {w : ι → 𝕜} {x : ι → V} [DecidableEq ι] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (hst : Disjoint s t) (hw₀ : ∀ i ∈ s ∪ t, 0 ≤ w i) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) : (s ∪ t).centerMass w x = (∑ i ∈ s, w i) • s.centerMass w x + (∑ i ∈ t, w i) • t.centerMass w x

theorem lineMap_centerMass_centerMass_of_nonneg {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s t : Finset ι} {w : ι → 𝕜} {x : ι → V} [DecidableEq ι] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (hst : Disjoint s t) (hw₀ : ∀ i ∈ s ∪ t, 0 ≤ w i) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) : (AffineMap.lineMap (s.centerMass w x) (t.centerMass w x)) (∑ i ∈ t, w i) = (s ∪ t).centerMass w x

theorem lineMap_centerMass_sdiff_singleton_of_nonneg {ι : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [Field 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Finset ι} {w : ι → 𝕜} {x : ι → V} {i : ι} [DecidableEq ι] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (hi : i ∈ s) (hw₀ : ∀ j ∈ s \ {i}, 0 ≤ w j) (hw₁ : ∑ j ∈ s, w j = 1) : (AffineMap.lineMap ((s \ {i}).centerMass w x) (x i)) (w i) = s.centerMass w x