section ‹Spectral Theory\label{sec:expander_eigenvalues}› text ‹This section establishes the correspondence of the variationally defined expansion paramters with the definitions using the spectrum of the stochastic matrix. Additionally stronger results for the expansion parameters are derived.› theory Expander_Graphs_Eigenvalues imports Expander_Graphs_Algebra Expander_Graphs_TTS Perron_Frobenius.HMA_Connect Commuting_Hermitian.Commuting_Hermitian begin unbundle intro_cong_syntax hide_const Matrix_Legacy.transpose hide_const Matrix_Legacy.row hide_const Matrix_Legacy.mat hide_const Matrix.mat hide_const Matrix.row hide_fact Matrix_Legacy.row_def hide_fact Matrix_Legacy.mat_def hide_fact Matrix.vec_eq_iff hide_fact Matrix.mat_def hide_fact Matrix.row_def no_notation Matrix.scalar_prod (infix "∙" 70) no_notation Ordered_Semiring.max ("Maxı") lemma mult_right_mono': "y ≥ (0::real) ⟹ x ≤ z ∨ y = 0 ⟹ x * y ≤ z * y" by (metis mult_cancel_right mult_right_mono) lemma poly_prod_zero: fixes x :: "'a :: idom" assumes "poly (∏a∈#xs. [:- a, 1:]) x = 0" shows "x ∈# xs" using assms by (induction xs, auto) lemma poly_prod_inj_aux_1: fixes xs ys :: "('a :: idom) multiset" assumes "x ∈# xs" assumes "(∏a∈#xs. [:- a, 1:]) = (∏a∈#ys. [:- a, 1:])" shows "x ∈# ys" proof - have "poly (∏a∈#ys. [:- a, 1:]) x = poly (∏a∈#xs. [:- a, 1:]) x" using assms(2) by simp also have "... = poly (∏a∈#xs - {#x#} + {#x#}. [:- a, 1:]) x" using assms(1) by simp also have "... = 0" by simp finally have "poly (∏a∈#ys. [:- a, 1:]) x = 0" by simp thus "x ∈# ys" using poly_prod_zero by blast qed lemma poly_prod_inj_aux_2: fixes xs ys :: "('a :: idom) multiset" assumes "x ∈# xs ∪# ys" assumes "(∏a∈#xs. [:- a, 1:]) = (∏a∈#ys. [:- a, 1:])" shows "x ∈# xs ∩# ys" proof (cases "x ∈# xs") case True then show ?thesis using poly_prod_inj_aux_1[OF True assms(2)] by simp next case False hence a:"x ∈# ys" using assms(1) by simp then show ?thesis using poly_prod_inj_aux_1[OF a assms(2)[symmetric]] by simp qed lemma poly_prod_inj: fixes xs ys :: "('a :: idom) multiset" assumes "(∏a∈#xs. [:- a, 1:]) = (∏a∈#ys. [:- a, 1:])" shows "xs = ys" using assms proof (induction "size xs + size ys" arbitrary: xs ys rule:nat_less_induct) case 1 show ?case proof (cases "xs ∪# ys = {#}") case True then show ?thesis by simp next case False then obtain x where "x ∈# xs ∪# ys" by auto hence a:"x ∈# xs ∩# ys" by (intro poly_prod_inj_aux_2[OF _ 1(2)]) have b: "[:- x, 1:] ≠ 0" by simp have c: "size (xs-{#x#}) + size (ys-{#x#}) < size xs + size ys" using a by (simp add: add_less_le_mono size_Diff1_le size_Diff1_less) have "[:- x, 1:] * (∏a∈#xs - {#x#}. [:- a, 1:]) = (∏a∈#xs. [:- a, 1:])" using a by (subst prod_mset.insert[symmetric]) simp also have "... = (∏a∈#ys. [:- a, 1:])" using 1 by simp also have "... = [:- x, 1:] * (∏a∈#ys - {#x#}. [:- a, 1:])" using a by (subst prod_mset.insert[symmetric]) simp finally have "[:- x, 1:]*(∏a∈#xs-{#x#}. [:- a, 1:])=[:-x, 1:]*(∏a∈#ys-{#x#}. [:- a, 1:])" by simp hence "(∏a∈#xs-{#x#}. [:- a, 1:]) = (∏a∈#ys-{#x#}. [:- a, 1:])" using mult_left_cancel[OF b] by simp hence d:"xs - {#x#} = ys - {#x#}" using 1 c by simp have "xs = xs - {#x#} + {#x#}" using a by simp also have "... = ys - {#x#} + {#x#}" unfolding d by simp also have "... = ys" using a by simp finally show ?thesis by simp qed qed definition eigenvalues :: "('a::comm_ring_1)^'n^'n ⇒ 'a multiset" where "eigenvalues A = (SOME as. charpoly A = (∏a∈#as. [:- a, 1:]) ∧ size as = CARD ('n))" lemma char_poly_factorized_hma: fixes A :: "complex^'n^'n" shows "∃as. charpoly A = (∏a←as. [:- a, 1:]) ∧ length as = CARD ('n)" by (transfer_hma rule:char_poly_factorized) lemma eigvals_poly_length: fixes A :: "complex^'n^'n" shows "charpoly A = (∏a∈#eigenvalues A. [:- a, 1:])" (is "?A") "size (eigenvalues A) = CARD ('n)" (is "?B") proof - define f where "f as = (charpoly A = (∏a∈#as. [:- a, 1:]) ∧ size as = CARD('n))" for as obtain as where as_def: "charpoly A = (∏a←as. [:- a, 1:])" "length as = CARD('n)" using char_poly_factorized_hma by auto have "charpoly A = (∏a←as. [:- a, 1:])" unfolding as_def by simp also have "... = (∏a∈#mset as. [:- a, 1:])" unfolding prod_mset_prod_list[symmetric] mset_map by simp finally have "charpoly A = (∏a∈#mset as. [:- a, 1:])" by simp moreover have "size (mset as) = CARD('n)" using as_def by simp ultimately have "f (mset as)" unfolding f_def by auto hence "f (eigenvalues A)" unfolding eigenvalues_def f_def[symmetric] using someI[where x = "mset as" and P="f"] by auto thus ?A ?B unfolding f_def by auto qed lemma similar_matrix_eigvals: fixes A B :: "complex^'n^'n" assumes "similar_matrix A B" shows "eigenvalues A = eigenvalues B" proof - have "(∏a∈#eigenvalues A. [:- a, 1:]) = (∏a∈#eigenvalues B. [:- a, 1:])" using similar_matrix_charpoly[OF assms] unfolding eigvals_poly_length(1) by simp thus ?thesis by (intro poly_prod_inj) simp qed definition upper_triangular_hma :: "'a::zero^'n^'n ⇒ bool" where "upper_triangular_hma A ≡ ∀i. ∀ j. (to_nat j < Bij_Nat.to_nat i ⟶ A $h i $h j = 0)" lemma for_all_reindex2: assumes "range f = A" shows "(∀x ∈ A. ∀y ∈ A. P x y) ⟷ (∀x y. P (f x) (f y))" using assms by auto lemma upper_triangular_hma: fixes A :: "('a::zero)^'n^'n" shows "upper_triangular (from_hma⇩_{m}A) = upper_triangular_hma A" (is "?L = ?R") proof - have "?L ⟷ (∀i∈{0..<CARD('n)}. ∀j∈{0..<CARD('n)}. j < i ⟶ A $h from_nat i $h from_nat j = 0)" unfolding upper_triangular_def from_hma⇩_{m}_def by auto also have "... ⟷ (∀(i::'n) (j::'n). to_nat j < to_nat i ⟶ A $h from_nat (to_nat i) $h from_nat (to_nat j) = 0)" by (intro for_all_reindex2 range_to_nat[where 'a="'n"]) also have "... ⟷ ?R" unfolding upper_triangular_hma_def by auto finally show ?thesis by simp qed lemma from_hma_carrier: fixes A :: "'a^('n::finite)^('m::finite)" shows "from_hma⇩_{m}A ∈ carrier_mat (CARD ('m)) (CARD ('n))" unfolding from_hma⇩_{m}_def by simp definition diag_mat_hma :: "'a^'n^'n ⇒ 'a multiset" where "diag_mat_hma A = image_mset (λi. A $h i $h i) (mset_set UNIV)" lemma diag_mat_hma: fixes A :: "'a^'n^'n" shows "mset (diag_mat (from_hma⇩_{m}A)) = diag_mat_hma A" (is "?L = ?R") proof - have "?L = {#from_hma⇩_{m}A $$ (i, i). i ∈# mset [0..<CARD('n)]#}" using from_hma_carrier[where A="A"] unfolding diag_mat_def mset_map by simp also have "... = {#from_hma⇩_{m}A $$ (i, i). i ∈# image_mset to_nat (mset_set (UNIV :: 'n set))#}" using range_to_nat[where 'a="'n"] by (intro arg_cong2[where f="image_mset"] refl) (simp add:image_mset_mset_set[OF inj_to_nat]) also have "... = {#from_hma⇩_{m}A $$ (to_nat i, to_nat i). i ∈# (mset_set (UNIV :: 'n set))#}" by (simp add:image_mset.compositionality comp_def) also have "... = ?R" unfolding diag_mat_hma_def from_hma⇩_{m}_def using to_nat_less_card[where 'a="'n"] by (intro image_mset_cong) auto finally show ?thesis by simp qed definition adjoint_hma :: "complex^'m^'n ⇒ complex^'n^'m" where "adjoint_hma A = map_matrix cnj (transpose A)" lemma adjoint_hma_eq: "adjoint_hma A $h i $h j = cnj (A $h j $h i)" unfolding adjoint_hma_def map_matrix_def map_vector_def transpose_def by auto lemma adjoint_hma: fixes A :: "complex^('n::finite)^('m::finite)" shows "mat_adjoint (from_hma⇩_{m}A) = from_hma⇩_{m}(adjoint_hma A)" proof - have "mat_adjoint (from_hma⇩_{m}A) $$ (i,j) = from_hma⇩_{m}(adjoint_hma A) $$ (i,j)" if "i < CARD('n)" "j < CARD('m)" for i j using from_hma_carrier that unfolding mat_adjoint_def from_hma⇩_{m}_def adjoint_hma_def Matrix.mat_of_rows_def map_matrix_def map_vector_def transpose_def by auto thus ?thesis using from_hma_carrier by (intro eq_matI) auto qed definition cinner where "cinner v w = scalar_product v (map_vector cnj w)" context includes lifting_syntax begin lemma cinner_hma: fixes x y :: "complex^'n" shows "cinner x y = (from_hma⇩_{v}x) ∙c (from_hma⇩_{v}y)" (is "?L = ?R") proof - have "?L = (∑i∈UNIV. x $h i * cnj (y $h i))" unfolding cinner_def map_vector_def scalar_product_def by simp also have "... = (∑i = 0..<CARD('n). x $h from_nat i * cnj (y $h from_nat i))" using to_nat_less_card to_nat_from_nat_id by (intro sum.reindex_bij_betw[symmetric] bij_betwI[where g="to_nat"]) auto also have "... = ?R" unfolding Matrix.scalar_prod_def from_hma⇩_{v}_def by simp finally show ?thesis by simp qed lemma cinner_hma_transfer[transfer_rule]: "(HMA_V ===> HMA_V ===> (=)) (∙c) cinner" unfolding HMA_V_def cinner_hma by (auto simp:rel_fun_def) lemma adjoint_hma_transfer[transfer_rule]: "(HMA_M ===> HMA_M) (mat_adjoint) adjoint_hma" unfolding HMA_M_def rel_fun_def by (auto simp add:adjoint_hma) end lemma adjoint_adjoint_id[simp]: "adjoint_hma (adjoint_hma A ) = A" by (transfer) (simp add:adjoint_adjoint) lemma adjoint_def_alter_hma: "cinner (A *v v) w = cinner v (adjoint_hma A *v w)" by (transfer_hma rule:adjoint_def_alter) lemma cinner_0: "cinner 0 0 = 0" by (transfer_hma) lemma cinner_scale_left: "cinner (a *s v) w = a * cinner v w" by transfer_hma lemma cinner_scale_right: "cinner v (a *s w) = cnj a * cinner v w" by transfer (simp add: inner_prod_smult_right) lemma norm_of_real: shows "norm (map_vector complex_of_real v) = norm v" unfolding norm_vec_def map_vector_def by (intro L2_set_cong) auto definition unitary_hma :: "complex^'n^'n ⇒ bool" where "unitary_hma A ⟷ A ** adjoint_hma A = Finite_Cartesian_Product.mat 1" definition unitarily_equiv_hma where "unitarily_equiv_hma A B U ≡ (unitary_hma U ∧ similar_matrix_wit A B U (adjoint_hma U))" definition diagonal_mat :: "('a::zero)^('n::finite)^'n ⇒ bool" where "diagonal_mat A ≡ (∀i. ∀j. i ≠ j ⟶ A $h i $h j = 0)" lemma diagonal_mat_ex: assumes "diagonal_mat A" shows "A = diag (χ i. A $h i $h i)" using assms unfolding diagonal_mat_def diag_def by (intro iffD2[OF vec_eq_iff] allI) auto lemma diag_diagonal_mat[simp]: "diagonal_mat (diag x)" unfolding diag_def diagonal_mat_def by auto lemma diag_imp_upper_tri: "diagonal_mat A ⟹ upper_triangular_hma A" unfolding diagonal_mat_def upper_triangular_hma_def by (metis nat_neq_iff) definition unitary_diag where "unitary_diag A b U ≡ unitarily_equiv_hma A (diag b) U" definition real_diag_decomp_hma where "real_diag_decomp_hma A d U ≡ unitary_diag A d U ∧ (∀i. d $h i ∈ Reals)" definition hermitian_hma :: "complex^'n^'n ⇒ bool" where "hermitian_hma A = (adjoint_hma A = A)" lemma from_hma_one: "from_hma⇩_{m}(mat 1 :: (('a::{one,zero})^'n^'n)) = 1⇩_{m}CARD('n)" unfolding Finite_Cartesian_Product.mat_def from_hma⇩_{m}_def using from_nat_inj by (intro eq_matI) auto lemma from_hma_mult: fixes A :: "('a :: semiring_1)^'m^'n" fixes B :: "'a^'k^'m::finite" shows "from_hma⇩_{m}A * from_hma⇩_{m}B = from_hma⇩_{m}(A ** B)" using HMA_M_mult unfolding rel_fun_def HMA_M_def by auto lemma hermitian_hma: "hermitian_hma A = hermitian (from_hma⇩_{m}A)" unfolding hermitian_def adjoint_hma hermitian_hma_def by auto lemma unitary_hma: fixes A :: "complex^'n^'n" shows "unitary_hma A = unitary (from_hma⇩_{m}A)" (is "?L = ?R") proof - have "?R ⟷ from_hma⇩_{m}A * mat_adjoint (from_hma⇩_{m}A) = 1⇩_{m}(CARD('n))" using from_hma_carrier unfolding unitary_def inverts_mat_def by simp also have "... ⟷ from_hma⇩_{m}(A ** adjoint_hma A) = from_hma⇩_{m}(mat 1::complex^'n^'n)" unfolding adjoint_hma from_hma_mult from_hma_one by simp also have "... ⟷ A ** adjoint_hma A = Finite_Cartesian_Product.mat 1" unfolding from_hma⇩_{m}_inj by simp also have "... ⟷ ?L" unfolding unitary_hma_def by simp finally show ?thesis by simp qed lemma unitary_hmaD: fixes A :: "complex^'n^'n" assumes "unitary_hma A" shows "adjoint_hma A ** A = mat 1" (is "?A") "A ** adjoint_hma A = mat 1" (is "?B") proof - have "mat_adjoint (from_hma⇩_{m}A) * from_hma⇩_{m}A = 1⇩_{m}CARD('n)" using assms unitary_hma by (intro unitary_simps from_hma_carrier ) auto thus ?A unfolding adjoint_hma from_hma_mult from_hma_one[symmetric] from_hma⇩_{m}_inj by simp show ?B using assms unfolding unitary_hma_def by simp qed lemma unitary_hma_adjoint: assumes "unitary_hma A" shows "unitary_hma (adjoint_hma A)" unfolding unitary_hma_def adjoint_adjoint_id unitary_hmaD[OF assms] by simp lemma unitarily_equiv_hma: fixes A :: "complex^'n^'n" shows "unitarily_equiv_hma A B U = unitarily_equiv (from_hma⇩_{m}A) (from_hma⇩_{m}B) (from_hma⇩_{m}U)" (is "?L = ?R") proof - have "?R ⟷ (unitary_hma U ∧ similar_mat_wit (from_hma⇩_{m}A) (from_hma⇩_{m}B) (from_hma⇩_{m}U) (from_hma⇩_{m}(adjoint_hma U)))" unfolding Spectral_Theory_Complements.unitarily_equiv_def unitary_hma[symmetric] adjoint_hma by simp also have "... ⟷ unitary_hma U ∧ similar_matrix_wit A B U (adjoint_hma U)" using HMA_similar_mat_wit unfolding rel_fun_def HMA_M_def by (intro arg_cong2[where f="(∧)"] refl) force also have "... ⟷ ?L" unfolding unitarily_equiv_hma_def by auto finally show ?thesis by simp qed lemma Matrix_diagonal_matD: assumes "Matrix.diagonal_mat A" assumes "i<dim_row A" "j<dim_col A" assumes "i ≠ j" shows "A $$ (i,j) = 0" using assms unfolding Matrix.diagonal_mat_def by auto lemma diagonal_mat_hma: fixes A :: "('a :: zero)^('n :: finite)^'n" shows "diagonal_mat A = Matrix.diagonal_mat (from_hma⇩_{m}A)" (is "?L = ?R") proof show "?L ⟹ ?R" unfolding diagonal_mat_def Matrix.diagonal_mat_def from_hma⇩_{m}_def using from_nat_inj by auto next assume a:"?R" have "A $h i $h j = 0" if "i ≠ j" for i j proof - have "A $h i $h j = (from_hma⇩_{m}A) $$ (to_nat i,to_nat j)" unfolding from_hma⇩_{m}_def using to_nat_less_card[where 'a="'n"] by simp also have "... = 0" using to_nat_less_card[where 'a="'n"] to_nat_inj that by (intro Matrix_diagonal_matD[OF a]) auto finally show ?thesis by simp qed thus "?L" unfolding diagonal_mat_def by auto qed lemma unitary_diag_hma: fixes A :: "complex^'n^'n" shows "unitary_diag A d U = Spectral_Theory_Complements.unitary_diag (from_hma⇩_{m}A) (from_hma⇩_{m}(diag d)) (from_hma⇩_{m}U)" proof - have "Matrix.diagonal_mat (from_hma⇩_{m}(diag d))" unfolding diagonal_mat_hma[symmetric] by simp thus ?thesis unfolding unitary_diag_def Spectral_Theory_Complements.unitary_diag_def unitarily_equiv_hma by auto qed lemma real_diag_decomp_hma: fixes A :: "complex^'n^'n" shows "real_diag_decomp_hma A d U = real_diag_decomp (from_hma⇩_{m}A) (from_hma⇩_{m}(diag d)) (from_hma⇩_{m}U)" proof - have 0:"(∀i. d $h i ∈ ℝ) ⟷ (∀i < CARD('n). from_hma⇩_{m}(diag d) $$ (i,i) ∈ ℝ)" unfolding from_hma⇩_{m}_def diag_def using to_nat_less_card by fastforce show ?thesis unfolding real_diag_decomp_hma_def real_diag_decomp_def unitary_diag_hma 0 by auto qed lemma diagonal_mat_diag_ex_hma: assumes "Matrix.diagonal_mat A" "A ∈ carrier_mat CARD('n) CARD ('n :: finite)" shows "from_hma⇩_{m}(diag (χ (i::'n). A $$ (to_nat i,to_nat i))) = A" using assms from_nat_inj unfolding from_hma⇩_{m}_def diag_def Matrix.diagonal_mat_def by (intro eq_matI) (auto simp add:to_nat_from_nat_id) theorem commuting_hermitian_family_diag_hma: fixes Af :: "(complex^'n^'n) set" assumes "finite Af" and "Af ≠ {}" and "⋀A. A ∈ Af ⟹ hermitian_hma A" and "⋀A B. A ∈ Af ⟹ B∈ Af ⟹ A ** B = B ** A" shows "∃ U. ∀ A∈ Af. ∃B. real_diag_decomp_hma A B U" proof - have 0:"finite (from_hma⇩_{m}` Af)" using assms(1)by (intro finite_imageI) have 1: "from_hma⇩_{m}` Af ≠ {}" using assms(2) by simp have 2: "A ∈ carrier_mat (CARD ('n)) (CARD ('n))" if "A ∈ from_hma⇩_{m}` Af" for A using that unfolding from_hma⇩_{m}_def by (auto simp add:image_iff) have 3: "0 < CARD('n)" by simp have 4: "hermitian A" if "A ∈ from_hma⇩_{m}` Af" for A using hermitian_hma assms(3) that by auto have 5: "A * B = B * A" if "A ∈ from_hma⇩_{m}` Af" "B ∈ from_hma⇩_{m}` Af" for A B using that assms(4) by (auto simp add:image_iff from_hma_mult) have "∃U. ∀A∈ from_hma⇩_{m}` Af. ∃B. real_diag_decomp A B U" using commuting_hermitian_family_diag[OF 0 1 2 3 4 5] by auto then obtain U Bmap where U_def: "⋀A. A ∈ from_hma⇩_{m}` Af ⟹ real_diag_decomp A (Bmap A) U" by metis define U' :: "complex^'n^'n" where "U' = to_hma⇩_{m}U" define Bmap' :: "complex^'n^'n ⇒ complex^'n" where "Bmap' = (λM. (χ i. (Bmap (from_hma⇩_{m}M)) $$ (to_nat i,to_nat i)))" have "real_diag_decomp_hma A (Bmap' A) U'" if "A ∈ Af" for A proof - have rdd: "real_diag_decomp (from_hma⇩_{m}A) (Bmap (from_hma⇩_{m}A)) U" using U_def that by simp have "U ∈ carrier_mat CARD('n) CARD('n)" "Bmap (from_hma⇩_{m}A) ∈ carrier_mat CARD('n) CARD('n)" "Matrix.diagonal_mat (Bmap (from_hma⇩_{m}A))" using rdd unfolding real_diag_decomp_def Spectral_Theory_Complements.unitary_diag_def Spectral_Theory_Complements.unitarily_equiv_def similar_mat_wit_def by (auto simp add:Let_def) hence "(from_hma⇩_{m}(diag (Bmap' A))) = Bmap (from_hma⇩_{m}A)" "(from_hma⇩_{m}U') = U" unfolding Bmap'_def U'_def by (auto simp add:diagonal_mat_diag_ex_hma) hence "real_diag_decomp (from_hma⇩_{m}A) (from_hma⇩_{m}(diag (Bmap' A))) (from_hma⇩_{m}U')" using rdd by auto thus "?thesis" unfolding real_diag_decomp_hma by simp qed thus ?thesis by (intro exI[where x="U'"]) auto qed lemma char_poly_upper_triangular: fixes A :: "complex^'n^'n" assumes "upper_triangular_hma A" shows "charpoly A = (∏a ∈# diag_mat_hma A. [:- a, 1:])" proof - have "charpoly A = char_poly (from_hma⇩_{m}A)" using HMA_char_poly unfolding rel_fun_def HMA_M_def by (auto simp add:eq_commute) also have "... = (∏a←diag_mat (from_hma⇩_{m}A). [:- a, 1:])" using assms unfolding upper_triangular_hma[symmetric] by (intro char_poly_upper_triangular[where n="CARD('n)"] from_hma_carrier) auto also have "... = (∏a∈# mset (diag_mat (from_hma⇩_{m}A)). [:- a, 1:])" unfolding prod_mset_prod_list[symmetric] mset_map by simp also have "... = (∏a∈# diag_mat_hma A. [:- a, 1:])" unfolding diag_mat_hma by simp finally show "charpoly A = (∏a∈# diag_mat_hma A. [:- a, 1:])" by simp qed lemma upper_tri_eigvals: fixes A :: "complex^'n^'n" assumes "upper_triangular_hma A" shows "eigenvalues A = diag_mat_hma A" proof - have "(∏a∈#eigenvalues A. [:- a, 1:]) = charpoly A" unfolding eigvals_poly_length[symmetric] by simp also have "... = (∏a∈#diag_mat_hma A. [:- a, 1:])" by (intro char_poly_upper_triangular assms) finally have "(∏a∈#eigenvalues A. [:- a, 1:]) = (∏a∈#diag_mat_hma A. [:- a, 1:])" by simp thus ?thesis by (intro poly_prod_inj) simp qed lemma cinner_self: fixes v :: "complex^'n" shows "cinner v v = norm v^2" proof - have 0: "x * cnj x = complex_of_real (x ∙ x)" for x :: complex unfolding inner_complex_def complex_mult_cnj by (simp add:power2_eq_square) thus ?thesis unfolding cinner_def power2_norm_eq_inner scalar_product_def inner_vec_def map_vector_def by simp qed lemma unitary_iso: assumes "unitary_hma U" shows "norm (U *v v) = norm v" proof - have "norm (U *v v)^2 = cinner (U *v v) (U *v v)" unfolding cinner_self by simp also have "... = cinner v v" unfolding adjoint_def_alter_hma matrix_vector_mul_assoc unitary_hmaD[OF assms] by simp also have "... = norm v^2" unfolding cinner_self by simp finally have "complex_of_real (norm (U *v v)^2) = norm v^2" by simp thus ?thesis by (meson norm_ge_zero of_real_hom.injectivity power2_eq_iff_nonneg) qed lemma (in semiring_hom) mult_mat_vec_hma: "map_vector hom (A *v v) = map_matrix hom A *v map_vector hom v" using mult_mat_vec_hom by transfer auto lemma (in semiring_hom) mat_hom_mult_hma: "map_matrix hom (A ** B) = map_matrix hom A ** map_matrix hom B" using mat_hom_mult by transfer auto context regular_graph_tts begin lemma to_nat_less_n: "to_nat (x::'n) < n" using to_nat_less_card card_n by metis lemma to_nat_from_nat: "x < n ⟹ to_nat (from_nat x :: 'n) = x" using to_nat_from_nat_id card_n by metis lemma hermitian_A: "hermitian_hma A" using count_sym unfolding hermitian_hma_def adjoint_hma_def A_def map_matrix_def map_vector_def transpose_def by simp lemma nonneg_A: "nonneg_mat A" unfolding nonneg_mat_def A_def by auto lemma g_step_1: assumes "v ∈ verts G" shows "g_step (λ_. 1) v = 1" (is "?L = ?R") proof - have "?L = in_degree G v / d" unfolding g_step_def in_degree_def by simp also have "... = 1" unfolding reg(2)[OF assms] using d_gt_0 by simp finally show ?thesis by simp qed lemma markov: "markov (A :: real^'n^'n)" proof - have "A *v 1 = (1::real ^'n)" (is "?L = ?R") proof - have "A *v 1 = (χ i. g_step (λ_. 1) (enum_verts i))" unfolding g_step_conv one_vec_def by simp also have "... = (χ i. 1)" using bij_betw_apply[OF enum_verts] by (subst g_step_1) auto also have "... = 1" unfolding one_vec_def by simp finally show ?thesis by simp qed thus ?thesis by (intro markov_symI nonneg_A symmetric_A) qed lemma nonneg_J: "nonneg_mat J" unfolding nonneg_mat_def J_def by auto lemma J_eigvals: "eigenvalues J = {#1::complex#} + replicate_mset (n - 1) 0" proof - define α :: "nat ⇒ real" where "α i = sqrt (i^2+i)" for i :: nat define q :: "nat ⇒ nat ⇒ real" where "q i j = ( if i = 0 then (1/sqrt n) else ( if j < i then ((-1) / α i) else ( if j = i then (i / α i) else 0)))" for i j define Q :: "complex^'n^'n" where "Q = (χ i j. complex_of_real (q (to_nat i) (to_nat j)))" define D :: "complex^'n^'n" where "D = (χ i j. if to_nat i = 0 ∧ to_nat j = 0 then 1 else 0)" have 2: "[0..<n] = 0#[1..<n]" using n_gt_0 upt_conv_Cons by auto have aux0: "(∑k = 0..<n. q j k * q i k) = of_bool (i = j)" if 1:"i ≤ j" "j < n" for i j proof - consider (a) "i = j ∧ j = 0" | (b) "i = 0 ∧ i < j" | (c) " 0 < i ∧ i < j" | (d) "0 < i ∧ i = j" using 1 by linarith thus ?thesis proof (cases) case a then show ?thesis using n_gt_0 by (simp add:q_def) next case b have "(∑k = 0..<n. q j k*q i k)=(∑k∈insert j ({0..<j} ∪ {j+1..<n}). q j k*q i k)" using that(2) by (intro sum.cong) auto also have "...=q j j*q i j+(∑k=0..<j. q j k * q i k)+(∑k=j+1..<n. q j k * q i k)" by (subst sum.insert) (auto simp add: sum.union_disjoint) also have "... = 0" using b unfolding q_def by simp finally show ?thesis using b by simp next case c have "(∑k = 0..<n. q j k*q i k)=(∑k∈insert i ({0..<i} ∪ {i+1..<n}). q j k*q i k)" using that(2) c by (intro sum.cong) auto also have "...=q j i*q i i+(∑k=0..<i. q j k * q i k)+(∑k=i+1..<n. q j k * q i k)" by (subst sum.insert) (auto simp add: sum.union_disjoint) also have "... =(-1) / α j * i / α i+ i * ((-1) / α j * (-1) / α i)" using c unfolding q_def by simp also have "... = 0" by (simp add:algebra_simps) finally show ?thesis using c by simp next case d have "real i + real i^2 = real (i + i^2)" by simp also have "... ≠ real 0" unfolding of_nat_eq_iff using d by simp finally have d_1: "real i + real i^2 ≠ 0" by simp have "(∑k = 0..<n. q j k*q i k)=(∑k∈insert i ({0..<i} ∪ {i+1..<n}). q j k*q i k)" using that(2) d by (intro sum.cong) auto also have "...=q j i*q i i+(∑k=0..<i. q j k * q i k)+(∑k=i+1..<n. q j k * q i k)" by (subst sum.insert) (auto simp add: sum.union_disjoint) also have "... = i/ α i * i / α i+ i * ((-1) / α i * (-1) / α i)" using d that unfolding q_def by simp also have "... = (i^2 + i) / (α i)^2" by (simp add: power2_eq_square divide_simps) also have "... = 1" using d_1 unfolding α_def by (simp add:algebra_simps) finally show ?thesis using d by simp qed qed have 0:"(∑k = 0..<n. q j k * q i k) = of_bool (i = j)" (is "?L = ?R") if "i < n" "j < n" for i j proof - have "?L = (∑k = 0..<n. q (max i j) k * q (min i j) k)" by (cases "i ≤ j") ( simp_all add:ac_simps cong:sum.cong) also have "... = of_bool (min i j = max i j)" using that by (intro aux0) auto also have "... = ?R" by (cases "i ≤ j") auto finally show ?thesis by simp qed have "(∑k∈UNIV. Q $h j $h k * cnj (Q $h i $h k)) = of_bool (i=j)" (is "?L = ?R") for i j proof - have "?L = complex_of_real (∑k ∈ (UNIV::'n set). q (to_nat j) (to_nat k) * q (to_nat i) (to_nat k))" unfolding Q_def by (simp add:case_prod_beta scalar_prod_def map_vector_def inner_vec_def row_def inner_complex_def) also have "... = complex_of_real (∑k=0..<n. q (to_nat j) k * q (to_nat i) k)" using to_nat_less_n to_nat_from_nat by (intro arg_cong[where f="of_real"] sum.reindex_bij_betw bij_betwI[where g="from_nat"]) (auto) also have "... = complex_of_real (of_bool(to_nat i = to_nat j))" using to_nat_less_n by (intro arg_cong[where f="of_real"] 0) auto also have "... = ?R" using to_nat_inj by auto finally show ?thesis by simp qed hence "Q ** adjoint_hma Q = mat 1" by (intro iffD2[OF vec_eq_iff]) (auto simp add:matrix_matrix_mult_def mat_def adjoint_hma_eq) hence unit_Q: "unitary_hma Q" unfolding unitary_hma_def by simp have "card {(k::'n). to_nat k = 0} = card {from_nat 0 :: 'n}" using to_nat_from_nat[where x="0"] n_gt_0 by (intro arg_cong[where f="card"] iffD2[OF set_eq_iff]) auto hence 5:"card {(k::'n). to_nat k = 0} = 1" by simp hence 1:"adjoint_hma Q ** D = (χ i j. (if to_nat j = 0 then complex_of_real (1/sqrt n) else 0))" unfolding Q_def D_def by (intro iffD2[OF vec_eq_iff] allI) (auto simp add:adjoint_hma_eq matrix_matrix_mult_def q_def if_distrib if_distribR sum.If_cases) have "(adjoint_hma Q ** D ** Q) $h i $h j = J $h i $h j" (is "?L1 = ?R1") for i j proof - have "?L1 =1/((sqrt (real n)) * complex_of_real (sqrt (real n)))" unfolding 1 unfolding Q_def using n_gt_0 5 by (auto simp add:matrix_matrix_mult_def q_def if_distrib if_distribR sum.If_cases) also have "... = 1/sqrt (real n)^2" unfolding of_real_divide of_real_mult power2_eq_square by simp also have "... = J $h i $h j" unfolding J_def card_n using n_gt_0 by simp finally show ?thesis by simp qed hence "adjoint_hma Q ** D ** Q = J" by (intro iffD2[OF vec_eq_iff] allI) auto hence "similar_matrix_wit J D (adjoint_hma Q) Q" unfolding similar_matrix_wit_def unitary_hmaD[OF unit_Q] by auto hence "similar_matrix J D" unfolding similar_matrix_def by auto hence "eigenvalues J = eigenvalues D" by (intro similar_matrix_eigvals) also have "... = diag_mat_hma D" by (intro upper_tri_eigvals diag_imp_upper_tri) (simp add:D_def diagonal_mat_def) also have "... = {# of_bool (to_nat i = 0). i ∈# mset_set (UNIV :: 'n set)#}" unfolding diag_mat_hma_def D_def of_bool_def by simp also have "... = {# of_bool (i = 0). i ∈# mset_set (to_nat ` (UNIV :: 'n set))#}" unfolding image_mset_mset_set[OF inj_to_nat, symmetric] by (simp add:image_mset.compositionality comp_def) also have "... = mset (map (λi. of_bool(i=0)) [0..<n])" unfolding range_to_nat card_n mset_map by simp also have "... = mset (1 # map (λi. 0) [1..<n])" unfolding 2 by (intro arg_cong[where f="mset"]) simp also have "... = {#1#} + replicate_mset (n-1) 0" using n_gt_0 by (simp add:map_replicate_const mset_repl) finally show ?thesis by simp qed lemma J_markov: "markov J" proof - have "nonneg_mat J" unfolding J_def nonneg_mat_def by auto moreover have "transpose J = J" unfolding J_def transpose_def by auto moreover have "J *v 1 = (1 :: real^'n)" unfolding J_def by (simp add:matrix_vector_mult_def one_vec_def) ultimately show ?thesis by (intro markov_symI) auto qed lemma markov_complex_apply: assumes "markov M" shows "(map_matrix complex_of_real M) *v (1 :: complex^'n) = 1" (is "?L = ?R") proof - have "?L = (map_matrix complex_of_real M) *v (map_vector complex_of_real 1)" by (intro arg_cong2[where f="(*v)"] refl) (simp add: map_vector_def one_vec_def) also have "... = map_vector (complex_of_real) 1" unfolding of_real_hom.mult_mat_vec_hma[symmetric] markov_apply[OF assms] by simp also have "... = ?R" by (simp add: map_vector_def one_vec_def) finally show ?thesis by simp qed lemma J_A_comm_real: "J ** A = A ** (J :: real^'n^'n)" proof - have 0: "(∑k∈UNIV. A $h k $h i / real CARD('n)) = 1 / real CARD('n)" (is "?L = ?R") for i proof - have "?L = (1 v* A) $h i / real CARD('n)" unfolding vector_matrix_mult_def by (simp add:sum_divide_distrib) also have "... = ?R" unfolding markov_apply[OF markov] by simp finally show ?thesis by simp qed have 1: "(∑k∈UNIV. A $h i $h k / real CARD('n)) = 1 / real CARD('n)" (is "?L = ?R") for i proof - have "?L = (A *v 1) $h i / real CARD('n)" unfolding matrix_vector_mult_def by (simp add:sum_divide_distrib) also have "... = ?R" unfolding markov_apply[OF markov] by simp finally show ?thesis by simp qed show ?thesis unfolding J_def using 0 1 by (intro iffD2[OF vec_eq_iff] allI) (simp add:matrix_matrix_mult_def) qed lemma J_A_comm: "J ** A = A ** (J :: complex^'n^'n)" (is "?L = ?R") proof - have "J ** A = map_matrix complex_of_real (J ** A)" unfolding of_real_hom.mat_hom_mult_hma J_def A_def by (auto simp add:map_matrix_def map_vector_def) also have "... = map_matrix complex_of_real (A ** J)" unfolding J_A_comm_real by simp also have "... = map_matrix complex_of_real A ** map_matrix complex_of_real J" unfolding of_real_hom.mat_hom_mult_hma by simp also have "... = ?R" unfolding A_def J_def by (auto simp add:map_matrix_def map_vector_def) finally show ?thesis by simp qed definition γ⇩_{a}:: "'n itself ⇒ real" where "γ⇩_{a}_ = (if n > 1 then Max_mset (image_mset cmod (eigenvalues A - {#1#})) else 0)" definition γ⇩_{2}:: "'n itself ⇒ real" where "γ⇩_{2}_ = (if n > 1 then Max_mset {# Re x. x ∈# (eigenvalues A - {#1#})#} else 0)" lemma J_sym: "hermitian_hma J" unfolding J_def hermitian_hma_def by (intro iffD2[OF vec_eq_iff] allI) (simp add: adjoint_hma_eq) lemma shows evs_real: "set_mset (eigenvalues A::complex multiset) ⊆ ℝ" (is "?R1") and ev_1: "(1::complex) ∈# eigenvalues A" and γ⇩_{a}_ge_0: "γ⇩_{a}TYPE ('n) ≥ 0" and find_any_ev: "∀α ∈# eigenvalues A - {#1#}. ∃v. cinner v 1 = 0 ∧ v ≠ 0 ∧ A *v v = α *s v" and γ⇩_{a}_bound: "∀v. cinner v 1 = 0 ⟶ norm (A *v v) ≤ γ⇩_{a}TYPE('n) * norm v" and γ⇩_{2}_bound: "∀(v::real^'n). v ∙ 1 = 0 ⟶ v ∙ (A *v v) ≤ γ⇩_{2}TYPE ('n) * norm v^2" proof - have "∃ U. ∀ A∈ {J,A}. ∃B. real_diag_decomp_hma A B U" using J_sym hermitian_A J_A_comm by (intro commuting_hermitian_family_diag_hma) auto then obtain U Ad Jd where A_decomp: "real_diag_decomp_hma A Ad U" and K_decomp: "real_diag_decomp_hma J Jd U" by auto have J_sim: "similar_matrix_wit J (diag Jd) U (adjoint_hma U)" and unit_U: "unitary_hma U" using K_decomp unfolding real_diag_decomp_hma_def unitary_diag_def unitarily_equiv_hma_def by auto have "diag_mat_hma (diag Jd) = eigenvalues (diag Jd)" by (intro upper_tri_eigvals[symmetric] diag_imp_upper_tri J_sim) auto also have "... = eigenvalues J" using J_sim by (intro similar_matrix_eigvals[symmetric]) (auto simp add:similar_matrix_def) also have "... ={#1::complex#} + replicate_mset (n - 1) 0" unfolding J_eigvals by simp finally have 0:"diag_mat_hma (diag Jd) = {#1::complex#} + replicate_mset (n - 1) 0" by simp hence "1 ∈# diag_mat_hma (diag Jd)" by simp then obtain i where i_def:"Jd $h i = 1" unfolding diag_mat_hma_def diag_def by auto have "{# Jd $h j. j ∈# mset_set (UNIV - {i}) #} = {#Jd $h j. j ∈# mset_set UNIV - mset_set {i}#}" unfolding diag_mat_hma_def by (intro arg_cong2[where f="image_mset"] mset_set_Diff) auto also have "... = diag_mat_hma (diag Jd) - {#1#}" unfolding diag_mat_hma_def diag_def by (subst image_mset_Diff) (auto simp add:i_def) also have "... = replicate_mset (n - 1) 0" unfolding 0 by simp finally have "{# Jd $h j. j ∈# mset_set (UNIV - {i}) #} = replicate_mset (n - 1) 0" by simp hence "set_mset {# Jd $h j. j ∈# mset_set (UNIV - {i}) #} ⊆ {0}" by simp hence 1:"Jd $h j = 0" if "j ≠ i" for j using that by auto define u where "u = adjoint_hma U *v 1" define α where "α = u $h i" have "U *v u = (U ** adjoint_hma U) *v 1" unfolding u_def by (simp add:matrix_vector_mul_assoc) also have "... = 1" unfolding unitary_hmaD[OF unit_U] by simp also have "... ≠ 0" by simp finally have "U *v u ≠ 0" by simp hence u_nz: "u ≠ 0" by (cases "u = 0") auto have "diag Jd *v u = adjoint_hma U ** U ** diag Jd ** adjoint_hma U *v 1" unfolding unitary_hmaD[OF unit_U] u_def by (auto simp add:matrix_vector_mul_assoc) also have "... = adjoint_hma U ** (U ** diag Jd ** adjoint_hma U) *v 1" by (simp add:matrix_mul_assoc) also have "... = adjoint_hma U ** J *v 1" using J_sim unfolding similar_matrix_wit_def by simp also have "... = adjoint_hma U *v (map_matrix complex_of_real J *v 1)" by (simp add:map_matrix_def map_vector_def J_def matrix_vector_mul_assoc) also have "... = u" unfolding u_def markov_complex_apply[OF J_markov] by simp finally have u_ev: "diag Jd *v u = u" by simp hence "Jd * u = u" unfolding diag_vec_mult_eq by simp hence "u $h j = 0" if "j ≠ i" for j using 1 that unfolding times_vec_def vec_eq_iff by auto hence u_alt: "u = axis i α" unfolding α_def axis_def vec_eq_iff by auto hence α_nz: "α ≠ 0" using u_nz by (cases "α=0") auto have A_sim: "similar_matrix_wit A (diag Ad) U (adjoint_hma U)" and Ad_real: "∀i. Ad $h i ∈ ℝ" using A_decomp unfolding real_diag_decomp_hma_def unitary_diag_def unitarily_equiv_hma_def by auto have "diag_mat_hma (diag Ad) = eigenvalues (diag Ad)" by (intro upper_tri_eigvals[symmetric] diag_imp_upper_tri A_sim) auto also have "... = eigenvalues A" using A_sim by (intro similar_matrix_eigvals[symmetric]) (auto simp add:similar_matrix_def) finally have 3:"diag_mat_hma (diag Ad) = eigenvalues A" by simp show ?R1 unfolding 3[symmetric] diag_mat_hma_def diag_def using Ad_real by auto have "diag Ad *v u = adjoint_hma U ** U ** diag Ad ** adjoint_hma U *v 1" unfolding unitary_hmaD[OF unit_U] u_def by (auto simp add:matrix_vector_mul_assoc) also have "... = adjoint_hma U ** (U ** diag Ad ** adjoint_hma U) *v 1" by (simp add:matrix_mul_assoc) also have "... = adjoint_hma U ** A *v 1" using A_sim unfolding similar_matrix_wit_def by simp also have "... = adjoint_hma U *v (map_matrix complex_of_real A *v 1)" by (simp add:map_matrix_def map_vector_def A_def matrix_vector_mul_assoc) also have "... = u" unfolding u_def markov_complex_apply[OF markov] by simp finally have u_ev_A: "diag Ad *v u = u" by simp hence "Ad * u = u" unfolding diag_vec_mult_eq by simp hence 5:"Ad $h i = 1" using α_nz unfolding u_alt times_vec_def vec_eq_iff axis_def by force thus ev_1: "(1::complex) ∈# eigenvalues A" unfolding 3[symmetric] diag_mat_hma_def diag_def by auto have "eigenvalues A - {#1#} = diag_mat_hma (diag Ad) - {#1#}" unfolding 3 by simp also have "... = {#Ad $h j. j ∈# mset_set UNIV#} - {# Ad $h i #}" unfolding 5 diag_mat_hma_def diag_def by simp also have "... = {#Ad $h j. j ∈# mset_set UNIV - mset_set {i}#}" by (subst image_mset_Diff) auto also have "... = {#Ad $h j. j ∈# mset_set (UNIV - {i})#}" by (intro arg_cong2[where f="image_mset"] mset_set_Diff[symmetric]) auto finally have 4:"eigenvalues A - {#1#} = {#Ad $h j. j ∈# mset_set (UNIV - {i})#}" by simp have "cmod (Ad $h k) ≤ γ⇩_{a}TYPE ('n)" if "n > 1" "k ≠ i" for k unfolding γ⇩_{a}_def 4 using that Max_ge by auto moreover have "k = i" if "n = 1" for k using that to_nat_less_n by simp ultimately have norm_Ad: "norm (Ad $h k) ≤ γ⇩_{a}TYPE ('n) ∨ k = i" for k using n_gt_0 by (cases "n = 1", auto) have "Re (Ad $h k) ≤ γ⇩_{2}TYPE ('n)" if "n > 1" "k ≠ i" for k unfolding γ⇩_{2}_def 4 using that Max_ge by auto moreover have "k = i" if "n = 1" for k using that to_nat_less_n by simp ultimately have Re_Ad: "Re (Ad $h k) ≤ γ⇩_{2}TYPE ('n) ∨ k = i" for k using n_gt_0 by (cases "n = 1", auto) show Λ⇩_{e}_ge_0: "γ⇩_{a}TYPE ('n) ≥ 0" proof (cases "n > 1") case True then obtain k where k_def: "k ≠ i" by (metis (full_types) card_n from_nat_inj n_gt_0 one_neq_zero) have "0 ≤ cmod (Ad $h k)" by simp also have "... ≤ γ⇩_{a}TYPE ('n)" using norm_Ad k_def by auto finally show ?thesis by auto next case False thus ?thesis unfolding γ⇩_{a}_def by simp qed have "∃v. cinner v 1 = 0 ∧ v ≠ 0 ∧ A *v v = β *s v" if β_ran: "β ∈# eigenvalues A - {#1#}" for β proof - obtain j where j_def: "β = Ad $h j" "j ≠ i" using β_ran unfolding 4 by auto define v where "v = U *v axis j 1" have "A *v v = A ** U *v axis j 1" unfolding v_def by (simp add:matrix_vector_mul_assoc) also have "... = ((U ** diag Ad ** adjoint_hma U) ** U) *v axis j 1" using A_sim unfolding similar_matrix_wit_def by simp also have "... = U ** diag Ad ** (adjoint_hma U ** U) *v axis j 1" by (simp add:matrix_mul_assoc) also have "... = U ** diag Ad *v axis j 1" using unitary_hmaD[OF unit_U] by simp also have "... = U *v (Ad * axis j 1)" by (simp add:matrix_vector_mul_assoc[symmetric] diag_vec_mult_eq) also have "... = U *v (β *s axis j 1)" by (intro arg_cong2[where f="(*v)"] iffD2[OF vec_eq_iff]) (auto simp:j_def axis_def) also have "... = β *s v" unfolding v_def by (simp add:vector_scalar_commute) finally have 5:"A *v v = β *s v" by simp have "cinner v 1 = cinner (axis j 1) (adjoint_hma U *v 1)" unfolding v_def adjoint_def_alter_hma by simp also have "... = cinner (axis j 1) (axis i α)" unfolding u_def[symmetric] u_alt by simp also have " ... = 0" using j_def(2) unfolding cinner_def axis_def scalar_product_def map_vector_def by (auto simp:if_distrib if_distribR sum.If_cases) finally have 6:"cinner v 1 = 0 " by simp have "cinner v v = cinner (axis j 1) (adjoint_hma U *v (U *v (axis j 1)))" unfolding v_def adjoint_def_alter_hma by simp also have "... = cinner (axis j 1) (axis j 1)" unfolding matrix_vector_mul_assoc unitary_hmaD[OF unit_U] by simp also have "... = 1" unfolding cinner_def axis_def scalar_product_def map_vector_def by (auto simp:if_distrib if_distribR sum.If_cases) finally have "cinner v v = 1" by simp hence 7:"v ≠ 0" by (cases "v=0") (auto simp add:cinner_0) show ?thesis by (intro exI[where x="v"] conjI 6 7 5) qed thus "∀α ∈# eigenvalues A - {#1#}. ∃v. cinner v 1 = 0 ∧ v ≠ 0 ∧ A *v v = α *s v" by simp have "norm (A *v v) ≤ γ⇩_{a}TYPE('n) * norm v" if "cinner v 1 = 0" for v proof - define w where "w= adjoint_hma U *v v" have "w $h i = cinner w (axis i 1)" unfolding cinner_def axis_def scalar_product_def map_vector_def by (auto simp:if_distrib if_distribR sum.If_cases) also have "... = cinner v (U *v axis i 1)" unfolding w_def adjoint_def_alter_hma by simp also have "... = cinner v ((1 / α) *s (U *v u))" unfolding vector_scalar_commute[symmetric] u_alt using α_nz by (intro_cong "[σ⇩_{2}cinner, σ⇩_{2}(*v)]") (auto simp add:axis_def vec_eq_iff) also have "... = cinner v ((1 / α) *s 1)" unfolding u_def matrix_vector_mul_assoc unitary_hmaD[OF unit_U] by simp also have "... = 0" unfolding cinner_scale_right that by simp finally have w_orth: "w $h i = 0" by simp have "norm (A *v v) = norm (U *v (diag Ad *v w))" using A_sim unfolding matrix_vector_mul_assoc similar_matrix_wit_def w_def by (simp add:matrix_mul_assoc) also have "... = norm (diag Ad *v w)" unfolding unitary_iso[OF unit_U] by simp also have "... = norm (Ad * w)" unfolding diag_vec_mult_eq by simp also have "... = sqrt (∑i∈UNIV. (cmod (Ad $h i) * cmod (w $h i))⇧^{2})" unfolding norm_vec_def L2_set_def times_vec_def by (simp add:norm_mult) also have "... ≤ sqrt (∑i∈UNIV. ((γ⇩_{a}TYPE('n)) * cmod (w $h i))^2)" using w_orth norm_Ad by (intro iffD2[OF real_sqrt_le_iff] sum_mono power_mono mult_right_mono') auto also have "... = ¦γ⇩_{a}TYPE('n)¦ * sqrt (∑i∈UNIV. (cmod (w $h i))⇧^{2})" by (simp add:power_mult_distrib sum_distrib_left[symmetric] real_sqrt_mult) also have "... = ¦γ⇩_{a}TYPE('n)¦ * norm w" unfolding norm_vec_def L2_set_def by simp also have "... = γ⇩_{a}TYPE('n) * norm w" using Λ⇩_{e}_ge_0 by simp also have "... = γ⇩_{a}TYPE('n) * norm v" unfolding w_def unitary_iso[OF unitary_hma_adjoint[OF unit_U]] by simp finally show "norm (A *v v) ≤ γ⇩_{a}TYPE('n) * norm v" by simp qed thus "∀v. cinner v 1 = 0 ⟶ norm (A *v v) ≤ γ⇩_{a}TYPE('n) * norm v" by auto have "v ∙ (A *v v) ≤ γ⇩_{2}TYPE ('n) * norm v^2" if "v ∙ 1 = 0" for v :: "real^'n" proof - define v' where "v' = map_vector complex_of_real v" define w where "w= adjoint_hma U *v v'" have "w $h i = cinner w (axis i 1)" unfolding cinner_def axis_def scalar_product_def map_vector_def by (auto simp:if_distrib if_distribR sum.If_cases) also have "... = cinner v' (U *v axis i 1)" unfolding w_def adjoint_def_alter_hma by simp also have "... = cinner v' ((1 / α) *s (U *v u))" unfolding vector_scalar_commute[symmetric] u_alt using α_nz by (intro_cong "[σ⇩_{2}cinner, σ⇩_{2}(*v)]") (auto simp add:axis_def vec_eq_iff) also have "... = cinner v' ((1 / α) *s 1)" unfolding u_def matrix_vector_mul_assoc unitary_hmaD[OF unit_U] by simp also have "... = cnj (1 / α) * cinner v' 1" unfolding cinner_scale_right by simp also have "... = cnj (1 / α) * complex_of_real (v ∙ 1)" unfolding cinner_def scalar_product_def map_vector_def inner_vec_def v'_def by (intro arg_cong2[where f="(*)"] refl) (simp) also have "... = 0" unfolding that by simp finally have w_orth: "w $h i = 0" by simp have "complex_of_real (norm v^2) = complex_of_real (v ∙ v)" by (simp add: power2_norm_eq_inner) also have "... = cinner v' v'" unfolding v'_def cinner_def scalar_product_def inner_vec_def map_vector_def by simp also have "... = norm v'^2" unfolding cinner_self by simp also have "... = norm w^2" unfolding w_def unitary_iso[OF unitary_hma_adjoint[OF unit_U]] by simp also have "... = cinner w w" unfolding cinner_self by simp also have "... = (∑j∈UNIV. complex_of_real (cmod (w $h j)^2))" unfolding cinner_def scalar_product_def map_vector_def cmod_power2 complex_mult_cnj[symmetric] by simp also have "... = complex_of_real (∑j∈UNIV. (cmod (w $h j)^2))" by simp finally have "complex_of_real (norm v^2) = complex_of_real (∑j∈UNIV. (cmod (w $h j)^2))" by simp hence norm_v: "norm v^2 = (∑j∈UNIV. (cmod (w $h j)^2))" using of_real_hom.injectivity by blast have "complex_of_real (v ∙ (A *v v)) = cinner v' (map_vector of_real (A *v v))" unfolding v'_def cinner_def scalar_product_def inner_vec_def map_vector_def by simp also have "... = cinner v' (map_matrix of_real A *v v')" unfolding v'_def of_real_hom.mult_mat_vec_hma by simp also have "... = cinner v' (A *v v')" unfolding map_matrix_def map_vector_def A_def by auto also have "... = cinner v' (U ** diag Ad ** adjoint_hma U *v v')" using A_sim unfolding similar_matrix_wit_def by simp also have "... = cinner (adjoint_hma U *v v') (diag Ad ** adjoint_hma U *v v')" unfolding adjoint_def_alter_hma adjoint_adjoint adjoint_adjoint_id by (simp add:matrix_vector_mul_assoc matrix_mul_assoc) also have "... = cinner w (diag Ad *v w)" unfolding w_def by (simp add:matrix_vector_mul_assoc) also have "... = cinner w (Ad * w)" unfolding diag_vec_mult_eq by simp also have "... = (∑j∈UNIV. cnj (Ad $h j) * cmod (w $h j)^2)" unfolding cinner_def map_vector_def scalar_product_def cmod_power2 complex_mult_cnj[symmetric] by (simp add:algebra_simps) also have "... = (∑j∈UNIV. Ad $h j * cmod (w $h j)^2)" using Ad_real by (intro sum.cong refl arg_cong2[where f="(*)"] iffD1[OF Reals_cnj_iff]) auto also have "... = (∑j∈UNIV. complex_of_real (Re (Ad $h j) * cmod (w $h j)^2))" using Ad_real by (intro sum.cong refl) simp also have "... = complex_of_real (∑j∈ UNIV. Re (Ad $h j) * cmod (w $h j)^2)" by simp finally have "complex_of_real (v∙(A *v v)) = of_real(∑j∈UNIV. Re (Ad $h j) * cmod (w $h j)^2)" by simp hence "v∙(A *v v) = (∑j∈UNIV. Re (Ad $h j) * cmod (w $h j)^2)" using of_real_hom.injectivity by blast also have "... ≤ (∑j∈UNIV. γ⇩_{2}TYPE ('n) * cmod (w $h j)^2)" using w_orth Re_Ad by (intro sum_mono mult_right_mono') auto also have "... = γ⇩_{2}TYPE ('n) * (∑j∈UNIV. cmod (w $h j)^2)" by (simp add:sum_distrib_left) also have "... = γ⇩_{2}TYPE ('n) * norm v^2" unfolding norm_v by simp finally show ?thesis by simp qed thus "∀(v::real^'n). v ∙ 1 = 0 ⟶ v ∙ (A *v v) ≤ γ⇩_{2}TYPE ('n) * norm v^2" by auto qed lemma find_any_real_ev: assumes "complex_of_real α ∈# eigenvalues A - {#1#}" shows "∃v. v ∙ 1 = 0 ∧ v ≠ 0 ∧ A *v v = α *s v" proof - obtain w where w_def: "cinner w 1 = 0" "w ≠ 0" "A *v w = α *s w" using find_any_ev assms by auto have "w = 0" if "map_vector Re (1 *s w) = 0" "map_vector Re (𝗂 *s w) = 0" using that by (simp add:vec_eq_iff map_vector_def complex_eq_iff) then obtain c where c_def: "map_vector Re (c *s w) ≠ 0" using w_def(2) by blast define u where "u = c *s w" define v where "v = map_vector Re u" hence "v ∙ 1 = Re (cinner u 1)" unfolding cinner_def inner_vec_def scalar_product_def map_vector_def by simp also have "... = 0" unfolding u_def cinner_scale_left w_def(1) by simp finally have 1:"v ∙ 1 = 0" by simp have "A *v v = (χ i. ∑j∈UNIV. A $h i $h j * Re (u $h j))" unfolding matrix_vector_mult_def v_def map_vector_def by simp also have "... = (χ i. ∑j∈UNIV. Re ( of_real (A $h i $h j) * u $h j))" by simp also have "... = (χ i. Re (∑j∈UNIV. A $h i $h j * u $h j))" unfolding A_def by simp also have "... = map_vector Re (A *v u)" unfolding map_vector_def matrix_vector_mult_def by simp also have "... = map_vector Re (of_real α *s u)" unfolding u_def vector_scalar_commute w_def(3) by (simp add:ac_simps) also have "... = α *s v" unfolding v_def by (simp add:vec_eq_iff map_vector_def) finally have 2: "A *v v = α *s v" by simp have 3:"v ≠ 0" unfolding v_def u_def using c_def by simp show ?thesis by (intro exI[where x="v"] conjI 1 2 3) qed lemma size_evs: "size (eigenvalues A - {#1::complex#}) = n-1" proof - have "size (eigenvalues A :: complex multiset) = n" using eigvals_poly_length card_n[symmetric] by auto thus "size (eigenvalues A - {#(1::complex)#}) = n -1" using ev_1 by (simp add: size_Diff_singleton) qed lemma find_γ⇩_{2}: assumes "n > 1" shows "γ⇩_{a}TYPE('n) ∈# image_mset cmod (eigenvalues A - {#1::complex#})" proof - have "set_mset (eigenvalues A - {#(1::complex)#}) ≠ {}" using assms size_evs by auto hence 2: "cmod ` set_mset (eigenvalues A - {#1#}) ≠ {}" by simp have "γ⇩_{a}TYPE('n) ∈ set_mset (image_mset cmod (eigenvalues A - {#1#}))" unfolding γ⇩_{a}_def using assms 2 Max_in by auto thus "γ⇩_{a}TYPE('n) ∈# image_mset cmod (eigenvalues A - {#1#})" by simp qed lemma γ⇩_{2}_real_ev: assumes "n > 1" shows "∃v. (∃α. abs α=γ⇩_{a}TYPE('n) ∧ v ∙ 1=0 ∧ v ≠ 0 ∧ A *v v = α *s v)" proof - obtain α where α_def: "cmod α = γ⇩_{a}TYPE('n)" "α ∈# eigenvalues A - {#1#}" using find_γ⇩_{2}[OF assms] by auto have "α ∈ ℝ" using in_diffD[OF α_def(2)] evs_real by auto then obtain β where β_def: "α = of_real β" using Reals_cases by auto have 0:"complex_of_real β ∈# eigenvalues A-{#1#}" using α_def unfolding β_def by auto have 1: "¦β¦ = γ⇩_{a}TYPE('n)" using α_def unfolding β_def by simp show ?thesis using find_any_real_ev[OF 0] 1 by auto qed lemma γ⇩_{a}_real_bound: fixes v :: "real^'n" assumes "v ∙ 1 = 0" shows "norm (A *v v) ≤ γ⇩_{a}TYPE('n) * norm v" proof - define w where "w = map_vector complex_of_real v" have "cinner w 1 = v ∙ 1" unfolding w_def cinner_def map_vector_def scalar_product_def inner_vec_def by simp also have "... = 0" using assms by simp finally have 0: "cinner w 1 = 0" by simp have "norm (A *v v) = norm (map_matrix complex_of_real A *v (map_vector complex_of_real v))" unfolding norm_of_real of_real_hom.mult_mat_vec_hma[symmetric] by simp also have "... = norm (A *v w)" unfolding w_def A_def map_matrix_def map_vector_def by simp also have "... ≤ γ⇩_{a}TYPE('n) * norm w" using γ⇩_{a}_bound 0 by auto also have "... = γ⇩_{a}TYPE('n) * norm v" unfolding w_def norm_of_real by simp finally show ?thesis by simp qed lemma Λ⇩_{e}_eq_Λ: "Λ⇩_{a}= γ⇩_{a}TYPE('n)" proof - have "¦g_inner f (g_step f)¦ ≤ γ⇩_{a}TYPE('n) * (g_norm f)⇧^{2}" (is "?L ≤ ?R") if "g_inner f (λ_. 1) = 0" for f proof - define v where "v = (χ i. f (enum_verts i))" have 0: " v ∙ 1 = 0" using that unfolding g_inner_conv one_vec_def v_def by auto have "?L = ¦v ∙ (A *v v)¦" unfolding g_inner_conv g_step_conv v_def by simp also have "... ≤ (norm v * norm (A *v v))" by (intro Cauchy_Schwarz_ineq2) also have "... ≤ (norm v * (γ⇩_{a}TYPE('n) * norm v))" by (intro mult_left_mono γ⇩_{a}_real_bound 0) auto also have "... = ?R" unfolding g_norm_conv v_def by (simp add:algebra_simps power2_eq_square) finally show ?thesis by simp qed hence "Λ⇩_{a}≤ γ⇩_{a}TYPE('n)" using γ⇩_{a}_ge_0 by (intro expander_intro_1) auto moreover have "Λ⇩_{a}≥ γ⇩_{a}TYPE('n)" proof (cases "n > 1") case True then obtain v α where v_def: "abs α = γ⇩_{a}TYPE('n)" "A *v v =α *s v" "v ≠ 0" "v ∙ 1 = 0" using γ⇩_{2}_real_ev by auto define f where "f x = v $h enum_verts_inv x" for x have v_alt: "v = (χ i. f (enum_verts i))" unfolding f_def Rep_inverse by simp have "g_inner f (λ_. 1) = v ∙ 1" unfolding g_inner_conv v_alt one_vec_def by simp also have "... = 0" using v_def by simp finally have 2:"g_inner f (λ_. 1) = 0" by simp have "γ⇩_{a}TYPE('n) * g_norm f^2 = γ⇩_{a}TYPE('n) * norm v^2" unfolding g_norm_conv v_alt by simp also have "... = γ⇩_{a}TYPE('n) * ¦v ∙ v¦" by (simp add: power2_norm_eq_inner) also have "... = ¦v ∙ (α *s v)¦