# Theory 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,

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)
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

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))"
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))"

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)"

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)
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)))"
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"
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))"])
show ?thesis
unfolding FT_def
by (subst g_inner_reindex[OF 0]) (simp add:algebra_simps)
qed

fixes a x y :: int
shows "(a + x * (y mod m)) mod m = (a+x*y) mod m"

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)
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
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))"
also have "... = g_inner f (λx. ω⇩F (fst x* (u-c * v) + snd x * v-d * v))"
also have "... = g_inner f (λx. ω⇩F (-d* v)*ω⇩F (fst x*(u-c* v) + snd x * v))"
also have "... = ω⇩F (d* v)*g_inner f (λx. ω⇩F (fst x*(u-c* v) + snd x * v))"
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

fixes x y u v :: "'a :: ab_semigroup_add"
assumes "x = y" "u = v"
shows "x + u = v + y"

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"
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"
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 + θ)"
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]
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]
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)

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]
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]
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)

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 )"
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
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

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)"
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)`