The quantum query lower bound for search

A quantum query algorithm with T queries to x : Fin N → Bool alternates T + 1 arbitrary linear isometries U₀, …, U_T of a finite-dimensional state space ℂ^{Fin N × Bool × W}, with a query register, a control bit and a workspace W, with T applications of the controlled phase oracle O_x |i, b, w⟩ = (-1)^{b · x_i} |i, b, w⟩ (Cslib.Quantum.phaseOracle, Cslib.Quantum.run). Up to Hadamard gates on the control bit this is the standard bit oracle |i, b⟩ ↦ |i, b ⊕ x_i⟩, so the model is the standard one of Bennett, Bernstein, Brassard, Vazirani. Its output is the measurement of the query register: the probability of outcome i is ∑_{b, w} |ψ(i, b, w)|² (Cslib.Quantum.regProb).

Bennett–Bernstein–Brassard–Vazirani. Searching for a single marked item among N takes Ω(√N) queries: if, for every z, the algorithm outputs z with probability at least 2 / 3 on the input e_z marking only z, then N - 2 ≤ 144 T² (Cslib.Quantum.card_sub_two_le) Bennett, Bernstein, Brassard, Vazirani.

The proof is the hybrid argument. On the all-zero input the oracle is the identity; replacing it by O_{e_z} at one query moves the state by 2 ‖Π_z φ‖, where Π_z projects onto query index z with control bit 1 (Cslib.Quantum.ctrlProj) and φ is the state before that query. So the final states differ by at most 2 ∑_{t < T} ‖Π_z φ_t‖, and by Cauchy–Schwarz and ∑_z ‖Π_z φ‖² ≤ ‖φ‖² = 1, ∑_z ‖ψ_T^{e_z} - ψ_T^0‖² ≤ 4 T² (Cslib.Quantum.sum_sq_norm_run_sub_le). Success on e_z but not on the all-zero input, for all but at most two z, forces each of these distances to be at least 1 / 6.

Main definitions

• Cslib.Quantum.phaseOracle: the controlled phase oracle of x.
• Cslib.Quantum.run: the state of a query algorithm after t queries.
• Cslib.Quantum.regProb: the probability of measuring query index i.
• Cslib.Quantum.ctrlProj: the projection onto query index z with control bit 1.

Main results

• Cslib.Quantum.norm_run_sub_le: the hybrid argument for one marked item.
• Cslib.Quantum.sum_sq_norm_run_sub_le: ∑_z ‖ψ_T^{e_z} - ψ_T^0‖² ≤ 4 T².
• Cslib.Quantum.card_sub_two_le: the BBBV lower bound N - 2 ≤ 144 T².

References

• C. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and Weaknesses of Quantum Computing

@[reducible, inline]

abbrev Cslib.Quantum.State (N : ℕ) (W : Type u_2) : Type u_2

The state space ℂ^{Fin N × Bool × W} of a query algorithm: a query register, a control bit and a workspace.

noncomputable def Cslib.Quantum.phaseOracle {N : ℕ} {W : Type u_1} (x : Fin N → Bool) : State N W →ₗ[ℂ] State N W

The controlled phase oracle of x : Fin N → Bool: |i, b, w⟩ ↦ (-1)^{b · x_i} |i, b, w⟩.

@[simp]

theorem Cslib.Quantum.phaseOracle_apply {N : ℕ} {W : Type u_1} (x : Fin N → Bool) (ψ : State N W) (p : Fin N × Bool × W) : ((phaseOracle x) ψ).ofLp p = (if (p.2.1 && x p.1) = true then -1 else 1) * ψ.ofLp p

theorem Cslib.Quantum.norm_phaseOracle {N : ℕ} {W : Type u_1} [Fintype W] (x : Fin N → Bool) (ψ : State N W) : ‖(phaseOracle x) ψ‖ = ‖ψ‖

The phase oracle preserves norms.

@[simp]

theorem Cslib.Quantum.phaseOracle_zero {N : ℕ} {W : Type u_1} (ψ : State N W) : (phaseOracle fun (x : Fin N) => false) ψ = ψ

The oracle of the all-zero input is the identity.

