Fourier analysis on the Boolean cube

The character of a set S of coordinates is χ_S x = ∏_{i ∈ S} (-1) ^ (x i) (BitString.chi), the sign of the parity of the bits of x : ι → Bool in S (BitString.chi_eq_neg_one_pow_parityOn), with values in any commutative ring R; Fourier analysis takes R = ℝ, where the sign of a bit is BitString.signVal. Bit strings add coordinatewise modulo two, (x + y) i = (x i ^^ y i), through Mathlib's Boolean ring structure on Bool, and the characters turn sums into products (BitString.chi_add): they are additive characters of the cube (BitString.chiChar), whose sums are Mathlib's AddChar.sum_eq_ite. The characters are orthonormal for the uniform expectation (BitString.expect_chi_mul_chi), and every real function on the cube is the sum of its Fourier expansion f = ∑_S f̂(S) χ_S, with the Fourier coefficients f̂(S) = 𝔼_x f x χ_S x (BitString.fourierCoeff, BitString.sum_fourierCoeff_mul_chi), which are unique (BitString.fourierCoeff_sum_mul_chi), so the Fourier transform is a linear equivalence (BitString.fourierTransform). The expectation of a product is the sum of products of coefficients (Plancherel, BitString.expect_mul_eq_sum_fourierCoeff_mul), so the squared coefficients of a function with values ±1 sum to one (BitString.sum_fourierCoeff_sq_signVal). For Boolean functions read as signs, correlation is one minus twice the relative Hamming distance (BitString.expect_signVal_mul_signVal), so the coefficient on S measures the distance to the parity on S (BitString.fourierCoeff_signVal) O'Donnell, Chapter 1.

The coefficients are named BitString.fourierCoeff; Mathlib's root fourierCoeff is the Fourier coefficient on the circle, so the name is meant to be used qualified.

Main definitions

• Cslib.BitString.chi: the character of a set of coordinates, with values in a commutative ring, and Cslib.BitString.chiChar the same as an additive character.
• Cslib.BitString.fourierCoeff: the Fourier coefficient of a real function on the cube, and Cslib.BitString.fourierCoeffₗ the same as a linear map.
• Cslib.BitString.fourierTransform: the Fourier transform, as a linear equivalence.

Main results

• Cslib.BitString.expect_chi_mul_chi: the characters are orthonormal.
• Cslib.BitString.chi_add, Cslib.BitString.chi_mul_chi: the characters are multiplicative, in the input and in the set.
• Cslib.BitString.sum_fourierCoeff_mul_chi: the Fourier expansion.
• Cslib.BitString.fourierCoeff_sum_mul_chi, Cslib.BitString.fourierCoeff_injective: uniqueness of the Fourier coefficients.
• Cslib.BitString.expect_mul_eq_sum_fourierCoeff_mul: Plancherel's identity.
• Cslib.BitString.sum_fourierCoeff_sq_signVal: Parseval's identity for functions with values ±1; so their coefficients have square and absolute value at most one (Cslib.BitString.fourierCoeff_sq_signVal_le_one, Cslib.BitString.abs_fourierCoeff_signVal_le_one) and their spectral norm is at least one (Cslib.BitString.one_le_sum_abs_fourierCoeff_signVal).
• Cslib.BitString.expect_signVal_mul_signVal, Cslib.BitString.fourierCoeff_signVal: the correlation of two Boolean functions is one minus twice their relative Hamming distance.

References

• R. O'Donnell, Analysis of Boolean Functions

def Cslib.BitString.chi {ι : Type u_1} (R : Type u_2) [CommRing R] (S : Finset ι) (x : ι → Bool) : R

The character of a set S of coordinates, with values in a commutative ring R: the product of the signs (-1) ^ xᵢ over S, the sign of the parity of the bits in S (chi_eq_neg_one_pow_parityOn). The Fourier analysis of real functions uses chi ℝ.

@[simp]

