Theory Basic_Bounds_Application
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 𝒱"
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 (∑a∈A. p a) else 0)"
proof (cases "A ⊆ Ω")
case True
then have "finite A" using finite_event by auto
moreover have "ennreal (sum p A) = (∑a∈A. ennreal (p a))"
using sum_ennreal pgte0 True by (simp add: subset_iff Ω_def)
ultimately have "emeasure M A = (∑a∈A. 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: "(∑x∈F 𝒱. 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"
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
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 -
interpret P: vertex_colour_space 𝒱 E 2
by unfold_locales (auto simp add: order_ge_two)
define A where "A ≡(λ e. {f ∈ 𝒞⇧2 . mono_edge f e})"
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
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