Theory Girth_Chromatic.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 "(APow 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 (edgesA. 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 (edgesA. 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: "integralL P f = (xPow 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 "(Tcylinder 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 * (Tcylinder 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: 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
    ― ‹@{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)
      =  (xspace P. card (XG x) * prob {x})"
    by (simp add: XG_def integral_finite_singleton space_eq)
  also have " = (cC 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 "(xspace P. card (XG x) * prob {x}) = (xspace P. (c  XG x. prob {x}))"
      by simp
    also have " = (xspace 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 " = (cC 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_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 - {xA. P x} = {xA. ¬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