Grover's algorithm

AbbreviationReal amplitude vectors#✓fully proved

For a type \(\alpha\) (the search space), a real amplitude vector indexed by \(\alpha\) is a function \(\psi : \alpha \to \mathbb{R}\), assigning a real amplitude to each point of \(\alpha\).

abbrev Amplitude (α : Type*) := α → ℝ

Used by 14

Used bySquared norm of an amplitude vector · Grover iteration preserves the squared norm · The uniform amplitude vector is normalized · Symmetric Grover state at a given angle · Inversion about the mean · Grover iterate · Grover step · Probability of the marked outcomes · Exact success probability of Grover search · Mean amplitude · One Grover iteration suffices when a quarter is marked · Phase oracle · Symmetric amplitude vector · Uniform amplitude vector

DefinitionPhase oracle#✓fully proved

For a type \(\alpha\) and a finite set \(M \subseteq \alpha\) of marked elements, the phase oracle sends a real amplitude vector \(\psi\) on \(\alpha\) to the amplitude vector whose value at \(x\) is \(-\psi(x)\) if \(x \in M\) and \(\psi(x)\) if \(x \notin M\); that is, it negates exactly the amplitudes at the marked elements.

def phaseOracle {α : Type*} [DecidableEq α] (marked : Finset α)
    (ψ : Amplitude α) : Amplitude α :=
  fun x => if x ∈ marked then -ψ x else ψ x

Uses 1 · Used by 4

Statement usesReal amplitude vectors

Used byGrover iteration preserves the squared norm · Grover step · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionSquared norm of an amplitude vector#✓fully proved

For a finite type \(\alpha\) and a real amplitude vector \(\psi : \alpha \to \mathbb{R}\), the squared norm of \(\psi\) is its squared Euclidean norm \(\sum_{x \in \alpha} \psi(x)^2\).

def amplitudeNormSq {α : Type*} [Fintype α] (ψ : Amplitude α) : ℝ :=
  ∑ x, (ψ x) ^ 2

Uses 1 · Used by 3

Statement usesReal amplitude vectors

Used byGrover iteration preserves the squared norm · Grover iterates of the uniform state are unit vectors · The uniform amplitude vector is normalized

DefinitionProbability of the marked outcomes#✓fully proved

For a real amplitude vector \(\psi\) on a type \(\alpha\) and a finite set \(M \subseteq \alpha\) of marked elements, the marked probability is \(\sum_{x \in M} \psi(x)^2\). When \(\alpha\) is finite and \(\psi\) has squared norm \(1\), this is the probability of observing a marked outcome.

def markedProbability {α : Type*} (marked : Finset α) (ψ : Amplitude α) : ℝ :=
  ∑ x ∈ marked, (ψ x) ^ 2

Uses 1 · Used by 2

Statement usesReal amplitude vectors

Used byExact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionUniform amplitude vector#✓fully proved

For a finite type \(\alpha\), the uniform amplitude vector on \(\alpha\) is the real amplitude vector whose value at every point is \(1/\sqrt{|\alpha|}\), where \(|\alpha|\) is the number of elements of \(\alpha\).

noncomputable def uniformAmplitude (α : Type*) [Fintype α] : Amplitude α :=
  fun _ => 1 / Real.sqrt (Fintype.card α)

Uses 1 · Used by 4

Statement usesReal amplitude vectors

Used byGrover iterates of the uniform state are unit vectors · The uniform amplitude vector is normalized · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked

TheoremThe uniform amplitude vector is normalized#✓fully proved

For every nonempty finite type \(\alpha\), the uniform amplitude vector on \(\alpha\) has squared Euclidean norm \(1\).

@[simp]
theorem amplitudeNormSq_uniformAmplitude (α : Type*) [Fintype α] [Nonempty α] :
    amplitudeNormSq (uniformAmplitude α) = 1

Uses 3 · Used by 1

Statement usesSquared norm of an amplitude vector · Uniform amplitude vector

Proof usesReal amplitude vectors

Used byGrover iterates of the uniform state are unit vectors

DefinitionMean amplitude#✓fully proved

For a finite type \(\alpha\) and a real amplitude vector \(\psi\) on \(\alpha\), the mean amplitude of \(\psi\) is \(\bigl(\sum_{x \in \alpha} \psi(x)\bigr) / |\alpha|\), the arithmetic mean of its amplitudes. When \(\alpha\) is empty it is \(0\).

noncomputable def meanAmplitude {α : Type*} [Fintype α] (ψ : Amplitude α) : ℝ :=
  (∑ x, ψ x) / Fintype.card α

