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 norm_syntax 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. y∈cspan {x}}›
    by auto
  also have ‹… = {α *⇩C x| α. True}›
    apply (subst complex_vector.span_breakdown_eq)
    by auto
  finally show ?thesis
    by -
qed


lemma cspan_as_span:
  "cspan (B::'a::complex_vector set) = span (B ∪ scaleC 𝗂 ` B)"
proof (intro set_eqI iffI)
  let ?cspan = complex_vector.span
  let ?rspan = real_vector.span
  fix ψ
  assume cspan: "ψ ∈ ?cspan B"
  have "∃B' r. finite B' ∧ B' ⊆ B ∧ ψ = (∑b∈B'. r b *⇩C b)"
    using complex_vector.span_explicit[of B] cspan
    by auto
  then obtain B' r where "finite B'" and "B' ⊆ B" and ψ_explicit: "ψ = (∑b∈B'. r b *⇩C b)"
    by atomize_elim
  define R where "R = B ∪ scaleC 𝗂 ` B"

  have x2: "(case x of (b, i) ⇒ if i
            then Im (r b) *⇩R 𝗂 *⇩C b
            else Re (r b) *⇩R b) ∈ span (B ∪ (*⇩C) 𝗂 ` B)"
    if "x ∈ B' × (UNIV::bool set)"
    for x :: "'a × bool"
    using that ‹B' ⊆ B› by (auto simp add: real_vector.span_base real_vector.span_scale subset_iff)
  have x1: "ψ = (∑x∈B'. ∑i∈UNIV. if i then Im (r x) *⇩R 𝗂 *⇩C x else Re (r x) *⇩R x)"
    if "⋀b. r b *⇩C b = Re (r b) *⇩R b + Im (r b) *⇩R 𝗂 *⇩C b"
    using that by (simp add: UNIV_bool ψ_explicit)
  moreover have "r b *⇩C b = Re (r b) *⇩R b + Im (r b) *⇩R 𝗂 *⇩C b" for b
    using complex_eq scaleC_add_left scaleC_scaleC scaleR_scaleC
    by (metis (no_types, lifting) complex_of_real_i i_complex_of_real)
  ultimately have "ψ = (∑(b,i)∈(B'×UNIV). if i then Im (r b) *⇩R (𝗂 *⇩C b) else Re (r b) *⇩R b)"
    by (simp add: sum.cartesian_product)
  also have "… ∈ ?rspan R"
    unfolding R_def
    using x2
    by (rule real_vector.span_sum)
  finally show "ψ ∈ ?rspan R" by -
next
  let ?cspan = complex_vector.span
  let ?rspan = real_vector.span
  define R where "R = B ∪ scaleC 𝗂 ` B"
  fix ψ
  assume rspan: "ψ ∈ ?rspan R"
  have "subspace {a. a ∈ cspan B}"
    by (rule real_vector.subspaceI, auto simp add: complex_vector.span_zero
        complex_vector.span_add_eq2 complex_vector.span_scale scaleR_scaleC)
  moreover have "x ∈ cspan B"
    if "x ∈ R"
    for x :: 'a
    using that R_def complex_vector.span_base complex_vector.span_scale by fastforce
  ultimately show "ψ ∈ ?cspan B"
    using real_vector.span_induct rspan by blast
qed


lemma isomorphic_equal_cdim:
  assumes lin_f: ‹clinear f›
  assumes inj_f: ‹inj_on f (cspan S)›
  assumes im_S: ‹f ` S = T›
  shows ‹cdim S = cdim T›
proof -
  obtain SB where SB_span: "cspan SB = cspan S" and indep_SB: ‹cindependent SB›
    by (metis complex_vector.basis_exists complex_vector.span_mono complex_vector.span_span subset_antisym)
  with lin_f inj_f have indep_fSB: ‹cindependent (f ` SB)›
    apply (rule_tac complex_vector.linear_independent_injective_image)
    by auto
  from lin_f have ‹cspan (f ` SB) = f ` cspan SB›
    by (meson complex_vector.linear_span_image)
  also from SB_span lin_f have ‹… = cspan T›
    by (metis complex_vector.linear_span_image im_S)
  finally have ‹cdim T = card (f ` SB)›
    using indep_fSB complex_vector.dim_eq_card by blast
  also have ‹… = card SB›
    apply (rule card_image) using inj_f
    by (metis SB_span complex_vector.linear_inj_on_span_iff_independent_image indep_fSB lin_f)
  also have ‹… = cdim S›
    using indep_SB SB_span
    by (metis complex_vector.dim_eq_card)
  finally show ?thesis by simp
qed


lemma cindependent_inter_scaleC_cindependent:
  assumes a1: "cindependent (B::'a::complex_vector set)" and a3: "c ≠ 1"
  shows "B ∩ (*⇩C) c ` B = {}"
proof (rule classical, cases ‹c = 0›)
  case True
  then show ?thesis
    using a1 by (auto simp add: complex_vector.dependent_zero)
next
  case False
  assume "¬(B ∩ (*⇩C) c ` B = {})"
  hence "B ∩ (*⇩C) c ` B ≠ {}"
    by blast
  then obtain x where u1: "x ∈ B ∩ (*⇩C) c ` B"
    by blast
  then obtain b where u2: "x = b" and u3: "b∈B"
    by blast
  then  obtain b' where u2': "x = c *⇩C b'" and u3': "b'∈B"
    using u1
    by blast
  have g1: "b = c *⇩C b'"
    using u2 and u2' by simp
  hence "b ∈ complex_vector.span {b'}"
    using False
    by (simp add: complex_vector.span_base complex_vector.span_scale)
  hence "b = b'"
    by (metis  u3' a1 complex_vector.dependent_def complex_vector.span_base
        complex_vector.span_scale insertE insert_Diff u2 u2' u3)
  hence "b' = c *⇩C b'"
    using g1 by blast
  thus ?thesis
    by (metis a1 a3 complex_vector.dependent_zero complex_vector.scale_right_imp_eq
        mult_cancel_right2 scaleC_scaleC u3')
qed

lemma real_independent_from_complex_independent:
  assumes "cindependent (B::'a::complex_vector set)"
  defines "B' == ((*⇩C) 𝗂 ` B)"
  shows "independent (B ∪ B')"
proof (rule notI)
  assume ‹dependent (B ∪ B')›
  then obtain T f0 x where [simp]: ‹finite T› and ‹T ⊆ B ∪ B'› and f0_sum: ‹(∑v∈T. f0 v *⇩R v) = 0›
    and x: ‹x ∈ T› and f0_x: ‹f0 x ≠ 0›
    by (auto simp: real_vector.dependent_explicit)
  define f T1 T2 T' f' x' where ‹f v = (if v ∈ T then f0 v else 0)›
    and ‹T1 = T ∩ B› and ‹T2 = scaleC (-𝗂) ` (T ∩ B')›
    and ‹T' = T1 ∪ T2› and ‹f' v = f v + 𝗂 * f (𝗂 *⇩C v)›
    and ‹x' = (if x ∈ T1 then x else -𝗂 *⇩C x)› for v
  have ‹B ∩ B' = {}›
    by (simp add: assms cindependent_inter_scaleC_cindependent)
  have ‹T' ⊆ B›
    by (auto simp: T'_def T1_def T2_def B'_def)
  have [simp]: ‹finite T'› ‹finite T1› ‹finite T2›
    by (auto simp add: T'_def T1_def T2_def)
  have f_sum: ‹(∑v∈T. f v *⇩R v) = 0›
    unfolding f_def using f0_sum by auto
  have f_x: ‹f x ≠ 0›
    using f0_x x by (auto simp: f_def)
  have f'_sum: ‹(∑v∈T'. f' v *⇩C v) = 0›
  proof -
    have ‹(∑v∈T'. f' v *⇩C v) = (∑v∈T'. complex_of_real (f v) *⇩C v) + (∑v∈T'. (𝗂 * complex_of_real (f (𝗂 *⇩C v))) *⇩C v)›
      by (auto simp: f'_def sum.distrib scaleC_add_left)
    also have ‹(∑v∈T'. complex_of_real (f v) *⇩C v) = (∑v∈T1. f v *⇩R v)› (is ‹_ = ?left›)
      apply (auto simp: T'_def scaleR_scaleC intro!: sum.mono_neutral_cong_right)
      using T'_def T1_def ‹T' ⊆ B› f_def by auto
    also have ‹(∑v∈T'. (𝗂 * complex_of_real (f (𝗂 *⇩C v))) *⇩C v) = (∑v∈T2. (𝗂 * complex_of_real (f (𝗂 *⇩C v))) *⇩C v)› (is ‹_ = ?right›)
      apply (auto simp: T'_def intro!: sum.mono_neutral_cong_right)
      by (smt (z3) B'_def IntE IntI T1_def T2_def ‹f ≡ λv. if v ∈ T then f0 v else 0› add.inverse_inverse complex_vector.vector_space_axioms i_squared imageI mult_minus_left vector_space.vector_space_assms(3) vector_space.vector_space_assms(4))
    also have ‹?right = (∑v∈T∩B'. f v *⇩R v)› (is ‹_ = ?right›)
      apply (rule sum.reindex_cong[symmetric, where l=‹scaleC 𝗂›])
        apply (auto simp: T2_def image_image scaleR_scaleC)
      using inj_on_def by fastforce
    also have ‹?left + ?right = (∑v∈T. f v *⇩R v)›
      apply (subst sum.union_disjoint[symmetric])
      using ‹B ∩ B' = {}› ‹T ⊆ B ∪ B'› apply (auto simp: T1_def)
      by (metis Int_Un_distrib Un_Int_eq(4) sup.absorb_iff1)
    also have ‹… = 0›
      by (rule f_sum)
    finally show ?thesis
      by -
  qed

  have x': ‹x' ∈ T'›
    using ‹T ⊆ B ∪ B'› x by (auto simp: x'_def T'_def T1_def T2_def)

  have f'_x': ‹f' x' ≠ 0›
    using Complex_eq Complex_eq_0 f'_def f_x x'_def by auto

  from ‹finite T'› ‹T' ⊆ B› f'_sum x' f'_x'
  have ‹cdependent B›
    using complex_vector.independent_explicit_module by blast
  with assms show False
    by auto
qed

lemma crepresentation_from_representation:
  assumes a1: "cindependent B" and a2: "b ∈ B" and a3: "finite B"
  shows "crepresentation B ψ b = (representation (B ∪ (*⇩C) 𝗂 ` B) ψ b)
                           + 𝗂 *⇩C (representation (B ∪ (*⇩C) 𝗂 ` B) ψ (𝗂 *⇩C b))"
proof (cases "ψ ∈ cspan B")
  define B' where "B' = B ∪ (*⇩C) 𝗂 ` B"
  case True
  define r  where "r v = real_vector.representation B' ψ v" for v
  define r' where "r' v = real_vector.representation B' ψ (𝗂 *⇩C v)" for v
  define f  where "f v = r v + 𝗂 *⇩C r' v" for v
  define g  where "g v = crepresentation B ψ v" for v
  have "(∑v | g v ≠ 0. g v *⇩C v) = ψ"
    unfolding g_def
    using Collect_cong Collect_mono_iff DiffD1 DiffD2 True a1
      complex_vector.finite_representation
      complex_vector.sum_nonzero_representation_eq sum.mono_neutral_cong_left
    by fastforce
  moreover have "finite {v. g v ≠ 0}"
    unfolding g_def
    by (simp add: complex_vector.finite_representation)
  moreover have "v ∈ B"
    if "g v ≠ 0" for v
    using that unfolding g_def
    by (simp add: complex_vector.representation_ne_zero)
  ultimately have rep1: "(∑v∈B. g v *⇩C v) = ψ"
    unfolding g_def
    using a3 True a1 complex_vector.sum_representation_eq by blast
  have l0': "inj ((*⇩C) 𝗂::'a ⇒'a)"
    unfolding inj_def
    by simp
  have l0: "inj ((*⇩C) (- 𝗂)::'a ⇒'a)"
    unfolding inj_def
    by simp
  have l1: "(*⇩C) (- 𝗂) ` B ∩ B = {}"
    using cindependent_inter_scaleC_cindependent[where B=B and c = "- 𝗂"]
    by (metis Int_commute a1 add.inverse_inverse complex_i_not_one i_squared mult_cancel_left1
        neg_equal_0_iff_equal)
  have l2: "B ∩ (*⇩C) 𝗂 ` B = {}"
    by (simp add: a1 cindependent_inter_scaleC_cindependent)
  have rr1: "r (𝗂 *⇩C v) = r' v" for v
    unfolding r_def r'_def
    by simp
  have k1: "independent B'"
    unfolding B'_def using a1 real_independent_from_complex_independent by simp
  have "ψ ∈ span B'"
    using B'_def True cspan_as_span by blast
  have "v ∈ B'"
    if "r v ≠ 0"
    for v
    unfolding r_def
    using r_def real_vector.representation_ne_zero that by auto
  have "finite B'"
    unfolding B'_def using a3
    by simp
  have "(∑v∈B'. r v *⇩R v) = ψ"
    unfolding r_def
    using True  Real_Vector_Spaces.real_vector.sum_representation_eq[where B = B' and basis = B'
        and v = ψ]
    by (smt Real_Vector_Spaces.dependent_raw_def ‹ψ ∈ Real_Vector_Spaces.span B'› ‹finite B'›
        equalityD2 k1)
  have d1: "(∑v∈B. r (𝗂 *⇩C v) *⇩R (𝗂 *⇩C v)) = (∑v∈(*⇩C) 𝗂 ` B. r v *⇩R v)"
    using l0'
    by (metis (mono_tags, lifting) inj_eq inj_on_def sum.reindex_cong)
  have "(∑v∈B. (r v + 𝗂 * (r' v)) *⇩C v) = (∑v∈B. r v *⇩C v + (𝗂 * r' v) *⇩C v)"
    by (meson scaleC_left.add)
  also have "… = (∑v∈B. r v *⇩C v) + (∑v∈B. (𝗂 * r' v) *⇩C v)"
    using sum.distrib by fastforce
  also have "… = (∑v∈B. r v *⇩C v) + (∑v∈B. 𝗂 *⇩C (r' v *⇩C v))"
    by auto
  also have "… = (∑v∈B. r v *⇩R v) + (∑v∈B. 𝗂 *⇩C (r (𝗂 *⇩C v) *⇩R v))"
    unfolding r'_def r_def
    by (metis (mono_tags, lifting) scaleR_scaleC sum.cong)
  also have "… = (∑v∈B. r v *⇩R v) + (∑v∈B. r (𝗂 *⇩C v) *⇩R (𝗂 *⇩C v))"
    by (metis (no_types, lifting) complex_vector.scale_left_commute scaleR_scaleC)
  also have "… = (∑v∈B. r v *⇩R v) + (∑v∈(*⇩C) 𝗂 ` B. r v *⇩R v)"
    using d1
    by simp
  also have "… = ψ"
    using l2 ‹(∑v∈B'. r v *⇩R v) = ψ›
    unfolding B'_def
    by (simp add: a3 sum.union_disjoint)
  finally have "(∑v∈B. f v *⇩C v) = ψ" unfolding r'_def r_def f_def by simp
  hence "0 = (∑v∈B. f v *⇩C v) - (∑v∈B. crepresentation B ψ v *⇩C v)"
    using rep1
    unfolding g_def
    by simp
  also have "… = (∑v∈B. f v *⇩C v - crepresentation B ψ v *⇩C v)"
    by (simp add: sum_subtractf)
  also have "… = (∑v∈B. (f v - crepresentation B ψ v) *⇩C v)"
    by (metis scaleC_left.diff)
  finally have "0 = (∑v∈B. (f v - crepresentation B ψ v) *⇩C v)".
  hence "(∑v∈B. (f v - crepresentation B ψ v) *⇩C v) = 0"
    by simp
  hence "f b - crepresentation B ψ b = 0"
    using a1 a2 a3 complex_vector.independentD[where s = B and t = B
        and u = "λv. f v - crepresentation B ψ v" and v = b]
      order_refl  by smt
  hence "crepresentation B ψ b = f b"
    by simp
  thus ?thesis unfolding f_def r_def r'_def B'_def by auto
next
  define B' where "B' = B ∪ (*⇩C) 𝗂 ` B"
  case False
  have b2: "ψ ∉ real_vector.span B'"
    unfolding B'_def
    using False cspan_as_span by auto
  have "ψ ∉ complex_vector.span B"
    using False by blast
  have "crepresentation B ψ b = 0"
    unfolding complex_vector.representation_def
    by (simp add: False)
  moreover have "real_vector.representation B' ψ b = 0"
    unfolding real_vector.representation_def
    by (simp add: b2)
  moreover have "real_vector.representation B' ψ ((*⇩C) 𝗂 b) = 0"
    unfolding real_vector.representation_def
    by (simp add: b2)
  ultimately show ?thesis unfolding B'_def by simp
qed


lemma CARD_1_vec_0[simp]: ‹(ψ :: _ ::{complex_vector,CARD_1}) = 0›
  by auto


lemma scaleC_cindependent:
  assumes a1: "cindependent (B::'a::complex_vector set)" and a3: "c ≠ 0"
  shows "cindependent ((*⇩C) c ` B)"
proof-
  have "u y = 0"
    if g1: "y∈S" and g2: "(∑x∈S. u x *⇩C x) = 0" and g3: "finite S" and g4: "S⊆(*⇩C) c ` B"
    for u y S
  proof-
    define v where "v x = u (c *⇩C x)" for x
    obtain S' where "S'⊆B" and S_S': "S = (*⇩C) c ` S'"
      by (meson g4 subset_imageE)
    have "inj ((*⇩C) c::'a⇒_)"
      unfolding inj_def
      using a3 by auto
    hence "finite S'"
      using S_S' finite_imageD g3 subset_inj_on by blast
    have "t ∈ (*⇩C) (inverse c) ` S"
      if "t ∈ S'" for t
    proof-
      have "c *⇩C t ∈ S"
        using ‹S = (*⇩C) c ` S'› that by blast
      hence "(inverse c) *⇩C (c *⇩C t) ∈ (*⇩C) (inverse c) ` S"
        by blast
      moreover have "(inverse c) *⇩C (c *⇩C t) = t"
        by (simp add: a3)
      ultimately show ?thesis by simp
    qed
    moreover have "t ∈ S'"
      if "t ∈ (*⇩C) (inverse c) ` S" for t
    proof-
      obtain t' where "t = (inverse c) *⇩C t'" and "t' ∈ S"
        using ‹t ∈ (*⇩C) (inverse c) ` S› by auto
      have "c *⇩C t = c *⇩C ((inverse c) *⇩C t')"
        using ‹t = (inverse c) *⇩C t'› by simp
      also have "… = (c * (inverse c)) *⇩C t'"
        by simp
      also have "… = t'"
        by (simp add: a3)
      finally have "c *⇩C t = t'".
      thus ?thesis using ‹t' ∈ S›
        using ‹S = (*⇩C) c ` S'› a3 complex_vector.scale_left_imp_eq by blast
    qed
    ultimately have "S' = (*⇩C) (inverse c) ` S"
      by blast
    hence "inverse c *⇩C y ∈ S'"
      using that(1) by blast
    have t: "inj (((*⇩C) c)::'a ⇒ _)"
      using a3 complex_vector.injective_scale[where c = c]
      by blast
    have "0 = (∑x∈(*⇩C) c ` S'. u x *⇩C x)"
      using ‹S = (*⇩C) c ` S'› that(2) by auto
    also have "… = (∑x∈S'. v x *⇩C (c *⇩C x))"
      unfolding v_def
      using t Groups_Big.comm_monoid_add_class.sum.reindex[where h = "((*⇩C) c)" and A = S'
          and g = "λx. u x *⇩C x"] subset_inj_on by auto
    also have "… = c *⇩C (∑x∈S'. v x *⇩C x)"
      by (metis (mono_tags, lifting) complex_vector.scale_left_commute scaleC_right.sum sum.cong)
    finally have "0 = c *⇩C (∑x∈S'. v x *⇩C x)".
    hence "(∑x∈S'. v x *⇩C x) = 0"
      using a3 by auto
    hence "v (inverse c *⇩C y) = 0"
      using ‹inverse c *⇩C y ∈ S'› ‹finite S'› ‹S' ⊆ B› a1
        complex_vector.independentD
      by blast
    thus "u y = 0"
      unfolding v_def
      by (simp add: a3)
  qed
  thus ?thesis
    using complex_vector.dependent_explicit
    by (simp add: complex_vector.dependent_explicit )
qed

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

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

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

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

lemma bounded_clinear_inv:
  assumes [simp]: ‹bounded_clinear f›
  assumes b: ‹b > 0›
  assumes bound: ‹⋀x. norm (f x) ≥ b * norm x›
  assumes ‹surj f›
  shows ‹bounded_clinear (inv f)›
proof (rule bounded_clinear_intro)
  fix x y :: 'b and r :: complex
  define x' y' where ‹x' = inv f x› and ‹y' = inv f y›
  have [simp]: ‹clinear f›
    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 ‹∀x∈M. ∀y∈ M. ∀u. ∀v. u *⇩C x + v *⇩C y ∈  M›
    using a1
    by (simp add:  complex_vector.subspace_def)
  hence ‹∀x∈M. ∀y∈M. ∀u::real. ∀v::real. u *⇩R x + v *⇩R y ∈ M›
    by (simp add: scaleR_scaleC)
  hence ‹∀x∈M. ∀y∈M. ∀u≥0. ∀v≥0. u + v = 1 ⟶ u *⇩R x + v *⇩R y ∈M›
    by blast
  thus ?thesis using convex_def by blast
qed

lemma kernel_is_csubspace[simp]:
  assumes a1: "clinear f"
  shows "csubspace  (f -` {0})"
  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)

lemma clinear_of_complex[iff]: ‹clinear of_complex›
  by (simp add: clinearI)

lemma infsum_of_bool_scaleC: ‹(∑⇩∞x∈X. of_bool (x=y) *⇩C f x) = of_bool (y∈X) *⇩C f y› for f :: ‹_ ⇒ _::complex_vector›
  apply (cases ‹y∈X›)
   apply (subst infsum_cong_neutral[where T=‹{y}› and g=f])
      apply auto[4]
  apply (subst infsum_cong_neutral[where T=‹{}› and g=f])
  by auto

lemma has_sum_bounded_clinear:
  assumes "bounded_clinear h" and "(f has_sum S) A"
  shows "((λx. h (f x)) has_sum h S) A"
  apply (rule has_sum_bounded_linear[where h=h])
  by (auto intro!: bounded_clinear.bounded_linear assms)

lemma scaleC_scaleR_commute: ‹a *⇩C b *⇩R x = b *⇩R a *⇩C x› for x :: ‹_::complex_normed_vector›
  by (simp add: scaleR_scaleC scaleC_left_commute)

lemma csubspace_has_basis:
  assumes ‹csubspace S›
  shows ‹∃B. cindependent B ∧ cspan B = S›
proof -
  obtain B where ‹cindependent B› and ‹cspan B = S›
    by (rule complex_vector.maximal_independent_subset[where V=S])
       (use assms complex_vector.span_subspace in blast)
  then show ?thesis
    by auto
qed

lemma inj_scaleC:
  fixes A :: ‹'a::complex_vector set›
  assumes ‹c ≠ 0›
  shows ‹inj_on (scaleC c) A›
  by (meson assms inj_onI scaleC_left_imp_eq)

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 \<^locale>‹linear› 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 \<^locale>‹linear› 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 bounded mult.assoc mult.left_commute)

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

lemma antilinear_diff:
  assumes ‹antilinear f› and ‹antilinear g›
  shows ‹antilinear (λx. f x - g x)›
  apply (rule antilinearI)
   apply (metis add_diff_add additive.add antilinear_def assms(1,2))
  by (simp add: antilinear.scaleC assms(1,2) scaleC_right.diff)

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

lemma has_sum_scaleC_right:
  fixes f :: ‹'a ⇒ 'b :: complex_normed_vector›
  assumes ‹(f has_sum s) A›
  shows ‹((λx. c *⇩C f x) has_sum c *⇩C s) A›
  apply (rule has_sum_bounded_clinear[where h=‹(*⇩C) c›])
  using bounded_clinear_scaleC_right assms by auto


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)

lemma compact_scaleC:
  fixes s :: "'a::complex_normed_vector set"
  assumes "compact s"
  shows "compact (scaleC c ` s)"
  by (auto intro!: compact_continuous_image assms continuous_at_imp_continuous_on)

subsection ‹Finite dimension and canonical basis›

lemma vector_finitely_spanned:
  assumes ‹z ∈ cspan T›
  shows ‹∃ S. finite S ∧ S ⊆ T ∧ z ∈ cspan S›
proof-
  have ‹∃ S r. finite S ∧ S ⊆ T ∧ z = (∑a∈S. r a *⇩C a)›
    using complex_vector.span_explicit[where b = "T"]
      assms by auto
  then obtain S r where ‹finite S› and ‹S ⊆ T› and ‹z = (∑a∈S. r a *⇩C a)›
    by blast
  thus ?thesis
    by (meson complex_vector.span_scale complex_vector.span_sum complex_vector.span_superset subset_iff)
qed

setup ‹Sign.add_const_constraint ("Complex_Vector_Spaces0.cindependent", SOME \<^typ>‹'a set ⇒ bool›)›
setup ‹Sign.add_const_constraint (\<^const_name>‹cdependent›, SOME \<^typ>‹'a set ⇒ bool›)›
setup ‹Sign.add_const_constraint (\<^const_name>‹cspan›, SOME \<^typ>‹'a set ⇒ 'a set›)›

class cfinite_dim = complex_vector +
  assumes cfinitely_spanned: "∃S::'a set. finite S ∧ cspan S = UNIV"

class basis_enum = complex_vector +
  fixes canonical_basis :: ‹'a list›
    and canonical_basis_length :: ‹'a itself ⇒ nat›
  assumes distinct_canonical_basis[simp]:
    "distinct canonical_basis"
    and is_cindependent_set[simp]:
    "cindependent (set canonical_basis)"
    and is_generator_set[simp]:
    "cspan (set canonical_basis) = UNIV"
    and canonical_basis_length:
    ‹canonical_basis_length TYPE('a) = length canonical_basis›

setup ‹Sign.add_const_constraint ("Complex_Vector_Spaces0.cindependent", SOME \<^typ>‹'a::complex_vector set ⇒ bool›)›
setup ‹Sign.add_const_constraint (\<^const_name>‹cdependent›, SOME \<^typ>‹'a::complex_vector set ⇒ bool›)›
setup ‹Sign.add_const_constraint (\<^const_name>‹cspan›, SOME \<^typ>‹'a::complex_vector set ⇒ 'a set›)›


instantiation complex :: basis_enum begin
definition "canonical_basis = [1::complex]"
definition ‹canonical_basis_length (_::complex itself) = 1›
instance
proof
  show "distinct (canonical_basis::complex list)"
    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 \<^class>‹finite›

   Since we anyway assume that $B$ is finite, this added assumption does not make the lemma
   weaker. However, we cannot derive the existence of \<^typ>‹'basis› inside the proof
   (HOL does not support such reasoning). Therefore we have the type \<^typ>‹'basis› as
   an explicit assumption and remove it using @{attribute internalize_sort} after the proof.›

lemma finite_span_complete_aux:
  fixes b :: "'b::real_normed_vector" and B :: "'b set"
    and  rep :: "'basis::finite ⇒ 'b" and abs :: "'b ⇒ 'basis"
  assumes t: "type_definition rep abs B"
    and t1: "finite B" and t2: "b∈B" and t3: "independent B"
  shows "∃D>0. ∀ψ. norm (representation B ψ b) ≤ norm ψ * D"
    and "complete (span B)"
proof -
  define repr  where "repr = real_vector.representation B"
  define repr' where "repr' ψ = Abs_euclidean_space (repr ψ o rep)" for ψ
  define comb  where "comb l = (∑b∈B. l b *⇩R b)" for l
  define comb' where "comb' l = comb (Rep_euclidean_space l o abs)" for l

  have comb_cong: "comb x = comb y" if "⋀z. z∈B ⟹ x z = y z" for x y
    unfolding comb_def using that by auto
  have comb_repr[simp]: "comb (repr ψ) = ψ" if "ψ ∈ real_vector.span B" for ψ
    using ‹comb ≡ λl. ∑b∈B. l b *⇩R b› local.repr_def real_vector.sum_representation_eq t1 t3 that
    by fastforce

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

proof (cases "B≠{}")
  case True

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

  hence d2:"∃D. ∀ψ. D>0 ∧ norm (repr ψ b) ≤ norm ψ * D" if ‹b∈B› for b
    by (simp add: repr_def that True)
  have d1: " (⋀b. b ∈ B ⟹
          ∃D. ∀ψ. 0 < D ∧ norm (repr ψ b) ≤ norm ψ * D) ⟹
    ∃D. ∀b ψ. b ∈ B ⟶
               0 < D b ∧ norm (repr ψ b) ≤ norm ψ * D b"
    apply (rule choice) by auto
  then obtain D where D: "D b > 0 ∧ norm (repr ψ b) ≤ norm ψ * D b" if "b∈B" for b ψ
    apply atomize_elim
    using d2 by blast

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

hide_fact finite_span_complete_aux


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

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


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

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


lemma finite_cspan_crepresentation_bounded:
  fixes B :: "'a::complex_normed_vector set"
  assumes a1: "finite B" and a2: "cindependent B"
  shows "∃D>0. ∀ψ b. 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 "b∈B")
    case True
    have d3: "norm 𝗂 = 1"
      by simp

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

lemma bounded_clinear_finite_dim[simp]:
  fixes f :: ‹'a::{cfinite_dim,complex_normed_vector} ⇒ 'b::complex_normed_vector›
  assumes ‹clinear f›
  shows ‹bounded_clinear f›
proof -
  include norm_syntax
  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 * (∑a∈basis. ∥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: "(∑a∈basis. crepresentation basis x a *⇩C a) = x"
      by (simp add: b2 b3 complex_vector.sum_representation_eq x_span)
    have f3: "(∑a∈basis. r a *⇩C a) = x"
      unfolding r_def
      by (simp add: g1)
    hence "f x = f (∑a∈basis. r a *⇩C a)"
      by simp
    also have "… = (∑a∈basis. 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 = (∑a∈basis. r a *⇩C f a)".
    hence "∥f x∥ = ∥(∑a∈basis. r a *⇩C f a)∥"
      by simp
    also have "… ≤ (∑a∈basis. ∥r a *⇩C f a∥)"
      by (simp add: sum_norm_le)
    also have "… ≤ (∑a∈basis. ∥r a∥ * ∥f a∥)"
      by simp
    also have "… ≤ (∑a∈basis. ∥x∥ * C * ∥f a∥)"
      using sum_mono s1 unfolding r_def
      by (simp add: sum_mono mult_right_mono)
    also have "… ≤ ∥x∥ * C * (∑a∈basis. ∥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 ‹y∈T› ‹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 ‹x∈T› ‹y∈T› 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 ‹(∑⇩∞x∈A. of_real (f x) :: 'b::{real_normed_vector, real_algebra_1}) = of_real (∑⇩∞x∈A. 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)


definition ‹cfinite_dim S ⟷ (∃B. finite B ∧ S ⊆ cspan B)›

lemma cspan_finite_dim[intro]: ‹cfinite_dim (cspan B)› if ‹finite B›
  using cfinite_dim_def that by auto

lemma cfinite_dim_subspace_has_basis:
  assumes ‹cfinite_dim S› and ‹csubspace S›
  shows ‹∃B. finite B ∧ cindependent B ∧ cspan B = S›
proof -
  obtain B where ‹cindependent B› and ‹cspan B = S›
    by (rule complex_vector.maximal_independent_subset[where V=S])
       (use ‹csubspace S› complex_vector.span_subspace in blast)
  from ‹cfinite_dim S›
  obtain C where ‹finite C› and ‹S ⊆ cspan C›
    using cfinite_dim_def by auto
  from ‹cspan B = S› and ‹S ⊆ cspan C›
  have ‹B ⊆ cspan C›
    using complex_vector.span_superset by force
  from ‹finite C› ‹cindependent B› this
  have ‹finite B›
    by (rule complex_vector.independent_span_bound[THEN conjunct1])
  from this and ‹cindependent B› and ‹cspan B = S›
  show ?thesis
    by auto
qed


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  "x∈C ⟹ y∈C ⟹ x+y∈C" 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 ‹x∈C› 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 (A∩B)"
proof-
  obtain C where ‹C = A ∩ B› by blast
  have ‹csubspace C›
  proof-
    have "x∈C ⟹ y∈C ⟹ x+y∈C" for x y
      by (metis IntD1 IntD2 IntI ‹C = A ∩ B› assms(1) assms(2) complex_vector.subspace_def closed_csubspace_def)
    moreover have "x∈C ⟹ 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. x∈X ⟹ 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

lift_definition finite_dim_ccsubspace :: ‹'a::complex_normed_vector ccsubspace ⇒ bool› is cfinite_dim.

lemma ccspan_finite_dim[intro]: ‹finite_dim_ccsubspace (ccspan B)› if ‹finite B›
  using ccspan_finite finite_dim_ccsubspace.rep_eq that by fastforce

lemma finite_dim_ccsubspace_zero[iff]: ‹finite_dim_ccsubspace 0›
proof -
  have *: ‹cfinite_dim (cspan {0})›
    by blast
  show ?thesis
    apply transfer
    using * by simp
qed

lemma finite_dim_ccsubspace_bot[iff]: ‹finite_dim_ccsubspace ⊥›
  using finite_dim_ccsubspace_zero by auto


lemma ccsubspace_contains_unit:
  assumes ‹E ≠ ⊥›
  shows ‹∃h∈space_as_set E. norm h = 1›
proof -
  from assms have ‹space_as_set E ≠ {0}›
    by (metis bot_ccsubspace.rep_eq space_as_set_inject)
  then obtain h⇩0 where ‹h⇩0 ∈ space_as_set E› and ‹h⇩0 ≠ 0›
    by auto
  then have ‹sgn h⇩0 ∈ space_as_set E›
    using csubspace_space_as_set
    by (auto intro!: complex_vector.subspace_scale
        simp add: sgn_div_norm scaleR_scaleC)
  moreover from ‹h⇩0 ≠ 0› have ‹norm (sgn h⇩0) = 1›
    by (simp add: norm_sgn)
  ultimately show ?thesis
    by auto
qed


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 \<^term>‹A+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 x∈X. ccspan (S x)) = ccspan (⋃x∈X. S x)›
proof (rule SUP_eqI)
  show ‹ccspan (S x) ≤ ccspan (⋃x∈X. S x)› if ‹x ∈ X› for x
    apply (rule ccspan_mono)
    using that by auto
  show ‹ccspan (⋃x∈X. 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]: ‹(∑x∈X. ⊥) = (⊥ :: _ 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

lemma to_conjugate_space_0[simp]: ‹to_conjugate_space 0 = 0›
  by (simp add: zero_conjugate_space.abs_eq)

lemma from_conjugate_space_0[simp]: ‹from_conjugate_space 0 = 0›
  using zero_conjugate_space.rep_eq by blast

lemma antilinear_eq_0_on_span:
  assumes ‹antilinear f›
    and ‹⋀x. x ∈ b ⟹ f x = 0›
    and ‹x ∈ cspan b›
  shows ‹f x = 0›
proof -
  from assms(1)
  have ‹clinear (λx. to_conjugate_space (f x))›
    apply (rule antilinear_o_antilinear[unfolded o_def])
    by simp
  then have ‹to_conjugate_space (f x) = 0›
    apply (rule complex_vector.linear_eq_0_on_span)
    using assms by auto
  then have ‹from_conjugate_space (to_conjugate_space (f x)) = 0›
    by simp
  then show ?thesis
    by (simp add: to_conjugate_space_inverse)
qed

subsection ‹Separating sets›

lemma separating_set_bounded_clinear_dense:
  assumes ‹ccspan S = ⊤›
  shows ‹separating_set bounded_clinear S›
  unfolding separating_set_def
  apply (intro allI impI ext, rule bounded_clinear_eq_on_closure[where G=S])
  by (use assms ccspan.rep_eq top_ccsubspace.rep_eq in force)+

lemma separating_set_bounded_cbilinear_nested:
  assumes ‹separating_set (bounded_clinear :: (_ => 'e::complex_normed_vector) ⇒ _) ((λ(x, y). h x y) ` (UNIV × UNIV))›
  assumes ‹bounded_cbilinear h›
  assumes ‹separating_set (bounded_clinear :: (_ => 'e) ⇒ _) A›
  assumes ‹separating_set (bounded_clinear :: (_ => 'e) ⇒ _) B›
  shows ‹separating_set (bounded_clinear :: (_ => 'e) ⇒ _) ((λ(x,y). h x y) ` (A × B))›
proof (rule separating_setI)
  fix f g :: ‹'a ⇒ 'e›
  assume [simp]: ‹bounded_clinear f› ‹bounded_clinear g›
  have [simp]: ‹bounded_clinear (λx. f (h x y))› for y
    apply (rule bounded_clinear_compose[OF ‹bounded_clinear f›])
    using assms(2) by (rule bounded_cbilinear.bounded_clinear_left)
  have [simp]: ‹bounded_clinear (λx. g (h x y))› for y
    apply (rule bounded_clinear_compose[OF ‹bounded_clinear g›])
    using assms(2) by (rule bounded_cbilinear.bounded_clinear_left)
  have [simp]: ‹bounded_clinear (λy. f (h x y))› for x
    apply (rule bounded_clinear_compose[OF ‹bounded_clinear f›])
    using assms(2) by (rule bounded_cbilinear.bounded_clinear_right)
  have [simp]: ‹bounded_clinear (λy. g (h x y))› for x
    apply (rule bounded_clinear_compose[OF ‹bounded_clinear g›])
    using assms(2) by (rule bounded_cbilinear.bounded_clinear_right)

  assume ‹z ∈ (λ(x, y). h x y) ` (A × B) ⟹ f z = g z› for z
  then have ‹f (h x y) = g (h x y)› if ‹x ∈ A› and ‹y ∈ B› for x y
    using that by auto
  then have ‹(λx. f (h x y)) = (λx. g (h x y))› if ‹y ∈ B› for y
    by (intro eq_from_separatingI[OF assms(3)]) (use that in auto)
  then have ‹(λy. f (h x y)) = (λy. g (h x y))› for x
    apply (intro eq_from_separatingI[OF assms(4)])
    subgoal by simp
    subgoal by simp
    subgoal by meson
    done
  then have ‹f (h x y) = g (h x y)› for x y
    by meson
  with ‹bounded_clinear f› ‹bounded_clinear g›
  show ‹f = g›
    by (rule eq_from_separatingI2[where f=f and g=g and P=bounded_clinear and S=UNIV and T=UNIV, rotated 1])
       (fact assms(1))
qed


lemma separating_set_bounded_clinear_antilinear:
  assumes ‹separating_set (bounded_clinear :: (_ => 'e::complex_normed_vector conjugate_space) ⇒ _) A›
  shows ‹separating_set (bounded_antilinear :: (_ => 'e) ⇒ _) A›
proof (rule separating_setI)
  fix f g :: ‹'a ⇒ 'e›
  assume ‹bounded_antilinear f›
  then have lin_f: ‹bounded_clinear (to_conjugate_space o f)›
    by (simp add: bounded_antilinear_o_bounded_antilinear')
  assume ‹bounded_antilinear g›
  then have lin_g: ‹bounded_clinear (to_conjugate_space o g)›
    by (simp add: bounded_antilinear_o_bounded_antilinear')
  assume ‹f x = g x› if ‹x ∈ A› for x
  then have ‹(to_conjugate_space o f) x = (to_conjugate_space o g) x› if ‹x ∈ A› for x
    by (simp add: that)
  with lin_f lin_g
  have ‹to_conjugate_space o f = to_conjugate_space o g›
    by (rule eq_from_separatingI[OF assms])
  then show ‹f = g›
    by (metis UNIV_I fun.inj_map_strong to_conjugate_space_inverse)
qed

lemma separating_set_bounded_sesquilinear_nested:
  assumes ‹separating_set (bounded_clinear :: (_ => 'e::complex_normed_vector) ⇒ _) ((λ(x, y). h x y) ` (UNIV × UNIV))›
  assumes ‹bounded_sesquilinear h›
  assumes sep_A: ‹separating_set (bounded_clinear :: (_ => 'e conjugate_space) ⇒ _) A›
  assumes sep_B: ‹separating_set (bounded_clinear :: (_ => 'e) ⇒ _) B›
  shows ‹separating_set (bounded_clinear :: (_ => 'e) ⇒ _) ((λ(x,y). h x y) ` (A × B))›
proof (rule separating_setI)
  fix f g :: ‹'a ⇒ 'e›
  assume [simp]: ‹bounded_clinear f› ‹bounded_clinear g›
  have [simp]: ‹bounded_antilinear (λx. f (h x y))› for y
    apply (rule bounded_clinear_o_bounded_antilinear[OF ‹bounded_clinear f›])
    using assms(2) by (rule bounded_sesquilinear.bounded_antilinear_left)
  have [simp]: ‹bounded_antilinear (λx. g (h x y))› for y
    apply (rule bounded_clinear_o_bounded_antilinear[OF ‹bounded_clinear g›])
    using assms(2) by (rule bounded_sesquilinear.bounded_antilinear_left)
  have [simp]: ‹bounded_clinear (λy. f (h x y))› for x
    apply (rule bounded_clinear_compose[OF ‹bounded_clinear f›])
    using assms(2) by (rule bounded_sesquilinear.bounded_clinear_right)
  have [simp]: ‹bounded_clinear (λy. g (h x y))› for x
    apply (rule bounded_clinear_compose[OF ‹bounded_clinear g›])
    using assms(2) by (rule bounded_sesquilinear.bounded_clinear_right)

  from sep_A have sep_A': ‹separating_set (bounded_antilinear :: (_ => 'e) ⇒ _) A›
    by (rule separating_set_bounded_clinear_antilinear)
  assume ‹z ∈ (λ(x, y). h x y) ` (A × B) ⟹ f z = g z› for z
  then have ‹f (h x y) = g (h x y)› if ‹x ∈ A› and ‹y ∈ B› for x y
    using that by auto
  then have ‹(λx. f (h x y)) = (λx. g (h x y))› if ‹y ∈ B› for y
    by (intro eq_from_separatingI[OF sep_A']) (use that in auto)
  then have ‹(λy. f (h x y)) = (λy. g (h x y))› for x
    apply (intro eq_from_separatingI[OF sep_B])
    subgoal by simp
    subgoal by simp
    subgoal by meson
    done
  then have ‹f (h x y) = g (h x y)› for x y
    by meson
  with ‹bounded_clinear f› ‹bounded_clinear g›
  show ‹f = g›
    by (rule eq_from_separatingI2[where f=f and g=g and P=bounded_clinear and S=UNIV and T=UNIV, rotated 1])
       (fact assms(1))
qed


lemma separating_set_clinear_cspan:
  assumes ‹cspan S = UNIV›
  shows ‹separating_set clinear S›
  using assms
  by (auto intro: complex_vector.linear_eq_on simp: separating_set_def)


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 = (∑a∈t1. 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 = (∑a∈t2. 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) = (∑a∈t. 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