Skip to content

Fourier analysis on the Boolean cube

AbbreviationBoolean cube#✓fully proved

For \(n \in \mathbb{N}\), the Boolean cube of dimension \(n\) is the set of functions \(x : \{0, \dots, n-1\} \to \{\mathrm{true}, \mathrm{false}\}\). It represents \(\{-1, 1\}^n\), with true standing for \(1\) and false for \(-1\).

abbrev BoolCube (n : ℕ) : Type := Fin n → Bool
Used by 98
Used byAll-true function · Fourier coefficient on the Boolean cube · Empty Fourier coefficient of a constant function · A character's own Fourier coefficient · The empty Fourier coefficient is the mean · Fourier coefficients of the zero function · Boolean degree · The two-bit AND has Boolean degree two · Constant functions have Boolean degree zero · Coordinate projections have Boolean degree one · Number of points of the Boolean cube · Lagrange basis polynomial of a cube point · Fourier character on the Boolean cube · The empty Fourier character is constant one · Fourier characters square to one · Singleton Fourier characters are coordinate signs · Decoding a cube point as a subset · Decoding inverts encoding · Lagrange basis polynomials on the cube are point indicators · The multilinear extension agrees with its function on the cube · Subset characters agree with cube characters · Subset Fourier coefficients agree with cube Fourier coefficients · Fourier degree bounds are monotone · Fourier degree at most \(d\) · Fourier degree is at most Boolean degree · Fourier degree is at most the dimension · The zero function satisfies every Fourier degree bound · Multilinear extension · Multilinear extension of the AND function · Multilinear extension of a constant function · Multilinear extension of a coordinate projection · Subsets of a finite set as points of the Boolean cube · Coordinates of an encoded subset · Additivity of Fourier coefficients · Fourier coefficients of the noise operator · Flipping a coordinate negates the Fourier coefficients of the sets containing it · Fourier coefficients of a constant function · Homogeneity of Fourier coefficients · Fourier coefficients of a character · Fourier coefficients as averages · Fourier coefficients as sums over the cube · Fourier coefficients determine the function · Fourier coefficients of a difference · Uniqueness of the Fourier expansion · Influence of a coordinate · Constant functions have zero influence · Influence of a Boolean function as a flip probability · Fourier formula for influence · Influences are nonnegative · Noise operator on the Boolean cube · Semigroup property of the noise operator · The noise operator fixes constants · Characters are eigenfunctions of the noise operator · Fourier expansion of the noise operator · Positivity of the noise operator · The noise operator \(T_1\) is the identity · The noise operator \(T_0\) takes the mean · Total influence on the Boolean cube · Constant functions have zero total influence · Total influence in Fourier form · Total influence is nonnegative · Variance on the Boolean cube · Constant functions have zero variance · Variance as mean square minus squared mean · Variance in terms of Fourier coefficients · Poincaré inequality on the Boolean cube · Variance on the Boolean cube is nonnegative · Flipping a coordinate in a Fourier character · The noise operator preserves the mean · Averages are invariant under flipping a coordinate · Average over the Boolean cube as the empty Fourier coefficient · Uniform average over the Boolean cube as a sum · Plancherel's identity on the Boolean cube · Parseval's identity on the Boolean cube · Coordinate flip on the Boolean cube · A coordinate flip fixes the other coordinates · A coordinate flip negates the flipped coordinate · Flipping a coordinate twice · Flipping a coordinate is an involution · A coordinate flip moves every point · Fourier inversion on the Boolean cube · Flipping a coordinate preserves sums over the cube · Dual orthogonality of the Boolean cube characters · Sum of a Boolean cube character · Orthogonality of the Boolean cube characters · Bonami–Beckner applied to a discrete derivative · Walsh coefficient is the canonical Fourier coefficient up to sign · Event influence is four times the canonical influence · Hypercontractivity in Fourier form · Parseval's identity on the Boolean cube · Total influence as Fourier weight · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance · Linear threshold function · Majority function · Majority Is Least Stable conjecture in \(n\) variables · Noise stability · Agreement of the two noise operators on the Boolean cube

DefinitionSign of a Boolean coordinate#✓fully proved

The sign of a Boolean value \(b\) is the real number \(\sigma(b)\) given by \(\sigma(\text{true}) = 1\) and \(\sigma(\text{false}) = -1\).

def cubeVal : Bool → ℝ
  | true => 1
  | false => -1
Used by 21
Used byFourier character on the Boolean cube · Fourier characters square to one · Singleton Fourier characters are coordinate signs · Sign of false · Coordinate signs square to one · Sign of true · Subset characters agree with cube characters · Fourier degree is at most Boolean degree · Coordinate signs have absolute value one · Noise operator on the Boolean cube · Fourier expansion of the noise operator · Positivity of the noise operator · Flipping a coordinate in a Fourier character · Coordinate signs are nonzero · Sign of a negated Boolean value · Dual orthogonality of the Boolean cube characters · Orthogonality of the Boolean cube characters · Walsh character agrees with the canonical cube character up to sign · Linear threshold function · Majority function · Agreement of the two noise operators on the Boolean cube

DefinitionFourier character on the Boolean cube#✓fully proved

For a set \(S\) of coordinates among \(n\), the Fourier character \(\chi_S\) is the real-valued function on the Boolean cube in \(n\) coordinates given by \(\chi_S(x) = \prod_{i \in S} \sigma(x_i)\), where \(\sigma\) is the sign of a coordinate: \(\sigma(\text{true}) = 1\) and \(\sigma(\text{false}) = -1\).

