Theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities

section ‹Cardinalities of Interpolation Polynomials›

text ‹This section establishes the cardinalities of the set of polynomials with a degree bound
interpolating a given set of points.›

theory Interpolation_Polynomial_Cardinalities
  imports Bounded_Degree_Polynomials Lagrange_Interpolation
begin

lemma (in ring) poly_add_coeff:
  assumes "x ∈ carrier (poly_ring R)"
  assumes "y ∈ carrier (poly_ring R)"
  shows "coeff (x ⊕⇘poly_ring R⇙ y) k = coeff x k ⊕ coeff y k"
  by (metis assms univ_poly_carrier polynomial_incl univ_poly_add poly_add_coeff)

lemma (in domain) poly_neg_coeff:
  assumes "x ∈ carrier (poly_ring R)"
  shows "coeff (⊖⇘poly_ring R⇙ x) k = ⊖coeff x k"
proof -
  interpret x:cring "poly_ring R"
    using assms cring_def carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

  have a:"𝟬⇘poly_ring R⇙ = x ⊖⇘poly_ring R⇙ x"
    by (metis x.r_right_minus_eq assms(1))

  have "𝟬 = coeff (𝟬⇘poly_ring R⇙) k" by (simp add:univ_poly_zero)
  also have "... = coeff x k ⊕ coeff (⊖⇘poly_ring R⇙ x) k" using a assms
    by (simp add:a_minus_def poly_add_coeff)
  finally have "𝟬 = coeff x k ⊕ coeff (⊖⇘poly_ring R⇙ x) k" by simp
  thus ?thesis
    by (metis local.minus_minus x.a_inv_closed sum_zero_eq_neg coeff_in_carrier assms)
qed

lemma (in domain) poly_substract_coeff:
  assumes "x ∈ carrier (poly_ring R)"
  assumes "y ∈ carrier (poly_ring R)"
  shows "coeff (x ⊖⇘poly_ring R⇙ y) k = coeff x k ⊖ coeff y k"
proof -
  interpret x:cring "poly_ring R"
    using assms cring_def carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto
  show ?thesis
    using assms by (simp add:a_minus_def poly_add_coeff poly_neg_coeff)
qed

text ‹A polynomial with more zeros than its degree is the zero polynomial.›

lemma (in field) max_roots:
  assumes "p ∈ carrier (poly_ring R)"
  assumes "K ⊆ carrier R"
  assumes "finite K"
  assumes "degree p < card K"
  assumes "⋀x. x ∈ K ⟹ eval p x = 𝟬"
  shows "p = 𝟬⇘poly_ring R⇙"
proof (rule ccontr)
  assume "p ≠ 𝟬⇘poly_ring R⇙"
  hence a:"p ≠ []" by (simp add: univ_poly_zero)
  have "⋀x. count (mset_set K) x ≤ count (roots p) x"
  proof -
    fix x
    show "count (mset_set K) x ≤ count (roots p) x"
    proof (cases "x ∈ K")
      case True
      hence "is_root p x"
        by (meson a assms(2,5) is_ring is_root_def subsetD)
      hence "x ∈ set_mset (roots p)"
        using assms(1) roots_mem_iff_is_root field_def by force
      hence "1 ≤ count (roots p) x" by simp
      moreover have "count (mset_set K) x = 1" using True assms(3) by simp
      ultimately show ?thesis by presburger
    next
      case False
      hence "count (mset_set K) x = 0" by simp
      then show ?thesis by presburger
    qed
  qed
  hence "mset_set K ⊆# roots p"
    by (simp add: subseteq_mset_def)
  hence "card K ≤ size (roots p)"
    by (metis size_mset_mono size_mset_set)
  moreover have "size (roots p) ≤ degree p"
    using a size_roots_le_degree assms by auto
  ultimately show "False" using assms(4)
    by (meson leD less_le_trans)
qed

