# Theory Complex_Vector_Spaces

```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"
"HOL-Library.Complemented_Lattices"
"HOL-Library.Function_Algebras"

Extra_Vector_Spaces
Extra_Ordered_Fields
Extra_Operator_Norm
Extra_General

Complex_Vector_Spaces0
begin

bundle notation_norm begin
notation norm ("∥_∥")
end

unbundle lattice_syntax

subsection ‹Misc›

(* Should rather be in Extra_Vector_Spaces but then complex_vector.span_image_scale' does not exist for some reason.
Ideally this would replace Vector_Spaces.vector_space.span_image_scale. *)
lemma (in vector_space) span_image_scale':
― ‹Strengthening of @{thm [source] vector_space.span_image_scale} without the condition ‹finite S››
assumes nz: "⋀x. x ∈ S ⟹ c x ≠ 0"
shows "span ((λx. c x *s x) ` S) = span S"
proof
have ‹((λx. c x *s x) ` S) ⊆ span S›
by (metis (mono_tags, lifting) image_subsetI in_mono local.span_superset local.subspace_scale local.subspace_span)
then show ‹span ((λx. c x *s x) ` S) ⊆ span S›
next
have ‹x ∈ span ((λx. c x *s x) ` S)› if ‹x ∈ S› for x
proof -
have ‹x = inverse (c x) *s c x *s x›
moreover have ‹c x *s x ∈ (λx. c x *s x) ` S›
using that by blast
ultimately show ?thesis
by (metis local.span_base local.span_scale)
qed
then show ‹span S ⊆ span ((λx. c x *s x) ` S)›
qed

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 bounded_clinear) bounded_linear: "bounded_linear f"
by standard

lemma clinear_times: "clinear (λx. c * x)"
for c :: "'a::complex_algebra"
by (auto simp: clinearI distrib_left)

lemma (in clinear) linear: ‹linear f›
by standard

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›

lemma bounded_clinear_0[simp]: ‹bounded_clinear 0›
by (auto intro!: bounded_clinearI[where K=0])

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)) )›

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)

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
also have ‹… = g' b1 * g y + g' b2 * g y›
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›
also have ‹… = r *⇩C (g' b * g y)›
also have ‹… = r *⇩C (h b y)›
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
also have ‹… = g' x * g b1 + g' x * g b2›
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)›
also have ‹… = r *⇩C (g' x * g b)›
also have ‹… = r *⇩C (h x b)›
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
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

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 (intro set_eqI iffI)
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
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)"
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
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
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' = {}›
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
moreover have "v ∈ B"
if "g v ≠ 0" for v
using that unfolding g_def
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 = {}"
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)"
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
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)"
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
moreover have "real_vector.representation B' ψ b = 0"
unfolding real_vector.representation_def
moreover have "real_vector.representation B' ψ ((*⇩C) 𝗂 b) = 0"
unfolding real_vector.representation_def
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"
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'"
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
qed
thus ?thesis
using complex_vector.dependent_explicit
qed

lemma cspan_eqI:
assumes ‹⋀a. a∈A ⟹ a∈cspan B›
assumes ‹⋀b. b∈B ⟹ b∈cspan A›
shows ‹cspan A = cspan B›
apply (rule complex_vector.span_subspace[rotated])
apply (rule complex_vector.span_minimal)
using assms by auto

lemma (in bounded_cbilinear) bounded_bilinear[simp]: "bounded_bilinear prod"
by standard

lemma norm_scaleC_sgn[simp]: ‹complex_of_real (norm ψ) *⇩C sgn ψ = ψ› for ψ :: "'a::complex_normed_vector"
apply (cases ‹ψ = 0›)
by (auto simp: sgn_div_norm scaleR_scaleC)

lemma scaleC_of_complex[simp]: ‹scaleC x (of_complex y) = of_complex (x * y)›
unfolding of_complex_def using scaleC_scaleC by blast

lemma bounded_clinear_inv:
assumes [simp]: ‹bounded_clinear f›
assumes b: ‹b > 0›
assumes bound: ‹⋀x. norm (f x) ≥ b * norm x›
assumes ‹surj f›
shows ‹bounded_clinear (inv f)›
proof (rule bounded_clinear_intro)
fix x y :: 'b and r :: complex
define x' y' where ‹x' = inv f x› and ‹y' = inv f y›
have [simp]: ‹clinear f›
have [simp]: ‹inj f›
proof (rule injI)
fix x y assume ‹f x = f y›
then have ‹norm (f (x - y)) = 0›
with bound b have ‹norm (x - y) = 0›
by (metis linorder_not_le mult_le_0_iff nle_le norm_ge_zero)
then show ‹x = y›
by simp
qed

from ‹surj f›
have [simp]: ‹x = f x'› ‹y = f y'›
by (simp_all add: surj_f_inv_f x'_def y'_def)
show "inv f (x + y) = inv f x + inv f y"
show "inv f (r *⇩C x) = r *⇩C inv f x"
by (simp flip: clinear.scaleC)
from bound have "b * norm (inv f x) ≤ norm x"
by (simp flip: clinear.scaleC)
with b show "norm (inv f x) ≤ norm x * inverse b"
by (smt (verit, ccfv_threshold) left_inverse mult.commute mult_cancel_right1 mult_le_cancel_left_pos vector_space_over_itself.scale_scale)
qed

lemma range_is_csubspace[simp]:
assumes a1: "clinear f"
shows "csubspace (range f)"
using assms complex_vector.linear_subspace_image complex_vector.subspace_UNIV by blast

lemma csubspace_is_convex[simp]:
assumes a1: "csubspace M"
shows "convex M"
proof-
have ‹∀x∈M. ∀y∈ M. ∀u. ∀v. u *⇩C x + v *⇩C y ∈  M›
using a1
hence ‹∀x∈M. ∀y∈M. ∀u::real. ∀v::real. u *⇩R x + v *⇩R y ∈ M›
hence ‹∀x∈M. ∀y∈M. ∀u≥0. ∀v≥0. u + v = 1 ⟶ u *⇩R x + v *⇩R y ∈M›
by blast
thus ?thesis using convex_def by blast
qed

lemma kernel_is_csubspace[simp]:
assumes a1: "clinear f"
shows "csubspace  (f -` {0})"

lemma bounded_cbilinear_0[simp]: ‹bounded_cbilinear (λ_ _. 0)›
by (auto intro!: bounded_cbilinear.intro exI[where x=0])
lemma bounded_cbilinear_0'[simp]: ‹bounded_cbilinear 0›
by (auto intro!: bounded_cbilinear.intro exI[where x=0])

lemma bounded_cbilinear_apply_bounded_clinear: ‹bounded_clinear (f x)› if ‹bounded_cbilinear f›
proof -
interpret f: bounded_cbilinear f
by (fact that)
from f.bounded obtain K where ‹norm (f a b) ≤ norm a * norm b * K› for a b
by auto
then show ?thesis
by (auto intro!: bounded_clinearI[where K=‹norm x * K›]
qed

lemma clinear_scaleR[simp]: ‹clinear (scaleR x)›

lemma abs_summable_on_scaleC_left [intro]:
fixes c :: ‹'a :: complex_normed_vector›
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows   "(λx. f x *⇩C c) abs_summable_on A"
apply (cases ‹c = 0›)
apply simp
by (auto intro!: summable_on_cmult_left assms simp: norm_scaleC)

lemma abs_summable_on_scaleC_right [intro]:
fixes f :: ‹'a ⇒ 'b :: complex_normed_vector›
assumes "c ≠ 0 ⟹ f abs_summable_on A"
shows   "(λx. c *⇩C f x) abs_summable_on A"
apply (cases ‹c = 0›)
apply simp
by (auto intro!: summable_on_cmult_right assms simp: norm_scaleC)

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
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
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)

lemma clinear_o_antilinear: "antilinear f ⟹ clinear g ⟹ antilinear (g o f)"
apply (rule antilinearI)

lemma antilinear_o_clinear: "clinear f ⟹ antilinear g ⟹ antilinear (g o f)"
apply (rule antilinearI)

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 ⊆ real: bounded_linear
apply standard by (fact bounded)

lemma (in bounded_antilinear) bounded_linear: "bounded_linear f"
by (fact real.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 (auto intro!: bounded_antilinearI[where K=0])

lemma bounded_antilinear_0'[simp]: ‹bounded_antilinear 0›
by (auto intro!: bounded_antilinearI[where K=0])

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)"
show "f (g (r *⇩C b)) = r *⇩C f (g b)"
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_antilinear':
assumes "bounded_antilinear f"
and "bounded_antilinear g"
shows "bounded_clinear (g o f)"
using assms by (simp add: o_def bounded_antilinear_o_bounded_antilinear)

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
show "f (g (scaleC r x)) = scaleC (cnj r) (f (g x))" for r x
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_clinear f"
and "bounded_antilinear g"
shows "bounded_antilinear (g o f)"
using assms by (simp add: o_def bounded_antilinear_o_bounded_clinear)

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
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 bounded_clinear_o_bounded_antilinear':
assumes "bounded_antilinear f"
and "bounded_clinear g"
shows "bounded_antilinear (g o f)"
using assms by (simp add: o_def bounded_clinear_o_bounded_antilinear)

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"
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 ⊆ real: bounded_bilinear
apply standard

lemma (in bounded_sesquilinear) bounded_bilinear[simp]: "bounded_bilinear prod"
by intro_locales

lemma (in bounded_sesquilinear) bounded_antilinear_left: "bounded_antilinear (λa. prod a b)"
apply standard
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
by (metis ab_semigroup_mult_class.mult_ac(1) ordered_field_class.sign_simps(34) real.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"
show "prod (g a) (b + b') = prod (g a) b + prod (g a) b'"
show "prod (g (r *⇩C a)) b = cnj r *⇩C prod (g a) b"
show "prod (g a) (r *⇩C b) = r *⇩C prod (g a) b"
interpret bi: bounded_bilinear ‹(λx. prod (g x))›
show "∃K. ∀a b. norm (prod (g a) b) ≤ norm a * norm b * K"
using bi.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)"
show "prod a (g (b + b')) = prod a (g b) + prod a (g b')"
show "prod (r *⇩C a) (g b) = cnj r *⇩C prod a (g b)"
show "prod a (g (r *⇩C b)) = r *⇩C prod a (g b)"
interpret bi: 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 bi.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 )›
thus ?thesis
qed

