6.1. Required analytic input🔗

Put a = π/4 and g(t) = hardyXi(t)/(t²+1/4). Prove absolute integrability of g(t) cosh(αt) on t ≥ 0 for every 0 ≤ α < a, and prove

F(α) = ∫₀∞ g(t) cosh(αt) dt = π cos(α/2) − π H(α),
H(α) = exp(iα/2) (1/2 + ψ(exp(2iα))).

The right side is real by this identity. One may take its real part throughout. Prove H(a−u) = o(u^N) as u → 0+ for every natural N. The checked sector estimate for ψ supplies the decay bound once the path exp(2iα)−i is shown to approach zero within a closed sector. No derivative estimate is needed. The transform identity and absolute integrability are proved in ThetaInversion.lean and HardyWeight.lean.