# Theory Expander_Graphs_Definition

section ‹Definitions\label{sec:definitions}›

text ‹This section introduces regular graphs as a sublocale in the graph theory developed by
Lars Noschinski~\cite{Graph_Theory-AFP} and introduces various expansion coefficients.›

theory Expander_Graphs_Definition
imports
Graph_Theory.Digraph_Isomorphism
"HOL-Analysis.L2_Norm"
Extra_Congruence_Method
Expander_Graphs_Multiset_Extras
Jordan_Normal_Form.Conjugate
Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
begin

unbundle intro_cong_syntax

definition arcs_betw where "arcs_betw G u v = {a. a ∈ arcs G ∧ head G a = v ∧ tail G a = u}"

text ‹The following is a stronger notion than the notion of symmetry defined in
@{theory "Graph_Theory.Digraph"}, it requires that the number of edges from @{term "v"} to
@{term "w"} must be equal to the number of edges from @{term "w"} to @{term "v"} for any pair of
vertices @{term "v"} @{term "w ∈ verts G"}.›

definition symmetric_multi_graph where "symmetric_multi_graph G =
(fin_digraph G ∧ (∀v w. {v, w} ⊆ verts G ⟶ card (arcs_betw G w v) = card (arcs_betw G v w)))"

lemma symmetric_multi_graphI:
assumes "fin_digraph G"
assumes "bij_betw f (arcs G) (arcs G)"
assumes "⋀e. e ∈ arcs G ⟹ head G (f e) = tail G e ∧ tail G (f e) = head G e"
shows "symmetric_multi_graph G"
proof -
have "card (arcs_betw G w v) = card (arcs_betw G v w)"
(is "?L = ?R") if "v ∈ verts G" "w ∈ verts G" for v w
proof -
have a:"f x ∈ arcs G" if "x ∈ arcs G" for x
using assms(2) that unfolding bij_betw_def by auto
have b:"∃y. y ∈ arcs G ∧ f y = x" if "x ∈ arcs G" for x
using bij_betw_imp_surj_on[OF assms(2)] that by force

have "inj_on f (arcs G)"
using assms(2) unfolding bij_betw_def by simp
hence "inj_on f {e ∈ arcs G. head G e = v ∧ tail G e = w}"
by (rule inj_on_subset, auto)
hence "?L = card (f  {e ∈ arcs G. head G e = v ∧ tail G e = w})"
unfolding arcs_betw_def
by (intro card_image[symmetric])
also have "... = ?R"
unfolding arcs_betw_def using a b assms(3)
by (intro arg_cong[where f="card"] order_antisym image_subsetI subsetI) fastforce+
finally show ?thesis by simp
qed
thus ?thesis
using assms(1) unfolding symmetric_multi_graph_def by simp
qed

lemma symmetric_multi_graphD2:
assumes "symmetric_multi_graph G"
shows "fin_digraph G"
using assms unfolding symmetric_multi_graph_def by simp

lemma symmetric_multi_graphD:
assumes "symmetric_multi_graph G"
shows "card {e ∈ arcs G. head G e=v ∧ tail G e=w} = card {e ∈ arcs G. head G e=w ∧ tail G e=v}"
(is "card ?L = card ?R")
proof (cases "v ∈ verts G ∧ w ∈ verts G")
case True
then show ?thesis
using assms unfolding symmetric_multi_graph_def arcs_betw_def by simp
next
case False
interpret fin_digraph G
using symmetric_multi_graphD2[OF assms(1)] by simp
have 0:"?L = {}" "?R = {}"
using False wellformed by auto
show ?thesis unfolding 0 by simp
qed

lemma symmetric_multi_graphD3:
assumes "symmetric_multi_graph G"
shows
"card {e∈arcs G. tail G e=v ∧ head G e=w}=card {e∈arcs G. tail G e=w∧head G e=v}"
using symmetric_multi_graphD[OF assms] by (simp add:conj.commute)

lemma symmetric_multi_graphD4:
assumes "symmetric_multi_graph G"
shows "card (arcs_betw G v w) = card (arcs_betw G w v)"
using symmetric_multi_graphD[OF assms] unfolding arcs_betw_def by simp

lemma symmetric_degree_eq:
assumes "symmetric_multi_graph G"
assumes "v ∈ verts G"
shows "out_degree G v = in_degree G v" (is "?L = ?R")
proof -
interpret fin_digraph "G"
using assms(1) symmetric_multi_graph_def by auto

have "?L = card {e ∈ arcs G. tail G e = v}"
unfolding out_degree_def out_arcs_def by simp
also have "... = card (⋃w ∈ verts G. {e ∈ arcs G. head G e = w ∧ tail G e = v})"
by (intro arg_cong[where f="card"]) (auto simp add:set_eq_iff)
also have "... = (∑w ∈ verts G. card {e ∈ arcs G. head G e = w ∧ tail G e = v})"
by (intro card_UN_disjoint) auto
also have "... = (∑w ∈ verts G. card {e ∈ arcs G. head G e = v ∧ tail G e = w})"
by (intro sum.cong refl symmetric_multi_graphD assms)
also have "... = card (⋃w ∈ verts G. {e ∈ arcs G. head G e = v ∧ tail G e = w})"
by (intro card_UN_disjoint[symmetric]) auto
also have "... = card (in_arcs G v)"
by (intro arg_cong[where f="card"]) (auto simp add:set_eq_iff)
also have "... = ?R"
unfolding in_degree_def by simp
finally show ?thesis by simp
qed

definition edges where "edges G = image_mset (arc_to_ends G) (mset_set (arcs G))"

lemma (in fin_digraph) count_edges:
"count (edges G) (u,v) = card (arcs_betw G u v)" (is "?L = ?R")
proof -
have "?L = card {x ∈ arcs G. arc_to_ends G x = (u, v)}"
unfolding edges_def count_mset_exp image_mset_filter_mset_swap[symmetric] by simp
also have "... = ?R"
unfolding arcs_betw_def arc_to_ends_def
by (intro arg_cong[where f="card"]) auto
finally show ?thesis by simp
qed

