Mathlib.Algebra.GeomSum

geom_sum_succ theorem

{x : R} {n : ℕ} : ∑ i ∈ range (n + 1), x ^ i = (x * ∑ i ∈ range n, x ^ i) + 1

Full source

theorem geom_sum_succ {x : R} {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i = (x * ∑ i ∈ range n, x ^ i) + 1 := by
  simp only [mul_sum, ← pow_succ', sum_range_succ', pow_zero]

Recursive Formula for Geometric Series: $\sum_{i=0}^n x^i = x \cdot \sum_{i=0}^{n-1} x^i + 1$

Informal description

For any element $x$ in a semiring $R$ and any natural number $n$, the sum of the geometric series $\sum_{i=0}^n x^i$ equals $x$ multiplied by the sum $\sum_{i=0}^{n-1} x^i$ plus $1$, i.e., \[ \sum_{i=0}^n x^i = x \left( \sum_{i=0}^{n-1} x^i \right) + 1. \]

geom_sum_succ' theorem

{x : R} {n : ℕ} : ∑ i ∈ range (n + 1), x ^ i = x ^ n + ∑ i ∈ range n, x ^ i

Full source

theorem geom_sum_succ' {x : R} {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i = x ^ n + ∑ i ∈ range n, x ^ i :=
  (sum_range_succ _ _).trans (add_comm _ _)

Recursive Formula for Geometric Series: $\sum_{i=0}^n x^i = x^n + \sum_{i=0}^{n-1} x^i$

Informal description

For any element $x$ in a semiring $R$ and any natural number $n$, the sum of the geometric series $\sum_{i=0}^n x^i$ equals $x^n$ plus the sum $\sum_{i=0}^{n-1} x^i$.

geom_sum_zero theorem

(x : R) : ∑ i ∈ range 0, x ^ i = 0

Full source

theorem geom_sum_zero (x : R) : ∑ i ∈ range 0, x ^ i = 0 :=
  rfl

Empty geometric sum equals zero

Informal description

For any element $x$ in a semiring $R$, the sum $\sum_{i=0}^{-1} x^i$ (an empty sum) equals $0$.

geom_sum_one theorem

(x : R) : ∑ i ∈ range 1, x ^ i = 1

Full source

theorem geom_sum_one (x : R) : ∑ i ∈ range 1, x ^ i = 1 := by simp [geom_sum_succ']

Geometric sum identity: $\sum_{i=0}^0 x^i = 1$

Informal description

For any element $x$ in a semiring $R$, the sum $\sum_{i=0}^0 x^i$ equals $1$.

geom_sum_two theorem

{x : R} : ∑ i ∈ range 2, x ^ i = x + 1

Full source

@[simp]
theorem geom_sum_two {x : R} : ∑ i ∈ range 2, x ^ i = x + 1 := by simp [geom_sum_succ']

Geometric sum identity: $\sum_{i=0}^1 x^i = x + 1$

Informal description

For any element $x$ in a semiring $R$, the sum $\sum_{i=0}^1 x^i$ equals $x + 1$.

zero_geom_sum theorem

: ∀ {n}, ∑ i ∈ range n, (0 : R) ^ i = if n = 0 then 0 else 1

Full source

@[simp]
theorem zero_geom_sum : ∀ {n}, ∑ i ∈ range n, (0 : R) ^ i = if n = 0 then 0 else 1
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by
    rw [geom_sum_succ']
    simp [zero_geom_sum]

Geometric Sum of Zero: $\sum_{i=0}^{n-1} 0^i = \begin{cases} 0 & \text{if } n = 0 \\ 1 & \text{otherwise} \end{cases}$

Informal description

For any natural number $n$ and in any semiring $R$, the sum $\sum_{i=0}^{n-1} 0^i$ equals $0$ if $n = 0$ and $1$ otherwise.

one_geom_sum theorem

(n : ℕ) : ∑ i ∈ range n, (1 : R) ^ i = n

Full source

theorem one_geom_sum (n : ℕ) : ∑ i ∈ range n, (1 : R) ^ i = n := by simp

Geometric Sum of Ones: $\sum_{i=0}^{n-1} 1^i = n$

Informal description

For any natural number $n$ and in any semiring $R$, the sum $\sum_{i=0}^{n-1} 1^i$ equals $n$.

op_geom_sum theorem

(x : R) (n : ℕ) : op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i

Full source

theorem op_geom_sum (x : R) (n : ℕ) : op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i := by
  simp

Geometric Sum Preservation under Multiplicative Opposition: $\text{op}\left(\sum_{i=0}^{n-1} x^i\right) = \sum_{i=0}^{n-1} (\text{op}\,x)^i$

Informal description

For any element $x$ in a semiring $R$ and any natural number $n$, the multiplicative opposite of the geometric sum $\sum_{i=0}^{n-1} x^i$ is equal to the geometric sum $\sum_{i=0}^{n-1} (\text{op}(x))^i$ in the multiplicative opposite semiring $R^\text{op}$.

op_geom_sum₂ theorem

 (x y : R) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)

Full source

@[simp]
theorem op_geom_sum₂ (x y : R) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i =
    ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i) := by
  rw [← sum_range_reflect]
  refine sum_congr rfl fun j j_in => ?_
  rw [mem_range, Nat.lt_iff_add_one_le] at j_in
  congr
  apply tsub_tsub_cancel_of_le
  exact le_tsub_of_add_le_right j_in

Geometric Sum Symmetry in Multiplicative Opposite: $\sum_{i=0}^{n-1} y^{n-1-i}x^i = \sum_{i=0}^{n-1} y^i x^{n-1-i}$ in $R^\text{op}$

Informal description

For any elements $x$ and $y$ in a semiring $R$ and any natural number $n$, the sum $\sum_{i=0}^{n-1} \text{op}(y)^{n-1-i} \cdot \text{op}(x)^i$ equals the sum $\sum_{i=0}^{n-1} \text{op}(y)^i \cdot \text{op}(x)^{n-1-i}$, where $\text{op}$ denotes the multiplicative opposite operation.

geom_sum₂_with_one theorem

(x : R) (n : ℕ) : ∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i

Full source

theorem geom_sum₂_with_one (x : R) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i :=
  sum_congr rfl fun i _ => by rw [one_pow, mul_one]

Simplification of Geometric Sum with Unit Coefficient: $\sum_{i=0}^{n-1} x^i \cdot 1^{n-1-i} = \sum_{i=0}^{n-1} x^i$

Informal description

For any element $x$ in a semiring $R$ and any natural number $n$, the sum $\sum_{i=0}^{n-1} x^i \cdot 1^{n-1-i}$ equals the sum $\sum_{i=0}^{n-1} x^i$.

Commute.geom_sum₂_mul_add theorem

{x y : R} (h : Commute x y) (n : ℕ) : (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Full source

/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
protected theorem Commute.geom_sum₂_mul_add {x y : R} (h : Commute x y) (n : ℕ) :
    (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n := by
  let f :  ℕ → ℕ → R := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)
  change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n
  induction n with
  | zero => rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
  | succ n ih =>
    have f_last : f (n + 1) n = (x + y) ^ n := by
      dsimp only [f]
      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
    have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
    rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]

Geometric Sum Identity for Commuting Elements: $\left(\sum_{i=0}^{n-1} (x + y)^i y^{n-1-i}\right) x + y^n = (x + y)^n$

Informal description

Let $x$ and $y$ be elements in a semiring $R$ that commute (i.e., $xy = yx$). Then for any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} (x + y)^i y^{n-1-i}\right) x + y^n = (x + y)^n. \]

