verfied signal processing algorithms

Stream: general

[Kayla Thomas]

I'm wondering if anyone knows what has been done and, or is being done, in Lean or elsewhere, in terms of formalizing and verifying digital signal processing algorithms, such as the FFT, FIR and IIR filters, etc.

[MohanadAhmed]

Hello Kayla
From the things you mention we probably share an area of interest.

The way I think of it is there is some mathematical theorems that should be in place before doing signal processing type proofs becomes a reasonable proposition. Let's call this necessary math "Mathematics for Signal Processing".

In this repo https://github.com/MohanadAhmed/LeanMathSigProc I am starting to slowly do some of this math but I still think I have a long way.

In #6517 I tried to define DFT (the slow version of FFT but mathematically more malleable )

Any form of signal processing which deals with stochastic signals wil need significant effort to build up the probability part of mathlib.

Finally @Tomas Skrivan and @Eric Wieser might have knowledge of some other relevant efforts.

[Eric Wieser]

While strictly I'm a member of the "signal processing group" at my department, I have nothing to offer here besides agreeing that it would be great to have some results in this area!

[Kayla Thomas]

Thank you for the info. I honestly don't know much about the subject, but I am helping to refactor a signal processing library for work, and I have to ensure that I don't introduce errors while doing so, so formalization came to mind. I'm not really looking to work on formalizing it myself, since I have another formalization project I am already working on, but was hoping maybe there was something already out there.