Influences and the noise operator on the Boolean cube

55 fully proved

Coordinate flips

DefinitionCoordinate flip on the Boolean cube#✓fully proved

For a point \(x\) of the Boolean cube of dimension \(n\) and a coordinate \(i \in \{0, \dots, n-1\}\), the point \(x^{\oplus i}\) is obtained from \(x\) by negating its \(i\)-th coordinate (exchanging true and false) and leaving every other coordinate unchanged.

def flipCoord (x : BoolCube n) (i : Fin n) : BoolCube n :=
  Function.update x i (!x i)

Uses 1 · Used by 15

Statement usesBoolean cube

Used byFlipping a coordinate negates the Fourier coefficients of the sets containing it · Influence of a coordinate · Constant functions have zero influence · Influence of a Boolean function as a flip probability · Fourier formula for influence · Influences are nonnegative · Flipping a coordinate in a Fourier character · Averages are invariant under flipping a coordinate · A coordinate flip fixes the other coordinates · A coordinate flip negates the flipped coordinate · Flipping a coordinate twice · Flipping a coordinate is an involution · A coordinate flip moves every point · Flipping a coordinate preserves sums over the cube · Event influence is four times the canonical influence

TheoremA coordinate flip negates the flipped coordinate#✓fully proved

For every point \(x\) of the Boolean cube of dimension \(n\) and every coordinate \(i \in \{0, \dots, n-1\}\), the \(i\)-th coordinate of \(x^{\oplus i}\), the point \(x\) with its \(i\)-th coordinate flipped, is the negation \(\lnot x_i\) of \(x_i\) (true and false exchanged).

@[simp] theorem flipCoord_apply_self (x : BoolCube n) (i : Fin n) : flipCoord x i i = !x i

Uses 2 · Used by 3

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Used byFlipping a coordinate in a Fourier character · Flipping a coordinate twice · A coordinate flip moves every point

TheoremA coordinate flip fixes the other coordinates#✓fully proved

For every point \(x\) of the Boolean cube of dimension \(n\) and all coordinates \(i, j \in \{0, \dots, n-1\}\) with \(j \ne i\), the \(j\)-th coordinate of \(x^{\oplus i}\), the point \(x\) with its \(i\)-th coordinate flipped, is \(x_j\).

@[simp] theorem flipCoord_apply_of_ne (x : BoolCube n) {i j : Fin n} (h : j ≠ i) :
    flipCoord x i j = x j

Uses 2 · Used by 2

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Used byFlipping a coordinate in a Fourier character · Flipping a coordinate twice

TheoremFlipping a coordinate twice#✓fully proved

For every point \(x\) of the Boolean cube of dimension \(n\) and every coordinate \(i \in \{0, \dots, n-1\}\), writing \(x^{\oplus i}\) for \(x\) with its \(i\)-th coordinate flipped, we have \((x^{\oplus i})^{\oplus i} = x\).

@[simp] theorem flipCoord_flipCoord (x : BoolCube n) (i : Fin n) :
    flipCoord (flipCoord x i) i = x

Uses 4 · Used by 2

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Proof usesA coordinate flip fixes the other coordinates · A coordinate flip negates the flipped coordinate

Used byFlipping a coordinate negates the Fourier coefficients of the sets containing it · Flipping a coordinate is an involution

TheoremFlipping a coordinate is an involution#✓fully proved

For every \(n \in \mathbb{N}\) and every coordinate \(i \in \{0, \dots, n-1\}\), the map \(x \mapsto x^{\oplus i}\) on the Boolean cube of dimension \(n\), which flips the \(i\)-th coordinate, is an involution: applying it twice gives the identity.

theorem flipCoord_involutive (i : Fin n) : Function.Involutive (flipCoord · i)

Uses 3 · Used by 2

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Proof usesFlipping a coordinate twice

Used byAverages are invariant under flipping a coordinate · Flipping a coordinate preserves sums over the cube

TheoremA coordinate flip moves every point#✓fully proved

For every point \(x\) of the Boolean cube of dimension \(n\) and every coordinate \(i \in \{0, \dots, n-1\}\), the point \(x^{\oplus i}\) obtained from \(x\) by flipping its \(i\)-th coordinate is different from \(x\).

theorem flipCoord_ne_self (x : BoolCube n) (i : Fin n) : flipCoord x i ≠ x

Uses 3

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Proof usesA coordinate flip negates the flipped coordinate

TheoremSign of a negated Boolean value#✓fully proved

For every Boolean value \(b\), the sign of its negation is the negative of its sign: \(\sigma(\lnot b) = -\sigma(b)\), where \(\sigma(\text{true}) = 1\) and \(\sigma(\text{false}) = -1\).

@[simp] theorem cubeVal_not (b : Bool) : cubeVal (!b) = -cubeVal b

Uses 1 · Used by 1

Statement usesSign of a Boolean coordinate

Used byFlipping a coordinate in a Fourier character

TheoremCoordinate signs are nonzero#✓fully proved

For every Boolean value \(b\), its sign \(\sigma(b)\) (equal to \(1\) for true and \(-1\) for false) is nonzero.

@[simp] theorem cubeVal_ne_zero (b : Bool) : cubeVal b ≠ 0

Uses 1

Statement usesSign of a Boolean coordinate

TheoremCoordinate signs have absolute value one#✓fully proved

For every Boolean value \(b\), its sign \(\sigma(b)\), which is \(1\) for true and \(-1\) for false, satisfies \(|\sigma(b)| = 1\).

@[simp] theorem abs_cubeVal (b : Bool) : |cubeVal b| = 1

Uses 1 · Used by 1

