JacobiTheta

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) : ℂ

The n-th term of the Jacobi theta series Θ₂.

Equations

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

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

The n-th term of the Jacobi theta series Θ₃.

Equations

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

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

The n-th term of the Jacobi theta series Θ₄.

Equations

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

noncomputable def Θ₂ (τ : UpperHalfPlane) : ℂ

The Jacobi theta function Θ₂.

Equations

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

noncomputable def Θ₃ (τ : UpperHalfPlane) : ℂ

The Jacobi theta function Θ₃.

Equations

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

noncomputable def Θ₄ (τ : UpperHalfPlane) : ℂ

The Jacobi theta function Θ₄.

Equations

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

noncomputable def H₂ (τ : UpperHalfPlane) : ℂ

The fourth power Θ₂ ^ 4 of the theta function Θ₂.

Equations

• H₂ τ = Θ₂ τ ^ 4

noncomputable def H₃ (τ : UpperHalfPlane) : ℂ

The fourth power Θ₃ ^ 4 of the theta function Θ₃.

Equations

• H₃ τ = Θ₃ τ ^ 4

noncomputable def H₄ (τ : UpperHalfPlane) : ℂ

The fourth power Θ₄ ^ 4 of the theta function Θ₄.

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_action' (z : UpperHalfPlane) : H₂ (ModularGroup.S • z) = -↑z ^ 2 * H₄ z

theorem H₄_S_action' (z : UpperHalfPlane) : H₄ (ModularGroup.S • z) = -↑z ^ 2 * H₂ z

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

H₃ as a slash-invariant form 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

H₄ as a slash-invariant form of weight 2 and level Γ(2).

Equations

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

@[simp]

theorem H₂_SIF_coe : ⇑H₂SIF = H₂

@[simp]

theorem H₃_SIF_coe : ⇑H₃SIF = H₃

@[simp]

theorem H₄_SIF_coe : ⇑H₄SIF = H₄

theorem H₂_SIF_MDifferentiable : MDiff ⇑H₂SIF

theorem H₃_SIF_MDifferentiable : MDiff ⇑H₃SIF

theorem H₄_SIF_MDifferentiable : MDiff ⇑H₄SIF

theorem H₂_MDifferentiable : MDiff H₂

theorem H₃_MDifferentiable : MDiff H₃

theorem H₄_MDifferentiable : MDiff H₄

theorem differentiableAt_jacobiTheta₂_half (τ : UpperHalfPlane) : DifferentiableAt ℂ (fun (t : ℂ) => jacobiTheta₂ (t / 2) t) ↑τ

Differentiability of t ↦ jacobiTheta₂(t/2, t) at points in the upper half-plane.

theorem Θ₂_MDifferentiable : MDiff Θ₂

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