Uses 1 · Used by 4

Statement usesReal amplitude vectors

Used byGrover iteration preserves the squared norm · Inversion about the mean · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionInversion about the mean#✓fully proved

For a finite type \(\alpha\), the diffusion operator sends a real amplitude vector \(\psi\) on \(\alpha\) to the amplitude vector \(x \mapsto 2\bar\psi - \psi(x)\), where \(\bar\psi\) is the arithmetic mean of the amplitudes of \(\psi\).

noncomputable def diffusion {α : Type*} [Fintype α]
    (ψ : Amplitude α) : Amplitude α :=
  fun x => 2 * meanAmplitude ψ - ψ x

Uses 2 · Used by 2

Statement usesReal amplitude vectors · Mean amplitude

Used byGrover iteration preserves the squared norm · Grover step

DefinitionGrover step#✓fully proved

Let \(\alpha\) be a finite type and \(M \subseteq \alpha\) a set of marked elements. Write \(O_M\) for the phase oracle, which negates the amplitudes at the points of \(M\), and \(D\) for inversion about the mean, which sends an amplitude vector \(\varphi\) on \(\alpha\) to \(x \mapsto 2\bar\varphi - \varphi(x)\), where \(\bar\varphi\) is the arithmetic mean of the amplitudes of \(\varphi\). One Grover step sends a real amplitude vector \(\psi\) on \(\alpha\) to \(D(O_M \psi)\): phase inversion followed by inversion about the mean.

noncomputable def groverStep {α : Type*} [Fintype α] [DecidableEq α]
    (marked : Finset α) (ψ : Amplitude α) : Amplitude α :=
  diffusion (phaseOracle marked ψ)

Uses 3 · Used by 4

Statement usesReal amplitude vectors · Inversion about the mean · Phase oracle

Used byGrover iteration preserves the squared norm · Grover iterate · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionSymmetric amplitude vector#✓fully proved

Let \(M\) be a set of marked elements of a search space \(\alpha\), and let \(a, b \in \mathbb{R}\). The symmetric amplitude vector with marked amplitude \(a\) and unmarked amplitude \(b\) is the real amplitude vector on \(\alpha\) whose value is \(a\) at every element of \(M\) and \(b\) at every element outside \(M\).

def symmetricAmplitude {α : Type*} [DecidableEq α] (marked : Finset α)
    (markedAmplitude unmarkedAmplitude : ℝ) : Amplitude α :=
  fun x => if x ∈ marked then markedAmplitude else unmarkedAmplitude

Uses 1 · Used by 3

Statement usesReal amplitude vectors

Used bySymmetric Grover state at a given angle · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionMean amplitude after the phase oracle#✓fully proved

Let \(M\) be a set of marked elements of a finite search space of size \(N\), let \(M^c\) be the set of unmarked elements, and let \(a, b \in \mathbb{R}\). The oracle mean is \((|M^c|\, b - |M|\, a) / N\).

It is the mean of the amplitude vector obtained by applying the phase oracle to the vector equal to \(a\) on \(M\) and to \(b\) off \(M\).

noncomputable def oracleMean {α : Type*} [Fintype α] [DecidableEq α]
    (marked : Finset α) (a b : ℝ) : ℝ :=
  ((markedᶜ.card : ℝ) * b - (marked.card : ℝ) * a) /
    Fintype.card α

Used by 4

Used byMarked amplitude after a Grover step · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked · Unmarked amplitude after a Grover step

DefinitionMarked amplitude after a Grover step#✓fully proved

Let \(M\) be a set of marked elements of a finite search space of size \(N\), let \(M^c\) be the set of unmarked elements, and let \(a, b \in \mathbb{R}\). With \(\mu = (|M^c|\, b - |M|\, a) / N\), the next marked amplitude is \(2\mu + a\).

It is the common value at the marked elements after one Grover step applied to the amplitude vector equal to \(a\) on \(M\) and to \(b\) off \(M\).

noncomputable def markedAmplitudeNext {α : Type*} [Fintype α] [DecidableEq α]
    (marked : Finset α) (a b : ℝ) : ℝ :=
  2 * oracleMean marked a b + a

Uses 1 · Used by 2

Statement usesMean amplitude after the phase oracle

Used byExact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionUnmarked amplitude after a Grover step#✓fully proved

Let \(M\) be a set of marked elements of a finite search space of size \(N\), let \(M^c\) be the set of unmarked elements, and let \(a, b \in \mathbb{R}\). With \(\mu = (|M^c|\, b - |M|\, a) / N\), the next unmarked amplitude is \(2\mu - b\).