Statement usesSign of a Boolean coordinate

Used byPositivity of the noise operator

TheoremFlipping a coordinate in a Fourier character#✓fully proved

Let \(S \subseteq \{0, \dots, n-1\}\), let \(x\) be a point of the Boolean cube in \(n\) coordinates, let \(i < n\), and write \(x^{\oplus i}\) for \(x\) with coordinate \(i\) flipped. Then the Fourier character \(\chi_S\) satisfies \(\chi_S(x^{\oplus i}) = -\chi_S(x)\) if \(i \in S\), and \(\chi_S(x^{\oplus i}) = \chi_S(x)\) if \(i \notin S\).

theorem cubeChi_flipCoord (S : Finset (Fin n)) (x : BoolCube n) (i : Fin n) :
    cubeChi n S (flipCoord x i) = if i ∈ S then -cubeChi n S x else cubeChi n S x

Uses 7 · Used by 1

Statement usesBoolean cube · Fourier character on the Boolean cube · Coordinate flip on the Boolean cube

Proof usesSign of a Boolean coordinate · Sign of a negated Boolean value · A coordinate flip fixes the other coordinates · A coordinate flip negates the flipped coordinate

Used byFlipping a coordinate negates the Fourier coefficients of the sets containing it

TheoremFlipping a coordinate preserves sums over the cube#✓fully proved

Let \(M\) be an additive commutative monoid, \(n \in \mathbb{N}\), \(f\) a function from the Boolean cube of dimension \(n\) to \(M\), and \(i \in \{0, \dots, n-1\}\). For a point \(x\) of the cube write \(x^{\oplus i}\) for the point \(x\) with its \(i\)-th coordinate flipped. Then \(\sum_x f(x^{\oplus i}) = \sum_x f(x)\), both sums ranging over all points \(x\) of the cube.

theorem sum_comp_flipCoord {M : Type*} [AddCommMonoid M] (f : BoolCube n → M) (i : Fin n) :
    ∑ x, f (flipCoord x i) = ∑ x, f x

Uses 3

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Proof usesFlipping a coordinate is an involution

TheoremAverages are invariant under flipping a coordinate#✓fully proved

Let \(M\) be an additive commutative monoid that is a module over the nonnegative rationals, let \(f\) be a function from the Boolean cube in \(n\) coordinates to \(M\), and let \(i < n\). Writing \(x^{\oplus i}\) for \(x\) with coordinate \(i\) flipped, the uniform average of \(f(x^{\oplus i})\) over all points \(x\) of the cube equals the uniform average of \(f(x)\).

theorem expect_comp_flipCoord {M : Type*} [AddCommMonoid M] [Module ℚ≥0 M]
    (f : BoolCube n → M) (i : Fin n) : 𝔼 x, f (flipCoord x i) = 𝔼 x, f x

Uses 3 · Used by 1

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Proof usesFlipping a coordinate is an involution

Used byFlipping a coordinate negates the Fourier coefficients of the sets containing it

Fourier expansion

TheoremUniform average over the Boolean cube as a sum#✓fully proved

For every \(n \in \mathbb{N}\) and every function \(f : \{-1, 1\}^n \to \mathbb{R}\), the uniform average of \(f\) over the Boolean cube \(\{-1, 1\}^n\) is \(\mathbb{E}_x f(x) = \frac{1}{2^n} \sum_{x \in \{-1, 1\}^n} f(x)\).

theorem expect_eq_sum_div_two_pow (f : BoolCube n → ℝ) : 𝔼 x, f x = (∑ x, f x) / 2 ^ n

Uses 2 · Used by 2

Statement usesBoolean cube

Proof usesNumber of points of the Boolean cube

Used byFourier coefficients as sums over the cube · Uniform variance agrees with the canonical Boolean variance

TheoremFourier coefficients as averages#✓fully proved

For every real-valued function \(f\) on the Boolean cube in \(n\) coordinates and every set \(S\) of the \(n\) coordinates, the Fourier coefficient \(\hat f(S)\) is the average of \(f(x) \chi_S(x)\) over all points \(x\) of the cube, \(\hat f(S) = \mathbb{E}_x [f(x) \chi_S(x)]\), where \(\chi_S\) is the Fourier character of \(S\).

