The overlap lemma and the boundary/influence identity

The overlap lemma (Lemma 4.1 of the paper; overlap, overlap_pos) and the identity b_j(g) = 2^(n-1) I_j(g) (Lemma 2.1; two_mul_bdry).

theorem AaronsonAmbainis.overlap {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {p q : Cube ι} (hpq : g p ≠ g q) {x y : ι → ℝ} (hx : IsRow g p x) (hy : IsRow g q y) : 1 ≤ ∑ j ∈ diffSet p q, min (x j) (y j)

The overlap lemma (Lemma 4.1 of the paper): rows at points with different values overlap on the difference set.

theorem AaronsonAmbainis.overlap_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {p q : Cube ι} (hpq : g p ≠ g q) {x y : ι → ℝ} (hx : IsRow g p x) (hy : IsRow g q y) {w : ι → ℝ} (hw : ∀ (j : ι), 0 < w j) : 0 < ∑ j ∈ diffSet p q, w j * x j * y j

Consequence of the overlap lemma: the weighted overlap is positive.

theorem AaronsonAmbainis.card_sensitive {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : {x : Cube ι | g (flipSet x {j}) ≠ g x}.card = 2 * bdry g j

The points where flipping j changes g are twice the bichromatic j-edges.

theorem AaronsonAmbainis.two_mul_bdry {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : 2 * ↑(bdry g j) = 2 ^ Fintype.card ι * infl g j

Lemma 2.1 of the paper: 2 b_j(g) = 2^n I_j(g), that is, b_j(g) = 2^(n-1) I_j(g).