D-dimensional Fourier series

Stream: Is there code for X?

[Niklas Halonen]

Is there code for the d-dimensional Fourier series? I found code for one dimension.

@Kalle Kytölä, a couple others and I started looking for ways to generalize the code in AddCircle.lean.

[Oliver Nash]

I don't think we have anything more for Fourier series.

One thing I think is worth considering is whether our Fourier series should involve the concrete type docs#AddCircle or whether they could be set up to work relative to an abstract characterisation of the circle (or tori). I made a similar remark a while ago here.

This raises the question of what is a convenient characterisation of the circle.
I think a compact connected abelian topological group with no small subgroups is a real torus. So that just leaves the dimension question. I guess one could look at the size of the automorphism group but maybe more convenient is to require the existence of a norm and demand $‖x‖ = ‖y‖ ↔ x = I(y)$ for some involution $I$.

[Scott Carnahan]

Perhaps the fact that the only finite subgroups are cyclic is helpful.