LeanFun RevOLVER

2.9 Rootfinding with colleague matrices

The roots of a polynomial can be recovered as eigenvalues of a finite multiplication matrix. Choosing the Chebyshev basis gives the colleague matrix.

2.9.1 Multiplication modulo a polynomial

Let \(K\) be a field and let \(P_j\) have degree \(j\). Every polynomial of degree below \(n\) has coordinates in \(P_0,\ldots ,P_{n-1}\). In \(K[x]/(g)\), multiplication by \(x\) is followed by taking the remainder modulo \(g\). The matrix columns are the coordinates of these basis images.

Definition 2.9.1 Comrade matrix in a degree-graded basis

✓ 🤖

#

For monic \(g\) of degree \(n\), give \(K[x]/(g)\) the basis whose coordinates are the sequence coordinates \([r]_0,\ldots ,[r]_{n-1}\) of the remainder \(r\) modulo \(g\); by Theorem 2.9.3 its vectors are the images of \(P_0,\ldots ,P_{n-1}\). Define \(C_g\) to be the matrix of multiplication by \(x\) in this basis, with basis images as columns.

References: [Bar75]; [ATAP, Chapter 18].

Lean Formalisation

def Polynomial.Sequence.quotientBasis.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {g : Polynomial K}
  (hg : g.Monic) : Module.Basis (Fin g.natDegree) K (AdjoinRoot g)

Lean definition

/-- The first deg(g) members form a basis of K[X]/(g), for monic g. -/
noncomputable def quotientBasis {g : K[X]} (hg : g.Monic) :
    Basis (Fin g.natDegree) K (AdjoinRoot g) :=
  Basis.ofEquivFun
    { toFun := fun x i ↦ (P.basis P.isUnit_leadingCoeff).repr (AdjoinRoot.modByMonicHom hg x) i
      invFun := fun v ↦ AdjoinRoot.mk g (∑ i, v i • P i)
      map_add' := by intro x y; ext i; simp
      map_smul' := by intro a x; ext i; simp
      left_inv := by
        intro x
        dsimp only
        rw [P.sum_fin_repr (by
          rw [← degree_eq_natDegree hg.ne_zero]
          induction x using AdjoinRoot.induction_on with
          | ih p => exact degree_modByMonic_lt p hg)]
        exact AdjoinRoot.mk_leftInverse hg x
      right_inv := by
        intro v
        funext i
        dsimp only
        rw [AdjoinRoot.modByMonicHom_mk,
          (modByMonic_eq_self_iff hg).mpr (by
            rw [degree_eq_natDegree hg.ne_zero]
            exact P.degree_sum_fin_lt _ v)]
        simp only [map_sum, map_smul, Finsupp.finsetSum_apply, Finsupp.smul_apply, smul_eq_mul]
        have hb (j : Fin g.natDegree) :
            (P.basis P.isUnit_leadingCoeff).repr (P j) = Finsupp.single (j : ℕ) 1 := by
          rw [← P.basis_eq_self P.isUnit_leadingCoeff j, Basis.repr_self]
        simp only [hb, Finsupp.single_apply, ← Fin.ext_iff, mul_ite, mul_one, mul_zero]
        simp }

1 related Lean declaration

def Polynomial.Sequence.comradeMatrix.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {g : Polynomial K}
  (hg : g.Monic) : Matrix (Fin g.natDegree) (Fin g.natDegree) K

Lean definition

/-- The comrade matrix has columns given by multiplication by X modulo g. -/
noncomputable def comradeMatrix {g : K[X]} (hg : g.Monic) :
    Matrix (Fin g.natDegree) (Fin g.natDegree) K :=
  Algebra.leftMulMatrix (P.quotientBasis hg) (AdjoinRoot.root g)

Theorem 2.9.2 Comrade characteristic polynomial and final-column correction

✓ 🤖

#

The characteristic polynomial of \(C_g\) is \(g\), and its spectrum over \(K\) is the set of roots of \(g\) in \(K\). Write \([q]_i\) for sequence coordinates and \([x^n]q\) for a monomial coefficient. Its entries are

\[ (C_g)_{ij}=[xP_j]_i-([x^n](xP_j))[g]_i,\qquad 0\le i,j{\lt}n. \]

The correction vanishes for \(j+1{\lt}n\), so only the final column changes. This includes arbitrary monic input polynomials, with repeated roots allowed.

