Partial sums of geometric series

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^iy^{n - 1 - 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 : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i = x * ∑ i ∈ Finset.range n, x ^ i + 1

theorem geom_sum_succ' {α : Type u} [Semiring α] {x : α} {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i = x ^ n + ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_zero {α : Type u} [Semiring α] (x : α) : ∑ i ∈ Finset.range 0, x ^ i = 0

theorem geom_sum_one {α : Type u} [Semiring α] (x : α) : ∑ i ∈ Finset.range 1, x ^ i = 1

@[simp]

theorem geom_sum_two {α : Type u} [Semiring α] {x : α} : ∑ i ∈ Finset.range 2, x ^ i = x + 1

@[simp]

theorem zero_geom_sum {α : Type u} [Semiring α] {n : ℕ} : ∑ i ∈ Finset.range n, 0 ^ i = if n = 0 then 0 else 1

theorem one_geom_sum {α : Type u} [Semiring α] (n : ℕ) : ∑ i ∈ Finset.range n, 1 ^ i = ↑n

theorem op_geom_sum {α : Type u} [Semiring α] (x : α) (n : ℕ) : MulOpposite.op (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, MulOpposite.op x ^ i

@[simp]

theorem op_geom_sum₂ {α : Type u} [Semiring α] (x y : α) (n : ℕ) : ∑ i ∈ Finset.range n, MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i = ∑ i ∈ Finset.range n, MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)

theorem geom_sum₂_with_one {α : Type u} [Semiring α] (x : α) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ Finset.range n, x ^ i

theorem Commute.geom_sum₂_mul_add {α : Type u} [Semiring α] {x y : α} (h : Commute x y) (n : ℕ) : (∑ i ∈ Finset.range n, (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 : ℕ} : ∑ i ∈ Finset.range n, (-1) ^ i = if Even n then 0 else 1

theorem geom_sum₂_self {α : Type u_1} [CommRing α] (x : α) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) = ↑n * x ^ (n - 1)

theorem geom_sum₂_mul_add {α : Type u} [CommSemiring α] (x y : α) (n : ℕ) : (∑ i ∈ Finset.range n, (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 : ℕ) : (∑ i ∈ Finset.range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

theorem Commute.geom_sum₂_mul {α : Type u} [Ring α] {x y : α} (h : Commute x y) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

theorem Commute.mul_neg_geom_sum₂ {α : Type u} [Ring α] {x y : α} (h : Commute x y) (n : ℕ) : (y - x) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n

theorem Commute.mul_geom_sum₂ {α : Type u} [Ring α] {x y : α} (h : Commute x y) (n : ℕ) : (x - y) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n

theorem geom_sum₂_mul {α : Type u} [CommRing α] (x y : α) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

theorem geom_sum₂_mul_of_ge {α : Type u} [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : y ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

theorem geom_sum₂_mul_of_le {α : Type u} [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : x ≤ y) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

theorem Commute.sub_dvd_pow_sub_pow {α : Type u} [Ring α] {x y : α} (h : Commute x y) (n : ℕ) : x - y ∣ x ^ n - y ^ n

theorem sub_dvd_pow_sub_pow {α : Type u} [CommRing α] (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 one_sub_dvd_one_sub_pow {α : Type u} [Ring α] (x : α) (n : ℕ) : 1 - x ∣ 1 - x ^ n

theorem sub_one_dvd_pow_sub_one {α : Type u} [Ring α] (x : α) (n : ℕ) : x - 1 ∣ x ^ n - 1

theorem pow_one_sub_dvd_pow_mul_sub_one {α : Type u} [Ring α] (x : α) (m n : ℕ) : x ^ m - 1 ∣ x ^ (m * n) - 1

theorem nat_pow_one_sub_dvd_pow_mul_sub_one (x m n : ℕ) : x ^ m - 1 ∣ x ^ (m * n) - 1

theorem Odd.add_dvd_pow_add_pow {α : Type u} [CommRing α] (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 : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1

theorem geom_sum_mul_of_one_le {α : Type u} [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x : α} (hx : 1 ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1

theorem geom_sum_mul_of_le_one {α : Type u} [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x : α} (hx : x ≤ 1) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n

theorem mul_geom_sum {α : Type u} [Ring α] (x : α) (n : ℕ) : (x - 1) * ∑ i ∈ Finset.range n, x ^ i = x ^ n - 1

theorem geom_sum_mul_neg {α : Type u} [Ring α] (x : α) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n

theorem mul_neg_geom_sum {α : Type u} [Ring α] (x : α) (n : ℕ) : (1 - x) * ∑ i ∈ Finset.range n, x ^ i = 1 - x ^ n

theorem Commute.geom_sum₂_comm {α : Type u} [Semiring α] {x y : α} (n : ℕ) (h : Commute x y) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)

theorem geom_sum₂_comm {α : Type u} [CommSemiring α] (x y : α) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)

theorem Commute.geom_sum₂ {α : Type u} [DivisionRing α] {x y : α} (h' : Commute x y) (h : x ≠ y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

theorem geom₂_sum {α : Type u} [Field α] {x y : α} (h : x ≠ y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

theorem geom₂_sum_of_gt {α : Type u_1} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] {x y : α} (h : y < x) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

theorem geom₂_sum_of_lt {α : Type u_1} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] {x y : α} (h : x < y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)

theorem geom_sum_eq {α : Type u} [DivisionRing α] {x : α} (h : x ≠ 1) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)

theorem geom_sum_of_one_lt {α : Type u} {x : α} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] (h : 1 < x) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)

theorem geom_sum_of_lt_one {α : Type u} {x : α} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] (h : x < 1) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x)

