Jacobi theta functions

Define Jacobi theta functions Θ₂, Θ₃, Θ₄ and their fourth powers H₂, H₃, H₄. Prove that H₂, H₃, H₄ are modualar forms of weight 2 and level Γ(2). Also Jacobi identity: Θ₂^4 + Θ₄^4 = Θ₃^4.

noncomputable def Θ₂_term (n : ℤ) (τ : UpperHalfPlane) : ℂ

Define Θ₂, Θ₃, Θ₄ as series.

Equations

• Θ₂_term n τ = Complex.exp (↑Real.pi * Complex.I * (↑n + 1 / 2) ^ 2 * ↑τ)

noncomputable def Θ₃_term (n : ℤ) (τ : UpperHalfPlane) : ℂ

Equations

• Θ₃_term n τ = Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * ↑τ)

noncomputable def Θ₄_term (n : ℤ) (τ : UpperHalfPlane) : ℂ

Equations

• Θ₄_term n τ = (-1) ^ n * Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * ↑τ)

noncomputable def Θ₂ (τ : UpperHalfPlane) : ℂ

Equations

• Θ₂ τ = ∑' (n : ℤ), Θ₂_term n τ

noncomputable def Θ₃ (τ : UpperHalfPlane) : ℂ

Equations

• Θ₃ τ = ∑' (n : ℤ), Θ₃_term n τ

noncomputable def Θ₄ (τ : UpperHalfPlane) : ℂ

Equations

• Θ₄ τ = ∑' (n : ℤ), Θ₄_term n τ

noncomputable def H₂ (τ : UpperHalfPlane) : ℂ

Equations

• H₂ τ = Θ₂ τ ^ 4

noncomputable def H₃ (τ : UpperHalfPlane) : ℂ

Equations

• H₃ τ = Θ₃ τ ^ 4

noncomputable def H₄ (τ : UpperHalfPlane) : ℂ

Equations

• H₄ τ = Θ₄ τ ^ 4

theorem Θ₂_term_as_jacobiTheta₂_term (τ : UpperHalfPlane) (n : ℤ) : Θ₂_term n τ = Complex.exp (↑Real.pi * Complex.I * ↑τ / 4) * jacobiTheta₂_term n (↑τ / 2) ↑τ

Theta functions as specializations of jacobiTheta₂

theorem Θ₂_as_jacobiTheta₂ (τ : UpperHalfPlane) : Θ₂ τ = Complex.exp (↑Real.pi * Complex.I * ↑τ / 4) * jacobiTheta₂ (↑τ / 2) ↑τ

theorem Θ₃_term_as_jacobiTheta₂_term (τ : UpperHalfPlane) (n : ℤ) : Θ₃_term n τ = jacobiTheta₂_term n 0 ↑τ

theorem Θ₃_as_jacobiTheta₂ (τ : UpperHalfPlane) : Θ₃ τ = jacobiTheta₂ 0 ↑τ

theorem Θ₄_term_as_jacobiTheta₂_term (τ : UpperHalfPlane) (n : ℤ) : Θ₄_term n τ = jacobiTheta₂_term n (1 / 2) ↑τ

theorem Θ₄_as_jacobiTheta₂ (τ : UpperHalfPlane) : Θ₄ τ = jacobiTheta₂ (1 / 2) ↑τ

theorem H₂_negI_action : SlashAction.map 2 (↑negI) H₂ = H₂

Slash action of various elements on H₂, H₃, H₄

theorem H₃_negI_action : SlashAction.map 2 (↑negI) H₃ = H₃

theorem H₄_negI_action : SlashAction.map 2 (↑negI) H₄ = H₄

theorem H₂_T_action : SlashAction.map 2 ModularGroup.T H₂ = -H₂

These three transformation laws follow directly from tsum definition.

theorem H₃_T_action : SlashAction.map 2 ModularGroup.T H₃ = H₄

theorem H₄_T_action : SlashAction.map 2 ModularGroup.T H₄ = H₃

theorem H₂_T_inv_action : SlashAction.map 2 ModularGroup.T⁻¹ H₂ = -H₂

theorem H₃_T_inv_action : SlashAction.map 2 ModularGroup.T⁻¹ H₃ = H₄

theorem H₄_T_inv_action : SlashAction.map 2 ModularGroup.T⁻¹ H₄ = H₃

theorem H₂_α_action : SlashAction.map 2 (↑α) H₂ = H₂

