Mathlib.Algebra.Polynomial.Inductions

Polynomial.divX definition

(p : R[X]) : R[X]

Full source

/-- `divX p` returns a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
  It can be used in a semiring where the usual division algorithm is not possible -/
def divX (p : R[X]) : R[X] :=
  ⟨AddMonoidAlgebra.divOf p.toFinsupp 1⟩

Polynomial division by X in a semiring

Informal description

For a polynomial $ p \in R[X] $ over a semiring $ R $, the function `divX` returns a polynomial $ q $ such that $ q \cdot X + C(p_0) = p $, where $ p_0 $ is the constant term of $ p $. This provides a way to "divide" $ p $ by $ X $ in semirings where the usual division algorithm is not available.

Polynomial.coeff_divX theorem

: (divX p).coeff n = p.coeff (n + 1)

Full source

@[simp]
theorem coeff_divX : (divX p).coeff n = p.coeff (n + 1) := by
  rw [add_comm]; cases p; rfl

Coefficient Shift under Polynomial Division by $X$: $(\text{divX}(p))_n = p_{n+1}$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the coefficient of $X^n$ in the polynomial $\text{divX}(p)$ is equal to the coefficient of $X^{n+1}$ in $p$, i.e., \[ (\text{divX}(p))_n = p_{n+1}. \]

Polynomial.divX_mul_X_add theorem

(p : R[X]) : divX p * X + C (p.coeff 0) = p

Full source

theorem divX_mul_X_add (p : R[X]) : divX p * X + C (p.coeff 0) = p :=
  ext <| by rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]

Polynomial Division Identity: $\text{divX}(p) \cdot X + C(p_0) = p$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the polynomial obtained by dividing $p$ by $X$ (denoted $\text{divX}(p)$) satisfies the equation: \[ \text{divX}(p) \cdot X + C(p_0) = p, \] where $C(p_0)$ is the constant polynomial formed from the constant term $p_0$ of $p$.

Polynomial.X_mul_divX_add theorem

(p : R[X]) : X * divX p + C (p.coeff 0) = p

Full source

@[simp]
theorem X_mul_divX_add (p : R[X]) : X * divX p + C (p.coeff 0) = p :=
  ext <| by rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]

Polynomial Division Identity: $X \cdot \text{divX}(p) + C(p_0) = p$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the following identity holds: \[ X \cdot \text{divX}(p) + C(p_0) = p, \] where $\text{divX}(p)$ is the polynomial obtained by dividing $p$ by $X$, and $C(p_0)$ is the constant polynomial formed from the constant term $p_0$ of $p$.

Polynomial.divX_C theorem

(a : R) : divX (C a) = 0

Full source

@[simp]
theorem divX_C (a : R) : divX (C a) = 0 :=
  ext fun n => by simp [coeff_divX, coeff_C, Finsupp.single_eq_of_ne _]

Division of Constant Polynomial by $X$ Yields Zero

Informal description

For any element $a$ in a semiring $R$, the polynomial obtained by dividing the constant polynomial $C(a)$ by $X$ is equal to the zero polynomial, i.e., $\mathrm{divX}(C(a)) = 0$.

Polynomial.divX_eq_zero_iff theorem

: divX p = 0 ↔ p = C (p.coeff 0)

Full source

theorem divX_eq_zero_iff : divXdivX p = 0 ↔ p = C (p.coeff 0) :=
  ⟨fun h => by simpa [eq_comm, h] using divX_mul_X_add p, fun h => by rw [h, divX_C]⟩

Characterization of Polynomials with Zero Division by $X$: $\mathrm{divX}(p) = 0 \leftrightarrow p = C(p_0)$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the polynomial obtained by dividing $p$ by $X$ is equal to the zero polynomial if and only if $p$ is equal to the constant polynomial formed from its constant term, i.e., \[ \mathrm{divX}(p) = 0 \leftrightarrow p = C(p_0), \] where $p_0$ is the coefficient of $X^0$ in $p$.

Polynomial.divX_add theorem

: divX (p + q) = divX p + divX q

Full source

theorem divX_add : divX (p + q) = divX p + divX q :=
  ext <| by simp

Additivity of Polynomial Division by $X$: $\mathrm{divX}(p + q) = \mathrm{divX}(p) + \mathrm{divX}(q)$

Informal description

For any polynomials $p, q \in R[X]$ over a semiring $R$, the operation of dividing by $X$ distributes over addition, i.e., \[ \mathrm{divX}(p + q) = \mathrm{divX}(p) + \mathrm{divX}(q). \]

