Theory Basic_Bounds_Application

(* Theory: Basic_Bounds_Application.thy
   Author: Chelsea Edmonds
*)

section ‹Basic Probabilistic Method Application›
text ‹This section establishes step (1) of the basic framework for incidence set systems, 
as well as some basic bounds on hypergraph colourings ›
theory Basic_Bounds_Application imports "Lovasz_Local.Basic_Method" Hypergraph_Colourings
begin

subsection ‹Probability Spaces for Incidence Set Systems ›
text ‹This is effectively step (1) of the formal framework for probabilistic method. Unlike stages (3) 
and (4), which were formalised in the Lovasz\_Local\_Lemma AFP entry, this stage required a 
formalisation of incidence set systems as well as the background probability space locales ›

text ‹A basic probability space for a point measure on a non-trivial structure ›
locale vertex_fn_space = fin_hypersystem_vne +
  fixes F :: "'a set  'b set"
  fixes p :: "'b  real"
  assumes ne: "F 𝒱  {}"
  assumes fin: "finite (F 𝒱)"
  assumes pgte0: " fv . fv  F 𝒱  p fv  0"
  assumes sump: "(x  (F 𝒱) . p x) = 1"
begin

definition "Ω  F 𝒱" (* model space *)

lemma fin_Ω: "finite Ω"
  unfolding Ω_def using fin by auto

lemma ne_Ω: "Ω  {}"
  unfolding Ω_def using ne by simp

definition "M = point_measure Ω p"

lemma space_eq: "space M = Ω"
  unfolding M_def Ω_def by (simp add: space_point_measure)

lemma sets_eq: "sets M =  Pow (Ω)"
  unfolding M_def by (simp add: sets_point_measure)

lemma finite_event: "A  Ω  finite A"
  by (simp add: finite_subset fin_Ω)

lemma emeasure_eq: "emeasure M A = (if (A  Ω) then (aA. p a) else 0)"
proof (cases "A  Ω")
  case True
  then have "finite A" using finite_event by auto
  moreover have "ennreal (sum p A) = (aA. ennreal (p a))" 
    using sum_ennreal pgte0 True by (simp add: subset_iff Ω_def) 
  ultimately have "emeasure M A = (aA. p a)" 
    using emeasure_point_measure_finite2[of A Ω p] M_def
    using True by presburger 
  then show ?thesis using True by auto
next
  case False
  then show ?thesis using emeasure_notin_sets sets_eq by auto
qed

lemma integrable_M[intro, simp]: "integrable M (f::_  real)"
  using fin_Ω by (simp add: integrable_point_measure_finite M_def)

lemma borel_measurable_M[measurable]: "f  borel_measurable M"
  unfolding M_def by simp

lemma prob_space_M: "prob_space M"
  unfolding M_def using fin_Ω ne_Ω pgte0 sump Ω_def
  by (intro prob_space_point_measure) (simp_all)

end

sublocale vertex_fn_space  prob_space M
  using prob_space_M .

text ‹A uniform variation of the space ›
locale vertex_fn_space_uniform = fin_hypersystem_vne +
  fixes F :: "'a set  'b set"
  assumes ne: "F 𝒱  {}"
  assumes fin: "finite (F 𝒱)"
begin

definition "ΩU  F 𝒱"

definition "MU  uniform_count_measure ΩU"

end

sublocale vertex_fn_space_uniform  vertex_fn_space 𝒱 E F "(λx. 1 / card ΩU)"
  rewrites  "Ω = ΩU" and "M = MU"
proof (unfold_locales )
  show 1: "F 𝒱  {}" and 2: "finite (F 𝒱)" by (simp_all add: fin ne)
  show 3: "fv. fv  F 𝒱  0  1 / real (card (ΩU))" by auto
  show 4: "(xF 𝒱. 1 / real (card ΩU)) = 1"
    using sum_constant ne fin ΩU_def by auto
  interpret vf: vertex_fn_space 𝒱 E F "(λx. 1 / card (ΩU))"
    using 1 2 3 4 by (unfold_locales)
  show "vf.Ω = ΩU" unfolding vf.Ω_def ΩU_def by simp
  show "vf.M = MU"  unfolding vf.M_def vf.Ω_def MU_def uniform_count_measure_def using ΩU_def by auto