def cubeChi (n : ℕ) (S : Finset (Fin n)) (x : BoolCube n) : ℝ :=
  ∏ i ∈ S, cubeVal (x i)
Uses 2 · Used by 39
Statement usesBoolean cube · Sign of a Boolean coordinate
Used byFourier coefficient on the Boolean cube · Empty Fourier coefficient of a constant function · A character's own Fourier coefficient · The empty Fourier coefficient is the mean · Fourier coefficients of the zero function · The empty Fourier character is constant one · Fourier characters square to one · Singleton Fourier characters are coordinate signs · Subset characters agree with cube characters · Subset Fourier coefficients agree with cube Fourier coefficients · Fourier degree is at most Boolean degree · Additivity of Fourier coefficients · Fourier coefficients of the noise operator · Flipping a coordinate negates the Fourier coefficients of the sets containing it · Fourier coefficients of a constant function · Homogeneity of Fourier coefficients · Fourier coefficients of a character · Fourier coefficients as averages · Fourier coefficients as sums over the cube · Fourier coefficients determine the function · Fourier coefficients of a difference · Uniqueness of the Fourier expansion · The noise operator fixes constants · Characters are eigenfunctions of the noise operator · Fourier expansion of the noise operator · The noise operator \(T_1\) is the identity · The noise operator \(T_0\) takes the mean · Flipping a coordinate in a Fourier character · Average over the Boolean cube as the empty Fourier coefficient · Plancherel's identity on the Boolean cube · Fourier inversion on the Boolean cube · Dual orthogonality of the Boolean cube characters · Sum of a Boolean cube character · Orthogonality of the Boolean cube characters · Bonami–Beckner applied to a discrete derivative · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier inversion on the Boolean cube · Noise operator is diagonal in the Walsh basis · Walsh character agrees with the canonical cube character up to sign

DefinitionFourier coefficient on the Boolean cube#✓fully proved

For \(n \in \mathbb{N}\), a function \(f : \{-1, 1\}^n \to \mathbb{R}\) and a set \(S \subseteq \{0, \dots, n-1\}\), the normalized Fourier coefficient of \(f\) at \(S\) is \(\hat f(S) = \frac{1}{|\{-1, 1\}^n|} \sum_{x \in \{-1, 1\}^n} f(x) \chi_S(x)\), where \(\chi_S(x) = \prod_{i \in S} x_i\). That is, \(\hat f(S)\) is the uniform expectation of \(f \chi_S\).

noncomputable def boolFourierCoeff (n : ℕ) (f : BoolCube n → ℝ)
    (S : Finset (Fin n)) : ℝ :=
  (∑ x : BoolCube n, f x * cubeChi n S x) / (Fintype.card (BoolCube n) : ℝ)
Uses 2 · Used by 44
Statement usesBoolean cube · Fourier character on the Boolean cube
Used byEmpty Fourier coefficient of a constant function · A character's own Fourier coefficient · The empty Fourier coefficient is the mean · Fourier coefficients of the zero function · Subset Fourier coefficients agree with cube Fourier coefficients · Fourier degree at most \(d\) · Fourier degree is at most Boolean degree · Fourier degree is at most the dimension · The zero function satisfies every Fourier degree bound · Additivity of Fourier coefficients · Fourier coefficients of the noise operator · Flipping a coordinate negates the Fourier coefficients of the sets containing it · Fourier coefficients of a constant function · Homogeneity of Fourier coefficients · Fourier coefficients of a character · Fourier coefficients as averages · Fourier coefficients as sums over the cube · Fourier coefficients determine the function · Fourier coefficients of a difference · Uniqueness of the Fourier expansion · Fourier formula for influence · Semigroup property of the noise operator · The noise operator fixes constants · Characters are eigenfunctions of the noise operator · Fourier expansion of the noise operator · The noise operator \(T_1\) is the identity · The noise operator \(T_0\) takes the mean · Total influence in Fourier form · Variance in terms of Fourier coefficients · Poincaré inequality on the Boolean cube · The noise operator preserves the mean · Average over the Boolean cube as the empty Fourier coefficient · Plancherel's identity on the Boolean cube · Parseval's identity on the Boolean cube · Fourier inversion on the Boolean cube · Walsh coefficient is the canonical Fourier coefficient up to sign · Fourier inversion on the Boolean cube · Influence of a coordinate as Fourier weight · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Parseval's identity on the Boolean cube · Total influence as Fourier weight · Variance as Fourier weight off the empty set · Noise stability

DefinitionFourier degree at most \(d\)#✓fully proved

A real-valued function \(f\) on the Boolean cube of dimension \(n\) has Fourier degree at most a natural number \(d\) when its Fourier coefficient \(\hat f(S)\) vanishes for every set \(S\) of coordinates with \(|S| > d\).

This is the degree of the multilinear polynomial representing the function on the cube.

def MultilinearDegreeLE (n : ℕ) (f : BoolCube n → ℝ) (d : ℕ) : Prop :=
  ∀ S : Finset (Fin n), d < S.card → boolFourierCoeff n f S = 0
Uses 2 · Used by 4
Statement usesBoolean cube · Fourier coefficient on the Boolean cube
Used byFourier degree bounds are monotone · Fourier degree is at most Boolean degree · Fourier degree is at most the dimension · The zero function satisfies every Fourier degree bound

TheoremSign of true#✓fully proved

The sign \(\sigma(\text{true})\) of the Boolean value true equals \(1\).

@[simp] theorem cubeVal_true : cubeVal true = 1
Uses 1
Statement usesSign of a Boolean coordinate

