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 : ℕ}
:
((Finset.range (n + 1)).sum fun (i : ℕ) => x ^ i) = (x * (Finset.range n).sum fun (i : ℕ) => x ^ i) + 1
theorem
geom_sum_succ'
{α : Type u}
[Semiring α]
{x : α}
{n : ℕ}
:
((Finset.range (n + 1)).sum fun (i : ℕ) => x ^ i) = x ^ n + (Finset.range n).sum fun (i : ℕ) => x ^ i
theorem
geom_sum_zero
{α : Type u}
[Semiring α]
(x : α)
:
((Finset.range 0).sum fun (i : ℕ) => x ^ i) = 0
theorem
geom_sum_one
{α : Type u}
[Semiring α]
(x : α)
:
((Finset.range 1).sum fun (i : ℕ) => x ^ i) = 1
@[simp]
theorem
geom_sum_two
{α : Type u}
[Semiring α]
{x : α}
:
((Finset.range 2).sum fun (i : ℕ) => x ^ i) = x + 1
@[simp]
theorem
zero_geom_sum
{α : Type u}
[Semiring α]
{n : ℕ}
:
((Finset.range n).sum fun (i : ℕ) => 0 ^ i) = if n = 0 then 0 else 1
theorem
one_geom_sum
{α : Type u}
[Semiring α]
(n : ℕ)
:
((Finset.range n).sum fun (i : ℕ) => 1 ^ i) = ↑n
theorem
op_geom_sum
{α : Type u}
[Semiring α]
(x : α)
(n : ℕ)
:
MulOpposite.op ((Finset.range n).sum fun (i : ℕ) => x ^ i) = (Finset.range n).sum fun (i : ℕ) => MulOpposite.op x ^ i
@[simp]
theorem
op_geom_sum₂
{α : Type u}
[Semiring α]
(x : α)
(y : α)
(n : ℕ)
:
((Finset.range n).sum fun (i : ℕ) => MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i) = (Finset.range n).sum fun (i : ℕ) => MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
@[simp]
theorem
neg_one_geom_sum
{α : Type u}
[Ring α]
{n : ℕ}
:
((Finset.range n).sum fun (i : ℕ) => (-1) ^ i) = if Even n then 0 else 1
theorem
geom_sum_Ico_le_of_lt_one
{α : Type u}
[LinearOrderedField α]
{x : α}
(hx : 0 ≤ x)
(h'x : x < 1)
{m : ℕ}
{n : ℕ}
:
theorem
RingHom.map_geom_sum
{α : Type u}
{β : Type u_1}
[Semiring α]
[Semiring β]
(x : α)
(n : ℕ)
(f : α →+* β)
:
f ((Finset.range n).sum fun (i : ℕ) => x ^ i) = (Finset.range n).sum fun (i : ℕ) => f x ^ i
Geometric sum with ℕ
-division #
theorem
geom_sum_pos
{α : Type u}
{n : ℕ}
{x : α}
[StrictOrderedSemiring α]
(hx : 0 ≤ x)
(hn : n ≠ 0)
:
0 < (Finset.range n).sum 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.range n).sum fun (i : ℕ) => x ^ i) ∧ ((Finset.range n).sum 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.range n).sum fun (i : ℕ) => x ^ i) ≤ 0 else 1 ≤ (Finset.range n).sum 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.range n).sum fun (i : ℕ) => x ^ i) < 0 else 1 < (Finset.range n).sum fun (i : ℕ) => x ^ i
theorem
geom_sum_pos'
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hx : 0 < x + 1)
(hn : n ≠ 0)
:
0 < (Finset.range n).sum fun (i : ℕ) => x ^ i
theorem
Odd.geom_sum_pos
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(h : Odd n)
:
0 < (Finset.range n).sum fun (i : ℕ) => x ^ i
theorem
geom_sum_ne_zero
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hx : x ≠ -1)
(hn : n ≠ 0)
:
((Finset.range n).sum fun (i : ℕ) => x ^ i) ≠ 0
theorem
geom_sum_eq_zero_iff_neg_one
{α : Type u}
{n : ℕ}
{x : α}
[LinearOrderedRing α]
(hn : n ≠ 0)
:
Value of a geometric sum over the naturals. Note: see geom_sum_mul_add
for a formulation
that avoids division and subtraction.