Theory Expander_Graphs.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
    by (simp add:image_mset.compositionality image_mset_filter_mset_swap[symmetric] comp_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
    by (simp add:image_mset.compositionality image_mset_filter_mset_swap[symmetric] comp_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"
    using False by (simp add:conjugate_dist_mul[symmetric])
  thus ?thesis
    by (simp add:divide_simps)
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
      conjugate_dist_mul conjugate_dist_add)

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)
      (auto simp add:in_arcs_def)
  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]
    by (simp add:f_def)
  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
      by (simp add:power2_eq_square)
    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

lemma sum_arcs_head:
  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
    by (simp add:power2_eq_square)
  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
    by (simp add:power2_eq_square)
  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
      by (simp add:divide_simps)
  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
    using True by (simp add:divide_simps)
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
      by (simp add:divide_simps)
  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
    using True by (simp add:divide_simps)
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"
    by (simp add:abs_mult)
  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
      by (simp add:divide_simps)
  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
    by (simp add: bij_betw_def digraph_isomorphism_inj_on_verts)

  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]]
      by (simp add:in_arcs_def)
    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"
      by (simp add:n_eq)
    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"
      by (simp add:n_eq)
    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 h`arcs 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"])
         (simp add: iso_verts_tail[OF hom_iso] iso_verts_head[OF hom_iso])
      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