section "Frequency Moments" theory Frequency_Moments imports Frequency_Moments_Preliminary_Results Finite_Fields.Finite_Fields_Mod_Ring_Code Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities begin text ‹This section contains a definition of the frequency moments of a stream and a few general results about frequency moments..› definition F where "F k xs = (∑ x ∈ set xs. (rat_of_nat (count_list xs x)^k))" lemma F_ge_0: "F k as ≥ 0" unfolding F_def by (rule sum_nonneg, simp) lemma F_gr_0: assumes "as ≠ []" shows "F k as > 0" proof - have "rat_of_nat 1 ≤ rat_of_nat (card (set as))" using assms card_0_eq[where A="set as"] by (intro of_nat_mono) (metis List.finite_set One_nat_def Suc_leI neq0_conv set_empty) also have "... = (∑x∈set as. 1)" by simp also have "... ≤ (∑x∈set as. rat_of_nat (count_list as x) ^ k)" by (intro sum_mono one_le_power) (metis count_list_gr_1 of_nat_1 of_nat_le_iff) also have "... ≤ F k as" by (simp add:F_def) finally show ?thesis by simp qed definition P⇩_{e}:: "nat ⇒ nat ⇒ nat list ⇒ bool list option" where "P⇩_{e}p n f = (if p > 1 ∧ f ∈ bounded_degree_polynomials (ring_of (mod_ring p)) n then ([0..<n] →⇩_{e}Nb⇩_{e}p) (λi ∈ {..<n}. ring.coeff (ring_of (mod_ring p)) f i) else None)" lemma poly_encoding: "is_encoding (P⇩_{e}p n)" proof (cases "p > 1") case True interpret cring "ring_of (mod_ring p)" using mod_ring_is_cring True by blast have a:"inj_on (λx. (λi∈{..<n}. coeff x i)) (bounded_degree_polynomials (ring_of (mod_ring p)) n)" proof (rule inj_onI) fix x y assume b:"x ∈ bounded_degree_polynomials (ring_of (mod_ring p)) n" assume c:"y ∈ bounded_degree_polynomials (ring_of (mod_ring p)) n" assume d:"restrict (coeff x) {..<n} = restrict (coeff y) {..<n}" have "coeff x i = coeff y i" for i proof (cases "i < n") case True then show ?thesis by (metis lessThan_iff restrict_apply d) next case False hence e: "i ≥ n" by linarith have "coeff x i = 𝟬⇘ring_of (mod_ring p)⇙" using b e by (subst coeff_length, auto simp:bounded_degree_polynomials_length) also have "... = coeff y i" using c e by (subst coeff_length, auto simp:bounded_degree_polynomials_length) finally show ?thesis by simp qed then show "x = y" using b c univ_poly_carrier by (subst coeff_iff_polynomial_cond) (auto simp:bounded_degree_polynomials_length) qed have "is_encoding (λf. P⇩_{e}p n f)" unfolding P⇩_{e}_def using a True by (intro encoding_compose[where f="([0..<n] →⇩_{e}Nb⇩_{e}p)"] fun_encoding bounded_nat_encoding) auto thus ?thesis by simp next case False hence "is_encoding (λf. P⇩_{e}p n f)" unfolding P⇩_{e}_def using encoding_triv by simp then show ?thesis by simp qed lemma bounded_degree_polynomial_bit_count: assumes "p > 1" assumes "x ∈ bounded_degree_polynomials (ring_of (mod_ring p)) n" shows "bit_count (P⇩_{e}p n x) ≤ ereal (real n * (log 2 p + 1))" proof - interpret cring "ring_of (mod_ring p)" using mod_ring_is_cring assms by blast have a: "x ∈ carrier (poly_ring (ring_of (mod_ring p)))" using assms(2) by (simp add:bounded_degree_polynomials_def) have "real_of_int ⌊log 2 (p-1)⌋+1 ≤ log 2 (p-1) + 1" using floor_eq_iff by (intro add_mono, auto) also have "... ≤ log 2 p + 1" using assms by (intro add_mono, auto) finally have b: "⌊log 2 (p-1)⌋+1 ≤ log 2 p + 1" by simp have "bit_count (P⇩_{e}p n x) = (∑ k ← [0..<n]. bit_count (Nb⇩_{e}p (coeff x k)))" using assms restrict_extensional by (auto intro!:arg_cong[where f="sum_list"] simp add:P⇩_{e}_def fun_bit_count lessThan_atLeast0) also have "... = (∑ k ← [0..<n]. ereal (floorlog 2 (p-1)))" using coeff_in_carrier[OF a] mod_ring_carr by (subst bounded_nat_bit_count_2, auto) also have "... = n * ereal (floorlog 2 (p-1))" by (simp add: sum_list_triv) also have "... = n * real_of_int (⌊log 2 (p-1)⌋+1)" using assms(1) by (simp add:floorlog_def) also have "... ≤ ereal (real n * (log 2 p + 1))" by (subst ereal_less_eq, intro mult_left_mono b, auto) finally show ?thesis by simp qed end