feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368)

Author: astrainfinita

src/data/polynomial/derivative.lean

@@ -109,27 +109,25 @@ derivative.to_add_monoid_hom.iterate_map_add _ _ _
   derivative (∑ b in s, f b) = ∑ b in s, derivative (f b) :=
 derivative.map_sum
 
-@[simp] lemma derivative_smul (r : R) (p : R[X]) : derivative (r • p) = r • derivative p :=
-derivative.map_smul _ _
-
-@[simp] lemma iterate_derivative_smul (r : R) (p : R[X]) (k : ℕ) :
-  derivative^[k] (r • p) = r • (derivative^[k] p) :=
+@[simp] lemma derivative_smul {S : Type*} [monoid S]
+  [distrib_mul_action S R] [is_scalar_tower S R R]
+  (s : S) (p : R[X]) : derivative (s • p) = s • derivative p :=
+derivative.map_smul_of_tower s p
+
+@[simp] lemma iterate_derivative_smul {S : Type*} [monoid S]
+  [distrib_mul_action S R] [is_scalar_tower S R R]
+  (s : S) (p : R[X]) (k : ℕ) :
+  derivative^[k] (s • p) = s • (derivative^[k] p) :=
 begin
   induction k with k ih generalizing p,
   { simp, },
   { simp [ih], },
 end
 
-/- We can't use `derivative_mul` here because
-we want to prove this statement also for noncommutative rings.-/
-@[simp]
-lemma derivative_C_mul (a : R) (p : R[X]) : derivative (C a * p) = C a * derivative p :=
-by convert derivative_smul a p; apply C_mul'
-
 @[simp]
 lemma iterate_derivative_C_mul (a : R) (p : R[X]) (k : ℕ) :
   derivative^[k] (C a * p) = C a * (derivative^[k] p) :=
-by convert iterate_derivative_smul a p k; apply C_mul'
+by simp_rw [← smul_eq_C_mul, iterate_derivative_smul]
 
 theorem of_mem_support_derivative {p : R[X]} {n : ℕ} (h : n ∈ p.derivative.support) :
   n + 1 ∈ p.support :=
@@ -197,42 +195,42 @@ begin
   exact hf h2
 end
 
-end semiring
-
-section comm_semiring
-variables [comm_semiring R]
-
-lemma derivative_eval (p : R[X]) (x : R) :
-  p.derivative.eval x = p.sum (λ n a, (a * n)*x^(n-1)) :=
-by simp only [derivative_apply, eval_sum, eval_pow, eval_C, eval_X, eval_nat_cast, eval_mul]
-
 @[simp] lemma derivative_mul {f g : R[X]} :
   derivative (f * g) = derivative f * g + f * derivative g :=
-calc derivative (f * g) = f.sum (λn a, g.sum (λm b, C ((a * b) * (n + m : ℕ)) * X^((n + m) - 1))) :
+calc derivative (f * g) = f.sum (λn a, g.sum (λm b, (n + m) • (C (a * b) * X^((n + m) - 1)))) :
   begin
     rw mul_eq_sum_sum,
     transitivity, exact derivative_sum,
     transitivity, { apply finset.sum_congr rfl, assume x hx, exact derivative_sum },
     apply finset.sum_congr rfl, assume n hn, apply finset.sum_congr rfl, assume m hm,
     transitivity,
     { apply congr_arg, exact monomial_eq_C_mul_X },
-    exact derivative_C_mul_X_pow _ _
+    dsimp, rw [← smul_mul_assoc, smul_C, nsmul_eq_mul'], exact derivative_C_mul_X_pow _ _
   end
   ... = f.sum (λn a, g.sum (λm b,
-      (C (a * n) * X^(n - 1)) * (C b * X^m) + (C a * X^n) * (C (b * m) * X^(m - 1)))) :
+      (n • (C a * X^(n - 1))) * (C b * X^m) + (C a * X^n) * (m • (C b * X^(m - 1))))) :
     sum_congr rfl $ assume n hn, sum_congr rfl $ assume m hm,
