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_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^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_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]
@[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 : ℕ), mul_opposite.op x ^ 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 : ℕ), mul_opposite.op y ^ i * mul_opposite.op x ^ (n - 1 - i))
theorem
geom_sum_Ico_le_of_lt_one
{α : Type u}
[linear_ordered_field α]
{x : α}
(hx : 0 ≤ x)
(h'x : x < 1)
{m n : ℕ} :
Geometric sum with ℕ-division #
theorem
geom_sum_pos
{α : Type u}
{n : ℕ}
{x : α}
[strict_ordered_semiring α]
(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 : α}
[strict_ordered_ring α]
(hx : x < 0)
(hx' : 0 < x + 1)
(hn : 1 < n) :
theorem
geom_sum_alternating_of_le_neg_one
{α : Type u}
{x : α}
[strict_ordered_ring α]
(hx : x + 1 ≤ 0)
(n : ℕ) :
theorem
geom_sum_alternating_of_lt_neg_one
{α : Type u}
{n : ℕ}
{x : α}
[strict_ordered_ring α]
(hx : x + 1 < 0)
(hn : 1 < n) :
theorem
geom_sum_pos'
{α : Type u}
{n : ℕ}
{x : α}
[linear_ordered_ring α]
(hx : 0 < x + 1)
(hn : n ≠ 0) :
0 < (finset.range n).sum (λ (i : ℕ), x ^ i)
theorem
odd.geom_sum_pos
{α : Type u}
{n : ℕ}
{x : α}
[linear_ordered_ring α]
(h : odd n) :
0 < (finset.range n).sum (λ (i : ℕ), x ^ i)
theorem
geom_sum_ne_zero
{α : Type u}
{n : ℕ}
{x : α}
[linear_ordered_ring α]
(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 : α}
[linear_ordered_ring α]
(hn : n ≠ 0) :