References: [Bar75]; [ATAP, Chapter 18].

Lean Formalisation

theorem Polynomial.Sequence.comradeMatrix_apply.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {g : Polynomial K}
  (hg : g.Monic) (i j : Fin g.natDegree) : P.comradeMatrix hg i j = ((P.basis ⋯).repr (Polynomial.X * ↑P ↑j %ₘ g)) ↑i

Lean proof

/-- Entries use the existing polynomial coordinates and the monic remainder. -/
theorem comradeMatrix_apply {g : K[X]} (hg : g.Monic) (i j : Fin g.natDegree) :
    P.comradeMatrix hg i j =
      (P.basis P.isUnit_leadingCoeff).repr ((X * P j) %ₘ g) i := by
  rw [comradeMatrix, Algebra.leftMulMatrix_eq_repr_mul, quotientBasis_apply,
    ← AdjoinRoot.mk_X, ← map_mul, quotientBasis_repr, AdjoinRoot.modByMonicHom_mk]

4 related Lean declarations

theorem Polynomial.Sequence.charpoly_comradeMatrix.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {g : Polynomial K}
  (hg : g.Monic) : (P.comradeMatrix hg).charpoly = g

Lean proof

/-- The characteristic polynomial is exactly the monic input polynomial. -/
theorem charpoly_comradeMatrix {g : K[X]} (hg : g.Monic) :
    (P.comradeMatrix hg).charpoly = g := by
  let := (AdjoinRoot.powerBasis' hg).finite
  rw [comradeMatrix, Algebra.leftMulMatrix_apply, LinearMap.charpoly_toMatrix,
    ← LinearMap.charpoly_toMatrix _ (AdjoinRoot.powerBasis hg.ne_zero).basis,
    ← Algebra.leftMulMatrix_apply]
  exact (charpoly_leftMulMatrix (AdjoinRoot.powerBasis hg.ne_zero)).trans
    (AdjoinRoot.minpoly_powerBasis_gen_of_monic hg)

theorem Polynomial.Sequence.mem_spectrum_comradeMatrix_iff.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K)
  {g : Polynomial K} (hg : g.Monic) (x : K) : x ∈ spectrum K (P.comradeMatrix hg) ↔ g.IsRoot x

Lean proof

/-- The matrix spectrum is precisely the roots of the defining polynomial. -/
theorem mem_spectrum_comradeMatrix_iff {g : K[X]} (hg : g.Monic) (x : K) :
    x ∈ spectrum K (P.comradeMatrix hg) ↔ g.IsRoot x := by
  rw [Matrix.mem_spectrum_iff_isRoot_charpoly, P.charpoly_comradeMatrix hg]

theorem Polynomial.Sequence.comradeMatrix_rank_one_entry.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K)
  {g : Polynomial K} (hg : g.Monic) (i j : Fin g.natDegree) :
  P.comradeMatrix hg i j =
    ((P.basis ⋯).repr (Polynomial.X * ↑P ↑j)) ↑i - (Polynomial.X * ↑P ↑j).coeff g.natDegree * ((P.basis ⋯).repr g) ↑i

Lean proof

/-- Explicit rank-one correction to the leading multiplication section.
Only the top-degree coefficient of X times a basis member is removed. -/
theorem comradeMatrix_rank_one_entry {g : K[X]} (hg : g.Monic)
    (i j : Fin g.natDegree) :
    P.comradeMatrix hg i j =
      (P.basis P.isUnit_leadingCoeff).repr (X * P j) i -
        (X * P j).coeff g.natDegree * (P.basis P.isUnit_leadingCoeff).repr g i := by
  have hq : ((X * P j) /ₘ g).natDegree = 0 := by
    rw [natDegree_divByMonic _ hg, natDegree_X_mul (P.ne_zero j), P.natDegree_eq]
    omega
  have heq := congrArg (fun q : K[X] ↦ g * q) (eq_C_of_natDegree_eq_zero hq)
  have hc := congrArg (fun p : K[X] ↦ p.coeff g.natDegree) (modByMonic_add_div (X * P j) g)
  rw [heq, coeff_add, coeff_mul_C, hg.coeff_natDegree,
    coeff_eq_zero_of_degree_lt (by
      rw [← degree_eq_natDegree hg.ne_zero]
      exact degree_modByMonic_lt _ hg), zero_add, one_mul] at hc
  rw [P.comradeMatrix_apply, modByMonic_eq_sub_mul_div, heq, hc, mul_comm g,
    ← smul_eq_C_mul, map_sub, map_smul]
  rfl

