Chapter 1: Boolean functions and the Fourier expansion — Definitions

This file contains the core definitions for Fourier analysis of Boolean functions following Chapter 1 of "Analysis of Boolean Functions" by Ryan O'Donnell.

We work with the Hamming cube modeled as Fin n → ZMod 2, with the encoding χ : ZMod 2 → ℝ sending 0 ↦ 1 and 1 ↦ -1. This corresponds to the book's convention of representing the cube as {-1, 1}^n via the map b ↦ (-1)^b.

The space BooleanFunction n of real-valued functions on the Boolean cube carries the uniform-measure L² inner product ⟪f, g⟫ = 𝔼[f·g] = (1/2ⁿ) · ∑_x f(x)·g(x) (Definition 1.3), realized as a Mathlib InnerProductSpace ℝ. The def (rather than abbrev) for BooleanFunction blocks typeclass resolution from seeing through to Cube n → ℝ, avoiding a norm diamond with Mathlib's Pi-type sup norm.

Notation

Within the BooleanAnalysis namespace, we provide notation that mirrors the book's conventions:

• 𝔼[f] — uniform expectation over the Hamming cube
• ⟪f, g⟫ — inner product 𝔼[f·g] (Mathlib's inner on BooleanFunction n)
• ‖f‖₂ — L² norm √⟪f, f⟫ (Mathlib's norm on BooleanFunction n)
• χ S — parity function on set S
• 𝓕 f S — Fourier coefficient of f on S
• 𝐖 f k — Fourier weight of f at degree k
• Var[f] — variance of f
• Cov[f, g] — covariance of f and g
• f ⊛ g — convolution
• 𝟙 P — indicator function of predicate P
• Pr[P] — uniform probability 𝔼[𝟙 P]
• Pr₂[P] — joint uniform probability over pairs

Basic types

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.Cube (n : ℕ) : Type

The Hamming cube 𝔽₂ⁿ is Fin n → ZMod 2.

Equations

• Complexity.BooleanAnalysis.Cube n = (Fin n → ZMod 2)

def Complexity.BooleanAnalysis.BooleanFunction (n : ℕ) : Type

BooleanFunction n is the space of real-valued functions on the Boolean cube 𝔽₂ⁿ, equipped with the uniform-measure L² inner product ⟪f, g⟫ = 𝔼[f·g] (Definition 1.3 in O'Donnell).

The def (rather than abbrev) blocks typeclass resolution from seeing through to Cube n → ℝ, preventing a norm diamond with Mathlib's Pi-type sup norm while still allowing the kernel to see through for type checking.

Equations

• Complexity.BooleanAnalysis.BooleanFunction n = (Complexity.BooleanAnalysis.Cube n → ℝ)

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instCommRing {n : ℕ} : CommRing (BooleanFunction n)

Equations

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

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instModuleReal {n : ℕ} : Module ℝ (BooleanFunction n)

Equations

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

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instAlgebraReal {n : ℕ} : Algebra ℝ (BooleanFunction n)

Equations

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

@[instance_reducible]

instance Complexity.BooleanAnalysis.BooleanFunction.instInhabited {n : ℕ} : Inhabited (BooleanFunction n)

Equations

• Complexity.BooleanAnalysis.BooleanFunction.instInhabited = { default := Complexity.BooleanAnalysis.BooleanFunction.instInhabited._aux_1 }

@[instance_reducible]

instance Complexity.BooleanAnalysis.BooleanFunction.instFunLikeCubeReal {n : ℕ} : FunLike (BooleanFunction n) (Cube n) ℝ

Equations

• Complexity.BooleanAnalysis.BooleanFunction.instFunLikeCubeReal = { coe := fun (f : Complexity.BooleanAnalysis.BooleanFunction n) => f, coe_injective := ⋯ }

theorem Complexity.BooleanAnalysis.BooleanFunction.ext {n : ℕ} {f g : BooleanFunction n} (h : ∀ (x : Cube n), f x = g x) : f = g

theorem Complexity.BooleanAnalysis.BooleanFunction.ext_iff {n : ℕ} {f g : BooleanFunction n} : f = g ↔ ∀ (x : Cube n), f x = g x

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.zero_apply {n : ℕ} (x : Cube n) : 0 x = 0

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.add_apply {n : ℕ} (f g : BooleanFunction n) (x : Cube n) : (f + g) x = f x + g x

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.neg_apply {n : ℕ} (f : BooleanFunction n) (x : Cube n) : (-f) x = -f x

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.sub_apply {n : ℕ} (f g : BooleanFunction n) (x : Cube n) : (f - g) x = f x - g x

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.smul_apply {n : ℕ} (r : ℝ) (f : BooleanFunction n) (x : Cube n) : (r • f) x = r * f x

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.mul_apply {n : ℕ} (f g : BooleanFunction n) (x : Cube n) : (f * g) x = f x * g x

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.one_apply {n : ℕ} (x : Cube n) : 1 x = 1

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.sum_apply {n : ℕ} {ι : Type u_1} (s : Finset ι) (g : ι → BooleanFunction n) (x : Cube n) : (∑ i ∈ s, g i) x = ∑ i ∈ s, g i x

Evaluate a Finset sum of BooleanFunctions pointwise.

def Complexity.BooleanAnalysis.BooleanFunction.ofFun {n : ℕ} (f : Cube n → ℝ) : BooleanFunction n

Coerce a plain function Cube n → ℝ to BooleanFunction n.

Equations

• Complexity.BooleanAnalysis.BooleanFunction.ofFun f = f

def Complexity.BooleanAnalysis.BooleanFunction.toFun {n : ℕ} (f : BooleanFunction n) : Cube n → ℝ

Extract the underlying function from a BooleanFunction.

Equations

• f.toFun = f

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.toFun_ofFun {n : ℕ} (f : Cube n → ℝ) : (ofFun f).toFun = f

@[simp]

theorem Complexity.BooleanAnalysis.BooleanFunction.ofFun_toFun {n : ℕ} (f : BooleanFunction n) : ofFun f.toFun = f

Inner product space structure

The inner product on BooleanFunction n is the uniform-measure inner product ⟪f, g⟫ = (1/2ⁿ) · ∑_x f(x)·g(x), matching O'Donnell's Definition 1.3. This is the expectation 𝔼[f·g] under the uniform distribution on 𝔽₂ⁿ.

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instInner {n : ℕ} : Inner ℝ (BooleanFunction n)

The uniform-measure inner product: ⟪f, g⟫ = (1/2ⁿ) · ∑_x f(x)·g(x).

Equations

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

theorem Complexity.BooleanAnalysis.BooleanFunction.inner_def {n : ℕ} (f g : BooleanFunction n) : inner ℝ f g = 1 / 2 ^ n * ∑ x : Cube n, f x * g x

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instCore {n : ℕ} : PreInnerProductSpace.Core ℝ (BooleanFunction n)

Equations

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

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instFullCore {n : ℕ} : InnerProductSpace.Core ℝ (BooleanFunction n)

Equations

• Complexity.BooleanAnalysis.BooleanFunction.instFullCore = { toCore := Complexity.BooleanAnalysis.BooleanFunction.instCore, definite := ⋯ }

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.instNormedAddCommGroup {n : ℕ} : NormedAddCommGroup (BooleanFunction n)

Equations

• Complexity.BooleanAnalysis.BooleanFunction.instNormedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance Complexity.BooleanAnalysis.BooleanFunction.innerProductSpace {n : ℕ} : InnerProductSpace ℝ (BooleanFunction n)

Equations

• Complexity.BooleanAnalysis.BooleanFunction.innerProductSpace = InnerProductSpace.ofCore Complexity.BooleanAnalysis.BooleanFunction.instCore

Notation

The book uses ⟪f, g⟫ for the inner product (Definition 1.3) and ‖f‖₂ for the L² norm (§1.3, page 24). These map to Mathlib's inner and norm on BooleanFunction n.

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

⟪f, g⟫ — the inner product 𝔼[f·g] on BooleanFunction n (Definition 1.3).

Equations

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

def Complexity.BooleanAnalysis.«term‖_‖₂» : Lean.ParserDescr

‖f‖₂ — the L² norm √⟪f, f⟫ on BooleanFunction n (§1.3, page 24).

This equals Mathlib's ‖f‖ since the InnerProductSpace instance makes norm the L² norm. We use the subscript to match the book's convention and to distinguish from other norms that may appear in later chapters.

Equations

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

theorem Complexity.BooleanAnalysis.inner_def {n : ℕ} (f g : BooleanFunction n) : inner ℝ f g = 1 / 2 ^ n * ∑ x : Cube n, f x * g x

⟪f, g⟫ = (1/2ⁿ) · ∑_x f(x)·g(x) — unfold the inner product to the explicit sum form.

§1.2 The encoding and parity functions

def Complexity.BooleanAnalysis.IsBooleanValued {n : ℕ} (f : BooleanFunction n) : Prop

A function f : 𝔽₂ⁿ → ℝ is Boolean-valued if its range is {-1, 1}. In the ±1 encoding, this means f(x) = ±1 for all x.

Equations

• Complexity.BooleanAnalysis.IsBooleanValued f = ∀ (x : Complexity.BooleanAnalysis.Cube n), f x = 1 ∨ f x = -1

def Complexity.BooleanAnalysis.chi : ZMod 2 → ℝ

The encoding χ : ZMod 2 → ℝ defined by χ(b) = (-1)^b. Concretely, χ(0) = 1 and χ(1) = -1. (Book §1.2)

Equations

• Complexity.BooleanAnalysis.chi b = if b = 0 then 1 else -1

noncomputable def Complexity.BooleanAnalysis.parityFun {n : ℕ} (S : Finset (Fin n)) : BooleanFunction n

The parity function χ S : 𝔽₂ⁿ → ℝ for S ⊆ [n], defined by (χ S)(x) = ∏_{i ∈ S} χ(xᵢ) = (-1)^(∑_{i ∈ S} xᵢ). (Definition 1.2)

Equations

• Complexity.BooleanAnalysis.parityFun S x = ∏ i ∈ S, Complexity.BooleanAnalysis.chi (x i)

def Complexity.BooleanAnalysis.termχ_ : Lean.ParserDescr

χ S — the parity function on the coordinate set S.

Equations

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

§1.3–1.4 Expectation, Fourier coefficients

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

The uniform expectation 𝔼[f] = 2⁻ⁿ · ∑_x f(x).

Equations

• Complexity.BooleanAnalysis.expect f = Finset.univ.expect f

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

𝔼[f] — the uniform expectation of f over the Hamming cube.

Equations

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

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

The Fourier coefficient 𝓕 f S = ⟪f, χ S⟫. (Proposition 1.8 / our definition)

Equations

• Complexity.BooleanAnalysis.fourierCoeff f S = inner ℝ f (Complexity.BooleanAnalysis.parityFun S)

def Complexity.BooleanAnalysis.term𝓕 : Lean.ParserDescr

𝓕 f S — the Fourier coefficient of f on the coordinate set S.

Equations

• Complexity.BooleanAnalysis.term𝓕 = Lean.ParserDescr.node `Complexity.BooleanAnalysis.term𝓕 1024 (Lean.ParserDescr.symbol "𝓕")

Bridge lemmas

theorem Complexity.BooleanAnalysis.expect_unfold {n : ℕ} (f : BooleanFunction n) : expect f = 1 / 2 ^ n * ∑ x : Cube n, f x

Unfold 𝔼[f] to the explicit sum form 1/2^n · ∑_x f(x).

theorem Complexity.BooleanAnalysis.inner_eq_expect {n : ℕ} (f g : BooleanFunction n) : inner ℝ f g = expect fun (x : Cube n) => f x * g x

The inner product equals the expectation of the product. This is the book's Definition 1.3: ⟪f, g⟫ = 𝔼[f·g].

§1.4 Mean, variance, covariance

def Complexity.BooleanAnalysis.IsUnbiased {n : ℕ} (f : BooleanFunction n) : Prop

A function f : 𝔽₂ⁿ → ℝ is unbiased (or balanced) if 𝔼[f] = 0. (Definition 1.11)

Equations

• Complexity.BooleanAnalysis.IsUnbiased f = (Complexity.BooleanAnalysis.expect f = 0)

noncomputable def Complexity.BooleanAnalysis.variance {n : ℕ} (f : BooleanFunction n) : ℝ

The variance of f : 𝔽₂ⁿ → ℝ, defined as Var[f] = 𝔼[f²] - 𝔼[f]². (Proposition 1.13)

Equations

• Complexity.BooleanAnalysis.variance f = (Complexity.BooleanAnalysis.expect fun (x : Complexity.BooleanAnalysis.Cube n) => f x ^ 2) - Complexity.BooleanAnalysis.expect f ^ 2

def Complexity.BooleanAnalysis.«termVar[_]» : Lean.ParserDescr

Var[f] — the variance of f.

Equations

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

noncomputable def Complexity.BooleanAnalysis.covariance {n : ℕ} (f g : BooleanFunction n) : ℝ

The covariance of f, g : 𝔽₂ⁿ → ℝ, defined as Cov[f, g] = 𝔼[f·g] - 𝔼[f]·𝔼[g]. (Proposition 1.16)

Equations

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

def Complexity.BooleanAnalysis.«termCov[_,_]» : Lean.ParserDescr

Cov[f, g] — the covariance of f and g.

Equations

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

noncomputable def Complexity.BooleanAnalysis.indicator {n : ℕ} (P : Cube n → Prop) : BooleanFunction n

The 0-1 indicator function of a predicate P on 𝔽₂ⁿ. (𝟙 P)(x) = 1 if P x, else 0.

The book (Definition 1.22) defines 𝟙_A for a set A ⊆ 𝔽₂ⁿ. We generalize to predicates so that probability expressions like Pr_x[P(x)] = 𝔼[𝟙 P] read cleanly without Finset.univ.filter boilerplate. For the set version, use 𝟙 (· ∈ A).

Equations

• Complexity.BooleanAnalysis.indicator P x = if P x then 1 else 0

def Complexity.BooleanAnalysis.«term𝟙_» : Lean.ParserDescr

𝟙 P — the 0-1 indicator function of predicate P.

Equations

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

noncomputable def Complexity.BooleanAnalysis.prob {n : ℕ} (P : Cube n → Prop) : ℝ

The uniform probability Pr_x[P(x)] = 𝔼[𝟙 P].

Equations

• Complexity.BooleanAnalysis.prob P = Complexity.BooleanAnalysis.expect (Complexity.BooleanAnalysis.indicator P)

def Complexity.BooleanAnalysis.«termPr[_]» : Lean.ParserDescr

Pr[P] — the uniform probability of predicate P.

Equations

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

noncomputable def Complexity.BooleanAnalysis.prob₂ {n : ℕ} (P : Cube n → Cube n → Prop) : ℝ

The joint uniform probability Pr_{x,y}[P(x,y)] = 𝔼_x[𝔼_y[𝟙 (P x)]]. Equivalent to the uniform probability over the product space by Fubini.

Equations

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

def Complexity.BooleanAnalysis.«termPr₂[_]» : Lean.ParserDescr

Pr₂[P] — the joint uniform probability of P over pairs.

Equations

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

noncomputable def Complexity.BooleanAnalysis.hammingDist {n : ℕ} (f g : BooleanFunction n) : ℝ

The relative Hamming distance between functions f and g, dist(f, g) = Pr_x[f(x) ≠ g(x)]. (Definition 1.10)

Equations

• Complexity.BooleanAnalysis.hammingDist f g = Complexity.BooleanAnalysis.prob fun (x : Complexity.BooleanAnalysis.Cube n) => f x ≠ g x

§1.4 Fourier weight distribution

noncomputable def Complexity.BooleanAnalysis.fourierWeight {n : ℕ} (f : BooleanFunction n) (S : Finset (Fin n)) : ℝ

The Fourier weight of f on set S, defined as (𝓕 f S)². (Definition 1.17)

Equations

• Complexity.BooleanAnalysis.fourierWeight f S = Complexity.BooleanAnalysis.fourierCoeff f S ^ 2

noncomputable def Complexity.BooleanAnalysis.fourierWeightAtDegree {n : ℕ} (f : BooleanFunction n) (k : ℕ) : ℝ

The Fourier weight of f at degree k: 𝐖 f k = ∑_{|S|=k} (𝓕 f S)². (Definition 1.19)

Equations

• Complexity.BooleanAnalysis.fourierWeightAtDegree f k = ∑ S : Finset (Fin n) with S.card = k, Complexity.BooleanAnalysis.fourierWeight f S

def Complexity.BooleanAnalysis.«term𝐖» : Lean.ParserDescr

𝐖 f k — the Fourier weight of f at degree k.

Equations

• Complexity.BooleanAnalysis.«term𝐖» = Lean.ParserDescr.node `Complexity.BooleanAnalysis.«term𝐖» 1024 (Lean.ParserDescr.symbol "𝐖")

noncomputable def Complexity.BooleanAnalysis.degreePart {n : ℕ} (f : BooleanFunction n) (k : ℕ) : BooleanFunction n

The degree-k part of f: f^{=k} = ∑_{|S|=k} 𝓕 f S · χ S. (Definition 1.19)

Equations

• Complexity.BooleanAnalysis.degreePart f k x = ∑ S : Finset (Fin n) with S.card = k, Complexity.BooleanAnalysis.fourierCoeff f S * Complexity.BooleanAnalysis.parityFun S x

noncomputable def Complexity.BooleanAnalysis.lowDegreePart {n : ℕ} (f : BooleanFunction n) (k : ℕ) : BooleanFunction n

The degree-at-most-k part of f: f^{≤k} = ∑_{|S|≤k} 𝓕 f S · χ S. (Definition 1.19)

Equations

• Complexity.BooleanAnalysis.lowDegreePart f k x = ∑ S : Finset (Fin n) with S.card ≤ k, Complexity.BooleanAnalysis.fourierCoeff f S * Complexity.BooleanAnalysis.parityFun S x

noncomputable def Complexity.BooleanAnalysis.fourierWeightAbove {n : ℕ} (f : BooleanFunction n) (k : ℕ) : ℝ

The Fourier weight of f at degrees above k: 𝐖^{>k}[f] = ∑_{|S|>k} (𝓕 f S)². (Definition 1.19)

Equations

• Complexity.BooleanAnalysis.fourierWeightAbove f k = ∑ S : Finset (Fin n) with S.card > k, Complexity.BooleanAnalysis.fourierWeight f S

noncomputable def Complexity.BooleanAnalysis.degree {n : ℕ} (f : BooleanFunction n) : WithBot ℕ

The (real) degree of f : 𝔽₂ⁿ → ℝ: deg(f) = max { |S| : 𝓕 f S ≠ 0 }. (Exercise 1.10, referenced in main text)

Returns ⊥ for the zero function (which has no nonzero Fourier coefficients). The book leaves the degree undefined in this case. We use WithBot ℕ so that degree comparisons integrate cleanly with Mathlib's order theory.

Equations

• Complexity.BooleanAnalysis.degree f = {S : Finset (Fin n) | Complexity.BooleanAnalysis.fourierCoeff f S ≠ 0}.sup fun (S : Finset (Fin n)) => ↑S.card

§1.5 Probability densities and convolution

structure Complexity.BooleanAnalysis.IsDensity {n : ℕ} (φ : BooleanFunction n) : Prop

A probability density on 𝔽₂ⁿ is a nonneg function with 𝔼[φ] = 1. (Definition 1.20)

• nonneg (x : Cube n) : 0 ≤ φ x
• expect_one : expect φ = 1

noncomputable def Complexity.BooleanAnalysis.setDensity {n : ℕ} (A : Finset (Cube n)) : BooleanFunction n

The density function associated to a nonempty set A ⊆ 𝔽₂ⁿ: φ_A = (1 / 𝔼[𝟙 A]) · 𝟙 A. (Definition 1.22)

Warning: This definition is junk when A = ∅, since it divides by 𝔼[𝟙 ∅] = 0. The book requires A to be nonempty. Theorems using setDensity should include a hypothesis A.Nonempty where needed.

Equations

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

noncomputable def Complexity.BooleanAnalysis.convolution {n : ℕ} (f g : BooleanFunction n) : BooleanFunction n

The convolution of f, g : 𝔽₂ⁿ → ℝ, defined by (f ⊛ g)(x) = 𝔼_y[f(y)·g(x + y)]. (Definition 1.24)

Equations

• Complexity.BooleanAnalysis.convolution f g x = Complexity.BooleanAnalysis.expect fun (y : Complexity.BooleanAnalysis.Cube n) => f y * g (x + y)

def Complexity.BooleanAnalysis.«term_⊛_» : Lean.TrailingParserDescr

f ⊛ g — the convolution of f and g.

Equations

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

§1.6 Linearity and the BLR test

def Complexity.BooleanAnalysis.IsLinear {n : ℕ} (f : BooleanFunction n) : Prop

A function f : 𝔽₂ⁿ → 𝔽₂ (encoded as BooleanFunction n with ±1 values) is linear if it equals some parity function χ S. (Definition 1.28)

Equations

• Complexity.BooleanAnalysis.IsLinear f = ∃ (S : Finset (Fin n)), ∀ (x : Complexity.BooleanAnalysis.Cube n), f x = Complexity.BooleanAnalysis.parityFun S x

def Complexity.BooleanAnalysis.IsMultiplicative {n : ℕ} (f : BooleanFunction n) : Prop

A function f : 𝔽₂ⁿ → ℝ is multiplicative if f(x+y) = f(x)·f(y) for all x, y. This generalizes property (1) from Definition 1.28 to real-valued functions; the equivalence with IsLinear requires IsBooleanValued (see isLinear_iff_isMultiplicative).

Equations

• Complexity.BooleanAnalysis.IsMultiplicative f = ∀ (x y : Complexity.BooleanAnalysis.Cube n), f (x + y) = f x * f y

def Complexity.BooleanAnalysis.IsClose {n : ℕ} (f g : BooleanFunction n) (ε : ℝ) : Prop

Two functions are ε-close if dist(f, g) ≤ ε, where dist is the fraction of inputs on which they differ (Definition 1.29, stated there for Boolean-valued functions; no Boolean-valuedness is required here).

Equations

• Complexity.BooleanAnalysis.IsClose f g ε = (Complexity.BooleanAnalysis.hammingDist f g ≤ ε)

def Complexity.BooleanAnalysis.IsCloseToProperty {n : ℕ} (f : BooleanFunction n) (P : BooleanFunction n → Prop) (ε : ℝ) : Prop

A function is ε-close to a property P if there exists g satisfying P with dist(f, g) ≤ ε (Definition 1.29, stated there for Boolean-valued functions; no Boolean-valuedness is required here).

Equations

• Complexity.BooleanAnalysis.IsCloseToProperty f P ε = ∃ (g : Complexity.BooleanAnalysis.BooleanFunction n), P g ∧ Complexity.BooleanAnalysis.IsClose f g ε

noncomputable def Complexity.BooleanAnalysis.blrAcceptProb {n : ℕ} (f : BooleanFunction n) : ℝ

The BLR acceptance probability: Pr_{x,y}[f(x)·f(y) = f(x+y)]. For Boolean-valued f it equals 1/2 + 1/2 · ∑_S 𝓕 f S ^ 3 (blrAcceptProb_eq); without that hypothesis the identity can fail (for f = 0 the probability is 1).

Equations

• Complexity.BooleanAnalysis.blrAcceptProb f = Complexity.BooleanAnalysis.prob₂ fun (x y : Complexity.BooleanAnalysis.Cube n) => f x * f y = f (x + y)