Theory Distributed_Distinct_Elements_Tail_Bounds

section ‹Tail Bounds for Expander Walks›

theory Distributed_Distinct_Elements_Tail_Bounds
  imports
    Distributed_Distinct_Elements_Preliminary
    Expander_Graphs.Expander_Graphs_Definition
    Expander_Graphs.Expander_Graphs_Walks
    "HOL-Decision_Procs.Approximation"
    Pseudorandom_Combinators
begin

text ‹This section introduces tail estimates for random walks in expander graphs, specific to the
verification of this algorithm (in particular to two-stage expander graph sampling and obtained
tail bounds for subgaussian random variables). They follow from the more fundamental results
@{thm [source] regular_graph.kl_chernoff_property} and
@{thm [source] regular_graph.uniform_property} which are verified in the AFP entry for
expander graphs~\cite{Expander_Graphs-AFP}.›

hide_fact Henstock_Kurzweil_Integration.integral_sum

unbundle intro_cong_syntax

lemma x_ln_x_min:
  assumes "x ≥ (0::real)"
  shows  "x * ln x ≥ -exp (-1)"
proof -
  define f where "f x = x * ln x" for x :: real
  define f' where "f' x = ln x + 1" for x :: real

  have 0:"(f has_real_derivative (f' x)) (at x)" if "x > 0" for x
    unfolding f_def f'_def using that
    by (auto intro!: derivative_eq_intros)

  have "f' x ≥ 0" if "exp (-1) ≤ x" for x :: real
  proof -
    have "ln x ≥ -1"
      using that order_less_le_trans[OF exp_gt_zero]
      by (intro iffD2[OF ln_ge_iff]) auto
    thus ?thesis
      unfolding f'_def by (simp)
  qed

  hence "∃y. (f has_real_derivative y) (at x) ∧ 0 ≤ y" if "x ≥ exp (-1)" for x :: real
    using that order_less_le_trans[OF exp_gt_zero]
    by (intro exI[where x="f' x"] conjI 0) auto
  hence "f (exp (-1)) ≤ f x" if "exp(-1) ≤ x"
    by (intro DERIV_nonneg_imp_nondecreasing[OF that]) auto
  hence 2:?thesis if  "exp(-1) ≤ x"
    unfolding f_def using that by simp

  have "f' x ≤ 0" if "x > 0" "x ≤ exp (-1)" for x :: real
  proof -
    have "ln x ≤ ln (exp (-1))"
      by (intro iffD2[OF ln_le_cancel_iff] that exp_gt_zero)
    also have "... = -1"
      by simp
    finally have "ln x ≤ -1" by simp
    thus ?thesis unfolding f'_def by simp
  qed

  hence "∃y. (f has_real_derivative y) (at x) ∧ y ≤ 0" if "x > 0 " "x ≤ exp (-1)" for x :: real
    using that by (intro exI[where x="f' x"] conjI 0) auto
  hence "f (exp (-1)) ≤ f x" if "x > 0" "x ≤ exp(-1)"
    using that(1) by (intro DERIV_nonpos_imp_nonincreasing[OF that(2)]) auto
  hence 3:?thesis if "x > 0" "x ≤ exp(-1)"
    unfolding f_def using that by simp

  have ?thesis if "x = 0"
    using that by simp
  thus ?thesis
    using 2 3 assms by fastforce
qed

theorem (in regular_graph) walk_tail_bound:
  assumes "l > 0"
  assumes "S ⊆ verts G"
  defines "μ ≡ real (card S) / card (verts G)"
  assumes "γ < 1" "μ + Λ⇩a ≤ γ"
  shows "measure (pmf_of_multiset (walks G l)) {w. real (card {i ∈ {..<l}. w ! i ∈ S}) ≥ γ*l}
    ≤ exp (- real l * (γ * ln (1/(μ+Λ⇩a)) - 2 * exp(-1)))" (is "?L ≤ ?R")