theorem boolFourierCoeff_eq_expect (f : BoolCube n → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n f S = 𝔼 x, f x * cubeChi n S x

Uses 3 · Used by 7

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Fourier character on the Boolean cube

Used byAdditivity of Fourier coefficients · Flipping a coordinate negates the Fourier coefficients of the sets containing it · Homogeneity of Fourier coefficients · Fourier coefficients as sums over the cube · Fourier coefficients of a difference · Average over the Boolean cube as the empty Fourier coefficient · Plancherel's identity on the Boolean cube

TheoremFourier coefficients as sums over the cube#✓fully proved

For every real-valued function \(f\) on the Boolean cube in \(n\) coordinates and every set \(S\) of the \(n\) coordinates, the Fourier coefficient of \(f\) at \(S\) is \(\hat f(S) = \frac{1}{2^n} \sum_x f(x) \chi_S(x)\), where the sum runs over all points \(x\) of the cube and \(\chi_S\) is the Fourier character of \(S\).

theorem boolFourierCoeff_eq_sum_div_two_pow (f : BoolCube n → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n f S = (∑ x, f x * cubeChi n S x) / 2 ^ n

Uses 5 · Used by 5

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Fourier character on the Boolean cube

Proof usesFourier coefficients as averages · Uniform average over the Boolean cube as a sum

Used byFourier coefficients of a constant function · Fourier coefficients of a character · Uniqueness of the Fourier expansion · Fourier expansion of the noise operator · Fourier inversion on the Boolean cube

TheoremAverage over the Boolean cube as the empty Fourier coefficient#✓fully proved

For every \(n \in \mathbb{N}\) and every function \(f : \{-1, 1\}^n \to \mathbb{R}\), the uniform average \(\mathbb{E}_x f(x)\) of \(f\) over the Boolean cube \(\{-1, 1\}^n\) equals the Fourier coefficient \(\hat f(\emptyset)\) of \(f\) at the empty set.

theorem expect_eq_boolFourierCoeff_empty (f : BoolCube n → ℝ) :
    𝔼 x, f x = boolFourierCoeff n f ∅

Uses 5 · Used by 3

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier coefficients as averages · Fourier character on the Boolean cube · The empty Fourier character is constant one

Used byThe noise operator \(T_0\) takes the mean · Variance in terms of Fourier coefficients · The noise operator preserves the mean

TheoremOrthogonality of the Boolean cube characters#✓fully proved

Let \(n \in \mathbb{N}\), let \(S\) and \(T\) be subsets of \(\{0, \dots, n-1\}\), and let \(\chi_S\) and \(\chi_T\) be their Fourier characters. Then \(\sum_x \chi_S(x) \chi_T(x)\), the sum ranging over all points \(x\) of the Boolean cube of dimension \(n\), equals \(2^n\) if \(S = T\) and \(0\) otherwise.

theorem sum_cubeChi_mul_cubeChi_eq_ite (S T : Finset (Fin n)) :
    ∑ x : BoolCube n, cubeChi n S x * cubeChi n T x = if S = T then 2 ^ n else 0

Uses 3 · Used by 3

Statement usesBoolean cube · Fourier character on the Boolean cube

Proof usesSign of a Boolean coordinate

Used byFourier coefficients of a character · Uniqueness of the Fourier expansion · Sum of a Boolean cube character

TheoremSum of a Boolean cube character#✓fully proved

For every \(n \in \mathbb{N}\) and every subset \(S\) of \(\{0, \dots, n-1\}\), the sum of the Fourier character \(\chi_S\) over all points of the Boolean cube of dimension \(n\) equals \(2^n\) if \(S\) is empty and \(0\) otherwise.

theorem sum_cubeChi_eq_ite (S : Finset (Fin n)) :
    ∑ x : BoolCube n, cubeChi n S x = if S = ∅ then 2 ^ n else 0

Uses 4 · Used by 2

Statement usesBoolean cube · Fourier character on the Boolean cube

Proof usesThe empty Fourier character is constant one · Orthogonality of the Boolean cube characters

Used byFourier coefficients of a constant function · Bonami–Beckner applied to a discrete derivative

TheoremDual orthogonality of the Boolean cube characters#✓fully proved

Let \(n \in \mathbb{N}\) and let \(x, y\) be points of the Boolean cube of dimension \(n\). For each subset \(S\) of \(\{0, \dots, n-1\}\) let \(\chi_S\) be the Fourier character of \(S\). Then \(\sum_S \chi_S(x) \chi_S(y)\), the sum ranging over all subsets \(S\) of \(\{0, \dots, n-1\}\), equals \(2^n\) if \(x = y\) and \(0\) otherwise.

theorem sum_cubeChi_apply_mul_cubeChi_apply_eq_ite (x y : BoolCube n) :
    ∑ S : Finset (Fin n), cubeChi n S x * cubeChi n S y = if x = y then 2 ^ n else 0

Uses 4 · Used by 1

Statement usesBoolean cube · Fourier character on the Boolean cube

Proof usesSign of a Boolean coordinate · Coordinate signs square to one

Used byFourier inversion on the Boolean cube

TheoremFourier inversion on the Boolean cube#✓fully proved

Let \(n \in \mathbb{N}\), let \(f\) be a real-valued function on the Boolean cube of dimension \(n\), and let \(x\) be a point of the cube. For each subset \(S\) of \(\{0, \dots, n-1\}\) let \(\hat f(S)\) be the Fourier coefficient of \(f\) at \(S\) and \(\chi_S\) the Fourier character of \(S\). Then \(\sum_S \hat f(S) \chi_S(x) = f(x)\), the sum ranging over all subsets \(S\) of \(\{0, \dots, n-1\}\).

theorem sum_boolFourierCoeff_mul_cubeChi (f : BoolCube n → ℝ) (x : BoolCube n) :
    ∑ S, boolFourierCoeff n f S * cubeChi n S x = f x

Uses 5 · Used by 4

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Fourier character on the Boolean cube

Proof usesFourier coefficients as sums over the cube · Dual orthogonality of the Boolean cube characters

Used byFourier coefficients determine the function · The noise operator \(T_1\) is the identity · Plancherel's identity on the Boolean cube · Fourier inversion on the Boolean cube

TheoremPlancherel's identity on the Boolean cube#✓fully proved

For every \(n \in \mathbb{N}\) and all functions \(f, g : \{-1, 1\}^n \to \mathbb{R}\), the uniform average of \(f g\) over the Boolean cube \(\{-1, 1\}^n\) is the sum, over all sets \(S \subseteq \{0, \dots, n-1\}\), of the products of the Fourier coefficients of \(f\) and \(g\) at \(S\): \(\mathbb{E}_x f(x) g(x) = \sum_S \hat f(S) \hat g(S)\).

theorem expect_mul_eq_sum_boolFourierCoeff_mul (f g : BoolCube n → ℝ) :
    𝔼 x, f x * g x = ∑ S, boolFourierCoeff n f S * boolFourierCoeff n g S

Uses 5 · Used by 2

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier coefficients as averages · Fourier character on the Boolean cube · Fourier inversion on the Boolean cube

Used byParseval's identity on the Boolean cube · Parseval's identity on the Boolean cube

TheoremParseval's identity on the Boolean cube#✓fully proved

For every \(n \in \mathbb{N}\) and every function \(f : \{-1, 1\}^n \to \mathbb{R}\), the uniform average of \(f^2\) over the Boolean cube \(\{-1, 1\}^n\) is the sum, over all sets \(S \subseteq \{0, \dots, n-1\}\), of the squares of the Fourier coefficients of \(f\) at \(S\): \(\mathbb{E}_x f(x)^2 = \sum_S \hat f(S)^2\).

theorem expect_sq_eq_sum_boolFourierCoeff_sq (f : BoolCube n → ℝ) :
    𝔼 x, f x ^ 2 = ∑ S, boolFourierCoeff n f S ^ 2

Uses 3 · Used by 3

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesPlancherel's identity on the Boolean cube

Used byFourier formula for influence · Variance in terms of Fourier coefficients · Hypercontractivity in Fourier form

TheoremFourier coefficients determine the function#✓fully proved

If two real-valued functions \(f\) and \(g\) on the Boolean cube in \(n\) coordinates have the same Fourier coefficient \(\hat f(S) = \hat g(S)\) at every set \(S\) of the \(n\) coordinates, then \(f = g\).

theorem boolFourierCoeff_injective : Function.Injective (boolFourierCoeff n)

Uses 4 · Used by 1

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier character on the Boolean cube · Fourier inversion on the Boolean cube

Used bySemigroup property of the noise operator

TheoremAdditivity of Fourier coefficients#✓fully proved

For all real-valued functions \(f\) and \(g\) on the Boolean cube in \(n\) coordinates and every set \(S\) of the \(n\) coordinates, the Fourier coefficient of \(f + g\) at \(S\) is the sum of the Fourier coefficients of \(f\) and \(g\) at \(S\): \(\widehat{f + g}(S) = \hat f(S) + \hat g(S)\).

theorem boolFourierCoeff_add (f g : BoolCube n → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun x => f x + g x) S =
      boolFourierCoeff n f S + boolFourierCoeff n g S

Uses 4

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier coefficients as averages · Fourier character on the Boolean cube

TheoremFourier coefficients of a difference#✓fully proved

For real-valued functions \(f\) and \(g\) on the Boolean cube \(\{-1, 1\}^n\) and every set \(S \subseteq \{0, \dots, n-1\}\), the Fourier coefficient of \(f - g\) at \(S\) is \(\widehat{f - g}(S) = \hat f(S) - \hat g(S)\).

theorem boolFourierCoeff_sub (f g : BoolCube n → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun x => f x - g x) S =
      boolFourierCoeff n f S - boolFourierCoeff n g S

Uses 4 · Used by 2

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier coefficients as averages · Fourier character on the Boolean cube

Used byFourier formula for influence · Variance in terms of Fourier coefficients

TheoremHomogeneity of Fourier coefficients#✓fully proved

For every real \(c\), every real-valued function \(f\) on the Boolean cube in \(n\) coordinates and every set \(S\) of the \(n\) coordinates, the Fourier coefficient of \(c f\) at \(S\) is \(c\) times the Fourier coefficient of \(f\) at \(S\): \(\widehat{c f}(S) = c \hat f(S)\).

theorem boolFourierCoeff_const_mul (c : ℝ) (f : BoolCube n → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun x => c * f x) S = c * boolFourierCoeff n f S

Uses 4 · Used by 1

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier coefficients as averages · Fourier character on the Boolean cube

Used byFourier formula for influence

TheoremFourier coefficients of a constant function#✓fully proved

For every real \(c\) and every set \(S\) of the \(n\) coordinates, the Fourier coefficient at \(S\) of the constant function \(x \mapsto c\) on the Boolean cube in \(n\) coordinates is \(c\) if \(S = \emptyset\) and \(0\) otherwise.

theorem boolFourierCoeff_const (c : ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun _ => c) S = if S = ∅ then c else 0

Uses 5 · Used by 2

Statement usesBoolean cube · Fourier coefficient on the Boolean cube

Proof usesFourier coefficients as sums over the cube · Fourier character on the Boolean cube · Sum of a Boolean cube character

Used byThe noise operator fixes constants · Variance in terms of Fourier coefficients

TheoremFourier coefficients of a character#✓fully proved

For all sets \(S\) and \(T\) of the \(n\) coordinates, the Fourier coefficient at \(S\) of the Fourier character \(\chi_T\) on the Boolean cube in \(n\) coordinates, \(\chi_T(x) = \prod_{i \in T} \sigma(x_i)\) with \(\sigma(\text{true}) = 1\) and \(\sigma(\text{false}) = -1\), is \(1\) if \(T = S\) and \(0\) otherwise.

theorem boolFourierCoeff_cubeChi (T S : Finset (Fin n)) :
    boolFourierCoeff n (cubeChi n T) S = if T = S then 1 else 0

Uses 5 · Used by 1

Statement usesFourier coefficient on the Boolean cube · Fourier character on the Boolean cube

Proof usesBoolean cube · Fourier coefficients as sums over the cube · Orthogonality of the Boolean cube characters

Used byCharacters are eigenfunctions of the noise operator

TheoremUniqueness of the Fourier expansion#✓fully proved

For real numbers \(a_T\) indexed by the sets \(T \subseteq \{0, \dots, n-1\}\), let \(g(x) = \sum_T a_T \chi_T(x)\) on the Boolean cube \(\{-1, 1\}^n\), where \(\chi_T\) is the Fourier character of \(T\). Then for every set \(S \subseteq \{0, \dots, n-1\}\) the Fourier coefficient of \(g\) at \(S\) is \(\hat g(S) = a_S\).

theorem boolFourierCoeff_sum_mul_cubeChi (a : Finset (Fin n) → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun x => ∑ T, a T * cubeChi n T x) S = a S

Uses 5 · Used by 1

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Fourier character on the Boolean cube

Proof usesFourier coefficients as sums over the cube · Orthogonality of the Boolean cube characters

Used byFourier coefficients of the noise operator

TheoremFlipping a coordinate negates the Fourier coefficients of the sets containing it#✓fully proved

Let \(f\) be a real-valued function on the Boolean cube in \(n\) coordinates, let \(i\) be a coordinate, and let \(g(x) = f(x^{\oplus i})\), where \(x^{\oplus i}\) is the point \(x\) with its \(i\)-th coordinate flipped. Write \(\hat f(S)\) and \(\hat g(S)\) for the Fourier coefficients of \(f\) and \(g\) at a set \(S\) of the \(n\) coordinates. Then for every such \(S\), \(\hat g(S) = -\hat f(S)\) if \(i \in S\) and \(\hat g(S) = \hat f(S)\) if \(i \notin S\).

theorem boolFourierCoeff_comp_flipCoord (f : BoolCube n → ℝ) (i : Fin n) (S : Finset (Fin n)) :
    boolFourierCoeff n (fun x => f (flipCoord x i)) S =
      if i ∈ S then -boolFourierCoeff n f S else boolFourierCoeff n f S

Uses 8 · Used by 1

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Coordinate flip on the Boolean cube

Proof usesFourier coefficients as averages · Fourier character on the Boolean cube · Flipping a coordinate in a Fourier character · Averages are invariant under flipping a coordinate · Flipping a coordinate twice

Used byFourier formula for influence

Influence, total influence and variance

DefinitionInfluence of a coordinate#✓fully proved

For a real-valued function \(f\) on the Boolean cube \(\{-1, 1\}^n\) and a coordinate \(i \in \{0, \dots, n-1\}\), the influence of \(i\) on \(f\) is \(\mathrm{Inf}_i[f] = \mathbb{E}_x\big[\big((f(x) - f(x^{\oplus i})) / 2\big)^2\big]\), where the expectation is over \(x\) uniform on the cube and \(x^{\oplus i}\) is \(x\) with its \(i\)-th coordinate flipped.

noncomputable def boolInfluence (f : BoolCube n → ℝ) (i : Fin n) : ℝ :=
  𝔼 x, ((f x - f (flipCoord x i)) / 2) ^ 2

Uses 2 · Used by 11

Statement usesBoolean cube · Coordinate flip on the Boolean cube

Used byConstant functions have zero influence · Influence of a Boolean function as a flip probability · Fourier formula for influence · Influences are nonnegative · Total influence on the Boolean cube · Constant functions have zero total influence · Total influence in Fourier form · Total influence is nonnegative · Event influence is four times the canonical influence · Influence of a coordinate as Fourier weight · Total influence as Fourier weight

DefinitionTotal influence on the Boolean cube#✓fully proved

For a function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\), the total influence of \(f\) is the sum of the influences of its \(n\) coordinates, \(\mathrm{I}[f] = \sum_{i=0}^{n-1} \mathrm{Inf}_i[f]\), where \(\mathrm{Inf}_i[f] = \mathbb{E}_x \left[\left(\frac{f(x) - f(x^{\oplus i})}{2}\right)^2\right]\), \(x^{\oplus i}\) is \(x\) with its \(i\)-th coordinate flipped and \(\mathbb{E}_x\) is the uniform average over the points \(x\) of the cube.

noncomputable def boolTotalInfluence (f : BoolCube n → ℝ) : ℝ :=
  ∑ i, boolInfluence f i

Uses 2 · Used by 5

Statement usesBoolean cube · Influence of a coordinate

Used byConstant functions have zero total influence · Total influence in Fourier form · Total influence is nonnegative · Poincaré inequality on the Boolean cube · Total influence as Fourier weight

DefinitionVariance on the Boolean cube#✓fully proved

For a function \(f : \{-1, 1\}^n \to \mathbb{R}\) on the Boolean cube, its variance under the uniform distribution is \(\mathrm{Var}[f] = \mathbb{E}_x\big[(f(x) - \mathbb{E}_y[f(y)])^2\big]\), where \(\mathbb{E}_x\) denotes the uniform average over the \(2^n\) points \(x\) of the cube.

noncomputable def boolVariance (f : BoolCube n → ℝ) : ℝ :=
  𝔼 x, (f x - 𝔼 y, f y) ^ 2

Uses 1 · Used by 7

Statement usesBoolean cube

Used byConstant functions have zero variance · Variance as mean square minus squared mean · Variance in terms of Fourier coefficients · Poincaré inequality on the Boolean cube · Variance on the Boolean cube is nonnegative · Variance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance

TheoremInfluences are nonnegative#✓fully proved

For every real-valued function \(f\) on the Boolean cube \(\{-1, 1\}^n\) and every coordinate \(i \in \{0, \dots, n-1\}\), the influence \(\mathrm{Inf}_i[f]\) of coordinate \(i\) on \(f\) satisfies \(\mathrm{Inf}_i[f] \ge 0\).

theorem boolInfluence_nonneg (f : BoolCube n → ℝ) (i : Fin n) : 0 ≤ boolInfluence f i

Uses 3 · Used by 1

Statement usesBoolean cube · Influence of a coordinate

Proof usesCoordinate flip on the Boolean cube

Used byTotal influence is nonnegative

TheoremTotal influence is nonnegative#✓fully proved

For every function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\), the total influence of \(f\) is nonnegative.