-      by simp only [nat.cast_add, mul_add, add_mul, C_add, C_mul];
-      cases n; simp only [nat.succ_sub_succ, pow_zero];
-      cases m; simp only [nat.cast_zero, C_0, nat.succ_sub_succ, zero_mul, mul_zero, nat.add_succ,
-        tsub_zero, pow_zero, pow_add, one_mul, pow_succ, mul_comm, mul_left_comm]
+      by cases n; cases m; simp_rw [add_smul, mul_smul_comm, smul_mul_assoc,
+        X_pow_mul_assoc, ← mul_assoc, ← C_mul, mul_assoc, ← pow_add];
+        simp only [nat.add_succ, nat.succ_add, nat.succ_sub_one, zero_smul, add_comm]
   ... = derivative f * g + f * derivative g :
     begin
       conv { to_rhs, congr,
         { rw [← sum_C_mul_X_eq g] },
         { rw [← sum_C_mul_X_eq f] } },
-      simp only [sum, sum_add_distrib, finset.mul_sum, finset.sum_mul, derivative_apply]
+      simp only [sum, sum_add_distrib, finset.mul_sum, finset.sum_mul, derivative_apply],
+      simp_rw [← smul_mul_assoc, smul_C, nsmul_eq_mul'],
     end
 
+end semiring
+
+section comm_semiring
+variables [comm_semiring R]
+
+lemma derivative_eval (p : R[X]) (x : R) :
+  p.derivative.eval x = p.sum (λ n a, (a * n)*x^(n-1)) :=
+by simp only [derivative_apply, eval_sum, eval_pow, eval_C, eval_X, eval_nat_cast, eval_mul]
+
 theorem derivative_pow_succ (p : R[X]) (n : ℕ) :
   (p ^ (n + 1)).derivative = (n + 1) * (p ^ n) * p.derivative :=
 nat.rec_on n (by rw [pow_one, nat.cast_zero, zero_add, one_mul, pow_zero, one_mul]) $ λ n ih,

src/data/polynomial/iterated_deriv.lean

@@ -49,7 +49,9 @@ begin
   { simp only [iterated_deriv_succ, ih, derivative_add] }
 end
 
-@[simp] lemma iterated_deriv_smul : iterated_deriv (r • p) n = r • iterated_deriv p n :=
+@[simp] lemma iterated_deriv_smul {S : Type*} [monoid S]
+  [distrib_mul_action S R] [is_scalar_tower S R R]
+  (s : S) : iterated_deriv (s • p) n = s • iterated_deriv p n :=
 begin
   induction n with n ih,
   { simp only [iterated_deriv_zero_right] },
@@ -96,120 +98,110 @@ begin
   rw eq1, exact iterated_deriv_C _ _ h,
 end
 
-end semiring
-
-section ring
-variables [ring R] (p q : R[X]) (n : ℕ)
-
-@[simp] lemma iterated_deriv_neg : iterated_deriv (-p) n = - iterated_deriv p n :=
-begin
-  induction n with n ih,
-  { simp only [iterated_deriv_zero_right] },
-  { simp only [iterated_deriv_succ, ih, derivative_neg] }
-end
-
-@[simp] lemma iterated_deriv_sub :
-  iterated_deriv (p - q) n = iterated_deriv p n - iterated_deriv q n :=
-by rw [sub_eq_add_neg, iterated_deriv_add, iterated_deriv_neg, ←sub_eq_add_neg]
-
-
-end ring
-
-section comm_semiring
-variable [comm_semiring R]
-variables (f p q : R[X]) (n k : ℕ)
-
 lemma coeff_iterated_deriv_as_prod_Ico :
-  ∀ m : ℕ, (iterated_deriv f k).coeff m = (∏ i in Ico m.succ (m + k.succ), i) * (f.coeff (m+k)) :=
+  ∀ m : ℕ, (iterated_deriv f k).coeff m = (∏ i in Ico m.succ (m + k.succ), i) • (f.coeff (m+k)) :=
 begin
   induction k with k ih,
-  { simp only [add_zero, forall_const, one_mul, Ico_self, eq_self_iff_true,
+  { simp only [add_zero, forall_const, one_smul, Ico_self, eq_self_iff_true,
       iterated_deriv_zero_right, prod_empty] },
-  { intro m, rw [iterated_deriv_succ, coeff_derivative, ih (m+1), mul_right_comm],
+  { intro m, rw [iterated_deriv_succ, coeff_derivative, ih (m+1), ← nat.cast_add_one,
+      ← nsmul_eq_mul', smul_smul, mul_comm],
     apply congr_arg2,
     { have set_eq : (Ico m.succ (m + k.succ.succ)) = (Ico (m + 1).succ (m + 1 + k.succ)) ∪ {m+1},
-      { rw [union_comm, ←insert_eq, Ico_insert_succ_left, add_succ, add_succ, add_succ _ k,
-            ←succ_eq_add_one, succ_add],
-        rw succ_eq_add_one,
-        linarith },
-      rw [set_eq, prod_union],
-      apply congr_arg2,
-      { refl },
-      { simp only [prod_singleton], norm_cast },
+      { simp_rw [← Ico_succ_singleton, union_comm, succ_eq_add_one, add_comm (k + 1), add_assoc],
+        rw [Ico_union_Ico_eq_Ico]; simp_rw [add_le_add_iff_left, le_add_self], },
+      rw [set_eq, prod_union, prod_singleton],
       { rw [disjoint_singleton_right, mem_Ico],
         exact λ h, (nat.lt_succ_self _).not_le h.1 } },
     { exact congr_arg _ (succ_add m k) } },
 end
 
 lemma coeff_iterated_deriv_as_prod_range :
-  ∀ m : ℕ, (iterated_deriv f k).coeff m = f.coeff (m + k) * (∏ i in range k, ↑(m + k - i)) :=
+  ∀ m : ℕ, (iterated_deriv f k).coeff m = (∏ i in range k, (m + k - i)) • f.coeff (m + k) :=
 begin
   induction k with k ih,
   { simp },
   intro m,
   calc (f.iterated_deriv k.succ).coeff m
-      = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * (m + 1) :
+      = (∏ i in range k, (m + k.succ - i)) • f.coeff (m + k.succ) * (m + 1) :
     by rw [iterated_deriv_succ, coeff_derivative, ih m.succ, succ_add, add_succ]
-  ... = f.coeff (m + k.succ) * (∏ i in range k, ↑(m + k.succ - i)) * ↑(m + 1) :
-    by push_cast
-  ... = f.coeff (m + k.succ) * (∏ i in range k.succ, ↑(m + k.succ - i)) :
-    by rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, succ_sub le_rfl, tsub_self, mul_assoc]
+  ... = ((∏ i in range k, (m + k.succ - i)) * (m + 1)) • f.coeff (m + k.succ) :
+    by rw [← nat.cast_add_one, ← nsmul_eq_mul', smul_smul, mul_comm]
+  ... = (∏ i in range k.succ, (m + k.succ - i)) • f.coeff (m + k.succ) :
+    by rw [prod_range_succ, add_tsub_assoc_of_le k.le_succ, succ_sub le_rfl, tsub_self]
 end
 
 lemma iterated_deriv_eq_zero_of_nat_degree_lt (h : f.nat_degree < n) : iterated_deriv f n = 0 :=
 begin
   ext m,
-  rw [coeff_iterated_deriv_as_prod_range, coeff_zero, coeff_eq_zero_of_nat_degree_lt, zero_mul],
+  rw [coeff_iterated_deriv_as_prod_range, coeff_zero, coeff_eq_zero_of_nat_degree_lt, smul_zero],
   linarith
 end
 
 lemma iterated_deriv_mul :
   iterated_deriv (p * q) n =
   ∑ k in range n.succ,
-    (C (n.choose k : R)) * iterated_deriv p (n - k) * iterated_deriv q k :=
+    n.choose k • (iterated_deriv p (n - k) * iterated_deriv q k) :=
 begin
   induction n with n IH,
   { simp },
 
   calc (p * q).iterated_deriv n.succ
       = (∑ (k : ℕ) in range n.succ,
-           C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv k).derivative :
+          (n.choose k) • (p.iterated_deriv (n - k) * q.iterated_deriv k)).derivative :
     by rw [iterated_deriv_succ, IH]
   ... = ∑ (k : ℕ) in range n.succ,
-          C ↑(n.choose k) * p.iterated_deriv (n - k + 1) * q.iterated_deriv k +
+          (n.choose k) • (p.iterated_deriv (n - k + 1) * q.iterated_deriv k) +
         ∑ (k : ℕ) in range n.succ,
-          C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) :
-    by simp_rw [derivative_sum, derivative_mul, derivative_C, zero_mul, zero_add,
-                iterated_deriv_succ, sum_add_distrib]
+          (n.choose k) • (p.iterated_deriv (n - k) * q.iterated_deriv (k + 1)) :
+    by simp_rw [derivative_sum, derivative_smul, derivative_mul, iterated_deriv_succ, smul_add,
+      sum_add_distrib]
   ... = (∑ (k : ℕ) in range n.succ,
-            C ↑(n.choose k.succ) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) +
-          C ↑1 * p.iterated_deriv n.succ * q.iterated_deriv 0) +
+            (n.choose k.succ) • (p.iterated_deriv (n - k) * q.iterated_deriv (k + 1)) +
+          1 • (p.iterated_deriv n.succ * q.iterated_deriv 0)) +
         ∑ (k : ℕ) in range n.succ,
-          C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) : _
+          (n.choose k) • (p.iterated_deriv (n - k) * q.iterated_deriv (k + 1)) : _
   ... = ∑ (k : ℕ) in range n.succ,
