diff -r b4552595b04e -r f6bb31879698 src/HOL/Probability/Hoeffding.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Hoeffding.thy	Fri Feb 19 13:42:12 2021 +0100
@@ -0,0 +1,923 @@
+(*
+  File:    Hoeffding.thy
+  Author:  Manuel Eberl, TU München
+*)
+section \<open>Hoeffding's Lemma and Hoeffding's Inequality\<close>
+theory Hoeffding
+  imports Product_PMF Independent_Family
+begin
+
+text \<open>
+  Hoeffding's inequality shows that a sum of bounded independent random variables is concentrated
+  around its mean, with an exponential decay of the tail probabilities.
+\<close>
+
+subsection \<open>Hoeffding's Lemma\<close>
+
+lemma convex_on_exp: 
+  fixes l :: real
+  assumes "l \<ge> 0"
+  shows   "convex_on UNIV (\<lambda>x. exp(l*x))"
+  using assms
+  by (intro convex_on_realI[where f' = "\<lambda>x. l * exp (l * x)"])
+     (auto intro!: derivative_eq_intros mult_left_mono)
+
+lemma mult_const_minus_self_real_le:
+  fixes x :: real
+  shows "x * (c - x) \<le> c\<^sup>2 / 4"
+proof -
+  have "x * (c - x) = -(x - c / 2)\<^sup>2 + c\<^sup>2 / 4"
+    by (simp add: field_simps power2_eq_square)
+  also have "\<dots> \<le> 0 + c\<^sup>2 / 4"
+    by (intro add_mono) auto
+  finally show ?thesis by simp
+qed
+
+lemma Hoeffdings_lemma_aux:
+  fixes h p :: real
+  assumes "h \<ge> 0" and "p \<ge> 0"
+  defines "L \<equiv> (\<lambda>h. -h * p + ln (1 + p * (exp h - 1)))"
+  shows   "L h \<le> h\<^sup>2 / 8"
+proof (cases "h = 0")
+  case False
+  hence h: "h > 0"
+    using \<open>h \<ge> 0\<close> by simp
+  define L' where "L' = (\<lambda>h. -p + p * exp h / (1 + p * (exp h - 1)))"
+  define L'' where "L'' = (\<lambda>h. -(p\<^sup>2) * exp h * exp h / (1 + p * (exp h - 1))\<^sup>2 +
+                              p * exp h / (1 + p * (exp h - 1)))"
+  define Ls where "Ls = (\<lambda>n. [L, L', L''] ! n)"
+
+  have [simp]: "L 0 = 0" "L' 0 = 0"
+    by (auto simp: L_def L'_def)
+
+  have L': "(L has_real_derivative L' x) (at x)" if "x \<in> {0..h}" for x
+  proof -
+    have "1 + p * (exp x - 1) > 0"
+      using \<open>p \<ge> 0\<close> that by (intro add_pos_nonneg mult_nonneg_nonneg) auto
+    thus ?thesis
+      unfolding L_def L'_def by (auto intro!: derivative_eq_intros)
+  qed
+
+  have L'': "(L' has_real_derivative L'' x) (at x)" if "x \<in> {0..h}" for x
+  proof -
+    have *: "1 + p * (exp x - 1) > 0"
+      using \<open>p \<ge> 0\<close> that by (intro add_pos_nonneg mult_nonneg_nonneg) auto
+    show ?thesis
+      unfolding L'_def L''_def
+      by (insert *, (rule derivative_eq_intros refl | simp)+) (auto simp: divide_simps; algebra)
+  qed
+
+  have diff: "\<forall>m t. m < 2 \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> (Ls m has_real_derivative Ls (Suc m) t) (at t)"
+    using L' L'' by (auto simp: Ls_def nth_Cons split: nat.splits)
+  from Taylor[of 2 Ls L 0 h 0 h, OF _ _ diff]
+    obtain t where t: "t \<in> {0<..<h}" "L h = L'' t * h\<^sup>2 / 2"
+      using \<open>h > 0\<close> by (auto simp: Ls_def lessThan_nat_numeral)
+  define u where "u = p * exp t / (1 + p * (exp t - 1))"
+
+  have "L'' t = u * (1 - u)"
+    by (simp add: L''_def u_def divide_simps; algebra)
+  also have "\<dots> \<le> 1 / 4"
+    using mult_const_minus_self_real_le[of u 1] by simp
+  finally have "L'' t \<le> 1 / 4" .
+
+  note t(2)
+  also have "L'' t * h\<^sup>2 / 2 \<le> (1 / 4) * h\<^sup>2 / 2"
+    using \<open>L'' t \<le> 1 / 4\<close> by (intro mult_right_mono divide_right_mono) auto
+  finally show "L h \<le> h\<^sup>2 / 8" by simp
+qed (auto simp: L_def)
+
+
+locale interval_bounded_random_variable = prob_space +
+  fixes f :: "'a \<Rightarrow> real" and a b :: real
+  assumes random_variable [measurable]: "random_variable borel f"
+  assumes AE_in_interval: "AE x in M. f x \<in> {a..b}"
+begin
+
+lemma integrable [intro]: "integrable M f"
+proof (rule integrable_const_bound)
+  show "AE x in M. norm (f x) \<le> max \<bar>a\<bar> \<bar>b\<bar>"
+    by (intro eventually_mono[OF AE_in_interval]) auto
+qed (fact random_variable)
+
+text \<open>
+  We first show Hoeffding's lemma for distributions whose expectation is 0. The general
+  case will easily follow from this later.
+\<close>
+lemma Hoeffdings_lemma_nn_integral_0:
+  assumes "l > 0" and E0: "expectation f = 0"
+  shows   "nn_integral M (\<lambda>x. exp (l * f x)) \<le> ennreal (exp (l\<^sup>2 * (b - a)\<^sup>2 / 8))"
+proof (cases "AE x in M. f x = 0")
+  case True
+  hence "nn_integral M (\<lambda>x. exp (l * f x)) = nn_integral M (\<lambda>x. ennreal 1)"
+    by (intro nn_integral_cong_AE) auto
+  also have "\<dots> = ennreal (expectation (\<lambda>_. 1))"
+    by (intro nn_integral_eq_integral) auto
+  finally show ?thesis by (simp add: prob_space)
+next
+  case False
+  have "a < 0"
+  proof (rule ccontr)
+    assume a: "\<not>(a < 0)"
+    have "AE x in M. f x = 0"
+    proof (subst integral_nonneg_eq_0_iff_AE [symmetric])
+      show "AE x in M. f x \<ge> 0"
+        using AE_in_interval by eventually_elim (use a in auto)
+    qed (use E0 in \<open>auto simp: id_def integrable\<close>)
+    with False show False by contradiction
+  qed
+
+  have "b > 0"
+  proof (rule ccontr)
+    assume b: "\<not>(b > 0)"
+    have "AE x in M. -f x = 0"
+    proof (subst integral_nonneg_eq_0_iff_AE [symmetric])
+      show "AE x in M. -f x \<ge> 0"
+        using AE_in_interval by eventually_elim (use b in auto)
+    qed (use E0 in \<open>auto simp: id_def integrable\<close>)
+    with False show False by simp
+  qed
+    
+  have "a < b"
+    using \<open>a < 0\<close> \<open>b > 0\<close> by linarith
+
+  define p where "p = -a / (b - a)"
+  define L where "L = (\<lambda>t. -t* p + ln (1 - p + p * exp t))"
+  define z where "z = l * (b - a)"
+  have "z > 0"
+    unfolding z_def using \<open>a < b\<close> \<open>l > 0\<close> by auto
+  have "p > 0"
+    using \<open>a < 0\<close> \<open>a < b\<close> unfolding p_def by (intro divide_pos_pos) auto
+
+  have "(\<integral>\<^sup>+x. exp (l * f x) \<partial>M) \<le>
+        (\<integral>\<^sup>+x. (b - f x) / (b - a) * exp (l * a) + (f x - a) / (b - a) * exp (l * b) \<partial>M)"
+  proof (intro nn_integral_mono_AE eventually_mono[OF AE_in_interval] ennreal_leI)
+    fix x assume x: "f x \<in> {a..b}"
+    define y where "y = (b - f x) / (b-a)"
+    have y: "y \<in> {0..1}"
+      using x \<open>a < b\<close> by (auto simp: y_def)
+    have conv: "convex_on UNIV (\<lambda>x. exp(l*x))"
+      using \<open>l > 0\<close> by (intro convex_on_exp) auto
+    have "exp (l * ((1 - y) *\<^sub>R b + y *\<^sub>R a)) \<le> (1 - y) * exp (l * b) + y * exp (l * a)"
+      using y \<open>l > 0\<close> by (intro convex_onD[OF convex_on_exp]) auto
+    also have "(1 - y) *\<^sub>R b + y *\<^sub>R a = f x"
+      using \<open>a < b\<close> by (simp add: y_def divide_simps) (simp add: algebra_simps)?
+    also have "1 - y = (f x - a) / (b - a)"
+      using \<open>a < b\<close> by (simp add: field_simps y_def)
+    finally show "exp (l * f x) \<le> (b - f x) / (b - a) * exp (l*a) + (f x - a)/(b-a) * exp (l*b)"
+      by (simp add: y_def)
+  qed
+  also have "\<dots> = (\<integral>\<^sup>+x. ennreal (b - f x) * exp (l * a) / (b - a) +
+                        ennreal (f x - a) * exp (l * b) / (b - a) \<partial>M)"
+    using \<open>a < 0\<close> \<open>b > 0\<close>
+    by (intro nn_integral_cong_AE eventually_mono[OF AE_in_interval])
+       (simp add: ennreal_plus ennreal_mult flip: divide_ennreal)
+  also have "\<dots> = ((\<integral>\<^sup>+ x. ennreal (b - f x) \<partial>M) * ennreal (exp (l * a)) +
+                   (\<integral>\<^sup>+ x. ennreal (f x - a) \<partial>M) * ennreal (exp (l * b))) / ennreal (b - a)"
+    by (simp add: nn_integral_add nn_integral_divide nn_integral_multc add_divide_distrib_ennreal)
+  also have "(\<integral>\<^sup>+ x. ennreal (b - f x) \<partial>M) = ennreal (expectation (\<lambda>x. b - f x))"
+    by (intro nn_integral_eq_integral Bochner_Integration.integrable_diff
+              eventually_mono[OF AE_in_interval] integrable_const integrable) auto
+  also have "expectation (\<lambda>x. b - f x) = b"
+    using assms by (subst Bochner_Integration.integral_diff) (auto simp: prob_space)
+  also have "(\<integral>\<^sup>+ x. ennreal (f x - a) \<partial>M) = ennreal (expectation (\<lambda>x. f x - a))"
+    by (intro nn_integral_eq_integral Bochner_Integration.integrable_diff
+              eventually_mono[OF AE_in_interval] integrable_const integrable) auto
+  also have "expectation (\<lambda>x. f x - a) = (-a)"
+    using assms by (subst Bochner_Integration.integral_diff) (auto simp: prob_space)
+  also have "(ennreal b * (exp (l * a)) + ennreal (-a) * (exp (l * b))) / (b - a) =
+             ennreal (b * exp (l * a) - a * exp (l * b)) / ennreal (b - a)"
+    using \<open>a < 0\<close> \<open>b > 0\<close>
+    by (simp flip: ennreal_mult ennreal_plus add: mult_nonpos_nonneg divide_ennreal mult_mono)
+  also have "b * exp (l * a) - a * exp (l * b) = exp (L z) * (b - a)"
+  proof -
+    have pos: "1 - p + p * exp z > 0"
+    proof -
+      have "exp z > 1" using \<open>l > 0\<close> and \<open>a < b\<close>
+        by (subst one_less_exp_iff) (auto simp: z_def intro!: mult_pos_pos)
+      hence "(exp z - 1) * p \<ge> 0"
+        unfolding p_def using \<open>a < 0\<close> and \<open>a < b\<close>
+        by (intro mult_nonneg_nonneg divide_nonneg_pos) auto
+      thus ?thesis
+        by (simp add: algebra_simps)
+    qed
+
+    have "exp (L z) * (b - a) = exp (-z * p) * (1 - p + p * exp z) * (b - a)"
+      using pos by (simp add: exp_add L_def exp_diff exp_minus divide_simps)
+    also have "\<dots> = b * exp (l * a) - a * exp (l * b)" using \<open>a < b\<close>
+      by (simp add: p_def z_def divide_simps) (simp add:  exp_diff algebra_simps)?
+    finally show ?thesis by simp
+  qed
+  also have "ennreal (exp (L z) * (b - a)) / ennreal (b - a) = ennreal (exp (L z))"
+    using \<open>a < b\<close> by (simp add: divide_ennreal)
+  also have "L z = -z * p + ln (1 + p * (exp z - 1))"
+    by (simp add: L_def algebra_simps)
+  also have "\<dots> \<le> z\<^sup>2 / 8"
+    unfolding L_def by (rule Hoeffdings_lemma_aux[where p = p]) (use \<open>z > 0\<close> \<open>p > 0\<close> in simp_all)
+  hence "ennreal (exp (-z * p + ln (1 + p * (exp z - 1)))) \<le> ennreal (exp (z\<^sup>2 / 8))"
+    by (intro ennreal_leI) auto
+  finally show ?thesis
+    by (simp add: z_def power_mult_distrib)
+qed
+
+context
+begin
+
+interpretation shift: interval_bounded_random_variable M "\<lambda>x. f x - \<mu>" "a - \<mu>" "b - \<mu>"
+  rewrites "b - \<mu> - (a - \<mu>) \<equiv> b - a"
+  by unfold_locales (auto intro!: eventually_mono[OF AE_in_interval])
+
+lemma expectation_shift: "expectation (\<lambda>x. f x - expectation f) = 0"
+  by (subst Bochner_Integration.integral_diff) (auto simp: integrable prob_space)
+
+lemmas Hoeffdings_lemma_nn_integral = shift.Hoeffdings_lemma_nn_integral_0[OF _ expectation_shift]
+
+end
+
+end
+
+
+
+subsection \<open>Hoeffding's Inequality\<close>
+
+text \<open>
+  Consider \<open>n\<close> independent real random variables $X_1, \ldots, X_n$ that each almost surely lie
+  in a compact interval $[a_i, b_i]$. Hoeffding's inequality states that the distribution of the
+  sum of the $X_i$ is tightly concentrated around the sum of the expected values: the probability
+  of it being above or below the sum of the expected values by more than some \<open>\<epsilon>\<close> decreases
+  exponentially with \<open>\<epsilon>\<close>.
+\<close>
+
+locale indep_interval_bounded_random_variables = prob_space +
+  fixes I :: "'b set" and X :: "'b \<Rightarrow> 'a \<Rightarrow> real"
+  fixes a b :: "'b \<Rightarrow> real"
+  assumes fin: "finite I"
+  assumes indep: "indep_vars (\<lambda>_. borel) X I"
+  assumes AE_in_interval: "\<And>i. i \<in> I \<Longrightarrow> AE x in M. X i x \<in> {a i..b i}"
+begin
+
+lemma random_variable [measurable]:
+  assumes i: "i \<in> I"
+  shows "random_variable borel (X i)"
+  using i indep unfolding indep_vars_def by blast
+
+lemma bounded_random_variable [intro]:
+  assumes i: "i \<in> I"
+  shows   "interval_bounded_random_variable M (X i) (a i) (b i)"
+  by unfold_locales (use AE_in_interval[OF i] i in auto)
+
+end
+
+
+locale Hoeffding_ineq = indep_interval_bounded_random_variables +
+  fixes \<mu> :: real
+  defines "\<mu> \<equiv> (\<Sum>i\<in>I. expectation (X i))"
+begin
+
+theorem%important Hoeffding_ineq_ge:
+  assumes "\<epsilon> \<ge> 0"
+  assumes "(\<Sum>i\<in>I. (b i - a i)\<^sup>2) > 0"
+  shows   "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> + \<epsilon>} \<le> exp (-2 * \<epsilon>\<^sup>2 / (\<Sum>i\<in>I. (b i - a i)\<^sup>2))"
+proof (cases "\<epsilon> = 0")
+  case [simp]: True
+  have "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> + \<epsilon>} \<le> 1"
+    by simp
+  thus ?thesis by simp
+next
+  case False
+  with \<open>\<epsilon> \<ge> 0\<close> have \<epsilon>: "\<epsilon> > 0"
+    by auto
+
+  define d where "d = (\<Sum>i\<in>I. (b i - a i)\<^sup>2)"
+  define l :: real where "l = 4 * \<epsilon> / d"
+  have d: "d > 0"
+    using assms by (simp add: d_def)
+  have l: "l > 0"
+    using \<epsilon> d by (simp add: l_def)
+  define \<mu>' where "\<mu>' = (\<lambda>i. expectation (X i))"
+
+  have "{x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> + \<epsilon>} = {x\<in>space M. (\<Sum>i\<in>I. X i x) - \<mu> \<ge> \<epsilon>}"
+    by (simp add: algebra_simps)
+  hence "ennreal (prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> + \<epsilon>}) = emeasure M \<dots>"
+    by (simp add: emeasure_eq_measure)
+  also have "\<dots> \<le> ennreal (exp (-l*\<epsilon>)) * (\<integral>\<^sup>+x\<in>space M. exp (l * ((\<Sum>i\<in>I. X i x) - \<mu>)) \<partial>M)"
+    by (intro Chernoff_ineq_nn_integral_ge l) auto
+  also have "(\<lambda>x. (\<Sum>i\<in>I. X i x) - \<mu>) = (\<lambda>x. (\<Sum>i\<in>I. X i x - \<mu>' i))"
+    by (simp add: \<mu>_def sum_subtractf \<mu>'_def)
+  also have "(\<integral>\<^sup>+x\<in>space M. exp (l * ((\<Sum>i\<in>I. X i x - \<mu>' i))) \<partial>M) =
+             (\<integral>\<^sup>+x. (\<Prod>i\<in>I. ennreal (exp (l * (X i x - \<mu>' i)))) \<partial>M)"
+    by (intro nn_integral_cong)
+       (simp_all add: sum_distrib_left ring_distribs exp_diff exp_sum fin prod_ennreal)
+  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+x. ennreal (exp (l * (X i x - \<mu>' i))) \<partial>M)"
+    by (intro indep_vars_nn_integral fin indep_vars_compose2[OF indep]) auto
+  also have "ennreal (exp (-l * \<epsilon>)) * \<dots> \<le>
+               ennreal (exp (-l * \<epsilon>)) * (\<Prod>i\<in>I. ennreal (exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8)))"
+  proof (intro mult_left_mono prod_mono_ennreal)
+    fix i assume i: "i \<in> I"
+    from i interpret interval_bounded_random_variable M "X i" "a i" "b i" ..
+    show "(\<integral>\<^sup>+x. ennreal (exp (l * (X i x - \<mu>' i))) \<partial>M) \<le> ennreal (exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8))"
+      unfolding \<mu>'_def by (rule Hoeffdings_lemma_nn_integral) fact+
+  qed auto
+  also have "\<dots> = ennreal (exp (-l*\<epsilon>) * (\<Prod>i\<in>I. exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8)))"
+    by (simp add: prod_ennreal prod_nonneg flip: ennreal_mult)
+  also have "exp (-l*\<epsilon>) * (\<Prod>i\<in>I. exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8)) = exp (d * l\<^sup>2 / 8 - l * \<epsilon>)"
+    by (simp add: exp_diff exp_minus sum_divide_distrib sum_distrib_left
+                  sum_distrib_right exp_sum fin divide_simps mult_ac d_def)
+  also have "d * l\<^sup>2 / 8 - l * \<epsilon> = -2 * \<epsilon>\<^sup>2 / d"
+    using d by (simp add: l_def field_simps power2_eq_square)
+  finally show ?thesis
+    by (subst (asm) ennreal_le_iff) (simp_all add: d_def)
+qed
+
+corollary Hoeffding_ineq_le:
+  assumes \<epsilon>: "\<epsilon> \<ge> 0"
+  assumes "(\<Sum>i\<in>I. (b i - a i)\<^sup>2) > 0"
+  shows   "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<le> \<mu> - \<epsilon>} \<le> exp (-2 * \<epsilon>\<^sup>2 / (\<Sum>i\<in>I. (b i - a i)\<^sup>2))"
+proof -
+  interpret flip: Hoeffding_ineq M I "\<lambda>i x. -X i x" "\<lambda>i. -b i" "\<lambda>i. -a i" "-\<mu>"
+  proof unfold_locales
+    fix i assume "i \<in> I"
+    then interpret interval_bounded_random_variable M "X i" "a i" "b i" ..
+    show "AE x in M. - X i x \<in> {- b i..- a i}"
+      by (intro eventually_mono[OF AE_in_interval]) auto
+  qed (auto simp: fin \<mu>_def sum_negf intro: indep_vars_compose2[OF indep])
+
+  have "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<le> \<mu> - \<epsilon>} = prob {x\<in>space M. (\<Sum>i\<in>I. -X i x) \<ge> -\<mu> + \<epsilon>}"
+    by (simp add: sum_negf algebra_simps)
+  also have "\<dots> \<le> exp (- 2 * \<epsilon>\<^sup>2 / (\<Sum>i\<in>I. (b i - a i)\<^sup>2))"
+    using flip.Hoeffding_ineq_ge[OF \<epsilon>] assms(2) by simp
+  finally show ?thesis .
+qed
+
+corollary Hoeffding_ineq_abs_ge:
+  assumes \<epsilon>: "\<epsilon> \<ge> 0"
+  assumes "(\<Sum>i\<in>I. (b i - a i)\<^sup>2) > 0"
+  shows   "prob {x\<in>space M. \<bar>(\<Sum>i\<in>I. X i x) - \<mu>\<bar> \<ge> \<epsilon>} \<le> 2 * exp (-2 * \<epsilon>\<^sup>2 / (\<Sum>i\<in>I. (b i - a i)\<^sup>2))"
+proof -
+  have "{x\<in>space M. \<bar>(\<Sum>i\<in>I. X i x) - \<mu>\<bar> \<ge> \<epsilon>} =
+        {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> + \<epsilon>} \<union> {x\<in>space M. (\<Sum>i\<in>I. X i x) \<le> \<mu> - \<epsilon>}"
+    by auto
+  also have "prob \<dots> \<le> prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> + \<epsilon>} +
+                       prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<le> \<mu> - \<epsilon>}"
+    by (intro measure_Un_le) auto
+  also have "\<dots> \<le> exp (-2 * \<epsilon>\<^sup>2 / (\<Sum>i\<in>I. (b i - a i)\<^sup>2)) + exp (-2 * \<epsilon>\<^sup>2 / (\<Sum>i\<in>I. (b i - a i)\<^sup>2))"
+    by (intro add_mono Hoeffding_ineq_ge Hoeffding_ineq_le assms)
+  finally show ?thesis by simp
+qed
+
+end
+
+
+subsection \<open>Hoeffding's inequality for i.i.d. bounded random variables\<close>
+
+text \<open>
+  If we have \<open>n\<close> even identically-distributed random variables, the statement of Hoeffding's
+  lemma simplifies a bit more: it shows that the probability that the average of the $X_i$
+  is more than \<open>\<epsilon>\<close> above the expected value is no greater than $e^{\frac{-2ny^2}{(b-a)^2}}$.
+
+  This essentially gives us a more concrete version of the weak law of large numbers: the law
+  states that the probability vanishes for \<open>n \<rightarrow> \<infinity>\<close> for any \<open>\<epsilon> > 0\<close>. Unlike Hoeffding's inequality,
+  it does not assume the variables to have bounded support, but it does not provide concrete bounds.
+\<close>
+
+locale iid_interval_bounded_random_variables = prob_space +
+  fixes I :: "'b set" and X :: "'b \<Rightarrow> 'a \<Rightarrow> real" and Y :: "'a \<Rightarrow> real"
+  fixes a b :: real
+  assumes fin: "finite I"
+  assumes indep: "indep_vars (\<lambda>_. borel) X I"
+  assumes distr_X: "i \<in> I \<Longrightarrow> distr M borel (X i) = distr M borel Y"
+  assumes rv_Y [measurable]: "random_variable borel Y"
+  assumes AE_in_interval: "AE x in M. Y x \<in> {a..b}"
+begin
+
+lemma random_variable [measurable]:
+  assumes i: "i \<in> I"
+  shows "random_variable borel (X i)"
+  using i indep unfolding indep_vars_def by blast
+
+sublocale X: indep_interval_bounded_random_variables M I X "\<lambda>_. a" "\<lambda>_. b"
+proof
+  fix i assume i: "i \<in> I"
+  have "AE x in M. Y x \<in> {a..b}"
+    by (fact AE_in_interval)
+  also have "?this \<longleftrightarrow> (AE x in distr M borel Y. x \<in> {a..b})"
+    by (subst AE_distr_iff) auto
+  also have "distr M borel Y = distr M borel (X i)"
+    using i by (simp add: distr_X)
+  also have "(AE x in \<dots>. x \<in> {a..b}) \<longleftrightarrow> (AE x in M. X i x \<in> {a..b})"
+    using i by (subst AE_distr_iff) auto
+  finally show "AE x in M. X i x \<in> {a..b}" .
+qed (simp_all add: fin indep)
+
+lemma expectation_X [simp]:
+  assumes i: "i \<in> I"
+  shows "expectation (X i) = expectation Y"
+proof -
+  have "expectation (X i) = lebesgue_integral (distr M borel (X i)) (\<lambda>x. x)"
+    using i by (intro integral_distr [symmetric]) auto
+  also have "distr M borel (X i) = distr M borel Y"
+    using i by (rule distr_X)
+  also have "lebesgue_integral \<dots> (\<lambda>x. x) = expectation Y"
+    by (rule integral_distr) auto
+  finally show "expectation (X i) = expectation Y" .
+qed
+
+end
+
+
+locale Hoeffding_ineq_iid = iid_interval_bounded_random_variables +
+  fixes \<mu> :: real
+  defines "\<mu> \<equiv> expectation Y"
+begin
+
+sublocale X: Hoeffding_ineq M I X "\<lambda>_. a" "\<lambda>_. b" "real (card I) * \<mu>"
+  by unfold_locales (simp_all add: \<mu>_def)
+
+corollary
+  assumes \<epsilon>: "\<epsilon> \<ge> 0"
+  assumes "a < b" "I \<noteq> {}"
+  defines "n \<equiv> card I"
+  shows   Hoeffding_ineq_ge:
+            "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> n * \<mu> + \<epsilon>} \<le>
+               exp (-2 * \<epsilon>\<^sup>2 / (n * (b - a)\<^sup>2))" (is ?le)
+    and   Hoeffding_ineq_le:
+            "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) \<le> n * \<mu> - \<epsilon>} \<le>
+               exp (-2 * \<epsilon>\<^sup>2 / (n * (b - a)\<^sup>2))" (is ?ge)
+    and   Hoeffding_ineq_abs_ge:
+            "prob {x\<in>space M. \<bar>(\<Sum>i\<in>I. X i x) - n * \<mu>\<bar> \<ge> \<epsilon>} \<le>
+               2 * exp (-2 * \<epsilon>\<^sup>2 / (n * (b - a)\<^sup>2))" (is ?abs_ge)
+proof -
+  have pos: "(\<Sum>i\<in>I. (b - a)\<^sup>2) > 0"
+    using \<open>a < b\<close> \<open>I \<noteq> {}\<close> fin by (intro sum_pos) auto
+  show ?le
+    using X.Hoeffding_ineq_ge[OF \<epsilon> pos] by (simp add: n_def)
+  show ?ge
+    using X.Hoeffding_ineq_le[OF \<epsilon> pos] by (simp add: n_def)
+  show ?abs_ge
+    using X.Hoeffding_ineq_abs_ge[OF \<epsilon> pos] by (simp add: n_def)
+qed
+
+lemma 
+  assumes \<epsilon>: "\<epsilon> \<ge> 0"
+  assumes "a < b" "I \<noteq> {}"
+  defines "n \<equiv> card I"
+  shows   Hoeffding_ineq_ge':
+            "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) / n \<ge> \<mu> + \<epsilon>} \<le>
+               exp (-2 * n * \<epsilon>\<^sup>2 / (b - a)\<^sup>2)" (is ?ge)
+    and   Hoeffding_ineq_le':
+            "prob {x\<in>space M. (\<Sum>i\<in>I. X i x) / n \<le> \<mu> - \<epsilon>} \<le>
+               exp (-2 * n * \<epsilon>\<^sup>2 / (b - a)\<^sup>2)" (is ?le)
+    and   Hoeffding_ineq_abs_ge':
+            "prob {x\<in>space M. \<bar>(\<Sum>i\<in>I. X i x) / n - \<mu>\<bar> \<ge> \<epsilon>} \<le>
+               2 * exp (-2 * n * \<epsilon>\<^sup>2 / (b - a)\<^sup>2)" (is ?abs_ge)
+proof -
+  have "n > 0"
+    using assms fin by (auto simp: field_simps)
+  have \<epsilon>': "\<epsilon> * n \<ge> 0"
+    using \<open>n > 0\<close> \<open>\<epsilon> \<ge> 0\<close> by auto
+  have eq: "- (2 * (\<epsilon> * real n)\<^sup>2 / (real (card I) * (b - a)\<^sup>2)) =
+            - (2 * real n * \<epsilon>\<^sup>2 / (b - a)\<^sup>2)"
+    using \<open>n > 0\<close> by (simp add: power2_eq_square divide_simps n_def)
+
+  have "{x\<in>space M. (\<Sum>i\<in>I. X i x) / n \<ge> \<mu> + \<epsilon>} =
+        {x\<in>space M. (\<Sum>i\<in>I. X i x) \<ge> \<mu> * n + \<epsilon> * n}"
+    using \<open>n > 0\<close> by (intro Collect_cong conj_cong refl) (auto simp: field_simps)
+  with Hoeffding_ineq_ge[OF \<epsilon>' \<open>a < b\<close> \<open>I \<noteq> {}\<close>] \<open>n > 0\<close> eq show ?ge
+    by (simp add: n_def mult_ac)
+
+  have "{x\<in>space M. (\<Sum>i\<in>I. X i x) / n \<le> \<mu> - \<epsilon>} =
+        {x\<in>space M. (\<Sum>i\<in>I. X i x) \<le> \<mu> * n - \<epsilon> * n}"
+    using \<open>n > 0\<close> by (intro Collect_cong conj_cong refl) (auto simp: field_simps)
+  with Hoeffding_ineq_le[OF \<epsilon>' \<open>a < b\<close> \<open>I \<noteq> {}\<close>] \<open>n > 0\<close> eq show ?le
+    by (simp add: n_def mult_ac)
+
+  have "{x\<in>space M. \<bar>(\<Sum>i\<in>I. X i x) / n - \<mu>\<bar> \<ge> \<epsilon>} =
+        {x\<in>space M. \<bar>(\<Sum>i\<in>I. X i x) - \<mu> * n\<bar> \<ge> \<epsilon> * n}"
+    using \<open>n > 0\<close> by (intro Collect_cong conj_cong refl) (auto simp: field_simps)
+  with Hoeffding_ineq_abs_ge[OF \<epsilon>' \<open>a < b\<close> \<open>I \<noteq> {}\<close>] \<open>n > 0\<close> eq show ?abs_ge
+    by (simp add: n_def mult_ac)
+qed
+
+end
+
+
+subsection \<open>Hoeffding's Inequality for the Binomial distribution\<close>
+
+text \<open>
+  We can now apply Hoeffding's inequality to the Binomial distribution, which can be seen
+  as the sum of \<open>n\<close> i.i.d. coin flips (the support of each of which is contained in $[0,1]$).
+\<close>
+
+locale binomial_distribution =
+  fixes n :: nat and p :: real
+  assumes p: "p \<in> {0..1}"
+begin
+
+context
+  fixes coins :: "(nat \<Rightarrow> bool) pmf" and \<mu>
+  assumes n: "n > 0"
+  defines "coins \<equiv> Pi_pmf {..<n} False (\<lambda>_. bernoulli_pmf p)"
+begin
+
+lemma coins_component:
+  assumes i: "i < n"
+  shows   "distr (measure_pmf coins) borel (\<lambda>f. if f i then 1 else 0) =
+             distr (measure_pmf (bernoulli_pmf p)) borel (\<lambda>b. if b then 1 else 0)"
+proof -
+  have "distr (measure_pmf coins) borel (\<lambda>f. if f i then 1 else 0) =
+        distr (measure_pmf (map_pmf (\<lambda>f. f i) coins)) borel (\<lambda>b. if b then 1 else 0)"
+    unfolding map_pmf_rep_eq by (subst distr_distr) (auto simp: o_def)
+  also have "map_pmf (\<lambda>f. f i) coins = bernoulli_pmf p"
+    unfolding coins_def using i by (subst Pi_pmf_component) auto
+  finally show ?thesis
+    unfolding map_pmf_rep_eq .
+qed
+
+lemma prob_binomial_pmf_conv_coins:
+  "measure_pmf.prob (binomial_pmf n p) {x. P (real x)} = 
+   measure_pmf.prob coins {x. P (\<Sum>i<n. if x i then 1 else 0)}"
+proof -
+  have eq1: "(\<Sum>i<n. if x i then 1 else 0) = real (card {i\<in>{..<n}. x i})" for x
+  proof -
+    have "(\<Sum>i<n. if x i then 1 else (0::real)) = (\<Sum>i\<in>{i\<in>{..<n}. x i}. 1)"
+      by (intro sum.mono_neutral_cong_right) auto
+    thus ?thesis by simp
+  qed
+  have eq2: "binomial_pmf n p = map_pmf (\<lambda>v. card {i\<in>{..<n}. v i}) coins"
+    unfolding coins_def by (rule binomial_pmf_altdef') (use p in auto)
+  show ?thesis
+    by (subst eq2) (simp_all add: eq1)
+qed
+
+interpretation Hoeffding_ineq_iid
+  coins "{..<n}" "\<lambda>i f. if f i then 1 else 0" "\<lambda>f. if f 0 then 1 else 0" 0 1 p
+proof unfold_locales
+  show "prob_space.indep_vars (measure_pmf coins) (\<lambda>_. borel) (\<lambda>i f. if f i then 1 else 0) {..<n}"
+    unfolding coins_def
+    by (intro prob_space.indep_vars_compose2[OF _ indep_vars_Pi_pmf])
+       (auto simp: measure_pmf.prob_space_axioms)
+next
+  have "measure_pmf.expectation coins (\<lambda>f. if f 0 then 1 else 0 :: real) =
+        measure_pmf.expectation (map_pmf (\<lambda>f. f 0) coins) (\<lambda>b. if b then 1 else 0 :: real)"
+    by (simp add: coins_def)
+  also have "map_pmf (\<lambda>f. f 0) coins = bernoulli_pmf p"
+    using n by (simp add: coins_def Pi_pmf_component)
+  also have "measure_pmf.expectation \<dots> (\<lambda>b. if b then 1 else 0) = p"
+    using p by simp
+  finally show "p \<equiv> measure_pmf.expectation coins (\<lambda>f. if f 0 then 1 else 0)" by simp
+qed (auto simp: coins_component)
+
+corollary
+  fixes \<epsilon> :: real
+  assumes \<epsilon>: "\<epsilon> \<ge> 0"
+  shows prob_ge: "measure_pmf.prob (binomial_pmf n p) {x. x \<ge> n * p + \<epsilon>} \<le> exp (-2 * \<epsilon>\<^sup>2 / n)"
+    and prob_le: "measure_pmf.prob (binomial_pmf n p) {x. x \<le> n * p - \<epsilon>} \<le> exp (-2 * \<epsilon>\<^sup>2 / n)"
+    and prob_abs_ge:
+          "measure_pmf.prob (binomial_pmf n p) {x. \<bar>x - n * p\<bar> \<ge> \<epsilon>} \<le> 2 * exp (-2 * \<epsilon>\<^sup>2 / n)"
+proof -
+  have [simp]: "{..<n} \<noteq> {}"
+    using n by auto
+  show "measure_pmf.prob (binomial_pmf n p) {x. x \<ge> n * p + \<epsilon>} \<le> exp (-2 * \<epsilon>\<^sup>2 / n)"
+    using Hoeffding_ineq_ge[of \<epsilon>] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all)
+  show "measure_pmf.prob (binomial_pmf n p) {x. x \<le> n * p - \<epsilon>} \<le> exp (-2 * \<epsilon>\<^sup>2 / n)"
+    using Hoeffding_ineq_le[of \<epsilon>] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all)
+  show "measure_pmf.prob (binomial_pmf n p) {x. \<bar>x - n * p\<bar> \<ge> \<epsilon>} \<le> 2 *  exp (-2 * \<epsilon>\<^sup>2 / n)"
+    using Hoeffding_ineq_abs_ge[of \<epsilon>]
+    by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all)
+qed
+
+corollary
+  fixes \<epsilon> :: real
+  assumes \<epsilon>: "\<epsilon> \<ge> 0"
+  shows prob_ge': "measure_pmf.prob (binomial_pmf n p) {x. x / n \<ge> p + \<epsilon>} \<le> exp (-2 * n * \<epsilon>\<^sup>2)"
+    and prob_le': "measure_pmf.prob (binomial_pmf n p) {x. x / n \<le> p - \<epsilon>} \<le> exp (-2 * n * \<epsilon>\<^sup>2)"
+    and prob_abs_ge':
+          "measure_pmf.prob (binomial_pmf n p) {x. \<bar>x / n - p\<bar> \<ge> \<epsilon>} \<le> 2 * exp (-2 * n * \<epsilon>\<^sup>2)"
+proof -
+  have [simp]: "{..<n} \<noteq> {}"
+    using n by auto
+  show "measure_pmf.prob (binomial_pmf n p) {x. x / n \<ge> p + \<epsilon>} \<le> exp (-2 * n * \<epsilon>\<^sup>2)"
+    using Hoeffding_ineq_ge'[of \<epsilon>] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all)
+  show "measure_pmf.prob (binomial_pmf n p) {x. x / n \<le> p - \<epsilon>} \<le> exp (-2 * n * \<epsilon>\<^sup>2)"
+    using Hoeffding_ineq_le'[of \<epsilon>] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all)
+  show "measure_pmf.prob (binomial_pmf n p) {x. \<bar>x / n - p\<bar> \<ge> \<epsilon>} \<le> 2 * exp (-2 * n * \<epsilon>\<^sup>2)"
+    using Hoeffding_ineq_abs_ge'[of \<epsilon>]
+    by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all)
+qed
+
+end
+
+end
+
+
+subsection \<open>Tail bounds for the negative binomial distribution\<close>
+
+text \<open>
+  Since the tail probabilities of a negative Binomial distribution are equal to the
+  tail probabilities of some Binomial distribution, we can obtain tail bounds for the
+  negative Binomial distribution through the Hoeffding tail bounds for the Binomial
+  distribution.
+\<close>
+
+context
+  fixes p q :: real
+  assumes p: "p \<in> {0<..<1}"
+  defines "q \<equiv> 1 - p"
+begin
+
+lemma prob_neg_binomial_pmf_ge_bound:
+  fixes n :: nat and k :: real
+  defines "\<mu> \<equiv> real n * q / p"
+  assumes k: "k \<ge> 0"
+  shows "measure_pmf.prob (neg_binomial_pmf n p) {x. real x \<ge> \<mu> + k}
+         \<le> exp (- 2 * p ^ 3 * k\<^sup>2 / (n + p * k))"
+proof -
+  consider "n = 0" | "p = 1" | "n > 0" "p \<noteq> 1"
+    by blast
+  thus ?thesis
+  proof cases
+    assume [simp]: "n = 0"
+    show ?thesis using k
+      by (simp add: indicator_def \<mu>_def)
+  next
+    assume [simp]: "p = 1"
+    show ?thesis using k
+      by (auto simp add: indicator_def \<mu>_def q_def)
+  next
+    assume n: "n > 0" and "p \<noteq> 1"
+    from \<open>p \<noteq> 1\<close> and p have p: "p \<in> {0<..<1}"
+      by auto
+    from p have q: "q \<in> {0<..<1}"
+      by (auto simp: q_def)
+
+    define k1 where "k1 = \<mu> + k"
+    have k1: "k1 \<ge> \<mu>"
+      using k by (simp add: k1_def)
+    have "k1 > 0"
+      by (rule less_le_trans[OF _ k1]) (use p n in \<open>auto simp: q_def \<mu>_def\<close>)
+  
+    define k1' where "k1' = nat (ceiling k1)"
+    have "\<mu> \<ge> 0" using p
+      by (auto simp: \<mu>_def q_def)
+    have "\<not>(x < k1') \<longleftrightarrow> real x \<ge> k1" for x
+      unfolding k1'_def by linarith
+    hence eq: "UNIV - {..<k1'} = {x. x \<ge> k1}"
+      by auto
+    hence "measure_pmf.prob (neg_binomial_pmf n p) {n. n \<ge> k1} =
+          1 - measure_pmf.prob (neg_binomial_pmf n p) {..<k1'}"
+      using measure_pmf.prob_compl[of "{..<k1'}" "neg_binomial_pmf n p"] by simp
+    also have "measure_pmf.prob (neg_binomial_pmf n p) {..<k1'} =
+               measure_pmf.prob (binomial_pmf (n + k1' - 1) q) {..<k1'}"
+      unfolding q_def using p by (intro prob_neg_binomial_pmf_lessThan) auto
+    also have "1 - \<dots> = measure_pmf.prob (binomial_pmf (n + k1' - 1) q) {n. n \<ge> k1}"
+      using measure_pmf.prob_compl[of "{..<k1'}" "binomial_pmf (n + k1' - 1) q"] eq by simp
+    also have "{x. real x \<ge> k1} = {x. x \<ge> real (n + k1' - 1) * q + (k1 - real (n + k1' - 1) * q)}"
+      by simp
+    also have "measure_pmf.prob (binomial_pmf (n + k1' - 1) q) \<dots> \<le>
+                 exp (-2 * (k1 - real (n + k1' - 1) * q)\<^sup>2 / real (n + k1' - 1))"
+    proof (rule binomial_distribution.prob_ge)
+      show "binomial_distribution q"
+        by unfold_locales (use q in auto)
+    next
+      show "n + k1' - 1 > 0"
+        using \<open>k1 > 0\<close> n unfolding k1'_def by linarith
+    next
+      have "real (n + nat \<lceil>k1\<rceil> - 1) \<le> real n + k1"
+        using \<open>k1 > 0\<close> by linarith
+      hence "real (n + k1' - 1) * q  \<le> (real n + k1) * q"
+        unfolding k1'_def by (intro mult_right_mono) (use p in \<open>simp_all add: q_def\<close>)
+      also have "\<dots> \<le> k1"
+        using k1 p by (simp add: q_def field_simps \<mu>_def)
+      finally show "0 \<le> k1 - real (n + k1' - 1) * q"
+        by simp
+    qed
+    also have "{x. real (n + k1' - 1) * q + (k1 - real (n + k1' - 1) * q) \<le> real x} = {x. real x \<ge> k1}"
+      by simp
+    also have "exp (-2 * (k1 - real (n + k1' - 1) * q)\<^sup>2 / real (n + k1' - 1)) \<le>
+               exp (-2 * (k1 - (n + k1) * q)\<^sup>2 / (n + k1))"
+    proof -
+      have "real (n + k1' - Suc 0) \<le> real n + k1"
+        unfolding k1'_def using \<open>k1 > 0\<close> by linarith
+      moreover have "(real n + k1) * q \<le> k1"
+        using k1 p by (auto simp: q_def field_simps \<mu>_def)
+      moreover have "1 < n + k1'"
+        using n \<open>k1 > 0\<close> unfolding k1'_def by linarith
+      ultimately have "2 * (k1 - real (n + k1' - 1) * q)\<^sup>2 / real (n + k1' - 1) \<ge>
+                       2 * (k1 - (n + k1) * q)\<^sup>2 / (n + k1)"
+        by (intro frac_le mult_left_mono power_mono mult_nonneg_nonneg mult_right_mono diff_mono)
+           (use q in simp_all)
+      thus ?thesis
+        by simp
+    qed
+    also have "\<dots> = exp (-2 * (p * k1 - q * n)\<^sup>2 / (k1 + n))"
+      by (simp add: q_def algebra_simps)
+    also have "-2 * (p * k1 - q * n)\<^sup>2 = -2 * p\<^sup>2 * (k1 - \<mu>)\<^sup>2"
+      using p by (auto simp: field_simps \<mu>_def)
+    also have "k1 - \<mu> = k"
+      by (simp add: k1_def \<mu>_def)
+    also note k1_def
+    also have "\<mu> + k + real n = real n / p + k"
+      using p by (simp add: \<mu>_def q_def field_simps)
+    also have "- 2 * p\<^sup>2 * k\<^sup>2 / (real n / p + k) = - 2 * p ^ 3 * k\<^sup>2 / (p * k + n)"
+      using p by (simp add: field_simps power3_eq_cube power2_eq_square)
+    finally show ?thesis by (simp add: add_ac)
+  qed
+qed
+
+lemma prob_neg_binomial_pmf_le_bound:
+  fixes n :: nat and k :: real
+  defines "\<mu> \<equiv> real n * q / p"
+  assumes k: "k \<ge> 0"
+  shows "measure_pmf.prob (neg_binomial_pmf n p) {x. real x \<le> \<mu> - k}
+         \<le> exp (-2 * p ^ 3 * k\<^sup>2 / (n - p * k))"
+proof -
+  consider "n = 0" | "p = 1" | "k > \<mu>" | "n > 0" "p \<noteq> 1" "k \<le> \<mu>"
+    by force
+  thus ?thesis
+  proof cases
+    assume [simp]: "n = 0"
+    show ?thesis using k
+      by (simp add: indicator_def \<mu>_def)
+  next
+    assume [simp]: "p = 1"
+    show ?thesis using k
+      by (auto simp add: indicator_def \<mu>_def q_def)
+  next
+    assume "k > \<mu>"
+    hence "{x. real x \<le> \<mu> - k} = {}"
+      by auto
+    thus ?thesis by simp
+  next
+    assume n: "n > 0" and "p \<noteq> 1" and "k \<le> \<mu>"
+    from \<open>p \<noteq> 1\<close> and p have p: "p \<in> {0<..<1}"
+      by auto
+    from p have q: "q \<in> {0<..<1}"
+      by (auto simp: q_def)
+
+    define f :: "real \<Rightarrow> real" where "f = (\<lambda>x. (p * x - q * n)\<^sup>2 / (x + n))"
+    have f_mono: "f x \<ge> f y" if "x \<ge> 0" "y \<le> n * q / p" "x \<le> y" for x y :: real
+      using that(3)
+    proof (rule DERIV_nonpos_imp_nonincreasing)
+      fix t assume t: "t \<ge> x" "t \<le> y"
+      have "x > -n"
+        using n \<open>x \<ge> 0\<close> by linarith
+      hence "(f has_field_derivative ((p * t - q * n) * (n * (1 + p) + p * t) / (n + t) ^ 2)) (at t)"
+        unfolding f_def using t
+        by (auto intro!: derivative_eq_intros simp: algebra_simps q_def power2_eq_square)
+      moreover {
+        have "p * t \<le> p * y"
+          using p by (intro mult_left_mono t) auto
+        also have "p * y \<le> q * n"
+          using \<open>y \<le> n * q / p\<close> p by (simp add: field_simps)
+        finally have "p * t \<le> q * n" .
+      }
+      hence "(p * t - q * n) * (n * (1 + p) + p * t) / (n + t) ^ 2 \<le> 0"
+        using p \<open>x \<ge> 0\<close> t
+        by (intro mult_nonpos_nonneg divide_nonpos_nonneg add_nonneg_nonneg mult_nonneg_nonneg) auto
+      ultimately show "\<exists>y. (f has_real_derivative y) (at t) \<and> y \<le> 0"
+        by blast
+    qed
+
+    define k1 where "k1 = \<mu> - k"
+    have k1: "k1 \<le> real n * q / p"
+      using assms by (simp add: \<mu>_def k1_def)
+    have "k1 \<ge> 0"
+      using k \<open>k \<le> \<mu>\<close> by (simp add: \<mu>_def k1_def)
+  
+    define k1' where "k1' = nat (floor k1)"
+    have "\<mu> \<ge> 0" using p
+      by (auto simp: \<mu>_def q_def)
+    have "(x \<le> k1') \<longleftrightarrow> real x \<le> k1" for x
+      unfolding k1'_def not_less using \<open>k1 \<ge> 0\<close> by linarith
+    hence eq: "{n. n \<le> k1}  = {..k1'}"
+      by auto
+    hence "measure_pmf.prob (neg_binomial_pmf n p) {n. n \<le> k1} =
+           measure_pmf.prob (neg_binomial_pmf n p) {..k1'}"
+      by simp
+    also have "measure_pmf.prob (neg_binomial_pmf n p) {..k1'} =
+               measure_pmf.prob (binomial_pmf (n + k1') q) {..k1'}"
+      unfolding q_def using p by (intro prob_neg_binomial_pmf_atMost) auto
+    also note eq [symmetric]
+    also have "{x. real x \<le> k1} = {x. x \<le> real (n + k1') * q - (real (n + k1') * q - real k1')}"
+      using eq by auto
+    also have "measure_pmf.prob (binomial_pmf (n + k1') q) \<dots> \<le>
+                 exp (-2 * (real (n + k1') * q - real k1')\<^sup>2 / real (n + k1'))"
+    proof (rule binomial_distribution.prob_le)
+      show "binomial_distribution q"
+        by unfold_locales (use q in auto)
+    next
+      show "n + k1' > 0"
+        using \<open>k1 \<ge> 0\<close> n unfolding k1'_def by linarith
+    next
+      have "p * k1' \<le> p * k1"
+        using p \<open>k1 \<ge> 0\<close> by (intro mult_left_mono) (auto simp: k1'_def)
+      also have "\<dots> \<le> q * n"
+        using k1 p by (simp add: field_simps)
+      finally show "0 \<le> real (n + k1') * q - real k1'"
+        by (simp add: algebra_simps q_def)
+    qed
+    also have "{x. real x \<le> real (n + k1') * q - (real (n + k1') * q - k1')} = {..k1'}"
+      by auto
+    also have "real (n + k1') * q - k1' = -(p * k1' - q * n)"
+      by (simp add: q_def algebra_simps)
+    also have "\<dots> ^ 2 = (p * k1' - q * n) ^ 2"
+      by algebra
+    also have "- 2 * (p * real k1' - q * real n)\<^sup>2 / real (n + k1') = -2 * f (real k1')"
+      by (simp add: f_def)
+    also have "f (real k1') \<ge> f k1"
+      by (rule f_mono) (use \<open>k1 \<ge> 0\<close> k1 in \<open>auto simp: k1'_def\<close>)
+    hence "exp (-2 * f (real k1')) \<le> exp (-2 * f k1)"
+      by simp
+    also have "\<dots> = exp (-2 * (p * k1 - q * n)\<^sup>2 / (k1 + n))"
+      by (simp add: f_def)
+
+    also have "-2 * (p * k1 - q * n)\<^sup>2 = -2 * p\<^sup>2 * (k1 - \<mu>)\<^sup>2"
+      using p by (auto simp: field_simps \<mu>_def)
+    also have "(k1 - \<mu>) ^ 2 = k ^ 2"
+      by (simp add: k1_def \<mu>_def)
+    also note k1_def
+    also have "\<mu> - k + real n = real n / p - k"
+      using p by (simp add: \<mu>_def q_def field_simps)
+    also have "- 2 * p\<^sup>2 * k\<^sup>2 / (real n / p - k) = - 2 * p ^ 3 * k\<^sup>2 / (n - p * k)"
+      using p by (simp add: field_simps power3_eq_cube power2_eq_square)
+    also have "{..k1'} = {x. real x \<le> \<mu> - k}"
+      using eq by (simp add: k1_def)
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  Due to the function $exp(-l/x)$ being concave for $x \geq \frac{l}{2}$, the above two
+  bounds can be combined into the following one for moderate values of \<open>k\<close>.
+  (cf. \<^url>\<open>https://math.stackexchange.com/questions/1565559\<close>)
+\<close>
+lemma prob_neg_binomial_pmf_abs_ge_bound:
+  fixes n :: nat and k :: real
+  defines "\<mu> \<equiv> real n * q / p"
+  assumes "k \<ge> 0" and n_ge: "n \<ge> p * k * (p\<^sup>2 * k + 1)"
+  shows "measure_pmf.prob (neg_binomial_pmf n p) {x. \<bar>real x - \<mu>\<bar> \<ge> k} \<le>
+           2 * exp (-2 * p ^ 3 * k ^ 2 / n)"
+proof (cases "k = 0")
+  case False
+  with \<open>k \<ge> 0\<close> have k: "k > 0"
+    by auto
+  define l :: real where "l = 2 * p ^ 3 * k ^ 2"
+  have l: "l > 0"
+    using p k by (auto simp: l_def)
+  define f :: "real \<Rightarrow> real" where "f = (\<lambda>x. exp (-l / x))"
+  define f' where "f' = (\<lambda>x. -l * exp (-l / x) / x ^ 2)"
+
+  have f'_mono: "f' x \<le> f' y" if "x \<ge> l / 2" "x \<le> y" for x y :: real
+    using that(2)
+  proof (rule DERIV_nonneg_imp_nondecreasing)
+    fix t assume t: "x \<le> t" "t \<le> y"
+    have "t > 0"
+      using that l t by auto
+    have "(f' has_field_derivative (l * (2 * t - l) / (exp (l / t) * t ^ 4))) (at t)"
+      unfolding f'_def using t that \<open>t > 0\<close>
+      by (auto intro!: derivative_eq_intros simp: field_simps exp_minus simp flip: power_Suc)
+    moreover have "l * (2 * t - l) / (exp (l / t) * t ^ 4) \<ge> 0"
+      using that t l by (intro divide_nonneg_pos mult_nonneg_nonneg) auto
+    ultimately show "\<exists>y. (f' has_real_derivative y) (at t) \<and> 0 \<le> y" by blast
+  qed
+
+  have convex: "convex_on {l/2..} (\<lambda>x. -f x)" unfolding f_def
+  proof (intro convex_on_realI[where f' = f'])
+    show "((\<lambda>x. - exp (- l / x)) has_real_derivative f' x) (at x)" if "x \<in> {l/2..}" for x
+      using that l
+      by (auto intro!: derivative_eq_intros simp: f'_def power2_eq_square algebra_simps)
+  qed (use l in \<open>auto intro!: f'_mono\<close>)
+
+  have eq: "{x. \<bar>real x - \<mu>\<bar> \<ge> k} = {x. real x \<le> \<mu> - k} \<union> {x. real x \<ge> \<mu> + k}"
+    by auto
+  have "measure_pmf.prob (neg_binomial_pmf n p) {x. \<bar>real x - \<mu>\<bar> \<ge> k} \<le>
+        measure_pmf.prob (neg_binomial_pmf n p) {x. real x \<le> \<mu> - k} +
+        measure_pmf.prob (neg_binomial_pmf n p) {x. real x \<ge> \<mu> + k}"
+    by (subst eq, rule measure_Un_le) auto
+  also have "\<dots> \<le> exp (-2 * p ^ 3 * k\<^sup>2 / (n - p * k)) + exp (-2 * p ^ 3 * k\<^sup>2 / (n + p * k))"
+    unfolding \<mu>_def
+    by (intro prob_neg_binomial_pmf_le_bound prob_neg_binomial_pmf_ge_bound add_mono \<open>k \<ge> 0\<close>)
+  also have "\<dots> = 2 * (1/2 * f (n - p * k) + 1/2 * f (n + p * k))"
+    by (simp add: f_def l_def)
+  also have "1/2 * f (n - p * k) + 1/2 * f (n + p * k) \<le> f (1/2 * (n - p * k) + 1/2 * (n + p * k))"
+  proof -
+    let ?x = "n - p * k" and ?y = "n + p * k"
+    have le1: "l / 2 \<le> ?x" using n_ge
+      by (simp add: l_def power2_eq_square power3_eq_cube algebra_simps)
+    also have "\<dots> \<le> ?y"
+      using p k by simp
+    finally have le2: "l / 2 \<le> ?y" .
+    have "-f ((1 - 1 / 2) *\<^sub>R ?x + (1 / 2) *\<^sub>R ?y) \<le> (1 - 1 / 2) * - f ?x + 1 / 2 * - f ?y"
+      using le1 le2 by (intro convex_onD[OF convex]) auto
+    thus ?thesis by simp
+  qed
+  also have "1/2 * (n - p * k) + 1/2 * (n + p * k) = n"
+    by (simp add: algebra_simps)
+  also have "2 * f n = 2 * exp (-l / n)"
+    by (simp add: f_def)
+  finally show ?thesis
+    by (simp add: l_def)
+qed auto
+
+end
+
+end