lemma (in fin_digraph) count_edges_sym:
assumes "symmetric_multi_graph G"
shows "count (edges G) (v, w) = count (edges G) (w, v)"
unfolding count_edges using symmetric_multi_graphD4[OF assms]  by simp

lemma (in fin_digraph) edges_sym:
assumes "symmetric_multi_graph G"
shows "{# (y,x). (x,y) ∈# (edges G) #} = edges G"
proof -
have "count {#(y, x). (x, y) ∈# edges G#} x = count (edges G) x" (is "?L = ?R") for x
proof -
have "?L = count (edges G) (snd x, fst x)"
unfolding count_mset_exp
by (simp add:image_mset_filter_mset_swap[symmetric] case_prod_beta prod_eq_iff ac_simps)
also have "... = count (edges G) (fst x, snd x)"
unfolding count_edges_sym[OF assms] by simp
also have "... = count (edges G) x" by simp
finally show ?thesis by simp
qed

thus ?thesis
by (intro multiset_eqI) simp
qed

definition "vertices_from G v = {# snd e | e ∈# edges G. fst e = v #}"
definition "vertices_to G v = {# fst e | e ∈# edges G. snd e = v #}"

context fin_digraph
begin

lemma edge_set:
assumes "x ∈# edges G"
shows "fst x ∈ verts G" "snd x ∈ verts G"
using assms unfolding edges_def arc_to_ends_def by auto

lemma  verts_from_alt:
"vertices_from G v = image_mset (head G) (mset_set (out_arcs G v))"
proof -
have "{#x ∈# mset_set (arcs G). tail G x = v#} = mset_set {a ∈ arcs G. tail G a = v}"
by (intro filter_mset_mset_set) simp
thus ?thesis
unfolding vertices_from_def out_arcs_def edges_def arc_to_ends_def
qed

lemma verts_to_alt:
"vertices_to G v = image_mset (tail G) (mset_set (in_arcs G v))"
proof -
have "{#x ∈# mset_set (arcs G). head G x = v#} = mset_set {a ∈ arcs G. head G a = v}"
by (intro filter_mset_mset_set) simp
thus ?thesis
unfolding vertices_to_def in_arcs_def edges_def arc_to_ends_def
qed

lemma set_mset_vertices_from:
"set_mset (vertices_from G x) ⊆ verts G"
unfolding vertices_from_def using edge_set by auto

lemma set_mset_vertices_to:
"set_mset (vertices_to G x) ⊆ verts G"
unfolding vertices_to_def using edge_set by auto

end

text ‹A symmetric multigraph is regular if every node has the same degree. This is the context
in which the expansion conditions are introduced.›

locale regular_graph = fin_digraph +
assumes sym: "symmetric_multi_graph G"
assumes verts_non_empty: "verts G ≠ {}"
assumes arcs_non_empty: "arcs G ≠ {}"
assumes reg': "⋀v w. v ∈ verts G ⟹ w ∈ verts G ⟹ out_degree G v = out_degree G w"
begin

definition d where "d = out_degree G (SOME v. v ∈ verts G)"

lemmas count_sym = count_edges_sym[OF sym]

