7.1. The Poisson inequality: an alternative proof by Phragmén–Lindelöf
The report proves the interior bound of Lemma 3.2 by mapping the strip conformally onto the upper
half-plane and applying the Poisson inequality to the subharmonic function \log|Z|; this is the
proof formalized in Lemma 4.1.18, on top of the subharmonic-function
library of the preliminaries chapter. The formalization also contains a second, independent proof
of the Poisson inequality for the strip, which stays inside the strip: the holomorphic Poisson
integral W of the boundary datum is built directly from the strip kernel, and a maximum-modulus
(Phragmén–Lindelöf) argument is applied to e^{-W}Z. It gives the principle for functions of
Phragmén–Lindelöf growth rather than only for bounded ones
(Lemma 7.1.2), and it re-derives the capped bound
of Lemma 3.2 (CohnElkies.norm_Z_g_le_exp_integral_of_cap_phragmenLindelof,
CohnElkies.exists_capped_poisson_majorization_phragmenLindelof, module
CohnElkies/LowerBound/PhragmenLindelofMajorization.lean); nothing else depends on it. Mathlib's
PhragmenLindelof.horizontal_strip cannot be applied directly, because it requires the function
itself, not only its modulus, to extend continuously to the closed strip (DiffContOnCl); only
\operatorname{Re}W, not W, extends continuously.
Let a < b, C > 0, and let f : \mathbb{C} \to \mathbb{C} be holomorphic on the open strip
\{a < \operatorname{Im}z < b\}. Suppose |f| has a continuous extension N \ge 0 to the
closed strip, that N \le C on the two boundary lines, and that
|f(z)| = O\bigl(\exp(B\exp(c|\operatorname{Re}z|))\bigr) in the strip as
|\operatorname{Re}z| \to \infty,
for some B and some c < \pi/(b-a). Then N \le C throughout the closed strip.
Lean code for Lemma7.1.1●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkiesForMathlib/Analysis/Complex/PhragmenLindelof.leancomplete
theorem PhragmenLindelof.horizontal_strip_norm_extension {a b C : ℝ} (hab : a < b) (hC : 0 < C) (f : ℂ → ℂ) (N : ℂ → ℝ) (hf : DifferentiableOn ℂ f (Complex.im ⁻¹' Set.Ioo a b)) (hN : ContinuousOn N (Complex.im ⁻¹' Set.Icc a b)) (hNnonneg : ∀ (w : ℂ), w.im ∈ Set.Icc a b → 0 ≤ N w) (hinterior : ∀ (w : ℂ), w.im ∈ Set.Ioo a b → N w = ‖f w‖) (hbottom : ∀ (w : ℂ), w.im = a → N w ≤ C) (htop : ∀ (w : ℂ), w.im = b → N w ≤ C) (hgrowth : ∃ c < Real.pi / (b - a), ∃ B, f =O[Filter.comap (fun w ↦ |w.re|) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun w ↦ Real.exp (B * Real.exp (c * |w.re|))) {z : ℂ} (hza : a ≤ z.im) (hzb : z.im ≤ b) : N z ≤ C
theorem PhragmenLindelof.horizontal_strip_norm_extension {a b C : ℝ} (hab : a < b) (hC : 0 < C) (f : ℂ → ℂ) (N : ℂ → ℝ) (hf : DifferentiableOn ℂ f (Complex.im ⁻¹' Set.Ioo a b)) (hN : ContinuousOn N (Complex.im ⁻¹' Set.Icc a b)) (hNnonneg : ∀ (w : ℂ), w.im ∈ Set.Icc a b → 0 ≤ N w) (hinterior : ∀ (w : ℂ), w.im ∈ Set.Ioo a b → N w = ‖f w‖) (hbottom : ∀ (w : ℂ), w.im = a → N w ≤ C) (htop : ∀ (w : ℂ), w.im = b → N w ≤ C) (hgrowth : ∃ c < Real.pi / (b - a), ∃ B, f =O[Filter.comap (fun w ↦ |w.re|) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun w ↦ Real.exp (B * Real.exp (c * |w.re|))) {z : ℂ} (hza : a ≤ z.im) (hzb : z.im ≤ b) : N z ≤ C
**Phragmén–Lindelöf principle** in a horizontal strip `{z | a < im z < b}` for a function whose *modulus* extends continuously to the closed strip. Let `f` be differentiable on the open strip and let `N` be continuous and nonnegative on the closed strip with `N = ‖f‖` on the open strip. Assume `N ≤ C` on the two boundary lines `im z = a` and `im z = b`, and that `f z = O(exp (B * exp (c * |re z|)))` as `|re z| → ∞` inside the strip, for some `c < π / (b - a)`. Then `N ≤ C` on the whole closed strip. This strengthens `PhragmenLindelof.horizontal_strip`, which requires `f` itself to be continuous on the closed strip (`DiffContOnCl`); here only `‖f‖` is assumed to extend. Proof: recenter the strip as `|im z - m| < r`, choose `c < q < π / (2r)` and, for `ε < 0`, damp `f` by `exp (ε (e^{q(z - mi)} + e^{-q(z - mi)}))`, whose modulus is at most `1` on the boundary lines and at most `exp (ε cos (qr) e^{q |re z|})` in the strip, so that the damped function is bounded by `C` on the vertical sides of a wide rectangle by the growth assumption; the maximum principle on that rectangle bounds the damped function at `z`, and `ε → 0⁻` concludes.
Standard Phragmén–Lindelöf argument on the strip: multiply by \exp(-\eta\cosh(c'(z - z_0)))-type
factors with c < c' < \pi/(b-a) to kill the growth, apply the maximum-modulus principle on large
rectangles, and let the auxiliary parameter tend to zero. The distinction between continuity of
f and continuity of its modulus matters: only the modulus is assumed to extend continuously,
so the maximum-modulus principle on the rectangles is applied to N rather than to f
(Complex.norm_extension_le_of_forall_mem_frontier_le).
(Poisson inequality for the strip, functions of Phragmén–Lindelöf growth.) Let \lambda > 0 and
let Z be holomorphic on the open strip \{|\operatorname{Im} t| < \lambda\}, continuous on
its closure, and of growth |Z(t)| \le C\exp(Ce^{c|\operatorname{Re} t|}) there for some
c < \pi/(2\lambda). Let b : \mathbb{R} \to \mathbb{R} be continuous with
|b(y)| \le A(1 + |y|), and suppose \log|Z(y - i\lambda)| \le b(y) and
\log|Z(y + i\lambda)| \le 0 for all y \in \mathbb{R}. Then for -1 < \sigma < 1 and
s \in \mathbb{R},
\log|Z(s + i\sigma\lambda)| \le \int_{\mathbb{R}}P_\sigma(T)\,b(s - \lambda T)\,dT,
with P_\sigma from Definition 4.1.8.
Lean code for Lemma7.1.2●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/PhragmenLindelofMajorization.leancomplete
theorem CohnElkies.norm_le_exp_integral_P_σ_of_strip_of_isBigO {ℓ : ℝ} (hℓ : 0 < ℓ) {Z : ℂ → ℂ} (hZ : DiffContOnCl ℂ Z (Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ)) (hgrowth : ∃ c < Real.pi / (2 * ℓ), ∃ B, Z =O[Filter.comap (fun z ↦ |z.re|) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ)] fun z ↦ Real.exp (B * Real.exp (c * |z.re|))) {b : ℝ → ℝ} (hb : Continuous b) {A : ℝ} (hA : 0 ≤ A) (hbound : ∀ (y : ℝ), |b y| ≤ A * (1 + |y|)) (hbottom : ∀ (y : ℝ), ‖Z (↑y - Complex.I * ↑ℓ)‖ ≤ Real.exp (b y)) (htop : ∀ (y : ℝ), ‖Z (↑y + Complex.I * ↑ℓ)‖ ≤ 1) {σ : ℝ} (hσbelow : -1 < σ) (hσabove : σ < 1) (s : ℝ) : ‖Z (↑s + Complex.I * (↑σ * ↑ℓ))‖ ≤ Real.exp (∫ (T : ℝ), CohnElkies.P_σ σ T * b (s - ℓ * T))
theorem CohnElkies.norm_le_exp_integral_P_σ_of_strip_of_isBigO {ℓ : ℝ} (hℓ : 0 < ℓ) {Z : ℂ → ℂ} (hZ : DiffContOnCl ℂ Z (Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ)) (hgrowth : ∃ c < Real.pi / (2 * ℓ), ∃ B, Z =O[Filter.comap (fun z ↦ |z.re|) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ)] fun z ↦ Real.exp (B * Real.exp (c * |z.re|))) {b : ℝ → ℝ} (hb : Continuous b) {A : ℝ} (hA : 0 ≤ A) (hbound : ∀ (y : ℝ), |b y| ≤ A * (1 + |y|)) (hbottom : ∀ (y : ℝ), ‖Z (↑y - Complex.I * ↑ℓ)‖ ≤ Real.exp (b y)) (htop : ∀ (y : ℝ), ‖Z (↑y + Complex.I * ↑ℓ)‖ ≤ 1) {σ : ℝ} (hσbelow : -1 < σ) (hσabove : σ < 1) (s : ℝ) : ‖Z (↑s + Complex.I * (↑σ * ↑ℓ))‖ ≤ Real.exp (∫ (T : ℝ), CohnElkies.P_σ σ T * b (s - ℓ * T))
**Poisson inequality for the strip** (report, proof of Lemma 3.2). Let `Z` be holomorphic on the open strip `|Im z| < ℓ` and continuous on its closure, with the Phragmén–Lindelöf growth `Z = O(exp (B e^{c |Re z|}))` as `|Re z| → ∞` in the strip for some `c < π/(2ℓ)`. Let `b` be a continuous profile with `|b y| ≤ A (1 + |y|)` such that `‖Z(y − iℓ)‖ ≤ e^{b(y)}` on the bottom edge and `‖Z(y + iℓ)‖ ≤ 1` on the top edge. Then at every interior point `s + iσℓ`, `-1 < σ < 1`, `‖Z(s + iσℓ)‖ ≤ exp (∫ P_σ(T) b(s − ℓT) dT)`, the exponential of the Poisson integral of `b`. Proof: Phragmén–Lindelöf (`PhragmenLindelof.horizontal_strip_norm_extension`) applied to `e^{-W[b]} Z`, where `W[b]` is the holomorphic Poisson integral of `b`: `Re W[b]` is the Poisson average of `b`, its extension to the closed strip is continuous with traces `b` (bottom) and `0` (top), so `e^{-W[b]} Z` has modulus at most `1` on both edges, and it keeps the growth of `Z` since `|Re W[b](z)| ≤ B (1 + |Re z|)`.
The lower-edge harmonic measure \lambda^{-1}P_\sigma((s-y)/\lambda)\,dy of
Lemma 4.1.16 is the real part of the holomorphic kernel
K_\lambda(z,y) = \frac{i}{4\lambda}\frac{E+1}{E-1}, E = e^{\pi(z-y+i\lambda)/(2\lambda)},
regularized to \widetilde K_\lambda(z,y) = K_\lambda(z,y) \pm i/(4\lambda) so that it decays like
e^{-\pi|y|/(2\lambda)} in y. Let W(z) = \int_{\mathbb{R}}\widetilde K_\lambda(z,y)\,b(y)\,dy.
Since |b(y)| \le A(1+|y|), W is holomorphic on the open strip (differentiation under the
integral sign), \operatorname{Re}W(s + i\sigma\lambda) = \int P_\sigma(T)\,b(s-\lambda T)\,dT, and
|\operatorname{Re}W(z)| \le B(1 + |\operatorname{Re}z|) because M_\sigma \le 1 and
\int P_\sigma(T)|T|\,dT is bounded uniformly in \sigma. By dominated convergence
(P_\sigma concentrates at T = 0 as \sigma \downarrow -1 and tends to 0 as
\sigma \uparrow 1), \operatorname{Re}W extends continuously to the closed strip with boundary
values b on the lower edge and 0 on the upper edge. Hence e^{-W}Z is holomorphic on the
open strip, its modulus e^{-\operatorname{Re}W}|Z| extends continuously to the closed strip with
values at most e^{-b(y)}|Z(y-i\lambda)| \le 1 on the lower edge and |Z(y+i\lambda)| \le 1 on
the upper edge, and it is O(\exp(B'e^{c'|\operatorname{Re}z|})) for some c' < \pi/(2\lambda).
The Phragmén–Lindelöf principle for the strip (Lemma 7.1.1) gives
e^{-\operatorname{Re}W}|Z| \le 1 inside, i.e.
\log|Z(s+i\sigma\lambda)| \le \operatorname{Re}W(s+i\sigma\lambda) = \int P_\sigma(T)\,b(s-\lambda T)\,dT.
(Capped Poisson majorization.) In the setting of Definition 4.1.2 there is
D_0 \in \mathbb{R} such that for every D \ge D_0, every -1 < \sigma < 1 and every
s \in \mathbb{R},
|Z(s + i\sigma\lambda)|
\le \exp\Bigl(\int_{\mathbb{R}}P_\sigma(T)\,h_{\lambda,D}(s - \lambda T)\,dT\Bigr),
where h_{\lambda,D}(y) = \min\{h_\lambda(y), D\} for y \ne 0 and h_{\lambda,D}(0) = D
(Definition 4.1.7, Definition 4.1.8). Letting
D \to \infty (dominated convergence) recovers the uncapped bound (18) of Lemma 4.1.22
(Definition 4.1.11).
Lean code for Lemma7.1.3●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CappedMajorization.leancomplete
theorem CohnElkies.norm_Z_g_le_exp_integral_of_cap {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R D : ℝ) (hcap : ∀ (y : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑y - Complex.I * (↑d / 2))‖ ≤ Real.exp (CohnElkies.h_ℓD (↑d / 2) R D y)) {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ Real.exp (∫ (T : ℝ), CohnElkies.P_σ σ T * CohnElkies.h_ℓD (↑d / 2) R D (s - ↑d / 2 * T))
theorem CohnElkies.norm_Z_g_le_exp_integral_of_cap {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R D : ℝ) (hcap : ∀ (y : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑y - Complex.I * (↑d / 2))‖ ≤ Real.exp (CohnElkies.h_ℓD (↑d / 2) R D y)) {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ Real.exp (∫ (T : ℝ), CohnElkies.P_σ σ T * CohnElkies.h_ℓD (↑d / 2) R D (s - ↑d / 2 * T))
Report Lemma 3.2: `|Z(s + iσλ)| ≤ exp(∫ P_σ(T) h_{λ,D}(s − λT) dT)`, the Poisson inequality `norm_le_exp_integral_P_σ_of_strip` for the bounded function `Z_g` on the strip `|Im z| < λ = d/2` with the capped profile `b = h_{λ,D}`, which is continuous and linearly bounded; the top-edge bound is (16).
The bottom boundary values of Z satisfy |Z(y - i\lambda)| \le e^{h_\lambda(y)} for y \ne 0
(Lemma 4.1.21) and Z is bounded on the closed strip
(Lemma 4.1.19), so for D \ge D_0 :=
\max\{0, \sup_y \log|Z(y - i\lambda)|\} also |Z(y - i\lambda)| \le e^{h_{\lambda,D}(y)} for all
y; the top boundary values satisfy |Z(y + i\lambda)| \le 1 (Lemma 4.1.20).
The capped majorant
h_{\lambda,D} is continuous with |h_{\lambda,D}(y)| \le A(1 + |y|) (it is -\lambda\log|y| +
O(1) at infinity). The Poisson inequality for the strip (Lemma 4.1.18)
gives the claim.