Derivatives of the Jacobi theta functions

This file proves the Serre derivative identities for the Jacobi theta functions H₂, H₃, H₄ (Blueprint Proposition 6.52, equations (32)–(34)).

Main results

• serre_D_H₂ : serre_D 2 H₂ = (1/6) * (H₂ ^ 2 + 2 * H₂ * H₄)
• serre_D_H₃ : serre_D 2 H₃ = (1/6) * (H₂ ^ 2 - H₄ ^ 2)
• serre_D_H₄ : serre_D 2 H₄ = -(1/6) * (2 * H₂ * H₄ + H₄ ^ 2)
• D_H₂, D_H₃, D_H₄ : the corresponding formulas for the ordinary derivative D
• E₄_eq_H_sum_sq : E₄ = H₂ ^ 2 + H₂ * H₄ + H₄ ^ 2

Proof strategy

Let f₂, f₃, f₄ be the differences of the two sides of the three Serre derivative identities. The Jacobi identity gives f₂ + f₄ = f₃, and the transformation rules of H₂, H₃, H₄ under the generators S, T of SL(2, ℤ) yield f₂ ∣[4] S = -f₄, f₂ ∣[4] T = -f₂, f₄ ∣[4] S = -f₂, f₄ ∣[4] T = f₃. Hence

• theta_g = (2 * H₂ + H₄) * f₂ + (H₂ + 2 * H₄) * f₄ (weight 6) and
• theta_h = f₂ ^ 2 + f₂ * f₄ + f₄ ^ 2 (weight 8)

are SL(2, ℤ)-invariant. They vanish at infinity, so they are level-1 cusp forms of weight less than 12, hence zero. From theta_g = theta_h = 0 we deduce f₂ = f₃ = f₄ = 0.

The error terms f₂, f₃, f₄

noncomputable def f₂ : UpperHalfPlane → ℂ

Error term for the ∂₂H₂ identity: f₂ = ∂₂H₂ - (1/6)(H₂² + 2H₂H₄)

Equations

• f₂ = serre_D 2 H₂ - (1 / 6) • (H₂ * (H₂ + 2 • H₄))

noncomputable def f₃ : UpperHalfPlane → ℂ

Error term for the ∂₂H₃ identity: f₃ = ∂₂H₃ - (1/6)(H₂² - H₄²)

Equations

• f₃ = serre_D 2 H₃ - (1 / 6) • (H₂ ^ 2 - H₄ ^ 2)

noncomputable def f₄ : UpperHalfPlane → ℂ

Error term for the ∂₂H₄ identity: f₄ = ∂₂H₄ + (1/6)(2H₂H₄ + H₄²)

Equations

• f₄ = serre_D 2 H₄ + (1 / 6) • (H₄ * (2 • H₂ + H₄))

theorem f₂_decompose : f₂ = serre_D (↑2) H₂ + (-1 / 6) • (H₂ * (H₂ + 2 • H₄))

f₂ decomposes as serre_D 2 H₂ + (-1/6) • (H₂ * (H₂ + 2*H₄))

theorem f₄_decompose : f₄ = serre_D (↑2) H₄ + (1 / 6) • (H₄ * (2 • H₂ + H₄))

f₄ decomposes as serre_D 2 H₄ + (1/6) • (H₄ * (2*H₂ + H₄))

theorem f₂_MDifferentiable : MDiff f₂

f₂ is MDifferentiable

theorem f₃_MDifferentiable : MDiff f₃

f₃ is MDifferentiable

theorem f₄_MDifferentiable : MDiff f₄

f₄ is MDifferentiable

theorem f₂_add_f₄_eq_f₃ : f₂ + f₄ = f₃

The error terms satisfy f₂ + f₄ = f₃, by the Jacobi identity H₂ + H₄ = H₃.

Transformation of the error terms under S and T

The transformation rules follow from serre_D_slash_equivariant together with the S/T-transformation rules of H₂, H₃, H₄.

theorem f₂_S_action : SlashAction.map 4 ModularGroup.S f₂ = -f₄

f₂ transforms under S as f₂ ∣[4] S = -f₄.