lemma reg:
assumes "v ∈ verts G"
shows "out_degree G v = d" "in_degree G v = d"
proof -
define w where "w = (SOME v. v ∈ verts G)"
have "w ∈ verts G"
unfolding w_def using assms(1) by (rule someI)
hence "out_degree G v = out_degree G w"
by (intro reg' assms(1))
also have "... = d"
unfolding d_def w_def by simp
finally show a:"out_degree G v = d" by simp

show "in_degree G v = d"
using a symmetric_degree_eq[OF sym assms(1)] by simp
qed

definition n where "n = card (verts G)"

lemma n_gt_0: "n > 0"
unfolding n_def using verts_non_empty by auto

lemma d_gt_0: "d > 0"
proof -
obtain a where a:"a ∈ arcs G"
using arcs_non_empty by auto
hence "a ∈ in_arcs G (head G a) "
unfolding in_arcs_def by simp
hence "0 < in_degree G (head G a)"
unfolding in_degree_def card_gt_0_iff by blast
also have "... = d"
using a by (intro reg) simp
finally show ?thesis by simp
qed

definition g_inner :: "('a ⇒ ('c :: conjugatable_field)) ⇒ ('a ⇒ 'c) ⇒ 'c"
where "g_inner f g = (∑x ∈ verts G. (f x) * conjugate (g x))"

lemma conjugate_divide[simp]:
fixes x y :: "'c :: conjugatable_field"
shows "conjugate (x / y) = conjugate x / conjugate y"
proof (cases "y = 0")
case True
then show ?thesis by simp
next
case False
have "conjugate (x/y) * conjugate y = conjugate x"
thus ?thesis
qed

lemma g_inner_simps:
"g_inner (λx. 0) g = 0"
"g_inner f (λx. 0) = 0"
"g_inner (λx. c * f x) g = c * g_inner f g"
"g_inner f (λx. c * g x) = conjugate c * g_inner f g"
"g_inner (λx. f x - g x) h = g_inner f h - g_inner g h"
"g_inner (λx. f x + g x) h = g_inner f h + g_inner g h"
"g_inner f (λx. g x + h x) = g_inner f g + g_inner f h"
"g_inner f (λx. g x / c) = g_inner f g / conjugate c"
"g_inner (λx. f x / c) g = g_inner f g / c"
unfolding g_inner_def
by (auto simp add:sum.distrib algebra_simps sum_distrib_left sum_subtractf sum_divide_distrib

definition "g_norm f = sqrt (g_inner f f)"

lemma g_norm_eq: "g_norm f = L2_set f (verts G)"
unfolding g_norm_def g_inner_def L2_set_def
by (intro arg_cong[where f="sqrt"] sum.cong refl) (simp add:power2_eq_square)

lemma g_inner_cauchy_schwartz:
fixes f g :: "'a ⇒ real"
shows "¦g_inner f g¦ ≤ g_norm f * g_norm g"
proof -
have "¦g_inner f g¦ ≤ (∑v ∈ verts G. ¦f v * g v¦)"
unfolding g_inner_def conjugate_real_def by (intro sum_abs)
also have "... ≤ g_norm f * g_norm g"
unfolding g_norm_eq abs_mult by (intro L2_set_mult_ineq)
finally show ?thesis by simp
qed

lemma g_inner_cong:
assumes "⋀x. x ∈ verts G ⟹ f1 x = f2 x"
assumes "⋀x. x ∈ verts G ⟹ g1 x = g2 x"
shows "g_inner f1 g1 = g_inner f2 g2"
unfolding g_inner_def using assms
by (intro sum.cong refl) auto

lemma g_norm_cong:
assumes "⋀x. x ∈ verts G ⟹ f x = g x"
shows "g_norm f = g_norm g"
unfolding g_norm_def
by (intro arg_cong[where f="sqrt"] g_inner_cong assms)

lemma g_norm_nonneg: "g_norm f ≥ 0"
unfolding g_norm_def g_inner_def
by (intro real_sqrt_ge_zero sum_nonneg) auto

lemma g_norm_sq:
"g_norm f^2 = g_inner f f"
using g_norm_nonneg g_norm_def by simp

definition g_step :: "('a ⇒ real) ⇒ ('a ⇒ real)"
where "g_step f v = (∑x ∈ in_arcs G v. f (tail G x) / real d)"

lemma g_step_simps:
"g_step (λx. f x + g x) y = g_step f y + g_step g y"
"g_step (λx. f x / c) y = g_step f y / c"
unfolding g_step_def sum_divide_distrib[symmetric] using finite_in_arcs d_gt_0
by (auto intro:sum.cong simp add:sum.distrib field_simps sum_distrib_left sum_subtractf)

lemma g_inner_step_eq:
"g_inner f (g_step f) = (∑a ∈ arcs G. f (head G a) * f (tail G a)) / d" (is "?L = ?R")
proof -
have "?L = (∑v∈verts G. f v * (∑a∈in_arcs G v. f (tail G a) / d))"
unfolding g_inner_def g_step_def by simp
also have "... = (∑v∈verts G. (∑a∈in_arcs G v. f v * f (tail G a) / d))"
by (subst sum_distrib_left) simp
also have "... =  (∑v∈verts G. (∑a∈in_arcs G v. f (head G a) * f (tail G a) / d))"
unfolding in_arcs_def by (intro sum.cong refl) simp
also have "... = (∑a ∈ (⋃ (in_arcs G  verts G)). f (head G a) * f (tail G a) / d)"
using finite_verts by (intro sum.UNION_disjoint[symmetric] ballI)
also have "... = (∑a ∈ arcs G. f (head G a) * f (tail G a) / d)"
unfolding in_arcs_def using wellformed by (intro sum.cong) auto
also have "... = ?R"
by (intro sum_divide_distrib[symmetric])
finally show ?thesis by simp
qed

definition Λ_test
where "Λ_test = {f. g_norm f^2 ≠ 0 ∧ g_inner f (λ_. 1) = 0}"

lemma Λ_test_ne:
assumes "n > 1"
shows "Λ_test ≠ {}"
proof -
obtain v where v_def: "v ∈ verts G" using verts_non_empty by auto
have "False" if "⋀w. w ∈ verts G ⟹ w = v"
proof -
have "verts G = {v}" using that v_def
by (intro iffD2[OF set_eq_iff] allI) blast
thus False
using assms n_def by simp
qed
then obtain w where w_def: "w ∈ verts G" "v ≠ w"
by auto
define f where "f x= (if x = v then 1 else (if x = w then (-1) else (0::real)))" for x

have "g_norm f^2 = (∑x∈verts G. (if x = v then 1 else if x = w then - 1 else 0)⇧2)"
unfolding g_norm_sq g_inner_def conjugate_real_def power2_eq_square[symmetric]
also have "... = (∑x ∈ {v,w}. (if x = v then 1 else if x = w then -1 else 0)⇧2)"
using v_def(1) w_def(1) by (intro sum.mono_neutral_cong refl) auto
also have "... = (∑x ∈ {v,w}. (if x = v then 1 else - 1)⇧2)"
by (intro sum.cong) auto
also have "... = 2"
using w_def(2) by (simp add:if_distrib if_distribR sum.If_cases)
finally have "g_norm f^2 = 2" by simp
hence "g_norm f ≠ 0" by auto

moreover have "g_inner f (λ_.1) = 0"
unfolding g_inner_def f_def using v_def w_def by (simp add:sum.If_cases)
ultimately have "f ∈ Λ_test"
unfolding Λ_test_def by simp
thus ?thesis by auto
qed

lemma Λ_test_empty:
assumes "n = 1"
shows "Λ_test = {}"
proof -
obtain v where v_def: "verts G = {v}"
using assms card_1_singletonE unfolding n_def by auto
have "False" if "f ∈ Λ_test" for f
proof -
have "0 = (g_inner f (λ_.1))^2"
using that Λ_test_def by simp
also have "... = (f v)^2"
unfolding g_inner_def v_def by simp
also have "... = g_norm f^2"
unfolding g_norm_sq g_inner_def v_def
also have "... ≠ 0"
using that Λ_test_def by simp
finally show "False" by simp
qed
thus ?thesis by auto
qed

text ‹The following are variational definitions for the maxiumum of the spectrum (resp. maximum
modulus of the spectrum) of the stochastic matrix (excluding the Perron eigenvalue $1$). Note that
both values can still obtain the value one $1$ (if the multiplicity of the eigenvalue $1$ is larger
than $1$ in the stochastic matrix, or in the modulus case if $-1$ is an eigenvalue).

The definition relies on the supremum of the Rayleigh-Quotient for vectors orthogonal to the
stationary distribution). In Section~\ref{sec:expander_eigenvalues}, the equivalence of this
value with the algebraic definition will be shown. The definition here has the advantage
that it is (obviously) independent of the matrix representation (ordering of the vertices) used.›

definition Λ⇩2 :: real
where "Λ⇩2 = (if n > 1 then (SUP f ∈ Λ_test. g_inner f (g_step f)/g_inner f f) else 0)"

definition Λ⇩a :: real
where "Λ⇩a = (if n > 1 then (SUP f ∈ Λ_test. ¦g_inner f (g_step f)¦/g_inner f f) else 0)"

lemma sum_arcs_tail:
fixes f :: "'a ⇒ ('c :: semiring_1)"
shows "(∑a ∈ arcs G. f (tail G a)) = of_nat d * (∑v ∈ verts G. f v)" (is "?L = ?R")
proof -
have "?L = (∑a∈(⋃(out_arcs G  verts G)). f (tail G a))"
by (intro sum.cong) auto
also have "... =  (∑v ∈ verts G. (∑a ∈ out_arcs G v. f (tail G a)))"
by (intro sum.UNION_disjoint) auto
also have "... = (∑v ∈ verts G. of_nat (out_degree G v) * f v)"
unfolding out_degree_def by simp
also have "... = (∑v ∈ verts G. of_nat d * f v)"
by (intro sum.cong arg_cong2[where f="(*)"] arg_cong[where f="of_nat"] reg) auto
also have "... = ?R" by (simp add:sum_distrib_left)
finally show ?thesis by simp
qed

fixes f :: "'a ⇒ ('c :: semiring_1)"
shows "(∑a ∈ arcs G. f (head G a)) = of_nat d * (∑v ∈ verts G. f v)" (is "?L = ?R")
proof -
have "?L = (∑a∈(⋃(in_arcs G  verts G)). f (head G a))"
by (intro sum.cong) auto
also have "... =  (∑v ∈ verts G. (∑a ∈ in_arcs G v. f (head G a)))"
by (intro sum.UNION_disjoint) auto
also have "... = (∑v ∈ verts G. of_nat (in_degree G v) * f v)"
unfolding in_degree_def by simp
also have "... = (∑v ∈ verts G. of_nat d * f v)"
by (intro sum.cong arg_cong2[where f="(*)"] arg_cong[where f="of_nat"] reg) auto
also have "... = ?R" by (simp add:sum_distrib_left)
finally show ?thesis by simp
qed

lemma bdd_above_aux:
"¦∑a∈arcs G. f(head G a)*f(tail G a)¦ ≤ d* g_norm f^2" (is "?L ≤ ?R")
proof -
have "(∑a∈arcs G. f (head G a)^2) =  d * g_norm f^2"
unfolding sum_arcs_head[where f="λx. f x^2"] g_norm_sq g_inner_def
hence 0:"L2_set (λa. f (head G a)) (arcs G) ≤ sqrt (d * g_norm f^2)"
using g_norm_nonneg unfolding L2_set_def by simp

have "(∑a∈arcs G. f (tail G a)^2) = d * g_norm f^2"
unfolding sum_arcs_tail[where f="λx. f x^2"] sum_distrib_left[symmetric] g_norm_sq g_inner_def
hence 1:"L2_set (λa. f (tail G a)) (arcs G) ≤ sqrt (d * g_norm f^2)"
unfolding L2_set_def by simp

have "?L ≤ (∑a ∈ arcs G. ¦f (head G a)¦ * ¦f(tail G a)¦)"
unfolding abs_mult[symmetric] by (intro divide_right_mono sum_abs)
also have "... ≤ (L2_set (λa. f (head G a)) (arcs G) * L2_set (λa. f (tail G a)) (arcs G))"
by (intro L2_set_mult_ineq)
also have "... ≤ (sqrt (d * g_norm f^2) * sqrt (d * g_norm f^2))"
by (intro mult_mono 0 1) auto
also have "... = d * g_norm f^2"
using d_gt_0 g_norm_nonneg by simp
finally show ?thesis by simp
qed

lemma bdd_above_aux_2:
assumes "f ∈ Λ_test"
shows "¦g_inner f (g_step f)¦ / g_inner f f ≤ 1"
proof -
have 0:"g_inner f f > 0"
using assms unfolding Λ_test_def g_norm_sq[symmetric] by auto

have "¦g_inner f (g_step f)¦ = ¦∑a∈arcs G. f (head G a) * f (tail G a)¦ / real d"
unfolding g_inner_step_eq by simp
also have "... ≤ d * g_norm f^2 / d"
by (intro divide_right_mono bdd_above_aux assms) auto
also have "... = g_inner f f"
using d_gt_0 unfolding g_norm_sq by simp
finally have "¦g_inner f (g_step f)¦ ≤ g_inner f f"
by simp

thus ?thesis
using 0 by simp
qed

lemma bdd_above_aux_3:
assumes "f ∈ Λ_test"
shows "g_inner f (g_step f) / g_inner f f ≤ 1" (is "?L ≤ ?R")
proof -
have "?L ≤ ¦g_inner f (g_step f)¦ / g_inner f f"
unfolding g_norm_sq[symmetric]
by (intro divide_right_mono) auto
also have "... ≤ 1"
using bdd_above_aux_2[OF assms] by simp
finally show ?thesis by simp
qed

lemma bdd_above_Λ: "bdd_above ((λf. ¦g_inner f (g_step f)¦ / g_inner f f)  Λ_test)"
using bdd_above_aux_2
by (intro bdd_aboveI[where M="1"])  auto

lemma bdd_above_Λ⇩2: "bdd_above ((λf. g_inner f (g_step f) / g_inner f f)  Λ_test)"
using bdd_above_aux_3
by (intro bdd_aboveI[where M="1"])  auto

lemma Λ_le_1: "Λ⇩a ≤ 1"
proof (cases "n > 1")
case True
have "(SUP f∈Λ_test. ¦g_inner f (g_step f)¦ / g_inner f f) ≤ 1"
using bdd_above_aux_2 Λ_test_ne[OF True] by (intro cSup_least) auto
thus "Λ⇩a ≤ 1"
unfolding Λ⇩a_def using True by simp
next
case False
thus ?thesis unfolding Λ⇩a_def by simp
qed

lemma Λ⇩2_le_1: "Λ⇩2 ≤ 1"
proof (cases "n > 1")
case True
have "(SUP f∈Λ_test. g_inner f (g_step f) / g_inner f f) ≤ 1"
using bdd_above_aux_3 Λ_test_ne[OF True] by (intro cSup_least) auto
thus "Λ⇩2 ≤ 1"
unfolding Λ⇩2_def using True by simp
next
case False
thus ?thesis unfolding Λ⇩2_def by simp
qed

lemma Λ_ge_0: "Λ⇩a ≥ 0"
proof (cases "n > 1")
case True
obtain f where f_def: "f ∈ Λ_test"
using Λ_test_ne[OF True] by auto
have "0 ≤ ¦g_inner f (g_step f)¦ / g_inner f f"
unfolding g_norm_sq[symmetric] by (intro divide_nonneg_nonneg) auto
also have "... ≤ (SUP f∈Λ_test. ¦g_inner f (g_step f)¦ / g_inner f f)"
using f_def by (intro cSup_upper bdd_above_Λ) auto
finally have "(SUP f∈Λ_test. ¦g_inner f (g_step f)¦ / g_inner f f) ≥ 0"
by simp
thus ?thesis
unfolding Λ⇩a_def using True by simp
next
case False
thus ?thesis unfolding Λ⇩a_def by simp
qed

lemma os_expanderI:
assumes "n > 1"
assumes "⋀f. g_inner f (λ_. 1)=0 ⟹ g_inner f (g_step f) ≤ C*g_norm f^2"
shows "Λ⇩2 ≤ C"
proof -
have "g_inner f (g_step f) / g_inner f f ≤ C" if "f ∈ Λ_test" for f
proof -
have "g_inner f (g_step f) ≤ C*g_inner f f"
using that Λ_test_def assms(2) unfolding g_norm_sq by auto
moreover have "g_inner f f > 0"
using that unfolding Λ_test_def g_norm_sq[symmetric] by auto
ultimately show ?thesis
qed
hence "(SUP f∈Λ_test. g_inner f (g_step f) / g_inner f f) ≤ C"
using Λ_test_ne[OF assms(1)] by (intro cSup_least) auto
thus ?thesis
unfolding Λ⇩2_def using assms by simp
qed

lemma os_expanderD:
assumes "g_inner f (λ_. 1) = 0"
shows "g_inner f (g_step f) ≤ Λ⇩2 * g_norm f^2"  (is "?L ≤ ?R")
proof (cases "g_norm f ≠ 0")
case True

have 0:"f ∈ Λ_test"
unfolding Λ_test_def using assms True by auto

hence 1:"n > 1"
using Λ_test_empty n_gt_0 by fastforce

have "g_inner f (g_step f)/ g_norm f^2 = g_inner f (g_step f)/g_inner f f"
unfolding g_norm_sq by simp
also have "... ≤ (SUP f∈Λ_test. g_inner f (g_step f) / g_inner f f)"
by (intro cSup_upper bdd_above_Λ⇩2 imageI 0)
also have "... = Λ⇩2"
using 1 unfolding Λ⇩2_def by simp
finally have "g_inner f (g_step f)/ g_norm f^2 ≤ Λ⇩2" by simp
thus ?thesis
next
case False
hence "g_inner f f = 0"
unfolding g_norm_sq[symmetric] by simp
hence 0:"⋀v. v ∈ verts G ⟹ f v = 0"
unfolding g_inner_def by (subst (asm) sum_nonneg_eq_0_iff) auto
hence "?L = 0"
unfolding g_step_def g_inner_def by simp
also have "... ≤ Λ⇩2 * g_norm f^2"
using False by simp
finally show ?thesis by simp
qed

lemma expander_intro_1:
assumes "C ≥ 0"
assumes "⋀f. g_inner f (λ_. 1)=0 ⟹ ¦g_inner f (g_step f)¦ ≤ C*g_norm f^2"
shows "Λ⇩a ≤ C"
proof (cases "n > 1")
case True
have "¦g_inner f (g_step f)¦ / g_inner f f ≤ C" if "f ∈ Λ_test" for f
proof -
have "¦g_inner f (g_step f)¦ ≤ C*g_inner f f"
using that Λ_test_def assms(2) unfolding g_norm_sq by auto
moreover have "g_inner f f > 0"
using that unfolding Λ_test_def g_norm_sq[symmetric] by auto
ultimately show ?thesis
qed

hence "(SUP f∈Λ_test. ¦g_inner f (g_step f)¦ / g_inner f f) ≤ C"
using Λ_test_ne[OF True] by (intro cSup_least) auto
thus ?thesis using True unfolding Λ⇩a_def by auto
next
case False
then show ?thesis using assms unfolding Λ⇩a_def by simp
qed

lemma expander_intro:
assumes "C ≥ 0"
assumes "⋀f. g_inner f (λ_. 1)=0 ⟹ ¦∑a ∈ arcs G. f(head G a) * f(tail G a)¦ ≤ C*g_norm f^2"
shows "Λ⇩a ≤ C/d"
proof -
have "¦g_inner f (g_step f)¦ ≤ C / real d * (g_norm f)⇧2" (is "?L ≤ ?R")
if "g_inner f (λ_. 1) = 0" for f
proof -
have "?L = ¦∑a∈arcs G. f (head G a) * f (tail G a)¦ / real d"
unfolding g_inner_step_eq by simp
also have "... ≤ C*g_norm f^2 / real d"
by (intro divide_right_mono assms(2)[OF that]) auto
also have "... = ?R" by simp
finally show ?thesis by simp
qed
thus ?thesis
by (intro expander_intro_1 divide_nonneg_nonneg assms) auto
qed

lemma expansionD1:
assumes "g_inner f (λ_. 1) = 0"
shows "¦g_inner f (g_step f)¦ ≤ Λ⇩a * g_norm f^2"  (is "?L ≤ ?R")
proof (cases "g_norm f ≠ 0")
case True

have 0:"f ∈ Λ_test"
unfolding Λ_test_def using assms True by auto

hence 1:"n > 1"
using Λ_test_empty n_gt_0 by fastforce

have "¦g_inner f (g_step f)¦/ g_norm f^2 = ¦g_inner f (g_step f)¦/g_inner f f"
unfolding g_norm_sq by simp
also have "... ≤ (SUP f∈Λ_test. ¦g_inner f (g_step f)¦ / g_inner f f)"
by (intro cSup_upper bdd_above_Λ imageI 0)
also have "... = Λ⇩a"
using 1 unfolding Λ⇩a_def by simp
finally have "¦g_inner f (g_step f)¦/ g_norm f^2 ≤ Λ⇩a" by simp
thus ?thesis
next
case False
hence "g_inner f f = 0"
unfolding g_norm_sq[symmetric] by simp
hence 0:"⋀v. v ∈ verts G ⟹ f v = 0"
unfolding g_inner_def by (subst (asm) sum_nonneg_eq_0_iff) auto
hence "?L = 0"
unfolding g_step_def g_inner_def by simp
also have "... ≤ Λ⇩a * g_norm f^2"
using False by simp
finally show ?thesis by simp
qed

lemma expansionD:
assumes "g_inner f (λ_. 1) = 0"
shows "¦∑a ∈ arcs G. f (head G a) * f (tail G a)¦ ≤ d * Λ⇩a * g_norm f^2"  (is "?L ≤ ?R")
proof -
have "?L = ¦g_inner f (g_step f) * d¦"
unfolding g_inner_step_eq using d_gt_0 by simp
also have "... ≤ ¦g_inner f (g_step f)¦ * d"
also have "... ≤ (Λ⇩a * g_norm f^2) * d"
by (intro expansionD1 mult_right_mono assms(1)) auto
also have "... = ?R" by simp
finally show ?thesis by simp
qed

definition edges_betw where "edges_betw S T = {a ∈ arcs G. tail G a ∈ S ∧ head G a ∈ T}"

text ‹This parameter is the edge expansion. It is usually denoted by the symbol $h$ or $h(G)$ in
text books. Contrary to the previous definitions it doesn't have a spectral theoretic counter
part.›

definition Λ⇩e where "Λ⇩e = (if n > 1 then
(MIN S∈{S. S⊆verts G∧2*card S≤n∧S≠{}}. real (card (edges_betw S (-S)))/card S) else 0)"

