Theory Expander_Graphs.Expander_Graphs_Power_Construction

section ‹Graph Powers\label{sec:graph_power}›

theory Expander_Graphs_Power_Construction
  imports
    Expander_Graphs_Walks
    Graph_Theory.Arc_Walk
begin

unbundle intro_cong_syntax

fun is_arc_walk :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b list ⇒ bool"
  where
    "is_arc_walk G _ [] = True" |
    "is_arc_walk G y (x#xs) = (is_arc_walk G (head G x) xs ∧ tail G x = y ∧ x ∈ arcs G)"

definition arc_walk_head :: "('a, 'b) pre_digraph ⇒ ('a × 'b list) ⇒ 'a"
  where
    "arc_walk_head G x = (if snd x = [] then fst x else head G (last (snd x)))"

lemma is_arc_walk_snoc:
  "is_arc_walk G y (xs@[x]) ⟷ is_arc_walk G y xs ∧ x ∈ out_arcs G (arc_walk_head G (y,xs))"
  by (induction xs arbitrary: y, simp_all add:ac_simps arc_walk_head_def)

lemma is_arc_walk_set:
  assumes "is_arc_walk G u w"
  shows "set w ⊆ arcs G"
  using assms by (induction w arbitrary: u, auto)

lemma (in wf_digraph) awalk_is_arc_walk:
  assumes "u ∈ verts G"
  shows "is_arc_walk G u w ⟷ awalk u w (awlast u w)"
  using assms unfolding awalk_def by (induction w arbitrary: u, auto)

definition arc_walks :: "('a, 'b) pre_digraph ⇒ nat ⇒ ('a × 'b list) set"
  where
    "arc_walks G l = {(u,w). u ∈ verts G ∧ is_arc_walk G u w ∧ length w = l}"

lemma arc_walks_len:
  assumes "x ∈ arc_walks G l"
  shows "length (snd x) = l"
  using assms unfolding arc_walks_def by auto

lemma (in wf_digraph) awhd_of_arc_walk:
  assumes "w ∈ arc_walks G l"
  shows "awhd (fst w) (snd w) = fst w"
  using assms unfolding arc_walks_def awalk_verts_def
  by (cases "snd w", auto)

lemma (in wf_digraph) awlast_of_arc_walk:
  assumes "w ∈ arc_walks G l"
  shows "awlast (fst w) (snd w) = arc_walk_head G w"
  unfolding awalk_verts_conv arc_walk_head_def by simp

lemma (in wf_digraph) arc_walk_head_wellformed:
  assumes "w ∈ arc_walks G l"
  shows "arc_walk_head G w ∈ verts G"
proof (cases "snd w = []")
  case True
  then show ?thesis
    using assms unfolding arc_walks_def arc_walk_head_def by auto
next
  case False
  have 0:"is_arc_walk G (fst w) (snd w)" using assms unfolding arc_walks_def by auto
  have "last (snd w) ∈ set (snd w)"
    using False last_in_set by auto
  also have "... ⊆ arcs G"
    by (intro is_arc_walk_set[OF 0])
  finally have "last (snd w) ∈ arcs G" by simp
  thus ?thesis unfolding arc_walk_head_def using False by simp
qed

lemma (in wf_digraph) arc_walk_tail_wellformed:
  assumes "w ∈ arc_walks G l"
  shows "fst w ∈ verts G"
  using assms unfolding arc_walks_def by auto

lemma (in fin_digraph) arc_walks_fin:
  "finite (arc_walks G l)"
proof -
  have 0:"finite (verts G × {w. set w ⊆ arcs G ∧ length w = l})"
    by (intro finite_cartesian_product finite_lists_length_eq) auto
  show "finite (arc_walks G l)"
    unfolding arc_walks_def using is_arc_walk_set[where G="G"]
    by (intro finite_subset[OF _ 0] subsetI) auto
qed

lemma (in wf_digraph) awalk_verts_unfold:
  assumes "w ∈ arc_walks G l"
  shows "awalk_verts (fst w) (snd w) = fst w#map (head G) (snd w)" (is "?L = ?R")
