Theory Big_Blue_Steps
section ‹Big Blue Steps: theorems›
theory Big_Blue_Steps imports Book
begin
subsection ‹Material to delete for Isabelle 2025›
lemma gbinomial_mono:
fixes k::nat and a::real
assumes "of_nat k ≤ a" "a ≤ b" shows "a gchoose k ≤ b gchoose k"
using assms
by (force simp: gbinomial_prod_rev intro!: divide_right_mono prod_mono)
lemma gbinomial_is_prod: "(a gchoose k) = (∏i<k. (a - of_nat i) / (1 + of_nat i))"
unfolding gbinomial_prod_rev
by (induction k; simp add: divide_simps)
lemma smallo_multiples:
assumes f: "f ∈ o(real)" and "k>0"
shows "(λn. f (k * n)) ∈ o(real)"
unfolding smallo_def mem_Collect_eq
proof (intro strip)
fix c::real
assume "c>0"
then have "c/k > 0"
by (simp add: assms)
with assms have "∀⇩F n in sequentially. ¦f n¦ ≤ c / real k * n"
by (force simp: smallo_def del: divide_const_simps)
then obtain N where "⋀n. n≥N ⟹ ¦f n¦ ≤ c/k * n"
by (meson eventually_at_top_linorder)
then have "⋀m. (k*m)≥N ⟹ ¦f (k*m)¦ ≤ c/k * (k*m)"
by blast
with ‹k>0› have "∀⇩F m in sequentially. ¦f (k*m)¦ ≤ c/k * (k*m)"
by (smt (verit, del_insts) One_nat_def Suc_leI eventually_at_top_linorderI mult_1_left mult_le_mono)
then show "∀⇩F n in sequentially. norm (f (k * n)) ≤ c * norm (real n)"
by eventually_elim (use ‹k>0› in auto)
qed
subsection ‹Preliminaries›
text ‹A bounded increasing sequence of finite sets eventually terminates›
lemma Union_incseq_finite:
assumes fin: "⋀n. finite (A n)" and N: "⋀n. card (A n) < N" and "incseq A"
shows "∀⇩F k in sequentially. ⋃ (range A) = A k"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∀k. ∃l≥k. ⋃ (range A) ≠ A l"
using eventually_sequentially by force
then have "∀k. ∃l≥k. ∃m≥l. A m ≠ A l"
by (smt (verit, ccfv_threshold) ‹incseq A› cSup_eq_maximum image_iff monotoneD nle_le rangeI)
then have "∀k. ∃l≥k. A l - A k ≠ {}"
by (metis ‹incseq A› diff_shunt_var monotoneD nat_le_linear subset_antisym)
then obtain f where f: "⋀k. f k ≥ k ∧ A (f k) - A k ≠ {}"
by metis
have "card (A ((f^^i)0)) ≥ i" for i
proof (induction i)
case 0
then show ?case
by auto
next
case (Suc i)
have "card (A ((f ^^ i) 0)) < card (A (f ((f ^^ i) 0)))"
by (metis Diff_cancel ‹incseq A› card_seteq f fin leI monotoneD)
then show ?case
using Suc by simp
qed
with N show False
using linorder_not_less by auto
qed
text ‹Two lemmas for proving "bigness lemmas" over a closed interval›
lemma eventually_all_geI0:
assumes "∀⇩F l in sequentially. P a l"
"⋀l x. ⟦P a l; a≤x; x≤b; l ≥ L⟧ ⟹ P x l"
shows "∀⇩F l in sequentially. ∀x. a ≤ x ∧ x ≤ b ⟶ P x l"
by (smt (verit, del_insts) assms eventually_sequentially eventually_elim2)
lemma eventually_all_geI1:
assumes "∀⇩F l in sequentially. P b l"
"⋀l x. ⟦P b l; a≤x; x≤b; l ≥ L⟧ ⟹ P x l"
shows "∀⇩F l in sequentially. ∀x. a ≤ x ∧ x ≤ b ⟶ P x l"
by (smt (verit, del_insts) assms eventually_sequentially eventually_elim2)
text ‹Mehta's binomial function: convex on the entire real line and coinciding with
gchoose under weak conditions›
definition "mfact ≡ λa k. if a < real k - 1 then 0 else prod (λi. a - of_nat i) {0..<k}"
text ‹Mehta's special rule for convexity, my proof›
lemma convex_on_extend:
fixes f :: "real ⇒ real"
assumes cf: "convex_on {k..} f" and mon: "mono_on {k..} f"
and fk: "⋀x. x<k ⟹ f x = f k"
shows "convex_on UNIV f"
proof (intro convex_on_linorderI)
fix t x y :: real
assume t: "0 < t" "t < 1" and "x < y"
let ?u = "((1 - t) *⇩R x + t *⇩R y)"
show "f ?u ≤ (1 - t) * f x + t * f y"
proof (cases "k ≤ x")
case True
with ‹x < y› t show ?thesis
by (intro convex_onD [OF cf]) auto
next
case False
then have "x < k" and fxk: "f x = f k" by (auto simp: fk)
show ?thesis
proof (cases "k ≤ y")
case True
then have "f y ≥ f k"
using mon mono_onD by auto
have kle: "k ≤ (1 - t) * k + t * y"
using True segment_bound_lemma t by auto
have fle: "f ((1 - t) *⇩R k + t *⇩R y) ≤ (1 - t) * f k + t * f y"
using t True by (intro convex_onD [OF cf]) auto
with False
show ?thesis
proof (cases "?u < k")
case True
then show ?thesis
using ‹f k ≤ f y› fxk fk segment_bound_lemma t by auto
next
case False
have "f ?u ≤ f ((1 - t) *⇩R k + t *⇩R y)"
using kle ‹x < k› False t by (intro mono_onD [OF mon]) auto
then show ?thesis
using fle fxk by auto
qed
next
case False
with ‹x < k› show ?thesis
by (simp add: fk convex_bound_lt order_less_imp_le segment_bound_lemma t)
qed
qed
qed auto
lemma convex_mfact:
assumes "k>0"
shows "convex_on UNIV (λa. mfact a k)"
unfolding mfact_def
proof (rule convex_on_extend)
show "convex_on {real (k - 1)..} (λa. if a < real k - 1 then 0 else ∏i = 0..<k. a - real i)"
using convex_gchoose_aux [of k] assms
apply (simp add: convex_on_def Ball_def)
by (smt (verit, del_insts) distrib_right mult_cancel_right2 mult_left_mono)
show "mono_on {real (k - 1)..} (λa. if a < real k - 1 then 0 else ∏i = 0..<k. a - real i)"
using ‹k > 0› by (auto simp: mono_on_def intro!: prod_mono)
qed (use assms gr0_conv_Suc in force)
definition mbinomial :: "real ⇒ nat ⇒ real"
where "mbinomial ≡ λa k. mfact a k / fact k"
lemma convex_mbinomial: "k>0 ⟹ convex_on UNIV (λx. mbinomial x k)"
by (simp add: mbinomial_def convex_mfact convex_on_cdiv)
lemma mbinomial_eq_choose [simp]: "mbinomial (real n) k = n choose k"
by (simp add: binomial_gbinomial gbinomial_prod_rev mbinomial_def mfact_def)
lemma mbinomial_eq_gchoose [simp]: "k ≤ a ⟹ mbinomial a k = a gchoose k"
by (simp add: gbinomial_prod_rev mbinomial_def mfact_def)
subsection ‹Preliminaries: Fact D1›
text ‹from appendix D, page 55›
lemma Fact_D1_73_aux:
fixes σ::real and m b::nat
assumes σ: "0<σ" and bm: "real b < real m"
shows "((σ*m) gchoose b) * inverse (m gchoose b) = σ^b * (∏i<b. 1 - ((1-σ)*i) / (σ * (real m - real i)))"
proof -
have "((σ*m) gchoose b) * inverse (m gchoose b) = (∏i<b. (σ*m - i) / (real m - real i))"
using bm by (simp add: gbinomial_prod_rev prod_dividef atLeast0LessThan)
also have "… = σ^b * (∏i<b. 1 - ((1-σ)*i) / (σ * (real m - real i)))"
using bm σ by (induction b) (auto simp: field_simps)
finally show ?thesis .
qed
text ‹This is fact 4.2 (page 11) as well as equation (73), page 55.›
lemma Fact_D1_73:
fixes σ::real and m b::nat
assumes σ: "0<σ" "σ≤1" and b: "real b ≤ σ * m / 2"
shows "(σ*m) gchoose b ∈ {σ^b * (real m gchoose b) * exp (- (real b ^ 2) / (σ*m)) .. σ^b * (m gchoose b)}"
proof (cases "m=0 ∨ b=0")
case True
then show ?thesis
using True assms by auto
next
case False
then have "σ * m / 2 < real m"
using σ by auto
with b σ False have bm: "real b < real m"
by linarith
then have nonz: "m gchoose b ≠ 0"
by (simp add: flip: binomial_gbinomial)
have EQ: "((σ*m) gchoose b) * inverse (m gchoose b) = σ^b * (∏i<b. 1 - ((1-σ)*i) / (σ * (real m - real i)))"
using Fact_D1_73_aux ‹0<σ› bm by blast
also have "… ≤ σ ^ b * 1"
proof (intro mult_left_mono prod_le_1 conjI)
fix i assume "i ∈ {..<b}"
with b σ bm show "0 ≤ 1 - (1 - σ) * i / (σ * (real m - i))"
by (simp add: field_split_simps)
qed (use σ bm in auto)
finally have upper: "(σ*m) gchoose b ≤ σ^b * (m gchoose b)"
using nonz by (simp add: divide_simps flip: binomial_gbinomial)
have *: "exp (-2 * real i / (σ*m)) ≤ 1 - ((1-σ)*i) / (σ * (real m - real i))" if "i<b" for i
proof -
have "i ≤ m"
using bm that by linarith
have exp_le: "1-x ≥ exp (-2 * x)" if "0 ≤x" "x ≤ 1/2" for x::real
proof -
have "exp (-2 * x) ≤ inverse (1 + 2*x)"
using exp_ge_add_one_self that by (simp add: exp_minus)
also have "… ≤ 1-x"
using that by (simp add: mult_left_le field_simps)
finally show ?thesis .
qed
have "exp (-2 * real i / (σ*m)) = exp (-2 * (i / (σ*m)))"
by simp
also have "… ≤ 1 - i/(σ * m)"
using b that by (intro exp_le) auto
also have "… ≤ 1 - ((1-σ)*i) / (σ * (real m - real i))"
using σ b that ‹i ≤ m› by (simp add: field_split_simps)
finally show ?thesis .
qed
have "sum real {..<b} ≤ real b ^ 2 / 2"
by (induction b) (auto simp: power2_eq_square algebra_simps)
with σ have "exp (- (real b ^ 2) / (σ*m)) ≤ exp (- (2 * (∑i<b. i) / (σ*m)))"
by (simp add: mult_less_0_iff divide_simps)
also have "… = exp (∑i<b. -2 * real i / (σ*m))"
by (simp add: sum_negf sum_distrib_left sum_divide_distrib)
also have "… = (∏i<b. exp (-2 * real i / (σ*m)))"
using exp_sum by blast
also have "… ≤ (∏i<b. 1 - ((1-σ)*i) / (σ * (real m - real i)))"
using * by (force intro: prod_mono)
finally have "exp (- (real b)⇧2 / (σ * m)) ≤ (∏i<b. 1 - (1 - σ) * i / (σ * (real m - real i)))" .
with EQ have "σ^b * exp (- (real b ^ 2) / (σ*m)) ≤ ((σ*m) gchoose b) * inverse (real m gchoose b)"
by (simp add: σ)
with σ bm have lower: "σ^b * (real m gchoose b) * exp (- (real b ^ 2) / (σ*m)) ≤ (σ*m) gchoose b"
by (simp add: field_split_simps flip: binomial_gbinomial)
with upper show ?thesis
by simp
qed
text ‹Exact at zero, so cannot be done using the approximation method›
lemma exp_inequality_17:
fixes x::real
assumes "0 ≤ x" "x ≤ 1/7"
shows "1 - 4*x/3 ≥ exp (-3*x/2)"
proof (cases "x ≤ 1/12")
case True
have "exp (-3*x/2) ≤ 1/(1 + (3*x)/2)"
using exp_ge_add_one_self [of "3*x/2"] assms
by (simp add: exp_minus divide_simps)
also have "… ≤ 1 - 4*x/3"
using assms True mult_left_le [of "x*12"] by (simp add: field_simps)
finally show ?thesis .
next
case False
with assms have "x ∈ {1/12..1/7}"
by auto
then show ?thesis
by (approximation 12 splitting: x=5)
qed
text ‹additional part›
lemma Fact_D1_75:
fixes σ::real and m b::nat
assumes σ: "0<σ" "σ<1" and b: "real b ≤ σ * m / 2" and b': "b ≤ m/7" and σ': "σ ≥ 7/15"
shows "(σ*m) gchoose b ≥ exp (- (3 * real b ^ 2) / (4*m)) * σ^b * (m gchoose b)"
proof (cases "m=0 ∨ b=0")
case True
then show ?thesis
using True assms by auto
next
case False
with b b' σ have bm: "real b < real m"
by linarith
have *: "exp (- 3 * real i / (2*m)) ≤ 1 - ((1-σ)*i) / (σ * (real m - real i))" if "i<b" for i
proof -
have im: "0 ≤ i/m" "i/m ≤ 1/7"
using b' that by auto
have "exp (- 3* real i / (2*m)) ≤ 1 - 4*i / (3*m)"
using exp_inequality_17 [OF im] by (simp add: mult.commute)
also have "… ≤ 1 - 8*i / (7 * (real m - real b))"
proof -
have "real i * (real b * 7) ≤ real i * real m"
using b' by (simp add: mult_left_mono)
then show ?thesis
using b' by (simp add: field_split_simps)
qed
also have "… ≤ 1 - ((1-σ)*i) / (σ * (real m - real i))"
proof -
have 1: "(1 - σ) / σ ≤ 8/7"
using σ σ' that
by (simp add: field_split_simps)
have 2: "1 / (real m - real i) ≤ 1 / (real m - real b)"
using σ σ' b' that by (simp add: field_split_simps)
have §: "(1 - σ) / (σ * (real m - real i)) ≤ 8 / (7 * (real m - real b))"
using mult_mono [OF 1 2] b' that by auto
show ?thesis
using mult_left_mono [OF §, of i]
by (simp add: mult_of_nat_commute)
qed
finally show ?thesis .
qed
have EQ: "((σ*m) gchoose b) * inverse (m gchoose b) = σ^b * (∏i<b. 1 - ((1-σ)*i) / (σ * (real m - real i)))"
using Fact_D1_73_aux ‹0<σ› bm by blast
have "sum real {..<b} ≤ real b ^ 2 / 2"
by (induction b) (auto simp: power2_eq_square algebra_simps)
with σ have "exp (- (3 * real b ^ 2) / (4*m)) ≤ exp (- (3 * (∑i<b. i) / (2*m)))"
by (simp add: mult_less_0_iff divide_simps)
also have "… = exp (∑i<b. -3 * real i / (2*m))"
by (simp add: sum_negf sum_distrib_left sum_divide_distrib)
also have "… = (∏i<b. exp (-3 * real i / (2*m)))"
using exp_sum by blast
also have "… ≤ (∏i<b. 1 - ((1-σ)*i) / (σ * (real m - real i)))"
using * by (force intro: prod_mono)
finally have "exp (- (3 * real b ^ 2) / (4*m)) ≤ (∏i<b. 1 - (1-σ) * i / (σ * (real m - real i)))" .
with EQ have "σ^b * exp (- (3 * real b ^ 2) / (4*m)) ≤ ((σ*m) gchoose b) / (m gchoose b)"
by (simp add: assms field_simps)
with σ bm show ?thesis
by (simp add: field_split_simps flip: binomial_gbinomial)
qed
lemma power2_12: "m ≥ 12 ⟹ 25 * m⇧2 ≤ 2^m"
proof (induction m)
case 0
then show ?case by auto
next
case (Suc m)
then consider "m=11" | "m≥12"
by linarith
then show ?case
proof cases
case 1
then show ?thesis
by auto
next
case 2
then have "Suc(m+m) ≤ m*3" "m≥3"
using Suc by auto
then have "25 * Suc (m+m) ≤ 25 * (m*m)"
by (metis le_trans mult_le_mono2)
with Suc show ?thesis
by (auto simp: power2_eq_square algebra_simps 2)
qed
qed
text ‹How @{term b} and @{term m} are obtained from @{term l}›
definition b_of where "b_of ≡ λl::nat. nat⌈l powr (1/4)⌉"
definition m_of where "m_of ≡ λl::nat. nat⌈l powr (2/3)⌉"
definition "Big_Blue_4_1 ≡
λμ l. m_of l ≥ 12 ∧ l ≥ (6/μ) powr (12/5) ∧ l ≥ 15
∧ 1 ≤ 5/4 * exp (- real((b_of l)⇧2) / ((μ - 2/l) * m_of l)) ∧ μ > 2/l
∧ 2/l ≤ (μ - 2/l) * ((5/4) powr (1/b_of l) - 1)"
text ‹Establishing the size requirements for 4.1.
NOTE: it doesn't become clear until SECTION 9 that all bounds involving
the parameter @{term μ} must hold for a RANGE of values›
lemma Big_Blue_4_1:
assumes "0<μ0"
shows "∀⇧∞l. ∀μ. μ ∈ {μ0..μ1} ⟶ Big_Blue_4_1 μ l"
proof -
have 3: "3 / μ0 > 0"
using assms by force
have 2: "μ0 * nat ⌈3 / μ0⌉ > 2"
by (smt (verit, best) mult.commute assms of_nat_ceiling pos_less_divide_eq)
have "∀⇧∞l. 12 ≤ m_of l"
unfolding m_of_def by real_asymp
moreover have "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ (6 / μ) powr (12 / 5) ≤ l"
using assms
apply (intro eventually_all_geI0, real_asymp)
by (smt (verit, ccfv_SIG) divide_pos_pos frac_le powr_mono2)
moreover have "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 4 ≤ 5 * exp (- ((real (b_of l))⇧2 / ((μ - 2/l) * real (m_of l))))"
proof (intro eventually_all_geI0 [where L = "nat ⌈3/μ0⌉"])
show "∀⇧∞l. 4 ≤ 5 * exp (- ((real (b_of l))⇧2 / ((μ0 - 2/l) * real (m_of l))))"
unfolding b_of_def m_of_def using assms by real_asymp
next
fix l μ
assume §: "4 ≤ 5 * exp (- ((real (b_of l))⇧2 / ((μ0 - 2/l) * real (m_of l))))"
and "μ0 ≤ μ" "μ ≤ μ1" and lel: "nat ⌈3 / μ0⌉ ≤ l"
then have "l>0"
using "3" by linarith
then have 0: "m_of l > 0"
using 3 by (auto simp: m_of_def)
have "μ0 > 2/l"
using lel assms by (auto simp: divide_simps mult.commute)
then show "4 ≤ 5 * exp (- ((real (b_of l))⇧2 / ((μ - 2/l) * real (m_of l))))"
using order_trans [OF §] by (simp add: "0" ‹μ0 ≤ μ› frac_le)
qed
moreover have "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 2/l < μ"
using assms by (intro eventually_all_geI0, real_asymp, linarith)
moreover have "∀⇧∞l. ∀μ. μ0 ≤ μ ∧ μ ≤ μ1 ⟶ 2/l ≤ (μ - 2/l) * ((5 / 4) powr (1 / real (b_of l)) - 1)"
proof -
have "⋀l μ. μ0 ≤ μ ⟹ μ0 - 2/l ≤ μ - 2/l"
by (auto simp: divide_simps ge_one_powr_ge_zero mult.commute)
show ?thesis
using assms
unfolding b_of_def
apply (intro eventually_all_geI0, real_asymp)
by (smt (verit, best) divide_le_eq_1 ge_one_powr_ge_zero mult_right_mono of_nat_0_le_iff zero_le_divide_1_iff)
qed
ultimately show ?thesis
by (auto simp: Big_Blue_4_1_def eventually_conj_iff all_imp_conj_distrib)
qed
context Book
begin
proposition Blue_4_1:
assumes "X⊆V" and manyb: "many_bluish X"
and big: "Big_Blue_4_1 μ l"
shows "∃S T. good_blue_book X (S,T) ∧ card S ≥ l powr (1/4)"
proof -
have lpowr0[simp]: "0 ≤ ⌈l powr r⌉" for r
by (metis ceiling_mono ceiling_zero powr_ge_pzero)
define b where "b ≡ b_of l"
define W where "W ≡ {x∈X. bluish X x}"
define m where "m ≡ m_of l"
have "m>0" "m ≥ 6" "m ≥ 12" "b>0"
using big by (auto simp: Big_Blue_4_1_def m_def b_def b_of_def)
have Wbig: "card W ≥ RN k m"
using manyb by (simp add: W_def m_def m_of_def many_bluish_def)
with Red_Blue_RN obtain U where "U ⊆ W" and U_m_Blue: "size_clique m U Blue"
by (metis W_def ‹X ⊆ V› mem_Collect_eq no_Red_clique subset_eq)
then obtain "card U = m" and "clique U Blue" and "U ⊆ V" "finite U"
by (simp add: finV finite_subset size_clique_def)
have "finite X"
using ‹X⊆V› finV finite_subset by auto
have "k ≤ RN k m"
using ‹m≥12› by (simp add: RN_3plus')
moreover have "card W ≤ card X"
by (simp add: W_def ‹finite X› card_mono)
ultimately have "card X ≥ l"
using Wbig l_le_k by linarith
then have "U ≠ X"
by (metis U_m_Blue ‹card U = m› le_eq_less_or_eq no_Blue_clique size_clique_smaller)
then have "U ⊂ X"
using W_def ‹U ⊆ W› by blast
then have cardU_less_X: "card U < card X"
by (meson ‹X⊆V› finV finite_subset psubset_card_mono)
with ‹X⊆V› have cardXU: "card (X-U) = card X - card U"
by (meson ‹U ⊂ X› card_Diff_subset finV finite_subset psubset_imp_subset)
then have real_cardXU: "real (card (X-U)) = real (card X) - m"
using ‹card U = m› cardU_less_X by linarith
have [simp]: "m ≤ card X"
using ‹card U = m› cardU_less_X nless_le by blast
have lpowr23: "real l powr (2/3) ≤ real l powr 1"
using ln0 by (intro powr_mono) auto
then have "m ≤ l" "m≤k"
using l_le_k by (auto simp: m_def m_of_def)
then have "m < RN k m"
using ‹12 ≤ m› RN_gt2 by auto
also have cX: "RN k m ≤ card X"
using Wbig ‹card W ≤ card X› by linarith
finally have "card U < card X"
using ‹card U = m› by blast
text ‹First part of (10)›
have "card U * (μ * card X - card U) = m * (μ * (card X - card U)) - (1-μ) * m⇧2"
using cardU_less_X by (simp add: ‹card U = m› algebra_simps of_nat_diff numeral_2_eq_2)
also have "… ≤ real (card (Blue ∩ all_edges_betw_un U (X-U)))"
proof -
have dfam: "disjoint_family_on (λu. Blue ∩ all_edges_betw_un {u} (X-U)) U"
by (auto simp: disjoint_family_on_def all_edges_betw_un_def)
have "μ * (card X - card U) ≤ card (Blue ∩ all_edges_betw_un {u} (X-U)) + (1-μ) * m"
if "u ∈ U" for u
proof -
have NBU: "Neighbours Blue u ∩ U = U - {u}"
using ‹clique U Blue› Red_Blue_all singleton_not_edge that
by (force simp: Neighbours_def clique_def)
then have NBX_split: "(Neighbours Blue u ∩ X) = (Neighbours Blue u ∩ (X-U)) ∪ (U - {u})"
using ‹U ⊂ X› by blast
moreover have "Neighbours Blue u ∩ (X-U) ∩ (U - {u}) = {}"
by blast
ultimately have "card(Neighbours Blue u ∩ X) = card(Neighbours Blue u ∩ (X-U)) + (m - Suc 0)"
by (simp add: card_Un_disjoint finite_Neighbours ‹finite U› ‹card U = m› that)
then have "μ * (card X) ≤ real (card (Neighbours Blue u ∩ (X-U))) + real (m - Suc 0)"
using W_def ‹U ⊆ W› bluish_def that by force
then have "μ * (card X - card U)
≤ card (Neighbours Blue u ∩ (X-U)) + real (m - Suc 0) - μ *card U"
by (smt (verit) cardU_less_X nless_le of_nat_diff right_diff_distrib')
then have *: "μ * (card X - card U) ≤ real (card (Neighbours Blue u ∩ (X-U))) + (1-μ)*m"
using assms by (simp add: ‹card U = m› left_diff_distrib)
have "inj_on (λx. {u,x}) (Neighbours Blue u ∩ X)"
by (simp add: doubleton_eq_iff inj_on_def)
moreover have "(λx. {u,x}) ` (Neighbours Blue u ∩ (X-U)) ⊆ Blue ∩ all_edges_betw_un {u} (X-U)"
using Blue_E by (auto simp: Neighbours_def all_edges_betw_un_def)
ultimately have "card (Neighbours Blue u ∩ (X-U)) ≤ card (Blue ∩ all_edges_betw_un {u} (X-U))"
by (metis NBX_split card_inj_on_le finite_Blue finite_Int inj_on_Un)
with * show ?thesis
by auto
qed
then have "(card U) * (μ * real (card X - card U))
≤ (∑x∈U. card (Blue ∩ all_edges_betw_un {x} (X-U)) + (1-μ) * m)"
by (meson sum_bounded_below)
then have "m * (μ * (card X - card U))
≤ (∑x∈U. card (Blue ∩ all_edges_betw_un {x} (X-U))) + (1-μ) * m⇧2"
by (simp add: sum.distrib power2_eq_square ‹card U = m› mult_ac)
also have "… ≤ card (⋃u∈U. Blue ∩ all_edges_betw_un {u} (X-U)) + (1-μ) * m⇧2"
by (simp add: dfam card_UN_disjoint' ‹finite U› flip: UN_simps)
finally have "m * (μ * (card X - card U))
≤ card (⋃u∈U. Blue ∩ all_edges_betw_un {u} (X-U)) + (1-μ) * m⇧2" .
moreover have "(⋃u∈U. Blue ∩ all_edges_betw_un {u} (X-U)) = (Blue ∩ all_edges_betw_un U (X-U))"
by (auto simp: all_edges_betw_un_def)
ultimately show ?thesis
by simp
qed
also have "… ≤ edge_card Blue U (X-U)"
by (simp add: edge_card_def)
finally have edge_card_XU: "edge_card Blue U (X-U) ≥ card U * (μ * card X - card U)" .
define σ where "σ ≡ blue_density U (X-U)"
then have "σ ≥ 0" by (simp add: gen_density_ge0)
have "σ ≤ 1"
by (simp add: σ_def gen_density_le1)
have 6: "real (6*k) ≤ real (2 + k*m)"
by (metis mult.commute ‹6≤m› mult_le_mono2 of_nat_mono trans_le_add2)
then have km: "k + m ≤ Suc (k * m)"
using big l_le_k ‹m ≤ l› by linarith
have "m/2 * (2 + real k * (1-μ)) ≤ m/2 * (2 + real k)"
using assms μ01 by (simp add: algebra_simps)
also have "… ≤ (k - 1) * (m - 1)"
using big l_le_k 6 ‹m≤k› by (simp add: Big_Blue_4_1_def algebra_simps add_divide_distrib km)
finally have "(m/2) * (2 + k * (1-μ)) ≤ RN k m"
using RN_times_lower' [of k m] by linarith
then have "μ - 2/k ≤ (μ * card X - card U) / (card X - card U)"
using kn0 assms cardU_less_X ‹card U = m› cX by (simp add: field_simps)
also have "… ≤ σ"
using ‹m>0› ‹card U = m› cardU_less_X cardXU edge_card_XU
by (simp add: σ_def gen_density_def divide_simps mult_ac)
finally have eq10: "μ - 2/k ≤ σ" .
have "2 * b / m ≤ μ - 2/k"
proof -
have 512: "5/12 ≤ (1::real)"
by simp
with big have "l powr (5/12) ≥ ((6/μ) powr (12/5)) powr (5/12)"
by (simp add: Big_Blue_4_1_def powr_mono2)
then have lge: "l powr (5/12) ≥ 6/μ"
using assms μ01 powr_powr by force
have "2 * b ≤ 2 * (l powr (1/4) + 1)"
by (simp add: b_def b_of_def del: zero_le_ceiling distrib_left_numeral)
then have "2*b / m + 2/l ≤ 2 * (l powr (1/4) + 1) / l powr (2/3) + 2/l"
by (simp add: m_def m_of_def frac_le ln0 del: zero_le_ceiling distrib_left_numeral)
also have "… ≤ (2 * l powr (1/4) + 4) / l powr (2/3)"
using ln0 lpowr23 by (simp add: pos_le_divide_eq pos_divide_le_eq add_divide_distrib algebra_simps)
also have "… ≤ (2 * l powr (1/4) + 4 * l powr (1/4)) / l powr (2/3)"
using big by (simp add: Big_Blue_4_1_def divide_right_mono ge_one_powr_ge_zero)
also have "… = 6 / l powr (5/12)"
by (simp add: divide_simps flip: powr_add)
also have "… ≤ μ"
using lge assms μ01 by (simp add: divide_le_eq mult.commute)
finally have "2*b / m + 2/l ≤ μ" .
then show ?thesis
using l_le_k ‹m>0› ln0
by (smt (verit, best) frac_le of_nat_0_less_iff of_nat_mono)
qed
with eq10 have "2 / (m/b) ≤ σ"
by simp
moreover have "l powr (2/3) ≤ nat ⌈real l powr (2/3)⌉"
using of_nat_ceiling by blast
ultimately have ble: "b ≤ σ * m / 2"
using mult_left_mono ‹σ ≥ 0› big kn0 l_le_k
by (simp add: Big_Blue_4_1_def powr_diff b_def m_def divide_simps)
then have "σ > 0"
using ‹0 < b› ‹0 ≤ σ› less_eq_real_def by force
define Φ where "Φ ≡ ∑v ∈ X-U. card (Neighbours Blue v ∩ U) choose b"
text ‹now for the material between (10) and (11)›
have "σ * real m / 2 ≤ m"
using ‹σ ≤ 1› ‹m>0› by auto
with ble have "b ≤ m"
by linarith
have "μ^b * 1 * card X ≤ (5/4 * σ^b) * (5/4 * exp(- real(b⇧2) / (σ*m))) * (5/4 * (card X - m))"
proof (intro mult_mono)
have 2: "2/k ≤ 2/l"
by (simp add: l_le_k frac_le ln0)
also have "… ≤ (μ - 2/l) * ((5/4) powr (1/b) - 1)"
using big by (simp add: Big_Blue_4_1_def b_def)
also have "… ≤ σ * ((5/4) powr (1/b) - 1)"
using "2" ‹0 < b› eq10 by auto
finally have "2 / real k ≤ σ * ((5/4) powr (1/b) - 1)" .
then have 1: "μ ≤ (5/4)powr(1/b) * σ"
using eq10 ‹b>0› by (simp add: algebra_simps)
show "μ ^ b ≤ 5/4 * σ ^ b"
using power_mono[OF 1, of b] assms ‹σ>0› ‹b>0› μ01
by (simp add: powr_mult powr_powr flip: powr_realpow)
have "μ - 2/l ≤ σ"
using "2" eq10 by linarith
moreover have "2/l < μ"
using big by (auto simp: Big_Blue_4_1_def)
ultimately have "exp (- real(b⇧2) / ((μ - 2/l) * m)) ≤ exp (- real (b⇧2) / (σ * m))"
using ‹σ>0› ‹m>0› by (simp add: frac_le)
then show "1 ≤ 5/4 * exp (- real(b⇧2) / (σ * real m))"
using big unfolding Big_Blue_4_1_def b_def m_def
by (smt (verit, best) divide_minus_left frac_le mult_left_mono)
have "25 * (real m * real m) ≤ 2 powr m"
using of_nat_mono [OF power2_12 [OF ‹12 ≤ m›]] by (simp add: power2_eq_square powr_realpow)
then have "real (5 * m) ≤ 2 powr (real m / 2)"
by (simp add: powr_half_sqrt_powr power2_eq_square real_le_rsqrt)
moreover
have "card X > 2 powr (m/2)"
by (metis RN_commute RN_lower_nodiag ‹6 ≤ m› ‹m≤k› add_leE less_le_trans cX numeral_Bit0 of_nat_mono)
ultimately have "5 * m ≤ real (card X)"
by linarith
then show "card X ≤ 5/4 * (card X - m)"
using ‹card U = m› cardU_less_X by simp
qed (use ‹0 ≤ σ› in auto)
also have "… = (125/64) * (σ^b) * exp(- (real b)⇧2 / (σ*m)) * (card X - m)"
by simp
also have "… ≤ 2 * (σ^b) * exp(- (real b)⇧2 / (σ*m)) * (card X - m)"
by (intro mult_right_mono) (auto simp: ‹0 ≤ σ›)
finally have "μ^b/2 * card X ≤ σ^b * exp(- of_nat (b⇧2) / (σ*m)) * card (X-U)"
by (simp add: ‹card U = m› cardXU real_cardXU)
also have "… ≤ 1/(m choose b) * ((σ*m) gchoose b) * card (X-U)"
proof (intro mult_right_mono)
have "0 < real m gchoose b"
by (metis ‹b ≤ m› binomial_gbinomial of_nat_0_less_iff zero_less_binomial_iff)
then have "σ ^ b * ((real m gchoose b) * exp (- ((real b)⇧2 / (σ * real m)))) ≤ σ * real m gchoose b"
using Fact_D1_73 [OF ‹σ>0› ‹σ≤1› ble] ‹b≤m› cardU_less_X ‹0 < σ›
by (simp add: field_split_simps binomial_gbinomial)
then show "σ^b * exp (- real (b⇧2) / (σ * m)) ≤ 1/(m choose b) * (σ * m gchoose b)"
using ‹b≤m› cardU_less_X ‹0 < σ› ‹0 < m gchoose b›
by (simp add: field_split_simps binomial_gbinomial)
qed auto
also have "… ≤ 1/(m choose b) * Φ"
unfolding mult.assoc
proof (intro mult_left_mono)
have eeq: "edge_card Blue U (X-U) = (∑i∈X-U. card (Neighbours Blue i ∩ U))"
proof (intro edge_card_eq_sum_Neighbours)
show "finite (X-U)"
by (meson ‹X⊆V› finV finite_Diff finite_subset)
qed (use disjnt_def Blue_E in auto)
have "(∑i∈X - U. card (Neighbours Blue i ∩ U)) / (real (card X) - m) = blue_density U (X-U) * m"
using ‹m>0› by (simp add: gen_density_def real_cardXU ‹card U = m› eeq divide_simps)
then have *: "(∑i∈X - U. real (card (Neighbours Blue i ∩ U)) /⇩R real (card (X-U))) = σ * m"
by (simp add: σ_def divide_inverse_commute real_cardXU flip: sum_distrib_left)
have "mbinomial (∑i∈X - U. real (card (Neighbours Blue i ∩ U)) /⇩R (card (X-U))) b
≤ (∑i∈X - U. inverse (real (card (X-U))) * mbinomial (card (Neighbours Blue i ∩ U)) b)"
proof (rule convex_on_sum)
show "finite (X-U)"
using cardU_less_X zero_less_diff by fastforce
show "convex_on UNIV (λa. mbinomial a b)"
by (simp add: ‹0 < b› convex_mbinomial)
show "(∑i∈X - U. inverse (card (X-U))) = 1"
using cardU_less_X cardXU by force
qed (use ‹U ⊂ X› in auto)
with ble
show "(σ*m gchoose b) * card (X-U) ≤ Φ"
unfolding * Φ_def
by (simp add: cardU_less_X cardXU binomial_gbinomial divide_simps flip: sum_distrib_left sum_divide_distrib)
qed auto
finally have 11: "μ^b / 2 * card X ≤ Φ / (m choose b)"
by simp
define Ω where "Ω ≡ nsets U b"
have cardΩ: "card Ω = m choose b"
by (simp add: Ω_def ‹card U = m›)
then have finΩ: "finite Ω" and "Ω ≠ {}" and "card Ω > 0"
using ‹b ≤ m› not_less by fastforce+
define M where "M ≡ uniform_count_measure Ω"
interpret P: prob_space M
using M_def ‹b ≤ m› cardΩ finΩ prob_space_uniform_count_measure by force
have measure_eq: "measure M C = (if C ⊆ Ω then card C / card Ω else 0)" for C
by (simp add: M_def finΩ measure_uniform_count_measure_if)
define Int_NB where "Int_NB ≡ λS. ⋂v∈S. Neighbours Blue v ∩ (X-U)"
have sum_card_NB: "(∑A∈Ω. card (⋂(Neighbours Blue ` A) ∩ Y))
= (∑v∈Y. card (Neighbours Blue v ∩ U) choose b)"
if "finite Y" "Y ⊆ X-U" for Y
using that
proof (induction Y)
case (insert y Y)
have *: "Ω ∩ {A. ∀x∈A. y ∈ Neighbours Blue x} = nsets (Neighbours Blue y ∩ U) b"
"Ω ∩ - {A. ∀x∈A. y ∈ Neighbours Blue x} = Ω - nsets (Neighbours Blue y ∩ U) b"
"[Neighbours Blue y ∩ U]⇗b⇖ ⊆ Ω"
using insert.prems by (auto simp: Ω_def nsets_def in_Neighbours_iff insert_commute)
then show ?case
using insert finΩ
by (simp add: Int_insert_right sum_Suc sum.If_cases if_distrib [of card]
sum.subset_diff flip: insert.IH)
qed auto
have "(∑x∈Ω. card (if x = {} then UNIV else ⋂ (Neighbours Blue ` x) ∩ (X-U)))
= (∑x∈Ω. card (⋂ (Neighbours Blue ` x) ∩ (X-U)))"
unfolding Ω_def nsets_def using ‹0 < b› by (force intro: sum.cong)
also have "… = (∑v∈X - U. card (Neighbours Blue v ∩ U) choose b)"
by (metis sum_card_NB ‹X⊆V› dual_order.refl finV finite_Diff rev_finite_subset)
finally have "sum (card o Int_NB) Ω = Φ"
by (simp add: Ω_def Φ_def Int_NB_def)
moreover
have "ennreal (P.expectation (λS. card (Int_NB S))) = sum (card o Int_NB) Ω / (card Ω)"
using integral_uniform_count_measure M_def finΩ by fastforce
ultimately have P: "P.expectation (λS. card (Int_NB S)) = Φ / (m choose b)"
by (metis Bochner_Integration.integral_nonneg cardΩ divide_nonneg_nonneg ennreal_inj of_nat_0_le_iff)
have False if "⋀S. S ∈ Ω ⟹ card (Int_NB S) < Φ / (m choose b)"
proof -
define L where "L ≡ (λS. Φ / real (m choose b) - card (Int_NB S)) ` Ω"
have "finite L" "L ≠ {}"
using L_def finΩ ‹Ω≠{}› by blast+
define ε where "ε ≡ Min L"
have "ε > 0"
using that finΩ ‹Ω ≠ {}› by (simp add: L_def ε_def)
then have "⋀S. S ∈ Ω ⟹ card (Int_NB S) ≤ Φ / (m choose b) - ε"
using Min_le [OF ‹finite L›] by (fastforce simp: algebra_simps ε_def L_def)
then have "P.expectation (λS. card (Int_NB S)) ≤ Φ / (m choose b) - ε"
using P P.not_empty not_integrable_integral_eq ‹ε > 0›
by (intro P.integral_le_const) (fastforce simp: M_def space_uniform_count_measure)+
then show False
using P ‹0 < ε› by auto
qed
then obtain S where "S ∈ Ω" and Sge: "card (Int_NB S) ≥ Φ / (m choose b)"
using linorder_not_le by blast
then have "S ⊆ U"
by (simp add: Ω_def nsets_def subset_iff)
have "card S = b" "clique S Blue"
using ‹S ∈ Ω› ‹U ⊆ V› ‹clique U Blue› smaller_clique
unfolding Ω_def nsets_def size_clique_def by auto
have "Φ / (m choose b) ≥ μ^b * card X / 2"
using 11 by simp
then have S: "card (Int_NB S) ≥ μ^b * card X / 2"
using Sge by linarith
obtain v where "v ∈ S"
using ‹0 < b› ‹card S = b› by fastforce
have "all_edges_betw_un S (S ∪ Int_NB S) ⊆ Blue"
using ‹clique S Blue›
unfolding all_edges_betw_un_def Neighbours_def clique_def Int_NB_def by fastforce
then have "good_blue_book X (S, Int_NB S)"
using ‹S⊆U› ‹v ∈ S› ‹U ⊂ X› S ‹card S = b›
unfolding good_blue_book_def book_def size_clique_def Int_NB_def disjnt_iff
by blast
then show ?thesis
by (metis ‹card S = b› b_def b_of_def of_nat_ceiling)
qed
text ‹Lemma 4.3›
proposition bblue_step_limit:
assumes big: "Big_Blue_4_1 μ l"
shows "card (Step_class {bblue_step}) ≤ l powr (3/4)"
proof -
define BBLUES where "BBLUES ≡ λr. {m. m < r ∧ stepper_kind m = bblue_step}"
have cardB_ge: "card (Bseq n) ≥ b_of l * card(BBLUES n)"
for n
proof (induction n)
case 0 then show ?case by (auto simp: BBLUES_def)
next
case (Suc n)
show ?case
proof (cases "stepper_kind n = bblue_step")
case True
have [simp]: "card (insert n (BBLUES n)) = Suc (card (BBLUES n))"
by (simp add: BBLUES_def)
have card_B': "card (Bseq (Suc n)) ≥ b_of l * card (BBLUES n)"
using Suc.IH
by (meson Bseq_Suc_subset card_mono finite_Bseq le_trans)
define S where "S ≡ fst (choose_blue_book (Xseq n, Yseq n, Aseq n, Bseq n))"
have BSuc: "Bseq (Suc n) = Bseq n ∪ S"
and manyb: "many_bluish (Xseq n)"
and cbb: "choose_blue_book (Xseq n, Yseq n, Aseq n, Bseq n) = (S, Xseq (Suc n))"
and same: "Aseq (Suc n) = Aseq n" "Yseq (Suc n) = Yseq n"
using True
by (force simp: S_def step_kind_defs next_state_def split: prod.split if_split_asm)+
have l14: "l powr (1/4) ≤ card S"
using Blue_4_1 [OF Xseq_subset_V manyb big]
by (smt (verit, best) choose_blue_book_works best_blue_book_is_best cbb finite_Xseq of_nat_mono)
then have ble: "b_of l ≤ card S"
using b_of_def nat_ceiling_le_eq by presburger
have S: "good_blue_book (Xseq n) (S, Xseq (Suc n))"
by (metis cbb choose_blue_book_works finite_Xseq)
then have "card S ≤ best_blue_book_card (Xseq n)"
by (simp add: best_blue_book_is_best finite_Xseq)
have finS: "finite S"
using ln0 l14 card.infinite by force
have "disjnt (Bseq n) (Xseq n)"
using valid_state_seq [of n]
by (auto simp: Bseq_def Xseq_def valid_state_def disjoint_state_def disjnt_iff split: prod.split_asm)
then have dBS: "disjnt (Bseq n) S"
using S cbb by (force simp: good_blue_book_def book_def disjnt_iff)
have eq: "BBLUES(Suc n) = insert n (BBLUES n)"
using less_Suc_eq True unfolding BBLUES_def by blast
then have "b_of l * card (BBLUES (Suc n)) = b_of l + b_of l * card (BBLUES n)"
by auto
also have "… ≤ card (Bseq n) + card S"
using ble card_B' Suc.IH by linarith
also have "… ≤ card (Bseq n ∪ S)"
using ble dBS by (simp add: card_Un_disjnt finS finite_Bseq)
finally have **: "b_of l * card (BBLUES (Suc n)) ≤ card (Bseq (Suc n))"
using order.trans BSuc by argo
then show ?thesis
by (simp add: BBLUES_def)
next
case False
then have "BBLUES(Suc n) = BBLUES n"
using less_Suc_eq by (auto simp: BBLUES_def)
then show ?thesis
by (metis Bseq_Suc_subset Suc.IH card_mono finite_Bseq le_trans)
qed
qed
{ assume §: "card (Step_class {bblue_step}) > l powr (3/4)"
then have fin: "finite (Step_class {bblue_step})"
using card.infinite by fastforce
then obtain n where n: "(Step_class {bblue_step}) = {m. m<n ∧ stepper_kind m = bblue_step}"
using Step_class_iterates by blast
with § have card_gt: "card{m. m<n ∧ stepper_kind m = bblue_step} > l powr (3/4)"
by (simp add: n)
have "l = l powr (1/4) * l powr (3/4)"
by (simp flip: powr_add)
also have "… ≤ b_of l * l powr (3/4)"
by (simp add: b_of_def mult_mono')
also have "… ≤ b_of l * card{m. m<n ∧ stepper_kind m = bblue_step}"
using card_gt less_eq_real_def by fastforce
also have "… ≤ card (Bseq n)"
using cardB_ge step of_nat_mono unfolding BBLUES_def by blast
also have "… < l"
by (simp add: Bseq_less_l)
finally have False
by simp
}
then show ?thesis by force
qed
lemma red_steps_eq_A:
defines "REDS ≡ λr. {i. i < r ∧ stepper_kind i = red_step}"
shows "card(REDS n) = card (Aseq n)"
proof (induction n)
case 0
then show ?case
by (auto simp: REDS_def)
next
case (Suc n)
show ?case
proof (cases "stepper_kind n = red_step")
case True
then have [simp]: "REDS (Suc n) = insert n (REDS n)" "card (insert n (REDS n)) = Suc (card (REDS n))"
by (auto simp: REDS_def)
have Aeq: "Aseq (Suc n) = insert (choose_central_vx (Xseq n,Yseq n,Aseq n,Bseq n)) (Aseq n)"
using Suc.prems True
by (auto simp: step_kind_defs next_state_def split: if_split_asm prod.split)
have "finite (Xseq n)"
using finite_Xseq by presburger
then have "choose_central_vx (Xseq n,Yseq n,Aseq n,Bseq n) ∈ Xseq n"
using True
by (simp add: step_kind_defs choose_central_vx_X split: if_split_asm prod.split_asm)
moreover have "disjnt (Xseq n) (Aseq n)"
using valid_state_seq by (simp add: valid_state_def disjoint_state_def)
ultimately have "choose_central_vx (Xseq n,Yseq n,Aseq n,Bseq n) ∉ Aseq n"
by (simp add: disjnt_iff)
then show ?thesis
by (simp add: Aeq Suc.IH finite_Aseq)
next
case False
then have "REDS(Suc n) = REDS n"
using less_Suc_eq unfolding REDS_def by blast
moreover have "Aseq (Suc n) = Aseq n"
using False
by (auto simp: step_kind_defs degree_reg_def next_state_def split: prod.split)
ultimately show ?thesis
using Suc.IH by presburger
qed
qed
proposition red_step_eq_Aseq: "card (Step_class {red_step}) = card (Aseq halted_point)"
proof -
have "card{i. i < halted_point ∧ stepper_kind i = red_step} = card (Aseq halted_point)"
by (rule red_steps_eq_A)
moreover have "(Step_class {red_step}) = {i. i < halted_point ∧ stepper_kind i = red_step}"
using halted_point_minimal' by (fastforce simp: Step_class_def)
ultimately show ?thesis
by argo
qed
proposition red_step_limit: "card (Step_class {red_step}) < k"
using Aseq_less_k red_step_eq_Aseq by presburger
proposition bblue_dboost_step_limit:
assumes big: "Big_Blue_4_1 μ l"
shows "card (Step_class {bblue_step}) + card (Step_class {dboost_step}) < l"
proof -
define BDB where "BDB ≡ λr. {i. i < r ∧ stepper_kind i ∈ {bblue_step,dboost_step}}"
have *: "card(BDB n) ≤ card B"
if "stepper n = (X,Y,A,B)" for n X Y A B
using that
proof (induction n arbitrary: X Y A B)
case 0
then show ?case
by (auto simp: BDB_def)
next
case (Suc n)
obtain X' Y' A' B' where step_n: "stepper n = (X',Y',A',B')"
by (metis surj_pair)
then obtain "valid_state (X',Y',A',B')" and "V_state (X',Y',A',B')"
and disjst: "disjoint_state(X',Y',A',B')" and "finite X'"
by (metis finX valid_state_def valid_state_stepper)
have "B' ⊆ B"
using Suc.prems by (auto simp: next_state_def Let_def degree_reg_def step_n split: prod.split_asm if_split_asm)
show ?case
proof (cases "stepper_kind n ∈ {bblue_step,dboost_step}")
case True
then have "BDB (Suc n) = insert n (BDB n)"
by (auto simp: BDB_def)
moreover have "card (insert n (BDB n)) = Suc (card (BDB n))"
by (simp add: BDB_def)
ultimately have card_Suc[simp]: "card (BDB (Suc n)) = Suc (card (BDB n))"
by presburger
have card_B': "card (BDB n) ≤ card B'"
using step_n BDB_def Suc.IH by blast
consider "stepper_kind n = bblue_step" | "stepper_kind n = dboost_step"
using True by force
then have Bigger: "B' ⊂ B"
proof cases
case 1
then have "¬ termination_condition X' Y'"
by (auto simp: stepper_kind_def step_n)
with 1 obtain S where "A' = A" "Y' = Y" and manyb: "many_bluish X'"
and cbb: "choose_blue_book (X',Y,A,B') = (S,X)" and le_cardB: "B = B' ∪ S"
using Suc.prems
by (auto simp: step_kind_defs next_state_def step_n split: prod.split_asm if_split_asm)
then obtain "X' ⊆ V" "finite X'"
using Xseq_subset_V ‹finite X'› step_n stepper_XYseq by blast
then have "l powr (1/4) ≤ real (card S)"
using Blue_4_1 [OF _ manyb big]
by (smt (verit, best) of_nat_mono best_blue_book_is_best cbb choose_blue_book_works)
then have "S ≠ {}"
using ln0 by fastforce
moreover have "disjnt B' S"
using choose_blue_book_subset [OF ‹finite X'›] disjst cbb
unfolding disjoint_state_def
by (smt (verit) in_mono ‹A' = A› ‹Y' = Y› disjnt_iff old.prod.case)
ultimately show ?thesis
by (metis ‹B' ⊆ B› disjnt_Un1 disjnt_self_iff_empty le_cardB psubsetI)
next
case 2
then have "choose_central_vx (X',Y',A',B') ∈ X'"
unfolding step_kind_defs
by (auto simp: ‹finite X'› choose_central_vx_X step_n split: if_split_asm)
moreover have "disjnt B' X'"
using disjst disjnt_sym by (force simp: disjoint_state_def)
ultimately have "choose_central_vx (X',Y',A',B') ∉ B'"
by (meson disjnt_iff)
then show ?thesis
using 2 Suc.prems
by (auto simp: step_kind_defs next_state_def step_n split: if_split_asm)
qed
moreover have "finite B"
by (metis Suc.prems V_state_stepper finB)
ultimately show ?thesis
by (metis card_B' card_Suc card_seteq le_trans not_less_eq_eq psubset_eq)
next
case False
then have "BDB (Suc n) = BDB n"
using less_Suc_eq unfolding BDB_def by blast
with ‹B' ⊆ B› Suc show ?thesis
by (metis V_state_stepper card_mono finB le_trans step_n)
qed
qed
have less_l: "card (BDB n) < l" for n
by (meson card_B_limit * order.trans linorder_not_le prod_cases4)
moreover have fin: "⋀n. finite (BDB n)" "incseq BDB"
by (auto simp: BDB_def incseq_def)
ultimately have **: "∀⇧∞n. ⋃ (range BDB) = BDB n"
using Union_incseq_finite by blast
then have "finite (⋃ (range BDB))"
using BDB_def eventually_sequentially by force
moreover have Uneq: "⋃ (range BDB) = Step_class {bblue_step,dboost_step}"
by (auto simp: Step_class_def BDB_def)
ultimately have fin: "finite (Step_class {bblue_step,dboost_step})"
by fastforce
obtain n where "⋃ (range BDB) = BDB n"
using ** by force
then have "card (BDB n) = card (Step_class {bblue_step} ∪ Step_class {dboost_step})"
by (metis Step_class_insert Uneq)
also have "… = card (Step_class {bblue_step}) + card (Step_class {dboost_step})"
by (simp add: card_Un_disjnt disjnt_Step_class)
finally show ?thesis
by (metis less_l)
qed
end
end