lemma bounded_linear_bounded_clinear:
‹bounded_linear A ⟹ ∀c x. A (c *⇩C x) = c *⇩C A x ⟹ bounded_clinear A›
apply standard

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)

‹bounded_sesquilinear (λ x y. A x y + B x y)› if ‹bounded_sesquilinear A› and ‹bounded_sesquilinear B›
proof
fix a a' :: 'a and b b' :: 'b and r :: complex
show "A (a + a') b + B (a + a') b = (A a b + B a b) + (A a' b + B a' b)"
show ‹A a (b + b') + B a (b + b') = (A a b + B a b) + (A a b' + B a b')›
show ‹A (r *⇩C a) b + B (r *⇩C a) b = cnj r *⇩C (A a b + B a b)›
show ‹A a (r *⇩C b) + B a (r *⇩C b) = r *⇩C (A a b + B a b)›
show ‹∃K. ∀a b. norm (A a b + B a b) ≤ norm a * norm b * K›
proof-
have ‹∃ KA. ∀ a b. norm (A a b) ≤ norm a * norm b * KA›
then obtain KA where ‹∀ a b. norm (A a b) ≤ norm a * norm b * KA›
by blast
have ‹∃ KB. ∀ a b. norm (B a b) ≤ norm a * norm b * KB›
then obtain KB where ‹∀ a b. norm (B a b) ≤ norm a * norm b * KB›
by blast
have ‹norm (A a b + B a b) ≤ norm a * norm b * (KA + KB)›
for a b
proof-
have ‹norm (A a b + B a b) ≤ norm (A a b) +  norm (B a b)›
using norm_triangle_ineq by blast
also have ‹… ≤ norm a * norm b * KA + norm a * norm b * KB›
using  ‹∀ a b. norm (A a b) ≤ norm a * norm b * KA›
‹∀ a b. norm (B a b) ≤ norm a * norm b * KB›
also have ‹…=  norm a * norm b * (KA + KB)›
finally show ?thesis
by blast
qed
thus ?thesis by blast
qed
qed

