Jacobi theta basics

Prove transformation laws, modularity, asymptotics, and the Jacobi identity for the Jacobi theta functions defined in Defs.lean.

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 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₄)

Limits at infinity

We prove the limit of Θᵢ(z) and Hᵢ(z) as z tends to i∞. These results are used in JacobiIdentity.lean.

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)

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.