Theory Distributed_Distinct_Elements_Accuracy_Without_Cutoff

section ‹Accuracy without cutoff\label{sec:accuracy_wo_cutoff}›

text ‹This section verifies that each of the $l$ estimate have the required accuracy with high
probability assuming that there was no cut-off, i.e., that $s=0$. Section~\ref{sec:accuracy} will
then show that this remains true as long as the cut-off is below @{term "t f"} the subsampling
threshold.›

theory Distributed_Distinct_Elements_Accuracy_Without_Cutoff
  imports
    Concentration_Inequalities.Bienaymes_Identity
    Distributed_Distinct_Elements_Inner_Algorithm
    Distributed_Distinct_Elements_Balls_and_Bins
begin

hide_fact (open) Discrete.log_mono
no_notation Polynomials.var ("Xı")

locale inner_algorithm_fix_A = inner_algorithm +
  fixes A
  assumes A_range: "A  {..<n}"
  assumes A_nonempty: "{}  A"
begin

definition X :: nat where "X = card A"

definition q_max where "q_max = nat (log 2 X - b_exp)"

definition t :: "(nat  nat)  int"
  where "t f = int (Max (f ` A)) - b_exp + 9"

definition s :: "(nat  nat)  nat"
  where "s f = nat (t f)"

definition R :: "(nat  nat)  nat set"
  where "R f = {a. a  A  f a  s f}"

definition r :: "nat  (nat  nat)  nat"
  where "r x f = card {a. a  A  f a  x}"

definition p where "p = (λ(f,g,h). card {j {..<b}. τ1 (f,g,h) A 0 j  s f})"

definition Y where "Y = (λ(f,g,h). 2 ^ s f * ρ_inv (p (f,g,h)))"

lemma fin_A: "finite A"
  using A_range finite_nat_iff_bounded by auto

lemma X_le_n: "X  n"
proof -
  have "card A  card {..<n}"
    by (intro card_mono A_range) simp
  thus ?thesis
    unfolding X_def by simp
qed

lemma X_ge_1: "X  1"
  unfolding X_def
  using fin_A A_nonempty by (simp add: leI)

lemma of_bool_square: "(of_bool x)2 = ((of_bool x)::real)"
  by (cases x, auto)

lemma r_eq: "r x f = ( a  A.( of_bool( x  f a) :: real))"
  unfolding r_def of_bool_def sum.If_cases[OF fin_A]
  by (simp add: Collect_conj_eq)

lemma
  shows
    r_exp: "(ω. real (r x ω)  Ψ1) = real X * (of_bool (x  max (nat log 2 n) 1) / 2^x)" and
    r_var: "measure_pmf.variance Ψ1 (λω. real (r x ω))  (ω. real (r x ω)  Ψ1)"
proof -
  define V :: "nat  (nat  nat)  real" where "V = (λa f. of_bool (x  f a))"

  have V_exp: "(ω. V a ω Ψ1) = of_bool (x  max (nat log 2 n) 1)/2^x"
    (is "?L = ?R") if "a  A" for a
  proof -
    have a_le_n: "a < n"
      using that A_range by auto

    have "?L = (ω. indicator {f. x  f a} ω  Ψ1)"
      unfolding V_def by (intro integral_cong_AE) auto
    also have "... = measure (map_pmf (λω. ω a) (sample_pro Ψ1)) {f. x  f}"
      by simp
    also have "... = measure (𝒢 n_exp) {f. x  f}"
      by (subst hash_pro_component[OF Ψ1 a_le_n]) auto
    also have "... = of_bool (x  max (nat log 2 n) 1)/2^x"
      unfolding geom_pro_prob n_exp_def by simp
    finally show ?thesis by simp
  qed

  have b:"(ω. real (r x ω)  Ψ1) = ( a  A. (ω. V a ω Ψ1))"
    unfolding r_eq V_def by (intro Bochner_Integration.integral_sum) auto
  also have "... = ( a  A.  of_bool (x  max (nat log 2 n) 1)/2^x)"
    using V_exp by (intro sum.cong) auto
  also have "... = X * (of_bool (x  max (nat log 2 n) 1) / 2^x)"
    using X_def by simp
  finally show "(ω. real (r x ω)  Ψ1) = real X * (of_bool (x  max (nat log 2 n) 1)/ 2^x)"
    by simp

  have "(ω. (V a ω)^2  Ψ1) = (ω. V a ω  Ψ1)" for a
    unfolding V_def of_bool_square by simp

  hence a:"measure_pmf.variance Ψ1 (V a)  measure_pmf.expectation Ψ1 (V a)"  for a
    by (subst measure_pmf.variance_eq) auto

  have "J  A  card J = 2  prob_space.indep_vars Ψ1 (λ_. borel) V J" for J
    unfolding V_def using A_range finite_subset[OF _ fin_A]
    by (intro  prob_space.indep_vars_compose2[where Y="λi y. of_bool(x  y)" and M'="λ_. discrete"]
         hash_pro_indep[OF Ψ1]) (auto simp:prob_space_measure_pmf)
  hence "measure_pmf.variance Ψ1 (λω. real (r x ω)) = ( a  A. measure_pmf.variance Ψ1 (V a))"
    unfolding r_eq V_def by (intro measure_pmf.bienaymes_identity_pairwise_indep_2 fin_A) simp_all
  also have "...  ( a  A. (ω. V a ω  Ψ1))"
    by (intro sum_mono a)
  also have "... = (ω. real (r x ω)  Ψ1)"
    unfolding b by simp
  finally show "measure_pmf.variance Ψ1 (λω. real (r x ω))  (ω. real (r x ω)  Ψ1)" by simp
qed

definition E1 where "E1 = (λ(f,g,h). 2 powr (-t f) * X  {b/2^16..b/2})"

lemma t_low:
  "measure Ψ1 {f. of_int (t f) < log 2 (real X) + 1 - b_exp}  1/2^7" (is "?L  ?R")
proof (cases "log 2 (real X)  8")
  case True
  define Z :: "(nat  nat)  real" where "Z = r (nat log 2 (real X) - 8)"

  have "log 2 (real X)  log 2 (real n)"
    using X_le_n X_ge_1 by (intro log_mono) auto
  hence "nat log 2 (real X) - 8  nat log 2 (real n)"
    by (intro nat_mono ceiling_mono) simp
  hence a:"(nat log 2 (real X) - 8  max (nat log 2 (real n)) 1)"
    by simp

  have b:"real (nat (log 2 (real X) - 8))  log 2 (real X) - 7"
    using True by linarith

  have "2 ^ 7 = real X / (2 powr (log 2 X) * 2 powr (-7))"
    using X_ge_1 by simp
  also have "... = real X / (2 powr (log 2 X - 7))"
    by (subst powr_add[symmetric]) simp
  also have "...  real X / (2 powr (real (nat log 2 (real X) - 8)))"
    using b by (intro divide_left_mono powr_mono) auto
  also have "... = real X / 2 ^ nat log 2 (real X) - 8"
    by (subst powr_realpow) auto
  finally have "2 ^ 7  real X / 2 ^ nat log 2 (real X) - 8"
    by simp
  hence exp_Z_gt_2_7: "(ω. Z ω Ψ1)  2^7"
    using a unfolding Z_def r_exp by simp

  have var_Z_le_exp_Z: "measure_pmf.variance Ψ1 Z  (ω. Z ω Ψ1)"
    unfolding Z_def by (intro r_var)

  have "?L  measure Ψ1 {f. of_nat (Max (f ` A)) < log 2 (real X) - 8}"
    unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def)
  also have "...  measure Ψ1 {f  space Ψ1.  (ω. Z ω Ψ1)  ¦Z f - (ω. Z ω Ψ1) ¦}"
  proof (rule pmf_mono)
    fix f assume "f  set_pmf (sample_pro Ψ1)"
    have fin_f_A: "finite (f ` A)" using fin_A finite_imageI by blast
    assume " f  {f. real (Max (f ` A)) < log 2 (real X) - 8}"
    hence "real (Max (f ` A)) < log 2 (real X) - 8" by auto
    hence "real (f a) < log 2 (real X) - 8" if "a  A" for a
      using Max_ge[OF fin_f_A] imageI[OF that]  order_less_le_trans by fastforce
    hence "of_nat (f a) < log 2 (real X) - 8" if "a  A" for a
      using that by (subst less_ceiling_iff) auto
    hence "f a < nat log 2 (real X) - 8" if "a  A" for a
      using that True by fastforce
    hence "r (nat log 2 (real X) - 8) f = 0"
      unfolding r_def card_eq_0_iff using not_less by auto
    hence "Z f = 0"
      unfolding Z_def by simp
    thus "f  {f  space Ψ1.  (ω. Z ω Ψ1)  ¦Z f - (ω. Z ω Ψ1)¦}"
      by auto
  qed
  also have "...  measure_pmf.variance Ψ1 Z / (ω. Z ω Ψ1)^2"
    using exp_Z_gt_2_7 by (intro measure_pmf.second_moment_method) simp_all
  also have "...  (ω. Z ω Ψ1) / (ω. Z ω Ψ1)^2"
    by (intro divide_right_mono var_Z_le_exp_Z) simp
  also have "... = 1 / (ω. Z ω Ψ1)"
    using exp_Z_gt_2_7 by (simp add:power2_eq_square)
  also have "...  ?R"
    using exp_Z_gt_2_7 by (intro divide_left_mono) auto
  finally show ?thesis by simp
