Mathlib.Algebra.Polynomial.Reverse

Polynomial.revAtFun definition

(N i : ℕ) : ℕ

Full source

/-- If `i ≤ N`, then `revAtFun N i` returns `N - i`, otherwise it returns `i`.
This is the map used by the embedding `revAt`.
-/
def revAtFun (N i : ℕ) : ℕ :=
  ite (i ≤ N) (N - i) i

Reversal function for polynomial coefficients

Informal description

For natural numbers $ N $ and $ i $, the function $\text{revAtFun}(N, i)$ is defined as $ N - i $ if $ i \leq N $, and $ i $ otherwise. This function is used to reverse the order of coefficients in a polynomial up to degree $ N $.

Polynomial.revAtFun_invol theorem

{N i : ℕ} : revAtFun N (revAtFun N i) = i

Full source

theorem revAtFun_invol {N i : ℕ} : revAtFun N (revAtFun N i) = i := by
  unfold revAtFun
  split_ifs with h j
  · exact tsub_tsub_cancel_of_le h
  · exfalso
    apply j
    exact Nat.sub_le N i
  · rfl

Involutive Property of Polynomial Coefficient Reversal: $\text{revAtFun}_N \circ \text{revAtFun}_N = \text{id}$

Informal description

For any natural numbers $N$ and $i$, applying the coefficient reversal function $\text{revAtFun}$ twice at degree $N$ returns the original index $i$, i.e., $\text{revAtFun}\, N\, (\text{revAtFun}\, N\, i) = i$.

Polynomial.revAtFun_inj theorem

{N : ℕ} : Function.Injective (revAtFun N)

Full source

theorem revAtFun_inj {N : ℕ} : Function.Injective (revAtFun N) := by
  intro a b hab
  rw [← @revAtFun_invol N a, hab, revAtFun_invol]

Injectivity of Polynomial Coefficient Reversal Function

Informal description

For any natural number $N$, the coefficient reversal function $\text{revAtFun}_N$ is injective. That is, for any $i, j \in \mathbb{N}$, if $\text{revAtFun}_N(i) = \text{revAtFun}_N(j)$, then $i = j$.

Polynomial.revAt definition

(N : ℕ) : Function.Embedding ℕ ℕ

Full source

/-- 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.
-/
def revAt (N : ℕ) : Function.Embedding ℕ ℕ where
  toFun i := ite (i ≤ N) (N - i) i
  inj' := revAtFun_inj

Polynomial coefficient reversal function at degree $N$

Informal description

For a given natural number $N$, the function $\text{revAt}\, N$ is an injective function from $\mathbb{N}$ to $\mathbb{N}$ defined by: \[ \text{revAt}\, N\, i = \begin{cases} N - i & \text{if } i \leq N, \\ i & \text{otherwise.} \end{cases} \] This function acts as an involution when restricted to $i \leq N$, meaning $\text{revAt}\, N\, (\text{revAt}\, N\, i) = i$ for $i \leq N$.

Polynomial.revAtFun_eq theorem

(N i : ℕ) : revAtFun N i = revAt N i

Full source

/-- We prefer to use the bundled `revAt` over unbundled `revAtFun`. -/
@[simp]
theorem revAtFun_eq (N i : ℕ) : revAtFun N i = revAt N i :=
  rfl

Equality of Polynomial Coefficient Reversal Functions

Informal description

For any natural numbers $N$ and $i$, the reversal function $\text{revAtFun}(N, i)$ equals the bundled reversal embedding $\text{revAt}\, N\, i$.

Polynomial.revAt_invol theorem

{N i : ℕ} : (revAt N) (revAt N i) = i

Full source

@[simp]
theorem revAt_invol {N i : ℕ} : (revAt N) (revAt N i) = i :=
  revAtFun_invol

Involutive Property of Polynomial Coefficient Reversal: $\text{revAt}_N \circ \text{revAt}_N = \text{id}$

Informal description

For any natural numbers $N$ and $i$, the polynomial coefficient reversal function $\text{revAt}$ satisfies the involutive property: \[ \text{revAt}\, N\, (\text{revAt}\, N\, i) = i. \]

Polynomial.revAt_le theorem

{N i : ℕ} (H : i ≤ N) : revAt N i = N - i

Full source

@[simp]
theorem revAt_le {N i : ℕ} (H : i ≤ N) : revAt N i = N - i :=
  if_pos H

Coefficient Reversal Formula for $i \leq N$

Informal description

For any natural numbers $N$ and $i$ with $i \leq N$, the coefficient reversal function satisfies $\text{revAt}\, N\, i = N - i$.

Polynomial.revAt_eq_self_of_lt theorem

{N i : ℕ} (h : N < i) : revAt N i = i

Full source

lemma revAt_eq_self_of_lt {N i : ℕ} (h : N < i) : revAt N i = i := by simp [revAt, Nat.not_le.mpr h]

Invariance of Coefficient Reversal Function for Large Indices

Informal description

For any natural numbers $N$ and $i$, if $N < i$, then the reversal function $\text{revAt}\, N\, i$ equals $i$.

Polynomial.revAt_add theorem

{N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) : revAt (N + O) (n + o) = revAt N n + revAt O o

Full source

theorem revAt_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
    revAt (N + O) (n + o) = revAt N n + revAt O o := by
  rcases Nat.le.dest hn with ⟨n', rfl⟩
  rcases Nat.le.dest ho with ⟨o', rfl⟩
  repeat' rw [revAt_le (le_add_right rfl.le)]
  rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]
  repeat' rw [add_tsub_cancel_left]

