# Theory Graph_Theory_Preliminaries

```section‹Background material for the graph-theoretic aspects of the main proof›
text ‹This section includes a number of lemmas on project specific definitions for graph theory,
building on the general undirected graph theory library \cite{Undirected_Graph_Theory-AFP} ›

(*
Session: Balog_Szemeredi_Gowers
Title:   Graph_Theory_Preliminaries.thy
Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
Affiliation: University of Cambridge
Date: August 2022.
*)

theory Graph_Theory_Preliminaries
imports
Miscellaneous_Lemmas
Undirected_Graph_Theory.Bipartite_Graphs
Undirected_Graph_Theory.Connectivity
Random_Graph_Subgraph_Threshold.Ugraph_Misc
begin

subsection‹On graphs with loops›

context ulgraph

begin

definition degree_normalized:: "'a ⇒ 'a set ⇒ real" where
"degree_normalized v S ≡ card (neighbors_ss v S) / (card S)"

lemma degree_normalized_le_1: "degree_normalized x S ≤ 1"

proof(cases "finite S")
assume hA: "finite S"
then have "card (neighbors_ss x S) ≤ card S" using neighbors_ss_def card_mono hA
by fastforce
then show ?thesis using degree_normalized_def divide_le_eq_1
by (metis antisym_conv3 of_nat_le_iff of_nat_less_0_iff)
next
case False
then show ?thesis using degree_normalized_def by auto
qed

end

subsection‹On bipartite graphs ›

context bipartite_graph
begin

(* codegree counts the number of paths between two vertices, including loops *)
definition codegree:: "'a ⇒ 'a ⇒ nat" where
"codegree v u ≡ card {x ∈ V . vert_adj v x ∧ vert_adj u x}"

lemma codegree_neighbors: "codegree v u = card (neighborhood v ∩ neighborhood u)"
unfolding codegree_def neighborhood_def

proof -
have "{x ∈ V. vert_adj v x ∧ vert_adj u x} = {va ∈ V. vert_adj v va} ∩ {v ∈ V. vert_adj u v}"
by blast
thus "card {x ∈ V. vert_adj v x ∧ vert_adj u x} = card ({va ∈ V. vert_adj v va} ∩ {v ∈ V. vert_adj u v})"
by auto
qed

lemma codegree_sym: "codegree v u = codegree u v"

definition codegree_normalized:: "'a ⇒ 'a ⇒ 'a set ⇒ real" where
"codegree_normalized v u S ≡ codegree v u / card S"

lemma codegree_normalized_altX:
assumes "x ∈ X" and "x' ∈ X"
shows "codegree_normalized x x' Y = card (neighbors_ss x Y ∩ neighbors_ss x' Y) / card Y"

proof -
have "((neighbors_ss x Y) ∩ (neighbors_ss x' Y)) = neighborhood x ∩ neighborhood x'"
using neighbors_ss_eq_neighborhoodX assms by auto
then show ?thesis unfolding codegree_normalized_def
using codegree_def codegree_neighbors by presburger
qed

lemma codegree_normalized_altY:
assumes "y ∈ Y" and "y' ∈ Y"
shows "codegree_normalized y y' X = card (neighbors_ss y X ∩ neighbors_ss y' X) / card X"

proof -
have "neighbors_ss y X ∩ neighbors_ss y' X = neighborhood y ∩ neighborhood y'"
using neighbors_ss_eq_neighborhoodY assms by auto
then show ?thesis unfolding codegree_normalized_def
using codegree_def codegree_neighbors by presburger
qed

lemma codegree_normalized_sym: "codegree_normalized u v S = codegree_normalized v u S"
unfolding codegree_normalized_def using codegree_sym by simp

definition bad_pair:: " 'a ⇒ 'a ⇒ 'a set ⇒ real ⇒ bool" where
"bad_pair v u S c ≡ codegree_normalized v u S < c"

assumes "bad_pair v u S c" shows "bad_pair u v S c"

definition bad_pair_set:: "'a set ⇒ 'a set ⇒ real ⇒ ('a × 'a) set" where
"bad_pair_set S T c  ≡ {(u, v) ∈ S × S. bad_pair u v T c}"

"bad_pair_set S T c = Set.filter (λ p . bad_pair (fst p) (snd p) T c) (S × S)"

assumes "finite S"
shows "finite (bad_pair_set S T c)"
proof -
have "finite (S × S)" using finite_cartesian_product assms by blast
thus ?thesis using bad_pair_set_filter_alt finite_filter by auto
qed

lemma codegree_is_path_length_two:
"codegree x x' = card {p . connecting_path x x' p ∧ walk_length p = 2}"
unfolding codegree_def
proof-
define f:: "'a list ⇒ 'a" where "f = (λ p. p!1)"
have f_inj: "inj_on f {p . connecting_path x x' p ∧ walk_length p = 2}"
unfolding f_def
proof (intro inj_onI, simp del: One_nat_def)
fix a b assume ha: "connecting_path x x' a ∧ walk_length a = 2" and
hb: "connecting_path x x' b ∧ walk_length b = 2" and 1: "a!1 = b!1"
then have len: "length a = 3" "length b = 3" using walk_length_conv by auto
show "a = b" using list2_middle_singleton 1 len list_middle_eq ha hb connecting_path_def len by metis
qed
have f_image: "f ` {p . connecting_path x x' p ∧ walk_length p = 2} =
proof(intro subset_antisym)
show "f ` {p. connecting_path x x' p ∧ walk_length p = 2}
proof (intro subsetI)
fix a assume "a ∈ f ` {p. connecting_path x x' p ∧ walk_length p = 2}"
then obtain p where ha: "p!1 = a" and hp: "connecting_path x x' p" and hpl: "length p = 3"
using f_def walk_length_conv by auto
have "p ! 0 = x" using hd_conv_nth[of p] hpl hp connecting_path_def by fastforce
then have va1: "vert_adj x a" using is_walk_index[of 0 p] hp connecting_path_def is_gen_path_def
have "p ! 2 = x'" using last_conv_nth[of p] hpl hp connecting_path_def by fastforce
then have "vert_adj a x'" using is_walk_index[of 1 p] hp connecting_path_def is_gen_path_def
then show "a ∈ {a ∈ V. vert_adj x a ∧ vert_adj x' a}"
qed
⊆ f ` {p. connecting_path x x' p ∧ walk_length p = 2}"
proof (intro subsetI)
fix a assume ha: "a ∈ {xa ∈ V. vert_adj x xa ∧ vert_adj x' xa}"
then have "a ∈ V" and "x ∈ V" and "x' ∈ V" and "vert_adj x a" and "vert_adj x' a"
then have "is_gen_path [x, a, x']"
using is_walk_def vert_adj_def vert_adj_sym ha singleton_not_edge is_gen_path_def by auto (* Slow *)
then have "connecting_path x x' [x, a, x']"
unfolding connecting_path_def vert_adj_def hd_conv_nth last_conv_nth by simp
moreover have "walk_length [x, a, x'] = 2" using walk_length_conv by simp
ultimately show "a ∈ f ` {p. connecting_path x x' p ∧ walk_length p = 2}" using f_def by force
qed
qed
then show "card {xa ∈ V. vert_adj x xa ∧ vert_adj x' xa} =
card {p. connecting_path x x' p ∧ walk_length p = 2}"
using f_inj card_image by fastforce
qed

lemma codegree_bipartite_eq:
"∀ x ∈ X. ∀ x' ∈ X. codegree x x' = card {y ∈ Y. vert_adj x y ∧ vert_adj x' y}"
by (metis (no_types, lifting) Collect_cong)

lemma (in fin_bipartite_graph) bipartite_deg_square_eq:
"∀ y ∈ Y. (∑ x' ∈ X. ∑ x ∈ X. indicator {z. vert_adj x z ∧ vert_adj x' z} y) = (degree y)^2"
proof
have hX: "finite X" by (simp add: partitions_finite(1))
fix y assume hy: "y ∈ Y"
have 1: "∀ x' ∈ X. ∀ x ∈ X. indicator {z. vert_adj x z ∧ vert_adj x' z} y =
by (metis (mono_tags, lifting) Int_Collect indicator_simps(1) indicator_simps(2) mem_Collect_eq)
have 2: "∀ x' ∈ X. ∀ x ∈ X. (indicator ({z. vert_adj x' z} ∩ {z. vert_adj x z}) y:: nat) =
indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y" using indicator_inter_arith
by auto
have "(∑ x' ∈ X. ∑ x ∈ X. (indicator {z. vert_adj x z ∧ vert_adj x' z} y:: nat)) =
(∑ x' ∈ X. ∑ x ∈ X. indicator ({z. vert_adj x' z} ∩ {z. vert_adj x z}) y)"
using 1 sum.cong by (metis (no_types, lifting))
also have "... = (∑ x' ∈ X. ∑ x ∈ X. indicator {z. vert_adj x' z} y *
indicator {z. vert_adj x z} y)" using 2 sum.cong by auto
also have "... = sum (λ x. indicator {z. vert_adj x z} y) X * sum (λ x. indicator {z. vert_adj x z} y) X"
using sum_product[of "(λ x. (indicator {z. vert_adj x z} y:: nat))" "X"
"(λ x. indicator {z. vert_adj x z} y)" "X"] by auto
finally have 3: "(∑ x' ∈ X. ∑ x ∈ X. (indicator {z. vert_adj x z ∧ vert_adj x' z} y:: nat)) =
(sum (λ x. indicator {z. vert_adj x z} y) X) ^ 2" using power2_eq_square
by (metis (no_types, lifting))
have "∀ x ∈ X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x"
from this have "(sum (λ x. indicator {z. vert_adj x z} y) X) = sum (λ x. indicator {x. vert_adj x y} x) X"
using sum.cong by fastforce
also have "... = card ({x ∈ X. vert_adj x y})" using sum_indicator_eq_card hX
by (metis Collect_conj_eq Collect_mem_eq)
finally show "(∑x'∈X. ∑x∈X. indicator {z. vert_adj x z ∧ vert_adj x' z} y) = (degree y)^2"
using 3 hy degree_neighbors_ssY neighbors_ss_def vert_adj_sym by presburger
qed

