Ramanujan's derivative identities

This file proves Ramanujan's classical derivative identities for the level-one Eisenstein series, using Mathlib's normalized derivative D = (2πi)⁻¹ d/dτ (Derivative.normalizedDerivOfComplex) and Serre derivative Derivative.serreDerivative:

• Chudnovsky.deriv_E2 : D E₂ = (E₂² - E₄) / 12;
• Chudnovsky.deriv_E₄ : D E₄ = (E₂·E₄ - E₆) / 3;
• Chudnovsky.deriv_E₆ : D E₆ = (E₂·E₆ - E₄²) / 2;
• Chudnovsky.deriv_discriminant : D Δ = E₂·Δ (from logDeriv_eta_eq_E2).

The proofs follow the classical finite-dimensionality argument (as in the sphere-packing-lean project referenced by Mathlib's ModularForms/Derivative.lean):

1. For a weight-k level-one modular form f, the Serre derivative ∂ₖ f = D f - (k/12)·E₂·f is a weight-(k+2) level-one modular form. Slash-invariance is checked on the generators S, T of SL(2, ℤ) by differentiating the functional equations f(-1/τ) = τᵏ f(τ) and E₂(-1/τ) = τ²E₂(τ) + 6τ/(πi) (the latter is Mathlib's E2_slash_action); holomorphy is serreDerivative_mdifferentiable; and boundedness at i∞ follows since D f vanishes at i∞ (D f = q·dF/dq where F is the cusp function of f).
2. The spaces M₄, M₆, M₈ of level-one modular forms are one-dimensional, spanned by E₄, E₆, E₄² (Mathlib's LevelOne.DimensionFormula), so each Serre derivative is a scalar multiple of the corresponding basis vector; the scalar is identified by comparing limits at i∞ (E₂, E₄, E₆ → 1 and D f → 0).

Byproducts stated for downstream use (Kummer/PicardFuchs and MainTheorem):

• Chudnovsky.normalizedDeriv_eq_q_mul_deriv_cuspFunction : D f τ = q·F′(q) with F the cusp function — the bridge from τ-derivatives to q-derivatives;
• Chudnovsky.isZeroAtImInfty_normalizedDeriv, Chudnovsky.tendsto_E2_atImInfty, Chudnovsky.tendsto_E₄_atImInfty, Chudnovsky.tendsto_E₆_atImInfty;
• pointwise raw-derivative forms deriv_comp_ofComplex_E2/_E₄/_E₆.

Elementary helpers

theorem Chudnovsky.deriv_eqOn_upperHalfPlaneSet {F G : ℂ → ℂ} (h : Set.EqOn F G UpperHalfPlane.upperHalfPlaneSet) {z : ℂ} (hz : 0 < z.im) : deriv F z = deriv G z

Two functions agreeing on the (open) upper half-plane have the same derivative there.

theorem Chudnovsky.periodic_comp_ofComplex_of_vadd {f : UpperHalfPlane → ℂ} (hf : ∀ (τ : UpperHalfPlane), f (1 +ᵥ τ) = f τ) : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1

A 1-translation-invariant function on ℍ extends to a 1-periodic function on ℂ.

Transformation behaviour of E₂ and of level-one modular forms under T and S

theorem Chudnovsky.E2_slash_T : SlashAction.map 2 ModularGroup.T EisensteinSeries.E2 = EisensteinSeries.E2

theorem Chudnovsky.E2_vadd_one (τ : UpperHalfPlane) : EisensteinSeries.E2 (1 +ᵥ τ) = EisensteinSeries.E2 τ

E₂ is invariant under τ ↦ τ + 1.

theorem Chudnovsky.E2_periodic_comp_ofComplex : Function.Periodic (EisensteinSeries.E2 ∘ ↑UpperHalfPlane.ofComplex) 1

theorem Chudnovsky.E2_S_smul (τ : UpperHalfPlane) : EisensteinSeries.E2 (ModularGroup.S • τ) = ↑τ ^ 2 * EisensteinSeries.E2 τ + 6 / (↑Real.pi * Complex.I) * ↑τ

The S-transformation law of E₂, in a form using only the combination π * I: E₂(-1/τ) = τ²E₂(τ) + 6τ/(πi).

theorem Chudnovsky.modularForm_vadd_one {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (τ : UpperHalfPlane) : f (1 +ᵥ τ) = f τ

Any level-one modular form is invariant under τ ↦ τ + 1.

theorem Chudnovsky.modularForm_S_smul {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (τ : UpperHalfPlane) : f (ModularGroup.S • τ) = ↑τ ^ k * f τ

The S-transformation law of a level-one modular form: f(-1/τ) = τᵏ·f(τ).

Asymptotics of E₂, E₄, E₆ at i∞

theorem Chudnovsky.tendsto_E2_atImInfty : Filter.Tendsto EisensteinSeries.E2 UpperHalfPlane.atImInfty (nhds 1)

E₂ → 1 as Im τ → ∞.

theorem Chudnovsky.isBoundedAtImInfty_E2 : UpperHalfPlane.IsBoundedAtImInfty EisensteinSeries.E2

theorem Chudnovsky.tendsto_valueAtInfty_atImInfty {f : UpperHalfPlane → ℂ} (hper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (hhol : MDiff f) (hbdd : UpperHalfPlane.IsBoundedAtImInfty f) : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds (UpperHalfPlane.valueAtInfty f))

A 1-periodic, holomorphic, bounded function on ℍ tends to its value at i∞.

theorem Chudnovsky.tendsto_E₄_atImInfty : Filter.Tendsto (⇑ModularForm.E₄) UpperHalfPlane.atImInfty (nhds 1)

E₄ → 1 as Im τ → ∞.

theorem Chudnovsky.tendsto_E₆_atImInfty : Filter.Tendsto (⇑ModularForm.E₆) UpperHalfPlane.atImInfty (nhds 1)

E₆ → 1 as Im τ → ∞.

The normalized derivative D via the cusp function

For a 1-periodic, holomorphic, bounded function f on ℍ with cusp function F (so f(τ) = F(q)), we have D f τ = q·F′(q). In particular D f vanishes at i∞.

theorem Chudnovsky.normalizedDeriv_eq_q_mul_deriv_cuspFunction {f : UpperHalfPlane → ℂ} (hper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (hhol : MDiff f) (hbdd : UpperHalfPlane.IsBoundedAtImInfty f) (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex f τ = q τ * deriv (UpperHalfPlane.cuspFunction 1 f) (q τ)

D f τ = q · F′(q) where F = cuspFunction 1 f. This is the bridge between τ-derivatives and q-derivatives, used throughout the q-expansion arguments.

theorem Chudnovsky.isZeroAtImInfty_normalizedDeriv {f : UpperHalfPlane → ℂ} (hper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (hhol : MDiff f) (hbdd : UpperHalfPlane.IsBoundedAtImInfty f) : UpperHalfPlane.IsZeroAtImInfty (Derivative.normalizedDerivOfComplex f)

The normalized derivative of a 1-periodic bounded holomorphic function vanishes at i∞.

theorem Chudnovsky.normalizedDeriv_vadd_one {f : UpperHalfPlane → ℂ} (hper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex f (1 +ᵥ τ) = Derivative.normalizedDerivOfComplex f τ

D f is invariant under τ ↦ τ + 1 when f is 1-periodic.

Behaviour of D under S

theorem Chudnovsky.deriv_comp_ofComplex_S {f : UpperHalfPlane → ℂ} (hhol : MDiff f) {Φ : ℂ → ℂ} (heq : Set.EqOn ((f ∘ ↑UpperHalfPlane.ofComplex) ∘ fun (w : ℂ) => -w⁻¹) Φ UpperHalfPlane.upperHalfPlaneSet) (τ : UpperHalfPlane) : deriv (f ∘ ↑UpperHalfPlane.ofComplex) (-(↑τ)⁻¹) = ↑τ ^ 2 * deriv Φ ↑τ

Differentiating a functional equation along S: if f extends Φ along w ↦ -w⁻¹ on the upper half-plane, then (f ∘ ofComplex)′(-1/τ) = τ² Φ′(τ).

theorem Chudnovsky.normalizedDeriv_S_smul_of_weight {f : UpperHalfPlane → ℂ} (hhol : MDiff f) {m : ℕ} (hfS : ∀ (σ : UpperHalfPlane), f (ModularGroup.S • σ) = ↑σ ^ (m + 1) * f σ) (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex f (ModularGroup.S • τ) = ↑τ ^ (m + 3) * Derivative.normalizedDerivOfComplex f τ + (↑m + 1) * ↑τ ^ (m + 2) * (2 * ↑Real.pi * Complex.I)⁻¹ * f τ

How D f transforms under S for a function of weight m + 1: if f(-1/τ) = τ^(m+1)·f(τ) then (D f)(-1/τ) = τ^(m+3)·D f(τ) + (m+1)·τ^(m+2)·f(τ)/(2πi).

theorem Chudnovsky.normalizedDeriv_E2_S_smul (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex EisensteinSeries.E2 (ModularGroup.S • τ) = ↑τ ^ 4 * Derivative.normalizedDerivOfComplex EisensteinSeries.E2 τ + (↑Real.pi * Complex.I)⁻¹ * ↑τ ^ 3 * EisensteinSeries.E2 τ + 3 * ((↑Real.pi * Complex.I) ^ 2)⁻¹ * ↑τ ^ 2

How D E₂ transforms under S: (D E₂)(-1/τ) = τ⁴·D E₂(τ) + τ³·E₂(τ)/(πi) + 3τ²/(πi)².

The Serre derivatives of E₂, E₄, E₆ as bundled modular forms

The one-dimensionality arguments

theorem Chudnovsky.serreDerivative_E₄_eq : Derivative.serreDerivative 4 ⇑ModularForm.E₄ = fun (τ : UpperHalfPlane) => -3⁻¹ * ModularForm.E₆ τ

The Serre-derivative form of Ramanujan's identity for E₄: D E₄ - (1/3)·E₂·E₄ = -(1/3)·E₆.

theorem Chudnovsky.serreDerivative_E₆_eq : Derivative.serreDerivative 6 ⇑ModularForm.E₆ = fun (τ : UpperHalfPlane) => -2⁻¹ * (ModularForm.E₄ τ * ModularForm.E₄ τ)

The Serre-derivative form of Ramanujan's identity for E₆: D E₆ - (1/2)·E₂·E₆ = -(1/2)·E₄².

theorem Chudnovsky.serreDerivative_E2_eq : Derivative.serreDerivative 1 EisensteinSeries.E2 = fun (τ : UpperHalfPlane) => -12⁻¹ * ModularForm.E₄ τ

The Serre-derivative form of Ramanujan's identity for E₂: D E₂ - (1/12)·E₂² = -(1/12)·E₄.

Ramanujan's identities

theorem Chudnovsky.deriv_E2 (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex EisensteinSeries.E2 τ = (EisensteinSeries.E2 τ ^ 2 - ModularForm.E₄ τ) / 12

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

theorem Chudnovsky.deriv_E₄ (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex (⇑ModularForm.E₄) τ = (EisensteinSeries.E2 τ * ModularForm.E₄ τ - ModularForm.E₆ τ) / 3

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

theorem Chudnovsky.deriv_E₆ (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex (⇑ModularForm.E₆) τ = (EisensteinSeries.E2 τ * ModularForm.E₆ τ - ModularForm.E₄ τ ^ 2) / 2

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

Raw-derivative corollaries

The identities in terms of deriv (f ∘ ofComplex), i.e. d/dτ = 2πi·D, for direct use in chain-rule computations.

theorem Chudnovsky.deriv_comp_ofComplex_E2 (τ : UpperHalfPlane) : deriv (EisensteinSeries.E2 ∘ ↑UpperHalfPlane.ofComplex) ↑τ = ↑Real.pi * Complex.I / 6 * (EisensteinSeries.E2 τ ^ 2 - ModularForm.E₄ τ)

theorem Chudnovsky.deriv_comp_ofComplex_E₄ (τ : UpperHalfPlane) : deriv (⇑ModularForm.E₄ ∘ ↑UpperHalfPlane.ofComplex) ↑τ = 2 * ↑Real.pi * Complex.I / 3 * (EisensteinSeries.E2 τ * ModularForm.E₄ τ - ModularForm.E₆ τ)

theorem Chudnovsky.deriv_comp_ofComplex_E₆ (τ : UpperHalfPlane) : deriv (⇑ModularForm.E₆ ∘ ↑UpperHalfPlane.ofComplex) ↑τ = ↑Real.pi * Complex.I * (EisensteinSeries.E2 τ * ModularForm.E₆ τ - ModularForm.E₄ τ ^ 2)

The discriminant: D Δ = E₂·Δ

theorem Chudnovsky.deriv_discriminant (τ : UpperHalfPlane) : Derivative.normalizedDerivOfComplex ModularForm.discriminant τ = EisensteinSeries.E2 τ * ModularForm.discriminant τ

D Δ = E₂·Δ, from Mathlib's logDeriv_eta_eq_E2 and Δ = η²⁴.