Documentation

Complexity.Computability.QueryComplexity.Quantum.Grover

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. 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 #

Main results #

References #

source
noncomputable def Cslib.Quantum.uniform (N : ℕ) :
State N Unit

The uniform superposition |s⟩ = N^{-1/2} ∑_i |i, 1⟩ with control bit 1.

Instances For
    source
    theorem Cslib.Quantum.norm_uniform {N : ℕ} (hN : 0 < N) :
    ‖uniform N‖ = 1
    source
    noncomputable def Cslib.Quantum.diffusion (N : ℕ) :
    State N Unit ≃ₗᵢ[ℂ] State N Unit

    The diffusion D = 2|s⟩⟨s| - I: the reflection about the uniform superposition.

    Instances For
      source
      theorem Cslib.Quantum.diffusion_apply {N : ℕ} (hN : 0 < N) (ψ : State N Unit) (p : Fin N × Bool × Unit) :
      ((diffusion N) ψ).ofLp p = (2 * if p.2.1 = true then (↑N)⁻¹ * ∑ q : Fin N × Bool × Unit, if q.2.1 = true then ψ.ofLp q else 0 else 0) - ψ.ofLp p

      The diffusion inverts every control-1 amplitude about their mean: (Dψ)(i, b) = 2 b · mean_j ψ(j, 1) - ψ(i, b).

      source
      noncomputable def Cslib.Quantum.grover (N a✝ : ℕ) :
      State N Unit →ₗᵢ[ℂ] State N Unit

      The isometries of Grover's algorithm: the identity, then the diffusion after every query. Its initial state is uniform N.

      Instances For
        source
        noncomputable def Cslib.Quantum.groverAngle (N : ℕ) :
        ℝ

        The Grover angle θ = arcsin(1 / √N).

        Instances For
          source
          theorem Cslib.Quantum.run_grover {N : ℕ} [DecidableEq (Fin N)] (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 = true then ↑(if p.1 = z then Real.sin ((2 * ↑k + 1) * groverAngle N) else Real.cos ((2 * ↑k + 1) * groverAngle N) / √(↑N - 1)) else 0

          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.

          source
          theorem Cslib.Quantum.regProb_run_grover {N : ℕ} [DecidableEq (Fin N)] (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

          Grover's success probability: after k queries on the input marking z, measuring the query register gives z with probability sin²((2k + 1) θ).

          source
          theorem Cslib.Quantum.grover_success {N : ℕ} [DecidableEq (Fin N)] (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 * √↑N / 4

          Grover's algorithm Grover: 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.