Parameter-shift rule

A variational (parameterized) quantum model has a cost C(θ) = ⟨ψ| U(θ)† O U(θ) |ψ⟩ that is optimized over the parameters θ. When θ enters through a single Pauli rotation gate, C is a frequency-1 trigonometric polynomial in θ, and its exact analytic gradient is obtained from two shifted evaluations — the parameter-shift rule C'(θ) = (C(θ + π/2) − C(θ − π/2)) / 2.

This module records the parameter-shift rule abstractly (ParamShiftModel), and instantiates it on a concrete single-qubit R_Y(θ) ansatz with observable Z, whose cost is cos θ.

Sources: Schuld et al. (2019), Evaluating analytic gradients on quantum hardware; Wierichs et al. (2022), General parameter-shift rules for quantum gradients; Farhi, Goldstone, Gutmann (2014), A Quantum Approximate Optimization Algorithm.

Main results

• LeanPool.LeanQuantumAlg.ParamShiftModel / ParamShiftModel.parameter_shift — the parameter-shift rule for any frequency-1 trigonometric cost.
• LeanPool.LeanQuantumAlg.varCost — the single-qubit R_Y(θ) variational cost.
• LeanPool.LeanQuantumAlg.varCost_ket0_Z — the R_Y / Z / |0⟩ cost equals cos θ.
• LeanPool.LeanQuantumAlg.varCost_ket0_Z_parameter_shift — the parameter-shift rule for it.

structure QuantumAlg.ParamShiftModel : Type

A single-parameter variational cost whose dependence on the parameter is a frequency-1 trigonometric polynomial a + b cos θ + c sin θ — the structure that makes the parameter-shift rule exact. A parameterized-circuit cost built from a single Pauli rotation gate has this form.

• cost : ℝ → ℝ

  The cost function.

• a : ℝ

  Constant Fourier coefficient.

• b : ℝ

  Cosine Fourier coefficient.

• c : ℝ

  Sine Fourier coefficient.

• trig (θ : ℝ) : self.cost θ = self.a + self.b * Real.cos θ + self.c * Real.sin θ

  The cost is a frequency-1 trigonometric polynomial.

theorem QuantumAlg.ParamShiftModel.parameter_shift (M : ParamShiftModel) (θ : ℝ) : deriv M.cost θ = (M.cost (θ + Real.pi / 2) - M.cost (θ - Real.pi / 2)) / 2

Parameter-shift rule. The exact derivative of a frequency-1 trigonometric cost is the symmetric finite difference at shift π/2.

noncomputable def QuantumAlg.varCost (ψ : PureState 1) (O : HilbertOperator 1) (θ : ℝ) : ℝ

The single-qubit R_Y(θ) variational cost with observable O on input ψ: C(θ) = ⟨ψ| R_Y(θ)† O R_Y(θ) |ψ⟩.

Equations

• QuantumAlg.varCost ψ O θ = ((QuantumAlg.rotY θ).apply ψ).expVal O

theorem QuantumAlg.rotY_apply_ket0 (θ : ℝ) : ((rotY θ).apply PureState.ket0).vec = ↑(Real.cos (θ / 2)) • PureState.ket0.vec + ↑(Real.sin (θ / 2)) • PureState.ket1.vec

R_Y(θ) |0⟩ = cos(θ/2) |0⟩ + sin(θ/2) |1⟩.

theorem QuantumAlg.inner_ket01_combo (a b c d : ℂ) : inner ℂ (a • PureState.ket0.vec + b • PureState.ket1.vec) (c • PureState.ket0.vec + d • PureState.ket1.vec) = (starRingEnd ℂ) a * c + (starRingEnd ℂ) b * d

Inner product of two single-qubit states in the computational basis.

theorem QuantumAlg.varCost_ket0_Z (θ : ℝ) : varCost PureState.ket0 Gate.Z.op θ = Real.cos θ

The R_Y(θ) ansatz cost with observable Z on |0⟩ equals cos θ.

noncomputable def QuantumAlg.rotYZModel : ParamShiftModel

A concrete variational model: the R_Y / Z / |0⟩ cost cos θ.

Equations

• QuantumAlg.rotYZModel = { cost := QuantumAlg.varCost QuantumAlg.PureState.ket0 QuantumAlg.Gate.Z.op, a := 0, b := 1, c := 0, trig := ⋯ }

theorem QuantumAlg.varCost_ket0_Z_parameter_shift (θ : ℝ) : deriv (varCost PureState.ket0 Gate.Z.op) θ = (varCost PureState.ket0 Gate.Z.op (θ + Real.pi / 2) - varCost PureState.ket0 Gate.Z.op (θ - Real.pi / 2)) / 2

Parameter-shift rule for the R_Y / Z / |0⟩ ansatz.

theorem QuantumAlg.ParameterShiftRule.main (M : ParamShiftModel) (θ : ℝ) : deriv M.cost θ = (M.cost (θ + Real.pi / 2) - M.cost (θ - Real.pi / 2)) / 2

Main parameter-shift theorem for a frequency-1 variational cost.

theorem QuantumAlg.ParameterShiftRule.main_trig_identity (a b c θ : ℝ) : deriv (fun (t : ℝ) => a + b * Real.cos t + c * Real.sin t) θ = (a + b * Real.cos (θ + Real.pi / 2) + c * Real.sin (θ + Real.pi / 2) - (a + b * Real.cos (θ - Real.pi / 2) + c * Real.sin (θ - Real.pi / 2))) / 2

Public supporting theorem: the quantum-free trigonometric identity.

theorem QuantumAlg.ParameterShiftRule.main_ry_z_example (θ : ℝ) : varCost PureState.ket0 Gate.Z.op θ = Real.cos θ

Public supporting theorem: the concrete R_Y / Z / |0⟩ cost.

theorem QuantumAlg.ParameterShiftRule.main_ry_z_parameter_shift (θ : ℝ) : deriv (varCost PureState.ket0 Gate.Z.op) θ = (varCost PureState.ket0 Gate.Z.op (θ + Real.pi / 2) - varCost PureState.ket0 Gate.Z.op (θ - Real.pi / 2)) / 2

Public supporting theorem: parameter shift for the concrete R_Y / Z / |0⟩ cost.