lemma edge_expansionD:
assumes "S ⊆ verts G" "2*card S ≤ n"
shows "Λ⇩e * card S ≤ real (card (edges_betw S (-S)))"
proof (cases "S ≠ {}")
case True
moreover have "finite S"
using finite_subset[OF assms(1)] by simp
ultimately have "card S > 0" by auto
hence 1: "real (card S) > 0" by simp
hence 2: "n > 1" using assms(2) by simp

let ?St = "{S. S ⊆ verts G ∧ 2 * card S ≤ n ∧ S ≠ {}}"

have 0: "finite ?St"
by (rule finite_subset[where B="Pow (verts G)"]) auto
have "Λ⇩e = (MIN S∈?St. real (card (edges_betw S (-S)))/card S)"
using 2 unfolding Λ⇩e_def by simp

also have "... ≤ real (card (edges_betw S (-S))) / card S"
using assms True by (intro Min_le finite_imageI imageI) auto
finally have "Λ⇩e ≤ real (card (edges_betw S (-S))) / card S" by simp
thus ?thesis using 1 by (simp add:divide_simps)
next
case False
hence "card S = 0" by simp
thus ?thesis by simp
qed

lemma edge_expansionI:
fixes α :: real
assumes "n > 1"
assumes "⋀S. S ⊆ verts G ⟹ 2*card S ≤ n ⟹ S ≠ {} ⟹ card (edges_betw S (-S)) ≥ α * card S"
shows "Λ⇩e ≥ α"
proof -
define St where "St = {S. S ⊆ verts G ∧ 2*card S ≤ n ∧ S ≠ {}}"
have 0: "finite St"
unfolding St_def
by (rule finite_subset[where B="Pow (verts G)"]) auto

