Theory Trace_Class
section ‹‹Trace_Class› -- Trace-class operators›
theory Trace_Class
imports Complex_Bounded_Operators.Complex_L2 HS2Ell2
Weak_Operator_Topology Positive_Operators Compact_Operators
Spectral_Theorem
begin
hide_fact (open) Infinite_Set_Sum.abs_summable_on_Sigma_iff
hide_fact (open) Infinite_Set_Sum.abs_summable_on_comparison_test
hide_const (open) Determinants.trace
hide_fact (open) Determinants.trace_def
unbundle cblinfun_syntax
subsection ‹Auxiliary lemmas›
lemma
fixes h :: ‹'a::{chilbert_space}›
assumes ‹is_onb E›
shows parseval_abs_summable: ‹(λe. (cmod (e ∙⇩C h))⇧2) abs_summable_on E›
proof (cases ‹h = 0›)
case True
then show ?thesis by simp
next
case False
then have ‹(∑⇩∞e∈E. (cmod (e ∙⇩C h))⇧2) ≠ 0›
using assms by (simp add: parseval_identity is_onb_def)
then show ?thesis
using infsum_not_exists by auto
qed
lemma basis_image_square_has_sum1:
fixes E :: ‹'a::complex_inner set› and F :: ‹'b::chilbert_space set›
assumes ‹is_onb E› and ‹is_onb F›
shows ‹((λe. (norm (A *⇩V e))⇧2) has_sum t) E ⟷ ((λ(e,f). (cmod (f ∙⇩C (A *⇩V e)))⇧2) has_sum t) (E×F)›
proof (rule iffI)
assume asm: ‹((λe. (norm (A *⇩V e))⇧2) has_sum t) E›
have sum1: ‹t = (∑⇩∞e∈E. (norm (A *⇩V e))⇧2)›
using asm infsumI by blast
have abs1: ‹(λe. (norm (A *⇩V e))⇧2) abs_summable_on E›
using asm summable_on_def by auto
have sum2: ‹t = (∑⇩∞e∈E. ∑⇩∞f∈F. (cmod (f ∙⇩C (A *⇩V e)))⇧2)›
apply (subst sum1)
apply (rule infsum_cong)
using assms(2)
by (simp add: is_onb_def flip: parseval_identity)
have abs2: ‹(λe. ∑⇩∞f∈F. (cmod (f ∙⇩C (A *⇩V e)))⇧2) abs_summable_on E›
using _ abs1 apply (rule summable_on_cong[THEN iffD2])
apply (subst parseval_identity)
using assms(2) by (auto simp: is_onb_def)
have abs3: ‹(λ(x, y). (cmod (y ∙⇩C (A *⇩V x)))⇧2) abs_summable_on E × F›
thm abs_summable_on_Sigma_iff
apply (rule abs_summable_on_Sigma_iff[THEN iffD2], rule conjI)
using abs2 apply (auto simp del: real_norm_def)
using assms(2) parseval_abs_summable apply blast
by auto
have sum3: ‹t = (∑⇩∞(e,f)∈E×F. (cmod (f ∙⇩C (A *⇩V e)))⇧2)›
apply (subst sum2)
apply (subst infsum_Sigma'_banach[symmetric])
using abs3 abs_summable_summable apply blast
by auto
then show ‹((λ(e,f). (cmod (f ∙⇩C (A *⇩V e)))⇧2) has_sum t) (E×F)›
using abs3 abs_summable_summable has_sum_infsum by blast
next
assume asm: ‹((λ(e,f). (cmod (f ∙⇩C (A *⇩V e)))⇧2) has_sum t) (E×F)›
have abs3: ‹(λ(x, y). (cmod (y ∙⇩C (A *⇩V x)))⇧2) abs_summable_on E × F›
using asm summable_on_def summable_on_iff_abs_summable_on_real
by blast
have sum3: ‹t = (∑⇩∞(e,f)∈E×F. (cmod (f ∙⇩C (A *⇩V e)))⇧2)›
using asm infsumI by blast
have sum2: ‹t = (∑⇩∞e∈E. ∑⇩∞f∈F. (cmod (f ∙⇩C (A *⇩V e)))⇧2)›
by (metis (mono_tags, lifting) asm infsum_Sigma'_banach infsum_cong sum3 summable_iff_has_sum_infsum)
have abs2: ‹(λe. ∑⇩∞f∈F. (cmod (f ∙⇩C (A *⇩V e)))⇧2) abs_summable_on E›
by (smt (verit, del_insts) abs3 summable_on_Sigma_banach summable_on_cong summable_on_iff_abs_summable_on_real)
have sum1: ‹t = (∑⇩∞e∈E. (norm (A *⇩V e))⇧2)›
apply (subst sum2)
apply (rule infsum_cong)
using assms
by (auto intro!: simp: parseval_identity is_onb_def)
have abs1: ‹(λe. (norm (A *⇩V e))⇧2) abs_summable_on E›
using assms abs2
by (auto intro!: simp: parseval_identity is_onb_def)
show ‹((λe. (norm (A *⇩V e))⇧2) has_sum t) E›
using abs1 sum1 by auto
qed
lemma basis_image_square_has_sum2:
fixes E :: ‹'a::chilbert_space set› and F :: ‹'b::chilbert_space set›
assumes ‹is_onb E› and ‹is_onb F›
shows ‹((λe. (norm (A *⇩V e))⇧2) has_sum t) E ⟷ ((λf. (norm (A* *⇩V f))⇧2) has_sum t) F›
proof -
have ‹((λe. (norm (A *⇩V e))⇧2) has_sum t) E ⟷ ((λ(e,f). (cmod (f ∙⇩C (A *⇩V e)))⇧2) has_sum t) (E×F)›
using basis_image_square_has_sum1 assms by blast
also have ‹… ⟷ ((λ(e,f). (cmod ((A* *⇩V f) ∙⇩C e))⇧2) has_sum t) (E×F)›
apply (subst cinner_adj_left)
by (rule refl)
also have ‹… ⟷ ((λ(f,e). (cmod ((A* *⇩V f) ∙⇩C e))⇧2) has_sum t) (F×E)›
apply (subst asm_rl[of ‹F×E = prod.swap ` (E×F)›])
apply force
apply (subst has_sum_reindex)
by (auto simp: o_def)
also have ‹… ⟷ ((λf. (norm (A* *⇩V f))⇧2) has_sum t) F›
apply (subst cinner_commute, subst complex_mod_cnj)
using basis_image_square_has_sum1 assms
by blast
finally show ?thesis
by -
qed
subsection ‹Trace-norm and trace-class›
lemma trace_norm_basis_invariance:
assumes ‹is_onb E› and ‹is_onb F›
shows ‹((λe. cmod (e ∙⇩C (abs_op A *⇩V e))) has_sum t) E ⟷ ((λf. cmod (f ∙⇩C (abs_op A *⇩V f))) has_sum t) F›
proof -
define B where ‹B = sqrt_op (abs_op A)›
have ‹complex_of_real (cmod (e ∙⇩C (abs_op A *⇩V e))) = (B* *⇩V B*⇩V e) ∙⇩C e› for e
apply (simp add: B_def positive_selfadjointI[unfolded selfadjoint_def] flip: cblinfun_apply_cblinfun_compose)
by (metis abs_op_pos abs_pos cinner_commute cinner_pos_if_pos complex_cnj_complex_of_real complex_of_real_cmod)
also have ‹… e = complex_of_real ((norm (B *⇩V e))⇧2)› for e
apply (subst cdot_square_norm[symmetric])
apply (subst cinner_adj_left[symmetric])
by (simp add: B_def)
finally have *: ‹cmod (e ∙⇩C (abs_op A *⇩V e)) = (norm (B *⇩V e))⇧2› for e
by (metis Re_complex_of_real)
have ‹((λe. cmod (e ∙⇩C (abs_op A *⇩V e))) has_sum t) E ⟷ ((λe. (norm (B *⇩V e))⇧2) has_sum t) E›
by (simp add: *)
also have ‹… = ((λf. (norm (B* *⇩V f))⇧2) has_sum t) F›
apply (subst basis_image_square_has_sum2[where F=F])
by (simp_all add: assms)
also have ‹… = ((λf. (norm (B *⇩V f))⇧2) has_sum t) F›
using basis_image_square_has_sum2 assms(2) by blast
also have ‹… = ((λe. cmod (e ∙⇩C (abs_op A *⇩V e))) has_sum t) F›
by (simp add: *)
finally show ?thesis
by simp
qed
definition trace_class :: ‹('a::chilbert_space ⇒⇩C⇩L 'b::complex_inner) ⇒ bool›
where ‹trace_class A ⟷ (∃E. is_onb E ∧ (λe. e ∙⇩C (abs_op A *⇩V e)) abs_summable_on E)›
lemma trace_classI:
assumes ‹is_onb E› and ‹(λe. e ∙⇩C (abs_op A *⇩V e)) abs_summable_on E›
shows ‹trace_class A›
using assms(1) assms(2) trace_class_def by blast
lemma trace_class_iff_summable:
assumes ‹is_onb E›
shows ‹trace_class A ⟷ (λe. e ∙⇩C (abs_op A *⇩V e)) abs_summable_on E›
apply (auto intro!: trace_classI assms simp: trace_class_def)
using assms summable_on_def trace_norm_basis_invariance by blast
lemma trace_class_0[simp]: ‹trace_class 0›
unfolding trace_class_def
by (auto intro!: exI[of _ some_chilbert_basis] simp: is_onb_def is_normal_some_chilbert_basis)
lemma trace_class_uminus: ‹trace_class t ⟹ trace_class (-t)›
by (auto simp add: trace_class_def)
lemma trace_class_uminus_iff[simp]: ‹trace_class (-a) = trace_class a›
by (auto simp add: trace_class_def)
definition trace_norm where ‹trace_norm A = (if trace_class A then (∑⇩∞e∈some_chilbert_basis. cmod (e ∙⇩C (abs_op A *⇩V e))) else 0)›
definition trace where ‹trace A = (if trace_class A then (∑⇩∞e∈some_chilbert_basis. e ∙⇩C (A *⇩V e)) else 0)›
lemma trace_0[simp]: ‹trace 0 = 0›
unfolding trace_def by simp
lemma trace_class_abs_op[simp]: ‹trace_class (abs_op A) = trace_class A›
unfolding trace_class_def
by simp
lemma trace_abs_op[simp]: ‹trace (abs_op A) = trace_norm A›
proof (cases ‹trace_class A›)
case True
have pos: ‹e ∙⇩C (abs_op A *⇩V e) ≥ 0› for e
by (simp add: cinner_pos_if_pos)
then have abs: ‹e ∙⇩C (abs_op A *⇩V e) = abs (e ∙⇩C (abs_op A *⇩V e))› for e
by (simp add: abs_pos)
have ‹trace (abs_op A) = (∑⇩∞e∈some_chilbert_basis. e ∙⇩C (abs_op A *⇩V e))›
by (simp add: trace_def True)
also have ‹… = (∑⇩∞e∈some_chilbert_basis. complex_of_real (cmod (e ∙⇩C (abs_op A *⇩V e))))›
using pos abs complex_of_real_cmod by presburger
also have ‹… = complex_of_real (∑⇩∞e∈some_chilbert_basis. cmod (e ∙⇩C (abs_op A *⇩V e)))›
by (simp add: infsum_of_real)
also have ‹… = trace_norm A›
by (simp add: trace_norm_def True)
finally show ?thesis
by -
next
case False
then show ?thesis
by (simp add: trace_def trace_norm_def)
qed
lemma trace_norm_pos: ‹trace_norm A = trace A› if ‹A ≥ 0›
by (metis abs_op_id_on_pos that trace_abs_op)
lemma trace_norm_alt_def:
assumes ‹is_onb B›
shows ‹trace_norm A = (if trace_class A then (∑⇩∞e∈B. cmod (e ∙⇩C (abs_op A *⇩V e))) else 0)›
by (metis (mono_tags, lifting) assms infsum_eqI' is_onb_some_chilbert_basis trace_norm_basis_invariance trace_norm_def)
lemma trace_class_finite_dim[simp]: ‹trace_class A› for A :: ‹'a::{cfinite_dim,chilbert_space} ⇒⇩C⇩L 'b::complex_inner›
apply (subst trace_class_iff_summable[of some_chilbert_basis])
by (auto intro!: summable_on_finite)
lemma trace_class_scaleC: ‹trace_class (c *⇩C a)› if ‹trace_class a›
proof -
from that obtain B where ‹is_onb B› and ‹(λx. x ∙⇩C (abs_op a *⇩V x)) abs_summable_on B›
by (auto simp: trace_class_def)
then show ?thesis
by (auto intro!: exI[of _ B] summable_on_cmult_right simp: trace_class_def ‹is_onb B› abs_op_scaleC norm_mult)
qed
lemma trace_scaleC: ‹trace (c *⇩C a) = c * trace a›
proof -
consider (trace_class) ‹trace_class a› | (c0) ‹c = 0› | (non_trace_class) ‹¬ trace_class a› ‹c ≠ 0›
by auto
then show ?thesis
proof cases
case trace_class
then have ‹trace_class (c *⇩C a)›
by (rule trace_class_scaleC)
then have ‹trace (c *⇩C a) = (∑⇩∞e∈some_chilbert_basis. e ∙⇩C (c *⇩C a *⇩V e))›
unfolding trace_def by simp
also have ‹… = c * (∑⇩∞e∈some_chilbert_basis. e ∙⇩C (a *⇩V e))›
by (auto simp: infsum_cmult_right')
also from trace_class have ‹… = c * trace a›
by (simp add: Trace_Class.trace_def)
finally show ?thesis
by -
next
case c0
then show ?thesis
by simp
next
case non_trace_class
then have ‹¬ trace_class (c *⇩C a)›
by (metis divideC_field_simps(2) trace_class_scaleC)
with non_trace_class show ?thesis
by (simp add: trace_def)
qed
qed
lemma trace_uminus: ‹trace (- a) = - trace a›
by (metis mult_minus1 scaleC_minus1_left trace_scaleC)
lemma trace_norm_0[simp]: ‹trace_norm 0 = 0›
by (auto simp: trace_norm_def)
lemma trace_norm_nneg[simp]: ‹trace_norm a ≥ 0›
apply (cases ‹trace_class a›)
by (auto simp: trace_norm_def infsum_nonneg)
lemma trace_norm_scaleC: ‹trace_norm (c *⇩C a) = norm c * trace_norm a›
proof -
consider (trace_class) ‹trace_class a› | (c0) ‹c = 0› | (non_trace_class) ‹¬ trace_class a› ‹c ≠ 0›
by auto
then show ?thesis
proof cases
case trace_class
then have ‹trace_class (c *⇩C a)›
by (rule trace_class_scaleC)
then have ‹trace_norm (c *⇩C a) = (∑⇩∞e∈some_chilbert_basis. norm (e ∙⇩C (abs_op (c *⇩C a) *⇩V e)))›
unfolding trace_norm_def by simp
also have ‹… = norm c * (∑⇩∞e∈some_chilbert_basis. norm (e ∙⇩C (abs_op a *⇩V e)))›
by (auto simp: infsum_cmult_right' abs_op_scaleC norm_mult)
also from trace_class have ‹… = norm c * trace_norm a›
by (simp add: trace_norm_def)
finally show ?thesis
by -
next
case c0
then show ?thesis
by simp
next
case non_trace_class
then have ‹¬ trace_class (c *⇩C a)›
by (metis divideC_field_simps(2) trace_class_scaleC)
with non_trace_class show ?thesis
by (simp add: trace_norm_def)
qed
qed
lemma trace_norm_nondegenerate: ‹a = 0› if ‹trace_class a› and ‹trace_norm a = 0›
proof (rule ccontr)
assume ‹a ≠ 0›
then have ‹abs_op a ≠ 0›
using abs_op_nondegenerate by blast
then obtain x where xax: ‹x ∙⇩C (abs_op a *⇩V x) ≠ 0›
by (metis cblinfun.zero_left cblinfun_cinner_eqI cinner_zero_right)
then have ‹norm x ≠ 0›
by auto
then have xax': ‹sgn x ∙⇩C (abs_op a *⇩V sgn x) ≠ 0› and [simp]: ‹norm (sgn x) = 1›
unfolding sgn_div_norm using xax by (auto simp: cblinfun.scaleR_right)
obtain B where sgnx_B: ‹{sgn x} ⊆ B› and ‹is_onb B›
apply atomize_elim apply (rule orthonormal_basis_exists)
using ‹norm x ≠ 0› by (auto simp: is_ortho_set_def sgn_div_norm)
from ‹is_onb B› that
have summable: ‹(λe. e ∙⇩C (abs_op a *⇩V e)) abs_summable_on B›
using trace_class_iff_summable by fastforce
from that have ‹0 = trace_norm a›
by simp
also from ‹is_onb B› have ‹trace_norm a = (∑⇩∞e∈B. cmod (e ∙⇩C (abs_op a *⇩V e)))›
by (smt (verit, ccfv_SIG) abs_norm_cancel infsum_cong infsum_not_exists real_norm_def trace_class_def trace_norm_alt_def)
also have ‹… ≥ (∑⇩∞e∈{sgn x}. cmod (e ∙⇩C (abs_op a *⇩V e)))› (is ‹_ ≥ …›)
apply (rule infsum_mono2)
using summable sgnx_B by auto
also from xax' have ‹… > 0›
by (simp add: is_orthogonal_sym xax')
finally show False
by simp
qed
typedef (overloaded) ('a::chilbert_space, 'b::chilbert_space) trace_class = ‹Collect trace_class :: ('a ⇒⇩C⇩L 'b) set›
morphisms from_trace_class Abs_trace_class
by (auto intro!: exI[of _ 0])
setup_lifting type_definition_trace_class
lemma trace_class_from_trace_class[simp]: ‹trace_class (from_trace_class t)›
using from_trace_class by blast
lemma trace_pos: ‹trace a ≥ 0› if ‹a ≥ 0›
by (metis abs_op_def complex_of_real_nn_iff sqrt_op_unique that trace_abs_op trace_norm_nneg)
lemma trace_adj_prelim: ‹trace (a*) = cnj (trace a)› if ‹trace_class a› and ‹trace_class (a*)›
by (simp add: trace_def that flip: cinner_adj_right infsum_cnj)
subsection ‹Hilbert-Schmidt operators›
definition hilbert_schmidt where ‹hilbert_schmidt a ⟷ trace_class (a* o⇩C⇩L a)›
definition hilbert_schmidt_norm where ‹hilbert_schmidt_norm a = sqrt (trace_norm (a* o⇩C⇩L a))›
lemma hilbert_schmidtI: ‹hilbert_schmidt a› if ‹trace_class (a* o⇩C⇩L a)›
using that unfolding hilbert_schmidt_def by simp
lemma hilbert_schmidt_0[simp]: ‹hilbert_schmidt 0›
unfolding hilbert_schmidt_def by simp
lemma hilbert_schmidt_norm_pos[simp]: ‹hilbert_schmidt_norm a ≥ 0›
by (auto simp: hilbert_schmidt_norm_def)
lemma has_sum_hilbert_schmidt_norm_square:
assumes ‹is_onb B› and ‹hilbert_schmidt a›
shows ‹((λx. (norm (a *⇩V x))⇧2) has_sum (hilbert_schmidt_norm a)⇧2) B›
proof -
from ‹hilbert_schmidt a›
have ‹trace_class (a* o⇩C⇩L a)›
using hilbert_schmidt_def by blast
with ‹is_onb B› have ‹((λx. cmod (x ∙⇩C ((a* o⇩C⇩L a) *⇩V x))) has_sum trace_norm (a* o⇩C⇩L a)) B›
by (metis (no_types, lifting) abs_op_def has_sum_cong has_sum_infsum positive_cblinfun_squareI sqrt_op_unique trace_class_def trace_norm_alt_def trace_norm_basis_invariance)
then show ?thesis
by (auto simp: cinner_adj_right cdot_square_norm of_real_power norm_power hilbert_schmidt_norm_def)
qed
lemma summable_hilbert_schmidt_norm_square:
assumes ‹is_onb B› and ‹hilbert_schmidt a›
shows ‹(λx. (norm (a *⇩V x))⇧2) summable_on B›
using assms(1) assms(2) has_sum_hilbert_schmidt_norm_square summable_on_def by blast
lemma summable_hilbert_schmidt_norm_square_converse:
assumes ‹is_onb B›
assumes ‹(λx. (norm (a *⇩V x))⇧2) summable_on B›
shows ‹hilbert_schmidt a›
proof -
from assms(2)
have ‹(λx. cmod (x ∙⇩C ((a* o⇩C⇩L a) *⇩V x))) summable_on B›
by (metis (no_types, lifting) cblinfun_apply_cblinfun_compose cinner_adj_right cinner_pos_if_pos cmod_Re positive_cblinfun_squareI power2_norm_eq_cinner' summable_on_cong)
then have ‹trace_class (a* o⇩C⇩L a)›
by (metis (no_types, lifting) abs_op_def assms(1) positive_cblinfun_squareI sqrt_op_unique summable_on_cong trace_class_def)
then show ?thesis
using hilbert_schmidtI by blast
qed
lemma infsum_hilbert_schmidt_norm_square:
assumes ‹is_onb B› and ‹hilbert_schmidt a›
shows ‹(∑⇩∞x∈B. (norm (a *⇩V x))⇧2) = ((hilbert_schmidt_norm a)⇧2)›
using assms has_sum_hilbert_schmidt_norm_square infsumI by blast
lemma
assumes ‹hilbert_schmidt b›
shows hilbert_schmidt_comp_right: ‹hilbert_schmidt (a o⇩C⇩L b)›
and hilbert_schmidt_norm_comp_right: ‹hilbert_schmidt_norm (a o⇩C⇩L b) ≤ norm a * hilbert_schmidt_norm b›
proof -
define B :: ‹'a set› where ‹B = some_chilbert_basis›
have [simp]: ‹is_onb B›
by (simp add: B_def)
have leq: ‹(norm ((a o⇩C⇩L b) *⇩V x))⇧2 ≤ (norm a)⇧2 * (norm (b *⇩V x))⇧2› for x
by (metis cblinfun_apply_cblinfun_compose norm_cblinfun norm_ge_zero power_mono power_mult_distrib)
have ‹(λx. (norm (b *⇩V x))⇧2) summable_on B›
using ‹is_onb B› summable_hilbert_schmidt_norm_square assms by blast
then have sum2: ‹(λx. (norm a)⇧2 * (norm (b *⇩V x))⇧2) summable_on B›
using summable_on_cmult_right by blast
then have ‹(λx. ((norm a)⇧2 * (norm (b *⇩V x))⇧2)) abs_summable_on B›
by auto
then have ‹(λx. (norm ((a o⇩C⇩L b) *⇩V x))⇧2) abs_summable_on B›
apply (rule abs_summable_on_comparison_test)
using leq by force
then have sum5: ‹(λx. (norm ((a o⇩C⇩L b) *⇩V x))⇧2) summable_on B›
by auto
then show [simp]: ‹hilbert_schmidt (a o⇩C⇩L b)›
using ‹is_onb B›
by (rule summable_hilbert_schmidt_norm_square_converse[rotated])
have ‹(hilbert_schmidt_norm (a o⇩C⇩L b))⇧2 = (∑⇩∞x∈B. (norm ((a o⇩C⇩L b) *⇩V x))⇧2)›
apply (rule infsum_hilbert_schmidt_norm_square[symmetric])
by simp_all
also have ‹… ≤ (∑⇩∞x∈B. (norm a)⇧2 * (norm (b *⇩V x))⇧2)›
using sum5 sum2 leq by (rule infsum_mono)
also have ‹… = (norm a)⇧2 * (∑⇩∞x∈B. (norm (b *⇩V x))⇧2)›
by (simp add: infsum_cmult_right')
also have ‹… = (norm a)⇧2 * (hilbert_schmidt_norm b)⇧2›
by (simp add: assms infsum_hilbert_schmidt_norm_square)
finally show ‹hilbert_schmidt_norm (a o⇩C⇩L b) ≤ norm a * hilbert_schmidt_norm b›
apply (rule_tac power2_le_imp_le)
by (auto intro!: mult_nonneg_nonneg simp: power_mult_distrib)
qed
lemma hilbert_schmidt_adj[simp]:
assumes ‹hilbert_schmidt a›
shows ‹hilbert_schmidt (a*)›
proof -
from assms
have ‹(λe. (norm (a *⇩V e))⇧2) summable_on some_chilbert_basis›
using is_onb_some_chilbert_basis summable_hilbert_schmidt_norm_square by blast
then have ‹(λe. (norm (a* *⇩V e))⇧2) summable_on some_chilbert_basis›
by (metis basis_image_square_has_sum2 is_onb_some_chilbert_basis summable_on_def)
then show ?thesis
using is_onb_some_chilbert_basis summable_hilbert_schmidt_norm_square_converse by blast
qed
lemma hilbert_schmidt_norm_adj[simp]:
shows ‹hilbert_schmidt_norm (a*) = hilbert_schmidt_norm a›
proof (cases ‹hilbert_schmidt a›)
case True
then have ‹((λx. (norm (a *⇩V x))⇧2) has_sum (hilbert_schmidt_norm a)⇧2) some_chilbert_basis›
by (simp add: has_sum_hilbert_schmidt_norm_square)
then have 1: ‹((λx. (norm (a* *⇩V x))⇧2) has_sum (hilbert_schmidt_norm a)⇧2) some_chilbert_basis›
by (metis basis_image_square_has_sum2 is_onb_some_chilbert_basis)
from True
have ‹hilbert_schmidt (a*)›
by simp
then have 2: ‹((λx. (norm (a* *⇩V x))⇧2) has_sum (hilbert_schmidt_norm (a*))⇧2) some_chilbert_basis›
by (simp add: has_sum_hilbert_schmidt_norm_square)
from 1 2 show ?thesis
by (metis abs_of_nonneg hilbert_schmidt_norm_pos infsumI real_sqrt_abs)
next
case False
then have ‹¬ hilbert_schmidt (a*)›
using hilbert_schmidt_adj by fastforce
then show ?thesis
by (metis False hilbert_schmidt_def hilbert_schmidt_norm_def trace_norm_def)
qed
lemma
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space› and b
assumes ‹hilbert_schmidt a›
shows hilbert_schmidt_comp_left: ‹hilbert_schmidt (a o⇩C⇩L b)›
apply (subst asm_rl[of ‹a o⇩C⇩L b = (b* o⇩C⇩L a*)*›], simp)
by (auto intro!: assms hilbert_schmidt_comp_right hilbert_schmidt_adj simp del: adj_cblinfun_compose)
lemma
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space› and b
assumes ‹hilbert_schmidt a›
shows hilbert_schmidt_norm_comp_left: ‹hilbert_schmidt_norm (a o⇩C⇩L b) ≤ norm b * hilbert_schmidt_norm a›
apply (subst asm_rl[of ‹a o⇩C⇩L b = (b* o⇩C⇩L a*)*›], simp)
using hilbert_schmidt_norm_comp_right[of ‹a*› ‹b*›]
by (auto intro!: assms hilbert_schmidt_adj simp del: adj_cblinfun_compose)
lemma hilbert_schmidt_scaleC: ‹hilbert_schmidt (c *⇩C a)› if ‹hilbert_schmidt a›
using hilbert_schmidt_def that trace_class_scaleC by fastforce
lemma hilbert_schmidt_scaleR: ‹hilbert_schmidt (r *⇩R a)› if ‹hilbert_schmidt a›
by (simp add: hilbert_schmidt_scaleC scaleR_scaleC that)
lemma hilbert_schmidt_uminus: ‹hilbert_schmidt (- a)› if ‹hilbert_schmidt a›
by (metis hilbert_schmidt_scaleC scaleC_minus1_left that)
lemma hilbert_schmidt_plus: ‹hilbert_schmidt (t + u)› if ‹hilbert_schmidt t› and ‹hilbert_schmidt u›
for t u :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
define II :: ‹'a ⇒⇩C⇩L ('a×'a)› where ‹II = cblinfun_left + cblinfun_right›
define JJ :: ‹('b×'b) ⇒⇩C⇩L 'b› where ‹JJ = cblinfun_left* + cblinfun_right*›
define t2 u2 where ‹t2 = t* o⇩C⇩L t› and ‹u2 = u* o⇩C⇩L u›
define tu :: ‹('a×'a) ⇒⇩C⇩L ('b×'b)› where ‹tu = (cblinfun_left o⇩C⇩L t o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L u o⇩C⇩L cblinfun_right*)›
define tu2 :: ‹('a×'a) ⇒⇩C⇩L ('a×'a)› where ‹tu2 = (cblinfun_left o⇩C⇩L t2 o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L u2 o⇩C⇩L cblinfun_right*)›
have t_plus_u: ‹t + u = JJ o⇩C⇩L tu o⇩C⇩L II›
apply (simp add: II_def JJ_def tu_def cblinfun_compose_add_left cblinfun_compose_add_right cblinfun_compose_assoc)
by (simp flip: cblinfun_compose_assoc)
have tu_tu2: ‹tu* o⇩C⇩L tu = tu2›
by (simp add: tu_def tu2_def t2_def u2_def cblinfun_compose_add_left
cblinfun_compose_add_right cblinfun_compose_assoc adj_plus
isometryD[THEN simp_a_oCL_b] cblinfun_right_left_ortho[THEN simp_a_oCL_b]
cblinfun_left_right_ortho[THEN simp_a_oCL_b])
have ‹trace_class tu2›
proof (rule trace_classI)
define BL BR B :: ‹('a×'a) set› where ‹BL = some_chilbert_basis × {0}›
and ‹BR = {0} × some_chilbert_basis›
and ‹B = BL ∪ BR›
have ‹BL ∩ BR = {}›
using is_ortho_set_some_chilbert_basis
by (auto simp: BL_def BR_def is_ortho_set_def)
show ‹is_onb B›
by (simp add: BL_def BR_def B_def is_onb_prod)
have ‹tu2 ≥ 0›
by (auto intro!: positive_cblinfunI simp: t2_def u2_def cinner_adj_right tu2_def cblinfun.add_left cinner_pos_if_pos)
then have abs_tu2: ‹abs_op tu2 = tu2›
by (metis abs_opI)
have abs_t2: ‹abs_op t2 = t2›
by (metis abs_opI positive_cblinfun_squareI t2_def)
have abs_u2: ‹abs_op u2 = u2›
by (metis abs_opI positive_cblinfun_squareI u2_def)
from that(1)
have ‹(λx. x ∙⇩C (abs_op t2 *⇩V x)) abs_summable_on some_chilbert_basis›
by (simp add: hilbert_schmidt_def t2_def trace_class_iff_summable[OF is_onb_some_chilbert_basis])
then have ‹(λx. x ∙⇩C (t2 *⇩V x)) abs_summable_on some_chilbert_basis›
by (simp add: abs_t2)
then have sum_BL: ‹(λx. x ∙⇩C (tu2 *⇩V x)) abs_summable_on BL›
apply (subst asm_rl[of ‹BL = (λx. (x,0)) ` some_chilbert_basis›])
by (auto simp: BL_def summable_on_reindex inj_on_def o_def tu2_def cblinfun.add_left)
from that(2)
have ‹(λx. x ∙⇩C (abs_op u2 *⇩V x)) abs_summable_on some_chilbert_basis›
by (simp add: hilbert_schmidt_def u2_def trace_class_iff_summable[OF is_onb_some_chilbert_basis])
then have ‹(λx. x ∙⇩C (u2 *⇩V x)) abs_summable_on some_chilbert_basis›
by (simp add: abs_u2)
then have sum_BR: ‹(λx. x ∙⇩C (tu2 *⇩V x)) abs_summable_on BR›
apply (subst asm_rl[of ‹BR = (λx. (0,x)) ` some_chilbert_basis›])
by (auto simp: BR_def summable_on_reindex inj_on_def o_def tu2_def cblinfun.add_left)
from sum_BL sum_BR
show ‹(λx. x ∙⇩C (abs_op tu2 *⇩V x)) abs_summable_on B›
using ‹BL ∩ BR = {}›
by (auto intro!: summable_on_Un_disjoint simp: B_def abs_tu2)
qed
then have ‹hilbert_schmidt tu›
by (auto simp flip: tu_tu2 intro!: hilbert_schmidtI)
with t_plus_u
show ‹hilbert_schmidt (t + u)›
by (auto intro: hilbert_schmidt_comp_left hilbert_schmidt_comp_right)
qed
lemma hilbert_schmidt_minus: ‹hilbert_schmidt (a - b)› if ‹hilbert_schmidt a› and ‹hilbert_schmidt b›
for a b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
using hilbert_schmidt_plus hilbert_schmidt_uminus that(1) that(2) by fastforce
typedef (overloaded) ('a::chilbert_space,'b::complex_inner) hilbert_schmidt = ‹Collect hilbert_schmidt :: ('a ⇒⇩C⇩L 'b) set›
by (auto intro!: exI[of _ 0])
setup_lifting type_definition_hilbert_schmidt
instantiation hilbert_schmidt :: (chilbert_space, chilbert_space)
"{zero,scaleC,uminus,plus,minus,dist_norm,sgn_div_norm,uniformity_dist,open_uniformity}" begin
lift_definition zero_hilbert_schmidt :: ‹('a,'b) hilbert_schmidt› is 0 by auto
lift_definition norm_hilbert_schmidt :: ‹('a,'b) hilbert_schmidt ⇒ real› is hilbert_schmidt_norm .
lift_definition scaleC_hilbert_schmidt :: ‹complex ⇒ ('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt› is scaleC
by (simp add: hilbert_schmidt_scaleC)
lift_definition scaleR_hilbert_schmidt :: ‹real ⇒ ('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt› is scaleR
by (simp add: hilbert_schmidt_scaleR)
lift_definition uminus_hilbert_schmidt :: ‹('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt› is uminus
by (simp add: hilbert_schmidt_uminus)
lift_definition minus_hilbert_schmidt :: ‹('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt› is minus
by (simp add: hilbert_schmidt_minus)
lift_definition plus_hilbert_schmidt :: ‹('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt› is plus
by (simp add: hilbert_schmidt_plus)
definition ‹dist a b = norm (a - b)› for a b :: ‹('a,'b) hilbert_schmidt›
definition ‹sgn x = inverse (norm x) *⇩R x› for x :: ‹('a,'b) hilbert_schmidt›
definition ‹uniformity = (INF e∈{0<..}. principal {(x::('a,'b) hilbert_schmidt, y). dist x y < e})›
definition ‹open U = (∀x∈U. ∀⇩F (x', y) in INF e∈{0<..}. principal {(x, y). norm (x - y) < e}. x' = x ⟶ y ∈ U)› for U :: ‹('a,'b) hilbert_schmidt set›
instance
proof intro_classes
show ‹(*⇩R) r = ((*⇩C) (complex_of_real r) :: ('a,'b) hilbert_schmidt ⇒ _)› for r :: real
apply (rule ext)
apply transfer
by (auto simp: scaleR_scaleC)
show ‹dist x y = norm (x - y)› for x y :: ‹('a,'b) hilbert_schmidt›
by (simp add: dist_hilbert_schmidt_def)
show ‹sgn x = inverse (norm x) *⇩R x› for x :: ‹('a,'b) hilbert_schmidt›
by (simp add: Trace_Class.sgn_hilbert_schmidt_def)
show ‹uniformity = (INF e∈{0<..}. principal {(x::('a,'b) hilbert_schmidt, y). dist x y < e})›
using Trace_Class.uniformity_hilbert_schmidt_def by blast
show ‹open U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)› for U :: ‹('a,'b) hilbert_schmidt set›
by (simp add: uniformity_hilbert_schmidt_def open_hilbert_schmidt_def dist_hilbert_schmidt_def)
qed
end
lift_definition hs_compose :: ‹('b::chilbert_space,'c::complex_inner) hilbert_schmidt
⇒ ('a::chilbert_space,'b) hilbert_schmidt ⇒ ('a,'c) hilbert_schmidt› is
cblinfun_compose
by (simp add: hilbert_schmidt_comp_right)
lemma
fixes A :: ‹'a :: chilbert_space ⇒⇩C⇩L 'b :: chilbert_space›
shows trace_class_iff_sqrt_hs: ‹trace_class A ⟷ hilbert_schmidt (sqrt_op (abs_op A))› (is ?thesis1)
and trace_class_iff_hs_times_hs: ‹trace_class A ⟷ (∃B (C::'a⇒⇩C⇩L'a). hilbert_schmidt B ∧ hilbert_schmidt C ∧ A = B o⇩C⇩L C)› (is ?thesis2)
and trace_class_iff_abs_hs_times_hs: ‹trace_class A ⟷ (∃B (C::'a⇒⇩C⇩L'a). hilbert_schmidt B ∧ hilbert_schmidt C ∧ abs_op A = B o⇩C⇩L C)› (is ?thesis3)
proof -
define Sq W where ‹Sq = sqrt_op (abs_op A)› and ‹W = polar_decomposition A›
have trace_class_sqrt_hs: ‹hilbert_schmidt Sq› if ‹trace_class A›
proof (rule hilbert_schmidtI)
from that
have ‹trace_class (abs_op A)›
by simp
then show ‹trace_class (Sq* o⇩C⇩L Sq)›
by (auto simp: Sq_def positive_selfadjointI[unfolded selfadjoint_def])
qed
have sqrt_hs_hs_times_hs: ‹∃B (C :: 'a ⇒⇩C⇩L 'a). hilbert_schmidt B ∧ hilbert_schmidt C ∧ A = B o⇩C⇩L C›
if ‹hilbert_schmidt Sq›
proof -
have ‹A = W o⇩C⇩L abs_op A›
by (simp add: polar_decomposition_correct W_def)
also have ‹… = (W o⇩C⇩L Sq) o⇩C⇩L Sq›
by (metis Sq_def abs_op_pos cblinfun_compose_assoc positive_selfadjointI sqrt_op_pos sqrt_op_square)
finally have ‹A = (W o⇩C⇩L Sq) o⇩C⇩L Sq›
by -
then show ?thesis
apply (rule_tac exI[of _ ‹W o⇩C⇩L Sq›], rule_tac exI[of _ Sq])
using that by (auto simp add: hilbert_schmidt_comp_right)
qed
have hs_times_hs_abs_hs_times_hs: ‹∃B (C :: 'a ⇒⇩C⇩L 'a). hilbert_schmidt B ∧ hilbert_schmidt C ∧ abs_op A = B o⇩C⇩L C›
if ‹∃B (C :: 'a ⇒⇩C⇩L 'a). hilbert_schmidt B ∧ hilbert_schmidt C ∧ A = B o⇩C⇩L C›
proof -
from that obtain B and C :: ‹'a ⇒⇩C⇩L 'a› where ‹hilbert_schmidt B› and ‹hilbert_schmidt C› and ABC: ‹A = B o⇩C⇩L C›
by auto
from ‹hilbert_schmidt B›
have hs_WB: ‹hilbert_schmidt (W* o⇩C⇩L B)›
by (simp add: hilbert_schmidt_comp_right)
have ‹abs_op A = W* o⇩C⇩L A›
by (simp add: W_def polar_decomposition_correct')
also have ‹… = (W* o⇩C⇩L B) o⇩C⇩L C›
by (metis ABC cblinfun_compose_assoc)
finally have ‹abs_op A = (W* o⇩C⇩L B) o⇩C⇩L C›
by -
with hs_WB ‹hilbert_schmidt C›
show ?thesis
by auto
qed
have abs_hs_times_hs_trace_class: ‹trace_class A›
if ‹∃B (C :: 'a ⇒⇩C⇩L 'a). hilbert_schmidt B ∧ hilbert_schmidt C ∧ abs_op A = B o⇩C⇩L C›
proof -
from that obtain B and C :: ‹'a ⇒⇩C⇩L 'a› where ‹hilbert_schmidt B› and ‹hilbert_schmidt C› and ABC: ‹abs_op A = B o⇩C⇩L C›
by auto
from ‹hilbert_schmidt B›
have ‹hilbert_schmidt (B*)›
by simp
then have ‹(λe. (norm (B* *⇩V e))⇧2) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_hilbert_schmidt_norm_square summable_on_iff_abs_summable_on_real)
moreover
from ‹hilbert_schmidt C›
have ‹(λe. (norm (C *⇩V e))⇧2) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_hilbert_schmidt_norm_square summable_on_iff_abs_summable_on_real)
ultimately have ‹(λe. norm (B* *⇩V e) * norm (C *⇩V e)) abs_summable_on some_chilbert_basis›
apply (rule_tac abs_summable_product)
by (metis (no_types, lifting) power2_eq_square summable_on_cong)+
then have ‹(λe. cinner e (abs_op A *⇩V e)) abs_summable_on some_chilbert_basis›
proof (rule Infinite_Sum.abs_summable_on_comparison_test)
fix e :: 'a assume ‹e ∈ some_chilbert_basis›
have ‹norm (e ∙⇩C (abs_op A *⇩V e)) = norm ((B* *⇩V e) ∙⇩C (C *⇩V e))›
by (simp add: ABC cinner_adj_left)
also have ‹… ≤ norm (B* *⇩V e) * norm (C *⇩V e)›
by (rule Cauchy_Schwarz_ineq2)
also have ‹… = norm (norm (B* *⇩V e) * norm (C *⇩V e))›
by simp
finally show ‹cmod (e ∙⇩C (abs_op A *⇩V e)) ≤ norm (norm (B* *⇩V e) * norm (C *⇩V e))›
by -
qed
then show ‹trace_class A›
apply (rule trace_classI[rotated]) by simp
qed
from trace_class_sqrt_hs sqrt_hs_hs_times_hs hs_times_hs_abs_hs_times_hs abs_hs_times_hs_trace_class
show ?thesis1 and ?thesis2 and ?thesis3
unfolding Sq_def by metis+
qed
lemma trace_exists:
assumes ‹is_onb B› and ‹trace_class A›
shows ‹(λe. e ∙⇩C (A *⇩V e)) summable_on B›
proof -
obtain b c :: ‹'a ⇒⇩C⇩L 'a› where ‹hilbert_schmidt b› ‹hilbert_schmidt c› and Abc: ‹A = c* o⇩C⇩L b›
by (metis abs_op_pos adj_cblinfun_compose assms(2) double_adj hilbert_schmidt_comp_left hilbert_schmidt_comp_right polar_decomposition_correct polar_decomposition_correct' positive_selfadjointI[unfolded selfadjoint_def] trace_class_iff_hs_times_hs)
have ‹(λe. (norm (b *⇩V e))⇧2) summable_on B›
using ‹hilbert_schmidt b› assms(1) summable_hilbert_schmidt_norm_square by auto
moreover have ‹(λe. (norm (c *⇩V e))⇧2) summable_on B›
using ‹hilbert_schmidt c› assms(1) summable_hilbert_schmidt_norm_square by auto
ultimately have ‹(λe. (((norm (b *⇩V e))⇧2 + (norm (c *⇩V e))⇧2)) / 2) summable_on B›
by (auto intro!: summable_on_cdivide summable_on_add)
then have ‹(λe. (((norm (b *⇩V e))⇧2 + (norm (c *⇩V e))⇧2)) / 2) abs_summable_on B›
by simp
then have ‹(λe. e ∙⇩C (A *⇩V e)) abs_summable_on B›
proof (rule abs_summable_on_comparison_test)
fix e assume ‹e ∈ B›
obtain γ where ‹cmod γ = 1› and γ: ‹γ * ((b *⇩V e) ∙⇩C (c *⇩V e)) = abs ((b *⇩V e) ∙⇩C (c *⇩V e))›
apply atomize_elim
apply (cases ‹(b *⇩V e) ∙⇩C (c *⇩V e) ≠ 0›)
apply (rule exI[of _ ‹cnj (sgn ((b *⇩V e) ∙⇩C (c *⇩V e)))›])
apply (auto simp add: norm_sgn intro!: norm_one)
by (metis (no_types, lifting) abs_mult_sgn cblinfun.scaleC_right cblinfun_mult_right.rep_eq cdot_square_norm complex_norm_square complex_scaleC_def mult.comm_neutral norm_one norm_sgn one_cinner_one)
have ‹cmod (e ∙⇩C (A *⇩V e)) = Re (abs (e ∙⇩C (A *⇩V e)))›
by (metis abs_nn cmod_Re norm_abs)
also have ‹… = Re (abs ((b *⇩V e) ∙⇩C (c *⇩V e)))›
by (metis (mono_tags, lifting) Abc abs_nn cblinfun_apply_cblinfun_compose cinner_adj_left cinner_commute' complex_mod_cnj complex_of_real_cmod norm_abs)
also have ‹… = Re (((b *⇩V e) ∙⇩C (γ *⇩C (c *⇩V e))))›
by (simp add: γ)
also have ‹… ≤ ((norm (b *⇩V e))⇧2 + (norm (γ *⇩C (c *⇩V e)))⇧2) / 2›
by (smt (z3) field_sum_of_halves norm_ge_zero polar_identity_minus zero_le_power_eq_numeral)
also have ‹… = ((norm (b *⇩V e))⇧2 + (norm (c *⇩V e))⇧2) / 2›
by (simp add: ‹cmod γ = 1›)
also have ‹… ≤ norm (((norm (b *⇩V e))⇧2 + (norm (c *⇩V e))⇧2) / 2)›
by simp
finally show ‹cmod (e ∙⇩C (A *⇩V e)) ≤ norm (((norm (b *⇩V e))⇧2 + (norm (c *⇩V e))⇧2) / 2)›
by -
qed
then show ?thesis
by (metis abs_summable_summable)
qed
lemma trace_plus_prelim:
assumes ‹trace_class a› ‹trace_class b› ‹trace_class (a+b)›
shows ‹trace (a + b) = trace a + trace b›
by (auto simp add: assms infsum_add trace_def cblinfun.add_left cinner_add_right
intro!: infsum_add trace_exists)
lemma hs_times_hs_trace_class:
fixes B :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space› and C :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes ‹hilbert_schmidt B› and ‹hilbert_schmidt C›
shows ‹trace_class (B o⇩C⇩L C)›
proof -
define A Sq W where ‹A = B o⇩C⇩L C› and ‹Sq = sqrt_op (abs_op A)› and ‹W = polar_decomposition A›
from ‹hilbert_schmidt B›
have hs_WB: ‹hilbert_schmidt (W* o⇩C⇩L B)›
by (simp add: hilbert_schmidt_comp_right)
have ‹abs_op A = W* o⇩C⇩L A›
by (simp add: W_def polar_decomposition_correct')
also have ‹… = (W* o⇩C⇩L B) o⇩C⇩L C›
by (metis A_def cblinfun_compose_assoc)
finally have abs_op_A: ‹abs_op A = (W* o⇩C⇩L B) o⇩C⇩L C›
by -
from ‹hilbert_schmidt (W* o⇩C⇩L B)›
have ‹hilbert_schmidt (B* o⇩C⇩L W)›
by (simp add: assms(1) hilbert_schmidt_comp_left)
then have ‹(λe. (norm ((B* o⇩C⇩L W) *⇩V e))⇧2) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_hilbert_schmidt_norm_square summable_on_iff_abs_summable_on_real)
moreover from ‹hilbert_schmidt C›
have ‹(λe. (norm (C *⇩V e))⇧2) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_hilbert_schmidt_norm_square summable_on_iff_abs_summable_on_real)
ultimately have ‹(λe. norm ((B* o⇩C⇩L W) *⇩V e) * norm (C *⇩V e)) abs_summable_on some_chilbert_basis›
apply (rule_tac abs_summable_product)
by (metis (no_types, lifting) power2_eq_square summable_on_cong)+
then have ‹(λe. cinner e (abs_op A *⇩V e)) abs_summable_on some_chilbert_basis›
proof (rule Infinite_Sum.abs_summable_on_comparison_test)
fix e :: 'a assume ‹e ∈ some_chilbert_basis›
have ‹norm (e ∙⇩C (abs_op A *⇩V e)) = norm (((B* o⇩C⇩L W) *⇩V e) ∙⇩C (C *⇩V e))›
by (simp add: abs_op_A cinner_adj_left cinner_adj_right)
also have ‹… ≤ norm ((B* o⇩C⇩L W) *⇩V e) * norm (C *⇩V e)›
by (rule Cauchy_Schwarz_ineq2)
also have ‹… = norm (norm ((B* o⇩C⇩L W) *⇩V e) * norm (C *⇩V e))›
by simp
finally show ‹cmod (e ∙⇩C (abs_op A *⇩V e)) ≤ norm (norm ((B* o⇩C⇩L W) *⇩V e) * norm (C *⇩V e))›
by -
qed
then show ‹trace_class A›
apply (rule trace_classI[rotated]) by simp
qed
instantiation hilbert_schmidt :: (chilbert_space, chilbert_space) complex_vector begin
instance
proof intro_classes
fix a b c :: ‹('a,'b) hilbert_schmidt›
show ‹a + b + c = a + (b + c)›
apply transfer by auto
show ‹a + b = b + a›
apply transfer by auto
show ‹0 + a = a›
apply transfer by auto
show ‹- a + a = 0›
apply transfer by auto
show ‹a - b = a + - b›
apply transfer by auto
show ‹r *⇩C (a + b) = r *⇩C a + r *⇩C b› for r :: complex
apply transfer
using scaleC_add_right
by auto
show ‹(r + r') *⇩C a = r *⇩C a + r' *⇩C a› for r r' :: complex
apply transfer
by (simp add: scaleC_add_left)
show ‹r *⇩C r' *⇩C a = (r * r') *⇩C a› for r r'
apply transfer by auto
show ‹1 *⇩C a = a›
apply transfer by auto
qed
end
instantiation hilbert_schmidt :: (chilbert_space, chilbert_space) "complex_inner" begin
lift_definition cinner_hilbert_schmidt :: ‹('a,'b) hilbert_schmidt ⇒ ('a,'b) hilbert_schmidt ⇒ complex› is
‹λb c. trace (b* o⇩C⇩L c)› .
instance
proof intro_classes
fix x y z :: ‹('a,'b) hilbert_schmidt›
show ‹x ∙⇩C y = cnj (y ∙⇩C x)›
proof (transfer; unfold mem_Collect_eq)
fix x y :: ‹'a ⇒⇩C⇩L 'b›
assume hs_xy: ‹hilbert_schmidt x› ‹hilbert_schmidt y›
then have tc: ‹trace_class ((y* o⇩C⇩L x)*)› ‹trace_class (y* o⇩C⇩L x)›
by (auto intro!: hs_times_hs_trace_class)
have ‹trace (x* o⇩C⇩L y) = trace ((y* o⇩C⇩L x)*)›
by simp
also have ‹… = cnj (trace (y* o⇩C⇩L x))›
using tc trace_adj_prelim by blast
finally show ‹trace (x* o⇩C⇩L y) = cnj (trace (y* o⇩C⇩L x))›
by -
qed
show ‹(x + y) ∙⇩C z = x ∙⇩C z + y ∙⇩C z›
proof (transfer; unfold mem_Collect_eq)
fix x y z :: ‹'a ⇒⇩C⇩L 'b›
assume [simp]: ‹hilbert_schmidt x› ‹hilbert_schmidt y› ‹hilbert_schmidt z›
have [simp]: ‹trace_class ((x + y)* o⇩C⇩L z)› ‹trace_class (x* o⇩C⇩L z)› ‹trace_class (y* o⇩C⇩L z)›
by (auto intro!: hs_times_hs_trace_class hilbert_schmidt_adj hilbert_schmidt_plus)
then have [simp]: ‹trace_class ((x* o⇩C⇩L z) + (y* o⇩C⇩L z))›
by (simp add: adj_plus cblinfun_compose_add_left)
show ‹trace ((x + y)* o⇩C⇩L z) = trace (x* o⇩C⇩L z) + trace (y* o⇩C⇩L z)›
by (simp add: trace_plus_prelim adj_plus cblinfun_compose_add_left hs_times_hs_trace_class)
qed
show ‹r *⇩C x ∙⇩C y = cnj r * (x ∙⇩C y)› for r
apply transfer
by (simp add: trace_scaleC)
show ‹0 ≤ x ∙⇩C x›
apply transfer
by (simp add: positive_cblinfun_squareI trace_pos)
show ‹(x ∙⇩C x = 0) = (x = 0)›
proof (transfer; unfold mem_Collect_eq)
fix x :: ‹'a ⇒⇩C⇩L 'b›
assume [simp]: ‹hilbert_schmidt x›
have ‹trace (x* o⇩C⇩L x) = 0 ⟷ trace (abs_op (x* o⇩C⇩L x)) = 0›
by (metis abs_op_def positive_cblinfun_squareI sqrt_op_unique)
also have ‹… ⟷ trace_norm (x* o⇩C⇩L x) = 0›
by simp
also have ‹… ⟷ x* o⇩C⇩L x = 0›
by (metis ‹hilbert_schmidt x› hilbert_schmidt_def trace_norm_0 trace_norm_nondegenerate)
also have ‹… ⟷ x = 0›
using cblinfun_compose_zero_right op_square_nondegenerate by blast
finally show ‹trace (x* o⇩C⇩L x) = 0 ⟷ x = 0›
by -
qed
show ‹norm x = sqrt (cmod (x ∙⇩C x))›
apply transfer
apply (auto simp: hilbert_schmidt_norm_def)
by (metis Re_complex_of_real cmod_Re positive_cblinfun_squareI trace_norm_pos trace_pos)
qed
end
lemma hilbert_schmidt_norm_triangle_ineq:
fixes a b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes ‹hilbert_schmidt a› ‹hilbert_schmidt b›
shows ‹hilbert_schmidt_norm (a + b) ≤ hilbert_schmidt_norm a + hilbert_schmidt_norm b›
proof -
define a' b' where ‹a' = Abs_hilbert_schmidt a› and ‹b' = Abs_hilbert_schmidt b›
have [transfer_rule]: ‹cr_hilbert_schmidt a a'›
by (simp add: Abs_hilbert_schmidt_inverse a'_def assms(1) cr_hilbert_schmidt_def)
have [transfer_rule]: ‹cr_hilbert_schmidt b b'›
by (simp add: Abs_hilbert_schmidt_inverse assms(2) b'_def cr_hilbert_schmidt_def)
have ‹norm (a' + b') ≤ norm a' + norm b'›
by (rule norm_triangle_ineq)
then show ?thesis
apply transfer
by -
qed
lift_definition adj_hs :: ‹('a::chilbert_space,'b::chilbert_space) hilbert_schmidt ⇒ ('b,'a) hilbert_schmidt› is adj
by auto
lemma adj_hs_plus: ‹adj_hs (x + y) = adj_hs x + adj_hs y›
apply transfer
by (simp add: adj_plus)
lemma adj_hs_minus: ‹adj_hs (x - y) = adj_hs x - adj_hs y›
apply transfer
by (simp add: adj_minus)
lemma norm_adj_hs[simp]: ‹norm (adj_hs x) = norm x›
apply transfer
by simp
lemma hilbert_schmidt_norm_geq_norm:
assumes ‹hilbert_schmidt a›
shows ‹norm a ≤ hilbert_schmidt_norm a›
proof -
have ‹norm (a x) ≤ hilbert_schmidt_norm a› if ‹norm x = 1› for x
proof -
obtain B where ‹x ∈ B› and ‹is_onb B›
using orthonormal_basis_exists[of ‹{x}›] ‹norm x = 1›
by force
have ‹(norm (a x))⇧2 = (∑⇩∞x∈{x}. (norm (a x))⇧2)›
by simp
also have ‹… ≤ (∑⇩∞x∈B. (norm (a x))⇧2)›
apply (rule infsum_mono_neutral)
by (auto intro!: summable_hilbert_schmidt_norm_square ‹is_onb B› assms ‹x ∈ B›)
also have ‹… = (hilbert_schmidt_norm a)⇧2›
using infsum_hilbert_schmidt_norm_square[OF ‹is_onb B› assms]
by -
finally show ?thesis
by force
qed
then show ?thesis
by (auto intro!: norm_cblinfun_bound_unit)
qed
subsection ‹Trace-norm and trace-class, continued›
lemma trace_class_comp_left: ‹trace_class (a o⇩C⇩L b)› if ‹trace_class a› for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
from ‹trace_class a›
obtain C :: ‹'a ⇒⇩C⇩L 'b› and B where ‹hilbert_schmidt C› and ‹hilbert_schmidt B› and aCB: ‹a = C o⇩C⇩L B›
by (auto simp: trace_class_iff_hs_times_hs)
from ‹hilbert_schmidt B› have ‹hilbert_schmidt (B o⇩C⇩L b)›
by (simp add: hilbert_schmidt_comp_left)
with ‹hilbert_schmidt C› have ‹trace_class (C o⇩C⇩L (B o⇩C⇩L b))›
using hs_times_hs_trace_class by blast
then show ?thesis
by (simp flip: aCB cblinfun_compose_assoc)
qed
lemma trace_class_comp_right: ‹trace_class (a o⇩C⇩L b)› if ‹trace_class b› for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
from ‹trace_class b›
obtain C :: ‹'c ⇒⇩C⇩L 'a› and B where ‹hilbert_schmidt C› and ‹hilbert_schmidt B› and aCB: ‹b = C o⇩C⇩L B›
by (auto simp: trace_class_iff_hs_times_hs)
from ‹hilbert_schmidt C› have ‹hilbert_schmidt (a o⇩C⇩L C)›
by (simp add: hilbert_schmidt_comp_right)
with ‹hilbert_schmidt B› have ‹trace_class ((a o⇩C⇩L C) o⇩C⇩L B)›
using hs_times_hs_trace_class by blast
then show ?thesis
by (simp flip: aCB add: cblinfun_compose_assoc)
qed
lemma
fixes B :: ‹'a::chilbert_space set› and A :: ‹'a ⇒⇩C⇩L 'a› and b :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space› and c :: ‹'c ⇒⇩C⇩L 'b›
shows trace_alt_def:
‹is_onb B ⟹ trace A = (if trace_class A then (∑⇩∞e∈B. e ∙⇩C (A *⇩V e)) else 0)›
and trace_hs_times_hs: ‹hilbert_schmidt c ⟹ hilbert_schmidt b ⟹ trace (c o⇩C⇩L b) =
((of_real (hilbert_schmidt_norm ((c*) + b)))⇧2 - (of_real (hilbert_schmidt_norm ((c*) - b)))⇧2 -
𝗂 * (of_real (hilbert_schmidt_norm (((c*) + 𝗂 *⇩C b))))⇧2 +
𝗂 * (of_real (hilbert_schmidt_norm (((c*) - 𝗂 *⇩C b))))⇧2) / 4›
proof -
have ecbe_has_sum: ‹((λe. e ∙⇩C ((c o⇩C⇩L b) *⇩V e)) has_sum
((of_real (hilbert_schmidt_norm ((c*) + b)))⇧2 - (of_real (hilbert_schmidt_norm ((c*) - b)))⇧2 -
𝗂 * (of_real (hilbert_schmidt_norm ((c*) + 𝗂 *⇩C b)))⇧2 +
𝗂 * (of_real (hilbert_schmidt_norm ((c*) - 𝗂 *⇩C b)))⇧2) / 4) B›
if ‹is_onb B› and ‹hilbert_schmidt c› and ‹hilbert_schmidt b› for B :: ‹'y::chilbert_space set› and c :: ‹'x::chilbert_space ⇒⇩C⇩L 'y› and b
apply (simp flip: cinner_adj_left[of c])
apply (subst cdot_norm)
using that by (auto simp add: field_class.field_divide_inverse infsum_cmult_left'
simp del: Num.inverse_eq_divide_numeral
simp flip: cblinfun.add_left cblinfun.diff_left cblinfun.scaleC_left of_real_power
intro!: has_sum_cmult_left has_sum_cmult_right has_sum_add has_sum_diff has_sum_of_real
has_sum_hilbert_schmidt_norm_square hilbert_schmidt_plus hilbert_schmidt_minus hilbert_schmidt_scaleC)
then have ecbe_infsum: ‹(∑⇩∞e∈B. e ∙⇩C ((c o⇩C⇩L b) *⇩V e)) =
(((of_real (hilbert_schmidt_norm ((c*) + b)))⇧2 - (of_real (hilbert_schmidt_norm ((c*) - b)))⇧2 -
𝗂 * (of_real (hilbert_schmidt_norm ((c*) + 𝗂 *⇩C b)))⇧2 +
𝗂 * (of_real (hilbert_schmidt_norm ((c*) - 𝗂 *⇩C b)))⇧2) / 4)›
if ‹is_onb B› and ‹hilbert_schmidt c› and ‹hilbert_schmidt b› for B :: ‹'y::chilbert_space set› and c :: ‹'x::chilbert_space ⇒⇩C⇩L 'y› and b
using infsumI that(1) that(2) that(3) by blast
show ‹trace (c o⇩C⇩L b) =
((of_real (hilbert_schmidt_norm ((c*) + b)))⇧2 - (of_real (hilbert_schmidt_norm ((c*) - b)))⇧2 -
𝗂 * (of_real (hilbert_schmidt_norm ((c*) + 𝗂 *⇩C b)))⇧2 +
𝗂 * (of_real (hilbert_schmidt_norm ((c*) - 𝗂 *⇩C b)))⇧2) / 4›
if ‹hilbert_schmidt c› and ‹hilbert_schmidt b›
proof -
from that have tc_cb[simp]: ‹trace_class (c o⇩C⇩L b)›
by (rule hs_times_hs_trace_class)
show ?thesis
using ecbe_infsum[OF is_onb_some_chilbert_basis ‹hilbert_schmidt c› ‹hilbert_schmidt b›]
apply (simp only: trace_def)
by simp
qed
show ‹trace A = (if trace_class A then (∑⇩∞e∈B. e ∙⇩C (A *⇩V e)) else 0)› if ‹is_onb B›
proof (cases ‹trace_class A›)
case True
with that
obtain b c :: ‹'a ⇒⇩C⇩L 'a› where hs_b: ‹hilbert_schmidt b› and hs_c: ‹hilbert_schmidt c› and Acb: ‹A = c o⇩C⇩L b›
by (metis trace_class_iff_hs_times_hs)
have [simp]: ‹trace_class (c o⇩C⇩L b)›
using Acb True by auto
show ‹trace A = (if trace_class A then (∑⇩∞e∈B. e ∙⇩C (A *⇩V e)) else 0)›
using ecbe_infsum[OF is_onb_some_chilbert_basis hs_c hs_b]
using ecbe_infsum[OF ‹is_onb B› hs_c hs_b]
by (simp only: Acb trace_def)
next
case False
then show ?thesis
by (simp add: trace_def)
qed
qed
lemma trace_ket_sum:
fixes A :: ‹'a ell2 ⇒⇩C⇩L 'a ell2›
assumes ‹trace_class A›
shows ‹trace A = (∑⇩∞e. ket e ∙⇩C (A *⇩V ket e))›
apply (subst infsum_reindex[where h=ket, unfolded o_def, symmetric])
by (auto simp: ‹trace_class A› trace_alt_def[OF is_onb_ket] is_onb_ket)
lemma trace_one_dim[simp]: ‹trace A = one_dim_iso A› for A :: ‹'a::one_dim ⇒⇩C⇩L 'a›
proof -
have onb: ‹is_onb {1 :: 'a}›
by auto
have ‹trace A = 1 ∙⇩C (A *⇩V 1)›
apply (subst trace_alt_def)
apply (fact onb)
by simp
also have ‹… = one_dim_iso A›
by (simp add: cinner_cblinfun_def one_dim_iso_def)
finally show ?thesis
by -
qed
lemma trace_has_sum:
assumes ‹is_onb E›
assumes ‹trace_class t›
shows ‹((λe. e ∙⇩C (t *⇩V e)) has_sum trace t) E›
using assms(1) assms(2) trace_alt_def trace_exists by fastforce
lemma trace_sandwich_isometry[simp]: ‹trace (sandwich U A) = trace A› if ‹isometry U›
proof (cases ‹trace_class A›)
case True
note True[simp]
have ‹is_ortho_set ((*⇩V) U ` some_chilbert_basis)›
unfolding is_ortho_set_def
apply auto
apply (metis (no_types, opaque_lifting) cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply cinner_adj_right is_ortho_set_def is_ortho_set_some_chilbert_basis isometry_def that)
by (metis is_normal_some_chilbert_basis isometry_preserves_norm norm_zero that zero_neq_one)
moreover have ‹x ∈ (*⇩V) U ` some_chilbert_basis ⟹ norm x = 1› for x
using is_normal_some_chilbert_basis isometry_preserves_norm that by fastforce
ultimately obtain B where BU: ‹B ⊇ U ` some_chilbert_basis› and ‹is_onb B›
apply atomize_elim
by (rule orthonormal_basis_exists)
have xUy: ‹x ∙⇩C U y = 0› if xBU: ‹x ∈ B - U ` some_chilbert_basis› for x y
proof -
from that ‹is_onb B› ‹isometry U›
have ‹x ∙⇩C z = 0› if ‹z ∈ U ` some_chilbert_basis› for z
using that by (metis BU Diff_iff in_mono is_onb_def is_ortho_set_def)
then have ‹x ∈ orthogonal_complement (closure (cspan (U ` some_chilbert_basis)))›
by (metis orthogonal_complementI orthogonal_complement_of_closure orthogonal_complement_of_cspan)
then have ‹x ∈ space_as_set (- ccspan (U ` some_chilbert_basis))›
by (simp add: ccspan.rep_eq uminus_ccsubspace.rep_eq)
then have ‹x ∈ space_as_set (- (U *⇩S top))›
by (metis cblinfun_image_ccspan ccspan_some_chilbert_basis)
moreover have ‹U y ∈ space_as_set (U *⇩S top)›
by simp
ultimately show ?thesis
apply (transfer fixing: x y)
using orthogonal_complement_orthoI by blast
qed
have [simp]: ‹trace_class (sandwich U A)›
by (simp add: sandwich.rep_eq trace_class_comp_left trace_class_comp_right)
have ‹trace (sandwich U A) = (∑⇩∞e∈B. e ∙⇩C ((sandwich U *⇩V A) *⇩V e))›
using ‹is_onb B› trace_alt_def by fastforce
also have ‹… = (∑⇩∞e∈U ` some_chilbert_basis. e ∙⇩C ((sandwich U *⇩V A) *⇩V e))›
apply (rule infsum_cong_neutral)
using BU xUy by (auto simp: sandwich_apply)
also have ‹… = (∑⇩∞e∈some_chilbert_basis. U e ∙⇩C ((sandwich U *⇩V A) *⇩V U e))›
apply (subst infsum_reindex)
apply (metis cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply inj_on_inverseI isometry_def that)
by (auto simp: o_def)
also have ‹… = (∑⇩∞e∈some_chilbert_basis. e ∙⇩C A e)›
apply (rule infsum_cong)
apply (simp add: sandwich_apply flip: cinner_adj_right)
by (metis cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply isometry_def that)
also have ‹… = trace A›
by (simp add: trace_def)
finally show ?thesis
by -
next
case False
note False[simp]
then have [simp]: ‹¬ trace_class (sandwich U A)›
by (smt (verit, ccfv_SIG) cblinfun_assoc_left(1) cblinfun_compose_id_left cblinfun_compose_id_right isometryD sandwich.rep_eq that trace_class_comp_left trace_class_comp_right)
show ?thesis
by (simp add: trace_def)
qed
lemma circularity_of_trace:
fixes a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space› and b :: ‹'b ⇒⇩C⇩L 'a›
assumes ‹trace_class a›
shows ‹trace (a o⇩C⇩L b) = trace (b o⇩C⇩L a)›
proof -
define a' b' :: ‹('a×'b) ⇒⇩C⇩L ('a×'b)›
where ‹a' = cblinfun_right o⇩C⇩L a o⇩C⇩L cblinfun_left*›
and ‹b' = cblinfun_left o⇩C⇩L b o⇩C⇩L cblinfun_right*›
have ‹trace_class a'›
by (simp add: a'_def assms trace_class_comp_left trace_class_comp_right)
have circ': ‹trace (a' o⇩C⇩L b') = trace (b' o⇩C⇩L a')›
proof -
from ‹trace_class a'›
obtain B C :: ‹('a×'b) ⇒⇩C⇩L ('a×'b)› where ‹hilbert_schmidt B› and ‹hilbert_schmidt C› and aCB: ‹a' = C* o⇩C⇩L B›
by (metis abs_op_pos adj_cblinfun_compose double_adj hilbert_schmidt_comp_left hilbert_schmidt_comp_right polar_decomposition_correct polar_decomposition_correct' positive_selfadjointI[unfolded selfadjoint_def] trace_class_iff_hs_times_hs)
have hs_iB: ‹hilbert_schmidt (𝗂 *⇩C B)›
by (metis Abs_hilbert_schmidt_inverse Rep_hilbert_schmidt ‹hilbert_schmidt B› mem_Collect_eq scaleC_hilbert_schmidt.rep_eq)
have *: ‹Re (trace (C* o⇩C⇩L B)) = Re (trace (C o⇩C⇩L B*))› if ‹hilbert_schmidt B› ‹hilbert_schmidt C› for B C :: ‹('a×'b) ⇒⇩C⇩L ('a×'b)›
proof -
from that
obtain B' C' where ‹B = Rep_hilbert_schmidt B'› and ‹C = Rep_hilbert_schmidt C'›
by (meson Rep_hilbert_schmidt_cases mem_Collect_eq)
then have [transfer_rule]: ‹cr_hilbert_schmidt B B'› ‹cr_hilbert_schmidt C C'›
by (simp_all add: cr_hilbert_schmidt_def)
have ‹Re (trace (C* o⇩C⇩L B)) = Re (C' ∙⇩C B')›
apply transfer by simp
also have ‹… = (1/4) * ((norm (C' + B'))⇧2 - (norm (C' - B'))⇧2)›
by (simp add: cdot_norm)
also have ‹… = (1/4) * ((norm (adj_hs C' + adj_hs B'))⇧2 - (norm (adj_hs C' - adj_hs B'))⇧2)›
by (simp add: flip: adj_hs_plus adj_hs_minus)
also have ‹… = Re (adj_hs C' ∙⇩C adj_hs B')›
by (simp add: cdot_norm)
also have ‹… = Re (trace (C o⇩C⇩L B*))›
apply transfer by simp
finally show ?thesis
by -
qed
have **: ‹trace (C* o⇩C⇩L B) = cnj (trace (C o⇩C⇩L B*))› if ‹hilbert_schmidt B› ‹hilbert_schmidt C› for B C :: ‹('a×'b) ⇒⇩C⇩L ('a×'b)›
using *[OF ‹hilbert_schmidt B› ‹hilbert_schmidt C›]
using *[OF hilbert_schmidt_scaleC[of _ 𝗂, OF ‹hilbert_schmidt B›] ‹hilbert_schmidt C›]
apply (auto simp: trace_scaleC cblinfun_compose_uminus_right trace_uminus)
by (smt (verit, best) cnj.code complex.collapse)
have ‹trace (b' o⇩C⇩L a') = trace ((b' o⇩C⇩L C*) o⇩C⇩L B)›
by (simp add: aCB cblinfun_assoc_left(1))
also from ** ‹hilbert_schmidt B› ‹hilbert_schmidt C› have ‹… = cnj (trace ((C o⇩C⇩L b'*) o⇩C⇩L B*))›
by (metis adj_cblinfun_compose double_adj hilbert_schmidt_comp_left)
also have ‹… = cnj (trace (C o⇩C⇩L (B o⇩C⇩L b')*))›
by (simp add: cblinfun_assoc_left(1))
also from ** ‹hilbert_schmidt B› ‹hilbert_schmidt C› have ‹… = trace (C* o⇩C⇩L (B o⇩C⇩L b'))›
by (simp add: hilbert_schmidt_comp_left)
also have ‹… = trace (a' o⇩C⇩L b')›
by (simp add: aCB cblinfun_compose_assoc)
finally show ?thesis
by simp
qed
have ‹trace (a o⇩C⇩L b) = trace (sandwich cblinfun_right (a o⇩C⇩L b) :: ('a×'b) ⇒⇩C⇩L ('a×'b))›
by simp
also have ‹… = trace (sandwich cblinfun_right (a o⇩C⇩L (cblinfun_left* o⇩C⇩L (cblinfun_left :: _⇒⇩C⇩L('a×'b))) o⇩C⇩L b) :: ('a×'b) ⇒⇩C⇩L ('a×'b))›
by simp
also have ‹… = trace (a' o⇩C⇩L b')›
by (simp only: a'_def b'_def sandwich_apply cblinfun_compose_assoc)
also have ‹… = trace (b' o⇩C⇩L a')›
by (rule circ')
also have ‹… = trace (sandwich cblinfun_left (b o⇩C⇩L (cblinfun_right* o⇩C⇩L (cblinfun_right :: _⇒⇩C⇩L('a×'b))) o⇩C⇩L a) :: ('a×'b) ⇒⇩C⇩L ('a×'b))›
by (simp only: a'_def b'_def sandwich_apply cblinfun_compose_assoc)
also have ‹… = trace (sandwich cblinfun_left (b o⇩C⇩L a) :: ('a×'b) ⇒⇩C⇩L ('a×'b))›
by simp
also have ‹… = trace (b o⇩C⇩L a)›
by simp
finally show ‹trace (a o⇩C⇩L b) = trace (b o⇩C⇩L a)›
by -
qed
lemma trace_butterfly_comp: ‹trace (butterfly x y o⇩C⇩L a) = y ∙⇩C (a *⇩V x)›
proof -
have ‹trace (butterfly x y o⇩C⇩L a) = trace (vector_to_cblinfun y* o⇩C⇩L (a o⇩C⇩L (vector_to_cblinfun x :: complex ⇒⇩C⇩L _)))›
unfolding butterfly_def
by (metis cblinfun_compose_assoc circularity_of_trace trace_class_finite_dim)
also have ‹… = y ∙⇩C (a *⇩V x)›
by (simp add: one_dim_iso_cblinfun_comp)
finally show ?thesis
by -
qed
lemma trace_butterfly: ‹trace (butterfly x y) = y ∙⇩C x›
using trace_butterfly_comp[where a=id_cblinfun] by auto
lemma trace_butterfly_comp': ‹trace (a o⇩C⇩L butterfly x y) = y ∙⇩C (a *⇩V x)›
by (simp add: cblinfun_comp_butterfly trace_butterfly)
lemma trace_norm_adj[simp]: ‹trace_norm (a*) = trace_norm a›
proof -
have ‹of_real (trace_norm (a*)) = trace (sandwich (polar_decomposition a) *⇩V abs_op a)›
by (metis abs_op_adj trace_abs_op)
also have ‹… = trace ((polar_decomposition a)* o⇩C⇩L (polar_decomposition a) o⇩C⇩L abs_op a)›
by (metis (no_types, lifting) abs_op_adj cblinfun_compose_assoc circularity_of_trace double_adj
polar_decomposition_correct polar_decomposition_correct' sandwich.rep_eq trace_class_abs_op trace_def)
also have ‹… = trace (abs_op a)›
by (simp add: cblinfun_compose_assoc polar_decomposition_correct polar_decomposition_correct')
also have ‹… = of_real (trace_norm a)›
by simp
finally show ?thesis
by simp
qed
lemma trace_class_adj[simp]: ‹trace_class (a*)› if ‹trace_class a›
proof (rule ccontr)
assume asm: ‹¬ trace_class (a*)›
then have ‹trace_norm (a*) = 0›
by (simp add: trace_norm_def)
then have ‹trace_norm a = 0›
by (metis trace_norm_adj)
then have ‹a = 0›
using that trace_norm_nondegenerate by blast
then have ‹trace_class (a*)›
by simp
with asm show False
by simp
qed
lift_definition adj_tc :: ‹('a::chilbert_space, 'b::chilbert_space) trace_class ⇒ ('b,'a) trace_class› is adj
by simp
lift_definition selfadjoint_tc :: ‹('a::chilbert_space, 'a) trace_class ⇒ bool› is selfadjoint.
lemma selfadjoint_tc_def': ‹selfadjoint_tc a ⟷ adj_tc a = a›
apply transfer
using selfadjoint_def by blast
lemma trace_class_finite_dim'[simp]: ‹trace_class A› for A :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::{cfinite_dim,chilbert_space}›
by (metis double_adj trace_class_adj trace_class_finite_dim)
lemma trace_class_plus[simp]:
fixes t u :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes ‹trace_class t› and ‹trace_class u›
shows ‹trace_class (t + u)›
proof -
define II :: ‹'a ⇒⇩C⇩L ('a×'a)› where ‹II = cblinfun_left + cblinfun_right›
define JJ :: ‹('b×'b) ⇒⇩C⇩L 'b› where ‹JJ = cblinfun_left* + cblinfun_right*›
define tu :: ‹('a×'a) ⇒⇩C⇩L ('b×'b)› where ‹tu = (cblinfun_left o⇩C⇩L t o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L u o⇩C⇩L cblinfun_right*)›
have t_plus_u: ‹t + u = JJ o⇩C⇩L tu o⇩C⇩L II›
apply (simp add: II_def JJ_def tu_def cblinfun_compose_add_left cblinfun_compose_add_right cblinfun_compose_assoc)
by (simp flip: cblinfun_compose_assoc)
have ‹trace_class tu›
proof (rule trace_classI)
define BL BR B :: ‹('a×'a) set› where ‹BL = some_chilbert_basis × {0}›
and ‹BR = {0} × some_chilbert_basis›
and ‹B = BL ∪ BR›
have ‹BL ∩ BR = {}›
using is_ortho_set_some_chilbert_basis
by (auto simp: BL_def BR_def is_ortho_set_def)
show ‹is_onb B›
by (simp add: BL_def BR_def B_def is_onb_prod)
have abs_tu: ‹abs_op tu = (cblinfun_left o⇩C⇩L abs_op t o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L abs_op u o⇩C⇩L cblinfun_right*)›
using [[show_consts]]
proof -
have ‹((cblinfun_left o⇩C⇩L abs_op t o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L abs_op u o⇩C⇩L cblinfun_right*))*
o⇩C⇩L ((cblinfun_left o⇩C⇩L abs_op t o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L abs_op u o⇩C⇩L cblinfun_right*))
= tu* o⇩C⇩L tu›
proof -
have tt[THEN simp_a_oCL_b, simp]: ‹(abs_op t)* o⇩C⇩L abs_op t = t* o⇩C⇩L t›
by (simp add: abs_op_def positive_cblinfun_squareI positive_selfadjointI[unfolded selfadjoint_def])
have uu[THEN simp_a_oCL_b, simp]: ‹(abs_op u)* o⇩C⇩L abs_op u = u* o⇩C⇩L u›
by (simp add: abs_op_def positive_cblinfun_squareI positive_selfadjointI[unfolded selfadjoint_def])
note isometryD[THEN simp_a_oCL_b, simp]
note cblinfun_right_left_ortho[THEN simp_a_oCL_b, simp]
note cblinfun_left_right_ortho[THEN simp_a_oCL_b, simp]
show ?thesis
using tt[of ‹cblinfun_left* :: ('a×'a) ⇒⇩C⇩L 'a›] uu[of ‹cblinfun_right* :: ('a×'a) ⇒⇩C⇩L 'a›]
by (simp add: tu_def cblinfun_compose_add_right cblinfun_compose_add_left adj_plus
cblinfun_compose_assoc)
qed
moreover have ‹(cblinfun_left o⇩C⇩L abs_op t o⇩C⇩L cblinfun_left*) + (cblinfun_right o⇩C⇩L abs_op u o⇩C⇩L cblinfun_right*) ≥ 0›
apply (rule positive_cblinfunI)
by (auto simp: cblinfun.add_left cinner_pos_if_pos)
ultimately show ?thesis
by (rule abs_opI[symmetric])
qed
from assms(1)
have ‹(λx. x ∙⇩C (abs_op t *⇩V x)) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_on_iff_abs_summable_on_complex trace_class_abs_op trace_exists)
then have sum_BL: ‹(λx. x ∙⇩C (abs_op tu *⇩V x)) abs_summable_on BL›
apply (subst asm_rl[of ‹BL = (λx. (x,0)) ` some_chilbert_basis›])
by (auto simp: BL_def summable_on_reindex inj_on_def o_def abs_tu cblinfun.add_left)
from assms(2)
have ‹(λx. x ∙⇩C (abs_op u *⇩V x)) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_on_iff_abs_summable_on_complex trace_class_abs_op trace_exists)
then have sum_BR: ‹(λx. x ∙⇩C (abs_op tu *⇩V x)) abs_summable_on BR›
apply (subst asm_rl[of ‹BR = (λx. (0,x)) ` some_chilbert_basis›])
by (auto simp: BR_def summable_on_reindex inj_on_def o_def abs_tu cblinfun.add_left)
from sum_BL sum_BR
show ‹(λx. x ∙⇩C (abs_op tu *⇩V x)) abs_summable_on B›
using ‹BL ∩ BR = {}›
by (auto intro!: summable_on_Un_disjoint simp: B_def)
qed
with t_plus_u
show ‹trace_class (t + u)›
by (simp add: trace_class_comp_left trace_class_comp_right)
qed
lemma trace_class_minus[simp]: ‹trace_class t ⟹ trace_class u ⟹ trace_class (t - u)›
for t u :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
by (metis trace_class_plus trace_class_uminus uminus_add_conv_diff)
lemma trace_plus:
assumes ‹trace_class a› ‹trace_class b›
shows ‹trace (a + b) = trace a + trace b›
by (simp add: assms(1) assms(2) trace_plus_prelim)
hide_fact trace_plus_prelim
lemma trace_class_sum:
fixes a :: ‹'a ⇒ 'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space›
assumes ‹⋀i. i∈I ⟹ trace_class (a i)›
shows ‹trace_class (∑i∈I. a i)›
using assms apply (induction I rule:infinite_finite_induct)
by auto
lemma
assumes ‹⋀i. i∈I ⟹ trace_class (a i)›
shows trace_sum: ‹trace (∑i∈I. a i) = (∑i∈I. trace (a i))›
using assms apply (induction I rule:infinite_finite_induct)
by (auto simp: trace_plus trace_class_sum)
lemma cmod_trace_times: ‹cmod (trace (a o⇩C⇩L b)) ≤ norm a * trace_norm b› if ‹trace_class b›
for b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
define W where ‹W = polar_decomposition b›
have ‹norm W ≤ 1›
by (metis W_def norm_partial_isometry norm_zero order_refl polar_decomposition_partial_isometry zero_less_one_class.zero_le_one)
have hs1: ‹hilbert_schmidt (sqrt_op (abs_op b))›
using that trace_class_iff_sqrt_hs by blast
then have hs2: ‹hilbert_schmidt (sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*)›
by (simp add: hilbert_schmidt_comp_left)
from ‹trace_class b›
have ‹trace_class (a o⇩C⇩L b)›
using trace_class_comp_right by blast
then have sum1: ‹(λe. e ∙⇩C ((a o⇩C⇩L b) *⇩V e)) abs_summable_on some_chilbert_basis›
by (metis is_onb_some_chilbert_basis summable_on_iff_abs_summable_on_complex trace_exists)
have sum5: ‹(λx. (norm (sqrt_op (abs_op b) *⇩V x))⇧2) summable_on some_chilbert_basis›
using summable_hilbert_schmidt_norm_square[OF is_onb_some_chilbert_basis hs1]
by (simp add: power2_eq_square)
have sum4: ‹(λx. (norm ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V x))⇧2) summable_on some_chilbert_basis›
using summable_hilbert_schmidt_norm_square[OF is_onb_some_chilbert_basis hs2]
by (simp add: power2_eq_square)
have sum3: ‹(λe. norm ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e) * norm (sqrt_op (abs_op b) *⇩V e)) summable_on some_chilbert_basis›
apply (rule abs_summable_summable)
apply (rule abs_summable_product)
by (intro sum4 sum5 summable_on_iff_abs_summable_on_real[THEN iffD1])+
have sum2: ‹(λe. ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e) ∙⇩C (sqrt_op (abs_op b) *⇩V e)) abs_summable_on some_chilbert_basis›
using sum3[THEN summable_on_iff_abs_summable_on_real[THEN iffD1]]
apply (rule abs_summable_on_comparison_test)
by (simp add: complex_inner_class.Cauchy_Schwarz_ineq2)
from ‹trace_class b›
have ‹cmod (trace (a o⇩C⇩L b)) = cmod (∑⇩∞e∈some_chilbert_basis. e ∙⇩C ((a o⇩C⇩L b) *⇩V e))›
by (simp add: trace_class_comp_right trace_def)
also have ‹… ≤ (∑⇩∞e∈some_chilbert_basis. cmod (e ∙⇩C ((a o⇩C⇩L b) *⇩V e)))›
using sum1 by (rule norm_infsum_bound)
also have ‹… = (∑⇩∞e∈some_chilbert_basis. cmod (((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e) ∙⇩C (sqrt_op (abs_op b) *⇩V e)))›
apply (simp add: positive_selfadjointI[unfolded selfadjoint_def] flip: cinner_adj_right cblinfun_apply_cblinfun_compose)
by (metis (full_types) W_def abs_op_def cblinfun_compose_assoc polar_decomposition_correct sqrt_op_pos sqrt_op_square)
also have ‹… ≤ (∑⇩∞e∈some_chilbert_basis. norm ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e) * norm (sqrt_op (abs_op b) *⇩V e))›
using sum2 sum3 apply (rule infsum_mono)
using complex_inner_class.Cauchy_Schwarz_ineq2 by blast
also have ‹… = (∑⇩∞e∈some_chilbert_basis. norm (norm ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e) * norm (sqrt_op (abs_op b) *⇩V e)))›
by simp
also have ‹… ≤ sqrt (∑⇩∞e∈some_chilbert_basis. (norm (norm ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e)))⇧2)
* sqrt (∑⇩∞e∈some_chilbert_basis. (norm (norm (sqrt_op (abs_op b) *⇩V e)))⇧2)›
apply (rule Cauchy_Schwarz_ineq_infsum)
using sum4 sum5 by auto
also have ‹… = sqrt (∑⇩∞e∈some_chilbert_basis. (norm ((sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) *⇩V e))⇧2)
* sqrt (∑⇩∞e∈some_chilbert_basis. (norm (sqrt_op (abs_op b) *⇩V e))⇧2)›
by simp
also have ‹… = hilbert_schmidt_norm (sqrt_op (abs_op b) o⇩C⇩L W* o⇩C⇩L a*) * hilbert_schmidt_norm (sqrt_op (abs_op b))›
apply (subst infsum_hilbert_schmidt_norm_square, simp, fact hs2)
apply (subst infsum_hilbert_schmidt_norm_square, simp, fact hs1)
by simp
also have ‹… ≤ hilbert_schmidt_norm (sqrt_op (abs_op b)) * norm (W* o⇩C⇩L a*) * hilbert_schmidt_norm (sqrt_op (abs_op b))›
by (metis cblinfun_assoc_left(1) hilbert_schmidt_norm_comp_left hilbert_schmidt_norm_pos mult.commute mult_right_mono that trace_class_iff_sqrt_hs)
also have ‹… ≤ hilbert_schmidt_norm (sqrt_op (abs_op b)) * norm (W*) * norm (a*) * hilbert_schmidt_norm (sqrt_op (abs_op b))›
by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) hilbert_schmidt_norm_pos mult_right_mono norm_cblinfun_compose ordered_comm_semiring_class.comm_mult_left_mono)
also have ‹… ≤ hilbert_schmidt_norm (sqrt_op (abs_op b)) * norm (a*) * hilbert_schmidt_norm (sqrt_op (abs_op b))›
by (metis ‹norm W ≤ 1› hilbert_schmidt_norm_pos mult.right_neutral mult_left_mono mult_right_mono norm_adj norm_ge_zero)
also have ‹… = norm a * (hilbert_schmidt_norm (sqrt_op (abs_op b)))⇧2›
by (simp add: power2_eq_square)
also have ‹… = norm a * trace_norm b›
apply (simp add: hilbert_schmidt_norm_def positive_selfadjointI[unfolded selfadjoint_def])
by (metis abs_op_idem of_real_eq_iff trace_abs_op)
finally show ?thesis
by -
qed
lemma trace_leq_trace_norm[simp]: ‹cmod (trace a) ≤ trace_norm a›
proof (cases ‹trace_class a›)
case True
then have ‹cmod (trace a) ≤ norm (id_cblinfun :: 'a ⇒⇩C⇩L 'a) * trace_norm a›
using cmod_trace_times[where a=‹id_cblinfun :: 'a ⇒⇩C⇩L 'a› and b=a]
by simp
also have ‹… ≤ trace_norm a›
apply (rule mult_left_le_one_le)
by (auto intro!: mult_left_le_one_le simp: norm_cblinfun_id_le)
finally show ?thesis
by -
next
case False
then show ?thesis
by (simp add: trace_def)
qed
lemma trace_norm_triangle:
fixes a b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes [simp]: ‹trace_class a› ‹trace_class b›
shows ‹trace_norm (a + b) ≤ trace_norm a + trace_norm b›
proof -
define w where ‹w = polar_decomposition (a+b)›
have ‹norm (w*) ≤ 1›
by (metis dual_order.refl norm_adj norm_partial_isometry norm_zero polar_decomposition_partial_isometry w_def zero_less_one_class.zero_le_one)
have ‹trace_norm (a + b) = cmod (trace (abs_op (a+b)))›
by simp
also have ‹… = cmod (trace (w* o⇩C⇩L (a+b)))›
by (simp add: polar_decomposition_correct' w_def)
also have ‹… ≤ cmod (trace (w* o⇩C⇩L a)) + cmod (trace (w* o⇩C⇩L b))›
by (simp add: cblinfun_compose_add_right norm_triangle_ineq trace_class_comp_right trace_plus)
also have ‹… ≤ (norm (w*) * trace_norm a) + (norm (w*) * trace_norm b)›
by (smt (verit, best) assms(1) assms(2) cmod_trace_times)
also have ‹… ≤ trace_norm a + trace_norm b›
using ‹norm (w*) ≤ 1›
by (smt (verit, ccfv_SIG) mult_le_cancel_right2 trace_norm_nneg)
finally show ?thesis
by -
qed
instantiation trace_class :: (chilbert_space, chilbert_space) "{complex_vector}" begin
lift_definition zero_trace_class :: ‹('a,'b) trace_class› is 0 by auto
lift_definition minus_trace_class :: ‹('a,'b) trace_class ⇒ ('a,'b) trace_class ⇒ ('a,'b) trace_class› is minus by auto
lift_definition uminus_trace_class :: ‹('a,'b) trace_class ⇒ ('a,'b) trace_class› is uminus by simp
lift_definition plus_trace_class :: ‹('a,'b) trace_class ⇒ ('a,'b) trace_class ⇒ ('a,'b) trace_class› is plus by auto
lift_definition scaleC_trace_class :: ‹complex ⇒ ('a,'b) trace_class ⇒ ('a,'b) trace_class› is scaleC
by (metis (no_types, opaque_lifting) cblinfun_compose_id_right cblinfun_compose_scaleC_right mem_Collect_eq trace_class_comp_left)
lift_definition scaleR_trace_class :: ‹real ⇒ ('a,'b) trace_class ⇒ ('a,'b) trace_class› is scaleR
by (metis (no_types, opaque_lifting) cblinfun_compose_id_right cblinfun_compose_scaleC_right mem_Collect_eq scaleR_scaleC trace_class_comp_left)
instance
proof standard
fix a b c :: ‹('a,'b) trace_class›
show ‹a + b + c = a + (b + c)›
apply transfer by auto
show ‹a + b = b + a›
apply transfer by auto
show ‹0 + a = a›
apply transfer by auto
show ‹- a + a = 0›
apply transfer by auto
show ‹a - b = a + - b›
apply transfer by auto
show ‹(*⇩R) r = ((*⇩C) (complex_of_real r) :: _ ⇒ ('a,'b) trace_class)› for r :: real
by (metis (mono_tags, opaque_lifting) Trace_Class.scaleC_trace_class_def Trace_Class.scaleR_trace_class_def id_apply map_fun_def o_def scaleR_scaleC)
show ‹r *⇩C (a + b) = r *⇩C a + r *⇩C b› for r :: complex
apply transfer
by (metis (no_types, lifting) scaleC_add_right)
show ‹(r + r') *⇩C a = r *⇩C a + r' *⇩C a› for r r' :: complex
apply transfer
by (metis (no_types, lifting) scaleC_add_left)
show ‹r *⇩C r' *⇩C a = (r * r') *⇩C a› for r r' :: complex
apply transfer by auto
show ‹1 *⇩C a = a›
apply transfer by auto
qed
end
lemma from_trace_class_0[simp]: ‹from_trace_class 0 = 0›
by (simp add: zero_trace_class.rep_eq)
lemma not_not_singleton_tc_zero:
‹x = 0› if ‹¬ class.not_singleton TYPE('a)› for x :: ‹('a::chilbert_space,'b::chilbert_space) trace_class›
apply transfer'
using that by (rule not_not_singleton_cblinfun_zero)
instantiation trace_class :: (chilbert_space, chilbert_space) "{complex_normed_vector}" begin
lift_definition norm_trace_class :: ‹('a,'b) trace_class ⇒ real› is trace_norm .
definition sgn_trace_class :: ‹('a,'b) trace_class ⇒ ('a,'b) trace_class› where ‹sgn_trace_class a = a /⇩R norm a›
definition dist_trace_class :: ‹('a,'b) trace_class ⇒ _ ⇒ _› where ‹dist_trace_class a b = norm (a - b)›
definition [code del]: "uniformity_trace_class = (INF e∈{0<..}. principal {(x::('a,'b) trace_class, y). dist x y < e})"
definition [code del]: "open_trace_class U = (∀x∈U. ∀⇩F (x', y) in INF e∈{0<..}. principal {(x, y). dist x y < e}. x' = x ⟶ y ∈ U)" for U :: "('a,'b) trace_class set"
instance
proof standard
fix a b :: ‹('a,'b) trace_class›
show ‹dist a b = norm (a - b)›
by (metis (no_types, lifting) Trace_Class.dist_trace_class_def)
show ‹uniformity = (INF e∈{0<..}. principal {(x :: ('a,'b) trace_class, y). dist x y < e})›
by (simp add: uniformity_trace_class_def)
show ‹open U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)› for U :: ‹('a,'b) trace_class set›
by (smt (verit, del_insts) case_prod_beta' eventually_mono open_trace_class_def uniformity_trace_class_def)
show ‹(norm a = 0) = (a = 0)›
apply transfer
by (auto simp add: trace_norm_nondegenerate)
show ‹norm (a + b) ≤ norm a + norm b›
apply transfer
by (auto simp: trace_norm_triangle)
show ‹norm (r *⇩C a) = cmod r * norm a› for r
apply transfer
by (auto simp: trace_norm_scaleC)
then show ‹norm (r *⇩R a) = ¦r¦ * norm a› for r
by (metis norm_of_real scaleR_scaleC)
show ‹sgn a = a /⇩R norm a›
by (simp add: sgn_trace_class_def)
qed
end
lemma trace_norm_comp_right:
fixes a :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space› and b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b›
assumes ‹trace_class b›
shows ‹trace_norm (a o⇩C⇩L b) ≤ norm a * trace_norm b›
proof -
define w w1 s where ‹w = polar_decomposition b› and ‹w1 = polar_decomposition (a o⇩C⇩L b)›
and ‹s = w1* o⇩C⇩L a o⇩C⇩L w›
have abs_ab: ‹abs_op (a o⇩C⇩L b) = s o⇩C⇩L abs_op b›
by (auto simp: w1_def w_def s_def cblinfun_compose_assoc polar_decomposition_correct polar_decomposition_correct')
have norm_s_t: ‹norm s ≤ norm a›
proof -
have ‹norm s ≤ norm (w1* o⇩C⇩L a) * norm w›
by (simp add: norm_cblinfun_compose s_def)
also have ‹… ≤ norm (w1*) * norm a * norm w›
by (metis mult.commute mult_left_mono norm_cblinfun_compose norm_ge_zero)
also have ‹… ≤ norm a›
by (metis (no_types, opaque_lifting) dual_order.refl mult.commute mult.right_neutral mult_zero_left norm_adj norm_ge_zero norm_partial_isometry norm_zero polar_decomposition_partial_isometry w1_def w_def)
finally show ?thesis
by -
qed
have ‹trace_norm (a o⇩C⇩L b) = cmod (trace (abs_op (a o⇩C⇩L b)))›
by simp
also have ‹… = cmod (trace (s o⇩C⇩L abs_op b))›
using abs_ab by presburger
also have ‹… ≤ norm s * trace_norm (abs_op b)›
using assms by (simp add: cmod_trace_times)
also from norm_s_t have ‹… ≤ norm a * trace_norm b›
by (metis abs_op_idem mult_right_mono of_real_eq_iff trace_abs_op trace_norm_nneg)
finally show ?thesis
by -
qed
lemma trace_norm_comp_left:
fixes a :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space› and b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b›
assumes [simp]: ‹trace_class a›
shows ‹trace_norm (a o⇩C⇩L b) ≤ trace_norm a * norm b›
proof -
have ‹trace_norm (b* o⇩C⇩L a*) ≤ norm (b*) * trace_norm (a*)›
apply (rule trace_norm_comp_right)
by simp
then have ‹trace_norm ((b* o⇩C⇩L a*)*) ≤ norm b * trace_norm a›
by (simp del: adj_cblinfun_compose)
then show ?thesis
by (simp add: mult.commute)
qed
lemma bounded_clinear_trace_duality: ‹trace_class t ⟹ bounded_clinear (λa. trace (t o⇩C⇩L a))›
apply (rule bounded_clinearI[where K=‹trace_norm t›])
apply (auto simp add: cblinfun_compose_add_right trace_class_comp_left trace_plus trace_scaleC)[2]
by (metis circularity_of_trace order_trans trace_leq_trace_norm trace_norm_comp_right)
lemma trace_class_butterfly[simp]: ‹trace_class (butterfly x y)› for x :: ‹'a::chilbert_space› and y :: ‹'b::chilbert_space›
unfolding butterfly_def
apply (rule trace_class_comp_left)
by simp
lemma trace_adj: ‹trace (a*) = cnj (trace a)›
by (metis Complex_Inner_Product0.complex_inner_1_right cinner_zero_right double_adj is_onb_some_chilbert_basis is_orthogonal_sym trace_adj_prelim trace_alt_def trace_class_adj)
hide_fact trace_adj_prelim
lemma cmod_trace_times': ‹cmod (trace (a o⇩C⇩L b)) ≤ norm b * trace_norm a› if ‹trace_class a›
apply (subst asm_rl[of ‹a o⇩C⇩L b = (b* o⇩C⇩L a*)*›], simp)
apply (subst trace_adj)
using cmod_trace_times[of ‹a*› ‹b*›]
by (auto intro!: that trace_class_adj hilbert_schmidt_comp_right hilbert_schmidt_adj simp del: adj_cblinfun_compose)
lift_definition iso_trace_class_compact_op_dual' :: ‹('a::chilbert_space,'b::chilbert_space) trace_class ⇒ ('b,'a) compact_op ⇒⇩C⇩L complex› is
‹λt c. trace (from_compact_op c o⇩C⇩L t)›
proof (rename_tac t)
include lifting_syntax
fix t :: ‹'a ⇒⇩C⇩L 'b›
assume ‹t ∈ Collect trace_class›
then have [simp]: ‹trace_class t›
by simp
have ‹cmod (trace (from_compact_op x o⇩C⇩L t)) ≤ norm x * trace_norm t› for x
by (metis ‹trace_class t› cmod_trace_times from_compact_op_norm)
then show ‹bounded_clinear (λc. trace (from_compact_op c o⇩C⇩L t))›
apply (rule_tac bounded_clinearI[where K=‹trace_norm t›])
by (auto simp: from_compact_op_plus from_compact_op_scaleC cblinfun_compose_add_right
cblinfun_compose_add_left trace_plus trace_class_comp_right trace_scaleC)
qed
lemma iso_trace_class_compact_op_dual'_apply: ‹iso_trace_class_compact_op_dual' t c = trace (from_compact_op c o⇩C⇩L from_trace_class t)›
by (simp add: iso_trace_class_compact_op_dual'.rep_eq)
lemma iso_trace_class_compact_op_dual'_plus: ‹iso_trace_class_compact_op_dual' (a + b) = iso_trace_class_compact_op_dual' a + iso_trace_class_compact_op_dual' b›
apply transfer
by (simp add: cblinfun_compose_add_right trace_class_comp_right trace_plus)
lemma iso_trace_class_compact_op_dual'_scaleC: ‹iso_trace_class_compact_op_dual' (c *⇩C a) = c *⇩C iso_trace_class_compact_op_dual' a›
apply transfer
by (simp add: trace_scaleC)
lemma iso_trace_class_compact_op_dual'_bounded_clinear[bounded_clinear, simp]:
‹bounded_clinear (iso_trace_class_compact_op_dual' :: ('a::chilbert_space,'b::chilbert_space) trace_class ⇒ _)›
proof -
let ?iso = ‹iso_trace_class_compact_op_dual' :: ('a,'b) trace_class ⇒ _›
have ‹norm (?iso t) ≤ norm t› for t
proof (rule norm_cblinfun_bound)
show ‹norm t ≥ 0› by simp
fix c
show ‹cmod (iso_trace_class_compact_op_dual' t *⇩V c) ≤ norm t * norm c›
apply (transfer fixing: c)
apply simp
by (metis cmod_trace_times from_compact_op_norm ordered_field_class.sign_simps(5))
qed
then show ‹bounded_clinear ?iso›
apply (rule_tac bounded_clinearI[where K=1])
by (auto simp: iso_trace_class_compact_op_dual'_plus iso_trace_class_compact_op_dual'_scaleC)
qed
lemma iso_trace_class_compact_op_dual'_surjective[simp]:
‹surj (iso_trace_class_compact_op_dual' :: ('a::chilbert_space,'b::chilbert_space) trace_class ⇒ _)›
proof -
let ?iso = ‹iso_trace_class_compact_op_dual' :: ('a,'b) trace_class ⇒ _›
have ‹∃A. Φ = ?iso A› for Φ :: ‹('b, 'a) compact_op ⇒⇩C⇩L complex›
proof -
define p where ‹p x y = Φ (butterfly_co y x)› for x y
have norm_p: ‹norm (p x y) ≤ norm Φ * norm x * norm y› for x y
proof -
have ‹norm (p x y) ≤ norm Φ * norm (butterfly_co y x)›
by (auto simp: p_def norm_cblinfun)
also have ‹… = norm Φ * norm (butterfly y x)›
apply transfer by simp
also have ‹… = norm Φ * norm x * norm y›
by (simp add: norm_butterfly)
finally show ?thesis
by -
qed
have [simp]: ‹bounded_sesquilinear p›
apply (rule bounded_sesquilinear.intro)
using norm_p
by (auto
intro!: exI[of _ ‹norm Φ›]
simp add: p_def butterfly_co_add_left butterfly_co_add_right complex_vector.linear_add
cblinfun.scaleC_right cblinfun.scaleC_left ab_semigroup_mult_class.mult_ac)
define A where ‹A = (the_riesz_rep_sesqui p)*›
then have xAy: ‹x ∙⇩C (A y) = p x y› for x y
by (simp add: cinner_adj_right the_riesz_rep_sesqui_apply)
have ΦC: ‹Φ C = trace (from_compact_op C o⇩C⇩L A)› if ‹finite_rank (from_compact_op C)› for C
proof -
from that
obtain x y and n :: nat where C_sum: ‹from_compact_op C = (∑i<n. butterfly (y i) (x i))›
apply atomize_elim by (rule finite_rank_sum_butterfly)
then have ‹C = (∑i<n. butterfly_co (y i) (x i))›
apply transfer by simp
then have ‹Φ C = (∑i<n. Φ *⇩V butterfly_co (y i) (x i))›
using cblinfun.sum_right by blast
also have ‹… = (∑i<n. p (x i) (y i))›
using p_def by presburger
also have ‹… = (∑i<n. (x i) ∙⇩C (A (y i)))›
using xAy by presburger
also have ‹… = (∑i<n. trace (butterfly (y i) (x i) o⇩C⇩L A))›
by (simp add: trace_butterfly_comp)
also have ‹… = trace ((∑i<n. butterfly (y i) (x i)) o⇩C⇩L A)›
by (metis (mono_tags, lifting) cblinfun_compose_sum_left sum.cong trace_class_butterfly trace_class_comp_left trace_sum)
also have ‹… = trace (from_compact_op C o⇩C⇩L A)›
using C_sum by presburger
finally show ?thesis
by -
qed
have ‹trace_class A›
proof (rule trace_classI)
show ‹is_onb some_chilbert_basis›
by simp
define W where ‹W = polar_decomposition A›
have ‹norm (W*) ≤ 1›
by (metis W_def nle_le norm_adj norm_partial_isometry norm_zero not_one_le_zero polar_decomposition_partial_isometry)
have ‹(∑x∈E. cmod (x ∙⇩C (abs_op A *⇩V x))) ≤ norm Φ› if ‹finite E› and ‹E ⊆ some_chilbert_basis› for E
proof -
define CE where ‹CE = (∑x∈E. (butterfly x x))›
from ‹E ⊆ some_chilbert_basis›
have ‹norm CE ≤ 1›
by (auto intro!: sum_butterfly_is_Proj norm_is_Proj is_normal_some_chilbert_basis simp: CE_def is_ortho_set_antimono)
have ‹(∑x∈E. cmod (x ∙⇩C (abs_op A *⇩V x))) = cmod (∑x∈E. x ∙⇩C (abs_op A *⇩V x))›
apply (rule sum_cmod_pos)
by (simp add: cinner_pos_if_pos)
also have ‹… = cmod (∑x∈E. (W *⇩V x) ∙⇩C (A *⇩V x))›
apply (rule arg_cong, rule sum.cong, simp)
by (metis W_def cblinfun_apply_cblinfun_compose cinner_adj_right polar_decomposition_correct')
also have ‹… = cmod (∑x∈E. Φ (butterfly_co x (W x)))›
apply (rule arg_cong, rule sum.cong, simp)
by (simp flip: p_def xAy)
also have ‹… = cmod (Φ (∑x∈E. butterfly_co x (W x)))›
by (simp add: cblinfun.sum_right)
also have ‹… ≤ norm Φ * norm (∑x∈E. butterfly_co x (W x))›
using norm_cblinfun by blast
also have ‹… = norm Φ * norm (∑x∈E. butterfly x (W x))›
apply transfer by simp
also have ‹… = norm Φ * norm (∑x∈E. (butterfly x x o⇩C⇩L W*))›
apply (rule arg_cong, rule sum.cong, simp)
by (simp add: butterfly_comp_cblinfun)
also have ‹… = norm Φ * norm (CE o⇩C⇩L W*)›
by (simp add: CE_def cblinfun_compose_sum_left)
also have ‹… ≤ norm Φ›
apply (rule mult_left_le, simp_all)
using ‹norm CE ≤ 1› ‹norm (W*) ≤ 1›
by (metis mult_le_one norm_cblinfun_compose norm_ge_zero order_trans)
finally show ?thesis
by -
qed
then show ‹(λx. x ∙⇩C (abs_op A *⇩V x)) abs_summable_on some_chilbert_basis›
apply (rule_tac nonneg_bdd_above_summable_on)
by (auto intro!: bdd_aboveI2)
qed
then obtain A' where A': ‹A = from_trace_class A'›
using from_trace_class_cases by blast
from ΦC have ΦC': ‹Φ C = ?iso A' C› if ‹finite_rank (from_compact_op C)› for C
by (simp add: that iso_trace_class_compact_op_dual'_apply A')
have ‹Φ = ?iso A'›
apply (unfold cblinfun_apply_inject[symmetric])
apply (rule finite_rank_separating_on_compact_op)
using ΦC' by (auto intro!: cblinfun.bounded_clinear_right)
then show ?thesis
by auto
qed
then show ?thesis
by auto
qed
lemma iso_trace_class_compact_op_dual'_isometric[simp]:
‹norm (iso_trace_class_compact_op_dual' t) = norm t› for t :: ‹('a::chilbert_space, 'b::chilbert_space) trace_class›
proof -
let ?iso = ‹iso_trace_class_compact_op_dual' :: ('a,'b) trace_class ⇒ _›
have ‹norm (?iso t) ≤ norm t› for t
proof (rule norm_cblinfun_bound)
show ‹norm t ≥ 0› by simp
fix c
show ‹cmod (iso_trace_class_compact_op_dual' t *⇩V c) ≤ norm t * norm c›
apply (transfer fixing: c)
apply simp
by (metis cmod_trace_times from_compact_op_norm ordered_field_class.sign_simps(5))
qed
moreover have ‹norm (?iso t) ≥ norm t› for t
proof -
define s where ‹s E = (∑e∈E. cmod (e ∙⇩C (abs_op (from_trace_class t) *⇩V e)))› for E
have bound: ‹norm (?iso t) ≥ s E› if ‹finite E› and ‹E ⊆ some_chilbert_basis› for E
proof -
text ‹Partial duplication from the proof of @{thm [source] iso_trace_class_compact_op_dual'_surjective}.
In Conway's text, this subproof occurs only once. However, it did not become clear to use how this works:
It seems that Conway's proof only implies that \<^const>‹iso_trace_class_compact_op_dual'› is isometric on
the subset of trace-class operators \<^term>‹A› constructed in that proof, but not necessarily on others (if \<^const>‹iso_trace_class_compact_op_dual'› were non-injective, there might be others)›
define A Φ where ‹A = from_trace_class t› and ‹Φ = ?iso t›
define W where ‹W = polar_decomposition A›
have ‹norm (W*) ≤ 1›
by (metis W_def nle_le norm_adj norm_partial_isometry norm_zero not_one_le_zero polar_decomposition_partial_isometry)
define CE where ‹CE = (∑x∈E. (butterfly x x))›
from ‹E ⊆ some_chilbert_basis›
have ‹norm CE ≤ 1›
by (auto intro!: sum_butterfly_is_Proj norm_is_Proj is_normal_some_chilbert_basis simp: CE_def is_ortho_set_antimono)
have ‹s E = (∑x∈E. cmod (x ∙⇩C (abs_op A *⇩V x)))›
using A_def s_def by blast
also have ‹… = cmod (∑x∈E. x ∙⇩C (abs_op A *⇩V x))›
apply (rule sum_cmod_pos)
by (simp add: cinner_pos_if_pos)
also have ‹… = cmod (∑x∈E. (W *⇩V x) ∙⇩C (A *⇩V x))›
apply (rule arg_cong, rule sum.cong, simp)
by (metis W_def cblinfun_apply_cblinfun_compose cinner_adj_right polar_decomposition_correct')
also have ‹… = cmod (∑x∈E. Φ (butterfly_co x (W x)))›
apply (rule arg_cong, rule sum.cong, simp)
by (auto simp: Φ_def iso_trace_class_compact_op_dual'_apply butterfly_co.rep_eq trace_butterfly_comp
simp flip: A_def)
also have ‹… = cmod (Φ (∑x∈E. butterfly_co x (W x)))›
by (simp add: cblinfun.sum_right)
also have ‹… ≤ norm Φ * norm (∑x∈E. butterfly_co x (W x))›
using norm_cblinfun by blast
also have ‹… = norm Φ * norm (∑x∈E. butterfly x (W x))›
apply transfer by simp
also have ‹… = norm Φ * norm (∑x∈E. (butterfly x x o⇩C⇩L W*))›
apply (rule arg_cong, rule sum.cong, simp)
by (simp add: butterfly_comp_cblinfun)
also have ‹… = norm Φ * norm (CE o⇩C⇩L W*)›
by (simp add: CE_def cblinfun_compose_sum_left)
also have ‹… ≤ norm Φ›
apply (rule mult_left_le, simp_all)
using ‹norm CE ≤ 1› ‹norm (W*) ≤ 1›
by (metis mult_le_one norm_cblinfun_compose norm_ge_zero order_trans)
finally show ?thesis
by (simp add: Φ_def)
qed
have ‹trace_class (from_trace_class t)› and ‹norm t = trace_norm (from_trace_class t)›
using from_trace_class
by (auto simp add: norm_trace_class.rep_eq)
then have ‹((λe. cmod (e ∙⇩C (abs_op (from_trace_class t) *⇩V e))) has_sum norm t) some_chilbert_basis›
by (metis (no_types, lifting) has_sum_cong has_sum_infsum is_onb_some_chilbert_basis trace_class_def trace_norm_alt_def trace_norm_basis_invariance)
then have lim: ‹(s ⤏ norm t) (finite_subsets_at_top some_chilbert_basis)›
by (simp add: filterlim_iff has_sum_def s_def)
show ?thesis
using _ _ lim apply (rule tendsto_le)
by (auto intro!: tendsto_const eventually_finite_subsets_at_top_weakI bound)
qed
ultimately show ?thesis
using nle_le by blast
qed
instance trace_class :: (chilbert_space, chilbert_space) cbanach
proof
let ?UNIVc = ‹UNIV :: (('b,'a) compact_op ⇒⇩C⇩L complex) set›
let ?UNIVt = ‹UNIV :: ('a,'b) trace_class set›
let ?iso = ‹iso_trace_class_compact_op_dual' :: ('a,'b) trace_class ⇒ _›
have lin_inv[simp]: ‹bounded_clinear (inv ?iso)›
apply (rule bounded_clinear_inv[where b=1])
by auto
have [simp]: ‹inj ?iso›
proof (rule injI)
fix x y assume ‹?iso x = ?iso y›
then have ‹norm (?iso (x - y)) = 0›
by (metis (no_types, opaque_lifting) add_diff_cancel_left diff_self iso_trace_class_compact_op_dual'_isometric iso_trace_class_compact_op_dual'_plus norm_eq_zero ordered_field_class.sign_simps(12))
then have ‹norm (x - y) = 0›
by simp
then show ‹x = y›
by simp
qed
have norm_inv[simp]: ‹norm (inv ?iso x) = norm x› for x
by (metis iso_trace_class_compact_op_dual'_isometric iso_trace_class_compact_op_dual'_surjective surj_f_inv_f)
have ‹complete ?UNIVc›
by (simp add: complete_UNIV)
then have ‹complete (inv ?iso ` ?UNIVc)›
apply (rule complete_isometric_image[rotated 4, where e=1])
by (auto simp: bounded_clinear.bounded_linear)
then have ‹complete ?UNIVt›
by (simp add: inj_imp_surj_inv)
then show ‹Cauchy X ⟹ convergent X› for X :: ‹nat ⇒ ('a, 'b) trace_class›
by (simp add: complete_def convergent_def)
qed
lemma trace_norm_geq_cinner_abs_op: ‹ψ ∙⇩C (abs_op t *⇩V ψ) ≤ trace_norm t› if ‹trace_class t› and ‹norm ψ = 1›
proof -
have ‹∃B. {ψ} ⊆ B ∧ is_onb B›
apply (rule orthonormal_basis_exists)
using ‹norm ψ = 1›
by auto
then obtain B where ‹is_onb B› and ‹ψ ∈ B›
by auto
have ‹ψ ∙⇩C (abs_op t *⇩V ψ) = (∑⇩∞ψ∈{ψ}. ψ ∙⇩C (abs_op t *⇩V ψ))›
by simp
also have ‹… ≤ (∑⇩∞ψ∈B. ψ ∙⇩C (abs_op t *⇩V ψ))›
apply (rule infsum_mono_neutral_complex)
using ‹ψ ∈ B› ‹is_onb B› that
by (auto simp add: trace_exists cinner_pos_if_pos)
also have ‹… = trace_norm t›
using ‹is_onb B› that
by (metis trace_abs_op trace_alt_def trace_class_abs_op)
finally show ?thesis
by -
qed
lemma norm_leq_trace_norm: ‹norm t ≤ trace_norm t› if ‹trace_class t›
for t :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
wlog not_singleton: ‹class.not_singleton TYPE('a)›
using not_not_singleton_cblinfun_zero[of t] negation by simp
note cblinfun_norm_approx_witness' = cblinfun_norm_approx_witness[internalize_sort' 'a, OF complex_normed_vector_axioms not_singleton]
show ?thesis
proof (rule field_le_epsilon)
fix ε :: real assume ‹ε > 0›
define δ :: real where
‹δ = min (sqrt (ε / 2)) (ε / (4 * (norm (sqrt_op (abs_op t)) + 1)))›
have ‹δ > 0›
using ‹ε > 0› apply (auto simp add: δ_def)
by (smt (verit) norm_not_less_zero zero_less_divide_iff)
have δ_small: ‹δ⇧2 + 2 * norm (sqrt_op (abs_op t)) * δ ≤ ε›
proof -
define n where ‹n = norm (sqrt_op (abs_op t))›
then have ‹n ≥ 0›
by simp
have δ: ‹δ = min (sqrt (ε / 2)) (ε / (4 * (n + 1)))›
by (simp add: δ_def n_def)
have ‹δ⇧2 + 2 * n * δ ≤ ε / 2 + 2 * n * δ›
apply (rule add_right_mono)
apply (subst δ) apply (subst min_power_distrib_left)
using ‹ε > 0› ‹n ≥ 0› by auto
also have ‹… ≤ ε / 2 + 2 * n * (ε / (4 * (n + 1)))›
apply (intro add_left_mono mult_left_mono)
by (simp_all add: δ ‹n ≥ 0›)
also have ‹… = ε / 2 + 2 * (n / (n+1)) * (ε / 4)›
by simp
also have ‹… ≤ ε / 2 + 2 * 1 * (ε / 4)›
apply (intro add_left_mono mult_left_mono mult_right_mono)
using ‹n ≥ 0› ‹ε > 0› by auto
also have ‹… = ε›
by simp
finally show ‹δ⇧2 + 2 * n * δ ≤ ε›
by -
qed
from ‹δ > 0› obtain ψ where ψε: ‹norm (sqrt_op (abs_op t)) - δ ≤ norm (sqrt_op (abs_op t) *⇩V ψ)› and ‹norm ψ = 1›
apply atomize_elim by (rule cblinfun_norm_approx_witness')
have aux1: ‹2 * complex_of_real x = complex_of_real (2 * x)› for x
by simp
have ‹complex_of_real (norm t) = norm (abs_op t)›
by simp
also have ‹… = (norm (sqrt_op (abs_op t)))⇧2›
by (simp add: positive_selfadjointI[unfolded selfadjoint_def] flip: norm_AadjA)
also have ‹… ≤ (norm (sqrt_op (abs_op t) *⇩V ψ) + δ)⇧2›
by (smt (verit) ψε complex_of_real_mono norm_triangle_ineq4 norm_triangle_sub pos2 power_strict_mono)
also have ‹… = (norm (sqrt_op (abs_op t) *⇩V ψ))⇧2 + δ⇧2 + 2 * norm (sqrt_op (abs_op t) *⇩V ψ) * δ›
by (simp add: power2_sum)
also have ‹… ≤ (norm (sqrt_op (abs_op t) *⇩V ψ))⇧2 + δ⇧2 + 2 * norm (sqrt_op (abs_op t)) * δ›
apply (rule complex_of_real_mono_iff[THEN iffD2])
by (smt (z3) ‹0 < δ› ‹norm ψ = 1› more_arith_simps(11) mult_less_cancel_right_disj norm_cblinfun one_power2 power2_eq_square)
also have ‹… ≤ (norm (sqrt_op (abs_op t) *⇩V ψ))⇧2 + ε›
apply (rule complex_of_real_mono_iff[THEN iffD2])
using δ_small by auto
also have ‹… = ((sqrt_op (abs_op t) *⇩V ψ) ∙⇩C (sqrt_op (abs_op t) *⇩V ψ)) + ε›
by (simp add: cdot_square_norm)
also have ‹… = (ψ ∙⇩C (abs_op t *⇩V ψ)) + ε›
by (simp add: positive_selfadjointI[unfolded selfadjoint_def] flip: cinner_adj_right cblinfun_apply_cblinfun_compose)
also have ‹… ≤ trace_norm t + ε›
using ‹norm ψ = 1› ‹trace_class t› by (auto simp add: trace_norm_geq_cinner_abs_op)
finally show ‹norm t ≤ trace_norm t + ε›
using complex_of_real_mono_iff by blast
qed
qed
lemma clinear_from_trace_class[iff]: ‹clinear from_trace_class›
apply (rule clinearI; transfer)
by auto
lemma bounded_clinear_from_trace_class[bounded_clinear]:
‹bounded_clinear (from_trace_class :: ('a::chilbert_space,'b::chilbert_space) trace_class ⇒ _)›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
apply (rule bounded_clinearI[where K=1]; transfer)
by (auto intro!: norm_leq_trace_norm[internalize_sort' 'a] chilbert_space_axioms True)
next
case False
then have zero: ‹A = 0› for A :: ‹'a ⇒⇩C⇩L 'b›
by (rule not_not_singleton_cblinfun_zero)
show ?thesis
apply (rule bounded_clinearI[where K=1])
by (subst zero, simp)+
qed
instantiation trace_class :: (chilbert_space, chilbert_space) order begin
lift_definition less_eq_trace_class :: ‹('a, 'b) trace_class ⇒ ('a, 'b) trace_class ⇒ bool› is
less_eq.
lift_definition less_trace_class :: ‹('a, 'b) trace_class ⇒ ('a, 'b) trace_class ⇒ bool› is
less.
instance
apply intro_classes
apply (auto simp add: less_eq_trace_class.rep_eq less_trace_class.rep_eq)
by (simp add: from_trace_class_inject)
end
lift_definition compose_tcl :: ‹('a::chilbert_space, 'b::chilbert_space) trace_class ⇒ ('c::chilbert_space ⇒⇩C⇩L 'a) ⇒ ('c,'b) trace_class› is
‹cblinfun_compose :: 'a ⇒⇩C⇩L 'b ⇒ 'c ⇒⇩C⇩L 'a ⇒ 'c ⇒⇩C⇩L 'b›
by (simp add: trace_class_comp_left)
lift_definition compose_tcr :: ‹('a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space) ⇒ ('c::chilbert_space, 'a) trace_class ⇒ ('c,'b) trace_class› is
‹cblinfun_compose :: 'a ⇒⇩C⇩L 'b ⇒ 'c ⇒⇩C⇩L 'a ⇒ 'c ⇒⇩C⇩L 'b›
by (simp add: trace_class_comp_right)
lemma norm_compose_tcl: ‹norm (compose_tcl a b) ≤ norm a * norm b›
by (auto intro!: trace_norm_comp_left simp: norm_trace_class.rep_eq compose_tcl.rep_eq)
lemma norm_compose_tcr: ‹norm (compose_tcr a b) ≤ norm a * norm b›
by (auto intro!: trace_norm_comp_right simp: norm_trace_class.rep_eq compose_tcr.rep_eq)
interpretation compose_tcl: bounded_cbilinear compose_tcl
proof (intro bounded_cbilinear.intro exI[of _ 1] allI)
fix a a' :: ‹('a,'b) trace_class› and b b' :: ‹'c ⇒⇩C⇩L 'a› and r :: complex
show ‹compose_tcl (a + a') b = compose_tcl a b + compose_tcl a' b›
apply transfer
by (simp add: cblinfun_compose_add_left)
show ‹compose_tcl a (b + b') = compose_tcl a b + compose_tcl a b'›
apply transfer
by (simp add: cblinfun_compose_add_right)
show ‹compose_tcl (r *⇩C a) b = r *⇩C compose_tcl a b›
apply transfer
by simp
show ‹compose_tcl a (r *⇩C b) = r *⇩C compose_tcl a b›
apply transfer
by simp
show ‹norm (compose_tcl a b) ≤ norm a * norm b * 1›
by (simp add: norm_compose_tcl)
qed
interpretation compose_tcr: bounded_cbilinear compose_tcr
proof (intro bounded_cbilinear.intro exI[of _ 1] allI)
fix a a' :: ‹'a ⇒⇩C⇩L 'b› and b b' :: ‹('c,'a) trace_class› and r :: complex
show ‹compose_tcr (a + a') b = compose_tcr a b + compose_tcr a' b›
apply transfer
by (simp add: cblinfun_compose_add_left)
show ‹compose_tcr a (b + b') = compose_tcr a b + compose_tcr a b'›
apply transfer
by (simp add: cblinfun_compose_add_right)
show ‹compose_tcr (r *⇩C a) b = r *⇩C compose_tcr a b›
apply transfer
by simp
show ‹compose_tcr a (r *⇩C b) = r *⇩C compose_tcr a b›
apply transfer
by simp
show ‹norm (compose_tcr a b) ≤ norm a * norm b * 1›
by (simp add: norm_compose_tcr)
qed
lemma trace_norm_sandwich: ‹trace_norm (sandwich e t) ≤ (norm e)^2 * trace_norm t› if ‹trace_class t›
apply (simp add: sandwich_apply)
by (smt (z3) Groups.mult_ac(2) more_arith_simps(11) mult_left_mono norm_adj norm_ge_zero power2_eq_square that trace_class_comp_right trace_norm_comp_left trace_norm_comp_right)
lemma trace_class_sandwich: ‹trace_class b ⟹ trace_class (sandwich a b)›
by (simp add: sandwich_apply trace_class_comp_right trace_class_comp_left)
definition ‹sandwich_tc e t = compose_tcl (compose_tcr e t) (e*)›
lemma sandwich_tc_transfer[transfer_rule]:
includes lifting_syntax
shows ‹((=) ===> cr_trace_class ===> cr_trace_class) (λe. (*⇩V) (sandwich e)) sandwich_tc›
by (auto intro!: rel_funI simp: sandwich_tc_def cr_trace_class_def compose_tcl.rep_eq compose_tcr.rep_eq sandwich_apply)
lemma from_trace_class_sandwich_tc:
‹from_trace_class (sandwich_tc e t) = sandwich e (from_trace_class t)›
apply transfer
by (rule sandwich_apply)
lemma norm_sandwich_tc: ‹norm (sandwich_tc e t) ≤ (norm e)^2 * norm t›
by (simp add: norm_trace_class.rep_eq from_trace_class_sandwich_tc trace_norm_sandwich)
lemma sandwich_tc_pos: ‹sandwich_tc e t ≥ 0› if ‹t ≥ 0›
using that apply (transfer fixing: e)
by (simp add: sandwich_pos)
lemma sandwich_tc_scaleC_right: ‹sandwich_tc e (c *⇩C t) = c *⇩C sandwich_tc e t›
apply (transfer fixing: e c)
by (simp add: cblinfun.scaleC_right)
lemma sandwich_tc_plus: ‹sandwich_tc e (t + u) = sandwich_tc e t + sandwich_tc e u›
by (simp add: sandwich_tc_def compose_tcr.add_right compose_tcl.add_left)
lemma sandwich_tc_minus: ‹sandwich_tc e (t - u) = sandwich_tc e t - sandwich_tc e u›
by (simp add: sandwich_tc_def compose_tcr.diff_right compose_tcl.diff_left)
lemma sandwich_tc_uminus_right: ‹sandwich_tc e (- t) = - sandwich_tc e t›
by (metis (no_types, lifting) add.right_inverse arith_simps(50) diff_0 group_cancel.sub1 sandwich_tc_minus)
lemma trace_comp_pos:
fixes a b :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹trace_class b›
assumes ‹a ≥ 0› and ‹b ≥ 0›
shows ‹trace (a o⇩C⇩L b) ≥ 0›
proof -
obtain c :: ‹'a ⇒⇩C⇩L 'a› where ‹a = c* o⇩C⇩L c›
by (metis assms(2) positive_selfadjointI sqrt_op_pos sqrt_op_square selfadjoint_def)
then have ‹trace (a o⇩C⇩L b) = trace (sandwich c b)›
by (simp add: sandwich_apply assms(1) cblinfun_assoc_left(1) circularity_of_trace trace_class_comp_right)
also have ‹… ≥ 0›
by (auto intro!: trace_pos sandwich_pos assms)
finally show ?thesis
by -
qed
lemma trace_norm_one_dim: ‹trace_norm x = cmod (one_dim_iso x)›
apply (rule of_real_eq_iff[where 'a=complex, THEN iffD1])
apply (simp add: abs_op_one_dim flip: trace_abs_op)
by (simp add: abs_complex_def)
lemma trace_norm_bounded:
fixes A B :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹A ≥ 0› and ‹trace_class B›
assumes ‹A ≤ B›
shows ‹trace_class A›
proof -
have ‹(λx. x ∙⇩C (B *⇩V x)) abs_summable_on some_chilbert_basis›
by (metis assms(2) is_onb_some_chilbert_basis summable_on_iff_abs_summable_on_complex trace_exists)
then have ‹(λx. x ∙⇩C (A *⇩V x)) abs_summable_on some_chilbert_basis›
apply (rule abs_summable_on_comparison_test)
using ‹A ≥ 0› ‹A ≤ B›
by (auto intro!: cmod_mono cinner_pos_if_pos simp: abs_op_id_on_pos less_eq_cblinfun_def)
then show ?thesis
by (auto intro!: trace_classI[OF is_onb_some_chilbert_basis] simp: abs_op_id_on_pos ‹A ≥ 0›)
qed
lemma trace_norm_cblinfun_mono:
fixes A B :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹A ≥ 0› and ‹trace_class B›
assumes ‹A ≤ B›
shows ‹trace_norm A ≤ trace_norm B›
proof -
from assms have ‹trace_class A›
by (rule trace_norm_bounded)
from ‹A ≤ B› and ‹A ≥ 0›
have ‹B ≥ 0›
by simp
have ‹cmod (x ∙⇩C (abs_op A *⇩V x)) ≤ cmod (x ∙⇩C (abs_op B *⇩V x))› for x
using ‹A ≤ B›
unfolding less_eq_cblinfun_def
using ‹A ≥ 0› ‹B ≥ 0›
by (auto intro!: cmod_mono cinner_pos_if_pos simp: abs_op_id_on_pos)
then show ‹trace_norm A ≤ trace_norm B›
using ‹trace_class A› ‹trace_class B›
by (auto intro!: infsum_mono
simp add: trace_norm_def trace_class_iff_summable[OF is_onb_some_chilbert_basis])
qed
lemma norm_cblinfun_mono_trace_class:
fixes A B :: ‹('a::chilbert_space, 'a) trace_class›
assumes ‹A ≥ 0›
assumes ‹A ≤ B›
shows ‹norm A ≤ norm B›
using assms
apply transfer
apply (rule trace_norm_cblinfun_mono)
by auto
lemma trace_norm_butterfly: ‹trace_norm (butterfly a b) = (norm a) * (norm b)›
for a b :: ‹_ :: chilbert_space›
proof -
have ‹trace_norm (butterfly a b) = trace (abs_op (butterfly a b))›
by (simp flip: trace_abs_op)
also have ‹… = (norm a / norm b) * trace (selfbutter b)›
by (simp add: abs_op_butterfly scaleR_scaleC trace_scaleC del: trace_abs_op)
also have ‹… = (norm a / norm b) * trace ((vector_to_cblinfun b :: complex ⇒⇩C⇩L _)* o⇩C⇩L vector_to_cblinfun b)›
apply (subst butterfly_def)
apply (subst circularity_of_trace)
by simp_all
also have ‹… = (norm a / norm b) * (b ∙⇩C b)›
by simp
also have ‹… = (norm a) * (norm b)›
by (simp add: cdot_square_norm power2_eq_square)
finally show ?thesis
using of_real_eq_iff by blast
qed
lemma from_trace_class_sum:
shows ‹from_trace_class (∑x∈M. f x) = (∑x∈M. from_trace_class (f x))›
apply (induction M rule:infinite_finite_induct)
by (simp_all add: plus_trace_class.rep_eq)
lemma has_sum_mono_neutral_traceclass:
fixes f :: "'a ⇒ ('b::chilbert_space, 'b) trace_class"
assumes ‹(f has_sum a) A› and "(g has_sum b) B"
assumes ‹⋀x. x ∈ A∩B ⟹ f x ≤ g x›
assumes ‹⋀x. x ∈ A-B ⟹ f x ≤ 0›
assumes ‹⋀x. x ∈ B-A ⟹ g x ≥ 0›
shows "a ≤ b"
proof -
from assms(1)
have ‹((λx. from_trace_class (f x)) has_sum from_trace_class a) A›
apply (rule Infinite_Sum.has_sum_bounded_linear[rotated])
by (intro bounded_clinear_from_trace_class bounded_clinear.bounded_linear)
moreover
from assms(2)
have ‹((λx. from_trace_class (g x)) has_sum from_trace_class b) B›
apply (rule Infinite_Sum.has_sum_bounded_linear[rotated])
by (intro bounded_clinear_from_trace_class bounded_clinear.bounded_linear)
ultimately have ‹from_trace_class a ≤ from_trace_class b›
apply (rule has_sum_mono_neutral_cblinfun)
using assms by (auto simp: less_eq_trace_class.rep_eq)
then show ?thesis
by (auto simp: less_eq_trace_class.rep_eq)
qed
lemma has_sum_mono_traceclass:
fixes f :: "'a ⇒ ('b::chilbert_space, 'b) trace_class"
assumes "(f has_sum x) A" and "(g has_sum y) A"
assumes ‹⋀x. x ∈ A ⟹ f x ≤ g x›
shows "x ≤ y"
using assms has_sum_mono_neutral_traceclass by force
lemma infsum_mono_traceclass:
fixes f :: "'a ⇒ ('b::chilbert_space, 'b) trace_class"
assumes "f summable_on A" and "g summable_on A"
assumes ‹⋀x. x ∈ A ⟹ f x ≤ g x›
shows "infsum f A ≤ infsum g A"
by (meson assms has_sum_infsum has_sum_mono_traceclass)
lemma infsum_mono_neutral_traceclass:
fixes f :: "'a ⇒ ('b::chilbert_space, 'b) trace_class"
assumes "f summable_on A" and "g summable_on B"
assumes ‹⋀x. x ∈ A∩B ⟹ f x ≤ g x›
assumes ‹⋀x. x ∈ A-B ⟹ f x ≤ 0›
assumes ‹⋀x. x ∈ B-A ⟹ g x ≥ 0›
shows "infsum f A ≤ infsum g B"
using assms(1) assms(2) assms(3) assms(4) assms(5) has_sum_mono_neutral_traceclass summable_iff_has_sum_infsum by blast
instance trace_class :: (chilbert_space, chilbert_space) ordered_complex_vector
apply (intro_classes; transfer)
by (auto intro!: scaleC_left_mono scaleC_right_mono)
lemma Abs_trace_class_geq0I: ‹0 ≤ Abs_trace_class t› if ‹trace_class t› and ‹t ≥ 0›
using that by (simp add: zero_trace_class.abs_eq less_eq_trace_class.abs_eq eq_onp_def)
lift_definition tc_compose :: ‹('b::chilbert_space, 'c::chilbert_space) trace_class
⇒ ('a::chilbert_space, 'b) trace_class ⇒ ('a,'c) trace_class› is
cblinfun_compose
by (simp add: trace_class_comp_left)
lemma norm_tc_compose:
‹norm (tc_compose a b) ≤ norm a * norm b›
proof transfer
fix a :: ‹'c ⇒⇩C⇩L 'b› and b :: ‹'a ⇒⇩C⇩L 'c›
assume ‹a ∈ Collect trace_class› and tc_b: ‹b ∈ Collect trace_class›
then have ‹trace_norm (a o⇩C⇩L b) ≤ trace_norm a * norm b›
by (simp add: trace_norm_comp_left)
also have ‹… ≤ trace_norm a * trace_norm b›
using tc_b by (auto intro!: mult_left_mono norm_leq_trace_norm)
finally show ‹trace_norm (a o⇩C⇩L b) ≤ trace_norm a * trace_norm b›
by -
qed
lift_definition trace_tc :: ‹('a::chilbert_space, 'a) trace_class ⇒ complex› is trace.
lemma trace_tc_plus: ‹trace_tc (a + b) = trace_tc a + trace_tc b›
apply transfer by (simp add: trace_plus)
lemma trace_tc_scaleC: ‹trace_tc (c *⇩C a) = c *⇩C trace_tc a›
apply transfer by (simp add: trace_scaleC)
lemma trace_tc_norm: ‹norm (trace_tc a) ≤ norm a›
apply transfer by auto
lemma bounded_clinear_trace_tc[bounded_clinear, simp]: ‹bounded_clinear trace_tc›
apply (rule bounded_clinearI[where K=1])
by (auto simp: trace_tc_scaleC trace_tc_plus intro!: trace_tc_norm)
lemma norm_tc_pos: ‹norm A = trace_tc A› if ‹A ≥ 0›
using that apply transfer by (simp add: trace_norm_pos)
lemma norm_tc_pos_Re: ‹norm A = Re (trace_tc A)› if ‹A ≥ 0›
using norm_tc_pos[OF that]
by (metis Re_complex_of_real)
lemma from_trace_class_pos: ‹from_trace_class A ≥ 0 ⟷ A ≥ 0›
by (simp add: less_eq_trace_class.rep_eq)
lemma infsum_tc_norm_bounded_abs_summable:
fixes A :: ‹'a ⇒ ('b::chilbert_space, 'b::chilbert_space) trace_class›
assumes pos: ‹⋀x. x ∈ M ⟹ A x ≥ 0›
assumes bound_B: ‹⋀F. finite F ⟹ F ⊆ M ⟹ norm (∑x∈F. A x) ≤ B›
shows ‹A abs_summable_on M›
proof -
have ‹(∑x∈F. norm (A x)) = norm (∑x∈F. A x)› if ‹F ⊆ M› for F
proof -
have ‹complex_of_real (∑x∈F. norm (A x)) = (∑x∈F. complex_of_real (trace_norm (from_trace_class (A x))))›
by (simp add: norm_trace_class.rep_eq trace_norm_pos)
also have ‹… = (∑x∈F. trace (from_trace_class (A x)))›
using that pos by (auto intro!: sum.cong simp add: trace_norm_pos less_eq_trace_class.rep_eq)
also have ‹… = trace (from_trace_class (∑x∈F. A x))›
by (simp add: from_trace_class_sum trace_sum)
also have ‹… = norm (∑x∈F. A x)›
by (smt (verit, ccfv_threshold) calculation norm_of_real norm_trace_class.rep_eq sum_norm_le trace_leq_trace_norm)
finally show ?thesis
using of_real_eq_iff by blast
qed
with bound_B have bound_B': ‹(∑x∈F. norm (A x)) ≤ B› if ‹finite F› and ‹F ⊆ M› for F
by (metis that(1) that(2))
then show ‹A abs_summable_on M›
apply (rule_tac nonneg_bdd_above_summable_on)
by (auto intro!: bdd_aboveI)
qed
lemma trace_norm_uminus[simp]: ‹trace_norm (-a) = trace_norm a›
by (metis abs_op_uminus of_real_eq_iff trace_abs_op)
lemma trace_norm_triangle_minus:
fixes a b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes [simp]: ‹trace_class a› ‹trace_class b›
shows ‹trace_norm (a - b) ≤ trace_norm a + trace_norm b›
using trace_norm_triangle[of a ‹-b›]
by auto
lemma trace_norm_abs_op[simp]: ‹trace_norm (abs_op t) = trace_norm t›
by (simp add: trace_norm_def)
lemma
fixes t :: ‹'a ⇒⇩C⇩L 'a::chilbert_space›
shows cblinfun_decomp_4pos: ‹
∃t1 t2 t3 t4.
t = t1 - t2 + 𝗂 *⇩C t3 - 𝗂 *⇩C t4
∧ t1 ≥ 0 ∧ t2 ≥ 0 ∧ t3 ≥ 0 ∧ t4 ≥ 0› (is ?thesis1)
and trace_class_decomp_4pos: ‹trace_class t ⟹
∃t1 t2 t3 t4.
t = t1 - t2 + 𝗂 *⇩C t3 - 𝗂 *⇩C t4
∧ trace_class t1 ∧ trace_class t2 ∧ trace_class t3 ∧ trace_class t4
∧ trace_norm t1 ≤ trace_norm t ∧ trace_norm t2 ≤ trace_norm t ∧ trace_norm t3 ≤ trace_norm t ∧ trace_norm t4 ≤ trace_norm t
∧ t1 ≥ 0 ∧ t2 ≥ 0 ∧ t3 ≥ 0 ∧ t4 ≥ 0› (is ‹_ ⟹ ?thesis2›)
proof -
define th ta where ‹th = (1/2) *⇩C (t + t*)› and ‹ta = (-𝗂/2) *⇩C (t - t*)›
have th_herm: ‹th* = th›
by (simp add: adj_plus th_def)
have ‹ta* = ta›
by (simp add: adj_minus ta_def scaleC_diff_right adj_uminus)
have ‹t = th + 𝗂 *⇩C ta›
by (smt (verit, ccfv_SIG) add.commute add.inverse_inverse complex_i_mult_minus complex_vector.vector_space_assms(1) complex_vector.vector_space_assms(3) diff_add_cancel group_cancel.add2 i_squared scaleC_half_double ta_def th_def times_divide_eq_right)
define t1 t2 where ‹t1 = (abs_op th + th) /⇩R 2› and ‹t2 = (abs_op th - th) /⇩R 2›
have ‹t1 ≥ 0›
using abs_op_geq_neq[unfolded selfadjoint_def, OF ‹th* = th›] ordered_field_class.sign_simps(15)
by (fastforce simp add: t1_def intro!: scaleR_nonneg_nonneg)
have ‹t2 ≥ 0›
using abs_op_geq[unfolded selfadjoint_def, OF ‹th* = th›] ordered_field_class.sign_simps(15)
by (fastforce simp add: t2_def intro!: scaleR_nonneg_nonneg)
have ‹th = t1 - t2›
apply (simp add: t1_def t2_def)
by (metis (no_types, opaque_lifting) Extra_Ordered_Fields.sign_simps(8) diff_add_cancel ordered_field_class.sign_simps(2) ordered_field_class.sign_simps(27) scaleR_half_double)
define t3 t4 where ‹t3 = (abs_op ta + ta) /⇩R 2› and ‹t4 = (abs_op ta - ta) /⇩R 2›
have ‹t3 ≥ 0›
using abs_op_geq_neq[unfolded selfadjoint_def, OF ‹ta* = ta›] ordered_field_class.sign_simps(15)
by (fastforce simp add: t3_def intro!: scaleR_nonneg_nonneg)
have ‹t4 ≥ 0›
using abs_op_geq[unfolded selfadjoint_def, OF ‹ta* = ta›] ordered_field_class.sign_simps(15)
by (fastforce simp add: t4_def intro!: scaleR_nonneg_nonneg)
have ‹ta = t3 - t4›
apply (simp add: t3_def t4_def)
by (metis (no_types, opaque_lifting) Extra_Ordered_Fields.sign_simps(8) diff_add_cancel ordered_field_class.sign_simps(2) ordered_field_class.sign_simps(27) scaleR_half_double)
have decomp: ‹t = t1 - t2 + 𝗂 *⇩C t3 - 𝗂 *⇩C t4›
by (simp add: ‹t = th + 𝗂 *⇩C ta› ‹th = t1 - t2› ‹ta = t3 - t4› scaleC_diff_right)
from decomp ‹t1 ≥ 0› ‹t2 ≥ 0› ‹t3 ≥ 0› ‹t4 ≥ 0›
show ?thesis1
by auto
show ?thesis2 if ‹trace_class t›
proof -
have ‹trace_class th› ‹trace_class ta›
by (auto simp add: th_def ta_def
intro!: ‹trace_class t› trace_class_scaleC trace_class_plus trace_class_minus trace_class_uminus trace_class_adj)
then have tc: ‹trace_class t1› ‹trace_class t2› ‹trace_class t3› ‹trace_class t4›
by (auto simp add: t1_def t2_def t3_def t4_def scaleR_scaleC intro!: trace_class_scaleC)
have tn_th: ‹trace_norm th ≤ trace_norm t›
using trace_norm_triangle[of t ‹t*›]
by (auto simp add: that th_def trace_norm_scaleC)
have tn_ta: ‹trace_norm ta ≤ trace_norm t›
using trace_norm_triangle_minus[of t ‹t*›]
by (auto simp add: that ta_def trace_norm_scaleC)
have tn1: ‹trace_norm t1 ≤ trace_norm t›
using trace_norm_triangle[of ‹abs_op th› th] tn_th
by (auto simp add: ‹trace_class th› t1_def trace_norm_scaleC scaleR_scaleC)
have tn2: ‹trace_norm t2 ≤ trace_norm t›
using trace_norm_triangle_minus[of ‹abs_op th› th] tn_th
by (auto simp add: ‹trace_class th› t2_def trace_norm_scaleC scaleR_scaleC)
have tn3: ‹trace_norm t3 ≤ trace_norm t›
using trace_norm_triangle[of ‹abs_op ta› ta] tn_ta
by (auto simp add: ‹trace_class ta› t3_def trace_norm_scaleC scaleR_scaleC)
have tn4: ‹trace_norm t4 ≤ trace_norm t›
using trace_norm_triangle_minus[of ‹abs_op ta› ta] tn_ta
by (auto simp add: ‹trace_class ta› t4_def trace_norm_scaleC scaleR_scaleC)
from decomp tc ‹t1 ≥ 0› ‹t2 ≥ 0› ‹t3 ≥ 0› ‹t4 ≥ 0› tn1 tn2 tn3 tn4
show ?thesis2
by auto
qed
qed
lemma trace_class_decomp_4pos':
fixes t :: ‹('a::chilbert_space,'a) trace_class›
shows ‹∃t1 t2 t3 t4.
t = t1 - t2 + 𝗂 *⇩C t3 - 𝗂 *⇩C t4
∧ norm t1 ≤ norm t ∧ norm t2 ≤ norm t ∧ norm t3 ≤ norm t ∧ norm t4 ≤ norm t
∧ t1 ≥ 0 ∧ t2 ≥ 0 ∧ t3 ≥ 0 ∧ t4 ≥ 0›
proof -
from trace_class_decomp_4pos[of ‹from_trace_class t›, OF trace_class_from_trace_class]
obtain t1' t2' t3' t4'
where *: ‹from_trace_class t = t1' - t2' + 𝗂 *⇩C t3' - 𝗂 *⇩C t4'
∧ trace_class t1' ∧ trace_class t2' ∧ trace_class t3' ∧ trace_class t4'
∧ trace_norm t1' ≤ trace_norm (from_trace_class t) ∧ trace_norm t2' ≤ trace_norm (from_trace_class t) ∧ trace_norm t3' ≤ trace_norm (from_trace_class t) ∧ trace_norm t4' ≤ trace_norm (from_trace_class t)
∧ t1' ≥ 0 ∧ t2' ≥ 0 ∧ t3' ≥ 0 ∧ t4' ≥ 0›
by auto
then obtain t1 t2 t3 t4 where
t1234: ‹t1' = from_trace_class t1› ‹t2' = from_trace_class t2› ‹t3' = from_trace_class t3› ‹t4' = from_trace_class t4›
by (metis from_trace_class_cases mem_Collect_eq)
with * have n1234: ‹norm t1 ≤ norm t› ‹norm t2 ≤ norm t› ‹norm t3 ≤ norm t› ‹norm t4 ≤ norm t›
by (metis norm_trace_class.rep_eq)+
have t_decomp: ‹t = t1 - t2 + 𝗂 *⇩C t3 - 𝗂 *⇩C t4›
using * unfolding t1234
by (auto simp: from_trace_class_inject
simp flip: scaleC_trace_class.rep_eq plus_trace_class.rep_eq minus_trace_class.rep_eq)
have pos1234: ‹t1 ≥ 0› ‹t2 ≥ 0› ‹t3 ≥ 0› ‹t4 ≥ 0›
using * unfolding t1234
by (auto simp: less_eq_trace_class_def)
from t_decomp pos1234 n1234
show ?thesis
by blast
qed
thm bounded_clinear_trace_duality
lemma bounded_clinear_trace_duality': ‹trace_class t ⟹ bounded_clinear (λa. trace (a o⇩C⇩L t))› for t :: ‹_::chilbert_space ⇒⇩C⇩L _::chilbert_space›
apply (rule bounded_clinearI[where K=‹trace_norm t›])
apply (auto simp add: cblinfun_compose_add_left trace_class_comp_right trace_plus trace_scaleC)[2]
by (metis circularity_of_trace order_trans trace_leq_trace_norm trace_norm_comp_right)
lemma infsum_nonneg_traceclass:
fixes f :: "'a ⇒ ('b::chilbert_space, 'b) trace_class"
assumes "⋀x. x ∈ M ⟹ 0 ≤ f x"
shows "infsum f M ≥ 0"
apply (cases ‹f summable_on M›)
apply (subst infsum_0_simp[symmetric])
apply (rule infsum_mono_neutral_traceclass)
using assms by (auto simp: infsum_not_exists)
lemma sandwich_tc_compose: ‹sandwich_tc (A o⇩C⇩L B) = sandwich_tc A o sandwich_tc B›
apply (rule ext)
apply (rule from_trace_class_inject[THEN iffD1])
apply (transfer fixing: A B)
by (simp add: sandwich_compose)
lemma sandwich_tc_0_left[simp]: ‹sandwich_tc 0 = 0›
by (auto intro!: ext simp add: sandwich_tc_def compose_tcl.zero_left compose_tcr.zero_left)
lemma sandwich_tc_0_right[simp]: ‹sandwich_tc e 0 = 0›
by (auto intro!: ext simp add: sandwich_tc_def compose_tcl.zero_left compose_tcr.zero_right)
lemma sandwich_tc_scaleC_left: ‹sandwich_tc (c *⇩C e) t = (cmod c)^2 *⇩C sandwich_tc e t›
apply (rule from_trace_class_inject[THEN iffD1])
by (simp add: from_trace_class_sandwich_tc scaleC_trace_class.rep_eq
sandwich_scaleC_left)
lemma sandwich_tc_scaleR_left: ‹sandwich_tc (r *⇩R e) t = r^2 *⇩R sandwich_tc e t›
by (simp add: scaleR_scaleC sandwich_tc_scaleC_left flip: of_real_power)
lemma bounded_cbilinear_tc_compose: ‹bounded_cbilinear tc_compose›
unfolding bounded_cbilinear_def
apply transfer
apply (auto intro!: exI[of _ 1] simp: cblinfun_compose_add_left cblinfun_compose_add_right)
by (meson norm_leq_trace_norm dual_order.trans mult_right_mono trace_norm_comp_right trace_norm_nneg)
lemmas bounded_clinear_tc_compose_left[bounded_clinear] = bounded_cbilinear.bounded_clinear_left[OF bounded_cbilinear_tc_compose]
lemmas bounded_clinear_tc_compose_right[bounded_clinear] = bounded_cbilinear.bounded_clinear_right[OF bounded_cbilinear_tc_compose]
lift_definition tc_butterfly :: ‹'a::chilbert_space ⇒ 'b::chilbert_space ⇒ ('b,'a) trace_class›
is butterfly
by simp
lemma norm_tc_butterfly: ‹norm (tc_butterfly ψ φ) = norm ψ * norm φ›
apply (transfer fixing: ψ φ)
by (simp add: trace_norm_butterfly)
lemma trace_tc_butterfly: ‹trace_tc (tc_butterfly x y) = y ∙⇩C x›
apply (transfer fixing: x y)
by (rule trace_butterfly)
lemma comp_tc_butterfly[simp]: ‹tc_compose (tc_butterfly a b) (tc_butterfly c d) = (b ∙⇩C c) *⇩C tc_butterfly a d›
apply transfer'
by simp
lemma tc_butterfly_pos[simp]: ‹0 ≤ tc_butterfly ψ ψ›
apply transfer
by simp
lift_definition rank1_tc :: ‹('a::chilbert_space, 'b::chilbert_space) trace_class ⇒ bool› is rank1.
lift_definition finite_rank_tc :: ‹('a::chilbert_space, 'b::chilbert_space) trace_class ⇒ bool› is finite_rank.
lemma finite_rank_tc_0[iff]: ‹finite_rank_tc 0›
apply transfer by simp
lemma finite_rank_tc_plus: ‹finite_rank_tc (a + b)›
if ‹finite_rank_tc a› and ‹finite_rank_tc b›
using that apply transfer
by simp
lemma finite_rank_tc_scale: ‹finite_rank_tc (c *⇩C a)› if ‹finite_rank_tc a›
using that apply transfer by simp
lemma csubspace_finite_rank_tc: ‹csubspace (Collect finite_rank_tc)›
apply (rule complex_vector.subspaceI)
by (auto intro!: finite_rank_tc_plus finite_rank_tc_scale)
lemma rank1_trace_class: ‹trace_class a› if ‹rank1 a›
for a b :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
using that by (auto intro!: simp: rank1_iff_butterfly)
lemma finite_rank_trace_class: ‹trace_class a› if ‹finite_rank a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
from ‹finite_rank a› obtain F f where ‹finite F› and ‹F ⊆ Collect rank1›
and a_def: ‹a = (∑x∈F. f x *⇩C x)›
by (smt (verit, ccfv_threshold) complex_vector.span_explicit finite_rank_def mem_Collect_eq)
then show ‹trace_class a›
unfolding a_def
apply induction
by (auto intro!: trace_class_plus trace_class_scaleC intro: rank1_trace_class)
qed
lemma trace_minus:
assumes ‹trace_class a› ‹trace_class b›
shows ‹trace (a - b) = trace a - trace b›
by (metis (no_types, lifting) add_uminus_conv_diff assms(1) assms(2) trace_class_uminus trace_plus trace_uminus)
lemma trace_cblinfun_mono:
fixes A B :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹trace_class A› and ‹trace_class B›
assumes ‹A ≤ B›
shows ‹trace A ≤ trace B›
proof -
have sumA: ‹(λe. e ∙⇩C (A *⇩V e)) summable_on some_chilbert_basis›
by (auto intro!: trace_exists assms)
moreover have sumB: ‹(λe. e ∙⇩C (B *⇩V e)) summable_on some_chilbert_basis›
by (auto intro!: trace_exists assms)
moreover have ‹x ∙⇩C (A *⇩V x) ≤ x ∙⇩C (B *⇩V x)› for x
using assms(3) less_eq_cblinfun_def by blast
ultimately have ‹(∑⇩∞e∈some_chilbert_basis. e ∙⇩C (A *⇩V e)) ≤ (∑⇩∞e∈some_chilbert_basis. e ∙⇩C (B *⇩V e))›
by (rule infsum_mono_complex)
then show ?thesis
by (metis assms(1) assms(2) assms(3) diff_ge_0_iff_ge trace_minus trace_pos)
qed
lemma trace_tc_mono:
assumes ‹A ≤ B›
shows ‹trace_tc A ≤ trace_tc B›
using assms
apply transfer
by (simp add: trace_cblinfun_mono)
lemma trace_tc_0[simp]: ‹trace_tc 0 = 0›
apply transfer' by simp
lemma cspan_tc_transfer[transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_trace_class ===> rel_set cr_trace_class) cspan cspan›
proof (intro rel_funI rel_setI)
fix B :: ‹('a ⇒⇩C⇩L 'b) set› and C
assume ‹rel_set cr_trace_class B C›
then have BC: ‹B = from_trace_class ` C›
by (auto intro!: simp: cr_trace_class_def image_iff rel_set_def)
show ‹∃t∈cspan C. cr_trace_class a t› if ‹a ∈ cspan B› for a
proof -
from that obtain F f where ‹finite F› and ‹F ⊆ B› and a_sum: ‹a = (∑x∈F. f x *⇩C x)›
by (auto simp: complex_vector.span_explicit)
from ‹F ⊆ B›
obtain F' where ‹F' ⊆ C› and FF': ‹F = from_trace_class ` F'›
by (auto elim!: subset_imageE simp: BC)
define t where ‹t = (∑x∈F'. f (from_trace_class x) *⇩C x)›
have ‹a = from_trace_class t›
by (simp add: a_sum t_def from_trace_class_sum scaleC_trace_class.rep_eq FF'
sum.reindex o_def from_trace_class_inject inj_on_def)
moreover have ‹t ∈ cspan C›
by (metis (no_types, lifting) ‹F' ⊆ C› complex_vector.span_clauses(4) complex_vector.span_sum complex_vector.span_superset subsetD t_def)
ultimately show ‹∃t∈cspan C. cr_trace_class a t›
by (auto simp: cr_trace_class_def)
qed
show ‹∃a∈cspan B. cr_trace_class a t› if ‹t ∈ cspan C› for t
proof -
from that obtain F f where ‹finite F› and ‹F ⊆ C› and t_sum: ‹t = (∑x∈F. f x *⇩C x)›
by (auto simp: complex_vector.span_explicit)
define a where ‹a = (∑x∈F. f x *⇩C from_trace_class x)›
then have ‹a = from_trace_class t›
by (simp add: t_sum a_def from_trace_class_sum scaleC_trace_class.rep_eq)
moreover have ‹a ∈ cspan B›
using BC ‹F ⊆ C›
by (auto intro!: complex_vector.span_base complex_vector.span_sum complex_vector.span_scale simp: a_def)
ultimately show ?thesis
by (auto simp: cr_trace_class_def)
qed
qed
lemma finite_rank_tc_def': ‹finite_rank_tc A ⟷ A ∈ cspan (Collect rank1_tc)›
apply transfer'
apply (auto simp: finite_rank_def)
apply (metis (no_types, lifting) Collect_cong rank1_trace_class)
by (metis (no_types, lifting) Collect_cong rank1_trace_class)
lemma tc_butterfly_add_left: ‹tc_butterfly (a + a') b = tc_butterfly a b + tc_butterfly a' b›
apply transfer
by (rule butterfly_add_left)
lemma tc_butterfly_add_right: ‹tc_butterfly a (b + b') = tc_butterfly a b + tc_butterfly a b'›
apply transfer
by (rule butterfly_add_right)
lemma tc_butterfly_sum_left: ‹tc_butterfly (∑i∈M. ψ i) φ = (∑i∈M. tc_butterfly (ψ i) φ)›
apply transfer
by (rule butterfly_sum_left)
lemma tc_butterfly_sum_right: ‹tc_butterfly ψ (∑i∈M. φ i) = (∑i∈M. tc_butterfly ψ (φ i))›
apply transfer
by (rule butterfly_sum_right)
lemma tc_butterfly_scaleC_left[simp]: "tc_butterfly (c *⇩C ψ) φ = c *⇩C tc_butterfly ψ φ"
apply transfer by simp
lemma tc_butterfly_scaleC_right[simp]: "tc_butterfly ψ (c *⇩C φ) = cnj c *⇩C tc_butterfly ψ φ"
apply transfer by simp
lemma bounded_sesquilinear_tc_butterfly[iff]: ‹bounded_sesquilinear (λa b. tc_butterfly b a)›
by (auto intro!: bounded_sesquilinear.intro exI[of _ 1]
simp: tc_butterfly_add_left tc_butterfly_add_right norm_tc_butterfly)
lemma trace_norm_plus_orthogonal:
assumes ‹trace_class a› and ‹trace_class b›
assumes ‹a* o⇩C⇩L b = 0› and ‹a o⇩C⇩L b* = 0›
shows ‹trace_norm (a + b) = trace_norm a + trace_norm b›
proof -
have ‹trace_norm (a + b) = trace (abs_op (a + b))›
by simp
also have ‹… = trace (abs_op a + abs_op b)›
by (simp add: abs_op_plus_orthogonal assms)
also have ‹… = trace (abs_op a) + trace (abs_op b)›
by (simp add: assms trace_plus)
also have ‹… = trace_norm a + trace_norm b›
by simp
finally show ?thesis
using of_real_eq_iff by blast
qed
lemma norm_tc_plus_orthogonal:
assumes ‹tc_compose (adj_tc a) b = 0› and ‹tc_compose a (adj_tc b) = 0›
shows ‹norm (a + b) = norm a + norm b›
using assms apply transfer
by (auto intro!: trace_norm_plus_orthogonal)
lemma trace_norm_sum_exchange:
fixes t :: ‹_ ⇒ (_::chilbert_space ⇒⇩C⇩L _::chilbert_space)›
assumes ‹⋀i. i ∈ F ⟹ trace_class (t i)›
assumes ‹⋀i j. i ∈ F ⟹ j ∈ F ⟹ i ≠ j ⟹ (t i)* o⇩C⇩L t j = 0›
assumes ‹⋀i j. i ∈ F ⟹ j ∈ F ⟹ i ≠ j ⟹ t i o⇩C⇩L (t j)* = 0›
shows ‹trace_norm (∑i∈F. t i) = (∑i∈F. trace_norm (t i))›
proof (insert assms, induction F rule:infinite_finite_induct)
case (infinite A)
then show ?case
by simp
next
case empty
show ?case
by simp
next
case (insert x F)
have ‹trace_norm (∑i∈insert x F. t i) = trace_norm (t x + (∑x∈F. t x))›
by (simp add: insert)
also have ‹… = trace_norm (t x) + trace_norm (∑x∈F. t x)›
proof (rule trace_norm_plus_orthogonal)
show ‹trace_class (t x)›
by (simp add: insert.prems)
show ‹trace_class (∑x∈F. t x)›
by (simp add: trace_class_sum insert.prems)
show ‹t x* o⇩C⇩L (∑x∈F. t x) = 0›
by (auto intro!: sum.neutral insert.prems simp: cblinfun_compose_sum_right sum_adj insert.hyps)
show ‹t x o⇩C⇩L (∑x∈F. t x)* = 0›
by (auto intro!: sum.neutral insert.prems simp: cblinfun_compose_sum_right sum_adj insert.hyps)
qed
also have ‹… = trace_norm (t x) + (∑x∈F. trace_norm (t x))›
apply (subst insert.IH)
by (simp_all add: insert.prems)
also have ‹… = (∑i∈insert x F. trace_norm (t i))›
by (simp add: insert)
finally show ?case
by -
qed
lemma norm_tc_sum_exchange:
assumes ‹⋀i j. i ∈ F ⟹ j ∈ F ⟹ i ≠ j ⟹ tc_compose (adj_tc (t i)) (t j) = 0›
assumes ‹⋀i j. i ∈ F ⟹ j ∈ F ⟹ i ≠ j ⟹ tc_compose (t i) (adj_tc (t j)) = 0›
shows ‹norm (∑i∈F. t i) = (∑i∈F. norm (t i))›
using assms apply transfer
by (auto intro!: trace_norm_sum_exchange)
instantiation trace_class :: (one_dim, one_dim) complex_inner begin
lift_definition cinner_trace_class :: ‹('a, 'b) trace_class ⇒ ('a, 'b) trace_class ⇒ complex› is ‹(∙⇩C)›.
instance
proof intro_classes
fix x y z :: ‹('a, 'b) trace_class›
show ‹x ∙⇩C y = cnj (y ∙⇩C x)›
apply transfer'
by simp
show ‹(x + y) ∙⇩C z = x ∙⇩C z + y ∙⇩C z›
apply transfer'
by (simp add: cinner_simps)
show ‹r *⇩C x ∙⇩C y = cnj r * (x ∙⇩C y)› for r
apply (transfer' fixing: r)
using cinner_simps by blast
show ‹0 ≤ x ∙⇩C x›
apply transfer'
by simp
show ‹(x ∙⇩C x = 0) = (x = 0)›
apply transfer'
by auto
show ‹norm x = sqrt (cmod (x ∙⇩C x))›
proof transfer'
fix x :: ‹'a ⇒⇩C⇩L 'b›
define c :: complex where ‹c = one_dim_iso x›
then have xc: ‹x = c *⇩C 1›
by simp
have ‹trace_norm x = norm c›
by (simp add: trace_norm_one_dim xc)
also have ‹norm c = sqrt (cmod (x ∙⇩C x))›
by (metis inner_real_def norm_eq_sqrt_cinner norm_one norm_scaleC real_inner_1_right xc)
finally show ‹trace_norm x = sqrt (cmod (x ∙⇩C x)) ›
by (simp add: cinner_cblinfun_def)
qed
qed
end
instantiation trace_class :: (one_dim, one_dim) one_dim begin
lift_definition one_trace_class :: ‹('a, 'b) trace_class› is 1
by auto
lift_definition times_trace_class :: ‹('a, 'b) trace_class ⇒ ('a, 'b) trace_class ⇒ ('a, 'b) trace_class› is ‹(*)›
by auto
lift_definition divide_trace_class :: ‹('a, 'b) trace_class ⇒ ('a, 'b) trace_class ⇒ ('a, 'b) trace_class› is ‹(/)›
by auto
lift_definition inverse_trace_class :: ‹('a, 'b) trace_class ⇒ ('a, 'b) trace_class› is ‹Fields.inverse›
by auto
definition canonical_basis_trace_class :: ‹('a, 'b) trace_class list› where ‹canonical_basis_trace_class = [1]›
definition canonical_basis_length_trace_class :: ‹('a, 'b) trace_class itself ⇒ nat› where ‹canonical_basis_length_trace_class = 1›
instance
proof intro_classes
fix x y z :: ‹('a, 'b) trace_class›
have [simp]: ‹1 ≠ (0 :: ('a, 'b) trace_class)›
using one_trace_class.rep_eq by force
then have [simp]: ‹0 ≠ (1 :: ('a, 'b) trace_class)›
by force
show ‹distinct (canonical_basis :: (_,_) trace_class list)›
by (simp add: canonical_basis_trace_class_def)
show ‹cindependent (set canonical_basis :: (_,_) trace_class set)›
by (simp add: canonical_basis_trace_class_def)
show ‹canonical_basis_length TYPE(('a, 'b) trace_class) = length (canonical_basis :: (_,_) trace_class list)›
by (simp add: canonical_basis_length_trace_class_def canonical_basis_trace_class_def)
show ‹x ∈ set canonical_basis ⟹ norm x = 1›
apply (simp add: canonical_basis_trace_class_def)
by (smt (verit, ccfv_threshold) one_trace_class_def cinner_trace_class.abs_eq cnorm_eq_1 one_cinner_one one_trace_class.rsp)
show ‹canonical_basis = [1 :: ('a,'b) trace_class]›
by (simp add: canonical_basis_trace_class_def)
show ‹a *⇩C 1 * b *⇩C 1 = (a * b) *⇩C (1 :: ('a,'b) trace_class)› for a b :: complex
apply (transfer' fixing: a b)
by simp
show ‹x div y = x * inverse y›
apply transfer'
by (simp add: divide_cblinfun_def)
show ‹inverse (a *⇩C 1 :: ('a,'b) trace_class) = 1 /⇩C a› for a :: complex
apply transfer'
by simp
show ‹is_ortho_set (set canonical_basis :: ('a,'b) trace_class set)›
by (simp add: is_ortho_set_def canonical_basis_trace_class_def)
show ‹cspan (set canonical_basis :: ('a,'b) trace_class set) = UNIV›
proof (intro Set.set_eqI iffI UNIV_I)
fix x :: ‹('a,'b) trace_class›
have ‹∃c. y = c *⇩C 1› for y :: ‹'a ⇒⇩C⇩L 'b›
apply (rule exI[where x=‹one_dim_iso y›])
by simp
then obtain c where ‹x = c *⇩C 1›
apply transfer'
by auto
then show ‹x ∈ cspan (set canonical_basis)›
by (auto intro!: complex_vector.span_base complex_vector.span_clauses
simp: canonical_basis_trace_class_def)
qed
qed
end
lemma from_trace_class_one_dim_iso[simp]: ‹from_trace_class = one_dim_iso›
proof (rule ext)
fix x:: ‹('a, 'b) trace_class›
have ‹from_trace_class x = from_trace_class (one_dim_iso x *⇩C 1)›
by simp
also have ‹… = one_dim_iso x *⇩C from_trace_class 1›
using scaleC_trace_class.rep_eq by blast
also have ‹… = one_dim_iso x *⇩C 1›
by (simp add: one_trace_class.rep_eq)
also have ‹… = one_dim_iso x›
by simp
finally show ‹from_trace_class x = one_dim_iso x›
by -
qed
lemma trace_tc_one_dim_iso[simp]: ‹trace_tc = one_dim_iso›
by (simp add: trace_tc.rep_eq[abs_def])
lemma compose_tcr_id_left[simp]: ‹compose_tcr id_cblinfun t = t›
by (auto intro!: from_trace_class_inject[THEN iffD1] simp: compose_tcr.rep_eq)
lemma compose_tcl_id_right[simp]: ‹compose_tcl t id_cblinfun = t›
by (auto intro!: from_trace_class_inject[THEN iffD1] simp: compose_tcl.rep_eq)
lemma sandwich_tc_id_cblinfun[simp]: ‹sandwich_tc id_cblinfun t = t›
by (simp add: from_trace_class_inverse sandwich_tc_def)
lemma bounded_clinear_sandwich_tc[bounded_clinear]: ‹bounded_clinear (sandwich_tc e)›
using norm_sandwich_tc[of e]
by (auto intro!: bounded_clinearI[where K=‹(norm e)⇧2›]
simp: sandwich_tc_plus sandwich_tc_scaleC_right cross3_simps)
lemma trace_class_Proj: ‹trace_class (Proj S) ⟷ finite_dim_ccsubspace S›
proof -
define C where ‹C = some_onb_of S›
then obtain B where ‹is_onb B› and ‹C ⊆ B›
using orthonormal_basis_exists some_onb_of_norm1 by blast
have card_C: ‹card C = cdim (space_as_set S)›
by (simp add: C_def some_onb_of_card)
have S_C: ‹S = ccspan C›
by (simp add: C_def)
from ‹is_onb B›
have ‹trace_class (Proj S) ⟷ ((λx. x ∙⇩C (abs_op (Proj S) *⇩V x)) abs_summable_on B)›
by (rule trace_class_iff_summable)
also have ‹… ⟷ ((λx. cmod (x ∙⇩C (Proj S *⇩V x))) abs_summable_on B)›
by simp
also have ‹… ⟷ ((λx. 1::real) abs_summable_on C)›
proof (rule summable_on_cong_neutral)
fix x :: 'a
show ‹norm 1 = 0› if ‹x ∈ C - B›
using that ‹C ⊆ B› by auto
show ‹norm (cmod (x ∙⇩C (Proj S *⇩V x))) = norm (1::real)› if ‹x ∈ B ∩ C›
apply (subst Proj_fixes_image)
using C_def Int_absorb1 that ‹is_onb B›
by (auto simp: is_onb_def cnorm_eq_1)
show ‹norm (cmod (x ∙⇩C (Proj S *⇩V x))) = 0› if ‹x ∈ B - C›
apply (subst Proj_0_compl)
apply (subst S_C)
apply (rule mem_ortho_ccspanI)
using that ‹is_onb B› ‹C ⊆ B›
by (force simp: is_onb_def is_ortho_set_def)+
qed
also have ‹… ⟷ finite C›
using infsum_diverge_constant[where A=C and c=‹1::real›]
by auto
also have ‹… ⟷ finite_dim_ccsubspace S›
by (metis C_def S_C ccspan_finite_dim some_onb_of_finite_dim)
finally show ?thesis
by -
qed
lemma not_trace_class_trace0: ‹trace a = 0› if ‹¬ trace_class a›
using that by (simp add: trace_def)
lemma trace_Proj: ‹trace (Proj S) = cdim (space_as_set S)›
proof (cases ‹finite_dim_ccsubspace S›)
case True
define C where ‹C = some_onb_of S›
then obtain B where ‹is_onb B› and ‹C ⊆ B›
using orthonormal_basis_exists some_onb_of_norm1 by blast
have [simp]: ‹finite C›
using C_def True some_onb_of_finite_dim by blast
have card_C: ‹card C = cdim (space_as_set S)›
by (simp add: C_def some_onb_of_card)
have S_C: ‹S = ccspan C›
by (simp add: C_def)
from True have ‹trace_class (Proj S)›
by (simp add: trace_class_Proj)
with ‹is_onb B› have ‹((λe. e ∙⇩C (Proj S *⇩V e)) has_sum trace (Proj S)) B›
by (rule trace_has_sum)
then have ‹((λe. 1) has_sum trace (Proj S)) C›
proof (rule has_sum_cong_neutral[THEN iffD1, rotated -1])
fix x :: 'a
show ‹1 = 0› if ‹x ∈ C - B›
using that ‹C ⊆ B› by auto
show ‹x ∙⇩C (Proj S *⇩V x) = 1› if ‹x ∈ B ∩ C›
apply (subst Proj_fixes_image)
using C_def Int_absorb1 that ‹is_onb B›
by (auto simp: is_onb_def cnorm_eq_1)
show ‹is_orthogonal x (Proj S *⇩V x)› if ‹x ∈ B - C›
apply (subst Proj_0_compl)
apply (subst S_C)
apply (rule mem_ortho_ccspanI)
using that ‹is_onb B› ‹C ⊆ B›
by (force simp: is_onb_def is_ortho_set_def)+
qed
then have ‹trace (Proj S) = card C›
using has_sum_constant[OF ‹finite C›, of 1]
apply simp
using has_sum_unique by blast
also have ‹… = cdim (space_as_set S)›
using card_C by presburger
finally show ?thesis
by -
next
case False
then have ‹¬ trace_class (Proj S)›
using trace_class_Proj by blast
then have ‹trace (Proj S) = 0›
by (rule not_trace_class_trace0)
moreover from False have ‹cdim (space_as_set S) = 0›
apply transfer
by (simp add: cdim_infinite_0)
ultimately show ?thesis
by simp
qed
lemma trace_tc_pos: ‹t ≥ 0 ⟹ trace_tc t ≥ 0›
using trace_tc_mono by fastforce
lift_definition tc_apply :: ‹('a::chilbert_space,'b::chilbert_space) trace_class ⇒ 'a ⇒ 'b› is cblinfun_apply.
lemma bounded_cbilinear_tc_apply: ‹bounded_cbilinear tc_apply›
apply (rule bounded_cbilinear.intro; transfer)
apply (auto intro!: exI[of _ 1] cblinfun.add_left cblinfun.add_right cblinfun.scaleC_right)
by (smt (verit, del_insts) mult_right_mono norm_cblinfun norm_ge_zero norm_leq_trace_norm)
lift_definition diagonal_operator_tc :: ‹('a ⇒ complex) ⇒ ('a ell2, 'a ell2) trace_class› is
‹λf. if f abs_summable_on UNIV then diagonal_operator f else 0›
proof (rule CollectI)
fix f :: ‹'a ⇒ complex›
show ‹trace_class (if f abs_summable_on UNIV then diagonal_operator f else 0)›
proof (cases ‹f abs_summable_on UNIV›)
case True
have bdd: ‹bdd_above (range (λx. cmod (f x)))›
proof (rule bdd_aboveI2)
fix x
have ‹cmod (f x) = (∑⇩∞x∈{x}. cmod (f x))›
by simp
also have ‹… ≤ (∑⇩∞x. cmod (f x))›
apply (rule infsum_mono_neutral)
by (auto intro!: True)
finally show ‹cmod (f x) ≤ (∑⇩∞x. cmod (f x))›
by -
qed
have ‹trace_class (diagonal_operator f)›
by (auto intro!: trace_classI[OF is_onb_ket] summable_on_reindex[THEN iffD2] True
simp: abs_op_diagonal_operator o_def diagonal_operator_ket bdd)
with True show ?thesis
by simp
next
case False
then show ?thesis
by simp
qed
qed
lemma from_trace_class_diagonal_operator_tc:
assumes ‹f abs_summable_on UNIV›
shows ‹from_trace_class (diagonal_operator_tc f) = diagonal_operator f›
apply (transfer fixing: f)
using assms by simp
lemma tc_butterfly_scaleC_summable:
fixes f :: ‹'a ⇒ complex›
assumes ‹f abs_summable_on A›
shows ‹(λx. f x *⇩C tc_butterfly (ket x) (ket x)) summable_on A›
proof -
define M where ‹M = (∑⇩∞x∈A. norm (f x))›
have ‹(∑x∈F. cmod (f x) * norm (tc_butterfly (ket x) (ket x))) ≤ M› if ‹finite F› and ‹F ⊆ A› for F
proof -
have ‹(∑x∈F. norm (f x) * norm (tc_butterfly (ket x) (ket x))) = (∑x∈F. norm (f x))›
by (simp add: norm_tc_butterfly)
also have ‹… ≤ (∑⇩∞x∈A. norm (f x))›
using assms finite_sum_le_infsum norm_ge_zero that(1) that(2) by blast
also have ‹… = M›
by (simp add: M_def)
finally show ?thesis
by -
qed
then have ‹(λx. norm (f x *⇩C tc_butterfly (ket x) (ket x))) abs_summable_on A›
apply (intro nonneg_bdd_above_summable_on bdd_aboveI)
by auto
then show ?thesis
by (auto intro: abs_summable_summable)
qed
lemma tc_butterfly_scaleC_has_sum:
fixes f :: ‹'a ⇒ complex›
assumes ‹f abs_summable_on UNIV›
shows ‹((λx. f x *⇩C tc_butterfly (ket x) (ket x)) has_sum diagonal_operator_tc f) UNIV›
proof -
define D where ‹D = (∑⇩∞x. f x *⇩C tc_butterfly (ket x) (ket x))›
have bdd_f: ‹bdd_above (range (λx. cmod (f x)))›
by (metis assms summable_on_bdd_above_real)
have ‹ket y ∙⇩C from_trace_class D (ket z) = ket y ∙⇩C from_trace_class (diagonal_operator_tc f) (ket z)› for y z
proof -
have blin_tc_apply: ‹bounded_linear (λa. tc_apply a (ket z))›
by (intro bounded_clinear.bounded_linear bounded_cbilinear.bounded_clinear_left bounded_cbilinear_tc_apply)
have summ: ‹(λx. f x *⇩C tc_butterfly (ket x) (ket x)) summable_on UNIV›
by (intro tc_butterfly_scaleC_summable assms)
have ‹((λx. f x *⇩C tc_butterfly (ket x) (ket x)) has_sum D) UNIV›
by (simp add: D_def summ)
with blin_tc_apply have ‹((λx. tc_apply (f x *⇩C tc_butterfly (ket x) (ket x)) (ket z)) has_sum tc_apply D (ket z)) UNIV›
by (rule Infinite_Sum.has_sum_bounded_linear)
then have ‹((λx. ket y ∙⇩C tc_apply (f x *⇩C tc_butterfly (ket x) (ket x)) (ket z)) has_sum ket y ∙⇩C tc_apply D (ket z)) UNIV›
by (smt (verit, best) has_sum_cong has_sum_imp_summable has_sum_infsum infsumI infsum_cinner_left summable_on_cinner_left)
then have ‹((λx. of_bool (x=y) * of_bool (y=z) * f y) has_sum ket y ∙⇩C tc_apply D (ket z)) UNIV›
apply (rule has_sum_cong[THEN iffD2, rotated])
by (auto intro!: simp: tc_apply.rep_eq scaleC_trace_class.rep_eq tc_butterfly.rep_eq)
then have ‹((λx. of_bool (y=z) * f y) has_sum ket y ∙⇩C tc_apply D (ket z)) {y}›
apply (rule has_sum_cong_neutral[THEN iffD2, rotated -1])
by auto
then have ‹ket y ∙⇩C tc_apply D (ket z) = of_bool (y=z) * f y›
by simp
also have ‹… = ket y ∙⇩C from_trace_class (diagonal_operator_tc f) (ket z)›
by (simp add: diagonal_operator_tc.rep_eq assms diagonal_operator_ket bdd_f)
finally show ?thesis
by (simp add: tc_apply.rep_eq)
qed
then have ‹from_trace_class D = from_trace_class (diagonal_operator_tc f)›
by (auto intro!: equal_ket cinner_ket_eqI)
then have ‹D = diagonal_operator_tc f›
by (simp add: from_trace_class_inject)
with tc_butterfly_scaleC_summable[OF assms]
show ?thesis
using D_def by force
qed
lemma diagonal_operator_tc_invalid: ‹¬ f abs_summable_on UNIV ⟹ diagonal_operator_tc f = 0›
apply (transfer fixing: f) by simp
lemma tc_butterfly_scaleC_infsum:
fixes f :: ‹'a ⇒ complex›
shows ‹(∑⇩∞x. f x *⇩C tc_butterfly (ket x) (ket x)) = diagonal_operator_tc f›
proof (cases ‹f abs_summable_on UNIV›)
case True
then show ?thesis
using infsumI tc_butterfly_scaleC_has_sum by fastforce
next
case False
then have [simp]: ‹diagonal_operator_tc f = 0›
apply (transfer fixing: f) by simp
have ‹¬ (λx. f x *⇩C tc_butterfly (ket x) (ket x)) summable_on UNIV›
proof (rule notI)
assume ‹(λx. f x *⇩C tc_butterfly (ket x) (ket x)) summable_on UNIV›
then have ‹(λx. trace_tc (f x *⇩C tc_butterfly (ket x) (ket x))) summable_on UNIV›
apply (rule summable_on_bounded_linear[rotated])
by (simp add: bounded_clinear.bounded_linear)
then have ‹f summable_on UNIV›
apply (rule summable_on_cong[THEN iffD1, rotated])
apply (transfer' fixing: f)
by (simp add: trace_scaleC trace_butterfly)
with False
show False
by (metis summable_on_iff_abs_summable_on_complex)
qed
then have [simp]: ‹(∑⇩∞x. f x *⇩C tc_butterfly (ket x) (ket x)) = 0›
using infsum_not_exists by blast
show ?thesis
by simp
qed
lemma from_trace_class_abs_summable: ‹f abs_summable_on X ⟹ (λx. from_trace_class (f x)) abs_summable_on X›
apply (rule abs_summable_on_comparison_test[where g=‹f›])
by (simp_all add: norm_leq_trace_norm norm_trace_class.rep_eq)
lemma from_trace_class_summable: ‹f summable_on X ⟹ (λx. from_trace_class (f x)) summable_on X›
apply (rule Infinite_Sum.summable_on_bounded_linear[where h=from_trace_class])
by (simp_all add: bounded_clinear.bounded_linear bounded_clinear_from_trace_class)
lemma from_trace_class_infsum:
assumes ‹f summable_on UNIV›
shows ‹from_trace_class (∑⇩∞x. f x) = (∑⇩∞x. from_trace_class (f x))›
apply (rule infsum_bounded_linear_strong[symmetric])
using assms
by (auto intro!: bounded_clinear.bounded_linear bounded_clinear_from_trace_class from_trace_class_summable)
lemma cspan_trace_class:
‹cspan (Collect trace_class :: ('a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space) set) = Collect trace_class›
proof (intro Set.set_eqI iffI)
fix x :: ‹'a ⇒⇩C⇩L 'b›
show ‹x ∈ Collect trace_class ⟹ x ∈ cspan (Collect trace_class)›
by (simp add: complex_vector.span_clauses)
assume ‹x ∈ cspan (Collect trace_class)›
then obtain F f where x_def: ‹x = (∑a∈F. f a *⇩C a)› and ‹F ⊆ Collect trace_class›
by (auto intro!: simp: complex_vector.span_explicit)
then have ‹trace_class x›
by (auto intro!: trace_class_sum trace_class_scaleC simp: x_def)
then show ‹x ∈ Collect trace_class ›
by simp
qed
lemma monotone_convergence_tc:
fixes f :: ‹'b ⇒ ('a, 'a::chilbert_space) trace_class›
assumes bounded: ‹∀⇩F x in F. trace_tc (f x) ≤ B›
assumes pos: ‹∀⇩F x in F. f x ≥ 0›
assumes increasing: ‹increasing_filter (filtermap f F)›
shows ‹∃L. (f ⤏ L) F›
proof -
wlog ‹F ≠ ⊥›
using negation by simp
then have ‹filtermap f F ≠ ⊥›
by (simp add: filtermap_bot_iff)
have ‹mono_on {t::('a,'a) trace_class. t ≥ 0} trace_tc›
by (simp add: ord.mono_onI trace_tc_mono)
with increasing
have ‹increasing_filter (filtermap (trace_tc o f) F)›
unfolding filtermap_compose
apply (rule increasing_filtermap)
by (auto intro!: pos simp: eventually_filtermap)
then obtain l where l: ‹((λx. trace_tc (f x)) ⤏ l) F›
apply atomize_elim
apply (rule monotone_convergence_complex)
using bounded by (simp_all add: o_def)
have ‹cauchy_filter (filtermap f F)›
proof (rule cauchy_filter_metricI)
fix e :: real assume ‹e > 0›
define d where ‹d = e/4›
have ‹∀⇩F x in filtermap f F. dist (trace_tc x) l < d›
unfolding eventually_filtermap
using l apply (rule tendstoD)
using ‹e > 0› by (simp add: d_def)
then obtain P1 where ev_P1: ‹eventually P1 (filtermap f F)› and P1: ‹P1 x ⟹ dist (trace_tc x) l < d› for x
by blast
from increasing obtain P2 where ev_P2: ‹eventually P2 (filtermap f F)› and
P2: ‹P2 x ⟹ (∀⇩F z in filtermap f F. z ≥ x)› for x
using increasing_filter_def by blast
define P where ‹P x ⟷ P1 x ∧ P2 x› for x
with ev_P1 ev_P2 have ev_P: ‹eventually P (filtermap f F)›
by (auto intro!: eventually_conj simp: P_def[abs_def])
have ‹dist x y < e› if ‹P x› and ‹P y› for x y
proof -
from ‹P x› have ‹∀⇩F z in filtermap f F. z ≥ x›
by (simp add: P_def P2)
moreover from ‹P y› have ‹∀⇩F z in filtermap f F. z ≥ y›
by (simp add: P_def P2)
ultimately have ‹∀⇩F z in filtermap f F. z ≥ x ∧ z ≥ y ∧ P1 z›
using ev_P1 by (auto intro!: eventually_conj)
from eventually_happens'[OF ‹filtermap f F ≠ ⊥› this]
obtain z where ‹z ≥ x› and ‹z ≥ y› and ‹P1 z›
by auto
have ‹dist x y ≤ norm (z - x) + norm (z - y)›
by (metis (no_types, lifting) diff_add_cancel diff_add_eq_diff_diff_swap dist_trace_class_def norm_minus_commute norm_triangle_sub)
also from ‹x ≤ z› ‹y ≤ z› have ‹… = (trace_tc z - trace_tc x) + (trace_tc z - trace_tc y)›
by (metis (no_types, lifting) cross3_simps(16) diff_left_mono diff_self norm_tc_pos of_real_add trace_tc_plus)
also from ‹x ≤ z› ‹y ≤ z› have ‹… = norm (trace_tc z - trace_tc x) + norm (trace_tc z - trace_tc y)›
by (simp add: complex_of_real_cmod trace_tc_mono abs_pos)
also have ‹… = dist (trace_tc z) (trace_tc x) + dist (trace_tc z) (trace_tc y)›
using dist_complex_def by presburger
also have ‹… ≤ (dist (trace_tc z) l + dist (trace_tc x) l) + (dist (trace_tc z) l + dist (trace_tc y) l)›
apply (intro complex_of_real_mono add_mono)
by (simp_all add: dist_triangle2)
also from P1 ‹P1 z› that have ‹… < 4 * d›
by (smt (verit, best) P_def complex_of_real_strict_mono_iff)
also have ‹… = e›
by (simp add: d_def)
finally show ?thesis
by simp
qed
with ev_P show ‹∃P. eventually P (filtermap f F) ∧ (∀x y. P x ∧ P y ⟶ dist x y < e)›
by blast
qed
then have ‹convergent_filter (filtermap f F)›
using cauchy_filter_convergent by fastforce
then show ‹∃L. (f ⤏ L) F›
by (simp add: convergent_filter_iff filterlim_def)
qed
lemma nonneg_bdd_above_summable_on_tc:
fixes f :: ‹'a ⇒ ('c::chilbert_space, 'c) trace_class›
assumes pos: ‹⋀x. x∈A ⟹ f x ≥ 0›
assumes bdd: ‹bdd_above (trace_tc ` sum f ` {F. F⊆A ∧ finite F})›
shows ‹f summable_on A›
proof -
have pos': ‹(∑x∈F. f x) ≥ 0› if ‹finite F› and ‹F ⊆ A› for F
using that pos
by (simp add: basic_trans_rules(31) sum_nonneg)
from pos have incr: ‹increasing_filter (filtermap (sum f) (finite_subsets_at_top A))›
by (auto intro!: increasing_filtermap[where X=‹{F. finite F ∧ F ⊆ A}›] mono_onI sum_mono2)
from bdd obtain B where B: ‹trace_tc (sum f X) ≤ B› if ‹finite X› and ‹X ⊆ A› for X
apply atomize_elim
by (auto simp: bdd_above_def)
show ?thesis
apply (simp add: summable_on_def has_sum_def)
by (safe intro!: pos' incr monotone_convergence_tc[where B=B] B
eventually_finite_subsets_at_top_weakI)
qed
lemma summable_Sigma_positive_tc:
fixes f :: ‹'a ⇒ 'b ⇒ ('c, 'c::chilbert_space) trace_class›
assumes ‹⋀x. x∈X ⟹ f x summable_on Y x›
assumes ‹(λx. ∑⇩∞y∈Y x. f x y) summable_on X›
assumes ‹⋀x y. x ∈ X ⟹ y ∈ Y x ⟹ f x y ≥ 0›
shows ‹(λ(x, y). f x y) summable_on (SIGMA x:X. Y x)›
proof -
have ‹trace_tc (∑(x,y)∈F. f x y) ≤ trace_tc (∑⇩∞x∈X. ∑⇩∞y∈Y x. f x y)› if ‹F ⊆ Sigma X Y› and ‹finite F› for F
proof -
define g where ‹g x y = (if (x,y) ∈ Sigma X Y then f x y else 0)› for x y
have g_pos[iff]: ‹g x y ≥ 0› for x y
using assms by (auto intro!: simp: g_def)
have g_summable: ‹g x summable_on Y x› for x
by (metis assms(1) g_def mem_Sigma_iff summable_on_0 summable_on_cong)
have sum_g_summable: ‹(λx. ∑⇩∞y∈Y x. g x y) summable_on X›
by (metis (mono_tags, lifting) SigmaI g_def assms(2) infsum_cong summable_on_cong)
have ‹(∑(x,y)∈F. f x y) = (∑(x,y)∈F. g x y)›
by (smt (verit, ccfv_SIG) g_def split_cong subsetD sum.cong that(1))
also have ‹(∑(x,y)∈F. g x y) ≤ (∑(x,y)∈fst ` F × snd ` F. g x y)›
using that assms apply (auto intro!: sum_mono2 assms simp: image_iff)
by force+
also have ‹… = (∑x∈fst ` F. ∑y∈snd ` F. g x y)›
by (metis (no_types, lifting) finite_imageI sum.Sigma sum.cong that(2))
also have ‹… = (∑x∈fst ` F. ∑⇩∞y∈snd ` F. g x y)›
by (metis finite_imageI infsum_finite that(2))
also have ‹… ≤ (∑x∈fst ` F. ∑⇩∞y∈Y x. g x y)›
apply (intro sum_mono infsum_mono_neutral_traceclass)
using assms that
apply (auto intro!: g_summable)
by (simp add: g_def)
also have ‹… = (∑⇩∞x∈fst ` F. ∑⇩∞y∈Y x. g x y)›
using that by (auto intro!: infsum_finite[symmetric] simp: )
also have ‹… ≤ (∑⇩∞x∈X. ∑⇩∞y∈Y x. g x y)›
apply (rule infsum_mono_neutral_traceclass)
using that assms by (auto intro!: infsum_nonneg_traceclass sum_g_summable)
also have ‹… = (∑⇩∞x∈X. ∑⇩∞y∈Y x. f x y)›
by (smt (verit, ccfv_threshold) g_def infsum_cong mem_Sigma_iff)
finally show ?thesis
using trace_tc_mono by blast
qed
then show ?thesis
apply (rule_tac nonneg_bdd_above_summable_on_tc)
by (auto intro!: assms bdd_aboveI2)
qed
lemma infsum_Sigma_positive_tc:
fixes f :: ‹'a ⇒ 'b ⇒ ('c::chilbert_space, 'c) trace_class›
assumes ‹⋀x. x∈X ⟹ f x summable_on Y x›
assumes ‹⋀x y. x ∈ X ⟹ y ∈ Y x ⟹ f x y ≥ 0›
shows ‹(∑⇩∞x∈X. ∑⇩∞y∈Y x. f x y) = (∑⇩∞(x,y)∈Sigma X Y. f x y)›
proof (cases ‹(λx. ∑⇩∞y∈Y x. f x y) summable_on X›)
case True
show ?thesis
apply (rule infsum_Sigma'_banach)
apply (rule summable_Sigma_positive_tc)
using assms True by auto
next
case False
then have 1: ‹(∑⇩∞x∈X. ∑⇩∞y∈Y x. f x y) = 0›
using infsum_not_exists by blast
from False have ‹¬ (λ(x,y). f x y) summable_on Sigma X Y›
using summable_on_Sigma_banach by blast
then have 2: ‹(∑⇩∞(x, y)∈Sigma X Y. f x y) = 0›
using infsum_not_exists by blast
from 1 2 show ?thesis
by simp
qed
lemma infsum_swap_positive_tc:
fixes f :: ‹'a ⇒ 'b ⇒ ('c::chilbert_space, 'c) trace_class›
assumes ‹⋀x. x∈X ⟹ f x summable_on Y›
assumes ‹⋀y. y∈Y ⟹ (λx. f x y) summable_on X›
assumes ‹⋀x y. x ∈ X ⟹ y ∈ Y ⟹ f x y ≥ 0›
shows ‹(∑⇩∞x∈X. ∑⇩∞y∈Y. f x y) = (∑⇩∞y∈Y. ∑⇩∞x∈X. f x y)›
proof -
have ‹(∑⇩∞x∈X. ∑⇩∞y∈Y. f x y) = (∑⇩∞(x,y)∈X×Y. f x y)›
apply (rule infsum_Sigma_positive_tc)
using assms by auto
also have ‹… = (∑⇩∞(y,x)∈Y×X. f x y)›
apply (subst product_swap[symmetric])
by (simp add: infsum_reindex o_def)
also have ‹… = (∑⇩∞y∈Y. ∑⇩∞x∈X. f x y)›
apply (rule infsum_Sigma_positive_tc[symmetric])
using assms by auto
finally show ?thesis
by -
qed
lemma separating_density_ops:
assumes ‹B > 0›
shows ‹separating_set clinear {t :: ('a::chilbert_space, 'a) trace_class. 0 ≤ t ∧ norm t ≤ B}›
proof -
define S where ‹S = {t :: ('a, 'a) trace_class. 0 ≤ t ∧ norm t ≤ B}›
have ‹cspan S = UNIV›
proof (intro Set.set_eqI iffI UNIV_I)
fix t :: ‹('a, 'a) trace_class›
from trace_class_decomp_4pos'
obtain t1 t2 t3 t4 where t_decomp: ‹t = t1 - t2 + 𝗂 *⇩C t3 - 𝗂 *⇩C t4›
and pos: ‹t1 ≥ 0› ‹t2 ≥ 0› ‹t3 ≥ 0› ‹t4 ≥ 0›
by fast
have ‹t' ∈ cspan S› if ‹t' ≥ 0› for t'
proof -
define t'' where ‹t'' = (B / norm t') *⇩R t'›
have ‹t'' ∈ S›
using ‹B > 0›
by (simp add: S_def that zero_le_scaleR_iff t''_def)
have t'_t'': ‹t' = (norm t' / B) *⇩R t''›
using ‹B > 0› t''_def by auto
show ‹t' ∈ cspan S›
apply (subst t'_t'')
using ‹t'' ∈ S›
by (simp add: scaleR_scaleC complex_vector.span_clauses)
qed
with pos have ‹t1 ∈ cspan S› and ‹t2 ∈ cspan S› and ‹t3 ∈ cspan S› and ‹t4 ∈ cspan S›
by auto
then show ‹t ∈ cspan S›
by (auto intro!: complex_vector.span_diff complex_vector.span_add complex_vector.span_scale
intro: complex_vector.span_base simp: t_decomp)
qed
then show ‹separating_set clinear S›
by (rule separating_set_clinear_cspan)
qed
lemma summable_abs_summable_tc:
fixes f :: ‹'a ⇒ ('b::chilbert_space,'b) trace_class›
assumes ‹f summable_on X›
assumes ‹⋀x. x∈X ⟹ f x ≥ 0›
shows ‹f abs_summable_on X›
proof -
from assms(1) have ‹(λx. trace_tc (f x)) summable_on X›
apply (rule summable_on_bounded_linear[rotated])
by (simp add: bounded_clinear.bounded_linear)
then have ‹(λx. Re (trace_tc (f x))) summable_on X›
using summable_on_Re by blast
then show ‹(λx. norm (f x)) summable_on X›
by (metis (mono_tags, lifting) assms(2) norm_tc_pos_Re summable_on_cong)
qed
lemma sandwich_tc_eq0_D:
assumes eq0: ‹⋀ρ. ρ ≥ 0 ⟹ norm ρ ≤ B ⟹ sandwich_tc a ρ = 0›
assumes Bpos: ‹B > 0›
shows ‹a = 0›
proof (rule ccontr)
assume ‹a ≠ 0›
obtain h where ‹a h ≠ 0›
proof (atomize_elim, rule ccontr)
assume ‹∄h. a *⇩V h ≠ 0›
then have ‹a h = 0› for h
by blast
then have ‹a = 0›
by (auto intro!: cblinfun_eqI)
with ‹a ≠ 0›
show False
by simp
qed
then have ‹h ≠ 0›
by force
define k where ‹k = sqrt B *⇩R sgn h›
from ‹a h ≠ 0› Bpos have ‹a k ≠ 0›
by (smt (verit, best) cblinfun.scaleR_right k_def linordered_field_class.inverse_positive_iff_positive real_sqrt_gt_zero scaleR_simps(7) sgn_div_norm zero_less_norm_iff)
have ‹norm (from_trace_class (sandwich_tc a (tc_butterfly k k))) = norm (butterfly (a k) (a k))›
by (simp add: from_trace_class_sandwich_tc tc_butterfly.rep_eq sandwich_butterfly)
also have ‹… = (norm (a k))⇧2›
by (simp add: norm_butterfly power2_eq_square)
also from ‹a k ≠ 0›
have ‹… ≠ 0›
by simp
finally have sand_neq0: ‹sandwich_tc a (tc_butterfly k k) ≠ 0›
by fastforce
have ‹norm (tc_butterfly k k) = B›
using ‹h ≠ 0› Bpos
by (simp add: norm_tc_butterfly k_def norm_sgn)
with sand_neq0 assms
show False
by simp
qed
lemma sandwich_tc_butterfly: ‹sandwich_tc c (tc_butterfly a b) = tc_butterfly (c a) (c b)›
by (metis from_trace_class_inverse from_trace_class_sandwich_tc sandwich_butterfly tc_butterfly.rep_eq)
lemma tc_butterfly_0_left[simp]: ‹tc_butterfly 0 t = 0›
by (metis mult_eq_0_iff norm_eq_zero norm_tc_butterfly)
lemma tc_butterfly_0_right[simp]: ‹tc_butterfly t 0 = 0›
by (metis mult_eq_0_iff norm_eq_zero norm_tc_butterfly)
subsection ‹More Hilbert-Schmidt›
lemma trace_class_hilbert_schmidt: ‹hilbert_schmidt a› if ‹trace_class a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
by (auto intro!: trace_class_comp_right that simp: hilbert_schmidt_def)
lemma finite_rank_hilbert_schmidt: ‹hilbert_schmidt a› if ‹finite_rank a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
using finite_rank_comp_right finite_rank_trace_class hilbert_schmidtI that by blast
lemma hilbert_schmidt_compact: ‹compact_op a› if ‹hilbert_schmidt a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
have ‹∃b. finite_rank b ∧ hilbert_schmidt_norm (b - a) < ε› if ‹ε > 0› for ε
proof -
have ‹ε⇧2 > 0›
using that by force
obtain B :: ‹'a set› where ‹is_onb B›
using is_onb_some_chilbert_basis by blast
with ‹hilbert_schmidt a› have a_sum_B: ‹(λx. (norm (a *⇩V x))⇧2) summable_on B›
by (auto intro!: summable_hilbert_schmidt_norm_square)
then have ‹((λx. (norm (a *⇩V x))⇧2) has_sum (∑⇩∞x∈B. (norm (a *⇩V x))⇧2)) B›
using has_sum_infsum by blast
from tendsto_iff[THEN iffD1, rule_format, OF this[unfolded has_sum_def] ‹ε⇧2 > 0›]
obtain F where [simp]: ‹finite F› and ‹F ⊆ B›
and Fbound: ‹dist (∑x∈F. (norm (a *⇩V x))⇧2) (∑⇩∞x∈B. (norm (a *⇩V x))⇧2) < ε⇧2›
apply atomize_elim
by (auto intro!: simp: eventually_finite_subsets_at_top)
define p b where ‹p = (∑x∈F. selfbutter x)› and ‹b = a o⇩C⇩L p›
have [simp]: ‹p x = x› if ‹x ∈ F› for x
apply (simp add: p_def cblinfun.sum_left)
apply (subst sum_single[where i=x])
using ‹F ⊆ B› that ‹is_onb B›
by (auto intro!: simp: cnorm_eq_1 is_onb_def is_ortho_set_def)
have [simp]: ‹p x = 0› if ‹x ∈ B - F› for x
using ‹F ⊆ B› that ‹is_onb B›
apply (auto intro!: sum.neutral simp add: p_def cblinfun.sum_left is_onb_def is_ortho_set_def)
by auto
have ‹finite_rank p›
by (simp add: finite_rank_sum p_def)
then have ‹finite_rank b›
by (simp add: b_def finite_rank_comp_right)
with ‹hilbert_schmidt a› have ‹hilbert_schmidt (b - a)›
by (auto intro!: hilbert_schmidt_minus intro: finite_rank_hilbert_schmidt)
then have ‹(hilbert_schmidt_norm (b - a))⇧2 = (∑⇩∞x∈B. (norm ((b - a) *⇩V x))⇧2)›
by (simp add: infsum_hilbert_schmidt_norm_square ‹is_onb B›)
also have ‹… = (∑⇩∞x∈B-F. (norm (a *⇩V x))⇧2)›
by (auto intro!: infsum_cong_neutral
simp: b_def cblinfun.diff_left)
also have ‹… = (∑⇩∞x∈B. (norm (a *⇩V x))⇧2) - (∑x∈F. (norm (a *⇩V x))⇧2)›
apply (subst infsum_Diff)
using ‹F ⊆ B› a_sum_B by auto
also have ‹… < ε⇧2›
using Fbound
by (simp add: dist_norm)
finally show ?thesis
using ‹finite_rank b›
using power_less_imp_less_base that by fastforce
qed
then have ‹∃b. finite_rank b ∧ dist b a < ε› if ‹ε > 0› for ε
apply (rule ex_mono[rule_format, rotated])
apply (auto intro!: that simp: dist_norm)
using hilbert_schmidt_minus ‹hilbert_schmidt a› finite_rank_hilbert_schmidt hilbert_schmidt_norm_geq_norm
by fastforce
then show ?thesis
by (simp add: compact_op_finite_rank closure_approachable)
qed
lemma trace_class_compact: ‹compact_op a› if ‹trace_class a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
by (simp add: hilbert_schmidt_compact that trace_class_hilbert_schmidt)
subsection ‹Spectral Theorem›
text ‹The spectral theorem for trace class operators.
A corollary of the one for compact operators (\<^theory>‹Hilbert_Space_Tensor_Product.Spectral_Theorem›) but not an immediate one.›
lift_definition spectral_dec_proj_tc :: ‹('a::chilbert_space, 'a) trace_class ⇒ nat ⇒ ('a, 'a) trace_class› is
spectral_dec_proj
using finite_rank_trace_class spectral_dec_proj_finite_rank trace_class_compact by blast
lift_definition spectral_dec_val_tc :: ‹('a::chilbert_space, 'a) trace_class ⇒ nat ⇒ complex› is
spectral_dec_val.
lemma spectral_dec_proj_tc_finite_rank:
assumes ‹adj_tc a = a›
shows ‹finite_rank_tc (spectral_dec_proj_tc a n)›
using assms apply transfer
by (simp add: spectral_dec_proj_finite_rank trace_class_compact)
lemma spectral_dec_summable_tc:
assumes ‹selfadjoint_tc a›
shows ‹(λn. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) abs_summable_on UNIV›
proof (intro nonneg_bounded_partial_sums_imp_summable_on norm_ge_zero eventually_finite_subsets_at_top_weakI)
define a' where ‹a' = from_trace_class a›
then have [transfer_rule]: ‹cr_trace_class a' a›
by (simp add: cr_trace_class_def)
have ‹compact_op a'›
by (auto intro!: trace_class_compact simp: a'_def)
have ‹selfadjoint a'›
using a'_def assms selfadjoint_tc.rep_eq by blast
fix F :: ‹nat set› assume ‹finite F›
define R where ‹R = (⨆n∈F. spectral_dec_space a' n)›
have ‹(∑x∈F. norm (spectral_dec_val_tc a x *⇩C spectral_dec_proj_tc a x))
= norm (∑x∈F. spectral_dec_val_tc a x *⇩C spectral_dec_proj_tc a x)›
proof (rule norm_tc_sum_exchange[symmetric]; transfer; rename_tac n m F)
fix n m :: nat assume ‹n ≠ m›
then have *: ‹Proj (spectral_dec_space a' n) o⇩C⇩L Proj (spectral_dec_space a' m) = 0› if ‹spectral_dec_val a' n ≠ 0› and ‹spectral_dec_val a' m ≠ 0›
by (auto intro!: orthogonal_projectors_orthogonal_spaces[THEN iffD1] spectral_dec_space_orthogonal ‹compact_op a'› ‹selfadjoint a'›simp: )
show ‹(spectral_dec_val a' n *⇩C spectral_dec_proj a' n)* o⇩C⇩L spectral_dec_val a' m *⇩C spectral_dec_proj a' m = 0›
by (auto intro!: * simp: spectral_dec_proj_def adj_Proj)
show ‹spectral_dec_val a' n *⇩C spectral_dec_proj a' n o⇩C⇩L (spectral_dec_val a' m *⇩C spectral_dec_proj a' m)* = 0›
by (auto intro!: * simp: spectral_dec_proj_def adj_Proj)
qed
also have ‹… = trace_norm (∑x∈F. spectral_dec_val a' x *⇩C spectral_dec_proj a' x)›
by (metis (no_types, lifting) a'_def spectral_dec_proj_tc.rep_eq spectral_dec_val_tc.rep_eq from_trace_class_sum norm_trace_class.rep_eq scaleC_trace_class.rep_eq sum.cong)
also have ‹… = trace_norm (∑x. if x∈F then spectral_dec_val a' x *⇩C spectral_dec_proj a' x else 0)›
by (simp add: ‹finite F› suminf_If_finite_set)
also have ‹… = trace_norm (∑x. (spectral_dec_val a' x *⇩C spectral_dec_proj a' x) o⇩C⇩L Proj R)›
proof -
have ‹spectral_dec_proj a' n = spectral_dec_proj a' n o⇩C⇩L Proj R› if ‹n ∈ F› for n
by (auto intro!: Proj_o_Proj_subspace_left[symmetric] SUP_upper that simp: spectral_dec_proj_def R_def)
moreover have ‹spectral_dec_proj a' n o⇩C⇩L Proj R = 0› if ‹n ∉ F› for n
using that
by (auto intro!: orthogonal_spaces_SUP_right spectral_dec_space_orthogonal ‹compact_op a'› ‹selfadjoint a'›
simp: spectral_dec_proj_def R_def
simp flip: orthogonal_projectors_orthogonal_spaces)
ultimately show ?thesis
by (auto intro!: arg_cong[where f=trace_norm] suminf_cong)
qed
also have ‹… = trace_norm ((∑x. spectral_dec_val a' x *⇩C spectral_dec_proj a' x) o⇩C⇩L Proj R)›
apply (intro arg_cong[where f=trace_norm] bounded_linear.suminf[symmetric]
bounded_clinear.bounded_linear bounded_clinear_cblinfun_compose_left sums_summable)
using ‹compact_op a'› ‹selfadjoint a'› spectral_dec_sums by blast
also have ‹… = trace_norm (a' o⇩C⇩L Proj R)›
using spectral_dec_sums[OF ‹compact_op a'› ‹selfadjoint a'›] sums_unique by fastforce
also have ‹… ≤ trace_norm a' * norm (Proj R)›
by (auto intro!: trace_norm_comp_left simp: a'_def)
also have ‹… ≤ trace_norm a'›
by (simp add: mult_left_le norm_Proj_leq1)
finally show ‹(∑x∈F. norm (spectral_dec_val_tc a x *⇩C spectral_dec_proj_tc a x)) ≤ trace_norm a'›
by -
qed
lemma spectral_dec_has_sum_tc:
assumes ‹selfadjoint_tc a›
shows ‹((λn. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) has_sum a) UNIV›
proof -
define a' b b' where ‹a' = from_trace_class a›
and ‹b = (∑⇩∞n. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n)› and ‹b' = from_trace_class b›
have [simp]: ‹compact_op a'›
by (auto intro!: trace_class_compact simp: a'_def)
have [simp]: ‹selfadjoint a'›
using a'_def assms selfadjoint_tc.rep_eq by blast
have [simp]: ‹trace_class b'›
by (simp add: b'_def)
from spectral_dec_summable_tc[OF assms]
have has_sum_b: ‹((λn. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) has_sum b) UNIV›
by (metis abs_summable_summable b_def summable_iff_has_sum_infsum)
then have ‹((λF. ∑n∈F. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) ⤏ b) (finite_subsets_at_top UNIV)›
by (simp add: has_sum_def)
then have ‹((λF. norm ((∑n∈F. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) - b)) ⤏ 0) (finite_subsets_at_top UNIV)›
using LIM_zero tendsto_norm_zero by blast
then have ‹((λF. norm ((∑n∈F. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) - b)) ⤏ 0) (filtermap (λn. {..<n}) sequentially)›
by (meson filterlim_compose filterlim_filtermap filterlim_lessThan_at_top)
then have ‹((λm. norm ((∑n∈{..<m}. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) - b)) ⤏ 0) sequentially›
by (simp add: filterlim_filtermap)
then have ‹((λm. trace_norm ((∑n∈{..<m}. spectral_dec_val a' n *⇩C spectral_dec_proj a' n) - b')) ⤏ 0) sequentially›
unfolding a'_def b'_def
by transfer
then have ‹((λm. norm ((∑n∈{..<m}. spectral_dec_val a' n *⇩C spectral_dec_proj a' n) - b')) ⤏ 0) sequentially›
apply (rule tendsto_0_le[where K=1])
by (auto intro!: eventually_sequentiallyI norm_leq_trace_norm trace_class_minus
trace_class_sum trace_class_scaleC spectral_dec_proj_finite_rank
intro: finite_rank_trace_class)
then have ‹(λn. spectral_dec_val a' n *⇩C spectral_dec_proj a' n) sums b'›
using LIM_zero_cancel sums_def tendsto_norm_zero_iff by blast
moreover have ‹(λn. spectral_dec_val a' n *⇩C spectral_dec_proj a' n) sums a'›
using ‹compact_op a'› ‹selfadjoint a'› by (rule spectral_dec_sums)
ultimately have ‹a = b›
using a'_def b'_def from_trace_class_inject sums_unique2 by blast
with has_sum_b show ?thesis
by simp
qed
lemma spectral_dec_sums_tc:
assumes ‹selfadjoint_tc a›
shows ‹(λn. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) sums a›
using assms has_sum_imp_sums spectral_dec_has_sum_tc by blast
lift_definition spectral_dec_vecs_tc :: ‹('a,'a) trace_class ⇒ 'a::chilbert_space set› is
spectral_dec_vecs.
lemma compact_from_trace_class[iff]: ‹compact_op (from_trace_class t)›
by (auto intro!: simp: trace_class_compact)
lemma sum_some_onb_of_tc_butterfly:
assumes ‹finite_dim_ccsubspace S›
shows ‹(∑x∈some_onb_of S. tc_butterfly x x) = Abs_trace_class (Proj S)›
by (metis (mono_tags, lifting) assms from_trace_class_inverse from_trace_class_sum sum.cong sum_some_onb_of_butterfly tc_butterfly.rep_eq)
lemma butterfly_spectral_dec_vec_tc_has_sum:
assumes ‹t ≥ 0›
shows ‹((λv. tc_butterfly v v) has_sum t) (spectral_dec_vecs_tc t)›
proof -
define t' where ‹t' = from_trace_class t›
note power2_csqrt[unfolded power2_eq_square, simp]
note Reals_cnj_iff[simp]
have [simp]: ‹compact_op t'›
by (simp add: t'_def)
from assms have ‹selfadjoint_tc t›
apply transfer
apply (rule comparable_selfadjoint[of 0])
by simp_all
have spectral_real[simp]: ‹spectral_dec_val t' n ∈ ℝ› for n
apply (rule spectral_dec_val_real)
using ‹selfadjoint_tc t› by (auto intro!: trace_class_compact simp: selfadjoint_tc.rep_eq t'_def)
have *: ‹((λ(n,v). tc_butterfly v v) has_sum t) (SIGMA n:UNIV. (*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n))›
proof (rule has_sum_SigmaI[where g=‹λn. spectral_dec_val t' n *⇩C spectral_dec_proj_tc t n›])
have ‹spectral_dec_val t' n ≥ 0› for n
by (simp add: assms from_trace_class_pos spectral_dec_val_nonneg t'_def)
then have [simp]: ‹cnj (csqrt (spectral_dec_val t' n)) * csqrt (spectral_dec_val t' n) = spectral_dec_val t' n› for n
apply (auto simp add: csqrt_of_real_nonneg less_eq_complex_def)
by (metis of_real_Re of_real_mult spectral_real sqrt_sqrt)
have sum: ‹(∑y∈(λx. csqrt (spectral_dec_val t' n) *⇩C x) ` some_onb_of (spectral_dec_space t' n). tc_butterfly y y) = spectral_dec_val t' n *⇩C spectral_dec_proj_tc t n› for n
proof (cases ‹spectral_dec_val t' n = 0›)
case True
then show ?thesis
by (metis (mono_tags, lifting) csqrt_0 imageE scaleC_eq_0_iff sum.neutral tc_butterfly_scaleC_left)
next
case False
then have ‹inj_on (λx. csqrt (spectral_dec_val t' n) *⇩C x) X› for X :: ‹'a set›
by (meson csqrt_eq_0 inj_scaleC)
then show ?thesis
by (simp add: sum.reindex False spectral_dec_space_finite_dim sum_some_onb_of_tc_butterfly
spectral_dec_proj_def spectral_dec_proj_tc_def flip: scaleC_sum_right t'_def)
qed
then show ‹((λy. case (n, y) of (n, v) ⇒ tc_butterfly v v) has_sum spectral_dec_val t' n *⇩C spectral_dec_proj_tc t n)
((*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n))› for n
by (auto intro!: has_sum_finiteI finite_imageI some_onb_of_finite_dim spectral_dec_space_finite_dim simp: t'_def)
show ‹((λn. spectral_dec_val t' n *⇩C spectral_dec_proj_tc t n) has_sum t) UNIV›
by (auto intro!: spectral_dec_has_sum_tc ‹selfadjoint_tc t› simp: t'_def simp flip: spectral_dec_val_tc.rep_eq)
show ‹(λ(n, v). tc_butterfly v v) summable_on (SIGMA n:UNIV. (*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n))›
proof -
have inj: ‹inj_on ((*⇩C) (csqrt (spectral_dec_val t' n))) (some_onb_of (spectral_dec_space t' n))› for n
proof (cases ‹spectral_dec_val t' n = 0›)
case True
then have ‹spectral_dec_space t' n = 0›
using spectral_dec_space_0 by blast
then have ‹some_onb_of (spectral_dec_space t' n) = {}›
using some_onb_of_0 by auto
then show ?thesis
by simp
next
case False
then show ?thesis
by (auto intro!: inj_scaleC)
qed
have 1: ‹(λx. tc_butterfly x x) abs_summable_on (λxa. csqrt (spectral_dec_val t' n) *⇩C xa) ` some_onb_of (spectral_dec_space t' n)› for n
by (auto intro!: summable_on_finite some_onb_of_finite_dim spectral_dec_space_finite_dim simp: t'_def)
have ‹(λn. cmod (spectral_dec_val t' n) * (∑⇩∞h∈some_onb_of (spectral_dec_space t' n). norm (tc_butterfly h h))) abs_summable_on UNIV›
proof -
have *: ‹(∑⇩∞h∈some_onb_of (spectral_dec_space t' n). norm (tc_butterfly h h)) = norm (spectral_dec_proj_tc t n)› for n
proof -
have ‹(∑⇩∞h∈some_onb_of (spectral_dec_space t' n). norm (tc_butterfly h h))
= (∑⇩∞h∈some_onb_of (spectral_dec_space t' n). 1)›
by (simp add: infsum_cong norm_tc_butterfly some_onb_of_norm1)
also have ‹… = card (some_onb_of (spectral_dec_space t' n))›
by simp
also have ‹… = cdim (space_as_set (spectral_dec_space t' n))›
by (simp add: some_onb_of_card)
also have ‹… = norm (spectral_dec_proj_tc t n)›
unfolding t'_def
apply transfer
by (metis of_real_eq_iff of_real_of_nat_eq spectral_dec_proj_def spectral_dec_proj_pos
trace_Proj trace_norm_pos)
finally show ?thesis
by -
qed
show ?thesis
apply (simp add: * )
by (metis (no_types, lifting) ‹selfadjoint_tc t› norm_scaleC spectral_dec_summable_tc
spectral_dec_val_tc.rep_eq summable_on_cong t'_def)
qed
then have 2: ‹(λn. ∑⇩∞v∈(*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n).
norm (tc_butterfly v v)) abs_summable_on UNIV›
apply (subst infsum_reindex)
by (auto intro!: inj simp: o_def infsum_cmult_right' norm_mult simp del: real_norm_def)
show ?thesis
apply (rule abs_summable_summable)
apply (rule abs_summable_on_Sigma_iff[THEN iffD2])
using 1 2 by auto
qed
qed
have ‹((λv. tc_butterfly v v) has_sum t) (⋃n. (*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n))›
proof -
have **: ‹(⋃n. (*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n)) =
snd ` (SIGMA n:UNIV. (*⇩C) (csqrt (spectral_dec_val t' n)) ` some_onb_of (spectral_dec_space t' n))›
by force
have inj: ‹inj_on snd (SIGMA n:UNIV. (λx. csqrt (spectral_dec_val t' n) *⇩C x) ` some_onb_of (spectral_dec_space t' n))›
proof (rule inj_onI)
fix nh assume nh: ‹nh ∈ (SIGMA n:UNIV. (λx. csqrt (spectral_dec_val t' n) *⇩C x) ` some_onb_of (spectral_dec_space t' n))›
fix mg assume mg: ‹mg ∈ (SIGMA m:UNIV. (λx. csqrt (spectral_dec_val t' m) *⇩C x) ` some_onb_of (spectral_dec_space t' m))›
assume ‹snd nh = snd mg›
from nh obtain n h where nh': ‹nh = (n, csqrt (spectral_dec_val t' n) *⇩C h)› and h: ‹h ∈ some_onb_of (spectral_dec_space t' n)›
by blast
from mg obtain m g where mg': ‹mg = (m, csqrt (spectral_dec_val t' m) *⇩C g)› and g: ‹g ∈ some_onb_of (spectral_dec_space t' m)›
by blast
have ‹n = m›
proof (rule ccontr)
assume [simp]: ‹n ≠ m›
from h have val_not_0: ‹spectral_dec_val t' n ≠ 0›
using some_onb_of_0 spectral_dec_space_0 by fastforce
from ‹snd nh = snd mg› nh' mg' have eq: ‹csqrt (spectral_dec_val t' n) *⇩C h = csqrt (spectral_dec_val t' m) *⇩C g›
by simp
from ‹n ≠ m› have ‹orthogonal_spaces (spectral_dec_space t' n) (spectral_dec_space t' m)›
apply (rule spectral_dec_space_orthogonal[rotated -1])
using ‹selfadjoint_tc t› by (auto intro!: trace_class_compact simp: t'_def selfadjoint_tc.rep_eq)
with h g have ‹is_orthogonal h g›
using orthogonal_spaces_ccspan by fastforce
then have ‹is_orthogonal (csqrt (spectral_dec_val t' n) *⇩C h) (csqrt (spectral_dec_val t' m) *⇩C g)›
by force
with eq have val_h_0: ‹csqrt (spectral_dec_val t' n) *⇩C h = 0›
by simp
with val_not_0 have ‹h = 0›
by fastforce
with h show False
using some_onb_of_is_ortho_set
by (auto simp: is_ortho_set_def)
qed
with ‹snd nh = snd mg› nh' mg' show ‹nh = mg›
by simp
qed
from * show ?thesis
apply (subst ** )
apply (rule has_sum_reindex[THEN iffD2, rotated])
by (auto intro!: inj simp: o_def case_prod_unfold)
qed
then show ?thesis
by (simp add: spectral_dec_vecs_tc.rep_eq spectral_dec_vecs_def flip: t'_def)
qed
lemma spectral_dec_vec_tc_norm_summable:
assumes ‹t ≥ 0›
shows ‹(λv. (norm v)⇧2) summable_on (spectral_dec_vecs_tc t)›
proof -
from butterfly_spectral_dec_vec_tc_has_sum[OF assms]
have ‹(λv. tc_butterfly v v) summable_on (spectral_dec_vecs_tc t)›
using has_sum_imp_summable by blast
then have ‹(λv. trace_tc (tc_butterfly v v)) summable_on (spectral_dec_vecs_tc t)›
apply (rule summable_on_bounded_linear[rotated])
by (simp add: bounded_clinear.bounded_linear)
moreover have *: ‹trace_tc (tc_butterfly v v) = of_real ((norm v)⇧2)› for v :: 'a
by (metis norm_tc_butterfly norm_tc_pos power2_eq_square tc_butterfly_pos)
ultimately have ‹(λv. complex_of_real ((norm v)⇧2)) summable_on (spectral_dec_vecs_tc t)›
by simp
then show ?thesis
by (smt (verit, ccfv_SIG) norm_of_real summable_on_cong summable_on_iff_abs_summable_on_complex zero_le_power2)
qed
subsection ‹More Trace-Class›
lemma finite_rank_tc_dense_aux: ‹closure (Collect finite_rank_tc :: ('a::chilbert_space, 'a) trace_class set) = UNIV›
proof (intro order_top_class.top_le subsetI)
fix a :: ‹('a,'a) trace_class›
wlog selfadj: ‹selfadjoint_tc a› goal ‹a ∈ closure (Collect finite_rank_tc)› generalizing a
proof -
define b c where ‹b = a + adj_tc a› and ‹c = 𝗂 *⇩C (a - adj_tc a)›
have ‹adj_tc b = b›
unfolding b_def
apply transfer
by (simp add: adj_plus)
have ‹adj_tc c = c›
unfolding c_def
apply transfer
apply (simp add: adj_minus)
by (metis minus_diff_eq scaleC_right.minus)
have abc: ‹a = (1/2) *⇩C b + (-𝗂/2) *⇩C c›
apply (simp add: b_def c_def)
by (metis (no_types, lifting) cross3_simps(8) diff_add_cancel group_cancel.add2 scaleC_add_right scaleC_half_double)
have ‹b ∈ closure (Collect finite_rank_tc)› and ‹c ∈ closure (Collect finite_rank_tc)›
using ‹adj_tc b = b› ‹adj_tc c = c› hypothesis selfadjoint_tc_def' by auto
with abc have ‹a ∈ cspan (closure (Collect finite_rank_tc))›
by (metis complex_vector.span_add complex_vector.span_clauses(1) complex_vector.span_clauses(4))
also have ‹… ⊆ closure (cspan (Collect finite_rank_tc))›
by (simp add: closure_mono complex_vector.span_minimal complex_vector.span_superset)
also have ‹… = closure (Collect finite_rank_tc)›
by (metis Set.basic_monos(1) complex_vector.span_minimal complex_vector.span_superset csubspace_finite_rank_tc subset_antisym)
finally show ?thesis
by -
qed
then have ‹(λn. spectral_dec_val_tc a n *⇩C spectral_dec_proj_tc a n) sums a›
by (simp add: spectral_dec_sums_tc)
moreover from selfadj
have ‹finite_rank_tc (∑i<n. spectral_dec_val_tc a i *⇩C spectral_dec_proj_tc a i)› for n
apply (induction n)
by (auto intro!: finite_rank_tc_plus spectral_dec_proj_tc_finite_rank finite_rank_tc_scale
simp: selfadjoint_tc_def')
ultimately show ‹a ∈ closure (Collect finite_rank_tc)›
unfolding sums_def closure_sequential
apply (auto intro!: simp: sums_def closure_sequential)
by meson
qed
lemma finite_rank_tc_dense: ‹closure (Collect finite_rank_tc :: ('a::chilbert_space, 'b::chilbert_space) trace_class set) = UNIV›
proof -
have ‹UNIV = closure (Collect finite_rank_tc :: ('a×'b, 'a×'b) trace_class set)›
by (rule finite_rank_tc_dense_aux[symmetric])
define l r and corner :: ‹('a×'b, 'a×'b) trace_class ⇒ _› where
‹l = cblinfun_left› and ‹r = cblinfun_right› and
‹corner t = compose_tcl (compose_tcr (r*) t) l› for t
have [iff]: ‹bounded_clinear corner›
by (auto intro: bounded_clinear_compose compose_tcl.bounded_clinear_left compose_tcr.bounded_clinear_right
simp: corner_def[abs_def])
have ‹UNIV = corner ` UNIV›
proof (intro UNIV_eq_I range_eqI)
fix t
have ‹from_trace_class (corner (compose_tcl (compose_tcr r t) (l*)))
= (r* o⇩C⇩L r) o⇩C⇩L from_trace_class t o⇩C⇩L (l* o⇩C⇩L l)›
by (simp add: corner_def compose_tcl.rep_eq compose_tcr.rep_eq cblinfun_compose_assoc)
also have ‹… = from_trace_class t›
by (simp add: l_def r_def)
finally show ‹t = corner (compose_tcl (compose_tcr r t) (l*))›
by (metis from_trace_class_inject)
qed
also have ‹… = corner ` closure (Collect finite_rank_tc)›
by (simp add: finite_rank_tc_dense_aux)
also have ‹… ⊆ closure (corner ` Collect finite_rank_tc)›
by (auto intro!: bounded_clinear.bounded_linear closure_bounded_linear_image_subset)
also have ‹… ⊆ closure (Collect finite_rank_tc)›
proof (intro closure_mono subsetI CollectI)
fix t assume ‹t ∈ corner ` Collect finite_rank_tc›
then obtain u where ‹finite_rank_tc u› and tu: ‹t = corner u›
by blast
show ‹finite_rank_tc t›
using ‹finite_rank_tc u›
by (auto intro!: finite_rank_compose_right[of _ l] finite_rank_compose_left[of _ ‹r*›]
simp add: corner_def tu finite_rank_tc.rep_eq compose_tcl.rep_eq compose_tcr.rep_eq)
qed
finally show ?thesis
by blast
qed
hide_fact finite_rank_tc_dense_aux
lemma ccspan_finite_rank_tc[simp]: ‹ccspan (Collect finite_rank_tc) = ⊤›
apply transfer'
apply (rule order_top_class.top_le)
by (metis complex_vector.span_eq_iff csubspace_finite_rank_tc finite_rank_tc_dense order.refl)
lemma ccspan_rank1_tc[simp]: ‹ccspan (Collect rank1_tc) = ⊤›
by (smt (verit, ccfv_SIG) basic_trans_rules(31) ccspan.rep_eq ccspan_finite_rank_tc ccspan_leqI ccspan_mono closure_subset
complex_vector.span_superset cspan_eqI finite_rank_tc_def' mem_Collect_eq order_trans_rules(24))
lemma onb_butterflies_span_trace_class:
fixes A :: ‹'a::chilbert_space set› and B :: ‹'b::chilbert_space set›
assumes ‹is_onb A› and ‹is_onb B›
shows ‹ccspan ((λ(x, y). tc_butterfly x y) ` (A×B)) = ⊤›
proof -
have ‹closure (cspan ((λ(x, y). tc_butterfly x y) ` (A×B))) ⊇ Collect rank1_tc›
proof (rule subsetI)
fix x :: ‹('b, 'a) trace_class› assume ‹x ∈ Collect rank1_tc›
then obtain a b where xab: ‹x = tc_butterfly a b›
apply transfer using rank1_iff_butterfly by fastforce
define f where ‹f F G = tc_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 d: ‹norm a * d + norm a * d + norm b * d < e›
proof -
have ‹norm a * d ≤ e/4›
using ‹e > 0› apply (auto simp: d_def)
apply (simp add: divide_le_eq)
by (smt (z3) Extra_Ordered_Fields.mult_sign_intros(3) ‹0 < e› antisym_conv divide_le_eq less_imp_le linordered_field_class.mult_imp_div_pos_le mult_left_mono nice_ordered_field_class.dense_le nice_ordered_field_class.divide_nonneg_neg nice_ordered_field_class.divide_nonpos_pos nle_le nonzero_mult_div_cancel_left norm_imp_pos_and_ge ordered_field_class.sign_simps(5) split_mult_pos_le)
moreover have ‹norm b * d ≤ e/4›
using ‹e > 0› apply (auto simp: d_def)
apply (simp add: divide_le_eq)
by (smt (verit) linordered_field_class.mult_imp_div_pos_le mult_left_mono norm_le_zero_iff ordered_field_class.sign_simps(5))
ultimately have ‹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
by -
qed
have [simp]: ‹d > 0›
using ‹e > 0› apply (auto simp: d_def)
apply (smt (verit, best) nice_ordered_field_class.divide_pos_pos norm_eq_zero norm_not_less_zero)
by (smt (verit) linordered_field_class.divide_pos_pos zero_less_norm_iff)
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) a + Proj (ccspan (A-F)) a›
using assms apply (simp add: is_onb_def is_ortho_set_def that Proj_orthog_ccspan_union flip: cblinfun.add_left)
apply (subst Proj_orthog_ccspan_union[symmetric])
apply (metis DiffD1 DiffD2 in_mono that(3))
using ‹F ⊆ A› by (auto intro!: simp: Un_absorb1)
have b_split: ‹b = Proj (ccspan G) b + Proj (ccspan (B-G)) b›
using assms apply (simp add: is_onb_def is_ortho_set_def that Proj_orthog_ccspan_union flip: cblinfun.add_left)
apply (subst Proj_orthog_ccspan_union[symmetric])
apply (metis DiffD1 DiffD2 in_mono that(4))
using ‹G ⊆ B› by (auto intro!: simp: Un_absorb1)
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_tc_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_tc_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
apply (subst a_split, subst b_split)
by (simp add: f_def tc_butterfly_add_right tc_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
show ‹∀⇩F FG in finite_subsets_at_top A ×⇩F finite_subsets_at_top B. norm (case_prod f FG - x) < e›
apply (rule eventually_elim2)
apply (rule eventually_prodI[where P=‹λF. finite F ∧ F ⊆ A› and Q=‹λG. finite G ∧ G ⊆ B›])
apply auto[2]
apply (rule FG_close)
using fFG_dist by fastforce
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 ((λ(ξ,η). tc_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 ((λ(ξ,η). tc_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)›
apply atomize_elim
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)›
apply atomize_elim
using complex_vector.span_finite[OF ‹finite G›]
by auto
have ‹tc_butterfly ξ η ∈ (λ(ξ, η). tc_butterfly ξ η) ` (A × B)›
if ‹η ∈ G› and ‹ξ ∈ F› for η ξ
using ‹F ⊆ A› ‹G ⊆ B› that by (auto intro!: pair_imageI)
then show ?thesis
by (auto intro!: complex_vector.span_sum complex_vector.span_scale
intro: complex_vector.span_base[where a=‹tc_butterfly _ _›]
simp add: f_def ProjFsum ProjGsum tc_butterfly_sum_left tc_butterfly_sum_right)
qed
show ‹∀⇩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 ((λ(ξ, η). tc_butterfly ξ η) ` (A × B))›
apply (rule eventually_mono)
apply (rule eventually_prodI[where P=‹λF. finite F ∧ F ⊆ A› and Q=‹λG. finite G ∧ G ⊆ B›])
by (auto intro!: f_in_span)
qed
show ‹x ∈ closure (cspan ((λ(ξ, η). tc_butterfly ξ η) ` (A × B)))›
using lim nontriv inside by (rule limit_in_closure)
qed
moreover have ‹cspan (Collect rank1_tc :: ('b,'a) trace_class set) = Collect finite_rank_tc›
using finite_rank_tc_def' by fastforce
moreover have ‹closure (Collect finite_rank_tc :: ('b,'a) trace_class set) = UNIV›
by (rule finite_rank_tc_dense)
ultimately have ‹closure (cspan ((λ(x, y). tc_butterfly x y) ` (A×B))) ⊇ UNIV›
by (smt (verit, del_insts) Un_UNIV_left closed_sum_closure_left closed_sum_cspan closure_closure closure_is_csubspace complex_vector.span_eq_iff complex_vector.subspace_span subset_Un_eq)
then show ?thesis
by (metis ccspan.abs_eq ccspan_UNIV closure_UNIV complex_vector.span_UNIV top.extremum_uniqueI)
qed
lemma separating_set_tc_butterfly: ‹separating_set bounded_clinear ((λ(g,h). tc_butterfly g h) ` (UNIV × UNIV))›
apply (rule separating_set_mono[where S=‹(λ(g, h). tc_butterfly g h) ` (some_chilbert_basis × some_chilbert_basis)›])
by (auto intro!: separating_set_bounded_clinear_dense onb_butterflies_span_trace_class)
lemma separating_set_tc_butterfly_nested:
assumes ‹separating_set (bounded_clinear :: (_ ⇒ 'c::complex_normed_vector) ⇒ _) A›
assumes ‹separating_set (bounded_clinear :: (_ ⇒ 'c conjugate_space) ⇒ _) B›
shows ‹separating_set (bounded_clinear :: (_ ⇒ 'c) ⇒ _) ((λ(g,h). tc_butterfly g h) ` (A × B))›
proof -
from separating_set_tc_butterfly
have ‹separating_set bounded_clinear ((λ(g,h). tc_butterfly g h) ` prod.swap ` (UNIV × UNIV))›
by simp
then have ‹separating_set bounded_clinear ((λ(g,h). tc_butterfly h g) ` (UNIV × UNIV))›
unfolding image_image by simp
then have ‹separating_set (bounded_clinear :: (_ ⇒ 'c) ⇒ _) ((λ(g,h). tc_butterfly h g) ` (B × A))›
apply (rule separating_set_bounded_sesquilinear_nested)
apply (rule bounded_sesquilinear_tc_butterfly)
using assms by auto
then have ‹separating_set (bounded_clinear :: (_ ⇒ 'c) ⇒ _) ((λ(g,h). tc_butterfly h g) ` prod.swap ` (A × B))›
by (smt (verit, del_insts) SigmaE SigmaI eq_from_separatingI image_iff pair_in_swap_image separating_setI)
then show ?thesis
unfolding image_image by simp
qed
unbundle no cblinfun_syntax
end