Theory Expander_Graphs.Expander_Graphs_MGG

section ‹Margulis Gabber Galil Construction\label{sec:margulis}›

text ‹This section formalizes the Margulis-Gabber-Galil expander graph, which is defined on the
product space $\mathbb Z_n \times \mathbb Z_n$. The construction is an adaptation of graph
introduced by Margulis~\cite{margulis1973}, for which he gave a non-constructive proof of its
spectral gap. Later Gabber and Galil~\cite{gabber1981} adapted the graph and derived an explicit
spectral gap, i.e., that the second largest eigenvalue is bounded by $\frac{5}{8} \sqrt{2}$. The
proof was later improved by Jimbo and Marouka~\cite{jimbo1987} using Fourier Analysis.
Hoory et al.~\cite[\S 8]{hoory2006} present a slight simplification of that proof (due to Boppala)
which this formalization is based on.›

theory Expander_Graphs_MGG
  imports
    "HOL-Analysis.Complex_Transcendental"
    "HOL-Decision_Procs.Approximation"
    Expander_Graphs_Definition
begin

datatype ('a, 'b) arc = Arc (arc_tail: 'a)  (arc_head: 'a) (arc_label: 'b)

fun mgg_graph_step :: "nat ⇒ (int × int) ⇒ (nat × int) ⇒ (int × int)"
  where "mgg_graph_step n (i,j) (l,σ) =
  [ ((i+σ*(2*j+0)) mod int n, j), (i, (j+σ*(2*i+0)) mod int n)
  , ((i+σ*(2*j+1)) mod int n, j), (i, (j+σ*(2*i+1)) mod int n) ] ! l"

definition mgg_graph :: "nat ⇒ (int × int, (int × int, nat × int) arc) pre_digraph" where
  "mgg_graph n =
    ⦇ verts = {0..<n} × {0..<n},
      arcs = (λ(t,l). (Arc t (mgg_graph_step n t l) l))`(({0..<int n}×{0..<int n})×({..<4}×{-1,1})),
      tail = arc_tail,
      head = arc_head ⦈"

locale margulis_gaber_galil =
  fixes m :: nat
  assumes m_gt_0: "m > 0"
begin

abbreviation G where "G ≡ mgg_graph m"

lemma wf_digraph: "wf_digraph (mgg_graph m)"
proof -
  have
    "tail (mgg_graph m) e ∈ verts (mgg_graph m)" (is "?A")
    "head (mgg_graph m) e ∈ verts (mgg_graph m)" (is "?B")
    if a:"e ∈ arcs (mgg_graph m)" for e
  proof -
    obtain t l σ where tl_def:
      "t ∈ {0..<int m} × {0..<int m}" "l ∈ {..<4}" "σ ∈ {-1,1}"
      "e = Arc t (mgg_graph_step m t (l,σ)) (l,σ)"
      using a mgg_graph_def by auto
    thus ?A
      unfolding mgg_graph_def by auto
    have "mgg_graph_step m (fst t, snd t) (l,σ) ∈ {0..<int m} × {0..<int m}"
      unfolding mgg_graph_step.simps using tl_def(1,2) m_gt_0
      by (intro set_mp[OF _ nth_mem])  auto
    hence "arc_head e ∈ {0..<int m} × {0..<int m}"
      unfolding tl_def(4) by simp
    thus ?B
      unfolding mgg_graph_def by simp
  qed
  thus ?thesis
    by unfold_locales auto
qed

lemma mgg_finite: "fin_digraph (mgg_graph m)"
proof -
  have "finite (verts (mgg_graph m))" "finite (arcs (mgg_graph m))"
    unfolding mgg_graph_def by auto
  thus ?thesis
    using wf_digraph
    unfolding fin_digraph_def fin_digraph_axioms_def by auto
qed

interpretation fin_digraph "mgg_graph m"
  using mgg_finite by simp

definition arcs_pos :: "(int × int, nat × int) arc set"
    where "arcs_pos = (λ(t,l). (Arc t (mgg_graph_step m t (l,1)) (l, 1)))`(verts G×{..<4})"
definition arcs_neg :: "(int × int, nat × int) arc set"
    where "arcs_neg = (λ(h,l). (Arc (mgg_graph_step m h (l,1)) h (l,-1)))`(verts G×{..<4})"

lemma arcs_sym:
  "arcs G = arcs_pos ∪ arcs_neg"
proof -
  have 0: "x ∈ arcs G" if "x ∈ arcs_pos" for x
    using that unfolding arcs_pos_def mgg_graph_def by auto
  have 1: "a ∈ arcs G" if t:"a ∈ arcs_neg" for a
  proof -
    obtain h l where hl_def: "h ∈ verts G" "l ∈ {..<4}" "a = Arc (mgg_graph_step m h (l,1)) h (l,-1)"
      using t unfolding arcs_neg_def by auto

    define t where "t = mgg_graph_step m h (l,1)"

    have h_ran: "h ∈ {0..<int m} × {0..<int m}"
      using hl_def(1) unfolding mgg_graph_def by simp
    have l_ran: "l ∈ set [0,1,2,3]"
      using hl_def(2) by auto

    have "t ∈ {0..<int m} × {0..<int m}"
      using h_ran l_ran
      unfolding t_def by (cases h, auto simp add:mod_simps)
    hence t_ran: "t ∈ verts G"
      unfolding mgg_graph_def by simp

    have "h = mgg_graph_step m t (l,-1)"
      using h_ran l_ran unfolding t_def by (cases h, auto simp add:mod_simps)
    hence "a = Arc t (mgg_graph_step m t (l,-1)) (l,-1)"
      unfolding t_def hl_def(3) by simp
    thus ?thesis
      using t_ran hl_def(2) mgg_graph_def by (simp add:image_iff)
  qed

  have "card (arcs_pos ∪ arcs_neg) = card arcs_pos + card arcs_neg"
    unfolding arcs_pos_def arcs_neg_def by (intro card_Un_disjoint finite_imageI) auto
  also have "... = card (verts G×{..<4::nat}) + card (verts G×{..<4::nat})"
    unfolding arcs_pos_def arcs_neg_def
    by (intro arg_cong2[where f="(+)"] card_image inj_onI) auto
  also have "... = card (verts G×{..<4::nat}×{-1,1::int})"
    by simp
  also have "... = card ((λ(t, l). Arc t (mgg_graph_step m t l) l) ` (verts G ×{..<4}×{-1,1}))"
    by (intro card_image[symmetric] inj_onI) auto
  also have "... = card (arcs G)"
    unfolding mgg_graph_def by simp
  finally have "card (arcs_pos ∪ arcs_neg) = card (arcs G)"
    by simp
  hence "arcs_pos ∪ arcs_neg = arcs G"
    using 0 1 by (intro card_subset_eq, auto)
  thus ?thesis by simp
qed

lemma sym: "symmetric_multi_graph (mgg_graph m)"
proof -
  define f :: "(int × int, nat × int) arc ⇒ (int × int, nat × int) arc"
    where "f a = Arc (arc_head a) (arc_tail a) (apsnd (λx. (-1) * x) (arc_label a))" for a

  have a: "bij_betw f arcs_pos arcs_neg"
    by (intro bij_betwI[where g="f"])
     (auto simp add:f_def image_iff arcs_pos_def arcs_neg_def)

  have b: "bij_betw f arcs_neg arcs_pos"
    by (intro bij_betwI[where g="f"])
     (auto simp add:f_def image_iff  arcs_pos_def arcs_neg_def)

  have c:"bij_betw f (arcs_pos ∪ arcs_neg) (arcs_neg ∪ arcs_pos)"
    by (intro bij_betw_combine[OF a b])  (auto simp add:arcs_pos_def arcs_neg_def)

  hence c:"bij_betw f (arcs G) (arcs G)"
    unfolding arcs_sym by (subst (2) sup_commute, simp)
  show ?thesis
    by (intro symmetric_multi_graphI[where f="f"] fin_digraph_axioms c)
     (simp add:f_def mgg_graph_def)
qed

lemma out_deg:
  assumes "v ∈ verts G"
  shows "out_degree G v = 8"
proof -
  have "out_degree (mgg_graph m) v = card (out_arcs (mgg_graph m) v)"
    unfolding out_degree_def by simp
  also have "... = card {e. (∃w ∈ verts (mgg_graph m). ∃l ∈ {..<4} × {-1,1}.
    e = Arc w (mgg_graph_step m w l) l ∧ arc_tail e = v)}"
    unfolding mgg_graph_def out_arcs_def by (simp add:image_iff)
  also have "... = card {e. (∃l ∈ {..<4} × {-1,1}. e = Arc v (mgg_graph_step m v l) l)}"
    using assms by (intro arg_cong[where f="card"] iffD2[OF set_eq_iff] allI)  auto
  also have "... = card ((λl. Arc v (mgg_graph_step m v l) l) ` ({..<4} × {-1,1}))"
    by (intro arg_cong[where f="card"]) (auto simp add:image_iff)
  also have "... = card ({..<4::nat} × {-1,1::int})"
    by (intro card_image inj_onI) simp
  also have "... = 8" by simp
  finally show ?thesis by simp
