Finite sums and products of polynomials

If each factor f i of a finite product has degree at most n i, then the product has degree at most ∑ i, n i, and its coefficient in that degree is the product of the coefficients of the factors in the degrees n i. Mathlib proves this for a uniform bound n (Polynomial.coeff_prod_of_natDegree_le) and for two factors (Polynomial.coeff_mul_add_eq_of_natDegree_le); here the bounds may vary with the factor. This is what is needed to read off the top coefficient of a determinant whose columns have different degree bounds.

This file also groups products of linear factors according to their constant terms, records that a sum ∑ j ∈ range N, C (c j) * X ^ (N - j) has no constant term, and computes the degree of geometric sums of mixed powers of equal-degree monic polynomials.

It also records that the image of a finite product of polynomials under a ring homomorphism into a ring without zero divisors has degree the sum of the factors' degrees when each factor's image is nonzero, and is itself nonzero when the target ring is moreover nontrivial.

Finally, TauCeti.sum_range_monomial_add_monomial_eq_of_eq_add turns coefficient relations cᵢ = bᵢ + qᵢ + qᵢ₋₁ into the polynomial identity ∑ᵢ₌₀ⁿ cᵢ Xⁱ + qₙ Xⁿ⁺¹ = ∑ᵢ₌₀ⁿ bᵢ Xⁱ + (1 + X) ∑ᵢ₌₀ⁿ qᵢ Xⁱ, the shape of the Morse polynomial identity.

theorem Polynomial.coeff_zero_sum_C_mul_X_pow_sub {R : Type u_1} [Semiring R] (c : ℕ → R) (N : ℕ) : (∑ j ∈ Finset.range N, C (c j) * X ^ (N - j)).coeff 0 = 0

The polynomial ∑ j ∈ range N, C (c j) * X ^ (N - j) has no constant term.

theorem Polynomial.map_prod_ne_zero {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] [NoZeroDivisors S] [Nontrivial S] (f : R →+* S) (s : Finset ι) (P : ι → Polynomial R) (h : ∀ k ∈ s, map f (P k) ≠ 0) : map f (∏ k ∈ s, P k) ≠ 0

Over a nontrivial ring without zero divisors, the image of a finite product of polynomials is nonzero when the image of each factor is nonzero.

theorem Polynomial.natDegree_map_prod {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] [NoZeroDivisors S] (f : R →+* S) (s : Finset ι) (P : ι → Polynomial R) (h : ∀ k ∈ s, map f (P k) ≠ 0) : (map f (∏ k ∈ s, P k)).natDegree = ∑ k ∈ s, (map f (P k)).natDegree

Over a ring without zero divisors, the degree of the image of a finite product of polynomials is the sum of the degrees of the images of the factors, when each image is nonzero.

theorem Polynomial.coeff_prod_sum_eq_of_natDegree_le {ι : Type u_1} {R : Type u_2} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (n : ι → ℕ) (h : ∀ i ∈ s, (f i).natDegree ≤ n i) : (∏ i ∈ s, f i).coeff (∑ i ∈ s, n i) = ∏ i ∈ s, (f i).coeff (n i)

If each factor f i has degree at most n i, the coefficient of the product in degree ∑ i ∈ s, n i is the product of the coefficients of the factors in the degrees n i.

@[instance_reducible]

noncomputable def Polynomial.instDecidableEqProductGrouping {R : Type u_2} : DecidableEq R

A local classical equality decision used to group the constant terms.

theorem Polynomial.pow_card_filter_eq_prod_X_add_C {ι : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype ι] (f : ι → R) (a : R) : (X + C a) ^ {i : ι | f i = a}.card = ∏ i : ι with f i = a, (X + C (f i))

The product of the linear factors whose constant term equals a is the corresponding power of X + C a.

theorem Polynomial.prod_X_add_C_eq_pow_card_filter_mul_prod_filter_ne {ι : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype ι] (f : ι → R) (a : R) : ∏ i : ι, (X + C (f i)) = (X + C a) ^ {i : ι | f i = a}.card * ∏ i : ι with f i ≠ a, (X + C (f i))

Group a product of linear factors according to whether their constant term equals a.

theorem Polynomial.natDegree_geom_sum₂ {S : Type u_3} [CommSemiring S] [CharZero S] {p q : Polynomial S} (hp : p.Monic) (hq : q.Monic) (hdeg : p.natDegree = q.natDegree) (n : ℕ) : (∑ i ∈ Finset.range n, p ^ i * q ^ (n - 1 - i)).natDegree = (n - 1) * p.natDegree

The geometric sum of mixed powers of two monic polynomials of equal degree has the expected degree in characteristic zero.

theorem TauCeti.sum_range_monomial_add_monomial_eq_of_eq_add {R : Type u_1} [Semiring R] {b c q : ℕ → R} {n : ℕ} (h₀ : c 0 = b 0 + q 0) (hsucc : ∀ i < n, c (i + 1) = b (i + 1) + q (i + 1) + q i) : ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (c i) + (Polynomial.monomial (n + 1)) (q n) = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (b i) + (1 + Polynomial.X) * ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial i) (q i)

The polynomial form of cᵢ = bᵢ + qᵢ + qᵢ₋₁. If c₀ = b₀ + q₀ and cᵢ₊₁ = bᵢ₊₁ + qᵢ₊₁ + qᵢ for i < n, then ∑ᵢ₌₀ⁿ cᵢ Xⁱ + qₙ Xⁿ⁺¹ = ∑ᵢ₌₀ⁿ bᵢ Xⁱ + (1 + X) ∑ᵢ₌₀ⁿ qᵢ Xⁱ.