Theory Complex_Bounded_Linear_Function
section ‹‹Complex_Bounded_Linear_Function› -- Complex bounded linear functions (bounded operators)›
theory Complex_Bounded_Linear_Function
imports
"HOL-Types_To_Sets.Types_To_Sets"
Banach_Steinhaus.Banach_Steinhaus
Complex_Inner_Product
One_Dimensional_Spaces
Complex_Bounded_Linear_Function0
"HOL-Library.Function_Algebras"
begin
unbundle lattice_syntax
subsection ‹Misc basic facts and declarations›
notation cblinfun_apply (infixr "*⇩V" 70)
lemma id_cblinfun_apply[simp]: "id_cblinfun *⇩V ψ = ψ"
by simp
lemma apply_id_cblinfun[simp]: ‹(*⇩V) id_cblinfun = id›
by auto
lemma isCont_cblinfun_apply[simp]: "isCont ((*⇩V) A) ψ"
by transfer (simp add: clinear_continuous_at)
declare cblinfun.scaleC_left[simp]
lemma cblinfun_apply_clinear[simp]: ‹clinear (cblinfun_apply A)›
using bounded_clinear.axioms(1) cblinfun_apply by blast
lemma cblinfun_cinner_eqI:
fixes A B :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀ψ. norm ψ = 1 ⟹ cinner ψ (A *⇩V ψ) = cinner ψ (B *⇩V ψ)›
shows ‹A = B›
proof -
define C where ‹C = A - B›
have C0[simp]: ‹cinner ψ (C ψ) = 0› for ψ
apply (cases ‹ψ = 0›)
using assms[of ‹sgn ψ›]
by (simp_all add: C_def norm_sgn sgn_div_norm cblinfun.scaleR_right assms cblinfun.diff_left cinner_diff_right)
{ fix f g α
have ‹0 = cinner (f + α *⇩C g) (C *⇩V (f + α *⇩C g))›
by (simp add: cinner_diff_right minus_cblinfun.rep_eq)
also have ‹… = α *⇩C cinner f (C g) + cnj α *⇩C cinner g (C f)›
by (smt (z3) C0 add.commute add.right_neutral cblinfun.add_right cblinfun.scaleC_right cblinfun_cinner_right.rep_eq cinner_add_left cinner_scaleC_left complex_scaleC_def)
finally have ‹α *⇩C cinner f (C g) = - cnj α *⇩C cinner g (C f)›
by (simp add: eq_neg_iff_add_eq_0)
}
then have ‹cinner f (C g) = 0› for f g
by (metis complex_cnj_i complex_cnj_one complex_vector.scale_cancel_right complex_vector.scale_left_imp_eq equation_minus_iff i_squared mult_eq_0_iff one_neq_neg_one)
then have ‹C g = 0› for g
using cinner_eq_zero_iff by blast
then have ‹C = 0›
by (simp add: cblinfun_eqI)
then show ‹A = B›
using C_def by auto
qed
lemma id_cblinfun_not_0[simp]: ‹(id_cblinfun :: 'a::{complex_normed_vector, not_singleton} ⇒⇩C⇩L _) ≠ 0›
by (metis (full_types) Extra_General.UNIV_not_singleton cblinfun.zero_left cblinfun_id_cblinfun_apply ex_norm1 norm_zero one_neq_zero)
lemma cblinfun_norm_geqI:
assumes ‹norm (f *⇩V x) / norm x ≥ K›
shows ‹norm f ≥ K›
using assms by transfer (smt (z3) bounded_clinear.bounded_linear le_onorm)
declare scaleC_conv_of_complex[simp]
lemma cblinfun_eq_0_on_span:
fixes S::‹'a::complex_normed_vector set›
assumes "x ∈ cspan S"
and "⋀s. s∈S ⟹ F *⇩V s = 0"
shows ‹F *⇩V x = 0›
using bounded_clinear.axioms(1) cblinfun_apply assms complex_vector.linear_eq_0_on_span
by blast
lemma cblinfun_eq_on_span:
fixes S::‹'a::complex_normed_vector set›
assumes "x ∈ cspan S"
and "⋀s. s∈S ⟹ F *⇩V s = G *⇩V s"
shows ‹F *⇩V x = G *⇩V x›
using bounded_clinear.axioms(1) cblinfun_apply assms complex_vector.linear_eq_on_span
by blast
lemma cblinfun_eq_0_on_UNIV_span:
fixes basis::‹'a::complex_normed_vector set›
assumes "cspan basis = UNIV"
and "⋀s. s∈basis ⟹ F *⇩V s = 0"
shows ‹F = 0›
by (metis cblinfun_eq_0_on_span UNIV_I assms cblinfun.zero_left cblinfun_eqI)
lemma cblinfun_eq_on_UNIV_span:
fixes basis::"'a::complex_normed_vector set" and φ::"'a ⇒ 'b::complex_normed_vector"
assumes "cspan basis = UNIV"
and "⋀s. s∈basis ⟹ F *⇩V s = G *⇩V s"
shows ‹F = G›
by (metis (no_types) assms cblinfun_eqI cblinfun_eq_on_span iso_tuple_UNIV_I)
lemma cblinfun_eq_on_canonical_basis:
fixes f g::"'a::{basis_enum,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector"
defines "basis == set (canonical_basis::'a list)"
assumes "⋀u. u ∈ basis ⟹ f *⇩V u = g *⇩V u"
shows "f = g"
using assms cblinfun_eq_on_UNIV_span is_generator_set by blast
lemma cblinfun_eq_0_on_canonical_basis:
fixes f ::"'a::{basis_enum,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector"
defines "basis == set (canonical_basis::'a list)"
assumes "⋀u. u ∈ basis ⟹ f *⇩V u = 0"
shows "f = 0"
by (simp add: assms cblinfun_eq_on_canonical_basis)
lemma cinner_canonical_basis_eq_0:
defines "basisA == set (canonical_basis::'a::onb_enum list)"
and "basisB == set (canonical_basis::'b::onb_enum list)"
assumes "⋀u v. u∈basisA ⟹ v∈basisB ⟹ is_orthogonal v (F *⇩V u)"
shows "F = 0"
proof-
have "F *⇩V u = 0"
if "u∈basisA" for u
proof-
have "⋀v. v∈basisB ⟹ is_orthogonal v (F *⇩V u)"
by (simp add: assms(3) that)
moreover have "(⋀v. v∈basisB ⟹ is_orthogonal v x) ⟹ x = 0"
for x
proof-
assume r1: "⋀v. v∈basisB ⟹ is_orthogonal v x"
have "is_orthogonal v x" for v
proof-
have "cspan basisB = UNIV"
using basisB_def is_generator_set by auto
hence "v ∈ cspan basisB"
by (smt iso_tuple_UNIV_I)
hence "∃t s. v = (∑a∈t. s a *⇩C a) ∧ finite t ∧ t ⊆ basisB"
using complex_vector.span_explicit
by (smt mem_Collect_eq)
then obtain t s where b1: "v = (∑a∈t. s a *⇩C a)" and b2: "finite t" and b3: "t ⊆ basisB"
by blast
have "v ∙⇩C x = (∑a∈t. s a *⇩C a) ∙⇩C x"
by (simp add: b1)
also have "… = (∑a∈t. (s a *⇩C a) ∙⇩C x)"
using cinner_sum_left by blast
also have "… = (∑a∈t. cnj (s a) * (a ∙⇩C x))"
by auto
also have "… = 0"
using b3 r1 subsetD by force
finally show ?thesis by simp
qed
thus ?thesis
by (simp add: ‹⋀v. (v ∙⇩C x) = 0› cinner_extensionality)
qed
ultimately show ?thesis by simp
qed
thus ?thesis
using basisA_def cblinfun_eq_0_on_canonical_basis by auto
qed
lemma cinner_canonical_basis_eq:
defines "basisA == set (canonical_basis::'a::onb_enum list)"
and "basisB == set (canonical_basis::'b::onb_enum list)"
assumes "⋀u v. u∈basisA ⟹ v∈basisB ⟹ v ∙⇩C (F *⇩V u) = v ∙⇩C (G *⇩V u)"
shows "F = G"
proof-
define H where "H = F - G"
have "⋀u v. u∈basisA ⟹ v∈basisB ⟹ is_orthogonal v (H *⇩V u)"
unfolding H_def
by (simp add: assms(3) cinner_diff_right minus_cblinfun.rep_eq)
hence "H = 0"
by (simp add: basisA_def basisB_def cinner_canonical_basis_eq_0)
thus ?thesis unfolding H_def by simp
qed
lemma cinner_canonical_basis_eq':
defines "basisA == set (canonical_basis::'a::onb_enum list)"
and "basisB == set (canonical_basis::'b::onb_enum list)"
assumes "⋀u v. u∈basisA ⟹ v∈basisB ⟹ (F *⇩V u) ∙⇩C v = (G *⇩V u) ∙⇩C v"
shows "F = G"
using cinner_canonical_basis_eq assms
by (metis cinner_commute')
lemma not_not_singleton_cblinfun_zero:
‹x = 0› if ‹¬ class.not_singleton TYPE('a)› for x :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
apply (rule cblinfun_eqI)
apply (subst not_not_singleton_zero[OF that])
by simp
lemma cblinfun_norm_approx_witness:
fixes A :: ‹'a::{not_singleton,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹ε > 0›
shows ‹∃ψ. norm (A *⇩V ψ) ≥ norm A - ε ∧ norm ψ = 1›
proof (transfer fixing: ε)
fix A :: ‹'a ⇒ 'b› assume [simp]: ‹bounded_clinear A›
have ‹∃y∈{norm (A x) |x. norm x = 1}. y > ⨆ {norm (A x) |x. norm x = 1} - ε›
apply (rule Sup_real_close)
using assms by (auto simp: ex_norm1 bounded_clinear.bounded_linear bdd_above_norm_f)
also have ‹⨆ {norm (A x) |x. norm x = 1} = onorm A›
by (simp add: bounded_clinear.bounded_linear onorm_sphere)
finally
show ‹∃ψ. onorm A - ε ≤ norm (A ψ) ∧ norm ψ = 1›
by force
qed
lemma cblinfun_norm_approx_witness_mult:
fixes A :: ‹'a::{not_singleton,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹ε < 1›
shows ‹∃ψ. norm (A *⇩V ψ) ≥ norm A * ε ∧ norm ψ = 1›
proof (cases ‹norm A = 0›)
case True
then show ?thesis
by auto (simp add: ex_norm1)
next
case False
then have ‹(1 - ε) * norm A > 0›
using assms by fastforce
then obtain ψ where geq: ‹norm (A *⇩V ψ) ≥ norm A - ((1 - ε) * norm A)› and ‹norm ψ = 1›
using cblinfun_norm_approx_witness by blast
have ‹norm A * ε = norm A - (1 - ε) * norm A›
by (simp add: mult.commute right_diff_distrib')
also have ‹… ≤ norm (A *⇩V ψ)›
by (rule geq)
finally show ?thesis
using ‹norm ψ = 1› by auto
qed
lemma cblinfun_norm_approx_witness':
fixes A :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹ε > 0›
shows ‹∃ψ. norm (A *⇩V ψ) / norm ψ ≥ norm A - ε›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
obtain ψ where ‹norm (A *⇩V ψ) ≥ norm A - ε› and ‹norm ψ = 1›
apply atomize_elim
using complex_normed_vector_axioms True assms
by (rule cblinfun_norm_approx_witness[internalize_sort' 'a])
then have ‹norm (A *⇩V ψ) / norm ψ ≥ norm A - ε›
by simp
then show ?thesis
by auto
next
case False
show ?thesis
apply (subst not_not_singleton_cblinfun_zero[OF False])
apply simp
apply (subst not_not_singleton_cblinfun_zero[OF False])
using ‹ε > 0› by simp
qed
lemma cblinfun_to_CARD_1_0[simp]: ‹(A :: _ ⇒⇩C⇩L _::CARD_1) = 0›
by (simp add: cblinfun_eqI)
lemma cblinfun_from_CARD_1_0[simp]: ‹(A :: _::CARD_1 ⇒⇩C⇩L _) = 0›
using cblinfun_eq_on_UNIV_span by force
lemma cblinfun_cspan_UNIV:
fixes basis :: ‹('a::{complex_normed_vector,cfinite_dim} ⇒⇩C⇩L 'b::complex_normed_vector) set›
and basisA :: ‹'a set› and basisB :: ‹'b set›
assumes ‹cspan basisA = UNIV› and ‹cspan basisB = UNIV›
assumes basis: ‹⋀a b. a∈basisA ⟹ b∈basisB ⟹ ∃F∈basis. ∀a'∈basisA. F *⇩V a' = (if a'=a then b else 0)›
shows ‹cspan basis = UNIV›
proof -
obtain basisA' where ‹basisA' ⊆ basisA› and ‹cindependent basisA'› and ‹cspan basisA' = UNIV›
by (metis assms(1) complex_vector.maximal_independent_subset complex_vector.span_eq top_greatest)
then have [simp]: ‹finite basisA'›
by (simp add: cindependent_cfinite_dim_finite)
have basis': ‹⋀a b. a∈basisA' ⟹ b∈basisB ⟹ ∃F∈basis. ∀a'∈basisA'. F *⇩V a' = (if a'=a then b else 0)›
using basis ‹basisA' ⊆ basisA› by fastforce
obtain F where F: ‹F a b ∈ basis ∧ F a b *⇩V a' = (if a'=a then b else 0)›
if ‹a∈basisA'› ‹b∈basisB› ‹a'∈basisA'› for a b a'
apply atomize_elim apply (intro choice allI)
using basis' by metis
then have F_apply: ‹F a b *⇩V a' = (if a'=a then b else 0)›
if ‹a∈basisA'› ‹b∈basisB› ‹a'∈basisA'› for a b a'
using that by auto
have F_basis: ‹F a b ∈ basis›
if ‹a∈basisA'› ‹b∈basisB› for a b
using that F by auto
have b_span: ‹∃G∈cspan {F a b|b. b∈basisB}. ∀a'∈basisA'. G *⇩V a' = (if a'=a then b else 0)› if ‹a∈basisA'› for a b
proof -
from ‹cspan basisB = UNIV›
obtain r t where ‹finite t› and ‹t ⊆ basisB› and b_lincom: ‹b = (∑a∈t. r a *⇩C a)›
unfolding complex_vector.span_alt by atomize_elim blast
define G where ‹G = (∑i∈t. r i *⇩C F a i)›
have ‹G ∈ cspan {F a b|b. b∈basisB}›
using ‹finite t› ‹t ⊆ basisB› unfolding G_def
by (smt (verit) complex_vector.span_scale complex_vector.span_sum complex_vector.span_superset mem_Collect_eq subsetD)
moreover have ‹G *⇩V a' = (if a'=a then b else 0)› if ‹a'∈basisA'› for a'
using ‹t ⊆ basisB› ‹a∈basisA'› ‹a'∈basisA'›
by (auto simp: b_lincom G_def cblinfun.sum_left F_apply intro!: sum.neutral sum.cong)
ultimately show ?thesis
by blast
qed
have a_span: ‹cspan (⋃a∈basisA'. cspan {F a b|b. b∈basisB}) = UNIV›
proof (intro equalityI subset_UNIV subsetI, rename_tac H)
fix H
obtain G where G: ‹G a b ∈ cspan {F a b|b. b∈basisB} ∧ G a b *⇩V a' = (if a'=a then b else 0)›
if ‹a∈basisA'› and ‹a'∈basisA'› for a b a'
apply atomize_elim apply (intro choice allI)
using b_span by blast
then have G_cspan: ‹G a b ∈ cspan {F a b|b. b∈basisB}› if ‹a∈basisA'› for a b
using that by auto
from G have G: ‹G a b *⇩V a' = (if a'=a then b else 0)› if ‹a∈basisA'› and ‹a'∈basisA'› for a b a'
using that by auto
define H' where ‹H' = (∑a∈basisA'. G a (H *⇩V a))›
have ‹H' ∈ cspan (⋃a∈basisA'. cspan {F a b|b. b∈basisB})›
unfolding H'_def using G_cspan
by (smt (verit, del_insts) UN_iff complex_vector.span_clauses(1) complex_vector.span_sum)
moreover have ‹H' = H›
using ‹cspan basisA' = UNIV›
by (auto simp: H'_def cblinfun_eq_on_UNIV_span cblinfun.sum_left G)
ultimately show ‹H ∈ cspan (⋃a∈basisA'. cspan {F a b |b. b ∈ basisB})›
by simp
qed
moreover have ‹cspan basis ⊇ cspan (⋃a∈basisA'. cspan {F a b|b. b∈basisB})›
by (smt (verit) F_basis UN_subset_iff complex_vector.span_base complex_vector.span_minimal complex_vector.subspace_span mem_Collect_eq subsetI)
ultimately show ‹cspan basis = UNIV›
by auto
qed
instance cblinfun :: (‹{cfinite_dim,complex_normed_vector}›, ‹{cfinite_dim,complex_normed_vector}›) cfinite_dim
proof intro_classes
obtain basisA :: ‹'a set› where [simp]: ‹cspan basisA = UNIV› ‹cindependent basisA› ‹finite basisA›
using finite_basis by blast
obtain basisB :: ‹'b set› where [simp]: ‹cspan basisB = UNIV› ‹cindependent basisB› ‹finite basisB›
using finite_basis by blast
define f where ‹f a b = cconstruct basisA (λx. if x=a then b else 0)› for a :: 'a and b :: 'b
have f_a: ‹f a b a = b› if ‹a : basisA› for a b
by (simp add: complex_vector.construct_basis f_def that)
have f_not_a: ‹f a b c = 0› if ‹a : basisA› and ‹c : basisA› and ‹a ≠ c›for a b c
using that by (simp add: complex_vector.construct_basis f_def)
define F where ‹F a b = CBlinfun (f a b)› for a b
have ‹clinear (f a b)› for a b
by (auto intro: complex_vector.linear_construct simp: f_def)
then have ‹bounded_clinear (f a b)› for a b
by auto
then have F_apply: ‹cblinfun_apply (F a b) = f a b› for a b
by (simp add: F_def bounded_clinear_CBlinfun_apply)
define basis where ‹basis = {F a b| a b. a∈basisA ∧ b∈basisB}›
have "⋀a b. ⟦a ∈ basisA; b ∈ basisB⟧ ⟹ ∃F∈basis. ∀a'∈basisA. F *⇩V a' = (if a' = a then b else 0)"
by (smt (verit, del_insts) F_apply basis_def f_a f_not_a mem_Collect_eq)
then have ‹cspan basis = UNIV›
by (metis ‹cspan basisA = UNIV› ‹cspan basisB = UNIV› cblinfun_cspan_UNIV)
moreover have ‹finite basis›
unfolding basis_def by (auto intro: finite_image_set2)
ultimately show ‹∃S :: ('a ⇒⇩C⇩L 'b) set. finite S ∧ cspan S = UNIV›
by auto
qed
lemma norm_cblinfun_bound_dense:
assumes ‹0 ≤ b›
assumes S: ‹closure S = UNIV›
assumes bound: ‹⋀x. x∈S ⟹ norm (cblinfun_apply f x) ≤ b * norm x›
shows ‹norm f ≤ b›
proof -
have 1: ‹continuous_on UNIV (λa. norm (f *⇩V a))›
by (simp add: continuous_on_eq_continuous_within)
have 2: ‹continuous_on UNIV (λa. b * norm a)›
using continuous_on_mult_left continuous_on_norm_id by blast
have ‹norm (cblinfun_apply f x) ≤ b * norm x› for x
by (metis (mono_tags, lifting) UNIV_I S bound 1 2 on_closure_leI)
then show ‹norm f ≤ b›
using ‹0 ≤ b› norm_cblinfun_bound by blast
qed
lemma infsum_cblinfun_apply:
assumes ‹g summable_on S›
shows ‹infsum (λx. A *⇩V g x) S = A *⇩V (infsum g S)›
using infsum_bounded_linear[unfolded o_def] assms cblinfun.real.bounded_linear_right by blast
lemma has_sum_cblinfun_apply:
assumes ‹(g has_sum x) S›
shows ‹((λx. A *⇩V g x) has_sum (A *⇩V x)) S›
using assms has_sum_bounded_linear[unfolded o_def] using cblinfun.real.bounded_linear_right by blast
lemma abs_summable_on_cblinfun_apply:
assumes ‹g abs_summable_on S›
shows ‹(λx. A *⇩V g x) abs_summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_right] assms
by (rule abs_summable_on_bounded_linear[unfolded o_def])
lemma summable_on_cblinfun_apply:
assumes ‹g summable_on S›
shows ‹(λx. A *⇩V g x) summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_right] assms
by (rule summable_on_bounded_linear[unfolded o_def])
lemma summable_on_cblinfun_apply_left:
assumes ‹A summable_on S›
shows ‹(λx. A x *⇩V g) summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_left] assms
by (rule summable_on_bounded_linear[unfolded o_def])
lemma abs_summable_on_cblinfun_apply_left:
assumes ‹A abs_summable_on S›
shows ‹(λx. A x *⇩V g) abs_summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_left] assms
by (rule abs_summable_on_bounded_linear[unfolded o_def])
lemma infsum_cblinfun_apply_left:
assumes ‹A summable_on S›
shows ‹infsum (λx. A x *⇩V g) S = (infsum A S) *⇩V g›
apply (rule infsum_bounded_linear[unfolded o_def, of ‹λA. cblinfun_apply A g›])
using assms
by (auto simp add: bounded_clinear.bounded_linear bounded_cbilinear_cblinfun_apply)
lemma has_sum_cblinfun_apply_left:
assumes ‹(A has_sum x) S›
shows ‹((λx. A x *⇩V g) has_sum (x *⇩V g)) S›
apply (rule has_sum_bounded_linear[unfolded o_def, of ‹λA. cblinfun_apply A g›])
using assms by (auto simp add: bounded_clinear.bounded_linear cblinfun.bounded_clinear_left)
text ‹The next eight lemmas logically belong in \<^theory>‹Complex_Bounded_Operators.Complex_Inner_Product›
but the proofs use facts from this theory.›
lemma has_sum_cinner_left:
assumes ‹(f has_sum x) I›
shows ‹((λi. cinner a (f i)) has_sum cinner a x) I›
by (metis assms cblinfun_cinner_right.rep_eq has_sum_cblinfun_apply)
lemma summable_on_cinner_left:
assumes ‹f summable_on I›
shows ‹(λi. cinner a (f i)) summable_on I›
by (metis assms has_sum_cinner_left summable_on_def)
lemma infsum_cinner_left:
assumes ‹φ summable_on I›
shows ‹cinner ψ (∑⇩∞i∈I. φ i) = (∑⇩∞i∈I. cinner ψ (φ i))›
by (metis assms has_sum_cinner_left has_sum_infsum infsumI)
lemma has_sum_cinner_right:
assumes ‹(f has_sum x) I›
shows ‹((λi. f i ∙⇩C a) has_sum (x ∙⇩C a)) I›
using assms has_sum_bounded_linear[unfolded o_def] bounded_antilinear.bounded_linear
bounded_antilinear_cinner_left by blast
lemma summable_on_cinner_right:
assumes ‹f summable_on I›
shows ‹(λi. f i ∙⇩C a) summable_on I›
by (metis assms has_sum_cinner_right summable_on_def)
lemma infsum_cinner_right:
assumes ‹φ summable_on I›
shows ‹(∑⇩∞i∈I. φ i) ∙⇩C ψ = (∑⇩∞i∈I. φ i ∙⇩C ψ)›
by (metis assms has_sum_cinner_right has_sum_infsum infsumI)
lemma Cauchy_cinner_product_summable:
assumes asum: ‹a summable_on UNIV›
assumes bsum: ‹b summable_on UNIV›
assumes ‹finite X› ‹finite Y›
assumes pos: ‹⋀x y. x ∉ X ⟹ y ∉ Y ⟹ cinner (a x) (b y) ≥ 0›
shows absum: ‹(λ(x, y). cinner (a x) (b y)) summable_on UNIV›
proof -
have ‹(∑(x,y)∈F. norm (cinner (a x) (b y))) ≤ norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) + norm (infsum b (-Y)) + 1›
if ‹finite F› and ‹F ⊆ (-X)×(-Y)› for F
proof -
from asum ‹finite X›
have ‹a summable_on (-X)›
by (simp add: Compl_eq_Diff_UNIV summable_on_cofin_subset)
then obtain MA where ‹finite MA› and ‹MA ⊆ -X›
and MA: ‹G ⊇ MA ⟹ G ⊆ -X ⟹ finite G ⟹ norm (sum a G - infsum a (-X)) ≤ 1› for G
apply (simp add: summable_iff_has_sum_infsum has_sum_metric dist_norm)
by (meson less_eq_real_def zero_less_one)
from bsum ‹finite Y›
have ‹b summable_on (-Y)›
by (simp add: Compl_eq_Diff_UNIV summable_on_cofin_subset)
then obtain MB where ‹finite MB› and ‹MB ⊆ -Y›
and MB: ‹G ⊇ MB ⟹ G ⊆ -Y ⟹ finite G ⟹ norm (sum b G - infsum b (-Y)) ≤ 1› for G
apply (simp add: summable_iff_has_sum_infsum has_sum_metric dist_norm)
by (meson less_eq_real_def zero_less_one)
define F1 F2 where ‹F1 = fst ` F ∪ MA› and ‹F2 = snd ` F ∪ MB›
define t1 t2 where ‹t1 = sum a F1 - infsum a (-X)› and ‹t2 = sum b F2 - infsum b (-Y)›
have [simp]: ‹finite F1› ‹finite F2›
using F1_def F2_def ‹finite MA› ‹finite MB› that by auto
have [simp]: ‹F1 ⊆ -X› ‹F2 ⊆ -Y›
using ‹F ⊆ (-X)×(-Y)› ‹MA ⊆ -X› ‹MB ⊆ -Y›
by (auto simp: F1_def F2_def)
from MA[OF _ ‹F1 ⊆ -X› ‹finite F1›] have ‹norm t1 ≤ 1›
by (auto simp: t1_def F1_def)
from MB[OF _ ‹F2 ⊆ -Y› ‹finite F2›] have ‹norm t2 ≤ 1›
by (auto simp: t2_def F2_def)
have [simp]: ‹F ⊆ F1 × F2›
by (force simp: F1_def F2_def image_def)
have ‹(∑(x,y)∈F. norm (cinner (a x) (b y))) ≤ (∑(x,y)∈F1×F2. norm (cinner (a x) (b y)))›
by (intro sum_mono2) auto
also have "... = (∑x∈F1 × F2. norm (a (fst x) ∙⇩C b (snd x)))"
by (auto simp: case_prod_beta)
also have "... = norm (∑x∈F1 × F2. a (fst x) ∙⇩C b (snd x))"
proof -
have "(∑x∈F1 × F2. ¦a (fst x) ∙⇩C b (snd x)¦) = ¦∑x∈F1 × F2. a (fst x) ∙⇩C b (snd x)¦"
by (smt (verit, best) pos sum.cong sum_nonneg ComplD SigmaE ‹F1 ⊆ - X› ‹F2 ⊆ - Y› abs_pos prod.sel subset_iff)
then show ?thesis
by (smt (verit) abs_complex_def norm_ge_zero norm_of_real o_def of_real_sum sum.cong sum_norm_le)
qed
also from pos have ‹… = norm (∑(x,y)∈F1×F2. cinner (a x) (b y))›
by (auto simp: case_prod_beta)
also have ‹… = norm (cinner (sum a F1) (sum b F2))›
by (simp add: sum.cartesian_product sum_cinner)
also have ‹… = norm (cinner (infsum a (-X) + t1) (infsum b (-Y) + t2))›
by (simp add: t1_def t2_def)
also have ‹… ≤ norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) * norm t2 + norm t1 * norm (infsum b (-Y)) + norm t1 * norm t2›
apply (simp add: cinner_add_right cinner_add_left)
by (smt (verit, del_insts) complex_inner_class.Cauchy_Schwarz_ineq2 norm_triangle_ineq)
also from ‹norm t1 ≤ 1› ‹norm t2 ≤ 1›
have ‹… ≤ norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) + norm (infsum b (-Y)) + 1›
by (auto intro!: add_mono mult_left_le mult_left_le_one_le mult_le_one)
finally show ?thesis
by -
qed
then have ‹(λ(x, y). cinner (a x) (b y)) abs_summable_on (-X)×(-Y)›
apply (rule_tac nonneg_bdd_above_summable_on)
by (auto intro!: bdd_aboveI2 simp: case_prod_unfold)
then have 1: ‹(λ(x, y). cinner (a x) (b y)) summable_on (-X)×(-Y)›
using abs_summable_summable by blast
from bsum
have ‹(λy. b y) summable_on (-Y)›
by (simp add: Compl_eq_Diff_UNIV assms(4) summable_on_cofin_subset)
then have ‹(λy. cinner (a x) (b y)) summable_on (-Y)› for x
using summable_on_cinner_left by blast
with ‹finite X› have 2: ‹(λ(x, y). cinner (a x) (b y)) summable_on X×(-Y)›
by (force intro: summable_on_product_finite_left)
from asum
have ‹(λx. a x) summable_on (-X)›
by (simp add: Compl_eq_Diff_UNIV assms(3) summable_on_cofin_subset)
then have ‹(λx. cinner (a x) (b y)) summable_on (-X)› for y
using summable_on_cinner_right by blast
with ‹finite Y› have 3: ‹(λ(x, y). cinner (a x) (b y)) summable_on (-X)×Y›
by (force intro: summable_on_product_finite_right)
have 4: ‹(λ(x, y). cinner (a x) (b y)) summable_on X×Y›
by (simp add: ‹finite X› ‹finite Y›)
have §: "UNIV = ((-X) × -Y) ∪ (X × -Y) ∪ ((-X) × Y) ∪ (X × Y)"
by auto
show ?thesis
using 1 2 3 4 by (force simp: § intro!: summable_on_Un_disjoint)
qed
text ‹A variant of @{thm [source] Series.Cauchy_product_sums} with \<^term>‹(*)› replaced by \<^term>‹cinner›.
Differently from @{thm [source] Series.Cauchy_product_sums}, we do not require absolute summability
of \<^term>‹a› and \<^term>‹b› individually but only unconditional summability of \<^term>‹a›, \<^term>‹b›, and their product.
While on, e.g., reals, unconditional summability is equivalent to absolute summability, in
general unconditional summability is a weaker requirement.
Logically belong in \<^theory>‹Complex_Bounded_Operators.Complex_Inner_Product›
but the proof uses facts from this theory.›
lemma
fixes a b :: "nat ⇒ 'a::complex_inner"
assumes asum: ‹a summable_on UNIV›
assumes bsum: ‹b summable_on UNIV›
assumes absum: ‹(λ(x, y). cinner (a x) (b y)) summable_on UNIV›
shows Cauchy_cinner_product_infsum: ‹(∑⇩∞k. ∑i≤k. cinner (a i) (b (k - i))) = cinner (∑⇩∞k. a k) (∑⇩∞k. b k)›
and Cauchy_cinner_product_infsum_exists: ‹(λk. ∑i≤k. cinner (a i) (b (k - i))) summable_on UNIV›
proof -
have img: ‹(λ(k::nat, i). (i, k - i)) ` {(k, i). i ≤ k} = UNIV›
apply (auto simp: image_def)
by (metis add.commute add_diff_cancel_right' diff_le_self)
have inj: ‹inj_on (λ(k::nat, i). (i, k - i)) {(k, i). i ≤ k}›
by (smt (verit, del_insts) Pair_inject case_prodE case_prod_conv eq_diff_iff inj_onI mem_Collect_eq)
have sigma: ‹(SIGMA k:UNIV. {i. i ≤ k}) = {(k, i). i ≤ k}›
by auto
from absum
have §: ‹(λ(x, y). cinner (a y) (b (x - y))) summable_on {(k, i). i ≤ k}›
by (rule Cauchy_cinner_product_summable'[THEN iffD1])
then have ‹(λk. ∑⇩∞i|i≤k. cinner (a i) (b (k-i))) summable_on UNIV›
by (metis (mono_tags, lifting) sigma summable_on_Sigma_banach summable_on_cong)
then show ‹(λk. ∑i≤k. cinner (a i) (b (k - i))) summable_on UNIV›
by (metis (mono_tags, lifting) atMost_def finite_Collect_le_nat infsum_finite summable_on_cong)
have ‹cinner (∑⇩∞k. a k) (∑⇩∞k. b k) = (∑⇩∞k. ∑⇩∞l. cinner (a k) (b l))›
by (smt (verit, best) asum bsum infsum_cinner_left infsum_cinner_right infsum_cong)
also have ‹… = (∑⇩∞(k,l). cinner (a k) (b l))›
by (smt (verit) UNIV_Times_UNIV infsum_Sigma'_banach infsum_cong local.absum)
also have ‹… = (∑⇩∞(k, l)∈(λ(k, i). (i, k - i)) ` {(k, i). i ≤ k}. cinner (a k) (b l))›
by (simp only: img)
also have ‹… = infsum ((λ(k, l). a k ∙⇩C b l) ∘ (λ(k, i). (i, k - i))) {(k, i). i ≤ k}›
using inj by (rule infsum_reindex)
also have ‹… = (∑⇩∞(k,i)|i≤k. a i ∙⇩C b (k-i))›
by (simp add: o_def case_prod_unfold)
also have ‹… = (∑⇩∞k. ∑⇩∞i|i≤k. a i ∙⇩C b (k-i))›
by (metis (no_types) § infsum_Sigma'_banach sigma)
also have ‹… = (∑⇩∞k. ∑i≤k. a i ∙⇩C b (k-i))›
by (simp add: atMost_def)
finally show ‹(∑⇩∞k. ∑i≤k. a i ∙⇩C b (k - i)) = (∑⇩∞k. a k) ∙⇩C (∑⇩∞k. b k)›
by simp
qed
lemma CBlinfun_plus:
assumes [simp]: ‹bounded_clinear f› ‹bounded_clinear g›
shows ‹CBlinfun (f + g) = CBlinfun f + CBlinfun g›
by (auto intro!: cblinfun_eqI simp: plus_fun_def bounded_clinear_add CBlinfun_inverse cblinfun.add_left)
lemma CBlinfun_scaleC:
assumes ‹bounded_clinear f›
shows ‹CBlinfun (λy. c *⇩C f y) = c *⇩C CBlinfun f›
by (simp add: assms eq_onp_same_args scaleC_cblinfun.abs_eq)
lemma cinner_sup_norm_cblinfun:
fixes A :: ‹'a::{complex_normed_vector,not_singleton} ⇒⇩C⇩L 'b::complex_inner›
shows ‹norm A = (SUP (ψ,φ). cmod (cinner ψ (A *⇩V φ)) / (norm ψ * norm φ))›
apply transfer
apply (rule cinner_sup_onorm)
by (simp add: bounded_clinear.bounded_linear)
lemma norm_cblinfun_Sup: ‹norm A = (SUP ψ. norm (A *⇩V ψ) / norm ψ)›
by (simp add: norm_cblinfun.rep_eq onorm_def)
lemma cblinfun_eq_on:
fixes A B :: "'a::cbanach ⇒⇩C⇩L'b::complex_normed_vector"
assumes "⋀x. x ∈ G ⟹ A *⇩V x = B *⇩V x" and ‹t ∈ closure (cspan G)›
shows "A *⇩V t = B *⇩V t"
using assms
apply transfer
using bounded_clinear_eq_on_closure by blast
lemma cblinfun_eq_gen_eqI:
fixes A B :: "'a::cbanach ⇒⇩C⇩L'b::complex_normed_vector"
assumes "⋀x. x ∈ G ⟹ A *⇩V x = B *⇩V x" and ‹ccspan G = ⊤›
shows "A = B"
by (metis assms cblinfun_eqI cblinfun_eq_on ccspan.rep_eq iso_tuple_UNIV_I top_ccsubspace.rep_eq)
declare cnj_bounded_antilinear[bounded_antilinear]
lemma Cblinfun_comp_bounded_cbilinear: ‹bounded_clinear (CBlinfun o p)› if ‹bounded_cbilinear p›
by (metis bounded_cbilinear.bounded_clinear_prod_right bounded_cbilinear.prod_right_def comp_id map_fun_def that)
lemma Cblinfun_comp_bounded_sesquilinear: ‹bounded_antilinear (CBlinfun o p)› if ‹bounded_sesquilinear p›
by (metis (mono_tags, opaque_lifting) bounded_clinear_CBlinfun_apply bounded_sesquilinear.bounded_clinear_right comp_apply that transfer_bounded_sesquilinear_bounded_antilinearI)
subsection ‹Relationship to real bounded operators (\<^typ>‹_ ⇒⇩L _›)›
instantiation blinfun :: (real_normed_vector, complex_normed_vector) "complex_normed_vector"
begin
lift_definition scaleC_blinfun :: ‹complex ⇒
('a::real_normed_vector, 'b::complex_normed_vector) blinfun ⇒
('a, 'b) blinfun›
is ‹λ c::complex. λ f::'a⇒'b. (λ x. c *⇩C (f x) )›
proof
fix c::complex and f :: ‹'a⇒'b› and b1::'a and b2::'a
assume ‹bounded_linear f›
show ‹c *⇩C f (b1 + b2) = c *⇩C f b1 + c *⇩C f b2›
by (simp add: ‹bounded_linear f› linear_simps scaleC_add_right)
fix c::complex and f :: ‹'a⇒'b› and b::'a and r::real
assume ‹bounded_linear f›
show ‹c *⇩C f (r *⇩R b) = r *⇩R (c *⇩C f b)›
by (simp add: ‹bounded_linear f› linear_simps(5) scaleR_scaleC)
fix c::complex and f :: ‹'a⇒'b›
assume ‹bounded_linear f›
have ‹∃ K. ∀ x. norm (f x) ≤ norm x * K›
using ‹bounded_linear f›
by (simp add: bounded_linear.bounded)
then obtain K where ‹∀ x. norm (f x) ≤ norm x * K›
by blast
have ‹cmod c ≥ 0›
by simp
hence ‹∀ x. (cmod c) * norm (f x) ≤ (cmod c) * norm x * K›
using ‹∀ x. norm (f x) ≤ norm x * K›
by (metis ordered_comm_semiring_class.comm_mult_left_mono vector_space_over_itself.scale_scale)
moreover have ‹norm (c *⇩C f x) = (cmod c) * norm (f x)›
for x
by simp
ultimately show ‹∃K. ∀x. norm (c *⇩C f x) ≤ norm x * K›
by (metis ab_semigroup_mult_class.mult_ac(1) mult.commute)
qed
instance
proof
have "r *⇩R x = complex_of_real r *⇩C x"
for x :: "('a, 'b) blinfun" and r
by transfer (simp add: scaleR_scaleC)
thus "((*⇩R) r::'a ⇒⇩L 'b ⇒ _) = (*⇩C) (complex_of_real r)" for r
by auto
show "a *⇩C (x + y) = a *⇩C x + a *⇩C y"
for a :: complex and x y :: "'a ⇒⇩L 'b"
by transfer (simp add: scaleC_add_right)
show "(a + b) *⇩C x = a *⇩C x + b *⇩C x"
for a b :: complex and x :: "'a ⇒⇩L 'b"
by transfer (simp add: scaleC_add_left)
show "a *⇩C b *⇩C x = (a * b) *⇩C x"
for a b :: complex and x :: "'a ⇒⇩L 'b"
by transfer simp
have ‹1 *⇩C f x = f x›
for f :: ‹'a⇒'b› and x
by auto
thus "1 *⇩C x = x"
for x :: "'a ⇒⇩L 'b"
by (simp add: scaleC_blinfun.rep_eq blinfun_eqI)
have ‹onorm (λx. a *⇩C f x) = cmod a * onorm f›
if ‹bounded_linear f›
for f :: ‹'a ⇒ 'b› and a :: complex
proof-
have ‹cmod a ≥ 0›
by simp
have ‹∃ K::real. ∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
using ‹bounded_linear f› le_onorm by fastforce
then obtain K::real where ‹∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
by blast
hence ‹∀ x. (cmod a) *(¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ (cmod a) * K›
using ‹cmod a ≥ 0›
by (metis abs_ereal.simps(1) abs_ereal_pos abs_pos ereal_mult_left_mono times_ereal.simps(1))
hence ‹∀ x. (¦ ereal ((cmod a) * (norm (f x)) / (norm x)) ¦) ≤ (cmod a) * K›
by simp
hence ‹bdd_above {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}›
by simp
moreover have ‹{ereal (cmod a * (norm (f x)) / (norm x)) | x. True} ≠ {}›
by auto
ultimately have p1: ‹(SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦) ≤ cmod a * K›
using ‹∀ x. ¦ ereal (cmod a * (norm (f x)) / (norm x)) ¦ ≤ cmod a * K›
Sup_least mem_Collect_eq
by (simp add: SUP_le_iff)
have p2: ‹⋀i. i ∈ UNIV ⟹ 0 ≤ ereal (cmod a * norm (f i) / norm i)›
by simp
hence ‹¦SUP x. ereal (cmod a * (norm (f x)) / (norm x))¦
≤ (SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦)›
using ‹bdd_above {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}›
‹{ereal (cmod a * (norm (f x)) / (norm x)) | x. True} ≠ {}›
by (metis (mono_tags, lifting) SUP_upper2 Sup.SUP_cong UNIV_I
p2 abs_ereal_ge0 ereal_le_real)
hence ‹¦SUP x. ereal (cmod a * (norm (f x)) / (norm x))¦ ≤ cmod a * K›
using ‹(SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦) ≤ cmod a * K›
by simp
hence ‹¦ ( SUP i∈UNIV::'a set. ereal ((λ x. (cmod a) * (norm (f x)) / norm x) i)) ¦ ≠ ∞›
by auto
hence w2: ‹( SUP i∈UNIV::'a set. ereal ((λ x. cmod a * (norm (f x)) / norm x) i))
= ereal ( Sup ((λ x. cmod a * (norm (f x)) / norm x) ` (UNIV::'a set) ))›
by (simp add: ereal_SUP)
have ‹(UNIV::('a set)) ≠ {}›
by simp
moreover have ‹⋀ i. i ∈ (UNIV::('a set)) ⟹ (λ x. (norm (f x)) / norm x :: ereal) i ≥ 0›
by simp
moreover have ‹cmod a ≥ 0›
by simp
ultimately have ‹(SUP i∈(UNIV::('a set)). ((cmod a)::ereal) * (λ x. (norm (f x)) / norm x :: ereal) i )
= ((cmod a)::ereal) * ( SUP i∈(UNIV::('a set)). (λ x. (norm (f x)) / norm x :: ereal) i )›
by (simp add: Sup_ereal_mult_left')
hence ‹(SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) )
= ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) )›
by simp
hence z1: ‹real_of_ereal ( (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) ) )
= real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )›
by simp
have z2: ‹real_of_ereal (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) )
= (SUP x. cmod a * (norm (f x) / norm x))›
using w2
by auto
have ‹real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
= (cmod a) * real_of_ereal ( SUP x. ( (norm (f x)) / norm x :: ereal) )›
by simp
moreover have ‹real_of_ereal ( SUP x. ( (norm (f x)) / norm x :: ereal) )
= ( SUP x. ((norm (f x)) / norm x) )›
proof-
have ‹¦ ( SUP i∈UNIV::'a set. ereal ((λ x. (norm (f x)) / norm x) i)) ¦ ≠ ∞›
proof-
have ‹∃ K::real. ∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
using ‹bounded_linear f› le_onorm by fastforce
then obtain K::real where ‹∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
by blast
hence ‹bdd_above {ereal ((norm (f x)) / (norm x)) | x. True}›
by simp
moreover have ‹{ereal ((norm (f x)) / (norm x)) | x. True} ≠ {}›
by auto
ultimately have ‹(SUP x. ¦ereal ((norm (f x)) / (norm x))¦) ≤ K›
using ‹∀ x. ¦ ereal ((norm (f x)) / (norm x)) ¦ ≤ K›
Sup_least mem_Collect_eq
by (simp add: SUP_le_iff)
hence ‹¦SUP x. ereal ((norm (f x)) / (norm x))¦
≤ (SUP x. ¦ereal ((norm (f x)) / (norm x))¦)›
using ‹bdd_above {ereal ((norm (f x)) / (norm x)) | x. True}›
‹{ereal ((norm (f x)) / (norm x)) | x. True} ≠ {}›
by (metis (mono_tags, lifting) SUP_upper2 Sup.SUP_cong UNIV_I ‹⋀i. i ∈ UNIV ⟹ 0 ≤ ereal (norm (f i) / norm i)› abs_ereal_ge0 ereal_le_real)
hence ‹¦SUP x. ereal ((norm (f x)) / (norm x))¦ ≤ K›
using ‹(SUP x. ¦ereal ((norm (f x)) / (norm x))¦) ≤ K›
by simp
thus ?thesis
by auto
qed
hence ‹ ( SUP i∈UNIV::'a set. ereal ((λ x. (norm (f x)) / norm x) i))
= ereal ( Sup ((λ x. (norm (f x)) / norm x) ` (UNIV::'a set) ))›
by (simp add: ereal_SUP)
thus ?thesis
by simp
qed
have z3: ‹real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
= cmod a * (SUP x. norm (f x) / norm x)›
by (simp add: ‹real_of_ereal (SUP x. ereal (norm (f x) / norm x)) = (SUP x. norm (f x) / norm x)›)
hence w1: ‹(SUP x. cmod a * (norm (f x) / norm x)) =
cmod a * (SUP x. norm (f x) / norm x)›
using z1 z2 by linarith
have v1: ‹onorm (λx. a *⇩C f x) = (SUP x. norm (a *⇩C f x) / norm x)›
by (simp add: onorm_def)
have v2: ‹(SUP x. norm (a *⇩C f x) / norm x) = (SUP x. ((cmod a) * norm (f x)) / norm x)›
by simp
have v3: ‹(SUP x. ((cmod a) * norm (f x)) / norm x) = (SUP x. (cmod a) * ((norm (f x)) / norm x))›
by simp
have v4: ‹(SUP x. (cmod a) * ((norm (f x)) / norm x)) = (cmod a) * (SUP x. ((norm (f x)) / norm x))›
using w1
by blast
show ‹onorm (λx. a *⇩C f x) = cmod a * onorm f›
using v1 v2 v3 v4
by (metis (mono_tags, lifting) onorm_def)
qed
thus ‹norm (a *⇩C x) = cmod a * norm x›
for a::complex and x::‹('a, 'b) blinfun›
by transfer blast
qed
end
lemma clinear_blinfun_compose_left: ‹clinear (λx. blinfun_compose x y)›
by (auto intro!: clinearI simp: blinfun_eqI scaleC_blinfun.rep_eq bounded_bilinear.add_left
bounded_bilinear_blinfun_compose)
instance blinfun :: (real_normed_vector, cbanach) cbanach..
lemma blinfun_compose_assoc: "(A o⇩L B) o⇩L C = A o⇩L (B o⇩L C)"
by (simp add: blinfun_eqI)
lift_definition blinfun_of_cblinfun::‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector
⇒ 'a ⇒⇩L 'b› is "id"
by transfer (simp add: bounded_clinear.bounded_linear)
lift_definition blinfun_cblinfun_eq ::
‹'a ⇒⇩L 'b ⇒ 'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector ⇒ bool› is "(=)" .
lemma blinfun_cblinfun_eq_bi_unique[transfer_rule]: ‹bi_unique blinfun_cblinfun_eq›
unfolding bi_unique_def by transfer auto
lemma blinfun_cblinfun_eq_right_total[transfer_rule]: ‹right_total blinfun_cblinfun_eq›
unfolding right_total_def by transfer (simp add: bounded_clinear.bounded_linear)
named_theorems cblinfun_blinfun_transfer
lemma cblinfun_blinfun_transfer_0[cblinfun_blinfun_transfer]:
"blinfun_cblinfun_eq (0::(_,_) blinfun) (0::(_,_) cblinfun)"
by transfer simp
lemma cblinfun_blinfun_transfer_plus[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (+) (+)"
unfolding rel_fun_def by transfer auto
lemma cblinfun_blinfun_transfer_minus[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (-) (-)"
unfolding rel_fun_def by transfer auto
lemma cblinfun_blinfun_transfer_uminus[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (uminus) (uminus)"
unfolding rel_fun_def by transfer auto
definition "real_complex_eq r c ⟷ complex_of_real r = c"
lemma bi_unique_real_complex_eq[transfer_rule]: ‹bi_unique real_complex_eq›
unfolding real_complex_eq_def bi_unique_def by auto
lemma left_total_real_complex_eq[transfer_rule]: ‹left_total real_complex_eq›
unfolding real_complex_eq_def left_total_def by auto
lemma cblinfun_blinfun_transfer_scaleC[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(real_complex_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (scaleR) (scaleC)"
unfolding rel_fun_def by transfer (simp add: real_complex_eq_def scaleR_scaleC)
lemma cblinfun_blinfun_transfer_CBlinfun[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(eq_onp bounded_clinear ===> blinfun_cblinfun_eq) Blinfun CBlinfun"
unfolding rel_fun_def blinfun_cblinfun_eq.rep_eq eq_onp_def
by (auto simp: CBlinfun_inverse Blinfun_inverse bounded_clinear.bounded_linear)
lemma cblinfun_blinfun_transfer_norm[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> (=)) norm norm"
unfolding rel_fun_def by transfer auto
lemma cblinfun_blinfun_transfer_dist[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> (=)) dist dist"
unfolding rel_fun_def dist_norm by transfer auto
lemma cblinfun_blinfun_transfer_sgn[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) sgn sgn"
unfolding rel_fun_def sgn_blinfun_def sgn_cblinfun_def by transfer (auto simp: scaleR_scaleC)
lemma cblinfun_blinfun_transfer_Cauchy[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(((=) ===> blinfun_cblinfun_eq) ===> (=)) Cauchy Cauchy"
proof -
note cblinfun_blinfun_transfer[transfer_rule]
show ?thesis
unfolding Cauchy_def
by transfer_prover
qed
lemma cblinfun_blinfun_transfer_tendsto[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) tendsto tendsto"
proof -
note cblinfun_blinfun_transfer[transfer_rule]
show ?thesis
unfolding tendsto_iff
by transfer_prover
qed
lemma cblinfun_blinfun_transfer_compose[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (o⇩L) (o⇩C⇩L)"
unfolding rel_fun_def by transfer auto
lemma cblinfun_blinfun_transfer_apply[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> (=) ===> (=)) blinfun_apply cblinfun_apply"
unfolding rel_fun_def by transfer auto
lemma blinfun_of_cblinfun_inj:
‹blinfun_of_cblinfun f = blinfun_of_cblinfun g ⟹ f = g›
by (metis cblinfun_apply_inject blinfun_of_cblinfun.rep_eq)
lemma blinfun_of_cblinfun_inv:
assumes "⋀c. ⋀x. f *⇩v (c *⇩C x) = c *⇩C (f *⇩v x)"
shows "∃g. blinfun_of_cblinfun g = f"
using assms
proof transfer
show "∃g∈Collect bounded_clinear. id g = f"
if "bounded_linear f"
and "⋀c x. f (c *⇩C x) = c *⇩C f x"
for f :: "'a ⇒ 'b"
using that bounded_linear_bounded_clinear by auto
qed
lemma blinfun_of_cblinfun_zero:
‹blinfun_of_cblinfun 0 = 0›
by transfer simp
lemma blinfun_of_cblinfun_uminus:
‹blinfun_of_cblinfun (- f) = - (blinfun_of_cblinfun f)›
by transfer auto
lemma blinfun_of_cblinfun_minus:
‹blinfun_of_cblinfun (f - g) = blinfun_of_cblinfun f - blinfun_of_cblinfun g›
by transfer auto
lemma blinfun_of_cblinfun_scaleC:
‹blinfun_of_cblinfun (c *⇩C f) = c *⇩C (blinfun_of_cblinfun f)›
by transfer auto
lemma blinfun_of_cblinfun_scaleR:
‹blinfun_of_cblinfun (c *⇩R f) = c *⇩R (blinfun_of_cblinfun f)›
by transfer auto
lemma blinfun_of_cblinfun_norm:
fixes f::‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
shows ‹norm f = norm (blinfun_of_cblinfun f)›
by transfer auto
lemma blinfun_of_cblinfun_cblinfun_compose:
fixes f::‹'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector›
and g::‹'a::complex_normed_vector ⇒⇩C⇩L 'b›
shows ‹blinfun_of_cblinfun (f o⇩C⇩L g) = (blinfun_of_cblinfun f) o⇩L (blinfun_of_cblinfun g)›
by transfer auto
subsection ‹Composition›
lemma cblinfun_compose_assoc:
shows "(A o⇩C⇩L B) o⇩C⇩L C = A o⇩C⇩L (B o⇩C⇩L C)"
by (metis (no_types, lifting) cblinfun_apply_inject fun.map_comp cblinfun_compose.rep_eq)
lemma cblinfun_compose_zero_right[simp]: "U o⇩C⇩L 0 = 0"
using bounded_cbilinear.zero_right bounded_cbilinear_cblinfun_compose by blast
lemma cblinfun_compose_zero_left[simp]: "0 o⇩C⇩L U = 0"
using bounded_cbilinear.zero_left bounded_cbilinear_cblinfun_compose by blast
lemma cblinfun_compose_scaleC_left[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹(a *⇩C A) o⇩C⇩L B = a *⇩C (A o⇩C⇩L B)›
by (simp add: bounded_cbilinear.scaleC_left bounded_cbilinear_cblinfun_compose)
lemma cblinfun_compose_scaleR_left[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹(a *⇩R A) o⇩C⇩L B = a *⇩R (A o⇩C⇩L B)›
by (simp add: scaleR_scaleC)
lemma cblinfun_compose_scaleC_right[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹A o⇩C⇩L (a *⇩C B) = a *⇩C (A o⇩C⇩L B)›
by transfer (auto intro!: ext bounded_clinear.clinear complex_vector.linear_scale)
lemma cblinfun_compose_scaleR_right[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹A o⇩C⇩L (a *⇩R B) = a *⇩R (A o⇩C⇩L B)›
by (simp add: scaleR_scaleC)
lemma cblinfun_compose_id_right[simp]:
shows "U o⇩C⇩L id_cblinfun = U"
by transfer auto
lemma cblinfun_compose_id_left[simp]:
shows "id_cblinfun o⇩C⇩L U = U"
by transfer auto
lemma cblinfun_compose_add_left: ‹(a + b) o⇩C⇩L c = (a o⇩C⇩L c) + (b o⇩C⇩L c)›
by (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose)
lemma cblinfun_compose_add_right: ‹a o⇩C⇩L (b + c) = (a o⇩C⇩L b) + (a o⇩C⇩L c)›
by (simp add: bounded_cbilinear.add_right bounded_cbilinear_cblinfun_compose)
lemma cbilinear_cblinfun_compose[simp]: "cbilinear cblinfun_compose"
by (auto intro!: clinearI simp add: cbilinear_def bounded_cbilinear.add_left bounded_cbilinear.add_right bounded_cbilinear_cblinfun_compose)
lemma cblinfun_compose_sum_left: ‹(∑i∈S. g i) o⇩C⇩L x = (∑i∈S. g i o⇩C⇩L x)›
by (induction S rule:infinite_finite_induct) (auto simp: cblinfun_compose_add_left)
lemma cblinfun_compose_sum_right: ‹x o⇩C⇩L (∑i∈S. g i) = (∑i∈S. x o⇩C⇩L g i)›
by (induction S rule:infinite_finite_induct) (auto simp: cblinfun_compose_add_right)
lemma cblinfun_compose_minus_right: ‹a o⇩C⇩L (b - c) = (a o⇩C⇩L b) - (a o⇩C⇩L c)›
by (simp add: bounded_cbilinear.diff_right bounded_cbilinear_cblinfun_compose)
lemma cblinfun_compose_minus_left: ‹(a - b) o⇩C⇩L c = (a o⇩C⇩L c) - (b o⇩C⇩L c)›
by (simp add: bounded_cbilinear.diff_left bounded_cbilinear_cblinfun_compose)
lemma simp_a_oCL_b: ‹a o⇩C⇩L b = c ⟹ a o⇩C⇩L (b o⇩C⇩L d) = c o⇩C⇩L d›
by (auto simp: cblinfun_compose_assoc)
lemma simp_a_oCL_b': ‹a o⇩C⇩L b = c ⟹ a *⇩V (b *⇩V d) = c *⇩V d›
by auto
lemma cblinfun_compose_uminus_left: ‹(- a) o⇩C⇩L b = - (a o⇩C⇩L b)›
by (simp add: bounded_cbilinear.minus_left bounded_cbilinear_cblinfun_compose)
lemma cblinfun_compose_uminus_right: ‹a o⇩C⇩L (- b) = - (a o⇩C⇩L b)›
by (simp add: bounded_cbilinear.minus_right bounded_cbilinear_cblinfun_compose)
lemma bounded_clinear_cblinfun_compose_left: ‹bounded_clinear (λx. x o⇩C⇩L y)›
by (simp add: bounded_cbilinear.bounded_clinear_left bounded_cbilinear_cblinfun_compose)
lemma bounded_clinear_cblinfun_compose_right: ‹bounded_clinear (λy. x o⇩C⇩L y)›
by (simp add: bounded_cbilinear.bounded_clinear_right bounded_cbilinear_cblinfun_compose)
lemma clinear_cblinfun_compose_left: ‹clinear (λx. x o⇩C⇩L y)›
by (simp add: bounded_cbilinear.bounded_clinear_left bounded_cbilinear_cblinfun_compose bounded_clinear.clinear)
lemma clinear_cblinfun_compose_right: ‹clinear (λy. x o⇩C⇩L y)›
by (simp add: bounded_clinear.clinear bounded_clinear_cblinfun_compose_right)
lemma additive_cblinfun_compose_left[simp]: ‹Modules.additive (λx. x o⇩C⇩L a)›
by (simp add: Modules.additive_def cblinfun_compose_add_left)
lemma additive_cblinfun_compose_right[simp]: ‹Modules.additive (λx. a o⇩C⇩L x)›
by (simp add: Modules.additive_def cblinfun_compose_add_right)
lemma isCont_cblinfun_compose_left: ‹isCont (λx. x o⇩C⇩L a) y›
apply (rule clinear_continuous_at)
by (rule bounded_clinear_cblinfun_compose_left)
lemma isCont_cblinfun_compose_right: ‹isCont (λx. a o⇩C⇩L x) y›
apply (rule clinear_continuous_at)
by (rule bounded_clinear_cblinfun_compose_right)
lemma cspan_compose_closed:
assumes ‹⋀a b. a ∈ A ⟹ b ∈ A ⟹ a o⇩C⇩L b ∈ A›
assumes ‹a ∈ cspan A› and ‹b ∈ cspan A›
shows ‹a o⇩C⇩L b ∈ cspan A›
proof -
from ‹a ∈ cspan A›
obtain F f where ‹finite F› and ‹F ⊆ A› and a_def: ‹a = (∑x∈F. f x *⇩C x)›
by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
from ‹b ∈ cspan A›
obtain G g where ‹finite G› and ‹G ⊆ A› and b_def: ‹b = (∑x∈G. g x *⇩C x)›
by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
have ‹a o⇩C⇩L b = (∑(x,y)∈F×G. (f x *⇩C x) o⇩C⇩L (g y *⇩C y))›
apply (simp add: a_def b_def cblinfun_compose_sum_left)
by (auto intro!: sum.cong simp add: cblinfun_compose_sum_right scaleC_sum_right sum.cartesian_product case_prod_beta)
also have ‹… = (∑(x,y)∈F×G. (f x * g y) *⇩C (x o⇩C⇩L y))›
by (metis (no_types, opaque_lifting) cblinfun_compose_scaleC_left cblinfun_compose_scaleC_right scaleC_scaleC)
also have ‹… ∈ cspan A›
using assms ‹G ⊆ A› ‹F ⊆ A›
apply (auto intro!: complex_vector.span_sum complex_vector.span_scale
simp: complex_vector.span_clauses)
using complex_vector.span_clauses(1) by blast
finally show ?thesis
by -
qed
subsection ‹Adjoint›
lift_definition
adj :: "'a::chilbert_space ⇒⇩C⇩L 'b::complex_inner ⇒ 'b ⇒⇩C⇩L 'a" ("_*" [99] 100)
is cadjoint by (fact cadjoint_bounded_clinear)
definition selfadjoint :: ‹('a::chilbert_space ⇒⇩C⇩L 'a) ⇒ bool› where
‹selfadjoint a ⟷ a* = a›
lemma id_cblinfun_adjoint[simp]: "id_cblinfun* = id_cblinfun"
by (metis adj.rep_eq apply_id_cblinfun cadjoint_id cblinfun_apply_inject)
lemma double_adj[simp]: "(A*)* = A"
apply transfer using double_cadjoint by blast
lemma adj_cblinfun_compose[simp]:
fixes B::‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
and A::‹'b ⇒⇩C⇩L 'c::complex_inner›
shows "(A o⇩C⇩L B)* = (B*) o⇩C⇩L (A*)"
proof transfer
fix A :: ‹'b ⇒ 'c› and B :: ‹'a ⇒ 'b›
assume ‹bounded_clinear A› and ‹bounded_clinear B›
hence ‹bounded_clinear (A ∘ B)›
by (simp add: comp_bounded_clinear)
have ‹((A ∘ B) u ∙⇩C v) = (u ∙⇩C (B⇧† ∘ A⇧†) v)›
for u v
by (metis (no_types, lifting) cadjoint_univ_prop ‹bounded_clinear A› ‹bounded_clinear B› cinner_commute' comp_def)
thus ‹(A ∘ B)⇧† = B⇧† ∘ A⇧†›
using ‹bounded_clinear (A ∘ B)›
by (metis cadjoint_eqI cinner_commute')
qed
lemma scaleC_adj[simp]: "(a *⇩C A)* = (cnj a) *⇩C (A*)"
by transfer (simp add: bounded_clinear.bounded_linear bounded_clinear_def complex_vector.linear_scale scaleC_cadjoint)
lemma scaleR_adj[simp]: "(a *⇩R A)* = a *⇩R (A*)"
by (simp add: scaleR_scaleC)
lemma adj_plus: ‹(A + B)* = (A*) + (B*)›
proof transfer
fix A B::‹'b ⇒ 'a›
assume a1: ‹bounded_clinear A› and a2: ‹bounded_clinear B›
define F where ‹F = (λx. (A⇧†) x + (B⇧†) x)›
define G where ‹G = (λx. A x + B x)›
have ‹bounded_clinear G›
unfolding G_def
by (simp add: a1 a2 bounded_clinear_add)
moreover have ‹(F u ∙⇩C v) = (u ∙⇩C G v)› for u v
unfolding F_def G_def
using cadjoint_univ_prop a1 a2 cinner_add_left
by (simp add: cadjoint_univ_prop cinner_add_left cinner_add_right)
ultimately have ‹F = G⇧† ›
using cadjoint_eqI by blast
thus ‹(λx. A x + B x)⇧† = (λx. (A⇧†) x + (B⇧†) x)›
unfolding F_def G_def
by auto
qed
lemma cinner_adj_left:
fixes G :: "'b::chilbert_space ⇒⇩C⇩L 'a::complex_inner"
shows ‹(G* *⇩V x) ∙⇩C y = x ∙⇩C (G *⇩V y)›
apply transfer using cadjoint_univ_prop by blast
lemma cinner_adj_right:
fixes G :: "'b::chilbert_space ⇒⇩C⇩L 'a::complex_inner"
shows ‹x ∙⇩C (G* *⇩V y) = (G *⇩V x) ∙⇩C y›
apply transfer using cadjoint_univ_prop' by blast
lemma adj_0[simp]: ‹0* = 0›
by (metis add_cancel_right_left adj_plus)
lemma selfadjoint_0[simp]: ‹selfadjoint 0›
by (simp add: selfadjoint_def)
lemma norm_adj[simp]: ‹norm (A*) = norm A›
for A :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::complex_inner›
proof (cases ‹(∃x y :: 'b. x ≠ y) ∧ (∃x y :: 'c. x ≠ y)›)
case True
then have c1: ‹class.not_singleton TYPE('b)›
by intro_classes simp
from True have c2: ‹class.not_singleton TYPE('c)›
by intro_classes simp
have normA: ‹norm A = (SUP (ψ, φ). cmod (ψ ∙⇩C (A *⇩V φ)) / (norm ψ * norm φ))›
apply (rule cinner_sup_norm_cblinfun[internalize_sort ‹'a::{complex_normed_vector,not_singleton}›])
apply (rule complex_normed_vector_axioms)
by (rule c1)
have normAadj: ‹norm (A*) = (SUP (ψ, φ). cmod (ψ ∙⇩C (A* *⇩V φ)) / (norm ψ * norm φ))›
apply (rule cinner_sup_norm_cblinfun[internalize_sort ‹'a::{complex_normed_vector,not_singleton}›])
apply (rule complex_normed_vector_axioms)
by (rule c2)
have ‹norm (A*) = (SUP (ψ, φ). cmod (φ ∙⇩C (A *⇩V ψ)) / (norm ψ * norm φ))›
unfolding normAadj
apply (subst cinner_adj_right)
apply (subst cinner_commute)
apply (subst complex_mod_cnj)
by rule
also have ‹… = Sup ((λ(ψ, φ). cmod (φ ∙⇩C (A *⇩V ψ)) / (norm ψ * norm φ)) ` prod.swap ` UNIV)›
by auto
also have ‹… = (SUP (φ, ψ). cmod (φ ∙⇩C (A *⇩V ψ)) / (norm ψ * norm φ))›
apply (subst image_image)
by auto
also have ‹… = norm A›
unfolding normA
by (simp add: mult.commute)
finally show ?thesis
by -
next
case False
then consider (b) ‹⋀x::'b. x = 0› | (c) ‹⋀x::'c. x = 0›
by auto
then have ‹A = 0›
apply (cases; transfer)
apply (metis (full_types) bounded_clinear_def complex_vector.linear_0)
by auto
then show ‹norm (A*) = norm A›
by simp
qed
lemma antilinear_adj[simp]: ‹antilinear adj›
by (simp add: adj_plus antilinearI)
lemma bounded_antilinear_adj[bounded_antilinear, simp]: ‹bounded_antilinear adj›
by (auto intro!: antilinearI exI[of _ 1] simp: bounded_antilinear_def bounded_antilinear_axioms_def adj_plus)
lemma adjoint_eqI:
fixes G:: ‹'b::chilbert_space ⇒⇩C⇩L 'a::complex_inner›
and F:: ‹'a ⇒⇩C⇩L 'b›
assumes ‹⋀x y. ((cblinfun_apply F) x ∙⇩C y) = (x ∙⇩C (cblinfun_apply G) y)›
shows ‹F = G*›
using assms apply transfer using cadjoint_eqI by auto
lemma adj_uminus: ‹(-A)* = - (A*)›
by (metis scaleR_adj scaleR_minus1_left scaleR_minus1_left)
lemma cinner_real_hermiteanI:
assumes ‹⋀ψ. ψ ∙⇩C (A *⇩V ψ) ∈ ℝ›
shows ‹A* = A›
proof -
{ fix g h :: 'a
{
fix α :: complex
have ‹cinner h (A h) + cnj α *⇩C cinner g (A h) + α *⇩C cinner h (A g) + (abs α)⇧2 * cinner g (A g)
= cinner (h + α *⇩C g) (A *⇩V (h + α *⇩C g))› (is ‹?sum4 = _›)
apply (auto simp: cinner_add_right cinner_add_left cblinfun.add_right cblinfun.scaleC_right ring_class.ring_distribs)
by (metis cnj_x_x mult.commute)
also have ‹… ∈ ℝ›
using assms by auto
finally have ‹?sum4 = cnj ?sum4›
using Reals_cnj_iff by fastforce
then have ‹cnj α *⇩C cinner g (A h) + α *⇩C cinner h (A g)
= α *⇩C cinner (A h) g + cnj α *⇩C cinner (A g) h›
using Reals_cnj_iff abs_complex_real assms by force
also have ‹… = α *⇩C cinner h (A* *⇩V g) + cnj α *⇩C cinner g (A* *⇩V h)›
by (simp add: cinner_adj_right)
finally have ‹cnj α *⇩C cinner g (A h) + α *⇩C cinner h (A g) = α *⇩C cinner h (A* *⇩V g) + cnj α *⇩C cinner g (A* *⇩V h)›
by -
}
from this[where α2=1] this[where α2=𝗂]
have 1: ‹cinner g (A h) + cinner h (A g) = cinner h (A* *⇩V g) + cinner g (A* *⇩V h)›
and i: ‹- 𝗂 * cinner g (A h) + 𝗂 *⇩C cinner h (A g) = 𝗂 *⇩C cinner h (A* *⇩V g) - 𝗂 *⇩C cinner g (A* *⇩V h)›
by auto
from arg_cong2[OF 1 arg_cong[OF i, where f=‹(*) (-𝗂)›], where f=plus]
have ‹cinner h (A g) = cinner h (A* *⇩V g)›
by (auto simp: ring_class.ring_distribs)
}
then show "A* = A"
apply (rule_tac sym)
by (simp add: adjoint_eqI cinner_adj_right)
qed
lemma norm_AAadj[simp]: ‹norm (A o⇩C⇩L A*) = (norm A)⇧2› for A :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::{complex_inner}›
proof (cases ‹class.not_singleton TYPE('b)›)
case True
then have [simp]: ‹class.not_singleton TYPE('b)›
by -
have 1: ‹(norm A)⇧2 * ε ≤ norm (A o⇩C⇩L A*)› if ‹ε < 1› and ‹ε ≥ 0› for ε
proof -
obtain ψ where ψ: ‹norm ((A*) *⇩V ψ) ≥ norm (A*) * sqrt ε› and [simp]: ‹norm ψ = 1›
apply atomize_elim
apply (rule cblinfun_norm_approx_witness_mult[internalize_sort' 'a])
using ‹ε < 1› by (auto intro: complex_normed_vector_class.complex_normed_vector_axioms)
have ‹complex_of_real ((norm A)⇧2 * ε) = (norm (A*) * sqrt ε)⇧2›
by (simp add: ordered_field_class.sign_simps(23) that(2))
also have ‹… ≤ (norm ((A* *⇩V ψ)))⇧2›
by (meson ψ complex_of_real_mono mult_nonneg_nonneg norm_ge_zero power_mono real_sqrt_ge_zero ‹ε ≥ 0›)
also have ‹… ≤ cinner (A* *⇩V ψ) (A* *⇩V ψ)›
by (auto simp flip: power2_norm_eq_cinner)
also have §: ‹… = cinner ψ ((A o⇩C⇩L A*) *⇩V ψ)›
by (auto simp: cinner_adj_left)
also have ‹… ≤ norm (A o⇩C⇩L A*)›
using ‹norm ψ = 1›
by (smt (verit) Re_complex_of_real § cdot_square_norm cinner_ge_zero cmod_Re complex_inner_class.Cauchy_Schwarz_ineq2 complex_of_real_mono mult_cancel_left1 mult_cancel_right1 norm_cblinfun)
finally show ?thesis
by (auto simp: less_eq_complex_def)
qed
then have 1: ‹(norm A)⇧2 ≤ norm (A o⇩C⇩L A*)›
by (metis field_le_mult_one_interval less_eq_real_def ordered_field_class.sign_simps(5))
have 2: ‹norm (A o⇩C⇩L A*) ≤ (norm A)⇧2›
proof (rule norm_cblinfun_bound)
show ‹0 ≤ (norm A)⇧2› by simp
fix ψ
have ‹norm ((A o⇩C⇩L A*) *⇩V ψ) = norm (A *⇩V A* *⇩V ψ)›
by auto
also have ‹… ≤ norm A * norm (A* *⇩V ψ)›
by (simp add: norm_cblinfun)
also have ‹… ≤ norm A * norm (A*) * norm ψ›
by (metis mult.assoc norm_cblinfun norm_imp_pos_and_ge ordered_comm_semiring_class.comm_mult_left_mono)
also have ‹… = (norm A)⇧2 * norm ψ›
by (simp add: power2_eq_square)
finally show ‹norm ((A o⇩C⇩L A*) *⇩V ψ) ≤ (norm A)⇧2 * norm ψ›
by -
qed
from 1 2 show ?thesis by simp
next
case False
then have [simp]: ‹class.CARD_1 TYPE('b)›
by (rule not_singleton_vs_CARD_1)
have ‹A = 0›
apply (rule cblinfun_to_CARD_1_0[internalize_sort' 'b])
by (auto intro: complex_normed_vector_class.complex_normed_vector_axioms)
then show ?thesis
by auto
qed
lemma sum_adj: ‹(sum a F)* = sum (λi. (a i)*) F›
by (induction rule:infinite_finite_induct) (auto simp add: adj_plus)
lemma has_sum_adj:
assumes ‹(f has_sum x) I›
shows ‹((λx. adj (f x)) has_sum adj x) I›
apply (rule has_sum_comm_additive[where f=adj, unfolded o_def])
apply (simp add: antilinear.axioms(1))
apply (metis (no_types, lifting) LIM_eq adj_plus adj_uminus norm_adj uminus_add_conv_diff)
by (simp add: assms)
lemma adj_minus: ‹(A - B)* = (A*) - (B*)›
by (metis add_implies_diff adj_plus diff_add_cancel)
lemma cinner_hermitian_real: ‹x ∙⇩C (A *⇩V x) ∈ ℝ› if ‹selfadjoint A›
by (metis Reals_cnj_iff cinner_adj_right cinner_commute' that selfadjoint_def)
lemma adj_inject: ‹adj a = adj b ⟷ a = b›
by (metis (no_types, opaque_lifting) adj_minus eq_iff_diff_eq_0 norm_adj norm_eq_zero)
lemma norm_AadjA[simp]: ‹norm (A* o⇩C⇩L A) = (norm A)⇧2› for A :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
by (metis double_adj norm_AAadj norm_adj)
lemma cspan_adj_closed:
assumes ‹⋀a. a ∈ A ⟹ a* ∈ A›
assumes ‹a ∈ cspan A›
shows ‹a* ∈ cspan A›
proof -
from ‹a ∈ cspan A›
obtain F f where ‹finite F› and ‹F ⊆ A› and ‹a = (∑x∈F. f x *⇩C x)›
by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
then have ‹a* = (∑x∈F. cnj (f x) *⇩C x*)›
by (auto simp: sum_adj)
also have ‹… ∈ cspan A›
using assms ‹F ⊆ A›
by (auto intro!: complex_vector.span_sum complex_vector.span_scale simp: complex_vector.span_clauses)
finally show ?thesis
by -
qed
subsection ‹Powers of operators›
lift_definition cblinfun_power :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'a ⇒ nat ⇒ 'a ⇒⇩C⇩L 'a› is
‹λ(a::'a⇒'a) n. a ^^ n›
apply (rename_tac f n, induct_tac n, auto simp: Nat.funpow_code_def)
by (simp add: bounded_clinear_compose)
lemma cblinfun_power_0[simp]: ‹cblinfun_power A 0 = id_cblinfun›
by transfer auto
lemma cblinfun_power_Suc': ‹cblinfun_power A (Suc n) = A o⇩C⇩L cblinfun_power A n›
by transfer auto
lemma cblinfun_power_Suc: ‹cblinfun_power A (Suc n) = cblinfun_power A n o⇩C⇩L A›
apply (induction n)
by (auto simp: cblinfun_power_Suc' simp flip: cblinfun_compose_assoc)
lemma cblinfun_power_compose[simp]: ‹cblinfun_power A n o⇩C⇩L cblinfun_power A m = cblinfun_power A (n+m)›
apply (induction n)
by (auto simp: cblinfun_power_Suc' cblinfun_compose_assoc)
lemma cblinfun_power_scaleC: ‹cblinfun_power (c *⇩C a) n = c^n *⇩C cblinfun_power a n›
apply (induction n)
by (auto simp: cblinfun_power_Suc)
lemma cblinfun_power_scaleR: ‹cblinfun_power (c *⇩R a) n = c^n *⇩R cblinfun_power a n›
apply (induction n)
by (auto simp: cblinfun_power_Suc)
lemma cblinfun_power_uminus: ‹cblinfun_power (-a) n = (-1)^n *⇩R cblinfun_power a n›
apply (subst asm_rl[of ‹-a = (-1) *⇩R a›])
by simp (rule cblinfun_power_scaleR)
lemma cblinfun_power_adj: ‹(cblinfun_power S n)* = cblinfun_power (S*) n›
apply (induction n)
apply simp
apply (subst cblinfun_power_Suc)
apply (subst cblinfun_power_Suc')
by auto
subsection ‹Unitaries / isometries›
definition isometry::‹'a::chilbert_space ⇒⇩C⇩L 'b::complex_inner ⇒ bool› where
‹isometry U ⟷ U* o⇩C⇩L U = id_cblinfun›
definition unitary::‹'a::chilbert_space ⇒⇩C⇩L 'b::complex_inner ⇒ bool› where
‹unitary U ⟷ (U* o⇩C⇩L U = id_cblinfun) ∧ (U o⇩C⇩L U* = id_cblinfun)›
lemma unitaryI: ‹unitary a› if ‹a* o⇩C⇩L a = id_cblinfun› and ‹a o⇩C⇩L a* = id_cblinfun›
unfolding unitary_def using that by simp
lemma unitary_twosided_isometry: "unitary U ⟷ isometry U ∧ isometry (U*)"
unfolding unitary_def isometry_def by simp
lemma isometryD[simp]: "isometry U ⟹ U* o⇩C⇩L U = id_cblinfun"
unfolding isometry_def by simp
lemma unitaryD1: "unitary U ⟹ U* o⇩C⇩L U = id_cblinfun"
unfolding unitary_def by simp
lemma unitaryD2[simp]: "unitary U ⟹ U o⇩C⇩L U* = id_cblinfun"
unfolding unitary_def by simp
lemma unitary_isometry[simp]: "unitary U ⟹ isometry U"
unfolding unitary_def isometry_def by simp
lemma unitary_adj[simp]: "unitary (U*) = unitary U"
unfolding unitary_def by auto
lemma isometry_cblinfun_compose[simp]:
assumes "isometry A" and "isometry B"
shows "isometry (A o⇩C⇩L B)"
proof-
have "B* o⇩C⇩L A* o⇩C⇩L (A o⇩C⇩L B) = id_cblinfun" if "A* o⇩C⇩L A = id_cblinfun" and "B* o⇩C⇩L B = id_cblinfun"
using that
by (smt (verit, del_insts) adjoint_eqI cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply)
thus ?thesis
using assms unfolding isometry_def by simp
qed
lemma unitary_cblinfun_compose[simp]: "unitary (A o⇩C⇩L B)"
if "unitary A" and "unitary B"
using that
by (smt (z3) adj_cblinfun_compose cblinfun_compose_assoc cblinfun_compose_id_right double_adj isometryD isometry_cblinfun_compose unitary_def unitary_isometry)
lemma unitary_surj:
assumes "unitary U"
shows "surj (cblinfun_apply U)"
apply (rule surjI[where f=‹cblinfun_apply (U*)›])
using assms unfolding unitary_def apply transfer
using comp_eq_dest_lhs by force
lemma unitary_id[simp]: "unitary id_cblinfun"
by (simp add: unitary_def)
lemma orthogonal_on_basis_is_isometry:
assumes spanB: ‹ccspan B = ⊤›
assumes orthoU: ‹⋀b c. b∈B ⟹ c∈B ⟹ cinner (U *⇩V b) (U *⇩V c) = cinner b c›
shows ‹isometry U›
proof -
have [simp]: ‹b ∈ closure (cspan B)› for b
using spanB by transfer simp
have *: ‹cinner (U* *⇩V U *⇩V ψ) φ = cinner ψ φ› if ‹ψ∈B› and ‹φ∈B› for ψ φ
by (simp add: cinner_adj_left orthoU that(1) that(2))
have *: ‹cinner (U* *⇩V U *⇩V ψ) φ = cinner ψ φ› if ‹ψ∈B› for ψ φ
apply (rule bounded_clinear_eq_on_closure[where t=φ and G=B])
using bounded_clinear_cinner_right *[OF that]
by auto
have ‹U* *⇩V U *⇩V φ = φ› if ‹φ∈B› for φ
apply (rule cinner_extensionality)
apply (subst cinner_eq_flip)
by (simp add: * that)
then have ‹U* o⇩C⇩L U = id_cblinfun›
by (metis cblinfun_apply_cblinfun_compose cblinfun_eq_gen_eqI cblinfun_id_cblinfun_apply spanB)
then show ‹isometry U›
using isometry_def by blast
qed
lemma isometry_preserves_norm: ‹isometry U ⟹ norm (U *⇩V ψ) = norm ψ›
by (metis (no_types, lifting) cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply cinner_adj_right cnorm_eq isometryD)
lemma norm_isometry_compose:
assumes ‹isometry U›
shows ‹norm (U o⇩C⇩L A) = norm A›
proof -
have *: ‹norm (U *⇩V A *⇩V ψ) = norm (A *⇩V ψ)› for ψ
by (smt (verit, ccfv_threshold) assms cblinfun_apply_cblinfun_compose cinner_adj_right cnorm_eq id_cblinfun_apply isometryD)
have ‹norm (U o⇩C⇩L A) = (SUP ψ. norm (U *⇩V A *⇩V ψ) / norm ψ)›
unfolding norm_cblinfun_Sup by auto
also have ‹… = (SUP ψ. norm (A *⇩V ψ) / norm ψ)›
using * by auto
also have ‹… = norm A›
unfolding norm_cblinfun_Sup by auto
finally show ?thesis
by simp
qed
lemma norm_isometry:
fixes U :: ‹'a::{chilbert_space,not_singleton} ⇒⇩C⇩L 'b::complex_inner›
assumes ‹isometry U›
shows ‹norm U = 1›
apply (subst asm_rl[of ‹U = U o⇩C⇩L id_cblinfun›], simp)
apply (subst norm_isometry_compose, simp add: assms)
by simp
lemma norm_preserving_isometry: ‹isometry U› if ‹⋀ψ. norm (U *⇩V ψ) = norm ψ›
by (smt (verit, ccfv_SIG) cblinfun_cinner_eqI cblinfun_id_cblinfun_apply cinner_adj_right cnorm_eq isometry_def simp_a_oCL_b' that)
lemma norm_isometry_compose': ‹norm (A o⇩C⇩L U) = norm A› if ‹isometry (U*)›
by (smt (verit) cblinfun_compose_assoc cblinfun_compose_id_right double_adj isometryD mult_cancel_left2 norm_AadjA norm_cblinfun_compose norm_isometry_compose norm_zero power2_eq_square right_diff_distrib that zero_less_norm_iff)
lemma unitary_nonzero[simp]: ‹¬ unitary (0 :: 'a::{chilbert_space, not_singleton} ⇒⇩C⇩L _)›
by (simp add: unitary_def)
lemma isometry_inj:
assumes ‹isometry U›
shows ‹inj_on U X›
apply (rule inj_on_inverseI[where g=‹U*›])
using assms by (simp flip: cblinfun_apply_cblinfun_compose)
lemma unitary_inj:
assumes ‹unitary U›
shows ‹inj_on U X›
apply (rule isometry_inj)
using assms by simp
lemma unitary_adj_inv: ‹unitary U ⟹ cblinfun_apply (U*) = inv (cblinfun_apply U)›
apply (rule inj_imp_inv_eq[symmetric])
apply (simp add: unitary_inj)
unfolding unitary_def
by (simp flip: cblinfun_apply_cblinfun_compose)
lemma isometry_cinner_both_sides:
assumes ‹isometry U›
shows ‹cinner (U x) (U y) = cinner x y›
using assms by (simp add: flip: cinner_adj_right cblinfun_apply_cblinfun_compose)
lemma isometry_image_is_ortho_set:
assumes ‹is_ortho_set A›
assumes ‹isometry U›
shows ‹is_ortho_set (U ` A)›
using assms apply (auto simp add: is_ortho_set_def isometry_cinner_both_sides)
by (metis cinner_eq_zero_iff isometry_cinner_both_sides)
subsection ‹Product spaces›
lift_definition cblinfun_left :: ‹'a::complex_normed_vector ⇒⇩C⇩L ('a×'b::complex_normed_vector)› is ‹(λx. (x,0))›
by (auto intro!: bounded_clinearI[where K=1])
lift_definition cblinfun_right :: ‹'b::complex_normed_vector ⇒⇩C⇩L ('a::complex_normed_vector×'b)› is ‹(λx. (0,x))›
by (auto intro!: bounded_clinearI[where K=1])
lemma isometry_cblinfun_left[simp]: ‹isometry cblinfun_left›
apply (rule orthogonal_on_basis_is_isometry[of some_chilbert_basis])
apply simp
by transfer simp
lemma isometry_cblinfun_right[simp]: ‹isometry cblinfun_right›
apply (rule orthogonal_on_basis_is_isometry[of some_chilbert_basis])
apply simp
by transfer simp
lemma cblinfun_left_right_ortho[simp]: ‹cblinfun_left* o⇩C⇩L cblinfun_right = 0›
proof -
have ‹x ∙⇩C ((cblinfun_left* o⇩C⇩L cblinfun_right) *⇩V y) = 0› for x :: 'b and y :: 'a
apply (simp add: cinner_adj_right)
by transfer auto
then show ?thesis
by (metis cblinfun.zero_left cblinfun_eqI cinner_eq_zero_iff)
qed
lemma cblinfun_right_left_ortho[simp]: ‹cblinfun_right* o⇩C⇩L cblinfun_left = 0›
proof -
have ‹x ∙⇩C ((cblinfun_right* o⇩C⇩L cblinfun_left) *⇩V y) = 0› for x :: 'b and y :: 'a
apply (simp add: cinner_adj_right)
by transfer auto
then show ?thesis
by (metis cblinfun.zero_left cblinfun_eqI cinner_eq_zero_iff)
qed
lemma cblinfun_left_apply[simp]: ‹cblinfun_left *⇩V ψ = (ψ,0)›
by transfer simp
lemma cblinfun_left_adj_apply[simp]: ‹cblinfun_left* *⇩V ψ = fst ψ›
apply (cases ψ)
by (auto intro!: cinner_extensionality[of ‹_ *⇩V _›] simp: cinner_adj_right)
lemma cblinfun_right_apply[simp]: ‹cblinfun_right *⇩V ψ = (0,ψ)›
by transfer simp
lemma cblinfun_right_adj_apply[simp]: ‹cblinfun_right* *⇩V ψ = snd ψ›
apply (cases ψ)
by (auto intro!: cinner_extensionality[of ‹_ *⇩V _›] simp: cinner_adj_right)
lift_definition ccsubspace_Times :: ‹'a::complex_normed_vector ccsubspace ⇒ 'b::complex_normed_vector ccsubspace ⇒ ('a×'b) ccsubspace› is
Product_Type.Times
proof -
fix S :: ‹'a set› and T :: ‹'b set›
assume [simp]: ‹closed_csubspace S› ‹closed_csubspace T›
have ‹csubspace (S × T)›
by (simp add: complex_vector.subspace_Times)
moreover have ‹closed (S × T)›
by (simp add: closed_Times closed_csubspace.closed)
ultimately show ‹closed_csubspace (S × T)›
by (rule closed_csubspace.intro)
qed
lemma ccspan_Times: ‹ccspan (S × T) = ccsubspace_Times (ccspan S) (ccspan T)› if ‹0 ∈ S› and ‹0 ∈ T›
proof (transfer fixing: S T)
from that have ‹closure (cspan (S × T)) = closure (cspan S × cspan T)›
by (simp add: cspan_Times)
also have ‹… = closure (cspan S) × closure (cspan T)›
using closure_Times by blast
finally show ‹closure (cspan (S × T)) = closure (cspan S) × closure (cspan T)›
by -
qed
lemma ccspan_Times_sing1: ‹ccspan ({0::'a::complex_normed_vector} × B) = ccsubspace_Times 0 (ccspan B)›
proof (transfer fixing: B)
have ‹closure (cspan ({0::'a} × B)) = closure ({0} × cspan B)›
by (simp add: complex_vector.span_Times_sing1)
also have ‹… = closure {0} × closure (cspan B)›
using closure_Times by blast
also have ‹… = {0} × closure (cspan B)›
by simp
finally show ‹closure (cspan ({0::'a} × B)) = {0} × closure (cspan B)›
by -
qed
lemma ccspan_Times_sing2: ‹ccspan (B × {0::'a::complex_normed_vector}) = ccsubspace_Times (ccspan B) 0›
proof (transfer fixing: B)
have ‹closure (cspan (B × {0::'a})) = closure (cspan B × {0})›
by (simp add: complex_vector.span_Times_sing2)
also have ‹… = closure (cspan B) × closure {0}›
using closure_Times by blast
also have ‹… = closure (cspan B) × {0}›
by simp
finally show ‹closure (cspan (B × {0::'a})) = closure (cspan B) × {0}›
by -
qed
lemma ccsubspace_Times_sup: ‹sup (ccsubspace_Times A B) (ccsubspace_Times C D) = ccsubspace_Times (sup A C) (sup B D)›
proof transfer
fix A C :: ‹'a set› and B D :: ‹'b set›
have ‹A × B +⇩M C × D = closure ((A × B) + (C × D))›
using closed_sum_def by blast
also have ‹… = closure ((A + C) × (B + D))›
by (simp add: set_Times_plus_distrib)
also have ‹… = closure (A + C) × closure (B + D)›
by (simp add: closure_Times)
also have ‹… = (A +⇩M C) × (B +⇩M D)›
by (simp add: closed_sum_def)
finally show ‹A × B +⇩M C × D = (A +⇩M C) × (B +⇩M D)›
by -
qed
lemma ccsubspace_Times_top_top[simp]: ‹ccsubspace_Times top top = top›
by transfer simp
lemma is_ortho_set_prod:
assumes ‹is_ortho_set B› ‹is_ortho_set B'›
shows ‹is_ortho_set ((B × {0}) ∪ ({0} × B'))›
using assms unfolding is_ortho_set_def
apply (auto simp: is_onb_def is_ortho_set_def zero_prod_def)
by (meson is_onb_def is_ortho_set_def)+
lemma ccsubspace_Times_ccspan:
assumes ‹ccspan B = S› and ‹ccspan B' = S'›
shows ‹ccspan ((B × {0}) ∪ ({0} × B')) = ccsubspace_Times S S'›
by (smt (z3) Diff_eq_empty_iff Sigma_cong assms(1) assms(2) ccspan.rep_eq ccspan_0 ccspan_Times_sing1 ccspan_Times_sing2 ccspan_of_empty ccspan_remove_0 ccspan_superset ccspan_union ccsubspace_Times_sup complex_vector.span_insert_0 space_as_set_bot sup_bot_left sup_bot_right)
lemma is_onb_prod:
assumes ‹is_onb B› ‹is_onb B'›
shows ‹is_onb ((B × {0}) ∪ ({0} × B'))›
using assms by (auto intro!: is_ortho_set_prod simp add: is_onb_def ccsubspace_Times_ccspan)
subsection ‹Images›
text ‹The following definition defines the image of a closed subspace \<^term>‹S› under a bounded operator \<^term>‹A›.
We do not define that image as the image of \<^term>‹A› seen as a function (\<^term>‹A ` S›) but as the topological closure of that image.
This is because \<^term>‹A ` S› might in general not be closed.
For example, if $e_i$ ($i\in\mathbb N$) form an orthonormal basis, and $A$ maps $e_i$ to $e_i/i$,
then all $e_i$ are in \<^term>‹A ` S›, so the closure of \<^term>‹A ` S› is the whole space.
However, $\sum_i e_i/i$ is not in \<^term>‹A ` S› because its preimage would have to be $\sum_i e_i$ which does not converge.
So \<^term>‹A ` S› does not contain the whole space, hence it is not closed.›
lift_definition cblinfun_image :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector
⇒ 'a ccsubspace ⇒ 'b ccsubspace› (infixr "*⇩S" 70)
is "λA S. closure (A ` S)"
using bounded_clinear_def closed_closure closed_csubspace.intro
by (simp add: bounded_clinear_def complex_vector.linear_subspace_image closure_is_closed_csubspace)
lemma cblinfun_image_mono:
assumes a1: "S ≤ T"
shows "A *⇩S S ≤ A *⇩S T"
using a1
by (simp add: cblinfun_image.rep_eq closure_mono image_mono less_eq_ccsubspace.rep_eq)
lemma cblinfun_image_0[simp]:
shows "U *⇩S 0 = 0"
thm zero_ccsubspace_def
by transfer (simp add: bounded_clinear_def complex_vector.linear_0)
lemma cblinfun_image_bot[simp]: "U *⇩S bot = bot"
using cblinfun_image_0 by auto
lemma cblinfun_image_sup[simp]:
fixes A B :: ‹'a::chilbert_space ccsubspace› and U :: "'a ⇒⇩C⇩L'b::chilbert_space"
shows ‹U *⇩S (sup A B) = sup (U *⇩S A) (U *⇩S B)›
apply transfer using bounded_clinear.bounded_linear closure_image_closed_sum by blast
lemma scaleC_cblinfun_image[simp]:
fixes A :: ‹'a::chilbert_space ⇒⇩C⇩L 'b :: chilbert_space›
and S :: ‹'a ccsubspace› and α :: complex
shows ‹(α *⇩C A) *⇩S S = α *⇩C (A *⇩S S)›
proof-
have ‹closure ( ( ((*⇩C) α) ∘ (cblinfun_apply A) ) ` space_as_set S) =
((*⇩C) α) ` (closure (cblinfun_apply A ` space_as_set S))›
by (metis closure_scaleC image_comp)
hence ‹(closure (cblinfun_apply (α *⇩C A) ` space_as_set S)) =
((*⇩C) α) ` (closure (cblinfun_apply A ` space_as_set S))›
by (metis (mono_tags, lifting) comp_apply image_cong scaleC_cblinfun.rep_eq)
hence ‹Abs_ccsubspace (closure (cblinfun_apply (α *⇩C A) ` space_as_set S)) =
α *⇩C Abs_ccsubspace (closure (cblinfun_apply A ` space_as_set S))›
by (metis space_as_set_inverse cblinfun_image.rep_eq scaleC_ccsubspace.rep_eq)
have x1: "Abs_ccsubspace (closure ((*⇩V) (α *⇩C A) ` space_as_set S)) =
α *⇩C Abs_ccsubspace (closure ((*⇩V) A ` space_as_set S))"
using ‹Abs_ccsubspace (closure (cblinfun_apply (α *⇩C A) ` space_as_set S)) =
α *⇩C Abs_ccsubspace (closure (cblinfun_apply A ` space_as_set S))›
by blast
show ?thesis
unfolding cblinfun_image_def using x1 by force
qed
lemma cblinfun_image_id[simp]:
"id_cblinfun *⇩S ψ = ψ"
by transfer (simp add: closed_csubspace.closed)
lemma cblinfun_compose_image:
‹(A o⇩C⇩L B) *⇩S S = A *⇩S (B *⇩S S)›
apply transfer unfolding image_comp[symmetric]
apply (rule closure_bounded_linear_image_subset_eq[symmetric])
by (simp add: bounded_clinear.bounded_linear)
lemmas cblinfun_assoc_left = cblinfun_compose_assoc[symmetric] cblinfun_compose_image[symmetric]
add.assoc[where ?'a="'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space", symmetric]
lemmas cblinfun_assoc_right = cblinfun_compose_assoc cblinfun_compose_image
add.assoc[where ?'a="'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space"]
lemma cblinfun_image_INF_leq[simp]:
fixes U :: "'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and V :: "'a ⇒ 'b ccsubspace"
shows ‹U *⇩S (INF i∈X. V i) ≤ (INF i∈X. U *⇩S (V i))›
apply transfer
by (simp add: INT_greatest Inter_lower closure_mono image_mono)
lemma isometry_cblinfun_image_inf_distrib':
fixes U::‹'a::complex_normed_vector ⇒⇩C⇩L 'b::cbanach› and B C::"'a ccsubspace"
shows "U *⇩S (inf B C) ≤ inf (U *⇩S B) (U *⇩S C)"
proof -
define V where ‹V b = (if b then B else C)› for b
have ‹U *⇩S (INF i. V i) ≤ (INF i. U *⇩S (V i))›
by auto
then show ?thesis
unfolding V_def
by (metis (mono_tags, lifting) INF_UNIV_bool_expand)
qed
lemma cblinfun_image_eq:
fixes S :: "'a::cbanach ccsubspace"
and A B :: "'a::cbanach ⇒⇩C⇩L'b::cbanach"
assumes "⋀x. x ∈ G ⟹ A *⇩V x = B *⇩V x" and "ccspan G ≥ S"
shows "A *⇩S S = B *⇩S S"
proof (use assms in transfer)
fix G :: "'a set" and A :: "'a ⇒ 'b" and B :: "'a ⇒ 'b" and S :: "'a set"
assume a1: "bounded_clinear A"
assume a2: "bounded_clinear B"
assume a3: "⋀x. x ∈ G ⟹ A x = B x"
assume a4: "S ⊆ closure (cspan G)"
have "A ` closure S = B ` closure S"
by (smt (verit, best) UnCI a1 a2 a3 a4 bounded_clinear_eq_on_closure closure_Un closure_closure image_cong sup.absorb_iff1)
then show "closure (A ` S) = closure (B ` S)"
by (metis bounded_clinear.bounded_linear a1 a2 closure_bounded_linear_image_subset_eq)
qed
lemma cblinfun_fixes_range:
assumes "A o⇩C⇩L B = B" and "ψ ∈ space_as_set (B *⇩S top)"
shows "A *⇩V ψ = ψ"
proof-
define rangeB rangeB' where "rangeB = space_as_set (B *⇩S top)"
and "rangeB' = range (cblinfun_apply B)"
from assms have "ψ ∈ closure rangeB'"
by (simp add: cblinfun_image.rep_eq rangeB'_def top_ccsubspace.rep_eq)
then obtain ψi where ψi_lim: "ψi ⇢ ψ" and ψi_B: "ψi i ∈ rangeB'" for i
using closure_sequential by blast
have A_invariant: "A *⇩V ψi i = ψi i"
for i
proof-
from ψi_B obtain φ where φ: "ψi i = B *⇩V φ"
using rangeB'_def by blast
hence "A *⇩V ψi i = (A o⇩C⇩L B) *⇩V φ"
by (simp add: cblinfun_compose.rep_eq)
also have "… = B *⇩V φ"
by (simp add: assms)
also have "… = ψi i"
by (simp add: φ)
finally show ?thesis.
qed
from ψi_lim have "(λi. A *⇩V (ψi i)) ⇢ A *⇩V ψ"
by (rule isCont_tendsto_compose[rotated], simp)
with A_invariant have "(λi. ψi i) ⇢ A *⇩V ψ"
by auto
with ψi_lim show "A *⇩V ψ = ψ"
using LIMSEQ_unique by blast
qed
lemma zero_cblinfun_image[simp]: "0 *⇩S S = (0::_ ccsubspace)"
by transfer (simp add: complex_vector.subspace_0 image_constant[where x=0])
lemma cblinfun_image_INF_eq_general:
fixes V :: "'a ⇒ 'b::chilbert_space ccsubspace"
and U :: "'b ⇒⇩C⇩L'c::chilbert_space"
and Uinv :: "'c ⇒⇩C⇩L'b"
assumes UinvUUinv: "Uinv o⇩C⇩L U o⇩C⇩L Uinv = Uinv" and UUinvU: "U o⇩C⇩L Uinv o⇩C⇩L U = U"
and V: "⋀i. V i ≤ Uinv *⇩S top"
and ‹X ≠ {}›
shows "U *⇩S (INF i∈X. V i) = (INF i∈X. U *⇩S V i)"
proof (rule antisym)
show "U *⇩S (INF i∈X. V i) ≤ (INF i∈X. U *⇩S V i)"
by (rule cblinfun_image_INF_leq)
next
define rangeU rangeUinv where "rangeU = U *⇩S top" and "rangeUinv = Uinv *⇩S top"
define INFUV INFV where INFUV_def: "INFUV = (INF i∈X. U *⇩S V i)" and INFV_def: "INFV = (INF i∈X. V i)"
from assms have "V i ≤ rangeUinv"
for i
unfolding rangeUinv_def by simp
moreover have "(Uinv o⇩C⇩L U) *⇩V ψ = ψ" if "ψ ∈ space_as_set rangeUinv"
for ψ
using UinvUUinv cblinfun_fixes_range rangeUinv_def that by fastforce
ultimately have "(Uinv o⇩C⇩L U) *⇩V ψ = ψ" if "ψ ∈ space_as_set (V i)"
for ψ i
using less_eq_ccsubspace.rep_eq that by blast
hence d1: "(Uinv o⇩C⇩L U) *⇩S (V i) = (V i)" for i
proof (transfer fixing: i)
fix V :: "'a ⇒ 'b set"
and Uinv :: "'c ⇒ 'b"
and U :: "'b ⇒ 'c"
assume "pred_fun ⊤ closed_csubspace V"
and "bounded_clinear Uinv"
and "bounded_clinear U"
and "⋀ψ i. ψ ∈ V i ⟹ (Uinv ∘ U) ψ = ψ"
then show "closure ((Uinv ∘ U) ` V i) = V i"
proof auto
fix x
from ‹pred_fun ⊤ closed_csubspace V›
show "x ∈ V i"
if "x ∈ closure (V i)"
using that apply simp
by (metis orthogonal_complement_of_closure closed_csubspace.subspace double_orthogonal_complement_id closure_is_closed_csubspace)
with ‹pred_fun ⊤ closed_csubspace V›
show "x ∈ closure (V i)"
if "x ∈ V i"
using that
using setdist_eq_0_sing_1 setdist_sing_in_set
by blast
qed
qed
have "U *⇩S V i ≤ rangeU" for i
by (simp add: cblinfun_image_mono rangeU_def)
hence "INFUV ≤ rangeU"
unfolding INFUV_def using ‹X ≠ {}›
by (metis INF_eq_const INF_lower2)
moreover have "(U o⇩C⇩L Uinv) *⇩V ψ = ψ" if "ψ ∈ space_as_set rangeU" for ψ
using UUinvU cblinfun_fixes_range rangeU_def that by fastforce
ultimately have x: "(U o⇩C⇩L Uinv) *⇩V ψ = ψ" if "ψ ∈ space_as_set INFUV" for ψ
by (simp add: in_mono less_eq_ccsubspace.rep_eq that)
have "closure ((U ∘ Uinv) ` INFUV) = INFUV"
if "closed_csubspace INFUV"
and "bounded_clinear U"
and "bounded_clinear Uinv"
and "⋀ψ. ψ ∈ INFUV ⟹ (U ∘ Uinv) ψ = ψ"
for INFUV :: "'c set"
using that
proof auto
fix x
show "x ∈ INFUV" if "x ∈ closure INFUV"
using that ‹closed_csubspace INFUV›
by (metis orthogonal_complement_of_closure closed_csubspace.subspace double_orthogonal_complement_id closure_is_closed_csubspace)
show "x ∈ closure INFUV"
if "x ∈ INFUV"
using that ‹closed_csubspace INFUV›
using setdist_eq_0_sing_1 setdist_sing_in_set
by (simp add: closed_csubspace.closed)
qed
hence "(U o⇩C⇩L Uinv) *⇩S INFUV = INFUV"
by (metis (mono_tags, opaque_lifting) x cblinfun_image.rep_eq cblinfun_image_id id_cblinfun_apply image_cong
space_as_set_inject)
hence "INFUV = U *⇩S Uinv *⇩S INFUV"
by (simp add: cblinfun_compose_image)
also have "… ≤ U *⇩S (INF i∈X. Uinv *⇩S U *⇩S V i)"
unfolding INFUV_def
by (metis cblinfun_image_mono cblinfun_image_INF_leq)
also have "… = U *⇩S INFV"
using d1
by (metis (no_types, lifting) INFV_def cblinfun_assoc_left(2) image_cong)
finally show "INFUV ≤ U *⇩S INFV".
qed
lemma unitary_range[simp]:
assumes "unitary U"
shows "U *⇩S top = top"
using assms unfolding unitary_def by transfer (metis closure_UNIV comp_apply surj_def)
lemma range_adjoint_isometry:
assumes "isometry U"
shows "U* *⇩S top = top"
proof-
from assms have "top = U* *⇩S U *⇩S top"
by (simp add: cblinfun_assoc_left(2))
also have "… ≤ U* *⇩S top"
by (simp add: cblinfun_image_mono)
finally show ?thesis
using top.extremum_unique by blast
qed
lemma cblinfun_image_INF_eq[simp]:
fixes V :: "'a ⇒ 'b::chilbert_space ccsubspace"
and U :: "'b ⇒⇩C⇩L 'c::chilbert_space"
assumes ‹isometry U› ‹X ≠ {}›
shows "U *⇩S (INF i∈X. V i) = (INF i∈X. U *⇩S V i)"
proof -
from ‹isometry U› have "U* o⇩C⇩L U o⇩C⇩L U* = U*"
unfolding isometry_def by simp
moreover from ‹isometry U› have "U o⇩C⇩L U* o⇩C⇩L U = U"
unfolding isometry_def
by (simp add: cblinfun_compose_assoc)
moreover have "V i ≤ U* *⇩S top" for i
by (simp add: range_adjoint_isometry assms)
ultimately show ?thesis
using ‹X ≠ {}› by (rule cblinfun_image_INF_eq_general)
qed
lemma isometry_cblinfun_image_inf_distrib[simp]:
fixes U::‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
and X Y::"'a ccsubspace"
assumes "isometry U"
shows "U *⇩S (inf X Y) = inf (U *⇩S X) (U *⇩S Y)"
using cblinfun_image_INF_eq[where V="λb. if b then X else Y" and U=U and X=UNIV]
unfolding INF_UNIV_bool_expand
using assms by auto
lemma cblinfun_image_ccspan:
shows "A *⇩S ccspan G = ccspan ((*⇩V) A ` G)"
by transfer (simp add: bounded_clinear.bounded_linear bounded_clinear_def closure_bounded_linear_image_subset_eq complex_vector.linear_span_image)
lemma cblinfun_apply_in_image[simp]: "A *⇩V ψ ∈ space_as_set (A *⇩S ⊤)"
by (metis cblinfun_image.rep_eq closure_subset in_mono range_eqI top_ccsubspace.rep_eq)
lemma cblinfun_plus_image_distr:
‹(A + B) *⇩S S ≤ A *⇩S S ⊔ B *⇩S S›
by transfer (smt (verit, ccfv_threshold) closed_closure closed_sum_def closure_minimal closure_subset image_subset_iff set_plus_intro subset_eq)
lemma cblinfun_sum_image_distr:
‹(∑i∈I. A i) *⇩S S ≤ (SUP i∈I. A i *⇩S S)›
proof (cases ‹finite I›)
case True
then show ?thesis
proof induction
case empty
then show ?case
by auto
next
case (insert x F)
then show ?case
by auto (smt (z3) cblinfun_plus_image_distr inf_sup_aci(6) le_iff_sup)
qed
next
case False
then show ?thesis
by auto
qed
lemma space_as_set_image_commute:
assumes UV: ‹U o⇩C⇩L V = id_cblinfun› and VU: ‹V o⇩C⇩L U = id_cblinfun›
shows ‹(*⇩V) U ` space_as_set T = space_as_set (U *⇩S T)›
proof -
have ‹space_as_set (U *⇩S T) = U ` V ` space_as_set (U *⇩S T)›
by (simp add: image_image UV flip: cblinfun_apply_cblinfun_compose)
also have ‹… ⊆ U ` space_as_set (V *⇩S U *⇩S T)›
by (metis cblinfun_image.rep_eq closure_subset image_mono)
also have ‹… = U ` space_as_set T›
by (simp add: VU cblinfun_assoc_left(2))
finally have 1: ‹space_as_set (U *⇩S T) ⊆ U ` space_as_set T›
by -
have 2: ‹U ` space_as_set T ⊆ space_as_set (U *⇩S T)›
by (simp add: cblinfun_image.rep_eq closure_subset)
from 1 2 show ?thesis
by simp
qed
lemma right_total_rel_ccsubspace:
fixes R :: ‹'a::complex_normed_vector ⇒ 'b::complex_normed_vector ⇒ bool›
assumes UV: ‹U o⇩C⇩L V = id_cblinfun›
assumes VU: ‹V o⇩C⇩L U = id_cblinfun›
assumes R_def: ‹⋀x y. R x y ⟷ x = U *⇩V y›
shows ‹right_total (rel_ccsubspace R)›
proof (rule right_totalI)
fix T :: ‹'b ccsubspace›
show ‹∃S. rel_ccsubspace R S T›
apply (rule exI[of _ ‹U *⇩S T›])
using UV VU by (auto simp add: rel_ccsubspace_def R_def rel_set_def simp flip: space_as_set_image_commute)
qed
lemma left_total_rel_ccsubspace:
fixes R :: ‹'a::complex_normed_vector ⇒ 'b::complex_normed_vector ⇒ bool›
assumes UV: ‹U o⇩C⇩L V = id_cblinfun›
assumes VU: ‹V o⇩C⇩L U = id_cblinfun›
assumes R_def: ‹⋀x y. R x y ⟷ y = U *⇩V x›
shows ‹left_total (rel_ccsubspace R)›
proof -
have ‹right_total (rel_ccsubspace (conversep R))›
apply (rule right_total_rel_ccsubspace)
using assms by auto
then show ?thesis
by (auto intro!: right_total_conversep[THEN iffD1] simp: converse_rel_ccsubspace)
qed
lemma cblinfun_image_bot_zero[simp]: ‹A *⇩S top = bot ⟷ A = 0›
by (metis Complex_Bounded_Linear_Function.zero_cblinfun_image bot_ccsubspace.rep_eq cblinfun_apply_in_image cblinfun_eqI empty_iff insert_iff zero_ccsubspace_def)
lemma surj_isometry_is_unitary:
fixes U :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes ‹isometry U›
assumes ‹U *⇩S ⊤ = ⊤›
shows ‹unitary U›
by (metis UNIV_I assms(1) assms(2) cblinfun_assoc_left(1) cblinfun_compose_id_right cblinfun_eqI cblinfun_fixes_range id_cblinfun_apply isometry_def space_as_set_top unitary_def)
lemma cblinfun_apply_in_image': "A *⇩V ψ ∈ space_as_set (A *⇩S S)" if ‹ψ ∈ space_as_set S›
by (metis cblinfun_image.rep_eq closure_subset image_subset_iff that)
lemma cblinfun_image_ccspan_leqI:
assumes ‹⋀v. v ∈ M ⟹ A *⇩V v ∈ space_as_set T›
shows ‹A *⇩S ccspan M ≤ T›
by (simp add: assms cblinfun_image_ccspan ccspan_leqI image_subsetI)
lemma cblinfun_same_on_image: ‹A ψ = B ψ› if eq: ‹A o⇩C⇩L C = B o⇩C⇩L C› and mem: ‹ψ ∈ space_as_set (C *⇩S ⊤)›
proof -
have ‹A ψ = B ψ› if ‹ψ ∈ range C› for ψ
by (metis (no_types, lifting) eq cblinfun_apply_cblinfun_compose image_iff that)
moreover have ‹ψ ∈ closure (range C)›
by (metis cblinfun_image.rep_eq mem top_ccsubspace.rep_eq)
ultimately show ?thesis
apply (rule on_closure_eqI)
by (auto simp: continuous_on_eq_continuous_at)
qed
lemma lift_cblinfun_comp:
assumes ‹a o⇩C⇩L b = c›
shows ‹a o⇩C⇩L b = c›
and ‹a o⇩C⇩L (b o⇩C⇩L d) = c o⇩C⇩L d›
and ‹a *⇩S (b *⇩S S) = c *⇩S S›
and ‹a *⇩V (b *⇩V x) = c *⇩V x›
apply (fact assms)
apply (simp add: assms cblinfun_assoc_left(1))
using assms cblinfun_assoc_left(2) apply force
using assms by force
lemma cblinfun_image_def2: ‹A *⇩S S = ccspan ((*⇩V) A ` space_as_set S)›
apply (simp add: flip: cblinfun_image_ccspan)
by (metis ccspan_leqI ccspan_superset less_eq_ccsubspace.rep_eq order_class.order_eq_iff)
lemma unitary_image_onb:
assumes ‹is_onb A›
assumes ‹unitary U›
shows ‹is_onb (U ` A)›
using assms
by (auto simp add: is_onb_def isometry_image_is_ortho_set isometry_preserves_norm
simp flip: cblinfun_image_ccspan)
subsection ‹Sandwiches›
lift_definition sandwich :: ‹('a::chilbert_space ⇒⇩C⇩L 'b::complex_inner) ⇒ (('a ⇒⇩C⇩L 'a) ⇒⇩C⇩L ('b ⇒⇩C⇩L 'b))› is
‹λ(A::'a⇒⇩C⇩L'b) B. A o⇩C⇩L B o⇩C⇩L A*›
proof
fix A :: ‹'a ⇒⇩C⇩L 'b› and B B1 B2 :: ‹'a ⇒⇩C⇩L 'a› and c :: complex
show ‹A o⇩C⇩L (B1 + B2) o⇩C⇩L A* = (A o⇩C⇩L B1 o⇩C⇩L A*) + (A o⇩C⇩L B2 o⇩C⇩L A*)›
by (simp add: cblinfun_compose_add_left cblinfun_compose_add_right)
show ‹A o⇩C⇩L (c *⇩C B) o⇩C⇩L A* = c *⇩C (A o⇩C⇩L B o⇩C⇩L A*)›
by auto
show ‹∃K. ∀B. norm (A o⇩C⇩L B o⇩C⇩L A*) ≤ norm B * K›
proof (rule exI[of _ ‹norm A * norm (A*)›], rule allI)
fix B
have ‹norm (A o⇩C⇩L B o⇩C⇩L A*) ≤ norm (A o⇩C⇩L B) * norm (A*)›
using norm_cblinfun_compose by blast
also have ‹… ≤ (norm A * norm B) * norm (A*)›
by (simp add: mult_right_mono norm_cblinfun_compose)
finally show ‹norm (A o⇩C⇩L B o⇩C⇩L A*) ≤ norm B * (norm A * norm (A*))›
by (simp add: mult.assoc vector_space_over_itself.scale_left_commute)
qed
qed
lemma sandwich_0[simp]: ‹sandwich 0 = 0›
by (simp add: cblinfun_eqI sandwich.rep_eq)
lemma sandwich_apply: ‹sandwich A *⇩V B = A o⇩C⇩L B o⇩C⇩L A*›
apply (transfer fixing: A B) by auto
lemma sandwich_arg_compose:
assumes ‹isometry U›
shows ‹sandwich U x o⇩C⇩L sandwich U y = sandwich U (x o⇩C⇩L y)›
apply (simp add: sandwich_apply)
by (metis (no_types, lifting) lift_cblinfun_comp(2) assms cblinfun_compose_id_right isometryD)
lemma norm_sandwich: ‹norm (sandwich A) = (norm A)⇧2› for A :: ‹'a::{chilbert_space} ⇒⇩C⇩L 'b::{complex_inner}›
proof -
have main: ‹norm (sandwich A) = (norm A)⇧2› for A :: ‹'c::{chilbert_space,not_singleton} ⇒⇩C⇩L 'd::{complex_inner}›
proof (rule norm_cblinfun_eqI)
show ‹(norm A)⇧2 ≤ norm (sandwich A *⇩V id_cblinfun) / norm (id_cblinfun :: 'c ⇒⇩C⇩L _)›
apply (auto simp: sandwich_apply)
by -
fix B
have ‹norm (sandwich A *⇩V B) ≤ norm (A o⇩C⇩L B) * norm (A*)›
using norm_cblinfun_compose by (auto simp: sandwich_apply simp del: norm_adj)
also have ‹… ≤ (norm A * norm B) * norm (A*)›
by (simp add: mult_right_mono norm_cblinfun_compose)
also have ‹… ≤ (norm A)⇧2 * norm B›
by (simp add: power2_eq_square mult.assoc vector_space_over_itself.scale_left_commute)
finally show ‹norm (sandwich A *⇩V B) ≤ (norm A)⇧2 * norm B›
by -
show ‹0 ≤ (norm A)⇧2›
by auto
qed
show ?thesis
proof (cases ‹class.not_singleton TYPE('a)›)
case True
show ?thesis
apply (rule main[internalize_sort' 'c2])
apply standard[1]
using True by simp
next
case False
have ‹A = 0›
apply (rule cblinfun_from_CARD_1_0[internalize_sort' 'a])
apply (rule not_singleton_vs_CARD_1)
apply (rule False)
by standard
then show ?thesis
by simp
qed
qed
lemma sandwich_apply_adj: ‹sandwich A (B*) = (sandwich A B)*›
by (simp add: cblinfun_assoc_left(1) sandwich_apply)
lemma sandwich_id[simp]: "sandwich id_cblinfun = id_cblinfun"
apply (rule cblinfun_eqI)
by (auto simp: sandwich_apply)
lemma sandwich_compose: ‹sandwich (A o⇩C⇩L B) = sandwich A o⇩C⇩L sandwich B›
by (auto intro!: cblinfun_eqI simp: sandwich_apply)
lemma inj_sandwich_isometry: ‹inj (sandwich U)› if [simp]: ‹isometry U› for U :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
apply (rule inj_on_inverseI[where g=‹(*⇩V) (sandwich (U*))›])
by (auto simp flip: cblinfun_apply_cblinfun_compose sandwich_compose)
lemma sandwich_isometry_id: ‹isometry (U*) ⟹ sandwich U id_cblinfun = id_cblinfun›
by (simp add: sandwich_apply isometry_def)
subsection ‹Projectors›
lift_definition Proj :: "('a::chilbert_space) ccsubspace ⇒ 'a ⇒⇩C⇩L'a"
is ‹projection›
by (rule projection_bounded_clinear)
lemma Proj_range[simp]: "Proj S *⇩S top = S"
proof transfer
fix S :: ‹'a set› assume ‹closed_csubspace S›
then have "closure (range (projection S)) ⊆ S"
by (metis closed_csubspace.closed closed_csubspace.subspace closure_closed complex_vector.subspace_0 csubspace_is_convex dual_order.eq_iff insert_absorb insert_not_empty projection_image)
moreover have "S ⊆ closure (range (projection S))"
using ‹closed_csubspace S›
by (metis closed_csubspace_def closure_subset csubspace_is_convex equals0D projection_image subset_iff)
ultimately show ‹closure (range (projection S)) = S›
by auto
qed
lemma adj_Proj: ‹(Proj M)* = Proj M›
by transfer (simp add: projection_cadjoint)
lemma Proj_idempotent[simp]: ‹Proj M o⇩C⇩L Proj M = Proj M›
proof -
have u1: ‹(cblinfun_apply (Proj M)) = projection (space_as_set M)›
by transfer blast
have ‹closed_csubspace (space_as_set M)›
using space_as_set by auto
hence u2: ‹(projection (space_as_set M))∘(projection (space_as_set M))
= (projection (space_as_set M))›
using projection_idem by fastforce
have ‹(cblinfun_apply (Proj M)) ∘ (cblinfun_apply (Proj M)) = cblinfun_apply (Proj M)›
using u1 u2
by simp
hence ‹cblinfun_apply ((Proj M) o⇩C⇩L (Proj M)) = cblinfun_apply (Proj M)›
by (simp add: cblinfun_compose.rep_eq)
thus ?thesis using cblinfun_apply_inject
by auto
qed
lift_definition is_Proj :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'a ⇒ bool› is
‹λP. ∃M. is_projection_on P M› .
lemma is_Proj_id[simp]: ‹is_Proj id_cblinfun›
apply transfer
by (auto intro!: exI[of _ UNIV] simp: is_projection_on_def is_arg_min_def)
lemma Proj_top[simp]: ‹Proj ⊤ = id_cblinfun›
by (metis Proj_idempotent Proj_range cblinfun_eqI cblinfun_fixes_range id_cblinfun_apply iso_tuple_UNIV_I space_as_set_top)
lemma Proj_on_own_range':
fixes P :: ‹'a::chilbert_space ⇒⇩C⇩L'a›
assumes ‹P o⇩C⇩L P = P› and ‹P = P*›
shows ‹Proj (P *⇩S top) = P›
proof -
define M where "M = P *⇩S top"
have v3: "x ∈ (λx. x - P *⇩V x) -` {0}"
if "x ∈ range (cblinfun_apply P)"
for x :: 'a
proof-
have v3_1: ‹cblinfun_apply P ∘ cblinfun_apply P = cblinfun_apply P›
by (metis ‹P o⇩C⇩L P = P› cblinfun_compose.rep_eq)
have ‹∃t. P *⇩V t = x›
using that by blast
then obtain t where t_def: ‹P *⇩V t = x›
by blast
hence ‹x - P *⇩V x = x - P *⇩V (P *⇩V t)›
by simp
also have ‹… = x - (P *⇩V t)›
using v3_1
by (metis comp_apply)
also have ‹… = 0›
by (simp add: t_def)
finally have ‹x - P *⇩V x = 0›
by blast
thus ?thesis
by simp
qed
have v1: "range (cblinfun_apply P) ⊆ (λx. x - cblinfun_apply P x) -` {0}"
using v3
by blast
have "x ∈ range (cblinfun_apply P)"
if "x ∈ (λx. x - P *⇩V x) -` {0}"
for x :: 'a
proof-
have x1:‹x - P *⇩V x = 0›
using that by blast
have ‹x = P *⇩V x›
by (simp add: x1 eq_iff_diff_eq_0)
thus ?thesis
by blast
qed
hence v2: "(λx. x - cblinfun_apply P x) -` {0} ⊆ range (cblinfun_apply P)"
by blast
have i1: ‹range (cblinfun_apply P) = (λ x. x - cblinfun_apply P x) -` {0}›
using v1 v2
by (simp add: v1 dual_order.antisym)
have p1: ‹closed {(0::'a)}›
by simp
have p2: ‹continuous (at x) (λ x. x - P *⇩V x)›
for x
proof-
have ‹cblinfun_apply (id_cblinfun - P) = (λ x. x - P *⇩V x)›
by (simp add: id_cblinfun.rep_eq minus_cblinfun.rep_eq)
hence ‹bounded_clinear (cblinfun_apply (id_cblinfun - P))›
using cblinfun_apply
by blast
hence ‹continuous (at x) (cblinfun_apply (id_cblinfun - P))›
by (simp add: clinear_continuous_at)
thus ?thesis
using ‹cblinfun_apply (id_cblinfun - P) = (λ x. x - P *⇩V x)›
by simp
qed
have i2: ‹closed ( (λ x. x - P *⇩V x) -` {0} )›
using p1 p2
by (rule Abstract_Topology.continuous_closed_vimage)
have ‹closed (range (cblinfun_apply P))›
using i1 i2
by simp
have u2: ‹cblinfun_apply P x ∈ space_as_set M›
for x
by (simp add: M_def ‹closed (range ((*⇩V) P))› cblinfun_image.rep_eq top_ccsubspace.rep_eq)
have xy: ‹is_orthogonal (x - P *⇩V x) y›
if y1: ‹y ∈ space_as_set M›
for x y
proof-
have ‹∃t. y = P *⇩V t›
using y1
by (simp add: M_def ‹closed (range ((*⇩V) P))› cblinfun_image.rep_eq image_iff
top_ccsubspace.rep_eq)
then obtain t where t_def: ‹y = P *⇩V t›
by blast
have ‹(x - P *⇩V x) ∙⇩C y = (x - P *⇩V x) ∙⇩C (P *⇩V t)›
by (simp add: t_def)
also have ‹… = (P *⇩V (x - P *⇩V x)) ∙⇩C t›
by (metis ‹P = P*› cinner_adj_left)
also have ‹… = (P *⇩V x - P *⇩V (P *⇩V x)) ∙⇩C t›
by (simp add: cblinfun.diff_right)
also have ‹… = (P *⇩V x - P *⇩V x) ∙⇩C t›
by (metis assms(1) comp_apply cblinfun_compose.rep_eq)
also have ‹… = (0 ∙⇩C t)›
by simp
also have ‹… = 0›
by simp
finally show ?thesis by blast
qed
hence u1: ‹x - P *⇩V x ∈ orthogonal_complement (space_as_set M)›
for x
by (simp add: orthogonal_complementI)
have "closed_csubspace (space_as_set M)"
using space_as_set by auto
hence f1: "(Proj M) *⇩V a = P *⇩V a" for a
by (simp add: Proj.rep_eq projection_eqI u1 u2)
have "(+) ((P - Proj M) *⇩V a) = id" for a
using f1
by (auto intro!: ext simp add: minus_cblinfun.rep_eq)
hence "b - b = cblinfun_apply (P - Proj M) a"
for a b
by (metis (no_types) add_diff_cancel_right' id_apply)
hence "cblinfun_apply (id_cblinfun - (P - Proj M)) a = a"
for a
by (simp add: minus_cblinfun.rep_eq)
thus ?thesis
using u1 u2 cblinfun_apply_inject diff_diff_eq2 diff_eq_diff_eq eq_id_iff id_cblinfun.rep_eq
by (metis (no_types, opaque_lifting) M_def)
qed
lemma Proj_range_closed:
assumes "is_Proj P"
shows "closed (range (cblinfun_apply P))"
apply (rule is_projection_on_closed[where f=‹cblinfun_apply P›])
using assms is_Proj.rep_eq is_projection_on_image by auto
lemma Proj_is_Proj[simp]:
fixes M::‹'a::chilbert_space ccsubspace›
shows ‹is_Proj (Proj M)›
proof-
have u1: "closed_csubspace (space_as_set M)"
using space_as_set by blast
have v1: "h - Proj M *⇩V h
∈ orthogonal_complement (space_as_set M)" for h
by (simp add: Proj.rep_eq orthogonal_complementI projection_orthogonal u1)
have v2: "Proj M *⇩V h ∈ space_as_set M" for h
by (metis Proj.rep_eq mem_Collect_eq orthog_proj_exists projection_eqI space_as_set)
have u2: "is_projection_on ((*⇩V) (Proj M)) (space_as_set M)"
unfolding is_projection_on_def
by (simp add: smallest_dist_is_ortho u1 v1 v2)
show ?thesis
using u1 u2 is_Proj.rep_eq by blast
qed
lemma is_Proj_algebraic:
fixes P::‹'a::chilbert_space ⇒⇩C⇩L 'a›
shows ‹is_Proj P ⟷ P o⇩C⇩L P = P ∧ P = P*›
proof
have "P o⇩C⇩L P = P"
if "is_Proj P"
using that apply transfer
using is_projection_on_idem
by fastforce
moreover have "P = P*"
if "is_Proj P"
using that Proj_range_closed[OF that] is_projection_on_cadjoint[where π=P and M=‹range P›]
by transfer (metis bounded_clinear.axioms(1) closed_csubspace_UNIV closed_csubspace_def complex_vector.linear_subspace_image is_projection_on_image)
ultimately show "P o⇩C⇩L P = P ∧ P = P*"
if "is_Proj P"
using that
by blast
show "is_Proj P"
if "P o⇩C⇩L P = P ∧ P = P*"
using that Proj_on_own_range' Proj_is_Proj by metis
qed
lemma Proj_on_own_range:
fixes P :: ‹'a::chilbert_space ⇒⇩C⇩L'a›
assumes ‹is_Proj P›
shows ‹Proj (P *⇩S top) = P›
using Proj_on_own_range' assms is_Proj_algebraic by blast
lemma Proj_image_leq: "(Proj S) *⇩S A ≤ S"
by (metis Proj_range inf_top_left le_inf_iff isometry_cblinfun_image_inf_distrib')
lemma Proj_sandwich:
fixes A::"'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space"
assumes "isometry A"
shows "sandwich A *⇩V Proj S = Proj (A *⇩S S)"
proof -
define P where ‹P = A o⇩C⇩L Proj S o⇩C⇩L (A*)›
have ‹P o⇩C⇩L P = P›
using assms
unfolding P_def isometry_def
by (metis (no_types, lifting) Proj_idempotent cblinfun_assoc_left(1) cblinfun_compose_id_left)
moreover have ‹P = P*›
unfolding P_def
by (metis adj_Proj adj_cblinfun_compose cblinfun_assoc_left(1) double_adj)
ultimately have
‹∃M. P = Proj M ∧ space_as_set M = range (cblinfun_apply (A o⇩C⇩L (Proj S) o⇩C⇩L (A*)))›
using P_def Proj_on_own_range'
by (metis Proj_is_Proj Proj_range_closed cblinfun_image.rep_eq closure_closed top_ccsubspace.rep_eq)
then obtain M where ‹P = Proj M›
and ‹space_as_set M = range (cblinfun_apply (A o⇩C⇩L (Proj S) o⇩C⇩L (A*)))›
by blast
have f1: "A o⇩C⇩L Proj S = P o⇩C⇩L A"
by (simp add: P_def assms cblinfun_compose_assoc)
hence "P o⇩C⇩L A o⇩C⇩L A* = P"
using P_def by presburger
hence "(P o⇩C⇩L A) *⇩S (c ⊔ A* *⇩S d) = P *⇩S (A *⇩S c ⊔ d)"
for c d
by (simp add: cblinfun_assoc_left(2))
hence "P *⇩S (A *⇩S ⊤ ⊔ c) = (P o⇩C⇩L A) *⇩S ⊤"
for c
by (metis sup_top_left)
hence ‹M = A *⇩S S›
using f1
by (metis ‹P = Proj M› cblinfun_assoc_left(2) Proj_range sup_top_right)
thus ?thesis
using ‹P = Proj M›
unfolding P_def sandwich_apply by blast
qed
lemma Proj_orthog_ccspan_union:
assumes "⋀x y. x ∈ X ⟹ y ∈ Y ⟹ is_orthogonal x y"
shows ‹Proj (ccspan (X ∪ Y)) = Proj (ccspan X) + Proj (ccspan Y)›
proof -
have ‹x ∈ cspan X ⟹ y ∈ cspan Y ⟹ is_orthogonal x y› for x y
apply (rule is_orthogonal_closure_cspan[where X=X and Y=Y])
using closure_subset assms by auto
then have ‹x ∈ closure (cspan X) ⟹ y ∈ closure (cspan Y) ⟹ is_orthogonal x y› for x y
by (metis orthogonal_complementI orthogonal_complement_of_closure orthogonal_complement_orthoI')
then show ?thesis
apply (transfer fixing: X Y)
apply (subst projection_plus[symmetric])
by auto
qed
abbreviation proj :: "'a::chilbert_space ⇒ 'a ⇒⇩C⇩L 'a" where "proj ψ ≡ Proj (ccspan {ψ})"
lemma proj_0[simp]: ‹proj 0 = 0›
by transfer auto
lemma ccsubspace_supI_via_Proj:
fixes A B C::"'a::chilbert_space ccsubspace"
assumes a1: ‹Proj (- C) *⇩S A ≤ B›
shows "A ≤ B ⊔ C"
proof-
have x2: ‹x ∈ space_as_set B›
if "x ∈ closure ( (projection (orthogonal_complement (space_as_set C))) ` space_as_set A)" for x
using that
by (metis Proj.rep_eq cblinfun_image.rep_eq assms less_eq_ccsubspace.rep_eq subsetD
uminus_ccsubspace.rep_eq)
have q1: ‹x ∈ closure {ψ + φ |ψ φ. ψ ∈ space_as_set B ∧ φ ∈ space_as_set C}›
if ‹x ∈ space_as_set A›
for x
proof-
have p1: ‹closed_csubspace (space_as_set C)›
using space_as_set by auto
hence ‹x = (projection (space_as_set C)) x
+ (projection (orthogonal_complement (space_as_set C))) x›
by simp
hence ‹x = (projection (orthogonal_complement (space_as_set C))) x
+ (projection (space_as_set C)) x›
by (metis ordered_field_class.sign_simps(2))
moreover have ‹(projection (orthogonal_complement (space_as_set C))) x ∈ space_as_set B›
using x2
by (meson closure_subset image_subset_iff that)
moreover have ‹(projection (space_as_set C)) x ∈ space_as_set C›
by (metis mem_Collect_eq orthog_proj_exists projection_eqI space_as_set)
ultimately show ?thesis
using closure_subset by force
qed
have x1: ‹x ∈ (space_as_set B +⇩M space_as_set C)›
if "x ∈ space_as_set A" for x
proof -
have f1: "x ∈ closure {a + b |a b. a ∈ space_as_set B ∧ b ∈ space_as_set C}"
by (simp add: q1 that)
have "{a + b |a b. a ∈ space_as_set B ∧ b ∈ space_as_set C} = {a. ∃p. p ∈ space_as_set B
∧ (∃q. q ∈ space_as_set C ∧ a = p + q)}"
by blast
hence "x ∈ closure {a. ∃b∈space_as_set B. ∃c∈space_as_set C. a = b + c}"
using f1 by (simp add: Bex_def_raw)
thus ?thesis
using that
unfolding closed_sum_def set_plus_def
by blast
qed
hence ‹x ∈ space_as_set (Abs_ccsubspace (space_as_set B +⇩M space_as_set C))›
if "x ∈ space_as_set A" for x
using that
by (metis space_as_set_inverse sup_ccsubspace.rep_eq)
thus ?thesis
by (simp add: x1 less_eq_ccsubspace.rep_eq subset_eq sup_ccsubspace.rep_eq)
qed
lemma is_Proj_idempotent:
assumes "is_Proj P"
shows "P o⇩C⇩L P = P"
using assms apply transfer
using is_projection_on_fixes_image is_projection_on_in_image by fastforce
lemma is_proj_selfadj:
assumes "is_Proj P"
shows "P* = P"
using assms
unfolding is_Proj_def
by (metis is_Proj_algebraic is_Proj_def)
lemma is_Proj_I:
assumes "P o⇩C⇩L P = P" and "P* = P"
shows "is_Proj P"
using assms is_Proj_algebraic by metis
lemma is_Proj_0[simp]: "is_Proj 0"
apply transfer apply (rule exI[of _ 0])
by (simp add: is_projection_on_zero)
lemma is_Proj_complement[simp]:
fixes P :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes a1: "is_Proj P"
shows "is_Proj (id_cblinfun - P)"
by (smt (z3) add_diff_cancel_left add_diff_cancel_left' adj_cblinfun_compose adj_plus assms bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose diff_add_cancel id_cblinfun_adjoint is_Proj_algebraic cblinfun_compose_id_left)
lemma Proj_bot[simp]: "Proj bot = 0"
by (metis zero_cblinfun_image Proj_on_own_range' is_Proj_0 is_Proj_algebraic
zero_ccsubspace_def)
lemma Proj_ortho_compl:
"Proj (- X) = id_cblinfun - Proj X"
by (transfer, auto)
lemma Proj_inj:
assumes "Proj X = Proj Y"
shows "X = Y"
by (metis assms Proj_range)
lemma norm_Proj_leq1: ‹norm (Proj M) ≤ 1› for M :: ‹'a :: chilbert_space ccsubspace›
by transfer (metis (no_types, opaque_lifting) mult.left_neutral onorm_bound projection_reduces_norm zero_less_one_class.zero_le_one)
lemma Proj_orthog_ccspan_insert:
assumes "⋀y. y ∈ Y ⟹ is_orthogonal x y"
shows ‹Proj (ccspan (insert x Y)) = proj x + Proj (ccspan Y)›
apply (subst asm_rl[of ‹insert x Y = {x} ∪ Y›], simp)
apply (rule Proj_orthog_ccspan_union)
using assms by auto
lemma Proj_fixes_image: ‹Proj S *⇩V ψ = ψ› if ‹ψ ∈ space_as_set S›
by (metis Proj_idempotent Proj_range that cblinfun_fixes_range)
lemma norm_is_Proj: ‹norm P ≤ 1› if ‹is_Proj P› for P :: ‹'a :: chilbert_space ⇒⇩C⇩L 'a›
by (metis Proj_on_own_range norm_Proj_leq1 that)
lemma Proj_sup: ‹orthogonal_spaces S T ⟹ Proj (sup S T) = Proj S + Proj T›
unfolding orthogonal_spaces_def
by transfer (simp add: projection_plus)
lemma Proj_sum_spaces:
assumes ‹finite X›
assumes ‹⋀x y. x∈X ⟹ y∈X ⟹ x≠y ⟹ orthogonal_spaces (J x) (J y)›
shows ‹Proj (∑x∈X. J x) = (∑x∈X. Proj (J x))›
using assms
proof induction
case empty
show ?case
by auto
next
case (insert x F)
have ‹Proj (sum J (insert x F)) = Proj (J x ⊔ sum J F)›
by (simp add: insert)
also have ‹… = Proj (J x) + Proj (sum J F)›
apply (rule Proj_sup)
apply (rule orthogonal_sum)
using insert by auto
also have ‹… = (∑x∈insert x F. Proj (J x))›
by (simp add: insert.IH insert.hyps(1) insert.hyps(2) insert.prems)
finally show ?case
by -
qed
lemma is_Proj_reduces_norm:
fixes P :: ‹'a::complex_inner ⇒⇩C⇩L 'a›
assumes ‹is_Proj P›
shows ‹norm (P *⇩V ψ) ≤ norm ψ›
apply (rule is_projection_on_reduces_norm[where M=‹range P›])
using assms is_Proj.rep_eq is_projection_on_image by blast (simp add: Proj_range_closed assms closed_csubspace.intro)
lemma norm_Proj_apply: ‹norm (Proj T *⇩V ψ) = norm ψ ⟷ ψ ∈ space_as_set T›
proof (rule iffI)
show ‹norm (Proj T *⇩V ψ) = norm ψ› if ‹ψ ∈ space_as_set T›
by (simp add: Proj_fixes_image that)
assume assm: ‹norm (Proj T *⇩V ψ) = norm ψ›
have ψ_decomp: ‹ψ = Proj T ψ + Proj (-T) ψ›
by (simp add: Proj_ortho_compl cblinfun.real.diff_left)
have ‹(norm (Proj (-T) ψ))⇧2 = (norm (Proj T ψ))⇧2 + (norm (Proj (-T) ψ))⇧2 - (norm (Proj T ψ))⇧2›
by auto
also have ‹… = (norm (Proj T ψ + Proj (-T) ψ))⇧2 - (norm (Proj T ψ))⇧2›
apply (subst pythagorean_theorem)
apply (metis (no_types, lifting) Proj_idempotent ψ_decomp add_cancel_right_left adj_Proj cblinfun.real.add_right cblinfun_apply_cblinfun_compose cinner_adj_left cinner_zero_left)
by simp
also with ψ_decomp have ‹… = (norm ψ)⇧2 - (norm (Proj T ψ))⇧2›
by metis
also with assm have ‹… = 0›
by simp
finally have ‹norm (Proj (-T) ψ) = 0›
by auto
with ψ_decomp have ‹ψ = Proj T ψ›
by auto
then show ‹ψ ∈ space_as_set T›
by (metis Proj_range cblinfun_apply_in_image)
qed
lemma norm_Proj_apply_1: ‹norm ψ = 1 ⟹ norm (Proj T *⇩V ψ) = 1 ⟷ ψ ∈ space_as_set T›
using norm_Proj_apply by metis
lemma norm_is_Proj_nonzero: ‹norm P = 1› if ‹is_Proj P› and ‹P ≠ 0› for P :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
proof (rule antisym)
show ‹norm P ≤ 1›
by (simp add: norm_is_Proj that(1))
from ‹P ≠ 0›
have ‹range P ≠ 0›
by (metis cblinfun_eq_0_on_UNIV_span complex_vector.span_UNIV rangeI set_zero singletonD)
then obtain ψ where ‹ψ ∈ range P› and ‹ψ ≠ 0›
by force
then have ‹P ψ = ψ›
using is_Proj.rep_eq is_projection_on_fixes_image is_projection_on_image that(1) by blast
then show ‹norm P ≥ 1›
apply (rule_tac cblinfun_norm_geqI[of _ _ ψ])
using ‹ψ ≠ 0› by simp
qed
lemma Proj_compose_cancelI:
assumes ‹A *⇩S ⊤ ≤ S›
shows ‹Proj S o⇩C⇩L A = A›
apply (rule cblinfun_eqI)
proof -
fix x
have ‹(Proj S o⇩C⇩L A) *⇩V x = Proj S *⇩V (A *⇩V x)›
by simp
also have ‹… = A *⇩V x›
apply (rule Proj_fixes_image)
using assms cblinfun_apply_in_image less_eq_ccsubspace.rep_eq by blast
finally show ‹(Proj S o⇩C⇩L A) *⇩V x = A *⇩V x›
by -
qed
lemma space_as_setI_via_Proj:
assumes ‹Proj M *⇩V x = x›
shows ‹x ∈ space_as_set M›
using assms norm_Proj_apply by fastforce
lemma unitary_image_ortho_compl:
fixes U :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes [simp]: ‹unitary U›
shows ‹U *⇩S (- A) = - (U *⇩S A)›
proof -
have ‹Proj (U *⇩S (- A)) = sandwich U (Proj (- A))›
by (simp add: Proj_sandwich)
also have ‹… = sandwich U (id_cblinfun - Proj A)›
by (simp add: Proj_ortho_compl)
also have ‹… = id_cblinfun - sandwich U (Proj A)›
by (metis assms cblinfun.diff_right sandwich_isometry_id unitary_twosided_isometry)
also have ‹… = id_cblinfun - Proj (U *⇩S A)›
by (simp add: Proj_sandwich)
also have ‹… = Proj (- (U *⇩S A))›
by (simp add: Proj_ortho_compl)
finally show ?thesis
by (simp add: Proj_inj)
qed
lemma Proj_on_image [simp]: ‹Proj S *⇩S S = S›
by (metis Proj_idempotent Proj_range cblinfun_compose_image)
subsection ‹Kernel / eigenspaces›
lift_definition kernel :: "'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector
⇒ 'a ccsubspace"
is "λf. f -` {0}"
by (metis kernel_is_closed_csubspace)
definition eigenspace :: "complex ⇒ 'a::complex_normed_vector ⇒⇩C⇩L'a ⇒ 'a ccsubspace" where
"eigenspace a A = kernel (A - a *⇩C id_cblinfun)"
lemma kernel_scaleC[simp]: "a≠0 ⟹ kernel (a *⇩C A) = kernel A"
for a :: complex and A :: "(_,_) cblinfun"
apply transfer
using complex_vector.scale_eq_0_iff by blast
lemma kernel_0[simp]: "kernel 0 = top"
by transfer auto
lemma kernel_id[simp]: "kernel id_cblinfun = 0"
by transfer simp
lemma eigenspace_scaleC[simp]:
assumes a1: "a ≠ 0"
shows "eigenspace b (a *⇩C A) = eigenspace (b/a) A"
proof -
have "b *⇩C (id_cblinfun::('a, _) cblinfun) = a *⇩C (b / a) *⇩C id_cblinfun"
using a1
by (metis ceq_vector_fraction_iff)
hence "kernel (a *⇩C A - b *⇩C id_cblinfun) = kernel (A - (b / a) *⇩C id_cblinfun)"
using a1 by (metis (no_types) complex_vector.scale_right_diff_distrib kernel_scaleC)
thus ?thesis
unfolding eigenspace_def
by blast
qed
lemma eigenspace_memberD:
assumes "x ∈ space_as_set (eigenspace e A)"
shows "A *⇩V x = e *⇩C x"
using assms unfolding eigenspace_def by transfer auto
lemma kernel_memberD:
assumes "x ∈ space_as_set (kernel A)"
shows "A *⇩V x = 0"
using assms by transfer auto
lemma eigenspace_memberI:
assumes "A *⇩V x = e *⇩C x"
shows "x ∈ space_as_set (eigenspace e A)"
using assms unfolding eigenspace_def by transfer auto
lemma kernel_memberI:
assumes "A *⇩V x = 0"
shows "x ∈ space_as_set (kernel A)"
using assms by transfer auto
lemma kernel_Proj[simp]: ‹kernel (Proj S) = - S›
apply transfer
apply auto
apply (metis diff_0_right is_projection_on_iff_orthog projection_is_projection_on')
by (simp add: complex_vector.subspace_0 projection_eqI)
lemma orthogonal_projectors_orthogonal_spaces:
fixes S T :: ‹'a::chilbert_space ccsubspace›
shows ‹orthogonal_spaces S T ⟷ Proj S o⇩C⇩L Proj T = 0›
proof (intro ballI iffI)
assume ‹Proj S o⇩C⇩L Proj T = 0›
then have ‹is_orthogonal x y› if ‹x ∈ space_as_set S› ‹y ∈ space_as_set T› for x y
by (metis (no_types, opaque_lifting) Proj_fixes_image adj_Proj cblinfun.zero_left cblinfun_apply_cblinfun_compose cinner_adj_right cinner_zero_right that(1) that(2))
then show ‹orthogonal_spaces S T›
by (simp add: orthogonal_spaces_def)
next
assume ‹orthogonal_spaces S T›
then have ‹S ≤ - T›
by (simp add: orthogonal_spaces_leq_compl)
then show ‹Proj S o⇩C⇩L Proj T = 0›
by (metis (no_types, opaque_lifting) Proj_range adj_Proj adj_cblinfun_compose basic_trans_rules(31) cblinfun.zero_left cblinfun_apply_cblinfun_compose cblinfun_apply_in_image cblinfun_eqI kernel_Proj kernel_memberD less_eq_ccsubspace.rep_eq)
qed
lemma cblinfun_compose_Proj_kernel[simp]: ‹a o⇩C⇩L Proj (kernel a) = 0›
apply (rule cblinfun_eqI)
by simp (metis Proj_range cblinfun_apply_in_image kernel_memberD)
lemma kernel_compl_adj_range:
shows ‹kernel a = - (a* *⇩S top)›
proof (rule ccsubspace_eqI)
fix x
have ‹x ∈ space_as_set (kernel a) ⟷ a x = 0›
by transfer simp
also have ‹a x = 0 ⟷ (∀y. is_orthogonal y (a x))›
by (metis cinner_gt_zero_iff cinner_zero_right)
also have ‹… ⟷ (∀y. is_orthogonal (a* *⇩V y) x)›
by (simp add: cinner_adj_left)
also have ‹… ⟷ x ∈ space_as_set (- (a* *⇩S top))›
by transfer (metis (mono_tags, opaque_lifting) UNIV_I image_iff is_orthogonal_sym orthogonal_complementI orthogonal_complement_of_closure orthogonal_complement_orthoI')
finally show ‹x ∈ space_as_set (kernel a) ⟷ x ∈ space_as_set (- (a* *⇩S top))›
by -
qed
lemma kernel_apply_self: ‹A *⇩S kernel A = 0›
proof transfer
fix A :: ‹'b ⇒ 'a›
assume ‹bounded_clinear A›
then have ‹A 0 = 0›
by (simp add: bounded_clinear_def complex_vector.linear_0)
then have ‹A ` A -` {0} = {0}›
by fastforce
then show ‹closure (A ` A -` {0}) = {0}›
by auto
qed
lemma leq_kernel_iff:
shows ‹A ≤ kernel B ⟷ B *⇩S A = 0›
proof (rule iffI)
assume ‹A ≤ kernel B›
then have ‹B *⇩S A ≤ B *⇩S kernel B›
by (simp add: cblinfun_image_mono)
also have ‹… = 0›
by (simp add: kernel_apply_self)
finally show ‹B *⇩S A = 0›
by (simp add: bot.extremum_unique)
next
assume ‹B *⇩S A = 0›
then show ‹A ≤ kernel B›
apply transfer
by (metis closure_subset image_subset_iff_subset_vimage)
qed
lemma cblinfun_image_kernel:
assumes ‹C *⇩S A *⇩S kernel B ≤ kernel B›
assumes ‹A o⇩C⇩L C = id_cblinfun›
shows ‹A *⇩S kernel B = kernel (B o⇩C⇩L C)›
proof (rule antisym)
show ‹A *⇩S kernel B ≤ kernel (B o⇩C⇩L C)›
using assms(1) by (simp add: leq_kernel_iff cblinfun_compose_image)
show ‹kernel (B o⇩C⇩L C) ≤ A *⇩S kernel B›
proof (insert assms(2), transfer, intro subsetI)
fix A :: ‹'a ⇒ 'b› and B :: ‹'a ⇒ 'c› and C :: ‹'b ⇒ 'a› and x
assume ‹x ∈ (B ∘ C) -` {0}›
then have BCx: ‹B (C x) = 0›
by simp
assume ‹A ∘ C = (λx. x)›
then have ‹x = A (C x)›
apply (simp add: o_def)
by metis
then show ‹x ∈ closure (A ` B -` {0})›
using ‹B (C x) = 0› closure_subset by fastforce
qed
qed
lemma cblinfun_image_kernel_unitary:
assumes ‹unitary U›
shows ‹U *⇩S kernel B = kernel (B o⇩C⇩L U*)›
apply (rule cblinfun_image_kernel)
using assms by (auto simp flip: cblinfun_compose_image)
lemma kernel_cblinfun_compose:
assumes ‹kernel B = 0›
shows ‹kernel A = kernel (B o⇩C⇩L A)›
using assms apply transfer by auto
lemma eigenspace_0[simp]: ‹eigenspace 0 A = kernel A›
by (simp add: eigenspace_def)
lemma kernel_isometry: ‹kernel U = 0› if ‹isometry U›
by (simp add: kernel_compl_adj_range range_adjoint_isometry that)
lemma cblinfun_image_eigenspace_isometry:
assumes [simp]: ‹isometry A› and ‹c ≠ 0›
shows ‹A *⇩S eigenspace c B = eigenspace c (sandwich A B)›
proof (rule antisym)
show ‹A *⇩S eigenspace c B ≤ eigenspace c (sandwich A B)›
proof (unfold cblinfun_image_def2, rule ccspan_leqI, rule subsetI)
fix x assume ‹x ∈ (*⇩V) A ` space_as_set (eigenspace c B)›
then obtain y where x_def: ‹x = A y› and ‹y ∈ space_as_set (eigenspace c B)›
by auto
then have ‹B y = c *⇩C y›
by (simp add: eigenspace_memberD)
then have ‹sandwich A B x = c *⇩C x›
apply (simp add: sandwich_apply x_def cblinfun_compose_assoc
flip: cblinfun_apply_cblinfun_compose)
by (simp add: cblinfun.scaleC_right)
then show ‹x ∈ space_as_set (eigenspace c (sandwich A B))›
by (simp add: eigenspace_memberI)
qed
show ‹eigenspace c (sandwich A *⇩V B) ≤ A *⇩S eigenspace c B›
proof (rule ccsubspace_leI_unit)
fix x
assume ‹x ∈ space_as_set (eigenspace c (sandwich A B))›
then have *: ‹sandwich A B x = c *⇩C x›
by (simp add: eigenspace_memberD)
then have ‹c *⇩C x ∈ range A›
apply (simp add: sandwich_apply)
by (metis rangeI)
then have ‹(inverse c * c) *⇩C x ∈ range A›
apply (simp flip: scaleC_scaleC)
by (metis (no_types, lifting) cblinfun.scaleC_right rangeE rangeI)
with ‹c ≠ 0› have ‹x ∈ range A›
by simp
then obtain y where x_def: ‹x = A y›
by auto
have ‹B *⇩V y = A* *⇩V sandwich A B x›
apply (simp add: sandwich_apply x_def)
by (metis assms cblinfun_apply_cblinfun_compose id_cblinfun.rep_eq isometryD)
also have ‹… = c *⇩C y›
apply (simp add: * cblinfun.scaleC_right)
apply (simp add: x_def)
by (metis assms(1) cblinfun_apply_cblinfun_compose id_cblinfun_apply isometry_def)
finally have ‹y ∈ space_as_set (eigenspace c B)›
by (simp add: eigenspace_memberI)
then show ‹x ∈ space_as_set (A *⇩S eigenspace c B) ›
by (simp add: x_def cblinfun_apply_in_image')
qed
qed
lemma cblinfun_image_eigenspace_unitary:
assumes [simp]: ‹unitary A›
shows ‹A *⇩S eigenspace c B = eigenspace c (sandwich A B)›
apply (cases ‹c = 0›)
apply (simp add: sandwich_apply cblinfun_image_kernel_unitary kernel_isometry cblinfun_compose_assoc
flip: kernel_cblinfun_compose)
by (simp add: cblinfun_image_eigenspace_isometry)
lemma kernel_member_iff: ‹x ∈ space_as_set (kernel A) ⟷ A *⇩V x = 0›
using kernel_memberD kernel_memberI by blast
lemma kernel_square[simp]: ‹kernel (A* o⇩C⇩L A) = kernel A›
proof (intro ccsubspace_eqI iffI)
fix x
assume ‹x ∈ space_as_set (kernel A)›
then show ‹x ∈ space_as_set (kernel (A* o⇩C⇩L A))›
by (simp add: kernel.rep_eq)
next
fix x
assume ‹x ∈ space_as_set (kernel (A* o⇩C⇩L A))›
then have ‹A* *⇩V A *⇩V x = 0›
by (simp add: kernel.rep_eq)
then have ‹(A *⇩V x) ∙⇩C (A *⇩V x) = 0›
by (metis cinner_adj_right cinner_zero_right)
then have ‹A *⇩V x = 0›
by auto
then show ‹x ∈ space_as_set (kernel A)›
by (simp add: kernel.rep_eq)
qed
subsection ‹Partial isometries›
definition partial_isometry where
‹partial_isometry A ⟷ (∀h ∈ space_as_set (- kernel A). norm (A h) = norm h)›
lemma partial_isometryI:
assumes ‹⋀h. h ∈ space_as_set (- kernel A) ⟹ norm (A h) = norm h›
shows ‹partial_isometry A›
using assms partial_isometry_def by blast
lemma
fixes A :: ‹'a :: chilbert_space ⇒⇩C⇩L 'b :: complex_normed_vector›
assumes iso: ‹⋀ψ. ψ ∈ space_as_set V ⟹ norm (A *⇩V ψ) = norm ψ›
assumes zero: ‹⋀ψ. ψ ∈ space_as_set (- V) ⟹ A *⇩V ψ = 0›
shows partial_isometryI': ‹partial_isometry A›
and partial_isometry_initial: ‹kernel A = - V›
proof -
from zero
have ‹- V ≤ kernel A›
by (simp add: kernel_memberI less_eq_ccsubspace.rep_eq subsetI)
moreover have ‹kernel A ≤ -V›
by (smt (verit, ccfv_threshold) Proj_ortho_compl Proj_range assms(1) cblinfun.diff_left cblinfun.diff_right cblinfun_apply_in_image cblinfun_id_cblinfun_apply ccsubspace_leI kernel_Proj kernel_memberD kernel_memberI norm_eq_zero ortho_involution subsetI zero)
ultimately show kerA: ‹kernel A = -V›
by simp
show ‹partial_isometry A›
apply (rule partial_isometryI)
by (simp add: kerA iso)
qed
lemma Proj_partial_isometry[simp]: ‹partial_isometry (Proj S)›
apply (rule partial_isometryI)
by (simp add: Proj_fixes_image)
lemma is_Proj_partial_isometry: ‹is_Proj P ⟹ partial_isometry P› for P :: ‹_ :: chilbert_space ⇒⇩C⇩L _›
by (metis Proj_on_own_range Proj_partial_isometry)
lemma isometry_partial_isometry: ‹isometry P ⟹ partial_isometry P›
by (simp add: isometry_preserves_norm partial_isometry_def)
lemma unitary_partial_isometry: ‹unitary P ⟹ partial_isometry P›
using isometry_partial_isometry unitary_isometry by blast
lemma norm_partial_isometry:
fixes A :: ‹'a :: chilbert_space ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹partial_isometry A› and ‹A ≠ 0›
shows ‹norm A = 1›
proof -
from ‹A ≠ 0›
have ‹- (kernel A) ≠ 0›
by (metis cblinfun_eqI diff_zero id_cblinfun_apply kernel_id kernel_memberD ortho_involution orthog_proj_exists orthogonal_complement_closed_subspace uminus_ccsubspace.rep_eq zero_cblinfun.rep_eq)
then obtain h where ‹h ∈ space_as_set (- kernel A)› and ‹h ≠ 0›
by (metis cblinfun_id_cblinfun_apply ccsubspace_eqI closed_csubspace.subspace complex_vector.subspace_0 kernel_id kernel_memberD kernel_memberI orthogonal_complement_closed_subspace uminus_ccsubspace.rep_eq)
with ‹partial_isometry A›
have ‹norm (A h) = norm h›
using partial_isometry_def by blast
then have ‹norm A ≥ 1›
by (smt (verit) ‹h ≠ 0› mult_cancel_right1 mult_left_le_one_le norm_cblinfun norm_eq_zero norm_ge_zero)
have ‹norm A ≤ 1›
proof (rule norm_cblinfun_bound)
show ‹0 ≤ (1::real)›
by simp
fix ψ :: 'a
define g h where ‹g = Proj (kernel A) ψ› and ‹h = Proj (- kernel A) ψ›
have ‹A g = 0›
by (metis Proj_range cblinfun_apply_in_image g_def kernel_memberD)
moreover from ‹partial_isometry A›
have ‹norm (A h) = norm h›
by (metis Proj_range cblinfun_apply_in_image h_def partial_isometry_def)
ultimately have ‹norm (A ψ) = norm h›
by (simp add: Proj_ortho_compl cblinfun.diff_left cblinfun.diff_right g_def h_def)
also have ‹norm h ≤ norm ψ›
by (smt (verit, del_insts) h_def mult_left_le_one_le norm_Proj_leq1 norm_cblinfun norm_ge_zero)
finally show ‹norm (A *⇩V ψ) ≤ 1 * norm ψ›
by simp
qed
from ‹norm A ≤ 1› and ‹norm A ≥ 1›
show ‹norm A = 1›
by auto
qed
lemma partial_isometry_adj_a_o_a:
assumes ‹partial_isometry a›
shows ‹a* o⇩C⇩L a = Proj (- kernel a)›
proof (rule cblinfun_cinner_eqI)
define P where ‹P = Proj (- kernel a)›
have aP: ‹a o⇩C⇩L P = a›
by (auto intro!: simp: cblinfun_compose_minus_right P_def Proj_ortho_compl)
have is_Proj_P[simp]: ‹is_Proj P›
by (simp add: P_def)
fix ψ :: 'a
have ‹ψ ∙⇩C ((a* o⇩C⇩L a) *⇩V ψ) = a ψ ∙⇩C a ψ›
by (simp add: cinner_adj_right)
also have ‹… = a (P ψ) ∙⇩C a (P ψ)›
by (metis aP cblinfun_apply_cblinfun_compose)
also have ‹… = P ψ ∙⇩C P ψ›
by (metis P_def Proj_range assms cblinfun_apply_in_image cdot_square_norm partial_isometry_def)
also have ‹… = ψ ∙⇩C P ψ›
by (simp flip: cinner_adj_right add: is_proj_selfadj is_Proj_idempotent[THEN simp_a_oCL_b'])
finally show ‹ψ ∙⇩C ((a* o⇩C⇩L a) *⇩V ψ) = ψ ∙⇩C P ψ›
by -
qed
lemma partial_isometry_square_proj: ‹is_Proj (a* o⇩C⇩L a)› if ‹partial_isometry a›
by (simp add: partial_isometry_adj_a_o_a that)
lemma partial_isometry_adj[simp]: ‹partial_isometry (a*)› if ‹partial_isometry a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof -
have ran_ker: ‹a *⇩S top = - kernel (a*)›
by (simp add: kernel_compl_adj_range)
have ‹norm (a* *⇩V h) = norm h› if ‹h ∈ range a› for h
proof -
from that obtain x where h: ‹h = a x›
by auto
have ‹norm (a* *⇩V h) = norm (a* *⇩V a *⇩V x)›
by (simp add: h)
also have ‹… = norm (Proj (- kernel a) *⇩V x)›
by (simp add: ‹partial_isometry a› partial_isometry_adj_a_o_a simp_a_oCL_b')
also have ‹… = norm (a *⇩V Proj (- kernel a) *⇩V x)›
by (metis Proj_range ‹partial_isometry a› cblinfun_apply_in_image partial_isometry_def)
also have ‹… = norm (a *⇩V x)›
by (smt (verit, best) Proj_idempotent ‹partial_isometry a› adj_Proj cblinfun_apply_cblinfun_compose cinner_adj_right cnorm_eq partial_isometry_adj_a_o_a)
also have ‹… = norm h›
using h by auto
finally show ?thesis
by -
qed
then have norm_pres: ‹norm (a* *⇩V h) = norm h› if ‹h ∈ closure (range a)› for h
using that apply (rule on_closure_eqI)
by assumption (intro continuous_intros)+
show ?thesis
apply (rule partial_isometryI)
by (auto simp: cblinfun_image.rep_eq norm_pres simp flip: ran_ker)
qed
subsection ‹Isomorphisms and inverses›
definition iso_cblinfun :: ‹('a::complex_normed_vector, 'b::complex_normed_vector) cblinfun ⇒ bool› where
‹iso_cblinfun A = (∃ B. A o⇩C⇩L B = id_cblinfun ∧ B o⇩C⇩L A = id_cblinfun)›
definition ‹invertible_cblinfun A ⟷ (∃B. B o⇩C⇩L A = id_cblinfun)›
definition cblinfun_inv :: ‹('a::complex_normed_vector, 'b::complex_normed_vector) cblinfun ⇒ ('b,'a) cblinfun› where
‹cblinfun_inv A = (if invertible_cblinfun A then SOME B. B o⇩C⇩L A = id_cblinfun else 0)›
lemma cblinfun_inv_left:
assumes ‹invertible_cblinfun A›
shows ‹cblinfun_inv A o⇩C⇩L A = id_cblinfun›
apply (simp add: assms cblinfun_inv_def)
apply (rule someI_ex)
using assms by (simp add: invertible_cblinfun_def)
lemma inv_cblinfun_invertible: ‹iso_cblinfun A ⟹ invertible_cblinfun A›
by (auto simp: iso_cblinfun_def invertible_cblinfun_def)
lemma cblinfun_inv_right:
assumes ‹iso_cblinfun A›
shows ‹A o⇩C⇩L cblinfun_inv A = id_cblinfun›
proof -
from assms
obtain B where AB: ‹A o⇩C⇩L B = id_cblinfun› and BA: ‹B o⇩C⇩L A = id_cblinfun›
using iso_cblinfun_def by blast
from BA have ‹cblinfun_inv A o⇩C⇩L A = id_cblinfun›
by (simp add: assms cblinfun_inv_left inv_cblinfun_invertible)
with AB BA have ‹cblinfun_inv A = B›
by (metis cblinfun_assoc_left(1) cblinfun_compose_id_right)
with AB show ‹A o⇩C⇩L cblinfun_inv A = id_cblinfun›
by auto
qed
lemma cblinfun_inv_uniq:
assumes "A o⇩C⇩L B = id_cblinfun" and "B o⇩C⇩L A = id_cblinfun"
shows "cblinfun_inv A = B"
using assms by (metis inv_cblinfun_invertible cblinfun_compose_assoc cblinfun_compose_id_right cblinfun_inv_left iso_cblinfun_def)
lemma iso_cblinfun_unitary: ‹unitary A ⟹ iso_cblinfun A›
using iso_cblinfun_def unitary_def by blast
lemma invertible_cblinfun_isometry: ‹isometry A ⟹ invertible_cblinfun A›
using invertible_cblinfun_def isometryD by blast
lemma summable_cblinfun_apply_invertible:
assumes ‹invertible_cblinfun A›
shows ‹(λx. A *⇩V g x) summable_on S ⟷ g summable_on S›
proof (rule iffI)
assume ‹g summable_on S›
then show ‹(λx. A *⇩V g x) summable_on S›
by (rule summable_on_cblinfun_apply)
next
assume ‹(λx. A *⇩V g x) summable_on S›
then have ‹(λx. cblinfun_inv A *⇩V A *⇩V g x) summable_on S›
by (rule summable_on_cblinfun_apply)
then show ‹g summable_on S›
by (simp add: cblinfun_inv_left assms flip: cblinfun_apply_cblinfun_compose)
qed
lemma infsum_cblinfun_apply_invertible:
assumes ‹invertible_cblinfun A›
shows ‹(∑⇩∞x∈S. A *⇩V g x) = A *⇩V (∑⇩∞x∈S. g x)›
proof (cases ‹g summable_on S›)
case True
then show ?thesis
by (rule infsum_cblinfun_apply)
next
case False
then have ‹¬ (λx. A *⇩V g x) summable_on S›
using assms by (simp add: summable_cblinfun_apply_invertible)
with False show ?thesis
by (simp add: infsum_not_exists)
qed
subsection ‹One-dimensional spaces›
instantiation cblinfun :: (one_dim, one_dim) complex_inner begin
text ‹Once we have a theory for the trace, we could instead define the Hilbert-Schmidt inner product
and relax the \<^class>‹one_dim›-sort constraint to (\<^class>‹cfinite_dim›,\<^class>‹complex_normed_vector›) or similar›
definition "cinner_cblinfun (A::'a ⇒⇩C⇩L 'b) (B::'a ⇒⇩C⇩L 'b)
= cnj (one_dim_iso (A *⇩V 1)) * one_dim_iso (B *⇩V 1)"
instance
proof intro_classes
fix A B C :: "'a ⇒⇩C⇩L 'b"
and c c' :: complex
show "(A ∙⇩C B) = cnj (B ∙⇩C A)"
unfolding cinner_cblinfun_def by auto
show "(A + B) ∙⇩C C = (A ∙⇩C C) + (B ∙⇩C C)"
by (simp add: cinner_cblinfun_def algebra_simps plus_cblinfun.rep_eq)
show "(c *⇩C A ∙⇩C B) = cnj c * (A ∙⇩C B)"
by (simp add: cblinfun.scaleC_left cinner_cblinfun_def)
show "0 ≤ (A ∙⇩C A)"
unfolding cinner_cblinfun_def by auto
have "bounded_clinear A ⟹ A 1 = 0 ⟹ A = (λ_. 0)"
for A::"'a ⇒ 'b"
proof (rule one_dim_clinear_eqI [where x = 1] , auto)
show "clinear A"
if "bounded_clinear A"
and "A 1 = 0"
for A :: "'a ⇒ 'b"
using that
by (simp add: bounded_clinear.clinear)
show "clinear ((λ_. 0)::'a ⇒ 'b)"
if "bounded_clinear A"
and "A 1 = 0"
for A :: "'a ⇒ 'b"
using that
by (simp add: complex_vector.module_hom_zero)
qed
hence "A *⇩V 1 = 0 ⟹ A = 0"
by transfer
hence "one_dim_iso (A *⇩V 1) = 0 ⟹ A = 0"
by (metis one_dim_iso_of_zero one_dim_iso_inj)
thus "((A ∙⇩C A) = 0) = (A = 0)"
by (auto simp: cinner_cblinfun_def)
show "norm A = sqrt (cmod (A ∙⇩C A))"
unfolding cinner_cblinfun_def
by transfer (simp add: norm_mult abs_complex_def one_dim_onorm' cnj_x_x power2_eq_square bounded_clinear.clinear)
qed
end
instantiation cblinfun :: (one_dim, one_dim) one_dim begin
lift_definition one_cblinfun :: "'a ⇒⇩C⇩L 'b" is "one_dim_iso"
by (rule bounded_clinear_one_dim_iso)
lift_definition times_cblinfun :: "'a ⇒⇩C⇩L 'b ⇒ 'a ⇒⇩C⇩L 'b ⇒ 'a ⇒⇩C⇩L 'b"
is "λf g. f o one_dim_iso o g"
by (simp add: comp_bounded_clinear)
lift_definition inverse_cblinfun :: "'a ⇒⇩C⇩L 'b ⇒ 'a ⇒⇩C⇩L 'b" is
"λf. ((*) (one_dim_iso (inverse (f 1)))) o one_dim_iso"
by (auto intro!: comp_bounded_clinear bounded_clinear_mult_right)
definition divide_cblinfun :: "'a ⇒⇩C⇩L 'b ⇒ 'a ⇒⇩C⇩L 'b ⇒ 'a ⇒⇩C⇩L 'b" where
"divide_cblinfun A B = A * inverse B"
definition "canonical_basis_cblinfun = [1 :: 'a ⇒⇩C⇩L 'b]"
definition ‹canonical_basis_length_cblinfun (_ :: ('a ⇒⇩C⇩L 'b) itself) = (1::nat)›
instance
proof intro_classes
let ?basis = "canonical_basis :: ('a ⇒⇩C⇩L 'b) list"
fix A B C :: "'a ⇒⇩C⇩L 'b"
and c c' :: complex
show "distinct ?basis"
unfolding canonical_basis_cblinfun_def by simp
have "(1::'a ⇒⇩C⇩L 'b) ≠ (0::'a ⇒⇩C⇩L 'b)"
by (metis cblinfun.zero_left one_cblinfun.rep_eq one_dim_iso_of_one zero_neq_one)
thus "cindependent (set ?basis)"
unfolding canonical_basis_cblinfun_def by simp
have "A ∈ cspan (set ?basis)" for A
proof -
define c :: complex where "c = one_dim_iso (A *⇩V 1)"
have "A x = one_dim_iso (A 1) *⇩C one_dim_iso x" for x
by (smt (z3) cblinfun.scaleC_right complex_vector.scale_left_commute one_dim_iso_idem one_dim_scaleC_1)
hence "A = one_dim_iso (A *⇩V 1) *⇩C 1"
by transfer metis
thus "A ∈ cspan (set ?basis)"
unfolding canonical_basis_cblinfun_def
by (smt complex_vector.span_base complex_vector.span_scale list.set_intros(1))
qed
thus "cspan (set ?basis) = UNIV" by auto
have "A = (1::'a ⇒⇩C⇩L 'b) ⟹
norm (1::'a ⇒⇩C⇩L 'b) = (1::real)"
by transfer simp
thus "A ∈ set ?basis ⟹ norm A = 1"
unfolding canonical_basis_cblinfun_def
by simp
show "?basis = [1]"
unfolding canonical_basis_cblinfun_def by simp
show "c *⇩C 1 * c' *⇩C 1 = (c * c') *⇩C (1::'a⇒⇩C⇩L'b)"
by transfer auto
have "(1::'a ⇒⇩C⇩L 'b) = (0::'a ⇒⇩C⇩L 'b) ⟹ False"
by (metis cblinfun.zero_left one_cblinfun.rep_eq one_dim_iso_of_zero' zero_neq_neg_one)
thus "is_ortho_set (set ?basis)"
unfolding is_ortho_set_def canonical_basis_cblinfun_def by auto
show "A div B = A * inverse B"
by (simp add: divide_cblinfun_def)
show "inverse (c *⇩C 1) = (1::'a⇒⇩C⇩L'b) /⇩C c"
by transfer (simp add: o_def one_dim_inverse)
show ‹canonical_basis_length TYPE('a ⇒⇩C⇩L 'b) = length (canonical_basis :: ('a ⇒⇩C⇩L 'b) list)›
by (simp add: canonical_basis_length_cblinfun_def canonical_basis_cblinfun_def)
qed
end
lemma id_cblinfun_eq_1[simp]: ‹id_cblinfun = 1›
by transfer auto
lemma one_dim_cblinfun_compose_is_times[simp]:
fixes A :: "'a::one_dim ⇒⇩C⇩L 'a" and B :: "'a ⇒⇩C⇩L 'a"
shows "A o⇩C⇩L B = A * B"
by transfer simp
lemma scaleC_one_dim_is_times: ‹r *⇩C x = one_dim_iso r * x›
by simp
lemma one_comp_one_cblinfun[simp]: "1 o⇩C⇩L 1 = 1"
apply transfer unfolding o_def by simp
lemma one_cblinfun_adj[simp]: "1* = 1"
by transfer simp
lemma scaleC_1_apply[simp]: ‹(x *⇩C 1) *⇩V y = x *⇩C y›
by (metis cblinfun.scaleC_left cblinfun_id_cblinfun_apply id_cblinfun_eq_1)
lemma cblinfun_apply_1_left[simp]: ‹1 *⇩V y = y›
by (metis cblinfun_id_cblinfun_apply id_cblinfun_eq_1)
lemma of_complex_cblinfun_apply[simp]: ‹of_complex x *⇩V y = one_dim_iso (x *⇩C y)›
by (metis of_complex_def cblinfun.scaleC_right one_cblinfun.rep_eq scaleC_cblinfun.rep_eq)
lemma cblinfun_compose_1_left[simp]: ‹1 o⇩C⇩L x = x›
by transfer auto
lemma cblinfun_compose_1_right[simp]: ‹x o⇩C⇩L 1 = x›
by transfer auto
lemma one_dim_iso_id_cblinfun: ‹one_dim_iso id_cblinfun = id_cblinfun›
by simp
lemma one_dim_iso_id_cblinfun_eq_1: ‹one_dim_iso id_cblinfun = 1›
by simp
lemma one_dim_iso_comp_distr[simp]: ‹one_dim_iso (a o⇩C⇩L b) = one_dim_iso a o⇩C⇩L one_dim_iso b›
by (smt (z3) cblinfun_compose_scaleC_left cblinfun_compose_scaleC_right one_cinner_a_scaleC_one one_comp_one_cblinfun one_dim_iso_of_one one_dim_iso_scaleC)
lemma one_dim_iso_comp_distr_times[simp]: ‹one_dim_iso (a o⇩C⇩L b) = one_dim_iso a * one_dim_iso b›
by (smt (verit, del_insts) mult.left_neutral mult_scaleC_left one_cinner_a_scaleC_one one_comp_one_cblinfun one_dim_iso_of_one one_dim_iso_scaleC cblinfun_compose_scaleC_right cblinfun_compose_scaleC_left)
lemma one_dim_iso_adjoint[simp]: ‹one_dim_iso (A*) = (one_dim_iso A)*›
by (smt (z3) one_cblinfun_adj one_cinner_a_scaleC_one one_dim_iso_of_one one_dim_iso_scaleC scaleC_adj)
lemma one_dim_iso_adjoint_complex[simp]: ‹one_dim_iso (A*) = cnj (one_dim_iso A)›
by (metis (mono_tags, lifting) one_cblinfun_adj one_dim_iso_idem one_dim_scaleC_1 scaleC_adj)
lemma one_dim_cblinfun_compose_commute: ‹a o⇩C⇩L b = b o⇩C⇩L a› for a b :: ‹('a::one_dim,'a) cblinfun›
by (simp add: one_dim_iso_inj)
lemma one_cblinfun_apply_one[simp]: ‹1 *⇩V 1 = 1›
by (simp add: one_cblinfun.rep_eq)
lemma one_dim_cblinfun_apply_is_times:
fixes A :: "'a::one_dim ⇒⇩C⇩L 'b::one_dim" and b :: "'a"
shows "A *⇩V b = one_dim_iso A * one_dim_iso b"
apply (subst one_dim_scaleC_1[of A, symmetric])
apply (subst one_dim_scaleC_1[of b, symmetric])
apply (simp only: cblinfun.scaleC_left cblinfun.scaleC_right)
by simp
lemma is_onb_one_dim[simp]: ‹norm x = 1 ⟹ is_onb {x}› for x :: ‹_ :: one_dim›
by (auto simp: is_onb_def intro!: ccspan_one_dim)
lemma one_dim_iso_cblinfun_comp: ‹one_dim_iso (a o⇩C⇩L b) = of_complex (cinner (a* *⇩V 1) (b *⇩V 1))›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::one_dim› and b :: ‹'c::one_dim ⇒⇩C⇩L 'a›
by (simp add: cinner_adj_left cinner_cblinfun_def one_dim_iso_def)
lemma one_dim_iso_cblinfun_apply[simp]: ‹one_dim_iso ψ *⇩V φ = one_dim_iso (one_dim_iso ψ *⇩C φ)›
by (smt (verit) cblinfun.scaleC_left one_cblinfun.rep_eq one_dim_iso_of_one one_dim_iso_scaleC one_dim_scaleC_1)
subsection ‹Loewner order›
lift_definition heterogenous_cblinfun_id :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
is ‹if bounded_clinear (heterogenous_identity :: 'a::complex_normed_vector ⇒ 'b::complex_normed_vector) then heterogenous_identity else (λ_. 0)›
by auto
lemma heterogenous_cblinfun_id_def'[simp]: "heterogenous_cblinfun_id = id_cblinfun"
by transfer auto
definition "heterogenous_same_type_cblinfun (x::'a::chilbert_space itself) (y::'b::chilbert_space itself) ⟷
unitary (heterogenous_cblinfun_id :: 'a ⇒⇩C⇩L 'b) ∧ unitary (heterogenous_cblinfun_id :: 'b ⇒⇩C⇩L 'a)"
lemma heterogenous_same_type_cblinfun[simp]: ‹heterogenous_same_type_cblinfun (x::'a::chilbert_space itself) (y::'a::chilbert_space itself)›
unfolding heterogenous_same_type_cblinfun_def by auto
instantiation cblinfun :: (chilbert_space, chilbert_space) ord begin
definition less_eq_cblinfun_def_heterogenous: ‹A ≤ B ⟷
(if heterogenous_same_type_cblinfun TYPE('a) TYPE('b) then
∀ψ::'b. cinner ψ ((B-A) *⇩V heterogenous_cblinfun_id *⇩V ψ) ≥ 0 else (A=B))›
definition ‹(A :: 'a ⇒⇩C⇩L 'b) < B ⟷ A ≤ B ∧ ¬ B ≤ A›
instance..
end
lemma less_eq_cblinfun_def: ‹A ≤ B ⟷
(∀ψ. cinner ψ (A *⇩V ψ) ≤ cinner ψ (B *⇩V ψ))›
unfolding less_eq_cblinfun_def_heterogenous
by (auto simp del: less_eq_complex_def simp: cblinfun.diff_left cinner_diff_right)
instantiation cblinfun :: (chilbert_space, chilbert_space) ordered_complex_vector begin
instance
proof intro_classes
fix x y z :: ‹'a ⇒⇩C⇩L 'b›
fix a b :: complex
define pos where ‹pos X ⟷ (∀ψ. cinner ψ (X *⇩V ψ) ≥ 0)› for X :: ‹'b ⇒⇩C⇩L 'b›
consider (unitary) ‹heterogenous_same_type_cblinfun TYPE('a) TYPE('b)›
‹⋀A B :: 'a ⇒⇩C⇩L 'b. A ≤ B = pos ((B-A) o⇩C⇩L (heterogenous_cblinfun_id :: 'b⇒⇩C⇩L'a))›
| (trivial) ‹⋀A B :: 'a ⇒⇩C⇩L 'b. A ≤ B ⟷ A = B›
by atomize_elim (auto simp: pos_def less_eq_cblinfun_def_heterogenous)
note cases = this
have [simp]: ‹pos 0›
unfolding pos_def by auto
have pos_nondeg: ‹X = 0› if ‹pos X› and ‹pos (-X)› for X
apply (rule cblinfun_cinner_eqI, simp)
using that by (metis (no_types, lifting) cblinfun.minus_left cinner_minus_right dual_order.antisym equation_minus_iff neg_le_0_iff_le pos_def)
have pos_add: ‹pos (X+Y)› if ‹pos X› and ‹pos Y› for X Y
by (smt (z3) pos_def cblinfun.diff_left cinner_minus_right cinner_simps(3) diff_ge_0_iff_ge diff_minus_eq_add neg_le_0_iff_le order_trans that(1) that(2) uminus_cblinfun.rep_eq)
have pos_scaleC: ‹pos (a *⇩C X)› if ‹a≥0› and ‹pos X› for X a
using that unfolding pos_def by (auto simp: cblinfun.scaleC_left)
let ?id = ‹heterogenous_cblinfun_id :: 'b ⇒⇩C⇩L 'a›
show ‹x ≤ x›
apply (cases rule:cases) by auto
show ‹(x < y) ⟷ (x ≤ y ∧ ¬ y ≤ x)›
unfolding less_cblinfun_def by simp
show ‹x ≤ z› if ‹x ≤ y› and ‹y ≤ z›
proof (cases rule:cases)
case unitary
define a b :: ‹'b ⇒⇩C⇩L 'b› where ‹a = (y-x) o⇩C⇩L heterogenous_cblinfun_id›
and ‹b = (z-y) o⇩C⇩L heterogenous_cblinfun_id›
with unitary that have ‹pos a› and ‹pos b›
by auto
then have ‹pos (a + b)›
by (rule pos_add)
moreover have ‹a + b = (z - x) o⇩C⇩L heterogenous_cblinfun_id›
unfolding a_def b_def
by (metis (no_types, lifting) bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose diff_add_cancel ordered_field_class.sign_simps(2) ordered_field_class.sign_simps(8))
ultimately show ?thesis
using unitary by auto
next
case trivial
with that show ?thesis by auto
qed
show ‹x = y› if ‹x ≤ y› and ‹y ≤ x›
proof (cases rule:cases)
case unitary
then have ‹unitary ?id›
by (auto simp: heterogenous_same_type_cblinfun_def)
define a b :: ‹'b ⇒⇩C⇩L 'b› where ‹a = (y-x) o⇩C⇩L ?id›
and ‹b = (x-y) o⇩C⇩L ?id›
with unitary that have ‹pos a› and ‹pos b›
by auto
then have ‹a = 0›
apply (rule_tac pos_nondeg)
apply (auto simp: a_def b_def)
by (smt (verit, best) add.commute bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose cblinfun_compose_zero_left diff_0 diff_add_cancel group_cancel.rule0 group_cancel.sub1)
then show ?thesis
unfolding a_def using ‹unitary ?id›
by (metis cblinfun_compose_assoc cblinfun_compose_id_right cblinfun_compose_zero_left eq_iff_diff_eq_0 unitaryD2)
next
case trivial
with that show ?thesis by simp
qed
show ‹x + y ≤ x + z› if ‹y ≤ z›
proof (cases rule:cases)
case unitary
with that show ?thesis
by auto
next
case trivial
with that show ?thesis
by auto
qed
show ‹a *⇩C x ≤ a *⇩C y› if ‹x ≤ y› and ‹0 ≤ a›
proof (cases rule:cases)
case unitary
with that pos_scaleC show ?thesis
by (metis cblinfun_compose_scaleC_left complex_vector.scale_right_diff_distrib)
next
case trivial
with that show ?thesis
by auto
qed
show ‹a *⇩C x ≤ b *⇩C x› if ‹a ≤ b› and ‹0 ≤ x›
proof (cases rule:cases)
case unitary
with that show ?thesis
by (auto intro!: pos_scaleC simp flip: scaleC_diff_left)
next
case trivial
with that show ?thesis
by auto
qed
qed
end
lemma positive_id_cblinfun[simp]: "id_cblinfun ≥ 0"
unfolding less_eq_cblinfun_def using cinner_ge_zero by auto
lemma positive_hermitianI: ‹A* = A› if ‹A ≥ 0›
apply (rule cinner_real_hermiteanI)
using that by (auto simp: complex_is_real_iff_compare0 less_eq_cblinfun_def)
lemma cblinfun_leI:
assumes ‹⋀x. norm x = 1 ⟹ x ∙⇩C (A *⇩V x) ≤ x ∙⇩C (B *⇩V x)›
shows ‹A ≤ B›
proof (unfold less_eq_cblinfun_def, intro allI, case_tac ‹ψ = 0›)
fix ψ :: 'a assume ‹ψ = 0›
then show ‹ψ ∙⇩C (A *⇩V ψ) ≤ ψ ∙⇩C (B *⇩V ψ)›
by simp
next
fix ψ :: 'a assume ‹ψ ≠ 0›
define φ where ‹φ = ψ /⇩R norm ψ›
have ‹φ ∙⇩C (A *⇩V φ) ≤ φ ∙⇩C (B *⇩V φ)›
apply (rule assms)
unfolding φ_def
by (simp add: ‹ψ ≠ 0›)
with ‹ψ ≠ 0› show ‹ψ ∙⇩C (A *⇩V ψ) ≤ ψ ∙⇩C (B *⇩V ψ)›
unfolding φ_def
by (smt (verit) cinner_adj_left cinner_scaleR_left cinner_simps(6) complex_of_real_nn_iff mult_cancel_right1 mult_left_mono norm_eq_zero norm_ge_zero of_real_1 right_inverse scaleR_scaleC scaleR_scaleR)
qed
lemma positive_cblinfunI: ‹A ≥ 0› if ‹⋀x. norm x = 1 ⟹ cinner x (A *⇩V x) ≥ 0›
apply (rule cblinfun_leI)
using that by simp
lemma less_eq_scaled_id_norm:
assumes ‹norm A ≤ c› and ‹selfadjoint A›
shows ‹A ≤ c *⇩R id_cblinfun›
proof -
have ‹x ∙⇩C (A *⇩V x) ≤ complex_of_real c› if ‹norm x = 1› for x
proof -
have ‹norm (x ∙⇩C (A *⇩V x)) ≤ norm (A *⇩V x)›
by (metis complex_inner_class.Cauchy_Schwarz_ineq2 mult_cancel_right1 that)
also have ‹… ≤ norm A›
by (metis more_arith_simps(6) norm_cblinfun that)
also have ‹… ≤ c›
by (rule assms)
finally have ‹norm (x ∙⇩C (A *⇩V x)) ≤ c›
by -
moreover have ‹x ∙⇩C (A *⇩V x) ∈ ℝ›
by (metis assms(2) cinner_hermitian_real)
ultimately show ?thesis
by (smt (verit) Re_complex_of_real Reals_cases complex_of_real_nn_iff less_eq_complex_def norm_of_real reals_zero_comparable)
qed
then show ?thesis
by (smt (verit) cblinfun.scaleC_left cblinfun_id_cblinfun_apply cblinfun_leI cinner_scaleC_right cnorm_eq_1 mult_cancel_left2 scaleR_scaleC)
qed
lemma positive_cblinfun_squareI: ‹A = B* o⇩C⇩L B ⟹ A ≥ 0›
apply (rule positive_cblinfunI)
by (metis cblinfun_apply_cblinfun_compose cinner_adj_right cinner_ge_zero)
lemma one_dim_loewner_order: ‹A ≥ B ⟷ one_dim_iso A ≥ (one_dim_iso B :: complex)› for A B :: ‹'a ⇒⇩C⇩L 'a::{chilbert_space, one_dim}›
proof -
have A: ‹A = one_dim_iso A *⇩C id_cblinfun›
by simp
have B: ‹B = one_dim_iso B *⇩C id_cblinfun›
by simp
have ‹A ≥ B ⟷ (∀ψ. cinner ψ (A ψ) ≥ cinner ψ (B ψ))›
by (simp add: less_eq_cblinfun_def)
also have ‹… ⟷ (∀ψ::'a. one_dim_iso B * (ψ ∙⇩C ψ) ≤ one_dim_iso A * (ψ ∙⇩C ψ))›
apply (subst A, subst B)
by (metis (no_types, opaque_lifting) cinner_scaleC_right id_cblinfun_apply scaleC_cblinfun.rep_eq)
also have ‹… ⟷ one_dim_iso A ≥ (one_dim_iso B :: complex)›
by (auto intro!: mult_right_mono elim!: allE[where x=1])
finally show ?thesis
by -
qed
lemma one_dim_positive: ‹A ≥ 0 ⟷ one_dim_iso A ≥ (0::complex)› for A :: ‹'a ⇒⇩C⇩L 'a::{chilbert_space, one_dim}›
using one_dim_loewner_order[where B=0] by auto
lemma op_square_nondegenerate: ‹a = 0› if ‹a* o⇩C⇩L a = 0›
proof (rule cblinfun_eq_0_on_UNIV_span[where basis=UNIV]; simp)
fix s
from that have ‹s ∙⇩C ((a* o⇩C⇩L a) *⇩V s) = 0›
by simp
then have ‹(a *⇩V s) ∙⇩C (a *⇩V s) = 0›
by (simp add: cinner_adj_right)
then show ‹a *⇩V s = 0›
by simp
qed
lemma comparable_hermitean:
assumes ‹a ≤ b›
assumes ‹selfadjoint a›
shows ‹selfadjoint b›
by (smt (verit, best) assms(1) assms(2) cinner_hermitian_real cinner_real_hermiteanI comparable complex_is_real_iff_compare0 less_eq_cblinfun_def selfadjoint_def)
lemma comparable_hermitean':
assumes ‹a ≤ b›
assumes ‹selfadjoint b›
shows ‹selfadjoint a›
by (smt (verit, best) assms(1) assms(2) cinner_hermitian_real cinner_real_hermiteanI comparable complex_is_real_iff_compare0 less_eq_cblinfun_def selfadjoint_def)
lemma Proj_mono: ‹Proj S ≤ Proj T ⟷ S ≤ T›
proof (rule iffI)
assume ‹S ≤ T›
define D where ‹D = Proj T - Proj S›
from ‹S ≤ T› have TS_S[simp]: ‹Proj T o⇩C⇩L Proj S = Proj S›
by (smt (verit, ccfv_threshold) Proj_idempotent Proj_range cblinfun_apply_cblinfun_compose cblinfun_apply_in_image cblinfun_eqI cblinfun_fixes_range less_eq_ccsubspace.rep_eq subset_iff)
then have ST_S[simp]: ‹Proj S o⇩C⇩L Proj T = Proj S›
by (metis adj_Proj adj_cblinfun_compose)
have ‹D* o⇩C⇩L D = D›
by (simp add: D_def cblinfun_compose_minus_left cblinfun_compose_minus_right adj_minus adj_Proj)
then have ‹D ≥ 0›
by (metis positive_cblinfun_squareI)
then show ‹Proj S ≤ Proj T›
by (simp add: D_def)
next
assume PS_PT: ‹Proj S ≤ Proj T›
show ‹S ≤ T›
proof (rule ccsubspace_leI_unit)
fix ψ assume ‹ψ ∈ space_as_set S› and [simp]: ‹norm ψ = 1›
then have ‹1 = norm (Proj S *⇩V ψ)›
by (simp add: Proj_fixes_image)
also from PS_PT have ‹… ≤ norm (Proj T *⇩V ψ)›
by (metis (no_types, lifting) Proj_idempotent adj_Proj cblinfun_apply_cblinfun_compose cinner_adj_left cnorm_le less_eq_cblinfun_def)
also have ‹… ≤ 1›
by (metis Proj_is_Proj ‹norm ψ = 1› is_Proj_reduces_norm)
ultimately have ‹norm (Proj T *⇩V ψ) = 1›
by auto
then show ‹ψ ∈ space_as_set T›
by (simp add: norm_Proj_apply_1)
qed
qed
subsection ‹Embedding vectors to operators›
lift_definition vector_to_cblinfun :: ‹'a::complex_normed_vector ⇒ 'b::one_dim ⇒⇩C⇩L 'a› is
‹λψ φ. one_dim_iso φ *⇩C ψ›
by (simp add: bounded_clinear_scaleC_const)
lemma vector_to_cblinfun_cblinfun_compose[simp]:
"A o⇩C⇩L (vector_to_cblinfun ψ) = vector_to_cblinfun (A *⇩V ψ)"
apply transfer
unfolding comp_def bounded_clinear_def clinear_def Vector_Spaces.linear_def
module_hom_def module_hom_axioms_def
by simp
lemma vector_to_cblinfun_add: ‹vector_to_cblinfun (x + y) = vector_to_cblinfun x + vector_to_cblinfun y›
by transfer (simp add: scaleC_add_right)
lemma norm_vector_to_cblinfun[simp]: "norm (vector_to_cblinfun x) = norm x"
proof transfer
have "bounded_clinear (one_dim_iso::'a ⇒ complex)"
by simp
moreover have "onorm (one_dim_iso::'a ⇒ complex) * norm x = norm x"
for x :: 'b
by simp
ultimately show "onorm (λφ. one_dim_iso (φ::'a) *⇩C x) = norm x"
for x :: 'b
by (subst onorm_scaleC_left)
qed
lemma bounded_clinear_vector_to_cblinfun[bounded_clinear]: "bounded_clinear vector_to_cblinfun"
apply (rule bounded_clinearI[where K=1])
apply (transfer, simp add: scaleC_add_right)
apply (transfer, simp add: mult.commute)
by simp
lemma vector_to_cblinfun_scaleC[simp]:
"vector_to_cblinfun (a *⇩C ψ) = a *⇩C vector_to_cblinfun ψ" for a::complex
by (intro clinear.scaleC bounded_clinear.clinear bounded_clinear_vector_to_cblinfun)
lemma vector_to_cblinfun_apply_one_dim[simp]:
shows "vector_to_cblinfun φ *⇩V γ = one_dim_iso γ *⇩C φ"
by transfer (rule refl)
lemma vector_to_cblinfun_one_dim_iso[simp]: ‹vector_to_cblinfun = one_dim_iso›
by (auto intro!: ext cblinfun_eqI)
lemma vector_to_cblinfun_adj_apply[simp]:
shows "vector_to_cblinfun ψ* *⇩V φ = of_complex (cinner ψ φ)"
by (simp add: cinner_adj_right one_dim_iso_def one_dim_iso_inj)
lemma vector_to_cblinfun_comp_one[simp]:
"(vector_to_cblinfun s :: 'a::one_dim ⇒⇩C⇩L _) o⇩C⇩L 1
= (vector_to_cblinfun s :: 'b::one_dim ⇒⇩C⇩L _)"
apply (transfer fixing: s)
by fastforce
lemma vector_to_cblinfun_0[simp]: "vector_to_cblinfun 0 = 0"
by (metis cblinfun.zero_left cblinfun_compose_zero_left vector_to_cblinfun_cblinfun_compose)
lemma image_vector_to_cblinfun[simp]: "vector_to_cblinfun x *⇩S ⊤ = ccspan {x}"
proof transfer
show "closure (range (λφ::'b. one_dim_iso φ *⇩C x)) = closure (cspan {x})"
for x :: 'a
proof (rule arg_cong [where f = closure])
have "k *⇩C x ∈ range (λφ. one_dim_iso φ *⇩C x)" for k
by (smt (z3) id_apply one_dim_iso_id one_dim_iso_idem range_eqI)
thus "range (λφ. one_dim_iso (φ::'b) *⇩C x) = cspan {x}"
unfolding complex_vector.span_singleton
by auto
qed
qed
lemma vector_to_cblinfun_adj_comp_vector_to_cblinfun[simp]:
shows "vector_to_cblinfun ψ* o⇩C⇩L vector_to_cblinfun φ = cinner ψ φ *⇩C id_cblinfun"
proof -
have "one_dim_iso γ *⇩C one_dim_iso (of_complex (ψ ∙⇩C φ)) =
(ψ ∙⇩C φ) *⇩C one_dim_iso γ"
for γ :: "'c::one_dim"
by (metis complex_vector.scale_left_commute of_complex_def one_dim_iso_of_one one_dim_iso_scaleC one_dim_scaleC_1)
hence "one_dim_iso ((vector_to_cblinfun ψ* o⇩C⇩L vector_to_cblinfun φ) *⇩V γ)
= one_dim_iso ((cinner ψ φ *⇩C id_cblinfun) *⇩V γ)"
for γ :: "'c::one_dim"
by simp
hence "((vector_to_cblinfun ψ* o⇩C⇩L vector_to_cblinfun φ) *⇩V γ) = ((cinner ψ φ *⇩C id_cblinfun) *⇩V γ)"
for γ :: "'c::one_dim"
by (rule one_dim_iso_inj)
thus ?thesis
using cblinfun_eqI[where x = "vector_to_cblinfun ψ* o⇩C⇩L vector_to_cblinfun φ"
and y = "(ψ ∙⇩C φ) *⇩C id_cblinfun"]
by auto
qed
lemma isometry_vector_to_cblinfun[simp]:
assumes "norm x = 1"
shows "isometry (vector_to_cblinfun x)"
using assms cnorm_eq_1 isometry_def by force
lemma image_vector_to_cblinfun_adj:
assumes ‹ψ ∉ space_as_set (- S)›
shows ‹(vector_to_cblinfun ψ)* *⇩S S = ⊤›
proof -
from assms obtain φ where ‹φ ∈ space_as_set S› and ‹¬ is_orthogonal ψ φ›
by (metis orthogonal_complementI uminus_ccsubspace.rep_eq)
have ‹((vector_to_cblinfun ψ)* *⇩S S :: 'b ccsubspace) ≥ (vector_to_cblinfun ψ)* *⇩S ccspan {φ}› (is ‹_ ≥ …›)
by (simp add: ‹φ ∈ space_as_set S› cblinfun_image_mono ccspan_leqI)
also have ‹… = ccspan {(vector_to_cblinfun ψ)* *⇩V φ}›
by (auto simp: cblinfun_image_ccspan)
also have ‹… = ccspan {of_complex (ψ ∙⇩C φ)}›
by auto
also have ‹… > ⊥›
by (simp add: ‹ψ ∙⇩C φ ≠ 0› flip: bot.not_eq_extremum )
finally(dual_order.strict_trans1) show ?thesis
using one_dim_ccsubspace_all_or_nothing bot.not_eq_extremum by auto
qed
lemma image_vector_to_cblinfun_adj':
assumes ‹ψ ≠ 0›
shows ‹(vector_to_cblinfun ψ)* *⇩S ⊤ = ⊤›
apply (rule image_vector_to_cblinfun_adj)
using assms by simp
subsection ‹Rank-1 operators / butterflies›
definition rank1 where ‹rank1 A ⟷ (∃ψ. A *⇩S ⊤ = ccspan {ψ})›
definition "butterfly (s::'a::complex_normed_vector) (t::'b::chilbert_space)
= vector_to_cblinfun s o⇩C⇩L (vector_to_cblinfun t :: complex ⇒⇩C⇩L _)*"
abbreviation "selfbutter s ≡ butterfly s s"
lemma butterfly_add_left: ‹butterfly (a + a') b = butterfly a b + butterfly a' b›
by (simp add: butterfly_def vector_to_cblinfun_add cbilinear_add_left bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose)
lemma butterfly_add_right: ‹butterfly a (b + b') = butterfly a b + butterfly a b'›
by (simp add: butterfly_def adj_plus vector_to_cblinfun_add cblinfun_compose_add_right)
lemma butterfly_def_one_dim: "butterfly s t = (vector_to_cblinfun s :: 'c::one_dim ⇒⇩C⇩L _)
o⇩C⇩L (vector_to_cblinfun t :: 'c ⇒⇩C⇩L _)*"
(is "_ = ?rhs") for s :: "'a::complex_normed_vector" and t :: "'b::chilbert_space"
proof -
let ?isoAC = "1 :: 'c ⇒⇩C⇩L complex"
let ?isoCA = "1 :: complex ⇒⇩C⇩L 'c"
let ?vector = "vector_to_cblinfun :: _ ⇒ ('c ⇒⇩C⇩L _)"
have "butterfly s t =
(?vector s o⇩C⇩L ?isoCA) o⇩C⇩L (?vector t o⇩C⇩L ?isoCA)*"
unfolding butterfly_def vector_to_cblinfun_comp_one by simp
also have "… = ?vector s o⇩C⇩L (?isoCA o⇩C⇩L ?isoCA*) o⇩C⇩L (?vector t)*"
by (metis (no_types, lifting) cblinfun_compose_assoc adj_cblinfun_compose)
also have "… = ?rhs"
by simp
finally show ?thesis
by simp
qed
lemma butterfly_comp_cblinfun: "butterfly ψ φ o⇩C⇩L a = butterfly ψ (a* *⇩V φ)"
unfolding butterfly_def
by (simp add: cblinfun_compose_assoc flip: vector_to_cblinfun_cblinfun_compose)
lemma cblinfun_comp_butterfly: "a o⇩C⇩L butterfly ψ φ = butterfly (a *⇩V ψ) φ"
unfolding butterfly_def
by (simp add: cblinfun_compose_assoc flip: vector_to_cblinfun_cblinfun_compose)
lemma butterfly_apply[simp]: "butterfly ψ ψ' *⇩V φ = (ψ' ∙⇩C φ) *⇩C ψ"
by (simp add: butterfly_def scaleC_cblinfun.rep_eq)
lemma butterfly_scaleC_left[simp]: "butterfly (c *⇩C ψ) φ = c *⇩C butterfly ψ φ"
unfolding butterfly_def vector_to_cblinfun_scaleC scaleC_adj
by (simp add: cnj_x_x)
lemma butterfly_scaleC_right[simp]: "butterfly ψ (c *⇩C φ) = cnj c *⇩C butterfly ψ φ"
unfolding butterfly_def vector_to_cblinfun_scaleC scaleC_adj
by (simp add: cnj_x_x)
lemma butterfly_scaleR_left[simp]: "butterfly (r *⇩R ψ) φ = r *⇩C butterfly ψ φ"
by (simp add: scaleR_scaleC)
lemma butterfly_scaleR_right[simp]: "butterfly ψ (r *⇩R φ) = r *⇩C butterfly ψ φ"
by (simp add: butterfly_scaleC_right scaleR_scaleC)
lemma butterfly_adjoint[simp]: "(butterfly ψ φ)* = butterfly φ ψ"
unfolding butterfly_def by auto
lemma butterfly_comp_butterfly[simp]: "butterfly ψ1 ψ2 o⇩C⇩L butterfly ψ3 ψ4 = (ψ2 ∙⇩C ψ3) *⇩C butterfly ψ1 ψ4"
by (simp add: butterfly_comp_cblinfun)
lemma butterfly_0_left[simp]: "butterfly 0 a = 0"
by (simp add: butterfly_def)
lemma butterfly_0_right[simp]: "butterfly a 0 = 0"
by (simp add: butterfly_def)
lemma butterfly_is_rank1:
assumes ‹φ ≠ 0›
shows ‹butterfly ψ φ *⇩S ⊤ = ccspan {ψ}›
using assms by (simp add: butterfly_def cblinfun_compose_image image_vector_to_cblinfun_adj')
lemma rank1_is_butterfly:
assumes ‹A *⇩S ⊤ = ccspan {ψ::_::chilbert_space}›
shows ‹∃φ. A = butterfly ψ φ›
proof (rule exI[of _ ‹A* *⇩V (ψ /⇩R (norm ψ)⇧2)›], rule cblinfun_eqI)
fix γ :: 'b
from assms have ‹A *⇩V γ ∈ space_as_set (ccspan {ψ})›
by (simp flip: assms)
then obtain c where c: ‹A *⇩V γ = c *⇩C ψ›
apply atomize_elim
apply (auto simp: ccspan.rep_eq)
by (metis complex_vector.span_breakdown_eq complex_vector.span_empty eq_iff_diff_eq_0 singletonD)
have ‹A *⇩V γ = butterfly ψ (ψ /⇩R (norm ψ)⇧2) *⇩V (A *⇩V γ)›
apply (auto simp: c simp flip: scaleC_scaleC)
by (metis cinner_eq_zero_iff divideC_field_simps(1) power2_norm_eq_cinner scaleC_left_commute scaleC_zero_right)
also have ‹… = (butterfly ψ (ψ /⇩R (norm ψ)⇧2) o⇩C⇩L A) *⇩V γ›
by simp
also have ‹… = butterfly ψ (A* *⇩V (ψ /⇩R (norm ψ)⇧2)) *⇩V γ›
by (simp add: cinner_adj_left)
finally show ‹A *⇩V γ = …›
by -
qed
lemma rank1_0[simp]: ‹rank1 0›
by (metis ccspan_0 kernel_0 kernel_apply_self rank1_def)
lemma rank1_iff_butterfly: ‹rank1 A ⟷ (∃ψ φ. A = butterfly ψ φ)›
for A :: ‹_::complex_inner ⇒⇩C⇩L _::chilbert_space›
proof (rule iffI)
assume ‹rank1 A›
then obtain ψ where ‹A *⇩S ⊤ = ccspan {ψ}›
using rank1_def by auto
then have ‹∃φ. A = butterfly ψ φ›
by (rule rank1_is_butterfly)
then show ‹∃ψ φ. A = butterfly ψ φ›
by auto
next
assume asm: ‹∃ψ φ. A = butterfly ψ φ›
show ‹rank1 A›
proof (cases ‹A = 0›)
case True
then show ?thesis
by simp
next
case False
from asm obtain ψ φ where A: ‹A = butterfly ψ φ›
by auto
with False have ‹ψ ≠ 0› and ‹φ ≠ 0›
by auto
then have ‹butterfly ψ φ *⇩S ⊤ = ccspan {ψ}›
by (rule_tac butterfly_is_rank1)
with A ‹ψ ≠ 0› show ‹rank1 A›
by (auto intro!: exI[of _ ψ] simp: rank1_def)
qed
qed
lemma norm_butterfly: "norm (butterfly ψ φ) = norm ψ * norm φ"
proof (cases "φ=0")
case True
then show ?thesis by simp
next
case False
show ?thesis
unfolding norm_cblinfun.rep_eq
proof (rule onormI[OF _ False])
fix x
have "cmod (φ ∙⇩C x) * norm ψ ≤ norm ψ * norm φ * norm x"
by (metis ab_semigroup_mult_class.mult_ac(1) complex_inner_class.Cauchy_Schwarz_ineq2 mult.commute mult_left_mono norm_ge_zero)
thus "norm (butterfly ψ φ *⇩V x) ≤ norm ψ * norm φ * norm x"
by (simp add: power2_eq_square)
show "norm (butterfly ψ φ *⇩V φ) = norm ψ * norm φ * norm φ"
by (smt (z3) ab_semigroup_mult_class.mult_ac(1) butterfly_apply mult.commute norm_eq_sqrt_cinner norm_ge_zero norm_scaleC power2_eq_square real_sqrt_abs real_sqrt_eq_iff)
qed
qed
lemma bounded_sesquilinear_butterfly[bounded_sesquilinear]: ‹bounded_sesquilinear (λ(b::'b::chilbert_space) (a::'a::chilbert_space). butterfly a b)›
proof standard
fix a a' :: 'a and b b' :: 'b and r :: complex
show ‹butterfly (a + a') b = butterfly a b + butterfly a' b›
by (rule butterfly_add_left)
show ‹butterfly a (b + b') = butterfly a b + butterfly a b'›
by (rule butterfly_add_right)
show ‹butterfly (r *⇩C a) b = r *⇩C butterfly a b›
by simp
show ‹butterfly a (r *⇩C b) = cnj r *⇩C butterfly a b›
by simp
show ‹∃K. ∀b a. norm (butterfly a b) ≤ norm b * norm a * K ›
apply (rule exI[of _ 1])
by (simp add: norm_butterfly)
qed
lemma inj_selfbutter_upto_phase:
assumes "selfbutter x = selfbutter y"
shows "∃c. cmod c = 1 ∧ x = c *⇩C y"
proof (cases "x = 0")
case True
from assms have "y = 0"
using norm_butterfly
by (metis True butterfly_0_left divisors_zero norm_eq_zero)
with True show ?thesis
using norm_one by fastforce
next
case False
define c where "c = (y ∙⇩C x) / (x ∙⇩C x)"
have "(x ∙⇩C x) *⇩C x = selfbutter x *⇩V x"
by (simp add: butterfly_apply)
also have "… = selfbutter y *⇩V x"
using assms by simp
also have "… = (y ∙⇩C x) *⇩C y"
by (simp add: butterfly_apply)
finally have xcy: "x = c *⇩C y"
by (simp add: c_def ceq_vector_fraction_iff)
have "cmod c * norm x = cmod c * norm y"
using assms norm_butterfly
by (smt (verit, ccfv_SIG) ‹(x ∙⇩C x) *⇩C x = selfbutter x *⇩V x› ‹selfbutter y *⇩V x = (y ∙⇩C x) *⇩C y› cinner_scaleC_right complex_vector.scale_left_commute complex_vector.scale_right_imp_eq mult_cancel_left norm_eq_sqrt_cinner norm_eq_zero scaleC_scaleC xcy)
also have "cmod c * norm y = norm (c *⇩C y)"
by simp
also have "… = norm x"
unfolding xcy[symmetric] by simp
finally have c: "cmod c = 1"
by (simp add: False)
from c xcy show ?thesis
by auto
qed
lemma butterfly_eq_proj:
assumes "norm x = 1"
shows "selfbutter x = proj x"
proof -
define B and φ :: "complex ⇒⇩C⇩L 'a"
where "B = selfbutter x" and "φ = vector_to_cblinfun x"
then have B: "B = φ o⇩C⇩L φ*"
unfolding butterfly_def by simp
have φadjφ: "φ* o⇩C⇩L φ = id_cblinfun"
using φ_def assms isometry_def isometry_vector_to_cblinfun by blast
have "B o⇩C⇩L B = φ o⇩C⇩L (φ* o⇩C⇩L φ) o⇩C⇩L φ*"
by (simp add: B cblinfun_assoc_left(1))
also have "… = B"
unfolding φadjφ by (simp add: B)
finally have idem: "B o⇩C⇩L B = B".
have herm: "B = B*"
unfolding B by simp
from idem herm have BProj: "B = Proj (B *⇩S top)"
by (rule Proj_on_own_range'[symmetric])
have "B *⇩S top = ccspan {x}"
by (simp add: B φ_def assms cblinfun_compose_image range_adjoint_isometry)
with BProj show "B = proj x"
by simp
qed
lemma butterfly_sgn_eq_proj:
shows "selfbutter (sgn x) = proj x"
proof (cases ‹x = 0›)
case True
then show ?thesis
by simp
next
case False
then have ‹selfbutter (sgn x) = proj (sgn x)›
by (simp add: butterfly_eq_proj norm_sgn)
also have ‹ccspan {sgn x} = ccspan {x}›
by (metis ccspan_singleton_scaleC scaleC_eq_0_iff scaleR_scaleC sgn_div_norm sgn_zero_iff)
finally show ?thesis
by -
qed
lemma butterfly_is_Proj:
‹norm x = 1 ⟹ is_Proj (selfbutter x)›
by (subst butterfly_eq_proj, simp_all)
lemma cspan_butterfly_UNIV:
assumes ‹cspan basisA = UNIV›
assumes ‹cspan basisB = UNIV›
assumes ‹is_ortho_set basisB›
assumes ‹⋀b. b ∈ basisB ⟹ norm b = 1›
shows ‹cspan {butterfly a b| (a::'a::{complex_normed_vector}) (b::'b::{chilbert_space,cfinite_dim}). a ∈ basisA ∧ b ∈ basisB} = UNIV›
proof -
have F: ‹∃F∈{butterfly a b |a b. a ∈ basisA ∧ b ∈ basisB}. ∀b'∈basisB. F *⇩V b' = (if b' = b then a else 0)›
if ‹a ∈ basisA› and ‹b ∈ basisB› for a b
apply (rule bexI[where x=‹butterfly a b›])
using assms that by (auto simp: is_ortho_set_def cnorm_eq_1)
show ?thesis
apply (rule cblinfun_cspan_UNIV[where basisA=basisB and basisB=basisA])
using assms apply auto[2]
using F by (smt (verit, ccfv_SIG) image_iff)
qed
lemma cindependent_butterfly:
fixes basisA :: ‹'a::chilbert_space set› and basisB :: ‹'b::chilbert_space set›
assumes ‹is_ortho_set basisA› ‹is_ortho_set basisB›
assumes normA: ‹⋀a. a∈basisA ⟹ norm a = 1› and normB: ‹⋀b. b∈basisB ⟹ norm b = 1›
shows ‹cindependent {butterfly a b| a b. a∈basisA ∧ b∈basisB}›
proof (unfold complex_vector.independent_explicit_module, intro allI impI, rename_tac T f g)
fix T :: ‹('b ⇒⇩C⇩L 'a) set› and f :: ‹'b ⇒⇩C⇩L 'a ⇒ complex› and g :: ‹'b ⇒⇩C⇩L 'a›
assume ‹finite T›
assume T_subset: ‹T ⊆ {butterfly a b |a b. a ∈ basisA ∧ b ∈ basisB}›
define lin where ‹lin = (∑g∈T. f g *⇩C g)›
assume ‹lin = 0›
assume ‹g ∈ T›
then obtain a b where g: ‹g = butterfly a b› and [simp]: ‹a ∈ basisA› ‹b ∈ basisB›
using T_subset by auto
have *: "(vector_to_cblinfun a)* *⇩V f g *⇩C g *⇩V b = 0"
if ‹g ∈ T - {butterfly a b}› for g
proof -
from that
obtain a' b' where g: ‹g = butterfly a' b'› and [simp]: ‹a' ∈ basisA› ‹b' ∈ basisB›
using T_subset by auto
from that have ‹g ≠ butterfly a b› by auto
with g consider (a) ‹a≠a'› | (b) ‹b≠b'›
by auto
then show ‹(vector_to_cblinfun a)* *⇩V f g *⇩C g *⇩V b = 0›
proof cases
case a
then show ?thesis
using ‹is_ortho_set basisA› unfolding g
by (auto simp: is_ortho_set_def butterfly_def scaleC_cblinfun.rep_eq)
next
case b
then show ?thesis
using ‹is_ortho_set basisB› unfolding g
by (auto simp: is_ortho_set_def butterfly_def scaleC_cblinfun.rep_eq)
qed
qed
have ‹0 = (vector_to_cblinfun a)* *⇩V lin *⇩V b›
using ‹lin = 0› by auto
also have ‹… = (∑g∈T. (vector_to_cblinfun a)* *⇩V (f g *⇩C g) *⇩V b)›
unfolding lin_def
apply (rule complex_vector.linear_sum)
by (smt (z3) cblinfun.scaleC_left cblinfun.scaleC_right cblinfun.add_right clinearI plus_cblinfun.rep_eq)
also have ‹… = (∑g∈{butterfly a b}. (vector_to_cblinfun a)* *⇩V (f g *⇩C g) *⇩V b)›
apply (rule sum.mono_neutral_right)
using ‹finite T› * ‹g ∈ T› g by auto
also have ‹… = (vector_to_cblinfun a)* *⇩V (f g *⇩C g) *⇩V b›
by (simp add: g)
also have ‹… = f g›
unfolding g
using normA normB by (auto simp: butterfly_def scaleC_cblinfun.rep_eq cnorm_eq_1)
finally show ‹f g = 0›
by simp
qed
lemma clinear_eq_butterflyI:
fixes F G :: ‹('a::{chilbert_space,cfinite_dim} ⇒⇩C⇩L 'b::complex_inner) ⇒ 'c::complex_vector›
assumes "clinear F" and "clinear G"
assumes ‹cspan basisA = UNIV› ‹cspan basisB = UNIV›
assumes ‹is_ortho_set basisA› ‹is_ortho_set basisB›
assumes "⋀a b. a∈basisA ⟹ b∈basisB ⟹ F (butterfly a b) = G (butterfly a b)"
assumes ‹⋀b. b∈basisB ⟹ norm b = 1›
shows "F = G"
apply (rule complex_vector.linear_eq_on_span[where f=F, THEN ext, rotated 3])
apply (subst cspan_butterfly_UNIV)
using assms by auto
lemma sum_butterfly_is_Proj:
assumes ‹is_ortho_set E›
assumes ‹⋀e. e∈E ⟹ norm e = 1›
shows ‹is_Proj (∑e∈E. butterfly e e)›
proof (cases ‹finite E›)
case True
show ?thesis
proof (rule is_Proj_I)
show ‹(∑e∈E. butterfly e e)* = (∑e∈E. butterfly e e)›
by (simp add: sum_adj)
have ortho: ‹f ≠ e ⟹ e ∈ E ⟹ f ∈ E ⟹ is_orthogonal f e› for f e
by (meson assms(1) is_ortho_set_def)
have unit: ‹e ∙⇩C e = 1› if ‹e ∈ E› for e
using assms(2) cnorm_eq_1 that by blast
have *: ‹(∑f∈E. (f ∙⇩C e) *⇩C butterfly f e) = butterfly e e› if ‹e ∈ E› for e
apply (subst sum_single[where i=e])
by (auto intro!: simp: that ortho unit True)
show ‹(∑e∈E. butterfly e e) o⇩C⇩L (∑e∈E. butterfly e e) = (∑e∈E. butterfly e e)›
by (auto simp: * cblinfun_compose_sum_right cblinfun_compose_sum_left)
qed
next
case False
then show ?thesis
by simp
qed
lemma rank1_compose_left: ‹rank1 (a o⇩C⇩L b)› if ‹rank1 b›
proof -
from ‹rank1 b›
obtain ψ where ‹b *⇩S ⊤ = ccspan {ψ}›
using rank1_def by blast
then have *: ‹(a o⇩C⇩L b) *⇩S ⊤ = ccspan {a ψ}›
by (metis cblinfun_assoc_left(2) cblinfun_image_ccspan image_empty image_insert)
then show ‹rank1 (a o⇩C⇩L b)›
using rank1_def by blast
qed
lemma csubspace_of_1dim_space:
assumes ‹S ≠ {0}›
assumes ‹csubspace S›
assumes ‹S ⊆ cspan {ψ}›
shows ‹S = cspan {ψ}›
proof -
from ‹S ≠ {0}› ‹csubspace S›
obtain φ where ‹φ ∈ S› and ‹φ ≠ 0›
using complex_vector.subspace_0 by blast
then have ‹φ ∈ cspan {ψ}›
using ‹S ⊆ cspan {ψ}› by blast
with ‹φ ≠ 0› obtain c where ‹φ = c *⇩C ψ› and ‹c ≠ 0›
by (metis complex_vector.span_breakdown_eq complex_vector.span_empty right_minus_eq scaleC_eq_0_iff singletonD)
have ‹cspan {ψ} = cspan {inverse c *⇩C φ}›
by (simp add: ‹φ = c *⇩C ψ› ‹c ≠ 0›)
also have ‹… ⊆ cspan {φ}›
using ‹c ≠ 0› by auto
also from ‹φ = c *⇩C ψ› ‹φ ∈ S› ‹c ≠ 0› assms
have ‹… ⊆ S›
by (metis complex_vector.span_subspace cspan_singleton_scaleC empty_subsetI insert_Diff insert_mono)
finally have ‹cspan {ψ} ⊆ S›
by -
with ‹S ⊆ cspan {ψ}› show ?thesis
by simp
qed
lemma subspace_of_1dim_ccspan:
assumes ‹S ≠ 0›
assumes ‹S ≤ ccspan {ψ}›
shows ‹S = ccspan {ψ}›
using assms apply transfer
by (simp add: csubspace_of_1dim_space)
lemma rank1_compose_right: ‹rank1 (a o⇩C⇩L b)› if ‹rank1 a›
proof -
have ‹(a o⇩C⇩L b) *⇩S ⊤ ≤ a *⇩S ⊤›
by (metis cblinfun_apply_cblinfun_compose cblinfun_apply_in_image cblinfun_image_ccspan_leqI ccspan_UNIV)
also from ‹rank1 a›
obtain ψ where ‹a *⇩S ⊤ = ccspan {ψ}›
using rank1_def by blast
finally have *: ‹(a o⇩C⇩L b) *⇩S ⊤ ≤ ccspan {ψ}›
by -
show ‹rank1 (a o⇩C⇩L b)›
proof (cases ‹(a o⇩C⇩L b) *⇩S ⊤ = 0›)
case True
then show ?thesis
by simp
next
case False
with * have ‹(a o⇩C⇩L b) *⇩S ⊤ = ccspan {ψ}›
using subspace_of_1dim_ccspan by blast
then show ?thesis
using rank1_def by blast
qed
qed
lemma rank1_scaleC: ‹rank1 (c *⇩C a)› if ‹rank1 a› and ‹c ≠ 0›
using rank1_compose_left[OF ‹rank1 a›, where a=‹c *⇩C id_cblinfun›]
using that by force
lemma rank1_uminus: ‹rank1 (-a)› if ‹rank1 a›
using that rank1_scaleC[where c=‹-1› and a=a] by simp
lemma rank1_uminus_iff[simp]: ‹rank1 (-a) ⟷ rank1 a›
using rank1_uminus by force
lemma rank1_adj: ‹rank1 (a*)› if ‹rank1 a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
by (metis adj_0 butterfly_adjoint rank1_iff_butterfly that)
lemma rank1_adj_iff[simp]: ‹rank1 (a*) ⟷ rank1 a›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
by (metis double_adj rank1_adj)
lemma butterflies_sum_id_finite: ‹id_cblinfun = (∑x∈B. selfbutter x)› if ‹is_onb B› for B :: ‹'a :: {cfinite_dim, chilbert_space} set›
proof (rule cblinfun_eq_gen_eqI)
from ‹is_onb B› show ‹ccspan B = ⊤›
by (simp add: is_onb_def)
from ‹is_onb B› have ‹cindependent B›
by (simp add: is_onb_def is_ortho_set_cindependent)
then have [simp]: ‹finite B›
using cindependent_cfinite_dim_finite by blast
from ‹is_onb B›
have 1: ‹j ≠ b ⟹ j ∈ B ⟹ is_orthogonal j b› if ‹b ∈ B› for j b
using that by (auto simp add: is_onb_def is_ortho_set_def)
from ‹is_onb B›
have 2: ‹b ∙⇩C b = 1› if ‹b ∈ B› for b
using that by (simp add: is_onb_def cnorm_eq_1)
fix b assume ‹b ∈ B›
then show ‹id_cblinfun *⇩V b = (∑x∈B. selfbutter x) *⇩V b›
using 1 2 by (simp add: cblinfun.sum_left sum_single[where i=b])
qed
lemma butterfly_sum_left: ‹butterfly (∑i∈M. ψ i) φ = (∑i∈M. butterfly (ψ i) φ)›
apply (induction M rule:infinite_finite_induct)
by (auto simp add: butterfly_add_left)
lemma butterfly_sum_right: ‹butterfly ψ (∑i∈M. φ i) = (∑i∈M. butterfly ψ (φ i))›
apply (induction M rule:infinite_finite_induct)
by (auto simp add: butterfly_add_right)
subsection ‹Banach-Steinhaus›
theorem cbanach_steinhaus:
fixes F :: ‹'c ⇒ 'a::cbanach ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹⋀x. ∃M. ∀n. norm ((F n) *⇩V x) ≤ M›
shows ‹∃M. ∀ n. norm (F n) ≤ M›
using cblinfun_blinfun_transfer[transfer_rule]
apply fail?
proof (use assms in transfer)
fix F :: ‹'c ⇒ 'a ⇒⇩L 'b› assume ‹(⋀x. ∃M. ∀n. norm (F n *⇩v x) ≤ M)›
hence ‹⋀x. bounded (range (λn. blinfun_apply (F n) x))›
by (metis (no_types, lifting) boundedI rangeE)
hence ‹bounded (range F)›
by (simp add: banach_steinhaus)
thus ‹∃M. ∀n. norm (F n) ≤ M›
by (simp add: bounded_iff)
qed
subsection ‹Riesz-representation theorem›
theorem riesz_representation_cblinfun_existence:
fixes f::‹'a::chilbert_space ⇒⇩C⇩L complex›
shows ‹∃t. ∀x. f *⇩V x = (t ∙⇩C x)›
by transfer (rule riesz_representation_existence)
lemma riesz_representation_cblinfun_unique:
fixes f::‹'a::complex_inner ⇒⇩C⇩L complex›
assumes ‹⋀x. f *⇩V x = (t ∙⇩C x)›
assumes ‹⋀x. f *⇩V x = (u ∙⇩C x)›
shows ‹t = u›
using assms by (rule riesz_representation_unique)
theorem riesz_representation_cblinfun_norm:
includes notation_norm
fixes f::‹'a::chilbert_space ⇒⇩C⇩L complex›
assumes ‹⋀x. f *⇩V x = (t ∙⇩C x)›
shows ‹∥f∥ = ∥t∥›
using assms
proof transfer
fix f::‹'a ⇒ complex› and t
assume ‹bounded_clinear f› and ‹⋀x. f x = (t ∙⇩C x)›
from ‹⋀x. f x = (t ∙⇩C x)›
have ‹(norm (f x)) / (norm x) ≤ norm t›
for x
proof(cases ‹norm x = 0›)
case True
thus ?thesis by simp
next
case False
have ‹norm (f x) = norm ((t ∙⇩C x))›
using ‹⋀x. f x = (t ∙⇩C x)› by simp
also have ‹norm (t ∙⇩C x) ≤ norm t * norm x›
by (simp add: complex_inner_class.Cauchy_Schwarz_ineq2)
finally have ‹norm (f x) ≤ norm t * norm x›
by blast
thus ?thesis
by (metis False linordered_field_class.divide_right_mono nonzero_mult_div_cancel_right norm_ge_zero)
qed
moreover have ‹(norm (f t)) / (norm t) = norm t›
proof(cases ‹norm t = 0›)
case True
thus ?thesis
by simp
next
case False
have ‹f t = (t ∙⇩C t)›
using ‹⋀x. f x = (t ∙⇩C x)› by blast
also have ‹… = (norm t)^2›
by (meson cnorm_eq_square)
also have ‹… = (norm t)*(norm t)›
by (simp add: power2_eq_square)
finally have ‹f t = (norm t)*(norm t)›
by blast
thus ?thesis
by (metis ‹f t = t ∙⇩C t› norm_eq_sqrt_cinner norm_ge_zero real_div_sqrt)
qed
ultimately have ‹Sup {(norm (f x)) / (norm x)| x. True} = norm t›
by (smt cSup_eq_maximum mem_Collect_eq)
moreover have ‹Sup {(norm (f x)) / (norm x)| x. True} = (SUP x. (norm (f x)) / (norm x))›
by (simp add: full_SetCompr_eq)
ultimately show ‹onorm f = norm t›
by (simp add: onorm_def)
qed
definition the_riesz_rep :: ‹('a::chilbert_space ⇒⇩C⇩L complex) ⇒ 'a› where
‹the_riesz_rep f = (SOME t. ∀x. f *⇩V x = t ∙⇩C x)›
lemma the_riesz_rep[simp]: ‹the_riesz_rep f ∙⇩C x = f *⇩V x›
unfolding the_riesz_rep_def
apply (rule someI2_ex)
by (simp_all add: riesz_representation_cblinfun_existence)
lemma the_riesz_rep_unique:
assumes ‹⋀x. f *⇩V x = t ∙⇩C x›
shows ‹t = the_riesz_rep f›
using assms riesz_representation_cblinfun_unique the_riesz_rep by metis
lemma the_riesz_rep_scaleC: ‹the_riesz_rep (c *⇩C f) = cnj c *⇩C the_riesz_rep f›
apply (rule the_riesz_rep_unique[symmetric])
by auto
lemma the_riesz_rep_add: ‹the_riesz_rep (f + g) = the_riesz_rep f + the_riesz_rep g›
apply (rule the_riesz_rep_unique[symmetric])
by (auto simp: cinner_add_left cblinfun.add_left)
lemma the_riesz_rep_norm[simp]: ‹norm (the_riesz_rep f) = norm f›
apply (rule riesz_representation_cblinfun_norm[symmetric])
by simp
lemma bounded_antilinear_the_riesz_rep[bounded_antilinear]: ‹bounded_antilinear the_riesz_rep›
by (metis (no_types, opaque_lifting) bounded_antilinear_intro dual_order.refl mult.commute mult_1 the_riesz_rep_add the_riesz_rep_norm the_riesz_rep_scaleC)
lift_definition the_riesz_rep_sesqui :: ‹('a::complex_normed_vector ⇒ 'b::chilbert_space ⇒ complex) ⇒ ('a ⇒⇩C⇩L 'b)› is
‹λp. if bounded_sesquilinear p then the_riesz_rep o CBlinfun o p else 0›
by (metis (mono_tags, lifting) Cblinfun_comp_bounded_sesquilinear bounded_antilinear_o_bounded_antilinear' bounded_antilinear_the_riesz_rep bounded_clinear_0 fun.map_comp)
lemma the_riesz_rep_sesqui_apply:
assumes ‹bounded_sesquilinear p›
shows ‹(the_riesz_rep_sesqui p *⇩V x) ∙⇩C y = p x y›
apply (transfer fixing: p x y)
by (auto simp add: CBlinfun_inverse bounded_sesquilinear_apply_bounded_clinear assms)
subsection ‹Bidual›
lift_definition bidual_embedding :: ‹'a::complex_normed_vector ⇒⇩C⇩L (('a ⇒⇩C⇩L complex) ⇒⇩C⇩L complex)›
is ‹λx f. f *⇩V x›
by (simp add: cblinfun.flip)
lemma bidual_embedding_apply[simp]: ‹(bidual_embedding *⇩V x) *⇩V f = f *⇩V x›
by (transfer fixing: x f, simp)
lemma bidual_embedding_isometric[simp]: ‹norm (bidual_embedding *⇩V x) = norm x› for x :: ‹'a::complex_inner›
proof -
define f :: ‹'a ⇒⇩C⇩L complex› where ‹f = CBlinfun (λy. cinner x y)›
then have [simp]: ‹f *⇩V y = cinner x y› for y
by (simp add: bounded_clinear_CBlinfun_apply bounded_clinear_cinner_right)
then have [simp]: ‹norm f = norm x›
apply (auto intro!: norm_cblinfun_eqI[where x=x] simp: power2_norm_eq_cinner[symmetric])
apply (smt (verit, best) norm_eq_sqrt_cinner norm_ge_zero power2_norm_eq_cinner real_div_sqrt)
using Cauchy_Schwarz_ineq2 by blast
show ?thesis
apply (auto intro!: norm_cblinfun_eqI[where x=f])
apply (metis norm_eq_sqrt_cinner norm_imp_pos_and_ge real_div_sqrt)
by (metis norm_cblinfun ordered_field_class.sign_simps(33))
qed
lemma norm_bidual_embedding[simp]: ‹norm (bidual_embedding :: 'a::{complex_inner, not_singleton} ⇒⇩C⇩L _) = 1›
proof -
obtain x :: 'a where [simp]: ‹norm x = 1›
by (meson UNIV_not_singleton ex_norm1)
show ?thesis
by (auto intro!: norm_cblinfun_eqI[where x=x])
qed
lemma isometry_bidual_embedding[simp]: ‹isometry bidual_embedding›
by (simp add: norm_preserving_isometry)
lemma bidual_embedding_surj[simp]: ‹surj (bidual_embedding :: 'a::chilbert_space ⇒⇩C⇩L _)›
proof -
have ‹∃y''. ∀f. (bidual_embedding *⇩V y'') *⇩V f = y *⇩V f›
for y :: ‹('a ⇒⇩C⇩L complex) ⇒⇩C⇩L complex›
proof -
define y' where ‹y' = CBlinfun (λz. cnj (y (cblinfun_cinner_right z)))›
have y'_apply: ‹y' z = cnj (y (cblinfun_cinner_right z))› for z
unfolding y'_def
apply (subst CBlinfun_inverse)
by (auto intro!: bounded_linear_intros)
obtain y'' where ‹y' z = y'' ∙⇩C z› for z
using riesz_representation_cblinfun_existence by blast
then have y'': ‹z ∙⇩C y'' = cnj (y' z)› for z
by auto
have ‹(bidual_embedding *⇩V y'') *⇩V f = y *⇩V f› for f :: ‹'a ⇒⇩C⇩L complex›
proof -
obtain f' where f': ‹f z = f' ∙⇩C z› for z
using riesz_representation_cblinfun_existence by blast
then have f'2: ‹f = cblinfun_cinner_right f'›
using cblinfun_apply_inject by force
show ?thesis
by (auto simp add: f' f'2 y'' y'_apply)
qed
then show ?thesis
by blast
qed
then show ?thesis
by (metis cblinfun_eqI surj_def)
qed
subsection ‹Extension of complex bounded operators›
definition cblinfun_extension where
"cblinfun_extension S φ = (SOME B. ∀x∈S. B *⇩V x = φ x)"
definition cblinfun_extension_exists where
"cblinfun_extension_exists S φ = (∃B. ∀x∈S. B *⇩V x = φ x)"
lemma cblinfun_extension_existsI:
assumes "⋀x. x∈S ⟹ B *⇩V x = φ x"
shows "cblinfun_extension_exists S φ"
using assms cblinfun_extension_exists_def by blast
lemma cblinfun_extension_exists_finite_dim:
fixes φ::"'a::{complex_normed_vector,cfinite_dim} ⇒ 'b::complex_normed_vector"
assumes "cindependent S"
and "cspan S = UNIV"
shows "cblinfun_extension_exists S φ"
proof-
define f::"'a ⇒ 'b"
where "f = complex_vector.construct S φ"
have "clinear f"
by (simp add: complex_vector.linear_construct assms linear_construct f_def)
have "bounded_clinear f"
using ‹clinear f› assms by auto
then obtain B::"'a ⇒⇩C⇩L 'b"
where "B *⇩V x = f x" for x
using cblinfun_apply_cases by blast
have "B *⇩V x = φ x"
if c1: "x∈S"
for x
proof-
have "B *⇩V x = f x"
by (simp add: ‹⋀x. B *⇩V x = f x›)
also have "… = φ x"
using assms complex_vector.construct_basis f_def that
by (simp add: complex_vector.construct_basis)
finally show?thesis by blast
qed
thus ?thesis
unfolding cblinfun_extension_exists_def
by blast
qed
lemma cblinfun_extension_apply:
assumes "cblinfun_extension_exists S f"
and "v ∈ S"
shows "(cblinfun_extension S f) *⇩V v = f v"
by (smt assms cblinfun_extension_def cblinfun_extension_exists_def tfl_some)
lemma
fixes f :: ‹'a::complex_normed_vector ⇒ 'b::cbanach›
assumes ‹csubspace S›
assumes ‹closure S = UNIV›
assumes f_add: ‹⋀x y. x ∈ S ⟹ y ∈ S ⟹ f (x + y) = f x + f y›
assumes f_scale: ‹⋀c x y. x ∈ S ⟹ f (c *⇩C x) = c *⇩C f x›
assumes bounded: ‹⋀x. x ∈ S ⟹ norm (f x) ≤ B * norm x›
shows cblinfun_extension_exists_bounded_dense: ‹cblinfun_extension_exists S f›
and cblinfun_extension_norm_bounded_dense: ‹B ≥ 0 ⟹ norm (cblinfun_extension S f) ≤ B›
proof -
define B' where ‹B' = (if B≤0 then 1 else B)›
then have bounded': ‹⋀x. x ∈ S ⟹ norm (f x) ≤ B' * norm x›
using bounded by (metis mult_1 mult_le_0_iff norm_ge_zero order_trans)
have ‹B' > 0›
by (simp add: B'_def)
have ‹∃xi. (xi ⇢ x) ∧ (∀i. xi i ∈ S)› for x
using assms(2) closure_sequential by blast
then obtain seq :: ‹'a ⇒ nat ⇒ 'a› where seq_lim: ‹seq x ⇢ x› and seq_S: ‹seq x i ∈ S› for x i
apply (atomize_elim, subst all_conj_distrib[symmetric])
apply (rule choice)
by auto
define g where ‹g x = lim (λi. f (seq x i))› for x
have ‹Cauchy (λi. f (seq x i))› for x
proof (rule CauchyI)
fix e :: real assume ‹e > 0›
have ‹Cauchy (seq x)›
using LIMSEQ_imp_Cauchy seq_lim by blast
then obtain M where less_eB: ‹norm (seq x m - seq x n) < e/B'› if ‹n ≥ M› and ‹m ≥ M› for n m
by atomize_elim (meson CauchyD ‹0 < B'› ‹0 < e› linordered_field_class.divide_pos_pos)
have ‹norm (f (seq x m) - f (seq x n)) < e› if ‹n ≥ M› and ‹m ≥ M› for n m
proof -
have ‹norm (f (seq x m) - f (seq x n)) = norm (f (seq x m - seq x n))›
using f_add f_scale seq_S
by (metis add_diff_cancel assms(1) complex_vector.subspace_diff diff_add_cancel)
also have ‹… ≤ B' * norm (seq x m - seq x n)›
apply (rule bounded')
by (simp add: assms(1) complex_vector.subspace_diff seq_S)
also from less_eB have ‹… < B' * (e/B')›
by (meson ‹0 < B'› linordered_semiring_strict_class.mult_strict_left_mono that)
also have ‹… ≤ e›
using ‹0 < B'› by auto
finally show ?thesis
by -
qed
then show ‹∃M. ∀m≥M. ∀n≥M. norm (f (seq x m) - f (seq x n)) < e›
by auto
qed
then have f_seq_lim: ‹(λi. f (seq x i)) ⇢ g x› for x
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff g_def)
have f_xi_lim: ‹(λi. f (xi i)) ⇢ g x› if ‹xi ⇢ x› and ‹⋀i. xi i ∈ S› for xi x
proof -
from seq_lim that
have ‹(λi. B' * norm (xi i - seq x i)) ⇢ 0›
by (metis (no_types) ‹0 < B'› cancel_comm_monoid_add_class.diff_cancel norm_not_less_zero norm_zero tendsto_diff tendsto_norm_zero_iff tendsto_zero_mult_left_iff)
then have ‹(λi. f (xi i + (-1) *⇩C seq x i)) ⇢ 0›
apply (rule Lim_null_comparison[rotated])
using bounded' by (simp add: assms(1) complex_vector.subspace_diff seq_S that(2))
then have ‹(λi. f (xi i) - f (seq x i)) ⇢ 0›
apply (subst (asm) f_add)
apply (auto simp: that ‹csubspace S› complex_vector.subspace_neg seq_S)[2]
apply (subst (asm) f_scale)
by (auto simp: that ‹csubspace S› complex_vector.subspace_neg seq_S)
then show ‹(λi. f (xi i)) ⇢ g x›
using Lim_transform f_seq_lim by fastforce
qed
have g_add: ‹g (x + y) = g x + g y› for x y
proof -
obtain xi :: ‹nat ⇒ 'a› where ‹xi ⇢ x› and ‹xi i ∈ S› for i
using seq_S seq_lim by auto
obtain yi :: ‹nat ⇒ 'a› where ‹yi ⇢ y› and ‹yi i ∈ S› for i
using seq_S seq_lim by auto
have ‹(λi. xi i + yi i) ⇢ x + y›
using ‹xi ⇢ x› ‹yi ⇢ y› tendsto_add by blast
then have lim1: ‹(λi. f (xi i + yi i)) ⇢ g (x + y)›
by (simp add: ‹⋀i. xi i ∈ S› ‹⋀i. yi i ∈ S› assms(1) complex_vector.subspace_add f_xi_lim)
have ‹(λi. f (xi i + yi i)) = (λi. f (xi i) + f (yi i))›
by (simp add: ‹⋀i. xi i ∈ S› ‹⋀i. yi i ∈ S› f_add)
also have ‹… ⇢ g x + g y›
by (simp add: ‹⋀i. xi i ∈ S› ‹⋀i. yi i ∈ S› ‹xi ⇢ x› ‹yi ⇢ y› f_xi_lim tendsto_add)
finally show ?thesis
using lim1 LIMSEQ_unique by blast
qed
have g_scale: ‹g (c *⇩C x) = c *⇩C g x› for c x
proof -
obtain xi :: ‹nat ⇒ 'a› where ‹xi ⇢ x› and ‹xi i ∈ S› for i
using seq_S seq_lim by auto
have ‹(λi. c *⇩C xi i) ⇢ c *⇩C x›
using ‹xi ⇢ x› bounded_clinear_scaleC_right clinear_continuous_at isCont_tendsto_compose by blast
then have lim1: ‹(λi. f (c *⇩C xi i)) ⇢ g (c *⇩C x)›
by (simp add: ‹⋀i. xi i ∈ S› assms(1) complex_vector.subspace_scale f_xi_lim)
have ‹(λi. f (c *⇩C xi i)) = (λi. c *⇩C f (xi i))›
by (simp add: ‹⋀i. xi i ∈ S› f_scale)
also have ‹… ⇢ c *⇩C g x›
using ‹⋀i. xi i ∈ S› ‹xi ⇢ x› bounded_clinear_scaleC_right clinear_continuous_at f_xi_lim isCont_tendsto_compose by blast
finally show ?thesis
using lim1 LIMSEQ_unique by blast
qed
have [simp]: ‹f x = g x› if ‹x ∈ S› for x
proof -
have ‹(λ_. x) ⇢ x›
by auto
then have ‹(λ_. f x) ⇢ g x›
using that by (rule f_xi_lim)
then show ‹f x = g x›
by (simp add: LIMSEQ_const_iff)
qed
have g_bounded: ‹norm (g x) ≤ B' * norm x› for x
proof -
obtain xi :: ‹nat ⇒ 'a› where ‹xi ⇢ x› and ‹xi i ∈ S› for i
using seq_S seq_lim by auto
then have ‹(λi. f (xi i)) ⇢ g x›
using f_xi_lim by presburger
then have ‹(λi. norm (f (xi i))) ⇢ norm (g x)›
by (metis tendsto_norm)
moreover have ‹(λi. B' * norm (xi i)) ⇢ B' * norm x›
by (simp add: ‹xi ⇢ x› tendsto_mult_left tendsto_norm)
ultimately show ‹norm (g x) ≤ B' * norm x›
apply (rule lim_mono[rotated])
using bounded' using ‹xi _ ∈ S› by blast
qed
have ‹bounded_clinear g›
using g_add g_scale apply (rule bounded_clinearI[where K=B'])
using g_bounded by (simp add: ordered_field_class.sign_simps(5))
then have [simp]: ‹CBlinfun g *⇩V x = g x› for x
by (subst CBlinfun_inverse, auto)
show ‹cblinfun_extension_exists S f›
apply (rule cblinfun_extension_existsI[where B=‹CBlinfun g›])
by auto
then have ‹cblinfun_extension S f *⇩V ψ = CBlinfun g *⇩V ψ› if ‹ψ ∈ S› for ψ
by (simp add: cblinfun_extension_apply that)
then have ext_is_g: ‹(*⇩V) (cblinfun_extension S f) = g›
apply (rule_tac ext)
apply (rule on_closure_eqI[where S=S])
using ‹closure S = UNIV› ‹bounded_clinear g›
by (auto simp add: continuous_at_imp_continuous_on clinear_continuous_within)
show ‹norm (cblinfun_extension S f) ≤ B› if ‹B ≥ 0›
proof (cases ‹B > 0›)
case True
then have ‹B = B'›
unfolding B'_def
by auto
moreover have *: ‹norm (cblinfun_extension S f) ≤ B'›
by (metis ext_is_g ‹0 < B'› g_bounded norm_cblinfun_bound order_le_less)
ultimately show ?thesis
by simp
next
case False
with bounded have ‹f x = 0› if ‹x ∈ S› for x
by (smt (verit) mult_nonpos_nonneg norm_ge_zero norm_le_zero_iff that)
then have ‹g x = (λ_. 0) x› if ‹x ∈ S› for x
using that by simp
then have ‹g x = 0› for x
apply (rule on_closure_eqI[where S=S])
using ‹closure S = UNIV› ‹bounded_clinear g›
by (auto simp add: continuous_at_imp_continuous_on clinear_continuous_within)
with ext_is_g have ‹cblinfun_extension S f = 0›
by (simp add: cblinfun_eqI)
then show ?thesis
using that by simp
qed
qed
lemma cblinfun_extension_cong:
assumes ‹cspan A = cspan B›
assumes ‹B ⊆ A›
assumes fg: ‹⋀x. x∈B ⟹ f x = g x›
assumes ‹cblinfun_extension_exists A f›
shows ‹cblinfun_extension A f = cblinfun_extension B g›
proof -
from ‹cblinfun_extension_exists A f› fg ‹B ⊆ A›
have ‹cblinfun_extension_exists B g›
by (metis assms(2) cblinfun_extension_exists_def subset_eq)
have ‹(∀x∈A. C *⇩V x = f x) ⟷ (∀x∈B. C *⇩V x = f x)› for C
by (smt (verit, ccfv_SIG) assms(1) assms(2) assms(4) cblinfun_eq_on_span cblinfun_extension_exists_def complex_vector.span_eq subset_iff)
also from fg have ‹… C ⟷ (∀x∈B. C *⇩V x = g x)› for C
by auto
finally show ‹cblinfun_extension A f = cblinfun_extension B g›
unfolding cblinfun_extension_def
by auto
qed
lemma
fixes f :: ‹'a::complex_inner ⇒ 'b::chilbert_space› and S
assumes ‹is_ortho_set S› and ‹closure (cspan S) = UNIV›
assumes ortho_f: ‹⋀x y. x∈S ⟹ y∈S ⟹ x≠y ⟹ is_orthogonal (f x) (f y)›
assumes bounded: ‹⋀x. x ∈ S ⟹ norm (f x) ≤ B * norm x›
shows cblinfun_extension_exists_ortho: ‹cblinfun_extension_exists S f›
and cblinfun_extension_exists_ortho_norm: ‹B ≥ 0 ⟹ norm (cblinfun_extension S f) ≤ B›
proof -
define g where ‹g = cconstruct S f›
have ‹cindependent S›
using assms(1) is_ortho_set_cindependent by blast
have g_f: ‹g x = f x› if ‹x∈S› for x
unfolding g_def using ‹cindependent S› that by (rule complex_vector.construct_basis)
have [simp]: ‹clinear g›
unfolding g_def using ‹cindependent S› by (rule complex_vector.linear_construct)
then have g_add: ‹g (x + y) = g x + g y› if ‹x ∈ cspan S› and ‹y ∈ cspan S› for x y
using clinear_iff by blast
from ‹clinear g› have g_scale: ‹g (c *⇩C x) = c *⇩C g x› if ‹x ∈ cspan S› for x c
by (simp add: complex_vector.linear_scale)
moreover have g_bounded: ‹norm (g x) ≤ abs B * norm x› if ‹x ∈ cspan S› for x
proof -
from that obtain t r where x_sum: ‹x = (∑a∈t. r a *⇩C a)› and ‹finite t› and ‹t ⊆ S›
unfolding complex_vector.span_explicit by auto
have ‹(norm (g x))⇧2 = (norm (∑a∈t. r a *⇩C g a))⇧2›
by (simp add: x_sum complex_vector.linear_sum clinear.scaleC)
also have ‹… = (norm (∑a∈t. r a *⇩C f a))⇧2›
by (smt (verit) ‹t ⊆ S› g_f in_mono sum.cong)
also have ‹… = (∑a∈t. (norm (r a *⇩C f a))⇧2)›
using _ ‹finite t› apply (rule pythagorean_theorem_sum)
using ‹t ⊆ S› ortho_f in_mono by fastforce
also have ‹… = (∑a∈t. (cmod (r a) * norm (f a))⇧2)›
by simp
also have ‹… ≤ (∑a∈t. (cmod (r a) * B * norm a)⇧2)›
apply (rule sum_mono)
by (metis ‹t ⊆ S› assms(4) in_mono mult_left_mono mult_nonneg_nonneg norm_ge_zero power_mono vector_space_over_itself.scale_scale)
also have ‹… = B⇧2 * (∑a∈t. (norm (r a *⇩C a))⇧2)›
by (simp add: sum_distrib_left mult.commute vector_space_over_itself.scale_left_commute flip: power_mult_distrib)
also have ‹… = B⇧2 * (norm (∑a∈t. (r a *⇩C a)))⇧2›
apply (subst pythagorean_theorem_sum)
using ‹finite t› by auto (meson ‹t ⊆ S› assms(1) is_ortho_set_def subsetD)
also have ‹… = (abs B * norm x)⇧2›
by (simp add: power_mult_distrib x_sum)
finally show ‹norm (g x) ≤ abs B * norm x›
by auto
qed
from g_add g_scale g_bounded
have extg_exists: ‹cblinfun_extension_exists (cspan S) g›
apply (rule_tac cblinfun_extension_exists_bounded_dense[where B=‹abs B›])
using ‹closure (cspan S) = UNIV› by auto
then show ‹cblinfun_extension_exists S f›
by (metis (mono_tags, opaque_lifting) g_f cblinfun_extension_apply cblinfun_extension_existsI complex_vector.span_base)
have norm_extg: ‹norm (cblinfun_extension (cspan S) g) ≤ B› if ‹B ≥ 0›
apply (rule cblinfun_extension_norm_bounded_dense)
using g_add g_scale g_bounded ‹closure (cspan S) = UNIV› that by auto
have extg_extf: ‹cblinfun_extension (cspan S) g = cblinfun_extension S f›
apply (rule cblinfun_extension_cong)
by (auto simp add: complex_vector.span_base g_f extg_exists)
from norm_extg extg_extf
show ‹norm (cblinfun_extension S f) ≤ B› if ‹B ≥ 0›
using that by simp
qed
lemma cblinfun_extension_exists_proj:
fixes f :: ‹'a::complex_normed_vector ⇒ 'b::cbanach›
assumes ‹csubspace S›
assumes ex_P: ‹∃P :: 'a ⇒⇩C⇩L 'a. is_Proj P ∧ range P = closure S›
assumes f_add: ‹⋀x y. x ∈ S ⟹ y ∈ S ⟹ f (x + y) = f x + f y›
assumes f_scale: ‹⋀c x y. x ∈ S ⟹ f (c *⇩C x) = c *⇩C f x›
assumes bounded: ‹⋀x. x ∈ S ⟹ norm (f x) ≤ B * norm x›
shows ‹cblinfun_extension_exists S f›
proof (cases ‹B ≥ 0›)
case True
note True[simp]
obtain P :: ‹'a ⇒⇩C⇩L 'a› where P_proj: ‹is_Proj P› and P_im: ‹range P = closure S›
using ex_P by blast
define f' S' where ‹f' ψ = f (P ψ)› and ‹S' = S + space_as_set (kernel P)› for ψ
have PS': ‹P *⇩V x ∈ S› if ‹x ∈ S'› for x
proof -
obtain x1 x2 where x12: ‹x = x1 + x2› and x1: ‹x1 ∈ S› and x2: ‹x2 ∈ space_as_set (kernel P)›
using that S'_def ‹x ∈ S'› set_plus_elim by blast
have ‹P *⇩V x = P *⇩V x1›
using x2 by (simp add: x12 cblinfun.add_right kernel_memberD)
also have ‹… = x1›
by (metis (no_types, opaque_lifting) P_im P_proj cblinfun_apply_cblinfun_compose closure_insert image_iff insertI1 insert_absorb is_Proj_idempotent x1)
also have ‹… ∈ S›
by (fact x1)
finally show ?thesis
by -
qed
have SS': ‹S ⊆ S'›
by (metis S'_def ordered_field_class.sign_simps(2) set_zero_plus2 zero_space_as_set)
have ‹csubspace S'›
by (simp add: S'_def assms(1) csubspace_set_plus)
moreover have ‹closure S' = UNIV›
proof auto
fix ψ
have ‹ψ = P ψ + (id - P) ψ›
by simp
also have ‹… ∈ closure S + space_as_set (kernel P)›
by (smt (verit) P_im P_proj calculation cblinfun.real.add_right eq_add_iff is_Proj_idempotent kernel_memberI rangeI set_plus_intro simp_a_oCL_b')
also have ‹… ⊆ closure (closure S + space_as_set (kernel P))›
using closure_subset by blast
also have ‹… = closure (S + space_as_set (kernel P))›
using closed_sum_closure_left closed_sum_def by blast
also have ‹… = closure S'›
using S'_def by fastforce
finally show ‹ψ ∈ closure S'›
by -
qed
moreover have ‹f' (x + y) = f' x + f' y› if ‹x ∈ S'› and ‹y ∈ S'› for x y
using that by (auto simp: f'_def cblinfun.add_right f_add PS')
moreover have ‹f' (c *⇩C x) = c *⇩C f' x› if ‹x ∈ S'› for c x
using that by (auto simp: f'_def cblinfun.scaleC_right f_scale PS')
moreover
have ‹norm (f' x) ≤ (B * norm P) * norm x› if ‹x ∈ S'› for x
proof -
have ‹norm (f' x) ≤ B* norm (P x)›
by (auto simp: f'_def PS' bounded that)
also have ‹… ≤ B * norm P * norm x›
by (simp add: mult.assoc mult_left_mono norm_cblinfun)
finally show ?thesis
by auto
qed
ultimately have F_ex: ‹cblinfun_extension_exists S' f'›
by (rule cblinfun_extension_exists_bounded_dense)
define F where ‹F = cblinfun_extension S' f'›
have ‹F ψ = f ψ› if ‹ψ ∈ S› for ψ
proof -
from F_ex that SS' have ‹F ψ = f' ψ›
by (auto simp add: F_def cblinfun_extension_apply)
also have ‹… = f (P *⇩V ψ)›
by (simp add: f'_def)
also have ‹… = f ψ›
using P_proj P_im
apply (transfer fixing: ψ S f)
by (metis closure_subset in_mono is_projection_on_fixes_image is_projection_on_image that)
finally show ?thesis
by -
qed
then show ‹cblinfun_extension_exists S f›
using cblinfun_extension_exists_def by blast
next
case False
then have ‹S ⊆ {0}›
using bounded by auto (meson norm_ge_zero norm_le_zero_iff order_trans zero_le_mult_iff)
then show ‹cblinfun_extension_exists S f›
apply (rule_tac cblinfun_extension_existsI[where B=0])
apply auto
using bounded by fastforce
qed
lemma cblinfun_extension_exists_hilbert:
fixes f :: ‹'a::chilbert_space ⇒ 'b::cbanach›
assumes ‹csubspace S›
assumes f_add: ‹⋀x y. x ∈ S ⟹ y ∈ S ⟹ f (x + y) = f x + f y›
assumes f_scale: ‹⋀c x y. x ∈ S ⟹ f (c *⇩C x) = c *⇩C f x›
assumes bounded: ‹⋀x. x ∈ S ⟹ norm (f x) ≤ B * norm x›
shows ‹cblinfun_extension_exists S f›
proof -
have ‹∃P. is_Proj P ∧ range ((*⇩V) P) = closure S›
apply (rule exI[of _ ‹Proj (ccspan S)›])
apply (rule conjI)
by simp (metis Proj_is_Proj Proj_range Proj_range_closed assms(1) cblinfun_image.rep_eq ccspan.rep_eq closure_closed complex_vector.span_eq_iff space_as_set_top)
from assms(1) this assms(2-4)
show ?thesis
by (rule cblinfun_extension_exists_proj)
qed
lemma cblinfun_extension_exists_restrict:
assumes ‹B ⊆ A›
assumes ‹⋀x. x∈B ⟹ f x = g x›
assumes ‹cblinfun_extension_exists A f›
shows ‹cblinfun_extension_exists B g›
by (metis assms cblinfun_extension_exists_def subset_eq)
subsection ‹Bijections between different ONBs›
text ‹Some of the theorems here logically belong into \<^theory>‹Complex_Bounded_Operators.Complex_Inner_Product›
but the proof uses some concepts from the present theory.›
lemma all_ortho_bases_same_card:
fixes E F :: ‹'a::chilbert_space set›
assumes ‹is_ortho_set E› ‹is_ortho_set F› ‹ccspan E = ⊤› ‹ccspan F = ⊤›
shows ‹∃f. bij_betw f E F›
proof -
have ‹|F| ≤o |E|› if ‹infinite E› and
‹is_ortho_set E› ‹is_ortho_set F› ‹ccspan E = top› ‹ccspan F = top› for E F :: ‹'a set›
proof -
define F' where ‹F' e = {f∈F. ¬ is_orthogonal f e}› for e
have ‹∃e∈E. cinner f e ≠ 0› if ‹f ∈ F› for f
proof (rule ccontr, simp)
assume ‹∀e∈E. is_orthogonal f e›
then have ‹f ∈ orthogonal_complement E›
by (simp add: orthogonal_complementI)
also have ‹… = orthogonal_complement (closure (cspan E))›
using orthogonal_complement_of_closure orthogonal_complement_of_cspan by blast
also have ‹… = space_as_set (- ccspan E)›
by transfer simp
also have ‹… = space_as_set (- top)›
by (simp add: ‹ccspan E = top›)
also have ‹… = {0}›
by (auto simp add: top_ccsubspace.rep_eq uminus_ccsubspace.rep_eq)
finally have ‹f = 0›
by simp
with ‹f ∈ F› ‹is_ortho_set F› show False
by (simp add: is_onb_def is_ortho_set_def)
qed
then have F'_union: ‹F = (⋃e∈E. F' e)›
unfolding F'_def by auto
have ‹countable (F' e)› for e
proof -
have ‹(∑f∈M. (cmod (cinner (sgn f) e))⇧2) ≤ (norm e)⇧2› if ‹finite M› and ‹M ⊆ F› for M
proof -
have [simp]: ‹is_ortho_set M›
using ‹is_ortho_set F› is_ortho_set_antimono that(2) by blast
have [simp]: ‹norm (sgn f) = 1› if ‹f ∈ M› for f
by (metis ‹is_ortho_set M› is_ortho_set_def norm_sgn that)
have ‹(∑f∈M. (cmod (cinner (sgn f) e))⇧2) = (∑f∈M. (norm ((cinner (sgn f) e) *⇩C sgn f))⇧2)›
apply (rule sum.cong[OF refl])
by simp
also have ‹… = (norm (∑f∈M. ((cinner (sgn f) e) *⇩C sgn f)))⇧2›
apply (rule pythagorean_theorem_sum[symmetric])
using that by auto (meson ‹is_ortho_set M› is_ortho_set_def)
also have ‹… = (norm (∑f∈M. proj f e))⇧2›
by (metis butterfly_apply butterfly_sgn_eq_proj)
also have ‹… = (norm (Proj (ccspan M) e))⇧2›
apply (rule arg_cong[where f=‹λx. (norm x)⇧2›])
using ‹finite M› ‹is_ortho_set M› apply induction
by simp (smt (verit, ccfv_threshold) Proj_orthog_ccspan_insert insertCI is_ortho_set_def plus_cblinfun.rep_eq sum.insert)
also have ‹… ≤ (norm (Proj (ccspan M)) * norm e)⇧2›
by (auto simp: norm_cblinfun intro!: power_mono)
also have ‹… ≤ (norm e)⇧2›
apply (rule power_mono)
apply (metis norm_Proj_leq1 mult_left_le_one_le norm_ge_zero)
by simp
finally show ?thesis
by -
qed
then have ‹(λf. (cmod (cinner (sgn f) e))⇧2) abs_summable_on F›
apply (intro nonneg_bdd_above_summable_on bdd_aboveI)
by auto
then have ‹countable {f ∈ F. (cmod (sgn f ∙⇩C e))⇧2 ≠ 0}›
by (rule abs_summable_countable)
then have ‹countable {f ∈ F. ¬ is_orthogonal (sgn f) e}›
by force
then have ‹countable {f ∈ F. ¬ is_orthogonal f e}›
by force
then show ?thesis
unfolding F'_def by simp
qed
then have F'_leq: ‹|F' e| ≤o natLeq› for e
using countable_leq_natLeq by auto
from F'_union have ‹|F| ≤o |Sigma E F'|› (is ‹_ ≤o …›)
using card_of_UNION_Sigma by blast
also have ‹… ≤o |E × (UNIV::nat set)|› (is ‹_ ≤o …›)
apply (rule card_of_Sigma_mono1)
using F'_leq
using card_of_nat ordIso_symmetric ordLeq_ordIso_trans by blast
also have ‹… =o |E| *c natLeq› (is ‹ordIso2 _ …›)
by (metis Field_card_of Field_natLeq card_of_ordIso_subst cprod_def)
also have ‹… =o |E|›
apply (rule card_prod_omega)
using that by (simp add: cinfinite_def)
finally show ‹|F| ≤o |E|›
by -
qed
then have infinite: ‹|E| =o |F|› if ‹infinite E› and ‹infinite F›
by (simp add: assms ordIso_iff_ordLeq that(1) that(2))
have ‹|E| =o |F|› if ‹finite E› and ‹is_ortho_set E› ‹is_ortho_set F› ‹ccspan E = top› ‹ccspan F = top›
for E F :: ‹'a set›
proof -
have ‹card E = card F›
using that
by (metis bij_betw_same_card ccspan.rep_eq closure_finite_cspan complex_vector.bij_if_span_eq_span_bases
complex_vector.independent_span_bound is_ortho_set_cindependent top_ccsubspace.rep_eq top_greatest)
with ‹finite E› have ‹finite F›
by (metis ccspan.rep_eq closure_finite_cspan complex_vector.independent_span_bound is_ortho_set_cindependent that(3) that(4) top_ccsubspace.rep_eq top_greatest)
with ‹card E = card F› that show ?thesis
apply (rule_tac finite_card_of_iff_card[THEN iffD2])
by auto
qed
with infinite assms have ‹|E| =o |F|›
by (meson ordIso_symmetric)
then show ?thesis
by (simp add: card_of_ordIso)
qed
lemma all_onbs_same_card:
fixes E F :: ‹'a::chilbert_space set›
assumes ‹is_onb E› ‹is_onb F›
shows ‹∃f. bij_betw f E F›
apply (rule all_ortho_bases_same_card)
using assms by (auto simp: is_onb_def)
definition bij_between_bases where ‹bij_between_bases E F = (SOME f. bij_betw f E F)› for E F :: ‹'a::chilbert_space set›
lemma bij_between_bases_bij:
fixes E F :: ‹'a::chilbert_space set›
assumes ‹is_onb E› ‹is_onb F›
shows ‹bij_betw (bij_between_bases E F) E F›
using all_onbs_same_card
by (metis assms(1) assms(2) bij_between_bases_def someI)
definition unitary_between where ‹unitary_between E F = cblinfun_extension E (bij_between_bases E F)›
lemma unitary_between_apply:
fixes E F :: ‹'a::chilbert_space set›
assumes ‹is_onb E› ‹is_onb F› ‹e ∈ E›
shows ‹unitary_between E F *⇩V e = bij_between_bases E F e›
proof -
from ‹is_onb E› ‹is_onb F›
have EF: ‹bij_between_bases E F e ∈ F› if ‹e ∈ E› for e
by (meson bij_betwE bij_between_bases_bij that)
have ortho: ‹is_orthogonal (bij_between_bases E F x) (bij_between_bases E F y)› if ‹x ≠ y› and ‹x ∈ E› and ‹y ∈ E› for x y
by (smt (verit, del_insts) assms(1) assms(2) bij_betw_iff_bijections bij_between_bases_bij is_onb_def is_ortho_set_def that(1) that(2) that(3))
have spanE: ‹closure (cspan E) = UNIV›
by (metis assms(1) ccspan.rep_eq is_onb_def top_ccsubspace.rep_eq)
show ?thesis
unfolding unitary_between_def
apply (rule cblinfun_extension_apply)
apply (rule cblinfun_extension_exists_ortho[where B=1])
using assms EF ortho spanE
by (auto simp: is_onb_def)
qed
lemma unitary_between_unitary:
fixes E F :: ‹'a::chilbert_space set›
assumes ‹is_onb E› ‹is_onb F›
shows ‹unitary (unitary_between E F)›
proof -
have ‹(unitary_between E F *⇩V b) ∙⇩C (unitary_between E F *⇩V c) = b ∙⇩C c› if ‹b ∈ E› and ‹c ∈ E› for b c
proof (cases ‹b = c›)
case True
from ‹is_onb E› that have 1: ‹b ∙⇩C b = 1›
using cnorm_eq_1 is_onb_def by blast
from that have ‹unitary_between E F *⇩V b ∈ F›
by (metis assms(1) assms(2) bij_betw_apply bij_between_bases_bij unitary_between_apply)
with ‹is_onb F› have 2: ‹(unitary_between E F *⇩V b) ∙⇩C (unitary_between E F *⇩V b) = 1›
by (simp add: cnorm_eq_1 is_onb_def)
from 1 2 True show ?thesis
by simp
next
case False
from ‹is_onb E› that have 1: ‹b ∙⇩C c = 0›
by (simp add: False is_onb_def is_ortho_set_def)
from that have inF: ‹unitary_between E F *⇩V b ∈ F› ‹unitary_between E F *⇩V c ∈ F›
by (metis assms(1) assms(2) bij_betw_apply bij_between_bases_bij unitary_between_apply)+
have neq: ‹unitary_between E F *⇩V b ≠ unitary_between E F *⇩V c›
by (metis (no_types, lifting) False assms(1) assms(2) bij_betw_iff_bijections bij_between_bases_bij that(1) that(2) unitary_between_apply)
from inF neq ‹is_onb F› have 2: ‹(unitary_between E F *⇩V b) ∙⇩C (unitary_between E F *⇩V c) = 0›
by (simp add: is_onb_def is_ortho_set_def)
from 1 2 show ?thesis
by simp
qed
then have iso: ‹isometry (unitary_between E F)›
apply (rule_tac orthogonal_on_basis_is_isometry[where B=E])
using assms(1) is_onb_def by auto
have ‹unitary_between E F *⇩S top = unitary_between E F *⇩S ccspan E›
by (metis assms(1) is_onb_def)
also have ‹… ≥ ccspan (unitary_between E F ` E)› (is ‹_ ≥ …›)
by (simp add: cblinfun_image_ccspan)
also have ‹… = ccspan (bij_between_bases E F ` E)›
by (metis assms(1) assms(2) image_cong unitary_between_apply)
also have ‹… = ccspan F›
by (metis assms(1) assms(2) bij_betw_imp_surj_on bij_between_bases_bij)
also have ‹… = top›
using assms(2) is_onb_def by blast
finally have surj: ‹unitary_between E F *⇩S top = top›
by (simp add: top.extremum_unique)
from iso surj show ?thesis
by (rule surj_isometry_is_unitary)
qed
subsection ‹Notation›
bundle cblinfun_notation begin
notation cblinfun_compose (infixl "o⇩C⇩L" 67)
notation cblinfun_apply (infixr "*⇩V" 70)
notation cblinfun_image (infixr "*⇩S" 70)
notation adj ("_*" [99] 100)
type_notation cblinfun ("(_ ⇒⇩C⇩L /_)" [22, 21] 21)
end
bundle no_cblinfun_notation begin
no_notation cblinfun_compose (infixl "o⇩C⇩L" 67)
no_notation cblinfun_apply (infixr "*⇩V" 70)
no_notation cblinfun_image (infixr "*⇩S" 70)
no_notation adj ("_*" [99] 100)
no_type_notation cblinfun ("(_ ⇒⇩C⇩L /_)" [22, 21] 21)
end
unbundle no_cblinfun_notation
unbundle no_lattice_syntax
end