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,327 +1,315 @@
 section \<open>Accuracy with cutoff\label{sec:accuracy}\<close>
 
 text \<open>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}.\<close>
 
 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 \<noteq> {}"
   assumes "\<And>i. i \<in> I \<Longrightarrow> finite (Z i)"
   assumes "\<And>i. i \<in> I \<Longrightarrow> Z i \<noteq> {}"
   shows "F (\<Union> (Z ` I)) = F ((\<lambda>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 (\<Union> (Z ` insert x I)) = F ((Z x) \<union> (\<Union> (Z ` I)))"
     by simp
   also have "... = f (F (Z x)) (F (\<Union> (Z ` I)))"
     using insert by (intro union finite_UN_I) auto
   also have "... = f (F {F (Z x)}) (F ((\<lambda>i. F (Z i)) ` I))"
     using insert(5,6) by (subst insert(4)) auto
   also have "... = F ({F (Z x)} \<union> (\<lambda>i. F (Z i)) ` I)"
     using insert(1,2) by (intro union[symmetric] finite_imageI) auto
   also have "... = F ((\<lambda>i. F (Z i)) ` insert x I)"
     by simp
   finally show ?case by simp
 qed
 
 text \<open>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)"}.\<close>
 
 lemma hom_Max_commute':
   assumes "finite A" "A \<noteq> {}"
   assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> 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 \<psi> \<sigma> = (Max ((\<lambda>j. \<tau>\<^sub>1 \<psi> A \<sigma> j + \<sigma>) ` {..<b})) - b_exp + 9"
 
 definition s\<^sub>c (* tilde t *)
   where "s\<^sub>c \<psi> \<sigma> = nat (t\<^sub>c \<psi> \<sigma>)"
 
 definition p\<^sub>c (* tilde p *)
   where "p\<^sub>c \<psi> \<sigma> = card {j\<in> {..<b}. \<tau>\<^sub>1 \<psi> A \<sigma> j + \<sigma> \<ge> s\<^sub>c \<psi> \<sigma>}"
 
 definition Y\<^sub>c (* tilde A* *)
   where "Y\<^sub>c \<psi> \<sigma> = 2 ^ s\<^sub>c \<psi> \<sigma> * \<rho>_inv (p\<^sub>c \<psi> \<sigma>)"
 
 lemma s\<^sub>c_eq_s:
   assumes "(f,g,h) \<in> sample_pro \<Psi>"
   assumes "\<sigma> \<le> s f"
   shows "s\<^sub>c (f,g,h) \<sigma> = s f"
 proof -
   have "int (Max (f ` A)) - int b_exp + 9 \<le> int (Max (f ` A)) - 26 + 9"
     using b_exp_ge_26 by (intro add_mono diff_left_mono) auto
   also have "... \<le> int (Max (f ` A))" by simp
   finally have 1:"int (Max (f ` A)) - int b_exp + 9 \<le> int (Max (f ` A))"
     by simp
   have "\<sigma> \<le> int (s f)" using assms(2) by simp
   also have "... = max 0 (t f)"
     unfolding s_def by simp
   also have "... \<le> max 0 (int (Max (f ` A)))"
     unfolding t_def using 1 by simp
   also have "... = int (Max (f ` A))"
     by simp
   finally have "\<sigma> \<le> int (Max (f ` A))"
     by simp
   hence 0: "int \<sigma> - 1 \<le> int (Max (f ` A))"
     by simp
 
   have c:"h \<in> sample_pro (\<H> k (C\<^sub>7 * b\<^sup>2) (\<N> b))"
     using assms(1) sample_set_\<Psi> by auto
   hence h_range: "h x < b" for x
     using h_range_1 by simp
 
   have "(MAX j\<in>{..<b}. \<tau>\<^sub>1 (f, g, h) A \<sigma> j + int \<sigma>) =
     (MAX x\<in>{..<b}. Max ({int (f a) |a. a \<in> A \<and> h (g a) = x} \<union> {-1} \<union> {int \<sigma> -1}))"
     using fin_f[OF assms(1)] by (simp add:max_add_distrib_left max.commute \<tau>\<^sub>1_def)
   also have "... = Max (\<Union>x<b. {int (f a) |a. a \<in> A \<and> h (g a) = x} \<union> {- 1} \<union> {int \<sigma> - 1})"
     using fin_f[OF assms(1)] b_ne by (intro Max.Union[symmetric]) auto
   also have "... = Max ({int (f a) |a. a \<in> A} \<union> {- 1, int \<sigma> - 1})"
     using h_range by (intro arg_cong[where f="Max"]) auto
   also have "... = max (Max (int ` f ` A)) (int \<sigma> - 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 \<sigma> - 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\<in>{..<b}. \<tau>\<^sub>1 (f, g, h) A \<sigma> j + int \<sigma>) = 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) \<in> sample_pro \<Psi>"
   assumes "\<sigma> \<le> s f"
   shows "p\<^sub>c (f,g,h) \<sigma> = p (f,g,h)"
 proof -
   have "{j \<in> {..<b}. int (s f) \<le> max (\<tau>\<^sub>0 (f, g, h) A j) (int \<sigma> - 1)} =
     {j \<in> {..<b}. int (s f) \<le> max (\<tau>\<^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 \<tau>\<^sub>1_def del:\<tau>\<^sub>0.simps)
 qed
 
 lemma Y\<^sub>c_eq_Y:
   assumes "(f,g,h) \<in> sample_pro \<Psi>"
   assumes "\<sigma> \<le> s f"
   shows "Y\<^sub>c (f,g,h) \<sigma> = 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 \<Psi> {\<psi>. \<exists>\<sigma> \<le> q_max. \<bar>Y\<^sub>c \<psi> \<sigma> - real X\<bar> > \<epsilon> * X} \<le> 1/2^4"
   (is "?L \<le> ?R")
 proof -
   have "measure \<Psi> {\<psi>. \<exists>\<sigma> \<le> q_max. \<bar>Y\<^sub>c \<psi> \<sigma> - real X\<bar> > \<epsilon> * real X} \<le>
     measure \<Psi> {(f,g,h). \<bar>Y (f,g,h) - real X\<bar> >  \<epsilon> * real X \<or> s f < q_max}"
   proof (rule pmf_mono)
     fix \<psi>
     assume a:"\<psi> \<in> {\<psi>. \<exists>\<sigma>\<le>q_max. \<epsilon> * real X < \<bar>Y\<^sub>c \<psi> \<sigma> - real X\<bar>}"
     assume d:"\<psi> \<in> set_pmf (sample_pro \<Psi>)"
     obtain \<sigma> where b:"\<sigma> \<le> q_max" and c:" \<epsilon> * real X < \<bar>Y\<^sub>c \<psi> \<sigma> - real X\<bar>"
       using a by auto
     obtain f g h where \<psi>_def: "\<psi> = (f,g,h)" by (metis prod_cases3)
     hence e:"(f,g,h) \<in> sample_pro \<Psi>" using d by simp
 
     show "\<psi> \<in> {(f, g, h). \<epsilon> * real X < \<bar>Y (f, g, h) - real X\<bar> \<or> s f < q_max}"
     proof (cases "s f \<ge> q_max")
       case True
       hence f:"\<sigma> \<le> s f" using b by simp
       have "\<epsilon> * real X < \<bar>Y \<psi> - real X\<bar>"
         using Y\<^sub>c_eq_Y[OF e f] c unfolding \<psi>_def by simp
       then show ?thesis unfolding \<psi>_def by simp
     next
       case False
       then show ?thesis unfolding \<psi>_def by simp
     qed
   qed
   also have "... \<le> 1/2^4"
     using accuracy_without_cutoff by simp
   finally show ?thesis by simp
 qed
 
 lemma estimate1_eq:
   assumes "j < l"
   shows "estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) j = Y\<^sub>c (\<omega> j) \<sigma>" (is "?L = ?R")
 proof -
   define t where "t = max 0 (Max ((\<tau>\<^sub>2 \<omega> A \<sigma> j) ` {..<b}) + \<sigma> - \<lfloor>log 2 b\<rfloor> + 9)"
   define p where "p = card { k. k \<in> {..<b} \<and> (\<tau>\<^sub>2 \<omega> A \<sigma> j k) + \<sigma> \<ge> t }"
 
   have 0: "int (nat x) = max 0 x" for x
     by simp
   have 1: "\<lfloor>log 2 b\<rfloor> = b_exp"
     unfolding b_def by simp
 
   have "b > 0"
     using b_min by simp
   hence 2: " {..<b} \<noteq> {}" by auto
 
   have "t = int (nat (Max ((\<tau>\<^sub>2 \<omega> A \<sigma> j) ` {..<b}) + \<sigma> - b_exp + 9))"
     unfolding t_def 0 1 by (rule refl)
   also have "... = int (nat (Max ((\<lambda>x. x + \<sigma>) ` (\<tau>\<^sub>2 \<omega> A \<sigma> j) ` {..<b}) - b_exp + 9))"
     by (intro_cong "[\<sigma>\<^sub>1 int,\<sigma>\<^sub>1 nat,\<sigma>\<^sub>2(+),\<sigma>\<^sub>2(-)]" more:hom_Max_commute) (simp_all add:2)
   also have "... = int (s\<^sub>c (\<omega> j) \<sigma>)"
     using assms
     unfolding s\<^sub>c_def t\<^sub>c_def \<tau>\<^sub>2_def image_image by simp
   finally have 3:"t = int (s\<^sub>c (\<omega> j) \<sigma>)"
     by simp
 
   have 4: "p = p\<^sub>c (\<omega> j) \<sigma>"
     using assms unfolding p_def p\<^sub>c_def 3 \<tau>\<^sub>2_def by simp
 
   have "?L = 2 powr t * ln (1-p/b) / ln(1-1/b)"
     unfolding estimate1.simps \<tau>_def \<tau>\<^sub>3_def
     by (simp only:t_def p_def Let_def)
   also have "... = 2 powr (s\<^sub>c (\<omega> j) \<sigma>) * \<rho>_inv p"
     unfolding 3 \<rho>_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 \<Omega> {\<omega>. (\<exists>\<sigma>\<le>q_max. \<epsilon>*X < \<bar>estimate (\<tau>\<^sub>2 \<omega> A \<sigma>,\<sigma>)-X\<bar>) } \<le> \<delta>/2" (is "?L \<le> ?R")
 proof -
   define I :: "real set" where "I = {x. \<bar>x - real X\<bar> \<le> \<epsilon>*X}"
 
   define \<mu> where "\<mu> = measure \<Psi> {\<psi>. \<exists>\<sigma>\<le>q_max. Y\<^sub>c \<psi> \<sigma>\<notin>I}"
 
   have int_I: "interval I"
     unfolding interval_def I_def by auto
 
   have "\<mu> = measure \<Psi> {\<psi>. \<exists>\<sigma> \<le> q_max. \<bar>Y\<^sub>c \<psi> \<sigma> - real X\<bar> > \<epsilon> * X}"
     unfolding \<mu>_def I_def by (simp add:not_le)
   also have "... \<le>  1 / 2 ^ 4"
     by (intro accuracy_single)
   also have "... = 1/ 16"
     by simp
   finally have 1:"\<mu> \<le> 1 / 16" by simp
 
   have "(\<mu> + \<Lambda>) \<le> 1/16 + 1/16"
     unfolding \<Lambda>_def by (intro add_mono 1) auto
   also have "... \<le> 1/8"
     by simp
   finally have 2:"(\<mu> + \<Lambda>) \<le> 1/8"
     by simp
 
   hence 0: "(\<mu> + \<Lambda>) \<le> 1/2"
     by simp
 
   have "\<mu> \<ge> 0"
     unfolding \<mu>_def by simp
   hence 3: "\<mu> + \<Lambda> > 0"
     by (intro add_nonneg_pos \<Lambda>_gt_0)
 
   have "?L = measure \<Omega> {\<omega>. (\<exists>\<sigma>\<le>q_max. \<epsilon>*X < \<bar>median l (estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>,\<sigma>))-X\<bar>) }"
     by simp
   also have "... = measure \<Omega> {\<omega>. (\<exists>\<sigma>\<le>q_max. median l (estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>,\<sigma>)) \<notin> I)}"
     unfolding I_def by (intro measure_pmf_cong) auto
   also have "... \<le> measure \<Omega> {\<omega>. real(card{i\<in>{..<l}.(\<exists>\<sigma>\<le>q_max. Y\<^sub>c (\<omega> i) \<sigma>\<notin>I)})\<ge> real l/2}"
   proof (rule pmf_mono)
     fix \<omega>
     assume "\<omega> \<in> set_pmf \<Omega>" "\<omega> \<in> {\<omega>. \<exists>\<sigma>\<le>q_max. median l (estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>)) \<notin> I}"
     then obtain \<sigma> where \<sigma>_def: "median l (estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>)) \<notin> I" "\<sigma>\<le>q_max"
       by auto
-
-    have "real l = 2 * real l - real l"
+    hence "real l \<le> real (2 * card {i. i <l \<and> estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<notin> I})"
+      by (intro of_nat_mono median_est_rev[OF int_I])
+    also have "... = 2 * real (card {i\<in>{..<l}. estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<notin> I})"
       by simp
-    also have "... \<le> 2 * real l - 2 * card {i. i < l \<and> estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<in> I}"
-      using \<sigma>_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 {..<l}) -card {i. i < l \<and> estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<in> I})"
-      by (simp del:estimate1.simps)
-    also have "... = 2 * real (card {..<l} -card {i. i < l \<and> estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<in> I})"
-      by (intro_cong "[\<sigma>\<^sub>2 (*)]" more:of_nat_diff[symmetric] card_mono)
-        (auto simp del:estimate1.simps)
-    also have "... = 2 * real (card ({..<l} - {i. i < l \<and> estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<in> I}))"
-      by (intro_cong "[\<sigma>\<^sub>2 (*), \<sigma>\<^sub>1 of_nat]" more:card_Diff_subset[symmetric])
-        (auto simp del:estimate1.simps)
-    also have "... = 2 * real (card {i\<in>{..<l}. estimate1 (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>) i \<notin> I})"
-      by (intro_cong "[\<sigma>\<^sub>2 (*), \<sigma>\<^sub>1 of_nat, \<sigma>\<^sub>1 card]") (auto simp del:estimate1.simps)
     also have "... = 2 * real (card {i \<in> {..<l}. Y\<^sub>c (\<omega> i) \<sigma> \<notin> I})"
       using estimate1_eq by (intro_cong "[\<sigma>\<^sub>2 (*), \<sigma>\<^sub>1 of_nat, \<sigma>\<^sub>1 card]" more:restr_Collect_cong) auto
     also have "... \<le> 2 * real (card {i \<in> {..<l}. (\<exists>\<sigma>\<le>q_max. Y\<^sub>c (\<omega> i) \<sigma> \<notin> I)})"
       using \<sigma>_def(2) by (intro mult_left_mono Nat.of_nat_mono card_mono) auto
     finally have "real l \<le> 2 * real (card {i \<in> {..<l}. (\<exists>\<sigma>\<le>q_max. Y\<^sub>c (\<omega> i) \<sigma> \<notin> I)})"
       by simp
     thus "\<omega> \<in> {\<omega>. real l/2 \<le> real (card {i \<in> {..<l}. \<exists>\<sigma>\<le>q_max. Y\<^sub>c (\<omega> i) \<sigma> \<notin> I})}"
       by simp
   qed
   also have "... = measure \<Omega> {\<omega>. real (card{i\<in>{..<l}. (\<exists>\<sigma>\<le>q_max. Y\<^sub>c (\<omega> i) \<sigma>\<notin>I)}) \<ge> (1/2)*real l}"
     unfolding p_def by simp
   also have "... \<le> exp (- real l * ((1/2) * ln (1 / (\<mu> + \<Lambda>)) - 2 * exp (- 1)))"
     using 0 unfolding \<mu>_def by (intro walk_tail_bound l_gt_0 \<Lambda>_gt_0) auto
   also have "... = exp (- (real l * ((1/2) * ln (1 / (\<mu> + \<Lambda>)) - 2 * exp (- 1))))"
     by simp
   also have "... \<le> 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 "... \<le> 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 "... \<le> exp (- (C\<^sub>6 * ln (2/ \<delta>)*(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/ \<delta>))"
     unfolding C\<^sub>6_def by simp
   also have "... = ?R"
     using \<delta>_gt_0 by (subst ln_inverse[symmetric]) auto
   finally show ?thesis
     by simp
 qed
 
 theorem estimate_result:
   "measure \<Omega> {\<omega>. \<bar>estimate (\<tau> \<omega> A)- X\<bar> >  \<epsilon> * X} \<le>  \<delta>"
   (is "?L \<le> ?R")
 proof -
   let ?P = "measure \<Omega>"
   have "?L \<le> ?P {\<omega>. (\<exists>\<sigma>\<le>q_max.  \<epsilon>*real X<\<bar>estimate (\<tau>\<^sub>2 \<omega> A \<sigma>, \<sigma>)-real X\<bar>)\<or>q \<omega> A> q_max}"
     unfolding \<tau>_def \<tau>\<^sub>3_def not_le[symmetric]
     by (intro pmf_mono) auto
   also have "...\<le> ?P {\<omega>. (\<exists>\<sigma>\<le>q_max. \<epsilon>*real X<\<bar>estimate (\<tau>\<^sub>2 \<omega> A \<sigma>,\<sigma>)-X\<bar>)} + ?P {\<omega>. q \<omega> A> q_max}"
     by (intro pmf_add) auto
   also have "...\<le>  \<delta>/2 +  \<delta>/2"
     by (intro add_mono cutoff_level estimate_result_1)
   also have "... =  \<delta>"
     by simp
   finally show ?thesis
     by simp
 qed
 
 end
 
 lemma (in inner_algorithm) estimate_result:
   assumes "A \<subseteq> {..<n}" "A \<noteq> {}"
   shows "measure \<Omega> {\<omega>. \<bar>estimate (\<tau> \<omega> A)- real (card A)\<bar> > \<epsilon> * real (card A)} \<le> \<delta>" (is "?L \<le> ?R")
 proof -
   interpret inner_algorithm_fix_A
     using assms by unfold_locales auto
   have "?L = measure \<Omega> {\<omega>. \<bar>estimate (\<tau> \<omega> A)- X\<bar> > \<epsilon> * X}"
     unfolding X_def by simp
   also have "... \<le> ?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_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,807 +1,795 @@
 section \<open>Outer Algorithm\label{sec:outer_algorithm}\<close>
 
 text \<open>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$.\<close>
 
 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 \<open>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)$.\<close>
 
 definition "state_space_usage = (\<lambda>(n,\<epsilon>,\<delta>). 2^40 * (ln(1/\<delta>)+1)/ \<epsilon>^2 + log 2 (log 2 n + 3))"
 definition "seed_space_usage = (\<lambda>(n,\<epsilon>,\<delta>). 2^30+2^23*ln n+48*(log 2(1/\<epsilon>)+16)\<^sup>2+336*ln (1/\<delta>))"
 
 locale outer_algorithm =
   fixes n :: nat
   fixes \<delta> :: real
   fixes \<epsilon> :: real
   assumes n_gt_0: "n > 0"
   assumes \<delta>_gt_0: "\<delta> > 0" and \<delta>_lt_1: "\<delta> < 1"
   assumes \<epsilon>_gt_0: "\<epsilon> > 0" and \<epsilon>_lt_1: "\<epsilon> < 1"
 begin
 
 definition n\<^sub>0 where "n\<^sub>0 = max (real n) (exp (exp 5))"
 definition stage_two where "stage_two = (\<delta> < (1/ln n\<^sub>0))"
 definition \<delta>\<^sub>i :: real where "\<delta>\<^sub>i = (if stage_two then (1/ln n\<^sub>0) else \<delta>)"
 definition m :: nat where "m = (if stage_two then nat \<lceil>4 * ln (1/ \<delta>)/ln (ln n\<^sub>0)\<rceil> else 1)"
 definition \<alpha> where "\<alpha> = (if stage_two then (1/ln n\<^sub>0) else 1)"
 
 lemma m_lbound:
   assumes "stage_two"
   shows "m \<ge> 4 * ln (1/ \<delta>)/ln(ln n\<^sub>0)"
 proof -
   have "m = real (nat \<lceil>4 * ln (1 / \<delta>) / ln (ln n\<^sub>0)\<rceil>)"
     using assms unfolding m_def by simp
   also have "... \<ge> 4 * ln (1 / \<delta>) / ln (ln n\<^sub>0)"
     by linarith
   finally show ?thesis by simp
 qed
 
 lemma n_lbound:
   "n\<^sub>0 \<ge> exp (exp 5)" "ln n\<^sub>0 \<ge> exp 5" "5 \<le> ln (ln n\<^sub>0)" "ln n\<^sub>0 > 1" "n\<^sub>0 > 1"
 proof -
   show 0:"n\<^sub>0 \<ge> exp (exp 5)"
     unfolding n\<^sub>0_def by simp
   have "(1::real) \<le> exp (exp 5)"
     by (approximation 5)
   hence "n\<^sub>0 \<ge> 1"
     using 0 by argo
   thus 1:"ln n\<^sub>0 \<ge> 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 \<le> 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 \<delta>1_gt_0: "0 < \<delta>\<^sub>i"
   using n_lbound(4) \<delta>_gt_0 unfolding \<delta>\<^sub>i_def
   by (cases "stage_two") simp_all
 
 lemma \<delta>1_lt_1: "\<delta>\<^sub>i < 1"
   using n_lbound(4) \<delta>_lt_1 unfolding \<delta>\<^sub>i_def
   by (cases "stage_two") simp_all
 
 lemma m_gt_0_aux:
   assumes "stage_two"
   shows "1 \<le> ln (1 / \<delta>) / ln (ln n\<^sub>0)"
 proof -
   have "ln n\<^sub>0 \<le> 1 / \<delta>"
     using n_lbound(4)
     using assms unfolding pos_le_divide_eq[OF \<delta>_gt_0] stage_two_def
     by (simp add:divide_simps ac_simps)
   hence "ln (ln n\<^sub>0) \<le> ln (1 / \<delta>)"
     using n_lbound(4) \<delta>_gt_0 by (intro iffD2[OF ln_le_cancel_iff] divide_pos_pos) auto
   thus "1 \<le> ln (1 / \<delta>) / 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/ \<delta>)/ln(ln n\<^sub>0)"
     using m_gt_0_aux[OF True] by simp
   also have "... \<le> 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 \<alpha>_gt_0: "\<alpha> > 0"
   using n_lbound(4) unfolding \<alpha>_def
   by (cases "stage_two") auto
 
 lemma \<alpha>_le_1: "\<alpha> \<le> 1"
   using n_lbound(4) unfolding \<alpha>_def
   by (cases "stage_two") simp_all
 
 sublocale I: inner_algorithm "n" "\<delta>\<^sub>i" "\<epsilon>"
   unfolding inner_algorithm_def using n_gt_0 \<epsilon>_gt_0 \<epsilon>_lt_1 \<delta>1_gt_0 \<delta>1_lt_1 by auto
 
 abbreviation \<Theta> where "\<Theta> \<equiv> \<E> m \<alpha> I.\<Omega>"
 
 lemma \<Theta>: "m > 0" "\<alpha> > 0" using \<alpha>_gt_0 m_gt_0 by auto
 
 type_synonym state = "inner_algorithm.state list"
 
 fun single :: "nat \<Rightarrow> nat \<Rightarrow> state" where
   "single \<theta> x = map (\<lambda>j. I.single (pro_select \<Theta> \<theta> j) x) [0..<m]"
 
 fun merge :: "state \<Rightarrow> state \<Rightarrow> state" where
   "merge x y = map (\<lambda>(x,y). I.merge x y) (zip x y)"
 
 fun estimate :: "state \<Rightarrow> real" where
   "estimate x = median m (\<lambda>i. I.estimate (x ! i))"
 
 definition \<nu> :: "nat \<Rightarrow> nat set \<Rightarrow> state"
   where "\<nu> \<theta> A = map (\<lambda>i. I.\<tau> (pro_select \<Theta> \<theta> i) A) [0..<m]"
 
 text \<open>The following three theorems verify the correctness of the algorithm. The term @{term "\<tau>"}
 is a mathematical description of the sketch for a given subset, while @{term "single"},
 @{term "merge"} are the actual functions that compute the sketches.\<close>
 
 theorem merge_result: "merge (\<nu> \<omega> A) (\<nu> \<omega> B) = \<nu> \<omega> (A \<union> B)" (is "?L = ?R")
 proof -
   have 0: "zip [0..<m] [0..<m] = map (\<lambda>x. (x,x)) [0..<m]" for m
     by (induction m, auto)
 
   have "?L = map (\<lambda>x. I.merge (I.\<tau> (pro_select \<Theta> \<omega> x) A) (I.\<tau> (pro_select \<Theta> \<omega> x) B)) [0..<m]"
     unfolding \<nu>_def
     by (simp add:zip_map_map 0 comp_def case_prod_beta)
   also have "... = map (\<lambda>x.  I.\<tau> (pro_select \<Theta> \<omega> x) (A \<union> B)) [0..<m]"
     by (intro map_cong refl I.merge_result expander_pro_range[OF \<Theta>])
   also have "... = ?R"
     unfolding \<nu>_def by simp
   finally show ?thesis by simp
 qed
 
 theorem single_result: "single \<omega> x = \<nu> \<omega> {x}" (is "?L = ?R")
 proof -
   have "?L = map (\<lambda>j. I.single (pro_select \<Theta> \<omega> j) x) [0..<m]"
     by (simp del:I.single.simps)
   also have "... = ?R"
     unfolding \<nu>_def by (intro map_cong I.single_result expander_pro_range[OF \<Theta>]) auto
   finally show ?thesis by simp
 qed
 
 theorem estimate_result:
   assumes "A \<subseteq> {..<n}" "A \<noteq> {}"
   defines "p \<equiv> (pmf_of_set {..<pro_size \<Theta>})"
   shows "measure p {\<omega>. \<bar>estimate (\<nu> \<omega> A)- real (card A)\<bar> > \<epsilon> * real (card A)} \<le> \<delta>" (is "?L \<le> ?R")
 proof (cases "stage_two")
   case True
   define I where "I = {x. \<bar>x - real (card A)\<bar> \<le> \<epsilon> * real (card A)}"
   have int_I: "interval I"
     unfolding interval_def I_def by auto
 
   define \<mu> where "\<mu> = measure I.\<Omega> {\<omega>. I.estimate (I.\<tau> \<omega> A) \<notin> I}"
 
   have 0:"\<mu> + \<alpha> > 0"
     unfolding \<mu>_def
     by (intro add_nonneg_pos \<alpha>_gt_0) auto
 
   have "\<mu> \<le> \<delta>\<^sub>i"
     unfolding \<mu>_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 \<delta>\<^sub>i_def by simp
   finally have "\<mu> \<le> 1/ln n\<^sub>0" by simp
   hence "\<mu> + \<alpha> \<le> 1/ln n\<^sub>0 + 1/ln n\<^sub>0"
     unfolding \<alpha>_def using True by (intro add_mono) auto
   also have "... = 2/ln n\<^sub>0"
     by simp
   finally have 1:"\<mu> + \<alpha> \<le> 2 / ln n\<^sub>0"
     by simp
   hence 2:"ln n\<^sub>0 \<le> 2 / (\<mu> + \<alpha>)"
     using 0 n_lbound by (simp add:field_simps)
 
   have "\<mu> + \<alpha> \<le> 2/ln n\<^sub>0"
     by (intro 1)
   also have "... \<le> 2/exp 5"
     using n_lbound by (intro divide_left_mono) simp_all
   also have "... \<le> 1/2"
     by (approximation 5)
   finally have 3:"\<mu> + \<alpha> \<le> 1/2" by simp
 
   have 4: "2 * ln 2 + 8 * exp (- 1) \<le> (5::real)"
     by (approximation 5)
 
   have "?L = measure p {\<omega>. median m (\<lambda>i. I.estimate (\<nu> \<omega> A  ! i)) \<notin> I}"
     unfolding I_def by (simp add:not_le)
   also have "... \<le>
     measure p {\<theta>. real (card {i \<in> {..<m}. I.estimate (I.\<tau> (pro_select \<Theta> \<theta> i) A) \<notin> I})\<ge> real m/2}"
   proof (rule pmf_mono)
     fix \<theta> assume "\<theta> \<in> set_pmf p"
     assume a:"\<theta> \<in> {\<omega>. median m (\<lambda>i. I.estimate (\<nu> \<omega> A ! i)) \<notin> I}"
