Research proof index

Derivative bounds for q-expansion coefficients. Given ‖a n‖ ≤ n^k, produces bounds ‖a n * 2πin * exp(2πin z)‖ ≤ 2π * n^(k+1) * exp(-2πn * y_min) on compact K ⊆ {z : 0 < z.im}. This is a key hypothesis for D_qexp_tsum_pnat.

Serre derivative of E₆: serre_D 6 E₆ = - 2⁻¹ * E₄². Uses the dimension argument: 1. serre_D 6 E₆ is weight-8 slash-invariant (by serre_D_slash_invariant) 2. Weight-8 modular forms are 1-dimensional, spanned by E₄² 3. Constant term is -1/2 (from D E₆ → 0, E₂ → 1, E₆ → 1)

For any function F : ℍ → ℂ and t > 0, F.resToImagAxis (1/t) = F(S • (I*t)).

Real part of a product on the imaginary axis is the product of real parts, when both factors are real-valued there.

Restriction and slash action under S: $(F |_k S) (it) = (it)^{-k} * F(it)$

The Serre derivative of a bounded holomorphic function is bounded at infinity. serre_D k f = D f - (k/12)·E₂·f. Both terms are bounded: - D f is bounded by D_isBoundedAtImInfty_of_bounded - (k/12)·E₂·f is bounded since E₂ and f are bounded