Mandelbrot connectedness

Stream: maths

[Geoffrey Irving]

https://github.com/girving/ray proves that the Mandelbrot set and its complement are connected, by exhibiting the analytic Böttcher homeomorphism from the exterior of the Mandelbrot set to the exterior of the closed unit disk (actually we add the point at infinity and map to the open unit disk). The main result is https://github.com/girving/ray/blob/main/src/mandelbrot.lean#L25. Most of the work is done for a general holomorphic map from a compact Riemann surface to itself. It's still Lean 3, but once I port it to Lean 4 it would be nice to upstream at least some of it (it defines complex manifolds, for instance).

[Yaël Dillies]

Can you give us an outline for how big the project is? How many lines of code for the prerequisites (that's the most relevant figure for me as a mathlib reviewer)? for the future mathlib contributions? for the proof of each big theorem?

[Geoffrey Irving]

I’ll give you some statistics later, since I’d want to give separate counts for the different prerequisite chunks (and then any subset could be upstreamed). But regardless, any upstreaming would only be after the Lean 4 port.

[Geoffrey Irving]

Here's a file + line count breakdown: https://docs.google.com/spreadsheets/d/1L2V7eXWDd7XnQJF8fUF1YgAEPGdjw40F1TvqCuZuYLk/edit?usp=sharing

Category - Total
Miscellaneous small lemmas - 2373
Tactics - 161
Analytic functions - 1447
Likely removable - 208
Complex manifolds - 3180
Hartogs' theorem - 2992
Complex dynamics - 4799
Overall - 15160

By "miscellaneous small lemmas" I mean files where one or a couple lemmas at a time could be a PR by themselves if it made sense (some of these may actually already be in mathlib, if I failed to notice them). Example:

-- continuous_at in terms of 𝓝[{x}ᶜ] x
lemma continuous_at_iff_tendsto_nhds_within {A B : Type} [topological_space A] [topological_space B]
    {f : A → B} {x : A} : continuous_at f x ↔ tendsto f (𝓝[{x}ᶜ] x) (𝓝 (f x)) := begin
  rw continuous_at, constructor,
  exact λ t, t.mono_left nhds_within_le_nhds,
  intro t, rw ←nhds_within_compl_singleton_sup_pure,
  exact filter.tendsto.sup t (tendsto_pure_nhds _ _),
end

[Kalle Kytölä]

This is very cool! I really hope you port this to Lean4 and PR to Mathlib soon.

[Yury G. Kudryashov]

I had a quick look at a couple of "basic" files. It looks like quite a few of the lemmas are already in mathlib.

[Yury G. Kudryashov]

Of course, I'm talking about basic lemmas like continuous_on.compact_max (in your code) vs docs#IsCompact.exists_isMaxOn (in Mathlib), not something more advanced.

[Yury G. Kudryashov]

And is_empty.continuous is docs#continuous_of_discreteTopology

[Junyan Xu]

Contragulations! Link to previous thread on Hartogs's theorem

[Geoffrey Irving]

@Yury G. Kudryashov: Yep, that duplication is unsurprising (I predicted it earlier in the thread). Some of it is due to lemmas appearing after I started, but most are likely just my failures in searching the docs.

[Yury G. Kudryashov]

Do you plan to migrate it to Lean 4 & PR?

[Geoffrey Irving]

I've started the Lean 4 port, and yep, I do hope to PR parts of it. I'll leave it to others how far to go from preliminaries to core results: simple lemmas and ComplexManifold seem clearly good to upstream, for instance, and Hartogs' theorem seems good, but I'm far from confident the holomorphic dynamics work is expressed in a sufficiently canonical way that it would be appropriate.

[Yury G. Kudryashov]

Do you use mathport?

[Geoffrey Irving]

Yes to mathport, though I used some admittedly ugly hacks to get it to format my tactic correctly (https://github.com/girving/ray/blob/main/src/tactics.lean#L72), and it leaves a bunch of holes separate from that. I don't think it will take too long, but I haven't done very much of it yet.

[Geoffrey Irving]

@Yury G. Kudryashov Incidentally, me missing continuous_of_discreteTopology is an example of a general phenomenon I hit a bunch of times: I would search for a specific version of theorem but get all the keywords wrong as Mathlib only has the general version. It will be nice when we have the fancy search machinery.

[Yury G. Kudryashov]

Lean 4 exact? should work in many cases.

[Geoffrey Irving]

Nice! Is that better than Lean 3 library_search? That seemed to mostly time out for me in interesting cases.

[Kevin Buzzard]

Yes, it's much faster now

[Junyan Xu]

Controllism x Mandelbrot :)
https://x.com/gener8ive/status/1703102771078066252