theorem f₂_T_action : SlashAction.map 4 ModularGroup.T f₂ = -f₂

f₂ transforms under T as f₂ ∣[4] T = -f₂.

theorem f₄_S_action : SlashAction.map 4 ModularGroup.S f₄ = -f₂

f₄ transforms under S as f₄ ∣[4] S = -f₂.

theorem f₄_T_action : SlashAction.map 4 ModularGroup.T f₄ = f₃

f₄ transforms under T as f₄ ∣[4] T = f₃.

The invariants theta_g and theta_h

noncomputable def theta_g : UpperHalfPlane → ℂ

Level-1 invariant of weight 6: g = (2H₂ + H₄)f₂ + (H₂ + 2H₄)f₄

Equations

• theta_g = (2 • H₂ + H₄) * f₂ + (H₂ + 2 • H₄) * f₄

noncomputable def theta_h : UpperHalfPlane → ℂ

Level-1 invariant of weight 8: h = f₂² + f₂f₄ + f₄²

Equations

• theta_h = f₂ ^ 2 + f₂ * f₄ + f₄ ^ 2

theorem theta_g_S_action : SlashAction.map 6 ModularGroup.S theta_g = theta_g

theta_g is invariant under S.

theorem theta_g_T_action : SlashAction.map 6 ModularGroup.T theta_g = theta_g

theta_g is invariant under T.

theorem theta_h_S_action : SlashAction.map 8 ModularGroup.S theta_h = theta_h

theta_h is invariant under S.

theorem theta_h_T_action : SlashAction.map 8 ModularGroup.T theta_h = theta_h

theta_h is invariant under T.

Vanishing of theta_g and theta_h

Both invariants extend to cusp forms of level 1 and weight less than 12, hence vanish.

theorem theta_g_MDifferentiable : MDiff theta_g

theta_g is MDifferentiable

theorem theta_h_MDifferentiable : MDiff theta_h

theta_h is MDifferentiable

theorem theta_g_slash_invariant_GL (γ : GL (Fin 2) ℝ) : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1) → SlashAction.map 6 γ theta_g = theta_g

theta_g is slash-invariant under Γ(1) in GL₂(ℝ) form

theorem theta_h_slash_invariant_GL (γ : GL (Fin 2) ℝ) : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1) → SlashAction.map 8 γ theta_h = theta_h

theta_h is slash-invariant under Γ(1) in GL₂(ℝ) form

noncomputable def theta_g_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6

theta_g as a SlashInvariantForm of level 1

Equations