theorem Cslib.BitString.chi_empty {ι : Type u_1} {R : Type u_2} [CommRing R] (x : ι → Bool) : chi R ∅ x = 1

The character of the empty set is the constant 1.

def Cslib.BitString.chiChar {ι : Type u_1} (R : Type u_2) [CommRing R] (S : Finset ι) : AddChar (ι → Bool) R

The character of S, as an additive character of the cube: it sends sums of bit strings, their coordinatewise exclusive or, to products.

@[simp]

theorem Cslib.BitString.coe_chiChar {ι : Type u_1} {R : Type u_2} [CommRing R] (S : Finset ι) : ⇑(chiChar R S) = chi R S

The additive character chiChar R S is the character chi R S as a function.

theorem Cslib.BitString.chi_add {ι : Type u_1} {R : Type u_2} [CommRing R] (S : Finset ι) (x y : ι → Bool) : chi R S (x + y) = chi R S x * chi R S y

Characters are multiplicative: the character of the sum of two bit strings, their coordinatewise exclusive or, is the product of their characters.

@[simp]

theorem Cslib.BitString.chi_zero {ι : Type u_1} {R : Type u_2} [CommRing R] (S : Finset ι) : chi R S 0 = 1

Every character is 1 at the all-false bit string.

theorem Cslib.BitString.chi_eq_neg_one_pow_parityOn {ι : Type u_1} {R : Type u_2} [CommRing R] (S : Finset ι) (x : ι → Bool) : chi R S x = (-1) ^ (parityOn S x).toNat

The character of S is the sign of the parity of the bits in S.

theorem Cslib.BitString.chi_mul_self {ι : Type u_1} {R : Type u_2} [CommRing R] (S : Finset ι) (x : ι → Bool) : chi R S x * chi R S x = 1

A character squares to one.

theorem Cslib.BitString.chi_mul_chi {ι : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq ι] (S T : Finset ι) (x : ι → Bool) : chi R S x * chi R T x = chi R (symmDiff S T) x

Characters multiply by the symmetric difference of their sets.

theorem Cslib.BitString.chi_union {ι : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq ι] {S T : Finset ι} (h : Disjoint S T) (x : ι → Bool) : chi R (S ∪ T) x = chi R S x * chi R T x

The character of a disjoint union is the product of the characters.

theorem Cslib.BitString.chi_update_of_notMem {ι : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq ι] {i : ι} {S : Finset ι} (hi : i ∉ S) (x : ι → Bool) (b : Bool) : chi R S (Function.update x i b) = chi R S x

Changing a bit outside S leaves the character of S unchanged.

theorem Cslib.BitString.chi_update_of_mem {ι : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq ι] {i : ι} {S : Finset ι} (hi : i ∈ S) (x : ι → Bool) (b : Bool) : chi R S (Function.update x i b) = (-1) ^ b.toNat * chi R (S.erase i) x

Setting a bit in S to b splits off the sign (-1) ^ b from the character of S.

theorem Cslib.BitString.chi_eq_prod_signVal {ι : Type u_1} (S : Finset ι) (x : ι → Bool) : chi ℝ S x = ∏ i ∈ S, signVal (x i)

The real character of S is the product of the real signs of the bits in S.

theorem Cslib.BitString.chi_singleton {ι : Type u_1} (i : ι) (x : ι → Bool) : chi ℝ {i} x = signVal (x i)

The real character of a single coordinate is the sign of that bit.

theorem Cslib.BitString.chi_eq_signVal_parityOn {ι : Type u_1} (S : Finset ι) (x : ι → Bool) : chi ℝ S x = signVal (parityOn S x)

The real character of S is the real sign of the parity of the bits in S.

@[simp]

theorem Cslib.BitString.abs_chi {ι : Type u_1} (T : Finset ι) (x : ι → Bool) : |chi ℝ T x| = 1

A real character has absolute value one.

@[simp]

theorem Cslib.BitString.chiChar_eq_zero_iff {ι : Type u_1} {S : Finset ι} : chiChar ℝ S = 0 ↔ S = ∅