next
  case "False"
  have "?L  measure Ψ1 {f. of_nat (Max (f ` A)) < log 2 (real X) - 8}"
    unfolding t_def by (intro pmf_mono) (auto simp add:int_of_nat_def)
  also have "...  measure Ψ1 {}"
    using False by (intro pmf_mono) simp
  also have "... = 0"
    by simp
  also have "...  ?R" by simp
  finally show ?thesis by simp
qed

lemma t_high:
  "measure Ψ1 {f. of_int (t f) > log 2 (real X) + 16 - b_exp}  1/2^7" (is "?L  ?R")
proof -
  define Z :: "(nat  nat)  real" where "Z = r (nat log 2 (real X) + 8)"

  have Z_nonneg: "Z f  0" for f
    unfolding Z_def r_def by simp

  have "(ω. Z ω Ψ1)  real X / (2 ^ nat log 2 (real X) + 8)"
    unfolding Z_def r_exp by simp
  also have "...  real X / (2 powr (real (nat log 2 (real X) + 8)))"
    by (subst powr_realpow) auto
  also have "...  real X / (2 powr log 2 (real X) + 8)"
    by (intro divide_left_mono powr_mono) auto
  also have "...  real X / (2 powr (log 2 (real X) + 7))"
    by (intro divide_left_mono powr_mono, linarith) auto
  also have "... = real X / 2 powr (log 2 (real X)) / 2 powr 7"
    by (subst powr_add) simp
  also have "...  1/2 powr 7"
    using X_ge_1 by (subst powr_log_cancel) auto
  finally have Z_exp: "(ω. Z ω Ψ1)  1/2^7"
    by simp

  have "?L  measure Ψ1 {f. of_nat (Max (f ` A)) > log 2 (real X) + 7}"
    unfolding t_def  by (intro pmf_mono) (auto simp add:int_of_nat_def)
  also have "...  measure Ψ1 {f. Z f  1}"
  proof (rule pmf_mono)
    fix f assume "f  set_pmf (sample_pro Ψ1)"
    assume " f  {f. real (Max (f ` A)) > log 2 (real X) + 7}"
    hence "real (Max (f ` A)) > log 2 (real X) + 7" by simp
    hence "int (Max (f ` A))  log 2 (real X) + 8"
      by linarith
    hence "Max (f ` A)  nat log 2 (real X) + 8"
      by simp
    moreover have "f ` A  {}" "finite (f ` A)"
      using fin_A finite_imageI A_nonempty by auto
    ultimately obtain fa where "fa  f ` A" " fa   nat log 2 (real X) + 8"
      using Max_in by auto
    then obtain ae where ae_def: "ae  A" "nat log 2 (real X) + 8  f ae"
      by auto
    hence "r (nat log 2 (real X) + 8) f > 0"
      unfolding r_def card_gt_0_iff using fin_A by auto
    hence "Z f  1"
      unfolding Z_def by simp
    thus "f  {f. 1  Z f}" by simp
  qed
  also have "...  (ω. Z ω Ψ1) / 1"
    using Z_nonneg by (intro pmf_markov) auto
  also have "...  ?R"
    using Z_exp by simp
  finally show ?thesis by simp
qed