qed

context vertex_fn_space_uniform
begin

lemma emeasure_eq: "emeasure MU A = (if (A  ΩU) then ((card A)/card (ΩU)) else 0)"
  using fin_Ω MU_def emeasure_uniform_count_measure[of "ΩU" "A"]
    sets_uniform_count_measure emeasure_notin_sets Pow_iff ennreal_0 by (metis (full_types))

lemma measure_eq_valid: "A  events  measure MU A = (card A)/card (ΩU)"
  using sets_eq by (simp add: MU_def ΩU_def fin measure_uniform_count_measure) 

lemma expectation_eq:
  shows "expectation f = ( x  ΩU. f x) / card ΩU"
proof-
  have "(a. a  ΩU  0  1 / real (card ΩU))"
    using fin_Ω ne_Ω by auto
  moreover have " a. aΩU  (1 / real (card ΩU)) *R f a = 1 / (card ΩU) * f a"
    using real_scaleR_def by simp
  ultimately have "expectation f = ( x  ΩU. f x * (1 / (card ΩU)))" 
    using uniform_count_measure_def[of ΩU] lebesgue_integral_point_measure_finite[of ΩU "(λ x. 1 / card ΩU)" "f"] 
      MU_def fin_Ω by auto
  then show ?thesis using sum_distrib_right[symmetric, of f "1 / (card ΩU)" ΩU] by auto
qed

end

text ‹A probability space over the full vertex set ›
locale vertex_space = fin_hypersystem_vne +
  fixes p :: "'a  real"
  assumes pgte0: " fv . fv  𝒱  p fv  0"
  assumes sump: "(x  (𝒱) . p x) = 1"


sublocale vertex_space  vertex_fn_space 𝒱 E "λ i . i" p
  rewrites "Ω = 𝒱"
proof (unfold_locales)
  interpret vertex_fn_space 𝒱 E "λ i . i" p
    by unfold_locales (simp_all add: pgte0 sump V_nempty finite_sets)
  show "Ω = 𝒱"
    using Ω_def by simp
qed (simp_all add: pgte0 sump V_nempty finite_sets)

text ‹A uniform variation of the probability space over the vertex set ›
locale vertex_space_uniform = fin_hypersystem_vne

sublocale vertex_space_uniform  vertex_fn_space_uniform 𝒱 E "λ i . i"
  rewrites "ΩU = 𝒱"
proof (unfold_locales)
 interpret vertex_fn_space_uniform 𝒱 E "λ i . i"
   by unfold_locales (simp_all add: V_nempty finite_sets)
  show "ΩU = 𝒱" unfolding ΩU_def by simp
qed (simp_all add: V_nempty finite_sets)

text ‹A uniform probability space over a vertex subset ›
locale vertex_ss_space_uniform = fin_hypersystem_vne + 
  fixes VS 
  assumes vs_ss: "VS  𝒱"
  assumes ne_vs: "VS  {}"
begin

lemma finite_vs: "finite VS"
  using vs_ss finite_subset finite_sets by auto

end

sublocale vertex_ss_space_uniform  vertex_fn_space_uniform 𝒱 E "λ i. VS"
  rewrites "Ω = VS" 
proof (unfold_locales)
  interpret vertex_fn_space_uniform 𝒱 E "λ i . VS" 
    by unfold_locales (simp_all add: ne_vs finite_vs)
  show "Ω = VS"
    using Ω_def by simp
qed (simp_all add: ne_vs finite_vs)

text ‹A non-uniform prob space over a vertex subset ›
locale vertex_ss_space = fin_hypersystem_vne +
  fixes VS
  assumes vs_ss: "VS  𝒱"
  assumes ne_vs: "VS  {}"
  fixes p :: "'a  real"
  assumes pgte0: " fv . fv  VS  p fv  0"
  assumes sump: "(x  (VS) . p x) = 1"
