Phase kickback

Querying the XOR oracle of f with the target qubit in |−⟩ leaves the target untouched and kicks the value of f back into the phase of the input register [dW19, qcnotes.tex:1167]:

U_f (|x⟩ ⊗ |−⟩) = (−1)^{f(x)} · (|x⟩ ⊗ |−⟩),

the "phase kick-back trick" [dW19, qcnotes.tex:1173]. Dually, a |+⟩ target is left invariant, which lets circuits choose per-branch whether a phase query happens [dW19, qcnotes.tex:1173].

The eigenvalue form replaces the oracle by a controlled unitary: if the target register holds an eigenstate |u⟩ of U, the eigenvalue e^{iθ} is "kicked back" in front of the |1⟩ component of the control [CEMM98, cemm6.tex:163].

Main results

• LeanPool.LeanQuantumAlg.phase_kickback — U_f (|x⟩ ⊗ |−⟩) = (−1)^{f(x)} (|x⟩ ⊗ |−⟩), with the sign written as if f x then -1 else 1.
• LeanPool.LeanQuantumAlg.xorOracle_apply_tensor_ketPlus — U_f (|x⟩ ⊗ |+⟩) = |x⟩ ⊗ |+⟩.
• LeanPool.LeanQuantumAlg.eigenvalue_phase_kickback — c-U ((a|0⟩ + b|1⟩) ⊗ |u⟩) = (a|0⟩ + e^{iθ} b|1⟩) ⊗ |u⟩ when U |u⟩ = e^{iθ} |u⟩.

theorem QuantumAlg.PhaseKickback.main {n : ℕ} (f : Fin (2 ^ n) → Bool) (x : Fin (2 ^ n)) : ((Gate.xorOracle f).apply ((PureState.ket x).tensor PureState.ketMinus)).vec = (if f x = true then -1 else 1) • ((PureState.ket x).tensor PureState.ketMinus).vec

Phase kickback: on a |−⟩ target the XOR oracle acts as the phase oracle |x⟩ ↦ (−1)^{f(x)} |x⟩; the sign (−1)^{f(x)} is written if f x then -1 else 1.

theorem QuantumAlg.xorOracle_apply_tensor_ketPlus {n : ℕ} (f : Fin (2 ^ n) → Bool) (x : Fin (2 ^ n)) : (Gate.xorOracle f).apply ((PureState.ket x).tensor PureState.ketPlus) = (PureState.ket x).tensor PureState.ketPlus

On a |+⟩ target the XOR oracle acts trivially, whatever f is.

theorem QuantumAlg.GeneralizedPhaseKickback.main {n : ℕ} (U : Gate n) (u : PureState n) (θ : ℝ) (hu : U.applyVec u.vec = Complex.exp (↑θ * Complex.I) • u.vec) (a b : ℂ) : U.controlled.applyVec ((a • PureState.ket0.vec + b • PureState.ket1.vec).tensor u.vec) = (a • PureState.ket0.vec + (Complex.exp (↑θ * Complex.I) * b) • PureState.ket1.vec).tensor u.vec

Eigenvalue phase kickback [CEMM98, cemm6.tex:163]: if the target register holds an eigenstate |u⟩ of U with eigenvalue e^{iθ}, the controlled U leaves the target unchanged and kicks the eigenvalue back onto the |1⟩ component of the control [CEMM98, cemm6.tex:142]:

c-U ((a|0⟩ + b|1⟩) ⊗ |u⟩) = (a|0⟩ + e^{iθ} b|1⟩) ⊗ |u⟩.