Quantum signal processing (single qubit) — Fourier basis (trigonometric)

The Fourier-basis single-qubit QSP characterizations: the YZY and YZZYZ (W-Z-W) quantum-neural-network forms of [YYLW22, neurips_2022.tex:283] and [YYLW22, neurips_2022.tex:333]. These use the encoding rotation R_Z(x) = e^{-ixZ/2} and trainable R_Y/R_Z gates (all in Core.Components.Gates), and produce Laurent polynomials in e^{ix/2}.

A Laurent polynomial of degree ≤ L and parity L mod 2 is exactly e^{-iLx/2}·A(e^{ix}) for a unique ordinary A : ℂ[X] with deg A ≤ L, encoded here by lEval L A x. Under this encoding, conjugation on the unit circle is the conjugate-reflection A ↦ reflect L (conjP A) (conj_lEval), and the pointwise normalization becomes the polynomial identity A·reflect L (conjP A) + B·reflect L (conjP B) = X^L (qspYZ_normalization_iff).

LeanPool.LeanQuantumAlg.qsp_yzy_iff and LeanPool.LeanQuantumAlg.qsp_yzzyz_iff are the YZY and YZZYZ characterizations, with pair conditions IsYZYPair/IsYZPair and a Laurent-side induction (this is the single-qubit precursor of the controlled-unitary / QET-QPP transformations). The polynomial normalization matches the pointwise |P|² + |Q|² = 1 via LeanPool.LeanQuantumAlg.qspYZ_normalization_iff.

This module is one half of the single-qubit QSP development; the Chebyshev-basis (reflection + Wx) forms live in LeanPool.LeanQuantumAlg.Primitives.QSP.Chebyshev, and LeanPool.LeanQuantumAlg.Primitives.QSP re-exports both.

Main results

• LeanPool.LeanQuantumAlg.qspYZY_mem_unitaryGroup, LeanPool.LeanQuantumAlg.qspYZZYZ_mem_unitaryGroup — the QNN products are unitary.
• LeanPool.LeanQuantumAlg.qspYZZYZ_forward / LeanPool.LeanQuantumAlg.qspYZZYZ_converse and LeanPool.LeanQuantumAlg.qspYZY_forward / LeanPool.LeanQuantumAlg.qspYZY_converse — soundness and completeness via Laurent-encoded induction.
• LeanPool.LeanQuantumAlg.qsp_yzzyz_iff, LeanPool.LeanQuantumAlg.qsp_yzy_iff — the trigonometric characterizations (registered targets).

Pinned Mathlib API: Polynomial.reflect, Polynomial.divX, Complex.exp_mul_I, Complex.norm_mul_exp_arg_mul_I, Complex.exp_eq_exp_iff_exists_int, Complex.cos_arg, Complex.sin_arg, Set.Ioo.infinite, List.reverseRecOn.

Trigonometric QSP: the YZY and YZZYZ (W-Z-W) forms

[YYLW22, neurips_2022.tex:283] and [YYLW22, neurips_2022.tex:333] characterize the single-qubit QNNs R_Y(θ₀)·∏_j R_Z(x)R_Y(θ_j) and R_Z(φ)·W(θ₀,φ₀)·∏_j R_Z(x)W(θ_j,φ_j) (with W(θ,φ) = R_Y(θ)R_Z(φ) and encoding gate R_Z(x) = e^{-ixZ/2}) through Laurent polynomials P, Q ∈ ℂ[e^{ix/2}, e^{-ix/2}] with degree ≤ L, parity L mod 2, and |P(x)|² + |Q(x)|² = 1 on ℝ.

A Laurent polynomial of degree ≤ L and parity L mod 2 has exponent support in {-L, -L+2, …, L}, so it is exactly e^{-iLx/2}·A(e^{ix}) for a unique ordinary A : ℂ[X] with deg A ≤ L (lEval below). Under this encoding, conjugation on the unit circle becomes the conjugate-reflection A ↦ reflect L (conjP A) (conj_lEval), and the pointwise normalization becomes the polynomial identity A·reflect L (conjP A) + B·reflect L (conjP B) = X^L (qspYZ_normalization_iff).

noncomputable def QuantumAlg.lEval (L : ℕ) (F : Polynomial ℂ) (x : ℝ) : ℂ

e^{-iLx/2}·F(e^{ix}): the value at z = e^{ix/2} of the Laurent polynomial z^{-L}·F(z²) encoded by F : ℂ[X].