theorem Commute.mul_geom_sum₂_Ico {α : Type u} [Ring α] {x y : α} (h : Commute x y) {m n : ℕ} (hmn : m ≤ n) : (x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

theorem Commute.geom_sum₂_succ_eq {α : Type u} [Ring α] {x y : α} (h : Commute x y) {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)

theorem geom_sum₂_succ_eq {α : Type u} [CommRing α] (x y : α) {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)

theorem mul_geom_sum₂_Ico {α : Type u} [CommRing α] (x y : α) {m n : ℕ} (hmn : m ≤ n) : (x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

theorem Commute.geom_sum₂_Ico_mul {α : Type u} [Ring α] {x y : α} (h : Commute x y) {m n : ℕ} (hmn : m ≤ n) : (∑ i ∈ Finset.Ico m n, 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) : (∑ i ∈ Finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m

theorem geom_sum_Ico_mul_neg {α : Type u} [Ring α] (x : α) {m n : ℕ} (hmn : m ≤ n) : (∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

theorem Commute.geom_sum₂_Ico {α : Type u} [DivisionRing α] {x y : α} (h : Commute x y) (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, 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) : ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

theorem geom_sum_Ico {α : Type u} [DivisionRing α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

theorem geom_sum_Ico' {α : Type u} [DivisionRing α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)

theorem geom_sum_Ico_le_of_lt_one {α : Type u} [LinearOrderedField α] {x : α} (hx : 0 ≤ x) (h'x : x < 1) {m n : ℕ} : ∑ i ∈ Finset.Ico m n, x ^ i ≤ x ^ m / (1 - x)

theorem geom_sum_inv {α : Type u} [DivisionRing α] {x : α} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) : ∑ i ∈ Finset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

theorem RingHom.map_geom_sum {α : Type u} {β : Type u_1} [Semiring α] [Semiring β] (x : α) (n : ℕ) (f : α →+* β) : f (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, f x ^ i

theorem RingHom.map_geom_sum₂ {α : Type u} {β : Type u_1} [Semiring α] [Semiring β] (x y : α) (n : ℕ) (f : α →+* β) : f (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ Finset.range n, f x ^ i * f y ^ (n - 1 - i)

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 geom_sum_pos {α : Type u} {n : ℕ} {x : α} [StrictOrderedSemiring α] (hx : 0 ≤ x) (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_pos_and_lt_one {α : Type u} {n : ℕ} {x : α} [StrictOrderedRing α] (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_le_neg_one {α : Type u} {x : α} [StrictOrderedRing α] (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_alternating_of_lt_neg_one {α : Type u} {n : ℕ} {x : α} [StrictOrderedRing α] (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' {α : Type u} {n : ℕ} {x : α} [LinearOrderedRing α] (hx : 0 < x + 1) (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i

theorem Odd.geom_sum_pos {α : Type u} {n : ℕ} {x : α} [LinearOrderedRing α] (h : Odd n) : 0 < ∑ i ∈ Finset.range n, x ^ i

theorem geom_sum_pos_iff {α : Type u} {n : ℕ} {x : α} [LinearOrderedRing α] (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i ↔ Odd n ∨ 0 < x + 1

theorem geom_sum_ne_zero {α : Type u} {n : ℕ} {x : α} [LinearOrderedRing α] (hx : x ≠ -1) (hn : n ≠ 0) : ∑ i ∈ Finset.range n, x ^ i ≠ 0

theorem geom_sum_eq_zero_iff_neg_one {α : Type u} {n : ℕ} {x : α} [LinearOrderedRing α] (hn : n ≠ 0) : ∑ i ∈ Finset.range n, x ^ i = 0 ↔ x = -1 ∧ Even n

theorem geom_sum_neg_iff {α : Type u} {n : ℕ} {x : α} [LinearOrderedRing α] (hn : n ≠ 0) : ∑ i ∈ Finset.range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

theorem Nat.geomSum_eq {m : ℕ} (hm : 2 ≤ m) (n : ℕ) : ∑ k ∈ Finset.range n, m ^ k = (m ^ n - 1) / (m - 1)

Value of a geometric sum over the naturals. Note: see geom_sum_mul_add for a formulation that avoids division and subtraction.

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.