English
For a fixed vertex i, the sum over all j of excenterWeightsUnnorm {i} j is strictly positive.
Русский
Для фиксированного i сумма по j весов excenterWeightsUnnorm {i} j положительна.
LaTeX
$$$0 < \sum_j s.excenterWeightsUnnorm { i } j$$$
Lean4
theorem sum_excenterWeightsUnnorm_singleton_pos [Nat.AtLeastTwo n] (i : Fin (n + 1)) :
0 < ∑ j, s.excenterWeightsUnnorm { i } j :=
by
rw [← Finset.sum_add_sum_compl { i }, Finset.sum_singleton]
nth_rw 1 [excenterWeightsUnnorm]
simp only [Finset.mem_singleton, ↓reduceIte, neg_mul, one_mul, lt_neg_add_iff_add_lt, add_zero]
convert s.inv_height_lt_sum_inv_height i using 2 with j h
· ext j
simp
· rw [Finset.mem_filter_univ] at h
simp [excenterWeightsUnnorm, h]