amplitude estimation

Point phase estimation at the amplitude-amplification rotation and the success probability itself becomes measurable, quadratically faster than sampling could ever learn it.

proved in corpus · proved here, no imported axiomsLean amplitude_estimation

In plain terms

Amplitude amplification boosts a success probability a; amplitude estimation MEASURES it. Classically, learning a to precision 1/T costs about T-squared samples. The quantum route: the amplification step rotates its two-dimensional stage by an angle whose sine squared IS a, so the angle is sitting in the eigenvalues -- and eigenvalue angles are exactly what phase estimation reads out.

Run the rotation a controlled number of times, Fourier-read the control register, and the measured index lands near the angle with fixed odds; squaring its sine gives the estimate of a, accurate to about 1/T after only T rounds. That quadratic saving is what makes quantum counting and Monte Carlo speedups tick.

The state splits into exactly two clean branches -- clockwise and counterclockwise rotation -- and because their companions are perpendicular, the readout is an honest 50/50 mixture of two well-understood distributions, with no interference between them.

In CSD

The AA-5b assembly, where three prepared layers meet in one theorem: the eigenstructure of the amplification step (its rotation plane carries eigenvectors g +- i b with eigenvalues e^(+-2 i theta)), the joint-register mixture law (orthogonal second factors kill every cross-term in a Born marginal), and the 4/pi^2 phase-estimation bound. The kickback state is proved EQUAL to a two-branch phase form, so the counting marginal is an exact half-half mixture -- an equality, not an estimate.

The stated bounds: any index in the closest-index window carries probability at least 2/pi^2; its mirror index -c carries the other branch's 2/pi^2 and decodes to the SAME estimate, so the pair jointly carries 4/pi^2; and the estimate lands within pi sqrt(a(1-a))/T + pi^2/(4 T^2) of the truth. Honest scope: the paper's literal 8/pi^2 additionally counts both rounding directions, which needs a two-index Dirichlet -kernel inequality recorded in the plan and not attempted. The standing disclaimer applies: the algorithm layer consumes the unitary pillar and does not support foundations.

Mathematically

With Q the amplification step at angle theta (sin theta = sqrt a) on the rotation plane, the kickback state (1/sqrt T) sum_x |x> tensor Q^x psi decomposes exactly as c_+ phaseState(theta/pi) tensor v_+ + c_- phaseState(-theta/pi) tensor v_-, where v_+- = g +- i b are the orthogonal eigenvectors, Q^x v_+- = e^(+-2 i x theta) v_+-, and |c_+-| = 1/2.

Applying the inverse QFT to the counting register and taking the Born marginal gives exactly (P_+(c) + P_-(c))/2, the half-half mixture of the two single-phase counting distributions. At any c with |theta/pi - c/T| <= 1/(2T), the plus branch contributes at least 4/pi^2, so the marginal carries at least 2/pi^2; and sin^2(pi c / T) estimates a = sin^2 theta within 2 sqrt(a(1-a)) eps + eps^2 at eps = pi/(2T), the product-form sin^2 difference identity plus the Lipschitz bound on sin.

The name

The same four authors as amplitude amplification -- Brassard, Hoyer, Mosca and Tapp -- in the same 2000 paper, "Quantum Amplitude Amplification and Estimation". The estimation half is the paper's Theorem 12, feeding their quantum counting results: estimating how many marked items a database holds without ever listing them.

The technique is the meeting point of the field's two workhorse subroutines -- Grover's rotation geometry (1996) and Kitaev-style phase estimation (1995) -- and later became the engine of quantum Monte Carlo speedups via Montanaro's 2015 work.

Module
CsdLean4/Mathlib/QuantumInfo/AmplitudeEstimation.lean
Background
BHMT, Quantum Amplitude Amplification and Estimation (quant-ph/0005055), Thm 12
Related
amplitude amplification, phase estimation, quantum fourier transform, grover algorithm

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy