Partial sums of geometric series in an ordered field

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.

theorem geom₂_sum_of_gt {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x y : K} (h : y < x) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

theorem geom₂_sum_of_lt {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x y : K} (h : x < y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)

theorem geom_sum_of_one_lt {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x : K} (h : 1 < x) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)

theorem geom_sum_of_lt_one {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x : K} (h : x < 1) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x)

theorem geom_sum_lt {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x : K} (h0 : x ≠ 0) (h1 : x < 1) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i < (1 - x)⁻¹

theorem geom_sum_Ico_le_of_lt_one {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {x : K} {m n : ℕ} (hx : 0 ≤ x) (h'x : x < 1) : ∑ i ∈ Finset.Ico m n, x ^ i ≤ x ^ m / (1 - x)