TheoremSign of false#✓fully proved

The sign \(\sigma(\text{false})\) of the Boolean value false equals \(-1\).

@[simp] theorem cubeVal_false : cubeVal false = -1
Uses 1
Statement usesSign of a Boolean coordinate

TheoremCoordinate signs square to one#✓fully proved

For every Boolean value \(b\), its sign \(\sigma(b)\) satisfies \(\sigma(b) \cdot \sigma(b) = 1\).

@[simp] theorem cubeVal_mul_self (b : Bool) : cubeVal b * cubeVal b = 1
Uses 1 · Used by 2
Statement usesSign of a Boolean coordinate
Used byFourier characters square to one · Dual orthogonality of the Boolean cube characters

TheoremThe empty Fourier character is constant one#✓fully proved

For every \(n\) and every point \(x\) of the Boolean cube in \(n\) coordinates, the Fourier character \(\chi_\emptyset\) of the empty set of coordinates satisfies \(\chi_\emptyset(x) = 1\).

@[simp] theorem cubeChi_empty (n : ℕ) (x : BoolCube n) : cubeChi n ∅ x = 1
Uses 2 · Used by 6
Statement usesBoolean cube · Fourier character on the Boolean cube
Used byEmpty Fourier coefficient of a constant function · The empty Fourier coefficient is the mean · The noise operator fixes constants · The noise operator \(T_0\) takes the mean · Average over the Boolean cube as the empty Fourier coefficient · Sum of a Boolean cube character

TheoremSingleton Fourier characters are coordinate signs#✓fully proved

For every \(n\), every coordinate \(i\) and every point \(x\) of the Boolean cube in \(n\) coordinates, the Fourier character \(\chi_{\{i\}}\) of the singleton \(\{i\}\) satisfies \(\chi_{\{i\}}(x) = \sigma(x_i)\), where \(\sigma\) is the sign of a coordinate: \(\sigma(\text{true}) = 1\) and \(\sigma(\text{false}) = -1\).

@[simp] theorem cubeChi_singleton (n : ℕ) (i : Fin n) (x : BoolCube n) :
    cubeChi n {i} x = cubeVal (x i)
Uses 3
Statement usesBoolean cube · Fourier character on the Boolean cube · Sign of a Boolean coordinate

TheoremFourier characters square to one#✓fully proved

For every \(n\), every set \(S\) of the \(n\) coordinates and every point \(x\) of the Boolean cube in \(n\) coordinates, the Fourier character \(\chi_S\) satisfies \(\chi_S(x) \cdot \chi_S(x) = 1\).

@[simp] theorem cubeChi_mul_self (n : ℕ) (S : Finset (Fin n)) (x : BoolCube n) :
    cubeChi n S x * cubeChi n S x = 1
Uses 4 · Used by 1
Statement usesBoolean cube · Fourier character on the Boolean cube
Proof usesSign of a Boolean coordinate · Coordinate signs square to one
Used byA character's own Fourier coefficient

TheoremThe empty Fourier coefficient is the mean#✓fully proved

For every \(n \in \mathbb{N}\) and every function \(f : \{-1, 1\}^n \to \mathbb{R}\), the normalized Fourier coefficient of \(f\) at the empty set is the uniform mean of \(f\): \(\hat f(\emptyset) = \frac{1}{|\{-1, 1\}^n|} \sum_{x \in \{-1, 1\}^n} f(x)\).

theorem boolFourierCoeff_empty (n : ℕ) (f : BoolCube n → ℝ) :
    boolFourierCoeff n f ∅ = (∑ x : BoolCube n, f x) / (Fintype.card (BoolCube n) : ℝ)
Uses 4
Statement usesBoolean cube · Fourier coefficient on the Boolean cube
Proof usesFourier character on the Boolean cube · The empty Fourier character is constant one

TheoremFourier coefficients of the zero function#✓fully proved

For every \(n \in \mathbb{N}\) and every \(S \subseteq \{0, \dots, n-1\}\), the normalized Fourier coefficient at \(S\) of the identically zero function on \(\{-1, 1\}^n\) is \(0\).

@[simp] theorem boolFourierCoeff_zero (n : ℕ) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun _ => 0) S = 0
Uses 3 · Used by 1
Statement usesBoolean cube · Fourier coefficient on the Boolean cube
Proof usesFourier character on the Boolean cube
Used byThe zero function satisfies every Fourier degree bound

TheoremA character's own Fourier coefficient#✓fully proved

For every \(n \in \mathbb{N}\) and every \(S \subseteq \{0, \dots, n-1\}\), the normalized Fourier coefficient at \(S\) of the character \(\chi_S(x) = \prod_{i \in S} x_i\) on \(\{-1, 1\}^n\) equals \(1\), that is, \(\widehat{\chi_S}(S) = 1\).

@[simp] theorem boolFourierCoeff_cubeChi_self (n : ℕ) (S : Finset (Fin n)) :
    boolFourierCoeff n (cubeChi n S) S = 1
Uses 4
Statement usesFourier coefficient on the Boolean cube · Fourier character on the Boolean cube
Proof usesBoolean cube · Fourier characters square to one

TheoremEmpty Fourier coefficient of a constant function#✓fully proved

For every \(n \in \mathbb{N}\) and every real \(c\), the normalized Fourier coefficient at the empty set of the constant function \(x \mapsto c\) on the Boolean cube \(\{-1, 1\}^n\) equals \(c\). This includes dimension \(n = 0\).

@[simp] theorem boolFourierCoeff_const_empty (n : ℕ) (c : ℝ) :
    boolFourierCoeff n (fun _ => c) ∅ = c