definition (in ring) split_poly
  where "split_poly K p = (restrict (eval p) K, λk. coeff p (k+card K))"

text ‹To establish the count of the number of polynomials of degree less than
$n$ interpolating a function $f$ on $K$ where $\lvert K \rvert \leq n$, the function
@{term "split_poly K"} establishes a bijection between the polynomials of degree less than
$n$ and the values of the polynomials on $K$ in combination with the coefficients of order
$\lvert K \rvert$ and greater.

For the injectivity: Note that the difference of two polynomials whose coefficients of order
$\lvert K \rvert$ and larger agree must have a degree less than $\lvert K \rvert$ and because
their values agree on $k$ points, it must have $\lvert K \rvert$ zeros and hence is the zero
polynomial.

For the surjectivty: Let $p$ be a polynomial whose coefficients larger than $\lvert K \rvert$ are
chosen, and all other coefficients be $0$. Now it is possible to find a polynomial $q$ interpolating
$f - p$ on $K$ using Lagrange interpolation. Then $p + q$ will interpolate $f$ on $K$ and because
the degree of $q$ is less than $\lvert K \rvert$ its coefficients of order $\lvert K \rvert$ will
be the same as those of $p$.

A tempting question is whether it would be easier to instead establish a bijection between the
polynomials of degree less than $n$ and its values on $K \cup K'$ where $K'$ are arbitrarily chosen
$n-\lvert K \rvert$ points in the field. This approach is indeed easier, however, it fails for
the case where the size of the field is less than $n$.›

lemma (in field) split_poly_inj:
  assumes "finite K"
  assumes "K ⊆ carrier R"
  shows "inj_on (split_poly K) (carrier (poly_ring R))"
proof
  fix x
  fix y
  assume a1:"x ∈ carrier (poly_ring R)"
  assume a2:"y ∈ carrier (poly_ring R)"
  assume a3:"split_poly K x = split_poly K y"

  interpret x:cring "poly_ring R"
    using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

  have x_y_carrier: "x ⊖⇘poly_ring R⇙ y ∈ carrier (poly_ring R)" using a1 a2 by simp
  have "⋀k. coeff x (k+card K) = coeff y (k+card K)"
    using a3 by (simp add:split_poly_def, meson)
  hence "⋀k. coeff (x ⊖⇘poly_ring R⇙ y) (k+card K) = 𝟬"
    using coeff_in_carrier a1 a2 by (simp add:poly_substract_coeff)
  hence "degree (x ⊖⇘poly_ring R⇙ y) < card K ∨ (x ⊖⇘poly_ring R⇙ y) = 𝟬⇘poly_ring R⇙"
    by (metis poly_degree_bound_from_coeff add.commute le_iff_add x_y_carrier)
  moreover have "⋀k. k ∈ K ⟹ eval x k = eval y k"
    using a3 by (simp add:split_poly_def restrict_def, meson)
  hence "⋀k. k ∈ K ⟹ eval x k ⊖ eval y k = 𝟬"
    by (metis eval_in_carrier univ_poly_carrier polynomial_incl a1 assms(2) in_mono r_right_minus_eq)
  hence "⋀k. k ∈ K ⟹ eval (x ⊖⇘poly_ring R⇙ y) k = 𝟬"
    using a1 a2 subsetD[OF assms(2)] carrier_is_subring
    by (simp add: ring_hom_cring.hom_sub[OF eval_cring_hom])
  ultimately have "x ⊖⇘poly_ring R⇙ y = 𝟬⇘poly_ring R⇙"
    using max_roots x_y_carrier assms by blast
  then show "x = y"
    using x.r_right_minus_eq[OF a1 a2] by simp
qed

lemma (in field) split_poly_image:
  assumes "finite K"
  assumes "K ⊆ carrier R"
  shows "split_poly K ` carrier (poly_ring R) ⊇
        (K →⇩E carrier R) × {f. range f ⊆ carrier R ∧ (∃n. ∀k ≥ n. f k = 𝟬⇘R⇙)}"
