Finite geometric sums

Stream: Is there code for X?

[Mark Gerads]

I am working on it because I was unable to find it. What I have so far:

import analysis.specific_limits
import analysis.normed_space.basic
import analysis.complex.basic
import data.complex.basic
import topology.algebra.infinite_sum
import analysis.special_functions.pow

noncomputable theory

open topological_space normed_space set
open_locale topological_space
open_locale classical big_operators nat
open real is_absolute_value finset cau_seq

namespace complex

lemma finiteGeometricSum (z:ℂ) (n:ℕ) (h:z≠1):((z^n-1)/(z-1)=∑ m in range n, z ^ m):=
begin
  induction n,
  simp,
  have h1 : ((z ^ n_n - 1) / (z - 1) + z ^ n_n = (∑ (m : ℕ) in range n_n, z ^ m) + z ^ n_n),
  exact congr_fun (congr_arg has_add.add n_ih) (z ^ n_n),
  have h2 : ((∑ (m : ℕ) in range n_n, z ^ m) + z ^ n_n = ∑ (m : ℕ) in range n_n.succ, z ^ m),
  exact (sum_range_succ (λ (x : ℕ), z ^ x) n_n).symm,
  -- have h3 : (z ^ n_n * (z - 1) = z ^ n_n * (z - 1)),
  -- exact rfl,
  have h4 : (z ^ n_n * z - z ^ n_n * 1 = z ^ n_n * (z - 1)),
  exact (mul_sub (z ^ n_n) z 1).symm,
  have h5 : (z ^ n_n * z = z ^ (n_n + 1)),
  exact mul_comm (z ^ n_n) z,
  have h6 : (z ^ (n_n + 1) - z ^ n_n * 1 = z ^ n_n * (z - 1)),
  --substitute h5 in h4

  --have h : (z ^ n_n * (z - 1) / (z - 1) = z ^ n_n),
  --have h : ((z ^ n_n.succ - 1) / (z - 1) = (z ^ n_n - 1) / (z - 1) + z ^ n_n),
end

end complex

Context: I need it to show that any [[size n geometric sum] of [an nth root of unity other than 1]] equals 0. This can be generalized to roots of unity outside the complex numbers.

[Heather Macbeth]

Have you seen lemmas like docs#geom_sum_mul ?

[Mark Gerads]

No. I will look now.

[Mark Gerads]

It looks almost like what I want. Thanks.

[Mark Gerads]

With the right import, this works

lemma finiteGeometricSum (z:ℂ) (n:ℕ) (h:z≠1):((z^n-1)/(z-1)=∑ m in range n, z ^ m):=
begin
  exact (geom_sum_eq h n).symm,
end

[Mark Gerads]

Yay, library_search!,.

[Mark Gerads]

The trouble with library_search is that it only searches the imports rather than all of mathlib.

[Eric Rodriguez]

ring_theory.roots_of_unity may be a nice file to check out, btw

[Mark Gerads]

I'll take a look then. :)

[Kevin Buzzard]

You can always run ./scripts/mk_all.sh on the command line and then import all if you want to search all of mathlib.