The polynomial method for value and XOR query oracles

Ported from the corresponding upstream modules listed by the source sections below. References beginning with Source name these retained sections.

Real polynomials on the Boolean cube

The small algebra API behind the polynomial method (SourceQuantumPolynomialMethod):

• bit b, the 0/1 real value of a Boolean, and evalBool p a, the evaluation of a real multivariate polynomial at a Boolean point of the cube (any finite index type ι);
• select i P₀ P₁ = (1 − Xᵢ)·P₀ + Xᵢ·P₁, which on the cube evaluates to the polynomial selected by the i-th bit and raises the degree bound by one — the one operation an oracle query performs on an amplitude;
• AmpPoly ι, a pair of real polynomials representing the real and imaginary parts of a complex amplitude, with the complex-scalar action and sums needed to push an input-independent unitary through a representation. Working with two real polynomials avoids any coefficient-ring map: Complex.re is not a ring homomorphism.

Everything is stated for arbitrary finite ι, including Fin n.

Bits and evaluation

def QuantumQueryComplexity.bit (b : Bool) : ℝ

The real value of a Boolean: 1 for true, 0 for false.

Equations

• QuantumQueryComplexity.bit b = if b = true then 1 else 0

@[simp]

theorem QuantumQueryComplexity.bit_true : bit true = 1

@[simp]

theorem QuantumQueryComplexity.bit_false : bit false = 0

theorem QuantumQueryComplexity.bit_nonneg (b : Bool) : 0 ≤ bit b

theorem QuantumQueryComplexity.bit_le_one (b : Bool) : bit b ≤ 1

theorem QuantumQueryComplexity.one_sub_bit (b : Bool) : 1 - bit b = bit !b

noncomputable def QuantumQueryComplexity.evalBool {ι : Type u_1} (p : MvPolynomial ι ℝ) (a : ι → Bool) : ℝ

Evaluating a real multivariate polynomial at a Boolean point of the cube.

Equations

• QuantumQueryComplexity.evalBool p a = (MvPolynomial.eval fun (i : ι) => QuantumQueryComplexity.bit (a i)) p

@[simp]

theorem QuantumQueryComplexity.evalBool_C {ι : Type u_1} (c : ℝ) (a : ι → Bool) : evalBool (MvPolynomial.C c) a = c

@[simp]

theorem QuantumQueryComplexity.evalBool_X {ι : Type u_1} (i : ι) (a : ι → Bool) : evalBool (MvPolynomial.X i) a = bit (a i)

@[simp]

theorem QuantumQueryComplexity.evalBool_add {ι : Type u_1} (p q : MvPolynomial ι ℝ) (a : ι → Bool) : evalBool (p + q) a = evalBool p a + evalBool q a

@[simp]

theorem QuantumQueryComplexity.evalBool_sub {ι : Type u_1} (p q : MvPolynomial ι ℝ) (a : ι → Bool) : evalBool (p - q) a = evalBool p a - evalBool q a

@[simp]

theorem QuantumQueryComplexity.evalBool_neg {ι : Type u_1} (p : MvPolynomial ι ℝ) (a : ι → Bool) : evalBool (-p) a = -evalBool p a

@[simp]

theorem QuantumQueryComplexity.evalBool_mul {ι : Type u_1} (p q : MvPolynomial ι ℝ) (a : ι → Bool) : evalBool (p * q) a = evalBool p a * evalBool q a

@[simp]

theorem QuantumQueryComplexity.evalBool_pow {ι : Type u_1} (p : MvPolynomial ι ℝ) (k : ℕ) (a : ι → Bool) : evalBool (p ^ k) a = evalBool p a ^ k

@[simp]

theorem QuantumQueryComplexity.evalBool_zero {ι : Type u_1} (a : ι → Bool) : evalBool 0 a = 0

@[simp]

theorem QuantumQueryComplexity.evalBool_one {ι : Type u_1} (a : ι → Bool) : evalBool 1 a = 1

theorem QuantumQueryComplexity.evalBool_sum {ι : Type u_1} {κ : Type u_2} (s : Finset κ) (p : κ → MvPolynomial ι ℝ) (a : ι → Bool) : evalBool (∑ k ∈ s, p k) a = ∑ k ∈ s, evalBool (p k) a

