A million digits of log 2

Stream: general

[Bhavik Mehta]

A mini announcement: Here I proved a rational approximation to log 2 up to about a million digits. The code is pretty messy, but it originated in work I did in early 2023, then used in my Ramsey project and then updated for Chris Birkbeck's LeanBridge project. (Neither of these projects needed close to this much precision, but I got a bit carried away :slight_smile: ) The key part is the command on line 928, which finds and defines the rational approximation and verifies that it's correct up to about 3321929 binary digits. None of this uses ofReduceBool, just the usual three axioms.

[Michael Rothgang]

How easy would it be to upstream this to mathlib? To what extent can this be generalised? A tactic to approximate logarithms would be pretty nice (especially coupled with an interval arithmetic tactic that the FRO is working on, if I remember correctly).

[Bhavik Mehta]

The method here is to approximate logs of 1+1/n for arbitrary positive naturals n, then this lemma

lemma decompose :
    log 2 = 7 * log (16 / 15) + 5 * log (25 / 24) + 3 * log (81 / 80) := by

is used to generate an approximation of log 2. So, it generalises trivially to rationals 1+1/n, and can be generalised to work for rationals which can be written as a product of things of this form.
Getting other logs can also be done (as I did in the Ramsey project), but I haven't worked on getting it to high precision (my best so far is 30 digits, compiling in about 0.1 seconds).

The aim here, however, was to get a high precision, at the potential cost of usability. My understanding is that the general interval arithmetic work should subsume this, and be strictly more general (since it's not just for logs!), but instead the aim here was a special-purpose setup. Indeed, while bound_log2'% is what's in the example for a million digits, the other version bound_log2% is faster for up to the tens of thousands of digits, but is too memory intensive to get much higher; so there's already a tradeoff between practicality and precision.

As such, it's not clear to me that this should be in mathlib? Do we really want some file in mathlib taking 10 minutes to get a million digits of this specific constant?
And the FRO's work, in my understanding, will likely be faster for the kind of (more reasonable) precision useful in mathlib.

All that said, I'd like to make this into a standalone repo with a friendlier interface that one could import if desired, and if there's general agreement that something like this should be in mathlib, I'm not really opposed to it.

[Bhavik Mehta]

And as an aside, I also proved some more wild decompositions of log 2, but ended up not using them:

lemma main : 122324552 * log (929166876 / 929166875) +
             -75806406 * log (920577798 / 920577797) +
             -58834645 * log (876219201 / 876219200) +
             52889168 * log (658831251 / 658831250) +
             -9727598 * log (611969281 / 611969280) +
             90645248 * log (591130375 / 591130374) +
             -61102303 * log (490145734 / 490145733) +
             108313849 * log (487530862 / 487530861) +
             6176249 * log (457318225 / 457318224) +
             -29974075 * log (415704576 / 415704575) +
             23287250 * log (382241601 / 382241600) +
             64465156 * log (370256250 / 370256249) +
             11016954 * log (308950929 / 308950928) +
             12805279 * log (293635441 / 293635440) +
             19164767 * log (136835245 / 136835244) = log 2 := by calc

[Bhavik Mehta]

Here's a PR for the main bit of analysis (it's not much!) needed for this: #31487

[Eric Wieser]

Can you point to where log2Approx3321929 is defined? Github search isn't finding it for me Oh, it comes from the meta code!

[Bhavik Mehta]

Yup, this is one of the things I'd like to change, it is confusing! Ultimately using eval% would be nicer here, but currently the code finding the approximation and proving it are very tightly linked, so for now I made it just one command.