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 "... = (iS. card (out_arcs G i))"
    using finite_subset[OF assms] unfolding out_arcs_def
    by (intro card_UN_disjoint) auto
  also have "... = (iS. out_degree G i)"
    unfolding out_degree_def by simp
  also have "... = (iS. 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 Sedges_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 = (vverts G. f v^2)"
      unfolding g_norm_sq g_inner_def conjugate_real_def by (simp add:power2_eq_square)
    also have "...=(vverts G. ?ct^2*(of_bool (v  S))2)+(vverts 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) = (iUNIV. (L *v f) $h i * f $h i)"
    unfolding inner_vec_def by (simp add:ac_simps)
  also have "...  (iUNIV. ((1-Λ2) * g $h i) * f $h i)"
    by (intro sum_mono mult_right_mono' 0) (simp add:f_def)
  also have "... = (iUNIV. (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 Bf where "Bf  = (aarcs 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 "(aarcs G.(f'(tail G a)+ f'(head G a))2)(aarcs G. 2*(f'(tail G a)^2+f'(head G a)^2))"
    by (intro sum_mono) auto
  also have "... = 2*((aarcs G. f'(tail G a)^2) +  (aarcs 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: "(iarcs G. (f' (tail G i) + f' (head G i))2)  4*d* norm f^2"
    by simp

  have "(aarcs G. (f' (tail G a) - f' (head G a))2) = (aarcs G. (f' (tail G a))2) +
    (aarcs G. (f' (head G a))2) - 2* (aarcs 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 * (vverts G. (f' v)2) - (aarcs 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:"(aarcs G. (f' (tail G a) - f' (head G a))2) = 2 * d * (f  (L *v f))" by simp

  have "Bf = (aarcs G. ¦f' (tail G a)+f' (head G a)¦*¦f' (tail G a)-f' (head G a)¦)"
    unfolding Bf_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: "Bf  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 "Bf = (aarcs G. ¦f' (tail G a)^2 - f' (head G a)^2¦)"
    unfolding Bf_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|aarcs 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|aarcs 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|aarcs 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|aarcs Gρ(tail G a)>ρ(head G a). (-(τ(ρ(tail G a))^2)) - (-(τ(ρ(head G a))^2)))"
    by (simp add:algebra_simps)
  also have "... = 2 *(a|aarcs 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)ii<ρ(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)  ii < ρ(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|aarcs G ρ(head G a)  ii < ρ(tail G a). τ i^2 - τ (i+1)^2))"
    by (subst sum.Sigma) auto
  also have "...=2*(i<n. card {aarcs G. ρ(head G a)ii<ρ(tail G a)} * (τ i^2 - τ (i+1)^2))"
    by simp
  also have "...=2*(i<n. card {aarcs 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 {aarcs 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:
    "Bf = 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 "... = Bf"
    unfolding Bf_eq by simp
  finally have hoory_4_13: "2 * Λe * norm f^2  Bf"
    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 "xUNIV. -(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