Milgram's formula for a positive definite even lattice

Let L be an even full lattice in a real inner product space E of even dimension n = 2k, with discriminant group A_L = L^∨ / L and quadratic phase e(q_L(γ)) = exp (π i ‖γ‖²) on A_L (ZLattice.IsEven.discriminantQuadraticChar). Milgram's formula evaluates the Gauss sum of the discriminant form:

∑_{γ ∈ A_L} e(q_L(γ)) = √|A_L| · e(n/8),

where e(n/8) = i^k. It is the case a = c = 1 of the reciprocity law for the Gauss sums of L (ZLattice.IsEven.gaussSum_eq_mul_dualGaussSum), whose left side is then 1: the law reads 1 = (covol L)⁻¹ i^k ∑_{γ ∈ A_L} e(-q_L(γ)), and complex conjugation, together with covol L = √|A_L|, turns it into the formula. The formula thus comes from the asymptotics of theta series near the cusps, as in Milnor–Husemoller, and is independent of the finite arithmetic of the rational model behind TauCeti.IntegralLattice.gaussSign_discriminantQuadraticModule_eq_sigPos_sub_sigNeg.

Since √|A_L| > 0, the formula determines n modulo 8 from the discriminant form: 8 ∣ n exactly when the Gauss sum is the positive real number √|A_L|. For an even unimodular lattice of even rank the group A_L is trivial and the sum is 1, so 8 ∣ n; the general statement for even unimodular lattices of any rank is ZLattice.IsEven.eight_dvd_finrank. The root lattice A₂, of rank 2 with |A_L| = 3, has Gauss sum i √3.

Main statements

• ZLattice.IsEven.sum_discriminantQuadraticChar: Milgram's formula ∑_{γ ∈ A_L} e(q_L(γ)) = √|A_L| · i^k for an even lattice of rank 2k.
• ZLattice.IsEven.eight_dvd_finrank_iff_sum_discriminantQuadraticChar_eq: for an even lattice of even rank n, 8 ∣ n if and only if ∑_{γ ∈ A_L} e(q_L(γ)) = √|A_L|.
• TauCeti.IntegralLattice.finsum_discriminantQuadraticChar_realModel_typeARootLattice_two: the Gauss sum of the discriminant form of the root lattice A₂ is i √3.

References

• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Springer, 1973, Appendix 4.
• B. Schoeneberg, Elliptic Modular Functions, Springer, 1974, Chapter IX.

theorem ZLattice.IsEven.sum_discriminantQuadraticChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {k : ℕ} (hL : IsEven L) (hk : Module.finrank ℝ E = 2 * k) [Fintype (DiscriminantGroup L)] : ∑ γ : DiscriminantGroup L, hL.discriminantQuadraticChar γ = ↑√↑(Nat.card (DiscriminantGroup L)) * Complex.I ^ k

Milgram's formula. If L is an even lattice and dim E = 2k, then ∑_{γ ∈ L^∨/L} e(q_L(γ)) = √|L^∨/L| · i^k, where i^k = e(n/8) for n = 2k.

theorem ZLattice.IsEven.eight_dvd_finrank_iff_sum_discriminantQuadraticChar_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (hn : Even (Module.finrank ℝ E)) [Fintype (DiscriminantGroup L)] : 8 ∣ Module.finrank ℝ E ↔ ∑ γ : DiscriminantGroup L, hL.discriminantQuadraticChar γ = ↑√↑(Nat.card (DiscriminantGroup L))

The rank modulo 8 from Milgram's formula. For an even lattice of even rank n, 8 ∣ n if and only if the Gauss sum ∑_{γ ∈ L^∨/L} e(q_L(γ)) is the positive real number √|L^∨/L|.

theorem TauCeti.IntegralLattice.finsum_discriminantQuadraticChar_realModel_typeARootLattice_two : ∑ᶠ (γ : ZLattice.DiscriminantGroup ((typeARootLattice 2).realModel ⋯)), ⋯.discriminantQuadraticChar γ = ↑√3 * Complex.I

Milgram's formula for A₂. The Gauss sum of the discriminant form of the real model of the root lattice A₂, of rank 2 and determinant 3, is i √3. The discriminant group is finite, so the finsum is its finite sum.