Complex dynamics and potential theory

Stream: maths

[Bryan Wang]

Are there any results on complex dynamics (in one variable) and potential theory (e.g. Julia sets, equilibrium measures) in mathlib? A cursory search shows that there was work done on e.g. the Mandelbrot set here but I am not sure what is the status in mathlib.

[Yaël Dillies]

No, it's not in mathlib, but it would be great if it were! Maybe you would be interested in upstreaming some of @Geoffrey Irving's code?

[Geoffrey Irving]

The full repo is https://github.com/girving/ray

[Bryan Wang]

sure, I would be happy to do so! Are there any parts of the repo which have (effectively) already been upstreamed? E.g. I see a file named HolomorphicUpstream which seems like it has been upstreamed to mathlib. Also what would you say is the best place(s) to start currently?

[Geoffrey Irving]

The first thing to do then is try to delete that file and use the Mathlib versions instead. I would love to review PRs!

After that, I would suggest trying to upstream some of the utilities to get some experience doing upstreaming; good places to start would be Topology.lean, Manifold.lean or Manifold/Analytic.lean.

For bigger stuff, there are two routes:

1. Start with Hartogs.lean and dependencies, including subharmonic functions. These are upstreamable separate from any complex dynamics considerations.
2. Remove the dependency of the complex dynamics stuff on Hartogs, then focus only complex dynamics. This is fairly straightforward: it just means threading some multidimensional analyticity through more lemmas in BottcherNear.lean, instead of doing the stunt of proving separate analyticity and invoking Hartogs theorem.

[Geoffrey Irving]

Also, worth saying explicitly that the typical route is to pick some leaf lemmas and definitions, upstream then to Mathlib without changing Ray, then do an update PR to Ray to depend on the new Mathlib versions and remove the local versions.

[Michael Rothgang]

I don't have time to work on the upstreaming, but I'd be excited to see this happen. I'll be happy to review any differential geometry changes you'll PR.

[Michael Rothgang]

(I may also have time to review more, but cannot promise that right now.)

[Bryan Wang]

Thank you very much! I should have some time to work on this over the next few weeks, so hopefully there will be some PRs coming your way :smile:

[Michael Rothgang]

That's great! I may be on holiday in the coming weeks (in which case I'll update my zulip, and reviews will take correspondingly longer).

[Bryan Wang]

@Geoffrey Irving I've opened a PR to delete HolomorphicUpstream.lean!

[Geoffrey Irving]

Merged, thank you! Since the mathematical parts of ray build and then rendering parts do not (due to a compiler bug), I might split out the latter into a separate repo so that the mathematical repo has a clean build.

[Geoffrey Irving]

^ Done, https://github.com/girving/ray just has the math now (and builds), and https://github.com/girving/ray-render has the interval arithmetic-based rendering.

[Bryan Wang]

Thanks!

[Bryan Wang]

Just to clarify something mathematical, when you say to remove the dependency of BottcherNear on Hartogs, you mean do something like the proof of the corollary in the attached picture?
image.png

[Bryan Wang]

By the way, #28286 and #28292 upstream most of the results from Manifold/Analytic.lean that aren't already in mathlib.

[Geoffrey Irving]

@Bryan Wang Roughly, but concretely what it would mean is making all results in BottcherNear.lean account for c from the start. Currently the top half of the file operates at fixed c, then https://github.com/girving/ray/blob/62df108da25af730ab82442b69027e861648d111/Ray/Dynamics/BottcherNear.lean#L535 applies Hartogs' theorem. The alternative is always having f : ℂ → ℂ → ℂ throughout.

But there are some obstacles: https://github.com/girving/ray/blob/62df108da25af730ab82442b69027e861648d111/Ray/Dynamics/BottcherNear.lean#L139 applies docs#Complex.differentiableOn_compl_singleton_and_continuousAt_iff to remove a singularity, and I don't know if Mathlib has a 2D version of this.

[Bryan Wang]

Somehow it feels like it would be slightly complicated to show analyticity in two variables directly (for example, docs#Complex.analyticOnNhd_iff_differentiableOn is also used in line 117 of BottcherNear). Do you think it would make sense to say use continuity and apply Osgood instead? Based on the import graph it seems that Osgood is pretty separate from the rest of Hartogs (and a few other things also depend on Osgood).

[Geoffrey Irving]

Yes, using Osgood is a reasonable path!

[Bryan Wang]

Regarding Hartogs itself, the definition of harmonic functions was recently added to mathlib docs#InnerProductSpace.HarmonicAt using vanishing of the Laplacian, so we would probably want to have the equivalence between harmonicity and the mean-value property in mathlib (I probably won't have time for this, but this is certainly important to have anyway).