definition of exp using tsum

Stream: Is there code for X?

[Mark Gerads]

This seems like it is important. I desire to work on some specific infinite sums of entire functions related to exp, and tsum seems like the best tool. On the other hand, I want my results to be related to exp in mathlib. Does anyone have an easy way to prove this?

import all

open classical complex real

lemma expTsumForm (z:ℂ) : exp z = tsum (λ (k:ℕ), z ^ k / k.factorial):=
begin
  sorry,
end

[Matt Diamond]

https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/exponential.html#exp_eq_tsum ?

[Mark Gerads]

I'll see if I can twist that into the specific form I asked about. Thanks.

[Matt Diamond]

there's also https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/exponential.html#exp_eq_tsum_div

(sorry, I'm a bit out of my element with this one, someone else might have a better suggestion)

[Mark Gerads]

Yeah, I still feel like a newb. I haven't figured out how to apply that theorem to complex numbers because I don't know how to use some theorems like this one, or because I don't even know how to break apart syntactic sugar to deal with lower-level implementations. The learning curve is steep. I'm hoping someone will see that theorem and know how to apply it to complex numbers.

[Matt Diamond]

have you already looked at docs#complex.exp? was that what you were trying to use initially? I may have assumed the wrong exp

[Mark Gerads]

I have skimmed the code. Maybe it is more complicated than it needs to be if we can replace the definition of exp with the tsum version, but I honestly don't know.
And yes, I want to have sums of [tsum]s to make my functions, some of which would be my tsum version of exp. The problem is that I want the tsum version to be known equivalent to whatever is in complex.exp. If someone replaces the definition of complex.exp, to make this easier, I don't mind.

[Anatole Dedecker]

import analysis.special_functions.exponential

open classical complex real

lemma expTsumForm (z:ℂ) : exp z = tsum (λ (k:ℕ), z ^ k / k.factorial):=
begin
  rw [exp_eq_exp_ℂ, exp_eq_tsum_div]
end

[Anatole Dedecker]

Okay so let me explain. In mathlib, we currently have three exponentials : docs#complex.exp, docs#real.exp and docs#exp. The last one strictly supercedes the first two, but the reason why we keep the first two is exactly the reason why the definition of docs#complex.exp looks so strange : the goal is to have docs#complex.exp and docs#real.exp sit as low as possible in the import tree, to avoid importing the whole analysis library each time we want to talk about an exponential of real numbers, e.g for algebraic purposes.

[Mark Gerads]

Thanks. I am saving this in my Lean notes.

[Anatole Dedecker]

The definition of docs#complex.exp basically only depends on the basic construction of real and complex numbers, and in particular completeness, since we define it as the limit of the Cauchy sequence of partial sums (with a really dirty proof of Cauchyness, this file is really horrible to read)

[Anatole Dedecker]

Actually, if you have a look at the proof of complex.exp_eq_exp_ℂ, you'll see that it proves exactly what you want, so you could probably copy-paste the proof and it would work. But I do not recommend doing this : you should just treat complex.exp_eq_exp_ℂ as a black box that translates between the dirty definition and the nice one so that you don't have to look at the dirty definition.

[Mark Gerads]

I have a decent enough computer, so I like scripts/mk_all.sh, import all and running library_search!, suggest, hint to see if I can get anything and I think if library_search! does nothing, then the statement of the lemma is worth implementing in my view, such that library_search would work on the statement. Such is a process of my generating lemma discussions which mostly others prove for me.
@Anatole Dedecker I suggest you take credit for this if it is worth having in mathlib. If it is not worth adding, I am content to have my own library extending mathlib but with this lemma in my notes/library. Thanks again.