Analysis of Boolean functions, Arrow's theorem

Stream: new members

[Joris Roos]

Hi everyone, I'm mainly working in classical harmonic analysis in Euclidean spaces and I've been interested in Lean for a while now, though unfortunately didn't get around to really work with it until very recently. Mainly as a learning exercise I've started this project formalizing some very basic analysis of Boolean functions following Ryan O'Donnell's book Analysis of Boolean functions. The most interesting result formalized so far is probably Arrow's theorem (see Sec. 2.6 in the book). I know there are several formalizations of stronger formulations of Arrow's theorem already (even one using Lean), but I couldn't find any existing formalizations of this Fourier-analytic approach (is there one?). Any comments or thoughts are welcome

[Shreyas Srinivas]

It's a welcome addition.

[Shreyas Srinivas]

I would suggest defining the Boolean fourier transform independently of any mathlib definitions first

[Shreyas Srinivas]

A lot of TCS content isn't available yet

[Daniel Weber]

There is some Fourier transform of boolean functions in https://command-master.github.io/lean-bourgain/, that might be useful

[Joris Roos]

Daniel Weber @Shreyas Srinivas Thanks for the comments. Maybe I wasn't clear: I already have a FT for Boolean functions, I used it to formalize a Fourier-analytic proof of Arrow's theorem, see https://github.com/roos-j/lean-booleanfun

[Yaël Dillies]

Hey Joris! Nice meeting you. I am the author of LeanAPAP, which is a dependency of Daniel's library linked above

[Joris Roos]

Hi Yaël, you too! I saw your very nice project. I suppose I could have used your discrete FT formalization, but for my purpose it was more convenient to do it from scratch; Boolean functions are just a very simple special case :)