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.Pseudorandom_Objects_Expander_Walks
    "HOL-Decision_Procs.Approximation"
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 disjI_safe: "(¬x ⟹ y) ⟹  x ∨ y" by auto

lemma walk_tail_bound:
  fixes T
  assumes "l > 0" "Λ > 0"
  assumes "measure (sample_pro S) {w. T w} ≤ μ"
  assumes "γ ≤ 1" "μ + Λ ≤ γ" "μ ≤ 1"
  shows "measure (sample_pro (ℰ l Λ S)) {w. real (card {i ∈ {..<l}. T (w i)}) ≥ γ*l}
    ≤ exp (- real l * (γ * ln (1/(μ+Λ)) - 2 * exp(-1)))" (is "?L ≤ ?R")
proof -
  have μ_ge_0: "μ ≥ 0" using assms(3) measure_nonneg order.trans by metis
  hence γ_gt_0: "γ > 0" using assms(2,5) by auto
  hence γ_ge_0: "γ ≥ 0" by simp

  have "μ + Λ * (1 - μ) ≤ μ + Λ * 1" using assms(2,6) μ_ge_0 by auto
  also have "... ≤ γ" using assms(5) by simp
  finally have 1:"μ + Λ * (1 - μ) ≤ γ" by simp

  have 2: "0 < μ + Λ * (1 - μ)"
  proof (cases "μ = 1")
    case True then show ?thesis by simp
  next
    case False
    then show ?thesis  using assms(2,6)
      by (intro add_nonneg_pos μ_ge_0 linordered_semiring_strict_class.mult_pos_pos) auto
  qed

  have 3: "0 < μ + Λ" using μ_ge_0 assms(2) by simp

  have "γ * ln (1 / (μ + Λ)) - 2*exp (- 1) = γ * ln (1 / (μ + Λ*1))+0 -2*exp (-1)" by simp
  also have "... ≤ γ * ln (1 / (μ + Λ*(1-μ)))+0-2*exp(-1)"
    using 2 3 γ_ge_0 μ_ge_0 assms(2) by (intro diff_right_mono add_mono mult_left_mono
        iffD2[OF ln_le_cancel_iff] divide_left_mono divide_pos_pos) simp_all
  also have "... ≤ γ * ln (1 / (μ + Λ*(1-μ)))+(1-γ)*ln(1/(1-(μ+Λ*(1-μ))))-2* exp(-1)"
  proof (cases "γ < 1")
    case True
    hence "μ + Λ * (1 - μ) < 1" using 1 by simp
    thus ?thesis using assms(4) 2
      by (intro diff_right_mono add_mono mult_nonneg_nonneg order.refl ln_ge_zero) auto
  next
    case False
    hence "γ=1" using assms(4) by simp
    thus ?thesis by simp
  qed
  also have "... = (-exp(-1))+γ*ln(1/(μ+Λ*(1-μ)))+(-exp(-1))+(1-γ)*ln(1/(1-(μ+Λ*(1-μ))))"
    by simp
  also have "... ≤ γ*ln γ+γ*ln(1/(μ+Λ*(1-μ)))+(1-γ)*ln(1-γ)+(1-γ)*ln(1/(1-(μ+Λ*(1-μ))))"
    using assms(4) γ_ge_0 by (intro add_mono x_ln_x_min) auto
  also have "... = γ*(ln γ+ln(1/(μ+Λ*(1-μ))))+(1-γ)*(ln(1-γ)+ln(1/(1-(μ+Λ*(1-μ)))))"
    by (simp add:algebra_simps)
  also have "... = γ * ln (γ*(1/(μ+Λ*(1-μ))))+(1-γ)*ln((1-γ)*(1/(1-(μ+Λ*(1-μ)))))"
    using 2 1 assms(4) γ_gt_0 by (intro arg_cong2[where f="(+)"] iffD2[OF mult_cancel_left]
        disjI_safe ln_mult[symmetric] divide_pos_pos) auto
  also have "... = KL_div γ (μ+Λ*(1-μ))" unfolding KL_div_def by simp
  finally have 4: "γ * ln (1 / (μ + Λ)) - 2 * exp (- 1) ≤ KL_div γ (μ + Λ * (1 - μ))"
    by simp

  have "?L ≤ exp (- real l * KL_div γ (μ+Λ*(1-μ)))"
    using 1 by (intro expander_kl_chernoff_bound assms)
  also have "... ≤ exp (- real l * (γ * ln (1 / (μ + Λ)) - 2 * exp (- 1)))"
    by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg 4) auto
  finally show ?thesis by simp
