Analysis of Boolean Functions in Lean

1.2. The “Fourier expansion”: functions as multilinear polynomials🔗

Lemma1.2.1
uses 0used by 1✓L∃∀N
Tagssection-1-2support

Section 1.2. For a,x\in\{-1,1\}^n, define \mathbf 1_{\{a\}}(x)=\prod_{i=1}^n\frac{1+a_i x_i}{2}. This polynomial equals 1 when x=a and 0 otherwise. Consequently, every f:\{-1,1\}^n\to\mathbb R satisfies f(x)=\sum_{a\in\{-1,1\}^n}f(a)\mathbf 1_{\{a\}}(x).

Lean code for Lemma1.2.1●3 declarations
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.indicatorPolynomial {n : ℕ} (a x : FABL.SignCube n) : ℝ
    def FABL.indicatorPolynomial {n : ℕ}
  (a x : FABL.SignCube n) : ℝ
    The indicator polynomial `𝟙_{a}(x) = ∏ᵢ (1 + aᵢxᵢ)/2` from Section 1.2.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.indicatorPolynomial_eq_ite {n : ℕ} (a x : FABL.SignCube n) :
  FABL.indicatorPolynomial a x = if x = a then 1 else 0
    theorem FABL.indicatorPolynomial_eq_ite {n : ℕ}
  (a x : FABL.SignCube n) :
  FABL.indicatorPolynomial a x =
    if x = a then 1 else 0
    The indicator polynomial is one exactly at its indexed point.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.sum_indicatorPolynomial {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) : f x = ∑ a, f a * FABL.indicatorPolynomial a x
    theorem FABL.sum_indicatorPolynomial {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  f x =
    ∑ a,
      f a * FABL.indicatorPolynomial a x
    The interpolation formula used for existence in O'Donnell, Theorem 1.1.
Definition1.2.2
uses 0
Used by 3
Reverse dependency previews
Preview
Lemma 1.3.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-2support

Section 1.2. For S\subseteq[n] and x\in\{-1,1\}^n, write x^S=\chi_S(x)=\prod_{i\in S}x_i, \qquad x^\varnothing=1. A squarefree coefficient family a(S) determines the multilinear polynomial x\mapsto\sum_{S\subseteq[n]}a(S)x^S; for a function f, the corresponding coefficient is denoted \widehat f(S).

Lean code for Definition1.2.2●3 definitions
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.monomial {n : ℕ} (S : Finset (Fin n)) (x : FABL.SignCube n) : ℝ
    def FABL.monomial {n : ℕ} (S : Finset (Fin n))
  (x : FABL.SignCube n) : ℝ
    The monomial `xˢ = ∏ i ∈ S, xᵢ` on the sign cube.
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.multilinearPolynomial {n : ℕ} (a : Finset (Fin n) → ℝ)
  (x : FABL.SignCube n) : ℝ
    def FABL.multilinearPolynomial {n : ℕ}
  (a : Finset (Fin n) → ℝ)
  (x : FABL.SignCube n) : ℝ
    The multilinear polynomial with coefficient function `a`, evaluated at `x`.
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.fourierCoeff {n : ℕ} (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) : ℝ
    def FABL.fourierCoeff {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) : ℝ
    The uniform coefficient `f̂(S)` of a real-valued function on the sign cube.
Theorem1.2.3
uses 1
Used by 14
Reverse dependency previews
Preview
Definition 1.2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-2fidelity-exact-up-to-squarefree-coefficient-representation

Theorem 1.1. Every function f : \{-1,1\}^n \to \mathbb R can be uniquely expressed as a multilinear polynomial f(x) = \sum_{S \subseteq [n]} \widehat f(S)x^S, \qquad x^S = \prod_{i \in S}x_i, with x^\varnothing = 1. This expression is the Fourier expansion of f, the real number \widehat f(S) is the Fourier coefficient of f on S, and the collection of coefficients is the Fourier spectrum of f.

Lean code for Theorem1.2.3●2 theorems
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.fourier_expansion_unique {n : ℕ} (f : FABL.SignCube n → ℝ) :
  (∀ (x : FABL.SignCube n),
      f x = FABL.multilinearPolynomial (FABL.fourierCoeff f) x) ∧
    ∀ (a : Finset (Fin n) → ℝ),
      (∀ (x : FABL.SignCube n), f x = FABL.multilinearPolynomial a x) →
        a = FABL.fourierCoeff f
    theorem FABL.fourier_expansion_unique {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  (∀ (x : FABL.SignCube n),
      f x =
        FABL.multilinearPolynomial
          (FABL.fourierCoeff f) x) ∧
    ∀ (a : Finset (Fin n) → ℝ),
      (∀ (x : FABL.SignCube n),
          f x =
            FABL.multilinearPolynomial a
              x) →
        a = FABL.fourierCoeff f
    O'Donnell, Theorem 1.1: every real-valued function on `{-1,1}ⁿ` has a unique multilinear
expansion.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.fourier_expansion {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  f x = ∑ S, FABL.fourierCoeff f S * FABL.monomial S x
    theorem FABL.fourier_expansion {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  f x =
    ∑ S,
      FABL.fourierCoeff f S *
        FABL.monomial S x
    The expansion identity from O'Donnell, Theorem 1.1.
Definition1.2.4
uses 1
Used by 5
Reverse dependency previews
Preview
Lemma 1.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-2supportfidelity-exact-with-explicit-zero-function-convention

Exercise 1.10: real degree. If f:\{-1,1\}^n\to\mathbb R is not identically zero, its real degree is the degree of its multilinear Fourier expansion: \deg(f)=\max\{|S|:S\subseteq[n],\ \widehat f(S)\ne0\}. Equivalently, \deg(f)\le k if and only if \widehat f(S)=0 whenever |S|>k. FABL extends this definition to the zero function by the explicit convention \deg(0)=0.

Lean code for Definition1.2.4●5 declarations
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.fourierSupport {n : ℕ} (f : FABL.SignCube n → ℝ) :
  Finset (Finset (Fin n))
    def FABL.fourierSupport {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  Finset (Finset (Fin n))
    Exercise 1.10: the finite support of the multilinear Fourier expansion.
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.fourierDegree {n : ℕ} (f : FABL.SignCube n → ℝ) : ℕ
    def FABL.fourierDegree {n : ℕ}
  (f : FABL.SignCube n → ℝ) : ℕ
    Exercise 1.10: the real degree is the largest cardinality in the Fourier support.

The zero function has degree zero; this extends the book's definition, which is stated only for
functions that are not identically zero.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.mem_fourierSupport {n : ℕ} (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  S ∈ FABL.fourierSupport f ↔ FABL.fourierCoeff f S ≠ 0
    theorem FABL.mem_fourierSupport {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  S ∈ FABL.fourierSupport f ↔
    FABL.fourierCoeff f S ≠ 0
    Membership in the Fourier support is nonvanishing of the corresponding coefficient.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.fourierDegree_le_iff {n : ℕ} (f : FABL.SignCube n → ℝ) (k : ℕ) :
  FABL.fourierDegree f ≤ k ↔
    ∀ (S : Finset (Fin n)), k < S.card → FABL.fourierCoeff f S = 0
    theorem FABL.fourierDegree_le_iff {n : ℕ}
  (f : FABL.SignCube n → ℝ) (k : ℕ) :
  FABL.fourierDegree f ≤ k ↔
    ∀ (S : Finset (Fin n)),
      k < S.card →
        FABL.fourierCoeff f S = 0
    A function has Fourier degree at most `k` exactly when every coefficient above `k`
vanishes.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.fourierDegree_le_dimension {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.fourierDegree f ≤ n
    theorem FABL.fourierDegree_le_dimension {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.fourierDegree f ≤ n
    Every function on the `n`-dimensional sign cube has Fourier degree at most `n`.
Lemma1.2.5
Statement uses 2
Statement dependency previews
Preview
Theorem 1.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Definition 3.2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-2supportfidelity-generalized-degree-at-most

Exercise 1.11(b). Suppose f:\{-1,1\}^n\to\{-1,1\} has \deg(f)=k\ge1. Then the Fourier spectrum of f is 2^{1-k}-granular: for every S\subseteq[n] there is an integer z_S such that \widehat f(S)=z_S\,2^{1-k}.

The Lean declaration proves the stronger monotone form: it is enough to assume \deg(f)\le k with k\ge1.

Lean code for Lemma1.2.5●2 declarations
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.IsFourierGranular {n : ℕ} (f : FABL.SignCube n → ℝ) (ε : ℝ) : Prop
    def FABL.IsFourierGranular {n : ℕ}
  (f : FABL.SignCube n → ℝ) (ε : ℝ) : Prop
    Exercise 1.11(b): a Fourier transform is `ε`-granular when every coefficient is an integer
multiple of `ε`.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.isFourierGranular_signValue_of_fourierDegree_le {n : ℕ}
  (f : FABL.SignCube n → FABL.Sign) {k : ℕ} (hk : 1 ≤ k)
  (hdegree : (FABL.fourierDegree fun x => FABL.signValue (f x)) ≤ k) :
  FABL.IsFourierGranular (fun x => FABL.signValue (f x)) (2 * 2⁻¹ ^ k)
    theorem FABL.isFourierGranular_signValue_of_fourierDegree_le
  {n : ℕ}
  (f : FABL.SignCube n → FABL.Sign)
  {k : ℕ} (hk : 1 ≤ k)
  (hdegree :
    (FABL.fourierDegree fun x =>
        FABL.signValue (f x)) ≤
      k) :
  FABL.IsFourierGranular
    (fun x => FABL.signValue (f x))
    (2 * 2⁻¹ ^ k)
    O'Donnell, Exercise 1.11(b): if a sign-valued function has Fourier degree at most
`k ≥ 1`, every Fourier coefficient of its real encoding is an integer multiple of
`2^(1-k) = 2 * (2⁻¹)^k`.

This is stated directly for `SignCube n → Sign` to preserve the Chapter 1 import order;
`BooleanFunction.toReal` is definitionally the real encoding used here.
Definition1.2.6
uses 0
Used by 5
Reverse dependency previews
Preview
Lemma 1.2.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-2fidelity-exact

Definition 1.2. Let \chi : \mathbb F_2 \to \mathbb R be given by \chi(0)=+1 and \chi(1)=-1. For S \subseteq [n], define \chi_S : \mathbb F_2^n \to \mathbb R by \chi_S(x) = \prod_{i \in S}\chi(x_i) = (-1)^{\sum_{i \in S}x_i}. This satisfies \chi_S(x+y)=\chi_S(x)\chi_S(y) for all x,y \in \mathbb F_2^n.

Lean code for Definition1.2.6●4 declarations
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.binarySign : AddChar FABL.𝔽₂ ℝ
    def FABL.binarySign : AddChar FABL.𝔽₂ ℝ
    The basic encoding `χ(0)=1`, `χ(1)=-1`.
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.coordinateSum {n : ℕ} (S : Finset (Fin n)) :
  FABL.F₂Cube n →+ FABL.𝔽₂
    def FABL.coordinateSum {n : ℕ}
  (S : Finset (Fin n)) :
  FABL.F₂Cube n →+ FABL.𝔽₂
    The `𝔽₂`-linear sum of the coordinates indexed by `S`.
  • defdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    def FABL.χ {n : ℕ} (S : Finset (Fin n)) : AddChar (FABL.F₂Cube n) ℝ
    def FABL.χ {n : ℕ} (S : Finset (Fin n)) :
  AddChar (FABL.F₂Cube n) ℝ
    O'Donnell, Definition 1.2: the parity character `χₛ : 𝔽₂ⁿ → ℝ`.
  • theoremdefined in FABL/Chapter01/FunctionsAsMultilinearPolynomials.lean
    complete
    theorem FABL.χ_add {n : ℕ} (S : Finset (Fin n)) (x y : FABL.F₂Cube n) :
  (FABL.χ S) (x + y) = (FABL.χ S) x * (FABL.χ S) y
    theorem FABL.χ_add {n : ℕ} (S : Finset (Fin n))
  (x y : FABL.F₂Cube n) :
  (FABL.χ S) (x + y) =
    (FABL.χ S) x * (FABL.χ S) y
    O'Donnell, equation (1.5): parity characters turn addition into multiplication.
Lemma1.2.7
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-1-2support

Additive-cube bridge for Definition 1.2 and Theorem 1.1. Every function f:\mathbb F_2^n\to\mathbb R has the subset-indexed Fourier expansion f(x)=\sum_{S\subseteq[n]}\widehat f(S)\chi_S(x), where \widehat f(S)=\mathbb E_{x\sim\mathbb F_2^n}[f(x)\chi_S(x)].

Lean code for Lemma1.2.7●2 declarations
  • defdefined in FABL/Chapter01/ProbabilityDensitiesAndConvolution.lean
    complete
    def FABL.binaryFourierCoeff {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (S : Finset (Fin n)) : ℝ
    def FABL.binaryFourierCoeff {n : ℕ}
  (f : FABL.F₂Cube n → ℝ)
  (S : Finset (Fin n)) : ℝ
    The Fourier coefficient of a real-valued function on the additive cube `𝔽₂ⁿ`.
  • theoremdefined in FABL/Chapter01/ProbabilityDensitiesAndConvolution.lean
    complete
    theorem FABL.binary_fourier_expansion {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  f x = ∑ S, FABL.binaryFourierCoeff f S * (FABL.χ S) x
    theorem FABL.binary_fourier_expansion {n : ℕ}
  (f : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  f x =
    ∑ S,
      FABL.binaryFourierCoeff f S *
        (FABL.χ S) x
    Fourier expansion on the additive cube, derived from Mathlib's finite-character basis.