Lemmas on the degree of Polynomials

Stream: Is there code for X?

[Xavier Xarles]

I was not able to find the following two lemmas on the degree of polynomials. I provided a proof to be sure they are correct.

import Mathlib.Algebra.Polynomial.Degree.Definitions

open Polynomial

variable [Semiring R] {p : Polynomial R} {q : Polynomial R}

theorem natDegree_add_eq_natDegree_leadingCoeff_add_zero_lt
    (hd: p.natDegree = q.natDegree) (h : leadingCoeff p + leadingCoeff q = 0) (hne: p.natDegree ≠ 0):
    natDegree (p + q) < p.natDegree := by
    have hm: p.natDegree= max p.natDegree q.natDegree:= by rw[hd]; exact Eq.symm (max_self q.natDegree)
    have hsum : (p + q).coeff p.natDegree = 0 := by
        rw [←h, leadingCoeff, leadingCoeff, hd.symm]
        exact coeff_add p q p.natDegree
    cases eq_or_ne (p+q) 0 with
    | inl hq => exact hq ▸ Nat.sub_ne_zero_iff_lt.mp hne
    | inr hp =>
      have pqne :(p + q).natDegree ≠ p.natDegree := by
        by_contra uu
        rw [uu.symm, ←leadingCoeff, leadingCoeff_eq_zero] at hsum
        exact hp hsum
      have hadd :=Polynomial.natDegree_add_le p q
      rw [lt_iff_le_and_ne]
      exact ⟨hm▸hadd, pqne⟩

theorem degree_add_eq_degree_leadingCoeff_add_zero_lt
    (hd: p.degree = q.degree) (h : leadingCoeff p + leadingCoeff q = 0) (hne: p ≠ 0):
    degree (p + q) < p.degree := by
  cases eq_or_ne (p+q) 0 with
  | inl hq => rw[hq, @degree_zero,@WithBot.bot_lt_iff_ne_bot]; exact degree_ne_bot.mpr hne
  | inr hp =>
    have hpq : p.degree ≠ 0 := by
      by_contra uu
      have hCp : p = C (p.leadingCoeff):= by
         rw [leadingCoeff, natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq uu)]
         exact eq_C_of_degree_le_zero (le_of_eq uu)
      have hCq : q = C (q.leadingCoeff):= by
         rw [leadingCoeff, natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq (hd ▸ uu))]
         exact eq_C_of_degree_le_zero (le_of_eq (hd ▸ uu))
      rw [hCp, hCq, (@C_add).symm] at hp
      exact hp (@C_0 R _ ▸ (congrArg (⇑C) h))
    rw [degree_eq_natDegree hne] at hpq
    rw [degree_eq_natDegree hne, degree_eq_natDegree hp,Nat.cast_lt]
    have hdd :=natDegree_eq_of_degree_eq hd
    exact natDegree_add_eq_natDegree_leadingCoeff_add_zero_lt hdd h (fun a => hpq (congrArg Nat.cast a))

[Damiano Testa]

I suspect that they are not in the library. Below is a small golfing: I am a little disappointed by how little (if at all) one proof helps the other...

theorem helper {n : Nat} (hp : p ≠ 0) (h0 : p.coeff n = 0) : p.natDegree ≠ n := by
  contrapose! h0
  simp [← h0, hp]

theorem natDegree_add_eq_natDegree_leadingCoeff_add_zero_lt
    (hd: p.natDegree = q.natDegree) (h : leadingCoeff p + leadingCoeff q = 0) (hne: p.natDegree ≠ 0):
    natDegree (p + q) < p.natDegree := by
  rcases eq_or_ne (p + q) 0 with (h0|h0)
  · simp [h0, Nat.zero_lt_of_ne_zero hne]
  apply lt_of_le_of_ne
  · apply (natDegree_add_le p q).trans <| by simp [hd]
  apply helper h0
  rw [coeff_add]
  convert h
  rw [hd]
  rfl

theorem degree_add_eq_degree_leadingCoeff_add_zero_lt
    (hd: p.degree = q.degree) (h : leadingCoeff p + leadingCoeff q = 0) (hne: p ≠ 0):
    degree (p + q) < p.degree := by
  obtain (h0|h0) := eq_or_ne p.natDegree 0
  · obtain ⟨c, rfl⟩ := natDegree_eq_zero.mp h0
    have hq0 : q.natDegree = 0 := by
      simpa [natDegree_eq_zero_iff_degree_le_zero, ← hd] using degree_C_le
    obtain ⟨d, rfl⟩ := natDegree_eq_zero.mp hq0
    rw [leadingCoeff_C, leadingCoeff_C] at h
    rw [← C_add, C_eq_zero.mpr h, degree_zero, degree_C]
    apply Ne.bot_lt WithBot.bot_ne_zero.symm
    simpa using hne
  apply degree_lt_degree (natDegree_add_eq_natDegree_leadingCoeff_add_zero_lt _ h h0)
  exact natDegree_eq_of_degree_eq hd

[Antoine Chambert-Loir]

I'd say one misses the result that says that degree p equals n iff degree p is at most n and coeff n p is nonzero. I have written similar results in the PR on monomial orders.

[Damiano Testa]

docs#Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, maybe?

[Xavier Xarles]

In fact, I found a version of one of the results I asked but for subtraction:
docs#Polynomial.degree_sub_lt

[Damiano Testa]

Ah, so that one can also be golfed with the proofs above!