Equations

• QuantumAlg.lEval L F x = Complex.exp (-(↑(↑L * x / 2) * Complex.I)) * Polynomial.eval (Complex.exp (↑x * Complex.I)) F

theorem QuantumAlg.lEval_C_mul (L : ℕ) (c : ℂ) (F : Polynomial ℂ) (x : ℝ) : lEval L (Polynomial.C c * F) x = c * lEval L F x

theorem QuantumAlg.lEval_add (L : ℕ) (F G : Polynomial ℂ) (x : ℝ) : lEval L (F + G) x = lEval L F x + lEval L G x

theorem QuantumAlg.lEval_sub (L : ℕ) (F G : Polynomial ℂ) (x : ℝ) : lEval L (F - G) x = lEval L F x - lEval L G x

theorem QuantumAlg.lEval_succ (L : ℕ) (F : Polynomial ℂ) (x : ℝ) : lEval (L + 1) F x = Complex.exp (-(↑(x / 2) * Complex.I)) * lEval L F x

Raising the parity budget multiplies the encoded value by e^{-ix/2}.

theorem QuantumAlg.lEval_succ_X_mul (L : ℕ) (F : Polynomial ℂ) (x : ℝ) : lEval (L + 1) (Polynomial.X * F) x = Complex.exp (↑(x / 2) * Complex.I) * lEval L F x

Raising the budget while multiplying by X multiplies by e^{ix/2}.

theorem QuantumAlg.lEval_zero_C (c : ℂ) (x : ℝ) : lEval 0 (Polynomial.C c) x = c

The encoded value of a constant at budget 0.

theorem QuantumAlg.conj_lEval {L : ℕ} {F : Polynomial ℂ} (hF : F.natDegree ≤ L) (x : ℝ) : (starRingEnd ℂ) (lEval L F x) = lEval L (Polynomial.reflect L (conjP F)) x

Conjugating the encoded value reflects the conjugated coefficients.

Gates and products

noncomputable def QuantumAlg.qspYZY (θ₀ : ℝ) (θs : List ℝ) (x : ℝ) : Gate 1

The YZY QNN U^{YZY}_{θ,L}(x) = R_Y(θ₀)·∏_{j=1}^L R_Z(x)·R_Y(θ_j) [YYLW22, neurips_2022.tex:266].

Equations

• QuantumAlg.qspYZY θ₀ θs x = List.foldl (fun (U : QuantumAlg.Gate 1) (θ : ℝ) => U * (QuantumAlg.rotZStd x * QuantumAlg.rotY θ)) (QuantumAlg.rotY θ₀) θs

@[simp]

theorem QuantumAlg.qspYZY_nil (θ₀ x : ℝ) : qspYZY θ₀ [] x = rotY θ₀

theorem QuantumAlg.qspYZY_concat (θ₀ : ℝ) (θs : List ℝ) (θ x : ℝ) : qspYZY θ₀ (θs ++ [θ]) x = qspYZY θ₀ θs x * (rotZStd x * rotY θ)

noncomputable def QuantumAlg.qspYZZYZ (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) (x : ℝ) : Gate 1

The YZZYZ (W-Z-W) QNN U^{WZW}_{θ,φ,L}(x) = R_Z(φ)·W(θ₀,φ₀)·∏_{j=1}^L R_Z(x)·W(θ_j,φ_j) with trainable blocks W(θ,φ) = R_Y(θ)·R_Z(φ) [YYLW22, neurips_2022.tex:316].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumAlg.qspYZZYZ_nil (φ θ₀ φ₀ x : ℝ) : qspYZZYZ φ θ₀ φ₀ [] x = rotZStd φ * (rotY θ₀ * rotZStd φ₀)

theorem QuantumAlg.qspYZZYZ_concat (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) (p : ℝ × ℝ) (x : ℝ) : qspYZZYZ φ θ₀ φ₀ (ps ++ [p]) x = qspYZZYZ φ θ₀ φ₀ ps x * (rotZStd x * (rotY p.1 * rotZStd p.2))

theorem QuantumAlg.qspYZY_eq_qspYZZYZ (θ₀ : ℝ) (θs : List ℝ) (x : ℝ) : qspYZY θ₀ θs x = qspYZZYZ 0 θ₀ 0 (List.map (fun (t : ℝ) => (t, 0)) θs) x

