Theta series of lattices
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremPoisson's summation formula#
Poisson's summation formula over a full lattice L of a finite-dimensional real inner
product space: for a Schwartz function f and v : E,
∑' ℓ : L, f (v + ℓ) = (covolume L)⁻¹ * ∑' m : L^∨, 𝓕 f m * exp (2πi ⟪v, m⟫).
The sign of the phase is the one forced by Mathlib's 𝓕 f w = ∫ x, exp (-2πi ⟪x, w⟫) f x.
SchwartzMap.tsum_eq_tsum_dual_fourier.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(f : SchwartzMap E ℂ) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (v : E) :
∑' (ℓ : ↥L), f (v + ↑ℓ) =
(↑(ZLattice.covolume L MeasureTheory.volume))⁻¹ *
∑' (m : ↥(ZLattice.dual L)),
FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m))
Lean
Formalized in Tau Ceti as SchwartzMap.tsum_eq_tsum_dual_fourier.
Other forms
Poisson's summation formula. Formalized in Tau Ceti as SchwartzMap.tsum_eq_tsum_fourier_span_orthonormalBasis.
SchwartzMap.tsum_eq_tsum_fourier_span_orthonormalBasis.{u_1, u_2} {E : Type u_1}
[NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (f : SchwartzMap E ℂ)
(o : OrthonormalBasis ι ℝ E) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) :
∑' (ℓ : ↥(Submodule.span ℤ (Set.range ⇑o))), f (v + ↑ℓ) =
∑' (m : ↥(Submodule.span ℤ (Set.range ⇑o))),
FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m))
Sources
Uses 1 · Used by 1
TheoremZLattice.IsEven.qExpansion_thetaSeries_coeff#
The coefficients of the q-expansion of the theta series of an even lattice: the m-th
coefficient in q = exp (2 π i τ) is the number r_L(2m) of vectors of half-norm m.
ZLattice.IsEven.qExpansion_thetaSeries_coeff.{u_1} {E : Type u_1} [NormedAddCommGroup E]
{L : Submodule ℤ E} [NormedSpace ℝ E] [FiniteDimensional ℝ E] [DiscreteTopology ↥L]
(hL : ZLattice.IsEven L) (m : ℕ) :
(PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 (ZLattice.thetaSeries L)) =
↑(ZLattice.representationNumber L (2 * ↑m))
Uses 4
TheoremZLattice.IsEven.thetaSeries_slash_T#
The theta series of an even lattice is invariant under T, in every weight:
Θ_L ∣[k] T = Θ_L.
ZLattice.IsEven.thetaSeries_slash_T.{u_1} {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E}
(hL : ZLattice.IsEven L) (k : ℤ) :
SlashAction.map k ModularGroup.T (ZLattice.thetaSeries L) = ZLattice.thetaSeries L
Uses 3
TheoremZLattice.IsEven.thetaCoset_one_vadd#
The translation law of the theta series of a coset of an even lattice: for γ ∈ L^∨,
θ_{γ+L}(τ + 1) = e(q_L(γ)) θ_{γ+L}(τ) with e(q_L(γ)) = exp (π i ‖γ‖²).
ZLattice.IsEven.thetaCoset_one_vadd.{u_1} {E : Type u_1} [NormedAddCommGroup E] {L : Submodule ℤ E}
[InnerProductSpace ℝ E] {γ : E} (hL : ZLattice.IsEven L) (hγ : γ ∈ ZLattice.dual L)
(τ : UpperHalfPlane) :
ZLattice.thetaCoset L γ (1 +ᵥ τ) =
Complex.exp (↑Real.pi * Complex.I * ↑(‖γ‖ ^ 2)) * ZLattice.thetaCoset L γ τ
Uses 3
TheoremZLattice.IsIntegral.det_eq_card_discriminantGroup#
For an integral lattice L, the determinant is the order of the discriminant group
L^∨ ⧸ L. In particular it is a positive integer.
ZLattice.IsIntegral.det_eq_card_discriminantGroup.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : ZLattice.IsIntegral L) :
ZLattice.det L = ↑(Nat.card (ZLattice.DiscriminantGroup L))
Lean
Formalized in Tau Ceti as ZLattice.IsIntegral.det_eq_card_discriminantGroup.
Sources
Uses 1 · Used by 1
TheoremZLattice.IsIntegral.thetaSeries_dual_eq_sum#
For an integral lattice L, the theta series of the dual lattice is the sum of the coset theta
series over the finite discriminant group L^∨ ⧸ L: Θ_{L^∨} = ∑_{γ ∈ A_L} θ_γ. The discriminant
group of an integral lattice is finite (IsIntegral.finite_discriminantGroup), so a Fintype
instance is always available.
ZLattice.IsIntegral.thetaSeries_dual_eq_sum.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L]
[IsZLattice ℝ L] (h : ZLattice.IsIntegral L) [Fintype (ZLattice.DiscriminantGroup L)]
(τ : UpperHalfPlane) :
ZLattice.thetaSeries (ZLattice.dual L) τ = ∑ γ, ZLattice.thetaCosetClass L γ τ
Uses 3
DefinitionZLattice.thetaSeries#
The theta series Θ_L(τ) = ∑_{v ∈ L} exp (π i ‖v‖² τ) of L : Submodule ℤ E. It converges
on ℍ when L is discrete and E is finite-dimensional (ZLattice.summable_thetaSeries).
ZLattice.thetaSeries.{u_1} {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E)
(τ : UpperHalfPlane) : ℂ
DefinitionZLattice.thetaCoset#
The theta series θ_{γ+L}(τ) = ∑_{v ∈ L} exp (π i ‖γ + v‖² τ) of the translate γ + L of
L : Submodule ℤ E. For γ in the dual lattice this is the coset theta series of the coset
γ + L.
ZLattice.thetaCoset.{u_1} {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E)
(τ : UpperHalfPlane) : ℂ
DefinitionZLattice.representationNumber#
The representation number r_L(t): the number of vectors of L of squared norm t. For a
discrete L in a proper space every shell is finite, so this is a genuine count.
ZLattice.representationNumber.{u_1} {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E)
(t : ℝ) : ℕ
Used by 1
DefinitionZLattice.dual#
The dual lattice of L : Submodule ℤ E: the vectors whose inner product with every vector of
L is an integer. It is Mathlib's BilinForm.dualSubmodule of the inner product.
ZLattice.dual.{u} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) :
Submodule ℤ E
DefinitionZLattice.IsEven#
A lattice is even if the squared norm of each of its vectors is an even integer.
ZLattice.IsEven.{u_1} {E : Type u_1} [SeminormedAddCommGroup E] (L : Submodule ℤ E) : Prop
TheoremMilgram's formula#
If L is an even lattice and dim E = 2k, then
∑_{γ ∈ L^∨/L} e(‖γ‖² / 2) = √|L^∨/L| · i^k, where i^k = e(n/8) for n = 2k. The left side
is written as a sum over L^∨ / 1L; ZLattice.dualGaussSum_one rewrites it as a sum over the
discriminant group L^∨/L.
ZLattice.IsEven.dualGaussSum_one_one.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L]
[IsZLattice ℝ L] {k : ℕ} (hL : ZLattice.IsEven L) (hk : Module.finrank ℝ E = 2 * k)
[Fintype (↥(ZLattice.dual L) ⧸ (↑1 • L).submoduleOf (ZLattice.dual L))] :
ZLattice.dualGaussSum L hL 1 1 = ↑√↑(Nat.card (ZLattice.DiscriminantGroup L)) * Complex.I ^ k
Uses 6
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.