Theory Expander_Graphs_Cheeger_Inequality
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