Use α = T * T

theorem H₃_α_action : SlashAction.map 2 (↑α) H₃ = H₃

theorem H₄_α_action : SlashAction.map 2 (↑α) H₄ = H₄

theorem H₂_S_action : SlashAction.map 2 ModularGroup.S H₂ = -H₄

Use jacobiTheta₂_functional_equation

theorem H₃_S_action : SlashAction.map 2 ModularGroup.S H₃ = -H₃

theorem H₄_S_action : SlashAction.map 2 ModularGroup.S H₄ = -H₂

theorem H₂_S_inv_action : SlashAction.map 2 ModularGroup.S⁻¹ H₂ = -H₄

theorem H₃_S_inv_action : SlashAction.map 2 ModularGroup.S⁻¹ H₃ = -H₃

theorem H₄_S_inv_action : SlashAction.map 2 ModularGroup.S⁻¹ H₄ = -H₂

theorem H₂_β_action : SlashAction.map 2 (↑β) H₂ = H₂

Use β = -S * α^(-1) * S

theorem H₃_β_action : SlashAction.map 2 (↑β) H₃ = H₃

theorem H₄_β_action : SlashAction.map 2 (↑β) H₄ = H₄

noncomputable def H₂_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

H₂, H₃, H₄ are modular forms of weight 2 and level Γ(2)

Equations

• H₂_SIF = { toFun := H₂, slash_action_eq' := H₂_SIF._proof_1 }

noncomputable def H₃_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₃_SIF = { toFun := H₃, slash_action_eq' := H₃_SIF._proof_1 }

noncomputable def H₄_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₄_SIF = { toFun := H₄, slash_action_eq' := H₄_SIF._proof_1 }

theorem H₂_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₂_SIF

theorem H₃_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₃_SIF

theorem H₄_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₄_SIF

theorem jacobiTheta₂_term_half_apply (n : ℤ) (z : ℂ) : jacobiTheta₂_term n (z / 2) z = Complex.exp (↑Real.pi * Complex.I * (↑n ^ 2 + ↑n) * z)

theorem jacobiTheta₂_rel_aux (n : ℤ) (t : ℝ) : ↑(Real.exp (-Real.pi * (↑n + 1 / 2) ^ 2 * t)) = ↑(Real.exp (-Real.pi * t / 4)) * jacobiTheta₂_term n (Complex.I * ↑t / 2) (Complex.I * ↑t)

theorem Complex.norm_exp_mul_I (z : ℂ) : ‖exp (z * I)‖ = Real.exp (-z.im)

theorem isBoundedAtImInfty_H₂ : UpperHalfPlane.IsBoundedAtImInfty H₂

theorem isBoundedAtImInfty_H₃_aux (z : UpperHalfPlane) (hz : 1 ≤ z.im) : ∑' (n : ℤ), ‖Θ₃_term n z‖ ≤ ∑' (n : ℤ), Real.exp (-Real.pi * ↑n ^ 2)

theorem isBoundedAtImInfty_H₃ : UpperHalfPlane.IsBoundedAtImInfty H₃

theorem isBoundedAtImInfty_H₄ : UpperHalfPlane.IsBoundedAtImInfty H₄

theorem isBoundedAtImInfty_H_slash (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 2 γ H₂) ∧ UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 2 γ H₃) ∧ UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 2 γ H₄)

theorem isBoundedAtImInfty_H₂_slash (A : GL (Fin 2) ℝ) : A ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 2 A H₂)

theorem isBoundedAtImInfty_H₃_slash (A : GL (Fin 2) ℝ) : A ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 2 A H₃)

theorem isBoundedAtImInfty_H₄_slash (A : GL (Fin 2) ℝ) : A ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 2 A H₄)

noncomputable def H₂_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₂_MF = { toSlashInvariantForm := H₂_SIF, holo' := H₂_SIF_MDifferentiable, bdd_at_cusps' := @H₂_MF._proof_1 }

noncomputable def H₃_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₃_MF = { toSlashInvariantForm := H₃_SIF, holo' := H₃_SIF_MDifferentiable, bdd_at_cusps' := @H₃_MF._proof_1 }

noncomputable def H₄_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₄_MF = { toSlashInvariantForm := H₄_SIF, holo' := H₄_SIF_MDifferentiable, bdd_at_cusps' := @H₄_MF._proof_1 }