proof -
  obtain u v where w_def: "w = (u,v)" by fastforce

  have "awalk u v (awlast u v)"
    using assms unfolding w_def arc_walks_def
    by (intro iffD1[OF awalk_is_arc_walk]) auto
  hence cas: "cas u v (awlast u v)"
    unfolding awalk_def by simp

  have 0: "tail G (hd v) = u" if "v ≠ []"
    using cas that by (cases v) auto

  have "?L = awalk_verts u v"
    unfolding w_def by simp
  also have "... = (if v = [] then [u] else tail G (hd v) # map (head G) v)"
    by (intro awalk_verts_conv'[OF cas])
  also have "... = u# map (head G) v"
    using 0 by simp
  also have "... = ?R"
    unfolding w_def by simp
  finally show ?thesis by simp
qed

lemma (in fin_digraph) arc_walks_map_walks':
  "walks' G l = image_mset (case_prod awalk_verts) (mset_set (arc_walks G l))"
proof (induction l)
  case 0
  let ?g = "λx. fst x#map (head G) (snd x)"

  have "walks' G 0 = {#[x]. x ∈# mset_set (verts G)#}"
    by simp
  also have "... = image_mset ?g (image_mset (λx. (x,[])) (mset_set (verts G)))"
    unfolding image_mset.compositionality by (simp add:comp_def)
  also have "... = image_mset ?g (mset_set ((λx. (x,[])) ` verts G))"
    by (intro arg_cong2[where f="image_mset"] image_mset_mset_set inj_onI) auto
  also have "... = image_mset ?g (mset_set ({(u, w). u ∈ verts G ∧ w = []}))"
    by (intro_cong "[σ⇩2 image_mset]") auto
  also have "... = image_mset ?g (mset_set (arc_walks G 0))"
    unfolding arc_walks_def by (intro_cong "[σ⇩2 image_mset,σ⇩1 mset_set]") auto
  also have "... = image_mset (case_prod awalk_verts) (mset_set (arc_walks G 0))"
    using arc_walks_fin by (intro image_mset_cong) (simp add:case_prod_beta awalk_verts_unfold)
  finally show ?case by simp
next
  case (Suc l)
  let ?f = "λ(u,w) a. (u,w@[a])"
  let ?g = "λx. fst x#map (head G) (snd x)"

  have "arc_walks G (l+1) = case_prod ?f ` {(x,y). ?f x y ∈ arc_walks G (l+1)}"
    using arc_walks_len[where G="G" and l="Suc l", THEN iffD1[OF length_Suc_conv_rev]]
    by force
  also have "... = case_prod ?f ` {(x,y). x ∈ arc_walks G l ∧ y ∈ out_arcs G (arc_walk_head G x)}"
    unfolding arc_walks_def using is_arc_walk_snoc[where G="G"]
    by (intro_cong "[σ⇩2 image]")  auto
  also have "... = (⋃w ∈ arc_walks G l. ?f w ` out_arcs G (arc_walk_head G w))"
    by (auto simp add:image_iff)
  finally have 0:"arc_walks G (l+1) = (⋃w ∈ arc_walks G l. ?f w ` out_arcs G (arc_walk_head G w))"
    by simp

  have "mset_set (arc_walks G (l+1)) = concat_mset (image_mset (mset_set ∘
    (λw. ?f w ` out_arcs G (arc_walk_head G w))) (mset_set (arc_walks G l)))"
    unfolding 0 by (intro concat_disjoint_union_mset arc_walks_fin finite_imageI) auto
  also have "... = concat_mset {# mset_set (?f x ` out_arcs G (arc_walk_head G x)).
    x∈#mset_set(arc_walks G l)#}"
    by (simp add:comp_def case_prod_beta)
  also have "... = concat_mset {# {# ?f x y. y ∈# mset_set (out_arcs G (arc_walk_head G x))#}.
    x ∈# mset_set (arc_walks G l)#}"
    by (intro_cong "[σ⇩1 concat_mset]" more:image_mset_cong image_mset_mset_set[symmetric] inj_onI)
     auto
  finally have 1:"mset_set (arc_walks G (l+1)) = concat_mset
    {# {# ?f x y. y ∈# mset_set (out_arcs G (arc_walk_head G x))#}. x ∈# mset_set (arc_walks G l)#}"
    by simp

  have "walks' G (l+1)=concat_mset {#{#w @ [z]. z∈# vertices_from G (last w)#}. w ∈# walks' G l#}"
    by simp
  also have "... = concat_mset {#
      {#awalk_verts (fst x) (snd x) @ [z]. z ∈# vertices_from G (awlast (fst x) (snd x))#}.
      x ∈# mset_set (arc_walks G l)#}"
    unfolding Suc by (simp add:image_mset.compositionality comp_def case_prod_beta)
  also have "... = concat_mset {#
      {#?g x @ [z]. z ∈# vertices_from G (awlast (fst x) (snd x))#}.
      x ∈# mset_set (arc_walks G l)#}"
    using arc_walks_fin
    by (intro_cong "[σ⇩1 concat_mset]" more:image_mset_cong) (auto simp: awalk_verts_unfold)
  also have "... = concat_mset {# {#?g x @ [z]. z ∈# vertices_from G (arc_walk_head G x)#}.
      x ∈# mset_set (arc_walks G l)#}"
    using arc_walks_fin awlast_of_arc_walk
    by (intro_cong "[σ⇩1 concat_mset, σ⇩2 image_mset]" more: image_mset_cong) auto
  also have "... = (concat_mset {# {# ?g (fst x, snd x@[y]).
    y ∈# mset_set (out_arcs G (arc_walk_head G x))#}. x ∈# mset_set (arc_walks G l)#})"
    unfolding verts_from_alt by (simp add:image_mset.compositionality comp_def)
  also have "... = image_mset ?g (concat_mset {# {# ?f x y.
    y ∈# mset_set (out_arcs G (arc_walk_head G x))#}. x ∈# mset_set (arc_walks G l)#})"
    unfolding image_concat_mset
    by (auto simp add:comp_def case_prod_beta image_mset.compositionality)
  also have "... = image_mset ?g (mset_set (arc_walks G (l+1)))"
    unfolding 1 by simp
  also have "... = image_mset (case_prod awalk_verts) (mset_set (arc_walks G (l+1)))"
    using arc_walks_fin by (intro image_mset_cong) (simp add:case_prod_beta awalk_verts_unfold)
  finally show ?case by simp
qed

lemma (in fin_digraph) arc_walks_map_walks:
  "walks G (l+1) = image_mset (case_prod awalk_verts) (mset_set (arc_walks G l))"
  using arc_walks_map_walks' unfolding walks_def by simp

lemma (in wf_digraph)
  assumes "awalk u a v " "length a = l" "l > 0"
  shows awalk_ends: "tail G (hd a) = u" "head G (last a) = v"
proof -
  have 0:"cas u a v"
    using assms unfolding awalk_def by simp
  have 1: "a ≠ []" using assms(2,3) by auto

  show "tail G (hd a) = u"
    using 0 unfolding cas_simp[OF 1] by auto

  show "head G (last a) = v"
    using 1 0 by (induction a arbitrary:u rule:list_nonempty_induct) auto
qed

definition graph_power :: "('a, 'b) pre_digraph ⇒ nat ⇒ ('a, ('a × 'b list)) pre_digraph"
  where "graph_power G l =
    ⦇ verts = verts G, arcs = arc_walks G l, tail = fst, head = arc_walk_head G ⦈"

lemma (in wf_digraph) graph_power_wf:
  "wf_digraph (graph_power G l)"
proof -
  have "tail (graph_power G l) a ∈ verts (graph_power G l)"
       "head (graph_power G l) a ∈ verts (graph_power G l)"
       if "a ∈ arcs (graph_power G l)" for a
    using that arc_walk_head_wellformed arc_walk_tail_wellformed
    unfolding graph_power_def by simp_all
  thus ?thesis
    unfolding wf_digraph_def by auto
qed

lemma (in fin_digraph) graph_power_fin:
  "fin_digraph (graph_power G l)"
proof -
  interpret H:wf_digraph "graph_power G l"
    using graph_power_wf by auto

  have "finite (arcs (graph_power G l))"
    using arc_walks_fin
    unfolding graph_power_def by simp

  moreover have "finite (verts (graph_power G l))"
    unfolding graph_power_def by simp
  ultimately show ?thesis
    by unfold_locales auto
qed

lemma (in fin_digraph) graph_power_count_edges:
  fixes l v w
  defines "S ≡ {x. length x=l+1∧set x⊆verts G∧hd x=v∧last x=w}"
  shows "count (edges (graph_power G l)) (v,w) = (∑x ∈ S.(∏i<l. count(edges G)(x!i,x!(i+1))))"
    (is "?L = ?R")
proof -
  interpret H:fin_digraph "graph_power G l"
    using graph_power_fin by auto

  have 0:"finite {x. set x ⊆ verts G ∧ length x = l+1}"
    by (intro finite_lists_length_eq) auto
  have fin_S: "finite S"
    unfolding S_def by (intro finite_subset[OF _ 0]) auto

  have "?L = size {#x ∈# mset_set (arc_walks G l). fst x = v ∧ arc_walk_head G x = w#}"
    unfolding graph_power_def edges_def arc_to_ends_def
    by (simp add:count_mset_exp image_mset_filter_mset_swap[symmetric])
  also have "... = size
    {#x ∈# mset_set (arc_walks G l). awhd (fst x) (snd x) = v ∧ awlast (fst x) (snd x) = w#}"
    using awlast_of_arc_walk awhd_of_arc_walk arc_walks_fin
    by (intro arg_cong[where f="size"] filter_mset_cong refl) simp
  also have "... = size {#x ∈# walks G (l+1). hd x = v ∧ last x = w#}"
    unfolding arc_walks_map_walks
    by (simp add:image_mset_filter_mset_swap[symmetric] case_prod_beta)
  also have "...=size{#x∈# walks G (l+1).x ∈ S#}"
    unfolding S_def using set_walks_3
    by (intro arg_cong[where f="size"] filter_mset_cong refl) auto
  also have "...=sum (count (walks G (l+1))) S"
    by (intro sum_count_2[symmetric] fin_S)
  also have "...=(∑x∈S.(∏i<l+1-1. count (edges G) (x!i,x!(i+1))))"
    unfolding S_def
    by (intro sum.cong refl count_walks) auto
  also have "...=?R"
    by simp
  finally show ?thesis by simp
qed

lemma (in fin_digraph) graph_power_sym_aux:
  assumes "symmetric_multi_graph G"
  assumes "v ∈ verts (graph_power G l)"  "w ∈ verts (graph_power G l)"
  shows "card (arcs_betw (graph_power G l) v w) = card (arcs_betw (graph_power G l) w v)"
    (is "?L = ?R")
proof -
  interpret H:fin_digraph "graph_power G l"
    using graph_power_fin by auto

  define S where "S v w = {x. length x=l+1 ∧ set x ⊆ verts G ∧ hd x = v ∧ last x = w}" for v w

  have 0: "bij_betw rev (S w v) (S v w)"
    unfolding S_def by (intro bij_betwI[where g="rev"]) (auto simp add:hd_rev last_rev)

  have 1: "bij_betw ((-) (l - 1)) {..<l} {..<l}"
    by (intro bij_betwI[where g="λx. (l-1-x)"]) auto

  have "?L = count (edges (graph_power G l)) (v, w)"
    unfolding H.count_edges by simp
  also have "... = (∑x ∈ S v w. (∏i<l. count (edges G) (x!i,x!(i+1))))"
    unfolding S_def graph_power_count_edges by simp
  also have "... = (∑x ∈ S w v. (∏i<l. count (edges G) (rev x!i,rev x!(i+1))))"
    by (intro sum.reindex_bij_betw[symmetric] 0)
  also have "... = (∑x ∈ S w v. (∏i<l. count (edges G) (x!((l-1-i)+1),x!(l-1-i))))"
    unfolding S_def by (intro sum.cong refl prod.cong) (simp_all add: rev_nth Suc_diff_Suc)
  also have "... = (∑x ∈ S w v. (∏i<l. count (edges G) (x!(i+1),x!i)))"
    by (intro sum.cong prod.reindex_bij_betw refl 1)
  also have "... = (∑x ∈ S w v. (∏i<l. count (edges G) (x!i,x!(i+1))))"
    by (intro sum.cong prod.cong count_edges_sym[OF assms(1)] refl)
  also have "... = count (edges (graph_power G l)) (w, v)"
    unfolding S_def graph_power_count_edges by simp
  also have "... = ?R"
    unfolding H.count_edges by simp
  finally show ?thesis by simp
qed

lemma (in fin_digraph) graph_power_sym:
  assumes "symmetric_multi_graph G"
  shows "symmetric_multi_graph (graph_power G l)"
proof -
  interpret H:fin_digraph "graph_power G l"
    using graph_power_fin by auto

  show ?thesis
    using graph_power_sym_aux[OF assms]
    unfolding symmetric_multi_graph_def by auto
qed

lemma  (in fin_digraph) graph_power_out_degree':
  assumes reg: "⋀v. v ∈ verts G ⟹ out_degree G v = d"
  assumes "v ∈ verts (graph_power G l)"
  shows "out_degree (graph_power G l) v = d ^ l"  (is "?L = ?R")
proof -
  interpret H:fin_digraph "graph_power G l"
    using graph_power_fin by auto

  have v_vert: "v ∈ verts G"
    using assms unfolding graph_power_def by simp

  have "?L = size (vertices_from (graph_power G l) v)"
    unfolding out_degree_def H.verts_from_alt by simp
  also have "... = size ({# e ∈# edges (graph_power G l). fst e = v #})"
    unfolding vertices_from_def by simp
  also have "... = size {#w ∈# mset_set (arc_walks G l). fst w = v#}"
    unfolding graph_power_def edges_def arc_to_ends_def
    by (simp add:count_mset_exp image_mset_filter_mset_swap[symmetric])
  also have "... = size {#w ∈# mset_set (arc_walks G l). awhd (fst w) (snd w) = v#}"
    using awlast_of_arc_walk awhd_of_arc_walk arc_walks_fin
    by (intro arg_cong[where f="size"] filter_mset_cong refl) simp
  also have "... = size {#x ∈# walks' G l. hd x = v #}"
    unfolding arc_walks_map_walks'
    by (simp add:image_mset_filter_mset_swap[symmetric] case_prod_beta)
  also have "... = d^l"
  proof (induction l)
    case 0
    have "size {#x ∈# walks' G 0. hd x = v#} = card {x. x = v ∧ x ∈ verts G}"
      by (simp add:image_mset_filter_mset_swap[symmetric])
    also have "... = card {v}"
      using v_vert by (intro arg_cong[where f="card"]) auto
    also have "... = d^0" by simp
    finally show ?case by simp
  next
    case (Suc l)
    have "size {#x ∈# walks' G (Suc l). hd x = v#} =
      (∑x∈#walks' G l. size {#y ∈# vertices_from G (last x). hd (x @ [y]) = v#})"
      by (simp add:size_concat_mset image_mset_filter_mset_swap[symmetric]
          filter_concat_mset image_mset.compositionality comp_def)
    also have "... = (∑x∈#walks' G l. size {#y ∈# vertices_from G (last x). hd x = v#})"
      using set_walks_2
      by (intro_cong "[σ⇩1 sum_mset, σ⇩1 size]" more:image_mset_cong filter_mset_cong) auto
    also have "... = (∑x∈#walks' G l. (if hd x = v then out_degree G (last x) else 0))"
      unfolding verts_from_alt out_degree_def
      by (simp add:filter_mset_const if_distribR if_distrib cong:if_cong)
    also have "... = (∑x∈#walks' G l. d * of_bool (hd x = v))"
      using set_walks_2[where l="l"] last_in_set
      by (intro arg_cong[where f="sum_mset"] image_mset_cong) (auto intro!:reg)
    also have "... = d * (∑x∈#walks' G l. of_bool (hd x = v))"
      by (simp add:sum_mset_distrib_left image_mset.compositionality comp_def)
    also have "... = d * (size {#x ∈# walks' G l. hd x = v#})"
      by (simp add:size_filter_mset_conv)
    also have "... = d * d ^ l"
      using Suc by simp
    also have "... = d^Suc l"
      by simp
    finally show ?case by simp
  qed

  finally show ?thesis by simp
qed

lemma  (in regular_graph) graph_power_out_degree:
  assumes "v ∈ verts (graph_power G l)"
  shows "out_degree (graph_power G l) v = d ^ l"  (is "?L = ?R")
  by (intro graph_power_out_degree' assms reg) auto

lemma (in regular_graph) graph_power_regular:
  "regular_graph (graph_power G l)"
proof -
  interpret H:fin_digraph "graph_power G l"
    using graph_power_fin by auto

  have "verts (graph_power G l) ≠ {}"
    using verts_non_empty unfolding graph_power_def by simp

  moreover have "0 < d^l"
    using d_gt_0 by simp

  ultimately show ?thesis
    using graph_power_out_degree
    by (intro regular_graphI[where d="d^l"] graph_power_sym sym)
qed

lemma (in regular_graph) graph_power_degree:
  "regular_graph.d (graph_power G l) = d^l" (is "?L = ?R")
proof -
  interpret H:regular_graph "graph_power G l"
    using graph_power_regular by auto
  obtain v where v_set: "v ∈ verts (graph_power G l)"
    using H.verts_non_empty by auto
  hence "?L = out_degree (graph_power G l) v"
    using v_set H.reg by auto
  also have "... =?R"
    by (intro graph_power_out_degree[OF v_set])
  finally show ?thesis by simp
qed

lemma (in regular_graph) graph_power_step:
  assumes "x ∈ verts G"
  shows "regular_graph.g_step (graph_power G l) f x = (g_step^^l) f x"
  using assms
proof (induction l arbitrary: x)
  case 0
  let ?H = "graph_power G 0"
  interpret H:regular_graph "?H"
    using graph_power_regular by auto
  have "regular_graph.g_step (graph_power G 0) f x = H.g_step f x"
    by simp
  have "H.g_step f x = (∑x∈in_arcs ?H x. f (tail ?H x))"
    unfolding H.g_step_def graph_power_degree by simp
  also have "... = (∑v∈{e ∈ arc_walks G 0. arc_walk_head G e = x}. f (fst v))"
    unfolding in_arcs_def graph_power_def by (simp add:case_prod_beta)
  also have "... = (∑v∈{x}. f v)"
    unfolding arc_walks_def using 0
    by (intro sum.reindex_bij_betw bij_betwI[where g="(λx. (x,[]))"])
      (auto simp add:arc_walk_head_def)
  also have "... = f x"
    by simp
  also have "... = (g_step^^0) f x"
    by simp
  finally show ?case by simp
next
  case (Suc l)
  let ?H = "graph_power G l"
  interpret H:regular_graph "?H"
    using graph_power_regular by auto
  let ?HS = "graph_power G (l+1)"
  interpret HS:regular_graph "?HS"
    using graph_power_regular by auto

  let ?bij = "(λ(x,(y1,y2)). (y1,y2@[x]))"
  let ?bijr = "(λ(y1,y2). (last y2, (y1,butlast y2)))"

  define S where "S = {y. fst y ∈ in_arcs G x ∧ snd y ∈ in_arcs ?H (tail G (fst y))}"

  have "S = {(u,v). u ∈ arcs G ∧ head G u = x ∧ v ∈ arc_walks G l ∧ arc_walk_head G v = tail G u}"
    unfolding S_def graph_power_def in_arcs_def by auto
  also have "... = {(u,v). (fst v,snd v@[u]) ∈ arc_walks G (l+1) ∧ arc_walk_head G (fst v,snd v@[u]) = x}"
    unfolding arc_walks_def by (intro iffD2[OF set_eq_iff] allI)
      (auto simp add: is_arc_walk_snoc case_prod_beta arc_walk_head_def)
  also have "... = {(u,v). (fst v,snd v@[u]) ∈ in_arcs ?HS x}"
    unfolding in_arcs_def graph_power_def by auto
  finally have S_alt: "S = {(u,v). (fst v,snd v@[u]) ∈ in_arcs ?HS x}" by simp

  have len_in_arcs: "a ∈ in_arcs ?HS x ⟹ snd a ≠ []" for a
    unfolding in_arcs_def graph_power_def arc_walks_def by auto

  have 0:"bij_betw ?bij S (in_arcs ?HS x)"
    unfolding S_alt using len_in_arcs
    by (intro bij_betwI[where g="?bijr"]) auto

  have "HS.g_step f x = (∑y∈in_arcs ?HS x. f (tail ?HS y)/ d^(l+1))"
    unfolding HS.g_step_def graph_power_degree by simp
  also have "... = (∑y∈in_arcs ?HS x. f (fst y)/ d^(l+1))"
    unfolding graph_power_def by simp
  also have "... = (∑y ∈ S. f (fst (?bij y))/ d^(l+1))"
    by (intro sum.reindex_bij_betw[symmetric] 0)
  also have "... = (∑y ∈ S. f (fst (snd y))/ d^(l+1))"
    by (intro_cong "[σ⇩2 (/),σ⇩1 f]" more: sum.cong) (simp add:case_prod_beta)
  also have "...=(∑y∈(⋃a∈in_arcs G x. (Pair a)`in_arcs ?H (tail G a)). f (fst (snd y))/ d^(l+1))"
    unfolding S_def by (intro sum.cong) auto
  also have "...=(∑a∈in_arcs G x. (∑y∈(Pair a)`in_arcs ?H (tail G a). f (fst (snd y))/ d^(l+1)))"
    by (intro sum.UNION_disjoint) auto
  also have "... = (∑a ∈ in_arcs G x. (∑b ∈ in_arcs ?H (tail G a). f (fst b) / d^(l+1)))"
    by (intro sum.cong sum.reindex_bij_betw) (auto simp add:bij_betw_def inj_on_def image_iff)
  also have "... = (∑a ∈ in_arcs G x. (∑b ∈ in_arcs ?H (tail G a). f (tail ?H b) / d^l)/d)"
    unfolding graph_power_def
    by (simp add:sum_divide_distrib algebra_simps)
  also have "... = (∑a ∈ in_arcs G x. H.g_step f (tail G a)/ d)"
    unfolding H.g_step_def graph_power_degree by simp
  also have "... = (∑a ∈ in_arcs G x. (g_step^^l) f (tail G a)/ d)"
    by (intro sum.cong refl arg_cong2[where f="(/)"] Suc) auto
  also have "... = g_step ((g_step^^l) f) x"
    unfolding g_step_def by simp
  also have "... = (g_step^^(l+1)) f x"
    by simp
  finally show ?case by simp
qed

lemma (in regular_graph) graph_power_expansion:
  "regular_graph.Λ⇩a (graph_power G l) ≤ Λ⇩a^l"
proof -
  interpret H:regular_graph "graph_power G l"
    using graph_power_regular by auto

  have "¦H.g_inner f (H.g_step f)¦ ≤ Λ⇩a ^ l * (H.g_norm f)⇧2" (is "?L ≤ ?R")
    if "H.g_inner f (λ_. 1) = 0"  for f
  proof -
    have "g_inner f (λ_. 1) = H.g_inner f (λ_.1)"
      unfolding g_inner_def H.g_inner_def
      by (intro sum.cong) (auto simp add:graph_power_def)
    also have "... = 0" using that by simp
    finally have 1:"g_inner f (λ_. 1) = 0" by simp

    have 2: "g_inner ((g_step^^l) f) (λ_. 1) = 0" for l
      using g_step_remains_orth 1 by (induction l, auto)

    have 0: "g_norm ((g_step^^l) f) ≤ Λ⇩a ^ l * g_norm f"
    proof (induction l)
      case 0
      then show ?case by simp
    next
      case (Suc l)
      have "g_norm ((g_step ^^ Suc l) f) = g_norm (g_step ((g_step ^^ l) f))"
        by simp
      also have "... ≤ Λ⇩a * g_norm (((g_step ^^ l) f))"
        by (intro expansionD2 2)
      also have "... ≤ Λ⇩a * (Λ⇩a^l * g_norm f)"
        by (intro mult_left_mono Λ_ge_0 Suc)
      also have "... = Λ⇩a^(l+1) * g_norm f" by simp
      finally show ?case by simp
    qed

    have "?L = ¦g_inner f (H.g_step f)¦"
      unfolding H.g_inner_def g_inner_def
      by (intro_cong "[σ⇩1 abs]" more:sum.cong) (auto simp add:graph_power_def)
    also have "... = ¦g_inner f ((g_step^^l) f)¦"
      by (intro_cong "[σ⇩1 abs]" more:g_inner_cong graph_power_step) auto
    also have "... ≤ g_norm f * g_norm ((g_step^^l) f)"
      by (intro g_inner_cauchy_schwartz)
    also have "... ≤ g_norm f * (Λ⇩a ^ l * g_norm f)"
      by (intro mult_left_mono 0 g_norm_nonneg)
    also have "... = Λ⇩a ^ l * g_norm f^2"
      by (simp add:power2_eq_square)
    also have "... = ?R"
      unfolding g_norm_sq H.g_norm_sq g_inner_def H.g_inner_def
      by (intro_cong "[σ⇩2 (*)]" more:sum.cong) (auto simp add:graph_power_def)
    finally show ?thesis by simp
  qed
  moreover have " 0 ≤ Λ⇩a ^ l"
    using Λ_ge_0 by simp

  ultimately show ?thesis
    by (intro H.expander_intro_1) auto
qed

unbundle no intro_cong_syntax

end