Theory Eigenvalues
section ‹‹Eigenvalues› -- Material related to eigenvalues and eigenspaces›
theory Eigenvalues
imports
Weak_Operator_Topology
Misc_Tensor_Product_TTS
begin
unbundle cblinfun_syntax
definition normal_op :: ‹('a::chilbert_space ⇒⇩C⇩L 'a) ⇒ bool› where
‹normal_op A ⟷ A o⇩C⇩L A* = A* o⇩C⇩L A›
definition eigenvalues :: ‹('a::complex_normed_vector ⇒⇩C⇩L 'a) ⇒ complex set› where
‹eigenvalues a = {x. eigenspace x a ≠ 0}›
definition invariant_subspace :: ‹'a::complex_inner ccsubspace ⇒ ('a ⇒⇩C⇩L 'a) ⇒ bool› where
‹invariant_subspace S A ⟷ A *⇩S S ≤ S›
lemma invariant_subspaceI: ‹A *⇩S S ≤ S ⟹ invariant_subspace S A›
by (simp add: invariant_subspace_def)
definition reducing_subspace :: ‹'a::complex_inner ccsubspace ⇒ ('a ⇒⇩C⇩L 'a) ⇒ bool› where
‹reducing_subspace S A ⟷ invariant_subspace S A ∧ invariant_subspace (-S) A›
lemma reducing_subspaceI: ‹A *⇩S S ≤ S ⟹ A *⇩S (-S) ≤ -S ⟹ reducing_subspace S A›
by (simp add: reducing_subspace_def invariant_subspace_def)
lemma reducing_subspace_ortho[simp]: ‹reducing_subspace (-S) A ⟷ reducing_subspace S A›
for S :: ‹'a::chilbert_space ccsubspace›
by (auto simp: reducing_subspace_def)
lemma invariant_subspace_bot[simp]: ‹invariant_subspace ⊥ A›
by (simp add: invariant_subspaceI)
lemma invariant_subspace_top[simp]: ‹invariant_subspace ⊤ A›
by (simp add: invariant_subspaceI)
lemma reducing_subspace_bot[simp]: ‹reducing_subspace ⊥ A›
by (metis cblinfun_image_bot eq_refl orthogonal_spaces_bot_right orthogonal_spaces_leq_compl reducing_subspaceI)
lemma reducing_subspace_top[simp]: ‹reducing_subspace ⊤ A›
by (simp add: reducing_subspace_def)
lemma kernel_uminus[simp]: "kernel (-A) = kernel A"
for a :: complex and A :: "(_,_) cblinfun"
by transfer auto
lemma kernel_scaleC': "kernel (a *⇩C A) = (if a = 0 then ⊤ else kernel A)"
for a :: complex and A :: "(_,_) cblinfun"
by (cases "a = 0") auto
lemma eigenvalues_0[simp]: ‹eigenvalues (0 :: 'a::{not_singleton,complex_normed_vector} ⇒⇩C⇩L 'a) = {0}›
by (auto simp: eigenvalues_def eigenspace_def kernel_scaleC')
lemma nonzero_ccsubspace_contains_unit_vector:
assumes ‹S ≠ 0›
shows ‹∃ψ. ψ ∈ space_as_set S ∧ norm ψ = 1›
proof -
from assms
obtain ψ where ψ: ‹ψ ∈ space_as_set S› ‹ψ ≠ 0›
by transfer (auto simp: complex_vector.subspace_0)
have ‹sgn ψ ∈ space_as_set S›
using ψ by (simp add: complex_vector.subspace_scale scaleR_scaleC sgn_div_norm)
moreover have ‹norm (sgn ψ) = 1›
by (simp add: ‹ψ ≠ 0› norm_sgn)
ultimately show ?thesis
by auto
qed
lemma unit_eigenvector_ex:
assumes ‹x ∈ eigenvalues a›
shows ‹∃h. norm h = 1 ∧ a h = x *⇩C h›
proof -
from assms have ‹eigenspace x a ≠ 0›
by (simp add: eigenvalues_def)
then obtain ψ where ψ_ev: ‹ψ ∈ space_as_set (eigenspace x a)› and ‹ψ ≠ 0›
using nonzero_ccsubspace_contains_unit_vector by force
define h where ‹h = sgn ψ›
with ‹ψ ≠ 0› have ‹norm h = 1›
by (simp add: norm_sgn)
from ψ_ev have ‹h ∈ space_as_set (eigenspace x a)›
by (simp add: h_def sgn_in_spaceI)
then have ‹a *⇩V h = x *⇩C h›
unfolding eigenspace_def
by (transfer' fixing: x) simp
with ‹norm h = 1› show ?thesis
by auto
qed
lemma eigenvalue_norm_bound:
assumes ‹e ∈ eigenvalues a›
shows ‹norm e ≤ norm a›
proof -
from assms obtain h where ‹norm h = 1› and ah_eh: ‹a h = e *⇩C h›
using unit_eigenvector_ex by blast
have ‹cmod e = norm (e *⇩C h)›
by (simp add: ‹norm h = 1›)
also have ‹… = norm (a h)›
using ah_eh by presburger
also have ‹… ≤ norm a›
by (metis ‹norm h = 1› cblinfun.real.bounded_linear_right mult_cancel_left1 norm_cblinfun.rep_eq onorm)
finally show ‹cmod e ≤ norm a›
by -
qed
lemma eigenvalue_selfadj_real:
assumes ‹e ∈ eigenvalues a›
assumes ‹selfadjoint a›
shows ‹e ∈ ℝ›
proof -
from assms obtain h where ‹norm h = 1› and ah_eh: ‹a h = e *⇩C h›
using unit_eigenvector_ex by blast
have ‹e = h ∙⇩C (e *⇩C h)›
by (metis ‹norm h = 1› cinner_simps(6) mult_cancel_left1 norm_one one_cinner_one power2_norm_eq_cinner power2_norm_eq_cinner)
also have ‹… = h ∙⇩C a h›
by (simp add: ah_eh)
also from assms(2) have ‹… ∈ ℝ›
using cinner_selfadjoint_real selfadjoint_def by blast
finally show ‹e ∈ ℝ›
by -
qed
lemma is_Sup_imp_ex_tendsto:
fixes X :: ‹'a::{linorder_topology,first_countable_topology} set›
assumes sup: ‹is_Sup X l›
assumes ‹X ≠ {}›
shows ‹∃f. range f ⊆ X ∧ f ⇢ l›
proof (cases ‹∃x. x < l›)
case True
obtain A :: ‹nat ⇒ 'a set› where openA: ‹open (A n)› and lA: ‹l ∈ A n›
and fl: ‹(⋀n. f n ∈ A n) ⟹ f ⇢ l› for n f
by (rule Topological_Spaces.countable_basis[of l]) blast
obtain f where fAX: ‹f n ∈ A n ∩ X› for n
proof (atomize_elim, intro choice allI)
fix n :: nat
from True obtain x where ‹x < l›
by blast
from open_left[OF openA lA this]
obtain b where ‹b < l› and bl_A: ‹{b<..l} ⊆ A n›
by blast
from sup ‹b < l› obtain x where ‹x ∈ X› and ‹x > b›
by (meson is_Sup_def leD leI)
from ‹x ∈ X› sup have ‹x ≤ l›
by (simp add: is_Sup_def)
from ‹x ≤ l› and ‹x > b› and bl_A
have ‹x ∈ A n›
by fastforce
with ‹x ∈ X›
show ‹∃x. x ∈ A n ∩ X›
by blast
qed
with fl have ‹f ⇢ l›
by auto
moreover from fAX have ‹range f ⊆ X›
by auto
ultimately show ?thesis
by blast
next
case False
from ‹X ≠ {}› obtain x where ‹x ∈ X›
by blast
with ‹is_Sup X l› have ‹x ≤ l›
by (simp add: is_Sup_def)
with False have ‹x = l›
using basic_trans_rules(17) by auto
with ‹x ∈ X› have ‹l ∈ X›
by simp
define f where ‹f n = l› for n :: nat
then have ‹f ⇢ l›
by (auto intro!: simp: f_def[abs_def])
moreover from ‹l ∈ X› have ‹range f ⊆ X›
by (simp add: f_def)
ultimately show ?thesis
by blast
qed
lemma eigenvaluesI:
assumes ‹A *⇩V h = e *⇩C h›
assumes ‹h ≠ 0›
shows ‹e ∈ eigenvalues A›
proof -
from assms have ‹h ∈ space_as_set (eigenspace e A)›
by (simp add: eigenspace_def kernel.rep_eq cblinfun.diff_left)
moreover from ‹h ≠ 0› have ‹h ∉ space_as_set ⊥›
by transfer simp
ultimately have ‹eigenspace e A ≠ ⊥›
by fastforce
then show ?thesis
by (simp add: eigenvalues_def)
qed
lemma tendsto_diff_const_left_rewrite:
fixes c d :: ‹'a::{topological_group_add, ab_group_add}›
assumes ‹((λx. f x) ⤏ c - d) F›
shows ‹((λx. c - f x) ⤏ d) F›
by (auto intro!: assms tendsto_eq_intros)
lemma not_not_singleton_no_eigenvalues:
fixes a :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'a›
assumes ‹¬ class.not_singleton TYPE('a)›
shows ‹eigenvalues a = {}›
proof (rule equals0I)
fix e assume ‹e ∈ eigenvalues a›
then have ‹eigenspace e a ≠ ⊥›
by (simp add: eigenvalues_def)
then obtain h where ‹norm h = 1› and ‹h ∈ space_as_set (eigenspace e a)›
using nonzero_ccsubspace_contains_unit_vector by auto
from assms have ‹h = 0›
by (rule not_not_singleton_zero)
with ‹norm h = 1›
show False
by simp
qed
lemma cblinfun_cinner_eq0I:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀h. h ∙⇩C a h = 0›
shows ‹a = 0›
by (rule cblinfun_cinner_eqI) (use assms in simp)
lemma normal_op_iff_adj_same_norms:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
shows ‹normal_op a ⟷ (∀h. norm (a h) = norm ((a*) h))›
proof -
have aux: ‹(⋀h. a h = b h) ==> (∀h. a h = (0::complex)) ⟷ (∀h. b h = (0::real))› for a :: ‹'a ⇒ complex› and b :: ‹'a ⇒ real›
by simp
have ‹normal_op a ⟷ (a* o⇩C⇩L a) - (a o⇩C⇩L a*) = 0›
using normal_op_def by force
also have ‹… ⟷ (∀h. h ∙⇩C ((a* o⇩C⇩L a) - (a o⇩C⇩L a*)) h = 0)›
by (auto intro!: cblinfun_cinner_eqI simp: cblinfun.diff_left cinner_diff_right
simp flip: cblinfun_apply_cblinfun_compose)
also have ‹… ⟷ (∀h. (norm (a h))⇧2 - (norm ((a*) h))⇧2 = 0)›
proof (rule aux)
fix h
have ‹(norm (a *⇩V h))⇧2 - (norm (a* *⇩V h))⇧2
= (a *⇩V h) ∙⇩C (a *⇩V h) - (a* *⇩V h) ∙⇩C (a* *⇩V h)›
by (simp add: of_real_diff flip: cdot_square_norm of_real_power)
also have ‹… = h ∙⇩C ((a* o⇩C⇩L a) - (a o⇩C⇩L a*)) h›
by (simp add: cblinfun.diff_left cinner_diff_right cinner_adj_left
cinner_adj_right flip: cinner_adj_left)
finally show ‹h ∙⇩C ((a* o⇩C⇩L a) - (a o⇩C⇩L a*)) h = (norm (a *⇩V h))⇧2 - (norm (a* *⇩V h))⇧2›
by simp
qed
also have ‹… ⟷ (∀h. norm (a h) = norm ((a*) h))›
by simp
finally show ?thesis.
qed
lemma normal_op_same_eigenspace_as_adj:
assumes ‹normal_op a›
shows ‹eigenspace l a = eigenspace (cnj l) (a* )›
proof -
from ‹normal_op a›
have ‹normal_op (a - l *⇩C id_cblinfun)›
by (auto intro!: simp: normal_op_def cblinfun_compose_minus_left
cblinfun_compose_minus_right adj_minus scaleC_diff_right)
then have *: ‹norm ((a - l *⇩C id_cblinfun) h) = norm (((a - l *⇩C id_cblinfun)*) h)› for h
using normal_op_iff_adj_same_norms by blast
show ?thesis
proof (rule ccsubspace_eqI)
fix h
have ‹h ∈ space_as_set (eigenspace l a) ⟷ norm ((a - l *⇩C id_cblinfun) h) = 0›
by (simp add: eigenspace_def kernel_member_iff)
also have ‹… ⟷ norm (((a*) - cnj l *⇩C id_cblinfun) h) = 0›
by (simp add: "*" adj_minus)
also have ‹… ⟷ h ∈ space_as_set (eigenspace (cnj l) (a*))›
by (simp add: eigenspace_def kernel_member_iff)
finally show ‹h ∈ space_as_set (eigenspace l a) ⟷ h ∈ space_as_set (eigenspace (cnj l) (a*))›.
qed
qed
lemma normal_op_adj_eigenvalues:
assumes ‹normal_op a›
shows ‹eigenvalues (a*) = cnj ` eigenvalues a›
by (auto intro!: complex_cnj_cnj[symmetric] image_eqI
simp: eigenvalues_def assms normal_op_same_eigenspace_as_adj)
lemma invariant_subspace_iff_PAP:
‹invariant_subspace S A ⟷ Proj S o⇩C⇩L A o⇩C⇩L Proj S = A o⇩C⇩L Proj S›
proof -
define S' where ‹S' = space_as_set S›
have ‹invariant_subspace S A ⟷ (∀h∈S'. A h ∈ S')›
proof safe
fix h assume A: "invariant_subspace S A" and h: "h ∈ S'"
from h have "A *⇩V h ∈ space_as_set (A *⇩S S)"
using cblinfun_apply_in_image'[of h S A] unfolding S'_def by auto
also have "space_as_set (A *⇩S S) ⊆ S'"
using A unfolding S'_def invariant_subspace_def less_eq_ccsubspace_def by auto
finally show "A *⇩V h ∈ S'" .
next
assume *: "∀h∈S'. A *⇩V h ∈ S'"
hence "A *⇩S S ≤ S"
unfolding S'_def using cblinfun_image_less_eqI by blast
thus "invariant_subspace S A"
unfolding invariant_subspace_def less_eq_ccsubspace_def map_fun_def o_def id_def .
qed
also have ‹… ⟷ (∀h. A *⇩V Proj S *⇩V h ∈ S')›
by (metis (no_types, lifting) Proj_fixes_image Proj_range S'_def cblinfun_apply_in_image)
also have ‹… ⟷ (∀h. Proj S *⇩V A *⇩V Proj S *⇩V h = A *⇩V Proj S *⇩V h)›
using Proj_fixes_image S'_def space_as_setI_via_Proj by blast
also have ‹… ⟷ Proj S o⇩C⇩L A o⇩C⇩L Proj S = A o⇩C⇩L Proj S›
by (auto intro!: cblinfun_eqI simp:
simp flip: cblinfun_apply_cblinfun_compose cblinfun_compose_assoc)
finally show ?thesis
by -
qed
lemma reducing_iff_PA:
‹reducing_subspace S A ⟷ Proj S o⇩C⇩L A = A o⇩C⇩L Proj S›
proof (rule iffI)
assume red: ‹reducing_subspace S A›
define P where ‹P = Proj S›
from red have AP: ‹P o⇩C⇩L A o⇩C⇩L P = A o⇩C⇩L P›
by (simp add: invariant_subspace_iff_PAP reducing_subspace_def P_def)
from red have ‹reducing_subspace (- S) A›
by simp
then have ‹(id_cblinfun - P) o⇩C⇩L A o⇩C⇩L (id_cblinfun - P) = A o⇩C⇩L (id_cblinfun - P)›
using invariant_subspace_iff_PAP[of ‹- S›] reducing_subspace_def P_def Proj_ortho_compl
by metis
then have ‹P o⇩C⇩L A = P o⇩C⇩L A o⇩C⇩L P›
by (simp add: cblinfun_compose_minus_left cblinfun_compose_minus_right)
with AP show ‹P o⇩C⇩L A = A o⇩C⇩L P›
by simp
next
define P where ‹P = Proj S›
assume ‹P o⇩C⇩L A = A o⇩C⇩L P›
then have ‹P o⇩C⇩L A o⇩C⇩L P = A o⇩C⇩L P o⇩C⇩L P›
by simp
then have ‹P o⇩C⇩L A o⇩C⇩L P = A o⇩C⇩L P›
by (metis P_def Proj_idempotent cblinfun_assoc_left(1))
then have ‹invariant_subspace S A›
by (simp add: P_def invariant_subspace_iff_PAP)
have ‹(id_cblinfun - P) o⇩C⇩L A o⇩C⇩L (id_cblinfun - P) = A o⇩C⇩L (id_cblinfun - P)›
by (metis (no_types, opaque_lifting) P_def Proj_idempotent Proj_ortho_compl ‹P o⇩C⇩L A = A o⇩C⇩L P› cblinfun_assoc_left(1) cblinfun_compose_id_left cblinfun_compose_minus_left cblinfun_compose_minus_right)
then have ‹invariant_subspace (- S) A›
by (simp add: P_def Proj_ortho_compl invariant_subspace_iff_PAP)
with ‹invariant_subspace S A›
show ‹reducing_subspace S A›
using reducing_subspace_def by blast
qed
lemma reducing_iff_also_adj_invariant:
shows ‹reducing_subspace S A ⟷ invariant_subspace S A ∧ invariant_subspace S (A*)›
proof (intro iffI conjI; (erule conjE)?)
assume ‹invariant_subspace S A› and ‹invariant_subspace S (A*)›
have ‹invariant_subspace (- S) A›
proof (intro invariant_subspaceI cblinfun_image_less_eqI)
fix h assume ‹h ∈ space_as_set (- S)›
show ‹A *⇩V h ∈ space_as_set (- S)›
proof (unfold uminus_ccsubspace.rep_eq, intro orthogonal_complementI)
fix g assume ‹g ∈ space_as_set S›
with ‹invariant_subspace S (A*)› have ‹(A*) g ∈ space_as_set S›
by (metis Proj_compose_cancelI Proj_range cblinfun_apply_in_image' cblinfun_fixes_range invariant_subspace_def space_as_setI_via_Proj)
have ‹A h ∙⇩C g = h ∙⇩C (A*) g›
by (simp add: cinner_adj_right)
also from ‹(A*) g ∈ space_as_set S› and ‹h ∈ space_as_set (- S)›
have ‹… = 0›
using orthogonal_spaces_def orthogonal_spaces_leq_compl by blast
finally show ‹A h ∙⇩C g = 0›
by blast
qed
qed
with ‹invariant_subspace S A›
show ‹reducing_subspace S A›
using reducing_subspace_def by blast
next
assume ‹reducing_subspace S A›
then show ‹invariant_subspace S A›
using reducing_subspace_def by blast
show ‹invariant_subspace S (A*)›
by (metis ‹reducing_subspace S A› adj_Proj adj_cblinfun_compose reducing_iff_PA reducing_subspace_def)
qed
lemma eigenspace_is_reducing:
assumes ‹normal_op a›
shows ‹reducing_subspace (eigenspace l a) a›
proof (unfold reducing_iff_also_adj_invariant invariant_subspace_def,
intro conjI cblinfun_image_less_eqI subsetI)
fix h
assume h_eigen: ‹h ∈ space_as_set (eigenspace l a)›
then have ‹a h = l *⇩C h›
by (simp add: eigenspace_memberD)
also have ‹… ∈ space_as_set (eigenspace l a)›
by (simp add: Proj_fixes_image cblinfun.scaleC_right h_eigen space_as_setI_via_Proj)
finally show ‹a h ∈ space_as_set (eigenspace l a)›.
next
fix h
assume h_eigen: ‹h ∈ space_as_set (eigenspace l a)›
then have ‹h ∈ space_as_set (eigenspace (cnj l) (a*))›
by (simp add: assms normal_op_same_eigenspace_as_adj)
then have ‹(a*) h = cnj l *⇩C h›
by (simp add: eigenspace_memberD)
also have ‹… ∈ space_as_set (eigenspace l a)›
by (simp add: Proj_fixes_image cblinfun.scaleC_right h_eigen space_as_setI_via_Proj)
finally show ‹(a*) h ∈ space_as_set (eigenspace l a)›.
qed
lemma invariant_subspace_Inf:
assumes ‹⋀S. S ∈ M ⟹ invariant_subspace S a›
shows ‹invariant_subspace (⨅M) a›
proof (rule invariant_subspaceI)
have ‹a *⇩S ⨅ M ≤ (⨅S∈M. a *⇩S S)›
using cblinfun_image_INF_leq[where U=a and V=id and X=M] by simp
also have ‹… ≤ (⨅S∈M. S)›
by (rule INF_superset_mono, simp) (use assms in ‹auto simp: invariant_subspace_def›)
also have ‹… = ⨅M›
by simp
finally show ‹a *⇩S ⨅ M ≤ ⨅ M› .
qed
lemma invariant_subspace_INF:
assumes ‹⋀x. x ∈ X ⟹ invariant_subspace (S x) a›
shows ‹invariant_subspace (⨅x∈X. S x) a›
by (smt (verit) assms imageE invariant_subspace_Inf)
lemma invariant_subspace_Sup:
assumes ‹⋀S. S ∈ M ⟹ invariant_subspace S a›
shows ‹invariant_subspace (⨆M) a›
proof -
have *: ‹a ` cspan (⋃S∈M. space_as_set S) ⊆ space_as_set (⨆M)›
proof (rule image_subsetI)
fix h
assume ‹h ∈ cspan (⋃S∈M. space_as_set S)›
then obtain F r where ‹h = (∑g∈F. r g *⇩C g)› and F_in_union: ‹F ⊆ (⋃S∈M. space_as_set S)›
by (auto intro!: simp: complex_vector.span_explicit)
then have ‹a h = (∑g∈F. r g *⇩C a g)›
by (simp add: cblinfun.scaleC_right cblinfun.sum_right)
also have ‹… ∈ space_as_set (⨆M)›
proof (rule complex_vector.subspace_sum)
show ‹csubspace (space_as_set (⨆ M))›
by simp
fix g assume ‹g ∈ F›
then obtain S where ‹S ∈ M› and ‹g ∈ space_as_set S›
using F_in_union by auto
from assms[OF ‹S ∈ M›] ‹g ∈ space_as_set S›
have ‹a g ∈ space_as_set S›
by (simp add: Set.basic_monos(7) cblinfun_apply_in_image' invariant_subspace_def less_eq_ccsubspace.rep_eq)
also from ‹S ∈ M›have ‹… ⊆ space_as_set (⨆ M)›
by (meson Sup_upper less_eq_ccsubspace.rep_eq)
finally show ‹r g *⇩C (a g) ∈ space_as_set (⨆ M)›
by (simp add: complex_vector.subspace_scale)
qed
finally show ‹a h ∈ space_as_set (⨆M)›.
qed
have ‹space_as_set (a *⇩S ⨆M) = closure (a ` closure (cspan (⨆S∈M. space_as_set S)))›
by (metis Sup_ccsubspace.rep_eq cblinfun_image.rep_eq)
also have ‹… = closure (a ` cspan (⨆S∈M. space_as_set S))›
by (rule closure_bounded_linear_image_subset_eq)
(simp add: cblinfun.real.bounded_linear_right)
also from * have ‹… ⊆ closure (space_as_set (⨆M))›
by (meson closure_mono)
also have ‹… = space_as_set (⨆M)›
by force
finally have ‹a *⇩S ⨆M ≤ ⨆M›
by (simp add: less_eq_ccsubspace.rep_eq)
then show ?thesis
using invariant_subspaceI by blast
qed
lemma invariant_subspace_SUP:
assumes ‹⋀x. x ∈ X ⟹ invariant_subspace (S x) a›
shows ‹invariant_subspace (⨆x∈X. S x) a›
by (metis (mono_tags, lifting) assms imageE invariant_subspace_Sup)
lemma reducing_subspace_Inf:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀S. S ∈ M ⟹ reducing_subspace S a›
shows ‹reducing_subspace (⨅M) a›
using assms
by (auto intro!: invariant_subspace_Inf invariant_subspace_SUP
simp add: reducing_subspace_def uminus_Inf invariant_subspace_Inf)
lemma reducing_subspace_INF:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀x. x ∈ X ⟹ reducing_subspace (S x) a›
shows ‹reducing_subspace (⨅x∈X. S x) a›
by (metis (mono_tags, lifting) assms imageE reducing_subspace_Inf)
lemma reducing_subspace_Sup:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀S. S ∈ M ⟹ reducing_subspace S a›
shows ‹reducing_subspace (⨆M) a›
using assms
by (auto intro!: invariant_subspace_Sup invariant_subspace_INF
simp add: reducing_subspace_def uminus_Sup invariant_subspace_Inf)
lemma reducing_subspace_SUP:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀x. x ∈ X ⟹ reducing_subspace (S x) a›
shows ‹reducing_subspace (⨆x∈X. S x) a›
by (metis (mono_tags, lifting) assms imageE reducing_subspace_Sup)
lemma selfadjoint_imp_normal: ‹normal_op a› if ‹selfadjoint a›
using that by (simp add: selfadjoint_def normal_op_def)
lemma eigenspaces_orthogonal:
assumes ‹e ≠ f›
assumes ‹normal_op a›
shows ‹orthogonal_spaces (eigenspace e a) (eigenspace f a)›
proof (intro orthogonal_spaces_def[THEN iffD2] ballI)
fix g h assume g_eigen: ‹g ∈ space_as_set (eigenspace e a)› and h_eigen: ‹h ∈ space_as_set (eigenspace f a)›
with ‹normal_op a› have ‹g ∈ space_as_set (eigenspace (cnj e) (a*))›
by (simp add: normal_op_same_eigenspace_as_adj)
then have a_adj_g: ‹(a*) g = cnj e *⇩C g›
using eigenspace_memberD by blast
from h_eigen have a_h: ‹a h = f *⇩C h›
by (simp add: eigenspace_memberD)
have ‹f * (g ∙⇩C h) = g ∙⇩C a h›
by (simp add: a_h)
also have ‹… = (a*) g ∙⇩C h›
by (simp add: cinner_adj_left)
also have ‹… = e * (g ∙⇩C h)›
using a_adj_g by auto
finally have ‹(f - e) * (g ∙⇩C h) = 0›
by (simp add: vector_space_over_itself.scale_left_diff_distrib)
with ‹e ≠ f› show ‹g ∙⇩C h = 0›
by simp
qed
definition largest_eigenvalue :: ‹('a::complex_normed_vector ⇒⇩C⇩L 'a) ⇒ complex› where
‹largest_eigenvalue a =
(if ∃x. x ∈ eigenvalues a ∧ (∀y ∈ eigenvalues a. cmod x ≥ cmod y) then
SOME x. x ∈ eigenvalues a ∧ (∀y ∈ eigenvalues a. cmod x ≥ cmod y) else 0)›
lemma largest_eigenvalue_0_aux:
‹largest_eigenvalue (0 :: 'a::{not_singleton,complex_normed_vector} ⇒⇩C⇩L 'a) = 0›
proof -
let ?zero = ‹0 :: 'a ⇒⇩C⇩L 'a›
define e where ‹e = (SOME x. x ∈ eigenvalues ?zero ∧ (∀y ∈ eigenvalues ?zero. cmod x ≥ cmod y))›
have ‹∃e. e ∈ eigenvalues ?zero ∧ (∀y∈eigenvalues ?zero. cmod y ≤ cmod e)› (is ‹∃e. ?P e›)
by (auto intro!: exI[of _ 0])
then have ‹?P e›
unfolding e_def
by (rule someI_ex)
then have ‹e = 0›
by simp
then show ‹largest_eigenvalue ?zero = 0›
by (simp add: largest_eigenvalue_def)
qed
lemma largest_eigenvalue_0[simp]:
‹largest_eigenvalue (0 :: 'a::complex_normed_vector ⇒⇩C⇩L 'a) = 0›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
using complex_normed_vector_axioms True
by (rule largest_eigenvalue_0_aux[internalize_sort' 'a])
next
case False
then have ‹eigenvalues (0 :: 'a::complex_normed_vector ⇒⇩C⇩L 'a) = {}›
by (rule not_not_singleton_no_eigenvalues)
then show ?thesis
by (auto simp add: largest_eigenvalue_def)
qed
hide_fact largest_eigenvalue_0_aux
lemma eigenvalues_nonneg:
assumes ‹a ≥ 0› and ‹v ∈ eigenvalues a›
shows ‹v ≥ 0›
proof -
from assms obtain h where ‹norm h = 1› and ahvh: ‹a *⇩V h = v *⇩C h›
using unit_eigenvector_ex by blast
have ‹0 ≤ h ∙⇩C a h›
by (simp add: assms(1) cinner_pos_if_pos)
also have ‹… = v * (h ∙⇩C h)›
by (simp add: ahvh)
also have ‹… = v›
using ‹norm h = 1› cnorm_eq_1 by auto
finally show ‹v ≥ 0›
by blast
qed
unbundle no cblinfun_syntax
end