obtain v where v_def: "v ∈ verts G" using verts_non_empty by auto

have "{v} ∈ St"
using assms v_def unfolding St_def n_def by auto
hence 1: "St ≠ {}" by auto

have 2: "α ≤ real (card (edges_betw S (- S))) / real (card S)" if "S ∈ St" for S
proof -
have "real (card (edges_betw S (- S)))  ≥ α * card S"
using assms(2) that unfolding St_def by simp
moreover have "finite S"
using that unfolding St_def
by (intro finite_subset[OF _ finite_verts]) auto
hence "card S > 0"
using that unfolding St_def by auto
ultimately show ?thesis
qed

have "α ≤ (MIN S∈St. real (card (edges_betw S (- S))) / real (card S))"
using 0 1 2
by (intro Min.boundedI finite_imageI) auto

thus ?thesis
unfolding Λ⇩e_def St_def[symmetric] using assms by auto
qed

end

lemma regular_graphI:
assumes "symmetric_multi_graph G"
assumes "verts G ≠ {}" "d > 0"
assumes "⋀v. v ∈ verts G ⟹ out_degree G v = d"
shows "regular_graph G"
proof -
obtain v where v_def: "v ∈ verts G"
using assms(2) by auto
have "arcs G ≠ {}"
proof (rule ccontr)
assume "¬arcs G ≠ {}"
hence "arcs G = {}" by simp
hence "out_degree G v = 0"
unfolding out_degree_def out_arcs_def by simp
hence "d = 0"
using v_def assms(4) by simp
thus False
using assms(3) by simp
qed