neg_one_geom_sum theorem

[Ring R] {n : ℕ} : ∑ i ∈ range n, (-1 : R) ^ i = if Even n then 0 else 1

Full source

@[simp]
theorem neg_one_geom_sum [Ring R] {n : ℕ} :
    ∑ i ∈ range n, (-1 : R) ^ i = if Even n then 0 else 1 := by
  induction n with
  | zero => simp
  | succ k hk =>
    simp only [geom_sum_succ', Nat.even_add_one, hk]
    split_ifs with h
    · rw [h.neg_one_pow, add_zero]
    · rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

Alternating Geometric Sum Identity: $\sum_{i=0}^{n-1} (-1)^i = \begin{cases} 0 & \text{if } n \text{ is even} \\ 1 & \text{if } n \text{ is odd} \end{cases}$

Informal description

For any ring $R$ and natural number $n$, the sum $\sum_{i=0}^{n-1} (-1)^i$ equals $0$ if $n$ is even and $1$ if $n$ is odd.

geom_sum₂_self theorem

{R : Type*} [Semiring R] (x : R) (n : ℕ) : ∑ i ∈ range n, x ^ i * x ^ (n - 1 - i) = n * x ^ (n - 1)

Full source

theorem geom_sum₂_self {R : Type*} [Semiring R] (x : R) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * x ^ (n - 1 - i) = n * x ^ (n - 1) :=
  calc
    ∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) =
        ∑ i ∈ Finset.range n, x ^ (i + (n - 1 - i)) := by
      simp_rw [← pow_add]
    _ = ∑ _i ∈ Finset.range n, x ^ (n - 1) :=
      Finset.sum_congr rfl fun _ hi =>
        congr_arg _ <| add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| Finset.mem_range.1 hi
    _ = #(range n) • x ^ (n - 1) := sum_const _
    _ = n * x ^ (n - 1) := by rw [Finset.card_range, nsmul_eq_mul]

Geometric Sum Identity: $\sum_{i=0}^{n-1} x^i x^{n-1-i} = n x^{n-1}$

Informal description

For any semiring $R$ and element $x \in R$, the sum $\sum_{i=0}^{n-1} x^i \cdot x^{n-1-i}$ equals $n \cdot x^{n-1}$ for any natural number $n$.

geom_sum₂_mul_add theorem

[CommSemiring R] (x y : R) (n : ℕ) : (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Full source

/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
theorem geom_sum₂_mul_add [CommSemiring R] (x y : R) (n : ℕ) :
    (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n :=
  (Commute.all x y).geom_sum₂_mul_add n

Geometric Sum Identity: $\left(\sum_{i=0}^{n-1} (x + y)^i y^{n-1-i}\right) x + y^n = (x + y)^n$ in a Commutative Semiring

Informal description

Let $R$ be a commutative semiring and let $x, y \in R$. For any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} (x + y)^i y^{n-1-i}\right) x + y^n = (x + y)^n. \]

geom_sum_mul_add theorem

[Semiring R] (x : R) (n : ℕ) : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Full source

theorem geom_sum_mul_add [Semiring R] (x : R) (n : ℕ) :
    (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n := by
  have := (Commute.one_right x).geom_sum₂_mul_add n
  rw [one_pow, geom_sum₂_with_one] at this
  exact this

Geometric Sum Identity: $\left(\sum_{i=0}^{n-1} (x + 1)^i\right) x + 1 = (x + 1)^n$

Informal description

For any element $x$ in a semiring $R$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} (x + 1)^i\right) x + 1 = (x + 1)^n. \]

Commute.geom_sum₂_mul theorem

[Ring R] {x y : R} (h : Commute x y) (n : ℕ) : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Full source

protected theorem Commute.geom_sum₂_mul [Ring R] {x y : R} (h : Commute x y) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n := by
  have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
  rw [sub_add_cancel] at this
  rw [← this, add_sub_cancel_right]

Geometric Sum Identity for Commuting Elements: $\left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right)(x-y) = x^n - y^n$

Informal description

Let $R$ be a ring and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). Then for any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) (x - y) = x^n - y^n. \]

Commute.mul_neg_geom_sum₂ theorem

[Ring R] {x y : R} (h : Commute x y) (n : ℕ) : ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = y ^ n - x ^ n

Full source

theorem Commute.mul_neg_geom_sum₂ [Ring R] {x y : R} (h : Commute x y) (n : ℕ) :
    ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = y ^ n - x ^ n := by
  apply op_injective
  simp only [op_mul, op_sub, op_geom_sum₂, op_pow]
  simp [(Commute.op h.symm).geom_sum₂_mul n]

Geometric Sum Identity for Commuting Elements: $(y - x) \cdot \sum_{i=0}^{n-1} x^i y^{n-1-i} = y^n - x^n$

Informal description

Let $R$ be a ring and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). Then for any natural number $n$, the following identity holds: \[ (y - x) \cdot \left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) = y^n - x^n. \]

Commute.mul_geom_sum₂ theorem

[Ring R] {x y : R} (h : Commute x y) (n : ℕ) : ((x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = x ^ n - y ^ n

Full source

theorem Commute.mul_geom_sum₂ [Ring R] {x y : R} (h : Commute x y) (n : ℕ) :
    ((x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = x ^ n - y ^ n := by
  rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]

Geometric Sum Identity for Commuting Elements: $(x - y) \cdot \sum_{i=0}^{n-1} x^i y^{n-1-i} = x^n - y^n$

Informal description

Let $R$ be a ring and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). Then for any natural number $n$, the following identity holds: \[ (x - y) \cdot \left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) = x^n - y^n. \]

geom_sum₂_mul theorem

[CommRing R] (x y : R) (n : ℕ) : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Full source

theorem geom_sum₂_mul [CommRing R] (x y : R) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n :=
  (Commute.all x y).geom_sum₂_mul n

Geometric Sum Identity in Commutative Ring: $\left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right)(x-y) = x^n - y^n$

Informal description

Let $R$ be a commutative ring and let $x, y \in R$. For any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) (x - y) = x^n - y^n. \]

geom_sum₂_mul_of_ge theorem

 [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R]
  {x y : R} (hxy : y ≤ x) (n : ℕ) : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Full source

theorem geom_sum₂_mul_of_ge [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
    [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : y ≤ x) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n := by
  apply eq_tsub_of_add_eq
  simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n

Geometric Sum Identity: $\left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right)(x - y) = x^n - y^n$ for $y \leq x$ in Ordered Commutative Semiring

Informal description

Let $R$ be a commutative semiring with a partial order, where addition is order-reflecting and monotone on the left, and subtraction is well-behaved with respect to the order. For any elements $x, y \in R$ such that $y \leq x$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) (x - y) = x^n - y^n. \]

geom_sum₂_mul_of_le theorem

 [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R]
  {x y : R} (hxy : x ≤ y) (n : ℕ) : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Full source

theorem geom_sum₂_mul_of_le [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
    [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : x ≤ y) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n := by
  rw [← Finset.sum_range_reflect]
  convert geom_sum₂_mul_of_ge hxy n using 3
  simp_all only [Finset.mem_range]
  rw [mul_comm]
  congr
  omega

Geometric Sum Identity: $\left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right)(y - x) = y^n - x^n$ for $x \leq y$ in Ordered Commutative Semiring

