Quelle  Zigzag.thy

section ‹The Zigzag Lemma›
                                                        
theory Zigzag imports Bounding_X

begin                  
          
subsection ‹Lemma 8.1 (the actual Zigzag Lemma)›

definition "Big_ZZ_8_2 ≡ λk. (1 + eps k powr (1/2)) ≥ (1 + eps k) powr (eps k powr (-1/4))"
                                                 
text ‹An inequality that pops up in the proof of (39)›
definition "Big39 ≡ λk. 1/2 ≤ (1 + eps k) powr (-2 * eps k powr (-1/2))"

text ‹Two inequalities that pops up in the proof of (42)›
definition "Big42a ≡ λk. (1 + eps k)² / (1 - eps k powr (1/2)) ≤ 1 + 2 * k powr (-1/16)" 

definition "Big42b ≡ λk. 2 * k powr (-1/16) * k
                        + (1 + 2 * ln k / eps k + 2 * k powr (7/8)) / (1 - eps k powr (1/2))
                       ≤ real k powr (19/20)"

definition "Big_ZZ_8_1 ≡
   λμ l. Big_Blue_4_1 μ l ∧ Big_Red_5_1 μ l ∧ Big_Red_5_3 μ l ∧ Big_Y_6_5_Bblue l
        ∧ (∀k. k≥l ⟶ Big_height_upper_bound k ∧ Big_ZZ_8_2 k ∧ k≥16 ∧ Big39 k
                      ∧ Big42a k ∧ Big42b k)"

text ‹@{term "k≥16"} is for @{text Y_6_5_Red}›


lemma Big_ZZ_8_1:
  assumes "0<μ0" "μ1<1" 
  shows "∀^\<infinity>l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_ZZ_8_1 μ l"
  using assms Big_Blue_4_1 Big_Red_5_1 Big_Red_5_3 Big_Y_6_5_Bblue
  unfolding Big_ZZ_8_1_def Big_ZZ_8_2_def Big39_def Big42a_def Big42b_def
            eventually_conj_iff all_imp_conj_distrib eps_def
  apply (simp add: eventually_conj_iff eventually_frequently_const_simps)   
  apply (intro conjI strip eventually_all_ge_at_top Big_height_upper_bound; real_asymp)
  done

lemma (in Book) ZZ_8_1:
  assumes big: "Big_ZZ_8_1 μ l" 
  defines "R ≡ Step_class {red_step}"
  defines "sum_SS ≡ (∑i∈dboost_star. (1 - beta i) / beta i)"
  shows "sum_SS ≤ card R + k powr (19/20)"