The YZY product is the φ = φ₀ = 0 special case of the YZZYZ product: it sets every R_Z processing angle in the trainable blocks to 0. This is the gate-level form of "YZZYZ subsumes YZY" — the encoding/normalization theory of the trigonometric family is shared, and the two characterizations differ only in their completeness arguments (one real angle per block vs. three SU(2) angles).

noncomputable def QuantumAlg.qspMatYZ (L : ℕ) (A B : Polynomial ℂ) (x : ℝ) : HilbertOperator 1

The trigonometric QSP target form [[P, -Q], [Q*, P*]] with P = e^{-iLx/2}·A(e^{ix}) and Q = e^{-iLx/2}·B(e^{ix}) [YYLW22, neurips_2022.tex:286].

Equations

• QuantumAlg.qspMatYZ L A B x = !![QuantumAlg.lEval L A x, -QuantumAlg.lEval L B x; (starRingEnd ℂ) (QuantumAlg.lEval L B x), (starRingEnd ℂ) (QuantumAlg.lEval L A x)]

The pair conditions and the one-step recurrence

structure QuantumAlg.IsYZPair (L : ℕ) (A B : Polynomial ℂ) : Prop

Conditions of [YYLW22, neurips_2022.tex:333] in the encoded form: degree bounds and the circle normalization A·reflect L (conjP A) + B·reflect L (conjP B) = X^L, the polynomial form of |P(x)|² + |Q(x)|² = 1 on ℝ (qspYZ_normalization_iff). Degree ≤ L and parity L mod 2 of the Laurent pair are built into the encoding.

• degA : A.degree ≤ ↑L
• degB : B.degree ≤ ↑L
• norm : A * Polynomial.reflect L (conjP A) + B * Polynomial.reflect L (conjP B) = Polynomial.X ^ L

structure QuantumAlg.IsYZYPair (L : ℕ) (A B : Polynomial ℂ) extends QuantumAlg.IsYZPair L A B : Prop

The YZY pair conditions [YYLW22, neurips_2022.tex:283]: an IsYZPair with real coefficients.

• degA : A.degree ≤ ↑L
• degB : B.degree ≤ ↑L
• norm : A * Polynomial.reflect L (conjP A) + B * Polynomial.reflect L (conjP B) = Polynomial.X ^ L
• realA : conjP A = A
• realB : conjP B = B

theorem QuantumAlg.IsYZPair.coeff_A_eq_zero {L : ℕ} {A B : Polynomial ℂ} (h : IsYZPair L A B) {m : ℕ} (hm : L < m) : A.coeff m = 0

theorem QuantumAlg.IsYZPair.coeff_B_eq_zero {L : ℕ} {A B : Polynomial ℂ} (h : IsYZPair L A B) {m : ℕ} (hm : L < m) : B.coeff m = 0

theorem QuantumAlg.IsYZPair.natDegA {L : ℕ} {A B : Polynomial ℂ} (h : IsYZPair L A B) : A.natDegree ≤ L

theorem QuantumAlg.IsYZPair.natDegB {L : ℕ} {A B : Polynomial ℂ} (h : IsYZPair L A B) : B.natDegree ≤ L

theorem QuantumAlg.isYZPair_of_coeff {L : ℕ} {A B : Polynomial ℂ} (hA : ∀ (m : ℕ), L < m → A.coeff m = 0) (hB : ∀ (m : ℕ), L < m → B.coeff m = 0) (norm : A * Polynomial.reflect L (conjP A) + B * Polynomial.reflect L (conjP B) = Polynomial.X ^ L) : IsYZPair L A B

Build the degree conditions from coefficient bounds.

Soundness of the YZY and YZZYZ forms

theorem QuantumAlg.qspYZZYZ_forward (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) : ∃ (A : Polynomial ℂ) (B : Polynomial ℂ), IsYZPair ps.length A B ∧ ∀ (x : ℝ), (qspYZZYZ φ θ₀ φ₀ ps x).op = qspMatYZ ps.length A B x

Soundness for the YZZYZ form: every qspYZZYZ product realizes the target form for a pair satisfying the conditions [YYLW22, neurips_2022.tex:333, forward direction].

theorem QuantumAlg.qspYZY_forward (θ₀ : ℝ) (θs : List ℝ) : ∃ (A : Polynomial ℂ) (B : Polynomial ℂ), IsYZYPair θs.length A B ∧ ∀ (x : ℝ), (qspYZY θ₀ θs x).op = qspMatYZ θs.length A B x

