Arithmetic function and general functions

Stream: Is there code for X?

[Ella Yu]

Hi, I learn from mathlib that an "arithmetic function" is defined to be a function that preserves zero. But I'm not sure how can we change the type f: arithmetic_function R to a general function type f: ℕ → R and vice versa. Thanks for your help in advance!

[Eric Wieser]

Writing (f : ℕ → R) will convert a docs#nat.arithmetic_function into a general function

[Eric Wieser]

To go in the other direction, use { to_fun := f, map_zero' := sorry}

[Ella Yu]

I think I didn't make myself clear. My question is: for example, we define l-series as def l_series (f : arithmetic_function ℂ) (z : ℂ) : ℂ := ∑'n, (f n) / (n ^ z) If we now want to state it as a function and trying to say that they are the same, what should I do? Thanks for your help!

[Ella Yu]

Eric Wieser said:

To go in the other direction, use { to_fun := f, map_zero' := sorry}

Hi, I'm not sure if I understand your words correctly. lemma changing_type {f : arithmetic_function R}: (f : ℕ → R):=by sorry Should I have something like this to do the conversion? But there would be an error in type if I did that.

[Eric Wieser]

I don't understandwhat you mean by "state it as a function"; you did state l_series as a function

[Eric Wieser]

Perhaps it would help if you un- #xy your problem; what are you trying to state, and where is this conversion getting in the way?

[Eric Wieser]

Ella Yu said:

Hi, I'm not sure if I understand your words correctly. lemma changing_type {f : arithmetic_function R}: (f : ℕ → R):=by sorry Should I have something like this to do the conversion? But there would be an error in type if I did that.

I was decribing

def changing_type {f : arithmetic_function R} : ℕ → R := (f : ℕ → R)

but obviously you don't want to actually write changing_type f when you could just write (f : ℕ → R)

[Ella Yu]

I see, so if I want to state l_series as a function from ℕ → R, I can just write it as (l_series : ℕ → R). Thank you so much!

[Bart Michels]

I'm not sure that you have your answer already. You can do f : ℕ → R because an arithmetic_function can be coerced to a function. (This in turn is because it is defined as of type zero_hom ℕ R and there is docs#zero_hom.has_coe_to_fun that tells how to coerce it.) If you want to coerce your l_series back to an arithmetic function (I'm not sure if this is possible; depends what you mean by it) then you would need to define explicitly how that is done.

[Eric Wieser]

Right now l_series is a function from arithmetic_function ℂ to a function from ℂ to ℂ, so (l_series : ℂ → ℂ) doesn't make sense

[Ella Yu]

Eric Wieser said:

Right now l_series is a function from arithmetic_function ℂ to a function from ℂ to ℂ, so (l_series : ℂ → ℂ) doesn't make sense

You are right, I see, l-series is not an arithmetic function. But I understand how to do the conversion with an arithmetic function now. Thanks a lot!