Mandelbrot - Lean 4 version

Stream: maths

[Geoffrey Irving]

I ported https://github.com/girving/ray to Lean 4, so now Lean 4 knows that the Mandelbrot set is connected (and also Hartogs' theorem that functions which are analytic along each axis are jointly analytic)

I'd be curious to upstream parts of this is there is interest. I'm not sure the best way to go about this, since it's a fair amount of code. One option is if someone is interested in skimming the overall structure (file comments) and getting a sense what is worth cleaning up and upstreaming (I'm happy to do nontrivial cleanup). Another route is me suggesting things: three possible starting points are

1. AnalyticManifold.lean and RiemannSphere.lean (or rather the holomorphic structure in RiemannSphere, if we should use the existing sphere type). E.g., https://github.com/girving/ray/tree/main/Ray/AnalyticManifold
2. The bound tactic (https://github.com/girving/ray/blob/main/Ray/Tactic/Bound.lean), which is used heavily throughout the rest of the repo, including for both Hartogs' theorem and holomorphic dynamics results. This needs significant cleanup, and I'm not sure if it's wanted at all due to relationships with positivity and mono, but it will be hard to upstream much else (except for (1)) without something similar to it.
3. Various tiny lemmas, such as topology lemmas in https://github.com/girving/ray/blob/main/Ray/Misc/Topology.lean

Here are directory and file counts:

% for d in *; do wc $d/*.lean; echo; done
     661    5467   34456 Analytic/Analytic.lean
     146    1031    7002 Analytic/Holomorphic.lean
     194    1796    9174 Analytic/Products.lean
     165    1557    7740 Analytic/Series.lean
     272    2448   13505 Analytic/Uniform.lean
    1438   12299   71877 total

     740    5980   42358 AnalyticManifold/AnalyticManifold.lean
     132    1441    7593 AnalyticManifold/GlobalInverse.lean
     326    2567   16419 AnalyticManifold/Inverse.lean
      68     576    3661 AnalyticManifold/LocalInj.lean
     241    1954   13793 AnalyticManifold/Nonseparating.lean
     436    3861   24925 AnalyticManifold/Nontrivial.lean
     392    3161   20693 AnalyticManifold/OneDimension.lean
     262    2455   15576 AnalyticManifold/OpenMapping.lean
     604    4329   33035 AnalyticManifold/RiemannSphere.lean
    3201   26324  178053 total

     247    1910   12648 Dynamics/Bottcher.lean
     704    6486   34202 Dynamics/BottcherNear.lean
     635    5029   32804 Dynamics/BottcherNearM.lean
     653    5947   35532 Dynamics/Grow.lean
      42     217    1532 Dynamics/Mandelbrot.lean
    1418   12876   76623 Dynamics/Multibrot.lean
     110     748    5834 Dynamics/MultibrotConnected.lean
     242    2174   14282 Dynamics/Multiple.lean
     242    1961   12465 Dynamics/Postcritical.lean
     527    4559   27954 Dynamics/Potential.lean
     343    2982   18802 Dynamics/Ray.lean
    5163   44889  272678 total

     153    1325    7347 Hartogs/Duals.lean
     357    2762   17713 Hartogs/FubiniBall.lean
     831    7322   43772 Hartogs/Hartogs.lean
     102     694    4269 Hartogs/MaxLog.lean
     612    5634   33450 Hartogs/Osgood.lean
    1091    9503   59868 Hartogs/Subharmonic.lean
    3146   27240  166419 total

      21     126     682 Misc/AbsoluteValue.lean
     112     824    5654 Misc/AtInf.lean
     426    3743   19401 Misc/Bounds.lean
      62     424    3229 Misc/ChartedSpace.lean
     275    2431   15739 Misc/Connected.lean
     195    1927   10392 Misc/Continuation.lean
      83     573    3368 Misc/Finset.lean
      41     275    1651 Misc/Max.lean
     353    2777   18017 Misc/Measure.lean
     266    2325   14634 Misc/Multilinear.lean
      20     108     663 Misc/Pow.lean
      65     439    2791 Misc/Prod.lean
     557    5405   31829 Misc/Topology.lean
      85     587    4182 Misc/TotallyDisconnected.lean
    2561   21964  132232 total

     333    2691   15470 Tactic/Bound.lean
      13      36     253 Tactic/BoundRules.lean
     346    2727   15723 total

[Jireh Loreaux]

Your bound tactic, at a cursory glance, seems to perform similar duties to gcongr (with a variety of dischargers). Can you compare and contrast the two tactics so we can get a better idea?

[Geoffrey Irving]

bound and gcongr do look similar, but does gcongr use DiscrTree? If not, how is it fast for a large number of lemmas?

Another small difference is that bound applies le_of_lt on the fly in appropriate places, and this is very important for ergonomics. Ah, looks like gcongr does that too.

[Yaël Dillies]

I should also mention that @Jovan Gerbscheid has written a generalised rewrite tactic which could be useful here.

[Patrick Massot]

Geoffrey, looking only at your messages here, I would say everything is in scope for Mathlib.

[Geoffrey Irving]

^ Thank you! But I think the main worry I'd have is whether the various machinery is deemed general enough. At a minimum I expect reviewers to reasonably want a bunch of refactoring.

[Geoffrey Irving]

I'll also say that someone fluent in sheafs and such could probably make a significantly cleaner proof , but I don't know that stuff well so I went with lower tech arguments (that amount to the same thing, but less generally).

[Geoffrey Irving]

@Jireh Loreaux And yep, gcongr does use DiscrTree, so it would be similar speed. It doesn't seem to have syntax for passing in extra lemmas (things like bound [h.1] occur all the time), but that's not hard to add. I think the gcongr_forward machinery might miss some cases that the logic in bound would catch: bound can jump back from ≤ to <if a lemma has that kind of side condition (and I think at least one does), and it seems like forward only handles unapplied lemmas. But these issues may be easy to fix, or I might be imagining them.

[Patrick Massot]

@Mario Carneiro, @Heather Macbeth :up:

[Geoffrey Irving]

@Jireh Loreaux My tentative conclusion is that with not much work bound can either go away entirely or call into internals of gcongr.

[Jireh Loreaux]

Thanks for that assessment.

[Wen Yang]

Thank you for your work! I am going to formalize hyperbolic surfaces and I am trying to build it on the RiemannSphere.lean in your work. I shall be glad to see them in the mathlib!

[Henrik Böving]

And naive computer science me was thinking someone drew a pretty picture upon reading the title of this topic :( Still nice work though!

@Tomas Skrivan can you make a pretty picture out of this? :P

[Kevin Buzzard]

This is already done IIRC (I'm pretty sure I tweeted about it a year or so ago)

[Geoffrey Irving]

I’m going to make a formalized picture using interval arithmetic, the Koebe quarter theorem, and injectivity of the Bottcher map soon.

[Geoffrey Irving]

Presumably that’s not the picture that was already made: mine will have some red “who knows” pixels.

[Kevin Buzzard]

[Jason Rute]

@Kevin Buzzard This is just using the usual (unverified) algorithm I'm sure where you just iterate a fixed number of steps. What I think @Geoffrey Irving is thinking is something like this
image.png
as in this the paper Images of Julia Sets You Can Trust (slides).

[Jason Rute]

Geoffrey Irving said:

Presumably that’s not the picture that was already made: mine will have some red “who knows” pixels.

Funny, I remember a similar drawing to the Julia set above but of a Mandelbrot set instead of a Julia set also with red pixels for the unknown areas. Mandela effect?

[Kevin Buzzard]

Yes this is just a picture using the usual algorithm; I was just noting that what Henrik suggested was already done in Lean. I'm well aware that Geoffrey is suggesting something rather different.

[Jason Rute]

(Also, I can't help mentioning my favorite tidbit about the Mandelbrot set. We currently don't know if the area of the Mandelbrot set is computable. It probably is and we even know how to compute it if certain hypotheses hold, but we can't be sure.)

[Kevin Buzzard]

Coincidentally I think Geoffrey holds the record for computing it :-) (or more precisely for computing the coefficients of the Boettcher map): https://github.com/girving/mandelbrot

[Geoffrey Irving]

I should clarify that I have the record for computing Bottcher power series coefficients (2^27 of them), which gives you an area estimate as described in that repo, but the area estimate record is due to Fisher and Hill (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.53.2337&rep=rep1&type=pdf) using the Koebe quarter theorem but not interval arithmetic. They also did it a while ago, so we should be able to beat their estimate as a theorem (though using native_decide of course).

[Geoffrey Irving]

Probably we don’t want to commit that theorem to Mathlib, though.

[Geoffrey Irving]

Jason Rute said:

(Also, I can't help mentioning my favorite tidbit about the Mandelbrot set. We currently don't know if the area of the Mandelbrot set is computable. It probably is and we even know how to compute it if certain hypotheses hold, but we can't be sure.)

Yep, though of course for computability you need a way weaker assumption than hyperbolicity: all you need is not-uncomputably-slow convergence of the coefficients of the Bottcher series, and it’s really really implausible that it’s uncomputable how slowly they converge.

[Geoffrey Irving]

They’re maddeningly noisy and heavy-tailed, though.

[Jason Rute]

Yes, it would be crazy novel (and dare I say unprecedented) to have a naturally occurring convergent series whose convergence is uncomputable.

[Geoffrey Irving]

Edit: Of course the coefficients converge to zero as O(1/sqrt(n)) trivially; I mean how fast the partial sums of the area series converge.

[Geoffrey Irving]

I spent a good while tinkering with the first 2^27 area series terms a_n to try to conjecture a convergence rate, but all I got was

1. They look like they’re O(1/n).
2. Plausibly limsup n a_n > 0: there are Theta(1/n) terms occurring sparsely forever
3. The locally averaged terms converge faster, of course, but the local distribution is so heavy tailed that I couldn’t model it well enough to make a conjecture.

But this is mostly off topic: feel free to ping if that experimental math aspect is interesting.

[Oliver Nash]

Somewhat off-topic but a cute goal might be to formalise the statement appearing in this question: https://mathoverflow.net/questions/215187/is-there-a-reference-for-computing-pi-using-external-rays-of-the-mandelbrot

[Geoffrey Irving]

What would be the right next step for upstreaming? I’d be curious to do at least one piece soon for learning purposes.

[Sebastien Gouezel]

You should open a PR, a small one to get started (ideally less than 100 lines, but could go up to 200 lines ). For instance some of your lemmas on analytic functions, say. The PR process is explained on https://leanprover-community.github.io/contribute/index.html#making-a-pull-request-pr. Most importantly, it should be done from a branch on the main mathlib repo, not your own fork, to make sure that all the infrastructure works on it (and notably the cache, to make sure that people can review the PR without having to build the files themselves).

[Sebastien Gouezel]

Often, the first PR is a little bit painful, with a lot of back and forth between author and reviewer, because we are quite picky on style details and suitable generality and things like that. Apologies in advance, but please bear with us, this is important to make sure that mathlib is a unified library and not a disjoint union of individual contributions (and it won't be specific to you, of course!)

[Anatole Dedecker]

Also it will probably be easier if you start by PR-ing lemmas that fit in existing APIs (Sébastien’s recommandation works perfectly for that) rather than new APIs like your AnalyticManifold file. You should of course open PR for those too at some point, but there will probably be way more discussion on them and they will potentially require substantial rewrite (I haven’t actually looked at them closely) so it’s best to do that once you’re used to the PR process.

[Geoffrey Irving]

Great! I will send a first PR soon.

[Johan Commelin]

@Geoffrey Irving Here's an invitation for push access to non-master branches of mathlib: https://github.com/leanprover-community/mathlib4/invitations

[Geoffrey Irving]

Accepted, thanks!

[Geoffrey Irving]

Here's a very small first PR: https://github.com/leanprover-community/mathlib4/pull/7677