theorem boolTotalInfluence_nonneg (f : BoolCube n → ℝ) : 0 ≤ boolTotalInfluence f

Uses 4

Statement usesBoolean cube · Total influence on the Boolean cube

Proof usesInfluence of a coordinate · Influences are nonnegative

TheoremVariance on the Boolean cube is nonnegative#✓fully proved

For every function \(f : \{-1, 1\}^n \to \mathbb{R}\) on the Boolean cube, the variance of \(f\) under the uniform distribution is at least \(0\).

theorem boolVariance_nonneg (f : BoolCube n → ℝ) : 0 ≤ boolVariance f

Uses 2

Statement usesBoolean cube · Variance on the Boolean cube

TheoremConstant functions have zero influence#✓fully proved

For every real number \(c\) and every coordinate \(i \in \{0, \dots, n-1\}\), the influence of coordinate \(i\) on the constant function with value \(c\) on the Boolean cube \(\{-1, 1\}^n\) is \(0\).

@[simp] theorem boolInfluence_const (c : ℝ) (i : Fin n) : boolInfluence (fun _ => c) i = 0

Uses 3 · Used by 1

Statement usesBoolean cube · Influence of a coordinate

Proof usesCoordinate flip on the Boolean cube

Used byConstant functions have zero total influence

TheoremConstant functions have zero total influence#✓fully proved

