section ‹‹Complex_Vector_Spaces› -- Complex Vector Spaces› (* Authors: Dominique Unruh, University of Tartu, unruh@ut.ee Jose Manuel Rodriguez Caballero, University of Tartu, jose.manuel.rodriguez.caballero@ut.ee *) theory Complex_Vector_Spaces imports "HOL-Analysis.Elementary_Topology" "HOL-Analysis.Operator_Norm" "HOL-Analysis.Elementary_Normed_Spaces" "HOL-Library.Set_Algebras" "HOL-Analysis.Starlike" "HOL-Types_To_Sets.Types_To_Sets" "Complex_Bounded_Operators.Extra_Vector_Spaces" "Complex_Bounded_Operators.Extra_Ordered_Fields" "HOL-Library.Complemented_Lattices" "Complex_Bounded_Operators.Extra_General" Complex_Vector_Spaces0 begin bundle notation_norm begin notation norm ("∥_∥") end unbundle lattice_syntax subsection ‹Misc› lemma (in scaleC) scaleC_real: assumes "r∈ℝ" shows "r *⇩_{C}x = Re r *⇩_{R}x" unfolding scaleR_scaleC using assms by simp lemma of_complex_of_real_eq [simp]: "of_complex (of_real n) = of_real n" unfolding of_complex_def of_real_def unfolding scaleR_scaleC by simp lemma Complexs_of_real [simp]: "of_real r ∈ ℂ" unfolding Complexs_def of_real_def of_complex_def apply (subst scaleR_scaleC) by simp lemma Reals_in_Complexs: "ℝ ⊆ ℂ" unfolding Reals_def by auto lemma (in clinear) "linear f" apply standard by (simp_all add: add scaleC scaleR_scaleC) lemma (in bounded_clinear) bounded_linear: "bounded_linear f" by (simp add: add bounded bounded_linear.intro bounded_linear_axioms.intro linearI scaleC scaleR_scaleC) lemma clinear_times: "clinear (λx. c * x)" for c :: "'a::complex_algebra" by (auto simp: clinearI distrib_left) lemma (in clinear) linear: shows ‹linear f› by (simp add: add linearI scaleC scaleR_scaleC) lemma bounded_clinearI: assumes ‹⋀b1 b2. f (b1 + b2) = f b1 + f b2› assumes ‹⋀r b. f (r *⇩_{C}b) = r *⇩_{C}f b› assumes ‹∀x. norm (f x) ≤ norm x * K› shows "bounded_clinear f" using assms by (auto intro!: exI bounded_clinear.intro clinearI simp: bounded_clinear_axioms_def) lemma bounded_clinear_id[simp]: ‹bounded_clinear id› by (simp add: id_def) (* The following would be a natural inclusion of locales, but unfortunately it leads to name conflicts upon interpretation of bounded_cbilinear *) (* sublocale bounded_cbilinear ⊆ bounded_bilinear by (rule bounded_bilinear) *) definition cbilinear :: ‹('a::complex_vector ⇒ 'b::complex_vector ⇒ 'c::complex_vector) ⇒ bool› where ‹cbilinear = (λ f. (∀ y. clinear (λ x. f x y)) ∧ (∀ x. clinear (λ y. f x y)) )› lemma cbilinear_add_left: assumes ‹cbilinear f› shows ‹f (a + b) c = f a c + f b c› by (smt (verit, del_insts) assms cbilinear_def complex_vector.linear_add) lemma cbilinear_add_right: assumes ‹cbilinear f› shows ‹f a (b + c) = f a b + f a c› by (smt (verit, del_insts) assms cbilinear_def complex_vector.linear_add) lemma cbilinear_times: fixes g' :: ‹'a::complex_vector ⇒ complex› and g :: ‹'b::complex_vector ⇒ complex› assumes ‹⋀ x y. h x y = (g' x)*(g y)› and ‹clinear g› and ‹clinear g'› shows ‹cbilinear h› proof - have w1: "h (b1 + b2) y = h b1 y + h b2 y" for b1 :: 'a and b2 :: 'a and y proof- have ‹h (b1 + b2) y = g' (b1 + b2) * g y› using ‹⋀ x y. h x y = (g' x)*(g y)› by auto also have ‹… = (g' b1 + g' b2) * g y› using ‹clinear g'› unfolding clinear_def by (simp add: assms(3) complex_vector.linear_add) also have ‹… = g' b1 * g y + g' b2 * g y› by (simp add: ring_class.ring_distribs(2)) also have ‹… = h b1 y + h b2 y› using assms(1) by auto finally show ?thesis by blast qed have w2: "h (r *⇩_{C}b) y = r *⇩_{C}h b y" for r :: complex and b :: 'a and y proof- have ‹h (r *⇩_{C}b) y = g' (r *⇩_{C}b) * g y› by (simp add: assms(1)) also have ‹… = r *⇩_{C}(g' b * g y)› by (simp add: assms(3) complex_vector.linear_scale) also have ‹… = r *⇩_{C}(h b y)› by (simp add: assms(1)) finally show ?thesis by blast qed have "clinear (λx. h x y)" for y :: 'b unfolding clinear_def by (meson clinearI clinear_def w1 w2) hence t2: "∀y. clinear (λx. h x y)" by simp have v1: "h x (b1 + b2) = h x b1 + h x b2" for b1 :: 'b and b2 :: 'b and x proof- have ‹h x (b1 + b2) = g' x * g (b1 + b2)› using ‹⋀ x y. h x y = (g' x)*(g y)› by auto also have ‹… = g' x * (g b1 + g b2)› using ‹clinear g'› unfolding clinear_def by (simp add: assms(2) complex_vector.linear_add) also have ‹… = g' x * g b1 + g' x * g b2› by (simp add: ring_class.ring_distribs(1)) also have ‹… = h x b1 + h x b2› using assms(1) by auto finally show ?thesis by blast qed have v2: "h x (r *⇩_{C}b) = r *⇩_{C}h x b" for r :: complex and b :: 'b and x proof- have ‹h x (r *⇩_{C}b) = g' x * g (r *⇩_{C}b)› by (simp add: assms(1)) also have ‹… = r *⇩_{C}(g' x * g b)› by (simp add: assms(2) complex_vector.linear_scale) also have ‹… = r *⇩_{C}(h x b)› by (simp add: assms(1)) finally show ?thesis by blast qed have "Vector_Spaces.linear (*⇩_{C}) (*⇩_{C}) (h x)" for x :: 'a using v1 v2 by (meson clinearI clinear_def) hence t1: "∀x. clinear (h x)" unfolding clinear_def by simp show ?thesis unfolding cbilinear_def by (simp add: t1 t2) qed lemma csubspace_is_subspace: "csubspace A ⟹ subspace A" apply (rule subspaceI) by (auto simp: complex_vector.subspace_def scaleR_scaleC) lemma span_subset_cspan: "span A ⊆ cspan A" unfolding span_def complex_vector.span_def by (simp add: csubspace_is_subspace hull_antimono) lemma cindependent_implies_independent: assumes "cindependent (S::'a::complex_vector set)" shows "independent S" using assms unfolding dependent_def complex_vector.dependent_def using span_subset_cspan by blast lemma cspan_singleton: "cspan {x} = {α *⇩_{C}x| α. True}" proof - have ‹cspan {x} = {y. y∈cspan {x}}› by auto also have ‹… = {α *⇩_{C}x| α. True}› apply (subst complex_vector.span_breakdown_eq) by auto finally show ?thesis by - qed lemma cspan_as_span: "cspan (B::'a::complex_vector set) = span (B ∪ scaleC 𝗂 ` B)" proof auto let ?cspan = complex_vector.span let ?rspan = real_vector.span fix ψ assume cspan: "ψ ∈ ?cspan B" have "∃B' r. finite B' ∧ B' ⊆ B ∧ ψ = (∑b∈B'. r b *⇩_{C}b)" using complex_vector.span_explicit[of B] cspan by auto then obtain B' r where "finite B'" and "B' ⊆ B" and ψ_explicit: "ψ = (∑b∈B'. r b *⇩_{C}b)" by atomize_elim define R where "R = B ∪ scaleC 𝗂 ` B" have x2: "(case x of (b, i) ⇒ if i then Im (r b) *⇩_{R}𝗂 *⇩_{C}b else Re (r b) *⇩_{R}b) ∈ span (B ∪ (*⇩_{C}) 𝗂 ` B)" if "x ∈ B' × (UNIV::bool set)" for x :: "'a × bool" using that ‹B' ⊆ B› by (auto simp add: real_vector.span_base real_vector.span_scale subset_iff) have x1: "ψ = (∑x∈B'. ∑i∈UNIV. if i then Im (r x) *⇩_{R}𝗂 *⇩_{C}x else Re (r x) *⇩_{R}x)" if "⋀b. r b *⇩_{C}b = Re (r b) *⇩_{R}b + Im (r b) *⇩_{R}𝗂 *⇩_{C}b" using that by (simp add: UNIV_bool ψ_explicit) moreover have "r b *⇩_{C}b = Re (r b) *⇩_{R}b + Im (r b) *⇩_{R}𝗂 *⇩_{C}b" for b using complex_eq scaleC_add_left scaleC_scaleC scaleR_scaleC by (metis (no_types, lifting) complex_of_real_i i_complex_of_real) ultimately have "ψ = (∑(b,i)∈(B'×UNIV). if i then Im (r b) *⇩_{R}(𝗂 *⇩_{C}b) else Re (r b) *⇩_{R}b)" by (simp add: sum.cartesian_product) also have "… ∈ ?rspan R" unfolding R_def using x2 by (rule real_vector.span_sum) finally show "ψ ∈ ?rspan R" by - next let ?cspan = complex_vector.span let ?rspan = real_vector.span define R where "R = B ∪ scaleC 𝗂 ` B" fix ψ assume rspan: "ψ ∈ ?rspan R" have "subspace {a. a ∈ cspan B}" by (rule real_vector.subspaceI, auto simp add: complex_vector.span_zero complex_vector.span_add_eq2 complex_vector.span_scale scaleR_scaleC) moreover have "x ∈ cspan B" if "x ∈ R" for x :: 'a using that R_def complex_vector.span_base complex_vector.span_scale by fastforce ultimately show "ψ ∈ ?cspan B" using real_vector.span_induct rspan by blast qed lemma isomorphic_equal_cdim: assumes lin_f: ‹clinear f› assumes inj_f: ‹inj_on f (cspan S)› assumes im_S: ‹f ` S = T› shows ‹cdim S = cdim T› proof - obtain SB where SB_span: "cspan SB = cspan S" and indep_SB: ‹cindependent SB› by (metis complex_vector.basis_exists complex_vector.span_mono complex_vector.span_span subset_antisym) with lin_f inj_f have indep_fSB: ‹cindependent (f ` SB)› apply (rule_tac complex_vector.linear_independent_injective_image) by auto from lin_f have ‹cspan (f ` SB) = f ` cspan SB› by (meson complex_vector.linear_span_image) also from SB_span lin_f have ‹… = cspan T› by (metis complex_vector.linear_span_image im_S) finally have ‹cdim T = card (f ` SB)› using indep_fSB complex_vector.dim_eq_card by blast also have ‹… = card SB› apply (rule card_image) using inj_f by (metis SB_span complex_vector.linear_inj_on_span_iff_independent_image indep_fSB lin_f) also have ‹… = cdim S› using indep_SB SB_span by (metis complex_vector.dim_eq_card) finally show ?thesis by simp qed lemma cindependent_inter_scaleC_cindependent: assumes a1: "cindependent (B::'a::complex_vector set)" and a3: "c ≠ 1" shows "B ∩ (*⇩_{C}) c ` B = {}" proof (rule classical, cases ‹c = 0›) case True then show ?thesis using a1 by (auto simp add: complex_vector.dependent_zero) next case False assume "¬(B ∩ (*⇩_{C}) c ` B = {})" hence "B ∩ (*⇩_{C}) c ` B ≠ {}" by blast then obtain x where u1: "x ∈ B ∩ (*⇩_{C}) c ` B" by blast then obtain b where u2: "x = b" and u3: "b∈B" by blast then obtain b' where u2': "x = c *⇩_{C}b'" and u3': "b'∈B" using u1 by blast have g1: "b = c *⇩_{C}b'" using u2 and u2' by simp hence "b ∈ complex_vector.span {b'}" using False by (simp add: complex_vector.span_base complex_vector.span_scale) hence "b = b'" by (metis u3' a1 complex_vector.dependent_def complex_vector.span_base complex_vector.span_scale insertE insert_Diff u2 u2' u3) hence "b' = c *⇩_{C}b'" using g1 by blast thus ?thesis by (metis a1 a3 complex_vector.dependent_zero complex_vector.scale_right_imp_eq mult_cancel_right2 scaleC_scaleC u3') qed lemma real_independent_from_complex_independent: assumes "cindependent (B::'a::complex_vector set)" defines "B' == ((*⇩_{C}) 𝗂 ` B)" shows "independent (B ∪ B')" proof (rule notI) assume ‹dependent (B ∪ B')› then obtain T f0 x where [simp]: ‹finite T› and ‹T ⊆ B ∪ B'› and f0_sum: ‹(∑v∈T. f0 v *⇩_{R}v) = 0› and x: ‹x ∈ T› and f0_x: ‹f0 x ≠ 0› by (auto simp: real_vector.dependent_explicit) define f T1 T2 T' f' x' where ‹f v = (if v ∈ T then f0 v else 0)› and ‹T1 = T ∩ B› and ‹T2 = scaleC (-𝗂) ` (T ∩ B')› and ‹T' = T1 ∪ T2› and ‹f' v = f v + 𝗂 * f (𝗂 *⇩_{C}v)› and ‹x' = (if x ∈ T1 then x else -𝗂 *⇩_{C}x)› for v have ‹B ∩ B' = {}› by (simp add: assms cindependent_inter_scaleC_cindependent) have ‹T' ⊆ B› by (auto simp: T'_def T1_def T2_def B'_def) have [simp]: ‹finite T'› ‹finite T1› ‹finite T2› by (auto simp add: T'_def T1_def T2_def) have f_sum: ‹(∑v∈T. f v *⇩_{R}v) = 0› unfolding f_def using f0_sum by auto have f_x: ‹f x ≠ 0› using f0_x x by (auto simp: f_def) have f'_sum: ‹(∑v∈T'. f' v *⇩_{C}v) = 0› proof - have ‹(∑v∈T'. f' v *⇩_{C}v) = (∑v∈T'. complex_of_real (f v) *⇩_{C}v) + (∑v∈T'. (𝗂 * complex_of_real (f (𝗂 *⇩_{C}v))) *⇩_{C}v)› by (auto simp: f'_def sum.distrib scaleC_add_left) also have ‹(∑v∈T'. complex_of_real (f v) *⇩_{C}v) = (∑v∈T1. f v *⇩_{R}v)› (is ‹_ = ?left›) apply (auto simp: T'_def scaleR_scaleC intro!: sum.mono_neutral_cong_right) using T'_def T1_def ‹T' ⊆ B› f_def by auto also have ‹(∑v∈T'. (𝗂 * complex_of_real (f (𝗂 *⇩_{C}v))) *⇩_{C}v) = (∑v∈T2. (𝗂 * complex_of_real (f (𝗂 *⇩_{C}v))) *⇩_{C}v)› (is ‹_ = ?right›) apply (auto simp: T'_def intro!: sum.mono_neutral_cong_right) by (smt (z3) B'_def IntE IntI T1_def T2_def ‹f ≡ λv. if v ∈ T then f0 v else 0› add.inverse_inverse complex_vector.vector_space_axioms i_squared imageI mult_minus_left vector_space.vector_space_assms(3) vector_space.vector_space_assms(4)) also have ‹?right = (∑v∈T∩B'. f v *⇩_{R}v)› (is ‹_ = ?right›) apply (rule sum.reindex_cong[symmetric, where l=‹scaleC 𝗂›]) apply (auto simp: T2_def image_image scaleR_scaleC) using inj_on_def by fastforce also have ‹?left + ?right = (∑v∈T. f v *⇩_{R}v)› apply (subst sum.union_disjoint[symmetric]) using ‹B ∩ B' = {}› ‹T ⊆ B ∪ B'› apply (auto simp: T1_def) by (metis Int_Un_distrib Un_Int_eq(4) sup.absorb_iff1) also have ‹… = 0› by (rule f_sum) finally show ?thesis by - qed have x': ‹x' ∈ T'› using ‹T ⊆ B ∪ B'› x by (auto simp: x'_def T'_def T1_def T2_def) have f'_x': ‹f' x' ≠ 0› using Complex_eq Complex_eq_0 f'_def f_x x'_def by auto from ‹finite T'› ‹T' ⊆ B› f'_sum x' f'_x' have ‹cdependent B› using complex_vector.independent_explicit_module by blast with assms show False by auto qed lemma crepresentation_from_representation: assumes a1: "cindependent B" and a2: "b ∈ B" and a3: "finite B" shows "crepresentation B ψ b = (representation (B ∪ (*⇩_{C}) 𝗂 ` B) ψ b) + 𝗂 *⇩_{C}(representation (B ∪ (*⇩_{C}) 𝗂 ` B) ψ (𝗂 *⇩_{C}b))" proof (cases "ψ ∈ cspan B") define B' where "B' = B ∪ (*⇩_{C}) 𝗂 ` B" case True define r where "r v = real_vector.representation B' ψ v" for v define r' where "r' v = real_vector.representation B' ψ (𝗂 *⇩_{C}v)" for v define f where "f v = r v + 𝗂 *⇩_{C}r' v" for v define g where "g v = crepresentation B ψ v" for v have "(∑v | g v ≠ 0. g v *⇩_{C}v) = ψ" unfolding g_def using Collect_cong Collect_mono_iff DiffD1 DiffD2 True a1 complex_vector.finite_representation complex_vector.sum_nonzero_representation_eq sum.mono_neutral_cong_left by fastforce moreover have "finite {v. g v ≠ 0}" unfolding g_def by (simp add: complex_vector.finite_representation) moreover have "v ∈ B" if "g v ≠ 0" for v using that unfolding g_def by (simp add: complex_vector.representation_ne_zero) ultimately have rep1: "(∑v∈B. g v *⇩_{C}v) = ψ" unfolding g_def using a3 True a1 complex_vector.sum_representation_eq by blast have l0': "inj ((*⇩_{C}) 𝗂::'a ⇒'a)" unfolding inj_def by simp have l0: "inj ((*⇩_{C}) (- 𝗂)::'a ⇒'a)" unfolding inj_def by simp have l1: "(*⇩_{C}) (- 𝗂) ` B ∩ B = {}" using cindependent_inter_scaleC_cindependent[where B=B and c = "- 𝗂"] by (metis Int_commute a1 add.inverse_inverse complex_i_not_one i_squared mult_cancel_left1 neg_equal_0_iff_equal) have l2: "B ∩ (*⇩_{C}) 𝗂 ` B = {}" by (simp add: a1 cindependent_inter_scaleC_cindependent) have rr1: "r (𝗂 *⇩_{C}v) = r' v" for v unfolding r_def r'_def by simp have k1: "independent B'" unfolding B'_def using a1 real_independent_from_complex_independent by simp have "ψ ∈ span B'" using B'_def True cspan_as_span by blast have "v ∈ B'" if "r v ≠ 0" for v unfolding r_def using r_def real_vector.representation_ne_zero that by auto have "finite B'" unfolding B'_def using a3 by simp have "(∑v∈B'. r v *⇩_{R}v) = ψ" unfolding r_def using True Real_Vector_Spaces.real_vector.sum_representation_eq[where B = B' and basis = B' and v = ψ] by (smt Real_Vector_Spaces.dependent_raw_def ‹ψ ∈ Real_Vector_Spaces.span B'› ‹finite B'› equalityD2 k1) have d1: "(∑v∈B. r (𝗂 *⇩_{C}v) *⇩_{R}(𝗂 *⇩_{C}v)) = (∑v∈(*⇩_{C}) 𝗂 ` B. r v *⇩_{R}v)" using l0' by (metis (mono_tags, lifting) inj_eq inj_on_def sum.reindex_cong) have "(∑v∈B. (r v + 𝗂 * (r' v)) *⇩_{C}v) = (∑v∈B. r v *⇩_{C}v + (𝗂 * r' v) *⇩_{C}v)" by (meson scaleC_left.add) also have "… = (∑v∈B. r v *⇩_{C}v) + (∑v∈B. (𝗂 * r' v) *⇩_{C}v)" using sum.distrib by fastforce also have "… = (∑v∈B. r v *⇩_{C}v) + (∑v∈B. 𝗂 *⇩_{C}(r' v *⇩_{C}v))" by auto also have "… = (∑v∈B. r v *⇩_{R}v) + (∑v∈B. 𝗂 *⇩_{C}(r (𝗂 *⇩_{C}v) *⇩_{R}v))" unfolding r'_def r_def by (metis (mono_tags, lifting) scaleR_scaleC sum.cong) also have "… = (∑v∈B. r v *⇩_{R}v) + (∑v∈B. r (𝗂 *⇩_{C}v) *⇩_{R}(𝗂 *⇩_{C}v))" by (metis (no_types, lifting) complex_vector.scale_left_commute scaleR_scaleC) also have "… = (∑v∈B. r v *⇩_{R}v) + (∑v∈(*⇩_{C}) 𝗂 ` B. r v *⇩_{R}v)" using d1 by simp also have "… = ψ" using l2 ‹(∑v∈B'. r v *⇩_{R}v) = ψ› unfolding B'_def by (simp add: a3 sum.union_disjoint) finally have "(∑v∈B. f v *⇩_{C}v) = ψ" unfolding r'_def r_def f_def by simp hence "0 = (∑v∈B. f v *⇩_{C}v) - (∑v∈B. crepresentation B ψ v *⇩_{C}v)" using rep1 unfolding g_def by simp also have "… = (∑v∈B. f v *⇩_{C}v - crepresentation B ψ v *⇩_{C}v)" by (simp add: sum_subtractf) also have "… = (∑v∈B. (f v - crepresentation B ψ v) *⇩_{C}v)" by (metis scaleC_left.diff) finally have "0 = (∑v∈B. (f v - crepresentation B ψ v) *⇩_{C}v)". hence "(∑v∈B. (f v - crepresentation B ψ v) *⇩_{C}v) = 0" by simp hence "f b - crepresentation B ψ b = 0" using a1 a2 a3 complex_vector.independentD[where s = B and t = B and u = "λv. f v - crepresentation B ψ v" and v = b] order_refl by smt hence "crepresentation B ψ b = f b" by simp thus ?thesis unfolding f_def r_def r'_def B'_def by auto next define B' where "B' = B ∪ (*⇩_{C}) 𝗂 ` B" case False have b2: "ψ ∉ real_vector.span B'" unfolding B'_def using False cspan_as_span by auto have "ψ ∉ complex_vector.span B" using False by blast have "crepresentation B ψ b = 0" unfolding complex_vector.representation_def by (simp add: False) moreover have "real_vector.representation B' ψ b = 0" unfolding real_vector.representation_def by (simp add: b2) moreover have "real_vector.representation B' ψ ((*⇩_{C}) 𝗂 b) = 0" unfolding real_vector.representation_def by (simp add: b2) ultimately show ?thesis unfolding B'_def by simp qed lemma CARD_1_vec_0[simp]: ‹(ψ :: _ ::{complex_vector,CARD_1}) = 0› by auto lemma scaleC_cindependent: assumes a1: "cindependent (B::'a::complex_vector set)" and a3: "c ≠ 0" shows "cindependent ((*⇩_{C}) c ` B)" proof- have "u y = 0" if g1: "y∈S" and g2: "(∑x∈S. u x *⇩_{C}x) = 0" and g3: "finite S" and g4: "S⊆(*⇩_{C}) c ` B" for u y S proof- define v where "v x = u (c *⇩_{C}x)" for x obtain S' where "S'⊆B" and S_S': "S = (*⇩_{C}) c ` S'" by (meson g4 subset_imageE) have "inj ((*⇩_{C}) c::'a⇒_)" unfolding inj_def using a3 by auto hence "finite S'" using S_S' finite_imageD g3 subset_inj_on by blast have "t ∈ (*⇩_{C}) (inverse c) ` S" if "t ∈ S'" for t proof- have "c *⇩_{C}t ∈ S" using ‹S = (*⇩_{C}) c ` S'› that by blast hence "(inverse c) *⇩_{C}(c *⇩_{C}t) ∈ (*⇩_{C}) (inverse c) ` S" by blast moreover have "(inverse c) *⇩_{C}(c *⇩_{C}t) = t" by (simp add: a3) ultimately show ?thesis by simp qed moreover have "t ∈ S'" if "t ∈ (*⇩_{C}) (inverse c) ` S" for t proof- obtain t' where "t = (inverse c) *⇩_{C}t'" and "t' ∈ S" using ‹t ∈ (*⇩_{C}) (inverse c) ` S› by auto have "c *⇩_{C}t = c *⇩_{C}((inverse c) *⇩_{C}t')" using ‹t = (inverse c) *⇩_{C}t'› by simp also have "… = (c * (inverse c)) *⇩_{C}t'" by simp also have "… = t'" by (simp add: a3) finally have "c *⇩_{C}t = t'". thus ?thesis using ‹t' ∈ S› using ‹S = (*⇩_{C}) c ` S'› a3 complex_vector.scale_left_imp_eq by blast qed ultimately have "S' = (*⇩_{C}) (inverse c) ` S" by blast hence "inverse c *⇩_{C}y ∈ S'" using that(1) by blast have t: "inj (((*⇩_{C}) c)::'a ⇒ _)" using a3 complex_vector.injective_scale[where c = c] by blast have "0 = (∑x∈(*⇩_{C}) c ` S'. u x *⇩_{C}x)" using ‹S = (*⇩_{C}) c ` S'› that(2) by auto also have "… = (∑x∈S'. v x *⇩_{C}(c *⇩_{C}x))" unfolding v_def using t Groups_Big.comm_monoid_add_class.sum.reindex[where h = "((*⇩_{C}) c)" and A = S' and g = "λx. u x *⇩_{C}x"] subset_inj_on by auto also have "… = c *⇩_{C}(∑x∈S'. v x *⇩_{C}x)" by (metis (mono_tags, lifting) complex_vector.scale_left_commute scaleC_right.sum sum.cong) finally have "0 = c *⇩_{C}(∑x∈S'. v x *⇩_{C}x)". hence "(∑x∈S'. v x *⇩_{C}x) = 0" using a3 by auto hence "v (inverse c *⇩_{C}y) = 0" using ‹inverse c *⇩_{C}y ∈ S'› ‹finite S'› ‹S' ⊆ B› a1 complex_vector.independentD by blast thus "u y = 0" unfolding v_def by (simp add: a3) qed thus ?thesis using complex_vector.dependent_explicit by (simp add: complex_vector.dependent_explicit ) qed subsection ‹Antilinear maps and friends› locale antilinear = additive f for f :: "'a::complex_vector ⇒ 'b::complex_vector" + assumes scaleC: "f (scaleC r x) = cnj r *⇩_{C}f x" sublocale antilinear ⊆ linear proof (rule linearI) show "f (b1 + b2) = f b1 + f b2" for b1 :: 'a and b2 :: 'a by (simp add: add) show "f (r *⇩_{R}b) = r *⇩_{R}f b" for r :: real and b :: 'a unfolding scaleR_scaleC by (subst scaleC, simp) qed lemma antilinear_imp_scaleC: fixes D :: "complex ⇒ 'a::complex_vector" assumes "antilinear D" obtains d where "D = (λx. cnj x *⇩_{C}d)" proof - interpret clinear "D o cnj" apply standard apply auto apply (simp add: additive.add assms antilinear.axioms(1)) using assms antilinear.scaleC by fastforce obtain d where "D o cnj = (λx. x *⇩_{C}d)" using clinear_axioms complex_vector.linear_imp_scale by blast then have ‹D = (λx. cnj x *⇩_{C}d)› by (metis comp_apply complex_cnj_cnj) then show ?thesis by (rule that) qed corollary complex_antilinearD: fixes f :: "complex ⇒ complex" assumes "antilinear f" obtains c where "f = (λx. c * cnj x)" by (rule antilinear_imp_scaleC [OF assms]) (force simp: scaleC_conv_of_complex) lemma antilinearI: assumes "⋀x y. f (x + y) = f x + f y" and "⋀c x. f (c *⇩_{C}x) = cnj c *⇩_{C}f x" shows "antilinear f" by standard (rule assms)+ lemma antilinear_o_antilinear: "antilinear f ⟹ antilinear g ⟹ clinear (g o f)" apply (rule clinearI) apply (simp add: additive.add antilinear_def) by (simp add: antilinear.scaleC) lemma clinear_o_antilinear: "antilinear f ⟹ clinear g ⟹ antilinear (g o f)" apply (rule antilinearI) apply (simp add: additive.add complex_vector.linear_add antilinear_def) by (simp add: complex_vector.linear_scale antilinear.scaleC) lemma antilinear_o_clinear: "clinear f ⟹ antilinear g ⟹ antilinear (g o f)" apply (rule antilinearI) apply (simp add: additive.add complex_vector.linear_add antilinear_def) by (simp add: complex_vector.linear_scale antilinear.scaleC) locale bounded_antilinear = antilinear f for f :: "'a::complex_normed_vector ⇒ 'b::complex_normed_vector" + assumes bounded: "∃K. ∀x. norm (f x) ≤ norm x * K" lemma bounded_antilinearI: assumes ‹⋀b1 b2. f (b1 + b2) = f b1 + f b2› assumes ‹⋀r b. f (r *⇩_{C}b) = cnj r *⇩_{C}f b› assumes ‹∀x. norm (f x) ≤ norm x * K› shows "bounded_antilinear f" using assms by (auto intro!: exI bounded_antilinear.intro antilinearI simp: bounded_antilinear_axioms_def) sublocale bounded_antilinear ⊆ bounded_linear apply standard by (fact bounded) lemma (in bounded_antilinear) bounded_linear: "bounded_linear f" by (fact bounded_linear) lemma (in bounded_antilinear) antilinear: "antilinear f" by (fact antilinear_axioms) lemma bounded_antilinear_intro: assumes "⋀x y. f (x + y) = f x + f y" and "⋀r x. f (scaleC r x) = scaleC (cnj r) (f x)" and "⋀x. norm (f x) ≤ norm x * K" shows "bounded_antilinear f" by standard (blast intro: assms)+ lemma bounded_antilinear_0[simp]: ‹bounded_antilinear (λ_. 0)› by (rule bounded_antilinear_intro[where K=0], auto) lemma cnj_bounded_antilinear[simp]: "bounded_antilinear cnj" apply (rule bounded_antilinear_intro [where K = 1]) by auto lemma bounded_antilinear_o_bounded_antilinear: assumes "bounded_antilinear f" and "bounded_antilinear g" shows "bounded_clinear (λx. f (g x))" proof interpret f: bounded_antilinear f by fact interpret g: bounded_antilinear g by fact fix b1 b2 b r show "f (g (b1 + b2)) = f (g b1) + f (g b2)" by (simp add: f.add g.add) show "f (g (r *⇩_{C}b)) = r *⇩_{C}f (g b)" by (simp add: f.scaleC g.scaleC) have "bounded_linear (λx. f (g x))" using f.bounded_linear g.bounded_linear by (rule bounded_linear_compose) then show "∃K. ∀x. norm (f (g x)) ≤ norm x * K" by (rule bounded_linear.bounded) qed lemma bounded_antilinear_o_bounded_clinear: assumes "bounded_antilinear f" and "bounded_clinear g" shows "bounded_antilinear (λx. f (g x))" proof interpret f: bounded_antilinear f by fact interpret g: bounded_clinear g by fact show "f (g (x + y)) = f (g x) + f (g y)" for x y by (simp only: f.add g.add) show "f (g (scaleC r x)) = scaleC (cnj r) (f (g x))" for r x by (simp add: f.scaleC g.scaleC) have "bounded_linear (λx. f (g x))" using f.bounded_linear g.bounded_linear by (rule bounded_linear_compose) then show "∃K. ∀x. norm (f (g x)) ≤ norm x * K" by (rule bounded_linear.bounded) qed lemma bounded_clinear_o_bounded_antilinear: assumes "bounded_clinear f" and "bounded_antilinear g" shows "bounded_antilinear (λx. f (g x))" proof interpret f: bounded_clinear f by fact interpret g: bounded_antilinear g by fact show "f (g (x + y)) = f (g x) + f (g y)" for x y by (simp only: f.add g.add) show "f (g (scaleC r x)) = scaleC (cnj r) (f (g x))" for r x using f.scaleC g.scaleC by fastforce have "bounded_linear (λx. f (g x))" using f.bounded_linear g.bounded_linear by (rule bounded_linear_compose) then show "∃K. ∀x. norm (f (g x)) ≤ norm x * K" by (rule bounded_linear.bounded) qed lemma bij_clinear_imp_inv_clinear: "clinear (inv f)" if a1: "clinear f" and a2: "bij f" proof fix b1 b2 r b show "inv f (b1 + b2) = inv f b1 + inv f b2" by (simp add: a1 a2 bij_is_inj bij_is_surj complex_vector.linear_add inv_f_eq surj_f_inv_f) show "inv f (r *⇩_{C}b) = r *⇩_{C}inv f b" using that by (smt bij_inv_eq_iff clinear_def complex_vector.linear_scale) qed locale bounded_sesquilinear = fixes prod :: "'a::complex_normed_vector ⇒ 'b::complex_normed_vector ⇒ 'c::complex_normed_vector" (infixl "**" 70) assumes add_left: "prod (a + a') b = prod a b + prod a' b" and add_right: "prod a (b + b') = prod a b + prod a b'" and scaleC_left: "prod (r *⇩_{C}a) b = (cnj r) *⇩_{C}(prod a b)" and scaleC_right: "prod a (r *⇩_{C}b) = r *⇩_{C}(prod a b)" and bounded: "∃K. ∀a b. norm (prod a b) ≤ norm a * norm b * K" sublocale bounded_sesquilinear ⊆ bounded_bilinear apply standard by (auto simp: add_left add_right scaleC_left scaleC_right bounded scaleR_scaleC) lemma (in bounded_sesquilinear) bounded_bilinear[simp]: "bounded_bilinear prod" by (fact bounded_bilinear_axioms) lemma (in bounded_sesquilinear) bounded_antilinear_left: "bounded_antilinear (λa. prod a b)" apply standard apply (auto simp add: scaleC_left add_left) by (metis ab_semigroup_mult_class.mult_ac(1) bounded) lemma (in bounded_sesquilinear) bounded_clinear_right: "bounded_clinear (λb. prod a b)" apply standard apply (auto simp add: scaleC_right add_right) by (metis ab_semigroup_mult_class.mult_ac(1) ordered_field_class.sign_simps(34) pos_bounded) lemma (in bounded_sesquilinear) comp1: assumes ‹bounded_clinear g› shows ‹bounded_sesquilinear (λx. prod (g x))› proof interpret bounded_clinear g by fact fix a a' b b' r show "prod (g (a + a')) b = prod (g a) b + prod (g a') b" by (simp add: add add_left) show "prod (g a) (b + b') = prod (g a) b + prod (g a) b'" by (simp add: add add_right) show "prod (g (r *⇩_{C}a)) b = cnj r *⇩_{C}prod (g a) b" by (simp add: scaleC scaleC_left) show "prod (g a) (r *⇩_{C}b) = r *⇩_{C}prod (g a) b" by (simp add: scaleC_right) interpret bounded_bilinear ‹(λx. prod (g x))› by (simp add: bounded_linear comp1) show "∃K. ∀a b. norm (prod (g a) b) ≤ norm a * norm b * K" using bounded by blast qed lemma (in bounded_sesquilinear) comp2: assumes ‹bounded_clinear g› shows ‹bounded_sesquilinear (λx y. prod x (g y))› proof interpret bounded_clinear g by fact fix a a' b b' r show "prod (a + a') (g b) = prod a (g b) + prod a' (g b)" by (simp add: add add_left) show "prod a (g (b + b')) = prod a (g b) + prod a (g b')" by (simp add: add add_right) show "prod (r *⇩_{C}a) (g b) = cnj r *⇩_{C}prod a (g b)" by (simp add: scaleC scaleC_left) show "prod a (g (r *⇩_{C}b)) = r *⇩_{C}prod a (g b)" by (simp add: scaleC scaleC_right) interpret bounded_bilinear ‹(λx y. prod x (g y))› apply (rule bounded_bilinear.flip) using _ bounded_linear apply (rule bounded_bilinear.comp1) using bounded_bilinear by (rule bounded_bilinear.flip) show "∃K. ∀a b. norm (prod a (g b)) ≤ norm a * norm b * K" using bounded by blast qed lemma (in bounded_sesquilinear) comp: "bounded_clinear f ⟹ bounded_clinear g ⟹ bounded_sesquilinear (λx y. prod (f x) (g y))" using comp1 bounded_sesquilinear.comp2 by auto lemma bounded_clinear_const_scaleR: fixes c :: real assumes ‹bounded_clinear f› shows ‹bounded_clinear (λ x. c *⇩_{R}f x )› proof- have ‹bounded_clinear (λ x. (complex_of_real c) *⇩_{C}f x )› by (simp add: assms bounded_clinear_const_scaleC) thus ?thesis by (simp add: scaleR_scaleC) qed lemma bounded_linear_bounded_clinear: ‹bounded_linear A ⟹ ∀c x. A (c *⇩_{C}x) = c *⇩_{C}A x ⟹ bounded_clinear A› apply standard by (simp_all add: linear_simps bounded_linear.bounded) lemma comp_bounded_clinear: fixes A :: ‹'b::complex_normed_vector ⇒ 'c::complex_normed_vector› and B :: ‹'a::complex_normed_vector ⇒ 'b› assumes ‹bounded_clinear A› and ‹bounded_clinear B› shows ‹bounded_clinear (A ∘ B)› by (metis clinear_compose assms(1) assms(2) bounded_clinear_axioms_def bounded_clinear_compose bounded_clinear_def o_def) lemmas isCont_scaleC [simp] = bounded_bilinear.isCont [OF bounded_cbilinear_scaleC[THEN bounded_cbilinear.bounded_bilinear]] subsection ‹Misc 2› lemmas sums_of_complex = bounded_linear.sums [OF bounded_clinear_of_complex[THEN bounded_clinear.bounded_linear]] lemmas summable_of_complex = bounded_linear.summable [OF bounded_clinear_of_complex[THEN bounded_clinear.bounded_linear]] lemmas suminf_of_complex = bounded_linear.suminf [OF bounded_clinear_of_complex[THEN bounded_clinear.bounded_linear]] lemmas sums_scaleC_left = bounded_linear.sums[OF bounded_clinear_scaleC_left[THEN bounded_clinear.bounded_linear]] lemmas summable_scaleC_left = bounded_linear.summable[OF bounded_clinear_scaleC_left[THEN bounded_clinear.bounded_linear]] lemmas suminf_scaleC_left = bounded_linear.suminf[OF bounded_clinear_scaleC_left[THEN bounded_clinear.bounded_linear]] lemmas sums_scaleC_right = bounded_linear.sums[OF bounded_clinear_scaleC_right[THEN bounded_clinear.bounded_linear]] lemmas summable_scaleC_right = bounded_linear.summable[OF bounded_clinear_scaleC_right[THEN bounded_clinear.bounded_linear]] lemmas suminf_scaleC_right = bounded_linear.suminf[OF bounded_clinear_scaleC_right[THEN bounded_clinear.bounded_linear]] lemma closed_scaleC: fixes S::‹'a::complex_normed_vector set› and a :: complex assumes ‹closed S› shows ‹closed ((*⇩_{C}) a ` S)› proof (cases ‹a = 0›) case True then show ?thesis apply (cases ‹S = {}›) by (auto simp: image_constant) next case False then have ‹(*⇩_{C}) a ` S = (*⇩_{C}) (inverse a) -` S› by (auto simp add: rev_image_eqI) moreover have ‹closed ((*⇩_{C}) (inverse a) -` S)› by (simp add: assms continuous_closed_vimage) ultimately show ?thesis by simp qed lemma closure_scaleC: fixes S::‹'a::complex_normed_vector set› shows ‹closure ((*⇩_{C}) a ` S) = (*⇩_{C}) a ` closure S› proof have ‹closed (closure S)› by simp show "closure ((*⇩_{C}) a ` S) ⊆ (*⇩_{C}) a ` closure S" by (simp add: closed_scaleC closure_minimal closure_subset image_mono) have "x ∈ closure ((*⇩_{C}) a ` S)" if "x ∈ (*⇩_{C}) a ` closure S" for x :: 'a proof- obtain t where ‹x = ((*⇩_{C}) a) t› and ‹t ∈ closure S› using ‹x ∈ (*⇩_{C}) a ` closure S› by auto have ‹∃s. (∀n. s n ∈ S) ∧ s ⇢ t› using ‹t ∈ closure S› Elementary_Topology.closure_sequential by blast then obtain s where ‹∀n. s n ∈ S› and ‹s ⇢ t› by blast have ‹(∀ n. scaleC a (s n) ∈ ((*⇩_{C}) a ` S))› using ‹∀n. s n ∈ S› by blast moreover have ‹(λ n. scaleC a (s n)) ⇢ x› proof- have ‹isCont (scaleC a) t› by simp thus ?thesis using ‹s ⇢ t› ‹x = ((*⇩_{C}) a) t› by (simp add: isCont_tendsto_compose) qed ultimately show ?thesis using Elementary_Topology.closure_sequential by metis qed thus "(*⇩_{C}) a ` closure S ⊆ closure ((*⇩_{C}) a ` S)" by blast qed lemma onorm_scalarC: fixes f :: ‹'a::complex_normed_vector ⇒ 'b::complex_normed_vector› assumes a1: ‹bounded_clinear f› shows ‹onorm (λ x. r *⇩_{C}(f x)) = (cmod r) * onorm f› proof- have ‹(norm (f x)) / norm x ≤ onorm f› for x using a1 by (simp add: bounded_clinear.bounded_linear le_onorm) hence t2: ‹bdd_above {(norm (f x)) / norm x | x. True}› by fastforce have ‹continuous_on UNIV ( (*) w ) › for w::real by simp hence ‹isCont ( ((*) (cmod r)) ) x› for x by simp hence t3: ‹continuous (at_left (Sup {(norm (f x)) / norm x | x. True})) ((*) (cmod r))› using Elementary_Topology.continuous_at_imp_continuous_within by blast have ‹{(norm (f x)) / norm x | x. True} ≠ {}› by blast moreover have ‹mono ((*) (cmod r))› by (simp add: monoI ordered_comm_semiring_class.comm_mult_left_mono) ultimately have ‹Sup {((*) (cmod r)) ((norm (f x)) / norm x) | x. True} = ((*) (cmod r)) (Sup {(norm (f x)) / norm x | x. True})› using t2 t3 by (simp add: continuous_at_Sup_mono full_SetCompr_eq image_image) hence ‹Sup {(cmod r) * ((norm (f x)) / norm x) | x. True} = (cmod r) * (Sup {(norm (f x)) / norm x | x. True})› by blast moreover have ‹Sup {(cmod r) * ((norm (f x)) / norm x) | x. True} = (SUP x. cmod r * norm (f x) / norm x)› by (simp add: full_SetCompr_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 have t1: "(SUP x. cmod r * norm (f x) / norm x) = cmod r * (SUP x. norm (f x) / norm x)" by simp have ‹onorm (λ x. r *⇩_{C}(f x)) = (SUP x. norm ( (λ t. r *⇩_{C}(f t)) x) / norm x)› by (simp add: onorm_def) hence ‹onorm (λ x. r *⇩_{C}(f x)) = (SUP x. (cmod r) * (norm (f x)) / norm x)› by simp also have ‹... = (cmod r) * (SUP x. (norm (f x)) / norm x)› using t1. finally show ?thesis by (simp add: onorm_def) qed lemma onorm_scaleC_left_lemma: fixes f :: "'a::complex_normed_vector" assumes r: "bounded_clinear r" shows "onorm (λx. r x *⇩_{C}f) ≤ onorm r * norm f" proof (rule onorm_bound) fix x have "norm (r x *⇩_{C}f) = norm (r x) * norm f" by simp also have "… ≤ onorm r * norm x * norm f" by (simp add: bounded_clinear.bounded_linear mult.commute mult_left_mono onorm r) finally show "norm (r x *⇩_{C}f) ≤ onorm r * norm f * norm x" by (simp add: ac_simps) show "0 ≤ onorm r * norm f" by (simp add: bounded_clinear.bounded_linear onorm_pos_le r) qed lemma onorm_scaleC_left: fixes f :: "'a::complex_normed_vector" assumes f: "bounded_clinear r" shows "onorm (λx. r x *⇩_{C}f) = onorm r * norm f" proof (cases "f = 0") assume "f ≠ 0" show ?thesis proof (rule order_antisym) show "onorm (λx. r x *⇩_{C}f) ≤ onorm r * norm f" using f by (rule onorm_scaleC_left_lemma) next have bl1: "bounded_clinear (λx. r x *⇩_{C}f)" by (metis bounded_clinear_scaleC_const f) have x1:"bounded_clinear (λx. r x * norm f)" by (metis bounded_clinear_mult_const f) have "onorm r ≤ onorm (λx. r x * complex_of_real (norm f)) / norm f" if "onorm r ≤ onorm (λx. r x * complex_of_real (norm f)) * cmod (1 / complex_of_real (norm f))" and "f ≠ 0" using that by (metis complex_of_real_cmod complex_of_real_nn_iff field_class.field_divide_inverse inverse_eq_divide nice_ordered_field_class.zero_le_divide_1_iff norm_ge_zero of_real_1 of_real_divide of_real_eq_iff) hence "onorm r ≤ onorm (λx. r x * norm f) * inverse (norm f)" using ‹f ≠ 0› onorm_scaleC_left_lemma[OF x1, of "inverse (norm f)"] by (simp add: inverse_eq_divide) also have "onorm (λx. r x * norm f) ≤ onorm (λx. r x *⇩_{C}f)" proof (rule onorm_bound) have "bounded_linear (λx. r x *⇩_{C}f)" using bl1 bounded_clinear.bounded_linear by auto thus "0 ≤ onorm (λx. r x *⇩_{C}f)" by (rule Operator_Norm.onorm_pos_le) show "cmod (r x * complex_of_real (norm f)) ≤ onorm (λx. r x *⇩_{C}f) * norm x" for x :: 'b by (smt ‹bounded_linear (λx. r x *⇩_{C}f)› complex_of_real_cmod complex_of_real_nn_iff complex_scaleC_def norm_ge_zero norm_scaleC of_real_eq_iff onorm) qed finally show "onorm r * norm f ≤ onorm (λx. r x *⇩_{C}f)" using ‹f ≠ 0› by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute) qed qed (simp add: onorm_zero) subsection ‹Finite dimension and canonical basis› lemma vector_finitely_spanned: assumes ‹z ∈ cspan T› shows ‹∃ S. finite S ∧ S ⊆ T ∧ z ∈ cspan S› proof- have ‹∃ S r. finite S ∧ S ⊆ T ∧ z = (∑a∈S. r a *⇩_{C}a)› using complex_vector.span_explicit[where b = "T"] assms by auto then obtain S r where ‹finite S› and ‹S ⊆ T› and ‹z = (∑a∈S. r a *⇩_{C}a)› by blast thus ?thesis by (meson complex_vector.span_scale complex_vector.span_sum complex_vector.span_superset subset_iff) qed setup ‹Sign.add_const_constraint ("Complex_Vector_Spaces0.cindependent", SOME \<^typ>‹'a set ⇒ bool›)› setup ‹Sign.add_const_constraint (\<^const_name>‹cdependent›, SOME \<^typ>‹'a set ⇒ bool›)› setup ‹Sign.add_const_constraint (\<^const_name>‹cspan›, SOME \<^typ>‹'a set ⇒ 'a set›)› class cfinite_dim = complex_vector + assumes cfinitely_spanned: "∃S::'a set. finite S ∧ cspan S = UNIV" class basis_enum = complex_vector + fixes canonical_basis :: "'a list" assumes distinct_canonical_basis[simp]: "distinct canonical_basis" and is_cindependent_set[simp]: "cindependent (set canonical_basis)" and is_generator_set[simp]: "cspan (set canonical_basis) = UNIV" setup ‹Sign.add_const_constraint ("Complex_Vector_Spaces0.cindependent", SOME \<^typ>‹'a::complex_vector set ⇒ bool›)› setup ‹Sign.add_const_constraint (\<^const_name>‹cdependent›, SOME \<^typ>‹'a::complex_vector set ⇒ bool›)› setup ‹Sign.add_const_constraint (\<^const_name>‹cspan›, SOME \<^typ>‹'a::complex_vector set ⇒ 'a set›)› lemma cdim_UNIV_basis_enum[simp]: ‹cdim (UNIV::'a::basis_enum set) = length (canonical_basis::'a list)› apply (subst is_generator_set[symmetric]) apply (subst complex_vector.dim_span_eq_card_independent) apply (rule is_cindependent_set) using distinct_canonical_basis distinct_card by blast lemma finite_basis: "∃basis::'a::cfinite_dim set. finite basis ∧ cindependent basis ∧ cspan basis = UNIV" proof - from cfinitely_spanned obtain S :: ‹'a set› where ‹finite S› and ‹cspan S = UNIV› by auto from complex_vector.maximal_independent_subset obtain B :: ‹'a set› where ‹B ⊆ S› and ‹cindependent B› and ‹S ⊆ cspan B› by metis moreover have ‹finite B› using ‹B ⊆ S› ‹finite S› by (meson finite_subset) moreover have ‹cspan B = UNIV› using ‹cspan S = UNIV› ‹S ⊆ cspan B› by (metis complex_vector.span_eq top_greatest) ultimately show ?thesis by auto qed instance basis_enum ⊆ cfinite_dim apply intro_classes apply (rule exI[of _ ‹set canonical_basis›]) using is_cindependent_set is_generator_set by auto lemma cindependent_cfinite_dim_finite: assumes ‹cindependent (S::'a::cfinite_dim set)› shows ‹finite S› by (metis assms cfinitely_spanned complex_vector.independent_span_bound top_greatest) lemma cfinite_dim_finite_subspace_basis: assumes ‹csubspace X› shows "∃basis::'a::cfinite_dim set. finite basis ∧ cindependent basis ∧ cspan basis = X" by (meson assms cindependent_cfinite_dim_finite complex_vector.basis_exists complex_vector.span_subspace) text ‹The following auxiliary lemma (‹finite_span_complete_aux›) shows more or less the same as ‹finite_span_representation_bounded›, ‹finite_span_complete› below (see there for an intuition about the mathematical content of the lemmas). However, there is one difference: Here we additionally assume here that there is a bijection rep/abs between a finite type \<^typ>‹'basis› and the set $B$. This is needed to be able to use results about euclidean spaces that are formulated w.r.t. the type class \<^class>‹finite› Since we anyway assume that $B$ is finite, this added assumption does not make the lemma weaker. However, we cannot derive the existence of \<^typ>‹'basis› inside the proof (HOL does not support such reasoning). Therefore we have the type \<^typ>‹'basis› as an explicit assumption and remove it using @{attribute internalize_sort} after the proof.› lemma finite_span_complete_aux: fixes b :: "'b::real_normed_vector" and B :: "'b set" and rep :: "'basis::finite ⇒ 'b" and abs :: "'b ⇒ 'basis" assumes t: "type_definition rep abs B" and t1: "finite B" and t2: "b∈B" and t3: "independent B" shows "∃D>0. ∀ψ. norm (representation B ψ b) ≤ norm ψ * D" and "complete (span B)" proof - define repr where "repr = real_vector.representation B" define repr' where "repr' ψ = Abs_euclidean_space (repr ψ o rep)" for ψ define comb where "comb l = (∑b∈B. l b *⇩_{R}b)" for l define comb' where "comb' l = comb (Rep_euclidean_space l o abs)" for l have comb_cong: "comb x = comb y" if "⋀z. z∈B ⟹ x z = y z" for x y unfolding comb_def using that by auto have comb_repr[simp]: "comb (repr ψ) = ψ" if "ψ ∈ real_vector.span B" for ψ using ‹comb ≡ λl. ∑b∈B. l b *⇩_{R}b› local.repr_def real_vector.sum_representation_eq t1 t3 that by fastforce have w5:"(∑b | (b ∈ B ⟶ x b ≠ 0) ∧ b ∈ B. x b *⇩_{R}b) = (∑b∈B. x b *⇩_{R}b)" for x using ‹finite B› by (smt DiffD1 DiffD2 mem_Collect_eq real_vector.scale_eq_0_iff subset_eq sum.mono_neutral_left) have "representation B (∑b∈B. x b *⇩_{R}b) = (λb. if b ∈ B then x b else 0)" for x proof (rule real_vector.representation_eqI) show "independent B" by (simp add: t3) show "(∑b∈B. x b *⇩_{R}b) ∈ span B" by (meson real_vector.span_scale real_vector.span_sum real_vector.span_superset subset_iff) show "b ∈ B" if "(if b ∈ B then x b else 0) ≠ 0" for b :: 'b using that by meson show "finite {b. (if b ∈ B then x b else 0) ≠ 0}" using t1 by auto show "(∑b | (if b ∈ B then x b else 0) ≠ 0. (if b ∈ B then x b else 0) *⇩_{R}b) = (∑b∈B. x b *⇩_{R}b)" using w5 by simp qed hence repr_comb[simp]: "repr (comb x) = (λb. if b∈B then x b else 0)" for x unfolding repr_def comb_def. have repr_bad[simp]: "repr ψ = (λ_. 0)" if "ψ ∉ real_vector.span B" for ψ unfolding repr_def using that by (simp add: real_vector.representation_def) have [simp]: "repr' ψ = 0" if "ψ ∉ real_vector.span B" for ψ unfolding repr'_def repr_bad[OF that] apply transfer by auto have comb'_repr'[simp]: "comb' (repr' ψ) = ψ" if "ψ ∈ real_vector.span B" for ψ proof - have x1: "(repr ψ ∘ rep ∘ abs) z = repr ψ z" if "z ∈ B" for z unfolding o_def using t that type_definition.Abs_inverse by fastforce have "comb' (repr' ψ) = comb ((repr ψ ∘ rep) ∘ abs)" unfolding comb'_def repr'_def by (subst Abs_euclidean_space_inverse; simp) also have "… = comb (repr ψ)" using x1 comb_cong by blast also have "… = ψ" using that by simp finally show ?thesis by - qed have t1: "Abs_euclidean_space (Rep_euclidean_space t) = t" if "⋀x. rep x ∈ B" for t::"'a euclidean_space" apply (subst Rep_euclidean_space_inverse) by simp have "Abs_euclidean_space (λy. if rep y ∈ B then Rep_euclidean_space x y else 0) = x" for x using type_definition.Rep[OF t] apply simp using t1 by blast hence "Abs_euclidean_space (λy. if rep y ∈ B then Rep_euclidean_space x (abs (rep y)) else 0) = x" for x apply (subst type_definition.Rep_inverse[OF t]) by simp hence repr'_comb'[simp]: "repr' (comb' x) = x" for x unfolding comb'_def repr'_def o_def by simp have sphere: "compact (sphere 0 d :: 'basis euclidean_space set)" for d using compact_sphere by blast have "complete (UNIV :: 'basis euclidean_space set)" by (simp add: complete_UNIV) have "(∑b∈B. (Rep_euclidean_space (x + y) ∘ abs) b *⇩_{R}b) = (∑b∈B. (Rep_euclidean_space x ∘ abs) b *⇩_{R}b) + (∑b∈B. (Rep_euclidean_space y ∘ abs) b *⇩_{R}b)" for x :: "'basis euclidean_space" and y :: "'basis euclidean_space" apply (transfer fixing: abs) by (simp add: scaleR_add_left sum.distrib) moreover have "(∑b∈B. (Rep_euclidean_space (c *⇩_{R}x) ∘ abs) b *⇩_{R}b) = c *⇩_{R}(∑b∈B. (Rep_euclidean_space x ∘ abs) b *⇩_{R}b)" for c :: real and x :: "'basis euclidean_space" apply (transfer fixing: abs) by (simp add: real_vector.scale_sum_right) ultimately have blin_comb': "bounded_linear comb'" unfolding comb_def comb'_def by (rule bounded_linearI') hence "continuous_on X comb'" for X by (simp add: linear_continuous_on) hence "compact (comb' ` sphere 0 d)" for d using sphere by (rule compact_continuous_image) hence compact_norm_comb': "compact (norm ` comb' ` sphere 0 1)" using compact_continuous_image continuous_on_norm_id by blast have not0: "0 ∉ norm ` comb' ` sphere 0 1" proof (rule ccontr, simp) assume "0 ∈ norm ` comb' ` sphere 0 1" then obtain x where nc0: "norm (comb' x) = 0" and x: "x ∈ sphere 0 1" by auto hence "comb' x = 0" by simp hence "repr' (comb' x) = 0" unfolding repr'_def o_def repr_def apply simp by (smt repr'_comb' blin_comb' dist_0_norm linear_simps(3) mem_sphere norm_zero x) hence "x = 0" by auto with x show False by simp qed have "closed (norm ` comb' ` sphere 0 1)" using compact_imp_closed compact_norm_comb' by blast moreover have "0 ∉ norm ` comb' ` sphere 0 1" by (simp add: not0) ultimately have "∃d>0. ∀x∈norm ` comb' ` sphere 0 1. d ≤ dist 0 x" by (meson separate_point_closed) then obtain d where d: "x∈norm ` comb' ` sphere 0 1 ⟹ d ≤ dist 0 x" and "d > 0" for x by metis define D where "D = 1/d" hence "D > 0" using ‹d>0› unfolding D_def by auto have "x ≥ d" if "x∈norm ` comb' ` sphere 0 1" for x using d that apply auto by fastforce hence *: "norm (comb' x) ≥ d" if "norm x = 1" for x using that by auto have norm_comb': "norm (comb' x) ≥ d * norm x" for x proof (cases "x=0") show "d * norm x ≤ norm (comb' x)" if "x = 0" using that by simp show "d * norm x ≤ norm (comb' x)" if "x ≠ 0" using that using *[of "(1/norm x) *⇩_{R}x"] unfolding linear_simps(5)[OF blin_comb'] apply auto by (simp add: le_divide_eq) qed have *: "norm (repr' ψ) ≤ norm ψ * D" for ψ proof (cases "ψ ∈ real_vector.span B") show "norm (repr' ψ) ≤ norm ψ * D" if "ψ ∈ span B" using that unfolding D_def using norm_comb'[of "repr' ψ"] ‹d>0› by (simp_all add: linordered_field_class.mult_imp_le_div_pos mult.commute) show "norm (repr' ψ) ≤ norm ψ * D" if "ψ ∉ span B" using that ‹0 < D› by auto qed hence "norm (Rep_euclidean_space (repr' ψ) (abs b)) ≤ norm ψ * D" for ψ proof - have "(Rep_euclidean_space (repr' ψ) (abs b)) = repr' ψ ∙ euclidean_space_basis_vector (abs b)" apply (transfer fixing: abs b) by auto also have "¦…¦ ≤ norm (repr' ψ)" apply (rule Basis_le_norm) unfolding Basis_euclidean_space_def by simp also have "… ≤ norm ψ * D" using * by auto finally show ?thesis by simp qed hence "norm (repr ψ b) ≤ norm ψ * D" for ψ unfolding repr'_def by (smt ‹comb' ≡ λl. comb (Rep_euclidean_space l ∘ abs)› ‹repr' ≡ λψ. Abs_euclidean_space (repr ψ ∘ rep)› comb'_repr' comp_apply norm_le_zero_iff repr_bad repr_comb) thus "∃D>0. ∀ψ. norm (repr ψ b) ≤ norm ψ * D" using ‹D>0› by auto from ‹d>0› have complete_comb': "complete (comb' ` UNIV)" proof (rule complete_isometric_image) show "subspace (UNIV::'basis euclidean_space set)" by simp show "bounded_linear comb'" by (simp add: blin_comb') show "∀x∈UNIV. d * norm x ≤ norm (comb' x)" by (simp add: norm_comb') show "complete (UNIV::'basis euclidean_space set)" by (simp add: ‹complete UNIV›) qed have range_comb': "comb' ` UNIV = real_vector.span B" proof (auto simp: image_def) show "comb' x ∈ real_vector.span B" for x by (metis comb'_def comb_cong comb_repr local.repr_def repr_bad repr_comb real_vector.representation_zero real_vector.span_zero) next fix ψ assume "ψ ∈ real_vector.span B" then obtain f where f: "comb f = ψ" apply atomize_elim unfolding span_finite[OF ‹finite B›] comb_def by auto define f' where "f' b = (if b∈B then f b else 0)" for b :: 'b have f': "comb f' = ψ" unfolding f[symmetric] apply (rule comb_cong) unfolding f'_def by simp define x :: "'basis euclidean_space" where "x = Abs_euclidean_space (f' o rep)" have "ψ = comb' x" by (metis (no_types, lifting) ‹ψ ∈ span B› ‹repr' ≡ λψ. Abs_euclidean_space (repr ψ ∘ rep)› comb'_repr' f' fun.map_cong repr_comb t type_definition.Rep_range x_def) thus "∃x. ψ = comb' x" by auto qed from range_comb' complete_comb' show "complete (real_vector.span B)" by simp qed lemma finite_span_complete[simp]: fixes A :: "'a::real_normed_vector set" assumes "finite A" shows "complete (span A)" text ‹The span of a finite set is complete.› proof (cases "A ≠ {} ∧ A ≠ {0}") case True obtain B where BT: "real_vector.span B = real_vector.span A" and "independent B" and "finite B" by (meson True assms finite_subset real_vector.maximal_independent_subset real_vector.span_eq real_vector.span_superset subset_trans) have "B≠{}" apply (rule ccontr, simp) using BT True by (metis real_vector.span_superset real_vector.span_empty subset_singletonD) (* The following generalizes finite_span_complete_aux to hold without the assumption that 'basis has type class finite *) { (* The type variable 'basisT must not be the same as the one used in finite_span_complete_aux, otherwise "internalize_sort" below fails *) assume "∃(Rep :: 'basisT⇒'a) Abs. type_definition Rep Abs B" then obtain rep :: "'basisT ⇒ 'a" and abs :: "'a ⇒ 'basisT" where t: "type_definition rep abs B" by auto have basisT_finite: "class.finite TYPE('basisT)" apply intro_classes using ‹finite B› t by (metis (mono_tags, opaque_lifting) ex_new_if_finite finite_imageI image_eqI type_definition_def) note finite_span_complete_aux(2)[internalize_sort "'basis::finite"] note this[OF basisT_finite t] } note this[cancel_type_definition, OF ‹B≠{}› ‹finite B› _ ‹independent B›] hence "complete (real_vector.span B)" using ‹B≠{}› by auto thus "complete (real_vector.span A)" unfolding BT by simp next case False thus ?thesis using complete_singleton by auto qed lemma finite_span_representation_bounded: fixes B :: "'a::real_normed_vector set" assumes "finite B" and "independent B" shows "∃D>0. ∀ψ b. abs (representation B ψ b) ≤ norm ψ * D" text ‹ Assume $B$ is a finite linear independent set of vectors (in a real normed vector space). Let $\alpha^\psi_b$ be the coefficients of $\psi$ expressed as a linear combination over $B$. Then $\alpha$ is is uniformly cblinfun (i.e., $\lvert\alpha^\psi_b \leq D \lVert\psi\rVert\psi$ for some $D$ independent of $\psi,b$). (This also holds when $b$ is not in the span of $B$ because of the way ‹real_vector.representation› is defined in this corner case.)› proof (cases "B≠{}") case True (* The following generalizes finite_span_complete_aux to hold without the assumption that 'basis has type class finite *) define repr where "repr = real_vector.representation B" { (* Step 1: Create a fake type definition by introducing a new type variable 'basis and then assuming the existence of the morphisms Rep/Abs to B This is then roughly equivalent to "typedef 'basis = B" *) (* The type variable 'basisT must not be the same as the one used in finite_span_complete_aux (I.e., we cannot call it 'basis) *) assume "∃(Rep :: 'basisT⇒'a) Abs. type_definition Rep Abs B" then obtain rep :: "'basisT ⇒ 'a" and abs :: "'a ⇒ 'basisT" where t: "type_definition rep abs B" by auto (* Step 2: We show that our fake typedef 'basisT could be instantiated as type class finite *) have basisT_finite: "class.finite TYPE('basisT)" apply intro_classes using ‹finite B› t by (metis (mono_tags, opaque_lifting) ex_new_if_finite finite_imageI image_eqI type_definition_def) (* Step 3: We take the finite_span_complete_aux and remove the requirement that 'basis::finite (instead, a precondition "class.finite TYPE('basisT)" is introduced) *) note finite_span_complete_aux(1)[internalize_sort "'basis::finite"] (* Step 4: We instantiate the premises *) note this[OF basisT_finite t] } (* Now we have the desired fact, except that it still assumes that B is isomorphic to some type 'basis together with the assumption that there are morphisms between 'basis and B. 'basis and that premise are removed using cancel_type_definition *) note this[cancel_type_definition, OF True ‹finite B› _ ‹independent B›] hence d2:"∃D. ∀ψ. D>0 ∧ norm (repr ψ b) ≤ norm ψ * D" if ‹b∈B› for b by (simp add: repr_def that True) have d1: " (⋀b. b ∈ B ⟹ ∃D. ∀ψ. 0 < D ∧ norm (repr ψ b) ≤ norm ψ * D) ⟹ ∃D. ∀b ψ. b ∈ B ⟶ 0 < D b ∧ norm (repr ψ b) ≤ norm ψ * D b" apply (rule choice) by auto then obtain D where D: "D b > 0 ∧ norm (repr ψ b) ≤ norm ψ * D b" if "b∈B" for b ψ apply atomize_elim using d2 by blast hence Dpos: "D b > 0" and Dbound: "norm (repr ψ b) ≤ norm ψ * D b" if "b∈B" for b ψ using that by auto define Dall where "Dall = Max (D`B)" have "Dall > 0" unfolding Dall_def using ‹finite B› ‹B≠{}› Dpos by (metis (mono_tags, lifting) Max_in finite_imageI image_iff image_is_empty) have "Dall ≥ D b" if "b∈B" for b unfolding Dall_def using ‹finite B› that by auto with Dbound have "norm (repr ψ b) ≤ norm ψ * Dall" if "b∈B" for b ψ using that by (smt mult_left_mono norm_not_less_zero) moreover have "norm (repr ψ b) ≤ norm ψ * Dall" if "b∉B" for b ψ unfolding repr_def using real_vector.representation_ne_zero True by (metis calculation empty_subsetI less_le_trans local.repr_def norm_ge_zero norm_zero not_less subsetI subset_antisym) ultimately show "∃D>0. ∀ψ b. abs (repr ψ b) ≤ norm ψ * D" using ‹Dall > 0› real_norm_def by metis next case False thus ?thesis unfolding repr_def using real_vector.representation_ne_zero[of B] using nice_ordered_field_class.linordered_field_no_ub by fastforce qed hide_fact finite_span_complete_aux lemma finite_cspan_complete[simp]: fixes B :: "'a::complex_normed_vector set" assumes "finite B" shows "complete (cspan B)" by (simp add: assms cspan_as_span) lemma finite_span_closed[simp]: fixes B :: "'a::real_normed_vector set" assumes "finite B" shows "closed (real_vector.span B)" by (simp add: assms complete_imp_closed) lemma finite_cspan_closed[simp]: fixes S::‹'a::complex_normed_vector set› assumes a1: ‹finite S› shows ‹closed (cspan S)› by (simp add: assms complete_imp_closed) lemma closure_finite_cspan: fixes T::‹'a::complex_normed_vector set› assumes ‹finite T› shows ‹closure (cspan T) = cspan T› by (simp add: assms) lemma finite_cspan_crepresentation_bounded: fixes B :: "'a::complex_normed_vector set" assumes a1: "finite B" and a2: "cindependent B" shows "∃D>0. ∀ψ b. norm (crepresentation B ψ b) ≤ norm ψ * D" proof - define B' where "B' = (B ∪ scaleC 𝗂 ` B)" have independent_B': "independent B'" using B'_def ‹cindependent B› by (simp add: real_independent_from_complex_independent a1) have "finite B'" unfolding B'_def using ‹finite B› by simp obtain D' where "D' > 0" and D': "norm (real_vector.representation B' ψ b) ≤ norm ψ * D'" for ψ b apply atomize_elim using independent_B' ‹finite B'› by (simp add: finite_span_representation_bounded) define D where "D = 2*D'" from ‹D' > 0› have ‹D > 0› unfolding D_def by simp have "norm (crepresentation B ψ b) ≤ norm ψ * D" for ψ b proof (cases "b∈B") case True have d3: "norm 𝗂 = 1" by simp have "norm (𝗂 *⇩_{C}complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b))) = norm 𝗂 * norm (complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b)))" using norm_scaleC by blast also have "… = norm (complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b)))" using d3 by simp finally have d2:"norm (𝗂 *⇩_{C}complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b))) = norm (complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b)))". have "norm (crepresentation B ψ b) = norm (complex_of_real (real_vector.representation B' ψ b) + 𝗂 *⇩_{C}complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b)))" by (simp add: B'_def True a1 a2 crepresentation_from_representation) also have "… ≤ norm (complex_of_real (real_vector.representation B' ψ b)) + norm (𝗂 *⇩_{C}complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b)))" using norm_triangle_ineq by blast also have "… = norm (complex_of_real (real_vector.representation B' ψ b)) + norm (complex_of_real (real_vector.representation B' ψ (𝗂 *⇩_{C}b)))" using d2 by simp also have "… = norm (real_vector.representation B' ψ b) + norm (real_vector.representation B' ψ (𝗂 *⇩_{C}b))" by simp also have "… ≤ norm ψ * D' + norm ψ * D'" by (rule add_mono; rule D') also have "… ≤ norm ψ * D" unfolding D_def by linarith finally show ?thesis by auto next case False hence "crepresentation B ψ b = 0" using complex_vector.representation_ne_zero by blast thus ?thesis by (smt ‹0 < D› norm_ge_zero norm_zero split_mult_pos_le) qed with ‹D > 0› show ?thesis by auto qed lemma bounded_clinear_finite_dim[simp]: fixes f :: ‹'a::{cfinite_dim,complex_normed_vector} ⇒ 'b::complex_normed_vector› assumes ‹clinear f›