Ramanujan's formulas for derivatives of Eisenstein series

We prove Ramanujan's formulas for derivatives of the normalised Eisenstein series E₂, E₄, E₆, in terms of the Serre derivative ∂ₖ = D - (k / 12) E₂ and the normalized derivative D = (2πi)⁻¹ d/dz:

• Derivative.serreDerivative_E₂ : ∂₁ E₂ = -E₄ / 12
• Derivative.serreDerivative_E₄ : ∂₄ E₄ = -E₆ / 3
• Derivative.serreDerivative_E₆ : ∂₆ E₆ = -E₄² / 2
• Derivative.normalizedDerivOfComplex_E₂ : D E₂ = (E₂² - E₄) / 12
• Derivative.normalizedDerivOfComplex_E₄ : D E₄ = (E₂ E₄ - E₆) / 3
• Derivative.normalizedDerivOfComplex_E₆ : D E₆ = (E₂ E₆ - E₄²) / 2

Proof Strategy

Proof uses dimension formula of modular forms of level 1, and the (Serre derivative) identities are obtained by showing that the limit of both sides at i∞ agree.

theorem Derivative.serreDerivative_E₄ : serreDerivative 4 ⇑ModularForm.E₄ = -3⁻¹ • ⇑ModularForm.E₆

Ramanujan's formula for E₄: ∂₄ E₄ = -E₆ / 3.

theorem Derivative.serreDerivative_E₆ : serreDerivative 6 ⇑ModularForm.E₆ = -2⁻¹ • ⇑ModularForm.E₄ ^ 2

Ramanujan's formula for E₆: ∂₆ E₆ = -E₄² / 2.

theorem Derivative.normalizedDerivOfComplex_D2 (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : normalizedDerivOfComplex (EisensteinSeries.D2 γ) = fun (z : UpperHalfPlane) => -↑(↑γ 1 0) ^ 2 / UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ 2

The normalized derivative of the modular defect D2 γ is -(γ₁₀)² / denom γ ².

theorem Derivative.serreDerivative_E₂ : serreDerivative 1 EisensteinSeries.E2 = -12⁻¹ • ⇑ModularForm.E₄

Ramanujan's formula for E₂: ∂₁ E₂ = -E₄ / 12.

Ramanujan's formulas in terms of D

theorem Derivative.normalizedDerivOfComplex_E₂ : normalizedDerivOfComplex EisensteinSeries.E2 = 12⁻¹ • (EisensteinSeries.E2 ^ 2 - ⇑ModularForm.E₄)

Ramanujan's formula for E₂: D E₂ = (E₂² - E₄) / 12.

theorem Derivative.normalizedDerivOfComplex_E₄ : normalizedDerivOfComplex ⇑ModularForm.E₄ = 3⁻¹ • (EisensteinSeries.E2 * ⇑ModularForm.E₄ - ⇑ModularForm.E₆)

Ramanujan's formula for E₄: D E₄ = (E₂ E₄ - E₆) / 3.

theorem Derivative.normalizedDerivOfComplex_E₆ : normalizedDerivOfComplex ⇑ModularForm.E₆ = 2⁻¹ • (EisensteinSeries.E2 * ⇑ModularForm.E₆ - ⇑ModularForm.E₄ ^ 2)

Ramanujan's formula for E₆: D E₆ = (E₂ E₆ - E₄²) / 2.