section ‹Strongly Explicit Expander Graphs\label{sec:see}› text ‹In some applications, representing an expander graph using a data structure (for example as an adjacency lists) would be prohibitive. For such cases strongly explicit expander graphs (SEE) are relevant. These are expander graphs, which can be represented implicitly using a function that computes for each vertex its neighbors in space and time logarithmic w.r.t. to the size of the graph. An application can for example sample a random walk, from a SEE using such a function efficiently. An example of such a graph is the Margulis construction from Section~\ref{sec:margulis}. This section presents the latter as a SEE but also shows that two graph operations that preserve the SEE property, in particular the graph power construction from Section~\ref{sec:graph_power} and a compression scheme introduced by Murtagh et al.~\cite[Theorem~20]{murtagh2019}. Combining all of the above it is possible to construct strongly explicit expander graphs of \emph{every size} and spectral gap.› theory Expander_Graphs_Strongly_Explicit imports Expander_Graphs_Power_Construction Expander_Graphs_MGG begin unbundle intro_cong_syntax no_notation Digraph.dominates ("_ →ı _" [100,100] 40) record strongly_explicit_expander = see_size :: nat see_degree :: nat see_step :: "nat ⇒ nat ⇒ nat" definition graph_of :: "strongly_explicit_expander ⇒ (nat, (nat,nat) arc) pre_digraph" where "graph_of e = ⦇ verts = {..<see_size e}, arcs = (λ(v, i). Arc v (see_step e i v) i) ` ({..<see_size e} × {..<see_degree e}), tail = arc_tail, head = arc_head ⦈" definition "is_expander e Λ⇩_{a}⟷ regular_graph (graph_of e) ∧ regular_graph.Λ⇩_{a}(graph_of e) ≤ Λ⇩_{a}" lemma is_expander_mono: assumes "is_expander e a" "a ≤ b" shows "is_expander e b" using assms unfolding is_expander_def by auto lemma graph_of_finI: assumes "see_step e ∈ ({..<see_degree e} → ({..<see_size e} → {..<see_size e}))" shows "fin_digraph (graph_of e)" proof - let ?G = "graph_of e" have "head ?G a ∈ verts ?G ∧ tail ?G a ∈ verts ?G" if "a ∈ arcs ?G" for a using assms that unfolding graph_of_def by (auto simp add:Pi_def) hence 0: "wf_digraph ?G" unfolding wf_digraph_def by auto have 1: "finite (verts ?G)" unfolding graph_of_def by simp have 2: "finite (arcs ?G)" unfolding graph_of_def by simp show ?thesis using 0 1 2 unfolding fin_digraph_def fin_digraph_axioms_def by auto qed lemma edges_graph_of: "edges(graph_of e)={#(v,see_step e i v). (v,i)∈#mset_set ({..<see_size e}×{..<see_degree e})#}" proof - have 0:"mset_set ((λ(v, i). Arc v (see_step e i v) i) ` ({..<see_size e} × {..<see_degree e})) = {# Arc v (see_step e i v) i. (v,i) ∈# mset_set ( {..<see_size e} × {..<see_degree e})#}" by (intro image_mset_mset_set[symmetric] inj_onI) auto have "edges (graph_of e) = {#(fst p, see_step e (snd p) (fst p)). p ∈# mset_set ({..<see_size e} × {..<see_degree e})#}" unfolding edges_def graph_of_def arc_to_ends_def using 0 by (simp add:image_mset.compositionality comp_def case_prod_beta) also have "... = {#(v, see_step e i v). (v,i) ∈# mset_set ({..<see_size e} × {..<see_degree e})#}" by (intro image_mset_cong) auto finally show ?thesis by simp qed lemma out_degree_see: assumes "v ∈ verts (graph_of e)" shows "out_degree (graph_of e) v = see_degree e" (is "?L = ?R") proof - let ?d = "see_degree e" let ?n = "see_size e" have 0: "v < ?n" using assms unfolding graph_of_def by simp have "?L = card {a. (∃x∈{..<?n}. ∃y∈{..<?d}. a = Arc x (see_step e y x) y) ∧ arc_tail a = v}" unfolding out_degree_def out_arcs_def graph_of_def by (simp add:image_iff) also have "... = card {a. (∃y∈{..<?d}. a = Arc v (see_step e y v) y)}" using 0 by (intro arg_cong[where f="card"]) auto also have "... = card ((λy. Arc v (see_step e y v) y) ` {..<?d})" by (intro arg_cong[where f="card"] iffD2[OF set_eq_iff]) (simp add:image_iff) also have "... = card {..<?d}" by (intro card_image inj_onI) auto also have "... = ?d" by simp finally show ?thesis by simp qed lemma card_arc_walks_see: assumes "fin_digraph (graph_of e)" shows "card (arc_walks (graph_of e) n) = see_degree e^n * see_size e" (is "?L = ?R") proof - let ?G = "graph_of e" interpret fin_digraph ?G using assms by auto have "?L = card (⋃v ∈ verts ?G. {x. fst x = v ∧ is_arc_walk ?G v (snd x) ∧ length (snd x) = n})" unfolding arc_walks_def by (intro arg_cong[where f="card"]) auto also have "... = (∑v ∈ verts ?G. card {x. fst x=v∧is_arc_walk ?G v (snd x)∧length (snd x) = n})" using is_arc_walk_set[where G="?G"] by (intro card_UN_disjoint ballI finite_cartesian_product subsetI finite_lists_length_eq finite_subset[where B="verts ?G × {x. set x ⊆ arcs ?G ∧ length x = n}"]) force+ also have "... = (∑v ∈ verts ?G. out_degree (graph_power ?G n) v)" unfolding out_degree_def graph_power_def out_arcs_def arc_walks_def by (intro sum.cong arg_cong[where f="card"]) auto also have "... = (∑v ∈ verts ?G. see_degree e^n)" by (intro sum.cong graph_power_out_degree' out_degree_see refl) (simp_all add: graph_power_def) also have "... = ?R" by (simp add:graph_of_def) finally show ?thesis by simp qed lemma regular_graph_degree_eq_see_degree: assumes "regular_graph (graph_of e)" shows "regular_graph.d (graph_of e) = see_degree e" (is "?L = ?R") proof - interpret regular_graph "graph_of e" using assms(1) by simp obtain v where v_set: "v ∈ verts (graph_of e)" using verts_non_empty by auto hence "?L = out_degree (graph_of e) v" using v_set reg by auto also have "... = see_degree e" by (intro out_degree_see v_set) finally show ?thesis by simp qed text ‹The following introduces the compression scheme, described in \cite[Theorem 20]{murtagh2019}.› fun see_compress :: "nat ⇒ strongly_explicit_expander ⇒ strongly_explicit_expander" where "see_compress m e = ⦇ see_size = m, see_degree = see_degree e * 2 , see_step = (λk v. if k < see_degree e then (see_step e k v) mod m else (if v+m < see_size e then (see_step e (k-see_degree e) (v+m)) mod m else v)) ⦈" lemma edges_of_compress: fixes e m assumes "2*m ≥ see_size e" "m ≤ see_size e" defines "A ≡ {# (x mod m, y mod m). (x,y) ∈# edges (graph_of e)#}" defines "B ≡ repeat_mset (see_degree e) {# (x,x). x ∈# (mset_set {see_size e - m..<m})#}" shows "edges (graph_of (see_compress m e)) = A + B" (is "?L = ?R") proof - let ?d = "see_degree e" let ?c = "see_step (see_compress m e)" let ?n = "see_size e" let ?s = "see_step e" have 7:"m ≤ v ⟹ v < ?n ⟹ v - m = v mod m" for v using assms by (simp add: le_mod_geq) let ?M = "mset_set ({..<m}×{..<2*?d})" define M1 where "M1 = mset_set ({..<m} × {..<?d})" define M2 where "M2 = mset_set ({..<?n-m} × {?d..<2*?d})" define M3 where "M3 = mset_set ({?n-m..<m} × {?d..<2*?d})" have "M2 = mset_set ((λ(x,y). (x-m,y+?d)) ` ({m..<?n} × {..<?d}))" using assms(2) unfolding M2_def map_prod_def[symmetric] atLeast0LessThan[symmetric] by (intro arg_cong[where f="mset_set"] map_prod_surj_on[symmetric]) (simp_all add: image_minus_const_atLeastLessThan_nat mult_2) also have "... = image_mset (λ(x,y). (x-m,y+?d)) (mset_set ({m..<?n} × {..<?d}))" by (intro image_mset_mset_set[symmetric] inj_onI) auto finally have M2_eq: "M2 = image_mset (λ(x,y). (x-m,y+?d)) (mset_set ({m..<?n} × {..<?d}))" by simp have "?M = mset_set ({..<m}×{..<?d} ∪ {..<?n-m}×{?d..<2*?d} ∪ {?n-m..<m}×{?d..<2*?d})" using assms(1,2) by (intro arg_cong[where f="mset_set"]) auto also have "... = mset_set ({..<m}×{..<?d} ∪ {..<?n-m}×{?d..<2*?d}) + M3" unfolding M3_def by (intro mset_set_Union) auto also have "... = M1 + M2 + M3" unfolding M1_def M2_def by (intro arg_cong2[where f="(+)"] mset_set_Union) auto finally have 0:"mset_set ({..<m} × {..<2*?d}) = M1 + M2 + M3" by simp have 1:"{#(v,?c i v). (v,i)∈#M1#}={#(v mod m,?s i v mod m). (v,i)∈#mset_set ({..<m}×{..<?d})#}" unfolding M1_def by (intro image_mset_cong) auto have "{#(v,?c i v).(v,i)∈#M2#}={#(fst x-m,?c(snd x+?d)(fst x-m)).x∈#mset_set({m..<?n}×{..<?d})#}" unfolding M2_eq by (simp add:image_mset.compositionality comp_def case_prod_beta del:see_compress.simps) also have "... = {#(v - m,?s i v mod m). (v,i)∈#mset_set ({m..<?n}×{..<?d})#}" by (intro image_mset_cong) auto also have "... = {#(v mod m,?s i v mod m). (v,i)∈#mset_set ({m..<?n}×{..<?d})#}" using 7 by (intro image_mset_cong) auto finally have 2: "{#(v,?c i v). (v,i)∈#M2#}={#(v mod m,?s i v mod m). (v,i)∈#mset_set ({m..<?n}×{..<?d})#}" by simp have "{#(v,?c i v). (v,i)∈#M3#} = {#(v,v). (v,i) ∈# mset_set ({?n-m..<m} × {?d..<2*?d})#}" unfolding M3_def by (intro image_mset_cong) auto also have "... = concat_mset {#{#(x, x). xa ∈# mset_set {?d..<2 * ?d}#}. x ∈# mset_set {?n - m..<m}#}" by (subst mset_prod_eq) (auto simp:image_mset.compositionality image_concat_mset comp_def) also have "... = concat_mset {#replicate_mset ?d (x, x). x ∈# mset_set {?n - m..<m}#}" unfolding image_mset_const_eq by simp also have "... = B" unfolding B_def repeat_image_concat_mset by simp finally have 3:"{#(v,?c i v). (v,i)∈#M3#}=B" by simp have "A = {#(fst x mod m, ?s (snd x) (fst x) mod m). x ∈# mset_set ({..<?n} × {..<?d})#}" unfolding A_def edges_graph_of by (simp add:image_mset.compositionality comp_def case_prod_beta) also have "... = {#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<?n}×{..<?d})#}" by (intro image_mset_cong) auto finally have 4: "A = {#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<?n}×{..<?d})#}" by simp have "?L = {# (v, ?c i v). (v,i) ∈# ?M #}" unfolding edges_graph_of by (simp add:ac_simps) also have "... = {#(v,?c i v). (v,i)∈#M1#}+{#(v,?c i v). (v,i)∈#M2#}+{#(v,?c i v). (v,i)∈#M3#}" unfolding 0 image_mset_union by simp also have "...={#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<m}×{..<?d}∪{m..<?n}×{..<?d})#}+B" unfolding 1 2 3 image_mset_union[symmetric] by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}image_mset]" more: mset_set_Union[symmetric]) auto also have "...={#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<?n}×{..<?d})#}+B" using assms(2) by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}image_mset, σ⇩_{1}mset_set]") auto also have "... = A + B" unfolding 4 by simp finally show ?thesis by simp qed lemma see_compress_sym: assumes "2*m ≥ see_size e" "m ≤ see_size e" assumes "symmetric_multi_graph (graph_of e)" shows "symmetric_multi_graph (graph_of (see_compress m e))" proof - let ?c = "see_compress m e" let ?d = "see_degree e" let ?G = "graph_of e" let ?H = "graph_of (see_compress m e)" interpret G:"fin_digraph" "?G" by (intro symmetric_multi_graphD2[OF assms(3)]) interpret H:"fin_digraph" "?H" by (intro graph_of_finI) simp have deg_compres: "see_degree ?c = 2 * see_degree e" by simp have 1: "card (arcs_betw ?H v w) = card (arcs_betw ?H w v)" (is "?L = ?R") if "v ∈ verts ?H" "w ∈ verts ?H" for v w proof - define b where "b =count {#(x, x). x ∈# mset_set {see_size e - m..<m}#} (v, w)" have b_alt_def: "b = count {#(x, x). x ∈# mset_set {see_size e - m..<m}#} (w, v)" unfolding b_def count_mset_exp by (simp add:case_prod_beta image_mset_filter_mset_swap[symmetric] ac_simps) have "?L = count (edges ?H) (v,w)" unfolding H.count_edges by simp also have "... = count {#(x mod m, y mod m). (x, y) ∈# edges (graph_of e)#} (v, w) + ?d * b" unfolding edges_of_compress[OF assms(1,2)] b_def by simp also have "... = count {#(snd e mod m, fst e mod m). e ∈# edges (graph_of e)#} (v, w) + ?d * b" by (subst G.edges_sym[OF assms(3),symmetric]) (simp add:image_mset.compositionality comp_def case_prod_beta) also have "... = count {#(x mod m, y mod m). (x,y) ∈# edges (graph_of e)#} (w, v) + ?d * b" unfolding count_mset_exp by (simp add:image_mset_filter_mset_swap[symmetric] ac_simps case_prod_beta) also have "... = count (edges ?H) (w,v)" unfolding edges_of_compress[OF assms(1,2)] b_alt_def by simp also have "... = ?R" unfolding H.count_edges by simp finally show ?thesis by simp qed show ?thesis using 1 H.fin_digraph_axioms unfolding symmetric_multi_graph_def by auto qed lemma see_compress: assumes "is_expander e Λ⇩_{a}" assumes "2*m ≥ see_size e" "m ≤ see_size e" shows "is_expander (see_compress m e) (Λ⇩_{a}/2 + 1/2)" proof - let ?H = "graph_of (see_compress m e)" let ?G = "graph_of e" let ?d = "see_degree e" let ?n = "see_size e" interpret G:regular_graph "graph_of e" using assms(1) is_expander_def by simp have d_eq: "?d = G.d" using regular_graph_degree_eq_see_degree[OF G.regular_graph_axioms] by simp have n_eq: "G.n = ?n" unfolding G.n_def by (simp add:graph_of_def) have n_gt_1: "?n > 0" using G.n_gt_0 n_eq by auto have "symmetric_multi_graph (graph_of (see_compress m e))" by (intro see_compress_sym assms(2,3) G.sym) moreover have "see_size e > 0" using G.verts_non_empty unfolding graph_of_def by auto hence "m > 0" using assms(2) by simp hence "verts (graph_of (see_compress m e)) ≠ {}" unfolding graph_of_def by auto moreover have 1:"0 < see_degree e" using d_eq G.d_gt_0 by auto hence "0 < see_degree (see_compress m e)" by simp ultimately have 0:"regular_graph ?H" by (intro regular_graphI[where d="see_degree (see_compress m e)"] out_degree_see) auto interpret H:regular_graph ?H using 0 by auto have "¦∑a∈arcs ?H. f (head ?H a) * f (tail ?H a)¦ ≤ (real G.d * G.Λ⇩_{a}+ G.d) * (H.g_norm f)⇧^{2}" (is "?L ≤ ?R") if "H.g_inner f (λ_. 1) = 0" for f proof - define f' where "f' x = f (x mod m)" for x let ?L1 = "G.g_norm f'^2 + ¦∑x=?n-m..<m. f x^2¦" let ?L2 = "G.g_inner f' (λ_.1)^2/ G.n + ¦∑x=?n-m..<m. f x^2¦" have "?L1 = (∑x<?n. f (x mod m)^2) + ¦∑x=?n-m..<m. f x^2¦" unfolding G.g_norm_sq G.g_inner_def f'_def by (simp add:graph_of_def power2_eq_square) also have "... = (∑x∈{0..<m} ∪ {m..<?n}. f (x mod m)^2) + (∑x=?n-m..<m. f x^2)" using assms(3) by (intro_cong "[σ⇩_{2}(+)]" more:sum.cong abs_of_nonneg sum_nonneg) auto also have "...=(∑x=0..<m. f (x mod m)^2) + (∑x=m..<?n. f (x mod m)^2) + (∑x=?n-m..<m. f x^2)" by (intro_cong "[σ⇩_{2}(+)]" more:sum.union_disjoint) auto also have "... = (∑x=0..<m. f (x mod m)^2) + (∑x=0..<?n-m. f x^2) + (∑x=?n-m..<m. f x^2)" using assms(2,3) by (intro_cong "[σ⇩_{2}(+)]" more: sum.reindex_bij_betw bij_betwI[where g="(λx. x+m)"]) (auto simp add:le_mod_geq) also have "... = (∑x=0..<m. f x^2) + (∑x=0..<?n-m. f x^2) + (∑x=?n-m..<m. f x^2)" by (intro sum.cong arg_cong2[where f="(+)"]) auto also have "... = (∑x=0..<m. f x^2) + ((∑x=0..<?n-m. f x^2) + (∑x=?n-m..<m. f x^2))" by simp also have "... = (∑x=0..<m. f x^2) + (∑x∈{0..<?n-m}∪{?n-m..<m}. f x^2)" by (intro sum.union_disjoint[symmetric] arg_cong2[where f="(+)"]) auto also have "... = (∑x<m. f x^2) + (∑x<m. f x^2)" using assms(2,3) by (intro arg_cong2[where f="(+)"] sum.cong) auto also have " ... = 2 * H.g_norm f^2" unfolding mult_2 H.g_norm_sq H.g_inner_def by (simp add:graph_of_def power2_eq_square) finally have 2:"?L1 = 2 * H.g_norm f^2" by simp have "?L2 = (∑x∈{..<m}∪{m..<?n}. f (x mod m))^2/G.n + (∑x=?n-m..<m. f x^2)" unfolding G.g_inner_def f'_def using assms(2,3) by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}(/), σ⇩_{2}(power)]" more: sum.cong abs_of_nonneg sum_nonneg) (auto simp add:graph_of_def) also have "...=((∑x<m. f (x mod m))+(∑x=m..<?n. f (x mod m)))^2/G.n + (∑x=?n-m..<m. f x^2)" by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}(/), σ⇩_{2}(power)]" more:sum.union_disjoint) auto also have "...=((∑x<m. f (x mod m))+(∑x=0..<?n-m. f x))^2/G.n + (∑x=?n-m..<m. f x^2)" using assms(2,3) by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}(/), σ⇩_{2}(power)]" more:sum.reindex_bij_betw bij_betwI[where g="(λx. x+m)"]) (auto simp add:le_mod_geq) also have "...=(H.g_inner f (λ_. 1) +(∑x<?n-m. f x))^2/G.n + (∑x=?n-m..<m. f x^2)" unfolding H.g_inner_def by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}(/), σ⇩_{2}(power)]" more: sum.cong) (auto simp:graph_of_def) also have "...=(∑x<?n-m. f x)^2/G.n + (∑x=?n-m..<m. f x^2)" unfolding that by simp also have "...≤ (∑x<?n-m. ¦f x¦ * ¦1¦)^2/G.n + (∑x=?n-m..<m. f x^2)" by (intro add_mono divide_right_mono iffD1[OF abs_le_square_iff]) auto also have "... ≤ (L2_set f {..<?n-m} * L2_set (λ_. 1) {..<?n-m})^2/G.n + (∑x=?n-m..<m. f x^2)" by (intro add_mono divide_right_mono power_mono L2_set_mult_ineq sum_nonneg) auto also have "... = ((∑x <?n-m. f x^2) * (?n-m))/G.n + (∑x=?n-m..<m. f x^2)" unfolding power_mult_distrib L2_set_def real_sqrt_mult by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}(/),σ⇩_{2}(*)]" more:real_sqrt_pow2 sum_nonneg) auto also have "... = (∑x <?n-m. f x^2) * ((?n-m)/?n) + (∑x=?n-m..<m. f x^2)" unfolding n_eq by simp also have "... ≤ (∑x <?n-m. f x^2) * 1 + (∑x=?n-m..<m. f x^2)" using assms(3) n_gt_1 by (intro mult_left_mono add_mono sum_nonneg) auto also have "... = (∑x∈{..<?n-m}∪{?n-m..<m}. f x^2)" unfolding mult_1_right by (intro sum.union_disjoint[symmetric]) auto also have "... = H.g_norm f^2" using assms(2,3) unfolding H.g_norm_sq H.g_inner_def by (intro sum.cong) (auto simp add:graph_of_def power2_eq_square) finally have 3:"?L2 ≤ H.g_norm f^2" by simp have "?L = ¦∑(u, v)∈#edges ?H. f v * f u¦" unfolding edges_def arc_to_ends_def sum_unfold_sum_mset by (simp add:image_mset.compositionality comp_def del:see_compress.simps) also have "...=¦(∑x ∈# edges ?G.f(snd x mod m)*f(fst x mod m))+(∑x=?n-m..<m.?d*(f x^2))¦" unfolding edges_of_compress[OF assms(2,3)] sum_unfold_sum_mset by (simp add:image_mset.compositionality sum_mset_repeat comp_def case_prod_beta power2_eq_square del:see_compress.simps) also have "...=¦(∑(u,v) ∈# edges ?G.f(u mod m)*f(v mod m))+(∑x=?n-m..<m.?d*(f x^2))¦" by (intro_cong "[σ⇩_{1}abs, σ⇩_{2}(+), σ⇩_{1}sum_mset]" more:image_mset_cong) (simp_all add:case_prod_beta) also have "... ≤ ¦∑(u,v) ∈# edges ?G.f(u mod m)*f(v mod m)¦+¦∑x=?n-m..<m.?d*(f x^2)¦ " by (intro abs_triangle_ineq) also have "... = ?d * (¦∑(u,v) ∈# edges ?G.f(v mod m)*f(u mod m)¦/G.d+¦∑x=?n-m..<m.(f x^2)¦)" unfolding d_eq using G.d_gt_0 by (simp add:divide_simps ac_simps sum_distrib_left[symmetric] abs_mult) also have "... = ?d * (¦G.g_inner f' (G.g_step f')¦ + ¦∑x=?n-m..<m. f x^2¦)" unfolding G.g_inner_step_eq sum_unfold_sum_mset edges_def arc_to_ends_def f'_def by (simp add:image_mset.compositionality comp_def del:see_compress.simps) also have "...≤ ?d * ((G.Λ⇩_{a}* G.g_norm f'^2 + (1-G.Λ⇩_{a})*G.g_inner f' (λ_.1)^2/ G.n) + ¦∑x=?n-m..<m. f x^2¦)" by (intro add_mono G.expansionD3 mult_left_mono) auto also have "... = ?d * (G.Λ⇩_{a}* ?L1 + (1 - G.Λ⇩_{a}) * ?L2)" by (simp add:algebra_simps) also have "... ≤ ?d * (G.Λ⇩_{a}* (2 * H.g_norm f^2) + (1-G.Λ⇩_{a}) * H.g_norm f^2)" unfolding 2 using G.Λ_ge_0 G.Λ_le_1 by (intro mult_left_mono add_mono 3) auto also have "... = ?R" unfolding d_eq[symmetric] by (simp add:algebra_simps) finally show ?thesis by simp qed hence "H.Λ⇩_{a}≤ (G.d*G.Λ⇩_{a}+G.d)/H.d" using G.d_gt_0 G.Λ_ge_0 by (intro H.expander_intro) (auto simp del:see_compress.simps) also have "... = (see_degree e * G.Λ⇩_{a}+ see_degree e) / (2* see_degree e)" unfolding d_eq[symmetric] regular_graph_degree_eq_see_degree[OF H.regular_graph_axioms] by simp also have "... = G.Λ⇩_{a}/2 + 1/2" using 1 by (simp add:field_simps) also have "... ≤ Λ⇩_{a}/2 + 1/2" using assms(1) unfolding is_expander_def by simp finally have "H.Λ⇩_{a}≤ Λ⇩_{a}/2 + 1/2" by simp thus ?thesis unfolding is_expander_def using 0 by simp qed text ‹The graph power of a strongly explicit expander graph is itself a strongly explicit expander graph.› fun to_digits :: "nat ⇒ nat ⇒ nat ⇒ nat list" where "to_digits _ 0 _ = []" | "to_digits b (Suc l) k = (k mod b)# to_digits b l (k div b)" fun from_digits :: "nat ⇒ nat list ⇒ nat" where "from_digits b [] = 0" | "from_digits b (x#xs) = x + b * from_digits b xs" lemma to_from_digits: assumes "length xs = n" "set xs ⊆ {..<b}" shows "to_digits b n (from_digits b xs) = xs" proof - have "to_digits b (length xs) (from_digits b xs) = xs" using assms(2) by (induction xs, auto) thus ?thesis unfolding assms(1) by auto qed lemma from_digits_range: assumes "length xs = n" "set xs ⊆ {..<b}" shows "from_digits b xs < b^n" proof (cases "b > 0") case True have "from_digits b xs ≤ b^length xs - 1" using assms(2) proof (induction xs) case Nil then show ?case by simp next case (Cons a xs) have "from_digits b (a # xs) = a + b * from_digits b xs" by simp also have "... ≤ (b-1) + b * from_digits b xs" using Cons by (intro add_mono) auto also have "... ≤ (b-1) + b * (b^length xs-1)" using Cons(2) by (intro add_mono mult_left_mono Cons(1)) auto also have "... = b^length (a#xs) - 1" using True by (simp add:algebra_simps) finally show "from_digits b (a # xs) ≤ b^length (a#xs) - 1" by simp qed also have "... < b^n" using True assms(1) by simp finally show ?thesis by simp next case False hence "b = 0" by simp hence "xs = []" using assms(2) by simp thus ?thesis using assms(1) by simp qed lemma from_digits_inj: "inj_on (from_digits b) {xs. set xs ⊆ {..<b} ∧ length xs = n}" by (intro inj_on_inverseI[where g="to_digits b n"] to_from_digits) auto fun see_power :: "nat ⇒ strongly_explicit_expander ⇒ strongly_explicit_expander" where "see_power l e = ⦇ see_size = see_size e, see_degree = see_degree e^l , see_step = (λk v. foldl (λy x. see_step e x y) v (to_digits (see_degree e) l k)) ⦈" lemma graph_power_iso_see_power: assumes "fin_digraph (graph_of e)" shows "digraph_iso (graph_power (graph_of e) n) (graph_of (see_power n e))" proof - let ?G = "graph_of e" let ?P = "graph_power (graph_of e) n" let ?H = "graph_of (see_power n e)" let ?d = "see_degree e" let ?n = "see_size e" interpret fin_digraph "(graph_of e)" using assms by auto interpret P:fin_digraph ?P by (intro graph_power_fin) define φ where "φ = (λ(u,v). Arc u (arc_walk_head ?G (u, v)) (from_digits ?d (map arc_label v)))" define iso where "iso = ⦇ iso_verts = id, iso_arcs = φ, iso_head = arc_head, iso_tail = arc_tail ⦈" have "xs = ys" if "length xs = length ys" "map arc_label xs = map arc_label ys" "is_arc_walk ?G u xs ∧ is_arc_walk ?G u ys ∧ u ∈ verts ?G" for xs ys u using that proof (induction xs ys arbitrary: u rule:list_induct2) case Nil then show ?case by simp next case (Cons x xs y ys) have "arc_label x = arc_label y" "u ∈ verts ?G" "x ∈ out_arcs ?G u" "y ∈ out_arcs ?G u" using Cons by auto hence a:"x = y" unfolding graph_of_def by auto moreover have "head ?G y ∈ verts ?G" using Cons by auto ultimately have "xs = ys" using Cons(3,4) by (intro Cons(2)[of "head ?G y"]) auto thus ?case using a by auto qed hence 5:"inj_on (λ(u,v). (u, map arc_label v)) (arc_walks ?G n)" unfolding arc_walks_def by (intro inj_onI) auto have 3:"set (map arc_label (snd xs)) ⊆ {..<?d}" "length (snd xs) = n" if "xs ∈ arc_walks ?G n" for xs proof - show "length (snd xs) = n" using subsetD[OF is_arc_walk_set[where G="?G"]] that unfolding arc_walks_def by auto have "set (snd xs) ⊆ arcs ?G" using subsetD[OF is_arc_walk_set[where G="?G"]] that unfolding arc_walks_def by auto thus "set (map arc_label (snd xs)) ⊆ {..<?d}" unfolding graph_of_def by auto qed hence 7:"inj_on (λ(u,v). (u, from_digits ?d (map arc_label v))) (arc_walks ?G n)" using inj_onD[OF 5] inj_onD[OF from_digits_inj] by (intro inj_onI) auto hence "inj_on φ (arc_walks ?G n)" unfolding inj_on_def φ_def by auto hence "inj_on (iso_arcs iso) (arcs (graph_power (graph_of e) n))" unfolding iso_def graph_power_def by simp moreover have "inj_on (iso_verts iso) (verts (graph_power (graph_of e) n))" unfolding iso_def by simp moreover have "iso_verts iso (tail ?P a) = iso_tail iso (iso_arcs iso a)" "iso_verts iso (head ?P a) = iso_head iso (iso_arcs iso a)" if "a ∈ arcs ?P" for a unfolding φ_def iso_def graph_power_def by (simp_all add:case_prod_beta) ultimately have 0:"P.digraph_isomorphism iso" unfolding P.digraph_isomorphism_def by (intro conjI ballI P.wf_digraph_axioms) auto have "card((λ(u, v).(u,from_digits ?d (map arc_label v)))`arc_walks ?G n)=card(arc_walks ?G n)" by (intro card_image 7) also have "... = ?d^n * ?n" by (intro card_arc_walks_see fin_digraph_axioms) finally have "card((λ(u, v).(u,from_digits ?d (map arc_label v)))`arc_walks ?G n) = ?d^n * ?n" by simp moreover have "fst v ∈ {..<?n}" if "v ∈ arc_walks ?G n" for v using that unfolding arc_walks_def graph_of_def by auto moreover have "from_digits ?d (map arc_label (snd v)) < ?d ^ n" if "v ∈ arc_walks ?G n" for v using 3[OF that] by (intro from_digits_range) auto ultimately have 2: "{..<?n}×{..<?d^n} = (λ(u,v). (u, from_digits ?d (map arc_label v))) ` arc_walks ?G n" by (intro card_subset_eq[symmetric]) auto have "foldl (λy x. see_step e x y) u (map arc_label w) = arc_walk_head ?G (u,w)" if "is_arc_walk ?G u w" "u ∈ verts ?G" for u w using that proof (induction w rule:rev_induct) case Nil then show ?case by (simp add:arc_walk_head_def) next case (snoc x xs) hence "x ∈ arcs ?G" by (simp add:is_arc_walk_snoc) hence "see_step e (arc_label x) (tail ?G x) = (head ?G x)" unfolding graph_of_def by (auto simp add:image_iff) also have "... = arc_walk_head (graph_of e) (u, xs @ [x])" unfolding arc_walk_head_def by simp finally have "see_step e (arc_label x) (tail ?G x) = arc_walk_head (graph_of e) (u, xs @ [x])" by simp thus ?case using snoc by (simp add:is_arc_walk_snoc) qed hence 4: "foldl (λy x. see_step e x y) (fst x) (map arc_label (snd x)) = arc_walk_head ?G x" if "x ∈ arc_walks (graph_of e) n" for x using that unfolding arc_walks_def by (simp add:case_prod_beta) have "arcs ?H = (λ(v, i). Arc v (see_step (see_power n e) i v) i) ` ({..<?n}×{..<?d^n})" unfolding graph_of_def by simp also have "... = (λ(v,w). Arc v (see_step (see_power n e) (from_digits ?d (map arc_label w)) v) (from_digits ?d (map arc_label w))) ` arc_walks ?G n" unfolding 2 image_image by (simp del:see_power.simps add: case_prod_beta comp_def) also have "... = (λ(v,w). Arc v (foldl (λy x. see_step e x y) v (map arc_label w)) (from_digits ?d (map arc_label w))) ` arc_walks ?G n" using 3 by (intro image_cong refl) (simp add:case_prod_beta to_from_digits) also have "... = φ ` arc_walks ?G n" unfolding φ_def using 4 by (simp add:case_prod_beta) also have "... = iso_arcs iso ` arcs ?P" unfolding iso_def graph_power_def by simp finally have "arcs ?H = iso_arcs iso ` arcs ?P" by simp moreover have "verts ?H = iso_verts iso ` verts ?P" unfolding iso_def graph_of_def graph_power_def by simp moreover have "tail ?H = iso_tail iso" unfolding iso_def graph_of_def by simp moreover have "head ?H = iso_head iso" unfolding iso_def graph_of_def by simp ultimately have 1:"?H = app_iso iso ?P" unfolding app_iso_def by (intro pre_digraph.equality) (simp_all del:see_power.simps) show ?thesis using 0 1 unfolding digraph_iso_def by auto qed lemma see_power: assumes "is_expander e Λ⇩_{a}" shows "is_expander (see_power n e) (Λ⇩_{a}^n)" proof - interpret G: "regular_graph" "graph_of e" using assms unfolding is_expander_def by auto interpret H:"regular_graph" "graph_power (graph_of e) n" by (intro G.graph_power_regular) have 0:"digraph_iso (graph_power (graph_of e) n) (graph_of (see_power n e))" by (intro graph_power_iso_see_power) auto have "regular_graph.Λ⇩_{a}(graph_of (see_power n e)) = H.Λ⇩_{a}" using H.regular_graph_iso_expansion[OF 0] by auto also have "... ≤ G.Λ⇩_{a}^n" by (intro G.graph_power_expansion) also have "... ≤ Λ⇩_{a}^n" using assms(1) unfolding is_expander_def by (intro power_mono G.Λ_ge_0) auto finally have "regular_graph.Λ⇩_{a}(graph_of (see_power n e)) ≤ Λ⇩_{a}^n" by simp moreover have "regular_graph (graph_of (see_power n e))" using H.regular_graph_iso[OF 0] by auto ultimately show ?thesis unfolding is_expander_def by auto qed text ‹The Margulis Construction from Section~\ref{sec:margulis} is a strongly explicit expander graph.› definition mgg_vert :: "nat ⇒ nat ⇒ (int × int)" where "mgg_vert n x = (x mod n, x div n)" definition mgg_vert_inv :: "nat ⇒ (int × int) ⇒ nat" where "mgg_vert_inv n x = nat (fst x) + nat (snd x) * n" lemma mgg_vert_inv: assumes "n > 0" "x ∈ {0..<int n}×{0..<int n}" shows "mgg_vert n (mgg_vert_inv n x) = x" using assms unfolding mgg_vert_def mgg_vert_inv_def by auto definition mgg_arc :: "nat ⇒ (nat × int)" where "mgg_arc k = (k mod 4, if k ≥ 4 then (-1) else 1)" definition mgg_arc_inv :: "(nat × int) ⇒ nat" where "mgg_arc_inv x = (nat (fst x) + 4 * of_bool (snd x < 0))" lemma mgg_arc_inv: assumes "x ∈ {..<4}×{-1,1}" shows "mgg_arc (mgg_arc_inv x) = x" using assms unfolding mgg_arc_def mgg_arc_inv_def by auto definition see_mgg :: "nat ⇒ strongly_explicit_expander" where "see_mgg n = ⦇ see_size = n^2, see_degree = 8, see_step = (λi v. mgg_vert_inv n (mgg_graph_step n (mgg_vert n v) (mgg_arc i))) ⦈" lemma mgg_graph_iso: assumes "n > 0" shows "digraph_iso (mgg_graph n) (graph_of (see_mgg n))" proof - let ?v = "mgg_vert n" let ?vi = "mgg_vert_inv n" let ?a = "mgg_arc" let ?ai = "mgg_arc_inv" let ?G = "graph_of (see_mgg n)" let ?s = "mgg_graph_step n" define φ where "φ a = Arc (?vi (arc_tail a)) (?vi (arc_head a)) (?ai (arc_label a))" for a define iso where "iso = ⦇ iso_verts = mgg_vert_inv n, iso_arcs = φ, iso_head = arc_head, iso_tail = arc_tail ⦈" interpret M: margulis_gaber_galil n using assms by unfold_locales have inj_vi: "inj_on ?vi (verts M.G)" unfolding mgg_graph_def mgg_vert_inv_def by (intro inj_on_inverseI[where g="mgg_vert n"]) (auto simp:mgg_vert_def) have "card (?vi ` verts M.G) = card (verts M.G)" by (intro card_image inj_vi) moreover have "card (verts M.G) = n⇧^{2}" unfolding mgg_graph_def by (auto simp:power2_eq_square) moreover have "mgg_vert_inv n x ∈ {..<n⇧^{2}}" if "x ∈ verts M.G" for x proof - have "mgg_vert_inv n x = nat (fst x) + nat (snd x) * n" unfolding mgg_vert_inv_def by simp also have "... ≤ (n-1) + (n-1) * n" using that unfolding mgg_graph_def by (intro add_mono mult_right_mono) auto also have "... = n * n - 1" using assms by (simp add:algebra_simps) also have "... < n^2" using assms by (simp add: power2_eq_square) finally have "mgg_vert_inv n x < n^2" by simp thus ?thesis by simp qed ultimately have 0:"{..<n^2} = ?vi ` verts M.G" by (intro card_subset_eq[symmetric] image_subsetI) auto have inj_ai: "inj_on ?ai ({..<4} × {-1,1})" unfolding mgg_arc_inv_def by (intro inj_onI) auto have "card (?ai ` ({..<4} × {- 1, 1})) = card ({..<4::nat} × {-1,1::int})" by (intro card_image inj_ai) hence 1:"{..<8} = ?ai ` ({..<4} × {-1,1})" by (intro card_subset_eq[symmetric] image_subsetI) (auto simp add:mgg_arc_inv_def) have "arcs ?G = (λ(v, i). Arc v (?vi (?s (?v v) (?a i))) i) ` ({..<n⇧^{2}} × {..<8})" by (simp add:see_mgg_def graph_of_def) also have "... = (λ(v, i). Arc (?vi v) (?vi (?s (?v (?vi v)) (?a (?ai i)))) (?ai i)) ` (verts M.G × ({..<4} × {-1,1}))" unfolding 0 1 mgg_arc_inv by (auto simp add:image_iff) also have "... = (λ(v, i). Arc (?vi v) (?vi (?s v i)) (?ai i)) ` (verts M.G × ({..<4} × {-1,1}))" using mgg_vert_inv[OF assms] mgg_arc_inv unfolding mgg_graph_def by (intro image_cong) auto also have "... = (φ ∘ (λ(t, l). Arc t (?s t l) l)) ` (verts M.G × ({..<4} × {-1,1}))" unfolding φ_def by (intro image_cong refl) ( simp add:comp_def case_prod_beta ) also have "... = φ ` arcs M.G" unfolding mgg_graph_def by (simp add:image_image) also have "... = iso_arcs iso ` arcs (mgg_graph n)" unfolding iso_def by simp finally have "arcs (graph_of (see_mgg n)) = iso_arcs iso ` arcs (mgg_graph n)" by simp moreover have "verts ?G = iso_verts iso ` verts (mgg_graph n)" unfolding iso_def graph_of_def see_mgg_def using 0 by simp moreover have "tail ?G = iso_tail iso" unfolding iso_def graph_of_def by simp moreover have "head ?G = iso_head iso" unfolding iso_def graph_of_def by simp ultimately have 0:"?G = app_iso iso (mgg_graph n)" unfolding app_iso_def by (intro pre_digraph.equality) simp_all have "inj_on φ (arcs M.G)" proof (rule inj_onI) fix x y assume assms': "x ∈ arcs M.G" "y ∈ arcs M.G" "φ x = φ y" have "?vi (head M.G x) = ?vi (head M.G y)" using assms'(3) unfolding φ_def mgg_graph_def by auto hence "head M.G x = head M.G y" using assms'(1,2) by (intro inj_onD[OF inj_vi]) auto hence "arc_head x = arc_head y" unfolding mgg_graph_def by simp moreover have "?vi (tail M.G x) = ?vi (tail M.G y)" using assms'(3) unfolding φ_def mgg_graph_def by auto hence "tail M.G x = tail M.G y" using assms'(1,2) by (intro inj_onD[OF inj_vi]) auto hence "arc_tail x = arc_tail y" unfolding mgg_graph_def by simp moreover have "?ai (arc_label x) = ?ai (arc_label y)" using assms'(3) unfolding φ_def by auto hence "arc_label x = arc_label y" using assms'(1,2) unfolding mgg_graph_def by (intro inj_onD[OF inj_ai]) (auto simp del:mgg_graph_step.simps) ultimately show "x = y" by (intro arc.expand) auto qed hence "inj_on (iso_arcs iso) (arcs M.G)" unfolding iso_def by simp moreover have "inj_on (iso_verts iso) (verts M.G)" using inj_vi unfolding iso_def by simp moreover have "iso_verts iso (tail M.G a) = iso_tail iso (iso_arcs iso a)" "iso_verts iso (head M.G a) = iso_head iso (iso_arcs iso a)" if "a ∈ arcs M.G" for a unfolding iso_def φ_def mgg_graph_def by auto ultimately have 1:"M.digraph_isomorphism iso" unfolding M.digraph_isomorphism_def by (intro conjI ballI M.wf_digraph_axioms) auto show ?thesis unfolding digraph_iso_def using 0 1 by auto qed lemma see_mgg: assumes "n > 0" shows "is_expander (see_mgg n) (5* sqrt 2 / 8)" proof - interpret G: "margulis_gaber_galil" "n" using assms by unfold_locales auto note 0 = mgg_graph_iso[OF assms] have "regular_graph.Λ⇩_{a}(graph_of (see_mgg n)) = G.Λ⇩_{a}" using G.regular_graph_iso_expansion[OF 0] by auto also have "... ≤ (5* sqrt 2 / 8)" using G.mgg_numerical_radius unfolding G.MGG_bound_def by simp finally have "regular_graph.Λ⇩_{a}(graph_of (see_mgg n)) ≤ (5* sqrt 2 / 8)" by simp moreover have "regular_graph (graph_of (see_mgg n))" using G.regular_graph_iso[OF 0] by auto ultimately show ?thesis unfolding is_expander_def by auto qed text ‹Using all of the above it is possible to construct strongly explicit expanders of every size and spectral gap with asymptotically optimal degree.› definition see_standard_aux where "see_standard_aux n = see_compress n (see_mgg (nat ⌈sqrt n⌉))" lemma see_standard_aux: assumes "n > 0" shows "is_expander (see_standard_aux n) ((8+5 * sqrt 2) / 16)" (is "?A") "see_degree (see_standard_aux n) = 16" (is "?B") "see_size (see_standard_aux n) = n" (is "?C") proof - have 2:"sqrt (real n) > -1" by (rule less_le_trans[where y="0"]) auto have 0:"real n ≤ of_int ⌈sqrt (real n)⌉^2" by (simp add:sqrt_le_D) consider (a) "n = 1" | (b) "n ≥ 2 ∧ n ≤ 4" | (c) "n ≥ 5 ∧ n ≤ 9" | (d) "n ≥ 10" using assms by linarith hence 1:"of_int ⌈sqrt (real n)⌉^2 ≤ 2 * real n" proof (cases) case a then show ?thesis by simp next case b hence "real_of_int ⌈sqrt (real n)⌉^2 ≤ of_int ⌈sqrt (real 4)⌉^2" using 2 by (intro power_mono iffD2[OF of_int_le_iff] ceiling_mono iffD2[OF real_sqrt_le_iff]) auto also have "... = 2 * real 2" by simp also have "... ≤ 2 * real n" using b by (intro mult_left_mono) auto finally show ?thesis by simp next case c hence "real_of_int ⌈sqrt (real n)⌉^2 ≤ of_int ⌈sqrt (real 9)⌉^2" using 2 by (intro power_mono iffD2[OF of_int_le_iff] ceiling_mono iffD2[OF real_sqrt_le_iff]) auto also have "... = 9" by simp also have "... ≤ 2 * real 5" by simp also have "... ≤ 2 * real n" using c by (intro mult_left_mono) auto finally show ?thesis by simp next case d have "real_of_int ⌈sqrt (real n)⌉^2 ≤ (sqrt (real n)+1)^2" using 2 by (intro power_mono) auto also have "... = real n + sqrt (4 * real n + 0) + 1" using real_sqrt_pow2 by (simp add:power2_eq_square algebra_simps real_sqrt_mult) also have "... ≤ real n + sqrt (4 * real n + (real n * (real n - 6) + 1)) + 1" using d by (intro add_mono iffD2[OF real_sqrt_le_iff]) auto also have "... = real n + sqrt ((real n-1)^2) + 1" by (intro_cong "[σ⇩_{2}(+), σ⇩_{1}sqrt]") (auto simp add:power2_eq_square algebra_simps) also have "... = 2 * real n" using d by simp finally show ?thesis by simp qed have "nat ⌈sqrt (real n)⌉^2 ∈ {n..2*n}" by (simp add: approximation_preproc_nat(13) sqrt_le_D 1) hence "see_size (see_mgg (nat ⌈sqrt (real n)⌉)) ∈ {n..2*n}" by (simp add:see_mgg_def) moreover have "sqrt (real n) > 0" using assms by simp hence "0 < nat ⌈sqrt (real n)⌉" by simp ultimately have "is_expander (see_standard_aux n) ((5* sqrt 2 / 8)/2 + 1/2)" unfolding see_standard_aux_def by (intro see_compress see_mgg) auto thus ?A by (auto simp add:field_simps) show ?B unfolding see_standard_aux_def by (simp add:see_mgg_def) show ?C unfolding see_standard_aux_def by simp qed definition see_standard_power where "see_standard_power x = (if x ≤ (0::real) then 0 else nat ⌈ln x / ln 0.95⌉)" lemma see_standard_power: assumes "Λ⇩_{a}> 0" shows "0.95^(see_standard_power Λ⇩_{a}) ≤ Λ⇩_{a}" (is "?L ≤ ?R") proof (cases "Λ⇩_{a}≤ 1") case True hence "0 ≤ ln Λ⇩_{a}/ ln 0.95" using assms by (intro divide_nonpos_neg) auto hence 1:"0 ≤ ⌈ln Λ⇩_{a}/ ln 0.95⌉" by simp have "?L = 0.95^nat ⌈ln Λ⇩_{a}/ ln 0.95⌉" using assms unfolding see_standard_power_def by simp also have "... = 0.95 powr (of_nat (nat (⌈ln Λ⇩_{a}/ ln 0.95⌉)))" by (subst powr_realpow) auto also have "... = 0.95 powr ⌈ln Λ⇩_{a}/ ln 0.95⌉" using 1 by (subst of_nat_nat) auto also have "... ≤ 0.95 powr (ln Λ⇩_{a}/ ln 0.95)" by (intro powr_mono_rev) auto also have "... = ?R" using assms unfolding powr_def by simp finally show ?thesis by simp next case False hence "ln Λ⇩_{a}/ ln 0.95 ≤ 0" by (subst neg_divide_le_eq) auto hence "see_standard_power Λ⇩_{a}= 0" unfolding see_standard_power_def by simp then show ?thesis using False by simp qed lemma see_standard_power_eval[code]: "see_standard_power x = (if x ≤ 0 ∨ x ≥ 1 then 0 else (1+see_standard_power (x/0.95)))" proof (cases "x ≤ 0 ∨ x ≥ 1") case True have "ln x / ln (19 / 20) ≤ 0" if "x > 0" proof - have "x ≥ 1" using that True by auto thus ?thesis by (intro divide_nonneg_neg) auto qed then show ?thesis using True unfolding see_standard_power_def by simp next case False hence x_range: "x > 0" "x < 1" by auto have "ln (x / 0.95) < ln (1/0.95)" using x_range by (intro iffD2[OF ln_less_cancel_iff]) auto also have "... = - ln 0.95" by (subst ln_div) auto finally have "ln (x / 0.95) < - ln 0.95" by simp hence 0: "-1 < ln (x / 0.95) / ln 0.95" by (subst neg_less_divide_eq) auto have "see_standard_power x = nat ⌈ln x / ln 0.95⌉" using x_range unfolding see_standard_power_def by simp also have "... = nat ⌈ln (x/0.95) / ln 0.95 + 1⌉" by (subst ln_div[OF x_range(1)]) (simp_all add:field_simps ) also have "... = nat (⌈ln (x/0.95) / ln 0.95⌉+1)" by (intro arg_cong[where f="nat"]) simp also have "... = 1 + nat ⌈ln (x/0.95) / ln 0.95⌉" using 0 by (subst nat_add_distrib) auto also have "... = (if x ≤ 0 ∨ 1 ≤ x then 0 else 1 + see_standard_power (x/0.95))" unfolding see_standard_power_def using x_range by auto finally show ?thesis by simp qed definition see_standard :: "nat ⇒ real ⇒ strongly_explicit_expander" where "see_standard n Λ⇩_{a}= see_power (see_standard_power Λ⇩_{a}) (see_standard_aux n)" theorem see_standard: assumes "n > 0" "Λ⇩_{a}> 0" shows "is_expander (see_standard n Λ⇩_{a}) Λ⇩_{a}" and "see_size (see_standard n Λ⇩_{a}) = n" and "see_degree (see_standard n Λ⇩_{a}) = 16 ^ (nat ⌈ln Λ⇩_{a}/ ln 0.95⌉)" (is "?C") proof - have 0:"is_expander (see_standard_aux n) 0.95" by (intro see_standard_aux(1)[OF assms(1)] is_expander_mono[where a="(8+5 * sqrt 2) / 16"]) (approximation 10) show "is_expander (see_standard n Λ⇩_{a}) Λ⇩_{a}" unfolding see_standard_def by (intro see_power 0 is_expander_mono[where a="0.95^(see_standard_power Λ⇩_{a})"] see_standard_power assms(2)) show "see_size (see_standard n Λ⇩_{a}) = n" unfolding see_standard_def using see_standard_aux[OF assms(1)] by simp have "see_degree (see_standard n Λ⇩_{a}) = 16 ^ (see_standard_power Λ⇩_{a})" unfolding see_standard_def using see_standard_aux[OF assms(1)] by simp also have "... = 16 ^ (nat ⌈ln Λ⇩_{a}/ ln 0.95⌉)" unfolding see_standard_power_def using assms(2) by simp finally show ?C by simp qed fun see_sample_walk :: "strongly_explicit_expander ⇒ nat ⇒ nat ⇒ nat list" where "see_sample_walk e 0 x = [x]" | "see_sample_walk e (Suc l) x = (let w = see_sample_walk e l (x div (see_degree e)) in w@[see_step e (x mod (see_degree e)) (last w)])" theorem see_sample_walk: fixes e l assumes "fin_digraph (graph_of e)" defines "r ≡ see_size e * see_degree e ^l" shows "{# see_sample_walk e l k. k ∈# mset_set {..<r} #} = walks' (graph_of e) l" unfolding r_def proof (induction l) case 0 then show ?case unfolding graph_of_def by simp next case (Suc l) interpret fin_digraph "graph_of e" using assms(1) by auto let ?d = "see_degree e" let ?n = "see_size e" let ?w = "see_sample_walk e" let ?G = "graph_of e" define r where "r = ?n * ?d^l" have 1: "{i * ?d..<(i + 1) * ?d} ∩ {j * ?d..<(j + 1) * ?d} = {}" if "i ≠ j" for i j using that index_div_eq by blast have 2:"vertices_from ?G x = {# see_step e i x. i ∈# mset_set {..<?d}#}" (is "?L = ?R") if "x ∈ verts ?G" for x proof - have "x < ?n" using that unfolding graph_of_def by simp hence 1:"out_arcs ?G x = (λi. Arc x (see_step e i x) i) ` {..<?d}" unfolding out_arcs_def graph_of_def by (auto simp add:image_iff set_eq_iff) have "?L = {# arc_head a. a ∈# mset_set (out_arcs ?G x) #}" unfolding verts_from_alt by (simp add:graph_of_def) also have "... = {# arc_head a. a ∈# {# Arc x (see_step e i x) i. i ∈# mset_set {..<?d}#}#} " unfolding 1 by (intro arg_cong2[where f= "image_mset"] image_mset_mset_set[symmetric] inj_onI) auto also have "... = ?R" by (simp add:image_mset.compositionality comp_def) finally show ?thesis by simp qed have "card (⋃w<r. {w * ?d..<(w + 1) *?d}) = (∑w < r. card {w * ?d..<(w + 1) *?d})" using 1 by (intro card_UN_disjoint) auto also have "... = r * ?d" by simp finally have "card (⋃w<r. {w * ?d..<(w + 1) *?d}) = card {..<?d * r}" by simp moreover have "?d + z * ?d ≤ ?d * r" if "z < r" for z proof - have "?d + z * ?d = ?d * (z + 1)" by simp also have "... ≤ ?d * r" using that by (intro mult_left_mono) auto finally show ?thesis by simp qed ultimately have 0: "(⋃w<r. {w * ?d..<(w + 1) *?d}) = {..<?d * r}" using order_less_le_trans by (intro card_subset_eq subsetI) auto have "{# ?w (l+1) k. k ∈# mset_set {..<?n * ?d^(l+1)} #} = {#?w (l+1) k. k ∈# mset_set {..<?d * r}#}" unfolding r_def by (simp add:ac_simps) also have "... = {# ?w (l+1) x. x ∈# mset_set (⋃w<r. {w * ?d..<(w + 1) * ?d})#}" unfolding 0 by simp also have "... = image_mset (?w (l+1)) (concat_mset (image_mset (mset_set ∘ (λw. {w * ?d..<(w + 1) * ?d})) (mset_set {..<r})))" by (intro arg_cong2[where f="image_mset"] concat_disjoint_union_mset refl 1) auto also have "... = concat_mset{#{#?w (l+1) i. i∈#mset_set {w*?d..<(w+1)*?d}#}. w∈#mset_set {..<r}#}" by (simp add:image_concat_mset image_mset.compositionality comp_def del:see_sample_walk.simps) also have "...=concat_mset {#{#?w(l+1)i. i∈#mset_set ((+)(w*?d)`{..<?d})#}. w∈#mset_set {..<r}#}" by (intro_cong "[σ⇩_{1}concat_mset, σ⇩_{2}image_mset, σ⇩_{1}mset_set]" more:ext) (simp add: atLeast0LessThan[symmetric]) also have "... = concat_mset {#{#?w (l+1) i. i∈#image_mset ((+) (w*?d)) (mset_set {..<?d})#}. w∈#mset_set {..<r}#}" by (intro_cong "[σ⇩_{1}concat_mset, σ⇩_{2}image_mset]" more:image_mset_cong image_mset_mset_set[symmetric] inj_onI) auto also have "... = concat_mset {#{#?w (l+1) (w*?d+i).i∈#mset_set {..<?d}#}. w∈#mset_set {..<r}#}" by (simp add:image_mset.compositionality comp_def del:see_sample_walk.simps) also have "... = concat_mset {#{#?w l w@[see_step e i (last (?w l w))].i∈#mset_set {..<?d}#}.w∈#mset_set {..<r}#}" by (intro_cong "[σ⇩_{1}concat_mset]" more:image_mset_cong) (simp add:Let_def) also have "... = concat_mset {#{#w@[see_step e i (last w)].i∈#mset_set {..<?d}#}.w∈#walks' ?G l#}" unfolding r_def Suc[symmetric] image_mset.compositionality comp_def by simp also have "... = concat_mset {#{#w@[x].x∈#{# see_step e i (last w). i∈#mset_set {..<?d}#}#}. w ∈# walks' ?G l#}" unfolding image_mset.compositionality comp_def by simp also have "... = concat_mset {#{#w@[x].x∈#vertices_from ?G (last w)#}. w ∈# walks' ?G l#}" using last_in_set set_walks_2(1,2) by (intro_cong "[σ⇩_{1}concat_mset, σ⇩_{2}image_mset]" more:image_mset_cong 2[symmetric]) blast also have "... = walks' (graph_of e) (l+1)" by (simp add:image_mset.compositionality comp_def) finally show ?case by simp qed unbundle no_intro_cong_syntax end