Evaluation of finite-support ℓ¹ coefficient sequences

These lemmas translate the normalized sequence factorization into the monic polynomial identity used by the public preparation witness.

theorem ClassicalComplexWPT.evalL1PowerSeries_smul (c : ℂ) (a : ↥L1Sequence) (w : ℂ) : evalL1PowerSeries (c • a) w = c * evalL1PowerSeries a w

theorem ClassicalComplexWPT.evalL1PowerSeries_monomialSeq (d : ℕ) {w : ℂ} (hw : ‖w‖ < 1) : evalL1PowerSeries (monomialSeq d) w = w ^ d

theorem ClassicalComplexWPT.evalL1PowerSeries_eq_sum_fin_of_highShift_eq_zero (d : ℕ) (a : ↥L1Sequence) (ha : seqHighShift d a = 0) {w : ℂ} (hw : ‖w‖ < 1) : evalL1PowerSeries a w = ∑ i : Fin d, ↑a ↑i * w ^ ↑i