lemma bounded_sesquilinear_uminus:
‹bounded_sesquilinear (λ x y. - A x y)› if ‹bounded_sesquilinear A›
proof
fix a a' :: 'a and b b' :: 'b and r :: complex
show "- A (a + a') b = (- A a b) + (- A a' b)"
show ‹- A a (b + b') = (- A a b) + (- A a b')›
show ‹- A (r *⇩C a) b = cnj r *⇩C (- A a b)›
show ‹- A a (r *⇩C b) = r *⇩C (- A a b)›
show ‹∃K. ∀a b. norm (- A a b) ≤ norm a * norm b * K›
proof-
have ‹∃ KA. ∀ a b. norm (A a b) ≤ norm a * norm b * KA›
then obtain KA where ‹∀ a b. norm (A a b) ≤ norm a * norm b * KA›
by blast
have ‹norm (- A a b) ≤ norm a * norm b * KA›
for a b
by (simp add: ‹∀a b. norm (A a b) ≤ norm a * norm b * KA›)
thus ?thesis by blast
qed
qed

lemma bounded_sesquilinear_diff:
‹bounded_sesquilinear (λ x y. A x y - B x y)› if ‹bounded_sesquilinear A› and ‹bounded_sesquilinear B›
proof -
have ‹bounded_sesquilinear (λ x y. - B x y)›
using that(2) by (rule bounded_sesquilinear_uminus)
then have ‹bounded_sesquilinear (λ x y. A x y + (- B x y))›
then show ?thesis
by auto
qed

lemmas isCont_scaleC [simp] =
bounded_bilinear.isCont [OF bounded_cbilinear_scaleC[THEN bounded_cbilinear.bounded_bilinear]]

