English
The normalized weights of the vertices in an affine combination giving an excenter are given by the unnormalized weights scaled by the reciprocal of their sum.
Русский
Нормированные веса вершин в аффинной комбинации, задающей эксцентр, получаются путём масштабирования ненормированных весов на обратную величину их суммы.
LaTeX
$$$\text{excenterWeights}(signs) : Fin (n+1) \to \mathbb{R} = (\sum_i s.excenterWeightsUnnorm(signs,i))^{-1} \cdot s.excenterWeightsUnnorm(signs)$$$
Lean4
/-- The normalized weights of the vertices in an affine combination that gives an excenter with
signs determined by the given set of indices. An excenter with those signs exists if and only if
the sum of these weights is 1. -/
def excenterWeights (signs : Finset (Fin (n + 1))) : Fin (n + 1) → ℝ :=
(∑ i, s.excenterWeightsUnnorm signs i)⁻¹ • s.excenterWeightsUnnorm signs
