geom_sum_pos' — Mathlib

English

If 0 < x+1 and n ≠ 0, then the geometric sum ∑ x^i is positive.

Русский

Если 0 < x+1 и n ≠ 0, то геометрическая сумма положительна.

LaTeX

$$$0 < x+1 \\text{ and } n \\neq 0 \\Rightarrow 0 < \\sum_{i=0}^{n-1} x^i$$$

Lean4

theorem geom_sum_pos' (hx : 0 < x + 1) (hn : n ≠ 0) : 0 < ∑ i ∈ range n, x ^ i :=
  by
  obtain _ | _ | n := n
  · cases hn rfl
  · simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]
  obtain hx' | hx' := lt_or_ge x 0
  · exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1
  · exact geom_sum_pos hx' (by simp only [Nat.succ_ne_zero, Ne, not_false_iff])

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