Research proof index

The real part of negDE₂(it) is positive for t > 0.

Q-expansion identity: negDE₂ = 24 * ∑ n * σ₁(n) * q^n From Ramanujan's formula: D E₂ = (E₂² - E₄)/12, so -D E₂ = (E₄ - E₂²)/12. And the derivative of E₂ = 1 - 24∑ σ₁(n) q^n gives -D E₂ = 24 ∑ n σ₁(n) q^n. See blueprint equation at line 136 of modform-ineq.tex. Proof outline: 1. E₂_sigma_qexp: E₂ = 1 - 24 * ∑ σ₁(n) * q^n 2. D_qexp_tsum_pnat: D(∑ a(n) * q^n...

Each term n*σ₁(n)*exp(-2πnt) in the q-expansion of negDE₂ has positive real part.

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‖.

If g is continuous on (0, ∞), positive for t ≥ t₀, and has strictly negative derivative at any zero in (0, t₀), then g is positive on all of (0, ∞).