mathlib documentation

algebra.geom_sum

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 definitions #

geom_sum defines for each $x$ in a semiring and each natural number $n$ the partial sum $\sum_{i=0}^{n-1} x^i$ of the geometric series.
geom_sum₂ defines for each $x,y$ in a semiring and each natural number $n$ the partial sum $\sum_{i=0}^{n-1} x^i y^{n-1-i}$ of the geometric series.

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^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.

def geom_sum {α : Type u} [semiring α] (x : α) (n : ℕ) :

α

Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i$.

Equations

geom_sum x n = ∑ (i : ℕ) in finset.range n, x ^ i

theorem geom_sum_def {α : Type u} [semiring α] (x : α) (n : ℕ) :

geom_sum x n = ∑ (i : ℕ) in finset.range n, x ^ i

theorem geom_sum_succ {α : Type u} [semiring α] {x : α} {n : ℕ} :

geom_sum x (n + 1) = x * geom_sum x n + 1

theorem geom_sum_succ' {α : Type u} [semiring α] {x : α} {n : ℕ} :

geom_sum x (n + 1) = x ^ n + geom_sum x n

@[simp]

theorem geom_sum_zero {α : Type u} [semiring α] (x : α) :

geom_sum x 0 = 0

@[simp]

theorem geom_sum_one {α : Type u} [semiring α] (x : α) :

geom_sum x 1 = 1

@[simp]

theorem geom_sum_two {α : Type u} [semiring α] {x : α} :

geom_sum x 2 = x + 1

@[simp]

theorem zero_geom_sum {α : Type u} [semiring α] {n : ℕ} :

geom_sum 0 n = ite (n = 0) 0 1

@[simp]

theorem one_geom_sum {α : Type u} [semiring α] (n : ℕ) :

geom_sum 1 n = ↑n

@[simp]

theorem op_geom_sum {α : Type u} [semiring α] (x : α) (n : ℕ) :

mul_opposite.op (geom_sum x n) = geom_sum (mul_opposite.op x) n

def geom_sum₂ {α : Type u} [semiring α] (x y : α) (n : ℕ) :

α

Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i y^{n-1-i}$.

Equations

geom_sum₂ x y n = ∑ (i : ℕ) in finset.range n, (x ^ i) * y ^ (n - 1 - i)

theorem geom_sum₂_def {α : Type u} [semiring α] (x y : α) (n : ℕ) :

geom_sum₂ x y n = ∑ (i : ℕ) in finset.range n, (x ^ i) * y ^ (n - 1 - i)

@[simp]

theorem geom_sum₂_zero {α : Type u} [semiring α] (x y : α) :

geom_sum₂ x y 0 = 0

@[simp]

theorem geom_sum₂_one {α : Type u} [semiring α] (x y : α) :

geom_sum₂ x y 1 = 1

@[simp]

theorem op_geom_sum₂ {α : Type u} [semiring α] (x y : α) (n : ℕ) :

mul_opposite.op (geom_sum₂ x y n) = geom_sum₂ (mul_opposite.op y) (mul_opposite.op x) n

@[simp]

theorem geom_sum₂_with_one {α : Type u} [semiring α] (x : α) (n : ℕ) :

geom_sum₂ x 1 n = geom_sum x n

@[protected]

theorem commute.geom_sum₂_mul_add {α : Type u} [semiring α] {x y : α} (h : commute x y) (n : ℕ) :

(geom_sum₂ (x + y) y n) * x + y ^ n = (x + y) ^ n

$x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without - signs.

@[simp]

theorem neg_one_geom_sum {α : Type u} [ring α] {n : ℕ} :

geom_sum (-1) n = ite (even n) 0 1

theorem geom_sum₂_self {α : Type u_1} [comm_ring α] (x : α) (n : ℕ) :

geom_sum₂ x x n = (↑n) * x ^ (n - 1)

theorem geom_sum₂_mul_add {α : Type u} [comm_semiring α] (x y : α) (n : ℕ) :