Soundness for the YZY form: every qspYZY product realizes the target form for a real pair satisfying the conditions [YYLW22, neurips_2022.tex:283, forward direction].

Normalization on the circle

theorem QuantumAlg.qspYZ_normalization_iff {L : ℕ} {A B : Polynomial ℂ} (hA : A.natDegree ≤ L) (hB : B.natDegree ≤ L) : A * Polynomial.reflect L (conjP A) + B * Polynomial.reflect L (conjP B) = Polynomial.X ^ L ↔ ∀ (x : ℝ), lEval L A x * (starRingEnd ℂ) (lEval L A x) + lEval L B x * (starRingEnd ℂ) (lEval L B x) = 1

The polynomial normalization identity is equivalent to the pointwise circle normalization |P(x)|² + |Q(x)|² = 1 on ℝ [YYLW22, neurips_2022.tex:288].

Completeness (converse direction)

Degree-reduction induction following [YYLW22, neurips_2022.tex:848]: the norm identity forces the edge-coefficient relation a₀·a*_{L+1} + b₀·b*_{L+1} = 0 (IsYZPair.edge_rel), so some unit pair (v, w) with real product kills both the top coefficient of v·A + w·B and the bottom coefficient of v*·B - w*·A (exists_unstep_vw); the inverse recurrence then factors the pair through one trainable block (isYZPair_unstep), which is realized by angles via exists_rotYZ_angles.

theorem QuantumAlg.qspYZZYZ_converse (L : ℕ) (A B : Polynomial ℂ) : IsYZPair L A B → ∃ (φ : ℝ) (θ₀ : ℝ) (φ₀ : ℝ) (ps : List (ℝ × ℝ)), ps.length = L ∧ ∀ (x : ℝ), (qspYZZYZ φ θ₀ φ₀ ps x).op = qspMatYZ L A B x

Completeness for the YZZYZ form [YYLW22, neurips_2022.tex:848, converse direction]: every IsYZPair pair is realized by some angle sequence with exactly L encoding blocks.

theorem QuantumAlg.qspYZY_converse (L : ℕ) (A B : Polynomial ℂ) : IsYZYPair L A B → ∃ (θ₀ : ℝ) (θs : List ℝ), θs.length = L ∧ ∀ (x : ℝ), (qspYZY θ₀ θs x).op = qspMatYZ L A B x

Completeness for the YZY form [YYLW22, neurips_2022.tex:702, converse direction].

The characterization theorems

theorem QuantumAlg.qspYZZYZ_mem_unitaryGroup (φ θ₀ φ₀ : ℝ) (ps : List (ℝ × ℝ)) (x : ℝ) : (qspYZZYZ φ θ₀ φ₀ ps x).op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

theorem QuantumAlg.qspYZY_mem_unitaryGroup (θ₀ : ℝ) (θs : List ℝ) (x : ℝ) : (qspYZY θ₀ θs x).op ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

theorem QuantumAlg.TrigonometricQuantumSignalProcessing.main (L : ℕ) (A B : Polynomial ℂ) : IsYZPair L A B ↔ ∃ (φ : ℝ) (θ₀ : ℝ) (φ₀ : ℝ) (ps : List (ℝ × ℝ)), ps.length = L ∧ ∀ (x : ℝ), (qspYZZYZ φ θ₀ φ₀ ps x).op = qspMatYZ L A B x

Trigonometric QSP, YZZYZ (W-Z-W) form [YYLW22, neurips_2022.tex:333] (lem:qnn_yzzyz, encoded form): a pair (A, B) satisfies the degree and normalization conditions IsYZPair L iff some angles (φ, θ₀, φ₀, ps) with L encoding gates realize the matrix form [[P, -Q], [Q*, P*]] with P = e^{-iLx/2}·A(e^{ix}) and Q = e^{-iLx/2}·B(e^{ix}) for all x : ℝ.

theorem QuantumAlg.TrigonometricQuantumSignalProcessing.main_yzy (L : ℕ) (A B : Polynomial ℂ) : IsYZYPair L A B ↔ ∃ (θ₀ : ℝ) (θs : List ℝ), θs.length = L ∧ ∀ (x : ℝ), (qspYZY θ₀ θs x).op = qspMatYZ L A B x

Trigonometric QSP, YZY form [YYLW22, neurips_2022.tex:283] (lem:qnn_yzy, encoded form): real-coefficient pairs IsYZYPair L are exactly those realized by R_Y angles (θ₀, θs) with L encoding gates.