Characters at special points

Row.sgn b = (-1)^b, the all-false point Row.zero, the unit points Row.unit b, the value of a character at these points and at a flipped point, and chi S * chi T = chi (S ∆ T).

Since false stands for +1 and true for -1, the point Row.zero β is the point (1,…,1) of Section 6.3 of the paper, and Row.unit b is obtained from it by changing the sign of the coordinate b.

noncomputable def AaronsonAmbainis.Row.sgn (b : Bool) : ℝ

The sign (-1)^b of a bit.

Equations

• AaronsonAmbainis.Row.sgn b = if b = true then -1 else 1

@[simp]

theorem AaronsonAmbainis.Row.sgn_true : sgn true = -1

@[simp]

theorem AaronsonAmbainis.Row.sgn_false : sgn false = 1

theorem AaronsonAmbainis.Row.sgn_mul_self (b : Bool) : sgn b * sgn b = 1

theorem AaronsonAmbainis.Row.abs_sgn (b : Bool) : |sgn b| = 1

theorem AaronsonAmbainis.Row.sgn_not (b : Bool) : (sgn !b) = -sgn b

def AaronsonAmbainis.Row.zero (β : Type u_1) : Cube β

The all-false point of a cube.

Equations

• AaronsonAmbainis.Row.zero β x✝ = false

def AaronsonAmbainis.Row.unit {β : Type u_1} [DecidableEq β] (b : β) : Cube β

The point with exactly the coordinate b equal to true.

Equations

• AaronsonAmbainis.Row.unit b b' = decide (b' = b)

theorem AaronsonAmbainis.Row.chi_eq_prod_sgn {ι : Type u_1} (T : Finset ι) (x : Cube ι) : chi T x = ∏ i ∈ T, sgn (x i)

theorem AaronsonAmbainis.Row.chi_zero {ι : Type u_1} (U : Finset ι) : chi U (zero ι) = 1

theorem AaronsonAmbainis.Row.chi_unit {ι : Type u_1} [DecidableEq ι] (U : Finset ι) (b : ι) : chi U (unit b) = if b ∈ U then -1 else 1

theorem AaronsonAmbainis.Row.sgn_flipSet {ι : Type u_1} [DecidableEq ι] (x : Cube ι) (U : Finset ι) (i : ι) : sgn (flipSet x U i) = sgn (x i) * if i ∈ U then -1 else 1

The sign of a coordinate of a flipped point.

theorem AaronsonAmbainis.Row.chi_flipSet {ι : Type u_1} [DecidableEq ι] (T U : Finset ι) (x : Cube ι) : chi T (flipSet x U) = ∏ i ∈ T, sgn (x i) * if i ∈ U then -1 else 1

The character at a flipped point.

theorem AaronsonAmbainis.Row.chi_mul_chi {ι : Type u_1} [Finite ι] [DecidableEq ι] (S T : Finset ι) (x : Cube ι) : chi S x * chi T x = chi (symmDiff S T) x

Characters multiply by symmetric difference.