Informal description

Let $R$ be a commutative semiring with a partial order, where addition is order-reflecting and monotone on the left, and subtraction is well-behaved with respect to the order. For any elements $x, y \in R$ such that $x \leq y$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) (y - x) = y^n - x^n. \]

Commute.sub_dvd_pow_sub_pow theorem

[Ring R] {x y : R} (h : Commute x y) (n : ℕ) : x - y ∣ x ^ n - y ^ n

Full source

theorem Commute.sub_dvd_pow_sub_pow [Ring R] {x y : R} (h : Commute x y) (n : ℕ) :
    x - y ∣ x ^ n - y ^ n :=
  Dvd.intro _ <| h.mul_geom_sum₂ _

Divisibility of Power Differences for Commuting Elements: $x - y \mid x^n - y^n$

Informal description

Let $R$ be a ring and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). Then for any natural number $n$, the difference $x - y$ divides $x^n - y^n$.

sub_dvd_pow_sub_pow theorem

[CommRing R] (x y : R) (n : ℕ) : x - y ∣ x ^ n - y ^ n

Full source

theorem sub_dvd_pow_sub_pow [CommRing R] (x y : R) (n : ℕ) : x - y ∣ x ^ n - y ^ n :=
  (Commute.all x y).sub_dvd_pow_sub_pow n

Divisibility of Power Differences in Commutative Rings: $x - y \mid x^n - y^n$

Informal description

Let $R$ be a commutative ring. For any elements $x, y \in R$ and any natural number $n$, the difference $x - y$ divides $x^n - y^n$.

nat_sub_dvd_pow_sub_pow theorem

(x y n : ℕ) : x - y ∣ x ^ n - y ^ n

Full source

theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n := by
  rcases le_or_lt y x with h | h
  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
    exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
    exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

Divisibility of Power Differences for Natural Numbers: $x - y \mid x^n - y^n$

Informal description

For any natural numbers $x, y, n$, the difference $x - y$ divides $x^n - y^n$.

one_sub_dvd_one_sub_pow theorem

[Ring R] (x : R) (n : ℕ) : 1 - x ∣ 1 - x ^ n

Full source

theorem one_sub_dvd_one_sub_pow [Ring R] (x : R) (n : ℕ) :
    1 - x ∣ 1 - x ^ n := by
  conv_rhs => rw [← one_pow n]
  exact (Commute.one_left x).sub_dvd_pow_sub_pow n

Divisibility of $1 - x^n$ by $1 - x$ in a ring

Informal description

Let $R$ be a ring and let $x \in R$. For any natural number $n$, the element $1 - x$ divides $1 - x^n$ in $R$.

sub_one_dvd_pow_sub_one theorem

[Ring R] (x : R) (n : ℕ) : x - 1 ∣ x ^ n - 1

Full source

theorem sub_one_dvd_pow_sub_one [Ring R] (x : R) (n : ℕ) :
    x - 1 ∣ x ^ n - 1 := by
  conv_rhs => rw [← one_pow n]
  exact (Commute.one_right x).sub_dvd_pow_sub_pow n

Divisibility of Power Minus One: $x - 1 \mid x^n - 1$

Informal description

For any element $x$ in a ring $R$ and any natural number $n$, the difference $x - 1$ divides $x^n - 1$.

pow_one_sub_dvd_pow_mul_sub_one theorem

[Ring R] (x : R) (m n : ℕ) : ((x ^ m) - 1 : R) ∣ (x ^ (m * n) - 1)

Full source

lemma pow_one_sub_dvd_pow_mul_sub_one [Ring R] (x : R) (m n : ℕ) :
    ((x ^ m) - 1 : R) ∣ (x ^ (m * n) - 1) := by
  rw [npow_mul]
  exact sub_one_dvd_pow_sub_one (x := x ^ m) (n := n)

Divisibility of Power Product Minus One: $x^m - 1 \mid x^{m \cdot n} - 1$

Informal description

Let $R$ be a ring and $x \in R$. For any natural numbers $m$ and $n$, the element $x^m - 1$ divides $x^{m \cdot n} - 1$ in $R$.

nat_pow_one_sub_dvd_pow_mul_sub_one theorem

(x m n : ℕ) : x ^ m - 1 ∣ x ^ (m * n) - 1

Full source

lemma nat_pow_one_sub_dvd_pow_mul_sub_one (x m n : ℕ) : x ^ m - 1 ∣ x ^ (m * n) - 1 := by
  nth_rw 2 [← Nat.one_pow n]
  rw [Nat.pow_mul x m n]
  apply nat_sub_dvd_pow_sub_pow (x ^ m) 1

Divisibility of Power Product Minus One in Natural Numbers: $x^m - 1 \mid x^{m \cdot n} - 1$

Informal description

For any natural numbers $x$, $m$, and $n$, the difference $x^m - 1$ divides $x^{m \cdot n} - 1$.

Odd.add_dvd_pow_add_pow theorem

[CommRing R] (x y : R) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n

Full source

theorem Odd.add_dvd_pow_add_pow [CommRing R] (x y : R) {n : ℕ} (h : Odd n) :
    x + y ∣ x ^ n + y ^ n := by
  have h₁ := geom_sum₂_mul x (-y) n
  rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁
  exact Dvd.intro_left _ h₁

Divisibility of Sum of Powers by Sum for Odd Exponents: $x + y \mid x^n + y^n$ when $n$ is odd

Informal description

Let $R$ be a commutative ring and let $x, y \in R$. For any odd natural number $n$, the sum $x + y$ divides the sum $x^n + y^n$.

Odd.nat_add_dvd_pow_add_pow theorem

(x y : ℕ) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n

Full source

theorem Odd.nat_add_dvd_pow_add_pow (x y : ℕ) {n : ℕ} (h : Odd n) : x + y ∣ x ^ n + y ^ n :=
  mod_cast Odd.add_dvd_pow_add_pow (x : ℤ) (↑y) h

Divisibility of Sum of Powers by Sum for Odd Exponents in Natural Numbers: $x + y \mid x^n + y^n$ when $n$ is odd

Informal description

For any natural numbers $x$ and $y$, and any odd natural number $n$, the sum $x + y$ divides the sum $x^n + y^n$.

geom_sum_mul theorem

[Ring R] (x : R) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Full source

theorem geom_sum_mul [Ring R] (x : R) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1 := by
  have := (Commute.one_right x).geom_sum₂_mul n
  rw [one_pow, geom_sum₂_with_one] at this
  exact this

Geometric Sum Identity: $(\sum_{i=0}^{n-1} x^i)(x-1) = x^n - 1$

Informal description

For any element $x$ in a ring $R$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i\right) (x - 1) = x^n - 1. \]

geom_sum_mul_of_one_le theorem

 [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R}
  (hx : 1 ≤ x) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Full source

theorem geom_sum_mul_of_one_le [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R]
    [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : 1 ≤ x) (n : ℕ) :
    (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1 := by
  simpa using geom_sum₂_mul_of_ge hx n

Geometric Sum Identity: $(\sum_{i=0}^{n-1} x^i)(x-1) = x^n - 1$ for $1 \leq x$ in Ordered Commutative Semiring

Informal description

Let $R$ be a commutative semiring with a partial order, where addition is order-reflecting and monotone on the left, and subtraction is well-behaved with respect to the order. For any element $x \in R$ such that $1 \leq x$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i\right) (x - 1) = x^n - 1. \]

