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"

    "Complex_Bounded_Operators.Extra_Vector_Spaces"
    "Complex_Bounded_Operators.Extra_Ordered_Fields"
    "HOL-Library.Complemented_Lattices"
    "Complex_Bounded_Operators.Extra_General"

    Complex_Vector_Spaces0
begin

bundle notation_norm begin
notation norm ("_")
end

unbundle lattice_syntax

subsection Misc

lemma (in scaleC) scaleC_real: assumes "r" shows "r *C x = Re r *R x"
  unfolding scaleR_scaleC using assms by simp

lemma of_complex_of_real_eq [simp]: "of_complex (of_real n) = of_real n"
  unfolding of_complex_def of_real_def unfolding scaleR_scaleC by simp

lemma Complexs_of_real [simp]: "of_real r  "
  unfolding Complexs_def of_real_def of_complex_def
  apply (subst scaleR_scaleC) by simp

lemma Reals_in_Complexs: "  "
  unfolding Reals_def by auto

lemma (in clinear) "linear f"
  apply standard
  by (simp_all add: add scaleC scaleR_scaleC)

lemma (in bounded_clinear) bounded_linear: "bounded_linear f"
  by (simp add: add bounded bounded_linear.intro bounded_linear_axioms.intro linearI scaleC scaleR_scaleC)

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

lemma (in clinear) linear:
  shows linear f
  by (simp add: add linearI scaleC scaleR_scaleC)

lemma bounded_clinearI:
  assumes b1 b2. f (b1 + b2) = f b1 + f b2
  assumes r b. f (r *C b) = r *C f b
  assumes x. norm (f x)  norm x * K
  shows "bounded_clinear f"
  using assms by (auto intro!: exI bounded_clinear.intro clinearI simp: bounded_clinear_axioms_def)

lemma bounded_clinear_id[simp]: bounded_clinear id
  by (simp add: id_def)

(* The following would be a natural inclusion of locales, but unfortunately it leads to
   name conflicts upon interpretation of bounded_cbilinear *)
(* sublocale bounded_cbilinear ⊆ bounded_bilinear
  by (rule bounded_bilinear) *)


