the proof notes, §5.1: logistic integral representation of U_r.

With t = 1/2 + iy, ρ(y) = (π/2) sech²(πy) and w = 2rρ + iρ' (wfun of Interfaces.lean), integration by parts gives ∫ G(t) w(y) dy = 2r E[G] + E[G'], i.e. U_r(f) = B((tf)') + 2r B(tf) for G = t f. Together with the moments of Contour/Moments.lean this identifies every entry:

∫ (t · t^e R_n)(1/2 + iy) w(y) dy = C_r · slope n e + intercept r n e.

noncomputable def Zeta32.Analytic.Contour.Uint (r : ℚ) (G : ℂ → ℂ) : ℂ

U_r(G) := ∫ G(1/2 + iy) w(y) dy.

Equations

• Zeta32.Analytic.Contour.Uint r G = ∫ (y : ℝ), G (Zeta32.Analytic.Contour.tpt y) * Zeta32.wfun r y

theorem Zeta32.Analytic.Contour.hasDerivAt_tpt (y : ℝ) : HasDerivAt tpt Complex.I y

theorem Zeta32.Analytic.Contour.Uint_eq (r : ℚ) {G G' : ℂ → ℂ} (hG : ∀ (y : ℝ), HasDerivAt G (G' (tpt y)) (tpt y)) (hc' : Continuous fun (y : ℝ) => G' (tpt y)) {C C' : ℝ} {N N' : ℕ} (hb : ∀ (y : ℝ), ‖G (tpt y)‖ ≤ C * (1 + |y|) ^ N) (hb' : ∀ (y : ℝ), ‖G' (tpt y)‖ ≤ C' * (1 + |y|) ^ N') : Uint r G = 2 * ↑r * Erho G + Erho G'

Integration by parts: ∫ G(t) w = 2r E[G] + E[G'].

theorem Zeta32.Analytic.Contour.Erho_const_mul (c : ℂ) (φ : ℂ → ℂ) : (Erho fun (t : ℂ) => c * φ t) = c * Erho φ

theorem Zeta32.Analytic.Contour.norm_pow_tpt_le (m : ℕ) (y : ℝ) : ‖tpt y ^ m‖ ≤ 1 * (1 + |y|) ^ m

theorem Zeta32.Analytic.Contour.Uint_pow (r : ℚ) (m : ℕ) : (Uint r fun (t : ℂ) => t ^ (m + 1)) = ↑(moment r m)

U_r(t^m) = (m+1)B_m + 2r B_{m+1}, i.e. ∫ t^{m+1} w = moment r m.

theorem Zeta32.Analytic.Contour.inv_add_nat_eq_invPow (j : ℕ) (t : ℂ) : (t + ↑j)⁻¹ = invPow j 0 t

theorem Zeta32.Analytic.Contour.norm_inv_add_nat_tpt_le (j : ℕ) (y : ℝ) : ‖(tpt y + ↑j)⁻¹‖ ≤ 2

theorem Zeta32.Analytic.Contour.norm_pole_tpt_le (j : ℕ) (y : ℝ) : ‖tpt y * (tpt y + ↑j)⁻¹‖ ≤ 2 * (1 + |y|) ^ 1

theorem Zeta32.Analytic.Contour.continuous_pole_tpt (j : ℕ) : Continuous fun (y : ℝ) => tpt y * (tpt y + ↑j)⁻¹

theorem Zeta32.Analytic.Contour.Erho_invPow_zero (j : ℕ) : Erho (invPow j 0) = ↑(zeta2val - ↑(H 2 j))

theorem Zeta32.Analytic.Contour.Erho_invPow_one (j : ℕ) : Erho (invPow j 1) = 2 * ↑(zeta3val - ↑(H 3 j))

theorem Zeta32.Analytic.Contour.Uint_pole (r : ℚ) (j : ℕ) : (Uint r fun (t : ℂ) => t * (t + ↑j)⁻¹) = 2 * ↑j * ↑(Cr r) + ↑(beta r j)

U_r((t+j)^{-1}) = 2j C_r + β_j, i.e. ∫ t/(t+j) w = 2j C_r + beta r j.

theorem Zeta32.Analytic.Contour.integrable_pow_wfun (r : ℚ) (m : ℕ) : MeasureTheory.Integrable (fun (y : ℝ) => tpt y ^ m * wfun r y) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.integrable_pole_wfun (r : ℚ) (j : ℕ) : MeasureTheory.Integrable (fun (y : ℝ) => tpt y * (tpt y + ↑j)⁻¹ * wfun r y) MeasureTheory.volume

theorem Zeta32.Analytic.Contour.mul_aeval_eq_sum (q : Polynomial ℚ) (t : ℂ) : t * (Polynomial.aeval t) q = ∑ e ∈ q.support, ↑(q.coeff e) * t ^ (e + 1)

theorem Zeta32.Analytic.logistic_entry_integrand_eq (r : ℚ) (n e : ℕ) (y : ℝ) : Contour.tpt y * (Contour.tpt y ^ e * Rfun n (Contour.tpt y)) * wfun r y = ∑ e' ∈ (polynomialPart n e).support, ↑((polynomialPart n e).coeff e') * (Contour.tpt y ^ (e' + 1) * wfun r y) + ∑ j ∈ Finset.Icc 1 (5 * n), ↑(residue n e j) * (Contour.tpt y * (Contour.tpt y + ↑j)⁻¹ * wfun r y)

The entry integrand, decomposed along the partial fractions of t^e R_n.

theorem Zeta32.Analytic.logistic_integrable_entry (r : ℚ) (n e : ℕ) : MeasureTheory.Integrable (fun (y : ℝ) => Contour.tpt y * (Contour.tpt y ^ e * Rfun n (Contour.tpt y)) * wfun r y) MeasureTheory.volume

theorem Zeta32.Analytic.logistic_representation (r : ℚ) (n e : ℕ) : ∫ (y : ℝ), Contour.tpt y * (Contour.tpt y ^ e * Rfun n (Contour.tpt y)) * wfun r y = ↑(Cr r) * ↑(slope n e) + ↑(intercept r n e)

Entry identity (the proof notes, 5.1): U_r(t^e R_n) = C_r · slope + intercept.