(geom_sum₂ (x + y) y n) * x + y ^ n = (x + y) ^ n

$x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without - signs.

theorem geom_sum_mul_add {α : Type u} [semiring α] (x : α) (n : ℕ) :

(geom_sum (x + 1) n) * x + 1 = (x + 1) ^ n

@[protected]

theorem commute.geom_sum₂_mul {α : Type u} [ring α] {x y : α} (h : commute x y) (n : ℕ) :

(geom_sum₂ x y n) * (x - y) = x ^ n - y ^ n

theorem commute.mul_neg_geom_sum₂ {α : Type u} [ring α] {x y : α} (h : commute x y) (n : ℕ) :

(y - x) * geom_sum₂ x y n = y ^ n - x ^ n

theorem commute.mul_geom_sum₂ {α : Type u} [ring α] {x y : α} (h : commute x y) (n : ℕ) :

(x - y) * geom_sum₂ x y n = x ^ n - y ^ n

theorem geom_sum₂_mul {α : Type u} [comm_ring α] (x y : α) (n : ℕ) :

(geom_sum₂ x y n) * (x - y) = x ^ n - y ^ n

theorem geom_sum_mul {α : Type u} [ring α] (x : α) (n : ℕ) :

(geom_sum x n) * (x - 1) = x ^ n - 1

theorem mul_geom_sum {α : Type u} [ring α] (x : α) (n : ℕ) :

(x - 1) * geom_sum x n = x ^ n - 1

theorem geom_sum_mul_neg {α : Type u} [ring α] (x : α) (n : ℕ) :

(geom_sum x n) * (1 - x) = 1 - x ^ n

theorem mul_neg_geom_sum {α : Type u} [ring α] (x : α) (n : ℕ) :

(1 - x) * geom_sum x n = 1 - x ^ n

@[protected]

theorem commute.geom_sum₂ {α : Type u} [division_ring α] {x y : α} (h' : commute x y) (h : x ≠ y) (n : ℕ) :

geom_sum₂ x y n = (x ^ n - y ^ n) / (x - y)

theorem geom₂_sum {α : Type u} [field α] {x y : α} (h : x ≠ y) (n : ℕ) :

geom_sum₂ x y n = (x ^ n - y ^ n) / (x - y)

theorem geom_sum_eq {α : Type u} [division_ring α] {x : α} (h : x ≠ 1) (n : ℕ) :

geom_sum x n = (x ^ n - 1) / (x - 1)

@[protected]

theorem commute.mul_geom_sum₂_Ico {α : Type u} [ring α] {x y : α} (h : commute x y) {m n : ℕ} (hmn : m ≤ n) :

(x - y) * ∑ (i : ℕ) in finset.Ico m n, (x ^ i) * y ^ (n - 1 - i) = x ^ n - (x ^ m) * y ^ (n - m)

@[protected]

theorem commute.geom_sum₂_succ_eq {α : Type u} [ring α] {x y : α} (h : commute x y) {n : ℕ} :

geom_sum₂ x y (n + 1) = x ^ n + y * geom_sum₂ x y n

theorem geom_sum₂_succ_eq {α : Type u} [comm_ring α] (x y : α) {n : ℕ} :

geom_sum₂ x y (n + 1) = x ^ n + y * geom_sum₂ x y n

theorem mul_geom_sum₂_Ico {α : Type u} [comm_ring α] (x y : α) {m n : ℕ} (hmn : m ≤ n) :

(x - y) * ∑ (i : ℕ) in finset.Ico m n, (x ^ i) * y ^ (n - 1 - i) = x ^ n - (x ^ m) * y ^ (n - m)

@[protected]

theorem commute.geom_sum₂_Ico_mul {α : Type u} [ring α] {x y : α} (h : commute x y) {m n : ℕ} (hmn : m ≤ n) :

(∑ (i : ℕ) in finset.Ico m n, (x ^ i) * y ^ (n - 1 - i)) * (x - y) = x ^ n - (y ^ (n - m)) * x ^ m

theorem geom_sum_Ico_mul {α : Type u} [ring α] (x : α) {m n : ℕ} (hmn : m ≤ n) :

(∑ (i : ℕ) in finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m

theorem geom_sum_Ico_mul_neg {α : Type u} [ring α] (x : α) {m n : ℕ} (hmn : m ≤ n) :

(∑ (i : ℕ) in finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

@[protected]

theorem commute.geom_sum₂_Ico {α : Type u} [division_ring α] {x y : α} (h : commute x y) (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) :

∑ (i : ℕ) in finset.Ico m n, (x ^ i) * y ^ (n - 1 - i) = (x ^ n - (y ^ (n - m)) * x ^ m) / (x - y)

theorem geom_sum₂_Ico {α : Type u} [field α] {x y : α} (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) :

∑ (i : ℕ) in finset.Ico m n, (x ^ i) * y ^ (n - 1 - i) = (x ^ n - (y ^ (n - m)) * x ^ m) / (x - y)

theorem geom_sum_Ico {α : Type u} [division_ring α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :

∑ (i : ℕ) in finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

theorem geom_sum_Ico' {α : Type u} [division_ring α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :

∑ (i : ℕ) in finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)

theorem geom_sum_inv {α : Type u} [division_ring α] {x : α} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) :

geom_sum x⁻¹ n = (x - 1)⁻¹ * (x - (x⁻¹ ^ n) * x)

theorem ring_hom.map_geom_sum {α : Type u} {β : Type u_1} [semiring α] [semiring β] (x : α) (n : ℕ) (f : α →+* β) :

⇑f (geom_sum x n) = geom_sum (⇑f x) n

theorem ring_hom.map_geom_sum₂ {α : Type u} {β : Type u_1} [semiring α] [semiring β] (x y : α) (n : ℕ) (f : α →+* β) :

⇑f (geom_sum₂ x y n) = geom_sum₂ (⇑f x) (⇑f y) n

Geometric sum with `ℕ`-division #

theorem nat.pred_mul_geom_sum_le (a b n : ℕ) :

(b - 1) * ∑ (i : ℕ) in finset.range n.succ, a / b ^ i ≤ a * b - a / b ^ n

theorem nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :

∑ (i : ℕ) in finset.range n, a / b ^ i ≤ a * b / (b - 1)

theorem nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :

∑ (i : ℕ) in finset.Ico 1 n, a / b ^ i ≤ a / (b - 1)

theorem geom_sum_pos {α : Type u} {n : ℕ} {x : α} [ordered_semiring α] (hx : 0 < x) (hn : n ≠ 0) :

0 < geom_sum x n

theorem geom_sum_pos_and_lt_one {α : Type u} {n : ℕ} {x : α} [ordered_ring α] (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :

0 < geom_sum x n ∧ geom_sum x n < 1

theorem geom_sum_alternating_of_lt_neg_one {α : Type u} {n : ℕ} {x : α} [ordered_ring α] (hx : x + 1 < 0) (hn : 1 < n) :

ite (even n) (geom_sum x n < 0) (1 < geom_sum x n)

theorem geom_sum_pos_of_odd {α : Type u} {n : ℕ} {x : α} [linear_ordered_ring α] (h : odd n) :

0 < geom_sum x n

theorem geom_sum_pos_iff {α : Type u} {n : ℕ} {x : α} [linear_ordered_ring α] (hn : 1 < n) :

0 < geom_sum x n ↔ odd n ∨ 0 < x + 1

theorem geom_sum_eq_zero_iff_neg_one {α : Type u} {n : ℕ} {x : α} [linear_ordered_ring α] (hn : 1 < n) :

geom_sum x n = 0 ↔ x = -1 ∧ even n

theorem geom_sum_neg_iff {α : Type u} {n : ℕ} {x : α} [linear_ordered_ring α] (hn : 1 < n) :

geom_sum x n < 0 ↔ even n ∧ x + 1 < 0