Constant Pi functions (numeric literals) are MDifferentiable.
Inverse of a constant Pi function (e.g. 6⁻¹ : ℍ → ℂ) is MDifferentiable.
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.
Division of MDifferentiable functions on ℍ is MDifferentiable, when the denominator is everywhere nonzero.
Normalize a numeric literal (n : ℍ → ℂ) to Function.const ℍ n so D_const fires.
Normalize (Function.const ℍ c)⁻¹ to Function.const ℍ c⁻¹ so D_const fires.
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 real on the imaginary axis and MDifferentiable, then D F is also real on the imaginary axis.
The real part of F.resToImagAxis has derivative -2π * ((D F).resToImagAxis t).re at t.
If F is MDifferentiable and antitone on the imaginary axis, then D F has non-negative real part on the imaginary axis.
If F is real on the imaginary axis, MDifferentiable, and has strictly negative derivative on the imaginary axis, then D F is positive on the imaginary axis.
Note: StrictAntiOn is NOT sufficient - a strictly decreasing function can have deriv = 0
at isolated points (e.g., -x³ at x=0). Use this theorem when you can prove the derivative
is strictly negative, typically from q-expansion analysis.
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$.
Cauchy Estimates for D-derivative #
Infrastructure for bounding derivatives using Cauchy estimates on disks in the upper half plane.
If f : ℍ → ℂ is MDifferentiable and a closed disk in ℂ lies in the upper
half-plane, then f ∘ ofComplex is DiffContOnCl on the corresponding open disk.
Closed ball centered at z with radius z.im/2 is contained in the upper half plane.
Cauchy estimate for the D-derivative: if f ∘ ofComplex is holomorphic on a disk
of radius r around z and bounded by M on the boundary sphere,
then ‖D f z‖ ≤ M / (2πr).
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/π.
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 → ∞.
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
A level-1 modular form is invariant under slash action by any element of SL(2,ℤ).
The Serre derivative of a weight-k level-1 modular form is a weight-(k+2) modular form.
Equations
- serre_D_ModularForm k f = { toFun := serre_D ↑k ⇑f, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }