Prove2Me

Exact success probability after rr iterations: sin⁡2((r+12)θ)\sin^2((r+\frac12)\theta)

Proved
GroverWiki.measureProb_groverState

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

grover-algorithmquantum-computingquantum-search

Let f ⁣:{0,…,N−1}→{0,1}f\colon\{0,\dots,N-1\}\to\{0,1\} have exactly one index ω\omega with f(ω)=1f(\omega) = 1, and let θ=2arcsin⁡1N\theta = 2\arcsin\frac{1}{\sqrt N}. Starting from ∣s⟩|s\rangle and applying rr Grover iterations, the probability that a computational-basis measurement of (UsUω)r∣s⟩(U_sU_\omega)^r|s\rangle yields ω\omega is exactly

∣⟨ω∣(UsUω)r∣s⟩∣2=sin⁡2 ⁣((r+12)θ).\bigl|\langle\omega|(U_sU_\omega)^r|s\rangle\bigr|^2 = \sin^2\!\Bigl(\bigl(r+\tfrac12\bigr)\theta\Bigr) .

This is the central quantitative statement about Grover's algorithm: the success probability oscillates with the number of iterations and is close to 11 when (r+12)θ≈π/2(r+\frac12)\theta \approx \pi/2.

Preamble
import Mathlib
import Definitions.Def_GroverWiki_Defs

open Matrix
Formal statement
namespace GroverWiki

/-- Geometric proof: the exact probability of measuring `ω` after `r` Grover iterations is
`sin²((r + 1/2) θ)` with `θ = 2 arcsin(1/√N)`. -/
theorem measureProb_groverState {N : ℕ} (f : Fin N → Fin 2) (ω : Fin N)
    (hω : ∀ x, f x = 1 ↔ x = ω) (r : ℕ) :
    measureProb (groverState f r) ω =
      Real.sin ((r + 1 / 2) * (2 * Real.arcsin (1 / Real.sqrt N))) ^ 2 := by sorry

end GroverWiki
Source
Wikipedia, "Grover's algorithm", revision oldid=1373498442, https://en.wikipedia.org/w/index.php?title=Grover%27s_algorithm&oldid=1373498442, section "Geometric proof" (PDF p. 5)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph