Theory Distributed_Distinct_Elements_Inner_Algorithm

section ‹Inner Algorithm\label{sec:inner_algorithm}›

text ‹This section introduces the inner algorithm (as mentioned it is already a solution to the
cardinality estimation with the caveat that, if $\varepsilon$ is too small it requires to much
space. The outer algorithm in Section~\ref{sec:outer_algorithm} resolved this problem.

The algorithm makes use of the balls and bins model, more precisely, the fact that the number of
hit bins can be used to estimate the number of balls thrown (even if there are collusions). I.e.
it assigns each universe element to a bin using a $k$-wise independent hash function. Then it
counts the number of bins hit.

This strategy however would only work if the number of balls is roughly equal to the number of
bins, to remedy that the algorithm performs an adaptive sub-sampling strategy. This works by
assigning each universe element a level (using a second hash function) with a geometric
distribution. The algorithm then selects a level that is appropriate based on a rough estimate
obtained using the maximum level in the bins.

To save space the algorithm drops information about small levels, whenever the space usage would
be too high otherwise. This level will be called the cutoff-level. This is okey as long as the
cutoff level is not larger than the sub-sampling threshold. A lot of the complexity in the
proof is devoted to verifying that the cutoff-level will not cross it, it works by defining a
third value @{term "sM"} that is both an upper bound for the cutoff level and a lower bound for the
subsampling threshold simultaneously with high probability.›

theory Distributed_Distinct_Elements_Inner_Algorithm
  imports
    Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
    Distributed_Distinct_Elements_Preliminary
    Distributed_Distinct_Elements_Balls_and_Bins
    Distributed_Distinct_Elements_Tail_Bounds
    Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
begin

unbundle intro_cong_syntax
hide_const Abstract_Rewriting.restrict

definition C4 :: real where "C4 = 3^2*2^23"
definition C5 :: int where "C5 = 33"
definition C6 :: real where "C6 = 4"
definition C7 :: nat where "C7 = 2^5"

locale inner_algorithm =
  fixes n :: nat
  fixes δ :: real
  fixes ε :: real
  assumes n_gt_0: "n > 0"
  assumes δ_gt_0: "δ > 0" and δ_lt_1: "δ < 1"
  assumes ε_gt_0: "ε > 0" and ε_lt_1: "ε < 1"
begin

definition b_exp where "b_exp = nat log 2 (C4 / ε^2)"
definition b :: nat where "b = 2^b_exp"
definition l where "l = nat C6 * ln (2/ δ)"
definition k where "k = nat C2*ln b + C3"
definition Λ :: real where "Λ = min (1/16) (exp (-l * ln l^3))"
definition ρ :: "real  real" where "ρ x = b * (1 - (1-1/b) powr x)"
definition ρ_inv :: "real  real" where "ρ_inv x = ln (1-x/b) / ln (1-1/b)"

lemma l_lbound: "C6 * ln (2 / δ)  l"
  unfolding l_def by linarith

lemma k_min: "C2 * ln (real b) + C3  real k"
  unfolding k_def by linarith

lemma Λ_gt_0: "Λ > 0"
  unfolding Λ_def min_less_iff_conj by auto

lemma Λ_le_1: "Λ  1"
  unfolding Λ_def by auto

lemma l_gt_0: "l > 0"
proof -
  have "0 < C6 * ln (2 / δ)"
    unfolding C6_def using δ_gt_0 δ_lt_1
    by (intro Rings.mult_pos_pos ln_gt_zero) auto
  also have "...  l"
    by (intro l_lbound)
  finally show ?thesis
    by simp
qed

lemma l_ubound: "l  C6 * ln(1 / δ)+C6*ln 2 + 1"
proof -
  have "l = of_int C6 * ln (2/ δ)"
    using l_gt_0 unfolding l_def
    by (intro of_nat_nat) simp
  also have "...  C6 * ln (1/ δ*2)+1"
    by simp
  also have "... = C6 * ln (1/ δ)+C6 * ln 2+1"
    using δ_gt_0 δ_lt_1
    by (subst ln_mult) (auto simp add:algebra_simps)
  finally show ?thesis by simp
qed

lemma b_exp_ge_26: "b_exp  26"
proof -
  have "2 powr 25 < C4 / 1 " unfolding C4_def by simp
  also have "...  C4 / ε^2"
    using ε_gt_0 ε_lt_1 unfolding C4_def
    by (intro divide_left_mono power_le_one) auto
  finally have "2 powr 25 < C4 / ε^2" by simp
  hence "log 2 (C4 / ε^2) > 25"
    using ε_gt_0 unfolding C4_def
    by (intro iffD2[OF less_log_iff] divide_pos_pos zero_less_power) auto
  hence "log 2 (C4 / ε^2)  26" by simp
  thus ?thesis
    unfolding b_exp_def by linarith
qed

lemma b_min: "b  2^26"
  unfolding b_def
  by (meson b_exp_ge_26  nat_power_less_imp_less not_less power_eq_0_iff power_zero_numeral)

lemma k_gt_0: "k > 0"
proof -
  have "(0::real) < 7.5 * 0 + 16" by simp
  also have "...  7.5 * ln(real b) + 16"
    using b_min
    by (intro add_mono mult_left_mono ln_ge_zero) auto
  finally have "0 < real k"
    using k_min unfolding C2_def C3_def by simp
  thus ?thesis by simp
qed

lemma b_ne: "{..<b}  {}"
proof -
  have "0  {0..<b}"
    using b_min by simp
  thus ?thesis
    by auto
qed

lemma b_lower_bound: "C4 / ε^2  real b"
proof -
  have "C4 /  ε^2 = 2 powr (log 2 (C4 / ε^2))"
    using ε_gt_0 unfolding C4_def by (intro powr_log_cancel[symmetric] divide_pos_pos) auto
  also have "...  2 powr (nat log 2 (C4 /  ε^2))"
    by (intro powr_mono of_nat_ceiling) simp
  also have "... = real b"
    unfolding b_def b_exp_def by (simp add:powr_realpow)
  finally show ?thesis by simp
qed

definition n_exp where "n_exp = max (nat log 2 n) 1"

lemma n_exp_gt_0: "n_exp > 0"
  unfolding n_exp_def by simp

abbreviation Ψ1 where "Ψ1   2 n (𝒢 n_exp)"
abbreviation Ψ2 where "Ψ2   2 n (𝒩 (C7*b2))"
abbreviation Ψ3 where "Ψ3   k (C7*b2) (𝒩 b)"

definition Ψ where "Ψ = Ψ1 ×P Ψ2 ×P Ψ3"

abbreviation Ω where "Ω   l Λ Ψ"

type_synonym state = "(nat  nat  int) × (nat)"

fun is_too_large :: "(nat  nat  int)  bool" where
  "is_too_large B = (( (i,j)  {..<l} × {..<b}. log 2 (max (B i j) (-1) + 2)) > C5 * b * l)"

fun compress_step :: "state  state" where
  "compress_step (B,q) = (λ i j. max (B i j - 1) (-1), q+1)"

function compress :: "state  state" where
  "compress (B,q) = (
    if is_too_large B
      then (compress (compress_step (B,q)))
      else (B,q))"
  by auto

fun compress_termination :: "state  nat" where
  "compress_termination (B,q) = ( (i,j)  {..<l} × {..<b}. nat (B i j + 1))"

