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