noncomputable def Cslib.Quantum.run {N : ℕ} {W : Type u_1} [Fintype W] (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (x : Fin N → Bool) : ℕ → State N W

The state after t queries of the algorithm with isometries U and initial state ψ₀ on input x: U_t O_x U_{t-1} ⋯ O_x U_0 ψ₀.

theorem Cslib.Quantum.norm_run {N : ℕ} {W : Type u_1} [Fintype W] (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (x : Fin N → Bool) (t : ℕ) : ‖run U ψ₀ x t‖ = ‖ψ₀‖

Query algorithms preserve norms.

noncomputable def Cslib.Quantum.regProb {N : ℕ} {W : Type u_1} [Fintype W] (ψ : State N W) (i : Fin N) : ℝ

The probability of measuring query index i in the state ψ: the probability (Cslib.Quantum.measureProb) that measuring ψ gives an outcome (i, b, w).

theorem Cslib.Quantum.regProb_eq_sum {N : ℕ} {W : Type u_1} [Fintype W] (ψ : State N W) (i : Fin N) : regProb ψ i = ∑ w : Bool × W, ‖ψ.ofLp (i, w)‖ ^ 2

The probability of measuring query index i is ∑_{b, w} |ψ(i, b, w)|².

noncomputable def Cslib.Quantum.proj {N : ℕ} {W : Type u_1} (z : Fin N) (ψ : State N W) : State N W

The projection Π_z onto query index z.

theorem Cslib.Quantum.norm_sq_proj {N : ℕ} {W : Type u_1} [Fintype W] (z : Fin N) (ψ : State N W) : ‖proj z ψ‖ ^ 2 = regProb ψ z

theorem Cslib.Quantum.proj_sub {N : ℕ} {W : Type u_1} (z : Fin N) (ψ φ : State N W) : proj z (ψ - φ) = proj z ψ - proj z φ

theorem Cslib.Quantum.norm_proj_le {N : ℕ} {W : Type u_1} [Fintype W] (z : Fin N) (ψ : State N W) : ‖proj z ψ‖ ≤ ‖ψ‖

theorem Cslib.Quantum.sum_regProb {N : ℕ} {W : Type u_1} [Fintype W] (ψ : State N W) : ∑ i : Fin N, regProb ψ i = ‖ψ‖ ^ 2

The measurement probabilities of all query indices sum to ‖ψ‖².

noncomputable def Cslib.Quantum.ctrlProj {N : ℕ} {W : Type u_1} (z : Fin N) (ψ : State N W) : State N W

The projection onto query index z with control bit 1: the part of the state the oracle of e_z acts on.

theorem Cslib.Quantum.norm_sq_ctrlProj_le {N : ℕ} {W : Type u_1} [Fintype W] (z : Fin N) (ψ : State N W) : ‖ctrlProj z ψ‖ ^ 2 ≤ regProb ψ z

def Cslib.Quantum.marked {N : ℕ} [DecidableEq (Fin N)] (z : Fin N) : Fin N → Bool

The input e_z marking only z.

theorem Cslib.Quantum.phaseOracle_marked_sub {N : ℕ} {W : Type u_1} [DecidableEq (Fin N)] (z : Fin N) (ψ : State N W) : (phaseOracle (marked z)) ψ - ψ = -2 • ctrlProj z ψ

Marking z changes a state by -2 Π_z.

theorem Cslib.Quantum.norm_run_sub_le {N : ℕ} {W : Type u_1} [Fintype W] [DecidableEq (Fin N)] (U : ℕ → State N W →ₗᵢ[ℂ] State N W) (ψ₀ : State N W) (z : Fin N) (t : ℕ) : ‖run U ψ₀ (marked z) t - run U ψ₀ (fun (x : Fin N) => false) t‖ ≤ 2 * ∑ s ∈ Finset.range t, ‖ctrlProj z (run U ψ₀ (fun (x : Fin N) => false) s)‖

The hybrid argument for one marked item: on the inputs e_z and 0, the states after t queries differ by at most 2 ∑_{s < t} ‖Π_z φ_s‖, where φ_s is the state on the all-zero input after s queries.

theorem Cslib.Quantum.sum_sq_norm_run_sub_le {N : ℕ} {W : Type u_1} [Fintype W] [DecidableEq (Fin N)] (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) : ∑ z : Fin N, ‖run U ψ₀ (marked z) T - run U ψ₀ (fun (x : Fin N) => false) T‖ ^ 2 ≤ 4 * ↑T ^ 2

The sum of squared distances: for a unit initial state, ∑_z ‖ψ_T^{e_z} - ψ_T^0‖² ≤ 4 T².

theorem Cslib.Quantum.regProb_sub_le {N : ℕ} {W : Type u_1} [Fintype W] {ψ φ : State N W} (hψ : ‖ψ‖ = 1) (hφ : ‖φ‖ = 1) (z : Fin N) : regProb ψ z - regProb φ z ≤ 2 * ‖ψ - φ‖

Two unit states assign probabilities to a query index that differ by at most twice their distance.

theorem Cslib.Quantum.card_sub_two_le {N : ℕ} {W : Type u_1} [Fintype W] [DecidableEq (Fin N)] (U : ℕ → State N W →ₗᵢ[ℂ] State N W) {ψ₀ : State N W} (hψ₀ : ‖ψ₀‖ = 1) (T : ℕ) (hsucc : ∀ (z : Fin N), 2 / 3 ≤ regProb (run U ψ₀ (marked z) T) z) : ↑N - 2 ≤ 144 * ↑T ^ 2

The BBBV lower bound for search Bennett, Bernstein, Brassard, Vazirani: if a T-query algorithm with a unit initial state outputs z with probability at least 2 / 3 on the input marking only z, for every z, then N - 2 ≤ 144 T².