Definition of (Serre) derivative of modular forms. Prove Ramanujan's formulas on derivatives of Eisenstein series.

noncomputable def D (F : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

Equations

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

theorem MDifferentiableAt_DifferentiableAt {F : UpperHalfPlane → ℂ} {z : UpperHalfPlane} (h : MDifferentiableAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F z) : DifferentiableAt ℂ (F ∘ ↑UpperHalfPlane.ofComplex) ↑z

TODO: Remove this or move this to somewhere more appropriate.

theorem E₂_holo' : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) E₂

TODO: Move this to E2.lean.

@[simp]

theorem D_add (F G : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (hG : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) G) : D (F + G) = D F + D G

Basic properties of derivatives: linearity, Leibniz rule, etc.

@[simp]

theorem D_sub (F G : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (hG : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) G) : D (F - G) = D F - D G

@[simp]

theorem D_smul (c : ℂ) (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) : D (c • F) = c • D F

@[simp]

theorem D_mul (F G : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (hG : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) G) : D (F * G) = F * D G + D F * G

@[simp]

theorem D_sq (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) : D (F ^ 2) = 2 * F * D F

@[simp]

theorem D_cube (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) : D (F ^ 3) = 3 * F ^ 2 * D F

@[simp]

theorem D_const (c : ℂ) (z : UpperHalfPlane) : D (Function.const UpperHalfPlane c) z = 0

noncomputable def serre_D (k : ℂ) : (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ

Serre derivative of weight $k$. Note that the definition makes sense for any analytic function $F : \mathbb{H} \to \mathbb{C}$.

Equations

• serre_D k F z = D F z - k * 12⁻¹ * E₂ z * F z

theorem serre_D_add (k : ℤ) (F G : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (hG : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) G) : serre_D (↑k) (F + G) = serre_D (↑k) F + serre_D (↑k) G

Basic properties of Serre derivative: linearity, Leibniz rule, etc.

theorem serre_D_smul (k : ℤ) (c : ℂ) (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (z : UpperHalfPlane) : serre_D (↑k) (c • F) z = c * serre_D (↑k) F z

theorem serre_D_mul (k₁ k₂ : ℤ) (F G : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (hG : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) G) (z : UpperHalfPlane) : serre_D (↑k₁ + ↑k₂) (F * G) z = F z * serre_D (↑k₁) G z + G z * serre_D (↑k₂) F z

theorem serre_D_slash_equivariant (k : ℤ) (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map (k + 2) γ (serre_D (↑k) F) = serre_D (↑k) (SlashAction.map k γ F)

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.

theorem serre_D_slash_invariant (k : ℤ) (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (h : SlashAction.map k γ F = F) : SlashAction.map (k + 2) γ (serre_D (↑k) F) = serre_D (↑k) F

theorem ramanujan_E₂' : serre_D 1 E₂ = -12⁻¹ * E₄.toFun

Serre derivative of Eisenstein series. Use serre_D_slash_invariant and compare constant terms. Note that the dimensions of the spaces of modular forms are all 1.

theorem ramanujan_E₄' : serre_D 4 E₄.toFun = -3⁻¹ * E₆.toFun

theorem ramanujan_E₆' : serre_D 6 E₆.toFun = -2⁻¹ * E₄.toFun * E₄.toFun

@[simp]

theorem ramanujan_E₂ : D E₂ = 12⁻¹ * (E₂ * E₂ - E₄.toFun)

@[simp]

theorem ramanujan_E₄ : D E₄.toFun = 3⁻¹ * (E₂ * E₄.toFun - E₆.toFun)

@[simp]

theorem ramanujan_E₆ : D E₆.toFun = 2⁻¹ * (E₂ * E₆.toFun - E₄.toFun * E₄.toFun)

noncomputable def X₄₂ : UpperHalfPlane → ℂ

Prove modular linear differential equation satisfied by $F$.

Equations

• X₄₂ = 288⁻¹ * (E₄.toFun - E₂ * E₂)

noncomputable def Δ_fun : UpperHalfPlane → ℂ

Equations

• Δ_fun = 1728⁻¹ * (E₄.toFun ^ 3 - E₆.toFun ^ 2)

noncomputable def F : UpperHalfPlane → ℂ

Equations

• F = (E₂ * E₄.toFun - E₆.toFun) ^ 2

theorem F_aux : D F = 5 * 6⁻¹ * E₂ ^ 3 * E₄.toFun ^ 2 - 5 * 2⁻¹ * E₂ ^ 2 * E₄.toFun * E₆.toFun + 5 * 6⁻¹ * E₂ * E₄.toFun ^ 3 + 5 * 3⁻¹ * E₂ * E₆.toFun ^ 2 - 5 * 6⁻¹ * E₄.toFun ^ 2 * E₆.toFun

theorem MLDE_F : serre_D 12 (serre_D 10 F) = 5 * 6⁻¹ * F + 172800 * Δ_fun * X₄₂

Modular linear differential equation satisfied by F. TODO: Move this to a more appropriate place.

theorem antiDerPos {F : UpperHalfPlane → ℂ} {k : ℤ} (hF : ResToImagAxis.EventuallyPos F) (hDF : ResToImagAxis.Pos (D F)) : ResToImagAxis.Pos F

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.

theorem antiSerreDerPos {F : UpperHalfPlane → ℂ} {k : ℤ} (hSDF : ResToImagAxis.Pos (serre_D (↑k) F)) (hF : ResToImagAxis.EventuallyPos F) : ResToImagAxis.Pos F

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$.