Additivity of Coefficient Reversal Function under Addition

Informal description

For any natural numbers $N, O, n, o$ such that $n \leq N$ and $o \leq O$, the coefficient reversal function satisfies: \[ \text{revAt}\, (N + O)\, (n + o) = \text{revAt}\, N\, n + \text{revAt}\, O\, o. \]

Polynomial.revAt_zero theorem

(N : ℕ) : revAt N 0 = N

Full source

theorem revAt_zero (N : ℕ) : revAt N 0 = N := by simp

Coefficient Reversal at Zero: $\text{revAt}\, N\, 0 = N$

Informal description

For any natural number $N$, the coefficient reversal function evaluated at $0$ equals $N$, i.e., $\text{revAt}\, N\, 0 = N$.

Polynomial.reflect definition

(N : ℕ) : R[X] → R[X]

Full source

/-- `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`. -/
noncomputable def reflect (N : ℕ) : R[X] → R[X]
  | ⟨f⟩ => ⟨Finsupp.embDomain (revAt N) f⟩

Polynomial coefficient reflection at degree $N$

Informal description

For a natural number $N$ and a polynomial $f \in R[X]$, the polynomial $\text{reflect}\, N\, f$ is defined such that its coefficient at degree $i$ equals the coefficient of $f$ at degree $\text{revAt}\, N\, i$, where $\text{revAt}\, N\, i = N - i$ when $i \leq N$ and $i$ otherwise. This operation effectively reverses the coefficients of $f$ for degrees up to $N$.

Polynomial.reflect_support theorem

(N : ℕ) (f : R[X]) : (reflect N f).support = Finset.image (revAt N) f.support

Full source

theorem reflect_support (N : ℕ) (f : R[X]) :
    (reflect N f).support = Finset.image (revAt N) f.support := by
  rcases f with ⟨⟩
  ext1
  simp only [reflect, support_ofFinsupp, support_embDomain, Finset.mem_map, Finset.mem_image]

Support of Reflected Polynomial Equals Image of Original Support under Coefficient Reversal

Informal description

For any natural number $N$ and polynomial $f \in R[X]$, the support of the reflected polynomial $\text{reflect}\, N\, f$ is equal to the image of the support of $f$ under the coefficient reversal function $\text{revAt}\, N$. That is: \[ \text{support}(\text{reflect}\, N\, f) = \{\text{revAt}\, N\, i \mid i \in \text{support}(f)\} \]

Polynomial.coeff_reflect theorem

(N : ℕ) (f : R[X]) (i : ℕ) : coeff (reflect N f) i = f.coeff (revAt N i)

Full source

@[simp]
theorem coeff_reflect (N : ℕ) (f : R[X]) (i : ℕ) : coeff (reflect N f) i = f.coeff (revAt N i) := by
  rcases f with ⟨f⟩
  simp only [reflect, coeff]
  calc
    Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by
      rw [revAt_invol]
    _ = f (revAt N i) := Finsupp.embDomain_apply _ _ _

Coefficient Reflection Formula for Polynomials: $(\text{reflect}\, N\, f)_i = f_{\text{revAt}\, N\, i}$

Informal description

For any natural number $N$, polynomial $f \in R[X]$, and degree $i \in \mathbb{N}$, the coefficient of the reflected polynomial $\text{reflect}\, N\, f$ at degree $i$ is equal to the coefficient of $f$ at degree $\text{revAt}\, N\, i$, where $\text{revAt}\, N\, i = N - i$ if $i \leq N$ and $i$ otherwise. In other words, the coefficient at degree $i$ in $\text{reflect}\, N\, f$ is given by: \[ (\text{reflect}\, N\, f)_i = f_{N - i} \quad \text{if } i \leq N, \quad \text{and } f_i \text{ otherwise.} \]

Polynomial.reflect_zero theorem

{N : ℕ} : reflect N (0 : R[X]) = 0

Full source

@[simp]
theorem reflect_zero {N : ℕ} : reflect N (0 : R[X]) = 0 :=
  rfl

Reflection of Zero Polynomial is Zero

Informal description

For any natural number $N$, the reflection of the zero polynomial at degree $N$ is the zero polynomial, i.e., $\text{reflect}\, N\, 0 = 0$.

Polynomial.reflect_eq_zero_iff theorem

{N : ℕ} {f : R[X]} : reflect N (f : R[X]) = 0 ↔ f = 0

Full source

@[simp]
theorem reflect_eq_zero_iff {N : ℕ} {f : R[X]} : reflectreflect N (f : R[X]) = 0 ↔ f = 0 := by
  rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]

Reflected Polynomial is Zero if and Only if Original Polynomial is Zero

Informal description

For any natural number $N$ and polynomial $f \in R[X]$, the reflected polynomial $\text{reflect}\, N\, f$ is equal to the zero polynomial if and only if $f$ itself is the zero polynomial.

Polynomial.reflect_add theorem

(f g : R[X]) (N : ℕ) : reflect N (f + g) = reflect N f + reflect N g

Full source

@[simp]
theorem reflect_add (f g : R[X]) (N : ℕ) : reflect N (f + g) = reflect N f + reflect N g := by
  ext
  simp only [coeff_add, coeff_reflect]

Additivity of Polynomial Reflection: $\text{reflect}_N(f + g) = \text{reflect}_N f + \text{reflect}_N g$

Informal description

For any polynomials $f, g \in R[X]$ and natural number $N$, the reflection of their sum equals the sum of their reflections: \[ \text{reflect}_N(f + g) = \text{reflect}_N f + \text{reflect}_N g. \]

