Boolean Analysis

This file develops the basic theory of Boolean functions f : {-1, 1}ⁿ → ℝ (or equivalently f : {0, 1}ⁿ → ℝ) and their Fourier–Walsh expansion over the real numbers.

Main definitions

• BooleanFunc n: the type of functions (Fin n → Bool) → ℝ.
• innerProduct f g: the inner product 𝔼[f · g] = 2⁻ⁿ ∑_{x} f(x) g(x).
• chiS n S: the Walsh–Fourier character χ_S(x) = (-1)^{|S ∩ supp(x)|} for S : Finset (Fin n).
• fourierCoeff f S: the Fourier coefficient f̂(S) = ⟪f, χ_S⟫.
• influence i f: the influence of coordinate i on f, Inf_i[f] = 𝔼[(f(x) - f(xⁱ))² / 4] where xⁱ is x with bit i flipped.
• totalInfluence f: the total influence I[f] = ∑ᵢ Inf_i[f].
• noise f ρ: the noise operator T_ρ f(x) = 𝔼_y[f(y)] where each bit of y is x independently with probability (1+ρ)/2 and flipped with probability (1-ρ)/2.

Main results

• walsh_expansion: every Boolean function has a unique Fourier–Walsh expansion f = ∑_{S ⊆ [n]} f̂(S) χ_S.
• parseval: Parseval's identity ‖f‖² = ∑_S f̂(S)².
• fourier_coeff_chi: orthonormality of the Walsh characters, ⟪χ_S, χ_T⟫ = [S = T].
• totalInfluence_eq_sum_sq_deg: I[f] = ∑_S |S| · f̂(S)².

Notation

• 𝔹 n for Fin n → Bool (the Boolean hypercube).
• ⟪f, g⟫_𝔹 for the Boolean inner product.
• χ_[S] for the Walsh character of S.

References

• Ryan O'Donnell, Analysis of Boolean Functions, Cambridge University Press, 2014.

Setup: the Boolean hypercube

@[reducible, inline]

abbrev BooleanAnalysis.BoolCube (n : ℕ) : Type

The Boolean hypercube {0,1}ⁿ.

Equations

• BooleanAnalysis.BoolCube n = (Fin n → Bool)

@[reducible, inline]

abbrev BooleanAnalysis.BooleanFunc (n : ℕ) : Type

A Boolean function f : {0,1}ⁿ → ℝ.

Equations

• BooleanAnalysis.BooleanFunc n = (BooleanAnalysis.BoolCube n → ℝ)

Uniform measure and expectation

noncomputable def BooleanAnalysis.uniformWeight (n : ℕ) : ℝ

The uniform probability measure on {0,1}ⁿ assigns weight 2⁻ⁿ to each point.

Equations

• BooleanAnalysis.uniformWeight n = 2⁻¹ ^ n

noncomputable def BooleanAnalysis.expect {n : ℕ} (f : BooleanFunc n) : ℝ

Expectation of f under the uniform measure on {0,1}ⁿ. 𝔼[f] = 2⁻ⁿ · ∑_{x ∈ {0,1}ⁿ} f(x).

Equations

• BooleanAnalysis.expect f = BooleanAnalysis.uniformWeight n * ∑ x : BooleanAnalysis.BoolCube n, f x

noncomputable def BooleanAnalysis.innerProduct {n : ℕ} (f g : BooleanFunc n) : ℝ

The L² inner product on Boolean functions with respect to the uniform measure: ⟪f, g⟫ = 𝔼[f · g] = 2⁻ⁿ · ∑_x f(x) g(x).

Equations

• BooleanAnalysis.innerProduct f g = BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => f x * g x

def BooleanAnalysis.«term⟪_,_⟫_𝔹» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BooleanAnalysis.l2Norm {n : ℕ} (f : BooleanFunc n) : ℝ

The L² norm of a Boolean function: ‖f‖ = √(⟪f, f⟫).

Equations

• BooleanAnalysis.l2Norm f = √(BooleanAnalysis.innerProduct f f)

