Theory Complex_Vector_Spaces

section ‹‹Complex_Vector_Spaces› -- Complex Vector Spaces›

(*
Authors:

  Dominique Unruh, University of Tartu, unruh@ut.ee
  Jose Manuel Rodriguez Caballero, University of Tartu, jose.manuel.rodriguez.caballero@ut.ee
*)

theory Complex_Vector_Spaces
  imports
    "HOL-Analysis.Elementary_Topology"
    "HOL-Analysis.Operator_Norm"
    "HOL-Analysis.Elementary_Normed_Spaces"
    "HOL-Library.Set_Algebras"
    "HOL-Analysis.Starlike"
    "HOL-Types_To_Sets.Types_To_Sets"
    "HOL-Library.Complemented_Lattices"
    "HOL-Library.Function_Algebras"

    Extra_Vector_Spaces
    Extra_Ordered_Fields
    Extra_Operator_Norm
    Extra_General

    Complex_Vector_Spaces0
begin

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

unbundle lattice_syntax

subsection ‹Misc›


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

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

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

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

lemma Reals_in_Complexs: "ℝ ⊆ ℂ"
  unfolding Reals_def by auto

lemma (in bounded_clinear) bounded_linear: "bounded_linear f"
  by standard

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

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

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

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

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

definition cbilinear :: ‹('a::complex_vector ⇒ 'b::complex_vector ⇒ 'c::complex_vector) ⇒ bool›
  where ‹cbilinear = (λ f. (∀ y. clinear (λ x. f x y)) ∧ (∀ x. clinear (λ y. f x y)) )›

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

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

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

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

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

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


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

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


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 ab_semigroup_mult_class.mult_ac(1) ordered_field_class.sign_simps(34) real.pos_bounded)

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

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

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

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

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

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


lemma bounded_sesquilinear_add:
  ‹bounded_sesquilinear (λ x y. A x y + B x y)› if ‹bounded_sesquilinear A› and ‹bounded_sesquilinear B›
proof
  fix a a' :: 'a and b b' :: 'b and r :: complex
  show "A (a + a') b + B (a + a') b = (A a b + B a b) + (A a' b + B a' b)"
    by (simp add: bounded_sesquilinear.add_left that(1) that(2))
  show ‹A a (b + b') + B a (b + b') = (A a b + B a b) + (A a b' + B a b')›
    by (simp add: bounded_sesquilinear.add_right that(1) that(2))
  show ‹A (r *⇩C a) b + B (r *⇩C a) b = cnj r *⇩C (A a b + B a b)›
    by (simp add: bounded_sesquilinear.scaleC_left scaleC_add_right that(1) that(2))
  show ‹A a (r *⇩C b) + B a (r *⇩C b) = r *⇩C (A a b + B a b)›
    by (simp add: bounded_sesquilinear.scaleC_right scaleC_add_right that(1) that(2))
  show ‹∃K. ∀a b. norm (A a b + B a b) ≤ norm a * norm b * K›
  proof-
    have ‹∃ KA. ∀ a b. norm (A a b) ≤ norm a * norm b * KA›
      by (simp add: bounded_sesquilinear.bounded that(1))
    then obtain KA where ‹∀ a b. norm (A a b) ≤ norm a * norm b * KA›
      by blast
    have ‹∃ KB. ∀ a b. norm (B a b) ≤ norm a * norm b * KB›
      by (simp add: bounded_sesquilinear.bounded that(2))
    then obtain KB where ‹∀ a b. norm (B a b) ≤ norm a * norm b * KB›
      by blast
    have ‹norm (A a b + B a b) ≤ norm a * norm b * (KA + KB)›
      for a b
    proof-
      have ‹norm (A a b + B a b) ≤ norm (A a b) +  norm (B a b)›
        using norm_triangle_ineq by blast
      also have ‹… ≤ norm a * norm b * KA + norm a * norm b * KB›
        using  ‹∀ a b. norm (A a b) ≤ norm a * norm b * KA›
          ‹∀ a b. norm (B a b) ≤ norm a * norm b * KB›
        using add_mono by blast
      also have ‹…=  norm a * norm b * (KA + KB)›
        by (simp add: mult.commute ring_class.ring_distribs(2))
      finally show ?thesis
        by blast
    qed
    thus ?thesis by blast
  qed
qed

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

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

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

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

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

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

subsection ‹Misc 2›

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

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

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

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



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

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

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

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

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

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

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

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

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

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

subsection ‹Finite dimension and canonical basis›

lemma vector_finitely_spanned:
  assumes ‹z ∈ cspan T›
  shows ‹∃ S. finite S ∧ S ⊆ T ∧ z ∈ cspan S›
proof-
  have ‹∃ S r. finite S ∧ S ⊆ T ∧ z = (∑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