Theory Cauchy_Eigenvalue_Interlacing
theory Cauchy_Eigenvalue_Interlacing
imports Misc_Matrix_Results
begin
section "Rayleigh Quotient Lemmas"
definition rayleigh_quotient_complex ("ρ⇩c") where
"ρ⇩c M x = (QF M x) / (x ∙c x)"
definition rayleigh_quotient ("ρ") where
"ρ M x = Re (ρ⇩c M x)"
declare
rayleigh_quotient_complex_def[simp]
rayleigh_quotient_def[simp]
lemma rayleigh_quotient_negative: "A ∈ carrier_mat n n ⟹ x ∈ carrier_vec n ⟹ ρ A x = - ρ (- A) x"
by auto
lemma rayleigh_quotient_complex_scale:
fixes k :: real
assumes "A ∈ carrier_mat n n"
assumes "v ∈ carrier_vec n"
assumes "k ≠ 0"
shows "ρ⇩c A v = ρ⇩c A (k ⋅⇩v v)"
proof-
have "ρ⇩c A v = (k^2 * ((A *⇩v v) ∙c v)) / (k^2 * (v ∙c v))" using assms(3) by simp
also have "... = (((k ⋅⇩v (A *⇩v v)) ∙c (k ⋅⇩v v))) / (k^2 * (v ∙c v))"
by (smt (verit, ccfv_SIG) assms(1) assms(2) more_arith_simps(11) mult_mat_vec_carrier power2_eq_square scalar_prod_smult_distrib smult_carrier_vec smult_scalar_prod_distrib vec_conjugate_real)
also have "... = (((k ⋅⇩v (A *⇩v v)) ∙c (k ⋅⇩v v))) / (((k ⋅⇩v v) ∙c (k ⋅⇩v v)))"
by (simp add: power2_eq_square)
also have "... = ((((A *⇩v (k ⋅⇩v v))) ∙c (k ⋅⇩v v))) / (((k ⋅⇩v v) ∙c (k ⋅⇩v v)))"
by (metis assms(1) assms(2) mult_mat_vec)
also have "... = ρ⇩c A (k ⋅⇩v v)" by auto
finally show ?thesis .
qed
lemma rayleigh_quotient_scale:
fixes k :: real
assumes "A ∈ carrier_mat n n"
assumes "v ∈ carrier_vec n"
assumes "k ≠ 0"
shows "ρ A v = ρ A (k ⋅⇩v v)"
by (smt (verit, ccfv_SIG) rayleigh_quotient_complex_scale assms Groups.mult_ac(2) complex_norm_square conjugate_complex_def inner_prod_smult_left_right mult_divide_mult_cancel_left_if mult_mat_vec mult_mat_vec_carrier norm_of_real of_real_eq_0_iff power_eq_0_iff quadratic_form_def rayleigh_quotient_complex_def rayleigh_quotient_def)
lemma hermitian_rayleigh_quotient_real:
fixes A :: "complex mat"
assumes "A ∈ carrier_mat n n"
assumes "v ∈ carrier_vec n"
assumes "hermitian A"
assumes "v ≠ 0⇩v n"
shows "ρ⇩c A v ∈ Reals"
proof-
have "QF A v ∈ Reals"
using hermitian_quadratic_form_real assms by blast
moreover have "inner_prod v v ∈ Reals" by (simp add: self_inner_prod_real)
moreover have "inner_prod v v ≠ 0" using assms(2,4) by fastforce
ultimately show ?thesis unfolding rayleigh_quotient_complex_def using Reals_divide by blast
qed
section "Vector Summation Lemmas"
lemma complex_vec_norm_sum:
fixes x :: "complex vec"
assumes "x ∈ carrier_vec n"
shows "vec_norm x = csqrt ((∑i ∈ {..<n}. (cmod (x$i))^2))"
proof-
have *: "⋀i. i ∈ {..<n} ⟹ (conjugate x)$i = conjugate (x$i)"
using assms by auto
have **: "⋀i. i ∈ {..<n} ⟹ (x$i) * conjugate (x$i) = (cmod (x$i))^2"
using mult_conj_cmod_square by blast
have "vec_norm x = csqrt (x ∙c x)"
by (simp add: vec_norm_def)
also have "... = csqrt (∑i ∈ {..<n}. (x$i) * (conjugate x)$i)"
by (metis assms atLeast0LessThan carrier_vecD dim_vec_conjugate scalar_prod_def)
also have "... = csqrt (∑i ∈ {..<n}. (x$i) * conjugate (x$i))"
by (simp add: *)
also have "... = csqrt ((∑i ∈ {..<n}. (cmod (x$i))^2))" using ** by fastforce
finally show ?thesis .
qed
lemma inner_prod_vec_sum:
assumes "v ∈ carrier_vec n"
assumes "w ∈ carrier_vec n"
assumes "B ⊆ carrier_vec n"
assumes "finite B"
assumes "v = finsum_vec TYPE('a::conjugatable_ring) n (λb. cs b ⋅⇩v b) B"
shows "inner_prod w v = (∑b ∈ B. cs b * inner_prod w b)"
proof-
let ?vs = "λb. cs b ⋅⇩v b"
let ?f = "λi b. if i ∈ {..<n} then (?vs b)$i * (conjugate w)$i else 0"
have f: "⋀y. finite {x. ?f x y ≠ 0}"
proof-
fix y
have "{x. ?f x y ≠ 0} ⊆ {..<n}" by (simp add: subset_eq)
thus "finite {x. ?f x y ≠ 0}" using finite_nat_iff_bounded by blast
qed
have vs: "?vs ∈ B → carrier_vec n" using assms(3) by force
have b_scale: "⋀i b. i ∈ {..<n} ⟹ b ∈ B ⟹ (?vs b)$i = cs b * b$i"
using assms(3) by auto
have assoc: "⋀i b. (cs b * b$i) * (conjugate w)$i = cs b * (b$i * (conjugate w)$i)"
using Groups.mult_ac(1) by blast
have "inner_prod w v = (∑i ∈ {..<n}. v$i * (conjugate w)$i)"
unfolding scalar_prod_def using atLeast0LessThan assms(2) by force
moreover have "⋀i. i ∈ {..<n} ⟹ v$i = (∑b ∈ B. (?vs b)$i)"
using index_finsum_vec[OF assms(4) _ vs] unfolding assms(5) by blast
ultimately have "inner_prod w v = (∑i ∈ {..<n}. (∑b ∈ B. (?vs b)$i) * (conjugate w)$i)"
by force
also have "... = (∑i ∈ {..<n}. ∑b ∈ B. (?vs b)$i * (conjugate w)$i)"
by (simp add: sum_distrib_right)
also have "... = (∑i ∈ {..<n}. ∑b ∈ B. ?f i b)"
by fastforce
also have "... = Sum_any (λi. ∑b ∈ B. ?f i b)"
using Sum_any.conditionalize[of "{..<n}" "λi. (∑b ∈ B. ?f i b)"]
by (smt (verit, ccfv_SIG) Sum_any.cong finite_nat_iff_bounded subset_eq sum.neutral)
also have "... = (∑b ∈ B. (Sum_any (λi. ?f i b)))"
using Sum_any_sum_swap[OF assms(4) f, of "λx. x"] .
also have "... = (∑b ∈ B. (∑i ∈ {..<n}. (?vs b)$i * (conjugate w)$i))"
proof-
have "⋀b. b ∈ B ⟹ (∑i ∈ {..<n}. (?vs b)$i * (conjugate w)$i) = Sum_any (λi. ?f i b)"
using Sum_any.conditionalize[of "{..<n}"] by blast
thus ?thesis by fastforce
qed
also have "... = (∑b ∈ B. (∑i ∈ {..<n}. (cs b * b$i) * (conjugate w)$i))"
using b_scale by simp
also have "... = (∑b ∈ B. (∑i ∈ {..<n}. cs b * (b$i * (conjugate w)$i)))"
using assoc by force
also have "... = (∑b ∈ B. cs b * (∑i ∈ {..<n}. b$i * (conjugate w)$i))"
by (simp add: sum_distrib_left)
also have "... = (∑b ∈ B. cs b * inner_prod w b)"
unfolding scalar_prod_def using atLeast0LessThan assms(2) by force
finally show ?thesis .
qed
lemma sprod_vec_sum:
assumes "v ∈ carrier_vec n"
assumes "w ∈ carrier_vec n"
assumes "B ⊆ carrier_vec n"
assumes "finite B"
assumes "v = finsum_vec TYPE('a::{comm_ring}) n (λb. cs b ⋅⇩v b) B"
shows "w ∙ v = (∑b ∈ B. cs b * (w ∙ b))"
proof-
let ?vs = "λb. cs b ⋅⇩v b"
let ?f = "λi b. if i ∈ {..<n} then (?vs b)$i * w$i else 0"
have f: "⋀y. finite {x. ?f x y ≠ 0}"
proof-
fix y
have "{x. ?f x y ≠ 0} ⊆ {..<n}" by (simp add: subset_eq)
thus "finite {x. ?f x y ≠ 0}" using finite_nat_iff_bounded by blast
qed
have vs: "?vs ∈ B → carrier_vec n" using assms(3) by force
have b_scale: "⋀i b. i ∈ {..<n} ⟹ b ∈ B ⟹ (?vs b)$i = cs b * b$i"
using assms(3) by auto
have assoc: "⋀i b. (cs b * b$i) * w$i = cs b * (b$i * w$i)"
using Groups.mult_ac(1) by blast
have B_dim: "⋀b. b ∈ B ⟹ dim_vec b = n"
using assms(3) by fastforce
have "w ∙ v = (∑i ∈ {..<n}. v$i * w$i)"
unfolding scalar_prod_def using atLeast0LessThan[of n] assms(1)
by (metis (no_types, lifting) Groups.mult_ac(2) carrier_vecD sum.cong)
moreover have "⋀i. i ∈ {..<n} ⟹ v$i = (∑b ∈ B. (?vs b)$i)"
using index_finsum_vec[OF assms(4) _ vs] unfolding assms(5) by blast
ultimately have "w ∙ v = (∑i ∈ {..<n}. (∑b ∈ B. (?vs b)$i) * w$i)"
by force
also have "... = (∑i ∈ {..<n}. ∑b ∈ B. (?vs b)$i * w$i)"
by (simp add: sum_distrib_right)
also have "... = (∑i ∈ {..<n}. ∑b ∈ B. ?f i b)"
by fastforce
also have "... = Sum_any (λi. ∑b ∈ B. ?f i b)"
using Sum_any.conditionalize[of "{..<n}" "λi. (∑b ∈ B. ?f i b)"]
by (smt (verit, ccfv_SIG) Sum_any.cong finite_nat_iff_bounded subset_eq sum.neutral)
also have "... = (∑b ∈ B. (Sum_any (λi. ?f i b)))"
using Sum_any_sum_swap[OF assms(4) f, of "λx. x"] .
also have "... = (∑b ∈ B. (∑i ∈ {..<n}. (?vs b)$i * w$i))"
proof-
have "⋀b. b ∈ B ⟹ (∑i ∈ {..<n}. (?vs b)$i * w$i) = Sum_any (λi. ?f i b)"
using Sum_any.conditionalize[of "{..<n}"] by blast
thus ?thesis by fastforce
qed
also have "... = (∑b ∈ B. (∑i ∈ {..<n}. (cs b * b$i) * w$i))"
using b_scale by simp
also have "... = (∑b ∈ B. (∑i ∈ {..<n}. cs b * (b$i * w$i)))"
using assoc by force
also have "... = (∑b ∈ B. cs b * (∑i ∈ {..<n}. b$i * w$i))"
by (simp add: sum_distrib_left)
also have "... = (∑b ∈ B. cs b * (∑i ∈ {..<n}. w$i * b$i))"
by (metis (no_types, lifting) Groups.mult_ac(2) sum.cong)
also have "... = (∑b ∈ B. cs b * (w ∙ b))"
unfolding scalar_prod_def using atLeast0LessThan assms(3) B_dim by fastforce
finally show ?thesis .
qed
lemma mat_vec_mult_sum:
assumes "v ∈ carrier_vec n"
assumes "A ∈ carrier_mat n n"
assumes "B ⊆ carrier_vec n"
assumes "finite B"
assumes "v = finsum_vec TYPE('a::comm_ring) n (λb. cs b ⋅⇩v b) B"
shows "A *⇩v v = finsum_vec TYPE('a::comm_ring) n (λb. cs b ⋅⇩v (A *⇩v b)) B"
(is "?lhs = ?rhs")
proof-
have "⋀i. i < n ⟹ ?lhs$i = ?rhs$i"
proof-
fix i assume *: "i < n"
let ?r = "row A i"
have "?lhs$i = ?r ∙ v" using * assms(2) unfolding mult_mat_vec_def by simp
also have "... = (∑b ∈ B. (cs b * (?r ∙ b)))"
using sprod_vec_sum[OF assms(1) _ assms(3) assms(4) assms(5)] assms(2) by fastforce
also have "... = (∑b ∈ B. (cs b * ((A *⇩v b)$i)))"
using * assms(2) unfolding mult_mat_vec_def by simp
also have "... = (∑b ∈ B. ((cs b ⋅⇩v (A *⇩v b))$i))"
using assms(2) * by force
also have "... = (finsum_vec TYPE('a::comm_ring) n (λb. cs b ⋅⇩v (A *⇩v b)) B)$i"
using index_finsum_vec[OF assms(4) *]
by (smt (verit, best) Pi_I assms(2) carrier_matD(1) carrier_vec_dim_vec dim_mult_mat_vec index_smult_vec(2) sum.cong)
finally show "?lhs$i = ?rhs$i" by blast
qed
moreover have "?lhs ∈ carrier_vec n" using assms(1) assms(2) by force
moreover have "?rhs ∈ carrier_vec n"
by (smt (verit, ccfv_SIG) Pi_iff assms(2) assms(3) finsum_vec_closed mult_mat_vec_carrier smult_carrier_vec subsetD)
ultimately show ?thesis by (metis (no_types, lifting) carrier_vecD eq_vecI)
qed
section "Module Span Lemmas"
context module
begin
lemma mk_coeffs_of_list:
assumes "α ∈ (set A → carrier R)"
shows "∃c ∈ {0..<length A} → carrier R. ∀v ∈ set A. mk_coeff A c v = α v"
using assms
proof(induct "length A" arbitrary: A)
case 0
thus ?case by fastforce
next
case (Suc n)
then obtain a A' where a: "A = A' @ [a]" by (metis length_Suc_conv_rev)
hence "α ∈ (set A' → carrier R)" using Suc.prems by simp
moreover from a have len_A': "n = length A'" using Suc(2) by auto
ultimately obtain c' where c':
"c' ∈ {0..<length A'} → carrier R ∧ (∀v ∈ set A'. mk_coeff A' c' v = α v)"
using Suc.hyps by blast
have len_A'_A: "length A' = length A - 1" using Suc(2) len_A' by presburger
moreover have "[0..<length A] = [0..<length A - 1] @ [length A - 1]"
by (metis Suc(2) calculation len_A' upt_Suc_append zero_order(1))
ultimately have A_A'_int: "[0..<length A] = [0..<length A'] @ [length A']" by presburger
show ?case
proof(cases "a ∈ set A'")
case True
hence A_A': "set A = set A'" using a by auto
define c where "c ≡ (λi. if i ∈ {0..<length A'} then c' i else 𝟬)"
hence c_carrier: "c ∈ {0..<length A} → carrier R" using c' by force
moreover have "∀v ∈ set A. mk_coeff A c v = α v"
proof
fix v assume *: "v ∈ set A"
show "mk_coeff A c v = α v"
proof(cases "v = a")
case True
hence "find_indices v A = (find_indices v A') @ [length A - 1]"
proof-
from A_A'_int have "find_indices v A
= (filter (λi. A ! i = v) [0..<length A']) @ (filter (λi. A ! i = v) [length A'])"
unfolding find_indices_def by (metis Suc.hyps(2) filter_append len_A')
moreover then have "(filter (λi. A ! i = v) [0..<length A']) = (find_indices v A')"
using a by auto
moreover have "filter (λi. A ! i = v) [length A'] = [length A']" by (simp add: True a)
ultimately show ?thesis using len_A'_A by argo
qed
hence "map c (find_indices v A) = (map c (find_indices v A')) @ [c (length A - 1)]"
by auto
hence "foldr (⊕) (map c (find_indices v A)) 𝟬
= foldr (⊕) (map c (find_indices v A')) (𝟬 ⊕ c (length A - 1))"
by (simp add: c_def len_A'_A)
also have "... = (foldr (⊕) (map c (find_indices v A')) 𝟬) ⊕ c (length A - 1)"
by (metis R.sumlist_def R.zero_closed c_carrier atLeastLessThan_iff c_def calculation cring_simprules(16) len_A'_A less_irrefl_nat mk_coeff_carrier mk_coeff_def)
finally have "mk_coeff A c v = mk_coeff A' c v ⊕ c (length A - 1)"
unfolding mk_coeff_def R.sumlist_def .
moreover have "c (length A - 1) = 𝟬" unfolding c_def using len_A' a by force
moreover have "mk_coeff A' c v ∈ carrier R"
by (smt (verit) Pi_iff c' c_def mk_coeff_carrier)
ultimately have "mk_coeff A c v = mk_coeff A' c v" by algebra
moreover have "mk_coeff A' c v = mk_coeff A' c' v"
unfolding mk_coeff_def find_indices_def
by (metis (mono_tags, lifting) c_def list.map_cong mem_Collect_eq set_filter set_upt)
ultimately show ?thesis by (metis "*" A_A' c')
next
case v_neq_a: False
hence "find_indices v A = find_indices v A'"
proof-
from A_A'_int have "find_indices v A
= (filter (λi. A ! i = v) [0..<length A']) @ (filter (λi. A ! i = v) [length A'])"
unfolding find_indices_def by (metis Suc.hyps(2) filter_append len_A')
moreover have "(filter (λi. A ! i = v) [0..<length A']) = find_indices v A'"
unfolding find_indices_def
by (smt (verit, ccfv_SIG) a append.right_neutral calculation filter.simps(1) filter.simps(2) filter_cong find_indices_def find_indices_snoc nth_append_length v_neq_a)
moreover have "(filter (λi. A ! i = v) [length A']) = []" using a v_neq_a by auto
ultimately show ?thesis by force
qed
hence "mk_coeff A c v = mk_coeff A' c v" unfolding mk_coeff_def by fastforce
also have "... = mk_coeff A' c' v"
unfolding mk_coeff_def find_indices_def c_def
by (smt (verit, best) atLeastLessThan_upt list.map_cong mem_Collect_eq set_filter)
also have "... = α v" using c' * A_A' by blast
finally show ?thesis .
qed
qed
ultimately show ?thesis by blast
next
case False
hence A_A': "set A' = set A - {a}" by (simp add: a)
define c where "c ≡ (λi. if i ∈ {0..<length A'} then c' i else α a)"
hence "c ∈ {0..<length A} → carrier R" using Suc.prems a c' by fastforce
moreover have "∀v ∈ set A. mk_coeff A c v = α v"
proof
fix v assume *: "v ∈ set A"
show "mk_coeff A c v = α v"
proof(cases "v = a")
case v_eq_a: True
hence "filter (λi. A ! i = v) [0..<length A] = [length A - 1]"
proof-
from A_A'_int have "filter (λi. A ! i = v) [0..<length A]
= (filter (λi. A ! i = v) [0..<length A']) @ (filter (λi. A ! i = v) [length A'])"
by (metis Suc.hyps(2) filter_append len_A')
moreover have "(filter (λi. A ! i = v) [0..<length A']) = []"
proof-
have "⋀i. i < length A' ⟹ A!i ≠ v" by (metis False a nth_append nth_mem v_eq_a)
thus ?thesis by fastforce
qed
moreover have "(filter (λi. A ! i = v) [length A']) = [length A']" by (simp add: a v_eq_a)
ultimately show ?thesis by (metis Suc.hyps(2) diff_Suc_1 len_A' self_append_conv2)
qed
hence "map c (filter (λi. A ! i = v) [0..<length A]) = [c (length A')]"
by (metis len_A' Suc.hyps(2) diff_Suc_1 list.map(1) list.map(2))
moreover have "c (length A') = α v" by (simp add: v_eq_a c_def)
ultimately have "mk_coeff A c v = α v ⊕ 𝟬" unfolding mk_coeff_def find_indices_def by force
moreover have "α v ∈ carrier R" using "*" Suc(3) by blast
ultimately show ?thesis by auto
next
case v_neq_a: False
hence "find_indices v A = find_indices v A'"
proof-
from A_A'_int have "find_indices v A
= (filter (λi. A ! i = v) [0..<length A']) @ (filter (λi. A ! i = v) [length A'])"
unfolding find_indices_def by (metis Suc.hyps(2) filter_append len_A')
moreover have "(filter (λi. A ! i = v) [0..<length A']) = find_indices v A'"
unfolding find_indices_def
by (smt (verit, ccfv_SIG) a append.right_neutral calculation filter.simps(1) filter.simps(2) filter_cong find_indices_def find_indices_snoc nth_append_length v_neq_a)
moreover have "(filter (λi. A ! i = v) [length A']) = []" using a v_neq_a by auto
ultimately show ?thesis by force
qed
hence "mk_coeff A c v = mk_coeff A' c v" unfolding mk_coeff_def by fastforce
also have "... = mk_coeff A' c' v"
unfolding mk_coeff_def find_indices_def c_def
by (smt (verit, best) atLeastLessThan_upt list.map_cong mem_Collect_eq set_filter)
also have "... = α v" by (metis c' * a insert_iff v_neq_a vec_space.append_insert)
finally show ?thesis .
qed
qed
ultimately show ?thesis by blast
qed
qed
lemma span_list_span:
assumes "set A ⊆ carrier M"
shows "span_list A = span (set A)"
proof-
have "span_list A ⊆ span (set A)"
proof(rule subsetI)
fix x assume "x ∈ span_list A"
then obtain c where c: "x = lincomb_list c A ∧ c ∈ {0..<length A} → carrier R"
unfolding span_list_def by blast
hence 1: "lincomb_list c A = lincomb (mk_coeff A c) (set A)"
using lincomb_list_as_lincomb[OF assms(1)] by presburger
have "mk_coeff A c ∈ (set A) → carrier R" by (simp add: c mk_coeff_carrier)
hence 2: "lincomb (mk_coeff A c) (set A) ∈ span (set A)" unfolding span_def by blast
show "x ∈ span (set A)" using 1 2 c by argo
qed
moreover have "span (set A) ⊆ span_list A"
proof(rule subsetI)
fix x assume *: "x ∈ span (set A)"
then obtain α where α: "x = lincomb α (set A) ∧ α ∈ (set A → carrier R)"
using * finite_span assms by auto
define α' where "α' = (λv. if v ∈ set A then α v else 𝟬)"
hence α_α': "⋀v. v ∈ set A ⟹ α v = α' v" by presburger
hence x_α': "x = lincomb α' (set A)"
using α
unfolding lincomb_def
by (smt (verit) M.add.finprod_cong' Pi_iff assms basic_trans_rules(31) carrier_is_submodule submoduleE(4))
have 1: "α' ∈ (set A → carrier R)" by (simp add: Pi_cong α α'_def)
then obtain c where c: "c ∈ {0..<length A} → carrier R ∧ (∀v ∈ set A. mk_coeff A c v = α' v)"
using mk_coeffs_of_list by blast
have "mk_coeff A c = α'" unfolding α'_def by (metis mk_coeff_0 c α_α')
hence "lincomb α' (set A) = lincomb_list c A"
using lincomb_list_as_lincomb[OF assms(1), of c] c by argo
also have "... ∈ span_list A" using c in_span_listI by blast
finally show "x ∈ span_list A" using x_α' by blast
qed
ultimately show ?thesis by blast
qed
end
section "Module Homomorphism Linear Combination and Span Lemmas"
context mod_hom
begin
lemma lincomb_list_distrib:
assumes "set S ⊆ carrier M"
assumes "α ∈ {..<length S} → carrier R"
shows "f (M.lincomb_list α S) = N.lincomb_list α (map f S)"
using assms
proof(induct "length S" arbitrary: S α)
case 0
then show ?case by auto
next
case (Suc n)
then obtain v S' where v: "S = v # S'" by (metis length_Suc_conv)
have 1: "n = length S'" using Suc(2) v by auto
have 2: "set S' ⊆ carrier M" using Suc(3) v by auto
have 3: "(α ∘ Suc) ∈ {..<length S'} → carrier R" using "1" Suc(4) Suc.hyps(2) by fastforce
have ih: "f (M.lincomb_list (α ∘ Suc) S') = N.lincomb_list (α ∘ Suc) (map f S')"
using Suc.hyps(1)[OF 1 2 3] .
have *: "M.lincomb_list α (v # S') = (α 0 ⊙⇘M⇙ v) ⊕⇘M⇙ (M.lincomb_list (α ∘ Suc) S')"
using M.lincomb_list_Cons .
have "v ∈ carrier M" using Suc.prems(1) v by force
moreover have "α 0 ∈ carrier R" using Suc(4) Suc.hyps(2) by auto
ultimately have "α 0 ⊙⇘M⇙ v ∈ carrier M" by blast
moreover have "M.lincomb_list (α ∘ Suc) S' ∈ carrier M"
by (metis (no_types, lifting) "1" "2" M.lincomb_list_carrier Pi_iff Suc(4) Suc.hyps(2) Suc_less_eq atLeastLessThan_iff lessThan_iff o_apply)
ultimately have "f (M.lincomb_list α S) = (f (α 0 ⊙⇘M⇙ v)) ⊕⇘N⇙ (f (M.lincomb_list (α ∘ Suc) S'))"
using f_hom * v unfolding module_hom_def by force
also have "... = (α 0 ⊙⇘N⇙ f v) ⊕⇘N⇙ (f (M.lincomb_list (α ∘ Suc) S'))"
by (simp add: ‹α 0 ∈ carrier R› ‹v ∈ carrier M›)
also have "... = (α 0 ⊙⇘N⇙ f v) ⊕⇘N⇙ (N.lincomb_list (α ∘ Suc) (map f S'))" using ih by argo
also have "... = N.lincomb_list α (map f S)"
using N.lincomb_list_Cons by (simp add: v)
finally show ?case .
qed
lemma lincomb_distrib:
assumes "inj_on f S"
assumes "S ⊆ carrier M"
assumes "α ∈ S → carrier R"
assumes "∀v ∈ S. α v = β (f v)"
assumes "finite S"
shows "f (M.lincomb α S) = N.lincomb β (f`S)"
proof-
let ?α' = "(λv. (α v) ⊙⇘M⇙ v)"
let ?β' = "(λv. (β v) ⊙⇘N⇙ v)"
have *: "?α' ∈ S → carrier M" using assms(2,3) by auto
have "f (M.lincomb α S) = f (finsum M ?α' S)" using M.lincomb_def by presburger
also have "... = (⨁⇘N⇙a∈S. f ((α a) ⊙⇘M⇙ a))" using hom_sum[OF assms(2) *] .
also have "... = (⨁⇘N⇙a∈S. (α a) ⊙⇘N⇙ (f a))"
proof-
have "∀a ∈ S. a ∈ carrier M" using assms(2) by fastforce
moreover have "∀a ∈ S. α a ∈ carrier R" using assms(3) by blast
ultimately show ?thesis
using f_hom unfolding module_hom_def by (simp add: N.M.add.finprod_cong')
qed
also have "... = (⨁⇘N⇙a∈S. (β (f a)) ⊙⇘N⇙ (f a))"
by (smt (verit, del_insts) N.M.add.finprod_cong' M.summands_valid PiE Pi_I assms(2-4) basic_trans_rules(31) f_im f_smult)
also have "... = (⨁⇘N⇙a∈(f`S). (?β' a))"
by (smt (verit, best) assms(1,4) M.summands_valid N.M.add.finprod_cong' N.M.add.finprod_reindex PiE Pi_I assms(2) assms(3) assms(4) basic_trans_rules(31) f_im f_smult imageE)
also have "... = N.lincomb β (f`S)" using N.lincomb_def by presburger
finally show ?thesis .
qed
lemma lincomb_distrib_obtain:
assumes "inj_on f S"
assumes "S ⊆ carrier M"
assumes "α ∈ S → carrier R"
assumes "∀v ∈ S. α v = β (f v)"
assumes "finite S"
obtains β where "(∀v ∈ S. α v = β (f v)) ∧ f (M.lincomb α S) = N.lincomb β (f`S)"
proof-
obtain β where β: "∀v ∈ S. α v = β (f v)"
proof-
let ?β = "λy. α (THE x. x ∈ S ∧ f x = y)"
have "∀v ∈ S. α v = ?β (f v)"
proof
fix v assume "v ∈ S"
then have "v = (THE x. x ∈ S ∧ f x = f v)"
using assms(1) by (simp add: inj_on_def the_equality)
thus "α v = ?β (f v)" by argo
qed
thus ?thesis using that by fast
qed
thus ?thesis using lincomb_distrib that assms by blast
qed
lemma image_span_list:
assumes "set vs ⊆ carrier M"
shows "f`(M.span_list vs) = N.span_list (map f vs)" (is "?lhs = ?rhs")
proof-
have "?lhs ⊆ ?rhs"
proof(rule subsetI)
fix w assume "w ∈ ?lhs"
then obtain v where v: "v ∈ M.span_list vs ∧ f v = w" by blast
then obtain α where α: "v = M.lincomb_list α vs ∧ α ∈ {..<length vs} → carrier R"
unfolding M.span_list_def by fastforce
hence "f v = N.lincomb_list α (map f vs)" using lincomb_list_distrib[OF assms(1)] v by blast
thus "w ∈ ?rhs" using v α unfolding N.span_list_def by force
qed
moreover have "?rhs ⊆ ?lhs"
proof(rule subsetI)
fix w assume "w ∈ ?rhs"
then obtain α where α: "w = N.lincomb_list α (map f vs) ∧ α ∈ {..<length vs} → carrier R"
unfolding N.span_list_def by fastforce
hence "w = f (M.lincomb_list α vs)"
using lincomb_list_distrib[OF assms] by presburger
thus "w ∈ ?lhs" using α unfolding M.span_list_def by fastforce
qed
ultimately show ?thesis by blast
qed
lemma image_span:
assumes "finite vs"
assumes "vs ⊆ carrier M"
shows "f`(M.span vs) = N.span (f`vs)"
proof-
obtain vs_list where vs_list: "set vs_list = vs" using assms(1) finite_list by blast
have "f`vs = set (map f vs_list)" using vs_list by simp
hence "N.span (f`vs) = N.span_list (map f vs_list)"
by (metis N.span_list_span M.sum_simp assms(2) f_im image_subset_iff)
moreover have "M.span vs = M.span_list vs_list"
using M.span_list_span vs_list assms(2) by presburger
ultimately show ?thesis using image_span_list assms vs_list by presburger
qed
end
section "Linear Map Lemmas"
lemma (in linear_map) inj_image_lin_indpt:
assumes "inj_on T (carrier V)"
assumes "S ⊆ carrier V"
assumes "V.module.lin_indpt S"
assumes "finite S"
shows "W.module.lin_indpt (T`S)"
proof(rule ccontr)
assume "¬ W.module.lin_indpt (T`S)"
then obtain B β b where B: "finite B
∧ B ⊆ T`S
∧ (β ∈ (B → carrier K))
∧ (lincomb β B = 𝟬⇘W⇙)
∧ (b∈B)
∧ (β b ≠ 𝟬⇘K⇙)"
using W.module.lin_dep_def by auto
define A where "A ≡ {a ∈ S. T a ∈ B}"
define α where "α ≡ (λv. β (T v))"
have 1: "inj_on T A"
by (metis (no_types, lifting) assms(1,2) inj_on_subset A_def mem_Collect_eq subsetI)
have 2: "A ⊆ carrier V" using A_def assms(2) by blast
have 3: "α ∈ A → carrier K"
proof
fix x assume "x ∈ A"
moreover then have "T x ∈ carrier W" using 2 by blast
ultimately show "α x ∈ carrier K" unfolding α_def using B A_def by blast
qed
have 4: "∀v∈A. α v = β (T v)" using α_def by blast
have 5: "finite A" using A_def assms(4) by force
have "B = T`A" unfolding A_def using B by blast
hence "lincomb β B = T (V.module.lincomb α A)" using lincomb_distrib[OF 1 2 3 4 5] by argo
hence "T (V.module.lincomb α A) = 𝟬⇘W⇙" using B by argo
moreover have "T (𝟬⇘V⇙) = 𝟬⇘W⇙" by auto
ultimately have *: "(V.module.lincomb α A) = 𝟬⇘V⇙" using assms(1) by (simp add: 2 3 inj_onD)
moreover obtain a where "T a = b ∧ a ∈ A" using B ‹B = T ` A› by blast
moreover then have "α a ≠ 𝟬⇘K⇙" by (simp add: B α_def)
moreover have "A ⊆ S" using A_def by blast
ultimately show False using assms(3) 5 3 V.module.lin_dep_def by blast
qed
lemma linear_map_mat:
assumes "A ∈ carrier_mat n m"
shows "linear_map class_ring (module_vec TYPE('a::{field,ring_1}) m) (module_vec TYPE('a) n) ((*⇩v) A)"
(is "linear_map ?K ?V ?W ?T")
proof-
have "vectorspace ?K ?V" using VS_Connect.vec_vs[of "m"] by blast
moreover have "vectorspace ?K ?W" using VS_Connect.vec_vs[of "n"] by blast
moreover have "mod_hom ?K ?V ?W ?T"
proof-
have V: "module ?K ?V" by (simp add: vec_module)
moreover have W: "module ?K ?W" by (simp add: vec_module)
moreover have "?T ∈ LinearCombinations.module_hom ?K ?V ?W"
proof-
have "?T ∈ carrier ?V → carrier ?W" by (metis Pi_I assms mult_mat_vec_carrier vec_space.cV)
moreover have "∀v⇩1 ∈ carrier ?V. ∀v⇩2 ∈ carrier ?V. ?T (v⇩1 + v⇩2) = ?T v⇩1 + ?T v⇩2"
by (metis module_vec_def assms monoid_record_simps(1) mult_add_distrib_mat_vec)
moreover have "∀α ∈ carrier ?K. ∀v ∈ carrier ?V. ?T (α ⋅⇩v v) = α ⋅⇩v (?T v)"
by (metis assms mult_mat_vec vec_space.cV)
ultimately show ?thesis unfolding module_vec_def module_hom_def by force
qed
ultimately show ?thesis
unfolding mod_hom_def mod_hom_axioms_def by blast
qed
ultimately show ?thesis unfolding linear_map_def by blast
qed
section "Courant-Fischer Minimax Theorem"
text
"We follow the proof given in this set of lecture notes by Dr. David Bindel:
https://www.cs.cornell.edu/courses/cs6210/2019fa/lec/2019-11-04.pdf."
definition sup_defined :: "'a::preorder set ⇒ bool" where
"sup_defined S ⟷ S ≠ {} ∧ bdd_above S"
definition inf_defined :: "'a::preorder set ⇒ bool" where
"inf_defined S ⟷ S ≠ {} ∧ bdd_below S"
locale hermitian_mat = complex_vec_space n for n +
fixes A :: "complex mat"
assumes dim_is: "A ∈ carrier_mat n n"
assumes is_herm: "hermitian A"
begin
definition dimensional :: "complex vec set ⇒ nat ⇒ bool" where
"dimensional 𝒱 k ⟷ (∃vs. 𝒱 = span vs ∧ card vs = k ∧ vs ⊆ carrier_vec n ∧ lin_indpt vs)"
lemma dimensional_n: "dimensional 𝒱 k ⟹ 𝒱 ⊆ carrier_vec n"
using hermitian_mat.dimensional_def hermitian_mat_axioms by auto
lemma dimensional_n_vec: "⋀v. v ∈ 𝒱 ⟹ dimensional 𝒱 k ⟹ v ∈ carrier_vec n"
using dimensional_n by fast
text "Note here that we refer to the Inf and Sup rather than the Min and Max."
definition rayleigh_min:
"rayleigh_min 𝒱 = Inf {ρ A v | v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1}"
definition rayleigh_max:
"rayleigh_max 𝒱 = Sup {ρ A v | v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1}"
definition maximin :: "nat ⇒ real" where
"maximin k = Sup {rayleigh_min 𝒱 | 𝒱. dimensional 𝒱 k}"
definition minimax :: "nat ⇒ real" where
"minimax k = Inf {rayleigh_max 𝒱 | 𝒱. dimensional 𝒱 (n - k + 1)}"
definition maximin_defined where
"maximin_defined k ⟷ sup_defined {rayleigh_min 𝒱 | 𝒱. dimensional 𝒱 k}"
definition minimax_defined where
"minimax_defined k ⟷ inf_defined {rayleigh_max 𝒱 | 𝒱. dimensional 𝒱 (n - k + 1)}"
end
locale courant_fischer = hermitian_mat n for n +
fixes Λ U :: "complex mat"
fixes es :: "complex list"
assumes eigvals: "eigvals_of A es"
assumes eigvals_sorted: "sorted_wrt (≥) es"
assumes A_decomp: "real_diag_decomp A Λ U
∧ diag_mat Λ = es
∧ set es ⊆ Reals
∧ U ∈ carrier_mat n n
∧ Λ ∈ carrier_mat n n"
begin
sublocale conjugatable_vec_space "TYPE(complex)" n .
lemma dim: "local.dim = n"
by (simp add: dim_is_n)
lemma fin_dim: "fin_dim" by simp
lemma gr_n_lin_dpt:
assumes "B ⊆ carrier_vec n"
assumes "card B > local.dim"
shows "lin_dep B"
using li_le_dim(2)[of B] dim fin_dim assms by linarith
lemma rayleigh_kx:
assumes "v ∈ carrier_vec n"
assumes "k ≠ 0"
assumes "v ≠ 0⇩v n"
shows "ρ A (k ⋅⇩v v) = ρ A v"
proof-
let ?v' = "(k ⋅⇩v v)"
have "(A *⇩v ?v') ∙c ?v' = (cmod k)^2 * (QF A v)"
by (smt (verit, ccfv_SIG) dim_is assms(1) carrier_vecD cring_simprules(11) dim_vec_conjugate index_smult_vec(2) inner_prod_smult_right mult_conj_cmod_square mult_mat_vec mult_mat_vec_carrier quadratic_form_def scalar_prod_smult_left)
moreover have "?v' ∙c ?v' = (cmod k)^2 * (v ∙c v)"
by (metis assms(1) cring_simprules(11) dim_vec_conjugate index_smult_vec(2) inner_prod_smult_right mult_conj_cmod_square scalar_prod_smult_left)
ultimately show "ρ A ?v' = ρ A v" by (simp add: assms(2))
qed
lemma unit_vec_rayleigh_formula:
assumes unit_v: "vec_norm v = 1"
assumes v_dim: "v ∈ carrier_vec n"
shows "ρ A v = (∑j ∈ {..<n}. es!j * (cmod ((U⇧H *⇩v v)$j))^2)"
proof-
have U_Λ: "unitary U ∧ unitary U⇧H" "A = U * Λ * U⇧H" "U⇧H ∈ carrier_mat n n"
apply (metis A_decomp adjoint_is_conjugate_transpose real_diag_decomp_def unitarily_equiv_def unitary_adjoint unitary_diag_def)
apply (metis A_decomp adjoint_is_conjugate_transpose real_diag_decomp_def similar_mat_wit_def unitarily_equiv_def unitary_diag_def)
by (simp add: A_decomp)
have"diagonal_mat Λ" using A_decomp unfolding real_diag_decomp_def by fastforce
hence Λ_diag_mult: "⋀x i. x ∈ carrier_vec n ⟹ i ∈ {..<n} ⟹ (Λ *⇩v x)$i = (Λ$$(i,i) * x$i)"
using A_decomp diagonal_mat_mult_vec by blast
have Λ_diag_eigenvals: "⋀i. i ∈ {..<n} ⟹ Λ$$(i,i) = es!i"
using A_decomp
unfolding diag_mat_def
by (smt (verit, del_insts) carrier_matD(1) diff_zero length_map length_upt lessThan_iff nth_map nth_upt semiring_norm(50))
define x where "x ≡ U⇧H *⇩v v"
hence x_dim: "x ∈ carrier_vec n"
using U_Λ(3) mult_mat_vec_carrier v_dim by blast
hence x_conj_dim: "conjugate x ∈ carrier_vec n" by simp
have x_norm: "vec_norm x = 1" using U_Λ unit_v unitary_vec_norm v_dim x_def by presburger
have *: "⋀i. i ∈ {..<n} ⟹ (conjugate x)$i = conjugate (x$i)"
unfolding conjugate_vec_def using x_dim by auto
have "v ∙c v = 1" using unit_v csqrt_eq_1 unfolding vec_norm_def by blast
hence "QF A v / Complex_Matrix.inner_prod v v = QF A v" by simp
hence "ρ A v = complex_of_real (Re (QF A v))"
unfolding rayleigh_quotient_def by simp
also have "... = QF A v"
using hermitian_quadratic_form_real[OF dim_is v_dim is_herm] by simp
also have "... = inner_prod v ((U * Λ * U⇧H) *⇩v v)"
unfolding quadratic_form_def using U_Λ by blast
also have "... = inner_prod v (U *⇩v ((Λ * U⇧H) *⇩v v))"
by (smt (verit, best) A_decomp More_Matrix.carrier_vec_conjugate assoc_mat_mult_vec' carrier_dim_vec mat_vec_mult_assoc transpose_carrier_mat v_dim)
also have "... = inner_prod (U⇧H *⇩v v) ((Λ * U⇧H) *⇩v v)"
by (metis A_decomp More_Matrix.carrier_vec_conjugate adjoint_def_alter adjoint_is_conjugate_transpose mult_carrier_mat mult_mat_vec_carrier transpose_carrier_mat v_dim)
also have "... = (Λ *⇩v x) ∙c x"
by (metis A_decomp More_Matrix.carrier_vec_conjugate carrier_vecD mat_vec_mult_assoc transpose_carrier_mat v_dim x_def)
also have "... = (∑j ∈ {..<n}. (Λ *⇩v x)$j * (conjugate x)$j)"
unfolding inner_prod_def scalar_prod_def using atLeast0LessThan x_dim by auto
also have "... = (∑j ∈ {..<n}. (Λ$$(j,j) * x$j) * (conjugate x)$j)"
using Λ_diag_mult x_dim by auto
also have "... = (∑j ∈ {..<n}. (es!j * x$j) * (conjugate x)$j)"
using Λ_diag_eigenvals by simp
also have "... = (∑j ∈ {..<n}. (es!j * x$j) * conjugate (x$j))"
using * by simp
also have "... = (∑j ∈ {..<n}. es!j * (cmod (x$j))^2)"
by (smt (verit) cring_simprules(11) mult_conj_cmod_square of_real_mult of_real_sum sum.cong)
finally show "ρ A v = (∑j ∈ {..<n}. es!j * (cmod (x$j))^2)"
using of_real_eq_iff by blast
qed
lemma rayleigh_bdd_below':
assumes "k ≤ n"
shows "∃m. ∀v ∈ carrier_vec n. v ≠ 0⇩v n ⟶ ρ A v ≥ m"
proof-
define m where "m ≡ Min (Re ` set es)"
have "⋀v. v ∈ carrier_vec n ⟹ v ≠ 0⇩v n ⟹ ρ A v ≥ m"
proof-
fix v :: "complex vec"
assume *: "v ∈ carrier_vec n" "v ≠ 0⇩v n"
define v' where "v' ≡ vec_normalize v"
have v': "vec_norm v' = 1 ∧ v' ∈ carrier_vec n"
using normalized_vec_norm[of v n] unfolding vec_norm_def v'_def
using * csqrt_1 normalized_vec_dim by presburger
have "ρ A v = ρ A v'"
by (metis "*"(1) normalize_zero rayleigh_kx v' v'_def vec_eq_norm_smult_normalized vec_norm_zero)
also have "... = (∑i ∈ {..<n}. es!i * (cmod ((U⇧H *⇩v v')$i))^2)"
using unit_vec_rayleigh_formula * v' by blast
also have "... ≥ m"
proof-
have "vec_norm (U⇧H *⇩v v') = 1"
by (metis v' A_decomp Complex_Matrix.unitary_def adjoint_dim_row adjoint_is_conjugate_transpose carrier_matD(2) real_diag_decomp_def unitary_adjoint unitary_diagD(3) unitary_vec_norm)
moreover have "vec_norm (U⇧H *⇩v v') = csqrt (∑i ∈ {..<n}. (cmod ((U⇧H *⇩v v')$i))^2)"
by (metis complex_vec_norm_sum A_decomp carrier_dim_vec carrier_matD(2) dim_mult_mat_vec dim_row_conjugate index_transpose_mat(2))
ultimately have norm: "(∑i ∈ {..<n}. (cmod ((U⇧H *⇩v v')$i))^2) = 1"
by (metis Re_complex_of_real one_complex.sel(1) one_power2 power2_csqrt)
have "finite (Re ` set es)" by simp
hence "∀x ∈ Re ` set es. m ≤ x" using Min_le m_def by blast
moreover have "∀i ∈ {..<n}. ∃x ∈ Re ` set es. x = es!i"
by (metis A_decomp carrier_matD(1) diag_mat_length image_eqI lessThan_iff nth_mem of_real_Re subsetD)
ultimately have "⋀i. i ∈ {..<n} ⟹ m ≤ es!i"
by (metis Im_complex_of_real Re_complex_of_real less_eq_complex_def)
hence ineq:
"⋀i. i ∈ {..<n} ⟹ m * (cmod ((U⇧H *⇩v v')$i))^2 ≤ es!i * (cmod ((U⇧H *⇩v v')$i))^2"
by (metis conjugate_square_positive mult_conj_cmod_square mult_right_mono of_real_hom.hom_mult)
have "m ≤ m * (∑i ∈ {..<n}. (cmod ((U⇧H *⇩v v')$i))^2)" using norm by auto
also have "... = (∑i ∈ {..<n}. m * (cmod ((U⇧H *⇩v v')$i))^2)"
by (simp add: mult_hom.hom_sum)
also have "... ≤ (∑i ∈ {..<n}. es!i * (cmod ((U⇧H *⇩v v')$i))^2)"
by (smt (verit, best) of_real_sum sum_mono ineq)
finally show ?thesis
by (metis Im_complex_of_real Re_complex_of_real less_eq_complex_def)
qed
finally show "ρ A v ≥ m" by (simp add: less_eq_complex_def)
qed
thus ?thesis by blast
qed
lemma rayleigh_bdd_below:
assumes "dimensional 𝒱 k"
assumes "k ≤ n"
shows "∃m. ∀v ∈ 𝒱. v ≠ 0⇩v n ⟶ ρ A v ≥ m"
using assms
unfolding dimensional_def
by (meson span_is_subset2 subsetI rayleigh_bdd_below' span_closed span_mem)
lemma rayleigh_min_exists:
assumes "dimensional 𝒱 k"
assumes "k ≤ n"
shows "∀x ∈ {ρ A v | v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1}. rayleigh_min 𝒱 ≤ x"
using rayleigh_bdd_below[OF assms(1) assms(2)]
unfolding rayleigh_min
by (smt (verit) bdd_below.I cInf_lower mem_Collect_eq)
lemma courant_fischer_unit_rayleigh_helper2:
assumes "dimensional 𝒱 (k + 1)"
shows "∃v. vec_norm v = 1 ∧ v ∈ 𝒱 ∧ v ≠ 0⇩v n ∧ ρ A v ≤ es!k"
proof-
have suc_k_leq_n: "k + 1 ≤ n"
using assms(1) unfolding dimensional_def using gr_n_lin_dpt
by (metis dim fin_dim li_le_dim(2))
obtain v where v:
"v ∈ carrier_vec n" "vec_norm v = 1" "(∀j < k. (U⇧H *⇩v v)$j = 0) ∧ v ≠ 0⇩v n ∧ v ∈ 𝒱"
proof-
let ?k_kernel = "{v ∈ carrier_vec n. (∀j < k. (U⇧H *⇩v v)$j = 0)}"
obtain v where v: "v ∈ ?k_kernel ∩ 𝒱 ∧ v ≠ 0⇩v n"
proof-
obtain B⇩𝒱 where B⇩𝒱: "𝒱 = span B⇩𝒱 ∧ card B⇩𝒱 = k + 1 ∧ B⇩𝒱 ⊆ carrier_vec n ∧ lin_indpt B⇩𝒱"
using assms unfolding dimensional_def by blast
obtain B⇩k where B⇩k: "span B⇩k ⊆ ?k_kernel ∧ card B⇩k = n - k ∧ B⇩k ⊆ carrier_vec n ∧ lin_indpt B⇩k"
proof-
obtain M where M: "M * U⇧H = 1⇩m n ∧ U⇧H * M = 1⇩m n ∧ M ∈ carrier_mat n n"
by (metis A_decomp Complex_Matrix.unitary_def adjoint_dim_row adjoint_is_conjugate_transpose carrier_matD(2) mat_mult_left_right_inverse real_diag_decomp_def unitary_adjoint unitary_diagD(3) unitary_simps(1))
define B⇩k where "B⇩k = set (drop k (cols M))"
hence "B⇩k ⊆ set (cols M)" by (meson set_drop_subset)
hence lin_indpt: "lin_indpt B⇩k"
by (metis M A_decomp More_Matrix.carrier_vec_conjugate det_zero_low_rank distinct_cols_id idom_vec.lin_dep_cols_imp_det_0 lin_indpt_id linorder_not_le one_carrier_mat rank_mat_mul_right supset_ld_is_ld transpose_carrier_mat vec_space.lin_indpt_full_rank)
have 1: "span B⇩k ⊆ ?k_kernel"
proof
fix v assume *: "v ∈ span B⇩k"
then obtain cs where "v = lincomb cs B⇩k"
by (metis (no_types, lifting) M ‹B⇩k ⊆ set (cols M)› carrier_matD(1) cols_dim fin_dim finite_in_span li_le_dim(1) lin_indpt order_trans)
hence sum: "U⇧H *⇩v v = finsum_vec TYPE(complex) n (λb. (cs b) ⋅⇩v (U⇧H *⇩v b)) B⇩k"
using mat_vec_mult_sum[of v n "U⇧H" B⇩k cs] unfolding lincomb_def
by (metis A_decomp B⇩k_def List.finite_set M More_Matrix.carrier_vec_conjugate ‹B⇩k ⊆ set (cols M)› ‹v = lincomb cs B⇩k› basic_trans_rules(23) carrier_matD(1) cols_dim finsum_vec lincomb_closed transpose_carrier_mat)
have "⋀i. i < k ⟹ (U⇧H *⇩v v)$i = 0"
proof-
fix i assume *: "i < k"
have cs: "(λb. cs b ⋅⇩v (U⇧H *⇩v b)) ∈ B⇩k → carrier_vec n"
proof
fix x assume "x ∈ B⇩k"
thus "cs x ⋅⇩v (U⇧H *⇩v x) ∈ carrier_vec n"
by (metis A_decomp carrier_dim_vec carrier_matD(2) dim_mult_mat_vec dim_row_conjugate index_smult_vec(2) index_transpose_mat(2))
qed
have B⇩k: "⋀b. b ∈ B⇩k ⟹ (U⇧H *⇩v b)$i = 0"
proof-
fix b assume **: "b ∈ B⇩k"
then obtain j' where "b = drop k (cols M)!j' ∧ j' < n - k"
by (metis B⇩k_def M carrier_matD(2) cols_length in_set_conv_nth length_drop)
then obtain j where j: "b = (cols M)!j ∧ j ≥ k ∧ j < n"
by (metis Groups.add_ac(2) M add_leD1 carrier_matD(2) cols_length le_add2 less_diff_conv nth_drop suc_k_leq_n)
have "i < n ∧ j < n ∧ i ≠ j" using * j by simp
hence "0 = (1⇩m n)$$(i,j)" by simp
also have "... = (U⇧H * M)$$(i,j)"
using M by argo
also have "... = row U⇧H i ∙ col M j"
by (metis "*" M add_leD1 carrier_matD(1) carrier_matD(2) dual_order.strict_trans1 index_mult_mat(1) index_mult_mat(2) j suc_k_leq_n)
also have "... = row U⇧H i ∙ b"
using j M by auto
also have "... = (U⇧H *⇩v b)$i"
by (metis "*" A_decomp carrier_matD(2) dim_row_conjugate dual_order.strict_trans dual_order.strict_trans1 index_mult_mat_vec index_transpose_mat(2) j)
finally show "(U⇧H *⇩v b)$i = 0" by presburger
qed
have "(U⇧H *⇩v v)$i = (finsum_vec TYPE(complex) n (λb. (cs b) ⋅⇩v (U⇧H *⇩v b)) B⇩k)$i"
using sum by simp
also have "... = (∑b ∈ B⇩k. ((cs b) ⋅⇩v (U⇧H *⇩v b))$i)"
using index_finsum_vec[of B⇩k i n "(λb. (cs b) ⋅⇩v (U⇧H *⇩v b))"] cs "*" B⇩k_def suc_k_leq_n
by fastforce
also have "... = (∑b ∈ B⇩k. (cs b) * ((U⇧H *⇩v b))$i)"
using "*" A_decomp suc_k_leq_n by force
also have "... = (∑b ∈ B⇩k. (cs b) * 0)"
using B⇩k by fastforce
also have "... = 0"
by simp
finally show "(U⇧H *⇩v v)$i = 0" .
qed
thus "v ∈ ?k_kernel"
by (smt (verit) "*" M ‹B⇩k ⊆ set (cols M)› basic_trans_rules(23) carrier_matD(1) cols_dim mem_Collect_eq span_closed)
qed
have 2: "card B⇩k = n - k"
proof-
have "distinct (cols M)"
by (metis A_decomp M More_Matrix.carrier_vec_conjugate conjugatable_vec_space.distinct_cols_id lin_indpt_full_rank lin_indpt_id linorder_not_le non_distinct_low_rank one_carrier_mat rank_mat_mul_right transpose_carrier_mat)
hence "card B⇩k = length (drop k (cols M))"
using B⇩k_def distinct_card distinct_drop by blast
moreover have "length (cols M) = n" using M by force
ultimately show ?thesis by force
qed
have 3: "B⇩k ⊆ carrier_vec n"
by (metis M ‹B⇩k ⊆ set (cols M)› basic_trans_rules(23) carrier_matD(1) cols_dim)
from 1 2 3 lin_indpt that show ?thesis by blast
qed
define B where "B = B⇩𝒱 ∪ B⇩k"
have "B⇩𝒱 ∩ B⇩k ≠ {} ⟹ ?thesis"
proof-
assume *: "B⇩𝒱 ∩ B⇩k ≠ {}"
have "0⇩v n ∉ B⇩𝒱" by (simp add: B⇩𝒱 vs_zero_lin_dep)
moreover have "0⇩v n ∉ B⇩k" by (simp add: B⇩k vs_zero_lin_dep)
ultimately obtain b where b: "b ∈ B⇩𝒱 ∩ B⇩k ∧ b ≠ 0⇩v n" using * by blast
moreover then have "b ∈ 𝒱" by (simp add: B⇩𝒱 span_mem)
moreover have "b ∈ ?k_kernel"
by (metis (no_types, lifting) B⇩k IntE Set.basic_monos(7) b in_own_span)
ultimately show ?thesis using that by fast
qed
moreover have "B⇩𝒱 ∩ B⇩k = {} ⟹ ?thesis"
proof-
assume *: "B⇩𝒱 ∩ B⇩k = {}"
hence "card (B⇩𝒱 ∪ B⇩k) = card B⇩𝒱 + card B⇩k"
by (simp add: B⇩𝒱 B⇩k card_Un_disjnt disjnt_def li_le_dim(1))
hence "card B > n" using B_def B⇩𝒱 B⇩k suc_k_leq_n by presburger
moreover have "B ⊆ carrier_vec n" unfolding B_def using B⇩𝒱 B⇩k by blast
ultimately have lin_dep: "lin_dep B" using gr_n_lin_dpt dim by presburger
obtain cs cs' where
eq: "lincomb cs B⇩𝒱 = lincomb cs' B⇩k ∧ (∃b ∈ B⇩𝒱. cs b ≠ 0) ∧ (∃b ∈ B⇩k. cs' b ≠ 0)"
proof-
obtain cs where cs: "lincomb cs B = 0⇩v n ∧ (∃b ∈ B. cs b ≠ 0)"
by (metis lin_dep ‹B ⊆ carrier_vec n› ‹n < card B› bot_nat_0.extremum_strict card.infinite finite_lin_indpt2)
define cs' where "cs' = (λv. - cs v)"
have "⋀i. i < n ⟹ (lincomb cs B⇩𝒱)$i = (lincomb cs' B⇩k)$i"
proof-
fix i
assume **: "i < n"
have "0 = (lincomb cs B)$i"
by (simp add: "**" cs)
also have "... = (∑b ∈ B. (cs b ⋅⇩v b)$i)"
by (smt (verit, ccfv_SIG) ** R.add.finprod_cong' ‹B ⊆ carrier_vec n› carrier_vecD index_smult_vec(1) lincomb_index smult_carrier_vec summands_valid)
also have "... = (∑b ∈ B⇩𝒱. (cs b ⋅⇩v b)$i) + (∑b ∈ B⇩k. (cs b ⋅⇩v b)$i)"
by (simp add: B⇩𝒱 B⇩k B_def fin_dim_li_fin sum.union_disjoint *)
finally have "(∑b ∈ B⇩𝒱. (cs b ⋅⇩v b)$i) = - (∑b ∈ B⇩k. (cs b ⋅⇩v b)$i)"
by (simp add: eq_neg_iff_add_eq_0)
hence "(lincomb cs B⇩𝒱)$i = (∑b ∈ B⇩k. - ((cs b) ⋅⇩v b)$i)"
by (smt (verit, best) "**" B⇩𝒱 R.add.finprod_cong' carrier_vecD index_smult_vec(1) lincomb_index smult_carrier_vec sum_negf summands_valid)
moreover have "⋀v. v ∈ carrier_vec n ⟹ - (v$i) = (-v)$i"
by (simp add: "**")
moreover have "⋀b. (- (cs b) ⋅⇩v b)$i = (( - cs b) ⋅⇩v b)$i"
by blast
ultimately have "(lincomb cs B⇩𝒱)$i = (∑b ∈ B⇩k. ((- cs b) ⋅⇩v b)$i)"
by (smt (verit, del_insts) B⇩k R.add.finprod_cong' local.vec_neg smult_carrier_vec smult_l_minus summands_valid)
also have "... = (lincomb cs' B⇩k)$i"
by (smt (verit, best) "**" B⇩k R.add.finprod_cong' carrier_vecD cs'_def index_smult_vec(1) lincomb_index smult_carrier_vec summands_valid)
finally show "(lincomb cs B⇩𝒱)$i = (lincomb cs' B⇩k)$i" by blast
qed
hence 1: "(lincomb cs B⇩𝒱) = (lincomb cs' B⇩k)"
by (metis (no_types, lifting) B⇩𝒱 B⇩k carrier_vecD eq_vecI lincomb_closed)
have 2: "∃b ∈ B⇩𝒱. cs b ≠ 0"
proof(rule ccontr)
assume "¬ (∃b∈B⇩𝒱. cs b ≠ 0)"
hence *: "∀b ∈ B⇩𝒱. cs b = 0" by blast
hence "∀i < n. (lincomb cs B⇩𝒱)$i = 0" by (simp add: B⇩𝒱 vec_space.lincomb_index)
hence "lincomb cs B⇩𝒱 = 0⇩v n" using B⇩𝒱 by auto
moreover have "lin_indpt B⇩k" using B⇩k by blast
ultimately have "∀b ∈ B⇩k. cs' b = 0"
by (metis (no_types, lifting) "1" B⇩k fin fin_dim lin_dep_def order.refl)
hence "∀b ∈ B⇩k. cs b = 0" unfolding cs'_def by fastforce
hence "∀b ∈ B. cs b = 0" using * unfolding B_def by blast
thus False using cs by blast
qed
have 3: "∃b ∈ B⇩k. cs' b ≠ 0"
proof(rule ccontr)
assume "¬ (∃b ∈ B⇩k. cs' b ≠ 0)"
hence *: "∀b ∈ B⇩k. cs' b = 0" by blast
hence "∀i < n. (lincomb cs' B⇩k)$i = 0" by (simp add: B⇩k vec_space.lincomb_index)
hence "lincomb cs' B⇩k = 0⇩v n" using B⇩k by auto
moreover have "lin_indpt B⇩𝒱" using B⇩𝒱 by blast
ultimately have "∀b ∈ B⇩𝒱. cs b = 0"
by (metis "1" B⇩𝒱 fin_dim li_le_dim(1) lin_dep_def subsetI)
hence "∀b ∈ B. cs b = 0" using * unfolding B_def cs'_def by fastforce
thus False using cs by blast
qed
from 1 2 3 that show ?thesis by algebra
qed
define v where "v ≡ lincomb cs B⇩𝒱"
define w where "w ≡ lincomb cs' B⇩k"
have "⋀i. i < n ⟹ v$i = w$i" using eq v_def w_def by argo
moreover have "⋀i. i < n ⟹ w$i = (∑b ∈ B⇩k. (cs' b ⋅⇩v b)$i)"
by (smt (verit, best) B⇩k carrier_vecD index_smult_vec(1) lincomb_index smult_carrier_vec sum.cong summands_valid w_def)
moreover have "v ∈ 𝒱" by (simp add: B⇩𝒱 in_spanI li_le_dim(1) v_def)
moreover have "w ∈ ?k_kernel"
proof-
have "w ∈ carrier_vec n" by (metis B⇩𝒱 eq lincomb_closed w_def)
moreover have "U⇧H ∈ carrier_mat n n" by (simp add: A_decomp)
moreover have "B⇩k ⊆ carrier_vec n" by (simp add: B⇩k)
moreover have "finite B⇩k" by (simp add: B⇩k fin)
ultimately have "U⇧H *⇩v w = finsum_vec TYPE(complex) n (λb. cs' b ⋅⇩v (U⇧H *⇩v b)) B⇩k"
using mat_vec_mult_sum[of w n "U⇧H" B⇩k] lincomb_def w_def by fastforce
thus ?thesis using B⇩k ‹finite B⇩k› w_def by blast
qed
moreover have "v ≠ 0⇩v n" by (metis B⇩𝒱 eq fin fin_dim lin_dep_crit order.refl v_def)
ultimately show ?thesis using eq that v_def w_def by auto
qed
ultimately show ?thesis by blast
qed
moreover define v' where "v' ≡ vec_normalize v"
ultimately have "v' ∈ carrier_vec n ∧ vec_norm v' = 1"
using normalized_vec_norm vec_norm_def by force
moreover then have v': "v' = (1 / vec_norm v) ⋅⇩v v"
by (metis div_by_1 one_smult_vec v'_def vec_normalize_def)
moreover have "v' ≠ 0⇩v n" by (metis calculation(1) field.one_not_zero vec_norm_zero)
moreover have "v' ∈ 𝒱"
proof-
have "v ∈ 𝒱" using v by blast
thus ?thesis using v' assms unfolding dimensional_def by auto
qed
moreover have "∀j < k. (U⇧H *⇩v v')$j = 0"
proof clarify
fix j assume *: "j < k"
have "(U⇧H *⇩v v')$j = (U⇧H *⇩v ((1 / vec_norm v) ⋅⇩v v))$j"
using v' by blast
also have "... = ((1 / vec_norm v) ⋅⇩v (U⇧H *⇩v v))$j"
by (metis A_decomp More_Matrix.carrier_vec_conjugate ‹v' ∈ carrier_vec n ∧ vec_norm v' = 1› mult_mat_vec smult_carrier_vec transpose_carrier_mat v')
also have "... = (1 / vec_norm v) * ((U⇧H *⇩v v)$j)"
using "*" A_decomp suc_k_leq_n by auto
also have "... = (1 / vec_norm v) * 0" using "*" v by auto
finally show "(U⇧H *⇩v v')$j = 0" by algebra
qed
ultimately show ?thesis using that by blast
qed
then obtain weights where weights: "(∀i ∈ {k..<n}. weights i ≥ 0)
∧ (∑i ∈ {k..<n}. weights i) = 1 ∧ ρ A v = (∑i ∈ {k..<n}. weights i * es!i)"
proof-
define weights where "weights ≡ λi. (cmod ((U⇧H *⇩v v)$i))^2"
hence 1: "(∀i ∈ {k..<n}. weights i ≥ 0)" by auto
have "⋀i. i ∈ {..<k} ⟹ (U⇧H *⇩v v)$i = 0" using v by blast
hence *: "⋀i. i ∈ {..<k} ⟹ weights i = 0" using weights_def by auto
hence **: "⋀i. i ∈ {..<k} ⟹ weights i * es!i = 0" by (simp add: weights_def)
have "(∑i ∈ {..<n}. weights i) = (∑i ∈ {..<k}. weights i) + (∑i ∈ {k..<n}. weights i)"
by (smt (verit, ccfv_threshold) "*" atLeast0LessThan atLeastLessThan_iff le_eq_less_or_eq linorder_not_le sum.atLeastLessThan_concat sum.not_neutral_contains_not_neutral zero_order(1))
also have "... = (∑i ∈ {k..<n}. weights i)"
by (simp add: "*")
finally have weights: "(∑i ∈ {..<n}. weights i) = (∑i ∈ {k..<n}. weights i)" .
have "(∑i ∈ {..<n}. weights i * es!i) = (∑i ∈ {..<k}. weights i * es!i)
+ (∑i ∈ {k..<n}. weights i * es!i)"
by (smt (verit, ccfv_threshold) "**" atLeast0LessThan atLeastLessThan_iff le_eq_less_or_eq linorder_not_le sum.atLeastLessThan_concat sum.not_neutral_contains_not_neutral zero_order(1))
also have "... = (∑i ∈ {k..<n}. weights i * es!i)"
by (simp add: **)
finally have weights_es: "(∑i ∈ {..<n}. weights i * es!i) = (∑i ∈ {k..<n}. weights i * es!i)" .
have "ρ A v = (∑i ∈ {..<n}. weights i * es!i)"
using unit_vec_rayleigh_formula v weights_def by algebra
hence 2: "ρ A v = (∑i ∈ {k..<n}. weights i * es!i)" using weights_es by argo
have norm: "vec_norm (U⇧H *⇩v v) = vec_norm v"
by (metis A_decomp More_Matrix.carrier_vec_conjugate adjoint_is_conjugate_transpose real_diag_decompD(1) transpose_carrier_mat unitary_adjoint unitary_diagD(3) unitary_vec_norm v(1))
hence "vec_norm (U⇧H *⇩v v) = 1" using v(2) by argo
moreover have "U⇧H *⇩v v ∈ carrier_vec n"
by (metis A_decomp adjoint_dim_row adjoint_is_conjugate_transpose carrier_matD(2) carrier_vec_dim_vec dim_mult_mat_vec)
ultimately have "(∑i ∈ {..<n}. weights i) = 1"
unfolding weights_def by (metis complex_vec_norm_sum norm Re_complex_of_real csqrt_eq_1 one_complex.sel(1) v(2))
hence 3: "(∑i ∈ {k..<n}. weights i) = 1" using weights by presburger
show ?thesis
by (metis 1 2 3 that[of weights] Im_complex_of_real Re_complex_of_real less_eq_complex_def of_real_hom.hom_one of_real_hom.hom_zero of_real_sum)
qed
have "length es = n"
using A_decomp
unfolding diag_mat_def
by (metis A_decomp carrier_matD(1) diag_mat_length)
hence "⋀i. i ∈ {k..<n} ⟹ es!i ≤ es!k"
using eigvals_sorted
by (metis atLeastLessThan_iff le_eq_less_or_eq sorted_wrt_iff_nth_less verit_eq_simplify(6))
then have "⋀i. i ∈ {k..<n} ⟹ weights i * es!i ≤ weights i * es!k"
by (meson weights atLeastLessThan_iff mult_left_mono)
then have "(∑i ∈ {k..<n}. weights i * es!i) ≤ (∑i ∈ {k..<n}. weights i * es!k)"
by (meson sum_mono)
also have "... = (∑i ∈ {k..<n}. weights i) * es!k"
by (metis ideal.scale_sum_left)
also have "... = es!k" using weights by auto
finally have "ρ A v ≤ es!k"
using weights by presburger
thus "∃v. vec_norm v = 1 ∧ v ∈ 𝒱 ∧ v ≠ 0⇩v n ∧ ρ A v ≤ es!k" using v by blast
qed
lemma courant_fischer_unit_rayleigh_helper3:
assumes "n > 0"
assumes "k < n"
assumes "eigvals_of A es"
defines "es_R ≡ map Re es"
shows "∃𝒱. dimensional 𝒱 (k + 1) ∧ (∀v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1 ⟶ es_R ! k ≤ ρ A v)"
proof-
let ?geq = "λv. ρ A v ≥ es_R!k"
let ?P = "λ𝒱 v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1"
let ?Q = "λ𝒱. dimensional 𝒱 (k + 1)"
have "inverts_mat U (adjoint U)"
using A_decomp
unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def similar_mat_wit_def
by (metis Complex_Matrix.unitary_def)
hence U_invertible: "invertible_mat U"
by (metis A_decomp Complex_Matrix.unitary_def carrier_matD(1) carrier_matD(2) invertible_mat_def square_mat.simps unitaryD2)
have "unitary U"
using A_decomp
unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def
by blast
hence U_ortho: "corthogonal_mat U" using unitary_is_corthogonal A_decomp by auto
have "set es ⊆ Reals" by (simp add: A_decomp)
hence es_R: "map complex_of_real es_R = es"
proof-
{ fix i assume *: "i < length es"
hence "es!i ∈ Reals" using A_decomp by auto
hence "complex_of_real (es_R!i) = es!i" by (simp add: * es_R_def)
}
thus ?thesis by (simp add: es_R_def map_nth_eq_conv)
qed
let ?𝒱_basis = "set (take (k + 1) (cols U))"
define 𝒱 where "𝒱 ≡ span ?𝒱_basis"
have "lin_indpt ?𝒱_basis"
using lin_indpt_subset_cols[of U "?𝒱_basis"] A_decomp U_invertible
by (meson in_set_takeD subset_code(1))
moreover have 𝒱_basis_card: "card ?𝒱_basis = k + 1"
proof-
have "distinct (cols U)"
by (metis A_decomp U_invertible invertible_det nat_less_le non_distinct_low_rank vec_space.det_rank_iff)
hence "distinct (take (k + 1) (cols U))"
using distinct_take by blast
thus ?thesis
by (metis A_decomp Suc_leI add.commute add_diff_cancel_right' append_take_drop_id assms(2) carrier_matD(2) cols_length diff_diff_cancel distinct_card length_append length_drop plus_1_eq_Suc)
qed
ultimately have 1: "?Q 𝒱"
unfolding dimensional_def
by (metis A_decomp 𝒱_def carrier_matD(1) cols_dim in_set_takeD subset_code(1))
moreover have 2: "∀v. ?P 𝒱 v ⟶ ?geq v"
proof clarify
fix v :: "complex vec"
assume *: "v ≠ 0⇩v n"
assume **: "v ∈ 𝒱"
assume ***: "vec_norm v = 1"
have "set (cols U) ⊆ carrier_vec n" using A_decomp cols_dim by blast
hence 𝒱_basis_dim: "?𝒱_basis ⊆ carrier_vec n" by (meson in_set_takeD subset_code(1))
hence v_dim: "v ∈ carrier_vec n" using "**" 𝒱_def span_closed by blast
define x where "x ≡ U⇧H *⇩v v"
have x_dim: "x ∈ carrier_vec n"
by (metis A_decomp More_Matrix.carrier_vec_conjugate mult_mat_vec_carrier transpose_carrier_mat v_dim x_def)
have x_norm: "vec_norm x = 1"
by (metis "***" A_decomp More_Matrix.carrier_vec_conjugate adjoint_is_conjugate_transpose real_diag_decomp_def transpose_carrier_mat unitarily_equiv_def unitary_adjoint unitary_diag_def unitary_vec_norm v_dim x_def)
have weights: "(∑j ∈ {..<n}. (cmod (x$j))^2) = 1"
by (metis atLeast0LessThan carrier_vecD cpx_vec_length_square of_real_eq_1_iff power_one vec_norm_sq_cpx_vec_length_sq x_dim x_norm)
have ineq: "⋀j. j ∈ {..<n} ⟹ es!k * (cmod (x$j))^2 ≤ es!j * (cmod (x$j))^2"
proof-
fix j
assume *: "j ∈ {..<n}"
show "es!k * (cmod (x$j))^2 ≤ es!j * (cmod (x$j))^2"
proof(cases "j ≤ k")
case True
hence "es!k ≤ es!j"
by (metis A_decomp antisym_conv1 assms(2) carrier_matD(1) diag_mat_length eigvals_sorted nless_le sorted_wrt_nth_less)
thus ?thesis by (simp add: less_eq_complex_def mult_right_mono)
next
case False
hence j_gr_k: "j > k" by simp
have "inner_prod (col U j) v = 0"
proof-
have j: "j < dim_col U" using * A_decomp by blast
have "∀b ∈ ?𝒱_basis. ∃i. i < dim_col U ∧ b = col U i ∧ i ≠ j"
proof
fix b assume *: "b ∈ ?𝒱_basis"
then obtain i where "b = (cols U)!i ∧ i ≤ k"
by (metis A_decomp U_invertible 𝒱_basis_card add.commute distinct_card distinct_take in_set_conv_nth invertible_det less_Suc_eq_le nat_less_le nth_take plus_1_eq_Suc vec_space.det_rank_iff vec_space.non_distinct_low_rank)
moreover then have "i ≠ j" using j_gr_k by force
ultimately show "∃i<dim_col U. b = col U i ∧ i ≠ j"
by (meson cols_nth j j_gr_k le_simps(1) order_le_less_trans)
qed
hence basis_ortho: "∀b ∈ ?𝒱_basis. inner_prod (col U j) b = 0"
using j_gr_k corthogonal_matD[OF U_ortho _ j] by fast
obtain cs where "lincomb cs ?𝒱_basis = v"
using "**" 𝒱_def 𝒱_basis_dim finite_in_span by blast
hence "inner_prod (col U j) v = (∑b∈?𝒱_basis. cs b * inner_prod (col U j) b)"
by (smt (verit, best) A_decomp List.finite_set R.add.finprod_cong' 𝒱_basis_dim carrier_matD(1) col_dim finsum_vec inner_prod_vec_sum lincomb_def v_dim)
thus ?thesis using basis_ortho by fastforce
qed
hence "conjugate (col U j) ∙ v = 0"
by (metis A_decomp carrier_matD(1) col_dim conjugate_vec_sprod_comm v_dim)
hence "row U⇧H j ∙ v = 0"
by (metis "*" adjoint_dim_row adjoint_is_conjugate_transpose adjoint_row carrier_vecD dim_mult_mat_vec lessThan_iff x_def x_dim)
hence "x$j = 0"
unfolding x_def
by (metis "*" carrier_vecD dim_mult_mat_vec index_mult_mat_vec lessThan_iff x_def x_dim)
thus ?thesis by fastforce
qed
qed
have "es_R!k = es!k"
by (metis A_decomp assms(2) carrier_matD(1) diag_mat_length es_R length_map nth_map)
also have "... = es!k * (∑j ∈ {..<n}. (cmod (x$j))^2)"
by (simp add: weights)
also have "... = (∑j ∈ {..<n}. es!k * (cmod (x$j))^2)"
by (simp add: mult_hom.hom_sum)
also have "... ≤ (∑j ∈ {..<n}. es!j * (cmod (x$j))^2)"
by (meson ineq sum_mono)
also have "... = ρ A v"
using unit_vec_rayleigh_formula A_decomp *** v_dim x_def by fastforce
finally show "?geq v" by (simp add: less_eq_complex_def)
qed
ultimately show ?thesis by blast
qed
theorem courant_fischer_maximin:
assumes "n > 0"
assumes "k < n"
shows "es!k = maximin (k + 1)"
"maximin_defined (k + 1)"
proof-
have "inverts_mat U (adjoint U)"
using A_decomp
unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def similar_mat_wit_def
by (metis Complex_Matrix.unitary_def)
hence U_invertible: "invertible_mat U"
by (metis A_decomp Complex_Matrix.unitary_def carrier_matD(1) carrier_matD(2) invertible_mat_def square_mat.simps unitaryD2)
have "unitary U"
using A_decomp
unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def
by blast
hence U_ortho: "corthogonal_mat U" using unitary_is_corthogonal A_decomp by auto
define es_R where "es_R ≡ map Re es"
have "set es ⊆ Reals" by (simp add: A_decomp)
hence es_R: "map complex_of_real es_R = es"
proof-
{ fix i assume *: "i < length es"
hence "es!i ∈ Reals" using A_decomp by auto
hence "complex_of_real (es_R!i) = es!i" by (simp add: * es_R_def)
}
thus ?thesis by (simp add: es_R_def map_nth_eq_conv)
qed
hence es_R_i: "⋀i. i ∈ {..<n} ⟹ es_R!i = Re (es!i)"
using dim_is eigvals eigvals_poly_length es_R_def by simp
hence es_R_k: "es_R!k = Re (es!k)" by (simp add: assms(2))
let ?leq = "λv. ρ A v ≤ es_R!k"
let ?geq = "λv. ρ A v ≥ es_R!k"
let ?P = "λ𝒱 v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1"
let ?Q = "λ𝒱. dimensional 𝒱 (k + 1)"
let ?S⇩ρ = "λ𝒱. {ρ A v |v. ?P 𝒱 v}"
have 1: "⋀𝒱. ?Q 𝒱 ⟹ (∃v. ?P 𝒱 v ∧ ?leq v)"
by (metis Re_complex_of_real courant_fischer.courant_fischer_unit_rayleigh_helper2 courant_fischer_axioms es_R_k less_eq_complex_def)
have 2: "∃𝒱. ?Q 𝒱 ∧ (∀v. ?P 𝒱 v ⟶ ?geq v)"
using courant_fischer_unit_rayleigh_helper3[OF assms(1) assms(2) eigvals]
unfolding es_R_def
by blast
from 2 obtain 𝒱' where 𝒱': "?Q 𝒱' ∧ (∀v. ?P 𝒱' v ⟶ ?geq v)" by blast
from this 1 obtain v' where v': "?P 𝒱' v' ∧ ?leq v'" by presburger
moreover have all_v_geq: "∀v. ?P 𝒱' v ⟶ ?geq v" using 𝒱' by blast
ultimately have "ρ A v' = es_R!k" by fastforce
hence "es_R!k ∈ ?S⇩ρ 𝒱'" using v' by fastforce
moreover have "∀x ∈ ?S⇩ρ 𝒱'. x ≥ es_R!k" using all_v_geq by blast
ultimately have "es_R!k = Inf (?S⇩ρ 𝒱')" by (smt (verit) rayleigh_bdd_below cInf_eq_minimum)
moreover have "⋀𝒱. ?Q 𝒱 ⟹ Inf (?S⇩ρ 𝒱) ≤ es_R!k"
proof-
fix 𝒱
assume *: "?Q 𝒱"
then obtain v where v: "?P 𝒱 v ∧ ?leq v" using 1 by presburger
then have "ρ A v ∈ ?S⇩ρ 𝒱" by blast
then have "Inf (?S⇩ρ 𝒱) ≤ ρ A v"
using rayleigh_min_exists[OF *] assms(2) rayleigh_min courant_fischer_axioms by auto
thus "Inf (?S⇩ρ 𝒱) ≤ es_R!k" using v by linarith
qed
ultimately have *: "es_R!k ∈ {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱} ∧ (∀x ∈ {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱}. x ≤ es_R!k)"
using 𝒱' by blast
hence "Sup {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱} = es_R!k" by (meson cSup_eq_maximum)
moreover have "Sup {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱} = maximin (k + 1)"
unfolding maximin_def rayleigh_min dimensional_def by blast
ultimately show "es!k = maximin (k + 1)"
by (metis A_decomp assms(2) carrier_matD(1) diag_mat_length es_R length_map nth_map)
show "maximin_defined (k + 1)"
using * unfolding maximin_defined_def sup_defined_def rayleigh_min bdd_above_def by blast
qed
end
lemma courant_fischer_maximin:
fixes A :: "complex mat"
assumes "n > 0"
assumes "k < n"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A es"
assumes "sorted_wrt (≥) es"
shows "es!k = hermitian_mat.maximin n A (k + 1)" "hermitian_mat.maximin_defined n A (k + 1)"
proof-
obtain Λ U where "real_diag_decomp A Λ U
∧ diag_mat Λ = es
∧ set es ⊆ Reals
∧ U ∈ carrier_mat n n
∧ Λ ∈ carrier_mat n n"
by (metis hermitian_real_diag_decomp_eigvals assms(3-5))
then interpret cf: courant_fischer A n Λ U es
using assms by unfold_locales
show "es!k = hermitian_mat.maximin n A (k + 1)"
using cf.courant_fischer_maximin(1)[OF assms(1) assms(2)] .
show "hermitian_mat.maximin_defined n A (k + 1)"
using cf.courant_fischer_maximin(2)[OF assms(1) assms(2)] .
qed
lemma maximin_minimax:
fixes A :: "complex mat"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "k < n"
shows "hermitian_mat.maximin n (-A) (n - k) = - hermitian_mat.minimax n A (k + 1)"
"hermitian_mat.maximin_defined n (-A) (n - k) ⟹ hermitian_mat.minimax_defined n A (k + 1)"
proof-
interpret hm: hermitian_mat n A using assms by unfold_locales
interpret hm': hermitian_mat n "-A"
using assms by (simp add: hermitian_mat.intro negative_hermitian)
define P where "P ≡ λv 𝒱. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1"
define Q where "Q ≡ λ𝒱. hm'.dimensional 𝒱 (n - k)"
have "Inf {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = - Sup (uminus`{Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱})"
using Inf_real_def .
moreover have *: "uminus`{Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = {- Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}"
by blast
moreover have **: "{- Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = {Inf {ρ (-A) v |v. P v 𝒱} |𝒱. Q 𝒱}"
proof-
have "⋀𝒱. Q 𝒱 ⟹ - Sup {ρ A v |v. P v 𝒱} = Inf {ρ (-A) v |v. P v 𝒱}"
proof-
fix 𝒱 assume *: "Q 𝒱"
have "Inf {ρ (-A) v |v. P v 𝒱} = - Sup (uminus`{ρ (-A) v |v. P v 𝒱})"
using Inf_real_def by fast
moreover have "uminus`{ρ (-A) v |v. P v 𝒱} = {- ρ (-A) v |v. P v 𝒱}" by blast
moreover have "{- ρ (-A) v |v. P v 𝒱} = {ρ A v |v. P v 𝒱}"
proof-
have "⋀v. P v 𝒱 ⟹ - ρ (- A) v = ρ A v"
by (metis * P_def Q_def assms(1) hm.dimensional_n_vec rayleigh_quotient_negative)
thus ?thesis by metis
qed
ultimately show "- Sup {ρ A v |v. P v 𝒱} = Inf {ρ (-A) v |v. P v 𝒱}" by presburger
qed
thus ?thesis by force
qed
ultimately have "- Inf {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = Sup {Inf {ρ (-A) v |v. P v 𝒱} |𝒱. Q 𝒱}"
by auto
moreover have "n - (k + 1) + 1 = n - k" using assms(3) by fastforce
ultimately show "hermitian_mat.maximin n (-A) (n - k) = - hermitian_mat.minimax n A (k + 1)"
by (simp add: hm.minimax_def hm'.maximin_def hm'.rayleigh_min hm.rayleigh_max P_def Q_def)
show "hermitian_mat.minimax_defined n A (k + 1)" if "hermitian_mat.maximin_defined n (-A) (n - k)"
proof-
have "{Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} ≠ {}"
using that
unfolding hm'.maximin_defined_def sup_defined_def hm'.rayleigh_min P_def Q_def
by fast
moreover have "bdd_below {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}"
proof-
have "bdd_above {Inf {ρ (-A) v |v. P v 𝒱} |𝒱. Q 𝒱}"
using that
unfolding hm'.maximin_defined_def sup_defined_def hm'.rayleigh_min P_def Q_def
by argo
hence "bdd_above {- Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}" using ** by argo
hence "bdd_below {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}" by (smt (verit, best) * bdd_above_uminus)
thus ?thesis by blast
qed
moreover have "n - k = n - (k + 1) + 1" using assms(3) by simp
ultimately show ?thesis
unfolding hm.minimax_defined_def inf_defined_def hm.rayleigh_max P_def Q_def by algebra
qed
qed
lemma courant_fischer_minimax:
fixes A :: "complex mat"
assumes "n > 0"
assumes "k < n"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A es"
assumes "sorted_wrt (≥) es"
shows "es!k = hermitian_mat.minimax n A (k + 1)"
"hermitian_mat.minimax_defined n A (k + 1)"
proof-
define A' where "A' ≡ - A"
define es' where "es' = rev (map (λx. -x) es)"
have A'_hermitian: "hermitian A'" using negative_hermitian A'_def assms by blast
moreover have "eigvals_of A' es'"
using neg_mat_eigvals A'_def assms(3) assms(5) es'_def by blast
moreover have A'_dim: "A' ∈ carrier_mat n n" by (simp add: A'_def assms(3))
moreover have "sorted_wrt (≥) es'"
proof-
let ?l = "(map (λx. -x) es)"
{ fix i j assume "i < j" "j < length ?l"
moreover then have "es!i ≥ es!j" using assms(6) sorted_wrt_iff_nth_less[of "(≥)" es] by force
ultimately have "?l!i ≤ ?l!j" by simp
}
hence "sorted_wrt (≤) ?l" by (metis sorted_wrt_iff_nth_less)
thus ?thesis by (simp add: sorted_wrt_rev es'_def)
qed
ultimately have *: "es'!(n - k - 1) = hermitian_mat.maximin n A' (n - k)
∧ hermitian_mat.maximin_defined n A' (n - k)"
using courant_fischer_maximin[of n "n - k - 1" A' es'] assms by (simp add: Suc_diff_Suc)
moreover have "es!k = - es'!(n - k - 1)"
proof-
have "n - k - 1 < length es" using assms(2) assms(3) assms(5) eigvals_poly_length by force
moreover have "length es = n"
using assms(3) assms(5) by auto
ultimately have "es!k = (rev es)!(n - k - 1)"
using rev_nth[of "n - k - 1" es] by (simp add: Suc_diff_Suc assms(2) le_simps(1))
also have "... = rev (map (λx. -x) (map (λx. -x) es))!(n - k - 1)"
by simp
also have "... = - es'!(n - k - 1)"
by (metis ‹n - k - 1 < length es› es'_def length_map length_rev nth_map rev_map)
finally show ?thesis .
qed
ultimately show "es!k = hermitian_mat.minimax n A (k + 1)"
"hermitian_mat.minimax_defined n A (k + 1)"
apply (simp add: A'_def assms(2) assms(3) assms(4) maximin_minimax(1))
using A'_def * assms(2) assms(3) assms(4) maximin_minimax(2) by blast
qed
subsection "Theorem Statement"
theorem courant_fischer:
fixes A :: "complex mat"
assumes "n > 0"
assumes "k < n"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A es"
assumes "sorted_wrt (≥) es"
shows "es!k = hermitian_mat.minimax n A (k + 1)"
"es!k = hermitian_mat.maximin n A (k + 1)"
"hermitian_mat.minimax_defined n A (k + 1)"
"hermitian_mat.maximin_defined n A (k + 1)"
using assms courant_fischer_minimax apply algebra
using assms courant_fischer_maximin apply algebra
using assms courant_fischer_minimax apply algebra
using assms courant_fischer_maximin by algebra
section "Cauchy Eigenvalue Interlacing Theorem"
text
"We follow the proof given in this set of lecture notes by Dr. David Bindel:
https://www.cs.cornell.edu/courses/cs6210/2019fa/lec/2019-11-04.pdf"
subsection "Theorem Statement and Proof"
theorem cauchy_eigval_interlacing:
fixes A W :: "complex mat"
assumes "n > 0"
assumes "j < n"
assumes "m ≤ n"
assumes "m > 0"
assumes "j < m"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A α"
assumes "sorted_wrt (≥) α"
assumes "W ∈ carrier_mat n m"
assumes "W⇧H * W = 1⇩m m"
assumes "inj_on (λv. W *⇩v v) (carrier_vec m)"
defines "B ≡ W⇧H * A * W"
assumes "eigvals_of B β"
assumes "sorted_wrt (≥) β"
shows "α!(n-m+j) ≤ β!j" "β!j ≤ α!j"
proof-
interpret A: hermitian_mat n A using assms hermitian_mat_def by presburger
interpret B: hermitian_mat m B
proof unfold_locales
show "B ∈ carrier_mat m m" unfolding B_def using assms by fastforce
show "hermitian B"
proof-
have "B⇧H = (W⇧H * A * W)⇧H" unfolding B_def by blast
also have "... = W⇧H * A * (W⇧H)⇧H"
by (smt (verit, ccfv_threshold) assms adjoint_dim' adjoint_is_conjugate_transpose adjoint_mult assoc_mult_mat hermitian_def mult_carrier_mat)
also have "... = W⇧H * A * W" by (simp add: transpose_conjugate)
also have "... = B" unfolding B_def by blast
finally show ?thesis by (simp add: adjoint_is_conjugate_transpose hermitian_def)
qed
qed
have α: "∀k < n. α!k = hermitian_mat.minimax n A (k + 1)
∧ α!k = hermitian_mat.maximin n A (k + 1)
∧ hermitian_mat.minimax_defined n A (k + 1)
∧ hermitian_mat.maximin_defined n A (k + 1)"
using courant_fischer assms by presburger
let ?lhs = "λ𝒱. {ρ B v |v. v ≠ 0⇩v m ∧ v ∈ 𝒱 ∧ vec_norm v = 1}"
let ?rhs = "λ𝒱. {ρ A v |v. v ≠ 0⇩v n ∧ v ∈ (*⇩v) W ` 𝒱 ∧ vec_norm v = 1}"
have rayleigh_sets_eq: "⋀𝒱 k. B.dimensional 𝒱 k ⟹ ?lhs 𝒱 = ?rhs 𝒱"
proof-
fix 𝒱 k assume *: "B.dimensional 𝒱 k"
have "?lhs 𝒱 ⊆ ?rhs 𝒱"
proof
let ?lhs = "?lhs 𝒱"
let ?rhs = "?rhs 𝒱"
fix x assume **: "x ∈ ?lhs"
then obtain v where v: "v ≠ 0⇩v m ∧ v ∈ 𝒱 ∧ vec_norm v = 1 ∧ x = ρ B v" by blast
let ?c = "1 / (vec_norm (W *⇩v v))"
define v' where "v' ≡ ?c ⋅⇩v (W *⇩v v)"
have "ρ⇩c B v = ((B *⇩v v) ∙c v) / (v ∙c v)" by simp
also have "... = ((W⇧H *⇩v (A * W *⇩v v)) ∙c v) / (v ∙c v)"
unfolding assms(9)
by (smt (verit, best) assms "*" A.dim_is B.dimensional_n_vec More_Matrix.carrier_vec_conjugate assoc_mult_mat assoc_mult_mat_vec carrier_vecD dim_mult_mat_vec hermitian_def index_mult_mat(2) mult_carrier_mat transpose_carrier_mat v)
also have "... = ((A * W *⇩v v) ∙c (W *⇩v v)) / (v ∙c v)"
by (metis (no_types, lifting) assms(6,10) "*" A.dim_is B.hermitian_mat_axioms cscalar_prod_conjugate_transpose hermitian_mat.dimensional_n_vec mult_carrier_mat mult_mat_vec_carrier v)
also have "... = ((A * W *⇩v v) ∙c (W *⇩v v)) / (v ∙c ((1⇩m m) *⇩v v))"
using "*" v B.dimensional_n_vec by force
also have "... = ((A *⇩v (W *⇩v v)) ∙c (W *⇩v v)) / (v ∙c (W⇧H *⇩v (W *⇩v v)))"
by (metis "*" assms(6,10,11) B.dimensional_n_vec adjoint_dim' adjoint_is_conjugate_transpose assoc_mult_mat_vec v)
also have "... = ((A *⇩v (W *⇩v v)) ∙c (W *⇩v v)) / ((W *⇩v v) ∙c ((W *⇩v v)))"
by (metis "*" assms(10) B.dimensional_n_vec adjoint_def_alter adjoint_is_conjugate_transpose mult_mat_vec_carrier v)
also have "... = ρ⇩c A (W *⇩v v)" by simp
finally have "ρ B v = ρ A (W *⇩v v)" by fastforce
also have "... = ρ A v'"
unfolding v'_def
by (smt (verit, best) assms(6,10,11) "*" rayleigh_quotient_scale B.hermitian_mat_axioms adjoint_is_conjugate_transpose div_by_1 hermitian_mat.dimensional_n_vec inner_prod_mult_mat_vec_right mult_mat_vec_carrier of_real_hom.hom_one one_mult_mat_vec v vec_norm_def)
finally have "x = ρ A v'" using v by fast
moreover have "vec_norm v' = 1"
by (smt (verit, ccfv_threshold) assms(10,11) "*" B.dimensional_n_vec adjoint_dim' adjoint_is_conjugate_transpose assoc_mult_mat_vec carrier_matD(1) cscalar_prod_adjoint dim_mult_mat_vec div_by_1 one_mult_mat_vec scalar_vec_one v v'_def vec_norm_def)
moreover have "v' ∈ (*⇩v) W ` 𝒱"
by (smt (z3) assms(10,11) "*" B.dimensional_n_vec Setcompr_eq_image adjoint_is_conjugate_transpose div_by_1 inner_prod_mult_mat_vec_left mem_Collect_eq one_mult_mat_vec one_smult_vec v v'_def vec_norm_def)
moreover have "v' ≠ 0⇩v n"
by (metis A.add.one_closed calculation(2) one_neq_zero vec_norm_zero)
ultimately show "x ∈ ?rhs" by blast
qed
moreover have "?rhs 𝒱 ⊆ ?lhs 𝒱"
proof
let ?lhs = "?lhs 𝒱"
let ?rhs = "?rhs 𝒱"
fix x assume **: "x ∈ ?rhs"
then obtain v' where v': "v' ≠ 0⇩v n ∧ v' ∈ (*⇩v) W ` 𝒱 ∧ vec_norm v' = 1 ∧ x = ρ A v'" by blast
then obtain u where u: "W *⇩v u = v' ∧ u ≠ 0⇩v m ∧ u ∈ 𝒱"
by (smt (verit, ccfv_threshold) assms(6,10,11) B.dimensional_n B.smult_l_null Setcompr_eq_image * adjoint_is_conjugate_transpose assms(15) assms(7) csqrt_1 inner_prod_mult_mat_vec_left inner_prod_smult_left_right mem_Collect_eq mult_eq_0_iff one_mult_mat_vec one_neq_zero power2_csqrt subset_eq vec_norm_def)
hence u_m: "u ∈ carrier_vec m" using "*" B.dimensional_n_vec by blast
let ?c = "1 / vec_norm u"
define v where "v ≡ ?c ⋅⇩v u"
have "ρ⇩c B v = ((B *⇩v v) ∙c v) / (v ∙c v)" by simp
also have "... = ((W⇧H *⇩v (A * W *⇩v v)) ∙c v) / (v ∙c v)"
unfolding assms(9)
by (smt (verit, ccfv_threshold) assms(6,10,11,13) u_m A.dim_is B.smult_one adjoint_is_conjugate_transpose adjoint_mult assms(15) assms(4) assms(7) cscalar_prod_conjugate_transpose divide_self_if hermitian_def inner_prod_mult_mat_vec_right mult_carrier_mat mult_mat_vec_carrier one_mult_mat_vec u v' v_def vec_norm_def)
also have "... = ((A * W *⇩v v) ∙c (W *⇩v v)) / (v ∙c v)"
by (smt (verit, ccfv_threshold) assms(6,10,11) "*" A.dim_is B.dimensional_n_vec Complex_Matrix.adjoint_adjoint adjoint_dim' adjoint_is_conjugate_transpose assms(7) carrier_matD(1) carrier_vecD cscalar_prod_adjoint dim_mult_mat_vec index_mult_mat(2) index_smult_vec(2) u v_def)
also have "... = ((A * W *⇩v v) ∙c (W *⇩v v)) / (v ∙c ((1⇩m m) *⇩v v))"
by (simp add: u_m v_def)
also have "... = ((A *⇩v (W *⇩v v)) ∙c (W *⇩v v)) / (v ∙c (W⇧H *⇩v (W *⇩v v)))"
by (metis assms(6,10,11) B.smult_one adjoint_dim' adjoint_is_conjugate_transpose assoc_mult_mat_vec div_by_1 inner_prod_mult_mat_vec_left one_mult_mat_vec u u_m v' v_def vec_norm_def)
also have "... = ((A *⇩v (W *⇩v v)) ∙c (W *⇩v v)) / ((W *⇩v v) ∙c ((W *⇩v v)))"
by (metis assms(10) B.smult_closed u_m v_def adjoint_def_alter adjoint_is_conjugate_transpose mult_mat_vec_carrier)
also have "... = ρ⇩c A (W *⇩v v)" by simp
finally have "ρ B v = ρ A (W *⇩v v)" by fastforce
also have "... = ρ A (W *⇩v (?c ⋅⇩v u))" using v_def by blast
also have "... = ρ A (?c ⋅⇩v (W *⇩v u))" by (metis assms(10) mult_mat_vec u u_m)
also have "... = ρ A v'"
by (metis assms(10,11) u_m adjoint_is_conjugate_transpose div_by_1 inner_prod_mult_mat_vec_left one_mult_mat_vec one_smult_vec u v' vec_norm_def)
finally have "x = ρ B v" using v' by presburger
moreover have "vec_norm v = 1"
by (metis carrier_dim_vec csqrt_1 normalized_vec_norm u u_m v_def vec_norm_def vec_normalize_def)
moreover then have "v ≠ 0⇩v m" using vec_norm_zero by force
moreover have "v ∈ 𝒱"
by (metis assms(10,11) B.smult_one adjoint_is_conjugate_transpose div_by_1 inner_prod_mult_mat_vec_right one_mult_mat_vec u u_m v' v_def vec_norm_def)
ultimately show "x ∈ ?lhs" by blast
qed
ultimately show "?lhs 𝒱 = ?rhs 𝒱" by blast
qed
let ?lhs_min = "λk. {A.rayleigh_min ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 k}"
let ?rhs_min = "λk. {A.rayleigh_min 𝒱 | 𝒱. A.dimensional 𝒱 k}"
let ?lhs_max = "λk. {A.rayleigh_max ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 k}"
let ?rhs_max = "λk. {A.rayleigh_max 𝒱 | 𝒱. A.dimensional 𝒱 k}"
have rayleigh_sets_eq': "⋀k. ?lhs_min k ⊆ ?rhs_min k" "⋀k. ?lhs_max k ⊆ ?rhs_max k"
proof-
fix k
have *: "{(λv. W *⇩v v)`𝒱 | 𝒱. B.dimensional 𝒱 k} ⊆ {𝒱 | 𝒱. A.dimensional 𝒱 k}"
proof(rule subsetI)
fix 𝒱 assume *: "𝒱 ∈ {(λv. W *⇩v v)`𝒱 | 𝒱. B.dimensional 𝒱 k}"
have "A.dimensional 𝒱 k"
proof-
let ?f = "λv. W *⇩v v"
obtain 𝒱' where 𝒱': "𝒱 = ?f`𝒱' ∧ B.dimensional 𝒱' k" using * by blast
then obtain vs' where vs': "𝒱' = B.span vs'
∧ card vs' = k
∧ vs' ⊆ carrier_vec m
∧ B.lin_indpt vs'"
unfolding B.dimensional_def by presburger
define vs where "vs = ?f`vs'"
interpret W: linear_map
class_ring
"(module_vec TYPE(complex) m)"
"(module_vec TYPE(complex) n)"
"(λv. W *⇩v v)"
using linear_map_mat[OF assms(10)] .
have inj: "inj_on ?f (carrier B.V)" using assms(12) by fastforce
have 1: "vs' ⊆ carrier B.V" using B.cV vs' by argo
have "𝒱 = A.span vs" using W.image_span by (simp add: B.li_le_dim(1) 𝒱' vs' vs_def)
moreover have "card vs = k"
proof-
have "card vs' = k" using vs' by blast
moreover have "vs' ⊆ carrier B.V" by (simp add: vs')
ultimately show ?thesis by (metis inj card_image subset_inj_on vs_def)
qed
moreover have "vs ⊆ carrier_vec n"
proof(rule subsetI)
fix v assume "v ∈ vs"
then obtain v' where "v' ∈ vs' ∧ ?f v' = v" using vs_def by blast
thus "v ∈ carrier_vec n" using assms(10) mult_mat_vec_carrier vs' by blast
qed
moreover have "A.lin_indpt vs"
using W.inj_image_lin_indpt[OF inj] vs' vs_def B.fin_dim_li_fin by auto
ultimately show ?thesis unfolding A.dimensional_def by blast
qed
thus "𝒱 ∈ {𝒱 | 𝒱. A.dimensional 𝒱 k}" by blast
qed
from * show "?lhs_min k ⊆ ?rhs_min k" by blast
from * show "?lhs_max k ⊆ ?rhs_max k" by blast
qed
have "β!j = B.maximin (j + 1)"
using courant_fischer(2)[OF assms(4,5) B.dim_is B.is_herm assms(14,15)] .
also have "... = Sup {A.rayleigh_min ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 (j + 1)}"
unfolding B.maximin_def B.rayleigh_min A.rayleigh_min
by (metis (no_types, lifting) rayleigh_sets_eq)
also have "... ≤ α!j"
proof-
let ?lhs = "{A.rayleigh_min ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 (j + 1)}"
let ?rhs = "{A.rayleigh_min 𝒱 | 𝒱. A.dimensional 𝒱 (j + 1)}"
have α⇩j: "α!j = A.maximin (j + 1)"
using courant_fischer(2)[OF assms(1,2,6,7,8,9)] by argo
hence Re_α⇩j: "Re (α!j) = Sup ?rhs"
by (simp add: A.maximin_def image_Collect)
hence "?lhs ⊆ ?rhs" using rayleigh_sets_eq'(1) by presburger
moreover have "?lhs ≠ {}"
proof-
let ?vs = "set (take (j + 1) (unit_vecs m))"
have "B.dimensional (B.span ?vs) (j + 1)"
proof-
have "card ?vs = j + 1"
by (metis B.unit_vecs_distinct distinct_take B.unit_vecs_length Groups.add_ac(2) One_nat_def Suc_leI add_0_right add_Suc_right assms(5) diff_zero distinct_card length_take length_upt take_upt)
moreover have "B.lin_indpt ?vs"
by (meson B.basis_def B.supset_ld_is_ld B.unit_vecs_basis set_take_subset)
moreover have "?vs ⊆ carrier_vec m"
by (meson in_set_takeD subset_code(1) unit_vecs_carrier)
ultimately show ?thesis unfolding B.dimensional_def by blast
qed
thus ?thesis by blast
qed
moreover have "bdd_above ?rhs"
using α
by (simp add: A.maximin_defined_def assms(2) sup_defined_def)
ultimately have "Sup ?lhs ≤ Sup ?rhs" by (meson cSup_subset_mono)
thus ?thesis using Re_α⇩j α⇩j less_eq_complex_def by force
qed
finally show "β!j ≤ α!j" .
let ?j' = "n - m + j"
have j'_le: "?j' < n" using assms by linarith
hence j'_eq: "n - ?j' + 1 = m - j + 1" using assms(3) by force
have "α!?j' = A.minimax (?j' + 1)" using courant_fischer(1)[OF assms(1) j'_le assms(6,7,8,9)] .
also have "... ≤ Inf {A.rayleigh_max ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 (n - ?j')}"
proof-
let ?rhs = "{A.rayleigh_max ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 (n - ?j')}"
let ?lhs = "{A.rayleigh_max 𝒱 | 𝒱. A.dimensional 𝒱 (n - ?j')}"
have "?rhs ⊆ ?lhs" using rayleigh_sets_eq'(2) by presburger
moreover have "?rhs ≠ {}"
proof-
let ?vs = "set (take (n - ?j') (unit_vecs m))"
have "B.dimensional (B.span ?vs) (n - ?j')"
proof-
have "card ?vs = n - ?j'"
by (metis B.unit_vecs_distinct distinct_take B.unit_vecs_length Groups.add_ac(2) One_nat_def add_Suc_right diff_zero distinct_card length_take length_upt take_upt diff_add_inverse2 diff_le_self j'_eq)
moreover have "B.lin_indpt ?vs"
by (meson B.basis_def B.supset_ld_is_ld B.unit_vecs_basis set_take_subset)
moreover have "?vs ⊆ carrier_vec m"
by (meson in_set_takeD subset_code(1) unit_vecs_carrier)
ultimately show ?thesis unfolding B.dimensional_def by blast
qed
thus ?thesis by blast
qed
moreover have "bdd_below ?lhs"
proof-
have "n - m + j < n" using j'_le by blast
moreover then have "n - ((n - m + j) + 1) + 1 = n - (n - m + j)" by linarith
ultimately show ?thesis
using α
unfolding A.minimax_defined_def inf_defined_def
by (smt (verit, del_insts) Collect_cong)
qed
ultimately have "Inf ?lhs ≤ Inf ?rhs"
using cInf_superset_mono[of ?rhs ?lhs] by fast
moreover have "n - (n - m + j) = n - (n - m + j + 1) + 1" using assms by linarith
ultimately show ?thesis by (simp add: less_eq_complex_def A.minimax_def)
qed
also have "... = Inf {A.rayleigh_max ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 (m - j)}"
using assms(3) by force
also have "... = B.minimax (j + 1)"
proof-
have "m - j = m - (j + 1) + 1" by (simp add: Suc_diff_Suc assms(5))
thus ?thesis
unfolding B.minimax_def B.rayleigh_max A.rayleigh_max
by (metis (mono_tags, lifting) rayleigh_sets_eq)
qed
also have "... = β!j"
using courant_fischer(1)[OF assms(4,5) B.dim_is B.is_herm assms(14,15)] by argo
finally show "α!(n - m + j) ≤ β!j" .
qed
corollary cauchy_eigval_interlacing_alt:
fixes A W :: "complex mat"
assumes "n > 0"
assumes "j < n"
assumes "m ≤ n"
assumes "m > 0"
assumes "j < m"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A α"
assumes "sorted_wrt (≥) α"
assumes "W ∈ carrier_mat n m"
assumes "W⇧H * W = 1⇩m m"
assumes "inj_on (λv. W *⇩v v) (carrier_vec m)"
defines "B ≡ W⇧H * A * W"
assumes "eigvals_of B β"
assumes "sorted_wrt (≥) β"
shows "β!j ∈ {α!(n-m+j)..α!j}"
using cauchy_eigval_interlacing assms by presburger
subsection "Principal Submatrix Corollaries"
corollary ps_eigval_interlacing:
fixes A :: "complex mat"
fixes k
assumes "n > 0"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A α"
assumes "sorted_wrt (≥) α"
assumes "I ⊆ {..<n}"
assumes "I ≠ {}"
defines "B ≡ submatrix A I I"
defines "m ≡ card I"
assumes "eigvals_of B β"
assumes "sorted_wrt (≥) β"
assumes "j < m"
shows "α!(n-m+j) ≤ β!j" "β!j ≤ α!j"
proof-
have 0: "n > 0" using assms(1) .
have 1: "j < n"
by (metis assms(6,12) card_lessThan card_mono finite_lessThan m_def not_le not_less_iff_gr_or_eq order.strict_trans)
have 2: "m ≤ n"
using assms(6,9) atLeast0LessThan subset_eq_atLeast0_lessThan_card by presburger
have 3: "m > 0" using assms(12) by linarith
have 4: "j < m" using assms(12) .
have 5: "A ∈ carrier_mat n n" using assms(2) .
have 6: "hermitian A" using assms(3) .
have 7: "eigvals_of A α" using assms(4) .
have 8: "sorted_wrt (≥) α" using assms(5) .
obtain Inm where Inm:
"B = Inm⇧H * A * Inm"
"Inm⇧H * Inm = 1⇩m m"
"Inm ∈ carrier_mat n m"
"inj_on ((*⇩v) Inm) (carrier_vec m)"
using submatrix_as_matrix_prod_obt assms by blast
hence 9: "eigvals_of (Inm⇧H * A * Inm) β" using assms(10) by blast
have 10: "sorted_wrt (λx y. y ≤ x) β" by (simp add: assms(11))
have *: "β!j ∈ {α!(n-m+j)..α!j}"
using cauchy_eigval_interlacing_alt[OF 0 1 2 3 4 5 6 7 8 Inm(3,2,4) 9 10] .
from * show "α!(n-m+j) ≤ β!j" by presburger
from * show"β!j ≤ α!j" by presburger
qed
corollary ps_eigval_interlacing_alt:
fixes A :: "complex mat"
fixes k
assumes "n > 0"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A α"
assumes "sorted_wrt (≥) α"
assumes "I ⊆ {..<n}"
assumes "I ≠ {}"
defines "B ≡ submatrix A I I"
defines "m ≡ card I"
assumes "eigvals_of B β"
assumes "sorted_wrt (≥) β"
assumes "j < m"
shows "β!j ∈ {α!(n-m+j)..α!j}"
using ps_eigval_interlacing assms by presburger
subsection "Leading Principal Submatrix Corollaries"
corollary lps_eigval_interlacing:
fixes A :: "complex mat"
fixes k
assumes "n > 0"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A α"
assumes "sorted_wrt (≥) α"
assumes "0 < m"
assumes "m ≤ n"
defines "B ≡ lps A m"
assumes "eigvals_of B β"
assumes "sorted_wrt (≥) β"
assumes "j < m"
shows "α!(n-m+j) ≤ β!j" "β!j ≤ α!j"
using ps_eigval_interlacing(1)[OF assms(1,2,3,4,5), of "{..<m}"] assms apply auto[1]
using ps_eigval_interlacing(2)[OF assms(1,2,3,4,5), of "{..<m}"] assms by auto
corollary lps_eigval_interlacing_alt:
fixes A :: "complex mat"
fixes k
assumes "n > 0"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A α"
assumes "sorted_wrt (≥) α"
assumes "0 < m"
assumes "m ≤ n"
defines "B ≡ lps A m"
assumes "eigvals_of B β"
assumes "sorted_wrt (≥) β"
assumes "j < m"
shows "β!j ∈ {α!(n-m+j)..α!j}"
using lps_eigval_interlacing assms by presburger
end