Hartog's theorem

Stream: maths

[Geoffrey Irving]

https://github.com/girving/ray proves Hartog's theorem: that separately analytic functions on two complex variables are jointly analytic. The repo is a bit messy at the moment since this is the first Lean thing I've done, but I'd be curious to do the work to gradually clean it up and upstream to mathlib if there is interest. The proof is straightforward but required building up some machinery missing from mathlib, in particular harmonic and subharmonic functions.

[Geoffrey Irving]

The extension to n complex variables shouldn't be too much work, as the result I have for two variables is for any separable Banach space output. The result for more than two variables should follow from induction and currying, rewriting functions from n variables to E to functions from 2 variables to a Banach space of bounded analytic functions.

[Riccardo Brasca]

This is a very nice result, and we surely want it in mathlib.

How long is the proof, with all the prerequisites? I am asking because we are in the process of moving to Lean 4, and a lot of reviewers are working on it, so the PR process is slower than usual.

[Geoffrey Irving]

It’s probably 4-5k lines, unfortunately, though this may shrink during refactoring since I was learning along the way. What’s the ETA for mathlib4? (I’m in no hurry.)

[Riccardo Brasca]

The port has already started, so it really depends on which mathlib files you need (but we are surely quite far from complex analysis, at least a couple of months). If you are interested in learning Lean 4 you can also help porting some files :)

[Geoffrey Irving]

I won’t have capacity to help with the port, but with that ETA it likely makes sense to wait for the port and then upstream into mathlib4. The stuff I use from complex analysis is (1) Cauchy’s theorem and analytic function basics, (2) the Schwarz lemma, and (3) exp and log. But I also use a bunch of measure theory, Baire’s theorem, etc., so there may be other unported dependencies.

[Johan Commelin]

I agree that this would be a great addition to mathlib.

[Johan Commelin]

I think that you shouldn't worry too much about the port right now. You indicate that there's likely some clean-up that should be done. You could start with that.

[Geoffrey Irving]

Would anyone be up for a quick scan through the repo to provide suggestions for that cleanup? I’d benefit hugely from even a small bit of feedback, as so far it’s just been me learning on my own.

[Riccardo Brasca]

You can also open small PR about the prerequisites, if they're small they tend to be reviewed faster, and in any case you get some suggestions.

[Eric Wieser]

I had a quick look at https://github.com/girving/ray/blob/main/src/multilinear.lean since I've done a lot of multilinear map refactors in the past:

• docs#continuous_multilinear_map.curry0 does indeed hold more generally; I just created #18044 to get the more general version, but with a name that matches the existing docs#multilinear_map.of_subsingleton
• re_clm looks like a duplicate of docs#complex.re_clm? I don't see conj_clm anywhere, but suspect we have it
• fst_cmmapcan be written as (continuous_linear_map.fst R M₂ M₃).comp_continuous_multilinear_map (continuous_multilinear_map.of_subsingleton R (M₂ × M₃) (0 : fin 1))

[Junyan Xu]

No one noticed yet the name should be Hartogs :lol:

[Geoffrey Irving]

@Eric Wieser: Thank you! I will make those simplifications.

@Junyan Xu: The name of what? If you mean the repo, it’s called that because the goal was to prove simply connectedness of the Mandelbrot set via external rays.

[Reid Barton]

https://en.wikipedia.org/wiki/Hartogs%27s_extension_theorem (TIL)

[Geoffrey Irving]

@Junyan Xu: Ah, now I understand. :)