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
    by (simp add: local.span_minimal)
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
      by (simp add: nz that)
    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)
    by (simp add: local.span_minimal subsetI)
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
  by (simp add: id_def)

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

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. ycspan {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  ψ = (bB'. 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: "ψ = (bB'. 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: "ψ = (xB'. iUNIV. 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: "bB"
    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: (vT. 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: (vT. 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: (vT'. f' v *C v) = 0
  proof -
    have (vT'. f' v *C v) = (vT'. complex_of_real (f v) *C v) + (vT'. (𝗂 * complex_of_real (f (𝗂 *C v))) *C v)
      by (auto simp: f'_def sum.distrib scaleC_add_left)
    also have (vT'. complex_of_real (f v) *C v) = (vT1. 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 (vT'. (𝗂 * complex_of_real (f (𝗂 *C v))) *C v) = (vT2. (𝗂 * 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 = (vTB'. 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 = (vT. 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: "(vB. 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 "(vB'. 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: "(vB. 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 "(vB. (r v + 𝗂 * (r' v)) *C v) = (vB. r v *C v + (𝗂 * r' v) *C v)"
    by (meson scaleC_left.add)
  also have " = (vB. r v *C v) + (vB. (𝗂 * r' v) *C v)"
    using sum.distrib by fastforce
  also have " = (vB. r v *C v) + (vB. 𝗂 *C (r' v *C v))"
    by auto
  also have " = (vB. r v *R v) + (vB. 𝗂 *C (r (𝗂 *C v) *R v))"
    unfolding r'_def r_def
    by (metis (mono_tags, lifting) scaleR_scaleC sum.cong)
  also have " = (vB. r v *R v) + (vB. r (𝗂 *C v) *R (𝗂 *C v))"
    by (metis (no_types, lifting) complex_vector.scale_left_commute scaleR_scaleC)
  also have " = (vB. r v *R v) + (v(*C) 𝗂 ` B. r v *R v)"
    using d1
    by simp
  also have " = ψ"
    using l2 (vB'. r v *R v) = ψ
    unfolding B'_def
    by (simp add: a3 sum.union_disjoint)
  finally have "(vB. f v *C v) = ψ" unfolding r'_def r_def f_def by simp
  hence "0 = (vB. f v *C v) - (vB. crepresentation B ψ v *C v)"
    using rep1
    unfolding g_def
    by simp
  also have " = (vB. f v *C v - crepresentation B ψ v *C v)"
    by (simp add: sum_subtractf)
  also have " = (vB. (f v - crepresentation B ψ v) *C v)"
    by (metis scaleC_left.diff)
  finally have "0 = (vB. (f v - crepresentation B ψ v) *C v)".
  hence "(vB. (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: "yS" and g2: "(xS. 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 " = (xS'. 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 (xS'. v x *C x)"
      by (metis (mono_tags, lifting) complex_vector.scale_left_commute scaleC_right.sum sum.cong)
    finally have "0 = c *C (xS'. v x *C x)".
    hence "(xS'. 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

lemma cspan_eqI:
  assumes a. aA  acspan B
  assumes b. bB  bcspan 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
    by (simp add: bounded_clinear.clinear)
  have [simp]: inj f
  proof (rule injI)
    fix x y assume f x = f y
    then have norm (f (x - y)) = 0
      by (simp add: complex_vector.linear_diff)
    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"
    by (simp flip: complex_vector.linear_add)
  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 xM. y M. u. v. u *C x + v *C y   M
    using a1
    by (simp add:  complex_vector.subspace_def)
  hence xM. yM. u::real. v::real. u *R x + v *R y  M
    by (simp add: scaleR_scaleC)
  hence xM. yM. u0. v0. 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})"
  by (simp add: assms complex_vector.linear_subspace_vimage)

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] 
        simp add: f.add_right f.scaleC_right mult.commute mult.left_commute)
qed

lemma clinear_scaleR[simp]: clinear (scaleR x)
  by (simp add: complex_vector.linear_scale_self scaleR_scaleC)


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
    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  real: bounded_linear
  ― ‹Gives access to all lemmas from localelinear using prefix real.›
  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)"
    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_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
    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_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
    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 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"
    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  real: bounded_bilinear
  ― ‹Gives access to all lemmas from localelinear using prefix real.›
  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 intro_locales

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) 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"
    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 bi: bounded_bilinear (λx. prod (g x))
    by (simp add: bounded_linear real.comp1)
  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)"
    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 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 )
    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)


lemma bounded_sesquilinear_add:
  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)"
    by (simp add: bounded_sesquilinear.add_left that(1) that(2))
  show A a (b + b') + B a (b + b') = (A a b + B a b) + (A a b' + B a b')
    by (simp add: bounded_sesquilinear.add_right that(1) that(2))
  show A (r *C a) b + B (r *C a) b = cnj r *C (A a b + B a b)
    by (simp add: bounded_sesquilinear.scaleC_left scaleC_add_right that(1) that(2))
  show A a (r *C b) + B a (r *C b) = r *C (A a b + B a b)
    by (simp add: bounded_sesquilinear.scaleC_right scaleC_add_right that(1) that(2))
  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
      by (simp add: bounded_sesquilinear.bounded that(1))
    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
      by (simp add: bounded_sesquilinear.bounded that(2))
    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
        using add_mono by blast
      also have =  norm a * norm b * (KA + KB)
        by (simp add: mult.commute ring_class.ring_distribs(2))
      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)"
    by (simp add: bounded_sesquilinear.add_left that)
  show - A a (b + b') = (- A a b) + (- A a b')
    by (simp add: bounded_sesquilinear.add_right that)
  show - A (r *C a) b = cnj r *C (- A a b)
    by (simp add: bounded_sesquilinear.scaleC_left that)
  show - A a (r *C b) = r *C (- A a b)
    by (simp add: bounded_sesquilinear.scaleC_right that)
  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
      by (simp add: bounded_sesquilinear.bounded that(1))
    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))
    using that(1) by (rule bounded_sesquilinear_add[rotated])
  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] 
        simp add: f.add_right f.scaleC_right mult.commute mult.left_commute)
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)
   apply (rule summable_on_comm_additive)
  using assms by (auto simp add: scaleC_left.additive_axioms)

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)
   apply (rule summable_on_comm_additive)
  using assms by (auto simp add: scaleC_right.additive_axioms)

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)
   apply (rule infsum_comm_additive)
  using assms by (auto simp add: scaleC_left.additive_axioms)

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)
      apply (rule infsum_comm_additive)
      using summable by (auto simp add: scaleC_right.additive_axioms)
  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
      by (simp add: infsum_not_exists not_summable(1)) 
  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
    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 = (aS. 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 = (aS. 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_namecdependent, SOME typ'a set  bool)
setup Sign.add_const_constraint (const_namecspan, 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_namecdependent, SOME typ'a::complex_vector set  bool)
setup Sign.add_const_constraint (const_namecspan, 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)"
    by (simp add: canonical_basis_complex_def)
  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)
    by (simp add: canonical_basis_length_complex_def canonical_basis_complex_def)
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 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 classfinite

   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: "bB" 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 = (bB. 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. zB  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. bB. 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) =
    (bB. x b