Theta series at the cusp ∞

Let L be a discrete subgroup of a finite-dimensional real normed space E. This file studies the theta series Θ_L(τ) = ∑_{v ∈ L} exp (π i ‖v‖² τ) and the theta series θ_{γ+L}(τ) = ∑_{v ∈ L} exp (π i ‖γ + v‖² τ) of a translate as im τ → ∞, and on the imaginary axis.

The term of index v has norm exp (-π ‖γ + v‖² im τ). On a half-plane {τ | y ≤ im τ}, 0 < y, the terms are therefore dominated by the summable Gaussian exp (-π y ‖γ + v‖²), so the series are bounded at i∞; and as im τ → ∞ every term tends to 0, except the term of the vector v = -γ, which is constantly 1 and exists only when γ ∈ L. By dominated convergence, Θ_L(τ) → 1, while θ_{γ+L}(τ) → 0 for γ ∉ L. Together with holomorphy and periodicity this identifies the constant term of the q-expansion of Θ_L: it is 1, in q = exp (2 π i τ) for an even lattice and in exp (π i τ) for an integral one. It also shows that Θ_L is never a cusp form, for any group having ∞ as a cusp.

On the imaginary axis τ = i y every term is the positive real number exp (-π y ‖γ + v‖²), so θ_{γ+L}(i y) is a positive real number and Θ_L(i y) ≥ 1. In particular Θ_L does not vanish there; this is the nonvanishing used to show that the rank of an even unimodular lattice is divisible by 8.

Main statements

• ZLattice.tendsto_tsum_mul_thetaTerm_atImInfty: a theta sum weighted by coefficients of norm at most 1 tends at i∞ to the sum of the weights of the vectors v ∈ L with γ + v = 0.
• ZLattice.isBoundedAtImInfty_thetaCoset, ZLattice.isBoundedAtImInfty_thetaSeries: the theta series are bounded at i∞.
• ZLattice.tendsto_thetaSeries_atImInfty, ZLattice.valueAtInfty_thetaSeries: Θ_L(τ) → 1 as im τ → ∞.
• ZLattice.not_isZeroAtImInfty_thetaSeries, ZLattice.coe_ne_thetaSeries, ZLattice.not_isCuspForm_of_coe_eq_thetaSeries: Θ_L does not vanish at ∞, so it is not a cusp form on any group having ∞ as a cusp.
• ZLattice.isZeroAtImInfty_thetaCoset: θ_{γ+L}(τ) → 0 as im τ → ∞ when γ ∉ L.
• ZLattice.IsEven.qExpansion_thetaSeries_coeff_zero: for even L the constant term of the q-expansion of Θ_L is 1; ZLattice.IsIntegral.qExpansion_two_thetaSeries_coeff_zero is the same statement in exp (π i τ) for integral L.
• ZLattice.thetaCoset_eq_ofReal_of_re_eq_zero, ZLattice.re_thetaCoset_pos, ZLattice.one_le_re_thetaSeries: on the imaginary axis θ_{γ+L} is real and positive, and Θ_L ≥ 1.

References

• J.-P. Serre, A Course in Arithmetic, Ch. VII §6.
• W. Ebeling, Lattices and Codes, Ch. 2.

theorem ZLattice.norm_thetaCoset_le {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) {y : ℝ} (hs : Summable fun (v : ↥L) => Real.exp (-(Real.pi * y) * ‖γ + ↑v‖ ^ 2)) {τ : UpperHalfPlane} (hτ : y ≤ τ.im) : ‖thetaCoset L γ τ‖ ≤ ∑' (v : ↥L), Real.exp (-(Real.pi * y) * ‖γ + ↑v‖ ^ 2)

On the half-plane {τ | y ≤ im τ}, the theta series of γ + L is bounded in norm by ∑_{v ∈ L} exp (-π y ‖γ + v‖²), its value at i y, provided this Gaussian sum converges (it does for a discrete L, by summable_exp_neg_mul_norm_add_sq).

theorem ZLattice.isBoundedAtImInfty_thetaCoset {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) : UpperHalfPlane.IsBoundedAtImInfty (thetaCoset L γ)

The theta series of a translate of a subgroup is bounded at i∞.

theorem ZLattice.isBoundedAtImInfty_thetaSeries {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) : UpperHalfPlane.IsBoundedAtImInfty (thetaSeries L)

The theta series of a subgroup is bounded at i∞.

theorem ZLattice.tendsto_tsum_mul_thetaTerm_atImInfty {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) (w : ↥L → ℂ) (hw : ∀ (v : ↥L), ‖w v‖ ≤ 1) {y : ℝ} (hs : Summable fun (v : ↥L) => Real.exp (-(Real.pi * y) * ‖γ + ↑v‖ ^ 2)) : Filter.Tendsto (fun (τ : UpperHalfPlane) => ∑' (v : ↥L), w v * Complex.exp (↑Real.pi * Complex.I * ↑(‖γ + ↑v‖ ^ 2) * ↑τ)) UpperHalfPlane.atImInfty (nhds (∑' (v : ↥L), if γ + ↑v = 0 then w v else 0))