Total-degree conveniences

theorem QuantumQueryComplexity.totalDegree_finsetSum_le {ι : Type u_1} {κ : Type u_2} (s : Finset κ) (p : κ → MvPolynomial ι ℝ) {d : ℕ} (h : ∀ k ∈ s, (p k).totalDegree ≤ d) : (∑ k ∈ s, p k).totalDegree ≤ d

theorem QuantumQueryComplexity.totalDegree_C_mul_le {ι : Type u_1} (c : ℝ) (p : MvPolynomial ι ℝ) : (MvPolynomial.C c * p).totalDegree ≤ p.totalDegree

theorem QuantumQueryComplexity.totalDegree_sq_le {ι : Type u_1} (p : MvPolynomial ι ℝ) {d : ℕ} (h : p.totalDegree ≤ d) : (p ^ 2).totalDegree ≤ 2 * d

The selector

noncomputable def QuantumQueryComplexity.select {ι : Type u_1} (i : ι) (P₀ P₁ : MvPolynomial ι ℝ) : MvPolynomial ι ℝ

select i P₀ P₁ = (1 − Xᵢ)·P₀ + Xᵢ·P₁: on the cube, P₁ where the i-th bit is set and P₀ where it is not.

Equations

• QuantumQueryComplexity.select i P₀ P₁ = (1 - MvPolynomial.X i) * P₀ + MvPolynomial.X i * P₁

theorem QuantumQueryComplexity.evalBool_select {ι : Type u_1} (i : ι) (P₀ P₁ : MvPolynomial ι ℝ) (a : ι → Bool) : evalBool (select i P₀ P₁) a = if a i = true then evalBool P₁ a else evalBool P₀ a

theorem QuantumQueryComplexity.totalDegree_select_le {ι : Type u_1} (i : ι) {P₀ P₁ : MvPolynomial ι ℝ} {t : ℕ} (h₀ : P₀.totalDegree ≤ t) (h₁ : P₁.totalDegree ≤ t) : (select i P₀ P₁).totalDegree ≤ t + 1

Amplitude polynomials

A complex amplitude, as a function of the input, is represented by two real polynomials: its real and its imaginary part.

structure QuantumQueryComplexity.AmpPoly (ι : Type u_2) : Type u_2

A pair of real polynomials, standing for re + im·I.

• re : MvPolynomial ι ℝ

  The real part.

• im : MvPolynomial ι ℝ

  The imaginary part.

noncomputable def QuantumQueryComplexity.AmpPoly.evalC {ι : Type u_1} (P : AmpPoly ι) (a : ι → Bool) : ℂ

The complex value at a Boolean point.

Equations

• P.evalC a = { re := QuantumQueryComplexity.evalBool P.re a, im := QuantumQueryComplexity.evalBool P.im a }

@[simp]

theorem QuantumQueryComplexity.AmpPoly.evalC_re {ι : Type u_1} (P : AmpPoly ι) (a : ι → Bool) : (P.evalC a).re = evalBool P.re a

@[simp]

theorem QuantumQueryComplexity.AmpPoly.evalC_im {ι : Type u_1} (P : AmpPoly ι) (a : ι → Bool) : (P.evalC a).im = evalBool P.im a

def QuantumQueryComplexity.AmpPoly.DegLe {ι : Type u_1} (P : AmpPoly ι) (t : ℕ) : Prop

Both parts have total degree at most t.

Equations

• P.DegLe t = (P.re.totalDegree ≤ t ∧ P.im.totalDegree ≤ t)

theorem QuantumQueryComplexity.AmpPoly.DegLe.mono {ι : Type u_1} {P : AmpPoly ι} {s t : ℕ} (h : P.DegLe s) (hst : s ≤ t) : P.DegLe t

noncomputable def QuantumQueryComplexity.AmpPoly.const {ι : Type u_1} (z : ℂ) : AmpPoly ι

The constant amplitude z.

Equations

• QuantumQueryComplexity.AmpPoly.const z = { re := MvPolynomial.C z.re, im := MvPolynomial.C z.im }

@[simp]

