Research proof index

For a strictly monotonic function f : ℕ → ℕ with f 0 = 0, f (segment f k) ≤ k for all k : ℕ.

For a strictly monotonic function f : ℕ → ℕ, segment' f and segment f are actually equal.

For $0\le t\le1$, the reciprocal of $1-2^{-t}$ is controlled in the extended nonnegative reals by

$(1-2^{-t})^{-1}\le 2t^{-1}.$

If g(t₀) = 0 and deriv g t₀ < 0, then g is negative shortly after t₀.

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