Poisson Summation on Lattices

Stream: Is there code for X?

[Gareth Ma]

Is there Poisson summation formula over lattices, perhaps from other projects? Also somewhat related, what is the correct notion of "dual lattice" in Mathlib?

[Edward van de Meent]

to answer your second question: use OrderDual, which will then get the instance via OrderDual.instLattice

[Edward van de Meent]

note the available notation αᵒᵈ for the type synonym

[Gareth Ma]

I'm not talking about the partial ordered set-kind lattice, but rather something like Zlattice, so a discrete full rank subgroup

[Edward van de Meent]

i don't know that we have that, sadly? at least it didn't exist a few months ago...

[Gareth Ma]

#docs IsZlattice

[Gareth Ma]

i suck at this

[Gareth Ma]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Zlattice/Basic.html#IsZlattice

[Edward van de Meent]

i see that i am not well versed in this corner of mathlib, so i'll shut up :face_with_hand_over_mouth:

[Jireh Loreaux]

Why in the world is a normed structure required in the definition of docs#IsZlattice ?

[Edward van de Meent]

because you want the topological structure to be related to the algebraic one, i'm guessing?

[Edward van de Meent]

(topological structure is for discreteness)

[Jireh Loreaux]

sure, but we have classes for that with far weaker assumptions.

[Jireh Loreaux]

docs#TopologicalSpace, docs#ContinuousAdd, docs#ContinuousSMul or docs#ContinuousConstSMul, for example.

[Jireh Loreaux]

Also, the name is wrong, it should be IsZLattice, not IsZlattice.

[Johan Commelin]

Lattices come with an inner product and a norm, right?

[Johan Commelin]

Informally, I mean

[Jireh Loreaux]

ah, if so then that's just my ignorance showing.

[Scott Carnahan]

Sometimes lattices are defined to be free abelian groups with nondegenerate inner products, and sometimes they are defined to be finite covolume discrete subgroups of Lie groups. The Poisson summation formula is normally formulated for the second case, where the Lie group is a real vector space without a specified inner product. However, the formula is often specialized to the first case, using the inner product to identify the real vector space with its dual.

[Antoine Chambert-Loir]

The word is also used to describe subsets of Q_p vector spaces which are free Z_p modules of the same rank!

[Gareth Ma]

I am aware there are multiple definitions of lattices (at least the "abelian group with inner product" and "discrete subgroup of e.g. R^n"). For my purpose I'm just looking for the simplest of all, that $\sum_{x \in \Lambda} f(x) = \frac{1}{\mathrm{Vol}(\mathbb{R}^n / \Lambda)} \sum_{y \in \widehat{\Lambda}} \widehat{f}(y)$. The responses above (and my grep searches) suggests it's not in Mathlib, so my next question is how should I even state the theorem? Here is the existing Poisson summation formula:

-- with additional conditions
example {f : C(ℝ, ℂ)} (x : ℝ) :
    ∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) := by
  sorry

So I tried to mimick the definition and define the following:

import Mathlib.LinearAlgebra.Dual
import Mathlib.Algebra.Module.Zlattice.Basic
import Mathlib.Analysis.Fourier.FourierTransform
import Mathlib.Analysis.Fourier.PoissonSummation
open Module FiniteDimensional Zspan FourierTransform
universe u
variable {d : ℕ} (L : AddSubgroup (EuclideanSpace ℝ (Fin d))) [DiscreteTopology L] [IsZlattice ℝ L]

example {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ} (c : EuclideanSpace ℝ (Fin d)) :
    ∑' x : L, f (c +ᵥ (n : EuclideanSpace ℝ (Fin d)))
      = ∑' y : Dual ℤ L, 𝓕 f ?_ * fourier ?_ ?_ := by
  sorry

However, I am not sure how to fill in the ?_ blanks. Can someone help?

[Gareth Ma]

Also a not so relevant question, I tried stating the theorem for $L = \mathbb{R}^n$ instead (since you can reduce the case for general lattices to it), but I don't know how to write "$\mathbb{Z}^n$" with a natural coercion/map to $\mathbb{R}^n$

[Gareth Ma]

(The reason I use EuclideanSpace \R (Fin d) instead of Fin d \to \R or something is because it has an inner product space structure along with a bunch of stuff that the Real.fourierTransform (the \MCF) seems to need)

[Gareth Ma]

@David Loeffler (Hope you don't mind)
Also I just found out about VectorFourier, is that the correct thing to use here?

[Antoine Chambert-Loir]

I would probably go the other way. The Fourier transform has been set up in a very general way in mathlib, see docs#VectorFourier.fourierIntegral, so you could get the Poisson summation formula in the similar generality, starting from two “lattices” $L$ and $M$ with a bilinear form (that may or not induce an isomorphism from $L$ to the dual of $M$, consider the scalar extensions $V$ and $W$ and the corresponding bilinear form.

Now, the main difficulty is probably that mathlib is still missing many results about Fourier transforms in this generality. (Are there Fourier series?)

[Kalle Kytölä]

Antoine Chambert-Loir said:

Now, the main difficulty is probably that mathlib is still missing many results about Fourier transforms in this generality. (Are there Fourier series?)

I don't think there is anything about more than 1-dimensional Fourier series (docs#fourierBasis); see this thread. Doing the higher-dimensional Fourier series should naturally involve lattices and their quotient tori.

It is quite unclear to me, however, what is the right generality and approach for Fourier series for mathlib. For example, taking quotients by full-rank lattices leads to compact tori and Fourier series, and maybe the $L^2$ theory with Hilbert bases just needs to be restricted to such cases? Should the Fourier series theory be done separately or be obtained more directly from Fourier transforms (as Antoine indeed seems to suggest)?

(In what we need for our project, we will probably for the moment only work with products of circles, thus "straight tori" $\R^d/\Z^d$, and Fourier series for $L^2$ functions on them. But this is most likely not the mathlib generality.)

[Alex Kontorovich]

At some point, @Heather Macbeth and I were pursuing this. See, e.g., #6223 for the "unfolding trick" docs#QuotientAddGroup.integral_mul_eq_integral_automorphize_mul. We wanted to prove Poisson as a "baby" trace formula, which indeed relies on the $L^2$ theory for the $d$-torus $\R^d/\Lambda$. Hopefully we'll get back to it some day...

[Gareth Ma]

If I am understanding the discussion correctly, there are/were multiple projects that needs some kind of multi-dimensional Fourier series. Maybe it is a good idea for us to ping everyone come up with some appropriate generality for Mathlib and then formalise it! Also helps to deduplicate work. Full disclaimer, I don't know anything beyond maybe the most basic theory found in UG textbooks...

[Gareth Ma]

Meanwhile I think Poisson summation might be doable via the VectorFourier.fourierIntegral Antoine linked above, so I can try that