Theory Girth_Chromatic
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"
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
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: choose_two 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
define XG where "XG es = {c. ?k_cycle es c k}" for es
define XC where "XC c = {es ∈ space P. ?k_cycle es c k}" for 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
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_right_pos 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 powr_minus divide_simps)
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
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