algebra.geom_sum

# Partial sums of geometric series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file determines 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 : ℕ.

## Main statements #

• geom_sum_Ico proves that $\sum_{i=m}^{n-1} x^i=\frac{x^n-x^m}{x-1}$ in a division ring.
• geom_sum₂_Ico proves that $\sum_{i=m}^{n-1} x^i=\frac{x^n-y^{n-m}x^m}{x-y}$ in a field.

Several variants are recorded, generalising in particular to the case of a noncommutative ring in which x and y commute. Even versions not using division or subtraction, valid in each semiring, are recorded.

theorem geom_sum_succ {α : Type u} [semiring α] {x : α} {n : } :
(finset.range (n + 1)).sum (λ (i : ), x ^ i) = x * (finset.range n).sum (λ (i : ), x ^ i) + 1
theorem geom_sum_succ' {α : Type u} [semiring α] {x : α} {n : } :
(finset.range (n + 1)).sum (λ (i : ), x ^ i) = x ^ n + (finset.range n).sum (λ (i : ), x ^ i)
theorem geom_sum_zero {α : Type u} [semiring α] (x : α) :
(finset.range 0).sum (λ (i : ), x ^ i) = 0
theorem geom_sum_one {α : Type u} [semiring α] (x : α) :
(finset.range 1).sum (λ (i : ), x ^ i) = 1
@[simp]
theorem geom_sum_two {α : Type u} [semiring α] {x : α} :
(finset.range 2).sum (λ (i : ), x ^ i) = x + 1
@[simp]
theorem zero_geom_sum {α : Type u} [semiring α] {n : } :
(finset.range n).sum (λ (i : ), 0 ^ i) = ite (n = 0) 0 1
theorem one_geom_sum {α : Type u} [semiring α] (n : ) :
(finset.range n).sum (λ (i : ), 1 ^ i) = n
@[simp]
theorem op_geom_sum {α : Type u} [semiring α] (x : α) (n : ) :
mul_opposite.op ((finset.range n).sum (λ (i : ), x ^ i)) = (finset.range n).sum (λ (i : ), ^ i)
@[simp]
theorem op_geom_sum₂ {α : Type u} [semiring α] (x y : α) (n : ) :
mul_opposite.op ((finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i))) = (finset.range n).sum (λ (i : ), * ^ (n - 1 - i))
theorem geom_sum₂_with_one {α : Type u} [semiring α] (x : α) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * 1 ^ (n - 1 - i)) = (finset.range n).sum (λ (i : ), x ^ i)
@[protected]
theorem commute.geom_sum₂_mul_add {α : Type u} [semiring α] {x y : α} (h : y) (n : ) :
(finset.range n).sum (λ (i : ), (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

$x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without - signs.

@[simp]
theorem neg_one_geom_sum {α : Type u} [ring α] {n : } :
(finset.range n).sum (λ (i : ), (-1) ^ i) = ite (even n) 0 1
theorem geom_sum₂_self {α : Type u_1} [comm_ring α] (x : α) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * x ^ (n - 1 - i)) = n * x ^ (n - 1)
theorem geom_sum₂_mul_add {α : Type u} (x y : α) (n : ) :
(finset.range n).sum (λ (i : ), (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

$x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without - signs.

theorem geom_sum_mul_add {α : Type u} [semiring α] (x : α) (n : ) :
(finset.range n).sum (λ (i : ), (x + 1) ^ i) * x + 1 = (x + 1) ^ n
@[protected]
theorem commute.geom_sum₂_mul {α : Type u} [ring α] {x y : α} (h : y) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
theorem commute.mul_neg_geom_sum₂ {α : Type u} [ring α] {x y : α} (h : y) (n : ) :
(y - x) * (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = y ^ n - x ^ n
theorem commute.mul_geom_sum₂ {α : Type u} [ring α] {x y : α} (h : y) (n : ) :
(x - y) * (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = x ^ n - y ^ n
theorem geom_sum₂_mul {α : Type u} [comm_ring α] (x y : α) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
theorem sub_dvd_pow_sub_pow {α : Type u} [comm_ring α] (x y : α) (n : ) :
x - y x ^ n - y ^ n
theorem nat_sub_dvd_pow_sub_pow (x y n : ) :
x - y x ^ n - y ^ n
theorem odd.add_dvd_pow_add_pow {α : Type u} [comm_ring α] (x y : α) {n : } (h : odd n) :
x + y x ^ n + y ^ n
theorem odd.nat_add_dvd_pow_add_pow (x y : ) {n : } (h : odd n) :
x + y x ^ n + y ^ n
theorem geom_sum_mul {α : Type u} [ring α] (x : α) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i) * (x - 1) = x ^ n - 1
theorem mul_geom_sum {α : Type u} [ring α] (x : α) (n : ) :
(x - 1) * (finset.range n).sum (λ (i : ), x ^ i) = x ^ n - 1
theorem geom_sum_mul_neg {α : Type u} [ring α] (x : α) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i) * (1 - x) = 1 - x ^ n
theorem mul_neg_geom_sum {α : Type u} [ring α] (x : α) (n : ) :
(1 - x) * (finset.range n).sum (λ (i : ), x ^ i) = 1 - x ^ n
@[protected]
theorem commute.geom_sum₂_comm {α : Type u} [semiring α] {x y : α} (n : ) (h : y) :
(finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = (finset.range n).sum (λ (i : ), y ^ i * x ^ (n - 1 - i))
theorem geom_sum₂_comm {α : Type u} (x y : α) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = (finset.range n).sum (λ (i : ), y ^ i * x ^ (n - 1 - i))
@[protected]
theorem commute.geom_sum₂ {α : Type u} {x y : α} (h' : y) (h : x y) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = (x ^ n - y ^ n) / (x - y)
theorem geom₂_sum {α : Type u} [field α] {x y : α} (h : x y) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = (x ^ n - y ^ n) / (x - y)
theorem geom_sum_eq {α : Type u} {x : α} (h : x 1) (n : ) :
(finset.range n).sum (λ (i : ), x ^ i) = (x ^ n - 1) / (x - 1)
@[protected]
theorem commute.mul_geom_sum₂_Ico {α : Type u} [ring α] {x y : α} (h : y) {m n : } (hmn : m n) :
(x - y) * n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m)
@[protected]
theorem commute.geom_sum₂_succ_eq {α : Type u} [ring α] {x y : α} (h : y) {n : } :
(finset.range (n + 1)).sum (λ (i : ), x ^ i * y ^ (n - i)) = x ^ n + y * (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i))
theorem geom_sum₂_succ_eq {α : Type u} [comm_ring α] (x y : α) {n : } :
(finset.range (n + 1)).sum (λ (i : ), x ^ i * y ^ (n - i)) = x ^ n + y * (finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i))
theorem mul_geom_sum₂_Ico {α : Type u} [comm_ring α] (x y : α) {m n : } (hmn : m n) :
(x - y) * n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m)
@[protected]
theorem commute.geom_sum₂_Ico_mul {α : Type u} [ring α] {x y : α} (h : y) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
theorem geom_sum_Ico_mul {α : Type u} [ring α] (x : α) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i) * (x - 1) = x ^ n - x ^ m
theorem geom_sum_Ico_mul_neg {α : Type u} [ring α] (x : α) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i) * (1 - x) = x ^ m - x ^ n
@[protected]
theorem commute.geom_sum₂_Ico {α : Type u} {x y : α} (h : y) (hxy : x y) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
theorem geom_sum₂_Ico {α : Type u} [field α] {x y : α} (hxy : x y) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i)) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
theorem geom_sum_Ico {α : Type u} {x : α} (hx : x 1) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i) = (x ^ n - x ^ m) / (x - 1)
theorem geom_sum_Ico' {α : Type u} {x : α} (hx : x 1) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i) = (x ^ m - x ^ n) / (1 - x)
theorem geom_sum_Ico_le_of_lt_one {α : Type u} {x : α} (hx : 0 x) (h'x : x < 1) {m n : } :
n).sum (λ (i : ), x ^ i) x ^ m / (1 - x)
theorem geom_sum_inv {α : Type u} {x : α} (hx1 : x 1) (hx0 : x 0) (n : ) :
(finset.range n).sum (λ (i : ), x⁻¹ ^ i) = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
theorem ring_hom.map_geom_sum {α : Type u} {β : Type u_1} [semiring α] [semiring β] (x : α) (n : ) (f : α →+* β) :
f ((finset.range n).sum (λ (i : ), x ^ i)) = (finset.range n).sum (λ (i : ), f x ^ i)
theorem ring_hom.map_geom_sum₂ {α : Type u} {β : Type u_1} [semiring α] [semiring β] (x y : α) (n : ) (f : α →+* β) :
f ((finset.range n).sum (λ (i : ), x ^ i * y ^ (n - 1 - i))) = (finset.range n).sum (λ (i : ), f x ^ i * f y ^ (n - 1 - i))