For every real number \(c\), the constant function with value \(c\) on the Boolean cube \(\{-1, 1\}^n\) has total influence \(0\).

@[simp] theorem boolTotalInfluence_const (c : ℝ) :
    boolTotalInfluence (fun _ : BoolCube n => c) = 0

Uses 4

Statement usesBoolean cube · Total influence on the Boolean cube

Proof usesInfluence of a coordinate · Constant functions have zero influence

TheoremConstant functions have zero variance#✓fully proved

For every real number \(c\), the constant function with value \(c\) on the Boolean cube \(\{-1, 1\}^n\) has variance \(0\) under the uniform distribution.

@[simp] theorem boolVariance_const (c : ℝ) : boolVariance (fun _ : BoolCube n => c) = 0

Uses 2

Statement usesBoolean cube · Variance on the Boolean cube

TheoremInfluence of a Boolean function as a flip probability#✓fully proved

Let \(f\) be a real-valued function on the Boolean cube \(\{-1, 1\}^n\) that takes only the values \(1\) and \(-1\), and let \(i \in \{0, \dots, n-1\}\). Then the influence of coordinate \(i\) on \(f\) equals the probability, for \(x\) uniform on the cube, that \(f(x^{\oplus i}) \ne f(x)\), where \(x^{\oplus i}\) is \(x\) with its \(i\)-th coordinate flipped.

