Theory Expander_Graphs.Expander_Graphs_Eigenvalues
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)¦"
unfolding v_def(1)[symmetric] scalar_mult_eq_scaleR
by (simp add:abs_mult)
also have "... = ¦v ∙ (A *v v)¦"
unfolding v_def by simp
also have "... = ¦g_inner f (g_step f)¦"
unfolding g_inner_conv g_step_conv v_alt by simp
also have "... ≤ Λ⇩a * g_norm f^2"
by (intro expansionD1 2)
finally have "γ⇩a TYPE('n) * g_norm f^2 ≤ Λ⇩a * g_norm f^2" by simp
moreover have "norm v^2 > 0"
using v_def(3) by simp
hence "g_norm f^2 > 0"
unfolding g_norm_conv v_alt by simp
ultimately show ?thesis by simp
next
case False
hence "n = 1" using n_gt_0 by simp
hence "γ⇩a TYPE('n) = 0"
unfolding γ⇩a_def by simp
then show ?thesis using Λ_ge_0 by simp
qed
ultimately show ?thesis by simp
qed
lemma γ⇩2_ev:
assumes "n > 1"
shows "∃v. v ∙ 1 = 0 ∧ v ≠ 0 ∧ A *v v = γ⇩2 TYPE('n) *s v"
proof -
have "set_mset (eigenvalues A - {#1::complex#}) ≠ {}"
using size_evs assms by auto
hence "Max (Re ` set_mset (eigenvalues A - {#1#})) ∈ Re ` set_mset (eigenvalues A - {#1#})"
by (intro Max_in) auto
hence "γ⇩2 TYPE ('n) ∈ Re ` set_mset (eigenvalues A - {#1#})"
unfolding γ⇩2_def using assms by simp
then obtain α where α_def: "α ∈ set_mset (eigenvalues A - {#1#})" "γ⇩2 TYPE ('n) = Re α"
by auto
have α_real: "α ∈ ℝ"
using evs_real in_diffD[OF α_def(1)] by auto
have "complex_of_real (γ⇩2 TYPE ('n)) = of_real (Re α)"
unfolding α_def by simp
also have "... = α"
using α_real by simp
also have "... ∈# eigenvalues A - {#1#}"
using α_def(1) by simp
finally have 0:"complex_of_real (γ⇩2 TYPE ('n)) ∈# eigenvalues A - {#1#}" by simp
thus ?thesis
using find_any_real_ev[OF 0] by auto
qed
lemma Λ⇩2_eq_γ⇩2: "Λ⇩2 = γ⇩2 TYPE ('n)"
proof (cases "n > 1")
case True
obtain v where v_def: "v ∙ 1 = 0" "v ≠ 0" "A *v v = γ⇩2 TYPE('n) *s v"
using γ⇩2_ev[OF True] 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" unfolding v_def(1) by simp
finally have f_orth: "g_inner f (λ_. 1) = 0" by simp
have "γ⇩2 TYPE('n) * norm v^2= v ∙ (γ⇩2 TYPE('n) *s v)"
unfolding power2_norm_eq_inner by (simp add:algebra_simps scalar_mult_eq_scaleR)
also have "... = v ∙ (A *v v)"
unfolding v_def by simp
also have "... = g_inner f (g_step f)"
unfolding v_alt g_inner_conv g_step_conv by simp
also have "... ≤ Λ⇩2 * g_norm f^2"
by (intro os_expanderD f_orth)
also have "... = Λ⇩2 * norm v^2"
unfolding v_alt g_norm_conv by simp
finally have "γ⇩2 TYPE('n) * norm v^2 ≤ Λ⇩2 * norm v^2" by simp
hence "γ⇩2 TYPE('n) ≤ Λ⇩2"
using v_def(2) by simp
moreover have "Λ⇩2 ≤ γ⇩2 TYPE ('n)"
using γ⇩2_bound
by (intro os_expanderI[OF True])
(simp add: g_inner_conv g_step_conv g_norm_conv one_vec_def)
ultimately show ?thesis by simp
next
case False
then show ?thesis
unfolding Λ⇩2_def γ⇩2_def by simp
qed
lemma expansionD2:
assumes "g_inner f (λ_. 1) = 0"
shows "g_norm (g_step f) ≤ Λ⇩a * g_norm f" (is "?L ≤ ?R")
proof -
define v where "v = (χ i. f (enum_verts i))"
have "v ∙ 1 = g_inner f (λ_. 1)"
unfolding g_inner_conv v_def one_vec_def by simp
also have "... = 0" using assms by simp
finally have 0:"v ∙ 1 = 0" by simp
have "g_norm (g_step f) = norm (A *v v)"
unfolding g_norm_conv g_step_conv v_def by auto
also have "... ≤ Λ⇩a * norm v"
unfolding Λ⇩e_eq_Λ by (intro γ⇩a_real_bound 0)
also have "... = Λ⇩a * g_norm f"
unfolding g_norm_conv v_def by simp
finally show ?thesis by simp
qed
lemma rayleigh_bound:
fixes v :: "real^'n"
shows "¦v ∙ (A *v v)¦ ≤ norm v^2"
proof -
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 "¦v ∙ (A *v v)¦ = ¦g_inner f (g_step f)¦"
unfolding v_alt g_inner_conv g_step_conv by simp
also have "... = ¦(∑a∈arcs G. f (head G a) * f (tail G a))¦/d"
unfolding g_inner_step_eq by simp
also have "... ≤ (d * (g_norm f)⇧2) / d"
by (intro divide_right_mono bdd_above_aux) auto
also have "... = g_norm f^2"
using d_gt_0 by simp
also have "... = norm v^2"
unfolding g_norm_conv v_alt by simp
finally show ?thesis by simp
qed
text ‹The following implies that two-sided expanders are also one-sided expanders.›
lemma Λ⇩2_range: "¦Λ⇩2¦ ≤ Λ⇩a"
proof (cases "n > 1")
case True
hence 0:"set_mset (eigenvalues A - {#1::complex#}) ≠ {}"
using size_evs by auto
have "γ⇩2 TYPE ('n) = Max (Re ` set_mset (eigenvalues A - {#1::complex#}))"
unfolding γ⇩2_def using True by simp
also have "... ∈ Re ` set_mset (eigenvalues A - {#1::complex#})"
using Max_in 0 by simp
finally have "γ⇩2 TYPE ('n) ∈ Re ` set_mset (eigenvalues A - {#1::complex#})"
by simp
then obtain α where α_def: "α ∈ set_mset (eigenvalues A - {#1::complex#})" "γ⇩2 TYPE ('n) = Re α"
by auto
have "¦Λ⇩2¦ = ¦γ⇩2 TYPE ('n) ¦"
using Λ⇩2_eq_γ⇩2 by simp
also have "... = ¦Re α¦"
using α_def by simp
also have "... ≤ cmod α"
using abs_Re_le_cmod by simp
also have "... ≤ Max (cmod ` set_mset (eigenvalues A - {#1#}))"
using α_def(1) by (intro Max_ge) auto
also have "... ≤ γ⇩a TYPE('n)"
unfolding γ⇩a_def using True by simp
also have "... = Λ⇩a"
using Λ⇩e_eq_Λ by simp
finally show ?thesis by simp
next
case False
thus ?thesis
unfolding Λ⇩2_def Λ⇩a_def by simp
qed
end
lemmas (in regular_graph) expansionD2 =
regular_graph_tts.expansionD2[OF eg_tts_1,
internalize_sort "'n :: finite", OF _ regular_graph_axioms,
unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty]
lemmas (in regular_graph) Λ⇩2_range =
regular_graph_tts.Λ⇩2_range[OF eg_tts_1,
internalize_sort "'n :: finite", OF _ regular_graph_axioms,
unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty]
unbundle no_intro_cong_syntax
end