lemma compress_termination:
  assumes "is_too_large B"
  shows "compress_termination (compress_step (B,q)) < compress_termination (B,q)"
proof (rule ccontr)
  let ?I = "{..<l} × {..<b}"
  have a: "nat (max (B i j - 1) (- 1) + 1)  nat (B i j + 1)" for i j
    by simp
  assume "¬ compress_termination (compress_step (B, q)) < compress_termination (B, q)"
  hence "( (i,j)  ?I. nat (B i j + 1))  ( (i,j)  ?I. nat (max (B i j - 1) (-1) + 1))"
    by simp
  moreover have "( (i,j)  ?I. nat (B i j + 1))  ( (i,j)  ?I. nat (max (B i j - 1) (-1) + 1))"
    by (intro sum_mono) auto
  ultimately have b:
    "( (i,j)  ?I. nat (max (B i j - 1) (-1) + 1)) = ( (i,j)  ?I. nat (B i j + 1))"
    using order_antisym by simp
  have "nat (B i j + 1) = nat (max (B i j - 1) (-1) + 1)" if "(i,j)  ?I" for i j
    using sum_mono_inv[OF b] that a by auto
  hence "max (B i j) (-1) = -1" if "(i,j)  ?I" for i j
    using that by fastforce
  hence "((i,j)  ?I. log 2 (max (B i j) (-1) + 2)) = ((i,j)  ?I. 0)"
    by (intro sum.cong, auto)
  also have "... = 0" by simp
  also have "...  C5 * b * l" unfolding C5_def by simp
  finally have "¬ is_too_large B" by simp
  thus "False" using assms by simp
qed

termination compress
  using measure_def compress_termination
  by (relation "Wellfounded.measure (compress_termination)", auto)

fun merge1 :: "state  state  state" where
  "merge1 (B1,q1) (B2, q2) = (
    let q = max q1 q2 in (λ i j. max (B1 i j + q1 - q) (B2 i j + q2 - q), q))"

fun merge :: "state  state  state" where
  "merge x y = compress (merge1 x y)"

type_synonym seed = "nat  (nat  nat) × (nat  nat) × (nat  nat)"

fun single1 :: "seed  nat  state" where
  "single1 ω x = (λ i j.
     let (f,g,h) = ω i in (
     if h (g x) = j  i < l then int (f x) else (-1)), 0)"

fun single :: "seed  nat  state" where
  "single ω x = compress (single1 ω x)"