geom_sum_mul_of_le_one theorem

 [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R}
  (hx : x ≤ 1) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Full source

theorem geom_sum_mul_of_le_one [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R]
    [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : x ≤ 1) (n : ℕ) :
    (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n := by
  simpa using geom_sum₂_mul_of_le hx n

Geometric Sum Identity: $(\sum_{i=0}^{n-1} x^i)(1 - x) = 1 - x^n$ for $x \leq 1$ in Ordered Commutative Semiring

Informal description

Let $R$ be a commutative semiring with a partial order, where addition is order-reflecting and monotone on the left, and subtraction is well-behaved with respect to the order. For any element $x \in R$ such that $x \leq 1$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i\right) (1 - x) = 1 - x^n. \]

mul_geom_sum theorem

[Ring R] (x : R) (n : ℕ) : ((x - 1) * ∑ i ∈ range n, x ^ i) = x ^ n - 1

Full source

theorem mul_geom_sum [Ring R] (x : R) (n : ℕ) : ((x - 1) * ∑ i ∈ range n, x ^ i) = x ^ n - 1 :=
  op_injective <| by simpa using geom_sum_mul (op x) n

Geometric Sum Identity: $(x-1)\sum_{i=0}^{n-1} x^i = x^n - 1$ in a Ring

Informal description

For any element $x$ in a ring $R$ and any natural number $n$, the following identity holds: \[ (x - 1) \left(\sum_{i=0}^{n-1} x^i\right) = x^n - 1. \]

geom_sum_mul_neg theorem

[Ring R] (x : R) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Full source

theorem geom_sum_mul_neg [Ring R] (x : R) (n : ℕ) :
    (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n := by
  have := congr_arg Neg.neg (geom_sum_mul x n)
  rw [neg_sub, ← mul_neg, neg_sub] at this
  exact this

Geometric Sum Identity: $(\sum_{i=0}^{n-1} x^i)(1 - x) = 1 - x^n$

Informal description

For any element $x$ in a ring $R$ and any natural number $n$, the following identity holds: \[ \left(\sum_{i=0}^{n-1} x^i\right) (1 - x) = 1 - x^n. \]

mul_neg_geom_sum theorem

[Ring R] (x : R) (n : ℕ) : ((1 - x) * ∑ i ∈ range n, x ^ i) = 1 - x ^ n

Full source

theorem mul_neg_geom_sum [Ring R] (x : R) (n : ℕ) : ((1 - x) * ∑ i ∈ range n, x ^ i) = 1 - x ^ n :=
  op_injective <| by simpa using geom_sum_mul_neg (op x) n

Geometric Sum Identity: $(1 - x) \sum_{i=0}^{n-1} x^i = 1 - x^n$

Informal description

For any element $x$ in a ring $R$ and any natural number $n$, the following identity holds: \[ (1 - x) \left( \sum_{i=0}^{n-1} x^i \right) = 1 - x^n. \]

Commute.geom_sum₂_comm theorem

 [Semiring R] {x y : R} (n : ℕ) (h : Commute x y) :
  ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i)

Full source

protected theorem Commute.geom_sum₂_comm [Semiring R] {x y : R} (n : ℕ)
    (h : Commute x y) :
    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i) := by
  cases n; · simp
  simp only [Nat.succ_eq_add_one, Nat.add_sub_cancel]
  rw [← Finset.sum_flip]
  refine Finset.sum_congr rfl fun i hi => ?_
  simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _

Commutativity of Geometric Sum with Commuting Elements: $\sum_{i=0}^{n-1} x^i y^{n-1-i} = \sum_{i=0}^{n-1} y^i x^{n-1-i}$

Informal description

Let $R$ be a semiring, and let $x, y \in R$ be two commuting elements (i.e., $x * y = y * x$). For any natural number $n$, the sum $\sum_{i=0}^{n-1} x^i y^{n-1-i}$ is equal to the sum $\sum_{i=0}^{n-1} y^i x^{n-1-i}$.

geom_sum₂_comm theorem

 [CommSemiring R] (x y : R) (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i)

Full source

theorem geom_sum₂_comm [CommSemiring R] (x y : R) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i) :=
  (Commute.all x y).geom_sum₂_comm n

Commutativity of Geometric Sum in Commutative Semiring: $\sum_{i=0}^{n-1} x^i y^{n-1-i} = \sum_{i=0}^{n-1} y^i x^{n-1-i}$

Informal description

Let $R$ be a commutative semiring, and let $x, y \in R$. For any natural number $n$, the sum $\sum_{i=0}^{n-1} x^i y^{n-1-i}$ is equal to the sum $\sum_{i=0}^{n-1} y^i x^{n-1-i}$.

Commute.geom_sum₂ theorem

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

Full source

protected theorem Commute.geom_sum₂ [DivisionRing K] {x y : K} (h' : Commute x y) (h : x ≠ y)
    (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) := by
  have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]

Geometric Sum Identity for Commuting Elements in Division Ring: $\sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^n}{x - y}$

Informal description

Let $K$ be a division ring, and let $x, y \in K$ be commuting elements (i.e., $xy = yx$) with $x \neq y$. Then for any natural number $n$, the following identity holds: \[ \sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^n}{x - y}. \]

geom₂_sum theorem

[Field K] {x y : K} (h : x ≠ y) (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Full source

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

Geometric Sum Identity in Field: $\sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^n}{x - y}$

Informal description

Let $K$ be a field, and let $x, y \in K$ with $x \neq y$. Then for any natural number $n$, the following identity holds: \[ \sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^n}{x - y}. \]

geom₂_sum_of_gt theorem

 [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x y : K}
  (h : y < x) (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Full source

theorem geom₂_sum_of_gt [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
    [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K]
    {x y : K} (h : y < x) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) :=
  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_ge h.le n)

Geometric Sum Identity for $y < x$ in Ordered Semifield: $\sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^n}{x - y}$

Informal description

Let $K$ be a semifield with a linear order and strict ordered ring structure, where addition is canonically ordered and subtraction is well-behaved with respect to the order. For any elements $x, y \in K$ such that $y < x$ and any natural number $n$, the following identity holds: \[ \sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^n}{x - y}. \]

geom₂_sum_of_lt theorem

 [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K] {x y : K}
  (h : x < y) (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)

Full source

theorem geom₂_sum_of_lt [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
    [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K]
    {x y : K} (h : x < y) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x) :=
  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_le h.le n)

Geometric Sum Identity for $x < y$ in Ordered Semifield: $\sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{y^n - x^n}{y - x}$

Informal description

Let $K$ be a linearly ordered semifield with a strict ordered ring structure, where addition is canonically ordered and subtraction is well-behaved with respect to the order. For any elements $x, y \in K$ such that $x < y$ and any natural number $n$, the following identity holds: \[ \sum_{i=0}^{n-1} x^i y^{n-1-i} = \frac{y^n - x^n}{y - x}. \]

geom_sum_eq theorem

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

Full source

theorem geom_sum_eq [DivisionRing K] {x : K} (h : x ≠ 1) (n : ℕ) :
    ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1) := by
  have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]

Geometric Series Sum Formula: $\sum_{i=0}^{n-1} x^i = \frac{x^n - 1}{x - 1}$ for $x \neq 1$

Informal description