lemma e_1: "measure Ψ {ψ. ¬E1 ψ}  1/2^6"
proof -
  have "measure Ψ1 {f. 2 powr (of_int (-t f)) * real X  {real b/2^16..real b/2}} 
    measure Ψ1 {f. 2 powr (of_int (-t f)) * real X < real b/2^16} +
    measure Ψ1 {f. 2 powr (of_int (-t f)) * real X > real b/2}"
    by (intro pmf_add) auto
  also have "...  measure Ψ1 {f. of_int (t f) > log 2 X + 16 - b_exp} +
                   measure Ψ1 {f. of_int (t f) < log 2 X + 1 - b_exp}"
  proof (rule add_mono)
    show "measure Ψ1 {f. 2 powr (of_int (-t f)) * real X < real b/2^16} 
    measure Ψ1 {f. of_int (t f) > log 2 X + 16 - b_exp}"
    proof (rule pmf_mono)
      fix f assume "f  {f. 2 powr real_of_int (-t f) * real X < real b / 2 ^ 16}"
      hence "2 powr real_of_int (-t f) * real X < real b / 2 ^ 16"
        by simp
      hence "log 2 (2 powr of_int (-t f) * real X) < log 2 (real b / 2^16)"
        using b_min X_ge_1 by (intro iffD2[OF log_less_cancel_iff]) auto
      hence "of_int (-t f) + log  2 (real X) < log 2 (real b / 2^16)"
        using X_ge_1 by (subst (asm) log_mult) auto
      also have  "... = real b_exp - log 2 (2 powr 16)"
        unfolding b_def by (subst log_divide) auto
      also have "... = real b_exp - 16"
        by (subst log_powr_cancel) auto
      finally have "of_int (-t f) + log 2 (real X) < real b_exp - 16" by simp
      thus "f  {f. of_int (t f) > log 2 (real X) + 16 - b_exp}"
        by simp
    qed
  next
    show "measure Ψ1 {f. 2 powr of_int (-t f) * real X > real b/2} 
      measure Ψ1 {f. of_int (t f) < log 2 X + 1 - b_exp}"
    proof (rule pmf_mono)
      fix f assume "f  {f. 2 powr real_of_int (-t f) * real X > real b / 2}"
      hence "2 powr real_of_int (-t f) * real X > real b / 2"
        by simp
      hence "log 2 (2 powr of_int (-t f) * real X) > log 2 (real b / 2)"
        using b_min X_ge_1 by (intro iffD2[OF log_less_cancel_iff]) auto
      hence "of_int (-t f) + log  2 (real X) > log 2 (real b / 2)"
        using X_ge_1 by (subst (asm) log_mult) auto
      hence  "of_int (-t f) + log  2 (real X) > real b_exp - 1"
        unfolding b_def by (subst (asm) log_divide) auto
      hence "of_int (t f) < log 2 (real X) + 1 - b_exp"
        by simp
      thus "f  {f. of_int (t f) < log 2 (real X) + 1 - b_exp}"
        by simp
    qed
  qed
  also have "...  1/2^7 + 1/2^7"
    by (intro add_mono t_low t_high)
  also have "... = 1/2^6" by simp
  finally have "measure Ψ1 {f. 2 powr of_int (-t f) * real X  {real b/2^16..real b/2}}  1/2^6"
    by simp

  thus ?thesis
    unfolding sample_pro_Ψ E1_def case_prod_beta
    by (subst pair_pmf_prob_left)
qed

definition E2 where "E2 = (λ(f,g,h). ¦card (R f) - X / 2^(s f)¦  ε/3 * X / 2^(s f))"