The character of S is the trivial additive character exactly when S is empty.

theorem Cslib.BitString.sum_chi_mul_chi {ι : Type u_1} [Fintype ι] (x y : ι → Bool) : ∑ S : Finset ι, chi ℝ S x * chi ℝ S y = if x = y then 2 ^ Fintype.card ι else 0

The characters at two points, summed over all sets, detect equality of the points.

theorem Cslib.BitString.chi_eq_prod_univ {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing R] (S : Finset ι) (x : ι → Bool) : chi R S x = ∏ i : ι, if i ∈ S then (-1) ^ (x i).toNat else 1

The character as a product over all coordinates.

theorem Cslib.BitString.sum_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : ∑ x : ι → Bool, chi ℝ S x = if S = ∅ then 2 ^ Fintype.card ι else 0

The characters of nonempty sets sum to zero.

theorem Cslib.BitString.expect_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : (Finset.univ.expect fun (x : ι → Bool) => chi ℝ S x) = if S = ∅ then 1 else 0

The characters of nonempty sets have expectation zero.

theorem Cslib.BitString.expect_chi_mul_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S T : Finset ι) : (Finset.univ.expect fun (x : ι → Bool) => chi ℝ S x * chi ℝ T x) = if S = T then 1 else 0

The characters are orthonormal.

noncomputable def Cslib.BitString.fourierCoeff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (S : Finset ι) : ℝ

The Fourier coefficient of f on S: the correlation of f with the character of S.

theorem Cslib.BitString.fourierCoeff_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff f S = (∑ x : ι → Bool, f x * chi ℝ S x) / 2 ^ Fintype.card ι

The Fourier coefficient as a normalised sum.

theorem Cslib.BitString.fourierCoeff_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => f x + g x) S = fourierCoeff f S + fourierCoeff g S

The Fourier coefficients are additive.

theorem Cslib.BitString.fourierCoeff_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => f x - g x) S = fourierCoeff f S - fourierCoeff g S

The Fourier coefficients commute with subtraction.

theorem Cslib.BitString.fourierCoeff_const_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) (f : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => c * f x) S = c * fourierCoeff f S

The Fourier coefficients commute with scaling.

theorem Cslib.BitString.fourierCoeff_chi_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : Finset ι) (f : (ι → Bool) → ℝ) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => chi ℝ T x * f x) S = fourierCoeff f (symmDiff T S)

Multiplying by a character shifts the coefficients by the symmetric difference.

theorem Cslib.BitString.fourierCoeff_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : ℝ) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => c) S = if S = ∅ then c else 0

A constant has all its weight on the empty set.

theorem Cslib.BitString.fourierCoeff_signVal_parityOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S U : Finset ι) : fourierCoeff (fun (x : ι → Bool) => signVal (parityOn S x)) U = if U = S then 1 else 0

A parity, read as ±1, is the character of its set, so all its weight is on that set.

@[simp]

theorem Cslib.BitString.fourierCoeff_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : fourierCoeff f ∅ = Finset.univ.expect fun (x : ι → Bool) => f x

The coefficient on the empty set is the expectation.

theorem Cslib.BitString.sum_fourierCoeff_mul_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (x : ι → Bool) : ∑ S : Finset ι, fourierCoeff f S * chi ℝ S x = f x

The Fourier expansion: every function is the sum of its characters weighted by its Fourier coefficients.

theorem Cslib.BitString.fourierCoeff_sum_mul_chi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : Finset ι → ℝ) (T : Finset ι) : fourierCoeff (fun (x : ι → Bool) => ∑ S : Finset ι, c S * chi ℝ S x) T = c T

The Fourier coefficients are unique: a combination of characters has its weights as coefficients.

