HarmonicOn and SubharmonicOn

Stream: mathlib4

[Geoffrey Irving]

I needed subharmonic and harmonic functions in one complex dimension for the proof of Hartogs' theorem, in order to use Hartogs' lemma. Specifically what I needed was that log |f z| is subharmonic for f analytic. (This is awkward due to the singularity if f z = 0, so instead I worked with max c (log |f z|).)

I'm interested in upstreaming Hartogs theorem. The question is how much of this 1D harmonic theory to import, since my impression is that eventually mathlib will have a much more general version.

The subharmonic and harmonic theory is https://github.com/girving/ray/blob/main/Ray/Hartogs/Subharmonic.lean. It's currently over 1000 lines, since it requires the maximum principle and thus harmonic extensions from circles to disks, etc. I'm not an expert here, of course, so it's likely large simplifications are possible.

This file and its dependencies use bound heavily as well, but that doesn't need to block at least discussion.

[Geoffrey Irving]

Ah, also: the subharmonic theory is likely simpler if I switch to superharmonic functions to ENNReal, both because the eventual measure theory I need is there (Fatou's lemma) and because then the singularity in -log |f z| is fine (though one still needs to scale before taking logs to avoid the cutoff at 0).

[Antoine Chambert-Loir]

My first reaction was “go for it”, but I then remembered that in complex analysis, people work with psh functions all the time, with “s”=”sub”. That means they have internalized the analogue of Fatou's lemma for these functions. So it might be neater to add this to mathlib.

[Geoffrey Irving]

What's the definition of psh function you have in mind? https://en.wikipedia.org/wiki/Plurisubharmonic_function seems to first define 1D subharmonic functions and then lift the definition up by requiring subharmonicity on each line.

[Geoffrey Irving]

Also I should clarify that I don't need these on manifolds currently, just for one flat complex dimension.

[Antoine Chambert-Loir]

That's indeed the definition I know. And in the complex setting, same, but with complex lines.

[Antoine Chambert-Loir]

To pass from complex line to manifolds, one has to prove invariance under complex diffeomorphisms.

[Antoine Chambert-Loir]

For a reference, I'd go to Demailly's book and formalize everything line by line.

[Geoffrey Irving]

Would an eventual desire to get to psh change the initial step of getting subharmonic defined in 1D? If psh is a definition on top of 1D, it seems like that one would a 1D definition even more useful, as opposed to wanting to define general dimension subharmonic functions.

[Antoine Chambert-Loir]

In the complex case, psh is on top of 1D complex, which is 2D real…
NB. 1D-psh functions are convex functions.

[Geoffrey Irving]

Got it, so one still wants HarmonicOn and SubharmonicOn to be defined over any normed space.

Which book do you mean, specifically? I'd likely be up for lifting my current theory such that it matches with a subset of a book, but probably not up for formalizing the rest of the book. :)

[Antoine Chambert-Loir]

Demailly, Complex analytic and differential geometry, https://www-fourier.ujf-grenoble.fr/~demailly/manuscripts/agbook.pdf (sections I.4 and I.5)

For the complex case, especially 1D, the book by Ransford, Potential theory in the complex plane, is nice and reasonably paced.

[Geoffrey Irving]

Hmm, do we have integrals over spherical shells, and the sphere/ball Fubini theorem? I have the 1D complex case at https://github.com/girving/ray/blob/main/Ray/Hartogs/FubiniBall.lean, but I’m not sure we can easily write down the general normed space case.

[Junyan Xu]

#7693
(integral_fun_norm_addHaar requires the function to be constant on each sphere, so you may want to use docs#MeasureTheory.integral_prod_symm at the line ∫ x : sphere (0 : E) 1 × Ioi (0 : ℝ), f x.2 ∂μ.toSphere.prod (.volumeIoiPow (dim E - 1)) instead of integral_fun_snd).