∫₀^b log|u + ix| du and the sum–integral comparison of the proof notes (5′). -- adapted from Li2Unified/Modular/Base/LogNormIntegral.lean, LogNormMonotone.lean, -- LogNormScaling.lean, -- LogNormSumComparison.lean, LogNormSumError.lean (namespace changed only).

noncomputable def Zeta32.Analytic.EnergyI.logNormIntegralPrimitive (x t : ℝ) : ℝ

The explicit primitive; its value at zero is zero for every x.

Equations

• Zeta32.Analytic.EnergyI.logNormIntegralPrimitive x t = t / 2 * Real.log (t ^ 2 + x ^ 2) - t + x * Real.arctan (t / x)

theorem Zeta32.Analytic.EnergyI.log_norm_real_add_imag (t x : ℝ) : Real.log ‖↑t + ↑x * Complex.I‖ = 1 / 2 * Real.log (t ^ 2 + x ^ 2)

theorem Zeta32.Analytic.EnergyI.log_norm_real_add_imag_zero (t : ℝ) : Real.log ‖↑t + 0 * Complex.I‖ = Real.log t

theorem Zeta32.Analytic.EnergyI.real_add_imag_ne_zero {x : ℝ} (hx : 0 < x) (t : ℝ) : ↑t + ↑x * Complex.I ≠ 0

theorem Zeta32.Analytic.EnergyI.continuous_log_norm_real_add_imag {x : ℝ} (hx : 0 < x) : Continuous fun (t : ℝ) => Real.log ‖↑t + ↑x * Complex.I‖

theorem Zeta32.Analytic.EnergyI.hasDerivAt_logNormIntegralPrimitive {x : ℝ} (hx : 0 < x) (t : ℝ) : HasDerivAt (logNormIntegralPrimitive x) (Real.log ‖↑t + ↑x * Complex.I‖) t

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_norm_real_add_imag {x : ℝ} (hx : 0 ≤ x) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log ‖↑t + ↑x * Complex.I‖) MeasureTheory.volume a b

theorem Zeta32.Analytic.EnergyI.integral_log_norm_real_add_imag_of_pos {x : ℝ} (hx : 0 < x) (b : ℝ) : ∫ (t : ℝ) in 0..b, Real.log ‖↑t + ↑x * Complex.I‖ = b / 2 * Real.log (b ^ 2 + x ^ 2) - b + x * Real.arctan (b / x)

theorem Zeta32.Analytic.EnergyI.integral_log_norm_real_add_imag {x b : ℝ} (hx : 0 ≤ x) : ∫ (t : ℝ) in 0..b, Real.log ‖↑t + ↑x * Complex.I‖ = b / 2 * Real.log (b ^ 2 + x ^ 2) - b + x * Real.arctan (b / x)

The integral from GLOBAL-INTEGRAL-v1, Section 2, with both boundary cases.

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_norm_real_add_imag_all (y a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log ‖↑t + ↑y * Complex.I‖) MeasureTheory.volume a b

Integrability for every real imaginary parameter, including zero.

theorem Zeta32.Analytic.EnergyI.monotoneOn_log_norm_real_add_imag (y : ℝ) : MonotoneOn (fun (t : ℝ) => Real.log ‖↑t + ↑y * Complex.I‖) (Set.Ioi 0)

The positive real axis excludes the exceptional value Real.log 0.

theorem Zeta32.Analytic.EnergyI.log_norm_real_add_imag_bounds (y : ℝ) {t : ℝ} (ht : 0 < t) : Real.log t ≤ Real.log ‖↑t + ↑y * Complex.I‖ ∧ Real.log ‖↑t + ↑y * Complex.I‖ ≤ Real.log (t + |y|)

Pointwise lower and upper bounds needed for the endpoint integrals.

theorem Zeta32.Analytic.EnergyI.integral_log_norm_scale {c : ℝ} (hc : 0 < c) (b x : ℝ) : ∫ (t : ℝ) in 0..c * b, Real.log ‖↑t + ↑(c * x) * Complex.I‖ = c * b * Real.log c + c * ∫ (t : ℝ) in 0..b, Real.log ‖↑t + ↑x * Complex.I‖

theorem Zeta32.Analytic.EnergyI.log_norm_sum_comparison (m : ℕ) (y : ℝ) : ∫ (t : ℝ) in 0..↑m, Real.log ‖↑t + ↑y * Complex.I‖ ≤ ∑ i ∈ Finset.range m, Real.log ‖↑(↑i + 3 / 2) + ↑y * Complex.I‖ ∧ ∑ i ∈ Finset.range m, Real.log ‖↑(↑i + 3 / 2) + ↑y * Complex.I‖ ≤ ∫ (t : ℝ) in 3 / 2..↑m + 3 / 2, Real.log ‖↑t + ↑y * Complex.I‖

The shifted samples lie between the two integral bounds. The first comparison uses only positive points inside each open unit cell.

theorem Zeta32.Analytic.EnergyI.log_norm_sum_le_integral_add_error (m : ℕ) (y : ℝ) : ∑ i ∈ Finset.range m, Real.log ‖↑(↑i + 3 / 2) + ↑y * Complex.I‖ ≤ (∫ (t : ℝ) in 0..↑m, Real.log ‖↑t + ↑y * Complex.I‖) + 3 / 2 * Real.log (↑m + 3 / 2 + |y|) + 3 / 2