Derivatives of modular forms

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

TODO:

• Serre derivative preserves modularity, i.e. $\partial_k (M_k) \subseteq M_{k+2}$.
• Use above, 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}$.

def Derivative.termD : Lean.ParserDescr

We denote the normalized derivative by 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$.

@[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.