Polynomial.reflect_C_mul theorem

(f : R[X]) (r : R) (N : ℕ) : reflect N (C r * f) = C r * reflect N f

Full source

@[simp]
theorem reflect_C_mul (f : R[X]) (r : R) (N : ℕ) : reflect N (C r * f) = C r * reflect N f := by
  ext
  simp only [coeff_reflect, coeff_C_mul]

Reflection of Scalar Multiple of Polynomial: $\text{reflect}_N(r \cdot f) = r \cdot \text{reflect}_N(f)$

Informal description

For any polynomial $f \in R[X]$, any element $r \in R$, and any natural number $N$, the reflection of the polynomial $r \cdot f$ at degree $N$ satisfies: \[ \text{reflect}_N(r \cdot f) = r \cdot \text{reflect}_N(f). \]

Polynomial.reflect_C_mul_X_pow theorem

(N n : ℕ) {c : R} : reflect N (C c * X ^ n) = C c * X ^ revAt N n

Full source

theorem reflect_C_mul_X_pow (N n : ℕ) {c : R} : reflect N (C c * X ^ n) = C c * X ^ revAt N n := by
  ext
  rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect]
  split_ifs with h
  · rw [h, revAt_invol, coeff_X_pow_self]
  · rw [not_mem_support_iff.mp]
    intro a
    rw [← one_mul (X ^ n), ← C_1] at a
    apply h
    rw [← mem_support_C_mul_X_pow a, revAt_invol]

Reflection of Scaled Monomial: $\text{reflect}_N(c X^n) = c X^{\text{revAt}_N(n)}$

Informal description

For any natural numbers $N$ and $n$, and any coefficient $c \in R$, the reflection of the monomial $c X^n$ at degree $N$ is given by: \[ \text{reflect}_N(c X^n) = c X^{\text{revAt}_N(n)}, \] where $\text{revAt}_N(n) = N - n$ if $n \leq N$ and $n$ otherwise.

Polynomial.reflect_C theorem

(r : R) (N : ℕ) : reflect N (C r) = C r * X ^ N

Full source

@[simp]
theorem reflect_C (r : R) (N : ℕ) : reflect N (C r) = C r * X ^ N := by
  conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]

Reflection of Constant Polynomial: $\text{reflect}_N(r) = r X^N$

Informal description

For any element $r$ in a semiring $R$ and any natural number $N$, the reflection at degree $N$ of the constant polynomial $r$ is equal to $r X^N$, i.e., \[ \text{reflect}_N(r) = r X^N. \]

Polynomial.reflect_monomial theorem

(N n : ℕ) : reflect N ((X : R[X]) ^ n) = X ^ revAt N n

Full source

@[simp]
theorem reflect_monomial (N n : ℕ) : reflect N ((X : R[X]) ^ n) = X ^ revAt N n := by
  rw [← one_mul (X ^ n), ← one_mul (X ^ revAt N n), ← C_1, reflect_C_mul_X_pow]

Reflection of Monomial: $\text{reflect}_N(X^n) = X^{\text{revAt}_N(n)}$

Informal description

For any natural numbers $N$ and $n$, the reflection of the monomial $X^n$ at degree $N$ in the polynomial ring $R[X]$ is given by: \[ \text{reflect}_N(X^n) = X^{\text{revAt}_N(n)}, \] where $\text{revAt}_N(n) = N - n$ if $n \leq N$ and $n$ otherwise.

Polynomial.reflect_one_X theorem

: reflect 1 (X : R[X]) = 1

Full source

@[simp] lemma reflect_one_X : reflect 1 (X : R[X]) = 1 := by
  simpa using reflect_monomial 1 1 (R := R)

Reflection of $X$ at Degree 1 Yields 1

Informal description

For the polynomial $X$ in the polynomial ring $R[X]$, reflecting it at degree $1$ yields the constant polynomial $1$, i.e., \[ \text{reflect}_1(X) = 1. \]

Polynomial.reflect_map theorem

{S : Type*} [Semiring S] (f : R →+* S) (p : R[X]) (n : ℕ) : (p.map f).reflect n = (p.reflect n).map f

Full source

lemma reflect_map {S : Type*} [Semiring S] (f : R →+* S) (p : R[X]) (n : ℕ) :
    (p.map f).reflect n = (p.reflect n).map f := by
  ext; simp

Commutativity of Polynomial Reflection and Ring Homomorphism Application

Informal description

Let $R$ and $S$ be semirings, and let $f : R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$ and natural number $n$, the reflection of $p$ at degree $n$ followed by applying $f$ is equal to applying $f$ to $p$ followed by reflection at degree $n$. That is, \[ \text{reflect}_n (p \cdot f) = (\text{reflect}_n p) \cdot f. \]

Polynomial.reflect_one theorem

(n : ℕ) : (1 : R[X]).reflect n = Polynomial.X ^ n

Full source

@[simp]
lemma reflect_one (n : ℕ) : (1 : R[X]).reflect n = Polynomial.X ^ n := by
  rw [← C.map_one, reflect_C, map_one, one_mul]

Reflection of the Constant One Polynomial: $\text{reflect}_n(1) = X^n$

Informal description

For any natural number $n$ and any semiring $R$, the reflection at degree $n$ of the constant polynomial $1 \in R[X]$ is equal to $X^n$, i.e., \[ \text{reflect}_n(1) = X^n. \]

Polynomial.reflect_mul_induction theorem

 (cf cg : ℕ) :
  ∀ N O : ℕ,
    ∀ f g : R[X],
      #f.support ≤ cf.succ →
        #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g

