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.
@[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 : ℕ)
:
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 : ℕ)
:
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 : ℕ)
:
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 : ℕ)
:
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 : ℕ)
:
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 : ℕ)
:
theorem
geom_sum_Ico'
{K : Type u_2}
[DivisionRing K]
{x : K}
(hx : x ≠ 1)
{m n : ℕ}
(hmn : m ≤ n)
:
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 : ℕ}
:
Geometric sum with ℕ
-division #
theorem
geom_sum_pos
{R : Type u_1}
{n : ℕ}
{x : R}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(hx : 0 ≤ x)
(hn : n ≠ 0)
:
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)
:
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 : ℕ)
:
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)
:
theorem
geom_sum_pos'
{R : Type u_1}
{n : ℕ}
{x : R}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
(hx : 0 < x + 1)
(hn : n ≠ 0)
:
theorem
Odd.geom_sum_pos
{R : Type u_1}
{n : ℕ}
{x : R}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
(h : Odd n)
:
theorem
geom_sum_pos_iff
{R : Type u_1}
{n : ℕ}
{x : R}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
(hn : n ≠ 0)
:
theorem
geom_sum_ne_zero
{R : Type u_1}
{n : ℕ}
{x : R}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
(hx : x ≠ -1)
(hn : n ≠ 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)
:
theorem
geom_sum_neg_iff
{R : Type u_1}
{n : ℕ}
{x : R}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
(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.