For any element $x \neq 1$ in a division ring $K$ and any natural number $n$, the sum of the geometric series $\sum_{i=0}^{n-1} x^i$ equals $\frac{x^n - 1}{x - 1}$.

geom_sum_of_one_lt theorem

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

Full source

lemma geom_sum_of_one_lt {x : K} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
    [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K]
    (h : 1 < x) (n : ℕ) :
    ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1) :=
  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_one_le h.le n)

Geometric Series Sum Formula for $1 < x$ in Ordered Semifield

Informal description

Let $K$ be a semifield with a linear order and a strict ordered ring structure, where addition is canonically ordered and subtraction is well-behaved with respect to the order. For any element $x \in K$ such that $1 < x$ and any natural number $n$, the sum of the geometric series satisfies: \[ \sum_{i=0}^{n-1} x^i = \frac{x^n - 1}{x - 1}. \]

geom_sum_of_lt_one theorem

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

Full source

lemma geom_sum_of_lt_one {x : K} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
    [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K]
    (h : x < 1) (n : ℕ) :
    ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x) :=
  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_le_one h.le n)

Geometric Series Sum Formula for $x < 1$ in Ordered Semifield

Informal description

Let $K$ be a linearly ordered semifield with a strict ordered ring structure, where addition is canonically ordered and subtraction is well-behaved with respect to the order. For any element $x \in K$ such that $x < 1$ and any natural number $n$, the sum of the geometric series satisfies: \[ \sum_{i=0}^{n-1} x^i = \frac{1 - x^n}{1 - x}. \]

geom_sum_lt theorem

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

Full source

theorem geom_sum_lt {x : K} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
    [CanonicallyOrderedAdd K] [Sub K] [OrderedSub K]
    (h0 : x ≠ 0) (h1 : x < 1) (n : ℕ) : ∑ i ∈ range n, x ^ i < (1 - x)⁻¹ := by
  rw [← pos_iff_ne_zero] at h0
  rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]
  · exact ⟨h0.trans h1, pow_pos h0 n⟩
  · rwa [ne_eq, tsub_eq_zero_iff_le, not_le]
  · rwa [tsub_pos_iff_lt]

Upper Bound for Geometric Series Sum when $0 < x < 1$

Informal description

Let $K$ be a linearly ordered semifield with a strict ordered ring structure, where addition is canonically ordered and subtraction is well-behaved with respect to the order. For any nonzero element $x \in K$ such that $x < 1$ and any natural number $n$, the sum of the geometric series satisfies: \[ \sum_{i=0}^{n-1} x^i < \frac{1}{1 - x}. \]

Commute.mul_geom_sum₂_Ico theorem

 [Ring R] {x y : R} (h : Commute x y) {m n : ℕ} (hmn : m ≤ n) :
  ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m)

Full source

protected theorem Commute.mul_geom_sum₂_Ico [Ring R] {x y : R} (h : Commute x y) {m n : ℕ}
    (hmn : m ≤ n) :
    ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m) := by
  rw [sum_Ico_eq_sub _ hmn]
  have :
    ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) =
      ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) := by
    refine sum_congr rfl fun j j_in => ?_
    rw [← pow_add]
    congr
    rw [mem_range] at j_in
    omega
  rw [this]
  simp_rw [pow_mul_comm y (n - m) _]
  simp_rw [← mul_assoc]
  rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)]

Geometric Sum Identity for Commuting Elements over Interval: $(x - y) \cdot \sum_{i=m}^{n-1} x^i y^{n-1-i} = x^n - x^m y^{n-m}$

Informal description

Let $R$ be a ring, and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). For any natural numbers $m \leq n$, the following identity holds: \[ (x - y) \cdot \left(\sum_{i=m}^{n-1} x^i y^{n-1-i}\right) = x^n - x^m y^{n-m}. \]

Commute.geom_sum₂_succ_eq theorem

 [Ring R] {x y : R} (h : Commute x y) {n : ℕ} :
  ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Full source

protected theorem Commute.geom_sum₂_succ_eq [Ring R] {x y : R} (h : Commute x y) {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) =
      x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) := by
  simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
    (h.symm.pow_right _).eq, mul_assoc, ← pow_succ']
  refine sum_congr rfl fun i hi => ?_
  suffices n - 1 - i + 1 = n - i by rw [this]
  rw [Finset.mem_range] at hi
  omega

Recursive Formula for Sum of Commuting Elements' Powers: $\sum_{i=0}^n x^i y^{n-i} = x^n + y \sum_{i=0}^{n-1} x^i y^{n-1-i}$

Informal description

Let $R$ be a ring, and let $x, y \in R$ be commuting elements (i.e., $xy = yx$). Then for any natural number $n$, the sum $\sum_{i=0}^n x^i y^{n-i}$ can be expressed as: \[ \sum_{i=0}^n x^i y^{n-i} = x^n + y \sum_{i=0}^{n-1} x^i y^{n-1-i}. \]

geom_sum₂_succ_eq theorem

 [CommRing R] (x y : R) {n : ℕ} :
  ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Full source

theorem geom_sum₂_succ_eq [CommRing R] (x y : R) {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) =
      x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) :=
  (Commute.all x y).geom_sum₂_succ_eq

Recursive Formula for Sum of Powers: $\sum_{i=0}^n x^i y^{n-i} = x^n + y \sum_{i=0}^{n-1} x^i y^{n-1-i}$

Informal description

Let $R$ be a commutative ring and $x, y \in R$. For any natural number $n$, the sum $\sum_{i=0}^n x^i y^{n-i}$ can be expressed as: \[ \sum_{i=0}^n x^i y^{n-i} = x^n + y \sum_{i=0}^{n-1} x^i y^{n-1-i}. \]

mul_geom_sum₂_Ico theorem

 [CommRing R] (x y : R) {m n : ℕ} (hmn : m ≤ n) :
  ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m)

Full source

