English
For a finite set fs of vertex indices, centroidWeightsWithCircumcenter fs gives weights such that the centroid of the corresponding vertices with respect to s.pointsWithCircumcenter equals the barycenter of those vertices.
Русский
Для конечного множества fs индексов вершин centroidWeightsWithCircumcenter fs задаёт веса, чтобы центроид соответствующих вершин по отношению к s.pointsWithCircumcenter совпал с барицентром этих вершин.
LaTeX
$$$\text{centroidWeightsWithCircumcenter} : (fs : Finset (Fin (n+1))) \to (PointsWithCircumcenterIndex n \to \mathbb{R})$$$
Lean4
/-- The weights for the centroid of some vertices of a simplex, in
terms of `pointsWithCircumcenter`. -/
def centroidWeightsWithCircumcenter {n : ℕ} (fs : Finset (Fin (n + 1))) : PointsWithCircumcenterIndex n → ℝ
| pointIndex i => if i ∈ fs then (#fs : ℝ)⁻¹ else 0
| circumcenterIndex => 0