proof (cases "μ > 0")
  case True

  have "0 < μ + Λ⇩a"
    by (intro add_pos_nonneg Λ_ge_0 True)
  also have "... ≤ γ"
    using assms(5) by simp
  finally have γ_gt_0: "0 < γ" by simp

  hence γ_ge_0: "0 ≤ γ"
    by simp

  have "card S ≤ card (verts G)"
    by (intro card_mono assms(2)) auto
  hence μ_le_1: "μ ≤ 1"
    unfolding μ_def by (simp add:divide_simps)

  have 2: "0 < μ + Λ⇩a * (1 - μ)"
    using μ_le_1 by (intro add_pos_nonneg True mult_nonneg_nonneg Λ_ge_0) auto

  have "μ + Λ⇩a * (1 - μ) ≤ μ +  Λ⇩a * 1"
    using Λ_ge_0 True by (intro add_mono mult_left_mono) auto
  also have "... ≤ γ"
    using assms(5) by simp
  also have "... < 1"
    using assms(4) by simp
  finally have 4:"μ + Λ⇩a * (1 - μ) < 1" by simp
  hence 3: "1 ≤ 1 / (1 - (μ + Λ⇩a * (1 - μ)))"
    using 2 by (subst pos_le_divide_eq) simp_all

  have "card S ≤ n"
    unfolding n_def by (intro card_mono assms(2)) auto
  hence 0:"μ ≤ 1"
    unfolding μ_def n_def[symmetric] using n_gt_0 by simp

  have "γ * ln (1 / (μ + Λ⇩a)) - 2*exp (- 1) = γ * ln (1 / (μ + Λ⇩a*1))+0 -2*exp (- 1)"
    by simp
  also have "... ≤ γ * ln (1 / (μ + Λ⇩a*(1-μ)))+0-2*exp(-1)"
    using True γ_ge_0 Λ_ge_0 0 2
    by (intro diff_right_mono mult_left_mono iffD2[OF ln_le_cancel_iff] divide_pos_pos
        divide_left_mono add_mono) auto
  also have "... ≤ γ * ln (1 / (μ + Λ⇩a*(1-μ)))+(1-γ)*ln(1/(1-(μ+Λ⇩a*(1-μ))))-2* exp(-1)"
    using assms(4) 3 by (intro add_mono diff_mono mult_nonneg_nonneg ln_ge_zero) auto
  also have "... = (-exp(-1))+γ*ln(1/(μ+Λ⇩a*(1-μ)))+(-exp(-1))+(1-γ)*ln(1/(1-(μ+Λ⇩a*(1-μ))))"
    by simp
  also have "... ≤ γ*ln γ+γ*ln(1/(μ+Λ⇩a*(1-μ)))+(1-γ)*ln(1-γ)+(1-γ)*ln(1/(1-(μ+Λ⇩a*(1-μ))))"
    using assms(4) γ_ge_0 by (intro add_mono x_ln_x_min) auto
  also have "... = γ*(ln γ+ln(1/(μ+Λ⇩a*(1-μ))))+(1-γ)*(ln(1-γ)+ln(1/(1-(μ+Λ⇩a*(1-μ)))))"
    by (simp add:algebra_simps)
  also have "... = γ * ln (γ*(1/(μ+Λ⇩a*(1-μ))))+(1-γ)*ln((1-γ)*(1/(1-(μ+Λ⇩a*(1-μ)))))"
    using 2 4 assms(4) γ_gt_0
    by (intro_cong "[σ⇩2(+), σ⇩2(*)]" more:ln_mult[symmetric] divide_pos_pos) auto
  also have "... = KL_div γ (μ+Λ⇩a*(1-μ))"
    unfolding KL_div_def by simp
  finally have 1: "γ * ln (1 / (μ + Λ⇩a)) - 2 * exp (- 1) ≤ KL_div γ (μ + Λ⇩a * (1 - μ))"
    by simp

  have "μ+Λ⇩a*(1-μ) ≤ μ+Λ⇩a*1"
    using True
    by (intro add_mono mult_left_mono Λ_ge_0) auto
  also have "... ≤ γ"
    using assms(5) by simp
  finally have "μ+Λ⇩a*(1-μ) ≤ γ"  by simp
  moreover have "μ+Λ⇩a*(1-μ) > 0"
    using 0 by (intro add_pos_nonneg True mult_nonneg_nonneg Λ_ge_0) auto
  ultimately have "μ+Λ⇩a*(1-μ) ∈ {0<..γ}" by simp
  hence "?L ≤ exp (- real l * KL_div γ (μ+Λ⇩a*(1-μ)))"
    using assms(4) unfolding μ_def by (intro kl_chernoff_property assms(1,2)) auto
  also have "... ≤ ?R"
    using assms(1) 1 by simp
  finally show ?thesis by simp
next
  case False
  hence "μ ≤ 0" by simp
  hence "card S = 0"
    unfolding μ_def n_def[symmetric] using n_gt_0 by (simp add:divide_simps)
  moreover have "finite S"
    using finite_subset[OF assms(2) finite_verts] by auto
  ultimately have 0:"S = {}" by auto
  have "μ = 0"
    unfolding μ_def 0 by simp
  hence "μ + Λ⇩a ≥0 "
    using Λ_ge_0 by simp
  hence "γ ≥ 0"
    using assms(5) by simp
  hence "γ * real l ≥ 0"
    by (intro mult_nonneg_nonneg) auto
  thus ?thesis using 0 by simp
qed

theorem (in regular_graph) walk_tail_bound_2:
  assumes "l > 0" "Λ⇩a ≤ Λ" "Λ > 0"
  assumes "S ⊆ verts G"
  defines "μ ≡ real (card S) / card (verts G)"
  assumes "γ < 1" "μ + Λ ≤ γ"
  shows "measure (pmf_of_multiset (walks G l)) {w. real (card {i ∈ {..<l}. w ! i ∈ S}) ≥ γ*l}
    ≤ exp (- real l * (γ * ln (1/(μ+Λ)) - 2 * exp(-1)))" (is "?L ≤ ?R")
proof (cases "μ > 0")
  case True

  have 0: "0 < μ + Λ⇩a"
    by (intro add_pos_nonneg Λ_ge_0 True)
  hence "0 < μ + Λ"
    using assms(2) by simp
  hence 1: "0 < (μ + Λ) * (μ + Λ⇩a)"
    using 0 by simp

  have 3:"μ + Λ⇩a ≤ γ"
    using assms(2,7) by simp
  have 2: "0 ≤ γ"
    using 3 True Λ_ge_0 by simp

  have "?L ≤ exp (- real l * (γ * ln (1/(μ+Λ⇩a)) - 2 * exp(-1)))"
    using 3 unfolding μ_def by (intro walk_tail_bound assms(1,4,6))
  also have "... = exp (- (real l * (γ * ln (1/(μ+Λ⇩a)) - 2 * exp(-1))))"
    by simp
  also have "... ≤ exp (- (real l * (γ * ln (1/(μ+Λ)) - 2 * exp(-1))))"
    using True assms(2,3) using 0 1 2
    by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono diff_mono iffD2[OF ln_le_cancel_iff]
        divide_left_mono le_imp_neg_le) simp_all
  also have "... = ?R"
    by simp
  finally show ?thesis by simp
