theory Girth_Chromatic imports Ugraphs Girth_Chromatic_Misc "HOL-Probability.Probability" "HOL-Decision_Procs.Approximation" begin section ‹Probability Space on Sets of Edges› definition cylinder :: "'a set ⇒ 'a set ⇒ 'a set ⇒ 'a set set" where "cylinder S A B = {T ∈ Pow S. A ⊆ T ∧ B ∩ T = {}}" lemma full_sum: fixes p :: real assumes "finite S" shows "(∑A∈Pow S. p^card A * (1 - p)^card (S - A)) = 1" using assms proof induct case (insert s S) have "inj_on (insert s) (Pow S)" and "⋀x. S - insert s x = S - x" and "Pow S ∩ insert s ` Pow S = {}" and "⋀x. x ∈ Pow S ⟹ card (insert s S - x) = Suc (card (S - x))" using insert(1-2) by (auto simp: insert_Diff_if intro!: inj_onI) moreover have "⋀x. x ⊆ S ⟹ card (insert s x) = Suc (card x)" using insert(1-2) by (subst card.insert) (auto dest: finite_subset) ultimately show ?case by (simp add: sum.reindex sum_distrib_left[symmetric] ac_simps insert.hyps sum.union_disjoint Pow_insert) qed simp text ‹Definition of the probability space on edges:› locale edge_space = fixes n :: nat and p :: real assumes p_prob: "0 ≤ p" "p ≤ 1" begin definition S_verts :: "nat set" where "S_verts ≡ {1..n}" definition S_edges :: "uedge set" where "S_edges = all_edges S_verts" definition edge_ugraph :: "uedge set ⇒ ugraph" where "edge_ugraph es ≡ (S_verts, es ∩ S_edges)" definition "P = point_measure (Pow S_edges) (λs. p^card s * (1 - p)^card (S_edges - s))" lemma finite_verts[intro!]: "finite S_verts" by (auto simp: S_verts_def) lemma finite_edges[intro!]: "finite S_edges" by (auto simp: S_edges_def all_edges_def finite_verts) lemma finite_graph[intro!]: "finite (uverts (edge_ugraph es))" unfolding edge_ugraph_def by auto lemma uverts_edge_ugraph[simp]: "uverts (edge_ugraph es) = S_verts" by (simp add: edge_ugraph_def) lemma uedges_edge_ugraph[simp]: "uedges (edge_ugraph es) = es ∩ S_edges" unfolding edge_ugraph_def by simp lemma space_eq: "space P = Pow S_edges" by (simp add: P_def space_point_measure) lemma sets_eq: "sets P = Pow (Pow S_edges)" by (simp add: P_def sets_point_measure) lemma emeasure_eq: "emeasure P A = (if A ⊆ Pow S_edges then (∑edges∈A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)" using finite_edges p_prob by (simp add: P_def space_point_measure emeasure_point_measure_finite sets_point_measure emeasure_notin_sets) lemma integrable_P[intro, simp]: "integrable P (f::_ ⇒ real)" using finite_edges by (simp add: integrable_point_measure_finite P_def) lemma borel_measurable_P[measurable]: "f ∈ borel_measurable P" unfolding P_def by simp lemma prob_space_P: "prob_space P" proof show "emeasure P (space P) = 1" ― ‹Sum of probabilities equals 1› using finite_edges by (simp add: emeasure_eq full_sum one_ereal_def space_eq) qed end sublocale edge_space ⊆ prob_space P by (rule prob_space_P) context edge_space begin lemma prob_eq: "prob A = (if A ⊆ Pow S_edges then (∑edges∈A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)" using emeasure_eq[of A] p_prob unfolding emeasure_eq_measure by (simp add: sum_nonneg) lemma integral_finite_singleton: "integral⇧^{L}P f = (∑x∈Pow S_edges. f x * measure P {x})" using p_prob prob_eq unfolding P_def by (subst lebesgue_integral_point_measure_finite) (auto intro!: sum.cong) text ‹Probability of cylinder sets:› lemma cylinder_prob: assumes "A ⊆ S_edges" "B ⊆ S_edges" "A ∩ B = {}" shows "prob (cylinder S_edges A B) = p ^ (card A) * (1 - p) ^ (card B)" (is "_ = ?pp A B") proof - have "Pow S_edges ∩ cylinder S_edges A B = cylinder S_edges A B" "⋀x. x ∈ cylinder S_edges A B ⟹ A ∪ x = x" "⋀x. x ∈ cylinder S_edges A B ⟹ finite x" "⋀x. x ∈ cylinder S_edges A B ⟹ B ∩ (S_edges - B - x) = {}" "⋀x. x ∈ cylinder S_edges A B ⟹ B ∪ (S_edges - B - x) = S_edges - x" "finite A" "finite B" using assms by (auto simp add: cylinder_def intro: finite_subset) then have "(∑T∈cylinder S_edges A B. ?pp T (S_edges - T)) = (∑T ∈ cylinder S_edges A B. p^(card A + card (T - A)) * (1 - p)^(card B + card ((S_edges - B) - T)))" using finite_edges by (simp add: card_Un_Int) also have "… = ?pp A B * (∑T∈cylinder S_edges A B. ?pp (T - A) (S_edges - B - T))" by (simp add: power_add sum_distrib_left ac_simps) also have "… = ?pp A B" proof - have "⋀T. T ∈ cylinder S_edges A B ⟹ S_edges - B - T = (S_edges - A) - B - (T - A)" "Pow (S_edges - A - B) = (λx. x - A) ` cylinder S_edges A B" "inj_on (λx. x - A) (cylinder S_edges A B)" "finite (S_edges - A - B)" using assms by (auto simp: cylinder_def intro!: inj_onI) with full_sum[of "S_edges - A - B"] show ?thesis by (simp add: sum.reindex) qed finally show ?thesis by (auto simp add: prob_eq cylinder_def) qed lemma Markov_inequality: fixes a :: real and X :: "uedge set ⇒ real" assumes "0 < c" "⋀x. 0 ≤ f x" shows "prob {x ∈ space P. c ≤ f x} ≤ (∫x. f x ∂ P) / c" proof - from assms have "(∫⇧^{+}x. ennreal (f x) ∂P) = (∫x. f x ∂P)" by (intro nn_integral_eq_integral) auto with assms show ?thesis using nn_integral_Markov_inequality[of f "space P" P "1 / c"] by (simp cong: nn_integral_cong add: emeasure_eq_measure ennreal_mult[symmetric]) qed end subsection ‹Graph Probabilities outside of @{term Edge_Space} locale› text ‹ These abbreviations allow a compact expression of probabilities about random graphs outside of the @{term Edge_Space} locale. We also transfer a few of the lemmas we need from the locale into the toplevel theory. › abbreviation MGn :: "(nat ⇒ real) ⇒ nat ⇒ (uedge set) measure" where "MGn p n ≡ (edge_space.P n (p n))" abbreviation probGn :: "(nat ⇒ real) ⇒ nat ⇒ (uedge set ⇒ bool) ⇒ real" where "probGn p n P ≡ measure (MGn p n) {es ∈ space (MGn p n). P es}" lemma probGn_le: assumes p_prob: "0 < p n" "p n < 1" assumes sub: "⋀n es. es ∈ space (MGn p n) ⟹ P n es ⟹ Q n es" shows "probGn p n (P n) ≤ probGn p n (Q n)" proof - from p_prob interpret E: edge_space n "p n" by unfold_locales auto show ?thesis by (auto intro!: E.finite_measure_mono sub simp: E.space_eq E.sets_eq) qed section ‹Short cycles› definition short_cycles :: "ugraph ⇒ nat ⇒ uwalk set" where "short_cycles G k ≡ {p ∈ ucycles G. uwalk_length p ≤ k}" text ‹obtains a vertex in a short cycle:› definition choose_v :: "ugraph ⇒ nat ⇒ uvert" where "choose_v G k ≡ SOME u. ∃p. p ∈ short_cycles G k ∧ u ∈ set p" partial_function (tailrec) kill_short :: "ugraph ⇒ nat ⇒ ugraph" where "kill_short G k = (if short_cycles G k = {} then G else (kill_short (G -- (choose_v G k)) k))" lemma ksc_simps[simp]: "short_cycles G k = {} ⟹ kill_short G k = G" "short_cycles G k ≠ {} ⟹ kill_short G k = kill_short (G -- (choose_v G k)) k" by (auto simp: kill_short.simps) lemma assumes "short_cycles G k ≠ {}" shows choose_v__in_uverts: "choose_v G k ∈ uverts G" (is ?t1) and choose_v__in_short: "∃p. p ∈ short_cycles G k ∧ choose_v G k ∈ set p" (is ?t2) proof - from assms obtain p where "p ∈ ucycles G" "uwalk_length p ≤ k" unfolding short_cycles_def by auto moreover then obtain u where "u ∈ set p" unfolding ucycles_def by (cases p) (auto simp: uwalk_length_conv) ultimately have "∃u p. p ∈ short_cycles G k ∧ u ∈ set p" by (auto simp: short_cycles_def) then show ?t2 by (auto simp: choose_v_def intro!: someI_ex) then show ?t1 by (auto simp: short_cycles_def ucycles_def uwalks_def) qed lemma kill_step_smaller: assumes "short_cycles G k ≠ {}" shows "short_cycles (G -- (choose_v G k)) k ⊂ short_cycles G k" proof - let ?cv = "choose_v G k" from assms obtain p where "p ∈ short_cycles G k" "?cv ∈ set p" by atomize_elim (rule choose_v__in_short) have "short_cycles (G -- ?cv) k ⊆ short_cycles G k" proof fix p assume "p ∈ short_cycles (G -- ?cv) k" then show "p ∈ short_cycles G k" unfolding short_cycles_def ucycles_def uwalks_def using edges_Gu[of G ?cv] by (auto simp: verts_Gu) qed moreover have "p ∉ short_cycles (G -- ?cv) k" using ‹?cv ∈ set p› by (auto simp: short_cycles_def ucycles_def uwalks_def verts_Gu) ultimately show ?thesis using ‹p ∈ short_cycles G k› by auto qed text ‹Induction rule for @{term kill_short}:› lemma kill_short_induct[consumes 1, case_names empty kill_vert]: assumes fin: "finite (uverts G)" assumes a_empty: "⋀G. short_cycles G k = {} ⟹ P G k" assumes a_kill: "⋀G. finite (short_cycles G k) ⟹ short_cycles G k ≠ {} ⟹ P (G -- (choose_v G k)) k ⟹ P G k" shows "P G k" proof - have "finite (short_cycles G k)" using finite_ucycles[OF fin] by (auto simp: short_cycles_def) then show ?thesis by (induct "short_cycles G k" arbitrary: G rule: finite_psubset_induct) (metis kill_step_smaller a_kill a_empty) qed text ‹Large Girth (after @{term kill_short}):› lemma kill_short_large_girth: assumes "finite (uverts G)" shows "k < girth (kill_short G k)" using assms proof (induct G k rule: kill_short_induct) case (empty G) then have "⋀p. p ∈ ucycles G ⟹ k < enat (uwalk_length p)" by (auto simp: short_cycles_def) with empty show ?case by (auto simp: girth_def intro: enat_less_INF_I) qed simp text ‹Order of graph (after @{term kill_short}):› lemma kill_short_order_of_graph: assumes "finite (uverts G)" shows "card (uverts G) - card (short_cycles G k) ≤ card (uverts (kill_short G k))" using assms assms proof (induct G k rule: kill_short_induct) case (kill_vert G) let ?oG = "G -- (choose_v G k)" have "finite (uverts ?oG)" using kill_vert by (auto simp: remove_vertex_def) moreover have "uverts (kill_short G k) = uverts (kill_short ?oG k)" using kill_vert by simp moreover have "card (uverts G) = Suc (card (uverts ?oG))" using choose_v__in_uverts kill_vert by (simp add: remove_vertex_def card_Suc_Diff1 del: card_Diff_insert) moreover have "card (short_cycles ?oG k) < card (short_cycles G k)" by (intro psubset_card_mono kill_vert.hyps kill_step_smaller) ultimately show ?case using kill_vert.hyps by presburger qed simp text ‹Independence number (after @{term kill_short}):› lemma kill_short_α: assumes "finite (uverts G)" shows "α (kill_short G k) ≤ α G" using assms proof (induct G k rule: kill_short_induct) case (kill_vert G) note kill_vert(3) also have "α (G -- (choose_v G k)) ≤ α G" by (rule α_remove_le) finally show ?case using kill_vert by simp qed simp text ‹Wellformedness (after @{term kill_short}):› lemma kill_short_uwellformed: assumes "finite (uverts G)" "uwellformed G" shows "uwellformed (kill_short G k)" using assms proof (induct G k rule: kill_short_induct) case (kill_vert G) from kill_vert.prems have "uwellformed (G -- (choose_v G k))" by (auto simp: uwellformed_def remove_vertex_def) with kill_vert.hyps show ?case by simp qed simp section ‹The Chromatic-Girth Theorem› text ‹Probability of Independent Edges:› lemma (in edge_space) random_prob_independent: assumes "n ≥ k" "k ≥ 2" shows "prob {es ∈ space P. k ≤ α (edge_ugraph es)} ≤ (n choose k)*(1-p)^(k choose 2)" proof - let "?k_sets" = "{vs. vs ⊆ S_verts ∧ card vs = k}" { fix vs assume A: "vs ∈ ?k_sets" then have B: "all_edges vs ⊆ S_edges" unfolding all_edges_def S_edges_def by blast have "{es ∈ space P. vs ∈ independent_sets (edge_ugraph es)} = cylinder S_edges {} (all_edges vs)" (is "?L = _") using A by (auto simp: independent_sets_def edge_ugraph_def space_eq cylinder_def) then have "prob ?L = (1-p)^(k choose 2)" using A B finite by (auto simp: cylinder_prob card_all_edges dest: finite_subset) } note prob_k_indep = this ― ‹probability that a fixed set of k vertices is independent in a random graph› have "{es ∈ space P. k ∈ card ` independent_sets (edge_ugraph es)} = (⋃vs ∈ ?k_sets. {es ∈ space P. vs ∈ independent_sets (edge_ugraph es)})" (is "?L = ?R") unfolding image_def space_eq independent_sets_def by auto then have "prob ?L ≤ (∑vs ∈ ?k_sets. prob {es ∈ space P. vs ∈ independent_sets (edge_ugraph es)})" by (auto intro!: finite_measure_subadditive_finite simp: space_eq sets_eq) also have "… = (n choose k)*((1 - p) ^ (k choose 2))" by (simp add: prob_k_indep S_verts_def n_subsets) finally show ?thesis using ‹k ≥ 2› by (simp add: le_α_iff) qed text ‹Almost never many independent edges:› lemma almost_never_le_α: fixes k :: nat and p :: "nat ⇒ real" assumes p_prob: "∀⇧^{∞}n. 0 < p n ∧ p n < 1" assumes [arith]: "k > 0" assumes N_prop: "∀⇧^{∞}n. (6 * k * ln n)/n ≤ p n" shows "(λn. probGn p n (λes. 1/2*n/k ≤ α (edge_space.edge_ugraph n es))) ⇢ 0" (is "(λn. ?prob_fun n) ⇢ 0") proof - let "?prob_fun_raw n" = "probGn p n (λes. nat(ceiling (1/2*n/k)) ≤ α (edge_space.edge_ugraph n es))" define r where "r n = 1 / 2 * n / k" for n :: nat let ?nr = "λn. nat(ceiling (r n))" have r_pos: "⋀n. 0 < n ⟹ 0 < r n " by (auto simp: r_def field_simps) have nr_bounds: "∀⇧^{∞}n. 2 ≤ ?nr n ∧ ?nr n ≤ n" by (intro eventually_sequentiallyI[of "4 * k"]) (simp add: r_def nat_ceiling_le_eq le_natceiling_iff field_simps) from nr_bounds p_prob have ev_prob_fun_raw_le: "∀⇧^{∞}n. probGn p n (λes. ?nr n≤ α (edge_space.edge_ugraph n es)) ≤ (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n" (is "∀⇧^{∞}n. ?prob_fun_raw_le n") proof (rule eventually_elim2) fix n :: nat assume A: "2 ≤ ?nr n ∧ ?nr n ≤ n" "0 < p n ∧p n < 1" then interpret pG: edge_space n "p n" by unfold_locales auto have r: "real (?nr n - Suc 0) = real (?nr n) - Suc 0" using A by auto have [simp]: "n>0" using A by linarith have "probGn p n (λes. ?nr n ≤ α (edge_space.edge_ugraph n es)) ≤ (n choose ?nr n) * (1 - p n)^(?nr n choose 2)" using A by (auto intro: pG.random_prob_independent) also have "… ≤ n powr ?nr n * (1 - p n) powr (?nr n choose 2)" using A by (simp add: powr_realpow of_nat_power [symmetric] binomial_le_pow del: of_nat_power) also have "… = n powr ?nr n * (1 - p n) powr (?nr n * (?nr n - 1) / 2)" by (cases "even (?nr n - 1)") (auto simp add: n_choose_2_nat real_of_nat_div) also have "… = n powr ?nr n * ((1 - p n) powr ((?nr n - 1) / 2)) powr ?nr n" by (auto simp add: powr_powr r ac_simps) also have "… ≤ (n * exp (- p n * (?nr n - 1) / 2)) powr ?nr n" proof - have "(1 - p n) powr ((?nr n - 1) / 2) ≤ exp (- p n) powr ((?nr n - 1) / 2)" using A by (auto simp: powr_mono2 diff_conv_add_uminus simp del: add_uminus_conv_diff) also have "… = exp (- p n * (?nr n - 1) / 2)" by (auto simp: powr_def) finally show ?thesis using A by (auto simp: powr_mono2 powr_mult) qed finally show "probGn p n (λes. ?nr n ≤ α (edge_space.edge_ugraph n es)) ≤ (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n" using A r by simp qed from p_prob N_prop have ev_expr_bound: "∀⇧^{∞}n. n * exp (-p n * (real (?nr n) - 1) / 2) ≤ (exp 1 / n) powr (1 / 2)" proof (elim eventually_rev_mp, intro eventually_sequentiallyI conjI impI) fix n assume n_bound[arith]: "2 ≤ n" and p_bound: "0 < p n ∧ p n < 1" "(6 * k * ln n) / n ≤ p n" have r_bound: "r n ≤ ?nr n" by (rule real_nat_ceiling_ge) have "n * exp (-p n * (real (?nr n)- 1) / 2) ≤ n * exp (- 3 / 2 * ln n + p n / 2)" proof - have "0 < ln n" using "n_bound" by auto then have "(3 / 2) * ln n ≤ ((6 * k * ln n) / n) * (?nr n / 2)" using r_bound le_of_int_ceiling[of "n/2*k"] by (simp add: r_def field_simps del: le_of_int_ceiling) also have "… ≤ p n * (?nr n / 2)" using n_bound p_bound r_bound r_pos[of n] by (auto simp: field_simps) finally show ?thesis using r_bound by (auto simp: field_simps) qed also have "… ≤ n * n powr (- 3 / 2) * exp 1 powr (1 / 2)" using p_bound by (simp add: powr_def exp_add [symmetric]) also have "… ≤ n powr (-1 / 2) * exp 1 powr (1 / 2)" by (simp add: powr_mult_base) also have "… = (exp 1 / n) powr (1/2)" by (simp add: powr_divide powr_minus_divide) finally show "n * exp (- p n * (real (?nr n) - 1) / 2) ≤ (exp 1 / n) powr (1 / 2)" . qed have ceil_bound: "⋀G n. 1/2*n/k ≤ α G ⟷ nat(ceiling (1/2*n/k)) ≤ α G" by (case_tac "α G") (auto simp: nat_ceiling_le_eq) show ?thesis proof (unfold ceil_bound, rule real_tendsto_sandwich) show "(λn. 0) ⇢ 0" "(λn. (exp 1 / n) powr (1 / 2)) ⇢ 0" "∀⇧^{∞}n. 0 ≤ ?prob_fun_raw n" using p_prob by (auto intro: measure_nonneg LIMSEQ_inv_powr elim: eventually_mono) next from nr_bounds ev_expr_bound ev_prob_fun_raw_le show "∀⇧^{∞}n. ?prob_fun_raw n ≤ (exp 1 / n) powr (1 / 2)" proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI conjI) fix n assume A: "3 ≤ n" and nr_bounds: "2 ≤ ?nr n ∧ ?nr n ≤ n" and prob_fun_raw_le: "?prob_fun_raw_le n" and expr_bound: "n * exp (- p n * (real (nat(ceiling (r n))) - 1) / 2) ≤ (exp 1 / n) powr (1 / 2)" have "exp 1 < (3 :: real)" by (approximation 6) then have "(exp 1 / n) powr (1 / 2) ≤ 1 powr (1 / 2)" using A by (intro powr_mono2) (auto simp: field_simps) then have ep_bound: "(exp 1 / n) powr (1 / 2) ≤ 1" by simp have "?prob_fun_raw n ≤ (n * exp (- p n * (real (?nr n) - 1) / 2)) powr (?nr n)" using prob_fun_raw_le by (simp add: r_def) also have "… ≤ ((exp 1 / n) powr (1 / 2)) powr ?nr n" using expr_bound A by (auto simp: powr_mono2) also have "… ≤ ((exp 1 / n) powr (1 / 2))" using nr_bounds ep_bound A by (auto simp: powr_le_one_le) finally show "?prob_fun_raw n ≤ (exp 1 / n) powr (1 / 2)" . qed qed qed text ‹Mean number of k-cycles in a graph. (Or rather of paths describing a circle of length @{term k}):› lemma (in edge_space) mean_k_cycles: assumes "3 ≤ k" "k < n" shows "(∫es. card {c ∈ ucycles (edge_ugraph es). uwalk_length c = k} ∂ P) = of_nat (fact n div fact (n - k)) * p ^ k" proof - let ?k_cycle = "λes c k. c ∈ ucycles (edge_ugraph es) ∧ uwalk_length c = k" define C where "C k = {c. ?k_cycle S_edges c k}" for k ― ‹@{term "C k"} is the set of all possible cycles of size @{term k} in @{term "edge_ugraph S_edges"}› define XG where "XG es = {c. ?k_cycle es c k}" for es ― ‹@{term "XG es"} is the set of cycles contained in a @{term "edge_ugraph es"}› define XC where "XC c = {es ∈ space P. ?k_cycle es c k}" for c ― ‹"@{term "XC c"} is the set of graphs (edge sets) containing a cycle c"› then have XC_in_sets: "⋀c. XC c ∈ sets P" and XC_cyl: "⋀c. c ∈ C k ⟹ XC c = cylinder S_edges (set (uwalk_edges c)) {}" by (auto simp: ucycles_def space_eq uwalks_def C_def cylinder_def sets_eq) have "(∫es. card {c ∈ ucycles (edge_ugraph es). uwalk_length c = k} ∂ P) = (∑x∈space P. card (XG x) * prob {x})" by (simp add: XG_def integral_finite_singleton space_eq) also have "… = (∑c∈C k. prob (cylinder S_edges (set (uwalk_edges c)) {}))" proof - have XG_Int_C: "⋀s. s ∈ space P ⟹ C k ∩ XG s = XG s" unfolding XG_def C_def ucycles_def uwalks_def edge_ugraph_def by auto have fin_XC: "⋀k. finite (XC k)" and fin_C: "finite (C k)" unfolding C_def XC_def by (auto simp: finite_edges space_eq intro!: finite_ucycles) have "(∑x∈space P. card (XG x) * prob {x}) = (∑x∈space P. (∑c ∈ XG x. prob {x}))" by simp also have "… = (∑x∈space P. (∑c ∈ C k. if c ∈ XG x then prob {x} else 0))" using fin_C by (simp add: sum.If_cases) (simp add: XG_Int_C) also have "… = (∑c ∈ C k. (∑ x ∈ space P ∩ XC c. prob {x}))" using finite_edges by (subst sum.swap) (simp add: sum.inter_restrict XG_def XC_def space_eq) also have "… = (∑c ∈ C k. prob (XC c))" using fin_XC XC_in_sets by (auto simp add: prob_eq sets_eq space_eq intro!: sum.cong) finally show ?thesis by (simp add: XC_cyl) qed also have "… = (∑c∈C k. p ^ k)" proof - have "⋀x. x ∈ C k ⟹ card (set (uwalk_edges x)) = uwalk_length x" by (auto simp: uwalk_length_def C_def ucycles_distinct_edges intro: distinct_card) then show ?thesis by (auto simp: C_def ucycles_def uwalks_def cylinder_prob) qed also have "… = of_nat (fact n div fact (n - k)) * p ^ k" proof - have inj_last_Cons: "⋀A. inj_on (λes. last es # es) A" by (rule inj_onI) simp { fix xs A assume "3 ≤ length xs - Suc 0" "hd xs = last xs" then have "xs ∈ (λxs. last xs # xs) ` A ⟷ tl xs ∈ A" by (cases xs) (auto simp: inj_image_mem_iff[OF inj_last_Cons] split: if_split_asm) } note image_mem_iff_inst = this { fix xs have "xs ∈ uwalks (edge_ugraph S_edges) ⟹ set (tl xs) ⊆ S_verts" unfolding uwalks_def by (induct xs) auto } moreover { fix xs assume "set xs ⊆ S_verts" "2 ≤ length xs" "distinct xs" then have "(last xs # xs) ∈ uwalks (edge_ugraph S_edges)" proof (induct xs rule: uwalk_edges.induct) case (3 x y ys) have S_edges_memI: "⋀x y. x ∈ S_verts ⟹ y ∈ S_verts ⟹ x ≠ y ⟹ {x, y} ∈ S_edges" unfolding S_edges_def all_edges_def image_def by auto have "ys ≠ [] ⟹ set ys ⊆ S_verts ⟹ last ys ∈ S_verts" by auto with 3 show ?case by (auto simp add: uwalks_def Suc_le_eq intro: S_edges_memI) qed simp_all} moreover note ‹3 ≤ k› ultimately have "C k = (λxs. last xs # xs) ` {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ S_verts}" by (auto simp: C_def ucycles_def uwalk_length_conv image_mem_iff_inst) moreover have "card S_verts = n" by (simp add: S_verts_def) ultimately have "card (C k) = fact n div fact (n - k)" using ‹k < n› by (simp add: card_image[OF inj_last_Cons] card_lists_distinct_length_eq' fact_div_fact) then show ?thesis by simp qed finally show ?thesis by simp qed text ‹Girth-Chromatic number theorem:› theorem girth_chromatic: fixes l :: nat shows "∃G. uwellformed G ∧ l < girth G ∧ l < chromatic_number G" proof - define k where "k = max 3 l" define ε where "ε = 1 / (2 * k)" define p where "p n = real n powr (ε - 1)" for n :: nat let ?ug = edge_space.edge_ugraph define short_count where "short_count g = card (short_cycles g k)" for g ― ‹This random variable differs from the one used in the proof of theorem 11.2.2, as we count the number of paths describing a circle, not the circles themselves› from k_def have "3 ≤ k" "l ≤ k" by auto from ‹3 ≤ k› have ε_props: "0 < ε" "ε < 1 / k" "ε < 1" by (auto simp: ε_def field_simps) have ev_p: "∀⇧^{∞}n. 0 < p n ∧ p n < 1" proof (rule eventually_sequentiallyI) fix n :: nat assume "2 ≤ n" with ‹ε < 1› have "n powr (ε - 1) < 1" by (auto intro!: powr_less_one) then show "0 < p n ∧ p n < 1" using ‹2 ≤ n› by (auto simp: p_def) qed then have prob_short_count_le: "∀⇧^{∞}n. probGn p n (λes. (real n/2) ≤ short_count (?ug n es)) ≤ 2 * (k - 2) * n powr (ε * k - 1)" (is "∀⇧^{∞}n. ?P n") proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI) fix n :: nat assume A: "Suc k ≤ n" "0 < p n ∧ p n < 1" then interpret pG: edge_space n "p n" by unfold_locales auto have "1 ≤ n" using A by auto define mean_short_count where "mean_short_count = (∫es. short_count (?ug n es) ∂ pG.P)" have mean_short_count_le: "mean_short_count ≤ (k - 2) * n powr (ε * k)" proof - have small_empty: "⋀es k. k ≤ 2 ⟹ short_cycles (edge_space.edge_ugraph n es) k = {}" by (auto simp add: short_cycles_def ucycles_def) have short_count_conv: "⋀es. short_count (?ug n es) = (∑i=3..k. real (card {c ∈ ucycles (?ug n es). uwalk_length c = i}))" proof (unfold short_count_def, induct k) case 0 with small_empty show ?case by auto next case (Suc k) show ?case proof (cases "Suc k ≤ 2") case True with small_empty show ?thesis by auto next case False have "{c ∈ ucycles (?ug n es). uwalk_length c ≤ Suc k} = {c ∈ ucycles (?ug n es). uwalk_length c ≤ k} ∪ {c ∈ ucycles (?ug n es). uwalk_length c = Suc k}" by auto moreover have "finite (uverts (edge_space.edge_ugraph n es))" by auto ultimately have "card {c ∈ ucycles (?ug n es). uwalk_length c ≤ Suc k} = card {c ∈ ucycles (?ug n es). uwalk_length c ≤ k} + card {c ∈ ucycles (?ug n es). uwalk_length c = Suc k}" using finite_ucycles by (subst card_Un_disjoint[symmetric]) auto then show ?thesis using Suc False unfolding short_cycles_def by (auto simp: not_le) qed qed have "mean_short_count = (∑i=3..k. ∫es. card {c ∈ ucycles (?ug n es). uwalk_length c = i} ∂ pG.P)" unfolding mean_short_count_def short_count_conv by (subst Bochner_Integration.integral_sum) (auto intro: pG.integral_finite_singleton) also have "… = (∑i∈{3..k}. of_nat (fact n div fact (n - i)) * p n ^ i)" using A by (simp add: pG.mean_k_cycles) also have "… ≤ (∑ i∈{3..k}. n ^ i * p n ^ i)" apply (rule sum_mono) by (meson A fact_div_fact_le_pow Suc_leD atLeastAtMost_iff of_nat_le_iff order_trans mult_le_cancel_iff1 zero_less_power) also have "... ≤ (∑ i∈{3..k}. n powr (ε * k))" using ‹1 ≤ n› ‹0 < ε› A by (intro sum_mono) (auto simp: p_def field_simps powr_mult_base powr_powr powr_realpow[symmetric] powr_mult[symmetric] powr_add[symmetric]) finally show ?thesis by simp qed have "pG.prob {es ∈ space pG.P. n/2 ≤ short_count (?ug n es)} ≤ mean_short_count / (n/2)" unfolding mean_short_count_def using ‹1 ≤ n› by (intro pG.Markov_inequality) (auto simp: short_count_def) also have "… ≤ 2 * (k - 2) * n powr (ε * k - 1)" proof - have "mean_short_count / (n / 2) ≤ 2 * (k - 2) * (1 / n powr 1) * n powr (ε * k)" using mean_short_count_le ‹1 ≤ n› by (simp add: field_simps) then show ?thesis by (simp add: powr_diff algebra_simps) qed finally show "?P n" . qed define pf_short_count pf_α where "pf_short_count n = probGn p n (λes. n/2 ≤ short_count (?ug n es))" and "pf_α n = probGn p n (λes. 1/2 * n/k ≤ α (edge_space.edge_ugraph n es))" for n have ev_short_count_le: "∀⇧^{∞}n. pf_short_count n < 1 / 2" proof - have "ε * k - 1 < 0" using ε_props ‹3 ≤ k› by (auto simp: field_simps) then have "(λn. 2 * (k - 2) * n powr (ε * k - 1)) ⇢ 0" (is "?bound ⇢ 0") by (intro tendsto_mult_right_zero LIMSEQ_neg_powr) then have "∀⇧^{∞}n. dist (?bound n) 0 < 1 / 2" by (rule tendstoD) simp with prob_short_count_le show ?thesis by (rule eventually_elim2) (auto simp: dist_real_def pf_short_count_def) qed have lim_α: "pf_α ⇢ 0" proof - have "0 < k" using ‹3 ≤ k› by simp have "∀⇧^{∞}n. (6*k) * ln n / n ≤ p n ⟷ (6*k) * ln n * n powr - ε ≤ 1" proof (rule eventually_sequentiallyI) fix n :: nat assume "1 ≤ n" then have "(6 * k) * ln n / n ≤ p n ⟷ (6*k) * ln n * (n powr - 1) ≤ n powr (ε - 1)" by (subst powr_minus) (simp add: divide_inverse p_def) also have "… ⟷ (6*k) * ln n * ((n powr - 1) / (n powr (ε - 1))) ≤ n powr (ε - 1) / (n powr (ε - 1))" using ‹1 ≤ n› by (auto simp: field_simps) also have "… ⟷ (6*k) * ln n * n powr - ε ≤ 1" by (simp add: powr_diff [symmetric] ) finally show "(6*k) * ln n / n ≤ p n ⟷ (6*k) * ln n * n powr - ε ≤ 1" . qed then have "(∀⇧^{∞}n. (6 * k) * ln n / real n ≤ p n) ⟷ (∀⇧^{∞}n. (6*k) * ln n * n powr - ε ≤ 1)" by (rule eventually_subst) also have "∀⇧^{∞}n. (6*k) * ln n * n powr - ε ≤ 1" proof - { fix n :: nat assume "0 < n" have "ln (real n) ≤ n powr (ε/2) / (ε/2)" using ‹0 < n› ‹0 < ε› by (intro ln_powr_bound) auto also have "… ≤ 2/ε * n powr (ε/2)" by (auto simp: field_simps) finally have "(6*k) * ln n * (n powr - ε) ≤ (6*k) * (2/ε * n powr (ε/2)) * (n powr - ε)" using ‹0 < n› ‹0 < k› by (intro mult_right_mono mult_left_mono) auto also have "… = 12*k/ε * n powr (-ε/2)" unfolding divide_inverse by (auto simp: field_simps powr_minus[symmetric] powr_add[symmetric]) finally have "(6*k) * ln n * (n powr - ε) ≤ 12*k/ε * n powr (-ε/2)" . } then have "∀⇧^{∞}n. (6*k) * ln n * (n powr - ε) ≤ 12*k/ε * n powr (-ε/2)" by (intro eventually_sequentiallyI[of 1]) auto also have "∀⇧^{∞}n. 12*k/ε * n powr (-ε/2) ≤ 1" proof - have "(λn. 12*k/ε * n powr (-ε/2)) ⇢ 0" using ‹0 < ε› by (intro tendsto_mult_right_zero LIMSEQ_neg_powr) auto then show ?thesis using ‹0 < ε› by - (drule tendstoD[where e=1], auto elim: eventually_mono) qed finally (eventually_le_le) show ?thesis . qed finally have "∀⇧^{∞}n. real (6 * k) * ln (real n) / real n ≤ p n" . with ev_p ‹0 < k› show ?thesis unfolding pf_α_def by (rule almost_never_le_α) qed from ev_short_count_le lim_α[THEN tendstoD, of "1/2"] ev_p have "∀⇧^{∞}n. 0 < p n ∧ p n < 1 ∧ pf_short_count n < 1/2 ∧ pf_α n < 1/2" by simp (elim eventually_rev_mp, auto simp: eventually_sequentially dist_real_def) then obtain n where "0 < p n" "p n < 1" and [arith]: "0 < n" and probs: "pf_short_count n < 1/2" "pf_α n < 1/2" by (auto simp: eventually_sequentially) then interpret ES: edge_space n "(p n)" by unfold_locales auto have rest_compl: "⋀A P. A - {x∈A. P x} = {x∈A. ¬P x}" by blast from probs have "ES.prob ({es ∈ space ES.P. n/2 ≤ short_count (?ug n es)} ∪ {es ∈ space ES.P. 1/2 * n/k ≤ α (?ug n es)}) ≤ pf_short_count n + pf_α n" unfolding pf_short_count_def pf_α_def by (subst ES.finite_measure_subadditive) auto also have "… < 1" using probs by auto finally have "0 < ES.prob (space ES.P - ({es ∈ space ES.P. n/2 ≤ short_count (?ug n es)} ∪ {es ∈ space ES.P. 1/2 * n/k ≤ α (?ug n es)}))" (is "0 < ES.prob ?S") by (subst ES.prob_compl) auto also have "?S = {es ∈ space ES.P. short_count (?ug n es) < n/2 ∧ α (?ug n es) < 1/2* n/k}" (is "… = ?C") by (auto simp: not_less rest_compl) finally have "?C ≠ {}" by (intro notI) (simp only:, auto) then obtain es where es_props: "es ∈ space ES.P" "short_count (?ug n es) < n/2" "α (?ug n es) < 1/2 * n/k" by auto ― ‹now we obtained a high colored graph (few independent nodes) with almost no short cycles› define G where "G = ?ug n es" define H where "H = kill_short G k" have G_props: "uverts G = {1..n}" "finite (uverts G)" "short_count G < n/2" "α G < 1/2 * n/k" unfolding G_def using es_props by (auto simp: ES.S_verts_def) have "uwellformed G" by (auto simp: G_def uwellformed_def all_edges_def ES.S_edges_def) with G_props have T1: "uwellformed H" unfolding H_def by (intro kill_short_uwellformed) have "enat l ≤ enat k" using ‹l ≤ k› by simp also have "… < girth H" using G_props by (auto simp: kill_short_large_girth H_def) finally have T2: "l < girth H" . have card_H: "n/2 ≤ card (uverts H)" using G_props es_props kill_short_order_of_graph[of G k] by (simp add: short_count_def H_def) then have uverts_H: "uverts H ≠ {}" "0 < card (uverts H)" by auto then have "0 < α H" using zero_less_α uverts_H by auto have α_HG: "α H ≤ α G" unfolding H_def G_def by (auto intro: kill_short_α) have "enat l ≤ ereal k" using ‹l ≤ k› by auto also have "… < (n/2) / α G" using G_props ‹3 ≤ k› by (cases "α G") (auto simp: field_simps) also have "… ≤ (n/2) / α H" using α_HG ‹0 < α H› by (auto simp: ereal_of_enat_pushout intro!: ereal_divide_left_mono) also have "… ≤ card (uverts H) / α H" using card_H ‹0 < α H› by (auto intro!: ereal_divide_right_mono) also have "… ≤ chromatic_number H" using uverts_H T1 by (intro chromatic_lb) auto finally have T3: "l < chromatic_number H" by (simp del: ereal_of_enat_simps) from T1 T2 T3 show ?thesis by fast qed end