English
If there exists hx: x+1 ≤ 0, then for each n, the alternating geometric sum has sign ≤ 0 when n is even and sign ≥ 1 when n is odd.
Русский
Если существует hx: x+1 ≤ 0, то для каждого n чередующаяся геометрическая сумма имеет знак ≤ 0, если n чётно, и ≥ 1, если нечётно.
LaTeX
$$$\\forall n, (\\text{Even}(n) \\Rightarrow \\sum x^i \\le 0) \\land (\\lnot\\text{Even}(n) \\Rightarrow 1 \\le \\sum x^i)$$$
Lean4
theorem geom_sum_alternating_of_lt_neg_one (hx : x + 1 < 0) (hn : 1 < n) :
if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i :=
by
have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
· simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, hx, even_two]
clear hn
intro n _ ihn
simp only [Nat.even_add_one, geom_sum_succ]
by_cases hn' : Even n
· rw [if_pos hn'] at ihn
rw [if_neg, lt_add_iff_pos_left]
· exact mul_pos_of_neg_of_neg hx0 ihn
· exact not_not_intro hn'
· rw [if_neg hn'] at ihn
rw [if_pos]
swap
· exact hn'
have := add_lt_add_right (mul_lt_mul_of_neg_left ihn hx0) 1
rw [mul_one] at this
exact this.trans hx
