Derivatives of modular forms

This file defines normalized derivative $D = \frac{1}{2\pi i} \frac{d}{dz}$ and (Ramanujan-)Serre derivative $\partial_k := D - \frac{k}{12} E_2$ of modular forms.

Main Definitions and Theorems

• normalizedDerivOfComplex: $D = \frac{1}{2\pi i} \frac{d}{dz}$
• serreDerivative: $\partial_k F := D F - \frac{k}{12} E_2 F$
• serreDerivative_slash_equivariant: Serre derivative is equivariant under the slash action.
• serreDerivativeMF: the Serre derivative preserves modularity, i.e. for a subgroup Γ of SL(2, ℤ) it maps a weight k level Γ modular form to a weight k + 2 level Γ modular form.

TODO:

• Use the above to prove Ramanujan's identities. See here for sorry-free proofs.

noncomputable def Derivative.normalizedDerivOfComplex (F : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℂ

Normalized derivative $D = \frac{1}{2\pi i} \frac{d}{dz}$.

Equations

• Derivative.normalizedDerivOfComplex F z = (2 * ↑Real.pi * Complex.I)⁻¹ * deriv (F ∘ ↑UpperHalfPlane.ofComplex) ↑z

def Derivative.termD : Lean.ParserDescr

We denote the normalized derivative by D.

Equations

• Derivative.termD = Lean.ParserDescr.node `Derivative.termD 1024 (Lean.ParserDescr.symbol "D")

theorem Derivative.normalizedDerivOfComplex_mdifferentiable {F : UpperHalfPlane → ℂ} (hF : MDiff F) : MDiff (normalizedDerivOfComplex F)

The derivative operator D preserves MDifferentiability. If F : ℍ → ℂ is MDifferentiable, then D F is also MDifferentiable.

Basic properties of normalized derivative.

@[simp]

theorem Derivative.normalizedDerivOfComplex_add (F G : UpperHalfPlane → ℂ) (hF : MDiff F) (hG : MDiff G) : normalizedDerivOfComplex (F + G) = normalizedDerivOfComplex F + normalizedDerivOfComplex G

@[simp]

theorem Derivative.normalizedDerivOfComplex_sub (F G : UpperHalfPlane → ℂ) (hF : MDiff F) (hG : MDiff G) : normalizedDerivOfComplex (F - G) = normalizedDerivOfComplex F - normalizedDerivOfComplex G

@[simp]

theorem Derivative.normalizedDerivOfComplex_const (c : ℂ) : (normalizedDerivOfComplex fun (x : UpperHalfPlane) => c) = 0

@[simp]

theorem Derivative.normalizedDerivOfComplex_smul (c : ℂ) (F : UpperHalfPlane → ℂ) (hF : MDiff F) : normalizedDerivOfComplex (c • F) = c • normalizedDerivOfComplex F

@[simp]

theorem Derivative.normalizedDerivOfComplex_neg (F : UpperHalfPlane → ℂ) (hF : MDiff F) : normalizedDerivOfComplex (-F) = -normalizedDerivOfComplex F

@[simp]

theorem Derivative.normalizedDerivOfComplex_mul (F G : UpperHalfPlane → ℂ) (hF : MDiff F) (hG : MDiff G) : normalizedDerivOfComplex (F * G) = normalizedDerivOfComplex F * G + F * normalizedDerivOfComplex G

@[simp]

theorem Derivative.normalizedDerivOfComplex_pow (F : UpperHalfPlane → ℂ) (n : ℕ) (hF : MDiff F) : normalizedDerivOfComplex (F ^ n) = ↑n * F ^ (n - 1) * normalizedDerivOfComplex F

noncomputable def Derivative.serreDerivative (k : ℂ) (F : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℂ

Serre derivative of weight $k$.

Equations

• Derivative.serreDerivative k F z = Derivative.normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z

@[simp]

theorem Derivative.serreDerivative_apply (k : ℂ) (F : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : serreDerivative k F z = normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z

@[simp]

theorem Derivative.serreDerivative_eq (k : ℂ) (F : UpperHalfPlane → ℂ) : serreDerivative k F = fun (z : UpperHalfPlane) => normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z

Basic properties of Serre derivative.

theorem Derivative.serreDerivative_add (k : ℂ) (F G : UpperHalfPlane → ℂ) (hF : MDiff F) (hG : MDiff G) : serreDerivative k (F + G) = serreDerivative k F + serreDerivative k G

theorem Derivative.serreDerivative_sub (k : ℂ) (F G : UpperHalfPlane → ℂ) (hF : MDiff F) (hG : MDiff G) : serreDerivative k (F - G) = serreDerivative k F - serreDerivative k G

theorem Derivative.serreDerivative_smul (k c : ℂ) (F : UpperHalfPlane → ℂ) (hF : MDiff F) : serreDerivative k (c • F) = c • serreDerivative k F

theorem Derivative.serreDerivative_mul (k₁ k₂ : ℂ) (F G : UpperHalfPlane → ℂ) (hF : MDiff F) (hG : MDiff G) : serreDerivative (k₁ + k₂) (F * G) = serreDerivative k₁ F * G + F * serreDerivative k₂ G

theorem Derivative.serreDerivative_mdifferentiable {F : UpperHalfPlane → ℂ} (k : ℂ) (hF : MDiff F) : MDiff (serreDerivative k F)

The Serre derivative preserves MDifferentiability. If F : ℍ → ℂ is MDifferentiable, then serreDerivative k F is also MDifferentiable.

theorem Derivative.normalizedDerivOfComplex_slash {k : ℤ} {F : UpperHalfPlane → ℂ} (hF : MDiff F) {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) : normalizedDerivOfComplex (SlashAction.map k g F) = fun (z : UpperHalfPlane) => (↑(↑g).det)⁻¹ * SlashAction.map (k + 2) g (normalizedDerivOfComplex F) z - ↑k * (2 * ↑Real.pi * Complex.I)⁻¹ * (↑(↑g 1 0) / UpperHalfPlane.denom g ↑z) * SlashAction.map k g F z

How D interacts with the slash action.

theorem Derivative.normalizedDerivOfComplex_SL_slash {k : ℤ} {F : UpperHalfPlane → ℂ} (hF : MDiff F) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} : normalizedDerivOfComplex (SlashAction.map k γ F) = SlashAction.map (k + 2) γ (normalizedDerivOfComplex F) - fun (z : UpperHalfPlane) => ↑k * (2 * ↑Real.pi * Complex.I)⁻¹ * (↑(↑γ 1 0) / UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) * SlashAction.map k γ F z

The SL(2, ℤ) case of normalizedDerivOfComplex_slash, where the determinant factor is 1.

theorem Derivative.serreDerivative_slash_equivariant {k : ℤ} {F : UpperHalfPlane → ℂ} (hF : MDiff F) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} : SlashAction.map (k + 2) γ (serreDerivative (↑k) F) = serreDerivative (↑k) (SlashAction.map k γ F)

Serre derivative is equivariant under the slash action. More precisely, $\partial_k (F ∣[k] γ) = (\partial_k F) ∣[k + 2] \gamma$ for all $\gamma \in SL(2, \mathbb{Z})$.

theorem Derivative.serreDerivative_slash_invariant {k : ℤ} {F : UpperHalfPlane → ℂ} (hF : MDiff F) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (h : SlashAction.map k γ F = F) : SlashAction.map (k + 2) γ (serreDerivative (↑k) F) = serreDerivative (↑k) F

As a corollary, if F is invariant under the slash action of weight k, then serreDerivative k F is invariant under the slash action of weight k + 2.

Boundedness of the normalized derivative and Serre derivative at infinity.

theorem Derivative.isBoundedAtImInfty_normalizedDerivOfComplex {F : UpperHalfPlane → ℂ} (hF : MDiff F) (hb : UpperHalfPlane.IsBoundedAtImInfty F) : UpperHalfPlane.IsBoundedAtImInfty (normalizedDerivOfComplex F)

The normalized derivative D F of a holomorphic function F that is bounded at infinity is again bounded at infinity. This is a Cauchy estimate: differentiating loses at most a factor of 1 / z.im.

theorem Derivative.isBoundedAtImInfty_serreDerivative {F : UpperHalfPlane → ℂ} (k : ℂ) (hF : MDiff F) (hb : UpperHalfPlane.IsBoundedAtImInfty F) : UpperHalfPlane.IsBoundedAtImInfty (serreDerivative k F)

The Serre derivative of a holomorphic function that is bounded at infinity is again bounded at infinity.

noncomputable def Derivative.serreDerivativeMF {Γ : Subgroup (GL (Fin 2) ℝ)} (k : ℤ) (f : ModularForm Γ k) (hΓ : Γ ≤ (Matrix.SpecialLinearGroup.mapGL ℝ).range := by rfl) : ModularForm Γ (k + 2)

The Serre derivative preserves modularity: if f is a modular form of weight k for a subgroup Γ of SL(2, ℤ), then ∂ₖ f is a modular form of weight k + 2 for Γ.

Equations

• Derivative.serreDerivativeMF k f hΓ = { toFun := Derivative.serreDerivative ↑k ⇑f, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem Derivative.coe_serreDerivativeMF {Γ : Subgroup (GL (Fin 2) ℝ)} (k : ℤ) (f : ModularForm Γ k) (hΓ : Γ ≤ (Matrix.SpecialLinearGroup.mapGL ℝ).range) : ⇑(serreDerivativeMF k f hΓ) = serreDerivative ↑k ⇑f