Partial sums of geometric series in an ordered ring #
This file upper- and lower-bounds 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 : ℕ
.
theorem
geom_sum_pos
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hx : 0 ≤ x)
(hn : n ≠ 0)
:
theorem
geom_sum_alternating_of_le_neg_one
{R : Type u_1}
[Ring R]
[PartialOrder R]
[IsOrderedRing R]
{x : R}
(hx : x + 1 ≤ 0)
(n : ℕ)
:
theorem
geom_sum_pos_and_lt_one
{R : Type u_1}
[Ring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hx : x < 0)
(hx' : 0 < x + 1)
(hn : 1 < n)
:
theorem
geom_sum_alternating_of_lt_neg_one
{R : Type u_1}
[Ring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hx : x + 1 < 0)
(hn : 1 < n)
:
theorem
geom_sum_pos'
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hx : 0 < x + 1)
(hn : n ≠ 0)
:
theorem
Odd.geom_sum_pos
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(h : Odd n)
:
theorem
geom_sum_pos_iff
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hn : n ≠ 0)
:
theorem
geom_sum_ne_zero
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hx : x ≠ -1)
(hn : n ≠ 0)
:
theorem
geom_sum_eq_zero_iff_neg_one
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hn : n ≠ 0)
:
theorem
geom_sum_neg_iff
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{n : ℕ}
{x : R}
(hn : n ≠ 0)
: