Stream: maths

Topic: Fourier transform

Gabriel Ebner (Oct 04 2019 at 09:10):

I'd like to do a small project to get to know mathlib, and @Rob Lewis suggested that I could work on Fourier analysis. AFAICT this would require some basic facts about Bochner integrals (such as linearity, etc.), and single-variable derivatives would be nice too. Is anybody working on this?

Johan Commelin (Oct 04 2019 at 09:12):

@Kenny Lau Did you ever formalise anything in this direction?

Patrick Massot (Oct 04 2019 at 09:30):

You should ask @Jeremy Avigad and @Joe about the current status of integration.

Patrick Massot (Oct 04 2019 at 09:30):

It would be really nice to see some move in this direction.

Joe (Oct 04 2019 at 15:23):

@Gabriel Ebner Bochner integral is already defined in the library, though simple properties are not proved yet. But I think I’ll finish that very soon.

Jeremy Avigad (Oct 05 2019 at 01:56):

@Gabriel Ebner An option in the meanwhile is just to axiomatize or sorry the properties of integrals that you need. I trust Joe when he says he'll get to it soon.

Last updated: May 19 2021 at 00:40 UTC