Uses 4
Statement usesBoolean cube · Fourier coefficient on the Boolean cube
Proof usesFourier character on the Boolean cube · The empty Fourier character is constant one

TheoremThe zero function satisfies every Fourier degree bound#✓fully proved

For all natural numbers \(n\) and \(d\), the zero function on the Boolean cube of dimension \(n\) has Fourier degree at most \(d\).

@[simp] theorem multilinearDegreeLE_zero (n d : ℕ) :
    MultilinearDegreeLE n (fun _ => 0) d
Uses 4
Statement usesBoolean cube · Fourier degree at most \(d\)
Proof usesFourier coefficient on the Boolean cube · Fourier coefficients of the zero function

TheoremFourier degree bounds are monotone#✓fully proved

Let \(f\) be a real-valued function on the Boolean cube of dimension \(n\), and let \(d \le e\) be natural numbers. If \(f\) has Fourier degree at most \(d\), then \(f\) has Fourier degree at most \(e\).

theorem MultilinearDegreeLE.mono {n d e : ℕ} {f : BoolCube n → ℝ}
    (h : MultilinearDegreeLE n f d) (hde : d ≤ e) : MultilinearDegreeLE n f e
Uses 2
Statement usesBoolean cube · Fourier degree at most \(d\)

TheoremFourier degree is at most the dimension#✓fully proved

Let \(f\) be a real-valued function on the Boolean cube of dimension \(n\), and let \(d \ge n\) be a natural number. Then \(f\) has Fourier degree at most \(d\).

theorem multilinearDegreeLE_of_dimension_le {n d : ℕ} (f : BoolCube n → ℝ)
    (hnd : n ≤ d) : MultilinearDegreeLE n f d
Uses 3
Statement usesBoolean cube · Fourier degree at most \(d\)
Proof usesFourier coefficient on the Boolean cube

DefinitionLagrange basis polynomial of a cube point#✓fully proved

Let \(x\) be a point of the Boolean cube in \(n\) coordinates, indexed by \(i \in \{0, \dots, n-1\}\). Its cube basis polynomial is the real polynomial \(\prod_{i=0}^{n-1} \ell_i\) in the variables \(X_0, \dots, X_{n-1}\), where \(\ell_i = X_i\) if \(x_i\) is true and \(\ell_i = 1 - X_i\) if \(x_i\) is false. Reading true as \(1\) and false as \(0\), it is the Lagrange basis polynomial of \(x\) on the grid \(\{0,1\}^n\).

noncomputable def cubeBasis {n : ℕ}
    (x : BoolCube n) : MvPolynomial (Fin n) ℝ :=
  ∏ i : Fin n,
    if x i then MvPolynomial.X i else 1 - MvPolynomial.X i
Uses 1 · Used by 6
Statement usesBoolean cube
Used byLagrange basis polynomials on the cube are point indicators · The multilinear extension agrees with its function on the cube · Multilinear extension · Multilinear extension of the AND function · Multilinear extension of a constant function · Multilinear extension of a coordinate projection

DefinitionMultilinear extension#✓fully proved

Let \(f\) be a Boolean-valued function on the Boolean cube of dimension \(n\), and read each coordinate and each value as \(1\) for true and \(0\) for false. The real multilinear extension of \(f\) is the polynomial in \(\mathbb{R}[X_0, \dots, X_{n-1}]\)

\[\sum_{x \in \{0,1\}^n} f(x) \prod_{i < n} \bigl(x_i X_i + (1 - x_i)(1 - X_i)\bigr).\]

For each cube point \(x\) the product is its Lagrange basis polynomial: it evaluates to \(1\) at \(x\) and to \(0\) at every other point of \(\{0,1\}^n\). Hence the extension agrees with \(f\) on \(\{0,1\}^n\), and it is the unique polynomial of degree at most one in each variable that does.

noncomputable def multilinearExtension {n : ℕ}
    (f : BoolCube n → Bool) : MvPolynomial (Fin n) ℝ := by
  classical
  exact
  ∑ x : BoolCube n,
    MvPolynomial.C (if f x then (1 : ℝ) else 0) *
      cubeBasis x
Uses 2 · Used by 9
Statement usesBoolean cube · Lagrange basis polynomial of a cube point
Used byBoolean degree · The two-bit AND has Boolean degree two · Constant functions have Boolean degree zero · Coordinate projections have Boolean degree one · The multilinear extension agrees with its function on the cube · Fourier degree is at most Boolean degree · Multilinear extension of the AND function · Multilinear extension of a constant function · Multilinear extension of a coordinate projection

TheoremLagrange basis polynomials on the cube are point indicators#✓fully proved

Let \(x\) and \(y\) be points of the Boolean cube of dimension \(n\), and identify \(y\) with the point of \(\{0,1\}^n \subseteq \mathbb{R}^n\) whose \(i\)-th coordinate is \(1\) when \(y_i\) is true and \(0\) when it is false. Then the cube basis polynomial of \(x\) evaluated at \(y\) equals \(1\) if \(x = y\) and \(0\) otherwise.

theorem eval_cubeBasis {n : ℕ} (x y : BoolCube n) :
    MvPolynomial.eval (fun i => if y i then (1 : ℝ) else 0) (cubeBasis x) =
      if x = y then 1 else 0
Uses 2 · Used by 1
Statement usesBoolean cube · Lagrange basis polynomial of a cube point
Used byThe multilinear extension agrees with its function on the cube

TheoremThe multilinear extension agrees with its function on the cube#✓fully proved