-          C ↑(n.choose k) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) +
+          (n.choose k) • (p.iterated_deriv (n - k) * q.iterated_deriv (k + 1)) +
         ∑ (k : ℕ) in range n.succ,
-            C ↑(n.choose k.succ) * p.iterated_deriv (n - k) * q.iterated_deriv (k + 1) +
-        C ↑1 * p.iterated_deriv n.succ * q.iterated_deriv 0 :
-    by ring
+            (n.choose k.succ) • (p.iterated_deriv (n - k) * q.iterated_deriv (k + 1)) +
+        1 • (p.iterated_deriv n.succ * q.iterated_deriv 0) :
+    by rw [add_comm, add_assoc]
   ... = ∑ (i : ℕ) in range n.succ,
-          C ↑((n+1).choose (i+1)) * p.iterated_deriv (n + 1 - (i+1)) * q.iterated_deriv (i+1) +
-        C ↑1 * p.iterated_deriv n.succ * q.iterated_deriv 0 :
-    by simp_rw [choose_succ_succ, succ_sub_succ, cast_add, C.map_add, add_mul, sum_add_distrib]
+          ((n+1).choose (i+1)) • (p.iterated_deriv (n + 1 - (i+1)) * q.iterated_deriv (i+1)) +
+        1 • (p.iterated_deriv n.succ * q.iterated_deriv 0) :
+    by simp_rw [choose_succ_succ, succ_sub_succ, add_smul, sum_add_distrib]
   ... = ∑ (k : ℕ) in range n.succ.succ,
