Zulip Chat Archive

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:32):

Did you actually typed log in the search form?

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: Dec 20 2023 at 11:08 UTC