Let \(f\) be a Boolean function on the Boolean cube of dimension \(n\), and let \(y\) be a point of the cube, identified with the point of \(\{0,1\}^n \subseteq \mathbb{R}^n\) whose \(i\)-th coordinate is \(1\) when \(y_i\) is true and \(0\) when it is false. Then the real multilinear extension of \(f\) evaluated at \(y\) equals \(1\) if \(f(y)\) is true and \(0\) if \(f(y)\) is false.

theorem eval_multilinearExtension {n : ℕ}
    (f : BoolCube n → Bool) (y : BoolCube n) :
    MvPolynomial.eval (fun i => if y i then (1 : ℝ) else 0)
      (multilinearExtension f) = if f y then 1 else 0
Uses 4 · Used by 1
Statement usesBoolean cube · Multilinear extension
Proof usesLagrange basis polynomial of a cube point · Lagrange basis polynomials on the cube are point indicators
Used byFourier degree is at most Boolean degree

TheoremMultilinear extension of a constant function#✓fully proved

For every natural number \(n\) and every Boolean value \(b\), the real multilinear extension of the constant function \(b\) on the Boolean cube of dimension \(n\) is the constant polynomial \(1\) if \(b\) is true and the constant polynomial \(0\) if \(b\) is false.

theorem multilinearExtension_const {n : ℕ} (b : Bool) :
    multilinearExtension (n := n) (fun _ => b) =
      MvPolynomial.C (if b then (1 : ℝ) else 0)
Uses 3 · Used by 1
Statement usesBoolean cube · Multilinear extension
Proof usesLagrange basis polynomial of a cube point
Used byConstant functions have Boolean degree zero

TheoremMultilinear extension of a coordinate projection#✓fully proved

For every coordinate \(i\) of the Boolean cube of dimension \(n\), the real multilinear extension of the projection \(x \mapsto x_i\) is the variable \(X_i\).

theorem multilinearExtension_projection {n : ℕ} (i : Fin n) :
    multilinearExtension (fun x => x i) = MvPolynomial.X i
Uses 3 · Used by 1
Statement usesBoolean cube · Multilinear extension
Proof usesLagrange basis polynomial of a cube point
Used byCoordinate projections have Boolean degree one

DefinitionBoolean degree#✓fully proved

Let \(f\) be a Boolean-valued function on the Boolean cube in \(n\) coordinates, and read true as \(1\) and false as \(0\). The Boolean degree of \(f\) is the total degree of the multilinear extension of \(f\): the real multilinear polynomial in \(n\) variables that takes the value \(f(x)\) at every point \(x \in \{0,1\}^n\).

noncomputable def booleanDegree {n : ℕ}
    (f : BoolCube n → Bool) : ℕ :=
  (multilinearExtension f).totalDegree
Uses 2 · Used by 5
Statement usesBoolean cube · Multilinear extension
Used byThe two-bit AND has Boolean degree two · Constant functions have Boolean degree zero · Coordinate projections have Boolean degree one · Fourier degree is at most Boolean degree · The Servedio–Tan–Verbin conjecture

TheoremConstant functions have Boolean degree zero#✓fully proved

For every \(n \in \mathbb{N}\) and every Boolean value \(b\), the constant function \(x \mapsto b\) on the Boolean cube of dimension \(n\) has Boolean degree \(0\).

theorem booleanDegree_const {n : ℕ} (b : Bool) :
    booleanDegree (n := n) (fun _ => b) = 0
Uses 4
Statement usesBoolean cube · Boolean degree
Proof usesMultilinear extension · Multilinear extension of a constant function

TheoremCoordinate projections have Boolean degree one#✓fully proved

For every \(n \in \mathbb{N}\) and every \(i < n\), the coordinate projection \(x \mapsto x_i\) on the Boolean cube of dimension \(n\) has Boolean degree \(1\).

theorem booleanDegree_projection {n : ℕ} (i : Fin n) :
    booleanDegree (fun x => x i) = 1
Uses 4
Statement usesBoolean cube · Boolean degree
Proof usesMultilinear extension · Multilinear extension of a coordinate projection

DefinitionAll-true function#✓fully proved

For \(n \in \mathbb{N}\), the all-true function on the Boolean cube of dimension \(n\) is the Boolean AND of all coordinates: it sends \(x = (x_0, \dots, x_{n-1})\) to true exactly when \(x_i\) is true for every \(i < n\). In dimension \(0\) it is constantly true.

def allTrueFunction {n : ℕ} (x : BoolCube n) : Bool :=
  decide (∀ i, x i = true)
Uses 1 · Used by 2
Statement usesBoolean cube
Used byThe two-bit AND has Boolean degree two · Multilinear extension of the AND function

TheoremMultilinear extension of the AND function#✓fully proved

For every natural number \(n\), the real multilinear extension of the AND function on the Boolean cube of dimension \(n\) (true exactly when every coordinate is true) is the monomial \(\prod_{i=0}^{n-1} X_i\).

theorem multilinearExtension_allTrue (n : ℕ) :
    multilinearExtension (n := n) allTrueFunction =
      ∏ i : Fin n, MvPolynomial.X i
Uses 4 · Used by 1
Statement usesAll-true function · Multilinear extension
Proof usesBoolean cube · Lagrange basis polynomial of a cube point
Used byThe two-bit AND has Boolean degree two

TheoremThe two-bit AND has Boolean degree two#✓fully proved

The all-true function on the Boolean cube of dimension \(2\), \((x_0, x_1) \mapsto x_0 \wedge x_1\), has Boolean degree \(2\); that is, its real multilinear extension has total degree \(2\).

