Documentation

Mathlib.Algebra.Order.Ring.GeomSum

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 < iFinset.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 iFinset.range n, x ^ i 0 else 1 iFinset.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 < iFinset.range n, x ^ i iFinset.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 iFinset.range n, x ^ i < 0 else 1 < iFinset.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 < iFinset.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 < iFinset.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 < iFinset.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) :
iFinset.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) :
iFinset.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) :
iFinset.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) * iFinset.range n.succ, a / b ^ i a * b - a / b ^ n
theorem Nat.geom_sum_le {b : } (hb : 2 b) (a n : ) :
iFinset.range n, a / b ^ i a * b / (b - 1)
theorem Nat.geom_sum_Ico_le {b : } (hb : 2 b) (a n : ) :
iFinset.Ico 1 n, a / b ^ i a / (b - 1)
theorem Nat.geomSum_lt {m n : } {s : Finset } (hm : 2 m) (hs : ks, k < n) :
ks, 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.