theorem Cslib.BitString.fourierCoeff_injective {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Function.Injective fourierCoeff

A function is determined by its Fourier coefficients.

noncomputable def Cslib.BitString.fourierCoeffₗ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : ((ι → Bool) → ℝ) →ₗ[ℝ] ℝ

The Fourier coefficient on S, as a linear map.

@[simp]

theorem Cslib.BitString.fourierCoeffₗ_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (f : (ι → Bool) → ℝ) : (fourierCoeffₗ S) f = fourierCoeff f S

The linear map fourierCoeffₗ S sends f to its Fourier coefficient on S.

noncomputable def Cslib.BitString.fourierTransform {ι : Type u_1} [Fintype ι] [DecidableEq ι] : ((ι → Bool) → ℝ) ≃ₗ[ℝ] Finset ι → ℝ

The Fourier transform, sending a real function on the cube to its Fourier coefficients, as a linear equivalence: its inverse is the Fourier expansion.

@[simp]

theorem Cslib.BitString.fourierTransform_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : fourierTransform f = fourierCoeff f

The Fourier transform sends a function to its Fourier coefficients.

@[simp]

theorem Cslib.BitString.fourierTransform_symm_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : Finset ι → ℝ) (x : ι → Bool) : fourierTransform.symm c x = ∑ S : Finset ι, c S * chi ℝ S x

The inverse Fourier transform sends weights c to the combination ∑ S, c S * χ_S.

theorem Cslib.BitString.expect_mul_eq_sum_fourierCoeff_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => f x * g x) = ∑ S : Finset ι, fourierCoeff f S * fourierCoeff g S

Plancherel's identity: the expectation of a product is the sum of the products of the Fourier coefficients.

theorem Cslib.BitString.expect_sq_eq_sum_fourierCoeff_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => f x ^ 2) = ∑ S : Finset ι, fourierCoeff f S ^ 2

Parseval's identity.

theorem Cslib.BitString.sum_fourierCoeff_sq_signVal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) : ∑ S : Finset ι, fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2 = 1

Parseval's identity for functions with values ±1: the squared Fourier coefficients sum to one.

theorem Cslib.BitString.fourierCoeff_sq_signVal_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S ^ 2 ≤ 1

A Fourier coefficient of a Boolean function, read as signs, has square at most one.

theorem Cslib.BitString.abs_fourierCoeff_signVal_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (S : Finset ι) : |fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S| ≤ 1

A Fourier coefficient of a Boolean function, read as signs, has absolute value at most one.

theorem Cslib.BitString.one_le_sum_abs_fourierCoeff_signVal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) : 1 ≤ ∑ S : Finset ι, |fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S|

A Boolean function, read as signs, has spectral norm ∑_S |f̂(S)| at least one.

Distance and correlation

theorem Cslib.BitString.expect_signVal_mul_signVal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f g : (ι → Bool) → Bool) : (Finset.univ.expect fun (x : ι → Bool) => signVal (f x) * signVal (g x)) = 1 - 2 * ↑(hammingDist f g) / 2 ^ Fintype.card ι

Correlation is one minus twice the distance: the correlation of two Boolean functions, read as signs, is one minus twice the fraction of the inputs on which they differ O'Donnell, Section 1.4.

theorem Cslib.BitString.fourierCoeff_signVal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (S : Finset ι) : fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S = 1 - 2 * ↑(hammingDist f (parityOn S)) / 2 ^ Fintype.card ι

The Fourier coefficient on S of a Boolean function read as signs is one minus twice the relative Hamming distance from the function to the parity on S.

Character sums for the inner product

theorem Cslib.BitString.sum_ite_dotProduct {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [Ring R] (w : ι → Bool) : (∑ y : ι → Bool, if w ⬝ᵥ y = true then -1 else 1) = if w = 0 then 2 ^ Fintype.card ι else 0

Character orthogonality for the inner product, over any ring: the signs (-1) ^ (w ⬝ᵥ y) cancel over all bit strings y unless w = 0, since flipping a bit i with w i = true negates them. Over ℝ this is sum_chi for the set of positions where w is true.