Polynomial.divX_zero theorem

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

Full source

@[simp]
theorem divX_zero : divX (0 : R[X]) = 0 := leadingCoeff_eq_zero.mp rfl

Division by X of the Zero Polynomial Yields Zero

Informal description

For the zero polynomial $0$ in the polynomial ring $R[X]$, the result of dividing by $X$ is again the zero polynomial, i.e., $\mathrm{divX}(0) = 0$.

Polynomial.divX_one theorem

: divX (1 : R[X]) = 0

Full source

@[simp]
theorem divX_one : divX (1 : R[X]) = 0 := by
  ext
  simpa only [coeff_divX, coeff_zero] using coeff_one

Division of the Constant Polynomial 1 by $X$ Yields Zero

Informal description

For the constant polynomial $1 \in R[X]$, the result of dividing by $X$ is the zero polynomial, i.e., $\mathrm{divX}(1) = 0$.

Polynomial.divX_C_mul theorem

: divX (C a * p) = C a * divX p

Full source

@[simp]
theorem divX_C_mul : divX (C a * p) = C a * divX p := by
  ext
  simp

Linearity of Polynomial Division by $X$ under Constant Multiplication: $\mathrm{divX}(C(a) \cdot p) = C(a) \cdot \mathrm{divX}(p)$

Informal description

For any element $a \in R$ and polynomial $p \in R[X]$, the result of dividing the polynomial $C(a) \cdot p$ by $X$ is equal to $C(a)$ multiplied by the result of dividing $p$ by $X$, i.e., \[ \mathrm{divX}(C(a) \cdot p) = C(a) \cdot \mathrm{divX}(p). \]

Polynomial.divX_X_pow theorem

: divX (X ^ n : R[X]) = if (n = 0) then 0 else X ^ (n - 1)

Full source

theorem divX_X_pow : divX (X ^ n : R[X]) = if (n = 0) then 0 else X ^ (n - 1) := by
  cases n
  · simp
  · ext n
    simp [coeff_X_pow]

Division of Monomial $X^n$ by $X$: $\mathrm{divX}(X^n) = X^{n-1}$ for $n > 0$

Informal description

For any natural number $n$, the result of dividing the monomial $X^n$ by $X$ is the zero polynomial if $n = 0$, and $X^{n-1}$ otherwise. That is, \[ \mathrm{divX}(X^n) = \begin{cases} 0 & \text{if } n = 0, \\ X^{n-1} & \text{otherwise}. \end{cases} \]

Polynomial.divX_hom definition

: R[X] →+ R[X]

Full source

/-- `divX` as an additive homomorphism. -/
noncomputable
def divX_hom : R[X]R[X] →+ R[X] :=
  { toFun := divX
    map_zero' := divX_zero
    map_add' := fun _ _ => divX_add }

Additive homomorphism of polynomial division by $X$

Informal description

The additive homomorphism version of the polynomial division by $X$ function, which maps a polynomial $p \in R[X]$ to $\mathrm{divX}(p)$. This homomorphism preserves addition and maps the zero polynomial to itself.

Polynomial.divX_hom_toFun theorem

: divX_hom p = divX p

Full source

@[simp] theorem divX_hom_toFun : divX_hom p = divX p := rfl

$\mathrm{divX\_hom}$ coincides with $\mathrm{divX}$

Informal description

For any polynomial $p \in R[X]$, the additive homomorphism $\mathrm{divX\_hom}$ evaluated at $p$ is equal to $\mathrm{divX}(p)$.

Polynomial.natDegree_divX_eq_natDegree_tsub_one theorem

: p.divX.natDegree = p.natDegree - 1

Full source

theorem natDegree_divX_eq_natDegree_tsub_one : p.divX.natDegree = p.natDegree - 1 := by
  apply map_natDegree_eq_sub (φ := divX_hom)
  · intro f
    simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero
  · intros n c c0
    rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]
    split_ifs with n0
    · simp [n0]
    · exact natDegree_C_mul_X_pow (n - 1) c c0

Degree Reduction under Division by $X$: $\mathrm{deg}(\mathrm{divX}(p)) = \mathrm{deg}(p) - 1$

Informal description

For any polynomial $p \in R[X]$, the degree of the polynomial $\mathrm{divX}(p)$ is equal to the degree of $p$ minus one, i.e., \[ \mathrm{deg}(\mathrm{divX}(p)) = \mathrm{deg}(p) - 1. \]

Polynomial.natDegree_divX_le theorem

: p.divX.natDegree ≤ p.natDegree

