Documentation

Mathlib.Algebra.GeomSum

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 #

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 {R : Type u_1} [Semiring R] {x : R} {n : } :
iFinset.range (n + 1), x ^ i = x * iFinset.range n, x ^ i + 1
theorem geom_sum_succ' {R : Type u_1} [Semiring R] {x : R} {n : } :
iFinset.range (n + 1), x ^ i = x ^ n + iFinset.range n, x ^ i
theorem geom_sum_zero {R : Type u_1} [Semiring R] (x : R) :
iFinset.range 0, x ^ i = 0
theorem geom_sum_one {R : Type u_1} [Semiring R] (x : R) :
iFinset.range 1, x ^ i = 1
@[simp]
theorem geom_sum_two {R : Type u_1} [Semiring R] {x : R} :
iFinset.range 2, x ^ i = x + 1
@[simp]
theorem zero_geom_sum {R : Type u_1} [Semiring R] {n : } :
iFinset.range n, 0 ^ i = if n = 0 then 0 else 1
theorem one_geom_sum {R : Type u_1} [Semiring R] (n : ) :
iFinset.range n, 1 ^ i = n
theorem op_geom_sum {R : Type u_1} [Semiring R] (x : R) (n : ) :
MulOpposite.op (∑ iFinset.range n, x ^ i) = iFinset.range n, MulOpposite.op x ^ i
@[simp]
theorem op_geom_sum₂ {R : Type u_1} [Semiring R] (x y : R) (n : ) :
iFinset.range n, MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i = iFinset.range n, MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
theorem geom_sum₂_with_one {R : Type u_1} [Semiring R] (x : R) (n : ) :
iFinset.range n, x ^ i * 1 ^ (n - 1 - i) = iFinset.range n, x ^ i
theorem Commute.geom_sum₂_mul_add {R : Type u_1} [Semiring R] {x y : R} (h : Commute x y) (n : ) :
(∑ iFinset.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 {R : Type u_1} [Ring R] {n : } :
iFinset.range n, (-1) ^ i = if Even n then 0 else 1
theorem geom_sum₂_self {R : Type u_3} [Semiring R] (x : R) (n : ) :
iFinset.range n, x ^ i * x ^ (n - 1 - i) = n * x ^ (n - 1)
theorem geom_sum₂_mul_add {R : Type u_1} [CommSemiring R] (x y : R) (n : ) :
(∑ iFinset.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 {R : Type u_1} [Semiring R] (x : R) (n : ) :
(∑ iFinset.range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
theorem Commute.geom_sum₂_mul {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ) :
(∑ iFinset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
theorem Commute.mul_neg_geom_sum₂ {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ) :
(y - x) * iFinset.range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
theorem Commute.mul_geom_sum₂ {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ) :
(x - y) * iFinset.range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
theorem geom_sum₂_mul {R : Type u_1} [CommRing R] (x y : R) (n : ) :
(∑ iFinset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
theorem geom_sum₂_mul_of_ge {R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : y x) (n : ) :
(∑ iFinset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
theorem geom_sum₂_mul_of_le {R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : x y) (n : ) :
(∑ iFinset.range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n
theorem Commute.sub_dvd_pow_sub_pow {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ) :
x - y x ^ n - y ^ n
theorem sub_dvd_pow_sub_pow {R : Type u_1} [CommRing R] (x y : R) (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 {R : Type u_1} [Ring R] (x : R) (n : ) :
1 - x 1 - x ^ n
theorem sub_one_dvd_pow_sub_one {R : Type u_1} [Ring R] (x : R) (n : ) :
x - 1 x ^ n - 1
theorem pow_one_sub_dvd_pow_mul_sub_one {R : Type u_1} [Ring R] (x : R) (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 {R : Type u_1} [CommRing R] (x y : R) {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 {R : Type u_1} [Ring R] (x : R) (n : ) :
(∑ iFinset.range n, x ^ i) * (x - 1) = x ^ n - 1
theorem geom_sum_mul_of_one_le {R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : 1 x) (n : ) :
(∑ iFinset.range n, x ^ i) * (x - 1) = x ^ n - 1
theorem geom_sum_mul_of_le_one {R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : x 1) (n : ) :
(∑ iFinset.range n, x ^ i) * (1 - x) = 1 - x ^ n
theorem mul_geom_sum {R : Type u_1} [Ring R] (x : R) (n : ) :
(x - 1) * iFinset.range n, x ^ i = x ^ n - 1
theorem geom_sum_mul_neg {R : Type u_1} [Ring R] (x : R) (n : ) :
(∑ iFinset.range n, x ^ i) * (1 - x) = 1 - x ^ n
theorem mul_neg_geom_sum {R : Type u_1} [Ring R] (x : R) (n : ) :
(1 - x) * iFinset.range n, x ^ i = 1 - x ^ n
theorem Commute.geom_sum₂_comm {R : Type u_1} [Semiring R] {x y : R} (n : ) (h : Commute x y) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = iFinset.range n, y ^ i * x ^ (n - 1 - i)
theorem geom_sum₂_comm {R : Type u_1} [CommSemiring R] (x y : R) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = iFinset.range n, y ^ i * x ^ (n - 1 - i)
theorem Commute.geom_sum₂ {K : Type u_2} [DivisionRing K] {x y : K} (h' : Commute x y) (h : x y) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
theorem geom₂_sum {K : Type u_2} [Field K] {x y : K} (h : x y) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
theorem geom₂_sum_of_gt {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x y : K} (h : y < x) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
theorem geom₂_sum_of_lt {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x y : K} (h : x < y) (n : ) :
iFinset.range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)
theorem geom_sum_eq {K : Type u_2} [DivisionRing K] {x : K} (h : x 1) (n : ) :
iFinset.range n, x ^ i = (x ^ n - 1) / (x - 1)
theorem geom_sum_of_one_lt {K : Type u_2} {x : K} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] (h : 1 < x) (n : ) :
iFinset.range n, x ^ i = (x ^ n - 1) / (x - 1)
theorem geom_sum_of_lt_one {K : Type u_2} {x : K} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] (h : x < 1) (n : ) :
iFinset.range n, x ^ i = (1 - x ^ n) / (1 - x)
theorem geom_sum_lt {K : Type u_2} {x : K} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] (h0 : x 0) (h1 : x < 1) (n : ) :
iFinset.range n, x ^ i < (1 - x)⁻¹
theorem Commute.mul_geom_sum₂_Ico {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) {m n : } (hmn : m n) :
(x - y) * iFinset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
theorem Commute.geom_sum₂_succ_eq {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) {n : } :
iFinset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * iFinset.range n, x ^ i * y ^ (n - 1 - i)
theorem geom_sum₂_succ_eq {R : Type u_1} [CommRing R] (x y : R) {n : } :
iFinset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * iFinset.range n, x ^ i * y ^ (n - 1 - i)
theorem mul_geom_sum₂_Ico {R : Type u_1} [CommRing R] (x y : R) {m n : } (hmn : m n) :
(x - y) * iFinset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
theorem Commute.geom_sum₂_Ico_mul {R : Type u_1} [Ring R] {x y : R} (h : Commute x y) {m n : } (hmn : m n) :
(∑ iFinset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
theorem geom_sum_Ico_mul {R : Type u_1} [Ring R] (x : R) {m n : } (hmn : m n) :
(∑ iFinset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
theorem geom_sum_Ico_mul_neg {R : Type u_1} [Ring R] (x : R) {m n : } (hmn : m n) :
(∑ iFinset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
theorem Commute.geom_sum₂_Ico {K : Type u_2} [DivisionRing K] {x y : K} (h : Commute x y) (hxy : x y) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
theorem geom_sum₂_Ico {K : Type u_2} [Field K] {x y : K} (hxy : x y) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
theorem geom_sum_Ico {K : Type u_2} [DivisionRing K] {x : K} (hx : x 1) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
theorem geom_sum_Ico' {K : Type u_2} [DivisionRing K] {x : K} (hx : x 1) {m n : } (hmn : m n) :
iFinset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
theorem geom_sum_Ico_le_of_lt_one {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {x : K} (hx : 0 x) (h'x : x < 1) {m n : } :
iFinset.Ico m n, x ^ i x ^ m / (1 - x)
theorem geom_sum_inv {K : Type u_2} [DivisionRing K] {x : K} (hx1 : x 1) (hx0 : x 0) (n : ) :
iFinset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
theorem RingHom.map_geom_sum {R : Type u_1} {S : Type u_3} [Semiring R] [Semiring S] (x : R) (n : ) (f : R →+* S) :
f (∑ iFinset.range n, x ^ i) = iFinset.range n, f x ^ i
theorem RingHom.map_geom_sum₂ {R : Type u_1} {S : Type u_3} [Semiring R] [Semiring S] (x y : R) (n : ) (f : R →+* S) :
f (∑ iFinset.range n, x ^ i * y ^ (n - 1 - i)) = iFinset.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) * 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 geom_sum_pos {R : Type u_1} {n : } {x : R} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (hx : 0 x) (hn : n 0) :
0 < iFinset.range n, x ^ i
theorem geom_sum_pos_and_lt_one {R : Type u_1} {n : } {x : R} [Ring R] [PartialOrder R] [IsStrictOrderedRing 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_le_neg_one {R : Type u_1} {x : R} [Ring R] [PartialOrder R] [IsStrictOrderedRing 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_alternating_of_lt_neg_one {R : Type u_1} {n : } {x : R} [Ring R] [PartialOrder R] [IsStrictOrderedRing 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} {n : } {x : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hx : 0 < x + 1) (hn : n 0) :
0 < iFinset.range n, x ^ i
theorem Odd.geom_sum_pos {R : Type u_1} {n : } {x : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (h : Odd n) :
0 < iFinset.range n, x ^ i
theorem geom_sum_pos_iff {R : Type u_1} {n : } {x : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n 0) :
0 < iFinset.range n, x ^ i Odd n 0 < x + 1
theorem geom_sum_ne_zero {R : Type u_1} {n : } {x : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing 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} {n : } {x : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n 0) :
iFinset.range n, x ^ i = 0 x = -1 Even n
theorem geom_sum_neg_iff {R : Type u_1} {n : } {x : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n 0) :
iFinset.range n, x ^ i < 0 Even n x + 1 < 0
theorem Nat.geomSum_eq {m : } (hm : 2 m) (n : ) :
kFinset.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 : 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.