English
If you take two centers of mass from the same index set with two weight functions w1 and w2 whose sums are 1, then any convex combination of these centers of mass equals the center of mass with the combined weights a w1 + b w2.
Русский
Если взять два центра масс по одному набору индексов с весами w1 и w2, сумма которых равна 1, то произвольная выпуклая комбинация центров масс равна центру массы с объединёнными весами a w1 + b w2.
LaTeX
$$a \cdot s.centerMass\, w1\, z + b \cdot s.centerMass\, w2\, z = s.centerMass\, (fun i => a * w1 i + b * w2 i)\, z$$
Lean4
/-- A convex combination of two centers of mass is a center of mass as well. This version
works if two centers of mass share the set of original points. -/
theorem centerMass_segment (s : Finset ι) (w₁ w₂ : ι → R) (z : ι → E) (hw₁ : ∑ i ∈ s, w₁ i = 1)
(hw₂ : ∑ i ∈ s, w₂ i = 1) (a b : R) (hab : a + b = 1) :
a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z :=
by
have hw : (∑ i ∈ s, (a * w₁ i + b * w₂ i)) = 1 := by simp only [← mul_sum, sum_add_distrib, mul_one, *]
simp only [Finset.centerMass_eq_of_sum_1, smul_sum, sum_add_distrib, add_smul, mul_smul, *]
