Amplitude estimation (exact, dyadic eigenphase)

Amplitude estimation reads the unknown good-state amplitude of an amplitude- amplification instance by running quantum phase estimation on the amplification operator [Lin22]. This module records the exact dyadic regime: QPE reads out the phase-register basis vector, and the estimate sin^2(pi*j/2^t) equals the good-state probability in the two-dimensional amplitude-amplification model.

theorem QuantumAlg.AmplitudeEstimation.main_exact_dyadic (t : ℕ) (j : Fin (2 ^ t)) (theta : ℝ) (htheta : theta = Real.pi * ↑↑j / 2 ^ t) : (invQFT t).applyVec (phaseState t (↑↑j / 2 ^ t)) = (PureState.ket j).vec ∧ (amplitudeAmplificationState theta 0).probOutcome 1 = Real.sin (Real.pi * ↑↑j / 2 ^ t) ^ 2

Exact amplitude estimation in the decoupled dyadic model. Phase estimation enters through the raw-vector readout theorem, while the success probability is the existing amplitude-amplification PureState probability theorem.

def QuantumAlg.amplitudeEstimationExactResourceProfile (t : ℕ) : ResourceProfile

Trusted resource profile for exact amplitude estimation in the decoupled dyadic-eigenphase model. It records the QPE layer used by the exact readout; source-level state-preparation and reflection oracles are outside this exact model.

Equations

• QuantumAlg.amplitudeEstimationExactResourceProfile t = QuantumAlg.qpeExactResourceProfile t

theorem QuantumAlg.amplitudeEstimationExactResourceProfile_exact (t : ℕ) : (amplitudeEstimationExactResourceProfile t).HasExactCounts (2 ^ t - 1) t (t ^ 2) 0

theorem QuantumAlg.AmplitudeEstimation.main_exact_dyadic_with_resources (t : ℕ) (j : Fin (2 ^ t)) (theta : ℝ) (htheta : theta = Real.pi * ↑↑j / 2 ^ t) : ((invQFT t).applyVec (phaseState t (↑↑j / 2 ^ t)) = (PureState.ket j).vec ∧ (amplitudeAmplificationState theta 0).probOutcome 1 = Real.sin (Real.pi * ↑↑j / 2 ^ t) ^ 2) ∧ (amplitudeEstimationExactResourceProfile t).HasExactCounts (2 ^ t - 1) t (t ^ 2) 0

Exact amplitude estimation paired with the decoupled QPE resource profile.

structure QuantumAlg.SourceAmplitudeEstimationInput : Type

Source-level exact-amplitude-estimation input in the same dyadic regime: a source-style preparation/reflection amplitude-amplification model together with a phase-register index for the exact QPE readout.

• source : SourceAmplitudeAmplificationModel

  The source-level amplitude-amplification model being estimated.

• t : ℕ

  Number of phase-register qubits in the exact dyadic regime.

• j : Fin (2 ^ self.t)

  The exact dyadic phase-register output.

• theta_eq : self.source.theta = Real.pi * ↑↑self.j / 2 ^ self.t

  The source angle is exactly represented by j / 2^t.

theorem QuantumAlg.AmplitudeEstimation.main (E : SourceAmplitudeEstimationInput) : ((E.source.preparation.apply PureState.ket0).probOutcome 1 = Real.sin (Real.pi * ↑↑E.j / 2 ^ E.t) ^ 2 ∧ (invQFT E.t).applyVec (phaseState E.t (↑↑E.j / 2 ^ E.t)) = (PureState.ket E.j).vec) ∧ (amplitudeEstimationExactResourceProfile E.t).HasExactCounts (2 ^ E.t - 1) E.t (E.t ^ 2) 0

Source-level exact amplitude-estimation bridge: the source preparation has good-state probability sin^2(theta), exact QPE reads the dyadic phase register, and the same trusted exact-QPE resource profile is recorded.