theorem mul_geom_sum₂_Ico [CommRing R] (x y : R) {m n : ℕ} (hmn : m ≤ n) :
    ((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m) :=
  (Commute.all x y).mul_geom_sum₂_Ico hmn

Geometric Sum Identity: $(x - y) \cdot \sum_{i=m}^{n-1} x^i y^{n-1-i} = x^n - x^m y^{n-m}$ in a Commutative Ring

Informal description

Let $R$ be a commutative ring and $x, y \in R$. For any natural numbers $m \leq n$, the following identity holds: \[ (x - y) \cdot \left(\sum_{i=m}^{n-1} x^i y^{n-1-i}\right) = x^n - x^m y^{n-m}. \]

Commute.geom_sum₂_Ico_mul theorem

 [Ring R] {x y : R} (h : Commute x y) {m n : ℕ} (hmn : m ≤ n) :
  (∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m

Full source

protected theorem Commute.geom_sum₂_Ico_mul [Ring R] {x y : R} (h : Commute x y) {m n : ℕ}
    (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m := by
  apply op_injective
  simp only [op_sub, op_mul, op_pow, op_sum]
  have : (∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
      ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
    refine sum_congr rfl fun k _ => ?_
    have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
    simpa [Commute, SemiconjBy] using hp
  simp only [this]
  convert (Commute.op h).mul_geom_sum₂_Ico hmn

Geometric Sum Identity for Commuting Elements: $\left(\sum_{i=m}^{n-1} x^i y^{n-1-i}\right)(x-y) = x^n - y^{n-m}x^m$

Informal description

Let $R$ be a ring and $x, y \in R$ be commuting elements (i.e., $xy = yx$). For any natural numbers $m \leq n$, the following identity holds: \[ \left(\sum_{i=m}^{n-1} x^i y^{n-1-i}\right) (x - y) = x^n - y^{n-m} x^m. \]

geom_sum_Ico_mul theorem

[Ring R] (x : R) {m n : ℕ} (hmn : m ≤ n) : (∑ i ∈ Finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m

Full source

theorem geom_sum_Ico_mul [Ring R] (x : R) {m n : ℕ} (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m := by
  rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]

Geometric Sum Identity over Interval: $(\sum_{i=m}^{n-1} x^i)(x-1) = x^n - x^m$

Informal description

Let $R$ be a ring and $x \in R$. For any natural numbers $m \leq n$, the following identity holds: \[ \left(\sum_{i=m}^{n-1} x^i\right) (x - 1) = x^n - x^m. \]

geom_sum_Ico_mul_neg theorem

[Ring R] (x : R) {m n : ℕ} (hmn : m ≤ n) : (∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

Full source

theorem geom_sum_Ico_mul_neg [Ring R] (x : R) {m n : ℕ} (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n := by
  rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]

Geometric Sum Identity over Interval: $(\sum_{i=m}^{n-1} x^i)(1 - x) = x^m - x^n$

Informal description

Let $R$ be a ring and $x \in R$. For any natural numbers $m \leq n$, the following identity holds: \[ \left(\sum_{i=m}^{n-1} x^i\right) (1 - x) = x^m - x^n. \]

Commute.geom_sum₂_Ico theorem

 [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)

Full source

protected theorem Commute.geom_sum₂_Ico [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) := by
  have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]

Geometric Sum Identity for Commuting Elements: $\sum_{i=m}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^{n-m}x^m}{x - y}$

Informal description

Let $K$ be a division ring and $x, y \in K$ be commuting elements (i.e., $xy = yx$) with $x \neq y$. For any natural numbers $m \leq n$, the sum of the geometric series satisfies: \[ \sum_{i=m}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^{n-m} x^m}{x - y}. \]

geom_sum₂_Ico theorem

 [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)

Full source

theorem geom_sum₂_Ico [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) :=
  (Commute.all x y).geom_sum₂_Ico hxy hmn

Geometric Sum Identity: $\sum_{i=m}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^{n-m}x^m}{x - y}$ for $x \neq y$ in a Field

Informal description

Let $K$ be a field and $x, y \in K$ with $x \neq y$. For any natural numbers $m \leq n$, the sum of the geometric series satisfies: \[ \sum_{i=m}^{n-1} x^i y^{n-1-i} = \frac{x^n - y^{n-m} x^m}{x - y}. \]

geom_sum_Ico theorem

 [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)

Full source

theorem geom_sum_Ico [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) := by
  simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]

Geometric Series Sum over Interval: $\sum_{i=m}^{n-1} x^i = \frac{x^n - x^m}{x - 1}$ for $x \neq 1$

Informal description

For any element $x \neq 1$ in a division ring $K$ and natural numbers $m \leq n$, the sum of the geometric series $\sum_{i=m}^{n-1} x^i$ equals $\frac{x^n - x^m}{x - 1}$.

geom_sum_Ico' theorem

 [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)

Full source

theorem geom_sum_Ico' [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) := by
  simp only [geom_sum_Ico hx hmn]
  convert neg_div_neg_eq (x ^ m - x ^ n) (1 - x) using 2 <;> abel

Geometric Series Sum over Interval: $\sum_{i=m}^{n-1} x^i = \frac{x^m - x^n}{1 - x}$ for $x \neq 1$

Informal description

For any element $x \neq 1$ in a division ring $K$ and natural numbers $m \leq n$, the sum of the geometric series $\sum_{i=m}^{n-1} x^i$ equals $\frac{x^m - x^n}{1 - x}$.

geom_sum_Ico_le_of_lt_one theorem

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

Full source

theorem geom_sum_Ico_le_of_lt_one [Field K] [LinearOrder K] [IsStrictOrderedRing K]
    {x : K} (hx : 0 ≤ x) (h'x : x < 1)
    {m n : ℕ} : ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x) := by
  rcases le_or_lt m n with (hmn | hmn)
  · rw [geom_sum_Ico' h'x.ne hmn]
    apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
    simpa using pow_nonneg hx _
  · rw [Ico_eq_empty, sum_empty]
    · apply div_nonneg (pow_nonneg hx _)
      simpa using h'x.le
    · simpa using hmn.le

Upper Bound for Geometric Series Sum: $\sum_{i=m}^{n-1} x^i \leq \frac{x^m}{1-x}$ when $0 \leq x < 1$

Informal description

Let $K$ be a linearly ordered field that is a strict ordered ring. For any $x \in K$ satisfying $0 \leq x < 1$ and any natural numbers $m \leq n$, the sum of the geometric series $\sum_{i=m}^{n-1} x^i$ is bounded above by $\frac{x^m}{1 - x}$.

geom_sum_inv theorem

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

Full source

theorem geom_sum_inv [DivisionRing K] {x : K} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) :
    ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x) := by
  have h₁ : x⁻¹x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
  have h₂ : x⁻¹x⁻¹ - 1 ≠ 0 := mt sub_eq_zero.1 h₁
  have h₃ : x - 1 ≠ 0 := mt sub_eq_zero.1 hx1
  have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
    Nat.recOn n (by simp) fun n h => by
      rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
  rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc,
    mul_inv_cancel₀ h₃]
  simp [mul_add, add_mul, mul_inv_cancel₀ hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm,
    add_left_comm]
  rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]

Geometric Sum of Inverses: $\sum_{i=0}^{n-1} x^{-i} = \frac{x - x^{-n+1}}{x - 1}$ for $x \neq 0, 1$

Informal description

For any nonzero element $x \neq 1$ in a division ring $K$ and any natural number $n$, the sum of the geometric series $\sum_{i=0}^{n-1} (x^{-1})^i$ equals $(x - 1)^{-1} \cdot (x - x^{-n} \cdot x)$.

RingHom.map_geom_sum theorem

[Semiring R] [Semiring S] (x : R) (n : ℕ) (f : R →+* S) : f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i

Full source

theorem RingHom.map_geom_sum [Semiring R] [Semiring S] (x : R) (n : ℕ) (f : R →+* S) :
    f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i := by simp [map_sum f]

Ring Homomorphism Preserves Geometric Sum

Informal description

Let $R$ and $S$ be semirings, and let $f: R \to S$ be a ring homomorphism. For any element $x \in R$ and any natural number $n$, the image under $f$ of the geometric sum $\sum_{i=0}^{n-1} x^i$ equals the geometric sum $\sum_{i=0}^{n-1} (f(x))^i$ in $S$.

RingHom.map_geom_sum₂ theorem

 [Semiring R] [Semiring S] (x y : R) (n : ℕ) (f : R →+* S) :
  f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i)

Full source

theorem RingHom.map_geom_sum₂ [Semiring R] [Semiring S] (x y : R) (n : ℕ) (f : R →+* S) :
    f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i) := by
  simp [map_sum f]

Ring Homomorphism Preserves Geometric Sum of Products: $f\left(\sum_{i=0}^{n-1} x^i y^{n-1-i}\right) = \sum_{i=0}^{n-1} (f x)^i (f y)^{n-1-i}$

Informal description

