Documentation

Mathlib.Algebra.Polynomial.Reverse

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.

source
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
Instances For
    source
    theorem Polynomial.revAtFun_invol {N i : ℕ} :
    revAtFun N (revAtFun N i) = i
    source
    theorem Polynomial.revAtFun_inj {N : ℕ} :
    Function.Injective (revAtFun N)
    source
    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
    Instances For
      source
      @[simp]
      theorem Polynomial.revAtFun_eq (N i : ℕ) :
      revAtFun N i = (revAt N) i

      We prefer to use the bundled revAt over unbundled revAtFun.

      source
      @[simp]
      theorem Polynomial.revAt_invol {N i : ℕ} :
      (revAt N) ((revAt N) i) = i
      source
      @[simp]
      theorem Polynomial.revAt_le {N i : ℕ} (H : i ≤ N) :
      (revAt N) i = N - i
      source
      theorem Polynomial.revAt_eq_self_of_lt {N i : ℕ} (h : N < i) :
      (revAt N) i = i
      source
      theorem Polynomial.revAt_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
      (revAt (N + O)) (n + o) = (revAt N) n + (revAt O) o
      source
      theorem Polynomial.revAt_zero (N : ℕ) :
      (revAt N) 0 = N
      source
      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
      Instances For
        source
        theorem Polynomial.reflect_support {R : Type u_1} [Semiring R] (N : ℕ) (f : Polynomial R) :
        (reflect N f).support = Finset.image (⇑(revAt N)) f.support
        source
        @[simp]
        theorem Polynomial.coeff_reflect {R : Type u_1} [Semiring R] (N : ℕ) (f : Polynomial R) (i : ℕ) :
        (reflect N f).coeff i = f.coeff ((revAt N) i)
        source
        @[simp]
        theorem Polynomial.reflect_reflect {R : Type u_1} [Semiring R] {N : ℕ} {p : Polynomial R} :
        reflect N (reflect N p) = p
        source
        @[simp]
        theorem Polynomial.reflect_zero {R : Type u_1} [Semiring R] {N : ℕ} :
        reflect N 0 = 0
        source
        @[simp]
        theorem Polynomial.reflect_eq_zero_iff {R : Type u_1} [Semiring R] {N : ℕ} {f : Polynomial R} :
        reflect N f = 0 ↔ f = 0
        source
        @[simp]
        theorem Polynomial.reflect_add {R : Type u_1} [Semiring R] (f g : Polynomial R) (N : ℕ) :
        reflect N (f + g) = reflect N f + reflect N g
        source
        @[simp]
        theorem Polynomial.reflect_C_mul {R : Type u_1} [Semiring R] (f : Polynomial R) (r : R) (N : ℕ) :
        reflect N (C r * f) = C r * reflect N f
        source
        theorem Polynomial.reflect_C_mul_X_pow {R : Type u_1} [Semiring R] (N n : ℕ) {c : R} :
        reflect N (C c * X ^ n) = C c * X ^ (revAt N) n
        source
        @[simp]
        theorem Polynomial.reflect_C {R : Type u_1} [Semiring R] (r : R) (N : ℕ) :
        reflect N (C r) = C r * X ^ N
        source
        @[simp]
        theorem Polynomial.reflect_monomial {R : Type u_1} [Semiring R] (N n : ℕ) :
        reflect N (X ^ n) = X ^ (revAt N) n
        source
        @[simp]
        theorem Polynomial.reflect_one_X {R : Type u_1} [Semiring R] :
        reflect 1 X = 1
        source
        theorem Polynomial.reflect_map {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ) :
        reflect n (map f p) = map f (reflect n p)
        source
        @[simp]
        theorem Polynomial.reflect_one {R : Type u_1} [Semiring R] (n : ℕ) :
        reflect n 1 = X ^ n
        source
        theorem Polynomial.reflect_mul_induction {R : Type u_1} [Semiring R] (cf cg N O : ℕ) (f g : Polynomial R) (Cf : f.support.card ≤ cf.succ) (Cg : g.support.card ≤ cg.succ) (Nf : f.natDegree ≤ N) (Og : g.natDegree ≤ O) :
        reflect (N + O) (f * g) = reflect N f * reflect O g
        source
        @[simp]
        theorem Polynomial.reflect_mul {R : Type u_1} [Semiring R] (f g : Polynomial R) {F G : ℕ} (Ff : f.natDegree ≤ F) (Gg : g.natDegree ≤ G) :
        reflect (F + G) (f * g) = reflect F f * reflect G g
        source
        theorem Polynomial.natDegree_reflect_le {R : Type u_1} [Semiring R] {N : ℕ} {p : Polynomial R} :
        (reflect N p).natDegree ≤ max N p.natDegree
        source
        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 : f.natDegree ≤ N) :
        eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f
        source
        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 : f.natDegree ≤ N) :
        eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0
        source
        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
        Instances For
          source
          theorem Polynomial.coeff_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) (n : ℕ) :
          f.reverse.coeff n = f.coeff ((revAt f.natDegree) n)
          source
          @[simp]
          theorem Polynomial.coeff_zero_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.coeff 0 = f.leadingCoeff
          source
          @[simp]
          theorem Polynomial.reverse_zero {R : Type u_1} [Semiring R] :
          reverse 0 = 0
          source
          @[simp]
          theorem Polynomial.reverse_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} :
          f.reverse = 0 ↔ f = 0
          source
          theorem Polynomial.reverse_natDegree_le {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.natDegree ≤ f.natDegree
          source
          theorem Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegree {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.natDegree = f.reverse.natDegree + f.natTrailingDegree
          source
          theorem Polynomial.reverse_natDegree {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.natDegree = f.natDegree - f.natTrailingDegree
          source
          theorem Polynomial.reverse_leadingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.leadingCoeff = f.trailingCoeff
          source
          theorem Polynomial.natTrailingDegree_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.natTrailingDegree = 0
          source
          theorem Polynomial.reverse_trailingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.trailingCoeff = f.leadingCoeff
          source
          theorem Polynomial.reverse_mul {R : Type u_1} [Semiring R] {f g : Polynomial R} (fg : f.leadingCoeff * g.leadingCoeff ≠ 0) :
          (f * g).reverse = f.reverse * g.reverse
          source
          @[simp]
          theorem Polynomial.reverse_mul_of_domain {R : Type u_2} [Semiring R] [NoZeroDivisors R] (f g : Polynomial R) :
          (f * g).reverse = f.reverse * g.reverse
          source
          theorem Polynomial.trailingCoeff_mul {R : Type u_2} [Semiring R] [NoZeroDivisors R] (p q : Polynomial R) :
          (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
          source
          @[simp]
          theorem Polynomial.coeff_one_reverse {R : Type u_1} [Semiring R] (f : Polynomial R) :
          f.reverse.coeff 1 = f.nextCoeff
          source
          @[simp]
          theorem Polynomial.reverse_C {R : Type u_1} [Semiring R] (t : R) :
          (C t).reverse = C t
          source
          @[simp]
          theorem Polynomial.reverse_mul_X {R : Type u_1} [Semiring R] (p : Polynomial R) :
          (p * X).reverse = p.reverse
          source
          @[simp]
          theorem Polynomial.reverse_X_mul {R : Type u_1} [Semiring R] (p : Polynomial R) :
          (X * p).reverse = p.reverse
          source
          @[simp]
          theorem Polynomial.reverse_mul_X_pow {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) :
          (p * X ^ n).reverse = p.reverse
          source
          @[simp]
          theorem Polynomial.reverse_X_pow_mul {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) :
          (X ^ n * p).reverse = p.reverse
          source
          @[simp]
          theorem Polynomial.reverse_add_C {R : Type u_1} [Semiring R] (p : Polynomial R) (t : R) :
          (p + C t).reverse = p.reverse + C t * X ^ p.natDegree
          source
          @[simp]
          theorem Polynomial.reverse_C_add {R : Type u_1} [Semiring R] (p : Polynomial R) (t : R) :
          (C t + p).reverse = C t * X ^ p.natDegree + p.reverse
          source
          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) :
          eval₂ i (⅟x) f.reverse * x ^ f.natDegree = eval₂ i x f
          source
          @[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) :
          eval₂ i (⅟x) f.reverse = 0 ↔ eval₂ i x f = 0
          source
          @[simp]
          theorem Polynomial.reflect_neg {R : Type u_1} [Ring R] (f : Polynomial R) (N : ℕ) :
          reflect N (-f) = -reflect N f
          source
          @[simp]
          theorem Polynomial.reflect_sub {R : Type u_1} [Ring R] (f g : Polynomial R) (N : ℕ) :
          reflect N (f - g) = reflect N f - reflect N g
          source
          @[simp]
          theorem Polynomial.reverse_neg {R : Type u_1} [Ring R] (f : Polynomial R) :
          (-f).reverse = -f.reverse