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_Icoproves that $\sum_{i=m}^{n-1} x^i=\frac{x^n-x^m}{x-1}$ in a division ring.geom_sum₂_Icoproves 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)