Theory Distributed_Distinct_Elements_Cutoff_Level
section ‹Cutoff Level›
text ‹This section verifies that the cutoff will be below @{term "q_max"} with high probability.
The result will be needed in Section~\ref{sec:accuracy}, where it is shown that the estimates
will be accurate for any cutoff below @{term "q_max"}.›
theory Distributed_Distinct_Elements_Cutoff_Level
imports
Distributed_Distinct_Elements_Accuracy_Without_Cutoff
Distributed_Distinct_Elements_Tail_Bounds
begin
hide_const (open) Quantum.Z
unbundle intro_cong_syntax
lemma mono_real_of_int: "mono real_of_int"
unfolding mono_def by auto
lemma Max_le_Sum:
fixes f :: "'a ⇒ int"
assumes "finite A"
assumes "⋀a. a ∈ A ⟹ f a ≥ 0"
shows "Max (insert 0 (f ` A)) ≤ (∑a ∈A .f a)" (is "?L ≤ ?R")
proof (cases "A≠{}")
case True
have 0: "f a ≤ (∑a ∈A .f a)" if "a ∈ A" for a
using that assms by (intro member_le_sum) auto
have "?L = max 0 (Max (f ` A))"
using True assms(1) by (subst Max_insert) auto
also have "... = Max (max 0 ` f ` A)"
using assms True by (intro mono_Max_commute monoI) auto
also have "... = Max (f ` A)"
unfolding image_image using assms
by (intro arg_cong[where f="Max"] image_cong) auto
also have "... ≤ ?R"
using 0 True assms(1)
by (intro iffD2[OF Max_le_iff]) auto
finally show ?thesis by simp
next
case False
hence "A = {}" by simp
then show ?thesis by simp
qed
context inner_algorithm_fix_A
begin
text ‹The following inequality is true for base e on the entire domain ($x > 0$). It is
shown in @{thm [source] ln_add_one_self_le_self}. In the following it is established for base
$2$, where it holds for $x \geq 1$.›
lemma log_2_estimate:
assumes "x ≥ (1::real)"
shows "log 2 (1+x) ≤ x"
proof -
define f where "f x = x - log 2 (1+ x)" for x :: real
define f' where "f' x = 1 - 1/((x+1)*ln 2)" for x :: real
have 0:"(f has_real_derivative (f' x)) (at x)" if "x > 0" for x
unfolding f_def f'_def using that
by (auto intro!: derivative_eq_intros)
have "f' x ≥ 0" if "1 ≤ x" for x :: real
proof -
have "(1::real) ≤ 2*ln 2"
by (approximation 5)
also have "... ≤ (x+1)*ln 2"
using that by (intro mult_right_mono) auto
finally have "1 ≤ (x+1)*ln 2" by simp
hence "1/((x+1)*ln 2) ≤ 1"
by simp
thus ?thesis
unfolding f'_def by simp
qed
hence "∃y. (f has_real_derivative y) (at x) ∧ 0 ≤ y" if "x ≥ 1" for x :: real
using that order_less_le_trans[OF exp_gt_zero]
by (intro exI[where x="f' x"] conjI 0) auto
hence "f 1 ≤ f x"
by (intro DERIV_nonneg_imp_nondecreasing[OF assms]) auto
thus "?thesis"
unfolding f_def by simp
qed
lemma cutoff_eq_7:
"real X * 2 powr (-real q_max) / b ≤ 1"
proof -
have "real X = 2 powr (log 2 X)"
using X_ge_1 by (intro powr_log_cancel[symmetric]) auto
also have "... ≤ 2 powr (nat ⌈log 2 X⌉)"
by (intro powr_mono) linarith+
also have "... = 2 ^ (nat ⌈log 2 X⌉)"
by (subst powr_realpow) auto
also have "... = real (2 ^ (nat ⌈log 2 (real X)⌉))"
by simp
also have "... ≤ real (2 ^ (b_exp + nat (⌈log 2 (real X)⌉ - int b_exp)))"
by (intro Nat.of_nat_mono power_increasing) linarith+
also have "... = b * 2^q_max"
unfolding q_max_def b_def by (simp add: power_add)
finally have "real X ≤ b * 2 ^ q_max" by simp
thus ?thesis
using b_min
unfolding powr_minus inverse_eq_divide
by (simp add:field_simps powr_realpow)
qed
lemma cutoff_eq_6:
fixes k
assumes "a ∈ A"
shows " (∫f. real_of_int (max 0 (int (f a) - int k)) ∂Ψ⇩1) ≤ 2 powr (-real k)" (is "?L ≤ ?R")
proof (cases "k ≤ n_exp - 1")
case True
have a_le_n: "a < n"
using assms A_range by auto
have "?L = (∫x. real_of_int (max 0 (int x - k)) ∂map_pmf (λx. x a) Ψ⇩1)"
by simp
also have "... = (∫x. real_of_int (max 0 (int x - k)) ∂(𝒢 n_exp))"
by (subst hash_pro_component[OF Ψ⇩1 a_le_n]) auto
also have "... = (∫x. max 0 (real x - real k) ∂(𝒢 n_exp))"
unfolding max_of_mono[OF mono_real_of_int,symmetric] by simp
also have "... = (∑x≤n_exp. max 0 (real x - real k) * pmf (𝒢 n_exp) x)"
using geom_pro_range by (intro integral_measure_pmf_real) auto
also have "... = (∑x=k+1..n_exp. (real x - real k) * pmf (𝒢 n_exp) x)"
by (intro sum.mono_neutral_cong_right) auto
also have "... = (∑x=k+1..n_exp. (real x - real k) * measure (𝒢 n_exp) {x})"
unfolding measure_pmf_single by simp
also have "... = (∑x=k+1..n_exp. (real x-real k)*(measure (𝒢 n_exp) ({ω. ω≥x}-{ω. ω≥(x+1)})))"
by (intro sum.cong arg_cong2[where f="(*)"] measure_pmf_cong) auto
also have "... = (∑x=k+1..n_exp. (real x-real k)*
(measure (𝒢 n_exp) {ω. ω≥x} - measure (𝒢 n_exp) {ω. ω≥(x+1)}))"
by (intro sum.cong arg_cong2[where f="(*)"] measure_Diff) auto
also have "... = (∑x=k+1..n_exp. (real x - real k) * (1/2^x - of_bool(x+1≤n_exp)/2^(x+1)))"
unfolding geom_pro_prob by (intro_cong "[σ⇩2 (*), σ⇩2 (-), σ⇩2 (/)]" more:sum.cong) auto
also have "... =
(∑x=k+1..n_exp. (real x-k)/2^x) - (∑x=k+1..n_exp. (real x-k)* of_bool(x+1≤n_exp)/2^(x+1))"
by (simp add:algebra_simps sum_subtractf)
also have "...=(∑x=k+1..n_exp. (real x-k)/2^x)-(∑x=k+1..n_exp-1. (real x-k)/2^(x+1))"
by (intro arg_cong2[where f="(-)"] refl sum.mono_neutral_cong_right) auto
also have "...=(∑x=k+1..(n_exp-1)+1. (real x-k)/2^x)-(∑x=k+1..n_exp-1. (real x-k)/2^(x+1))"
using n_exp_gt_0 by (intro arg_cong2[where f="(-)"] refl sum.cong) auto
also have "...= (∑x∈insert k {k+1..n_exp-1}. (real (x+1)-k)/2^(x+1))-
(∑x=k+1..n_exp-1. (real x-k)/2^(x+1))"
unfolding sum.shift_bounds_cl_nat_ivl using True
by (intro arg_cong2[where f="(-)"] sum.cong) auto
also have "... = 1/2^(k+1)+(∑x=k+1..n_exp-1. (real (x+1)-k)/2^(x+1)- (real x-k)/2^(x+1))"
by (subst sum.insert) (auto simp add:sum_subtractf)
also have "... = 1/2^(k+1)+(∑x=k+1..n_exp-1. (1/2^(x+1)))"
by (intro arg_cong2[where f="(+)"] sum.cong refl) (simp add:field_simps)
also have "... = (∑x∈insert k {k+1..n_exp-1}. (1/2^(x+1)))"
by (subst sum.insert) auto
also have "... = (∑x=0+k..(n_exp-1-k)+k. 1/2^(x+1))"
using True by (intro sum.cong) auto
also have "... = (∑x<n_exp-k. 1/2^(x+k+1))"
unfolding sum.shift_bounds_cl_nat_ivl using True n_exp_gt_0 by (intro sum.cong) auto
also have "... = (1/2)^(k+1) * (∑x<n_exp-k. (1/2)^x)"
unfolding sum_distrib_left power_add[symmetric] by (simp add:power_divide ac_simps)
also have "... = (1/2)^(k+1) * 2 * (1-(1 / 2) ^ (n_exp - k))"
by (subst geometric_sum) auto
also have "... ≤ (1/2)^(k+1) * 2 * (1-0)"
by (intro mult_left_mono diff_mono) auto
also have "... = (1/2)^k"
unfolding power_add by simp
also have "... = ?R"
unfolding powr_minus by (simp add:powr_realpow inverse_eq_divide power_divide)
finally show ?thesis
by simp
next
case False
hence k_ge_n_exp: "k ≥ n_exp"
by simp
have a_lt_n: "a < n"
using assms A_range by auto
have "?L = (∫x. real_of_int (max 0 (int x - k)) ∂map_pmf (λx. x a) Ψ⇩1)"
by simp
also have "... = (∫x. real_of_int (max 0 (int x - k)) ∂(𝒢 n_exp))"
by (subst hash_pro_component[OF Ψ⇩1 a_lt_n]) auto
also have "... = (∫x. real_of_int 0 ∂(𝒢 n_exp))"
using geom_pro_range k_ge_n_exp
by (intro integral_cong_AE AE_pmfI iffD2[OF of_int_eq_iff] max_absorb1) force+
also have "... = 0" by simp
finally show ?thesis by simp
qed
lemma cutoff_eq_5:
assumes "x ≥ (-1 :: real)"
shows "real_of_int ⌊log 2 (x+2)⌋ ≤ (real c+2) + max (x - 2^c) 0" (is "?L ≤ ?R")
proof -
have 0: "1 ≤ 2 ^ 1 * ln (2::real)"
by (approximation 5)
consider (a) "c = 0 ∧ x ≥ 2^c+1" | (b) "c > 0 ∧ x ≥ 2^c+1" | (c) "x ≤ 2^c+1"
by linarith
hence "log 2 (x+2) ≤ ?R"
proof (cases)
case a
have "log 2 (x+2) = log 2 (1+(x+1))"
by (simp add:algebra_simps)
also have "... ≤ x+1"
using a by (intro log_2_estimate) auto
also have "... = ?R"
using a by auto
finally show ?thesis by simp
next
case b
have "0 < 0 + (1::real)"
by simp
also have "... ≤ 2^c+(1::real)"
by (intro add_mono) auto
also have "... ≤ x"
using b by simp
finally have x_gt_0: "x > 0"
by simp
have "log 2 (x+2) = log 2 ((x+2)/2^c) + c"
using x_gt_0 by (subst log_divide) auto
also have "... = log 2 (1+(x+2-2^c)/2^c) + c"
by (simp add:divide_simps)
also have "... ≤ (x+2-2^c)/2^c / ln 2 + c"
using b unfolding log_def
by (intro add_mono divide_right_mono ln_add_one_self_le_self divide_nonneg_pos) auto
also have "... = (x+2-2^c)/(2^c*ln 2) + c"
by simp
also have "... ≤ (x+2-2^c)/(2^1*ln 2)+c"
using b by (intro add_mono divide_left_mono mult_right_mono power_increasing) simp_all
also have "... ≤ (x+2-2^c)/1 + c"
using b by (intro add_mono divide_left_mono 0) auto
also have "... ≤ (c+2) + max (x - 2^c) 0"
using b by simp
finally show ?thesis by simp
next
case c
hence "log 2 (x+2) ≤ log 2 ((2^c+1)+2)"
using assms by (intro log_mono add_mono) auto
also have "... = log 2 (2^c*(1+3/2^c))"
by (simp add:algebra_simps)
also have "... = c + log 2 (1+3/2^c)"
by (subst log_mult_pos) (auto intro:add_pos_nonneg)
also have "... ≤ c + log 2 (1+3/2^0)"
by (intro add_mono log_mono divide_left_mono power_increasing add_pos_nonneg) auto
also have "... = c + log 2 (2*2)"
by simp
also have "... = real c + 2"
by (subst log_mult) auto
also have "... ≤ (c+2) + max (x - 2^c) 0"
by simp
finally show ?thesis
by simp
qed
moreover have "⌊log 2 (x+2)⌋ ≤ log 2 (x+2)"
by simp
ultimately show ?thesis using order_trans by blast
qed
lemma cutoff_level:
"measure Ω {ω. q ω A > q_max} ≤ δ/2" (is "?L ≤ ?R")
proof -
have C⇩1_est: "C⇩1 * l ≤ 30 * real l"
unfolding C⇩1_def
by (intro mult_right_mono of_nat_0_le_iff) (approximation 10)
define Z where "Z ω = (∑j<b. real_of_int ⌊log 2 (of_int (max (τ⇩1 ω A q_max j) (-1)) + 2)⌋)" for ω
define V where "V ω = Z ω / real b - 3" for ω
have 2:"Z ψ ≤ real b*(real c+2) + of_int (∑a∈A. max 0 (int (fst ψ a) - q_max -2^c))"
(is "?L1 ≤ ?R1") if "ψ ∈ sample_pro Ψ" for c ψ
proof -
obtain f g h where ψ_def: "ψ = (f,g,h)"
using prod_cases3 by blast
have ψ_range: "(f,g,h) ∈ sample_pro Ψ"
using that unfolding ψ_def by simp
have "- 1 - 2^c ≤ -1-(1::real)"
by (intro diff_mono) auto
also have "... ≤ 0" by simp
finally have "- 1 - 2 ^ c ≤ (0::real)" by simp
hence aux3: "max (-1-2^c) 0 = (0::real)"
by (intro max_absorb2)
have "- 1 - int q_max - 2 ^ c ≤ -1 - 0 - 1"
by (intro diff_mono) auto
also have "... ≤ 0" by simp
finally have "- 1 - int q_max - 2 ^ c ≤ 0" by simp
hence aux3_2: "max 0 (- 1 - int q_max - 2 ^ c) = 0"
by (intro max_absorb1)
have "?L1 ≤ (∑j<b. (real c+2) + max (real_of_int (max (τ⇩1 ψ A q_max j) (- 1)) - 2^c) 0)"
unfolding Z_def by (intro sum_mono cutoff_eq_5) auto
also have "... = (∑j<b. (real c+2)+max (τ⇩0 ψ A j - q_max - 2^c) 0)"
unfolding τ⇩1_def max_of_mono[OF mono_real_of_int,symmetric]
by (intro_cong "[σ⇩2 (+)]" more:sum.cong) (simp add:max_diff_distrib_left max.assoc aux3)
also have "... = real b * (real c + 2) +
of_int (∑j<b. (max 0 (Max (insert (- 1) {int (f a) |a. a ∈ A ∧ h (g a) = j})-q_max - 2^c)))"
unfolding ψ_def by (simp add:max.commute)
also have "... = real b * (real c + 2) +
of_int (∑j<b. max 0 (Max ((λx. x-q_max-2^c)`(insert(-1){int (f a) |a. a ∈ A∧h(g a)=j}))))"
using fin_A
by (intro_cong "[σ⇩2 (+), σ⇩1 of_int, σ⇩2 max]" more:sum.cong mono_Max_commute) (auto simp:monoI)
also have "... = real b * (real c + 2) +
of_int(∑j<b. max 0(Max(insert(-1-q_max-2^c){int (f a)-q_max-2^c |a. a ∈ A ∧ h (g a) = j})))"
by (intro_cong "[σ⇩2 (+), σ⇩1 of_int, σ⇩2 max, σ⇩1 Max]" more:sum.cong) auto
also have "... = real b * (real c + 2) + of_int
(∑j<b. Max ((max 0) `(insert(-1-q_max-2^c){int (f a)-q_max-2^c |a. a ∈ A ∧ h (g a) = j})))"
using fin_A by (intro_cong "[σ⇩2 (+), σ⇩1 of_int]" more:sum.cong mono_Max_commute)
(auto simp add:monoI setcompr_eq_image)
also have "... = real b * (real c + 2) +
of_int (∑j<b. Max (insert 0 {max 0 (int (f a)-q_max-2^c) |a. a ∈ A ∧ h (g a) = j}))"
using aux3_2 by (intro_cong "[σ⇩2 (+), σ⇩1 of_int, σ⇩1 Max]" more:sum.cong)
(simp add:setcompr_eq_image image_image)
also have "... ≤ b*(real c+2)+ of_int(∑j<b. (∑a|a∈A∧h(g(a))=j. max 0(int(f a)-q_max-2^c)))"
using fin_A Max_le_Sum unfolding setcompr_eq_image
by (intro add_mono iffD2[OF of_int_le_iff] sum_mono Max_le_Sum) (simp_all)
also have "... = real b*(real c+2)+
of_int(∑a∈(⋃j∈{..<b}. {a. a∈A∧ h(g(a)) = j}). max 0(int(f a)-q_max-2^c))"
using fin_A
by (intro_cong "[σ⇩2 (+), σ⇩1 of_int]" more:sum.UNION_disjoint[symmetric]) auto
also have "... = real b*(real c+2) + of_int(∑a∈A. max 0(int(f a)-q_max-2^c))"
using h_range[OF ψ_range] by (intro_cong "[σ⇩2 (+), σ⇩1 of_int]" more:sum.cong) auto
also have "... = ?R1"
unfolding ψ_def by simp
finally show ?thesis
by simp
qed
have 1: "measure Ψ {ψ. real c ≤ V ψ} ≤ 2 powr (- (2^c))" (is "?L1 ≤ ?R1") for c
proof -
have "?L1 = measure Ψ {ψ. real b * (real c + 3) ≤ Z ψ}"
unfolding V_def using b_min by (intro measure_pmf_cong) (simp add:field_simps)
also have "... ≤ measure Ψ
{ψ. real b*(real c+3)≤ real b*(real c+2)+ of_int (∑a∈A. max 0 (int (fst ψ a)-q_max -2^c))}"
using 2 order_trans by (intro pmf_mono) blast
also have "... = measure Ψ {ψ. real b ≤ (∑a∈A. of_int (max 0 (int (fst ψ a) -q_max -2^c)))}"
by (intro measure_pmf_cong) (simp add:algebra_simps)
also have "... ≤ (∫ψ. (∑a∈A. of_int (max 0 (int (fst ψ a) -q_max -2^c))) ∂Ψ)/real b"
using b_min by (intro pmf_markov sum_nonneg) simp_all
also have "... = (∑a∈A. (∫ψ. of_int (max 0 (int (fst ψ a) -q_max -2^c)) ∂Ψ))/real b"
by (intro_cong "[σ⇩2(/)]" more:Bochner_Integration.integral_sum) simp
also have "... = (∑a∈A. (∫f. of_int (max 0 (int (f a)-q_max -2^c)) ∂(map_pmf fst Ψ)))/real b"
by simp
also have "... = (∑a∈A. (∫f. of_int (max 0 (int (f a) - (q_max +2^c))) ∂Ψ⇩1))/real b"
unfolding sample_pro_Ψ map_fst_pair_pmf by (simp add:algebra_simps)
also have "... ≤ (∑a∈A. 2 powr -real (q_max + 2^c))/real b"
using b_min by (intro sum_mono divide_right_mono cutoff_eq_6) auto
also have "... = real X * 2 powr (- real q_max + (- (2 ^ c))) / real b"
unfolding X_def by simp
also have "... = (real X * 2 powr (-real q_max) / b) * 2 powr (-(2^c))"
unfolding powr_add by (simp add:algebra_simps)
also have "... ≤ 1 * 2 powr (-(2^c))"
using cutoff_eq_7 by (intro mult_right_mono) auto
finally show ?thesis
by simp
qed
have 0: "measure Ψ {ψ. x ≤ V ψ} ≤ exp (- x * ln x ^ 3)" (is "?L1 ≤ ?R1") if "x ≥ 20" for x
proof -
define c where "c = nat ⌊x⌋"
have "x * ln x^3 ≤ exp (x * ln 2) * ln 2/2" if "x ≥ 150" for x::real
proof -
have aux_aux_0: "x^4 ≥ 0"
by simp
have "x * ln x^3 ≤ x * x^3"
using that by (intro mult_left_mono power_mono ln_bound) auto
also have "... = x^4 * 1"
by (simp add:numeral_eq_Suc)
also have "... ≤ x^4 * ((ln 2 / 10)^4 * (150 * (ln 2 / 10))^6 * (ln 2/2))"
by (intro mult_left_mono aux_aux_0) (approximation 8)
also have "... = (x * (ln 2 / 10))^4 * (150 * (ln 2 / 10))^6 * (ln 2/2)"
unfolding power_mult_distrib by (simp add:algebra_simps)
also have "... ≤ (x * (ln 2 / 10))^4 * (x * (ln 2 / 10))^6 * (ln 2/2)"
by (intro mult_right_mono mult_left_mono power_mono that) auto
also have "... = (0+x * (ln 2 / 10))^10 * (ln 2/2)"
unfolding power_add[symmetric] by simp
also have "... ≤ (1+x * ln 2 / 10)^10 * (ln 2/2)"
using that by (intro mult_right_mono power_mono add_mono) auto
also have "... ≤ exp (x * ln 2 / 10)^10 * (ln 2/2)"
using that by (intro mult_right_mono power_mono exp_ge_add_one_self) auto
also have "... = exp (x * ln 2) * (ln 2/2)"
unfolding exp_of_nat_mult[symmetric] by simp
finally show ?thesis by simp
qed
moreover have "x * ln x^3 ≤ exp (x * ln 2) * ln 2/2" if "x ∈ {20..150}"
using that by (approximation 10 splitting: x=1)
ultimately have "x * ln x^3 ≤ exp (x * ln 2) * ln 2/2"
using that by fastforce
also have "... = 2 powr (x-1) * ln 2"
unfolding powr_diff unfolding powr_def by simp
also have "... ≤ 2 powr c * ln 2"
unfolding c_def using that
by (intro mult_right_mono powr_mono) auto
also have "... = 2^c * ln 2"
using powr_realpow by simp
finally have aux0: "x * ln x^3 ≤ 2^c * ln 2"
by simp
have "real c ≤ x"
using that unfolding c_def by linarith
hence "?L1 ≤ measure Ψ {ψ. real c ≤ V ψ}"
by (intro pmf_mono) auto
also have "... ≤ 2 powr (-(2^c))"
by (intro 1)
also have "... = exp (- (2 ^ c * ln 2))"
by (simp add:powr_def)
also have "... ≤ exp (- (x *ln x^3))"
using aux0 by (intro iffD2[OF exp_le_cancel_iff]) auto
also have "... = ?R1"
by simp
finally show ?thesis
by simp
qed
have "?L ≤ measure Ω {ω. is_too_large (τ⇩2 ω A q_max)}"
using lt_s_too_large
by (intro pmf_mono) (simp del:is_too_large.simps)
also have "... = measure Ω
{ω. (∑(i,j)∈{..<l}×{..<b}. ⌊log 2 (of_int (max (τ⇩2 ω A q_max i j) (-1)) + 2)⌋) > C⇩5 * b *l}"
by simp
also have "... = measure Ω {ω. real_of_int (∑(i,j)∈{..<l}×{..<b}.
⌊log 2 (of_int (max (τ⇩2 ω A q_max i j) (-1)) + 2)⌋) > of_int (C⇩5 * b * l)}"
unfolding of_int_less_iff by simp
also have "... = measure Ω {ω. real_of_int C⇩5 * real b * real l < of_int (∑x∈{..<l} × {..<b}.
⌊log 2 (real_of_int (τ⇩1 (ω (fst x)) A q_max (snd x)) + 2)⌋)}"
by (intro_cong "[σ⇩2 measure, σ⇩1 Collect, σ⇩1 of_int, σ⇩2 (<)]" more:ext sum.cong)
(auto simp add:case_prod_beta τ⇩2_def τ⇩1_def)
also have "... = measure Ω {ω. (∑i<l. Z (ω i)) > of_int C⇩5 * real b * real l}"
unfolding Z_def sum.cartesian_product τ⇩1_def by (simp add:case_prod_beta)
also have "... = measure Ω {ω. (∑i<l. V (ω i) + 3) > of_int C⇩5 * real l}"
unfolding V_def using b_min
by (intro measure_pmf_cong) (simp add:sum_divide_distrib[symmetric] field_simps sum.distrib)
also have "... = measure Ω {ω. (∑i<l. V (ω i)) > of_int (C⇩5-3) * real l}"
by (simp add:sum.distrib algebra_simps)
also have "... ≤ measure Ω {ω. (∑i<l. V (ω i)) ≥ C⇩1 * real l}"
unfolding C⇩5_def using C⇩1_est by (intro pmf_mono) auto
also have "... ≤ exp (- real l)"
by (intro deviation_bound l_gt_0 0) (simp_all add: Λ_def)
also have "... ≤ exp (- (C⇩6 * ln (2 / δ)))"
using l_lbound by (intro iffD2[OF exp_le_cancel_iff]) auto
also have "... ≤ exp (- (1 * ln (2 / δ)))"
unfolding C⇩6_def using δ_gt_0 δ_lt_1
by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le mult_right_mono ln_ge_zero) auto
also have "... = exp ( ln ( δ / 2))"
using δ_gt_0 by (simp add: ln_div)
also have "... = δ/2"
using δ_gt_0 by simp
finally show ?thesis
by simp
qed
end
unbundle no intro_cong_syntax
end