Full source

theorem reflect_mul_induction (cf cg : ℕ) :
    ∀ N O : ℕ,
      ∀ f g : R[X],
        #f.support ≤ cf.succ →
          #g.support ≤ cg.succ →
            f.natDegree ≤ N →
              g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g := by
  induction' cf with cf hcf
  --first induction (left): base case
  · induction' cg with cg hcg
    -- second induction (right): base case
    · intro N O f g Cf Cg Nf Og
      rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
      simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]
    -- second induction (right): induction step
    · intro N O f g Cf Cg Nf Og
      by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cg (eraseLead_support_card_lt g0))
      · exact le_trans eraseLead_natDegree_le_aux Og
  --first induction (left): induction step
  · intro N O f g Cf Cg Nf Og
    by_cases f0 : f = 0
    · rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
    rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
      try assumption
    · exact le_add_left card_support_C_mul_X_pow_le_one
    · exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
    · exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cf (eraseLead_support_card_lt f0))
    · exact le_trans eraseLead_natDegree_le_aux Nf

Reflection of Polynomial Product under Induction on Support Size: $\text{reflect}_{N+O}(f \cdot g) = \text{reflect}_N f \cdot \text{reflect}_O g$

Informal description

Let $R$ be a semiring and let $f, g \in R[X]$ be polynomials with finite support sizes bounded by $c_f + 1$ and $c_g + 1$ respectively, where $c_f, c_g \in \mathbb{N}$. For any natural numbers $N, O$ such that $\deg(f) \leq N$ and $\deg(g) \leq O$, the reflection of the product $f \cdot g$ at degree $N + O$ equals the product of the reflections of $f$ at degree $N$ and $g$ at degree $O$: \[ \text{reflect}_{N+O}(f \cdot g) = \text{reflect}_N f \cdot \text{reflect}_O g. \]

Polynomial.reflect_mul theorem

 (f g : R[X]) {F G : ℕ} (Ff : f.natDegree ≤ F) (Gg : g.natDegree ≤ G) :
  reflect (F + G) (f * g) = reflect F f * reflect G g

Full source

@[simp]
theorem reflect_mul (f g : R[X]) {F G : ℕ} (Ff : f.natDegree ≤ F) (Gg : g.natDegree ≤ G) :
    reflect (F + G) (f * g) = reflect F f * reflect G g :=
  reflect_mul_induction _ _ F G f g f.support.card.le_succ g.support.card.le_succ Ff Gg

Reflection of polynomial product: $\text{reflect}_{F+G}(f \cdot g) = \text{reflect}_F f \cdot \text{reflect}_G g$

Informal description

Let $R$ be a semiring and let $f, g \in R[X]$ be polynomials with $\deg(f) \leq F$ and $\deg(g) \leq G$ for some natural numbers $F, G$. Then the reflection of the product $f \cdot g$ at degree $F + G$ equals the product of the reflections of $f$ at degree $F$ and $g$ at degree $G$: \[ \text{reflect}_{F+G}(f \cdot g) = \text{reflect}_F f \cdot \text{reflect}_G g. \]

Polynomial.eval₂_reflect_mul_pow theorem

 (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X]) (hf : f.natDegree ≤ N) :
  eval₂ i (⅟ x) (reflect N f) * x ^ N = eval₂ i x f

Full source

theorem eval₂_reflect_mul_pow (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X])
    (hf : f.natDegree ≤ N) : eval₂ i (⅟ x) (reflect N f) * x ^ N = eval₂ i x f := by
  refine
    induction_with_natDegree_le (fun f => eval₂ i (⅟ x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf
  · simp
  · intro n r _ hnN
    simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]
    conv in x ^ N => rw [← Nat.sub_add_cancel hnN]
    rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
  · intros
    simp [*, add_mul]

Evaluation of Reflected Polynomial: $\text{eval}_2\, i\, (x^{-1})\, (\text{reflect}_N\, f) \cdot x^N = \text{eval}_2\, i\, x\, f$

Informal description

Let $R$ and $S$ be commutative semirings, $i : R \to S$ a ring homomorphism, and $x \in S$ an invertible element. For any polynomial $f \in R[X]$ with $\deg(f) \leq N$, the following equality holds: \[ \text{eval}_2\, i\, (x^{-1})\, (\text{reflect}_N\, f) \cdot x^N = \text{eval}_2\, i\, x\, f, \] where $\text{eval}_2$ denotes the evaluation of a polynomial via the homomorphism $i$, and $\text{reflect}_N\, f$ is the polynomial obtained by reflecting the coefficients of $f$ at degree $N$.

Polynomial.eval₂_reflect_eq_zero_iff theorem

 (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X]) (hf : f.natDegree ≤ N) :
  eval₂ i (⅟ x) (reflect N f) = 0 ↔ eval₂ i x f = 0

Full source

