Definition of (Serre) derivative of modular forms. Prove Ramanujan's formulas on derivatives of Eisenstein series.
TODO: Remove this or move this to somewhere more appropriate.
The converse direction: DifferentiableAt on ℂ implies MDifferentiableAt on ℍ.
The derivative operator D preserves MDifferentiability.
If F : ℍ → ℂ is MDifferentiable, then D F is also MDifferentiable.
TODO: Move this to E2.lean.
Basic properties of derivatives: linearity, Leibniz rule, etc.
Termwise differentiation of q-series (Lemma 6.45) #
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 nat_pos_tsum2 to convert between sums,
then applies D_qexp_tsum.
Basic properties of Serre derivative: linearity, Leibniz rule, etc.
The Serre derivative preserves MDifferentiability.
If F : ℍ → ℂ is MDifferentiable, then serre_D k F is also MDifferentiable.
Helper lemmas for D_slash #
These micro-lemmas compute derivatives of the components in the slash action formula.
Derivative of the denominator function: d/dz[cz + d] = c.
Derivative of the numerator function: d/dz[az + b] = a.
Differentiability of denom.
Differentiability of num.
Derivative of the Möbius transformation: d/dz[(az+b)/(cz+d)] = 1/(cz+d)². Uses det(γ) = 1: a(cz+d) - c(az+b) = ad - bc = 1.
Derivative of denom^(-k): d/dz[(cz+d)^(-k)] = -k * c * (cz+d)^(-k-1).
The derivative anomaly: how D interacts with the slash action. This is the key computation for proving Serre derivative equivariance.
Serre derivative is equivariant under the slash action. More precisely, if F is invariant
under the slash action of weight k, then serre_D k F is invariant under the slash action
of weight k + 2.
Chain rule for restriction to imaginary axis: d/dt F(it) = -2π * (D F)(it).
This connects the real derivative along the imaginary axis to the normalized derivative D. The key computation is:
- The imaginary axis is parametrized by g(t) = I * t
- By chain rule: d/dt F(it) = (dF/dz)(it) · (d/dt)(it) = F'(it) · I
- Since D = (2πi)⁻¹ · d/dz, we have F' = 2πi · D F
- So d/dt F(it) = 2πi · D F(it) · I = -2π · D F(it)
If $F$ is a modular form where $F(it)$ is positive for sufficiently large $t$ (i.e. constant term is positive) and the derivative is positive, then $F$ is also positive.
Let $F : \mathbb{H} \to \mathbb{C}$ be a holomorphic function where $F(it)$ is real for all $t > 0$. Assume that Serre derivative $\partial_k F$ is positive on the imaginary axis. If $F(it)$ is positive for sufficiently large $t$, then $F(it)$ is positive for all $t > 0$.