Theory Spectral_Theorem
section ‹‹Spectral_Theorem› -- The spectral theorem for compact operators›
theory Spectral_Theorem
imports Compact_Operators Positive_Operators Eigenvalues
begin
unbundle cblinfun_syntax
subsection ‹Spectral decomp, compact op›
fun spectral_dec_val :: ‹('a::chilbert_space ⇒⇩C⇩L 'a) ⇒ nat ⇒ complex›
and spectral_dec_space :: ‹('a ⇒⇩C⇩L 'a) ⇒ nat ⇒ 'a ccsubspace›
and spectral_dec_op :: ‹('a ⇒⇩C⇩L 'a) ⇒ nat ⇒ ('a ⇒⇩C⇩L 'a)›
where ‹spectral_dec_val a n = largest_eigenvalue (spectral_dec_op a n)›
| ‹spectral_dec_space a n = (if spectral_dec_val a n = 0 then 0 else eigenspace (spectral_dec_val a n) (spectral_dec_op a n))›
| ‹spectral_dec_op a (Suc n) = spectral_dec_op a n o⇩C⇩L Proj (- spectral_dec_space a n)›
| ‹spectral_dec_op a 0 = a›
definition spectral_dec_proj :: ‹('a::chilbert_space ⇒⇩C⇩L 'a) ⇒ nat ⇒ ('a ⇒⇩C⇩L 'a)› where
‹spectral_dec_proj a n = Proj (spectral_dec_space a n)›
declare spectral_dec_val.simps[simp del]
declare spectral_dec_space.simps[simp del]
lemmas spectral_dec_def = spectral_dec_val.simps
lemmas spectral_dec_space_def = spectral_dec_space.simps
lemma spectral_dec_op_selfadj:
assumes ‹selfadjoint a›
shows ‹selfadjoint (spectral_dec_op a n)›
proof (induction n)
case 0
with assms show ?case
by simp
next
case (Suc n)
define E T where ‹E = spectral_dec_space a n› and ‹T = spectral_dec_op a n›
from Suc have ‹normal_op T›
by (auto intro!: selfadjoint_imp_normal simp: T_def)
then have ‹reducing_subspace E T›
by (auto intro!: eigenspace_is_reducing simp: spectral_dec_space_def E_def T_def)
then have ‹reducing_subspace (- E) T›
by simp
then have *: ‹Proj (- E) o⇩C⇩L T o⇩C⇩L Proj (- E) = T o⇩C⇩L Proj (- E)›
by (simp add: invariant_subspace_iff_PAP reducing_subspace_def)
show ?case
using Suc
apply (simp add: flip: T_def E_def * )
by (simp add: selfadjoint_def adj_Proj cblinfun_compose_assoc)
qed
lemma spectral_dec_op_compact:
assumes ‹compact_op a›
shows ‹compact_op (spectral_dec_op a n)›
apply (induction n)
by (auto intro!: compact_op_comp_left assms)
lemma spectral_dec_val_eigenvalue_of_spectral_dec_op:
fixes a :: ‹'a::{chilbert_space, not_singleton} ⇒⇩C⇩L 'a›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹spectral_dec_val a n ∈ eigenvalues (spectral_dec_op a n)›
by (auto intro!: largest_eigenvalue_ex spectral_dec_op_compact spectral_dec_op_selfadj assms
simp: spectral_dec_def)
lemma spectral_dec_proj_finite_rank:
assumes ‹compact_op a›
shows ‹finite_rank (spectral_dec_proj a n)›
apply (cases ‹spectral_dec_val a n = 0›)
by (auto intro!: finite_rank_Proj_finite_dim compact_op_eigenspace_finite_dim spectral_dec_op_compact assms
simp: spectral_dec_proj_def spectral_dec_space_def)
lemma norm_spectral_dec_op:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹norm (spectral_dec_op a n) = cmod (spectral_dec_val a n)›
by (simp add: spectral_dec_def cmod_largest_eigenvalue spectral_dec_op_compact spectral_dec_op_selfadj assms)
lemma spectral_dec_op_decreasing_eigenspaces:
assumes ‹n ≥ m› and ‹e ≠ 0›
assumes ‹selfadjoint a›
shows ‹eigenspace e (spectral_dec_op a n) ≤ eigenspace e (spectral_dec_op a m)›
proof -
have *: ‹eigenspace e (spectral_dec_op a (Suc n)) ≤ eigenspace e (spectral_dec_op a n)› for n
proof (intro ccsubspace_leI subsetI)
fix h
assume asm: ‹h ∈ space_as_set (eigenspace e (spectral_dec_op a (Suc n)))›
have ‹orthogonal_spaces (eigenspace e (spectral_dec_op a (Suc n))) (kernel (spectral_dec_op a (Suc n)))›
using spectral_dec_op_selfadj[of a ‹Suc n›] ‹e ≠ 0› ‹selfadjoint a›
by (auto intro!: eigenspaces_orthogonal selfadjoint_imp_normal spectral_dec_op_selfadj
simp: spectral_dec_space_def simp flip: eigenspace_0)
then have ‹eigenspace e (spectral_dec_op a (Suc n)) ≤ - kernel (spectral_dec_op a (Suc n))›
using orthogonal_spaces_leq_compl by blast
also have ‹… ≤ - spectral_dec_space a n›
by (auto intro!: ccsubspace_leI kernel_memberI simp: Proj_0_compl)
finally have ‹h ∈ space_as_set (- spectral_dec_space a n)›
using asm by (simp add: Set.basic_monos(7) less_eq_ccsubspace.rep_eq)
then have ‹spectral_dec_op a n h = spectral_dec_op a (Suc n) h›
by (simp add: Proj_fixes_image)
also have ‹… = e *⇩C h›
using asm eigenspace_memberD by blast
finally show ‹h ∈ space_as_set (eigenspace e (spectral_dec_op a n))›
by (simp add: eigenspace_memberI)
qed
define k where ‹k = n - m›
from * have ‹eigenspace e (spectral_dec_op a (m + k)) ≤ eigenspace e (spectral_dec_op a m)›
by (induction k) (auto simp del: spectral_dec_op.simps intro: order.trans)
then show ?thesis
using ‹n ≥ m› by (simp add: k_def)
qed
lemma spectral_dec_val_not_not_singleton:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹¬ class.not_singleton TYPE('a)›
shows ‹spectral_dec_val a n = 0›
proof -
from assms have ‹spectral_dec_op a n = 0›
by (rule not_not_singleton_cblinfun_zero)
then have ‹largest_eigenvalue (spectral_dec_op a n) = 0›
by simp
then show ?thesis
by (simp add: spectral_dec_def)
qed
lemma spectral_dec_val_eigenvalue_aux:
fixes a :: ‹'a::{chilbert_space, not_singleton} ⇒⇩C⇩L 'a›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
assumes eigen_neq0: ‹spectral_dec_val a n ≠ 0›
shows ‹spectral_dec_val a n ∈ eigenvalues a›
proof -
define e where ‹e = spectral_dec_val a n›
with assms have ‹e ≠ 0›
by fastforce
from spectral_dec_op_decreasing_eigenspaces[where m=0 and a=a and n=n, OF _ ‹e ≠ 0› ‹selfadjoint a›]
have 1: ‹eigenspace e (spectral_dec_op a n) ≤ eigenspace e a›
by simp
have 2: ‹spectral_dec_space a n ≠ ⊥›
proof -
have ‹spectral_dec_val a n ∈ eigenvalues (spectral_dec_op a n)›
by (simp add: assms(1) assms(2) spectral_dec_val.simps spectral_dec_op_compact spectral_dec_op_selfadj largest_eigenvalue_ex)
then show ?thesis
using ‹e ≠ 0› by (simp add: eigenvalues_def spectral_dec_space.simps e_def)
qed
from 1 2 have ‹eigenspace e a ≠ ⊥›
by (auto simp: spectral_dec_space_def bot_unique simp flip: e_def simp: ‹e ≠ 0›)
then show ‹e ∈ eigenvalues a›
by (simp add: eigenvalues_def)
qed
lemma spectral_dec_val_eigenvalue:
fixes a :: ‹('a::chilbert_space ⇒⇩C⇩L 'a)›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
assumes eigen_neq0: ‹spectral_dec_val a n ≠ 0›
shows ‹spectral_dec_val a n ∈ eigenvalues a›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
using chilbert_space_axioms True assms
by (rule spectral_dec_val_eigenvalue_aux[internalize_sort' 'a])
next
case False
then have ‹spectral_dec_val a n = 0›
by (rule spectral_dec_val_not_not_singleton)
with assms show ?thesis
by simp
qed
hide_fact spectral_dec_val_eigenvalue_aux
lemma spectral_dec_val_decreasing:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
assumes ‹n ≥ m›
shows ‹cmod (spectral_dec_val a n) ≤ cmod (spectral_dec_val a m)›
proof -
have ‹norm (spectral_dec_op a (Suc n)) ≤ norm (spectral_dec_op a n)› for n
apply simp
by (smt (verit) Proj_partial_isometry cblinfun_compose_zero_right mult_cancel_left2 norm_cblinfun_compose norm_le_zero_iff norm_partial_isometry)
then have *: ‹cmod (spectral_dec_val a (Suc n)) ≤ cmod (spectral_dec_val a n)› for n
by (simp add: cmod_largest_eigenvalue spectral_dec_op_compact assms spectral_dec_op_selfadj spectral_dec_def
del: spectral_dec_op.simps)
define k where ‹k = n - m›
have ‹cmod (spectral_dec_val a (m + k)) ≤ cmod (spectral_dec_val a m)›
apply (induction k arbitrary: m)
apply simp
by (metis "*" add_Suc_right order_trans_rules(23))
with ‹n ≥ m› show ?thesis
by (simp add: k_def)
qed
lemma spectral_dec_val_distinct_aux:
fixes a :: ‹('a::{chilbert_space, not_singleton} ⇒⇩C⇩L 'a)›
assumes ‹n ≠ m›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
assumes neq0: ‹spectral_dec_val a n ≠ 0›
shows ‹spectral_dec_val a n ≠ spectral_dec_val a m›
proof (rule ccontr)
assume ‹¬ spectral_dec_val a n ≠ spectral_dec_val a m›
then have eq: ‹spectral_dec_val a n = spectral_dec_val a m›
by blast
wlog nm: ‹n > m› goal False generalizing n m keeping eq neq0
using hypothesis[of n m] negation assms eq neq0
by auto
define e where ‹e = spectral_dec_val a n›
with neq0 have ‹e ≠ 0›
by simp
have ‹spectral_dec_space a n ≠ ⊥›
proof -
have ‹e ∈ eigenvalues (spectral_dec_op a n)›
by (auto intro!: spectral_dec_val_eigenvalue_of_spectral_dec_op assms simp: e_def)
then show ?thesis
by (simp add: spectral_dec_space_def eigenvalues_def e_def neq0)
qed
then obtain h where ‹norm h = 1› and h_En: ‹h ∈ space_as_set (spectral_dec_space a n)›
using ccsubspace_contains_unit by blast
have T_Sucm_h: ‹spectral_dec_op a (Suc m) h = 0›
proof -
have ‹spectral_dec_space a n = eigenspace e (spectral_dec_op a n)›
by (simp add: spectral_dec_space_def e_def neq0)
also have ‹… ≤ eigenspace e (spectral_dec_op a m)›
using ‹n > m› ‹e ≠ 0› assms
by (auto intro!: spectral_dec_op_decreasing_eigenspaces simp: )
also have ‹… = spectral_dec_space a m›
using neq0 by (simp add: spectral_dec_space_def e_def eq)
finally have ‹h ∈ space_as_set (spectral_dec_space a m)›
using h_En
by (simp add: basic_trans_rules(31) less_eq_ccsubspace.rep_eq)
then show ‹spectral_dec_op a (Suc m) h = 0›
by (simp add: Proj_0_compl)
qed
have ‹spectral_dec_op a (Suc m + k) h = 0› if ‹k ≤ n - m - 1› for k
proof (insert that, induction k)
case 0
from T_Sucm_h show ?case
by simp
next
case (Suc k)
define mk1 where ‹mk1 = Suc (m + k)›
from Suc.prems have ‹mk1 ≤ n›
using mk1_def by linarith
have ‹eigenspace e (spectral_dec_op a n) ≤ eigenspace e (spectral_dec_op a mk1)›
using ‹mk1 ≤ n› ‹e ≠ 0› ‹selfadjoint a›
by (rule spectral_dec_op_decreasing_eigenspaces)
with h_En have h_mk1: ‹h ∈ space_as_set (eigenspace e (spectral_dec_op a mk1))›
by (auto simp: e_def spectral_dec_space_def less_eq_ccsubspace.rep_eq neq0)
have ‹Proj (- spectral_dec_space a mk1) *⇩V h = 0 ∨ Proj (- spectral_dec_space a mk1) *⇩V h = h›
proof (cases ‹e = spectral_dec_val a mk1›)
case True
from h_mk1 have ‹Proj (- spectral_dec_space a mk1) h = 0›
using ‹e ≠ 0› by (simp add: Proj_0_compl True spectral_dec_space_def)
then show ?thesis
by simp
next
case False
have ‹orthogonal_spaces (eigenspace e (spectral_dec_op a mk1)) (spectral_dec_space a mk1)›
by (simp add: False assms eigenspaces_orthogonal spectral_dec_space.simps spectral_dec_op_selfadj selfadjoint_imp_normal)
with h_mk1 have ‹h ∈ space_as_set (- spectral_dec_space a mk1)›
using less_eq_ccsubspace.rep_eq orthogonal_spaces_leq_compl by blast
then have ‹Proj (- spectral_dec_space a mk1) h = h›
by (rule Proj_fixes_image)
then show ?thesis
by simp
qed
with Suc show ?case
by (auto simp: mk1_def)
qed
from this[where k=‹n - m - 1›]
have ‹spectral_dec_op a n h = 0›
using ‹n > m›
by (simp del: spectral_dec_op.simps)
moreover from h_En have ‹spectral_dec_op a n h = e *⇩C h›
by (simp add: neq0 e_def eigenspace_memberD spectral_dec_space_def)
ultimately show False
using ‹norm h = 1› ‹e ≠ 0›
by force
qed
lemma spectral_dec_val_distinct:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹n ≠ m›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
assumes neq0: ‹spectral_dec_val a n ≠ 0›
shows ‹spectral_dec_val a n ≠ spectral_dec_val a m›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
using chilbert_space_axioms True assms
by (rule spectral_dec_val_distinct_aux[internalize_sort' 'a])
next
case False
then have ‹spectral_dec_val a n = 0›
by (rule spectral_dec_val_not_not_singleton)
with assms show ?thesis
by simp
qed
hide_fact spectral_dec_val_distinct_aux
lemma spectral_dec_val_tendsto_0:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹spectral_dec_val a ⇢ 0›
proof (cases ‹∃n. spectral_dec_val a n = 0›)
case True
then obtain n where ‹spectral_dec_val a n = 0›
by auto
then have ‹spectral_dec_val a m = 0› if ‹m ≥ n› for m
using spectral_dec_val_decreasing[OF assms that]
by simp
then show ‹spectral_dec_val a ⇢ 0›
by (auto intro!: tendsto_eventually eventually_sequentiallyI)
next
case False
define E where ‹E = spectral_dec_val a›
from False have ‹E n ∈ eigenvalues a› for n
by (simp add: spectral_dec_val_eigenvalue assms E_def)
then have ‹eigenspace (E n) a ≠ 0› for n
by (simp add: eigenvalues_def)
then obtain e where e_E: ‹e n ∈ space_as_set (eigenspace (E n) a)›
and norm_e: ‹norm (e n) = 1› for n
apply atomize_elim
using ccsubspace_contains_unit
by (auto intro!: choice2)
then obtain h n where ‹strict_mono n› and aen_lim: ‹(λj. a (e (n j))) ⇢ h›
proof atomize_elim
from ‹compact_op a›
have compact:‹compact (closure (a ` cball 0 1))›
by (simp add: compact_op_def2)
from norm_e have ‹a (e n) ∈ closure (a ` cball 0 1)› for n
using closure_subset[of ‹a ` cball 0 1›] by auto
with compact[unfolded compact_def, rule_format, of ‹λn. a (e n)›]
show ‹∃n h. strict_mono n ∧ (λj. a (e (n j))) ⇢ h›
by (auto simp: o_def)
qed
have ortho_en: ‹is_orthogonal (e (n j)) (e (n k))› if ‹j ≠ k› for j k
proof -
have ‹n j ≠ n k›
by (simp add: ‹strict_mono n› strict_mono_eq that)
then have ‹E (n j) ≠ E (n k)›
unfolding E_def
apply (rule spectral_dec_val_distinct)
using False assms by auto
then have ‹orthogonal_spaces (eigenspace (E (n j)) a) (eigenspace (E (n k)) a)›
apply (rule eigenspaces_orthogonal)
by (simp add: assms(2) selfadjoint_imp_normal)
with e_E show ?thesis
using orthogonal_spaces_def by blast
qed
have aEe: ‹a (e n) = E n *⇩C e n› for n
by (simp add: e_E eigenspace_memberD)
obtain α where E_lim: ‹(λn. norm (E n)) ⇢ α›
by (rule decseq_convergent[where X=‹λn. cmod (E n)› and B=0])
(use spectral_dec_val_decreasing[OF assms] in ‹auto intro!: simp: decseq_def E_def›)
then have ‹α ≥ 0›
apply (rule LIMSEQ_le_const)
by simp
have aen_diff: ‹norm (a (e (n j)) - a (e (n k))) ≥ α * sqrt 2› if ‹j ≠ k› for j k
proof -
from E_lim and spectral_dec_val_decreasing[OF assms, folded E_def]
have E_geq_α: ‹cmod (E n) ≥ α› for n
apply (rule_tac decseq_ge[unfolded decseq_def, rotated])
by auto
have ‹(norm (a (e (n j)) - a (e (n k))))⇧2 = (cmod (E (n j)))⇧2 + (cmod (E (n k)))⇧2›
by (simp add: polar_identity_minus aEe that ortho_en norm_e)
also have ‹… ≥ α⇧2 + α⇧2› (is ‹_ ≥ …›)
apply (rule add_mono)
using E_geq_α ‹α ≥ 0› by auto
also have ‹… = (α * sqrt 2)⇧2›
by (simp add: algebra_simps)
finally show ?thesis
apply (rule power2_le_imp_le)
by simp
qed
have ‹α = 0›
proof -
have ‹α * sqrt 2 < ε› if ‹ε > 0› for ε
proof -
from ‹strict_mono n› have cauchy: ‹Cauchy (λk. a (e (n k)))›
using LIMSEQ_imp_Cauchy aen_lim by blast
obtain k where k: ‹∀m≥k. ∀na≥k. dist (a *⇩V e (n m)) (a *⇩V e (n na)) < ε›
apply atomize_elim
using cauchy[unfolded Cauchy_def, rule_format, OF ‹ε > 0›]
by simp
define j where ‹j = Suc k›
then have ‹j ≠ k›
by simp
from k have ‹dist (a (e (n j))) (a (e (n k))) < ε›
by (simp add: j_def)
with aen_diff[OF ‹j ≠ k›] show ‹α * sqrt 2 < ε›
by (simp add: Cauchy_def dist_norm)
qed
with ‹α ≥ 0› show ‹α = 0›
using less_eq_real_def by fastforce
qed
with E_lim show ?thesis
by (auto intro!: tendsto_norm_zero_cancel simp: E_def)
qed
lemma spectral_dec_op_tendsto:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹spectral_dec_op a ⇢ 0›
apply (rule tendsto_norm_zero_cancel)
using spectral_dec_val_tendsto_0[OF assms]
by (simp add: assms norm_spectral_dec_op tendsto_norm_zero)
lemma spectral_dec_op_spectral_dec_proj:
‹spectral_dec_op a n = a - (∑i<n. spectral_dec_val a i *⇩C spectral_dec_proj a i)›
proof (induction n)
case 0
show ?case
by simp
next
case (Suc n)
have ‹spectral_dec_op a (Suc n) = spectral_dec_op a n o⇩C⇩L Proj (- spectral_dec_space a n)›
by simp
also have ‹… = spectral_dec_op a n - spectral_dec_val a n *⇩C spectral_dec_proj a n› (is ‹?lhs = ?rhs›)
proof -
have ‹?lhs h = ?rhs h› if ‹h ∈ space_as_set (spectral_dec_space a n)› for h
proof -
have ‹?lhs h = 0›
by (simp add: Proj_0_compl that)
have ‹spectral_dec_op a n *⇩V h = spectral_dec_val a n *⇩C h›
by (smt (verit, best) Proj_fixes_image ‹(spectral_dec_op a n o⇩C⇩L Proj (- spectral_dec_space a n)) *⇩V h = 0› cblinfun_apply_cblinfun_compose complex_vector.scale_eq_0_iff eigenspace_memberD spectral_dec_space.elims kernel_Proj kernel_cblinfun_compose kernel_memberD kernel_memberI ortho_involution that)
also have ‹… = spectral_dec_val a n *⇩C (spectral_dec_proj a n *⇩V h)›
by (simp add: Proj_fixes_image spectral_dec_proj_def that)
finally
have ‹?rhs h = 0›
by (simp add: cblinfun.diff_left)
with ‹?lhs h = 0› show ?thesis
by simp
qed
moreover have ‹?lhs h = ?rhs h› if ‹h ∈ space_as_set (- spectral_dec_space a n)› for h
by (simp add: Proj_0_compl Proj_fixes_image cblinfun.diff_left spectral_dec_proj_def that)
ultimately have ‹?lhs h = ?rhs h›
if ‹h ∈ space_as_set (spectral_dec_space a n ⊔ - spectral_dec_space a n) › for h
using that by (rule eq_on_ccsubspaces_sup)
then show ‹?lhs = ?rhs›
by (auto intro!: cblinfun_eqI simp add: )
qed
also have ‹… = a - (∑i<Suc n. spectral_dec_val a i *⇩C spectral_dec_proj a i)›
by (simp add: Suc.IH)
finally show ?case
by -
qed
lemma sequential_tendsto_reorder:
assumes ‹inj g›
assumes ‹f ⇢ l›
shows ‹(f o g) ⇢ l›
proof (intro lim_explicit[THEN iffD2] impI allI)
fix S assume ‹open S› and ‹l ∈ S›
with ‹f ⇢ l›
obtain M where M: ‹f m ∈ S› if ‹m ≥ M› for m
using tendsto_obtains_N by blast
define N where ‹N = Max (g -` {..<M}) + 1›
have N: ‹g n ≥ M› if ‹n ≥ N› for n
proof -
from ‹inj g› have ‹finite (g -` {..<M})›
using finite_vimageI by blast
then have ‹N > n› if ‹n ∈ g -` {..<M}› for n
using N_def that
by (simp add: less_Suc_eq_le)
then have ‹N > n› if ‹g n < M› for n
by (simp add: that)
with that show ‹g n ≥ M›
using linorder_not_less by blast
qed
from N M show ‹∃N. ∀n≥N. (f ∘ g) n ∈ S›
by auto
qed
lemma spectral_dec_sums:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹(λn. spectral_dec_val a n *⇩C spectral_dec_proj a n) sums a›
proof -
from spectral_dec_op_tendsto[OF assms]
have ‹(λn. a - spectral_dec_op a n) ⇢ a›
by (simp add: tendsto_diff_const_left_rewrite)
moreover from spectral_dec_op_spectral_dec_proj[of a]
have ‹a - spectral_dec_op a n = (∑i<n. spectral_dec_val a i *⇩C spectral_dec_proj a i)› for n
by simp
ultimately show ?thesis
by (simp add: sums_def)
qed
lemma spectral_dec_val_real:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹spectral_dec_val a n ∈ ℝ›
by (metis Reals_0 assms(1) assms(2) eigenvalue_selfadj_real spectral_dec_val_eigenvalue)
lemma spectral_dec_space_orthogonal:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
assumes ‹n ≠ m›
shows ‹orthogonal_spaces (spectral_dec_space a n) (spectral_dec_space a m)›
proof (cases ‹spectral_dec_val a n = 0 ∨ spectral_dec_val a m = 0›)
case True
then show ?thesis
by (auto intro!: simp: spectral_dec_space_def)
next
case False
have ‹spectral_dec_space a n ≤ eigenspace (spectral_dec_val a n) a›
using ‹selfadjoint a›
by (metis False spectral_dec_space.elims spectral_dec_op.simps(2) spectral_dec_op_decreasing_eigenspaces zero_le)
moreover have ‹spectral_dec_space a m ≤ eigenspace (spectral_dec_val a m) a›
using ‹selfadjoint a›
by (metis False spectral_dec_space.elims spectral_dec_op.simps(2) spectral_dec_op_decreasing_eigenspaces zero_le)
moreover have ‹orthogonal_spaces (eigenspace (spectral_dec_val a n) a) (eigenspace (spectral_dec_val a m) a)›
apply (intro eigenspaces_orthogonal selfadjoint_imp_normal assms
spectral_dec_val_distinct)
using False by simp
ultimately show ?thesis
by (meson order.trans orthocomplemented_lattice_class.compl_mono orthogonal_spaces_leq_compl)
qed
lemma spectral_dec_proj_pos: ‹spectral_dec_proj a n ≥ 0›
by (auto intro!: simp: spectral_dec_proj_def)
lemma
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows spectral_dec_tendsto_pos_op: ‹(λn. max 0 (spectral_dec_val a n) *⇩C spectral_dec_proj a n) sums pos_op a› (is ?thesis1)
and spectral_dec_tendsto_neg_op: ‹(λn. - min (spectral_dec_val a n) 0 *⇩C spectral_dec_proj a n) sums neg_op a› (is ?thesis2)
proof -
define I J where ‹I = {n. spectral_dec_val a n ≥ 0}›
and ‹J = {n. spectral_dec_val a n ≤ 0}›
define R S where ‹R = (⨆n∈I. spectral_dec_space a n)›
and ‹S = (⨆n∈J. spectral_dec_space a n)›
define aR aS where ‹aR = a o⇩C⇩L Proj R› and ‹aS = - a o⇩C⇩L Proj S›
have spectral_dec_cases: ‹(0 < spectral_dec_val a n ⟹ P) ⟹
(spectral_dec_val a n < 0 ⟹ P) ⟹
(spectral_dec_val a n = 0 ⟹ P) ⟹ P› for n P
apply atomize_elim
using reals_zero_comparable[OF spectral_dec_val_real[OF assms, of n]]
by auto
have PRP: ‹spectral_dec_proj a n o⇩C⇩L Proj R = spectral_dec_proj a n› if ‹n ∈ I› for n
by (auto intro!: Proj_o_Proj_subspace_left
simp add: R_def SUP_upper that spectral_dec_proj_def)
have PR0: ‹spectral_dec_proj a n o⇩C⇩L Proj R = 0› if ‹n ∉ I› for n
apply (cases rule: spectral_dec_cases[of n])
using that
by (auto intro!: orthogonal_spaces_SUP_right spectral_dec_space_orthogonal assms
simp: spectral_dec_proj_def R_def I_def
simp flip: orthogonal_projectors_orthogonal_spaces)
have PSP: ‹spectral_dec_proj a n o⇩C⇩L Proj S = spectral_dec_proj a n› if ‹n ∈ J› for n
by (auto intro!: Proj_o_Proj_subspace_left
simp add: S_def SUP_upper that spectral_dec_proj_def)
have PS0: ‹spectral_dec_proj a n o⇩C⇩L Proj S = 0› if ‹n ∉ J› for n
apply (cases rule: spectral_dec_cases[of n])
using that
by (auto intro!: orthogonal_spaces_SUP_right spectral_dec_space_orthogonal assms
simp: spectral_dec_proj_def S_def J_def
simp flip: orthogonal_projectors_orthogonal_spaces)
from spectral_dec_sums[OF assms]
have ‹(λn. (spectral_dec_val a n *⇩C spectral_dec_proj a n) o⇩C⇩L Proj R) sums aR›
unfolding aR_def
apply (rule bounded_linear.sums[rotated])
by (intro bounded_clinear.bounded_linear bounded_clinear_cblinfun_compose_left)
then have sum_aR: ‹(λn. max 0 (spectral_dec_val a n) *⇩C spectral_dec_proj a n) sums aR›
apply (rule sums_cong[THEN iffD1, rotated])
by (simp add: I_def PR0 PRP max_def)
from sum_aR have ‹aR ≥ 0›
apply (rule sums_pos_cblinfun)
by (auto intro!: spectral_dec_proj_pos scaleC_nonneg_nonneg simp: max_def)
from spectral_dec_sums[OF assms]
have ‹(λn. spectral_dec_val a n *⇩C spectral_dec_proj a n o⇩C⇩L Proj S) sums - aS›
unfolding aS_def minus_minus cblinfun_compose_uminus_left
apply (rule bounded_linear.sums[rotated])
by (intro bounded_clinear.bounded_linear bounded_clinear_cblinfun_compose_left)
then have sum_aS': ‹(λn. min (spectral_dec_val a n) 0 *⇩C spectral_dec_proj a n) sums - aS›
apply (rule sums_cong[THEN iffD1, rotated])
by (simp add: J_def PS0 PSP min_def)
then have sum_aS: ‹(λn. - min (spectral_dec_val a n) 0 *⇩C spectral_dec_proj a n) sums aS›
using sums_minus by fastforce
from sum_aS have ‹aS ≥ 0›
by (rule sums_pos_cblinfun)
(auto intro!: spectral_dec_proj_pos scaleC_nonpos_nonneg simp: max_def min_def)
from sum_aR sum_aS'
have ‹(λn. max 0 (spectral_dec_val a n) *⇩C spectral_dec_proj a n
+ min (spectral_dec_val a n) 0 *⇩C spectral_dec_proj a n) sums (aR - aS)›
using sums_add by fastforce
then have ‹(λn. spectral_dec_val a n *⇩C spectral_dec_proj a n) sums (aR - aS)›
proof (rule sums_cong[THEN iffD1, rotated])
fix n
have ‹max 0 (spectral_dec_val a n) + min (spectral_dec_val a n) 0
= spectral_dec_val a n›
apply (cases rule: spectral_dec_cases[of n])
by (auto intro!: simp: max_def min_def)
then
show ‹max 0 (spectral_dec_val a n) *⇩C spectral_dec_proj a n +
min (spectral_dec_val a n) 0 *⇩C spectral_dec_proj a n =
spectral_dec_val a n *⇩C spectral_dec_proj a n›
by (metis scaleC_left.add)
qed
with spectral_dec_sums[OF assms]
have ‹aR - aS = a›
using sums_unique2 by blast
have ‹aR o⇩C⇩L aS = 0›
by (metis (no_types, opaque_lifting) Proj_idempotent ‹0 ≤ aR› ‹aR - aS = a› aR_def add_cancel_left_left add_minus_cancel adj_0 adj_Proj adj_cblinfun_compose assms(2) cblinfun_compose_minus_right comparable_selfadjoint lift_cblinfun_comp(2) selfadjoint_def uminus_add_conv_diff)
have ‹aR = pos_op a› and ‹aS = neg_op a›
by (intro pos_op_neg_op_unique[where b=aR and c=aS]
‹aR - aS = a› ‹0 ≤ aR› ‹0 ≤ aS› ‹aR o⇩C⇩L aS = 0›)+
with sum_aR and sum_aS
show ?thesis1 and ?thesis2
by auto
qed
lemma spectral_dec_tendsto_abs_op:
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹(λn. cmod (spectral_dec_val a n) *⇩R spectral_dec_proj a n) sums abs_op a›
proof -
from spectral_dec_tendsto_pos_op[OF assms] spectral_dec_tendsto_neg_op[OF assms]
have ‹(λn. max 0 (spectral_dec_val a n) *⇩C spectral_dec_proj a n
+ - min (spectral_dec_val a n) 0 *⇩C spectral_dec_proj a n) sums (pos_op a + neg_op a)›
using sums_add by blast
then have ‹(λn. cmod (spectral_dec_val a n) *⇩R spectral_dec_proj a n) sums (pos_op a + neg_op a)›
apply (rule sums_cong[THEN iffD1, rotated])
using spectral_dec_val_real[OF assms]
apply (simp add: complex_is_Real_iff cmod_def max_def min_def less_eq_complex_def scaleR_scaleC
flip: scaleC_add_right)
by (metis complex_surj zero_complex.code)
then show ?thesis
by (simp add: pos_op_plus_neg_op)
qed
definition spectral_dec_vecs :: ‹('a ⇒⇩C⇩L 'a) ⇒ 'a::chilbert_space set› where
‹spectral_dec_vecs a = (⋃n. scaleC (csqrt (spectral_dec_val a n)) ` some_onb_of (spectral_dec_space a n))›
lemma spectral_dec_vecs_ortho:
assumes ‹selfadjoint a› and ‹compact_op a›
shows ‹is_ortho_set (spectral_dec_vecs a)›
proof (unfold is_ortho_set_def, intro conjI ballI impI)
show ‹0 ∉ spectral_dec_vecs a›
proof (rule notI)
assume ‹0 ∈ spectral_dec_vecs a›
then obtain n v where v0: ‹0 = csqrt (spectral_dec_val a n) *⇩C v› and v_in: ‹v ∈ some_onb_of (spectral_dec_space a n)›
by (auto simp: spectral_dec_vecs_def)
from v_in have ‹v ≠ 0›
using some_onb_of_norm1 by fastforce
from v_in have ‹spectral_dec_space a n ≠ 0›
using some_onb_of_0 by force
then have ‹spectral_dec_val a n ≠ 0›
by (meson spectral_dec_space.elims)
with v0 ‹v ≠ 0› show False
by force
qed
fix g h assume g: ‹g ∈ spectral_dec_vecs a› and h: ‹h ∈ spectral_dec_vecs a› and ‹g ≠ h›
from g obtain ng g' where gg': ‹g = csqrt (spectral_dec_val a ng) *⇩C g'› and g'_in: ‹g' ∈ some_onb_of (spectral_dec_space a ng)›
by (auto simp: spectral_dec_vecs_def)
from h obtain nh h' where hh': ‹h = csqrt (spectral_dec_val a nh) *⇩C h'› and h'_in: ‹h' ∈ some_onb_of (spectral_dec_space a nh)›
by (auto simp: spectral_dec_vecs_def)
have ‹is_orthogonal g' h'›
proof (cases ‹ng = nh›)
case True
with h'_in have ‹h' ∈ some_onb_of (spectral_dec_space a nh)›
by simp
with g'_in True ‹g ≠ h› gg' hh'
show ?thesis
using is_ortho_set_def by fastforce
next
case False
then have ‹orthogonal_spaces (spectral_dec_space a ng) (spectral_dec_space a nh)›
by (auto intro!: spectral_dec_space_orthogonal assms simp: )
with h'_in g'_in show ‹is_orthogonal g' h'›
using orthogonal_spaces_ccspan by force
qed
then show ‹is_orthogonal g h›
by (simp add: gg' hh')
qed
lemma spectral_dec_val_nonneg:
assumes ‹a ≥ 0›
assumes ‹compact_op a›
shows ‹spectral_dec_val a n ≥ 0›
proof -
define v where ‹v = spectral_dec_val a n›
wlog non0: ‹spectral_dec_val a n ≠ 0› generalizing v keeping v_def
using negation by force
have [simp]: ‹selfadjoint a›
using adj_0 assms(1) comparable_selfadjoint selfadjoint_def by blast
have ‹v ∈ eigenvalues a›
by (auto intro!: non0 spectral_dec_val_eigenvalue assms simp: v_def)
then show ‹spectral_dec_val a n ≥ 0›
using assms(1) eigenvalues_nonneg v_def by blast
qed
lemma spectral_dec_space_finite_dim[intro]:
assumes ‹compact_op a›
shows ‹finite_dim_ccsubspace (spectral_dec_space a n)›
by (auto intro!: compact_op_eigenspace_finite_dim spectral_dec_op_compact assms simp: spectral_dec_space_def)
lemma spectral_dec_space_0:
assumes ‹spectral_dec_val a n = 0›
shows ‹spectral_dec_space a n = 0›
by (simp add: assms spectral_dec_space_def)
unbundle no cblinfun_syntax
end