Working with tsum

Stream: new members

[Matthew Honnor]

Dear all, I am struggling to work with infinite sums. I have included the code of my specific problem below but I am also interested in how to show that two tsums are equal.

I don't know how to make progress on the proof of the simple lemma below.

import analysis.complex.basic

def analytic_sum_term ( a : ℕ → ℂ ) ( z : ℂ ) ( u : ℂ ) : ℕ → ℂ :=
  λ k , a k *( z - u )^k

noncomputable def analytic_sum ( u : ℂ ) ( a : ℕ → ℂ ) : ℂ → ℂ :=
  λ z, ∑' k : ℕ, analytic_sum_term a z u k

lemma analytic_sum_leading_term { u : ℂ }{ a : ℕ → ℂ }
  ( h : analytic_sum u a u = 0 ) :
  a 0 = 0 :=
  begin
    rw analytic_sum at h,
    norm_num at h,
    rw analytic_sum_term at h,
    simp at h,

  end

Thanks in advance for any help.