section ‹Cheeger Inequality\label{sec:cheeger_ineq}› text ‹The Cheeger inequality relates edge expansion (a combinatorial property) with the second largest eigenvalue.› theory Expander_Graphs_Cheeger_Inequality imports Expander_Graphs_Eigenvalues begin unbundle intro_cong_syntax hide_const Quantum.T context regular_graph begin lemma edge_expansionD2: assumes "m = card (S ∩ verts G)" "2*m ≤ n" shows "Λ⇩_{e}* m ≤ real (card (edges_betw S (-S)))" proof - define S' where "S' = S ∩ verts G" have "Λ⇩_{e}* m = Λ⇩_{e}* card S'" using assms(1) S'_def by simp also have "... ≤ real (card (edges_betw S' (-S')))" using assms unfolding S'_def by (intro edge_expansionD) auto also have "... = real (card (edges_betw S (-S)))" unfolding S'_def edges_betw_def by (intro arg_cong[where f="real"] arg_cong[where f="card"]) auto finally show ?thesis by simp qed lemma edges_betw_sym: "card (edges_betw S T) = card (edges_betw T S)" (is "?L = ?R") proof - have "?L = (∑a ∈ arcs G. of_bool (tail G a ∈ S ∧ head G a ∈ T))" unfolding edges_betw_def of_bool_def by (simp add:sum.If_cases Int_def) also have "... = (∑e ∈# edges G. of_bool (fst e ∈ S ∧ snd e ∈ T))" unfolding sum_unfold_sum_mset edges_def arc_to_ends_def by (simp add:image_mset.compositionality comp_def) also have "... = (∑e ∈# edges G. of_bool (snd e ∈ S ∧ fst e ∈ T))" by (subst edges_sym[OF sym, symmetric]) (simp add:image_mset.compositionality comp_def case_prod_beta) also have "... = (∑a ∈ arcs G. of_bool (tail G a ∈ T ∧ head G a ∈ S))" unfolding sum_unfold_sum_mset edges_def arc_to_ends_def by (simp add:image_mset.compositionality comp_def conj.commute) also have "... = ?R" unfolding edges_betw_def of_bool_def by (simp add:sum.If_cases Int_def) finally show ?thesis by simp qed lemma edges_betw_reg: assumes "S ⊆ verts G" shows "card (edges_betw S UNIV) = card S * d" (is "?L = ?R") proof - have "?L = card (⋃(out_arcs G ` S))" unfolding edges_betw_def out_arcs_def by (intro arg_cong[where f="card"]) auto also have "... = (∑i∈S. card (out_arcs G i))" using finite_subset[OF assms] unfolding out_arcs_def by (intro card_UN_disjoint) auto also have "... = (∑i∈S. out_degree G i)" unfolding out_degree_def by simp also have "... = (∑i∈S. d)" using assms by (intro sum.cong reg) auto also have "... = ?R" by simp finally show ?thesis by simp qed text ‹The following proof follows Hoory et al.~@{cite ‹\S 4.5.1› "hoory2006"}.› lemma cheeger_aux_2: assumes "n > 1" shows "Λ⇩_{e}≥ d*(1-Λ⇩_{2})/2" proof - have "real (card (edges_betw S (-S))) ≥ (d * (1 - Λ⇩_{2}) / 2) * real (card S)" if "S ⊆ verts G" "2 * card S ≤ n" for S proof - let ?ct = "real (card (verts G - S))" let ?cs = "real (card S)" have "card (edges_betw S S)+card (edges_betw S (-S))=card(edges_betw S S∪edges_betw S (-S))" unfolding edges_betw_def by (intro card_Un_disjoint[symmetric]) auto also have "... = card (edges_betw S UNIV)" unfolding edges_betw_def by (intro arg_cong[where f="card"]) auto also have "... = d * ?cs" using edges_betw_reg[OF that(1)] by simp finally have "card (edges_betw S S) + card (edges_betw S (-S)) = d * ?cs" by simp hence 4: "card (edges_betw S S) = d * ?cs - card (edges_betw S (-S))" by simp have "card(edges_betw S(-S))+card(edges_betw(-S)(-S))=card(edges_betw S(-S)∪edges_betw(-S)(-S))" unfolding edges_betw_def by (intro card_Un_disjoint[symmetric]) auto also have "... = card (edges_betw UNIV (verts G - S))" unfolding edges_betw_def by (intro arg_cong[where f="card"]) auto also have "... = card (edges_betw (verts G - S) UNIV)" by (intro edges_betw_sym) also have "... = d * ?ct" using edges_betw_reg by auto finally have "card (edges_betw S (-S)) + card (edges_betw (-S) (-S)) = d * ?ct" by simp hence 5: "card (edges_betw (-S) (-S)) = d * ?ct - card (edges_betw S (-S))" by simp have 6: "card (edges_betw (-S) S) = card (edges_betw S (-S))" by (intro edges_betw_sym) have "?cs + ?ct =real (card (S ∪ (verts G- S)))" unfolding of_nat_add[symmetric] using finite_subset[OF that(1)] by (intro_cong "[σ⇩_{1}of_nat, σ⇩_{1}card]" more:card_Un_disjoint[symmetric]) auto also have "... = real n" unfolding n_def using that(1) by (intro_cong "[σ⇩_{1}of_nat, σ⇩_{1}card]") auto finally have 7: "?cs + ?ct = n" by simp define f where "f x = real (card (verts G - S)) * of_bool (x ∈ S) - card S * of_bool (x ∉ S)" for x have "g_inner f (λ_. 1) = ?cs * ?ct - real (card (verts G ∩ {x. x ∉ S})) * ?cs" unfolding g_inner_def f_def using Int_absorb1[OF that(1)] by (simp add:sum_subtractf) also have "... = ?cs * ?ct - ?ct * ?cs" by (intro_cong "[σ⇩_{2}(-), σ⇩_{2}(*), σ⇩_{1}of_nat, σ⇩_{1}card]") auto also have "... = 0" by simp finally have 11:" g_inner f (λ_. 1) = 0" by simp have "g_norm f^2 = (∑v∈verts G. f v^2)" unfolding g_norm_sq g_inner_def conjugate_real_def by (simp add:power2_eq_square) also have "...=(∑v∈verts G. ?ct^2*(of_bool (v ∈ S))⇧^{2})+(∑v∈verts G. ?cs^2*(of_bool (v ∉ S))⇧^{2})" unfolding f_def power2_diff by (simp add:sum.distrib sum_subtractf power_mult_distrib) also have "... = real (card (verts G ∩ S))*?ct^2 + real (card (verts G ∩ {v. v ∉ S})) * ?cs^2" unfolding of_bool_def by (simp add:if_distrib if_distribR sum.If_cases) also have "... = real(card S)*(real(card(verts G-S)))⇧^{2}+ real(card(verts G-S))*(real(card S))⇧^{2}" using that(1) by (intro_cong "[σ⇩_{2}(+), σ⇩_{2}(*), σ⇩_{2}power, σ⇩_{1}of_nat, σ⇩_{1}card]") auto also have "... = real(card S)*real (card (verts G -S))*(?cs + ?ct)" by (simp add:power2_eq_square algebra_simps) also have "... = real(card S)*real (card (verts G -S))*n" unfolding 7 by simp finally have 9:" g_norm f^2 = real(card S)*real (card (verts G -S))*real n" by simp have "(∑a ∈ arcs G. f (head G a) * f (tail G a)) = (card (edges_betw S S) * ?ct*?ct) + (card (edges_betw (-S) (-S)) * ?cs*?cs) - (card (edges_betw S (-S)) * ?ct*?cs) - (card (edges_betw (-S) S) * ?cs*?ct)" unfolding f_def by (simp add:of_bool_def algebra_simps Int_def if_distrib if_distribR edges_betw_def sum.If_cases) also have "... = d*?cs*?ct*(?cs+?ct) - card (edges_betw S (-S))*(?ct*?ct+2*?ct*?cs+?cs*?cs)" unfolding 4 5 6 by (simp add:algebra_simps) also have "... = d*?cs*?ct*n - (?ct+?cs)^2 * card (edges_betw S (-S))" unfolding power2_diff 7 power2_sum by (simp add:ac_simps power2_eq_square) also have "... = d *?cs*?ct*n - n^2 * card (edges_betw S (-S))" using 7 by (simp add:algebra_simps) finally have 8:"(∑a ∈ arcs G. f(head G a)*f(tail G a))=d*?cs*?ct*n-n^2*card(edges_betw S (-S))" by simp have "d*?cs*?ct*n-n^2*card(edges_betw S (-S)) = (∑a ∈ arcs G. f (head G a) * f (tail G a))" unfolding 8 by simp also have "... ≤ d * (g_inner f (g_step f))" unfolding g_inner_step_eq using d_gt_0 by simp also have "... ≤ d * (Λ⇩_{2}* g_norm f^2)" by (intro mult_left_mono os_expanderD 11) auto also have "... = d * Λ⇩_{2}* ?cs*?ct*n" unfolding 9 by simp finally have "d*?cs*?ct*n-n^2*card(edges_betw S (-S)) ≤ d * Λ⇩_{2}* ?cs*?ct*n" by simp hence "n * n * card (edges_betw S (-S)) ≥ n * (d * ?cs * ?ct * (1-Λ⇩_{2}))" by (simp add:power2_eq_square algebra_simps) hence 10:"n * card (edges_betw S (-S)) ≥ d * ?cs * ?ct * ( 1-Λ⇩_{2})" using n_gt_0 by simp have "(d * (1 - Λ⇩_{2}) / 2) * ?cs = (d * (1-Λ⇩_{2}) * (1 - 1 / 2)) * ?cs" by simp also have "... ≤ d * (1-Λ⇩_{2}) * ((n - ?cs) / n) * ?cs" using that n_gt_0 Λ⇩_{2}_le_1 by (intro mult_left_mono mult_right_mono mult_nonneg_nonneg) auto also have "... = (d * (1-Λ⇩_{2}) * ?ct / n) * ?cs" using 7 by simp also have "... = d * ?cs * ?ct * (1-Λ⇩_{2}) / n" by simp also have "... ≤ n * card (edges_betw S (-S)) / n" by (intro divide_right_mono 10) auto also have "... = card (edges_betw S (-S))" using n_gt_0 by simp finally show ?thesis by simp qed thus ?thesis by (intro edge_expansionI assms) auto qed end lemma surj_onI: assumes "⋀x. x ∈ B ⟹ g x ∈ A ∧ f (g x) = x" shows "B ⊆ f ` A" using assms by force lemma find_sorted_bij_1: fixes g :: "'a ⇒ ('b :: linorder)" assumes "finite S" shows "∃f. bij_betw f {..<card S} S ∧ mono_on {..<card S} (g∘ f)" proof - define h where "h x = from_nat_into S x" for x have h_bij:"bij_betw h {..<card S} S" unfolding h_def using bij_betw_from_nat_into_finite[OF assms] by simp define xs where "xs = sort_key (g ∘ h) [0..<card S]" define f where "f i = h (xs ! i)" for i have l_xs: "length xs = card S" unfolding xs_def by auto have set_xs: "set xs = {..<card S}" unfolding xs_def by auto have dist_xs: "distinct xs" using l_xs set_xs by (intro card_distinct) simp have sorted_xs: "sorted (map (g ∘ h) xs)" unfolding xs_def using sorted_sort_key by simp have "(λi. xs ! i) ` {..<card S} = set xs" using l_xs by (auto simp:in_set_conv_nth) also have "... = {..<card S}" unfolding set_xs by simp finally have set_xs': "(λi. xs ! i) ` {..<card S} = {..<card S}" by simp have "f ` {..<card S} = h ` ((λi. xs ! i) ` {..<card S})" unfolding f_def image_image by simp also have "... = h ` {..<card S}" unfolding set_xs' by simp also have "... = S" using bij_betw_imp_surj_on[OF h_bij] by simp finally have 0: "f ` {..<card S} = S" by simp have "inj_on ((!) xs) {..<card S}" using dist_xs l_xs unfolding distinct_conv_nth by (intro inj_onI) auto hence "inj_on (h ∘ (λi. xs ! i)) {..<card S}" using set_xs' bij_betw_imp_inj_on[OF h_bij] by (intro comp_inj_on) auto hence 1: "inj_on f {..<card S}" unfolding f_def comp_def by simp have 2: "mono_on {..<card S} (g ∘ f)" using sorted_nth_mono[OF sorted_xs] l_xs unfolding f_def by (intro mono_onI) simp thus ?thesis using 0 1 2 unfolding bij_betw_def by auto qed lemma find_sorted_bij_2: fixes g :: "'a ⇒ ('b :: linorder)" assumes "finite S" shows "∃f. bij_betw f S {..<card S} ∧ (∀x y. x ∈ S ∧ y ∈ S ∧ f x < f y ⟶ g x ≤ g y)" proof - obtain f where f_def: "bij_betw f {..<card S} S" "mono_on {..<card S} (g ∘ f)" using find_sorted_bij_1 [OF assms] by auto define h where "h = the_inv_into {..<card S} f" have bij_h: "bij_betw h S {..<card S}" unfolding h_def by (intro bij_betw_the_inv_into f_def) moreover have "g x ≤ g y" if "h x < h y" "x ∈ S" "y ∈ S" for x y proof - have "h y < card S" "h x < card S" "h x ≤ h y" using bij_betw_apply[OF bij_h] that by auto hence "g (f (h x)) ≤ g (f (h y))" using f_def(2) unfolding mono_on_def by simp moreover have "f ` {..<card S} = S" using bij_betw_imp_surj_on[OF f_def(1)] by simp ultimately show "g x ≤ g y" unfolding h_def using that f_the_inv_into_f[OF bij_betw_imp_inj_on[OF f_def(1)]] by auto qed ultimately show ?thesis by auto qed context regular_graph_tts begin text ‹Normalized Laplacian of the graph› definition L where "L = mat 1 - A" lemma L_pos_semidefinite: fixes v :: "real ^'n" shows "v ∙ (L *v v) ≥ 0" proof - have "0 = v ∙ v - norm v^2" unfolding power2_norm_eq_inner by simp also have "... ≤ v ∙ v - abs (v ∙ (A *v v))" by (intro diff_mono rayleigh_bound) auto also have "... ≤ v ∙ v - v ∙ (A *v v)" by (intro diff_mono) auto also have "... = v ∙ (L *v v)" unfolding L_def by (simp add:algebra_simps) finally show ?thesis by simp qed text ‹The following proof follows Hoory et al.~@{cite ‹\S 4.5.2› "hoory2006"}.› lemma cheeger_aux_1: assumes "n > 1" shows "Λ⇩_{e}≤ d * sqrt (2 * (1-Λ⇩_{2}))" proof - obtain v where v_def: "v ∙ 1 = 0" "v ≠ 0" "A *v v = Λ⇩_{2}*s v" using Λ⇩_{2}_eq_γ⇩_{2}γ⇩_{2}_ev[OF assms] by auto have "False" if "2*card {i. (1 *s v) $h i > 0} > n" "2*card {i. ((-1) *s v) $h i > 0} > n" proof - have "2 * n = n + n" by simp also have "... <2 * card {i. (1 *s v) $h i > 0} + 2 * card {i. ((-1) *s v) $h i > 0}" by (intro add_strict_mono that) also have "... = 2 * (card {i. (1 *s v) $h i > 0} + card {i. ((-1) *s v) $h i > 0})" by simp also have "... = 2 * (card ({i. (1 *s v) $h i > 0} ∪ {i. ((-1) *s v) $h i > 0}))" by (intro arg_cong2[where f="(*)"] card_Un_disjoint[symmetric]) auto also have "... ≤ 2 * (card (UNIV :: 'n set))" by (intro mult_left_mono card_mono) auto finally have "2 * n < 2 * n" unfolding n_def card_n by auto thus ?thesis by simp qed then obtain β :: real where β_def: "β = 1 ∨ β=(-1)" "2* card {i. (β *s v) $h i > 0 } ≤ n" unfolding not_le[symmetric] by blast define g where "g = β *s v" have g_orth: "g ∙ 1 = 0" unfolding g_def using v_def(1) by (simp add: scalar_mult_eq_scaleR) have g_nz: "g ≠ 0" unfolding g_def using β_def(1) v_def(2) by auto have g_ev: "A *v g = Λ⇩_{2}*s g" unfolding g_def scalar_mult_eq_scaleR matrix_vector_mult_scaleR v_def(3) by auto have g_supp: "2 * card { i. g $h i > 0 } ≤ n" unfolding g_def using β_def(2) by auto define f where "f = (χ i. max (g $h i) 0)" have "(L *v f) $h i ≤ (1-Λ⇩_{2}) * g $h i" (is "?L ≤ ?R") if "g $h i > 0" for i proof - have "?L = f $h i - (A *v f) $h i" unfolding L_def by (simp add:algebra_simps) also have "... = g $h i - (∑j ∈ UNIV. A $h i $h j * f $h j)" unfolding matrix_vector_mult_def f_def using that by auto also have "... ≤ g $h i - (∑j ∈ UNIV. A $h i $h j * g $h j)" unfolding f_def A_def by (intro diff_mono sum_mono mult_left_mono) auto also have "... = g $h i - (A *v g) $h i" unfolding matrix_vector_mult_def by simp also have "... = (1-Λ⇩_{2}) * g $h i" unfolding g_ev by (simp add:algebra_simps) finally show ?thesis by simp qed moreover have "f $h i ≠ 0 ⟹ g $h i > 0 "for i unfolding f_def by simp ultimately have 0:"(L *v f) $h i ≤ (1-Λ⇩_{2}) * g $h i ∨ f $h i = 0" for i by auto text ‹Part (i) in Hoory et al. (\S 4.5.2) but the operator L here is normalized.› have "f ∙ (L *v f) = (∑i∈UNIV. (L *v f) $h i * f $h i)" unfolding inner_vec_def by (simp add:ac_simps) also have "... ≤ (∑i∈UNIV. ((1-Λ⇩_{2}) * g $h i) * f $h i)" by (intro sum_mono mult_right_mono' 0) (simp add:f_def) also have "... = (∑i∈UNIV. (1-Λ⇩_{2}) * f $h i * f $h i)" unfolding f_def by (intro sum.cong refl) auto also have "... = (1-Λ⇩_{2}) * (f ∙ f)" unfolding inner_vec_def by (simp add:sum_distrib_left ac_simps) also have "... = (1 - Λ⇩_{2}) * norm f^2" by (simp add: power2_norm_eq_inner) finally have h_part_i: "f ∙ (L *v f) ≤ (1 - Λ⇩_{2}) * norm f^2" by simp define f' where "f' x = f $h (enum_verts_inv x)" for x have f'_alt: "f = (χ i. f' (enum_verts i))" unfolding f'_def Rep_inverse by simp define B⇩_{f}where "B⇩_{f}= (∑a∈arcs G. ¦f' (tail G a)^2-f' (head G a)^2¦)" have "(x + y)^2 ≤ 2 * (x^2 + y^2)" for x y :: real proof - have "(x + y)^2 = (x^2 + y^2) + 2 * x * y" unfolding power2_sum by simp also have "... ≤ (x^2 + y^2) + (x^2 + y^2)" by (intro add_mono sum_squares_bound) auto finally show ?thesis by simp qed hence "(∑a∈arcs G.(f'(tail G a)+ f'(head G a))⇧^{2})≤(∑a∈arcs G. 2*(f'(tail G a)^2+f'(head G a)^2))" by (intro sum_mono) auto also have "... = 2*((∑a∈arcs G. f'(tail G a)^2) + (∑a∈arcs G. f'(head G a)^2))" by (simp add:sum_distrib_left) also have "... = 4 * d * g_norm f'^2" unfolding sum_arcs_tail[where f="λx. f' x^2"] sum_arcs_head[where f="λx. f' x^2"] g_norm_sq g_inner_def by (simp add:power2_eq_square) also have "... = 4 * d * norm f^2" unfolding g_norm_conv f'_alt by simp finally have 1: "(∑i∈arcs G. (f' (tail G i) + f' (head G i))⇧^{2}) ≤ 4*d* norm f^2" by simp have "(∑a∈arcs G. (f' (tail G a) - f' (head G a))⇧^{2}) = (∑a∈arcs G. (f' (tail G a))⇧^{2}) + (∑a∈arcs G. (f' (head G a))⇧^{2}) - 2* (∑a∈arcs G. f' (tail G a) * f' (head G a))" unfolding power2_diff by (simp add:sum_subtractf sum_distrib_left ac_simps) also have "... = 2 * (d * (∑v∈verts G. (f' v)⇧^{2}) - (∑a∈arcs G. f' (tail G a) * f' (head G a)))" unfolding sum_arcs_tail[where f="λx. f' x^2"] sum_arcs_head[where f="λx. f' x^2"] by simp also have "... = 2 * (d * g_inner f' f' - d * g_inner f' (g_step f'))" unfolding g_inner_step_eq using d_gt_0 by (intro_cong "[σ⇩_{2}(*), σ⇩_{2}(-)]") (auto simp:power2_eq_square g_inner_def ac_simps) also have "... = 2 * d * (g_inner f' f' -g_inner f' (g_step f'))" by (simp add:algebra_simps) also have "... = 2 * d * (f ∙ f - f ∙ (A *v f))" unfolding g_inner_conv g_step_conv f'_alt by simp also have "... = 2 * d * (f ∙ (L *v f))" unfolding L_def by (simp add:algebra_simps) finally have 2:"(∑a∈arcs G. (f' (tail G a) - f' (head G a))⇧^{2}) = 2 * d * (f ∙ (L *v f))" by simp have "B⇩_{f}= (∑a∈arcs G. ¦f' (tail G a)+f' (head G a)¦*¦f' (tail G a)-f' (head G a)¦)" unfolding B⇩_{f}_def abs_mult[symmetric] by (simp add:algebra_simps power2_eq_square) also have "...≤ L2_set (λa. f'(tail G a) + f'(head G a)) (arcs G) * L2_set (λa. f' (tail G a) - f'(head G a)) (arcs G)" by (intro L2_set_mult_ineq) also have "... ≤ sqrt (4*d* norm f^2) * sqrt (2 * d * (f ∙ (L *v f)))" unfolding L2_set_def 2 by (intro mult_right_mono iffD2[OF real_sqrt_le_iff] 1 real_sqrt_ge_zero mult_nonneg_nonneg L_pos_semidefinite) auto also have "... = 2 * sqrt 2 * d * norm f * sqrt (f ∙ (L *v f))" by (simp add:real_sqrt_mult) finally have hoory_4_12: "B⇩_{f}≤ 2 * sqrt 2 * d * norm f * sqrt (f ∙ (L *v f))" by simp text ‹The last statement corresponds to Lemma 4.12 in Hoory et al.› obtain ρ :: "'a ⇒ nat" where ρ_bij: "bij_betw ρ (verts G) {..<n}" and ρ_dec: "⋀x y. x ∈ verts G ⟹ y ∈ verts G ⟹ ρ x < ρ y ⟹ f' x ≥ f' y" unfolding n_def using find_sorted_bij_2[where S="verts G" and g="(λx. - f' x)"] by auto define φ where "φ = the_inv_into (verts G) ρ" have φ_bij: "bij_betw φ {..<n} (verts G)" unfolding φ_def by (intro bij_betw_the_inv_into ρ_bij) have "edges G = {# e ∈# edges G . ρ(fst e) ≠ ρ(snd e) ∨ ρ(fst e) = ρ(snd e) #}" by simp also have "... = {# e ∈# edges G . ρ(fst e) ≠ ρ(snd e) #} + {#e∈#edges G. ρ(fst e)=ρ(snd e)#}" by (simp add:filter_mset_ex_predicates) also have "...={# e∈#edges G. ρ(fst e)<ρ(snd e)∨ρ(fst e)>ρ(snd e)#}+{#e∈#edges G. fst e=snd e#}" using bij_betw_imp_inj_on[OF ρ_bij] edge_set by (intro arg_cong2[where f="(+)"] filter_mset_cong refl inj_on_eq_iff[where A="verts G"]) auto also have "... = {#e ∈# edges G. ρ(fst e) < ρ (snd e) #} + {#e ∈# edges G. ρ(fst e) > ρ (snd e) #} + {#e ∈# edges G. fst e = snd e #}" by (intro arg_cong2[where f="(+)"] filter_mset_ex_predicates[symmetric]) auto finally have edges_split: "edges G = {#e ∈# edges G. ρ(fst e) < ρ (snd e) #} + {#e ∈# edges G. ρ(fst e) > ρ (snd e) #} + {#e ∈# edges G. fst e = snd e #}" by simp have ρ_lt_n: "ρ x < n" if "x ∈ verts G" for x using bij_betw_apply[OF ρ_bij] that by auto have φ_ρ_inv: "φ (ρ x) = x" if "x ∈ verts G" for x unfolding φ_def using bij_betw_imp_inj_on[OF ρ_bij] by (intro the_inv_into_f_f that) auto have ρ_φ_inv: "ρ (φ x) = x" if "x < n" for x unfolding φ_def using bij_betw_imp_inj_on[OF ρ_bij] bij_betw_imp_surj_on[OF ρ_bij] that by (intro f_the_inv_into_f) auto define τ where "τ x = (if x < n then f' (φ x) else 0)" for x have τ_nonneg: "τ k ≥ 0" for k unfolding τ_def f'_def f_def by auto have τ_antimono: "τ k ≥ τ l" if " k < l" for k l proof (cases "l ≥ n") case True hence "τ l = 0" unfolding τ_def by simp then show ?thesis using τ_nonneg by simp next case False hence "τ l = f' (φ l)" unfolding τ_def by simp also have "... ≤ f' (φ k)" using ρ_φ_inv False that by (intro ρ_dec bij_betw_apply[OF φ_bij]) auto also have "... = τ k" unfolding τ_def using False that by simp finally show ?thesis by simp qed define m :: nat where "m = Min {i. τ i = 0 ∧ i ≤ n}" have "τ n = 0" unfolding τ_def by simp hence "m ∈ {i. τ i = 0 ∧ i ≤ n}" unfolding m_def by (intro Min_in) auto hence m_rel_1: "τ m = 0" and m_le_n: "m ≤ n" by auto have "τ k > 0" if "k < m" for k proof (rule ccontr) assume "¬(τ k > 0)" hence "τ k = 0" by (intro order_antisym τ_nonneg) simp hence "k ∈ {i. τ i = 0 ∧ i ≤ n}" using that m_le_n by simp hence "m ≤ k" unfolding m_def by (intro Min_le) auto thus "False" using that by simp qed hence m_rel_2: "f' x > 0" if "x ∈ φ ` {..<m}" for x unfolding τ_def using m_le_n that by auto have "2 * m = 2 * card {..<m}" by simp also have "... = 2 * card (φ ` {..<m})" using m_le_n inj_on_subset[OF bij_betw_imp_inj_on[OF φ_bij]] by (intro_cong "[σ⇩_{2}(*)]" more:card_image[symmetric]) auto also have "... ≤ 2 * card {x ∈ verts G. f' x > 0}" using m_rel_2 bij_betw_apply[OF φ_bij] m_le_n by (intro mult_left_mono card_mono subsetI) auto also have "... = 2 * card (enum_verts_inv ` {x ∈ verts G. f $h (enum_verts_inv x) > 0})" unfolding f'_def using Abs_inject by (intro arg_cong2[where f="(*)"] card_image[symmetric] inj_onI) auto also have "... = 2 * card {x. f $h x > 0}" using Rep_inverse Rep_range unfolding f'_def by (intro_cong "[σ⇩_{2}(*), σ⇩_{1}card]" more:subset_antisym image_subsetI surj_onI[where g="enum_verts"]) auto also have "... = 2 * card {x. g $h x > 0}" unfolding f_def by (intro_cong "[σ⇩_{2}(*), σ⇩_{1}card]") auto also have "... ≤ n" by (intro g_supp) finally have m2_le_n: "2*m ≤ n" by simp have "τ k ≤ 0" if "k > m" for k using m_rel_1 τ_antimono that by metis hence "τ k ≤ 0" if "k ≥ m" for k using m_rel_1 that by (cases "k > m") auto hence τ_supp: "τ k = 0" if "k ≥ m" for k using that by (intro order_antisym τ_nonneg) auto have 4: "ρ v ≤ x ⟷ v ∈ φ ` {..x}" if "v ∈ verts G" "x < n" for v x proof - have "ρ v ≤ x ⟷ ρ v ∈ {..x}" by simp also have "... ⟷ φ (ρ v) ∈ φ ` {..x}" using bij_betw_imp_inj_on[OF φ_bij] bij_betw_apply[OF ρ_bij] that by (intro inj_on_image_mem_iff[where B="{..<n}", symmetric]) auto also have "... ⟷ v ∈ φ ` {..x}" unfolding φ_ρ_inv[OF that(1)] by simp finally show ?thesis by simp qed have "B⇩_{f}= (∑a∈arcs G. ¦f' (tail G a)^2 - f' (head G a)^2¦)" unfolding B⇩_{f}_def by simp also have "... = (∑e ∈# edges G. ¦f' (fst e)^2 - f' (snd e)^2¦)" unfolding edges_def arc_to_ends_def sum_unfold_sum_mset by (simp add:image_mset.compositionality comp_def) also have "... = (∑e∈#{#e ∈# edges G. ρ (fst e) < ρ (snd e)#}. ¦(f' (fst e))⇧^{2}- (f' (snd e))⇧^{2}¦) + (∑e∈#{#e ∈# edges G. ρ (snd e) < ρ (fst e)#}. ¦(f' (fst e))⇧^{2}- (f' (snd e))⇧^{2}¦) + (∑e∈#{#e ∈# edges G. fst e = snd e#}. ¦(f' (fst e))⇧^{2}- (f' (snd e))⇧^{2}¦)" by (subst edges_split) simp also have "... = (∑e∈#{#e ∈# edges G. ρ (snd e) < ρ (fst e)#}. ¦(f' (fst e))⇧^{2}- (f' (snd e))⇧^{2}¦) + (∑e∈#{#e ∈# edges G. ρ (snd e) < ρ (fst e)#}. ¦(f' (snd e))⇧^{2}- (f' (fst e))⇧^{2}¦) + (∑e∈#{#e ∈# edges G. fst e = snd e#}. ¦(f' (fst e))⇧^{2}- (f' (snd e))⇧^{2}¦)" by (subst edges_sym[OF sym, symmetric]) (simp add:image_mset.compositionality comp_def image_mset_filter_mset_swap[symmetric] case_prod_beta) also have "... = (∑e∈#{#e ∈# edges G. ρ (snd e) < ρ (fst e)#}. ¦(f' (snd e))⇧^{2}- (f' (fst e))⇧^{2}¦) + (∑e∈#{#e ∈# edges G. ρ (snd e) < ρ (fst e)#}. ¦(f' (snd e))⇧^{2}- (f' (fst e))⇧^{2}¦) + (∑e∈#{#e ∈# edges G. fst e = snd e#}. 0)" by (intro_cong "[σ⇩_{2}(+), σ⇩_{1}sum_mset]" more:image_mset_cong) auto also have "... = 2 * (∑e∈#{#e∈#edges G. ρ(snd e)<ρ(fst e)#}. ¦(f' (snd e))⇧^{2}- (f' (fst e))⇧^{2}¦)" by simp also have "... = 2 *(∑a|a∈arcs G∧ρ(tail G a)>ρ(head G a). ¦f'(head G a)^2 - f'(tail G a)^2¦)" unfolding edges_def arc_to_ends_def sum_unfold_sum_mset by (simp add:image_mset.compositionality comp_def image_mset_filter_mset_swap[symmetric]) also have "... = 2 * (∑a|a∈arcs G∧ρ(tail G a)>ρ(head G a). ¦τ(ρ(head G a))^2 - τ(ρ(tail G a))^2¦)" unfolding τ_def using φ_ρ_inv ρ_lt_n by (intro arg_cong2[where f="(*)"] sum.cong refl) auto also have "... = 2 * (∑a|a∈arcs G∧ρ(tail G a)>ρ(head G a). τ(ρ(head G a))^2 - τ(ρ(tail G a))^2)" using τ_antimono power_mono τ_nonneg by (intro arg_cong2[where f="(*)"] sum.cong refl abs_of_nonneg)(auto) also have "... = 2 * (∑a|a∈arcs G∧ρ(tail G a)>ρ(head G a). (-(τ(ρ(tail G a))^2)) - (-(τ(ρ(head G a))^2)))" by (simp add:algebra_simps) also have "... = 2 *(∑a|a∈arcs G∧ρ(tail G a)>ρ(head G a). (∑i=ρ(head G a)..<ρ(tail G a). (-(τ (Suc i)^2)) - (-(τ i^2))))" by (intro arg_cong2[where f="(*)"] sum.cong refl sum_Suc_diff'[symmetric]) auto also have "...=2*(∑(a, i)∈(SIGMA x:{a ∈ arcs G. ρ (head G a) < ρ (tail G a)}. {ρ (head G x)..<ρ (tail G x)}). τ i^2 - τ (Suc i)^2)" by (subst sum.Sigma) auto also have "...=2*(∑p∈{(a,i).a ∈ arcs G∧ρ(head G a)≤i∧i<ρ(tail G a)}. τ(snd p)^2-τ (snd p+1)^2)" by (intro arg_cong2[where f="(*)"] sum.cong refl) (auto simp add:Sigma_def) also have "...=2*(∑p∈{(i,a).a ∈ arcs G∧ρ(head G a) ≤ i∧i < ρ(tail G a)}. τ(fst p)^2-τ(fst p+1)^2)" by (intro sum.reindex_cong[where l="prod.swap"] arg_cong2[where f="(*)"]) auto also have "...=2* (∑(i, a)∈(SIGMA x:{..<n}. {a ∈ arcs G. ρ (head G a)≤x ∧ x<ρ(tail G a)}). τ i^2-τ (i+1)^2)" using less_trans[OF _ ρ_lt_n] by (intro sum.cong arg_cong2[where f="(*)"]) auto also have "...=2*(∑i<n. (∑a|a∈arcs G ∧ρ(head G a) ≤ i∧i < ρ(tail G a). τ i^2 - τ (i+1)^2))" by (subst sum.Sigma) auto also have "...=2*(∑i<n. card {a∈arcs G. ρ(head G a)≤i∧i<ρ(tail G a)} * (τ i^2 - τ (i+1)^2))" by simp also have "...=2*(∑i<n. card {a∈arcs G. ρ(head G a)≤i∧¬(ρ(tail G a)≤i)} * (τ i^2 - τ (i+1)^2))" by (intro_cong "[σ⇩_{2}(*), σ⇩_{1}card, σ⇩_{1}of_nat]" more:sum.cong Collect_cong) auto also have "...=2*(∑i<n. card {a∈arcs G. head G a∈φ`{..i}∧tail G a∉φ`{..i}} * (τ i^2-τ (i+1)^2))" using 4 by (intro_cong "[σ⇩_{2}(*), σ⇩_{1}card, σ⇩_{1}of_nat, σ⇩_{2}(∧)]" more:sum.cong restr_Collect_cong) auto also have "... = 2 * (∑i<n. real (card (edges_betw (-φ`{..i}) (φ`{..i}))) * (τ i^2-τ (i+1)^2))" unfolding edges_betw_def by (auto simp:conj.commute) also have "... = 2 * (∑i<n. real (card (edges_betw (φ`{..i}) (-φ`{..i}))) * (τ i^2-τ (i+1)^2))" using edges_betw_sym by simp also have "... = 2 * (∑i<m. real (card (edges_betw (φ`{..i}) (-φ`{..i}))) * (τ i^2-τ (i+1)^2))" using τ_supp m_le_n by (intro sum.mono_neutral_right arg_cong2[where f="(*)"]) auto finally have Bf_eq: "B⇩_{f}= 2 * (∑i<m. real (card (edges_betw (φ`{..i}) (-φ`{..i}))) * (τ i^2-τ (i+1)^2))" by simp have 3:"card (φ ` {..i} ∩ verts G) = i + 1" if "i < m" for i proof - have "card (φ ` {..i} ∩ verts G) = card (φ ` {..i})" using m_le_n that by (intro arg_cong[where f="card"] Int_absorb2 image_subsetI bij_betw_apply[OF φ_bij]) auto also have "... = card {..i}" using m_le_n that by (intro card_image inj_on_subset[OF bij_betw_imp_inj_on[OF φ_bij]]) auto also have "... = i+1" by simp finally show ?thesis by simp qed have "2 * Λ⇩_{e}* norm f^2 = 2 * Λ⇩_{e}* (g_norm f'^2)" unfolding g_norm_conv f'_alt by simp also have "... ≤ 2 * Λ⇩_{e}* (∑v∈ verts G. f' v^2)" unfolding g_norm_sq g_inner_def by (simp add:power2_eq_square) also have "... = 2 * Λ⇩_{e}* (∑i<n. f' (φ i)^2)" by (intro arg_cong2[where f="(*)"] refl sum.reindex_bij_betw[symmetric] φ_bij) also have "... = 2 * Λ⇩_{e}* (∑i<n. τ i^2)" unfolding τ_def by (intro arg_cong2[where f="(*)"] refl sum.cong) auto also have "... = 2 * Λ⇩_{e}* (∑i<m. τ i^2)" using τ_supp m_le_n by (intro sum.mono_neutral_cong_right arg_cong2[where f="(*)"] refl) auto also have "... ≤ 2 * Λ⇩_{e}* ((∑i<m. τ i^2) + (real 0 * τ 0^2 - m * τ m^2))" using τ_supp[of "m"] by simp also have "... ≤ 2 * Λ⇩_{e}* ((∑i<m. τ i^2) + (∑i<m. i*τ i^2-(Suc i)*τ (Suc i)^2))" by (subst sum_lessThan_telescope'[symmetric]) simp also have "... ≤ 2 * (∑i<m. (Λ⇩_{e}* (i+1)) * (τ i^2-τ (i+1)^2))" by (simp add:sum_distrib_left algebra_simps sum.distrib[symmetric]) also have "... ≤ 2 * (∑i<m. real (card (edges_betw (φ`{..i}) (-φ`{..i}))) * (τ i^2-τ (i+1)^2))" using τ_nonneg τ_antimono power_mono 3 m2_le_n by (intro mult_left_mono sum_mono mult_right_mono edge_expansionD2) auto also have "... = B⇩_{f}" unfolding Bf_eq by simp finally have hoory_4_13: "2 * Λ⇩_{e}* norm f^2 ≤ B⇩_{f}" by simp text ‹Corresponds to Lemma 4.13 in Hoory et al.› have f_nz: "f ≠ 0" proof (rule ccontr) assume f_nz_assms: "¬ (f ≠ 0)" have "g $h i ≤ 0" for i proof - have "g $h i ≤ max (g $h i) 0" by simp also have "... = 0" using f_nz_assms unfolding f_def vec_eq_iff by auto finally show ?thesis by simp qed moreover have "(∑i ∈ UNIV. 0-g $h i) = 0" using g_orth unfolding sum_subtractf inner_vec_def by auto ultimately have "∀x∈UNIV. -(g $h x) = 0" by (intro iffD1[OF sum_nonneg_eq_0_iff]) auto thus "False" using g_nz unfolding vec_eq_iff by simp qed hence norm_f_gt_0: "norm f> 0" by simp have "Λ⇩_{e}* norm f * norm f ≤ sqrt 2 * real d * norm f * sqrt (f ∙ (L *v f))" using order_trans[OF hoory_4_13 hoory_4_12] by (simp add:power2_eq_square) hence "Λ⇩_{e}≤ real d * sqrt 2 * sqrt (f ∙ (L *v f)) / norm f" using norm_f_gt_0 by (simp add:ac_simps divide_simps) also have "... ≤ real d * sqrt 2 * sqrt ((1 - Λ⇩_{2}) * (norm f)⇧^{2}) / norm f" by (intro mult_left_mono divide_right_mono real_sqrt_le_mono h_part_i) auto also have "... = real d * sqrt 2 * sqrt (1- Λ⇩_{2})" using f_nz by (simp add:real_sqrt_mult) also have "... = d * sqrt (2 * (1-Λ⇩_{2}))" by (simp add:real_sqrt_mult[symmetric]) finally show ?thesis by simp qed end context regular_graph begin lemmas (in regular_graph) cheeger_aux_1 = regular_graph_tts.cheeger_aux_1[OF eg_tts_1, internalize_sort "'n :: finite", OF _ regular_graph_axioms, unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty] theorem cheeger_inequality: assumes "n > 1" shows "Λ⇩_{e}∈ {d * (1 - Λ⇩_{2}) / 2.. d * sqrt (2 * (1 - Λ⇩_{2}))}" using cheeger_aux_1 cheeger_aux_2 assms by auto unbundle no_intro_cong_syntax end end