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 "s⇩M"} 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 C⇩4 :: real where "C⇩4 = 3^2*2^23"
definition C⇩5 :: int where "C⇩5 = 33"
definition C⇩6 :: real where "C⇩6 = 4"
definition C⇩7 :: nat where "C⇩7 = 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 (C⇩4 / ε^2)⌉"
definition b :: nat where "b = 2^b_exp"
definition l where "l = nat ⌈C⇩6 * ln (2/ δ)⌉"
definition k where "k = nat ⌈C⇩2*ln b + C⇩3⌉"
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: "C⇩6 * ln (2 / δ) ≤ l"
  unfolding l_def by linarith

lemma k_min: "C⇩2 * ln (real b) + C⇩3 ≤ 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 < C⇩6 * ln (2 / δ)"
    unfolding C⇩6_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 ≤ C⇩6 * ln(1 / δ)+C⇩6*ln 2 + 1"
proof -
  have "l = of_int ⌈C⇩6 * ln (2/ δ)⌉"
    using l_gt_0 unfolding l_def
    by (intro of_nat_nat) simp
  also have "... ≤ C⇩6 * ln (1/ δ*2)+1"
    by simp
  also have "... = C⇩6 * ln (1/ δ)+C⇩6 * 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 < C⇩4 / 1 " unfolding C⇩4_def by simp
  also have "... ≤ C⇩4 / ε^2"
    using ε_gt_0 ε_lt_1 unfolding C⇩4_def
    by (intro divide_left_mono power_le_one) auto
  finally have "2 powr 25 < C⇩4 / ε^2" by simp
  hence "log 2 (C⇩4 / ε^2) > 25"
    using ε_gt_0 unfolding C⇩4_def
    by (intro iffD2[OF less_log_iff] divide_pos_pos zero_less_power) auto
  hence "⌈log 2 (C⇩4 / ε^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 C⇩2_def C⇩3_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: "C⇩4 / ε^2 ≤ real b"
proof -
  have "C⇩4 /  ε^2 = 2 powr (log 2 (C⇩4 / ε^2))"
    using ε_gt_0 unfolding C⇩4_def by (intro powr_log_cancel[symmetric] divide_pos_pos) auto
  also have "... ≤ 2 powr (nat ⌈log 2 (C⇩4 /  ε^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 (𝒩 (C⇩7*b⇧2))"
