The Chebyshev gadget

The function G of the proof of the block inequality (Lemma 6.4 of the paper). For blocks S b ⊆ ι (b : β), a point x and coefficients a_T: cnt S i w = #{b : i ∈ S b, w b = true}, gate S m c i w = T_m (1 - c * cnt S i w) and gadget a x S m c w = ∑_T a_T ∏_{i ∈ T} (sgn (x i) * gate S m c i w). In the paper these are written cnt_i(w), θ_i(w) and G(w).

The lemmas abs_gadget_le_one, hasDegreeLE_gadget, gadget_zero and gadget_unit are the properties (a)–(d) of G in that proof, each under the hypotheses it needs: G is bounded by 1, it has degree at most d * m, and it takes the value ∑_T a_T chi_T(x) at Row.zero β and, for m ≥ 1 and c = 1 - cos (π / m), the value ∑_T a_T chi_T(x^{S b}) at Row.unit b.

noncomputable def AaronsonAmbainis.Row.cnt {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (i : ι) (w : Cube β) : ℝ

cnt_i(w): the number of blocks b ∋ i with w b = true, as a real number.

Equations

• AaronsonAmbainis.Row.cnt S i w = ∑ b : β with i ∈ S b, if w b = true then 1 else 0

noncomputable def AaronsonAmbainis.Row.gate {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (m : ℕ) (c : ℝ) (i : ι) (w : Cube β) : ℝ

θ_i(w) = T_m (1 - c cnt_i(w)).

Equations

• AaronsonAmbainis.Row.gate S m c i w = Polynomial.eval (1 - c * AaronsonAmbainis.Row.cnt S i w) (Polynomial.Chebyshev.T ℝ ↑m)

noncomputable def AaronsonAmbainis.Row.gadget {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [Fintype β] (a : Finset ι → ℝ) (x : Cube ι) (S : β → Finset ι) (m : ℕ) (c : ℝ) (w : Cube β) : ℝ

G(w) = ∑_T a_T ∏_{i ∈ T} (sgn (x i) θ_i(w)).

Equations

• AaronsonAmbainis.Row.gadget a x S m c w = ∑ T : Finset ι, a T * ∏ i ∈ T, AaronsonAmbainis.Row.sgn (x i) * AaronsonAmbainis.Row.gate S m c i w

theorem AaronsonAmbainis.Row.cnt_nonneg {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (i : ι) (w : Cube β) : 0 ≤ cnt S i w

theorem AaronsonAmbainis.Row.cnt_le {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (N : ℕ) (hN : ∀ (i : ι), {b : β | i ∈ S b}.card ≤ N) (i : ι) (w : Cube β) : cnt S i w ≤ ↑N

theorem AaronsonAmbainis.Row.cnt_zero {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (i : ι) : cnt S i (zero β) = 0

theorem AaronsonAmbainis.Row.cnt_unit {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] [DecidableEq β] (S : β → Finset ι) (i : ι) (b : β) : cnt S i (unit b) = if i ∈ S b then 1 else 0

theorem AaronsonAmbainis.Row.hasDegreeLE_cnt {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (i : ι) : HasDegreeLE (cnt S i) 1

theorem AaronsonAmbainis.Row.abs_gate_le_one {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (N m : ℕ) (c : ℝ) (hc : 0 ≤ c) (hN : ∀ (i : ι), {b : β | i ∈ S b}.card ≤ N) (hNc : ↑N * c ≤ 2) (i : ι) (w : Cube β) : |gate S m c i w| ≤ 1

theorem AaronsonAmbainis.Row.hasDegreeLE_gate {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (m : ℕ) (c : ℝ) (i : ι) : HasDegreeLE (gate S m c i) m

theorem AaronsonAmbainis.Row.gate_zero {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] (S : β → Finset ι) (m : ℕ) (c : ℝ) (i : ι) : gate S m c i (zero β) = 1

theorem AaronsonAmbainis.Row.gate_unit {ι : Type u_1} [DecidableEq ι] {β : Type u_2} [Fintype β] [DecidableEq β] (S : β → Finset ι) (m : ℕ) (hm : 0 < m) (i : ι) (b : β) : gate S m (1 - Real.cos (Real.pi / ↑m)) i (unit b) = if i ∈ S b then -1 else 1

theorem AaronsonAmbainis.Row.abs_gadget_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [Fintype β] (a : Finset ι → ℝ) (ha : ∀ (z : Cube ι), |∑ T : Finset ι, a T * chi T z| ≤ 1) (x : Cube ι) (S : β → Finset ι) (N m : ℕ) (c : ℝ) (hc : 0 ≤ c) (hN : ∀ (i : ι), {b : β | i ∈ S b}.card ≤ N) (hNc : ↑N * c ≤ 2) (w : Cube β) : |gadget a x S m c w| ≤ 1

theorem AaronsonAmbainis.Row.hasDegreeLE_gadget {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [Fintype β] (a : Finset ι → ℝ) (d : ℕ) (ha : ∀ (T : Finset ι), d < T.card → a T = 0) (x : Cube ι) (S : β → Finset ι) (m : ℕ) (c : ℝ) : HasDegreeLE (gadget a x S m c) (d * m)

theorem AaronsonAmbainis.Row.gadget_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [Fintype β] (a : Finset ι → ℝ) (x : Cube ι) (S : β → Finset ι) (m : ℕ) (c : ℝ) : gadget a x S m c (zero β) = ∑ T : Finset ι, a T * chi T x

theorem AaronsonAmbainis.Row.gadget_unit {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [Fintype β] [DecidableEq β] (a : Finset ι → ℝ) (x : Cube ι) (S : β → Finset ι) (m : ℕ) (hm : 0 < m) (b : β) : gadget a x S m (1 - Real.cos (Real.pi / ↑m)) (unit b) = ∑ T : Finset ι, a T * chi T (flipSet x (S b))