# Theory Frequency_Moments

```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"
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)))"

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))"