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_Icoproves that $\sum_{i=m}^{n-1} x^i=\frac{x^n-x^m}{x-1}$ in a division ring.geom_sum₂_Icoproves 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 : ℕ}
:
(Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => x ^ i) = (x * Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) + 1
theorem
geom_sum_succ'
{α : Type u}
[Semiring α]
{x : α}
{n : ℕ}
:
(Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => x ^ i) = x ^ n + Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i
theorem
geom_sum_zero
{α : Type u}
[Semiring α]
(x : α)
:
(Finset.sum (Finset.range 0) fun (i : ℕ) => x ^ i) = 0
theorem
geom_sum_one
{α : Type u}
[Semiring α]
(x : α)
:
(Finset.sum (Finset.range 1) fun (i : ℕ) => x ^ i) = 1
@[simp]
theorem
geom_sum_two
{α : Type u}
[Semiring α]
{x : α}
:
(Finset.sum (Finset.range 2) fun (i : ℕ) => x ^ i) = x + 1
@[simp]
theorem
zero_geom_sum
{α : Type u}
[Semiring α]
{n : ℕ}
:
(Finset.sum (Finset.range n) fun (i : ℕ) => 0 ^ i) = if n = 0 then 0 else 1
theorem
one_geom_sum
{α : Type u}
[Semiring α]
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => 1 ^ i) = ↑n
theorem
op_geom_sum
{α : Type u}
[Semiring α]
(x : α)
(n : ℕ)
:
MulOpposite.op (Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) = Finset.sum (Finset.range n) fun (i : ℕ) => MulOpposite.op x ^ i
@[simp]
theorem
op_geom_sum₂
{α : Type u}
[Semiring α]
(x : α)
(y : α)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i) = Finset.sum (Finset.range n) fun (i : ℕ) => MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
theorem
geom_sum₂_with_one
{α : Type u}
[Semiring α]
(x : α)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i * 1 ^ (n - 1 - i)) = Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i
@[simp]
theorem
neg_one_geom_sum
{α : Type u}
[Ring α]
{n : ℕ}
:
(Finset.sum (Finset.range n) fun (i : ℕ) => (-1) ^ i) = if Even n then 0 else 1
$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.sum (Finset.range n) fun (i : ℕ) => (x + 1) ^ i) * x + 1 = (x + 1) ^ n
theorem
geom_sum_mul
{α : Type u}
[Ring α]
(x : α)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) * (x - 1) = x ^ n - 1
theorem
mul_geom_sum
{α : Type u}
[Ring α]
(x : α)
(n : ℕ)
:
((x - 1) * Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) = x ^ n - 1
theorem
geom_sum_mul_neg
{α : Type u}
[Ring α]
(x : α)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) * (1 - x) = 1 - x ^ n
theorem
mul_neg_geom_sum
{α : Type u}
[Ring α]
(x : α)
(n : ℕ)
:
((1 - x) * Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) = 1 - x ^ n
theorem
Commute.geom_sum₂_comm
{α : Type u}
[Semiring α]
{x : α}
{y : α}
(n : ℕ)
(h : Commute x y)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i * y ^ (n - 1 - i)) = Finset.sum (Finset.range n) fun (i : ℕ) => y ^ i * x ^ (n - 1 - i)
theorem
geom_sum₂_comm
{α : Type u}
[CommSemiring α]
(x : α)
(y : α)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i * y ^ (n - 1 - i)) = Finset.sum (Finset.range n) fun (i : ℕ) => y ^ i * x ^ (n - 1 - i)
theorem
geom_sum_eq
{α : Type u}
[DivisionRing α]
{x : α}
(h : x ≠ 1)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) = (x ^ n - 1) / (x - 1)
theorem
geom_sum₂_succ_eq
{α : Type u}
[CommRing α]
(x : α)
(y : α)
{n : ℕ}
:
(Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => x ^ i * y ^ (n - i)) = x ^ n + y * Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i * y ^ (n - 1 - i)
theorem
geom_sum_Ico
{α : Type u}
[DivisionRing α]
{x : α}
(hx : x ≠ 1)
{m : ℕ}
{n : ℕ}
(hmn : m ≤ n)
:
(Finset.sum (Finset.Ico m n) fun (i : ℕ) => x ^ i) = (x ^ n - x ^ m) / (x - 1)
theorem
geom_sum_Ico'
{α : Type u}
[DivisionRing α]
{x : α}
(hx : x ≠ 1)
{m : ℕ}
{n : ℕ}
(hmn : m ≤ n)
:
(Finset.sum (Finset.Ico m n) fun (i : ℕ) => 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 : ℕ}
:
(Finset.sum (Finset.Ico m n) fun (i : ℕ) => x ^ i) ≤ x ^ m / (1 - x)
theorem
RingHom.map_geom_sum
{α : Type u}
{β : Type u_1}
[Semiring α]
[Semiring β]
(x : α)
(n : ℕ)
(f : α →+* β)
:
f (Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) = Finset.sum (Finset.range n) fun (i : ℕ) => f x ^ i
theorem
RingHom.map_geom_sum₂
{α : Type u}
{β : Type u_1}
[Semiring α]
[Semiring β]
(x : α)
(y : α)
(n : ℕ)
(f : α →+* β)
:
f (Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i * y ^ (n - 1 - i)) = Finset.sum (Finset.range n) fun (i : ℕ) => f x ^ i * f y ^ (n - 1 - i)
Geometric sum with ℕ-division #
theorem
Nat.geom_sum_le
{b : ℕ}
(hb : 2 ≤ b)
(a : ℕ)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => a / b ^ i) ≤ a * b / (b - 1)
theorem
Nat.geom_sum_Ico_le
{b : ℕ}
(hb : 2 ≤ b)
(a : ℕ)
(n : ℕ)
:
(Finset.sum (Finset.Ico 1 n) fun (i : ℕ) => a / b ^ i) ≤ a / (b - 1)
theorem
geom_sum_pos
{α : Type u}
{n : ℕ}
{x : α}
[StrictOrderedSemiring α]
(hx : 0 ≤ x)
(hn : n ≠ 0)
:
0 < Finset.sum (Finset.range n) fun (i : ℕ) => 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 < Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) ∧ (Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) < 1
theorem
geom_sum_alternating_of_le_neg_one
{α : Type u}
{x : α}
[StrictOrderedRing α]
(hx : x + 1 ≤ 0)
(n : ℕ)
:
if Even n then (Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) ≤ 0
else 1 ≤ Finset.sum (Finset.range n) fun (i : ℕ) => 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 (Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) < 0
else 1 < Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i
theorem
geom_sum_pos'
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hx : 0 < x + 1)
(hn : n ≠ 0)
:
0 < Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i
theorem
Odd.geom_sum_pos
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(h : Odd n)
:
0 < Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i
theorem
geom_sum_pos_iff
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hn : n ≠ 0)
:
(0 < Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) ↔ Odd n ∨ 0 < x + 1
theorem
geom_sum_ne_zero
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hx : x ≠ -1)
(hn : n ≠ 0)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) ≠ 0
theorem
geom_sum_eq_zero_iff_neg_one
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hn : n ≠ 0)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) = 0 ↔ x = -1 ∧ Even n
theorem
geom_sum_neg_iff
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hn : n ≠ 0)
:
(Finset.sum (Finset.range n) fun (i : ℕ) => x ^ i) < 0 ↔ Even n ∧ x + 1 < 0
theorem
Nat.geomSum_eq
{m : ℕ}
(hm : 2 ≤ m)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun (k : ℕ) => m ^ k) = (m ^ n - 1) / (m - 1)
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.