next
  case False
  hence "μ ≤ 0" by simp
  hence "card S = 0"
    unfolding μ_def n_def[symmetric] using n_gt_0 by (simp add:divide_simps)
  moreover have "finite S"
    using finite_subset[OF assms(4) finite_verts] by auto
  ultimately have 0:"S = {}" by auto
  have "μ = 0"
    unfolding μ_def 0 by simp
  hence "μ + Λ⇩a ≥0 "
    using Λ_ge_0 by simp
  hence "γ ≥ 0"
    using assms by simp
  hence "γ * real l ≥ 0"
    by (intro mult_nonneg_nonneg) auto
  thus ?thesis using 0 by simp
qed

lemma (in expander_sample_space) tail_bound:
  fixes T
  assumes "l > 0" "Λ > 0"
  defines "μ ≡ measure (sample_pmf S) {w. T w}"
  assumes "γ < 1" "μ + Λ ≤ γ"
  shows "measure (ℰ l Λ S) {w. real (card {i ∈ {..<l}. T (w i)}) ≥ γ*l}
    ≤ exp (- real l * (γ * ln (1/(μ+Λ)) - 2 * exp(-1)))" (is "?L ≤ ?R")
proof -
  let ?w = "pmf_of_multiset (walks (graph_of e) l)"
  define V where "V = {v∈ verts (graph_of e). T (select S v)} "

  have 0: "card {i ∈ {..<l}. T (select S (w ! i))} = card {i ∈ {..<l}. w ! i ∈ V}"
    if "w  ∈ set_pmf (pmf_of_multiset (walks (graph_of e) l))" for w
  proof -
    have a0: "w ∈# walks (graph_of e) l" using that E.walks_nonempty by simp
    have "w ! i ∈ verts (graph_of e)" if "i < l" for i
      using that E.set_walks_3[OF a0] by auto
    thus ?thesis
      unfolding V_def
      by (intro arg_cong[where f="card"] restr_Collect_cong) auto
  qed

  have 1:"E.Λ⇩a ≤ Λ"
    using see_standard(1) unfolding is_expander_def e_def by simp

  have 2: "V ⊆ verts (graph_of e)"
    unfolding V_def by simp

  have "μ = measure (pmf_of_set {..<size S}) ({v. T (select S v)})"
    unfolding μ_def sample_pmf_alt[OF sample_space_S]
    by simp
  also have "... = real (card ({v∈{..<size S}. T (select S v)})) / real (size S)"
    using size_S_gt_0 by (subst measure_pmf_of_set) (auto simp add:Int_def)
  also have "... = real (card V) / card (verts (graph_of e))"
    unfolding V_def graph_of_def e_def using see_standard by (simp add:Int_commute)
  finally have μ_eq: "μ = real (card V) / card (verts (graph_of e))"
    by simp

  have "?L = measure ?w {y. γ * real l ≤ real (card {i ∈ {..<l}. T (select S (y ! i))})}"
    unfolding walks by simp
  also have "... = measure ?w {y. γ * real l ≤ real (card {i ∈ {..<l}. y ! i ∈ V})}"
    using 0 by (intro measure_pmf_cong) (simp)
  also have "... ≤ ?R"
    using assms(5) unfolding μ_eq
    by (intro E.walk_tail_bound_2 assms(1,2,4) 1 2) auto
  finally show ?thesis
    by simp
qed

definition C⇩1 :: real where "C⇩1 = exp 2 + exp 3 + (exp 1 - 1)"

lemma (in regular_graph) deviation_bound:
  fixes f :: "'a ⇒ real"
  assumes "l > 0"
  assumes "Λ⇩a ≤ exp (-real l * ln (real l)^3)"
  assumes "⋀x. x ≥ 20 ⟹ measure (pmf_of_set (verts G)) {v. f v ≥ x} ≤ exp (-x * ln x^3)"
  shows "measure (pmf_of_multiset (walks G l)) {w. (∑i←w. f i) ≥ C⇩1 * l} ≤ exp (- real l)"
    (is "?L ≤ ?R")
