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_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

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 }

@[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 : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑H₂_SIF

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

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

theorem H₂_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) H₂

theorem H₃_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) H₃

theorem H₄_MDifferentiable : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) 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 : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) Θ₂

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 }

@[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 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

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

Θ₂(It) has positive real part for t > 0. Proof: Each term Θ₂_term n (It) = exp(-π(n+1/2)²t) is a positive real. The sum of positive reals is positive.

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.