thus ?thesis
using assms symmetric_multi_graphD2[OF assms(1)]
unfolding regular_graph_def regular_graph_axioms_def
by simp
qed

text ‹The following theorems verify that a graph isomorphisms preserve symmetry, regularity and all
the expansion coefficients.›

lemma (in fin_digraph) symmetric_graph_iso:
assumes "digraph_iso G H"
assumes "symmetric_multi_graph G"
shows "symmetric_multi_graph H"
proof -
obtain h where hom_iso: "digraph_isomorphism h" and H_alt: "H = app_iso h G"
using assms unfolding digraph_iso_def by auto

have 0:"fin_digraph H"
unfolding H_alt
by (intro fin_digraphI_app_iso hom_iso)

interpret H:fin_digraph H
using 0 by auto

have 1:"arcs_betw H (iso_verts h v) (iso_verts h w) = iso_arcs h  arcs_betw G v w"
(is "?L = ?R") if "v ∈ verts G" "w ∈ verts G" for v w
proof -
have "?L = {a ∈ iso_arcs h  arcs G. iso_head h a=iso_verts h w ∧ iso_tail h a=iso_verts h v}"
unfolding arcs_betw_def H_alt arcs_app_iso head_app_iso tail_app_iso by simp
also have "... = {a. (∃b ∈ arcs G. a = iso_arcs h b ∧ iso_verts h (head G b) = iso_verts h w ∧
iso_verts h (tail G b) = iso_verts h v)}"
using iso_verts_head[OF hom_iso] iso_verts_tail[OF hom_iso] by auto
also have "... = {a. (∃b ∈ arcs G. a = iso_arcs h b ∧ head G b = w ∧ tail G b = v)}"
using that iso_verts_eq_iff[OF hom_iso] by auto
also have "... = ?R"
unfolding arcs_betw_def by (auto simp add:image_iff set_eq_iff)
finally show ?thesis by simp
qed