fun estimate1 :: "state  nat  real" where
  "estimate1 (B,q) i = (
    let s = max 0 (Max ((B i) ` {..<b}) + q - log 2 b + 9);
        p = card { j. j  {..<b}  B i j + q  s } in
        2 powr s * ln (1-p/b) / ln(1-1/b))"

fun estimate :: "state  real" where
  "estimate x = median l (estimate1 x)"

subsection ‹History Independence›

fun τ0 :: "((nat  nat) × (nat  nat) × (nat  nat))  nat set  nat  int"
  where "τ0 (f,g,h) A j = Max ({ int (f a) | a . a  A  h (g a) = j }  {-1}) "

definition τ1 :: "((nat  nat) × (nat  nat) × (nat  nat))  nat set  nat  nat  int"
  where "τ1 ψ A q j = max (τ0 ψ A j - q) (-1)"

definition τ2 :: "seed  nat set  nat  nat  nat  int"
  where "τ2 ω A q i j = (if i < l then τ1 (ω i) A q j else (-1))"

definition τ3 :: "seed  nat set  nat  state"
  where "τ3 ω A q = (τ2 ω A q, q)"

definition q :: "seed  nat set  nat"
  where "q ω A = (LEAST q . ¬(is_too_large (τ2 ω A q)))"

definition τ :: "seed  nat set  state"
  where "τ ω A = τ3 ω A (q ω A)"

lemma τ2_step: "τ2 ω A (x+y) = (λi j. max (τ2 ω A x i j - y) (- 1))"
  by (intro ext) (auto simp add:τ2_def τ1_def)

lemma τ3_step: "compress_step (τ3 ω A x) = τ3 ω A (x+1)"
  unfolding τ3_def using τ2_step[where y="1"] by simp

lemma Ψ1: "is_prime_power (pro_size (𝒢 n_exp))"
  unfolding geom_pro_size by (intro is_prime_powerI n_exp_gt_0) auto

lemma Ψ2: "is_prime_power (pro_size (𝒩 (C7 * b^2)))"
proof -
  have 0:"pro_size (𝒩 (C7 * b^2)) = 2 ^ (5 + 2 * b_exp)"
    unfolding C7_def b_def by (subst nat_pro_size) (auto simp add: power_add power_even_eq)
  thus ?thesis unfolding 0 by (intro is_prime_powerI) auto
qed

lemma Ψ3: "is_prime_power (pro_size (𝒩 b))"
proof -
  have 0:"pro_size (𝒩 b) = 2 ^ b_exp" unfolding b_def by (subst nat_pro_size) auto
  thus ?thesis using b_exp_ge_26 unfolding 0 by (intro is_prime_powerI) auto
qed

lemma sample_pro_Ψ:
  "sample_pro Ψ = pair_pmf (sample_pro Ψ1) (pair_pmf (sample_pro Ψ2) (sample_pro Ψ3))"
  unfolding Ψ_def by (simp add:prod_pro)

lemma sample_set_Ψ: "pro_set Ψ = pro_set Ψ1 × pro_set Ψ2 × pro_set Ψ3"
  unfolding Ψ_def by (simp add:prod_pro_set)

lemma f_range:
  assumes "(f,g,h)  pro_set Ψ"
  shows "f x  n_exp"
proof -
  have "f  pro_set Ψ1" using sample_set_Ψ assms by auto
  hence "f  pro_select Ψ1 ` {..<pro_size Ψ1}" unfolding set_sample_pro by auto
  hence "f x  pro_set (𝒢 n_exp)" using hash_pro_range[OF Ψ1] by auto
  thus ?thesis using geom_pro_range by auto
qed

lemma g_range_1:
  assumes "g  pro_set Ψ2"
  shows "g x < C7*b^2"
proof -
  have "g  pro_select Ψ2 ` {..<pro_size Ψ2}" using assms unfolding set_sample_pro by auto
  hence "g x  pro_set (𝒩 ( C7*b^2))" using hash_pro_range[OF Ψ2] by auto
  moreover have "C7*b^2  > 0" unfolding C7_def b_def by simp
  ultimately show ?thesis using nat_pro_set by auto
qed

lemma h_range_1:
  assumes "h  pro_set Ψ3"
  shows "h x < b"
proof -
  have "h  pro_select Ψ3 ` {..<pro_size Ψ3}" using assms unfolding set_sample_pro by auto
  hence "h x  pro_set (𝒩 b)" using hash_pro_range[OF Ψ3] by auto
  moreover have "b  > 0" unfolding b_def by simp
  ultimately show ?thesis using nat_pro_set by auto
qed

lemma g_range:
  assumes "(f,g,h)  pro_set Ψ"
  shows "g x < C7*b^2"
  using g_range_1 sample_set_Ψ assms by simp

lemma h_range:
  assumes "(f,g,h)  pro_set Ψ"
  shows "h x < b"
  using h_range_1 sample_set_Ψ assms by simp

lemma fin_f:
  assumes "(f,g,h)  pro_set Ψ"
  shows "finite { int (f a) | a. P a }" (is "finite ?M")
proof -
  have "finite (range f)"
    using f_range[OF assms] finite_nat_set_iff_bounded_le by auto
  hence "finite (range (int  f))"
    by (simp add:image_image[symmetric])
  moreover have "?M  (range (int  f))"
    using image_mono by (auto simp add: setcompr_eq_image)
  ultimately show ?thesis
    using finite_subset by auto
qed

lemma Max_int_range: "x  (y::int)  Max {x..y} = y"
  by auto

lemma Ω: "l > 0" "Λ > 0" using l_gt_0 Λ_gt_0 by auto

lemma ω_range:
  assumes "ω  pro_set Ω"
  shows "ω i  pro_set Ψ"
proof -
  have "ω  pro_select Ω ` {..<pro_size Ω}" using assms unfolding set_sample_pro by auto
  thus "ω i  pro_set Ψ" using expander_pro_range[OF Ω] assms by auto
qed

lemma max_q_1:
  assumes "ω  pro_set Ω"
  shows "τ2 ω A (nat log 2 n+2) i j = (-1)"
proof (cases "i < l")
  case True
  obtain f g h where w_i: "ω i = (f,g,h)" by (metis prod_cases3)

  let ?max_q = "max log 2 (real n) 1"

  have c: "(f,g,h)  pro_set Ψ" using ω_range[OF assms] w_i[symmetric] by auto
  have a:"int (f x)  ?max_q" for x
  proof -
    have "int (f x)  int n_exp"
      using f_range[OF c] by auto
    also have "... = ?max_q" unfolding n_exp_def by simp
    finally show ?thesis by simp
  qed
  have "τ0 (ω i) A j  Max {(-1)..?max_q}"
    unfolding w_i τ0.simps using a by (intro Max_mono)  auto
  also have "... = ?max_q"
    by (intro Max_int_range) auto
  finally have "τ0 (ω i) A j  ?max_q" by simp
  hence "max (τ0 (ω i) A j - int (nat log 2 (real n) + 2)) (- 1) = (-1)"
    by (intro max_absorb2) linarith
  thus ?thesis
    unfolding τ2_def τ1_def using True by auto
next
  case False
  thus ?thesis unfolding τ2_def τ1_def by simp
qed

lemma max_q_2:
  assumes "ω  pro_set Ω"
  shows "¬ (is_too_large (τ2 ω A (nat log 2 n+2)))"
  using max_q_1[OF assms] by (simp add:C5_def case_prod_beta mult_less_0_iff)

lemma max_s_3:
  assumes "ω  pro_set Ω"
  shows "q ω A  (nat log 2 n+2)"
  unfolding q_def by (intro wellorder_Least_lemma(2) max_q_2 assms)

lemma max_mono: "x  (y::'a::linorder)  max x z  max y z"
  using max.coboundedI1 by auto

lemma max_mono_2: "y  (z::'a::linorder)  max x y  max x z"
  using max.coboundedI2 by auto

lemma τ0_mono:
  assumes "ψ  pro_set Ψ"
  assumes "A  B"
  shows "τ0 ψ A j  τ0 ψ B j"
proof -
  obtain f g h where w_i: "ψ = (f,g,h)"
    by (metis prod_cases3)
  show ?thesis
    using assms fin_f unfolding τ0.simps w_i
    by (intro Max_mono) auto
qed

lemma τ2_mono:
  assumes "ω  pro_set Ω"
  assumes "A  B"
  shows "τ2 ω A x i j  τ2 ω B x i j"
proof -
  have "max (τ0 (ω i) A j - int x) (- 1)  max (τ0 (ω i) B j - int x) (- 1)" if "i < l"
    using that ω_range[OF assms(1)] by (intro max_mono diff_mono τ0_mono assms(2) order.refl)
  thus ?thesis by (cases "i < l") (auto simp add:τ2_def τ1_def)
qed

lemma is_too_large_antimono:
  assumes "ω  pro_set Ω"
  assumes  "A  B"
  assumes "is_too_large (τ2 ω A x)"
  shows "is_too_large (τ2 ω B x)"
proof -
  have "C5 * b * l < ( (i,j)  {..<l} × {..<b}. log 2 (max (τ2 ω A x i j) (-1) + 2))"
    using assms(3) by simp
  also have "... = ( y  {..<l} × {..<b}.  log 2 (max (τ2 ω A x (fst y) (snd y)) (-1) + 2))"
    by (simp add:case_prod_beta)
  also have "...  ( y  {..<l} × {..<b}.  log 2 (max (τ2 ω B x (fst y) (snd y)) (-1) + 2))"
    by (intro sum_mono floor_mono iffD2[OF log_le_cancel_iff] iffD2[OF of_int_le_iff]
        add_mono max_mono τ2_mono[OF assms(1,2)]) auto
  also have "... = ( (i,j)  {..<l} × {..<b}.  log 2 (max (τ2 ω B x i j) (-1) + 2))"
    by (simp add:case_prod_beta)
  finally have "( (i,j)  {..<l} × {..<b}.  log 2 (max (τ2 ω B x i j) (-1) + 2)) > C5 * b * l"
    by simp
  thus ?thesis by simp
qed

lemma q_compact:
  assumes "ω  pro_set Ω"
  shows "¬ (is_too_large (τ2 ω A (q ω A)))"
  unfolding q_def using max_q_2[OF assms]
  by (intro wellorder_Least_lemma(1)) blast

lemma q_mono:
  assumes "ω  pro_set Ω"
  assumes "A  B"
  shows "q ω A  q ω B"
proof -
  have "¬ (is_too_large (τ2 ω A (q ω B)))"
    using is_too_large_antimono[OF assms] q_compact[OF assms(1)] by blast
  hence "(LEAST q . ¬(is_too_large (τ2 ω A q)))  q ω B"
    by (intro Least_le) blast
  thus ?thesis
    by (simp add:q_def)
qed

lemma lt_s_too_large: "x < q ω A  is_too_large (τ2 ω A x)"
  using not_less_Least unfolding q_def by auto

lemma compress_result_1:
  assumes "ω  pro_set Ω"
  shows "compress (τ3 ω A (q ω A - i)) = τ ω A"
proof (induction i)
  case 0
  then show ?case using q_compact[OF assms] by (simp add:τ3_def τ_def)
next
  case (Suc i)
  show ?case
  proof (cases "i < q ω A")
    case True
    have "is_too_large (τ2 ω A (q ω A - Suc i))"
      using True by (intro lt_s_too_large) simp
    hence "compress (τ3 ω A (q ω A - Suc i)) = compress (compress_step (τ3 ω A (q ω A - Suc i)))"
      unfolding τ3_def compress.simps
      by (simp del: compress.simps compress_step.simps)
    also have "... = compress (τ3 ω A ((q ω A - Suc i)+1))"
      by (subst τ3_step) blast
    also have "... = compress (τ3 ω A (q ω A - i))"
      using True by (metis Suc_diff_Suc Suc_eq_plus1)
    also have "... = τ ω A" using Suc by auto
    finally show ?thesis by simp
  next
    case False
    then show ?thesis using Suc by simp
  qed
qed

lemma compress_result:
  assumes "ω  pro_set Ω"
  assumes "x  q ω A"
  shows "compress (τ3 ω A x) = τ ω A"
proof -
  obtain i where i_def: "x = q ω A - i" using assms by (metis diff_diff_cancel)
  have "compress (τ3 ω A x) = compress (τ3 ω A (q ω A - i))"
    by (subst i_def) blast
  also have "... = τ ω A"
    using compress_result_1[OF assms(1)] by blast
  finally show ?thesis by simp
qed

lemma τ0_merge:
  assumes "(f,g,h)  pro_set Ψ"
  shows "τ0 (f,g,h) (A  B) j = max (τ0 (f,g,h) A j) (τ0 (f,g,h) B j)" (is "?L = ?R")
proof-
  let ?f = "λa. int (f a)"
  have "?L = Max (({ int (f a) |  a . a  A  h (g a) = j }  {-1}) 
                  ({ int (f a) | a . a  B  h (g a) = j }  {-1}))"
    unfolding τ0.simps
    by (intro arg_cong[where f="Max"])  auto
  also have "... = max (Max ({ int (f a) | a . a  A  h (g a) = j }  {-1}))
                       (Max ({ int (f a) | a . a  B  h (g a) = j }  {-1}))"
    by (intro Max_Un finite_UnI fin_f[OF assms]) auto
  also have "... = ?R"
    by (simp)
  finally show ?thesis by simp
qed

lemma τ2_merge:
  assumes "ω  pro_set Ω"
  shows "τ2 ω (A  B) x i j = max (τ2 ω A x i j) (τ2 ω B x i j)"
proof (cases "i < l")
  case True

  obtain f g h where w_i: "ω i = (f,g,h)" by (metis prod_cases3)

  have a: "(f,g,h)  pro_set Ψ" using w_i[symmetric] ω_range[OF assms(1)] by auto
  show ?thesis
    unfolding τ2_def τ1_def
    using True by (simp add:w_i τ0_merge[OF a] del:τ0.simps)
next
  case False
  thus ?thesis by (simp add:τ2_def)
qed

lemma merge1_result:
  assumes "ω  pro_set Ω"
  shows "merge1 (τ ω A) (τ ω B) = τ3 ω (A  B) (max (q ω A) (q ω B))"
proof -
  let ?qmax = "max (q ω A) (q ω B)"
  obtain u where u_def: "q ω A + u = ?qmax"
    by (metis add.commute max.commute nat_minus_add_max)
  obtain v where v_def: "q ω B + v = ?qmax"
    by (metis add.commute nat_minus_add_max)

  have "u = 0  v = 0" using u_def v_def by linarith
  moreover have "τ2 ω A (q ω A) i j - u  (-1)" if "u = 0" for i j
    using that by (simp add:τ2_def τ1_def)
  moreover have "τ2 ω B (q ω B) i j - v  (-1)" if "v = 0" for i j
    using that by (simp add:τ2_def τ1_def)
  ultimately have a:"max (τ2 ω A (q ω A) i j - u) (τ2 ω B (q ω B) i j - v)  (-1)" for i j
    unfolding le_max_iff_disj by blast

  have "τ2 ω (A  B) ?qmax = (λ i j.  max (τ2 ω A ?qmax i j) (τ2 ω B ?qmax i j))"
    using τ2_merge[OF assms] by blast
  also have "... = (λ i j.  max (τ2 ω A (q ω A + u) i j) (τ2 ω B (q ω B + v) i j))"
    unfolding u_def v_def by blast
  also have "... = (λ i j.  max (max (τ2 ω A (q ω A) i j - u) (-1)) (max (τ2 ω B (q ω B) i j - v) (-1)))"
    by (simp only: τ2_step)
  also have "... = (λ i j.  max (max (τ2 ω A (q ω A) i j - u) (τ2 ω B (q ω B) i j - v)) (-1))"
    by (metis (no_types, opaque_lifting) max.commute max.left_commute max.left_idem)
  also have "... = (λ i j. max (τ2 ω A (q ω A) i j - u) (τ2 ω B (q ω B) i j - v))"
    using a by simp
  also have "... =  (λi j. max (τ2 ω A (q ω A) i j + int (q ω A) - ?qmax)
    (τ2 ω B (q ω B) i j + int (q ω B) - ?qmax))"
    by (subst u_def[symmetric], subst v_def[symmetric]) simp
  finally have "τ2 ω (A  B) (max (q ω A) (q ω B)) =
    (λi j. max (τ2 ω A (q ω A) i j + int (q ω A) - int (?qmax))
             (τ2 ω B (q ω B) i j + int (q ω B) - int (?qmax)))" by simp
  thus ?thesis
    by (simp add:Let_def τ_def τ3_def)
