The finite Fourier sum of coset theta series

For an integral full lattice L, the character exp (2πi ⟪γ, m⟫) of the dual lattice, with γ ∈ L^∨, is constant on cosets modulo L. It is the exponential of the discriminant pairing of the rational model, transported through ZLattice.ratModelDiscriminantGroupEquiv.

This file identifies the absolutely convergent character-weighted theta sum over L^∨ with ∑ δ : A_L, e(b_L(γ, δ)) θ_δ. This is the finite sum occurring in the vector-valued inversion law. The pairing and its descent are taken from IntegralLattice.discriminantPairing; no new bilinear form on the discriminant group is introduced. Integrality suffices for this splitting, with no evenness or parity restriction on the rank.

The normalization of the finite sum is also recorded: the inverse covolume is the inverse square root of the determinant, and, for integral lattices, of the discriminant group's order.

References

• W. Ebeling, Lattices and Codes, 3rd ed., Chapter 2.

theorem ZLattice.IsIntegral.summable_norm_discriminantPairingChar_mul_thetaTerm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ : DiscriminantGroup L) (τ : UpperHalfPlane) : Summable fun (m : ↥(dual L)) => ‖(hL.discriminantPairingChar γ) (Submodule.Quotient.mk m) * Complex.exp (↑Real.pi * Complex.I * ↑(‖↑m‖ ^ 2) * ↑τ)‖

The character-weighted theta sum over the dual lattice is absolutely convergent.

theorem ZLattice.IsIntegral.tsum_discriminantPairingChar_mul_thetaTerm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) [Fintype (DiscriminantGroup L)] (γ : DiscriminantGroup L) (τ : UpperHalfPlane) : ∑' (m : ↥(dual L)), (hL.discriminantPairingChar γ) (Submodule.Quotient.mk m) * Complex.exp (↑Real.pi * Complex.I * ↑(‖↑m‖ ^ 2) * ↑τ) = ∑ δ : DiscriminantGroup L, (hL.discriminantPairingChar γ) δ * thetaCosetClass L δ τ

Splitting the character-weighted theta sum over L^∨ into cosets of L gives the finite Fourier sum of the coset theta series on the discriminant group.

theorem ZLattice.IsIntegral.tsum_exp_inner_mul_thetaTerm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) [Fintype (DiscriminantGroup L)] (γ : ↥(dual L)) (τ : UpperHalfPlane) : ∑' (m : ↥(dual L)), Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ ↑γ ↑m)) * Complex.exp (↑Real.pi * Complex.I * ↑(‖↑m‖ ^ 2) * ↑τ) = ∑ δ : DiscriminantGroup L, (hL.discriminantPairingChar (Submodule.Quotient.mk γ)) δ * thetaCosetClass L δ τ

In representative notation, the weighted dual theta sum is the finite sum with coefficients e(b_L(γ, δ)).

theorem ZLattice.IsIntegral.sum_discriminantPairingChar_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) [Fintype (DiscriminantGroup L)] (γ : DiscriminantGroup L) (τ : UpperHalfPlane) : ∑ δ : DiscriminantGroup L, (hL.discriminantPairingChar γ) (-δ) * thetaCosetClass L δ τ = ∑ δ : DiscriminantGroup L, (hL.discriminantPairingChar γ) δ * thetaCosetClass L δ τ

Negating the phase in the finite Fourier sum leaves it unchanged, since the coset theta series at δ and -δ agree.