diff --git a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Preliminary.thy b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Preliminary.thy
--- a/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Preliminary.thy
+++ b/thys/Distributed_Distinct_Elements/Distributed_Distinct_Elements_Preliminary.thy
@@ -1,336 +1,326 @@
 section \<open>Preliminary Results\<close>
 
 text \<open>This section contains various short preliminary results used in the sections below.\<close>
 
 theory Distributed_Distinct_Elements_Preliminary
   imports
     Frequency_Moments.Frequency_Moments_Preliminary_Results
     Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
     Median_Method.Median
     Expander_Graphs.Extra_Congruence_Method
     Expander_Graphs.Constructive_Chernoff_Bound
     Frequency_Moments.Landau_Ext
     Stirling_Formula.Stirling_Formula
 begin
 
 unbundle intro_cong_syntax
 
 text \<open>The following aliases are here to prevent possible merge-conflicts. The lemmas have been moved
 to @{theory "Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF"}.\<close>
 
 lemmas measure_pmf_cong = measure_pmf_cong
 lemmas pmf_mono = pmf_mono
+lemmas pmf_add = pmf_add
 
 lemma pmf_rev_mono:
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<notin> Q \<Longrightarrow> x \<notin> P"
   shows "measure p P \<le> measure p Q"
   using assms by (intro pmf_mono) blast
 
 lemma pmf_exp_mono:
   fixes f g :: "'a \<Rightarrow> real"
   assumes "integrable (measure_pmf p) f" "integrable (measure_pmf p) g"
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> f x \<le> g x"
   shows "integral\<^sup>L (measure_pmf p) f \<le> integral\<^sup>L (measure_pmf p) g"
   using assms  by (intro integral_mono_AE AE_pmfI) auto
 
 lemma pmf_markov:
   assumes "integrable (measure_pmf p) f" "c > 0"
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> f x \<ge> 0"
   shows "measure p {\<omega>. f \<omega> \<ge> c} \<le> (\<integral>\<omega>. f \<omega> \<partial>p)/ c" (is "?L \<le> ?R")
 proof -
   have a:"AE \<omega> in (measure_pmf p). 0 \<le> f \<omega>"
     by (intro AE_pmfI assms(3))
   have b:"{} \<in> measure_pmf.events p"
     unfolding assms(1) by simp
 
   have "?L = \<P>(\<omega> in (measure_pmf p). f \<omega> \<ge> c)"
     using assms(1) by simp
   also have "... \<le>  ?R"
     by (intro  integral_Markov_inequality_measure[OF _ b] assms a)
   finally show ?thesis by simp
 qed
 