theorem boolInfluence_eq_expect_ite_ne {f : BoolCube n → ℝ} (hf : ∀ x, f x = 1 ∨ f x = -1)
    (i : Fin n) :
    boolInfluence f i = 𝔼 x, if f (flipCoord x i) ≠ f x then (1 : ℝ) else 0

Uses 3

Statement usesBoolean cube · Influence of a coordinate · Coordinate flip on the Boolean cube

TheoremFourier formula for influence#✓fully proved

For every real-valued function \(f\) on the Boolean cube \(\{-1, 1\}^n\) and every coordinate \(i \in \{0, \dots, n-1\}\), the influence of coordinate \(i\) on \(f\) is \(\mathrm{Inf}_i[f] = \sum_{S \ni i} \hat f(S)^2\), where \(\hat f(S)\) is the Fourier coefficient of \(f\) at \(S\) and the sum runs over the sets \(S \subseteq \{0, \dots, n-1\}\) that contain \(i\).

theorem boolInfluence_eq_sum_sq (f : BoolCube n → ℝ) (i : Fin n) :
    boolInfluence f i = ∑ S with i ∈ S, boolFourierCoeff n f S ^ 2

Uses 8 · Used by 2

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Influence of a coordinate

Proof usesFlipping a coordinate negates the Fourier coefficients of the sets containing it · Homogeneity of Fourier coefficients · Fourier coefficients of a difference · Parseval's identity on the Boolean cube · Coordinate flip on the Boolean cube

Used byTotal influence in Fourier form · Influence of a coordinate as Fourier weight

TheoremVariance in terms of Fourier coefficients#✓fully proved

For every function \(f : \{-1, 1\}^n \to \mathbb{R}\) on the Boolean cube, the variance of \(f\) under the uniform distribution equals \(\sum_{S \neq \emptyset} \hat f(S)^2\), where the sum runs over the nonempty sets \(S \subseteq \{0, \dots, n-1\}\) and \(\hat f(S)\) is the Fourier coefficient of \(f\) at \(S\).

theorem boolVariance_eq_sum_sq (f : BoolCube n → ℝ) :
    boolVariance f = ∑ S with S.Nonempty, boolFourierCoeff n f S ^ 2

Uses 7 · Used by 2

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Variance on the Boolean cube

Proof usesFourier coefficients of a constant function · Fourier coefficients of a difference · Average over the Boolean cube as the empty Fourier coefficient · Parseval's identity on the Boolean cube

Used byPoincaré inequality on the Boolean cube · Variance as Fourier weight off the empty set

TheoremVariance as mean square minus squared mean#✓fully proved

