Theta Derivative Identities

This file defines error terms for the Serre derivative identities of Jacobi theta functions H₂, H₃, H₄ (Blueprint Proposition 6.52), establishes their S/T transformation rules, and constructs level-1 invariants.

Contents

Error Terms (Phases 1-5)

• Error terms f₂, f₃, f₄ definitions
• MDifferentiable proofs for error terms
• Relation f₂ + f₄ = f₃ (from jacobi_identity in JacobiTheta.lean)
• S/T transformation rules: f₂_S_action, f₂_T_action, f₄_S_action, f₄_T_action

Level-1 Invariants (Phase 6)

• Level-1 invariant theta_g (weight 6): g = (2H₂ + H₄)f₂ + (H₂ + 2H₄)f₄
• Level-1 invariant theta_h (weight 8): h = f₂² + f₂f₄ + f₄²
• S/T invariance: theta_g_S_action, theta_g_T_action, theta_h_S_action, theta_h_T_action

Strategy

We define error terms f₂, f₃, f₄ = (LHS - RHS) and prove their transformation rules under the S and T generators of SL(2,ℤ). The key results are:

• f₂|S = -f₄, f₂|T = -f₂
• f₄|S = -f₂, f₄|T = f₃

Using these transformation rules, we construct g and h such that g|S = g, g|T = g, h|S = h, h|T = h. This makes g and h into level-1 (SL(2,ℤ)-invariant) modular forms.

Phase 1: Error Term Definitions

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₄))

Phase 2: MDifferentiable for Error Terms

theorem f₂_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f₂

f₂ is MDifferentiable

theorem f₃_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f₃

f₃ is MDifferentiable

theorem f₄_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f₄

f₄ is MDifferentiable

Phase 3-4: Relation f₂ + f₄ = f₃

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

The error terms satisfy f₂ + f₄ = f₃ (from Jacobi identity)

Phase 5: S/T Transformation Rules for f₂, f₄

These transformations depend on serre_D_slash_equivariant (which has a sorry in Derivative.lean). The proofs use:

• serre_D_slash_equivariant: (serre_D k F)|[k+2]γ = serre_D k (F|[k]γ)
• H₂_S_action: H₂|[2]S = -H₄
• H₄_S_action: H₄|[2]S = -H₂
• H₂_T_action: H₂|[2]T = -H₂
• H₃_T_action: H₃|[2]T = H₄
• H₄_T_action: H₄|[2]T = H₃

From these, we get:

• (serre_D 2 H₂)|[4]S = serre_D 2 (H₂|[2]S) = serre_D 2 (-H₄) = -serre_D 2 H₄
• Products transform multiplicatively: (H₂·G)|[4]S = (H₂|[2]S)·(G|[2]S)

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

f₂ transforms under S as f₂|S = -f₄.

Proof outline using serre_D_slash_equivariant:

1. (serre_D 2 H₂)|[4]S = serre_D 2 (H₂|[2]S) = serre_D 2 (-H₄) = -serre_D 2 H₄
2. (H₂(H₂ + 2H₄))|[4]S = (-H₄)((-H₄) + 2(-H₂)) = H₄(H₄ + 2H₂)
3. f₂|[4]S = -serre_D 2 H₄ - (1/6)H₄(H₄ + 2H₂) = -f₄

Key lemmas used:

• serre_D_slash_equivariant: (serre_D k F)|[k+2]γ = serre_D k (F|[k]γ)
• serre_D_smul: serre_D k (c • F) = c • serre_D k F (used for negation)
• mul_slash_SL2: (f * g)|[k1+k2]A = (f|[k1]A) * (g|[k2]A)
• add_slash, SL_smul_slash for linearity

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

f₂ transforms under T as f₂|T = -f₂.

Proof outline:

