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"
    by (simp add:F_def)
  finally show ?thesis by simp
qed

definition Pe :: "nat ⇒ nat ⇒ nat list ⇒ bool list option" where
  "Pe p n f = (if p > 1 ∧ f ∈ bounded_degree_polynomials (ring_of (mod_ring p)) n then
    ([0..<n] →e Nbe p) (λi ∈ {..<n}. ring.coeff (ring_of (mod_ring p)) f i) else None)"

lemma poly_encoding:
  "is_encoding (Pe 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. Pe p n f)"
    unfolding Pe_def using a True
    by (intro encoding_compose[where f="([0..<n] →e Nbe p)"] fun_encoding bounded_nat_encoding)
     auto
  thus ?thesis by simp
next
  case False
  hence "is_encoding (λf. Pe p n f)"
    unfolding Pe_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 (Pe 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 (Pe p n x) = (∑ k ← [0..<n]. bit_count (Nbe p (coeff x k)))"
    using assms restrict_extensional
    by (auto intro!:arg_cong[where f="sum_list"] simp add:Pe_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