Sphere Packing in Dimension 8

The D-derivative of the anomaly function D₂. D₂ γ z = 2πi · (γ₁₀ / denom γ z), so D(D₂ γ) = (2πi)⁻¹ · d/dz[2πi · c / denom] = -c² / denom²

D(E₂E₄ - E₆) = 720 * ∑ n²·σ₃(n)·qⁿ. Key for the log-derivative limit: (D F)/F → 2 as z → i∞.

The D-derivative is bounded at infinity for bounded holomorphic functions. For y large (y ≥ 2·max(A,0) + 1), we use a ball of radius z.im/2 around z. The ball lies in the upper half plane, f is bounded by M on it, and norm_D_le_of_sphere_bound gives ‖D f z‖ ≤ M/(π·z.im) ≤ M/π.

Lemma 6.45 (Blueprint): The normalized derivative $D$ acts as $q \frac{d}{dq}$ on $q$-series. For a single q-power term: D(a·qⁿ) = n·a·qⁿ where q = exp(2πiz) and n ∈ ℤ. The key calculation: - d/dz(exp(2πinz)) = 2πin·exp(2πinz) - D(exp(2πinz)) = (2πi)⁻¹·(2πin·exp(2πinz)) = n·exp(2πinz)

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.