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 (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 (CongruenceSubgroup.Gamma 2) 2

Equations

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

noncomputable def H₄_SIF : SlashInvariantForm (CongruenceSubgroup.Gamma 2) 2

Equations

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

noncomputable def H₂_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₂_SIF

Equations

• ⋯ = ⋯

noncomputable def H₃_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₃_SIF

Equations

• H₃_SIF_MDifferentiable = ⋯

noncomputable def H₄_SIF_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₄_SIF

Equations

• H₄_SIF_MDifferentiable = ⋯

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 (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ 2 γ H₂)

theorem isBoundedAtImInfty_H₃_slash (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ 2 γ H₃)

theorem isBoundedAtImInfty_H₄_slash (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.IsBoundedAtImInfty (SlashAction.map ℂ 2 γ H₄)

noncomputable def H₂_MF : ModularForm (CongruenceSubgroup.Gamma 2) 2

Equations

• H₂_MF = { toSlashInvariantForm := H₂_SIF, holo' := H₂_SIF_MDifferentiable, bdd_at_infty' := isBoundedAtImInfty_H₂_slash }

noncomputable def H₃_MF : ModularForm (CongruenceSubgroup.Gamma 2) 2

Equations

• H₃_MF = { toSlashInvariantForm := H₃_SIF, holo' := H₃_SIF_MDifferentiable, bdd_at_infty' := isBoundedAtImInfty_H₃_slash }

noncomputable def H₄_MF : ModularForm (CongruenceSubgroup.Gamma 2) 2

Equations

• H₄_MF = { toSlashInvariantForm := H₄_SIF, holo' := H₄_SIF_MDifferentiable, bdd_at_infty' := isBoundedAtImInfty_H₄_slash }

theorem jacobi_identity (τ : UpperHalfPlane) : Θ₂ τ ^ 4 + Θ₄ τ ^ 4 = Θ₃ τ ^ 4

Jacobi identity