English
The same center-mass decomposition holds with a simplified auxiliary lemma about sums, refining the previous centerMass_segment result.
Русский
Тот же разложение центра массы справедливо и с упрощённой вспомогательной леммой о суммах, уточняющей предшествующий результат.
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
theorem centerMass_le_sup {s : Finset ι} {f : ι → α} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ s, w i) :
s.centerMass w f ≤ s.sup' (nonempty_of_ne_empty <| by rintro rfl; simp at hw₁) f :=
by
rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_smul]
exact sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi
