Theory Backported
section ‹Backported theorems›
text ‹This theory contains various lemmas that are already contained in a fork of the AFP but have
not yet been ported to the official AFP. (Sessions \<^session>‹Complex_Bounded_Operators› and
\<^session>‹Hilbert_Space_Tensor_Product› from 🌐‹https://github.com/dominique-unruh/afp/tree/unruh-edits›.)›
theory Backported
imports Hilbert_Space_Tensor_Product.Trace_Class
Hilbert_Space_Tensor_Product.Hilbert_Space_Tensor_Product
begin
unbundle cblinfun_syntax
lemma abs_summable_norm:
assumes ‹f abs_summable_on A›
shows ‹(λx. norm (f x)) abs_summable_on A›
using assms by simp
lemma abs_summable_on_add:
assumes ‹f abs_summable_on A› and ‹g abs_summable_on A›
shows ‹(λx. f x + g x) abs_summable_on A›
proof -
from assms have ‹(λx. norm (f x) + norm (g x)) summable_on A›
using summable_on_add by blast
then show ?thesis
apply (rule Infinite_Sum.abs_summable_on_comparison_test')
using norm_triangle_ineq by blast
qed
lemma bdd_above_transform_mono_pos:
assumes bdd: ‹bdd_above ((λx. g x) ` M)›
assumes gpos: ‹⋀x. x ∈ M ⟹ g x ≥ 0›
assumes mono: ‹mono_on (Collect ((≤) 0)) f›
shows ‹bdd_above ((λx. f (g x)) ` M)›
proof (cases ‹M = {}›)
case True
then show ?thesis
by simp
next
case False
from bdd obtain B where B: ‹g x ≤ B› if ‹x ∈ M› for x
by (meson bdd_above.unfold imageI)
with gpos False have ‹B ≥ 0›
using dual_order.trans by blast
have ‹f (g x) ≤ f B› if ‹x ∈ M› for x
using mono _ _ B
apply (rule mono_onD)
by (auto intro!: gpos that ‹B ≥ 0›)
then show ?thesis
by fast
qed
lemma Ex_iffI:
assumes ‹⋀x. P x ⟹ Q (f x)›
assumes ‹⋀x. Q x ⟹ P (g x)›
shows ‹Ex P ⟷ Ex Q›
using assms(1) assms(2) by auto
lemma has_sum_Sigma'_banach:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a ⇒ 'b ⇒ 'c::banach›
assumes "((λ(x,y). f x y) has_sum S) (Sigma A B)"
shows ‹((λx. infsum (f x) (B x)) has_sum S) A›
by (metis (no_types, lifting) assms has_sum_cong has_sum_imp_summable has_sum_infsum infsumI infsum_Sigma'_banach summable_on_Sigma_banach)
lemma summable_on_in_cong:
assumes "⋀x. x∈A ⟹ f x = g x"
shows "summable_on_in T f A ⟷ summable_on_in T g A"
by (simp add: summable_on_in_def has_sum_in_cong[OF assms])
lemma infsum_of_bool_scaleC: ‹(∑⇩∞x∈X. of_bool (x=y) *⇩C f x) = of_bool (y∈X) *⇩C f y› for f :: ‹_ ⇒ _::complex_vector›
apply (cases ‹y∈X›)
apply (subst infsum_cong_neutral[where T=‹{y}› and g=f])
apply auto[4]
apply (subst infsum_cong_neutral[where T=‹{}› and g=f])
by auto
lemma infsum_in_0:
assumes ‹Hausdorff_space T› and ‹0 ∈ topspace T›
assumes ‹⋀x. x∈M ⟹ f x = 0›
shows ‹infsum_in T f M = 0›
proof -
have ‹has_sum_in T f M 0›
using assms
by (auto intro!: has_sum_in_0 Hausdorff_imp_t1_space)
then show ?thesis
by (meson assms(1) has_sum_in_infsum_in has_sum_in_unique not_summable_infsum_in_0)
qed
lemma summable_on_in_finite:
fixes f :: ‹'a ⇒ 'b::{comm_monoid_add,topological_space}›
assumes "finite F"
assumes ‹sum f F ∈ topspace T›
shows "summable_on_in T f F"
using assms summable_on_in_def has_sum_in_finite by blast
lemma infsum_Sigma_topological_monoid:
fixes A :: "'a set" and B :: "'a ⇒ 'b set"
and f :: ‹'a × 'b ⇒ 'c::{topological_comm_monoid_add, t3_space}›
assumes summableAB: "f summable_on (Sigma A B)"
assumes summableB: ‹⋀x. x∈A ⟹ (λy. f (x, y)) summable_on (B x)›
shows "infsum f (Sigma A B) = (∑⇩∞x∈A. ∑⇩∞y∈B x. f (x, y))"
proof -
have 1: ‹(f has_sum infsum f (Sigma A B)) (Sigma A B)›
by (simp add: assms)
define b where ‹b x = (∑⇩∞y∈B x. f (x, y))› for x
have 2: ‹((λy. f (x, y)) has_sum b x) (B x)› if ‹x ∈ A› for x
using b_def assms(2) that by auto
have 3: ‹(b has_sum (∑⇩∞x∈A. b x)) A›
using 1 2 by (metis has_sum_SigmaD infsumI)
have 4: ‹(f has_sum (∑⇩∞x∈A. b x)) (Sigma A B)›
using 2 3 apply (rule has_sum_SigmaI)
using assms by auto
from 1 4 show ?thesis
using b_def[abs_def] infsumI by blast
qed
lemma ballI2 [intro!]: "(⋀x y. (x,y) ∈ A ⟹ P x y) ⟹ ∀(x,y)∈A. P x y"
by auto
lemma flip_eq_const: ‹(λy. y = x) = ((=) x)›
by auto
lemma vector_to_cblinfun_inj: ‹inj_on (vector_to_cblinfun :: 'a::complex_normed_vector ⇒ 'b::one_dim ⇒⇩C⇩L _) X›
proof (rule inj_onI)
fix x y :: 'a
assume ‹vector_to_cblinfun x = (vector_to_cblinfun y :: 'b ⇒⇩C⇩L _)›
then have ‹vector_to_cblinfun x (1::'b) = vector_to_cblinfun y (1::'b)›
by simp
then show ‹x = y›
by simp
qed
lemma has_sum_bounded_clinear:
assumes "bounded_clinear h" and "(f has_sum S) A"
shows "((λx. h (f x)) has_sum h S) A"
apply (rule has_sum_bounded_linear[where h=h])
by (auto intro!: bounded_clinear.bounded_linear assms)
lemma has_sum_scaleC_right:
fixes f :: ‹'a ⇒ 'b :: complex_normed_vector›
assumes ‹(f has_sum s) A›
shows ‹((λx. c *⇩C f x) has_sum c *⇩C s) A›
apply (rule has_sum_bounded_clinear[where h=‹(*⇩C) c›])
using bounded_clinear_scaleC_right assms by auto
lemma norm_cblinfun_bound_both_sides:
fixes a :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_inner›
assumes ‹b ≥ 0›
assumes leq: ‹⋀ψ φ. norm ψ = 1 ⟹ norm φ = 1 ⟹ norm (ψ ∙⇩C a φ) ≤ b›
shows ‹norm a ≤ b›
proof -
wlog not_singleton: ‹class.not_singleton TYPE('a)›
apply (subst not_not_singleton_cblinfun_zero)
by (simp_all add: negation assms)
have ‹norm a = (⨆(ψ, φ). cmod (ψ ∙⇩C (a *⇩V φ)) / (norm ψ * norm φ))›
apply (rule cinner_sup_norm_cblinfun[internalize_sort' 'a])
apply (rule complex_normed_vector_axioms)
by (fact not_singleton)
also have ‹… ≤ b›
proof (rule cSUP_least)
show ‹UNIV ≠ {}›
by simp
fix x :: ‹'b × 'a›
obtain ψ φ where x: ‹x = (ψ, φ)›
by fastforce
have ‹(case x of (ψ, φ) ⇒ cmod (ψ ∙⇩C (a *⇩V φ)) / (norm ψ * norm φ)) = cmod (ψ ∙⇩C a φ) / (norm ψ * norm φ)›
using x by force
also have ‹… = cmod (sgn ψ ∙⇩C a (sgn φ))›
by (simp add: sgn_div_norm cblinfun.scaleR_right divide_inverse_commute norm_inverse norm_mult)
also have ‹… ≤ b›
apply (cases ‹ψ = 0›, simp add: assms)
apply (cases ‹φ = 0›, simp add: assms)
apply (rule leq)
by (simp_all add: norm_sgn)
finally show ‹(case x of (ψ, φ) ⇒ cmod (ψ ∙⇩C (a *⇩V φ)) / (norm ψ * norm φ)) ≤ b›
by -
qed
finally show ?thesis
by -
qed
lemma has_sum_in_weaker_topology:
assumes ‹continuous_map T U (λf. f)›
assumes ‹has_sum_in T f A l›
shows ‹has_sum_in U f A l›
using continuous_map_limit[OF assms(1)]
using assms(2)
by (auto simp: has_sum_in_def o_def)
lemma summable_on_in_weaker_topology:
assumes ‹continuous_map T U (λf. f)›
assumes ‹summable_on_in T f A›
shows ‹summable_on_in U f A›
by (meson assms(1,2) has_sum_in_weaker_topology summable_on_in_def)
lemma summable_imp_wot_summable:
assumes ‹f summable_on A›
shows ‹summable_on_in cweak_operator_topology f A›
apply (rule summable_on_in_weaker_topology)
apply (rule cweak_operator_topology_weaker_than_euclidean)
by (simp add: assms summable_on_euclidean_eq)
lemma triangle_ineq_wot:
assumes ‹f abs_summable_on A›
shows ‹norm (infsum_in cweak_operator_topology f A) ≤ (∑⇩∞x∈A. norm (f x))›
proof -
wlog summable: ‹summable_on_in cweak_operator_topology f A›
by (simp add: infsum_nonneg negation not_summable_infsum_in_0)
have ‹cmod (ψ ∙⇩C (infsum_in cweak_operator_topology f A *⇩V φ)) ≤ (∑⇩∞x∈A. norm (f x))›
if ‹norm ψ = 1› and ‹norm φ = 1› for ψ φ
proof -
have sum1: ‹(λa. ψ ∙⇩C (f a *⇩V φ)) abs_summable_on A›
by (metis local.summable summable_on_iff_abs_summable_on_complex summable_on_in_cweak_operator_topology_pointwise)
have ‹ψ ∙⇩C infsum_in cweak_operator_topology f A φ = (∑⇩∞a∈A. ψ ∙⇩C f a φ)›
using summable by (rule infsum_in_cweak_operator_topology_pointwise)
then have ‹cmod (ψ ∙⇩C (infsum_in cweak_operator_topology f A *⇩V φ)) = norm (∑⇩∞a∈A. ψ ∙⇩C f a φ)›
by presburger
also have ‹… ≤ (∑⇩∞a∈A. norm (ψ ∙⇩C f a φ))›
apply (rule norm_infsum_bound)
by (metis summable summable_on_iff_abs_summable_on_complex
summable_on_in_cweak_operator_topology_pointwise)
also have ‹… ≤ (∑⇩∞a∈A. norm (f a))›
using sum1 assms apply (rule infsum_mono)
by (smt (verit) complex_inner_class.Cauchy_Schwarz_ineq2 mult_cancel_left1 mult_cancel_right1 norm_cblinfun that(1,2))
finally show ?thesis
by -
qed
then show ?thesis
apply (rule_tac norm_cblinfun_bound_both_sides)
by (auto simp: infsum_nonneg)
qed
lemma trace_tc_butterfly: ‹trace_tc (tc_butterfly x y) = y ∙⇩C x›
apply (transfer fixing: x y)
by (rule trace_butterfly)
lemma sandwich_tensor_ell2_right': ‹sandwich (tensor_ell2_right ψ) *⇩V a = a ⊗⇩o selfbutter ψ›
apply (rule cblinfun_cinner_tensor_eqI)
by (simp add: sandwich_apply tensor_op_ell2 cblinfun.scaleC_right)
lemma sandwich_tensor_ell2_left': ‹sandwich (tensor_ell2_left ψ) *⇩V a = selfbutter ψ ⊗⇩o a›
apply (rule cblinfun_cinner_tensor_eqI)
by (simp add: sandwich_apply tensor_op_ell2 cblinfun.scaleC_right)
lemma to_conjugate_space_0[simp]: ‹to_conjugate_space 0 = 0›
by (simp add: zero_conjugate_space.abs_eq)
lemma from_conjugate_space_0[simp]: ‹from_conjugate_space 0 = 0›
using zero_conjugate_space.rep_eq by blast
lemma antilinear_eq_0_on_span:
assumes ‹antilinear f›
and ‹⋀x. x ∈ b ⟹ f x = 0›
and ‹x ∈ cspan b›
shows ‹f x = 0›
proof -
from assms(1)
have ‹clinear (λx. to_conjugate_space (f x))›
apply (rule antilinear_o_antilinear[unfolded o_def])
by simp
then have ‹to_conjugate_space (f x) = 0›
apply (rule complex_vector.linear_eq_0_on_span)
using assms by auto
then have ‹from_conjugate_space (to_conjugate_space (f x)) = 0›
by simp
then show ?thesis
by (simp add: to_conjugate_space_inverse)
qed
lemma antilinear_diff:
assumes ‹antilinear f› and ‹antilinear g›
shows ‹antilinear (λx. f x - g x)›
apply (rule antilinearI)
apply (metis add_diff_add additive.add antilinear_def assms(1,2))
by (simp add: antilinear.scaleC assms(1,2) scaleC_right.diff)
lemma antilinear_cinner:
shows ‹antilinear (λx. x ∙⇩C y)›
by (simp add: antilinearI cinner_add_left)
lemma cinner_extensionality_basis:
fixes g h :: ‹'a::complex_inner›
assumes ‹ccspan B = ⊤›
assumes ‹⋀x. x ∈ B ⟹ x ∙⇩C g = x ∙⇩C h›
shows ‹g = h›
proof (rule cinner_extensionality)
fix y :: 'a
have ‹y ∈ closure (cspan B)›
using assms(1) ccspan.rep_eq by fastforce
then obtain x where ‹x ⇢ y› and xB: ‹x i ∈ cspan B› for i
using closure_sequential by blast
have lin: ‹antilinear (λa. a ∙⇩C g - a ∙⇩C h)›
by (intro antilinear_diff antilinear_cinner)
from lin have ‹x i ∙⇩C g - x i ∙⇩C h = 0› for i
apply (rule antilinear_eq_0_on_span[of _ B])
using xB assms by auto
then have ‹(λi. x i ∙⇩C g - x i ∙⇩C h) ⇢ 0› for i
by simp
moreover have ‹(λi. x i ∙⇩C g - x i ∙⇩C h) ⇢ y ∙⇩C g - y ∙⇩C h›
apply (rule_tac continuous_imp_tendsto[unfolded o_def, OF _ ‹x ⇢ y›])
by simp
ultimately have ‹y ∙⇩C g - y ∙⇩C h = 0›
using LIMSEQ_unique by blast
then show ‹y ∙⇩C g = y ∙⇩C h›
by simp
qed
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)
lemma infsum_in_finite:
assumes "finite F"
assumes ‹Hausdorff_space T›
assumes ‹sum f F ∈ topspace T›
shows "infsum_in T f F = sum f F"
using has_sum_in_finite[OF assms(1,3)]
using assms(2) has_sum_in_infsum_in has_sum_in_unique summable_on_in_def by blast
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))
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
declare compose_tcr.bounded_cbilinear_axioms[bounded_cbilinear]
lemma sandwich_butterfly: ‹sandwich a (butterfly x y) = butterfly (a x) (a y)›
by (simp add: sandwich_apply butterfly_comp_cblinfun cblinfun_comp_butterfly)
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 is_Proj_leq_id: ‹is_Proj P ⟹ P ≤ id_cblinfun›
by (metis diff_ge_0_iff_ge is_Proj_algebraic is_Proj_complement positive_cblinfun_squareI)
lemma sum_butterfly_leq_id:
assumes ‹is_ortho_set E›
assumes ‹⋀e. e∈E ⟹ norm e = 1›
shows ‹(∑i∈E. butterfly i i) ≤ id_cblinfun›
proof -
have ‹is_Proj (∑ψ∈E. butterfly ψ ψ)›
using assms by (rule sum_butterfly_is_Proj)
then show ?thesis
by (auto intro!: is_Proj_leq_id)
qed
lemma eq_from_separatingI2x:
assumes ‹separating_set P ((λ(x,y). h x y) ` (S×T))›
assumes ‹P f› and ‹P g›
assumes ‹⋀x y. x ∈ S ⟹ y ∈ T ⟹ f (h x y) = g (h x y)›
shows ‹f x = g x›
using assms eq_from_separatingI2 by blast
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)
end