qed

lemma merge_result:
  assumes "ω  pro_set Ω"
  shows "merge (τ ω A) (τ ω B) = τ ω (A  B)" (is "?L = ?R")
proof -
  have a:"max (q ω A) (q ω B)  q ω (A  B)"
    using q_mono[OF assms] by simp

  have "?L = compress (merge1 (τ ω A) (τ ω B))"
    by simp
  also have "... = compress ( τ3 ω (A  B) (max (q ω A) (q ω B)))"
    by (subst merge1_result[OF assms]) blast
  also have "... = ?R"
    by (intro compress_result[OF assms] a Un_least)
  finally show ?thesis by blast
qed

lemma single1_result: "single1 ω x = τ3 ω {x} 0"
proof -
  have "(case ω i of (f, g, h)  if h (g x) = j  i < l then int (f x) else - 1) = τ2 ω {x} 0 i j"
      for i j
  proof -
    obtain f g h where w_i:"ω i = (f, g,h)" by (metis prod_cases3)
    show ?thesis
      by (simp add:w_i τ2_def τ1_def)
  qed
  thus ?thesis
    unfolding τ3_def by fastforce
qed

lemma single_result:
  assumes "ω  pro_set Ω"
  shows "single ω x = τ ω {x}" (is "?L = ?R")
proof -
  have "?L = compress (single1 ω x)"
    by (simp)
  also have "... = compress (τ3 ω {x} 0)"
    by (subst single1_result) blast
  also have "... = ?R"
    by (intro compress_result[OF assms]) auto
  finally show ?thesis by blast
qed

subsection ‹Encoding states of the inner algorithm›

definition is_state_table :: "(nat × nat  int)  bool" where
  "is_state_table g = (range g  {-1..}  g ` (-({..<l} × {..<b}))  {-1})"

text ‹Encoding for state table values:›

definition Ve :: "int encoding"
  where "Ve x = (if x  -1 then Ne (nat (x+1)) else None)"

text ‹Encoding for state table:›

definition Te' :: "(nat × nat  int) encoding" where
  "Te' g = (
    if is_state_table g
      then (List.product [0..<l] [0..<b] e Ve) (restrict g ({..<l}×{..<b}))
      else None)"

definition Te :: "(nat  nat  int) encoding"
  where "Te f = Te' (case_prod f)"

definition encode_state :: "state encoding"
  where "encode_state = Te ×e Nbe (nat log 2 n+3)"

lemma inj_on_restrict:
  assumes "B  {f. f ` (- A)  {c}}"
  shows "inj_on (λx. restrict x A) B"
