Theory Formal_Polynomial_Derivatives

section ‹Formal Derivatives\label{sec:pderiv}›

theory Formal_Polynomial_Derivatives
  imports "HOL-Algebra.Polynomial_Divisibility" "Ring_Characteristic"
begin

definition pderiv ("pderivı") where
  "pderivRx = ring.normalize R (
    map (λi. int_embed R i Rring.coeff R x i) (rev [1..<length x]))"

context domain
begin

lemma coeff_range:
  assumes "subring K R"
  assumes "f  carrier (K[X])"
  shows "coeff f i  K"
proof -
  have "coeff f i  set f  {𝟬}"
    using coeff_img(3) by auto
  also have "...  K  {𝟬}"
    using assms(2) univ_poly_carrier polynomial_incl by blast
  also have "...  K"
    using subringE[OF assms(1)] by simp
  finally show ?thesis by simp
qed

lemma pderiv_carr:
  assumes "subring K R"
  assumes "f  carrier (K[X])"
  shows "pderiv f  carrier (K[X])"
proof -
  have "int_embed R i  coeff f i  K" for i
    using coeff_range[OF assms] int_embed_range[OF assms(1)]
    using subringE[OF assms(1)] by simp
  hence "polynomial K (pderiv f)"
    unfolding pderiv_def by (intro normalize_gives_polynomial, auto)
  thus ?thesis
    using univ_poly_carrier by auto
qed

lemma pderiv_coeff:
  assumes "subring K R"
  assumes "f  carrier (K[X])"
  shows "coeff (pderiv f) k = int_embed R (Suc k)  coeff f (Suc k)"
    (is "?lhs = ?rhs")
proof (cases "k + 1  < length f")
  case True
  define j where "j = length f - k - 2"
  define d where
    "d = map (λi. int_embed R i  coeff f i) (rev [1..<length f])"

  have a: "j+1 < length f"
    using True unfolding j_def by simp
  hence b: "j < length [1..<length f]"
    by simp
  have c: "k < length d"
    unfolding d_def using True by simp
  have d: "degree d - k = j"
    unfolding d_def j_def by simp
  have e: "rev [Suc 0..<length f] ! j = length f - 1 - j"
    using b  by (subst rev_nth, auto)
  have f: "length f - j - 1 = k+1"
    unfolding j_def using True by simp

  have "coeff (pderiv f ) k = coeff (normalize d) k"
    unfolding pderiv_def d_def by simp
  also have "... = coeff d k"
    using normalize_coeff by simp
  also have "... = d ! j"
    using c d by (subst coeff_nth, auto)
  also have
    "... = int_embed R (length f - j - 1)  coeff f (length f - j - 1)"
    using b e unfolding d_def by simp
  also have "... = ?rhs"
    using f by simp
  finally show ?thesis by simp
next
  case False
  hence "Suc k  length f"
    by simp
  hence a:"coeff f (Suc k) = 𝟬"
    using coeff_img by blast
  have b:"coeff (pderiv f) k = 𝟬"
    unfolding pderiv_def normalize_coeff[symmetric] using False
    by (intro coeff_length, simp)
  show ?thesis
    using int_embed_range[OF carrier_is_subring] by (simp add:a b)
qed

lemma pderiv_const:
  assumes "degree x = 0"
  shows "pderiv x = 𝟬K[X]⇙"
proof (cases "length x = 0")
  case True
  then show ?thesis by (simp add:univ_poly_zero pderiv_def)
next
  case False
  hence "length x = 1" using assms by linarith
  then obtain y where "x = [y]" by (cases x, auto)
  then show ?thesis by (simp add:univ_poly_zero pderiv_def)
qed

lemma pderiv_var:
  shows "pderiv X = 𝟭K[X]⇙"
  unfolding var_def pderiv_def
  by (simp add:univ_poly_one int_embed_def)

lemma pderiv_zero:
  shows "pderiv 𝟬K[X]= 𝟬K[X]⇙"
  unfolding pderiv_def univ_poly_zero by simp

lemma pderiv_add:
  assumes "subring K R"
  assumes [simp]: "f  carrier (K[X])" "g  carrier (K[X])"
  shows "pderiv (f K[X]g) = pderiv f K[X]pderiv g"
    (is "?lhs = ?rhs")
proof -
  interpret p: ring "(K[X])"
    using univ_poly_is_ring[OF assms(1)] by simp

  let ?n = "(λi. int_embed R i)"

  have a[simp]:"?n k  carrier R" for k
    using int_embed_range[OF carrier_is_subring] by auto
  have b[simp]:"coeff f k  carrier R" if "f  carrier (K[X])" for k f
    using coeff_range[OF assms(1)] that
    using subringE(1)[OF assms(1)] by auto

  have "coeff ?lhs i = coeff ?rhs i" for i
  proof -
    have "coeff ?lhs i = ?n (i+1)  coeff (f K [X]g) (i+1)"
      by (simp add: pderiv_coeff[OF assms(1)])
    also have "... = ?n (i+1)  (coeff f (i+1)  coeff g (i+1))"
      by (subst coeff_add[OF assms], simp)
    also have "... = ?n (i+1)  coeff f (i+1)
       int_embed R (i+1)  coeff g (i+1)"
      by (subst r_distr, simp_all)
    also have "... = coeff (pderiv f) i  coeff (pderiv g) i"
      by (simp add: pderiv_coeff[OF assms(1)])
    also have "... = coeff (pderiv f K [X]pderiv g) i"
      using pderiv_carr[OF assms(1)]
      by (subst coeff_add[OF assms(1)], auto)
    finally show ?thesis by simp
  qed
  hence "coeff ?lhs = coeff ?rhs" by auto
  thus "?lhs = ?rhs"
    using pderiv_carr[OF assms(1)]
    by (subst coeff_iff_polynomial_cond[where K="K"])
      (simp_all add:univ_poly_carrier)+
qed

lemma pderiv_inv:
  assumes "subring K R"
  assumes [simp]: "f  carrier (K[X])"
  shows "pderiv (K[X]f) = K[X]pderiv f" (is "?lhs = ?rhs")
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(1)] by simp

  have "pderiv (K[X]f) = pderiv (K[X]f) K[X]𝟬K[X]⇙"
    using pderiv_carr[OF assms(1)]
    by (subst p.r_zero, simp_all)
  also have "... = pderiv (K[X]f) K[X](pderiv f K[X]pderiv f)"
    using pderiv_carr[OF assms(1)] by simp
  also have "... = pderiv (K[X]f) K[X]pderiv f K[X]pderiv f"
    using pderiv_carr[OF assms(1)]
    unfolding a_minus_def by (simp add:p.a_assoc)
  also have "... = pderiv (K[X]f K[X]f) K[X]pderiv f"
    by (subst pderiv_add[OF assms(1)], simp_all)
  also have "... = pderiv 𝟬K[X]K[X]pderiv f"
    by (subst p.l_neg, simp_all)
  also have "... = 𝟬K[X]K[X]pderiv f"
    by (subst pderiv_zero, simp)
  also have "... = K[X]pderiv f"
    unfolding a_minus_def using pderiv_carr[OF assms(1)]
    by (subst p.l_zero, simp_all)
  finally show "pderiv (K[X]f) = K[X]pderiv f"
    by simp
qed


lemma coeff_mult:
  assumes "subring K R"
  assumes "f  carrier (K[X])" "g  carrier (K[X])"
  shows "coeff (f K[X]g) i =
    ( k  {..i}. (coeff f) k  (coeff g) (i - k))"
proof -
  have a:"set f  carrier R"
    using assms(1,2) univ_poly_carrier
    using subringE(1)[OF assms(1)] polynomial_incl by blast
  have b:"set g  carrier R"
    using assms(1,3) univ_poly_carrier
    using subringE(1)[OF assms(1)] polynomial_incl by blast
  show ?thesis
    unfolding univ_poly_mult poly_mult_coeff[OF a b] by simp
qed