qed

lemma verts_ne:
  "verts G ≠ {}"
  using m_gt_0 unfolding mgg_graph_def by simp

sublocale regular_graph "mgg_graph m"
  using out_deg verts_ne
  by (intro regular_graphI[where d="8"] sym) auto

lemma d_eq_8: "d = 8"
proof -
  obtain v where v_def: "v ∈ verts G"
    using verts_ne by auto
  hence 0:"(SOME v. v ∈ verts G) ∈ verts G"
    by (rule someI[where x="v"])
  show ?thesis
    using out_deg[OF 0]
    unfolding d_def by simp
qed

text ‹We start by introducing Fourier Analysis on the torus $\mathbb Z_n \times \mathbb Z_n$. The
following is too specialized for a general AFP entry.›

lemma g_inner_sum_left:
  assumes "finite I"
  shows "g_inner (λx. (∑i ∈ I. f i x)) g = (∑i∈ I. g_inner (f i) g)"
  using assms by (induction I rule:finite_induct) (auto simp add:g_inner_simps)

lemma g_inner_sum_right:
  assumes "finite I"
  shows "g_inner f (λx. (∑i ∈ I. g i x)) = (∑i∈ I. g_inner f (g i))"
  using assms by (induction I rule:finite_induct) (auto simp add:g_inner_simps)

lemma g_inner_reindex:
  assumes "bij_betw h (verts G) (verts G)"
  shows "g_inner f g = g_inner (λx. (f (h x))) (λx. (g (h x)))"
  unfolding g_inner_def
  by (subst sum.reindex_bij_betw[OF assms,symmetric]) simp

definition ω⇩F :: "real ⇒ complex" where "ω⇩F x = cis (2*pi*x/m)"

lemma ω⇩F_simps:
  "ω⇩F (x + y) = ω⇩F x * ω⇩F y"
  "ω⇩F (x - y) = ω⇩F x * ω⇩F (-y)"
  "cnj (ω⇩F x) = ω⇩F (-x)"
  unfolding ω⇩F_def by (auto simp add:algebra_simps diff_divide_distrib
      add_divide_distrib cis_mult cis_divide cis_cnj)

lemma ω⇩F_cong:
  fixes x y :: int
  assumes "x mod m = y mod m"
  shows "ω⇩F (of_int x) = ω⇩F (of_int y)"
proof -
  obtain z :: int where "y = x + m*z" using mod_eqE[OF assms] by auto
  hence "ω⇩F (of_int y) = ω⇩F (of_int x + of_int (m*z))"
    by simp
  also have "... = ω⇩F (of_int x) * ω⇩F (of_int (m*z))"
    by (simp add:ω⇩F_simps)
  also have "... = ω⇩F (of_int x) * cis (2 * pi * of_int (z))"
    unfolding ω⇩F_def  using m_gt_0
    by (intro arg_cong2[where f="(*)"] arg_cong[where f="cis"]) auto
  also have "... = ω⇩F (of_int x) * 1"
    by (intro arg_cong2[where f="(*)"] cis_multiple_2pi) auto
  finally show ?thesis by simp
qed

lemma cis_eq_1_imp:
  assumes "cis (2 * pi * x) = 1"
  shows "x ∈ ℤ"
proof -
  have "cos (2 * pi * x) = Re (cis (2*pi*x))"
    using cis.simps by simp
  also have "... = 1"
    unfolding assms by simp
  finally have "cos (2 * pi * x) = 1" by simp
  then obtain y where "2 * pi * x = of_int y * 2 * pi"
    using cos_one_2pi_int by auto
  hence "y = x" by simp
  thus ?thesis by auto
qed

lemma ω⇩F_eq_1_iff:
  fixes x :: int
  shows "ω⇩F x = 1 ⟷ x mod m = 0"
proof
  assume "ω⇩F (real_of_int x) = 1"
  hence "cis (2 * pi * real_of_int x / real m) = 1"
    unfolding ω⇩F_def by simp
  hence "real_of_int x / real m ∈ ℤ"
    using cis_eq_1_imp by simp
  then obtain z :: int where "of_int x / real m = z"
    using Ints_cases by auto
  hence "x = z * real m"
    using m_gt_0 by (simp add: nonzero_divide_eq_eq)
  hence "x = z * m" using of_int_eq_iff by fastforce
  thus "x mod m = 0" by simp
next
  assume "x mod m = 0"
  hence "ω⇩F x = ω⇩F (of_int 0)"
    by (intro ω⇩F_cong) auto
  also have "... = 1" unfolding ω⇩F_def by simp
  finally show "ω⇩F x= 1" by simp
qed

definition FT :: "(int × int ⇒ complex) ⇒ (int × int ⇒ complex)"
  where "FT f v = g_inner f (λx. ω⇩F (fst x * fst v + snd x * snd v))"

lemma FT_altdef: "FT f (u,v) = g_inner f (λx. ω⇩F (fst x * u + snd x * v))"
  unfolding FT_def by (simp add:case_prod_beta)

lemma FT_add: "FT (λx. f x + g x) v = FT f v + FT g v"
  unfolding FT_def by (simp add:g_inner_simps algebra_simps)

lemma FT_zero: "FT (λx. 0) v = 0"
  unfolding FT_def g_inner_def by simp

lemma FT_sum:
  assumes "finite I"
  shows "FT (λx. (∑i ∈ I. f i x)) v = (∑i ∈ I. FT (f i) v)"
  using assms by (induction rule: finite_induct, auto simp add:FT_zero FT_add)

lemma FT_scale: "FT (λx. c * f x) v = c * FT f v"
  unfolding FT_def by (simp add: g_inner_simps)

lemma FT_cong:
  assumes "⋀x. x ∈ verts G ⟹ f x = g x"
  shows "FT f = FT g"
  unfolding FT_def by (intro ext g_inner_cong assms refl)

lemma parseval:
  "g_inner f g = g_inner (FT f) (FT g)/m^2" (is "?L = ?R")
