English
If we form the center of mass from two different index types and take a convex combination of these centers of mass, the result is the center of mass of the combined system with appropriately weighted contributions.
Русский
Если взять центры масс двух различных индексов и взяться за их выпуклую комбинацию, то результат является центром масс объединённой системы с соответствующими весами.
LaTeX
$$a \cdot s.centerMass\, ws\, zs + b \cdot t.centerMass\, wt\, zt = (s.disjSum t).centerMass\, (Sum.elim (fun i => a * ws i) (fun j => b * wt j))\, (Sum.elim zs zt)$$
Lean4
/-- A convex combination of two centers of mass is a center of mass as well. This version
deals with two different index types. -/
theorem centerMass_segment' (s : Finset ι) (t : Finset ι') (ws : ι → R) (zs : ι → E) (wt : ι' → R) (zt : ι' → E)
(hws : ∑ i ∈ s, ws i = 1) (hwt : ∑ i ∈ t, wt i = 1) (a b : R) (hab : a + b = 1) :
a • s.centerMass ws zs + b • t.centerMass wt zt =
(s.disjSum t).centerMass (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt) :=
by
rw [s.centerMass_eq_of_sum_1 _ hws, t.centerMass_eq_of_sum_1 _ hwt, smul_sum, smul_sum, ← Finset.sum_sumElim,
Finset.centerMass_eq_of_sum_1]
· congr with ⟨⟩ <;> simp only [Sum.elim_inl, Sum.elim_inr, mul_smul]
· rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