-lemma pmf_add:
-  assumes  "\<And>x. x \<in> P \<Longrightarrow> x \<in> set_pmf p \<Longrightarrow> x \<in> Q \<or> x \<in> R"
-  shows "measure p P \<le> measure p Q + measure p R"
-proof -
-  have "measure p P \<le> measure p (Q \<union> R)"
-    using assms by (intro pmf_mono) blast
-  also have "... \<le> measure p Q + measure p R"
-    by (rule measure_subadditive, auto)
-  finally show ?thesis by simp
-qed
-
 lemma pair_pmf_prob_left:
   "measure_pmf.prob (pair_pmf A B) {\<omega>. P (fst \<omega>)} = measure_pmf.prob A {\<omega>. P \<omega>}" (is "?L = ?R")
 proof -
   have "?L = measure_pmf.prob (map_pmf fst (pair_pmf A B)) {\<omega>. P \<omega>}"
     by (subst measure_map_pmf) simp
   also have "... = ?R"
     by (subst map_fst_pair_pmf) simp
   finally show ?thesis by simp
 qed
 
 lemma pmf_exp_of_fin_function:
   assumes "finite A" "g ` set_pmf p \<subseteq> A"
   shows "(\<integral>\<omega>. f (g \<omega>) \<partial>p) = (\<Sum>y \<in> A. f y * measure p {\<omega>. g \<omega> = y})"
     (is "?L = ?R")
 proof -
   have "?L = integral\<^sup>L (map_pmf g p) f"
     using integral_map_pmf assms by simp
   also have "... = (\<Sum>a\<in>A. f a * pmf (map_pmf g p) a)"
     using assms
     by (intro integral_measure_pmf_real) auto
   also have " ... = (\<Sum>y \<in> A. f y * measure p (g -` {y}))"
     unfolding assms(1) by (intro_cong "[\<sigma>\<^sub>2 (*)]" more:sum.cong pmf_map)
   also have "... = ?R"
     by (intro sum.cong) (auto simp add: vimage_def)
   finally show ?thesis by simp
 qed
 
 text \<open>Cardinality rules for distinct/ordered pairs of a set without the finiteness constraint - to
 use in simplification:\<close>
 
 lemma card_distinct_pairs:
   "card {x \<in> B \<times> B. fst x \<noteq> snd x} = card B^2 - card B" (is "card ?L = ?R")
 proof (cases "finite B")
   case True
   include intro_cong_syntax
   have "card ?L = card (B \<times> B - (\<lambda>x. (x,x)) ` B)"
     by (intro arg_cong[where f="card"]) auto
   also have "... = card (B \<times> B) - card ((\<lambda>x. (x,x)) ` B)"
     by (intro card_Diff_subset finite_imageI True image_subsetI) auto
   also have "... = ?R"
     using True by (intro_cong "[\<sigma>\<^sub>2 (-)]" more: card_image)
       (auto simp add:power2_eq_square inj_on_def)
   finally show ?thesis by simp
 next
   case False
   then obtain p where p_in: "p \<in> B" by fastforce
   have "False" if "finite ?L"
   proof -
     have "(\<lambda>x. (p,x)) ` (B - {p}) \<subseteq> ?L"
       using p_in by (intro image_subsetI) auto
     hence "finite ((\<lambda>x. (p,x)) ` (B - {p}))"
       using finite_subset that by auto
     hence "finite (B - {p})"
       by (rule finite_imageD) (simp add:inj_on_def)
     hence "finite B"
       by simp
     thus "False" using False by simp
   qed
   hence "infinite ?L" by auto
   hence "card ?L = 0" by simp
   also have "... = ?R"
     using False by simp
   finally show ?thesis by simp
 qed
 
 lemma card_ordered_pairs':
   fixes M :: "('a ::linorder) set"
   shows "card {(x,y) \<in> M \<times> M. x < y} = card M * (card M - 1) / 2"
 proof (cases "finite M")
   case True
   show ?thesis using card_ordered_pairs[OF True] by linarith
 next
   case False
   then obtain p where p_in: "p \<in> M" by fastforce
   let ?f= "(\<lambda>x. if x < p then (x,p) else (p,x))"
   have "False" if "finite {(x,y) \<in> M \<times> M. x < y}" (is "finite ?X")
   proof -
     have "?f ` (M-{p}) \<subseteq> ?X"
       using p_in by (intro image_subsetI) auto
     hence "finite (?f ` (M-{p}))" using that finite_subset by auto
     moreover have "inj_on ?f (M-{p})"
       by (intro inj_onI) (metis Pair_inject)
     ultimately have "finite (M - {p})"
       using finite_imageD by blast
     hence "finite M"
       using finite_insert[where a="p" and A="M-{p}"] by simp
     thus "False" using False by simp
   qed
   hence "infinite ?X" by auto
   then show ?thesis using False by simp
 qed
 
 text \<open>The following are versions of the mean value theorem, where the interval endpoints may be
 reversed.\<close>
 
 lemma MVT_symmetric:
   assumes "\<And>x. \<lbrakk>min a b \<le> x; x \<le> max a b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x"
   shows "\<exists>z::real. min a b \<le> z \<and> z \<le> max a b \<and> (f b - f a = (b - a) * f' z)"
 proof -
   consider (a) "a < b" | (b) "a = b" | (c) "a > b"
     by argo
   then show ?thesis
   proof (cases)
     case a
     then obtain z :: real where r: "a < z" "z < b" "f b - f a = (b - a) * f' z"
       using assms MVT2[where a="a" and b="b" and f="f" and f'="f'"] by auto
     have "a \<le> z" "z \<le> b" using r(1,2) by auto
     thus ?thesis using a r(3) by auto
   next
     case b
     then show ?thesis by auto
   next
     case c
     then obtain z :: real where r: "b < z" "z < a" "f a - f b = (a - b) * f' z"
       using assms MVT2[where a="b" and b="a" and f="f" and f'="f'"] by auto
     have "f b - f a = (b-a) * f' z" using r by argo
     moreover have "b \<le> z" "z \<le> a" using r(1,2) by auto
     ultimately show ?thesis using c by auto
   qed
 qed
 
 lemma MVT_interval:
   fixes I :: "real set"
   assumes "interval I" "a \<in> I" "b \<in> I"
   assumes "\<And>x. x \<in> I \<Longrightarrow> DERIV f x :> f' x"
   shows "\<exists>z. z \<in> I \<and> (f b - f a = (b - a) * f' z)"
 proof -
   have a:"min a b \<in> I"
     using assms(2,3) by (cases "a < b") auto
   have b:"max a b \<in> I"
     using assms(2,3) by (cases "a < b") auto
   have c:"x \<in> {min a b..max a b} \<Longrightarrow> x \<in> I" for x
     using interval_def assms(1) a b by auto
   have "\<lbrakk>min a b \<le> x; x \<le> max a b\<rbrakk> \<Longrightarrow> DERIV f x :> f' x" for x
     using c assms(4) by auto
   then obtain z where z:"z \<ge> min a b" "z \<le> max a b" "f b - f a = (b-a) * f' z"
     using MVT_symmetric by blast
   have "z \<in> I"
     using c z(1,2) by auto
   thus ?thesis using z(3) by auto
 qed
 
 text \<open>Ln is monotone on the positive numbers and thus commutes with min and max:\<close>
 lemma ln_min_swap:
   "x > (0::real) \<Longrightarrow> (y > 0) \<Longrightarrow> ln (min x y) = min (ln x) (ln y)"
   using ln_less_cancel_iff by fastforce
 
 lemma ln_max_swap:
   "x > (0::real) \<Longrightarrow> (y > 0) \<Longrightarrow> ln (max x y) = max (ln x) (ln y)"
   using ln_le_cancel_iff by fastforce
 
 text \<open>Loose lower bounds for the factorial fuction:.\<close>
 
 lemma fact_lower_bound:
   "sqrt(2*pi*n)*(n/exp(1))^n \<le> fact n" (is "?L \<le> ?R")
 proof (cases "n > 0")
   case True
   have "ln ?L = ln (2*pi*n)/2 + n * ln n - n"
     using True by (simp add: ln_mult ln_sqrt ln_realpow ln_div algebra_simps)
   also have "... \<le> ln ?R"
     by (intro Stirling_Formula.ln_fact_bounds True)
   finally show ?thesis
     using iffD1[OF ln_le_cancel_iff] True by simp
 next
   case False
   then show ?thesis by simp
 qed
 
 lemma fact_lower_bound_1:
   assumes "n > 0"
   shows "(n/exp 1)^n \<le> fact n" (is "?L \<le> ?R")
 proof -
   have "2 * pi \<ge> 1" using pi_ge_two by auto
   moreover have "n \<ge> 1" using assms by simp
   ultimately have "2 * pi * n \<ge> 1*1"
     by (intro mult_mono) auto
   hence a:"2 * pi * n \<ge> 1" by simp
 
   have "?L = 1 * ?L" by simp
   also have "... \<le> sqrt(2 * pi * n) * ?L"
     using a by (intro mult_right_mono) auto
   also have "... \<le> ?R"
     using fact_lower_bound by simp
   finally show ?thesis by simp
 qed
 
 text \<open>Rules to handle O-notation with multiple variables, where some filters may be towards zero:\<close>
 
 lemma real_inv_at_right_0_inf:
   "\<forall>\<^sub>F x in at_right (0::real). c \<le> 1 / x"
 proof -
   have "c \<le> 1 /  x" if b:" x \<in> {0<..<1 / (max c 1)}" for x
   proof -
     have "c * x \<le> (max c 1) * x"
       using b by (intro mult_right_mono, linarith, auto)
     also have "... \<le> (max c 1)  * (1 / (max c 1))"
       using b by (intro mult_left_mono) auto
     also have "... \<le> 1"
       by (simp add:of_rat_divide)
     finally have "c * x \<le> 1" by simp
     moreover have "0 < x"
       using b by simp
     ultimately show ?thesis by (subst pos_le_divide_eq, auto)
   qed
   thus ?thesis
     by (intro eventually_at_rightI[where b="1/(max c 1)"], simp_all)
 qed
 
 lemma bigo_prod_1:
   assumes "(\<lambda>x. f x) \<in> O[F](\<lambda>x. g x)" "G \<noteq> bot"
   shows "(\<lambda>x. f (fst x)) \<in> O[F \<times>\<^sub>F G](\<lambda>x. g (fst x))"
 proof -
   obtain c where a: "\<forall>\<^sub>F x in F. norm (f x) \<le> c * norm (g x)" and c_gt_0: "c > 0"
     using assms unfolding bigo_def by auto
 
   have "\<exists>c>0. \<forall>\<^sub>F x in F \<times>\<^sub>F G. norm (f (fst x)) \<le> c * norm (g (fst x))"
     by (intro exI[where x="c"] conjI c_gt_0  eventually_prod1' a assms(2))
   thus ?thesis
     unfolding bigo_def by simp
 qed
 
 lemma bigo_prod_2:
   assumes "(\<lambda>x. f x) \<in> O[G](\<lambda>x. g x)" "F \<noteq> bot"
   shows "(\<lambda>x. f (snd x)) \<in> O[F \<times>\<^sub>F G](\<lambda>x. g (snd x))"
 proof -
   obtain c where a: "\<forall>\<^sub>F x in G. norm (f x) \<le> c * norm (g x)" and c_gt_0: "c > 0"
     using assms unfolding bigo_def by auto
 
   have "\<exists>c>0. \<forall>\<^sub>F x in F \<times>\<^sub>F G. norm (f (snd x)) \<le> c * norm (g (snd x))"
     by (intro exI[where x="c"] conjI c_gt_0  eventually_prod2' a assms(2))
   thus ?thesis
     unfolding bigo_def by simp
 qed
 
 lemma eventually_inv:
   fixes P :: "real \<Rightarrow> bool"
   assumes "eventually (\<lambda>x. P (1/x)) at_top "
   shows "eventually (\<lambda>x. P x) (at_right 0)"
 proof -
   obtain N where c:"n \<ge> N \<Longrightarrow> P (1/n)" for n
     using assms unfolding eventually_at_top_linorder by auto
 
   define q where "q = max 1 N"
   have d: "0 < 1 / q" "q > 0"
     unfolding q_def by auto
 
   have "P x" if "x \<in> {0<..<1 / q}" for x
   proof -
     define n where "n = 1/x"
     have x_eq: "x = 1 / n"
       unfolding n_def using that by simp
 
     have "N \<le> q" unfolding q_def by simp
     also have "... \<le> n"
       unfolding n_def using that d by (simp add:divide_simps ac_simps)
     finally have "N \<le> n" by simp
     thus ?thesis
       unfolding x_eq by (intro c)
   qed
 
   thus ?thesis
     by (intro eventually_at_rightI[where b="1/q"] d)
 qed
 
 lemma bigo_inv:
   fixes f g :: "real \<Rightarrow> real"
   assumes "(\<lambda>x. f (1/x)) \<in> O(\<lambda>x. g (1/x))"
   shows "f \<in> O[at_right 0](g)"
   using assms eventually_inv unfolding bigo_def by auto
 
 unbundle no_intro_cong_syntax
 
 end
\ No newline at end of file
diff --git a/thys/Expander_Graphs/Constructive_Chernoff_Bound.thy b/thys/Expander_Graphs/Constructive_Chernoff_Bound.thy
--- a/thys/Expander_Graphs/Constructive_Chernoff_Bound.thy
+++ b/thys/Expander_Graphs/Constructive_Chernoff_Bound.thy
@@ -1,539 +1,548 @@
 subsection \<open>Constructive Chernoff Bound\label{sec:constructive_chernoff_bound}\<close>
 
 text \<open>This section formalizes Theorem~5 by Impagliazzo and Kabanets~\cite{impagliazzo2010}. It is
 a general result with which Chernoff-type tail bounds for various kinds of weakly dependent random
 variables can be obtained. The results here are general and will be applied in
 Section~\ref{sec:random_walks} to random walks in expander graphs.\<close>
 
 theory Constructive_Chernoff_Bound
   imports
     "HOL-Probability.Probability_Measure"
     Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
     Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
 begin
 
 lemma powr_mono_rev:
   fixes x :: real
   assumes "a \<le> b" and  "x > 0" "x \<le> 1"
   shows "x powr b \<le> x powr a"
 proof -
   have "x powr b = (1/x) powr (-b)"
     using assms by (simp add: powr_divide powr_minus_divide)
   also have "... \<le> (1/x) powr (-a)"
     using assms by (intro powr_mono) auto
   also have "... = x powr a"
     using assms by (simp add: powr_divide powr_minus_divide)
   finally show ?thesis by simp
 qed
 
 lemma exp_powr: "(exp x) powr y = exp (x*y)" for x :: real
   unfolding powr_def by simp
 
 lemma integrable_pmf_iff_bounded:
   fixes f :: "'a \<Rightarrow> real"
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> abs (f x) \<le> C"
   shows "integrable (measure_pmf p) f"
 proof -
   obtain x where "x \<in> set_pmf p"
     using set_pmf_not_empty by fast
   hence "C \<ge> 0" using assms(1) by fastforce
   hence " (\<integral>\<^sup>+ x. ennreal (abs (f x)) \<partial>measure_pmf p) \<le> (\<integral>\<^sup>+ x. C \<partial>measure_pmf p)"
     using assms ennreal_le_iff
     by (intro nn_integral_mono_AE AE_pmfI) auto
   also have "... = C"
     by simp
   also have "... < Orderings.top"
     by simp
   finally have "(\<integral>\<^sup>+ x. ennreal (abs (f x)) \<partial>measure_pmf p) < Orderings.top" by simp
   thus ?thesis
     by (intro iffD2[OF integrable_iff_bounded]) auto
 qed
 
 lemma split_pair_pmf:
   "measure_pmf.prob (pair_pmf A B) S = integral\<^sup>L A (\<lambda>a. measure_pmf.prob B {b. (a,b) \<in> S})"
   (is "?L = ?R")
 proof -
   have a:"integrable (measure_pmf A) (\<lambda>x. measure_pmf.prob B {b. (x, b) \<in> S})"
     by (intro integrable_pmf_iff_bounded[where C="1"]) simp
 
   have "?L = (\<integral>\<^sup>+x. indicator S x \<partial>(measure_pmf (pair_pmf A B)))"
     by (simp add: measure_pmf.emeasure_eq_measure)
   also have "... = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator S (x,y) \<partial>B) \<partial>A)"
     by (simp add: nn_integral_pair_pmf')
   also have "... = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator {b. (x,b) \<in> S} y \<partial>B) \<partial>A)"
     by (simp add:indicator_def)
   also have "... = (\<integral>\<^sup>+x. (measure_pmf.prob B {b. (x,b) \<in> S}) \<partial>A)"
     by (simp add: measure_pmf.emeasure_eq_measure)
   also have "... = ?R"
     using a
     by (subst nn_integral_eq_integral) auto
   finally show ?thesis by simp
 qed
 
 lemma split_pair_pmf_2:
   "measure(pair_pmf A B) S = integral\<^sup>L B (\<lambda>a. measure_pmf.prob A {b. (b,a) \<in> S})"
   (is "?L = ?R")
 proof -
   have "?L = measure (pair_pmf B A) {\<omega>. (snd \<omega>, fst \<omega>) \<in> S}"
     by (subst pair_commute_pmf) (simp add:vimage_def case_prod_beta)
   also have "... = ?R"
     unfolding split_pair_pmf by simp
   finally show ?thesis by simp
 qed
 
 definition KL_div :: "real \<Rightarrow> real \<Rightarrow> real"
   where "KL_div p q = p * ln (p/q) + (1-p) * ln ((1-p)/(1-q))"
 
 theorem impagliazzo_kabanets_pmf:
   fixes Y :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
   fixes p :: "'a pmf"
   assumes "n > 0"
   assumes "\<And>i. i \<in> {..<n} \<Longrightarrow> \<delta> i \<in> {0..1}"
   assumes "\<And>S. S \<subseteq> {..<n} \<Longrightarrow> measure p {\<omega>. (\<forall>i \<in> S. Y i \<omega>)} \<le> (\<Prod>i \<in> S. \<delta> i)"
   defines "\<delta>_avg \<equiv> (\<Sum>i\<in> {..<n}. \<delta> i)/n"
   assumes "\<gamma> \<in> {\<delta>_avg..1}"
   assumes "\<delta>_avg > 0"
   shows "measure p {\<omega>. real (card {i \<in> {..<n}. Y i \<omega>}) \<ge> \<gamma> * n} \<le> exp (-real n * KL_div \<gamma> \<delta>_avg)"
     (is "?L \<le> ?R")
 proof -
   let ?n = "real n"
   define q :: real where "q = (if \<gamma> = 1 then 1 else (\<gamma>-\<delta>_avg)/(\<gamma>*(1-\<delta>_avg)))"
 
   define g where "g \<omega> = card {i. i < n \<and> \<not>Y i \<omega>}" for \<omega>
   let ?E = "(\<lambda>\<omega>. real (card {i. i < n \<and> Y i \<omega>}) \<ge> \<gamma> * n)"
   let ?\<Xi> = "prod_pmf {..<n} (\<lambda>_. bernoulli_pmf q)"
 
   have q_range:"q \<in>{0..1}"
   proof (cases "\<gamma> < 1")
     case True
     then show ?thesis
       using assms(5,6)
       unfolding q_def by (auto intro!:divide_nonneg_pos simp add:algebra_simps)
   next
     case False
     hence "\<gamma> = 1" using assms(5) by simp
     then show ?thesis unfolding q_def by simp
   qed
 
   have abs_pos_le_1I: "abs x \<le> 1" if "x \<ge> 0" "x \<le> 1" for x :: real
     using that by auto
 
   have \<gamma>_n_nonneg: "\<gamma>*?n \<ge> 0"
     using assms(1,5,6) by simp
   define r where "r = n - nat \<lceil>\<gamma>*n\<rceil>"
 
   have 2:"(1-q) ^ r \<le> (1-q)^ g \<omega>" if "?E \<omega>" for \<omega>
   proof -
     have "g \<omega> = card ({i. i < n} - {i. i < n \<and> Y i \<omega>})"
       unfolding g_def by (intro arg_cong[where f="\<lambda>x. card x"]) auto
     also have "... = card {i. i < n} - card {i. i < n \<and> Y i \<omega>}"
       by (subst card_Diff_subset, auto)
     also have "... \<le> card {i. i < n} - nat \<lceil>\<gamma>*n\<rceil>"
       using that \<gamma>_n_nonneg by (intro diff_le_mono2) simp
     also have "... = r"
       unfolding r_def by simp
     finally have "g \<omega> \<le> r" by simp
     thus "(1-q) ^ r \<le> (1-q) ^ (g \<omega>)"
       using q_range by (intro power_decreasing) auto
   qed
 
   have \<gamma>_gt_0: "\<gamma> > 0"
     using assms(5,6) by simp
 
   have q_lt_1: "q < 1" if "\<gamma> < 1"
   proof -
     have "\<delta>_avg < 1" using assms(5) that by simp
     hence "(\<gamma> - \<delta>_avg) / (\<gamma> * (1 - \<delta>_avg)) < 1"
       using \<gamma>_gt_0 assms(6) that
       by (subst pos_divide_less_eq) (auto simp add:algebra_simps)
     thus "q < 1"
       unfolding q_def using that by simp
   qed
 
   have 5: "(\<delta>_avg * q + (1-q)) / (1-q) powr (1-\<gamma>) = exp (- KL_div \<gamma> \<delta>_avg)" (is "?L1 = ?R1")
     if "\<gamma> < 1"
   proof -
     have \<delta>_avg_range: "\<delta>_avg \<in> {0<..<1}"
       using that assms(5,6)  by simp
 
     have "?L1 = (1 - (1-\<delta>_avg) * q) / (1-q) powr (1-\<gamma>)"
       by (simp add:algebra_simps)
     also have "... = (1 - (\<gamma>-\<delta>_avg) / \<gamma> ) / (1-q) powr (1-\<gamma>)"
       unfolding q_def using that \<gamma>_gt_0 \<delta>_avg_range by simp
     also have "... = (\<delta>_avg / \<gamma>) / (1-q) powr (1-\<gamma>)"
       using \<gamma>_gt_0 by (simp add:divide_simps)
     also have "... = (\<delta>_avg / \<gamma>) * (1/(1-q)) powr (1-\<gamma>)"
       using q_lt_1[OF that] by (subst powr_divide, simp_all)
     also have "... = (\<delta>_avg / \<gamma>) * (1/((\<gamma>*(1-\<delta>_avg)-(\<gamma>-\<delta>_avg))/(\<gamma>*(1-\<delta>_avg)))) powr (1-\<gamma>)"
       using \<gamma>_gt_0 \<delta>_avg_range unfolding q_def by (simp add:divide_simps)
     also have "... = (\<delta>_avg / \<gamma>) * ((\<gamma> / \<delta>_avg) *((1-\<delta>_avg)/(1-\<gamma>))) powr (1-\<gamma>)"
       by (simp add:algebra_simps)
     also have "... = (\<delta>_avg / \<gamma>) * (\<gamma> / \<delta>_avg) powr (1-\<gamma>) *((1-\<delta>_avg)/(1-\<gamma>)) powr (1-\<gamma>)"
       using \<gamma>_gt_0  \<delta>_avg_range that by (subst powr_mult, auto)
     also have "... = (\<delta>_avg / \<gamma>) powr 1 * (\<delta>_avg / \<gamma>) powr -(1-\<gamma>) *((1-\<delta>_avg)/(1-\<gamma>)) powr (1-\<gamma>)"
       using \<gamma>_gt_0 \<delta>_avg_range that unfolding powr_minus_divide by (simp add:powr_divide)
     also have "... = (\<delta>_avg / \<gamma>) powr \<gamma> *((1-\<delta>_avg)/(1-\<gamma>)) powr (1-\<gamma>)"
       by (subst powr_add[symmetric]) simp
     also have "... = exp ( ln ((\<delta>_avg / \<gamma>) powr \<gamma> *((1-\<delta>_avg)/(1-\<gamma>)) powr (1-\<gamma>)))"
       using \<gamma>_gt_0 \<delta>_avg_range that by (intro exp_ln[symmetric] mult_pos_pos) auto
     also have "... =  exp ((ln ((\<delta>_avg / \<gamma>) powr \<gamma>) + ln (((1 - \<delta>_avg) / (1 - \<gamma>)) powr (1-\<gamma>))))"
       using \<gamma>_gt_0 \<delta>_avg_range that by (subst ln_mult) auto
     also have "... =  exp ((\<gamma> * ln (\<delta>_avg / \<gamma>) + (1 - \<gamma>) * ln ((1 - \<delta>_avg) / (1 - \<gamma>))))"
       using \<gamma>_gt_0 \<delta>_avg_range that by (simp add:ln_powr algebra_simps)
     also have "... =  exp (- (\<gamma> * ln (\<gamma> / \<delta>_avg) + (1 - \<gamma>) * ln ((1 - \<gamma>) / (1 - \<delta>_avg))))"
       using \<gamma>_gt_0 \<delta>_avg_range that by (simp add: ln_div algebra_simps)
     also have "... = ?R1"
       unfolding KL_div_def by simp
 
     finally show ?thesis by simp
   qed
 
   have 3: "(\<delta>_avg * q + (1-q)) ^ n / (1-q) ^ r \<le> exp (- ?n* KL_div \<gamma> \<delta>_avg)" (is "?L1 \<le> ?R1")
   proof (cases "\<gamma> < 1")
     case True
     have "\<gamma> * real n \<le> 1 * real n"
       using True by (intro mult_right_mono) auto
     hence "r = real n - real (nat \<lceil>\<gamma> * real n\<rceil>)"
       unfolding r_def by (subst of_nat_diff) auto
     also have "... = real n - \<lceil>\<gamma> * real n\<rceil>"
       using \<gamma>_n_nonneg by (subst of_nat_nat, auto)
     also have "... \<le> ?n - \<gamma> * ?n"
       by (intro diff_mono) auto
     also have "... = (1-\<gamma>) *?n" by (simp add:algebra_simps)
     finally have r_bound: "r \<le> (1-\<gamma>)*n" by simp
 
     have "?L1 = (\<delta>_avg * q + (1-q)) ^ n / (1-q) powr r"
       using q_lt_1[OF True] assms(1) by (simp add: powr_realpow)
     also have "... = (\<delta>_avg * q + (1-q)) powr n / (1-q) powr r"
       using q_lt_1[OF True] assms(6) q_range
       by (subst powr_realpow[symmetric], auto intro!:add_nonneg_pos)
     also have "... \<le> (\<delta>_avg * q + (1-q)) powr n / (1-q) powr ((1-\<gamma>)*n)"
       using q_range q_lt_1[OF True] by (intro divide_left_mono powr_mono_rev r_bound) auto
     also have "... = (\<delta>_avg * q + (1-q)) powr n / ((1-q) powr (1-\<gamma>)) powr n"
       unfolding powr_powr by simp
     also have "... = ((\<delta>_avg * q + (1-q)) / (1-q) powr (1-\<gamma>)) powr n"
       using assms(6) q_range by (subst powr_divide) auto
     also have "... = exp (- KL_div \<gamma> \<delta>_avg) powr real n"
       unfolding 5[OF True] by simp
     also have "... = ?R1"
       unfolding exp_powr by simp
     finally show ?thesis by simp
   next
     case False
     hence \<gamma>_eq_1: "\<gamma>=1" using assms(5) by simp
     have "?L1 = \<delta>_avg ^ n"
       using \<gamma>_eq_1 r_def q_def by simp
     also have "... = exp( - KL_div 1 \<delta>_avg) ^ n"
       unfolding KL_div_def using assms(6) by (simp add:ln_div)
     also have "... = ?R1"
       using \<gamma>_eq_1 by (simp add: powr_realpow[symmetric] exp_powr)
     finally show ?thesis by simp
   qed
 
   have 4: "(1 - q) ^ r > 0"
   proof (cases "\<gamma> < 1")
     case True
     then show ?thesis using q_lt_1[OF True] by simp
   next
     case False
     hence "\<gamma>=1" using assms(5) by simp
     hence "r=0" unfolding r_def by simp
     then show ?thesis by simp
   qed
 
   have "(1-q) ^ r * ?L = (\<integral>\<omega>. indicator {\<omega>. ?E \<omega>} \<omega> * (1-q) ^ r \<partial>p)"
     by simp
   also have "... \<le> (\<integral>\<omega>. indicator {\<omega>. ?E \<omega>} \<omega> * (1-q) ^ g \<omega> \<partial>p)"
     using q_range 2 by (intro integral_mono_AE integrable_pmf_iff_bounded[where C="1"]
         abs_pos_le_1I mult_le_one power_le_one AE_pmfI) (simp_all split:split_indicator)
   also have "... = (\<integral>\<omega>. indicator {\<omega>. ?E \<omega>} \<omega> * (\<Prod>i \<in> {i. i < n \<and> \<not>Y i \<omega>}. (1-q)) \<partial>p)"
     unfolding g_def using q_range
     by (intro integral_cong_AE AE_pmfI, simp_all add:powr_realpow)
   also have "... = (\<integral>\<omega>. indicator {\<omega>. ?E \<omega>} \<omega> * measure ?\<Xi> ({j. j < n \<and> \<not>Y j \<omega>} \<rightarrow> {False}) \<partial>p)"
     using q_range by (subst prob_prod_pmf') (auto simp add:measure_pmf_single)
   also have "... = (\<integral>\<omega>. measure ?\<Xi> {\<xi>. ?E \<omega> \<and> (\<forall>i\<in>{j. j < n \<and> \<not>Y j \<omega>}. \<not>\<xi> i)} \<partial>p)"
     by (intro integral_cong_AE AE_pmfI, simp_all add:Pi_def split:split_indicator)
   also have "... = (\<integral>\<omega>. measure ?\<Xi> {\<xi>. ?E \<omega> \<and> (\<forall>i\<in>{..<n}. \<xi> i \<longrightarrow> Y i \<omega>)} \<partial>p)"
     by (intro integral_cong_AE AE_pmfI measure_eq_AE) auto
   also have "... = measure (pair_pmf p ?\<Xi>) {\<phi>.?E (fst \<phi>)\<and>(\<forall>i \<in> {..<n}. snd \<phi> i \<longrightarrow> Y i (fst \<phi>))}"
     unfolding split_pair_pmf by simp
   also have "... \<le> measure (pair_pmf p ?\<Xi>) {\<phi>. (\<forall>i \<in> {j. j < n \<and> snd \<phi> j}. Y i (fst \<phi>))}"
     by (intro pmf_mono, auto)
   also have "... = (\<integral>\<xi>. measure p {\<omega>. \<forall>i\<in>{j. j< n \<and> \<xi> j}. Y i \<omega>} \<partial> ?\<Xi>)"
     unfolding split_pair_pmf_2 by simp
   also have "... \<le> (\<integral>a. (\<Prod>i \<in> {j. j < n \<and> a j}. \<delta> i) \<partial> ?\<Xi>)"
     using assms(2) by (intro integral_mono_AE AE_pmfI assms(3) subsetI  prod_le_1 prod_nonneg
         integrable_pmf_iff_bounded[where C="1"] abs_pos_le_1I) auto
   also have "... = (\<integral>a. (\<Prod>i \<in> {..<n}. \<delta> i^ of_bool(a i)) \<partial> ?\<Xi>)"
     unfolding of_bool_def by (intro integral_cong_AE AE_pmfI)
       (auto simp add:if_distrib prod.If_cases Int_def)
   also have "... = (\<Prod>i<n. (\<integral>a. (\<delta> i ^ of_bool a) \<partial>(bernoulli_pmf q)))"
     using assms(2) by (intro expectation_prod_Pi_pmf integrable_pmf_iff_bounded[where C="1"]) auto
   also have "... = (\<Prod>i<n. \<delta> i * q + (1-q))"
     using q_range by simp
   also have "... = (root (card {..<n}) (\<Prod>i<n. \<delta> i * q + (1-q))) ^ (card {..<n})"
     using assms(1,2) q_range by (intro real_root_pow_pos2[symmetric] prod_nonneg) auto
   also have "... \<le> ((\<Sum>i<n. \<delta> i * q + (1-q))/card{..<n})^(card {..<n})"
     using assms(1,2) q_range by (intro power_mono arithmetic_geometric_mean)
       (auto intro: prod_nonneg)
   also have "... = ((\<Sum>i<n. \<delta> i * q)/n + (1-q))^n"
     using assms(1) by (simp add:sum.distrib divide_simps mult.commute)
   also have "... = (\<delta>_avg * q + (1-q))^n"
     unfolding \<delta>_avg_def by (simp add: sum_distrib_right[symmetric])
   finally have "(1-q) ^ r * ?L \<le> (\<delta>_avg * q + (1-q)) ^ n" by simp
   hence "?L \<le> (\<delta>_avg * q + (1-q)) ^ n / (1-q) ^ r"
     using 4 by (subst pos_le_divide_eq) (auto simp add:algebra_simps)
   also have "... \<le> ?R"
     by (intro 3)
   finally show ?thesis by simp
 qed
 
 text \<open>The distribution of a random variable with a countable range is a discrete probability space,
 i.e., induces a PMF. Using this it is possible to generalize the previous result to arbitrary
 probability spaces.\<close>
 
 lemma (in prob_space) establish_pmf:
   fixes f :: "'a \<Rightarrow> 'b"
   assumes rv: "random_variable discrete f"
   assumes "countable (f ` space M)"
   shows "distr M discrete f \<in> {M. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
 proof -
   define N where "N = {x \<in> space M.\<not> prob (f -` {f x} \<inter> space M) \<noteq> 0}"
   define I where "I = {z \<in> (f ` space M). prob (f -` {z}  \<inter> space M) = 0}"
 
   have countable_I: " countable I"
     unfolding I_def by (intro countable_subset[OF _ assms(2)]) auto
 
   have disj: "disjoint_family_on (\<lambda>y. f -` {y} \<inter> space M) I"
     unfolding disjoint_family_on_def by auto
 
   have N_alt_def: "N = (\<Union>y \<in> I. f -` {y} \<inter> space M)"
     unfolding N_def I_def by (auto simp add:set_eq_iff)
   have "emeasure M N = \<integral>\<^sup>+ y. emeasure M (f -` {y} \<inter> space M) \<partial>count_space I"
     using rv countable_I unfolding N_alt_def
     by (subst emeasure_UN_countable) (auto simp add:disjoint_family_on_def)
   also have "... =  \<integral>\<^sup>+ y. 0 \<partial>count_space I"
     unfolding I_def using emeasure_eq_measure ennreal_0
     by (intro nn_integral_cong) auto
   also have "... = 0" by simp
   finally have 0:"emeasure M N = 0" by simp
 
   have 1:"N \<in> events"
     unfolding N_alt_def using rv
     by (intro  sets.countable_UN'' countable_I) simp
 
   have " AE x in M. prob (f -` {f x} \<inter> space M) \<noteq> 0"
     using 0 1 by (subst AE_iff_measurable[OF _ N_def[symmetric]])
   hence " AE x in M. measure (distr M discrete f) {f x} \<noteq> 0"
     by (subst measure_distr[OF rv], auto)
   hence "AE x in distr M discrete f. measure (distr M discrete f) {x} \<noteq> 0"
     by (subst AE_distr_iff[OF rv], auto)
   thus ?thesis
     using prob_space_distr rv by auto
 qed
 
 lemma singletons_image_eq:
   "(\<lambda>x. {x}) ` T \<subseteq> Pow T"
   by auto
 
 theorem (in prob_space) impagliazzo_kabanets:
   fixes Y :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
   assumes "n > 0"
   assumes "\<And>i. i \<in> {..<n} \<Longrightarrow> random_variable discrete (Y i)"
   assumes "\<And>i. i \<in> {..<n} \<Longrightarrow> \<delta> i \<in> {0..1}"
   assumes "\<And>S. S \<subseteq> {..<n} \<Longrightarrow> \<P>(\<omega> in M. (\<forall>i \<in> S. Y i \<omega>)) \<le> (\<Prod>i \<in> S. \<delta> i)"
   defines "\<delta>_avg \<equiv> (\<Sum>i\<in> {..<n}. \<delta> i)/n"
   assumes "\<gamma> \<in> {\<delta>_avg..1}" "\<delta>_avg > 0"
   shows "\<P>(\<omega> in M. real (card {i \<in> {..<n}. Y i \<omega>}) \<ge> \<gamma> * n) \<le> exp (-real n * KL_div \<gamma> \<delta>_avg)"
     (is "?L \<le> ?R")
 proof -
   define f where "f = (\<lambda>\<omega> i. if i < n then Y i \<omega> else False)"
   define g where "g = (\<lambda>\<omega> i. if i < n then \<omega> i else False)"
   define T where "T = {\<omega>. (\<forall>i. \<omega> i \<longrightarrow> i < n)}"
 
   have g_idem: "g \<circ> f = f" unfolding f_def g_def by (simp add:comp_def)
 
   have f_range: " f \<in> space M \<rightarrow> T"
     unfolding T_def f_def by simp
 
   have "T = PiE_dflt {..<n} False (\<lambda>_. UNIV)"
     unfolding T_def PiE_dflt_def by auto
   hence "finite T"
     using finite_PiE_dflt by auto
   hence countable_T: "countable T"
     by (intro countable_finite)
   moreover have "f ` space M \<subseteq> T"
     using f_range by auto
   ultimately have countable_f: "countable (f ` space M)"
     using countable_subset by auto
 
   have "f -` y \<inter> space M \<in> events" if t:"y \<in> (\<lambda>x. {x}) ` T" for y
   proof -
     obtain t where "y = {t}" and t_range: "t \<in> T" using t by auto
     hence "f -` y \<inter> space M = {\<omega> \<in> space M. f \<omega> = t}"
       by (auto simp add:vimage_def)
     also have "... = {\<omega> \<in> space M. (\<forall>i < n. Y i \<omega> = t i)}"
       using t_range unfolding f_def T_def by auto
     also have "... = (\<Inter>i \<in> {..<n}. {\<omega> \<in> space M. Y i \<omega> = t i})"
       using assms(1) by auto
     also have "... \<in> events"
       using assms(1,2)
       by (intro sets.countable_INT) auto
     finally show ?thesis by simp
   qed
 
   hence "random_variable (count_space T) f"
     using sigma_sets_singletons[OF countable_T] singletons_image_eq f_range
     by (intro measurable_sigma_sets[where \<Omega>="T" and A=" (\<lambda>x. {x}) ` T"]) simp_all
   moreover have "g \<in> measurable discrete (count_space T)"
     unfolding g_def T_def by simp
   ultimately have "random_variable discrete (g \<circ> f)"
     by simp
   hence rv:"random_variable discrete f"
     unfolding g_idem by simp
 
   define M' :: "(nat \<Rightarrow> bool) measure"
     where "M' = distr M discrete f"
 
   define \<Omega> where "\<Omega> = Abs_pmf M'"
   have a:"measure_pmf (Abs_pmf M') = M'"
     unfolding M'_def
     by (intro Abs_pmf_inverse[OF establish_pmf] rv countable_f)
 
   have b:"{i. (i < n \<longrightarrow> Y i x) \<and> i < n} = {i. i < n \<and> Y i x}" for x
     by auto
 
   have c: "measure \<Omega> {\<omega>. \<forall>i\<in>S. \<omega> i} \<le> prod \<delta> S" (is "?L1 \<le> ?R1") if "S \<subseteq> {..<n}" for S
   proof -
     have d: "i \<in> S \<Longrightarrow> i < n" for i
       using that by auto
     have "?L1 = measure M' {\<omega>. \<forall>i\<in>S. \<omega> i}"
       unfolding \<Omega>_def a by simp
     also have "... = \<P>(\<omega> in M. (\<forall>i \<in> S. Y i \<omega>))"
       unfolding M'_def using that d
       by (subst measure_distr[OF rv]) (auto simp add:f_def Int_commute Int_def)
     also have "... \<le> ?R1"
       using that assms(4) by simp
     finally show ?thesis by simp
   qed
 
   have "?L = measure M' {\<omega>. real (card {i. i < n \<and> \<omega> i}) \<ge> \<gamma> * n}"
     unfolding M'_def by (subst measure_distr[OF rv])
       (auto simp add:f_def algebra_simps Int_commute Int_def b)
   also have "... = measure_pmf.prob \<Omega> {\<omega>. real (card {i \<in> {..<n}. \<omega> i}) \<ge> \<gamma> * n}"
     unfolding \<Omega>_def a by simp
   also have "... \<le> ?R"
     using assms(1,3,6,7) c unfolding \<delta>_avg_def
     by (intro impagliazzo_kabanets_pmf) auto
   finally show ?thesis by simp
 qed
 
 text \<open>Bounds and properties of @{term "KL_div"}\<close>
 
 lemma KL_div_mono_right_aux_1:
   assumes "0 \<le> p" "p \<le> q" "q \<le> q'" "q' < 1"
   shows "KL_div p q-2*(p-q)^2 \<le> KL_div p q'-2*(p-q')^2"
 proof (cases "p = 0")
   case True
   define f' :: "real \<Rightarrow> real" where "f' = (\<lambda>x. 1/(1-x) - 4 * x)"
 
   have deriv: "((\<lambda>q. ln (1/(1-q)) - 2*q^2) has_real_derivative (f' x)) (at x)"
     if "x \<in> {q..q'}" for x
   proof -
     have "x \<in> {0..<1}" using assms that by auto
     thus ?thesis unfolding f'_def by (auto intro!: derivative_eq_intros)
   qed
 
   have deriv_nonneg: "f' x \<ge> 0" if "x \<in> {q..q'}" for x
   proof -
     have 0:"x \<in> {0..<1}" using assms that by auto
     have "4 * x*(1-x) = 1 - 4*(x-1/2)^2" by (simp add:power2_eq_square field_simps)
     also have "... \<le> 1" by simp
     finally have "4*x*(1-x) \<le> 1" by simp
     hence "1/(1-x) \<ge> 4*x" using 0 by (simp add: pos_le_divide_eq)
     thus ?thesis unfolding f'_def by auto
   qed
 
   have "ln (1 / (1 - q)) - 2 * q^2 \<le> ln (1 / (1 - q')) - 2 * q'^2"
     using deriv deriv_nonneg by (intro DERIV_nonneg_imp_nondecreasing[OF assms(3)]) auto
   thus ?thesis using True unfolding KL_div_def by simp
 next
   case False
   hence p_gt_0: "p > 0" using assms by auto
 
   define f' :: "real \<Rightarrow> real" where "f' = (\<lambda>x. (1-p)/(1-x) - p/x + 4 * (p-x))"
 
   have deriv: "((\<lambda>q. KL_div p q - 2*(p-q)^2) has_real_derivative (f' x)) (at x)" if "x \<in> {q..q'}"
     for x
   proof -
     have "0 < p /x" " 0 < (1 - p) / (1 - x)" using that assms p_gt_0 by auto
     thus ?thesis unfolding KL_div_def f'_def by (auto intro!: derivative_eq_intros)
   qed
 
   have f'_part_nonneg: "(1/(x*(1-x)) - 4) \<ge> 0" if "x \<in> {0<..<1}" for x :: real
   proof -
     have "4 * x * (1-x) = 1 - 4 * (x-1/2)^2" by (simp add:power2_eq_square algebra_simps)
     also have "... \<le> 1" by simp
     finally have "4 * x * (1-x) \<le> 1" by simp
     hence "1/(x*(1-x)) \<ge> 4" using that by (subst pos_le_divide_eq) auto
     thus ?thesis by simp
   qed
 
   have f'_alt: "f' x = (x-p)*(1/(x*(1-x)) - 4)" if "x \<in> {0<..<1}" for x
   proof -
     have "f' x = (x-p)/(x*(1-x)) + 4 * (p-x)" using that unfolding f'_def by (simp add:field_simps)
     also have "... = (x-p)*(1/(x*(1-x)) - 4)" by (simp add:algebra_simps)
     finally show ?thesis by simp
   qed
 
   have deriv_nonneg: "f' x \<ge> 0" if "x \<in> {q..q'}" for x
   proof -
     have "x \<in> {0<..<1}" using assms that p_gt_0 by auto
     have "f' x =(x-p)*(1/(x*(1-x)) - 4)" using that assms p_gt_0 by (subst f'_alt) auto
     also have "... \<ge> 0" using that f'_part_nonneg assms p_gt_0 by (intro mult_nonneg_nonneg) auto
     finally show ?thesis by simp
   qed
 
   show ?thesis using deriv deriv_nonneg
     by (intro DERIV_nonneg_imp_nondecreasing[OF assms(3)]) auto
 qed
 
 lemma KL_div_swap: "KL_div (1-p) (1-q) = KL_div p q"
   unfolding KL_div_def by auto
 
 lemma KL_div_mono_right_aux_2:
   assumes "0 < q'" "q' \<le> q" "q \<le> p" "p \<le> 1"
   shows "KL_div p q-2*(p-q)^2 \<le> KL_div p q'-2*(p-q')^2"
 proof -
   have "KL_div (1-p) (1-q)-2*((1-p)-(1-q))^2 \<le> KL_div (1-p) (1-q')-2*((1-p)-(1-q'))^2"
     using assms by (intro KL_div_mono_right_aux_1) auto
   thus ?thesis unfolding KL_div_swap by (auto simp:algebra_simps power2_commute)
 qed
 
 lemma KL_div_mono_right_aux:
   assumes "(0 \<le> p \<and> p \<le> q \<and> q \<le> q' \<and> q' < 1) \<or> (0 < q' \<and> q' \<le> q \<and> q \<le> p \<and> p \<le> 1)"
   shows "KL_div p q-2*(p-q)^2 \<le> KL_div p q'-2*(p-q')^2"
   using KL_div_mono_right_aux_1 KL_div_mono_right_aux_2 assms by auto
 
 lemma KL_div_mono_right:
   assumes "(0 \<le> p \<and> p \<le> q \<and> q \<le> q' \<and> q' < 1) \<or> (0 < q' \<and> q' \<le> q \<and> q \<le> p \<and> p \<le> 1)"
   shows "KL_div p q \<le> KL_div p q'" (is "?L \<le> ?R")
 proof -
   consider (a) "0 \<le> p" "p \<le> q" "q \<le> q'" "q' < 1" | (b) "0 < q'" "q' \<le> q" "q \<le> p" "p \<le> 1"
     using assms by auto
   hence 0: "(p - q)\<^sup>2 \<le> (p - q')\<^sup>2"
   proof (cases)
     case a
     hence "(q-p)^2 \<le> (q' - p)^2" by auto
     thus ?thesis by (simp add: power2_commute)
   next
     case b thus ?thesis by simp
   qed
   have "?L = (KL_div p q - 2*(p-q)^2) + 2 * (p-q)^2" by simp
   also have "... \<le> (KL_div p q' - 2*(p-q')^2) + 2 * (p-q')^2"
     by (intro add_mono KL_div_mono_right_aux assms mult_left_mono 0) auto
   also have "... = ?R" by simp
   finally show ?thesis by simp
 qed
 
+lemma KL_div_lower_bound:
+  assumes "p \<in> {0..1}" "q \<in> {0<..<1}"
+  shows "2*(p-q)^2 \<le> KL_div p q"
+proof -
+  have "0 \<le> KL_div p p - 2 * (p-p)^2" unfolding KL_div_def by simp
+  also have "... \<le> KL_div p q - 2 * (p-q)^2" using assms by (intro KL_div_mono_right_aux) auto
+  finally show ?thesis by simp
+qed
+
 end
\ No newline at end of file
diff --git a/thys/Expander_Graphs/Pseudorandom_Objects_Expander_Walks.thy b/thys/Expander_Graphs/Pseudorandom_Objects_Expander_Walks.thy
--- a/thys/Expander_Graphs/Pseudorandom_Objects_Expander_Walks.thy
+++ b/thys/Expander_Graphs/Pseudorandom_Objects_Expander_Walks.thy
@@ -1,210 +1,312 @@
 section \<open>Expander Walks as Pseudorandom Objects\<close>
 
 theory Pseudorandom_Objects_Expander_Walks
   imports
     Universal_Hash_Families.Pseudorandom_Objects
     Expander_Graphs.Expander_Graphs_Strongly_Explicit
 begin
 
+unbundle intro_cong_syntax
 hide_const (open) Quantum.T
+hide_fact (open) SN_Orders.of_nat_mono
+hide_fact Missing_Ring.mult_pos_pos
 
 definition expander_pro ::
   "nat \<Rightarrow> real \<Rightarrow> ('a,'b) pseudorandom_object_scheme \<Rightarrow> (nat \<Rightarrow> 'a) pseudorandom_object"
   where "expander_pro l \<Lambda> S = (
     let e = see_standard (pro_size S) \<Lambda> in
       \<lparr> pro_last = see_size e * see_degree e^(l-1) - 1,
         pro_select = (\<lambda>i j. pro_select S (see_sample_walk e (l-1) i ! j mod pro_size S)) \<rparr>
     )"
 
 context
   fixes l :: nat
   fixes \<Lambda> :: real
   fixes S :: "('a,'b) pseudorandom_object_scheme"
   assumes l_gt_0: "l > 0"
   assumes \<Lambda>_gt_0: "\<Lambda> > 0"
 begin
 
 private definition e where "e = see_standard (pro_size S) \<Lambda>"
 
 private lemma expander_pro_alt: "expander_pro l \<Lambda> S = \<lparr> pro_last = see_size e * see_degree e^(l-1) - 1,
         pro_select = (\<lambda>i j. pro_select S (see_sample_walk e (l-1) i ! j mod pro_size S)) \<rparr>"
   unfolding expander_pro_def e_def[symmetric] by (auto simp:Let_def)
 
 private lemmas see_standard = see_standard [OF pro_size_gt_0[where S="S"] \<Lambda>_gt_0]
 
 interpretation E: regular_graph "graph_of e"
   using see_standard(1) unfolding is_expander_def e_def by auto
 
 private lemma e_deg_gt_0: "see_degree e > 0"
   unfolding e_def see_standard by simp
 
 private lemma e_size_gt_0: "see_size e > 0"
   unfolding e_def using see_standard pro_size_gt_0 by simp
 
 private lemma expander_sample_size: "pro_size (expander_pro l \<Lambda> S) =  see_size e * see_degree e^(l-1)"
   using e_deg_gt_0 e_size_gt_0 unfolding expander_pro_alt pro_size_def by simp
 
 private lemma sample_pro_expander_walks:
   defines "R \<equiv> map_pmf (\<lambda>xs i. pro_select S (xs ! i mod pro_size S))
     (pmf_of_multiset (walks (graph_of e) l))"
   shows "sample_pro (expander_pro l \<Lambda> S) = R"
 proof -
   let ?S = "{..<see_size e * see_degree e ^ (l-1)}"
   let ?T = "(map_pmf (see_sample_walk e (l-1)) (pmf_of_set ?S))"
 
   have "0 \<in> ?S"
     using e_size_gt_0 e_deg_gt_0  by auto
   hence "?S \<noteq> {}"
     by blast
   hence "?T = pmf_of_multiset {#see_sample_walk e (l-1) i. i \<in># mset_set ?S#}"
     by (subst map_pmf_of_set) simp_all
   also have "... = pmf_of_multiset (walks' (graph_of e) (l-1))"
     by (subst see_sample_walk) auto
   also have "... = pmf_of_multiset (walks (graph_of e) l)"
     unfolding walks_def using l_gt_0 by (cases l, simp_all)
   finally have 0:"?T = pmf_of_multiset (walks (graph_of e) l)"
     by simp
 
   have "sample_pro (expander_pro l \<Lambda> S) = map_pmf (\<lambda>xs j. pro_select S (xs ! j mod pro_size S)) ?T"
     unfolding expander_sample_size sample_pro_alt unfolding map_pmf_comp expander_pro_alt by simp
   also have "... = R" unfolding 0 R_def by simp
   finally show ?thesis by simp
 qed
 
+lemma expander_pro_range: "pro_select (expander_pro l \<Lambda> S) i j \<in> pro_set S"
+  unfolding expander_pro_alt by (simp add:pro_select_in_set)
+
 lemma expander_uniform_property:
   assumes "i < l"
   shows "map_pmf (\<lambda>w. w i) (sample_pro (expander_pro l \<Lambda> S)) = sample_pro S" (is "?L = ?R")
 proof -
   have "?L = map_pmf (\<lambda>x. pro_select S (x mod pro_size S)) (map_pmf (\<lambda>xs. (xs ! i)) (pmf_of_multiset (walks (graph_of e) l)))"
     unfolding sample_pro_expander_walks by (simp add: map_pmf_comp)
   also have "... = map_pmf (\<lambda>x. pro_select S (x mod pro_size S)) (pmf_of_set (verts (graph_of e)))"
     unfolding E.uniform_property[OF assms] by simp
   also have "... = ?R"
     using pro_size_gt_0 unfolding sample_pro_alt
     by (intro map_pmf_cong) (simp_all add:e_def graph_of_def see_standard select_def)
   finally show ?thesis
     by simp
 qed
 
 lemma expander_kl_chernoff_bound:
   assumes "measure (sample_pro S) {w. T w} \<le> \<mu>"
   assumes "\<gamma> \<le> 1" "\<mu> + \<Lambda> * (1-\<mu>) \<le> \<gamma>" "\<mu> \<le> 1"
   shows "measure (sample_pro (expander_pro l \<Lambda> S)) {w. real (card {i \<in> {..<l}. T (w i)}) \<ge> \<gamma>*l}
     \<le> exp (- real l * KL_div \<gamma> (\<mu> + \<Lambda>*(1-\<mu>)))" (is "?L \<le> ?R")
 proof (cases "measure (sample_pro S) {w. T w} > 0")
   case True
   let ?w = "pmf_of_multiset (walks (graph_of e) l)"
   define V where "V = {v\<in> verts (graph_of e). T (pro_select S v)} "
   define \<nu> where "\<nu> = measure (sample_pro S) {w. T w}"
 
   have \<nu>_gt_0: "\<nu> > 0" unfolding \<nu>_def using True by simp
   have \<nu>_le_1: "\<nu> \<le> 1" unfolding \<nu>_def by simp
   have \<nu>_le_\<mu>: "\<nu> \<le> \<mu>" unfolding \<nu>_def using assms(1) by simp
 
   have 0: "card {i \<in> {..<l}. T (pro_select S (w ! i mod pro_size S))} = card {i \<in> {..<l}. w ! i \<in> V}"
     if "w  \<in> set_pmf (pmf_of_multiset (walks (graph_of e) l))" for w
   proof -
     have a0: "w \<in># walks (graph_of e) l" using that E.walks_nonempty by simp
     have a1:"w ! i \<in> verts (graph_of e)" if "i < l" for i
       using that E.set_walks_3[OF a0] by auto
     moreover have "w ! i mod pro_size S = w ! i" if "i < l" for i
       using a1[OF that] see_standard(2) e_def by (simp add:graph_of_def)
     ultimately show ?thesis
       unfolding V_def
       by (intro arg_cong[where f="card"] restr_Collect_cong) auto
   qed
 
   have 1:"E.\<Lambda>\<^sub>a \<le> \<Lambda>"
     using see_standard(1) unfolding is_expander_def e_def by simp
 
   have 2: "V \<subseteq> verts (graph_of e)"
     unfolding V_def by simp
 
   have "\<nu> = measure (pmf_of_set {..<pro_size S}) ({v. T (pro_select S v)})"
     unfolding \<nu>_def sample_pro_alt by simp
   also have "... = real (card ({v\<in>{..<pro_size S}. T (pro_select S v)})) / real (pro_size S)"
     using pro_size_gt_0 by (subst measure_pmf_of_set) (auto simp add:Int_def)
   also have "... = real (card V) / card (verts (graph_of e))"
     unfolding V_def graph_of_def e_def using see_standard by (simp add:Int_commute)
   finally have \<nu>_eq: "\<nu> = real (card V) / card (verts (graph_of e))"
     by simp
 
   have 3: "0 < \<nu> + E.\<Lambda>\<^sub>a * (1 - \<nu>)"
     using \<nu>_le_1 by (intro add_pos_nonneg \<nu>_gt_0 mult_nonneg_nonneg E.\<Lambda>_ge_0) auto
 
   have "\<nu> + E.\<Lambda>\<^sub>a * (1 - \<nu>) = \<nu> * (1 - E.\<Lambda>\<^sub>a) + E.\<Lambda>\<^sub>a" by (simp add:algebra_simps)
   also have "... \<le> \<mu> * (1- E.\<Lambda>\<^sub>a) + E.\<Lambda>\<^sub>a" using E.\<Lambda>_le_1
     by (intro add_mono mult_right_mono \<nu>_le_\<mu>) auto
   also have "... = \<mu> + E.\<Lambda>\<^sub>a * (1 - \<mu>)" by (simp add:algebra_simps)
   also have "... \<le> \<mu> + \<Lambda> * (1 - \<mu>)" using assms(4) by (intro add_mono mult_right_mono 1) auto
   finally have 4: "\<nu> + E.\<Lambda>\<^sub>a * (1 - \<nu>) \<le> \<mu> + \<Lambda> * (1 - \<mu>)" by simp
 
   have 5: "\<nu> + E.\<Lambda>\<^sub>a*(1-\<nu>) \<le> \<gamma>" using 4 assms(3) by simp
 
   have "?L = measure ?w {y. \<gamma> * real l \<le> real (card {i \<in> {..<l}. T (pro_select S (y ! i mod pro_size S))})}"
     unfolding sample_pro_expander_walks by simp
   also have "... = measure ?w {y. \<gamma> * real l \<le> real (card {i \<in> {..<l}. y ! i \<in> V})}"
     using 0 by (intro measure_pmf_cong) (simp)
   also have "... \<le> exp (- real l * KL_div \<gamma> (\<nu> + E.\<Lambda>\<^sub>a*(1-\<nu>)) )"
     using assms(2) 3 5 unfolding \<nu>_eq by (intro E.kl_chernoff_property l_gt_0 2) auto
   also have "... \<le> exp (- real l * KL_div \<gamma> (\<mu> + \<Lambda>*(1-\<mu>)))"
     using l_gt_0 by (intro iffD2[OF exp_le_cancel_iff] iffD2[OF mult_le_cancel_left_neg]
       KL_div_mono_right[OF disjI2] conjI 3 4 assms(2,3)) auto
   finally show ?thesis by simp
 next
   case False
   hence 0:"measure (sample_pro S) {w. T w} = 0" using zero_less_measure_iff by blast
   hence 1:"T w = False" if "w \<in> pro_set S" for w using that measure_pmf_posI by force
 
   have "\<mu> + \<Lambda> * (1-\<mu>) > 0"
   proof (cases "\<mu> = 0")
     case True then show ?thesis using \<Lambda>_gt_0 by auto
   next
     case False
     then show ?thesis using assms(1,4) 0 \<Lambda>_gt_0
       by (intro add_pos_nonneg mult_nonneg_nonneg) simp_all
   qed
   hence "\<gamma> > 0" using assms(3) by auto
   hence 2:"\<gamma>*real l > 0" using l_gt_0 by simp
 
   let ?w = "pmf_of_multiset (walks (graph_of e) l)"
 
   have "?L = measure ?w {y. \<gamma>*real l\<le> card {i \<in> {..<l}. T (pro_select S (y ! i mod pro_size S))}}"
     unfolding sample_pro_expander_walks by simp
   also have "... = 0" using pro_select_in_set 2 by (subst 1) auto
   also have "... \<le> ?R" by simp
   finally show ?thesis by simp
 qed
 
+lemma expander_chernoff_bound_one_sided:
+  assumes "AE x in sample_pro S. f x \<in> {0,1::real}"
+  assumes "(\<integral>x. f x \<partial>sample_pro S) \<le> \<mu>" "l > 0" "\<gamma> \<ge> 0"
+  shows "measure (expander_pro l \<Lambda> S) {w. (\<Sum>i<l. f (w i))/l-\<mu>\<ge>\<gamma>+\<Lambda>} \<le> exp (- 2 * real l * \<gamma>^2)"
+    (is "?L \<le> ?R")
+proof -
+  let ?w = "sample_pro (expander_pro l \<Lambda> S)"
+  define T where "T x = (f x=1)" for x
+
+  have 1: "indicator {w. T w} x = f x" if "x \<in> pro_set S" for x
+  proof -
+    have "f x \<in> {0,1}" using assms(1) that unfolding AE_measure_pmf_iff by simp
+    thus ?thesis unfolding T_def by auto
+  qed
+
+  have "measure S {w. T w} = (\<integral>x. indicator {w. T w} x \<partial>S)" by simp
+  also have "... = (\<integral>x. f x \<partial>S)" using 1 by (intro integral_cong_AE AE_pmfI) auto
+  also have "... \<le> \<mu>" using assms(2) by simp
+  finally have 0: "measure S {w. T w} \<le> \<mu>" by simp
+
+  hence \<mu>_ge_0: "\<mu> \<ge> 0" using measure_nonneg order.trans by blast
+
+  have cases: "(\<gamma>=0 \<Longrightarrow> p) \<Longrightarrow> (\<gamma>+\<Lambda>+\<mu> > 1  \<Longrightarrow> p) \<Longrightarrow> (\<gamma>+\<Lambda>+\<mu> \<le> 1 \<and> \<gamma> > 0 \<Longrightarrow> p) \<Longrightarrow> p" for p
+    using assms(4) by argo
+
+  have "?L = measure ?w {w. (\<gamma>+\<Lambda>+\<mu>)*l \<le> (\<Sum>i<l. f (w i))}"
+    using assms(3) by (intro measure_pmf_cong) (auto simp:field_simps)
+  also have "... = measure ?w {w. (\<gamma>+\<Lambda>+\<mu>)*l \<le> card {i \<in> {..<l}. T (w i)}}"
+  proof (rule measure_pmf_cong)
+    fix \<omega>
+    assume "\<omega> \<in> pro_set (expander_pro l \<Lambda> S)"
+    hence "\<omega> x \<in> pro_set S" for x using expander_pro_range set_sample_pro by (metis image_iff)
+    hence "(\<Sum>i<l. f (\<omega> i)) = (\<Sum>i<l. indicator {w. T w} (\<omega> i))" using 1 by (intro sum.cong) auto
+    also have "... = card {i \<in> {..<l}. T (\<omega> i)}" unfolding indicator_def by (auto simp:Int_def)
+    finally have "(\<Sum>i<l. f (\<omega> i)) = (card {i \<in> {..<l}. T (\<omega> i)})" by simp
+    thus "(\<omega> \<in> {w. (\<gamma>+\<Lambda>+\<mu>)*l \<le> (\<Sum>i<l. f (w i))})=(\<omega> \<in> {w. (\<gamma>+\<Lambda>+\<mu>)*l\<le>card {i \<in> {..<l}. T (w i)}})"
+      by simp
+  qed
+  also have "... \<le> ?R" (is "?L1 \<le> _")
+  proof (rule cases)
+    assume "\<gamma> = 0" thus "?thesis" by simp
+  next
+    assume a:"\<gamma> + \<Lambda> + \<mu> \<le> 1 \<and> 0 < \<gamma>"
+    hence \<mu>_lt_1: "\<mu> < 1" using assms(4) \<Lambda>_gt_0 by simp
+    hence \<mu>_le_1: "\<mu> \<le> 1" by simp
+    have "\<mu> + \<Lambda> * (1 - \<mu>) \<le> \<mu> + \<Lambda> * 1" using \<mu>_ge_0 \<Lambda>_gt_0 by (intro add_mono mult_left_mono) auto
+    also have "... < \<gamma>+\<Lambda>+\<mu>" using assms(4) a by simp
+    finally have b:"\<mu> + \<Lambda> * (1 - \<mu>) < \<gamma> +\<Lambda> +\<mu>" by simp
+    hence "\<mu> + \<Lambda> * (1 - \<mu>) < 1" using a by simp
+    moreover have "\<mu> + \<Lambda> * (1 - \<mu>) > 0" using \<mu>_lt_1
+      by (intro add_nonneg_pos \<mu>_ge_0 mult_pos_pos \<Lambda>_gt_0) simp
+    ultimately have c: "\<mu> + \<Lambda> * (1 - \<mu>) \<in> {0<..<1}" by simp
+    have d: " \<gamma> + \<Lambda> + \<mu> \<in> {0..1}" using a b c by simp
+    have "?L1 \<le> exp (- real l * KL_div (\<gamma>+\<Lambda>+\<mu>) (\<mu> + \<Lambda>*(1-\<mu>)))"
+      using a b by (intro expander_kl_chernoff_bound \<mu>_le_1 0) auto
+    also have "... \<le> exp (- real l * (2 * ((\<gamma>+\<Lambda>+\<mu>)- (\<mu> + \<Lambda>*(1-\<mu>)))^2))"
+      by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg KL_div_lower_bound c d) simp
+    also have "... \<le> exp (- real l * (2 * (\<gamma>^2)))"
+      using assms(4) \<mu>_lt_1 \<Lambda>_gt_0 \<mu>_ge_0
+      by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg[where c="-real l"] mult_left_mono
+          power_mono) simp_all
+    also have "... = ?R" by simp
+    finally show "?L1 \<le> ?R" by simp
+  next
+    assume a:"1 < \<gamma> + \<Lambda> + \<mu>"
+    have "(\<gamma>+\<Lambda>+\<mu>)* real l > real (card {i \<in> {..<l}. (x i)})" for x
+    proof -
+      have "real (card {i \<in> {..<l}. (x i)}) \<le> card {..<l}" by (intro of_nat_mono card_mono) auto
+      also have "... = real l" by simp
+      also have "... < (\<gamma>+\<Lambda>+\<mu>)* real l" using assms(3) a by simp
+      finally show ?thesis by simp
+    qed
+    hence "?L1 = 0" unfolding not_le[symmetric] by auto
+    also have "... \<le> ?R" by simp
+    finally show "?L1 \<le> ?R" by simp
+  qed
+  finally show ?thesis by simp
+qed
+
+lemma expander_chernoff_bound:
+  assumes "AE x in sample_pro S. f x \<in> {0,1::real}" "l > 0" "\<gamma> \<ge> 0"
+  defines "\<mu> \<equiv> (\<integral>x. f x \<partial>sample_pro S)"
+  shows "measure (expander_pro l \<Lambda> S) {w. \<bar>(\<Sum>i<l. f (w i))/l-\<mu>\<bar>\<ge>\<gamma>+\<Lambda>} \<le> 2*exp (- 2 * real l * \<gamma>^2)"
+    (is "?L \<le> ?R")
+proof -
+  let ?w = "sample_pro (expander_pro l \<Lambda> S)"
+  have "?L \<le> measure ?w {w. (\<Sum>i<l. f (w i))/l-\<mu>\<ge>\<gamma>+\<Lambda>} + measure ?w {w. (\<Sum>i<l. f (w i))/l-\<mu>\<le>-(\<gamma>+\<Lambda>)}"
+    by (intro pmf_add) auto
+  also have "... \<le> exp (-2*real l*\<gamma>^2) + measure ?w {w. -((\<Sum>i<l. f (w i))/l-\<mu>)\<ge>(\<gamma>+\<Lambda>)}"
+    using assms by (intro add_mono expander_chernoff_bound_one_sided) (auto simp:algebra_simps)
+  also have "... \<le> exp (-2*real l*\<gamma>^2) + measure ?w {w. ((\<Sum>i<l. 1-f (w i))/l-(1-\<mu>))\<ge>(\<gamma>+\<Lambda>)}"
+    using assms(2) by (auto simp: sum_subtractf field_simps)
+  also have "... \<le> exp (-2*real l*\<gamma>^2) + exp (-2*real l*\<gamma>^2)"
+    using assms by (intro add_mono expander_chernoff_bound_one_sided) auto
+  also have "... = ?R" by simp
+  finally show ?thesis by simp
+qed
+
 lemma expander_pro_size:
   "pro_size (expander_pro l \<Lambda> S) = pro_size S * (16 ^ ((l-1) * nat \<lceil>ln \<Lambda> / ln (19 / 20)\<rceil>))"
   (is "?L = ?R")
 proof -
   have "?L = see_size e * see_degree e ^ (l - 1)"
     unfolding expander_sample_size by simp
   also have "... = pro_size S * (16 ^ nat \<lceil>ln \<Lambda> / ln (19 / 20)\<rceil>) ^ (l - 1)"
     using see_standard unfolding e_def by simp
   also have "... = pro_size S * (16 ^ ((l-1) * nat \<lceil>ln \<Lambda> / ln (19 / 20)\<rceil>))"
     unfolding power_mult[symmetric] by (simp add:ac_simps)
   finally show ?thesis
     by simp
 qed
 
-lemma expander_pro_range: "pro_select (expander_pro l \<Lambda> S) i j \<in> pro_set S"
-  unfolding expander_pro_alt by (simp add:pro_select_in_set)
-
 end
 
 bundle expander_pseudorandom_object_notation
 begin
 notation expander_pro ("\<E>")
 end
 
 bundle no_expander_pseudorandom_object_notation
 begin
 no_notation expander_pro ("\<E>")
 end
 
 unbundle expander_pseudorandom_object_notation
+unbundle no_intro_cong_syntax
 
 end
\ No newline at end of file
diff --git a/thys/Universal_Hash_Families/Universal_Hash_Families_More_Product_PMF.thy b/thys/Universal_Hash_Families/Universal_Hash_Families_More_Product_PMF.thy
--- a/thys/Universal_Hash_Families/Universal_Hash_Families_More_Product_PMF.thy
+++ b/thys/Universal_Hash_Families/Universal_Hash_Families_More_Product_PMF.thy
@@ -1,257 +1,268 @@
 section \<open>Indexed Products of Probability Mass Functions\<close>
 
 theory Universal_Hash_Families_More_Product_PMF
   imports
     "HOL-Probability.Product_PMF"
     Concentration_Inequalities.Concentration_Inequalities_Preliminary
     Finite_Fields.Finite_Fields_More_Bijections
     Universal_Hash_Families_More_Independent_Families
 begin
 
 hide_const (open) Isolated.discrete
 
 text \<open>This section introduces a restricted version of @{term "Pi_pmf"} where the default value is @{term "undefined"}
 and contains some additional results about that case in addition to @{theory "HOL-Probability.Product_PMF"}\<close>
 
 abbreviation prod_pmf where "prod_pmf I M \<equiv> Pi_pmf I undefined M"
 
 lemma measure_pmf_cong:
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> P \<longleftrightarrow> x \<in> Q"
   shows "measure (measure_pmf p) P = measure (measure_pmf p)  Q"
   using assms
   by (intro finite_measure.finite_measure_eq_AE AE_pmfI) auto
 
 lemma pmf_mono:
   assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> P \<Longrightarrow> x \<in> Q"
   shows "measure (measure_pmf p) P \<le> measure (measure_pmf p) Q"
 proof -
   have "measure (measure_pmf p) P = measure (measure_pmf p) (P \<inter> (set_pmf p))"
     by (intro measure_pmf_cong) auto
   also have "... \<le> measure (measure_pmf p) Q"
     using assms by (intro finite_measure.finite_measure_mono) auto
   finally show ?thesis by simp
 qed
 
+lemma pmf_add:
+  assumes  "\<And>x. x \<in> P \<Longrightarrow> x \<in> set_pmf p \<Longrightarrow> x \<in> Q \<or> x \<in> R"
+  shows "measure p P \<le> measure p Q + measure p R"
+proof -
+  have "measure p P \<le> measure p (Q \<union> R)"
+    using assms by (intro pmf_mono) blast
+  also have "... \<le> measure p Q + measure p R"
+    by (rule measure_subadditive, auto)
+  finally show ?thesis by simp
+qed
+
 lemma pmf_prod_pmf:
   assumes "finite I"
   shows "pmf (prod_pmf I M) x = (if x \<in> extensional I then \<Prod>i \<in> I. (pmf (M i)) (x i) else 0)"
   by (simp add:  pmf_Pi[OF assms(1)] extensional_def)
 
 lemma PiE_defaut_undefined_eq: "PiE_dflt I undefined M = PiE I M"
   by (simp add:PiE_dflt_def PiE_def extensional_def Pi_def set_eq_iff) blast
 
 lemma set_prod_pmf:
   assumes "finite I"
   shows "set_pmf (prod_pmf I M) = PiE I (set_pmf \<circ> M)"
   by (simp add:set_Pi_pmf[OF assms] PiE_defaut_undefined_eq)
 
 text \<open>A more general version of @{thm [source] "measure_Pi_pmf_Pi"}.\<close>
 lemma prob_prod_pmf':
   assumes "finite I"
   assumes "J \<subseteq> I"
   shows "measure (measure_pmf (Pi_pmf I d M)) (Pi J A) = (\<Prod> i \<in> J. measure (M i) (A i))"
 proof -
   have a:"Pi J A = Pi I (\<lambda>i. if i \<in> J then A i else UNIV)"
     using assms by (simp add:Pi_def set_eq_iff, blast)
   show ?thesis
     using assms
     by (simp add:if_distrib  a measure_Pi_pmf_Pi[OF assms(1)] prod.If_cases[OF assms(1)] Int_absorb1)
 qed
 
 lemma prob_prod_pmf_slice:
   assumes "finite I"
   assumes "i \<in> I"
   shows "measure (measure_pmf (prod_pmf I M)) {\<omega>. P (\<omega> i)} = measure (M i) {\<omega>. P \<omega>}"
   using prob_prod_pmf'[OF assms(1), where J="{i}" and M="M" and A="\<lambda>_. Collect P"]
   by (simp add:assms Pi_def)
 
 definition restrict_dfl where "restrict_dfl f A d = (\<lambda>x. if x \<in> A then f x else d)"
 
 lemma pi_pmf_decompose:
   assumes "finite I"
   shows "Pi_pmf I d M = map_pmf (\<lambda>\<omega>. restrict_dfl (\<lambda>i. \<omega> (f i) i) I d) (Pi_pmf (f ` I) (\<lambda>_. d) (\<lambda>j. Pi_pmf (f -` {j} \<inter> I) d M))"
 proof -
   have fin_F_I:"finite (f ` I)" using assms by blast
 
   have "finite I \<Longrightarrow> ?thesis"
     using fin_F_I
   proof (induction "f ` I" arbitrary: I rule:finite_induct)
     case empty
     then show ?case by (simp add:restrict_dfl_def)
   next
     case (insert x F)
     have a: "(f -` {x} \<inter> I) \<union> (f -` F \<inter> I) = I"
       using insert(4) by blast
     have b: "F = f `  (f -` F \<inter> I) " using insert(2,4)
       by (auto simp add:set_eq_iff image_def vimage_def)
     have c: "finite (f -` F \<inter> I)" using insert by blast
     have d: "\<And>j. j \<in> F \<Longrightarrow> (f -` {j} \<inter> (f -` F \<inter> I)) = (f -` {j} \<inter> I)"
       using insert(4) by blast
 
     have " Pi_pmf I d M = Pi_pmf ((f -` {x} \<inter> I) \<union> (f -` F \<inter> I)) d M"
       by (simp add:a)
     also have "... = map_pmf (\<lambda>(g, h) i. if i \<in> f -` {x} \<inter> I then g i else h i)
       (pair_pmf (Pi_pmf (f -` {x} \<inter> I) d M) (Pi_pmf (f -` F \<inter> I) d M))"
       using insert by (subst Pi_pmf_union) auto
     also have "... = map_pmf (\<lambda>(g,h) i. if f i = x \<and> i \<in> I then g i else if f i \<in> F \<and> i \<in> I then h (f i) i else d)
       (pair_pmf (Pi_pmf (f -` {x} \<inter> I) d M) (Pi_pmf F (\<lambda>_. d) (\<lambda>j. Pi_pmf (f -` {j} \<inter> (f -` F \<inter> I)) d M)))"
       by (simp add:insert(3)[OF b c] map_pmf_comp case_prod_beta' apsnd_def map_prod_def
           pair_map_pmf2 b[symmetric] restrict_dfl_def) (metis fst_conv snd_conv)
     also have "... = map_pmf (\<lambda>(g,h) i. if i \<in> I then (h(x := g)) (f i) i else d)
       (pair_pmf (Pi_pmf (f -` {x} \<inter> I) d M) (Pi_pmf F (\<lambda>_. d) (\<lambda>j. Pi_pmf (f -` {j} \<inter> I) d M)))"
       using insert(4) d
       by (intro arg_cong2[where f="map_pmf"] ext) (auto simp add:case_prod_beta' cong:Pi_pmf_cong)
     also have "... = map_pmf (\<lambda>\<omega> i. if i \<in> I then \<omega> (f i) i else d) (Pi_pmf (insert x F) (\<lambda>_. d) (\<lambda>j. Pi_pmf (f -` {j} \<inter> I) d M))"
       by (simp add:Pi_pmf_insert[OF insert(1,2)] map_pmf_comp case_prod_beta')
     finally show ?case by (simp add:insert(4) restrict_dfl_def)
   qed
   thus ?thesis using assms by blast
 qed
 
 lemma restrict_dfl_iter: "restrict_dfl (restrict_dfl f I d) J d = restrict_dfl f (I \<inter> J) d"
   by (rule ext, simp add:restrict_dfl_def)
 
 lemma indep_vars_restrict':
   assumes "finite I"
   shows "prob_space.indep_vars (Pi_pmf I d M) (\<lambda>_. discrete) (\<lambda>i \<omega>. restrict_dfl \<omega> (f -` {i} \<inter> I) d) (f ` I)"
 proof -
   let ?Q = "(Pi_pmf (f ` I) (\<lambda>_. d) (\<lambda>i. Pi_pmf (I \<inter> f -` {i}) d M))"
   have a:"prob_space.indep_vars ?Q (\<lambda>_. discrete) (\<lambda>i \<omega>. \<omega> i) (f ` I)"
     using assms by (intro indep_vars_Pi_pmf, blast)
   have b: "AE x in measure_pmf ?Q. \<forall>i\<in>f ` I. x i = restrict_dfl (\<lambda>i. x (f i) i) (I \<inter> f -` {i}) d"
     using assms
     by (auto simp add:PiE_dflt_def restrict_dfl_def AE_measure_pmf_iff set_Pi_pmf comp_def Int_commute)
   have "prob_space.indep_vars ?Q (\<lambda>_. discrete) (\<lambda>i x. restrict_dfl (\<lambda>i. x (f i) i) (I \<inter> f -` {i}) d) (f ` I)"
     by (rule prob_space.indep_vars_cong_AE[OF prob_space_measure_pmf b a],  simp)
   thus ?thesis
     using prob_space_measure_pmf
     by (auto intro!:prob_space.indep_vars_distr simp:pi_pmf_decompose[OF assms, where f="f"]
         map_pmf_rep_eq comp_def restrict_dfl_iter Int_commute)
 qed
 
 lemma indep_vars_restrict_intro':
   assumes "finite I"
   assumes "\<And>i \<omega>. i \<in> J \<Longrightarrow> X' i \<omega> = X' i (restrict_dfl \<omega> (f -` {i} \<inter> I) d)"
   assumes "J = f ` I"
   assumes "\<And>\<omega> i. i \<in> J \<Longrightarrow>  X' i \<omega> \<in> space (M' i)"
   shows "prob_space.indep_vars (measure_pmf (Pi_pmf I d p)) M' (\<lambda>i \<omega>. X' i \<omega>) J"
 proof -
   define M where "M \<equiv> measure_pmf (Pi_pmf I d p)"
   interpret prob_space "M"
     using M_def prob_space_measure_pmf by blast
   have "indep_vars (\<lambda>_. discrete) (\<lambda>i x. restrict_dfl x (f -` {i} \<inter> I) d) (f ` I)"
     unfolding M_def  by (rule indep_vars_restrict'[OF assms(1)])
   hence "indep_vars M' (\<lambda>i \<omega>. X' i (restrict_dfl \<omega> ( f -` {i} \<inter> I) d)) (f ` I)"
     using assms(4)
     by (intro indep_vars_compose2[where Y="X'" and N="M'" and M'="\<lambda>_. discrete"])  (auto simp:assms(3))
   hence "indep_vars M' (\<lambda>i \<omega>. X' i \<omega>) (f ` I)"
     using assms(2)[symmetric]
     by (simp add:assms(3) cong:indep_vars_cong)
   thus ?thesis
     unfolding M_def using assms(3) by simp
 qed
 
 lemma
   fixes f :: "'b \<Rightarrow> ('c :: {second_countable_topology,banach,real_normed_field})"
   assumes "finite I"
   assumes "i \<in> I"
   assumes "integrable (measure_pmf (M i)) f"
   shows  integrable_Pi_pmf_slice: "integrable (Pi_pmf I d M) (\<lambda>x. f (x i))"
   and expectation_Pi_pmf_slice: "integral\<^sup>L (Pi_pmf I d M) (\<lambda>x. f (x i)) = integral\<^sup>L (M i) f"
 proof -
   have a:"distr (Pi_pmf I d M) (M i) (\<lambda>\<omega>. \<omega> i) = distr (Pi_pmf I d M) discrete (\<lambda>\<omega>. \<omega> i)"
     by (rule distr_cong, auto)
 
   have b: "measure_pmf.random_variable (M i) borel f"
     using assms(3) by simp
 
   have c:"integrable (distr (Pi_pmf I d M) (M i) (\<lambda>\<omega>. \<omega> i)) f"
     using assms(1,2,3)
     by (subst a, subst map_pmf_rep_eq[symmetric], subst Pi_pmf_component, auto)
 
   show "integrable (Pi_pmf I d M) (\<lambda>x. f (x i))"
     by (rule integrable_distr[where f="f" and M'="M i"])  (auto intro: c)
 
   have "integral\<^sup>L (Pi_pmf I d M) (\<lambda>x. f (x i)) = integral\<^sup>L (distr (Pi_pmf I d M) (M i) (\<lambda>\<omega>. \<omega> i)) f"
     using b by (intro integral_distr[symmetric], auto)
   also have "... =  integral\<^sup>L (map_pmf (\<lambda>\<omega>. \<omega> i) (Pi_pmf I d M)) f"
     by (subst a, subst map_pmf_rep_eq[symmetric], simp)
   also have "... =  integral\<^sup>L (M i) f"
     using assms(1,2) by (simp add: Pi_pmf_component)
   finally show "integral\<^sup>L (Pi_pmf I d M) (\<lambda>x. f (x i)) = integral\<^sup>L (M i) f" by simp
 qed
 
 text \<open>This is an improved version of @{thm [source] "expectation_prod_Pi_pmf"}.
 It works for general normed fields instead of non-negative real functions .\<close>
 
 lemma expectation_prod_Pi_pmf:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: {second_countable_topology,banach,real_normed_field})"
   assumes "finite I"
   assumes "\<And>i. i \<in> I \<Longrightarrow> integrable (measure_pmf (M i)) (f i)"
   shows   "integral\<^sup>L (Pi_pmf I d M) (\<lambda>x. (\<Prod>i \<in> I. f i (x i))) = (\<Prod> i \<in> I. integral\<^sup>L (M i) (f i))"
 proof -
   have a: "prob_space.indep_vars (measure_pmf (Pi_pmf I d M)) (\<lambda>_. borel) (\<lambda>i \<omega>. f i (\<omega> i)) I"
     by (intro prob_space.indep_vars_compose2[where Y="f" and M'="\<lambda>_. discrete"]
         prob_space_measure_pmf indep_vars_Pi_pmf assms(1)) auto
   have "integral\<^sup>L (Pi_pmf I d M) (\<lambda>x. (\<Prod>i \<in> I. f i (x i))) = (\<Prod> i \<in> I. integral\<^sup>L (Pi_pmf I d M) (\<lambda>x. f i (x i)))"
     by (intro prob_space.indep_vars_lebesgue_integral prob_space_measure_pmf assms(1,2)
         a integrable_Pi_pmf_slice) auto
   also have "... = (\<Prod> i \<in> I. integral\<^sup>L (M i) (f i))"
     by (intro prod.cong expectation_Pi_pmf_slice assms(1,2)) auto
   finally show ?thesis by simp
 qed
 
 lemma variance_prod_pmf_slice:
   fixes f :: "'a \<Rightarrow> real"
   assumes "i \<in> I" "finite I"
   assumes "integrable (measure_pmf (M i)) (\<lambda>\<omega>. f \<omega>^2)"
   shows "prob_space.variance (Pi_pmf I d M) (\<lambda>\<omega>. f (\<omega> i)) = prob_space.variance (M i) f"
 proof -
   have a:"integrable (measure_pmf (M i)) f"
     using assms(3) measure_pmf.square_integrable_imp_integrable by auto
   have b:" integrable (measure_pmf (Pi_pmf I d M)) (\<lambda>x. (f (x i))\<^sup>2)"
     by (rule integrable_Pi_pmf_slice[OF assms(2) assms(1)], metis assms(3))
   have c:" integrable (measure_pmf (Pi_pmf I d M)) (\<lambda>x. (f (x i)))"
     by (rule integrable_Pi_pmf_slice[OF assms(2) assms(1)], metis a)
 
   have "measure_pmf.expectation (Pi_pmf I d M) (\<lambda>x. (f (x i))\<^sup>2) - (measure_pmf.expectation (Pi_pmf I d M) (\<lambda>x. f (x i)))\<^sup>2 =
       measure_pmf.expectation (M i) (\<lambda>x. (f x)\<^sup>2) - (measure_pmf.expectation (M i) f)\<^sup>2"
     using assms a b c by ((subst expectation_Pi_pmf_slice[OF assms(2,1)])?, simp)+
 
   thus ?thesis
     using assms a b c by (simp add: measure_pmf.variance_eq)
 qed
 
 lemma Pi_pmf_bind_return:
   assumes "finite I"
   shows "Pi_pmf I d (\<lambda>i. M i \<bind> (\<lambda>x. return_pmf (f i x))) = Pi_pmf I d' M \<bind> (\<lambda>x. return_pmf (\<lambda>i. if i \<in> I then f i (x i) else d))"
   using assms by (simp add: Pi_pmf_bind[where d'="d'"])
 
 lemma pmf_of_set_prod_eq:
   assumes "A \<noteq> {}" "finite A"
   assumes "B \<noteq> {}" "finite B"
   shows  "pmf_of_set (A \<times> B) = pair_pmf (pmf_of_set A) (pmf_of_set B)"
 proof -
   have "indicat_real (A \<times> B) (i, j) = indicat_real A i * indicat_real B j" for i j
     by (cases "i \<in> A"; cases "j \<in> B") auto
   hence "pmf (pmf_of_set (A \<times> B)) (i,j) = pmf (pair_pmf (pmf_of_set A) (pmf_of_set B)) (i,j)"
     for i j using assms by (simp add:pmf_pair)
   thus ?thesis
     by (intro pmf_eqI) auto
 qed
 
 lemma split_pmf_mod_div':
   assumes "a > (0::nat)"
   assumes "b > 0"
   shows "map_pmf (\<lambda>x. (x mod a, x div a)) (pmf_of_set {..<a * b}) = pmf_of_set ({..<a} \<times> {..<b})"
   using assms by (intro map_pmf_of_set_bij_betw bij_betw_prod finite_lessThan)
     (simp add: lessThan_empty_iff)
 
 lemma split_pmf_mod_div:
   assumes "a > (0::nat)"
   assumes "b > 0"
   shows "map_pmf (\<lambda>x. (x mod a, x div a)) (pmf_of_set {..<a * b}) =
     pair_pmf (pmf_of_set {..<a}) (pmf_of_set {..<b})"
   using assms by (auto intro!: pmf_of_set_prod_eq simp add:split_pmf_mod_div')
 
 end