have "card (arcs_betw H w v) = card (arcs_betw H v w)" (is "?L = ?R")
if v_range: "v ∈ verts H" and w_range: "w ∈ verts H" for v w
proof -
obtain v' where v': "v = iso_verts h v'" "v' ∈ verts G"
using that v_range verts_app_iso unfolding H_alt by auto
obtain w' where w': "w = iso_verts h w'" "w' ∈ verts G"
using that w_range verts_app_iso unfolding H_alt by auto
have "?L = card (arcs_betw H (iso_verts h w') (iso_verts h v'))"
unfolding v' w' by simp
also have "... = card (iso_arcs h  arcs_betw G w' v')"
by (intro arg_cong[where f="card"] 1 v' w')
also have "... = card (arcs_betw G w' v')"
using iso_arcs_eq_iff[OF hom_iso] unfolding arcs_betw_def
by (intro card_image inj_onI) auto
also have "... = card (arcs_betw G v' w')"
by (intro symmetric_multi_graphD4 assms(2))
also have "... = card (iso_arcs h  arcs_betw G v' w')"
using iso_arcs_eq_iff[OF hom_iso] unfolding arcs_betw_def
by (intro card_image[symmetric] inj_onI) auto
also have "... = card (arcs_betw H (iso_verts h v') (iso_verts h w'))"
by (intro arg_cong[where f="card"] 1[symmetric] v' w')
also have "... = ?R"
unfolding v' w' by simp
finally show ?thesis by simp
qed

thus ?thesis
using 0 unfolding symmetric_multi_graph_def by auto
qed

lemma (in regular_graph)
assumes "digraph_iso G H"
shows regular_graph_iso: "regular_graph H"
and regular_graph_iso_size: "regular_graph.n H = n"
and regular_graph_iso_degree: "regular_graph.d H = d"
and regular_graph_iso_expansion_le:  "regular_graph.Λ⇩a H ≤ Λ⇩a"
and regular_graph_iso_os_expansion_le: "regular_graph.Λ⇩2 H ≤ Λ⇩2"
and regular_graph_iso_edge_expansion_ge: "regular_graph.Λ⇩e H ≥ Λ⇩e"
proof -
obtain h where hom_iso: "digraph_isomorphism h" and H_alt: "H = app_iso h G"
using assms unfolding digraph_iso_def by auto

have 0:"symmetric_multi_graph H"
by (intro symmetric_graph_iso[OF assms(1)] sym)

have 1:"verts H ≠ {}"
unfolding H_alt verts_app_iso using verts_non_empty by simp

then obtain h_wit where h_wit: "h_wit ∈ verts H"
by auto