Jacobi identity

The Jacobi identity states H₂ + H₄ = H₃ (equivalently Θ₂⁴ + Θ₄⁴ = Θ₃⁴). This is blueprint Lemma 6.41, proved via dimension vanishing for weight 4 cusp forms.

The proof strategy:

1. Define g := H₂ + H₄ - H₃ and f := g²
2. Show f is SL₂(ℤ)-invariant (weight 4, level 1) via S/T invariance
3. Show f vanishes at i∞ (is a cusp form)
4. Apply cusp form vanishing: dim S₄(Γ₁) = 0
5. From g² = 0 conclude g = 0

The S/T slash action lemmas are proved here. The full proof requiring asymptotics (atImInfty) is in AtImInfty.lean to avoid circular imports.

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 SlashInvariantForm 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 : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) jacobi_g

jacobi_g is holomorphic (MDifferentiable) since H₂, H₃, H₄ are

theorem jacobi_f_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) jacobi_f

jacobi_f is holomorphic (MDifferentiable) since jacobi_g is

theorem jacobi_f_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑jacobi_f_SIF

jacobi_f_SIF is holomorphic

Limits at infinity

We prove the limit of Θᵢ(z) and Hᵢ(z) as z tends to i∞. This is used to prove the Jacobi identity.

theorem jacobiTheta₂_half_mul_apply_tendsto_atImInfty : Filter.Tendsto (fun (x : UpperHalfPlane) => jacobiTheta₂ (↑x / 2) ↑x) UpperHalfPlane.atImInfty (nhds 2)

theorem jacobiTheta₂_zero_apply_tendsto_atImInfty : Filter.Tendsto (fun (x : UpperHalfPlane) => jacobiTheta₂ 0 ↑x) UpperHalfPlane.atImInfty (nhds 1)

theorem jacobiTheta₂_half_apply_tendsto_atImInfty : Filter.Tendsto (fun (x : UpperHalfPlane) => jacobiTheta₂ (1 / 2) ↑x) UpperHalfPlane.atImInfty (nhds 1)

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

theorem Θ₃_tendsto_atImInfty : Filter.Tendsto Θ₃ UpperHalfPlane.atImInfty (nhds 1)

theorem Θ₄_tendsto_atImInfty : Filter.Tendsto Θ₄ UpperHalfPlane.atImInfty (nhds 1)

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

theorem H₃_tendsto_atImInfty : Filter.Tendsto H₃ UpperHalfPlane.atImInfty (nhds 1)

theorem H₄_tendsto_atImInfty : Filter.Tendsto H₄ UpperHalfPlane.atImInfty (nhds 1)

Jacobi identity proof

We prove that g := H₂ + H₄ - H₃ → 0 at i∞, hence f := g² → 0. Combined with the dimension vanishing 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∞. Since H₂ → 0, H₃ → 1, H₄ → 1, we have g → 0 + 1 - 1 = 0.

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

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

theorem isBoundedAtImInfty_jacobi_f : UpperHalfPlane.IsBoundedAtImInfty jacobi_f

jacobi_f is bounded at i∞ (follows from tending to 0)

theorem jacobi_f_slash_eq (A' : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 4 ((Matrix.SpecialLinearGroup.mapGL ℝ) A') jacobi_f = jacobi_f

jacobi_f slash by any SL₂(ℤ) element equals jacobi_f (for use with bounded_at_cusps)

theorem isBoundedAtImInfty_jacobi_f_slash (A : GL (Fin 2) ℝ) : A ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range → UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map 4 A jacobi_f)

jacobi_f slash by any SL₂(ℤ) element is bounded at i∞

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

jacobi_f as a ModularForm of weight 4 and level Γ(1)

Equations

• jacobi_f_MF = { toSlashInvariantForm := jacobi_f_SIF, holo' := jacobi_f_SIF_MDifferentiable, bdd_at_cusps' := @jacobi_f_MF._proof_1 }

theorem jacobi_f_MF_IsCuspForm : IsCuspForm (CongruenceSubgroup.Gamma 1) 4 jacobi_f_MF

jacobi_f_MF is a cusp form because it vanishes at i∞

theorem jacobi_f_MF_eq_zero : jacobi_f_MF = 0

The main dimension vanishing: jacobi_f_MF = 0

theorem jacobi_f_eq_zero : jacobi_f = 0

jacobi_f = 0 as a function

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