theorem Polynomial.Sequence.comradeMatrix_apply_of_lt.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K)
  {g : Polynomial K} (hg : g.Monic) (i j : Fin g.natDegree) (hj : ↑j + 1 < g.natDegree) :
  P.comradeMatrix hg i j = ((P.basis ⋯).repr (Polynomial.X * ↑P ↑j)) ↑i

Lean proof

/-- Every column except the last agrees with ordinary multiplication by X. -/
theorem comradeMatrix_apply_of_lt {g : K[X]} (hg : g.Monic)
    (i j : Fin g.natDegree) (hj : (j : ℕ) + 1 < g.natDegree) :
    P.comradeMatrix hg i j = (P.basis P.isUnit_leadingCoeff).repr (X * P j) i := by
  rw [P.comradeMatrix_rank_one_entry,
    coeff_eq_zero_of_natDegree_lt (by
      rw [natDegree_X_mul (P.ne_zero j), P.natDegree_eq]
      exact hj), zero_mul, sub_zero]

Quotient bases and finite coordinates

Theorem 2.9.3 Comrade basis vectors and coordinates

✓ 🤖

#

The \(i\)th basis vector of \(K[x]/(g)\) is the image of \(P_i\), and the coordinates of an element are the sequence coordinates of its remainder modulo \(g\).

Lean Formalisation

theorem Polynomial.Sequence.quotientBasis_apply.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {g : Polynomial K}
  (hg : g.Monic) (i : Fin g.natDegree) : (P.quotientBasis hg) i = (AdjoinRoot.mk g) (↑P ↑i)

Lean proof

