Research proof index

Lemma 6.45 (Blueprint): $D$ commutes with tsum for $q$-series. If F(z) = Σ a(n)·qⁿ where q = exp(2πiz), then D F(z) = Σ n·a(n)·qⁿ. More precisely, this lemma shows that for a ℕ-indexed q-series with summable coefficients satisfying appropriate derivative bounds, D acts termwise by multiplying coefficients by n.

Simplified version of D_qexp_tsum for ℕ+-indexed series (starting from n=1). This is the form most commonly used for Eisenstein series q-expansions. Thin layer implementation: Extends a : ℕ+ → ℂ to ℕ → ℂ with a' 0 = 0, uses tsum_pNat and summable_pnat_iff_summable_nat to convert between sums, then applies D_qexp_tsum.

If F is real on the imaginary axis and MDifferentiable, then D F is also real on the imaginary axis.

The derivative anomaly: how D interacts with the slash action. This is the key computation for proving Serre derivative equivariance.

The D-derivative of a bounded holomorphic function tends to zero at infinity. For z with im(z) = y, a Cauchy estimate on a ball of radius y/2 gives ‖D f z‖ ≤ M / (π · y), which tends to zero as y → ∞.

Derivative of denom^(-k): d/dz[(cz+d)^(-k)] = -k * c * (cz+d)^(-k-1).