sum_excenterWeightsUnnorm_singleton_pos

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]

Похожие утверждения