lemma pderiv_mult:
  assumes "subring K R"
  assumes [simp]: "f  carrier (K[X])" "g  carrier (K[X])"
  shows "pderiv (f K[X]g) =
    pderiv f K[X]g K[X]f K[X]pderiv g"
    (is "?lhs = ?rhs")
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(1)] by simp

  let ?n = "(λi. int_embed R i)"

  have a[simp]:"?n k  carrier R" for k
    using int_embed_range[OF carrier_is_subring] by auto
  have b[simp]:"coeff f k  carrier R" if "f  carrier (K[X])" for k f
    using coeff_range[OF assms(1)]
    using subringE(1)[OF assms(1)] that by auto

  have "coeff ?lhs i = coeff ?rhs i" for i
  proof -
    have "coeff ?lhs i = ?n (i+1)  coeff (f K [X]g) (i+1)"
      using assms(2,3) by (simp add: pderiv_coeff[OF assms(1)])
    also have "... = ?n (i+1) 
      (k  {..i+1}. coeff f k  (coeff g (i + 1 - k)))"
      by (subst coeff_mult[OF assms], simp)
    also have "... =
      (k  {..i+1}. ?n (i+1)  (coeff f k  coeff g (i + 1 - k)))"
      by (intro finsum_rdistr, simp_all add:Pi_def)
    also have "... =
      (k  {..i+1}. ?n k  (coeff f k  coeff g (i + 1 - k)) 
      ?n (i+1-k)  (coeff f k  coeff g (i + 1 - k)))"
      using int_embed_add[symmetric] of_nat_diff
      by (intro finsum_cong')
        (simp_all add:l_distr[symmetric] of_nat_diff)
    also have "... =
      (k  {..i+1}. ?n k  coeff f k  coeff g (i + 1 - k) 
      coeff f k  (?n (i+1-k)  coeff g (i + 1 - k)))"
      using Pi_def a b m_assoc m_comm
      by (intro finsum_cong' arg_cong2[where f="(⊕)"], simp_all)
    also have "... =
      (k  {..i+1}. ?n k  coeff f k  coeff g (i+1-k)) 
      (k  {..i+1}. coeff f k  (?n (i+1-k)  coeff g (i+1-k)))"
      by (subst finsum_addf[symmetric], simp_all add:Pi_def)
    also have "... =
      (kinsert 0 {1..i+1}. ?n k  coeff f k  coeff g (i+1-k)) 
      (kinsert (i+1) {..i}. coeff f k  (?n (i+1-k)  coeff g (i+1-k)))"
      using subringE(1)[OF assms(1)]
      by (intro arg_cong2[where f="(⊕)"] finsum_cong')
        (auto simp:set_eq_iff)
    also have "... =
      (k  {1..i+1}. ?n k  coeff f k  coeff g (i+1-k)) 
      (k  {..i}. coeff f k  (?n (i+1-k)  coeff g (i+1-k)))"
      by (subst (1 2) finsum_insert, auto simp add:int_embed_zero)
    also have "... =
      (k  Suc ` {..i}. ?n k  coeff f (k)  coeff g (i+1-k)) 
      (k  {..i}. coeff f k  (?n (i+1-k)  coeff g (i+1-k)))"
      by (intro arg_cong2[where f="(⊕)"] finsum_cong')
        (simp_all add:Pi_def atMost_atLeast0)
    also have "... =
      (k  {..i}. ?n (k+1)  coeff f (k+1)  coeff g (i-k)) 
      (k  {..i}. coeff f k  (?n (i+1-k)  coeff g (i+1-k)))"
      by (subst finsum_reindex, auto)
    also have "... =
      (k  {..i}. coeff (pderiv f) k  coeff g (i-k)) 
      (k  {..i}. coeff f k  coeff (pderiv g) (i-k))"
      using Suc_diff_le
      by (subst (1 2) pderiv_coeff[OF assms(1)])
        (auto intro!: finsum_cong')
    also have "... =
      coeff (pderiv f K[X]g) i  coeff (f K[X]pderiv g) i"
      using pderiv_carr[OF assms(1)]
      by (subst (1 2) coeff_mult[OF assms(1)], auto)
    also have "... = coeff ?rhs i"
      using pderiv_carr[OF assms(1)]
      by (subst coeff_add[OF assms(1)], auto)
    finally show ?thesis by simp
  qed

  hence "coeff ?lhs = coeff ?rhs" by auto
  thus "?lhs = ?rhs"
    using pderiv_carr[OF assms(1)]
    by (subst coeff_iff_polynomial_cond[where K="K"])
     (simp_all add:univ_poly_carrier)
qed

lemma pderiv_pow:
  assumes "n > (0 :: nat)"
  assumes "subring K R"
  assumes [simp]: "f  carrier (K[X])"
  shows "pderiv (f [^]K[X]n) =
    int_embed (K[X]) n K[X]f [^]K[X](n-1) K[X]pderiv f"
    (is "?lhs = ?rhs")
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(2)] by simp

  let ?n = "λn. int_embed (K[X]) n"

  have [simp]: "?n i  carrier (K[X])" for i
    using p.int_embed_range[OF p.carrier_is_subring] by simp

  obtain m where n_def: "n = Suc m" using assms(1) lessE by blast
  have "pderiv (f [^]K[X](m+1)) =
    ?n (m+1) K[X]f [^]K[X]m K[X]pderiv f"
  proof (induction m)
    case 0
    then show ?case
      using pderiv_carr[OF assms(2)] assms(3)
      using p.int_embed_one by simp
  next
    case (Suc m)
    have "pderiv (f [^]K [X](Suc m + 1)) =
      pderiv (f [^]K [X](m+1) K[X]f) "
      by simp
    also have "... =
      pderiv (f [^]K [X](m+1)) K[X]f K[X]f [^]K [X](m+1) K[X]pderiv f"
      using assms(3) by (subst pderiv_mult[OF assms(2)], auto)
    also have "... =
      (?n (m+1) K [X]f [^]K [X]m K [X]pderiv f) K[X]f
      K[X]f [^]K [X](m+1) K[X]pderiv f"
      by (subst Suc(1), simp)
    also have
      "... = ?n (m+1) K[X](f [^]K [X](m+1) K[X]pderiv f)
      K[X]𝟭K [X]K[X](f [^]K [X](m+1) K[X]pderiv f)"
      using assms(3) pderiv_carr[OF assms(2)]
      apply (intro arg_cong2[where f="(⊕K[X])"])
      apply (simp add:p.m_assoc)
       apply (simp add:p.m_comm)
      by simp
    also have
      "... = (?n (m+1) K[X]𝟭K [X]) K [X](f [^]K [X](m+1) K [X]pderiv f)"
      using assms(3) pderiv_carr[OF assms(2)]
      by (subst p.l_distr[symmetric], simp_all)
    also have "... =
      (𝟭K [X]K[X]?n (m+1)) K [X](f [^]K [X](m+1) K [X]pderiv f)"
      using assms(3) pderiv_carr[OF assms(2)]
      by (subst p.a_comm, simp_all)
    also have "... = ?n (1+ Suc m)
      K [X]f [^]K [X](Suc m) K [X]pderiv f"
      using assms(3) pderiv_carr[OF assms(2)] of_nat_add
      apply (subst (2) of_nat_add, subst p.int_embed_add)
      by (simp add:p.m_assoc p.int_embed_one)
    finally show ?case by simp
  qed
  thus "?thesis" using n_def by auto
qed

lemma pderiv_var_pow:
  assumes "n > (0::nat)"
  assumes "subring K R"
  shows "pderiv (X [^]K[X]n) =
    int_embed (K[X]) n K[X]X [^]K[X](n-1)"
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(2)] by simp

  have [simp]: "int_embed (K[X]) i  carrier (K[X])" for i
    using p.int_embed_range[OF p.carrier_is_subring] by simp

  show ?thesis
    using var_closed[OF assms(2)]
    using pderiv_var[where K="K"] pderiv_carr[OF assms(2)]
    by (subst pderiv_pow[OF assms(1,2)], simp_all)
qed

lemma int_embed_consistent_with_poly_of_const:
  assumes "subring K R"
  shows "int_embed (K[X]) m = poly_of_const (int_embed R m)"
proof -
  define K' where "K' = R  carrier := K "
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms] by simp
  interpret d: domain "K'"
    unfolding K'_def
    using assms(1) subdomainI' subdomain_is_domain by simp
  interpret h: ring_hom_ring  "K'" "K[X]" "poly_of_const"
    unfolding K'_def
    using canonical_embedding_ring_hom[OF assms(1)] by simp

  define n where "n=nat (abs m)"

  have a1: "int_embed (K[X]) (int n) = poly_of_const (int_embed K' n)"
  proof (induction n)
    case 0
    then show ?case by (simp add:d.int_embed_zero p.int_embed_zero)
  next
    case (Suc n)
    then show ?case
      using d.int_embed_closed d.int_embed_add d.int_embed_one
      by (simp add:p.int_embed_add p.int_embed_one)
  qed
  also have "... = poly_of_const (int_embed R n)"
    unfolding K'_def using int_embed_consistent[OF assms] by simp
  finally have a:
    "int_embed (K[X]) (int n) = poly_of_const (int_embed R (int n))"
    by simp

  have "int_embed (K[X]) (-(int n)) =
    poly_of_const (int_embed K' (- (int n)))"
    using d.int_embed_closed a1 by (simp add: p.int_embed_inv d.int_embed_inv)
  also have "... = poly_of_const (int_embed R (- (int n)))"
    unfolding K'_def using int_embed_consistent[OF assms] by simp
  finally have b:
    "int_embed (K[X]) (-int n) = poly_of_const (int_embed R (-int n))"
    by simp

  show ?thesis
    using a b n_def by (cases "m  0", simp, simp)
qed

end

end