7.10. Subharmonic functions and the half-plane Poisson inequality🔗

The report's proof of Lemma 3.2 rests on the Poisson inequality for the upper half-plane, applied to the subharmonic function \log|Z \circ \Phi^{-1}|. Mathlib (as of the pinned version) has harmonic functions on inner product spaces (InnerProductSpace.HarmonicOnNhd, with the mean value property, Liouville's theorem, and the harmonicity of the real and imaginary parts and of \log|f| away from the zeros of a holomorphic f), the Poisson kernel and the Poisson formula for discs, Jensen's formula (AnalyticOnNhd.circleAverage_log_norm), the maximum modulus principle and the Phragmén–Lindelöf principles for strips, quadrants and half-planes, but no subharmonic functions, no Poisson integral of the half-plane, no harmonic measure and no boundary theory (Dirichlet problem, Fatou's theorem). The Mathlib-candidate modules CohnElkiesForMathlib/Analysis/Complex/Subharmonic/Defs.lean, CohnElkiesForMathlib/Analysis/Complex/Subharmonic/Basic.lean, CohnElkiesForMathlib/Analysis/Complex/PoissonHalfPlane.lean and CohnElkiesForMathlib/Analysis/Complex/Subharmonic/HalfPlane.lean add what the proof needs: subharmonic functions with values in [-\infty, \infty) (Definition 3.4.1), whose circle averages are handled through truncations because Mathlib's convention Real.log 0 = 0 makes the real-valued \log|f| unusable at zeros; the strong and weak maximum principles (Lemma 3.4.4); the subharmonicity of \log|f| from Jensen's formula (Lemma 3.4.3); the Poisson kernel and integral of the half-plane with harmonicity and boundary values (Definition 3.4.7, Lemma 3.4.9); the extended maximum principle with a finite exceptional set (Lemma 3.4.11); and the Poisson principle (Theorem 3.4.12). The conformal transfer to the strip and the harmonic-measure identity are Lemma 4.1.16 (module CohnElkies/LowerBound/StripToHalfPlane.lean), and the report's proof of the strip principle is Lemma 4.1.18 (module CohnElkies/LowerBound/CappedMajorization.lean).