Possible PR: Poisson integral and Herglotz representation

Stream: mathlib4

[seb488]

Hi everyone!

We've been working on formalizing two theorems from classical complex
analysis:

• The Poisson integral formula for harmonic functions on the unit disc.
• Building on that, we derive the Herglotz-Riesz representation theorem for positive harmonic functions on the unit disc. The proof uses complex analysis and measure theory (Riesz-Markov-Kakutani representation).

Proposed location: Mathlib/Analysis/Complex/Harmonic/

Github repo: https://github.com/seb488/LeanComplexAnalysis

We have tried to follow mathlib conventions, but we'd appreciate
feedback on whether the file organization makes sense before opening a
PR.

Is this the kind of contribution that would be welcome in mathlib? Any
advice on next steps would be greatly appreciated!

Thanks! :folded_hands:

[Sébastien Gouëzel]

These topics would definitely be great additions to Mathlib! Could you tell us a little bit how you've proceeded, and in particular which LLMs you've used if any? They're often very handy to get working code, but require a little bit more of cleanup afterwards.

[Yan Yablonovskiy 🇺🇦]

You would have to make it complete and remove axioms like

/- # Assumption -/

/-
The property that for any function g in class Σ with expansion g(z) = z + h(1/z)
we have |h'(0)| <= 1 is treated as an axiom. (A consequence of Grönwall's area theorem.)
-/
axiom SigmaCoeffBound :
  ∀ (g : ℂ → ℂ), g ∈ classSigma →
  ∀ (h : ℂ → ℂ), AnalyticOn ℂ h (ball 0 1) →
  (∀ z, 1 < ‖z‖ → g z = z + h (1 / z)) → ‖deriv h 0‖ ≤ 1

In
ComplexAnalysis/UnivalentFunctions/BieberbachSecondCoeff.lean

[seb488]

Yan Yablonovskiy 🇺🇦 schrieb:

You would have to make it complete and remove axioms like

/- # Assumption -/

/-
The property that for any function g in class Σ with expansion g(z) = z + h(1/z)
we have |h'(0)| <= 1 is treated as an axiom. (A consequence of Grönwall's area theorem.)
-/
axiom SigmaCoeffBound :

:thank_you: True. We are working on that one, but it might take many (?) other formalizations. (In particular, Green's theorem, which relates a line integral around a simple closed curve to a double integral over the plane region.) For mathlib, for the time being, we were only thinking about the more fundamental Poisson integral and Herglotz-Riesz integral.

Sébastien Gouëzel schrieb:

These topics would definitely be great additions to Mathlib! Could you tell us a little bit how you've proceeded, and in particular which LLMs you've used if any? They're often very handy to get working code, but require a little bit more of cleanup afterwards.

:thank_you:
Help from AI:
Poisson integral formula: We primarily used Claude.
Herglotz-Riesz representation theorem: We split the proof into smaller steps, following a proof described in Section 3 of Garnett's "Bounded Analytic Functions". We used Aristotle to prove several of these steps, which we then simplified and refactored with assistance from Claude and ChatGPT.

Do you directly spot any necessary cleanup we should address?

[Sébastien Gouëzel]

seb488 said:

Do you directly spot any necessary cleanup we should address?

Unfortunately, yes. LLM code quality is for now very far from the code quality we expect in Mathlib: the proofs are often way too long because the goal of the LLM is just to get there, not get there in the elegant and natural way. Also, the statements are often not in the right generality: looking at the first lemma cauchy_integral_formula_unitDisc, it is written for functions taking values in $\mathbb{C}$ while it should be written for functions in any complex normed space. Real.pi should be written $\pi$ (opening the Real scope), notations should be used for neighborhoods, the proof starts with norm_num at * which is just crazy, and so on.

I am sorry if I sound a little bit negative. LLMs are great to get hints at ways to get a working proof, and to find the relevant lemmas in the library, but in the current state of things it is much much more efficient to write proofs by hand to get good quality code.

[seb488]

We will look into what changes can be made in these directions.

Thanks for your quick response!

[seb488]

Sébastien Gouëzel schrieb:

Also, the statements are often not in the right generality: looking at the first lemma cauchy_integral_formula_unitDisc, it is written for functions taking values in $\mathbb{C}$ while it should be written for functions in any complex normed space. Real.pi should be written $\pi$ (opening the Real scope), notations should be used for neighborhoods, the proof starts with norm_num at * which is just crazy, and so on.

We have updated the file https://github.com/seb488/LeanComplexAnalysis/blob/main/ComplexAnalysis/Harmonic/PoissonIntegral.lean:

• The lemmas/theorems are stated for functions taking values in {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] (with  [CompleteSpace E] if necessary). Only at the end, when using harmonic_is_realOfHolomorphic, we consider functions with values in $\mathbb{C}$ or $\mathbb{R}$.
• We have tried to get rid of all "overkill tactics". [By using #count_heartbeats in with set_option Elab.async false, we get that each proof takes approx. 10,000 heartbeats.]

Are these the right steps towards a cleanup? Any further comments are welcome.

[Kim Morrison]

seb488 said:

Real.pi should be written π (opening the Real scope), notations should be used for neighborhoods

These are things that could be linted for, right? We really need to be turning everything lintable into linters.

[Moritz Doll]

Writing an extensible 'use notation' linter shouldn't be that hard, right? I might give it a try if nobody else is working on it

[Kim Morrison]

I wonder if we should just tell people with partly AI-written proofs that they have to make sure no lemma is longer than 10 lines...

Obviously 10 lines is overkill, but it is cheap advice and otherwise painful to explain the importance of extracting lemmas.

[seb488]

Kim Morrison schrieb:

I wonder if we should just tell people with partly AI-written proofs that they have to make sure no lemma is longer than 10 lines...

Obviously 10 lines is overkill, but it is cheap advice and otherwise painful to explain the importance of extracting lemmas.

:thank_you: We have split the proofs into several smaller lemmas (https://github.com/seb488/LeanComplexAnalysis/blob/main/ComplexAnalysis/Harmonic/PoissonIntegral.lean).

Is this purely a software engineering best practice (modularity, reviewability), or are there performance or technical reasons intrinsic to Lean's design that make smaller proofs better?

[Kim Morrison]

seb488 said:

a software engineering best practice (modularity, reviewability)

:point_up:

[Violeta Hernández]

There's a recent PR with 500 line proofs... shudders

[Kim Morrison]

Please review asking them to break out more lemmas! :-)

[Ruben Van de Velde]

I did, if Violeta was thinking of the same one