Polynomial sequences

We define polynomial sequences – sequences of polynomials a₀, a₁, ... such that the polynomial aᵢ has degree i.

Main definitions

• Polynomial.Sequence R: the type of polynomial sequences with coefficients in R

Main statements

• Polynomial.Sequence.basis: a sequence is a basis for R[X]

TODO

Generalize linear independence to:

• IsCancelAdd semirings
• just require coefficients are regular
• arbitrary sets of polynomials which are pairwise different degree.

structure Polynomial.Sequence (R : Type u_1) [Semiring R] : Type u_1

A sequence of polynomials such that the polynomial at index i has degree i.

• elems' : ℕ → Polynomial R

  The i'th element in the sequence. Use S i instead, defined via CoeFun.

• degree_eq' (i : ℕ) : (↑self i).degree = ↑i

  The i'th element in the sequence has degree i. Use S.degree_eq instead.

instance Polynomial.Sequence.coeFun {R : Type u_1} [Semiring R] : CoeFun (Sequence R) fun (x : Sequence R) => ℕ → Polynomial R

Make S i mean S.elems' i.

Equations

• Polynomial.Sequence.coeFun = { coe := Polynomial.Sequence.elems' }

@[simp]

theorem Polynomial.Sequence.degree_eq {R : Type u_1} [Semiring R] (S : Sequence R) (i : ℕ) : (↑S i).degree = ↑i

S i has degree i.

@[simp]

theorem Polynomial.Sequence.natDegree_eq {R : Type u_1} [Semiring R] (S : Sequence R) (i : ℕ) : (↑S i).natDegree = i

S i has natDegree i.

@[simp]

theorem Polynomial.Sequence.ne_zero {R : Type u_1} [Semiring R] (S : Sequence R) (i : ℕ) : ↑S i ≠ 0

No polynomial in the sequence is zero.

theorem Polynomial.Sequence.degree_strictMono {R : Type u_1} [Semiring R] (S : Sequence R) : StrictMono (degree ∘ ↑S)

S i has strictly monotone degree.

theorem Polynomial.Sequence.natDegree_strictMono {R : Type u_1} [Semiring R] (S : Sequence R) : StrictMono (natDegree ∘ ↑S)

S i has strictly monotone natural degree.

theorem Polynomial.Sequence.span {R : Type u_1} [Ring R] (S : Sequence R) (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) : Submodule.span R (Set.range ↑S) = ⊤

A polynomial sequence spans R[X] if all of its elements' leading coefficients are units.

theorem Polynomial.Sequence.linearIndependent {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] : LinearIndependent R ↑S

Polynomials in a polynomial sequence are linearly independent.

noncomputable def Polynomial.Sequence.basis {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) : Basis ℕ R (Polynomial R)

Every polynomial sequence is a basis of R[X].

Equations

• S.basis hCoeff = Basis.mk ⋯ ⋯

@[simp]

theorem Polynomial.Sequence.basis_eq_self {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) (i : ℕ) : (S.basis hCoeff) i = ↑S i

The i'th basis vector is the i'th polynomial in the sequence.

theorem Polynomial.Sequence.basis_degree_strictMono {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) : StrictMono (degree ∘ ⇑(S.basis hCoeff))

Basis elements have strictly monotone degree.

theorem Polynomial.Sequence.basis_natDegree_strictMono {R : Type u_1} [Ring R] (S : Sequence R) [NoZeroDivisors R] (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) : StrictMono (natDegree ∘ ⇑(S.basis hCoeff))

Basis elements have strictly monotone natural degree.