begin

lemma finite_vs: "finite VS"
  using vs_ss finite_subset finite_sets by auto

end

sublocale vertex_ss_space  vertex_fn_space 𝒱 E "λ i . VS" p
  rewrites "Ω = VS"
proof (unfold_locales)
  interpret vertex_fn_space 𝒱 E "λ i . VS" p
    by unfold_locales (simp_all add: pgte0 sump ne_vs finite_vs)
  show "Ω = VS"
    using Ω_def by simp
qed (simp_all add: pgte0 sump ne_vs finite_vs)

text ‹A uniform probability space over a property on the vertex set ›
locale vertex_prop_space = fin_hypersystem_vne + 
  fixes P :: "'b set" (* property *)
  assumes finP: "finite P"
  assumes nempty_P: "P  {}"

sublocale vertex_prop_space  vertex_fn_space_uniform 𝒱 E "λ V. V E P"
rewrites "ΩU = 𝒱 E P" 
proof -
  interpret vertex_fn_space_uniform 𝒱 E "λ V. V E P"
  proof (unfold_locales)
    show "𝒱 E P  {}" using finP V_nempty PiE_eq_empty_iff nempty_P by meson
    show "finite (𝒱 E P)" using finP finite_PiE finite_sets by meson
  qed 
  show "vertex_fn_space_uniform 𝒱 E (λV. V E P)" by unfold_locales
  show "ΩU = 𝒱 E P "unfolding ΩU_def by simp
qed

context vertex_prop_space
begin

lemma prob_uniform_vertex_subset: 
  assumes "b  P"
  assumes "d  𝒱"
  shows "prob  {f  Ω . ( v  d .f v = b)} = 1/((card P) powi (card d))"
  using finP nempty_P V_nempty finite_sets MU_def ΩU_def
  by (simp add: assms(1) assms(2) prob_uniform_ex_fun_space) 

lemma prob_uniform_vertex: 
  assumes "b  P"
  assumes "v  𝒱"
  shows "prob  {f  ΩU . f v = b} = 1/(card P)"
proof -
  have "prob {f  ΩU . f v = b} = card {f  ΩU . f v = b}/card ΩU"
    using measure_eq_valid sets_eq by auto
  then show ?thesis 
    using card_PiE_val_indiv_eq[of "𝒱" b P v] Ω_def finite_sets finP nempty_P assms by auto
qed

end

text ‹A uniform vertex colouring space ›
locale vertex_colour_space = fin_hypergraph_nt +
  fixes n :: nat (*Number of colours *)
  assumes n_lt_order: "n  horder"
  assumes n_not_zero: "n  0"


sublocale vertex_colour_space  vertex_prop_space 𝒱 E "{0..<n}"
  rewrites "ΩU = 𝒞⇧n" 
proof -
  have "{0..<n}  {}" using n_not_zero by simp
  then interpret vertex_prop_space 𝒱 E "{0..<n}"
    by (unfold_locales) (simp_all)
  show "vertex_prop_space 𝒱 E {0..<n}" by (unfold_locales)
  show "ΩU = 𝒞⇧n"
    using Ω_def all_n_vertex_colourings_alt by auto
qed

text ‹This probability space contains several useful lemmas on basic vertex colouring probabilities
(and monochromatic edges), which are facts that are typically either not proven, or have very short
proofs on paper ›
context vertex_colour_space
begin

lemma colour_set_event: "{f  𝒞⇧n. mono_edge_col f e c}  events"
  using sets_eq by simp

lemma colour_functions_event: "(λ c. {f  𝒞⇧n . mono_edge_col f e c}) ` {0..<n}  events"
  using sets_eq by blast

lemma prob_vertex_colour: "v  𝒱  c  {0..<n}  prob {f  𝒞⇧n . f v = c} = 1/n"
  using prob_uniform_vertex by simp

lemma prob_edge_colour: 
  assumes "e ∈# E" "c  {0..<n}"
  shows "prob {f  𝒞⇧n . mono_edge_col f e c} = 1/(n powi (card e))"