abbreviation Ψ⇩3 where "Ψ⇩3 ≡ ℋ k (C⇩7*b⇧2) (𝒩 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)⌋) > C⇩5 * 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 "... ≤ C⇩5 * b * l" unfolding C⇩5_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,q⇩1) (B2, q⇩2) = (
    let q = max q⇩1 q⇩2 in (λ i j. max (B1 i j + q⇩1 - q) (B2 i j + q⇩2 - 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 (𝒩 (C⇩7 * b^2)))"
proof -
  have 0:"pro_size (𝒩 (C⇩7 * b^2)) = 2 ^ (5 + 2 * b_exp)"
    unfolding C⇩7_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 < C⇩7*b^2"
proof -
  have "g ∈ pro_select Ψ⇩2 ` {..<pro_size Ψ⇩2}" using assms unfolding set_sample_pro by auto
  hence "g x ∈ pro_set (𝒩 ( C⇩7*b^2))" using hash_pro_range[OF Ψ⇩2] by auto
  moreover have "C⇩7*b^2  > 0" unfolding C⇩7_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 < C⇩7*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:C⇩5_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 "C⇩5 * 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)⌋) > C⇩5 * 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 V⇩e :: "int encoding"
  where "V⇩e x = (if x ≥ -1 then N⇩e (nat (x+1)) else None)"

text ‹Encoding for state table:›

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

definition T⇩e :: "(nat ⇒ nat ⇒ int) encoding"
  where "T⇩e f = T⇩e' (case_prod f)"

definition encode_state :: "state encoding"
  where "encode_state = T⇩e ×⇩e Nb⇩e (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 V⇩e"
    unfolding V⇩e_def
    by (intro encoding_compose[OF exp_golomb_encoding] inj_onI) auto
  hence 0:"is_encoding (List.product [0..<l] [0..<b] →⇩e V⇩e)"
    by (intro fun_encoding)
  have "is_encoding T⇩e'"
    unfolding T⇩e'_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 T⇩e"
    unfolding T⇩e_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(T⇩e (τ⇩2 ω A (q ω A))) = bit_count(T⇩e t)"
    unfolding t_def by simp
  also have "... = bit_count ((List.product [0..<l] [0..<b] →⇩e V⇩e) (λ(x, y)∈{..<l}×{..<b}. t x y))"
    using 4 unfolding T⇩e_def T⇩e'_def by simp
  also have "... =
    (∑x←List.product [0..<l] [0..<b]. bit_count (V⇩e ((λ(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 (V⇩e (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 (V⇩e (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 ( N⇩e (nat (t (fst x) (snd x)+1))))"
    using 2 unfolding V⇩e_def not_less[symmetric]
    by (intro sum.cong refl arg_cong[where f="bit_count"]) auto
  also have "...=(∑x∈{..<l}×{..<b}. 1+2* of_int⌊log 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_int⌊log 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 (C⇩5 * 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 * C⇩5 + 1) * b * l"
    by (simp add:algebra_simps)
  finally have 5:"bit_count (T⇩e (τ⇩2 ω A (q ω A))) ≤ (2 * C⇩5 + 1) * b * l"
    by simp

  have "C⇩4 ≥ 1"
    unfolding C⇩4_def by simp
  moreover have "ε⇧2 ≤ 1"
    using ε_lt_1 ε_gt_0
    by (intro power_le_one) auto
  ultimately have "0 ≤ log 2 (C⇩4 / ε⇧2)"
    using ε_gt_0 ε_lt_1
    by (intro iffD2[OF zero_le_log_cancel_iff] divide_pos_pos)auto
  hence 6: "- 1 < log 2 (C⇩4 / ε⇧2)"
    by simp

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

  have "l ≤ C⇩6 * ln (1 / δ) + C⇩6 * ln 2 + 1"
    by (intro l_ubound)
  also have "... ≤ 4 * ln(1/δ) + 3+1"
    unfolding C⇩6_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 (T⇩e (τ⇩2 ω A (q ω A))) + bit_count (Nb⇩e (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(T⇩e(τ⇩2 ω A (q ω A)))+ereal (1+ of_int⌊log 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(T⇩e(τ⇩2 ω A (q ω A)))+ereal (1+ of_int⌊log 2 (2 + of_int ⌈log 2 n⌉)⌋)"
    using 0 by simp
  also have  "... ≤ bit_count(T⇩e(τ⇩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(T⇩e(τ⇩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(T⇩e(τ⇩2 ω A (q ω A)))+ereal (1+log 2 (log 2 n + 3))"
    by (simp add:ac_simps)
  also have "... ≤ ereal ((2 * C⇩5 + 1) * b * l) + ereal (1+log 2 (log 2 n + 3))"
    by (intro add_mono 5) auto
  also have "... = (2 * C⇩5 + 1) * real b * real l + log 2 (log 2 n + 3) + 1"
    by simp
  also have "... ≤ (2 * C⇩5 + 1) * (2 * C⇩4 / ε^2) * real l + log 2 (log 2 n + 3) + 1"
    unfolding C⇩5_def
    by (intro ereal_mono mult_right_mono mult_left_mono add_mono 7) auto
  also have "... = (4 * of_int C⇩5+2)*C⇩4*real l/ ε^2 + log 2 (log 2 n + 3) + 1"
    by simp
  also have "... ≤ (4 * of_int C⇩5+2)*C⇩4*(4*(ln(1/ δ)+1))/ ε^2 + log 2 (log 2 n + 3) + 1"
    using ε_gt_0 unfolding C⇩5_def C⇩4_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 C⇩5_def C⇩4_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 C⇩4 ≤ 27"
    unfolding C⇩4_def by (approximation 10)
  have "ε⇧2 ≤ 1"
    using ε_gt_0 ε_lt_1 by (intro power_le_one) auto
  also have "... ≤ C⇩4"
    unfolding C⇩4_def by simp
  finally have " ε⇧2 ≤ C⇩4" by simp
  hence 9: "0 ≤ log 2 (C⇩4 / ε⇧2)"
    using ε_gt_0 unfolding C⇩4_def
    by (intro iffD2[OF zero_le_log_cancel_iff]) simp_all
  hence 2: "- 1 < log 2 (C⇩4 / ε⇧2)"
    by simp

  have 3: "0 < C⇩7 * b⇧2" unfolding C⇩7_def using b_min by (intro Rings.mult_pos_pos) auto

  have "0 ≤ log 2 (real C⇩7) + real (b_exp * 2)"
    unfolding C⇩7_def by (intro add_nonneg_nonneg) auto
  hence 4: "-1 < log 2 (real C⇩7) + 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 (C⇩7 * b⇧2)"
    unfolding C⇩7_def b_def power_mult[symmetric] power_add by simp
  also have "... = split_power (pro_size (𝒩 (C⇩7 * b⇧2)))"
    unfolding C⇩7_def b_def by (subst nat_pro_size) auto
  finally have "(2, 5 + b_exp * 2) = split_power (pro_size (𝒩 (C⇩7 * b⇧2)))" 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 (C⇩4 / ε⇧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 (C⇩4 / ε⇧2)⌉ + log 2 (real n) * 2)"
    using 2 by (subst of_nat_nat) simp_all
  also have "... ≤ 2 powr (12 + 4 * (log 2 (C⇩4 / ε⇧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 (C⇩4 / ε⇧2) + 16)"
    by (simp add:ac_simps)
  finally have 6:"real (pro_size Ψ⇩2) ≤ 2 powr (2 * log 2 n + 4 * log 2 (C⇩4 / ε⇧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 (C⇩7*b^2))⌉)))"
    by (intro arg_cong[where f="real"] hash_pro_size'[OF Ψ⇩3]) (simp_all add:C⇩7_def b_def)
  also have "... = 2 ^ (k * max b_exp (nat ⌈log 2 (real C⇩7 * (2 ^ (b_exp*2)))⌉))"
    unfolding b_def power_mult by simp
  also have "... = 2 ^ (max b_exp (nat ⌈log 2 C⇩7 + log 2 (2 ^ (b_exp*2))⌉) * k)"
    unfolding C⇩7_def by (subst log_mult) simp_all
  also have "... = 2 ^ (max b_exp (nat ⌈log 2 C⇩7 + (b_exp*2)⌉) * k)"
    by (subst log_nat_power) simp_all
  also have "... = 2 powr (max (real b_exp) (real (nat ⌈log 2 C⇩7 + (b_exp*2)⌉)) * real k)"
    by (subst powr_realpow[symmetric]) simp_all
  also have "... = 2 powr (max (real b_exp) (of_int ⌈log 2 C⇩7 + (b_exp*2)⌉) * real k)"
    using 4 by (subst of_nat_nat) simp_all
  also have "... ≤ 2 powr (max (real b_exp) (log 2 C⇩7 + 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 C⇩7_def by (subst max_absorb2) simp_all
  also have "... = 2 powr ((real b_exp*2 +6) * real k)"
    unfolding C⇩7_def by (subst log_nat_power) (simp_all add:ac_simps)
  also have "... = 2 powr ((of_int ⌈log 2 (C⇩4 / ε⇧2)⌉ * 2 + 6) * real k)"
    using 2 unfolding b_exp_def by (subst of_nat_nat) simp_all
  also have "... ≤ 2 powr (((log 2 (C⇩4 / ε^2)+1) * 2 + 6) * real k)"
    by (intro powr_mono mult_right_mono add_mono) simp_all
  also have "... = 2 powr ((log 2 (C⇩4 / ε⇧2) * 2 + 8 ) * real k)"
    by (simp add:ac_simps)
  finally have 7:"real (pro_size Ψ⇩3) ≤ 2 powr ((log 2 (C⇩4 / ε⇧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 C⇩2_def C⇩3_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 (C⇩4 / ε⇧2)⌉ * 6 + 17"
    using 2 unfolding b_exp_def by (subst of_nat_nat) simp_all
  also have "... ≤ (log 2 (C⇩4 / ε^2) + 1) * 6 + 17"
    by (intro add_mono mult_right_mono) simp_all
  also have "... = 6 * log 2 (C⇩4 / ε^2) + 23"
    by simp
  finally have 8:"real k ≤ 6 * log 2 (C⇩4 / ε^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 (C⇩4/ε⇧2)+16)*2 powr((log 2 (C⇩4/ε⇧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 (C⇩4/ε⇧2)+16+(log 2 (C⇩4/ε⇧2)*2+8)*real k)"
    unfolding powr_add by simp
  also have "... = 2 powr (4*log 2 n + 4*log 2 (C⇩4/ε⇧2) + 18 + (2*log 2 (C⇩4/ε⇧2)+8)*real k)"
    by (simp add:ac_simps)
  also have "... ≤
    2 powr (4* log 2 n + 4* log 2 (C⇩4/ ε^2) + 18 + (2*log 2 (C⇩4/ε⇧2)+8)*(6 * log 2 (C⇩4 / ε^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 (C⇩4 / ε^2)^2 + 98 * log 2 (C⇩4 / ε^2)+202)"
    by (simp add:algebra_simps power2_eq_square)
  also have "... ≤ 2 powr (4 * log 2 n+12 * log 2 (C⇩4 / ε^2)^2 + 120 * log 2 (C⇩4 / ε^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 (C⇩4* (1/ ε)^2) + 5)^2)"
    by (simp add:power2_eq_square algebra_simps)
  also have "... = 2 powr (4 * log 2 n + 12 * (log 2 C⇩4 + log 2 ((1 / ε)^2) + 5)^2)"
    unfolding C⇩4_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:C⇩4_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:"C⇩6 * ln (2 / δ) > 0"
    using δ_lt_1 δ_gt_0 unfolding C⇩6_def
    by (intro Rings.mult_pos_pos ln_gt_zero) auto
  hence "1 ≤ real_of_int ⌈C⇩6 * ln (2 / δ)⌉" by simp
  hence 16: "1 ≤ 3 * real_of_int ⌈C⇩6 * ln (2 / δ)⌉" by argo

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

  have "16 ^ ((l - 1) * nat⌈ln Λ / 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 ⌈C⇩6 * ln (2 / δ)⌉ - 1) ^ 3)"
    using 15 unfolding l_def by (subst of_nat_nat) auto
  also have "... ≤ 16 powr (20 * (3 * (C⇩6 * 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 C⇩6_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) * nat⌈ln Λ / 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