proof -
  define δ :: "(int × int) ⇒ (int × int) ⇒ complex" where "δ x y = of_bool (x = y)" for x y

  have FT_δ: "FT (δ v) x = ω⇩F (-(fst v *fst x +snd v * snd x))" if "v ∈ verts G" for v x
    using that by (simp add:FT_def g_inner_def δ_def ω⇩F_simps)

  have 1: "(∑x=0..<int m. ω⇩F (z*x)) = m * of_bool(z mod m = 0)" (is "?L1 = ?R1") for z :: int
  proof (cases "z mod m = 0")
    case True
    have "(∑x=0..<int m. ω⇩F (z*x)) = (∑x=0..<int m. ω⇩F (of_int 0))"
      using True by (intro sum.cong ω⇩F_cong refl) auto
    also have "... = m * of_bool(z mod m = 0)"
      unfolding ω⇩F_def True by simp
    finally show ?thesis by simp
  next
    case False
    have "(1-ω⇩F z) * ?L1 = (1-ω⇩F z) * (∑x ∈ int ` {..<m}. ω⇩F(z*x))"
      by (intro arg_cong2[where f="(*)"] sum.cong refl)
       (simp add: image_atLeastZeroLessThan_int)
    also have "... = (∑x<m. ω⇩F(z*real x) - ω⇩F(z*(real (Suc x))))"
      by (subst sum.reindex, auto simp add:algebra_simps sum_distrib_left ω⇩F_simps)
    also have "... = ω⇩F (z * 0) - ω⇩F (z * m)"
      by (subst sum_lessThan_telescope') simp
    also have "... = ω⇩F (of_int 0) - ω⇩F (of_int 0)"
      by (intro arg_cong2[where f="(-)"] ω⇩F_cong) auto
    also have "... = 0"
      by simp
    finally have "(1- ω⇩F z) * ?L1 = 0" by simp
    moreover have "ω⇩F z ≠ 1" using ω⇩F_eq_1_iff False by simp
    hence "(1- ω⇩F z) ≠ 0" by simp
    ultimately have "?L1 = 0" by simp
    then show ?thesis using False by simp
  qed

  have 0:"g_inner (δ v) (δ w) = g_inner (FT (δ v)) (FT (δ w))/m^2" (is "?L1 = ?R1/_")
    if "v ∈ verts G" "w ∈ verts G" for v w
  proof -
    have "?R1=g_inner(λx. ω⇩F(-(fst v *fst x +snd v * snd x)))(λx. ω⇩F(-(fst w *fst x +snd w * snd x)))"
      using that by (intro g_inner_cong, auto simp add:FT_δ)
    also have "...=(∑(x,y)∈{0..<int m}×{0..<int m}. ω⇩F((fst w-fst v)*x)*ω⇩F((snd w - snd v)* y))"
      unfolding g_inner_def by (simp add:ω⇩F_simps algebra_simps case_prod_beta mgg_graph_def)
    also have "...=(∑x=0..<int m. ∑y = 0..<int m. ω⇩F((fst w - fst v)*x)*ω⇩F((snd w - snd v) * y))"
      by (subst sum.cartesian_product[symmetric]) simp
    also have "...=(∑x=0..<int m. ω⇩F((fst w - fst v)*x))*(∑y = 0..<int m. ω⇩F((snd w - snd v) * y))"
      by (subst sum.swap) (simp add:sum_distrib_left sum_distrib_right)
    also have "... = of_nat (m * of_bool(fst v mod m = fst w mod m)) *
      of_nat (m * of_bool(snd v mod m = snd w mod m))"
      using m_gt_0 unfolding 1
      by (intro arg_cong2[where f="(*)"] arg_cong[where f="of_bool"]
          arg_cong[where f="of_nat"] refl) (auto simp add:algebra_simps cong:mod_diff_cong)
    also have "... = m^2 * of_bool(v = w)"
      using that by (auto simp add:prod_eq_iff mgg_graph_def power2_eq_square)
    also have "... = m^2 * ?L1"
      using that unfolding g_inner_def δ_def by simp
    finally have "?R1 = m^2 * ?L1" by simp
    thus ?thesis using m_gt_0 by simp
  qed

  have "?L = g_inner (λx. (∑v ∈ verts G. (f v) * δ v x)) (λx. (∑v ∈ verts G. (g v) * δ v x))"
    unfolding δ_def by (intro g_inner_cong) auto
  also have "... = (∑v∈verts G. (f v) * (∑w∈verts G. cnj (g w) * g_inner (δ v) (δ w)))"
    by (simp add:g_inner_simps g_inner_sum_left g_inner_sum_right)
  also have "... = (∑v∈verts G. (f v) * (∑w∈verts G. cnj (g w) * g_inner(FT (δ v)) (FT (δ w))))/m^2"
    by (simp add:0 sum_divide_distrib sum_distrib_left algebra_simps)
  also have "...=g_inner(λx.(∑v∈verts G. (f v)*FT (δ v) x))(λx.(∑v∈verts G. (g v)*FT (δ v) x))/m⇧2"
    by (simp add:g_inner_simps g_inner_sum_left g_inner_sum_right)
  also have "...=g_inner(FT(λx.(∑v∈verts G.(f v)*δ v x)))(FT(λx.(∑v∈verts G.(g v)*δ v x)))/m⇧2"
    by (intro g_inner_cong arg_cong2[where f="(/)"]) (simp_all add: FT_sum FT_scale)
  also have "... = g_inner (FT f) (FT g)/m^2 "
    unfolding δ_def comp_def
    by (intro g_inner_cong arg_cong2[where f="(/)"] fun_cong[OF FT_cong]) auto
  finally show ?thesis by simp
qed

lemma plancharel:
  "(∑v ∈ verts G. norm (f v)^2) = (∑v ∈ verts G. norm (FT f v)^2)/m^2" (is "?L = ?R")
proof -
  have "complex_of_real ?L = g_inner f f"
    by (simp flip:of_real_power add:complex_norm_square g_inner_def algebra_simps)
  also have "... = g_inner (FT f) (FT f) / m^2"
    by (subst parseval) simp
  also have "... = complex_of_real ?R"
    by (simp flip:of_real_power add:complex_norm_square g_inner_def algebra_simps) simp
  finally have "complex_of_real ?L = complex_of_real ?R" by simp
  thus ?thesis
    using of_real_eq_iff by blast
qed

lemma FT_swap:
  "FT (λx. f (snd x, fst x)) (u,v) = FT f (v,u)"
proof -
  have 0:"bij_betw (λ(x::int × int). (snd x, fst x)) (verts G) (verts G)"
    by (intro bij_betwI[where g="(λ(x::int × int). (snd x, fst x))"])
     (auto simp add:mgg_graph_def)
  show ?thesis
    unfolding FT_def
    by (subst g_inner_reindex[OF 0]) (simp add:algebra_simps)
qed

lemma mod_add_mult_eq:
  fixes a x y :: int
  shows "(a + x * (y mod m)) mod m = (a+x*y) mod m"
  using mod_add_cong mod_mult_right_eq by blast

definition periodic where "periodic f = (∀x y. f (x,y) = f (x mod int m, y mod int m))"

lemma periodicD:
  assumes "periodic f"
  shows "f (x,y) = f (x mod m, y mod m)"
  using assms unfolding periodic_def by simp

lemma periodic_comp:
  assumes "periodic f"
  shows "periodic (λx. g (f x))"
  using assms unfolding periodic_def by simp

lemma periodic_cong:
  fixes x y u v :: int
  assumes "periodic f"
  assumes "x mod m = u mod m" "y mod m = v mod m"
  shows "f (x,y) = f (u, v)"
  using periodicD[OF assms(1)] assms(2,3) by metis

lemma periodic_FT: "periodic (FT f)"
proof -
  have "FT f (x,y) = FT f (x mod m,y mod m)" for x y
    unfolding FT_altdef by (intro g_inner_cong ω⇩F_cong ext)
     (auto simp add:mod_simps cong:mod_add_cong)
  thus ?thesis
    unfolding periodic_def by simp
qed

lemma FT_sheer_aux:
  fixes u v c d :: int
  assumes "periodic f"
  shows  "FT (λx. f (fst x,snd x+c*fst x+d)) (u,v) = ω⇩F (d* v) * FT f (u-c* v,v)"
    (is "?L = ?R")
proof -
  define s where "s = (λ(x,y). (x, (y - c * x-d) mod m))"
  define s0 where "s0 = (λ(x,y). (x, (y-c*x) mod m))"
  define s1 where "s1 = (λ(x::int,y). (x, (y-d) mod m))"

  have 0:"bij_betw s0 (verts G) (verts G)"
    by (intro bij_betwI[where g="λ(x,y). (x,(y+c*x) mod m)"])
     (auto simp add:mgg_graph_def s0_def Pi_def mod_simps)
  have 1:"bij_betw s1 (verts G) (verts G)"
    by (intro bij_betwI[where g="λ(x,y). (x,(y+d) mod m)"])
     (auto simp add:mgg_graph_def s1_def Pi_def mod_simps)
  have 2: "s = (s1 ∘ s0)"
    by (simp add:s1_def s0_def s_def comp_def mod_simps case_prod_beta ext)
  have 3:"bij_betw s (verts G) (verts G)"
    unfolding 2 using bij_betw_trans[OF 0 1] by simp

  have 4:"(snd (s x) + c * fst x + d) mod int m = snd x mod m" for x
    unfolding s_def by (simp add:case_prod_beta cong:mod_add_cong) (simp add:algebra_simps)
  have 5: "fst (s x) = fst x" for x
    unfolding s_def by (cases x, simp)

  have "?L = g_inner (λx. f (fst x, snd x + c*fst x+d)) (λx. ω⇩F (fst x*u + snd x* v))"
    unfolding FT_altdef by simp
  also have "... = g_inner (λx. f (fst x, (snd x + c*fst x+d) mod m)) (λx. ω⇩F (fst x*u + snd x* v))"
    by (intro g_inner_cong  periodic_cong[OF assms]) (auto simp add:algebra_simps)
  also have "... = g_inner (λx. f (fst x, snd x mod m)) (λx. ω⇩F (fst x*u+ snd (s x)* v))"
    by (subst g_inner_reindex[OF 3]) (simp add:4 5)
  also have "... =
    g_inner (λx. f (fst x, snd x mod m)) (λx. ω⇩F (fst x*u+ ((snd x-c*fst x-d) mod m)* v))"
    by (simp add:s_def case_prod_beta)
  also have "... = g_inner f (λx. ω⇩F (fst x* (u-c * v) + snd x * v-d * v))"
    by (intro g_inner_cong ω⇩F_cong) (auto simp add:mgg_graph_def algebra_simps mod_add_mult_eq)
  also have "... = g_inner f (λx. ω⇩F (-d* v)*ω⇩F (fst x*(u-c* v) + snd x * v))"
    by (simp add: ω⇩F_simps   algebra_simps)
  also have "... = ω⇩F (d* v)*g_inner f (λx. ω⇩F (fst x*(u-c* v) + snd x * v))"
    by (simp add:g_inner_simps ω⇩F_simps)
  also have "... = ?R"
    unfolding FT_altdef by simp
  finally show ?thesis by simp
qed

lemma FT_sheer:
  fixes u v c d :: int
  assumes "periodic f"
  shows
    "FT (λx. f (fst x,snd x+c*fst x+d)) (u,v) = ω⇩F (d* v) * FT f (u-c* v,v)" (is "?A")
    "FT (λx. f (fst x,snd x+c*fst x)) (u,v) = FT f (u-c* v,v)" (is "?B")
    "FT (λx. f (fst x+c* snd x+d,snd x)) (u,v) = ω⇩F (d* u) * FT f (u,v-c*u)" (is "?C")
    "FT (λx. f (fst x+c* snd x,snd x)) (u,v) = FT f (u,v-c*u)" (is "?D")
proof -
  have 1: "periodic (λx. f (snd x, fst x))"
    using assms unfolding periodic_def by simp

  have 0:"ω⇩F 0 = 1"
    unfolding ω⇩F_def by simp
  show ?A
    using FT_sheer_aux[OF assms] by simp
  show ?B
    using 0 FT_sheer_aux[OF assms, where d="0"] by simp
  show ?C
    using FT_sheer_aux[OF 1] by (subst (1 2) FT_swap[symmetric], simp)
  show ?D
    using 0 FT_sheer_aux[OF 1, where d="0"] by (subst (1 2) FT_swap[symmetric], simp)
qed

definition T⇩1 :: "int × int ⇒ int × int" where "T⇩1 x = ((fst x + 2 * snd x) mod m, snd x)"
definition S⇩1 :: "int × int ⇒ int × int" where "S⇩1 x = ((fst x - 2 * snd x) mod m, snd x)"
definition T⇩2 :: "int × int ⇒ int × int" where "T⇩2 x = (fst x, (snd x + 2 * fst x) mod m)"
definition S⇩2 :: "int × int ⇒ int × int" where "S⇩2 x = (fst x, (snd x - 2 * fst x) mod m)"

definition γ_aux :: "int × int ⇒ real × real"
    where "γ_aux x = (¦fst x/m-1/2¦,¦snd x/m-1/2¦)"

definition compare :: "real × real ⇒ real × real ⇒ bool"
  where "compare x y = (fst x ≤ fst y ∧ snd x ≤ snd y ∧ x ≠ y)"

text ‹The value here is different from the value in the source material. This is because the proof
in Hoory~\cite[\S 8]{hoory2006} only establishes the bound $\frac{73}{80}$ while this formalization
establishes the improved bound of $\frac{5}{8} \sqrt 2$.›

definition α :: real where "α = sqrt 2"

lemma α_inv: "1/α = α/2"
  unfolding α_def by (simp add: real_div_sqrt)

definition γ :: "int × int ⇒ int × int ⇒ real"
  where "γ x y = (if compare (γ_aux x) (γ_aux y) then α else (if compare  (γ_aux y) (γ_aux x) then (1 / α) else 1))"

lemma γ_sym: "γ x y * γ y x = 1"
  unfolding γ_def α_def compare_def by (auto simp add:prod_eq_iff)

lemma γ_nonneg: "γ x y ≥ 0"
  unfolding γ_def α_def by auto

definition τ :: "int ⇒ real" where "τ x = ¦cos(pi*x/m)¦"

definition γ' :: "real ⇒ real ⇒ real"
  where "γ' x y = (if abs (x - 1/2) < abs (y - 1/2) then α else (if abs (x-1/2) > abs (y-1/2) then (1 / α) else 1))"

definition φ :: "real ⇒ real ⇒ real"
  where "φ x y = γ' y (frac(y-2*x))+γ' y (frac (y+2*x))"

lemma γ'_cases:
  "abs (x-1/2) = abs (y-1/2) ⟹ γ' x y = 1"
  "abs (x-1/2) > abs (y-1/2) ⟹ γ' x y = 1/α"
  "abs (x-1/2) < abs (y-1/2) ⟹ γ' x y = α"
  unfolding γ'_def by auto

lemma if_cong_direct:
  assumes "a = b"
  assumes "c = d'"
  assumes "e = f"
  shows "(if a then c else e) = (if b then d' else f)"
  using assms by (intro if_cong) auto

lemma γ'_cong:
  assumes "abs (x-1/2) = abs (u-1/2)"
  assumes "abs (y-1/2) = abs (v-1/2)"
  shows "γ' x y = γ' u v"
  unfolding γ'_def
  using assms by (intro if_cong_direct refl) auto

lemma add_swap_cong:
  fixes x y u v :: "'a :: ab_semigroup_add"
  assumes "x = y" "u = v"
  shows "x + u = v + y"
  using assms by (simp add:algebra_simps)

lemma frac_cong:
  fixes x y :: real
  assumes "x - y ∈ ℤ"
  shows "frac x = frac y"
proof -
  obtain k where x_eq: "x = y + of_int k"
    using Ints_cases[OF assms] by (metis add_minus_cancel uminus_add_conv_diff)
  thus ?thesis
    unfolding x_eq  unfolding frac_def by simp
qed

lemma frac_expand:
  fixes x :: real
  shows "frac x = (if x < (-1) then (x-⌊x⌋) else (if x < 0 then (x+1) else (if x < 1 then x else (if x < 2 then (x-1) else  (x-⌊x⌋)))))"
proof -
  have "real_of_int y = -1 ⟷ y= -1" for y
    by auto
  thus ?thesis
    unfolding frac_def  by (auto simp add:not_less floor_eq_iff)
qed

lemma one_minus_frac:
  fixes x :: real
  shows "1 - frac x = (if x ∈ ℤ then 1 else frac (-x))"
  unfolding frac_neg by simp

lemma abs_rev_cong:
  fixes x y :: real
  assumes "x = - y"
  shows "abs x = abs y"
  using assms by simp

lemma cos_pi_ge_0:
  assumes "x ∈{-1/2.. 1/2}"
  shows "cos (pi * x) ≥ 0"
proof -
  have "pi * x ∈ ((*) pi ` {-1/2..1/2})"
    by (intro imageI assms)
  also have "... =  {-pi/2..pi/2}"
    by (subst image_mult_atLeastAtMost[OF pi_gt_zero])  simp
  finally have "pi * x ∈ {-pi/2..pi/2}" by simp
  thus ?thesis
    by (intro cos_ge_zero) auto
qed

text ‹The following is the first step in establishing Eq. 15 in Hoory et al.~\cite[\S 8]{hoory2006}.
Afterwards using various symmetries (diagonal, x-axis, y-axis) the result will follow for the entire
square $[0,1] \times [0,1]$.›

lemma fun_bound_real_3:
  assumes "0 ≤ x"  "x ≤ y" "y ≤ 1/2" "(x,y) ≠ (0,0)"
  shows "¦cos(pi*x)¦*φ x y + ¦cos(pi*y)¦*φ y x ≤ 2.5 * sqrt 2" (is "?L ≤ ?R")
proof -
  have apx:"4 ≤ 5 * sqrt (2::real)" "8 * cos (pi / 4) ≤ 5 * sqrt (2::real)"
    by (approximation 5)+

  have "cos (pi * x) ≥ 0"
    using assms(1,2,3)  by (intro cos_pi_ge_0) simp
  moreover have "cos (pi * y) ≥ 0"
    using assms(1,2,3)  by (intro cos_pi_ge_0) simp
  ultimately have 0:"?L = cos(pi*x)*φ x y + cos(pi*y)*φ y x"  (is "_ = ?T")
    by simp

  consider (a) "x+y < 1/2" | (b) "y = 1/2- x" | (c) "x+y > 1/2" by argo
  hence "?T ≤ 2.5 * sqrt 2" (is "?T ≤ ?R")
  proof (cases)
    case a
    consider
      (1) "x < y" "x > 0" |
      (2) "x=0" "y < 1/2" |
      (3) "y=x" "x > 0"
      using assms(1,2,3,4) a by fastforce
    thus ?thesis
    proof (cases)
      case 1
      have "φ x y = α + 1/α"
        unfolding φ_def using 1 a
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover have "φ y x = 1/α + 1/α"
        unfolding φ_def using 1 a
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (α + 1/α) + cos (pi * y) * (1/α + 1/α)"
        by simp
      also have "... ≤ 1 * (α + 1/α) + 1 * (1/α + 1/α)"
        unfolding α_def by (intro add_mono mult_right_mono) auto
      also have "... = ?R"
        unfolding α_def by (simp add:divide_simps)
      finally show ?thesis by simp
    next
      case 2
      have y_range: "y ∈ {0<..<1/2}"
        using assms 2 by simp
      have "φ 0 y = 1 + 1"
        unfolding φ_def using y_range
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover
      have "¦x¦ * 2 < 1 ⟷ x < 1/2 ∧ -x < 1/2" for x :: real by auto
      hence "φ y 0 = 1 / α + 1/ α"
        unfolding φ_def using y_range
        by (intro arg_cong2[where f="(+)"] γ'_cases) (simp_all add:frac_expand)
      ultimately have "?T = 2 + cos (pi * y) * (2 / α)"
        unfolding 2 by simp
      also have "... ≤ 2 + 1 * (2 / α)"
        unfolding α_def by (intro add_mono mult_right_mono) auto
      also have "... ≤ ?R"
        unfolding α_def by (approximation 10)
      finally show ?thesis by simp
    next
      case 3
      have "φ x y = 1 + 1/α"
        unfolding φ_def using 3 a
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover have "φ y x = 1 + 1/α"
        unfolding φ_def using 3 a
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (2*(1+1/ α))"
        unfolding 3 by simp
      also have "... ≤ 1 * (2*(1+1/ α))"
        unfolding α_def by (intro mult_right_mono) auto
      also have "... ≤ ?R"
        unfolding α_def by (approximation 10)
      finally show ?thesis by simp
    qed
  next
    case b
    have x_range: "x ∈ {0..1/4}"
      using assms b by simp
    then consider (1) "x = 0" | (2) "x = 1/4" | (3) "x ∈ {0<..<1/4}" by fastforce
    thus ?thesis
    proof (cases)
      case 1
      hence y_eq: "y = 1/2" using b by simp
      show ?thesis using apx unfolding 1 y_eq φ_def by (simp add:γ'_def α_def frac_def)
    next
      case 2
      hence y_eq: "y = 1/4" using b by simp
      show ?thesis using apx unfolding y_eq 2 φ_def by (simp add:γ'_def frac_def)
    next
      case 3
      have "φ x y = α + 1"
        unfolding φ_def b using 3
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover have "φ y x = 1/α + 1"
        unfolding φ_def b using 3
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (α + 1) + cos (pi * (1 / 2 - x)) * (1/α + 1)"
        unfolding b by simp
      also have "... ≤ ?R"
        unfolding α_def using x_range
        by (approximation 10 splitting: x=10)
      finally show ?thesis by simp
    qed
  next
    case c
    consider
      (1) "x < y" "y < 1/2" |
      (2) "y=1/2" "x < 1/2" |
      (3) "y=x" "x < 1/2" |
      (4) "x=1/2" "y =1/2"
      using assms(2,3) c  by fastforce
    thus ?thesis
    proof (cases)
      case 1
      define θ :: real where "θ = arcsin (6 / 10)"
      have "cos θ = sqrt (1-0.6^2)"
        unfolding θ_def by (intro cos_arcsin) auto
      also have "... = sqrt ( 0.8^2)"
        by (intro arg_cong[where f="sqrt"]) (simp add:power2_eq_square)
      also have "... = 0.8" by simp
      finally have cos_θ: "cos θ = 0.8" by simp
      have sin_θ: "sin θ = 0.6"
        unfolding θ_def by simp

      have "φ x y = α + α"
        unfolding φ_def using c 1
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover have "φ y x = 1/α + α"
        unfolding φ_def using c 1
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (2 * α) + cos (pi * y) * (α + 1 / α)"
        by simp
      also have "... ≤ cos (pi * (1/2-y)) * (2*α) + cos (pi * y) * (α+1 / α)"
        unfolding α_def using assms(1,2,3) c
        by (intro add_mono mult_right_mono order.refl iffD2[OF cos_mono_le_eq]) auto
      also have "... = (2.5*α)* (sin (pi * y) * 0.8 + cos (pi * y) * 0.6)"
        unfolding sin_cos_eq α_inv by (simp add:algebra_simps)
      also have "... = (2.5*α)* sin(pi*y + θ)"
        unfolding sin_add cos_θ sin_θ
        by (intro arg_cong2[where f="(*)"] arg_cong2[where f="(+)"] refl)
      also have "... ≤ (?R) * 1"
        unfolding α_def by (intro mult_left_mono) auto
      finally show ?thesis by simp
    next
      case 2
      have x_range: "x > 0" "x < 1/2"
        using c 2 by auto
      have "φ x y = α + α"
        unfolding φ_def 2 using x_range
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover have "φ y x = 1 + 1"
        unfolding φ_def 2 using x_range
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (2*α)"
        unfolding 2 by simp
      also have "... ≤ 1 * (2* sqrt 2)"
        unfolding α_def by (intro mult_right_mono) auto
      also have "... ≤ ?R"
        by (approximation 5)
      finally show ?thesis by simp
    next
      case 3
      have x_range: "x ∈ {1/4..1/2}" using 3 c by simp
      hence cos_bound: "cos (pi * x) ≤ 0.71"
        by (approximation 10)
      have "φ x y = 1+α"
        unfolding φ_def 3 using 3 c
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      moreover have "φ y x = 1+α"
        unfolding φ_def 3 using 3 c
        by (intro arg_cong2[where f="(+)"] γ'_cases) (auto simp add:frac_expand)
      ultimately have "?T = 2 * cos (pi * x) * (1+α)"
        unfolding 3 by simp
      also have "... ≤ 2 * 0.71 * (1+sqrt 2)"
        unfolding α_def by (intro mult_right_mono mult_left_mono cos_bound) auto
      also have "... ≤ ?R"
        by (approximation 6)
      finally show ?thesis by simp
    next
      case 4
      show ?thesis  unfolding 4 by simp
    qed
  qed
  thus ?thesis using 0 by simp
qed

text ‹Extend to square $[0, \frac{1}{2}] \times [0,\frac{1}{2}]$ using symmetry around x=y axis.›

lemma fun_bound_real_2:
  assumes "x ∈ {0..1/2}" "y ∈ {0..1/2}" "(x,y) ≠ (0,0)"
  shows "¦cos(pi*x)¦*φ x y + ¦cos(pi*y)¦*φ y x ≤ 2.5 * sqrt 2"  (is "?L ≤ ?R")
proof (cases "y < x")
  case True
  have "?L = ¦cos(pi*y)¦*φ y x + ¦cos(pi*x)¦*φ x y"
    by simp
  also have "... ≤ ?R"
    using True assms
    by (intro fun_bound_real_3)  auto
  finally show ?thesis by simp
next
  case False
  then show ?thesis using assms
    by (intro fun_bound_real_3) auto
qed

text ‹Extend to $x > \frac{1}{2}$ using symmetry around $x=\frac{1}{2}$ axis.›

lemma fun_bound_real_1:
  assumes "x ∈ {0..<1}" "y ∈ {0..1/2}" "(x,y) ≠ (0,0)"
  shows "¦cos(pi*x)¦*φ x y + ¦cos(pi*y)¦*φ y x ≤ 2.5 * sqrt 2" (is "?L ≤ ?R")
proof (cases "x > 1/2")
  case True
  define x' where "x' = 1-x"

  have "¦frac (x - 2 * y) - 1 / 2¦ = ¦frac (1 - x + 2 * y) - 1 / 2¦"
  proof (cases "x - 2 * y ∈ ℤ")
    case True
    then obtain k where x_eq: "x = 2*y + of_int k" using Ints_cases[OF True]
      by (metis add_minus_cancel uminus_add_conv_diff)
    show ?thesis unfolding x_eq frac_def by simp
  next
    case False
    hence "1 - x + 2 * y ∉ ℤ"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed

  moreover have "¦frac (x + 2 * y) - 1 / 2¦ = ¦frac (1 - x - 2 * y) - 1 / 2¦"
  proof (cases "x + 2 * y ∈ ℤ")
    case True
    then obtain k where x_eq: "x = of_int k - 2*y" using Ints_cases[OF True]
      by (metis add.right_neutral add_diff_eq cancel_comm_monoid_add_class.diff_cancel)
    show ?thesis unfolding x_eq frac_def by simp
  next
    case False
    hence "1 - x - 2 * y ∉ ℤ"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed
  ultimately have "φ y x = φ y x'"
    unfolding φ_def  x'_def by (intro γ'_cong add_swap_cong) simp_all

  moreover have "φ x y = φ x' y"
    unfolding φ_def x'_def
    by (intro γ'_cong add_swap_cong refl arg_cong[where f="(λx. abs (x-1/2))"] frac_cong)
     (simp_all add:algebra_simps)

  moreover have "¦cos(pi*x)¦ = ¦cos(pi*x')¦"
    unfolding x'_def by (intro abs_rev_cong) (simp add:algebra_simps)

  ultimately have "?L = ¦cos(pi*x')¦*φ x' y + ¦cos(pi*y)¦*φ y x'"
    by simp
  also have "... ≤ ?R"
    using assms True by (intro fun_bound_real_2) (auto simp add:x'_def)
  finally show ?thesis by simp
next
  case False
  thus ?thesis using assms fun_bound_real_2 by simp
qed

text ‹Extend to $y > \frac{1}{2}$ using symmetry around $y=\frac{1}{2}$ axis.›

lemma fun_bound_real:
  assumes "x ∈ {0..<1}" "y ∈ {0..<1}" "(x,y) ≠ (0,0)"
  shows "¦cos(pi*x)¦*φ x y + ¦cos(pi*y)¦*φ y x ≤ 2.5 * sqrt 2"  (is "?L ≤ ?R")
proof (cases "y > 1/2")
  case True
  define y' where "y' = 1-y"

  have "¦frac (y - 2 * x) - 1 / 2¦ = ¦frac (1 - y + 2 * x) - 1 / 2¦"
  proof (cases "y - 2 * x ∈ ℤ")
    case True
    then obtain k where y_eq: "y = 2*x + of_int k" using Ints_cases[OF True]
      by (metis add_minus_cancel uminus_add_conv_diff)
    show ?thesis unfolding y_eq frac_def by simp
  next
    case False
    hence "1 - y + 2 * x ∉ ℤ"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed

  moreover have "¦frac (y + 2 * x) - 1 / 2¦ = ¦frac (1 - y - 2 * x) - 1 / 2¦"
  proof (cases "y + 2 * x ∈ ℤ")
    case True
    then obtain k where y_eq: "y = of_int k - 2*x" using Ints_cases[OF True]
      by (metis add.right_neutral add_diff_eq cancel_comm_monoid_add_class.diff_cancel)
    show ?thesis unfolding y_eq frac_def by simp
  next
    case False
    hence "1 - y - 2 * x ∉ ℤ"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed
  ultimately have "φ x y = φ x y'"
    unfolding φ_def  y'_def  by (intro γ'_cong add_swap_cong) simp_all

  moreover have "φ y x = φ y' x"
    unfolding φ_def y'_def
    by (intro γ'_cong add_swap_cong refl arg_cong[where f="(λx. abs (x-1/2))"] frac_cong)
     (simp_all add:algebra_simps)

  moreover have "¦cos(pi*y)¦ = ¦cos(pi*y')¦"
    unfolding y'_def by (intro abs_rev_cong) (simp add:algebra_simps)

  ultimately have "?L = ¦cos(pi*x)¦*φ x y' + ¦cos(pi*y')¦*φ y' x"
    by simp
  also have "... ≤ ?R"
    using assms True by (intro fun_bound_real_1) (auto simp add:y'_def)
  finally show ?thesis by simp
next
  case False
  thus ?thesis using assms fun_bound_real_1 by simp
qed

lemma mod_to_frac:
  fixes x :: int
  shows "real_of_int (x mod m) = m * frac (x/m)" (is "?L = ?R")
proof -
  obtain y where y_def: "x mod m = x + int m* y"
    by (metis mod_eqE mod_mod_trivial)

  have 0: "x mod int m < m" "x mod int m ≥ 0"
    using m_gt_0 by auto

  have "?L = real m * (of_int (x mod m) / m )"
    using m_gt_0 by (simp add:algebra_simps)
  also have "... = real m * frac (of_int (x mod m) / m)"
    using 0 by (subst iffD2[OF frac_eq]) auto
  also have "... = real m * frac (x / m + y)"
    unfolding y_def using m_gt_0 by (simp add:divide_simps mult.commute)
  also have "... = ?R"
    unfolding frac_def by simp
  finally show ?thesis by simp
qed

lemma fun_bound:
  assumes "v ∈ verts G" "v ≠ (0,0)"
  shows "τ(fst v)*(γ v (S⇩2 v)+γ v (T⇩2 v))+τ(snd v)*(γ v (S⇩1 v)+γ v (T⇩1 v)) ≤ 2.5 * sqrt 2"
    (is "?L ≤ ?R")
proof -
  obtain x y where v_def: "v = (x,y)" by (cases v) auto
  define x' where "x' = x/real m"
  define y' where "y' = y/real m"

  have 0:"γ v (S⇩1 v) = γ' x' (frac(x'-2*y'))"
    unfolding γ_def γ'_def compare_def v_def γ_aux_def T⇩1_def S⇩1_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 1:"γ v (T⇩1 v) = γ' x' (frac(x'+2*y'))"
    unfolding γ_def γ'_def compare_def v_def γ_aux_def T⇩1_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 2:"γ v (S⇩2 v) = γ' y' (frac(y'-2*x'))"
    unfolding γ_def γ'_def compare_def v_def γ_aux_def S⇩2_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 3:"γ v (T⇩2 v) = γ' y' (frac(y'+2*x'))"
    unfolding γ_def γ'_def compare_def v_def γ_aux_def T⇩2_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 4: "τ (fst v)  = ¦cos(pi*x')¦" "τ (snd v)  = ¦cos(pi*y')¦"
    unfolding τ_def v_def x'_def y'_def by auto

  have "x ∈ {0..<int m}" "y ∈ {0..<int m}" "(x,y) ≠ (0,0)"
    using assms  unfolding v_def mgg_graph_def by auto
  hence 5:"x' ∈ {0..<1}" "y' ∈ {0..<1}" "(x',y') ≠ (0,0)"
    unfolding x'_def y'_def by auto

  have "?L = ¦cos(pi*x')¦*φ x' y' + ¦cos(pi*y')¦*φ y' x'"
    unfolding 0 1 2 3 4 φ_def by simp
  also have "... ≤ ?R"
    by (intro fun_bound_real 5)
  finally show ?thesis by simp
qed

text ‹Equation 15 in Proof of Theorem 8.8›

lemma hoory_8_8:
  fixes f :: "int × int ⇒ real"
  assumes "⋀x. f x ≥ 0"
  assumes "f (0,0) = 0"
  assumes "periodic f"
  shows "g_inner f (λx. f(S⇩2 x)*τ (fst x)+f(S⇩1 x)*τ (snd x))≤1.25* sqrt 2*g_norm f^2"
    (is "?L ≤ ?R")
proof -
  have 0: "2 * f x * f y ≤ γ x y * f x^2 + γ y x * f y^2" (is "?L1 ≤ ?R1") for x y
  proof -
    have "0 ≤ ((sqrt (γ x y) * f x) - (sqrt (γ y x) * f y))^2"
      by simp
    also have "... = ?R1 - 2 * (sqrt (γ x y) * f x) * (sqrt (γ y x) * f y)"
      unfolding power2_diff using γ_nonneg assms(1)
      by (intro arg_cong2[where f="(-)"] arg_cong2[where f="(+)"]) (auto simp add: power2_eq_square)
    also have "... = ?R1 -2 * sqrt (γ x y * γ y x) * f x * f y"
      unfolding real_sqrt_mult by simp
    also have "... = ?R1 - ?L1"
      unfolding γ_sym by simp
    finally have "0 ≤ ?R1 - ?L1" by simp
    thus ?thesis by simp
  qed

  have [simp]: "fst (S⇩2 x) = fst x"  "snd (S⇩1 x) = snd x" for x
    unfolding S⇩1_def S⇩2_def by auto

  have S_2_inv [simp]: "T⇩2 (S⇩2 x) = x" if "x ∈ verts G" for x
    using that unfolding T⇩2_def S⇩2_def mgg_graph_def
    by (cases x,simp add:mod_simps)
  have S_1_inv [simp]: "T⇩1 (S⇩1 x) = x" if "x ∈ verts G" for x
    using that unfolding T⇩1_def S⇩1_def mgg_graph_def
    by (cases x,simp add:mod_simps)

  have S2_inj: "inj_on S⇩2 (verts G)"
    using S_2_inv by (intro inj_on_inverseI[where g="T⇩2"])
  have S1_inj: "inj_on S⇩1 (verts G)"
    using S_1_inv by (intro inj_on_inverseI[where g="T⇩1"])

  have "S⇩2 ` verts G ⊆ verts G"
    unfolding mgg_graph_def S⇩2_def
    by (intro image_subsetI)  auto
  hence S2_ran: "S⇩2 ` verts G = verts G"
    by (intro card_subset_eq card_image S2_inj) auto

  have "S⇩1 ` verts G ⊆ verts G"
    unfolding mgg_graph_def S⇩1_def
    by (intro image_subsetI)  auto
  hence S1_ran: "S⇩1 ` verts G = verts G"
    by (intro card_subset_eq card_image S1_inj) auto

  have 2: "g v * f v^2 ≤ 2.5 * sqrt 2 * f v^2" if "g v ≤ 2.5 * sqrt 2 ∨ v = (0,0)" for v g
  proof (cases "v=(0,0)")
    case True
    then show ?thesis using assms(2) by simp
  next
    case False
    then show ?thesis using that by (intro mult_right_mono) auto
  qed

  have "2*?L=(∑v∈verts G. τ(fst v)*(2*f v *f(S⇩2 v)))+(∑v∈verts G. τ(snd v) * (2 * f v * f (S⇩1 v)))"
    unfolding g_inner_def by (simp add: algebra_simps sum_distrib_left sum.distrib)
  also have "... ≤
    (∑v∈verts G. τ(fst v)*(γ v (S⇩2 v) * f v^2 + γ (S⇩2 v) v * f(S⇩2 v)^2))+
    (∑v∈verts G. τ(snd v)*(γ v (S⇩1 v) * f v^2 + γ (S⇩1 v) v * f(S⇩1 v)^2))"
    unfolding τ_def by (intro add_mono sum_mono mult_left_mono 0) auto
  also have "... =
    (∑v∈verts G. τ(fst v)*γ v (S⇩2 v)*f v^2)+(∑v∈verts G. τ(fst v) * γ (S⇩2 v) v * f(S⇩2 v)^2)+
    (∑v∈verts G. τ(snd v)*γ v (S⇩1 v)*f v^2)+(∑v∈verts G. τ(snd v) * γ (S⇩1 v) v * f(S⇩1 v)^2)"
    by (simp add:sum.distrib algebra_simps)
  also have "... =
    (∑v∈verts G. τ(fst v)*γ v (S⇩2 v)*f v^2)+
    (∑v∈verts G. τ(fst (S⇩2 v)) * γ (S⇩2 v) (T⇩2 (S⇩2 v)) * f(S⇩2 v)^2)+
    (∑v∈verts G. τ(snd v)*γ v (S⇩1 v)*f v^2)+
    (∑v∈verts G. τ(snd (S⇩1 v)) * γ (S⇩1 v) (T⇩1 (S⇩1 v)) * f(S⇩1 v)^2)"
    by (intro arg_cong2[where f="(+)"] sum.cong refl) simp_all
  also have "... =
    (∑v∈verts G. τ(fst v)*γ v (S⇩2 v)*f v^2)+ (∑v∈S⇩2 ` verts G. τ(fst v) * γ v (T⇩2 v) * f v^2)+
    (∑v∈verts G. τ(snd v)*γ v (S⇩1 v)*f v^2)+ (∑v∈S⇩1 ` verts G. τ(snd v) * γ v (T⇩1 v) * f v^2)"
    using S1_inj S2_inj by (simp add:sum.reindex)
  also have "... =
    (∑v∈verts G. (τ(fst v)*(γ v (S⇩2 v)+γ v (T⇩2 v))+τ(snd v)*(γ v (S⇩1 v)+γ v (T⇩1 v))) *f v^2)"
    unfolding S1_ran S2_ran by (simp add:algebra_simps sum.distrib)
  also have "... ≤ (∑v∈verts G. 2.5 * sqrt 2 * f v^2)"
    using fun_bound by (intro sum_mono 2) auto
  also have "... ≤  2.5 * sqrt 2 * g_norm f^2"
    unfolding g_norm_sq g_inner_def
    by (simp add:algebra_simps power2_eq_square sum_distrib_left)
  finally have "2 * ?L ≤ 2.5 * sqrt 2 * g_norm f^2" by simp
  thus ?thesis by simp
qed

lemma hoory_8_7:
  fixes f :: "int×int ⇒ complex"
  assumes "f (0,0) = 0"
  assumes "periodic f"
  shows "norm(g_inner f (λx. f (S⇩2 x) * (1+ω⇩F (fst x)) + f (S⇩1 x) * (1+ω⇩F (snd x))))
    ≤ (2.5 * sqrt 2) * (∑v ∈ verts G. norm (f v)^2)" (is "?L ≤ ?R")
proof -
  define g :: "int×int ⇒ real" where "g x = norm (f x)" for x

  have g_zero: "g (0,0) = 0"
    using assms(1) unfolding g_def by simp
  have g_nonneg: "g x ≥ 0" for x
    unfolding g_def by simp
  have g_periodic: "periodic g"
    unfolding g_def by (intro periodic_comp[OF assms(2)])

  have 0: "norm(1+ω⇩F x) = 2*τ x" for x :: int
  proof -
    have "norm(1+ω⇩F x) = norm(ω⇩F (-x/2)*(ω⇩F 0 + ω⇩F x))"
      unfolding ω⇩F_def norm_mult by simp
    also have "... = norm (ω⇩F (0-x/2) + ω⇩F (x-x/2))"
      unfolding ω⇩F_simps by (simp add: algebra_simps)
    also have "... = norm (ω⇩F (x/2) + cnj (ω⇩F (x/2)))"
      unfolding ω⇩F_simps(3) by (simp add:algebra_simps)
    also have "... = ¦2*Re (ω⇩F (x/2))¦"
      unfolding complex_add_cnj norm_of_real by simp
    also have "... =  2*¦cos(pi*x/m)¦"
      unfolding ω⇩F_def cis.simps by simp
    also have "... = 2*τ x" unfolding τ_def by simp
    finally show ?thesis by simp
  qed

  have "?L≤norm(∑v∈verts G. f v * cnj(f(S⇩2 v)*(1+ω⇩F (fst v))+f(S⇩1 v )*(1+ω⇩F (snd v))))"
    unfolding g_inner_def by (simp add:case_prod_beta)
  also have "...≤(∑v∈verts G. norm(f v * cnj(f (S⇩2 v) *(1+ω⇩F (fst v))+f (S⇩1 v)*(1+ω⇩F (snd v)))))"
    by (intro norm_sum)
  also have "...=(∑v∈verts G. g v * norm(f (S⇩2 v) *(1+ω⇩F (fst v))+f (S⇩1 v)*(1+ω⇩F (snd v))))"
    unfolding norm_mult g_def complex_mod_cnj by simp
  also have "...≤(∑v∈verts G. g v * (norm (f(S⇩2 v)*(1+ω⇩F (fst v)))+norm(f(S⇩1 v)*(1+ω⇩F(snd v)))))"
    by (intro sum_mono norm_triangle_ineq mult_left_mono g_nonneg)
  also have "...=2*g_inner g (λx. g (S⇩2 x)*τ (fst x)+g(S⇩1 x)*τ (snd x))"
    unfolding g_def g_inner_def norm_mult 0
    by (simp add:sum_distrib_left algebra_simps case_prod_beta)
  also have "... ≤2*(1.25* sqrt 2*g_norm g^2)"
    by (intro mult_left_mono hoory_8_8 g_nonneg g_zero g_periodic) auto
  also have "... = ?R"
    unfolding g_norm_sq g_def g_inner_def by (simp add:power2_eq_square)
  finally show ?thesis by simp
qed

lemma hoory_8_3:
  assumes "g_inner f (λ_. 1) = 0"
  assumes "periodic f"
  shows "¦(∑(x,y)∈verts G. f(x,y)*(f(x+2*y,y)+f(x+2*y+1,y)+f(x,y+2*x)+f(x,y+2*x+1)))¦
    ≤ (2.5 * sqrt 2) * g_norm f^2" (is "¦?L¦ ≤ ?R")
proof -
  let ?f = "(λx. complex_of_real (f x))"

  define Ts :: "(int × int ⇒ int × int) list" where
    "Ts = [(λ(x,y).(x+2*y,y)),(λ(x,y).(x+2*y+1,y)),(λ(x,y).(x,y+2*x)),(λ(x,y).(x,y+2*x+1))]"
  have p: "periodic ?f"
    by (intro periodic_comp[OF assms(2)])

  have 0: "(∑T←Ts. FT (?f∘T) v) = FT ?f (S⇩2 v)*(1+ω⇩F (fst v))+FT ?f (S⇩1 v)*(1+ω⇩F (snd v))"
    (is "?L1 = ?R1") for v :: "int × int"
  proof -
    obtain x y where v_def: "v = (x,y)" by (cases v, auto)
    have "?L1 = (∑T←Ts. FT (?f∘T) (x,y))"
      unfolding v_def by simp
    also have "... = FT ?f (x,y-2*x)*(1+ω⇩F x) + FT ?f (x-2*y,y)*(1+ω⇩F y)"
      unfolding Ts_def by (simp add:FT_sheer[OF p] case_prod_beta comp_def) (simp add:algebra_simps)
    also have "... = ?R1"
      unfolding v_def S⇩2_def S⇩1_def
      by (intro arg_cong2[where f="(+)"] arg_cong2[where f="(*)"] periodic_cong[OF periodic_FT]) auto
    finally show ?thesis by simp
  qed

  have "cmod ((of_nat m)^2) = cmod (of_real (of_nat m^2))" by simp
  also have "... = abs (of_nat m^2)" by (intro norm_of_real)
  also have "... = real m^2" by simp
  finally have 1: "cmod ((of_nat m)⇧2) = (real m)⇧2" by simp

  have "FT (λx. complex_of_real (f x)) (0, 0) = complex_of_real (g_inner f (λ_ . 1))"
    unfolding FT_def g_inner_def g_inner_def ω⇩F_def by simp
  also have "... = 0"
    unfolding assms by simp
  finally have 2: "FT (λx. complex_of_real (f x)) (0, 0) = 0"
    by simp

  have "abs ?L = norm (complex_of_real ?L)"
    unfolding norm_of_real by simp
  also have "... = norm (∑T ← Ts. (g_inner ?f (?f ∘ T)))"
    unfolding Ts_def by (simp add:algebra_simps g_inner_def  sum.distrib comp_def case_prod_beta)
  also have "... = norm (∑T ← Ts. (g_inner (FT ?f) (FT (?f ∘ T)))/m^2)"
    by (subst parseval) simp
  also have "... = norm (g_inner (FT ?f) (λx. (∑T ← Ts. (FT (?f ∘ T) x)))/m^2)"
    unfolding Ts_def by (simp add:g_inner_simps case_prod_beta add_divide_distrib)
  also have "...=norm(g_inner(FT ?f)(λx.(FT ?f(S⇩2 x)*(1+ω⇩F (fst x))+FT f(S⇩1 x)*(1+ω⇩F (snd x)))))/m^2"
    by (subst 0) (simp add:norm_divide 1)
  also have "... ≤ (2.5 * sqrt 2) * (∑v ∈ verts G. norm (FT f v)^2) / m^2"
    by (intro divide_right_mono hoory_8_7[where f="FT f"] 2 periodic_FT) auto
  also have "... = (2.5 * sqrt 2) * (∑v ∈ verts G. cmod (f v)^2)"
    by (subst (2) plancharel) simp
  also have "... = (2.5 * sqrt 2) * (g_inner f f)"
    unfolding g_inner_def norm_of_real by (simp add: power2_eq_square)
  also have "... = ?R"
    using g_norm_sq by auto
  finally show ?thesis by simp
qed

text ‹Inequality stated before Theorem 8.3 in Hoory.›

lemma mgg_numerical_radius_aux:
  assumes "g_inner f (λ_. 1) = 0"
  shows "¦(∑a ∈ arcs G. f (head G a) * f (tail G a))¦ ≤ (5 * sqrt 2) * g_norm f^2"  (is "?L ≤ ?R")
proof -
  define g where "g x = f (fst x mod m, snd x mod m)" for x :: "int × int"
  have 0:"g x = f x" if "x ∈ verts G" for x
    unfolding g_def using that
    by (auto simp add:mgg_graph_def mem_Times_iff)

  have g_mod_simps[simp]: "g (x, y mod m) = g (x, y)" "g (x mod m, y) = g (x, y)" for x y :: int
    unfolding g_def by auto

  have periodic_g: "periodic g"
    unfolding periodic_def by simp

  have "g_inner g (λ_. 1) = g_inner f (λ_. 1)"
    by (intro g_inner_cong 0) auto
  also have "... = 0"
    using assms by simp
  finally have 1:"g_inner g (λ_. 1) = 0" by simp

  have 2:"g_norm g = g_norm f"
    by (intro g_norm_cong 0) (auto)

  have "?L = ¦(∑a ∈ arcs G. g (head G a) * g (tail G a))¦"
    using wellformed
    by (intro arg_cong[where f="abs"] sum.cong arg_cong2[where f="(*)"] 0[symmetric]) auto
  also have "...=¦(∑a∈arcs_pos. g(head G a)*g(tail G a))+(∑a∈arcs_neg. g(head G a)*g(tail G a))¦"
    unfolding arcs_sym arcs_pos_def arcs_neg_def
    by (intro arg_cong[where f="abs"] sum.union_disjoint) auto
  also have "... = ¦2 * (∑(v,l)∈verts G × {..<4}. g v * g (mgg_graph_step m v (l, 1)))¦"
    unfolding arcs_pos_def arcs_neg_def
    by (simp add:inj_on_def sum.reindex case_prod_beta mgg_graph_def algebra_simps)
  also have "... = 2 * ¦(∑v ∈ verts G. (∑l ∈ {..<4}. g v * g (mgg_graph_step m v (l, 1))))¦"
    by (subst sum.cartesian_product)  (simp add:abs_mult)
  also have "... = 2*¦(∑(x,y)∈verts G. (∑l←[0..<4]. g(x,y)* g (mgg_graph_step m (x,y) (l,1))))¦"
    by (subst interv_sum_list_conv_sum_set_nat)
      (auto simp add:atLeast0LessThan case_prod_beta simp del:mgg_graph_step.simps)
  also have "... =2*¦∑(x,y)∈verts G. g (x,y)* (g(x+2*y,y)+g(x+2*y+1,y)+g(x,y+2*x)+g(x,y+2*x+1))¦"
    by (simp add:case_prod_beta numeral_eq_Suc algebra_simps)
  also have "... ≤ 2* ((2.5 * sqrt 2) * g_norm g^2)"
    by (intro mult_left_mono hoory_8_3 1 periodic_g) auto
  also have "... ≤ ?R" unfolding 2 by simp
  finally show ?thesis by simp
qed

definition MGG_bound :: real
  where "MGG_bound = 5 * sqrt 2 / 8"

text ‹Main result: Theorem 8.2 in Hoory.›

lemma mgg_numerical_radius: "Λ⇩a ≤ MGG_bound"
proof -
  have "Λ⇩a ≤ (5 * sqrt 2)/real d"
    by (intro expander_intro mgg_numerical_radius_aux) auto
  also have "... = MGG_bound"
    unfolding MGG_bound_def d_eq_8 by simp
  finally show ?thesis by simp
qed

end

end