feat(Foundations/Combinatorics/BooleanFunctions): Fourier expansion, Plancherel, and Parseval#596
Conversation
…Plancherel, and Parseval Formalize Chapter 1 of O'Donnell's "Analysis of Boolean Functions" through Plancherel and Parseval. Sets up `HammingCube n = Fin n → ZMod 2` and the space `BooleanFunction n` of real-valued functions on the cube, carrying the uniform-measure L² inner product `⟪f, g⟫ = 𝔼[f·g]` as an `InnerProductSpace ℝ`. `BooleanFunction` is a `def` (not `abbrev`) to keep typeclass resolution from seeing through to the Pi-type sup norm. Defines the parity functions `χ S` and Fourier coefficients `𝓕 f S = ⟪f, χ S⟫`, then proves the Fourier expansion theorem (Theorem 1.1, existence and uniqueness) and orthonormality of the parity functions (Theorem 1.5). Plancherel and Parseval follow from packaging the parity functions as an `OrthonormalBasis` and applying Mathlib's `sum_inner_mul_inner`. Ported from the standalone `SamuelSchlesinger/analysis-of-boolean-functions` repo; downstream content (variance, convolution, BLR, density theorems) is left for follow-up.
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
A couple of small questions about definitions before I look closer at the proofs that follow.
| theorem ext {f g : BooleanFunction n} (h : ∀ x, f x = g x) : f = g := | ||
| DFunLike.ext f g h | ||
|
|
||
| @[simp] theorem zero_apply (x : HammingCube n) : (0 : BooleanFunction n) x = 0 := rfl |
There was a problem hiding this comment.
I think the new way to get these kind of theorems is via the classes added in leanprover-community/mathlib4#37779. I've just merged a Mathlib bump so that you can try this out.
There was a problem hiding this comment.
Ooh neat, thanks for pointing it out.
| /-! ### The Hamming cube and the space of Boolean functions -/ | ||
|
|
||
| /-- The Hamming cube `𝔽₂ⁿ`, modelled as `Fin n → ZMod 2`. -/ | ||
| abbrev HammingCube (n : ℕ) := Fin n → ZMod 2 |
There was a problem hiding this comment.
Could you explain why this representation is the most convenient? Both for my own understanding reviewing and the sake of documentation.
There was a problem hiding this comment.
Another natural representation would be Fin n -> Bool, which I initially used in my first draft. However, the book uses F_2 and the additive group structure on F_2 is the right one to be thinking about when we think about parities, etc. Thus, you end up translating back and forth anyways.
Further, when you get to the later chapters, we begin to generalize to arbitrary characters of abelian groups, so starting there is more illustrative for when we go to lift some of these definitions and theorems to characters of arbitrary Abelian groups.
Responded! My one thought is that as a definition in the standalone formalization, HammingCube using F_2 makes sense, but perhaps in CSLib we want HammingCube to use Bool, define it in a more general place, and eat the translation costs here. |
|
I'm realizing now that a lot of this stuff is in Mathlib under names I didn't know to look for, already in the arbitrary Abelian group generality. I think it would still be nice to have the O'Donnell interface, but maybe re-deriving it from the Mathlib work is a better approach. Going to make a PR targeting this one in my personal repo to try and understand how much better that ends up being. Edit: didn't end up helping, maybe a bridge to |
2 participants
Formalizes Chapter 1 of O'Donnell's "Analysis of Boolean Functions" through Plancherel and Parseval.
Defines
HammingCube n = Fin n → ZMod 2and the spaceBooleanFunction nof real-valued functions on the cube, carrying the uniform-measure L² inner product⟪f, g⟫ = 𝔼[f·g]as anInnerProductSpace ℝ.Defines the parity functions
χ Sand Fourier coefficients𝓕 f S = ⟪f, χ S⟫, then proves the Fourier expansion theorem (Theorem 1.1, existence and uniqueness) and orthonormality of the parity functions (Theorem 1.5). Plancherel and Parseval follow from packaging the parity functions as anOrthonormalBasisand applying Mathlib'ssum_inner_mul_inner.Ported from my
SamuelSchlesinger/analysis-of-boolean-functionsrepo. The rest of Chapter 1 from that repository is left for a follow-up, this first PR felt rightsized.Claude Code (with Opus 4.7 xHigh) was used as a coding assistant in the original repository, and in the port as well.