Polynomial helper lemmas (quantum-free)

Generic ℂ[X] lemmas used by the QSP development, factored out so they carry no dependency on the quantum framework:

• conjP — coefficient-conjugate of a polynomial (the P* of the QSP literature) and its ring/eval lemmas;
• HasParity — the predicate "all nonzero coefficients sit in degrees of a fixed parity" and its closure lemmas;
• total coefficient formulas (coeff_X_mul', coeff_X_sq_mul) and bounded product-coefficient lemmas;
• Polynomial.reflect coefficient/evaluation lemmas;
• eq_of_circle_eval_eq — two polynomials agreeing on the unit circle are equal.

These are upstream candidates for Mathlib; nothing here mentions Gate/PureState.

Coefficient-conjugate polynomials

noncomputable def QuantumAlg.conjP (P : Polynomial ℂ) : Polynomial ℂ

conjP P conjugates every coefficient of P : ℂ[X]; this is the P* of the QSP literature (for real x, (conjP P).eval x = conj (P.eval x)).

Equations

• QuantumAlg.conjP P = Polynomial.map (starRingEnd ℂ) P

@[simp]

theorem QuantumAlg.conjP_coeff (P : Polynomial ℂ) (k : ℕ) : (conjP P).coeff k = (starRingEnd ℂ) (P.coeff k)

@[simp]

theorem QuantumAlg.conjP_zero : conjP 0 = 0

@[simp]

theorem QuantumAlg.conjP_one : conjP 1 = 1

@[simp]

theorem QuantumAlg.conjP_X : conjP Polynomial.X = Polynomial.X

@[simp]

theorem QuantumAlg.conjP_C (c : ℂ) : conjP (Polynomial.C c) = Polynomial.C ((starRingEnd ℂ) c)

theorem QuantumAlg.conjP_add (P Q : Polynomial ℂ) : conjP (P + Q) = conjP P + conjP Q

theorem QuantumAlg.conjP_sub (P Q : Polynomial ℂ) : conjP (P - Q) = conjP P - conjP Q

theorem QuantumAlg.conjP_mul (P Q : Polynomial ℂ) : conjP (P * Q) = conjP P * conjP Q

theorem QuantumAlg.conjP_pow (P : Polynomial ℂ) (n : ℕ) : conjP (P ^ n) = conjP P ^ n

@[simp]

theorem QuantumAlg.conjP_conjP (P : Polynomial ℂ) : conjP (conjP P) = P

theorem QuantumAlg.conjP_eval_ofReal (P : Polynomial ℂ) (x : ℝ) : Polynomial.eval (↑x) (conjP P) = (starRingEnd ℂ) (Polynomial.eval (↑x) P)

Evaluating the coefficient-conjugate at a real point conjugates the value.

Parity of polynomials

HasParity P p says every nonzero coefficient of P sits in a degree congruent to p modulo 2 ("P has parity p mod 2" in [Lin22, hermfunc.tex:1132]). The zero polynomial has every parity.

def QuantumAlg.HasParity (P : Polynomial ℂ) (p : ℕ) : Prop

All nonzero coefficients of P are in degrees ≡ p (mod 2).

Equations

• QuantumAlg.HasParity P p = ∀ (k : ℕ), P.coeff k ≠ 0 → k % 2 = p % 2

theorem QuantumAlg.HasParity.coeff_eq_zero {P : Polynomial ℂ} {p : ℕ} (h : HasParity P p) {k : ℕ} (hk : k % 2 ≠ p % 2) : P.coeff k = 0

theorem QuantumAlg.hasParity_zero (p : ℕ) : HasParity 0 p

theorem QuantumAlg.hasParity_C (c : ℂ) {p : ℕ} (hp : p % 2 = 0) : HasParity (Polynomial.C c) p

theorem QuantumAlg.HasParity.add {P Q : Polynomial ℂ} {p : ℕ} (hP : HasParity P p) (hQ : HasParity Q p) : HasParity (P + Q) p

theorem QuantumAlg.HasParity.neg {P : Polynomial ℂ} {p : ℕ} (hP : HasParity P p) : HasParity (-P) p

theorem QuantumAlg.HasParity.sub {P Q : Polynomial ℂ} {p : ℕ} (hP : HasParity P p) (hQ : HasParity Q p) : HasParity (P - Q) p

theorem QuantumAlg.HasParity.C_mul {P : Polynomial ℂ} {p : ℕ} (c : ℂ) (hP : HasParity P p) : HasParity (Polynomial.C c * P) p

theorem QuantumAlg.HasParity.conjP {P : Polynomial ℂ} {p : ℕ} (hP : HasParity P p) : HasParity (QuantumAlg.conjP P) p

theorem QuantumAlg.HasParity.congr {P : Polynomial ℂ} {p q : ℕ} (hP : HasParity P p) (hpq : p % 2 = q % 2) : HasParity P q

Parity only depends on p modulo 2.

theorem QuantumAlg.coeff_X_mul' (P : Polynomial ℂ) (n : ℕ) : (Polynomial.X * P).coeff n = if n = 0 then 0 else P.coeff (n - 1)

Total coefficient formula for X * P.

theorem QuantumAlg.coeff_X_sq_mul (P : Polynomial ℂ) (n : ℕ) : (Polynomial.X ^ 2 * P).coeff n = if n < 2 then 0 else P.coeff (n - 2)

Total coefficient formula for X^2 * P.

theorem QuantumAlg.HasParity.X_mul {P : Polynomial ℂ} {p : ℕ} (hP : HasParity P p) : HasParity (Polynomial.X * P) (p + 1)

theorem QuantumAlg.HasParity.one_sub_X_sq_mul {P : Polynomial ℂ} {p : ℕ} (hP : HasParity P p) : HasParity ((1 - Polynomial.X ^ 2) * P) p

Bounded product coefficients

theorem QuantumAlg.coeff_mul_at_bound_add {P Q : Polynomial ℂ} {a b n : ℕ} (hn : n = a + b) (hP : ∀ (m : ℕ), a < m → P.coeff m = 0) (hQ : ∀ (m : ℕ), b < m → Q.coeff m = 0) : (P * Q).coeff n = P.coeff a * Q.coeff b

Product coefficient at the sum of two coefficient bounds: only the top-times-top term survives.

theorem QuantumAlg.coeff_mul_eq_zero_of_bound_add {P Q : Polynomial ℂ} {a b n : ℕ} (hn : a + b < n) (hP : ∀ (m : ℕ), a < m → P.coeff m = 0) (hQ : ∀ (m : ℕ), b < m → Q.coeff m = 0) : (P * Q).coeff n = 0

Product coefficient above the sum of two coefficient bounds vanishes.

Reflection of coefficients

theorem QuantumAlg.coeff_reflect_of_le {F : Polynomial ℂ} {N m : ℕ} (hm : m ≤ N) : (Polynomial.reflect N F).coeff m = F.coeff (N - m)

theorem QuantumAlg.coeff_reflect_eq_zero {F : Polynomial ℂ} {N m : ℕ} (hF : F.natDegree ≤ N) (hm : N < m) : (Polynomial.reflect N F).coeff m = 0

theorem QuantumAlg.reflect_sub (F G : Polynomial ℂ) (N : ℕ) : Polynomial.reflect N (F - G) = Polynomial.reflect N F - Polynomial.reflect N G

theorem QuantumAlg.reflect_add' (F G : Polynomial ℂ) (N : ℕ) : Polynomial.reflect N (F + G) = Polynomial.reflect N F + Polynomial.reflect N G

theorem QuantumAlg.reflect_succ {F : Polynomial ℂ} {L : ℕ} (hF : F.natDegree ≤ L) : Polynomial.reflect (L + 1) F = Polynomial.X * Polynomial.reflect L F

reflect (L+1) F = X · reflect L F for natDegree F ≤ L.

theorem QuantumAlg.reflect_X_mul {F : Polynomial ℂ} {L : ℕ} (hF : F.natDegree ≤ L) : Polynomial.reflect (L + 1) (Polynomial.X * F) = Polynomial.reflect L F

reflect (L+1) (X·F) = reflect L F for natDegree F ≤ L.

theorem QuantumAlg.eval_reflect {F : Polynomial ℂ} {L : ℕ} (hF : F.natDegree ≤ L) {z : ℂ} (hz : z ≠ 0) : Polynomial.eval z (Polynomial.reflect L F) = z ^ L * Polynomial.eval z⁻¹ F

Evaluation of a reflection: (reflect L F)(z) = z^L · F(z⁻¹).

theorem QuantumAlg.reflect_zero_C (r : ℂ) : Polynomial.reflect 0 (Polynomial.C r) = Polynomial.C r

Evaluation on the unit circle

theorem QuantumAlg.eq_of_circle_eval_eq {F G : Polynomial ℂ} (h : ∀ (x : ℝ), Polynomial.eval (Complex.exp (↑x * Complex.I)) F = Polynomial.eval (Complex.exp (↑x * Complex.I)) G) : F = G

Two polynomials agreeing on the unit circle are equal (the circle is an infinite evaluation set).