How to use sort

Stream: new members

[Matthew Honnor]

Dear all, I am trying to make some simple definitions but I don't know how to get lean to view the complex numbers as a sort rather then a type. I am trying to use \Sigma' to define a series and this is giving me an error:

has type
ℕ → ℂ : Type
but is expected to have type
ℕ → Sort ? : Type ?

I am also not aware of what a sort is! Any help or reccomendations for reading on this would be great.

Thanks in advance.

[Kevin Buzzard]

Can you post the code which created this error? See #mwe for a guide on how to ask effective questions here. PS the issue is probably not what you think it is: the error seems to indicate that Lean was expecting a type universe rather than the complex numbers. Oh -- also #backticks

[Kevin Buzzard]

PS hi Matthew!

[Matthew Honnor]

Thanks for letting me know about mwe and backticks, here is the code that created this error.

import analysis.complex.basic

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

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

Thanks again

[Ruben Van de Velde]

I think you're using the wrong Σ'

[Patrick Johnson]

You need ∑ (type with \sum)

[Ruben Van de Velde]

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

works

[Matthew Honnor]

Thanks, that works now. How does the noncomputable def work?