lemma bounded_sesquilinear_0[simp]: ‹bounded_sesquilinear (λ_ _.0)›
by (auto intro!: bounded_sesquilinear.intro exI[where x=0])

lemma bounded_sesquilinear_0'[simp]: ‹bounded_sesquilinear 0›
by (auto intro!: bounded_sesquilinear.intro exI[where x=0])

lemma bounded_sesquilinear_apply_bounded_clinear: ‹bounded_clinear (f x)› if ‹bounded_sesquilinear f›
proof -
interpret f: bounded_sesquilinear f
by (fact that)
from f.bounded obtain K where ‹norm (f a b) ≤ norm a * norm b * K› for a b
by auto
then show ?thesis
by (auto intro!: bounded_clinearI[where K=‹norm x * K›]
qed

subsection ‹Misc 2›

lemma summable_on_scaleC_left [intro]:
fixes c :: ‹'a :: complex_normed_vector›
assumes "c ≠ 0 ⟹ f summable_on A"
shows   "(λx. f x *⇩C c) summable_on A"
apply (cases ‹c ≠ 0›)
apply (subst asm_rl[of ‹(λx. f x *⇩C c) = (λy. y *⇩C c) o f›], simp add: o_def)

lemma summable_on_scaleC_right [intro]:
fixes f :: ‹'a ⇒ 'b :: complex_normed_vector›
assumes "c ≠ 0 ⟹ f summable_on A"
shows   "(λx. c *⇩C f x) summable_on A"
apply (cases ‹c ≠ 0›)
apply (subst asm_rl[of ‹(λx. c *⇩C f x) = (λy. c *⇩C y) o f›], simp add: o_def)

lemma infsum_scaleC_left:
fixes c :: ‹'a :: complex_normed_vector›
assumes "c ≠ 0 ⟹ f summable_on A"
shows   "infsum (λx. f x *⇩C c) A = infsum f A *⇩C c"
apply (cases ‹c ≠ 0›)
apply (subst asm_rl[of ‹(λx. f x *⇩C c) = (λy. y *⇩C c) o f›], simp add: o_def)

lemma infsum_scaleC_right:
fixes f :: ‹'a ⇒ 'b :: complex_normed_vector›
shows   "infsum (λx. c *⇩C f x) A = c *⇩C infsum f A"
proof -
consider (summable) ‹f summable_on A› | (c0) ‹c = 0› | (not_summable) ‹¬ f summable_on A› ‹c ≠ 0›
by auto
then show ?thesis
proof cases
case summable
then show ?thesis
apply (subst asm_rl[of ‹(λx. c *⇩C f x) = (λy. c *⇩C y) o f›], simp add: o_def)
next
case c0
then show ?thesis by auto
next
case not_summable
have ‹¬ (λx. c *⇩C f x) summable_on A›
proof (rule notI)
assume ‹(λx. c *⇩C f x) summable_on A›
then have ‹(λx. inverse c *⇩C c *⇩C f x) summable_on A›
using summable_on_scaleC_right by blast
then have ‹f summable_on A›
using not_summable by auto
with not_summable show False
by simp
qed
then show ?thesis
qed
qed

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›
moreover have ‹closed ((*⇩C) (inverse a) -` S)›
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›
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
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))›
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)›
moreover have ‹(Sup {(norm (f x)) / norm x | x. True})
= (SUP x. norm (f x) / norm x)›
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)›
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
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"
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 (smt (verit) divide_inverse mult_1 norm_divide norm_ge_zero norm_of_real of_real_1 of_real_eq_iff of_real_mult)
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)"]
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 (verit) ‹bounded_linear (λx. r x *⇩C f)› norm_ge_zero norm_mult norm_of_real norm_scaleC 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

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›
and canonical_basis_length :: ‹'a itself ⇒ nat›
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"
and canonical_basis_length:
‹canonical_basis_length TYPE('a) = length canonical_basis›

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›)›

instantiation complex :: basis_enum begin
definition "canonical_basis = [1::complex]"
definition ‹canonical_basis_length (_::complex itself) = 1›
instance
proof
show "distinct (canonical_basis::complex list)"
show "cindependent (set (canonical_basis::complex list))"
unfolding canonical_basis_complex_def
by auto
show "cspan (set (canonical_basis::complex list)) = UNIV"
unfolding canonical_basis_complex_def
apply (auto simp add: cspan_raw_def vector_space_over_itself.span_Basis)
by (metis complex_scaleC_def complex_vector.span_base complex_vector.span_scale cspan_raw_def insertI1 mult.right_neutral)
show ‹canonical_basis_length TYPE(complex) = length (canonical_basis :: complex list)›
qed
end

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 ```