Partial sums of geometric series in an ordered ring

This file upper- and lower-bounds the values of the geometric series $\sum_{i=0}^{n-1} x^i$ and $\sum_{i=0}^{n-1} x^i y^{n-1-i}$ and variants thereof. We also provide some bounds on the "geometric" sum of a/b^i where a b : ℕ.

theorem geom_sum_pos {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : 0 ≤ x) (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_alternating_of_le_neg_one {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] {x : R} (hx : x + 1 ≤ 0) (n : ℕ) : if Even n then ∑ i ∈ Finset.range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_pos_and_lt_one {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) : 0 < ∑ i ∈ Finset.range n, x ^ i ∧ ∑ i ∈ Finset.range n, x ^ i < 1

theorem geom_sum_alternating_of_lt_neg_one {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : x + 1 < 0) (hn : 1 < n) : if Even n then ∑ i ∈ Finset.range n, x ^ i < 0 else 1 < ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_pos' {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : 0 < x + 1) (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i

theorem Odd.geom_sum_pos {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (h : Odd n) : 0 < ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_pos_iff {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i ↔ Odd n ∨ 0 < x + 1

theorem geom_sum_ne_zero {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : x ≠ -1) (hn : n ≠ 0) : ∑ i ∈ Finset.range n, x ^ i ≠ 0

theorem geom_sum_eq_zero_iff_neg_one {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hn : n ≠ 0) : ∑ i ∈ Finset.range n, x ^ i = 0 ↔ x = -1 ∧ Even n

theorem geom_sum_neg_iff {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hn : n ≠ 0) : ∑ i ∈ Finset.range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

Geometric sum with ℕ-division

theorem Nat.pred_mul_geom_sum_le (a b n : ℕ) : (b - 1) * ∑ i ∈ Finset.range n.succ, a / b ^ i ≤ a * b - a / b ^ n

theorem Nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i ∈ Finset.range n, a / b ^ i ≤ a * b / (b - 1)

theorem Nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i ∈ Finset.Ico 1 n, a / b ^ i ≤ a / (b - 1)

theorem Nat.geomSum_lt {m n : ℕ} {s : Finset ℕ} (hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k ∈ s, m ^ k < m ^ n

If all the elements of a finset of naturals are less than n, then the sum of their powers of m ≥ 2 is less than m ^ n.