Full source

theorem natDegree_divX_le : p.divX.natDegree ≤ p.natDegree :=
  natDegree_divX_eq_natDegree_tsub_one.trans_le (Nat.pred_le _)

Degree Bound under Division by $X$: $\mathrm{deg}(\mathrm{divX}(p)) \leq \mathrm{deg}(p)$

Informal description

For any polynomial $p \in R[X]$, the degree of the polynomial $\mathrm{divX}(p)$ is less than or equal to the degree of $p$, i.e., \[ \mathrm{deg}(\mathrm{divX}(p)) \leq \mathrm{deg}(p). \]

Polynomial.divX_C_mul_X_pow theorem

: divX (C a * X ^ n) = if n = 0 then 0 else C a * X ^ (n - 1)

Full source

theorem divX_C_mul_X_pow : divX (C a * X ^ n) = if n = 0 then 0 else C a * X ^ (n - 1) := by
  simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero]

Division of Monomial $aX^n$ by $X$: $\mathrm{divX}(aX^n) = aX^{n-1}$ for $n > 0$

Informal description

For any element $a$ in a semiring $R$ and any natural number $n$, the result of dividing the polynomial $aX^n$ by $X$ is given by: \[ \mathrm{divX}(aX^n) = \begin{cases} 0 & \text{if } n = 0, \\ aX^{n-1} & \text{otherwise}. \end{cases} \]

Polynomial.degree_divX_lt theorem

(hp0 : p ≠ 0) : (divX p).degree < p.degree

Full source

theorem degree_divX_lt (hp0 : p ≠ 0) : (divX p).degree < p.degree := by
  haveI := Nontrivial.of_polynomial_ne hp0
  calc
    degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
      if h : degree p ≤ 0 then by
        have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
        rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
        exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
      else by
        have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
        have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
        have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
        rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
    _ = degree p := congr_arg _ (divX_mul_X_add _)

Degree Reduction under Division by $X$: $\deg(\mathrm{divX}(p)) < \deg(p)$ for $p \neq 0$

Informal description

For any nonzero polynomial $p \in R[X]$ over a semiring $R$, the degree of the polynomial obtained by dividing $p$ by $X$ is strictly less than the degree of $p$, i.e., $\deg(\mathrm{divX}(p)) < \deg(p)$.

Polynomial.recOnHorner definition

 {M : R[X] → Sort*} (p : R[X]) (M0 : M 0) (MC : ∀ p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a))
  (MX : ∀ p, p ≠ 0 → M p → M (p * X)) : M p

Full source

/-- An induction principle for polynomials, valued in Sort* instead of Prop. -/
@[elab_as_elim]
noncomputable def recOnHorner {M : R[X] → Sort*} (p : R[X]) (M0 : M 0)
    (MC : ∀ p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a))
    (MX : ∀ p, p ≠ 0 → M p → M (p * X)) : M p :=
  letI := Classical.decEq R
  if hp : p = 0 then hp ▸ M0
  else by
    have wf : degree (divX p) < degree p := degree_divX_lt hp
    rw [← divX_mul_X_add p] at *
    exact
      if hcp0 : coeff p 0 = 0 then by
        rw [hcp0, C_0, add_zero]
        exact
          MX _ (fun h : divX p = 0 => by simp [h, hcp0] at hp) (recOnHorner (divX p) M0 MC MX)
      else
        MC _ _ (coeff_mul_X_zero _) hcp0
          (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0
          else MX (divX p) hpX0 (recOnHorner _ M0 MC MX))
termination_by p.degree

Horner's scheme induction for polynomials

Informal description

Given a polynomial $p \in R[X]$ and a type family $M : R[X] \to \text{Sort}*$, the principle of induction on $p$ via Horner's scheme states that to prove $M(p)$ holds, it suffices to: 1. Show $M(0)$ holds (base case). 2. For any polynomial $p$ and element $a \in R$, if the constant term of $p$ is zero, $a$ is nonzero, and $M(p)$ holds, then $M(p + C(a))$ holds (addition of a constant term). 3. For any nonzero polynomial $p$, if $M(p)$ holds, then $M(p \cdot X)$ holds (multiplication by $X$). This induction principle allows proving properties of polynomials by decomposing them into their Horner form.