proof -
  have "card {0..<n} = n" by simp
  moreover have "𝒞⇧n = 𝒱 E {0..<n}" using all_n_vertex_colourings_alt by blast
  moreover have "{0..<n}  {}" using n_not_zero by simp
  ultimately show ?thesis using prob_uniform_ex_fun_space[of 𝒱 _ "{0..<n}" e] n_not_zero 
      finite_sets wellformed assms by (simp add: MU_def V_nempty mono_edge_col_def)
qed

lemma prob_monochromatic_edge_inv: 
  assumes "e ∈# E"
  shows "prob{f  𝒞⇧n . mono_edge f e} = 1/(n powi (int (card e) - 1))"
proof -
  have "finite {0..<n}"by auto
  then have "prob {f  𝒞⇧n . mono_edge f e} = (c  {0..<n} . prob {f  𝒞⇧n . mono_edge_col f e c})"
    using finite_measure_finite_Union[of "{0..<n}" "(λ c . {f  𝒞⇧n .  mono_edge_col f e c})" ] 
      disjoint_family_on_colourings colour_functions_event mono_edge_set_union assms by auto
  also have "... = n/(n powi (int (card e)))" using prob_edge_colour assms by simp
  also have "... = n/(n* (n powi ((int (card e)) - 1)))" using n_not_zero 
      power_int_commutes power_int_minus_mult by (metis of_nat_0_eq_iff) 
  finally show ?thesis using n_not_zero by simp 
qed

lemma prob_monochromatic_edge: 
  assumes "e ∈# E"
  shows "prob{f  𝒞⇧n . mono_edge f e} = n powi (1 - int (card e))"
  using prob_monochromatic_edge_inv assms n_not_zero by (simp add: power_int_diff) 

lemma prob_monochromatic_edge_bound: 
  assumes "e ∈# E"
  assumes " e. e ∈#E  card e  k"
  assumes "k > 0"
  shows "prob{f  𝒞⇧n . mono_edge f e}  1/((real n) powi (k-1))" 
proof -
  have "(int (card (e)) - 1)  k - 1" using assms(3) assms(1)
    using assms(2) int_ops(6) of_nat_0_less_iff of_nat_mono by fastforce
  then have "((n :: real) powi (int (card (e)) - 1))  (n powi (k - 1))" 
    using power_int_increasing[of "k - 1" "(int (card (e)) - 1)" n] n_not_zero by linarith 
  moreover have "prob({f  𝒞⇧n . mono_edge f e}) = 1/(n powi (int (card (e)) - 1))"
    using prob_monochromatic_edge_inv assms(1) by simp
  ultimately show ?thesis using frac_le zero_less_power_int n_not_zero 
    by (smt (verit) less_imp_of_nat_less of_nat_0_eq_iff of_nat_0_le_iff of_nat_1 of_nat_diff zle_int)
qed

end

subsection ‹More Hypergraph Colouring Results ›

context fin_hypergraph_nt
begin

lemma not_proper_colouring_edge_mono: "{f  𝒞⇧n . ¬ is_proper_colouring f n} = (e  (set_mset E). {f  𝒞⇧n . mono_edge f e})"
proof -
  have "{f  𝒞⇧n . ¬ is_proper_colouring f n} = {f  𝒞⇧n .  e  set_mset E . mono_edge f e}"
    using ex_monochomatic_not_colouring no_monochomatic_is_colouring 
    by (metis (mono_tags, lifting) all_n_vertex_colourings_alt)
  then show ?thesis using Union_exists by simp
qed

lemma proper_colouring_edge_mono: "{f  𝒞⇧n . is_proper_colouring f n} = (e  (set_mset E). {f  𝒞⇧n . ¬ mono_edge f e})"
proof -
  have "{f  𝒞⇧n . is_proper_colouring f n} = {f  𝒞⇧n .  e  set_mset E . ¬ mono_edge f e}"
    using is_proper_colouring_alt2 all_n_vertex_colourings_alt by auto
  moreover have "set_mset E  {}" using E_nempty by simp
  ultimately show ?thesis using Inter_forall by auto
