Definitions

The definitions of Section 2 of the paper: the cube, the points x^S, the antipode and the set Δ(x,y); the numbers b_j(g) and the zone of a Boolean function; 1-wings and rows; the influences of Boolean and of real functions, mean and variance, the mean absolute increments; the characters and the degree.

Points of the cube are functions ι → Bool for a finite index type ι (the paper's [n]). The paper writes the cube as Q_n = {-1,1}^n, and as {0,1}^n in Corollary 1.2; the identification is false ↦ 0 ↦ +1, true ↦ 1 ↦ -1.

@[reducible, inline]

abbrev AaronsonAmbainis.Cube (ι : Type u_1) : Type u_1

The Boolean cube {0,1}^n.

Equations

• AaronsonAmbainis.Cube ι = (ι → Bool)

def AaronsonAmbainis.flipSet {ι : Type u_1} [DecidableEq ι] (x : Cube ι) (S : Finset ι) : Cube ι

flipSet x S is the point x with exactly the coordinates in S flipped (written x^S in the paper).

Equations

• AaronsonAmbainis.flipSet x S i = if i ∈ S then !x i else x i

def AaronsonAmbainis.antipode {ι : Type u_1} (x : Cube ι) : Cube ι

The antipode of x (all coordinates flipped).

Equations

• AaronsonAmbainis.antipode x i = !x i

def AaronsonAmbainis.diffSet {ι : Type u_1} [Fintype ι] (x y : Cube ι) : Finset ι

diffSet x y is the set of coordinates in which x and y differ (written Δ(x,y) in the paper).

Equations

• AaronsonAmbainis.diffSet x y = {i : ι | x i ≠ y i}

def AaronsonAmbainis.bdry {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : ℕ

bdry g j = b_j(g): the number of bichromatic j-edges of g; each such edge is counted once, at its endpoint where g = true.

Equations

• AaronsonAmbainis.bdry g j = {x : AaronsonAmbainis.Cube ι | g x = true ∧ g (AaronsonAmbainis.flipSet x {j}) = false}.card

def AaronsonAmbainis.zone {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) : Finset (Cube ι)

zone g = Z(g): the points u with g u = true and g (antipode u) = false.

Equations

• AaronsonAmbainis.zone g = {u : AaronsonAmbainis.Cube ι | g u = true ∧ g (AaronsonAmbainis.antipode u) = false}

def AaronsonAmbainis.IsWing {ι : Type u_1} [DecidableEq ι] (g : Cube ι → Bool) (u : Cube ι) (A : Finset ι) : Prop

A is a 1-wing of g at u: flipping any subset of A at u keeps g = true.

Equations

• AaronsonAmbainis.IsWing g u A = ∀ S ⊆ A, g (AaronsonAmbainis.flipSet u S) = true

def AaronsonAmbainis.IsRow {ι : Type u_1} [DecidableEq ι] (g : Cube ι → Bool) (x : Cube ι) (lam : ι → ℝ) : Prop

lam is a row (fractional certificate) of g at x: it is nonnegative and has total weight at least one on every sensitive block of g at x.

Equations

• AaronsonAmbainis.IsRow g x lam = ((∀ (j : ι), 0 ≤ lam j) ∧ ∀ (S : Finset ι), g (AaronsonAmbainis.flipSet x S) ≠ g x → 1 ≤ ∑ j ∈ S, lam j)

noncomputable def AaronsonAmbainis.infl {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : ℝ

Influence of coordinate j on a Boolean function, uniform measure: the fraction of points x with g (x^j) ≠ g x (written I_j(g) in the paper).

Equations

• AaronsonAmbainis.infl g j = ↑{x : AaronsonAmbainis.Cube ι | g (AaronsonAmbainis.flipSet x {j}) ≠ g x}.card / 2 ^ Fintype.card ι

noncomputable def AaronsonAmbainis.mean {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) : ℝ

Mean of a real function on the cube.

Equations

• AaronsonAmbainis.mean f = (∑ x : AaronsonAmbainis.Cube ι, f x) / 2 ^ Fintype.card ι

noncomputable def AaronsonAmbainis.variance {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) : ℝ

Variance of a real function on the cube.

Equations

• AaronsonAmbainis.variance f = (∑ x : AaronsonAmbainis.Cube ι, (f x - AaronsonAmbainis.mean f) ^ 2) / 2 ^ Fintype.card ι

noncomputable def AaronsonAmbainis.inflR {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : ℝ

Influence of coordinate j on a real function: E[((f(x) - f(x^j))/2)^2] (written Inf_j(f) in the paper).

Equations

• AaronsonAmbainis.inflR f j = (∑ x : AaronsonAmbainis.Cube ι, ((f x - f (AaronsonAmbainis.flipSet x {j})) / 2) ^ 2) / 2 ^ Fintype.card ι

noncomputable def AaronsonAmbainis.meanAbsIncr {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : Cube ι → ℝ) (j : ι) : ℝ

The mean absolute increment of a real function in the coordinate j: E_x |f(x) - f(x^j)| (written L_j(f) in the paper; their sum over j is written L(f)). There is no factor 1/2 here, so that L_j(f)^2 ≤ 4 Inf_j(f).

Equations

• AaronsonAmbainis.meanAbsIncr f j = (∑ x : AaronsonAmbainis.Cube ι, |f x - f (AaronsonAmbainis.flipSet x {j})|) / 2 ^ Fintype.card ι

noncomputable def AaronsonAmbainis.chi {ι : Type u_1} (S : Finset ι) (x : Cube ι) : ℝ

The character χ_S(x) = ∏_{i ∈ S} (-1)^{x_i}.

Equations

• AaronsonAmbainis.chi S x = ∏ i ∈ S, if x i = true then -1 else 1

def AaronsonAmbainis.HasDegreeLE {ι : Type u_1} [Fintype ι] (f : Cube ι → ℝ) (d : ℕ) : Prop

f is the restriction to the cube of a multilinear polynomial of degree at most d: its expansion in characters uses only sets of size at most d.

Equations

• AaronsonAmbainis.HasDegreeLE f d = ∃ (c : Finset ι → ℝ), (∀ (S : Finset ι), d < S.card → c S = 0) ∧ ∀ (x : AaronsonAmbainis.Cube ι), f x = ∑ S : Finset ι, c S * AaronsonAmbainis.chi S x

theorem AaronsonAmbainis.flipSet_empty {ι : Type u_1} [DecidableEq ι] (x : Cube ι) : flipSet x ∅ = x

theorem AaronsonAmbainis.flipSet_flipSet_self {ι : Type u_1} [DecidableEq ι] (x : Cube ι) (S : Finset ι) : flipSet (flipSet x S) S = x

theorem AaronsonAmbainis.antipode_eq_flipSet_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : Cube ι) : antipode x = flipSet x Finset.univ

theorem AaronsonAmbainis.diffSet_flipSet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : Cube ι) (S : Finset ι) : diffSet x (flipSet x S) = S

theorem AaronsonAmbainis.flipSet_diffSet {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x y : Cube ι) : flipSet x (diffSet x y) = y