diff --git a/Complexity.lean b/Complexity.lean index 31eb4892de..454af6bad3 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1244,6 +1244,7 @@ public import Complexity.Computability.QueryComplexity.Huang public import Complexity.Computability.QueryComplexity.Monotone public import Complexity.Computability.QueryComplexity.NisanSzegedy public import Complexity.Computability.QueryComplexity.OneSided +public import Complexity.Computability.QueryComplexity.Quantum.Grover public import Complexity.Computability.QueryComplexity.Quantum.Search public import Complexity.Computability.QueryComplexity.Randomized public import Complexity.Computability.QueryComplexity.Randomized.Nisan diff --git a/Complexity/Computability/QueryComplexity/Quantum/Grover.lean b/Complexity/Computability/QueryComplexity/Quantum/Grover.lean new file mode 100644 index 0000000000..c3242279b8 --- /dev/null +++ b/Complexity/Computability/QueryComplexity/Quantum/Grover.lean @@ -0,0 +1,281 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.QueryComplexity.Quantum.Search +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds + +/-! +# Grover's algorithm + +Grover's algorithm finds the marked item among `N ≥ 2` with `O(√N)` queries, matching the BBBV +lower bound (`Cslib.Quantum.card_sub_two_le`) up to a constant [Grover][Grover1996]. In the query +model of `Cslib.Quantum.run`, with a trivial workspace, it starts in the uniform superposition +`|s⟩` of the query indices with control bit `1` (`Cslib.Quantum.uniform`) and alternates the +controlled phase oracle with the *diffusion* `D = 2|s⟩⟨s| - I`, the reflection about `|s⟩` +(`Cslib.Quantum.diffusion`, `Cslib.Quantum.grover`). The state never leaves the control-`1` +subspace, where the oracle acts as the phase oracle `(-1)^{x_i}`. + +Let `θ = arcsin(1 / √N)`. After `k` queries on the input marking `z`, the amplitude of `z` is +`sin((2k + 1) θ)` and every other amplitude with control bit `1` is `cos((2k + 1) θ) / √(N - 1)` +(`Cslib.Quantum.run_grover`): each round rotates the state by `2θ` in the plane spanned by `|z⟩` +and the uniform superposition of the other items. So `z` is measured with probability +`sin²((2k + 1) θ)` (`Cslib.Quantum.regProb_run_grover`). With `k = ⌊π / (4θ)⌋ ≤ π√N / 4` queries, +`(2k + 1) θ` lies within `θ` of `π / 2`, and the success probability is at least `1 - 1 / N` +(`Cslib.Quantum.grover_success`). + +## Main definitions + +* `Cslib.Quantum.uniform`: the uniform superposition. +* `Cslib.Quantum.diffusion`: the reflection about the uniform superposition. +* `Cslib.Quantum.grover`: the isometries of Grover's algorithm. + +## Main results + +* `Cslib.Quantum.run_grover`: the state of Grover's algorithm after `k` queries. +* `Cslib.Quantum.regProb_run_grover`: its success probability `sin²((2k + 1) θ)`. +* `Cslib.Quantum.grover_success`: `⌊π / (4θ)⌋ ≤ π√N / 4` queries find the marked item with + probability at least `1 - 1 / N`. + +## References + +* [L. K. Grover, *A Fast Quantum Mechanical Algorithm for Database Search*][Grover1996] +-/ + +@[expose] public section + +namespace Cslib.Quantum + +open Finset Real + +variable {N : ℕ} + +/-- The uniform superposition `|s⟩ = N^{-1/2} ∑_i |i, 1⟩` with control bit `1`. -/ +noncomputable def uniform (N : ℕ) : State N Unit := + WithLp.toLp 2 fun p => if p.2.1 then ((Real.sqrt N)⁻¹ : ℝ) else 0 + +theorem norm_uniform (hN : 0 < N) : ‖uniform N‖ = 1 := by + have h : ‖uniform N‖ ^ 2 = 1 := by + rw [EuclideanSpace.norm_sq_eq, Fintype.sum_prod_type] + simp only [Fintype.sum_prod_type, Fintype.sum_bool, Fintype.univ_unit, sum_singleton, uniform, + PiLp.toLp_apply, ite_true, Bool.false_eq_true, ite_false, norm_zero, Complex.norm_real, + Real.norm_eq_abs, sq_abs] + rw [sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul, inv_pow, + Real.sq_sqrt (Nat.cast_nonneg N)] + field_simp + ring + nlinarith [norm_nonneg (uniform N)] + +/-- The **diffusion** `D = 2|s⟩⟨s| - I`: the reflection about the uniform superposition. -/ +noncomputable def diffusion (N : ℕ) : State N Unit ≃ₗᵢ[ℂ] State N Unit := + (ℂ ∙ uniform N).reflection + +/-- The diffusion inverts every control-`1` amplitude about their mean: +`(Dψ)(i, b) = 2 b · mean_j ψ(j, 1) - ψ(i, b)`. -/ +theorem diffusion_apply (hN : 0 < N) (ψ : State N Unit) (p : Fin N × Bool × Unit) : + (diffusion N ψ).ofLp p = + 2 * (if p.2.1 then (N : ℂ)⁻¹ * ∑ q, (if q.2.1 then ψ.ofLp q else 0) else 0) - ψ.ofLp p := by + rw [diffusion, Submodule.reflection_apply, Submodule.starProjection_singleton, + norm_uniform hN] + simp only [one_pow, PiLp.sub_apply, PiLp.smul_apply, + EuclideanSpace.inner_eq_star_dotProduct, uniform, smul_eq_mul, nsmul_eq_mul] + have hsq : ((Real.sqrt N : ℂ))⁻¹ * ((Real.sqrt N : ℂ))⁻¹ = (N : ℂ)⁻¹ := by + rw [← mul_inv, ← Complex.ofReal_mul, Real.mul_self_sqrt (Nat.cast_nonneg N)] + push_cast + ring + simp only [dotProduct, Pi.star_apply, RCLike.star_def, apply_ite, Complex.conj_ofReal, map_zero] + push_cast + rw [div_one] + have hdot : (∑ q : Fin N × Bool × Unit, + if q.2.1 then ψ.ofLp q * ((Real.sqrt N : ℂ))⁻¹ else ψ.ofLp q * 0) = + ((Real.sqrt N : ℂ))⁻¹ * ∑ q, (if q.2.1 then ψ.ofLp q else 0) := by + rw [mul_sum] + refine sum_congr rfl fun q _ => ?_ + split_ifs <;> ring + rw [hdot] + split_ifs + · linear_combination (2 * ∑ q : Fin N × Bool × Unit, (if q.2.1 then ψ.ofLp q else 0)) * hsq + · ring + +/-- The isometries of **Grover's algorithm**: the identity, then the diffusion after every +query. Its initial state is `uniform N`. -/ +noncomputable def grover (N : ℕ) : ℕ → State N Unit →ₗᵢ[ℂ] State N Unit + | 0 => LinearIsometry.id + | _ + 1 => (diffusion N).toLinearIsometry + +/-- The Grover angle `θ = arcsin(1 / √N)`. -/ +noncomputable def groverAngle (N : ℕ) : ℝ := Real.arcsin (Real.sqrt N)⁻¹ + +/-- The sine and cosine of the Grover angle: `sin θ = 1 / √N` and `cos θ / √(N - 1) = 1 / √N`. -/ +private theorem sin_groverAngle (hN : 2 ≤ N) : Real.sin (groverAngle N) = (Real.sqrt N)⁻¹ := by + have hpos : (0 : ℝ) < Real.sqrt N := Real.sqrt_pos.mpr (by positivity) + have hle : (Real.sqrt N)⁻¹ ≤ 1 := by + rw [inv_le_one₀ hpos, Real.one_le_sqrt] + exact_mod_cast (by omega : 1 ≤ N) + exact Real.sin_arcsin (by linarith [inv_nonneg.mpr hpos.le]) hle + +private theorem cos_groverAngle (hN : 2 ≤ N) : + Real.cos (groverAngle N) = Real.sqrt (N - 1) * (Real.sqrt N)⁻¹ := by + have hN0 : (0 : ℝ) < N := by positivity + have hN1 : (0 : ℝ) ≤ N - 1 := by + have : (2 : ℝ) ≤ N := by exact_mod_cast hN + linarith + rw [groverAngle, Real.cos_arcsin, inv_pow, Real.sq_sqrt hN0.le, ← Real.sqrt_inv, + ← Real.sqrt_mul hN1] + congr 1 + field_simp + +variable [DecidableEq (Fin N)] + +/-- **The state of Grover's algorithm after `k` queries** on the input marking `z`: with control +bit `1`, amplitude `sin((2k + 1) θ)` on `z` and `cos((2k + 1) θ) / √(N - 1)` elsewhere; with +control bit `0`, amplitude `0`. -/ +theorem run_grover (hN : 2 ≤ N) (z : Fin N) (k : ℕ) (p : Fin N × Bool × Unit) : + (run (grover N) (uniform N) (marked z) k).ofLp p = + if p.2.1 then ((if p.1 = z then Real.sin ((2 * k + 1) * groverAngle N) + else Real.cos ((2 * k + 1) * groverAngle N) / Real.sqrt (N - 1) : ℝ) : ℂ) else 0 := by + have hN0 : (0 : ℝ) < N := by positivity + have hN1 : (0 : ℝ) < N - 1 := by + have : (2 : ℝ) ≤ N := by exact_mod_cast hN + linarith + have hsN : (0 : ℝ) < Real.sqrt N := Real.sqrt_pos.mpr hN0 + have hsN1 : (0 : ℝ) < Real.sqrt (N - 1) := Real.sqrt_pos.mpr hN1 + set θ := groverAngle N + have hs := sin_groverAngle hN + have hc := cos_groverAngle hN + induction k generalizing p with + | zero => + simp only [run, grover, LinearIsometry.id_apply, uniform, PiLp.toLp_apply, Nat.cast_zero, + mul_zero, zero_add, one_mul] + split_ifs + · rw [hs] + · rw [hc] + congr 1 + field_simp + · rfl + | succ k ih => + set a := Real.sin ((2 * k + 1) * θ) + set b := Real.cos ((2 * k + 1) * θ) / Real.sqrt (N - 1) + have hsum : ∑ q : Fin N × Bool × Unit, (if q.2.1 then (phaseOracle (marked z) + (run (grover N) (uniform N) (marked z) k)).ofLp q else 0) = + ((-a + (N - 1) * b : ℝ) : ℂ) := by + simp only [phaseOracle_apply, ih, marked, decide_eq_true_eq, Fintype.sum_prod_type, + Fintype.univ_unit, sum_singleton, Fintype.sum_bool, ite_true, Bool.true_and, + Bool.false_eq_true, ite_false, add_zero] + have hterm : ∀ x : Fin N, (if x = z then (-1 : ℂ) else 1) * + ((if x = z then a else b : ℝ) : ℂ) = + (b : ℂ) + (if x = z then ((-a - b : ℝ) : ℂ) else 0) := by + intro x + by_cases h : x = z <;> simp [h] + rw [sum_congr rfl fun x _ => hterm x, sum_add_distrib, sum_ite_eq', ite_eq_left (mem_univ z), + sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul] + push_cast + ring + have hX : (Real.sqrt (N - 1) * (Real.sqrt N)⁻¹) ^ 2 = (N - 1) * (N : ℝ)⁻¹ := by + rw [mul_pow, inv_pow, Real.sq_sqrt hN1.le, Real.sq_sqrt hN0.le] + have hS2 : (Real.sqrt N)⁻¹ * (Real.sqrt N)⁻¹ = (N : ℝ)⁻¹ := by + rw [← mul_inv, Real.mul_self_sqrt hN0.le] + have hNinv : (N : ℝ) * (N : ℝ)⁻¹ = 1 := mul_inv_cancel₀ hN0.ne' + have hcosx : Real.cos ((2 * k + 1) * θ) = b * Real.sqrt (N - 1) := by + simp only [b] + field_simp + have harg : (2 * ((k + 1 : ℕ) : ℝ) + 1) * θ = (2 * k + 1) * θ + 2 * θ := by + push_cast + ring + simp only [run, grover, LinearIsometryEquiv.coe_toLinearIsometry] + rw [diffusion_apply (by omega), hsum, phaseOracle_apply, ih] + obtain ⟨i, c, u⟩ := p + cases c + · simp + simp only [marked, decide_eq_true_eq, Bool.true_and, ite_true] + by_cases h : i = z + · have hreal : 2 * ((N : ℝ)⁻¹ * (-a + (N - 1) * b)) + a = + Real.sin ((2 * ((k + 1 : ℕ) : ℝ) + 1) * θ) := by + rw [harg, Real.sin_add, Real.sin_two_mul, Real.cos_two_mul, hs, hc, hcosx] + linear_combination (-(2 * a + 2 * b)) * hX + (-2 * a) * hNinv + simp only [h, ite_true] + rw [← hreal] + push_cast + ring + · have hreal : 2 * ((N : ℝ)⁻¹ * (-a + (N - 1) * b)) - b = + Real.cos ((2 * ((k + 1 : ℕ) : ℝ) + 1) * θ) / Real.sqrt (N - 1) := by + rw [harg, Real.cos_add, Real.sin_two_mul, Real.cos_two_mul, hs, hc, hcosx, + eq_div_iff hsN1.ne'] + linear_combination (2 * a * Real.sqrt (N - 1)) * hS2 + + (-2 * b * Real.sqrt (N - 1)) * hX + simp only [h, ite_false] + rw [← hreal] + push_cast + ring + +/-- **Grover's success probability**: after `k` queries on the input marking `z`, measuring the +query register gives `z` with probability `sin²((2k + 1) θ)`. -/ +theorem regProb_run_grover (hN : 2 ≤ N) (z : Fin N) (k : ℕ) : + regProb (run (grover N) (uniform N) (marked z) k) z = + Real.sin ((2 * k + 1) * groverAngle N) ^ 2 := by + simp only [regProb, run_grover hN, Fintype.sum_prod_type, Fintype.sum_bool, Fintype.univ_unit, + sum_singleton, ite_true, Bool.false_eq_true, ite_false, norm_zero, Complex.norm_real, + Real.norm_eq_abs, sq_abs] + ring + +/-- **Grover's algorithm** [Grover][Grover1996]: for `N ≥ 2` and every `z`, with +`T = ⌊π / (4θ)⌋` queries, where `θ = arcsin(1 / √N)`, the algorithm outputs the marked item `z` +with probability at least `1 - 1 / N`, and `T ≤ π √N / 4`. -/ +theorem grover_success (hN : 2 ≤ N) (z : Fin N) : + 1 - (N : ℝ)⁻¹ ≤ regProb (run (grover N) (uniform N) (marked z) + ⌊Real.pi / (4 * groverAngle N)⌋₊) z ∧ + (⌊Real.pi / (4 * groverAngle N)⌋₊ : ℝ) ≤ Real.pi * Real.sqrt N / 4 := by + have hN0 : (0 : ℝ) < N := by positivity + have hsN : (0 : ℝ) < Real.sqrt N := Real.sqrt_pos.mpr hN0 + set θ := groverAngle N + have hs : Real.sin θ = (Real.sqrt N)⁻¹ := sin_groverAngle hN + have hθ0 : 0 < θ := Real.arcsin_pos.mpr (inv_pos.mpr hsN) + have hθpi : θ ≤ Real.pi / 2 := Real.arcsin_le_pi_div_two _ + have hsinθ : Real.sin θ ≤ θ := Real.sin_le hθ0.le + set T := ⌊Real.pi / (4 * θ)⌋₊ + have hx : 0 ≤ Real.pi / (4 * θ) := by positivity + have hT1 : (T : ℝ) ≤ Real.pi / (4 * θ) := Nat.floor_le hx + have hT2 : Real.pi / (4 * θ) < T + 1 := Nat.lt_floor_add_one _ + refine ⟨?_, ?_⟩ + · rw [regProb_run_grover hN] + set y := (2 * (T : ℝ) + 1) * θ + -- `y` lies within `θ` of `π / 2`. + have hy1 : y ≤ Real.pi / 2 + θ := by + have : (T : ℝ) * (4 * θ) ≤ Real.pi := (le_div_iff₀ (by positivity)).mp hT1 + simp only [y] + nlinarith + have hy2 : Real.pi / 2 - θ < y := by + have : Real.pi < ((T : ℝ) + 1) * (4 * θ) := (div_lt_iff₀ (by positivity)).mp hT2 + simp only [y] + nlinarith + -- So `|cos y| = |sin (π/2 - y)| ≤ sin θ`. + have hcos : Real.cos y ^ 2 ≤ Real.sin θ ^ 2 := by + rw [← Real.sin_pi_div_two_sub] + have hu1 : -θ ≤ Real.pi / 2 - y := by linarith + have hu2 : Real.pi / 2 - y ≤ θ := by linarith + have h1 : Real.sin (Real.pi / 2 - y) ≤ Real.sin θ := + Real.sin_le_sin_of_le_of_le_pi_div_two (by linarith) hθpi hu2 + have h2 : Real.sin (-θ) ≤ Real.sin (Real.pi / 2 - y) := + Real.sin_le_sin_of_le_of_le_pi_div_two (by linarith) (by linarith) hu1 + rw [Real.sin_neg] at h2 + nlinarith + have hsq : Real.sin θ ^ 2 = (N : ℝ)⁻¹ := by + rw [hs, inv_pow, Real.sq_sqrt hN0.le] + nlinarith [Real.sin_sq_add_cos_sq y] + · calc + (T : ℝ) ≤ Real.pi / (4 * θ) := hT1 + _ ≤ Real.pi / (4 * Real.sin θ) := by + gcongr + rw [hs] + positivity + _ = Real.pi * Real.sqrt N / 4 := by + rw [hs] + field_simp + +end Cslib.Quantum diff --git a/ComplexityTests/QuantumGrover.lean b/ComplexityTests/QuantumGrover.lean new file mode 100644 index 0000000000..aabe103665 --- /dev/null +++ b/ComplexityTests/QuantumGrover.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.QueryComplexity.Quantum.Grover + +/-! Grover's algorithm: concrete instances and axiom guards. -/ + +namespace ComplexityTests.QuantumGrover + +open Cslib.Quantum + +-- With `N = 4`, Grover's algorithm finds the marked item with probability at least `3 / 4` using +-- at most `π √4 / 4 = π / 2` queries. +example (z : Fin 4) : + 1 - ((4 : ℕ) : ℝ)⁻¹ ≤ regProb (run (grover 4) (uniform 4) (marked z) + ⌊Real.pi / (4 * groverAngle 4)⌋₊) z ∧ + (⌊Real.pi / (4 * groverAngle 4)⌋₊ : ℝ) ≤ Real.pi * Real.sqrt (4 : ℕ) / 4 := + grover_success (by norm_num) z + +-- Grover's algorithm is a query algorithm with a unit initial state that succeeds with probability +-- `3 / 4 ≥ 2 / 3`, so it satisfies the hypothesis of the BBBV bound, a non-vacuous instance. +example : ‖uniform 4‖ = 1 := norm_uniform (by norm_num) + +example : ((4 : ℕ) : ℝ) - 2 ≤ 144 * ((⌊Real.pi / (4 * groverAngle 4)⌋₊ : ℕ) : ℝ) ^ 2 := + card_sub_two_le (grover 4) (norm_uniform (by norm_num)) _ fun z => + le_trans (by norm_num) (grover_success (by norm_num) z).1 + +-- Before any query, the marked item has probability `sin² θ`. +example (z : Fin 4) : + regProb (run (grover 4) (uniform 4) (marked z) 0) z = Real.sin (groverAngle 4) ^ 2 := by + simpa using regProb_run_grover (by norm_num) z 0 + +/-- +info: 'Cslib.Quantum.run_grover' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms run_grover + +/-- +info: 'Cslib.Quantum.grover_success' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms grover_success + +end ComplexityTests.QuantumGrover diff --git a/ROADMAP.md b/ROADMAP.md index 4fc0d0504c..272bb4b966 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -594,7 +594,7 @@ developments, not assertions that every prerequisite is missing or assignments t | Total search and computational games | Build on [FNP, FP and TFNP with search reductions](Complexity/Computability/Complexity/Classes/TFNP.lean), including `FP = FNP` exactly when `P = NP` ([search to decision](Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean)), `TFNP ⊆ FP → NP ∩ coNP ⊆ P`, and the canonical subclasses [PLS, PPP, PPAD and PPA](Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean) with their combinatorial totality principles ([Principles](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Principles.lean)), inclusions `PLS, PPP, PPAD, PPA ⊆ TFNP`, `PPAD ⊆ PPP`, and `PPAD ⊆ PPA`, and De Morgan circuit problems (`LocalOpt ∈ PLS`, `Pigeon ∈ PPP`, `EndOfLine ∈ PPAD`, `Leaf ∈ PPA`). Their [completeness](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Completeness.lean) now follows from polynomial-time construction of function-family circuit codes, preserving binary local-search costs. Develop CLS, further local search, fixed-point and equilibrium problems. | | Logic and descriptive complexity | Building on [Fagin's theorem](Complexity/Computability/Complexity/Fagin/Converse.lean): logical characterizations of additional resource classes, fixed-point and order-invariant queries, and uniform translations between syntax, structures and algorithms. | | Kolmogorov complexity and metacomplexity | Build on [plain Kolmogorov uncomputability](Complexity/Computability/Kolmogorov/Uncomputability.lean), [single-tape and Post–Turing (`TM0`/`TM1`) description methods and simulations](Complexity/Computability/Kolmogorov/SingleTape.lean), and [multi-tape description methods and `Partrec` optimality](Complexity/Computability/Kolmogorov/MultiTape.lean) (#318): `ofTM0` and `ofTM1` are defined through the `SingleTapeTM` embeddings of Mathlib's `TM0`/`TM1`; `ofSingleTapeTM` (and `ofTM0`) are simulated by `ofMultiTapeTM` with zero program overhead and linear time overhead (single-tape → multi-tape only; the reverse simulation is not formalized); and each of `ofSingleTapeTM`, `ofTM0`, `ofTM1` and `ofMultiTapeTM`, pushed forward along a computable decoder, is simulated by the universal partial-recursive description method `universal` with additive overhead. Extend prefix-free complexity, resource-bounded MCSP variants and connections to learning, cryptography and lower bounds. | -| Quantum complexity | The [quantum query model with phase oracles and the BBBV `Ω(√N)` lower bound for search](Complexity/Computability/QueryComplexity/Quantum/Search.lean) are proved (#896); Grover's algorithm, BQP and `BQP ⊆ PP` remain. Reusable circuit/channel/measurement semantics, uniformity and approximation costs, BQP/QMA and related query, communication and interactive classes, amplification, containments and complete problems. Reuse suitable quantum foundations rather than create incompatible models. | +| Quantum complexity | The [quantum query model with phase oracles and the BBBV `Ω(√N)` lower bound for search](Complexity/Computability/QueryComplexity/Quantum/Search.lean) are proved, with [Grover's algorithm](Complexity/Computability/QueryComplexity/Quantum/Grover.lean) meeting it (`⌊π/(4θ)⌋ ≤ π√N/4` queries, success at least `1 - 1/N`) (#896); BQP and `BQP ⊆ PP` remain. Reusable circuit/channel/measurement semantics, uniformity and approximation costs, BQP/QMA and related query, communication and interactive classes, amplification, containments and complete problems. Reuse suitable quantum foundations rather than create incompatible models. | ### Measure reuse across papers diff --git a/references.bib b/references.bib index 0539269adb..8f1302a9de 100644 --- a/references.bib +++ b/references.bib @@ -1732,6 +1732,15 @@ @article{GotsmanLinial1992 doi = {10.1016/0097-3165(92)90060-8} } +@inproceedings{Grover1996, + author = {Grover, Lov K.}, + title = {A Fast Quantum Mechanical Algorithm for Database Search}, + booktitle = {Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC)}, + pages = {212--219}, + year = {1996}, + doi = {10.1145/237814.237866} +} + @inproceedings{GuoKoppartySudan2013, author = {Guo, Alan and Kopparty, Swastik and Sudan, Madhu}, title = {New affine-invariant codes from lifting},