Theory 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))"

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"

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)))"
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))"
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)#}"
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
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
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
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
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'
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}"
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#})"
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))"
also have "... = d * (size {#x ∈# walks' G l. hd x = v#})"
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,[]))"])
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)
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
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"
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`