/-- The quotient basis is the image of the original degree-graded sequence. -/
@[simp] theorem quotientBasis_apply {g : K[X]} (hg : g.Monic) (i : Fin g.natDegree) :
    P.quotientBasis hg i = AdjoinRoot.mk g (P i) := by
  simp only [quotientBasis, Basis.coe_ofEquivFun, LinearEquiv.coe_symm_mk, Pi.single_apply]
  simp only [ite_smul, one_smul, zero_smul, Finset.sum_ite_eq', Finset.mem_univ, ite_true]

1 related Lean declaration

theorem Polynomial.Sequence.quotientBasis_repr.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {g : Polynomial K}
  (hg : g.Monic) (x : AdjoinRoot g) (i : Fin g.natDegree) :
  ((P.quotientBasis hg).repr x) i = ((P.basis ⋯).repr ((AdjoinRoot.modByMonicHom hg) x)) ↑i

Lean proof

/-- Coordinates are obtained by taking the polynomial remainder first. -/
@[simp] theorem quotientBasis_repr {g : K[X]} (hg : g.Monic)
    (x : AdjoinRoot g) (i : Fin g.natDegree) :
    (P.quotientBasis hg).repr x i =
      (P.basis P.isUnit_leadingCoeff).repr (AdjoinRoot.modByMonicHom hg x) i := rfl

2.9.2 Chebyshev colleague matrices

In the Chebyshev basis the multiplication recurrence determines all but a correction in the final column. The resulting eigenvalue problem finds the roots of the polynomial.

Theorem 2.9.4 Chebyshev colleague rootfinding

✓ 🤖

#

For every nonzero real polynomial \(p\), define its colleague matrix by applying the comrade construction in the \(T\) basis to \(p/\operatorname {lc}(p)\). Its size is \(\deg p\) and its characteristic polynomial is \(p/\operatorname {lc}(p)\). The entry formula is the final-column correction above, in the full-constant Chebyshev convention. Its real spectrum is the real roots of \(p\); after embedding its entries in \(\mathbb C\), its complex spectrum is all complex roots of \(p\). Repeated roots are allowed.

References: [Goo61]; [ATAP, Theorem 18.1].

Lean Formalisation

theorem Polynomial.Chebyshev.charpoly_colleagueMatrix (p : Polynomial ℝ) (hp : p ≠ 0) :
  (Polynomial.Chebyshev.colleagueMatrix p hp).charpoly = p * Polynomial.C p.leadingCoeff⁻¹

Lean proof

/-- The colleague characteristic polynomial is the input made monic. -/
theorem charpoly_colleagueMatrix (p : ℝ[X]) (hp : p ≠ 0) :
    (colleagueMatrix p hp).charpoly = p * Polynomial.C p.leadingCoeff⁻¹ :=
  (chebyshevTsequence ℝ).charpoly_comradeMatrix (monic_mul_leadingCoeff_inv hp)

5 related Lean declarations

def Polynomial.Chebyshev.colleagueMatrix (p : Polynomial ℝ) (hp : p ≠ 0) :
  Matrix (Fin (p * Polynomial.C p.leadingCoeff⁻¹).natDegree) (Fin (p * Polynomial.C p.leadingCoeff⁻¹).natDegree) ℝ

Lean definition

/-- The colleague matrix of a nonzero real polynomial, after monic scaling.
The zero polynomial is excluded by the characteristic-polynomial theorem. -/
noncomputable def colleagueMatrix (p : ℝ[X]) (hp : p ≠ 0) :
    Matrix (Fin (p * Polynomial.C p.leadingCoeff⁻¹).natDegree)
      (Fin (p * Polynomial.C p.leadingCoeff⁻¹).natDegree) ℝ :=
  (chebyshevTsequence ℝ).comradeMatrix (monic_mul_leadingCoeff_inv hp)

theorem Polynomial.Chebyshev.mem_spectrum_colleagueMatrix_iff (p : Polynomial ℝ) (hp : p ≠ 0) (x : ℝ) :
  x ∈ spectrum ℝ (Polynomial.Chebyshev.colleagueMatrix p hp) ↔ p.IsRoot x

Lean proof

/-- Colleague eigenvalues in the base field are exactly the input roots. -/
theorem mem_spectrum_colleagueMatrix_iff (p : ℝ[X]) (hp : p ≠ 0) (x : ℝ) :
    x ∈ spectrum ℝ (colleagueMatrix p hp) ↔ p.IsRoot x := by
  rw [Matrix.mem_spectrum_iff_isRoot_charpoly, charpoly_colleagueMatrix]
  simp [IsRoot, eval_mul, leadingCoeff_ne_zero.mpr hp]

theorem Polynomial.Chebyshev.colleagueMatrix_size (p : Polynomial ℝ) (hp : p ≠ 0) :
  (p * Polynomial.C p.leadingCoeff⁻¹).natDegree = p.natDegree

Lean proof

/-- The colleague dimension is exactly the degree of the input. -/
theorem colleagueMatrix_size (p : ℝ[X]) (hp : p ≠ 0) :
    (p * Polynomial.C p.leadingCoeff⁻¹).natDegree = p.natDegree := by
  simp [hp, natDegree_mul, leadingCoeff_ne_zero.mpr hp]

theorem Polynomial.Chebyshev.colleagueMatrix_entry (p : Polynomial ℝ) (hp : p ≠ 0)
  (i j : Fin (p * Polynomial.C p.leadingCoeff⁻¹).natDegree) :
  Polynomial.Chebyshev.colleagueMatrix p hp i j =
    (Polynomial.chebyshevBasis.repr (Polynomial.X * Polynomial.Chebyshev.T ℝ ↑↑j)) ↑i -
      (Polynomial.X * Polynomial.Chebyshev.T ℝ ↑↑j).coeff (p * Polynomial.C p.leadingCoeff⁻¹).natDegree *
        (Polynomial.chebyshevBasis.repr (p * Polynomial.C p.leadingCoeff⁻¹)) ↑i

Lean proof

/-- Explicit entries preserve the full-constant Chebyshev coordinates and
subtract a correction supported in the final column. -/
theorem colleagueMatrix_entry (p : ℝ[X]) (hp : p ≠ 0)
    (i j : Fin (p * Polynomial.C p.leadingCoeff⁻¹).natDegree) :
    colleagueMatrix p hp i j =
      chebyshevBasis.repr (X * T ℝ (j : ℕ)) i -
        (X * T ℝ (j : ℕ)).coeff (p * Polynomial.C p.leadingCoeff⁻¹).natDegree *
          chebyshevBasis.repr (p * Polynomial.C p.leadingCoeff⁻¹) i :=
  (chebyshevTsequence ℝ).comradeMatrix_rank_one_entry (monic_mul_leadingCoeff_inv hp) i j

theorem Polynomial.Chebyshev.mem_complex_spectrum_colleagueMatrix_iff (p : Polynomial ℝ) (hp : p ≠ 0) (z : ℂ) :
  z ∈ spectrum ℂ ((Polynomial.Chebyshev.colleagueMatrix p hp).map ⇑Complex.ofRealHom) ↔
    (Polynomial.map Complex.ofRealHom p).IsRoot z

Lean proof

/-- Complex eigenvalues of the real colleague matrix recover all complex roots. -/
theorem mem_complex_spectrum_colleagueMatrix_iff (p : ℝ[X]) (hp : p ≠ 0) (z : ℂ) :
    z ∈ spectrum ℂ ((colleagueMatrix p hp).map Complex.ofRealHom) ↔
      (p.map Complex.ofRealHom).IsRoot z := by
  rw [Matrix.mem_spectrum_iff_isRoot_charpoly, Matrix.charpoly_map,
    charpoly_colleagueMatrix, Polynomial.map_mul, Polynomial.map_C]
  simp [IsRoot, eval_mul, leadingCoeff_ne_zero.mpr hp]

Example (Julia).

For degree \(n\ge 2\), the final-column correction in the full-constant convention is \(c_i/(2c_n)\). The example forms that matrix and checks the polynomial residual at its computed eigenvalues. The recurrence starts with \(xT_0=T_1\).


using LinearAlgebra
function colleague(c)               # p = sum c[k+1] T_k of degree n >= 2
    n = length(c) - 1
    @assert n >= 2 && !iszero(c[end])
    C = zeros(n, n)
    C[2, 1] = 1                     # x T_0 = T_1
    for j in 1:n-1, i in (j, j+2)   # x T_j = (T_{j-1} + T_{j+1})/2
        i <= n && (C[i, j+1] = 1/2)
    end
    C[:, n] .-= c[1:n] ./ (2c[n+1]) # final-column correction
    C
end
function T(k, z)                    # T_k(z) by the recurrence
    a, b = one(z), z
    for _ in 1:k; a, b = b, 2z*b - a; end
    a
end
c = [0.2, -1.0, 0.5, 0.3, 0.0, 1.0] # T_5 + 0.3 T_3 + ... + 0.2
r = eigvals(colleague(c))
maximum(abs(sum(c[k+1]*T(k, z) for k in 0:5)) for z in r)  # polynomial residual at the computed eigenvalues
count(z -> abs(imag(z)) < 1e-12 && abs(real(z)) <= 1, r)   # number of computed real roots in the interval

Characteristic-polynomial and coordinate proofs

Theorem 2.9.5 Quotient power basis and characteristic polynomial Mathlib

✓

#

For a monic polynomial \(g\) over a field, \(K[x]/(g)\) has the power basis \(1,x,\ldots ,x^{\deg g-1}\). Multiplication by its generating root has characteristic polynomial \(g\). Characteristic polynomials are invariant under choice of basis, and their roots in the base field are exactly the matrix spectrum.

Lean Formalisation

theorem AdjoinRoot.minpoly_powerBasis_gen_of_monic.{u_5} {K : Type u_5} [Field K] {f : Polynomial K} (hf : f.Monic)
  (hf' : f ≠ 0 := ⋯) : minpoly K (AdjoinRoot.powerBasis hf').gen = f

Mathlib source

5 related Lean declarations

def AdjoinRoot.powerBasis.{u_5} {K : Type u_5} [Field K] {f : Polynomial K} (hf : f ≠ 0) : PowerBasis K (AdjoinRoot f)

Mathlib source

def AdjoinRoot.powerBasis'.{u_1} {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) : PowerBasis R (AdjoinRoot g)

Mathlib source

theorem charpoly_leftMulMatrix.{u, u_1} {R : Type u} [CommRing R] {S : Type u_1} [Ring S] [Algebra R S] (h : PowerBasis R S) :
  ((Algebra.leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

Mathlib source

theorem LinearMap.charpoly_toMatrix.{w, u_1, u_2} {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M]
  [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) {ι : Type w} [DecidableEq ι] [Fintype ι]
  (b : Module.Basis ι R M) : ((LinearMap.toMatrix b b) f).charpoly = f.charpoly

Mathlib source

theorem Matrix.mem_spectrum_iff_isRoot_charpoly.{u_1, u_3} {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_3} [Field K]
  {A : Matrix n n K} {r : K} : r ∈ spectrum K A ↔ A.charpoly.IsRoot r

Mathlib source

Theorem 2.9.6 Finite coordinates of a polynomial sequence

✓ 🤖

#

Let \(P_j\) have degree \(j\) over a field. A polynomial of degree below \(n\) has zero coordinates at every index \(j\ge n\) and reconstructs from its first \(n\) coordinates. Conversely, a combination of those \(n\) basis members has degree below \(n\). No orthogonality hypothesis is required.

Reference: elementary linear algebra used in the comrade construction [Bar75].

Lean Formalisation

theorem Polynomial.Sequence.basis_repr_eq_zero_of_degree_lt.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K)
  {p : Polynomial K} {n j : ℕ} (hp : p.degree < ↑n) (hj : n ≤ j) : ((P.basis ⋯).repr p) j = 0

Lean proof

/-- A degree-graded basis has no coordinates above the polynomial's degree. -/
theorem basis_repr_eq_zero_of_degree_lt {p : K[X]} {n j : ℕ}
    (hp : p.degree < n) (hj : n ≤ j) :
    (P.basis P.isUnit_leadingCoeff).repr p j = 0 := by
  have hs : p ∈ Submodule.span K (P '' Set.Iio n) := by
    rw [P.span_degreeLT (fun i _ ↦ P.isUnit_leadingCoeff i)]
    exact mem_degreeLT.mpr hp
  clear hp
  induction hs using Submodule.span_induction with
  | mem q hq =>
    obtain ⟨i, hi, rfl⟩ := hq
    rw [← P.basis_eq_self P.isUnit_leadingCoeff i, Basis.repr_self]
    simp [show i ≠ j by exact ne_of_lt (lt_of_lt_of_le hi hj)]
  | zero => simp
  | add q r _ _ hq hr => simp [hq, hr]
  | smul a q _ hq => simp [hq]

2 related Lean declarations

theorem Polynomial.Sequence.sum_fin_repr.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) {p : Polynomial K} {n : ℕ}
  (hp : p.degree < ↑n) : ∑ i, ((P.basis ⋯).repr p) ↑i • ↑P ↑i = p

Lean proof

/-- Finite reconstruction below a degree cutoff, without orthogonality hypotheses. -/
theorem sum_fin_repr {p : K[X]} {n : ℕ} (hp : p.degree < n) :
    ∑ i : Fin n, (P.basis P.isUnit_leadingCoeff).repr p i • P i = p := by
  classical
  change (∑ i : Fin n, (fun j : ℕ ↦ (P.basis P.isUnit_leadingCoeff).repr p j • P j) i) = p
  rw [Fin.sum_univ_eq_sum_range (fun j : ℕ ↦ (P.basis P.isUnit_leadingCoeff).repr p j • P j) n]
  have hs : ((P.basis P.isUnit_leadingCoeff).repr p).support ⊆ Finset.range n := by
    intro j hj
    apply Finset.mem_range.mpr
    by_contra hn
    exact Finsupp.mem_support_iff.mp hj
      (P.basis_repr_eq_zero_of_degree_lt hp (by omega))
  have he := (P.basis P.isUnit_leadingCoeff).linearCombination_repr p
  simp only [Finsupp.linearCombination_apply, Finsupp.sum, basis_eq_self] at he
  conv_rhs => rw [← he]
  exact (Finset.sum_subset hs (fun j _ hj ↦ by
    rw [Finsupp.notMem_support_iff.mp hj, zero_smul])).symm

theorem Polynomial.Sequence.degree_sum_fin_lt.{u_1} {K : Type u_1} [Field K] (P : Polynomial.Sequence K) (n : ℕ)
  (v : Fin n → K) : (∑ i, v i • ↑P ↑i).degree < ↑n

Lean proof

/-- A finite expansion in the first n polynomials has degree below n. -/
theorem degree_sum_fin_lt (n : ℕ) (v : Fin n → K) :
    (∑ i : Fin n, v i • P i).degree < n := by
  apply (degree_sum_le _ _).trans_lt
  apply (Finset.sup_lt_iff (WithBot.bot_lt_coe n)).mpr
  intro i _
  exact lt_of_le_of_lt (degree_smul_le _ _) (by rw [P.degree_eq]; exact WithBot.coe_lt_coe.mpr i.isLt)