It is the common value at the unmarked elements after one Grover step applied to the amplitude vector equal to \(a\) on \(M\) and to \(b\) off \(M\).

noncomputable def unmarkedAmplitudeNext {α : Type*} [Fintype α]
    [DecidableEq α] (marked : Finset α) (a b : ℝ) : ℝ :=
  2 * oracleMean marked a b - b

Uses 1 · Used by 2

Statement usesMean amplitude after the phase oracle

Used byExact success probability of Grover search · One Grover iteration suffices when a quarter is marked

DefinitionGrover angle#✓fully proved

For a finite search space \(\alpha\) and a marked set \(M \subseteq \alpha\), the Grover angle of \(M\) is \(\theta = \arcsin \sqrt{|M| / |\alpha|}\), where the quotient \(|M| / |\alpha|\) is taken to be \(0\) when \(\alpha\) is empty.

noncomputable def groverAngle {α : Type*} [Fintype α] (marked : Finset α) : ℝ :=
  Real.arcsin (Real.sqrt ((marked.card : ℝ) / Fintype.card α))

Used by 3

Used byStandard Grover iteration count · Grover phase · Exact success probability of Grover search

DefinitionSymmetric Grover state at a given angle#✓fully proved

Let \(\alpha\) be a finite search space and \(M \subseteq \alpha\) a marked set with complement \(M^c\). For a real number \(\varphi\), this is the real amplitude vector on \(\alpha\) whose value is \(\sin\varphi / \sqrt{|M|}\) at every point of \(M\) and \(\cos\varphi / \sqrt{|M^c|}\) at every point of \(M^c\).

When \(M\) and \(M^c\) are nonempty, the marked and unmarked parts of this vector have Euclidean norms \(|\sin\varphi|\) and \(|\cos\varphi|\).

noncomputable def angleAmplitude {α : Type*} [Fintype α] [DecidableEq α]
    (marked : Finset α) (φ : ℝ) : Amplitude α :=
  symmetricAmplitude marked (Real.sin φ / Real.sqrt marked.card)
    (Real.cos φ / Real.sqrt markedᶜ.card)

Uses 2 · Used by 1

Statement usesReal amplitude vectors · Symmetric amplitude vector

Used byExact success probability of Grover search

DefinitionGrover iterate#✓fully proved

Let \(\alpha\) be a finite search space and \(M \subseteq \alpha\) a marked set. For \(k \in \mathbb{N}\) and a real amplitude vector \(\psi : \alpha \to \mathbb{R}\), the \(k\)-th Grover iterate of \(\psi\) is the vector obtained by applying the Grover step for \(M\) to \(\psi\) \(k\) times; the \(0\)-th iterate is \(\psi\) itself.

noncomputable def groverIterate {α : Type*} [Fintype α] [DecidableEq α]
    (marked : Finset α) (k : ℕ) (ψ : Amplitude α) : Amplitude α :=
  (groverStep marked)^[k] ψ

Uses 2 · Used by 4

Statement usesReal amplitude vectors · Grover step

Used byGrover iteration preserves the squared norm · Grover iterates of the uniform state are unit vectors · Exact success probability of Grover search · One Grover iteration suffices when a quarter is marked

TheoremGrover iteration preserves the squared norm#✓fully proved

Let \(\alpha\) be a nonempty finite search space and \(M \subseteq \alpha\) a marked set. For every real amplitude vector \(\psi : \alpha \to \mathbb{R}\) and every \(k \in \mathbb{N}\), let \(\psi_k\) be the vector obtained from \(\psi\) by applying the Grover step for \(M\) \(k\) times. Then \(\sum_{x \in \alpha} \psi_k(x)^2 = \sum_{x \in \alpha} \psi(x)^2\).

@[simp]
theorem amplitudeNormSq_groverIterate {α : Type*} [Fintype α]
    [DecidableEq α] [Nonempty α] (marked : Finset α) (k : ℕ)
    (ψ : Amplitude α) :
    amplitudeNormSq (groverIterate marked k ψ) = amplitudeNormSq ψ

Uses 7 · Used by 1

Statement usesReal amplitude vectors · Squared norm of an amplitude vector · Grover iterate

Proof usesInversion about the mean · Grover step · Mean amplitude · Phase oracle

Used byGrover iterates of the uniform state are unit vectors

TheoremGrover iterates of the uniform state are unit vectors#✓fully proved

