feat(data/polynomial/degree/erase_lead): definition and basic lemmas (#4527)

erase_lead serves as the reduction step in an induction, breaking off one monomial from a polynomial.  It is used in a later PR to prove that reverse is a multiplicative monoid map on polynomials.



Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: 3 people

src/data/finset/basic.lean

@@ -100,6 +100,8 @@ theorem subset_def {s₁ s₂ : finset α} : s₁ ⊆ s₂ ↔ s₁.1 ⊆ s₂.1
 
 @[simp] theorem subset.refl (s : finset α) : s ⊆ s := subset.refl _
 
+theorem subset_of_eq {s t : finset α} (h : s = t) : s ⊆ t := h ▸ subset.refl _
+
 theorem subset.trans {s₁ s₂ s₃ : finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ := subset.trans
 
 theorem superset.trans {s₁ s₂ s₃ : finset α} : s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃ :=
@@ -1641,6 +1643,14 @@ theorem card_erase_lt_of_mem [decidable_eq α] {a : α} {s : finset α} :
 theorem card_erase_le [decidable_eq α] {a : α} {s : finset α} :
   card (erase s a) ≤ card s := card_erase_le
 
+theorem pred_card_le_card_erase [decidable_eq α] {a : α} {s : finset α} :
+  card s - 1 ≤ card (erase s a) :=
+begin
+  by_cases h : a ∈ s,
+  { rw [card_erase_of_mem h], refl },
+  { rw [erase_eq_of_not_mem h], apply nat.sub_le }
+end
+
 @[simp] theorem card_range (n : ℕ) : card (range n) = n := card_range n
 
 @[simp] theorem card_attach {s : finset α} : card (attach s) = card s := multiset.card_attach

src/data/finsupp/basic.lean

@@ -102,6 +102,9 @@ lemma ext_iff {f g : α →₀ β} : f = g ↔ (∀a:α, f a = g a) :=
 ⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext_iff.1 h a).1 $
   mem_support_iff.2 H, by rintro rfl; refl⟩
 
+lemma card_support_eq_zero {f : α →₀ β} : card f.support = 0 ↔ f = 0 :=
+by simp
+
 instance finsupp.decidable_eq [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
 assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a))
   ⟨assume ⟨h₁, h₂⟩, ext $ assume a,
@@ -174,6 +177,15 @@ assume b₁ b₂ eq,
 have (single a b₁ : α →₀ β) a = (single a b₂ : α →₀ β) a, by rw eq,
 by rwa [single_eq_same, single_eq_same] at this
 
+lemma eq_single_iff {f : α →₀ β} {a b} : f = single a b ↔ f.support ⊆ {a} ∧ f a = b :=
+begin
+  refine ⟨λ h, h.symm ▸ ⟨support_single_subset, single_eq_same⟩, _⟩,
+  rintro ⟨h, rfl⟩,
+  ext x,
+  by_cases hx : a = x; simp only [hx, single_eq_same, single_eq_of_ne, ne.def, not_false_iff],
+  exact not_mem_support_iff.1 (mt (λ hx, (mem_singleton.1 (h hx)).symm) hx)
+end
+
 lemma single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : β) :
   single a₁ b₁ = single a₂ b₂ ↔ ((a₁ = a₂ ∧ b₁ = b₂) ∨ (b₁ = 0 ∧ b₂ = 0)) :=
 begin
