the proof notes (5′), layout (4,5,3): with t = 1/2 + iy, y = nx,

S_n |t R_n(t) w(y)| ≤ exp(c₀ + 7 log(n+1)) (1+|x|)^7 exp(−3n W(|x|)),

from the sum–integral comparison for log ∏|t+j| (LogNorm), the scaling of ∫₀^b log|u + i n x| du, the Stirling bound for S_n, |w(y)| ≤ 4π(|r|+π) e^{−2π|y|}, and the identity 5 log 5 − 1 + 4∫₀¹ log|u+ix| − ∫₀⁵ log|u+ix| − 2π|x| = −3 W(|x|). The wfun bound follows Zeta32/Analytic/Contour/Kernel.lean and the structure follows Li2Unified/Modular/Base/OriginalProductLog.lean, OriginalScaledProductLog.lean.

The kernel bound

theorem Zeta32.Analytic.EnergyI.inv_cosh_sq_le' (x : ℝ) : 1 / Real.cosh x ^ 2 ≤ 4 * Real.exp (-(2 * |x|))

theorem Zeta32.Analytic.EnergyI.norm_wfun_le (r : ℚ) (y : ℝ) : ‖wfun r y‖ ≤ 4 * Real.pi * (|↑r| + Real.pi) * Real.exp (-(2 * Real.pi) * |y|)

The products

theorem Zeta32.Analytic.EnergyI.prod_log_norm_eq_sum (m : ℕ) (y : ℝ) : Real.log ‖∏ j ∈ Finset.Icc 1 m, (1 / 2 + Complex.I * ↑y + ↑j)‖ = ∑ i ∈ Finset.range m, Real.log ‖↑(↑i + 3 / 2) + ↑y * Complex.I‖

theorem Zeta32.Analytic.EnergyI.prod_ne_zero (m : ℕ) (y : ℝ) : ∏ j ∈ Finset.Icc 1 m, (1 / 2 + Complex.I * ↑y + ↑j) ≠ 0

The external field identity

theorem Zeta32.Analytic.EnergyI.integral_log_norm_abs (b x : ℝ) : ∫ (t : ℝ) in 0..b, Real.log ‖↑t + ↑x * Complex.I‖ = ∫ (t : ℝ) in 0..b, Real.log ‖↑t + ↑|x| * Complex.I‖

theorem Zeta32.Analytic.EnergyI.external_field_eq (x : ℝ) : ((5 * Real.log 5 - 1 + 4 * ∫ (t : ℝ) in 0..1, Real.log ‖↑t + ↑x * Complex.I‖) - ∫ (t : ℝ) in 0..5, Real.log ‖↑t + ↑x * Complex.I‖) - 2 * Real.pi * |x| = -(3 * Wt |x|)

5 log 5 − 1 + 4 I₁ − I₅ − 2π|x| = −3 W(|x|).

The pointwise bound

noncomputable def Zeta32.Analytic.EnergyI.psiH (r : ℚ) (n : ℕ) (y : ℝ) : ℝ

The single-variable Heine factor |t R_n(t) w(y)|, t = 1/2 + iy.

Equations

• Zeta32.Analytic.EnergyI.psiH r n y = ‖(1 / 2 + Complex.I * ↑y) * Zeta32.Rfun n (1 / 2 + Complex.I * ↑y) * Zeta32.wfun r y‖

theorem Zeta32.Analytic.EnergyI.psiH_nonneg (r : ℚ) (n : ℕ) (y : ℝ) : 0 ≤ psiH r n y

noncomputable def Zeta32.Analytic.EnergyI.cPt (r : ℚ) : ℝ

The constant c₀ = 7 + log(4π(|r|+π)) + 6 log 2.

Equations

• Zeta32.Analytic.EnergyI.cPt r = 7 + Real.log (4 * Real.pi * (|↑r| + Real.pi)) + 6 * Real.log 2

theorem Zeta32.Analytic.EnergyI.pointwise_bound (r : ℚ) (n : ℕ) (hn : 1 ≤ n) (x : ℝ) : ↑(Sn n) * psiH r n (↑n * x) ≤ Real.exp (cPt r + 7 * Real.log (↑n + 1)) * ((1 + |x|) ^ 7 * Real.exp (-(3 * ↑n) * Wt |x|))

the proof notes (5′).