Research proof index

E_k(it) is real for all t > 0 when k is even and k ≥ 4. This is the generalized theorem from which E₄_imag_axis_real and E₆_imag_axis_real follow.

E₂(it) is real for all t > 0.

E₂ is bounded at infinity. Uses E₂_eq: E₂(z) = 1 - 24·Σₙ₌₁ n·qⁿ/(1-qⁿ) where q = exp(2πiz). For im(z) ≥ 1, |q| ≤ exp(-2π), so by norm_tsum_logDeriv_expo_le, |E₂| ≤ 1 + 24·exp(-2π)/(1-exp(-2π))³.

Bound on the q-series ∑ n·qⁿ/(1-qⁿ) that appears in E₂. For ‖q‖ < 1, we have ‖∑ₙ₌₁ n·qⁿ/(1-qⁿ)‖ ≤ ‖q‖/(1-‖q‖)³. The key estimates are: - |1-qⁿ| ≥ 1-|q|ⁿ ≥ 1-|q| for n ≥ 1 - |n·qⁿ/(1-qⁿ)| ≤ n·|q|ⁿ/(1-|q|) - ∑ n·rⁿ = r/(1-r)², so ∑ n·rⁿ/(1-r) = r/(1-r)³

Monotone version of norm_tsum_logDeriv_expo_le: if ‖q‖ ≤ r < 1, then ‖∑ n·qⁿ/(1-qⁿ)‖ ≤ r/(1-r)³. Useful when we have a uniform bound on ‖q‖.