geom_sum_pos_iff — Mathlib

English

For any n, the sum is positive exactly under the conditions described by parity or x+1>0.

Русский

Для любого n сумма положительна точно при указанных условиях по четности или x+1>0.

LaTeX

$$$0 < \\sum_{i=0}^{n-1} x^i \\iff (\\text{Odd}(n) \\lor x+1>0)$$$

Lean4

theorem geom_sum_pos_iff (hn : n ≠ 0) : 0 < ∑ i ∈ range n, x ^ i ↔ Odd n ∨ 0 < x + 1 :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
    refine fun hn hx => h.not_ge ?_
    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
  · rintro (hn | hx')
    · exact hn.geom_sum_pos
    · exact geom_sum_pos' hx' hn

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