@@ -219,6 +231,22 @@ lemma unique_ext_iff [unique α] {f g : α →₀ β} : f = g ↔  f (default α
   single a b = single a' b' ↔ b = b' :=
 by rw [unique_ext_iff, unique.eq_default a, unique.eq_default a', single_eq_same, single_eq_same]
 
+lemma support_eq_singleton {f : α →₀ β} {a : α} :
+  f.support = {a} ↔ f a ≠ 0 ∧ f = single a (f a) :=
+⟨λ h, ⟨mem_support_iff.1 $ h.symm ▸ finset.mem_singleton_self a,
+  eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩, λ h, h.2.symm ▸ support_single_ne_zero h.1⟩
+
+lemma support_eq_singleton' {f : α →₀ β} {a : α} :
+  f.support = {a} ↔ ∃ b ≠ 0, f = single a b :=
+⟨λ h, let h := support_eq_singleton.1 h in ⟨_, h.1, h.2⟩,
+  λ ⟨b, hb, hf⟩, hf.symm ▸ support_single_ne_zero hb⟩
+
+lemma card_support_eq_one {f : α →₀ β} : card f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a) :=
+by simp only [card_eq_one, support_eq_singleton]
+
+lemma card_support_eq_one' {f : α →₀ β} : card f.support = 1 ↔ ∃ a (b ≠ 0), f = single a b :=
+by simp only [card_eq_one, support_eq_singleton']
+
 end single
 
 /-! ### Declarations about `on_finset` -/
@@ -442,6 +470,10 @@ begin
   { rw [erase_ne hs] }
 end
 
+@[simp] lemma erase_zero [has_zero β] (a : α) :
+  erase a (0 : α →₀ β) = 0 :=
+by rw [← support_eq_empty, support_erase, support_zero, erase_empty]
+
 end erase
 
 /-!

src/data/polynomial/basic.lean

@@ -137,18 +137,18 @@ begin
     exact finset.subset.refl {n}, },
 end
 
-lemma monomial_eq_X_pow (n) : X^n = monomial n (1:R) :=
+lemma X_pow_eq_monomial (n) : X ^ n = monomial n (1:R) :=
 begin
   induction n with n hn,
-    { refl, },
-    { conv_rhs {rw nat.succ_eq_add_one, congr, skip, rw ← mul_one (1:R)},
-      rw [← monomial_mul_monomial, ← hn, pow_succ, X_mul, X], },
+  { refl, },
+  { conv_rhs {rw nat.succ_eq_add_one, congr, skip, rw ← mul_one (1:R)},
+    rw [← monomial_mul_monomial, ← hn, pow_succ, X_mul, X], },
 end
 
 lemma support_X_pow (H : ¬ (1:R) = 0) (n : ℕ) : (X^n : polynomial R).support = singleton n :=
 begin
   convert support_monomial n 1 H,
-  exact monomial_eq_X_pow n,
+  exact X_pow_eq_monomial n,
 end
 
 lemma support_X_empty (H : (1:R)=0) : (X : polynomial R).support = ∅ :=

src/data/polynomial/degree.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.eval
+import tactic.interval_cases
 
 /-!
 # Theory of degrees of polynomials
@@ -148,6 +149,25 @@ end
 
 end injective
 
+section
+variable {f : polynomial R}
+
+lemma monomial_nat_degree_leading_coeff_eq_self (h : f.support.card ≤ 1) :
+  monomial f.nat_degree f.leading_coeff = f :=
+begin
+  interval_cases f.support.card with H,
+  { have : f = 0 := finsupp.card_support_eq_zero.1 H,
+    simp [this] },
+  { obtain ⟨n, x, hx, rfl : f = monomial n x⟩ := finsupp.card_support_eq_one'.1 H,
+    simp [hx] }
+end
+
+lemma C_mul_X_pow_eq_self (h : f.support.card ≤ 1) :
+  C f.leading_coeff * X^f.nat_degree = f :=
+by rw [C_mul_X_pow_eq_monomial, monomial_nat_degree_leading_coeff_eq_self h]
+
+end
+
 end degree
 end semiring
 

src/data/polynomial/degree/basic.lean

@@ -173,6 +173,10 @@ if h : a = 0 then by rw [h, C_0, zero_mul]; exact bot_le else le_of_eq (degree_m
 @[simp] lemma nat_degree_C_mul_X_pow (n : ℕ) (a : R) (ha : a ≠ 0) : nat_degree (C a * X ^ n) = n :=
 nat_degree_eq_of_degree_eq_some (degree_monomial n ha)
 
+@[simp] lemma nat_degree_monomial (i : ℕ) (r : R) (hr : r ≠ 0) :
+  nat_degree (monomial i r) = i :=
+by rw [← C_mul_X_pow_eq_monomial, nat_degree_C_mul_X_pow i r hr]
+
 lemma coeff_eq_zero_of_degree_lt (h : degree p < n) : coeff p n = 0 :=
 not_not.1 (mt le_degree_of_ne_zero (not_le_of_gt h))
 
@@ -540,6 +544,9 @@ begin
     exact @finsupp.single_eq_same _ _ _ n a }
 end
 
+@[simp] lemma leading_coeff_monomial' (a : R) (n : ℕ) : leading_coeff (monomial n a) = a :=
+by rw [← C_mul_X_pow_eq_monomial, leading_coeff_monomial]
+
 @[simp] lemma leading_coeff_C (a : R) : leading_coeff (C a) = a :=
 suffices leading_coeff (C a * X^0) = a, by rwa [pow_zero, mul_one] at this,
 leading_coeff_monomial a 0

src/data/polynomial/erase_lead.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2020 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import data.polynomial.degree.basic
+import data.polynomial.degree.trailing_degree
+
+/-!
+# Erase the leading term of a univariate polynomial
+
+## Definition
+
+* `erase_lead f`: the polynomial `f - leading term of f`
+
+`erase_lead` serves as reduction step in an induction, shaving off one monomial from a polynomial.
+The definition is set up so that it does not mention subtraction in the definition,
+and thus works for polynomials over semirings as well as rings.
+-/
+
+noncomputable theory
+open_locale classical
+
+open polynomial finsupp finset
+
+namespace polynomial
+
+variables {R : Type*} [semiring R] {f : polynomial R}
+
+/-- `erase_lead f` for a polynomial `f` is the polynomial obtained by
+subtracting from `f` the leading term of `f`. -/
+def erase_lead (f : polynomial R) : polynomial R :=
+finsupp.erase f.nat_degree f
+
+section erase_lead
+
+lemma erase_lead_support (f : polynomial R) :
+  f.erase_lead.support = f.support.erase f.nat_degree :=
+-- `rfl` fails because LHS uses `nat.decidable_eq` but RHS is classical.
+by convert rfl
+
+lemma erase_lead_coeff (i : ℕ) :
+  f.erase_lead.coeff i = if i = f.nat_degree then 0 else f.coeff i :=
+-- `rfl` fails because LHS uses `nat.decidable_eq` but RHS is classical.
+by convert rfl
+
+@[simp] lemma erase_lead_coeff_nat_degree : f.erase_lead.coeff f.nat_degree = 0 :=
+finsupp.erase_same
+
+lemma erase_lead_coeff_of_ne (i : ℕ) (hi : i ≠ f.nat_degree) :
+  f.erase_lead.coeff i = f.coeff i :=
+finsupp.erase_ne hi
+
+@[simp] lemma erase_lead_zero : erase_lead (0 : polynomial R) = 0 :=
+finsupp.erase_zero _
+
+@[simp] lemma erase_lead_add_monomial_nat_degree_leading_coeff (f : polynomial R) :
+  f.erase_lead + monomial f.nat_degree f.leading_coeff = f :=
+begin
+  ext i,
+  simp only [erase_lead_coeff, coeff_monomial, coeff_add, @eq_comm _ _ i],
+  split_ifs with h,
+  { subst i, simp only [leading_coeff, zero_add] },
+  { exact add_zero _ }
+end
+
+@[simp] lemma erase_lead_add_C_mul_X_pow (f : polynomial R) :
+  f.erase_lead + (C f.leading_coeff) * X ^ f.nat_degree = f :=
+by rw [C_mul_X_pow_eq_monomial, erase_lead_add_monomial_nat_degree_leading_coeff]
+
+@[simp] lemma self_sub_monomial_nat_degree_leading_coeff {R : Type*} [ring R] (f : polynomial R) :
+  f - monomial f.nat_degree f.leading_coeff = f.erase_lead :=
+(eq_sub_iff_add_eq.mpr (erase_lead_add_monomial_nat_degree_leading_coeff f)).symm
+
+@[simp] lemma self_sub_C_mul_X_pow {R : Type*} [ring R] (f : polynomial R) :
+  f - (C f.leading_coeff) * X ^ f.nat_degree = f.erase_lead :=
+by rw [C_mul_X_pow_eq_monomial, self_sub_monomial_nat_degree_leading_coeff]
+
+lemma erase_lead_ne_zero (f0 : 2 ≤ f.support.card) : erase_lead f ≠ 0 :=
+begin
+  rw [ne.def, ← finsupp.card_support_eq_zero, erase_lead_support],
+  exact (zero_lt_one.trans_le $ (nat.sub_le_sub_right f0 1).trans
+    finset.pred_card_le_card_erase).ne.symm
+end
+
+@[simp] lemma nat_degree_not_mem_erase_lead_support : f.nat_degree ∉ (erase_lead f).support :=
+by convert not_mem_erase _ _
+
+lemma ne_nat_degree_of_mem_erase_lead_support {a : ℕ} (h : a ∈ (erase_lead f).support) :
+  a ≠ f.nat_degree :=
+by { rintro rfl, exact nat_degree_not_mem_erase_lead_support h }
+
+lemma erase_lead_support_card_lt (h : f ≠ 0) : (erase_lead f).support.card < f.support.card :=
+begin
+  rw erase_lead_support,
+  exact card_lt_card (erase_ssubset $ nat_degree_mem_support_of_nonzero h)
+end
+
+@[simp] lemma erase_lead_monomial (i : ℕ) (r : R) :
+  erase_lead (monomial i r) = 0 :=
+begin
+  by_cases hr : r = 0,
+  { subst r, simp only [monomial_zero_right, erase_lead_zero] },
+  { rw [erase_lead, nat_degree_monomial _ _ hr, monomial, erase_single] }
+end
+
+@[simp] lemma erase_lead_C (r : R) : erase_lead (C r) = 0 :=
+erase_lead_monomial _ _
+
+@[simp] lemma erase_lead_X : erase_lead (X : polynomial R) = 0 :=
+erase_lead_monomial _ _
+
+@[simp] lemma erase_lead_X_pow (n : ℕ) : erase_lead (X ^ n : polynomial R) = 0 :=
+by rw [X_pow_eq_monomial, erase_lead_monomial]
+
+@[simp] lemma erase_lead_C_mul_X_pow (r : R) (n : ℕ) : erase_lead (C r * X ^ n) = 0 :=
+by rw [C_mul_X_pow_eq_monomial, erase_lead_monomial]
+
+lemma erase_lead_degree_le : (erase_lead f).degree ≤ f.degree :=
+begin
+  rw degree_le_iff_coeff_zero,
+  intros i hi,
+  rw erase_lead_coeff,
+  split_ifs with h, { refl },
+  apply coeff_eq_zero_of_degree_lt hi
+end
+
+lemma erase_lead_nat_degree_le : (erase_lead f).nat_degree ≤ f.nat_degree :=
+nat_degree_le_nat_degree erase_lead_degree_le
+
+lemma erase_lead_nat_degree_lt (f0 : 2 ≤ f.support.card) :
+  (erase_lead f).nat_degree < f.nat_degree :=
+lt_of_le_of_ne erase_lead_nat_degree_le $ ne_nat_degree_of_mem_erase_lead_support $
+  nat_degree_mem_support_of_nonzero $ erase_lead_ne_zero f0
+
+end erase_lead
+
+end polynomial