Weighted theta sums at i∞. For weights w v of norm at most 1, the weighted theta sum ∑_{v ∈ L} w v exp (π i ‖γ + v‖² τ) tends at i∞ to the sum of the weights of the vectors v ∈ L with γ + v = 0, by dominated convergence: the term of such a v is constantly w v, and every other term tends to 0. The Gaussian sum ∑_{v ∈ L} exp (-π y ‖γ + v‖²) has to converge for some y, as it does for a discrete L, by summable_exp_neg_mul_norm_add_sq.

theorem ZLattice.tendsto_thetaSeries_atImInfty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : Filter.Tendsto (thetaSeries L) UpperHalfPlane.atImInfty (nhds 1)

The theta series of a discrete subgroup tends to 1 at i∞: every term except the term exp 0 = 1 of the zero vector tends to 0.

@[simp]

theorem ZLattice.valueAtInfty_thetaSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : UpperHalfPlane.valueAtInfty (thetaSeries L) = 1

The value of the theta series of a discrete subgroup at the cusp ∞ is 1.

@[simp]

theorem ZLattice.not_isZeroAtImInfty_thetaSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : ¬UpperHalfPlane.IsZeroAtImInfty (thetaSeries L)

The theta series of a discrete subgroup does not vanish at i∞, since it tends to 1.

theorem ZLattice.coe_ne_thetaSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {F : Type u_2} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [CuspFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)] (f : F) : ⇑f ≠ thetaSeries L

The theta series is never a cusp form. For a subgroup Γ of GL(2, ℝ) having ∞ as a cusp, no cusp form on Γ, of any weight, has Θ_L as its underlying function, because Θ_L does not vanish at ∞.

theorem ZLattice.not_isCuspForm_of_coe_eq_thetaSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [Fact (IsCusp OnePoint.infty Γ)] {k : ℤ} {f : ModularForm Γ k} (hf : ⇑f = thetaSeries L) : ¬f.IsCuspForm

A modular form whose underlying function is Θ_L, on a subgroup Γ of GL(2, ℝ) having ∞ as a cusp, is not a cusp form.

theorem ZLattice.isZeroAtImInfty_thetaCoset {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) {γ : E} (hγ : γ ∉ L) : UpperHalfPlane.IsZeroAtImInfty (thetaCoset L γ)

For γ ∉ L the theta series of the translate γ + L tends to 0 at i∞, since no vector of γ + L is zero.

theorem ZLattice.valueAtInfty_thetaCoset {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) {γ : E} (hγ : γ ∉ L) : UpperHalfPlane.valueAtInfty (thetaCoset L γ) = 0

For γ ∉ L the value of the theta series of γ + L at the cusp ∞ is 0.

theorem ZLattice.qExpansion_thetaSeries_coeff_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {h : ℝ} (hh : 0 < h) (hper : ∀ (τ : UpperHalfPlane), thetaSeries L (h +ᵥ τ) = thetaSeries L τ) : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h (thetaSeries L)) = 1

The constant term of the q-expansion with period h of the theta series of a discrete subgroup is 1, whenever the theta series has period h.

theorem ZLattice.IsEven.qExpansion_thetaSeries_coeff_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] (hL : IsEven L) : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 (thetaSeries L)) = 1

For an even lattice, the constant term of the q-expansion of Θ_L in q = exp (2 π i τ) is 1.

theorem ZLattice.IsIntegral.qExpansion_two_thetaSeries_coeff_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] (hL : IsIntegral L) : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 2 (thetaSeries L)) = 1

For an integral lattice, the constant term of the q-expansion of Θ_L with period 2, in exp (π i τ), is 1.

theorem ZLattice.thetaCoset_eq_ofReal_of_re_eq_zero {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) {τ : UpperHalfPlane} (hτ : τ.re = 0) : thetaCoset L γ τ = ↑(∑' (v : ↥L), Real.exp (-(Real.pi * τ.im) * ‖γ + ↑v‖ ^ 2))

On the imaginary axis the theta series of γ + L is real: θ_{γ+L}(i y) = ∑_{v ∈ L} exp (-π y ‖γ + v‖²).

theorem ZLattice.re_thetaCoset_pos {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) [NormedSpace ℝ E] [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (γ : E) {τ : UpperHalfPlane} (hτ : τ.re = 0) : 0 < (thetaCoset L γ τ).re

On the imaginary axis the theta series of γ + L has positive real part (and is real, by ZLattice.thetaCoset_eq_ofReal_of_re_eq_zero).

theorem ZLattice.one_le_re_thetaSeries {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) [NormedSpace ℝ E] [FiniteDimensional ℝ E] [DiscreteTopology ↥L] {τ : UpperHalfPlane} (hτ : τ.re = 0) : 1 ≤ (thetaSeries L τ).re

On the imaginary axis the theta series of a discrete subgroup has real part at least 1, the contribution of the zero vector (and is real, by ZLattice.thetaCoset_eq_ofReal_of_re_eq_zero).

theorem ZLattice.thetaSeries_ne_zero_of_re_eq_zero {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) [NormedSpace ℝ E] [FiniteDimensional ℝ E] [DiscreteTopology ↥L] {τ : UpperHalfPlane} (hτ : τ.re = 0) : thetaSeries L τ ≠ 0

The theta series of a discrete subgroup does not vanish on the imaginary axis.