Reverse of a univariate polynomial

The main definition is reverse. Applying reverse to a polynomial f : R[X] produces the polynomial with a reversed list of coefficients, equivalent to X^f.natDegree * f(1/X).

The main result is that reverse (f * g) = reverse f * reverse g, provided the leading coefficients of f and g do not multiply to zero.

def Polynomial.revAtFun (N : ℕ) (i : ℕ) : ℕ

If i ≤ N, then revAtFun N i returns N - i, otherwise it returns i. This is the map used by the embedding revAt.

Equations

• Polynomial.revAtFun N i = if i ≤ N then N - i else i

theorem Polynomial.revAtFun_invol {N : ℕ} {i : ℕ} : Polynomial.revAtFun N (Polynomial.revAtFun N i) = i

theorem Polynomial.revAtFun_inj {N : ℕ} : Function.Injective (Polynomial.revAtFun N)

def Polynomial.revAt (N : ℕ) : ℕ ↪ ℕ

If i ≤ N, then revAt N i returns N - i, otherwise it returns i. Essentially, this embedding is only used for i ≤ N. The advantage of revAt N i over N - i is that revAt is an involution.

Equations

• Polynomial.revAt N = { toFun := fun i => if i ≤ N then N - i else i, inj' := (_ : Function.Injective (Polynomial.revAtFun N)) }

@[simp]

theorem Polynomial.revAtFun_eq (N : ℕ) (i : ℕ) : Polynomial.revAtFun N i = ↑(Polynomial.revAt N) i

We prefer to use the bundled revAt over unbundled revAtFun.

@[simp]

theorem Polynomial.revAt_invol {N : ℕ} {i : ℕ} : ↑(Polynomial.revAt N) (↑(Polynomial.revAt N) i) = i

@[simp]

theorem Polynomial.revAt_le {N : ℕ} {i : ℕ} (H : i ≤ N) : ↑(Polynomial.revAt N) i = N - i

theorem Polynomial.revAt_eq_self_of_lt {N : ℕ} {i : ℕ} (h : N < i) : ↑(Polynomial.revAt N) i = i

theorem Polynomial.revAt_add {N : ℕ} {O : ℕ} {n : ℕ} {o : ℕ} (hn : n ≤ N) (ho : o ≤ O) : ↑(Polynomial.revAt (N + O)) (n + o) = ↑(Polynomial.revAt N) n + ↑(Polynomial.revAt O) o

theorem Polynomial.revAt_zero (N : ℕ) : ↑(Polynomial.revAt N) 0 = N

noncomputable def Polynomial.reflect {R : Type u_1} [Semiring R] (N : ℕ) : Polynomial R → Polynomial R

reflect N f is the polynomial such that (reflect N f).coeff i = f.coeff (revAt N i). In other words, the terms with exponent [0, ..., N] now have exponent [N, ..., 0].

In practice, reflect is only used when N is at least as large as the degree of f.

Eventually, it will be used with N exactly equal to the degree of f.

Equations

• Polynomial.reflect N x = match x with | { toFinsupp := f } => { toFinsupp := Finsupp.embDomain (Polynomial.revAt N) f }

theorem Polynomial.reflect_support {R : Type u_1} [Semiring R] (N : ℕ) (f : Polynomial R) : Polynomial.support (Polynomial.reflect N f) = Finset.image (↑(Polynomial.revAt N)) (Polynomial.support f)

@[simp]

theorem Polynomial.coeff_reflect {R : Type u_1} [Semiring R] (N : ℕ) (f : Polynomial R) (i : ℕ) : Polynomial.coeff (Polynomial.reflect N f) i = Polynomial.coeff f (↑(Polynomial.revAt N) i)

@[simp]

theorem Polynomial.reflect_zero {R : Type u_1} [Semiring R] {N : ℕ} : Polynomial.reflect N 0 = 0

@[simp]

theorem Polynomial.reflect_eq_zero_iff {R : Type u_1} [Semiring R] {N : ℕ} {f : Polynomial R} : Polynomial.reflect N f = 0 ↔ f = 0

@[simp]

theorem Polynomial.reflect_add {R : Type u_1} [Semiring R] (f : Polynomial R) (g : Polynomial R) (N : ℕ) : Polynomial.reflect N (f + g) = Polynomial.reflect N f + Polynomial.reflect N g

@[simp]

theorem Polynomial.reflect_C_mul {R : Type u_1} [Semiring R] (f : Polynomial R) (r : R) (N : ℕ) : Polynomial.reflect N (↑Polynomial.C r * f) = ↑Polynomial.C r * Polynomial.reflect N f

theorem Polynomial.reflect_C_mul_X_pow {R : Type u_1} [Semiring R] (N : ℕ) (n : ℕ) {c : R} : Polynomial.reflect N (↑Polynomial.C c * Polynomial.X ^ n) = ↑Polynomial.C c * Polynomial.X ^ ↑(Polynomial.revAt N) n

@[simp]

theorem Polynomial.reflect_C {R : Type u_1} [Semiring R] (r : R) (N : ℕ) : Polynomial.reflect N (↑Polynomial.C r) = ↑Polynomial.C r * Polynomial.X ^ N

@[simp]

theorem Polynomial.reflect_monomial {R : Type u_1} [Semiring R] (N : ℕ) (n : ℕ) : Polynomial.reflect N (Polynomial.X ^ n) = Polynomial.X ^ ↑(Polynomial.revAt N) n

@[simp]

theorem Polynomial.reflect_one_X {R : Type u_1} [Semiring R] : Polynomial.reflect 1 Polynomial.X = 1

theorem Polynomial.reflect_mul_induction {R : Type u_1} [Semiring R] (cf : ℕ) (cg : ℕ) (N : ℕ) (O : ℕ) (f : Polynomial R) (g : Polynomial R) : Finset.card (Polynomial.support f) ≤ Nat.succ cf → Finset.card (Polynomial.support g) ≤ Nat.succ cg → Polynomial.natDegree f ≤ N → Polynomial.natDegree g ≤ O → Polynomial.reflect (N + O) (f * g) = Polynomial.reflect N f * Polynomial.reflect O g

@[simp]

theorem Polynomial.reflect_mul {R : Type u_1} [Semiring R] (f : Polynomial R) (g : Polynomial R) {F : ℕ} {G : ℕ} (Ff : Polynomial.natDegree f ≤ F) (Gg : Polynomial.natDegree g ≤ G) : Polynomial.reflect (F + G) (f * g) = Polynomial.reflect F f * Polynomial.reflect G g

theorem Polynomial.eval₂_reflect_mul_pow {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : Polynomial R) (hf : Polynomial.natDegree f ≤ N) : Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) * x ^ N = Polynomial.eval₂ i x f

