Partial sums of geometric series in a ring #
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.
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.
@[simp]
@[simp]
theorem
op_geom_sum₂
{R : Type u_1}
[Semiring R]
(x y : R)
(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₂_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 : ℕ)
:
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 : ℕ)
:
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 : ℕ)
:
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 : ℕ)
:
Value of a geometric sum over the naturals. Note: see geom_sum_mul_add
for a formulation
that avoids division and subtraction.