theorem booleanDegree_allTrue_two :
    booleanDegree (allTrueFunction (n := 2)) = 2
Uses 5
Statement usesAll-true function · Boolean degree
Proof usesBoolean cube · Multilinear extension · Multilinear extension of the AND function

TheoremFourier degree is at most Boolean degree#✓fully proved

Let \(f\) be a Boolean function on the Boolean cube of dimension \(n\), and let \(g\) be the real function with \(g(x) = 1\) if \(f(x)\) is true and \(g(x) = 0\) otherwise. Then \(g\) has Fourier degree at most the Boolean degree of \(f\): every Fourier coefficient \(\hat g(S)\) with \(|S|\) greater than the total degree of the multilinear extension of \(f\) vanishes.

theorem multilinearDegreeLE_indicator {n : ℕ} (f : BoolCube n → Bool) :
    MultilinearDegreeLE n (fun x => if f x then (1 : ℝ) else 0)
      (booleanDegree f)
Uses 8
Statement usesBoolean cube · Fourier degree at most \(d\) · Boolean degree
Proof usesFourier coefficient on the Boolean cube · Fourier character on the Boolean cube · Sign of a Boolean coordinate · The multilinear extension agrees with its function on the cube · Multilinear extension
44 fully proved

Finset Fourier

DefinitionFourier character on finite sets#✓fully proved

For finite sets \(S\) and \(T\), the Fourier character of \(S\) at \(T\) is the real number \(\chi_S(T) = (-1)^{|S \cap T|}\).

This is the subset-indexed form of the Fourier character on the Boolean cube; after reindexing the coordinates, the two agree.

noncomputable def fourierChar (S T : Finset ι) : ℝ :=
  (-1 : ℝ) ^ (S ∩ T).card
Used by 5
Used bySubset characters agree with cube characters · Fourier coefficient on the subsets of a finite set · Subset Fourier coefficients agree with cube Fourier coefficients · Fourier inversion on the subsets of a finite set · Plancherel identity on the subsets of a finite set

DefinitionFourier coefficient on the subsets of a finite set#✓fully proved

Let \(E\) be a finite subset of a type \(\iota\) and let \(f\) be a function from finite subsets of \(\iota\) to \(\mathbb{R}\). For a finite subset \(S\) of \(\iota\), the Fourier coefficient of \(f\) at \(S\) over \(E\) is

\[\hat f(S) = \frac{1}{2^{|E|}} \sum_{U \subseteq E} f(U) \, (-1)^{|S \cap U|},\]

the uniform average over the subsets \(U\) of \(E\) of \(f(U)\) times the Fourier character \(\chi_S(U) = (-1)^{|S \cap U|}\).

After reindexing, it agrees with the Fourier coefficient on the Boolean cube.

noncomputable def fourierCoeff (E : Finset ι) (f : Finset ι → ℝ)
    (S : Finset ι) : ℝ :=
  (∑ U ∈ E.powerset, f U * fourierChar S U) / 2 ^ E.card
Uses 1 · Used by 3
Statement usesFourier character on finite sets
Used bySubset Fourier coefficients agree with cube Fourier coefficients · Fourier inversion on the subsets of a finite set · Plancherel identity on the subsets of a finite set

TheoremNumber of points of the Boolean cube#✓fully proved

For every \(n \in \mathbb{N}\), the Boolean cube of dimension \(n\) has exactly \(2^n\) points.

theorem card_boolCube (n : ℕ) : Fintype.card (BoolCube n) = 2 ^ n
Uses 1 · Used by 3
Statement usesBoolean cube
Used bySubset Fourier coefficients agree with cube Fourier coefficients · Uniform average over the Boolean cube as a sum · Walsh coefficient is the canonical Fourier coefficient up to sign

DefinitionSubsets of a finite set as indicator functions#✓fully proved

For a finite set \(E\), this is the bijection from the subsets \(T \subseteq E\) to the functions \(b\) from \(E\) to \(\{\mathrm{true}, \mathrm{false}\}\) given by \(b(a) = \mathrm{false}\) if \(a \in T\) and \(b(a) = \mathrm{true}\) if \(a \notin T\). Its inverse sends \(b\) to the set \(\{a \in E : b(a) = \mathrm{false}\}\).

Members of \(T\) read false, matching the convention that identifies false with the sign \(-1\) and true with the sign \(+1\).

BooleanCube.powersetEquivIndicator · 48 lines 
noncomputable def powersetEquivIndicator (E : Finset ι) :
    ↥E.powerset ≃ (↥E → Bool) where
  toFun S i := decide (i.val ∉ S.val)
  invFun b :=
    ⟨E.filter (fun a => if h : a ∈ E then b ⟨a, h⟩ = false else False),
      Finset.mem_powerset.mpr (Finset.filter_subset _ _)⟩
  left_inv S := by
    obtain ⟨T, hT⟩ := S
    have hsub : T ⊆ E := Finset.mem_powerset.mp hT
    refine Subtype.ext ?_
    change E.filter (fun a =>
      if _h : a ∈ E then decide (a ∉ T) = false else False) = T
    ext a
    simp only [Finset.mem_filter]
    constructor
    · rintro ⟨haE, hdec⟩
      rw [dite_eq_left haE] at hdec
      revert hdec
      by_cases haT : a ∈ T
      · intro _; exact haT
      · intro hdec; simp [haT] at hdec
    · intro haT
      refine ⟨hsub haT, ?_⟩
      rw [dite_eq_left (hsub haT)]
      show decide (a ∉ T) = false
      simp [haT]
  right_inv b := by
    funext i
    change decide (i.val ∉ E.filter
      (fun a => if h : a ∈ E then b ⟨a, h⟩ = false else False)) = b i
    have h2 : (i.val ∈ E ∧
          (if h : i.val ∈ E then b ⟨i.val, h⟩ = false else False))
        ↔ b i = false := by
      constructor
      · rintro ⟨-, hite⟩
        rw [dite_eq_left i.property] at hite
        exact hite
      · intro hbi
        refine ⟨i.property, ?_⟩
        rw [dite_eq_left i.property]
        exact hbi
    have hmem : (i.val ∉ E.filter
          (fun a => if h : a ∈ E then b ⟨a, h⟩ = false else False))
        ↔ b i = true := by
      simp only [Finset.mem_filter, h2]
      cases b i <;> simp
    simp only [hmem]
    cases b i <;> simp