definition cbilinear :: ('a::complex_vector  'b::complex_vector  'c::complex_vector)  bool
  where cbilinear = (λ f. ( y. clinear (λ x. f x y))  ( x. clinear (λ y. f x y)) )

lemma cbilinear_add_left:
  assumes cbilinear f
  shows f (a + b) c = f a c + f b c
  by (smt (verit, del_insts) assms cbilinear_def complex_vector.linear_add)

lemma cbilinear_add_right:
  assumes cbilinear f
  shows f a (b + c) = f a b + f a c
  by (smt (verit, del_insts) assms cbilinear_def complex_vector.linear_add)

lemma cbilinear_times:
  fixes g' :: 'a::complex_vector  complex and g :: 'b::complex_vector  complex
  assumes  x y. h x y = (g' x)*(g y) and clinear g and clinear g'
  shows cbilinear h
proof -
  have w1: "h (b1 + b2) y = h b1 y + h b2 y"
    for b1 :: 'a
      and b2 :: 'a
      and y
  proof-
    have h (b1 + b2) y = g' (b1 + b2) * g y
      using  x y. h x y = (g' x)*(g y)
      by auto
    also have  = (g' b1 + g' b2) * g y
      using clinear g'
      unfolding clinear_def
      by (simp add: assms(3) complex_vector.linear_add)
    also have  = g' b1 * g y + g' b2 * g y
      by (simp add: ring_class.ring_distribs(2))
    also have  = h b1 y + h b2 y
      using assms(1) by auto
    finally show ?thesis by blast
  qed
  have w2: "h (r *C b) y = r *C h b y"
    for r :: complex
      and b :: 'a
      and y
  proof-
    have h (r *C b) y = g' (r *C b) * g y
      by (simp add: assms(1))
    also have  = r *C (g' b * g y)
      by (simp add: assms(3) complex_vector.linear_scale)
    also have  = r *C (h b y)
      by (simp add: assms(1))
    finally show ?thesis by blast
  qed
  have "clinear (λx. h x y)"
    for y :: 'b
    unfolding clinear_def
    by (meson clinearI clinear_def w1 w2)
  hence t2: "y. clinear (λx. h x y)"
    by simp
  have v1: "h x (b1 + b2) = h x b1 + h x b2"
    for b1 :: 'b
      and b2 :: 'b
      and x
  proof-
    have h x (b1 + b2)  = g' x * g (b1 + b2)
      using  x y. h x y = (g' x)*(g y)
      by auto
    also have  = g' x * (g b1 + g b2)
      using clinear g'
      unfolding clinear_def
      by (simp add: assms(2) complex_vector.linear_add)
    also have  = g' x * g b1 + g' x * g b2
      by (simp add: ring_class.ring_distribs(1))
    also have  = h x b1 + h x b2
      using assms(1) by auto
    finally show ?thesis by blast
  qed

  have v2:  "h x (r *C b) = r *C h x b"
    for r :: complex
      and b :: 'b
      and x
  proof-
    have h x (r *C b) =  g' x * g (r *C b)
      by (simp add: assms(1))
    also have  = r *C (g' x * g b)
      by (simp add: assms(2) complex_vector.linear_scale)
    also have  = r *C (h x b)
      by (simp add: assms(1))
    finally show ?thesis by blast
  qed
  have "Vector_Spaces.linear (*C) (*C) (h x)"
    for x :: 'a
    using v1 v2
    by (meson clinearI clinear_def)
  hence t1: "x. clinear (h x)"
    unfolding clinear_def
    by simp
  show ?thesis
    unfolding cbilinear_def
    by (simp add: t1 t2)
qed

lemma csubspace_is_subspace: "csubspace A  subspace A"
  apply (rule subspaceI)
  by (auto simp: complex_vector.subspace_def scaleR_scaleC)

lemma span_subset_cspan: "span A  cspan A"
  unfolding span_def complex_vector.span_def
  by (simp add: csubspace_is_subspace hull_antimono)


lemma cindependent_implies_independent:
  assumes "cindependent (S::'a::complex_vector set)"
  shows "independent S"
  using assms unfolding dependent_def complex_vector.dependent_def
  using span_subset_cspan by blast

lemma cspan_singleton: "cspan {x} = {α *C x| α. True}"
proof -
  have cspan {x} = {y. 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 auto
  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

subsection Antilinear maps and friends

locale antilinear = additive f for f :: "'a::complex_vector  'b::complex_vector" +
  assumes scaleC: "f (scaleC r x) = cnj r *C f x"

sublocale antilinear  linear
proof (rule linearI)
  show "f (b1 + b2) = f b1 + f b2"
    for b1 :: 'a
      and b2 :: 'a
    by (simp add: add)
  show "f (r *R b) = r *R f b"
    for r :: real
      and b :: 'a
    unfolding scaleR_scaleC by (subst scaleC, simp)
qed

lemma antilinear_imp_scaleC:
  fixes D :: "complex  'a::complex_vector"
  assumes "antilinear D"
  obtains d where "D = (λx. cnj x *C d)"
proof -
  interpret clinear "D o cnj"
    apply standard apply auto
     apply (simp add: additive.add assms antilinear.axioms(1))
    using assms antilinear.scaleC by fastforce
  obtain d where "D o cnj = (λx. x *C d)"
    using clinear_axioms complex_vector.linear_imp_scale by blast
  then have D = (λx. cnj x *C d)
    by (metis comp_apply complex_cnj_cnj)
  then show ?thesis
    by (rule that)
qed

corollary complex_antilinearD:
  fixes f :: "complex  complex"
  assumes "antilinear f" obtains c where "f = (λx. c * cnj x)"
  by (rule antilinear_imp_scaleC [OF assms]) (force simp: scaleC_conv_of_complex)

lemma antilinearI:
  assumes "x y. f (x + y) = f x + f y"
    and "c x. f (c *C x) = cnj c *C f x"
  shows "antilinear f"
  by standard (rule assms)+

lemma antilinear_o_antilinear: "antilinear f  antilinear g  clinear (g o f)"
  apply (rule clinearI)
   apply (simp add: additive.add antilinear_def)
  by (simp add: antilinear.scaleC)

lemma clinear_o_antilinear: "antilinear f  clinear g  antilinear (g o f)"
  apply (rule antilinearI)
   apply (simp add: additive.add complex_vector.linear_add antilinear_def)
  by (simp add: complex_vector.linear_scale antilinear.scaleC)

lemma antilinear_o_clinear: "clinear f  antilinear g  antilinear (g o f)"
  apply (rule antilinearI)
   apply (simp add: additive.add complex_vector.linear_add antilinear_def)
  by (simp add: complex_vector.linear_scale antilinear.scaleC)

locale bounded_antilinear = antilinear f for f :: "'a::complex_normed_vector  'b::complex_normed_vector" +
  assumes bounded: "K. x. norm (f x)  norm x * K"

lemma bounded_antilinearI:
  assumes b1 b2. f (b1 + b2) = f b1 + f b2
  assumes r b. f (r *C b) = cnj r *C f b
  assumes x. norm (f x)  norm x * K
  shows "bounded_antilinear f"
  using assms by (auto intro!: exI bounded_antilinear.intro antilinearI simp: bounded_antilinear_axioms_def)

sublocale bounded_antilinear  bounded_linear
  apply standard by (fact bounded)

lemma (in bounded_antilinear) bounded_linear: "bounded_linear f"
  by (fact bounded_linear)

lemma (in bounded_antilinear) antilinear: "antilinear f"
  by (fact antilinear_axioms)

lemma bounded_antilinear_intro:
  assumes "x y. f (x + y) = f x + f y"
    and "r x. f (scaleC r x) = scaleC (cnj r) (f x)"
    and "x. norm (f x)  norm x * K"
  shows "bounded_antilinear f"
  by standard (blast intro: assms)+

lemma bounded_antilinear_0[simp]: bounded_antilinear (λ_. 0)
  by (rule bounded_antilinear_intro[where K=0], auto)

lemma cnj_bounded_antilinear[simp]: "bounded_antilinear cnj"
  apply (rule bounded_antilinear_intro [where K = 1])
  by auto

lemma bounded_antilinear_o_bounded_antilinear:
  assumes "bounded_antilinear f"
    and "bounded_antilinear g"
  shows "bounded_clinear (λx. f (g x))"
proof
  interpret f: bounded_antilinear f by fact
  interpret g: bounded_antilinear g by fact
  fix b1 b2 b r
  show "f (g (b1 + b2)) = f (g b1) + f (g b2)"
    by (simp add: f.add g.add)
  show "f (g (r *C b)) = r *C f (g b)"
    by (simp add: f.scaleC g.scaleC)
  have "bounded_linear (λx. f (g x))"
    using f.bounded_linear g.bounded_linear by (rule bounded_linear_compose)
  then show "K. x. norm (f (g x))  norm x * K"
    by (rule bounded_linear.bounded)
qed

lemma bounded_antilinear_o_bounded_clinear:
  assumes "bounded_antilinear f"
    and "bounded_clinear g"
  shows "bounded_antilinear (λx. f (g x))"
proof
  interpret f: bounded_antilinear f by fact
  interpret g: bounded_clinear g by fact
  show "f (g (x + y)) = f (g x) + f (g y)" for x y
    by (simp only: f.add g.add)
  show "f (g (scaleC r x)) = scaleC (cnj r) (f (g x))" for r x
    by (simp add: f.scaleC g.scaleC)
  have "bounded_linear (λx. f (g x))"
    using f.bounded_linear g.bounded_linear by (rule bounded_linear_compose)
  then show "K. x. norm (f (g x))  norm x * K"
    by (rule bounded_linear.bounded)
qed

lemma bounded_clinear_o_bounded_antilinear:
  assumes "bounded_clinear f"
    and "bounded_antilinear g"
  shows "bounded_antilinear (λx. f (g x))"
proof
  interpret f: bounded_clinear f by fact
  interpret g: bounded_antilinear g by fact
  show "f (g (x + y)) = f (g x) + f (g y)" for x y
    by (simp only: f.add g.add)
  show "f (g (scaleC r x)) = scaleC (cnj r) (f (g x))" for r x
    using f.scaleC g.scaleC by fastforce
  have "bounded_linear (λx. f (g x))"
    using f.bounded_linear g.bounded_linear by (rule bounded_linear_compose)
  then show "K. x. norm (f (g x))  norm x * K"
    by (rule bounded_linear.bounded)
qed

lemma bij_clinear_imp_inv_clinear: "clinear (inv f)"
  if a1: "clinear f" and a2: "bij f"
proof
  fix b1 b2 r b
  show "inv f (b1 + b2) = inv f b1 + inv f b2"
    by (simp add: a1 a2 bij_is_inj bij_is_surj complex_vector.linear_add inv_f_eq surj_f_inv_f)
  show "inv f (r *C b) = r *C inv f b"
    using that
    by (smt bij_inv_eq_iff clinear_def complex_vector.linear_scale)
qed


locale bounded_sesquilinear =
  fixes
    prod :: "'a::complex_normed_vector  'b::complex_normed_vector  'c::complex_normed_vector"
      (infixl "**" 70)
  assumes add_left: "prod (a + a') b = prod a b + prod a' b"
    and add_right: "prod a (b + b') = prod a b + prod a b'"
    and scaleC_left: "prod (r *C a) b = (cnj r) *C (prod a b)"
    and scaleC_right: "prod a (r *C b) = r *C (prod a b)"
    and bounded: "K. a b. norm (prod a b)  norm a * norm b * K"

sublocale bounded_sesquilinear  bounded_bilinear
  apply standard
  by (auto simp: add_left add_right scaleC_left scaleC_right bounded scaleR_scaleC)

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

lemma (in bounded_sesquilinear) bounded_antilinear_left: "bounded_antilinear (λa. prod a b)"
  apply standard
    apply (auto simp add: scaleC_left add_left)
  by (metis ab_semigroup_mult_class.mult_ac(1) bounded)

lemma (in bounded_sesquilinear) bounded_clinear_right: "bounded_clinear (λb. prod a b)"
  apply standard
    apply (auto simp add: scaleC_right add_right)
  by (metis ab_semigroup_mult_class.mult_ac(1) ordered_field_class.sign_simps(34) pos_bounded)

lemma (in bounded_sesquilinear) comp1:
  assumes bounded_clinear g
  shows bounded_sesquilinear (λx. prod (g x))
proof
  interpret bounded_clinear g by fact
  fix a a' b b' r
  show "prod (g (a + a')) b = prod (g a) b + prod (g a') b"
    by (simp add: add add_left)
  show "prod (g a) (b + b') = prod (g a) b + prod (g a) b'"
    by (simp add: add add_right)
  show "prod (g (r *C a)) b = cnj r *C prod (g a) b"
    by (simp add: scaleC scaleC_left)
  show "prod (g a) (r *C b) = r *C prod (g a) b"
    by (simp add: scaleC_right)
  interpret bounded_bilinear (λx. prod (g x))
    by (simp add: bounded_linear comp1)
  show "K. a b. norm (prod (g a) b)  norm a * norm b * K"
    using bounded by blast
qed

lemma (in bounded_sesquilinear) comp2:
  assumes bounded_clinear g
  shows bounded_sesquilinear (λx y. prod x (g y))
proof
  interpret bounded_clinear g by fact
  fix a a' b b' r
  show "prod (a + a') (g b) = prod a (g b) + prod a' (g b)"
    by (simp add: add add_left)
  show "prod a (g (b + b')) = prod a (g b) + prod a (g b')"
    by (simp add: add add_right)
  show "prod (r *C a) (g b) = cnj r *C prod a (g b)"
    by (simp add: scaleC scaleC_left)
  show "prod a (g (r *C b)) = r *C prod a (g b)"
    by (simp add: scaleC scaleC_right)
  interpret bounded_bilinear (λx y. prod x (g y))
    apply (rule bounded_bilinear.flip)
    using _ bounded_linear apply (rule bounded_bilinear.comp1)
    using bounded_bilinear by (rule bounded_bilinear.flip)
  show "K. a b. norm (prod a (g b))  norm a * norm b * K"
    using bounded by blast
qed

lemma (in bounded_sesquilinear) comp: "bounded_clinear f  bounded_clinear g  bounded_sesquilinear (λx y. prod (f x) (g y))"
  using comp1 bounded_sesquilinear.comp2 by auto

lemma bounded_clinear_const_scaleR:
  fixes c :: real
  assumes bounded_clinear f
  shows bounded_clinear (λ x. c *R f x )
proof-
  have  bounded_clinear (λ x. (complex_of_real c) *C f x )
    by (simp add: assms bounded_clinear_const_scaleC)
  thus ?thesis
    by (simp add: scaleR_scaleC)
qed

lemma bounded_linear_bounded_clinear:
  bounded_linear A  c x. A (c *C x) = c *C A x  bounded_clinear A
  apply standard
  by (simp_all add: linear_simps bounded_linear.bounded)

lemma comp_bounded_clinear:
  fixes  A :: 'b::complex_normed_vector  'c::complex_normed_vector
    and B :: 'a::complex_normed_vector  'b
  assumes bounded_clinear A and bounded_clinear B
  shows bounded_clinear (A  B)
  by (metis clinear_compose assms(1) assms(2) bounded_clinear_axioms_def bounded_clinear_compose bounded_clinear_def o_def)


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

subsection Misc 2

lemmas sums_of_complex = bounded_linear.sums [OF bounded_clinear_of_complex[THEN bounded_clinear.bounded_linear]]
lemmas summable_of_complex = bounded_linear.summable [OF bounded_clinear_of_complex[THEN bounded_clinear.bounded_linear]]
lemmas suminf_of_complex = bounded_linear.suminf [OF bounded_clinear_of_complex[THEN bounded_clinear.bounded_linear]]

lemmas sums_scaleC_left = bounded_linear.sums[OF bounded_clinear_scaleC_left[THEN bounded_clinear.bounded_linear]]
lemmas summable_scaleC_left = bounded_linear.summable[OF bounded_clinear_scaleC_left[THEN bounded_clinear.bounded_linear]]
lemmas suminf_scaleC_left = bounded_linear.suminf[OF bounded_clinear_scaleC_left[THEN bounded_clinear.bounded_linear]]

lemmas sums_scaleC_right = bounded_linear.sums[OF bounded_clinear_scaleC_right[THEN bounded_clinear.bounded_linear]]
lemmas summable_scaleC_right = bounded_linear.summable[OF bounded_clinear_scaleC_right[THEN bounded_clinear.bounded_linear]]
lemmas suminf_scaleC_right = bounded_linear.suminf[OF bounded_clinear_scaleC_right[THEN bounded_clinear.bounded_linear]]

lemma closed_scaleC:
  fixes S::'a::complex_normed_vector set and a :: complex
  assumes closed S
  shows closed ((*C) a ` S)
proof (cases a = 0)
  case True
  then show ?thesis
    apply (cases S = {})
    by (auto simp: image_constant)
next
  case False
  then have (*C) a ` S = (*C) (inverse a) -` S
    by (auto simp add: rev_image_eqI)
  moreover have closed ((*C) (inverse a) -` S)
    by (simp add: assms continuous_closed_vimage)
  ultimately show ?thesis
    by simp
qed

lemma closure_scaleC:
  fixes S::'a::complex_normed_vector set
  shows closure ((*C) a ` S) = (*C) a ` closure S
proof
  have closed (closure S)
    by simp
  show "closure ((*C) a ` S)  (*C) a ` closure S"
    by (simp add: closed_scaleC closure_minimal closure_subset image_mono)

  have "x  closure ((*C) a ` S)"
    if "x  (*C) a ` closure S"
    for x :: 'a
  proof-
    obtain t where x = ((*C) a) t and t  closure S
      using x  (*C) a ` closure S by auto
    have s. (n. s n  S)  s  t
      using t  closure S Elementary_Topology.closure_sequential
      by blast
    then obtain s where n. s n  S and s  t
      by blast
    have ( n. scaleC a (s n)  ((*C) a ` S))
      using n. s n  S by blast
    moreover have (λ n. scaleC a (s n))  x
    proof-
      have isCont (scaleC a) t
        by simp
      thus ?thesis
        using  s  t  x = ((*C) a) t
        by (simp add: isCont_tendsto_compose)
    qed
    ultimately show ?thesis using Elementary_Topology.closure_sequential
      by metis
  qed
  thus "(*C) a ` closure S  closure ((*C) a ` S)" by blast
qed

lemma onorm_scalarC:
  fixes f :: 'a::complex_normed_vector  'b::complex_normed_vector
  assumes a1: bounded_clinear f
  shows  onorm (λ x. r *C (f x)) = (cmod r) * onorm f
proof-
  have (norm (f x)) / norm x  onorm f
    for x
    using a1
    by (simp add: bounded_clinear.bounded_linear le_onorm)
  hence t2: bdd_above {(norm (f x)) / norm x | x. True}
    by fastforce
  have continuous_on UNIV ( (*) w ) 
    for w::real
    by simp
  hence isCont ( ((*) (cmod r)) ) x
    for x
    by simp
  hence t3: continuous (at_left (Sup {(norm (f x)) / norm x | x. True})) ((*) (cmod r))
    using Elementary_Topology.continuous_at_imp_continuous_within
    by blast
  have {(norm (f x)) / norm x | x. True}  {}
    by blast
  moreover have mono ((*) (cmod r))
    by (simp add: monoI ordered_comm_semiring_class.comm_mult_left_mono)
  ultimately have Sup {((*) (cmod r)) ((norm (f x)) / norm x) | x. True}
         = ((*) (cmod r)) (Sup {(norm (f x)) / norm x | x. True})
    using t2 t3
    by (simp add:  continuous_at_Sup_mono full_SetCompr_eq image_image)
  hence  Sup {(cmod r) * ((norm (f x)) / norm x) | x. True}
         = (cmod r) * (Sup {(norm (f x)) / norm x | x. True})
    by blast
  moreover have Sup {(cmod r) * ((norm (f x)) / norm x) | x. True}
                = (SUP x. cmod r * norm (f x) / norm x)
    by (simp add: full_SetCompr_eq)
  moreover have (Sup {(norm (f x)) / norm x | x. True})
                = (SUP x. norm (f x) / norm x)
    by (simp add: full_SetCompr_eq)
  ultimately have t1: "(SUP x. cmod r * norm (f x) / norm x)
      = cmod r * (SUP x. norm (f x) / norm x)"
    by simp
  have onorm (λ x. r *C (f x)) = (SUP x. norm ( (λ t. r *C (f t)) x) / norm x)
    by (simp add: onorm_def)
  hence onorm (λ x. r *C (f x)) = (SUP x. (cmod r) * (norm (f x)) / norm x)
    by simp
  also have ... = (cmod r) * (SUP x. (norm (f x)) / norm x)
    using t1.
  finally show ?thesis
    by (simp add: onorm_def)
qed

lemma onorm_scaleC_left_lemma:
  fixes f :: "'a::complex_normed_vector"
  assumes r: "bounded_clinear r"
  shows "onorm (λx. r x *C f)  onorm r * norm f"
proof (rule onorm_bound)
  fix x
  have "norm (r x *C f) = norm (r x) * norm f"
    by simp
  also have "  onorm r * norm x * norm f"
    by (simp add: bounded_clinear.bounded_linear mult.commute mult_left_mono onorm r)
  finally show "norm (r x *C f)  onorm r * norm f * norm x"
    by (simp add: ac_simps)
  show "0  onorm r * norm f"
    by (simp add: bounded_clinear.bounded_linear onorm_pos_le r)
qed

lemma onorm_scaleC_left:
  fixes f :: "'a::complex_normed_vector"
  assumes f: "bounded_clinear r"
  shows "onorm (λx. r x *C f) = onorm r * norm f"
proof (cases "f = 0")
  assume "f  0"
  show ?thesis
  proof (rule order_antisym)
    show "onorm (λx. r x *C f)  onorm r * norm f"
      using f by (rule onorm_scaleC_left_lemma)
  next
    have bl1: "bounded_clinear (λx. r x *C f)"
      by (metis bounded_clinear_scaleC_const f)
    have x1:"bounded_clinear (λx. r x * norm f)"
      by (metis bounded_clinear_mult_const f)

    have "onorm r  onorm (λx. r x * complex_of_real (norm f)) / norm f"
      if "onorm r  onorm (λx. r x * complex_of_real (norm f)) * cmod (1 / complex_of_real (norm f))"
        and "f  0"
      using that
      by (metis complex_of_real_cmod complex_of_real_nn_iff field_class.field_divide_inverse
          inverse_eq_divide nice_ordered_field_class.zero_le_divide_1_iff norm_ge_zero of_real_1
          of_real_divide of_real_eq_iff)
    hence "onorm r  onorm (λx. r x * norm f) * inverse (norm f)"
      using f  0 onorm_scaleC_left_lemma[OF x1, of "inverse (norm f)"]
      by (simp add: inverse_eq_divide)
    also have "onorm (λx. r x * norm f)  onorm (λx. r x *C f)"
    proof (rule onorm_bound)
      have "bounded_linear (λx. r x *C f)"
        using bl1 bounded_clinear.bounded_linear by auto
      thus "0  onorm (λx. r x *C f)"
        by (rule Operator_Norm.onorm_pos_le)
      show "cmod (r x * complex_of_real (norm f))  onorm (λx. r x *C f) * norm x"
        for x :: 'b
        by (smt bounded_linear (λx. r x *C f) complex_of_real_cmod complex_of_real_nn_iff
            complex_scaleC_def norm_ge_zero norm_scaleC of_real_eq_iff onorm)
    qed
    finally show "onorm r * norm f  onorm (λx. r x *C f)"
      using f  0
      by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
  qed
qed (simp add: onorm_zero)

subsection Finite dimension and canonical basis

lemma vector_finitely_spanned:
  assumes z  cspan T
  shows  S. finite S  S  T  z  cspan S
proof-
  have  S r. finite S  S  T  z = (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"
  assumes distinct_canonical_basis[simp]:
    "distinct canonical_basis"
    and is_cindependent_set[simp]:
    "cindependent (set canonical_basis)"
    and is_generator_set[simp]:
    "cspan (set canonical_basis) = UNIV"

setup Sign.add_const_constraint ("Complex_Vector_Spaces0.cindependent", SOME typ'a::complex_vector set  bool)
setup Sign.add_const_constraint (const_namecdependent, SOME typ'a::complex_vector set  bool)
setup Sign.add_const_constraint (const_namecspan, SOME typ'a::complex_vector set  'a set)

lemma cdim_UNIV_basis_enum[simp]: cdim (UNIV::'a::basis_enum set) = length (canonical_basis::'a list)
  apply (subst is_generator_set[symmetric])
  apply (subst complex_vector.dim_span_eq_card_independent)
   apply (rule is_cindependent_set)
  using distinct_canonical_basis distinct_card by blast

lemma finite_basis: "basis::'a::cfinite_dim set. finite basis  cindependent basis  cspan basis = UNIV"
proof -
  from cfinitely_spanned
  obtain S :: 'a set where finite S and cspan S = UNIV
    by auto
  from complex_vector.maximal_independent_subset
  obtain B :: 'a set where B  S and cindependent B and S  cspan B
    by metis
  moreover have finite B
    using B  S finite S
    by (meson finite_subset)
  moreover have cspan B = UNIV
    using cspan S = UNIV S  cspan B
    by (metis complex_vector.span_eq top_greatest)
  ultimately show ?thesis
    by auto
qed

instance basis_enum  cfinite_dim
  apply intro_classes
  apply (rule exI[of _ set canonical_basis])
  using is_cindependent_set is_generator_set by auto

lemma cindependent_cfinite_dim_finite:
  assumes cindependent (S::'a::cfinite_dim set)
  shows finite S
  by (metis assms cfinitely_spanned complex_vector.independent_span_bound top_greatest)

lemma cfinite_dim_finite_subspace_basis:
  assumes csubspace X
  shows "basis::'a::cfinite_dim set. finite basis  cindependent basis  cspan basis = X"
  by (meson assms cindependent_cfinite_dim_finite complex_vector.basis_exists complex_vector.span_subspace)


text The following auxiliary lemma (finite_span_complete_aux›) shows more or less the same as finite_span_representation_bounded›,
   finite_span_complete› below (see there for an intuition about the mathematical
   content of the lemmas). However, there is one difference: Here we additionally assume here
   that there is a bijection rep/abs between a finite type typ'basis and the set $B$.
   This is needed to be able to use results about euclidean spaces that are formulated w.r.t.
   the type class 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. norm (crepresentation B ψ b)  norm ψ * D"
proof -
  define B' where "B' = (B  scaleC 𝗂 ` B)"
  have independent_B': "independent B'"
    using B'_def cindependent B
    by (simp add: real_independent_from_complex_independent a1)
  have "finite B'"
    unfolding B'_def using finite B by simp
  obtain D' where "D' > 0" and D': "norm (real_vector.representation B' ψ b)  norm ψ * D'"
    for ψ b
    apply atomize_elim
    using independent_B' finite B'
    by (simp add: finite_span_representation_bounded)

  define D where "D = 2*D'"
  from D' > 0 have D > 0
    unfolding D_def by simp
  have "norm (crepresentation B ψ b)  norm ψ * D" for ψ b
  proof (cases "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