The inversion law of theta series

Let L be a full lattice in a real inner product space E of even dimension n = 2k, with dual lattice L^∨. Poisson summation over L, applied to the Gaussian x ↦ exp (π i (-1/τ) ‖x‖²), whose Fourier transform is (-i)^k τ^k exp (π i τ ‖y‖²), gives the behaviour of theta series under the inversion S : τ ↦ -1/τ:

• at a general translate v : E, θ_{v+L}(-1/τ) = (covol L)⁻¹ (-i)^k τ^k ∑_{m ∈ L^∨} e(⟪v, m⟫) exp (π i ‖m‖² τ), with e(x) = exp (2 π i x);
• at v = 0, Θ_L(-1/τ) = (covol L)⁻¹ (-i)^k τ^k Θ_{L^∨}(τ), that is Θ_L ∣[k] S = (-i)^k (covol L)⁻¹ Θ_{L^∨} in weight k;
• for integral L and γ ∈ L^∨, splitting the dual sum into the cosets of L gives the vector-valued law θ_γ(-1/τ) = (covol L)⁻¹ (-i)^k τ^k ∑_{δ ∈ L^∨/L} e(b_L(γ, δ)) θ_δ(τ).

No integrality is needed for the first two statements. The phase e(+⟪v, m⟫) is the one produced by Poisson summation with Mathlib's Fourier transform; since θ_δ = θ_{-δ}, the vector-valued law also holds with the opposite phase (ZLattice.IsIntegral.sum_discriminantPairingChar_neg).

Main statements

• ZLattice.thetaCoset_S_smul: the inversion law at a general translate.
• ZLattice.thetaSeries_S_smul, ZLattice.thetaSeries_slash_S: the scalar inversion law.
• ZLattice.IsUnimodular.thetaSeries_slash_S: the scalar inversion law of a unimodular lattice.
• ZLattice.IsIntegral.thetaCoset_S_smul, ZLattice.IsIntegral.thetaCoset_slash_S: the vector-valued inversion law, pointwise and in slash form.

References

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

theorem ZLattice.thetaCoset_S_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) (v : E) (τ : UpperHalfPlane) : thetaCoset L v (ModularGroup.S • τ) = (↑(covolume L MeasureTheory.volume))⁻¹ * ((-Complex.I) ^ k * ↑τ ^ k) * ∑' (m : ↥(dual L)), Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m)) * Complex.exp (↑Real.pi * Complex.I * ↑(‖↑m‖ ^ 2) * ↑τ)

The inversion law of theta series at a general translate: if dim E = 2k, then for every v : E and τ ∈ ℍ, θ_{v+L}(-1/τ) = (covol L)⁻¹ (-i)^k τ^k ∑_{m ∈ L^∨} e(⟪v, m⟫) exp (π i ‖m‖² τ).

theorem ZLattice.thetaSeries_S_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) (τ : UpperHalfPlane) : thetaSeries L (ModularGroup.S • τ) = (↑(covolume L MeasureTheory.volume))⁻¹ * ((-Complex.I) ^ k * ↑τ ^ k) * thetaSeries (dual L) τ

The inversion law of theta series: if dim E = 2k, then for τ ∈ ℍ, Θ_L(-1/τ) = (covol L)⁻¹ (-i)^k τ^k Θ_{L^∨}(τ).

theorem ZLattice.thetaSeries_slash_S {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) : SlashAction.map (↑k) ModularGroup.S (thetaSeries L) = ((-Complex.I) ^ k * (↑(covolume L MeasureTheory.volume))⁻¹) • thetaSeries (dual L)

The inversion law of theta series in slash form: if dim E = 2k, then in weight k, Θ_L ∣[k] S = (-i)^k (covol L)⁻¹ Θ_{L^∨}.

theorem ZLattice.IsUnimodular.thetaSeries_slash_S {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hU : IsUnimodular L) (hk : Module.finrank ℝ E = 2 * k) : SlashAction.map (↑k) ModularGroup.S (thetaSeries L) = (-Complex.I) ^ k • thetaSeries L

The inversion law of a unimodular lattice: if L = L^∨ and dim E = 2k, then in weight k, Θ_L ∣[k] S = (-i)^k Θ_L.

theorem ZLattice.IsIntegral.thetaCoset_S_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsIntegral L) [Fintype (DiscriminantGroup L)] (hk : Module.finrank ℝ E = 2 * k) (γ : ↥(dual L)) (τ : UpperHalfPlane) : thetaCoset L (↑γ) (ModularGroup.S • τ) = (↑(covolume L MeasureTheory.volume))⁻¹ * ((-Complex.I) ^ k * ↑τ ^ k) * ∑ δ : DiscriminantGroup L, (hL.discriminantPairingChar (Submodule.Quotient.mk γ)) δ * thetaCosetClass L δ τ

The vector-valued inversion law of coset theta series: if L is integral and dim E = 2k, then for γ ∈ L^∨ and τ ∈ ℍ, θ_{γ+L}(-1/τ) = (covol L)⁻¹ (-i)^k τ^k ∑_{δ ∈ L^∨/L} e(b_L(γ, δ)) θ_{δ+L}(τ), a finite sum over the discriminant group.

theorem ZLattice.IsIntegral.thetaCoset_slash_S {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsIntegral L) [Fintype (DiscriminantGroup L)] (hk : Module.finrank ℝ E = 2 * k) (γ : ↥(dual L)) : SlashAction.map (↑k) ModularGroup.S (thetaCoset L ↑γ) = ((-Complex.I) ^ k * (↑(covolume L MeasureTheory.volume))⁻¹) • ∑ δ : DiscriminantGroup L, (hL.discriminantPairingChar (Submodule.Quotient.mk γ)) δ • thetaCosetClass L δ

In weight k, inversion sends a coset theta series to a finite linear combination of coset theta series, with coefficients given by the discriminant pairing characters.