• theta_g_SIF = { toFun := theta_g, slash_action_eq' := theta_g_slash_invariant_GL }

noncomputable def theta_h_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 8

theta_h as a SlashInvariantForm of level 1

Equations

• theta_h_SIF = { toFun := theta_h, slash_action_eq' := theta_h_slash_invariant_GL }

theorem f₂_tendsto_atImInfty : Filter.Tendsto f₂ UpperHalfPlane.atImInfty (nhds 0)

f₂ tends to 0 at infinity, since H₂ → 0.

theorem f₄_tendsto_atImInfty : Filter.Tendsto f₄ UpperHalfPlane.atImInfty (nhds 0)

f₄ tends to 0 at infinity: serre_D 2 H₄ → -1/6 cancels against (1/6) * H₄ * (2 * H₂ + H₄) → 1/6.

theorem theta_g_tendsto_atImInfty : Filter.Tendsto theta_g UpperHalfPlane.atImInfty (nhds 0)

theta_g tends to 0 at infinity.

theorem theta_h_tendsto_atImInfty : Filter.Tendsto theta_h UpperHalfPlane.atImInfty (nhds 0)

theta_h tends to 0 at infinity.

theorem theta_g_eq_zero : theta_g = 0

theta_g = 0, since level-1 cusp forms of weight 6 vanish.

theorem theta_h_eq_zero : theta_h = 0

theta_h = 0, since level-1 cusp forms of weight 8 vanish.

The identity E₄ = H₂² + H₂H₄ + H₄²

E₄ and H_sum_sq = H₂ ^ 2 + H₂ * H₄ + H₄ ^ 2 are weight-4 level-1 modular forms tending to 1 at infinity, so their difference is a cusp form of weight 4, hence zero.

noncomputable def H_sum_sq : UpperHalfPlane → ℂ

H₂² + H₂H₄ + H₄²

Equations

• H_sum_sq z = H₂ z ^ 2 + H₂ z * H₄ z + H₄ z ^ 2

theorem H_sum_sq_MDifferentiable : MDiff H_sum_sq

H_sum_sq is MDifferentiable

theorem H_sum_sq_tendsto : Filter.Tendsto H_sum_sq UpperHalfPlane.atImInfty (nhds 1)

H_sum_sq → 1 at infinity

theorem H_sum_sq_ne_zero : H_sum_sq ≠ 0

H_sum_sq ≠ 0 (since it tends to 1 ≠ 0)

theorem three_H_sum_sq_ne_zero : (fun (z : UpperHalfPlane) => 3 * H_sum_sq z) ≠ 0

3 * H_sum_sq ≠ 0

theorem three_H_sum_sq_MDifferentiable : MDiff fun (z : UpperHalfPlane) => 3 * H_sum_sq z

3 * H_sum_sq is MDifferentiable

theorem E₄_eq_H_sum_sq : E₄.toFun = H_sum_sq

E₄ = H₂ ^ 2 + H₂ * H₄ + H₄ ^ 2.

Vanishing of the error terms

theorem f₄_sq_mul_eq (z : UpperHalfPlane) (hg_z : theta_g z = 0) : f₄ z ^ 2 * (3 * H_sum_sq z) = (2 * H₂ z + H₄ z) ^ 2 * theta_h z

The algebraic identity behind f₂_eq_zero: with A = 2H₂ + H₄ and B = H₂ + 2H₄, the relation A * f₂ + B * f₄ = 0 gives f₄ ^ 2 * (A ^ 2 - A * B + B ^ 2) = A ^ 2 * theta_h.

theorem f₂_eq_zero : f₂ = 0

f₂ = 0: from theta_g = theta_h = 0 we get f₄ ^ 2 * (3 * H_sum_sq) = 0, and since H_sum_sq ≠ 0 this forces f₄ = 0, whence f₂ = 0 from theta_h = f₂ ^ 2 = 0.

theorem f₄_eq_zero : f₄ = 0

f₄ = 0, from f₂ = 0 and theta_h = 0.

theorem f₃_eq_zero : f₃ = 0

f₃ = 0, since f₃ = f₂ + f₄.

Main results

theorem serre_D_H₂ : serre_D 2 H₂ = fun (z : UpperHalfPlane) => 1 / 6 * (H₂ z ^ 2 + 2 * H₂ z * H₄ z)

Serre derivative of H₂: ∂₂H₂ = (1/6)(H₂² + 2H₂H₄)

theorem serre_D_H₃ : serre_D 2 H₃ = fun (z : UpperHalfPlane) => 1 / 6 * (H₂ z ^ 2 - H₄ z ^ 2)

Serre derivative of H₃: ∂₂H₃ = (1/6)(H₂² - H₄²)

theorem serre_D_H₄ : serre_D 2 H₄ = fun (z : UpperHalfPlane) => -(1 / 6) * (2 * H₂ z * H₄ z + H₄ z ^ 2)

Serre derivative of H₄: ∂₂H₄ = -(1/6)(2H₂H₄ + H₄²)

theorem D_H₂ : D H₂ = (1 / 6) • (H₂ ^ 2 + 2 • (H₂ * H₄)) + (1 / 6) • (E₂ * H₂)

Ordinary derivative of H₂ in terms of H₂, H₄, and E₂.

theorem D_H₃ : D H₃ = (1 / 6) • (H₂ ^ 2 - H₄ ^ 2) + (1 / 6) • (E₂ * H₃)

Ordinary derivative of H₃ in terms of H₂, H₄, and E₂.

theorem D_H₄ : D H₄ = -(1 / 6) • (2 • (H₂ * H₄) + H₄ ^ 2) + (1 / 6) • (E₂ * H₄)

Ordinary derivative of H₄ in terms of H₂, H₄, and E₂.