Theory Misc_Matrix_Results
theory Misc_Matrix_Results
imports "Commuting_Hermitian.Commuting_Hermitian"
"BenOr_Kozen_Reif.More_Matrix"
"Jordan_Normal_Form.Spectral_Radius"
"Jordan_Normal_Form.DL_Rank_Submatrix"
"Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness"
"Jordan_Normal_Form.VS_Connect"
"QHLProver.Complex_Matrix"
"Fishers_Inequality.Matrix_Vector_Extras"
"Complex_Bounded_Operators.Extra_Jordan_Normal_Form"
"Hermite_Lindemann.Misc_HLW"
begin
hide_type (open)
Finite_Cartesian_Product.vec
Matrix_Legacy.vec
Matrix_Legacy.mat
hide_fact (open)
Matrix_Legacy.mat_def
Finite_Cartesian_Product.mat_def
Finite_Cartesian_Product.row_def
Matrix_Legacy.row_def
Matrix_Legacy.row_def
Matrix_Legacy.col_def
Determinants.det_def
Determinants.det_def
Finite_Cartesian_Product.vec_def
Matrix_Legacy.vec_def
Linear_Algebra.adjoint_def
hide_const (open)
Matrix_Legacy.mat
Finite_Cartesian_Product.mat
Finite_Cartesian_Product.row
Matrix_Legacy.row
Matrix_Legacy.row
Matrix_Legacy.col
Determinants.det
Determinants.det
Finite_Cartesian_Product.vec
Matrix_Legacy.vec
Linear_Algebra.adjoint
no_notation fps_nth (infixl "$" 75)
unbundle no inner_syntax
unbundle no vec_syntax
hide_const (open) Spectral_Radius.spectrum
hide_fact (open) Spectral_Radius.spectrum_def
section "Polynomial Factorization"
lemma idom_poly_factor_unique_aux:
fixes rs rs' :: "'a::idom list"
assumes eq: "(∏a←rs. [:a, 1:]) = (∏a←rs'. [:a, 1:])"
shows "mset rs ⊆# mset rs'"
using eq
by (metis count_list_eq_length_filter count_mset poly_linear_exp_linear_factors
poly_linear_exp_linear_factors_rev subseteq_mset_def)
lemma idom_poly_factor_unique:
fixes rs rs' :: "'a::idom list"
assumes eq: "(∏a←rs. [:a, 1:]) = (∏a←rs'. [:a, 1:])"
shows "mset rs = mset rs'"
using idom_poly_factor_unique_aux[OF eq] idom_poly_factor_unique_aux[OF eq[symmetric]]
by order
lemma idom_poly_factor_unique':
fixes rs rs' :: "'a::idom list"
assumes eq: "(∏a←rs. [:- a, 1:]) = (∏a←rs'. [:- a, 1:])"
shows "mset rs = mset rs'"
proof-
have "(∏a←rs. [:- a, 1:]) = (∏a←(map uminus rs). [:a, 1:])"
by (simp add: o_def pCons_def)
moreover have "(∏a←rs'. [:- a, 1:]) = (∏a←(map uminus rs'). [:a, 1:])"
by (simp add: o_def pCons_def)
ultimately have "mset (map uminus rs) = mset (map uminus rs')"
using idom_poly_factor_unique[of "map uminus rs" "map uminus rs'"] eq by argo
moreover have "mset (map uminus (map uminus (as::'a list))) = mset as" for as by simp
ultimately show ?thesis using mset_map by metis
qed
section "Vector Normalization"
lemma vec_normalize_norm: "v ∈ carrier_vec n ⟹ v ≠ 0⇩v n ⟹ vec_norm (vec_normalize v) = 1"
by (simp add: normalized_vec_norm vec_norm_def)
section "Determinant, Invertability, and Eigenvalues"
definition eigvals_of [simp]:
"eigvals_of M es ⟷ char_poly M = (∏a←es. [:- a, 1:]) ∧ length es = dim_row M"
lemma eigvals_of_mset_eq:
"eigvals_of (A::'a::idom mat) es ⟹ eigvals_of A es' ⟹ mset es = mset es'"
unfolding eigvals_of by (metis idom_poly_factor_unique')
lemma det_is_prod_of_eigenvalues:
fixes A :: "complex mat"
assumes "square_mat A"
shows "Determinant.det A = (∏e ← (eigvals A). e)"
proof-
define es where "es ≡ eigvals A"
define n where "n ≡ dim_row A"
have 1: "A ∈ carrier_mat n n" using assms n_def by fastforce
have 2: "char_poly A = (∏e ← es. [:- e, 1:])"
unfolding es_def eigvals_def
using 1
by (metis (mono_tags, lifting) eigvals_poly_length someI_ex)
obtain Q Q' B where *: "similar_mat_wit A B Q Q' ∧ upper_triangular B ∧ diag_mat B = es"
using schur_decomposition[OF 1 2] by (metis surj_pair)
then have "Determinant.det A = Determinant.det (Q * B * Q')" unfolding similar_mat_wit_def by metis
also have "… = Determinant.det Q * Determinant.det B * Determinant.det Q'"
by (smt (verit, ccfv_SIG) "*" "1" det_mult mult_carrier_mat similar_mat_witD2(5) similar_mat_witD2(6) similar_mat_witD2(7))
also have "… = Determinant.det Q * Determinant.det B * 1/(Determinant.det Q)"
by (smt (verit, ccfv_threshold) "*" "1" det_mult det_one div_by_0 helper mult_cancel_left1 n_def nonzero_mult_div_cancel_left similar_mat_witD(6) similar_mat_witD(7) similar_mat_witD2(1))
also have "… = Determinant.det Q * (∏e ← diag_mat B. e) * 1/(Determinant.det Q)"
by (metis "*" det_upper_triangular list.map_ident similar_mat_witD(5))
also have "… = (∏e ← (eigvals A). e)"
by (metis (no_types, lifting) * es_def "1" Groups.mult_ac(2) class_field.zero_not_one det_mult det_one mult_cancel_left2 nonzero_mult_div_cancel_left similar_mat_witD(6) similar_mat_witD(7) similar_mat_witD2(2))
finally show ?thesis .
qed
lemma eigvals_of_spectrum:
"(A::(complex mat)) ∈ carrier_mat n n ⟹ eigvals_of A α ⟹ Spectral_Radius.spectrum A = set α"
unfolding eigvals_of
using eigenvalue_root_char_poly[of A n]
by (metis Spectral_Radius.spectrum_def equalityI linear_poly_root mem_Collect_eq root_poly_linear subsetI)
lemma spectrum_connect:
"(A::complex mat) ∈ carrier_mat n n ⟹ Spectral_Radius.spectrum A = spectrum A"
by (metis eigvals_of eigvals_of_spectrum eigvals_poly_length spectrum_def)
lemma spectrum_shift:
fixes A :: "complex mat"
assumes dim: "A ∈ carrier_mat n n"
shows "spectrum (A - r ⋅⇩m 1⇩m n) = {μ - r | μ. μ ∈ spectrum A}" (is "?lhs = ?rhs")
proof
{ let ?A' = "A - r ⋅⇩m 1⇩m n"
fix μ assume μ: "μ ∈ ?lhs"
then obtain v where v: "v ∈ carrier_vec n" "v ≠ 0⇩v n" "?A' *⇩v v = μ ⋅⇩v v"
by (metis (no_types, lifting) carrier_mat_triv eigenvalue_def eigenvector_def index_minus_mat(2,3)
index_one_mat(2,3) index_smult_mat(2,3) spectrum_eigenvalues)
hence "?A' *⇩v v = A *⇩v v - r ⋅⇩v v"
using dim
by (smt (verit, best) minus_mult_distrib_mat_vec one_carrier_mat one_mult_mat_vec
smult_carrier_mat smult_mat_mult_mat_vec_assoc)
hence "A *⇩v v = μ ⋅⇩v v + r ⋅⇩v v" using v(1,3) dim by auto
also have "… = (μ + r) ⋅⇩v v" using v(1) by (simp add: add_smult_distrib_vec)
finally have "μ + r ∈ spectrum A"
using spectrum_connect[OF dim] v(1,2) dim
by (metis Spectral_Radius.spectrum_def carrier_matD(1) eigenvalue_def eigenvector_def mem_Collect_eq)
hence "μ ∈ ?rhs" by force
}
thus "?lhs ⊆ ?rhs" by blast
next
{ let ?A' = "A - r ⋅⇩m 1⇩m n"
fix μ assume μ: "μ ∈ ?rhs"
then obtain μ' where μ': "μ = μ' - r" "μ' ∈ spectrum A" by blast
then obtain v where v: "v ∈ carrier_vec n" "v ≠ 0⇩v n" "A *⇩v v = μ' ⋅⇩v v"
using spectrum_connect[OF dim] dim
by (metis carrier_matD(1) eigenvalue_def eigenvector_def spectrum_eigenvalues)
have "?A' *⇩v v = A *⇩v v - r ⋅⇩v v"
using v(1) dim
by (smt (verit, del_insts) minus_mult_distrib_mat_vec one_carrier_mat one_mult_mat_vec
smult_carrier_mat smult_mat_mult_mat_vec_assoc)
also have "… = μ' ⋅⇩v v - r ⋅⇩v v" using v(3) by auto
also have "… = μ ⋅⇩v v" using dim v(1) μ'(1) by (simp add: minus_smult_vec_distrib)
finally have "μ ∈ spectrum ?A'"
using v(1,2) spectrum_connect[OF dim]
by (smt (verit) Spectral_Radius.spectrum_def carrier_mat_def eigenvalue_def eigenvector_def
index_minus_mat(2,3) index_one_mat(2,3) index_smult_mat(2,3) mem_Collect_eq spectrum_connect)
hence "μ ∈ ?lhs" by blast
}
thus "?rhs ⊆ ?lhs" by blast
qed
lemma trivial_kernel_imp_nonzero_eigenvalues:
fixes M :: "'a::{idom,ring_1_no_zero_divisors} mat"
assumes "square_mat M"
assumes "mat_kernel M ⊆ {0⇩v (dim_row M)}"
assumes "eigenvalue M e"
shows "e ≠ 0"
using assms by (metis (no_types, lifting) carrier_matI carrier_vecD eigenvalue_def eigenvector_def empty_iff mat_kernelI singleton_iff smult_vec_zero square_mat.simps subset_singletonD)
lemma trivial_kernel_imp_invertible:
fixes M :: "complex mat"
assumes "square_mat M"
assumes "mat_kernel M ⊆ {0⇩v (dim_row M)}"
shows "invertible_mat M"
using assms by (metis carrier_matI det_0_iff_vec_prod_zero_field empty_iff invertible_det mat_kernelI singletonD square_mat.elims(2) subset_singletonD)
lemma trivial_kernel_imp_det_nz:
fixes M :: "complex mat"
assumes "square_mat M"
assumes "mat_kernel M ⊆ {0⇩v (dim_row M)}"
shows "Determinant.det M ≠ 0"
using trivial_kernel_imp_invertible[OF assms(1) assms(2)]
using invertible_det assms(1) square_mat.simps
by blast
lemma similar_mats_eigvals:
assumes "A ∈ carrier_mat n n"
assumes "B ∈ carrier_mat n n"
assumes "similar_mat A B"
assumes "eigvals_of A es"
shows "eigvals_of B es"
using assms unfolding eigvals_of
by (metis (no_types) char_poly_similar assms(1-3) carrier_matD(1))
lemma scale_eigvals:
fixes A :: "'a::conjugatable_ordered_field mat"
assumes "square_mat A"
assumes "B = c ⋅⇩m A"
assumes "eigvals_of A es"
shows "eigvals_of B (map (λx. c * x) es)"
proof-
obtain A' P Q where A_decomp: "schur_decomposition A es = (A', P, Q)
∧ similar_mat_wit A A' P Q
∧ upper_triangular A'
∧ diag_mat A' = es"
using assms(1,3) unfolding eigvals_of square_mat.simps
by (metis carrier_mat_triv old.prod.exhaust schur_decomposition)
define B' where "B' ≡ c ⋅⇩m A'"
have B'_square: "square_mat B'" using A_decomp B'_def similar_mat_witD(5) by fastforce
have B_decomp: "similar_mat_wit B B' P Q ∧ upper_triangular B'"
proof-
have "upper_triangular B'"
proof-
{ fix i j assume *: "j < i" "i < dim_row B'"
hence "B'$$(i,j) = c * A'$$(i,j)" using B'_def B'_square by auto
also have "… = 0" using A_decomp * unfolding upper_triangular_def by (simp add: B'_def)
finally have "B'$$(i,j) = 0" .
}
thus ?thesis by blast
qed
moreover have "similar_mat_wit B B' P Q"
proof-
have "B = c ⋅⇩m (P * A' * Q)" using A_decomp assms(2) similar_mat_witD2(3) by blast
also have "… = P * (c ⋅⇩m A') * Q"
by (metis A_decomp similar_mat_wit_def similar_mat_wit_smult)
also have "… = P * B' * Q" using B'_def by argo
finally have "B = P * B' * Q" .
thus ?thesis by (smt (verit, best) A_decomp B'_def assms(2) similar_mat_wit_smult)
qed
ultimately show ?thesis by blast
qed
hence "char_poly B' = (∏a←diag_mat B'. [:- a, 1:])"
using char_poly_upper_triangular B_decomp B'_square by auto
moreover have "length (diag_mat B') = dim_row B'" by (simp add: diag_mat_length)
ultimately have "eigvals_of B' (diag_mat B')" using eigvals_of by blast
moreover have "diag_mat B' = map (λx. c * x) es"
using A_decomp B'_def by (metis diag_mat_map similar_mat_witD(5) smult_mat_def)
ultimately show ?thesis
using similar_mats_eigvals B_decomp assms(2) assms(3) char_poly_similar similar_mat_def
by fastforce
qed
lemma neg_mat_eigvals:
fixes A :: "complex mat"
assumes "square_mat A"
assumes "eigvals_of A es"
shows "eigvals_of (-A) (rev (map (λx. -x) es))"
proof-
have "eigvals_of A (rev es)"
using assms(2)
unfolding eigvals_of
by (metis length_rev prod_list.rev rev_map)
thus ?thesis
using scale_eigvals[of A "-A" "-1" "rev es"]
by (metis (lifting) ext assms(1) carrier_mat_triv mult_commute_abs mult_minus1_right rev_map square_mat.elims(2) uminus_mat)
qed
section "Quadratic Form"
definition quadratic_form :: "'a mat ⇒ 'a vec ⇒ 'a::{conjugatable_ring}" where
"quadratic_form M x ≡ inner_prod x (M *⇩v x)"
abbreviation "QF ≡ quadratic_form"
declare
quadratic_form_def[simp]
section "Leading Principal Submatrix"
definition leading_principal_submatrix :: "'a mat ⇒ nat ⇒ 'a mat" where
[simp]: "leading_principal_submatrix A k = submatrix A {..<k} {..<k}"
abbreviation "lps ≡ leading_principal_submatrix"
lemma leading_principal_submatrix_carrier:
"m ≥ n ⟹ A ∈ carrier_mat m m ⟹ lps A n ∈ carrier_mat n n"
proof-
assume *: "m ≥ n" "A ∈ carrier_mat m m"
let ?B = "lps A n"
have "(card {i. i < dim_row A ∧ i ∈ {..<n}}) = n"
by (metis "*"(1) "*"(2) Collect_conj_eq Collect_mem_eq card_lessThan carrier_matD(1) inf.absorb_iff2 lessThan_def lessThan_subset_iff)
hence "dim_col ?B = n ∧ dim_row ?B = n"
unfolding leading_principal_submatrix_def submatrix_def
using "*"(2) by auto
thus ?thesis by blast
qed
lemma pick_n:
assumes "i ≤ n"
shows "pick {..n} i = i"
using assms
proof(induct i)
case 0
then show ?case by force
next
case (Suc i)
hence "Suc i ∈ {..n}" by blast
moreover from Suc have "Suc i > pick {..n} i" by simp
moreover from Suc have "∀i' < Suc i. ¬ (i'∈{..n} ∧ i' > pick {..n} i)"
using Suc_leD not_less_eq by presburger
ultimately have "Suc i = (LEAST a. a∈{..n} ∧ a > pick {..n} i)"
by (metis (no_types, lifting) LeastI linorder_not_less not_less_Least order.strict_iff_order)
thus ?case by (metis DL_Missing_Sublist.pick.simps(2))
qed
lemma pick_n_le:
assumes "i < n"
shows "pick {..<n} i = i"
by (metis assms lessThan_Suc_atMost less_Suc_eq_le not0_implies_Suc not_less_zero pick_n)
lemma leading_principal_submatrix_index:
assumes "A ∈ carrier_mat n n"
assumes "k ≤ n"
assumes "i < k"
assumes "j < k"
shows "(lps A k)$$(i,j) = A$$(i,j)"
proof-
have "⋀i. i < k ⟹ pick {..<k} i = i" by (simp add: pick_n_le)
moreover have "card {i. i < dim_row A ∧ i ∈ {..<k}} = k"
by (metis Collect_conj_eq Collect_mem_eq assms(1) assms(2) card_lessThan carrier_matD(1) inf.absorb_iff2 lessThan_def lessThan_subset_iff)
moreover then have "card {j. j < dim_col A ∧ j ∈ {..<k}} = k" using assms(1) by force
moreover have "(mat k k (λ(i, j). A$$(i,j)))$$(i,j) = A$$(i,j)" using assms(3) assms(4) by auto
ultimately show ?thesis by (simp add: assms(3) assms(4) submatrix_def)
qed
lemma nested_leading_principle_submatrices:
assumes "A ∈ carrier_mat n n"
assumes "k⇩1 ≤ k⇩2"
assumes "k⇩2 ≤ n"
shows "lps A k⇩1 = lps (lps A k⇩2) k⇩1" (is "?lhs = ?rhs")
proof-
have "⋀i j. i < k⇩1 ⟹ j < k⇩1 ⟹ ?lhs$$(i,j) = ?rhs$$(i,j)"
by (smt (verit, best) assms dual_order.trans leading_principal_submatrix_carrier leading_principal_submatrix_index order.strict_trans2)
moreover have "?lhs ∈ carrier_mat k⇩1 k⇩1"
by (meson assms leading_principal_submatrix_carrier order_trans)
moreover have "?rhs ∈ carrier_mat k⇩1 k⇩1"
by (meson assms leading_principal_submatrix_carrier)
ultimately show ?thesis by auto
qed
section "Hermitian Matrix"
lemma hermitian_real_diag_decomp_eigvals:
fixes A :: "complex mat"
assumes "A ∈ carrier_mat n n"
assumes "hermitian A"
assumes "eigvals_of A es"
obtains B U where
"real_diag_decomp A B U"
"diag_mat B = es"
"set es ⊆ Reals"
"B ∈ carrier_mat n n"
"U ∈ carrier_mat n n"
proof-
have es: "char_poly A = (∏ (e :: complex) ← es. [:- e, 1:])"
using assms eigvals_poly_length by auto
obtain B U Q where us: "unitary_schur_decomposition A es = (B,U,Q)"
by (cases "unitary_schur_decomposition A es")
hence *: "similar_mat_wit A B U (adjoint U) ∧ diagonal_mat B
∧ diag_mat B = es ∧ unitary U ∧ (∀i < n. B$$(i, i) ∈ Reals)"
using hermitian_eigenvalue_real assms es by auto
moreover then have "dim_row B = n" using assms similar_mat_wit_dim_row[of A] by auto
ultimately have 1: "real_diag_decomp A B U" using unitary_diagI[of A]
unfolding real_diag_decomp_def by simp
from * have 2: "diag_mat B = es" by blast
from * have 3: "set es ⊆ Reals" by (metis ‹dim_row B = n› diag_elems_real diag_elems_set_diag_mat)
from * have 4: "B ∈ carrier_mat n n" by (meson assms(1) similar_mat_witD2(5))
from * have 5: "U ∈ carrier_mat n n" by (meson assms(1) similar_mat_witD2(6))
from that show ?thesis using 1 2 3 4 5 by blast
qed
lemma hermitian_eigvals_of_real: "hermitian (A::complex mat) ⟹ eigvals_of A es ⟹ set es ⊆ ℝ"
using hermitian_real_diag_decomp_eigvals[of A _ es] hermitian_square by blast
lemma hermitian_is_square: "hermitian A ⟹ square_mat A"
by (metis adjoint_dim_col hermitian_def square_mat.simps)
lemma hermitian_ij_ji_iff:
"hermitian A
⟷ square_mat A ∧ (∀i j. i < dim_row A ∧ j < dim_row A ⟶ A$$(i,j) = conjugate (A$$(j,i)))"
by (metis (no_types, lifting) adjoint_dim_col adjoint_dim_row adjoint_eval hermitian_def mat_eq_iff square_mat.simps)
lemma adjoint_is_conjugate_transpose: "A⇧H = adjoint A"
by (simp add: adjoint_def transpose_def cong_mat conjugate_mat_def)
subsection "Locale for Complex Hermitian Matrices"
locale cmplx_herm_mat = complex_vec_space n for n +
fixes A :: "complex mat"
assumes A_dim: "A ∈ carrier_mat n n"
assumes A_herm: "hermitian A"
begin
lemma hermitian_quadratic_form_real:
fixes v :: "complex vec"
assumes v: "v ∈ carrier_vec n"
shows "QF A v ∈ Reals"
proof-
have "conjugate (QF A v) = inner_prod (A *⇩v v) v"
using A_dim v by (metis inner_prod_swap mult_mat_vec_carrier quadratic_form_def)
also have "… = inner_prod v ((adjoint A) *⇩v v)"
using A_dim A_herm v by (metis adjoint_def_alter hermitian_def)
also have "… = inner_prod v (A *⇩v v)" using A_herm by (simp add: hermitian_def)
finally have "conjugate (QF A v) = QF A v" by simp
thus ?thesis by (simp add: Reals_cnj_iff)
qed
definition eigenvalues⇩0 :: "complex list" where
"eigenvalues⇩0 ≡ eigvals A"
lemma eigenvalues⇩0_exist: "∃es. eigvals_of A es" using A_dim eigvals_poly_length by auto
lemma eigenvalues⇩0: "eigvals_of A eigenvalues⇩0"
using eigenvalues⇩0_exist unfolding eigvals_of eigenvalues⇩0_def eigvals_def ..
lemma eigenvalues⇩0_real: "set eigenvalues⇩0 ⊆ ℝ"
using A_herm eigenvalues⇩0 hermitian_eigvals_of_real
by blast
definition eigenvalues :: "complex list" where
"eigenvalues ≡ rev (sort_key Re eigenvalues⇩0)"
lemma eigenvalues: "eigvals_of A eigenvalues"
proof-
have "mset eigenvalues = mset eigenvalues⇩0" by (simp add: eigenvalues_def)
thus ?thesis
using eigenvalues_def eigvals_of eigenvalues⇩0
by (metis (mono_tags, lifting) mset_eq_length mset_map prod_mset_prod_list)
qed
lemma eigenvalues_sorted: "sorted_wrt (≥) eigenvalues"
proof-
have "∀μ⇩1 μ⇩2. μ⇩1 ∈ set eigenvalues⇩0 ⟶ μ⇩2 ∈ set eigenvalues⇩0 ⟶ (μ⇩1 ≤ μ⇩2 ⟷ Re μ⇩1 ≤ Re μ⇩2)"
using eigenvalues_def eigenvalues⇩0_real by (simp add: complex_is_Real_iff less_eq_complex_def subset_iff)
hence "sorted_wrt (≤) (sort_key Re eigenvalues⇩0)"
by (smt (verit, ccfv_threshold) length_map nth_map nth_mem order_trans_rules(19) set_sort sorted_sort_key
sorted_wrt_iff_nth_less)
thus ?thesis unfolding eigenvalues_def sorted_wrt_rev .
qed
lemma eigenvalues_unique:
assumes es: "eigvals_of A es'"
assumes es_sorted: "sorted_wrt (≥) es'"
shows "es' = eigenvalues"
proof-
have "mset es' = mset eigenvalues" using es eigenvalues eigvals_of_mset_eq by blast
moreover have "length es' = length eigenvalues" by (metis calculation size_mset)
moreover have "sorted (rev (map Re es'))"
using es_sorted by (metis less_eq_complex_def sorted_wrt_map_mono sorted_wrt_rev)
moreover have "sorted (rev (map Re eigenvalues))"
using eigenvalues by (simp add: eigenvalues_def rev_map)
ultimately have "rev (map Re es') = rev (map Re eigenvalues)"
by (metis mset_map mset_rev properties_for_sort)
hence "map Re es' = map Re eigenvalues" by force
moreover have "set es' ⊆ ℝ ∧ set eigenvalues ⊆ ℝ"
using es A_herm eigenvalues hermitian_eigvals_of_real by blast
ultimately show "es' = eigenvalues" by (metis list.inj_map_strong of_real_Re subset_code(1))
qed
lemma eigenvalues_real: "set eigenvalues ⊆ ℝ"
using A_herm hermitian_eigvals_of_real eigenvalues(1) by blast
lemma eigenvalues_set_eq: "set eigenvalues⇩0 = set eigenvalues"
by (simp add: eigenvalues_def)
lemma hermitian_eigenvalues_real:
assumes e: "eigenvalue A e"
shows "e ∈ Reals"
using cpx_sq_mat.hermitian_spectrum_real[OF _ A_dim A_herm, of n n e]
using A_dim e
by (metis Projective_Measurements.spectrum_def cpx_sq_mat_axioms.intro cpx_sq_mat_def eigenvalue_imp_nonzero_dim eigenvalue_root_char_poly eigvals_poly_length fixed_carrier_mat.intro root_poly_linear)
lemma hermitian_spectrum_real: "spectrum A ⊆ Reals"
unfolding spectrum_connect[OF A_dim, symmetric]
by (simp add: Spectral_Radius.spectrum_def hermitian_eigenvalues_real unfold_simps(2))
lemma leading_principal_submatrix_hermitian:
assumes k: "k ≤ n"
shows "hermitian (lps A k)" (is "hermitian ?A'")
proof-
have "⋀i j. i < dim_row ?A' ⟹ j < dim_col ?A' ⟹ ?A'$$(i,j) = conjugate (?A'$$(j,i))"
using k A_dim A_herm
by (metis (no_types, lifting) adjoint_eval carrier_matD(1) carrier_matD(2) dual_order.strict_trans1 hermitian_def leading_principal_submatrix_carrier leading_principal_submatrix_index)
thus ?thesis
using A_dim k
by (metis (no_types, lifting) adjoint_dim_col adjoint_dim_row adjoint_eval carrier_matD(1) carrier_matD(2) eq_matI hermitian_def leading_principal_submatrix_carrier)
qed
lemma hermitian_mat_inv:
assumes A'_dim: "A' ∈ carrier_mat n n"
assumes inv: "inverts_mat A A'"
shows "hermitian A'"
using A_dim A_herm assms
by (metis (no_types, lifting) ext adjoint_dim' adjoint_mult adjoint_one
carrier_matD(1,2) hermitian_def invertible_det invertible_mat_def inverts_mat_def inverts_mat_sym
square_mat.simps vec_space.det_nonzero_congruence)
lemma negative_hermitian: "hermitian (-A)"
using A_dim A_herm
by (metis hermitian_minus left_add_zero_mat minus_add_uminus_mat uminus_carrier_iff_mat zero_carrier_mat zero_hermitian)
lemma principal_submatrix_hermitian:
assumes I: "I ⊆ {..<n}"
shows "hermitian (submatrix A I I)" (is "hermitian ?B")
proof-
have "square_mat ?B"
using A_dim
by (metis (full_types) carrier_matD(1) carrier_matD(2) dim_submatrix(1) dim_submatrix(2) square_mat.elims(1))
moreover {
fix i j assume *: "i < dim_row ?B ∧ j < dim_row ?B"
then obtain i' j' where "?B$$(i,j) = A$$(i',j') ∧ i' = pick I i ∧ j' = pick I j"
unfolding submatrix_def using A_dim pick_le by auto
moreover then have "?B$$(j,i) = A$$(j',i')"
unfolding submatrix_def
using A_dim
by (metis (no_types, lifting) Collect_cong * carrier_matD(1) carrier_matD(2) case_prod_conv dim_submatrix(1) index_mat(1))
ultimately have "?B$$(i,j) = conjugate (?B$$(j,i))"
using * A_herm by (metis dim_submatrix(1) hermitian_ij_ji_iff pick_le)
}
ultimately show ?thesis by (metis hermitian_ij_ji_iff)
qed
lemma hermitian_row_col:
assumes "i < n"
shows "row A i = conjugate (col A i)"
using A_dim A_herm assms by (metis adjoint_row carrier_matD(2) hermitian_def)
lemma inner_prod_swap:
assumes v: "v ∈ carrier_vec n"
assumes w: "w ∈ carrier_vec n"
shows "(A *⇩v v) ∙c w = v ∙c (A *⇩v w)"
proof-
have "(A *⇩v v) ∙c w = v ∙c (A⇧H *⇩v w)"
using assms by (metis adjoint_def_alter adjoint_is_conjugate_transpose A_dim)
also have "… = v ∙c (A *⇩v w)"
using A_herm assms by (simp add: adjoint_is_conjugate_transpose hermitian_def)
finally show ?thesis .
qed
end
section "Matrix Conjugate"
lemma conjugate_mat_dist:
fixes A B :: "'a::conjugatable_ring mat"
assumes "A ∈ carrier_mat m n"
assumes "B ∈ carrier_mat n p"
shows "(conjugate A) * (conjugate B) = conjugate (A * B)"
using assms
by (smt (z3) carrier_matD(1) carrier_matD(2) col_conjugate conjugate_scalar_prod dim_col dim_col_conjugate dim_row_conjugate eq_matI index_mult_mat(1) index_mult_mat(2) index_mult_mat(3) index_row(2) mat_index_conjugate row_conjugate)
lemma conjugate_mat_inv:
fixes A :: "'a::{conjugatable_ring,semiring_1} mat"
assumes "A ∈ carrier_mat n n"
assumes "A' ∈ carrier_mat n n"
assumes "inverts_mat A A'"
shows "inverts_mat (conjugate A) (conjugate A')"
proof-
have "(conjugate A) * (conjugate A') = conjugate (A * A')"
using conjugate_mat_dist assms(1) assms(2) by blast
also have "… = conjugate (1⇩m n)"
by (metis assms(1) assms(3) carrier_matD(1) inverts_mat_def)
also have "… = 1⇩m n"
by (metis (no_types, lifting) carrier_matI conjugate_id conjugate_mat_dist dim_col_conjugate dim_row_conjugate index_one_mat(2) index_one_mat(3) left_mult_one_mat' right_mult_one_mat')
finally show ?thesis
by (metis index_mult_mat(2) index_one_mat(2) inverts_mat_def)
qed
lemma conjugate_dist_mult_mat:
fixes A :: "'a::conjugatable_ring mat"
assumes "A ∈ carrier_mat m n" "B ∈ carrier_mat n p"
shows "conjugate (A * B) = conjugate A * conjugate B"
(is "?lhs = ?rhs")
proof-
have "⋀i j. i < m ⟹ j < p ⟹ ?lhs$$(i,j) = ?rhs$$(i,j)"
by (smt (verit, del_insts) assms carrier_matD(1) carrier_matD(2) col_conjugate conjugate_scalar_prod dim_col dim_col_conjugate dim_row_conjugate index_mult_mat(1) index_mult_mat(2) index_mult_mat(3) index_row(2) mat_index_conjugate row_conjugate)
moreover have "?lhs ∈ carrier_mat m p" using assms by auto
ultimately show ?thesis using assms carrier_matD(2) by auto
qed
lemma conjugate_dist_add_mat:
fixes A :: "'a::conjugatable_ring mat"
assumes "A ∈ carrier_mat m n" "B ∈ carrier_mat m n"
shows "conjugate (A + B) = conjugate A + conjugate B"
(is "?lhs = ?rhs")
proof-
have "⋀i j. i < m ⟹ j < n ⟹ ?lhs$$(i,j) = ?rhs$$(i,j)"
using assms assms conjugate_dist_add by fastforce
moreover have "?lhs ∈ carrier_mat m n" using assms by auto
ultimately show ?thesis using assms carrier_matD(2) by auto
qed
lemma mat_row_conj:
assumes "A ∈ carrier_mat m n"
assumes "i < m"
shows "conjugate (row A i) = row (conjugate A) i"
using assms
unfolding conjugate_mat_def
by auto
lemma conj_mat_vec_mult:
fixes A :: "'a::{conjugate,conjugatable_ring} mat"
fixes v :: "'a vec"
assumes "A ∈ carrier_mat n n"
assumes "v ∈ carrier_vec n"
shows "conjugate (A *⇩v v) = (conjugate A) *⇩v (conjugate v)"
(is "?lhs = ?rhs")
proof-
have "⋀i. i < n ⟹ ?lhs$i = ?rhs$i"
by (metis assms carrier_matD(1) conjugate_sprod_vec dim_mult_mat_vec dim_row_conjugate index_mult_mat_vec mat_row_conj row_carrier_vec vec_index_conjugate)
moreover have "?lhs ∈ carrier_vec n" using assms by force
ultimately show ?thesis using assms(1) by auto
qed
lemma conjugate_vec_first:
assumes "v ∈ carrier_vec n"
assumes "i ≤ n"
shows "conjugate (vec_first v i) = vec_first (conjugate v) i"
by (smt (verit, ccfv_SIG) assms carrier_vecD dim_vec_conjugate dim_vec_first eq_vecI index_vec le_less less_trans vec_first_def vec_index_conjugate)
lemma conjugate_vec_last: "i ≤ dim_vec v ⟹ conjugate (vec_last v i) = vec_last (conjugate v) i"
unfolding vec_last_def by auto
lemma cscalar_prod_symm_conj:
"dim_vec (x::('a::{comm_semiring_0,conjugatable_ring} vec)) = dim_vec (y::'a vec)
⟹ x ∙c y = conjugate (y ∙c x)"
by (simp add: conjugate_scalar_prod scalar_prod_comm)
section "Block Matrix"
lemma block_mat_vec_mult:
fixes x
assumes "A ∈ carrier_mat nr1 nc1"
assumes "B ∈ carrier_mat nr1 nc2"
assumes "C ∈ carrier_mat nr2 nc1"
assumes "D ∈ carrier_mat nr2 nc2"
assumes "M = four_block_mat A B C D"
assumes "x ∈ carrier_vec (nc1 + nc2)"
defines "x⇩1 ≡ vec_first x nc1"
defines "x⇩2 ≡ vec_last x nc2"
shows "M *⇩v x = (A *⇩v x⇩1 + B *⇩v x⇩2) @⇩v (C *⇩v x⇩1 + D *⇩v x⇩2)"
by (smt (verit, ccfv_threshold) assms four_block_mat_mult_vec vec_first_carrier vec_first_last_append vec_last_carrier)
lemma mat_vec_prod_leading_principal_submatrix:
fixes A :: "('a :: comm_ring) mat"
assumes "A ∈ carrier_mat (Suc n) (Suc n)"
assumes "x ∈ carrier_vec (Suc n)"
defines "A⇩n ≡ lps A n"
defines "v⇩n ≡ vec_first (col A n) n"
defines "w⇩n ≡ vec_first (row A n) n"
defines "a ≡ A $$ (n, n)"
defines "x⇩n ≡ vec_first x n"
defines "b ≡ x$n"
shows "A *⇩v x = (A⇩n *⇩v x⇩n + b ⋅⇩v v⇩n) @⇩v (vec 1 (λi. (w⇩n ∙ x⇩n) + a * b))" (is "?lhs = ?rhs")
proof
have dim_x⇩n: "dim_vec x⇩n = n" by (simp add: assms(7))
have dim_w⇩n: "dim_vec w⇩n = n" by (simp add: assms(5))
have dim_row_A⇩n: "dim_row A⇩n = n"
by (metis assms(1) assms(3) carrier_matD(1) le_add2 leading_principal_submatrix_carrier plus_1_eq_Suc)
have dim_col_A⇩n: "dim_col A⇩n = n"
by (metis assms(1) assms(3) carrier_matD(2) le_add2 leading_principal_submatrix_carrier plus_1_eq_Suc)
show dims: "dim_vec ?lhs = dim_vec ?rhs" using assms(1) v⇩n_def by auto
show "⋀i. i < dim_vec ?rhs ⟹ ?lhs$i = ?rhs$i"
proof-
fix i assume *: "i < dim_vec ?rhs"
hence i: "i < Suc n" using dims assms(1) by auto
hence dot: "?lhs$i = row A i ∙ x" using * dims by fastforce
have row_j: "⋀j. j < Suc n ⟹ (row A i)$j = A$$(i,j)" using assms(1) i by force
show "?lhs$i = ?rhs$i"
proof(cases "i < n")
case True
have A⇩n: "⋀j. j < n ⟹ A$$(i,j) = A⇩n$$(i,j)"
by (metis True assms(1) assms(3) le_add2 leading_principal_submatrix_index plus_1_eq_Suc)
have A⇩n_row: "⋀j. j < n ⟹ A⇩n$$(i,j) = (row A⇩n i)$j"
by (metis True assms(1) assms(3) carrier_matD(1) carrier_matD(2) index_row(1) le_add2 leading_principal_submatrix_carrier plus_1_eq_Suc)
have "?lhs$i = (A⇩n *⇩v x⇩n + b ⋅⇩v v⇩n)$i"
proof-
have "?lhs$i = (∑j<Suc n. A$$(i,j) * x$j)"
unfolding dot scalar_prod_def using row_j assms(2) atLeast0LessThan by force
moreover have "(∑j<n. A$$(i,j) * x$j) = (∑j<n. A⇩n$$(i,j) * x⇩n$j)"
by (smt (verit) A⇩n assms(7) index_vec lessThan_iff sum.cong vec_first_def)
moreover have "(∑j<n. A⇩n$$(i,j) * x⇩n$j) = (A⇩n *⇩v x⇩n)$i"
proof-
have "(A⇩n *⇩v x⇩n)$i = (row A⇩n i) ∙ x⇩n"
by (metis True assms(1) assms(3) carrier_matD(1) index_mult_mat_vec le_add2 leading_principal_submatrix_carrier plus_1_eq_Suc)
moreover have "⋀j. j < n ⟹ A⇩n$$(i,j) * x⇩n$j = (row A⇩n i)$j * x⇩n$j"
using A⇩n_row by presburger
ultimately show ?thesis
unfolding scalar_prod_def using atLeast0LessThan dim_x⇩n by fastforce
qed
moreover have "(A$$(i,n) * x$n) = (b ⋅⇩v v⇩n)$i"
proof-
have "x$n = b" unfolding b_def by blast
moreover have "A$$(i,n) = v⇩n$i"
using assms(1) i by (simp add: True vec_first_def v⇩n_def)
moreover have "(b ⋅⇩v v⇩n)$i = b * (v⇩n$i)" by (simp add: True v⇩n_def)
ultimately show ?thesis by (simp add: mult.commute)
qed
ultimately show ?thesis by (simp add: True assms(4))
qed
thus ?thesis by (simp add: True i v⇩n_def)
next
case False
hence *: "i = n" using i by linarith
hence "?lhs$i = (row A n) ∙ x" using dot by blast
also have "… = w⇩n ∙ x⇩n + a * b"
proof-
have "row A n = w⇩n @⇩v vec_last (row A n) 1"
by (metis "*" w⇩n_def assms(1) i row_carrier_vec semiring_norm(174) vec_first_last_append)
moreover have "(vec_last (row A n) 1)$0 = (row A n)$n"
by (metis "*" False assms(1) calculation carrier_matD(2) dim_w⇩n gr0I i index_append_vec(1) index_append_vec(2) index_row(2) zero_less_diff)
ultimately have "row A n = w⇩n @⇩v (vec 1 (λ_. A$$(n,n)))"
by (smt (verit, best) "*" One_nat_def carrier_vecD dim_vec eq_vecI i index_vec less_Suc0 row_j vec_last_carrier)
moreover have "x = x⇩n @⇩v (vec 1 (λ_. b))"
proof
show *: "dim_vec x = dim_vec (x⇩n @⇩v (vec 1 (λ_. b)))" by (simp add: assms(2) dim_x⇩n)
have "⋀i. i < Suc n ⟹ x$i = (x⇩n @⇩v (vec 1 (λ_. b)))$i"
proof-
fix i assume "i < Suc n"
show "x$i = (x⇩n @⇩v (vec 1 (λ_. b)))$i"
apply (cases "i = n")
apply (simp add: append_vec_def assms(8) dim_x⇩n)
apply (simp add: append_vec_def)
by (smt (verit, best) ‹i < Suc n› dim_x⇩n index_vec less_antisym vec_first_def x⇩n_def)
qed
thus "⋀i. i < dim_vec (x⇩n @⇩v vec 1 (λ_. b)) ⟹ x $ i = (x⇩n @⇩v vec 1 (λ_. b)) $ i"
by (metis * assms(2) carrier_vecD)
qed
ultimately have "(row A n) ∙ x = (w⇩n ∙ x⇩n) + ((vec 1 (λ_. A$$(n,n))) ∙ (vec 1 (λ_. b)))"
by (metis assms(5) assms(7) scalar_prod_append vec_carrier vec_first_carrier)
moreover have "((vec 1 (λ_. A$$(n,n))) ∙ (vec 1 (λ_. b))) = a * b"
by (simp add: a_def b_def scalar_prod_def)
ultimately show ?thesis by argo
qed
finally show ?thesis by (simp add: * v⇩n_def)
qed
qed
qed
lemma vec_first_index: "n ≤ dim_vec v ⟹ i < n ⟹ v$i = (vec_first v n)$i"
unfolding vec_first_def by simp
lemma vec_last_index:
"n ≤ dim_vec v ⟹ i ∈ {dim_vec v - m..<m} ⟹ v$i = (vec_last v m)$(i - (dim_vec v - m))"
unfolding vec_last_def by auto
lemma inner_prod_append:
assumes "x ∈ carrier_vec (dim_vec (u @⇩v v))"
shows "x ∙c (u @⇩v v) = (vec_first x (dim_vec u)) ∙c u + (vec_last x (dim_vec v)) ∙c v"
"(u @⇩v v) ∙c x = u ∙c (vec_first x (dim_vec u)) + v ∙c (vec_last x (dim_vec v))"
proof-
define n where "n ≡ dim_vec (u @⇩v v)"
define n⇩u where "n⇩u ≡ dim_vec u"
define n⇩v where "n⇩v ≡ dim_vec v"
have dims_add: "n⇩u + n⇩v = n" by (simp add: n⇩u_def n⇩v_def n_def)
have n⇩u_prop: "⋀i. i < n⇩u ⟹ conjugate (u @⇩v v)$i = (conjugate u)$i" by (simp add: n⇩u_def)
have n⇩v_prop: "⋀i. i < n⇩v ⟹ conjugate (u @⇩v v)$(i + n⇩u) = (conjugate v)$i"
by (simp add: n⇩u_def n⇩v_def)
have "n = dim_vec (conjugate (u @⇩v v))" by (simp add: n_def)
hence "x ∙c (u @⇩v v) = (∑i ∈ {0..<n}. x$i * (conjugate (u @⇩v v))$i)"
unfolding scalar_prod_def by blast
hence "x ∙c (u @⇩v v) =
(∑i ∈ {0..<n⇩u}. x$i * (conjugate (u @⇩v v))$i)
+ (∑i ∈ {n⇩u..<n}. x$i * (conjugate (u @⇩v v))$i)"
by (smt (verit, best) bot_nat_0.extremum index_append_vec(2) n⇩u_def n_def nat_le_linear nless_le not_add_less1 sum.atLeastLessThan_concat)
moreover have "(∑i ∈ {0..<n⇩u}. x$i * (conjugate (u @⇩v v))$i) = (vec_first x (dim_vec u)) ∙c u"
proof-
have *: "⋀i. i ∈ {0..<n⇩u} ⟹ x$i = (vec_first x n⇩u)$i"
by (simp add: vec_first_def)
have "(∑i ∈ {0..<n⇩u}. x$i * (conjugate (u @⇩v v))$i) = (∑i ∈ {0..<n⇩u}. x$i * (conjugate u)$i)"
using n⇩u_prop by simp
also have "… = (∑i ∈ {0..<n⇩u}. (vec_first x n⇩u)$i * (conjugate u)$i)"
using * by auto
also have "… = (vec_first x (dim_vec u)) ∙c u"
by (metis (no_types, lifting) dim_vec_conjugate n⇩u_def scalar_prod_def sum.cong)
finally show ?thesis .
qed
moreover have "(∑i ∈ {n⇩u..<n}. x$i * (conjugate (u @⇩v v))$i) = (vec_last x (dim_vec v)) ∙c v"
proof-
have *: "vec_last (u @⇩v v) n⇩v = v"
by (metis append_vec_eq carrier_vecI dims_add n⇩u_def n_def vec_first_carrier vec_first_last_append)
have "⋀i. i ∈ {n⇩u..<n} ⟹ x$i = (vec_last x n⇩v)$(i - (n - n⇩v))"
unfolding vec_last_def using assms dims_add less_diff_conv2 n_def by simp
moreover have "⋀i. i ∈ {n⇩u..<n}
⟹ (conjugate (u @⇩v v))$i = (vec_last (conjugate (u @⇩v v)) n⇩v)$(i - (n - n⇩v))"
unfolding vec_last_def using assms dims_add less_diff_conv2 n_def by simp
ultimately have "(∑i ∈ {n⇩u..<n}. x$i * (conjugate (u @⇩v v))$i)
= (∑i ∈ {n⇩u..<n}. (vec_last x n⇩v)$(i - (n - n⇩v))
* (vec_last (conjugate (u @⇩v v)) n⇩v)$(i - (n - n⇩v)))"
(is "_ = (∑i ∈ _. ?F i)")
by force
also have "… = (∑i ∈ {0..<n-n⇩u}. (vec_last x n⇩v)$((i + n⇩u) - (n - n⇩v))
* (vec_last (conjugate (u @⇩v v)) n⇩v)$((i + n⇩u) - (n - n⇩v)))"
using sum.shift_bounds_nat_ivl[of ?F 0 n⇩u n⇩v] dims_add
by (metis (no_types, lifting) add.commute add_0 add_diff_cancel_left')
finally show ?thesis
by (smt (verit, ccfv_SIG) "*" add_diff_cancel_left' add_diff_cancel_right' carrier_vecI conjugate_vec_last dim_vec_conjugate dims_add le_add2 n⇩v_def n_def scalar_prod_def sum.cong)
qed
ultimately show "x ∙c (u @⇩v v) = (vec_first x (dim_vec u)) ∙c u + (vec_last x (dim_vec v)) ∙c v"
by argo
have n⇩u_prop: "⋀i. i < n⇩u ⟹ (u @⇩v v)$i = u$i" by (simp add: n⇩u_def)
have n⇩v_prop: "⋀i. i < n⇩v ⟹ (u @⇩v v)$(i + n⇩u) = v$i"
by (simp add: n⇩u_def n⇩v_def)
have "n = dim_vec (conjugate (u @⇩v v))" by (simp add: n_def)
moreover have "dim_vec (conjugate x) = n" using assms n_def by auto
ultimately have "(u @⇩v v) ∙c x = (∑i ∈ {0..<n}. (u @⇩v v)$i * (conjugate x)$i)"
unfolding scalar_prod_def by presburger
hence "(u @⇩v v) ∙c x =
(∑i ∈ {0..<n⇩u}. (u @⇩v v)$i * (conjugate x)$i)
+ (∑i ∈ {n⇩u..<n}. (u @⇩v v)$i * (conjugate x)$i)"
by (smt (verit, best) bot_nat_0.extremum index_append_vec(2) n⇩u_def n_def nat_le_linear nless_le not_add_less1 sum.atLeastLessThan_concat)
moreover have "(∑i ∈ {0..<n⇩u}. (u @⇩v v)$i * (conjugate x)$i) = u ∙c (vec_first x (dim_vec u))"
proof-
have *: "⋀i. i ∈ {0..<n⇩u} ⟹ (conjugate x)$i = (vec_first (conjugate x) n⇩u)$i"
by (simp add: vec_first_def)
have "(∑i ∈ {0..<n⇩u}. (u @⇩v v)$i * (conjugate x)$i)
= (∑i ∈ {0..<n⇩u}. u$i * (conjugate x)$i)"
using n⇩u_prop by simp
also have "… = (∑i ∈ {0..<n⇩u}. u$i * (vec_first (conjugate x) n⇩u)$i)"
using * by force
also have "… = u ∙c (vec_first x (dim_vec u))"
by (metis (no_types, lifting) add.commute assms conjugate_vec_first dim_vec_first dims_add le_add2 n⇩u_def n_def scalar_prod_def sum.cong)
finally show ?thesis .
qed
moreover have "(∑i ∈ {n⇩u..<n}. (u @⇩v v)$i * (conjugate x)$i) = v ∙c (vec_last x (dim_vec v))"
proof-
have *: "vec_last (u @⇩v v) n⇩v = v"
by (metis append_vec_eq carrier_vecI dims_add n⇩u_def n_def vec_first_carrier vec_first_last_append)
have "⋀i. i ∈ {n⇩u..<n} ⟹ (conjugate x)$i = (vec_last (conjugate x) n⇩v)$(i - (n - n⇩v))"
unfolding vec_last_def using assms dims_add less_diff_conv2 n_def by simp
moreover have "⋀i. i ∈ {n⇩u..<n}
⟹ (u @⇩v v)$i = (vec_last (u @⇩v v) n⇩v)$(i - (n - n⇩v))"
unfolding vec_last_def using assms dims_add less_diff_conv2 n_def by simp
ultimately have "(∑i ∈ {n⇩u..<n}. (u @⇩v v)$i * (conjugate x)$i)
= (∑i ∈ {n⇩u..<n}. (vec_last (u @⇩v v) n⇩v)$(i - (n - n⇩v))
* (vec_last (conjugate x) n⇩v)$(i - (n - n⇩v)))"
(is "_ = (∑i ∈ _. ?F i)")
by force
also have "… = (∑i ∈ {0..<n-n⇩u}. (vec_last (u @⇩v v) n⇩v)$((i + n⇩u) - (n - n⇩v))
* (vec_last (conjugate x) n⇩v)$((i + n⇩u) - (n - n⇩v)))"
using sum.shift_bounds_nat_ivl[of ?F 0 n⇩u n⇩v] dims_add
by (metis (no_types, lifting) add.commute add_0 add_diff_cancel_left')
finally show ?thesis
by (smt (verit, best) "*" ‹dim_vec (conjugate x) = n› add_diff_cancel_left' add_diff_cancel_right' conjugate_vec_last dim_vec_conjugate dim_vec_last dims_add le_add2 scalar_prod_def sum.cong)
qed
ultimately show "(u @⇩v v) ∙c x = u ∙c (vec_first x (dim_vec u)) + v ∙c (vec_last x (dim_vec v))"
by argo
qed
subsection "Schur's Formula"
proposition schur_formula:
fixes M :: "'a::field mat"
assumes "(A,B,C,D) = split_block M r c"
assumes "r < dim_row M"
assumes "c < dim_col M"
assumes "square_mat M"
assumes "square_mat A"
assumes "inverts_mat A' A"
assumes A'_dim: "A' ∈ carrier_mat r r"
shows "Determinant.det M = Determinant.det A * Determinant.det (D - C * A' * B)"
proof-
let ?r⇩M = "dim_row M"
let ?c⇩M = "dim_col M"
let ?r⇩A = "r"
let ?c⇩A = "c"
let ?r⇩B = "r"
let ?c⇩B = "?c⇩M - ?c⇩A"
let ?r⇩C = "?r⇩M - ?r⇩A"
let ?c⇩C = "c"
let ?r⇩D = "?r⇩M - ?r⇩A"
let ?c⇩D = "?c⇩M - ?c⇩A"
let ?I⇩A = "1⇩m r"
let ?I⇩D = "1⇩m ?r⇩D"
let ?O⇩B = "0⇩m ?r⇩B ?c⇩B"
let ?O⇩C = "0⇩m ?r⇩C ?c⇩C"
let ?P = "four_block_mat ?I⇩A ?O⇩B (C * A') ?I⇩D"
let ?Q = "four_block_mat A ?O⇩B ?O⇩C (D - C * A' * B)"
let ?R = "four_block_mat ?I⇩A (A' * B) ?O⇩C ?I⇩D"
have M: "M = four_block_mat A B C D"
using Matrix.split_block(5)[of M r c A B C D] by (metis assms(1-3) le_simps(1) less_eqE)
have M_dim: "M ∈ carrier_mat ?r⇩M ?c⇩M"
by blast
have A_dim: "A ∈ carrier_mat r r"
using assms(1)
unfolding split_block_def
by (metis Pair_inject assms(5) carrier_mat_triv dim_row_mat(1) square_mat.elims(2))
have square: "?r⇩M - ?r⇩A = ?c⇩M - ?c⇩A" "r = c" "?r⇩M = ?c⇩M"
using M_dim assms(4)
apply (metis A_dim assms(1) assms(5) carrier_matD(1) dim_col_mat(1) prod.sel(1) split_block_def square_mat.elims(2))
apply (metis A_dim assms(1) carrier_matD(2) dim_col_mat(1) prod.sel(1) split_block_def)
using assms(4) by force
have C_A'_dim: "C * A' ∈ carrier_mat ?r⇩C ?c⇩C"
by (smt (verit) A'_dim Pair_inject assms(1) carrier_matD(2) carrier_mat_triv dim_row_mat(1) index_mult_mat(2) index_mult_mat(3) split_block_def square(2))
have A'_B_dim: "A' * B ∈ carrier_mat ?r⇩B ?c⇩B"
by (metis (no_types, lifting) A'_dim Pair_inject assms(1) carrier_matD(1) carrier_mat_triv dim_col_mat(1) index_mult_mat(2) index_mult_mat(3) split_block_def)
have D_min_C_A'_B_dim: "D - C * A' * B ∈ carrier_mat ?c⇩D ?c⇩D"
by (metis A'_B_dim C_A'_dim carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3) minus_carrier_mat square(1))
have P_dim: "?P ∈ carrier_mat ?r⇩M ?c⇩M"
using assms(2) square(3) by auto
have Q_dim: "?Q ∈ carrier_mat ?r⇩M ?c⇩M"
by (smt (verit) A_dim D_min_C_A'_B_dim P_dim carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mat_four_block(2) index_mat_four_block(3) index_one_mat(3) square(2) square(3))
have R_dim: "?R ∈ carrier_mat ?r⇩M ?c⇩M"
using P_dim by fastforce
have M: "M = ?P * ?Q * ?R"
proof-
have B_dim: "B ∈ carrier_mat ?r⇩B ?c⇩B"
by (metis assms(1) assms(2) assms(3) less_imp_le_nat ordered_cancel_comm_monoid_diff_class.add_diff_inverse split_block(2))
have C_dim: "C ∈ carrier_mat ?r⇩C r"
by (metis assms(1) assms(3) diff_add_inverse less_eqE less_or_eq_imp_le split_block(3) square(2) square(3))
have D_dim: "D ∈ carrier_mat ?r⇩D ?c⇩D"
using A_dim M square(2) by auto
have 1: "?I⇩A ∈ carrier_mat r r" by simp
have 2: "?O⇩B ∈ carrier_mat ?r⇩B ?c⇩B" by auto
have 3: "C * A' ∈ carrier_mat ?r⇩C r" using C_A'_dim square(2) by blast
have 4: "?I⇩D ∈ carrier_mat ?r⇩C ?c⇩B" using "2" square(1) by auto
have 6: "?O⇩B ∈ carrier_mat r ?c⇩B" using "2" square(2) by blast
have 7: "?O⇩C ∈ carrier_mat ?c⇩B r" using "4" square(2) by auto
have 8: "(D - C * A' * B) ∈ carrier_mat ?c⇩B ?c⇩B"
using "4" D_min_C_A'_B_dim square(1) square(2) by auto
have a: "(D - C * A' * B) ∈ carrier_mat ?r⇩D ?c⇩D" using "8" square(1) by presburger
have b: "?I⇩D ∈ carrier_mat ?c⇩B ?c⇩B" using "2" square(1) by auto
have ass: "(C * A') * A = C * (A' * A)" using A_dim A'_dim C_dim by (simp add: square(2))
have "?P * ?Q = four_block_mat A ?O⇩B C (D - C * A' * B)"
proof-
have "A = ?I⇩A * A + ?O⇩B * ?O⇩C"
using A_dim square(2) square(3) by auto
moreover have "?O⇩B = ?I⇩A * ?O⇩B + ?O⇩B * (D - C * A' * B)"
by (smt (verit, ccfv_threshold) "1" "2" "8" D_min_C_A'_B_dim carrier_matD(2) left_add_zero_mat left_mult_zero_mat right_mult_zero_mat)
moreover have "C = (C * A') * A + ?I⇩D * ?O⇩C"
by (metis A'_dim C_dim square(2) Matrix.right_add_zero_mat ass assms(6) carrier_matD(1) index_zero_mat(2) inverts_mat_def left_mult_one_mat' right_mult_one_mat)
moreover have "(D - C * A' * B) = ((C * A') * ?O⇩B) + ?I⇩D * (D - C * A' * B)"
by (metis C_A'_dim D_min_C_A'_B_dim left_add_zero_mat left_mult_one_mat right_mult_zero_mat square(1) square(2))
ultimately show ?thesis
using mult_four_block_mat[OF 1 2 3 4 A_dim 6 7 8] by argo
qed
also have "… * ?R = four_block_mat A B C D"
proof-
have "A = A * ?I⇩A + ?O⇩B * C"
using A_dim C_dim square(1) by force
moreover have "B = A * (A' * B) + ?O⇩B * ?I⇩D"
by (smt (verit, ccfv_threshold) inverts_mat_symm A_dim B_dim Matrix.right_add_zero_mat assms(6) assms(7) assoc_mult_mat b carrier_mat_triv index_mult_mat(2) inverts_mat_def left_mult_one_mat left_mult_zero_mat)
moreover have "C = C * ?I⇩A + (D - C * A' * B) * ?O⇩C"
by (metis "8" C_dim Matrix.right_add_zero_mat right_mult_one_mat right_mult_zero_mat square(1) square(2))
moreover have "D = C * (A' * B) + (D - C * A' * B) * ?I⇩D"
proof-
have "C * A' * B ∈ carrier_mat ?r⇩D ?c⇩D"
using B_dim C_A'_dim mult_carrier_mat square(2) by blast
moreover have "C * (A' * B) = C * A' * B" using B_dim C_dim assms(7) by force
ultimately show ?thesis
by (metis (no_types, lifting) "8" D_dim left_add_zero_mat mat_minus_minus minus_r_inv_mat right_mult_one_mat square(2) square(3))
qed
ultimately show ?thesis
using mult_four_block_mat[OF A_dim 2 C_dim a 1 A'_B_dim 7 b] A_dim square(2) square(3)
by force
qed
also have "… = M" unfolding M by simp
finally show ?thesis by argo
qed
hence "Determinant.det M = Determinant.det ?P * Determinant.det ?Q * Determinant.det ?R"
by (smt (verit, best) det_mult P_dim Q_dim R_dim assms(4) mult_carrier_mat square_mat.elims(2))
moreover have "Determinant.det ?P = 1"
using det_four_block_mat_upper_right_zero[OF _ _ C_A'_dim, of ?I⇩A ?O⇩B ?I⇩D]
by (simp add: square)
moreover have "Determinant.det ?Q = Determinant.det A * Determinant.det (D - C * A' * B)"
using det_four_block_mat_upper_right_zero[OF A_dim _ _ D_min_C_A'_B_dim, of ?O⇩B ?O⇩C]
by (simp add: square)
moreover have "Determinant.det ?R = 1"
using det_four_block_mat_lower_left_zero[OF _ A'_B_dim, of ?I⇩A "?O⇩C" ?I⇩D]
by (simp add: square)
ultimately show ?thesis by fastforce
qed
section "Positive Definite Matrix"
definition positive_definite :: "'a::{ord,conjugatable_field} mat ⇒ bool" where
"positive_definite M ⟷ hermitian M
∧ (∀x ∈ carrier_vec (dim_col M). x ≠ 0⇩v (dim_col M) ⟶ QF M x > 0)"
lemma leading_principal_submatrix_positive_definite:
fixes A :: "'a::{conjugatable_field,ord} mat"
assumes "A ∈ carrier_mat n n"
assumes "positive_definite A"
assumes "k ≤ n"
shows "positive_definite (lps A k)"
proof-
define B where "B ≡ lps A k"
have B_carrier: "B ∈ carrier_mat k k"
using B_def assms(1) assms(3) leading_principal_submatrix_carrier by blast
hence B_dims: "dim_row B = k ∧ dim_col B = k" by simp
{ fix v :: "'a vec"
assume *: "v ∈ carrier_vec k" "v ≠ 0⇩v k"
define w where "w ≡ vec n (λi. if i < k then v$i else 0)"
hence "w ≠ 0⇩v n"
by (smt (verit) "*"(1) "*"(2) assms(3) carrier_vecD dual_order.strict_trans1 eq_vecI index_vec index_zero_vec(1) index_zero_vec(2))
hence "QF A w > 0" using assms(1) assms(2) positive_definite_def vec_carrier w_def by blast
moreover have "QF A w = QF B v"
proof-
have 1: "⋀i. i ∈ {k..<n} ⟹ conjugate (w$i) = 0" using w_def by simp
have 2: "⋀i. i ∈ {0..<k} ⟹ w$i = v$i" using assms(3) w_def by auto
hence 3: "⋀i. i ∈ {0..<k} ⟹ conjugate (w$i) = conjugate (v$i)" by presburger
have 4: "⋀i. i ∈ {0..<k} ⟹ (A *⇩v w)$i = (B *⇩v v)$i"
proof-
fix i assume **: "i ∈ {0..<k}"
have ***: "⋀j. j ∈ {0..<k} ⟹ (row A i)$j = (row B i)$j"
proof-
fix j assume "j ∈ {0..<k}"
moreover then have "(row A i)$j = A$$(i,j)"
using "**" * assms(1) assms(3) by force
ultimately show "(row A i)$j = (row B i)$j"
by (metis (mono_tags, lifting) ** B_def B_dims assms(1) assms(3) atLeastLessThan_iff index_vec leading_principal_submatrix_index row_def)
qed
have ****: "row B i ∈ carrier_vec k ∧ dim_vec v = k"
using B_carrier B_dims * by auto
have "(A *⇩v w)$i = row A i ∙ w" using ** assms(1) assms(3) by force
also have "… = (∑j ∈ {0..<n}. (row A i)$j * w$j)"
by (metis (no_types, lifting) dim_vec scalar_prod_def sum.cong w_def)
also have "… = (∑j ∈ {0..<k}. (row A i)$j * w$j) + (∑j ∈ {k..<n}. (row A i)$j * w$j)"
by (simp add: assms(3) sum.atLeastLessThan_concat)
also have "… = (∑j ∈ {0..<k}. (row A i)$j * v$j)"
using 1 2 by auto
also have "… = (∑j ∈ {0..<k}. (row B i)$j * v$j)"
using *** by fastforce
also have "… = (row B i) ∙ v"
using B_carrier **** unfolding scalar_prod_def by blast
also have "… = (B *⇩v v)$i" using ** B_carrier by auto
finally show "(A *⇩v w)$i = (B *⇩v v)$i" .
qed
have 5: "v ∈ carrier_vec k" by (simp add: "*"(1))
hence 6: "B *⇩v v ∈ carrier_vec k ∧ conjugate v ∈ carrier_vec k"
by (metis B_def Matrix.carrier_vec_conjugate assms(1) assms(3) leading_principal_submatrix_carrier mult_mat_vec_carrier)
have "QF A w = (A *⇩v w) ∙c w" by simp
also have "… = (∑i ∈ {0..<n}. (A *⇩v w)$i * conjugate (w$i))"
by (smt (verit, ccfv_SIG) atLeastLessThan_iff dim_vec dim_vec_conjugate scalar_prod_def sum.cong vec_index_conjugate w_def)
also have "… = (∑i ∈ {0..<k}. (A *⇩v w)$i * conjugate (w$i))
+ (∑i ∈ {k..<n}. (A *⇩v w)$i * conjugate (w$i))"
by (simp add: assms(3) sum.atLeastLessThan_concat)
also have "… = (∑i ∈ {0..<k}. (A *⇩v w)$i * conjugate (w$i))" using 1 by simp
also have "… = (∑i ∈ {0..<k}. (B *⇩v v)$i * conjugate (v$i))" using 3 4 by force
also have "… = (B *⇩v v) ∙c v"
by (smt (verit, best) 5 6 atLeastLessThan_iff carrier_vecD scalar_prod_def sum.cong vec_index_conjugate)
finally show ?thesis using quadratic_form_def by force
qed
ultimately have "QF B v > 0" by argo
}
thus ?thesis
using assms hermitian_ij_ji_iff cmplx_herm_mat.leading_principal_submatrix_hermitian B_dims
unfolding positive_definite_def B_def
by (smt (verit, best) carrier_matD(1) leading_principal_submatrix_index order_less_le_trans square_mat.simps)
qed
lemma positive_definite_invertible:
fixes M :: "complex mat"
assumes "positive_definite M"
shows "invertible_mat M"
proof-
define n where "n ≡ dim_row M"
have "⋀x. x ∈ carrier_vec n ⟹ x ≠ 0⇩v n ⟹ M *⇩v x ≠ 0⇩v n"
using assms n_def positive_definite_def hermitian_is_square by force
hence "mat_kernel M ⊆ {0⇩v n}"
unfolding mat_kernel_def n_def
by (metis (mono_tags, lifting) assms hermitian_is_square mem_Collect_eq positive_definite_def singleton_iff square_mat.simps subsetI)
thus ?thesis
using trivial_kernel_imp_invertible n_def assms positive_definite_def hermitian_is_square
by blast
qed
lemma positive_definite_det_nz:
fixes A :: "complex mat"
assumes "positive_definite A"
shows "Determinant.det A ≠ 0"
using positive_definite_invertible[OF assms] invertible_det invertible_mat_def square_mat.simps
by blast
section "Matrix-Vector Multiplication"
lemma diagonal_unit_vec':
assumes "B ∈ carrier_mat n n"
assumes "diagonal_mat (B::'a::{ring,zero_neq_one} Matrix.mat)"
shows "B *⇩v (unit_vec n i) = B $$ (i,i) ⋅⇩v (unit_vec n i)"
proof -
define v :: "'a Matrix.vec" where "v = unit_vec n i"
have "B *⇩v v = Matrix.vec n (λ i. Matrix.scalar_prod (Matrix.row B i) v)"
using assms unfolding mult_mat_vec_def by simp
also have "… = Matrix.vec n (λ i. B $$(i,i) * Matrix.vec_index v i)"
proof -
have "∀i < n. (Matrix.scalar_prod (Matrix.row B i) v = B $$(i,i) * Matrix.vec_index v i)"
proof (intro allI impI)
fix i
assume "i < n"
have "(Matrix.scalar_prod (Matrix.row B i) v) =
(∑ j ∈ {0 ..< n}. Matrix.vec_index (Matrix.row B i) j * Matrix.vec_index v j)" using assms
unfolding Matrix.scalar_prod_def v_def by simp
also have "… = Matrix.vec_index (Matrix.row B i) i * Matrix.vec_index v i"
proof (rule sum_but_one)
show "∀j < n. j ≠ i ⟶ Matrix.vec_index (Matrix.row B i) j = 0"
proof (intro allI impI)
fix j
assume "j < n" and "j ≠ i"
hence "Matrix.vec_index (Matrix.row B i) j = B $$ (i,j)" using ‹i < n› ‹j < n› assms
by auto
also have "… = 0" using assms ‹i < n› ‹j < n› ‹j≠ i› unfolding diagonal_mat_def by simp
finally show "Matrix.vec_index (Matrix.row B i) j = 0" .
qed
show "i < n" using ‹i < n› .
qed
also have "… = B $$(i,i) * Matrix.vec_index v i" using assms ‹i < n› by auto
finally show "(Matrix.scalar_prod (Matrix.row B i) v) = B $$(i,i) * Matrix.vec_index v i" .
qed
thus ?thesis by auto
qed
also have "... = B $$ (i,i) ⋅⇩v v" unfolding v_def unit_vec_def by auto
finally have "B *⇩v v = B $$ (i,i) ⋅⇩v v" .
thus ?thesis unfolding v_def by simp
qed
lemma mat_vec_idx_disjunct_eq_zero:
assumes A: "A ∈ carrier_mat m n"
assumes x: "x ∈ carrier_vec n"
assumes some_zero: "∀j < n. (row A i)$j = 0 ∨ x$j = 0"
assumes i: "i < m"
shows "(A *⇩v x)$i = 0"
proof-
have dim_x: "dim_vec x = n" using x by simp
have dim_A: "dim_row A = m" "dim_col A = n" using A by blast+
have all_zero: "∀j < n. (row A i)$j * x$j = 0" using some_zero by fastforce
have "(A *⇩v x)$i = (row A i) ∙ x" by (rule index_mult_mat_vec, subst dim_A(1), rule i)
also have "… = (∑j < n. (row A i)$j * x$j)"
unfolding scalar_prod_def dim_x using atLeast0LessThan by presburger
also have "… = 0" using all_zero by simp
finally show ?thesis .
qed
section "Module Span"
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"
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
lemma submodule_image:
assumes "submodule R M' M"
shows "submodule R (f`M') N"
using assms
by (smt (verit, ccfv_threshold) submodule_def N.module_axioms f0_is_0 f_add f_im f_smult
imageE rev_image_eqI subset_iff)
lemma submodule_restrict:
assumes "submodule R M' M"
shows "mod_hom R (M.md M') (N.md (f`M')) f"
proof-
interpret M': module R "M.md M'" by (simp add: M.submodule_is_module assms)
interpret N': module R "N.md (f`M')" by (rule submodule_is_module, rule submodule_image[OF assms])
have "f ∈ module_hom R (M.md M') (N.md (f`M'))"
by (simp add: module_hom_def, meson M'.sum_simp assms f_add f_smult submodule.subset)
thus ?thesis
apply (simp add: mod_hom_def mod_hom_axioms_def)
using M'.module_axioms N'.module_axioms by blast
qed
end
section "Vector Summation"
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 "Vector Space"
context vectorspace
begin
lemma basis_subset_carrier: "basis B ⟹ B ⊆ carrier V" by (simp add: basis_def)
lemma dim_of_lin_indpt_span:
assumes li: "lin_indpt S"
assumes carrier: "S ⊆ carrier V"
assumes fin: "finite S"
shows "vectorspace.dim K (vs (span S)) = card S"
using dim_span[unfolded maximal_def, OF carrier fin] li
by fast
lemma subspace_fin_dim:
assumes W: "subspace K W V"
assumes fin: "fin_dim"
shows "vectorspace.fin_dim K (vs W)"
proof-
have ?thesis if "{𝟬⇘V⇙} = W"
using W that
by (metis empty_subsetI finite.emptyI local.carrier_vs_is_self local.span_empty span_li_not_depend(1) subspace.submod
subspace_is_vs vectorspace.fin_dim_def)
moreover have ?thesis if *: "{𝟬⇘V⇙} ≠ W"
proof-
obtain b where b: "b ∈ W ∧ b ≠ 𝟬⇘V⇙" using W * submodule_def subspace_def by blast
let ?P = "λB. B ⊆ W ∧ lin_indpt B"
have "⋀B. ?P B ⟹ finite B ∧ card B ≤ dim"
using W fin by (metis submodule_def subspace_def dual_order.trans li_le_dim(1,2))
moreover have Pb: "?P {b}"
proof-
have "b ∉ span {}" by (simp add: b local.span_empty)
moreover have "{b} ⊆ carrier V" using b W[unfolded subspace_def submodule_def] by fast
ultimately show ?thesis using lindep_span[of "{b}", simplified] b by blast
qed
ultimately obtain B where B: "finite B ∧ maximal B ?P" by (metis (no_types, lifting) maximal_exists)
have "(λS. S ⊆ W ∧ ¬ LinearCombinations.module.lin_dep K (vs W) S) = ?P"
using B[unfolded maximal_def] span_li_not_depend(2) W by auto
hence "vectorspace.basis K (vs W) B"
using B vectorspace.max_li_is_basis[OF subspace_is_vs[OF W], of B, simplified] by argo
thus ?thesis
using B[unfolded maximal_def]
unfolding vectorspace.fin_dim_def[OF subspace_is_vs[OF W]] vectorspace.basis_def[OF subspace_is_vs[OF W]]
by auto
qed
ultimately show ?thesis by argo
qed
lemma nontriv_obtain:
assumes "dim ≠ 0" "fin_dim"
obtains v where "v ∈ carrier V" "v ≠ 𝟬⇘V⇙"
proof-
obtain B where B: "basis B ∧ 0 < card B" using assms dim_basis finite_basis_exists by force
then obtain b where "b ∈ B ∧ b ≠ 𝟬⇘V⇙"
by (metis all_not_in_conv basis_def bot_nat_0.not_eq_extremum card_eq_0_iff vs_zero_lin_dep)
thus ?thesis using that[of b] B[unfolded basis_def] by blast
qed
lemma nontriv_subspace_obtain:
assumes "subspace K W V"
assumes "vectorspace.dim K (vs W) ≠ 0"
assumes "fin_dim"
obtains v where "v ∈ W" "v ≠ 𝟬⇘V⇙"
using assms vectorspace.nontriv_obtain[of K "vs W"] subspace_fin_dim subspace_is_vs by auto
lemma nontriv_exists:
assumes "dim ≠ 0" "fin_dim"
shows "∃v ∈ carrier V. v ≠ 𝟬⇘V⇙"
using nontriv_obtain[OF assms] by metis
lemma nontriv_subspace_exists:
assumes "subspace K W V"
assumes "vectorspace.dim K (vs W) ≠ 0"
assumes "fin_dim"
shows "∃v ∈ W. v ≠ 𝟬⇘V⇙"
using nontriv_subspace_obtain[OF assms] by metis
lemma dim_sum_nontriv_int:
assumes W⇩1: "subspace K W⇩1 V"
assumes W⇩2: "subspace K W⇩2 V"
assumes dim: "dim < vectorspace.dim K (vs W⇩1) + vectorspace.dim K (vs W⇩2)"
assumes fin: "fin_dim"
shows "∃v ∈ W⇩1 ∩ W⇩2. v ≠ 𝟬⇘V⇙"
proof-
obtain B⇩1 where B⇩1: "vectorspace.basis K (vs W⇩1) B⇩1" "finite B⇩1"
using W⇩1 fin subspace_fin_dim subspace_is_vs vectorspace.finite_basis_exists by blast
obtain B⇩2 where B⇩2: "vectorspace.basis K (vs W⇩2) B⇩2" "finite B⇩2"
using W⇩2 fin subspace_fin_dim subspace_is_vs vectorspace.finite_basis_exists by blast
have basis_carriers: "B⇩1 ⊆ carrier V" "B⇩2 ⊆ carrier V"
using B⇩1 W⇩1 unfolding vectorspace.basis_def[OF subspace_is_vs[OF W⇩1]] subspace_def submodule_def
using B⇩2 W⇩2 unfolding vectorspace.basis_def[OF subspace_is_vs[OF W⇩2]] subspace_def submodule_def
by auto
show ?thesis
proof(cases "B⇩1 ∩ B⇩2 ≠ {}")
case True
then obtain b where "b ∈ B⇩1 ∩ B⇩2" by blast
hence "b ∈ W⇩1 ∩ W⇩2 ∧ b ≠ 𝟬⇘V⇙"
using B⇩1 B⇩2 W⇩1 W⇩2
using basic_trans_rules(31)[of B⇩1 W⇩1 b] basic_trans_rules(31)[of B⇩2 W⇩2 b] one_zeroI
span_li_not_depend(2)[of B⇩1 W⇩1] subspace_is_vs[of W⇩2] subspace_is_vs[of W⇩1] vectorspace.basis_def[of K "vs W⇩2" B⇩2]
vectorspace.basis_def[of K "vs W⇩1" B⇩1] zero_lin_dep[of B⇩1]
by force
thus ?thesis by blast
next
case False
hence card: "card (B⇩1 ∪ B⇩2) = card B⇩1 + card B⇩2" using B⇩1(2) B⇩2(2) card_Un_disjoint by blast
hence not_li: "¬ lin_indpt (B⇩1 ∪ B⇩2)"
using li_le_dim(2)[OF fin, of "B⇩1 ∪ B⇩2"] B⇩1 B⇩2 basis_carriers dim
unfolding vectorspace.dim_basis[OF subspace_is_vs[OF W⇩1] B⇩1(2) B⇩1(1)]
unfolding vectorspace.dim_basis[OF subspace_is_vs[OF W⇩2] B⇩2(2) B⇩2(1)]
by auto
have "{} ⊆ B⇩1 ∧ lin_indpt ({} ∪ B⇩2)"
by (metis B⇩2(1) LinearCombinations.module.span_li_not_depend(2) LinearCombinations.submodule_def Un_empty_left
VectorSpace.subspace_def W⇩2 empty_subsetI local.module.carrier_vs_is_self subspace_is_vs vectorspace.basis_def)
then obtain B⇩1' where B⇩1': "maximal B⇩1' (λB⇩1'. B⇩1' ⊆ B⇩1 ∧ lin_indpt (B⇩1' ∪ B⇩2))"
using B⇩1(2) by (metis (no_types, lifting) maximal_exists_superset)
have "B⇩1' ≠ B⇩1"
using B⇩1' not_li unfolding maximal_def by fastforce
then obtain b⇩1 where b⇩1: "b⇩1 ∈ B⇩1 - B⇩1'"
using B⇩1' by (metis (lifting) maximal_def psubsetI psubset_imp_ex_mem)
let ?S = "B⇩1' ∪ B⇩2"
have "lin_dep (?S ∪ {b⇩1})" using b⇩1 B⇩1' unfolding maximal_def by auto
hence b⇩1_span: "b⇩1 ∈ span ?S"
using B⇩1'[unfolded maximal_def]
using lin_dep_iff_in_span[of ?S b⇩1] basis_carriers False b⇩1
by blast
also have "… = subspace_sum (span B⇩1') (span B⇩2)"
using span_union_is_sum[of B⇩1' B⇩2] basis_carriers B⇩1'[unfolded maximal_def] by force
finally obtain v⇩1' v⇩2 where vs: "b⇩1 = v⇩1' ⊕⇘V⇙ v⇩2 ∧ v⇩1' ∈ span B⇩1' ∧ v⇩2 ∈ span B⇩2"
unfolding submodule_sum_def by fast
have "v⇩2 ≠ 𝟬⇘V⇙"
proof(rule ccontr, clarify)
assume "v⇩2 = 𝟬⇘V⇙"
hence "b⇩1 ∈ span B⇩1'"
using vs B⇩1' basis_carriers(1)
by (metis (no_types, lifting) M.add.r_one maximal_def span_closed subset_trans)
moreover have "lin_indpt B⇩1'"
using B⇩1' by (metis (lifting) Un_subset_iff maximal_def order.refl supset_ld_is_ld)
moreover have "¬ lin_dep (B⇩1' ∪ {b⇩1})"
proof-
have "B⇩1' ∪ {b⇩1} ⊆ B⇩1"
using B⇩1' b⇩1 by (metis (lifting) DiffE insert_subset insert_union maximal_def)
thus ?thesis
using B⇩1[unfolded vectorspace.basis_def[OF subspace_is_vs[OF W⇩1]]] W⇩1
by (metis VectorSpace.subspace_def local.module.carrier_vs_is_self span_li_not_depend(2) subset_li_is_li)
qed
ultimately show False
using lin_dep_iff_in_span[of B⇩1' b⇩1] B⇩1' b⇩1 basis_carriers(1)
by (metis (no_types, lifting) Diff_iff Set.basic_monos(7) basic_trans_rules(23) maximal_def)
qed
moreover have "b⇩1 ⊖⇘V⇙ v⇩1' = v⇩2"
using B⇩1' b⇩1_span basis_carriers vs
by (smt (verit, ccfv_SIG) M.add.m_comm M.r_neg1 Un_least a_minus_def basic_trans_rules(23)
local.span_neg maximal_def span_closed)
moreover have "b⇩1 ⊖⇘V⇙ v⇩1' ∈ span B⇩1"
proof-
have "v⇩1' ∈ span B⇩1"
using vs B⇩1' by (metis (no_types, lifting) maximal_def span_is_monotone subsetD)
thus ?thesis
using b⇩1 basis_carriers calculation(2) vs by (metis Diff_iff local.span_add span_closed span_mem)
qed
moreover have "v⇩2 ∈ span B⇩2" using vs by fast
ultimately have "v⇩2 ≠ 𝟬⇘V⇙ ∧ v⇩2 ∈ span B⇩1 ∩ span B⇩2"
by fastforce
thus ?thesis
using B⇩1 B⇩2 W⇩1 W⇩2
by (metis is_module subspace_is_vs vectorspace.basis_def local.module.carrier_vs_is_self span_li_not_depend(1))
qed
qed
end
section "Linear Map"
context linear_map
begin
lemma 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 subspace_restrict:
assumes "subspace K V' V"
shows "linear_map K (V.vs V') (W.vs (T`V')) T"
using assms submodule_restrict[of V']
by (simp add: field_axioms linear_map_def mod_hom.axioms(1,2) vectorspace_def)
lemma subspace_image:
assumes "subspace K V' V"
shows "subspace K (T`V') W"
using assms submodule_image[of V'] by (meson subspace_def W.vectorspace_axioms)
lemma inj_subspace_image:
assumes inj: "inj_on T (carrier V)"
assumes subspace: "subspace K V' V"
assumes fin: "V.fin_dim"
shows "vectorspace.dim K (W.vs (T`V')) = vectorspace.dim K (V.vs V')"
proof-
interpret restrict: linear_map K "V.vs V'" "W.vs (T`V')" T using subspace_restrict[OF subspace] .
have inj': "inj_on T (carrier (V.vs V'))"
using inj subspace by (simp add: submodule_def VectorSpace.subspace_def inj_on_subset)
have carrier_im: "T`carrier (V.vs V') = carrier (W.vs (T`V'))"
using V.carrier_vs_is_self W.carrier_vs_is_self by presburger
show ?thesis
by (rule restrict.dim_eq[OF V.subspace_fin_dim[OF subspace fin] inj' carrier_im, symmetric])
qed
end
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 "Matrix as Linear Map"
locale mat_as_linear_map =
fixes A :: "'a::field mat"
fixes m n
assumes carrier: "A ∈ carrier_mat m n"
begin
abbreviation "V ≡ module_vec TYPE('a) n"
abbreviation "W ≡ module_vec TYPE('a) m"
sublocale linear_map class_ring V W "(*⇩v) A"
by (rule linear_map_mat[OF carrier])
abbreviation "f ≡ (*⇩v) A"
end
section "Matrix Isometry"
locale isometry_mat = mat_as_linear_map A m n for A :: "complex mat" and m n +
assumes isom: "A⇧H * A = 1⇩m n"
begin
lemma preserves_norm: "v ∈ carrier_vec n ⟹ vec_norm v = vec_norm (f v)"
by (metis adjoint_is_conjugate_transpose carrier inner_prod_mult_mat_vec_right isom one_mult_mat_vec
vec_norm_def)
lemma is_inj: "inj_on f (carrier V)"
by (smt (verit, ccfv_threshold) adjoint_dim' adjoint_is_conjugate_transpose assoc_mult_mat_vec carrier inj_on_def
isom one_mult_mat_vec vec_space.cV)
end
section "Compression"
lemma compression_is_hermitian:
assumes B: "B ∈ carrier_mat n m"
assumes A: "A ∈ carrier_mat n n" "hermitian A"
shows "hermitian (B⇧H * A * B)" "B⇧H * A * B ∈ carrier_mat m m"
proof-
have "((B⇧H * A) * B)⇧H = B⇧H * (B⇧H * A)⇧H"
using A(1) B
by (metis adjoint_dim' adjoint_is_conjugate_transpose adjoint_mult mult_carrier_mat)
also have "… = B⇧H * (A⇧H * B⇧H⇧H)"
using A(1) assms(1)
by (metis adjoint_dim' adjoint_is_conjugate_transpose adjoint_mult)
also have "… = B⇧H * A * B"
using A B
by (smt (verit, best) Matrix.transpose_transpose adjoint_dim' adjoint_is_conjugate_transpose
assoc_mult_mat conjugate_id hermitian_def transpose_conjugate)
finally show "hermitian (B⇧H * A * B)"
unfolding hermitian_def adjoint_is_conjugate_transpose[of "B⇧H * A * B"] .
show "B⇧H * A * B ∈ carrier_mat m m"
using A(1) B by (meson More_Matrix.carrier_vec_conjugate mult_carrier_mat transpose_carrier_mat)
qed
section "Submatrix"
subsection "Submatrix of Injective Function on Indices, as Compression"
text "Note, with this definition of submatrix, reordering the indices is possible."
definition submatrix_of_inj :: "'a mat ⇒ (nat ⇒ nat) ⇒ (nat ⇒ nat) ⇒ nat ⇒ nat ⇒ 'a mat" where
"submatrix_of_inj A f g m n ≡ mat m n (λ(i,j). A$$(f i, g j))"
lemma submatrix_of_inj_as_compression:
fixes A :: "complex mat"
fixes f :: "nat ⇒ nat"
assumes A: "A ∈ carrier_mat n n"
assumes f: "f : {..<m} → {..<n}"
assumes inj: "inj_on f {..<m}"
defines "B ≡ submatrix_of_inj A f f m m"
defines "(Q::complex mat) ≡ mat n m (λ(i,j). if i = f j then 1 else 0)"
shows "B = Q⇧H * A * Q" "isometry_mat Q n m" "Q ∈ carrier_mat n m"
proof-
show dim: "Q ∈ carrier_mat n m" unfolding Q_def by simp
note m_leq_n = card_inj[OF f inj, simplified]
let ?φ = "λj k. if k = f j then 1 else 0"
have *: "⋀j. j < m ⟹ (∑k<n. cnj (?φ j k) * ?φ j k) = 1"
proof-
fix j assume j: "j < m"
have fj: "f j ∈ {..<n}" using f j by blast
have "(∑k<n. cnj (?φ j k) * ?φ j k) = (∑k ∈ {..<n} - {f j}. cnj (?φ j k) * ?φ j k) + (cnj (?φ j (f j)) * ?φ j (f j))"
using fj by (subst sum_diff1, simp_all)
thus "(∑k<n. cnj (?φ j k) * ?φ j k) = 1" by simp
qed
have "⋀i j k. i < m ⟹ j < m ⟹ i ≠ j ⟹ k < n ⟹ cnj (?φ i k) * ?φ j k = 0"
using inj by (simp add: inj_on_eq_iff)
hence **: "⋀i j. i < m ⟹ j < m ⟹ i ≠ j ⟹ (∑k<n. cnj (?φ i k) * ?φ j k) = 0"
by (meson lessThan_iff sum.not_neutral_contains_not_neutral)
have "Q⇧H * Q = 1⇩m m"
by (rule eq_matI, auto simp: Q_def m_leq_n * **)
thus "isometry_mat Q n m"
using dim isometry_mat_axioms_def[of Q m] mat_as_linear_map.intro[of Q n m]
unfolding isometry_mat_def
by blast
have "⋀i j. i < m ⟹ j < m ⟹ row (Q⇧H * A) i $ (f j) = A$$(f i, f j)"
proof-
fix i j assume i: "i < m" and j: "j < m"
have fj: "f j < n" using f j m_leq_n by blast
have "row (Q⇧H * A) i $ (f j) = row A (f i) $ (f j)"
using i fj A f sum_diff1[of "{..<n}" "λk. cnj (if k = f i then 1 else 0) * A $$ (k, f j)" "f i"]
by (subst adjoint_is_conjugate_transpose) (force simp: Q_def row_def adjoint_def)
thus "row (Q⇧H * A) i $ (f j) = A$$(f i, f j)"
using A fj by (metis carrier_matD(2) index_vec row_def)
qed
hence "⋀i j k. i < m ⟹ j < m ⟹ k < n ⟹ row (Q⇧H * A) i $ k * col Q j $ k = (if k = f j then A$$(f i, f j) else 0)"
unfolding Q_def row_def col_def times_mat_def scalar_prod_def by force
hence *: "⋀i j. i < dim_row Q⇧H ⟹ j < dim_col Q ⟹ B $$ (i, j) = row (Q⇧H * A) i ∙ col Q j"
using dim m_leq_n f by (auto simp: scalar_prod_def B_def submatrix_of_inj_def)
show "B = Q⇧H * A * Q"
apply (rule eq_matI, simp add: *)
using dim A by (simp add: B_def submatrix_of_inj_def)+
qed
lemma submatrix_of_inj_as_compression_obt:
fixes A :: "complex mat"
fixes f :: "nat ⇒ nat"
assumes A: "A ∈ carrier_mat n n"
assumes f: "f : {..<m} → {..<n}"
assumes inj: "inj_on f {..<m}"
defines "B ≡ submatrix_of_inj A f f m m"
obtains Q where "B = Q⇧H * A * Q" "isometry_mat Q n m" "Q ∈ carrier_mat n m"
using submatrix_of_inj_as_compression[OF assms(1-3), folded B_def] by blast
subsection "Submatrix of @{const pick} Function, as Compression"
lemma submatrix_inj:
assumes A: "A ∈ carrier_mat m n"
assumes I: "I ⊆ {..<m}"
assumes J: "J ⊆ {..<n}"
defines "m' ≡ card I"
defines "n' ≡ card J"
defines "B ≡ submatrix A I J"
defines "f ≡ λi. pick I i"
defines "g ≡ λj. pick J j"
shows "f : {..<m'} → {..<m}" "g : {..<n'} → {..<n}"
"inj_on f {..<m'}" "inj_on g {..<n'}"
"B = submatrix_of_inj A f g m' n'"
proof-
show "f : {..<m'} → {..<m}" unfolding f_def m'_def using I(1) pick_in_set_le by fastforce
show "g : {..<n'} → {..<n}" unfolding g_def n'_def using J(1) pick_in_set_le by fastforce
show "inj_on f {..<m'}"
unfolding inj_on_def f_def m'_def by (metis lessThan_iff nat_neq_iff pick_mono_le)
show "inj_on g {..<n'}"
unfolding inj_on_def g_def n'_def by (metis lessThan_iff nat_neq_iff pick_mono_le)
have "card {i. i < dim_row A ∧ i ∈ I} = card I"
using A I(1)
by (smt (verit, del_insts) basic_trans_rules(31) carrier_matD(1) equalityI lessThan_iff mem_Collect_eq subsetI)
moreover have "card {j. j < dim_col A ∧ j ∈ J} = card J"
using A J(1)
by (smt (verit, del_insts) basic_trans_rules(31) carrier_matD(2) equalityI lessThan_iff mem_Collect_eq subsetI)
ultimately show "B = submatrix_of_inj A f g m' n'"
unfolding submatrix_of_inj_def B_def submatrix_def f_def g_def m'_def n'_def by argo
qed
lemma submatrix_inj_square:
assumes A: "A ∈ carrier_mat n n"
assumes I: "I ⊆ {..<n}"
defines "m ≡ card I"
defines "B ≡ submatrix A I I"
defines "f ≡ λi. pick I i"
shows "f : {..<m} → {..<n}" "inj_on f {..<m}" "B = submatrix_of_inj A f f m m"
by (rule submatrix_inj[OF A I I, folded m_def B_def f_def])+
lemma submatrix_inj_obt:
assumes A: "A ∈ carrier_mat m n"
assumes I: "I ⊆ {..<m}"
assumes J: "J ⊆ {..<n}"
defines "m' ≡ card I"
defines "n' ≡ card J"
defines "B ≡ submatrix A I J"
obtains f g where "f : {..<m'} → {..<m}" "g : {..<n'} → {..<n}"
"inj_on f {..<m'}" "inj_on g {..<n'}"
"B = submatrix_of_inj A f g m' n'"
using submatrix_inj[OF A I J] m'_def n'_def B_def by blast
lemma submatrix_inj_square_obt:
assumes A: "A ∈ carrier_mat n n"
assumes I: "I ⊆ {..<n}"
defines "m ≡ card I"
defines "B ≡ submatrix A I I"
obtains f where "f : {..<m} → {..<n}" "inj_on f {..<m}" "B = submatrix_of_inj A f f m m"
using submatrix_inj_square[OF A I] m_def B_def by blast
lemma submatrix_as_compression:
fixes A :: "complex mat"
fixes f :: "nat ⇒ nat"
assumes A: "A ∈ carrier_mat n n"
assumes I: "I ⊆ {..<n}"
defines "m ≡ card I"
defines "B ≡ submatrix A I I"
defines "(Q::complex mat) ≡ mat n m (λ(i,j). if i = pick I j then 1 else 0)"
shows "B = Q⇧H * A * Q" "isometry_mat Q n m" "Q ∈ carrier_mat n m"
using submatrix_inj_square[OF A I] submatrix_of_inj_as_compression[OF A]
unfolding m_def B_def Q_def
by presburger+
lemma submatrix_as_compression_obt:
fixes A :: "complex mat"
assumes "A ∈ carrier_mat n n"
assumes "I ⊆ {..<n}"
defines "m ≡ card I"
defines "B ≡ submatrix A I I"
obtains Q where "B = Q⇧H * A * Q" "isometry_mat Q n m"
using submatrix_as_compression[OF assms(1,2)] m_def B_def by blast
section "Schur Decomposition"
context
fixes A Λ U :: "'a::{conjugatable_field,real_algebra_1,ord} mat"
fixes n
assumes *: "real_diag_decomp A Λ U"
defines "n ≡ dim_row A"
begin
lemma diag_decomp_inverse: "inverts_mat U (adjoint U)"
using *
unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def similar_mat_wit_def
using Complex_Matrix.unitary_def by blast
lemma diag_decomp_invertible: "invertible_mat U"
using diag_decomp_inverse *
by (meson Complex_Matrix.unitary_def carrier_matD(2) invertible_mat_def real_diag_decompD(1) square_mat.simps unitaryD2
unitary_diagD(3))
lemma diag_decomp_cols_distinct: "distinct (cols U)"
using diag_decomp_invertible *
by (metis carrier_mat_triv invertible_det invertible_mat_def order_less_irrefl square_mat.simps vec_space.low_rank_det_zero
vec_space.non_distinct_low_rank)
lemma diag_decomp_ortho: "corthogonal_mat U"
using unitary_is_corthogonal *
unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def unitary_def
by blast
private lemma carriers: "A ∈ carrier_mat n n" "U ∈ carrier_mat n n" "U⇧H ∈ carrier_mat n n" "Λ ∈ carrier_mat n n"
using *[unfolded real_diag_decomp_def unitary_diag_def unitarily_equiv_def similar_mat_wit_def,
folded adjoint_is_conjugate_transpose]
using insert_subset n_def
by metis+
lemma diag_decomp_cols_lin_indpt: "module.lin_indpt class_ring (module_vec TYPE('a) n) (set (cols U))"
using * carriers unfolding real_diag_decomp_def unitary_diag_def unitary_def n_def
by (metis diag_decomp_invertible idom_vec.lin_dep_cols_imp_det_0 invertible_det)
lemma real_diag_decomp_eq: "A = U * Λ * U⇧H"
using *[unfolded real_diag_decomp_def unitary_diag_def unitarily_equiv_def similar_mat_wit_def]
by (metis adjoint_is_conjugate_transpose)
private lemma U_unitary: "U⇧H * U = 1⇩m n ∧ U * U⇧H = 1⇩m n"
using *[unfolded real_diag_decomp_def unitary_diag_def unitarily_equiv_def unitary_def]
using n_def carriers
by (metis adjoint_is_conjugate_transpose carrier_matD(2) inverts_mat_def similar_mat_wit_def)
private lemma Λ_diag: "diagonal_mat Λ"
using * real_diag_decompD(1) unitary_diagD(2) by blast
lemma diag_decomp_cols_are_eigenvectors:
assumes "i < n"
shows "eigenvector A (col U i) ((diag_mat Λ)!i)" (is "eigenvector A ?v ?μ")
proof-
have "A *⇩v ?v = (U * Λ) *⇩v (U⇧H *⇩v ?v)"
using * real_diag_decomp_eq carriers assoc_mult_mat_vec[of "U * Λ" n n "U⇧H" n ?v] by force
also have "… = (U * Λ) *⇩v (col (1⇩m n) i)"
using U_unitary n_def assms carriers
by (metis (mono_tags, lifting) adjoint_is_conjugate_transpose col_mult2)
also have "… = U *⇩v (Λ *⇩v (unit_vec n i))"
using * real_diag_decomp_eq carriers col_one assms by fastforce
also have "… = U *⇩v ((diag_mat Λ)!i ⋅⇩v (unit_vec n i))"
using *[unfolded real_diag_decomp_def unitary_diag_def]
using diagonal_unit_vec'[OF carriers(4) Λ_diag, of i] assms carriers(4)
unfolding diag_mat_def
by force
also have "… = (diag_mat Λ)!i ⋅⇩v (U *⇩v (unit_vec n i))"
using carriers(2) by auto
also have "… = (diag_mat Λ)!i ⋅⇩v (col U i)"
by (simp add: assms carriers(2) mat_unit_vec_col)
finally show ?thesis
unfolding eigenvector_def
using assms carriers(2) n_def
by (metis carrier_matD(1,2) col_dim conjugate_zero_vec corthogonal_matD diag_decomp_ortho scalar_prod_left_zero)
qed
end
section "Rayleigh Quotient"
definition rayleigh_quotient_complex :: "complex mat ⇒ complex vec ⇒ complex" ("ρ⇩c") where
"ρ⇩c M x = (QF M x) / (x ∙c x)"
definition rayleigh_quotient :: "complex mat ⇒ complex vec ⇒ real" ("ρ") where
"ρ M x = Re (ρ⇩c M x)"
lemma rayleigh_quotient_negative: "A ∈ carrier_mat n n ⟹ x ∈ carrier_vec n ⟹ ρ A x = - ρ (- A) x"
by (simp add: rayleigh_quotient_def rayleigh_quotient_complex_def)
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 add: rayleigh_quotient_complex_def)
also have "… = (((k ⋅⇩v (A *⇩v v)) ∙c (k ⋅⇩v v))) / (((k ⋅⇩v v) ∙c (k ⋅⇩v v)))"
using assms(1,2) inner_prod_smult_right by force
also have "… = ((((A *⇩v (k ⋅⇩v v))) ∙c (k ⋅⇩v v))) / (((k ⋅⇩v v) ∙c (k ⋅⇩v v)))"
using assms by (metis mult_mat_vec)
also have "… = ρ⇩c A (k ⋅⇩v v)" by (simp add: rayleigh_quotient_complex_def)
finally show ?thesis .
qed
lemma rayleigh_quotient_scale_complex:
assumes "A ∈ carrier_mat n n"
assumes "v ∈ carrier_vec n"
assumes "k ≠ 0"
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)"
using assms(1,2)
by (smt (verit, ccfv_SIG) cross3_simps(11)inner_prod_smult_left_right mult_conj_cmod_square mult_mat_vec
mult_mat_vec_carrier quadratic_form_def)
moreover have "?v' ∙c ?v' = (cmod k)^2 * (v ∙c v)"
using assms(2) complex_norm_square inner_prod_smult_left_right by force
ultimately show "ρ A ?v' = ρ A v"
by (simp add: rayleigh_quotient_def rayleigh_quotient_complex_def assms(3))
qed
lemma rayleigh_quotient_scale_real:
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)
context cmplx_herm_mat
begin
lemma hermitian_rayleigh_quotient_real:
assumes "v ∈ carrier_vec n"
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 by fastforce
ultimately show ?thesis unfolding rayleigh_quotient_complex_def using Reals_divide by blast
qed
lemma rayleigh_quotient_QF:
assumes x: "x ≠ 0⇩v n" "x ∈ carrier_vec n"
shows "ρ A x = (QF A x) / (vec_norm x)⇧2"
using hermitian_rayleigh_quotient_real[OF x(2,1)]
unfolding rayleigh_quotient_def rayleigh_quotient_complex_def vec_norm_def
using of_real_Re power2_csqrt
by presburger
end
lemma rayleigh_eigenvector:
assumes "eigenvector A v e"
shows "ρ A v = e"
unfolding rayleigh_quotient_def rayleigh_quotient_complex_def quadratic_form_def
using assms[unfolded eigenvector_def]
by force
end