section ‹Bounded Degree Polynomials› text ‹This section contains a definition for the set of polynomials with a degree bound and establishes its cardinality.› theory Bounded_Degree_Polynomials imports "HOL-Algebra.Polynomial_Divisibility" begin lemma (in ring) coeff_in_carrier: "p ∈ carrier (poly_ring R) ⟹ coeff p i ∈ carrier R" using poly_coeff_in_carrier carrier_is_subring by (simp add: univ_poly_carrier) definition bounded_degree_polynomials where "bounded_degree_polynomials F n = {x. x ∈ carrier (poly_ring F) ∧ (degree x < n ∨ x = [])}" text ‹Note: The definition for @{term "bounded_degree_polynomials"} includes the zero polynomial in @{term "bounded_degree_polynomials F 0"}. The reason for this adjustment is that, contrary to definition in HOL Algebra, most authors set the degree of the zero polynomial to $-\infty$~\<^cite>‹‹\textsection 7.2.2› in "shoup2009computational"›. That definition make some identities, such as $\mathrm{deg}(f g) = \mathrm{deg}\, f + \mathrm{deg}\, g$ for polynomials $f$ and $g$ unconditionally true. In particular, it prevents an unnecessary corner case in the statement of the results established in this entry.› lemma bounded_degree_polynomials_length: "bounded_degree_polynomials F n = {x. x ∈ carrier (poly_ring F) ∧ length x ≤ n}" unfolding bounded_degree_polynomials_def using leI order_less_le_trans by fastforce lemma (in ring) fin_degree_bounded: assumes "finite (carrier R)" shows "finite (bounded_degree_polynomials R n)" proof - have "bounded_degree_polynomials R n ⊆ {p. set p ⊆ carrier R ∧ length p ≤ n}" unfolding bounded_degree_polynomials_length using assms polynomial_incl univ_poly_carrier by blast thus ?thesis using assms finite_lists_length_le finite_subset by fast qed lemma (in ring) non_empty_bounded_degree_polynomials: "bounded_degree_polynomials R k ≠ {}" proof - have "𝟬⇘poly_ring R⇙ ∈ bounded_degree_polynomials R k" by (simp add: bounded_degree_polynomials_def univ_poly_zero univ_poly_zero_closed) thus ?thesis by auto qed lemma in_image_by_witness: assumes "⋀x. x ∈ A ⟹ g x ∈ B ∧ f (g x) = x" shows "A ⊆ f ` B" by (metis assms image_eqI subsetI) lemma card_mostly_constant_maps: assumes "y ∈ B" shows "card {f. range f ⊆ B ∧ (∀x. x ≥ n ⟶ f x = y)} = card B ^ n" (is "card ?A = ?B") proof - define f where "f = (λf k. if k < n then f k else y)" have a:"?A ⊆ (f ` ({0..<n} →⇩_{E}B))" unfolding f_def by (rule in_image_by_witness[where g="λf. restrict f {0..<n}"], auto) have b:"(f ` ({0..<n} →⇩_{E}B)) ⊆ ?A" using f_def assms by auto have c: "inj_on f ({0..<n} →⇩_{E}B)" by (rule inj_onI, metis PiE_E atLeastLessThan_iff ext f_def) have "card ?A = card (f ` ({0..<n} →⇩_{E}B))" using a b by auto also have "... = card ({0..<n} →⇩_{E}B)" by (metis c card_image) also have "... = card B ^ n" by (simp add: card_PiE[OF finite_atLeastLessThan]) finally show ?thesis by simp qed definition (in ring) build_poly where "build_poly f n = normalize (rev (map f [0..<n]))" lemma (in ring) poly_degree_bound_from_coeff: assumes "x ∈ carrier (poly_ring R)" assumes "⋀k. k ≥ n ⟹ coeff x k = 𝟬" shows "degree x < n ∨ x = 𝟬⇘poly_ring R⇙" proof (rule ccontr) assume a:"¬(degree x < n ∨ x = 𝟬⇘poly_ring R⇙)" hence b:"lead_coeff x ≠ 𝟬⇘R⇙" by (metis assms(1) polynomial_def univ_poly_carrier univ_poly_zero) hence "coeff x (degree x) ≠ 𝟬" by (metis a lead_coeff_simp univ_poly_zero) moreover have "degree x ≥ n" by (meson a not_le) ultimately show "False" using assms(2) by blast qed lemma (in ring) poly_degree_bound_from_coeff_1: assumes "x ∈ carrier (poly_ring R)" assumes "⋀k. k ≥ n ⟹ coeff x k = 𝟬" shows "x ∈ bounded_degree_polynomials R n" using poly_degree_bound_from_coeff[OF assms] by (simp add:bounded_degree_polynomials_def univ_poly_zero assms) lemma (in ring) length_build_poly: "length (build_poly f n) ≤ n" by (metis length_map build_poly_def normalize_length_le length_rev length_upt less_imp_diff_less linorder_not_less) lemma (in ring) build_poly_degree: "degree (build_poly f n) ≤ n-1" using length_build_poly diff_le_mono by presburger lemma (in ring) build_poly_poly: assumes "⋀i. i < n ⟹ f i ∈ carrier R" shows "build_poly f n ∈ carrier (poly_ring R)" unfolding build_poly_def univ_poly_carrier[symmetric] by (rule normalize_gives_polynomial, simp add:image_subset_iff Ball_def assms) lemma (in ring) build_poly_coeff: "coeff (build_poly f n) i = (if i < n then f i else 𝟬)" proof - show "coeff (build_poly f n) i = (if i < n then f i else 𝟬)" unfolding build_poly_def normalize_coeff[symmetric] by (cases "i < n", (simp add:coeff_nth rev_nth coeff_length)+) qed lemma (in ring) build_poly_bounded: assumes "⋀k. k < n ⟹ f k ∈ carrier R" shows "build_poly f n ∈ bounded_degree_polynomials R n" unfolding bounded_degree_polynomials_length using build_poly_poly[OF assms] length_build_poly by auto text ‹The following establishes the total number of polynomials with a degree less than $n$. Unlike the results in the following sections, it is already possible to establish this property for polynomials with coefficients in a ring.› lemma (in ring) bounded_degree_polynomials_card: "card (bounded_degree_polynomials R n) = card (carrier R) ^ n" proof - have a:"coeff ` bounded_degree_polynomials R n ⊆ {f. range f ⊆ (carrier R) ∧ (∀k ≥ n. f k = 𝟬)}" by (rule image_subsetI, auto simp add:bounded_degree_polynomials_def coeff_length coeff_in_carrier) have b:"{f. range f ⊆ (carrier R) ∧ (∀k ≥ n. f k = 𝟬)} ⊆ coeff ` bounded_degree_polynomials R n" apply (rule in_image_by_witness[where g="λx. build_poly x n"]) by (auto simp add:build_poly_coeff intro:build_poly_bounded) have "inj_on coeff (carrier (poly_ring R))" by (rule inj_onI, simp add: coeff_iff_polynomial_cond univ_poly_carrier) hence coeff_inj: "inj_on coeff (bounded_degree_polynomials R n)" using inj_on_subset bounded_degree_polynomials_def by blast have "card ( bounded_degree_polynomials R n) = card (coeff ` bounded_degree_polynomials R n)" using coeff_inj card_image[symmetric] by blast also have "... = card {f. range f ⊆ (carrier R) ∧ (∀k ≥ n. f k = 𝟬)}" by (rule arg_cong[where f="card"], rule order_antisym[OF a b]) also have "... = card (carrier R)^n" by (rule card_mostly_constant_maps, simp) finally show ?thesis by simp qed end