For every function \(f : \{-1, 1\}^n \to \mathbb{R}\) on the Boolean cube, the variance of \(f\) under the uniform distribution equals \(\mathbb{E}_x[f(x)^2] - (\mathbb{E}_x[f(x)])^2\), where \(\mathbb{E}_x\) denotes the uniform average over the \(2^n\) points \(x\) of the cube.

theorem boolVariance_eq_expect_sq_sub_sq (f : BoolCube n → ℝ) :
    boolVariance f = 𝔼 x, f x ^ 2 - (𝔼 x, f x) ^ 2

Uses 2 · Used by 2

Statement usesBoolean cube · Variance on the Boolean cube

Used byVariance as Fourier weight off the empty set · Uniform variance agrees with the canonical Boolean variance

TheoremTotal influence in Fourier form#✓fully proved

For every function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\), the total influence of \(f\) is

\[\mathrm{I}[f] = \sum_{S \subseteq \{0, \dots, n-1\}} |S| \, \hat f(S)^2,\]

where \(\hat f(S)\) is the Fourier coefficient of \(f\) at \(S\).

theorem boolTotalInfluence_eq_sum_card_mul_sq (f : BoolCube n → ℝ) :
    boolTotalInfluence f = ∑ S, (S.card : ℝ) * boolFourierCoeff n f S ^ 2

Uses 5 · Used by 2

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Total influence on the Boolean cube

Proof usesInfluence of a coordinate · Fourier formula for influence

Used byPoincaré inequality on the Boolean cube · Total influence as Fourier weight

TheoremPoincaré inequality on the Boolean cube#✓fully proved

For every function \(f : \{-1, 1\}^n \to \mathbb{R}\) on the Boolean cube, the variance of \(f\) under the uniform distribution is at most the total influence of \(f\): \(\mathrm{Var}[f] \le I[f]\).

theorem boolVariance_le_boolTotalInfluence (f : BoolCube n → ℝ) :
    boolVariance f ≤ boolTotalInfluence f

Uses 6

Statement usesBoolean cube · Total influence on the Boolean cube · Variance on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Total influence in Fourier form · Variance in terms of Fourier coefficients

The noise operator

DefinitionNoise operator on the Boolean cube#✓fully proved

For a real number \(\rho\) and a function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\), the noise operator \(T_\rho\) sends \(f\) to the function

\[T_\rho f(x) = \sum_y \Bigl(\prod_{i < n} \frac{1 + \rho \sigma(x_i) \sigma(y_i)}{2}\Bigr) f(y),\]

where \(y\) runs over all points of the cube and \(\sigma\) is the sign of a coordinate: \(\sigma(\mathrm{true}) = 1\) and \(\sigma(\mathrm{false}) = -1\).

For \(-1 \le \rho \le 1\), \(T_\rho f(x)\) is the expectation of \(f(y)\) when each coordinate of \(y\) independently equals the corresponding coordinate of \(x\) with probability \((1 + \rho) / 2\); the formula is used for every real \(\rho\).

noncomputable def boolNoiseOp (ρ : ℝ) (f : BoolCube n → ℝ) (x : BoolCube n) : ℝ :=
  ∑ y, (∏ i, (1 + ρ * cubeVal (x i) * cubeVal (y i)) / 2) * f y

Uses 2 · Used by 13

Statement usesBoolean cube · Sign of a Boolean coordinate

Used byFourier coefficients of the noise operator · Semigroup property of the noise operator · The noise operator fixes constants · Characters are eigenfunctions of the noise operator · Fourier expansion of the noise operator · Positivity of the noise operator · The noise operator \(T_1\) is the identity · The noise operator \(T_0\) takes the mean · The noise operator preserves the mean · Bonami–Beckner applied to a discrete derivative · Hypercontractivity in Fourier form · Noise operator is diagonal in the Walsh basis · Agreement of the two noise operators on the Boolean cube

TheoremFourier expansion of the noise operator#✓fully proved

For every real number \(\rho\), every function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\) and every point \(x\) of the cube,

\[T_\rho f(x) = \sum_{S \subseteq \{0, \dots, n-1\}} \rho^{|S|} \, \hat f(S) \, \chi_S(x),\]

where \(T_\rho\) is the noise operator, \(\hat f(S)\) is the Fourier coefficient of \(f\) at \(S\), \(\chi_S\) is the Fourier character of \(S\), and \(\rho^0 = 1\) also when \(\rho = 0\).

theorem boolNoiseOp_eq_sum (ρ : ℝ) (f : BoolCube n → ℝ) (x : BoolCube n) :
    boolNoiseOp ρ f x = ∑ S, ρ ^ S.card * boolFourierCoeff n f S * cubeChi n S x

Uses 6 · Used by 6

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Noise operator on the Boolean cube · Fourier character on the Boolean cube

Proof usesFourier coefficients as sums over the cube · Sign of a Boolean coordinate

Used byFourier coefficients of the noise operator · The noise operator fixes constants · Characters are eigenfunctions of the noise operator · The noise operator \(T_1\) is the identity · The noise operator \(T_0\) takes the mean · Noise operator is diagonal in the Walsh basis

TheoremFourier coefficients of the noise operator#✓fully proved

For every real \(\rho\), every real-valued function \(f\) on the Boolean cube in \(n\) coordinates and every set \(S\) of the \(n\) coordinates, the Fourier coefficient at \(S\) of \(T_\rho f\), the noise operator with parameter \(\rho\) applied to \(f\), is \(\widehat{T_\rho f}(S) = \rho^{|S|} \hat f(S)\).

theorem boolFourierCoeff_boolNoiseOp (ρ : ℝ) (f : BoolCube n → ℝ) (S : Finset (Fin n)) :
    boolFourierCoeff n (boolNoiseOp ρ f) S = ρ ^ S.card * boolFourierCoeff n f S

