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 (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)"]
      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 (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
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 *R b)" for x
    using finite B
    by (smt DiffD1 DiffD2 mem_Collect_eq real_vector.scale_eq_0_iff subset_eq sum.mono_neutral_left)
  have "representation B (bB. x b *R b) =  (λb. if b  B then x b else 0)"
    for x
  proof (rule real_vector.representation_eqI)
    show "independent B"
      by (simp add: t3)
    show "(bB. x b *R b)  span B"
      by (meson real_vector.span_scale real_vector.span_sum real_vector.span_superset subset_iff)
    show "b  B"
      if "(if b  B then x b else 0)  0"
      for b :: 'b
      using that
      by meson
    show "finite {b. (if b  B then x b else 0)  0}"
      using t1 by auto
    show "(b | (if b  B then x b else 0)  0. (if b  B then x b else 0) *R b) = (bB. x b *R b)"
      using w5
      by simp
  qed
  hence repr_comb[simp]: "repr (comb x) = (λb. if bB then x b else 0)" for x
    unfolding repr_def comb_def.
  have repr_bad[simp]: "repr ψ = (λ_. 0)" if "ψ  real_vector.span B" for ψ
    unfolding repr_def using that
    by (simp add: real_vector.representation_def)
  have [simp]: "repr' ψ = 0" if "ψ  real_vector.span B" for ψ
    unfolding repr'_def repr_bad[OF that]
    apply transfer
    by auto
  have comb'_repr'[simp]: "comb' (repr' ψ) = ψ"
    if "ψ  real_vector.span B" for ψ
  proof -
    have x1: "(repr ψ  rep  abs) z = repr ψ z"
      if "z  B"
      for z
      unfolding o_def
      using t that type_definition.Abs_inverse by fastforce
    have "comb' (repr' ψ) = comb ((repr ψ  rep)  abs)"
      unfolding comb'_def repr'_def
      by (subst Abs_euclidean_space_inverse; simp)
    also have " = comb (repr ψ)"
      using x1 comb_cong by blast
    also have " = ψ"
      using that by simp
    finally show ?thesis by -
  qed

  have t1: "Abs_euclidean_space (Rep_euclidean_space t) = t"
    if "x. rep x  B"
    for t::"'a euclidean_space"
    apply (subst Rep_euclidean_space_inverse)
    by simp
  have "Abs_euclidean_space
     (λy. if rep y  B
           then Rep_euclidean_space x y
           else 0) = x"
    for x
    using type_definition.Rep[OF t] apply simp
    using t1 by blast
  hence "Abs_euclidean_space
     (λy. if rep y  B
           then Rep_euclidean_space x (abs (rep y))
           else 0) = x"
    for x
    apply (subst type_definition.Rep_inverse[OF t])
    by simp
  hence repr'_comb'[simp]: "repr' (comb' x) = x" for x
    unfolding comb'_def repr'_def o_def
    by simp
  have sphere: "compact (sphere 0 d :: 'basis euclidean_space set)" for d
    using compact_sphere by blast
  have "complete (UNIV :: 'basis euclidean_space set)"
    by (simp add: complete_UNIV)


  have "(bB. (Rep_euclidean_space (x + y)  abs) b *R b) = (bB. (Rep_euclidean_space x  abs) b *R b) + (bB. (Rep_euclidean_space y  abs) b *R b)"
    for x :: "'basis euclidean_space"
      and y :: "'basis euclidean_space"
    apply (transfer fixing: abs)
    by (simp add: scaleR_add_left sum.distrib)
  moreover have "(bB. (Rep_euclidean_space (c *R x)  abs) b *R b) = c *R (bB. (Rep_euclidean_space x  abs) b *R b)"
    for c :: real
      and x :: "'basis euclidean_space"
    apply (transfer fixing: abs)
    by (simp add: real_vector.scale_sum_right)
  ultimately have blin_comb': "bounded_linear comb'"
    unfolding comb_def comb'_def
    by (rule bounded_linearI')
  hence "continuous_on X comb'" for X
    by (simp add: linear_continuous_on)
  hence "compact (comb' ` sphere 0 d)" for d
    using sphere
    by (rule compact_continuous_image)
  hence compact_norm_comb': "compact (norm ` comb' ` sphere 0 1)"
    using compact_continuous_image continuous_on_norm_id by blast
  have not0: "0  norm ` comb' ` sphere 0 1"
  proof (rule ccontr, simp)
    assume "0  norm ` comb' ` sphere 0 1"
    then obtain x where nc0: "norm (comb' x) = 0" and x: "x  sphere 0 1"
      by auto
    hence "comb' x = 0"
      by simp
    hence "repr' (comb' x) = 0"
      unfolding repr'_def o_def repr_def apply simp
      by (smt repr'_comb' blin_comb' dist_0_norm linear_simps(3) mem_sphere norm_zero x)
    hence "x = 0"
      by auto
    with x show False
      by simp
  qed

  have "closed (norm ` comb' ` sphere 0 1)"
    using compact_imp_closed compact_norm_comb' by blast
  moreover have "0  norm ` comb' ` sphere 0 1"
    by (simp add: not0)
  ultimately have "d>0. xnorm ` comb' ` sphere 0 1. d  dist 0 x"
    by (meson separate_point_closed)

  then obtain d where d: "xnorm ` comb' ` sphere 0 1  d  dist 0 x"
    and "d > 0" for x
    by metis
  define D where "D = 1/d"
  hence "D > 0"
    using d>0 unfolding D_def by auto
  have "x  d"
    if "xnorm ` comb' ` sphere 0 1"
    for x
    using d that
    apply auto
    by fastforce
  hence *: "norm (comb' x)  d" if "norm x = 1" for x
    using that by auto
  have norm_comb': "norm (comb' x)  d * norm x" for x
  proof (cases "x=0")
    show "d * norm x  norm (comb' x)"
      if "x = 0"
      using that
      by simp
    show "d * norm x  norm (comb' x)"
      if "x  0"
      using that
      using *[of "(1/norm x) *R x"]
      unfolding linear_simps(5)[OF blin_comb']
      apply auto
      by (simp add: le_divide_eq)
  qed

  have *:  "norm (repr' ψ)  norm ψ * D" for ψ
  proof (cases "ψ  real_vector.span B")
    show "norm (repr' ψ)  norm ψ * D"
      if "ψ  span B"
      using that     unfolding D_def
      using norm_comb'[of "repr' ψ"] d>0
      by (simp_all add: linordered_field_class.mult_imp_le_div_pos mult.commute)

    show "norm (repr' ψ)  norm ψ * D"
      if "ψ  span B"
      using that 0 < D by auto
  qed

  hence "norm (Rep_euclidean_space (repr' ψ) (abs b))  norm ψ * D" for ψ
  proof -
    have "(Rep_euclidean_space (repr' ψ) (abs b)) = repr' ψ  euclidean_space_basis_vector (abs b)"
      apply (transfer fixing: abs b)
      by auto
    also have "¦¦  norm (repr' ψ)"
      apply (rule Basis_le_norm)
      unfolding Basis_euclidean_space_def by simp
    also have "  norm ψ * D"
      using * by auto
    finally show ?thesis by simp
  qed
  hence "norm (repr ψ b)  norm ψ * D" for ψ
    unfolding repr'_def
    by (smt comb'  λl. comb (Rep_euclidean_space l  abs)
        repr'  λψ. Abs_euclidean_space (repr ψ  rep) comb'_repr' comp_apply norm_le_zero_iff
        repr_bad repr_comb)
  thus "D>0. ψ. norm (repr ψ b)  norm ψ * D"
    using D>0 by auto
  from d>0
  have complete_comb': "complete (comb' ` UNIV)"
  proof (rule complete_isometric_image)
    show "subspace (UNIV::'basis euclidean_space set)"
      by simp
    show "bounded_linear comb'"
      by (simp add: blin_comb')
    show "xUNIV. d * norm x  norm (comb' x)"
      by (simp add: norm_comb')
    show "complete (UNIV::'basis euclidean_space set)"
      by (simp add: complete UNIV)
  qed

  have range_comb': "comb' ` UNIV = real_vector.span B"
  proof (auto simp: image_def)
    show "comb' x  real_vector.span B" for x
      by (metis comb'_def comb_cong comb_repr local.repr_def repr_bad repr_comb real_vector.representation_zero real_vector.span_zero)
  next
    fix ψ assume "ψ  real_vector.span B"
    then obtain f where f: "comb f = ψ"
      apply atomize_elim
      unfolding span_finite[OF finite B] comb_def
      by auto
    define f' where "f' b = (if bB then f b else 0)" for b :: 'b
    have f': "comb f' = ψ"
      unfolding f[symmetric]
      apply (rule comb_cong)
      unfolding f'_def by simp
    define x :: "'basis euclidean_space" where "x = Abs_euclidean_space (f' o rep)"
    have "ψ = comb' x"
      by (metis (no_types, lifting) ψ  span B repr'  λψ. Abs_euclidean_space (repr ψ  rep)
          comb'_repr' f' fun.map_cong repr_comb t type_definition.Rep_range x_def)
    thus "x. ψ = comb' x"
      by auto
  qed

  from range_comb' complete_comb'
  show "complete (real_vector.span B)"
    by simp
qed

lemma finite_span_complete[simp]:
  fixes A :: "'a::real_normed_vector set"
  assumes "finite A"
  shows "complete (span A)"
  text ‹The span of a finite set is complete.›
proof (cases "A  {}  A  {0}")
  case True
  obtain B where
    BT: "real_vector.span B = real_vector.span A"
    and "independent B"
    and "finite B"
    by (meson True assms finite_subset real_vector.maximal_independent_subset real_vector.span_eq
        real_vector.span_superset subset_trans)

  have "B{}"
    apply (rule ccontr, simp)
    using BT True
    by (metis real_vector.span_superset real_vector.span_empty subset_singletonD)

(* The following generalizes finite_span_complete_aux to hold without the assumption
     that 'basis has type class finite *)
  {
    (* The type variable 'basisT must not be the same as the one used in finite_span_complete_aux,
       otherwise "internalize_sort" below fails *)
    assume "(Rep :: 'basisT'a) Abs. type_definition Rep Abs B"
    then obtain rep :: "'basisT  'a" and abs :: "'a  'basisT" where t: "type_definition rep abs B"
      by auto
    have basisT_finite: "class.finite TYPE('basisT)"
      apply intro_classes
      using finite B t
      by (metis (mono_tags, opaque_lifting) ex_new_if_finite finite_imageI image_eqI type_definition_def)
    note finite_span_complete_aux(2)[internalize_sort "'basis::finite"]
    note this[OF basisT_finite t]
  }
  note this[cancel_type_definition, OF B{} finite B _ independent B]
  hence "complete (real_vector.span B)"
    using B{} by auto
  thus "complete (real_vector.span A)"
    unfolding BT by simp
next
  case False
  thus ?thesis
    using complete_singleton by auto
qed

lemma finite_span_representation_bounded:
  fixes B :: "'a::real_normed_vector set"
  assumes "finite B" and "independent B"
  shows "D>0. ψ b. abs (representation B ψ b)  norm ψ * D"

  text ‹
  Assume $B$ is a finite linear independent set of vectors (in a real normed vector space).
  Let $\alpha^\psi_b$ be the coefficients of $\psi$ expressed as a linear combination over $B$.
  Then $\alpha$ is is uniformly cblinfun (i.e., $\lvert\alpha^\psi_b \leq D \lVert\psi\rVert\psi$
  for some $D$ independent of $\psi,b$).

  (This also holds when $b$ is not in the span of $B$ because of the way real_vector.representation›
  is defined in this corner case.)›

proof (cases "B{}")
  case True

(* The following generalizes finite_span_complete_aux to hold without the assumption
     that 'basis has type class finite *)
  define repr  where "repr = real_vector.representation B"
  {
    (* Step 1: Create a fake type definition by introducing a new type variable 'basis
               and then assuming the existence of the morphisms Rep/Abs to B
               This is then roughly equivalent to "typedef 'basis = B" *)
    (* The type variable 'basisT must not be the same as the one used in finite_span_complete_aux
       (I.e., we cannot call it 'basis) *)
    assume "(Rep :: 'basisT'a) Abs. type_definition Rep Abs B"
    then obtain rep :: "'basisT  'a" and abs :: "'a  'basisT" where t: "type_definition rep abs B"
      by auto
        (* Step 2: We show that our fake typedef 'basisT could be instantiated as type class finite *)
    have basisT_finite: "class.finite TYPE('basisT)"
      apply intro_classes
      using finite B t
      by (metis (mono_tags, opaque_lifting) ex_new_if_finite finite_imageI image_eqI type_definition_def)
        (* Step 3: We take the finite_span_complete_aux and remove the requirement that 'basis::finite
               (instead, a precondition "class.finite TYPE('basisT)" is introduced) *)
    note finite_span_complete_aux(1)[internalize_sort "'basis::finite"]
      (* Step 4: We instantiate the premises *)
    note this[OF basisT_finite t]
  }
    (* Now we have the desired fact, except that it still assumes that B is isomorphic to some type 'basis
     together with the assumption that there are morphisms between 'basis and B. 'basis and that premise
     are removed using cancel_type_definition
  *)
  note this[cancel_type_definition, OF True finite B _ independent B]

  hence d2:"D. ψ. D>0  norm (repr ψ b)  norm ψ * D" if bB for b
    by (simp add: repr_def that True)
  have d1: " (b. b  B 
          D. ψ. 0 < D  norm (repr ψ b)  norm ψ * D) 
    D. b ψ. b  B 
               0 < D b  norm (repr ψ b)  norm ψ * D b"
    apply (rule choice) by auto
  then obtain D where D: "D b > 0  norm (repr ψ b)  norm ψ * D b" if "bB" for b ψ
    apply atomize_elim
    using d2 by blast

  hence Dpos: "D b > 0" and Dbound: "norm (repr ψ b)  norm ψ * D b"
    if "bB" for b ψ
    using that by auto
  define Dall where "Dall = Max (D`B)"
  have "Dall > 0"
    unfolding Dall_def using finite B B{} Dpos
    by (metis (mono_tags, lifting) Max_in finite_imageI image_iff image_is_empty)
  have "Dall  D b" if "bB" for b
    unfolding Dall_def using finite B that by auto
  with Dbound
  have "norm (repr ψ b)  norm ψ * Dall" if "bB" for b ψ
    using that
    by (smt mult_left_mono norm_not_less_zero)
  moreover have "norm (repr ψ b)  norm ψ * Dall" if "bB" for b ψ
    unfolding repr_def using real_vector.representation_ne_zero True
    by (metis calculation empty_subsetI less_le_trans local.repr_def norm_ge_zero norm_zero not_less
        subsetI subset_antisym)
  ultimately show "D>0. ψ b. abs (repr ψ b)  norm ψ * D"
    using Dall > 0 real_norm_def by metis
next
  case False
  thus ?thesis
    unfolding repr_def using real_vector.representation_ne_zero[of B]
    using nice_ordered_field_class.linordered_field_no_ub by fastforce
qed

hide_fact finite_span_complete_aux


lemma finite_cspan_complete[simp]:
  fixes B :: "'a::complex_normed_vector set"
  assumes "finite B"
  shows "complete (cspan B)"
  by (simp add: assms cspan_as_span)

lemma finite_span_closed[simp]:
  fixes B :: "'a::real_normed_vector set"
  assumes "finite B"
  shows "closed (real_vector.span B)"
  by (simp add: assms complete_imp_closed)


lemma finite_cspan_closed[simp]:
  fixes S::'a::complex_normed_vector set
  assumes a1: finite S
  shows closed (cspan S)
  by (simp add: assms complete_imp_closed)

lemma closure_finite_cspan:
  fixes T::'a::complex_normed_vector set
  assumes finite T
  shows closure (cspan T) = cspan T
  by (simp add: assms)


lemma finite_cspan_crepresentation_bounded:
  fixes B :: "'a::complex_normed_vector set"
  assumes a1: "finite B" and a2: "cindependent B"
  shows "D>0. ψ b. cmod (crepresentation B ψ b)  norm ψ * D"
proof -
  define B' where "B' = (B  scaleC 𝗂 ` B)"
  have independent_B': "independent B'"
    using B'_def cindependent B
    by (simp add: real_independent_from_complex_independent a1)
  have "finite B'"
    unfolding B'_def using finite B by simp
  obtain D' where "D' > 0" and D': "norm (real_vector.representation B' ψ b)  norm ψ * D'"
    for ψ b
    apply atomize_elim
    using independent_B' finite B'
    by (simp add: finite_span_representation_bounded)

  define D where "D = 2*D'"
  from D' > 0 have D > 0
    unfolding D_def by simp
  have "norm (crepresentation B ψ b)  norm ψ * D" for ψ b
  proof (cases "bB")
    case True
    have d3: "norm 𝗂 = 1"
      by simp

    have "norm (𝗂 *C complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))
          = norm 𝗂 * norm (complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))"
      using norm_scaleC by blast
    also have " = norm (complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))"
      using d3 by simp
    finally have d2:"norm (𝗂 *C complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))
          = norm (complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))".
    have "norm (crepresentation B ψ b)
        = norm (complex_of_real (real_vector.representation B' ψ b)
            + 𝗂 *C complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))"
      by (simp add: B'_def True a1 a2 crepresentation_from_representation)
    also have "  norm (complex_of_real (real_vector.representation B' ψ b))
             + norm (𝗂 *C complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))"
      using norm_triangle_ineq by blast
    also have " = norm (complex_of_real (real_vector.representation B' ψ b))
                  + norm (complex_of_real (real_vector.representation B' ψ (𝗂 *C b)))"
      using d2 by simp
    also have " = norm (real_vector.representation B' ψ b)
                  + norm (real_vector.representation B' ψ (𝗂 *C b))"
      by simp
    also have "  norm ψ * D' + norm ψ * D'"
      by (rule add_mono; rule D')
    also have "  norm ψ * D"
      unfolding D_def by linarith
    finally show ?thesis
      by auto
  next
    case False
    hence "crepresentation B ψ b = 0"
      using complex_vector.representation_ne_zero by blast
    thus ?thesis
      by (smt 0 < D norm_ge_zero norm_zero split_mult_pos_le)
  qed
  with D > 0
  show ?thesis
    by auto
qed

lemma bounded_clinear_finite_dim[simp]:
  fixes f :: 'a::{cfinite_dim,complex_normed_vector}  'b::complex_normed_vector
  assumes clinear f
  shows bounded_clinear f
proof -
  include notation_norm
  obtain basis :: 'a set where b1: "complex_vector.span basis = UNIV"
    and b2: "cindependent basis"
    and b3:"finite basis"
    using finite_basis by auto
  have "C>0. ψ b. cmod (crepresentation basis ψ b)  ψ * C"
    using finite_cspan_crepresentation_bounded[where B = basis] b2 b3 by blast
  then obtain C where s1: "cmod (crepresentation basis ψ b)  ψ * C"
    and s2: "C > 0"
  for ψ b by blast
  define M where "M = C * (abasis. f a)"
  have "f x  x * M"
    for x
  proof-
    define r where "r b = crepresentation basis x b" for b
    have x_span: "x  complex_vector.span basis"
      by (simp add: b1)
    have f0: "v  basis"
      if "r v  0" for v
      using complex_vector.representation_ne_zero r_def that by auto
    have w:"{a|a. r a  0}  basis"
      using f0 by blast
    hence f1: "finite {a|a. r a  0}"
      using b3 rev_finite_subset by auto
    have f2: "(a| r a  0. r a *C a) = x"
      unfolding r_def
      using b2 complex_vector.sum_nonzero_representation_eq x_span
        Collect_cong  by fastforce
    have g1: "(abasis. crepresentation basis x a *C a) = x"
      by (simp add: b2 b3 complex_vector.sum_representation_eq x_span)
    have f3: "(abasis. r a *C a) = x"
      unfolding r_def
      by (simp add: g1)
    hence "f x = f (abasis. r a *C a)"
      by simp
    also have " = (abasis. r a *C f a)"
      by (smt (verit, ccfv_SIG) assms complex_vector.linear_scale complex_vector.linear_sum sum.cong)
    finally have "f x = (abasis. r a *C f a)".
    hence "f x = (abasis. r a *C f a)"
      by simp
    also have "  (abasis. r a *C f a)"
      by (simp add: sum_norm_le)
    also have "  (abasis. r a * f a)"
      by simp
    also have "  (abasis. x * C * f a)"
      using sum_mono s1 unfolding r_def
      by (simp add: sum_mono mult_right_mono)
    also have "  x * C * (abasis. f a)"
      using sum_distrib_left
      by (smt sum.cong)
    also have " = x * M"
      unfolding M_def
      by linarith
    finally show ?thesis .
  qed
  thus ?thesis
    using assms bounded_clinear_def bounded_clinear_axioms_def by blast
qed

lemma summable_on_scaleR_left_converse:
  ― ‹This result has nothing to do with the bounded operator library but it
      uses @{thm [source] finite_span_closed} so it is proven here.›
  fixes f :: 'b  real
    and c :: 'a :: real_normed_vector
  assumes c  0
  assumes (λx. f x *R c) summable_on A
  shows f summable_on A
proof -
  define fromR toR T where fromR x = x *R c and toR = inv fromR and T = range fromR for x :: real
  have additive fromR
    by (simp add: fromR_def additive.intro scaleR_left_distrib)
  have inj fromR
    by (simp add: fromR_def c  0 inj_def)
  have toR_fromR: toR (fromR x) = x for x
    by (simp add: inj fromR toR_def)
  have fromR_toR: fromR (toR x) = x if x  T for x
    by (metis T_def f_inv_into_f that toR_def)

  have 1: sum (toR  (fromR  f)) F = toR (sum (fromR  f) F) if finite F for F
    by (simp add: o_def additive.sum[OF additive fromR, symmetric] toR_fromR)
  have 2: sum (fromR  f) F  T if finite F for F
    by (simp add: o_def additive.sum[OF additive fromR, symmetric] T_def)
  have 3: (toR  toR x) (at x within T) for x
  proof (cases x  T)
    case True
    have dist (toR y) (toR x) < e if yT e>0 dist y x < e * norm c for e y
    proof -
      obtain x' y' where x: x = fromR x' and y: y = fromR y'
        using T_def True y  T by blast
      have dist (toR y) (toR x) = dist (fromR (toR y)) (fromR (toR x)) / norm c
        by (auto simp: dist_real_def fromR_def c  0)
      also have  = dist y x / norm c
        using xT yT by (simp add: fromR_toR)
      also have  < e
        using dist y x < e * norm c
        by (simp add: divide_less_eq that(2))
      finally show ?thesis
        by (simp add: x y toR_fromR)
    qed
    then show ?thesis
      apply (auto simp: tendsto_iff at_within_def eventually_inf_principal eventually_nhds_metric)
      by (metis assms(1) div_0 divide_less_eq zero_less_norm_iff)
  next
    case False
    have T = span {c}
      by (simp add: T_def fromR_def span_singleton)
    then have closed T
      by simp
    with False have x  closure T
      by simp
    then have (at x within T) = bot
      by (rule not_in_closure_trivial_limitI)
    then show ?thesis
      by simp
  qed
  have 4: (fromR  f) summable_on A
    by (simp add: assms(2) fromR_def summable_on_cong)

  have (toR o (fromR o f)) summable_on A
    using 1 2 3 4 
    by (rule summable_on_comm_additive_general[where T=T])
  with toR_fromR
  show ?thesis
    by (auto simp: o_def)
qed

lemma infsum_scaleR_left:
  ― ‹This result has nothing to do with the bounded operator library but it
      uses @{thm [source] finite_span_closed} so it is proven here.

      It is a strengthening of @{thm [source] infsum_scaleR_left}.›
  fixes c :: 'a :: real_normed_vector
  shows "infsum (λx. f x *R c) A = infsum f A *R c"
proof (cases f summable_on A)
  case True
  then show ?thesis 
   apply (subst asm_rl[of (λx. f x *R c) = (λy. y *R c) o f], simp add: o_def)
   apply (rule infsum_comm_additive)
  using True by (auto simp add: scaleR_left.additive_axioms)
next
  case False
  then have ¬ (λx. f x *R c) summable_on A if c  0
    using summable_on_scaleR_left_converse[where A=A and f=f and c=c]
    using that by auto
  with False show ?thesis
    apply (cases c = 0)
    by (auto simp add: infsum_not_exists)
qed

lemma infsum_of_real: 
  shows (xA. of_real (f x) :: 'b::{real_normed_vector, real_algebra_1}) = of_real (xA. f x)
  ― ‹This result has nothing to do with the bounded operator library but it
      uses @{thm [source] finite_span_closed} so it is proven here.›
  unfolding of_real_def
  by (rule infsum_scaleR_left)



subsection ‹Closed subspaces›

lemma csubspace_INF[simp]: "(x. x  A  csubspace x)  csubspace (A)"
  by (simp add: complex_vector.subspace_Inter)

locale closed_csubspace =
  fixes A::"('a::{complex_vector,topological_space}) set"
  assumes subspace: "csubspace A"
  assumes closed: "closed A"

declare closed_csubspace.subspace[simp]

lemma closure_is_csubspace[simp]:
  fixes A::"('a::complex_normed_vector) set"
  assumes csubspace A
  shows csubspace (closure A)
proof-
  have "x  closure A  y  closure A  x+y  closure A" for x y
  proof-
    assume x(closure A)
    then obtain xx where  n::nat. xx n  A and xx  x
      using closure_sequential by blast
    assume y(closure A)
    then obtain yy where  n::nat. yy n  A and yy  y
      using closure_sequential by blast
    have  n::nat. (xx n) + (yy n)  A
      using n. xx n  A n. yy n  A assms complex_vector.subspace_def
      by (simp add: complex_vector.subspace_def)
    hence  (λ n. (xx n) + (yy n))  x + y using  xx  x yy  y
      by (simp add: tendsto_add)
    thus ?thesis using   n::nat. (xx n) + (yy n)  A
      by (meson closure_sequential)
  qed
  moreover have "x(closure A)  c *C x  (closure A)" for x c
  proof-
    assume x(closure A)
    then obtain xx where  n::nat. xx n  A and xx  x
      using closure_sequential by blast
    have  n::nat. c *C (xx n)  A
      using n. xx n  A assms complex_vector.subspace_def
      by (simp add: complex_vector.subspace_def)
    have isCont (λ t. c *C t) x
      using bounded_clinear.bounded_linear bounded_clinear_scaleC_right linear_continuous_at by auto
    hence  (λ n. c *C (xx n))  c *C x using  xx  x
      by (simp add: isCont_tendsto_compose)
    thus ?thesis using   n::nat. c *C (xx n)  A
      by (meson closure_sequential)
  qed
  moreover have "0  (closure A)"
    using assms closure_subset complex_vector.subspace_def
    by (metis in_mono)
  ultimately show ?thesis
    by (simp add: complex_vector.subspaceI)
qed

lemma csubspace_set_plus:
  assumes csubspace A and csubspace B
  shows csubspace (A + B)
proof -
  define C where C = {ψ+φ| ψ φ. ψA  φB}
  have  "xC  yC  x+yC" for x y
    using C_def assms(1) assms(2) complex_vector.subspace_add complex_vector.subspace_sums by blast
  moreover have "c *C x  C" if xC for x c
  proof -
    have "csubspace C"
      by (simp add: C_def assms(1) assms(2) complex_vector.subspace_sums)
    then show ?thesis
      using that by (simp add: complex_vector.subspace_def)
  qed
  moreover have  "0  C"
    using  C = {ψ + φ |ψ φ. ψ  A  φ  B} add.inverse_neutral add_uminus_conv_diff assms(1) assms(2) diff_0  mem_Collect_eq
      add.right_inverse
    by (metis (mono_tags, lifting) complex_vector.subspace_0)
  ultimately show ?thesis
    unfolding C_def complex_vector.subspace_def
    by (smt mem_Collect_eq set_plus_elim set_plus_intro)
qed

lemma closed_csubspace_0[simp]:
  "closed_csubspace ({0} :: ('a::{complex_vector,t1_space}) set)"
proof-
  have csubspace {0}
    using add.right_neutral complex_vector.subspace_def scaleC_right.zero
    by blast
  moreover have "closed ({0} :: 'a set)"
    by simp
  ultimately show ?thesis
    by (simp add: closed_csubspace_def)
qed

lemma closed_csubspace_UNIV[simp]: "closed_csubspace (UNIV::('a::{complex_vector,topological_space}) set)"
proof-
  have csubspace UNIV
    by simp
  moreover have closed UNIV
    by simp
  ultimately show ?thesis
    unfolding closed_csubspace_def by auto
qed

lemma closed_csubspace_inter[simp]:
  assumes "closed_csubspace A" and "closed_csubspace B"
  shows "closed_csubspace (AB)"
proof-
  obtain C where C = A  B by blast
  have csubspace C
  proof-
    have "xC  yC  x+yC" for x y
      by (metis IntD1 IntD2 IntI C = A  B assms(1) assms(2) complex_vector.subspace_def closed_csubspace_def)
    moreover have "xC  c *C x  C" for x c
      by (metis IntD1 IntD2 IntI C = A  B assms(1) assms(2) complex_vector.subspace_def closed_csubspace_def)
    moreover have "0  C"
      using  C = A  B assms(1) assms(2) complex_vector.subspace_def closed_csubspace_def by fastforce
    ultimately show ?thesis
      by (simp add: complex_vector.subspace_def)
  qed
  moreover have closed C
    using  C = A  B
    by (simp add: assms(1) assms(2) closed_Int closed_csubspace.closed)
  ultimately show ?thesis
    using  C = A  B
    by (simp add: closed_csubspace_def)
qed


lemma closed_csubspace_INF[simp]:
  assumes a1: "A𝒜. closed_csubspace A"
  shows "closed_csubspace (𝒜)"
proof-
  have csubspace (𝒜)
    by (simp add: assms closed_csubspace.subspace complex_vector.subspace_Inter)
  moreover have closed (𝒜)
    by (simp add: assms closed_Inter closed_csubspace.closed)
  ultimately show ?thesis
    by (simp add: closed_csubspace.intro)
qed


typedef (overloaded) ('a::"{complex_vector,topological_space}")
  ccsubspace = {S::'a set. closed_csubspace S}
  morphisms space_as_set Abs_ccsubspace
  using Complex_Vector_Spaces.closed_csubspace_UNIV by blast

setup_lifting type_definition_ccsubspace

lemma csubspace_space_as_set[simp]: csubspace (space_as_set S)
  by (metis closed_csubspace_def mem_Collect_eq space_as_set)

lemma closed_space_as_set[simp]: closed (space_as_set S)
  apply transfer by (simp add: closed_csubspace.closed)

lemma zero_space_as_set[simp]: 0  space_as_set A
  by (simp add: complex_vector.subspace_0)

instantiation ccsubspace :: (complex_normed_vector) scaleC begin
lift_definition scaleC_ccsubspace :: "complex  'a ccsubspace  'a ccsubspace" is
  "λc S. (*C) c ` S"
proof
  show "csubspace ((*C) c ` S)" if "closed_csubspace S" for c :: complex and S :: "'a set"
    using that
    by (simp add: complex_vector.linear_subspace_image)
  show "closed ((*C) c ` S)" if "closed_csubspace S" for c :: complex and S :: "'a set"
    using that
    by (simp add: closed_scaleC closed_csubspace.closed)
qed

lift_definition scaleR_ccsubspace :: "real  'a ccsubspace  'a ccsubspace" is
  "λc S. (*R) c ` S"
proof
  show "csubspace ((*R) r ` S)"
    if "closed_csubspace S"
    for r :: real
      and S :: "'a set"
    using that   using bounded_clinear_def bounded_clinear_scaleC_right scaleR_scaleC
    by (simp add: scaleR_scaleC complex_vector.linear_subspace_image)
  show "closed ((*R) r ` S)"
    if "closed_csubspace S"
    for r :: real
      and S :: "'a set"
    using that
    by (simp add: closed_scaling closed_csubspace.closed)
qed

instance
proof
  show "((*R) r::'a ccsubspace  _) = (*C) (complex_of_real r)" for r :: real
    by (simp add: scaleR_scaleC scaleC_ccsubspace_def scaleR_ccsubspace_def)
qed
end

instantiation ccsubspace :: ("{complex_vector,t1_space}") bot begin
lift_definition bot_ccsubspace :: 'a ccsubspace is {0}
  by simp
instance..
end

lemma zero_cblinfun_image[simp]: "0 *C S = bot" for S :: "_ ccsubspace"
proof transfer
  have "(0::'b)  (λx. 0) ` S"
    if "closed_csubspace S"
    for S::"'b set"
    using that unfolding closed_csubspace_def
    by (simp add: complex_vector.linear_subspace_image complex_vector.module_hom_zero
        complex_vector.subspace_0)
  thus "(*C) 0 ` S = {0::'b}"
    if "closed_csubspace (S::'b set)"
    for S :: "'b set"
    using that
    by (auto intro !: exI [of _ 0])
qed

lemma csubspace_scaleC_invariant:
  fixes a S
  assumes a  0 and csubspace S
  shows (*C) a ` S = S
proof-
  have  x  (*C) a ` S  x  S
    for x
    using assms(2) complex_vector.subspace_scale by blast
  moreover have  x  S  x  (*C) a ` S
    for x
  proof -
    assume "x  S"
    hence "c aa. (c / a) *C aa  S  c *C aa = x"
      using assms(2) complex_vector.subspace_def scaleC_one by metis
    hence "aa. aa  S  a *C aa = x"
      using assms(1) by auto
    thus ?thesis
      by (meson image_iff)
  qed
  ultimately show ?thesis by blast
qed


lemma ccsubspace_scaleC_invariant[simp]: "a  0  a *C S = S" for S :: "_ ccsubspace"
  apply transfer
  by (simp add: closed_csubspace.subspace csubspace_scaleC_invariant)


instantiation ccsubspace :: ("{complex_vector,topological_space}") "top"
begin
lift_definition top_ccsubspace :: 'a ccsubspace is UNIV
  by simp

instance ..
end

lemma space_as_set_bot[simp]: space_as_set bot = {0}
  by (rule bot_ccsubspace.rep_eq)

lemma ccsubspace_top_not_bot[simp]:
  "(top::'a::{complex_vector,t1_space,not_singleton} ccsubspace)  bot"
  (* The type class t1_space is needed because the definition of bot in ccsubspace needs it *)
  by (metis UNIV_not_singleton bot_ccsubspace.rep_eq top_ccsubspace.rep_eq)

lemma ccsubspace_bot_not_top[simp]:
  "(bot::'a::{complex_vector,t1_space,not_singleton} ccsubspace)  top"
  using ccsubspace_top_not_bot by metis

instantiation ccsubspace :: ("{complex_vector,topological_space}") "Inf"
begin
lift_definition Inf_ccsubspace::'a ccsubspace set  'a ccsubspace
  is λ S.  S
proof
  fix S :: "'a set set"
  assume closed: "closed_csubspace x" if x  S for x
  show "csubspace ( S::'a set)"
    by (simp add: closed closed_csubspace.subspace)
  show "closed ( S::'a set)"
    by (simp add: closed closed_csubspace.closed)
qed

instance ..
end

lift_definition ccspan :: "'a::complex_normed_vector set  'a ccsubspace"
  is "λG. closure (cspan G)"
proof (rule closed_csubspace.intro)
  fix S :: "'a set"
  show "csubspace (closure (cspan S))"
    by (simp add: closure_is_csubspace)
  show "closed (closure (cspan S))"
    by simp
qed

lemma ccspan_superset:
  A  space_as_set (ccspan A)
  for A :: 'a::complex_normed_vector set
  apply transfer
  by (meson closure_subset complex_vector.span_superset subset_trans)

lemma ccspan_superset': x  X  x  space_as_set (ccspan X)
  using ccspan_superset by auto

lemma ccspan_canonical_basis[simp]: "ccspan (set canonical_basis) = top"
  using ccspan.rep_eq space_as_set_inject top_ccsubspace.rep_eq
    closure_UNIV is_generator_set
  by metis

lemma ccspan_Inf_def: ccspan A = Inf {S. A  space_as_set S}
  for A::('a::cbanach) set
proof -
  have x  space_as_set (ccspan A)
     x  space_as_set (Inf {S. A  space_as_set S})
    for x::'a
  proof-
    assume x  space_as_set (ccspan A)
    hence "x  closure (cspan A)"
      by (simp add: ccspan.rep_eq)
    hence x  closure (complex_vector.span A)
      unfolding ccspan_def
      by simp
    hence  y::nat  'a. ( n. y n  (complex_vector.span A))  y  x
      by (simp add: closure_sequential)
    then obtain y where  n. y n  (complex_vector.span A) and y  x
      by blast
    have y n   {S. (complex_vector.span A)  S  closed_csubspace S}
      for n
      using   n. y n  (complex_vector.span A)
      by auto

    have closed_csubspace S  closed S
      for S::'a set
      by (simp add: closed_csubspace.closed)
    hence closed (  {S. (complex_vector.span A)  S  closed_csubspace S})
      by simp
    hence x   {S. (complex_vector.span A)  S  closed_csubspace S} using y  x
      using n. y n   {S. complex_vector.span A  S  closed_csubspace S} closed_sequentially
      by blast
    moreover have {S. A  S  closed_csubspace S}  {S. (complex_vector.span A)  S  closed_csubspace S}
      using Collect_mono_iff
      by (simp add: Collect_mono_iff closed_csubspace.subspace complex_vector.span_minimal)
    ultimately have x   {S. A  S  closed_csubspace S}
      by blast
    moreover have "(x::'a)   {x. A  x  closed_csubspace x}"
      if "(x::'a)   {S. A  S  closed_csubspace S}"
      for x :: 'a
        and A :: "'a set"
      using that
      by simp
    ultimately show x  space_as_set (Inf {S. A  space_as_set S})
      apply transfer.
  qed
  moreover have x  space_as_set (Inf {S. A  space_as_set S})
              x  space_as_set (ccspan A)
    for x::'a
  proof-
    assume x  space_as_set (Inf {S. A  space_as_set S})
    hence x   {S. A  S  closed_csubspace S}
      apply transfer
      by blast
    moreover have {S. (complex_vector.span A)  S  closed_csubspace S}  {S. A  S  closed_csubspace S}
      using Collect_mono_iff complex_vector.span_superset by fastforce
    ultimately have x   {S. (complex_vector.span A)  S  closed_csubspace S}
      by blast
    thus x  space_as_set (ccspan A)
      by (metis (no_types, lifting) Inter_iff space_as_set closure_subset mem_Collect_eq ccspan.rep_eq)
  qed
  ultimately have space_as_set (ccspan A) = space_as_set (Inf {S. A  space_as_set S})
    by blast
  thus ?thesis
    using space_as_set_inject by auto
qed

lemma cspan_singleton_scaleC[simp]: "(a::complex)0  cspan { a *C ψ } = cspan {ψ}"
  for ψ::"'a::complex_vector"
  by (smt complex_vector.dependent_single complex_vector.independent_insert
      complex_vector.scale_eq_0_iff complex_vector.span_base complex_vector.span_redundant
      complex_vector.span_scale doubleton_eq_iff insert_absorb insert_absorb2 insert_commute
      singletonI)

lemma closure_is_closed_csubspace[simp]:
  fixes S::'a::complex_normed_vector set
  assumes csubspace S
  shows closed_csubspace (closure S)
  using assms closed_csubspace.intro closure_is_csubspace by blast

lemma ccspan_singleton_scaleC[simp]: "(a::complex)0  ccspan {a *C ψ} = ccspan {ψ}"
  apply transfer by simp

lemma clinear_continuous_at:
  assumes bounded_clinear f
  shows isCont f x
  by (simp add: assms bounded_clinear.bounded_linear linear_continuous_at)

lemma clinear_continuous_within:
  assumes bounded_clinear f
  shows continuous (at x within s) f
  by (simp add: assms bounded_clinear.bounded_linear linear_continuous_within)

lemma antilinear_continuous_at:
  assumes bounded_antilinear f
  shows isCont f x
  by (simp add: assms bounded_antilinear.bounded_linear linear_continuous_at)

lemma antilinear_continuous_within:
  assumes bounded_antilinear f
  shows continuous (at x within s) f
  by (simp add: assms bounded_antilinear.bounded_linear linear_continuous_within)

lemma bounded_clinear_eq_on_closure:
  fixes A B :: "'a::complex_normed_vector  'b::complex_normed_vector"
  assumes bounded_clinear A and bounded_clinear B and
    eq: x. x  G  A x = B x and t: t  closure (cspan G)
  shows A t = B t
proof -
  have eq': A t = B t if t  cspan G for t
    using _ _ that eq apply (rule complex_vector.linear_eq_on)
    by (auto simp: assms bounded_clinear.clinear)
  have A t - B t = 0
    using _ _ t apply (rule continuous_constant_on_closure)
    by (auto simp add: eq' assms(1) assms(2) clinear_continuous_at continuous_at_imp_continuous_on)
  then show ?thesis
    by auto
qed

instantiation ccsubspace :: ("{complex_vector,topological_space}") "order"
begin
lift_definition less_eq_ccsubspace :: 'a ccsubspace  'a ccsubspace  bool
  is  (⊆).
declare less_eq_ccsubspace_def[code del]
lift_definition less_ccsubspace :: 'a ccsubspace  'a ccsubspace  bool
  is (⊂).
declare less_ccsubspace_def[code del]
instance
proof
  fix x y z :: "'a ccsubspace"
  show "(x < y) = (x  y  ¬ y  x)"
    by (simp add: less_eq_ccsubspace.rep_eq less_le_not_le less_ccsubspace.rep_eq)
  show "x  x"
    by (simp add: less_eq_ccsubspace.rep_eq)
  show "x  z" if "x  y" and "y  z"
    using that less_eq_ccsubspace.rep_eq by auto
  show "x = y" if "x  y" and "y  x"
    using that by (simp add: space_as_set_inject less_eq_ccsubspace.rep_eq)
qed
end

lemma ccspan_leqI:
  assumes M  space_as_set S
  shows ccspan M  S
  using assms apply transfer
  by (simp add: closed_csubspace.closed closure_minimal complex_vector.span_minimal)

lemma ccspan_mono:
  assumes A  B
  shows ccspan A  ccspan B
  apply (transfer fixing: A B)
  by (simp add: assms closure_mono complex_vector.span_mono)

lemma ccsubspace_leI:
  assumes t1: "space_as_set A  space_as_set B"
  shows "A  B"
  using t1 apply transfer by -

lemma ccspan_of_empty[simp]: "ccspan {} = bot"
proof transfer
  show "closure (cspan {}) = {0::'a}"
    by simp
qed


instantiation ccsubspace :: ("{complex_vector,topological_space}") inf begin
lift_definition inf_ccsubspace :: "'a ccsubspace  'a ccsubspace  'a ccsubspace"
  is "(∩)" by simp
instance .. end

lemma space_as_set_inf[simp]: "space_as_set (A  B) = space_as_set A  space_as_set B"
  by (rule inf_ccsubspace.rep_eq)

instantiation ccsubspace :: ("{complex_vector,topological_space}") order_top begin
instance
proof
  show "a  "
    for a :: "'a ccsubspace"
    apply transfer
    by simp
qed
end


instantiation ccsubspace :: ("{complex_vector,t1_space}") order_bot begin
instance
proof
  show "(::'a ccsubspace)  a"
    for a :: "'a ccsubspace"
    apply transfer
    apply auto
    using closed_csubspace.subspace complex_vector.subspace_0 by blast
qed
end


instantiation ccsubspace :: ("{complex_vector,topological_space}") semilattice_inf begin
instance
proof
  fix x y z :: 'a ccsubspace
  show "x  y  x"
    apply transfer by simp
  show "x  y  y"
    apply transfer by simp
  show "x  y  z" if "x  y" and "x  z"
    using that apply transfer by simp
qed
end


instantiation ccsubspace :: ("{complex_vector,t1_space}") zero begin
definition zero_ccsubspace :: "'a ccsubspace" where [simp]: "zero_ccsubspace = bot"
lemma zero_ccsubspace_transfer[transfer_rule]: pcr_ccsubspace (=) {0} 0
  unfolding zero_ccsubspace_def by transfer_prover
instance ..
end

lemma ccspan_0[simp]: ccspan {0} = 0
  apply transfer
  by simp

definition rel_ccsubspace R x y = rel_set R (space_as_set x) (space_as_set y)


lemma left_unique_rel_ccsubspace[transfer_rule]: left_unique (rel_ccsubspace R) if left_unique R
proof (rule left_uniqueI)
  fix S T :: 'a ccsubspace and U
  assume assms: rel_ccsubspace R S U rel_ccsubspace R T U
  have space_as_set S = space_as_set T
    apply (rule left_uniqueD)
      using that apply (rule left_unique_rel_set)
    using assms unfolding rel_ccsubspace_def by auto
  then show S = T
    by (simp add: space_as_set_inject)
qed

lemma right_unique_rel_ccsubspace[transfer_rule]: right_unique (rel_ccsubspace R) if right_unique R
  by (metis rel_ccsubspace_def right_unique_def right_unique_rel_set space_as_set_inject that)

lemma bi_unique_rel_ccsubspace[transfer_rule]: bi_unique (rel_ccsubspace R) if bi_unique R
  by (metis (no_types, lifting) bi_unique_def bi_unique_rel_set rel_ccsubspace_def space_as_set_inject that)

lemma converse_rel_ccsubspace: conversep (rel_ccsubspace R) = rel_ccsubspace (conversep R)
  by (auto simp: rel_ccsubspace_def[abs_def])

lemma space_as_set_top[simp]: space_as_set top = UNIV
  by (rule top_ccsubspace.rep_eq)

lemma ccsubspace_eqI:
  assumes x. x  space_as_set S  x  space_as_set T
  shows S = T
  by (metis Abs_ccsubspace_cases Abs_ccsubspace_inverse antisym assms subsetI)

lemma ccspan_remove_0: ccspan (A - {0}) = ccspan A
  apply transfer
  by auto

lemma sgn_in_spaceD: ψ  space_as_set A if sgn ψ  space_as_set A and ψ  0
  for ψ :: _ :: complex_normed_vector
  using that
  apply (transfer fixing: ψ)
  by (metis closed_csubspace.subspace complex_vector.subspace_scale divideC_field_simps(1) scaleR_eq_0_iff scaleR_scaleC sgn_div_norm sgn_zero_iff)

lemma sgn_in_spaceI: sgn ψ  space_as_set A if ψ  space_as_set A 
  for ψ :: _ :: complex_normed_vector
  using that by (auto simp: sgn_div_norm scaleR_scaleC complex_vector.subspace_scale)

lemma ccsubspace_leI_unit:
  fixes A B :: _ :: complex_normed_vector ccsubspace
  assumes "ψ. norm ψ = 1  ψ  space_as_set A  ψ  space_as_set B"
  shows "A  B"
proof (rule ccsubspace_leI, rule subsetI)
  fix ψ assume ψA: ψ  space_as_set A
  show ψ  space_as_set B
    apply (cases ψ = 0)
    apply simp
    using assms[of sgn ψ] ψA sgn_in_spaceD sgn_in_spaceI 
    by (auto simp: norm_sgn)
qed

lemma kernel_is_closed_csubspace[simp]:
  assumes a1: "bounded_clinear f"
  shows "closed_csubspace (f -` {0})"
proof-
  have csubspace (f -` {0})
    using assms bounded_clinear.clinear complex_vector.linear_subspace_vimage complex_vector.subspace_single_0 by blast
  have "L  {x. f x = 0}"
    if "r  L" and " n. r n  {x. f x = 0}"
    for r and  L
  proof-
    have d1:  n. f (r n) = 0
      using that(2) by auto
    have (λ n. f (r n))  f L
      using assms clinear_continuous_at continuous_within_tendsto_compose' that(1)
      by fastforce
    hence (λ n. 0)  f L
      using d1 by simp
    hence f L = 0
      using limI by fastforce
    thus ?thesis by blast
  qed
  then have s3: closed (f -` {0})
    using closed_sequential_limits by force
  with csubspace (f -` {0})
  show ?thesis
    using closed_csubspace.intro by blast
qed

lemma ccspan_closure[simp]: ccspan (closure X) = ccspan X
  by (simp add: basic_trans_rules(24) ccspan.rep_eq ccspan_leqI ccspan_mono closure_mono closure_subset complex_vector.span_superset)

lemma ccspan_finite: space_as_set (ccspan X) = cspan X if finite X
  by (simp add: ccspan.rep_eq that)

lemma ccspan_UNIV[simp]: ccspan UNIV = 
  by (simp add: ccspan.abs_eq top_ccsubspace_def)

lemma infsum_in_closed_csubspaceI:
  assumes x. xX  f x  A
  assumes closed_csubspace A
  shows infsum f X  A
proof (cases f summable_on X)
  case True
  then have lim: (sum f  infsum f X) (finite_subsets_at_top X)
    by (simp add: infsum_tendsto)
  have sumA: sum f F  A if finite F and F  X for F
    apply (rule complex_vector.subspace_sum)
    using that assms by auto
  from lim show infsum f X  A
    apply (rule Lim_in_closed_set[rotated -1])
    using assms sumA by (auto intro!: closed_csubspace.closed eventually_finite_subsets_at_top_weakI)
next
  case False
  then show ?thesis
    using assms by (auto intro!: closed_csubspace.closed complex_vector.subspace_0 simp add: infsum_not_exists)
qed

lemma closed_csubspace_space_as_set[simp]: closed_csubspace (space_as_set X)
  using space_as_set by simp

subsection ‹Closed sums›

definition closed_sum:: 'a::{semigroup_add,topological_space} set  'a set  'a set where
  closed_sum A B = closure (A + B)

notation closed_sum (infixl "+M" 65)

lemma closed_sum_comm: A +M B = B +M A for A B :: "_::ab_semigroup_add"
  by (simp add: add.commute closed_sum_def)

lemma closed_sum_left_subset: 0  B  A  A +M B for A B :: "_::monoid_add"
  by (metis add.right_neutral closed_sum_def closure_subset in_mono set_plus_intro subsetI)

lemma closed_sum_right_subset: 0  A  B  A +M B for A B :: "_::monoid_add"
  by (metis add.left_neutral closed_sum_def closure_subset set_plus_intro subset_iff)

lemma finite_cspan_closed_csubspace:
  assumes "finite (S::'a::complex_normed_vector set)"
  shows "closed_csubspace (cspan S)"
  by (simp add: assms closed_csubspace.intro)

lemma closed_sum_is_sup:
  fixes A B C:: ('a::{complex_vector,topological_space}) set
  assumes closed_csubspace C
  assumes A  C and B  C
  shows (A +M B)  C
proof -
  have A + B  C
    using assms unfolding set_plus_def
    using closed_csubspace.subspace complex_vector.subspace_add by blast
  then show (A +M B)  C
    unfolding closed_sum_def
    using closed_csubspace C
    by (simp add: closed_csubspace.closed closure_minimal)
qed

lemma closed_subspace_closed_sum:
  fixes A B::"('a::complex_normed_vector) set"
  assumes a1: csubspace A and a2: csubspace B
  shows closed_csubspace (A +M B)
  using a1 a2 closed_sum_def
  by (metis closure_is_closed_csubspace csubspace_set_plus)


lemma closed_sum_assoc:
  fixes A B C::"'a::real_normed_vector set"
  shows A +M (B +M C) = (A +M B) +M C
proof -
  have A + closure B  closure (A + B) for A B :: "'a set"
    by (meson closure_subset closure_sum dual_order.trans order_refl set_plus_mono2)
  then have A +M (B +M C) = closure (A + (B + C))
    unfolding closed_sum_def
    by (meson antisym_conv closed_closure closure_minimal closure_mono closure_subset equalityD1 set_plus_mono2)
  moreover
  have closure A + B  closure (A + B) for A B :: "'a set"
    by (meson closure_subset closure_sum dual_order.trans order_refl set_plus_mono2)
  then have (A +M B) +M C = closure ((A + B) + C)
    unfolding closed_sum_def
    by (meson closed_closure closure_minimal closure_mono closure_subset eq_iff set_plus_mono2)
  ultimately show ?thesis
    by (simp add: ab_semigroup_add_class.add_ac(1))
qed


lemma closed_sum_zero_left[simp]:
  fixes A :: ('a::{monoid_add, topological_space}) set
  shows {0} +M A = closure A
  unfolding closed_sum_def
  by (metis add.left_neutral set_zero)

lemma closed_sum_zero_right[simp]:
  fixes A :: ('a::{monoid_add, topological_space}) set
  shows A +M {0} = closure A
  unfolding closed_sum_def
  by (metis add.right_neutral set_zero)

lemma closed_sum_closure_right[simp]:
  fixes A B :: 'a::real_normed_vector set
  shows A +M closure B = A +M B
  by (metis closed_sum_assoc closed_sum_def closed_sum_zero_right closure_closure)

lemma closed_sum_closure_left[simp]:
  fixes A B :: 'a::real_normed_vector set
  shows closure A +M B = A +M B
  by (simp add: closed_sum_comm)

lemma closed_sum_mono_left:
  assumes A  B
  shows A +M C  B +M C
  by (simp add: assms closed_sum_def closure_mono set_plus_mono2)

lemma closed_sum_mono_right:
  assumes A  B
  shows C +M A  C +M B
  by (simp add: assms closed_sum_def closure_mono set_plus_mono2)

instantiation ccsubspace :: (complex_normed_vector) sup begin
lift_definition sup_ccsubspace :: "'a ccsubspace  'a ccsubspace  'a ccsubspace"
  ― ‹Note that termA+B would not be a closed subspace, we need the closure. See, e.g., 🌐‹https://math.stackexchange.com/a/1786792/403528›.›
  is "λA B::'a set. A +M B"
  by (simp add: closed_subspace_closed_sum)
instance ..
end

lemma closed_sum_cspan[simp]:
  shows cspan X +M cspan Y = closure (cspan (X  Y))
  by (smt (verit, best) Collect_cong closed_sum_def complex_vector.span_Un set_plus_def)

lemma closure_image_closed_sum:
  assumes bounded_linear U
  shows closure (U ` (A +M B)) = closure (U ` A) +M closure (U ` B)
proof -
  have closure (U ` (A +M B)) = closure (U ` closure (closure A + closure B))
    unfolding closed_sum_def
    by (smt (verit, best) closed_closure closure_minimal closure_mono closure_subset closure_sum set_plus_mono2 subset_antisym)
  also have  = closure (U ` (closure A + closure B))
    using assms closure_bounded_linear_image_subset_eq by blast
  also have  = closure (U ` closure A + U ` closure B)
    apply (subst image_set_plus)
    by (simp_all add: assms bounded_linear.linear)
  also have  = closure (closure (U ` A) + closure (U ` B))
    by (smt (verit, ccfv_SIG) assms closed_closure closure_bounded_linear_image_subset closure_bounded_linear_image_subset_eq closure_minimal closure_mono closure_sum dual_order.eq_iff set_plus_mono2)
  also have  = closure (U ` A) +M closure (U ` B)
    using closed_sum_def by blast
  finally show ?thesis
    by -
qed



lemma ccspan_union: "ccspan A  ccspan B = ccspan (A  B)"
  apply transfer by simp

instantiation ccsubspace :: (complex_normed_vector) "Sup"
begin
lift_definition Sup_ccsubspace::'a ccsubspace set  'a ccsubspace
  is λS. closure (complex_vector.span (Union S))
proof
  show "csubspace (closure (complex_vector.span ( S::'a set)))"
    if "x::'a set. x  S  closed_csubspace x"
    for S :: "'a set set"
    using that
    by (simp add: closure_is_closed_csubspace)
  show "closed (closure (complex_vector.span ( S::'a set)))"
    if "x. (x::'a set)  S  closed_csubspace x"
    for S :: "'a set set"
    using that
    by simp
qed

instance..
end


instance ccsubspace :: ("{complex_normed_vector}") semilattice_sup
proof
  fix x y z :: 'a ccsubspace
  show x  sup x y
    apply transfer
    by (simp add: closed_csubspace_def closed_sum_left_subset complex_vector.subspace_0)

  show "y  sup x y"
    apply transfer
    by (simp add: closed_csubspace_def closed_sum_right_subset complex_vector.subspace_0)

  show "sup x y  z" if "x  z" and "y  z"
    using that apply transfer
    apply (rule closed_sum_is_sup) by auto
qed

instance ccsubspace :: (complex_normed_vector) complete_lattice
proof
  show "Inf A  x" if "x  A"
    for x :: "'a ccsubspace" and A :: "'a ccsubspace set"
    using that
    apply transfer
    by auto

  have b1: "z   A"
    if "Ball A closed_csubspace" and
      "closed_csubspace z" and
      "(x. closed_csubspace x  x  A  z  x)"
    for z::"'a set" and A
    using that
    by auto
  show "z  Inf A"
    if "x::'a ccsubspace. x  A  z  x"
    for A :: "'a ccsubspace set"
      and z :: "'a ccsubspace"
    using that
    apply transfer
    using b1 by blast

  show "x  Sup A"
    if "x  A"
    for x :: "'a ccsubspace"
      and A :: "'a ccsubspace set"
    using that
    apply transfer
    by (meson Union_upper closure_subset complex_vector.span_superset dual_order.trans)

  show "Sup A  z"
    if "x::'a ccsubspace. x  A  x  z"
    for A :: "'a ccsubspace set"
      and z :: "'a ccsubspace"
    using that apply transfer
  proof -
    fix A :: "'a set set" and z :: "'a set"
    assume A_closed: "Ball A closed_csubspace"
    assume "closed_csubspace z"
    assume in_z: "x. closed_csubspace x  x  A  x  z"
    from A_closed in_z
    have V  z if V  A for V
      by (simp add: that)
    then have  A  z
      by (simp add: Sup_le_iff)
    with closed_csubspace z
    show "closure (cspan ( A))  z"
      by (simp add: closed_csubspace_def closure_minimal complex_vector.span_def subset_hull)
  qed

  show "Inf {} = (top::'a ccsubspace)"
    using z A. (x. x  A  z  x)  z  Inf A top.extremum_uniqueI by auto

  show "Sup {} = (bot::'a ccsubspace)"
    using z A. (x. x  A  x  z)  Sup A  z bot.extremum_uniqueI by auto
qed

instantiation ccsubspace :: (complex_normed_vector) comm_monoid_add begin
definition plus_ccsubspace :: "'a ccsubspace  _  _"
  where [simp]: "plus_ccsubspace = sup"
instance
proof
  fix a b c :: 'a ccsubspace
  show "a + b + c = a + (b + c)"
    using sup.assoc by auto
  show "a + b = b + a"
    by (simp add: sup.commute)
  show "0 + a = a"
    by (simp add: zero_ccsubspace_def)
qed
end

lemma SUP_ccspan: (SUP xX. ccspan (S x)) = ccspan (xX. S x)
proof (rule SUP_eqI)
  show ccspan (S x)  ccspan (xX. S x) if x  X for x
    apply (rule ccspan_mono)
    using that by auto
  show ccspan (xX. S x)  y if x. x  X  ccspan (S x)  y for y
    apply (intro ccspan_leqI UN_least)
    using that ccspan_superset by (auto simp: less_eq_ccsubspace.rep_eq)
qed

lemma ccsubspace_plus_sup: "y  x  z  x  y + z  x"
  for x y z :: "'a::complex_normed_vector ccsubspace"
  unfolding plus_ccsubspace_def by auto

lemma ccsubspace_Sup_empty: "Sup {} = (0::_ ccsubspace)"
  unfolding zero_ccsubspace_def by auto

lemma ccsubspace_add_right_incr[simp]: "a  a + c" for a::"_ ccsubspace"
  by (simp add: add_increasing2)

lemma ccsubspace_add_left_incr[simp]: "a  c + a" for a::"_ ccsubspace"
  by (simp add: add_increasing)

lemma sum_bot_ccsubspace[simp]: (xX. ) = ( :: _ ccsubspace)
  by (simp flip: zero_ccsubspace_def)

subsection ‹Conjugate space›

typedef 'a conjugate_space = "UNIV :: 'a set"
  morphisms from_conjugate_space to_conjugate_space ..
setup_lifting type_definition_conjugate_space

instantiation conjugate_space :: (complex_vector) complex_vector begin
lift_definition scaleC_conjugate_space :: complex  'a conjugate_space  'a conjugate_space is λc x. cnj c *C x.
lift_definition scaleR_conjugate_space :: real  'a conjugate_space  'a conjugate_space is λr x. r *R x.
lift_definition plus_conjugate_space :: "'a conjugate_space  'a conjugate_space  'a conjugate_space" is "(+)".
lift_definition uminus_conjugate_space :: "'a conjugate_space  'a conjugate_space" is λx. -x.
lift_definition zero_conjugate_space :: "'a conjugate_space" is 0.
lift_definition minus_conjugate_space :: "'a conjugate_space  'a conjugate_space  'a conjugate_space" is "(-)".
instance
  apply (intro_classes; transfer)
  by (simp_all add: scaleR_scaleC scaleC_add_right scaleC_left.add)
end

instantiation conjugate_space :: (complex_normed_vector) complex_normed_vector begin
lift_definition sgn_conjugate_space :: "'a conjugate_space  'a conjugate_space" is "sgn".
lift_definition norm_conjugate_space :: "'a conjugate_space  real" is norm.
lift_definition dist_conjugate_space :: "'a conjugate_space  'a conjugate_space  real" is dist.
lift_definition uniformity_conjugate_space :: "('a conjugate_space × 'a conjugate_space) filter" is uniformity.
lift_definition  open_conjugate_space :: "'a conjugate_space set  bool" is "open".
instance
  apply (intro_classes; transfer)
  by (simp_all add: dist_norm sgn_div_norm open_uniformity uniformity_dist norm_triangle_ineq)
end

instantiation conjugate_space :: (cbanach) cbanach begin
instance
  apply intro_classes
  unfolding Cauchy_def convergent_def LIMSEQ_def apply transfer
  using Cauchy_convergent unfolding Cauchy_def convergent_def LIMSEQ_def by metis
end

lemma bounded_antilinear_to_conjugate_space[simp]: bounded_antilinear to_conjugate_space
  by (rule bounded_antilinear_intro[where K=1]; transfer; auto)

lemma bounded_antilinear_from_conjugate_space[simp]: bounded_antilinear from_conjugate_space
  by (rule bounded_antilinear_intro[where K=1]; transfer; auto)

lemma antilinear_to_conjugate_space[simp]: antilinear to_conjugate_space
  by (rule antilinearI; transfer, auto)

lemma antilinear_from_conjugate_space[simp]: antilinear from_conjugate_space
  by (rule antilinearI; transfer, auto)

lemma cspan_to_conjugate_space[simp]: "cspan (to_conjugate_space ` X) = to_conjugate_space ` cspan X"
  unfolding complex_vector.span_def complex_vector.subspace_def hull_def
  apply transfer
  apply simp
  by (metis (no_types, opaque_lifting) complex_cnj_cnj)

lemma surj_to_conjugate_space[simp]: "surj to_conjugate_space"
  by (meson surj_def to_conjugate_space_cases)

lemmas has_derivative_scaleC[simp, derivative_intros] =
  bounded_bilinear.FDERIV[OF bounded_cbilinear_scaleC[THEN bounded_cbilinear.bounded_bilinear]]

lemma norm_to_conjugate_space[simp]: norm (to_conjugate_space x) = norm x
  by (fact norm_conjugate_space.abs_eq)

lemma norm_from_conjugate_space[simp]: norm (from_conjugate_space x) = norm x
  by (simp add: norm_conjugate_space.rep_eq)

lemma closure_to_conjugate_space: closure (to_conjugate_space ` X) = to_conjugate_space ` closure X
proof -
  have 1: to_conjugate_space ` closure X  closure (to_conjugate_space ` X)
    apply (rule closure_bounded_linear_image_subset)
    by (simp add: bounded_antilinear.bounded_linear)
  have  = to_conjugate_space ` from_conjugate_space ` closure (to_conjugate_space ` X)
    by (simp add: from_conjugate_space_inverse image_image)
  also have   to_conjugate_space ` closure (from_conjugate_space ` to_conjugate_space ` X)
    apply (rule image_mono)
    apply (rule closure_bounded_linear_image_subset)
    by (simp add: bounded_antilinear.bounded_linear)
  also have  = to_conjugate_space ` closure X
    by (simp add: to_conjugate_space_inverse image_image)
  finally show ?thesis
    using 1 by simp
qed

lemma closure_from_conjugate_space: closure (from_conjugate_space ` X) = from_conjugate_space ` closure X
proof -
  have 1: from_conjugate_space ` closure X  closure (from_conjugate_space ` X)
    apply (rule closure_bounded_linear_image_subset)
    by (simp add: bounded_antilinear.bounded_linear)
  have  = from_conjugate_space ` to_conjugate_space ` closure (from_conjugate_space ` X)
    by (simp add: to_conjugate_space_inverse image_image)
  also have   from_conjugate_space ` closure (to_conjugate_space ` from_conjugate_space ` X)
    apply (rule image_mono)
    apply (rule closure_bounded_linear_image_subset)
    by (simp add: bounded_antilinear.bounded_linear)
  also have  = from_conjugate_space ` closure X
    by (simp add: from_conjugate_space_inverse image_image)
  finally show ?thesis
    using 1 by simp
qed

lemma bounded_antilinear_eq_on:
  fixes A B :: "'a::complex_normed_vector  'b::complex_normed_vector"
  assumes bounded_antilinear A and bounded_antilinear B and
    eq: x. x  G  A x = B x and t: t  closure (cspan G)
  shows A t = B t
proof -
  let ?A = λx. A (from_conjugate_space x) and ?B = λx. B (from_conjugate_space x)
    and ?G = to_conjugate_space ` G and ?t = to_conjugate_space t
  have bounded_clinear ?A and bounded_clinear ?B
    by (auto intro!: bounded_antilinear_o_bounded_antilinear[OF bounded_antilinear A]
        bounded_antilinear_o_bounded_antilinear[OF bounded_antilinear B])
  moreover from eq have x. x  ?G  ?A x = ?B x
    by (metis image_iff iso_tuple_UNIV_I to_conjugate_space_inverse)
  moreover from t have ?t  closure (cspan ?G)
    by (metis bounded_antilinear.bounded_linear bounded_antilinear_to_conjugate_space closure_bounded_linear_image_subset cspan_to_conjugate_space imageI subsetD)
  ultimately have ?A ?t = ?B ?t
    by (rule bounded_clinear_eq_on_closure)
  then show A t = B t
    by (simp add: to_conjugate_space_inverse)
qed

subsection ‹Product is a Complex Vector Space›

(* Follows closely Product_Vector.thy *)

instantiation prod :: (complex_vector, complex_vector) complex_vector
begin

definition scaleC_prod_def:
  "scaleC r A = (scaleC r (fst A), scaleC r (snd A))"

lemma fst_scaleC [simp]: "fst (scaleC r A) = scaleC r (fst A)"
  unfolding scaleC_prod_def by simp

lemma snd_scaleC [simp]: "snd (scaleC r A) = scaleC r (snd A)"
  unfolding scaleC_prod_def by simp

proposition scaleC_Pair [simp]: "scaleC r (a, b) = (scaleC r a, scaleC r b)"
  unfolding scaleC_prod_def by simp

instance
proof
  fix a b :: complex and x y :: "'a × 'b"
  show "scaleC a (x + y) = scaleC a x + scaleC a y"
    by (simp add: scaleC_add_right scaleC_prod_def)
  show "scaleC (a + b) x = scaleC a x + scaleC b x"
    by (simp add: Complex_Vector_Spaces.scaleC_prod_def scaleC_left.add)
  show "scaleC a (scaleC b x) = scaleC (a * b) x"
    by (simp add: prod_eq_iff)
  show "scaleC 1 x = x"
    by (simp add: prod_eq_iff)
  show (scaleR :: _  _  'a*'b) r = (*C) (complex_of_real r) for r
    by (auto intro!: ext simp: scaleR_scaleC scaleC_prod_def scaleR_prod_def)
qed

end

lemma module_prod_scale_eq_scaleC: "module_prod.scale (*C) (*C) = scaleC"
  apply (rule ext) apply (rule ext)
  apply (subst module_prod.scale_def)
  subgoal by unfold_locales
  by (simp add: scaleC_prod_def)

interpretation complex_vector?: vector_space_prod "scaleC::__'a::complex_vector" "scaleC::__'b::complex_vector"
  rewrites "scale = ((*C)::__('a × 'b))"
    and "module.dependent (*C) = cdependent"
    and "module.representation (*C) = crepresentation"
    and "module.subspace (*C) = csubspace"
    and "module.span (*C) = cspan"
    and "vector_space.extend_basis (*C) = cextend_basis"
    and "vector_space.dim (*C) = cdim"
    and "Vector_Spaces.linear (*C) (*C) = clinear"
  subgoal by unfold_locales
  subgoal by (fact module_prod_scale_eq_scaleC)
  unfolding cdependent_raw_def crepresentation_raw_def csubspace_raw_def cspan_raw_def
    cextend_basis_raw_def cdim_raw_def clinear_def
  by (rule refl)+

instance prod :: (complex_normed_vector, complex_normed_vector) complex_normed_vector 
proof
  fix c :: complex and x y :: "'a × 'b"
  show "norm (c *C x) = cmod c * norm x"
    unfolding norm_prod_def
    apply (simp add: power_mult_distrib)
    apply (simp add: distrib_left [symmetric])
    by (simp add: real_sqrt_mult)
qed


lemma cspan_Times: cspan (S × T) = cspan S × cspan T if 0  S and 0  T
proof 
  have fst ` cspan (S × T)  cspan S
    apply (subst complex_vector.linear_span_image[symmetric])
    using that complex_vector.module_hom_fst by auto
  moreover have snd ` cspan (S × T)  cspan T
    apply (subst complex_vector.linear_span_image[symmetric])
    using that complex_vector.module_hom_snd by auto
  ultimately show cspan (S × T)  cspan S × cspan T
    by auto

  show cspan S × cspan T  cspan (S × T)
  proof
    fix x assume assm: x  cspan S × cspan T
    then have fst x  cspan S
      by auto
    then obtain t1 r1 where fst_x: fst x = (at1. r1 a *C a) and [simp]: finite t1 and t1  S
      by (auto simp add: complex_vector.span_explicit)
    from assm
    have snd x  cspan T
      by auto
    then obtain t2 r2 where snd_x: snd x = (at2. r2 a *C a) and [simp]: finite t2 and t2  T
      by (auto simp add: complex_vector.span_explicit)
    define t :: ('a+'b) set and r :: ('a+'b)  complex and f :: ('a+'b)  ('a×'b)
      where t = t1 <+> t2
      and r a = (case a of Inl a1  r1 a1 | Inr a2  r2 a2)
      and f a = (case a of Inl a1  (a1,0) | Inr a2  (0,a2))
    for a
    have finite t
      by (simp add: t_def)
    moreover have f ` t  S × T
      using  t1  S t2  T that
      by (auto simp: f_def t_def)
    moreover have (fst x, snd x) = (at. r a *C f a)
      apply (simp only: fst_x snd_x)
      by (auto simp: t_def sum.Plus r_def f_def sum_prod)
    ultimately show x  cspan (S × T)
      apply auto
      by (smt (verit, best) complex_vector.span_scale complex_vector.span_sum complex_vector.span_superset image_subset_iff subset_iff)
  qed
qed

lemma onorm_case_prod_plus: onorm (case_prod plus :: _  'a::{real_normed_vector, not_singleton}) = sqrt 2
proof -
  obtain x :: 'a where x  0
    apply atomize_elim by auto
  show ?thesis
    apply (rule onormI[where x=(x,x)])
    using norm_plus_leq_norm_prod apply force
    using  x  0
    by (auto simp add: zero_prod_def norm_prod_def real_sqrt_mult
        simp flip: scaleR_2)
qed


subsection ‹Copying existing theorems into sublocales›

context bounded_clinear begin
interpretation bounded_linear f by (rule bounded_linear)
lemmas continuous = real.continuous
lemmas uniform_limit = real.uniform_limit
lemmas Cauchy = real.Cauchy
end

context bounded_antilinear begin
interpretation bounded_linear f by (rule bounded_linear)
lemmas continuous = real.continuous
lemmas uniform_limit = real.uniform_limit
end


context bounded_cbilinear begin
interpretation bounded_bilinear prod by simp
lemmas tendsto = real.tendsto
lemmas isCont = real.isCont
lemmas scaleR_right = real.scaleR_right
lemmas scaleR_left = real.scaleR_left
end

context bounded_sesquilinear begin
interpretation bounded_bilinear prod by simp
lemmas tendsto = real.tendsto
lemmas isCont = real.isCont
lemmas scaleR_right = real.scaleR_right
lemmas scaleR_left = real.scaleR_left
end

lemmas tendsto_scaleC [tendsto_intros] =
  bounded_cbilinear.tendsto [OF bounded_cbilinear_scaleC]

unbundle no_lattice_syntax

end