Walsh–Fourier characters

def BooleanAnalysis.boolToSign (b : Bool) : ℝ

Convert a Bool to {-1, 1} ⊆ ℝ: false ↦ 1, true ↦ -1.

Equations

• BooleanAnalysis.boolToSign b = if b = true then -1 else 1

@[simp]

theorem BooleanAnalysis.boolToSign_false : boolToSign false = 1

@[simp]

theorem BooleanAnalysis.boolToSign_true : boolToSign true = -1

@[simp]

theorem BooleanAnalysis.boolToSign_sq (b : Bool) : boolToSign b ^ 2 = 1

@[simp]

theorem BooleanAnalysis.boolToSign_mul_self (b : Bool) : boolToSign b * boolToSign b = 1

noncomputable def BooleanAnalysis.chiS {n : ℕ} (S : Finset (Fin n)) : BooleanFunc n

The Walsh–Fourier character χ_S : {0,1}ⁿ → ℝ associated to a set S ⊆ [n]. χ_S(x) = ∏_{i ∈ S} (-1)^{x_i}.

This forms an orthonormal basis for L²({0,1}ⁿ, uniform).

Equations

• BooleanAnalysis.chiS S x = ∏ i ∈ S, BooleanAnalysis.boolToSign (x i)

def BooleanAnalysis.«termχ_[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BooleanAnalysis.chiS_empty {n : ℕ} : chiS ∅ = fun (x : BoolCube n) => 1

The character χ_∅ is the constant function 1.

@[simp]

theorem BooleanAnalysis.chiS_singleton {n : ℕ} (i : Fin n) (x : BoolCube n) : chiS {i} x = boolToSign (x i)

The character χ_{i} for a singleton {i} equals (-1)^{x_i}.

theorem BooleanAnalysis.chiS_sq_eq_one {n : ℕ} (S : Finset (Fin n)) (x : BoolCube n) : chiS S x ^ 2 = 1

Walsh characters take values in {-1, 1}.

theorem BooleanAnalysis.chiS_mul_of_disjoint {n : ℕ} (S T : Finset (Fin n)) (hST : Disjoint S T) (x : BoolCube n) : chiS (S ∪ T) x = chiS S x * chiS T x

Walsh characters are multiplicative: χ_{S ∪ T}(x) = χ_S(x) · χ_T(x) when S and T are disjoint.

theorem BooleanAnalysis.chiS_mul_chiS {n : ℕ} (S T : Finset (Fin n)) (x : BoolCube n) : chiS S x * chiS T x = chiS (symmDiff S T) x

The pointwise product of two Walsh characters is another Walsh character (up to sign), specifically χ_S · χ_T = χ_{S Δ T} where Δ denotes symmetric difference.

Fourier coefficients

noncomputable def BooleanAnalysis.fourierCoeff {n : ℕ} (f : BooleanFunc n) (S : Finset (Fin n)) : ℝ

The Fourier–Walsh coefficient of f at frequency S: f̂(S) = ⟪f, χ_S⟫ = 2⁻ⁿ · ∑_x f(x) · χ_S(x).

Equations

• BooleanAnalysis.fourierCoeff f S = BooleanAnalysis.innerProduct f (BooleanAnalysis.chiS S)

def BooleanAnalysis.«term_̂(_)» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem BooleanAnalysis.fourierCoeff_empty {n : ℕ} (f : BooleanFunc n) : fourierCoeff f ∅ = expect f

The Fourier coefficient at ∅ equals the expectation of f.

Fourier inversion (Walsh expansion)

theorem BooleanAnalysis.walsh_expansion {n : ℕ} (f : BooleanFunc n) (x : BoolCube n) : f x = ∑ S : Finset (Fin n), fourierCoeff f S * chiS S x

Walsh Expansion: every Boolean function f : {0,1}ⁿ → ℝ can be written as f(x) = ∑_{S ⊆ [n]} f̂(S) · χ_S(x).

This is the Fourier inversion formula for the uniform measure on {0,1}ⁿ.

Parseval's identity

Orthonormality of Walsh characters

theorem BooleanAnalysis.fourier_coeff_chi {n : ℕ} (S T : Finset (Fin n)) : innerProduct (chiS S) (chiS T) = if S = T then 1 else 0

Orthonormality: ⟪χ_S, χ_T⟫ = [S = T].

The Walsh characters form an orthonormal system in L²({0,1}ⁿ, uniform).

@[simp]

theorem BooleanAnalysis.innerProduct_chi_self {n : ℕ} (S : Finset (Fin n)) : innerProduct (chiS S) (chiS S) = 1

Self inner product of a Walsh character is 1.

theorem BooleanAnalysis.parseval {n : ℕ} (f : BooleanFunc n) : innerProduct f f = ∑ S : Finset (Fin n), fourierCoeff f S ^ 2

Parseval's Identity: ‖f‖² = ∑_{S ⊆ [n]} f̂(S)².

The sum of squared Fourier coefficients equals the squared L² norm.

def BooleanAnalysis.flipBit {n : ℕ} (x : BoolCube n) (i : Fin n) : BoolCube n

Flip the i-th bit of x : {0,1}ⁿ.

Equations

• BooleanAnalysis.flipBit x i = Function.update x i !x i

@[simp]

theorem BooleanAnalysis.flipBit_flipBit {n : ℕ} (x : BoolCube n) (i : Fin n) : flipBit (flipBit x i) i = x

theorem BooleanAnalysis.flipBit_ne {n : ℕ} (x : BoolCube n) (i j : Fin n) (h : i ≠ j) : flipBit x i j = x j

Influence of a coordinate

noncomputable def BooleanAnalysis.influence {n : ℕ} (i : Fin n) (f : BooleanFunc n) : ℝ

The influence of coordinate i on f: Inf_i[f] = Pr_x[f(x) ≠ f(xⁱ)] where xⁱ denotes x with the i-th bit flipped.

For {-1,1}-valued functions this equals 𝔼[(f(x) - f(xⁱ))² / 4].

Equations

• BooleanAnalysis.influence i f = BooleanAnalysis.expect fun (x : BooleanAnalysis.BoolCube n) => (f x - f (BooleanAnalysis.flipBit x i)) ^ 2 / 4

noncomputable def BooleanAnalysis.totalInfluence {n : ℕ} (f : BooleanFunc n) : ℝ

The total influence of f: I[f] = ∑_{i=1}^{n} Inf_i[f].

Equations

• BooleanAnalysis.totalInfluence f = ∑ i : Fin n, BooleanAnalysis.influence i f

theorem BooleanAnalysis.influence_chi {n : ℕ} (i : Fin n) (S : Finset (Fin n)) : influence i (chiS S) = if i ∈ S then 1 else 0

The influence of i on the Walsh character χ_S is [i ∈ S].

theorem BooleanAnalysis.influence_eq_sum_fourier {n : ℕ} (i : Fin n) (f : BooleanFunc n) : influence i f = ∑ S : Finset (Fin n), if i ∈ S then fourierCoeff f S ^ 2 else 0

Influence via Fourier: Inf_i[f] = ∑_{S ∋ i} f̂(S)².

theorem BooleanAnalysis.totalInfluence_eq_sum_sq_deg {n : ℕ} (f : BooleanFunc n) : totalInfluence f = ∑ S : Finset (Fin n), ↑S.card * fourierCoeff f S ^ 2

Total Influence via Fourier: I[f] = ∑_S |S| · f̂(S)².

Noise operator

noncomputable def BooleanAnalysis.noiseOp {n : ℕ} (ρ : ℝ) (f : BooleanFunc n) : BooleanFunc n

The noise operator T_ρ with noise rate ρ ∈ [-1, 1]: T_ρ f(x) = 𝔼_y[f(y)] where each coordinate of y independently equals x_i with probability (1+ρ)/2 and ¬x_i with probability (1-ρ)/2.

In the Fourier domain: (T_ρ f)̂(S) = ρ^{|S|} · f̂(S).

Equations

• BooleanAnalysis.noiseOp ρ f x = ∑ S : Finset (Fin n), ρ ^ S.card * BooleanAnalysis.fourierCoeff f S * BooleanAnalysis.chiS S x

theorem BooleanAnalysis.noiseOp_fourier {n : ℕ} (ρ : ℝ) (f : BooleanFunc n) (S : Finset (Fin n)) : fourierCoeff (noiseOp ρ f) S = ρ ^ S.card * fourierCoeff f S

Noise operator in Fourier domain: (T_ρ f)̂(S) = ρ^{|S|} · f̂(S).

theorem BooleanAnalysis.stability_formula {n : ℕ} (ρ : ℝ) (f : BooleanFunc n) : innerProduct f (noiseOp ρ f) = ∑ S : Finset (Fin n), ρ ^ S.card * fourierCoeff f S ^ 2

Stability formula: ⟪f, T_ρ f⟫ = ∑_S ρ^{|S|} · f̂(S)².

Linearity and combinatorial properties

instance BooleanAnalysis.instAddCommGroupBooleanFunc {n : ℕ} : AddCommGroup (BooleanFunc n)

Boolean functions form an ℝ-vector space.

Equations

• BooleanAnalysis.instAddCommGroupBooleanFunc = Pi.addCommGroup

noncomputable instance BooleanAnalysis.instModuleRealBooleanFunc {n : ℕ} : Module ℝ (BooleanFunc n)

Equations

• BooleanAnalysis.instModuleRealBooleanFunc = Pi.module (BooleanAnalysis.BoolCube n) (fun (a : BooleanAnalysis.BoolCube n) => ℝ) ℝ

theorem BooleanAnalysis.innerProduct_add_left {n : ℕ} (f g h : BooleanFunc n) : innerProduct (f + g) h = innerProduct f h + innerProduct g h

The inner product is bilinear in the first argument.

theorem BooleanAnalysis.innerProduct_comm {n : ℕ} (f g : BooleanFunc n) : innerProduct f g = innerProduct g f

The inner product is symmetric.

theorem BooleanAnalysis.innerProduct_self_nonneg {n : ℕ} (f : BooleanFunc n) : 0 ≤ innerProduct f f

The inner product is nonneg on the diagonal.

theorem BooleanAnalysis.card_walsh_characters {n : ℕ} : Finset.univ.card = 2 ^ n

The Walsh characters {χ_S}_{S ⊆ [n]} span L²({0,1}ⁿ). There are exactly 2ⁿ characters, matching the dimension of L²({0,1}ⁿ) ≅ ℝ^{2ⁿ}.

Dictator and parity functions

noncomputable def BooleanAnalysis.dictator {n : ℕ} (i : Fin n) : BooleanFunc n

The dictator function for coordinate i: f(x) = (-1)^{x_i}. Its only nonzero Fourier coefficient is f̂({i}) = 1.

Equations

• BooleanAnalysis.dictator i x = BooleanAnalysis.boolToSign (x i)

theorem BooleanAnalysis.dictator_eq_chi {n : ℕ} (i : Fin n) : dictator i = chiS {i}

The dictator function equals the Walsh character χ_{i}.

noncomputable def BooleanAnalysis.parity (n : ℕ) : BooleanFunc n

The parity function f(x) = (-1)^{x_1 + ⋯ + x_n}. Its only nonzero Fourier coefficient is f̂([n]) = 1.

Equations

• BooleanAnalysis.parity n x = ∏ i : Fin n, BooleanAnalysis.boolToSign (x i)

theorem BooleanAnalysis.parity_eq_chi_univ {n : ℕ} : parity n = chiS Finset.univ

The parity function equals χ_{Finset.univ}.

noncomputable def BooleanAnalysis.majority (k : ℕ) : BooleanFunc (2 * k + 1)

The majority function on {0,1}^{2k+1}: outputs 1 if more than half the bits are 0, and -1 otherwise.

Equations

• BooleanAnalysis.majority k x = if {i : Fin (2 * k + 1) | x i = false}.card > k then 1 else -1

Sensitivity and block sensitivity

noncomputable def BooleanAnalysis.sensitivity {n : ℕ} (f : BooleanFunc n) (x : BoolCube n) : ℕ

The sensitivity of f at x: the number of coordinates i such that flipping bit i changes the value of f.

Equations

• BooleanAnalysis.sensitivity f x = {i : Fin n | f x ≠ f (BooleanAnalysis.flipBit x i)}.card

noncomputable def BooleanAnalysis.maxSensitivity {n : ℕ} (f : BooleanFunc n) : ℕ

The maximum sensitivity of f over all inputs.

Equations

• BooleanAnalysis.maxSensitivity f = Finset.univ.sup (BooleanAnalysis.sensitivity f)

theorem BooleanAnalysis.influence_le_one {n : ℕ} (i : Fin n) (f : BooleanFunc n) (hf : ∀ (x : BoolCube n), f x ∈ {-1, 1}) : influence i f ≤ 1

Influence bounds sensitivity: Inf_i[f] ≤ 1.

theorem BooleanAnalysis.max_influence_lower_bound {n : ℕ} (f : BooleanFunc n) (hn : 0 < n) : ∃ (i : Fin n), totalInfluence f / ↑n ≤ influence i f

For any Boolean function f, the maximum individual influence is at least the average: max_i Inf_i[f] ≥ I[f] / n.

Additional lemmas for Arrow's theorem

@[simp]

theorem BooleanAnalysis.boolToSign_not (b : Bool) : (boolToSign !b) = -boolToSign b

boolToSign negates under Bool.not.

theorem BooleanAnalysis.chiS_neg {n : ℕ} (S : Finset (Fin n)) (x : BoolCube n) : (chiS S fun (i : Fin n) => !x i) = (-1) ^ S.card * chiS S x

Flipping all bits of x multiplies χ_S(x) by (-1)^|S|.

def BooleanAnalysis.isOddFunc {n : ℕ} (f : BooleanFunc n) : Prop

A Boolean function is odd if flipping all inputs negates the output. Models the antisymmetry requirement in social choice.

Equations

• BooleanAnalysis.isOddFunc f = ∀ (x : BooleanAnalysis.BoolCube n), (f fun (i : Fin n) => !x i) = -f x

def BooleanAnalysis.isPmOne {n : ℕ} (f : BooleanFunc n) : Prop

A Boolean function takes values in {-1, 1}.

Equations

• BooleanAnalysis.isPmOne f = ∀ (x : BooleanAnalysis.BoolCube n), f x = 1 ∨ f x = -1

theorem BooleanAnalysis.fourierCoeff_odd_even {n : ℕ} (f : BooleanFunc n) (hodd : isOddFunc f) (S : Finset (Fin n)) (heven : Even S.card) : fourierCoeff f S = 0

For an odd function, the Fourier coefficient at any even-cardinality set is zero.

theorem BooleanAnalysis.innerProduct_self_pm_one {n : ℕ} (f : BooleanFunc n) (hf : isPmOne f) : innerProduct f f = 1

For a ±1-valued function, the L² self-inner-product equals 1.

theorem BooleanAnalysis.parseval_pm_one {n : ℕ} (f : BooleanFunc n) (hf : isPmOne f) : ∑ S : Finset (Fin n), fourierCoeff f S ^ 2 = 1

Parseval for ±1-valued functions: ∑_S f̂(S)² = 1.

noncomputable def BooleanAnalysis.weightLevel {n : ℕ} (k : ℕ) (f : BooleanFunc n) : ℝ

Fourier weight concentrated on level k: W_k[f] = ∑_{|S|=k} f̂(S)².

Equations

• BooleanAnalysis.weightLevel k f = ∑ S : Finset (Fin n), if S.card = k then BooleanAnalysis.fourierCoeff f S ^ 2 else 0