English
The centroid of fs vertices equals the affine combination of pointsWithCircumcenter with centroidWeightsWithCircumcenter fs.
Русский
Центроид вершин fs равен аффинной комбинации pointsWithCircumcenter с весами centroidWeightsWithCircumcenter fs.
LaTeX
$$$fs.centroid\;\mathrel{\_}\;\mathbb{R}\; s.points = (\univ : Finset (PointsWithCircumcenterIndex n)).affineCombination\; s.pointsWithCircumcenter\; (centroidWeightsWithCircumcenter fs)$$$
Lean4
/-- The centroid of some vertices of a simplex, in terms of `pointsWithCircumcenter`. -/
theorem centroid_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P n)
(fs : Finset (Fin (n + 1))) :
fs.centroid ℝ s.points =
(univ : Finset (PointsWithCircumcenterIndex n)).affineCombination ℝ s.pointsWithCircumcenter
(centroidWeightsWithCircumcenter fs) :=
by
simp_rw [centroid_def, affineCombination_apply, weightedVSubOfPoint_apply, sum_pointsWithCircumcenter,
centroidWeightsWithCircumcenter, pointsWithCircumcenter_point, zero_smul, add_zero, centroidWeights, ←
sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (#fs : ℝ)⁻¹)
(fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun _ => zero_smul ℝ _,
Set.indicator_apply]
congr