lemma e_2: "measure Ψ {ψ. E1 ψ  ¬E2 ψ}  1/2^6" (is "?L  ?R")
proof -
  define tm :: int where "tm = log 2 (real X) + 16 - b_exp"

  have t_m_bound: "tm  log 2 (real X) - 10"
    unfolding tm_def using b_exp_ge_26 by simp

  have "real b / 2^16 = (real X * (1/ X)) * (real b / 2^16)"
    using X_ge_1 by simp
  also have "... = (real X * 2 powr (-log 2 X)) * (real b / 2^16)"
    using X_ge_1 by (subst powr_minus_divide) simp
  also have "...  (real X * 2 powr (- log 2 (real X))) * (2 powr b_exp / 2^16)"
    unfolding b_def using powr_realpow
    by (intro mult_mono powr_mono) auto
  also have "... = real X * (2 powr (- log 2 (real X)) * 2 powr(real b_exp-16))"
    by (subst powr_diff) simp
  also have "... = real X * 2 powr (- log 2 (real X) + (int b_exp - 16))"
    by (subst powr_add[symmetric]) simp
  also have "... = real X * 2 powr (-tm)"
    unfolding tm_def by (simp add:algebra_simps)
  finally have c:"real b / 2^16  real X * 2 powr (-tm)" by simp

  define T :: "nat set" where "T = {x. (real X / 2^x  real b / 2^16)}"

  have "x  T  int x  tm" for x
  proof -
    have "x  T  2^ x  real X * 2^16 / b"
      using b_min by (simp add: field_simps T_def)
    also have "...  log 2 (2^x)  log 2 (real X * 2^16 / b)"
      using X_ge_1 b_min by (intro log_le_cancel_iff[symmetric] divide_pos_pos) auto
    also have "...  x  log 2 (real X * 2^16) - log 2 b"
      using X_ge_1 b_min by (subst log_divide) auto
    also have "...  x  log 2 (real X) + log 2 (2 powr 16) - b_exp"
      unfolding b_def using X_ge_1 by (subst log_mult) auto
    also have "...  x  log 2 (real X) + log 2 (2 powr 16) - b_exp"
      by linarith
    also have "...  x  log 2 (real X) + 16 - real_of_int (int b_exp)"
      by (subst log_powr_cancel) auto
    also have "...  x  tm"
      unfolding tm_def by linarith
    finally show ?thesis by simp
  qed
  hence T_eq: "T = {x. int x  tm}" by auto

  have "T = {x. int x < tm+1}"
    unfolding T_eq by simp
  also have "... = {x. x < nat (tm + 1)}"
    unfolding zless_nat_eq_int_zless by simp
  finally have T_eq_2: "T = {x. x < nat (tm + 1)}"
    by simp

  have inj_1: "inj_on ((-) (nat tm)) T"
    unfolding T_eq by (intro inj_onI) simp
  have fin_T: "finite T"
    unfolding T_eq_2 by simp

  have r_exp: "(ω. real (r t ω) Ψ1) = real X / 2^t" if "t  T" for t
  proof -
    have "t  tm"
      using that unfolding T_eq by simp
    also have "...  log 2 (real X) - 10"
      using t_m_bound by simp
    also have "...  log 2 (real X)"
      by simp
    also have "...  log 2 (real n)"
      using X_le_n X_ge_1 by (intro floor_mono log_mono) auto
    also have "...  log 2 (real n)"
      by simp
    finally have "t  log 2 (real n)" by simp
    hence "t  max (nat log 2 (real n)) 1"by simp
    thus ?thesis
      unfolding r_exp by simp
  qed

  have r_var: "measure_pmf.variance Ψ1 (λω. real (r t ω))  real X / 2^t" if "t  T" for t
    using r_exp[OF that] r_var by metis

  have "9 = C4 / ε2 * ε^2/2^23"
    using ε_gt_0 by (simp add:C4_def)
  also have "... = 2 powr (log 2 (C4 /  ε2)) *  ε^2/2^23"
    using ε_gt_0 C4_def by (subst powr_log_cancel) auto
  also have "...  2 powr b_exp * ε^2/2^23"
    unfolding b_exp_def
    by (intro divide_right_mono mult_right_mono powr_mono, linarith) auto
  also have "... = b * ε^2/2^23"
    using powr_realpow unfolding b_def by simp
  also have "... = (b/2^16) * (ε^2/2^7)"
    by simp
  also have "...  (X * 2 powr (-tm)) * (ε^2/2^7)"
    by (intro mult_mono c) auto
  also have "... = X * (2 powr (-tm) * 2 powr (-7)) * ε^2"
    using powr_realpow by simp
  also have "... = 2 powr (-tm-7) * (ε^2 * X)"
    by (subst powr_add[symmetric]) (simp )
  finally have "9  2 powr (-tm-7) * (ε^2 * X)" by simp
  hence b: "9/ (ε^2 * X)  2 powr (-tm -7)"
    using ε_gt_0 X_ge_1
    by (subst pos_divide_le_eq) auto

  have a: "measure Ψ1 {f.¦real (r t f)-real X/2^t¦> ε/3 *real X/2^t}  2 powr (real t-tm-7)"
    (is"?L1  ?R1") if "t  T" for t
  proof -
    have "?L1  𝒫(f in Ψ1. ¦real (r t f) - real X / 2^t¦   ε/3 * real X / 2^t)"
      by (intro pmf_mono) auto
    also have "... = 𝒫(f in Ψ1. ¦real (r t f)-(ω. real (r t ω)  Ψ1)¦  ε/3 * real X/2^t)"
      by (simp add: r_exp[OF that])
    also have "...  measure_pmf.variance Ψ1 (λω. real (r t ω)) / (ε/3 * real X / 2^t)^2"
      using X_ge_1 ε_gt_0
      by (intro measure_pmf.Chebyshev_inequality divide_pos_pos mult_pos_pos) auto
    also have "...  (X / 2^t) / (ε/3 * X / 2^t)^2"
      by (intro divide_right_mono r_var[OF that]) simp
    also have "... = 2^t*(9/ ( ε^2 * X))"
      by (simp add:power2_eq_square algebra_simps)
    also have "...  2^t*(2 powr (-tm-7))"
      by (intro mult_left_mono b) simp
    also have "... = 2 powr t * 2 powr (-tm-7)"
      by (subst powr_realpow[symmetric]) auto
    also have "... = ?R1"
      by (subst powr_add[symmetric]) (simp add:algebra_simps)
    finally show "?L1  ?R1" by simp
  qed

  have "y<nat (tm + 1). x = nat tm - y" if "x < nat (tm+1)" for x
    using that by (intro exI[where x="nat tm - x"]) simp
  hence T_reindex: "(-) (nat tm) ` {x. x < nat (tm + 1)} = {..<nat (tm + 1)}"
    by (auto simp add: set_eq_iff image_iff)

  have "?L  measure Ψ {ψ. (t  T. ¦real (r t (fst ψ))-real X/2^t¦ > ε/3 * real X / 2^t)}"
  proof (rule pmf_mono)
    fix ψ
    assume "ψ  set_pmf (sample_pro Ψ)"
    obtain f g h where ψ_def: "ψ = (f,g,h)" by (metis prod_cases3)
    assume "ψ  {ψ. E1 ψ  ¬ E2 ψ}"
    hence a:"2 powr ( -real_of_int (t f)) * real X  {real b/2^16..real b/2}" and
      b:"¦card (R f) - real X / 2^(s f)¦ >  ε/3 * X / 2^(s f)"
      unfolding E1_def E2_def by (auto simp add:ψ_def)
    have "¦card (R f) - X / 2^(s f)¦ = 0" if "s f= 0"
      using that by (simp add:R_def X_def)
    moreover have "( ε/3) * (X / 2^s f)  0"
      using ε_gt_0 X_ge_1 by (intro mult_nonneg_nonneg) auto
    ultimately have "False" if "s f = 0"
      using b that by simp
    hence "s f > 0" by auto
    hence "t f = s f" unfolding s_def by simp
    hence "2 powr (-real (s f)) * X  b / 2^16"
      using a by simp
    hence "X / 2 powr (real (s f))  b / 2^16"
      by (simp add: divide_powr_uminus mult.commute)
    hence "real X / 2 ^ (s f)  b / 2^16"
      by (subst (asm) powr_realpow, auto)
    hence "s f  T" unfolding T_def by simp
    moreover have "¦r (s f) f - X / 2^s f¦ >  ε/3 * X / 2^s f"
      using R_def r_def b by simp
    ultimately have "t  T. ¦r t (fst ψ) - X / 2^t¦ >  ε/3 * X / 2^t"
      using ψ_def by (intro bexI[where x="s f"]) simp
    thus "ψ  {ψ. (t  T. ¦r t (fst ψ) - X / 2^t¦ >  ε/3 * X / 2^t)}" by simp
  qed
  also have "... = measure Ψ1 {f. (t  T. ¦real (r t f)-real X / 2^t¦ > ε/3 * real X/2^t)}"
    unfolding sample_pro_Ψ by (intro pair_pmf_prob_left)
  also have "... = measure Ψ1 (t  T. {f. ¦real (r t f)-real X / 2^t¦ > ε/3 * real X/2^t})"
    by (intro measure_pmf_cong) auto
  also have "...  (t  T. measure Ψ1 {f.¦real (r t f)-real X / 2^t¦ > ε/3 * real X/2^t})"
    by (intro measure_UNION_le fin_T) (simp)
  also have "...  (t  T.  2 powr (real t - of_int tm - 7))"
    by (intro sum_mono a)
  also have "... = (t  T.  2 powr (-int (nat tm-t) - 7))"
    unfolding T_eq
    by (intro sum.cong refl arg_cong2[where f="(powr)"]) simp
  also have "... = (x  (λx. nat tm - x) ` T. 2 powr (-real x - 7))"
    by (subst sum.reindex[OF inj_1]) simp
  also have "... = (x  (λx. nat tm - x) ` T. 2 powr (-7) * 2 powr (-real x))"
    by (subst powr_add[symmetric]) (simp add:algebra_simps)
  also have "... = 1/2^7 * (x  (λx. nat tm - x) ` T. 2 powr (-real x))"
    by (subst sum_distrib_left) simp
  also have "... = 1/2^7 * (x <nat (tm+1). 2 powr (-real x))"
    unfolding T_eq_2 T_reindex
    by (intro arg_cong2[where f="(*)"] sum.cong) auto
  also have "... = 1/2^7 * (x <nat (tm+1). (2 powr (-1)) powr (real x))"
    by (subst powr_powr) simp
  also have "... = 1/2^7 * (x <nat (tm+1). (1/2)^x)"
    using powr_realpow by simp
  also have "...  1/2^7 * 2"
    by(subst geometric_sum) auto
  also have "... = 1/2^6" by simp
  finally show ?thesis by simp
qed

definition E3 where "E3 = (λ(f,g,h). inj_on g (R f))"

lemma R_bound:
  fixes f g h
  assumes "E1 (f,g,h)"
  assumes "E2 (f,g,h)"
  shows "card (R f)  2/3 * b"
