English
If x ≤ 0 and x + 1 ≤ 0, then for all n, the alternating geometric sum satisfies certain sign bounds: either sum ≤ 0 or sum ≥ 1 depending on parity.
Русский
Если x ≤ 0 и x + 1 ≤ 0, тогда для любого n чередующая геометрическая сумма имеет знак: либо сумма ≤ 0, либо сумма ≥ 1 в зависимости от паритета.
LaTeX
$$$\\text{If } x \\le 0\\text{ and } x+1 \\le 0, \\text{ then } (\\text{Even } n) \\Rightarrow \\sum x^i \\le 0 \\text{ and } (\\text{Odd } n) \\Rightarrow 1 \\le \\sum x^i$$$
Lean4
theorem geom_sum_pos_and_lt_one (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 :=
by
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
· rw [geom_sum_two]
exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
clear hn
intro n _ ihn
rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
exact
⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
mul_neg_of_neg_of_pos hx ihn.1⟩