Polynomial.degree_pos_induction_on theorem

 {P : R[X] → Prop} (p : R[X]) (h0 : 0 < degree p) (hC : ∀ {a}, a ≠ 0 → P (C a * X))
  (hX : ∀ {p}, 0 < degree p → P p → P (p * X)) (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p

Full source

/-- A property holds for all polynomials of positive `degree` with coefficients in a semiring `R`
if it holds for
* `a * X`, with `a ∈ R`,
* `p * X`, with `p ∈ R[X]`,
* `p + a`, with `a ∈ R`, `p ∈ R[X]`,
with appropriate restrictions on each term.

See `natDegree_ne_zero_induction_on` for a similar statement involving no explicit multiplication.
-/
@[elab_as_elim]
theorem degree_pos_induction_on {P : R[X] → Prop} (p : R[X]) (h0 : 0 < degree p)
    (hC : ∀ {a}, a ≠ 0 → P (C a * X)) (hX : ∀ {p}, 0 < degree p → P p → P (p * X))
    (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
  recOnHorner p (fun h => by rw [degree_zero] at h; exact absurd h (by decide))
    (fun p a heq0 _ ih h0 =>
      (have : 0 < degree p :=
        (lt_of_not_ge fun h =>
          not_lt_of_ge (degree_C_le (a := a)) <|
            by rwa [eq_C_of_degree_le_zero h, ← C_add,heq0,zero_add] at h0)
      hadd this (ih this)))
    (fun p _ ih h0' =>
      if h0 : 0 < degree p then hX h0 (ih h0)
      else by
        rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢
        exact hC fun h : coeff p 0 = 0 => by simp [h, Nat.not_lt_zero] at h0')
    h0

Induction Principle for Polynomials of Positive Degree

Informal description

Let $R$ be a semiring and $P$ a property of polynomials in $R[X]$. For any polynomial $p \in R[X]$ with positive degree, if the following conditions hold: 1. For any nonzero $a \in R$, the property $P$ holds for the polynomial $aX$ (i.e., $P(aX)$). 2. For any polynomial $p$ with positive degree, if $P(p)$ holds, then $P(p \cdot X)$ holds. 3. For any polynomial $p$ with positive degree and any $a \in R$, if $P(p)$ holds, then $P(p + a)$ holds, then the property $P$ holds for $p$.

Polynomial.natDegree_ne_zero_induction_on theorem

 {M : R[X] → Prop} {f : R[X]} (f0 : f.natDegree ≠ 0) (h_C_add : ∀ {a p}, M p → M (C a + p))
  (h_add : ∀ {p q}, M p → M q → M (p + q)) (h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (monomial n a)) : M f

Full source

/-- A property holds for all polynomials of non-zero `natDegree` with coefficients in a
semiring `R` if it holds for
* `p + a`, with `a ∈ R`, `p ∈ R[X]`,
* `p + q`, with `p, q ∈ R[X]`,
* monomials with nonzero coefficient and non-zero exponent,
with appropriate restrictions on each term.
Note that multiplication is "hidden" in the assumption on monomials, so there is no explicit
multiplication in the statement.
See `degree_pos_induction_on` for a similar statement involving more explicit multiplications.
-/
@[elab_as_elim]
theorem natDegree_ne_zero_induction_on {M : R[X] → Prop} {f : R[X]} (f0 : f.natDegree ≠ 0)
    (h_C_add : ∀ {a p}, M p → M (C a + p)) (h_add : ∀ {p q}, M p → M q → M (p + q))
    (h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (monomial n a)) : M f := by
  suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
  refine Polynomial.induction_on f ?_ ?_ ?_
  · exact fun a => Or.inl (natDegree_C _)
  · rintro p q (hp | hp) (hq | hq)
    · refine Or.inl ?_
      rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp
    · exact Or.inr (h_add hp hq)
  · intro n a _
    by_cases a0 : a = 0
    · exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
    · refine Or.inr ?_
      rw [C_mul_X_pow_eq_monomial]
      exact h_monomial a0 n.succ_ne_zero

Induction Principle for Polynomials with Nonzero Degree via Constants, Addition, and Monomials

Informal description

Let $R$ be a semiring and $M$ be a property of polynomials in $R[X]$. For any polynomial $f \in R[X]$ with nonzero `natDegree`, if the following conditions hold: 1. For any $a \in R$ and polynomial $p \in R[X]$, if $M(p)$ holds, then $M(C(a) + p)$ holds. 2. For any polynomials $p, q \in R[X]$, if $M(p)$ and $M(q)$ hold, then $M(p + q)$ holds. 3. For any nonzero $a \in R$ and nonzero $n \in \mathbb{N}$, $M(a X^n)$ holds (where $a X^n$ is the monomial with coefficient $a$ and exponent $n$), then $M(f)$ holds.