Let \(\alpha\) be a nonempty finite search space, \(M \subseteq \alpha\) a marked set, and \(u\) the uniform amplitude vector, given by \(u(x) = 1/\sqrt{|\alpha|}\) for every \(x \in \alpha\). For every \(k \in \mathbb{N}\), let \(\psi_k\) be the vector obtained from \(u\) by applying the Grover step for \(M\) \(k\) times. Then \(\sum_{x \in \alpha} \psi_k(x)^2 = 1\).

@[simp]
theorem amplitudeNormSq_groverIterate_uniform {α : Type*} [Fintype α]
    [DecidableEq α] [Nonempty α] (marked : Finset α) (k : ℕ) :
    amplitudeNormSq (groverIterate marked k (uniformAmplitude α)) = 1

Uses 5

Statement usesSquared norm of an amplitude vector · Grover iterate · Uniform amplitude vector

Proof usesGrover iteration preserves the squared norm · The uniform amplitude vector is normalized

DefinitionGrover phase#✓fully proved

Let \(\alpha\) be a finite search space, \(M \subseteq \alpha\) a marked set and \(\theta\) the Grover angle of \(M\). For \(k \in \mathbb{N}\), the Grover phase of \(M\) after \(k\) iterations is the real number \((2k + 1)\theta\).

When \(M\) and its complement are both nonempty, this is the phase reached from the uniform initial state after \(k\) Grover steps.

noncomputable def groverPhase {α : Type*} [Fintype α]
    (marked : Finset α) (k : ℕ) : ℝ :=
  (2 * (k : ℝ) + 1) * groverAngle marked

Uses 1 · Used by 1

Statement usesGrover angle

Used byExact success probability of Grover search

TheoremExact success probability of Grover search#✓fully proved

Let \(\alpha\) be a finite search space and \(M \subseteq \alpha\) a marked set such that both \(M\) and its complement are nonempty, and let \(\theta = \arcsin \sqrt{|M| / |\alpha|}\) be the Grover angle of \(M\). For \(k \in \mathbb{N}\), let \(\psi_k\) be the vector obtained by applying the Grover step for \(M\) \(k\) times to the uniform amplitude vector, whose value is \(1/\sqrt{|\alpha|}\) at every point. Then the marked probability of \(\psi_k\) is \(\sum_{x \in M} \psi_k(x)^2 = \sin^2((2k + 1)\theta)\).

theorem markedProbability_groverIterate_uniform {α : Type*} [Fintype α]
    [DecidableEq α] (marked : Finset α) (hMarked : marked.Nonempty)
    (hUnmarked : markedᶜ.Nonempty) (k : ℕ) :
    markedProbability marked (groverIterate marked k (uniformAmplitude α)) =
      (Real.sin (groverPhase marked k)) ^ 2

Uses 14

Statement usesGrover iterate · Grover phase · Probability of the marked outcomes · Uniform amplitude vector

Proof usesReal amplitude vectors · Symmetric Grover state at a given angle · Grover angle · Grover step · Marked amplitude after a Grover step · Mean amplitude · Mean amplitude after the phase oracle · Phase oracle · Symmetric amplitude vector · Unmarked amplitude after a Grover step

DefinitionStandard Grover iteration count#✓fully proved

Let \(M\) be a set of marked elements of a finite search space of size \(N\), and let \(\theta = \arcsin \sqrt{|M| / N}\) be its Grover angle. The standard iteration count is \(\lfloor \pi / (4\theta) \rfloor\), the largest natural number at most \(\pi / (4\theta)\); it is \(0\) when \(\theta = 0\), that is, when no element is marked.

noncomputable def floorIterations {α : Type*} [Fintype α]
    (marked : Finset α) : ℕ :=
  ⌊Real.pi / (4 * groverAngle marked)⌋₊

Uses 1

Statement usesGrover angle

TheoremOne Grover iteration suffices when a quarter is marked#✓fully proved

Let \(M\) be a nonempty set of marked elements of a finite search space of size \(N\) with \(4|M| = N\). Starting from the uniform amplitude vector, one Grover iteration produces an amplitude vector whose marked probability is \(1\).

theorem one_step_success_of_four_mul_card_eq {α : Type*} [Fintype α]
    [DecidableEq α] (marked : Finset α) (hMarked : marked.Nonempty)
    (hquarter : 4 * marked.card = Fintype.card α) :
    markedProbability marked
        (groverIterate marked 1 (uniformAmplitude α)) = 1

Uses 11

Statement usesGrover iterate · Probability of the marked outcomes · Uniform amplitude vector

Proof usesReal amplitude vectors · Grover step · Marked amplitude after a Grover step · Mean amplitude · Mean amplitude after the phase oracle · Phase oracle · Symmetric amplitude vector · Unmarked amplitude after a Grover step

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.