H₂ as a modular form of weight 2 and level Γ(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

H₃ as a modular form of weight 2 and level Γ(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

H₄ as a modular form of weight 2 and level Γ(2).

Equations

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

@[simp]

theorem H₂_MF_coe : ⇑H₂MF = H₂

@[simp]

theorem H₃_MF_coe : ⇑H₃MF = H₃

@[simp]

theorem H₄_MF_coe : ⇑H₄MF = H₄

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 jacobiG : UpperHalfPlane → ℂ

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

Equations

• jacobiG = H₂ + H₄ - H₃

noncomputable def jacobiF : UpperHalfPlane → ℂ

The squared difference f := g²

Equations

• jacobiF = jacobiG ^ 2

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

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

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

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

theorem jacobi_f_eq_mul : jacobiF = jacobiG * jacobiG

Rewrite jacobiF as a pointwise product

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

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

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

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 γ jacobiF = jacobiF

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

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

jacobiF as a SlashInvariantForm of weight 4 and level Γ(1)

Equations

• jacobiFSIF = { toFun := jacobiF, slash_action_eq' := jacobiFSIF._proof_1 }

theorem jacobi_g_MDifferentiable : MDiff jacobiG

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

theorem jacobi_f_MDifferentiable : MDiff jacobiF

jacobiF is holomorphic (MDifferentiable) since jacobiG is

theorem jacobi_f_SIF_MDifferentiable : MDiff ⇑jacobiFSIF

jacobiFSIF 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 jacobiG 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 jacobiF UpperHalfPlane.atImInfty (nhds 0)

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

theorem jacobi_f_eq_zero : jacobiF = 0

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

theorem jacobi_g_eq_zero : jacobiG = 0

jacobiG = 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

Imaginary Axis Properties

Properties of theta functions when restricted to the positive imaginary axis z = I*t.

theorem Θ₂_term_imag_axis_real (n : ℤ) (t : ℝ) (ht : 0 < t) : (Θ₂Term n { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).im = 0

Each term Θ₂Term n (I*t) has zero imaginary part for t > 0.

theorem Complex.im_tsum_eq_zero_of_im_eq_zero (f : ℤ → ℂ) (hf : Summable f) (him : ∀ (n : ℤ), (f n).im = 0) : (∑' (n : ℤ), f n).im = 0

im distributes over tsum when each term has zero imaginary part.

theorem Θ₂_imag_axis_real (t : ℝ) (ht : 0 < t) : (Θ₂ { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).im = 0

Θ₂(I*t) has zero imaginary part for t > 0.

theorem neg_one_zpow_im_eq_zero (n : ℤ) : ((-1) ^ n).im = 0

(-1 : ℂ)^n has zero imaginary part for any integer n.

theorem Θ₄_term_imag_axis_real (n : ℤ) (t : ℝ) (ht : 0 < t) : (Θ₄Term n { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).im = 0

Each term Θ₄Term n (I*t) has zero imaginary part for t > 0.

theorem Θ₄_imag_axis_real (t : ℝ) (ht : 0 < t) : (Θ₄ { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).im = 0

Θ₄(I*t) has zero imaginary part for t > 0.

theorem H₂_imag_axis_real : ResToImagAxis.Real H₂

H₂(it) is real for all t > 0. Blueprint: Follows from the q-expansion having real coefficients. Proof strategy: H₂ = Θ₂^4 where Θ₂(it) = ∑ₙ exp(-π(n+1/2)²t) is a sum of real exponentials.

theorem Θ₂_term_imag_axis_re (n : ℤ) (t : ℝ) (ht : 0 < t) : (Θ₂Term n { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).re = Real.exp (-Real.pi * (↑n + 1 / 2) ^ 2 * t)

Each term Θ₂Term n (I*t) has positive real part equal to exp(-π(n+1/2)²t) for t > 0.

theorem Θ₂_term_imag_axis_re_pos (n : ℤ) (t : ℝ) (ht : 0 < t) : 0 < (Θ₂Term n { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).re

Each term Θ₂Term n (I*t) has positive real part for t > 0.

theorem Θ₂_imag_axis_re_pos (t : ℝ) (ht : 0 < t) : 0 < (Θ₂ { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).re

Θ₂(I*t) has positive real part for t > 0.

theorem H₂_imag_axis_pos : ResToImagAxis.Pos H₂

H₂(it) > 0 for all t > 0. Blueprint: Lemma 6.43 - H₂ is positive on the imaginary axis. Proof strategy: Each term exp(-π(n+1/2)²t) > 0, so Θ₂(it) > 0, hence H₂ = Θ₂^4 > 0.

theorem H₄_imag_axis_real : ResToImagAxis.Real H₄

H₄(it) is real for all t > 0. Blueprint: Corollary 6.43 - follows from Θ₄ being real on the imaginary axis.

theorem H₄_imag_axis_pos : ResToImagAxis.Pos H₄

H₄(it) > 0 for all t > 0. Blueprint: Corollary 6.43 - H₄ is positive on the imaginary axis.

Proof strategy: Use the modular S-transformation relating H₄ and H₂. From H₄_S_action: (H₄ ∣[2] S) = -H₂ From ResToImagAxis.SlashActionS: relates values at t and 1/t. This gives H₂(i/t) = t² * H₄(it), so H₄(it) > 0 follows from H₂(i/t) > 0.