theorem eval₂_reflect_eq_zero_iff (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X])
    (hf : f.natDegree ≤ N) : eval₂eval₂ i (⅟ x) (reflect N f) = 0 ↔ eval₂ i x f = 0 := by
  conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]
  constructor
  · intro h
    rw [h, zero_mul]
  · intro h
    rw [← mul_one (eval₂ i (⅟ x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

Equivalence of Zero Evaluations for Reflected Polynomials: $\text{eval}_2\, i\, (x^{-1})\, (\text{reflect}_N\, f) = 0 \leftrightarrow \text{eval}_2\, i\, x\, f = 0$

Informal description

Let $R$ and $S$ be commutative semirings, $i : R \to S$ a ring homomorphism, and $x \in S$ an invertible element. For any polynomial $f \in R[X]$ with $\deg(f) \leq N$, the following equivalence holds: \[ \text{eval}_2\, i\, (x^{-1})\, (\text{reflect}_N\, f) = 0 \quad \text{if and only if} \quad \text{eval}_2\, i\, x\, f = 0, \] where $\text{eval}_2$ denotes the evaluation of a polynomial via the homomorphism $i$, and $\text{reflect}_N\, f$ is the polynomial obtained by reflecting the coefficients of $f$ at degree $N$.

Polynomial.reverse definition

(f : R[X]) : R[X]

Full source

/-- 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`. -/
noncomputable def reverse (f : R[X]) : R[X] :=
  reflect f.natDegree f

Reverse of a polynomial

Informal description

The reverse of a polynomial $f \in R[X]$ is the polynomial obtained by reflecting the coefficients of $f$ at its degree, i.e., $\text{reverse}\, f = X^{\text{natDegree}\, f} \cdot f(1/X)$.

Polynomial.coeff_reverse theorem

(f : R[X]) (n : ℕ) : f.reverse.coeff n = f.coeff (revAt f.natDegree n)

Full source

theorem coeff_reverse (f : R[X]) (n : ℕ) : f.reverse.coeff n = f.coeff (revAt f.natDegree n) := by
  rw [reverse, coeff_reflect]

Coefficient Formula for Reverse Polynomial: $(\text{reverse}\, f)_n = f_{\text{revAt}\, N\, n}$ where $N = \deg f$

Informal description

For any polynomial $f \in R[X]$ and natural number $n$, the coefficient of degree $n$ in the reverse polynomial $\text{reverse}\, f$ is equal to the coefficient of $f$ at degree $\text{revAt}\, (\text{natDegree}\, f)\, n$, where $\text{revAt}\, N\, i$ is defined as $N - i$ if $i \leq N$ and $i$ otherwise. In other words: \[ (\text{reverse}\, f)_n = f_{N - n} \quad \text{if } n \leq N, \quad \text{and } f_n \text{ otherwise,} \] where $N = \text{natDegree}\, f$.

Polynomial.coeff_zero_reverse theorem

(f : R[X]) : coeff (reverse f) 0 = leadingCoeff f

Full source

@[simp]
theorem coeff_zero_reverse (f : R[X]) : coeff (reverse f) 0 = leadingCoeff f := by
  rw [coeff_reverse, revAt_le (zero_le f.natDegree), tsub_zero, leadingCoeff]

Constant Term of Reverse Polynomial Equals Leading Coefficient of Original Polynomial

Informal description

For any polynomial $f \in R[X]$, the constant term of its reverse polynomial $\text{reverse}\, f$ is equal to the leading coefficient of $f$, i.e., \[ (\text{reverse}\, f)(0) = \text{leadingCoeff}\, f. \]

Polynomial.reverse_zero theorem

: reverse (0 : R[X]) = 0

Full source

@[simp]
theorem reverse_zero : reverse (0 : R[X]) = 0 :=
  rfl

Reverse of Zero Polynomial is Zero

Informal description

The reverse of the zero polynomial is the zero polynomial, i.e., $\text{reverse}(0) = 0$.

Polynomial.reverse_eq_zero theorem

: f.reverse = 0 ↔ f = 0

Full source

@[simp]
theorem reverse_eq_zero : f.reverse = 0 ↔ f = 0 := by simp [reverse]

Reverse of a Polynomial is Zero if and only if the Polynomial is Zero

Informal description

For any polynomial $f$ over a semiring $R$, the reverse of $f$ is the zero polynomial if and only if $f$ itself is the zero polynomial. In other words, $\text{reverse}(f) = 0 \leftrightarrow f = 0$.

Polynomial.reverse_natDegree_le theorem

(f : R[X]) : f.reverse.natDegree ≤ f.natDegree

Full source

theorem reverse_natDegree_le (f : R[X]) : f.reverse.natDegree ≤ f.natDegree := by
  rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]
  intro n hn
  rw [Nat.cast_lt] at hn
  rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn),
    coeff_eq_zero_of_natDegree_lt hn]

Degree Bound for Reverse Polynomial: $\deg(\text{reverse}(f)) \leq \deg(f)$

Informal description

For any polynomial $f$ over a semiring $R$, the degree of the reverse polynomial $\text{reverse}(f)$ is less than or equal to the degree of $f$. That is, $\deg(\text{reverse}(f)) \leq \deg(f)$.

Polynomial.natDegree_eq_reverse_natDegree_add_natTrailingDegree theorem

(f : R[X]) : f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Full source

theorem natDegree_eq_reverse_natDegree_add_natTrailingDegree (f : R[X]) :
    f.natDegree = f.reverse.natDegree + f.natTrailingDegree := by
  by_cases hf : f = 0
  · rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
  apply le_antisymm
  · refine tsub_le_iff_right.mp ?_
    apply le_natDegree_of_ne_zero
    rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
    exact trailingCoeff_nonzero_iff_nonzero.mpr hf
  · rw [← le_tsub_iff_left f.reverse_natDegree_le]
    apply natTrailingDegree_le_of_ne_zero
    have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
    rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key

Degree Decomposition for Polynomial and Its Reverse: $\deg(f) = \deg(\text{reverse}(f)) + \deg_{\text{trailing}}(f)$

Informal description

For any polynomial $f$ over a semiring $R$, the degree of $f$ is equal to the sum of the degrees of its reverse polynomial and its trailing term. That is, \[ \deg(f) = \deg(\text{reverse}(f)) + \deg_{\text{trailing}}(f), \] where $\deg_{\text{trailing}}(f)$ denotes the degree of the trailing (lowest-degree) term of $f$.

Polynomial.reverse_natDegree theorem

(f : R[X]) : f.reverse.natDegree = f.natDegree - f.natTrailingDegree

Full source

theorem reverse_natDegree (f : R[X]) : f.reverse.natDegree = f.natDegree - f.natTrailingDegree := by
  rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]

Degree of Reverse Polynomial: $\deg(\text{reverse}(f)) = \deg(f) - \deg_{\text{trailing}}(f)$

Informal description

For any polynomial $f$ over a semiring $R$, the degree of the reverse polynomial $\text{reverse}(f)$ is equal to the difference between the degree of $f$ and the degree of its trailing term. That is, \[ \deg(\text{reverse}(f)) = \deg(f) - \deg_{\text{trailing}}(f), \] where $\deg_{\text{trailing}}(f)$ denotes the degree of the trailing (lowest-degree) term of $f$.

Polynomial.reverse_leadingCoeff theorem

(f : R[X]) : f.reverse.leadingCoeff = f.trailingCoeff

Full source

theorem reverse_leadingCoeff (f : R[X]) : f.reverse.leadingCoeff = f.trailingCoeff := by
  rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
    coeff_reverse, revAt_invol, trailingCoeff]

Leading coefficient of reverse polynomial equals trailing coefficient of original polynomial

Informal description

For any polynomial $f \in R[X]$, the leading coefficient of the reverse polynomial $\operatorname{reverse} f$ is equal to the trailing coefficient of $f$, i.e., \[ \text{leadingCoeff}(\operatorname{reverse} f) = \text{trailingCoeff}(f). \]

Polynomial.natTrailingDegree_reverse theorem

(f : R[X]) : f.reverse.natTrailingDegree = 0

Full source

theorem natTrailingDegree_reverse (f : R[X]) : f.reverse.natTrailingDegree = 0 := by
  rw [natTrailingDegree_eq_zero, reverse_eq_zero, coeff_zero_reverse, leadingCoeff_ne_zero]
  exact eq_or_ne _ _

Natural trailing degree of reverse polynomial is zero

Informal description

For any polynomial $f \in R[X]$, the natural trailing degree of its reverse polynomial $\text{reverse}\, f$ is zero. That is, the smallest exponent with a nonzero coefficient in $\text{reverse}\, f$ is zero.

Polynomial.reverse_trailingCoeff theorem

(f : R[X]) : f.reverse.trailingCoeff = f.leadingCoeff

Full source

theorem reverse_trailingCoeff (f : R[X]) : f.reverse.trailingCoeff = f.leadingCoeff := by
  rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]

Trailing coefficient of reverse polynomial equals leading coefficient of original polynomial

Informal description

For any polynomial $f \in R[X]$, the trailing coefficient of its reverse polynomial $\operatorname{reverse} f$ is equal to the leading coefficient of $f$, i.e., \[ (\operatorname{reverse} f)(0) = \text{leadingCoeff}\, f. \]

Polynomial.reverse_mul theorem

{f g : R[X]} (fg : f.leadingCoeff * g.leadingCoeff ≠ 0) : reverse (f * g) = reverse f * reverse g

Full source

theorem reverse_mul {f g : R[X]} (fg : f.leadingCoeff * g.leadingCoeff ≠ 0) :
    reverse (f * g) = reverse f * reverse g := by
  unfold reverse
  rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]

Reverse of Polynomial Product: $\operatorname{reverse}(f \cdot g) = \operatorname{reverse}(f) \cdot \operatorname{reverse}(g)$ under Nonzero Leading Coefficients Condition

Informal description

Let $R$ be a semiring and let $f, g \in R[X]$ be polynomials such that the product of their leading coefficients is nonzero, i.e., $f.\text{leadingCoeff} \cdot g.\text{leadingCoeff} \neq 0$. Then the reverse of the product $f \cdot g$ is equal to the product of the reverses of $f$ and $g$: \[ \operatorname{reverse}(f \cdot g) = \operatorname{reverse}(f) \cdot \operatorname{reverse}(g). \]

Polynomial.reverse_mul_of_domain theorem

{R : Type*} [Semiring R] [NoZeroDivisors R] (f g : R[X]) : reverse (f * g) = reverse f * reverse g

Full source

@[simp]
theorem reverse_mul_of_domain {R : Type*} [Semiring R] [NoZeroDivisors R] (f g : R[X]) :
    reverse (f * g) = reverse f * reverse g := by
  by_cases f0 : f = 0
  · simp only [f0, zero_mul, reverse_zero]
  by_cases g0 : g = 0
  · rw [g0, mul_zero, reverse_zero, mul_zero]
  simp [reverse_mul, *]

Reverse of Polynomial Product in Semiring without Zero Divisors: $\operatorname{reverse}(f \cdot g) = \operatorname{reverse}(f) \cdot \operatorname{reverse}(g)$

Informal description

Let $R$ be a semiring with no zero divisors, and let $f, g \in R[X]$ be polynomials. Then the reverse of the product $f \cdot g$ is equal to the product of the reverses of $f$ and $g$: \[ \operatorname{reverse}(f \cdot g) = \operatorname{reverse}(f) \cdot \operatorname{reverse}(g). \]

Polynomial.trailingCoeff_mul theorem

{R : Type*} [Semiring R] [NoZeroDivisors R] (p q : R[X]) : (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Full source

theorem trailingCoeff_mul {R : Type*} [Semiring R] [NoZeroDivisors R] (p q : R[X]) :
    (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff := by
  rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]

Product of Trailing Coefficients in Polynomial Multiplication

Informal description

Let $R$ be a semiring with no zero divisors, and let $p, q \in R[X]$ be polynomials. Then the trailing coefficient of the product $p \cdot q$ is equal to the product of the trailing coefficients of $p$ and $q$, i.e., \[ \text{trailingCoeff}(p \cdot q) = \text{trailingCoeff}(p) \cdot \text{trailingCoeff}(q). \]

Polynomial.coeff_one_reverse theorem

(f : R[X]) : coeff (reverse f) 1 = nextCoeff f

Full source

@[simp]
theorem coeff_one_reverse (f : R[X]) : coeff (reverse f) 1 = nextCoeff f := by
  rw [coeff_reverse, nextCoeff]
  split_ifs with hf
  · have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])
    simp [*, revAt]
  · rw [revAt_le]
    exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)

Coefficient of Degree One in Reverse Polynomial Equals Next Coefficient

Informal description

For any polynomial $f \in R[X]$, the coefficient of degree $1$ in the reverse polynomial $\text{reverse}\, f$ is equal to the next coefficient of $f$ (i.e., the coefficient of degree $\text{natDegree}\, f - 1$ if $\text{natDegree}\, f \geq 1$, and $0$ otherwise).

Polynomial.reverse_C theorem

(t : R) : reverse (C t) = C t

Full source

@[simp] lemma reverse_C (t : R) :
    reverse (C t) = C t := by
  simp [reverse]

Reverse of Constant Polynomial: $\text{reverse}(t) = t$

Informal description

For any element $t$ in a semiring $R$, the reverse of the constant polynomial $C(t)$ is equal to $C(t)$, i.e., $\text{reverse}(t) = t$.

Polynomial.reverse_mul_X theorem

(p : R[X]) : reverse (p * X) = reverse p

Full source

@[simp] lemma reverse_mul_X (p : R[X]) : reverse (p * X) = reverse p := by
  nontriviality R
  rcases eq_or_ne p 0 with rfl | hp
  · simp
  · simp [reverse, hp]

Reverse of Polynomial Multiplied by $X$: $\operatorname{reverse}(p \cdot X) = \operatorname{reverse}(p)$

Informal description

For any polynomial $p \in R[X]$, the reverse of the product $p \cdot X$ equals the reverse of $p$, i.e., \[ \operatorname{reverse}(p \cdot X) = \operatorname{reverse}(p). \]

Polynomial.reverse_X_mul theorem

(p : R[X]) : reverse (X * p) = reverse p

Full source

@[simp] lemma reverse_X_mul (p : R[X]) : reverse (X * p) = reverse p := by
  rw [commute_X p, reverse_mul_X]

Reverse of Polynomial Multiplied by $X$: $\operatorname{reverse}(X \cdot p) = \operatorname{reverse}(p)$

Informal description

For any polynomial $p \in R[X]$, the reverse of the product $X \cdot p$ equals the reverse of $p$, i.e., \[ \operatorname{reverse}(X \cdot p) = \operatorname{reverse}(p). \]

Polynomial.reverse_mul_X_pow theorem

(p : R[X]) (n : ℕ) : reverse (p * X ^ n) = reverse p

Full source

@[simp] lemma reverse_mul_X_pow (p : R[X]) (n : ℕ) : reverse (p * X ^ n) = reverse p := by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

Reverse of Polynomial Multiplied by $X^n$: $\operatorname{reverse}(p \cdot X^n) = \operatorname{reverse}(p)$

Informal description

For any polynomial $p \in R[X]$ and any natural number $n$, the reverse of the polynomial $p \cdot X^n$ equals the reverse of $p$, i.e., \[ \operatorname{reverse}(p \cdot X^n) = \operatorname{reverse}(p). \]

Polynomial.reverse_X_pow_mul theorem

(p : R[X]) (n : ℕ) : reverse (X ^ n * p) = reverse p

Full source

@[simp] lemma reverse_X_pow_mul (p : R[X]) (n : ℕ) : reverse (X ^ n * p) = reverse p := by
  rw [commute_X_pow p, reverse_mul_X_pow]

Reverse of Polynomial Multiplied by $X^n$: $\operatorname{reverse}(X^n \cdot p) = \operatorname{reverse}(p)$

Informal description

For any polynomial $p \in R[X]$ and any natural number $n$, the reverse of the polynomial $X^n \cdot p$ equals the reverse of $p$, i.e., \[ \operatorname{reverse}(X^n \cdot p) = \operatorname{reverse}(p). \]

Polynomial.reverse_add_C theorem

(p : R[X]) (t : R) : reverse (p + C t) = reverse p + C t * X ^ p.natDegree

Full source

@[simp] lemma reverse_add_C (p : R[X]) (t : R) :
    reverse (p + C t) = reverse p + C t * X ^ p.natDegree := by
  simp [reverse]

Reverse of Polynomial Plus Constant: $\text{reverse}(p + t) = \text{reverse}(p) + t X^{\text{deg}\, p}$

Informal description

For any polynomial $p \in R[X]$ and any element $t \in R$, the reverse of the polynomial $p + t$ (where $t$ is treated as a constant polynomial) is equal to the reverse of $p$ plus $t X^{\text{natDegree}\, p}$. That is, \[ \text{reverse}(p + t) = \text{reverse}(p) + t X^{\text{natDegree}\, p}. \]

Polynomial.reverse_C_add theorem

(p : R[X]) (t : R) : reverse (C t + p) = C t * X ^ p.natDegree + reverse p

Full source

@[simp] lemma reverse_C_add (p : R[X]) (t : R) :
    reverse (C t + p) = C t * X ^ p.natDegree + reverse p := by
  rw [add_comm, reverse_add_C, add_comm]

Reverse of Constant Plus Polynomial: $\text{reverse}(t + p) = t X^{\deg p} + \text{reverse}(p)$

Informal description

For any polynomial $p \in R[X]$ and any element $t \in R$, the reverse of the polynomial $t + p$ (where $t$ is treated as a constant polynomial) is equal to $t X^{\text{natDegree}\, p}$ plus the reverse of $p$. That is, \[ \text{reverse}(t + p) = t X^{\text{natDegree}\, p} + \text{reverse}(p). \]

Polynomial.eval₂_reverse_mul_pow theorem

(i : R →+* S) (x : S) [Invertible x] (f : R[X]) : eval₂ i (⅟ x) (reverse f) * x ^ f.natDegree = eval₂ i x f

Full source

theorem eval₂_reverse_mul_pow (i : R →+* S) (x : S) [Invertible x] (f : R[X]) :
    eval₂ i (⅟ x) (reverse f) * x ^ f.natDegree = eval₂ i x f :=
  eval₂_reflect_mul_pow i _ _ f le_rfl

Evaluation of Reversed Polynomial: $\text{eval}_2(i, x^{-1}, \text{reverse}(f)) \cdot x^{\deg(f)} = \text{eval}_2(i, x, f)$

Informal description

Let $R$ and $S$ be commutative semirings, $i : R \to S$ a ring homomorphism, and $x \in S$ an invertible element. For any polynomial $f \in R[X]$, the following equality holds: \[ \text{eval}_2(i, x^{-1}, \text{reverse}(f)) \cdot x^{\deg(f)} = \text{eval}_2(i, x, f), \] where $\text{eval}_2$ denotes polynomial evaluation via the homomorphism $i$, and $\text{reverse}(f)$ is the polynomial obtained by reversing the coefficients of $f$ (i.e., $\text{reverse}(f) = X^{\deg(f)} \cdot f(1/X)$).

Polynomial.eval₂_reverse_eq_zero_iff theorem

(i : R →+* S) (x : S) [Invertible x] (f : R[X]) : eval₂ i (⅟ x) (reverse f) = 0 ↔ eval₂ i x f = 0

Full source

@[simp]
theorem eval₂_reverse_eq_zero_iff (i : R →+* S) (x : S) [Invertible x] (f : R[X]) :
    eval₂eval₂ i (⅟ x) (reverse f) = 0 ↔ eval₂ i x f = 0 :=
  eval₂_reflect_eq_zero_iff i x _ _ le_rfl

Equivalence of Zero Evaluations for Reversed Polynomials: $\text{eval}_2(i, x^{-1}, \text{reverse}(f)) = 0 \leftrightarrow \text{eval}_2(i, x, f) = 0$

Informal description

Let $R$ and $S$ be commutative semirings, $i : R \to S$ a ring homomorphism, and $x \in S$ an invertible element. For any polynomial $f \in R[X]$, the following equivalence holds: \[ \text{eval}_2(i, x^{-1}, \text{reverse}(f)) = 0 \quad \text{if and only if} \quad \text{eval}_2(i, x, f) = 0, \] where $\text{eval}_2$ denotes polynomial evaluation via the homomorphism $i$, and $\text{reverse}(f)$ is the polynomial obtained by reversing the coefficients of $f$ (i.e., $\text{reverse}(f) = X^{\deg(f)} \cdot f(1/X)$).

Polynomial.reflect_neg theorem

(f : R[X]) (N : ℕ) : reflect N (-f) = -reflect N f

Full source

@[simp]
theorem reflect_neg (f : R[X]) (N : ℕ) : reflect N (-f) = -reflect N f := by
  rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]

Negation Commutes with Polynomial Reflection: $\text{reflect}_N(-f) = -\text{reflect}_N(f)$

Informal description

For any polynomial $f \in R[X]$ and any natural number $N$, the reflection of $-f$ at degree $N$ equals the negation of the reflection of $f$ at degree $N$, i.e., \[ \text{reflect}_N(-f) = -\text{reflect}_N(f). \]

Polynomial.reflect_sub theorem

(f g : R[X]) (N : ℕ) : reflect N (f - g) = reflect N f - reflect N g

Full source

@[simp]
theorem reflect_sub (f g : R[X]) (N : ℕ) : reflect N (f - g) = reflect N f - reflect N g := by
  rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]

Subtraction Commutes with Polynomial Reflection: $\text{reflect}_N(f - g) = \text{reflect}_N f - \text{reflect}_N g$

Informal description

For any polynomials $f, g \in R[X]$ and any natural number $N$, the reflection of their difference equals the difference of their reflections: \[ \text{reflect}_N(f - g) = \text{reflect}_N f - \text{reflect}_N g. \]

Polynomial.reverse_neg theorem

(f : R[X]) : reverse (-f) = -reverse f

Full source

@[simp]
theorem reverse_neg (f : R[X]) : reverse (-f) = -reverse f := by
  rw [reverse, reverse, reflect_neg, natDegree_neg]

Negation Commutes with Polynomial Reversal: $\text{reverse}(-f) = -\text{reverse}(f)$

Informal description

For any polynomial $f$ over a ring $R$, the reverse of $-f$ is equal to the negative of the reverse of $f$, i.e., \[ \text{reverse}(-f) = -\text{reverse}(f). \]