proof -
  have "real (card (R f))  ( ε / 3) * (real X / 2 ^ s f) + real X / 2 ^ s f"
    using assms(2) unfolding E2_def by simp
  also have "...  (1/3) * (real X / 2 ^ s f) + real X / 2 ^ s f"
    using ε_lt_1 by (intro add_mono mult_right_mono) auto
  also have "... = (4/3) * (real X / 2 powr s f)"
    using powr_realpow by simp
  also have "...  (4/3) * (real X / 2 powr t f)"
    unfolding s_def
    by (intro mult_left_mono divide_left_mono powr_mono) auto
  also have "... = (4/3) * (2 powr (-(of_int (t f))) * real X)"
    by (subst powr_minus_divide) simp
  also have "... = (4/3) * (2 powr (- t f) * real X)"
    by simp
  also have "...  (4/3) * (b/2)"
    using assms(1) unfolding E1_def
    by (intro mult_left_mono) auto
  also have "...  (2/3) * b" by simp
  finally show ?thesis by simp
qed

lemma e_3: "measure Ψ {ψ. E1 ψ  E2 ψ  ¬E3 ψ}  1/2^6" (is "?L  ?R")
proof -
  let  = "(λ(z,x,y) f. z < C7*b^2  x  R f  y  R f  x < y)"
  let  = "(λ(z,x,y) g. g x = z  g y = z)"

  have β_prob: "measure Ψ2 {g.  ω g}  (1/real (C7*b^2)^2)"
    if " ω f" for ω f
  proof -
    obtain x y z where ω_def: "ω = (z,x,y)" by (metis prod_cases3)
    have a:"prob_space.indep_vars Ψ2 (λi. discrete) (λx ω. ω x = z) I"
      if "I  {..<n}" "card I  2" for I
      by (intro  prob_space.indep_vars_compose2[OF _ hash_pro_indep[OF Ψ2]] that)
        (simp_all add:prob_space_measure_pmf)

    have "u  R f  u < n" for u
      unfolding R_def using A_range by auto
    hence b: "x < n" "y < n" "card {x, y} = 2"
      using that ω_def by auto
    have c: "z < C7*b2" using ω_def that by simp

    have "measure Ψ2 {g.  ω g} = measure Ψ2 {g. (ξ  {x,y}. g ξ = z)}"
      by (simp add:ω_def)
    also have "... = (ξ  {x,y}. measure Ψ2 {g. g ξ = z})"
      using b by (intro measure_pmf.split_indep_events[OF refl, where I="{x,y}"] a)
        (simp_all add:prob_space_measure_pmf)
    also have "... = (ξ  {x,y}. measure (map_pmf (λω. ω ξ) (sample_pro Ψ2)) {g. g = z}) "
      by (simp add:vimage_def)
    also have "... = (ξ  {x,y}. measure (𝒩 (C7 * b2)) {g. g=z})"
      using b hash_pro_component[OF Ψ2] by (intro prod.cong) fastforce+
    also have "... = (ξ  {x,y}. measure (pmf_of_set {..<C7 * b2}) {z})"
      by (subst nat_pro) (simp_all add:C7_def b_def)
    also have "... = (measure (pmf_of_set {..<C7 * b2}) {z})^2"
      using b by simp
    also have "...  (1 /(C7*b2))^2"
      using c by (subst measure_pmf_of_set) auto
    also have "... = (1 /(C7*b2)^2)"
      by (simp add:algebra_simps power2_eq_square)
    finally show ?thesis by simp
  qed

  have α_card: "card {ω.  ω f}  (C7*b^2) * (card (R f) * (card (R f)-1)/2)"
    (is "?TL  ?TR") and fin_α: "finite {ω.  ω f}" (is "?T2") for f
  proof -
    have t1: "{ω.  ω f}  {..<C7*b^2} × {(x,y)  R f × R f. x < y}"
      by (intro subsetI) auto
    moreover have "card ({..<C7*b^2} × {(x,y)  R f × R f. x < y}) = ?TR"
      using  card_ordered_pairs'[where M="R f"]
      by (simp add: card_cartesian_product)
    moreover have "finite (R f)"
      unfolding R_def using fin_A finite_subset by simp
    hence "finite {(x, y). (x, y)  R f × R f  x < y}"
      by (intro finite_subset[where B="R f × R f", OF _ finite_cartesian_product]) auto
    hence t2: "finite ({..<C7*b^2} × {(x,y)  R f × R f. x < y})"
      by (intro finite_cartesian_product) auto
    ultimately show "?TL  ?TR"
      using card_mono of_nat_le_iff by (metis (no_types, lifting))
    show ?T2
      using finite_subset[OF t1 t2] by simp
  qed

  have "?L  measure Ψ {(f,g,h). card (R f)  b  ( x y z.  (x,y,z) f   (x,y,z) g)}"
  proof (rule pmf_mono)
    fix ψ assume b:"ψ  set_pmf (sample_pro Ψ)"
    obtain f g h where ψ_def:"ψ = (f,g,h)" by (metis prod_cases3)
    have "(f,g,h)  pro_set Ψ" using b ψ_def by simp
    hence c:"g x < C7*b^2" for x
      using g_range by simp

    assume a:"ψ  {ψ. E1 ψ  E2 ψ  ¬ E3 ψ}"
    hence "card (R f)  2/3 * b"
      using R_bound ψ_def by force
    moreover have "a b. a  R f  b  R f  a  b  g a = g b"
      using a unfolding ψ_def E3_def inj_on_def by auto
    hence "x y. x  R f  y  R f  x < y  g x = g y"
      by (metis not_less_iff_gr_or_eq)
    hence "x y z.  (x,y,z) f   (x,y,z) g"
      using c by blast
    ultimately show "ψ  {(f, g, h). card (R f)  b  ( x y z.  (x,y,z) f   (x,y,z) g)}"
      unfolding ψ_def by auto
  qed
  also have "... = (f. measure (pair_pmf Ψ2 Ψ3)
     {g. card (R f)  b  (x y z.  (x,y,z) f   (x,y,z) (fst g))} Ψ1)"
    unfolding sample_pro_Ψ split_pair_pmf by (simp add: case_prod_beta)
  also have
    "... = (f. measure Ψ2 {g. card (R f)  b  (x y z.  (x,y,z) f   (x,y,z) g)} Ψ1)"
    by (subst pair_pmf_prob_left) simp
  also have "...  (f. 1/real (2*C7) Ψ1)"
  proof (rule pmf_exp_mono[OF integrable_sample_pro integrable_sample_pro])
    fix f assume "f  set_pmf (sample_pro Ψ1)"
    show "measure Ψ2 {g. card (R f)  b  (x y z.  (x,y,z) f   (x,y,z) g)}  1 / real (2 * C7)"
      (is "?L1  ?R1")
    proof (cases "card (R f)  b")
      case True
      have "?L1  measure Ψ2 ( ω  {ω.  ω f}. {g.  ω g})"
        by (intro pmf_mono) auto
      also have "...  (ω  {ω.  ω f}. measure Ψ2 {g.  ω g})"
        by (intro measure_UNION_le fin_α) auto
      also have "...  (ω  {ω.  ω f}. (1/real (C7*b^2)^2))"
        by (intro sum_mono β_prob) auto
      also have "... = card {ω.  ω f} /(C7*b^2)^2"
        by simp
      also have "...  (C7*b^2) * (card (R f) * (card (R f)-1)/2) / (C7*b^2)^2"
        by (intro α_card divide_right_mono) simp
      also have "...  (C7*b^2) * (b * b / 2)  / (C7*b^2)^2"
        unfolding C7_def using True
        by (intro divide_right_mono Nat.of_nat_mono mult_mono) auto
      also have "... = 1/(2*C7)"
        using b_min by (simp add:algebra_simps power2_eq_square)
      finally show ?thesis by simp
    next
      case False
      then show ?thesis by simp
    qed
  qed
  also have "...  1/2^6"
    unfolding C7_def by simp
  finally show ?thesis by simp
