how is log defined in lean?

Stream: new members

[Alex Kontorovich]

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]

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

[Alex Kontorovich]

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]

hang on, I'll have a look

[Patrick Massot]

Did you actually typed log in the search form?

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Alex Kontorovich]

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]

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]

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

[Patrick Massot]

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]

Both those things are in the pipes

[Patrick Massot]

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

[Alex Kontorovich]

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]

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]

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

[Alex Kontorovich]

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

[Alex Kontorovich]

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]

@Alex Kontorovich : @Sebastien Gouezel

[Patrick Massot]

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]

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