-    have "real m = 2 * real m - real m"
+    hence "real m \<le> real (2*card {i. i < m \<and> I.estimate (\<nu> \<theta> A ! i) \<notin> I})"
+      by (intro of_nat_mono median_est_rev int_I) auto
+    also have "... = 2 * real (card {i\<in>{..<m}. I.estimate (\<nu> \<theta> A ! i) \<notin> I})"
       by simp
-    also have "... \<le> 2 * real m - 2 * card {i. i < m \<and> I.estimate (\<nu> \<theta> A ! i) \<in> 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 {..<m}) - card {i. i < m \<and> I.estimate (\<nu> \<theta> A ! i) \<in> I})"
-      by (simp del:I.estimate.simps)
-    also have "... = 2 * real (card {..<m} - card {i. i < m \<and> I.estimate (\<nu> \<theta> A ! i) \<in> I})"
-      by (intro_cong "[\<sigma>\<^sub>2 (*)]" more:of_nat_diff[symmetric] card_mono)
-        (auto simp del:I.estimate.simps)
-    also have "... = 2 * real (card ({..<m} - {i. i < m \<and> I.estimate (\<nu> \<theta> A ! i) \<in> I}))"
-      by (intro_cong "[\<sigma>\<^sub>2 (*), \<sigma>\<^sub>1 of_nat]" more:card_Diff_subset[symmetric])
-        (auto simp del:I.estimate.simps)
-    also have "... = 2 * real (card {i\<in>{..<m}. I.estimate (\<nu> \<theta> A ! i) \<notin> I})"
-      by (intro_cong "[\<sigma>\<^sub>2 (*), \<sigma>\<^sub>1 of_nat, \<sigma>\<^sub>1 card]") (auto simp del:I.estimate.simps)
     also have "... = 2 * real (card {i \<in> {..<m}. I.estimate (I.\<tau> (pro_select \<Theta> \<theta> i) A) \<notin> I})"
       unfolding \<nu>_def by (intro_cong "[\<sigma>\<^sub>2 (*), \<sigma>\<^sub>1 of_nat, \<sigma>\<^sub>1 card]" more:restr_Collect_cong)
        (simp del:I.estimate.simps)
     finally have "real m \<le> 2 * real (card {i \<in> {..<m}. I.estimate (I.\<tau> (pro_select \<Theta> \<theta> i) A) \<notin> I})"
       by simp
     thus "\<theta> \<in> {\<theta>. real m / 2 \<le> real (card {i \<in> {..<m}. I.estimate (I.\<tau> (pro_select \<Theta> \<theta> i) A) \<notin> I})}"
       by simp
   qed
   also have "...=measure \<Theta>{\<theta>. real(card {i \<in> {..<m}. I.estimate (I.\<tau> (\<theta> i) A) \<notin> I})\<ge>(1/2)*real m}"
     unfolding sample_pro_alt p_def by (simp del:I.estimate.simps)
   also have "... \<le> exp (-real m * ((1/2) * ln (1/ (\<mu> + \<alpha>)) - 2*exp (-1)))"
     using 3 m_gt_0 \<alpha>_gt_0 unfolding \<mu>_def by (intro walk_tail_bound) force+
   also have "... \<le> 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 "... \<le> 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 "... \<le> 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 "... \<le> exp (- (4 * ln (1/ \<delta>)/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/ \<delta>))"
     using n_lbound by simp
   also have "... = \<delta>"
     using \<delta>_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 {\<omega>. \<epsilon> * real (card A) < \<bar>I.estimate (\<nu> \<omega> A ! 0) - real (card A)\<bar>}"
     unfolding estimate.simps m_eq median_def by simp
   also have "... =  measure p {\<omega>. \<epsilon>*card A<\<bar>I.estimate (I.\<tau> (pro_select \<Theta> \<omega> 0) A)-real(card A)\<bar>}"
     unfolding \<nu>_def m_eq by (simp del: I.estimate.simps)
   also have "... = measure \<Theta> {\<omega>. \<epsilon>*real(card A) < \<bar>I.estimate (I.\<tau> (\<omega> 0) A)-real(card A)\<bar>}"
     unfolding sample_pro_alt p_def by (simp del:I.estimate.simps)
   also have "...=
     measure (map_pmf (\<lambda>\<theta>. \<theta> 0) \<Theta>) {\<omega>. \<epsilon>*real(card A) < \<bar>I.estimate (I.\<tau> \<omega> A)-real(card A)\<bar>}"
     by simp
   also have "... = measure I.\<Omega> {\<omega>. \<epsilon>*real(card A) < \<bar>I.estimate (I.\<tau> \<omega> A)-real(card A)\<bar>}"
     using m_eq by (subst expander_uniform_property[OF \<Theta>]) auto
   also have "... \<le> \<delta>\<^sub>i"
     by (intro I.estimate_result[OF assms(1,2)])
   also have "... = ?R"
     unfolding \<delta>\<^sub>i_def using False by simp
   finally show ?thesis
     by simp
 qed
 
 text \<open>The function @{term "encode_state"} can represent states as bit strings.
 This enables verification of the space usage.\<close>
 
 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 (\<nu> \<omega> A)) \<le> state_space_usage (real n, \<epsilon>, \<delta>)"
     (is "?L \<le> ?R")
 proof -
   have 0: "length (\<nu> \<omega> A) = m"
     unfolding \<nu>_def by simp
   have "?L = (\<Sum>x\<leftarrow>\<nu> \<omega> A. bit_count (I.encode_state x))"
     using 0 unfolding encode_state_def fixed_list_bit_count by simp
   also have "... = (\<Sum>x\<leftarrow>[0..<m]. bit_count (I.encode_state (I.\<tau> (pro_select \<Theta> \<omega> x) A)))"
     unfolding \<nu>_def by (simp add:comp_def)
   also have "... \<le> (\<Sum>x\<leftarrow>[0..<m]. ereal (2^36 *(ln (1/\<delta>\<^sub>i)+ 1)/\<epsilon>\<^sup>2 + log 2 (log 2 (real n) + 3)))"
     using I.state_bit_count by (intro sum_list_mono I.state_bit_count expander_pro_range[OF \<Theta>])
   also have "... = ereal ( real m * (2^36 *(ln (1/\<delta>\<^sub>i)+ 1)/\<epsilon>\<^sup>2 + log 2 (log 2 (real n) + 3)))"
     unfolding sum_list_triv_ereal by simp
   also have "... \<le> 2^40 * (ln(1/\<delta>)+1)/ \<epsilon>^2 + log 2 (log 2 n + 3)" (is "?L1 \<le> ?R1")
   proof (cases "stage_two")
     case True
     have "\<lceil>4*ln (1/\<delta>)/ln(ln n\<^sub>0)\<rceil> \<le> 4*ln (1/\<delta>)/ln(ln n\<^sub>0) + 1"
       by simp
     also have "... \<le> 4*ln (1/\<delta>)/ln(ln n\<^sub>0) + ln (1/\<delta>)/ln(ln n\<^sub>0)"
       using m_gt_0_aux[OF True] by (intro add_mono) auto
     also have "... = 5 * ln (1/\<delta>)/ln(ln n\<^sub>0)" by simp
     finally have 3: "\<lceil>4*ln (1/\<delta>)/ln(ln n\<^sub>0)\<rceil> \<le> 5 * ln (1/\<delta>)/ln(ln n\<^sub>0)"
       by simp
 
     have 4: "0 \<le> 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 \<le> exp (1::real)"  "1.2 / ln 2 \<le> (2::real)"
       by (approximation 5)+
 
     have "log 2(log 2 (real n)+3) \<le> 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 "... \<le> 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 "... \<le> 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 "... \<le> (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 "... \<le> 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) \<le> 2 * ln (ln n\<^sub>0)"
       by simp
     hence 6: "log 2(log 2 (real n)+3)/ln(ln n\<^sub>0) \<le> 2"
       using n_lbound by (subst pos_divide_le_eq) simp_all
 
     have "?L1 = real(nat \<lceil>4*ln (1/\<delta>)/ln(ln n\<^sub>0)\<rceil>)*(2^36*(ln (ln n\<^sub>0)+1)/\<epsilon>^2+log 2(log 2 (real n)+3))"
       using True unfolding m_def \<delta>\<^sub>i_def by simp
     also have "... = \<lceil>4*ln (1/\<delta>)/ln(ln n\<^sub>0)\<rceil>*(2^36*(ln (ln n\<^sub>0)+1)/\<epsilon>^2+log 2(log 2 (real n)+3))"
       using m_gt_0_aux[OF True] by (subst of_nat_nat) simp_all
     also have "... \<le> (5*ln (1/\<delta>)/ln(ln n\<^sub>0)) *(2^36*(ln (ln n\<^sub>0)+1)/\<epsilon>^2+log 2(log 2 (real n)+3))"
       using n_lbound(3) \<epsilon>_gt_0  4 by (intro ereal_mono mult_right_mono
           add_nonneg_nonneg divide_nonneg_pos mult_nonneg_nonneg 3) simp_all
     also have "... \<le> (5 * ln (1/\<delta>)/ln(ln n\<^sub>0))*((2^36+2^36)*ln (ln n\<^sub>0)/\<epsilon>^2+log 2(log 2 (real n)+3))"
       using n_lbound \<delta>_gt_0 \<delta>_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/\<delta>)/ \<epsilon>^2 + (5*ln (1/\<delta>)) * (log 2(log 2 (real n)+3)/ln(ln n\<^sub>0))"
       using n_lbound by (simp add:algebra_simps)
     also have "... \<le> 5*(2^37)* ln (1/\<delta>)/ \<epsilon>^2 + (5*ln(1/ \<delta>)) * 2"
       using \<delta>_gt_0 \<delta>_lt_1 by (intro add_mono ereal_mono order.refl mult_left_mono 6) auto
     also have "... = 5*(2^37)* ln (1/\<delta>)/ \<epsilon>^2 + 5*2*ln(1/ \<delta>) / 1"
       by simp
     also have "... \<le> 5*(2^37)* ln (1/\<delta>)/ \<epsilon>^2 + 5*2*ln(1/ \<delta>) / \<epsilon>^2"
       using \<epsilon>_gt_0 \<epsilon>_lt_1 \<delta>_gt_0 \<delta>_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/\<delta>)+0)/ \<epsilon>^2 + 0"
       by (simp add:algebra_simps)
     also have "... \<le> 2^40 * (ln (1 / \<delta>)+1) / \<epsilon>^2 +  log 2 (log 2 (real n) + 3)"
       using \<epsilon>_gt_0 \<epsilon>_lt_1 \<delta>_gt_0 \<delta>_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/\<delta>)+ 1)/\<epsilon>\<^sup>2 + log 2 (log 2 (real n) + 3)"
       using False unfolding \<delta>\<^sub>i_def m_def by simp
     also have "... \<le> ?R1"
       using \<epsilon>_gt_0 \<epsilon>_lt_1 \<delta>_gt_0 \<delta>_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 \<open>Encoding function for the seeds which are just natural numbers smaller than
 @{term "pro_size \<Theta>"}.\<close>
 
 definition encode_seed
   where "encode_seed = Nb\<^sub>e (pro_size \<Theta>)"
 
 lemma encode_seed:
   "is_encoding encode_seed"
   unfolding encode_seed_def by (intro bounded_nat_encoding)
 
 lemma random_bit_count:
   assumes "\<omega> < pro_size \<Theta>"
   shows "bit_count (encode_seed \<omega>) \<le> seed_space_usage (real n, \<epsilon>, \<delta>)"
     (is "?L \<le> ?R")
 proof -
   have 0: "pro_size \<Theta> > 0" by (intro pro_size_gt_0)
   have 1: "pro_size I.\<Omega> > 0" by (intro pro_size_gt_0)
 
   have "(55+60*ln (ln n\<^sub>0))^3 \<le> (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 "... \<le> 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 "... \<le> 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 "... \<le> 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 \<le> 180^3 * ln n + 180^3*exp 5"
     by simp
 
   have 3:"(1::real)+180^3*exp 5 \<le> 2^30" "(4::real)/ln 2 + 180^3 \<le> 2^23"
     by (approximation 10)+
 
   have "?L = ereal (real (floorlog 2 (pro_size \<Theta> - 1)))"
     using assms unfolding encode_seed_def bounded_nat_bit_count by simp
   also have "... \<le> ereal (real (floorlog 2 (pro_size \<Theta>)))"
     by (intro ereal_mono Nat.of_nat_mono floorlog_mono) auto
   also have "... = ereal (1 + of_int \<lfloor>log 2 (real (pro_size \<Theta>))\<rfloor>)"
     using 0 unfolding floorlog_def by simp
   also have "... \<le> ereal (1 + log 2 (real (pro_size \<Theta>)))"
     by (intro add_mono ereal_mono) auto
   also have "... = 1 + log 2 (real (pro_size I.\<Omega>) * (2^4) ^ ((m - 1) * nat \<lceil>ln \<alpha> / ln 0.95\<rceil>))"
     unfolding expander_pro_size[OF \<Theta>] by simp
   also have "... = 1 + log 2 (real (pro_size I.\<Omega>) * 2^ (4 * (m - 1) * nat \<lceil>ln \<alpha> / ln 0.95\<rceil>))"
     unfolding power_mult by simp
   also have "... = 1 + log 2 (real (pro_size I.\<Omega>)) + (4*(m-1)* nat\<lceil>ln \<alpha> / ln 0.95\<rceil>)"
     using 1 by (subst log_mult) simp_all
   also have "... \<le> 1+log 2(2 powr (4*log 2 n + 48 * (log 2 (1/\<epsilon>)+16)\<^sup>2+ (55+60*ln (1/\<delta>\<^sub>i))^3))+
     (4*(m-1)* nat\<lceil>ln \<alpha> / ln 0.95\<rceil>)"
     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/\<epsilon>)+16)\<^sup>2+(55+60*ln (1/\<delta>\<^sub>i))^3+(4*(m-1)*nat\<lceil>ln \<alpha>/ln 0.95\<rceil>)"
     by (subst log_powr_cancel) auto
   also have "... \<le> 2^30 + 2^23*ln n+48*(log 2(1/\<epsilon>)+16)\<^sup>2 + 336*ln (1/\<delta>)" (is "?L1 \<le> ?R1")
   proof (cases "stage_two")
     case True
 
     have "-1 < (0::real)" by simp
     also have "... \<le> ln \<alpha> / ln 0.95"
       using \<alpha>_gt_0 \<alpha>_le_1 by (intro divide_nonpos_neg) auto
     finally have 4: "- 1 < ln \<alpha> / ln 0.95" by simp
 
     have 5: "- 1 / ln 0.95 \<le> (20::real)"
       by (approximation 10)
 
     have "(4*(m-1)*nat\<lceil>ln \<alpha>/ln 0.95\<rceil>) = 4 * (real m-1) * of_int \<lceil>ln \<alpha>/ln 0.95\<rceil>"
       using 4 m_gt_0 unfolding of_nat_mult by (subst of_nat_nat) auto
     also have "... \<le> 4 * (real m-1) * (ln \<alpha>/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 \<alpha>_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 "... \<le> 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 \<lceil>4 * ln (1 / \<delta>) / ln (ln n\<^sub>0)\<rceil>)-1) *  (ln (ln n\<^sub>0) * 20 + 1)"
       using True unfolding m_def by simp
     also have "... = 4 * (real_of_int \<lceil>4 * ln (1 / \<delta>) / ln (ln n\<^sub>0)\<rceil>-1) *  (ln (ln n\<^sub>0) * 20 + 1)"
       using m_gt_0_aux[OF True] by (subst of_nat_nat) simp_all
     also have "... \<le> 4 * (4 * ln (1 / \<delta>) / 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 "... \<le> 4 * (4 * ln (1 / \<delta>) / ln (ln n\<^sub>0)) * (ln (ln n\<^sub>0) * 20 + ln (ln n\<^sub>0))"
       using \<delta>_gt_0 \<delta>_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  / \<delta>)"
       using n_lbound by simp
     finally have 6: "4 * (m-1) * nat \<lceil>ln \<alpha>/ln 0.95\<rceil> \<le> 336 * ln (1/\<delta>)"
       by simp
 
     have "?L1 =1+4*log 2 n+48*(log 2(1/\<epsilon>)+16)\<^sup>2+(55+60*ln (ln n\<^sub>0))^3+(4*(m-1)*nat\<lceil>ln \<alpha>/ln 0.95\<rceil>)"
       using True unfolding \<delta>\<^sub>i_def by simp
     also have "... \<le> 1+4*log 2 n+48*(log 2(1/\<epsilon>)+16)\<^sup>2+(180^3 * ln n + 180^3*exp 5) + 336 * ln (1/\<delta>)"
       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/\<epsilon>)+16)\<^sup>2+ 336 * ln (1/\<delta>)"
       by (simp add:log_def algebra_simps)
     also have "... \<le> 2^30 + 2^23*ln n+48*(log 2(1/\<epsilon>)+16)\<^sup>2+ 336 * ln (1/\<delta>)"
       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 / \<delta> \<le> ln n\<^sub>0"
       using \<delta>_gt_0 n_lbound
       unfolding stage_two_def not_less by (simp add:divide_simps ac_simps)
     hence 7: "ln (1 / \<delta>) \<le> ln (ln n\<^sub>0)"
       using n_lbound \<delta>_gt_0 \<delta>_lt_1
       by (intro iffD2[OF ln_le_cancel_iff]) auto
 
     have 8: "0 \<le> 336*ln (1/\<delta>) "
       using \<delta>_gt_0 \<delta>_lt_1 by auto
 
     have "?L1 = 1 + 4 * log 2 (real n) + 48 * (log 2 (1 / \<epsilon>) + 16)\<^sup>2 + (55 + 60 * ln (1 / \<delta>)) ^ 3"
       using False unfolding \<delta>\<^sub>i_def m_def by simp
     also have "... \<le> 1 + 4 * log 2 (real n) + 48 * (log 2 (1 / \<epsilon>) + 16)\<^sup>2 + (55 + 60 * ln (ln n\<^sub>0))^3"
       using \<delta>_gt_0 \<delta>_lt_1
       by (intro add_mono order.refl ereal_mono power_mono mult_left_mono add_nonneg_nonneg 7) auto
     also have "... \<le> 1+4*log 2(real n)+48*(log 2 (1 / \<epsilon>)+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/\<epsilon>)+16)\<^sup>2+ 0"
       by (simp add:log_def algebra_simps)
     also have "... \<le> 2^30 + 2^23*ln n+48*(log 2(1/\<epsilon>)+16)\<^sup>2 + 336*ln (1/\<delta>)"
       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, \<epsilon>, \<delta>)"
     unfolding seed_space_usage_def by simp
   finally show ?thesis by simp
 qed
 
 text \<open>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, \<epsilon>, \<delta>)"} bits to encode and
 @{term "estimate x"} approximates the count of the distinct universe elements in the expression.
 
 For example:
 
 @{term "estimate (merge (single \<omega> 1) (merge (single \<omega> 5) (single \<omega> 1)))"} approximates the
 cardinality of @{term "{1::nat, 5, 1}"} i.e. $2$.\<close>
 
 datatype sketch_tree = Single nat | Merge sketch_tree sketch_tree
 
 fun eval :: "nat \<Rightarrow> sketch_tree \<Rightarrow> state"
   where
     "eval \<omega> (Single x) = single \<omega> x" |
     "eval \<omega> (Merge x y) = merge (eval \<omega> x) (eval \<omega> y)"
 
 fun sketch_tree_set :: "sketch_tree \<Rightarrow> nat set"
   where
     "sketch_tree_set (Single x) = {x}" |
     "sketch_tree_set (Merge x y) = sketch_tree_set x \<union> sketch_tree_set y"
 
 theorem correctness:
   fixes X
   assumes "sketch_tree_set t \<subseteq> {..<n}"
   defines "p \<equiv> pmf_of_set {..<pro_size \<Theta>}"
   defines "X \<equiv> real (card (sketch_tree_set t))"
   shows "measure p {\<omega>. \<bar>estimate (eval \<omega> t) - X\<bar> > \<epsilon> * X} \<le> \<delta>" (is "?L \<le> ?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 \<omega> t = \<nu> \<omega> A" for \<omega>
     unfolding A_def using single_result merge_result
     by (induction t) (auto simp del:merge.simps single.simps)
 
   have 1: "A \<subseteq> {..<n}"
     using assms(1) unfolding A_def by blast
 
   have 2: "A \<noteq> {}"
     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 "\<omega> < pro_size \<Theta>"
   shows
     "bit_count (encode_state (eval \<omega> t)) \<le> state_space_usage (real n, \<epsilon>, \<delta>)" (is "?A")
     "bit_count (encode_seed \<omega>) \<le> seed_space_usage (real n, \<epsilon>, \<delta>)" (is "?B")
 proof-
   define A where "A = sketch_tree_set t"
 
   have 0:"eval \<omega> t = \<nu> \<omega> A" for \<omega>
     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 \<open>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$.\<close>
 
 context
 begin
 
 text \<open>Some local notation to ease proofs about the asymptotic space usage of the algorithm:\<close>
 
 private definition n_of :: "real \<times> real \<times> real \<Rightarrow> real" where "n_of = (\<lambda>(n, \<epsilon>, \<delta>). n)"
 private definition \<delta>_of :: "real \<times> real \<times> real \<Rightarrow> real" where "\<delta>_of = (\<lambda>(n, \<epsilon>, \<delta>). \<delta>)"
 private definition \<epsilon>_of :: "real \<times> real \<times> real \<Rightarrow> real" where "\<epsilon>_of = (\<lambda>(n, \<epsilon>, \<delta>). \<epsilon>)"
 
 private abbreviation F :: "(real \<times> real \<times> real) filter"
   where "F \<equiv> (at_top \<times>\<^sub>F at_right 0 \<times>\<^sub>F at_right 0)"
 
 private lemma var_simps:
   "n_of = fst"
   "\<epsilon>_of = (\<lambda>x. fst (snd x))"
   "\<delta>_of = (\<lambda>x. snd (snd x))"
   unfolding n_of_def \<epsilon>_of_def \<delta>_of_def by (auto simp add:case_prod_beta)
 
 private lemma evt_n: "eventually (\<lambda>x. n_of x \<ge> 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: "\<forall>\<^sub>F x in F. 0 \<le> ln (n_of x)"
   by (intro eventually_mono[OF evt_n[of "1"]] ln_ge_zero) simp
 
 private lemma evt_n_2: "\<forall>\<^sub>F x in F. 0 \<le> 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_\<epsilon>: "eventually (\<lambda>x. 1/\<epsilon>_of x \<ge> \<epsilon> \<and> \<epsilon>_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_\<delta>: "eventually (\<lambda>x. 1/\<delta>_of x \<ge> \<delta> \<and> \<delta>_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_\<delta>_1: "\<forall>\<^sub>F x in F. 0 \<le> ln (1 / \<delta>_of x)"
   by (intro eventually_mono[OF evt_\<delta>[of "1"]] ln_ge_zero) simp
 
 theorem asymptotic_state_space_complexity:
   "state_space_usage \<in> O[F](\<lambda>(n, \<epsilon>, \<delta>). ln (1/\<delta>)/\<epsilon>^2 + ln (ln n))"
   (is "_ \<in> O[?F](?rhs)")
 proof -
   have 0:"(\<lambda>x. 1) \<in> O[?F](\<lambda>x. ln (1 / \<delta>_of x))"
     using order_less_le_trans[OF exp_gt_zero]
     by (intro landau_o.big_mono eventually_mono[OF evt_\<delta>[of "exp 1"]])
       (auto intro!: iffD2[OF ln_ge_iff] simp add:abs_ge_iff)
 
   have 1:"(\<lambda>x. 1) \<in> O[?F](\<lambda>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 "(\<lambda>x. ((ln (1/\<delta>_of x)+1)* (1/\<epsilon>_of x)\<^sup>2))\<in> O[?F](\<lambda>x. ln(1/\<delta>_of x)* (1/\<epsilon>_of x)\<^sup>2)"
     by (intro landau_o.mult sum_in_bigo 0) simp_all
   hence 2: "(\<lambda>x. 2^40*((ln (1/\<delta>_of x)+1)* (1/\<epsilon>_of x)\<^sup>2))\<in> O[?F](\<lambda>x. ln(1/\<delta>_of x)* (1/\<epsilon>_of x)\<^sup>2)"
     unfolding cmult_in_bigo_iff by simp
 
   have 3: "(1::real) \<le> exp 2"
     by (approximation 5)
 
   have "(\<lambda>x. ln (n_of x) / ln 2 + 3) \<in> O[?F](\<lambda>x. ln (n_of x))"
     using 1 by (intro sum_in_bigo) simp_all
   hence "(\<lambda>x. ln (ln (n_of x) / ln 2 + 3)) \<in> O[?F](\<lambda>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: "(\<lambda>x. log 2 (log 2 (n_of x) + 3))\<in> O[?F](\<lambda>x. ln(ln(n_of x)))"
     unfolding log_def by simp
 
   have 5: "\<forall>\<^sub>F x in ?F. 0 \<le> ln (1 / \<delta>_of x) * (1 / \<epsilon>_of x)\<^sup>2"
     by (intro eventually_mono[OF eventually_conj[OF evt_\<delta>_1 evt_\<epsilon>[of "1"]]]) auto
 
   have "state_space_usage = (\<lambda>x. state_space_usage (n_of x, \<epsilon>_of x, \<delta>_of x))"
     by (simp add:case_prod_beta' n_of_def \<delta>_of_def \<epsilon>_of_def)
   also have "... = (\<lambda>x. 2 ^ 40 * ((ln (1 / (\<delta>_of x)) + 1)* (1/\<epsilon>_of x)\<^sup>2) + log 2 (log 2 (n_of x)+3))"
     unfolding state_space_usage_def by (simp add:divide_simps)
   also have "... \<in> O[?F](\<lambda>x. ln (1/\<delta>_of x)* (1/\<epsilon>_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 \<delta>_of_def \<epsilon>_of_def divide_simps)
   finally show ?thesis by simp
 qed
 
 theorem asymptotic_seed_space_complexity:
   "seed_space_usage \<in> O[F](\<lambda>(n, \<epsilon>, \<delta>). ln (1/\<delta>)+ln (1/\<epsilon>)^2 + ln n)"
   (is "_ \<in> O[?F](?rhs)")
 proof -
   have 0: "\<forall>\<^sub>F x in ?F. 0 \<le> (ln (1 / \<epsilon>_of x))\<^sup>2"
     by simp
 
   have 1: "\<forall>\<^sub>F x in ?F. 0 \<le> ln (1 / \<delta>_of x) + (ln (1 / \<epsilon>_of x))\<^sup>2"
     by (intro eventually_mono[OF eventually_conj[OF evt_\<delta>_1 0]] add_nonneg_nonneg) auto
 
   have 2: "(\<lambda>x. 1) \<in> O[?F](\<lambda>x. ln (1 / \<epsilon>_of x))"
     using order_less_le_trans[OF exp_gt_zero]
     by (intro landau_o.big_mono eventually_mono[OF evt_\<epsilon>[of "exp 1"]])
       (auto intro!:iffD2[OF ln_ge_iff] simp add:abs_ge_iff)
 
   have "(\<lambda>x. 1) \<in> O[at_top \<times>\<^sub>F at_right 0 \<times>\<^sub>F at_right 0](\<lambda>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: "(\<lambda>x. 1) \<in> O[?F](\<lambda>x. ln (1 / \<delta>_of x) + (ln (1 / \<epsilon>_of x))\<^sup>2 + ln (n_of x))"
     by (intro landau_sum_2 1 evt_n_1 0 evt_\<delta>_1) simp
   have 4: "(\<lambda>x. ln (n_of x)) \<in> O[?F](\<lambda>x. ln (1 / \<delta>_of x) + (ln (1 / \<epsilon>_of x))\<^sup>2 + ln (n_of x))"
     by (intro landau_sum_2 1 evt_n_1) simp
   have "(\<lambda>x. log 2 (1 / \<epsilon>_of x) + 16) \<in> O[?F](\<lambda>x. ln (1 / \<epsilon>_of x))"
     using 2 unfolding log_def by (intro sum_in_bigo) simp_all
   hence 5: "(\<lambda>x. (log 2 (1 / \<epsilon>_of x) + 16)\<^sup>2) \<in> O[?F](\<lambda>x. ln (1/\<delta>_of x)+(ln (1/\<epsilon>_of x))\<^sup>2)"
     using 0 unfolding power2_eq_square by (intro landau_sum_2 landau_o.mult evt_\<delta>_1) simp_all
   have 6: "(\<lambda>x. (log 2 (1 / \<epsilon>_of x) + 16)\<^sup>2) \<in> O[?F](\<lambda>x. ln (1/\<delta>_of x)+(ln (1/\<epsilon>_of x))\<^sup>2+ln (n_of x))"
     by (intro landau_sum_1[OF _ _ 5] 1 evt_n_1)
   have 7: "(\<lambda>x. ln (1/\<delta>_of x)) \<in> O[?F](\<lambda>x. ln (1/\<delta>_of x)+(ln (1/\<epsilon>_of x))\<^sup>2+ln (n_of x))"
     by (intro landau_sum_1 1 evt_\<delta>_1 0 evt_n_1) simp
 
   have "seed_space_usage = (\<lambda>x. seed_space_usage (n_of x, \<epsilon>_of x, \<delta>_of x))"
     by (simp add:case_prod_beta' n_of_def \<delta>_of_def \<epsilon>_of_def)
   also have "... = (\<lambda>x. 2^30+2^23*ln (n_of x)+48*(log 2 (1/(\<epsilon>_of x))+16)\<^sup>2 + 336 * ln (1 / \<delta>_of x))"
     unfolding seed_space_usage_def by (simp add:divide_simps)
   also have "... \<in> O[?F](\<lambda>x. ln (1/\<delta>_of x)+ln (1/\<epsilon>_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 \<delta>_of_def \<epsilon>_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 \<in> O[at_top \<times>\<^sub>F at_right 0 \<times>\<^sub>F at_right 0](\<lambda>(n, \<epsilon>, \<delta>). ln (1/\<delta>)/\<epsilon>^2 + ln n)"
 proof -
   let ?f1 = "(\<lambda>x. ln (1/\<delta>_of x)*(1/\<epsilon>_of x^2)+ln (ln (n_of x)))"
   let ?f2 = "(\<lambda>x. ln(1/\<delta>_of x)+ln(1/\<epsilon>_of x)^2+ln (n_of x))"
 
   have 0: "\<forall>\<^sub>F x in F. 0 \<le> (1 / (\<epsilon>_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: "\<forall>\<^sub>F x in F. 0 \<le> ln (1 / \<delta>_of x) * (1 / (\<epsilon>_of x)\<^sup>2)"
     by (intro eventually_mono[OF eventually_conj[OF evt_\<delta>_1 0]] mult_nonneg_nonneg) auto
 
   have 2: "\<forall>\<^sub>F x in F. 0 \<le> ln (1 / \<delta>_of x) * (1 / (\<epsilon>_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: "\<forall>\<^sub>F x in F. 0 \<le> ln (1 / (\<epsilon>_of x)\<^sup>2)"
     unfolding power_one_over[symmetric]
     by (intro eventually_mono[OF evt_\<epsilon>[of "1"]] ln_ge_zero) simp
 
   have 4: "\<forall>\<^sub>F x in F. 0 \<le> ln (1 / \<delta>_of x) + (ln (1 / \<epsilon>_of x))\<^sup>2 + ln (n_of x)"
     by (intro eventually_mono[OF eventually_conj[OF evt_n_1 eventually_conj[OF evt_\<delta>_1 3]]]
         add_nonneg_nonneg) auto
 
   have 5: "(\<lambda>_. 1) \<in> O[F](\<lambda>x. 1 / (\<epsilon>_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: "(\<lambda>_. 1) \<in> O[F](\<lambda>x. ln (1 / \<delta>_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 \<in> O[F](\<lambda>x. ln (1 / \<delta>_of x) * (1 / (\<epsilon>_of x)\<^sup>2) + ln (ln (n_of x)))"
     using asymptotic_state_space_complexity unfolding \<delta>_of_def \<epsilon>_of_def n_of_def
     by (simp add:case_prod_beta')
 
   have 8: "seed_space_usage \<in> O[F](\<lambda>x. ln (1 / \<delta>_of x) + (ln (1 / \<epsilon>_of x))\<^sup>2 + ln (n_of x))"
     using asymptotic_seed_space_complexity unfolding \<delta>_of_def \<epsilon>_of_def n_of_def
     by (simp add:case_prod_beta')
 
   have 9: "(\<lambda>x. ln (n_of x)) \<in> O[F](\<lambda>x. ln (1 / \<delta>_of x) * (1 / (\<epsilon>_of x)\<^sup>2) + ln (n_of x))"
     by (intro landau_sum_2 evt_n_1 1) simp
 
   have "(\<lambda>x. (ln (1 / \<epsilon>_of x))\<^sup>2) \<in> O[F](\<lambda>x. 1 / \<epsilon>_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: "(\<lambda>x. (ln (1 / \<epsilon>_of x))\<^sup>2) \<in> O[F](\<lambda>x. ln (1 / \<delta>_of x) * (1 / \<epsilon>_of x^2) + ln (n_of x))"
     by (intro landau_sum_1 evt_n_1 1 landau_o.big_mult_1' 6)
   have 11: "(\<lambda>x. ln (1 / \<delta>_of x)) \<in> O[F](\<lambda>x. ln (1 / \<delta>_of x) * (1 / \<epsilon>_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: "(\<lambda>x. ln (1/\<delta>_of x) * (1/\<epsilon>_of x^2)) \<in> O[F](\<lambda>x. ln (1/\<delta>_of x)*(1/\<epsilon>_of x^2)+ln (n_of x))"
     by (intro landau_sum_1 1 evt_n_1) simp
 
   have "(\<lambda>x. ln (ln (n_of x))) \<in> O[F](\<lambda>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: "(\<lambda>x. ln (ln (n_of x))) \<in> O[F](\<lambda>x. ln (1 / \<delta>_of x) * (1 / \<epsilon>_of x^2) + ln (n_of x))"
     by (intro landau_sum_2 evt_n_1 1)
 
   have "space_usage = (\<lambda>x. state_space_usage x + seed_space_usage x)"
     unfolding space_usage_def by simp
   also have "... \<in> O[F](\<lambda>x. ?f1 x + ?f2 x)"
     by (intro landau_sum 2 4 7 8)
   also have "... \<subseteq> O[F](\<lambda>x. ln (1 / \<delta>_of x) * (1/\<epsilon>_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](\<lambda>(n, \<epsilon>, \<delta>). ln (1/\<delta>)/\<epsilon>^2 + ln n)"
     unfolding \<delta>_of_def \<epsilon>_of_def n_of_def
     by (simp add:case_prod_beta')
   finally show ?thesis by simp
 qed
 
 end
 
 unbundle no_intro_cong_syntax
 
 end
diff --git a/thys/Median_Method/Median.thy b/thys/Median_Method/Median.thy
--- a/thys/Median_Method/Median.thy
+++ b/thys/Median_Method/Median.thy
@@ -1,887 +1,885 @@
 section \<open>Intervals are Borel measurable\<close>
 
 theory Median
   imports 
     "HOL-Probability.Probability" 
     "HOL-Library.Multiset" 
     "Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families"
 begin
 
 text \<open>This section contains a proof that intervals are Borel measurable, where an interval is
 defined as a convex subset of linearly ordered space, more precisely, a set is an interval, if 
 for each triple of points $x < y < z$: If $x$ and $z$ are in the set so is $y$.
 This includes ordinary intervals like @{term "{a..b}"}, @{term "{a<..<b}"} but also for example
 @{term [show_types] "{(x::rat). x * x < 2}"} which cannot be expressed in the standard notation.
 
 In the @{theory "HOL-Analysis.Borel_Space"} there are proofs for the measurability of each specific
 type of interval, but those unfortunately do not help if we want to express the result about the
 median bound for arbitrary types of intervals.\<close>
 
 definition interval :: "('a :: linorder) set \<Rightarrow> bool" where
   "interval I = (\<forall>x y z. x \<in> I \<longrightarrow> z \<in> I \<longrightarrow> x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> y \<in> I)"
 
 definition up_ray :: "('a :: linorder) set \<Rightarrow> bool" where
   "up_ray I = (\<forall>x y. x \<in> I \<longrightarrow> x \<le> y \<longrightarrow> y \<in> I)"
 
 lemma up_ray_borel:
   assumes "up_ray (I :: (('a :: linorder_topology) set))"
   shows "I \<in> borel"
 proof (cases "closed I")
   case True
   then show ?thesis using borel_closed by blast
 next
   case False
   hence b:"\<not> closed I" by blast
 
   have "open I"
   proof (rule Topological_Spaces.openI)
     fix x
     assume c:"x \<in> I"
     show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> I"
     proof (cases "\<exists>y. y < x \<and> y \<in> I")
       case True
       then obtain y where a:"y < x \<and> y \<in> I" by blast
       have "open {y<..}" by simp
       moreover have "x \<in> {y<..}" using a by simp
       moreover have "{y<..} \<subseteq> I"
         using a assms(1) by (auto simp: up_ray_def) 
       ultimately show ?thesis by blast
     next
       case False
       hence "I \<subseteq> {x..}" using linorder_not_less by auto
       moreover have "{x..} \<subseteq> I"
         using c assms(1) unfolding up_ray_def by blast
       ultimately have "I = {x..}" 
         by (rule order_antisym)
       moreover have "closed {x..}" by simp
       ultimately have "False" using b by auto
       then show ?thesis by simp
     qed
   qed
   then show ?thesis by simp
 qed
 
 definition down_ray :: "('a :: linorder) set \<Rightarrow> bool" where
   "down_ray I = (\<forall>x y. y \<in> I \<longrightarrow> x \<le> y \<longrightarrow> x \<in> I)"
 
 lemma down_ray_borel:
   assumes "down_ray (I :: (('a :: linorder_topology) set))"
   shows "I \<in> borel"
 proof -
   have "up_ray (-I)" using assms 
     by (simp add: up_ray_def down_ray_def, blast)
   hence "(-I) \<in> borel" using up_ray_borel by blast
   thus "I \<in> borel" 
     by (metis borel_comp double_complement)
 qed
 
 text \<open>Main result of this section:\<close>
 
 lemma interval_borel:
   assumes "interval (I :: (('a :: linorder_topology) set))"
   shows "I \<in> borel"
 proof (cases "I = {}")
   case True
   then show ?thesis by simp
 next
   case False
   then obtain x where a:"x \<in> I" by blast
   have "\<And>y z. y \<in> I \<union> {x..} \<Longrightarrow> y \<le> z \<Longrightarrow> z \<in> I \<union> {x..}" 
     by (metis assms a interval_def  IntE UnE Un_Int_eq(1) Un_Int_eq(2) atLeast_iff nle_le order.trans)
   hence "up_ray (I \<union> {x..})"
     using up_ray_def by blast
   hence b:"I \<union> {x..} \<in> borel" 
     using up_ray_borel by blast
 
   have "\<And>y z. y \<in> I \<union> {..x} \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> I \<union> {..x}" 
     by (metis assms a interval_def UnE UnI1 UnI2 atMost_iff dual_order.trans linorder_le_cases)
   hence "down_ray (I \<union> {..x})"
     using down_ray_def by blast
   hence c:"I \<union> {..x} \<in> borel"
     using down_ray_borel by blast
 
   have "I = (I \<union> {x..}) \<inter> (I \<union> {..x})"
     using a by fastforce    
 
   then show ?thesis using b c
     by (metis sets.Int)
 qed
 
 section \<open>Order statistics are Borel measurable\<close>
 
 text \<open>This section contains a proof that order statistics of Borel measurable random variables are
 themselves Borel measurable.
 
 The proof relies on the existence of branch-free comparison-sort algorithms. Given a sequence length
 these algorithms perform compare-swap operations on predefined pairs of positions. In particular the
 result of a comparison does not affect future operations. An example for a branch-free comparison
 sort algorithm is shell-sort and also bubble-sort without the early exit.
 
 The advantage of using such a comparison-sort algorithm is that it can be lifted to work on random
 variables, where the result of a comparison-swap operation on two random variables @{term"X"} and
 @{term"Y"} can be represented as the expressions @{term "\<lambda>\<omega>. min (X \<omega>) (Y \<omega>)"} and
 @{term "\<lambda>\<omega>. max (X \<omega>) (Y \<omega>)"}.
 
 Because taking the point-wise minimum (resp. maximum) of two random variables is still
 Borel measurable, and because the entire sorting operation can be represented using such
 compare-swap operations, we can show that all order statistics are Borel measuable.\<close>
 
 fun sort_primitive where
   "sort_primitive i j f k = (if k = i then min (f i) (f j) else (if k = j then max (f i) (f j) else f k))"
 
 fun sort_map where
   "sort_map f n = fold id [sort_primitive j i. i <- [0..<n], j <- [0..<i]] f"
 
 lemma sort_map_ind:
   "sort_map f (Suc n) = fold id [sort_primitive j n. j <- [0..<n]] (sort_map f n)"
   by simp
 
 lemma sort_map_strict_mono:
   fixes f :: "nat \<Rightarrow> 'b :: linorder"
   shows "j < n \<Longrightarrow> i < j \<Longrightarrow> sort_map f n i \<le> sort_map f n j"
 proof (induction n arbitrary: i j)
   case 0
   then show ?case by simp
 next
   case (Suc n)
   define g where "g = (\<lambda>k. fold id [sort_primitive j n. j <- [0..<k]] (sort_map f n))"
   define k where "k = n"
   have a:"(\<forall>i j. j < n \<longrightarrow> i < j \<longrightarrow> g k i \<le> g k j) \<and> (\<forall>l. l < k \<longrightarrow> g k l \<le> g k n)"
   proof (induction k)
     case 0
     then show ?case using Suc by (simp add:g_def del:sort_map.simps)
   next
     case (Suc k)
     have "g (Suc k) = sort_primitive k n (g k)" 
       by (simp add:g_def)
     then show ?case using Suc
       apply (cases "g k k \<le> g k n")
        apply (simp add:min_def max_def)
        using less_antisym apply blast
       apply (cases "g k n \<le> g k k")
        apply (simp add:min_def max_def)
        apply (metis less_antisym max.coboundedI2 max.orderE)
       by simp
   qed
 
   hence "\<And>i j. j < Suc n \<Longrightarrow> i < j \<Longrightarrow> g n i \<le> g n j"
     apply (simp add:k_def) using less_antisym by blast
   moreover have "sort_map f (Suc n) = g n" 
     by (simp add:sort_map_ind g_def del:sort_map.simps)
   ultimately show ?case
     using Suc by (simp del:sort_map.simps)
 qed
 
 lemma sort_map_mono:
   fixes f :: "nat \<Rightarrow> 'b :: linorder"
   shows "j < n \<Longrightarrow> i \<le> j \<Longrightarrow> sort_map f n i \<le> sort_map f n j"
   by (metis sort_map_strict_mono eq_iff le_imp_less_or_eq)
 
 lemma sort_map_perm:
   fixes f :: "nat \<Rightarrow> 'b :: linorder"
   shows "image_mset (sort_map f n) (mset [0..<n]) = image_mset f (mset [0..<n])"
 proof -
   define is_swap where "is_swap = (\<lambda>(ts :: ((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b)). \<exists>i < n. \<exists>j < n. ts = sort_primitive i j)"
   define t :: "((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b) list" 
     where "t = [sort_primitive j i. i <- [0..<n], j <- [0..<i]]"
 
   have a: "\<And>x f. is_swap x \<Longrightarrow> image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})"
   proof -
     fix x
     fix f :: "nat \<Rightarrow> 'b :: linorder"
     assume "is_swap x"
     then obtain i j where x_def: "x = sort_primitive i j" and i_bound: "i < n" and j_bound:"j < n" 
       using is_swap_def by blast
     define inv where "inv = mset_set {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j}"
     have b:"{0..<n} = {k. k < n \<and> k \<noteq> i \<and> k \<noteq> j} \<union> {i,j}"
       apply (rule order_antisym, rule subsetI, simp, blast, rule subsetI, simp)
       using i_bound j_bound by meson
     have c:"\<And>k. k \<in># inv \<Longrightarrow> (x f) k = f k" 
       by (simp add:x_def inv_def)
     have "image_mset (x f) inv = image_mset f inv"
       apply (rule multiset_eqI)
       using c multiset.map_cong0 by force
     moreover have "image_mset (x f) (mset_set {i,j}) = image_mset f (mset_set {i,j})"
       apply (cases "i = j")
       by (simp add:x_def max_def min_def)+
     moreover have "mset_set {0..<n} = inv + mset_set {i,j}"
       by (simp only:inv_def b, rule mset_set_Union, simp, simp, simp) 
     ultimately show "image_mset (x f) (mset_set {0..<n}) = image_mset f (mset_set {0..<n})"
       by simp
   qed
 
   have "(\<forall>x \<in> set t. is_swap x) \<Longrightarrow> image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])"
     by (induction t arbitrary:f, simp, simp add:a) 
   moreover have "\<And>x. x \<in> set t \<Longrightarrow> is_swap x" 
     apply (simp add:t_def is_swap_def) 
     by (meson atLeastLessThan_iff imageE less_imp_le less_le_trans)  
   ultimately have "image_mset (fold id t f) (mset [0..<n]) = image_mset f (mset [0..<n])" by blast
   then show ?thesis by (simp add:t_def)
 qed
 
 lemma list_eq_iff:
   assumes "mset xs = mset ys"
   assumes "sorted xs"
   assumes "sorted ys"
   shows "xs = ys" 
   using assms properties_for_sort by blast
 
 lemma sort_map_eq_sort:
   fixes f :: "nat \<Rightarrow> ('b :: linorder)"
   shows "map (sort_map f n) [0..<n] = sort (map f [0..<n])" (is "?A = ?B")
 proof -
   have "mset ?A = mset ?B"
     using sort_map_perm[where f="f" and n="n"]
     by (simp del:sort_map.simps)
   moreover have "sorted ?B"
     by simp
   moreover have "sorted ?A"
     apply (subst sorted_wrt_iff_nth_less)
     apply (simp del:sort_map.simps)
     by (metis sort_map_mono nat_less_le)
   ultimately show "?A = ?B" 
     using list_eq_iff by blast
 qed
 
 lemma order_statistics_measurable_aux: 
   fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> ('b :: {linorder_topology, second_countable_topology})"
   assumes "n \<ge> 1" 
   assumes "j < n"
   assumes "\<And>i. i < n \<Longrightarrow> X i \<in> measurable M borel"
   shows "(\<lambda>x. (sort_map (\<lambda>i. X i x) n) j) \<in> measurable M borel"
 proof -
   have n_ge_0:"n > 0" using assms by simp
   define is_swap where "is_swap = (\<lambda>(ts :: ((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b)). \<exists>i < n. \<exists>j < n. ts = sort_primitive i j)"
   define t :: "((nat \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b) list" 
     where "t = [sort_primitive j i. i <- [0..<n], j <- [0..<i]]"
 
   define meas_ptw :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
     where "meas_ptw = (\<lambda>f. (\<forall>k. k < n \<longrightarrow> f k \<in> borel_measurable M))"
 
   have ind_step:
     "\<And>x (g :: nat \<Rightarrow> 'a \<Rightarrow> 'b). meas_ptw g \<Longrightarrow> is_swap x \<Longrightarrow> meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)"
   proof -
     fix x g
     assume "meas_ptw g"
     hence a:"\<And>k. k < n \<Longrightarrow> g k \<in> borel_measurable M" by (simp add:meas_ptw_def)
     assume "is_swap x"
     then obtain i j where x_def:"x=sort_primitive i j" and i_le:"i < n" and j_le:"j < n"
       by (simp add:is_swap_def, blast)
     have "\<And>k. k < n \<Longrightarrow> (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M"
     proof -
       fix k
       assume "k < n"
       thus " (\<lambda>\<omega>. x (\<lambda>i. g i \<omega>) k) \<in> borel_measurable M"
         apply (simp add:x_def)
         apply (cases "k = i", simp)
         using a i_le j_le borel_measurable_min apply blast
         apply (cases "k = j", simp)
         using a i_le j_le borel_measurable_max apply blast
         using a by simp
     qed
     thus "meas_ptw (\<lambda>k \<omega>. x (\<lambda>i. g i \<omega>) k)" 
       by (simp add:meas_ptw_def)
   qed
 
   have "(\<forall>x \<in> set t. is_swap x) \<Longrightarrow> meas_ptw (\<lambda> k \<omega>. (fold id t (\<lambda>k. X k \<omega>)) k)"
   proof (induction t rule:rev_induct)
     case Nil
     then show ?case using assms by (simp add:meas_ptw_def)
   next
     case (snoc x xs)
     have a:"meas_ptw (\<lambda>k \<omega>. fold (\<lambda>a. a) xs (\<lambda>k. X k \<omega>) k)" using snoc by simp
     have b:"is_swap x" using snoc by simp
     show ?case using ind_step[OF a b] by simp
   qed
   moreover have "\<And>x. x \<in> set t \<Longrightarrow> is_swap x" 
     apply (simp add:t_def is_swap_def) 
     by (meson atLeastLessThan_iff imageE less_imp_le less_le_trans)  
   ultimately show ?thesis using assms
     by (simp add:t_def[symmetric] meas_ptw_def)
 qed
 
 text \<open>Main results of this section:\<close>
 
 lemma order_statistics_measurable:
   fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> ('b :: {linorder_topology, second_countable_topology})"
   assumes "n \<ge> 1" 
   assumes "j < n"
   assumes "\<And>i. i < n \<Longrightarrow> X i \<in> measurable M borel"
   shows "(\<lambda>x. (sort (map (\<lambda>i. X i x) [0..<n])) ! j) \<in> measurable M borel"
   apply (subst sort_map_eq_sort[symmetric])
   using assms by (simp add:order_statistics_measurable_aux del:sort_map.simps)
 
 definition median :: "nat \<Rightarrow> (nat \<Rightarrow> ('a :: linorder)) \<Rightarrow> 'a" where
   "median n f = sort (map f [0..<n]) ! (n div 2)"
 
 lemma median_measurable:
   fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> ('b :: {linorder_topology, second_countable_topology})"
   assumes "n \<ge> 1" 
   assumes "\<And>i. i < n \<Longrightarrow> X i \<in> measurable M borel"
   shows "(\<lambda>x. median n (\<lambda>i. X i x)) \<in> measurable M borel"
   apply (simp add:median_def)
   apply (rule order_statistics_measurable[OF assms(1) _ assms(2)])
   using assms(1) by force+
 
 section \<open>The Median Method\<close>
 
 text \<open>This section contains the proof for the probability that the median of independent random
 variables will be in an interval with high probability if the individual variables are in the
 same interval with probability larger than $\frac{1}{2}$.
 
 The proof starts with the elementary observation that the median of a seqeuence with $n$ elements
 is in an interval $I$ if at least half of them are in $I$. This works because after sorting the
 sequence the elements that will be in the interval must necessarily form a consecutive subsequence,
 if its length is larger than $\frac{n}{2}$ the median must be in it.
 
 The remainder follows the proof in \<^cite>\<open>\<open>\textsection 2.1\<close> in "alon1999"\<close> using the Hoeffding inequality
 to estimate the probability that at least half of the sequence elements will be in the interval $I$.\<close>
 
 lemma interval_rule:
   assumes "interval I"
   assumes "a \<le> x" "x \<le> b"
   assumes "a \<in> I"
   assumes "b \<in> I"
   shows "x \<in> I"
   using assms(1) apply (simp add:interval_def)
   using assms by blast
 
 lemma sorted_int:
   assumes "interval I"
   assumes "sorted xs"
   assumes "k < length xs" "i \<le> j" "j \<le> k "
   assumes "xs ! i \<in> I" "xs ! k \<in> I"
   shows "xs ! j \<in> I"
   apply (rule interval_rule[where a="xs ! i" and b="xs ! k"])
   using assms by (simp add: sorted_nth_mono)+
 
 lemma mid_in_interval:
   assumes "2*length (filter (\<lambda>x. x \<in> I) xs) > length xs"
   assumes "interval I"
   assumes "sorted xs"
   shows "xs ! (length xs div 2) \<in> I"
 proof -
   have "length (filter (\<lambda>x. x \<in> I) xs) > 0"  using assms(1) by linarith
   then obtain v where v_1: "v < length xs" and v_2: "xs ! v \<in> I" 
     by (metis filter_False in_set_conv_nth length_greater_0_conv)
 
   define J where "J = {k. k < length xs \<and> xs ! k \<in> I}"
 
   have card_J_min: "2*card J > length xs"
     using assms(1) by (simp add:J_def length_filter_conv_card)
 
   consider
     (a) "xs ! (length xs div 2) \<in> I" |
     (b) "xs ! (length xs div 2) \<notin> I \<and> v > (length xs div 2)" |
     (c) "xs ! (length xs div 2) \<notin> I \<and> v < (length xs div 2)"
     by (metis linorder_cases v_2)
   thus ?thesis
   proof (cases)
     case a
     then show ?thesis by simp
   next
     case b
     have p:"\<And>k. k \<le> length xs div 2 \<Longrightarrow> xs ! k \<notin> I"
       using b v_2 sorted_int[OF assms(2) assms(3) v_1, where j="length xs div 2"] apply simp by blast
-    have "card J \<le> card {Suc (length xs div 2)..<length xs}"
-      apply (rule card_mono, simp)
-      apply (rule subsetI, simp add:J_def not_less_eq_eq[symmetric])
-      using p by metis
+    hence "card J \<le> card {Suc (length xs div 2)..<length xs}"
+      unfolding J_def using not_less_eq_eq[symmetric] by (intro card_mono subsetI) auto
     hence "card J \<le> length xs - (Suc (length xs div 2))"
       using card_atLeastLessThan by metis
     hence "length xs \<le> 2*( length xs - (Suc (length xs div 2)))"
       using card_J_min by linarith
-    hence "False"
-      apply (simp add:nat_distrib)
-      apply (subst (asm) le_diff_conv2) using b v_1 apply linarith
-      by simp
+    hence "False" using b v_1 by auto
     then show ?thesis by simp
   next
     case c
-    have p:"\<And>k. k \<ge> length xs div 2 \<Longrightarrow> k < length xs \<Longrightarrow> xs ! k \<notin> I"
-      using c v_1 v_2 sorted_int[OF assms(2) assms(3), where i ="v" and j="length xs div 2"] apply simp by blast
-    have "card J \<le> card {0..<(length xs div 2)}"
-      apply (rule card_mono, simp)
-      apply (rule subsetI, simp add:J_def not_less_eq_eq[symmetric])
-      using p linorder_le_less_linear by blast
+    have "\<And>k. k \<ge> length xs div 2 \<Longrightarrow> k < length xs \<Longrightarrow> xs ! k \<notin> I"
+      using c v_1 v_2 sorted_int[OF assms(2,3), where i ="v" and j="length xs div 2"]
+      by simp blast
+    hence "card J \<le> card {0..<(length xs div 2)}"
+      unfolding J_def using linorder_le_less_linear by (intro card_mono subsetI) auto
     hence "card J \<le> (length xs div 2)"
       using card_atLeastLessThan by simp
     then show ?thesis using card_J_min by linarith
   qed
 qed
 
 lemma median_est:
   assumes "interval I"
   assumes "2*card {k. k < n \<and> f k \<in> I} > n"
   shows "median n f \<in> I"
 proof -
-  have a:"{k. k < n \<and> f k \<in> I} = {i. i < n \<and> map f [0..<n] ! i \<in> I}"
-    apply (rule order_antisym, rule subsetI, simp)
-    by (rule subsetI, simp, metis add_0 diff_zero nth_map_upt)
+  have "{k. k < n \<and> f k \<in> I} = {i. i < n \<and> map f [0..<n] ! i \<in> I}" by auto
+  thus ?thesis using assms unfolding median_def
+    by (intro mid_in_interval[OF _ assms(1),where xs="sort (map f [0..<n])", simplified])
+      (simp_all add:filter_sort comp_def length_filter_conv_card)
+qed
 
-  show ?thesis
-    apply (simp add:median_def)
-    apply (rule mid_in_interval[where I="I" and xs="sort (map f [0..<n])", simplified])
-     using assms a apply (simp add:filter_sort comp_def length_filter_conv_card)
-    by (simp add:assms)
+lemma median_est_rev:
+  assumes "interval I"
+  assumes "median n f \<notin> I"
+  shows "2*card {k. k < n \<and> f k \<notin> I} \<ge> n"
+proof (rule ccontr)
+  assume a: "\<not>(2*card {k. k < n \<and> f k \<notin> I} \<ge> n)"
+
+  have "2 * n = 2 * card {k. k < n}" by simp
+  also have "... = 2 * card ({k. k < n \<and> f k \<in> I} \<union> {k. k < n \<and> f k \<notin> I})"
+    by (intro arg_cong2[where f="(*)"] refl arg_cong[where f="card"]) auto
+  also have "... = 2 * card {k. k < n \<and> f k \<in> I} + 2 * card {k. k < n \<and> f k \<notin> I}"
+    by (subst card_Un_disjoint) auto
+  also have "... \<le> n  + 2 * card {k. k < n \<and> f k \<notin> I}"
+    using median_est[OF assms(1)] assms(2) not_less by (intro add_mono) auto
+  also have "... < n + n"
+    using a by (intro add_strict_left_mono) auto
+  finally show "False" by auto
 qed
 
 lemma prod_pmf_bernoulli_mono:
   assumes "finite I"
   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i \<and> g i \<le> 1"
   assumes "\<And>x y. x \<in> A \<Longrightarrow> (\<forall>i \<in> I. x i \<le> y i) \<Longrightarrow> y \<in> A"
   shows "measure (Pi_pmf I d (bernoulli_pmf \<circ> f)) A \<le> measure (Pi_pmf I d (bernoulli_pmf \<circ> g)) A"
     (is "?L \<le> ?R")
 proof -
   define q where "q i = pmf_of_list [(0::nat, f i), (1, g i - f i), (2, 1 - g i)]" for i
 
   have wf:"pmf_of_list_wf [(0::nat, f i), (1, g i - f i), (2, 1 - g i)]" if "i \<in> I" for i
     using assms(2)[OF that] by (intro pmf_of_list_wfI) auto
 
   have 0: "bernoulli_pmf (f i) = map_pmf (\<lambda>x. x = 0) (q i)" (is "?L1 = ?R1") 
     if "i \<in> I" for i
   proof -
     have "0 \<le> f i" "f i \<le> 1" using assms(2)[OF that] by auto
     hence "pmf ?L1 x = pmf ?R1 x" for x
       unfolding q_def pmf_map measure_pmf_of_list[OF wf[OF that]] 
       by (cases x;simp_all add:vimage_def)
     thus ?thesis
       by (intro pmf_eqI) auto
   qed
 
   have 1: "bernoulli_pmf (g i) = map_pmf (\<lambda>x. x \<in> {0,1}) (q i)" (is "?L1 = ?R1")
     if "i \<in> I" for i
   proof -
     have "0 \<le> g i" "g i \<le> 1" using assms(2)[OF that] by auto
     hence "pmf ?L1 x = pmf ?R1 x" for x
       unfolding q_def pmf_map measure_pmf_of_list[OF wf[OF that]] 
       by (cases x;simp_all add:vimage_def)
     thus ?thesis
       by (intro pmf_eqI) auto
   qed
 
   have 2: "(\<lambda>k. x k = 0) \<in> A \<Longrightarrow> (\<lambda>k. x k = 0 \<or> x k = Suc 0) \<in> A" for x
     by (erule assms(3)) auto
 
   have "?L = measure (Pi_pmf I d (\<lambda>i. map_pmf (\<lambda>x. x = 0) (q i))) A"
     unfolding comp_def by (simp add:0 cong: Pi_pmf_cong)
   also have "... = measure (map_pmf ((\<circ>) (\<lambda>x. x = 0)) (Pi_pmf I (if d then 0 else 2) q)) A"
     by (intro arg_cong2[where f="measure_pmf.prob"] Pi_pmf_map[OF assms(1)]) auto 
   also have "... = measure (Pi_pmf I (if d then 0 else 2) q) {x. (\<lambda>k. x k = 0) \<in> A}"
     by (simp add:comp_def vimage_def)
   also have "... \<le> measure (Pi_pmf I (if d then 0 else 2) q) {x. (\<lambda>k. x k \<in> {0,1}) \<in> A}"
     using 2 by (intro measure_pmf.finite_measure_mono subsetI) auto 
   also have "... = measure (map_pmf ((\<circ>) (\<lambda>x. x \<in> {0,1})) (Pi_pmf I (if d then 0 else 2) q)) A"
     by (simp add:vimage_def comp_def)
   also have "... = measure (Pi_pmf I d (\<lambda>i. map_pmf (\<lambda>x. x \<in> {0,1}) (q i))) A"
     by (intro arg_cong2[where f="measure_pmf.prob"] Pi_pmf_map[OF assms(1), symmetric]) auto
   also have "... = ?R" 
     unfolding comp_def by (simp add:1 cong: Pi_pmf_cong)
   finally show ?thesis by simp
 qed
 
 lemma discrete_measure_eqI:
   assumes "sets M = count_space UNIV"
   assumes "sets N = count_space UNIV" 
   assumes "countable \<Omega>"
   assumes "\<And>x. x \<in> \<Omega> \<Longrightarrow> emeasure M {x} = emeasure N {x} \<and> emeasure M {x} \<noteq> \<infinity>"
   assumes "AE x in M. x \<in> \<Omega>"
   assumes "AE x in N. x \<in> \<Omega>"
   shows "M = N"
 proof -
   define E where "E = insert {} ((\<lambda>x. {x}) ` \<Omega>)"
 
   have 0: "Int_stable E" unfolding E_def by (intro Int_stableI) auto
   have 1: "countable E" using assms(3) unfolding E_def by simp
 
   have "E \<subseteq> Pow \<Omega>" unfolding E_def by auto
   have "emeasure M A = emeasure N A" if A_range: "A \<in> E" for A
     using that assms(4) unfolding E_def by auto
   moreover have "sets M = sets N" using assms(1,2) by simp
   moreover have "\<Omega> \<in> sets M" using assms(1) by simp
   moreover have "E \<noteq> {}" unfolding E_def by simp
   moreover have "\<Union>E = \<Omega>" unfolding E_def by simp
   moreover have "emeasure M a \<noteq> \<infinity>" if "a \<in> E" for a
     using that assms(4) unfolding E_def by auto
   moreover have "sets (restrict_space M \<Omega>) = Pow \<Omega>"
     using assms(1) by (simp add:sets_restrict_space range_inter)
   moreover have "sets (restrict_space N \<Omega>) = Pow \<Omega>"
     using assms(2) by (simp add:sets_restrict_space range_inter)
   moreover have "sigma_sets \<Omega> E = Pow \<Omega>"
     unfolding E_def by (intro sigma_sets_singletons_and_empty assms(3)) 
   ultimately show ?thesis
     by (intro measure_eqI_restrict_generator[OF 0 _ _ _ _ _ _ assms(5,6) 1]) auto
 qed
 
 text \<open>Main results of this section:\<close>
 
 text \<open>The next theorem establishes a bound for the probability of the median of independent random
 variables using the binomial distribution. In a follow-up step, we will establish tail bounds
 for the binomial distribution and corresponding median bounds.
 
 This two-step strategy was suggested by Yong Kiam Tan. In a previous version, I only had verified 
 the exponential tail bound (see theorem \verb+median_bound+ below).\<close>
 
 theorem (in prob_space) median_bound_raw:
   fixes I :: "('b :: {linorder_topology, second_countable_topology}) set"
   assumes "n > 0" "p \<ge> 0"
   assumes "interval I"
   assumes "indep_vars (\<lambda>_. borel) X {0..<n}"
   assumes "\<And>i. i < n \<Longrightarrow> \<P>(\<omega> in M. X i \<omega> \<in> I) \<ge> p" 
   shows "\<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> I) \<ge> 1 - measure (binomial_pmf n p) {..n div 2}" 
     (is "?L \<ge> ?R")
 proof -
   let ?pi = "Pi_pmf {..<n} undefined"
   define q where "q i = \<P>(\<omega> in M. X i \<omega> \<in> I)" for i
 
   have n_ge_1: "n \<ge> 1" using assms(1) by simp
 
   have 0: "{k. k < n \<and> (k < n \<longrightarrow> X k \<omega> \<in> I)} = {k. k < n \<and> X k \<omega> \<in> I}" for \<omega>
     by auto
 
   have "countable ({..<n} \<rightarrow>\<^sub>E (UNIV ::  bool set))"
     by (intro countable_PiE) auto
   hence countable_ext: "countable (extensional {..<n} :: (nat \<Rightarrow> bool) set)"
     unfolding PiE_def by auto
 
   have m0: "I \<in> sets borel"
     using interval_borel[OF assms(3)] by simp
 
   have m1: "random_variable borel (\<lambda>x. X k x)" if "k \<in> {..<n}" for k 
     using assms(4) that unfolding indep_vars_def by auto
 
   have m2: "(\<lambda>x. x \<in> I) \<in> borel \<rightarrow>\<^sub>M (measure_pmf ((bernoulli_pmf \<circ> q) k))"  
     for k using m0 by measurable
   hence m3: "random_variable (measure_pmf ((bernoulli_pmf \<circ> q) k)) (\<lambda>x. X k x \<in> I)"
     if "k \<in> {..<n}" for k 
     by (intro measurable_compose[OF m1] that)
 
   hence m4: "random_variable (PiM {..<n} (bernoulli_pmf \<circ> q)) (\<lambda>\<omega>. \<lambda>k\<in>{..<n}. X k \<omega> \<in> I)" 
     by (intro measurable_restrict) auto
   moreover have "A \<in> sets (Pi\<^sub>M {..<n} (\<lambda>x. measure_pmf (bernoulli_pmf (q x))))"
     if "A \<subseteq> extensional {..<n}" for A 
   proof -
     have "A = (\<Union>a \<in> A. {a})" by auto
     also have "... = (\<Union>a \<in> A. PiE {..<n} (\<lambda>k. {a k}))"
       using that by (intro arg_cong[where f="Union"] image_cong refl PiE_singleton[symmetric]) auto
     also have "... \<in> sets (Pi\<^sub>M {..<n} (\<lambda>x. measure_pmf (bernoulli_pmf (q x))))"
       using that countable_ext countable_subset
       by (intro sets.countable_Union countable_image image_subsetI sets_PiM_I_finite) auto
     finally show ?thesis by simp
   qed
   hence m5: "id \<in> (PiM {..<n} (bernoulli_pmf \<circ> q)) \<rightarrow>\<^sub>M (count_space UNIV)"
     by (intro measurableI) (simp_all add:vimage_def space_PiM PiE_def)
   ultimately have "random_variable (count_space UNIV) (id \<circ> (\<lambda>\<omega>. \<lambda>k\<in>{..<n}. X k \<omega> \<in> I))"
     by (rule measurable_comp)
   hence m6: "random_variable (count_space UNIV) (\<lambda>\<omega>. \<lambda>k\<in>{..<n}. X k \<omega> \<in> I)" by simp
 
   have indep: "indep_vars (bernoulli_pmf \<circ> q) (\<lambda>i x. X i x \<in> I) {0..<n}" 
     by (intro indep_vars_compose2[OF assms(4)] m2)
 
   have "measure M {x \<in> space M. (X k x \<in> I) = \<omega>} = measure (bernoulli_pmf (q k)) {\<omega>}"
     if "k < n" for \<omega> k
   proof (cases "\<omega>")
     case True
     then show ?thesis unfolding q_def  by (simp add:measure_pmf_single)
   next
     case False
     have "{x \<in> space M. X k x \<in> I} \<in> events"
       using that m0 by (intro measurable_sets_Collect[OF m1]) auto
     hence "prob {x \<in> space M. X k x \<notin> I} = 1 - prob {\<omega> \<in> space M. X k \<omega> \<in> I}" 
       by (subst prob_neg) auto
     thus ?thesis using False unfolding q_def by (simp add:measure_pmf_single)
   qed
 
   hence 1: "emeasure M {x \<in> space M. (X k x \<in> I) = \<omega>} = emeasure (bernoulli_pmf (q k)) {\<omega>}"
     if "k < n" for \<omega> k
     using that unfolding emeasure_eq_measure measure_pmf.emeasure_eq_measure by simp
 
   interpret product_sigma_finite "(bernoulli_pmf \<circ> q)"
     by standard
 
   have "distr M (count_space UNIV) (\<lambda>\<omega>. (\<lambda>k\<in>{..<n} . X k \<omega> \<in> I)) = distr 
     (distr M (PiM {..<n} (bernoulli_pmf \<circ> q)) (\<lambda>\<omega>. \<lambda>k\<in>{..<n}. X k \<omega> \<in> I)) (count_space UNIV) id"
     by (subst distr_distr[OF m5 m4]) (simp add:comp_def) 
   also have "... = distr (PiM {..<n} (\<lambda>i. (distr M ((bernoulli_pmf \<circ> q) i) (\<lambda>\<omega>. X i \<omega> \<in> I) )))
     (count_space UNIV) id" 
     using assms(1) indep atLeast0LessThan by (intro arg_cong2[where f="\<lambda>x y. distr x y id"] 
         iffD1[OF indep_vars_iff_distr_eq_PiM'] m3) auto 
   also have "... = distr (PiM {..<n} (bernoulli_pmf \<circ> q)) (count_space UNIV) id"
     using m3 1 by (intro distr_cong PiM_cong refl discrete_measure_eqI[where \<Omega>="UNIV"])
         (simp_all add:emeasure_distr vimage_def Int_def conj_commute)
   also have "... = ?pi (bernoulli_pmf \<circ> q)"
   proof (rule discrete_measure_eqI[where \<Omega>="extensional {..<n}"], goal_cases)
     case 1 show ?case by simp
   next
     case 2 show ?case by simp
   next
     case 3 show ?case using countable_ext by simp
   next
     case (4 x)
     have "emeasure (Pi\<^sub>M {..<n} (bernoulli_pmf \<circ> q)) {x} = 
       emeasure (Pi\<^sub>M {..<n} (bernoulli_pmf \<circ> q)) (PiE {..<n} (\<lambda>k. {x k}))"
       using PiE_singleton[OF 4] by simp
     also have "... = (\<Prod>i<n. emeasure (measure_pmf (bernoulli_pmf (q i))) {x i})"
       by (subst emeasure_PiM) auto
     also have "... = emeasure (Pi_pmf {..<n} undefined (bernoulli_pmf\<circ>q)) 
       (PiE_dflt {..<n} undefined (\<lambda>k. {x k}))"
       unfolding measure_pmf.emeasure_eq_measure
       by (subst measure_Pi_pmf_PiE_dflt) (simp_all add:prod_ennreal)
     also have "... = emeasure (Pi_pmf {..<n} undefined (bernoulli_pmf\<circ>q)) {x}"
       using 4 by (intro arg_cong2[where f="emeasure"]) (auto simp add:PiE_dflt_def extensional_def)
     finally have "emeasure (Pi\<^sub>M {..<n} (bernoulli_pmf \<circ> q)) {x} = 
       emeasure (Pi_pmf {..<n} undefined (bernoulli_pmf \<circ> q)) {x}"
       by simp
     thus ?case using 4 
       by (subst (1 2) emeasure_distr[OF m5]) (simp_all add:vimage_def space_PiM PiE_def)
   next
     case 5
     have "AE x in Pi\<^sub>M {..<n} (bernoulli_pmf \<circ> q). x \<in> extensional {..<n}"
       by (intro AE_I2) (simp add:space_PiM PiE_def)
     then show ?case by (subst AE_distr_iff[OF m5]) simp_all
   next
     case 6
     then show ?case by (intro AE_pmfI) (simp add: set_Pi_pmf PiE_dflt_def extensional_def)
   qed
   finally have 2: "distr M (count_space UNIV) (\<lambda>\<omega>. (\<lambda>k\<in>{..<n}. X k \<omega> \<in> I)) = ?pi (bernoulli_pmf\<circ>q)"
     by simp
 
   have 3: "n < 2 * card {k. k < n \<and> y k}" if 
     "n < 2 * card {k. k < n \<and> x k}" "\<And>i. i < n \<Longrightarrow> x i \<Longrightarrow> y i" for x y
   proof -
     have "2 * card {k. k < n \<and> x k} \<le> 2 * card {k. k < n \<and> y k}"
       using that(2) by (intro mult_left_mono card_mono) auto
     thus ?thesis using that(1) by simp
   qed
 
   have 4: "0 \<le> p \<and> p \<le> q i \<and> q i \<le> 1" if "i < n" for i
     unfolding q_def using assms(2,5) that by auto
 
   have p_range: "p \<in> {0..1}"
     using 4[OF assms(1)] by auto
 
   have "?R = 1 - measure_pmf.prob (binomial_pmf n p) {k. 2 * k \<le> n}"
     by (intro arg_cong2[where f="(-)"] arg_cong2[where f="measure_pmf.prob"]) auto
   also have "... = measure (binomial_pmf n p) {k. n < 2 * k}"
     by (subst measure_pmf.prob_compl[symmetric]) (simp_all add:set_diff_eq not_le)
   also have "... = measure (?pi (bernoulli_pmf \<circ> (\<lambda>_. p))) {\<omega>. n < 2 * card {k. k < n \<and> \<omega> k}}"
     using p_range by (subst binomial_pmf_altdef'[where A="{..<n}" and dflt="undefined"]) auto
   also have "... \<le> measure (?pi (bernoulli_pmf \<circ> q)) {\<omega>. n < 2 * card {k. k < n \<and> \<omega> k}}"
     using 3 4 by (intro prod_pmf_bernoulli_mono) auto
   also have "... = 
     \<P>(\<omega> in distr M (count_space UNIV) (\<lambda>\<omega>. \<lambda>k\<in>{..<n}. X k \<omega> \<in> I). n<2*card {k. k < n \<and> \<omega> k})"
     unfolding 2 by simp
   also have "... = \<P>(\<omega> in M. n < 2*card {k. k < n \<and> X k \<omega> \<in> I})" 
     by (subst measure_distr[OF m6]) (simp_all add:vimage_def Int_def conj_commute 0)
   also have "... \<le> ?L"
     using median_est[OF assms(3)] m0 m1
     by (intro finite_measure_mono measurable_sets_Collect[OF median_measurable[OF n_ge_1]]) auto 
   finally show "?R \<le> ?L" by simp
 qed
 
 text \<open>Cumulative distribution of the binomial distribution (contributed by Yong Kiam Tan):\<close>
 
 lemma prob_binomial_pmf_upto:
   assumes "0 \<le> p" "p \<le> 1"
   shows "measure_pmf.prob (binomial_pmf n p) {..m} =
     sum (\<lambda>i. real (n choose i) * p^i * (1 - p) ^(n-i)) {0..m}"
   by (auto simp: pmf_binomial[OF assms] measure_measure_pmf_finite intro!: sum.cong)
 
 text \<open>A tail bound for the binomial distribution using Hoeffding's inequality:\<close>
 
 lemma binomial_pmf_tail:
   assumes "p \<in> {0..1}" "real k \<le> real n * p"
   shows "measure (binomial_pmf n p) {..k} \<le> exp (- 2 * real n * (p - real k / n)^2)" 
     (is "?L \<le> ?R")
 proof (cases "n = 0")
   case True then show ?thesis by simp
 next
   case False
   let ?A = "{..<n}"
   let ?pi = "Pi_pmf ?A undefined (\<lambda>_. bernoulli_pmf p)"
 
   define \<mu> where "\<mu> = (\<Sum>i<n. (\<integral>x. (of_bool (x i) :: real) \<partial> ?pi))"
   define \<epsilon> :: real where "\<epsilon> = \<mu> - k" (* eps \<ge> 0 <-> k \<le> mu *)
 
   have "\<mu> = (\<Sum>i<n. (\<integral>x. (of_bool x :: real) \<partial> (map_pmf (\<lambda>\<omega>. \<omega> i) ?pi)))"
     unfolding \<mu>_def by simp
   also have "... = (\<Sum>i<n. (\<integral>x. (of_bool x :: real) \<partial> (bernoulli_pmf p)))"
     by (simp add: Pi_pmf_component)
   also have "... = real n * p" using assms(1) by simp
   finally have \<mu>_alt: "\<mu> = real n * p"
     by simp
 
   have \<epsilon>_ge_0: "\<epsilon> \<ge> 0"
     using assms(2) unfolding \<epsilon>_def \<mu>_alt by auto
 
   have indep: "prob_space.indep_vars ?pi (\<lambda>_. borel) (\<lambda>k \<omega>. of_bool (\<omega> k)) {..<n}"
     by (intro prob_space.indep_vars_compose2[OF prob_space_measure_pmf indep_vars_Pi_pmf]) auto
   interpret Hoeffding_ineq "?pi" "{..<n}" "\<lambda>k \<omega>. of_bool (\<omega> k)" "\<lambda>_.0" "\<lambda>_.1" \<mu>
     using indep unfolding \<mu>_def by (unfold_locales) simp_all  
   
   have "?L = measure (map_pmf (\<lambda>f. card {x \<in> ?A. f x}) ?pi) {..k}"
     by (intro arg_cong2[where f="measure_pmf.prob"] binomial_pmf_altdef' assms(1)) auto
   also have "... = \<P>(\<omega> in ?pi. (\<Sum>i<n. of_bool (\<omega> i)) \<le> \<mu> - \<epsilon>)"
     unfolding \<epsilon>_def by (simp add:vimage_def Int_def)
   also have "... \<le> exp (- 2 * \<epsilon>\<^sup>2 / (\<Sum>i<n. (1 - 0)\<^sup>2))"
     using False by (intro Hoeffding_ineq_le \<epsilon>_ge_0) auto
   also have "... = ?R"
     unfolding \<epsilon>_def \<mu>_alt by (simp add:power2_eq_square field_simps) 
   finally show ?thesis by simp
 qed
 
 theorem (in prob_space) median_bound:
   fixes n :: nat
   fixes I :: "('b :: {linorder_topology, second_countable_topology}) set"
   assumes "interval I"
   assumes "\<alpha> > 0"
   assumes "\<epsilon> \<in> {0<..<1}"
   assumes "indep_vars (\<lambda>_. borel) X {0..<n}"
   assumes "n \<ge> - ln \<epsilon> / (2 * \<alpha>\<^sup>2)"
   assumes "\<And>i. i < n \<Longrightarrow> \<P>(\<omega> in M. X i \<omega> \<in> I) \<ge> 1/2+\<alpha>" 
   shows "\<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> I) \<ge> 1-\<epsilon>"
 proof -
   have "0 < -ln \<epsilon> / (2 * \<alpha>\<^sup>2)"  
     using assms by (intro divide_pos_pos) auto
   also have "... \<le> real n" using assms by simp
   finally have "real n > 0" by simp
   hence n_ge_0:"n > 0" by simp
 
   have d0: "real_of_int \<lfloor>real n / 2\<rfloor> * 2 / real n \<le> 1"
     using n_ge_0 by simp linarith
 
   hence d1: "real (nat \<lfloor>real n / 2\<rfloor>) \<le> real n * (1 / 2)"
     using n_ge_0 by (simp add:field_simps)
   also have "... \<le> real n * (1 / 2 + \<alpha>)"
     using assms(2) by (intro mult_left_mono) auto
   finally have d1: "real (nat \<lfloor>real n / 2\<rfloor>) \<le> real n * (1 / 2 + \<alpha>)" by simp
 
   have "1/2 + \<alpha> \<le> \<P>(\<omega> in M. X 0 \<omega> \<in> I)" using n_ge_0 by (intro assms(6))
   also have "... \<le> 1" by simp
   finally have d2: "1 / 2 + \<alpha> \<le> 1" by simp
 
   have d3: "nat \<lfloor>real n / 2\<rfloor> = n div 2" by linarith
 
   have "1 - \<epsilon> \<le> 1 - exp (- 2 * real n * \<alpha>\<^sup>2)" 
     using assms(2,3,5) by (intro diff_mono order.refl iffD1[OF ln_ge_iff]) (auto simp:field_simps)
   also have "... \<le> 1 - exp (- 2 * real n * ((1/2+\<alpha>) - real (nat \<lfloor>real n/2\<rfloor>) / real n)\<^sup>2)"
     using d0 n_ge_0 assms(2)
     by (intro diff_mono order.refl iffD2[OF exp_le_cancel_iff] mult_left_mono_neg power_mono) auto 
   also have "... \<le> 1 - measure (binomial_pmf n (1/2+\<alpha>)) {..nat \<lfloor>real n/2\<rfloor>}"
     using assms(2) d1 d2 by (intro diff_mono order.refl binomial_pmf_tail) auto
   also have "... = 1 - measure (binomial_pmf n (1/2+\<alpha>)) {..n div 2}" by (simp add:d3)
   also have "... \<le> \<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> I)"
     using assms(2) by (intro median_bound_raw n_ge_0 assms(1,4,6) add_nonneg_nonneg) auto
   finally show ?thesis by simp
 qed
 
 text \<open>This is a specialization of the above to closed real intervals.\<close>
 
 corollary (in prob_space) median_bound_1:
   assumes "\<alpha> > 0"
   assumes "\<epsilon> \<in> {0<..<1}"
   assumes "indep_vars (\<lambda>_. borel) X {0..<n}"
   assumes "n \<ge> - ln \<epsilon> / (2 * \<alpha>\<^sup>2)"
   assumes "\<forall>i \<in> {0..<n}. \<P>(\<omega> in M. X i \<omega> \<in> ({a..b} :: real set)) \<ge> 1/2+\<alpha>" 
   shows "\<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> {a..b}) \<ge> 1-\<epsilon>" 
   using assms(5) by (intro median_bound[OF _ assms(1,2,3,4)]) (auto simp:interval_def)
 
 text \<open>This is a specialization of the above, where $\alpha = \frac{1}{6}$ and the interval is 
 described using a mid point @{term "\<mu>"} and radius @{term "\<delta>"}. The choice of 
 $\alpha = \frac{1}{6}$ implies a success probability per random variable of $\frac{2}{3}$. It is a 
 commonly chosen success probability for Monte-Carlo algorithms 
 (cf. \<^cite>\<open>\<open>\textsection 4\<close> in "baryossef2002"\<close> or \<^cite>\<open>\<open>\textsection 1\<close> in "kane2010"\<close>).\<close>
 
 corollary (in prob_space) median_bound_2:
   fixes \<mu> \<delta> :: real
   assumes "\<epsilon> \<in> {0<..<1}"
   assumes "indep_vars (\<lambda>_. borel) X {0..<n}"
   assumes "n \<ge> -18 * ln \<epsilon>"
   assumes "\<And>i. i < n \<Longrightarrow> \<P>(\<omega> in M. abs (X i \<omega> - \<mu>) > \<delta>) \<le> 1/3" 
   shows "\<P>(\<omega> in M. abs (median n (\<lambda>i. X i \<omega>) - \<mu>) \<le> \<delta>) \<ge> 1-\<epsilon>"
 proof -
-  have b:"\<And>i. i < n \<Longrightarrow> space M - {\<omega> \<in> space M. X i \<omega> \<in> {\<mu> - \<delta>..\<mu> + \<delta>}} =  {\<omega> \<in> space M. abs (X i \<omega> - \<mu>) > \<delta>}"
-    apply (rule order_antisym, rule subsetI, simp, linarith)
-    by (rule subsetI, simp, linarith)
+  have b:"space M - {\<omega> \<in> space M. X i \<omega> \<in> {\<mu>-\<delta>..\<mu>+\<delta>}} = {\<omega> \<in> space M. abs (X i \<omega> - \<mu>) > \<delta>}" for i
+    by auto
 
   have "\<And>i. i < n \<Longrightarrow> 1 - \<P>(\<omega> in M. X i \<omega> \<in> {\<mu>- \<delta>..\<mu>+\<delta>}) \<le> 1/3"
+    using assms
     apply (subst prob_compl[symmetric])
-     apply (measurable)
-     using assms(2) apply (simp add:indep_vars_def)
-    apply (subst b, simp)
-    using assms(4) by simp
+     apply (measurable, simp add:indep_vars_def)
+    by (subst b, simp)
 
   hence a:"\<And>i. i < n \<Longrightarrow> \<P>(\<omega> in M. X i \<omega> \<in> {\<mu>- \<delta>..\<mu>+\<delta>}) \<ge> 2/3" by simp
   
-  have "1-\<epsilon> \<le> \<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> {\<mu>-\<delta>..\<mu>+\<delta>})"
-    apply (rule median_bound_1[OF _ assms(1) assms(2), where \<alpha>="1/6"], simp) 
-     using assms(3) apply (simp add:power2_eq_square)
-    using a by simp
+  have "1-\<epsilon> \<le> \<P>(\<omega> in M. median n (\<lambda>i. X i \<omega>) \<in> {\<mu>-\<delta>..\<mu>+\<delta>})" using a assms(3)
+    by (intro median_bound_1[OF _ assms(1,2), where \<alpha>="1/6"]) (simp_all add:power2_eq_square)
   also have "... = \<P>(\<omega> in M. abs (median n (\<lambda>i. X i \<omega>) - \<mu>) \<le> \<delta>)"
-    apply (rule arg_cong2[where f="measure"], simp)
-    apply (rule order_antisym, rule subsetI, simp, linarith)
-    by (rule subsetI, simp, linarith)
+    by (intro arg_cong2[where f="measure"] Collect_cong) auto
   finally show ?thesis by simp
 qed
 
 section \<open>Some additional results about the median\<close>
 
 lemma sorted_mono_map: 
   assumes "sorted xs"
   assumes "mono f"
   shows "sorted (map f xs)"
-  using assms apply (simp add:sorted_wrt_map)
-  apply (rule sorted_wrt_mono_rel[where P="(\<le>)"])
-  by (simp add:mono_def, simp)
+  using assms(2) unfolding sorted_wrt_map
+  by (intro sorted_wrt_mono_rel[OF _ assms(1)]) (simp add:mono_def)
 
 text \<open>This could be added to @{theory "HOL.List"}:\<close>
 lemma map_sort:
   assumes "mono f"
   shows "sort (map f xs) = map f (sort xs)"
   using assms by (intro properties_for_sort sorted_mono_map) auto
 
 lemma median_cong:
   assumes "\<And>i. i < n \<Longrightarrow> f i = g i"
   shows "median n f = median n g"
-  apply (cases "n = 0", simp add:median_def)
-  apply (simp add:median_def)
-  apply (rule arg_cong2[where f="(!)"])
-   apply (rule arg_cong[where f="sort"], rule map_cong, simp, simp add:assms)
-  by simp
+  unfolding median_def using assms
+  by (intro arg_cong2[where f="(!)"] arg_cong[where f="sort"] map_cong) auto
 
 lemma median_restrict: 
   "median n (\<lambda>i \<in> {0..<n}.f i) = median n f"
   by (rule median_cong, simp)
 
 lemma median_commute_mono:
   assumes "n > 0"
   assumes "mono g"
   shows "g (median n f) = median n (g \<circ> f)"
   apply (simp add: median_def del:map_map)
   apply (subst map_map[symmetric])
   apply (subst map_sort[OF assms(2)])
   apply (subst nth_map, simp) using assms apply fastforce
   by simp
 
 lemma median_rat:
   assumes "n > 0"
   shows "real_of_rat (median n f) = median n (\<lambda>i. real_of_rat (f i))"
   apply (subst (2) comp_def[where g="f", symmetric])
   apply (rule median_commute_mono[OF assms(1)])
   by (simp add: mono_def of_rat_less_eq)
 
 lemma median_const:
   assumes "k > 0"
   shows "median k (\<lambda>i \<in> {0..<k}. a) = a"
 proof -
   have b: "sorted (map (\<lambda>_. a) [0..<k])" 
     by (subst sorted_wrt_map, simp)
   have a: "sort (map (\<lambda>_. a) [0..<k]) = map (\<lambda>_. a) [0..<k]"
     by (subst sorted_sort_id[OF b], simp)
   have "median k (\<lambda>i \<in> {0..<k}. a) = median k (\<lambda>_. a)"
     by (subst median_restrict, simp)
   also have "... = a" using assms by (simp add:median_def a)
   finally show ?thesis by simp
 qed
 
 end