theorem QuantumQueryComplexity.AmpPoly.evalC_const {ι : Type u_1} (z : ℂ) (a : ι → Bool) : (const z).evalC a = z

theorem QuantumQueryComplexity.AmpPoly.degLe_const {ι : Type u_1} (z : ℂ) (t : ℕ) : (const z).DegLe t

noncomputable def QuantumQueryComplexity.AmpPoly.cmul {ι : Type u_1} (z : ℂ) (P : AmpPoly ι) : AmpPoly ι

Multiplication by a fixed complex scalar z: (x + y I)(re + im I) = (x·re − y·im) + (y·re + x·im) I.

Equations

• QuantumQueryComplexity.AmpPoly.cmul z P = { re := MvPolynomial.C z.re * P.re - MvPolynomial.C z.im * P.im, im := MvPolynomial.C z.im * P.re + MvPolynomial.C z.re * P.im }

@[simp]

theorem QuantumQueryComplexity.AmpPoly.evalC_cmul {ι : Type u_1} (P : AmpPoly ι) (z : ℂ) (a : ι → Bool) : (cmul z P).evalC a = z * P.evalC a

theorem QuantumQueryComplexity.AmpPoly.degLe_cmul {ι : Type u_1} (P : AmpPoly ι) (z : ℂ) {t : ℕ} (h : P.DegLe t) : (cmul z P).DegLe t

noncomputable def QuantumQueryComplexity.AmpPoly.sum {ι : Type u_1} {κ : Type u_2} (s : Finset κ) (P : κ → AmpPoly ι) : AmpPoly ι

The sum of a finite family.

Equations

• QuantumQueryComplexity.AmpPoly.sum s P = { re := ∑ k ∈ s, (P k).re, im := ∑ k ∈ s, (P k).im }

@[simp]

theorem QuantumQueryComplexity.AmpPoly.evalC_sum {ι : Type u_1} {κ : Type u_2} (s : Finset κ) (P : κ → AmpPoly ι) (a : ι → Bool) : (sum s P).evalC a = ∑ k ∈ s, (P k).evalC a

theorem QuantumQueryComplexity.AmpPoly.degLe_sum {ι : Type u_1} {κ : Type u_2} (s : Finset κ) (P : κ → AmpPoly ι) {t : ℕ} (h : ∀ k ∈ s, (P k).DegLe t) : (sum s P).DegLe t

noncomputable def QuantumQueryComplexity.AmpPoly.select {ι : Type u_1} (i : ι) (P₀ P₁ : AmpPoly ι) : AmpPoly ι

The selector, applied to both parts.

Equations

• QuantumQueryComplexity.AmpPoly.select i P₀ P₁ = { re := QuantumQueryComplexity.select i P₀.re P₁.re, im := QuantumQueryComplexity.select i P₀.im P₁.im }

theorem QuantumQueryComplexity.AmpPoly.evalC_select {ι : Type u_1} (i : ι) (P₀ P₁ : AmpPoly ι) (a : ι → Bool) : (select i P₀ P₁).evalC a = if a i = true then P₁.evalC a else P₀.evalC a

theorem QuantumQueryComplexity.AmpPoly.degLe_select {ι : Type u_1} (i : ι) {P₀ P₁ : AmpPoly ι} {t : ℕ} (h₀ : P₀.DegLe t) (h₁ : P₁.DegLe t) : (select i P₀ P₁).DegLe (t + 1)

noncomputable def QuantumQueryComplexity.AmpPoly.normSqPoly {ι : Type u_1} (P : AmpPoly ι) : MvPolynomial ι ℝ

The squared modulus re² + im², a real polynomial of twice the degree.

Equations

• P.normSqPoly = P.re ^ 2 + P.im ^ 2

theorem QuantumQueryComplexity.AmpPoly.evalBool_normSqPoly {ι : Type u_1} (P : AmpPoly ι) (a : ι → Bool) : evalBool P.normSqPoly a = Complex.normSq (P.evalC a)

theorem QuantumQueryComplexity.AmpPoly.totalDegree_normSqPoly_le {ι : Type u_1} (P : AmpPoly ι) {t : ℕ} (h : P.DegLe t) : P.normSqPoly.totalDegree ≤ 2 * t

The polynomial method (Beals–Buhrman–Cleve–Mosca–de Wolf)