have 3:"out_degree H v = d" if v_range: "v ∈ verts H" for v
proof -
obtain v' where v': "v = iso_verts h v'" "v' ∈ verts G"
using that v_range verts_app_iso unfolding H_alt by auto
have "out_degree H v = out_degree G v'"
unfolding v' H_alt by (intro out_degree_app_iso_eq[OF hom_iso] v')
also have "... = d"
by (intro reg v')
finally  show ?thesis by simp
qed

thus 2:"regular_graph H"
by (intro regular_graphI[where d="d"] 0 d_gt_0 1) auto
interpret H:"regular_graph" H
using 2 by auto

have "H.n = card (iso_verts h  verts G)"
unfolding H.n_def unfolding H_alt verts_app_iso by simp
also have "... = card (verts G)"
by (intro card_image digraph_isomorphism_inj_on_verts hom_iso)
also have "... = n"
unfolding n_def by simp
finally show n_eq: "H.n = n" by simp

have "H.d = out_degree H h_wit"
by (intro H.reg[symmetric] h_wit)
also have "... = d"
by (intro 3 h_wit)
finally show 4:"H.d = d" by simp

have "bij_betw (iso_verts h) (verts G) (verts H)"
unfolding H_alt using hom_iso

hence g_inner_conv:
"H.g_inner f g = g_inner (λx. f (iso_verts h x)) (λx. g (iso_verts h x))"
for f g :: "'c ⇒ real"
unfolding g_inner_def H.g_inner_def by (intro sum.reindex_bij_betw[symmetric])

have g_step_conv:
"H.g_step f (iso_verts h x) = g_step (λx. f (iso_verts h x)) x" if "x ∈ verts G"
for f :: "'c ⇒ real" and x
proof -
have "inj_on (iso_arcs h) (in_arcs G x)"
using inj_on_subset[OF digraph_isomorphism_inj_on_arcs[OF hom_iso]]
moreover have "in_arcs H (iso_verts h x) = iso_arcs h  in_arcs G x"
unfolding H_alt by (intro in_arcs_app_iso_eq[OF hom_iso] that)
moreover have "tail H (iso_arcs h a) = iso_verts h (tail G a)" if "a ∈ in_arcs G x" for a
unfolding H_alt using that by (simp add: hom_iso iso_verts_tail)
ultimately show ?thesis
unfolding g_step_def H.g_step_def
by (intro_cong "[σ⇩2(/), σ⇩1 f, σ⇩1 of_nat]" more: 4 sum.reindex_cong[where l="iso_arcs h"])
qed

show "H.Λ⇩a ≤ Λ⇩a"
using expansionD1 by (intro H.expander_intro_1 Λ_ge_0)
(simp add:g_inner_conv g_step_conv H.g_norm_sq g_norm_sq cong:g_inner_cong)

show "H.Λ⇩2 ≤ Λ⇩2"
proof (cases "n > 1")
case True
hence "H.n  > 1"
thus ?thesis
using os_expanderD by (intro H.os_expanderI)
(simp_all add:g_inner_conv g_step_conv H.g_norm_sq g_norm_sq cong:g_inner_cong)
next
case False
thus ?thesis
unfolding H.Λ⇩2_def Λ⇩2_def by (simp add:n_eq)
qed

show "H.Λ⇩e ≥ Λ⇩e"
proof (cases "n > 1")
case True
hence n_gt_1: "H.n  > 1"
have "Λ⇩e * real (card S) ≤ real (card (H.edges_betw S (- S)))"
if "S ⊆ verts H" "2 * card S ≤ H.n" "S ≠ {}" for S
proof -
define T where "T = iso_verts h - S ∩ verts G"
have 4:"card T = card S"
using that(1) unfolding T_def H_alt verts_app_iso
by (intro card_vimage_inj_on digraph_isomorphism_inj_on_verts[OF hom_iso]) auto

have "card (H.edges_betw S (-S))=card {a∈iso_arcs harcs G. iso_tail h a∈S∧iso_head h a∈ -S}"
unfolding H.edges_betw_def unfolding H_alt tail_app_iso head_app_iso arcs_app_iso
by simp
also have "...=
card(iso_arcs h {a ∈ arcs G. iso_tail h (iso_arcs h a)∈S∧ iso_head h (iso_arcs h a)∈-S})"
by (intro arg_cong[where f="card"]) auto
also have "... = card {a ∈ arcs G. iso_tail h (iso_arcs h a)∈S∧ iso_head h (iso_arcs h a)∈-S}"
by (intro card_image inj_on_subset[OF digraph_isomorphism_inj_on_arcs[OF hom_iso]]) auto
also have "... = card {a ∈ arcs G. iso_verts h (tail G a) ∈ S ∧ iso_verts h (head G a) ∈ -S}"
by (intro restr_Collect_cong arg_cong[where f="card"])
also have "... = card {a ∈ arcs G. tail G a ∈ T ∧ head G a ∈ -T }"
unfolding T_def by (intro_cong "[σ⇩1(card),σ⇩2 (∧)]" more: restr_Collect_cong) auto
also have "... = card (edges_betw T (-T))"
unfolding edges_betw_def by simp
finally have 5:"card (edges_betw T (-T)) = card (H.edges_betw S (-S))"
by simp

have 6: "T ⊆ verts G" unfolding T_def by simp

have "Λ⇩e * real (card S) = Λ⇩e * real (card T)"
unfolding 4 by simp
also have "... ≤ real (card (edges_betw T (-T)))"
using that(2) by (intro edge_expansionD 6) (simp add:4 n_eq)
also have "... = real (card (H.edges_betw S (-S)))"
unfolding 5 by simp
finally show ?thesis by simp
qed

thus ?thesis
by (intro H.edge_expansionI n_gt_1) auto
next
case False
thus ?thesis
unfolding H.Λ⇩e_def Λ⇩e_def by (simp add:n_eq)
qed

qed

lemma (in regular_graph)
assumes "digraph_iso G H"
shows regular_graph_iso_expansion: "regular_graph.Λ⇩a H = Λ⇩a"
and regular_graph_iso_os_expansion: "regular_graph.Λ⇩2 H = Λ⇩2"
and regular_graph_iso_edge_expansion: "regular_graph.Λ⇩e H = Λ⇩e"
proof -
interpret H:"regular_graph" "H"
by (intro regular_graph_iso assms)

have iso:"digraph_iso H G"
using digraph_iso_swap assms wf_digraph_axioms by blast

hence "Λ⇩a ≤ H.Λ⇩a"
by (intro H.regular_graph_iso_expansion_le)
moreover have "H.Λ⇩a ≤ Λ⇩a"
using regular_graph_iso_expansion_le[OF assms] by auto
ultimately show "H.Λ⇩a = Λ⇩a"
by auto

have "Λ⇩2 ≤ H.Λ⇩2" using iso
by (intro H.regular_graph_iso_os_expansion_le)
moreover have "H.Λ⇩2 ≤ Λ⇩2"
using regular_graph_iso_os_expansion_le[OF assms] by auto
ultimately show "H.Λ⇩2 = Λ⇩2"
by auto

have "Λ⇩e ≥ H.Λ⇩e" using iso
by (intro H.regular_graph_iso_edge_expansion_ge)
moreover have "H.Λ⇩e ≥ Λ⇩e"
using regular_graph_iso_edge_expansion_ge[OF assms] by auto
ultimately show "H.Λ⇩e = Λ⇩e"
by auto
qed

unbundle no_intro_cong_syntax

end
`