qed

definition E4 where "E4 = (λ(f,g,h). ¦p (f,g,h) - ρ (card (R f))¦   ε/12 * card (R f))"

lemma e_4_h: "9 / sqrt b  ε / 12"
proof -
  have "108  sqrt (C4)"
    unfolding C4_def by (approximation 5)
  also have "...  sqrt( ε^2 * real b)"
    using b_lower_bound ε_gt_0
    by (intro real_sqrt_le_mono) (simp add: pos_divide_le_eq algebra_simps)
  also have "... =  ε * sqrt b"
    using ε_gt_0 by (simp add:real_sqrt_mult)
  finally have "108   ε * sqrt b"  by simp
  thus ?thesis
    using b_min by (simp add:pos_divide_le_eq)
qed

lemma e_4: "measure Ψ {ψ. E1 ψ  E2 ψ  E3 ψ  ¬E4 ψ}  1/2^6" (is "?L  ?R")
proof -
  have a: "measure Ψ3 {h. E1 (f,g,h)  E2 (f,g,h)  E3 (f,g,h)  ¬E4 (f,g,h)}  1/2^6"
    (is "?L1  ?R1") if "f  set_pmf (sample_pro Ψ1)" "g  set_pmf(sample_pro Ψ2)"
    for f g
  proof (cases "card (R f)  b  inj_on g (R f)")
    case True

    have g_inj: "inj_on g (R f)"
      using True by simp

    have fin_R: "finite (g ` R f)"
      unfolding R_def using fin_A
      by (intro finite_imageI) simp

    interpret B:balls_and_bins_abs "g ` R f" "{..<b}"
      using fin_R b_ne by unfold_locales auto

    have "range g  {..<C7 * b2}"
      using g_range_1 that(2) by auto
    hence g_ran: "g ` R f  {..<C7 * b2}"
      by auto

    have "sample_pro (𝒩 b) = pmf_of_set {..<b}"
      by (intro nat_pro) (simp add:b_def)
    hence " map_pmf (λω. ω x) (sample_pro ( k (C7 * b2) (𝒩 b))) = pmf_of_set {..<b}"
      if "x  g ` R f" for x
      using g_ran hash_pro_component[OF Ψ3 _ k_gt_0] that by auto
    moreover have "prob_space.k_wise_indep_vars Ψ3 k (λ_. discrete) (λx ω. ω x) (g ` R f)"
      by (intro prob_space.k_wise_indep_subset[OF _ _ hash_pro_k_indep[OF Ψ3]] g_ran
          prob_space_measure_pmf)
    ultimately have lim_balls_and_bins: "B.lim_balls_and_bins k (sample_pro ( k (C7 * b2) (𝒩 b)))"
      unfolding B.lim_balls_and_bins_def by auto

    have card_g_R: "card (g ` R f) = card (R f)"
      using True card_image by auto
    hence b_mu: "ρ (card (R f)) = B.μ"
      unfolding B.μ_def ρ_def using b_min by (simp add:powr_realpow)

    have card_g_le_b: "card (g ` R f)  card {..<b}"
      unfolding card_g_R using True by simp

    have "?L1  measure Ψ3 {h. ¦B.Y h - B.μ¦ > 9 * real (card (g ` R f)) / sqrt (card {..<b})}"
    proof (rule pmf_mono)
      fix h assume "h  {h. E1 (f,g,h)  E2 (f,g,h)  E3 (f,g,h)  ¬E4 (f,g,h)}"
      hence b: "¦p (f,g,h) -ρ (card (R f))¦ >  ε/12 * card (R f)"
        unfolding E4_def by simp
      assume "h  set_pmf (sample_pro Ψ3)"
      hence h_range: "h x < b" for x using h_range_1 by simp

      have "{j  {..<b}. int (s f)  τ1 (f, g, h) A 0 j} =
        {j  {..<b}. int (s f)  max (Max ({int (f a) |a. a  A  h (g a) = j}  {-1})) (- 1)}"
        unfolding τ1_def by simp
      also have "... = {j  {..<b}. int (s f)  Max ({int (f a) |a. a  A  h (g a) = j}  {-1})}"
        using fin_A by (subst max_absorb1) (auto intro: Max_ge)
      also have "... = {j  {..<b}. (a  R f. h (g a) = j)}"
        unfolding R_def using fin_A by (subst Max_ge_iff) auto
      also have "... = {j. a  R f. h (g a) = j}"
        using h_range by auto
      also have "... = (h  g) ` (R f)"
        by (auto simp add:set_eq_iff image_iff)
      also have "... = h ` (g ` (R f))"
        by (simp add:image_image)
      finally have c:"{j  {..<b}. int (s f)  τ1 (f, g, h) A 0 j} = h ` (g ` R f)"
        by simp
      have "9 * real (card (g ` R f)) / sqrt (card {..<b}) = 9/ sqrt b * real (card (R f))"
        using card_image[OF g_inj] by simp
      also have "...   ε/12 * card (R f)"
        by (intro mult_right_mono e_4_h) simp
      also have "... < ¦B.Y h - B.μ¦"
        using b c unfolding B.Y_def p_def b_mu by simp
      finally show "h  {h. ¦B.Y h - B.μ¦ >  9 * real (card (g ` R f)) / sqrt (card {..<b})}"
        by simp
    qed
    also have "...  1/2^6"
      using k_min
      by (intro B.devitation_bound[OF card_g_le_b lim_balls_and_bins]) auto
    finally show ?thesis by simp
  next
    case False
    have "?L1  measure Ψ3 {}"
    proof (rule pmf_mono)
      fix h assume b:"h  {h. E1 (f, g, h)  E2 (f, g, h)  E3 (f, g, h)  ¬ E4 (f, g, h)}"
      hence "card (R f)  (2/3)*b"
        by (auto intro!: R_bound[simplified])
      hence "card (R f)  b"
        by simp
      moreover have "inj_on g (R f)"
        using b by (simp add:E3_def)
      ultimately have "False" using False by simp
      thus "h  {}" by simp
    qed
    also have "... = 0" by simp
    finally show ?thesis by simp
  qed

  have "?L = (f. (g.
    measure Ψ3 {h. E1 (f,g,h)  E2 (f,g,h)  E3 (f,g,h)  ¬E4 (f,g,h)} Ψ2) Ψ1)"
    unfolding sample_pro_Ψ split_pair_pmf by simp
  also have "...  (f. (g.  1/2^6  Ψ2) Ψ1)"
    using a by (intro integral_mono_AE AE_pmfI) simp_all
  also have "... = 1/2^6"
    by simp
  finally show ?thesis by simp