Uses 6 · Used by 3

Statement usesBoolean cube · Fourier coefficient on the Boolean cube · Noise operator on the Boolean cube

Proof usesUniqueness of the Fourier expansion · Fourier expansion of the noise operator · Fourier character on the Boolean cube

Used bySemigroup property of the noise operator · The noise operator preserves the mean · Hypercontractivity in Fourier form

TheoremThe noise operator \(T_1\) is the identity#✓fully proved

For every function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\), the noise operator with \(\rho = 1\) fixes \(f\): \(T_1 f = f\).

@[simp] theorem boolNoiseOp_one (f : BoolCube n → ℝ) : boolNoiseOp 1 f = f

Uses 6

Statement usesBoolean cube · Noise operator on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier expansion of the noise operator · Fourier character on the Boolean cube · Fourier inversion on the Boolean cube

TheoremThe noise operator \(T_0\) takes the mean#✓fully proved

For every function \(f\) from the Boolean cube \(\{-1, 1\}^n\) to \(\mathbb{R}\), the noise operator with \(\rho = 0\) sends \(f\) to the constant function whose value is the mean \(\mathbb{E}_x f(x) = 2^{-n} \sum_x f(x)\) of \(f\) under the uniform distribution.

@[simp] theorem boolNoiseOp_zero (f : BoolCube n → ℝ) : boolNoiseOp 0 f = fun _ => 𝔼 x, f x

Uses 7

Statement usesBoolean cube · Noise operator on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier expansion of the noise operator · Fourier character on the Boolean cube · The empty Fourier character is constant one · Average over the Boolean cube as the empty Fourier coefficient

TheoremSemigroup property of the noise operator#✓fully proved

For all real numbers \(\rho\) and \(\sigma\) and every real-valued function \(f\) on the Boolean cube \(\{-1, 1\}^n\), applying the noise operator \(T_\sigma\) and then \(T_\rho\) to \(f\) gives \(T_{\rho\sigma} f\): \(T_\rho(T_\sigma f) = T_{\rho\sigma} f\).

theorem boolNoiseOp_boolNoiseOp (ρ σ : ℝ) (f : BoolCube n → ℝ) :
    boolNoiseOp ρ (boolNoiseOp σ f) = boolNoiseOp (ρ * σ) f

Uses 5

Statement usesBoolean cube · Noise operator on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier coefficients of the noise operator · Fourier coefficients determine the function

TheoremThe noise operator preserves the mean#✓fully proved

For every real \(\rho\) and every function \(f : \{-1, 1\}^n \to \mathbb{R}\) on the Boolean cube, the uniform average over the cube of \(T_\rho f\), the image of \(f\) under the noise operator with parameter \(\rho\), equals the uniform average of \(f\).

theorem expect_boolNoiseOp (ρ : ℝ) (f : BoolCube n → ℝ) :
    𝔼 x, boolNoiseOp ρ f x = 𝔼 x, f x

Uses 5

Statement usesBoolean cube · Noise operator on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier coefficients of the noise operator · Average over the Boolean cube as the empty Fourier coefficient

TheoremCharacters are eigenfunctions of the noise operator#✓fully proved

For every real number \(\rho\) and every set \(S \subseteq \{0, \dots, n-1\}\), the noise operator \(T_\rho\) maps the Fourier character \(\chi_S\) on the Boolean cube \(\{-1, 1\}^n\) to the function \(x \mapsto \rho^{|S|} \chi_S(x)\), so \(\chi_S\) is an eigenfunction of \(T_\rho\) with eigenvalue \(\rho^{|S|}\).

theorem boolNoiseOp_cubeChi (ρ : ℝ) (S : Finset (Fin n)) :
    boolNoiseOp ρ (cubeChi n S) = fun x => ρ ^ S.card * cubeChi n S x

Uses 6 · Used by 1

Statement usesBoolean cube · Noise operator on the Boolean cube · Fourier character on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier coefficients of a character · Fourier expansion of the noise operator

Used byBonami–Beckner applied to a discrete derivative

TheoremThe noise operator fixes constants#✓fully proved

For every real number \(\rho\) and every real number \(c\), the noise operator \(T_\rho\) maps the constant function with value \(c\) on the Boolean cube \(\{-1, 1\}^n\) to itself.

@[simp] theorem boolNoiseOp_const (ρ c : ℝ) :
    boolNoiseOp ρ (fun _ : BoolCube n => c) = fun _ => c

Uses 7

Statement usesBoolean cube · Noise operator on the Boolean cube

Proof usesFourier coefficient on the Boolean cube · Fourier coefficients of a constant function · Fourier expansion of the noise operator · Fourier character on the Boolean cube · The empty Fourier character is constant one

TheoremPositivity of the noise operator#✓fully proved

For every real number \(\rho\) with \(|\rho| \le 1\), the noise operator \(T_\rho\) on the Boolean cube maps nonnegative functions to nonnegative functions: if \(f\) is a real function on the cube with \(f(y) \ge 0\) for every point \(y\), then \(T_\rho f(x) \ge 0\) for every point \(x\) of the cube.

theorem boolNoiseOp_nonneg {ρ : ℝ} (hρ : |ρ| ≤ 1) {f : BoolCube n → ℝ} (hf : ∀ x, 0 ≤ f x)
    (x : BoolCube n) : 0 ≤ boolNoiseOp ρ f x

Uses 4

Statement usesBoolean cube · Noise operator on the Boolean cube

Proof usesCoordinate signs have absolute value one · Sign of a Boolean coordinate

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.