English
If i is not already in t and the sum of weights is nonzero, then the centerMass of insert i into t equals a weighted combination of z_i and the centerMass of t.
Русский
Если элемент i не принадлежит t и сумма весов не равна нулю, то центр массы вставки i в t равен взвешенному сочетанию z_i и centerMass t.
LaTeX
$$$\\text{centerMass of }(\\text{insert }i\\ t) = \\left(\\frac{w_i}{w_i+\\sum_{j\\in t} w_j}\\right) z_i + \\left(\\frac{\\sum_{j\\in t} w_j}{w_i+\\sum_{j\\in t} w_j}\\right) (t\\text{.centerMass } w z).$$$
Lean4
theorem centerMass_insert [DecidableEq ι] (ha : i ∉ t) (hw : ∑ j ∈ t, w j ≠ 0) :
(insert i t).centerMass w z =
(w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z :=
by
simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]
congr 2
rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]
