## Stream: new members

### Topic: how is log defined in lean?

#### Alex Kontorovich (May 07 2020 at 17:19):

I see that exp is defined as the limit of sum x^n/n! but I can't seem to find where log is defined? I'm hoping to be able to access something like: -log(1-x)=x+x^2/x+x^3/3+... (for |x|<1/2, say)? Thanks!

#### Kevin Buzzard (May 07 2020 at 17:23):

Searching for log at https://leanprover-community.github.io/mathlib_docs/ gives some info.

#### Alex Kontorovich (May 07 2020 at 17:27):

Thanks Kevin, I clicked around there for a while before asking, to no avail -- any more direct pointers please? What I'm hoping is the analog of:

def exp' (z : ℂ) : cau_seq ℂ complex.abs :=
⟨λ n, (range n).sum (λ m, z ^ m / nat.fact m), is_cau_exp z⟩


which I see in the complex/exponential file, but I don't see a similar definition for log?... Thanks!

#### Kevin Buzzard (May 07 2020 at 17:31):

hang on, I'll have a look

#### Patrick Massot (May 07 2020 at 17:34):

This brings to https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/exp_log.html#real.log really fast

#### Kevin Buzzard (May 07 2020 at 17:34):

log is defined on p200 of that file, as the inverse of exp (at least for positive inputs).

#### Kevin Buzzard (May 07 2020 at 17:35):

But I can't see the infinite sum fact there.

#### Alex Kontorovich (May 07 2020 at 17:36):

Ah thanks; I didn't know what classical.some was doing... So it's an inverse function; and is that expansion proved anywhere in Lean?

#### Kevin Buzzard (May 07 2020 at 17:37):

Not that I can see. It might be tricky to prove as well, because I don't think we have the fact that we can differentiate a power series term by term, which would be the way I'd prove it.

#### Kevin Buzzard (May 07 2020 at 17:37):

I don't think we have fund thm of calc either

#### Patrick Massot (May 07 2020 at 17:37):

The classical.some is hard to read in html doc because the proof is elided, but you can click the GitHub link to see the actual code

#### Patrick Massot (May 07 2020 at 17:38):

Both those things are in the pipes

#### Patrick Massot (May 07 2020 at 17:38):

FTC has an open PR, and differentiation of power series is very close to what Sébastien does those days

#### Alex Kontorovich (May 07 2020 at 17:41):

One could perhaps prove it as just a combinatorial identity -- open both series exp(-log(1-x)) = 1+[-log(1-x)]+[-log(1-x)]^2/2!+...
=1+[x+x^2/2+x^3/3+]+[x+x^2/2+x^3/3+]^2/2!+...
Open things up and see that everything combines into 1+x+x^2+x^3+... which Lean does know is (1-x)^(-1)...?

#### Patrick Massot (May 07 2020 at 17:53):

It sounds like a nice project (and certainly something we want in mathlib). If you want to give it a try you should coordinate with Sébastien.

#### Kevin Buzzard (May 07 2020 at 17:58):

Of course if you prove it using power series you'll still have the issue of checking all the rearrangements converge

#### Alex Kontorovich (May 07 2020 at 19:14):

Sure, sounds like fun. I'm sorry, I'm a newbie here - what is Sebastien's last name?

#### Alex Kontorovich (May 07 2020 at 19:16):

The convergence of the log power series should be "easy", no? It's dominated termwise by the geometric series, which Lean knows...? (Of course, a lot of things I thought would be easy haven't been...)

#### Johan Commelin (May 07 2020 at 19:21):

@Alex Kontorovich : @Sebastien Gouezel

#### Patrick Massot (May 07 2020 at 20:11):

Alex, I'm really sorry about that. There are many many people on this chat now, and I try to answer many questions really fast. I'm a bit lost about who knows who and what.

#### Sebastien Gouezel (May 10 2020 at 09:33):

Alex Kontorovich said:

I see that exp is defined as the limit of sum x^n/n! but I can't seem to find where log is defined? I'm hoping to be able to access something like: -log(1-x)=x+x^2/x+x^3/3+... (for |x|<1/2, say)? Thanks!

#2646

Last updated: May 08 2021 at 04:14 UTC