Quantum signal processing (single qubit) — Chebyshev basis

The Chebyshev-basis single-qubit QSP characterizations: the reflection-derived O-convention of [Lin22, hermfunc.tex:1103] and the Wx-convention (XZX form) of [GSLW19, BlockHam.tex:295]. Both interleave a fixed one-parameter signal rotation with tunable e^{iφZ} processing rotations (in Core.Components.Gates) and characterize exactly which SU(2)-valued polynomial transforms of the signal x ∈ [-1,1] are achievable.

O-convention: the signal operator is O(x) = [[x, -√(1-x²)], [√(1-x²), x]] and the QSP sequence with phase factors (φ₀, …, φ_d) is U_Φ(x) = e^{iφ₀Z} · ∏_{j=1}^d (O(x) e^{iφ_j Z}).

LeanPool.LeanQuantumAlg.ReflectionBasedQuantumSignalProcessing.main [Lin22, hermfunc.tex:1118]: U_Φ(x) takes the form [[P(x), -Q(x)√(1-x²)], [Q*(x)√(1-x²), P*(x)]] for all x ∈ [-1,1] for some phase factors iff (P, Q) is an IsQSPPair d, i.e.

1. deg P ≤ d and Q.degree < d,
2. P has parity d mod 2 and Q has parity (d-1) mod 2,
3. P·P* + (1-X²)·Q·Q* = 1 (* conjugates the coefficients; conjP).

Condition 3 is equivalent to the pointwise |P(x)|² + (1-x²)|Q(x)|² = 1 on the infinite set [-1,1] (LeanPool.LeanQuantumAlg.qsp_normalization_iff).

The Wx-convention replaces O(x) by W(x) = e^{i·arccos(x)·X}; the fixed conjugation W(x) = e^{-i(π/4)Z}·O(x)·e^{i(π/4)Z} [Lin22, hermfunc.tex:1279] transports the characterization (LeanPool.LeanQuantumAlg.ReflectionBasedQuantumSignalProcessing.main_wx) with the same pair conditions IsQSPPair.

This module is one half of the single-qubit QSP development; the Fourier-basis (trigonometric YZY/YZZYZ) forms live in LeanPool.LeanQuantumAlg.Primitives.QSP.Fourier, and LeanPool.LeanQuantumAlg.Primitives.QSP re-exports both.

Main results

• LeanPool.LeanQuantumAlg.qspO_mem_unitaryGroup — U_Φ(x) is unitary for x ∈ [-1,1].
• LeanPool.LeanQuantumAlg.qspO_forward / LeanPool.LeanQuantumAlg.qspO_converse — soundness and completeness of the O-convention.
• LeanPool.LeanQuantumAlg.ReflectionBasedQuantumSignalProcessing.main — the O-convention characterization (registered target entry point).
• LeanPool.LeanQuantumAlg.ReflectionBasedQuantumSignalProcessing.main_wx — the Wx-convention (XZX) characterization.

Pinned Mathlib API: Polynomial.coeff_X_mul, Polynomial.coeff_mul, Polynomial.degree_le_iff_coeff_zero, Polynomial.degree_lt_iff_coeff_zero, Polynomial.eq_of_infinite_eval_eq, Complex.exp_mul_I, Complex.mul_conj, Set.Icc.infinite, List.reverseRecOn.

Signal operator (the processing rotation rotZ is in

Core.Components.Gates)

noncomputable def QuantumAlg.signalO (x : ℝ) : HilbertOperator 1

The signal rotation O(x) = [[x, -√(1-x²)], [√(1-x²), x]] [Lin22, hermfunc.tex:1103]; equals U_A(x)·Z for the reflection U_A(x) of [GSLW19, BlockHam.tex:488].

Equations

• QuantumAlg.signalO x = !![↑x, -↑√(1 - x ^ 2); ↑√(1 - x ^ 2), ↑x]

noncomputable def QuantumAlg.qspO (φ₀ : ℝ) (φs : List ℝ) (x : ℝ) : HilbertOperator 1

The QSP sequence U_Φ(x) = e^{iφ₀Z} ∏_j (O(x) e^{iφ_jZ}) with phase factors Φ = (φ₀, φs) [Lin22, hermfunc.tex:1121].

Equations

• QuantumAlg.qspO φ₀ φs x = List.foldl (fun (U : QuantumAlg.HilbertOperator 1) (φ : ℝ) => U * (QuantumAlg.signalO x * (QuantumAlg.rotZ φ).op)) (QuantumAlg.rotZ φ₀).op φs

@[simp]

theorem QuantumAlg.qspO_nil (φ₀ x : ℝ) : qspO φ₀ [] x = (rotZ φ₀).op

theorem QuantumAlg.qspO_concat (φ₀ : ℝ) (φs : List ℝ) (φ x : ℝ) : qspO φ₀ (φs ++ [φ]) x = qspO φ₀ φs x * (signalO x * (rotZ φ).op)