1. (serre_D 2 H₂)|[4]T = serre_D 2 (H₂|[2]T) = serre_D 2 (-H₂) = -serre_D 2 H₂
2. (H₂(H₂ + 2H₄))|[4]T = (-H₂)((-H₂) + 2H₃) Using Jacobi H₃ = H₂ + H₄: -H₂ + 2H₃ = -H₂ + 2(H₂ + H₄) = H₂ + 2H₄ So: (H₂(H₂ + 2H₄))|[4]T = (-H₂)(H₂ + 2H₄)
3. f₂|[4]T = -serre_D 2 H₂ - (1/6)(-H₂)(H₂ + 2H₄) = -serre_D 2 H₂ + (1/6)H₂(H₂ + 2H₄) = -(serre_D 2 H₂ - (1/6)H₂(H₂ + 2H₄)) = -f₂

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

f₄ transforms under S as f₄|S = -f₂.

Proof outline (symmetric to f₂_S_action):

1. (serre_D 2 H₄)|[4]S = serre_D 2 (H₄|[2]S) = serre_D 2 (-H₂) = -serre_D 2 H₂
2. (H₄(2H₂ + H₄))|[4]S = (-H₂)(2(-H₄) + (-H₂)) = H₂(H₂ + 2H₄)
3. f₄|[4]S = -serre_D 2 H₂ + (1/6)H₂(H₂ + 2H₄) = -f₂

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

f₄ transforms under T as f₄|T = f₃.

Proof outline:

1. (serre_D 2 H₄)|[4]T = serre_D 2 (H₄|[2]T) = serre_D 2 H₃
2. (H₄(2H₂ + H₄))|[4]T = H₃(2(-H₂) + H₃) = H₃(H₃ - 2H₂) Using Jacobi H₃ = H₂ + H₄: H₃ - 2H₂ = H₄ - H₂
3. f₄|[4]T = serre_D 2 H₃ + (1/6)H₃(H₃ - 2H₂) But H₂² - H₄² = (H₂ - H₄)(H₂ + H₄) = (H₂ - H₄)H₃ So (1/6)(H₂² - H₄²) = -(1/6)H₃(H₄ - H₂) = -(1/6)H₃(H₃ - 2H₂) Thus f₃ = serre_D 2 H₃ - (1/6)(H₂² - H₄²) = f₄|[4]T

Phase 6: Level-1 Invariants g, 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

g is invariant under S.

Proof: g = (2H₂ + H₄)f₂ + (H₂ + 2H₄)f₄ Under S: H₂ ↦ -H₄, H₄ ↦ -H₂, f₂ ↦ -f₄, f₄ ↦ -f₂ g|S = (2(-H₄) + (-H₂))(-f₄) + ((-H₄) + 2(-H₂))(-f₂) = (2H₄ + H₂)f₄ + (H₄ + 2H₂)f₂ = g

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

g is invariant under T.

Proof: Under T: H₂ ↦ -H₂, H₄ ↦ H₃, f₂ ↦ -f₂, f₄ ↦ f₃ = f₂ + f₄ g|T = (2(-H₂) + H₃)(-f₂) + ((-H₂) + 2H₃)(f₂ + f₄) Using Jacobi: H₃ = H₂ + H₄, simplifies to g.

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

h is invariant under S.

Proof: h = f₂² + f₂f₄ + f₄² Under S: f₂|[4]S = -f₄, f₄|[4]S = -f₂ Using mul_slash_SL2: (f₂²)|[8]S = (f₂|[4]S)² = (-f₄)² = f₄² (f₂f₄)|[8]S = (f₂|[4]S)(f₄|[4]S) = (-f₄)(-f₂) = f₂f₄ (f₄²)|[8]S = (f₄|[4]S)² = (-f₂)² = f₂² So h|[8]S = f₄² + f₂f₄ + f₂² = f₂² + f₂f₄ + f₄² = h

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

h is invariant under T.

Proof: Under T: f₂ ↦ -f₂, f₄ ↦ f₃ = f₂ + f₄ h|T = (-f₂)² + (-f₂)(f₂ + f₄) + (f₂ + f₄)² = f₂² - f₂² - f₂f₄ + f₂² + 2f₂f₄ + f₄² = f₂² + f₂f₄ + f₄² = h