Jacobi theta definitions

Define Jacobi theta functions Θ₂, Θ₃, Θ₄ and their fourth powers H₂, H₃, H₄. Also record their realization as specializations of jacobiTheta₂.

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) ↑τ