proof (rule inj_onI)
  fix f g assume a:"f  B" "g  B" "restrict f A = restrict g A"

  have "f x = g x" if "x  A"  for x
    by (intro restrict_eq_imp[OF a(3) that])
  moreover have "f x = g x" if "x  A"  for x
  proof -
    have "f x = c" "g x = c"
      using that a(1,2) assms(1) by auto
    thus ?thesis by simp
  qed
  ultimately show "f = g"
    by (intro ext) auto
qed

lemma encode_state: "is_encoding encode_state"
proof -
  have "is_encoding Ve"
    unfolding Ve_def
    by (intro encoding_compose[OF exp_golomb_encoding] inj_onI) auto
  hence 0:"is_encoding (List.product [0..<l] [0..<b] e Ve)"
    by (intro fun_encoding)
  have "is_encoding Te'"
    unfolding Te'_def is_state_table_def
    by (intro encoding_compose[OF 0] inj_on_restrict[where c="-1"]) auto
  moreover have " inj case_prod"
    by (intro injI)  (metis curry_case_prod)
  ultimately have "is_encoding Te"
    unfolding Te_def by (rule encoding_compose_2)

  thus ?thesis
    unfolding encode_state_def
    by (intro dependent_encoding bounded_nat_encoding)
qed

lemma state_bit_count:
  assumes "ω  pro_set Ω"
  shows "bit_count (encode_state (τ ω A))   2^36 * (ln(1/δ)+1)/ ε^2 + log 2 (log 2 n + 3)"
    (is "?L  ?R")
proof -
  define t where "t = τ2 ω A (q ω A)"

  have "log 2 (real n)  0"
    using n_gt_0 by simp
  hence 0: "- 1 < log 2 (real n)"
    by simp

  have "t x y = -1" if "x < l" "y  b" for x y
  proof -
    obtain f g h where ω_def: "ω x = (f,g,h)"
      by (metis prod_cases3)
    have "(f, g, h)  pro_set Ψ"
      using ω_range[OF assms] unfolding Pi_def ω_def[symmetric] by auto
    hence "h (g a) < b" for a
      using h_range by auto
    hence "y  h (g a)" for a
      using that(2) not_less by blast
    hence aux_4: "{int (f a) |a. a  A  h (g a) = y} = {}"
      by auto
    hence "max (Max (insert (- 1) {int (f a) |a. a  A  h (g a) = y}) - int (q ω A)) (- 1) = - 1"
      unfolding aux_4 by simp
    thus ?thesis
      unfolding t_def τ2_def τ1_def by (simp add:ω_def)
  qed
  moreover have "t x y = -1" if "x  l" for x y
     using that unfolding t_def τ2_def τ1_def by simp
  ultimately have 1: "t x y = -1" if "x  l  y  b" for x y
    using that by (meson not_less)

  have 2: "t x y  -1" for x y
    unfolding t_def τ2_def τ1_def by simp
  hence 3: "t x y + 1  0" for x y
    by (metis add.commute le_add_same_cancel1 minus_add_cancel)

  have 4:"is_state_table (case_prod t)"
    using 2 1 unfolding is_state_table_def by auto

  have "bit_count(Te (τ2 ω A (q ω A))) = bit_count(Te t)"
    unfolding t_def by simp
  also have "... = bit_count ((List.product [0..<l] [0..<b] e Ve) (λ(x, y){..<l}×{..<b}. t x y))"
    using 4 unfolding Te_def Te'_def by simp
  also have "... =
    (xList.product [0..<l] [0..<b]. bit_count (Ve ((λ(x, y){..<l} × {..<b}. t x y) x)))"
    using restrict_extensional atLeast0LessThan by (simp add:fun_bit_count)
  also have "... = ((x,y)List.product [0..<l] [0..<b]. bit_count (Ve (t x y)))"
    by (intro arg_cong[where f="sum_list"] map_cong refl)
     (simp add:atLeast0LessThan case_prod_beta)
  also have "... = (x{0..<l} × {0..<b}. bit_count (Ve (t (fst x) (snd x))))"
    by (subst sum_list_distinct_conv_sum_set)
     (auto intro:distinct_product simp add:case_prod_beta)
  also have "... = (x{..<l} × {..<b}. bit_count ( Ne (nat (t (fst x) (snd x)+1))))"
    using 2 unfolding Ve_def not_less[symmetric]
    by (intro sum.cong refl arg_cong[where f="bit_count"]) auto
  also have "...=(x{..<l}×{..<b}. 1+2* of_intlog 2(1+real(nat(t (fst x)(snd x)+1))))"
    unfolding exp_golomb_bit_count_exact is_too_large.simps not_less by simp
  also have "...=(x{..<l}×{..<b}. 1+2* of_intlog 2(2+ of_int(t (fst x)(snd x))))"
    using 3 by (subst of_nat_nat) (auto simp add:ac_simps)
  also have "...=b*l + 2* of_int ((i,j){..<l}×{..<b}. log 2(2+ of_int(max (t i j) (-1))))"
    using 2 by (subst max_absorb1) (auto simp add:case_prod_beta sum.distrib sum_distrib_left)
  also have "...  b*l + 2 * of_int (C5 * int b * int l)"
    using q_compact[OF assms, where A="A"] unfolding is_too_large.simps not_less t_def[symmetric]
    by (intro add_mono ereal_mono iffD2[OF of_int_le_iff] mult_left_mono order.refl)
      (simp_all add:ac_simps)
  also have "... = (2 * C5 + 1) * b * l"
    by (simp add:algebra_simps)
  finally have 5:"bit_count (Te (τ2 ω A (q ω A)))  (2 * C5 + 1) * b * l"
    by simp

  have "C4  1"
    unfolding C4_def by simp
  moreover have "ε2  1"
    using ε_lt_1 ε_gt_0
    by (intro power_le_one) auto
  ultimately have "0  log 2 (C4 / ε2)"
    using ε_gt_0 ε_lt_1
    by (intro iffD2[OF zero_le_log_cancel_iff] divide_pos_pos)auto
  hence 6: "- 1 < log 2 (C4 / ε2)"
    by simp

  have "b = 2 powr (real (nat log 2 (C4 / ε2)))"
    unfolding b_def b_exp_def by (simp add:powr_realpow)
  also have "... = 2 powr (log 2 (C4 / ε^2))"
    using 6 by (intro arg_cong2[where f="(powr)"] of_nat_nat refl) simp
  also have "...  2 powr (log 2 (C4 / ε^2) + 1)"
    by (intro powr_mono) auto
  also have "... = 2 * C4 / ε^2"
    using ε_gt_0 unfolding powr_add C4_def
    by (subst powr_log_cancel) (auto intro:divide_pos_pos)
  finally have 7:"b  2 * C4 / ε^2" by simp

  have "l  C6 * ln (1 / δ) + C6 * ln 2 + 1"
    by (intro l_ubound)
  also have "...  4 * ln(1/δ) + 3+1"
    unfolding C6_def by (intro add_mono order.refl) (approximation 5)
  also have "... = 4 * (ln(1/δ)+1)"
    by simp
  finally have 8:"l  4 * (ln(1/δ)+1)"
    by simp

  have "ε2 = 0 + ε2"
    by simp
  also have "...  ln (1 / δ) + 1"
    using δ_gt_0 δ_lt_1 ε_gt_0 ε_lt_1
    by (intro add_mono power_le_one) auto
  finally have 9: "ε2  ln (1 / δ) + 1"
    by simp

  have 10: "0  ln (1 / δ) + 1"
    using δ_gt_0 δ_lt_1 by (intro add_nonneg_nonneg) auto

  have "?L = bit_count (Te (τ2 ω A (q ω A))) + bit_count (Nbe (nat log 2 (real n)+3) (q ω A))"
    unfolding encode_state_def τ_def τ3_def by (simp  add:dependent_bit_count)
  also have "...=bit_count(Te(τ2 ω A (q ω A)))+ereal (1+ of_intlog 2 (2 + real (nat log 2 n)))"
    using max_s_3[OF assms] by (subst bounded_nat_bit_count_2)
      (simp_all add:numeral_eq_Suc le_imp_less_Suc floorlog_def)
  also have  "... = bit_count(Te(τ2 ω A (q ω A)))+ereal (1+ of_intlog 2 (2 + of_int log 2 n))"
    using 0 by simp
  also have  "...  bit_count(Te(τ2 ω A (q ω A)))+ereal (1+log 2 (2 + of_int log 2 n))"
    by (intro add_mono ereal_mono) simp_all
  also have  "...  bit_count(Te(τ2 ω A (q ω A)))+ereal (1+log 2 (2 + (log 2 n + 1)))"
    using 0 n_gt_0 by (intro add_mono ereal_mono iffD2[OF log_le_cancel_iff] add_pos_nonneg) auto
  also have  "... = bit_count(Te(τ2 ω A (q ω A)))+ereal (1+log 2 (log 2 n + 3))"
    by (simp add:ac_simps)
  also have "...  ereal ((2 * C5 + 1) * b * l) + ereal (1+log 2 (log 2 n + 3))"
    by (intro add_mono 5) auto
  also have "... = (2 * C5 + 1) * real b * real l + log 2 (log 2 n + 3) + 1"
    by simp
  also have "...  (2 * C5 + 1) * (2 * C4 / ε^2) * real l + log 2 (log 2 n + 3) + 1"
    unfolding C5_def
    by (intro ereal_mono mult_right_mono mult_left_mono add_mono 7) auto
  also have "... = (4 * of_int C5+2)*C4*real l/ ε^2 + log 2 (log 2 n + 3) + 1"
    by simp
  also have "...  (4 * of_int C5+2)*C4*(4*(ln(1/ δ)+1))/ ε^2 + log 2 (log 2 n + 3) + 1"
    using ε_gt_0 unfolding C5_def C4_def
    by (intro ereal_mono add_mono order.refl divide_right_mono mult_left_mono 8) auto
  also have "... = ((2*33+1)*9*2^26)*(ln(1/ δ)+1)/ ε^2 + log 2 (log 2 n + 3) + 1"
    unfolding C5_def C4_def by simp
  also have "...  (2^36-1) * (ln(1/δ)+1)/ ε^2 + log 2 (log 2 n + 3) + (ln (1/ δ)+1)/ ε^2"
    using ε_gt_0 δ_gt_0 ε_lt_1 9 10
    by (intro add_mono ereal_mono divide_right_mono mult_right_mono mult_left_mono) simp_all
  also have "... = 2^36* (ln(1/δ)+1)/ ε^2 + log 2 (log 2 n + 3)"
    by (simp add:divide_simps)
  finally show ?thesis
    by simp