theorem Polynomial.eval₂_reflect_eq_zero_iff {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : Polynomial R) (hf : Polynomial.natDegree f ≤ N) : Polynomial.eval₂ i (⅟x) (Polynomial.reflect N f) = 0 ↔ Polynomial.eval₂ i x f = 0

noncomputable def Polynomial.reverse {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial R

The reverse of a polynomial f is the polynomial obtained by "reading f backwards". Even though this is not the actual definition, reverse f = f (1/X) * X ^ f.natDegree.

Equations

• Polynomial.reverse f = Polynomial.reflect (Polynomial.natDegree f) f

theorem Polynomial.coeff_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) (n : ℕ) : Polynomial.coeff (Polynomial.reverse f) n = Polynomial.coeff f (↑(Polynomial.revAt (Polynomial.natDegree f)) n)

@[simp]

theorem Polynomial.coeff_zero_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.coeff (Polynomial.reverse f) 0 = Polynomial.leadingCoeff f

@[simp]

theorem Polynomial.reverse_zero {R : Type u_1} [Semiring R] : Polynomial.reverse 0 = 0

@[simp]

theorem Polynomial.reverse_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} : Polynomial.reverse f = 0 ↔ f = 0

theorem Polynomial.reverse_natDegree_le {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.natDegree (Polynomial.reverse f) ≤ Polynomial.natDegree f

theorem Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegree {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.natDegree f = Polynomial.natDegree (Polynomial.reverse f) + Polynomial.natTrailingDegree f

theorem Polynomial.reverse_natDegree {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.natDegree (Polynomial.reverse f) = Polynomial.natDegree f - Polynomial.natTrailingDegree f

theorem Polynomial.reverse_leadingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.leadingCoeff (Polynomial.reverse f) = Polynomial.trailingCoeff f

theorem Polynomial.reverse_natTrailingDegree {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.natTrailingDegree (Polynomial.reverse f) = 0

theorem Polynomial.reverse_trailingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.trailingCoeff (Polynomial.reverse f) = Polynomial.leadingCoeff f

theorem Polynomial.reverse_mul {R : Type u_1} [Semiring R] {f : Polynomial R} {g : Polynomial R} (fg : Polynomial.leadingCoeff f * Polynomial.leadingCoeff g ≠ 0) : Polynomial.reverse (f * g) = Polynomial.reverse f * Polynomial.reverse g

@[simp]

theorem Polynomial.reverse_mul_of_domain {R : Type u_2} [Ring R] [NoZeroDivisors R] (f : Polynomial R) (g : Polynomial R) : Polynomial.reverse (f * g) = Polynomial.reverse f * Polynomial.reverse g

theorem Polynomial.trailingCoeff_mul {R : Type u_2} [Ring R] [NoZeroDivisors R] (p : Polynomial R) (q : Polynomial R) : Polynomial.trailingCoeff (p * q) = Polynomial.trailingCoeff p * Polynomial.trailingCoeff q

@[simp]

theorem Polynomial.coeff_one_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.coeff (Polynomial.reverse f) 1 = Polynomial.nextCoeff f

@[simp]

theorem Polynomial.reverse_C {R : Type u_1} [Semiring R] (t : R) : Polynomial.reverse (↑Polynomial.C t) = ↑Polynomial.C t

@[simp]

theorem Polynomial.reverse_mul_X {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.reverse (p * Polynomial.X) = Polynomial.reverse p

@[simp]

theorem Polynomial.reverse_X_mul {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.reverse (Polynomial.X * p) = Polynomial.reverse p

@[simp]

theorem Polynomial.reverse_mul_X_pow {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) : Polynomial.reverse (p * Polynomial.X ^ n) = Polynomial.reverse p

@[simp]

theorem Polynomial.reverse_X_pow_mul {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) : Polynomial.reverse (Polynomial.X ^ n * p) = Polynomial.reverse p

@[simp]

theorem Polynomial.reverse_add_C {R : Type u_1} [Semiring R] (p : Polynomial R) (t : R) : Polynomial.reverse (p + ↑Polynomial.C t) = Polynomial.reverse p + ↑Polynomial.C t * Polynomial.X ^ Polynomial.natDegree p

@[simp]

theorem Polynomial.reverse_C_add {R : Type u_1} [Semiring R] (p : Polynomial R) (t : R) : Polynomial.reverse (↑Polynomial.C t + p) = ↑Polynomial.C t * Polynomial.X ^ Polynomial.natDegree p + Polynomial.reverse p

theorem Polynomial.eval₂_reverse_mul_pow {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (f : Polynomial R) : Polynomial.eval₂ i (⅟x) (Polynomial.reverse f) * x ^ Polynomial.natDegree f = Polynomial.eval₂ i x f

@[simp]

theorem Polynomial.eval₂_reverse_eq_zero_iff {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (f : Polynomial R) : Polynomial.eval₂ i (⅟x) (Polynomial.reverse f) = 0 ↔ Polynomial.eval₂ i x f = 0

@[simp]

theorem Polynomial.reflect_neg {R : Type u_1} [Ring R] (f : Polynomial R) (N : ℕ) : Polynomial.reflect N (-f) = -Polynomial.reflect N f

@[simp]

theorem Polynomial.reflect_sub {R : Type u_1} [Ring R] (f : Polynomial R) (g : Polynomial R) (N : ℕ) : Polynomial.reflect N (f - g) = Polynomial.reflect N f - Polynomial.reflect N g

@[simp]

theorem Polynomial.reverse_neg {R : Type u_1} [Ring R] (f : Polynomial R) : Polynomial.reverse (-f) = -Polynomial.reverse f