diff --git a/metadata/entries/Universal_Hash_Families.toml b/metadata/entries/Universal_Hash_Families.toml
--- a/metadata/entries/Universal_Hash_Families.toml
+++ b/metadata/entries/Universal_Hash_Families.toml
@@ -1,38 +1,39 @@
title = "Universal Hash Families"
date = 2022-02-20
topics = [
"Computer science/Algorithms/Randomized",
]
abstract = """
A k-universal hash family is a probability
space of functions, which have uniform distribution and form
k-wise independent random variables. They can often be used
in place of classic (or cryptographic) hash functions and allow the
rigorous analysis of the performance of randomized algorithms and
data structures that rely on hash functions. In 1981
Wegman and Carter
introduced a generic construction for such families with arbitrary
k using polynomials over a finite field. This entry
contains a formalization of them and establishes the property of
k-universality. To be useful the formalization also provides
an explicit construction of finite fields using the factor ring of
integers modulo a prime. Additionally, some generic results about
independent families are shown that might be of independent interest."""
license = "bsd"
note = ""
[authors]
[authors.karayel]
homepage = "karayel_homepage"
[contributors]
[notify]
karayel = "karayel_email"
[history]
+2024-01-25 = "Added combinator library for pseudorandom objects."
[extra]
[related]
diff --git a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy.thy b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy.thy
--- a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy.thy
+++ b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy.thy
@@ -1,328 +1,327 @@
section \Accuracy with cutoff\label{sec:accuracy}\
text \This section verifies that each of the $l$ estimate have the required accuracy with high
probability assuming as long as the cutoff is below @{term "q_max"}, generalizing the result from
Section~\ref{sec:accuracy_wo_cutoff}.\
theory Distributed_Distinct_Elements_Accuracy
imports
Distributed_Distinct_Elements_Accuracy_Without_Cutoff
Distributed_Distinct_Elements_Cutoff_Level
begin
unbundle intro_cong_syntax
lemma (in semilattice_set) Union:
assumes "finite I" "I \ {}"
assumes "\i. i \ I \ finite (Z i)"
assumes "\i. i \ I \ Z i \ {}"
shows "F (\ (Z ` I)) = F ((\i. (F (Z i))) ` I)"
using assms(1,2,3,4)
proof (induction I rule:finite_ne_induct)
case (singleton x)
then show ?case by simp
next
case (insert x I)
have "F (\ (Z ` insert x I)) = F ((Z x) \ (\ (Z ` I)))"
by simp
also have "... = f (F (Z x)) (F (\ (Z ` I)))"
using insert by (intro union finite_UN_I) auto
also have "... = f (F {F (Z x)}) (F ((\i. F (Z i)) ` I))"
using insert(5,6) by (subst insert(4)) auto
also have "... = F ({F (Z x)} \ (\i. F (Z i)) ` I)"
using insert(1,2) by (intro union[symmetric] finite_imageI) auto
also have "... = F ((\i. F (Z i)) ` insert x I)"
by simp
finally show ?case by simp
qed
text \This is similar to the existing @{thm [source] hom_Max_commute} with the crucial difference
that it works even if the function is a homomorphism between distinct lattices.
An example application is @{term "Max (int ` A) = int (Max A)"}.\
lemma hom_Max_commute':
assumes "finite A" "A \ {}"
assumes "\x y. x \ A \ y \ A \ max (f x) (f y) = f (max x y)"
shows "Max (f ` A) = f (Max A)"
using assms by (induction A rule:finite_ne_induct) auto
context inner_algorithm_fix_A
begin
definition t\<^sub>c
where "t\<^sub>c \ \ = (Max ((\j. \\<^sub>1 \ A \ j + \) ` {..c (* tilde t *)
where "s\<^sub>c \ \ = nat (t\<^sub>c \ \)"
definition p\<^sub>c (* tilde p *)
where "p\<^sub>c \ \ = card {j\ {..\<^sub>1 \ A \ j + \ \ s\<^sub>c \ \}"
definition Y\<^sub>c (* tilde A* *)
where "Y\<^sub>c \ \ = 2 ^ s\<^sub>c \ \ * \_inv (p\<^sub>c \ \)"
lemma s\<^sub>c_eq_s:
- assumes "(f,g,h) \ sample_set \"
+ assumes "(f,g,h) \ sample_pro \"
assumes "\ \ s f"
shows "s\<^sub>c (f,g,h) \ = s f"
proof -
have "int (Max (f ` A)) - int b_exp + 9 \ int (Max (f ` A)) - 26 + 9"
using b_exp_ge_26 by (intro add_mono diff_left_mono) auto
also have "... \ int (Max (f ` A))" by simp
finally have 1:"int (Max (f ` A)) - int b_exp + 9 \ int (Max (f ` A))"
by simp
have "\ \ int (s f)" using assms(2) by simp
also have "... = max 0 (t f)"
unfolding s_def by simp
also have "... \ max 0 (int (Max (f ` A)))"
unfolding t_def using 1 by simp
also have "... = int (Max (f ` A))"
by simp
finally have "\ \ int (Max (f ` A))"
by simp
hence 0: "int \ - 1 \ int (Max (f ` A))"
by simp
- have c:"h \ sample_set (\ k (C\<^sub>7 * b\<^sup>2) [b]\<^sub>S)"
+ have c:"h \ sample_pro (\ k (C\<^sub>7 * b\<^sup>2) (\ b))"
using assms(1) sample_set_\ by auto
hence h_range: "h x < b" for x
using h_range_1 by simp
have "(MAX j\{..\<^sub>1 (f, g, h) A \ j + int \) =
(MAX x\{.. A \ h (g a) = x} \ {-1} \ {int \ -1}))"
using fin_f[OF assms(1)] by (simp add:max_add_distrib_left max.commute \\<^sub>1_def)
also have "... = Max (\x A \ h (g a) = x} \ {- 1} \ {int \ - 1})"
using fin_f[OF assms(1)] b_ne by (intro Max.Union[symmetric]) auto
also have "... = Max ({int (f a) |a. a \ A} \ {- 1, int \ - 1})"
using h_range by (intro arg_cong[where f="Max"]) auto
also have "... = max (Max (int ` f ` A)) (int \ - 1)"
using A_nonempty fin_A unfolding Setcompr_eq_image image_image
by (subst Max.union) auto
also have "... = max (int (Max (f ` A))) (int \ - 1)"
using fin_A A_nonempty by (subst hom_Max_commute') auto
also have "... = int (Max (f ` A))"
by (intro max_absorb1 0)
finally have "(MAX j\{..\<^sub>1 (f, g, h) A \ j + int \) = Max (f ` A)" by simp
thus ?thesis
unfolding s\<^sub>c_def t\<^sub>c_def s_def t_def by simp
qed
lemma p\<^sub>c_eq_p:
- assumes "(f,g,h) \ sample_set \"
+ assumes "(f,g,h) \ sample_pro \"
assumes "\ \ s f"
shows "p\<^sub>c (f,g,h) \ = p (f,g,h)"
proof -
have "{j \ {.. max (\\<^sub>0 (f, g, h) A j) (int \ - 1)} =
{j \ {.. max (\\<^sub>0 (f, g, h) A j) (- 1)}"
using assms(2) unfolding le_max_iff_disj by simp
thus ?thesis
unfolding p\<^sub>c_def p_def s\<^sub>c_eq_s[OF assms]
by (simp add:max_add_distrib_left \\<^sub>1_def del:\\<^sub>0.simps)
qed
lemma Y\<^sub>c_eq_Y:
- assumes "(f,g,h) \ sample_set \"
+ assumes "(f,g,h) \ sample_pro \"
assumes "\ \ s f"
shows "Y\<^sub>c (f,g,h) \ = Y (f,g,h)"
unfolding Y\<^sub>c_def Y_def s\<^sub>c_eq_s[OF assms] p\<^sub>c_eq_p[OF assms] by simp
lemma accuracy_single: "measure \ {\. \\ \ q_max. \Y\<^sub>c \ \ - real X\ > \ * X} \ 1/2^4"
(is "?L \ ?R")
proof -
have "measure \ {\. \\ \ q_max. \Y\<^sub>c \ \ - real X\ > \ * real X} \
measure \ {(f,g,h). \Y (f,g,h) - real X\ > \ * real X \ s f < q_max}"
proof (rule pmf_mono)
fix \
assume a:"\ \ {\. \\\q_max. \ * real X < \Y\<^sub>c \ \ - real X\}"
- assume d:"\ \ set_pmf (sample_pmf \)"
+ assume d:"\ \ set_pmf (sample_pro \)"
obtain \ where b:"\ \ q_max" and c:" \ * real X < \Y\<^sub>c \ \ - real X\"
using a by auto
obtain f g h where \_def: "\ = (f,g,h)" by (metis prod_cases3)
- hence e:"(f,g,h) \ sample_set \"
- using d unfolding sample_space_alt[OF sample_space_\] by simp
+ hence e:"(f,g,h) \ sample_pro \" using d by simp
show "\ \ {(f, g, h). \ * real X < \Y (f, g, h) - real X\ \ s f < q_max}"
proof (cases "s f \ q_max")
case True
hence f:"\ \ s f" using b by simp
have "\ * real X < \Y \ - real X\"
using Y\<^sub>c_eq_Y[OF e f] c unfolding \_def by simp
then show ?thesis unfolding \_def by simp
next
case False
then show ?thesis unfolding \_def by simp
qed
qed
also have "... \ 1/2^4"
using accuracy_without_cutoff by simp
finally show ?thesis by simp
qed
lemma estimate1_eq:
assumes "j < l"
shows "estimate1 (\\<^sub>2 \ A \, \) j = Y\<^sub>c (\ j) \" (is "?L = ?R")
proof -
define t where "t = max 0 (Max ((\\<^sub>2 \ A \ j) ` {.. - \log 2 b\ + 9)"
define p where "p = card { k. k \ {.. (\\<^sub>2 \ A \ j k) + \ \ t }"
have 0: "int (nat x) = max 0 x" for x
by simp
have 1: "\log 2 b\ = b_exp"
unfolding b_def by simp
have "b > 0"
using b_min by simp
hence 2: " {.. {}" by auto
have "t = int (nat (Max ((\\<^sub>2 \ A \ j) ` {.. - b_exp + 9))"
unfolding t_def 0 1 by (rule refl)
also have "... = int (nat (Max ((\x. x + \) ` (\\<^sub>2 \ A \ j) ` {..\<^sub>1 int,\\<^sub>1 nat,\\<^sub>2(+),\\<^sub>2(-)]" more:hom_Max_commute) (simp_all add:2)
also have "... = int (s\<^sub>c (\ j) \)"
using assms
unfolding s\<^sub>c_def t\<^sub>c_def \\<^sub>2_def image_image by simp
finally have 3:"t = int (s\<^sub>c (\ j) \)"
by simp
have 4: "p = p\<^sub>c (\ j) \"
using assms unfolding p_def p\<^sub>c_def 3 \\<^sub>2_def by simp
have "?L = 2 powr t * ln (1-p/b) / ln(1-1/b)"
unfolding estimate1.simps \_def \\<^sub>3_def
by (simp only:t_def p_def Let_def)
also have "... = 2 powr (s\<^sub>c (\