proof -
  let ?w = "pmf_of_multiset (walks G l)"
  let ?p = "pmf_of_set (verts G)"
  let ?a = "real l*(exp 2 + exp 3)"

  define b :: real where "b = exp 1 - 1"
  have b_gt_0: "b > 0"
    unfolding b_def by (approximation 5)

  define L where
    "L k = measure ?w {w. exp (real k)*card{i∈{..<l}.f(w!i)≥exp(real k)} ≥ real l/real k^2}" for k

  define k_max where "k_max = max 4 (MAX v ∈ verts G. nat ⌊ln (f v)⌋+1)"

  define Λ where "Λ = exp (-real l * ln (real l)^3)"

  have Λ⇩a_le_Λ: "Λ⇩a ≤ Λ"
    unfolding Λ_def using assms(2) by simp

  have Λ_gt_0: "Λ > 0"
    unfolding Λ_def by simp

  have k_max_ge_4: "k_max ≥ 4"
    unfolding k_max_def by simp
  have k_max_ge_3: "k_max ≥ 3"
    unfolding k_max_def by simp

  have 1:"of_bool(⌊ln(max x (exp 1))⌋+1=int k) =
    (of_bool(x ≥ exp (real k-1)) - of_bool(x ≥ exp k)::real)"
    (is "?L1 = ?R1") if "k ≥ 3" for k x
  proof -
    have a1: "real k - 1 ≤ k" by simp
    have "?L1 = of_bool(⌊ln(max x (exp 1))⌋=int k-1)"
      by simp
    also have "... = of_bool(ln(max x (exp 1))∈{real k-1..<real k})"
      unfolding floor_eq_iff by simp
    also have "... = of_bool(exp(ln(max x (exp 1)))∈{exp (real k-1)..<exp (real k)})"
      by simp
    also have "... = of_bool(max x (exp 1) ∈{exp (real k-1)..<exp (real k)})"
      by (subst exp_ln) (auto intro!:max.strict_coboundedI2)
    also have "... = of_bool(x ∈{exp (real k-1)..<exp (real k)})"
    proof (cases "x ≥ exp 1")
      case True
      then show ?thesis by simp
    next
      case False
      have "{exp (real k - 1)..<exp (real k)} ⊆ {exp (real k - 1)..}"
        by auto
      also have "... ⊆ {exp 1..}"
        using that by simp
      finally have "{exp (real k - 1)..<exp (real k)} ⊆ {exp 1..}" by simp
      moreover have "x ∉ {exp 1..}"
        using False by simp
      ultimately have "x ∉ {exp (real k - 1)..<exp (real k)}" by blast
      hence "of_bool(x ∈{exp (real k-1)..<exp (real k)}) = 0" by simp
      also have "... = of_bool(max x (exp 1) ∈{exp (real k-1)..<exp (real k)})"
        using False that by simp
      finally show ?thesis by metis
    qed
    also have "... = ?R1"
      using order_trans[OF iffD2[OF exp_le_cancel_iff a1]] by auto
    finally show ?thesis by simp
  qed

  have 0: "{nat ⌊ln (max (f x) (exp 1))⌋+1} ⊆ {2..k_max}" (is "{?L1} ⊆ ?R2")
    if "x ∈ verts G" for x
  proof (cases "f x ≥ exp 1")
    case True
    hence "?L1 = nat ⌊ln (f x)⌋+1"
      by simp
    also have "... ≤ (MAX v ∈ verts G. nat ⌊ln (f v)⌋+1)"
      by (intro Max_ge finite_imageI imageI that) auto
    also have "... ≤ k_max"
      unfolding k_max_def by simp
    finally have le_0: "?L1 ≤ k_max"
      by simp
    have "(1::nat) ≤ nat ⌊ln (exp (1::real))⌋"
      by simp
    also have "... ≤ nat ⌊ln (f x)⌋"
      using True order_less_le_trans[OF exp_gt_zero]
      by (intro nat_mono floor_mono iffD2[OF ln_le_cancel_iff]) auto
    finally have "1 ≤ nat ⌊ln (f x)⌋" by simp
    hence "?L1 ≥ 2"
      using True by simp
    hence "?L1 ∈ ?R2"
      using le_0 by simp
    then show ?thesis by simp
  next
    case False
    hence "{?L1} = {2}"
      by simp
    also have "... ⊆ ?R2"
      using k_max_ge_3 by simp
    finally show ?thesis by simp
  qed

  have 2:"(∑i←w. f i) ≤ ?a+b*(∑k=3..<k_max. exp k * card {i∈{..<l}. f (w!i)≥exp k})"
    (is "?L1 ≤ ?R1") if "w ∈# walks G l" for w
  proof -
    have l_w: "length w = l"
      using set_walks that by auto
    have s_w: "set w ⊆ verts G"
      using set_walks that by auto

    have "?L1 ≤ (∑i←w. exp( ln (max (f i) (exp 1))))"
      by (intro sum_list_mono) (simp add:less_max_iff_disj)
    also have "... ≤ (∑i←w. exp (of_nat (nat ⌊ln (max (f i) (exp 1))⌋+1)))"
      by (intro sum_list_mono iffD2[OF exp_le_cancel_iff]) linarith
    also have "... = (∑i←w. (∑k=2..k_max. exp k * of_bool (k=nat ⌊ln (max (f i)(exp 1))⌋+1)))"
      using Int_absorb1[OF 0] subsetD[OF s_w] by (intro_cong "[σ⇩1 sum_list]" more:map_cong)
        (simp add:of_bool_def if_distrib if_distribR sum.If_cases)
    also have "...=
      (∑i←w.(∑k∈(insert 2{3..k_max}). exp k* of_bool(k=nat⌊ln(max(f i)(exp 1))⌋+1)))"
      using k_max_ge_3 by (intro_cong "[σ⇩1 sum_list]" more:map_cong sum.cong) auto
    also have "... = (∑i←w. exp 2* of_bool (2=nat ⌊ln (max (f i)(exp 1))⌋+1) +
      (∑k=3..k_max. exp k * of_bool (k=nat ⌊ln (max (f i)(exp 1))⌋+1)))"
      by (subst sum.insert) auto
    also have "... ≤ (∑i←w. exp 2*1+(∑k=3..k_max. exp k* of_bool(k=nat⌊ln(max(f i)(exp 1))⌋+1)))"
      by (intro sum_list_mono add_mono mult_left_mono) auto
    also have "... = (∑i←w. exp 2+(∑k=3..k_max. exp k* of_bool(⌊ln(max(f i)(exp 1))⌋+1=int k)))"
      by (intro_cong "[σ⇩1 sum_list,σ⇩1 of_bool, σ⇩2(+),σ⇩2(*)]" more:map_cong sum.cong) auto
    also have "... =
      (∑i←w. exp 2+(∑k=3..k_max. exp k*(of_bool(f i≥exp (real k-1))-of_bool(f i≥exp k))))"
      by (intro_cong "[σ⇩1 sum_list,σ⇩1 of_bool, σ⇩2(+),σ⇩2(*)]" more:map_cong sum.cong 1) auto
    also have "... =
      (∑i←w. exp 2+(∑k=2+1..<k_max+1. exp k*(of_bool(f i≥exp(real k-1))-of_bool(f i≥exp k))))"
      by (intro_cong "[σ⇩1 sum_list,σ⇩2(+)]" more:map_cong sum.cong) auto
    also have "... =
      (∑i←w. exp 2+(∑k=2..<k_max. exp (k+1)*(of_bool(f i≥exp k)-of_bool(f i≥exp (Suc k)))))"
      by (subst sum.shift_bounds_nat_ivl) simp
    also have "... = (∑i←w. exp 2+ (∑k=2..<k_max. exp (k+1)* of_bool(f i≥exp k))-
      (∑k=2..<k_max. exp (k+1)* of_bool(f i≥exp (k+1))))"
      by (simp add:sum_subtractf algebra_simps)
    also have "... = (∑i←w. exp 2+ (∑k=2..<k_max. exp (k+1)* of_bool(f i≥exp k))-
      (∑k=3..<k_max+1. exp k* of_bool(f i≥exp k)))"
      by (subst sum.shift_bounds_nat_ivl[symmetric]) (simp cong:sum.cong)
    also have "... = (∑i←w. exp 2+ (∑k∈ insert 2 {3..<k_max}. exp (k+1)* of_bool(f i≥exp k))-
      (∑k=3..<k_max+1. exp k* of_bool(f i≥exp k)))"
      using k_max_ge_3
      by (intro_cong "[σ⇩1 sum_list, σ⇩2 (+), σ⇩2 (-)]" more: map_cong sum.cong) auto
    also have "... = (∑i←w. exp 2+ exp 3 * of_bool (f i ≥ exp 2) +
      (∑k=3..<k_max. exp (k+1)* of_bool(f i≥exp k))-(∑k=3..<k_max+1. exp k* of_bool(f i≥exp k)))"
      by (subst sum.insert) (simp_all add:algebra_simps)
    also have "... ≤ (∑i←w. exp 2+exp 3+(∑k=3..<k_max. exp (k+1)* of_bool(f i≥exp k))-
      (∑k=3..<k_max+1. exp k* of_bool(f i≥exp k)))"
      by (intro sum_list_mono add_mono diff_mono) auto
    also have "... = (∑i←w. exp 2+exp 3+(∑k=3..<k_max. exp (k+1)* of_bool(f i≥exp k))-
      (∑k∈ insert k_max {3..<k_max}. exp k* of_bool(f i≥exp k)))"
      using k_max_ge_3 by (intro_cong "[σ⇩1 sum_list, σ⇩2 (+), σ⇩2 (-)]" more: map_cong sum.cong) auto
    also have "... = (∑i←w. exp 2+exp 3+(∑k=3..<k_max. (exp (k+1)-exp k)* of_bool(f i≥exp k))-
      (exp k_max * of_bool (f i≥ exp k_max)))"
      by (subst sum.insert) (auto simp add:sum_subtractf algebra_simps)
    also have "...≤(∑i←w. exp 2+exp 3+(∑k=3..<k_max. (exp (k+1)-exp k)* of_bool(f i≥exp k))-0)"
      by (intro sum_list_mono add_mono diff_mono) auto
    also have "... ≤(∑i←w. exp 2+exp 3+ (∑k=3..<k_max. (exp (k+1)-exp k)* of_bool(f i≥exp k)))"
      by auto
    also have "... = (∑i←w. exp 2+exp 3+ (∑k=3..<k_max. (exp 1-1)*(exp k* of_bool(f i≥exp k))))"
      by (simp add:exp_add algebra_simps)
    also have "... = (∑i←w. exp 2+exp 3+b*(∑k=3..<k_max. exp k* of_bool(f i≥exp k)))"
      unfolding b_def
      by (subst sum_distrib_left) simp
    also have "... = ?a+b*(∑i=0..<l. (∑k=3..<k_max. exp k* of_bool(f (w ! i)≥exp k)))"
      unfolding sum_list_sum_nth by (simp add:l_w sum_distrib_left[symmetric])
    also have "... = ?R1"
      by (subst sum.swap) (simp add:ac_simps Int_def)
    finally show ?thesis by simp
  qed

  have 3: "∃k∈{3..<k_max}. g k ≥ l/real k^2" if "(∑k=3..<k_max. g k) ≥ real l" for g
  proof (rule ccontr)
    assume a3: "¬(∃k∈{3..<k_max}. g k ≥ l/real k^2)"
    hence "g k < l/real k^2" if "k ∈{3..<k_max}" for k
      using that by force
    hence "(∑k=3..<k_max. g k) < (∑k=3..<k_max. l/real k^2)"
      using k_max_ge_4 by (intro sum_strict_mono) auto
    also have "... ≤ (∑k=3..<k_max. l/ (real k*(real k-1)))"
      by (intro sum_mono divide_left_mono) (auto simp:power2_eq_square)
    also have "... = l * (∑k=3..<k_max. 1 / (real k-1) - 1/k)"
      by (simp add:sum_distrib_left field_simps)
    also have "... = l * (∑k=2+1..<(k_max-1)+1. (-1)/k - (-1) / (real k-1))"
      by (intro sum.cong arg_cong2[where f="(*)"]) auto
    also have "... = l * (∑k=2..<(k_max-1). (-1)/(Suc k) - (-1) / k)"
      by (subst sum.shift_bounds_nat_ivl) auto
    also have "... = l * (1/2 - 1 / real (k_max - 1))"
      using k_max_ge_3 by (subst sum_Suc_diff') auto
    also have "... ≤ real l * (1 - 0)"
       by (intro mult_left_mono diff_mono) auto
    also have "... = l"
      by simp
    finally have "(∑k=3..<k_max. g k) < l" by simp
    thus "False"
      using that by simp
  qed

  have 4: "L k ≤ exp(-real l-k+2)" if "k ≥ 3" for k
  proof (cases "k ≤ ln l")
    case True
    define γ where "γ = 1 / (real k)⇧2 / exp (real k)"
    define S where "S = {v ∈ verts G. f v ≥ exp (real k)}"
    define μ where "μ = card S / card (verts G)"

    have exp_k_ubound: "exp (real k) ≤ real l"
      using True assms(1)
      by (simp add: ln_ge_iff)

    have "20 ≤ exp (3::real)"
      by (approximation 10)
    also have "... ≤ exp (real k)"
      using that by simp
    finally have exp_k_lbound: "20 ≤ exp (real k)"
      by simp

    have S_range: "S ⊆ verts G"
      unfolding S_def by simp

    have "μ = measure (pmf_of_set (verts G)) S"
      unfolding μ_def using verts_non_empty Int_absorb1[OF S_range]
      by (simp add:measure_pmf_of_set)
    also have "... = measure (pmf_of_set (verts G)) {v. f v ≥ exp (real k)}"
      unfolding S_def using verts_non_empty by (intro measure_pmf_cong) auto
    also have "... ≤ exp (- exp (real k) * ln (exp (real k)) ^ 3)"
      by (intro assms(3) exp_k_lbound)
    also have "... = exp (-(exp(real k) * real k^3))"
      by simp
    finally have μ_bound: "μ ≤ exp (-exp(real k) * real k^3)" by simp

    have "μ+Λ ≤ exp (-exp(real k) * real k^3) + exp (- real l * ln (real l) ^ 3)"
      unfolding Λ_def by (intro add_mono μ_bound) auto
    also have "... =  exp (-(exp(real k) * real k^3)) + exp (- (real l * ln (real l) ^ 3))"
      by simp
    also have "... ≤ exp (-(exp(real k) * real k^3)) + exp (-(exp(real k) * ln(exp (real k))^3))"
      using assms(1) exp_k_ubound by (intro add_mono iffD2[OF exp_le_cancel_iff] le_imp_neg_le
          mult_mono power_mono iffD2[OF ln_le_cancel_iff]) simp_all
    also have "... = 2 * exp (-exp(real k) * real k^3)"
      by simp
    finally have μ_Λ_bound: "μ+Λ ≤ 2 * exp (-exp(real k) * real k^3)"
      by simp

    have "μ+Λ ≤ 2 * exp (-exp(real k) * real k^3)"
      by (intro μ_Λ_bound)
    also have "... = exp (-exp(real k) * real k^3 + ln 2)"
      unfolding exp_add by simp
    also have "... = exp (-(exp(real k) * real k^3 - ln 2))"
      by simp
    also have "... ≤ exp (-((1+ real k) * real k^3 - ln 2))"
      using that by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le diff_mono mult_right_mono
          exp_ge_add_one_self_aux) auto
    also have "... = exp (-(real k^4 + (real k^3- ln 2)))"
      by (simp add:power4_eq_xxxx power3_eq_cube algebra_simps)
    also have "... ≤ exp (-(real k^4 + (2^3- ln 2)))" using that
      by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le add_mono diff_mono power_mono) auto
    also have "... ≤ exp (-(real k^4 + 0))"
      by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le add_mono order.refl) (approximation 5)
    also have "... ≤ exp (-(real k^3 * real k))"
      by (simp add:power4_eq_xxxx power3_eq_cube algebra_simps)
    also have "... ≤ exp (-(2^3 * real k))" using that
      by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le mult_right_mono power_mono) auto
    also have "... ≤ exp (-3* real k )"
      by (intro iffD2[OF exp_le_cancel_iff]) auto
    also have "... = exp (-(real k + 2 * real k) )"
      by simp
    also have "... ≤ exp (-(real k + 2 * ln k) )"
      using that
      by (intro iffD2[OF exp_le_cancel_iff] le_imp_neg_le add_mono mult_left_mono ln_bound) auto
    also have "... = exp (-(real k + ln(k^2)) )"
      using that by (subst ln_powr[symmetric]) auto
    also have "... = γ"
      using that unfolding γ_def exp_minus exp_add inverse_eq_divide
      by (simp add:algebra_simps)
    finally have μ_Λ_le_γ: "μ+Λ≤γ"
      by simp

    have "μ ≥ 0"
      unfolding μ_def n_def[symmetric] using n_gt_0
      by (intro divide_nonneg_pos) auto
    hence μ_Λ_gt_0: "μ+Λ>0"
      using Λ_gt_0 by simp

    have "γ = 1 / ((real k)⇧2 * exp (real k))"
      unfolding γ_def by simp
    also have "... ≤ 1 / (2^2 * exp 2)"
      using that by (intro divide_left_mono mult_mono power_mono) (auto)
    finally have γ_ubound: "γ ≤ 1 / (4 * exp 2)"
      by simp

    have "γ ≤ 1 / (4 * exp 2)"
      by (intro γ_ubound)
    also have "... < 1"
      by (approximation 5)
    finally have γ_lt_1: "γ < 1"
      by simp

    have γ_ge_0: "γ ≥ 0"
      using that unfolding γ_def by (intro divide_nonneg_pos) auto

    have "L k = measure ?w {w. γ*l ≤ real (card {i ∈ {..<l}. exp (real k) ≤ f (w ! i)})}"
      unfolding L_def γ_def using that
      by (intro_cong "[σ⇩2 measure]" more:Collect_cong) (simp add:field_simps)
    also have "... = measure ?w {w. γ*l ≤ real (card {i ∈ {..<l}. w ! i ∈ S})}"
    proof (rule measure_pmf_cong)
      fix x assume "x ∈ set_pmf ?w"
      hence "card {i ∈ {..<l}. exp (real k) ≤ f (x ! i)}=card {i ∈ {..<l}. x ! i ∈ S}"
        using walks_nonempty set_walks_3[of "x"] nth_mem unfolding S_def
        by (intro restr_Collect_cong arg_cong[where f="card"]) force
      thus "x∈{w. γ*l≤card{i∈{..<l}. exp k≤f (w ! i)}}⟷x∈{w. γ*l≤card {i ∈ {..<l}. w ! i ∈ S}}"
        by simp
    qed
    also have "... ≤ exp (- real l * (γ * ln (1/(μ+Λ)) - 2 * exp(-1)))"
      using μ_Λ_le_γ γ_lt_1 S_range Λ⇩a_le_Λ Λ_gt_0 unfolding μ_def
      by (intro walk_tail_bound_2 assms(1)) auto
    also have "... = exp ( real l * (γ * ln (μ+Λ) + 2 * exp (-1)))"
      using μ_Λ_gt_0 by (simp_all add:ln_div algebra_simps)
    also have "... ≤ exp ( real l * (γ * ln (2 * exp (-exp(real k) * real k^3)) + 2 * exp(-1)))"
      using μ_Λ_gt_0 μ_Λ_bound γ_ge_0
      by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono add_mono iffD2[OF ln_le_cancel_iff])
       simp_all
    also have "... = exp (real l * (γ * (ln 2 - exp (real k) * real k ^ 3) + 2 * exp (- 1)))"
      by (simp add:ln_mult)
    also have "... = exp (real l * (γ * ln 2 - real k + 2 * exp (- 1)))"
      using that unfolding γ_def by (simp add:field_simps power2_eq_square power3_eq_cube)
    also have "... ≤ exp (real l * (ln 2 / (4 * exp 2) - real k + 2 * exp (-1)))"
      using γ_ubound by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono add_mono diff_mono)
        (auto simp:divide_simps)
    also have "... = exp (real l * (ln 2 / (4 * exp 2) + 2 *exp(-1) - real k))"
      by simp
    also have "... ≤ exp (real l * (1 - real k))"
      by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono diff_mono order.refl of_nat_0_le_iff)
       (approximation 12)
    also have "... ≤ exp (-real l - real k + 2)"
    proof (intro iffD2[OF exp_le_cancel_iff])
      have "1 * (real k-2) ≤ real l * (real k-2)"
        using assms(1) that by (intro mult_right_mono) auto
      thus "real l * (1 - real k) ≤ - real l - real k + 2"
        by argo
    qed
    finally show ?thesis by simp
  next
    case False
    hence k_gt_l: "k ≥ ln l" by simp
    define γ where "γ = 1 / (real k)⇧2 / exp (real k)"

    have "20 ≤ exp (3::real)"
      by (approximation 10)
    also have "... ≤ exp (real k)"
      using that by simp
    finally have exp_k_lbound: "20 ≤ exp (real k)"
      by simp

    have γ_gt_0: "0 < γ"
      using that unfolding γ_def by (intro divide_pos_pos) auto

    hence γ_l_gt_0: "0 < γ * real l"
      using assms(1) by auto

    have "L k = measure ?w {w. γ*l ≤ real (card {i ∈ {..<l}. exp (real k) ≤ f (w ! i)})}"
      unfolding L_def γ_def using that
      by (intro_cong "[σ⇩2 measure]" more:Collect_cong) (simp add:field_simps)
    also have "... ≤ (∫w. real (card {i ∈ {..<l}. exp (real k) ≤ f (w ! i)}) ∂?w) / (γ*l)"
      using walks_nonempty γ_l_gt_0
      by (intro pmf_markov integrable_measure_pmf_finite) simp_all
    also have "... = (∫w. (∑i<l. of_bool (exp(real k) ≤ f (w ! i)))∂?w) / (γ*l)"
      by (intro_cong "[σ⇩2 (/)]" more:integral_cong_AE AE_pmfI) (auto simp add:Int_def)
    also have "... = (∑i<l. (∫w. of_bool (exp(real k) ≤ f (w ! i))∂?w)) / (γ*l)"
      using walks_nonempty
      by (intro_cong "[σ⇩2 (/)]" more:integral_sum integrable_measure_pmf_finite) auto
    also have "... = (∑i<l. (∫v. of_bool (exp(real k) ≤ f v)∂(map_pmf (λw. w!i) ?w))) / (γ*l)"
      by simp
    also have "... = (∑i<l. (∫v. of_bool (exp(real k) ≤ f v)∂?p)) / (γ*l)"
      by (intro_cong "[σ⇩2(/),σ⇩2(integral⇧L),σ⇩1 measure_pmf]" more:sum.cong uniform_property) auto
    also have "... = (∑i<l. (∫v. indicat_real {v. (exp(real k) ≤ f v)} v∂?p)) / (γ*l)"
      by (intro_cong "[σ⇩2(/),σ⇩2(integral⇧L)]" more:sum.cong) auto
    also have "... = (∑i<l. (measure ?p {v. f v ≥ exp (real k)})) / (γ*l)"
      by simp
    also have "... ≤ (∑i<l. exp (- exp (real k) * ln (exp (real k)) ^ 3)) / (γ*l)"
      using γ_l_gt_0 by (intro divide_right_mono sum_mono assms(3) exp_k_lbound) auto
    also have "... = exp (- exp (real k) * real k ^ 3) / γ"
      using assms(1) by simp
    also have "... = exp (real k + ln (k^2) - exp (real k) * real k ^ 3)"
      using that unfolding γ_def
      by (simp add:exp_add exp_diff exp_minus algebra_simps inverse_eq_divide)
    also have "... = exp (real k + 2 * ln k - exp (real k) * real k ^ 3)"
      using that by (subst ln_powr[symmetric]) auto
    also have "... ≤ exp (real k + 2 * real k - exp (ln l) * real k^3)"
      using that k_gt_l ln_bound
      by (intro iffD2[OF exp_le_cancel_iff] add_mono diff_mono mult_left_mono mult_right_mono) auto
    also have "... = exp (3* real k - l * (real k^3-1) -l)"
      using assms(1) by (subst exp_ln) (auto simp add:algebra_simps)
    also have "... ≤ exp (3* real k - 1 * (real k^3-1) -l)"
      using assms(1) that by (intro iffD2[OF exp_le_cancel_iff] diff_mono mult_right_mono) auto
    also have "... = exp (3* real k - real k * real k^2-1 -l+2)"
      by (simp add:power2_eq_square power3_eq_cube)
    also have "... ≤ exp (3* real k - real k * 2^2-0 -l+2)"
      using assms(1) that
      by (intro iffD2[OF exp_le_cancel_iff] add_mono diff_mono mult_left_mono power_mono) auto
    also have "... = exp (- real l - real k + 2)"
      by simp
    finally show ?thesis by simp
  qed

  have "?L ≤ measure ?w
    {w. ?a+b*(∑k=3..<k_max. exp (real k) * card {i∈{..<l}. f (w!i)≥exp (real k)}) ≥ C⇩1*l}"
    using order_trans[OF _ 2] walks_nonempty by (intro pmf_mono) simp
  also have "... = measure ?w
    {w. (∑k=3..<k_max. exp(real k)*card{i∈{..<l}.f(w!i)≥exp(real k)})≥l}"
    unfolding C⇩1_def b_def[symmetric] using b_gt_0
    by (intro_cong "[σ⇩2 measure]" more:Collect_cong) (simp add:algebra_simps)
  also have "... ≤ measure ?w
    {w. (∃k∈{3..<k_max}. exp (real k)*card{i∈{..<l}.f(w!i)≥exp(real k)} ≥ real l/real k^2)}"
    using 3 by (intro pmf_mono) simp
  also have "... = measure ?w
    (⋃k∈{3..<k_max}. {w. exp (real k)*card{i∈{..<l}.f(w!i)≥exp(real k)} ≥ real l/real k^2})"
    by (intro_cong "[σ⇩2 measure]") auto
  also have "... ≤ (∑k=3..<k_max. L k)"
    unfolding L_def
    by (intro finite_measure.finite_measure_subadditive_finite) auto
  also have "... ≤ (∑k=3..<k_max. exp (- real l - real k + 2))"
    by (intro sum_mono 4) auto
  also have "... = (∑k=0+3..<(k_max-3)+3. exp (- real l - real k + 2))"
    using k_max_ge_3 by (intro sum.cong) auto
  also have "... = (∑k=0..<k_max-3. exp (-1 - real l - real k))"
    by (subst sum.shift_bounds_nat_ivl) ( simp add:algebra_simps)
  also have "... = exp(-1-real l) * (∑k<k_max-3. exp (real k*(-1)))"
    using atLeast0LessThan
    by (simp add:exp_diff exp_add sum_distrib_left exp_minus inverse_eq_divide)
  also have "... = exp (-1-real l) * ((exp (- 1) ^ (k_max - 3) - 1) / (exp (- 1) - 1))"
    unfolding exp_of_nat_mult by (subst geometric_sum) auto
  also have "... = exp(-1-real l) * (1-exp (- 1) ^ (k_max - 3)) / (1-exp (- 1))"
    by (simp add:field_simps)
  also have "... ≤ exp(-1-real l) * (1-0) / (1-exp (- 1))"
    using k_max_ge_3
    by (intro mult_left_mono divide_right_mono diff_mono) auto
  also have "... = exp (-real l) * (exp (-1) / (1-exp(-1)))"
    by (simp add:exp_diff exp_minus inverse_eq_divide)
  also have "... ≤ exp (-real l) * 1"
    by (intro mult_left_mono exp_ge_zero) (approximation 10)
  finally show ?thesis
    by simp
