English
For an (n+2)-simplex s, the Monge point M equals the weighted vector sum of the vertices relative to the circumcenter, with weights as in Sylvester's relation.
Русский
Для (n+2)-многоугольника MongePoint M выражается как взвешенная сумма вершин относительно описанной окружности с весами из баланса МонгеPoint.
LaTeX
$$$$ s.mongePoint = O + \sum_i w_i (P_i - O) \quad \text{with } w_i = \dfrac{1}{n+1}, \ w_{\text{circumcenter}} = -\dfrac{2}{n+1}. $$$$
Lean4
/-- **Sylvester's theorem**: The position of the Monge point relative to the circumcenter via the
sum of vectors to the vertices. -/
theorem smul_mongePoint_vsub_circumcenter_eq_sum_vsub {n : ℕ} (s : Simplex ℝ P (n + 2)) :
(n + 1) • (s.mongePoint -ᵥ s.circumcenter) = ∑ i, (s.points i -ᵥ s.circumcenter) :=
by
rw [mongePoint_eq_smul_vsub_vadd_circumcenter, vadd_vsub, ← smul_assoc]
simp only [Nat.cast_add, Nat.cast_ofNat, Nat.cast_one, Nat.add_one_sub_one, nsmul_eq_mul]
field_simp
have h : Invertible (n + 2 + 1 : ℝ) := by norm_cast; apply invertibleOfPos
rw [smul_eq_iff_eq_invOf_smul, smul_sum]
unfold Finset.centroid
rw [← Finset.sum_smul_vsub_const_eq_affineCombination_vsub _ _ _ _ (by simp)]
simp only [centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add, Nat.cast_ofNat, Nat.cast_one,
invOf_eq_inv]