A quantum algorithm making t queries to a Boolean input has, at every basis state, an amplitude whose real and imaginary parts are real polynomials of total degree at most t in the input bits; its acceptance probabilities are therefore polynomials of degree at most 2·t. This is Lemmas 4.1 and 4.2 of Quantum Lower Bounds by Polynomials (arXiv:quant-ph/9802049), proved here from the operational model of SourceQuantumAlgorithm.

The induction is stated once, for an arbitrary finite basis B and any oracle whose action on a basis state is either input-independent or selected by one input bit (HasAmpPoly.selector); the native value oracle (oracleMap) and the XOR oracle (SourceQuantumXorPolynomialMethod) are two instances. No query simulation between the models is used, so both get the degree bound 2·t, never 4·t.

Main statements:

• QAlg.hasAmpPoly_state: the amplitudes after t queries have degree ≤ t;
• QAlg.exists_probability_polynomial: output probabilities have degree at most 2·t;
• QAlg.exists_event_polynomial: the same for the probability of a set of outputs;
• ComputesWithErrorOn.exists_approx_polynomial: a t-query algorithm computing a Boolean f on a promise with error ε yields a degree-≤ 2t polynomial within ε of bit ∘ f on the promise, with values in [0, 1] on the whole cube.

Representations of input-dependent vectors

def QuantumQueryComplexity.Represents {ι B : Type} (Φ : B → AmpPoly ι) (φ : (ι → Bool) → B → ℂ) (t : ℕ) : Prop

Represents Φ φ t: the amplitude polynomials Φ b represent the input-dependent vector φ, with both parts of degree at most t.

Equations

• QuantumQueryComplexity.Represents Φ φ t = ((∀ (b : B), (Φ b).DegLe t) ∧ ∀ (a : ι → Bool) (b : B), (Φ b).evalC a = φ a b)

def QuantumQueryComplexity.HasAmpPoly {ι B : Type} (φ : (ι → Bool) → B → ℂ) (t : ℕ) : Prop

φ has a representation of degree at most t.

Equations

• QuantumQueryComplexity.HasAmpPoly φ t = ∃ (Φ : B → QuantumQueryComplexity.AmpPoly ι), QuantumQueryComplexity.Represents Φ φ t

theorem QuantumQueryComplexity.hasAmpPoly_const {ι B : Type} (v : B → ℂ) : HasAmpPoly (fun (x : ι → Bool) => v) 0

theorem QuantumQueryComplexity.HasAmpPoly.mono {ι B : Type} {φ : (ι → Bool) → B → ℂ} {t : ℕ} (h : HasAmpPoly φ t) {t' : ℕ} (htt : t ≤ t') : HasAmpPoly φ t'

theorem QuantumQueryComplexity.HasAmpPoly.mulVec {ι B : Type} {φ : (ι → Bool) → B → ℂ} {t : ℕ} [Fintype B] (U : Matrix B B ℂ) (h : HasAmpPoly φ t) : HasAmpPoly (fun (a : ι → Bool) => U.mulVec (φ a)) t

An input-independent linear map preserves the degree bound.

theorem QuantumQueryComplexity.HasAmpPoly.selector {ι B : Type} {φ : (ι → Bool) → B → ℂ} {t : ℕ} (orc : (ι → Bool) → B → B) (horc : ∀ (p : B), (∀ (a : ι → Bool), orc a p = p) ∨ ∃ (i : ι) (p₀ : B) (p₁ : B), ∀ (a : ι → Bool), orc a p = if a i = true then p₁ else p₀) (h : HasAmpPoly φ t) : HasAmpPoly (fun (a : ι → Bool) (p : B) => φ a (orc a p)) (t + 1)

A selector oracle raises the degree bound by one. An oracle whose action on each basis state is either input-independent or the choice between two fixed basis states made by one input bit.

From amplitudes to probabilities

theorem QuantumQueryComplexity.HasAmpPoly.exists_qProb_polynomial {ι B : Type} {φ : (ι → Bool) → B → ℂ} {t : ℕ} {O : Type} [DecidableEq O] [Fintype B] (h : HasAmpPoly φ t) (rd : B → O) (o : O) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ∀ (a : ι → Bool), evalBool p a = qProb rd (φ a) o