Let $R$ and $S$ be semirings, and let $f \colon R \to S$ be a ring homomorphism. For any elements $x, y \in R$ and any natural number $n$, the image under $f$ of the sum $\sum_{i=0}^{n-1} x^i y^{n-1-i}$ is equal to the sum $\sum_{i=0}^{n-1} (f x)^i (f y)^{n-1-i}$.

Nat.pred_mul_geom_sum_le theorem

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

Full source

theorem Nat.pred_mul_geom_sum_le (a b n : ℕ) :
    ((b - 1) * ∑ i ∈ range n.succ, a / b ^ i) ≤ a * b - a / b ^ n :=
  calc
    ((b - 1) * ∑ i ∈ range n.succ, a / b ^ i) =
    (∑ i ∈ range n, a / b ^ (i + 1) * b) + a * b - ((∑ i ∈ range n, a / b ^ i) + a / b ^ n) := by
      rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
    _ ≤ (∑ i ∈ range n, a / b ^ i) + a * b - ((∑ i ∈ range n, a / b ^ i) + a / b ^ n) := by
      gcongr with i hi
      rw [pow_succ, ← Nat.div_div_eq_div_mul]
      exact Nat.div_mul_le_self _ _
    _ = a * b - a / b ^ n := add_tsub_add_eq_tsub_left _ _ _

Inequality for Predessor Multiplied by Geometric Sum of Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $n$, the following inequality holds: $$(b - 1) \cdot \sum_{i=0}^{n} \frac{a}{b^i} \leq a \cdot b - \frac{a}{b^n}.$$

Nat.geom_sum_le theorem

{b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)

Full source

theorem Nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
    ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1) := by
  refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_
  rcases n with - | n
  · rw [sum_range_zero, zero_mul]
    exact Nat.zero_le _
  rw [mul_comm]
  exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

Upper Bound for Geometric Sum with Natural Division: $\sum_{i=0}^{n-1} \frac{a}{b^i} \leq \frac{a b}{b - 1}$

Informal description

For any natural numbers $a$, $b$, and $n$ with $b \geq 2$, the sum of the geometric series $\sum_{i=0}^{n-1} \frac{a}{b^i}$ is bounded above by $\frac{a \cdot b}{b - 1}$.

Nat.geom_sum_Ico_le theorem

{b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)

Full source

theorem Nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
    ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1) := by
  rcases n with - | n
  · rw [Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]
    exact Nat.zero_le _
  rw [← add_le_add_iff_left a]
  calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
      exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by
      rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

Upper Bound for Geometric Sum over Interval: $\sum_{i=1}^{n-1} \frac{a}{b^i} \leq \frac{a}{b - 1}$ when $b \geq 2$

Informal description

For any natural numbers $a$, $b$, and $n$ with $b \geq 2$, the sum of the geometric series $\sum_{i=1}^{n-1} \frac{a}{b^i}$ is bounded above by $\frac{a}{b - 1}$.

geom_sum_pos theorem

[Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (hx : 0 ≤ x) (hn : n ≠ 0) : 0 < ∑ i ∈ range n, x ^ i

Full source

theorem geom_sum_pos [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
    (hx : 0 ≤ x) (hn : n ≠ 0) :
    0 < ∑ i ∈ range n, x ^ i :=
  sum_pos' (fun _ _ => pow_nonneg hx _) ⟨0, mem_range.2 hn.bot_lt, by simp⟩

Positivity of Geometric Sum for Nonnegative Elements in Strict Ordered Semirings

Informal description

Let $R$ be a strict ordered semiring. For any nonnegative element $x \in R$ (i.e., $0 \leq x$) and any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ is strictly positive, i.e., $0 < \sum_{i=0}^{n-1} x^i$.

geom_sum_pos_and_lt_one theorem

 [Ring R] [PartialOrder R] [IsStrictOrderedRing R] (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
  (0 < ∑ i ∈ range n, x ^ i) ∧ ∑ i ∈ range n, x ^ i < 1

Full source

theorem geom_sum_pos_and_lt_one [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
    (0 < ∑ i ∈ range n, x ^ i) ∧ ∑ i ∈ range n, x ^ i < 1 := by
  refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
  · rw [geom_sum_two]
    exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
  clear hn
  intro n _ ihn
  rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
  exact
    ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
      mul_neg_of_neg_of_pos hx ihn.1⟩

Bounds on Geometric Sum for Negative $x$ Near $-1$: $0 < \sum_{i=0}^{n-1} x^i < 1$ when $x < 0$ and $x > -1$

Informal description

Let $R$ be a strict ordered ring, and let $x \in R$ satisfy $x < 0$ and $0 < x + 1$. For any natural number $n > 1$, the geometric sum $\sum_{i=0}^{n-1} x^i$ satisfies $0 < \sum_{i=0}^{n-1} x^i < 1$.

geom_sum_alternating_of_le_neg_one theorem

 [Ring R] [PartialOrder R] [IsOrderedRing R] (hx : x + 1 ≤ 0) (n : ℕ) :
  if Even n then (∑ i ∈ range n, x ^ i) ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i

Full source

theorem geom_sum_alternating_of_le_neg_one [Ring R] [PartialOrder R] [IsOrderedRing R]
    (hx : x + 1 ≤ 0) (n : ℕ) :
    if Even n then (∑ i ∈ range n, x ^ i) ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i := by
  have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
  induction n with
  | zero => simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]
  | succ n ih =>
    simp only [Nat.even_add_one, geom_sum_succ]
    split_ifs at ih with h
    · rw [if_neg (not_not_intro h), le_add_iff_nonneg_left]
      exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
    · rw [if_pos h]
      refine (add_le_add_right ?_ _).trans hx
      simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

Alternating Behavior of Geometric Sum for $x \leq -1$ in Ordered Rings

Informal description

Let $R$ be an ordered ring and let $x \in R$ satisfy $x + 1 \leq 0$. For any natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ satisfies: - If $n$ is even, then $\sum_{i=0}^{n-1} x^i \leq 0$. - If $n$ is odd, then $1 \leq \sum_{i=0}^{n-1} x^i$.

geom_sum_alternating_of_lt_neg_one theorem

 [Ring R] [PartialOrder R] [IsStrictOrderedRing R] (hx : x + 1 < 0) (hn : 1 < n) :
  if Even n then (∑ i ∈ range n, x ^ i) < 0 else 1 < ∑ i ∈ range n, x ^ i

Full source

theorem geom_sum_alternating_of_lt_neg_one [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    (hx : x + 1 < 0) (hn : 1 < n) :
    if Even n then (∑ i ∈ range n, x ^ i) < 0 else 1 < ∑ i ∈ range n, x ^ i := by
  have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx
  refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
  · simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, gt_iff_lt, hx, even_two]
  clear hn
  intro n _ ihn
  simp only [Nat.even_add_one, geom_sum_succ]
  by_cases hn' : Even n
  · rw [if_pos hn'] at ihn
    rw [if_neg, lt_add_iff_pos_left]
    · exact mul_pos_of_neg_of_neg hx0 ihn
    · exact not_not_intro hn'
  · rw [if_neg hn'] at ihn
    rw [if_pos]
    swap
    · exact hn'
    have := add_lt_add_right (mul_lt_mul_of_neg_left ihn hx0) 1
    rw [mul_one] at this
    exact this.trans hx

Alternating Behavior of Geometric Sum for $x < -1$ in Strict Ordered Rings

Informal description

Let $R$ be a strict ordered ring, $x \in R$ such that $x + 1 < 0$, and $n \in \mathbb{N}$ with $1 < n$. Then the geometric sum $\sum_{i=0}^{n-1} x^i$ satisfies: - If $n$ is even, then $\sum_{i=0}^{n-1} x^i < 0$. - If $n$ is odd, then $1 < \sum_{i=0}^{n-1} x^i$.

geom_sum_pos' theorem

[Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hx : 0 < x + 1) (hn : n ≠ 0) : 0 < ∑ i ∈ range n, x ^ i

Full source

theorem geom_sum_pos' [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
    (hx : 0 < x + 1) (hn : n ≠ 0) :
    0 < ∑ i ∈ range n, x ^ i := by
  obtain _ | _ | n := n
  · cases hn rfl
  · simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]
  obtain hx' | hx' := lt_or_le x 0
  · exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1
  · exact geom_sum_pos hx' (by simp only [Nat.succ_ne_zero, Ne, not_false_iff])

Positivity of Geometric Sum for $x > -1$ in Strict Ordered Rings

Informal description

Let $R$ be a strict ordered ring with a linear order. For any element $x \in R$ such that $x + 1 > 0$ and any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ is strictly positive, i.e., $0 < \sum_{i=0}^{n-1} x^i$.

Odd.geom_sum_pos theorem

[Ring R] [LinearOrder R] [IsStrictOrderedRing R] (h : Odd n) : 0 < ∑ i ∈ range n, x ^ i

Full source

theorem Odd.geom_sum_pos [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
    (h : Odd n) : 0 < ∑ i ∈ range n, x ^ i := by
  rcases n with (_ | _ | k)
  · exact (Nat.not_odd_zero h).elim
  · simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]
  rw [← Nat.not_even_iff_odd] at h
  rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
  · have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
    simp only [h, if_false] at this
    exact zero_lt_one.trans this
  · simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]
  · exact geom_sum_pos' hx k.succ.succ_ne_zero

Positivity of Geometric Sum for Odd $n$ in Strict Ordered Rings

Informal description

Let $R$ be a strict ordered ring with a linear order. For any element $x \in R$ and any odd natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ is strictly positive, i.e., $0 < \sum_{i=0}^{n-1} x^i$.

geom_sum_pos_iff theorem

 [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n ≠ 0) : (0 < ∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1

Full source

theorem geom_sum_pos_iff [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n ≠ 0) :
    (0 < ∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1 := by
  refine ⟨fun h => ?_, ?_⟩
  · rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
    refine fun hn hx => h.not_le ?_
    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
  · rintro (hn | hx')
    · exact hn.geom_sum_pos
    · exact geom_sum_pos' hx' hn

Positivity Criterion for Geometric Sum in Strict Ordered Rings

Informal description

Let $R$ be a strict ordered ring with a linear order. For any element $x \in R$ and any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ is strictly positive if and only if either $n$ is odd or $x + 1 > 0$. In other words: \[ 0 < \sum_{i=0}^{n-1} x^i \iff \text{$n$ is odd or $x > -1$}. \]

geom_sum_ne_zero theorem

[Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hx : x ≠ -1) (hn : n ≠ 0) : ∑ i ∈ range n, x ^ i ≠ 0

Full source

theorem geom_sum_ne_zero [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
    (hx : x ≠ -1) (hn : n ≠ 0) :
    ∑ i ∈ range n, x ^ i∑ i ∈ range n, x ^ i ≠ 0 := by
  obtain _ | _ | n := n
  · cases hn rfl
  · simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]
  rw [Ne, eq_neg_iff_add_eq_zero, ← Ne] at hx
  obtain h | h := hx.lt_or_lt
  · have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
    split_ifs at this
    · exact this.ne
    · exact (zero_lt_one.trans this).ne'
  · exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'

Non-vanishing of Geometric Sum for $x \neq -1$ in Strict Ordered Rings

Informal description

Let $R$ be a strict ordered ring with a linear order. For any element $x \in R$ such that $x \neq -1$ and any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ is nonzero, i.e., $\sum_{i=0}^{n-1} x^i \neq 0$.

geom_sum_eq_zero_iff_neg_one theorem

[Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n ≠ 0) : ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n

Full source

theorem geom_sum_eq_zero_iff_neg_one [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n ≠ 0) :
    ∑ i ∈ range n, x ^ i∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n := by
  refine ⟨fun h => ?_, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
  contrapose! h
  have hx := eq_or_ne x (-1)
  rcases hx with hx | hx
  · rw [hx, neg_one_geom_sum]
    simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true]
  · exact geom_sum_ne_zero hx hn

Geometric Sum Vanishes if and only if $x = -1$ and $n$ is Even

Informal description

Let $R$ be a strict ordered ring with a linear order. For any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ equals zero if and only if $x = -1$ and $n$ is even.

geom_sum_neg_iff theorem

[Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n ≠ 0) : ∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

Full source

theorem geom_sum_neg_iff [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (hn : n ≠ 0) :
    ∑ i ∈ range n, x ^ i∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0 := by
  rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]

Negativity Criterion for Geometric Sum in Strict Ordered Rings

Informal description

Let $R$ be a strict ordered ring with a linear order. For any element $x \in R$ and any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} x^i$ is strictly negative if and only if $n$ is even and $x + 1 < 0$. In other words: \[ \sum_{i=0}^{n-1} x^i < 0 \iff \text{$n$ is even and $x < -1$}. \]

Nat.geomSum_eq theorem

(hm : 2 ≤ m) (n : ℕ) : ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Full source

/-- Value of a geometric sum over the naturals. Note: see `geom_sum_mul_add` for a formulation
that avoids division and subtraction. -/
lemma Nat.geomSum_eq (hm : 2 ≤ m) (n : ℕ) :
    ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1) := by
  refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm
  simpa only [tsub_add_cancel_of_le (one_le_two.trans hm), eq_comm] using geom_sum_mul_add (m - 1) n

Geometric Sum Formula for Natural Numbers: $\sum_{k=0}^{n-1} m^k = \frac{m^n - 1}{m - 1}$ when $m \geq 2$

Informal description

For any natural numbers $m \geq 2$ and $n$, the geometric sum $\sum_{k=0}^{n-1} m^k$ equals $\frac{m^n - 1}{m - 1}$.

Nat.geomSum_lt theorem

(hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k ∈ s, m ^ k < m ^ n

Full source

/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of
`m ≥ 2` is less than `m ^ n`. -/
lemma Nat.geomSum_lt (hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k ∈ s, m ^ k < m ^ n :=
  calc
    ∑ k ∈ s, m ^ k ≤ ∑ k ∈ range n, m ^ k := sum_le_sum_of_subset fun _ hk ↦
      mem_range.2 <| hs _ hk
    _ = (m ^ n - 1) / (m - 1) := Nat.geomSum_eq hm _
    _ ≤ m ^ n - 1 := Nat.div_le_self _ _
    _ < m ^ n := tsub_lt_self (by positivity) zero_lt_one

Sum of Powers Bound: $\sum_{k \in s} m^k < m^n$ when $m \geq 2$ and $\forall k \in s, k < n$

Informal description

For any natural numbers $m \geq 2$ and $n$, and for any finite set $s$ of natural numbers where each element $k \in s$ satisfies $k < n$, the sum of $m^k$ over all $k \in s$ is strictly less than $m^n$.

Main statements