# 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:

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 -
by blast
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:
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
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. xX. 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