qed

lemma proper_colouring_edge_mono_compl: "{f  𝒞⇧n . is_proper_colouring f n} = (e  (set_mset E). 𝒞⇧n - {f  𝒞⇧n . mono_edge f e})"
  using proper_colouring_edge_mono by auto

lemma event_is_proper_colouring: 
  assumes "g  𝒞⇧n"
  assumes "g (e  (set_mset E). {f  𝒞⇧n . mono_edge f e})"
  shows "is_proper_colouring g n"
proof -
  have " e. e ∈# E  ¬ mono_edge g e" using assms
    by blast
  then show ?thesis using assms(1) all_n_vertex_colourings_def by (auto)
qed


end

subsection ‹The Basic Application ›
text ‹The comments below show the basic framework steps ›

context fin_kuniform_hypergraph_nt
begin
proposition erdos_propertyB:  
  assumes "size E < (2^(k - 1))"
  assumes "k > 0"
  shows "has_property_B"
proof -
  ― ‹(1) Set up the probability space: "Colour V randomly with two colours" ›
  interpret P: vertex_colour_space 𝒱 E 2 
    by unfold_locales (auto simp add: order_ge_two)
  ― ‹(2) define the event to avoid - monochromatic edges ›
  define A where "A (λ e. {f  𝒞⇧2 . mono_edge f e})"
  ― ‹(3) Calculation 2: Have Pr (of Ae for any e) \le Sum over e (Pr (A e)) < 1 ›
  have "(e  set_mset E. P.prob (A e)) < 1"
  proof -
    have "2 powi (int k - 1) = real (2 ^ (k - 1))"
      by (simp add: k > 0 power_int_def)
    then
    have "card (set_mset E) < 2 powi (int k - 1)" 
      using card_size_set_mset[of E] assms by linarith
    then have "(e  (set_mset E). P.prob (A e)) < 2 powi (int k - 1) * 2 powi (1 - int k)"
      unfolding A_def using P.prob_monochromatic_edge uniform assms(1) by simp
    moreover have "((2 :: real) powi ((int k) - 1)) * (2 powi (1 - (int k))) = 1" 
      using power_int_add[of 2 "int k - 1" "1- int k"] by force 
    ultimately show ?thesis using power_int_add[of 2 "int k - 1" "1- int k"] by simp
  qed
  moreover have "A ` (set_mset E)  P.events" unfolding A_def P.sets_eq by blast
  ― ‹(4) obtain a colouring avoiding bad events ›
  ultimately obtain f where "f  𝒞⇧2" and "f  (A `(set_mset E))" 
    using P.Union_bound_obtain_fun[of "set_mset E" A] finite_set_mset P.space_eq by auto 
  thus ?thesis using event_is_proper_colouring A_def is_n_colourable_def by auto 
qed

end

corollary erdos_propertyB_min: 
  fixes z :: "'a itself"
  assumes "n > 0"
  shows "(min_edges_colouring n z)  2^(n - 1)"      
proof (rule ccontr)
  assume "¬ 2 ^ (n - 1)  min_edges_colouring n z"
  then have "min_edges_colouring n z < 2^(n - 1)" by simp
  then obtain h :: "'a hyp_graph" where hin: " h  not_col_n_uni_hyps n" and 
    "enat (size (hyp_edges h)) < 2^(n-1)"
    using obtains_min_edge_colouring by blast 
  then have lt: " size (hyp_edges h) < 2^(n -1)"
    by (metis of_nat_eq_enat of_nat_less_imp_less of_nat_numeral of_nat_power)  
  then interpret kuf: fin_kuniform_hypergraph_nt "(hyp_verts h)" "hyp_edges h" n 
    using not_col_n_uni_hyps_def hin by auto 
  have "kuf.has_property_B" using kuf.erdos_propertyB lt assms by simp
  then show False using hin not_col_n_uni_hyps_def by auto 
qed

end