qed

lemma (in expander_sample_space) deviation_bound:
  fixes f :: "'a ⇒ real"
  assumes "l > 0"
  assumes "Λ ≤ exp (-real l * ln (real l)^3)"
  assumes "⋀x. x ≥ 20 ⟹ measure (sample_pmf S) {v. f v ≥ x} ≤ exp (-x * ln x^3)"
  shows "measure (ℰ l Λ S) {ω. (∑i<l. f (ω i)) ≥ C⇩1 * l} ≤ exp (- real l)"  (is "?L ≤ ?R")
proof -
  let ?w = "pmf_of_multiset (walks (graph_of e) l)"

  have "E.Λ⇩a ≤ Λ"
    using see_standard(1) unfolding is_expander_def e_def by simp
  also have "... ≤  exp (- real l * ln (real l) ^ 3)"
    using assms(2) by simp
  finally have 0: "E.Λ⇩a ≤ exp (- real l * ln (real l) ^ 3)"
    by simp

  have 1: "measure (pmf_of_set (verts (graph_of e))) {v. x ≤ f (select S v)} ≤ exp (- x*ln x^3)"
    (is "?L1 ≤ ?R1") if "x ≥ 20" for x
  proof -
    have "?L1 = measure (map_pmf (select S) (pmf_of_set {..<size S})) {v. x ≤ f v}"
      using see_standard(2) unfolding e_def graph_of_def by simp
    also have "... = measure (sample_pmf S) {v. x ≤ f v}"
      unfolding sample_pmf_alt[OF sample_space_S] by simp
    also have "... ≤ ?R1"
      by (intro assms(3) that)
    finally show ?thesis
      by simp
  qed

  have "?L = measure ?w {w. C⇩1 * real l ≤ (∑i<l. f (select S (w ! i)))}"
    unfolding walks by simp
  also have "... = measure ?w {ws. C⇩1 * real l ≤ (∑w←ws. f (select S w))}"
    using E.walks_nonempty E.set_walks_3 atLeast0LessThan
    unfolding sum_list_sum_nth by (intro measure_pmf_cong) simp
  also have "... ≤ ?R"
    by (intro E.deviation_bound assms(1) 0 1)
  finally show ?thesis by simp
qed

unbundle no_intro_cong_syntax

end