Documentation

Complexitylib.BooleanAnalysis.FourierExpansion

Chapter 1: Boolean functions and the Fourier expansion #

This file contains the main theorems from Chapter 1 of "Analysis of Boolean Functions" by Ryan O'Donnell.

References #

Β§1.2 The Fourier expansion theorem #

source
theorem Complexity.BooleanAnalysis.fourier_expansion {n : β„•} (f : BooleanFunction n) (x : Cube n) :
f x = βˆ‘ S : Finset (Fin n), fourierCoeff f S * parityFun S x

Theorem 1.1 (Fourier expansion existence): Every function f : 𝔽₂ⁿ β†’ ℝ can be expressed as f(x) = βˆ‘_S 𝓕 f S Β· (Ο‡ S) x.

source
theorem Complexity.BooleanAnalysis.fourier_uniqueness {n : β„•} (f : BooleanFunction n) (c : Finset (Fin n) β†’ ℝ) (h : βˆ€ (x : Cube n), f x = βˆ‘ S : Finset (Fin n), c S * parityFun S x) (S : Finset (Fin n)) :
c S = fourierCoeff f S

Theorem 1.1 (Fourier uniqueness): If f(x) = βˆ‘_S c_S Β· Ο‡_S(x) for all x, then c_S = 𝓕 f S for all S. Together with fourier_expansion, this establishes the parity functions as an orthonormal basis for the space of functions 𝔽₂ⁿ β†’ ℝ.

Β§1.3 Orthonormality of parity functions #

source
theorem Complexity.BooleanAnalysis.parityFun_add {n : β„•} (S : Finset (Fin n)) (x y : Cube n) :
parityFun S (x + y) = parityFun S x * parityFun S y

Equation 1.5: (Ο‡ S)(x + y) = (Ο‡ S) x Β· (Ο‡ S) y.

source
theorem Complexity.BooleanAnalysis.parityFun_mul {n : β„•} (S T : Finset (Fin n)) (x : Cube n) :
parityFun S x * parityFun T x = parityFun (symmDiff S T) x

Fact 1.6: (Ο‡ S) x Β· (Ο‡ T) x = (Ο‡ (S β–³ T)) x.