proof -
  define pp where "pp ≡ λi h. if h=1 then min (pseq i) (qfun 1)
                          else if pseq i ≤ qfun (h-1) then qfun (h-1)
                          else if pseq i ≥ qfun h then qfun h
                          else pseq i"
  define Δ where "Δ ≡ λi. pseq (Suc i) - pseq i"
  define ΔΔ where "ΔΔ ≡ λi h. pp (Suc i) h - pp i h"
  have pp_eq: "pp i h = (if h=1 then min (pseq i) (qfun 1)
                          else max (qfun (h-1)) (min (pseq i) (qfun h)))" for i h
    using qfun_mono [of "h-1" h] by (auto simp: pp_def max_def)

  define maxh where "maxh ≡ nat⌊2 * ln k / ε⌋ + 1"  
  have maxh: "∧pseq. pseq≤1 ==> hgt pseq ≤ 2 * ln k / ε" and "k≥16"
    using big l_le_k by (auto simp: Big_ZZ_8_1_def height_upper_bound)
  then have "1 ≤ 2 * ln k / ε"
    using hgt_gt0 [of 1] by force
  then have "maxh > 1"
    by (simp add: maxh_def eps_gt0)
  have "hgt pseq < maxh" if "pseq≤1"for pseq
    using that kn0 maxh[of "pseq"] unfolding maxh_def by linarith
  then have hgt_le_maxh: "hgt (pseq i) < maxh" for i
    using pee_le1 by auto

  have pp_eq_hgt [simp]: "pp i (hgt (pseq i)) = pseq i" for i
    using hgt_less_imp_qfun_less [of "hgt (pseq i) - 1" "pseq i"]  
    using hgt_works [of "pseq i"] hgt_gt0 [of "pseq i"] kn0 pp_eq by force

  have pp_less_hgt [simp]: "pp i h = qfun h" if "0<h" "h < hgt (pseq i)" for h i
  proof (cases "h=1")
    case True
    then show ?thesis
      using hgt_less_imp_qfun_less pp_def that by auto
  next
    case False
    with that show ?thesis
      using alpha_def alpha_ge0 hgt_less_imp_qfun_less pp_eq by force
  qed

  have pp_gt_hgt [simp]: "pp i h = qfun (h-1)" if "h > hgt (pseq i)" for h i
    using hgt_gt0 [of "pseq i"] kn0 that
    by (simp add: pp_def hgt_le_imp_qfun_ge)

  have Δ0: "Δ i ≥ 0 ⟷ (∀h>0. ΔΔ i h ≥ 0)" for i
  proof (intro iffI strip)
    fix h::nat
    assume "0 ≤ Δ i" "0 < h" then show "0 ≤ ΔΔ i h"
      using qfun_mono [of "h-1" h] kn0 by (auto simp: Δ_def ΔΔ_def pp_def) 
  next
    assume "∀h>0. 0 ≤ ΔΔ i h"
    then have "pseq i ≤ pp (Suc i) (hgt (pseq i))"
      unfolding ΔΔ_def
      by (smt (verit, best) hgt_gt0 pp_eq_hgt)
    then show "0 ≤ Δ i"
      using hgt_less_imp_qfun_less [of "hgt (pseq i) - 1" "pseq i"]  
      using hgt_gt0 [of "pseq i"] kn0
      by (simp add: Δ_def pp_def split: if_split_asm)
  qed

  have sum_pp_aux: "(∑h=Suc 0..n. pp i h)
                  = (if hgt (pseq i) ≤ n then pseq i + (∑h=1..<n. qfun h) else (∑h=1..n. qfun h))" 
    if "n>0" for n i
    using that
  proof (induction n)
    case (Suc n)
    show ?case
    proof (cases "n=0")
      case True
      then show ?thesis
        using kn0 hgt_Least [of 1 "pseq i"]
        by (simp add: pp_def hgt_le_imp_qfun_ge min_def)
    next
      case False
      with Suc show ?thesis
        by (simp split: if_split_asm) (smt (verit) le_Suc_eq not_less_eq pp_eq_hgt sum.head_if)
    qed
  qed auto
  have sum_pp: "(∑h=Suc 0..maxh. pp i h) = pseq i + (∑h=1..<maxh. qfun h)" for i
    using ‹1 < maxh› by (simp add: hgt_le_maxh less_or_eq_imp_le sum_pp_aux)
  have 33: "Δ i = (∑h=1..maxh. ΔΔ i h)" for i
    by (simp add: ΔΔ_def Δ_def sum_subtractf sum_pp)

  have "(∑i<halted_point. ΔΔ i h) = 0" 
    if "∧i. i≤halted_point ==> h > hgt (pseq i)" for h
    using that by (simp add: sum.neutral ΔΔ_def)
  then have B: "(∑i<halted_point. ΔΔ i h) = 0" if "h ≥ maxh" for h
    by (meson hgt_le_maxh le_simps le_trans not_less_eq that)
  have "(∑h=Suc 0..maxh. ∑i<halted_point. ΔΔ i h / alpha h) ≤ (∑h=Suc 0..maxh. 1)"
  proof (intro sum_mono)
    fix h
    assume "h ∈ {Suc 0..maxh}"
    have "(∑i<halted_point. ΔΔ i h) ≤ alpha h"
      using qfun_mono [of "h-1" h] kn0
      unfolding ΔΔ_def alpha_def sum_lessThan_telescope [where f = "λi. pp i h"]
      by (auto simp: pp_def pee_eq_p0)
    then show "(∑i<halted_point. ΔΔ i h / alpha h) ≤ 1"
      using alpha_ge0 [of h] by (simp add: divide_simps flip: sum_divide_distrib) 
  qed
  also have "… ≤ 1 + 2 * ln k / ε"
    using ‹maxh > 1› by (simp add: maxh_def)
  finally have 34: "(∑h=Suc 0..maxh. ∑i<halted_point. ΔΔ i h / alpha h) ≤ 1 + 2 * ln k / ε" .

  define D where "D ≡ Step_class {dreg_step}" 
  define B where "B ≡ Step_class {bblue_step}" 
  define S where "S ≡ Step_class {dboost_step}" 
  have "dboost_star ⊆ S"
    unfolding dboost_star_def S_def dboost_star_def by auto
  have BD_disj: "B∩D = {}" and disj: "R∩B = {}" "S∩B = {}" "R∩D = {}" "S∩D = {}" "R∩S = {}"
    by (auto simp: D_def R_def B_def S_def Step_class_def)

  have [simp]: "finite D" "finite B" "finite R" "finite S"
    using finite_components assms 
    by (auto simp: D_def B_def R_def S_def Step_class_insert_NO_MATCH)
  have "card R < k"
    using red_step_limit by (auto simp: R_def)

  have R52: "pseq (Suc i) - pseq i ≥ (1 - ε) * ((1 - beta i) / beta i) * alpha (hgt (pseq i))"
    and beta_gt0: "beta i > 0"
    and R53: "pseq (Suc i) ≥ pseq i ∧ beta i ≥ 1 / (real k)²"
        if "i ∈ S" for i
    using big Red_5_2 that by (auto simp: Big_ZZ_8_1_def Red_5_3 B_def S_def)
  have cardB: "card B ≤ l powr (3/4)" and bigY65B: "Big_Y_6_5_Bblue l"
    using big bblue_step_limit by (auto simp: Big_ZZ_8_1_def B_def)

  have ΔΔ_ge0: "ΔΔ i h ≥ 0" if "i ∈ S" "h ≥ 1" for i h
    using that R53 [OF ‹i ∈ S›] by (fastforce simp: ΔΔ_def pp_eq)
  have ΔΔ_eq_0: "ΔΔ i h = 0" if "hgt (pseq i) ≤ hgt (pseq (Suc i))" "hgt (pseq (Suc i)) < h" for h i
    using ΔΔ_def that by fastforce
  define oneminus where "oneminus ≡ 1 - ε powr (1/2)"
  have 35: "oneminus * ((1 - beta i) / beta i)
          ≤ (∑h=1..maxh. ΔΔ i h / alpha h)"   (is "?L ≤ ?R")
    if "i ∈ dboost_star" for i
  proof -
    have "i ∈ S"
      using ‹dboost_star ⊆ S› that by blast
    have [simp]: "real (hgt x - Suc 0) = real (hgt x) - 1" for x
      using hgt_gt0 [of x] by linarith
    have 36: "(1 - ε) * ((1 - beta i) / beta i) ≤ Δ i / alpha (hgt (pseq i))"
      using R52 alpha_gt0 [OF hgt_gt0] beta_gt0 that ‹dboost_star ⊆ S› by (force simp: Δ_def divide_simps)
    have k_big: "(1 + ε powr (1/2)) ≥ (1 + ε) powr (ε powr (-1/4))"
      using big l_le_k by (auto simp: Big_ZZ_8_1_def Big_ZZ_8_2_def)
    have *: "∧x::real. x > 0 ==> (1 - x powr (1/2)) * (1 + x powr (1/2)) = 1 - x"
      by (simp add: algebra_simps flip: powr_add)
    have "?L = (1 - ε) * ((1 - beta i) / beta i) / (1 + ε powr (1/2))"
      using beta_gt0 [OF ‹i ∈ S›] eps_gt0 k_big 
      by (force simp: oneminus_def divide_simps *)
    also have "… ≤ Δ i / alpha (hgt (pseq i)) / (1 + ε powr (1/2))"
      by (intro 36 divide_right_mono) auto
    also have "… ≤ Δ i / alpha (hgt (pseq i)) / (1 + ε) powr (real (hgt (pseq (Suc i))) - hgt (pseq i))"
    proof (intro divide_left_mono mult_pos_pos)
      have "real (hgt (pseq (Suc i))) - hgt (pseq i) ≤ ε powr (-1/4)"
        using that by (simp add: dboost_star_def)
      then show "(1 + ε) powr (real (hgt (pseq (Suc i))) - real (hgt (pseq i))) ≤ 1 + ε powr (1/2)"
        using k_big by (smt (verit) eps_ge0 powr_mono)
      show "0 ≤ Δ i / alpha (hgt (pseq i))"
        by (simp add: Δ0 ΔΔ_ge0 ‹i ∈ S› alpha_ge0)
      show "0 < (1 + ε) powr (real (hgt (pseq (Suc i))) - real (hgt (pseq i)))"
        using eps_gt0 by auto
    qed (auto simp: add_strict_increasing)
    also have "… ≤ Δ i / alpha (hgt (pseq (Suc i)))"
    proof -
      have "alpha (hgt (pseq (Suc i))) ≤ alpha (hgt (pseq i)) * (1 + ε) powr (real (hgt (pseq (Suc i))) - real (hgt (pseq i)))"
        using eps_gt0 hgt_gt0
        by (simp add: alpha_eq divide_right_mono flip: powr_realpow powr_add)
      moreover have "0 ≤ Δ i"
        by (simp add: Δ0 ΔΔ_ge0 ‹i ∈ S›)
      moreover have "0 < alpha (hgt (pseq (Suc i)))"
        by (simp add: alpha_gt0 hgt_gt0 kn0)
      ultimately show ?thesis
        by (simp add: divide_left_mono)
    qed
    also have "… ≤ ?R"
      unfolding 33 sum_divide_distrib
    proof (intro sum_mono)
      fix h
      assume h: "h ∈ {1..maxh}"
      show "ΔΔ i h / alpha (hgt (pseq (Suc i))) ≤ ΔΔ i h / alpha h"
      proof (cases  "hgt (pseq i) ≤ hgt (pseq (Suc i)) ∧ hgt (pseq (Suc i)) < h")
        case False
        then consider "hgt (pseq i) > hgt (pseq (Suc i))" | "hgt (pseq (Suc i)) ≥ h"
          by linarith
        then show ?thesis
        proof cases
          case 1
          then show ?thesis
            using R53 ‹i ∈ S› hgt_mono' kn0 by force
        next
          case 2
          have "alpha h ≤ alpha (hgt (pseq (Suc i)))"
            using "2" alpha_mono h by auto
          moreover have "0 ≤ ΔΔ i h"
            using ΔΔ_ge0 ‹i ∈ S› h by presburger
          moreover have "0 < alpha h"
            using h kn0 by (simp add: alpha_gt0 hgt_gt0)
          ultimately show ?thesis
            by (simp add: divide_left_mono)
        qed
      qed (auto simp: ΔΔ_eq_0)
    qed
    finally show ?thesis .
  qed
  ― ‹now we are able to prove claim 8.2›
  have "oneminus * sum_SS = (∑i∈dboost_star. oneminus * ((1 - beta i) / beta i))"
    using sum_distrib_left sum_SS_def by blast
  also have "… ≤ (∑i∈dboost_star. ∑h=1..maxh. ΔΔ i h / alpha h)"
    by (intro sum_mono 35)
  also have "… = (∑h=1..maxh. ∑i∈dboost_star. ΔΔ i h / alpha h)"
    using sum.swap by fastforce
  also have "… ≤ (∑h=1..maxh. ∑i∈S. ΔΔ i h / alpha h)"
    by (intro sum_mono sum_mono2) (auto simp: ‹dboost_star ⊆ S› ΔΔ_ge0 alpha_ge0)
  finally have 82: "oneminus * sum_SS
      ≤ (∑h=1..maxh. ∑i∈S. ΔΔ i h / alpha h)" .
  ― ‹leading onto claim 8.3›
  have Δalpha: "- 1 ≤ Δ i / alpha (hgt (pseq i))" if "i ∈ R" for i
    using Y_6_4_Red [of i] ‹i ∈ R›
    unfolding Δ_def R_def
    by (smt (verit, best) hgt_gt0 alpha_gt0 divide_minus_left less_divide_eq_1_pos)

  have "(∑i∈R. - (1 + ε)²) ≤ (∑i∈R. ∑h=1..maxh. ΔΔ i h / alpha h)"
  proof (intro sum_mono)
    fix i :: nat
    assume "i ∈ R"
    show "- (1 + ε)² ≤ (∑h = 1..maxh. ΔΔ i h / alpha h)"
    proof (cases "Δ i < 0")
      case True
      have "(1 + ε)² * -1 ≤ (1 + ε)² * (Δ i / alpha (hgt (pseq i)))"
        using Δalpha 
        by (smt (verit, best) power2_less_0 ‹i ∈ R› mult_le_cancel_left2 mult_minus_right)
      also have "… ≤ (∑h = 1..maxh. ΔΔ i h / alpha h)"
      proof -
        have le0: "ΔΔ i h ≤ 0" for h 
          using True by (auto simp: ΔΔ_def Δ_def pp_eq)
        have eq0: "ΔΔ i h = 0" if "1 ≤ h" "h < hgt (pseq i) - 2" for h 
        proof -
          have "hgt (pseq i) - 2 ≤ hgt (pseq (Suc i))"
            using Y_6_5_Red ‹16 ≤ k› ‹i ∈ R› unfolding R_def by blast
          then show ?thesis
            using that pp_less_hgt[of h] by (auto simp: ΔΔ_def pp_def)
        qed
        show ?thesis
          unfolding 33 sum_distrib_left sum_divide_distrib
        proof (intro sum_mono)
          fix h :: nat
          assume "h ∈ {1..maxh}"
          then have "1 ≤ h" "h ≤ maxh" by auto
          show "(1 + ε)² * (ΔΔ i h / alpha (hgt (pseq i))) ≤ ΔΔ i h / alpha h"
          proof (cases "h < hgt (pseq i) - 2")
            case True
            then show ?thesis
              using ‹1 ≤ h› eq0 by force
          next
            case False
            have *: "(1 + ε) ^ (hgt (pseq i) - Suc 0) ≤ (1 + ε)² * (1 + ε) ^ (h - Suc 0)"
              using False eps_ge0 unfolding power_add [symmetric] 
              by (intro power_increasing) auto
            have **: "(1 + ε)² * alpha h ≥ alpha (hgt (pseq i))"
              using ‹1 ≤ h› mult_left_mono [OF *, of "ε"] eps_ge0
              by (simp add: alpha_eq hgt_gt0 mult_ac divide_right_mono)
            show ?thesis
              using le0 alpha_gt0 ‹h≥1› hgt_gt0 mult_left_mono_neg [OF **, of "ΔΔ i h"]
              by (simp add: divide_simps mult_ac)
          qed
        qed
      qed
      finally show ?thesis
        by linarith 
    next
      case False
      then have "ΔΔ i h ≥ 0" for h
        using ΔΔ_def Δ_def pp_eq by auto
      then have "(∑h = 1..maxh. ΔΔ i h / alpha h) ≥ 0"
        by (simp add: alpha_ge0 sum_nonneg)
      then show ?thesis
        by (smt (verit, ccfv_SIG) sum_power2_ge_zero)
    qed
  qed
  then have 83: "- (1 + ε)² * card R ≤ (∑h=1..maxh. ∑i∈R. ΔΔ i h / alpha h)" 
    by (simp add: mult.commute sum.swap [of _ R])

  ― ‹now to tackle claim 8.4›

  have Δ0: "Δ i ≥ 0" if "i ∈ D" for i
    using Y_6_4_DegreeReg that unfolding D_def Δ_def by auto

  have 39: "-2 * ε powr(-1/2) ≤ (∑h = 1..maxh. (ΔΔ (i-1) h + ΔΔ i h) / alpha h)" (is "?L ≤ ?R")
    if "i ∈ B" for i
  proof -
    have "odd i"
      using step_odd that by (force simp: Step_class_insert_NO_MATCH B_def)
    then have "i>0"
      using odd_pos by auto
    show ?thesis
    proof (cases "Δ (i-1) + Δ i ≥ 0")
      case True
      with ‹i>0› have "ΔΔ (i-1) h + ΔΔ i h ≥ 0" if "h≥1" for h
        by (fastforce simp: ΔΔ_def Δ_def pp_eq)
      then have "(∑h = 1..maxh. (ΔΔ (i-1) h + ΔΔ i h) / alpha h) ≥ 0"
        by (force simp: alpha_ge0 intro: sum_nonneg)
      then show ?thesis
        by (smt (verit, ccfv_SIG) powr_ge_zero)
    next
      case False
      then have ΔΔ_le0: "ΔΔ (i-1) h + ΔΔ i h ≤ 0" if "h≥1" for h
        by (smt (verit, best) One_nat_def ΔΔ_def Δ_def ‹odd i› odd_Suc_minus_one pp_eq)
      have hge: "hgt (pseq (Suc i)) ≥ hgt (pseq (i-1)) - 2 * ε powr (-1/2)"
        using bigY65B that Y_6_5_Bblue by (fastforce simp: B_def)
      have ΔΔ0: "ΔΔ (i-1) h + ΔΔ i h = 0" if "0<h" "h < hgt (pseq (i-1)) - 2 * ε powr (-1/2)" for h
        using ‹odd i› that hge unfolding ΔΔ_def One_nat_def
        by (smt (verit) of_nat_less_iff odd_Suc_minus_one powr_non_neg pp_less_hgt)
      have big39: "1/2 ≤ (1 + ε) powr (-2 * ε powr (-1/2))"
        using big l_le_k by (auto simp: Big_ZZ_8_1_def Big39_def)
      have "?L * alpha (hgt (pseq (i-1))) * (1 + ε) powr (-2 * ε powr (-1/2))
           ≤ - (ε powr (-1/2)) * alpha (hgt (pseq (i-1)))"
        using mult_left_mono_neg [OF big39, of "- (ε powr (-1/2)) * alpha (hgt (pseq (i-1))) / 2"]
        using alpha_ge0 [of "hgt (pseq (i-1))"] eps_ge0
        by (simp add: mult_ac)
      also have "… ≤ Δ (i-1) + Δ i"
      proof -
        have "pseq (Suc i) ≥ pseq (i-1) - (ε powr (-1/2)) * alpha (hgt (pseq (i-1)))"
          using Y_6_4_Bblue that B_def by blast
        with ‹i>0› show ?thesis
          by (simp add: Δ_def)
      qed
      finally have "?L * alpha (hgt (pseq (i-1))) * (1 + ε) powr (-2 * ε powr (-1/2)) ≤ Δ (i-1) + Δ i" .
      then have "?L ≤ (1 + ε) powr (2 * ε powr (-1/2)) * (Δ (i-1) + Δ i) / alpha (hgt (pseq (i-1)))"
        using alpha_ge0 [of "hgt (pseq (i-1))"] eps_ge0 
        by (simp add: powr_minus divide_simps mult_ac)
      also have "… ≤ ?R"
      proof -
        have "(1 + ε) powr (2 * ε powr(-1/2)) * (ΔΔ (i - Suc 0) h + ΔΔ i h) / alpha (hgt (pseq (i - Suc 0)))
           ≤ (ΔΔ (i - Suc 0) h + ΔΔ i h) / alpha h"
          if h: "Suc 0 ≤ h" "h ≤ maxh" for h
        proof (cases "h < hgt (pseq (i-1)) - 2 * ε powr(-1/2)")
          case False
          then have "hgt (pseq (i-1)) - 1 ≤ 2 * ε powr(-1/2) + (h - 1)"
            using hgt_gt0 by (simp add: nat_less_real_le)
          then have *: "(1 + ε) powr (2 * ε powr(-1/2)) / alpha (hgt (pseq (i-1))) ≥ 1 / alpha h"
            using that eps_gt0 kn0 hgt_gt0
            by (simp add: alpha_eq divide_simps flip: powr_realpow powr_add)
          show ?thesis
            using mult_left_mono_neg [OF * ΔΔ_le0] that by (simp add: Groups.mult_ac) 
        qed (use h ΔΔ0 in auto)
        then show ?thesis
          by (force simp: 33 sum_distrib_left sum_divide_distrib simp flip: sum.distrib intro: sum_mono)
      qed
      finally show ?thesis .
    qed
  qed

  have B34: "card B ≤ k powr (3/4)"
    by (smt (verit) cardB l_le_k of_nat_0_le_iff of_nat_mono powr_mono2 zero_le_divide_iff)
  have "-2 * k powr (7/8) ≤ -2 * ε powr(-1/2) * k powr (3/4)"
    by (simp add: eps_def powr_powr flip: powr_add)
  also have "… ≤ -2 * ε powr(-1/2) * card B"
    using B34 by (intro mult_left_mono_neg powr_mono2) auto
  also have "… = (∑i∈B. -2 * ε powr(-1/2))"
    by simp
  also have "… ≤ (∑h = 1..maxh. ∑i∈B. (ΔΔ (i-1) h + ΔΔ i h) / alpha h)"
    unfolding sum.swap [of _ B] by (intro sum_mono 39)
  also have "… ≤ (∑h=1..maxh. ∑i∈B∪D. ΔΔ i h / alpha h)"
  proof (intro sum_mono)
    fix h
    assume "h ∈ {1..maxh}"
    have "B ⊆ {0<..}"
      using odd_pos [OF step_odd] by (auto simp: B_def Step_class_insert_NO_MATCH)
    with inj_on_diff_nat [of B 1] have inj_pred: "inj_on (λi. i - Suc 0) B"
      by (simp add: Suc_leI subset_eq)
    have "(∑i∈B. ΔΔ (i - Suc 0) h) = (∑i ∈ (λi. i-1) ` B. ΔΔ i h)"
      by (simp add: sum.reindex [OF inj_pred])
    also have "… ≤ (∑i∈D. ΔΔ i h)"
    proof (intro sum_mono2)
      show "(λi. i - 1) ` B ⊆ D"
        by (force simp: D_def B_def Step_class_insert_NO_MATCH intro: dreg_before_step')
      show "0 ≤ ΔΔ i h" if "i ∈ D ∖ (λi. i - 1) ` B" for i
        using that Δ0 ΔΔ_def Δ_def pp_eq by fastforce
    qed auto
    finally have "(∑i∈B. ΔΔ (i - Suc 0) h) ≤ (∑i∈D. ΔΔ i h)" .
    with alpha_ge0 [of h]
    show "(∑i∈B. (ΔΔ (i - 1) h + ΔΔ i h) / alpha h) ≤ (∑i ∈ B∪D. ΔΔ i h / alpha h)"
      by (simp add: BD_disj divide_right_mono sum.distrib sum.union_disjoint flip: sum_divide_distrib)
    qed
  finally have 84: "-2 * k powr (7/8) ≤ (∑h=1..maxh. ∑i∈B∪D. ΔΔ i h / alpha h)" .

  have m_eq: "{..<halted_point} = R ∪ S ∪ (B ∪ D)"
    using before_halted_eq by (auto simp: B_def D_def S_def R_def Step_class_insert_NO_MATCH)

  have "- (1 + ε)² * real (card R)
     + oneminus * sum_SS
     - 2 * real k powr (7/8) ≤ (∑h = Suc 0..maxh. ∑i∈R. ΔΔ i h / alpha h)
      + (∑h = Suc 0..maxh. ∑i∈S. ΔΔ i h / alpha h)
      + (∑h = Suc 0..maxh. ∑i ∈ B ∪ D. ΔΔ i h / alpha h) "
    using 82 83 84 by simp
  also have "… = (∑h = Suc 0..maxh. ∑i ∈ R ∪ S ∪ (B ∪ D). ΔΔ i h / alpha h)"
    by (simp add: sum.distrib disj sum.union_disjoint Int_Un_distrib Int_Un_distrib2)
  also have "… ≤ 1 + 2 * ln (real k) / ε"
    using 34 by (simp add: m_eq)
  finally
  have 41: "oneminus * sum_SS - (1 + ε)² * card R - 2 * k powr (7/8)
          ≤ 1 + 2 * ln k / ε" 
    by simp
  have big42: "(1 + ε)² / oneminus ≤ 1 + 2 * k powr (-1/16)"
              "2 * k powr (-1/16) * k
             + (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus
       ≤ real k powr (19/20)"
    using big l_le_k by (auto simp: Big_ZZ_8_1_def Big42a_def Big42b_def oneminus_def)
  have "oneminus > 0"
    using ‹16 ≤ k› eps_gt0 eps_less1 powr01_less_one by (auto simp: oneminus_def)
  with 41 have "sum_SS
        ≤ (1 + 2 * ln k / ε + (1 + ε)² * card R + 2 * k powr (7/8)) / oneminus" 
    by (simp add: mult_ac pos_le_divide_eq diff_le_eq)
  also have "… ≤ card R * (((1 + ε)²) / oneminus)
                 + (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus"
    by (simp add: field_simps add_divide_distrib)
  also have "… ≤ card R * (1 + 2 * k powr (-1/16))
                 + (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus"
    using big42 ‹oneminus > 0› by (intro add_mono mult_mono) auto
  also have "… ≤ card R + 2 * k powr (-1/16) * k
                 + (1 + 2 * ln k / ε + 2 * k powr (7/8)) / oneminus"
    using ‹card R < k› by (intro add_mono mult_mono) (auto simp: algebra_simps)
  also have "… ≤ real (card R) + real k powr (19/20)"
    using big42 by force
  finally show ?thesis .
qed

subsection ‹Lemma 8.5›

text ‹An inequality that pops up in the proof of (39)›
definition "inequality85 ≡ λk. 3 * eps k powr (1/4) * k ≤ k powr (19/20)"

definition "Big_ZZ_8_5 ≡
   λμ l. Big_X_7_5 μ l ∧ Big_ZZ_8_1 μ l ∧ Big_Red_5_3 μ l
      ∧ (∀k≥l. inequality85 k)"

lemma Big_ZZ_8_5:
  assumes "0<μ0" "μ1<1" 
  shows "∀^\<infinity>l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_ZZ_8_5 μ l"
  using assms Big_Red_5_3 Big_X_7_5 Big_ZZ_8_1
  unfolding Big_ZZ_8_5_def inequality85_def eps_def
  apply (simp add: eventually_conj_iff all_imp_conj_distrib)       
  apply (intro conjI strip eventually_all_ge_at_top; real_asymp)     
  done

lemma (in Book) ZZ_8_5:
  assumes big: "Big_ZZ_8_5 μ l" 
  defines "R ≡ Step_class {red_step}" and "S ≡ Step_class {dboost_step}"
  shows "card S ≤ (bigbeta / (1 - bigbeta)) * card R
        + (2 / (1-μ)) * k powr (19/20)"
proof -
  have [simp]: "finite S"
    by (simp add: S_def)
  moreover have "dboost_star ⊆ S"
    by (auto simp: dboost_star_def S_def)
  ultimately have "real (card S) - real (card dboost_star) = card (S∖dboost_star)"
    by (metis card_Diff_subset card_mono finite_subset of_nat_diff)
  also have "… ≤ 3 * ε powr (1/4) * k"
    using μ01 big X_7_5 by (auto simp: Big_ZZ_8_5_def dboost_star_def S_def)
  also have "… ≤ k powr (19/20)"
    using big l_le_k by (auto simp: Big_ZZ_8_5_def inequality85_def)
  finally have *: "real (card S) - card dboost_star ≤ k powr (19/20)" .
  have bigbeta_lt1: "bigbeta < 1" and bigbeta_gt0: "0 < bigbeta" and beta_gt0: "∧i. i ∈ S ==> beta i > 0" 
    using bigbeta_ge0 big by (auto simp: Big_ZZ_8_5_def S_def beta_gt0 bigbeta_gt0 bigbeta_less1)
  then have ge0: "bigbeta / (1 - bigbeta) ≥ 0"
    by auto
  show ?thesis
  proof (cases "dboost_star = {}")
    case True
    with * have "card S ≤ k powr (19/20)"
      by simp
    also have "… ≤ (2 / (1-μ)) * k powr (19/20)"
      using μ01 kn0 by (simp add: divide_simps)
    finally show ?thesis
      by (smt (verit, ccfv_SIG) mult_nonneg_nonneg of_nat_0_le_iff ge0) 
  next
    case False    
    have bb_le: "bigbeta ≤ μ"
      using big bigbeta_le by (auto simp: Big_ZZ_8_5_def)
    have "(card S - k powr (19/20)) / bigbeta ≤ card dboost_star / bigbeta"
      by (smt (verit) "*" bigbeta_ge0 divide_right_mono)
    also have "… = (∑i∈dboost_star. 1 / beta i)"
    proof (cases "card dboost_star = 0")
      case False
      then show ?thesis
        by (simp add: bigbeta_def Let_def inverse_eq_divide)
    qed (simp add: False card_eq_0_iff)
    also have "… ≤ real(card dboost_star) + card R + k powr (19/20)"
    proof -
      have "(∑i∈dboost_star. (1 - beta i) / beta i)
            ≤ real (card R) + k powr (19/20)"
        using ZZ_8_1 big unfolding Big_ZZ_8_5_def R_def by blast
      moreover have "(∑i∈dboost_star. beta i / beta i) = (∑i∈dboost_star. 1)"
        using ‹dboost_star ⊆ S› beta_gt0 by (intro sum.cong) force+
      ultimately show ?thesis
        by (simp add: field_simps diff_divide_distrib sum_subtractf)
    qed
    also have "… ≤ real(card S) + card R + k powr (19/20)"
      by (simp add: ‹dboost_star ⊆ S› card_mono)
    finally have "(card S - k powr (19/20)) / bigbeta ≤ real (card S) + card R + k powr (19/20)" .
    then have "card S - k powr (19/20) ≤ (real (card S) + card R + k powr (19/20)) * bigbeta"
      using bigbeta_gt0 by (simp add: field_simps)
    then have "card S * (1 - bigbeta) ≤ bigbeta * card R + (1 + bigbeta) * k powr (19/20)"
      by (simp add: algebra_simps)
    then have "card S ≤ (bigbeta * card R + (1 + bigbeta) * k powr (19/20)) / (1 - bigbeta)"
      using bigbeta_lt1 by (simp add: field_simps)
    also have "… = (bigbeta / (1 - bigbeta)) * card R
                  + ((1 + bigbeta) / (1 - bigbeta)) * k powr (19/20)"
      using bigbeta_gt0 bigbeta_lt1 by (simp add: divide_simps)
    also have "… ≤ (bigbeta / (1 - bigbeta)) * card R + (2 / (1-μ)) * k powr (19/20)"
      using μ01 bb_le by (intro add_mono order_refl mult_right_mono frac_le) auto
    finally show ?thesis .
  qed
qed

subsection ‹Lemma 8.6›

text ‹For some reason this was harder than it should have been.
 It does require a further small limit argument.›

definition "Big_ZZ_8_6 ≡
   λμ l. Big_ZZ_8_5 μ l ∧ (∀k≥l. 2 / (1-μ) * k powr (19/20) < k powr (39/40))"

lemma Big_ZZ_8_6:
  assumes "0<μ0" "μ1<1" 
  shows "∀^\<infinity>l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_ZZ_8_6 μ l"
  using assms Big_ZZ_8_5
  unfolding Big_ZZ_8_6_def
  apply (simp add: eventually_conj_iff all_imp_conj_distrib)  
  apply (intro conjI strip eventually_all_ge_at_top eventually_all_geI1 [where L=1])   
   apply real_asymp
  by (smt (verit, ccfv_SIG) frac_le powr_ge_zero)

lemma (in Book) ZZ_8_6:
  assumes big: "Big_ZZ_8_6 μ l" 
  defines "R ≡ Step_class {red_step}" and "S ≡ Step_class {dboost_step}"
    and "a ≡ 2 / (1-μ)"
  assumes s_ge: "card S ≥ k powr (39/40)"
  shows "bigbeta ≥ (1 - a * k powr (-1/40)) * (card S / (card S + card R))"
proof -
  have bigbeta_lt1: "bigbeta < 1" and bigbeta_gt0: "0 < bigbeta"
    using bigbeta_ge0 big 
    by (auto simp: Big_ZZ_8_6_def Big_ZZ_8_5_def bigbeta_less1 bigbeta_gt0 S_def)
  have "a > 0"
    using μ01 by (simp add: a_def)
  have s_gt_a: "a * k powr (19/20) < card S"
        and 85: "card S ≤ (bigbeta / (1 - bigbeta)) * card R + a * k powr (19/20)"
    using big l_le_k assms
    unfolding R_def S_def a_def Big_ZZ_8_6_def by (fastforce intro: ZZ_8_5)+
  then have t_non0: "card R ≠ 0"   ― ‹seemingly not provable without our assumption›
    using mult_eq_0_iff by fastforce
  then have "(card S - a * k powr (19/20)) / card R ≤ bigbeta / (1 - bigbeta)"
    using 85 bigbeta_gt0 bigbeta_lt1 t_non0 by (simp add: pos_divide_le_eq)
  then have "bigbeta ≥ (1 - bigbeta) * (card S - a * k powr (19/20)) / card R"
    by (smt (verit, ccfv_threshold) bigbeta_lt1 mult.commute le_divide_eq times_divide_eq_left)
  then have *: "bigbeta * (card R + card S - a * k powr (19/20)) ≥ card S - a * k powr (19/20)"
    using t_non0 by (simp add: field_simps)
  have "(1 - a * k powr - (1/40)) * card S ≤ card S - a * k powr (19/20)"
    using s_ge kn0 ‹a>0› t_non0 by (simp add: powr_minus field_simps flip: powr_add)
  then have "(1 - a * k powr (-1/40)) * (card S / (card S + card R))
          ≤ (card S - a * k powr (19/20)) / (card S + card R)"
    by (force simp: divide_right_mono)
  also have "… ≤ (card S - a * k powr (19/20)) / (card R + card S - a * k powr (19/20))"
    using s_gt_a ‹a>0› t_non0 by (intro divide_left_mono) auto
  also have "… ≤ bigbeta"
    using * s_gt_a
    by (simp add: divide_simps split: if_split_asm)
  finally show ?thesis .
qed

end