Partial sums of geometric series in a field

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.

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 division ring in which x and y commute.

theorem Commute.geom_sum₂ {K : Type u_2} [DivisionRing K] {x y : K} (h' : Commute x y) (h : x ≠ y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

theorem geom_sum_eq {K : Type u_2} [DivisionRing K] {x : K} (h : x ≠ 1) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)

theorem Commute.geom_sum₂_Ico {K : Type u_2} [DivisionRing K] {x y : K} (h : Commute x y) (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

theorem geom_sum_Ico {K : Type u_2} [DivisionRing K] {x : K} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

theorem geom_sum_Ico' {K : Type u_2} [DivisionRing K] {x : K} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)

theorem geom_sum_inv {K : Type u_2} [DivisionRing K] {x : K} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) : ∑ i ∈ Finset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

theorem geom₂_sum {K : Type u_2} [Field K] {x y : K} (h : x ≠ y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

theorem geom_sum₂_Ico {K : Type u_2} [Field K] {x y : K} (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)