Theta Derivative Identities

This file proves the Serre derivative identities for Jacobi theta functions (Blueprint Proposition 6.52, equations (32)–(34)):

• serre_D_H₂ : serre_D 2 H₂ = (1/6) * (H₂² + 2H₂H₄)
• serre_D_H₃ : serre_D 2 H₃ = (1/6) * (H₂² - H₄²)
• serre_D_H₄ : serre_D 2 H₄ = -(1/6) * (2H₂H₄ + H₄²)

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

Cusp Form Arguments (Phase 7)

• Tendsto lemmas for f₂, f₄, theta_g, theta_h at infinity
• Cusp form construction for theta_g and theta_h

Dimension Vanishing (Phase 8)

• theta_g = 0 and theta_h = 0 by weight < 12 cusp form vanishing

Main Deduction (Phase 9)

• f₂ = f₃ = f₄ = 0

Main Theorems (Phase 10)

• serre_D_H₂, serre_D_H₃, serre_D_H₄

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.

We then show g and h vanish at infinity (Phase 7), hence are cusp forms. By dimension vanishing (Phase 8), all level-1 cusp forms of weight < 12 are zero. This gives g = h = 0, from which we deduce f₂ = f₃ = f₄ = 0 (Phase 9), yielding the main theorems (Phase 10).

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

Phase 7: Cusp Form Arguments

We need to show g and h vanish at infinity. The tendsto lemmas for H₂, H₃, H₄ are already in AtImInfty.lean:

• H₂_tendsto_atImInfty : Tendsto H₂ atImInfty (𝓝 0)
• H₃_tendsto_atImInfty : Tendsto H₃ atImInfty (𝓝 1)
• H₄_tendsto_atImInfty : Tendsto H₄ atImInfty (𝓝 1)

theorem theta_g_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) theta_g

theta_g is MDifferentiable (from MDifferentiable of f₂, f₄, H₂, H₄)

theorem theta_h_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) theta_h

theta_h is MDifferentiable (from MDifferentiable of f₂, f₄)

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. Proof: f₂ = serre_D 2 H₂ - (1/6)H₂(H₂ + 2H₄) Since H₂ → 0 and serre_D 2 H₂ = D H₂ - (1/6)E₂ H₂ → 0, we get f₂ → 0 - 0 = 0.

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

f₄ tends to 0 at infinity. Proof: f₄ = serre_D 2 H₄ + (1/6)H₄(2H₂ + H₄) serre_D 2 H₄ = D H₄ - (1/6)E₂ H₄ → 0 - (1/6)11 = -1/6 (since H₄ → 1, E₂ → 1) H₄(2H₂ + H₄) → 1*(0 + 1) = 1 So f₄ → -1/6 + (1/6)*1 = 0.

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

theta_g tends to 0 at infinity. theta_g = (2H₂ + H₄)f₂ + (H₂ + 2H₄)f₄. Since 2H₂ + H₄ → 1, H₂ + 2H₄ → 2, and f₂, f₄ → 0, we get theta_g → 0.

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

theta_h tends to 0 at infinity. theta_h = f₂² + f₂f₄ + f₄² → 0 + 0 + 0 = 0 as f₂, f₄ → 0.

theorem theta_g_IsCuspForm : ∃ (g_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6), IsCuspForm (CongruenceSubgroup.Gamma 1) 6 g_MF ∧ ∀ (z : UpperHalfPlane), g_MF z = theta_g z

g is a cusp form of level 1.

theorem theta_h_IsCuspForm : ∃ (h_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 8), IsCuspForm (CongruenceSubgroup.Gamma 1) 8 h_MF ∧ ∀ (z : UpperHalfPlane), h_MF z = theta_h z

h is a cusp form of level 1.

Phase 8: Apply Dimension Vanishing

theorem theta_g_eq_zero : theta_g = 0

g = 0 by dimension argument.

Proof: g is a level-1 cusp form of weight 6. By IsCuspForm_weight_lt_eq_zero, all cusp forms of weight < 12 vanish. Hence g = 0.

theorem theta_h_eq_zero : theta_h = 0

h = 0 by dimension argument.

Proof: h is a level-1 cusp form of weight 8. By IsCuspForm_weight_lt_eq_zero, all cusp forms of weight < 12 vanish. Hence h = 0.

H_sum_sq: H₂² + H₂H₄ + H₄²

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 : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) 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 : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) fun (z : UpperHalfPlane) => 3 * H_sum_sq z

3 * H_sum_sq is MDifferentiable

E₄ = H_sum_sq (dimension argument)

E₄ and H_sum_sq are both weight-4 level-1 modular forms tending to 1 at ∞. Their difference is a weight-4 cusp form, hence zero by dimension vanishing.

theorem E₄_eq_H_sum_sq : E₄.toFun = H_sum_sq

E₄.toFun = H₂² + H₂H₄ + H₄². Both are weight-4 level-1 modular forms tending to 1 at ∞, so their difference is a weight-4 cusp form, hence zero.

Phase 9: Deduce f₂ = f₃ = f₄ = 0

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

Key algebraic identity for proving f₂ = f₄ = 0. Given Af₂ + Bf₄ = 0, we have f₄² * (A² - AB + B²) = A² * (f₂² + f₂f₄ + f₄²).

theorem f₂_eq_zero : f₂ = 0

From g = 0 and h = 0, deduce f₂ = 0.

Proof: From g = 0 we get a relation between f₂ and f₄. Combined with h = 0, we show f₄² · (3 · H_sum_sq) = 0. Since H_sum_sq → 1 ≠ 0, we get f₄ = 0, then f₂ = 0 follows from h = f₂² = 0.

theorem f₄_eq_zero : f₄ = 0

From f₂ = 0 and h = 0, deduce f₄ = 0

theorem f₃_eq_zero : f₃ = 0

From f₂ + f₄ = f₃ and both = 0, f₃ = 0

Phase 10: Main Theorems

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