The probability polynomial: the measured probability of an output is a real polynomial of degree at most 2·t.

theorem QuantumQueryComplexity.HasAmpPoly.exists_event_polynomial {ι B : Type} {φ : (ι → Bool) → B → ℂ} {t : ℕ} {O : Type} [DecidableEq O] [Fintype B] (h : HasAmpPoly φ t) (rd : B → O) (E : Finset O) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ∀ (a : ι → Bool), evalBool p a = ∑ o ∈ E, qProb rd (φ a) o

The probability of an event (a finite set of outputs).

The native value oracle

theorem QuantumQueryComplexity.oracleMap_selector {ι W : Type} (p : QBasis ι Bool W) : (∀ (a : ι → Bool), oracleMap a p = p) ∨ ∃ (i : ι) (p₀ : QBasis ι Bool W) (p₁ : QBasis ι Bool W), ∀ (a : ι → Bool), oracleMap a p = if a i = true then p₁ else p₀

The native oracle is a selector oracle: idle on index none, and at index some i a swap determined by the bit a i.

theorem QuantumQueryComplexity.QAlg.hasAmpPoly_state {ι : Type} [Fintype ι] [DecidableEq ι] {O W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι Bool O W) (t : ℕ) : HasAmpPoly (fun (a : ι → Bool) => A.state a t) t

Amplitudes after t queries have degree at most t (BBCMW Lemma 4.1).

theorem QuantumQueryComplexity.QAlg.exists_probability_polynomial {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι Bool O W) (t : ℕ) (o : O) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ∀ (a : ι → Bool), evalBool p a = A.prob a t o

The polynomial method (BBCMW Lemma 4.2): the probability that a t-query algorithm announces o is a real polynomial of total degree at most 2·t in the input bits, exactly, on the whole Boolean cube.

theorem QuantumQueryComplexity.QAlg.exists_event_polynomial {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι Bool O W) (t : ℕ) (E : Finset O) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ∀ (a : ι → Bool), evalBool p a = ∑ o ∈ E, A.prob a t o

The probability of announcing an output in E.

Probability bounds on the whole cube

theorem QuantumQueryComplexity.qProb_le_one_of_isQState {O : Type} [DecidableEq O] {H : Type} [Fintype H] {rd : H → O} {ψ : H → ℂ} (hψ : IsQState ψ) (o : O) : qProb rd ψ o ≤ 1

The probability bound specialized to the polynomial-method interface.

theorem QuantumQueryComplexity.QAlg.prob_le_one' {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {W : Type} [Fintype W] [DecidableEq W] (A : QAlg ι Bool O W) (a : ι → Bool) (t : ℕ) (o : O) : A.prob a t o ≤ 1

theorem QuantumQueryComplexity.QAlg.sum_prob_eq_one {ι : Type} [Fintype ι] [DecidableEq ι] {O : Type} [DecidableEq O] {W : Type} [Fintype W] [DecidableEq W] [Fintype O] (A : QAlg ι Bool O W) (a : ι → Bool) (t : ℕ) : ∑ o : O, A.prob a t o = 1

With finitely many outputs the output polynomials sum to 1 on the cube.

Correctness: the acceptance polynomial approximates the function

def QuantumQueryComplexity.ApproximatesOn {ι X : Type} (p : MvPolynomial ι ℝ) (read : X → ι → Bool) (f : X → Bool) (ε : ℝ) : Prop

p approximates the Boolean function f on the promise read within ε.

Equations

• QuantumQueryComplexity.ApproximatesOn p read f ε = ∀ (x : X), |QuantumQueryComplexity.evalBool p (read x) - QuantumQueryComplexity.bit (f x)| ≤ ε

theorem QuantumQueryComplexity.abs_qProb_true_sub_bit_le {H : Type} [Fintype H] {rd : H → Bool} {ψ : H → ℂ} (hψ : IsQState ψ) {b : Bool} {ε : ℝ} (h : 1 - ε ≤ qProb rd ψ b) : |qProb rd ψ true - bit b| ≤ ε

Two probabilities of a Boolean-output algorithm: correctness on true and on false, translated into a two-sided bound on the acceptance probability.