qed

lemma random_bit_count:
  "pro_size Ω  2 powr (4 * log 2 n + 48 * (log 2 (1 / ε) + 16)^2 + (55 + 60 * ln (1 / δ))^3)"
  (is "?L  ?R")
proof -
  have 1:"log 2 (real n)  0"
    using n_gt_0 by simp
  hence 0: "- 1 < log 2 (real n)"
    by simp

  have 10: "log 2 C4  27"
    unfolding C4_def by (approximation 10)
  have "ε2  1"
    using ε_gt_0 ε_lt_1 by (intro power_le_one) auto
  also have "...  C4"
    unfolding C4_def by simp
  finally have " ε2  C4" by simp
  hence 9: "0  log 2 (C4 / ε2)"
    using ε_gt_0 unfolding C4_def
    by (intro iffD2[OF zero_le_log_cancel_iff]) simp_all
  hence 2: "- 1 < log 2 (C4 / ε2)"
    by simp

  have 3: "0 < C7 * b2" unfolding C7_def using b_min by (intro Rings.mult_pos_pos) auto

  have "0  log 2 (real C7) + real (b_exp * 2)"
    unfolding C7_def by (intro add_nonneg_nonneg) auto
  hence 4: "-1 < log 2 (real C7) + real (b_exp * 2)" by simp
  have "(2, n_exp) = split_power (pro_size (𝒢 n_exp))"
    unfolding geom_pro_size by (intro split_power_prime[symmetric] n_exp_gt_0) auto
  hence "real (pro_size Ψ1) = real (2 ^ (2 * max n_exp (nat log (real 2) (real n))))"
    by (intro arg_cong[where f="real"] hash_pro_size'[OF Ψ1 n_gt_0])
  also have "... = 2 ^ (2 * max n_exp (nat log 2 (real n)))" by simp
  also have "... = 2 ^ (2 * max 1 (nat log 2 (real n)))" unfolding n_exp_def by simp
  also have "...  2 powr (2 * max (nat log 2 (real n)) 1)"
    by (subst powr_realpow) auto
  also have "... = 2 powr (2 * max (real (nat log 2 (real n))) 1)"
    using n_gt_0 unfolding of_nat_mult of_nat_max by simp
  also have "... = 2 powr (2 * max (of_int log 2 (real n)) 1)"
    using 0 by (subst of_nat_nat) simp_all
  also have "...  2 powr (2 * max (log 2 (real n) + 1) 1)"
    by (intro powr_mono mult_left_mono max_mono) auto
  also have "... = 2 powr (2 * (log 2 (real n) + 1))"
    using 1 by (subst max_absorb1) auto
  finally have 5:"real (pro_size Ψ1)  2 powr (2 * log 2 n + 2)"
    by simp

  have "(2, 5 + b_exp * 2) = split_power (2^(5+b_exp*2))"
    by (intro split_power_prime[symmetric]) auto
  also have "... = split_power (C7 * b2)"
    unfolding C7_def b_def power_mult[symmetric] power_add by simp
  also have "... = split_power (pro_size (𝒩 (C7 * b2)))"
    unfolding C7_def b_def by (subst nat_pro_size) auto
  finally have "(2, 5 + b_exp * 2) = split_power (pro_size (𝒩 (C7 * b2)))" by simp
  hence "real (pro_size Ψ2) = real (2 ^ (2 * max  (5 + b_exp * 2) (nat log (real 2) (real n))))"
    by (intro arg_cong[where f="real"] hash_pro_size'[OF Ψ2 n_gt_0])
  also have "... = 2 ^ (max (5 + b_exp * 2) (nat log 2 (real n)) * 2)" by simp
  also have "...  2 ^ (((5 + b_exp * 2) + (nat log 2 (real n))) * 2)"
    by (intro power_increasing mult_right_mono) auto
  also have "... = 2 powr ((5 + b_exp * 2 + real (nat log 2 (real n)))*2)"
    by (subst powr_realpow[symmetric]) auto
  also have "... = 2 powr ((5 + of_int b_exp * 2 + of_int log 2 (real n))*2)"
    using 0 by (subst of_nat_nat) auto
  also have "...  2 powr ((5 + of_int b_exp * 2 + (log 2 (real n) + 1))*2)"
    by (intro powr_mono mult_right_mono add_mono) simp_all
  also have "... = 2 powr (12 + 4 * real( nat log 2 (C4 / ε2)) + log 2 (real n) * 2)"
    unfolding b_exp_def by (simp add:ac_simps)
  also have "... = 2 powr (12 + 4 * real_of_int log 2 (C4 / ε2) + log 2 (real n) * 2)"
    using 2 by (subst of_nat_nat) simp_all
  also have "...  2 powr (12 + 4 * (log 2 (C4 / ε2) + 1) + log 2 (real n) * 2)"
    by (intro powr_mono add_mono order.refl mult_left_mono) simp_all
  also have "... = 2 powr (2 * log 2 n + 4 * log 2 (C4 / ε2) + 16)"
    by (simp add:ac_simps)
  finally have 6:"real (pro_size Ψ2)  2 powr (2 * log 2 n + 4 * log 2 (C4 / ε2) + 16)"
    by simp
  have "(2, b_exp) = split_power (2 ^ b_exp)"
    using b_exp_ge_26 by (intro split_power_prime[symmetric]) auto
  also have "... = split_power (pro_size (𝒩 b))"
    unfolding b_def by (subst nat_pro_size) auto
  finally have "(2, b_exp) = split_power (pro_size (𝒩 b))" by simp
  hence "real (pro_size Ψ3) = real (2 ^ (k * max b_exp (nat log (real 2) (real (C7*b^2)))))"
    by (intro arg_cong[where f="real"] hash_pro_size'[OF Ψ3]) (simp_all add:C7_def b_def)
  also have "... = 2 ^ (k * max b_exp (nat log 2 (real C7 * (2 ^ (b_exp*2)))))"
    unfolding b_def power_mult by simp
  also have "... = 2 ^ (max b_exp (nat log 2 C7 + log 2 (2 ^ (b_exp*2))) * k)"
    unfolding C7_def by (subst log_mult) simp_all
  also have "... = 2 ^ (max b_exp (nat log 2 C7 + (b_exp*2)) * k)"
    by (subst log_nat_power) simp_all
  also have "... = 2 powr (max (real b_exp) (real (nat log 2 C7 + (b_exp*2))) * real k)"
    by (subst powr_realpow[symmetric]) simp_all
  also have "... = 2 powr (max (real b_exp) (of_int log 2 C7 + (b_exp*2)) * real k)"
    using 4 by (subst of_nat_nat) simp_all
  also have "...  2 powr (max (real b_exp) (log 2 C7 + real b_exp*2 +1) * real k)"
    by (intro powr_mono mult_right_mono max_mono_2) simp_all
  also have "... = 2 powr ((log 2 (2^5) + real b_exp*2 +1) * real k)"
    unfolding C7_def by (subst max_absorb2) simp_all
  also have "... = 2 powr ((real b_exp*2 +6) * real k)"
    unfolding C7_def by (subst log_nat_power) (simp_all add:ac_simps)
  also have "... = 2 powr ((of_int log 2 (C4 / ε2) * 2 + 6) * real k)"
    using 2 unfolding b_exp_def by (subst of_nat_nat) simp_all
  also have "...  2 powr (((log 2 (C4 / ε^2)+1) * 2 + 6) * real k)"
    by (intro powr_mono mult_right_mono add_mono) simp_all
  also have "... = 2 powr ((log 2 (C4 / ε2) * 2 + 8 ) * real k)"
    by (simp add:ac_simps)
  finally have 7:"real (pro_size Ψ3)  2 powr ((log 2 (C4 / ε2) * 2 + 8 ) * real k)"
    by simp

  have "ln (real b)  0"
    using b_min by simp
  hence "real k = of_int 7.5  * ln (real b) + 16"
    unfolding k_def C2_def C3_def by (subst of_nat_nat) simp_all
  also have "...  (7.5 * ln (real b) + 16) + 1"
    unfolding b_def by (intro of_int_ceiling_le_add_one)
  also have "... = 7.5 * ln (2 powr b_exp) + 17"
    unfolding b_def using powr_realpow by simp
  also have "... = real b_exp * (7.5 * ln 2) + 17"
    unfolding powr_def by simp
  also have "...  real b_exp * 6 + 17"
    by (intro add_mono mult_left_mono order.refl of_nat_0_le_iff) (approximation 5)
  also have "... = of_int log 2 (C4 / ε2) * 6 + 17"
    using 2 unfolding b_exp_def by (subst of_nat_nat) simp_all
  also have "...  (log 2 (C4 / ε^2) + 1) * 6 + 17"
    by (intro add_mono mult_right_mono) simp_all
  also have "... = 6 * log 2 (C4 / ε^2) + 23"
    by simp
  finally have 8:"real k  6 * log 2 (C4 / ε^2) + 23"
    by simp

  have "real (pro_size Ψ) = real (pro_size Ψ1) * real (pro_size Ψ2) * real (pro_size Ψ3)"
    unfolding Ψ_def prod_pro_size by simp
  also have "... 
    2 powr(2*log 2 n+2)*2 powr (2*log 2 n+4*log 2 (C4/ε2)+16)*2 powr((log 2 (C4/ε2)*2+8)*real k)"
    by (intro mult_mono 5 6 7 mult_nonneg_nonneg) simp_all
  also have "... = 2 powr (2*log 2 n + 2 + 2 * log 2 n+4*log 2 (C4/ε2)+16+(log 2 (C4/ε2)*2+8)*real k)"
    unfolding powr_add by simp
  also have "... = 2 powr (4*log 2 n + 4*log 2 (C4/ε2) + 18 + (2*log 2 (C4/ε2)+8)*real k)"
    by (simp add:ac_simps)
  also have "... 
    2 powr (4* log 2 n + 4* log 2 (C4/ ε^2) + 18 + (2*log 2 (C4/ε2)+8)*(6 * log 2 (C4 / ε^2) + 23))"
    using 9 by (intro powr_mono add_mono order.refl mult_left_mono 8 add_nonneg_nonneg) simp_all
  also have "... = 2 powr (4 * log 2 n+12 * log 2 (C4 / ε^2)^2 + 98 * log 2 (C4 / ε^2)+202)"
    by (simp add:algebra_simps power2_eq_square)
  also have "...  2 powr (4 * log 2 n+12 * log 2 (C4 / ε^2)^2 + 120 * log 2 (C4 / ε^2)+300)"
    using 9 by (intro powr_mono add_mono order.refl mult_right_mono) simp_all
  also have "... = 2 powr (4 * log 2 n+12 * (log 2 (C4* (1/ ε)^2) + 5)^2)"
    by (simp add:power2_eq_square algebra_simps)
  also have "... = 2 powr (4 * log 2 n + 12 * (log 2 C4 + log 2 ((1 / ε)^2) + 5)^2)"
    unfolding C4_def using ε_gt_0 by (subst log_mult) auto
  also have "...  2 powr (4 * log 2 n + 12 * (27 + log 2 ((1/ ε)^2) + 5)^2)"
    using ε_gt_0 ε_lt_1
    by (intro powr_mono add_mono order.refl mult_left_mono power_mono add_nonneg_nonneg 10)
     (simp_all add:C4_def)
  also have "... = 2 powr (4 * log 2 n + 12 * (2 * (log 2 (1 / ε) + 16))^2)"
    using ε_gt_0 by (subst log_nat_power)  (simp_all add:ac_simps)
  also have "... = 2 powr (4 * log 2 n + 48 * (log 2 (1 / ε) + 16)^2)"
    unfolding power_mult_distrib by simp
  finally have 19:"real (pro_size Ψ)  2 powr (4 * log 2 n + 48 * (log 2 (1 / ε) + 16)^2)"
    by simp

  have "0  ln Λ / ln (19 / 20)"
    using Λ_gt_0 Λ_le_1 by (intro divide_nonpos_neg) simp_all
  hence 11: "-1 < ln Λ / ln (19 / 20)" by simp

  have 12: "ln (19 / 20)  -(0.05::real)" "- ln (1 / 16)  (2.8::real)" by (approximation 10)+

  have 13: "ln l  0" using l_gt_0 by auto

  have "ln l^3 = 27 * (0 + ln l/3)^3" by (simp add:power3_eq_cube)
  also have "...  27 * (1 + ln l/real 3)^3"
    using l_gt_0 by (intro mult_left_mono add_mono power_mono) auto
  also have "...  27 * (exp (ln l))"
    using l_gt_0 13 by (intro mult_left_mono exp_ge_one_plus_x_over_n_power_n) linarith+
  also have "... = 27 * real l" using l_gt_0 by (subst exp_ln) auto
  finally have 14:"ln l^3  27 * real l" by simp

  have 15:"C6 * ln (2 / δ) > 0"
    using δ_lt_1 δ_gt_0 unfolding C6_def
    by (intro Rings.mult_pos_pos ln_gt_zero) auto
  hence "1  real_of_int C6 * ln (2 / δ)" by simp
  hence 16: "1  3 * real_of_int C6 * ln (2 / δ)" by argo

  have 17: "12 * ln 2  (9::real)" by (approximation 5)

  have "16 ^ ((l - 1) * natln Λ / ln 0.95) = 16 powr (real (l-1)*real(nat ln Λ / ln (19 / 20)))"
    by (subst powr_realpow[symmetric]) auto
  also have "... = 16 powr (real (l-1)* of_int ln Λ / ln (19 / 20))"
    using 11 by (subst of_nat_nat) simp_all
  also have "...  16 powr (real (l-1)* (ln Λ / ln (19/20)+1))"
    by (intro powr_mono mult_left_mono) auto
  also have "... = 16 powr ((real l - 1)*(ln Λ / ln (19/20)+1))"
    using l_gt_0 by (subst of_nat_diff) auto
  also have "...  16 powr ((real l - 1)*(ln Λ / (-0.05)+1))"
    using l_gt_0 Λ_gt_0 Λ_le_1
    by (intro powr_mono mult_left_mono add_mono divide_left_mono_neg 12) auto
  also have "... = 16 powr ((real l - 1)*(20 * (-ln Λ)+1))"
    by (simp add:algebra_simps)
  also have "... = 16 powr ((real l - 1)*(20 * -(min (ln (1/16)) (-l*ln l^3))+1))"
    unfolding Λ_def by (subst ln_min_swap) auto
  also have "... = 16 powr ((real l - 1)*(20 * max (-ln (1/16)) (l*ln l^3)+1))"
    by (intro_cong "[σ2 (powr), σ2(+), σ2 (*)]") simp
  also have "...  16 powr ((real l - 1)*(20 * max (2.8) (l*ln l^3)+1))"
    using l_gt_0 by (intro powr_mono mult_left_mono add_mono max_mono 12) auto
  also have "...  16 powr ((real l - 1)*(20 * (2.8+l*ln l^3)+1))"
    using l_gt_0 by (intro powr_mono mult_left_mono add_mono) auto
  also have "... = 16 powr ((real l - 1)*(20 * (l*ln l^3)+57))"
    by (simp add:algebra_simps)
  also have "...  16 powr ((real l - 1)*(20 * (real l*(27*real l))+57))"
    using l_gt_0 by (intro powr_mono mult_left_mono add_mono 14) auto
  also have "... = 16 powr (540 * real l^3 - 540 * real l^2 + 57* real l - 57)"
    by (simp add:algebra_simps numeral_eq_Suc)
  also have "...  16 powr (540 * real l^3 - 540 * real l^2 + 180* real l - 20)"
    by (intro powr_mono add_mono diff_mono order.refl mult_right_mono) auto
  also have "... = 16 powr (20 * (3*real l - 1)^3)"
    by (simp add: algebra_simps power3_eq_cube power2_eq_square)
  also have "... = 16 powr (20 * (3 * of_int C6 * ln (2 / δ) - 1) ^ 3)"
    using 15 unfolding l_def by (subst of_nat_nat) auto
  also have "...  16 powr (20 * (3 * (C6 * ln (2 / δ) + 1) - 1) ^ 3)"
    using 16 by (intro powr_mono mult_left_mono power_mono diff_mono) auto
  also have "... = 16 powr (20 * (2 + 12 * ln (2 * (1 / δ))) ^ 3)"
    by (simp add:algebra_simps C6_def)
  also have "... = (2 powr 4) powr (20 * (2+ 12 * (ln 2 + ln(1/ δ)))^3)"
    using δ_gt_0 by (subst ln_mult) auto
  also have "... = 2 powr (80 * (2 + 12 * ln 2 + 12 * ln (1 / δ)) ^ 3)"
    unfolding powr_powr by (simp add:ac_simps)
  also have "...  2 powr (80 * (2 + 9 + 12 * ln (1 / δ)) ^ 3)"
    using δ_gt_0 δ_lt_1
    by (intro powr_mono mult_left_mono power_mono add_mono 17 add_nonneg_nonneg) auto
  also have "... = 2 powr (80 * (11 + 12 * ln (1 / δ)) ^ 3)" by simp
  also have "...  2 powr (5^3 * (11 + 12 * ln (1 / δ)) ^ 3)"
    using δ_gt_0 δ_lt_1 by (intro powr_mono mult_right_mono) (auto intro!:add_nonneg_nonneg)
  also have "... = 2 powr ((55 + 60 * ln (1 / δ))^3)"
    unfolding power_mult_distrib[symmetric] by simp
  finally have 18:"16^((l - 1) * natln Λ / ln (19/20))  2 powr ((55 + 60 * ln (1 / δ))^3)"
    by simp

  have "?L = real (pro_size Ψ) * 16 ^ ((l - 1) * nat ln Λ / ln (19 / 20))"
    unfolding expander_pro_size[OF Ω] by simp
  also have "...  2 powr (4*log 2 n+48*(log 2 (1/ε)+16)^2)*2 powr ((55 + 60 * ln (1 / δ))^3)"
    by (intro mult_mono 18 19) simp_all
  also have "... = 2 powr (4 * log 2 n + 48 * (log 2 (1 / ε) + 16)^2 + (55 + 60 * ln (1 / δ))^3)"
    unfolding powr_add[symmetric] by simp
  finally show ?thesis by simp
qed

end

unbundle no_intro_cong_syntax

end