4.1. The Mellin-strip obstruction
Fix 0 < c < 1/\pi, d \in \mathbb{N}, \lambda = d/2, R = c\sqrt d, and a nonzero
g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) with \widehat g = \varsigma g,
\varsigma \in \{-1,+1\}, and g(0) = 0. With S_d from Definition 3.3.1,
define in the logarithmic coordinate r = Re^v the normalized profile (equation (12))
\varphi(v) = \dfrac{S_d}{\|g\|_1}\,(Re^v)^d\,g(Re^v).
Lean code for Definition4.1.1●1 definition
Associated Lean declarations
-
CohnElkies.φ_g[complete]
-
CohnElkies.φ_g[complete]
-
defdefined in CohnElkies/LowerBound/LogProfile.leancomplete
def CohnElkies.φ_g {d : ℕ} (hd : 0 < d) (g : CohnElkies.TestFunction d) (R v : ℝ) : ℝ
def CohnElkies.φ_g {d : ℕ} (hd : 0 < d) (g : CohnElkies.TestFunction d) (R v : ℝ) : ℝ
The normalized logarithmic profile `φ(v) = (S_d/‖g‖₁) (R e^v)^d g(R e^v)` of report (12), in the logarithmic coordinate `r = R e^v`.
In the setting of Definition 4.1.1, with X_g from Definition 3.3.4, the
normalized Mellin transform is (equation (12))
Z(t) = \dfrac{S_d}{\|g\|_1}\,R^{\lambda+it}\,X_g(t)
(for complex t as well, through the Mellin transform of the profile, CohnElkies.X_f).
Lean code for Definition4.1.2●1 definition
Associated Lean declarations
-
CohnElkies.Z_g[complete]
-
CohnElkies.Z_g[complete]
-
defdefined in CohnElkies/LowerBound/MellinStrip.leancomplete
def CohnElkies.Z_g {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (R : ℝ) (z : ℂ) : ℂ
def CohnElkies.Z_g {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (R : ℝ) (z : ℂ) : ℂ
The normalized Mellin strip function `Z(z) = (S_d/‖g‖₁) R^{d/2 + iz} X_g(z)` of report (12).
In the setting of Definition 4.1.1 (equation (13)), \|\varphi\|_1 = 1.
Lean code for Lemma4.1.3●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LogProfile.leancomplete
theorem CohnElkies.RadialEigenfunction.integral_abs_logProfile {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) : ∫ (v : ℝ), |CohnElkies.φ_g hd g.toFun R v| = 1
theorem CohnElkies.RadialEigenfunction.integral_abs_logProfile {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) : ∫ (v : ℝ), |CohnElkies.φ_g hd g.toFun R v| = 1
Report (13): the profile `φ` of a radial eigenfunction has total variation `1`.
Polar integration (Lemma 3.3.2) with r = Re^v, dr = r\,dv, gives
\int|\varphi| = \frac{S_d}{\|g\|_1}\int_0^\infty |g(r)|r^{d-1}\,dr = 1.
In the setting of Definition 4.1.1 (equation (13)), \int_{\mathbb{R}}\varphi = 0.
Lean code for Lemma4.1.4●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LogProfile.leancomplete
theorem CohnElkies.RadialEigenfunction.integral_logProfile {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) : ∫ (v : ℝ), CohnElkies.φ_g hd g.toFun R v = 0
theorem CohnElkies.RadialEigenfunction.integral_logProfile {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) : ∫ (v : ℝ), CohnElkies.φ_g hd g.toFun R v = 0
Report (13): the profile `φ` of a radial eigenfunction has mean `0`.
As in Lemma 4.1.3, polar integration gives
\int\varphi = \widehat g(0)/\|g\|_1 = \varsigma g(0)/\|g\|_1 = 0.
In the setting of Definition 4.1.1 (equation (13)),
\int_{-\infty}^0|\varphi(v)|\,dv = \dfrac{1}{\|g\|_1}\int_{|x|<R}|g(x)|\,dx.
Lean code for Lemma4.1.5●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LogProfile.leancomplete
theorem CohnElkies.RadialEigenfunction.setIntegral_Iic_abs_logProfile {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) : ∫ (v : ℝ) in Set.Iic 0, |CohnElkies.φ_g hd g.toFun R v| = (∫ (x : CohnElkies.Euclidean d) in Metric.ball 0 R, ‖g.toFun x‖) / CohnElkies.L1norm g.toFun
theorem CohnElkies.RadialEigenfunction.setIntegral_Iic_abs_logProfile {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) : ∫ (v : ℝ) in Set.Iic 0, |CohnElkies.φ_g hd g.toFun R v| = (∫ (x : CohnElkies.Euclidean d) in Metric.ball 0 R, ‖g.toFun x‖) / CohnElkies.L1norm g.toFun
Report (13): `∫_{v ≤ 0} |φ| = ‖g‖₁⁻¹ ∫_{‖x‖ < R} |g|`.
The substitution r = Re^v of Lemma 4.1.3, where v < 0 corresponds to
r < R.
In the setting of Definition 4.1.2 (equation (13)),
Z(t) = \int_{\mathbb{R}}\varphi(v)e^{-(\lambda+it)v}\,dv for every complex t for which the
integral converges absolutely, in particular for real t: on the horizontal line
\operatorname{Im} t = \lambda - a of the strip, Z is the Fourier transform of the weighted
profile v \mapsto e^{-av}\varphi(v).
Lean code for Lemma4.1.6●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/MellinStrip.leancomplete
theorem CohnElkies.normalizedRadialMellinStrip_shifted_eq_fourier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hreal : CohnElkies.IsRealValued ⇑f) (R : ℝ) (hR : 0 < R) (a t : ℝ) : CohnElkies.Z_g hd f R (↑t + Complex.I * (↑d / 2 - ↑a)) = FourierTransform.fourier (fun v ↦ ↑(Real.exp (-a * v)) * ↑(CohnElkies.φ_g hd f R v)) (t / (2 * Real.pi))
theorem CohnElkies.normalizedRadialMellinStrip_shifted_eq_fourier {d : ℕ} (hd : 0 < d) (f : CohnElkies.TestFunction d) (hreal : CohnElkies.IsRealValued ⇑f) (R : ℝ) (hR : 0 < R) (a t : ℝ) : CohnElkies.Z_g hd f R (↑t + Complex.I * (↑d / 2 - ↑a)) = FourierTransform.fourier (fun v ↦ ↑(Real.exp (-a * v)) * ↑(CohnElkies.φ_g hd f R v)) (t / (2 * Real.pi))
Lemma 3.6 of the report: on the horizontal line `Im z = λ - a`, `Z` is the Fourier transform of the weighted profile `v ↦ e^{-a v} φ(v)`.
The substitution r = Re^v in X_g(t) = \int_0^\infty g(r)r^{\lambda-it-1}\,dr.
The strip estimates for the normalized Mellin transform Z (Lemmas 3.2–3.6 of the report).
The lower-boundary majorant is (equation (14)), for y \ne 0,
h_\lambda(y) = \lambda\log(\pi R^2) + \log|\Gamma(-iy/2)| - \log|\Gamma(\lambda + iy/2)|.
Lean code for Definition4.1.7●1 definition
Associated Lean declarations
-
CohnElkies.h_ℓ[complete]
-
CohnElkies.h_ℓ[complete]
-
defdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
def CohnElkies.h_ℓ (ℓ R y : ℝ) : ℝ
def CohnElkies.h_ℓ (ℓ R y : ℝ) : ℝ
The lower-boundary majorant `h_λ(y) = λ log(πR²) + log|Γ(-iy/2)| - log|Γ(λ + iy/2)|`; report (14).
For -1 < \sigma < 1 write \theta = \pi(1+\sigma)/2 \in (0,\pi) and define the strip Poisson
kernel (equation (15))
P_\sigma(T) = \dfrac{\sin\theta}{4(\cosh(\pi T/2) - \cos\theta)}.
Lean code for Definition4.1.8●2 definitions
Associated Lean declarations
-
CohnElkies.P_σ[complete]
-
CohnElkies.θ[complete]
-
CohnElkies.P_σ[complete] -
CohnElkies.θ[complete]
-
defdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
def CohnElkies.P_σ (σ T : ℝ) : ℝ
def CohnElkies.P_σ (σ T : ℝ) : ℝ
The strip Poisson kernel `P_σ(T) = sin θ / (4(cosh(πT/2) - cos θ))`; report (15).
-
defdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
def CohnElkies.θ (σ : ℝ) : ℝ
def CohnElkies.θ (σ : ℝ) : ℝ
The angle `θ = π(1 + σ)/2` attached to the height `σ` in the strip; report (15).
-
CohnElkies.stripPoissonKernel_pos[complete] -
CohnElkies.stripPoissonKernel_neg[complete] -
CohnElkies.stripPoissonKernel_antitone_abs[complete] -
CohnElkies.integral_stripPoissonKernel[complete] -
CohnElkies.stripPoissonKernel_le_mass_mul_exponential[complete]
For -1 < \sigma < 1 the kernel P_\sigma of Definition 4.1.8 is positive,
even and decreasing in |T|, and integrable with
\int_{\mathbb{R}}P_\sigma(T)\,dT = \dfrac{1-\sigma}{2}. For 0 \le \sigma < 1,
P_\sigma(T) \le \dfrac{1-\sigma}{2}\cdot\dfrac{\pi}{2}e^{-\pi|T|/2}; in particular
P_\sigma(T) \ll_\sigma e^{-\pi|T|/2}.
Lean code for Lemma4.1.9●5 theorems
Associated Lean declarations
-
CohnElkies.stripPoissonKernel_pos[complete]
-
CohnElkies.stripPoissonKernel_neg[complete]
-
CohnElkies.stripPoissonKernel_antitone_abs[complete]
-
CohnElkies.integral_stripPoissonKernel[complete]
-
CohnElkies.stripPoissonKernel_le_mass_mul_exponential[complete]
-
CohnElkies.stripPoissonKernel_pos[complete] -
CohnElkies.stripPoissonKernel_neg[complete] -
CohnElkies.stripPoissonKernel_antitone_abs[complete] -
CohnElkies.integral_stripPoissonKernel[complete] -
CohnElkies.stripPoissonKernel_le_mass_mul_exponential[complete]
-
theoremdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
theorem CohnElkies.stripPoissonKernel_pos {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) (T : ℝ) : 0 < CohnElkies.P_σ σ T
theorem CohnElkies.stripPoissonKernel_pos {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) (T : ℝ) : 0 < CohnElkies.P_σ σ T
-
theoremdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
theorem CohnElkies.stripPoissonKernel_neg (σ T : ℝ) : CohnElkies.P_σ σ (-T) = CohnElkies.P_σ σ T
theorem CohnElkies.stripPoissonKernel_neg (σ T : ℝ) : CohnElkies.P_σ σ (-T) = CohnElkies.P_σ σ T
-
theoremdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
theorem CohnElkies.stripPoissonKernel_antitone_abs {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) {x y : ℝ} (hxy : |x| ≤ |y|) : CohnElkies.P_σ σ y ≤ CohnElkies.P_σ σ x
theorem CohnElkies.stripPoissonKernel_antitone_abs {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) {x y : ℝ} (hxy : |x| ≤ |y|) : CohnElkies.P_σ σ y ≤ CohnElkies.P_σ σ x
-
theoremdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
theorem CohnElkies.integral_stripPoissonKernel {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) : ∫ (T : ℝ), CohnElkies.P_σ σ T = CohnElkies.M_σ σ
theorem CohnElkies.integral_stripPoissonKernel {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) : ∫ (T : ℝ), CohnElkies.P_σ σ T = CohnElkies.M_σ σ
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.stripPoissonKernel_le_mass_mul_exponential {σ : ℝ} (hzero : 0 ≤ σ) (habove : σ < 1) (T : ℝ) : CohnElkies.P_σ σ T ≤ CohnElkies.M_σ σ * CohnElkies.stripPoissonExponentialMajorant T
theorem CohnElkies.stripPoissonKernel_le_mass_mul_exponential {σ : ℝ} (hzero : 0 ≤ σ) (habove : σ < 1) (T : ℝ) : CohnElkies.P_σ σ T ≤ CohnElkies.M_σ σ * CohnElkies.stripPoissonExponentialMajorant T
\cosh(\pi T/2) \ge 1 > \cos\theta and \sin\theta > 0 give positivity; evenness and
monotonicity in |T| are those of \cosh. The primitive
Q_\sigma(T) = \pi^{-1}\arctan\bigl((e^{\pi T/2} - \cos\theta)/\sin\theta\bigr)
(CohnElkies.Q_σ) satisfies Q_\sigma' = P_\sigma, Q_\sigma(+\infty) = \tfrac12 and
Q_\sigma(-\infty) = \theta/\pi - \tfrac12, so \int P_\sigma = 1 - \theta/\pi = (1-\sigma)/2.
For \sigma \ge 0 one has \cos\theta \le 0, so \cosh(\pi T/2) - \cos\theta \ge \tfrac12e^{\pi|T|/2},
while \sin\theta = \sin(\pi(1-\sigma)/2) \le \pi(1-\sigma)/2.
The mass of the lower edge is (equation (15)) M_\sigma = \dfrac{1-\sigma}{2}, the total mass
\int_{\mathbb{R}}P_\sigma(T)\,dT of the kernel of Definition 4.1.8
(Lemma 4.1.9).
Lean code for Definition4.1.10●1 definition
Associated Lean declarations
-
CohnElkies.M_σ[complete]
-
CohnElkies.M_σ[complete]
-
defdefined in CohnElkies/LowerBound/PoissonKernel.leancomplete
def CohnElkies.M_σ (σ : ℝ) : ℝ
def CohnElkies.M_σ (σ : ℝ) : ℝ
The total mass `M_σ = (1 - σ)/2` of the kernel `P_σ`; report (15).
The Poisson majorant of the lower-boundary majorant h_\lambda of
Definition 4.1.7 is (equation (18))
H_\sigma(s) = \int_{\mathbb{R}}P_\sigma(T)\,h_\lambda(s - \lambda T)\,dT,
with P_\sigma from Definition 4.1.8.
Lean code for Definition4.1.11●1 definition
Associated Lean declarations
-
CohnElkies.H_σ[complete]
-
CohnElkies.H_σ[complete]
-
defdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
def CohnElkies.H_σ (ℓ R σ s : ℝ) : ℝ
def CohnElkies.H_σ (ℓ R σ s : ℝ) : ℝ
The Poisson extension `H_σ(s) = ∫ P_σ(T) h_λ(s - λT) dT` of the lower-boundary majorant; report (18).
-
CohnElkies.stripToHalfPlane[complete] -
CohnElkies.halfPlaneToStrip[complete]
Let \lambda > 0. The conformal map of the strip \{|\operatorname{Im} t| < \lambda\} onto the
upper half-plane \mathbb{H} is \Phi(t) = \exp(\pi(t + i\lambda)/(2\lambda)), with inverse
\Phi^{-1}(w) = (2\lambda/\pi)\log w - i\lambda (principal branch of the logarithm).
Lean code for Definition4.1.12●2 definitions
Associated Lean declarations
-
CohnElkies.stripToHalfPlane[complete]
-
CohnElkies.halfPlaneToStrip[complete]
-
CohnElkies.stripToHalfPlane[complete] -
CohnElkies.halfPlaneToStrip[complete]
-
defdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
def CohnElkies.stripToHalfPlane (ℓ : ℝ) (t : ℂ) : ℂ
def CohnElkies.stripToHalfPlane (ℓ : ℝ) (t : ℂ) : ℂ
The conformal map `t ↦ exp(π(t + iℓ)/(2ℓ))` of the strip `|Im t| < ℓ` onto the upper half-plane; it is `E_ℓ ℓ t 0`.
-
defdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
def CohnElkies.halfPlaneToStrip (ℓ : ℝ) (w : ℂ) : ℂ
def CohnElkies.halfPlaneToStrip (ℓ : ℝ) (w : ℂ) : ℂ
The inverse map `w ↦ (2ℓ/π) log w - iℓ` (principal branch of the logarithm) of the upper half-plane onto the strip `|Im t| < ℓ`.
-
CohnElkies.stripToHalfPlane_im_pos[complete] -
CohnElkies.halfPlaneToStrip_mem_strip[complete] -
CohnElkies.halfPlaneToStrip_stripToHalfPlane[complete] -
CohnElkies.stripToHalfPlane_ofReal_add_I_mul_mul[complete] -
CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_pos[complete] -
CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_neg[complete]
The map \Phi of Definition 4.1.12 sends the open strip into \mathbb{H},
\Phi^{-1} sends \mathbb{H} into the open strip, and \Phi^{-1} \circ \Phi is the identity
on the strip. The lower edge y - i\lambda goes to e^{\pi y/(2\lambda)} \in (0, \infty), the
upper edge y + i\lambda to -e^{\pi y/(2\lambda)} \in (-\infty, 0), and
t_0 = s + i\sigma\lambda to \rho e^{i\theta} with \rho = e^{\pi s/(2\lambda)} and
\theta = \pi(1 + \sigma)/2 the angle of Definition 4.1.8. The inverse
extends continuously to \mathbb{R} \setminus \{0\}: as w \to x within \mathbb{H},
\Phi^{-1}(w) \to (2\lambda/\pi)\log x - i\lambda for x > 0 and
\Phi^{-1}(w) \to (2\lambda/\pi)\log(-x) + i\lambda for x < 0.
Lean code for Lemma4.1.13●6 theorems
Associated Lean declarations
-
CohnElkies.stripToHalfPlane_im_pos[complete]
-
CohnElkies.halfPlaneToStrip_mem_strip[complete]
-
CohnElkies.halfPlaneToStrip_stripToHalfPlane[complete]
-
CohnElkies.stripToHalfPlane_ofReal_add_I_mul_mul[complete]
-
CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_pos[complete]
-
CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_neg[complete]
-
CohnElkies.stripToHalfPlane_im_pos[complete] -
CohnElkies.halfPlaneToStrip_mem_strip[complete] -
CohnElkies.halfPlaneToStrip_stripToHalfPlane[complete] -
CohnElkies.stripToHalfPlane_ofReal_add_I_mul_mul[complete] -
CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_pos[complete] -
CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_neg[complete]
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.stripToHalfPlane_im_pos {ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℂ} (ht : t ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ) : 0 < (CohnElkies.stripToHalfPlane ℓ t).im
theorem CohnElkies.stripToHalfPlane_im_pos {ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℂ} (ht : t ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ) : 0 < (CohnElkies.stripToHalfPlane ℓ t).im
The open strip `|Im t| < ℓ` is mapped into the upper half-plane.
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.halfPlaneToStrip_mem_strip {ℓ : ℝ} (hℓ : 0 < ℓ) {w : ℂ} (hw : 0 < w.im) : CohnElkies.halfPlaneToStrip ℓ w ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ
theorem CohnElkies.halfPlaneToStrip_mem_strip {ℓ : ℝ} (hℓ : 0 < ℓ) {w : ℂ} (hw : 0 < w.im) : CohnElkies.halfPlaneToStrip ℓ w ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ
The upper half-plane is mapped into the open strip `|Im t| < ℓ`.
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.halfPlaneToStrip_stripToHalfPlane {ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℂ} (ht : t ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ) : CohnElkies.halfPlaneToStrip ℓ (CohnElkies.stripToHalfPlane ℓ t) = t
theorem CohnElkies.halfPlaneToStrip_stripToHalfPlane {ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℂ} (ht : t ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ) : CohnElkies.halfPlaneToStrip ℓ (CohnElkies.stripToHalfPlane ℓ t) = t
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.stripToHalfPlane_ofReal_add_I_mul_mul {ℓ : ℝ} (hℓ : 0 < ℓ) (s σ : ℝ) : CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ)) = ↑(Real.exp (Real.pi * s / (2 * ℓ))) * Complex.exp (Complex.I * ↑(CohnElkies.θ σ))
theorem CohnElkies.stripToHalfPlane_ofReal_add_I_mul_mul {ℓ : ℝ} (hℓ : 0 < ℓ) (s σ : ℝ) : CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ)) = ↑(Real.exp (Real.pi * s / (2 * ℓ))) * Complex.exp (Complex.I * ↑(CohnElkies.θ σ))
The point `t₀ = s + iσℓ` of the strip is sent to `e^{πs/(2ℓ)} e^{iθ}` with `θ = θ σ` the angle `π(1 + σ)/2` of (15). -
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_pos (ℓ : ℝ) {x : ℝ} (hx : 0 < x) : Filter.Tendsto (CohnElkies.halfPlaneToStrip ℓ) (nhdsWithin ↑x {w | 0 < w.im}) (nhds (↑(2 * ℓ / Real.pi * Real.log x) - Complex.I * ↑ℓ))
theorem CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_pos (ℓ : ℝ) {x : ℝ} (hx : 0 < x) : Filter.Tendsto (CohnElkies.halfPlaneToStrip ℓ) (nhdsWithin ↑x {w | 0 < w.im}) (nhds (↑(2 * ℓ / Real.pi * Real.log x) - Complex.I * ↑ℓ))
Continuity of the inverse map up to the positive real axis: as `w → x > 0` in the half-plane, `halfPlaneToStrip ℓ w → (2ℓ/π) log x - iℓ`, a point of the lower edge.
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_neg (ℓ : ℝ) {x : ℝ} (hx : x < 0) : Filter.Tendsto (CohnElkies.halfPlaneToStrip ℓ) (nhdsWithin ↑x {w | 0 < w.im}) (nhds (↑(2 * ℓ / Real.pi * Real.log (-x)) + Complex.I * ↑ℓ))
theorem CohnElkies.tendsto_halfPlaneToStrip_ofReal_of_neg (ℓ : ℝ) {x : ℝ} (hx : x < 0) : Filter.Tendsto (CohnElkies.halfPlaneToStrip ℓ) (nhdsWithin ↑x {w | 0 < w.im}) (nhds (↑(2 * ℓ / Real.pi * Real.log (-x)) + Complex.I * ↑ℓ))
Continuity of the inverse map up to the negative real axis: as `w → x < 0` in the half-plane, `halfPlaneToStrip ℓ w → (2ℓ/π) log (-x) + iℓ`, a point of the upper edge (the principal logarithm satisfies `log x = log |x| + iπ` on the negative axis, approached from above).
\operatorname{Im}\Phi(t) = e^{\pi\operatorname{Re}t/(2\lambda)}\sin\bigl(\pi(\operatorname{Im}t + \lambda)/(2\lambda)\bigr) > 0
for |\operatorname{Im} t| < \lambda, and
\operatorname{Im}\Phi^{-1}(w) = (2\lambda/\pi)\arg w - \lambda \in (-\lambda, \lambda) for
\arg w \in (0, \pi). The boundary correspondence is read off from
\exp(\pi(y \mp i\lambda + i\lambda)/(2\lambda)) and e^{i\pi} = -1, and \Phi^{-1} is
continuous on \mathbb{H} \cup (\mathbb{R} \setminus \{0\}) because the principal logarithm is
continuous on the slit plane and, on the negative axis approached from above, tends to
\log|x| + i\pi.
For a lower-edge datum b : \mathbb{R} \to \mathbb{R} of the strip, the transferred datum on
\mathbb{R} = \partial\mathbb{H} is \tilde b(x) = b((2\lambda/\pi)\log x) for x > 0, the
image of the lower edge under \Phi of Definition 4.1.12, and
\tilde b(x) = 0 for x \le 0, the image of the upper edge.
Lean code for Definition4.1.14●1 definition
Associated Lean declarations
-
CohnElkies.halfPlaneDatum[complete]
-
CohnElkies.halfPlaneDatum[complete]
-
defdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
def CohnElkies.halfPlaneDatum (ℓ : ℝ) (b : ℝ → ℝ) (x : ℝ) : ℝ
def CohnElkies.halfPlaneDatum (ℓ : ℝ) (b : ℝ → ℝ) (x : ℝ) : ℝ
The boundary datum on the real axis corresponding to a lower-edge datum `b` of the strip: `x ↦ b((2ℓ/π) log x)` on `(0, ∞)`, the image of the lower edge, and `0` on `(-∞, 0]`, the image of the upper edge.
If b is continuous with |b(y)| \le A(1 + |y|), then \tilde b of
Definition 4.1.14 is continuous on \mathbb{R} \setminus \{0\} and
\tilde b(x)/(1 + x^2) is integrable: \tilde b is an admissible boundary datum for the
Poisson integral of Definition 3.4.7.
Lean code for Lemma4.1.15●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.halfPlaneDatum_continuousAt {ℓ : ℝ} {b : ℝ → ℝ} (hb : Continuous b) {x : ℝ} (hx : x ≠ 0) : ContinuousAt (CohnElkies.halfPlaneDatum ℓ b) x
theorem CohnElkies.halfPlaneDatum_continuousAt {ℓ : ℝ} {b : ℝ → ℝ} (hb : Continuous b) {x : ℝ} (hx : x ≠ 0) : ContinuousAt (CohnElkies.halfPlaneDatum ℓ b) x
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.integrable_halfPlaneDatum_div_one_add_sq {ℓ : ℝ} (hℓ : 0 < ℓ) {b : ℝ → ℝ} (hb : Continuous b) {A : ℝ} (hbound : ∀ (y : ℝ), |b y| ≤ A * (1 + |y|)) : MeasureTheory.Integrable (fun x ↦ CohnElkies.halfPlaneDatum ℓ b x / (1 + x ^ 2)) MeasureTheory.volume
theorem CohnElkies.integrable_halfPlaneDatum_div_one_add_sq {ℓ : ℝ} (hℓ : 0 < ℓ) {b : ℝ → ℝ} (hb : Continuous b) {A : ℝ} (hbound : ∀ (y : ℝ), |b y| ≤ A * (1 + |y|)) : MeasureTheory.Integrable (fun x ↦ CohnElkies.halfPlaneDatum ℓ b x / (1 + x ^ 2)) MeasureTheory.volume
The half-plane datum of a continuous, linearly bounded `b` is a Poisson-integrable datum: `halfPlaneDatum ℓ b x / (1 + x²)` is integrable on `ℝ`. Under `x = e^{u}` the integrand on `(0, ∞)` becomes `e^{u} b((2ℓ/π) u) / (1 + e^{2u})`, dominated by `A (1 + (2ℓ/π)|u|) e^{-|u|}`.
Continuity off 0 is clear. Under x = e^{u}, \tilde b(x)/(1 + x^2) on (0, \infty)
becomes e^{u}b((2\lambda/\pi)u)/(1 + e^{2u}), which is dominated by
A(1 + (2\lambda/\pi)|u|)e^{-|u|}.
(Harmonic measure of the strip.) With \Phi from Definition 4.1.12, \tilde b
from Definition 4.1.14, P_\sigma from Definition 4.1.8 and the
Poisson integral P[\,\cdot\,] of Definition 3.4.7, for
-1 < \sigma < 1 and s \in \mathbb{R},
P[\tilde b](\Phi(s + i\sigma\lambda)) = \int_{\mathbb{R}}\lambda^{-1}P_\sigma\Bigl(\dfrac{s - y}{\lambda}\Bigr)b(y)\,dy = \int_{\mathbb{R}}P_\sigma(T)\,b(s - \lambda T)\,dT:
\lambda^{-1}P_\sigma((s - y)/\lambda)\,dy is the harmonic measure of the lower edge at
s + i\sigma\lambda.
Lean code for Lemma4.1.16●3 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.poissonIntegralHalfPlane_halfPlaneDatum {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) (b : ℝ → ℝ) : Complex.poissonIntegralHalfPlane (CohnElkies.halfPlaneDatum ℓ b) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = ∫ (T : ℝ), CohnElkies.P_σ σ T * b (s - ℓ * T)
theorem CohnElkies.poissonIntegralHalfPlane_halfPlaneDatum {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) (b : ℝ → ℝ) : Complex.poissonIntegralHalfPlane (CohnElkies.halfPlaneDatum ℓ b) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = ∫ (T : ℝ), CohnElkies.P_σ σ T * b (s - ℓ * T)
**The harmonic measure identity of the report** (proof of Lemma 3.2): the half-plane Poisson integral of the transferred datum at the image of `t₀ = s + iσℓ` is the strip Poisson integral `∫ P_σ(T) b(s - ℓT) dT` of (16).
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.poissonKernelHalfPlane_stripToHalfPlane_mul {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s y : ℝ) : (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))).poissonKernelHalfPlane (Real.exp (Real.pi / (2 * ℓ) * y)) * (Real.pi / (2 * ℓ) * Real.exp (Real.pi / (2 * ℓ) * y)) = CohnElkies.P_σ σ ((s - y) / ℓ) / ℓ
theorem CohnElkies.poissonKernelHalfPlane_stripToHalfPlane_mul {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s y : ℝ) : (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))).poissonKernelHalfPlane (Real.exp (Real.pi / (2 * ℓ) * y)) * (Real.pi / (2 * ℓ) * Real.exp (Real.pi / (2 * ℓ) * y)) = CohnElkies.P_σ σ ((s - y) / ℓ) / ℓ
Under `x = e^{πy/(2ℓ)}` the half-plane Poisson kernel at the image of `t₀ = s + iσℓ`, times the Jacobian `dx/dy = (π/(2ℓ)) x`, is the strip kernel `ℓ⁻¹ P_σ((s - y)/ℓ)` of (15). -
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.poissonIntegralHalfPlane_halfPlaneDatum_eq_integral_P_σ {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) (b : ℝ → ℝ) : Complex.poissonIntegralHalfPlane (CohnElkies.halfPlaneDatum ℓ b) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = ∫ (y : ℝ), CohnElkies.P_σ σ ((s - y) / ℓ) / ℓ * b y
theorem CohnElkies.poissonIntegralHalfPlane_halfPlaneDatum_eq_integral_P_σ {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) (b : ℝ → ℝ) : Complex.poissonIntegralHalfPlane (CohnElkies.halfPlaneDatum ℓ b) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = ∫ (y : ℝ), CohnElkies.P_σ σ ((s - y) / ℓ) / ℓ * b y
The half-plane Poisson formula at `t₀ = s + iσℓ`, pulled back to the lower edge by `x = e^{πy/(2ℓ)}`: the lower-edge harmonic measure of the strip is `ℓ⁻¹ P_σ((s - y)/ℓ) dy` (report, proof of Lemma 3.2).
On (0, \infty) substitute x = e^{\pi y/(2\lambda)}, dx = (\pi/(2\lambda))\,x\,dy: the
half-plane kernel at \rho e^{i\theta} = \Phi(s + i\sigma\lambda)
(Lemma 4.1.13) satisfies
\dfrac{1}{\pi}\dfrac{\rho\sin\theta}{(x - \rho\cos\theta)^2 + \rho^2\sin^2\theta}\cdot\dfrac{\pi x}{2\lambda} = \dfrac{\sin\theta}{4\lambda\bigl(\tfrac12(\rho/x + x/\rho) - \cos\theta\bigr)} = \dfrac{1}{\lambda}P_\sigma\Bigl(\dfrac{s - y}{\lambda}\Bigr),
since (x - \rho\cos\theta)^2 + \rho^2\sin^2\theta = \rho x\,(x/\rho + \rho/x - 2\cos\theta) and
\tfrac12(\rho/x + x/\rho) = \cosh(\pi(s - y)/(2\lambda)); the substitution
T = (s - y)/\lambda gives the second form.
The harmonic measure of the lower edge at s + i\sigma\lambda
(Lemma 4.1.16) has total mass M_\sigma = (1 - \sigma)/2
(Definition 4.1.10), and the upper edge has harmonic measure (1 + \sigma)/2.
Lean code for Lemma4.1.17●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.poissonIntegralHalfPlane_halfPlaneDatum_one {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : Complex.poissonIntegralHalfPlane (CohnElkies.halfPlaneDatum ℓ fun x ↦ 1) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = CohnElkies.M_σ σ
theorem CohnElkies.poissonIntegralHalfPlane_halfPlaneDatum_one {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : Complex.poissonIntegralHalfPlane (CohnElkies.halfPlaneDatum ℓ fun x ↦ 1) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = CohnElkies.M_σ σ
The lower-edge harmonic measure has total mass `M_σ = (1 - σ)/2` (datum `b = 1`).
-
theoremdefined in CohnElkies/LowerBound/StripToHalfPlane.leancomplete
theorem CohnElkies.poissonIntegralHalfPlane_indicator_Iic {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : Complex.poissonIntegralHalfPlane (fun x ↦ if x ≤ 0 then 1 else 0) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = (1 + σ) / 2
theorem CohnElkies.poissonIntegralHalfPlane_indicator_Iic {ℓ σ : ℝ} (hℓ : 0 < ℓ) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : Complex.poissonIntegralHalfPlane (fun x ↦ if x ≤ 0 then 1 else 0) (CohnElkies.stripToHalfPlane ℓ (↑s + Complex.I * (↑σ * ↑ℓ))) = (1 + σ) / 2
The complementary upper-edge harmonic measure has mass `(1 + σ)/2`: the Poisson integral of the indicator of `(-∞, 0]`, the image of the upper edge, at the image of `t₀ = s + iσℓ`.
The datum b = 1 in Lemma 4.1.16 gives
\int P_\sigma = M_\sigma (Lemma 4.1.9), and the
complementary mass of (-\infty, 0] is 1 - M_\sigma = (1 + \sigma)/2 since the half-plane
kernel has total mass 1.
(Poisson inequality for the strip.) Let \lambda > 0 and let Z be holomorphic and bounded on
the open strip \{|\operatorname{Im} t| < \lambda\} and continuous on its closure. 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 Lemma4.1.18●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CappedMajorization.leancomplete
theorem CohnElkies.norm_le_exp_integral_P_σ_of_strip {ℓ : ℝ} (hℓ : 0 < ℓ) {Z : ℂ → ℂ} (hZ : DiffContOnCl ℂ Z (Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ)) {K : ℝ} (hK : ∀ z ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ, ‖Z z‖ ≤ K) {b : ℝ → ℝ} (hb : Continuous b) {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 {ℓ : ℝ} (hℓ : 0 < ℓ) {Z : ℂ → ℂ} (hZ : DiffContOnCl ℂ Z (Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ)) {K : ℝ} (hK : ∀ z ∈ Complex.im ⁻¹' Set.Ioo (-ℓ) ℓ, ‖Z z‖ ≤ K) {b : ℝ → ℝ} (hb : Continuous b) {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))
**The Poisson inequality for the strip** (the report's proof of Lemma 3.2, through the upper half-plane). Let `Z` be holomorphic and bounded on the open strip `|Im z| < ℓ` and continuous on its closure, let `b` be continuous with `|b y| ≤ A (1 + |y|)`, and assume `‖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: `F = Z ∘ Φ⁻¹` is analytic and bounded on `ℍ`, where `Φ⁻¹(w) = (2ℓ/π) log w − iℓ`. As `w → x` within `ℍ`, `F w → Z((2ℓ/π) log x − iℓ)` for `x > 0` and `F w → Z((2ℓ/π) log(−x) + iℓ)` for `x < 0`, so `limsup log ‖F‖ ≤ b((2ℓ/π) log x)` on `(0, ∞)` and `≤ 0` on `(−∞, 0)`: this is the datum `halfPlaneDatum ℓ b`, continuous off `0`. The Poisson inequality for the half-plane, with the exceptional point `0`, gives `‖F‖ ≤ exp P[halfPlaneDatum ℓ b]` on `ℍ`, and at `w = Φ(s + iσℓ)` the Poisson integral is `∫ P_σ(T) b(s − ℓT) dT` (`poissonIntegralHalfPlane_halfPlaneDatum`).
Let \Phi and \tilde b be as in Definition 4.1.12 and
Definition 4.1.14. The function F = Z \circ \Phi^{-1} is holomorphic and bounded
on \mathbb{H} (Lemma 4.1.13), so \log|F| is subharmonic and bounded
above (Lemma 3.4.3). As w \to x within \mathbb{H},
F(w) \to Z((2\lambda/\pi)\log x - i\lambda) for x > 0 and
F(w) \to Z((2\lambda/\pi)\log(-x) + i\lambda) for x < 0, by the continuity of \Phi^{-1}
up to \mathbb{R} \setminus \{0\} and of Z on the closed strip; hence \limsup_{w \to x}\log|F(w)| \le \tilde b(x) for every x \ne 0, the
lower-edge bound giving \tilde b(x) = b((2\lambda/\pi)\log x) on (0, \infty) and the
upper-edge bound giving 0 on (-\infty, 0). The datum \tilde b is continuous off 0 with
\tilde b(x)/(1 + x^2) integrable (Lemma 4.1.15), so the Poisson
principle for the upper half-plane
(Corollary 3.4.13, with the exceptional set E = \{0\}) gives
\log|F| \le P[\tilde b] on \mathbb{H}. At w = \Phi(s + i\sigma\lambda) this reads
\log|Z(s + i\sigma\lambda)| \le P[\tilde b](\Phi(s + i\sigma\lambda)) = \int_{\mathbb{R}}P_\sigma(T)\,b(s - \lambda T)\,dT
by Lemma 4.1.16.
In the setting of Definition 4.1.2, the function Z is holomorphic on a
neighbourhood of the strip |\operatorname{Im} t| \le \lambda (in particular holomorphic on
the open strip and continuous on its closure), and it is bounded on the closed strip.
Lean code for Lemma4.1.19●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
theorem CohnElkies.RadialEigenfunction.diffContOnCl_Z_g {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R : ℝ) : DiffContOnCl ℂ (CohnElkies.Z_g hd g.toFun R) (Complex.im ⁻¹' Set.Ioo (-(↑d / 2)) (↑d / 2))
theorem CohnElkies.RadialEigenfunction.diffContOnCl_Z_g {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R : ℝ) : DiffContOnCl ℂ (CohnElkies.Z_g hd g.toFun R) (Complex.im ⁻¹' Set.Ioo (-(↑d / 2)) (↑d / 2))
-
theoremdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
theorem CohnElkies.RadialEigenfunction.exists_norm_Z_g_le {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R : ℝ) : ∃ C, 0 ≤ C ∧ ∀ (z : ℂ), -(↑d / 2) ≤ z.im → z.im ≤ ↑d / 2 → ‖CohnElkies.Z_g hd g.toFun R z‖ ≤ C
theorem CohnElkies.RadialEigenfunction.exists_norm_Z_g_le {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R : ℝ) : ∃ C, 0 ≤ C ∧ ∀ (z : ℂ), -(↑d / 2) ≤ z.im → z.im ≤ ↑d / 2 → ‖CohnElkies.Z_g hd g.toFun R z‖ ≤ C
Holomorphy. Since g(0) = \widehat g(0) = 0, Lemma 3.3.12 shows that
M_g is holomorphic on \operatorname{Re} z > -2; as Z(t) is a multiple of
R^{it}M_g(\lambda - it) and \operatorname{Re}(\lambda - it) = \lambda + \operatorname{Im} t,
Z is holomorphic on \operatorname{Im} t > -\lambda - 2, a neighbourhood of the closed strip.
Boundedness. For -\lambda \le \eta \le \lambda, (12) gives
|Z(s+i\eta)| \le \frac{S_dR^{\lambda-\eta}}{\|g\|_1}\int_0^\infty|g(r)|r^{\lambda+\eta-1}\,dr.
Splitting at r = 1, using |g(r)| \le Cr^2 near 0 (so the integrand is at most
Cr^{\lambda+\eta+1} \le C on (0,1]) and the Schwartz decay of g on [1,\infty), bounds
the right-hand side uniformly in s and \eta. In particular
\sup_y|Z(y - i\lambda)| \le \frac{S_dR^d}{\|g\|_1}\int_0^\infty\frac{|g(r)|}{r}\,dr < \infty.
In the setting of Definition 4.1.2, |Z(y + i\lambda)| \le 1 for all real
y (equation (16)).
Lean code for Lemma4.1.20●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
theorem CohnElkies.RadialEigenfunction.norm_Z_g_top_le_one {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R y : ℝ) : ‖CohnElkies.Z_g hd g.toFun R (↑y + Complex.I * (↑d / 2))‖ ≤ 1
theorem CohnElkies.RadialEigenfunction.norm_Z_g_top_le_one {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) (R y : ℝ) : ‖CohnElkies.Z_g hd g.toFun R (↑y + Complex.I * (↑d / 2))‖ ≤ 1
Report (16): `|Z(y + iλ)| ≤ 1` on the top edge of the strip.
By Lemma 4.1.6 with t = y + i\lambda,
Z(y+i\lambda) = \int\varphi(v)e^{-iyv}\,dv, so |Z(y+i\lambda)| \le \|\varphi\|_1 = 1 by
Lemma 4.1.3.
In the setting of Definition 4.1.2, \log|Z(y - i\lambda)| \le h_\lambda(y)
for y \ne 0, with h_\lambda from Definition 4.1.7 (equation (17)).
Lean code for Lemma4.1.21●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
theorem CohnElkies.RadialEigenfunction.norm_Z_g_bottom_le_exp_h_ℓ {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) (y : ℝ) (hy : y ≠ 0) : ‖CohnElkies.Z_g hd g.toFun R (↑y - Complex.I * (↑d / 2))‖ ≤ Real.exp (CohnElkies.h_ℓ (↑d / 2) R y)
theorem CohnElkies.RadialEigenfunction.norm_Z_g_bottom_le_exp_h_ℓ {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) (y : ℝ) (hy : y ≠ 0) : ‖CohnElkies.Z_g hd g.toFun R (↑y - Complex.I * (↑d / 2))‖ ≤ Real.exp (CohnElkies.h_ℓ (↑d / 2) R y)
Lemma 3.2 of the report: `log |Z(y - iλ)| ≤ h_λ(y)` on the bottom edge of the strip.
Evaluating (9), continued to \operatorname{Re} z = 0 by
Lemma 3.3.12, at z = -iy and using \widehat g = \varsigma g gives
X_g(y - i\lambda)
= \varsigma\pi^{\lambda+iy}\frac{\Gamma(-iy/2)}{\Gamma(\lambda+iy/2)}X_g(-y+i\lambda),
hence
Z(y - i\lambda)
= \varsigma(\pi R^2)^{\lambda+iy}\frac{\Gamma(-iy/2)}{\Gamma(\lambda + iy/2)}Z(-y + i\lambda).
Taking absolute values and using (16) (Lemma 4.1.20) gives
\log|Z(y - i\lambda)| \le h_\lambda(y) for y \ne 0, independently of \varsigma. At
y = 0 the zero Z(i\lambda) = \int\varphi = 0 (Lemma 4.1.4) cancels the gamma
pole in (17), so Z(-i\lambda) is finite, although h_\lambda(y) = -\log|y| + O_\lambda(1) as
y \to 0.
In the setting of Definition 4.1.2, for every -1 < \sigma < 1 and every
s \in \mathbb{R}, with P_\sigma from Definition 4.1.8 and H_\sigma
from Definition 4.1.11 (equation (18)),
|Z(s + i\sigma\lambda)| \le \exp(H_\sigma(s))
= \exp\Bigl(\int_{\mathbb{R}}P_\sigma(T)h_\lambda(s-\lambda T)\,dT\Bigr).
Lean code for Lemma4.1.22●1 theorem
Associated Lean declarations
-
CohnElkies.norm_Z_g_le_exp_H_σ[complete]
-
CohnElkies.norm_Z_g_le_exp_H_σ[complete]
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.norm_Z_g_le_exp_H_σ {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) {σ : ℝ} (hσbelow : -1 < σ) (hσabove : σ < 1) (s : ℝ) : ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ Real.exp (CohnElkies.H_σ (↑d / 2) R σ s)
theorem CohnElkies.norm_Z_g_le_exp_H_σ {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ} (hR : 0 < R) {σ : ℝ} (hσbelow : -1 < σ) (hσabove : σ < 1) (s : ℝ) : ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ Real.exp (CohnElkies.H_σ (↑d / 2) R σ s)
Report Lemma 3.2 with (18): `|Z(s + iσλ)| ≤ exp H_σ(s)` on every interior line of the strip, by letting the cap `D → ∞` in `exists_capped_poisson_majorization`.
Z is bounded and holomorphic on the strip and continuous on its closure
(Lemma 4.1.19), with the boundary bounds (16) and (17) of
Lemma 4.1.20 and Lemma 4.1.21. The logarithmic singularity
of h_\lambda requires a bounded truncation. Choose
D > \max\{0, \sup_y\log|Z(y - i\lambda)|\} and let h_{\lambda,D} = \min\{h_\lambda, D\}
(with value D at 0), a continuous function of logarithmic growth. The Poisson inequality
(Lemma 4.1.18) applied to the bounded function Z with lower majorant
h_{\lambda,D} and upper majorant 0 gives the capped bound
\log|Z(s+i\sigma\lambda)| \le \int P_\sigma(T)h_{\lambda,D}(s-\lambda T)\,dT
(Lemma 7.1.3). The integral H_\sigma(s) converges absolutely, because
P_\sigma decays exponentially (Lemma 4.1.9), the
singularity of h_\lambda at 0 is locally integrable, and
h_\lambda(y) = -\lambda\log|y| + O_\lambda(1) as |y| \to \infty by Stirling's formula. Since
h_{\lambda,D} \le h_\lambda and P_\sigma \ge 0, the capped majorant is at most
H_\sigma(s); equivalently, dominated convergence lets D \to \infty
(CohnElkies.lowerStripCappedPoisson_tendsto). This proves (18).
Let f : \mathbb{R} \to [0,\infty) be integrable, compactly supported, even, and nonincreasing on
[0,\infty), and let -1 < \sigma < 1. Then (f * P_\sigma)(x) \le (f * P_\sigma)(0) for every
x \in \mathbb{R}, with P_\sigma from Definition 4.1.8 (which is
positive, even and nonincreasing on [0,\infty)).
Lean code for Lemma4.1.23●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.even_antitone_poisson_convolution_max {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) {f : ℝ → ℝ} {B : ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hfmeas : Measurable f) (hfnonneg : ∀ (x : ℝ), 0 ≤ f x) (heven : ∀ (x : ℝ), f (-x) = f x) (hanti : AntitoneOn f (Set.Ici 0)) (hsupport : Function.support f ⊆ Set.Icc (-B) B) (s : ℝ) : ∫ (x : ℝ), CohnElkies.P_σ σ (s - x) * f x ≤ ∫ (x : ℝ), CohnElkies.P_σ σ (0 - x) * f x
theorem CohnElkies.even_antitone_poisson_convolution_max {σ : ℝ} (hbelow : -1 < σ) (habove : σ < 1) {f : ℝ → ℝ} {B : ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hfmeas : Measurable f) (hfnonneg : ∀ (x : ℝ), 0 ≤ f x) (heven : ∀ (x : ℝ), f (-x) = f x) (hanti : AntitoneOn f (Set.Ici 0)) (hsupport : Function.support f ⊆ Set.Icc (-B) B) (s : ℝ) : ∫ (x : ℝ), CohnElkies.P_σ σ (s - x) * f x ≤ ∫ (x : ℝ), CohnElkies.P_σ σ (0 - x) * f x
An even, nonnegative, compactly supported weight that is antitone on `[0, ∞)` has its Poisson convolution maximal at the centre.
Layer-cake: f(x) = \int_0^\infty \mathbf 1_{\{f > \alpha\}}(x)\,d\alpha and similarly for q,
where, up to endpoints, \{f > \alpha\} = (-r_\alpha, r_\alpha) and
\{q > \beta\} = (-R_\beta, R_\beta) (CohnElkies.even_antitone_superlevel_interval). By
Tonelli, (f*q)(x) is the double integral over \alpha, \beta of the length of
(-R_\beta,R_\beta) \cap (x - r_\alpha, x + r_\alpha), and the length of the intersection of two
centred intervals, one translated by x, is largest at x = 0.
-
CohnElkies.f_T[complete] -
CohnElkies.lowerPoissonEndpointExpectation[complete]
Put f_T(x) = \log\sqrt{x^2 + T^2/4} and
J_\sigma = -\dfrac{1}{M_\sigma}\int_{\mathbb{R}}P_\sigma(T)\int_0^1 f_T(x)\,dx\,dT,
with P_\sigma, M_\sigma from Definition 4.1.8 and
Definition 4.1.10. The formalization uses instead
J^{\mathrm{Lean}}_\sigma = J_\sigma - 1 = \dfrac{1}{M_\sigma}\int_{\mathbb{R}}P_\sigma(T)\Lambda(T)\,dT,
the expectation against P_\sigma/M_\sigma of the endpoint phase
\Lambda(T) = -\int_0^1 f_T(x)\,dx - 1 of Lemma 7.2.3, so that
\log(2\pi c^2) + J_\sigma = \log(2\pi ec^2) + J^{\mathrm{Lean}}_\sigma.
Lean code for Definition4.1.24●2 definitions
Associated Lean declarations
-
CohnElkies.f_T[complete]
-
CohnElkies.lowerPoissonEndpointExpectation[complete]
-
CohnElkies.f_T[complete] -
CohnElkies.lowerPoissonEndpointExpectation[complete]
-
defdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
def CohnElkies.f_T (T x : ℝ) : ℝ
def CohnElkies.f_T (T x : ℝ) : ℝ
`f_T T x = log √(x² + T²/4)`, the integrand of the Riemann sum of report Lemma 3.3.
-
defdefined in CohnElkies/LowerBound/LimitingDensity.leancomplete
def CohnElkies.lowerPoissonEndpointExpectation (σ : ℝ) : ℝ
def CohnElkies.lowerPoissonEndpointExpectation (σ : ℝ) : ℝ
`J_σ`, the expectation of the endpoint phase against `P_σ / M_σ`; report Lemma 3.3.
In the setting of Definition 4.1.2 with d \ge 2, for every -1 < \sigma < 1
and every s \in \mathbb{R}, H_\sigma(s) \le H_\sigma(0), with H_\sigma from
Definition 4.1.11 and h_\lambda from Definition 4.1.7.
Lean code for Lemma4.1.25●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.lowerStripPoissonMajorant_dimension_centered_max {d : ℕ} (hd : 2 ≤ d) {c σ : ℝ} (hc : 0 < c) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : CohnElkies.H_σ (↑d / 2) (c * √↑d) σ s ≤ CohnElkies.H_σ (↑d / 2) (c * √↑d) σ 0
theorem CohnElkies.lowerStripPoissonMajorant_dimension_centered_max {d : ℕ} (hd : 2 ≤ d) {c σ : ℝ} (hc : 0 < c) (hbelow : -1 < σ) (habove : σ < 1) (s : ℝ) : CohnElkies.H_σ (↑d / 2) (c * √↑d) σ s ≤ CohnElkies.H_σ (↑d / 2) (c * √↑d) σ 0
Report Lemma 3.3: `H_σ(s) ≤ H_σ(0)`.
By the digamma series in Definition 3.1.4, for y > 0,
h_\lambda'(y)
= \tfrac12\bigl(\operatorname{Im}\psi(\lambda + iy/2) - \operatorname{Im}\psi(iy/2)\bigr) < 0,
because \sum_k b/((k+\lambda)^2+b^2) < \sum_k b/(k^2+b^2) termwise for b = y/2 > 0; the
formalization instead reads off the monotonicity from the product formulas of
Lemma 3.1.3 (CohnElkies.lowerGammaBoundaryLog_dimension_antitoneOn).
Thus h_\lambda is even and decreasing on (0,\infty), and so is P_\sigma. For N > 0,
the function q_N(u) = \max\{h_\lambda(\lambda u) + N, 0\} is nonnegative, even, decreasing on
(0,\infty), and integrable (the singularity at 0 is logarithmic and
h_\lambda \to -\infty at infinity, so q_N has compact support). Since
H_\sigma(s) = (P_\sigma * h_\lambda(\lambda\,\cdot))(s/\lambda),
Lemma 4.1.23 gives
(P_\sigma*q_N)(s/\lambda) \le (P_\sigma*q_N)(0). Subtracting NM_\sigma turns this into
\int P_\sigma(T)\max\{h_\lambda(s-\lambda T), -N\}\,dT
\le \int P_\sigma(T)\max\{h_\lambda(-\lambda T), -N\}\,dT.
The left side is at least H_\sigma(s), and the right side tends to H_\sigma(0) as
N \to \infty by dominated convergence (exponential decay of P_\sigma). Hence
H_\sigma(s) \le H_\sigma(0).
For every 0 \le \sigma < 1 there is E_\sigma < \infty, independent of d, c and g,
such that in the setting of Definition 4.1.2 (with d \ge 2), with J_\sigma
from Definition 4.1.24 (equation (20)),
H_\sigma(0) \le \lambda M_\sigma\bigl(\log(2\pi c^2) + J_\sigma\bigr) + E_\sigma;
hence, by Lemma 4.1.25,
H_\sigma(s) \le \lambda M_\sigma\bigl(\log(2\pi c^2) + J_\sigma\bigr) + E_\sigma for every
s \in \mathbb{R}. Uses Definition 4.1.7,
Definition 4.1.8, Definition 4.1.10 and
Definition 4.1.11.
Lean code for Lemma4.1.26●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.lowerStripPoissonMajorant_dimension_central_bound {d : ℕ} (hd : 2 ≤ d) {c σ : ℝ} (hc : 0 < c) (hzero : 0 ≤ σ) (habove : σ < 1) : CohnElkies.H_σ (↑d / 2) (c * √↑d) σ 0 ≤ ↑d / 2 * CohnElkies.M_σ σ * (Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) + CohnElkies.lowerPoissonEndpointExpectation σ) + CohnElkies.lowerRiemannPoissonError σ
theorem CohnElkies.lowerStripPoissonMajorant_dimension_central_bound {d : ℕ} (hd : 2 ≤ d) {c σ : ℝ} (hc : 0 < c) (hzero : 0 ≤ σ) (habove : σ < 1) : CohnElkies.H_σ (↑d / 2) (c * √↑d) σ 0 ≤ ↑d / 2 * CohnElkies.M_σ σ * (Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) + CohnElkies.lowerPoissonEndpointExpectation σ) + CohnElkies.lowerRiemannPoissonError σ
Report Lemma 3.3 at the centre: `H_σ(0)` is at most `(d/2) M_σ (log(2πe c²) + J_σ)` plus the Poisson average of the Riemann error.
Riemann sums. Since R = c\sqrt{2\lambda},
\lambda\log(\pi R^2) = \lambda\log(2\pi c^2) + \lambda\log\lambda. Put b = \lambda T/2. If
d = 2n is even, the recurrence in Lemma 3.1.3 gives
|\Gamma(n+ib)| = |\Gamma(ib)|\prod_{k=0}^{n-1}\sqrt{k^2+b^2} and |\Gamma(-ib)| = |\Gamma(ib)|,
so for T \ne 0 we get h_n(nT) = n\log(2\pi c^2) - \sum_{k=0}^{n-1}f_T(k/n).
Monotonicity of f_T on [0,1] bounds the left Riemann-sum error by f_T(1) - f_T(0):
0 \le h_n(nT) - n\bigl(\log(2\pi c^2) - \int_0^1 f_T\bigr) \le \tfrac12\log(1 + 4/T^2).
If d = 2n+1, so \lambda = n + \tfrac12, then
|\Gamma(\lambda + ib)| = |\Gamma(\tfrac12 + ib)|\prod_{k=0}^{n-1}\sqrt{(k+\tfrac12)^2 + b^2} and
|\Gamma(-ib)|^2/|\Gamma(\tfrac12+ib)|^2 = \coth(\pi|b|)/|b| by (7), whence
h_\lambda(\lambda T) = \lambda\log(2\pi c^2)
- \sum_{k=0}^{n-1}f_T\bigl(\tfrac{k+1/2}{\lambda}\bigr) + E_\lambda(T)
with E_\lambda(T) = \tfrac12\log\lambda + \tfrac12\log(\coth(\pi|b|)/|b|).
The midpoint Riemann-sum error on [0, n/\lambda] is at most f_T(n/\lambda) - f_T(0), and the
remaining interval [n/\lambda, 1] has length 1/(2\lambda); together these contribute at most
C(1 + \log(2+|T|) + \log(2+|T|^{-1})). Adding C\log(2+\lambda) also bounds the endpoint
correction E_\lambda(T). Since P_\sigma(T) \ll_\sigma e^{-\pi|T|/2} and \log(2+|T|^{-1})
is locally integrable, integrating the even- and odd-dimensional bounds against P_\sigma
proves (19). The formalization keeps only the upper bounds and absorbs E_\lambda(T) into the
d-independent majorant E(T) (Lemma 7.2.3).
Value at 0. Both P_\sigma and h_\lambda are even, so
H_\sigma(0) = \int P_\sigma(T)h_\lambda(\lambda T)\,dT, and (19) gives
|H_\sigma(0) - \lambda M_\sigma(\log(2\pi c^2) + J_\sigma)| \le C_\sigma\log(2+\lambda).
The probability density p(u) = \dfrac{\pi}{4}\operatorname{sech}^2\bigl(\dfrac{\pi u}{2}\bigr)
= \dfrac{\pi e^{\pi u}}{(1 + e^{\pi u})^2} on \mathbb{R} has characteristic function
(equation (21))
\int_{\mathbb{R}}p(u)e^{itu}\,du = \int_{\mathbb{R}}p(u)\cos(tu)\,du = \dfrac{t}{\sinh t}
for t \in \mathbb{R}, interpreted as 1 at t = 0.
Lean code for Lemma4.1.27●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LimitingDensity.leancomplete
theorem CohnElkies.poissonLogistic_characteristic (t : ℝ) : ∫ (u : ℝ), ↑(CohnElkies.poissonLogisticDensity u) * Complex.exp (Complex.I * ↑t * ↑u) = if t = 0 then 1 else ↑t / ↑(Real.sinh t)
theorem CohnElkies.poissonLogistic_characteristic (t : ℝ) : ∫ (u : ℝ), ↑(CohnElkies.poissonLogisticDensity u) * Complex.exp (Complex.I * ↑t * ↑u) = if t = 0 then 1 else ↑t / ↑(Real.sinh t)
The characteristic function of `p`: `∫ p(u) e^{itu} du = t / sinh t`; report (21).
The report shifts the contour by 2i: the integrand p(u)e^{itu} is 2i-periodic up to the
factor e^{-2t}, and the only pole between the two lines is the double pole of
\operatorname{sech}^2(\pi u/2) at u = i, whose residue contributes 2te^{-t}; thus
(1 - e^{-2t})\int p(u)e^{itu}\,du = 2te^{-t}, i.e. t/\sinh t for t > 0, and evenness
handles t < 0. The formalization argues without contour integration: p is the derivative
of the logistic function \ell(u) = e^{\pi u}/(1+e^{\pi u}), and the substitution x = \ell(u)
turns \int p(u)e^{\pi u w}\,du into the beta integral B(1+w, 1-w)
(CohnElkies.poissonLogistic_betaIntegral); with w = it/\pi this is
\Gamma(1 + it/\pi)\Gamma(1 - it/\pi), which equals t/\sinh t by the reflection formula
(Lemma 3.1.3, Complex.Gamma_one_add_I_mul_mul_Gamma_one_sub_I_mul).
The value 1 at t = 0 is \int p = 1.
With p from Lemma 4.1.27 and \psi from Definition 3.1.4,
for every x \ge 0 (equation (22))
\int_{\mathbb{R}}p(u)\log\sqrt{x^2+u^2}\,du = \psi\Bigl(\dfrac{x+1}{2}\Bigr) + \log 2.
Lean code for Lemma4.1.28●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LogMomentDigamma.leancomplete
theorem CohnElkies.integral_poissonLogisticDensity_mul_log_sqrt {x : ℝ} (hx : 0 ≤ x) : ∫ (u : ℝ), CohnElkies.poissonLogisticDensity u * Real.log √(x ^ 2 + u ^ 2) = ((x + 1) / 2).digamma + Real.log 2
theorem CohnElkies.integral_poissonLogisticDensity_mul_log_sqrt {x : ℝ} (hx : 0 ≤ x) : ∫ (u : ℝ), CohnElkies.poissonLogisticDensity u * Real.log √(x ^ 2 + u ^ 2) = ((x + 1) / 2).digamma + Real.log 2
Report (22): `∫ p(u) log √(x² + u²) du = ψ((x + 1) / 2) + log 2` for `x ≥ 0`.
Let x > 0. Taking real parts in the complex Frullani formula
\int_0^\infty (e^{-t} - e^{-(x+iu)t})/t\,dt = \log(x+iu) gives
\log\sqrt{x^2+u^2} = \int_0^\infty\dfrac{e^{-t} - e^{-xt}\cos(ut)}{t}\,dt. The integrand times
p(u) is integrable on \mathbb{R} \times (0,\infty) (it is bounded by p(u)(1 + x + |u|)
for t \le 1, using |1 - \cos(ut)| \le |u|t, and by p(u)(e^{-t} + e^{-xt}) for t \ge 1),
so by Fubini, \int p = 1 and Lemma 4.1.27,
\int_{\mathbb{R}}p(u)\log\sqrt{x^2+u^2}\,du = \int_0^\infty\Bigl(\dfrac{e^{-t}}{t} - \dfrac{e^{-xt}}{\sinh t}\Bigr)dt.
Gauss's integral (Lemma 3.1.7) at m = (x+1)/2, after the substitution
t = 2s, reads \psi((x+1)/2) = \int_0^\infty\bigl(e^{-2s}/s - e^{-xs}/\sinh s\bigr)ds. Subtracting,
the difference of the two sides is \int_0^\infty (e^{-s} - e^{-2s})/s\,ds = \log 2 (Frullani).
The case x = 0 follows by letting x \downarrow 0: the left side converges by dominated
convergence (for 0 \le x \le 1, |\log\sqrt{x^2+u^2}| \le |\log|u|| + |u|, and \log|u| is
locally integrable against the bounded density p), and \psi is continuous at 1/2.
For J_\sigma from Definition 4.1.24,
\lim_{\sigma\uparrow 1}J_\sigma = \log(\pi/2), that is,
J^{\mathrm{Lean}}_\sigma \to \log(\pi/2) - 1.
Lean code for Lemma4.1.29●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LimitingDensity.leancomplete
theorem CohnElkies.tendsto_lowerPoissonEndpointExpectation : Filter.Tendsto CohnElkies.lowerPoissonEndpointExpectation (nhdsWithin 1 (Set.Iio 1)) (nhds CohnElkies.limitingPoissonEndpointExpectation)
theorem CohnElkies.tendsto_lowerPoissonEndpointExpectation : Filter.Tendsto CohnElkies.lowerPoissonEndpointExpectation (nhdsWithin 1 (Set.Iio 1)) (nhds CohnElkies.limitingPoissonEndpointExpectation)
-
theoremdefined in CohnElkies/LowerBound/LimitingDensity.leancomplete
theorem CohnElkies.limitingPoissonEndpointExpectation_eq_log_pi_div_two_sub_one : CohnElkies.limitingPoissonEndpointExpectation = Real.log (Real.pi / 2) - 1
theorem CohnElkies.limitingPoissonEndpointExpectation_eq_log_pi_div_two_sub_one : CohnElkies.limitingPoissonEndpointExpectation = Real.log (Real.pi / 2) - 1
Lemma 3.4 of the report: `J_σ → log (π/2) - 1` as `σ ↑ 1`.
With T = 2u, divide the lower-edge harmonic measure P_\sigma(T)\,dT by its mass M_\sigma.
The resulting probability density in u is
p_\sigma(u) = \dfrac{2P_\sigma(2u)}{M_\sigma}
= \dfrac{\sin\theta}{(1-\sigma)(\cosh(\pi u) - \cos\theta)},
and J_\sigma = -\int_{\mathbb{R}}p_\sigma(u)\int_0^1\log\sqrt{x^2+u^2}\,dx\,du. As
\sigma \uparrow 1, \theta \to \pi, \sin\theta/(1-\sigma) \to \pi/2, and the densities
p_\sigma are uniformly bounded by Ce^{-\pi|u|}
(CohnElkies.stripNormalizedPoissonExtension_le_majorant); they converge pointwise and in
L^1 to p(u) = \dfrac{\pi}{2(\cosh(\pi u) + 1)}
= \dfrac{\pi}{4}\operatorname{sech}^2\bigl(\dfrac{\pi u}{2}\bigr)
of Lemma 4.1.27. The uniform exponential bound and the local
integrability of \log|u| justify dominated convergence in J_\sigma
(CohnElkies.tendsto_integral_stripNormalizedPoissonKernel_mul), so
\lim_{\sigma\uparrow1}J_\sigma = -\int p(u)\int_0^1\log\sqrt{x^2+u^2}\,dx\,du.
The report evaluates this limit with Lemma 4.1.28 and
\int_0^1\psi\bigl(\tfrac{x+1}{2}\bigr)\,dx = 2\log\dfrac{\Gamma(1)}{\Gamma(1/2)} = -\log\pi,
which give -\int_0^1(\psi(\tfrac{x+1}{2}) + \log 2)\,dx = \log\pi - \log 2. The formalization
evaluates it instead by Lemma 7.3.3: the inner integral is
1 + \Lambda(2u) with the endpoint phase \Lambda of Lemma 7.2.3, the
expectation of 1 + \Lambda(2u) against p is \log(\pi/2), and hence
\lim J^{\mathrm{Lean}}_\sigma = \int p(u)\Lambda(2u)\,du = \log(\pi/2) - 1.
For every 0 < c < 1/\pi, with J_\sigma from Definition 4.1.24,
\log(2\pi c^2) + \lim_{\sigma\uparrow1}J_\sigma = \log(\pi^2c^2) < 0, so
\delta_c(\sigma) = -(\log(2\pi c^2) + J_\sigma) > 0 for all \sigma < 1 close enough to 1;
fix such a \sigma = \sigma(c) \in (0,1) (equation (23)).
Lean code for Lemma4.1.30●2 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/LimitingDensity.leancomplete
theorem CohnElkies.lowerPoissonEndpointSharpCoefficient_eq {c : ℝ} (hc : 0 < c) : Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) + CohnElkies.limitingPoissonEndpointExpectation = Real.log (Real.pi ^ 2 * c ^ 2)
theorem CohnElkies.lowerPoissonEndpointSharpCoefficient_eq {c : ℝ} (hc : 0 < c) : Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) + CohnElkies.limitingPoissonEndpointExpectation = Real.log (Real.pi ^ 2 * c ^ 2)
The sharp threshold of report (23): `log (2πe c²) + lim J_σ = log (π² c²)`.
-
theoremdefined in CohnElkies/LowerBound/LimitingDensity.leancomplete
theorem CohnElkies.eventually_lowerPoissonEndpointSharpCoefficient_neg {c : ℝ} (hc : 0 < c) (hsharp : c < Real.pi⁻¹) : ∀ᶠ (σ : ℝ) in nhdsWithin 1 (Set.Iio 1), Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) + CohnElkies.lowerPoissonEndpointExpectation σ < 0
theorem CohnElkies.eventually_lowerPoissonEndpointSharpCoefficient_neg {c : ℝ} (hc : 0 < c) (hsharp : c < Real.pi⁻¹) : ∀ᶠ (σ : ℝ) in nhdsWithin 1 (Set.Iio 1), Real.log (2 * Real.pi * Real.exp 1 * c ^ 2) + CohnElkies.lowerPoissonEndpointExpectation σ < 0
Report (23): for `c < 1/π` the sharp coefficient is eventually negative as `σ ↑ 1`.
By Lemma 4.1.29, \log(2\pi c^2) + J_\sigma \to \log(2\pi c^2) + \log(\pi/2) = \log(\pi^2c^2)
as \sigma \uparrow 1, which is negative exactly when c < 1/\pi.
From now on fix \sigma = \sigma(c) and \delta_c > 0 as in (23). We first bound Z on the
horizontal line \operatorname{Im} t = \sigma\lambda, and then use that bound to control the mass
of g inside B(0,c\sqrt d).
There is \gamma_c > 0, depending only on c (not on d, g, or \varsigma), such that
for every sufficiently large d, with \sigma = \sigma(c) from
Lemma 4.1.30 and H_\sigma from Definition 4.1.11
(in the setting of Definition 4.1.2),
H_\sigma(s) \le -\gamma_c\lambda for all s \in \mathbb{R} (equation (24)).
Lean code for Lemma4.1.31●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.exists_lowerStripPoissonMajorant_uniform_negative {c : ℝ} (hc : 0 < c) (hsharp : c < Real.pi⁻¹) : ∃ σ γ, 0 < σ ∧ σ < 1 ∧ 0 < γ ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (s : ℝ), CohnElkies.H_σ (↑d / 2) (c * √↑d) σ s ≤ -γ * (↑d / 2)
theorem CohnElkies.exists_lowerStripPoissonMajorant_uniform_negative {c : ℝ} (hc : 0 < c) (hsharp : c < Real.pi⁻¹) : ∃ σ γ, 0 < σ ∧ σ < 1 ∧ 0 < γ ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (s : ℝ), CohnElkies.H_σ (↑d / 2) (c * √↑d) σ s ≤ -γ * (↑d / 2)
Report Lemma 3.5: for a subcritical radius the majorant is uniformly negative of order `d`.
Uniform negativity. The maximum estimate (20) of Lemma 4.1.26 and
\log(2\pi c^2) + J_\sigma = -\delta_c from Lemma 4.1.30 give
H_\sigma(s) \le -\lambda M_\sigma\delta_c + O_\sigma(\log\lambda) \le -\gamma_c\lambda for all
s once d is large, with \gamma_c > 0 independent of s, g and \varsigma.
For every 0 \le \sigma < 1 there are B_c, C_c, \kappa_c > 0, depending only on c and
\sigma, such that for all d \ge 2 and all |S| \ge B_c, in the setting of
Definition 4.1.2 and with H_\sigma from Definition 4.1.11,
H_\sigma(\lambda S) \le -\kappa_c\lambda\log\dfrac{|S|}{C_c} (equation (25)).
Lean code for Lemma4.1.32●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.exists_lowerStripPoissonMajorant_logarithmic_tail {c σ : ℝ} (hc : 0 < c) (hσ : 0 ≤ σ) (hσone : σ < 1) : ∃ A B κ, 0 < A ∧ 0 < B ∧ 0 < κ ∧ ∀ (d : ℕ), 2 ≤ d → ∀ (S : ℝ), B ≤ |S| → CohnElkies.H_σ (↑d / 2) (c * √↑d) σ (↑d / 2 * S) ≤ -κ * (↑d / 2) * Real.log (|S| / A)
theorem CohnElkies.exists_lowerStripPoissonMajorant_logarithmic_tail {c σ : ℝ} (hc : 0 < c) (hσ : 0 ≤ σ) (hσone : σ < 1) : ∃ A B κ, 0 < A ∧ 0 < B ∧ 0 < κ ∧ ∀ (d : ℕ), 2 ≤ d → ∀ (S : ℝ), B ≤ |S| → CohnElkies.H_σ (↑d / 2) (c * √↑d) σ (↑d / 2 * S) ≤ -κ * (↑d / 2) * Real.log (|S| / A)
All frequencies. Apply the gamma identities of Lemma 3.1.3 to (14): each
factor of the recurrence |\Gamma(\lambda + ib)|/|\Gamma(ib)| has modulus at least
|b| = \lambda|U|/2 at y = \lambda U, so in both parities
h_\lambda(\lambda U) \le \lambda\log\dfrac{4\pi c^2}{|U|} + E_\lambda(U) for U \ne 0, where
E_\lambda(U) = 0 for \lambda \in \mathbb{N} and
E_\lambda(U) = \tfrac12\log\coth(\pi\lambda|U|/2) for \lambda \in \mathbb{N} + \tfrac12
(CohnElkies.lowerGammaBoundaryLog_dimension_scaled_log_tail). Expanding \log\coth x in its
odd exponential series gives
\int_{\mathbb{R}}E_\lambda(U)\,dU = \frac{2}{\pi\lambda}\int_0^\infty\log\coth x\,dx
= \frac{\pi}{4\lambda},
so the P_\sigma-convolution of E_\lambda is at most \pi\|P_\sigma\|_\infty/(4\lambda).
Consequently (18) gives
H_\sigma(\lambda S) \le \lambda M_\sigma\log(4\pi c^2)
- \lambda\int_{\mathbb{R}}P_\sigma(T)\log|S - T|\,dT + O_\sigma(\lambda^{-1}).
Split the logarithmic integral at |T| = |S|/2. On |T| \le |S|/2 we have |S-T| \ge |S|/2
and the mass of P_\sigma there is M_\sigma + O_\sigma(e^{-\pi|S|/4}); on |T| > |S|/2 the
only possible negative contribution comes from |S - T| < 1, which is O_\sigma(e^{-\pi|S|/2})
by local integrability of \log|S-T| and exponential decay of P_\sigma. Hence there are
B_c, C_c' > 0 with \int P_\sigma(T)\log|S-T|\,dT \ge \frac{M_\sigma}{2}\log|S| - C_c' for
|S| \ge B_c, and after increasing C_c' this yields (25).
There are \gamma_c, C_c > 0, depending only on c, such that for every sufficiently large
d, with \sigma = \sigma(c) from Lemma 4.1.30 and Z as in
Definition 4.1.2,
\int_{\mathbb{R}}|Z(s + i\sigma\lambda)|\,ds \le C_c\lambda e^{-\gamma_c\lambda} (equation (26)).
Lean code for Lemma4.1.33●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/CenteredMax.leancomplete
theorem CohnElkies.integral_norm_Z_g_le_of_majorant {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R σ γ C : ℝ} (hR : 0 < R) (hσbelow : -1 < σ) (hσabove : σ < 1) (hpoint : ∀ (s : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ Real.exp (CohnElkies.H_σ (↑d / 2) R σ s)) (hmajor : ∀ (S : ℝ), Real.exp (CohnElkies.H_σ (↑d / 2) R σ (↑d / 2 * S)) ≤ C * Real.exp (-γ * (↑d / 2)) / (1 + |S|) ^ 2) : ∫ (s : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ C * CohnElkies.lowerInverseQuadraticMass * (↑d / 2) * Real.exp (-γ * (↑d / 2))
theorem CohnElkies.integral_norm_Z_g_le_of_majorant {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R σ γ C : ℝ} (hR : 0 < R) (hσbelow : -1 < σ) (hσabove : σ < 1) (hpoint : ∀ (s : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ Real.exp (CohnElkies.H_σ (↑d / 2) R σ s)) (hmajor : ∀ (S : ℝ), Real.exp (CohnElkies.H_σ (↑d / 2) R σ (↑d / 2 * S)) ≤ C * Real.exp (-γ * (↑d / 2)) / (1 + |S|) ^ 2) : ∫ (s : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖ ≤ C * CohnElkies.lowerInverseQuadraticMass * (↑d / 2) * Real.exp (-γ * (↑d / 2))
Report Lemma 3.6: the `L¹` norm of `Z` on the interior line `Im z = σλ`, under a pointwise Poisson majorization and a Cauchy-type majorant for `exp H_σ`.
Integration. Choose B > \max\{B_c, C_c'\} and q = M_\sigma\lambda/2 > 1. By (24) of Lemma 4.1.31,
\int_{|s| \le B\lambda}e^{H_\sigma(s)}\,ds \le 2B\lambda e^{-\gamma_c\lambda}, while the
substitution s = \lambda S and (25) of Lemma 4.1.32 give
\int_{|s| > B\lambda}e^{H_\sigma(s)}\,ds \le \lambda\int_{|S|>B}(|S|/C_c')^{-q}\,dS
= \dfrac{2\lambda C_c'}{q-1}\Bigl(\dfrac{B}{C_c'}\Bigr)^{1-q},
which decays at exponential rate (M_\sigma/2)\log(B/C_c') > 0 in \lambda. Decreasing
\gamma_c if necessary and applying |Z(s+i\sigma\lambda)| \le e^{H_\sigma(s)} from
Lemma 4.1.22 gives (26). The formalization merges the two integrals into the single
majorant of Lemma 7.4.1.
In the setting of Definition 4.1.2, for every -1 < \sigma < 1,
\int_{-\infty}^0|\varphi(v)|\,dv = \dfrac{1}{\|g\|_1}\int_{|x|<R}|g(x)|\,dx
\le \dfrac{1}{2\pi(1-\sigma)\lambda}\int_{\mathbb{R}}|Z(s+i\sigma\lambda)|\,ds,
the equality being Lemma 4.1.5. Consequently, by (26) of
Lemma 4.1.33, for every 0 < c < 1/\pi there exist C_c, \gamma_c > 0 and
d_0(c) such that \int_{-\infty}^0|\varphi(v)|\,dv \le C_c e^{-\gamma_c d} for all
d \ge d_0(c) (equation (27)); in the formalization this consequence is
Proposition 4.1.35 in the form (11).
Lean code for Lemma4.1.34●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/LowerBound/GammaBoundary.leancomplete
theorem CohnElkies.RadialEigenfunction.setIntegral_ball_norm_le {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R σ : ℝ} (hR : 0 < R) (hσbelow : -1 < σ) (hσabove : σ < 1) : ∫ (x : CohnElkies.Euclidean d) in Metric.ball 0 R, ‖g.toFun x‖ ≤ ((2 * Real.pi)⁻¹ * ∫ (s : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖) / ((1 - σ) * (↑d / 2)) * CohnElkies.L1norm g.toFun
theorem CohnElkies.RadialEigenfunction.setIntegral_ball_norm_le {d : ℕ} {ς : ℤˣ} (hd : 0 < d) (g : CohnElkies.RadialEigenfunction d ς) {R σ : ℝ} (hR : 0 < R) (hσbelow : -1 < σ) (hσabove : σ < 1) : ∫ (x : CohnElkies.Euclidean d) in Metric.ball 0 R, ‖g.toFun x‖ ≤ ((2 * Real.pi)⁻¹ * ∫ (s : ℝ), ‖CohnElkies.Z_g hd g.toFun R (↑s + Complex.I * (↑σ * (↑d / 2)))‖) / ((1 - σ) * (↑d / 2)) * CohnElkies.L1norm g.toFun
Lemmas 3.2 and 3.6 of the report combined: the mass of a radial eigenfunction `g` in the ball of radius `R` is controlled by the `L¹` norm of `Z` on the interior line `Im z = σλ`: `∫_{‖x‖<R} |g| ≤ ((2π)⁻¹ ‖Z(· + iσλ)‖₁ / ((1 - σ) λ)) ‖g‖₁`.
Let G(v) = e^{(\sigma-1)\lambda v}\varphi(v). By (12) and the substitution r = Re^v,
\int_{\mathbb{R}}|G(v)|\,dv
= \dfrac{S_dR^{(1-\sigma)\lambda}}{\|g\|_1}\int_0^\infty|g(r)|r^{(1+\sigma)\lambda-1}\,dr
< \infty,
so G \in L^1(\mathbb{R}), and Lemma 4.1.6 with t = s + i\sigma\lambda
identifies its Fourier transform \int G(v)e^{-isv}\,dv with Z(s + i\sigma\lambda). This
transform is integrable by (26) of Lemma 4.1.33
(CohnElkies.RadialEigenfunction.integrable_Z_g_shifted), so Fourier inversion gives
\varphi(v)
= \dfrac{e^{(1-\sigma)\lambda v}}{2\pi}\int_{\mathbb{R}}Z(s+i\sigma\lambda)e^{isv}\,ds.
Taking absolute values and integrating over v < 0 contributes
\int_{-\infty}^0e^{(1-\sigma)\lambda v}\,dv = ((1-\sigma)\lambda)^{-1}, hence
\int_{-\infty}^0|\varphi(v)|\,dv
\le \dfrac{1}{2\pi(1-\sigma)\lambda}\int_{\mathbb{R}}|Z(s+i\sigma\lambda)|\,ds,
which is at most \dfrac{C_c}{2\pi(1-\sigma)}e^{-\gamma_c d/2}. Renaming the constants (recall
\lambda = d/2) gives (27).
For every 0 < c < 1/\pi there exist C_c, \gamma_c > 0 and d_0(c) \in \mathbb{N} such
that, for every d \ge d_0(c), every \varsigma \in \{-1,+1\}, and every nonzero
g \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) satisfying \widehat g = \varsigma g
and g(0) = 0, one has (equation (11))
\int_{|x| < c\sqrt d}|g(x)|\,dx \le C_c e^{-\gamma_c d}\,\|g\|_1.
Lean code for Proposition4.1.35●1 theorem
Associated Lean declarations
-
CohnElkies.exists_interior_mass_bound[complete]
-
CohnElkies.exists_interior_mass_bound[complete]
-
theoremdefined in CohnElkies/LowerBound/Main.leancomplete
theorem CohnElkies.exists_interior_mass_bound {c : ℝ} (hc : 0 < c) (hcπ : c < Real.pi⁻¹) : ∃ C γ, 0 < C ∧ 0 < γ ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (ς : ℤˣ) (g : CohnElkies.RadialEigenfunction d ς), ∫ (x : CohnElkies.Euclidean d) in Metric.ball 0 (c * √↑d), ‖g.toFun x‖ ≤ C * Real.exp (-γ * ↑d) * ∫ (x : CohnElkies.Euclidean d), ‖g.toFun x‖
theorem CohnElkies.exists_interior_mass_bound {c : ℝ} (hc : 0 < c) (hcπ : c < Real.pi⁻¹) : ∃ C γ, 0 < C ∧ 0 < γ ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (ς : ℤˣ) (g : CohnElkies.RadialEigenfunction d ς), ∫ (x : CohnElkies.Euclidean d) in Metric.ball 0 (c * √↑d), ‖g.toFun x‖ ≤ C * Real.exp (-γ * ↑d) * ∫ (x : CohnElkies.Euclidean d), ‖g.toFun x‖
Proposition 3.1 of the report: for `0 < c < 1/π` there are `C, γ > 0` such that in every large dimension `d`, every nonzero real radial Schwartz `g` with `𝓕 g = ±g` and `g(0) = 0` has exponentially small mass inside the ball of radius `c√d`: `∫_{‖x‖ < c√d} |g| ≤ C e^{-γd} ‖g‖₁`. The constants come from the Cauchy-type majorant of Lemma 3.6 and depend only on `c`.
By Lemma 4.1.5, the left side of (27) is exactly
\|g\|_1^{-1}\int_{|x|<c\sqrt d}|g(x)|\,dx. Thus Lemma 4.1.34, fed with the L^1
bound (26) of Lemma 4.1.33, proves (11), uniformly in g and in its Fourier
eigenvalue \varsigma.