qed

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

lemma deviation_bound:
  fixes f :: "'a ⇒ real"
  assumes "l > 0"
  assumes "Λ ∈ {0<..exp (-real l * ln (real l)^3)}"
  assumes "⋀x. x ≥ 20 ⟹ measure (sample_pro S) {v. f v ≥ x} ≤ exp (-x * ln x^3)"
  shows "measure (sample_pro (ℰ l Λ S)) {ω. (∑i<l. f (ω i)) ≥ C⇩1 * l} ≤ exp (- real l)"  (is "?L ≤ ?R")
proof -
  let ?w = "sample_pro (ℰ l Λ S)"
  let ?p = "sample_pro S"
  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 ∈ pro_set S. nat ⌊ln (f v)⌋+1)"

  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 ∈ pro_set S" for x
  proof (cases "f x ≥ exp 1")
    case True
    hence "?L1 = nat ⌊ln (f x)⌋+1" by simp
    also have "... ≤ (MAX v ∈ pro_set S. nat ⌊ln (f v)⌋+1)"
      by (intro Max_ge finite_imageI imageI that finite_pro_set)
    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<l. f (w i)) ≤ ?a+b*(∑k=3..<k_max. exp k * card {i∈{..<l}. f (w i)≥exp k})"
    (is "?L1 ≤ ?R1") if "w ∈ pro_set (ℰ l Λ S)" for w
  proof -
    have s_w: "w i ∈ pro_set S" for i
      using that expander_pro_range[OF assms(1)] assms(2)
      unfolding set_sample_pro[where S="ℰ l Λ S"] by auto

    have "?L1 ≤ (∑i<l. exp( ln (max (f (w i)) (exp 1))))"
      by (intro sum_mono) (simp add:less_max_iff_disj)
    also have "... ≤ (∑i<l. exp (of_nat (nat ⌊ln (max (f (w i)) (exp 1))⌋+1)))"
      by (intro sum_mono iffD2[OF exp_le_cancel_iff]) linarith
    also have "... = (∑i<l. (∑k=2..k_max. exp k * of_bool (k=nat ⌊ln (max (f (w i))(exp 1))⌋+1)))"
      using Int_absorb1[OF 0] s_w by (intro sum.cong map_cong refl)
       (simp add:of_bool_def if_distrib if_distribR sum.If_cases)
    also have "...=
      (∑i<l.(∑k∈(insert 2{3..k_max}). exp k* of_bool(k=nat⌊ln(max(f (w i))(exp 1))⌋+1)))"
      using k_max_ge_3 by (intro_cong "[σ⇩1 sum_list]" more:map_cong sum.cong) auto
    also have "... = (∑i<l. exp 2* of_bool (2=nat ⌊ln (max (f (w i))(exp 1))⌋+1) +
      (∑k=3..k_max. exp k * of_bool (k=nat ⌊ln (max (f (w i))(exp 1))⌋+1)))"
      by (subst sum.insert) auto
    also have "...≤(∑i<l. exp 2*1+(∑k=3..k_max. exp k* of_bool(k=nat⌊ln(max(f (w i))(exp 1))⌋+1)))"
      by (intro sum_mono add_mono mult_left_mono) auto
    also have "...=(∑i<l. exp 2+(∑k=3..k_max. exp k* of_bool(⌊ln(max(f (w 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<l. exp 2+(∑k=3..k_max. exp k*(of_bool(f (w i)≥exp (real k-1))-of_bool(f (w i)≥exp k))))"
      by (intro_cong "[σ⇩1 sum_list,σ⇩1 of_bool, σ⇩2(+),σ⇩2(*)]" more:map_cong sum.cong 1) auto
    also have "... = (∑i<l.
      exp 2+(∑k=2+1..<k_max+1. exp k*(of_bool(f (w i)≥exp(real k-1))-of_bool(f (w i)≥exp k))))"
      by (intro_cong "[σ⇩2(+)]" more:map_cong sum.cong) auto
    also have "... = (∑i<l.
      exp 2+(∑k=2..<k_max. exp (k+1)*(of_bool(f (w i)≥exp k)-of_bool(f (w i)≥exp (Suc k)))))"
      by (subst sum.shift_bounds_nat_ivl) simp
    also have "... = (∑i<l. exp 2+ (∑k=2..<k_max. exp (k+1)* of_bool(f (w i)≥exp k))-
      (∑k=2..<k_max. exp (k+1)* of_bool(f (w i)≥exp (k+1))))"
      by (simp add:sum_subtractf algebra_simps)
    also have "... = (∑i<l. exp 2+ (∑k=2..<k_max. exp (k+1)* of_bool(f (w i)≥exp k))-
      (∑k=3..<k_max+1. exp k* of_bool(f (w i)≥exp k)))"
      by (subst sum.shift_bounds_nat_ivl[symmetric]) (simp cong:sum.cong)
    also have "... = (∑i<l. exp 2+ (∑k∈ insert 2 {3..<k_max}. exp (k+1)* of_bool(f (w i)≥exp k))-
      (∑k=3..<k_max+1. exp k* of_bool(f (w i)≥exp k)))"
      using k_max_ge_3 by (intro_cong "[σ⇩2 (+), σ⇩2 (-)]" more: map_cong sum.cong) auto
    also have "... = (∑i<l. exp 2+ exp 3 * of_bool (f (w i) ≥ exp 2) +
      (∑k=3..<k_max. exp (k+1)* of_bool(f (w i)≥exp k)) -
      (∑k=3..<k_max+1. exp k* of_bool(f (w i)≥exp k)))"
      by (subst sum.insert) (simp_all add:algebra_simps)
    also have "... ≤ (∑i<l. exp 2+exp 3+(∑k=3..<k_max. exp (k+1)* of_bool(f (w i)≥exp k))-
      (∑k=3..<k_max+1. exp k* of_bool(f (w i)≥exp k)))"
      by (intro sum_mono add_mono diff_mono) auto
    also have "... = (∑i<l. exp 2+exp 3+(∑k=3..<k_max. exp (k+1)* of_bool(f (w i)≥exp k))-
      (∑k∈ insert k_max {3..<k_max}. exp k* of_bool(f (w i)≥exp k)))"
      using k_max_ge_3 by (intro_cong "[σ⇩2 (+), σ⇩2 (-)]" more: map_cong sum.cong) auto
    also have "... = (∑i<l. exp 2+exp 3+(∑k=3..<k_max. (exp (k+1)-exp k)* of_bool(f (w i)≥exp k))-
      (exp k_max * of_bool (f (w i)≥ exp k_max)))"
      by (subst sum.insert) (auto simp add:sum_subtractf algebra_simps)
    also have "...≤(∑i<l. exp 2+exp 3+(∑k=3..<k_max. (exp (k+1)-exp k)* of_bool(f(w i)≥exp k))-0)"
      by (intro sum_mono add_mono diff_mono) auto
    also have "... ≤(∑i<l. exp 2+exp 3+ (∑k=3..<k_max. (exp (k+1)-exp k)* of_bool(f(w i)≥exp k)))"
      by auto
    also have "... = (∑i<l. exp 2+exp 3+(∑k=3..<k_max.(exp 1-1)*(exp k* of_bool(f (w i)≥exp k))))"
      by (simp add:exp_add algebra_simps)
    also have "... = (∑i<l. exp 2+exp 3+b*(∑k=3..<k_max. exp k* of_bool(f (w i)≥exp k)))"
      unfolding b_def by (subst sum_distrib_left) simp
    also have "... = ?a+b*(∑i<l. (∑k=3..<k_max. exp k* of_bool(f (w i)≥exp k)))"
       by (simp add: 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 μ where "μ = exp (-exp(real k) * real k^3)"

    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 "measure (sample_pro S) {v. f v≥exp(real k)} ≤ 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: "measure (sample_pro S) {v. f v ≥ exp (real k)} ≤ μ" by (simp add:μ_def)

    have "μ+Λ ≤ exp (-exp(real k) * real k^3) + exp (- real l * ln (real l) ^ 3)"
      unfolding μ_def using assms by (intro add_mono) 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 by simp
    hence μ_Λ_gt_0: "μ+Λ>0" using assms(2) by auto

    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 μ_le_1: "μ ≤ 1" unfolding μ_def by simp

    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 "... ≤ exp (- real l * (γ * ln (1/(μ+Λ)) - 2 * exp(-1)))"
      using γ_lt_1 assms(2) by (intro walk_tail_bound μ_bound assms(1) μ_Λ_le_γ μ_le_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)"
      by (intro pmf_markov γ_l_gt_0) 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)"
      by (intro_cong "[σ⇩2 (/)]" more:integral_sum integrable_measure_pmf_finite finite_pro_set)
    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)" using assms(1,2)
      by (intro_cong "[σ⇩2(/),σ⇩2(integral⇧L),σ⇩1 measure_pmf]" more:sum.cong expander_uniform_property)
        simp_all
    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] 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

unbundle no_intro_cong_syntax

end