Theory Closer_To_Diagonal
section ‹An exponential improvement closer to the diagonal›
theory Closer_To_Diagonal
imports Far_From_Diagonal
begin
subsection ‹Lemma 10.2›
context P0_min
begin
lemma error_10_2:
assumes "μ / real d > 1/200"
shows "∀⇧∞k. ok_fun_95b k + μ * real k / real d ≥ k/200"
proof -
have "d>0" "μ>0"
using assms by (auto simp: divide_simps split: if_split_asm)
then have *: "real k ≤ μ * (real k * 200) / real d" for k
using assms by (fastforce simp: divide_simps less_eq_real_def)
have "∀⇧∞k. ¦ok_fun_95b k¦ ≤ (μ/d - 1/200) * k"
using ok_fun_95b assms unfolding smallo_def
by (auto dest!: spec [where x = "μ/d"])
then show ?thesis
apply eventually_elim
using assms ‹d>0› *
by (simp add: algebra_simps not_less abs_if add_increasing split: if_split_asm)
qed
text ‹The "sufficiently large" assumptions are problematical.
The proof's calculation for @{term "γ > 3/20"} is sharp.
We need a finite gap for the limit to exist. We can get away with 1/300.›
definition x320::real where "x320 ≡ 3/20 + 1/300"
lemma error_10_2_True: "∀⇧∞k. ok_fun_95b k + x320 * real k / real 30 ≥ k/200"
unfolding x320_def
by (intro error_10_2) auto
lemma error_10_2_False: "∀⇧∞k. ok_fun_95b k + (1/10) * real k / real 15 ≥ k/200"
by (intro error_10_2) auto
definition "Big_Closer_10_2 ≡ λμ l. Big_Far_9_3 μ l ∧ Big_Far_9_5 μ l
∧ (∀k≥l. ok_fun_95b k + (if μ > x320 then μ*k/30 else μ*k/15) ≥ k/200)"
lemma Big_Closer_10_2:
assumes "1/10≤μ1" "μ1<1"
shows "∀⇧∞l. ∀μ. 1/10 ≤ μ ∧ μ ≤ μ1 ⟶ Big_Closer_10_2 μ l"
proof -
have T: "∀⇧∞l. ∀k≥l. (∀μ. x320 ≤ μ ∧ μ ≤ μ1 ⟶ k/200 ≤ ok_fun_95b k + μ*k / real 30)"
using assms
apply (intro eventually_all_ge_at_top eventually_all_geI0 error_10_2_True)
apply (auto simp: mult_right_mono elim!: order_trans)
done
have F: "∀⇧∞l. ∀k≥l. (∀μ. 1/10 ≤ μ ∧ μ ≤ μ1 ⟶ k/200 ≤ ok_fun_95b k + μ*k / real 15)"
using assms
apply (intro eventually_all_ge_at_top eventually_all_geI0 error_10_2_False)
by (smt (verit, ccfv_SIG) divide_right_mono mult_right_mono of_nat_0_le_iff)
have "∀⇧∞l. ∀k≥l. (∀μ. 1/10 ≤ μ ∧ μ ≤ μ1 ⟶ k/200 ≤ ok_fun_95b k + (if μ > x320 then μ*k/30 else μ*k/15))"
using assms
apply (split if_split)
unfolding eventually_conj_iff all_imp_conj_distrib all_conj_distrib
by (force intro: eventually_mono [OF T] eventually_mono [OF F])
then show ?thesis
using assms Big_Far_9_3[of "1/10"] Big_Far_9_5[of "1/10"]
unfolding Big_Closer_10_2_def eventually_conj_iff all_imp_conj_distrib
by (force simp: elim!: eventually_mono)
qed
end
text ‹A little tricky to express since the Book locale assumes that
there are no cliques in the original graph (page 10). So it's a contrapositive›
lemma (in Book') Closer_10_2_aux:
assumes 0: "real (card X0) ≥ nV/2" "card Y0 ≥ nV div 2" "p0 ≥ 1-γ"
assumes γ: "1/10 ≤ γ" "γ ≤ 1/5"
assumes nV: "real nV ≥ exp (-k/200) * (k+l choose l)"
assumes big: "Big_Closer_10_2 γ l"
shows False
proof -
define ℛ where "ℛ ≡ Step_class {red_step}"
define t where "t ≡ card ℛ"
define δ::real where "δ ≡ 1/200"
have γ01: "0 < γ" "γ < 1"
using ln0 l_le_k by (auto simp: γ_def)
have "t<k"
unfolding t_def ℛ_def using γ01 red_step_limit by blast
have big93: "Big_Far_9_3 γ l"
using big by (auto simp: Big_Closer_10_2_def Big_Far_9_2_def)
have t23: "t ≥ 2*k / 3"
unfolding t_def ℛ_def
proof (rule Far_9_3)
have "min (1/200) (l / (real k + real l) / 20) = 1/200"
using γ ln0 by (simp add: γ_def)
then show "exp (- min (1/200) (γ / 20) * real k) * real (k+l choose l) ≤ nV"
using nV divide_real_def inverse_eq_divide minus_mult_right mult.commute γ_def
by (metis of_int_of_nat_eq of_int_minus)
show "1/4 ≤ p0"
using γ 0 by linarith
show "Big_Far_9_3 γ l"
using γ_def big93 by blast
qed (use assms γ_def in auto)
have "card (Yseq halted_point) ≥
exp (-δ * k + ok_fun_95b k) * (1-γ) powr (γ*t / (1-γ)) * ((1-γ)/(1-γ))^t
* exp (γ * (real t)⇧2 / (2*k)) * (k-t+l choose l)"
proof (rule order_trans [OF _ Far_9_5])
show "exp (-δ * k) * real (k+l choose l) ≤ real nV"
using nV by (auto simp: δ_def)
show "1/2 ≤ 1 - γ - 0"
using divide_le_eq_1 l_le_k γ_def by fastforce
next
show "Big_Far_9_5 γ l"
using big by (simp add: Big_Closer_10_2_def Big_Far_9_2_def γ_def)
qed (use 0 kn0 in ‹auto simp flip: t_def γ_def ℛ_def›)
then have 52: "card (Yseq halted_point) ≥
exp (-δ * k + ok_fun_95b k) * (1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) * (k-t+l choose l)"
using γ by simp
define gamf where "gamf ≡ λx::real. (1-x) powr (1/(1-x))"
have deriv_gamf: "∃y. DERIV gamf x :> y ∧ y ≤ 0" if "0<a" "a≤x" "x≤b" "b<1" for a b x
unfolding gamf_def
using that ln_less_self[of "1-x"]
by (force intro!: DERIV_powr derivative_eq_intros simp: divide_simps mult_le_0_iff simp del: ln_less_self)
have "(1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) ≥ exp (δ*k - ok_fun_95b k)"
proof (cases "γ > x320")
case True
then have "ok_fun_95b k + γ*k / 30 ≥ k/200"
using big l_le_k by (auto simp: Big_Closer_10_2_def Big_Far_9_2_def)
with True kn0 have "δ * k - ok_fun_95b k ≤ (γ/30) * k"
by (simp add: δ_def)
also have "… ≤ 3 * γ * (real t)⇧2 / (40*k)"
using True mult_right_mono [OF mult_mono [OF t23 t23], of "3*γ / (40*k)"] ‹k>0›
by (simp add: power2_eq_square x320_def)
finally have †: "δ*k - ok_fun_95b k ≤ 3 * γ * (real t)⇧2 / (40*k)" .
have "gamf γ ≥ gamf (1/5)"
by (smt (verit, best) DERIV_nonpos_imp_nonincreasing[of γ "1/5" gamf] γ γ01 deriv_gamf divide_less_eq_1)
moreover have "ln (gamf (1/5)) ≥ -1/3 + 1/20"
unfolding gamf_def by (approximation 10)
moreover have "gamf (1/5) > 0"
by (simp add: gamf_def)
ultimately have "gamf γ ≥ exp (-1/3 + 1/20)"
using ln_ge_iff by auto
from powr_mono2 [OF _ _ this]
have "(1-γ) powr (γ*t / (1-γ)) ≥ exp (-17/60) powr (γ*t)"
unfolding gamf_def using γ01 powr_powr by fastforce
from mult_left_mono [OF this, of "exp (γ * (real t)⇧2 / (2*k))"]
have "(1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) ≥ exp (-17/60 * (γ*t) + (γ * (real t)⇧2 / (2*k)))"
by (smt (verit) mult.commute exp_add exp_ge_zero exp_powr_real)
moreover have "(-17/60 * (γ*t) + (γ * (real t)⇧2 / (2*k))) ≥ (3*γ * (real t)⇧2 / (40*k))"
using t23 ‹k>0› ‹γ>0› by (simp add: divide_simps eval_nat_numeral)
ultimately have "(1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) ≥ exp (3*γ * (real t)⇧2 / (40*k))"
by (smt (verit) exp_mono)
with † show ?thesis
by (smt (verit, best) exp_le_cancel_iff)
next
case False
then have "ok_fun_95b k + γ*k/15 ≥ k/200"
using big l_le_k by (auto simp: Big_Closer_10_2_def Big_Far_9_2_def)
with kn0 have "δ * k - ok_fun_95b k ≤ (γ/15) * k"
by (simp add: δ_def x320_def)
also have "… ≤ 3 * γ * (real t)⇧2 / (20*k)"
using γ mult_right_mono [OF mult_mono [OF t23 t23], of "3*γ / (40*k)"] kn0
by (simp add: power2_eq_square field_simps)
finally have †: "δ*k - ok_fun_95b k ≤ 3 * γ * (real t)⇧2 / (20*k)" .
have "gamf γ ≥ gamf x320"
using False γ
by (intro DERIV_nonpos_imp_nonincreasing[of γ "x320" gamf] deriv_gamf)
(auto simp: x320_def)
moreover have "ln (gamf x320) ≥ -1/3 + 1/10"
unfolding gamf_def x320_def by (approximation 6)
moreover have "gamf x320 > 0"
by (simp add: gamf_def x320_def)
ultimately have "gamf γ ≥ exp (-1/3 + 1/10)"
using ln_ge_iff by auto
from powr_mono2 [OF _ _ this]
have "(1-γ) powr (γ*t / (1-γ)) ≥ exp (-7/30) powr (γ*t)"
unfolding gamf_def using γ01 powr_powr by fastforce
from mult_left_mono [OF this, of "exp (γ * (real t)⇧2 / (2*k))"]
have "(1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) ≥ exp (-7/30 * (γ*t) + (γ * (real t)⇧2 / (2*k)))"
by (smt (verit) mult.commute exp_add exp_ge_zero exp_powr_real)
moreover have "(-7/30 * (γ*t) + (γ * (real t)⇧2 / (2*k))) ≥ (3*γ * (real t)⇧2 / (20*k))"
using t23 ‹k>0› ‹γ>0› by (simp add: divide_simps eval_nat_numeral)
ultimately have "(1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) ≥ exp (3*γ * (real t)⇧2 / (20*k))"
by (smt (verit) exp_mono)
with † show ?thesis
by (smt (verit, best) exp_le_cancel_iff)
qed
then have "1 ≤ exp (-δ*k + ok_fun_95b k) * (1-γ) powr (γ * t / (1-γ)) * exp (γ * (real t)⇧2 / (2 * k))"
by (simp add: exp_add exp_diff mult_ac pos_divide_le_eq)
then have "(k-t+l choose l) ≤
exp (-δ * k + ok_fun_95b k) * (1-γ) powr (γ*t / (1-γ)) * exp (γ * (real t)⇧2 / (2*k)) * (k-t+l choose l)"
by auto
with 52 have "(k-t+l choose l) ≤ card (Yseq halted_point)" by linarith
then show False
using Far_9_2_conclusion by (simp flip: ℛ_def t_def)
qed
text ‹Material that needs to be proved \textbf{outside} the book locales›
lemma (in No_Cliques) Closer_10_2:
fixes γ::real
defines "γ ≡ l / (real k + real l)"
assumes nV: "real nV ≥ exp (- real k/200) * (k+l choose l)"
assumes gd: "graph_density Red ≥ 1-γ" and p0_min_OK: "p0_min ≤ 1-γ"
assumes big: "Big_Closer_10_2 γ l" and "l≤k"
assumes γ: "1/10 ≤ γ" "γ ≤ 1/5"
shows False
proof -
obtain X0 Y0 where "l≥2" and card_X0: "card X0 ≥ nV/2"
and card_Y0: "card Y0 = gorder div 2"
and X0_def: "X0 = V ∖ Y0" and "Y0⊆V"
and gd_le: "graph_density Red ≤ gen_density Red X0 Y0"
and "Book' V E p0_min Red Blue l k γ X0 Y0"
using Basis_imp_Book' assms order.trans ln0 by blast
then interpret Book' V E p0_min Red Blue l k γ X0 Y0
by blast
show False
proof (intro Closer_10_2_aux)
show "1 - γ≤ p0"
using X0_def γ_def gd gd_le gen_density_commute p0_def by auto
qed (use assms card_X0 card_Y0 in auto)
qed
subsection ‹Theorem 10.1›
context P0_min
begin
definition "Big101a ≡ λk. 2 + real k / 2 ≤ exp (of_int⌊k/10⌋ * 2 - k/200)"
definition "Big101b ≡ λk. (real k)⇧2 - 10 * real k > (k/10) * real(10 + 9*k)"
text ‹The proof considers a smaller graph, so @{term l} needs to be so big
that the smaller @{term l'} will be big enough.›
definition "Big101c ≡ λγ0 l. ∀l' γ. l' ≥ nat ⌊2/5 * l⌋ ⟶ γ0 ≤ γ ⟶ γ ≤ 1/10 ⟶ Big_Far_9_1 γ l'"
definition "Big101d ≡ λl. (∀l' γ. l' ≥ nat ⌊2/5 * l⌋ ⟶ 1/10 ≤ γ ⟶ γ ≤ 1/5 ⟶ Big_Closer_10_2 γ l')"
definition "Big_Closer_10_1 ≡ λγ0 l. l≥9 ∧ (∀k≥l. Big101c γ0 k ∧ Big101d k ∧ Big101a k ∧ Big101b k)"
lemma Big_Closer_10_1_upward: "⟦Big_Closer_10_1 γ0 l; l ≤ k; γ0 ≤ γ⟧ ⟹ Big_Closer_10_1 γ k"
unfolding Big_Closer_10_1_def Big101c_def by (meson order.trans)
text ‹The need for $\gamma0$ is unfortunate, but it seems simpler to hide
the precise value of this term in the main proof.›
lemma Big_Closer_10_1:
fixes γ0::real
assumes "γ0>0"
shows "∀⇧∞l. Big_Closer_10_1 γ0 l"
proof -
have a: "∀⇧∞k. Big101a k"
unfolding Big101a_def by real_asymp
have b: "∀⇧∞k. Big101b k"
unfolding Big101b_def by real_asymp
have c: "∀⇧∞l. Big101c γ0 l"
proof -
have "∀⇧∞l. ∀γ. γ0 ≤ γ ∧ γ ≤ 1/10 ⟶ Big_Far_9_1 γ l"
using Big_Far_9_1 ‹γ0>0› eventually_sequentially order.trans by blast
then obtain N where N: "∀l≥N. ∀γ. γ0 ≤ γ ∧ γ ≤ 1/10 ⟶ Big_Far_9_1 γ l"
using eventually_sequentially by auto
define M where "M ≡ nat⌈5*N / 2⌉"
have "nat⌊(2/5) * l⌋ ≥ N" if "l ≥ M" for l
using that assms by (simp add: M_def le_nat_floor)
with N have "∀l≥M. ∀l' γ. nat⌊(2/5) * l⌋ ≤ l' ⟶ γ0 ≤ γ ∧ γ ≤ 1/10 ⟶ Big_Far_9_1 γ l'"
by (meson order.trans)
then show ?thesis
by (auto simp: Big101c_def eventually_sequentially)
qed
have d: "∀⇧∞l. Big101d l"
proof -
have "∀⇧∞l. ∀γ. 1/10 ≤ γ ∧ γ ≤ 1/5 ⟶ Big_Closer_10_2 γ l"
using assms Big_Closer_10_2 [of "1/5"] by linarith
then obtain N where N: "∀l≥N. ∀γ. 1/10 ≤ γ ∧ γ ≤ 1/5 ⟶ Big_Closer_10_2 γ l"
using eventually_sequentially by auto
define M where "M ≡ nat⌈5*N / 2⌉"
have "nat⌊(2/5) * l⌋ ≥ N" if "l ≥ M" for l
using that assms by (simp add: M_def le_nat_floor)
with N have "∀l≥M. ∀l' γ. l' ≥ nat ⌊2/5 * l⌋ ⟶ 1/10 ≤ γ ∧ γ ≤ 1/5 ⟶ Big_Closer_10_2 γ l'"
by (smt (verit, ccfv_SIG) of_nat_le_iff)
then show ?thesis
by (auto simp: eventually_sequentially Big101d_def)
qed
show ?thesis
using a b c d eventually_all_ge_at_top eventually_ge_at_top
unfolding Big_Closer_10_1_def eventually_conj_iff all_imp_conj_distrib
by blast
qed
text ‹The strange constant @{term γ0} is needed for the case where we consider a subgraph;
see near the end of this proof›
theorem Closer_10_1:
fixes l k::nat
fixes δ γ::real
defines "γ ≡ real l / (real k + real l)"
defines "δ ≡ γ/40"
defines "γ0 ≡ min γ (0.07)"
assumes big: "Big_Closer_10_1 γ0 l"
assumes γ: "γ ≤ 1/5"
assumes p0_min_101: "p0_min ≤ 1 - 1/5"
shows "RN k l ≤ exp (-δ*k + 3) * (k+l choose l)"
proof (rule ccontr)
assume non: "¬ RN k l ≤ exp (-δ*k + 3) * (k+l choose l)"
have "l≤k"
using γ_def γ nat_le_real_less by fastforce
moreover have "l≥9"
using big by (simp add: Big_Closer_10_1_def)
ultimately have "l>0" "k>0" "l≥3" by linarith+
then have l4k: "4*l ≤ k"
using γ by (auto simp: γ_def divide_simps)
have "k≥36"
using ‹l≥9› l4k by linarith
have exp_gt21: "exp (x + 2) > exp (x + 1)" for x::real
by auto
have exp2: "exp (2::real) = exp 1 * exp 1"
by (simp add: mult_exp_exp)
have Big91_I:"⋀l' μ. ⟦l' ≥ nat ⌊2/5 * l⌋; γ0 ≤ μ; μ ≤ 1/10⟧ ⟹ Big_Far_9_1 μ l'"
using big by (meson Big101c_def Big_Closer_10_1_def order.refl)
show False
proof (cases "γ ≤ 1/10")
case True
have "γ>0"
using ‹0 < l› γ_def by auto
have "RN k l ≤ exp (-δ*k + 1) * (k+l choose l)"
proof (intro order.trans [OF Far_9_1] strip)
show "Big_Far_9_1 (l / (real k + real l)) l"
proof (intro Big91_I)
show "l ≥ nat ⌊2/5 * l⌋"
by linarith
qed (use True γ0_def γ_def in auto)
next
show "exp (- (l / (k + real l) / 20) * k + 1) * (k+l choose l) ≤ exp (-δ*k + 1) * (k+l choose l)"
by (smt (verit, best) ‹0 < γ› γ_def δ_def exp_mono frac_le mult_right_mono of_nat_0_le_iff)
qed (use ‹l≥9› p0_min_101 True γ_def in auto)
then show False
using non exp_gt21 by (smt (verit, ccfv_SIG) mult_right_mono of_nat_0_le_iff)
next
case False
with ‹l>0› have "γ>0" "γ>1/10" and k9l: "k < 9*l"
by (auto simp: γ_def)
define U_lower_bound_ratio where
"U_lower_bound_ratio ≡ λm. (∏i<m. (l - real i) / (k+l - real i))"
define n where "n ≡ nat⌈RN k l - 1⌉"
have "k≥12"
using l4k ‹l≥3› by linarith
have "exp 1 / (exp 1 - 2) < (12::real)"
by (approximation 5)
also have RN12: "… ≤ RN k l"
by (meson RN_3plus' ‹l≥3› ‹k≥12› le_trans numeral_le_real_of_nat_iff)
finally have "exp 1 / (exp 1 - 2) < RN k l" .
moreover have "n < RN k l"
using RN12 by (simp add: n_def)
moreover have "2 < exp (1::real)"
by (approximation 5)
ultimately have nRNe: "n/2 > RN k l / exp 1"
by (simp add: n_def field_split_simps)
have "(k+l choose l) / exp (-3 + δ*k) < RN k l"
by (smt (verit) divide_inverse exp_minus mult_minus_left mult_of_nat_commute non)
then have "(k+l choose l) < (RN k l / exp 2) * exp (δ*k - 1)"
by (simp add: divide_simps exp_add exp_diff flip: exp_add)
also have "… ≤ (n/2) * exp (δ*k - 2)"
using nRNe by (simp add: divide_simps exp_diff)
finally have n2exp_gt': "(n/2) * exp (δ*k) > (k+l choose l) * exp 2"
by (metis exp_diff exp_gt_zero linorder_not_le pos_divide_le_eq times_divide_eq_right)
then have n2exp_gt: "(n/2) * exp (δ*k) > (k+l choose l)"
by (smt (verit, best) mult_le_cancel_left1 of_nat_0_le_iff one_le_exp_iff)
then have nexp_gt: "n * exp (δ*k) > (k+l choose l)"
using less_le_trans linorder_not_le by force
define V where "V ≡ {..<n}"
define E where "E ≡ all_edges V"
interpret Book_Basis V E
proof qed (auto simp: V_def E_def comp_sgraph.wellformed comp_sgraph.two_edges)
have [simp]: "nV = n"
by (simp add: V_def)
then obtain Red Blue
where Red_E: "Red ⊆ E" and Blue_def: "Blue = E-Red"
and no_Red_K: "¬ (∃K. size_clique k K Red)"
and no_Blue_K: "¬ (∃K. size_clique l K Blue)"
by (metis ‹n < RN k l› less_RN_Red_Blue)
have Blue_E: "Blue ⊆ E" and disjnt_Red_Blue: "disjnt Red Blue" and Blue_eq: "Blue = all_edges V - Red"
using complete by (auto simp: Blue_def disjnt_iff E_def)
define is_good_clique where
"is_good_clique ≡ λi K. clique K Blue ∧ K ⊆ V
∧ card (V ∩ (⋂w∈K. Neighbours Blue w))
≥ i * U_lower_bound_ratio (card K) - card K"
have is_good_card: "card K < l" if "is_good_clique i K" for i K
using no_Blue_K that unfolding is_good_clique_def
by (metis nat_neq_iff size_clique_def size_clique_smaller)
define max_m where "max_m ≡ Suc (nat ⌊l - k/9⌋)"
define GC where "GC ≡ {C. is_good_clique n C ∧ card C ≤ max_m}"
have maxm_bounds: "l - k/9 ≤ max_m" "max_m ≤ l+1 - k/9" "max_m > 0"
using k9l unfolding max_m_def by linarith+
then have "GC ≠ {}"
by (auto simp: GC_def is_good_clique_def U_lower_bound_ratio_def E_def V_def intro: exI [where x="{}"])
have "GC ⊆ Pow V"
by (auto simp: is_good_clique_def GC_def)
then have "finite GC"
by (simp add: finV finite_subset)
then obtain W where "W ∈ GC" and MaxW: "Max (card ` GC) = card W"
using ‹GC ≠ {}› obtains_MAX by blast
then have 53: "is_good_clique n W"
using GC_def by blast
then have "W⊆V"
by (auto simp: is_good_clique_def)
define m where "m ≡ card W"
define γ' where "γ' ≡ (l - real m) / (k+l-real m)"
have max53: "¬ (is_good_clique n (insert x W) ∧ card (insert x W) ≤ max_m)" if "x∈V∖W" for x
proof
assume x: "is_good_clique n (insert x W) ∧ card (insert x W) ≤ max_m"
then have "card (insert x W) = Suc (card W)"
using finV is_good_clique_def finite_subset that by fastforce
with x ‹finite GC› have "Max (card ` GC) ≥ Suc (card W)"
by (metis (no_types, lifting) GC_def Max_ge finite_imageI image_iff mem_Collect_eq)
then show False
by (simp add: MaxW)
qed
then have clique_cases: "m < max_m ∧ (∀x∈V∖W. ¬ is_good_clique n (insert x W)) ∨ m = max_m"
using GC_def ‹W ∈ GC› ‹W ⊆ V› finV finite_subset m_def by fastforce
have Red_Blue_RN: "∃K ⊆ X. size_clique m K Red ∨ size_clique n K Blue"
if "card X ≥ RN m n" "X⊆V" for m n and X
using partn_lst_imp_is_clique_RN [OF is_Ramsey_number_RN [of m n]] finV that
unfolding is_clique_RN_def size_clique_def clique_indep_def Blue_eq
by (metis clique_iff_indep finite_subset subset_trans)
define U where "U ≡ V ∩ (⋂w∈W. Neighbours Blue w)"
have "RN k l > 0"
by (metis RN_eq_0_iff gr0I ‹k>0› ‹l>0›)
with ‹n < RN k l› have n_less: "n < (k+l choose l)"
by (metis add.commute RN_commute RN_le_choose le_trans linorder_not_less)
have "γ' > 0"
using is_good_card [OF 53] by (simp add: γ'_def m_def)
have "finite W"
using ‹W ⊆ V› finV finite_subset by (auto simp: V_def)
have "U ⊆ V"
by (force simp: U_def)
then have VUU: "V ∩ U = U"
by blast
have "disjnt U W"
using Blue_E not_own_Neighbour unfolding E_def V_def U_def disjnt_iff by blast
have "m<l"
using 53 is_good_card m_def by blast
have "γ' ≤ 1"
using ‹m<l› by (simp add: γ'_def divide_simps)
have cardU: "n * U_lower_bound_ratio m ≤ m + card U"
using 53 VUU unfolding is_good_clique_def m_def U_def by force
have clique_W: "size_clique m W Blue"
using 53 is_good_clique_def m_def size_clique_def V_def by blast
have prod_gt0: "U_lower_bound_ratio m > 0"
unfolding U_lower_bound_ratio_def using ‹m<l› by (intro prod_pos) auto
have kl_choose: "real(k+l choose l) = (k+l-m choose (l-m)) / U_lower_bound_ratio m"
unfolding U_lower_bound_ratio_def using kl_choose ‹0 < k› ‹m < l› by blast
have extend_Blue_clique: "∃K'. size_clique l K' Blue"
if "K ⊆ U" "size_clique (l-m) K Blue" for K
proof -
have K: "card K = l-m" "clique K Blue"
using that by (auto simp: size_clique_def)
define K' where "K' ≡ K ∪ W"
have "card K' = l"
unfolding K'_def
proof (subst card_Un_disjnt)
show "finite K" "finite W"
using finV ‹K ⊆ U› ‹U⊆V› finite_subset ‹finite W› that by meson+
show "disjnt K W"
using ‹disjnt U W› ‹K ⊆ U› disjnt_subset1 by blast
show "card K + card W = l"
using K ‹m < l› m_def by auto
qed
moreover have "clique K' Blue"
using ‹clique K Blue› clique_W ‹K ⊆ U›
unfolding K'_def size_clique_def U_def
by (force simp: in_Neighbours_iff insert_commute intro: Ramsey.clique_Un)
ultimately show ?thesis
unfolding K'_def size_clique_def using ‹K ⊆ U› ‹U ⊆ V› ‹W ⊆ V› by auto
qed
have "γ' ≤ γ"
using ‹m<l› by (simp add: γ_def γ'_def field_simps)
consider "m < max_m" | "m = max_m"
using clique_cases by blast
then consider "m < max_m" "γ' ≥ 1/10" | "1/10 - 1/k ≤ γ' ∧ γ' ≤ 1/10"
proof cases
case 1
then have "γ' ≥ 1/10"
using ‹γ>1/10› ‹k>0› maxm_bounds by (auto simp: γ_def γ'_def)
with 1 that show thesis by blast
next
case 2
then have γ'_le110: "γ' ≤ 1/10"
using ‹γ>1/10› ‹k>0› maxm_bounds by (auto simp: γ_def γ'_def)
have "1/10 - 1/k ≤ γ'"
proof -
have §: "l-m ≥ k/9 - 1"
using ‹γ>1/10› ‹k>0› 2 by (simp add: max_m_def γ_def) linarith
have "1/10 - 1/k ≤ 1 - k / (10*k/9 - 1)"
using γ'_le110 ‹m<l› ‹k>0› by (simp add: γ'_def field_simps)
also have "… ≤ 1 - k / (k + l - m)"
using ‹l≤k› ‹m<l› § by (simp add: divide_left_mono)
also have "… = γ'"
using ‹l>0› ‹l≤k› ‹m<l› ‹k>0› by (simp add: γ'_def divide_simps)
finally show "1/10 - 1 / real k ≤ γ'" .
qed
with γ'_le110 that show thesis
by linarith
qed
note γ'_cases = this
have 110: "1/10 - 1/k ≤ γ'"
using γ'_cases by (smt (verit, best) divide_nonneg_nonneg of_nat_0_le_iff)
have "(real k)⇧2 - 10 * real k ≤ (l-m) * (10 + 9*k)"
using 110 ‹m<l› ‹k>0›
by (simp add: γ'_def field_split_simps power2_eq_square)
with big ‹k≥l› have "k/10 ≤ l-m"
unfolding Big101b_def Big_Closer_10_1_def by (smt (verit, best) mult_right_mono of_nat_0_le_iff of_nat_mult)
then have k10_lm: "nat ⌊k/10⌋ ≤ l - m"
by linarith
have lm_ge_25: "nat ⌊2/5 * l⌋ ≤ l - m"
using False l4k k10_lm by linarith
have "l + Suc l - q ≤ (k+q choose q) / exp(δ*k)"
if "nat⌊k/10⌋ ≤ q" "q≤l" for q
using that
proof (induction q rule: nat_induct_at_least)
case base
have †: "0 < 10 + 10 * real_of_int ⌊k/10⌋ / k"
using ‹k>0› by (smt (verit) divide_nonneg_nonneg of_nat_0_le_iff of_nat_int_floor)
have ln9: "ln (10::real) ≥ 2"
by (approximation 5)
have "l + real (Suc l - nat⌊k/10⌋) ≤ 2 + k/2"
using l4k by linarith
also have "… ≤ exp(of_int⌊k/10⌋ * 2 - k/200)"
using big by (simp add: Big101a_def Big_Closer_10_1_def ‹l ≤ k›)
also have "… ≤ exp(⌊k/10⌋ * ln(10) - k/200)"
by (intro exp_mono diff_mono mult_left_mono ln9) auto
also have "… ≤ exp(⌊k/10⌋ * ln(10)) * exp (-real k/200)"
by (simp add: mult_exp_exp)
also have "… ≤ exp(⌊k/10⌋ * ln(10 + (10 * nat⌊k/10⌋) / k)) * exp (-real k/200)"
using † by (intro mult_mono exp_mono) auto
also have "… ≤ (10 + (10 * nat⌊k/10⌋) / k) ^ nat⌊k/10⌋ * exp (-real k/200)"
using † by (auto simp: powr_def simp flip: powr_realpow)
also have "… ≤ ((k + nat⌊k/10⌋) / (k/10)) ^ nat⌊k/10⌋ * exp (-real k/200)"
using ‹k>0› by (simp add: mult.commute add_divide_distrib)
also have "… ≤ ((k + nat⌊k/10⌋) / nat⌊k/10⌋) ^ nat⌊k/10⌋ * exp (-real k/200)"
proof (intro mult_mono power_mono divide_left_mono)
show "nat⌊k/10⌋ ≤ k/10"
by linarith
qed (use ‹k≥36› in auto)
also have "… ≤ (k + nat⌊k/10⌋ gchoose nat⌊k/10⌋) * exp (-real k/200)"
by (meson exp_gt_zero gbinomial_ge_n_over_k_pow_k le_add2 mult_le_cancel_right_pos of_nat_mono)
also have "… ≤ (k + nat⌊k/10⌋ choose nat⌊k/10⌋) * exp (-real k/200)"
by (simp add: binomial_gbinomial)
also have "… ≤ (k + nat⌊k/10⌋ choose nat⌊k/10⌋) / exp (δ * k)"
using γ ‹0 < k› by (simp add: algebra_simps δ_def exp_minus' frac_le)
finally show ?case by linarith
next
case (Suc q)
then show ?case
apply simp
by (smt (verit) divide_right_mono exp_ge_zero of_nat_0_le_iff)
qed
from ‹m<l› this [of "l-m"]
have "1 + l + real m ≤ (k+l-m choose (l-m)) / exp δ ^ k"
by (simp add: exp_of_nat2_mult k10_lm)
also have "… ≤ (k+l-m choose (l-m)) / exp (δ * k)"
by (simp add: exp_of_nat2_mult)
also have "… < U_lower_bound_ratio m * (real n)"
proof -
have §: "(k+l choose l) / exp (δ * k) < n"
by (simp add: less_eq_real_def nexp_gt pos_divide_less_eq)
show ?thesis
using mult_strict_left_mono [OF §, of "U_lower_bound_ratio m"] kl_choose prod_gt0
by (auto simp: field_simps)
qed
finally have U_MINUS_M: "1+l < real n * U_lower_bound_ratio m - m"
by argo
then have cardU_gt: "card U > l + 1" "card U > 1"
using cardU by linarith+
show False
using γ'_cases
proof cases
case 1
define EU where "EU ≡ E ∩ Pow U"
define RedU where "RedU ≡ Red ∩ Pow U"
define BlueU where "BlueU ≡ Blue ∩ Pow U"
have RedU_eq: "RedU = EU ∖ BlueU"
using BlueU_def Blue_def EU_def RedU_def Red_E by fastforce
obtain [iff]: "finite RedU" "finite BlueU" "RedU ⊆ EU"
using BlueU_def EU_def RedU_def E_def V_def Red_E Blue_E fin_edges finite_subset by blast
then have card_EU: "card EU = card RedU + card BlueU"
by (simp add: BlueU_def Blue_def Diff_Int_distrib2 EU_def RedU_def card_Diff_subset card_mono)
then have card_RedU_le: "card RedU ≤ card EU"
by linarith
interpret UBB: Book_Basis U "E ∩ Pow U" p0_min
proof
fix e assume "e ∈ E ∩ Pow U"
with two_edges show "e ⊆ U" "card e = 2" by auto
next
show "finite U"
using ‹U ⊆ V› by (simp add: V_def finite_subset)
have "x ∈ E" if "x ∈ all_edges U" for x
using ‹U ⊆ V› all_edges_mono that complete E_def by blast
then show "E ∩ Pow U = all_edges U"
using comp_sgraph.wellformed ‹U ⊆ V› by (auto intro: e_in_all_edges_ss)
qed auto
have BlueU_eq: "BlueU = EU ∖ RedU"
using Blue_eq complete by (fastforce simp: BlueU_def RedU_def EU_def V_def E_def)
have [simp]: "UBB.graph_size = card EU"
using EU_def by blast
have "card EU > 0"
using ‹card U > 1› UBB.complete by (simp add: EU_def UBB.finV card_all_edges)
have False if "UBB.graph_density BlueU > γ'"
proof -
have Nx: "Neighbours BlueU x ∩ (U ∖ {x}) = Neighbours BlueU x" for x
using that by (auto simp: BlueU_eq EU_def Neighbours_def)
have "BlueU ⊆ E ∩ Pow U"
using BlueU_eq EU_def by blast
with UBB.exists_density_edge_density [of 1 BlueU]
obtain x where "x∈U" and x: "UBB.graph_density BlueU ≤ UBB.gen_density BlueU {x} (U∖{x})"
by (metis UBB.complete ‹1 < UBB.gorder› card_1_singletonE insertI1 zero_less_one subsetD)
with that have "γ' ≤ UBB.gen_density BlueU (U∖{x}) {x}"
using UBB.gen_density_commute by auto
then have *: "γ' * (card U - 1) ≤ card (Neighbours BlueU x)"
using ‹BlueU ⊆ E ∩ Pow U› ‹card U > 1› ‹x ∈ U›
by (simp add: UBB.gen_density_def UBB.edge_card_eq_sum_Neighbours UBB.finV divide_simps Nx)
have x: "x ∈ V∖W"
using ‹x ∈ U› ‹U ⊆ V› ‹disjnt U W› by (auto simp: U_def disjnt_iff)
moreover
have "is_good_clique n (insert x W)"
unfolding is_good_clique_def
proof (intro conjI)
show "clique (insert x W) Blue"
proof (intro clique_insert)
show "clique W Blue"
using 53 is_good_clique_def by blast
show "all_edges_betw_un {x} W ⊆ Blue"
using ‹x∈U› by (auto simp: U_def all_edges_betw_un_def insert_commute in_Neighbours_iff)
qed (use ‹W ⊆ V› ‹x ∈ V∖W› in auto)
next
show "insert x W ⊆ V"
using ‹W ⊆ V› ‹x ∈ V∖W› by auto
next
have NB_Int_U: "Neighbours Blue x ∩ U = Neighbours BlueU x"
using ‹x ∈ U› by (auto simp: BlueU_def U_def Neighbours_def)
have ulb_ins: "U_lower_bound_ratio (card (insert x W)) = U_lower_bound_ratio m * γ'"
using ‹x ∈ V∖W› ‹finite W› by (simp add: m_def U_lower_bound_ratio_def γ'_def)
have "n * U_lower_bound_ratio (card (insert x W)) = n * U_lower_bound_ratio m * γ'"
by (simp add: ulb_ins)
also have "… ≤ real (m + card U) * γ'"
using mult_right_mono [OF cardU, of "γ'"] ‹0 < γ'› by argo
also have "… ≤ m + card U * γ'"
using mult_left_mono [OF ‹γ'≤1›, of m] by (simp add: algebra_simps)
also have "… ≤ Suc m + γ' * (UBB.gorder - Suc 0)"
using * ‹x ∈ V∖W› ‹finite W› ‹1 < UBB.gorder› ‹γ'≤1›
by (simp add: U_lower_bound_ratio_def algebra_simps)
also have "… ≤ Suc m + card (V ∩ ⋂ (Neighbours Blue ` insert x W))"
using * NB_Int_U finV by (simp add: U_def Int_ac)
also have "… = real (card (insert x W) + card (V ∩ ⋂ (Neighbours Blue ` insert x W)))"
using x ‹finite W› VUU by (auto simp: m_def U_def)
finally show "n * U_lower_bound_ratio (card(insert x W)) - card(insert x W)
≤ card (V ∩ ⋂ (Neighbours Blue ` insert x W))"
by simp
qed
ultimately show False
using 1 clique_cases by blast
qed
then have *: "UBB.graph_density BlueU ≤ γ'" by force
have no_RedU_K: "¬ (∃K. UBB.size_clique k K RedU)"
unfolding UBB.size_clique_def RedU_def
by (metis Int_subset_iff VUU all_edges_subset_iff_clique no_Red_K size_clique_def)
have "(∃K. UBB.size_clique k K RedU) ∨ (∃K. UBB.size_clique (l-m) K BlueU)"
proof (rule ccontr)
assume neg: "¬ ((∃K. UBB.size_clique k K RedU) ∨ (∃K. UBB.size_clique (l-m) K BlueU))"
interpret UBB_NC: No_Cliques U "E ∩ Pow U" p0_min RedU BlueU "l-m" k
proof
show "BlueU = E ∩ Pow U ∖ RedU"
using BlueU_eq EU_def by fastforce
qed (use neg EU_def ‹RedU ⊆ EU› no_RedU_K ‹l≤k› in auto)
show False
proof (intro UBB_NC.Closer_10_2)
have "δ ≤ 1/200"
using γ by (simp add: δ_def field_simps)
then have "exp (δ * real k) ≤ exp (real k/200)"
using ‹0 < k› by auto
then have expexp: "exp (δ*k) * exp (- real k/200) ≤ 1"
by (metis divide_minus_left exp_ge_zero exp_minus_inverse mult_right_mono)
have "exp (- real k/200) * (k + (l-m) choose (l-m)) = exp (- real k/200) * U_lower_bound_ratio m * (k+l choose l)"
using ‹m < l› kl_choose by force
also have "… < (n/2) * exp (δ*k) * exp (- real k/200) * U_lower_bound_ratio m"
using n2exp_gt prod_gt0 by auto
also have "… ≤ (n/2) * U_lower_bound_ratio m"
using mult_left_mono [OF expexp, of "(n/2) * U_lower_bound_ratio m"] prod_gt0 by (simp add: mult_ac)
also have "… ≤ n * U_lower_bound_ratio m - m"
using U_MINUS_M ‹m < l› by auto
finally have "exp (- real k/200) * (k + (l-m) choose (l-m)) ≤ UBB.nV"
using cardU by linarith
then show "exp (- real k / 200) * (k + (l-m) choose (l-m)) ≤ UBB.nV"
using ‹m < l› by (simp add: γ'_def)
next
have "1 - γ' ≤ UBB.graph_density RedU"
using * card_EU ‹card EU > 0›
by (simp add: UBB.graph_density_def BlueU_eq field_split_simps split: if_split_asm)
then show "1 - real (l-m) / (real k + real (l-m)) ≤ UBB.graph_density RedU"
unfolding γ'_def using ‹m<l› by (smt (verit, ccfv_threshold) less_imp_le_nat of_nat_add of_nat_diff)
next
show "p0_min ≤ 1 - real (l-m) / (real k + real (l-m))"
using p0_min_101 ‹γ'≤γ› ‹m < l› γ
by (smt (verit, del_insts) of_nat_add γ'_def less_imp_le_nat of_nat_diff)
next
have Big_10_2I: "⋀l' μ. ⟦nat ⌊2/5 * l⌋ ≤ l'; 1/10 ≤ μ; μ ≤ 1 / 5⟧ ⟹ Big_Closer_10_2 μ l'"
using big by (meson Big101d_def Big_Closer_10_1_def order.refl)
have "m ≤ real l * (1 - (10/11)*γ)"
using ‹m<l› ‹γ>1/10› ‹γ'≥1/10› γ
apply (simp add: γ_def γ'_def field_simps)
by (smt (verit, ccfv_SIG) mult.commute mult_left_mono distrib_left)
then have "real l - real m ≥ (10/11) * γ * l"
by (simp add: algebra_simps)
moreover
have "1/10 ≤ γ' ∧ γ' ≤ 1/5"
using mult_mono [OF γ γ] ‹γ'≥1/10› ‹γ' ≤ γ› γ by (auto simp: power2_eq_square)
ultimately
have "Big_Closer_10_2 γ' (l-m)"
using lm_ge_25 by (intro Big_10_2I) auto
then show "Big_Closer_10_2 ((l-m) / (real k + real (l-m))) (l-m)"
by (simp add: γ'_def ‹m < l› add_diff_eq less_or_eq_imp_le)
next
show "l-m ≤ k"
using ‹l ≤ k› by auto
show "(l-m) / (real k + real (l-m)) ≤ 1/5"
using γ γ_def ‹m < l› by fastforce
show "1/10 ≤ (l-m) / (real k + real (l-m))"
using γ'_def ‹1/10 ≤ γ'› ‹m < l› by auto
qed
qed
with no_RedU_K UBB.size_clique_def obtain K where "K ⊆ U" "UBB.size_clique (l-m) K BlueU"
by meson
then show False
using no_Blue_K extend_Blue_clique VUU
unfolding UBB.size_clique_def size_clique_def BlueU_def
by (metis Int_subset_iff all_edges_subset_iff_clique)
next
case 2
have "RN k (l-m) ≤ exp (- ((l-m) / (k + real (l-m)) / 20) * k + 1) * (k + (l-m) choose (l-m))"
proof (intro Far_9_1 strip)
show "real (l-m) / (real k + real (l-m)) ≤ 1/10"
using γ'_def 2 ‹m < l› by auto
next
show "Big_Far_9_1 (real (l-m) / (k + real (l-m))) (l-m)"
proof (intro Big91_I [OF lm_ge_25])
have "0.07 ≤ (1::real)/10 - 1/36"
by (approximation 5)
also have "… ≤ 1/10 - 1/k"
using ‹k≥36› by (intro diff_mono divide_right_mono) auto
finally have 7: "γ' ≥ 0.07" using 110 by linarith
with ‹m<l› show "γ0 ≤ real (l-m) / (real k + real (l-m))"
by (simp add: γ0_def min_le_iff_disj γ'_def algebra_simps)
next
show "real (l-m) / (real k + real (l-m)) ≤ 1/10"
using 2 ‹m<l› by (simp add: γ'_def)
qed
next
show "p0_min ≤ 1 - 1/10 * (1 + 1 / 15)"
using p0_min_101 by auto
qed
also have "… ≤ real n * U_lower_bound_ratio m - m"
proof -
have "γ * real k ≤ k/5"
using γ ‹0 < k› by auto
also have "… ≤ γ' * (real k * 2) + 2"
using mult_left_mono [OF 110, of "k*2"] ‹k>0› by (simp add: algebra_simps)
finally have "γ * real k ≤ γ' * (real k * 2) + 2" .
then have expexp: "exp (δ * real k) * exp (-γ'*k / 20 - 1) ≤ 1"
by (simp add: δ_def flip: exp_add)
have "exp (-γ'*k/20 + 1) * (k + (l-m) choose (l-m)) = exp (-γ'*k/20+1) * U_lower_bound_ratio m * (k+l choose l)"
using ‹m < l› kl_choose by force
also have "… < (n/2) * exp (δ*k) * exp (-γ'*k/20 - 1) * U_lower_bound_ratio m"
using n2exp_gt' prod_gt0 by (simp add: exp2 exp_diff exp_minus' mult_ac pos_less_divide_eq)
also have "… ≤ (n/2) * U_lower_bound_ratio m"
using expexp order_le_less prod_gt0 by fastforce
also have "… ≤ n * U_lower_bound_ratio m - m"
using U_MINUS_M ‹m < l› by fastforce
finally show ?thesis
using ‹m < l› by (simp add: γ'_def) argo
qed
also have "… ≤ card U"
using cardU by auto
finally have "RN k (l-m) ≤ card U" by linarith
then show False
using Red_Blue_RN ‹U ⊆ V› extend_Blue_clique no_Blue_K no_Red_K by blast
qed
qed
qed
definition "ok_fun_10_1 ≡ λγ k. if Big_Closer_10_1 (min γ 0.07) (nat⌈((γ / (1-γ)) * k)⌉) then 3 else (γ/40 * k)"
lemma ok_fun_10_1:
assumes "0 < γ" "γ < 1"
shows "ok_fun_10_1 γ ∈ o(real)"
proof -
define γ0 where "γ0 ≡ min γ 0.07"
have "γ0 > 0"
using assms by (simp add: γ0_def)
then have "∀⇧∞l. Big_Closer_10_1 γ0 l"
by (simp add: Big_Closer_10_1)
then obtain l where "⋀l'. l' ≥ l ⟹ Big_Closer_10_1 γ0 l'"
using eventually_sequentially by auto
moreover
have "nat⌈((γ / (1-γ)) * k)⌉ ≥ l" if "real k ≥ l/γ - l" for k
using that assms
by (auto simp: field_simps intro!: le_natceiling_iff)
ultimately have "∀⇧∞k. Big_Closer_10_1 (min γ 0.07) (nat⌈((γ / (1-γ)) * k)⌉)"
by (smt (verit) γ0_def eventually_sequentially nat_ceiling_le_eq)
then have "∀⇧∞k. ok_fun_10_1 γ k = 3"
by (simp add: ok_fun_10_1_def eventually_mono)
then show ?thesis
by (simp add: const_smallo_real landau_o.small.in_cong)
qed
theorem Closer_10_1_unconditional:
fixes l k::nat
fixes δ γ::real
defines "γ ≡ real l / (real k + real l)"
defines "δ ≡ γ/40"
assumes γ: "0 < γ" "γ ≤ 1/5"
assumes p0_min_101: "p0_min ≤ 1 - 1/5"
shows "RN k l ≤ exp (-δ*k + ok_fun_10_1 γ k) * (k+l choose l)"
proof -
define γ0 where "γ0 ≡ min γ 0.07"
show ?thesis
proof (cases "Big_Closer_10_1 γ0 l")
case True
show ?thesis
using Closer_10_1 [OF True [unfolded γ0_def γ_def]] assms
by (simp add: ok_fun_10_1_def γ_def δ_def RN_le_choose')
next
case False
have "(nat ⌈γ * k / (1-γ)⌉) ≤ l"
by (simp add: γ_def divide_simps)
with False Big_Closer_10_1_upward
have "¬ Big_Closer_10_1 γ0 (nat ⌈γ * k / (1-γ)⌉)"
by blast
then show ?thesis
by (simp add: ok_fun_10_1_def δ_def γ0_def RN_le_choose')
qed
qed
end
end