source
theorem Complexity.BooleanAnalysis.expect_parityFun {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.parityFun_orthonormal {n : β„•} (S T : Finset (Fin n)) :
inner ℝ (parityFun S) (parityFun T) = if S = T then 1 else 0

Theorem 1.5 (orthonormality): The parity functions are orthonormal: βŸͺΟ‡ S, Ο‡ T⟫ = 1 if S = T and 0 otherwise.

source
theorem Complexity.BooleanAnalysis.parityFun_span {n : β„•} (f : BooleanFunction n) :
βˆƒ (c : Finset (Fin n) β†’ ℝ), βˆ€ (x : Cube n), f x = βˆ‘ S : Finset (Fin n), c S * parityFun S x

Theorem 1.5 (spanning): Every function f : 𝔽₂ⁿ β†’ ℝ is a linear combination of parity functions. Together with parityFun_orthonormal, this establishes that the parity functions form an orthonormal basis for the space of functions 𝔽₂ⁿ β†’ ℝ.

Β§1.4 Basic Fourier formulas #

source
theorem Complexity.BooleanAnalysis.fourierCoeff_eq_inner {n : β„•} (f : BooleanFunction n) (S : Finset (Fin n)) :
fourierCoeff f S = inner ℝ f (parityFun S)

Proposition 1.8: 𝓕 f S = βŸͺf, Ο‡ S⟫. This is true by definition.

source
theorem Complexity.BooleanAnalysis.parseval {n : β„•} (f : BooleanFunction n) :
inner ℝ f f = βˆ‘ S : Finset (Fin n), fourierCoeff f S ^ 2

Parseval's Theorem: βŸͺf, f⟫ = βˆ‘ S, (𝓕 f S) ^ 2.

source
theorem Complexity.BooleanAnalysis.parseval_boolean {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
βˆ‘ S : Finset (Fin n), fourierCoeff f S ^ 2 = 1

Parseval's Theorem (Boolean case): For Boolean-valued f, βˆ‘ S, (𝓕 f S) ^ 2 = 1.

source
theorem Complexity.BooleanAnalysis.inner_self_nonneg' {n : β„•} (f : BooleanFunction n) :
0 ≀ inner ℝ f f

The inner product βŸͺf, f⟫ is nonneg.

source
theorem Complexity.BooleanAnalysis.norm_sq_eq_inner {n : β„•} (f : BooleanFunction n) :
β€–fβ€– ^ 2 = inner ℝ f f

β€–fβ€–β‚‚Β² = βŸͺf, f⟫.

source
theorem Complexity.BooleanAnalysis.norm_sq_eq_sum_fourierCoeff_sq {n : β„•} (f : BooleanFunction n) :
β€–fβ€– ^ 2 = βˆ‘ S : Finset (Fin n), fourierCoeff f S ^ 2

β€–fβ€–β‚‚Β² = βˆ‘_S (𝓕 f S)Β² (Parseval via LΒ² norm).

source
theorem Complexity.BooleanAnalysis.sum_fourierWeightAtDegree {n : β„•} (f : BooleanFunction n) :
βˆ‘ k ∈ Finset.range (n + 1), fourierWeightAtDegree f k = inner ℝ f f

Parseval, partitioned by degree: summing the Fourier weight at each degree k = 0, …, n recovers βŸͺf, f⟫. Every coordinate set S βŠ† [n] has |S| ≀ n, so grouping the Fourier weights by |S| reassembles Parseval's total. This is the identity behind the degree/weight distribution 𝐖.

source
theorem Complexity.BooleanAnalysis.sum_degreePart {n : β„•} (f : BooleanFunction n) (x : Cube n) :
βˆ‘ k ∈ Finset.range (n + 1), degreePart f k x = f x

The degree decomposition of f: summing the degree-k parts f^{=k} over k = 0, …, n reconstructs f pointwise. This regroups the Fourier expansion f = βˆ‘_S 𝓕 f S Β· Ο‡_S by |S|, and is the starting point for the low-degree / degree-concentration results used in small-depth-circuit lower bounds.

source
theorem Complexity.BooleanAnalysis.fourierWeightAtDegree_nonneg {n : β„•} (f : BooleanFunction n) (k : β„•) :
0 ≀ fourierWeightAtDegree f k

The Fourier weight at any degree is nonnegative (it is a sum of squares).

source
theorem Complexity.BooleanAnalysis.sum_fourierWeightAtDegree_boolean {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
βˆ‘ k ∈ Finset.range (n + 1), fourierWeightAtDegree f k = 1

Total Fourier weight of a Boolean function is one. Summing the degree-k weights of a Β±1-valued function over all degrees gives 1, since βŸͺf, f⟫ = 𝔼[fΒ²] = 𝔼[1] = 1. This is what makes k ↦ 𝐖 f k a probability distribution on degrees β€” the spectral sample of f.

source
theorem Complexity.BooleanAnalysis.lowDegreePart_card {n : β„•} (f : BooleanFunction n) (x : Cube n) :
lowDegreePart f n x = f x

The degree-≀ n part is all of f. Every coordinate set has size at most n, so truncating at degree n keeps every Fourier term: f^{≀n} = f.

source
theorem Complexity.BooleanAnalysis.degreePart_eq_zero_of_lt {n : β„•} (f : BooleanFunction n) (x : Cube n) {k : β„•} (hk : n < k) :
degreePart f k x = 0

No mass above degree n. There are no coordinate sets of size greater than n, so every degree part f^{=k} with k > n is identically zero.

source
theorem Complexity.BooleanAnalysis.fourierWeightAtDegree_eq_zero_of_lt {n : β„•} (f : BooleanFunction n) {k : β„•} (hk : n < k) :
fourierWeightAtDegree f k = 0

No Fourier weight above degree n. For k > n the degree-k weight vanishes, so the degree-weight sum βˆ‘_{k=0}^n 𝐖 f k already captures all of f's spectral energy.

source
theorem Complexity.BooleanAnalysis.lowDegreePart_eq_sum_degreePart {n : β„•} (f : BooleanFunction n) (x : Cube n) (k : β„•) :
lowDegreePart f k x = βˆ‘ j ∈ Finset.range (k + 1), degreePart f j x

The low-degree part is the sum of exact-degree parts. f^{≀k} = βˆ‘_{j≀k} f^{=j}, obtained by grouping the coordinate sets of size ≀ k by their exact size β€” the identity linking the two degree-truncation operators.

source
theorem Complexity.BooleanAnalysis.plancherel {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).

source
theorem Complexity.BooleanAnalysis.inner_eq_agree_sub_disagree {n : β„•} (f g : BooleanFunction n) (hf : IsBooleanValued f) (hg : IsBooleanValued g) :
inner ℝ f g = 1 - hammingDist f g - hammingDist f g

Proposition 1.9a: For Boolean-valued f, g, βŸͺf, g⟫ = Pr[f(x) = g(x)] - Pr[f(x) β‰  g(x)].

source
theorem Complexity.BooleanAnalysis.inner_eq_one_sub_two_dist {n : β„•} (f g : BooleanFunction n) (hf : IsBooleanValued f) (hg : IsBooleanValued g) :
inner ℝ f g = 1 - 2 * hammingDist f g

Proposition 1.9b: For Boolean-valued f, g, βŸͺf, g⟫ = 1 - 2Β·dist(f, g).

source
theorem Complexity.BooleanAnalysis.expect_eq_fourierCoeff_empty {n : β„•} (f : BooleanFunction n) :
expect f = fourierCoeff f βˆ…

Fact 1.12: The mean of f equals its empty-set Fourier coefficient: 𝔼[f] = 𝓕 f βˆ….

source
theorem Complexity.BooleanAnalysis.variance_eq_sum_fourierCoeff_sq {n : β„•} (f : BooleanFunction n) :
variance f = βˆ‘ S : Finset (Fin n) with S β‰  βˆ…, fourierCoeff f S ^ 2

Proposition 1.13: The variance of f in terms of Fourier coefficients: Var[f] = βˆ‘_{S β‰  βˆ…} (𝓕 f S)Β².

source
theorem Complexity.BooleanAnalysis.variance_boolean {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
variance f = 1 - expect f ^ 2

Fact 1.14: For Boolean-valued f, Var[f] = 1 - 𝔼[f]Β² = 4Β·Pr[f=1]Β·Pr[f=-1] ∈ [0, 1].

source
theorem Complexity.BooleanAnalysis.variance_boolean_prob {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
variance f = (4 * prob fun (x : Cube n) => f x = 1) * prob fun (x : Cube n) => f x = -1

Fact 1.14 (probability form): For Boolean-valued f, Var[f] = 4 Β· Pr[f = 1] Β· Pr[f = -1].

source
theorem Complexity.BooleanAnalysis.variance_boolean_nonneg {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
0 ≀ variance f

Fact 1.14 (lower bound): For Boolean-valued f, 0 ≀ Var[f].

source
theorem Complexity.BooleanAnalysis.variance_boolean_le_one {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
variance f ≀ 1

Fact 1.14 (upper bound): For Boolean-valued f, Var[f] ≀ 1.

source
theorem Complexity.BooleanAnalysis.variance_dist_bounds {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
have Ξ΅ := min (hammingDist f fun (x : Cube n) => 1) (hammingDist f fun (x : Cube n) => -1); 2 * Ξ΅ ≀ variance f ∧ variance f ≀ 4 * Ξ΅

Proposition 1.15: For Boolean-valued f, 2Ξ΅ ≀ Var[f] ≀ 4Ξ΅ where Ξ΅ = min(dist(f, 1), dist(f, -1)).

Here 1 and -1 denote the constant functions.

source
theorem Complexity.BooleanAnalysis.covariance_eq_sum_fourierCoeff {n : β„•} (f g : BooleanFunction n) :
covariance f g = βˆ‘ S : Finset (Fin n) with S β‰  βˆ…, fourierCoeff f S * fourierCoeff g S

Proposition 1.16: The covariance in terms of Fourier coefficients: Cov[f, g] = βˆ‘_{S β‰  βˆ…} (𝓕 f S) Β· (𝓕 g S).

Β§1.4 Spectral sample distribution #

source
noncomputable def Complexity.BooleanAnalysis.spectralSample {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
PMF (Finset (Fin n))

Definition 1.18 (Spectral sample): For Boolean-valued f, the squared Fourier coefficients (𝓕 f S)Β² form a probability distribution on 2^[n], represented as a PMF. By Parseval's theorem, βˆ‘_S (𝓕 f S)Β² = 1.

Equations
Instances For

    Β§1.5 Probability densities and convolution #

    source
    theorem Complexity.BooleanAnalysis.expect_mul_eq_inner {n : β„•} (f g : BooleanFunction n) :
    (expect fun (x : Cube n) => f x * g x) = inner ℝ f g

    Fact 1.21: 𝔼[fΒ·g] = βŸͺf, g⟫ for all f, g.

    The book states this for densities Ο†, interpreting 𝔼_{y ~ Ο†}[g(y)] = βŸͺΟ†, g⟫, but the identity holds for all functions since our inner product is defined as βŸͺf, g⟫ = 𝔼[fΒ·g].

    source
    theorem Complexity.BooleanAnalysis.setDensity_isDensity {n : β„•} (A : Finset (Cube n)) (hA : A.Nonempty) :
    IsDensity (setDensity A)

    Definition 1.22 (Set density is a density): For nonempty A βŠ† 𝔽₂ⁿ, the set density Ο†_A is a valid probability density.

    source
    noncomputable def Complexity.BooleanAnalysis.IsDensity.toPMF {n : ℕ} {φ : BooleanFunction n} (hφ : IsDensity φ) :
    PMF (Cube n)

    Convert a density on 𝔽₂ⁿ to a Mathlib PMF, bridging the book's real-valued density convention with Mathlib's measure-theoretic probability API.

    The book's density satisfies 𝔼[Ο†] = (1/2ⁿ) Β· βˆ‘_x Ο†(x) = 1, so βˆ‘_x Ο†(x) = 2ⁿ. The PMF assigns mass Ο†(x) / 2ⁿ to each x.

    Equations
    Instances For
      source
      theorem Complexity.BooleanAnalysis.setDensity_singleton_zero {n : β„•} (y : Cube n) :
      setDensity {0} y = βˆ‘ S : Finset (Fin n), parityFun S y

      Fact 1.23: Every Fourier coefficient of Ο†_{0} is 1; i.e., Ο†_{0}(y) = βˆ‘_S (Ο‡ S) y.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_setDensity_singleton_zero {n : β„•} (S : Finset (Fin n)) :
      fourierCoeff (setDensity {0}) S = 1

      Fact 1.23 (Fourier coefficient form): Every Fourier coefficient of Ο†_{0} is 1, i.e., 𝓕 Ο†_{0} S = 1 for all S.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_setDensity {n : β„•} (A : Finset (Cube n)) (hA : A.Nonempty) (S : Finset (Fin n)) :
      fourierCoeff (setDensity A) S = 1 / ↑A.card * βˆ‘ x ∈ A, parityFun S x

      Fact 1.23 (general form): The Fourier coefficients of the set density Ο†_A are 𝓕 Ο†_A S = (1/|A|) Β· βˆ‘_{x ∈ A} Ο‡_S(x), i.e., the uniform average of Ο‡_S over A.

      source
      theorem Complexity.BooleanAnalysis.convolution_eq {n : β„•} (f g : BooleanFunction n) (x : Cube n) :
      convolution f g x = expect fun (y : Cube n) => f y * g (x + y)

      Proposition 1.25: (f βŠ› g)(x) = 𝔼_y[f(y)Β·g(x + y)].

      The book states this for densities, but our definition of convolution makes this hold definitionally for all functions.

      source
      theorem Complexity.BooleanAnalysis.convolution_density_isDensity {n : β„•} (Ο† ψ : BooleanFunction n) (hΟ† : IsDensity Ο†) (hψ : IsDensity ψ) :
      IsDensity (convolution Ο† ψ)

      Proposition 1.26: If Ο† and ψ are both densities, then Ο† βŠ› ψ is also a density.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_convolution {n : β„•} (f g : BooleanFunction n) (S : Finset (Fin n)) :
      fourierCoeff (convolution f g) S = fourierCoeff f S * fourierCoeff g S

      Theorem 1.27 (Convolution theorem): 𝓕 (f βŠ› g) S = (𝓕 f S) Β· (𝓕 g S).

      Β§1.6 Linearity characterizations #

      source
      theorem Complexity.BooleanAnalysis.isLinear_iff_isMultiplicative {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
      IsLinear f ↔ IsMultiplicative f

      Definition 1.28 (equivalence): For Boolean-valued f, linearity is equivalent to multiplicativity: f = Ο‡ S for some S iff f(x+y) = f(x)Β·f(y) for all x, y.

      Β§1.6 The BLR test #

      source
      theorem Complexity.BooleanAnalysis.blrAcceptProb_eq {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
      blrAcceptProb f = 1 / 2 + 1 / 2 * βˆ‘ S : Finset (Fin n), fourierCoeff f S ^ 3

      Equation 1.10: The BLR acceptance probability in terms of Fourier coefficients: Pr_{x,y}[f(x)Β·f(y) = f(x+y)] = 1/2 + 1/2 Β· βˆ‘_S (𝓕 f S)Β³.

      source
      theorem Complexity.BooleanAnalysis.blr_completeness {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.blr_soundness {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) (Ξ΅ : ℝ) (hΞ΅ : blrAcceptProb f β‰₯ 1 - Ξ΅) :
      IsCloseToProperty f IsLinear Ξ΅

      Theorem 1.30 (BLR soundness): If the BLR test accepts f with probability 1 - Ξ΅, then f is Ξ΅-close to being linear.

      source
      theorem Complexity.BooleanAnalysis.local_correctability {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 * Ξ΅

      Proposition 1.31 (Local correctability): If f is Ξ΅-close to the linear function Ο‡ S, then for every x, the algorithm "choose y uniformly, output f(y) Β· f(x + y)" outputs (Ο‡ S) x with probability at least 1 - 2Ξ΅.

      source
      theorem Complexity.BooleanAnalysis.degreePart_zero {n : β„•} (f : BooleanFunction n) (x : Cube n) :
      degreePart f 0 x = expect f

      The degree-0 part is the mean. The only coordinate set of size 0 is βˆ…, and Ο‡_βˆ… ≑ 1, so f^{=0} is the constant function 𝔼[f].

      Linearity of the Fourier transform #

      The Fourier coefficient 𝓕 Β· S = βŸͺΒ·, Ο‡ S⟫ is linear in its function argument, inherited directly from linearity of the inner product.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_add {n : β„•} (f g : BooleanFunction n) (S : Finset (Fin n)) :
      fourierCoeff (f + g) S = fourierCoeff f S + fourierCoeff g S

      Fourier coefficients are additive: 𝓕 (f + g) S = 𝓕 f S + 𝓕 g S.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_smul {n : β„•} (c : ℝ) (f : BooleanFunction n) (S : Finset (Fin n)) :
      fourierCoeff (c β€’ f) S = c * fourierCoeff f S

      Fourier coefficients are homogeneous: 𝓕 (c β€’ f) S = c Β· 𝓕 f S.

      source
      @[simp]
      theorem Complexity.BooleanAnalysis.fourierCoeff_zero {n : β„•} (S : Finset (Fin n)) :
      fourierCoeff 0 S = 0

      The zero function has all Fourier coefficients zero.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_neg {n : β„•} (f : BooleanFunction n) (S : Finset (Fin n)) :
      fourierCoeff (-f) S = -fourierCoeff f S

      Fourier coefficients respect negation: 𝓕 (-f) S = -𝓕 f S.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_sub {n : β„•} (f g : BooleanFunction n) (S : Finset (Fin n)) :
      fourierCoeff (f - g) S = fourierCoeff f S - fourierCoeff g S

      Fourier coefficients respect subtraction: 𝓕 (f - g) S = 𝓕 f S - 𝓕 g S.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_ext {n : β„•} {f g : BooleanFunction n} (h : βˆ€ (S : Finset (Fin n)), fourierCoeff f S = fourierCoeff g S) :
      f = g

      Fourier uniqueness. Two functions with identical Fourier coefficients are equal: the difference has zero norm by Parseval. The convenient way to prove a functional identity f = g by checking spectra.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_parityFun {n : β„•} (S T : Finset (Fin n)) :
      fourierCoeff (parityFun S) T = if S = T then 1 else 0

      A parity function is its own indicator in Fourier space. By orthonormality, 𝓕 Ο‡_S T = 1 if T = S and 0 otherwise β€” the parities are exactly the Fourier basis vectors.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_parityFun_mul {n : β„•} (S : Finset (Fin n)) (g : BooleanFunction n) (T : Finset (Fin n)) :
      fourierCoeff (fun (x : Cube n) => parityFun S x * g x) T = fourierCoeff g (symmDiff S T)

      Multiplying by a parity shifts the frequency by symmetric difference: 𝓕(Ο‡_S Β· g, T) = 𝓕(g, S β–³ T). Since Ο‡_S Β· Ο‡_T = Ο‡_{Sβ–³T}, multiplication by a character permutes the Fourier basis, so it relabels every coefficient of g.

      source
      theorem Complexity.BooleanAnalysis.degreePart_add {n : β„•} (f g : BooleanFunction n) (k : β„•) (x : Cube n) :
      degreePart (f + g) k x = degreePart f k x + degreePart g k x

      The degree-k part is additive, inheriting linearity from the Fourier coefficients: (f + g)^{=k} = f^{=k} + g^{=k}.

      source
      theorem Complexity.BooleanAnalysis.degreePart_smul {n : β„•} (c : ℝ) (f : BooleanFunction n) (k : β„•) (x : Cube n) :
      degreePart (c β€’ f) k x = c * degreePart f k x

      The degree-k part is homogeneous: (c β€’ f)^{=k} = c Β· f^{=k}.

      source
      theorem Complexity.BooleanAnalysis.degreePart_sub {n : β„•} (f g : BooleanFunction n) (k : β„•) (x : Cube n) :
      degreePart (f - g) k x = degreePart f k x - degreePart g k x

      The degree-k part respects subtraction: (f - g)^{=k} = f^{=k} - g^{=k}.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_degreePart {n : β„•} (f : BooleanFunction n) (k : β„•) (T : Finset (Fin n)) :
      fourierCoeff (degreePart f k) T = if T.card = k then fourierCoeff f T else 0

      Fourier coefficients of the degree-k projection. The projection f^{=k} keeps exactly the level-k Fourier coefficients and zeroes the rest: 𝓕 f^{=k} T = 𝓕 f T if |T| = k, and 0 otherwise. This is f^{=k}'s defining property as an orthogonal projection onto the degree-k subspace.

      source
      theorem Complexity.BooleanAnalysis.degreePart_inner_eq_zero {n : β„•} (f g : BooleanFunction n) {j k : β„•} (hjk : j β‰  k) :
      inner ℝ (degreePart f j) (degreePart g k) = 0

      Distinct degree parts are orthogonal. For j β‰  k the projections f^{=j} and g^{=k} live in orthogonal Fourier subspaces, so βŸͺf^{=j}, g^{=k}⟫ = 0. This is what makes the degree decomposition f = βˆ‘β‚– f^{=k} an orthogonal decomposition β€” the basis for Parseval-by-degree and degree concentration.

      source
      theorem Complexity.BooleanAnalysis.degreePart_self_inner {n : β„•} (f : BooleanFunction n) (k : β„•) :
      inner ℝ (degreePart f k) (degreePart f k) = fourierWeightAtDegree f k

      The degree-k weight is the squared length of the degree-k part. βŸͺf^{=k}, f^{=k}⟫ = 𝐖 f k = βˆ‘_{|S|=k} (𝓕 f S)Β² β€” Parseval restricted to level k.

      source
      theorem Complexity.BooleanAnalysis.norm_sq_degreePart {n : β„•} (f : BooleanFunction n) (k : β„•) :
      β€–degreePart f kβ€– ^ 2 = fourierWeightAtDegree f k

      The LΒ² norm form of degreePart_self_inner: β€–f^{=k}β€–β‚‚Β² = 𝐖 f k.

      source
      theorem Complexity.BooleanAnalysis.degreePart_parityFun {n : β„•} (S : Finset (Fin n)) (k : β„•) (x : Cube n) :
      degreePart (parityFun S) k x = if S.card = k then parityFun S x else 0

      Parities are homogeneous. The degree-k part of the parity Ο‡_S is Ο‡_S itself when |S| = k, and 0 otherwise β€” Ο‡_S lives entirely in the degree-|S| subspace.

      source
      theorem Complexity.BooleanAnalysis.lowDegreePart_eq_sum {n : β„•} (f : BooleanFunction n) (k : β„•) :
      lowDegreePart f k = βˆ‘ j ∈ Finset.range (k + 1), degreePart f j

      The function-level degree decomposition of the low-degree part: f^{≀k} = βˆ‘_{j≀k} f^{=j} as BooleanFunctions (the pointwise lowDegreePart_eq_sum_degreePart promoted to a function equality).

      source
      theorem Complexity.BooleanAnalysis.lowDegreePart_self_inner {n : β„•} (f : BooleanFunction n) (k : β„•) :
      inner ℝ (lowDegreePart f k) (lowDegreePart f k) = βˆ‘ j ∈ Finset.range (k + 1), fourierWeightAtDegree f j

      Energy of the low-degree part. By orthogonality of the degree parts, the squared length of f^{≀k} is the sum of the low-degree weights: βŸͺf^{≀k}, f^{≀k}⟫ = βˆ‘_{j≀k} 𝐖 f j.

      source
      theorem Complexity.BooleanAnalysis.degree_le {n : β„•} (f : BooleanFunction n) :
      degree f ≀ ↑n

      The degree of an n-bit function is at most n. Every coordinate set has size ≀ n, so the supremum defining deg(f) is bounded by n.

      source
      theorem Complexity.BooleanAnalysis.fourierWeightAtDegree_zero {n : β„•} (f : BooleanFunction n) :
      fourierWeightAtDegree f 0 = fourierCoeff f βˆ… ^ 2

      The degree-0 Fourier weight is the squared mean coefficient: 𝐖 f 0 = (𝓕 f βˆ…)Β² (the only size-0 coordinate set is βˆ…).

      source
      theorem Complexity.BooleanAnalysis.fourierWeightAtDegree_le_self_inner {n : β„•} (f : BooleanFunction n) (k : β„•) :
      fourierWeightAtDegree f k ≀ inner ℝ f f

      Each degree weight is at most the total energy: 𝐖 f k ≀ βŸͺf, f⟫. A trivial but useful spectral concentration bound (one level can hold no more mass than the whole).

      source
      theorem Complexity.BooleanAnalysis.eq_zero_iff_fourierCoeff {n : β„•} (f : BooleanFunction n) :
      f = 0 ↔ βˆ€ (S : Finset (Fin n)), fourierCoeff f S = 0

      Faithfulness of the Fourier transform. A function is zero iff all of its Fourier coefficients vanish β€” the parities separate points, so the transform is injective.

      source
      theorem Complexity.BooleanAnalysis.eq_iff_fourierCoeff {n : β„•} (f g : BooleanFunction n) :
      f = g ↔ βˆ€ (S : Finset (Fin n)), fourierCoeff f S = fourierCoeff g S

      The Fourier transform is injective. Two functions are equal iff they have the same Fourier coefficients at every coordinate set.

      source
      theorem Complexity.BooleanAnalysis.parityFun_injective {n : β„•} :
      Function.Injective fun (S : Finset (Fin n)) => parityFun S

      Distinct coordinate sets give distinct parities. The map S ↦ Ο‡_S is injective, so the parity functions are genuinely 2ⁿ distinct basis vectors.

      source
      theorem Complexity.BooleanAnalysis.isBooleanValued_parityFun {n : β„•} (S : Finset (Fin n)) :
      IsBooleanValued (parityFun S)

      Parity functions are Boolean-valued. Each Ο‡_S(x) is a product of Β±1 values, hence itself Β±1.

      source
      theorem Complexity.BooleanAnalysis.variance_eq_self_inner_sub_fourierWeightAtDegree_zero {n : β„•} (f : BooleanFunction n) :
      variance f = inner ℝ f f - fourierWeightAtDegree f 0

      Variance is the non-constant energy. Var[f] = βŸͺf, f⟫ - 𝐖 f 0: total spectral energy minus the degree-0 (mean) weight. Splits the Parseval sum by removing the βˆ… term.

      source
      theorem Complexity.BooleanAnalysis.variance_eq_sum_fourierWeightAtDegree_pos {n : β„•} (f : BooleanFunction n) :
      variance f = βˆ‘ k ∈ Finset.range n, fourierWeightAtDegree f (k + 1)

      Variance is the weight above degree 0. Var[f] = βˆ‘_{kβ‰₯1} 𝐖 f k β€” the total Fourier weight at all positive degrees.

      source
      theorem Complexity.BooleanAnalysis.variance_nonneg {n : β„•} (f : BooleanFunction n) :
      0 ≀ variance f

      Variance is nonnegative for every real-valued function on the cube (not only Boolean ones): it is a sum of nonnegative Fourier weights.

      source
      theorem Complexity.BooleanAnalysis.fourierWeightAtDegree_le_one {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) (k : β„•) :
      fourierWeightAtDegree f k ≀ 1

      For a Boolean-valued function, each degree weight is at most 1, since the total weight βˆ‘_k 𝐖 f k = βŸͺf, f⟫ = 1.

      source
      theorem Complexity.BooleanAnalysis.fourierCoeff_sq_le_one {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) (S : Finset (Fin n)) :
      fourierCoeff f S ^ 2 ≀ 1

      Every Fourier coefficient of a Boolean-valued function is bounded: (𝓕 f S)Β² ≀ 1, since it is one term of the Parseval sum βˆ‘_T (𝓕 f T)Β² = 1.

      source
      theorem Complexity.BooleanAnalysis.abs_fourierCoeff_le_one {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) (S : Finset (Fin n)) :
      |fourierCoeff f S| ≀ 1

      Every Fourier coefficient of a Boolean-valued function lies in [-1, 1].

      Β§2.4 Noise stability (spectral definition) #

      The noise stability of f at correlation ρ, Stabᡨ[f], measures how much f agrees with itself under ρ-correlated inputs. Here it is defined directly by its spectral formula Stabᡨ[f] = βˆ‘_S ρ^{|S|} 𝓕(f,S)Β² (O'Donnell, Theorem 2.49), which sidesteps the correlated-input distribution while capturing all the first-order facts: at ρ = 1 it is the total Fourier power βŸͺf, f⟫; at ρ = 0 it is the squared mean; and on ρ ∈ [0, 1] it interpolates monotonically between them, bounded by βŸͺf, f⟫ (which is 1 for Boolean f).

      source
      noncomputable def Complexity.BooleanAnalysis.noiseStability {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
      ℝ

      The noise stability of f at correlation ρ, defined spectrally: Stabᡨ[f] = βˆ‘_S ρ^{|S|} Β· 𝓕(f, S)Β².

      Equations
      Instances For
        source
        theorem Complexity.BooleanAnalysis.noiseStability_one {n : β„•} (f : BooleanFunction n) :
        noiseStability 1 f = inner ℝ f f

        At ρ = 1, noise stability is the total Fourier power βŸͺf, f⟫ (Parseval).

        source
        theorem Complexity.BooleanAnalysis.noiseStability_nonneg {n : β„•} {ρ : ℝ} (hρ : 0 ≀ ρ) (f : BooleanFunction n) :
        0 ≀ noiseStability ρ f

        Noise stability is nonnegative for 0 ≀ ρ.

        source
        theorem Complexity.BooleanAnalysis.noiseStability_le_self_inner {n : β„•} {ρ : ℝ} (hρ0 : 0 ≀ ρ) (hρ1 : ρ ≀ 1) (f : BooleanFunction n) :
        noiseStability ρ f ≀ inner ℝ f f

        For ρ ∈ [0, 1], noise stability is bounded above by the total power βŸͺf, f⟫ (each spectral weight is damped by ρ^{|S|} ≀ 1).

        source
        theorem Complexity.BooleanAnalysis.noiseStability_zero {n : β„•} (f : BooleanFunction n) :
        noiseStability 0 f = fourierCoeff f βˆ… ^ 2

        At ρ = 0, only the empty-set term survives: Stabβ‚€[f] = 𝓕(f, βˆ…)Β².

        source
        theorem Complexity.BooleanAnalysis.noiseStability_zero_eq_expect_sq {n : β„•} (f : BooleanFunction n) :
        noiseStability 0 f = expect f ^ 2

        At ρ = 0, noise stability is the squared mean 𝔼[f]Β² (since 𝔼[f] = 𝓕(f, βˆ…)).

        source
        theorem Complexity.BooleanAnalysis.noiseStability_boolean_le_one {n : β„•} {ρ : ℝ} (hρ0 : 0 ≀ ρ) (hρ1 : ρ ≀ 1) (f : BooleanFunction n) (hf : IsBooleanValued f) :
        noiseStability ρ f ≀ 1

        For a Boolean-valued function and ρ ∈ [0, 1], noise stability is at most 1 (its total power is 1).

        source
        theorem Complexity.BooleanAnalysis.sq_expect_le_noiseStability {n : β„•} {ρ : ℝ} (hρ : 0 ≀ ρ) (f : BooleanFunction n) :
        expect f ^ 2 ≀ noiseStability ρ f

        For ρ β‰₯ 0, noise stability is bounded below by the squared mean 𝔼[f]Β² β€” the S = βˆ… term of the spectral sum, which survives with weight ρ⁰ = 1.

        source
        theorem Complexity.BooleanAnalysis.noiseStability_eq_sum_weight {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
        noiseStability ρ f = βˆ‘ k ∈ Finset.range (n + 1), ρ ^ k * fourierWeightAtDegree f k

        Noise stability grouped by degree: Stabᡨ[f] = βˆ‘_k ρ^k Β· 𝐖(f, k). Grouping the spectral sum by |S| = k factors out the common damping ρ^k on each degree, exhibiting Stabᡨ as the ρ-weighted generating function of the Fourier weight distribution.

        source
        noncomputable def Complexity.BooleanAnalysis.noiseOp {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
        BooleanFunction n

        The noise operator T_ρ (a.k.a. the Bonami–Beckner operator), defined spectrally: T_ρ f = βˆ‘_S ρ^{|S|} Β· 𝓕(f, S) Β· Ο‡_S. It damps each frequency by ρ^{|S|}, and is the operator behind noise stability.

        Equations
        Instances For
          source
          theorem Complexity.BooleanAnalysis.fourierCoeff_noiseOp {n : β„•} (ρ : ℝ) (f : BooleanFunction n) (T : Finset (Fin n)) :
          fourierCoeff (noiseOp ρ f) T = ρ ^ T.card * fourierCoeff f T

          Fourier formula for the noise operator: 𝓕(T_ρ f, T) = ρ^{|T|} Β· 𝓕(f, T).

          source
          theorem Complexity.BooleanAnalysis.noiseStability_eq_inner {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
          noiseStability ρ f = inner ℝ f (noiseOp ρ f)

          Noise stability is the correlation of f with its noised copy: Stabᡨ[f] = βŸͺf, T_ρ f⟫ (Plancherel). This is the operator form of the spectral definition.

          source
          theorem Complexity.BooleanAnalysis.noiseOp_one {n : β„•} (f : BooleanFunction n) :
          noiseOp 1 f = f

          At ρ = 1 the noise operator is the identity: T_1 f = f (no frequency is damped).

          source
          theorem Complexity.BooleanAnalysis.noiseOp_zero {n : β„•} (f : BooleanFunction n) :
          noiseOp 0 f = expect f β€’ parityFun βˆ…

          At ρ = 0 the noise operator collapses f to its mean: T_0 f = 𝔼[f] Β· 1 (only the empty frequency, with 0⁰ = 1, survives). This is the constant function 𝔼[f], written as 𝔼[f] β€’ Ο‡_βˆ…. Complements noiseOp_one.

          source
          theorem Complexity.BooleanAnalysis.noiseStability_mono {n : β„•} {ρ₁ ρ₂ : ℝ} (h0 : 0 ≀ ρ₁) (h12 : ρ₁ ≀ ρ₂) (f : BooleanFunction n) :
          noiseStability ρ₁ f ≀ noiseStability ρ₂ f

          Noise stability is monotone in the correlation ρ on ρ β‰₯ 0: more correlation can only increase agreement.

          source
          noncomputable def Complexity.BooleanAnalysis.noiseStabilityBilin {n : β„•} (ρ : ℝ) (f g : BooleanFunction n) :
          ℝ

          The bilinear noise stability of f and g at correlation ρ: Stabᡨ[f, g] = βˆ‘_S ρ^{|S|} Β· 𝓕(f,S) Β· 𝓕(g,S). It specializes to noiseStability on the diagonal and to the inner product at ρ = 1.

          Equations
          Instances For
            source
            theorem Complexity.BooleanAnalysis.noiseStabilityBilin_self {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
            noiseStabilityBilin ρ f f = noiseStability ρ f

            On the diagonal, bilinear noise stability is ordinary noise stability.

            source
            theorem Complexity.BooleanAnalysis.noiseStabilityBilin_symm {n : β„•} (ρ : ℝ) (f g : BooleanFunction n) :
            noiseStabilityBilin ρ f g = noiseStabilityBilin ρ g f

            Bilinear noise stability is symmetric in its two arguments.

            source
            theorem Complexity.BooleanAnalysis.noiseStabilityBilin_one {n : β„•} (f g : BooleanFunction n) :
            noiseStabilityBilin 1 f g = inner ℝ f g

            At ρ = 1, bilinear noise stability is the inner product (Plancherel).

            source
            theorem Complexity.BooleanAnalysis.noiseStabilityBilin_eq_inner {n : β„•} (ρ : ℝ) (f g : BooleanFunction n) :
            noiseStabilityBilin ρ f g = inner ℝ f (noiseOp ρ g)

            Bilinear noise stability is the correlation across the noise operator: Stabᡨ[f, g] = βŸͺf, T_ρ g⟫. Since Stabᡨ is symmetric, this also exhibits T_ρ as self-adjoint: βŸͺf, T_ρ g⟫ = βŸͺT_ρ f, g⟫.

            Hypercontractivity foundations #

            The (2, 4)-hypercontractive inequality β€–T_{1/√3} fβ€–β‚„ ≀ β€–fβ€–β‚‚ is the analytic engine behind the KKL theorem, Friedgut's junta theorem, and the Linial–Mansour–Nisan AC⁰ bound (roadmap L7). Its proof is an induction over coordinates whose base case is the elementary single-bit inequality below; the tensorization step remains.

            source
            theorem Complexity.BooleanAnalysis.two_point_hypercontractive (a b : ℝ) :
            ((a + b / √3) ^ 4 + (a - b / √3) ^ 4) / 2 ≀ (a ^ 2 + b ^ 2) ^ 2

            The two-point (2, 4)-hypercontractive inequality (Bonami's base case). For a single-bit function f(x) = a + bΒ·x on x ∈ {βˆ’1, +1}, the noised function T_{1/√3} f = a + (b/√3)Β·x satisfies 𝔼[(T_{1/√3} f)⁴] ≀ (𝔼[fΒ²])Β² = (aΒ² + bΒ²)Β². The left side is ((a + b/√3)⁴ + (a βˆ’ b/√3)⁴)/2; the slack is 8b⁴/9 β‰₯ 0.

            Β§2.3 Total influence (average sensitivity, spectral form) #

            The total influence I[f] (a.k.a. average sensitivity) measures how sensitive f is to single-coordinate flips. Its spectral formula (O'Donnell, Theorem 2.38) weights each Fourier level by its degree: I[f] = βˆ‘_S |S| Β· 𝓕(f,S)Β². Grouped by degree it is βˆ‘_k k Β· 𝐖(f,k), and it is bounded by n Β· βŸͺf, f⟫ (so by n for Boolean f) β€” the fact that a function on n bits has average sensitivity at most n.

            source
            noncomputable def Complexity.BooleanAnalysis.totalInfluence {n : β„•} (f : BooleanFunction n) :
            ℝ

            The total influence of f, spectral form: I[f] = βˆ‘_S |S| Β· 𝓕(f, S)Β².

            Equations
            Instances For
              source
              theorem Complexity.BooleanAnalysis.totalInfluence_nonneg {n : β„•} (f : BooleanFunction n) :
              0 ≀ totalInfluence f

              Total influence is nonnegative.

              source
              theorem Complexity.BooleanAnalysis.totalInfluence_eq_sum_weight {n : β„•} (f : BooleanFunction n) :
              totalInfluence f = βˆ‘ k ∈ Finset.range (n + 1), ↑k * fourierWeightAtDegree f k

              Total influence grouped by degree: I[f] = βˆ‘_k k Β· 𝐖(f, k).

              source
              theorem Complexity.BooleanAnalysis.totalInfluence_le {n : β„•} (f : BooleanFunction n) :
              totalInfluence f ≀ ↑n * inner ℝ f f

              Total influence is bounded by n Β· βŸͺf, f⟫ (each degree is at most n).

              source
              theorem Complexity.BooleanAnalysis.totalInfluence_boolean_le {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
              totalInfluence f ≀ ↑n

              For a Boolean-valued function, total influence is at most n (its total power is 1).

              source
              theorem Complexity.BooleanAnalysis.totalInfluence_le_of_degree {n : β„•} (f : BooleanFunction n) (d : β„•) (hd : βˆ€ (S : Finset (Fin n)), d < S.card β†’ fourierCoeff f S = 0) :
              totalInfluence f ≀ ↑d * inner ℝ f f

              Low-degree functions have small total influence. If f has degree at most d (all Fourier coefficients on sets larger than d vanish), then I[f] ≀ d Β· βŸͺf, f⟫.

              source
              theorem Complexity.BooleanAnalysis.totalInfluence_boolean_le_of_degree {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) (d : β„•) (hd : βˆ€ (S : Finset (Fin n)), d < S.card β†’ fourierCoeff f S = 0) :
              totalInfluence f ≀ ↑d

              For a Boolean-valued function of degree at most d, total influence is at most d.

              source
              noncomputable def Complexity.BooleanAnalysis.influence {n : β„•} (i : Fin n) (f : BooleanFunction n) :
              ℝ

              The influence of coordinate i on f, spectral form: the Fourier weight carried by sets containing i, Infα΅’[f] = βˆ‘_{S βˆ‹ i} 𝓕(f, S)Β².

              Equations
              Instances For
                source
                theorem Complexity.BooleanAnalysis.influence_nonneg {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                0 ≀ influence i f

                Coordinate influence is nonnegative.

                source
                theorem Complexity.BooleanAnalysis.totalInfluence_eq_sum_influence {n : β„•} (f : BooleanFunction n) :
                totalInfluence f = βˆ‘ i : Fin n, influence i f

                Total influence is the sum of the coordinate influences: I[f] = βˆ‘_i Infα΅’[f]. Each set S contributes its weight 𝓕(f,S)Β² once for every coordinate it contains, i.e. |S| times β€” swapping the order of summation turns the degree weighting into a sum over coordinates.

                source
                theorem Complexity.BooleanAnalysis.influence_le_totalInfluence {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                influence i f ≀ totalInfluence f

                Each coordinate influence is at most the total influence.

                source
                theorem Complexity.BooleanAnalysis.influence_le_self_inner {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                influence i f ≀ inner ℝ f f

                A coordinate's influence is at most the total power βŸͺf, f⟫.

                source
                theorem Complexity.BooleanAnalysis.influence_boolean_le_one {n : β„•} (i : Fin n) (f : BooleanFunction n) (hf : IsBooleanValued f) :
                influence i f ≀ 1

                For a Boolean-valued function, every coordinate influence is at most 1.

                source
                theorem Complexity.BooleanAnalysis.totalInfluence_parityFun {n : β„•} (S : Finset (Fin n)) :
                totalInfluence (parityFun S) = ↑S.card

                Average sensitivity of a parity. The parity Ο‡_S has total influence exactly |S|: each of its |S| relevant coordinates is fully influential (a concrete check of the average-sensitivity theory on the Fourier basis).

                source
                theorem Complexity.BooleanAnalysis.influence_parityFun {n : β„•} (i : Fin n) (S : Finset (Fin n)) :
                influence i (parityFun S) = if i ∈ S then 1 else 0

                Coordinate influence of a parity. Coordinate i influences Ο‡_S fully when i ∈ S, and not at all otherwise.

                source
                theorem Complexity.BooleanAnalysis.fourierCoeff_singleton_sq_le_influence {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                fourierCoeff f {i} ^ 2 ≀ influence i f

                The squared degree-1 coefficient at i is a lower bound for the influence of i: 𝓕(f, {i})Β² ≀ Infα΅’[f]. It is the S = {i} term of the spectral sum defining the influence, and all other terms are nonnegative.

                source
                theorem Complexity.BooleanAnalysis.fourierWeightAtDegree_one_le_totalInfluence {n : β„•} (f : BooleanFunction n) :
                fourierWeightAtDegree f 1 ≀ totalInfluence f

                Degree-1 weight is bounded by total influence: WΒΉ[f] ≀ I[f]. Each degree-1 frequency contributes its weight once to WΒΉ but |S| = 1 times (i.e. also once) to I, and higher-degree frequencies only add to I.

                source
                theorem Complexity.BooleanAnalysis.sum_fourierCoeff_singleton_sq_le_totalInfluence {n : β„•} (f : BooleanFunction n) :
                βˆ‘ i : Fin n, fourierCoeff f {i} ^ 2 ≀ totalInfluence f

                Level-1 inequality (coordinate form). The total weight on the degree-1 coefficients is at most the total influence: βˆ‘_i 𝓕(f, {i})Β² ≀ I[f]. Immediate by summing fourierCoeff_singleton_sq_le_influence over the coordinates.

                source
                theorem Complexity.BooleanAnalysis.sum_fourierCoeff_singleton_sq_eq_fourierWeightAtDegree_one {n : β„•} (f : BooleanFunction n) :
                βˆ‘ i : Fin n, fourierCoeff f {i} ^ 2 = fourierWeightAtDegree f 1

                The coordinate sum of squared degree-1 coefficients is the degree-1 weight: βˆ‘_i 𝓕(f, {i})Β² = WΒΉ[f]. The singletons {i} are exactly the cardinality-1 frequencies, so the coordinate sum and the degree-1 weight coincide.

                source
                def Complexity.BooleanAnalysis.flipCoord {n : β„•} (i : Fin n) (x : Cube n) :
                Cube n

                Flip coordinate i of a point of the Hamming cube.

                Equations
                Instances For
                  source
                  theorem Complexity.BooleanAnalysis.chi_add_one (b : ZMod 2) :
                  chi (b + 1) = -chi b

                  The character Ο‡ negates under a bit flip: Ο‡(b + 1) = -Ο‡(b).

                  source
                  theorem Complexity.BooleanAnalysis.parityFun_flipCoord {n : β„•} (i : Fin n) (S : Finset (Fin n)) (x : Cube n) :
                  parityFun S (flipCoord i x) = (if i ∈ S then -1 else 1) * parityFun S x

                  A parity under a coordinate flip. Ο‡_S flips sign exactly when the flipped coordinate is one of its inputs: Ο‡_S(x with coordinate i flipped) = (βˆ’1)^{[i∈S]} Β· Ο‡_S(x). This is the key step toward reading coordinate influence as the probability that f is sensitive at i.

                  source
                  theorem Complexity.BooleanAnalysis.flipCoord_flipCoord {n : β„•} (i : Fin n) (x : Cube n) :
                  flipCoord i (flipCoord i x) = x

                  Flipping coordinate i twice is the identity (ZMod 2 has characteristic two).

                  source
                  def Complexity.BooleanAnalysis.flipEquiv {n : β„•} (i : Fin n) :
                  Cube n ≃ Cube n

                  Flipping coordinate i is an involutive equivalence of the Hamming cube.

                  Equations
                  Instances For
                    source
                    theorem Complexity.BooleanAnalysis.expect_flipCoord {n : β„•} (i : Fin n) (g : Cube n β†’ ℝ) :
                    (expect fun (x : Cube n) => g (flipCoord i x)) = expect g

                    The uniform expectation is invariant under a coordinate flip: flipCoord i is a measure-preserving bijection of the cube.

                    source
                    theorem Complexity.BooleanAnalysis.fourierCoeff_comp_flipCoord {n : β„•} (i : Fin n) (f : BooleanFunction n) (T : Finset (Fin n)) :
                    fourierCoeff (fun (x : Cube n) => f (flipCoord i x)) T = (if i ∈ T then -1 else 1) * fourierCoeff f T

                    Fourier coefficient of f precomposed with a coordinate flip. Flipping coordinate i negates exactly the frequencies containing i: 𝓕(f ∘ flipα΅’, T) = (βˆ’1)^[i∈T] Β· 𝓕(f, T).

                    source
                    noncomputable def Complexity.BooleanAnalysis.derivative {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                    BooleanFunction n

                    The discrete derivative D_i f of f in the direction of coordinate i, defined spectrally: D_i f = βˆ‘_{S βˆ‹ i} 𝓕(f, S) Β· Ο‡_{Sβˆ–{i}}. It strips coordinate i from every frequency that contains it.

                    Equations
                    Instances For
                      source
                      theorem Complexity.BooleanAnalysis.fourierCoeff_derivative {n : β„•} (i : Fin n) (f : BooleanFunction n) (T : Finset (Fin n)) :
                      fourierCoeff (derivative i f) T = if i ∈ T then 0 else fourierCoeff f (insert i T)

                      Fourier formula for the derivative: 𝓕(D_i f, T) = 𝓕(f, T βˆͺ {i}) when i βˆ‰ T, and 0 when i ∈ T.

                      source
                      theorem Complexity.BooleanAnalysis.influence_eq_norm_sq_derivative {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                      influence i f = β€–derivative i fβ€– ^ 2

                      Influence is the squared norm of the derivative: Infα΅’[f] = β€–D_i fβ€–Β². This is the analytic form of coordinate influence β€” the standard bridge to the combinatorial "probability f is sensitive at i" (O'Donnell Β§2.2).

                      source
                      noncomputable def Complexity.BooleanAnalysis.sensitivityOp {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                      BooleanFunction n

                      The sensitivity operator Lα΅’ f at coordinate i, the point-value analogue of the derivative: (Lα΅’ f)(x) = (f(x) βˆ’ f(x βŠ• eα΅’)) / 2. It vanishes exactly where f is insensitive to coordinate i, and equals Β±1 where flipping i flips f.

                      Equations
                      Instances For
                        source
                        theorem Complexity.BooleanAnalysis.fourierCoeff_sensitivityOp {n : β„•} (i : Fin n) (f : BooleanFunction n) (T : Finset (Fin n)) :
                        fourierCoeff (sensitivityOp i f) T = if i ∈ T then fourierCoeff f T else 0

                        Fourier formula for the sensitivity operator: Lα΅’ keeps the frequencies containing i and kills the rest β€” 𝓕(Lα΅’ f, T) = 𝓕(f, T) if i ∈ T, else 0. (Contrast the derivative Dα΅’, which additionally strips i from each frequency.)

                        source
                        theorem Complexity.BooleanAnalysis.influence_eq_norm_sq_sensitivityOp {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                        influence i f = β€–sensitivityOp i fβ€– ^ 2

                        Influence is the squared norm of the sensitivity operator: Infα΅’[f] = β€–Lα΅’ fβ€–Β². A second analytic form of coordinate influence, complementing influence_eq_norm_sq_derivative.

                        source
                        theorem Complexity.BooleanAnalysis.sensitivityOp_eq_parityFun_mul_derivative {n : β„•} (i : Fin n) (f : BooleanFunction n) :
                        sensitivityOp i f = fun (x : Cube n) => parityFun {i} x * derivative i f x

                        The sensitivity operator is the parity-twisted derivative: Lα΅’ f = Ο‡_{i} Β· Dα΅’ f. Both strip coordinate i from the surviving frequencies, but Lα΅’ twists each back by Ο‡_{i}; since |Ο‡_{i}| = 1 this is why β€–Lα΅’ fβ€– = β€–Dα΅’ fβ€– and the two influence formulas agree.

                        source
                        theorem Complexity.BooleanAnalysis.influence_boolean_eq_expect_sensitive {n : β„•} (i : Fin n) (f : BooleanFunction n) (hf : IsBooleanValued f) :
                        influence i f = expect fun (x : Cube n) => if f x β‰  f (flipCoord i x) then 1 else 0

                        Average sensitivity as a probability. For a Boolean-valued f, the influence of coordinate i is the probability that flipping i flips the output: Infα΅’[f] = Pr_x[f(x) β‰  f(x βŠ• eα΅’)] (O'Donnell Β§2.2). Summed over i, this reads total influence as the expected number of pivotal coordinates β€” the combinatorial meaning of "average sensitivity".

                        source
                        theorem Complexity.BooleanAnalysis.totalInfluence_boolean_eq_expect_sensitive {n : β„•} (f : BooleanFunction n) (hf : IsBooleanValued f) :
                        totalInfluence f = expect fun (x : Cube n) => βˆ‘ i : Fin n, if f x β‰  f (flipCoord i x) then 1 else 0

                        Total influence is the expected number of pivotal coordinates. For a Boolean-valued f, summing the per-coordinate sensitivity probabilities over all coordinates gives I[f] = 𝔼ₓ[#{i : f(x) β‰  f(x βŠ• eα΅’)}] β€” the literal meaning of "average sensitivity" (average, over a uniform input, of the number of coordinates whose flip changes the output).

                        source
                        theorem Complexity.BooleanAnalysis.noiseStability_one_sub_le {n : β„•} {ρ : ℝ} (h0 : 0 ≀ ρ) (h1 : ρ ≀ 1) (f : BooleanFunction n) :
                        inner ℝ f f - noiseStability ρ f ≀ (1 - ρ) * totalInfluence f

                        Stability decay is controlled by total influence. For ρ ∈ [0, 1], the loss of noise stability relative to the full power βŸͺf, f⟫ is at most (1 - ρ) times the total influence: βŸͺf, f⟫ - Stabᡨ[f] ≀ (1 - ρ) Β· I[f]. This is the spectral form of the standard bound NS_Ξ΄[f] ≀ Ξ΄ Β· I[f] on noise sensitivity.

                        source
                        theorem Complexity.BooleanAnalysis.variance_le_totalInfluence {n : β„•} (f : BooleanFunction n) :
                        variance f ≀ totalInfluence f

                        The PoincarΓ© inequality: the variance of f is at most its total influence, Var[f] ≀ I[f]. Spectrally, Var[f] = βˆ‘_{S β‰  βˆ…} 𝓕(f,S)Β² while I[f] = βˆ‘_S |S| 𝓕(f,S)Β², and each nonempty S has |S| β‰₯ 1, so influence dominates variance term by term.

                        source
                        noncomputable def Complexity.BooleanAnalysis.noiseSensitivity {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
                        ℝ

                        The noise sensitivity of f at correlation ρ, defined from noise stability as NSᡨ[f] = (βŸͺf, f⟫ - Stabᡨ[f]) / 2 β€” the amount of Fourier power lost to the ρ-damping, i.e. the propensity of f to disagree with itself under noise.

                        Equations
                        Instances For
                          source
                          theorem Complexity.BooleanAnalysis.noiseSensitivity_nonneg {n : β„•} {ρ : ℝ} (hρ0 : 0 ≀ ρ) (hρ1 : ρ ≀ 1) (f : BooleanFunction n) :
                          0 ≀ noiseSensitivity ρ f

                          Noise sensitivity is nonnegative for ρ ∈ [0, 1].

                          source
                          theorem Complexity.BooleanAnalysis.noiseSensitivity_one {n : β„•} (f : BooleanFunction n) :
                          noiseSensitivity 1 f = 0

                          At full correlation ρ = 1, noise sensitivity vanishes.

                          source
                          theorem Complexity.BooleanAnalysis.noiseSensitivity_le_influence {n : β„•} {ρ : ℝ} (hρ0 : 0 ≀ ρ) (hρ1 : ρ ≀ 1) (f : BooleanFunction n) :
                          noiseSensitivity ρ f ≀ (1 - ρ) / 2 * totalInfluence f

                          Noise sensitivity is controlled by total influence: NSᡨ[f] ≀ (1-ρ)/2 Β· I[f] (the spectral form of NS_Ξ΄[f] ≀ Ξ΄ Β· I[f]).

                          source
                          theorem Complexity.BooleanAnalysis.noiseStability_add_two_noiseSensitivity {n : β„•} (ρ : ℝ) (f : BooleanFunction n) :
                          noiseStability ρ f + 2 * noiseSensitivity ρ f = inner ℝ f f

                          Stability–sensitivity decomposition: Stabᡨ[f] + 2Β·NSᡨ[f] = βŸͺf, f⟫. The total Fourier power splits into the retained (stability) and lost (twice sensitivity) parts.

                          source
                          theorem Complexity.BooleanAnalysis.noiseSensitivity_antitone {n : β„•} {ρ₁ ρ₂ : ℝ} (h0 : 0 ≀ ρ₁) (h12 : ρ₁ ≀ ρ₂) (f : BooleanFunction n) :
                          noiseSensitivity ρ₂ f ≀ noiseSensitivity ρ₁ f

                          Noise sensitivity is antitone in the correlation ρ (more correlation, less disagreement) β€” dual to the monotonicity of noise stability.