Used by 1
Used bySubsets of a finite set as points of the Boolean cube

DefinitionSubsets of a finite set as points of the Boolean cube#✓fully proved

For a finite set \(E\) with \(n = |E|\) elements, fix a bijection \(e\) from \(E\) to \(\{0, \dots, n-1\}\) (an enumeration of \(E\), chosen noncanonically). This is the bijection from the subsets \(T \subseteq E\) to the Boolean cube of dimension \(n\) that sends \(T\) to the point \(x\) with \(x_{e(a)} = \mathrm{false}\) if \(a \in T\) and \(x_{e(a)} = \mathrm{true}\) if \(a \notin T\), for every \(a \in E\).

noncomputable def powersetEquivBoolCube (E : Finset ι) :
    ↥E.powerset ≃ BoolCube E.card :=
  (powersetEquivIndicator E).trans
    ((Finset.equivFin E).arrowCongr (Equiv.refl Bool))
Uses 2 · Used by 5
Statement usesBoolean cube · Subsets of a finite set as indicator functions
Used byDecoding a cube point as a subset · Decoding inverts encoding · Subset characters agree with cube characters · Subset Fourier coefficients agree with cube Fourier coefficients · Coordinates of an encoded subset

TheoremCoordinates of an encoded subset#✓fully proved

Let \(E\) be a finite set with \(m\) elements, listed in the fixed order \(e_0, \dots, e_{m-1}\) used to encode subsets of \(E\) as points of the Boolean cube of dimension \(m\). For every subset \(T \subseteq E\) and every coordinate \(j < m\), the \(j\)-th coordinate of the point encoding \(T\) is true if \(e_j \notin T\) and false if \(e_j \in T\).

theorem powersetEquivBoolCube_apply (E : Finset ι) (T : Finset ι)
    (hT : T ∈ E.powerset) (j : Fin E.card) :
    powersetEquivBoolCube E ⟨T, hT⟩ j
      = decide (((Finset.equivFin E).symm j).val ∉ T)
Uses 2 · Used by 1
Statement usesBoolean cube · Subsets of a finite set as points of the Boolean cube
Used bySubset characters agree with cube characters

DefinitionReindexing a subset as a set of coordinates#✓fully proved

For finite sets \(S \subseteq E\) with \(n = |E|\), let \(e\) be the fixed bijection from \(E\) to \(\{0, \dots, n-1\}\) (the enumeration of \(E\) used to identify subsets of \(E\) with points of the Boolean cube of dimension \(n\)). The reindexed set is the image \(e(S) = \{e(a) : a \in S\}\), a subset of \(\{0, \dots, n-1\}\).

noncomputable def reindexFinset (E S : Finset ι) (hS : S ⊆ E) :
    Finset (Fin E.card) :=
  S.attach.map
    ⟨fun a => Finset.equivFin E ⟨a.val, hS a.property⟩,
      fun a b h => by
        have h' := (Finset.equivFin E).injective h
        simp only [Subtype.mk.injEq] at h'
        exact Subtype.ext h'⟩
Used by 2
Used bySubset characters agree with cube characters · Subset Fourier coefficients agree with cube Fourier coefficients

DefinitionDecoding a cube point as a subset#✓fully proved

Let \(E\) be a finite set with \(m\) elements, listed in a fixed order as \(e_0, \dots, e_{m-1}\); this order identifies subsets of \(E\) with points of the Boolean cube of dimension \(m\). A point \(x\) of that cube decodes to the subset \(\{e_j : x_j = \mathrm{false}\}\) of \(E\); this inverts the encoding of subsets of \(E\) as cube points.

noncomputable def decodeBoolCube (E : Finset ι) (x : BoolCube E.card) :
    Finset ι :=
  ((powersetEquivBoolCube E).symm x).val
Uses 2 · Used by 2
Statement usesBoolean cube · Subsets of a finite set as points of the Boolean cube
Used byDecoding inverts encoding · Subset Fourier coefficients agree with cube Fourier coefficients

TheoremDecoding inverts encoding#✓fully proved

Let \(E\) be a finite set with \(m\) elements, listed in a fixed order as \(e_0, \dots, e_{m-1}\). Encode a subset \(T \subseteq E\) as the point \(x_T\) of the Boolean cube of dimension \(m\) whose \(j\)-th coordinate is false exactly when \(e_j \in T\), and decode a point \(x\) as the subset \(\{e_j : x_j = \mathrm{false}\}\). Then for every subset \(T \subseteq E\), decoding \(x_T\) gives back \(T\).