lemma (in fin_bipartite_graph) codegree_degree:
"(∑ x' ∈ X. ∑ x ∈ X. (codegree x x')) = (∑ y ∈ Y. (degree y)^2)"

proof-
have hX: "finite X" and hY: "finite Y"
have "∀ x' ∈ X. ∀ x ∈ X. {z ∈ V. vert_adj x z ∧ vert_adj x' z} = Y ∩ {z. vert_adj x z ∧ vert_adj x' z}"
from this have "(∑ x' ∈ X. ∑ x ∈ X. (codegree x x')) = (∑ x' ∈ X. ∑ x ∈ X. card (Y ∩ {z. vert_adj x z ∧ vert_adj x' z}))"
using codegree_def sum.cong by auto
also have "... = (∑ x' ∈ X. ∑ x ∈ X. ∑ y ∈ Y. indicator {z. vert_adj x z ∧ vert_adj x' z} y)"
using sum_indicator_eq_card hY by fastforce
also have "... =  (∑ x' ∈ X. ∑ y ∈ Y. (∑ x ∈ X. indicator {z. vert_adj x z ∧ vert_adj x' z} y))"
using sum.swap by (metis (no_types))
also have "... = (∑ y ∈ Y. ∑ x' ∈ X. (∑ x ∈ X. indicator {z. vert_adj x z ∧ vert_adj x' z} y))"
using sum.swap by fastforce
also have "... = (∑ y ∈ Y. (degree y)^2)" using bipartite_deg_square_eq sum.cong by force
finally show ?thesis by simp
qed

lemma (in fin_bipartite_graph) sum_degree_normalized_X_density:
"(∑ x ∈ X. degree_normalized x Y) / card X = edge_density X Y"
by (smt (z3) card_all_edges_betw_neighbor card_edges_between_set degree_normalized_def
divide_divide_eq_left' density_simp of_nat_mult of_nat_sum partitions_finite(1)
partitions_finite(2) sum.cong sum_left_div_distrib)

lemma (in fin_bipartite_graph) sum_degree_normalized_Y_density:
"(∑ y ∈ Y. degree_normalized y X) / card Y = edge_density X Y"
using bipartite_sym fin_bipartite_graph.sum_degree_normalized_X_density fin_bipartite_graph_def
fin_graph_system_axioms edge_density_commute by fastforce

end
end```