### Geometric sum with ℕ-division #

theorem nat.pred_mul_geom_sum_le (a b n : ) :
(b - 1) * (finset.range n.succ).sum (λ (i : ), a / b ^ i) a * b - a / b ^ n
theorem nat.geom_sum_le {b : } (hb : 2 b) (a n : ) :
(finset.range n).sum (λ (i : ), a / b ^ i) a * b / (b - 1)
theorem nat.geom_sum_Ico_le {b : } (hb : 2 b) (a n : ) :
n).sum (λ (i : ), a / b ^ i) a / (b - 1)
theorem geom_sum_pos {α : Type u} {n : } {x : α} (hx : 0 x) (hn : n 0) :
0 < (finset.range n).sum (λ (i : ), x ^ i)
theorem geom_sum_pos_and_lt_one {α : Type u} {n : } {x : α} (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
0 < (finset.range n).sum (λ (i : ), x ^ i) (finset.range n).sum (λ (i : ), x ^ i) < 1
theorem geom_sum_alternating_of_le_neg_one {α : Type u} {x : α} (hx : x + 1 0) (n : ) :
ite (even n) ((finset.range n).sum (λ (i : ), x ^ i) 0) (1 (finset.range n).sum (λ (i : ), x ^ i))
theorem geom_sum_alternating_of_lt_neg_one {α : Type u} {n : } {x : α} (hx : x + 1 < 0) (hn : 1 < n) :
ite (even n) ((finset.range n).sum (λ (i : ), x ^ i) < 0) (1 < (finset.range n).sum (λ (i : ), x ^ i))
theorem geom_sum_pos' {α : Type u} {n : } {x : α} (hx : 0 < x + 1) (hn : n 0) :
0 < (finset.range n).sum (λ (i : ), x ^ i)
theorem odd.geom_sum_pos {α : Type u} {n : } {x : α} (h : odd n) :
0 < (finset.range n).sum (λ (i : ), x ^ i)
theorem geom_sum_pos_iff {α : Type u} {n : } {x : α} (hn : n 0) :
0 < (finset.range n).sum (λ (i : ), x ^ i) odd n 0 < x + 1
theorem geom_sum_ne_zero {α : Type u} {n : } {x : α} (hx : x -1) (hn : n 0) :
(finset.range n).sum (λ (i : ), x ^ i) 0
theorem geom_sum_eq_zero_iff_neg_one {α : Type u} {n : } {x : α} (hn : n 0) :
(finset.range n).sum (λ (i : ), x ^ i) = 0 x = -1 even n
theorem geom_sum_neg_iff {α : Type u} {n : } {x : α} (hn : n 0) :
(finset.range n).sum (λ (i : ), x ^ i) < 0 even n x + 1 < 0