Zulip Chat Archive

Stream: new members

Topic: how is log defined in lean?


view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (May 07 2020 at 17:23):

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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (May 07 2020 at 17:31):

hang on, I'll have a look

view this post on Zulip Patrick Massot (May 07 2020 at 17:32):

Did you actually typed log in the search form?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (May 07 2020 at 17:35):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 07 2020 at 17:37):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 07 2020 at 17:38):

Both those things are in the pipes

view this post on Zulip 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

view this post on Zulip 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)...?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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...)

view this post on Zulip Johan Commelin (May 07 2020 at 19:21):

@Alex Kontorovich : @Sebastien Gouezel

view this post on Zulip 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.

view this post on Zulip 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