Chapter 1: Boolean functions and the Fourier expansion — Internal lemmas #

Technical helper lemmas for the Fourier expansion theory. These support the main results in BooleanAnalysis.FourierExpansion but are not intended for direct use by downstream code.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.chi_zero :

chi 0 = 1

χ(0) = 1.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.chi_one :

chi 1 = -1

χ(1) = -1.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.chi_sq (b : ZMod 2) :

chi b ^ 2 = 1

χ(b)² = 1 for all b : ZMod 2.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.chi_mul_self (b : ZMod 2) :

chi b * chi b = 1

χ(b) · χ(b) = 1 (non-pow form, useful when simp doesn't see sq).

source

theorem Complexity.BooleanAnalysis.Internal.chi_eq_one_or_neg_one (b : ZMod 2) :

chi b = 1 ∨ chi b = -1

χ(b) = 1 or χ(b) = -1.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.chi_add (a b : ZMod 2) :

chi (a + b) = chi a * chi b

χ is multiplicative: χ(a + b) = χ(a) · χ(b).

source

theorem Complexity.BooleanAnalysis.Internal.chi_ne_zero (b : ZMod 2) :

chi b ≠ 0

χ(b) ≠ 0 for all b : ZMod 2.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.parityFun_empty {n : ℕ} :

parityFun ∅ = fun (x : Cube n) => 1

The parity function on the empty set is the constant function 1.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.parityFun_add {n : ℕ} (S : Finset (Fin n)) (x y : Cube n) :

parityFun S (x + y) = parityFun S x * parityFun S y

Parity functions are multiplicative: χ S (x + y) = χ S x · χ S y. (Equation 1.5 in the book)

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.parityFun_sq {n : ℕ} (S : Finset (Fin n)) (x : Cube n) :

parityFun S x ^ 2 = 1

(χ S x)² = 1 for all S and x.

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.parityFun_zero {n : ℕ} (S : Finset (Fin n)) :

parityFun S 0 = 1

χ S 0 = 1.

source

theorem Complexity.BooleanAnalysis.Internal.expect_parityFun_proof {n : ℕ} (S : Finset (Fin n)) :

expect (parityFun S) = if S = ∅ then 1 else 0

Fact 1.7: 𝔼[χ S] = 1 if S = ∅ and 𝔼[χ S] = 0 if S ≠ ∅.

source

theorem Complexity.BooleanAnalysis.Internal.expect_boolean_eq_prob_diff {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) :

expect f = (prob fun (x : Cube n) => f x = 1) - prob fun (x : Cube n) => f x = -1

Definition 1.11 (explicit form): For Boolean-valued f, 𝔼[f] = Pr[f = 1] - Pr[f = -1].

source

theorem Complexity.BooleanAnalysis.Internal.prob_boolean_sum_one {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) :

((prob fun (x : Cube n) => f x = 1) + prob fun (x : Cube n) => f x = -1) = 1

For Boolean-valued f, Pr[f = 1] + Pr[f = -1] = 1. (Implicit in Definition 1.11: every input maps to exactly one of 1 or -1.)

source

theorem Complexity.BooleanAnalysis.Internal.inner_add_two_hammingDist {n : ℕ} (f g : BooleanFunction n) (hf : IsBooleanValued f) (hg : IsBooleanValued g) :

inner ℝ f g + 2 * hammingDist f g = 1

Helper: ⟪f, g⟫ + 2 · dist(f, g) = 1 for Boolean-valued f, g.

source

theorem Complexity.BooleanAnalysis.Internal.parityFun_mul {n : ℕ} (S T : Finset (Fin n)) (x : Cube n) :

parityFun S x * parityFun T x = parityFun (symmDiff S T) x

χ_S · χ_T = χ_{S △ T} (pointwise).

source

theorem Complexity.BooleanAnalysis.Internal.parityFun_orthonormal_proof {n : ℕ} (S T : Finset (Fin n)) :

inner ℝ (parityFun S) (parityFun T) = if S = T then 1 else 0

Theorem 1.5: The parity functions are orthonormal: ⟪χ S, χ T⟫ = 1 if S = T and 0 otherwise.

source

theorem Complexity.BooleanAnalysis.Internal.sum_parityFun {n : ℕ} (z : Cube n) :

∑ S : Finset (Fin n), parityFun S z = if z = 0 then 2 ^ n else 0

Sum of all parity functions at a point: ∑_S χ_S(z) = 2^n if z = 0, else 0.

source

theorem Complexity.BooleanAnalysis.Internal.fourier_expansion_proof {n : ℕ} (f : BooleanFunction n) (x : Cube n) :

f x = ∑ S : Finset (Fin n), fourierCoeff f S * parityFun S x

The Fourier expansion: f(x) = ∑_S 𝓕 f S · χ_S(x).

source

theorem Complexity.BooleanAnalysis.Internal.fourier_uniqueness_proof {n : ℕ} (f : BooleanFunction n) (c : Finset (Fin n) → ℝ) (h : ∀ (x : Cube n), f x = ∑ S : Finset (Fin n), c S * parityFun S x) (T : Finset (Fin n)) :

c T = fourierCoeff f T

Fourier uniqueness: If f(x) = ∑_S c_S · χ_S(x) for all x, then c_S = 𝓕 f S for all S.

Proof: take ⟪–, χ T⟫ of both sides. On the right, orthonormality kills every term except S = T, leaving c T. On the left we get 𝓕 f T.

Orthonormal basis of parity functions #

The parity functions χ S form an orthonormal basis for BooleanFunction n under the uniform-measure inner product. Plancherel and Parseval follow directly from Mathlib's OrthonormalBasis API.

source

theorem Complexity.BooleanAnalysis.Internal.parityFun_orthonormal {n : ℕ} :

Orthonormal ℝ parityFun

The parity functions are orthonormal under the uniform-measure inner product.

source

theorem Complexity.BooleanAnalysis.Internal.parityFun_span {n : ℕ} :

⊤ ≤ Submodule.span ℝ (Set.range parityFun)

The parity functions span BooleanFunction n.

source

noncomputable def Complexity.BooleanAnalysis.Internal.parityOrthonormalBasis {n : ℕ} :

OrthonormalBasis (Finset (Fin n)) ℝ (BooleanFunction n)

The parity functions form an orthonormal basis for BooleanFunction n.

Equations

Complexity.BooleanAnalysis.Internal.parityOrthonormalBasis = OrthonormalBasis.mk ⋯ ⋯

Instances For

source

@[simp]

theorem Complexity.BooleanAnalysis.Internal.parityOrthonormalBasis_apply {n : ℕ} (S : Finset (Fin n)) :

parityOrthonormalBasis S = parityFun S

source

theorem Complexity.BooleanAnalysis.Internal.plancherel_proof {n : ℕ} (f g : BooleanFunction n) :

inner ℝ f g = ∑ S : Finset (Fin n), fourierCoeff f S * fourierCoeff g S

Plancherel's theorem: ⟪f, g⟫ = ∑_S 𝓕 f S · 𝓕 g S. Derived from the OrthonormalBasis of parity functions.

Helpers for §1.4 Proposition 1.15 (variance–distance bounds) #

source

theorem Complexity.BooleanAnalysis.Internal.hammingDist_const_one {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) :

(hammingDist f fun (x : Cube n) => 1) = prob fun (x : Cube n) => f x = -1

dist(f, 1) = Pr[f = -1] for Boolean-valued f.

source

theorem Complexity.BooleanAnalysis.Internal.hammingDist_const_neg_one {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) :

(hammingDist f fun (x : Cube n) => -1) = prob fun (x : Cube n) => f x = 1

dist(f, -1) = Pr[f = 1] for Boolean-valued f.

source

theorem Complexity.BooleanAnalysis.Internal.variance_dist_bounds_arith (p q : ℝ) (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) :

2 * min q p ≤ 4 * p * q ∧ 4 * p * q ≤ 4 * min q p

For p, q ≥ 0 with p + q = 1: 2 · min(q, p) ≤ 4pq ≤ 4 · min(q, p).

Helpers for §1.5 (densities and convolution) #

source

theorem Complexity.BooleanAnalysis.Internal.cube_add_right_cancel {n : ℕ} (z y : Cube n) :

z + y + y = z

z + y + y = z in 𝔽₂ⁿ (characteristic 2 cancellation).

source

theorem Complexity.BooleanAnalysis.Internal.setDensity_singleton_zero_ite {n : ℕ} (y : Cube n) :

setDensity {0} y = if y = 0 then 2 ^ n else 0

setDensity {0} evaluates to 2^n at 0 and 0 elsewhere.

source

theorem Complexity.BooleanAnalysis.Internal.setDensity_singleton_zero_proof {n : ℕ} (y : Cube n) :

setDensity {0} y = ∑ S : Finset (Fin n), parityFun S y

setDensity {0} equals the sum of all parity functions.

source

theorem Complexity.BooleanAnalysis.Internal.fourierCoeff_setDensity_singleton_zero_proof {n : ℕ} (S : Finset (Fin n)) :

fourierCoeff (setDensity {0}) S = 1

Every Fourier coefficient of setDensity {0} is 1.

source

theorem Complexity.BooleanAnalysis.Internal.convolution_density_isDensity_proof {n : ℕ} (φ ψ : BooleanFunction n) (hφ : IsDensity φ) (hψ : IsDensity ψ) :

IsDensity (convolution φ ψ)

The convolution of two densities is again a density.

source

theorem Complexity.BooleanAnalysis.Internal.fourierCoeff_convolution_proof {n : ℕ} (f g : BooleanFunction n) (S : Finset (Fin n)) :

fourierCoeff (convolution f g) S = fourierCoeff f S * fourierCoeff g S

The convolution theorem: 𝓕 (f ⊛ g) S = (𝓕 f S) · (𝓕 g S).

Helpers for §1.6 (BLR test and local correctability) #

source

theorem Complexity.BooleanAnalysis.Internal.prob_compl {n : ℕ} (P : Cube n → Prop) :

(prob P + prob fun (x : Cube n) => ¬P x) = 1

Pr[P] + Pr[¬P] = 1.

source

theorem Complexity.BooleanAnalysis.Internal.prob_nonneg {n : ℕ} (P : Cube n → Prop) :

0 ≤ prob P

0 ≤ Pr[P].

source

theorem Complexity.BooleanAnalysis.Internal.prob_union_bound {n : ℕ} {P Q R : Cube n → Prop} (h : ∀ (x : Cube n), ¬P x → Q x ∨ R x) :

(prob fun (x : Cube n) => ¬P x) ≤ prob Q + prob R

Union bound: if ¬P ⊆ Q ∪ R then Pr[¬P] ≤ Pr[Q] + Pr[R].

source

theorem Complexity.BooleanAnalysis.Internal.prob_shift {n : ℕ} (P : Cube n → Prop) (x : Cube n) :

(prob fun (y : Cube n) => P (x + y)) = prob P

Shift invariance of probability: Pr_y[P(x + y)] = Pr_z[P(z)].

source

theorem Complexity.BooleanAnalysis.Internal.parityFun_mul_cancel {n : ℕ} (S : Finset (Fin n)) (x y : Cube n) :

parityFun S y * parityFun S (x + y) = parityFun S x

χ S y · χ S (x + y) = χ S x (key identity for local correctability).

source

theorem Complexity.BooleanAnalysis.Internal.local_correctability_proof {n : ℕ} (f : BooleanFunction n) (_hf : IsBooleanValued f) (S : Finset (Fin n)) (ε : ℝ) (hclose : IsClose f (parityFun S) ε) (x : Cube n) :

(prob fun (y : Cube n) => f y * f (x + y) = parityFun S x) ≥ 1 - 2 * ε

Local correctability of the Fourier decoding algorithm.

Helpers for §1.6 (BLR acceptance probability and soundness) #

source

theorem Complexity.BooleanAnalysis.Internal.parseval_proof {n : ℕ} (f : BooleanFunction n) :

inner ℝ f f = ∑ S : Finset (Fin n), fourierCoeff f S ^ 2

Parseval's theorem: ⟪f, f⟫ = ∑_S (𝓕 f S)².

source

theorem Complexity.BooleanAnalysis.Internal.parseval_boolean_proof {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) :

∑ S : Finset (Fin n), fourierCoeff f S ^ 2 = 1

Parseval's theorem for Boolean-valued functions.

source

theorem Complexity.BooleanAnalysis.Internal.fourierCoeff_sq_le_one {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) (S : Finset (Fin n)) :

fourierCoeff f S ^ 2 ≤ 1

For Boolean f, (𝓕 f S)² ≤ 1.

source

theorem Complexity.BooleanAnalysis.Internal.cube_le_max_sq {n : ℕ} {f : BooleanFunction n} (_f : BooleanFunction n) (_hf : IsBooleanValued f) (c : ℝ) (hmax : ∀ (T : Finset (Fin n)), fourierCoeff f T ≤ c) (S : Finset (Fin n)) :

fourierCoeff f S ^ 3 ≤ c * fourierCoeff f S ^ 2

For Boolean f, (𝓕 f S)³ ≤ c · (𝓕 f S)² when c dominates all Fourier coefficients.

source

theorem Complexity.BooleanAnalysis.Internal.parityFun_isBoolean {n : ℕ} (S : Finset (Fin n)) :

IsBooleanValued (parityFun S)

Parity functions are Boolean-valued.

source

theorem Complexity.BooleanAnalysis.Internal.hammingDist_eq_fourier {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) (S : Finset (Fin n)) :

hammingDist f (parityFun S) = (1 - fourierCoeff f S) / 2

dist(f, χ S) = (1 - 𝓕 f S) / 2 for Boolean-valued f.

source

theorem Complexity.BooleanAnalysis.Internal.blr_indicator_eq {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) (x y : Cube n) :

indicator (fun (y : Cube n) => f x * f y = f (x + y)) y = (1 + f x * f y * f (x + y)) / 2

For Boolean f, the BLR indicator equals (1 + f(x)·f(y)·f(x+y))/2.

source

theorem Complexity.BooleanAnalysis.Internal.triple_expect_eq {n : ℕ} (f : BooleanFunction n) :

(expect fun (x : Cube n) => expect fun (y : Cube n) => f x * f y * f (x + y)) = inner ℝ f (convolution f f)

𝔼_x[𝔼_y[f(x)·f(y)·f(x+y)]] = ⟪f, f ⊛ f⟫.

source

theorem Complexity.BooleanAnalysis.Internal.inner_conv_eq_sum_cube {n : ℕ} (f : BooleanFunction n) :

inner ℝ f (convolution f f) = ∑ S : Finset (Fin n), fourierCoeff f S ^ 3

⟪f, f ⊛ f⟫ = ∑_S (𝓕 f S)³.

source

theorem Complexity.BooleanAnalysis.Internal.expect_add_const {n : ℕ} (c : ℝ) (g : BooleanFunction n) :

(expect fun (x : Cube n) => c + g x) = c + expect g

Linearity of expectation: 𝔼[c + g] = c + 𝔼[g].

source

theorem Complexity.BooleanAnalysis.Internal.expect_scale {n : ℕ} (c : ℝ) (g : BooleanFunction n) :

(expect fun (x : Cube n) => c * g x) = c * expect g

Linearity of expectation: 𝔼[c · g] = c · 𝔼[g].

source

theorem Complexity.BooleanAnalysis.Internal.blrAcceptProb_eq_proof {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) :

blrAcceptProb f = 1 / 2 + 1 / 2 * ∑ S : Finset (Fin n), fourierCoeff f S ^ 3

The BLR acceptance probability formula.

source

theorem Complexity.BooleanAnalysis.Internal.blr_completeness_proof {n : ℕ} (f : BooleanFunction n) (hf : IsLinear f) :

blrAcceptProb f = 1

BLR completeness: If f is linear (i.e., f = χ_S for some S), then the BLR test accepts with probability 1.

source

theorem Complexity.BooleanAnalysis.Internal.blr_soundness_proof {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) (ε : ℝ) (hε : blrAcceptProb f ≥ 1 - ε) :

IsCloseToProperty f IsLinear ε

BLR soundness: if the BLR test accepts with probability ≥ 1 - ε, then f is ε-close to a linear function.

Equivalence of linearity characterizations (§1.6) #

source

theorem Complexity.BooleanAnalysis.Internal.multiplicative_zero {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) (hmul : IsMultiplicative f) :

f 0 = 1

For Boolean-valued multiplicative f, f(0) = 1.

source

theorem Complexity.BooleanAnalysis.Internal.isLinear_isMultiplicative {n : ℕ} (f : BooleanFunction n) (hlin : IsLinear f) :

IsMultiplicative f

Linear implies multiplicative.

source

theorem Complexity.BooleanAnalysis.Internal.multiplicative_finset_sum {n : ℕ} {ι : Type u_1} (f : BooleanFunction n) (hf : IsBooleanValued f) (hmul : IsMultiplicative f) (s : Finset ι) (g : ι → Cube n) :

f (∑ i ∈ s, g i) = ∏ i ∈ s, f (g i)

A multiplicative function distributes over finite sums: f(∑_{i ∈ s} gᵢ) = ∏_{i ∈ s} f(gᵢ).

source

theorem Complexity.BooleanAnalysis.Internal.cube_eq_sum_support {n : ℕ} (x : Cube n) :

x = ∑ i : Fin n with x i = 1, Pi.single i 1

In 𝔽₂ⁿ, every element is the sum of its support basis vectors: x = ∑_{i : x i = 1} eᵢ.

source

theorem Complexity.BooleanAnalysis.Internal.isMultiplicative_isLinear {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) (hmul : IsMultiplicative f) :

IsLinear f

Multiplicative + Boolean-valued implies linear. Key idea: define S = {i | f(eᵢ) = -1} and show f = χ S by decomposing x into a sum of basis vectors and using multiplicativity.

source