theorem QuantumAlg.signalO_mem_unitaryGroup {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : signalO x ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

theorem QuantumAlg.qspO_mem_unitaryGroup (φ₀ : ℝ) (φs : List ℝ) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : qspO φ₀ φs x ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

The QSP form and its one-step recurrence

noncomputable def QuantumAlg.qspMat (P Q : Polynomial ℂ) (x : ℝ) : HilbertOperator 1

The target matrix form [[P(x), -Q(x)s], [Q*(x)s, P*(x)]], s = √(1-x²) [Lin22, hermfunc.tex:1121].

Equations

• QuantumAlg.qspMat P Q x = !![Polynomial.eval (↑x) P, -Polynomial.eval (↑x) Q * ↑√(1 - x ^ 2); (starRingEnd ℂ) (Polynomial.eval (↑x) Q) * ↑√(1 - x ^ 2), (starRingEnd ℂ) (Polynomial.eval (↑x) P)]

The QSP pair conditions

structure QuantumAlg.IsQSPPair (d : ℕ) (P Q : Polynomial ℂ) : Prop

Conditions (1)–(3) of the QSP theorem [Lin22, hermfunc.tex:1127] for degree budget d: degree bounds (Q.degree < d encodes deg Q ≤ d-1, with Q = 0 forced when d = 0), parities, and the polynomial normalization identity (* = coefficient conjugation conjP).

• degP : P.degree ≤ ↑d
• degQ : Q.degree < ↑d
• parP : HasParity P d
• parQ : HasParity Q (d + 1)
• norm : P * conjP P + (1 - Polynomial.X ^ 2) * (Q * conjP Q) = 1

theorem QuantumAlg.IsQSPPair.coeff_P_eq_zero {d : ℕ} {P Q : Polynomial ℂ} (h : IsQSPPair d P Q) {m : ℕ} (hm : d < m) : P.coeff m = 0

theorem QuantumAlg.IsQSPPair.coeff_Q_eq_zero {d : ℕ} {P Q : Polynomial ℂ} (h : IsQSPPair d P Q) {m : ℕ} (hm : d ≤ m) : Q.coeff m = 0

theorem QuantumAlg.isQSPPair_of_coeff {d : ℕ} {P Q : Polynomial ℂ} (hP : ∀ (m : ℕ), d < m → P.coeff m = 0) (hQ : ∀ (m : ℕ), d ≤ m → Q.coeff m = 0) (parP : HasParity P d) (parQ : HasParity Q (d + 1)) (norm : P * conjP P + (1 - Polynomial.X ^ 2) * (Q * conjP Q) = 1) : IsQSPPair d P Q

Build the degree conditions from coefficient bounds.

Soundness (forward direction)

theorem QuantumAlg.qspO_forward (φ₀ : ℝ) (φs : List ℝ) : ∃ (P : Polynomial ℂ) (Q : Polynomial ℂ), IsQSPPair φs.length P Q ∧ ∀ x ∈ Set.Icc (-1) 1, qspO φ₀ φs x = qspMat P Q x

Soundness of QSP [Lin22, hermfunc.tex:1139]: every QSP product U_Φ(x) takes the form qspMat P Q x on [-1,1] for a pair (P, Q) satisfying the degree, parity, and normalization conditions.

Completeness (converse direction)

Degree-reduction induction [Lin22, hermfunc.tex:1212]: given an IsQSPPair pair with deg P = d ≥ 1, a phase φ with e^{2iφ} q_{d-1} = p_d makes the inverse recurrence drop the degree by one; if instead both leading coefficients vanish, the pair already satisfies the conditions two levels down and the sequence is padded with the no-op pair O(x)e^{i(π/2)Z} · O(x)e^{-i(π/2)Z} = 1.

Padding with a no-op pair

Completeness and the characterization

theorem QuantumAlg.qspO_converse (d : ℕ) (P Q : Polynomial ℂ) (h : IsQSPPair d P Q) : ∃ (φ₀ : ℝ) (φs : List ℝ), φs.length = d ∧ ∀ x ∈ Set.Icc (-1) 1, qspO φ₀ φs x = qspMat P Q x

Completeness of QSP [Lin22, hermfunc.tex:1212]: every pair satisfying the degree, parity, and normalization conditions is realized by a QSP sequence with exactly d signal operators.

theorem QuantumAlg.qsp_normalization_iff (P Q : Polynomial ℂ) : P * conjP P + (1 - Polynomial.X ^ 2) * (Q * conjP Q) = 1 ↔ ∀ x ∈ Set.Icc (-1) 1, Polynomial.eval (↑x) P * (starRingEnd ℂ) (Polynomial.eval (↑x) P) + (1 - ↑x ^ 2) * (Polynomial.eval (↑x) Q * (starRingEnd ℂ) (Polynomial.eval (↑x) Q)) = 1

The polynomial normalization identity is equivalent to the pointwise normalization |P(x)|² + (1-x²)|Q(x)|² = 1 on [-1,1] [Lin22, hermfunc.tex:1134].

theorem QuantumAlg.ReflectionBasedQuantumSignalProcessing.main (d : ℕ) (P Q : Polynomial ℂ) : IsQSPPair d P Q ↔ ∃ (φ₀ : ℝ) (φs : List ℝ), φs.length = d ∧ ∀ x ∈ Set.Icc (-1) 1, qspO φ₀ φs x = qspMat P Q x

Quantum signal processing, reflection convention [Lin22, hermfunc.tex:1118] ([GSLW19, BlockHam.tex:313] in the W-convention): a pair (P, Q) satisfies the degree, parity, and normalization conditions IsQSPPair d iff some phase factors (φ₀, φs) with d signal operators realize the matrix form [[P(x), -Q(x)√(1-x²)], [Q*(x)√(1-x²), P*(x)]] on [-1,1].

The Wx-convention (XZX form)

The Wx-convention of [GSLW19, BlockHam.tex:295] uses the signal rotation W(x) = e^{i·arccos(x)·X} in place of O(x). The two are related by the fixed conjugation W(x) = e^{-i(π/4)Z} · O(x) · e^{i(π/4)Z} [Lin22, hermfunc.tex:1279], so the characterization [GSLW19, BlockHam.tex:313] (thm:basicCharacterisation) transports verbatim from qsp_reflection_iff with the same pair conditions IsQSPPair.

noncomputable def QuantumAlg.signalW (x : ℝ) : HilbertOperator 1

The Wx signal rotation W(x) = [[x, i√(1-x²)], [i√(1-x²), x]] = e^{i·arccos(x)·X} [GSLW19, BlockHam.tex:295].

Equations

• QuantumAlg.signalW x = !![↑x, Complex.I * ↑√(1 - x ^ 2); Complex.I * ↑√(1 - x ^ 2), ↑x]

noncomputable def QuantumAlg.qspW (φ₀ : ℝ) (φs : List ℝ) (x : ℝ) : HilbertOperator 1

The Wx-convention QSP sequence e^{iφ₀Z} ∏_j (W(x) e^{iφ_jZ}) [GSLW19, BlockHam.tex:317].

Equations

• QuantumAlg.qspW φ₀ φs x = List.foldl (fun (U : QuantumAlg.HilbertOperator 1) (φ : ℝ) => U * (QuantumAlg.signalW x * (QuantumAlg.rotZ φ).op)) (QuantumAlg.rotZ φ₀).op φs

@[simp]

theorem QuantumAlg.qspW_nil (φ₀ x : ℝ) : qspW φ₀ [] x = (rotZ φ₀).op

theorem QuantumAlg.qspW_concat (φ₀ : ℝ) (φs : List ℝ) (φ x : ℝ) : qspW φ₀ (φs ++ [φ]) x = qspW φ₀ φs x * (signalW x * (rotZ φ).op)

noncomputable def QuantumAlg.qspMatW (P Q : Polynomial ℂ) (x : ℝ) : HilbertOperator 1

The Wx target form [[P(x), iQ(x)s], [iQ*(x)s, P*(x)]], s = √(1-x²) [GSLW19, BlockHam.tex:313].

Equations

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

theorem QuantumAlg.signalW_mem_unitaryGroup {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : signalW x ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

theorem QuantumAlg.qspW_mem_unitaryGroup (φ₀ : ℝ) (φs : List ℝ) {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : qspW φ₀ φs x ∈ Matrix.unitaryGroup (Fin (2 ^ 1)) ℂ

theorem QuantumAlg.qspW_form_iff (φ₀ : ℝ) (φs : List ℝ) (P Q : Polynomial ℂ) (x : ℝ) : qspW φ₀ φs x = qspMatW P Q x ↔ qspO φ₀ φs x = qspMat P Q x

Pointwise, the Wx form holds iff the reflection form holds (conjugation by the unit e^{i(π/4)Z}).

theorem QuantumAlg.ReflectionBasedQuantumSignalProcessing.main_wx (d : ℕ) (P Q : Polynomial ℂ) : IsQSPPair d P Q ↔ ∃ (φ₀ : ℝ) (φs : List ℝ), φs.length = d ∧ ∀ x ∈ Set.Icc (-1) 1, qspW φ₀ φs x = qspMatW P Q x

Quantum signal processing, Wx-convention (XZX form) [GSLW19, BlockHam.tex:313] (thm:basicCharacterisation): a pair (P, Q) satisfies IsQSPPair d iff some phase factors (φ₀, φs) with d signal operators realize the matrix form [[P(x), iQ(x)√(1-x²)], [iQ*(x)√(1-x²), P*(x)]] on [-1,1].