Discrete Fourier transform on `ZMod N`

Stream: Is there code for X?

[David Loeffler]

Do we have any definitions and API for the discrete Fourier transform for a function ZMod N → ℂ?

[Yaël Dillies]

Yes, LeanAPAP#dft

[Yaël Dillies]

My plan for integration in mathlib is:

• general prerequisites
• NNRat.cast (#11203)
• discuss how we expect discrete analysis to look like in mathlib, in particular whether we can satisfyingly avoid the LeanAPAP#dft vs LeanAPAP#cft duplication without making everything full of measurability side conditions
• Discrete Fourier transform, finally

[David Loeffler]

This is for general fg abelian groups , right? I just want the case of cyclic gps with a canonical generator, so the dual of G is identified with G.

[Yaël Dillies]

So what you want is my DFT conposed with an identification between the dual of ZMod n and ZMod n. Correct? That identification already exists in LeanAPAP, but it's private.

[David Loeffler]

What kind of timescale do you envisage for merging this? It sounds like it might not be soon, particularly since there are evidently nontrivial design decisions unsettled.

Perhaps it is best if for now I code up the very simple special cases I need myself, and we can reconcile it with the general treatment from APAP later.

[Michael Stoll]

David Loeffler said:

This is for general fg abelian groups , right? I just want the case of cyclic gps with a canonical generator, so the dual of G is identified with G.

Don't you also need to dix a primitve root of unity of the order the order of your group to get this identification?

[David Loeffler]

I’m fixing exp (2 * pi * I / n).

[Yaël Dillies]

David Loeffler said:

What kind of timescale do you envisage for merging this?

When I started moving things to mathlib five months ago, my project had 170 files. Now it has 55 and I am getting really close to PRing some nontrivial stuff. I envisage it will take another two weeks before #11203 is in, then discrete Fourier analysis will probably take 2-3 months to be absorbed by mathlib + maybe 1-2 months delay because I will be revising for exams.

[Eric Wieser]

Can we somehow avoid needing NNRat.cast before DFTs? I can imagine it's slightly cleaner, but we've managed without it so far elsewhere, so presumably in the short term we can get something in mathlib using Rat?

[Yaël Dillies]

I mean, sure. If you want to skip NNRat.cast, the next step is LeanAPAP#Finset.expect

[Yaël Dillies]

In particular, I want to know whether people think it should exist as a definition

[Eric Wieser]

I assume you meant to use a different linkifier?

[Yaël Dillies]

Yes, fixed

[Yaël Dillies]

Let me start a new thread because there is more to discuss than just the discrete Fourier transform