qed

lemma ρ_inverse: "ρ_inv (ρ x) = x"
proof -
  have a:"1-1/b  0"
    using b_min by simp

  have "ρ x = b * (1-(1-1/b) powr x)"
    unfolding ρ_def by simp
  hence "ρ x / real b = 1-(1-1/b) powr x" by simp
  hence "ln (1 - ρ x / real b) = ln ((1-1/b) powr x)" by simp
  also have "... = x * ln (1 - 1/ b)"
    using a by (intro ln_powr)
  finally have "ln (1 - ρ x / real b) = x * ln (1- 1/ b)"
    by simp
  moreover have "ln (1-1/b) < 0"
    using b_min by (subst ln_less_zero_iff) auto
  ultimately show ?thesis
    using ρ_inv_def by simp
qed

lemma rho_mono:
  assumes "x  y"
  shows "ρ x  ρ y"
proof-
  have "(1 - 1 / real b) powr y  (1 - 1 / real b) powr x"
    using b_min
    by (intro powr_mono_rev assms) auto
  thus ?thesis
    unfolding ρ_def by (intro mult_left_mono) auto
qed

lemma rho_two_thirds: "ρ (2/3 * b)  3/5 *b"
proof -
  have "1/3  exp ( - 13 / 12::real )"
    by (approximation 8)
  also have "...  exp ( - 1 - 2 / real b )"
    using b_min by (intro iffD2[OF exp_le_cancel_iff]) (simp add:algebra_simps)
  also have "...  exp ( b * (-(1/real b)-2*(1/real b)^2))"
    using b_min by (simp add:algebra_simps power2_eq_square)
  also have  "...  exp ( b * ln (1-1/real b))"
    using b_min
    by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono ln_one_minus_pos_lower_bound) auto
  also have "... = exp ( ln ( (1-1/real b) powr b))"
    using b_min by (subst ln_powr) auto
  also have "... = (1-1/real b) powr b"
    using b_min by (subst exp_ln) auto
  finally have a:"1/3  (1-1/real b) powr b" by simp

  have "2/5  (1/3) powr (2/3::real)"
    by (approximation 5)
  also have "...  ((1-1/real b) powr b) powr (2/3)"
    by (intro powr_mono2 a) auto
  also have "... = (1-1/real b) powr (2/3 * real b)"
    by (subst powr_powr) (simp add:algebra_simps)
  finally have "2/5  (1 - 1 / real b) powr (2 / 3 * real b)" by simp
  hence "1 - (1 - 1 / real b) powr (2 / 3 * real b)  3/5"
    by simp
  hence "ρ (2/3 * b)  b * (3/5)"
    unfolding ρ_def by (intro mult_left_mono) auto
  thus ?thesis
    by simp
qed

definition ρ_inv' :: "real  real"
  where "ρ_inv' x = -1 / (real b * (1-x / real b) * ln (1 - 1 / real b))"

lemma ρ_inv'_bound:
  assumes "x  0"
  assumes "x  59/90*b"
  shows "¦ρ_inv' x¦  4"
proof -
  have c:"ln (1 - 1 / real b) < 0"
    using b_min
    by (subst ln_less_zero_iff) auto
  hence d:"real b * (1 - x / real b) * ln (1 - 1 / real b) < 0"
    using b_min assms by (intro Rings.mult_pos_neg) auto

  have "(1::real)  31/30" by simp
  also have "...  (31/30) * (b * -(- 1 / real b))"
    using b_min by simp
  also have "...  (31/30) * (b * -ln (1 + (- 1 / real b)))"
    using b_min
    by (intro mult_left_mono le_imp_neg_le  ln_add_one_self_le_self2) auto
  also have "...  3 * (31/90) * (- b * ln (1 - 1 / real b))"
    by simp
  also have "...  3 * (1 - x / real b) * (- b * ln (1 - 1 / real b))"
    using assms b_min pos_divide_le_eq[where c="b"] c
    by (intro mult_right_mono mult_left_mono mult_nonpos_nonpos) auto
  also have "...  3 * (real b * (1 - x / real b) * (-ln (1 - 1 / real b)))"
    by (simp add:algebra_simps)
  finally have "3 * (real b * (1 - x / real b) * (-ln (1 - 1 / real b)))  1" by simp
  hence "3 * (real b * (1 - x / real b) * ln (1 - 1 / real b))  -1" by simp
  hence "ρ_inv' x  3"
    unfolding ρ_inv'_def using d
    by (subst neg_divide_le_eq) auto
  moreover have "ρ_inv' x > 0"
    unfolding ρ_inv'_def using d by (intro divide_neg_neg) auto
  ultimately show ?thesis by simp
qed

lemma ρ_inv':
  fixes x :: real
  assumes "x < b"
  shows "DERIV ρ_inv x :> ρ_inv' x"
