Jacobi theta identities

This file proves the Jacobi identity H₂ + H₄ = H₃ and the discriminant identity Delta = (H₂ * H₃ * H₄)^2 / 256.

The proof strategy:

1. Define g := H₂ + H₄ - H₃ and f := g².
2. Show f is a weight-4 level-1 modular form.
3. Show f vanishes at i∞ using the asymptotic lemmas from Basic.lean.
4. Apply cusp form vanishing in weight 4 to deduce f = 0, hence g = 0.
5. Use the weight-12 analogue for (H₂ * H₃ * H₄)^2 to identify Delta.

noncomputable def jacobi_g : UpperHalfPlane → ℂ

The difference g := H₂ + H₄ - H₃.

Equations

• jacobi_g = H₂ + H₄ - H₃

noncomputable def jacobi_f : UpperHalfPlane → ℂ

The squared difference f := g².

Equations

• jacobi_f = jacobi_g ^ 2

theorem jacobi_g_S_action : SlashAction.map 2 ModularGroup.S jacobi_g = -jacobi_g

S-action on g: g|[2]S = -g.

theorem jacobi_g_T_action : SlashAction.map 2 ModularGroup.T jacobi_g = -jacobi_g

T-action on g: g|[2]T = -g.

theorem jacobi_f_eq_mul : jacobi_f = jacobi_g * jacobi_g

Rewrite jacobi_f as a pointwise product.

theorem jacobi_f_S_action : SlashAction.map 4 ModularGroup.S jacobi_f = jacobi_f

S-invariance of f: f|[4]S = f, because g|[2]S = -g.

theorem jacobi_f_T_action : SlashAction.map 4 ModularGroup.T jacobi_f = jacobi_f

T-invariance of f: f|[4]T = f, because g|[2]T = -g.

theorem jacobi_f_SL2Z_invariant (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 4 γ jacobi_f = jacobi_f

Full SL₂(ℤ) invariance of f with weight 4.

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

jacobi_f as a slash-invariant form of weight 4 and level Γ(1).

Equations

• jacobi_f_SIF = { toFun := jacobi_f, slash_action_eq' := jacobi_f_SIF._proof_1 }

theorem jacobi_g_MDifferentiable : MDiff jacobi_g

jacobi_g is holomorphic since H₂, H₃, and H₄ are.

theorem jacobi_f_MDifferentiable : MDiff jacobi_f

jacobi_f is holomorphic since jacobi_g is.

theorem jacobi_f_SIF_MDifferentiable : MDiff ⇑jacobi_f_SIF

jacobi_f_SIF is holomorphic.

Jacobi identity proof

We prove that g := H₂ + H₄ - H₃ → 0 at i∞, hence f := g² → 0. Combined with the dimension-vanishing theorem for weight-4 cusp forms, this proves the Jacobi identity.

theorem jacobi_g_tendsto_atImInfty : Filter.Tendsto jacobi_g UpperHalfPlane.atImInfty (nhds 0)

The function g := H₂ + H₄ - H₃ tends to 0 at i∞.

theorem jacobi_f_tendsto_atImInfty : Filter.Tendsto jacobi_f UpperHalfPlane.atImInfty (nhds 0)

The function f := g² tends to 0 at i∞.

theorem jacobi_f_eq_zero : jacobi_f = 0

jacobi_f = 0 by dimension argument: weight-4 cusp forms vanish.

theorem jacobi_g_eq_zero : jacobi_g = 0

jacobi_g = 0 as a function, from g² = 0.

theorem jacobi_identity : H₂ + H₄ = H₃

Jacobi identity: H₂ + H₄ = H₃ (Blueprint Lemma 6.41).

theorem Delta_eq_H₂_H₃_H₄ (τ : UpperHalfPlane) : Delta τ = (H₂ τ * H₃ τ * H₄ τ) ^ 2 / 256