@[simp] theorem decode_encode (E : Finset ι) (T : Finset ι)
    (hT : T ∈ E.powerset) :
    decodeBoolCube E (powersetEquivBoolCube E ⟨T, hT⟩) = T
Uses 3 · Used by 1
Statement usesBoolean cube · Decoding a cube point as a subset · Subsets of a finite set as points of the Boolean cube
Used bySubset Fourier coefficients agree with cube Fourier coefficients

TheoremSubset characters agree with cube characters#✓fully proved

Let \(E\) be a finite set with \(m\) elements, listed in a fixed order as \(e_0, \dots, e_{m-1}\), and encode a subset \(T \subseteq E\) as the point \(x_T\) of the Boolean cube of dimension \(m\) whose \(j\)-th coordinate is false exactly when \(e_j \in T\). For all subsets \(S, T \subseteq E\),

\[(-1)^{|S \cap T|} = \chi_{S'}(x_T),\]

where the left side is the Fourier character of \(S\) at \(T\), \(S' = \{j : e_j \in S\}\) is \(S\) reindexed as a set of coordinates, and \(\chi_{S'}\) is the Fourier character on the cube.

theorem fourierChar_eq_cubeChi (E : Finset ι) (S T : Finset ι)
    (hS : S ⊆ E) (hT : T ∈ E.powerset) :
    fourierChar S T
      = cubeChi E.card (reindexFinset E S hS)
        (powersetEquivBoolCube E ⟨T, hT⟩)
Uses 7 · Used by 1
Statement usesBoolean cube · Fourier character on the Boolean cube · Fourier character on finite sets · Subsets of a finite set as points of the Boolean cube · Reindexing a subset as a set of coordinates
Proof usesSign of a Boolean coordinate · Coordinates of an encoded subset
Used bySubset Fourier coefficients agree with cube Fourier coefficients

TheoremSubset Fourier coefficients agree with cube Fourier coefficients#✓fully proved

Let \(E\) be a finite subset of a type \(\iota\) with \(m\) elements, listed in a fixed order as \(e_0, \dots, e_{m-1}\), and decode a point \(x\) of the Boolean cube of dimension \(m\) as the subset \(D(x) = \{e_j : x_j = \mathrm{false}\}\) of \(E\). Let \(f\) be a function from finite subsets of \(\iota\) to \(\mathbb{R}\) and let \(S \subseteq E\). Then the Fourier coefficient \(\hat f(S) = 2^{-m} \sum_{U \subseteq E} f(U) (-1)^{|S \cap U|}\) of \(f\) at \(S\) over \(E\) equals the Fourier coefficient on the cube of the function \(x \mapsto f(D(x))\) at the set of coordinates \(S' = \{j : e_j \in S\}\).

theorem fourierCoeff_eq_boolFourierCoeff (E : Finset ι)
    (f : Finset ι → ℝ) (S : Finset ι) (hS : S ⊆ E) :
    fourierCoeff E f S
      = boolFourierCoeff E.card (fun x => f (decodeBoolCube E x))
        (reindexFinset E S hS)
Uses 11
Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Decoding a cube point as a subset · Fourier coefficient on the subsets of a finite set · Reindexing a subset as a set of coordinates
Proof usesNumber of points of the Boolean cube · Fourier character on the Boolean cube · Decoding inverts encoding · Fourier character on finite sets · Subset characters agree with cube characters · Subsets of a finite set as points of the Boolean cube

Fourier Laws

TheoremFourier inversion on the subsets of a finite set#✓fully proved

Let \(E\) be a finite subset of a type \(\iota\) and let \(f\) be a function from finite subsets of \(\iota\) to \(\mathbb{R}\). For every subset \(T \subseteq E\),

\[f(T) = \sum_{S \subseteq E} \hat f(S) \, (-1)^{|S \cap T|},\]

where \(\hat f(S) = 2^{-|E|} \sum_{U \subseteq E} f(U) (-1)^{|S \cap U|}\) is the Fourier coefficient of \(f\) at \(S\) over \(E\) and \((-1)^{|S \cap T|}\) is the Fourier character of \(S\) at \(T\).

public theorem fourier_inversion (E : Finset ι) (f : Finset ι → ℝ)
    (T : Finset ι) (hT : T ∈ E.powerset) :
    f T = ∑ S ∈ E.powerset, fourierCoeff E f S * fourierChar S T
Uses 2 · Used by 1
Statement usesFourier character on finite sets · Fourier coefficient on the subsets of a finite set
Used byPlancherel identity on the subsets of a finite set

TheoremPlancherel identity on the subsets of a finite set#✓fully proved

Let \(E\) be a finite subset of a type \(\iota\) and let \(f\) be a function from finite subsets of \(\iota\) to \(\mathbb{R}\). Then

\[\frac{1}{2^{|E|}} \sum_{T \subseteq E} f(T)^2 = \sum_{S \subseteq E} \hat f(S)^2,\]

where \(\hat f(S) = 2^{-|E|} \sum_{U \subseteq E} f(U) (-1)^{|S \cap U|}\) is the Fourier coefficient of \(f\) at \(S\) over \(E\): the mean square of \(f\) over the subsets of \(E\) equals the sum of the squared Fourier coefficients.

public theorem fourier_plancherel (E : Finset ι) (f : Finset ι → ℝ) :
    (∑ T ∈ E.powerset, f T ^ 2) / 2 ^ E.card
      = ∑ S ∈ E.powerset, fourierCoeff E f S ^ 2
Uses 3
Statement usesFourier coefficient on the subsets of a finite set
Proof usesFourier character on finite sets · Fourier inversion on the subsets of a finite set

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.