proof -
  have "DERIV (ln  (λx. (1 - x / real b))) x :> 1 / (1-x / real b) * (0 -1/b)"
    using assms b_min
    by (intro DERIV_chain DERIV_ln_divide DERIV_cdivide derivative_intros) auto
  hence "DERIV ρ_inv x :> (1 / (1-x / real b) * (-1/b)) / ln (1-1/real b)"
    unfolding comp_def ρ_inv_def by (intro DERIV_cdivide) auto
  thus ?thesis
    by (simp add:ρ_inv'_def algebra_simps)
qed

lemma accuracy_without_cutoff:
  "measure Ψ {(f,g,h). ¦Y (f,g,h) - real X¦ > ε * X  s f < q_max}  1/2^4"
  (is "?L  ?R")
proof -
  have "?L  measure Ψ {ψ. ¬E1 ψ   ¬E2 ψ   ¬E3 ψ   ¬E4 ψ}"
  proof (rule pmf_rev_mono)
    fix ψ assume "ψ  set_pmf (sample_pro Ψ)"
    obtain f g h where ψ_def: "ψ = (f,g,h)" by (metis prod_cases3)

    assume "ψ  {ψ. ¬ E1 ψ  ¬ E2 ψ  ¬ E3 ψ  ¬ E4 ψ}"
    hence assms: "E1 (f,g,h)" "E2 (f,g,h)" "E3 (f,g,h)" "E4 (f,g,h)"
      unfolding ψ_def by auto

    define I :: "real set" where "I = {0..59/90*b}"

    have "p (f,g,h)  ρ (card (R f)) + ε/12 * card (R f)"
      using assms(4) E4_def unfolding abs_le_iff by simp
    also have "...  ρ(2/3*b) + 1/12* (2/3*b)"
      using ε_lt_1 R_bound[OF assms(1,2)]
      by (intro add_mono rho_mono mult_mono) auto
    also have "...  3/5 * b + 1/18*b"
      by (intro add_mono rho_two_thirds) auto
    also have "...  59/90 * b"
       by simp
    finally have "p (f,g,h)  59/90 * b" by simp
    hence p_in_I: "p (f,g,h)  I"
      unfolding I_def by simp

    have "ρ (card (R f))  ρ(2/3 * b)"
      using  R_bound[OF assms(1,2)]
      by (intro rho_mono) auto
    also have "...  3/5 * b"
      using rho_two_thirds by simp
    also have "...  b * 59/90" by simp
    finally have "ρ (card (R f))  b * 59/90" by simp
    moreover have "(1 - 1 / real b) powr (real (card (R f)))  1 powr (real (card (R f)))"
      using b_min by (intro powr_mono2) auto
    hence "ρ (card (R f))  0"
      unfolding ρ_def by (intro mult_nonneg_nonneg) auto
    ultimately have "ρ (card (R f))  I"
      unfolding I_def by simp

    moreover have "interval I"
      unfolding I_def interval_def by simp
    moreover have "59 / 90 * b < b"
      using b_min by simp
    hence "DERIV ρ_inv x :> ρ_inv' x" if "x  I" for x
      using that I_def by (intro ρ_inv') simp
    ultimately obtain ξ :: real where ξ_def: "ξ  I"
      "ρ_inv (p(f,g,h)) - ρ_inv (ρ (card (R f))) = (p (f,g,h) - ρ(card (R f))) * ρ_inv' ξ"
      using p_in_I MVT_interval by blast

    have "¦ρ_inv(p (f,g,h)) - card (R f)¦ = ¦ρ_inv(p (f,g,h)) - ρ_inv(ρ(card (R f)))¦"
      by (subst ρ_inverse) simp
    also have "... = ¦(p (f,g,h) - ρ (card (R f)))¦ * ¦ρ_inv' ξ ¦"
      using ξ_def(2) abs_mult by simp
    also have "...  ¦p (f,g,h) - ρ (card (R f))¦ * 4"
      using ξ_def(1) I_def
      by (intro mult_left_mono ρ_inv'_bound) auto
    also have "...  ( ε/12 * card (R f)) * 4"
      using assms(4) E4_def by (intro mult_right_mono) auto
    also have "... = ε/3 * card (R f)" by simp
    finally have b: "¦ρ_inv(p (f,g,h)) - card (R f)¦  ε/3 * card (R f)"  by simp

    have "¦ρ_inv(p (f,g,h)) - X / 2 ^ (s f)¦ 
      ¦ρ_inv(p (f,g,h)) - card (R f)¦ + ¦card (R f) - X / 2 ^ (s f)¦"
      by simp
    also have "...  ε/3 * card (R f) + ¦card (R f) - X / 2 ^ (s f)¦"
      by (intro add_mono b) auto
    also have "... =  ε/3 * ¦X / 2 ^ (s f) + (card (R f) - X / 2 ^ (s f))¦ +
      ¦card (R f) - X / 2 ^ (s f)¦" by simp
    also have "...   ε/3 * (¦X / 2 ^ (s f)¦ + ¦card (R f) - X / 2 ^ (s f)¦) +
      ¦card (R f) - X / 2 ^ (s f)¦"
      using ε_gt_0 by (intro mult_left_mono add_mono abs_triangle_ineq) auto
    also have "...   ε/3 * ¦X / 2 ^ (s f)¦ + (1+  ε/3) * ¦card (R f) - X / 2 ^ (s f)¦"
      using ε_gt_0 ε_lt_1 by (simp add:algebra_simps)
    also have "...   ε/3 * ¦X / 2 ^ s f¦ + (4/3) * ( ε / 3 * real X / 2 ^ s f)"
      using assms(2) ε_gt_0 ε_lt_1
      unfolding E2_def by (intro add_mono mult_mono) auto
    also have "... = (7/9) * ε * real X / 2^s f"
      using X_ge_1 by (subst abs_of_nonneg) auto
    also have "...  1 * ε * real X / 2^s f"
      using ε_gt_0 by (intro mult_mono divide_right_mono) auto
    also have "... =  ε * real X / 2^s f" by simp
    finally have a:"¦ρ_inv(p (f,g,h)) - X / 2 ^ (s f)¦  ε * X / 2 ^ (s f)"
      by simp

    have "¦Y (f, g, h) - real X¦ = ¦2 ^ (s f)¦ * ¦ρ_inv(p (f,g,h)) - real X / 2 ^ (s f)¦"
      unfolding Y_def by (subst abs_mult[symmetric]) (simp add:algebra_simps powr_add[symmetric])
    also have "...  2 ^ (s f) * (ε * X / 2 ^ (s f))"
      by (intro mult_mono a) auto
    also have "... = ε * X"
      by (simp add:algebra_simps powr_add[symmetric])
    finally have "¦Y (f, g, h) - real X¦  ε * X" by simp
    moreover have "2 powr (log 2 (real X) - t f)  2 powr b_exp" (is "?L1  ?R1")
    proof -
      have "?L1  2 powr (1 + log 2 (real X)- t f)"
        by (intro powr_mono, linarith) auto
      also have "... = 2 powr 1 * 2 powr (log 2 (real X)) * 2 powr (- t f)"
        unfolding powr_add[symmetric] by simp
      also have "... = 2 * (2 powr (-t f) * X)"
        using X_ge_1 by simp
      also have "...  2 * (b/2)"
        using assms(1) unfolding E1_def by (intro mult_left_mono) auto
      also have "... = b" by simp
      also have "... = ?R1"
        unfolding b_def by (simp add: powr_realpow)
      finally show ?thesis by simp
    qed
    hence "log 2 (real X) - t f  real b_exp"
      unfolding not_less[symmetric] using powr_less_mono[where x="2"] by simp
    hence "s f  q_max" unfolding s_def q_max_def by (intro nat_mono) auto
    ultimately show "ψ  {(f, g, h). ε * X < ¦Y (f, g, h) - real X¦  s f < q_max}"
      unfolding ψ_def by auto
  qed
  also have "... 
    measure Ψ {ψ. ¬E1 ψ  ¬E2 ψ  ¬E3 ψ} + measure Ψ {ψ. E1 ψ  E2 ψ  E3 ψ  ¬E4 ψ}"
    by (intro pmf_add) auto
  also have "...  (measure Ψ {ψ. ¬E1 ψ  ¬E2 ψ} + measure Ψ {ψ. E1 ψ  E2 ψ  ¬E3 ψ}) + 1/2^6"
    by (intro add_mono e_4 pmf_add) auto
  also have "...  ((measure Ψ {ψ. ¬E1 ψ} + measure Ψ {ψ. E1 ψ  ¬E2 ψ}) + 1/2^6) + 1/2^6"
    by (intro add_mono e_3 pmf_add) auto
  also have "...  ((1/2^6 + 1/2^6) + 1/2^6) + 1/2^6"
    by (intro add_mono e_2 e_1) auto
  also have "... = ?R" by simp
  finally show ?thesis by simp
qed

end

end