proof (rule subsetI)
  fix x
  assume a:"x ∈ (K →⇩E carrier R) × {f. range f ⊆ carrier R ∧ (∃(n::nat). ∀k ≥ n. f k = 𝟬)}"
  have a1: "fst x ∈ (K →⇩E carrier R)"
    using a by (simp add:mem_Times_iff)
  obtain n where a2: "snd x ∈ {f. range f ⊆ carrier R ∧ (∀k ≥ n. f k = 𝟬)}"
    using a mem_Times_iff by force
  have a3: "⋀y. snd x y ∈ carrier R" using a2 by blast

  define w where "w = build_poly (λi. if i ≥ card K then (snd x (i - card K)) else 𝟬) (card K + n)"

  have w_carr: "w ∈ carrier (poly_ring R)"
    unfolding w_def by (rule build_poly_poly, simp add:a3)

  have w_eval_range: "⋀x. x ∈ carrier R ⟹ local.eval w x ∈ carrier R"
  proof -
    fix x
    assume w_eval_range_1:"x ∈ carrier R"
    interpret x:ring_hom_cring "poly_ring R" "R" "(λp. eval p x)"
      using eval_cring_hom[OF carrier_is_subring] assms w_eval_range_1 by blast
    show "eval w x ∈ carrier R"
      by (rule x.hom_closed[OF w_carr])
  qed

  interpret r:cring "poly_ring R"
    using carrier_is_subring domain.univ_poly_is_cring domain_axioms by auto

  define y where "y = interpolate K (λk. fst x k ⊖ eval w k)"
  define r where "r = y ⊕⇘poly_ring R⇙ w"

  have x_minus_w_in_carrier: "⋀z. z ∈ K ⟹ fst x z ⊖ eval w z ∈ carrier R"
    using a1 PiE_def Pi_def minus_closed subsetD[OF assms(2)] w_eval_range by auto

  have y_poly: "y ∈ carrier (poly_ring R)" unfolding y_def
    using x_minus_w_in_carrier interpolate_poly[OF assms(1) assms(2)] image_subsetI by force

  have y_degree: "degree y ≤ card K - 1"
    unfolding y_def
    using x_minus_w_in_carrier interpolate_degree[OF assms(1) assms(2)] image_subsetI by force

  have y_len: "length y ≤ card K"
  proof (cases "K={}")
    case True
    then show ?thesis
      by (simp add:y_def interpolate_def univ_poly_zero)
  next
    case False
    then show ?thesis
      by (metis y_degree Suc_le_D assms(1) card_gt_0_iff diff_Suc_1 not_less_eq_eq order.strict_iff_not)
  qed

  have r_poly: "r ∈ carrier (poly_ring R)"
    using r_def y_poly w_carr by simp

  have coeff_r: "⋀k. coeff r (k + card K) = snd x k"
  proof -
    fix k :: nat
    have y_len': "length y ≤ k + card K" using y_len trans_le_add2 by blast
    have "coeff r (k + card K) = coeff y (k + card K) ⊕ coeff w (k+card K)"
      by (simp add:r_def  poly_add_coeff[OF y_poly w_carr])
    also have "... = 𝟬 ⊕ coeff w (k+card K)"
      using coeff_length[OF y_len'] by simp
    also have "... = coeff w (k+card K)"
      using coeff_in_carrier[OF w_carr] by simp
    also have "... = snd x k"
      using a2 by (simp add:w_def build_poly_coeff not_less)
    finally show "coeff r (k + card K) = snd x k" by simp
  qed

  have eval_r: "⋀k. k ∈ K ⟹ eval r k = fst x k"
  proof -
    fix k
    assume b:"k ∈ K"
    interpret s:ring_hom_cring "poly_ring R" "R" "(λp. eval p k)"
      using eval_cring_hom[OF carrier_is_subring] assms b by blast

    have k_carr: "k ∈ carrier R" using assms(2) b by blast
    have fst_x_k_carr: "⋀k. k ∈ K ⟹ fst x k ∈ carrier R"
      using  a1 PiE_def Pi_def by blast
    have "eval r k = eval y k ⊕ eval w k"
      using y_poly w_carr by (simp add:r_def)
    also have "... = fst x k ⊖ local.eval w k ⊕ local.eval w k"
      using assms b x_minus_w_in_carrier
      by (simp add:y_def interpolate_eval[OF _ _ image_subsetI])
    also have "... = fst x k ⊕ (⊖ local.eval w k ⊕ local.eval w k)"
      using fst_x_k_carr[OF b] w_eval_range[OF k_carr]
      by (simp add:a_minus_def a_assoc)
    also have "... = fst x k"
      using fst_x_k_carr[OF b] w_eval_range[OF k_carr]
      by (simp add:a_comm r_neg)
    finally show "eval r k = fst x k" by simp
  qed

  have "r ∈ (carrier (poly_ring R))"
    by (metis r_poly)
  moreover have "⋀y. (if y ∈ K then eval r y else undefined) = fst x y"
    using a1 eval_r PiE_E by auto
  hence "split_poly K r = x"
    by (simp add:split_poly_def prod_eq_iff coeff_r restrict_def)
  ultimately show "x ∈ split_poly K ` (carrier (poly_ring R))"
    by blast
qed

text ‹This is like @{thm [source] card_vimage_inj} but supports @{term "inj_on"} instead.›
lemma card_vimage_inj_on:
  assumes "inj_on f B"
  assumes "A ⊆ f ` B"
  shows "card (f -` A ∩ B) = card A"
proof -
  have "A = f ` (f -` A ∩ B)" using assms(2) by auto
  thus ?thesis using assms card_image
    by (metis inf_le2 inj_on_subset)
qed

lemma inv_subsetI:
  assumes "⋀x. x ∈ A ⟹ f x ∈ B ⟹ x ∈ C"
  shows "f -` B ∩ A ⊆ C"
  using assms by force

text ‹The following establishes the main result of this section: There are $\lvert F \rvert^{n-k}$
polynomials of degree less than $n$ interpolating $k \leq n$ points.›

lemma restrict_eq_imp:
  assumes "restrict f A = restrict g A"
  assumes "x ∈ A"
  shows "f x = g x"
  by (metis restrict_def assms)

theorem (in field) interpolating_polynomials_card:
  assumes "finite K"
  assumes "K ⊆ carrier R"
  assumes "f ` K ⊆ carrier R"
  shows "card {ω ∈ bounded_degree_polynomials R (card K + n). (∀k ∈ K. eval ω k = f k)} = card (carrier R)^n"
    (is "card ?A = ?B")
proof -
  define z where "z = restrict f K"
  define M where "M = {f. range f ⊆ carrier R ∧ (∀k ≥ n. f k = 𝟬)}"

  hence inj_on_bounded: "inj_on (split_poly K) (carrier (poly_ring R))"
    using split_poly_inj[OF assms(1) assms(2)] by blast

  have "?A ⊆ split_poly K -` ({z} × M)"
    unfolding split_poly_def z_def M_def bounded_degree_polynomials_length
    by (rule subsetI, auto intro!:coeff_in_carrier coeff_length)
  moreover have "?A ⊆ carrier (poly_ring R)"
    unfolding bounded_degree_polynomials_length by blast
  ultimately have a:"?A ⊆ split_poly K -` ({z} × M) ∩ carrier (poly_ring R)"
    by blast

  have "⋀x k . (λk. coeff x (k + card K)) ∈ M ⟹ k ≥ n + card K ⟹ coeff x k = 𝟬"
    by (simp add:M_def, metis Nat.le_diff_conv2 Nat.le_imp_diff_is_add add_leD2)
  hence "split_poly K -` ({z} × M) ∩ carrier (poly_ring R) ⊆ bounded_degree_polynomials R (card K + n)"
    unfolding split_poly_def z_def using poly_degree_bound_from_coeff_1 inv_subsetI by force
  moreover have "⋀ω k. ω ∈ split_poly K -` ({z} × M) ∩ carrier (poly_ring R) ⟹ k ∈ K ⟹ eval ω k = f k"
    unfolding split_poly_def z_def using restrict_eq_imp by fastforce
  ultimately have b:"split_poly K -` ({z} × M) ∩ carrier (poly_ring R) ⊆ ?A"
    by blast

  have "z ∈ K →⇩E carrier R"
    unfolding z_def using assms(3) by auto
  moreover have "M ⊆ {f. range f ⊆ carrier R ∧ (∃n. (∀k ≥ n. f k = 𝟬))}"
    unfolding M_def by blast
  ultimately have c:"{z} × M ⊆ split_poly K ` carrier (poly_ring R)"
    using split_poly_image[OF assms(1) assms(2)] by fast

  have "card ?A = card (split_poly K -` ({z} × M) ∩ carrier (poly_ring R))"
    using order_antisym[OF a b] by simp
  also have "... = card ({z} × M)"
    using card_vimage_inj_on[OF inj_on_bounded] c by blast
  also have "... = card (carrier R)^n"
    by (simp add:card_cartesian_product M_def card_mostly_constant_maps)
  finally show ?thesis by simp
qed

text ‹A corollary is the classic result~\<^cite>‹‹Theorem 7.15› in "shoup2009computational"› that there is
exactly one polynomial of degree less than $n$ interpolating $n$ points:›

corollary (in field) interpolating_polynomial_one:
  assumes "finite K"
  assumes "K ⊆ carrier R"
  assumes "f ` K ⊆ carrier R"
  shows "card {ω ∈ bounded_degree_polynomials R (card K). (∀k ∈ K. eval ω k = f k)} = 1"
  using interpolating_polynomials_card[OF assms(1) assms(2) assms(3), where n="0"]
  by simp

text ‹In the case of fields with infinite carriers, it is possible to conclude that there are
infinitely many polynomials of degree less than $n$ interpolating $k < n$ points.›

corollary (in field) interpolating_polynomial_inf:
  assumes "infinite (carrier R)"
  assumes "finite K" "K ⊆ carrier R" "f ` K ⊆ carrier R"
  assumes "n > 0"
  shows "infinite {ω ∈ bounded_degree_polynomials R (card K + n). (∀k ∈ K. eval ω k = f k)}"
    (is "infinite ?A")
proof -
  have "{} ⊂ {ω ∈ bounded_degree_polynomials R (card K). (∀k ∈ K. eval ω k = f k)}"
    using interpolating_polynomial_one[OF assms(2) assms(3) assms(4)] by fastforce
  also have "... ⊆ ?A"
    unfolding bounded_degree_polynomials_def by auto
  finally have a:"?A ≠ {}" by auto

  have "card ?A = card (carrier R)^n"
    using interpolating_polynomials_card[OF assms(2) assms(3) assms(4), where n="n"] by simp
  also have "... = 0"
    using assms(1) assms(5) by simp
  finally have b:"card ?A = 0" by simp

  show ?thesis using a b card_0_eq by blast
qed

text ‹The following is an additional independent result: The evaluation homomorphism is injective
for degree one polynomials.›

lemma  (in field) eval_inj_if_degree_1:
  assumes "p ∈ carrier (poly_ring R)" "degree p = 1"
  shows "inj_on (eval p) (carrier R)"
proof -
  obtain u v where p_def: "p = [u,v]" using assms
    by (cases p, cases "(tl p)", auto)

  have "u ∈ carrier R - {𝟬}" using p_def assms by blast
  moreover have "v ∈ carrier R" using p_def assms by blast
  ultimately show ?thesis by (simp add:p_def field_Units inj_on_def)
qed

end