theorem QuantumQueryComplexity.ComputesWithErrorOn.abs_prob_sub_bit_le {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {X : Type} {A : QAlg ι Bool Bool W} {t : ℕ} {read : X → ι → Bool} {f : X → Bool} {ε : ℝ} (h : ComputesWithErrorOn A t read f ε) (x : X) : |A.prob (read x) t true - bit (f x)| ≤ ε

Correctness transfers to the polynomial.

theorem QuantumQueryComplexity.ComputesWithErrorOn.exists_approx_polynomial {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {X : Type} {A : QAlg ι Bool Bool W} {t : ℕ} {read : X → ι → Bool} {f : X → Bool} {ε : ℝ} (h : ComputesWithErrorOn A t read f ε) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ApproximatesOn p read f ε ∧ ∀ (a : ι → Bool), 0 ≤ evalBool p a ∧ evalBool p a ≤ 1

The approximating polynomial of a bounded-error algorithm: degree at most 2·t, within ε of bit ∘ f on the promise, and with values in [0, 1] on the entire cube.

The polynomial method for the XOR oracle

The same induction as SourceQuantumPolynomialMethod, run on the XOR-oracle semantics xorState of SourceQuantumXorOracle. The XOR oracle is again a selector oracle (idle at index none; at index some i the answer register is XORed with the bit a i), so the shared lemma HasAmpPoly.selector applies directly and the degree bound is 2·t — the model simulation of SourceQuantumSimulation is not used, which would have cost a factor two.

theorem QuantumQueryComplexity.xorOracleMap_selector {ι W : Type} (p : QBasis ι Bool W) : (∀ (a : ι → Bool), xorOracleMap a p = p) ∨ ∃ (i : ι) (p₀ : QBasis ι Bool W) (p₁ : QBasis ι Bool W), ∀ (a : ι → Bool), xorOracleMap a p = if a i = true then p₁ else p₀

The XOR oracle is a selector oracle.

theorem QuantumQueryComplexity.hasAmpPoly_xorState {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {O : Type} (A : QAlg ι Bool O W) (t : ℕ) : HasAmpPoly (fun (a : ι → Bool) => xorState A a t) t

XOR amplitudes after t queries have degree at most t.

theorem QuantumQueryComplexity.exists_xor_probability_polynomial {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {O : Type} [DecidableEq O] (A : QAlg ι Bool O W) (t : ℕ) (o : O) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ∀ (a : ι → Bool), evalBool p a = qProb A.readout (xorState A a t) o

The polynomial method, XOR oracle: the acceptance probability after t XOR queries is a real polynomial of total degree at most 2·t.

theorem QuantumQueryComplexity.exists_xor_event_polynomial {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {O : Type} [DecidableEq O] (A : QAlg ι Bool O W) (t : ℕ) (E : Finset O) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ∀ (a : ι → Bool), evalBool p a = ∑ o ∈ E, qProb A.readout (xorState A a t) o

The probability of an event, XOR oracle.

theorem QuantumQueryComplexity.XorComputesWithErrorOn.abs_prob_sub_bit_le {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {X : Type} {A : QAlg ι Bool Bool W} {t : ℕ} {read : X → ι → Bool} {f : X → Bool} {ε : ℝ} (h : XorComputesWithErrorOn A t read f ε) (x : X) : |qProb A.readout (xorState A (read x) t) true - bit (f x)| ≤ ε

Correctness transfers to the polynomial, XOR oracle.

theorem QuantumQueryComplexity.XorComputesWithErrorOn.exists_approx_polynomial {ι : Type} [Fintype ι] [DecidableEq ι] {W : Type} [Fintype W] [DecidableEq W] {X : Type} {A : QAlg ι Bool Bool W} {t : ℕ} {read : X → ι → Bool} {f : X → Bool} {ε : ℝ} (h : XorComputesWithErrorOn A t read f ε) : ∃ (p : MvPolynomial ι ℝ), p.totalDegree ≤ 2 * t ∧ ApproximatesOn p read f ε ∧ ∀ (a : ι → Bool), 0 ≤ evalBool p a ∧ evalBool p a ≤ 1

The approximating polynomial of a bounded-error XOR algorithm.