-          C ↑(n.succ.choose k) * p.iterated_deriv (n.succ - k) * q.iterated_deriv k :
+          (n.succ.choose k) • (p.iterated_deriv (n.succ - k) * q.iterated_deriv k) :
     by rw [sum_range_succ' _ n.succ, choose_zero_right, tsub_zero],
 
   congr,
   refine (sum_range_succ' _ _).trans (congr_arg2 (+) _ _),
-  { rw [sum_range_succ, nat.choose_succ_self, cast_zero, C.map_zero, zero_mul, zero_mul, add_zero],
+  { rw [sum_range_succ, nat.choose_succ_self, zero_smul, add_zero],
     refine sum_congr rfl (λ k hk, _),
     rw mem_range at hk,
     congr,
     rw [tsub_add_eq_add_tsub (nat.succ_le_of_lt hk), nat.succ_sub_succ] },
   { rw [choose_zero_right, tsub_zero] },
 end
 
-end comm_semiring
+end semiring
+
+section ring
+variables [ring R] (p q : R[X]) (n : ℕ)
+
+@[simp] lemma iterated_deriv_neg : iterated_deriv (-p) n = - iterated_deriv p n :=
+begin
+  induction n with n ih,
+  { simp only [iterated_deriv_zero_right] },
+  { simp only [iterated_deriv_succ, ih, derivative_neg] }
+end
+
+@[simp] lemma iterated_deriv_sub :
+  iterated_deriv (p - q) n = iterated_deriv p n - iterated_deriv q n :=
+by rw [sub_eq_add_neg, iterated_deriv_add, iterated_deriv_neg, ←sub_eq_add_neg]
+
+
+end ring
 
 end polynomial