Theory Compact_Operators
section ‹‹Compact_Operators› -- Finite rank and compact operators›
theory Compact_Operators
imports
Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
Wlog.Wlog
"HOL-Analysis.Abstract_Metric_Spaces"
HS2Ell2
Strong_Operator_Topology
Misc_Tensor_Product_TTS
Eigenvalues
begin
unbundle cblinfun_syntax
subsection ‹Finite rank operators›
definition finite_rank where ‹finite_rank A ⟷ A ∈ cspan (Collect rank1)›
lemma finite_rank_0[simp]: ‹finite_rank 0›
by (simp add: complex_vector.span_zero finite_rank_def)
lemma finite_rank_scaleC[simp]: ‹finite_rank (c *⇩C a)› if ‹finite_rank a›
using complex_vector.span_scale finite_rank_def that by blast
lemma finite_rank_scaleR[simp]: ‹finite_rank (c *⇩R a)› if ‹finite_rank a›
by (simp add: scaleR_scaleC that)
lemma finite_rank_uminus[simp]: ‹finite_rank (-a) = finite_rank a›
by (metis add.inverse_inverse complex_vector.span_neg finite_rank_def)
lemma finite_rank_plus[simp]: ‹finite_rank (a + b)› if ‹finite_rank a› and ‹finite_rank b›
using that by (auto simp: finite_rank_def complex_vector.span_add_eq2)
lemma finite_rank_minus[simp]: ‹finite_rank (a - b)› if ‹finite_rank a› and ‹finite_rank b›
using complex_vector.span_diff finite_rank_def that(1) that(2) by blast
lemma finite_rank_butterfly[simp]: ‹finite_rank (butterfly x y)›
by (cases ‹x ≠ 0 ∧ y ≠ 0›)
(auto intro: complex_vector.span_base complex_vector.span_zero simp add: finite_rank_def)
lemma finite_rank_sum_butterfly:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes ‹finite_rank a›
shows ‹∃x y (n::nat). a = (∑i<n. butterfly (x i) (y i))›
proof -
from assms
have ‹a ∈ cspan (Collect rank1)›
by (simp add: finite_rank_def)
then obtain r t where ‹finite t› and t_rank1: ‹t ⊆ Collect rank1›
and a_sum: ‹a = (∑a∈t. r a *⇩C a)›
by (smt (verit, best) complex_vector.span_alt mem_Collect_eq)
from ‹finite t› obtain ι and n::nat where ι: ‹bij_betw ι {..<n} t›
using bij_betw_from_nat_into_finite by blast
define c where ‹c i = r (ι i) *⇩C ι i› for i
from ι t_rank1
have c_rank1: ‹rank1 (c i) ∨ c i = 0› if ‹i < n› for i
by (auto intro!: rank1_scaleC simp: c_def bij_betw_apply subset_iff that)
have ac_sum: ‹a = (∑i<n. c i)›
by (smt (verit, best) a_sum ι c_def sum.cong sum.reindex_bij_betw)
from c_rank1
obtain x y where ‹c i = butterfly (x i) (y i)› if ‹i < n› for i
apply atomize_elim
apply (rule SMT_choices)
using rank1_iff_butterfly by fastforce
with ac_sum show ?thesis
by auto
qed
lemma finite_rank_sum: ‹finite_rank (∑x∈F. f x)› if ‹⋀x. x∈F ⟹ finite_rank (f x)›
using that by (induction F rule:infinite_finite_induct) (auto intro!: finite_rank_plus)
lemma rank1_finite_rank: ‹finite_rank a› if ‹rank1 a›
by (simp add: complex_vector.span_base finite_rank_def that)
lemma finite_rank_compose_left:
assumes ‹finite_rank B›
shows ‹finite_rank (A o⇩C⇩L B)›
proof -
from assms have ‹B ∈ cspan (Collect rank1)›
by (simp add: finite_rank_def)
then obtain F t where ‹finite F› and F_rank1: ‹F ⊆ Collect rank1› and ‹B = (∑x∈F. t x *⇩C x)›
by (smt (verit, best) complex_vector.span_explicit mem_Collect_eq)
then have ‹A o⇩C⇩L B = (∑x∈F. t x *⇩C (A o⇩C⇩L x))›
by (metis (mono_tags, lifting) cblinfun_compose_scaleC_right cblinfun_compose_sum_right sum.cong)
also have ‹… ∈ cspan (Collect finite_rank)›
by (intro complex_vector.span_sum complex_vector.span_scale)
(use F_rank1 in ‹auto intro!: complex_vector.span_base rank1_finite_rank rank1_compose_left›)
also have ‹… = Collect finite_rank›
by (metis (no_types, lifting) complex_vector.span_superset cspan_eqI finite_rank_def mem_Collect_eq subset_antisym subset_iff)
finally show ?thesis
by simp
qed
lemma finite_rank_compose_right:
assumes ‹finite_rank A›
shows ‹finite_rank (A o⇩C⇩L B)›
proof -
from assms have ‹A ∈ cspan (Collect rank1)›
by (simp add: finite_rank_def)
then obtain F t where ‹finite F› and F_rank1: ‹F ⊆ Collect rank1› and ‹A = (∑x∈F. t x *⇩C x)›
by (smt (verit, best) complex_vector.span_explicit mem_Collect_eq)
then have ‹A o⇩C⇩L B = (∑x∈F. t x *⇩C (x o⇩C⇩L B))›
by (metis (mono_tags, lifting) cblinfun_compose_scaleC_left cblinfun_compose_sum_left sum.cong)
also have ‹… ∈ cspan (Collect finite_rank)›
by (intro complex_vector.span_sum complex_vector.span_scale)
(use F_rank1 in ‹auto intro!: complex_vector.span_base rank1_finite_rank rank1_compose_right›)
also have ‹… = Collect finite_rank›
by (metis (no_types, lifting) complex_vector.span_superset cspan_eqI finite_rank_def mem_Collect_eq subset_antisym subset_iff)
finally show ?thesis
by simp
qed
lemma rank1_Proj_singleton[iff]: ‹rank1 (Proj (ccspan {x}))›
using Proj_range rank1_def by blast
lemma finite_rank_Proj_singleton[iff]: ‹finite_rank (Proj (ccspan {x}))›
by (simp add: rank1_finite_rank)
lemma finite_rank_Proj_finite_dim:
fixes S :: ‹'a::chilbert_space ccsubspace›
assumes ‹finite_dim_ccsubspace S›
shows ‹finite_rank (Proj S)›
proof -
from assms
obtain B where ‹is_ortho_set B› and ‹finite B› and spanB: ‹cspan B = space_as_set S›
unfolding finite_dim_ccsubspace.rep_eq
using cfinite_dim_subspace_has_onb by force
have ‹Proj S = Proj (ccspan B)›
by (metis Proj.rep_eq ‹finite B› cblinfun_apply_inject ccspan_finite spanB)
moreover have ‹finite_rank (Proj (ccspan B))›
using ‹finite B› ‹is_ortho_set B›
proof induction
case empty
then show ?case
by simp
next
case (insert x F)
then have ‹is_ortho_set F›
by (meson is_ortho_set_antimono subset_insertI)
have ‹Proj (ccspan (insert x F)) = proj x + Proj (ccspan F)›
by (subst Proj_orthog_ccspan_insert)
(use insert in ‹auto simp: is_onb_def is_ortho_set_def›)
moreover have ‹finite_rank …›
by (rule finite_rank_plus)
(auto intro!: ‹is_ortho_set F› insert)
ultimately show ?case
by simp
qed
ultimately show ?thesis
by simp
qed
lemma finite_rank_Proj_finite:
fixes F :: ‹'a::chilbert_space set›
assumes ‹finite F›
shows ‹finite_rank (Proj (ccspan F))›
proof -
obtain B where ‹is_ortho_set B› and ‹finite B› and ‹cspan B = cspan F›
by (meson assms orthonormal_basis_of_cspan)
have ‹Proj (ccspan F) = Proj (ccspan B)›
by (simp add: ‹cspan B = cspan F› ccspan.abs_eq)
moreover have ‹finite_rank (Proj (ccspan B))›
using ‹finite B› ‹is_ortho_set B›
proof induction
case empty
then show ?case
by simp
next
case (insert x F)
then have ‹is_ortho_set F›
by (meson is_ortho_set_antimono subset_insertI)
have ‹Proj (ccspan (insert x F)) = proj x + Proj (ccspan F)›
by (subst Proj_orthog_ccspan_insert)
(use insert in ‹auto simp: is_onb_def is_ortho_set_def›)
moreover have ‹finite_rank …›
by (rule finite_rank_plus) (auto intro!: ‹is_ortho_set F› insert)
ultimately show ?case
by simp
qed
ultimately show ?thesis
by simp
qed
lemma finite_rank_cfinite_dim[simp]: ‹finite_rank (a :: 'a :: {cfinite_dim,chilbert_space} ⇒⇩C⇩L 'b :: complex_normed_vector)›
proof -
obtain B :: ‹'a set› where ‹is_onb B›
using is_onb_some_chilbert_basis by blast
from ‹is_onb B› have [simp]: ‹finite B›
by (auto intro!: cindependent_cfinite_dim_finite is_ortho_set_cindependent simp add: is_onb_def)
have [simp]: ‹cspan B = UNIV›
proof -
from ‹is_onb B› have ‹ccspan B = ⊤›
using is_onb_def by blast
then have ‹closure (cspan B) = UNIV›
by (metis ccspan.rep_eq space_as_set_top)
then show ?thesis
by simp
qed
have a_sum: ‹a = (∑b∈B. a o⇩C⇩L selfbutter b)›
proof (rule cblinfun_eq_on_UNIV_span[OF ‹cspan B = UNIV›])
fix s assume [simp]: ‹s ∈ B›
with ‹is_onb B› have ‹norm s = 1›
by (simp add: is_onb_def)
have 1: ‹j ≠ s ⟹ j ∈ B ⟹ (a o⇩C⇩L selfbutter j) *⇩V s = 0› for j
using ‹is_onb B› ‹s ∈ B› cblinfun.scaleC_right is_onb_def is_ortho_set_def scaleC_eq_0_iff
by fastforce
have 2: ‹a *⇩V s = (if s ∈ B then (a o⇩C⇩L selfbutter s) *⇩V s else 0)›
using ‹norm s = 1› ‹s ∈ B› by (simp add: cnorm_eq_1)
show ‹a *⇩V s = (∑b∈B. a o⇩C⇩L selfbutter b) *⇩V s›
by (subst cblinfun.sum_left, subst sum_single[where i=s]) (use 1 2 in auto)
qed
have ‹finite_rank (∑b∈B. a o⇩C⇩L selfbutter b)›
by (auto intro!: finite_rank_sum simp: cblinfun_comp_butterfly)
with a_sum show ?thesis
by simp
qed
lemma finite_rank_cspan_butterflies:
‹finite_rank a ⟷ a ∈ cspan (range (case_prod butterfly))›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
have ‹(Collect finite_rank :: ('a ⇒⇩C⇩L 'b) set) = cspan (Collect rank1)›
using finite_rank_def by fastforce
also have ‹… = cspan (insert 0 (Collect rank1))›
by force
also have ‹… = cspan (range (case_prod butterfly))›
by (rule arg_cong[where f=cspan])
(use butterfly_0_left in ‹force simp: image_iff rank1_iff_butterfly simp del: butterfly_0_left›)+
finally show ?thesis
by auto
qed
lemma finite_rank_comp_left: ‹finite_rank (a o⇩C⇩L b)› if ‹finite_rank a›
for a b :: ‹_::chilbert_space ⇒⇩C⇩L _::chilbert_space›
proof -
from that
have ‹a ∈ cspan (range (case_prod butterfly))›
by (simp add: finite_rank_cspan_butterflies)
then have ‹a o⇩C⇩L b ∈ (λa. a o⇩C⇩L b) ` cspan (range (case_prod butterfly))›
by fast
also have ‹… = cspan ((λa. a o⇩C⇩L b) ` range (case_prod butterfly))›
by (simp add: clinear_cblinfun_compose_left complex_vector.linear_span_image)
also have ‹… ⊆ cspan (range (case_prod butterfly))›
by (force intro!: complex_vector.span_mono
simp add: image_image case_prod_unfold butterfly_comp_cblinfun image_def)
finally show ?thesis
using finite_rank_cspan_butterflies by blast
qed
lemma finite_rank_comp_right: ‹finite_rank (a o⇩C⇩L b)› if ‹finite_rank b›
for a b :: ‹_::chilbert_space ⇒⇩C⇩L _::chilbert_space›
proof -
from that
have ‹b ∈ cspan (range (case_prod butterfly))›
by (simp add: finite_rank_cspan_butterflies)
then have ‹a o⇩C⇩L b ∈ ((o⇩C⇩L) a) ` cspan (range (case_prod butterfly))›
by fast
also have ‹… = cspan (((o⇩C⇩L) a) ` range (case_prod butterfly))›
by (simp add: clinear_cblinfun_compose_right complex_vector.linear_span_image)
also have ‹… ⊆ cspan (range (case_prod butterfly))›
by (force intro!: complex_vector.span_mono
simp add: image_image case_prod_unfold cblinfun_comp_butterfly image_def)
finally show ?thesis
using finite_rank_cspan_butterflies by blast
qed
subsection ‹Compact operators›
definition compact_map where ‹compact_map f ⟷ clinear f ∧ compact (closure (f ` cball 0 1))›
lemma ‹bounded_clinear f› if ‹compact_map f›
thm bounded_clinear_def
proof (unfold bounded_clinear_def bounded_clinear_axioms_def, intro conjI)
show ‹clinear f›
using compact_map_def that by blast
have ‹compact (closure (f ` cball 0 1))›
using compact_map_def that by blast
then have ‹bounded (f ` cball 0 1)›
by (meson bounded_subset closure_subset compact_imp_bounded)
then obtain K where *: ‹norm (f x) ≤ K› if ‹norm x ≤ 1› for x
by (force simp: bounded_iff dist_norm ball_def)
have ‹norm (f x) ≤ norm x * K› for x
proof (cases ‹x = 0›)
case True
then show ?thesis
using ‹clinear f› complex_vector.linear_0 by force
next
case False
have ‹norm (f x) = norm (f (norm x *⇩C sgn x))›
by simp
also have ‹… = norm x * norm (f (sgn x))›
by (smt (verit, best) ‹clinear f› complex_vector.linear_scale norm_ge_zero norm_of_real norm_scaleC)
also have ‹… ≤ norm x * K›
by (simp add: "*" mult_left_mono norm_sgn)
finally show ?thesis
by -
qed
then show ‹∃K. ∀x. norm (f x) ≤ norm x * K›
by blast
qed
lift_definition compact_op :: ‹('a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector) ⇒ bool› is compact_map.
lemma compact_op_def2: ‹compact_op a ⟷ compact (closure (a ` cball 0 1))›
by transfer (use bounded_clinear.clinear compact_map_def in blast)
lemma compact_op_0[simp]: ‹compact_op 0›
by (simp add: compact_op_def2 image_constant[where x=0] mem_cball_leI[where x=0])
lemma compact_op_scaleC[simp]: ‹compact_op (c *⇩C a)› if ‹compact_op a›
proof -
have ‹compact (closure (a ` cball 0 1))›
using compact_op_def2 that by blast
then have *: ‹compact (scaleC c ` closure (a ` cball 0 1))›
using compact_scaleC by blast
have ‹closure ((c *⇩C a) ` cball 0 1) = closure (scaleC c ` a ` cball 0 1)›
by (metis (no_types, lifting) cblinfun.scaleC_left image_cong image_image)
also have ‹… = scaleC c ` closure (a ` cball 0 1)›
using closure_scaleC by blast
finally have ‹compact (closure ((c *⇩C a) ` cball 0 1))›
using "*" by simp
then show ?thesis
using compact_op_def2 by blast
qed
lemma compact_op_scaleR[simp]: ‹compact_op (c *⇩R a)› if ‹compact_op a›
by (simp add: scaleR_scaleC that)
lemma compact_op_uminus[simp]: ‹compact_op (-a) = compact_op a›
by (metis compact_op_scaleC scaleC_minus1_left verit_minus_simplify(4))
lemma compact_op_plus[simp]: ‹compact_op (a + b)› if ‹compact_op a› and ‹compact_op b›
proof -
have ‹compact (closure (a ` cball 0 1))›
using compact_op_def2 that by blast
moreover have ‹compact (closure (b ` cball 0 1))›
using compact_op_def2 that by blast
ultimately have compact_sum:
‹compact {x + y |x y. x ∈ closure ((*⇩V) a ` cball 0 1)
∧ y ∈ closure ((*⇩V) b ` cball 0 1)}› (is ‹compact ?sum›)
by (rule compact_sums)
have ‹compact (closure ((a + b) ` cball 0 1))›
proof -
have ‹((*⇩V) (a + b) ` cball 0 1) ⊆ ?sum›
using cblinfun.real.add_left closure_subset image_subset_iff by blast
then have ‹closure ((*⇩V) (a + b) ` cball 0 1) ⊆ closure ?sum›
by (meson closure_mono)
also have ‹… = ?sum›
using compact_sum
by (auto intro!: closure_closed compact_imp_closed)
finally show ?thesis
by (rule compact_closed_subset[rotated 2]) (use compact_sum in auto)
qed
then show ?thesis
using compact_op_def2 by blast
qed
lemma csubspace_compact_op: ‹csubspace (Collect compact_op)›
by (simp add: complex_vector.subspace_def)
lemma compact_op_minus[simp]: ‹compact_op (a - b)› if ‹compact_op a› and ‹compact_op b›
by (metis compact_op_plus compact_op_uminus that(1) that(2) uminus_add_conv_diff)
lemma compact_op_sgn[simp]: ‹compact_op (sgn a) = compact_op a›
proof (cases ‹a = 0›)
case True
then show ?thesis
by simp
next
case False
have ‹compact_op (sgn a)› if ‹compact_op a›
by (simp add: sgn_cblinfun_def that)
moreover have ‹compact_op (norm a *⇩R sgn a)› if ‹compact_op (sgn a)›
by (simp add: that)
moreover have ‹norm a *⇩R sgn a = a›
by (simp add: False sgn_div_norm)
ultimately show ?thesis
by auto
qed
lemma closed_compact_op:
shows ‹closed (Collect (compact_op :: ('a::complex_normed_vector ⇒⇩C⇩L 'b::chilbert_space) ⇒ bool))›
proof (intro closed_sequential_limits[THEN iffD2] allI impI conjI)
fix T and A :: ‹'a ⇒⇩C⇩L 'b›
assume asm: ‹(∀n. T n ∈ Collect compact_op) ∧ T ⇢ A›
have ‹Met_TC.mtotally_bounded (A ` cball 0 1)›
proof (unfold Met_TC.mtotally_bounded_def, intro allI impI)
fix ε :: real assume ‹ε > 0›
define δ where ‹δ = ε/3›
then have ‹δ > 0›
using ‹ε > 0› by simp
from asm[unfolded LIMSEQ_def, THEN conjunct2, rule_format, OF ‹δ > 0›]
obtain n where dist_TA: ‹dist (T n) A < δ›
by auto
from asm have ‹compact_op (T n)›
by simp
then have ‹Met_TC.mtotally_bounded (T n ` cball 0 1)›
by (subst Met_TC.mtotally_bounded_eq_compact_closure_of)
(auto intro!: simp: compact_op_def2 Met_TC.mtotally_bounded_eq_compact_closure_of)
then obtain K where ‹finite K› and K_T: ‹K ⊆ T n ` cball 0 1› and
TK: ‹T n ` cball 0 1 ⊆ (⋃k∈K. Met_TC.mball k δ)›
unfolding Met_TC.mtotally_bounded_def using ‹δ > 0› by meson
from ‹finite K› and K_T obtain H where ‹finite H› and ‹H ⊆ cball 0 1›
and KTH: ‹K = T n ` H›
by (meson finite_subset_image)
from TK have TH: ‹T n ` cball 0 1 ⊆ (⋃h∈H. ball (T n *⇩V h) δ)›
by (simp add: KTH)
have ‹A ` cball 0 1 ⊆ (⋃h∈H. ball (A h) ε)›
proof (rule subsetI)
fix x assume ‹x ∈ (*⇩V) A ` cball 0 1›
then obtain l where ‹l ∈ cball 0 1› and xl: ‹x = A l›
by blast
then have ‹T n l ∈ T n ` cball 0 1›
by auto
with TH obtain h where ‹h ∈ H› and ‹T n l ∈ ball (T n h) δ›
by blast
then have dist_Tlh: ‹dist (T n l) (T n h) < δ›
by (simp add: dist_commute)
have ‹dist (A h) (A l) < ε›
proof -
have norm_h: ‹norm h ≤ 1›
using ‹H ⊆ cball 0 1› ‹h ∈ H› mem_cball_0 by blast
have norm_l: ‹norm l ≤ 1›
using ‹l ∈ cball 0 1› by auto
have ‹dist (A h) (T n h) < δ›
proof -
have ‹dist (T n *⇩V h) (A *⇩V h) ≤ norm h * dist (T n) A›
using norm_cblinfun[of "T n - A" h] by (simp add: dist_norm cblinfun.diff_left mult_ac)
also have ‹… ≤ 1 * dist (T n) A›
by (rule mult_right_mono) (use norm_h in auto)
also have ‹dist (T n) A < δ›
by fact
finally show ?thesis
by (simp add: dist_commute)
qed
moreover have ‹dist (T n h) (T n l) < δ›
using dist_Tlh by (metis dist_commute)
moreover from dist_TA norm_l have ‹dist (T n l) (A l) < δ›
proof -
have ‹dist (T n *⇩V l) (A *⇩V l) ≤ norm l * dist (T n) A›
using norm_cblinfun[of "T n - A" l] by (simp add: dist_norm cblinfun.diff_left mult_ac)
also have ‹… ≤ 1 * dist (T n) A›
by (rule mult_right_mono) (use norm_l in auto)
also have ‹dist (T n) A < δ›
by fact
finally show ?thesis
by (simp add: dist_commute)
qed
ultimately show ?thesis
unfolding δ_def
by (rule dist_triangle_third)
qed
then show ‹x ∈ (⋃h∈H. ball (A h) ε) ›
using ‹h ∈ H› by (auto intro!: simp: xl)
qed
then show ‹∃K. finite K ∧ K ⊆ (*⇩V) A ` cball 0 1 ∧
(*⇩V) A ` cball 0 1 ⊆ (⋃x∈K. Met_TC.mball x ε)›
using ‹H ⊆ cball 0 1›
by (force intro!: exI[of _ ‹A ` H›] ‹finite H› simp: ball_def)
qed
then have ‹Met_TC.mtotally_bounded (closure (A ` cball 0 1))›
using Met_TC.mtotally_bounded_closure_of by auto
then have ‹compact (closure (A ` cball 0 1))›
by (simp_all add: Met_TC.mtotally_bounded_eq_compact_closure_of complete_UNIV_cuspace)
then show ‹A ∈ Collect compact_op›
using compact_op_def2 by blast
qed
lemma rank1_compact_op: ‹compact_op a› if ‹rank1 a›
proof -
wlog ‹a ≠ 0›
using negation by simp
with that obtain ψ where im_a: ‹a *⇩S ⊤ = ccspan {ψ}› and ‹ψ ≠ 0›
using rank1_def by fastforce
define c where ‹c = norm a / norm ψ›
have compact_ψc: ‹compact ((λx. x *⇩C ψ) ` cball 0 c)›
proof -
have ‹continuous_on (cball 0 c) (λx. x *⇩C ψ)›
by (auto intro!: continuous_at_imp_continuous_on)
moreover have ‹compact (cball (0::complex) c)›
by (simp add: compact_eq_bounded_closed)
ultimately show ?thesis
by (rule compact_continuous_image)
qed
have ‹a ` cball 0 1 ⊆ (λx. x *⇩C ψ) ` cball 0 c›
proof (rule subsetI)
fix φ
assume asm: ‹φ ∈ a ` cball 0 1›
then have ‹φ ∈ space_as_set (a *⇩S ⊤)›
using cblinfun_apply_in_image by blast
also have ‹… = cspan {ψ}›
by (simp add: ccspan.rep_eq im_a)
finally obtain d where d: ‹φ = d *⇩C ψ›
by (metis complex_vector.span_breakdown_eq complex_vector.span_empty eq_iff_diff_eq_0 singletonD)
from asm obtain γ where ‹φ = a γ› and ‹norm γ ≤ 1›
by force
have ‹cmod d * norm ψ = norm φ›
by (simp add: d)
also have ‹… ≤ norm a * norm γ›
using ‹φ = a *⇩V γ› complex_of_real_mono norm_cblinfun by blast
also have ‹… ≤ norm a›
by (metis ‹norm γ ≤ 1› mult.commute mult_left_le_one_le norm_ge_zero)
finally have ‹cmod d ≤ c›
by (smt (verit, ccfv_threshold) ‹ψ ≠ 0› c_def linordered_field_class.pos_divide_le_eq nonzero_eq_divide_eq norm_le_zero_iff)
then show ‹φ ∈ (λx. x *⇩C ψ) ` cball 0 c›
by (auto simp: d)
qed
with compact_ψc have cl_in_cl: ‹closure (a ` cball 0 1) ⊆ ((λx. x *⇩C ψ) ` cball 0 c)›
using closure_mono[of _ ‹((λx. x *⇩C ψ) ` cball 0 c)›] compact_ψc
by (simp add: compact_imp_closed)
with compact_ψc show ‹compact_op a›
using compact_closed_subset compact_op_def2 by blast
qed
lemma finite_rank_compact_op: ‹compact_op a› if ‹finite_rank a›
proof -
from that obtain t r where ‹finite t› and ‹t ⊆ Collect rank1›
and a_decomp: ‹a = (∑x∈t. r x *⇩C x)›
by (auto simp: finite_rank_def complex_vector.span_explicit)
from ‹finite t› ‹t ⊆ Collect rank1› show ‹compact_op a›
by (unfold a_decomp, induction)
(auto intro!: compact_op_plus compact_op_scaleC intro: rank1_compact_op)
qed
lemma bounded_products_sot_lim_imp_lim:
fixes A :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::chilbert_space›
assumes lim_PA: ‹limitin cstrong_operator_topology (λx. P x o⇩C⇩L A) A F›
and ‹compact_op A›
and P_leq_B: ‹⋀x. norm (P x) ≤ B›
shows ‹((λx. P x o⇩C⇩L A) ⤏ A) F›
proof -
wlog ‹F ≠ ⊥›
using negation by simp
wlog ‹B ≠ 0›
proof -
from negation assms have P0: ‹P x = 0› for x
by auto
from lim_PA have ‹((λx. 0) ⤏ Abs_cblinfun_sot A) F›
unfolding limitin_canonical_iff [symmetric]
by (transfer fixing: P F) (use P0 in simp)
moreover have ‹((λx. 0) ⤏ 0) F›
by simp
ultimately have ‹Abs_cblinfun_sot A = 0›
using ‹F ≠ ⊥› tendsto_unique by blast
then have ‹A = 0›
by (metis Abs_cblinfun_sot_inverse cstrong_operator_topology_topspace lim_PA
limitin_def zero_cblinfun_sot.rep_eq)
with P0 show ?thesis
by simp
qed
have ‹B > 0›
proof -
from P_leq_B[of undefined] have ‹B ≥ 0›
by (smt (verit, del_insts) norm_ge_zero)
with ‹B ≠ 0›
show ?thesis
by simp
qed
show ?thesis
proof (rule metric_space_class.tendstoI)
fix ε :: real assume ‹ε > 0›
define δ γ T where ‹δ = ε/4› and ‹γ = min δ (δ/B)› and ‹T x = P x o⇩C⇩L A› for x
then have ‹δ > 0›
using ‹ε > 0› by simp
then have ‹γ > 0›
using ‹B > 0› by (simp add: γ_def)
from ‹compact_op A› have ‹Met_TC.mtotally_bounded (A ` cball 0 1)›
by (subst Met_TC.mtotally_bounded_eq_compact_closure_of)
(auto intro!: simp: compact_op_def2 Met_TC.mtotally_bounded_eq_compact_closure_of)
then obtain K where ‹finite K› and K_T: ‹K ⊆ A ` cball 0 1› and
AK: ‹A ` cball 0 1 ⊆ (⋃k∈K. Met_TC.mball k γ)›
unfolding Met_TC.mtotally_bounded_def using ‹γ > 0› by meson
from ‹finite K› and K_T obtain H where ‹finite H› and ‹H ⊆ cball 0 1›
and KAH: ‹K = A ` H›
by (meson finite_subset_image)
from AK have AH: ‹A ` cball 0 1 ⊆ (⋃h∈H. ball (A *⇩V h) γ)›
by (simp add: KAH)
have ‹∀⇩F x in F. ∀h∈H. dist (T x h) (A h) < δ›
using lim_PA ‹δ > 0›
by (auto intro!: eventually_ball_finite ‹finite H›
simp: limitin_cstrong_operator_topology T_def metric_space_class.tendsto_iff)
then show ‹∀⇩F x in F. dist (T x) A < ε›
proof (rule eventually_mono)
fix x
assume asm: ‹∀h∈H. dist (T x *⇩V h) (A *⇩V h) < δ›
have ‹dist (T x l) (A l) ≤ 3 * δ› if ‹norm l = 1› for l
proof -
from that have ‹A l ∈ A ` cball 0 1›
by auto
with AH obtain h where ‹h ∈ H› and Alγ: ‹A l ∈ ball (A h) γ›
by blast
then have dist_Alh: ‹dist (A l) (A h) < γ›
by (simp add: dist_commute)
have ‹dist (A l) (A h) < δ›
using dist_Alh by (simp add: γ_def)
moreover from asm have ‹dist (A h) (T x h) < δ›
by (simp add: ‹h ∈ H› dist_commute)
moreover have ‹dist (T x h) (T x l) < δ›
proof -
have ‹dist (T x h) (T x l) ≤ norm (P x) * dist (A h) (A l)›
by (metis T_def cblinfun.real.diff_right cblinfun_apply_cblinfun_compose
dist_norm norm_cblinfun)
also from Alγ P_leq_B have ‹… < B * γ›
by (metis ‹0 < B› dist_Alh dist_commute mult_le_less_imp_less mult_strict_mono norm_zero
zero_le_dist zero_less_norm_iff)
also have ‹… ≤ B * (δ / B)›
by (smt (verit, best) γ_def ‹0 < B› mult_left_mono)
also have ‹… ≤ δ›
by (simp add: ‹B ≠ 0›)
finally show ?thesis .
qed
ultimately show ?thesis
by (smt (verit) dist_commute dist_triangle2)
qed
then have ‹dist (T x) A ≤ 3 * δ›
unfolding dist_norm using ‹δ > 0›
by (auto intro!: norm_cblinfun_bound_unit simp: cblinfun.diff_left)
then show ‹dist (T x) A < ε›
by (rule order.strict_trans1) (use ‹ε > 0› in ‹simp add: δ_def›)
qed
qed
qed
lemma compact_op_finite_rank:
fixes A :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::chilbert_space›
shows ‹compact_op A ⟷ A ∈ closure (Collect finite_rank)›
proof (rule iffI)
assume ‹A ∈ closure (Collect finite_rank)›
then have ‹A ∈ closure (Collect compact_op)›
by (metis closure_sequential finite_rank_compact_op mem_Collect_eq)
also have ‹… = Collect compact_op›
by (simp add: closed_compact_op)
finally show ‹compact_op A›
by simp
next
assume ‹compact_op A›
then have ‹compact (closure (A ` cball 0 1))›
using compact_op_def2 by blast
then have sep_A_ball: ‹separable (closure (A ` cball 0 1))›
using compact_imp_separable by blast
define L where ‹L = closure (range A)›
obtain B :: ‹nat ⇒ _› where ‹L ⊆ closure (range B)›
proof atomize_elim
from sep_A_ball obtain B0 where ‹countable B0›
and A_B0: ‹A ` cball 0 1 ⊆ closure B0›
by (meson closure_subset order_trans separable_def)
define B1 where ‹B1 = (⋃n::nat. scaleR n ` B0)›
from ‹countable B0› have ‹countable B1›
by (auto intro!: countable_UN countable_image simp: B1_def)
have ‹range A = (⋃n::nat. A ` scaleR n ` cball (0::'a) 1)›
proof -
have ‹UNIV = (⋃n::nat. scaleR n ` cball (0::'a) 1)›
proof (intro antisym subsetI UNIV_I)
fix x :: 'a
have "norm x < 1 + real_of_int ⌈norm x⌉" "1 + real_of_int ⌈norm x⌉ > 0"
using norm_ge_zero[of x] by linarith+
hence ‹x ∈ scaleR (nat (ceiling (norm x)) + 1) ` cball (0::'a) 1›
by (intro image_eqI[where x=‹x /⇩R (nat (ceiling (norm x)) + 1)›])
(auto simp: divide_simps)
then show ‹x ∈ (⋃x::nat. (*⇩R) (real x) ` cball 0 1)›
by blast
qed
then show ?thesis
by fastforce
qed
also have ‹… = (⋃n::nat. scaleR n ` A ` cball 0 1)›
by (auto simp: cblinfun.scaleR_right image_comp fun_eq_iff)
also have ‹… ⊆ (⋃n::nat. scaleR n ` closure B0)›
using A_B0 by fastforce
also have ‹… ⊆ closure (⋃n::nat. scaleR n ` B0)›
by (metis (mono_tags, lifting) SUP_le_iff closure_closure closure_mono closure_scaleR closure_subset)
also have ‹… = closure B1›
using B1_def by fastforce
finally have ‹L ⊆ closure B1›
by (simp add: L_def closure_minimal)
with ‹countable B1›
show ‹∃B :: nat ⇒ _. L ⊆ closure (range B)›
by (metis L_def closure_eq_empty empty_not_UNIV image_is_empty range_from_nat_into subset_empty)
qed
define P T where ‹P n = Proj (ccspan (B ` {..n}))›
and ‹T n = P n o⇩C⇩L A› for n
have ‹limitin cstrong_operator_topology T A sequentially›
proof (intro limitin_cstrong_operator_topology[THEN iffD2, rule_format] metric_LIMSEQ_I)
fix h and ε :: real assume ‹ε > 0›
define Ah where ‹Ah = A h›
have ‹Ah ∈ closure (range B)›
by (metis L_def Ah_def ‹L ⊆ closure (range B)› cblinfun_apply_in_image
cblinfun_image.rep_eq subsetD top_ccsubspace.rep_eq)
then obtain x where ‹x ∈ range B› and ‹dist x Ah < ε›
using ‹ε > 0› unfolding closure_approachable by blast
then obtain n0 where x_n0: ‹x = B n0›
by blast
have ‹dist (P n *⇩V Ah) Ah < ε› if ‹n ≥ n0› for n
proof -
have ‹x ∈ space_as_set (P n *⇩S ⊤)›
using ‹n ≥ n0›
by (auto intro!: ccspan_superset' simp: P_def x_n0)
from Proj_nearest[OF this, of Ah]
have ‹dist (P n *⇩V Ah) Ah ≤ dist x Ah›
by (simp add: P_def)
with ‹dist x Ah < ε› show ?thesis
by auto
qed
then show ‹∃n0. ∀n≥n0. dist (T n *⇩V h) (A *⇩V h) < ε›
unfolding T_def Ah_def by auto
qed
then have ‹((λx. P x o⇩C⇩L A) ⤏ A) sequentially›
unfolding T_def
by (auto intro!: bounded_products_sot_lim_imp_lim[where B=1] ‹compact_op A› norm_is_Proj
simp: P_def)
moreover have ‹finite_rank (P x o⇩C⇩L A)› for x
by (auto intro!: finite_rank_compose_right finite_rank_Proj_finite simp: P_def)
ultimately show ‹A ∈ closure (Collect finite_rank)›
using closure_sequential by force
qed
typedef (overloaded) ('a::chilbert_space,'b::complex_normed_vector) compact_op =
‹Collect compact_op :: ('a ⇒⇩C⇩L 'b) set›
morphisms from_compact_op Abs_compact_op
by (auto intro!: exI[of _ 0])
setup_lifting type_definition_compact_op
instantiation compact_op :: (chilbert_space, complex_normed_vector) complex_normed_vector begin
lift_definition scaleC_compact_op :: ‹complex ⇒ ('a, 'b) compact_op ⇒ ('a, 'b) compact_op› is scaleC by simp
lift_definition uminus_compact_op :: ‹('a, 'b) compact_op ⇒ ('a, 'b) compact_op› is uminus by simp
lift_definition zero_compact_op :: ‹('a, 'b) compact_op› is 0 by simp
lift_definition minus_compact_op :: ‹('a, 'b) compact_op ⇒ ('a, 'b) compact_op ⇒ ('a, 'b) compact_op› is minus by simp
lift_definition plus_compact_op :: ‹('a, 'b) compact_op ⇒ ('a, 'b) compact_op ⇒ ('a, 'b) compact_op› is plus by simp
lift_definition sgn_compact_op :: ‹('a, 'b) compact_op ⇒ ('a, 'b) compact_op› is sgn by simp
lift_definition norm_compact_op :: ‹('a, 'b) compact_op ⇒ real› is norm .
lift_definition scaleR_compact_op :: ‹real ⇒ ('a, 'b) compact_op ⇒ ('a, 'b) compact_op› is scaleR by simp
lift_definition dist_compact_op :: ‹('a, 'b) compact_op ⇒ ('a, 'b) compact_op ⇒ real› is dist .
definition [code del]:
‹(uniformity :: (('a, 'b) compact_op × ('a, 'b) compact_op) filter) = (INF e∈{0 <..}. principal {(x, y). dist x y < e})›
definition open_compact_op :: "('a, 'b) compact_op set ⇒ bool"
where [code del]: "open_compact_op S = (∀x∈S. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ S)"
instance
proof
show "((*⇩R) r :: ('a, 'b) compact_op ⇒ _) = (*⇩C) (complex_of_real r)" for r
by (rule ext, transfer) (simp add: scaleR_scaleC)
show "a + b + c = a + (b + c)"
for a b c :: "('a, 'b) compact_op"
by transfer simp
show "a + b = b + a"
for a b :: "('a, 'b) compact_op"
by transfer simp
show "0 + a = a"
for a :: "('a, 'b) compact_op"
by transfer simp
show "- (a::('a, 'b) compact_op) + a = 0"
for a :: "('a, 'b) compact_op"
by transfer simp
show "a - b = a + - b"
for a b :: "('a, 'b) compact_op"
by transfer simp
show "a *⇩C (x + y) = a *⇩C x + a *⇩C y"
for a :: complex and x y :: "('a, 'b) compact_op"
by transfer (simp add: scaleC_add_right)
show "(a + b) *⇩C x = a *⇩C x + b *⇩C x"
for a b :: complex and x :: "('a, 'b) compact_op"
by transfer (simp add: scaleC_left.add)
show "a *⇩C b *⇩C x = (a * b) *⇩C x"
for a b :: complex and x :: "('a, 'b) compact_op"
by transfer simp
show "1 *⇩C x = x"
for x :: "('a, 'b) compact_op"
by transfer simp
show "dist x y = norm (x - y)"
for x y :: "('a, 'b) compact_op"
by transfer (simp add: dist_norm)
show "a *⇩R (x + y) = a *⇩R x + a *⇩R y"
for a :: real and x y :: "('a, 'b) compact_op"
by transfer (simp add: scaleR_right_distrib)
show "(a + b) *⇩R x = a *⇩R x + b *⇩R x"
for a b :: real and x :: "('a, 'b) compact_op"
by transfer (simp add: scaleR_left.add)
show "a *⇩R b *⇩R x = (a * b) *⇩R x"
for a b :: real and x :: "('a, 'b) compact_op"
by transfer simp
show "1 *⇩R x = x"
for x :: "('a, 'b) compact_op"
by transfer simp
show "sgn x = inverse (norm x) *⇩R x"
for x :: "('a, 'b) compact_op"
by transfer (simp add: sgn_div_norm)
show "uniformity = (INF e∈{0<..}. principal {(x, y). dist (x::('a, 'b) compact_op) y < e})"
using uniformity_compact_op_def by blast
show "open U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)"
for U :: "('a, 'b) compact_op set"
by (simp add: open_compact_op_def)
show "(norm x = 0) ⟷ (x = 0)"
for x :: "('a, 'b) compact_op"
by transfer simp
show "norm (x + y) ≤ norm x + norm y"
for x y :: "('a, 'b) compact_op"
by transfer (use norm_triangle_ineq in blast)
show "norm (a *⇩R x) = ¦a¦ * norm x"
for a :: real and x :: "('a, 'b) compact_op"
by transfer simp
show "norm (a *⇩C x) = cmod a * norm x"
for a :: complex and x :: "('a, 'b) compact_op"
by transfer simp
qed
end
lemma from_compact_op_plus: ‹from_compact_op (a + b) = from_compact_op a + from_compact_op b›
by transfer simp
lemma from_compact_op_scaleC: ‹from_compact_op (c *⇩C a) = c *⇩C from_compact_op a›
by transfer simp
lemma from_compact_op_norm[simp]: ‹norm (from_compact_op a) = norm a›
by transfer simp
lemma compact_op_butterfly[simp]: ‹compact_op (butterfly x y)›
by (simp add: finite_rank_compact_op)
lift_definition butterfly_co :: ‹'a::complex_normed_vector ⇒ 'b::chilbert_space ⇒ ('b,'a) compact_op› is butterfly
by simp
lemma butterfly_co_add_left: ‹butterfly_co (a + a') b = butterfly_co a b + butterfly_co a' b›
by transfer (rule butterfly_add_left)
lemma butterfly_co_add_right: ‹butterfly_co a (b + b') = butterfly_co a b + butterfly_co a b'›
by transfer (rule butterfly_add_right)
lemma butterfly_co_scaleR_left[simp]: "butterfly_co (r *⇩R ψ) φ = r *⇩C butterfly_co ψ φ"
by transfer (rule butterfly_scaleR_left)
lemma butterfly_co_scaleR_right[simp]: "butterfly_co ψ (r *⇩R φ) = r *⇩C butterfly_co ψ φ"
by transfer (rule butterfly_scaleR_right)
lemma butterfly_co_scaleC_left[simp]: "butterfly_co (r *⇩C ψ) φ = r *⇩C butterfly_co ψ φ"
by transfer (rule butterfly_scaleC_left)
lemma butterfly_co_scaleC_right[simp]: "butterfly_co ψ (r *⇩C φ) = cnj r *⇩C butterfly_co ψ φ"
by transfer (rule butterfly_scaleC_right)
lemma finite_rank_separating_on_compact_op:
fixes F G :: ‹('a::chilbert_space,'b::chilbert_space) compact_op ⇒ 'c::complex_normed_vector›
assumes ‹⋀x. finite_rank (from_compact_op x) ⟹ F x = G x›
assumes ‹bounded_clinear F›
assumes ‹bounded_clinear G›
shows ‹F = G›
proof -
define FG where ‹FG x = F x - G x› for x
from ‹bounded_clinear F› and ‹bounded_clinear G›
have ‹bounded_clinear FG›
by (auto simp: FG_def[abs_def] intro!: bounded_clinear_sub)
then have contFG': ‹continuous_map euclidean euclidean FG›
by (simp add: Complex_Vector_Spaces.bounded_clinear.bounded_linear linear_continuous_on)
have ‹continuous_on (Collect compact_op) (FG o Abs_compact_op)›
proof
fix a :: "'a ⇒⇩C⇩L 'b" and e :: real
assume "0 < e" and a_compact: "a ∈ Collect compact_op"
have dist_rw: ‹dist x' a = dist (Abs_compact_op x') (Abs_compact_op a)› if ‹compact_op x'› for x'
by (metis Abs_compact_op_inverse a_compact dist_compact_op.rep_eq mem_Collect_eq that)
from ‹bounded_clinear FG›
have ‹continuous_on UNIV FG›
using contFG' continuous_map_iff_continuous2 by blast
then have ‹∃d>0. ∀x'. dist x' (Abs_compact_op a) < d ⟶ dist (FG x') (FG (Abs_compact_op a)) ≤ e›
using ‹e > 0› by (force simp: continuous_on_iff)
then have ‹∃d>0. ∀x'. compact_op x' ⟶ dist (Abs_compact_op x') (Abs_compact_op a) < d ⟶
dist (FG (Abs_compact_op x')) (FG (Abs_compact_op a)) ≤ e›
by blast
then show "∃d>0. ∀x'∈Collect compact_op. dist x' a < d ⟶ dist ((FG ∘ Abs_compact_op) x') ((FG ∘ Abs_compact_op) a) ≤ e"
by (simp add: dist_rw o_def)
qed
then have contFG: ‹continuous_on (closure (Collect finite_rank)) (FG o Abs_compact_op)›
by (auto simp: compact_op_finite_rank[abs_def])
have FG0: ‹finite_rank a ⟹ (FG o Abs_compact_op) a = 0› for a
by (metis (no_types, lifting) Abs_compact_op_inverse FG_def assms(1) closure_subset comp_apply compact_op_finite_rank eq_iff_diff_eq_0 mem_Collect_eq subset_eq)
have ‹(FG o Abs_compact_op) a = 0› if ‹compact_op a› for a
using contFG FG0
by (rule continuous_constant_on_closure) (use that in ‹auto simp: compact_op_finite_rank›)
then have ‹FG a = 0› for a
by (metis Abs_compact_op_cases comp_apply mem_Collect_eq)
then show ‹F = G›
by (auto simp: FG_def[abs_def] fun_eq_iff)
qed
lemma trunc_ell2_as_Proj: ‹trunc_ell2 S ψ = Proj (ccspan (ket ` S)) ψ›
proof (rule cinner_ket_eqI)
fix x
have *: ‹Proj (ccspan (ket ` S)) (ket x) = 0› if ‹x ∉ S›
by (auto intro!: Proj_0_compl mem_ortho_ccspanI simp: that)
have ‹ket x ∙⇩C trunc_ell2 S ψ = of_bool (x∈S) * (ket x ∙⇩C ψ)›
by (simp add: cinner_ket_left trunc_ell2.rep_eq)
also have ‹… = Proj (ccspan (ket ` S)) (ket x) ∙⇩C ψ›
by (cases ‹x ∈ S›) (auto simp add: * ccspan_superset' Proj_fixes_image)
also have ‹… = ket x ∙⇩C (Proj (ccspan (ket ` S)) *⇩V ψ)›
by (simp add: adj_Proj flip: cinner_adj_left)
finally show ‹ket x ∙⇩C trunc_ell2 S ψ = ket x ∙⇩C (Proj (ccspan (ket ` S)) *⇩V ψ)› .
qed
lemma unitary_between_bij_betw:
assumes ‹is_onb A› ‹is_onb B›
shows ‹bij_betw ((*⇩V) (unitary_between A B)) A B›
using bij_between_bases_bij[OF assms]
by (rule bij_betw_cong[THEN iffD1, rotated])
(simp add: assms(1) assms(2) unitary_between_apply)
lemma tendsto_finite_subsets_at_top_image:
assumes ‹inj_on g X›
shows ‹(f ⤏ x) (finite_subsets_at_top (g ` X)) ⟷ ((λS. f (g ` S)) ⤏ x) (finite_subsets_at_top X)›
by (simp add: filterlim_def assms o_def
flip: filtermap_image_finite_subsets_at_top filtermap_compose)
lemma Proj_onb_limit:
shows ‹is_onb A ⟹ ((λS. Proj (ccspan S) ψ) ⤏ ψ) (finite_subsets_at_top A)›
proof -
have main: ‹((λS. Proj (ccspan S) ψ) ⤏ ψ) (finite_subsets_at_top A)› if ‹is_onb A›
for ψ :: ‹'b::{chilbert_space,not_singleton}› and A
proof -
define U where ‹U = unitary_between (ell2_to_hilbert* ` A) (range ket)›
have [simp]: ‹unitary U›
by (simp add: U_def that unitary_between_unitary unitary_image_onb)
have lim1: ‹((λS. trunc_ell2 S (U *⇩V ell2_to_hilbert* *⇩V ψ)) ⤏ U *⇩V ell2_to_hilbert* *⇩V ψ) (finite_subsets_at_top UNIV)›
by (rule trunc_ell2_lim_at_UNIV)
have lim2: ‹((λS. ell2_to_hilbert *⇩V U* *⇩V trunc_ell2 S (U *⇩V ell2_to_hilbert* *⇩V ψ)) ⤏ ell2_to_hilbert *⇩V U* *⇩V U *⇩V ell2_to_hilbert* *⇩V ψ) (finite_subsets_at_top UNIV)›
by (intro cblinfun.tendsto lim1) auto
have *: ‹ell2_to_hilbert *⇩V U* *⇩V trunc_ell2 S (U *⇩V ell2_to_hilbert* *⇩V ψ)
= Proj (ccspan ((ell2_to_hilbert o U* o ket) ` S)) ψ› (is ‹?lhs = ?rhs›) for S
proof -
have ‹?lhs = (sandwich ell2_to_hilbert *⇩V sandwich (U*) *⇩V Proj (ccspan (ket ` S))) *⇩V ψ›
by (simp add: trunc_ell2_as_Proj sandwich_apply)
also have ‹… = Proj (ell2_to_hilbert *⇩S U* *⇩S ccspan (ket ` S)) *⇩V ψ›
by (simp add: Proj_sandwich)
also have ‹… = Proj (ccspan (ell2_to_hilbert ` U* ` ket ` S)) *⇩V ψ›
by (simp add: cblinfun_image_ccspan)
also have ‹… = ?rhs›
by (simp add: image_comp)
finally show ?thesis
by -
qed
have **: ‹ell2_to_hilbert *⇩V U* *⇩V U *⇩V ell2_to_hilbert* *⇩V ψ = ψ›
by (simp add: lift_cblinfun_comp[OF unitaryD1] lift_cblinfun_comp[OF unitaryD2])
have ***: ‹range (ell2_to_hilbert o U* o ket) = A› (is ‹?lhs = _›)
proof -
have ‹bij_betw U (ell2_to_hilbert* ` A) (range ket)›
by (auto intro!: unitary_between_bij_betw that unitary_image_onb simp add: U_def)
then have bijUadj: ‹bij_betw (U*) (range ket) (ell2_to_hilbert* ` A)›
by (metis ‹unitary U› bij_betw_imp_surj_on inj_imp_bij_betw_inv unitary_adj_inv unitary_inj)
have ‹?lhs = ell2_to_hilbert ` U* ` range ket›
by (simp add: image_comp)
also from this and bijUadj have ‹… = ell2_to_hilbert ` (ell2_to_hilbert* ` A)›
by (metis bij_betw_imp_surj_on)
also have ‹… = A›
by (metis image_inv_f_f unitary_adj unitary_adj_inv unitary_ell2_to_hilbert unitary_inj)
finally show ?thesis
by -
qed
from lim2 have lim3: ‹((λS. Proj (ccspan ((ell2_to_hilbert o U* o ket) ` S)) ψ) ⤏ ψ) (finite_subsets_at_top UNIV)›
unfolding * ** by -
then have lim4: ‹((λS. Proj (ccspan S) ψ) ⤏ ψ) (finite_subsets_at_top (range (ell2_to_hilbert o U* o ket)))›
by (rule tendsto_finite_subsets_at_top_image[THEN iffD2, rotated])
(intro inj_compose unitary_inj unitary_ell2_to_hilbert unitary_adj[THEN iffD2] ‹unitary U› inj_ket)
then show ?thesis
unfolding *** by -
qed
assume ‹is_onb A›
show ?thesis
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
using chilbert_space_class.chilbert_space_axioms True ‹is_onb A›
by (rule main[internalize_sort' 'b2])
next
case False
then have ‹ψ = 0›
by (rule not_not_singleton_zero)
then show ?thesis
by simp
qed
qed
lemma is_ortho_setD:
assumes "is_ortho_set S" "x ∈ S" "y ∈ S" "x ≠ y"
shows "x ∙⇩C y = 0"
using assms unfolding is_ortho_set_def by blast
lemma finite_rank_dense_compact:
fixes A :: ‹'a::chilbert_space set› and B :: ‹'b::chilbert_space set›
assumes ‹is_onb A› and ‹is_onb B›
shows ‹closure (cspan ((λ(ξ,η). butterfly ξ η) ` (A × B))) = Collect compact_op›
proof (rule Set.equalityI)
show ‹closure (cspan ((λ(ξ,η). butterfly ξ η) ` (A × B))) ⊆ Collect compact_op›
proof -
have ‹closure (cspan ((λ(ξ,η). butterfly ξ η) ` (A × B))) ⊆ closure (Collect finite_rank)›
proof (rule closure_mono; safe)
fix x assume "x ∈ cspan ((λ(ξ, η). butterfly ξ η) ` (A × B))"
thus "finite_rank x"
by (induction rule: complex_vector.span_induct_alt) auto
qed
also have ‹… = Collect compact_op›
by (simp add: Set.set_eqI compact_op_finite_rank)
finally show ?thesis
by -
qed
show ‹Collect compact_op ⊆ closure (cspan ((λ(ξ,η). butterfly ξ η) ` (A × B)))›
proof -
have ‹Collect (compact_op :: 'b⇒⇩C⇩L'a ⇒ _) = closure (cspan (Collect rank1))›
by (simp add: compact_op_finite_rank[abs_def] finite_rank_def[abs_def])
also have ‹… ⊆ closure (cspan (closure (cspan ((λ(ξ,η). butterfly ξ η) ` (A × B)))))›
proof (rule closure_mono, rule complex_vector.span_mono, rule subsetI)
fix x :: ‹'b ⇒⇩C⇩L 'a› assume ‹x ∈ Collect rank1›
then obtain a b where xab: ‹x = butterfly a b›
using rank1_iff_butterfly by fastforce
define f where ‹f F G = butterfly (Proj (ccspan F) a) (Proj (ccspan G) b)› for F G
have lim: ‹(case_prod f ⤏ x) (finite_subsets_at_top A ×⇩F finite_subsets_at_top B)›
proof (rule tendstoI, subst dist_norm)
fix e :: real assume ‹e > 0›
define d where ‹d = (if norm a = 0 ∧ norm b = 0 then 1
else e / (max (norm a) (norm b)) / 4)›
have [simp]: "d > 0"
unfolding d_def using ‹e > 0›
by (auto intro!: divide_pos_pos simp: less_max_iff_disj)
have d: ‹norm a * d + norm a * d + norm b * d < e›
proof -
have ‹x * d ≤ e / 4› if x: "x ∈ {norm a, norm b}" for x
proof (cases "x = 0")
case False
have d: "d = e / (max (norm a) (norm b)) / 4"
using False x by (auto simp: d_def)
have "d ≤ e / x / 4"
unfolding d by (intro divide_left_mono divide_right_mono)
(use x ‹d > 0› ‹e > 0› False in ‹auto simp: less_max_iff_disj›)
thus ?thesis
using False x by (auto simp: field_simps)
qed (use ‹e > 0› in auto)
hence "norm a * d ≤ e / 4" "norm b * d ≤ e / 4"
by blast+
hence ‹norm a * d + norm a * d + norm b * d ≤ 3 * e / 4›
by linarith
also have ‹… < e›
by (simp add: ‹0 < e›)
finally show ?thesis .
qed
from Proj_onb_limit[where ψ=a, OF assms(1)]
have ‹∀⇩F F in finite_subsets_at_top A. norm (Proj (ccspan F) a - a) < d›
by (metis Lim_null ‹0 < d› order_tendstoD(2) tendsto_norm_zero_iff)
moreover from Proj_onb_limit[where ψ=b, OF assms(2)]
have ‹∀⇩F G in finite_subsets_at_top B. norm (Proj (ccspan G) b - b) < d›
by (metis Lim_null ‹0 < d› order_tendstoD(2) tendsto_norm_zero_iff)
ultimately have FG_close: ‹∀⇩F (F,G) in finite_subsets_at_top A ×⇩F finite_subsets_at_top B.
norm (Proj (ccspan F) a - a) < d ∧ norm (Proj (ccspan G) b - b) < d›
unfolding case_prod_beta
by (rule eventually_prodI)
have fFG_dist: ‹norm (f F G - x) < e›
if ‹norm (Proj (ccspan F) a - a) < d› and ‹norm (Proj (ccspan G) b - b) < d›
and ‹F ⊆ A› and ‹G ⊆ B› for F G
proof -
have a_split: ‹a = Proj (ccspan F) *⇩V a + Proj (ccspan (A-F)) *⇩V a›
proof -
have A: "is_ortho_set A" "ccspan A = ⊤"
using assms unfolding is_onb_def by auto
have "Proj (ccspan (F ∪ A)) = Proj (ccspan F) + Proj (ccspan (A-F))"
by (subst Proj_orthog_ccspan_union [symmetric])
(use that in ‹auto intro!: is_ortho_setD[OF A(1)]›)
also have "F ∪ A = A"
using that by blast
finally show ?thesis
using A(2) by (simp flip: cblinfun.add_left)
qed
have b_split: ‹b = Proj (ccspan G) *⇩V b + Proj (ccspan (B-G)) *⇩V b›
proof -
have B: "is_ortho_set B" "ccspan B = ⊤"
using assms unfolding is_onb_def by auto
have "Proj (ccspan (G ∪ B)) = Proj (ccspan G) + Proj (ccspan (B-G))"
by (subst Proj_orthog_ccspan_union [symmetric])
(use that in ‹auto intro!: is_ortho_setD[OF B(1)]›)
also have "G ∪ B = B"
using that by blast
finally show ?thesis
using B(2) by (simp flip: cblinfun.add_left)
qed
have n1: ‹norm (f F (B-G)) ≤ norm a * d› for F
proof -
have ‹norm (f F (B-G)) ≤ norm a * norm (Proj (ccspan (B-G)) b)›
by (auto intro!: mult_right_mono is_Proj_reduces_norm simp add: f_def norm_butterfly)
also have ‹… ≤ norm a * norm (Proj (ccspan G) b - b)›
by (metis add_diff_cancel_left' b_split less_eq_real_def norm_minus_commute)
also have ‹… ≤ norm a * d›
by (meson less_eq_real_def mult_left_mono norm_ge_zero that(2))
finally show ?thesis
by -
qed
have n2: ‹norm (f (A-F) G) ≤ norm b * d› for G
proof -
have ‹norm (f (A-F) G) ≤ norm b * norm (Proj (ccspan (A-F)) a)›
by (auto intro!: mult_right_mono is_Proj_reduces_norm simp add: f_def norm_butterfly mult.commute)
also have ‹… ≤ norm b * norm (Proj (ccspan F) a - a)›
by (smt (verit, best) a_split add_diff_cancel_left' minus_diff_eq norm_minus_cancel)
also have ‹… ≤ norm b * d›
by (meson less_eq_real_def mult_left_mono norm_ge_zero that(1))
finally show ?thesis
by -
qed
have ‹norm (f F G - x) = norm (- f F (B-G) - f (A-F) (B-G) - f (A-F) G)›
unfolding xab
by (subst a_split, subst b_split)
(simp add: f_def butterfly_add_right butterfly_add_left)
also have ‹… ≤ norm (f F (B-G)) + norm (f (A-F) (B-G)) + norm (f (A-F) G)›
by (smt (verit, best) norm_minus_cancel norm_triangle_ineq4)
also have ‹… ≤ norm a * d + norm a * d + norm b * d›
using n1 n2
by (meson add_mono_thms_linordered_semiring(1))
also have ‹… < e›
by (fact d)
finally show ?thesis
by -
qed
have "∀⇩F (F, G) in finite_subsets_at_top A ×⇩F finite_subsets_at_top B.
(finite F ∧ F ⊆ A) ∧ finite G ∧ G ⊆ B"
unfolding case_prod_unfold by (intro eventually_prodI) auto
thus ‹∀⇩F FG in finite_subsets_at_top A ×⇩F finite_subsets_at_top B.
norm ((case FG of (F, G) ⇒ f F G) - x) < e›
using FG_close by eventually_elim (use fFG_dist in auto)
qed
have nontriv: ‹finite_subsets_at_top A ×⇩F finite_subsets_at_top B ≠ ⊥›
by (simp add: prod_filter_eq_bot)
have inside: ‹∀⇩F x in finite_subsets_at_top A ×⇩F finite_subsets_at_top B.
case_prod f x ∈ cspan ((λ(ξ,η). butterfly ξ η) ` (A × B))›
proof (rule eventually_mp[where P=‹λ(F,G). finite F ∧ finite G›])
show ‹∀⇩F (F,G) in finite_subsets_at_top A ×⇩F finite_subsets_at_top B. finite F ∧ finite G›
by (smt (verit) case_prod_conv eventually_finite_subsets_at_top_weakI eventually_prod_filter)
have f_in_span: ‹f F G ∈ cspan ((λ(ξ,η). butterfly ξ η) ` (A × B))› if [simp]: ‹finite F› ‹finite G› and ‹F ⊆ A› ‹G ⊆ B› for F G
proof -
have ‹Proj (ccspan F) a ∈ cspan F›
by (metis Proj_range cblinfun_apply_in_image ccspan_finite that(1))
then obtain r where ProjFsum: ‹Proj (ccspan F) a = (∑x∈F. r x *⇩C x)›
using complex_vector.span_finite[OF ‹finite F›] by auto
have ‹Proj (ccspan G) b ∈ cspan G›
by (metis Proj_range cblinfun_apply_in_image ccspan_finite that(2))
then obtain s where ProjGsum: ‹Proj (ccspan G) b = (∑x∈G. s x *⇩C x)›
using complex_vector.span_finite[OF ‹finite G›] by auto
have ‹butterfly ξ η ∈ (λ(ξ, η). butterfly ξ η) ` (A × B)›
if ‹η ∈ G› and ‹ξ ∈ F› for η ξ
using ‹F ⊆ A› ‹G ⊆ B› that by auto
then show ?thesis
by (auto intro!: complex_vector.span_sum complex_vector.span_scale
complex_vector.span_base[where a=‹butterfly _ _›]
simp add: f_def ProjFsum ProjGsum butterfly_sum_left butterfly_sum_right)
qed
have "∀⇩F (F, G) in finite_subsets_at_top A ×⇩F finite_subsets_at_top B.
(finite F ∧ F ⊆ A) ∧ finite G ∧ G ⊆ B"
unfolding case_prod_unfold by (intro eventually_prodI) auto
thus ‹∀⇩F x in finite_subsets_at_top A ×⇩F finite_subsets_at_top B.
(case x of (F, G) ⇒ finite F ∧ finite G) ⟶ (case x of (F, G) ⇒ f F G) ∈ cspan ((λ(ξ, η). butterfly ξ η) ` (A × B))›
by eventually_elim (auto intro!: f_in_span)
qed
show ‹x ∈ closure (cspan ((λ(ξ, η). butterfly ξ η) ` (A × B)))›
using lim nontriv inside by (rule limit_in_closure)
qed
also have ‹… = closure (cspan ((λ(ξ,η). butterfly ξ η) ` (A × B)))›
by (simp add: complex_vector.span_eq_iff[THEN iffD2])
finally show ?thesis
by -
qed
qed
lemma compact_op_comp_left: ‹compact_op (a o⇩C⇩L b)› if ‹compact_op a›
for a b :: ‹_::chilbert_space ⇒⇩C⇩L _::chilbert_space›
proof -
from that have ‹a ∈ closure (Collect finite_rank)›
using compact_op_finite_rank by blast
then have ‹a o⇩C⇩L b ∈ (λa. a o⇩C⇩L b) ` closure (Collect finite_rank)›
by blast
also have ‹… ⊆ closure ((λa. a o⇩C⇩L b) ` Collect finite_rank)›
by (auto intro!: closure_bounded_linear_image_subset bounded_clinear.bounded_linear bounded_clinear_cblinfun_compose_left)
also have ‹… ⊆ closure (Collect finite_rank)›
by (auto intro!: closure_mono finite_rank_comp_left)
finally show ‹compact_op (a o⇩C⇩L b)›
using compact_op_finite_rank by blast
qed
lemma compact_op_eigenspace_finite_dim:
fixes a :: ‹'a ⇒⇩C⇩L 'a::chilbert_space›
assumes ‹compact_op a›
assumes ‹e ≠ 0›
shows ‹finite_dim_ccsubspace (eigenspace e a)›
proof -
define S where ‹S = space_as_set (eigenspace e a)›
obtain B where ‹ccspan B = eigenspace e a› and ‹is_ortho_set B›
and norm_B: ‹x ∈ B ⟹ norm x = 1› for x
using orthonormal_subspace_basis_exists[where S=‹{}› and V=‹eigenspace e a›]
by (auto simp: S_def)
then have span_BS: ‹closure (cspan B) = S›
by (metis S_def ccspan.rep_eq)
have ‹finite B›
proof (rule ccontr)
assume ‹infinite B›
then obtain b :: ‹nat ⇒ 'a› where range_b: ‹range b ⊆ B› and ‹inj b›
by (meson infinite_countable_subset)
define f where ‹f n = a (b n)› for n
have range_f: ‹range f ⊆ closure (a ` cball 0 1)›
using norm_B range_b
by (auto intro!: closure_subset[THEN subsetD] imageI simp: f_def)
from ‹compact_op a› have compact: ‹compact (closure (a ` cball 0 1))›
using compact_op_def2 by blast
obtain l r where ‹strict_mono r› and fr_lim: ‹(f o r) ⇢ l›
using range_f compact[unfolded compact_def, rule_format, of f]
by fast
define d :: real where ‹d = cmod e * sqrt 2›
from ‹e ≠ 0› have ‹d > 0›
by (auto intro!: mult_pos_pos simp: d_def)
have aux: ‹∃n≥N. P n› if ‹P (Suc N)› for P N
using Suc_n_not_le_n nat_le_linear that by blast
have ‹dist (f (r n)) (f (r (Suc n))) = d› for n
proof -
have ortho: ‹is_orthogonal (b (r n)) (b (r (Suc n)))›
proof -
have ‹b (r n) ≠ b (r (Suc n))›
by (metis Suc_n_not_n ‹inj b› ‹strict_mono r› injD strict_mono_eq)
moreover from range_b have ‹b (r n) ∈ B› and ‹b (r (Suc n)) ∈ B›
by fast+
ultimately show ?thesis
using ‹is_ortho_set B›
by (auto intro!: simp: is_ortho_set_def)
qed
have normb: ‹norm (b n) = 1› for n
by (metis ‹inj b› image_subset_iff inj_image_mem_iff norm_B range_b range_eqI)
have ‹f (r n) = e *⇩C b (r n)› for n
proof -
from range_b span_BS
have ‹b (r n) ∈ S›
using complex_vector.span_superset closure_subset
by (blast dest: range_subsetD[where i = ‹b n›])
then show ?thesis
by (auto intro!: dest!: eigenspace_memberD simp: S_def f_def)
qed
then have ‹(dist (f (r n)) (f (r (Suc n))))⇧2 = (cmod e * dist (b (r n)) (b (r (Suc n))))⇧2›
by (simp add: dist_norm flip: scaleC_diff_right)
also from ortho have ‹… = (cmod e * sqrt 2)⇧2›
by (simp add: dist_norm polar_identity_minus power_mult_distrib normb)
finally show ?thesis
by (simp add: d_def)
qed
with ‹d > 0› have ‹¬ Cauchy (f o r)›
by (auto intro!: exI[of _ ‹d/2›] aux
simp: Cauchy_altdef2 dist_commute simp del: less_divide_eq_numeral1)
with fr_lim show False
using LIMSEQ_imp_Cauchy by blast
qed
with span_BS show ?thesis
using S_def cspan_finite_dim finite_dim_ccsubspace.rep_eq by fastforce
qed
lemma eigenvalue_in_the_limit_compact_op:
assumes ‹compact_op T›
assumes ‹l ≠ 0›
assumes normh: ‹⋀n. norm (h n) = 1›
assumes Tl_lim: ‹(λn. (T - l *⇩C id_cblinfun) (h n)) ⇢ 0›
shows ‹l ∈ eigenvalues T›
proof -
from assms(1)
have compact_Tball: ‹compact (closure (T ` cball 0 1))›
using compact_op_def2 by blast
have ‹T (h n) ∈ closure (T ` cball 0 1)› for n
by (smt (z3) assms(3) closure_subset image_subset_iff mem_cball_0)
then obtain n f where lim_Thn: ‹(λk. T (h (n k))) ⇢ f› and ‹strict_mono n›
using compact_Tball[unfolded compact_def, rule_format, where f=‹T o h›, unfolded o_def]
by fast
have lThk_lim: ‹(λk. (l *⇩C id_cblinfun - T) (h (n k))) ⇢ 0›
proof -
have ‹(λn. (l *⇩C id_cblinfun - T) (h n)) ⇢ 0›
using Tl_lim[THEN tendsto_minus]
by (simp add: cblinfun.diff_left)
with ‹strict_mono n› show ?thesis
by (rule LIMSEQ_subseq_LIMSEQ[unfolded o_def, rotated])
qed
have ‹h (n k) = inverse l *⇩C ((l *⇩C id_cblinfun - T) (h (n k)) + T (h (n k)))› for k
by (metis assms(2) cblinfun.real.add_left cblinfun.scaleC_left diff_add_cancel divideC_field_splits_simps_1(5) id_cblinfun.rep_eq scaleC_zero_right)
moreover have ‹… ⇢ inverse l *⇩C (0 + f)›
by (intro tendsto_intros lThk_lim lim_Thn)
ultimately have lim_hn: ‹(λk. h (n k)) ⇢ inverse l *⇩C f›
by simp
have ‹f ≠ 0›
proof -
from lim_hn have ‹(λk. norm (h (n k))) ⇢ norm (inverse l *⇩C f)›
by (rule isCont_tendsto_compose[unfolded o_def, rotated]) fastforce
moreover have ‹(λ_. 1) ⇢ 1›
by simp
ultimately have ‹norm (inverse l *⇩C f) = 1›
unfolding normh
using LIMSEQ_unique by blast
then show ‹f ≠ 0›
by force
qed
from lim_hn have ‹(λk. T (h (n k))) ⇢ T (inverse l *⇩C f)›
by (rule isCont_tendsto_compose[rotated]) force
with lim_Thn have ‹f = T (inverse l *⇩C f)›
using LIMSEQ_unique by blast
with ‹l ≠ 0› have ‹l *⇩C f = T f›
by (metis cblinfun.scaleC_right divideC_field_simps(2))
with ‹f ≠ 0› show ‹l ∈ eigenvalues T›
by (auto intro!: eigenvaluesI[where h=f])
qed
lemma norm_is_eigenvalue:
fixes a :: ‹'a ⇒⇩C⇩L 'a::{not_singleton, chilbert_space}›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹norm a ∈ eigenvalues a ∨ - norm a ∈ eigenvalues a›
proof -
wlog ‹a ≠ 0›
using negation by auto
obtain h e where h_lim: ‹(λi. h i ∙⇩C a (h i)) ⇢ e› and normh: ‹norm (h i) = 1›
and norme: ‹cmod e = norm a› for i
proof atomize_elim
have sgn_cmod: ‹sgn x * cmod x = x› for x
by (simp add: complex_of_real_cmod sgn_mult_abs)
from cblinfun_norm_is_Sup_cinner[OF ‹selfadjoint a›]
obtain f where range_f: ‹range f ⊆ ((λψ. cmod (ψ ∙⇩C (a *⇩V ψ))) ` {ψ. norm ψ = 1})›
and f_lim: ‹f ⇢ norm a›
by (atomize_elim, rule is_Sup_imp_ex_tendsto) (auto simp: ex_norm1_not_singleton)
obtain h0 where normh0: ‹norm (h0 i) = 1› and f_h0: ‹f i = cmod (h0 i ∙⇩C a (h0 i))› for i
by (atomize_elim, rule choice2) (use range_f in auto)
from f_h0 f_lim have h0lim_cmod: ‹(λi. cmod (h0 i ∙⇩C a (h0 i))) ⇢ norm a›
by presburger
have sgn_sphere: ‹sgn (h0 i ∙⇩C a (h0 i)) ∈ insert 0 (sphere 0 1)› for i
using normh0 by (auto intro!: left_inverse simp: sgn_div_norm)
have compact: ‹compact (insert 0 (sphere (0::complex) 1))›
by simp
obtain r l where ‹strict_mono r› and l_sphere: ‹l ∈ insert 0 (sphere 0 1)›
and h0lim_sgn: ‹((λi. sgn (h0 i ∙⇩C a (h0 i))) ∘ r) ⇢ l›
using compact[unfolded compact_def, rule_format, OF sgn_sphere]
by fast
define h and e where ‹h i = h0 (r i)› and ‹e = l * norm a› for i
have hlim_cmod: ‹(λi. cmod (h i ∙⇩C a (h i))) ⇢ norm a›
using LIMSEQ_subseq_LIMSEQ[OF h0lim_cmod ‹strict_mono r›]
unfolding h_def o_def by auto
with h0lim_sgn have ‹(λi. sgn (h i ∙⇩C a (h i)) * cmod (h i ∙⇩C a (h i))) ⇢ e›
by (auto intro!: tendsto_mult tendsto_of_real simp: o_def h_def e_def)
then have hlim: ‹(λi. h i ∙⇩C a (h i)) ⇢ e›
by (simp add: sgn_cmod)
have ‹e ≠ 0›
proof (rule ccontr, unfold not_not)
assume ‹e = 0›
from hlim have ‹(λi. cmod (h i ∙⇩C a (h i))) ⇢ cmod e›
by (rule tendsto_compose[where g=cmod, rotated])
(smt (verit, del_insts) ‹e = 0› diff_zero dist_norm metric_LIM_imp_LIM
norm_ge_zero norm_zero real_norm_def tendsto_ident_at)
with ‹e = 0› hlim_cmod have ‹norm a = 0›
using LIMSEQ_unique by fastforce
with ‹a ≠ 0› show False
by simp
qed
then have norme: ‹norm e = norm a›
using l_sphere by (simp add: e_def norm_mult)
show ‹∃h e. (λi. h i ∙⇩C (a *⇩V h i)) ⇢ e ∧ (∀i. norm (h i) = 1) ∧ cmod e = norm a›
using norme normh0 hlim
by (auto intro!: exI[of _ h] exI[of _ e] simp: h_def)
qed
have ‹e ∈ ℝ›
proof -
from h_lim[THEN tendsto_Im]
have *: ‹(λi. Im (h i ∙⇩C a (h i))) ⇢ Im e›
by -
have **: ‹Im (h i ∙⇩C a (h i)) = 0› for i
using assms(2) selfadjoint_def cinner_selfadjoint_real complex_is_Real_iff by auto
have ‹Im e = 0›
using _ * by (rule tendsto_unique) (use ** in auto)
then show ?thesis
using complex_is_Real_iff by presburger
qed
define e' where ‹e' = Re e›
with ‹e ∈ ℝ› have ee': ‹e = of_real e'›
by simp
have ‹e' ∈ eigenvalues a›
proof -
have [trans]: ‹f ⇢ 0› if ‹⋀x. f x ≤ g x› and ‹g ⇢ 0› and ‹⋀x. f x ≥ 0› for f g :: ‹nat ⇒ real›
by (rule real_tendsto_sandwich[where h=g and f=‹λ_. 0›]) (use that in auto)
have [simp]: "a* = a"
using assms(2) by (simp add: selfadjoint_def)
have [simp]: "Re (h x ∙⇩C h x) = 1" for x
using normh[of x] by (simp flip: power2_norm_eq_cinner')
have ‹(norm ((a - e' *⇩R id_cblinfun) (h n)))⇧2 = (norm (a (h n)))⇧2 - 2 * e' * Re (h n ∙⇩C a (h n)) + e'⇧2› for n
by (simp add: power2_norm_eq_cinner' algebra_simps cblinfun.cbilinear_simps
cblinfun.scaleR_left power2_eq_square[of e'] flip: cinner_adj_right)
also have ‹…n ≤ e'⇧2 - 2 * e' * Re (h n ∙⇩C a (h n)) + e'⇧2› for n
proof -
from norme have ‹e'⇧2 = (norm a)⇧2›
by (auto simp: ee' power2_eq_iff abs_if split: if_splits)
then have ‹(norm (a *⇩V h n))⇧2 ≤ e'⇧2›
using norm_cblinfun[of a "h n"] by (simp add: normh)
then show ?thesis
by auto
qed
also have ‹… ⇢ 0›
apply (subst asm_rl[of ‹(λn. e'⇧2 - 2 * e' * Re (h n ∙⇩C a (h n)) + e'⇧2) = (λn. 2 * e' * (e' - Re (h n ∙⇩C (a *⇩V h n))))›])
subgoal
by (auto simp: fun_eq_iff right_diff_distrib power2_eq_square)[1]
subgoal
using h_lim[THEN tendsto_Re]
by (auto intro!: tendsto_mult_right_zero tendsto_diff_const_left_rewrite simp: ee')
done
finally have ‹(λn. (a - e' *⇩R id_cblinfun) (h n)) ⇢ 0›
by (simp add: tendsto_norm_zero_iff)
then show ‹e' ∈ eigenvalues a›
unfolding scaleR_scaleC
by (rule eigenvalue_in_the_limit_compact_op[rotated -1])
(use ‹a ≠ 0› norme in ‹auto intro!: normh simp: assms ee'›)
qed
from ‹e ∈ ℝ› norme
have ‹e = norm a ∨ e = - norm a›
by (smt (verit, best) in_Reals_norm of_real_Re)
with ‹e' ∈ eigenvalues a› show ?thesis
using ee' by presburger
qed
lemma
fixes a :: ‹'a ⇒⇩C⇩L 'a::{not_singleton, chilbert_space}›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows largest_eigenvalue_norm_aux: ‹largest_eigenvalue a ∈ {norm a, - norm a}›
and largest_eigenvalue_ex: ‹largest_eigenvalue a ∈ eigenvalues a›
proof -
define l where ‹l = (SOME x. x ∈ eigenvalues a ∧ (∀y ∈ eigenvalues a. cmod x ≥ cmod y))›
from norm_is_eigenvalue[OF assms]
obtain e where ‹e ∈ {of_real (norm a), - of_real (norm a)}› and ‹e ∈ eigenvalues a›
by auto
then have norme: ‹norm e = norm a›
by auto
have ‹e ∈ eigenvalues a ∧ (∀y∈eigenvalues a. cmod y ≤ cmod e)› (is ‹?P e›)
by (auto intro!: ‹e ∈ eigenvalues a› simp: eigenvalue_norm_bound norme)
then have *: ‹l ∈ eigenvalues a ∧ (∀y∈eigenvalues a. cmod y ≤ cmod l)›
unfolding l_def largest_eigenvalue_def by (rule someI)
then have l_def': ‹l = largest_eigenvalue a›
by (metis (mono_tags, lifting) l_def largest_eigenvalue_def)
from * have ‹l ∈ eigenvalues a›
by (simp add: l_def)
then show ‹largest_eigenvalue a ∈ eigenvalues a›
by (simp add: l_def')
have ‹norm l ≥ norm a›
using * norme ‹e ∈ eigenvalues a› by auto
moreover have ‹norm l ≤ norm a›
using "*" eigenvalue_norm_bound by blast
ultimately have ‹norm l = norm a›
by linarith
moreover have ‹l ∈ ℝ›
using ‹l ∈ eigenvalues a› assms(2) eigenvalue_selfadj_real by blast
ultimately have ‹l ∈ {norm a, - norm a}›
by (smt (verit, ccfv_SIG) in_Reals_norm insertCI l_def of_real_Re)
then show ‹largest_eigenvalue a ∈ {norm a, - norm a}›
by (simp add: l_def')
qed
lemma largest_eigenvalue_norm:
fixes a :: ‹'a ⇒⇩C⇩L 'a::chilbert_space›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹largest_eigenvalue a ∈ {norm a, - norm a}›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
using chilbert_space_class.chilbert_space_axioms True assms
by (rule largest_eigenvalue_norm_aux[internalize_sort' 'a])
next
case False
then have ‹a = 0›
by (rule not_not_singleton_cblinfun_zero)
then show ?thesis
by simp
qed
hide_fact largest_eigenvalue_norm_aux
lemma cmod_largest_eigenvalue:
fixes a :: ‹'a ⇒⇩C⇩L 'a::chilbert_space›
assumes ‹compact_op a›
assumes ‹selfadjoint a›
shows ‹cmod (largest_eigenvalue a) = norm a›
using largest_eigenvalue_norm[OF assms] by auto
lemma compact_op_comp_right: ‹compact_op (a o⇩C⇩L b)› if ‹compact_op b›
for a b :: ‹_::chilbert_space ⇒⇩C⇩L _::chilbert_space›
proof -
from that have ‹b ∈ closure (Collect finite_rank)›
using compact_op_finite_rank by blast
then have ‹a o⇩C⇩L b ∈ cblinfun_compose a ` closure (Collect finite_rank)›
by blast
also have ‹… ⊆ closure (cblinfun_compose a ` Collect finite_rank)›
by (auto intro!: closure_bounded_linear_image_subset bounded_clinear.bounded_linear bounded_clinear_cblinfun_compose_right)
also have ‹… ⊆ closure (Collect finite_rank)›
by (auto intro!: closure_mono finite_rank_comp_right)
finally show ‹compact_op (a o⇩C⇩L b)›
using compact_op_finite_rank by blast
qed
unbundle no cblinfun_syntax
end