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,328 @@ 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 "\ \ 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)" 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 "\ \ 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 "\ \ 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" +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}" + 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 a:"\ \ {\. \\\q_max. \ * real X < \Y\<^sub>c \ \ - real X\}" assume d:"\ \ set_pmf (sample_pmf \)" - obtain \ where b:"\ \ q_max" and c:" \ * real X < \Y\<^sub>c \ \ - real X\" + 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 - show "\ \ {(f, g, h). \ * real X < \Y (f, g, h) - real X\ \ s f < q_max}" + 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\" + 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 (\ j) \) * \_inv p" unfolding 3 \_inv_def by (simp) also have "... = ?R" unfolding Y\<^sub>c_def 3 4 by (simp add:powr_realpow) finally show ?thesis by blast qed lemma estimate_result_1: - "measure \ {\. (\\\q_max. \*X < \estimate (\\<^sub>2 \ A \,\)-X\) } \ \/2" (is "?L \ ?R") + "measure \ {\. (\\\q_max. \*X < \estimate (\\<^sub>2 \ A \,\)-X\) } \ \/2" (is "?L \ ?R") proof - - define I :: "real set" where "I = {x. \x - real X\ \ \*X}" + define I :: "real set" where "I = {x. \x - real X\ \ \*X}" define \ where "\ = measure \ {\. \\\q_max. Y\<^sub>c \ \\I}" have int_I: "interval I" unfolding interval_def I_def by auto - have "\ = measure \ {\. \\ \ q_max. \Y\<^sub>c \ \ - real X\ > \ * X}" + have "\ = measure \ {\. \\ \ q_max. \Y\<^sub>c \ \ - real X\ > \ * X}" unfolding \_def I_def by (simp add:not_le) also have "... \ 1 / 2 ^ 4" by (intro accuracy_single) also have "... = 1/ 16" by simp finally have 1:"\ \ 1 / 16" by simp have "(\ + \) \ 1/16 + 1/16" unfolding \_def by (intro add_mono 1) auto also have "... \ 1/8" by simp finally have 2:"(\ + \) \ 1/8" by simp hence 0: "(\ + \) \ 1/2" by simp have "\ \ 0" unfolding \_def by simp hence 3: "\ + \ > 0" by (intro add_nonneg_pos \_gt_0) - have "?L = measure \ {\. (\\\q_max. \*X < \median l (estimate1 (\\<^sub>2 \ A \,\))-X\) }" + have "?L = measure \ {\. (\\\q_max. \*X < \median l (estimate1 (\\<^sub>2 \ A \,\))-X\) }" by simp also have "... = measure \ {\. (\\\q_max. median l (estimate1 (\\<^sub>2 \ A \,\)) \ I)}" unfolding I_def by (intro measure_pmf_cong) auto also have "... \ measure \ {\. real(card{i\{..\\q_max. Y\<^sub>c (\ i) \\I)})\ real l/2}" proof (rule pmf_mono) fix \ assume "\ \ set_pmf \" "\ \ {\. \\\q_max. median l (estimate1 (\\<^sub>2 \ A \, \)) \ I}" then obtain \ where \_def: "median l (estimate1 (\\<^sub>2 \ A \, \)) \ I" "\\q_max" by auto have "real l = 2 * real l - real l" by simp also have "... \ 2 * real l - 2 * card {i. i < l \ estimate1 (\\<^sub>2 \ A \, \) i \ I}" using \_def median_est[OF int_I, where n="l"] not_less by (intro diff_left_mono Nat.of_nat_mono) (auto simp del:estimate1.simps) also have "... = 2 * (real (card {.. estimate1 (\\<^sub>2 \ A \, \) i \ I})" by (simp del:estimate1.simps) also have "... = 2 * real (card {.. estimate1 (\\<^sub>2 \ A \, \) i \ I})" by (intro_cong "[\\<^sub>2 (*)]" more:of_nat_diff[symmetric] card_mono) (auto simp del:estimate1.simps) also have "... = 2 * real (card ({.. estimate1 (\\<^sub>2 \ A \, \) i \ I}))" by (intro_cong "[\\<^sub>2 (*), \\<^sub>1 of_nat]" more:card_Diff_subset[symmetric]) (auto simp del:estimate1.simps) also have "... = 2 * real (card {i\{..\<^sub>2 \ A \, \) i \ I})" by (intro_cong "[\\<^sub>2 (*), \\<^sub>1 of_nat, \\<^sub>1 card]") (auto simp del:estimate1.simps) also have "... = 2 * real (card {i \ {..c (\ i) \ \ I})" using estimate1_eq by (intro_cong "[\\<^sub>2 (*), \\<^sub>1 of_nat, \\<^sub>1 card]" more:restr_Collect_cong) auto also have "... \ 2 * real (card {i \ {..\\q_max. Y\<^sub>c (\ i) \ \ I)})" using \_def(2) by (intro mult_left_mono Nat.of_nat_mono card_mono) auto finally have "real l \ 2 * real (card {i \ {..\\q_max. Y\<^sub>c (\ i) \ \ I)})" by simp thus "\ \ {\. real l/2 \ real (card {i \ {..\\q_max. Y\<^sub>c (\ i) \ \ I})}" by simp qed also have "... = measure \ {\. real (card{i\{..\\q_max. Y\<^sub>c (\ i) \\I)}) \ (1/2)*real l}" unfolding sample_pmf_alt[OF \.sample_space] p_def by simp also have "... \ exp (- real l * ((1/2) * ln (1 / (\ + \)) - 2 * exp (- 1)))" using 0 unfolding \_def by (intro \.tail_bound l_gt_0 \_gt_0) auto also have "... = exp (- (real l * ((1/2) * ln (1 / (\ + \)) - 2 * exp (- 1))))" by simp also have "... \ exp (- (real l * ((1/2) * ln 8 - 2 * exp (- 1))))" using 2 3 l_gt_0 by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le mult_left_mono diff_mono) (auto simp add:divide_simps) also have "... \ exp (- (real l * (1/4)))" by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le mult_left_mono of_nat_0_le_iff) (approximation 5) - also have "... \ exp (- (C\<^sub>6 * ln (2/ \)*(1/4)))" + also have "... \ exp (- (C\<^sub>6 * ln (2/ \)*(1/4)))" by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le mult_right_mono l_lbound) auto - also have "... = exp ( - ln (2/ \))" + also have "... = exp ( - ln (2/ \))" unfolding C\<^sub>6_def by simp also have "... = ?R" - using \_gt_0 by (subst ln_inverse[symmetric]) auto + using \_gt_0 by (subst ln_inverse[symmetric]) auto finally show ?thesis by simp qed theorem estimate_result: - "measure \ {\. \estimate (\ \ A)- X\ > \ * X} \ \" + "measure \ {\. \estimate (\ \ A)- X\ > \ * X} \ \" (is "?L \ ?R") proof - let ?P = "measure \" - have "?L \ ?P {\. (\\\q_max. \*real X<\estimate (\\<^sub>2 \ A \, \)-real X\)\q \ A> q_max}" + have "?L \ ?P {\. (\\\q_max. \*real X<\estimate (\\<^sub>2 \ A \, \)-real X\)\q \ A> q_max}" unfolding \_def \\<^sub>3_def not_le[symmetric] by (intro pmf_mono) auto - also have "...\ ?P {\. (\\\q_max. \*real X<\estimate (\\<^sub>2 \ A \,\)-X\)} + ?P {\. q \ A> q_max}" + also have "...\ ?P {\. (\\\q_max. \*real X<\estimate (\\<^sub>2 \ A \,\)-X\)} + ?P {\. q \ A> q_max}" by (intro pmf_add) auto - also have "...\ \/2 + \/2" + also have "...\ \/2 + \/2" by (intro add_mono cutoff_level estimate_result_1) - also have "... = \" + also have "... = \" by simp finally show ?thesis by simp qed end lemma (in inner_algorithm) estimate_result: assumes "A \ {.. {}" - shows "measure \ {\. \estimate (\ \ A)- real (card A)\ > \ * real (card A)} \ \" (is "?L \ ?R") + shows "measure \ {\. \estimate (\ \ A)- real (card A)\ > \ * real (card A)} \ \" (is "?L \ ?R") proof - interpret inner_algorithm_fix_A using assms by unfold_locales auto - have "?L = measure \ {\. \estimate (\ \ A)- X\ > \ * X}" + have "?L = measure \ {\. \estimate (\ \ A)- X\ > \ * X}" unfolding X_def by simp also have "... \ ?R" by (intro estimate_result) finally show ?thesis by simp qed unbundle no_intro_cong_syntax end \ No newline at end of file diff --git a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy_Without_Cutoff.thy b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy_Without_Cutoff.thy --- a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy_Without_Cutoff.thy +++ b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Accuracy_Without_Cutoff.thy @@ -1,1007 +1,1007 @@ section \Accuracy without cutoff\label{sec:accuracy_wo_cutoff}\ text \This section verifies that each of the $l$ estimate have the required accuracy with high probability assuming that there was no cut-off, i.e., that $s=0$. Section~\ref{sec:accuracy} will then show that this remains true as long as the cut-off is below @{term "t f"} the subsampling threshold.\ theory Distributed_Distinct_Elements_Accuracy_Without_Cutoff imports Distributed_Distinct_Elements_Inner_Algorithm Distributed_Distinct_Elements_Balls_and_Bins begin no_notation Polynomials.var ("X\") locale inner_algorithm_fix_A = inner_algorithm + fixes A assumes A_range: "A \ {.. A" begin definition X :: nat where "X = card A" definition q_max where "q_max = nat (\log 2 X\ - b_exp)" definition t :: "(nat \ nat) \ int" where "t f = int (Max (f ` A)) - b_exp + 9" definition s :: "(nat \ nat) \ nat" where "s f = nat (t f)" definition R :: "(nat \ nat) \ nat set" where "R f = {a. a \ A \ f a \ s f}" definition r :: "nat \ (nat \ nat) \ nat" where "r x f = card {a. a \ A \ f a \ x}" definition p where "p = (\(f,g,h). card {j\ {..\<^sub>1 (f,g,h) A 0 j \ s f})" definition Y where "Y = (\(f,g,h). 2 ^ s f * \_inv (p (f,g,h)))" lemma fin_A: "finite A" using A_range finite_nat_iff_bounded by auto lemma X_le_n: "X \ n" proof - have "card A \ card {.. 1" unfolding X_def using fin_A A_nonempty by (simp add: leI) lemma of_bool_square: "(of_bool x)\<^sup>2 = ((of_bool x)::real)" by (cases x, auto) lemma r_eq: "r x f = (\ a \ A.( of_bool( x \ f a) :: real))" unfolding r_def of_bool_def sum.If_cases[OF fin_A] by (simp add: Collect_conj_eq) lemma shows r_exp: "(\\. real (r x \) \ \\<^sub>1) = real X * (of_bool (x \ max (nat \log 2 n\) 1) / 2^x)" and r_var: "measure_pmf.variance \\<^sub>1 (\\. real (r x \)) \ (\\. real (r x \) \ \\<^sub>1)" proof - define V :: "nat \ (nat \ nat) \ real" where "V = (\a f. of_bool (x \ f a))" have V_exp: "(\\. V a \ \\\<^sub>1) = of_bool (x \ max (nat \log 2 n\) 1)/2^x" (is "?L = ?R") if "a \ A" for a proof - have a_le_n: "a < n" using that A_range by auto have "?L = (\\. indicator {f. x \ f a} \ \ \\<^sub>1)" unfolding V_def by (intro integral_cong_AE) auto also have "... = measure (map_pmf (\\. \ a) (sample_pmf \\<^sub>1)) {f. x \ f}" by simp also have "... = measure (\ n_exp) {f. x \ f}" unfolding \\<^sub>1.single[OF a_le_n] by simp also have "... = of_bool (x \ max (nat \log 2 n\) 1)/2^x" unfolding \_prob n_exp_def by simp finally show ?thesis by simp qed have b:"(\\. real (r x \) \ \\<^sub>1) = (\ a \ A. (\\. V a \ \\\<^sub>1))" unfolding r_eq V_def using \\<^sub>1.sample_space by (intro Bochner_Integration.integral_sum) auto also have "... = (\ a \ A. of_bool (x \ max (nat \log 2 n\) 1)/2^x)" using V_exp by (intro sum.cong) auto also have "... = X * (of_bool (x \ max (nat \log 2 n\) 1) / 2^x)" using X_def by simp finally show "(\\. real (r x \) \ \\<^sub>1) = real X * (of_bool (x \ max (nat \log 2 n\) 1)/ 2^x)" by simp have "(\\. (V a \)^2 \ \\<^sub>1) = (\\. V a \ \ \\<^sub>1)" for a unfolding V_def of_bool_square by simp hence a:"measure_pmf.variance \\<^sub>1 (V a) \ measure_pmf.expectation \\<^sub>1 (V a)" for a using \\<^sub>1.sample_space by (subst measure_pmf.variance_eq) auto have "J \ A \ card J = 2 \ prob_space.indep_vars \\<^sub>1 (\_. borel) V J" for J unfolding V_def using A_range finite_subset[OF _ fin_A] by (intro prob_space.indep_vars_compose2[where Y="\i y. of_bool(x \ y)" and M'="\_. discrete"] prob_space.k_wise_indep_vars_subset[OF _ \\<^sub>1.indep]) (auto simp:prob_space_measure_pmf) hence "measure_pmf.variance \\<^sub>1 (\\. real (r x \)) = (\ a \ A. measure_pmf.variance \\<^sub>1 (V a))" unfolding r_eq V_def using \\<^sub>1.sample_space by (intro measure_pmf.var_sum_pairwise_indep_2 fin_A) (simp_all) also have "... \ (\ a \ A. (\\. V a \ \ \\<^sub>1))" by (intro sum_mono a) also have "... = (\\. real (r x \) \ \\<^sub>1)" unfolding b by simp finally show "measure_pmf.variance \\<^sub>1 (\\. real (r x \)) \ (\\. real (r x \) \ \\<^sub>1)" by simp qed definition E\<^sub>1 where "E\<^sub>1 = (\(f,g,h). 2 powr (-t f) * X \ {b/2^16..b/2})" lemma t_low: "measure \\<^sub>1 {f. of_int (t f) < log 2 (real X) + 1 - b_exp} \ 1/2^7" (is "?L \ ?R") proof (cases "log 2 (real X) \ 8") case True define Z :: "(nat \ nat) \ real" where "Z = r (nat \log 2 (real X) - 8\)" have "log 2 (real X) \ log 2 (real n)" using X_le_n X_ge_1 by (intro log_mono) auto hence "nat \log 2 (real X) - 8\ \ nat \log 2 (real n)\" by (intro nat_mono ceiling_mono) simp hence a:"(nat \log 2 (real X) - 8\ \ max (nat \log 2 (real n)\) 1)" by simp have b:"real (nat (\log 2 (real X)\ - 8)) \ log 2 (real X) - 7" using True by linarith have "2 ^ 7 = real X / (2 powr (log 2 X) * 2 powr (-7))" using X_ge_1 by simp also have "... = real X / (2 powr (log 2 X - 7))" by (subst powr_add[symmetric]) simp also have "... \ real X / (2 powr (real (nat \log 2 (real X) - 8\)))" using b by (intro divide_left_mono powr_mono) auto also have "... = real X / 2 ^ nat \log 2 (real X) - 8\" by (subst powr_realpow) auto finally have "2 ^ 7 \ real X / 2 ^ nat \log 2 (real X) - 8\" by simp hence exp_Z_gt_2_7: "(\\. Z \ \\\<^sub>1) \ 2^7" using a unfolding Z_def r_exp by simp have var_Z_le_exp_Z: "measure_pmf.variance \\<^sub>1 Z \ (\\. Z \ \\\<^sub>1)" unfolding Z_def by (intro r_var) have "?L \ measure \\<^sub>1 {f. of_nat (Max (f ` A)) < log 2 (real X) - 8}" unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def) also have "... \ measure \\<^sub>1 {f \ space \\<^sub>1. (\\. Z \ \\\<^sub>1) \ \Z f - (\\. Z \ \\\<^sub>1) \}" proof (rule pmf_mono) fix f assume "f \ set_pmf (sample_pmf \\<^sub>1)" have fin_f_A: "finite (f ` A)" using fin_A finite_imageI by blast assume " f \ {f. real (Max (f ` A)) < log 2 (real X) - 8}" hence "real (Max (f ` A)) < log 2 (real X) - 8" by auto hence "real (f a) < log 2 (real X) - 8" if "a \ A" for a using Max_ge[OF fin_f_A] imageI[OF that] order_less_le_trans by fastforce hence "of_nat (f a) < \log 2 (real X) - 8\" if "a \ A" for a using that by (subst less_ceiling_iff) auto hence "f a < nat \log 2 (real X) - 8\" if "a \ A" for a using that True by fastforce hence "r (nat \log 2 (real X) - 8\) f = 0" unfolding r_def card_eq_0_iff using not_less by auto hence "Z f = 0" unfolding Z_def by simp thus "f \ {f \ space \\<^sub>1. (\\. Z \ \\\<^sub>1) \ \Z f - (\\. Z \ \\\<^sub>1)\}" by auto qed also have "... \ measure_pmf.variance \\<^sub>1 Z / (\\. Z \ \\\<^sub>1)^2" using exp_Z_gt_2_7 \\<^sub>1.sample_space by (intro measure_pmf.second_moment_method) simp_all also have "... \ (\\. Z \ \\\<^sub>1) / (\\. Z \ \\\<^sub>1)^2" by (intro divide_right_mono var_Z_le_exp_Z) simp also have "... = 1 / (\\. Z \ \\\<^sub>1)" using exp_Z_gt_2_7 by (simp add:power2_eq_square) also have "... \ ?R" using exp_Z_gt_2_7 by (intro divide_left_mono) auto finally show ?thesis by simp next case "False" have "?L \ measure \\<^sub>1 {f. of_nat (Max (f ` A)) < log 2 (real X) - 8}" unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def) also have "... \ measure \\<^sub>1 {}" using False by (intro pmf_mono) simp also have "... = 0" by simp also have "... \ ?R" by simp finally show ?thesis by simp qed lemma t_high: "measure \\<^sub>1 {f. of_int (t f) > log 2 (real X) + 16 - b_exp} \ 1/2^7" (is "?L \ ?R") proof - define Z :: "(nat \ nat) \ real" where "Z = r (nat \log 2 (real X) + 8\)" have Z_nonneg: "Z f \ 0" for f unfolding Z_def r_def by simp have "(\\. Z \ \\\<^sub>1) \ real X / (2 ^ nat \log 2 (real X) + 8\)" unfolding Z_def r_exp by simp also have "... \ real X / (2 powr (real (nat \log 2 (real X) + 8\)))" by (subst powr_realpow) auto also have "... \ real X / (2 powr \log 2 (real X) + 8\)" by (intro divide_left_mono powr_mono) auto also have "... \ real X / (2 powr (log 2 (real X) + 7))" by (intro divide_left_mono powr_mono, linarith) auto also have "... = real X / 2 powr (log 2 (real X)) / 2 powr 7" by (subst powr_add) simp also have "... \ 1/2 powr 7" using X_ge_1 by (subst powr_log_cancel) auto finally have Z_exp: "(\\. Z \ \\\<^sub>1) \ 1/2^7" by simp have "?L \ measure \\<^sub>1 {f. of_nat (Max (f ` A)) > log 2 (real X) + 7}" unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def) also have "... \ measure \\<^sub>1 {f. Z f \ 1}" proof (rule pmf_mono) fix f assume "f \ set_pmf (sample_pmf \\<^sub>1)" assume " f \ {f. real (Max (f ` A)) > log 2 (real X) + 7}" hence "real (Max (f ` A)) > log 2 (real X) + 7" by simp hence "int (Max (f ` A)) \ \log 2 (real X) + 8\" by linarith hence "Max (f ` A) \ nat \log 2 (real X) + 8\" by simp moreover have "f ` A \ {}" "finite (f ` A)" using fin_A finite_imageI A_nonempty by auto ultimately obtain fa where "fa \ f ` A" " fa \ nat \log 2 (real X) + 8\" using Max_in by auto then obtain ae where ae_def: "ae \ A" "nat \log 2 (real X) + 8\ \ f ae" by auto hence "r (nat \log 2 (real X) + 8\) f > 0" unfolding r_def card_gt_0_iff using fin_A by auto hence "Z f \ 1" unfolding Z_def by simp thus "f \ {f. 1 \ Z f}" by simp qed also have "... \ (\\. Z \ \\\<^sub>1) / 1" using Z_nonneg using \\<^sub>1.sample_space by (intro pmf_markov) auto also have "... \ ?R" using Z_exp by simp finally show ?thesis by simp qed lemma e_1: "measure \ {\. \E\<^sub>1 \} \ 1/2^6" proof - have "measure \\<^sub>1 {f. 2 powr (of_int (-t f)) * real X \ {real b/2^16..real b/2}} \ measure \\<^sub>1 {f. 2 powr (of_int (-t f)) * real X < real b/2^16} + measure \\<^sub>1 {f. 2 powr (of_int (-t f)) * real X > real b/2}" by (intro pmf_add) auto also have "... \ measure \\<^sub>1 {f. of_int (t f) > log 2 X + 16 - b_exp} + measure \\<^sub>1 {f. of_int (t f) < log 2 X + 1 - b_exp}" proof (rule add_mono) show "measure \\<^sub>1 {f. 2 powr (of_int (-t f)) * real X < real b/2^16} \ measure \\<^sub>1 {f. of_int (t f) > log 2 X + 16 - b_exp}" proof (rule pmf_mono) fix f assume "f \ {f. 2 powr real_of_int (-t f) * real X < real b / 2 ^ 16}" hence "2 powr real_of_int (-t f) * real X < real b / 2 ^ 16" by simp hence "log 2 (2 powr of_int (-t f) * real X) < log 2 (real b / 2^16)" using b_min X_ge_1 by (intro iffD2[OF log_less_cancel_iff]) auto hence "of_int (-t f) + log 2 (real X) < log 2 (real b / 2^16)" using X_ge_1 by (subst (asm) log_mult) auto also have "... = real b_exp - log 2 (2 powr 16)" unfolding b_def by (subst log_divide) auto also have "... = real b_exp - 16" by (subst log_powr_cancel) auto finally have "of_int (-t f) + log 2 (real X) < real b_exp - 16" by simp thus "f \ {f. of_int (t f) > log 2 (real X) + 16 - b_exp}" by simp qed next show "measure \\<^sub>1 {f. 2 powr of_int (-t f) * real X > real b/2} \ measure \\<^sub>1 {f. of_int (t f) < log 2 X + 1 - b_exp}" proof (rule pmf_mono) fix f assume "f \ {f. 2 powr real_of_int (-t f) * real X > real b / 2}" hence "2 powr real_of_int (-t f) * real X > real b / 2" by simp hence "log 2 (2 powr of_int (-t f) * real X) > log 2 (real b / 2)" using b_min X_ge_1 by (intro iffD2[OF log_less_cancel_iff]) auto hence "of_int (-t f) + log 2 (real X) > log 2 (real b / 2)" using X_ge_1 by (subst (asm) log_mult) auto hence "of_int (-t f) + log 2 (real X) > real b_exp - 1" unfolding b_def by (subst (asm) log_divide) auto hence "of_int (t f) < log 2 (real X) + 1 - b_exp" by simp thus "f \ {f. of_int (t f) < log 2 (real X) + 1 - b_exp}" by simp qed qed also have "... \ 1/2^7 + 1/2^7" by (intro add_mono t_low t_high) also have "... = 1/2^6" by simp finally have "measure \\<^sub>1 {f. 2 powr of_int (-t f) * real X \ {real b/2^16..real b/2}} \ 1/2^6" by simp thus ?thesis unfolding sample_pmf_\ E\<^sub>1_def case_prod_beta by (subst pair_pmf_prob_left) qed -definition E\<^sub>2 where "E\<^sub>2 = (\(f,g,h). \card (R f) - X / 2^(s f)\ \ \/3 * X / 2^(s f))" +definition E\<^sub>2 where "E\<^sub>2 = (\(f,g,h). \card (R f) - X / 2^(s f)\ \ \/3 * X / 2^(s f))" lemma e_2: "measure \ {\. E\<^sub>1 \ \ \E\<^sub>2 \} \ 1/2^6" (is "?L \ ?R") proof - define t\<^sub>m :: int where "t\<^sub>m = \log 2 (real X)\ + 16 - b_exp" have t_m_bound: "t\<^sub>m \ \log 2 (real X)\ - 10" unfolding t\<^sub>m_def using b_exp_ge_26 by simp have "real b / 2^16 = (real X * (1/ X)) * (real b / 2^16)" using X_ge_1 by simp also have "... = (real X * 2 powr (-log 2 X)) * (real b / 2^16)" using X_ge_1 by (subst powr_minus_divide) simp also have "... \ (real X * 2 powr (- \log 2 (real X)\)) * (2 powr b_exp / 2^16)" unfolding b_def using powr_realpow by (intro mult_mono powr_mono) auto also have "... = real X * (2 powr (- \log 2 (real X)\) * 2 powr(real b_exp-16))" by (subst powr_diff) simp also have "... = real X * 2 powr (- \log 2 (real X)\ + (int b_exp - 16))" by (subst powr_add[symmetric]) simp also have "... = real X * 2 powr (-t\<^sub>m)" unfolding t\<^sub>m_def by (simp add:algebra_simps) finally have c:"real b / 2^16 \ real X * 2 powr (-t\<^sub>m)" by simp define T :: "nat set" where "T = {x. (real X / 2^x \ real b / 2^16)}" have "x \ T \ int x \ t\<^sub>m" for x proof - have "x \ T \ 2^ x \ real X * 2^16 / b" using b_min by (simp add: field_simps T_def) also have "... \ log 2 (2^x) \ log 2 (real X * 2^16 / b)" using X_ge_1 b_min by (intro log_le_cancel_iff[symmetric] divide_pos_pos) auto also have "... \ x \ log 2 (real X * 2^16) - log 2 b" using X_ge_1 b_min by (subst log_divide) auto also have "... \ x \ log 2 (real X) + log 2 (2 powr 16) - b_exp" unfolding b_def using X_ge_1 by (subst log_mult) auto also have "... \ x \ \log 2 (real X) + log 2 (2 powr 16) - b_exp\" by linarith also have "... \ x \ \log 2 (real X) + 16 - real_of_int (int b_exp)\" by (subst log_powr_cancel) auto also have "... \ x \ t\<^sub>m" unfolding t\<^sub>m_def by linarith finally show ?thesis by simp qed hence T_eq: "T = {x. int x \ t\<^sub>m}" by auto have "T = {x. int x < t\<^sub>m+1}" unfolding T_eq by simp also have "... = {x. x < nat (t\<^sub>m + 1)}" unfolding zless_nat_eq_int_zless by simp finally have T_eq_2: "T = {x. x < nat (t\<^sub>m + 1)}" by simp have inj_1: "inj_on ((-) (nat t\<^sub>m)) T" unfolding T_eq by (intro inj_onI) simp have fin_T: "finite T" unfolding T_eq_2 by simp have r_exp: "(\\. real (r t \) \\\<^sub>1) = real X / 2^t" if "t \ T" for t proof - have "t \ t\<^sub>m" using that unfolding T_eq by simp also have "... \ \log 2 (real X)\ - 10" using t_m_bound by simp also have "... \ \log 2 (real X)\" by simp also have "... \ \log 2 (real n)\" using X_le_n X_ge_1 by (intro floor_mono log_mono) auto also have "... \ \log 2 (real n)\" by simp finally have "t \ \log 2 (real n)\" by simp hence "t \ max (nat \log 2 (real n)\) 1"by simp thus ?thesis unfolding r_exp by simp qed have r_var: "measure_pmf.variance \\<^sub>1 (\\. real (r t \)) \ real X / 2^t" if "t \ T" for t using r_exp[OF that] r_var by metis - have "9 = C\<^sub>4 / \\<^sup>2 * \^2/2^23" - using \_gt_0 by (simp add:C\<^sub>4_def) - also have "... = 2 powr (log 2 (C\<^sub>4 / \\<^sup>2)) * \^2/2^23" - using \_gt_0 C\<^sub>4_def by (subst powr_log_cancel) auto - also have "... \ 2 powr b_exp * \^2/2^23" + have "9 = C\<^sub>4 / \\<^sup>2 * \^2/2^23" + using \_gt_0 by (simp add:C\<^sub>4_def) + also have "... = 2 powr (log 2 (C\<^sub>4 / \\<^sup>2)) * \^2/2^23" + using \_gt_0 C\<^sub>4_def by (subst powr_log_cancel) auto + also have "... \ 2 powr b_exp * \^2/2^23" unfolding b_exp_def by (intro divide_right_mono mult_right_mono powr_mono, linarith) auto - also have "... = b * \^2/2^23" + also have "... = b * \^2/2^23" using powr_realpow unfolding b_def by simp - also have "... = (b/2^16) * (\^2/2^7)" + also have "... = (b/2^16) * (\^2/2^7)" by simp - also have "... \ (X * 2 powr (-t\<^sub>m)) * (\^2/2^7)" + also have "... \ (X * 2 powr (-t\<^sub>m)) * (\^2/2^7)" by (intro mult_mono c) auto - also have "... = X * (2 powr (-t\<^sub>m) * 2 powr (-7)) * \^2" + also have "... = X * (2 powr (-t\<^sub>m) * 2 powr (-7)) * \^2" using powr_realpow by simp - also have "... = 2 powr (-t\<^sub>m-7) * (\^2 * X)" + also have "... = 2 powr (-t\<^sub>m-7) * (\^2 * X)" by (subst powr_add[symmetric]) (simp ) - finally have "9 \ 2 powr (-t\<^sub>m-7) * (\^2 * X)" by simp - hence b: "9/ (\^2 * X) \ 2 powr (-t\<^sub>m -7)" - using \_gt_0 X_ge_1 + finally have "9 \ 2 powr (-t\<^sub>m-7) * (\^2 * X)" by simp + hence b: "9/ (\^2 * X) \ 2 powr (-t\<^sub>m -7)" + using \_gt_0 X_ge_1 by (subst pos_divide_le_eq) auto - have a: "measure \\<^sub>1 {f.\real (r t f)-real X/2^t\> \/3 *real X/2^t} \ 2 powr (real t-t\<^sub>m-7)" + have a: "measure \\<^sub>1 {f.\real (r t f)-real X/2^t\> \/3 *real X/2^t} \ 2 powr (real t-t\<^sub>m-7)" (is"?L1 \ ?R1") if "t \ T" for t proof - - have "?L1 \ \

(f in \\<^sub>1. \real (r t f) - real X / 2^t\ \ \/3 * real X / 2^t)" + have "?L1 \ \

(f in \\<^sub>1. \real (r t f) - real X / 2^t\ \ \/3 * real X / 2^t)" by (intro pmf_mono) auto - also have "... = \

(f in \\<^sub>1. \real (r t f)-(\\. real (r t \) \ \\<^sub>1)\ \ \/3 * real X/2^t)" + also have "... = \

(f in \\<^sub>1. \real (r t f)-(\\. real (r t \) \ \\<^sub>1)\ \ \/3 * real X/2^t)" by (simp add: r_exp[OF that]) - also have "... \ measure_pmf.variance \\<^sub>1 (\\. real (r t \)) / (\/3 * real X / 2^t)^2" - using X_ge_1 \_gt_0 \\<^sub>1.sample_space + also have "... \ measure_pmf.variance \\<^sub>1 (\\. real (r t \)) / (\/3 * real X / 2^t)^2" + using X_ge_1 \_gt_0 \\<^sub>1.sample_space by (intro measure_pmf.Chebyshev_inequality divide_pos_pos mult_pos_pos) auto - also have "... \ (X / 2^t) / (\/3 * X / 2^t)^2" + also have "... \ (X / 2^t) / (\/3 * X / 2^t)^2" by (intro divide_right_mono r_var[OF that]) simp - also have "... = 2^t*(9/ ( \^2 * X))" + also have "... = 2^t*(9/ ( \^2 * X))" by (simp add:power2_eq_square algebra_simps) also have "... \ 2^t*(2 powr (-t\<^sub>m-7))" by (intro mult_left_mono b) simp also have "... = 2 powr t * 2 powr (-t\<^sub>m-7)" by (subst powr_realpow[symmetric]) auto also have "... = ?R1" by (subst powr_add[symmetric]) (simp add:algebra_simps) finally show "?L1 \ ?R1" by simp qed have "\ym + 1). x = nat t\<^sub>m - y" if "x < nat (t\<^sub>m+1)" for x using that by (intro exI[where x="nat t\<^sub>m - x"]) simp hence T_reindex: "(-) (nat t\<^sub>m) ` {x. x < nat (t\<^sub>m + 1)} = {..m + 1)}" by (auto simp add: set_eq_iff image_iff) - have "?L \ measure \ {\. (\t \ T. \real (r t (fst \))-real X/2^t\ > \/3 * real X / 2^t)}" + have "?L \ measure \ {\. (\t \ T. \real (r t (fst \))-real X/2^t\ > \/3 * real X / 2^t)}" proof (rule pmf_mono) fix \ assume "\ \ set_pmf (sample_pmf \)" obtain f g h where \_def: "\ = (f,g,h)" by (metis prod_cases3) assume "\ \ {\. E\<^sub>1 \ \ \ E\<^sub>2 \}" hence a:"2 powr ( -real_of_int (t f)) * real X \ {real b/2^16..real b/2}" and - b:"\card (R f) - real X / 2^(s f)\ > \/3 * X / 2^(s f)" + b:"\card (R f) - real X / 2^(s f)\ > \/3 * X / 2^(s f)" unfolding E\<^sub>1_def E\<^sub>2_def by (auto simp add:\_def) have "\card (R f) - X / 2^(s f)\ = 0" if "s f= 0" using that by (simp add:R_def X_def) - moreover have "( \/3) * (X / 2^s f) \ 0" - using \_gt_0 X_ge_1 by (intro mult_nonneg_nonneg) auto + moreover have "( \/3) * (X / 2^s f) \ 0" + using \_gt_0 X_ge_1 by (intro mult_nonneg_nonneg) auto ultimately have "False" if "s f = 0" using b that by simp hence "s f > 0" by auto hence "t f = s f" unfolding s_def by simp hence "2 powr (-real (s f)) * X \ b / 2^16" using a by simp hence "X / 2 powr (real (s f)) \ b / 2^16" by (simp add: divide_powr_uminus mult.commute) hence "real X / 2 ^ (s f) \ b / 2^16" by (subst (asm) powr_realpow, auto) hence "s f \ T" unfolding T_def by simp - moreover have "\r (s f) f - X / 2^s f\ > \/3 * X / 2^s f" + moreover have "\r (s f) f - X / 2^s f\ > \/3 * X / 2^s f" using R_def r_def b by simp - ultimately have "\t \ T. \r t (fst \) - X / 2^t\ > \/3 * X / 2^t" + ultimately have "\t \ T. \r t (fst \) - X / 2^t\ > \/3 * X / 2^t" using \_def by (intro bexI[where x="s f"]) simp - thus "\ \ {\. (\t \ T. \r t (fst \) - X / 2^t\ > \/3 * X / 2^t)}" by simp + thus "\ \ {\. (\t \ T. \r t (fst \) - X / 2^t\ > \/3 * X / 2^t)}" by simp qed - also have "... = measure \\<^sub>1 {f. (\t \ T. \real (r t f)-real X / 2^t\ > \/3 * real X/2^t)}" + also have "... = measure \\<^sub>1 {f. (\t \ T. \real (r t f)-real X / 2^t\ > \/3 * real X/2^t)}" unfolding sample_pmf_\ by (intro pair_pmf_prob_left) - also have "... = measure \\<^sub>1 (\t \ T. {f. \real (r t f)-real X / 2^t\ > \/3 * real X/2^t})" + also have "... = measure \\<^sub>1 (\t \ T. {f. \real (r t f)-real X / 2^t\ > \/3 * real X/2^t})" by (intro measure_pmf_cong) auto - also have "... \ (\t \ T. measure \\<^sub>1 {f.\real (r t f)-real X / 2^t\ > \/3 * real X/2^t})" + also have "... \ (\t \ T. measure \\<^sub>1 {f.\real (r t f)-real X / 2^t\ > \/3 * real X/2^t})" by (intro measure_UNION_le fin_T) (simp) also have "... \ (\t \ T. 2 powr (real t - of_int t\<^sub>m - 7))" by (intro sum_mono a) also have "... = (\t \ T. 2 powr (-int (nat t\<^sub>m-t) - 7))" unfolding T_eq by (intro sum.cong refl arg_cong2[where f="(powr)"]) simp also have "... = (\x \ (\x. nat t\<^sub>m - x) ` T. 2 powr (-real x - 7))" by (subst sum.reindex[OF inj_1]) simp also have "... = (\x \ (\x. nat t\<^sub>m - x) ` T. 2 powr (-7) * 2 powr (-real x))" by (subst powr_add[symmetric]) (simp add:algebra_simps) also have "... = 1/2^7 * (\x \ (\x. nat t\<^sub>m - x) ` T. 2 powr (-real x))" by (subst sum_distrib_left) simp also have "... = 1/2^7 * (\x m+1). 2 powr (-real x))" unfolding T_eq_2 T_reindex by (intro arg_cong2[where f="(*)"] sum.cong) auto also have "... = 1/2^7 * (\x m+1). (2 powr (-1)) powr (real x))" by (subst powr_powr) simp also have "... = 1/2^7 * (\x m+1). (1/2)^x)" using powr_realpow by simp also have "... \ 1/2^7 * 2" by(subst geometric_sum) auto also have "... = 1/2^6" by simp finally show ?thesis by simp qed definition E\<^sub>3 where "E\<^sub>3 = (\(f,g,h). inj_on g (R f))" lemma R_bound: fixes f g h assumes "E\<^sub>1 (f,g,h)" assumes "E\<^sub>2 (f,g,h)" shows "card (R f) \ 2/3 * b" proof - - have "real (card (R f)) \ ( \ / 3) * (real X / 2 ^ s f) + real X / 2 ^ s f" + have "real (card (R f)) \ ( \ / 3) * (real X / 2 ^ s f) + real X / 2 ^ s f" using assms(2) unfolding E\<^sub>2_def by simp also have "... \ (1/3) * (real X / 2 ^ s f) + real X / 2 ^ s f" - using \_lt_1 by (intro add_mono mult_right_mono) auto + using \_lt_1 by (intro add_mono mult_right_mono) auto also have "... = (4/3) * (real X / 2 powr s f)" using powr_realpow by simp also have "... \ (4/3) * (real X / 2 powr t f)" unfolding s_def by (intro mult_left_mono divide_left_mono powr_mono) auto also have "... = (4/3) * (2 powr (-(of_int (t f))) * real X)" by (subst powr_minus_divide) simp also have "... = (4/3) * (2 powr (- t f) * real X)" by simp also have "... \ (4/3) * (b/2)" using assms(1) unfolding E\<^sub>1_def by (intro mult_left_mono) auto also have "... \ (2/3) * b" by simp finally show ?thesis by simp qed lemma e_3: "measure \ {\. E\<^sub>1 \ \ E\<^sub>2 \ \ \E\<^sub>3 \} \ 1/2^6" (is "?L \ ?R") proof - let ?\ = "(\(z,x,y) f. z < C\<^sub>7*b^2 \ x \ R f \ y \ R f \ x < y)" let ?\ = "(\(z,x,y) g. g x = z \ g y = z)" have \_prob: "measure \\<^sub>2 {g. ?\ \ g} \ (1/real (C\<^sub>7*b^2)^2)" if "?\ \ f" for \ f proof - obtain x y z where \_def: "\ = (z,x,y)" by (metis prod_cases3) have a:"prob_space.k_wise_indep_vars \\<^sub>2 2 (\i. discrete) (\x \. \ x = z) {..\<^sub>2.indep]) (simp_all add:prob_space_measure_pmf) have "u \ R f \ u < n" for u unfolding R_def using A_range by auto hence b: "x < n" "y < n" "card {x, y} = 2" using that \_def by auto have c: "z < C\<^sub>7*b\<^sup>2" using \_def that by simp have "measure \\<^sub>2 {g. ?\ \ g} = measure \\<^sub>2 {g. (\\ \ {x,y}. g \ = z)}" by (simp add:\_def) also have "... = (\\ \ {x,y}. measure \\<^sub>2 {g. g \ = z})" using b by (intro measure_pmf.split_indep_events[OF refl, where I="{x,y}"] prob_space.k_wise_indep_vars_subset[OF _ a]) (simp_all add:prob_space_measure_pmf) also have "... = (\\ \ {x,y}. measure (map_pmf (\\. \ \) (sample_pmf \\<^sub>2)) {g. g = z}) " by (simp add:vimage_def) also have "... = (\\ \ {x,y}. measure [C\<^sub>7 * b\<^sup>2]\<^sub>S {g. g=z})" using b \\<^sub>2.single by (intro prod.cong) fastforce+ also have "... = (\\ \ {x,y}. measure (pmf_of_set {..7 * b\<^sup>2}) {z})" by (subst nat_sample_pmf) simp also have "... = (measure (pmf_of_set {..7 * b\<^sup>2}) {z})^2" using b by simp also have "... \ (1 /(C\<^sub>7*b\<^sup>2))^2" using c by (subst measure_pmf_of_set) auto also have "... = (1 /(C\<^sub>7*b\<^sup>2)^2)" by (simp add:algebra_simps power2_eq_square) finally show ?thesis by simp qed have \_card: "card {\. ?\ \ f} \ (C\<^sub>7*b^2) * (card (R f) * (card (R f)-1)/2)" (is "?TL \ ?TR") and fin_\: "finite {\. ?\ \ f}" (is "?T2") for f proof - have t1: "{\. ?\ \ f} \ {..7*b^2} \ {(x,y) \ R f \ R f. x < y}" by (intro subsetI) auto moreover have "card ({..7*b^2} \ {(x,y) \ R f \ R f. x < y}) = ?TR" using card_ordered_pairs'[where M="R f"] by (simp add: card_cartesian_product) moreover have "finite (R f)" unfolding R_def using fin_A finite_subset by simp hence "finite {(x, y). (x, y) \ R f \ R f \ x < y}" by (intro finite_subset[where B="R f \ R f", OF _ finite_cartesian_product]) auto hence t2: "finite ({..7*b^2} \ {(x,y) \ R f \ R f. x < y})" by (intro finite_cartesian_product) auto ultimately show "?TL \ ?TR" using card_mono of_nat_le_iff by (metis (no_types, lifting)) show ?T2 using finite_subset[OF t1 t2] by simp qed have "?L \ measure \ {(f,g,h). card (R f) \ b \ (\ x y z. ?\ (x,y,z) f \ ?\ (x,y,z) g)}" proof (rule pmf_mono) fix \ assume b:"\ \ set_pmf (sample_pmf \)" obtain f g h where \_def:"\ = (f,g,h)" by (metis prod_cases3) have "(f,g,h) \ sample_set \" using sample_space_alt[OF sample_space_\] b \_def by simp hence c:"g x < C\<^sub>7*b^2" for x using g_range by simp assume a:"\ \ {\. E\<^sub>1 \ \ E\<^sub>2 \ \ \ E\<^sub>3 \}" hence "card (R f) \ 2/3 * b" using R_bound \_def by force moreover have "\a b. a \ R f \ b \ R f \ a \ b \ g a = g b" using a unfolding \_def E\<^sub>3_def inj_on_def by auto hence "\x y. x \ R f \ y \ R f \ x < y \ g x = g y" by (metis not_less_iff_gr_or_eq) hence "\x y z. ?\ (x,y,z) f \ ?\ (x,y,z) g" using c by blast ultimately show "\ \ {(f, g, h). card (R f) \ b \ (\ x y z. ?\ (x,y,z) f \ ?\ (x,y,z) g)}" unfolding \_def by auto qed also have "... = (\f. measure (pair_pmf \\<^sub>2 \\<^sub>3) {g. card (R f) \ b \ (\x y z. ?\ (x,y,z) f \ ?\ (x,y,z) (fst g))} \\\<^sub>1)" unfolding sample_pmf_\ split_pair_pmf by (simp add: case_prod_beta) also have "... = (\f. measure \\<^sub>2 {g. card (R f) \ b \ (\x y z. ?\ (x,y,z) f \ ?\ (x,y,z) g)} \\\<^sub>1)" by (subst pair_pmf_prob_left) simp also have "... \ (\f. 1/real (2*C\<^sub>7) \\\<^sub>1)" proof (rule pmf_exp_mono[OF integrable_sample_pmf[OF \\<^sub>1.sample_space] integrable_sample_pmf[OF \\<^sub>1.sample_space]]) fix f assume "f \ set_pmf (sample_pmf \\<^sub>1)" show "measure \\<^sub>2 {g. card (R f) \ b \ (\x y z. ?\ (x,y,z) f \ ?\ (x,y,z) g)} \ 1 / real (2 * C\<^sub>7)" (is "?L1 \ ?R1") proof (cases "card (R f) \ b") case True have "?L1 \ measure \\<^sub>2 (\ \ \ {\. ?\ \ f}. {g. ?\ \ g})" by (intro pmf_mono) auto also have "... \ (\\ \ {\. ?\ \ f}. measure \\<^sub>2 {g. ?\ \ g})" by (intro measure_UNION_le fin_\) auto also have "... \ (\\ \ {\. ?\ \ f}. (1/real (C\<^sub>7*b^2)^2))" by (intro sum_mono \_prob) auto also have "... = card {\. ?\ \ f} /(C\<^sub>7*b^2)^2" by simp also have "... \ (C\<^sub>7*b^2) * (card (R f) * (card (R f)-1)/2) / (C\<^sub>7*b^2)^2" by (intro \_card divide_right_mono) simp also have "... \ (C\<^sub>7*b^2) * (b * b / 2) / (C\<^sub>7*b^2)^2" unfolding C\<^sub>7_def using True by (intro divide_right_mono Nat.of_nat_mono mult_mono) auto also have "... = 1/(2*C\<^sub>7)" using b_min by (simp add:algebra_simps power2_eq_square) finally show ?thesis by simp next case False then show ?thesis by simp qed qed also have "... \ 1/2^6" unfolding C\<^sub>7_def by simp finally show ?thesis by simp qed -definition E\<^sub>4 where "E\<^sub>4 = (\(f,g,h). \p (f,g,h) - \ (card (R f))\ \ \/12 * card (R f))" +definition E\<^sub>4 where "E\<^sub>4 = (\(f,g,h). \p (f,g,h) - \ (card (R f))\ \ \/12 * card (R f))" -lemma e_4_h: "9 / sqrt b \ \ / 12" +lemma e_4_h: "9 / sqrt b \ \ / 12" proof - have "108 \ sqrt (C\<^sub>4)" unfolding C\<^sub>4_def by (approximation 5) - also have "... \ sqrt( \^2 * real b)" - using b_lower_bound \_gt_0 + also have "... \ sqrt( \^2 * real b)" + using b_lower_bound \_gt_0 by (intro real_sqrt_le_mono) (simp add: pos_divide_le_eq algebra_simps) - also have "... = \ * sqrt b" - using \_gt_0 by (simp add:real_sqrt_mult) - finally have "108 \ \ * sqrt b" by simp + also have "... = \ * sqrt b" + using \_gt_0 by (simp add:real_sqrt_mult) + finally have "108 \ \ * sqrt b" by simp thus ?thesis using b_min by (simp add:pos_divide_le_eq) qed lemma e_4: "measure \ {\. E\<^sub>1 \ \ E\<^sub>2 \ \ E\<^sub>3 \ \ \E\<^sub>4 \} \ 1/2^6" (is "?L \ ?R") proof - have a: "measure \\<^sub>3 {h. E\<^sub>1 (f,g,h) \ E\<^sub>2 (f,g,h) \ E\<^sub>3 (f,g,h) \ \E\<^sub>4 (f,g,h)} \ 1/2^6" (is "?L1 \ ?R1") if "f \ set_pmf (sample_pmf \\<^sub>1)" "g \ set_pmf(sample_pmf \\<^sub>2)" for f g proof (cases "card (R f) \ b \ inj_on g (R f)") case True have g_inj: "inj_on g (R f)" using True by simp have fin_R: "finite (g ` R f)" unfolding R_def using fin_A by (intro finite_imageI) simp interpret B:balls_and_bins_abs "g ` R f" "{.. {..7 * b\<^sup>2}" using g_range_1 that(2) unfolding sample_space_alt[OF \\<^sub>2.sample_space] by auto hence g_ran: "g ` R f \ {..7 * b\<^sup>2}" by auto have "sample_pmf [b]\<^sub>S = pmf_of_set {..\. \ x) (sample_pmf (\ k (C\<^sub>7 * b\<^sup>2) [b]\<^sub>S)) = pmf_of_set {.. g ` R f" for x using g_ran \\<^sub>3.single that by auto moreover have "prob_space.k_wise_indep_vars \\<^sub>3 k (\_. discrete) (\x \. \ x) (g ` R f)" by (intro prob_space.k_wise_indep_subset[OF _ _ \\<^sub>3.indep] g_ran prob_space_measure_pmf) ultimately have lim_balls_and_bins: "B.lim_balls_and_bins k (sample_pmf (\ k (C\<^sub>7 * b\<^sup>2) [b]\<^sub>S))" unfolding B.lim_balls_and_bins_def by auto have card_g_R: "card (g ` R f) = card (R f)" using True card_image by auto hence b_mu: "\ (card (R f)) = B.\" unfolding B.\_def \_def using b_min by (simp add:powr_realpow) have card_g_le_b: "card (g ` R f) \ card {.. measure \\<^sub>3 {h. \B.Y h - B.\\ > 9 * real (card (g ` R f)) / sqrt (card {.. {h. E\<^sub>1 (f,g,h) \ E\<^sub>2 (f,g,h) \ E\<^sub>3 (f,g,h) \ \E\<^sub>4 (f,g,h)}" - hence b: "\p (f,g,h) -\ (card (R f))\ > \/12 * card (R f)" + hence b: "\p (f,g,h) -\ (card (R f))\ > \/12 * card (R f)" unfolding E\<^sub>4_def by simp assume "h \ set_pmf (sample_pmf \\<^sub>3)" hence h_range: "h x < b" for x unfolding sample_space_alt[OF \\<^sub>3.sample_space,symmetric] using h_range_1 by simp have "{j \ {.. \\<^sub>1 (f, g, h) A 0 j} = {j \ {.. max (Max ({int (f a) |a. a \ A \ h (g a) = j} \ {-1})) (- 1)}" unfolding \\<^sub>1_def by simp also have "... = {j \ {.. Max ({int (f a) |a. a \ A \ h (g a) = j} \ {-1})}" using fin_A by (subst max_absorb1) (auto intro: Max_ge) also have "... = {j \ {..a \ R f. h (g a) = j)}" unfolding R_def using fin_A by (subst Max_ge_iff) auto also have "... = {j. \a \ R f. h (g a) = j}" using h_range by auto also have "... = (h \ g) ` (R f)" by (auto simp add:set_eq_iff image_iff) also have "... = h ` (g ` (R f))" by (simp add:image_image) finally have c:"{j \ {.. \\<^sub>1 (f, g, h) A 0 j} = h ` (g ` R f)" by simp have "9 * real (card (g ` R f)) / sqrt (card {.. \/12 * card (R f)" + also have "... \ \/12 * card (R f)" by (intro mult_right_mono e_4_h) simp also have "... < \B.Y h - B.\\" using b c unfolding B.Y_def p_def b_mu by simp finally show "h \ {h. \B.Y h - B.\\ > 9 * real (card (g ` R f)) / sqrt (card {.. 1/2^6" using k_min by (intro B.devitation_bound[OF card_g_le_b lim_balls_and_bins]) auto finally show ?thesis by simp next case False have "?L1 \ measure \\<^sub>3 {}" proof (rule pmf_mono) fix h assume b:"h \ {h. E\<^sub>1 (f, g, h) \ E\<^sub>2 (f, g, h) \ E\<^sub>3 (f, g, h) \ \ E\<^sub>4 (f, g, h)}" hence "card (R f) \ (2/3)*b" by (auto intro!: R_bound[simplified]) hence "card (R f) \ b" by simp moreover have "inj_on g (R f)" using b by (simp add:E\<^sub>3_def) ultimately have "False" using False by simp thus "h \ {}" by simp qed also have "... = 0" by simp finally show ?thesis by simp qed have "?L = (\f. (\g. measure \\<^sub>3 {h. E\<^sub>1 (f,g,h) \ E\<^sub>2 (f,g,h) \ E\<^sub>3 (f,g,h) \ \E\<^sub>4 (f,g,h)} \\\<^sub>2) \\\<^sub>1)" unfolding sample_pmf_\ split_pair_pmf by simp also have "... \ (\f. (\g. 1/2^6 \\\<^sub>2) \\\<^sub>1)" using a \\<^sub>1.sample_space \\<^sub>2.sample_space by (intro integral_mono_AE AE_pmfI) simp_all also have "... = 1/2^6" by simp finally show ?thesis by simp qed lemma \_inverse: "\_inv (\ x) = x" proof - have a:"1-1/b \ 0" using b_min by simp have "\ x = b * (1-(1-1/b) powr x)" unfolding \_def by simp hence "\ x / real b = 1-(1-1/b) powr x" by simp hence "ln (1 - \ x / real b) = ln ((1-1/b) powr x)" by simp also have "... = x * ln (1 - 1/ b)" using a by (intro ln_powr) finally have "ln (1 - \ x / real b) = x * ln (1- 1/ b)" by simp moreover have "ln (1-1/b) < 0" using b_min by (subst ln_less_zero_iff) auto ultimately show ?thesis using \_inv_def by simp qed lemma rho_mono: assumes "x \ y" shows "\ x \ \ y" proof- have "(1 - 1 / real b) powr y \ (1 - 1 / real b) powr x" using b_min by (intro powr_mono_rev assms) auto thus ?thesis unfolding \_def by (intro mult_left_mono) auto qed lemma rho_two_thirds: "\ (2/3 * b) \ 3/5 *b" proof - have "1/3 \ exp ( - 13 / 12::real )" by (approximation 8) also have "... \ exp ( - 1 - 2 / real b )" using b_min by (intro iffD2[OF exp_le_cancel_iff]) (simp add:algebra_simps) also have "... \ exp ( b * (-(1/real b)-2*(1/real b)^2))" using b_min by (simp add:algebra_simps power2_eq_square) also have "... \ exp ( b * ln (1-1/real b))" using b_min by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono ln_one_minus_pos_lower_bound) auto also have "... = exp ( ln ( (1-1/real b) powr b))" using b_min by (subst ln_powr) auto also have "... = (1-1/real b) powr b" using b_min by (subst exp_ln) auto finally have a:"1/3 \ (1-1/real b) powr b" by simp have "2/5 \ (1/3) powr (2/3::real)" by (approximation 5) also have "... \ ((1-1/real b) powr b) powr (2/3)" by (intro powr_mono2 a) auto also have "... = (1-1/real b) powr (2/3 * real b)" by (subst powr_powr) (simp add:algebra_simps) finally have "2/5 \ (1 - 1 / real b) powr (2 / 3 * real b)" by simp hence "1 - (1 - 1 / real b) powr (2 / 3 * real b) \ 3/5" by simp hence "\ (2/3 * b) \ b * (3/5)" unfolding \_def by (intro mult_left_mono) auto thus ?thesis by simp qed definition \_inv' :: "real \ real" where "\_inv' x = -1 / (real b * (1-x / real b) * ln (1 - 1 / real b))" lemma \_inv'_bound: assumes "x \ 0" assumes "x \ 59/90*b" shows "\\_inv' x\ \ 4" proof - have c:"ln (1 - 1 / real b) < 0" using b_min by (subst ln_less_zero_iff) auto hence d:"real b * (1 - x / real b) * ln (1 - 1 / real b) < 0" using b_min assms by (intro Rings.mult_pos_neg) auto have "(1::real) \ 31/30" by simp also have "... \ (31/30) * (b * -(- 1 / real b))" using b_min by simp also have "... \ (31/30) * (b * -ln (1 + (- 1 / real b)))" using b_min by (intro mult_left_mono le_imp_neg_le ln_add_one_self_le_self2) auto also have "... \ 3 * (31/90) * (- b * ln (1 - 1 / real b))" by simp also have "... \ 3 * (1 - x / real b) * (- b * ln (1 - 1 / real b))" using assms b_min pos_divide_le_eq[where c="b"] c by (intro mult_right_mono mult_left_mono mult_nonpos_nonpos) auto also have "... \ 3 * (real b * (1 - x / real b) * (-ln (1 - 1 / real b)))" by (simp add:algebra_simps) finally have "3 * (real b * (1 - x / real b) * (-ln (1 - 1 / real b))) \ 1" by simp hence "3 * (real b * (1 - x / real b) * ln (1 - 1 / real b)) \ -1" by simp hence "\_inv' x \ 3" unfolding \_inv'_def using d by (subst neg_divide_le_eq) auto moreover have "\_inv' x > 0" unfolding \_inv'_def using d by (intro divide_neg_neg) auto ultimately show ?thesis by simp qed lemma \_inv': fixes x :: real assumes "x < b" shows "DERIV \_inv x :> \_inv' x" proof - have "DERIV (ln \ (\x. (1 - x / real b))) x :> 1 / (1-x / real b) * (0 -1/b)" using assms b_min by (intro DERIV_chain DERIV_ln_divide DERIV_cdivide derivative_intros) auto hence "DERIV \_inv x :> (1 / (1-x / real b) * (-1/b)) / ln (1-1/real b)" unfolding comp_def \_inv_def by (intro DERIV_cdivide) auto thus ?thesis by (simp add:\_inv'_def algebra_simps) qed lemma accuracy_without_cutoff: - "measure \ {(f,g,h). \Y (f,g,h) - real X\ > \ * X \ s f < q_max} \ 1/2^4" + "measure \ {(f,g,h). \Y (f,g,h) - real X\ > \ * X \ s f < q_max} \ 1/2^4" (is "?L \ ?R") proof - have "?L \ measure \ {\. \E\<^sub>1 \ \ \E\<^sub>2 \ \ \E\<^sub>3 \ \ \E\<^sub>4 \}" proof (rule pmf_rev_mono) fix \ assume "\ \ set_pmf (sample_pmf \)" obtain f g h where \_def: "\ = (f,g,h)" by (metis prod_cases3) assume "\ \ {\. \ E\<^sub>1 \ \ \ E\<^sub>2 \ \ \ E\<^sub>3 \ \ \ E\<^sub>4 \}" hence assms: "E\<^sub>1 (f,g,h)" "E\<^sub>2 (f,g,h)" "E\<^sub>3 (f,g,h)" "E\<^sub>4 (f,g,h)" unfolding \_def by auto define I :: "real set" where "I = {0..59/90*b}" - have "p (f,g,h) \ \ (card (R f)) + \/12 * card (R f)" + have "p (f,g,h) \ \ (card (R f)) + \/12 * card (R f)" using assms(4) E\<^sub>4_def unfolding abs_le_iff by simp also have "... \ \(2/3*b) + 1/12* (2/3*b)" - using \_lt_1 R_bound[OF assms(1,2)] + using \_lt_1 R_bound[OF assms(1,2)] by (intro add_mono rho_mono mult_mono) auto also have "... \ 3/5 * b + 1/18*b" by (intro add_mono rho_two_thirds) auto also have "... \ 59/90 * b" by simp finally have "p (f,g,h) \ 59/90 * b" by simp hence p_in_I: "p (f,g,h) \ I" unfolding I_def by simp have "\ (card (R f)) \ \(2/3 * b)" using R_bound[OF assms(1,2)] by (intro rho_mono) auto also have "... \ 3/5 * b" using rho_two_thirds by simp also have "... \ b * 59/90" by simp finally have "\ (card (R f)) \ b * 59/90" by simp moreover have "(1 - 1 / real b) powr (real (card (R f))) \ 1 powr (real (card (R f)))" using b_min by (intro powr_mono2) auto hence "\ (card (R f)) \ 0" unfolding \_def by (intro mult_nonneg_nonneg) auto ultimately have "\ (card (R f)) \ I" unfolding I_def by simp moreover have "interval I" unfolding I_def interval_def by simp moreover have "59 / 90 * b < b" using b_min by simp hence "DERIV \_inv x :> \_inv' x" if "x \ I" for x using that I_def by (intro \_inv') simp ultimately obtain \ :: real where \_def: "\ \ I" "\_inv (p(f,g,h)) - \_inv (\ (card (R f))) = (p (f,g,h) - \(card (R f))) * \_inv' \" using p_in_I MVT_interval by blast have "\\_inv(p (f,g,h)) - card (R f)\ = \\_inv(p (f,g,h)) - \_inv(\(card (R f)))\" by (subst \_inverse) simp also have "... = \(p (f,g,h) - \ (card (R f)))\ * \\_inv' \ \" using \_def(2) abs_mult by simp also have "... \ \p (f,g,h) - \ (card (R f))\ * 4" using \_def(1) I_def by (intro mult_left_mono \_inv'_bound) auto - also have "... \ ( \/12 * card (R f)) * 4" + also have "... \ ( \/12 * card (R f)) * 4" using assms(4) E\<^sub>4_def by (intro mult_right_mono) auto - also have "... = \/3 * card (R f)" by simp - finally have b: "\\_inv(p (f,g,h)) - card (R f)\ \ \/3 * card (R f)" by simp + also have "... = \/3 * card (R f)" by simp + finally have b: "\\_inv(p (f,g,h)) - card (R f)\ \ \/3 * card (R f)" by simp have "\\_inv(p (f,g,h)) - X / 2 ^ (s f)\ \ \\_inv(p (f,g,h)) - card (R f)\ + \card (R f) - X / 2 ^ (s f)\" by simp - also have "... \ \/3 * card (R f) + \card (R f) - X / 2 ^ (s f)\" + also have "... \ \/3 * card (R f) + \card (R f) - X / 2 ^ (s f)\" by (intro add_mono b) auto - also have "... = \/3 * \X / 2 ^ (s f) + (card (R f) - X / 2 ^ (s f))\ + + also have "... = \/3 * \X / 2 ^ (s f) + (card (R f) - X / 2 ^ (s f))\ + \card (R f) - X / 2 ^ (s f)\" by simp - also have "... \ \/3 * (\X / 2 ^ (s f)\ + \card (R f) - X / 2 ^ (s f)\) + + also have "... \ \/3 * (\X / 2 ^ (s f)\ + \card (R f) - X / 2 ^ (s f)\) + \card (R f) - X / 2 ^ (s f)\" - using \_gt_0 by (intro mult_left_mono add_mono abs_triangle_ineq) auto - also have "... \ \/3 * \X / 2 ^ (s f)\ + (1+ \/3) * \card (R f) - X / 2 ^ (s f)\" - using \_gt_0 \_lt_1 by (simp add:algebra_simps) - also have "... \ \/3 * \X / 2 ^ s f\ + (4/3) * ( \ / 3 * real X / 2 ^ s f)" - using assms(2) \_gt_0 \_lt_1 + using \_gt_0 by (intro mult_left_mono add_mono abs_triangle_ineq) auto + also have "... \ \/3 * \X / 2 ^ (s f)\ + (1+ \/3) * \card (R f) - X / 2 ^ (s f)\" + using \_gt_0 \_lt_1 by (simp add:algebra_simps) + also have "... \ \/3 * \X / 2 ^ s f\ + (4/3) * ( \ / 3 * real X / 2 ^ s f)" + using assms(2) \_gt_0 \_lt_1 unfolding E\<^sub>2_def by (intro add_mono mult_mono) auto - also have "... = (7/9) * \ * real X / 2^s f" + also have "... = (7/9) * \ * real X / 2^s f" using X_ge_1 by (subst abs_of_nonneg) auto - also have "... \ 1 * \ * real X / 2^s f" - using \_gt_0 by (intro mult_mono divide_right_mono) auto - also have "... = \ * real X / 2^s f" by simp - finally have a:"\\_inv(p (f,g,h)) - X / 2 ^ (s f)\ \ \ * X / 2 ^ (s f)" + also have "... \ 1 * \ * real X / 2^s f" + using \_gt_0 by (intro mult_mono divide_right_mono) auto + also have "... = \ * real X / 2^s f" by simp + finally have a:"\\_inv(p (f,g,h)) - X / 2 ^ (s f)\ \ \ * X / 2 ^ (s f)" by simp have "\Y (f, g, h) - real X\ = \2 ^ (s f)\ * \\_inv(p (f,g,h)) - real X / 2 ^ (s f)\" unfolding Y_def by (subst abs_mult[symmetric]) (simp add:algebra_simps powr_add[symmetric]) - also have "... \ 2 ^ (s f) * (\ * X / 2 ^ (s f))" + also have "... \ 2 ^ (s f) * (\ * X / 2 ^ (s f))" by (intro mult_mono a) auto - also have "... = \ * X" + also have "... = \ * X" by (simp add:algebra_simps powr_add[symmetric]) - finally have "\Y (f, g, h) - real X\ \ \ * X" by simp + finally have "\Y (f, g, h) - real X\ \ \ * X" by simp moreover have "2 powr (\log 2 (real X)\ - t f) \ 2 powr b_exp" (is "?L1 \ ?R1") proof - have "?L1 \ 2 powr (1 + log 2 (real X)- t f)" by (intro powr_mono, linarith) auto also have "... = 2 powr 1 * 2 powr (log 2 (real X)) * 2 powr (- t f)" unfolding powr_add[symmetric] by simp also have "... = 2 * (2 powr (-t f) * X)" using X_ge_1 by simp also have "... \ 2 * (b/2)" using assms(1) unfolding E\<^sub>1_def by (intro mult_left_mono) auto also have "... = b" by simp also have "... = ?R1" unfolding b_def by (simp add: powr_realpow) finally show ?thesis by simp qed hence "\log 2 (real X)\ - t f \ real b_exp" unfolding not_less[symmetric] using powr_less_mono[where x="2"] by simp hence "s f \ q_max" unfolding s_def q_max_def by (intro nat_mono) auto - ultimately show "\ \ {(f, g, h). \ * X < \Y (f, g, h) - real X\ \ s f < q_max}" + ultimately show "\ \ {(f, g, h). \ * X < \Y (f, g, h) - real X\ \ s f < q_max}" unfolding \_def by auto qed also have "... \ measure \ {\. \E\<^sub>1 \ \ \E\<^sub>2 \ \ \E\<^sub>3 \} + measure \ {\. E\<^sub>1 \ \ E\<^sub>2 \ \ E\<^sub>3 \ \ \E\<^sub>4 \}" by (intro pmf_add) auto also have "... \ (measure \ {\. \E\<^sub>1 \ \ \E\<^sub>2 \} + measure \ {\. E\<^sub>1 \ \ E\<^sub>2 \ \ \E\<^sub>3 \}) + 1/2^6" by (intro add_mono e_4 pmf_add) auto also have "... \ ((measure \ {\. \E\<^sub>1 \} + measure \ {\. E\<^sub>1 \ \ \E\<^sub>2 \}) + 1/2^6) + 1/2^6" by (intro add_mono e_3 pmf_add) auto also have "... \ ((1/2^6 + 1/2^6) + 1/2^6) + 1/2^6" by (intro add_mono e_2 e_1) auto also have "... = ?R" by simp finally show ?thesis by simp qed end end diff --git a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Cutoff_Level.thy b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Cutoff_Level.thy --- a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Cutoff_Level.thy +++ b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Cutoff_Level.thy @@ -1,463 +1,463 @@ section \Cutoff Level\ text \This section verifies that the cutoff will be below @{term "q_max"} with high probability. The result will be needed in Section~\ref{sec:accuracy}, where it is shown that the estimates will be accurate for any cutoff below @{term "q_max"}.\ theory Distributed_Distinct_Elements_Cutoff_Level imports Distributed_Distinct_Elements_Accuracy_Without_Cutoff Distributed_Distinct_Elements_Tail_Bounds begin hide_const Quantum.Z unbundle intro_cong_syntax lemma mono_real_of_int: "mono real_of_int" unfolding mono_def by auto lemma Max_le_Sum: fixes f :: "'a \ int" assumes "finite A" assumes "\a. a \ A \ f a \ 0" shows "Max (insert 0 (f ` A)) \ (\a \A .f a)" (is "?L \ ?R") proof (cases "A\{}") case True have 0: "f a \ (\a \A .f a)" if "a \ A" for a using that assms by (intro member_le_sum) auto have "?L = max 0 (Max (f ` A))" using True assms(1) by (subst Max_insert) auto also have "... = Max (max 0 ` f ` A)" using assms True by (intro mono_Max_commute monoI) auto also have "... = Max (f ` A)" unfolding image_image using assms by (intro arg_cong[where f="Max"] image_cong) auto also have "... \ ?R" using 0 True assms(1) by (intro iffD2[OF Max_le_iff]) auto finally show ?thesis by simp next case False hence "A = {}" by simp then show ?thesis by simp qed context inner_algorithm_fix_A begin text \The following inequality is true for base e on the entire domain ($x > 0$). It is shown in @{thm [source] ln_add_one_self_le_self}. In the following it is established for base $2$, where it holds for $x \geq 1$.\ lemma log_2_estimate: assumes "x \ (1::real)" shows "log 2 (1+x) \ x" proof - define f where "f x = x - log 2 (1+ x)" for x :: real define f' where "f' x = 1 - 1/((x+1)*ln 2)" for x :: real have 0:"(f has_real_derivative (f' x)) (at x)" if "x > 0" for x unfolding f_def f'_def using that by (auto intro!: derivative_eq_intros) have "f' x \ 0" if "1 \ x" for x :: real proof - have "(1::real) \ 2*ln 2" by (approximation 5) also have "... \ (x+1)*ln 2" using that by (intro mult_right_mono) auto finally have "1 \ (x+1)*ln 2" by simp hence "1/((x+1)*ln 2) \ 1" by simp thus ?thesis unfolding f'_def by simp qed hence "\y. (f has_real_derivative y) (at x) \ 0 \ y" if "x \ 1" for x :: real using that order_less_le_trans[OF exp_gt_zero] by (intro exI[where x="f' x"] conjI 0) auto hence "f 1 \ f x" by (intro DERIV_nonneg_imp_nondecreasing[OF assms]) auto thus "?thesis" unfolding f_def by simp qed lemma cutoff_eq_7: "real X * 2 powr (-real q_max) / b \ 1" proof - have "real X = 2 powr (log 2 X)" using X_ge_1 by (intro powr_log_cancel[symmetric]) auto also have "... \ 2 powr (nat \log 2 X\)" by (intro powr_mono) linarith+ also have "... = 2 ^ (nat \log 2 X\)" by (subst powr_realpow) auto also have "... = real (2 ^ (nat \log 2 (real X)\))" by simp also have "... \ real (2 ^ (b_exp + nat (\log 2 (real X)\ - int b_exp)))" by (intro Nat.of_nat_mono power_increasing) linarith+ also have "... = b * 2^q_max" unfolding q_max_def b_def by (simp add: power_add) finally have "real X \ b * 2 ^ q_max" by simp thus ?thesis using b_min unfolding powr_minus inverse_eq_divide by (simp add:field_simps powr_realpow) qed lemma cutoff_eq_6: fixes k assumes "a \ A" shows " (\f. real_of_int (max 0 (int (f a) - int k)) \\\<^sub>1) \ 2 powr (-real k)" (is "?L \ ?R") proof (cases "k \ n_exp - 1") case True have a_le_n: "a < n" using assms A_range by auto have "?L = (\x. real_of_int (max 0 (int x - k)) \map_pmf (\x. x a) \\<^sub>1)" by simp also have "... = (\x. real_of_int (max 0 (int x - k)) \(\ n_exp))" unfolding \\<^sub>1.single[OF a_le_n] by simp also have "... = (\x. max 0 (real x - real k) \(\ n_exp))" unfolding max_of_mono[OF mono_real_of_int,symmetric] by simp also have "... = (\x\n_exp. max 0 (real x - real k) * pmf (\ n_exp) x)" using \_range unfolding sample_space_alt[OF \_sample_space] by (intro integral_measure_pmf_real) auto also have "... = (\x=k+1..n_exp. (real x - real k) * pmf (\ n_exp) x)" by (intro sum.mono_neutral_cong_right) auto also have "... = (\x=k+1..n_exp. (real x - real k) * measure (\ n_exp) {x})" unfolding measure_pmf_single by simp also have "... = (\x=k+1..n_exp. (real x-real k)*(measure (\ n_exp) ({\. \\x}-{\. \\(x+1)})))" by (intro sum.cong arg_cong2[where f="(*)"] measure_pmf_cong) auto also have "... = (\x=k+1..n_exp. (real x-real k)* (measure (\ n_exp) {\. \\x} - measure (\ n_exp) {\. \\(x+1)}))" by (intro sum.cong arg_cong2[where f="(*)"] measure_Diff) auto also have "... = (\x=k+1..n_exp. (real x - real k) * (1/2^x - of_bool(x+1\n_exp)/2^(x+1)))" unfolding \_prob by (intro_cong "[\\<^sub>2 (*), \\<^sub>2 (-), \\<^sub>2 (/)]" more:sum.cong) auto also have "... = (\x=k+1..n_exp. (real x-k)/2^x) - (\x=k+1..n_exp. (real x-k)* of_bool(x+1\n_exp)/2^(x+1))" by (simp add:algebra_simps sum_subtractf) also have "...=(\x=k+1..n_exp. (real x-k)/2^x)-(\x=k+1..n_exp-1. (real x-k)/2^(x+1))" by (intro arg_cong2[where f="(-)"] refl sum.mono_neutral_cong_right) auto also have "...=(\x=k+1..(n_exp-1)+1. (real x-k)/2^x)-(\x=k+1..n_exp-1. (real x-k)/2^(x+1))" using n_exp_gt_0 by (intro arg_cong2[where f="(-)"] refl sum.cong) auto also have "...= (\x\insert k {k+1..n_exp-1}. (real (x+1)-k)/2^(x+1))- (\x=k+1..n_exp-1. (real x-k)/2^(x+1))" unfolding sum.shift_bounds_cl_nat_ivl using True by (intro arg_cong2[where f="(-)"] sum.cong) auto also have "... = 1/2^(k+1)+(\x=k+1..n_exp-1. (real (x+1)-k)/2^(x+1)- (real x-k)/2^(x+1))" by (subst sum.insert) (auto simp add:sum_subtractf) also have "... = 1/2^(k+1)+(\x=k+1..n_exp-1. (1/2^(x+1)))" by (intro arg_cong2[where f="(+)"] sum.cong refl) (simp add:field_simps) also have "... = (\x\insert k {k+1..n_exp-1}. (1/2^(x+1)))" by (subst sum.insert) auto also have "... = (\x=0+k..(n_exp-1-k)+k. 1/2^(x+1))" using True by (intro sum.cong) auto also have "... = (\xx (1/2)^(k+1) * 2 * (1-0)" by (intro mult_left_mono diff_mono) auto also have "... = (1/2)^k" unfolding power_add by simp also have "... = ?R" unfolding powr_minus by (simp add:powr_realpow inverse_eq_divide power_divide) finally show ?thesis by simp next case False hence k_ge_n_exp: "k \ n_exp" by simp have a_lt_n: "a < n" using assms A_range by auto have "?L = (\x. real_of_int (max 0 (int x - k)) \map_pmf (\x. x a) \\<^sub>1)" by simp also have "... = (\x. real_of_int (max 0 (int x - k)) \(\ n_exp))" unfolding \\<^sub>1.single[OF a_lt_n] by simp also have "... = (\x. real_of_int 0 \(\ n_exp))" using \_range k_ge_n_exp unfolding sample_space_alt[OF \_sample_space] by (intro integral_cong_AE AE_pmfI iffD2[OF of_int_eq_iff] max_absorb1) force+ also have "... = 0" by simp finally show ?thesis by simp qed lemma cutoff_eq_5: assumes "x \ (-1 :: real)" shows "real_of_int \log 2 (x+2)\ \ (real c+2) + max (x - 2^c) 0" (is "?L \ ?R") proof - have 0: "1 \ 2 ^ 1 * ln (2::real)" by (approximation 5) consider (a) "c = 0 \ x \ 2^c+1" | (b) "c > 0 \ x \ 2^c+1" | (c) "x \ 2^c+1" by linarith hence "log 2 (x+2) \ ?R" proof (cases) case a have "log 2 (x+2) = log 2 (1+(x+1))" by (simp add:algebra_simps) also have "... \ x+1" using a by (intro log_2_estimate) auto also have "... = ?R" using a by auto finally show ?thesis by simp next case b have "0 < 0 + (1::real)" by simp also have "... \ 2^c+(1::real)" by (intro add_mono) auto also have "... \ x" using b by simp finally have x_gt_0: "x > 0" by simp have "log 2 (x+2) = log 2 ((x+2)/2^c) + c" using x_gt_0 by (subst log_divide) auto also have "... = log 2 (1+(x+2-2^c)/2^c) + c" by (simp add:divide_simps) also have "... \ (x+2-2^c)/2^c / ln 2 + c" using b unfolding log_def by (intro add_mono divide_right_mono ln_add_one_self_le_self divide_nonneg_pos) auto also have "... = (x+2-2^c)/(2^c*ln 2) + c" by simp also have "... \ (x+2-2^c)/(2^1*ln 2)+c" using b by (intro add_mono divide_left_mono mult_right_mono power_increasing) simp_all also have "... \ (x+2-2^c)/1 + c" using b by (intro add_mono divide_left_mono 0) auto also have "... \ (c+2) + max (x - 2^c) 0" using b by simp finally show ?thesis by simp next case c hence "log 2 (x+2) \ log 2 ((2^c+1)+2)" using assms by (intro log_mono add_mono) auto also have "... = log 2 (2^c*(1+3/2^c))" by (simp add:algebra_simps) also have "... = c + log 2 (1+3/2^c)" by (subst log_mult) (auto intro:add_pos_nonneg) also have "... \ c + log 2 (1+3/2^0)" by (intro add_mono log_mono divide_left_mono power_increasing add_pos_nonneg) auto also have "... = c + log 2 (2*2)" by simp also have "... = real c + 2" by (subst log_mult) auto also have "... \ (c+2) + max (x - 2^c) 0" by simp finally show ?thesis by simp qed moreover have "\log 2 (x+2)\ \ log 2 (x+2)" by simp ultimately show ?thesis using order_trans by blast qed lemma cutoff_level: - "measure \ {\. q \ A > q_max} \ \/2" (is "?L \ ?R") + "measure \ {\. q \ A > q_max} \ \/2" (is "?L \ ?R") proof - have C\<^sub>1_est: "C\<^sub>1 * l \ 30 * real l" unfolding C\<^sub>1_def by (intro mult_right_mono of_nat_0_le_iff) (approximation 10) define Z where "Z \ = (\jlog 2 (of_int (max (\\<^sub>1 \ A q_max j) (-1)) + 2)\)" for \ define V where "V \ = Z \ / real b - 3" for \ have 2:"Z \ \ real b*(real c+2) + of_int (\a\A. max 0 (int (fst \ a) - q_max -2^c))" (is "?L1 \ ?R1") if "\ \ sample_set \" for c \ proof - obtain f g h where \_def: "\ = (f,g,h)" using prod_cases3 by blast have \_range: "(f,g,h) \ sample_set \" using that unfolding \_def by simp have "- 1 - 2^c \ -1-(1::real)" by (intro diff_mono) auto also have "... \ 0" by simp finally have "- 1 - 2 ^ c \ (0::real)" by simp hence aux3: "max (-1-2^c) 0 = (0::real)" by (intro max_absorb2) have "- 1 - int q_max - 2 ^ c \ -1 - 0 - 1" by (intro diff_mono) auto also have "... \ 0" by simp finally have "- 1 - int q_max - 2 ^ c \ 0" by simp hence aux3_2: "max 0 (- 1 - int q_max - 2 ^ c) = 0" by (intro max_absorb1) have "?L1 \ (\j\<^sub>1 \ A q_max j) (- 1)) - 2^c) 0)" unfolding Z_def by (intro sum_mono cutoff_eq_5) auto also have "... = (\j\<^sub>0 \ A j - q_max - 2^c) 0)" unfolding \\<^sub>1_def max_of_mono[OF mono_real_of_int,symmetric] by (intro_cong "[\\<^sub>2 (+)]" more:sum.cong) (simp add:max_diff_distrib_left max.assoc aux3) also have "... = real b * (real c + 2) + of_int (\j A \ h (g a) = j})-q_max - 2^c)))" unfolding \_def by (simp add:max.commute) also have "... = real b * (real c + 2) + of_int (\jx. x-q_max-2^c)`(insert(-1){int (f a) |a. a \ A\h(g a)=j}))))" using fin_A by (intro_cong "[\\<^sub>2 (+), \\<^sub>1 of_int, \\<^sub>2 max]" more:sum.cong mono_Max_commute) (auto simp:monoI) also have "... = real b * (real c + 2) + of_int(\j A \ h (g a) = j})))" by (intro_cong "[\\<^sub>2 (+), \\<^sub>1 of_int, \\<^sub>2 max, \\<^sub>1 Max]" more:sum.cong) auto also have "... = real b * (real c + 2) + of_int (\j A \ h (g a) = j})))" using fin_A by (intro_cong "[\\<^sub>2 (+), \\<^sub>1 of_int]" more:sum.cong mono_Max_commute) (auto simp add:monoI setcompr_eq_image) also have "... = real b * (real c + 2) + of_int (\j A \ h (g a) = j}))" using aux3_2 by (intro_cong "[\\<^sub>2 (+), \\<^sub>1 of_int, \\<^sub>1 Max]" more:sum.cong) (simp add:setcompr_eq_image image_image) also have "... \ b*(real c+2)+ of_int(\ja|a\A\h(g(a))=j. max 0(int(f a)-q_max-2^c)))" using fin_A Max_le_Sum unfolding setcompr_eq_image by (intro add_mono iffD2[OF of_int_le_iff] sum_mono Max_le_Sum) (simp_all) also have "... = real b*(real c+2)+ of_int(\a\(\j\{..A\ h(g(a)) = j}). max 0(int(f a)-q_max-2^c))" using fin_A by (intro_cong "[\\<^sub>2 (+), \\<^sub>1 of_int]" more:sum.UNION_disjoint[symmetric]) auto also have "... = real b*(real c+2) + of_int(\a\A. max 0(int(f a)-q_max-2^c))" using h_range[OF \_range] by (intro_cong "[\\<^sub>2 (+), \\<^sub>1 of_int]" more:sum.cong) auto also have "... = ?R1" unfolding \_def by simp finally show ?thesis by simp qed have 1: "measure \ {\. real c \ V \} \ 2 powr (- (2^c))" (is "?L1 \ ?R1") for c proof - have "?L1 = measure \ {\. real b * (real c + 3) \ Z \}" unfolding V_def using b_min by (intro measure_pmf_cong) (simp add:field_simps) also have "... \ measure \ {\. real b*(real c+3)\ real b*(real c+2)+ of_int (\a\A. max 0 (int (fst \ a)-q_max -2^c))}" using 2 order_trans unfolding sample_space_alt[OF sample_space_\] by (intro pmf_mono) blast also have "... = measure \ {\. real b \ (\a\A. of_int (max 0 (int (fst \ a) -q_max -2^c)))}" by (intro measure_pmf_cong) (simp add:algebra_simps) also have "... \ (\\. (\a\A. of_int (max 0 (int (fst \ a) -q_max -2^c))) \\)/real b" using b_min sample_space_\ by (intro pmf_markov sum_nonneg) simp_all also have "... = (\a\A. (\\. of_int (max 0 (int (fst \ a) -q_max -2^c)) \\))/real b" using sample_space_\ by (intro_cong "[\\<^sub>2(/)]" more:Bochner_Integration.integral_sum) simp also have "... = (\a\A. (\f. of_int (max 0 (int (f a)-q_max -2^c)) \(map_pmf fst \)))/real b" by simp also have "... = (\a\A. (\f. of_int (max 0 (int (f a) - (q_max +2^c))) \\\<^sub>1))/real b" unfolding sample_pmf_\ map_fst_pair_pmf by (simp add:algebra_simps) also have "... \ (\a\A. 2 powr -real (q_max + 2^c))/real b" using b_min by (intro sum_mono divide_right_mono cutoff_eq_6) auto also have "... = real X * 2 powr (- real q_max + (- (2 ^ c))) / real b" unfolding X_def by simp also have "... = (real X * 2 powr (-real q_max) / b) * 2 powr (-(2^c))" unfolding powr_add by (simp add:algebra_simps) also have "... \ 1 * 2 powr (-(2^c))" using cutoff_eq_7 by (intro mult_right_mono) auto finally show ?thesis by simp qed have 0: "measure \ {\. x \ V \} \ exp (- x * ln x ^ 3)" (is "?L1 \ ?R1") if "x \ 20" for x proof - define c where "c = nat \x\" have "x * ln x^3 \ exp (x * ln 2) * ln 2/2" if "x \ 150" for x::real proof - have aux_aux_0: "x^4 \ 0" by simp have "x * ln x^3 \ x * x^3" using that by (intro mult_left_mono power_mono ln_bound) auto also have "... = x^4 * 1" by (simp add:numeral_eq_Suc) also have "... \ x^4 * ((ln 2 / 10)^4 * (150 * (ln 2 / 10))^6 * (ln 2/2))" by (intro mult_left_mono aux_aux_0) (approximation 8) also have "... = (x * (ln 2 / 10))^4 * (150 * (ln 2 / 10))^6 * (ln 2/2)" unfolding power_mult_distrib by (simp add:algebra_simps) also have "... \ (x * (ln 2 / 10))^4 * (x * (ln 2 / 10))^6 * (ln 2/2)" by (intro mult_right_mono mult_left_mono power_mono that) auto also have "... = (0+x * (ln 2 / 10))^10 * (ln 2/2)" unfolding power_add[symmetric] by simp also have "... \ (1+x * ln 2 / 10)^10 * (ln 2/2)" using that by (intro mult_right_mono power_mono add_mono) auto also have "... \ exp (x * ln 2 / 10)^10 * (ln 2/2)" using that by (intro mult_right_mono power_mono exp_ge_add_one_self) auto also have "... = exp (x * ln 2) * (ln 2/2)" unfolding exp_of_nat_mult[symmetric] by simp finally show ?thesis by simp qed moreover have "x * ln x^3 \ exp (x * ln 2) * ln 2/2" if "x \ {20..150}" using that by (approximation 10 splitting: x=1) ultimately have "x * ln x^3 \ exp (x * ln 2) * ln 2/2" using that by fastforce also have "... = 2 powr (x-1) * ln 2" unfolding powr_diff unfolding powr_def by simp also have "... \ 2 powr c * ln 2" unfolding c_def using that by (intro mult_right_mono powr_mono) auto also have "... = 2^c * ln 2" using powr_realpow by simp finally have aux0: "x * ln x^3 \ 2^c * ln 2" by simp have "real c \ x" using that unfolding c_def by linarith hence "?L1 \ measure \ {\. real c \ V \}" by (intro pmf_mono) auto also have "... \ 2 powr (-(2^c))" by (intro 1) also have "... = exp (- (2 ^ c * ln 2))" by (simp add:powr_def) also have "... \ exp (- (x *ln x^3))" using aux0 by (intro iffD2[OF exp_le_cancel_iff]) auto also have "... = ?R1" by simp finally show ?thesis by simp qed have "?L \ measure \ {\. is_too_large (\\<^sub>2 \ A q_max)}" using lt_s_too_large by (intro pmf_mono) (simp del:is_too_large.simps) also have "... = measure \ {\. (\(i,j)\{..{..log 2 (of_int (max (\\<^sub>2 \ A q_max i j) (-1)) + 2)\) > C\<^sub>5 * b *l}" by simp also have "... = measure \ {\. real_of_int (\(i,j)\{..{..log 2 (of_int (max (\\<^sub>2 \ A q_max i j) (-1)) + 2)\) > of_int (C\<^sub>5 * b * l)}" unfolding of_int_less_iff by simp also have "... = measure \ {\. real_of_int C\<^sub>5 * real b * real l < of_int (\x\{.. {..log 2 (real_of_int (\\<^sub>1 (\ (fst x)) A q_max (snd x)) + 2)\)}" by (intro_cong "[\\<^sub>2 measure, \\<^sub>1 Collect, \\<^sub>1 of_int, \\<^sub>2 (<)]" more:ext sum.cong) (auto simp add:case_prod_beta \\<^sub>2_def \\<^sub>1_def) also have "... = measure \ {\. (\i i)) > of_int C\<^sub>5 * real b * real l}" unfolding Z_def sum.cartesian_product \\<^sub>1_def by (simp add:case_prod_beta) also have "... = measure \ {\. (\i i) + 3) > of_int C\<^sub>5 * real l}" unfolding V_def using b_min by (intro measure_pmf_cong) (simp add:sum_divide_distrib[symmetric] field_simps sum.distrib) also have "... = measure \ {\. (\i i)) > of_int (C\<^sub>5-3) * real l}" by (simp add:sum.distrib algebra_simps) also have "... \ measure \ {\. (\i i)) \ C\<^sub>1 * real l}" unfolding C\<^sub>5_def using C\<^sub>1_est by (intro pmf_mono) auto also have "... \ exp (- real l)" by (intro \.deviation_bound l_gt_0 0) (simp_all add: \_def) - also have "... \ exp (- (C\<^sub>6 * ln (2 / \)))" + also have "... \ exp (- (C\<^sub>6 * ln (2 / \)))" using l_lbound by (intro iffD2[OF exp_le_cancel_iff]) auto - also have "... \ exp (- (1 * ln (2 / \)))" - unfolding C\<^sub>6_def using \_gt_0 \_lt_1 + also have "... \ exp (- (1 * ln (2 / \)))" + unfolding C\<^sub>6_def using \_gt_0 \_lt_1 by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le mult_right_mono ln_ge_zero) auto - also have "... = exp ( ln ( \ / 2))" - using \_gt_0 by (simp add: ln_div) - also have "... = \/2" - using \_gt_0 by simp + also have "... = exp ( ln ( \ / 2))" + using \_gt_0 by (simp add: ln_div) + also have "... = \/2" + using \_gt_0 by simp finally show ?thesis by simp qed end unbundle no_intro_cong_syntax end \ No newline at end of file diff --git a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Inner_Algorithm.thy b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Inner_Algorithm.thy --- a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Inner_Algorithm.thy +++ b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Inner_Algorithm.thy @@ -1,1104 +1,1104 @@ section \Inner Algorithm\label{sec:inner_algorithm}\ text \This section introduces the inner algorithm (as mentioned it is already a solution to the cardinality estimation with the caveat that, if $\varepsilon$ is too small it requires to much space. The outer algorithm in Section~\ref{sec:outer_algorithm} resolved this problem. The algorithm makes use of the balls and bins model, more precisely, the fact that the number of hit bins can be used to estimate the number of balls thrown (even if there are collusions). I.e. it assigns each universe element to a bin using a $k$-wise independent hash function. Then it counts the number of bins hit. This strategy however would only work if the number of balls is roughly equal to the number of bins, to remedy that the algorithm performs an adaptive sub-sampling strategy. This works by assigning each universe element a level (using a second hash function) with a geometric distribution. The algorithm then selects a level that is appropriate based on a rough estimate obtained using the maximum level in the bins. To save space the algorithm drops information about small levels, whenever the space usage would be too high otherwise. This level will be called the cutoff-level. This is okey as long as the cutoff level is not larger than the sub-sampling threshold. A lot of the complexity in the proof is devoted to verifying that the cutoff-level will not cross it, it works by defining a third value @{term "s\<^sub>M"} that is both an upper bound for the cutoff level and a lower bound for the subsampling threshold simultaneously with high probability.\ theory Distributed_Distinct_Elements_Inner_Algorithm imports Pseudorandom_Combinators Distributed_Distinct_Elements_Preliminary Distributed_Distinct_Elements_Balls_and_Bins Distributed_Distinct_Elements_Tail_Bounds Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators begin unbundle intro_cong_syntax hide_const Abstract_Rewriting.restrict definition C\<^sub>4 :: real where "C\<^sub>4 = 3^2*2^23" definition C\<^sub>5 :: int where "C\<^sub>5 = 33" definition C\<^sub>6 :: real where "C\<^sub>6 = 4" definition C\<^sub>7 :: nat where "C\<^sub>7 = 2^5" locale inner_algorithm = fixes n :: nat - fixes \ :: real fixes \ :: real + fixes \ :: real assumes n_gt_0: "n > 0" + assumes \_gt_0: "\ > 0" and \_lt_1: "\ < 1" assumes \_gt_0: "\ > 0" and \_lt_1: "\ < 1" - assumes \_gt_0: "\ > 0" and \_lt_1: "\ < 1" begin -definition b_exp where "b_exp = nat \log 2 (C\<^sub>4 / \^2)\" +definition b_exp where "b_exp = nat \log 2 (C\<^sub>4 / \^2)\" definition b :: nat where "b = 2^b_exp" -definition l where "l = nat \C\<^sub>6 * ln (2/ \)\" +definition l where "l = nat \C\<^sub>6 * ln (2/ \)\" definition k where "k = nat \C\<^sub>2*ln b + C\<^sub>3\" definition \ :: real where "\ = min (1/16) (exp (-l * ln l^3))" definition \ :: "real \ real" where "\ x = b * (1 - (1-1/b) powr x)" definition \_inv :: "real \ real" where "\_inv x = ln (1-x/b) / ln (1-1/b)" -lemma l_lbound: "C\<^sub>6 * ln (2 / \) \ l" +lemma l_lbound: "C\<^sub>6 * ln (2 / \) \ l" unfolding l_def by linarith lemma k_min: "C\<^sub>2 * ln (real b) + C\<^sub>3 \ real k" unfolding k_def by linarith lemma \_gt_0: "\ > 0" unfolding \_def min_less_iff_conj by auto lemma \_le_1: "\ \ 1" unfolding \_def by auto lemma l_gt_0: "l > 0" proof - - have "0 < C\<^sub>6 * ln (2 / \)" - unfolding C\<^sub>6_def using \_gt_0 \_lt_1 + have "0 < C\<^sub>6 * ln (2 / \)" + unfolding C\<^sub>6_def using \_gt_0 \_lt_1 by (intro Rings.mult_pos_pos ln_gt_zero) auto also have "... \ l" by (intro l_lbound) finally show ?thesis by simp qed -lemma l_ubound: "l \ C\<^sub>6 * ln(1 / \)+C\<^sub>6*ln 2 + 1" +lemma l_ubound: "l \ C\<^sub>6 * ln(1 / \)+C\<^sub>6*ln 2 + 1" proof - - have "l = of_int \C\<^sub>6 * ln (2/ \)\" + have "l = of_int \C\<^sub>6 * ln (2/ \)\" using l_gt_0 unfolding l_def by (intro of_nat_nat) simp - also have "... \ C\<^sub>6 * ln (1/ \*2)+1" + also have "... \ C\<^sub>6 * ln (1/ \*2)+1" by simp - also have "... = C\<^sub>6 * ln (1/ \)+C\<^sub>6 * ln 2+1" - using \_gt_0 \_lt_1 + also have "... = C\<^sub>6 * ln (1/ \)+C\<^sub>6 * ln 2+1" + using \_gt_0 \_lt_1 by (subst ln_mult) (auto simp add:algebra_simps) finally show ?thesis by simp qed lemma b_exp_ge_26: "b_exp \ 26" proof - have "2 powr 25 < C\<^sub>4 / 1 " unfolding C\<^sub>4_def by simp - also have "... \ C\<^sub>4 / \^2" - using \_gt_0 \_lt_1 unfolding C\<^sub>4_def + also have "... \ C\<^sub>4 / \^2" + using \_gt_0 \_lt_1 unfolding C\<^sub>4_def by (intro divide_left_mono power_le_one) auto - finally have "2 powr 25 < C\<^sub>4 / \^2" by simp - hence "log 2 (C\<^sub>4 / \^2) > 25" - using \_gt_0 unfolding C\<^sub>4_def + finally have "2 powr 25 < C\<^sub>4 / \^2" by simp + hence "log 2 (C\<^sub>4 / \^2) > 25" + using \_gt_0 unfolding C\<^sub>4_def by (intro iffD2[OF less_log_iff] divide_pos_pos zero_less_power) auto - hence "\log 2 (C\<^sub>4 / \^2)\ \ 26" by simp + hence "\log 2 (C\<^sub>4 / \^2)\ \ 26" by simp thus ?thesis unfolding b_exp_def by linarith qed lemma b_min: "b \ 2^26" unfolding b_def by (meson b_exp_ge_26 nat_power_less_imp_less not_less power_eq_0_iff power_zero_numeral) lemma k_gt_0: "k > 0" proof - have "(0::real) < 7.5 * 0 + 16" by simp also have "... \ 7.5 * ln(real b) + 16" using b_min by (intro add_mono mult_left_mono ln_ge_zero) auto finally have "0 < real k" using k_min unfolding C\<^sub>2_def C\<^sub>3_def by simp thus ?thesis by simp qed lemma b_ne: "{.. {}" proof - have "0 \ {0..4 / \^2 \ real b" +lemma b_lower_bound: "C\<^sub>4 / \^2 \ real b" proof - - have "C\<^sub>4 / \^2 = 2 powr (log 2 (C\<^sub>4 / \^2))" - using \_gt_0 unfolding C\<^sub>4_def by (intro powr_log_cancel[symmetric] divide_pos_pos) auto - also have "... \ 2 powr (nat \log 2 (C\<^sub>4 / \^2)\)" + have "C\<^sub>4 / \^2 = 2 powr (log 2 (C\<^sub>4 / \^2))" + using \_gt_0 unfolding C\<^sub>4_def by (intro powr_log_cancel[symmetric] divide_pos_pos) auto + also have "... \ 2 powr (nat \log 2 (C\<^sub>4 / \^2)\)" by (intro powr_mono of_nat_ceiling) simp also have "... = real b" unfolding b_def b_exp_def by (simp add:powr_realpow) finally show ?thesis by simp qed definition n_exp where "n_exp = max (nat \log 2 n\) 1" lemma n_exp_gt_0: "n_exp > 0" unfolding n_exp_def by simp abbreviation \\<^sub>1 where "\\<^sub>1 \ \ 2 n (\ n_exp)" abbreviation \\<^sub>2 where "\\<^sub>2 \ \ 2 n [C\<^sub>7*b\<^sup>2]\<^sub>S" abbreviation \\<^sub>3 where "\\<^sub>3 \ \ k (C\<^sub>7*b\<^sup>2) [b]\<^sub>S" definition \ where "\ = \\<^sub>1 \\<^sub>S \\<^sub>2 \\<^sub>S \\<^sub>3" abbreviation \ where "\ \ \ l \ \" type_synonym state = "(nat \ nat \ int) \ (nat)" fun is_too_large :: "(nat \ nat \ int) \ bool" where "is_too_large B = ((\ (i,j) \ {.. {..log 2 (max (B i j) (-1) + 2)\) > C\<^sub>5 * b * l)" fun compress_step :: "state \ state" where "compress_step (B,q) = (\ i j. max (B i j - 1) (-1), q+1)" function compress :: "state \ state" where "compress (B,q) = ( if is_too_large B then (compress (compress_step (B,q))) else (B,q))" by auto fun compress_termination :: "state \ nat" where "compress_termination (B,q) = (\ (i,j) \ {.. {.. nat (B i j + 1)" for i j by simp assume "\ compress_termination (compress_step (B, q)) < compress_termination (B, q)" hence "(\ (i,j) \ ?I. nat (B i j + 1)) \ (\ (i,j) \ ?I. nat (max (B i j - 1) (-1) + 1))" by simp moreover have "(\ (i,j) \ ?I. nat (B i j + 1)) \ (\ (i,j) \ ?I. nat (max (B i j - 1) (-1) + 1))" by (intro sum_mono) auto ultimately have b: "(\ (i,j) \ ?I. nat (max (B i j - 1) (-1) + 1)) = (\ (i,j) \ ?I. nat (B i j + 1))" using order_antisym by simp have "nat (B i j + 1) = nat (max (B i j - 1) (-1) + 1)" if "(i,j) \ ?I" for i j using sum_mono_inv[OF b] that a by auto hence "max (B i j) (-1) = -1" if "(i,j) \ ?I" for i j using that by fastforce hence "(\(i,j) \ ?I. \log 2 (max (B i j) (-1) + 2)\) = (\(i,j) \ ?I. 0)" by (intro sum.cong, auto) also have "... = 0" by simp also have "... \ C\<^sub>5 * b * l" unfolding C\<^sub>5_def by simp finally have "\ is_too_large B" by simp thus "False" using assms by simp qed termination compress using measure_def compress_termination by (relation "Wellfounded.measure (compress_termination)", auto) fun merge1 :: "state \ state \ state" where "merge1 (B1,q\<^sub>1) (B2, q\<^sub>2) = ( let q = max q\<^sub>1 q\<^sub>2 in (\ i j. max (B1 i j + q\<^sub>1 - q) (B2 i j + q\<^sub>2 - q), q))" fun merge :: "state \ state \ state" where "merge x y = compress (merge1 x y)" type_synonym seed = "nat \ (nat \ nat) \ (nat \ nat) \ (nat \ nat)" fun single1 :: "seed \ nat \ state" where "single1 \ x = (\ i j. let (f,g,h) = \ i in ( if h (g x) = j \ i < l then int (f x) else (-1)), 0)" fun single :: "seed \ nat \ state" where "single \ x = compress (single1 \ x)" fun estimate1 :: "state \ nat \ real" where "estimate1 (B,q) i = ( let s = max 0 (Max ((B i) ` {..log 2 b\ + 9); p = card { j. j \ {.. B i j + q \ s } in 2 powr s * ln (1-p/b) / ln(1-1/b))" fun estimate :: "state \ real" where "estimate x = median l (estimate1 x)" subsection \History Independence\ fun \\<^sub>0 :: "((nat \ nat) \ (nat \ nat) \ (nat \ nat)) \ nat set \ nat \ int" where "\\<^sub>0 (f,g,h) A j = Max ({ int (f a) | a . a \ A \ h (g a) = j } \ {-1}) " definition \\<^sub>1 :: "((nat \ nat) \ (nat \ nat) \ (nat \ nat)) \ nat set \ nat \ nat \ int" where "\\<^sub>1 \ A q j = max (\\<^sub>0 \ A j - q) (-1)" definition \\<^sub>2 :: "seed \ nat set \ nat \ nat \ nat \ int" where "\\<^sub>2 \ A q i j = (if i < l then \\<^sub>1 (\ i) A q j else (-1))" definition \\<^sub>3 :: "seed \ nat set \ nat \ state" where "\\<^sub>3 \ A q = (\\<^sub>2 \ A q, q)" definition q :: "seed \ nat set \ nat" where "q \ A = (LEAST q . \(is_too_large (\\<^sub>2 \ A q)))" definition \ :: "seed \ nat set \ state" where "\ \ A = \\<^sub>3 \ A (q \ A)" lemma \\<^sub>2_step: "\\<^sub>2 \ A (x+y) = (\i j. max (\\<^sub>2 \ A x i j - y) (- 1))" by (intro ext) (auto simp add:\\<^sub>2_def \\<^sub>1_def) lemma \\<^sub>3_step: "compress_step (\\<^sub>3 \ A x) = \\<^sub>3 \ A (x+1)" unfolding \\<^sub>3_def using \\<^sub>2_step[where y="1"] by simp sublocale \\<^sub>1: hash_sample_space 2 n 2 n_exp "\ n_exp" using n_exp_gt_0 unfolding hash_sample_space_def \_def by auto sublocale \\<^sub>2: hash_sample_space 2 n 2 "5 + b_exp*2" "[(C\<^sub>7*b\<^sup>2)]\<^sub>S" unfolding hash_sample_space_def nat_sample_space_def b_def C\<^sub>7_def by (auto simp add:power_mult power_add) sublocale \\<^sub>3: hash_sample_space k "C\<^sub>7*b\<^sup>2" 2 "b_exp" "[b]\<^sub>S" unfolding hash_sample_space_def b_def nat_sample_space_def using k_gt_0 b_exp_ge_26 by auto lemma sample_pmf_\: "sample_pmf \ = pair_pmf \\<^sub>1 (pair_pmf \\<^sub>2 \\<^sub>3)" unfolding \_def using \\<^sub>1.sample_space \\<^sub>2.sample_space \\<^sub>3.sample_space by (simp add:prod_sample_pmf) lemma sample_set_\: "sample_set \ = sample_set \\<^sub>1 \ sample_set \\<^sub>2 \ sample_set \\<^sub>3" using \\<^sub>1.sample_space \\<^sub>2.sample_space \\<^sub>3.sample_space unfolding \_def by (simp add: prod_sample_set) lemma sample_space_\: "sample_space \" unfolding \_def using \\<^sub>1.sample_space \\<^sub>2.sample_space \\<^sub>3.sample_space by simp lemma f_range: assumes "(f,g,h) \ sample_set \" shows "f x \ n_exp" proof - have "f \ sample_set \\<^sub>1" using sample_set_\ assms by auto then obtain i where f_def:"f = select \\<^sub>1 i" unfolding sample_set_def by auto hence "f x \ sample_set (\ n_exp)" using \\<^sub>1.range by auto also have "... \ {..n_exp}" by (intro \_range) finally have "f x \ {..n_exp}" by simp thus ?thesis by simp qed lemma g_range_1: assumes "g \ sample_set \\<^sub>2" shows "g x < C\<^sub>7*b^2" proof - obtain i where f_def:"g = select (\ 2 n [(C\<^sub>7*b\<^sup>2)]\<^sub>S) i" using assms unfolding sample_set_def by auto hence "range g \ sample_set ([(C\<^sub>7*b\<^sup>2)]\<^sub>S)" unfolding f_def by (intro \\<^sub>2.range) thus ?thesis unfolding sample_set_alt[OF \\<^sub>2.sample_space_R] unfolding nat_sample_space_def by auto qed lemma h_range_1: assumes "h \ sample_set \\<^sub>3" shows "h x < b" proof - obtain i where f_def:"h = select \\<^sub>3 i" using assms unfolding sample_set_def by auto hence "range h \ sample_set ([b]\<^sub>S)" unfolding f_def by (intro \\<^sub>3.range) thus ?thesis unfolding sample_set_alt[OF \\<^sub>3.sample_space_R] unfolding nat_sample_space_def by auto qed lemma g_range: assumes "(f,g,h) \ sample_set \" shows "g x < C\<^sub>7*b^2" proof - have "g \ sample_set \\<^sub>2" using sample_set_\ assms by auto thus ?thesis using g_range_1 by simp qed lemma h_range: assumes "(f,g,h) \ sample_set \" shows "h x < b" proof - have "h \ sample_set \\<^sub>3" using sample_set_\ assms by auto thus ?thesis using h_range_1 by simp qed lemma fin_f: assumes "(f,g,h) \ sample_set \" shows "finite { int (f a) | a. P a }" (is "finite ?M") proof - have "finite (range f)" using f_range[OF assms] finite_nat_set_iff_bounded_le by auto hence "finite (range (int \ f))" by (simp add:image_image[symmetric]) moreover have "?M \ (range (int \ f))" using image_mono by (auto simp add: setcompr_eq_image) ultimately show ?thesis using finite_subset by auto qed lemma Max_int_range: "x \ (y::int) \ Max {x..y} = y" by auto sublocale \: expander_sample_space l \ \ unfolding expander_sample_space_def using sample_space_\ l_gt_0 \_gt_0 by auto lemma max_q_1: assumes "\ \ sample_set \" shows "\\<^sub>2 \ A (nat \log 2 n\+2) i j = (-1)" proof (cases "i < l") case True obtain f g h where w_i: "\ i = (f,g,h)" by (metis prod_cases3) let ?max_q = "max \log 2 (real n)\ 1" have "\ i \ sample_set \" using \.sample_set assms unfolding Pi_def by auto hence c: "(f,g,h) \ sample_set \" using w_i by auto have a:"int (f x) \ ?max_q" for x proof - have "int (f x) \ int n_exp" using f_range[OF c] by auto also have "... = ?max_q" unfolding n_exp_def by simp finally show ?thesis by simp qed have "\\<^sub>0 (\ i) A j \ Max {(-1)..?max_q}" unfolding w_i \\<^sub>0.simps using a by (intro Max_mono) auto also have "... = ?max_q" by (intro Max_int_range) auto finally have "\\<^sub>0 (\ i) A j \ ?max_q" by simp hence "max (\\<^sub>0 (\ i) A j - int (nat \log 2 (real n)\ + 2)) (- 1) = (-1)" by (intro max_absorb2) linarith thus ?thesis unfolding \\<^sub>2_def \\<^sub>1_def using True by auto next case False thus ?thesis unfolding \\<^sub>2_def \\<^sub>1_def by simp qed lemma max_q_2: assumes "\ \ sample_set \" shows "\ (is_too_large (\\<^sub>2 \ A (nat \log 2 n\+2)))" using max_q_1[OF assms] by (simp add:C\<^sub>5_def case_prod_beta mult_less_0_iff) lemma max_s_3: assumes "\ \ sample_set \" shows "q \ A \ (nat \log 2 n\+2)" unfolding q_def by (intro wellorder_Least_lemma(2) max_q_2 assms) lemma max_mono: "x \ (y::'a::linorder) \ max x z \ max y z" using max.coboundedI1 by auto lemma max_mono_2: "y \ (z::'a::linorder) \ max x y \ max x z" using max.coboundedI2 by auto lemma \\<^sub>0_mono: assumes "\ \ sample_set \" assumes "A \ B" shows "\\<^sub>0 \ A j \ \\<^sub>0 \ B j" proof - obtain f g h where w_i: "\ = (f,g,h)" by (metis prod_cases3) show ?thesis using assms fin_f unfolding \\<^sub>0.simps w_i by (intro Max_mono) auto qed lemma \\<^sub>2_mono: assumes "\ \ sample_set \" assumes "A \ B" shows "\\<^sub>2 \ A x i j \ \\<^sub>2 \ B x i j" proof - have "max (\\<^sub>0 (\ i) A j - int x) (- 1) \ max (\\<^sub>0 (\ i) B j - int x) (- 1)" if "i < l" using assms(1) \.sample_set that by (intro max_mono diff_mono \\<^sub>0_mono assms(2) order.refl) auto thus ?thesis by (cases "i < l") (auto simp add:\\<^sub>2_def \\<^sub>1_def) qed lemma is_too_large_antimono: assumes "\ \ sample_set \" assumes "A \ B" assumes "is_too_large (\\<^sub>2 \ A x)" shows "is_too_large (\\<^sub>2 \ B x)" proof - have "C\<^sub>5 * b * l < (\ (i,j) \ {.. {..log 2 (max (\\<^sub>2 \ A x i j) (-1) + 2)\)" using assms(3) by simp also have "... = (\ y \ {.. {..log 2 (max (\\<^sub>2 \ A x (fst y) (snd y)) (-1) + 2)\)" by (simp add:case_prod_beta) also have "... \ (\ y \ {.. {..log 2 (max (\\<^sub>2 \ B x (fst y) (snd y)) (-1) + 2)\)" by (intro sum_mono floor_mono iffD2[OF log_le_cancel_iff] iffD2[OF of_int_le_iff] add_mono max_mono \\<^sub>2_mono[OF assms(1,2)]) auto also have "... = (\ (i,j) \ {.. {..log 2 (max (\\<^sub>2 \ B x i j) (-1) + 2)\)" by (simp add:case_prod_beta) finally have "(\ (i,j) \ {.. {..log 2 (max (\\<^sub>2 \ B x i j) (-1) + 2)\) > C\<^sub>5 * b * l" by simp thus ?thesis by simp qed lemma q_compact: assumes "\ \ sample_set \" shows "\ (is_too_large (\\<^sub>2 \ A (q \ A)))" unfolding q_def using max_q_2[OF assms] by (intro wellorder_Least_lemma(1)) blast lemma q_mono: assumes "\ \ sample_set \" assumes "A \ B" shows "q \ A \ q \ B" proof - have "\ (is_too_large (\\<^sub>2 \ A (q \ B)))" using is_too_large_antimono[OF assms] q_compact[OF assms(1)] by blast hence "(LEAST q . \(is_too_large (\\<^sub>2 \ A q))) \ q \ B" by (intro Least_le) blast thus ?thesis by (simp add:q_def) qed lemma lt_s_too_large: "x < q \ A \ is_too_large (\\<^sub>2 \ A x)" using not_less_Least unfolding q_def by auto lemma compress_result_1: assumes "\ \ sample_set \" shows "compress (\\<^sub>3 \ A (q \ A - i)) = \ \ A" proof (induction i) case 0 then show ?case using q_compact[OF assms] by (simp add:\\<^sub>3_def \_def) next case (Suc i) show ?case proof (cases "i < q \ A") case True have "is_too_large (\\<^sub>2 \ A (q \ A - Suc i))" using True by (intro lt_s_too_large) simp hence "compress (\\<^sub>3 \ A (q \ A - Suc i)) = compress (compress_step (\\<^sub>3 \ A (q \ A - Suc i)))" unfolding \\<^sub>3_def compress.simps by (simp del: compress.simps compress_step.simps) also have "... = compress (\\<^sub>3 \ A ((q \ A - Suc i)+1))" by (subst \\<^sub>3_step) blast also have "... = compress (\\<^sub>3 \ A (q \ A - i))" using True by (metis Suc_diff_Suc Suc_eq_plus1) also have "... = \ \ A" using Suc by auto finally show ?thesis by simp next case False then show ?thesis using Suc by simp qed qed lemma compress_result: assumes "\ \ sample_set \" assumes "x \ q \ A" shows "compress (\\<^sub>3 \ A x) = \ \ A" proof - obtain i where i_def: "x = q \ A - i" using assms by (metis diff_diff_cancel) have "compress (\\<^sub>3 \ A x) = compress (\\<^sub>3 \ A (q \ A - i))" by (subst i_def) blast also have "... = \ \ A" using compress_result_1[OF assms(1)] by blast finally show ?thesis by simp qed lemma \\<^sub>0_merge: assumes "(f,g,h) \ sample_set \" shows "\\<^sub>0 (f,g,h) (A \ B) j = max (\\<^sub>0 (f,g,h) A j) (\\<^sub>0 (f,g,h) B j)" (is "?L = ?R") proof- let ?f = "\a. int (f a)" have "?L = Max (({ int (f a) | a . a \ A \ h (g a) = j } \ {-1}) \ ({ int (f a) | a . a \ B \ h (g a) = j } \ {-1}))" unfolding \\<^sub>0.simps by (intro arg_cong[where f="Max"]) auto also have "... = max (Max ({ int (f a) | a . a \ A \ h (g a) = j } \ {-1})) (Max ({ int (f a) | a . a \ B \ h (g a) = j } \ {-1}))" by (intro Max_Un finite_UnI fin_f[OF assms]) auto also have "... = ?R" by (simp) finally show ?thesis by simp qed lemma \\<^sub>2_merge: assumes "\ \ sample_set \" shows "\\<^sub>2 \ (A \ B) x i j = max (\\<^sub>2 \ A x i j) (\\<^sub>2 \ B x i j)" proof (cases "i < l") case True obtain f g h where w_i: "\ i = (f,g,h)" by (metis prod_cases3) have "\ i \ sample_set \" using \.sample_set assms unfolding Pi_def by auto hence a: "(f,g,h) \ sample_set \" using w_i by auto show ?thesis unfolding \\<^sub>2_def \\<^sub>1_def using True by (simp add:w_i \\<^sub>0_merge[OF a] del:\\<^sub>0.simps) next case False thus ?thesis by (simp add:\\<^sub>2_def) qed lemma merge1_result: assumes "\ \ sample_set \" shows "merge1 (\ \ A) (\ \ B) = \\<^sub>3 \ (A \ B) (max (q \ A) (q \ B))" proof - let ?qmax = "max (q \ A) (q \ B)" obtain u where u_def: "q \ A + u = ?qmax" by (metis add.commute max.commute nat_minus_add_max) obtain v where v_def: "q \ B + v = ?qmax" by (metis add.commute nat_minus_add_max) have "u = 0 \ v = 0" using u_def v_def by linarith moreover have "\\<^sub>2 \ A (q \ A) i j - u \ (-1)" if "u = 0" for i j using that by (simp add:\\<^sub>2_def \\<^sub>1_def) moreover have "\\<^sub>2 \ B (q \ B) i j - v \ (-1)" if "v = 0" for i j using that by (simp add:\\<^sub>2_def \\<^sub>1_def) ultimately have a:"max (\\<^sub>2 \ A (q \ A) i j - u) (\\<^sub>2 \ B (q \ B) i j - v) \ (-1)" for i j unfolding le_max_iff_disj by blast have "\\<^sub>2 \ (A \ B) ?qmax = (\ i j. max (\\<^sub>2 \ A ?qmax i j) (\\<^sub>2 \ B ?qmax i j))" using \\<^sub>2_merge[OF assms] by blast also have "... = (\ i j. max (\\<^sub>2 \ A (q \ A + u) i j) (\\<^sub>2 \ B (q \ B + v) i j))" unfolding u_def v_def by blast also have "... = (\ i j. max (max (\\<^sub>2 \ A (q \ A) i j - u) (-1)) (max (\\<^sub>2 \ B (q \ B) i j - v) (-1)))" by (simp only: \\<^sub>2_step) also have "... = (\ i j. max (max (\\<^sub>2 \ A (q \ A) i j - u) (\\<^sub>2 \ B (q \ B) i j - v)) (-1))" by (metis (no_types, opaque_lifting) max.commute max.left_commute max.left_idem) also have "... = (\ i j. max (\\<^sub>2 \ A (q \ A) i j - u) (\\<^sub>2 \ B (q \ B) i j - v))" using a by simp also have "... = (\i j. max (\\<^sub>2 \ A (q \ A) i j + int (q \ A) - ?qmax) (\\<^sub>2 \ B (q \ B) i j + int (q \ B) - ?qmax))" by (subst u_def[symmetric], subst v_def[symmetric]) simp finally have "\\<^sub>2 \ (A \ B) (max (q \ A) (q \ B)) = (\i j. max (\\<^sub>2 \ A (q \ A) i j + int (q \ A) - int (?qmax)) (\\<^sub>2 \ B (q \ B) i j + int (q \ B) - int (?qmax)))" by simp thus ?thesis by (simp add:Let_def \_def \\<^sub>3_def) qed lemma merge_result: assumes "\ \ sample_set \" shows "merge (\ \ A) (\ \ B) = \ \ (A \ B)" (is "?L = ?R") proof - have a:"max (q \ A) (q \ B) \ q \ (A \ B)" using q_mono[OF assms] by simp have "?L = compress (merge1 (\ \ A) (\ \ B))" by simp also have "... = compress ( \\<^sub>3 \ (A \ B) (max (q \ A) (q \ B)))" by (subst merge1_result[OF assms]) blast also have "... = ?R" by (intro compress_result[OF assms] a Un_least) finally show ?thesis by blast qed lemma single1_result: "single1 \ x = \\<^sub>3 \ {x} 0" proof - have "(case \ i of (f, g, h) \ if h (g x) = j \ i < l then int (f x) else - 1) = \\<^sub>2 \ {x} 0 i j" for i j proof - obtain f g h where w_i:"\ i = (f, g,h)" by (metis prod_cases3) show ?thesis by (simp add:w_i \\<^sub>2_def \\<^sub>1_def) qed thus ?thesis unfolding \\<^sub>3_def by fastforce qed lemma single_result: assumes "\ \ sample_set \" shows "single \ x = \ \ {x}" (is "?L = ?R") proof - have "?L = compress (single1 \ x)" by (simp) also have "... = compress (\\<^sub>3 \ {x} 0)" by (subst single1_result) blast also have "... = ?R" by (intro compress_result[OF assms]) auto finally show ?thesis by blast qed subsection \Encoding states of the inner algorithm\ definition is_state_table :: "(nat \ nat \ int) \ bool" where "is_state_table g = (range g \ {-1..} \ g ` (-({.. {.. {-1})" text \Encoding for state table values:\ definition V\<^sub>e :: "int encoding" where "V\<^sub>e x = (if x \ -1 then N\<^sub>e (nat (x+1)) else None)" text \Encoding for state table:\ definition T\<^sub>e' :: "(nat \ nat \ int) encoding" where "T\<^sub>e' g = ( if is_state_table g then (List.product [0..\<^sub>e V\<^sub>e) (restrict g ({..{..e :: "(nat \ nat \ int) encoding" where "T\<^sub>e f = T\<^sub>e' (case_prod f)" definition encode_state :: "state encoding" where "encode_state = T\<^sub>e \\<^sub>e Nb\<^sub>e (nat \log 2 n\+3)" lemma inj_on_restrict: assumes "B \ {f. f ` (- A) \ {c}}" shows "inj_on (\x. restrict x A) B" proof (rule inj_onI) fix f g assume a:"f \ B" "g \ B" "restrict f A = restrict g A" have "f x = g x" if "x \ A" for x by (intro restrict_eq_imp[OF a(3) that]) moreover have "f x = g x" if "x \ A" for x proof - have "f x = c" "g x = c" using that a(1,2) assms(1) by auto thus ?thesis by simp qed ultimately show "f = g" by (intro ext) auto qed lemma encode_state: "is_encoding encode_state" proof - have "is_encoding V\<^sub>e" unfolding V\<^sub>e_def by (intro encoding_compose[OF exp_golomb_encoding] inj_onI) auto hence 0:"is_encoding (List.product [0..\<^sub>e V\<^sub>e)" by (intro fun_encoding) have "is_encoding T\<^sub>e'" unfolding T\<^sub>e'_def is_state_table_def by (intro encoding_compose[OF 0] inj_on_restrict[where c="-1"]) auto moreover have " inj case_prod" by (intro injI) (metis curry_case_prod) ultimately have "is_encoding T\<^sub>e" unfolding T\<^sub>e_def by (rule encoding_compose_2) thus ?thesis unfolding encode_state_def by (intro dependent_encoding bounded_nat_encoding) qed lemma state_bit_count: assumes "\ \ sample_set \" - shows "bit_count (encode_state (\ \ A)) \ 2^36 * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3)" + shows "bit_count (encode_state (\ \ A)) \ 2^36 * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3)" (is "?L \ ?R") proof - define t where "t = \\<^sub>2 \ A (q \ A)" have "log 2 (real n) \ 0" using n_gt_0 by simp hence 0: "- 1 < log 2 (real n)" by simp have "t x y = -1" if "x < l" "y \ b" for x y proof - obtain f g h where \_def: "\ x = (f,g,h)" by (metis prod_cases3) have "(f, g, h) \ sample_set \" using \.sample_set assms unfolding Pi_def \_def[symmetric] by auto hence "h (g a) < b" for a using h_range by auto hence "y \ h (g a)" for a using that(2) not_less by blast hence aux_4: "{int (f a) |a. a \ A \ h (g a) = y} = {}" by auto hence "max (Max (insert (- 1) {int (f a) |a. a \ A \ h (g a) = y}) - int (q \ A)) (- 1) = - 1" unfolding aux_4 by simp thus ?thesis unfolding t_def \\<^sub>2_def \\<^sub>1_def by (simp add:\_def) qed moreover have "t x y = -1" if "x \ l" for x y using that unfolding t_def \\<^sub>2_def \\<^sub>1_def by simp ultimately have 1: "t x y = -1" if "x \ l \ y \ b" for x y using that by (meson not_less) have 2: "t x y \ -1" for x y unfolding t_def \\<^sub>2_def \\<^sub>1_def by simp hence 3: "t x y + 1 \ 0" for x y by (metis add.commute le_add_same_cancel1 minus_add_cancel) have 4:"is_state_table (case_prod t)" using 2 1 unfolding is_state_table_def by auto have "bit_count(T\<^sub>e (\\<^sub>2 \ A (q \ A))) = bit_count(T\<^sub>e t)" unfolding t_def by simp also have "... = bit_count ((List.product [0..\<^sub>e V\<^sub>e) (\(x, y)\{..{..e_def T\<^sub>e'_def by simp also have "... = (\x\List.product [0..e ((\(x, y)\{.. {..(x,y)\List.product [0..e (t x y)))" by (intro arg_cong[where f="sum_list"] map_cong refl) (simp add:atLeast0LessThan case_prod_beta) also have "... = (\x\{0.. {0..e (t (fst x) (snd x))))" by (subst sum_list_distinct_conv_sum_set) (auto intro:distinct_product simp add:case_prod_beta) also have "... = (\x\{.. {..e (nat (t (fst x) (snd x)+1))))" using 2 unfolding V\<^sub>e_def not_less[symmetric] by (intro sum.cong refl arg_cong[where f="bit_count"]) auto also have "...=(\x\{..{..log 2(1+real(nat(t (fst x)(snd x)+1)))\)" unfolding exp_golomb_bit_count_exact is_too_large.simps not_less by simp also have "...=(\x\{..{..log 2(2+ of_int(t (fst x)(snd x)))\)" using 3 by (subst of_nat_nat) (auto simp add:ac_simps) also have "...=b*l + 2* of_int (\(i,j)\{..{..log 2(2+ of_int(max (t i j) (-1)))\)" using 2 by (subst max_absorb1) (auto simp add:case_prod_beta sum.distrib sum_distrib_left) also have "... \ b*l + 2 * of_int (C\<^sub>5 * int b * int l)" using q_compact[OF assms, where A="A"] unfolding is_too_large.simps not_less t_def[symmetric] by (intro add_mono ereal_mono iffD2[OF of_int_le_iff] mult_left_mono order.refl) (simp_all add:ac_simps) also have "... = (2 * C\<^sub>5 + 1) * b * l" by (simp add:algebra_simps) finally have 5:"bit_count (T\<^sub>e (\\<^sub>2 \ A (q \ A))) \ (2 * C\<^sub>5 + 1) * b * l" by simp have "C\<^sub>4 \ 1" unfolding C\<^sub>4_def by simp - moreover have "\\<^sup>2 \ 1" - using \_lt_1 \_gt_0 + moreover have "\\<^sup>2 \ 1" + using \_lt_1 \_gt_0 by (intro power_le_one) auto - ultimately have "0 \ log 2 (C\<^sub>4 / \\<^sup>2)" - using \_gt_0 \_lt_1 + ultimately have "0 \ log 2 (C\<^sub>4 / \\<^sup>2)" + using \_gt_0 \_lt_1 by (intro iffD2[OF zero_le_log_cancel_iff] divide_pos_pos)auto - hence 6: "- 1 < log 2 (C\<^sub>4 / \\<^sup>2)" + hence 6: "- 1 < log 2 (C\<^sub>4 / \\<^sup>2)" by simp - have "b = 2 powr (real (nat \log 2 (C\<^sub>4 / \\<^sup>2)\))" + have "b = 2 powr (real (nat \log 2 (C\<^sub>4 / \\<^sup>2)\))" unfolding b_def b_exp_def by (simp add:powr_realpow) - also have "... = 2 powr (\log 2 (C\<^sub>4 / \^2)\)" + also have "... = 2 powr (\log 2 (C\<^sub>4 / \^2)\)" using 6 by (intro arg_cong2[where f="(powr)"] of_nat_nat refl) simp - also have "... \ 2 powr (log 2 (C\<^sub>4 / \^2) + 1)" + also have "... \ 2 powr (log 2 (C\<^sub>4 / \^2) + 1)" by (intro powr_mono) auto - also have "... = 2 * C\<^sub>4 / \^2" - using \_gt_0 unfolding powr_add C\<^sub>4_def + also have "... = 2 * C\<^sub>4 / \^2" + using \_gt_0 unfolding powr_add C\<^sub>4_def by (subst powr_log_cancel) (auto intro:divide_pos_pos) - finally have 7:"b \ 2 * C\<^sub>4 / \^2" by simp + finally have 7:"b \ 2 * C\<^sub>4 / \^2" by simp - have "l \ C\<^sub>6 * ln (1 / \) + C\<^sub>6 * ln 2 + 1" + have "l \ C\<^sub>6 * ln (1 / \) + C\<^sub>6 * ln 2 + 1" by (intro l_ubound) - also have "... \ 4 * ln(1/\) + 3+1" + also have "... \ 4 * ln(1/\) + 3+1" unfolding C\<^sub>6_def by (intro add_mono order.refl) (approximation 5) - also have "... = 4 * (ln(1/\)+1)" + also have "... = 4 * (ln(1/\)+1)" by simp - finally have 8:"l \ 4 * (ln(1/\)+1)" + finally have 8:"l \ 4 * (ln(1/\)+1)" by simp - have "\\<^sup>2 = 0 + \\<^sup>2" + have "\\<^sup>2 = 0 + \\<^sup>2" by simp - also have "... \ ln (1 / \) + 1" - using \_gt_0 \_lt_1 \_gt_0 \_lt_1 + also have "... \ ln (1 / \) + 1" + using \_gt_0 \_lt_1 \_gt_0 \_lt_1 by (intro add_mono power_le_one) auto - finally have 9: "\\<^sup>2 \ ln (1 / \) + 1" + finally have 9: "\\<^sup>2 \ ln (1 / \) + 1" by simp - have 10: "0 \ ln (1 / \) + 1" - using \_gt_0 \_lt_1 by (intro add_nonneg_nonneg) auto + have 10: "0 \ ln (1 / \) + 1" + using \_gt_0 \_lt_1 by (intro add_nonneg_nonneg) auto have "?L = bit_count (T\<^sub>e (\\<^sub>2 \ A (q \ A))) + bit_count (Nb\<^sub>e (nat \log 2 (real n)\+3) (q \ A))" unfolding encode_state_def \_def \\<^sub>3_def by (simp add:dependent_bit_count) also have "...=bit_count(T\<^sub>e(\\<^sub>2 \ A (q \ A)))+ereal (1+ of_int\log 2 (2 + real (nat \log 2 n\))\)" using max_s_3[OF assms] by (subst bounded_nat_bit_count_2) (simp_all add:numeral_eq_Suc le_imp_less_Suc floorlog_def) also have "... = bit_count(T\<^sub>e(\\<^sub>2 \ A (q \ A)))+ereal (1+ of_int\log 2 (2 + of_int \log 2 n\)\)" using 0 by simp also have "... \ bit_count(T\<^sub>e(\\<^sub>2 \ A (q \ A)))+ereal (1+log 2 (2 + of_int \log 2 n\))" by (intro add_mono ereal_mono) simp_all also have "... \ bit_count(T\<^sub>e(\\<^sub>2 \ A (q \ A)))+ereal (1+log 2 (2 + (log 2 n + 1)))" using 0 n_gt_0 by (intro add_mono ereal_mono iffD2[OF log_le_cancel_iff] add_pos_nonneg) auto also have "... = bit_count(T\<^sub>e(\\<^sub>2 \ A (q \ A)))+ereal (1+log 2 (log 2 n + 3))" by (simp add:ac_simps) also have "... \ ereal ((2 * C\<^sub>5 + 1) * b * l) + ereal (1+log 2 (log 2 n + 3))" by (intro add_mono 5) auto also have "... = (2 * C\<^sub>5 + 1) * real b * real l + log 2 (log 2 n + 3) + 1" by simp - also have "... \ (2 * C\<^sub>5 + 1) * (2 * C\<^sub>4 / \^2) * real l + log 2 (log 2 n + 3) + 1" + also have "... \ (2 * C\<^sub>5 + 1) * (2 * C\<^sub>4 / \^2) * real l + log 2 (log 2 n + 3) + 1" unfolding C\<^sub>5_def by (intro ereal_mono mult_right_mono mult_left_mono add_mono 7) auto - also have "... = (4 * of_int C\<^sub>5+2)*C\<^sub>4*real l/ \^2 + log 2 (log 2 n + 3) + 1" + also have "... = (4 * of_int C\<^sub>5+2)*C\<^sub>4*real l/ \^2 + log 2 (log 2 n + 3) + 1" by simp - also have "... \ (4 * of_int C\<^sub>5+2)*C\<^sub>4*(4*(ln(1/ \)+1))/ \^2 + log 2 (log 2 n + 3) + 1" - using \_gt_0 unfolding C\<^sub>5_def C\<^sub>4_def + also have "... \ (4 * of_int C\<^sub>5+2)*C\<^sub>4*(4*(ln(1/ \)+1))/ \^2 + log 2 (log 2 n + 3) + 1" + using \_gt_0 unfolding C\<^sub>5_def C\<^sub>4_def by (intro ereal_mono add_mono order.refl divide_right_mono mult_left_mono 8) auto - also have "... = ((2*33+1)*9*2^26)*(ln(1/ \)+1)/ \^2 + log 2 (log 2 n + 3) + 1" + also have "... = ((2*33+1)*9*2^26)*(ln(1/ \)+1)/ \^2 + log 2 (log 2 n + 3) + 1" unfolding C\<^sub>5_def C\<^sub>4_def by simp - also have "... \ (2^36-1) * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3) + (ln (1/ \)+1)/ \^2" - using \_gt_0 \_gt_0 \_lt_1 9 10 + also have "... \ (2^36-1) * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3) + (ln (1/ \)+1)/ \^2" + using \_gt_0 \_gt_0 \_lt_1 9 10 by (intro add_mono ereal_mono divide_right_mono mult_right_mono mult_left_mono) simp_all - also have "... = 2^36* (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3)" + also have "... = 2^36* (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3)" by (simp add:divide_simps) finally show ?thesis by simp qed lemma random_bit_count: - "size \ \ 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2 + (55 + 60 * ln (1 / \))^3)" + "size \ \ 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2 + (55 + 60 * ln (1 / \))^3)" (is "?L \ ?R") proof - have 1:"log 2 (real n) \ 0" using n_gt_0 by simp hence 0: "- 1 < log 2 (real n)" by simp have 10: "log 2 C\<^sub>4 \ 27" unfolding C\<^sub>4_def by (approximation 10) - have "\\<^sup>2 \ 1" - using \_gt_0 \_lt_1 by (intro power_le_one) auto + have "\\<^sup>2 \ 1" + using \_gt_0 \_lt_1 by (intro power_le_one) auto also have "... \ C\<^sub>4" unfolding C\<^sub>4_def by simp - finally have " \\<^sup>2 \ C\<^sub>4" by simp - hence 9: "0 \ log 2 (C\<^sub>4 / \\<^sup>2)" - using \_gt_0 unfolding C\<^sub>4_def + finally have " \\<^sup>2 \ C\<^sub>4" by simp + hence 9: "0 \ log 2 (C\<^sub>4 / \\<^sup>2)" + using \_gt_0 unfolding C\<^sub>4_def by (intro iffD2[OF zero_le_log_cancel_iff]) simp_all - hence 2: "- 1 < log 2 (C\<^sub>4 / \\<^sup>2)" + hence 2: "- 1 < log 2 (C\<^sub>4 / \\<^sup>2)" by simp have 3: "0 < C\<^sub>7 * b\<^sup>2" unfolding C\<^sub>7_def using b_min by (intro Rings.mult_pos_pos) auto have "0 \ log 2 (real C\<^sub>7) + real (b_exp * 2)" unfolding C\<^sub>7_def by (intro add_nonneg_nonneg) auto hence 4: "-1 < log 2 (real C\<^sub>7) + real (b_exp * 2)" by simp have "real (size \\<^sub>1) = 2 ^ (max (nat \log 2 (real n)\) 1 * 2)" using \\<^sub>1.size[OF n_gt_0] unfolding n_exp_def by simp also have "... \ 2 powr (2 * max (nat \log 2 (real n)\) 1)" by (subst powr_realpow) auto also have "... = 2 powr (2 * max (real (nat \log 2 (real n)\)) 1)" using n_gt_0 unfolding of_nat_mult of_nat_max by simp also have "... = 2 powr (2 * max (of_int \log 2 (real n)\) 1)" using 0 by (subst of_nat_nat) simp_all also have "... \ 2 powr (2 * max (log 2 (real n) + 1) 1)" by (intro powr_mono mult_left_mono max_mono) auto also have "... = 2 powr (2 * (log 2 (real n) + 1))" using 1 by (subst max_absorb1) auto finally have 5:"real (size \\<^sub>1) \ 2 powr (2 * log 2 n + 2)" by simp have "real (size \\<^sub>2) = 2 ^ (max (5 + b_exp * 2) (nat \log 2 (real n)\) * 2)" unfolding \\<^sub>2.size[OF n_gt_0] by simp also have "... \ 2 ^ (((5 + b_exp * 2) + (nat \log 2 (real n)\)) * 2)" by (intro power_increasing mult_right_mono) auto also have "... = 2 powr ((5 + b_exp * 2 + real (nat \log 2 (real n)\))*2)" by (subst powr_realpow[symmetric]) auto also have "... = 2 powr ((5 + of_int b_exp * 2 + of_int \log 2 (real n)\)*2)" using 0 by (subst of_nat_nat) auto also have "... \ 2 powr ((5 + of_int b_exp * 2 + (log 2 (real n) + 1))*2)" by (intro powr_mono mult_right_mono add_mono) simp_all - also have "... = 2 powr (12 + 4 * real( nat \log 2 (C\<^sub>4 / \\<^sup>2)\) + log 2 (real n) * 2)" + also have "... = 2 powr (12 + 4 * real( nat \log 2 (C\<^sub>4 / \\<^sup>2)\) + log 2 (real n) * 2)" unfolding b_exp_def by (simp add:ac_simps) - also have "... = 2 powr (12 + 4 * real_of_int \log 2 (C\<^sub>4 / \\<^sup>2)\ + log 2 (real n) * 2)" + also have "... = 2 powr (12 + 4 * real_of_int \log 2 (C\<^sub>4 / \\<^sup>2)\ + log 2 (real n) * 2)" using 2 by (subst of_nat_nat) simp_all - also have "... \ 2 powr (12 + 4 * (log 2 (C\<^sub>4 / \\<^sup>2) + 1) + log 2 (real n) * 2)" + also have "... \ 2 powr (12 + 4 * (log 2 (C\<^sub>4 / \\<^sup>2) + 1) + log 2 (real n) * 2)" by (intro powr_mono add_mono order.refl mult_left_mono) simp_all - also have "... = 2 powr (2 * log 2 n + 4 * log 2 (C\<^sub>4 / \\<^sup>2) + 16)" + also have "... = 2 powr (2 * log 2 n + 4 * log 2 (C\<^sub>4 / \\<^sup>2) + 16)" by (simp add:ac_simps) - finally have 6:"real (size \\<^sub>2) \ 2 powr (2 * log 2 n + 4 * log 2 (C\<^sub>4 / \\<^sup>2) + 16)" + finally have 6:"real (size \\<^sub>2) \ 2 powr (2 * log 2 n + 4 * log 2 (C\<^sub>4 / \\<^sup>2) + 16)" by simp have "real (size \\<^sub>3) = 2 ^ (max b_exp (nat \log 2 (real C\<^sub>7 * (2 ^ (b_exp*2)))\) * k)" unfolding \\<^sub>3.size[OF 3] power_mult by (simp add:b_def) also have "... = 2 ^ (max b_exp (nat \log 2 C\<^sub>7 + log 2 (2 ^ (b_exp*2))\) * k)" unfolding C\<^sub>7_def by (subst log_mult) simp_all also have "... = 2 ^ (max b_exp (nat \log 2 C\<^sub>7 + (b_exp*2)\) * k)" by (subst log_nat_power) simp_all also have "... = 2 powr (max (real b_exp) (real (nat \log 2 C\<^sub>7 + (b_exp*2)\)) * real k)" by (subst powr_realpow[symmetric]) simp_all also have "... = 2 powr (max (real b_exp) (of_int \log 2 C\<^sub>7 + (b_exp*2)\) * real k)" using 4 by (subst of_nat_nat) simp_all also have "... \ 2 powr (max (real b_exp) (log 2 C\<^sub>7 + real b_exp*2 +1) * real k)" by (intro powr_mono mult_right_mono max_mono_2) simp_all also have "... = 2 powr ((log 2 (2^5) + real b_exp*2 +1) * real k)" unfolding C\<^sub>7_def by (subst max_absorb2) simp_all also have "... = 2 powr ((real b_exp*2 +6) * real k)" unfolding C\<^sub>7_def by (subst log_nat_power) (simp_all add:ac_simps) - also have "... = 2 powr ((of_int \log 2 (C\<^sub>4 / \\<^sup>2)\ * 2 + 6) * real k)" + also have "... = 2 powr ((of_int \log 2 (C\<^sub>4 / \\<^sup>2)\ * 2 + 6) * real k)" using 2 unfolding b_exp_def by (subst of_nat_nat) simp_all - also have "... \ 2 powr (((log 2 (C\<^sub>4 / \^2)+1) * 2 + 6) * real k)" + also have "... \ 2 powr (((log 2 (C\<^sub>4 / \^2)+1) * 2 + 6) * real k)" by (intro powr_mono mult_right_mono add_mono) simp_all - also have "... = 2 powr ((log 2 (C\<^sub>4 / \\<^sup>2) * 2 + 8 ) * real k)" + also have "... = 2 powr ((log 2 (C\<^sub>4 / \\<^sup>2) * 2 + 8 ) * real k)" by (simp add:ac_simps) - finally have 7:"real (size \\<^sub>3) \ 2 powr ((log 2 (C\<^sub>4 / \\<^sup>2) * 2 + 8 ) * real k)" + finally have 7:"real (size \\<^sub>3) \ 2 powr ((log 2 (C\<^sub>4 / \\<^sup>2) * 2 + 8 ) * real k)" by simp have "ln (real b) \ 0" using b_min by simp hence "real k = of_int \7.5 * ln (real b) + 16\" unfolding k_def C\<^sub>2_def C\<^sub>3_def by (subst of_nat_nat) simp_all also have "... \ (7.5 * ln (real b) + 16) + 1" unfolding b_def by (intro of_int_ceiling_le_add_one) also have "... = 7.5 * ln (2 powr b_exp) + 17" unfolding b_def using powr_realpow by simp also have "... = real b_exp * (7.5 * ln 2) + 17" unfolding powr_def by simp also have "... \ real b_exp * 6 + 17" by (intro add_mono mult_left_mono order.refl of_nat_0_le_iff) (approximation 5) - also have "... = of_int \log 2 (C\<^sub>4 / \\<^sup>2)\ * 6 + 17" + also have "... = of_int \log 2 (C\<^sub>4 / \\<^sup>2)\ * 6 + 17" using 2 unfolding b_exp_def by (subst of_nat_nat) simp_all - also have "... \ (log 2 (C\<^sub>4 / \^2) + 1) * 6 + 17" + also have "... \ (log 2 (C\<^sub>4 / \^2) + 1) * 6 + 17" by (intro add_mono mult_right_mono) simp_all - also have "... = 6 * log 2 (C\<^sub>4 / \^2) + 23" + also have "... = 6 * log 2 (C\<^sub>4 / \^2) + 23" by simp - finally have 8:"real k \ 6 * log 2 (C\<^sub>4 / \^2) + 23" + finally have 8:"real k \ 6 * log 2 (C\<^sub>4 / \^2) + 23" by simp have "real (size \) = real (size \\<^sub>1) * real (size \\<^sub>2) * real (size \\<^sub>3)" unfolding \_def prod_sample_space_def by simp also have "... \ - 2 powr(2*log 2 n+2)*2 powr (2*log 2 n+4*log 2 (C\<^sub>4/\\<^sup>2)+16)*2 powr((log 2 (C\<^sub>4/\\<^sup>2)*2+8)*real k)" + 2 powr(2*log 2 n+2)*2 powr (2*log 2 n+4*log 2 (C\<^sub>4/\\<^sup>2)+16)*2 powr((log 2 (C\<^sub>4/\\<^sup>2)*2+8)*real k)" by (intro mult_mono 5 6 7 mult_nonneg_nonneg) simp_all - also have "... = 2 powr (2*log 2 n + 2 + 2 * log 2 n+4*log 2 (C\<^sub>4/\\<^sup>2)+16+(log 2 (C\<^sub>4/\\<^sup>2)*2+8)*real k)" + also have "... = 2 powr (2*log 2 n + 2 + 2 * log 2 n+4*log 2 (C\<^sub>4/\\<^sup>2)+16+(log 2 (C\<^sub>4/\\<^sup>2)*2+8)*real k)" unfolding powr_add by simp - also have "... = 2 powr (4*log 2 n + 4*log 2 (C\<^sub>4/\\<^sup>2) + 18 + (2*log 2 (C\<^sub>4/\\<^sup>2)+8)*real k)" + also have "... = 2 powr (4*log 2 n + 4*log 2 (C\<^sub>4/\\<^sup>2) + 18 + (2*log 2 (C\<^sub>4/\\<^sup>2)+8)*real k)" by (simp add:ac_simps) also have "... \ - 2 powr (4* log 2 n + 4* log 2 (C\<^sub>4/ \^2) + 18 + (2*log 2 (C\<^sub>4/\\<^sup>2)+8)*(6 * log 2 (C\<^sub>4 / \^2) + 23))" + 2 powr (4* log 2 n + 4* log 2 (C\<^sub>4/ \^2) + 18 + (2*log 2 (C\<^sub>4/\\<^sup>2)+8)*(6 * log 2 (C\<^sub>4 / \^2) + 23))" using 9 by (intro powr_mono add_mono order.refl mult_left_mono 8 add_nonneg_nonneg) simp_all - also have "... = 2 powr (4 * log 2 n+12 * log 2 (C\<^sub>4 / \^2)^2 + 98 * log 2 (C\<^sub>4 / \^2)+202)" + also have "... = 2 powr (4 * log 2 n+12 * log 2 (C\<^sub>4 / \^2)^2 + 98 * log 2 (C\<^sub>4 / \^2)+202)" by (simp add:algebra_simps power2_eq_square) - also have "... \ 2 powr (4 * log 2 n+12 * log 2 (C\<^sub>4 / \^2)^2 + 120 * log 2 (C\<^sub>4 / \^2)+300)" + also have "... \ 2 powr (4 * log 2 n+12 * log 2 (C\<^sub>4 / \^2)^2 + 120 * log 2 (C\<^sub>4 / \^2)+300)" using 9 by (intro powr_mono add_mono order.refl mult_right_mono) simp_all - also have "... = 2 powr (4 * log 2 n+12 * (log 2 (C\<^sub>4* (1/ \)^2) + 5)^2)" + also have "... = 2 powr (4 * log 2 n+12 * (log 2 (C\<^sub>4* (1/ \)^2) + 5)^2)" by (simp add:power2_eq_square algebra_simps) - also have "... = 2 powr (4 * log 2 n + 12 * (log 2 C\<^sub>4 + log 2 ((1 / \)^2) + 5)^2)" - unfolding C\<^sub>4_def using \_gt_0 by (subst log_mult) auto - also have "... \ 2 powr (4 * log 2 n + 12 * (27 + log 2 ((1/ \)^2) + 5)^2)" - using \_gt_0 \_lt_1 + also have "... = 2 powr (4 * log 2 n + 12 * (log 2 C\<^sub>4 + log 2 ((1 / \)^2) + 5)^2)" + unfolding C\<^sub>4_def using \_gt_0 by (subst log_mult) auto + also have "... \ 2 powr (4 * log 2 n + 12 * (27 + log 2 ((1/ \)^2) + 5)^2)" + using \_gt_0 \_lt_1 by (intro powr_mono add_mono order.refl mult_left_mono power_mono add_nonneg_nonneg 10) (simp_all add:C\<^sub>4_def) - also have "... = 2 powr (4 * log 2 n + 12 * (2 * (log 2 (1 / \) + 16))^2)" - using \_gt_0 by (subst log_nat_power) (simp_all add:ac_simps) - also have "... = 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2)" + also have "... = 2 powr (4 * log 2 n + 12 * (2 * (log 2 (1 / \) + 16))^2)" + using \_gt_0 by (subst log_nat_power) (simp_all add:ac_simps) + also have "... = 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2)" unfolding power_mult_distrib by simp - finally have 19:"real (size \) \ 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2)" + finally have 19:"real (size \) \ 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2)" by simp have "0 \ ln \ / ln (19 / 20)" using \_gt_0 \_le_1 by (intro divide_nonpos_neg) simp_all hence 11: "-1 < ln \ / ln (19 / 20)" by simp have 12: "ln (19 / 20) \ -(0.05::real)" "- ln (1 / 16) \ (2.8::real)" by (approximation 10)+ have 13: "ln l \ 0" using l_gt_0 by auto have "ln l^3 = 27 * (0 + ln l/3)^3" by (simp add:power3_eq_cube) also have "... \ 27 * (1 + ln l/real 3)^3" using l_gt_0 by (intro mult_left_mono add_mono power_mono) auto also have "... \ 27 * (exp (ln l))" using l_gt_0 13 by (intro mult_left_mono exp_ge_one_plus_x_over_n_power_n) linarith+ also have "... = 27 * real l" using l_gt_0 by (subst exp_ln) auto finally have 14:"ln l^3 \ 27 * real l" by simp - have 15:"C\<^sub>6 * ln (2 / \) > 0" - using \_lt_1 \_gt_0 unfolding C\<^sub>6_def + have 15:"C\<^sub>6 * ln (2 / \) > 0" + using \_lt_1 \_gt_0 unfolding C\<^sub>6_def by (intro Rings.mult_pos_pos ln_gt_zero) auto - hence "1 \ real_of_int \C\<^sub>6 * ln (2 / \)\" + hence "1 \ real_of_int \C\<^sub>6 * ln (2 / \)\" by simp - hence 16: "1 \ 3 * real_of_int \C\<^sub>6 * ln (2 / \)\" + hence 16: "1 \ 3 * real_of_int \C\<^sub>6 * ln (2 / \)\" by argo have 17: "12 * ln 2 \ (9::real)" by (approximation 5) have "16 ^ ((l - 1) * nat\ln \ / ln 0.95\) = 16 powr (real (l-1)*real(nat \ln \ / ln (19 / 20)\))" by (subst powr_realpow[symmetric]) auto also have "... = 16 powr (real (l-1)* of_int \ln \ / ln (19 / 20)\)" using 11 by (subst of_nat_nat) simp_all also have "... \ 16 powr (real (l-1)* (ln \ / ln (19/20)+1))" by (intro powr_mono mult_left_mono) auto also have "... = 16 powr ((real l - 1)*(ln \ / ln (19/20)+1))" using l_gt_0 by (subst of_nat_diff) auto also have "... \ 16 powr ((real l - 1)*(ln \ / (-0.05)+1))" using l_gt_0 \_gt_0 \_le_1 by (intro powr_mono mult_left_mono add_mono divide_left_mono_neg 12) auto also have "... = 16 powr ((real l - 1)*(20 * (-ln \)+1))" by (simp add:algebra_simps) also have "... = 16 powr ((real l - 1)*(20 * -(min (ln (1/16)) (-l*ln l^3))+1))" unfolding \_def by (subst ln_min_swap) auto also have "... = 16 powr ((real l - 1)*(20 * max (-ln (1/16)) (l*ln l^3)+1))" by (intro_cong "[\\<^sub>2 (powr), \\<^sub>2(+), \\<^sub>2 (*)]") simp also have "... \ 16 powr ((real l - 1)*(20 * max (2.8) (l*ln l^3)+1))" using l_gt_0 by (intro powr_mono mult_left_mono add_mono max_mono 12) auto also have "... \ 16 powr ((real l - 1)*(20 * (2.8+l*ln l^3)+1))" using l_gt_0 by (intro powr_mono mult_left_mono add_mono) auto also have "... = 16 powr ((real l - 1)*(20 * (l*ln l^3)+57))" by (simp add:algebra_simps) also have "... \ 16 powr ((real l - 1)*(20 * (real l*(27*real l))+57))" using l_gt_0 by (intro powr_mono mult_left_mono add_mono 14) auto also have "... = 16 powr (540 * real l^3 - 540 * real l^2 + 57* real l - 57)" by (simp add:algebra_simps numeral_eq_Suc) also have "... \ 16 powr (540 * real l^3 - 540 * real l^2 + 180* real l - 20)" by (intro powr_mono add_mono diff_mono order.refl mult_right_mono) auto also have "... = 16 powr (20 * (3*real l - 1)^3)" by (simp add: algebra_simps power3_eq_cube power2_eq_square) - also have "... = 16 powr (20 * (3 * of_int \C\<^sub>6 * ln (2 / \)\ - 1) ^ 3)" + also have "... = 16 powr (20 * (3 * of_int \C\<^sub>6 * ln (2 / \)\ - 1) ^ 3)" using 15 unfolding l_def by (subst of_nat_nat) auto - also have "... \ 16 powr (20 * (3 * (C\<^sub>6 * ln (2 / \) + 1) - 1) ^ 3)" + also have "... \ 16 powr (20 * (3 * (C\<^sub>6 * ln (2 / \) + 1) - 1) ^ 3)" using 16 by (intro powr_mono mult_left_mono power_mono diff_mono) auto - also have "... = 16 powr (20 * (2 + 12 * ln (2 * (1 / \))) ^ 3)" + also have "... = 16 powr (20 * (2 + 12 * ln (2 * (1 / \))) ^ 3)" by (simp add:algebra_simps C\<^sub>6_def) - also have "... = (2 powr 4) powr (20 * (2+ 12 * (ln 2 + ln(1/ \)))^3)" - using \_gt_0 by (subst ln_mult) auto - also have "... = 2 powr (80 * (2 + 12 * ln 2 + 12 * ln (1 / \)) ^ 3)" + also have "... = (2 powr 4) powr (20 * (2+ 12 * (ln 2 + ln(1/ \)))^3)" + using \_gt_0 by (subst ln_mult) auto + also have "... = 2 powr (80 * (2 + 12 * ln 2 + 12 * ln (1 / \)) ^ 3)" unfolding powr_powr by (simp add:ac_simps) - also have "... \ 2 powr (80 * (2 + 9 + 12 * ln (1 / \)) ^ 3)" - using \_gt_0 \_lt_1 + also have "... \ 2 powr (80 * (2 + 9 + 12 * ln (1 / \)) ^ 3)" + using \_gt_0 \_lt_1 by (intro powr_mono mult_left_mono power_mono add_mono 17 add_nonneg_nonneg) auto - also have "... = 2 powr (80 * (11 + 12 * ln (1 / \)) ^ 3)" + also have "... = 2 powr (80 * (11 + 12 * ln (1 / \)) ^ 3)" by simp - also have "... \ 2 powr (5^3 * (11 + 12 * ln (1 / \)) ^ 3)" - using \_gt_0 \_lt_1 + also have "... \ 2 powr (5^3 * (11 + 12 * ln (1 / \)) ^ 3)" + using \_gt_0 \_lt_1 by (intro powr_mono mult_right_mono) (auto intro!:add_nonneg_nonneg) - also have "... = 2 powr ((55 + 60 * ln (1 / \))^3)" + also have "... = 2 powr ((55 + 60 * ln (1 / \))^3)" unfolding power_mult_distrib[symmetric] by simp - finally have 18:"16^((l - 1) * nat\ln \ / ln (19/20)\) \ 2 powr ((55 + 60 * ln (1 / \))^3)" + finally have 18:"16^((l - 1) * nat\ln \ / ln (19/20)\) \ 2 powr ((55 + 60 * ln (1 / \))^3)" by simp have "?L = real (size \) * 16 ^ ((l - 1) * nat \ln \ / ln (19 / 20)\)" unfolding \.size by simp - also have "... \ 2 powr (4*log 2 n+48*(log 2 (1/\)+16)^2)*2 powr ((55 + 60 * ln (1 / \))^3)" + also have "... \ 2 powr (4*log 2 n+48*(log 2 (1/\)+16)^2)*2 powr ((55 + 60 * ln (1 / \))^3)" by (intro mult_mono 18 19) simp_all - also have "... = 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2 + (55 + 60 * ln (1 / \))^3)" + also have "... = 2 powr (4 * log 2 n + 48 * (log 2 (1 / \) + 16)^2 + (55 + 60 * ln (1 / \))^3)" unfolding powr_add[symmetric] by simp finally show ?thesis by simp qed end unbundle no_intro_cong_syntax end \ No newline at end of file diff --git a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Outer_Algorithm.thy b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Outer_Algorithm.thy --- a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Outer_Algorithm.thy +++ b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Outer_Algorithm.thy @@ -1,810 +1,810 @@ section \Outer Algorithm\label{sec:outer_algorithm}\ text \This section introduces the final solution with optimal size space usage. Internally it relies on the inner algorithm described in Section~\ref{sec:inner_algorithm}, dependending on the paramaters $n$, $\varepsilon$ and $\delta$ it either uses the inner algorithm directly or if $\varepsilon^{-1}$ is larger than $\ln n$ it runs $\frac{\varepsilon^{-1}}{\ln \ln n}$ copies of the inner algorithm (with the modified failure probability $\frac{1}{\ln n}$) using an expander to select its seeds. The theorems below verify that the probability that the relative accuracy of the median of the copies is too large is below $\varepsilon$.\ theory Distributed_Distinct_Elements_Outer_Algorithm imports Distributed_Distinct_Elements_Accuracy Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators Frequency_Moments.Landau_Ext Landau_Symbols.Landau_More begin unbundle intro_cong_syntax text \The following are non-asymptotic hard bounds on the space usage for the sketches and seeds repsectively. The end of this section contains a proof that the sum is asymptotically in $\mathcal O(\ln( \varepsilon^{-1}) \delta^{-1} + \ln n)$.\ -definition "state_space_usage = (\(n,\,\). 2^40 * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3))" -definition "seed_space_usage = (\(n,\,\). 2^30+2^23*ln n+48*(log 2(1/\)+16)\<^sup>2+336*ln (1/\))" +definition "state_space_usage = (\(n,\,\). 2^40 * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3))" +definition "seed_space_usage = (\(n,\,\). 2^30+2^23*ln n+48*(log 2(1/\)+16)\<^sup>2+336*ln (1/\))" locale outer_algorithm = fixes n :: nat - fixes \ :: real fixes \ :: real + fixes \ :: real assumes n_gt_0: "n > 0" + assumes \_gt_0: "\ > 0" and \_lt_1: "\ < 1" assumes \_gt_0: "\ > 0" and \_lt_1: "\ < 1" - assumes \_gt_0: "\ > 0" and \_lt_1: "\ < 1" begin definition n\<^sub>0 where "n\<^sub>0 = max (real n) (exp (exp 5))" -definition stage_two where "stage_two = (\ < (1/ln n\<^sub>0))" -definition \\<^sub>i :: real where "\\<^sub>i = (if stage_two then (1/ln n\<^sub>0) else \)" -definition m :: nat where "m = (if stage_two then nat \4 * ln (1/ \)/ln (ln n\<^sub>0)\ else 1)" +definition stage_two where "stage_two = (\ < (1/ln n\<^sub>0))" +definition \\<^sub>i :: real where "\\<^sub>i = (if stage_two then (1/ln n\<^sub>0) else \)" +definition m :: nat where "m = (if stage_two then nat \4 * ln (1/ \)/ln (ln n\<^sub>0)\ else 1)" definition \ where "\ = (if stage_two then (1/ln n\<^sub>0) else 1)" lemma m_lbound: assumes "stage_two" - shows "m \ 4 * ln (1/ \)/ln(ln n\<^sub>0)" + shows "m \ 4 * ln (1/ \)/ln(ln n\<^sub>0)" proof - - have "m = real (nat \4 * ln (1 / \) / ln (ln n\<^sub>0)\)" + have "m = real (nat \4 * ln (1 / \) / ln (ln n\<^sub>0)\)" using assms unfolding m_def by simp - also have "... \ 4 * ln (1 / \) / ln (ln n\<^sub>0)" + also have "... \ 4 * ln (1 / \) / ln (ln n\<^sub>0)" by linarith finally show ?thesis by simp qed lemma n_lbound: "n\<^sub>0 \ exp (exp 5)" "ln n\<^sub>0 \ exp 5" "5 \ ln (ln n\<^sub>0)" "ln n\<^sub>0 > 1" "n\<^sub>0 > 1" proof - show 0:"n\<^sub>0 \ exp (exp 5)" unfolding n\<^sub>0_def by simp have "(1::real) \ exp (exp 5)" by (approximation 5) hence "n\<^sub>0 \ 1" using 0 by argo thus 1:"ln n\<^sub>0 \ exp 5" using 0 by (intro iffD2[OF ln_ge_iff]) auto moreover have "1 < exp (5::real)" by (approximation 5) ultimately show 2:"ln n\<^sub>0 > 1" by argo show "5 \ ln (ln n\<^sub>0)" using 1 2 by (subst ln_ge_iff) simp have "(1::real) < exp (exp 5)" by (approximation 5) thus "n\<^sub>0 > 1" using 0 by argo qed -lemma \1_gt_0: "0 < \\<^sub>i" - using n_lbound(4) \_gt_0 unfolding \\<^sub>i_def +lemma \1_gt_0: "0 < \\<^sub>i" + using n_lbound(4) \_gt_0 unfolding \\<^sub>i_def by (cases "stage_two") simp_all -lemma \1_lt_1: "\\<^sub>i < 1" - using n_lbound(4) \_lt_1 unfolding \\<^sub>i_def +lemma \1_lt_1: "\\<^sub>i < 1" + using n_lbound(4) \_lt_1 unfolding \\<^sub>i_def by (cases "stage_two") simp_all lemma m_gt_0_aux: assumes "stage_two" - shows "1 \ ln (1 / \) / ln (ln n\<^sub>0)" + shows "1 \ ln (1 / \) / ln (ln n\<^sub>0)" proof - - have "ln n\<^sub>0 \ 1 / \" + have "ln n\<^sub>0 \ 1 / \" using n_lbound(4) - using assms unfolding pos_le_divide_eq[OF \_gt_0] stage_two_def + using assms unfolding pos_le_divide_eq[OF \_gt_0] stage_two_def by (simp add:divide_simps ac_simps) - hence "ln (ln n\<^sub>0) \ ln (1 / \)" - using n_lbound(4) \_gt_0 by (intro iffD2[OF ln_le_cancel_iff] divide_pos_pos) auto - thus "1 \ ln (1 / \) / ln (ln n\<^sub>0)" + hence "ln (ln n\<^sub>0) \ ln (1 / \)" + using n_lbound(4) \_gt_0 by (intro iffD2[OF ln_le_cancel_iff] divide_pos_pos) auto + thus "1 \ ln (1 / \) / ln (ln n\<^sub>0)" using n_lbound(3) by (subst pos_le_divide_eq) auto qed lemma m_gt_0: "m > 0" proof (cases "stage_two") case True - have "0 < 4 * ln (1/ \)/ln(ln n\<^sub>0)" + have "0 < 4 * ln (1/ \)/ln(ln n\<^sub>0)" using m_gt_0_aux[OF True] by simp also have "... \ m" using m_lbound[OF True] by simp finally have "0 < real m" by simp then show ?thesis by simp next case False then show ?thesis unfolding m_def by simp qed lemma \_gt_0: "\ > 0" using n_lbound(4) unfolding \_def by (cases "stage_two") auto lemma \_le_1: "\ \ 1" using n_lbound(4) unfolding \_def by (cases "stage_two") simp_all -sublocale I: inner_algorithm "n" "\\<^sub>i" "\" - unfolding inner_algorithm_def using n_gt_0 \_gt_0 \_lt_1 \1_gt_0 \1_lt_1 by auto +sublocale I: inner_algorithm "n" "\\<^sub>i" "\" + unfolding inner_algorithm_def using n_gt_0 \_gt_0 \_lt_1 \1_gt_0 \1_lt_1 by auto abbreviation \ where "\ \ \ m \ I.\" sublocale \: expander_sample_space m \ I.\ unfolding expander_sample_space_def using I.\.sample_space \_gt_0 m_gt_0 by auto type_synonym state = "inner_algorithm.state list" fun single :: "nat \ nat \ state" where "single \ x = map (\j. I.single (select \ \ j) x) [0.. state \ state" where "merge x y = map (\(x,y). I.merge x y) (zip x y)" fun estimate :: "state \ real" where "estimate x = median m (\i. I.estimate (x ! i))" definition \ :: "nat \ nat set \ state" where "\ \ A = map (\i. I.\ (select \ \ i) A) [0..The following three theorems verify the correctness of the algorithm. The term @{term "\"} is a mathematical description of the sketch for a given subset, while @{term "single"}, @{term "merge"} are the actual functions that compute the sketches.\ theorem merge_result: "merge (\ \ A) (\ \ B) = \ \ (A \ B)" (is "?L = ?R") proof - have 0: "zip [0..x. (x,x)) [0..x. I.merge (I.\ (select \ \ x) A) (I.\ (select \ \ x) B)) [0.._def by (simp add:zip_map_map 0 comp_def case_prod_beta) also have "... = map (\x. I.\ (select \ \ x) (A \ B)) [0...range) auto also have "... = ?R" unfolding \_def by simp finally show ?thesis by simp qed theorem single_result: "single \ x = \ \ {x}" (is "?L = ?R") proof - have "?L = map (\j. I.single (select \ \ j) x) [0.._def by (intro map_cong I.single_result \.range) auto finally show ?thesis by simp qed theorem estimate_result: assumes "A \ {.. {}" defines "p \ (pmf_of_set {..})" - shows "measure p {\. \estimate (\ \ A)- real (card A)\ > \ * real (card A)} \ \" (is "?L \ ?R") + shows "measure p {\. \estimate (\ \ A)- real (card A)\ > \ * real (card A)} \ \" (is "?L \ ?R") proof (cases "stage_two") case True - define I where "I = {x. \x - real (card A)\ \ \ * real (card A)}" + define I where "I = {x. \x - real (card A)\ \ \ * real (card A)}" have int_I: "interval I" unfolding interval_def I_def by auto define \ where "\ = measure I.\ {\. I.estimate (I.\ \ A) \ I}" have 0:"\ + \ > 0" unfolding \_def by (intro add_nonneg_pos \_gt_0) auto - have "\ \ \\<^sub>i" + have "\ \ \\<^sub>i" unfolding \_def I_def using I.estimate_result[OF assms(1,2)] by (simp add: not_le del:I.estimate.simps) also have "... = 1/ln n\<^sub>0" - using True unfolding \\<^sub>i_def by simp + using True unfolding \\<^sub>i_def by simp finally have "\ \ 1/ln n\<^sub>0" by simp hence "\ + \ \ 1/ln n\<^sub>0 + 1/ln n\<^sub>0" unfolding \_def using True by (intro add_mono) auto also have "... = 2/ln n\<^sub>0" by simp finally have 1:"\ + \ \ 2 / ln n\<^sub>0" by simp hence 2:"ln n\<^sub>0 \ 2 / (\ + \)" using 0 n_lbound by (simp add:field_simps) have "\ + \ \ 2/ln n\<^sub>0" by (intro 1) also have "... \ 2/exp 5" using n_lbound by (intro divide_left_mono) simp_all also have "... \ 1/2" by (approximation 5) finally have 3:"\ + \ \ 1/2" by simp have 4: "2 * ln 2 + 8 * exp (- 1) \ (5::real)" by (approximation 5) have "?L = measure p {\. median m (\i. I.estimate (\ \ A ! i)) \ I}" unfolding I_def by (simp add:not_le) also have "... \ measure p {\. real (card {i \ {.. (select \ \ i) A) \ I})\ real m/2}" proof (rule pmf_mono) fix \ assume "\ \ set_pmf p" assume a:"\ \ {\. median m (\i. I.estimate (\ \ A ! i)) \ I}" have "real m = 2 * real m - real m" by simp also have "... \ 2 * real m - 2 * card {i. i < m \ I.estimate (\ \ A ! i) \ I}" using median_est[OF int_I, where n="m"] a by (intro diff_left_mono Nat.of_nat_mono) (auto simp add:not_less[symmetric] simp del:I.estimate.simps) also have "... = 2 * (real (card {.. I.estimate (\ \ A ! i) \ I})" by (simp del:I.estimate.simps) also have "... = 2 * real (card {.. I.estimate (\ \ A ! i) \ I})" by (intro_cong "[\\<^sub>2 (*)]" more:of_nat_diff[symmetric] card_mono) (auto simp del:I.estimate.simps) also have "... = 2 * real (card ({.. I.estimate (\ \ A ! i) \ I}))" by (intro_cong "[\\<^sub>2 (*), \\<^sub>1 of_nat]" more:card_Diff_subset[symmetric]) (auto simp del:I.estimate.simps) also have "... = 2 * real (card {i\{.. \ A ! i) \ I})" by (intro_cong "[\\<^sub>2 (*), \\<^sub>1 of_nat, \\<^sub>1 card]") (auto simp del:I.estimate.simps) also have "... = 2 * real (card {i \ {.. (select \ \ i) A) \ I})" unfolding \_def by (intro_cong "[\\<^sub>2 (*), \\<^sub>1 of_nat, \\<^sub>1 card]" more:restr_Collect_cong) (simp del:I.estimate.simps) finally have "real m \ 2 * real (card {i \ {.. (select \ \ i) A) \ I})" by simp thus "\ \ {\. real m / 2 \ real (card {i \ {.. (select \ \ i) A) \ I})}" by simp qed also have "...=measure \{\. real(card {i \ {.. (\ i) A) \ I})\(1/2)*real m}" unfolding sample_pmf_alt[OF \.sample_space] p_def by (simp del:I.estimate.simps) also have "... \ exp (-real m * ((1/2) * ln (1/ (\ + \)) - 2*exp (-1)))" using 3 m_gt_0 \_gt_0 unfolding \_def by (intro \.tail_bound) force+ also have "... \ exp (-real m * ((1/2) * ln (ln n\<^sub>0 / 2) - 2*exp (-1)))" using 0 2 3 n_lbound by (intro iffD2[OF exp_le_cancel_iff] mult_right_mono mult_left_mono_neg[where c="-real m"] diff_mono mult_left_mono iffD2[OF ln_le_cancel_iff]) (simp_all) also have "... = exp (-real m * (ln (ln n\<^sub>0) / 2 - (ln 2/2 + 2*exp (-1))))" using n_lbound by (subst ln_div) (simp_all add:algebra_simps) also have "... \ exp (-real m * (ln (ln n\<^sub>0) / 2 - (ln (ln (exp(exp 5))) / 4)))" using 4 by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg[where c="-real m"] diff_mono) simp_all also have "... \ exp (-real m * (ln (ln n\<^sub>0) / 2 - (ln (ln n\<^sub>0) / 4)))" using n_lbound by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg[where c="-real m"] diff_mono) simp_all also have "... = exp (- real m * (ln (ln n\<^sub>0)/ 4) )" by (simp add:algebra_simps) - also have "... \ exp (- (4 * ln (1/ \)/ln(ln n\<^sub>0)) * (ln (ln n\<^sub>0)/4))" + also have "... \ exp (- (4 * ln (1/ \)/ln(ln n\<^sub>0)) * (ln (ln n\<^sub>0)/4))" using m_lbound[OF True] n_lbound by (intro iffD2[OF exp_le_cancel_iff] mult_right_mono divide_nonneg_pos) simp_all - also have "... = exp (- ln (1/ \))" + also have "... = exp (- ln (1/ \))" using n_lbound by simp - also have "... = \" - using \_gt_0 by (subst ln_inverse[symmetric]) auto + also have "... = \" + using \_gt_0 by (subst ln_inverse[symmetric]) auto finally show ?thesis by simp next case False have m_eq: "m = 1" unfolding m_def using False by simp - hence "?L = measure p {\. \ * real (card A) < \I.estimate (\ \ A ! 0) - real (card A)\}" + hence "?L = measure p {\. \ * real (card A) < \I.estimate (\ \ A ! 0) - real (card A)\}" unfolding estimate.simps m_eq median_def by simp - also have "... = measure p {\. \*real(card A)<\I.estimate (I.\ (select \ \ 0) A)-real(card A)\}" + also have "... = measure p {\. \*real(card A)<\I.estimate (I.\ (select \ \ 0) A)-real(card A)\}" unfolding \_def m_eq by (simp del: I.estimate.simps) - also have "... = measure \ {\. \*real(card A) < \I.estimate (I.\ (\ 0) A)-real(card A)\}" + also have "... = measure \ {\. \*real(card A) < \I.estimate (I.\ (\ 0) A)-real(card A)\}" unfolding sample_pmf_alt[OF \.sample_space] p_def by (simp del:I.estimate.simps) also have "...= - measure (map_pmf (\\. \ 0) \) {\. \*real(card A) < \I.estimate (I.\ \ A)-real(card A)\}" + measure (map_pmf (\\. \ 0) \) {\. \*real(card A) < \I.estimate (I.\ \ A)-real(card A)\}" by simp - also have "... = measure I.\ {\. \*real(card A) < \I.estimate (I.\ \ A)-real(card A)\}" + also have "... = measure I.\ {\. \*real(card A) < \I.estimate (I.\ \ A)-real(card A)\}" using m_eq by (subst \.uniform_property) auto - also have "... \ \\<^sub>i" + also have "... \ \\<^sub>i" by (intro I.estimate_result[OF assms(1,2)]) also have "... = ?R" - unfolding \\<^sub>i_def using False by simp + unfolding \\<^sub>i_def using False by simp finally show ?thesis by simp qed text \The function @{term "encode_state"} can represent states as bit strings. This enables verification of the space usage.\ definition encode_state where "encode_state = Lf\<^sub>e I.encode_state m" lemma encode_state: "is_encoding encode_state" unfolding encode_state_def by (intro fixed_list_encoding I.encode_state) lemma state_bit_count: - "bit_count (encode_state (\ \ A)) \ state_space_usage (real n, \, \)" + "bit_count (encode_state (\ \ A)) \ state_space_usage (real n, \, \)" (is "?L \ ?R") proof - have 0: "length (\ \ A) = m" unfolding \_def by simp have "?L = (\x\\ \ A. bit_count (I.encode_state x))" using 0 unfolding encode_state_def fixed_list_bit_count by simp also have "... = (\x\[0.. (select \ \ x) A)))" unfolding \_def by (simp add:comp_def) - also have "... \ (\x\[0..\<^sub>i)+ 1)/\\<^sup>2 + log 2 (log 2 (real n) + 3)))" + also have "... \ (\x\[0..\<^sub>i)+ 1)/\\<^sup>2 + log 2 (log 2 (real n) + 3)))" using I.state_bit_count by (intro sum_list_mono I.state_bit_count \.range) - also have "... = ereal ( real m * (2^36 *(ln (1/\\<^sub>i)+ 1)/\\<^sup>2 + log 2 (log 2 (real n) + 3)))" + also have "... = ereal ( real m * (2^36 *(ln (1/\\<^sub>i)+ 1)/\\<^sup>2 + log 2 (log 2 (real n) + 3)))" unfolding sum_list_triv_ereal by simp - also have "... \ 2^40 * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3)" (is "?L1 \ ?R1") + also have "... \ 2^40 * (ln(1/\)+1)/ \^2 + log 2 (log 2 n + 3)" (is "?L1 \ ?R1") proof (cases "stage_two") case True - have "\4*ln (1/\)/ln(ln n\<^sub>0)\ \ 4*ln (1/\)/ln(ln n\<^sub>0) + 1" + have "\4*ln (1/\)/ln(ln n\<^sub>0)\ \ 4*ln (1/\)/ln(ln n\<^sub>0) + 1" by simp - also have "... \ 4*ln (1/\)/ln(ln n\<^sub>0) + ln (1/\)/ln(ln n\<^sub>0)" + also have "... \ 4*ln (1/\)/ln(ln n\<^sub>0) + ln (1/\)/ln(ln n\<^sub>0)" using m_gt_0_aux[OF True] by (intro add_mono) auto - also have "... = 5 * ln (1/\)/ln(ln n\<^sub>0)" by simp - finally have 3: "\4*ln (1/\)/ln(ln n\<^sub>0)\ \ 5 * ln (1/\)/ln(ln n\<^sub>0)" + also have "... = 5 * ln (1/\)/ln(ln n\<^sub>0)" by simp + finally have 3: "\4*ln (1/\)/ln(ln n\<^sub>0)\ \ 5 * ln (1/\)/ln(ln n\<^sub>0)" by simp have 4: "0 \ log 2 (log 2 (real n) + 3)" using n_gt_0 by (intro iffD2[OF zero_le_log_cancel_iff] add_nonneg_pos) auto have 5: "1 / ln 2 + 3 / exp 5 \ exp (1::real)" "1.2 / ln 2 \ (2::real)" by (approximation 5)+ have "log 2(log 2 (real n)+3) \ log 2 (log 2 n\<^sub>0 + 3)" using n_gt_0 by (intro iffD2[OF log_le_cancel_iff] add_mono add_nonneg_pos iffD2[OF zero_le_log_cancel_iff]) (simp_all add:n\<^sub>0_def) also have "... = ln (ln n\<^sub>0 / ln 2 + 3) / ln 2" unfolding log_def by simp also have "... \ ln (ln n\<^sub>0/ln 2 + (3 / exp 5) * ln n\<^sub>0) / ln 2" using n_lbound by (intro divide_right_mono iffD2[OF ln_le_cancel_iff] add_mono add_nonneg_pos) (simp_all add:divide_simps) also have "... = ln ( ln n\<^sub>0 * (1 /ln 2 + 3/exp 5)) / ln 2" by (simp add:algebra_simps) also have "... \ ln ( ln n\<^sub>0 * exp 1) / ln 2" using n_lbound by (intro divide_right_mono iffD2[OF ln_le_cancel_iff] add_mono mult_left_mono 5 Rings.mult_pos_pos add_pos_nonneg) auto also have "... = (ln (ln n\<^sub>0) + 1) / ln 2" using n_lbound by (subst ln_mult) simp_all also have "... \ (ln (ln n\<^sub>0) + 0.2 * ln (ln n\<^sub>0)) / ln 2" using n_lbound by (intro divide_right_mono add_mono) auto also have "... = (1.2/ ln 2) * ln (ln n\<^sub>0)" by simp also have "... \ 2 * ln (ln n\<^sub>0)" using n_lbound by (intro mult_right_mono 5) simp finally have "log 2(log 2 (real n)+3) \ 2 * ln (ln n\<^sub>0)" by simp hence 6: "log 2(log 2 (real n)+3)/ln(ln n\<^sub>0) \ 2" using n_lbound by (subst pos_divide_le_eq) simp_all - have "?L1 = real(nat \4*ln (1/\)/ln(ln n\<^sub>0)\)*(2^36*(ln (ln n\<^sub>0)+1)/\^2+log 2(log 2 (real n)+3))" - using True unfolding m_def \\<^sub>i_def by simp - also have "... = \4*ln (1/\)/ln(ln n\<^sub>0)\*(2^36*(ln (ln n\<^sub>0)+1)/\^2+log 2(log 2 (real n)+3))" + have "?L1 = real(nat \4*ln (1/\)/ln(ln n\<^sub>0)\)*(2^36*(ln (ln n\<^sub>0)+1)/\^2+log 2(log 2 (real n)+3))" + using True unfolding m_def \\<^sub>i_def by simp + also have "... = \4*ln (1/\)/ln(ln n\<^sub>0)\*(2^36*(ln (ln n\<^sub>0)+1)/\^2+log 2(log 2 (real n)+3))" using m_gt_0_aux[OF True] by (subst of_nat_nat) simp_all - also have "... \ (5*ln (1/\)/ln(ln n\<^sub>0)) *(2^36*(ln (ln n\<^sub>0)+1)/\^2+log 2(log 2 (real n)+3))" - using n_lbound(3) \_gt_0 4 by (intro ereal_mono mult_right_mono + also have "... \ (5*ln (1/\)/ln(ln n\<^sub>0)) *(2^36*(ln (ln n\<^sub>0)+1)/\^2+log 2(log 2 (real n)+3))" + using n_lbound(3) \_gt_0 4 by (intro ereal_mono mult_right_mono add_nonneg_nonneg divide_nonneg_pos mult_nonneg_nonneg 3) simp_all - also have "... \ (5 * ln (1/\)/ln(ln n\<^sub>0))*((2^36+2^36)*ln (ln n\<^sub>0)/\^2+log 2(log 2 (real n)+3))" - using n_lbound \_gt_0 \_lt_1 + also have "... \ (5 * ln (1/\)/ln(ln n\<^sub>0))*((2^36+2^36)*ln (ln n\<^sub>0)/\^2+log 2(log 2 (real n)+3))" + using n_lbound \_gt_0 \_lt_1 by (intro ereal_mono mult_left_mono add_mono divide_right_mono divide_nonneg_pos) auto - also have "... = 5*(2^37)* ln (1/\)/ \^2 + (5*ln (1/\)) * (log 2(log 2 (real n)+3)/ln(ln n\<^sub>0))" + also have "... = 5*(2^37)* ln (1/\)/ \^2 + (5*ln (1/\)) * (log 2(log 2 (real n)+3)/ln(ln n\<^sub>0))" using n_lbound by (simp add:algebra_simps) - also have "... \ 5*(2^37)* ln (1/\)/ \^2 + (5*ln(1/ \)) * 2" - using \_gt_0 \_lt_1 by (intro add_mono ereal_mono order.refl mult_left_mono 6) auto - also have "... = 5*(2^37)* ln (1/\)/ \^2 + 5*2*ln(1/ \) / 1" + also have "... \ 5*(2^37)* ln (1/\)/ \^2 + (5*ln(1/ \)) * 2" + using \_gt_0 \_lt_1 by (intro add_mono ereal_mono order.refl mult_left_mono 6) auto + also have "... = 5*(2^37)* ln (1/\)/ \^2 + 5*2*ln(1/ \) / 1" by simp - also have "... \ 5*(2^37)* ln (1/\)/ \^2 + 5*2*ln(1/ \) / \^2" - using \_gt_0 \_lt_1 \_gt_0 \_lt_1 + also have "... \ 5*(2^37)* ln (1/\)/ \^2 + 5*2*ln(1/ \) / \^2" + using \_gt_0 \_lt_1 \_gt_0 \_lt_1 by (intro add_mono ereal_mono divide_left_mono Rings.mult_pos_pos power_le_one) auto - also have "... = (5*(2^37+2))* (ln (1/\)+0)/ \^2 + 0" + also have "... = (5*(2^37+2))* (ln (1/\)+0)/ \^2 + 0" by (simp add:algebra_simps) - also have "... \ 2^40 * (ln (1 / \)+1) / \^2 + log 2 (log 2 (real n) + 3)" - using \_gt_0 \_lt_1 \_gt_0 \_lt_1 n_gt_0 by (intro add_mono ereal_mono divide_right_mono + also have "... \ 2^40 * (ln (1 / \)+1) / \^2 + log 2 (log 2 (real n) + 3)" + using \_gt_0 \_lt_1 \_gt_0 \_lt_1 n_gt_0 by (intro add_mono ereal_mono divide_right_mono mult_right_mono iffD2[OF zero_le_log_cancel_iff] add_nonneg_pos) auto finally show ?thesis by simp next case False - have "?L1 = 2^36 *(ln (1/\)+ 1)/\\<^sup>2 + log 2 (log 2 (real n) + 3)" - using False unfolding \\<^sub>i_def m_def by simp + have "?L1 = 2^36 *(ln (1/\)+ 1)/\\<^sup>2 + log 2 (log 2 (real n) + 3)" + using False unfolding \\<^sub>i_def m_def by simp also have "... \ ?R1" - using \_gt_0 \_lt_1 \_gt_0 \_lt_1 + using \_gt_0 \_lt_1 \_gt_0 \_lt_1 by (intro ereal_mono add_mono divide_right_mono mult_right_mono add_nonneg_nonneg) auto finally show ?thesis by simp qed finally show ?thesis unfolding state_space_usage_def by simp qed text \Encoding function for the seeds which are just natural numbers smaller than @{term "size \"}.\ definition encode_seed where "encode_seed = Nb\<^sub>e (size \)" lemma encode_seed: "is_encoding encode_seed" unfolding encode_seed_def by (intro bounded_nat_encoding) lemma random_bit_count: assumes "\ < size \" - shows "bit_count (encode_seed \) \ seed_space_usage (real n, \, \)" + shows "bit_count (encode_seed \) \ seed_space_usage (real n, \, \)" (is "?L \ ?R") proof - have 0: "size \ > 0" using \.sample_space unfolding sample_space_def by simp have 1: "size I.\ > 0" using I.\.sample_space unfolding sample_space_def by simp have "(55+60*ln (ln n\<^sub>0))^3 \ (180+60*ln (ln n\<^sub>0))^3" using n_lbound by (intro power_mono add_mono) auto also have "... = 180^3 * (1+ln (ln n\<^sub>0)/real 3)^3" unfolding power_mult_distrib[symmetric] by simp also have "... \ 180^3 * exp (ln (ln n\<^sub>0))" using n_lbound by (intro mult_left_mono exp_ge_one_plus_x_over_n_power_n) auto also have "... = 180^3 * ln n\<^sub>0" using n_lbound by (subst exp_ln) auto also have "... \ 180^3 * max (ln n) (ln (exp (exp 5)))" using n_gt_0 unfolding n\<^sub>0_def by (subst ln_max_swap) auto also have "... \ 180^3 * (ln n + exp 5)" using n_gt_0 unfolding ln_exp by (intro mult_left_mono) auto finally have 2:"(55+60*ln (ln n\<^sub>0))^3 \ 180^3 * ln n + 180^3*exp 5" by simp have 3:"(1::real)+180^3*exp 5 \ 2^30" "(4::real)/ln 2 + 180^3 \ 2^23" by (approximation 10)+ have "?L = ereal (real (floorlog 2 (size \ - 1)))" using assms unfolding encode_seed_def bounded_nat_bit_count by simp also have "... \ ereal (real (floorlog 2 (size \)))" by (intro ereal_mono Nat.of_nat_mono floorlog_mono) auto also have "... = ereal (1 + of_int \log 2 (real (sample_space.size \))\)" using 0 unfolding floorlog_def by simp also have "... \ ereal (1 + log 2 (real (size \)))" by (intro add_mono ereal_mono) auto also have "... = 1 + log 2 (real (size I.\) * (2^4) ^ ((m - 1) * nat \ln \ / ln 0.95\))" unfolding \.size by simp also have "... = 1 + log 2 (real (size I.\) * 2^ (4 * (m - 1) * nat \ln \ / ln 0.95\))" unfolding power_mult by simp also have "... = 1 + log 2 (real (size I.\)) + (4*(m-1)* nat\ln \ / ln 0.95\)" using 1 by (subst log_mult) simp_all - also have "... \ 1+log 2(2 powr (4*log 2 n + 48 * (log 2 (1/\)+16)\<^sup>2+ (55+60*ln (1/\\<^sub>i))^3))+ + also have "... \ 1+log 2(2 powr (4*log 2 n + 48 * (log 2 (1/\)+16)\<^sup>2+ (55+60*ln (1/\\<^sub>i))^3))+ (4*(m-1)* nat\ln \ / ln 0.95\)" using 1 by (intro ereal_mono add_mono iffD2[OF log_le_cancel_iff] I.random_bit_count) auto - also have "...=1+4*log 2 n+48*(log 2(1/\)+16)\<^sup>2+(55+60*ln (1/\\<^sub>i))^3+(4*(m-1)*nat\ln \/ln 0.95\)" + also have "...=1+4*log 2 n+48*(log 2(1/\)+16)\<^sup>2+(55+60*ln (1/\\<^sub>i))^3+(4*(m-1)*nat\ln \/ln 0.95\)" by (subst log_powr_cancel) auto - also have "... \ 2^30 + 2^23*ln n+48*(log 2(1/\)+16)\<^sup>2 + 336*ln (1/\)" (is "?L1 \ ?R1") + also have "... \ 2^30 + 2^23*ln n+48*(log 2(1/\)+16)\<^sup>2 + 336*ln (1/\)" (is "?L1 \ ?R1") proof (cases "stage_two") case True have "-1 < (0::real)" by simp also have "... \ ln \ / ln 0.95" using \_gt_0 \_le_1 by (intro divide_nonpos_neg) auto finally have 4: "- 1 < ln \ / ln 0.95" by simp have 5: "- 1 / ln 0.95 \ (20::real)" by (approximation 10) have "(4*(m-1)*nat\ln \/ln 0.95\) = 4 * (real m-1) * of_int \ln \/ln 0.95\" using 4 m_gt_0 unfolding of_nat_mult by (subst of_nat_nat) auto also have "... \ 4 * (real m-1) * (ln \/ln 0.95 + 1)" using m_gt_0 by (intro mult_left_mono) auto also have "... = 4 * (real m-1) * (-ln (ln n\<^sub>0)/ln 0.95 + 1)" using n_lbound True unfolding \_def by (subst ln_inverse[symmetric]) (simp_all add:inverse_eq_divide) also have "... = 4 * (real m - 1 ) * (ln (ln n\<^sub>0) * (-1/ln 0.95) + 1)" by simp also have "... \ 4 * (real m - 1 ) * (ln (ln n\<^sub>0) * 20 + 1)" using n_lbound m_gt_0 by (intro mult_left_mono add_mono 5) auto - also have "... = 4 * (real (nat \4 * ln (1 / \) / ln (ln n\<^sub>0)\)-1) * (ln (ln n\<^sub>0) * 20 + 1)" + also have "... = 4 * (real (nat \4 * ln (1 / \) / ln (ln n\<^sub>0)\)-1) * (ln (ln n\<^sub>0) * 20 + 1)" using True unfolding m_def by simp - also have "... = 4 * (real_of_int \4 * ln (1 / \) / ln (ln n\<^sub>0)\-1) * (ln (ln n\<^sub>0) * 20 + 1)" + also have "... = 4 * (real_of_int \4 * ln (1 / \) / ln (ln n\<^sub>0)\-1) * (ln (ln n\<^sub>0) * 20 + 1)" using m_gt_0_aux[OF True] by (subst of_nat_nat) simp_all - also have "... \ 4 * (4 * ln (1 / \) / ln (ln n\<^sub>0)) * (ln (ln n\<^sub>0) * 20 + 1)" + also have "... \ 4 * (4 * ln (1 / \) / ln (ln n\<^sub>0)) * (ln (ln n\<^sub>0) * 20 + 1)" using n_lbound by (intro mult_left_mono mult_right_mono) auto - also have "... \ 4 * (4 * ln (1 / \) / ln (ln n\<^sub>0)) * (ln (ln n\<^sub>0) * 20 + ln (ln n\<^sub>0))" - using \_gt_0 \_lt_1 n_lbound + also have "... \ 4 * (4 * ln (1 / \) / ln (ln n\<^sub>0)) * (ln (ln n\<^sub>0) * 20 + ln (ln n\<^sub>0))" + using \_gt_0 \_lt_1 n_lbound by (intro mult_left_mono mult_right_mono add_mono divide_nonneg_pos Rings.mult_nonneg_nonneg) simp_all - also have "... = 336 * ln (1 / \)" + also have "... = 336 * ln (1 / \)" using n_lbound by simp - finally have 6: "4 * (m-1) * nat \ln \/ln 0.95\ \ 336 * ln (1/\)" + finally have 6: "4 * (m-1) * nat \ln \/ln 0.95\ \ 336 * ln (1/\)" by simp - have "?L1 =1+4*log 2 n+48*(log 2(1/\)+16)\<^sup>2+(55+60*ln (ln n\<^sub>0))^3+(4*(m-1)*nat\ln \/ln 0.95\)" - using True unfolding \\<^sub>i_def by simp - also have "... \ 1+4*log 2 n+48*(log 2(1/\)+16)\<^sup>2+(180^3 * ln n + 180^3*exp 5) + 336 * ln (1/\)" + have "?L1 =1+4*log 2 n+48*(log 2(1/\)+16)\<^sup>2+(55+60*ln (ln n\<^sub>0))^3+(4*(m-1)*nat\ln \/ln 0.95\)" + using True unfolding \\<^sub>i_def by simp + also have "... \ 1+4*log 2 n+48*(log 2(1/\)+16)\<^sup>2+(180^3 * ln n + 180^3*exp 5) + 336 * ln (1/\)" by (intro add_mono 6 2 ereal_mono order.refl) - also have "... = (1+180^3*exp 5)+ (4/ln 2 + 180^3)*ln n+48*(log 2(1/\)+16)\<^sup>2+ 336 * ln (1/\)" + also have "... = (1+180^3*exp 5)+ (4/ln 2 + 180^3)*ln n+48*(log 2(1/\)+16)\<^sup>2+ 336 * ln (1/\)" by (simp add:log_def algebra_simps) - also have "... \ 2^30 + 2^23*ln n+48*(log 2(1/\)+16)\<^sup>2+ 336 * ln (1/\)" + also have "... \ 2^30 + 2^23*ln n+48*(log 2(1/\)+16)\<^sup>2+ 336 * ln (1/\)" using n_gt_0 by (intro add_mono ereal_mono 3 order.refl mult_right_mono) auto finally show ?thesis by simp next case False - hence "1 / \ \ ln n\<^sub>0" - using \_gt_0 n_lbound + hence "1 / \ \ ln n\<^sub>0" + using \_gt_0 n_lbound unfolding stage_two_def not_less by (simp add:divide_simps ac_simps) - hence 7: "ln (1 / \) \ ln (ln n\<^sub>0)" - using n_lbound \_gt_0 \_lt_1 + hence 7: "ln (1 / \) \ ln (ln n\<^sub>0)" + using n_lbound \_gt_0 \_lt_1 by (intro iffD2[OF ln_le_cancel_iff]) auto - have 8: "0 \ 336*ln (1/\) " - using \_gt_0 \_lt_1 by auto + have 8: "0 \ 336*ln (1/\) " + using \_gt_0 \_lt_1 by auto - have "?L1 = 1 + 4 * log 2 (real n) + 48 * (log 2 (1 / \) + 16)\<^sup>2 + (55 + 60 * ln (1 / \)) ^ 3" - using False unfolding \\<^sub>i_def m_def by simp - also have "... \ 1 + 4 * log 2 (real n) + 48 * (log 2 (1 / \) + 16)\<^sup>2 + (55 + 60 * ln (ln n\<^sub>0))^3" - using \_gt_0 \_lt_1 + have "?L1 = 1 + 4 * log 2 (real n) + 48 * (log 2 (1 / \) + 16)\<^sup>2 + (55 + 60 * ln (1 / \)) ^ 3" + using False unfolding \\<^sub>i_def m_def by simp + also have "... \ 1 + 4 * log 2 (real n) + 48 * (log 2 (1 / \) + 16)\<^sup>2 + (55 + 60 * ln (ln n\<^sub>0))^3" + using \_gt_0 \_lt_1 by (intro add_mono order.refl ereal_mono power_mono mult_left_mono add_nonneg_nonneg 7) auto - also have "... \ 1+4*log 2(real n)+48*(log 2 (1 / \)+16)\<^sup>2+(180^3*ln (real n) + 180 ^ 3 * exp 5)" + also have "... \ 1+4*log 2(real n)+48*(log 2 (1 / \)+16)\<^sup>2+(180^3*ln (real n) + 180 ^ 3 * exp 5)" by (intro add_mono ereal_mono 2 order.refl) - also have "... = (1+180^3*exp 5)+ (4/ln 2 + 180^3)*ln n+48*(log 2(1/\)+16)\<^sup>2+ 0" + also have "... = (1+180^3*exp 5)+ (4/ln 2 + 180^3)*ln n+48*(log 2(1/\)+16)\<^sup>2+ 0" by (simp add:log_def algebra_simps) - also have "... \ 2^30 + 2^23*ln n+48*(log 2(1/\)+16)\<^sup>2 + 336*ln (1/\)" + also have "... \ 2^30 + 2^23*ln n+48*(log 2(1/\)+16)\<^sup>2 + 336*ln (1/\)" using n_gt_0 by (intro add_mono ereal_mono 3 order.refl mult_right_mono 8) auto finally show ?thesis by simp qed - also have "... = seed_space_usage (real n, \, \)" + also have "... = seed_space_usage (real n, \, \)" unfolding seed_space_usage_def by simp finally show ?thesis by simp qed text \The following is an alternative form expressing the correctness and space usage theorems. If @{term "x"} is expression formed by @{term "single"} and @{term "merge"} operations. Then -@{term "x"} requires @{term "state_space_usage (real n, \, \)"} bits to encode and +@{term "x"} requires @{term "state_space_usage (real n, \, \)"} bits to encode and @{term "estimate x"} approximates the count of the distinct universe elements in the expression. For example: @{term "estimate (merge (single \ 1) (merge (single \ 5) (single \ 1)))"} approximates the cardinality of @{term "{1::nat, 5, 1}"} i.e. $2$.\ datatype sketch_tree = Single nat | Merge sketch_tree sketch_tree fun eval :: "nat \ sketch_tree \ state" where "eval \ (Single x) = single \ x" | "eval \ (Merge x y) = merge (eval \ x) (eval \ y)" fun sketch_tree_set :: "sketch_tree \ nat set" where "sketch_tree_set (Single x) = {x}" | "sketch_tree_set (Merge x y) = sketch_tree_set x \ sketch_tree_set y" theorem correctness: fixes X assumes "sketch_tree_set t \ {.. pmf_of_set {..}" defines "X \ real (card (sketch_tree_set t))" - shows "measure p {\. \estimate (eval \ t) - X\ > \ * X} \ \" (is "?L \ ?R") + shows "measure p {\. \estimate (eval \ t) - X\ > \ * X} \ \" (is "?L \ ?R") proof - define A where "A = sketch_tree_set t" have X_eq: "X = real (card A)" unfolding X_def A_def by simp have 0:"eval \ t = \ \ A" for \ unfolding A_def using single_result merge_result by (induction t) (auto simp del:merge.simps single.simps) have 1: "A \ {.. {}" unfolding A_def by (induction t) auto show ?thesis unfolding 0 X_eq p_def by (intro estimate_result 1 2) qed theorem space_usage: assumes "\ < size \" shows - "bit_count (encode_state (eval \ t)) \ state_space_usage (real n, \, \)" (is "?A") - "bit_count (encode_seed \) \ seed_space_usage (real n, \, \)" (is "?B") + "bit_count (encode_state (eval \ t)) \ state_space_usage (real n, \, \)" (is "?A") + "bit_count (encode_seed \) \ seed_space_usage (real n, \, \)" (is "?B") proof- define A where "A = sketch_tree_set t" have 0:"eval \ t = \ \ A" for \ unfolding A_def using single_result merge_result by (induction t) (auto simp del:merge.simps single.simps) show ?A unfolding 0 by (intro state_bit_count) show ?B using random_bit_count[OF assms] by simp qed end text \The functions @{term "state_space_usage"} and @{term "seed_space_usage"} are exact bounds on the space usage for the state and the seed. The following establishes asymptotic bounds with respect to the limit $n, \delta^{-1}, \varepsilon^{-1} \rightarrow \infty$.\ context begin text \Some local notation to ease proofs about the asymptotic space usage of the algorithm:\ -private definition n_of :: "real \ real \ real \ real" where "n_of = (\(n, \, \). n)" -private definition \_of :: "real \ real \ real \ real" where "\_of = (\(n, \, \). \)" -private definition \_of :: "real \ real \ real \ real" where "\_of = (\(n, \, \). \)" +private definition n_of :: "real \ real \ real \ real" where "n_of = (\(n, \, \). n)" +private definition \_of :: "real \ real \ real \ real" where "\_of = (\(n, \, \). \)" +private definition \_of :: "real \ real \ real \ real" where "\_of = (\(n, \, \). \)" private abbreviation F :: "(real \ real \ real) filter" where "F \ (at_top \\<^sub>F at_right 0 \\<^sub>F at_right 0)" private lemma var_simps: "n_of = fst" - "\_of = (\x. fst (snd x))" - "\_of = (\x. snd (snd x))" - unfolding n_of_def \_of_def \_of_def by (auto simp add:case_prod_beta) + "\_of = (\x. fst (snd x))" + "\_of = (\x. snd (snd x))" + unfolding n_of_def \_of_def \_of_def by (auto simp add:case_prod_beta) private lemma evt_n: "eventually (\x. n_of x \ n) F" unfolding var_simps by (intro eventually_prod1' eventually_prod2' eventually_ge_at_top) (simp add:prod_filter_eq_bot) private lemma evt_n_1: "\\<^sub>F x in F. 0 \ ln (n_of x)" by (intro eventually_mono[OF evt_n[of "1"]] ln_ge_zero) simp private lemma evt_n_2: "\\<^sub>F x in F. 0 \ ln (ln (n_of x))" using order_less_le_trans[OF exp_gt_zero] by (intro eventually_mono[OF evt_n[of "exp 1"]] ln_ge_zero iffD2[OF ln_ge_iff]) auto -private lemma evt_\: "eventually (\x. 1/\_of x \ \ \ \_of x > 0) F" - unfolding var_simps by (intro eventually_prod1' eventually_prod2' eventually_conj - real_inv_at_right_0_inf eventually_at_right_less) (simp_all add:prod_filter_eq_bot) - private lemma evt_\: "eventually (\x. 1/\_of x \ \ \ \_of x > 0) F" unfolding var_simps by (intro eventually_prod1' eventually_prod2' eventually_conj real_inv_at_right_0_inf eventually_at_right_less) (simp_all add:prod_filter_eq_bot) -private lemma evt_\_1: "\\<^sub>F x in F. 0 \ ln (1 / \_of x)" - by (intro eventually_mono[OF evt_\[of "1"]] ln_ge_zero) simp +private lemma evt_\: "eventually (\x. 1/\_of x \ \ \ \_of x > 0) F" + unfolding var_simps by (intro eventually_prod1' eventually_prod2' eventually_conj + real_inv_at_right_0_inf eventually_at_right_less) (simp_all add:prod_filter_eq_bot) + +private lemma evt_\_1: "\\<^sub>F x in F. 0 \ ln (1 / \_of x)" + by (intro eventually_mono[OF evt_\[of "1"]] ln_ge_zero) simp theorem asymptotic_state_space_complexity: - "state_space_usage \ O[F](\(n, \, \). ln (1/\)/\^2 + ln (ln n))" + "state_space_usage \ O[F](\(n, \, \). ln (1/\)/\^2 + ln (ln n))" (is "_ \ O[?F](?rhs)") proof - - have 0:"(\x. 1) \ O[?F](\x. ln (1 / \_of x))" + have 0:"(\x. 1) \ O[?F](\x. ln (1 / \_of x))" using order_less_le_trans[OF exp_gt_zero] - by (intro landau_o.big_mono eventually_mono[OF evt_\[of "exp 1"]]) + by (intro landau_o.big_mono eventually_mono[OF evt_\[of "exp 1"]]) (auto intro!: iffD2[OF ln_ge_iff] simp add:abs_ge_iff) have 1:"(\x. 1) \ O[?F](\x. ln (n_of x))" using order_less_le_trans[OF exp_gt_zero] by (intro landau_o.big_mono eventually_mono[OF evt_n[of "exp 1"]]) (auto intro!:iffD2[OF ln_ge_iff] simp add:abs_ge_iff) - have "(\x. ((ln (1/\_of x)+1)* (1/\_of x)\<^sup>2))\ O[?F](\x. ln(1/\_of x)* (1/\_of x)\<^sup>2)" + have "(\x. ((ln (1/\_of x)+1)* (1/\_of x)\<^sup>2))\ O[?F](\x. ln(1/\_of x)* (1/\_of x)\<^sup>2)" by (intro landau_o.mult sum_in_bigo 0) simp_all - hence 2: "(\x. 2^40*((ln (1/\_of x)+1)* (1/\_of x)\<^sup>2))\ O[?F](\x. ln(1/\_of x)* (1/\_of x)\<^sup>2)" + hence 2: "(\x. 2^40*((ln (1/\_of x)+1)* (1/\_of x)\<^sup>2))\ O[?F](\x. ln(1/\_of x)* (1/\_of x)\<^sup>2)" unfolding cmult_in_bigo_iff by simp have 3: "(1::real) \ exp 2" by (approximation 5) have "(\x. ln (n_of x) / ln 2 + 3) \ O[?F](\x. ln (n_of x))" using 1 by (intro sum_in_bigo) simp_all hence "(\x. ln (ln (n_of x) / ln 2 + 3)) \ O[?F](\x. ln (ln (n_of x)))" using order_less_le_trans[OF exp_gt_zero] order_trans[OF 3] by (intro landau_ln_2[where a="2"] eventually_mono[OF evt_n[of "exp 2"]]) (auto intro!:iffD2[OF ln_ge_iff] add_nonneg_nonneg divide_nonneg_pos) hence 4: "(\x. log 2 (log 2 (n_of x) + 3))\ O[?F](\x. ln(ln(n_of x)))" unfolding log_def by simp - have 5: "\\<^sub>F x in ?F. 0 \ ln (1 / \_of x) * (1 / \_of x)\<^sup>2" - by (intro eventually_mono[OF eventually_conj[OF evt_\_1 evt_\[of "1"]]]) auto + have 5: "\\<^sub>F x in ?F. 0 \ ln (1 / \_of x) * (1 / \_of x)\<^sup>2" + by (intro eventually_mono[OF eventually_conj[OF evt_\_1 evt_\[of "1"]]]) auto - have "state_space_usage = (\x. state_space_usage (n_of x, \_of x, \_of x))" - by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) - also have "... = (\x. 2 ^ 40 * ((ln (1 / (\_of x)) + 1)* (1/\_of x)\<^sup>2) + log 2 (log 2 (n_of x)+3))" + have "state_space_usage = (\x. state_space_usage (n_of x, \_of x, \_of x))" + by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) + also have "... = (\x. 2 ^ 40 * ((ln (1 / (\_of x)) + 1)* (1/\_of x)\<^sup>2) + log 2 (log 2 (n_of x)+3))" unfolding state_space_usage_def by (simp add:divide_simps) - also have "... \ O[?F](\x. ln (1/\_of x)* (1/\_of x)\<^sup>2 + ln (ln (n_of x)))" + also have "... \ O[?F](\x. ln (1/\_of x)* (1/\_of x)\<^sup>2 + ln (ln (n_of x)))" by (intro landau_sum 2 4 5 evt_n_2) also have "... = O[?F](?rhs)" - by (simp add:case_prod_beta' n_of_def \_of_def \_of_def divide_simps) + by (simp add:case_prod_beta' n_of_def \_of_def \_of_def divide_simps) finally show ?thesis by simp qed theorem asymptotic_seed_space_complexity: - "seed_space_usage \ O[F](\(n, \, \). ln (1/\)+ln (1/\)^2 + ln n)" + "seed_space_usage \ O[F](\(n, \, \). ln (1/\)+ln (1/\)^2 + ln n)" (is "_ \ O[?F](?rhs)") proof - - have 0: "\\<^sub>F x in ?F. 0 \ (ln (1 / \_of x))\<^sup>2" + have 0: "\\<^sub>F x in ?F. 0 \ (ln (1 / \_of x))\<^sup>2" by simp - have 1: "\\<^sub>F x in ?F. 0 \ ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2" - by (intro eventually_mono[OF eventually_conj[OF evt_\_1 0]] add_nonneg_nonneg) auto + have 1: "\\<^sub>F x in ?F. 0 \ ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2" + by (intro eventually_mono[OF eventually_conj[OF evt_\_1 0]] add_nonneg_nonneg) auto - have 2: "(\x. 1) \ O[?F](\x. ln (1 / \_of x))" + have 2: "(\x. 1) \ O[?F](\x. ln (1 / \_of x))" using order_less_le_trans[OF exp_gt_zero] - by (intro landau_o.big_mono eventually_mono[OF evt_\[of "exp 1"]]) + by (intro landau_o.big_mono eventually_mono[OF evt_\[of "exp 1"]]) (auto intro!:iffD2[OF ln_ge_iff] simp add:abs_ge_iff) have "(\x. 1) \ O[at_top \\<^sub>F at_right 0 \\<^sub>F at_right 0](\x. ln (n_of x))" using order_less_le_trans[OF exp_gt_zero] by (intro landau_o.big_mono eventually_mono[OF evt_n[of "exp 1"]]) (auto intro!:iffD2[OF ln_ge_iff] simp add:abs_ge_iff) - hence 3: "(\x. 1) \ O[?F](\x. ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x))" - by (intro landau_sum_2 1 evt_n_1 0 evt_\_1) simp - have 4: "(\x. ln (n_of x)) \ O[?F](\x. ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x))" + hence 3: "(\x. 1) \ O[?F](\x. ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x))" + by (intro landau_sum_2 1 evt_n_1 0 evt_\_1) simp + have 4: "(\x. ln (n_of x)) \ O[?F](\x. ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x))" by (intro landau_sum_2 1 evt_n_1) simp - have "(\x. log 2 (1 / \_of x) + 16) \ O[?F](\x. ln (1 / \_of x))" + have "(\x. log 2 (1 / \_of x) + 16) \ O[?F](\x. ln (1 / \_of x))" using 2 unfolding log_def by (intro sum_in_bigo) simp_all - hence 5: "(\x. (log 2 (1 / \_of x) + 16)\<^sup>2) \ O[?F](\x. ln (1/\_of x)+(ln (1/\_of x))\<^sup>2)" - using 0 unfolding power2_eq_square by (intro landau_sum_2 landau_o.mult evt_\_1) simp_all - have 6: "(\x. (log 2 (1 / \_of x) + 16)\<^sup>2) \ O[?F](\x. ln (1/\_of x)+(ln (1/\_of x))\<^sup>2+ln (n_of x))" + hence 5: "(\x. (log 2 (1 / \_of x) + 16)\<^sup>2) \ O[?F](\x. ln (1/\_of x)+(ln (1/\_of x))\<^sup>2)" + using 0 unfolding power2_eq_square by (intro landau_sum_2 landau_o.mult evt_\_1) simp_all + have 6: "(\x. (log 2 (1 / \_of x) + 16)\<^sup>2) \ O[?F](\x. ln (1/\_of x)+(ln (1/\_of x))\<^sup>2+ln (n_of x))" by (intro landau_sum_1[OF _ _ 5] 1 evt_n_1) - have 7: "(\x. ln (1/\_of x)) \ O[?F](\x. ln (1/\_of x)+(ln (1/\_of x))\<^sup>2+ln (n_of x))" - by (intro landau_sum_1 1 evt_\_1 0 evt_n_1) simp + have 7: "(\x. ln (1/\_of x)) \ O[?F](\x. ln (1/\_of x)+(ln (1/\_of x))\<^sup>2+ln (n_of x))" + by (intro landau_sum_1 1 evt_\_1 0 evt_n_1) simp - have "seed_space_usage = (\x. seed_space_usage (n_of x, \_of x, \_of x))" - by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) - also have "... = (\x. 2^30+2^23*ln (n_of x)+48*(log 2 (1/(\_of x))+16)\<^sup>2 + 336 * ln (1 / \_of x))" + have "seed_space_usage = (\x. seed_space_usage (n_of x, \_of x, \_of x))" + by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) + also have "... = (\x. 2^30+2^23*ln (n_of x)+48*(log 2 (1/(\_of x))+16)\<^sup>2 + 336 * ln (1 / \_of x))" unfolding seed_space_usage_def by (simp add:divide_simps) - also have "... \ O[?F](\x. ln (1/\_of x)+ln (1/\_of x)^2 + ln (n_of x))" + also have "... \ O[?F](\x. ln (1/\_of x)+ln (1/\_of x)^2 + ln (n_of x))" using 3 4 6 7 by (intro sum_in_bigo) simp_all also have "... = O[?F](?rhs)" - by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) + by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) finally show ?thesis by simp qed definition "space_usage x = state_space_usage x + seed_space_usage x" theorem asymptotic_space_complexity: - "space_usage \ O[at_top \\<^sub>F at_right 0 \\<^sub>F at_right 0](\(n, \, \). ln (1/\)/\^2 + ln n)" + "space_usage \ O[at_top \\<^sub>F at_right 0 \\<^sub>F at_right 0](\(n, \, \). ln (1/\)/\^2 + ln n)" proof - - let ?f1 = "(\x. ln (1/\_of x)*(1/\_of x^2)+ln (ln (n_of x)))" - let ?f2 = "(\x. ln(1/\_of x)+ln(1/\_of x)^2+ln (n_of x))" + let ?f1 = "(\x. ln (1/\_of x)*(1/\_of x^2)+ln (ln (n_of x)))" + let ?f2 = "(\x. ln(1/\_of x)+ln(1/\_of x)^2+ln (n_of x))" - have 0: "\\<^sub>F x in F. 0 \ (1 / (\_of x)\<^sup>2)" + have 0: "\\<^sub>F x in F. 0 \ (1 / (\_of x)\<^sup>2)" unfolding var_simps by (intro eventually_prod1' eventually_prod2' eventually_inv) (simp_all add:prod_filter_eq_bot eventually_nonzero_simps) - have 1: "\\<^sub>F x in F. 0 \ ln (1 / \_of x) * (1 / (\_of x)\<^sup>2)" - by (intro eventually_mono[OF eventually_conj[OF evt_\_1 0]] mult_nonneg_nonneg) auto + have 1: "\\<^sub>F x in F. 0 \ ln (1 / \_of x) * (1 / (\_of x)\<^sup>2)" + by (intro eventually_mono[OF eventually_conj[OF evt_\_1 0]] mult_nonneg_nonneg) auto - have 2: "\\<^sub>F x in F. 0 \ ln (1 / \_of x) * (1 / (\_of x)\<^sup>2) + ln (ln (n_of x))" + have 2: "\\<^sub>F x in F. 0 \ ln (1 / \_of x) * (1 / (\_of x)\<^sup>2) + ln (ln (n_of x))" by (intro eventually_mono[OF eventually_conj[OF 1 evt_n_2]] add_nonneg_nonneg) auto - have 3: "\\<^sub>F x in F. 0 \ ln (1 / (\_of x)\<^sup>2)" + have 3: "\\<^sub>F x in F. 0 \ ln (1 / (\_of x)\<^sup>2)" unfolding power_one_over[symmetric] - by (intro eventually_mono[OF evt_\[of "1"]] ln_ge_zero) simp + by (intro eventually_mono[OF evt_\[of "1"]] ln_ge_zero) simp - have 4: "\\<^sub>F x in F. 0 \ ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x)" - by (intro eventually_mono[OF eventually_conj[OF evt_n_1 eventually_conj[OF evt_\_1 3]]] + have 4: "\\<^sub>F x in F. 0 \ ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x)" + by (intro eventually_mono[OF eventually_conj[OF evt_n_1 eventually_conj[OF evt_\_1 3]]] add_nonneg_nonneg) auto - have 5: "(\_. 1) \ O[F](\x. 1 / (\_of x)\<^sup>2)" + have 5: "(\_. 1) \ O[F](\x. 1 / (\_of x)\<^sup>2)" unfolding var_simps by (intro bigo_prod_1 bigo_prod_2 bigo_inv) (simp_all add:power_divide prod_filter_eq_bot) - have 6: "(\_. 1) \ O[F](\x. ln (1 / \_of x))" + have 6: "(\_. 1) \ O[F](\x. ln (1 / \_of x))" unfolding var_simps by (intro bigo_prod_1 bigo_prod_2 bigo_inv) (simp_all add:prod_filter_eq_bot) - have 7: "state_space_usage \ O[F](\x. ln (1 / \_of x) * (1 / (\_of x)\<^sup>2) + ln (ln (n_of x)))" - using asymptotic_state_space_complexity unfolding \_of_def \_of_def n_of_def - by (simp add:case_prod_beta') - - have 8: "seed_space_usage \ O[F](\x. ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x))" - using asymptotic_seed_space_complexity unfolding \_of_def \_of_def n_of_def + have 7: "state_space_usage \ O[F](\x. ln (1 / \_of x) * (1 / (\_of x)\<^sup>2) + ln (ln (n_of x)))" + using asymptotic_state_space_complexity unfolding \_of_def \_of_def n_of_def by (simp add:case_prod_beta') - have 9: "(\x. ln (n_of x)) \ O[F](\x. ln (1 / \_of x) * (1 / (\_of x)\<^sup>2) + ln (n_of x))" + have 8: "seed_space_usage \ O[F](\x. ln (1 / \_of x) + (ln (1 / \_of x))\<^sup>2 + ln (n_of x))" + using asymptotic_seed_space_complexity unfolding \_of_def \_of_def n_of_def + by (simp add:case_prod_beta') + + have 9: "(\x. ln (n_of x)) \ O[F](\x. ln (1 / \_of x) * (1 / (\_of x)\<^sup>2) + ln (n_of x))" by (intro landau_sum_2 evt_n_1 1) simp - have "(\x. (ln (1 / \_of x))\<^sup>2) \ O[F](\x. 1 / \_of x^2)" + have "(\x. (ln (1 / \_of x))\<^sup>2) \ O[F](\x. 1 / \_of x^2)" unfolding var_simps by (intro bigo_prod_1 bigo_prod_2 bigo_inv) (simp_all add:power_divide prod_filter_eq_bot) - hence 10: "(\x. (ln (1 / \_of x))\<^sup>2) \ O[F](\x. ln (1 / \_of x) * (1 / \_of x^2) + ln (n_of x))" + hence 10: "(\x. (ln (1 / \_of x))\<^sup>2) \ O[F](\x. ln (1 / \_of x) * (1 / \_of x^2) + ln (n_of x))" by (intro landau_sum_1 evt_n_1 1 landau_o.big_mult_1' 6) - have 11: "(\x. ln (1 / \_of x)) \ O[F](\x. ln (1 / \_of x) * (1 / \_of x^2) + ln (n_of x))" + have 11: "(\x. ln (1 / \_of x)) \ O[F](\x. ln (1 / \_of x) * (1 / \_of x^2) + ln (n_of x))" by (intro landau_sum_1 evt_n_1 1 landau_o.big_mult_1 5) simp - have 12: "(\x. ln (1/\_of x) * (1/\_of x^2)) \ O[F](\x. ln (1/\_of x)*(1/\_of x^2)+ln (n_of x))" + have 12: "(\x. ln (1/\_of x) * (1/\_of x^2)) \ O[F](\x. ln (1/\_of x)*(1/\_of x^2)+ln (n_of x))" by (intro landau_sum_1 1 evt_n_1) simp have "(\x. ln (ln (n_of x))) \ O[F](\x. ln (n_of x))" unfolding var_simps by (intro bigo_prod_1 bigo_prod_2) (simp_all add:prod_filter_eq_bot) - hence 13: "(\x. ln (ln (n_of x))) \ O[F](\x. ln (1 / \_of x) * (1 / \_of x^2) + ln (n_of x))" + hence 13: "(\x. ln (ln (n_of x))) \ O[F](\x. ln (1 / \_of x) * (1 / \_of x^2) + ln (n_of x))" by (intro landau_sum_2 evt_n_1 1) have "space_usage = (\x. state_space_usage x + seed_space_usage x)" unfolding space_usage_def by simp also have "... \ O[F](\x. ?f1 x + ?f2 x)" by (intro landau_sum 2 4 7 8) - also have "... \ O[F](\x. ln (1 / \_of x) * (1/\_of x^2) + ln (n_of x))" + also have "... \ O[F](\x. ln (1 / \_of x) * (1/\_of x^2) + ln (n_of x))" by (intro landau_o.big.subsetI sum_in_bigo 9 10 11 12 13) - also have "... = O[F](\(n, \, \). ln (1/\)/\^2 + ln n)" - unfolding \_of_def \_of_def n_of_def + also have "... = O[F](\(n, \, \). ln (1/\)/\^2 + ln n)" + unfolding \_of_def \_of_def n_of_def by (simp add:case_prod_beta') finally show ?thesis by simp qed end unbundle no_intro_cong_syntax end