Theory Complex_Bounded_Linear_Function

section Complex_Bounded_Linear_Function› -- Complex bounded linear functions (bounded operators)›

(*
Authors:

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

*)

theory Complex_Bounded_Linear_Function
  imports
    "HOL-Types_To_Sets.Types_To_Sets"
    Banach_Steinhaus.Banach_Steinhaus
    Complex_Inner_Product
    One_Dimensional_Spaces
    Complex_Bounded_Linear_Function0
    "HOL-Library.Function_Algebras"
begin

unbundle lattice_syntax

subsection ‹Misc basic facts and declarations›

notation cblinfun_apply (infixr "*V" 70)

lemma id_cblinfun_apply[simp]: "id_cblinfun *V ψ = ψ"
  by simp

lemma apply_id_cblinfun[simp]: (*V) id_cblinfun = id
  by auto

lemma isCont_cblinfun_apply[simp]: "isCont ((*V) A) ψ"
  by transfer (simp add: clinear_continuous_at)

declare cblinfun.scaleC_left[simp]

lemma cblinfun_apply_clinear[simp]: clinear (cblinfun_apply A)
  using bounded_clinear.axioms(1) cblinfun_apply by blast

lemma cblinfun_cinner_eqI:
  fixes A B :: 'a::chilbert_space CL 'a
  assumes ψ. norm ψ = 1  cinner ψ (A *V ψ) = cinner ψ (B *V ψ)
  shows A = B
proof -
  define C where C = A - B
  have C0[simp]: cinner ψ (C ψ) = 0 for ψ
    apply (cases ψ = 0)
    using assms[of sgn ψ]
    by (simp_all add: C_def norm_sgn sgn_div_norm cblinfun.scaleR_right assms cblinfun.diff_left cinner_diff_right)
  { fix f g α
    have 0 = cinner (f + α *C g) (C *V (f + α *C g))
      by (simp add: cinner_diff_right minus_cblinfun.rep_eq)
    also have  = α *C cinner f (C g) + cnj α *C cinner g (C f)
      by (smt (z3) C0 add.commute add.right_neutral cblinfun.add_right cblinfun.scaleC_right cblinfun_cinner_right.rep_eq cinner_add_left cinner_scaleC_left complex_scaleC_def)
    finally have α *C cinner f (C g) = - cnj α *C cinner g (C f)
      by (simp add: eq_neg_iff_add_eq_0)
  }
  then have cinner f (C g) = 0 for f g
    by (metis complex_cnj_i complex_cnj_one complex_vector.scale_cancel_right complex_vector.scale_left_imp_eq equation_minus_iff i_squared mult_eq_0_iff one_neq_neg_one)
  then have C g = 0 for g
    using cinner_eq_zero_iff by blast
  then have C = 0
    by (simp add: cblinfun_eqI)
  then show A = B
    using C_def by auto
qed

lemma id_cblinfun_not_0[simp]: (id_cblinfun :: 'a::{complex_normed_vector, not_singleton} CL _)  0
  by (metis (full_types) Extra_General.UNIV_not_singleton cblinfun.zero_left cblinfun_id_cblinfun_apply ex_norm1 norm_zero one_neq_zero)

lemma cblinfun_norm_geqI:
  assumes norm (f *V x) / norm x  K
  shows norm f  K
  using assms by transfer (smt (z3) bounded_clinear.bounded_linear le_onorm)

(* This lemma is proven in Complex_Bounded_Linear_Function0 but we add the [simp]
   only here because we try to keep Complex_Bounded_Linear_Function0 as close to
   Bounded_Linear_Function as possible. *)
declare scaleC_conv_of_complex[simp]

lemma cblinfun_eq_0_on_span:
  fixes S::'a::complex_normed_vector set
  assumes "x  cspan S"
    and "s. sS  F *V s = 0"
  shows F *V x = 0
  using bounded_clinear.axioms(1) cblinfun_apply assms complex_vector.linear_eq_0_on_span
  by blast

lemma cblinfun_eq_on_span:
  fixes S::'a::complex_normed_vector set
  assumes "x  cspan S"
    and "s. sS  F *V s = G *V s"
  shows F *V x = G *V x
  using bounded_clinear.axioms(1) cblinfun_apply assms complex_vector.linear_eq_on_span
  by blast

lemma cblinfun_eq_0_on_UNIV_span:
  fixes basis::'a::complex_normed_vector set
  assumes "cspan basis = UNIV"
    and "s. sbasis  F *V s = 0"
  shows F = 0
  by (metis cblinfun_eq_0_on_span UNIV_I assms cblinfun.zero_left cblinfun_eqI)

lemma cblinfun_eq_on_UNIV_span:
  fixes basis::"'a::complex_normed_vector set" and φ::"'a  'b::complex_normed_vector"
  assumes "cspan basis = UNIV"
    and "s. sbasis  F *V s = G *V s"
  shows F = G
  by (metis (no_types) assms cblinfun_eqI cblinfun_eq_on_span iso_tuple_UNIV_I)

lemma cblinfun_eq_on_canonical_basis:
  fixes f g::"'a::{basis_enum,complex_normed_vector} CL 'b::complex_normed_vector"
  defines "basis == set (canonical_basis::'a list)"
  assumes "u. u  basis  f *V u = g *V u"
  shows  "f = g"
  using assms cblinfun_eq_on_UNIV_span is_generator_set by blast

lemma cblinfun_eq_0_on_canonical_basis:
  fixes f ::"'a::{basis_enum,complex_normed_vector} CL 'b::complex_normed_vector"
  defines "basis == set (canonical_basis::'a list)"
  assumes "u. u  basis  f *V u = 0"
  shows  "f = 0"
  by (simp add: assms cblinfun_eq_on_canonical_basis)

lemma cinner_canonical_basis_eq_0:
  defines "basisA == set (canonical_basis::'a::onb_enum list)"
    and   "basisB == set (canonical_basis::'b::onb_enum list)"
  assumes "u v. ubasisA  vbasisB  is_orthogonal v (F *V u)"
  shows "F = 0"
proof-
  have "F *V u = 0"
    if "ubasisA" for u
  proof-
    have "v. vbasisB  is_orthogonal v (F *V u)"
      by (simp add: assms(3) that)
    moreover have "(v. vbasisB  is_orthogonal v x)  x = 0"
      for x
    proof-
      assume r1: "v. vbasisB  is_orthogonal v x"
      have "is_orthogonal v x" for v
      proof-
        have "cspan basisB = UNIV"
          using basisB_def is_generator_set  by auto
        hence "v  cspan basisB"
          by (smt iso_tuple_UNIV_I)
        hence "t s. v = (at. s a *C a)  finite t  t  basisB"
          using complex_vector.span_explicit
          by (smt mem_Collect_eq)
        then obtain t s where b1: "v = (at. s a *C a)" and b2: "finite t" and b3: "t  basisB"
          by blast
        have "v C x = (at. s a *C a) C x"
          by (simp add: b1)
        also have " = (at. (s a *C a) C x)"
          using cinner_sum_left by blast
        also have " = (at. cnj (s a) * (a C x))"
          by auto
        also have " = 0"
          using b3 r1 subsetD by force
        finally show ?thesis by simp
      qed
      thus ?thesis
        by (simp add: v. (v C x) = 0 cinner_extensionality)
    qed
    ultimately show ?thesis by simp
  qed
  thus ?thesis
    using basisA_def cblinfun_eq_0_on_canonical_basis by auto
qed

lemma cinner_canonical_basis_eq:
  defines "basisA == set (canonical_basis::'a::onb_enum list)"
    and   "basisB == set (canonical_basis::'b::onb_enum list)"
  assumes "u v. ubasisA  vbasisB  v C (F *V u) = v C (G *V u)"
  shows "F = G"
proof-
  define H where "H = F - G"
  have "u v. ubasisA  vbasisB  is_orthogonal v (H *V u)"
    unfolding H_def
    by (simp add: assms(3) cinner_diff_right minus_cblinfun.rep_eq)
  hence "H = 0"
    by (simp add: basisA_def basisB_def cinner_canonical_basis_eq_0)
  thus ?thesis unfolding H_def by simp
qed

lemma cinner_canonical_basis_eq':
  defines "basisA == set (canonical_basis::'a::onb_enum list)"
    and   "basisB == set (canonical_basis::'b::onb_enum list)"
  assumes "u v. ubasisA  vbasisB  (F *V u) C v = (G *V u) C v"
  shows "F = G"
  using cinner_canonical_basis_eq assms
  by (metis cinner_commute')

lemma not_not_singleton_cblinfun_zero: 
  x = 0 if ¬ class.not_singleton TYPE('a) for x :: 'a::complex_normed_vector CL 'b::complex_normed_vector
  apply (rule cblinfun_eqI)
  apply (subst not_not_singleton_zero[OF that])
  by simp

lemma cblinfun_norm_approx_witness:
  fixes A :: 'a::{not_singleton,complex_normed_vector} CL 'b::complex_normed_vector
  assumes ε > 0
  shows ψ. norm (A *V ψ)  norm A - ε  norm ψ = 1
proof (transfer fixing: ε)
  fix A :: 'a  'b assume [simp]: bounded_clinear A
  have y{norm (A x) |x. norm x = 1}. y >  {norm (A x) |x. norm x = 1} - ε
    apply (rule Sup_real_close)
    using assms by (auto simp: ex_norm1 bounded_clinear.bounded_linear bdd_above_norm_f)
  also have  {norm (A x) |x. norm x = 1} = onorm A
    by (simp add: bounded_clinear.bounded_linear onorm_sphere)
  finally
  show ψ. onorm A - ε  norm (A ψ)  norm ψ = 1
    by force
qed

lemma cblinfun_norm_approx_witness_mult:
  fixes A :: 'a::{not_singleton,complex_normed_vector} CL 'b::complex_normed_vector
  assumes ε < 1
  shows ψ.  norm (A *V ψ)  norm A * ε  norm ψ = 1
proof (cases norm A = 0)
  case True
  then show ?thesis
    by auto (simp add: ex_norm1)
next
  case False
  then have (1 - ε) * norm A > 0
    using assms by fastforce
  then obtain ψ where geq: norm (A *V ψ)  norm A - ((1 - ε) * norm A) and norm ψ = 1
    using cblinfun_norm_approx_witness by blast
  have norm A * ε = norm A - (1 - ε) * norm A
    by (simp add: mult.commute right_diff_distrib')
  also have   norm (A *V ψ)
    by (rule geq)
  finally show ?thesis
    using norm ψ = 1 by auto
qed


lemma cblinfun_norm_approx_witness':
  fixes A :: 'a::complex_normed_vector CL 'b::complex_normed_vector
  assumes ε > 0
  shows ψ. norm (A *V ψ) / norm ψ  norm A - ε
proof (cases class.not_singleton TYPE('a))
  case True
  obtain ψ where norm (A *V ψ)  norm A - ε and norm ψ = 1
    apply atomize_elim
    using complex_normed_vector_axioms True assms
    by (rule cblinfun_norm_approx_witness[internalize_sort' 'a])
  then have norm (A *V ψ) / norm ψ  norm A - ε
    by simp
  then show ?thesis 
    by auto
next
  case False
  show ?thesis
    apply (subst not_not_singleton_cblinfun_zero[OF False])
     apply simp
    apply (subst not_not_singleton_cblinfun_zero[OF False])
    using ε > 0 by simp
qed

lemma cblinfun_to_CARD_1_0[simp]: (A :: _ CL _::CARD_1) = 0
  by (simp add: cblinfun_eqI)

lemma cblinfun_from_CARD_1_0[simp]: (A :: _::CARD_1 CL _) = 0
  using cblinfun_eq_on_UNIV_span by force


lemma cblinfun_cspan_UNIV:
  fixes basis :: ('a::{complex_normed_vector,cfinite_dim} CL 'b::complex_normed_vector) set
    and basisA :: 'a set and basisB :: 'b set
  assumes cspan basisA = UNIV and cspan basisB = UNIV
  assumes basis: a b. abasisA  bbasisB  Fbasis. a'basisA. F *V a' = (if a'=a then b else 0)
  shows cspan basis = UNIV
proof -
  obtain basisA' where basisA'  basisA and cindependent basisA' and cspan basisA' = UNIV
    by (metis assms(1) complex_vector.maximal_independent_subset complex_vector.span_eq top_greatest)
  then have [simp]: finite basisA'
    by (simp add: cindependent_cfinite_dim_finite)
  have basis': a b. abasisA'  bbasisB  Fbasis. a'basisA'. F *V a' = (if a'=a then b else 0)
    using basis basisA'  basisA by fastforce

  obtain F where F: F a b  basis  F a b *V a' = (if a'=a then b else 0)
    if abasisA' bbasisB a'basisA' for a b a'
    apply atomize_elim apply (intro choice allI)
    using basis' by metis
  then have F_apply: F a b *V a' = (if a'=a then b else 0)
    if abasisA' bbasisB a'basisA' for a b a'
    using that by auto
  have F_basis: F a b  basis
    if abasisA' bbasisB for a b
    using that F by auto
  have b_span: Gcspan {F a b|b. bbasisB}. a'basisA'. G *V a' = (if a'=a then b else 0) if abasisA' for a b
  proof -
    from cspan basisB = UNIV
    obtain r t where finite t and t  basisB and b_lincom: b = (at. r a *C a)
      unfolding complex_vector.span_alt by atomize_elim blast
    define G where G = (it. r i *C F a i)
    have G  cspan {F a b|b. bbasisB}
      using finite t t  basisB unfolding G_def
      by (smt (verit) complex_vector.span_scale complex_vector.span_sum complex_vector.span_superset mem_Collect_eq subsetD)
    moreover have G *V a' = (if a'=a then b else 0) if a'basisA' for a'
      using t  basisB abasisA' a'basisA'
      by (auto simp: b_lincom G_def cblinfun.sum_left F_apply intro!: sum.neutral sum.cong)
    ultimately show ?thesis
      by blast
  qed

  have a_span: cspan (abasisA'. cspan {F a b|b. bbasisB}) = UNIV
  proof (intro equalityI subset_UNIV subsetI, rename_tac H)
    fix H
    obtain G where G: G a b  cspan {F a b|b. bbasisB}  G a b *V a' = (if a'=a then b else 0) 
      if abasisA' and a'basisA' for a b a'
      apply atomize_elim apply (intro choice allI)
      using b_span by blast
    then have G_cspan: G a b  cspan {F a b|b. bbasisB} if abasisA' for a b
      using that by auto
    from G have G: G a b *V a' = (if a'=a then b else 0) if abasisA' and a'basisA' for a b a'
      using that by auto
    define H' where H' = (abasisA'. G a (H *V a))
    have H'  cspan (abasisA'. cspan {F a b|b. bbasisB})
      unfolding H'_def using G_cspan
      by (smt (verit, del_insts) UN_iff complex_vector.span_clauses(1) complex_vector.span_sum)
    moreover have H' = H
      using cspan basisA' = UNIV 
      by (auto simp: H'_def cblinfun_eq_on_UNIV_span cblinfun.sum_left G)
    ultimately show H  cspan (abasisA'. cspan {F a b |b. b  basisB})
      by simp
  qed

  moreover have cspan basis  cspan (abasisA'. cspan {F a b|b. bbasisB})
    by (smt (verit) F_basis UN_subset_iff complex_vector.span_base complex_vector.span_minimal complex_vector.subspace_span mem_Collect_eq subsetI)

  ultimately show cspan basis = UNIV
    by auto
qed


instance cblinfun :: ({cfinite_dim,complex_normed_vector}, {cfinite_dim,complex_normed_vector}) cfinite_dim
proof intro_classes
  obtain basisA :: 'a set where [simp]: cspan basisA = UNIV cindependent basisA finite basisA
    using finite_basis by blast
  obtain basisB :: 'b set where [simp]: cspan basisB = UNIV cindependent basisB finite basisB
    using finite_basis by blast
  define f where f a b = cconstruct basisA (λx. if x=a then b else 0) for a :: 'a and b :: 'b
  have f_a: f a b a = b if a : basisA for a b
    by (simp add: complex_vector.construct_basis f_def that)
  have f_not_a: f a b c = 0 if a : basisA and c : basisA and a  cfor a b c
    using that by (simp add: complex_vector.construct_basis f_def)
  define F where F a b = CBlinfun (f a b) for a b
  have clinear (f a b) for a b
    by (auto intro: complex_vector.linear_construct simp: f_def)
  then have bounded_clinear (f a b) for a b
    by auto
  then have F_apply: cblinfun_apply (F a b) = f a b for a b
    by (simp add: F_def bounded_clinear_CBlinfun_apply)
  define basis where basis = {F a b| a b. abasisA  bbasisB}
  have "a b. a  basisA; b  basisB  Fbasis. a'basisA. F *V a' = (if a' = a then b else 0)"
    by (smt (verit, del_insts) F_apply basis_def f_a f_not_a mem_Collect_eq)
  then have cspan basis = UNIV
    by (metis cspan basisA = UNIV cspan basisB = UNIV cblinfun_cspan_UNIV)

  moreover have finite basis
    unfolding basis_def by (auto intro: finite_image_set2) 
  ultimately show S :: ('a CL 'b) set. finite S  cspan S = UNIV
    by auto
qed

lemma norm_cblinfun_bound_dense:
  assumes 0  b
  assumes S: closure S = UNIV
  assumes bound: x. xS  norm (cblinfun_apply f x)  b * norm x
  shows norm f  b
proof -
  have 1: continuous_on UNIV (λa. norm (f *V a))
    by (simp add: continuous_on_eq_continuous_within)
  have 2: continuous_on UNIV (λa. b * norm a)
    using continuous_on_mult_left continuous_on_norm_id by blast
  have norm (cblinfun_apply f x)  b * norm x for x
    by (metis (mono_tags, lifting) UNIV_I S bound 1 2 on_closure_leI)
  then show norm f  b
    using 0  b norm_cblinfun_bound by blast
qed

lemma infsum_cblinfun_apply:
  assumes g summable_on S
  shows infsum (λx. A *V g x) S = A *V (infsum g S)
  using infsum_bounded_linear[unfolded o_def] assms cblinfun.real.bounded_linear_right by blast

lemma has_sum_cblinfun_apply:
  assumes (g has_sum x) S
  shows ((λx. A *V g x) has_sum (A *V x)) S
  using assms has_sum_bounded_linear[unfolded o_def] using cblinfun.real.bounded_linear_right by blast

lemma abs_summable_on_cblinfun_apply:
  assumes g abs_summable_on S
  shows (λx. A *V g x) abs_summable_on S
  using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_right] assms
  by (rule abs_summable_on_bounded_linear[unfolded o_def])

lemma summable_on_cblinfun_apply:
  assumes g summable_on S
  shows (λx. A *V g x) summable_on S
  using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_right] assms
  by (rule summable_on_bounded_linear[unfolded o_def])

lemma summable_on_cblinfun_apply_left:
  assumes A summable_on S
  shows (λx. A x *V g) summable_on S
  using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_left] assms
  by (rule summable_on_bounded_linear[unfolded o_def])

lemma abs_summable_on_cblinfun_apply_left:
  assumes A abs_summable_on S
  shows (λx. A x *V g) abs_summable_on S
  using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_left] assms
  by (rule abs_summable_on_bounded_linear[unfolded o_def])
lemma infsum_cblinfun_apply_left:
  assumes A summable_on S
  shows infsum (λx. A x *V g) S = (infsum A S) *V g
  apply (rule infsum_bounded_linear[unfolded o_def, of λA. cblinfun_apply A g])
  using assms 
  by (auto simp add: bounded_clinear.bounded_linear bounded_cbilinear_cblinfun_apply)
lemma has_sum_cblinfun_apply_left:
  assumes (A has_sum x) S
  shows ((λx. A x *V g) has_sum (x *V g)) S
  apply (rule has_sum_bounded_linear[unfolded o_def, of λA. cblinfun_apply A g])
  using assms by (auto simp add: bounded_clinear.bounded_linear cblinfun.bounded_clinear_left)

text ‹The next eight lemmas logically belong in theoryComplex_Bounded_Operators.Complex_Inner_Product
  but the proofs use facts from this theory.›
lemma has_sum_cinner_left:
  assumes (f has_sum x) I
  shows ((λi. cinner a (f i)) has_sum cinner a x) I
  by (metis assms cblinfun_cinner_right.rep_eq has_sum_cblinfun_apply)

lemma summable_on_cinner_left:
  assumes f summable_on I
  shows (λi. cinner a (f i)) summable_on I
  by (metis assms has_sum_cinner_left summable_on_def)

lemma infsum_cinner_left:
  assumes φ summable_on I
  shows cinner ψ (iI. φ i) = (iI. cinner ψ (φ i))
  by (metis assms has_sum_cinner_left has_sum_infsum infsumI)

lemma has_sum_cinner_right:
  assumes (f has_sum x) I
  shows ((λi. f i C a) has_sum (x C a)) I
  using assms has_sum_bounded_linear[unfolded o_def] bounded_antilinear.bounded_linear 
    bounded_antilinear_cinner_left by blast


lemma summable_on_cinner_right:
  assumes f summable_on I
  shows (λi. f i C a) summable_on I
  by (metis assms has_sum_cinner_right summable_on_def)

lemma infsum_cinner_right:
  assumes φ summable_on I
  shows (iI. φ i) C ψ = (iI. φ i C ψ)
  by (metis assms has_sum_cinner_right has_sum_infsum infsumI)

lemma Cauchy_cinner_product_summable:
  assumes asum: a summable_on UNIV
  assumes bsum: b summable_on UNIV
  assumes finite X finite Y
  assumes pos: x y. x  X  y  Y  cinner (a x) (b y)  0
  shows absum: (λ(x, y). cinner (a x) (b y)) summable_on UNIV
proof -
  have ((x,y)F. norm (cinner (a x) (b y)))  norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) + norm (infsum b (-Y)) + 1 
    if finite F and F  (-X)×(-Y) for F
  proof -
    from asum finite X
    have a summable_on (-X)
      by (simp add: Compl_eq_Diff_UNIV summable_on_cofin_subset)
    then obtain MA where finite MA and MA  -X
      and MA: G  MA  G  -X  finite G  norm (sum a G - infsum a (-X))  1 for G
      apply (simp add: summable_iff_has_sum_infsum has_sum_metric dist_norm)
      by (meson less_eq_real_def zero_less_one)
    
    from bsum finite Y
    have b summable_on (-Y)
      by (simp add: Compl_eq_Diff_UNIV summable_on_cofin_subset)
    then obtain MB where finite MB and MB  -Y
      and MB: G  MB  G  -Y  finite G  norm (sum b G - infsum b (-Y))  1 for G
      apply (simp add: summable_iff_has_sum_infsum has_sum_metric dist_norm)
      by (meson less_eq_real_def zero_less_one)

    define F1 F2 where F1 = fst ` F  MA and F2 = snd ` F  MB
    define t1 t2 where t1 = sum a F1 - infsum a (-X) and t2 = sum b F2 - infsum b (-Y)
  
    have [simp]: finite F1 finite F2
      using F1_def F2_def finite MA finite MB that by auto
    have [simp]: F1  -X F2  -Y
      using F  (-X)×(-Y) MA  -X MB  -Y
      by (auto simp: F1_def F2_def)
    from MA[OF _ F1  -X finite F1] have norm t1  1 
      by (auto simp: t1_def F1_def)
    from MB[OF _ F2  -Y finite F2] have norm t2  1 
      by (auto simp: t2_def F2_def)
    have [simp]: F  F1 × F2
      by (force simp: F1_def F2_def image_def)
    have ((x,y)F. norm (cinner (a x) (b y)))  ((x,y)F1×F2. norm (cinner (a x) (b y)))
      by (intro sum_mono2) auto
    also have "... = (xF1 × F2. norm (a (fst x) C b (snd x)))"
      by (auto  simp: case_prod_beta)
    also have "... =  norm (xF1 × F2. a (fst x) C b (snd x))"
    proof -
      have "(xF1 × F2. ¦a (fst x) C b (snd x)¦) = ¦xF1 × F2. a (fst x) C b (snd x)¦"
        by (smt (verit, best) pos sum.cong sum_nonneg ComplD SigmaE F1  - X F2  - Y abs_pos prod.sel subset_iff)
      then show ?thesis
        by (smt (verit) abs_complex_def norm_ge_zero norm_of_real o_def of_real_sum sum.cong sum_norm_le)
    qed
    also from pos have  = norm ((x,y)F1×F2. cinner (a x) (b y))
      by (auto simp: case_prod_beta)
    also have  = norm (cinner (sum a F1) (sum b F2))
      by (simp add: sum.cartesian_product sum_cinner)
    also have  = norm (cinner (infsum a (-X) + t1) (infsum b (-Y) + t2))
      by (simp add: t1_def t2_def)
    also have   norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) * norm t2 + norm t1 * norm (infsum b (-Y)) + norm t1 * norm t2
      apply (simp add: cinner_add_right cinner_add_left)
      by (smt (verit, del_insts) complex_inner_class.Cauchy_Schwarz_ineq2 norm_triangle_ineq)
    also from norm t1  1 norm t2  1
    have   norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) + norm (infsum b (-Y)) + 1
      by (auto intro!: add_mono mult_left_le mult_left_le_one_le mult_le_one)
    finally show ?thesis
      by -
  qed

  then have (λ(x, y). cinner (a x) (b y)) abs_summable_on (-X)×(-Y)
    apply (rule_tac nonneg_bdd_above_summable_on)
    by (auto intro!: bdd_aboveI2 simp: case_prod_unfold)
  then have 1: (λ(x, y). cinner (a x) (b y)) summable_on (-X)×(-Y)
    using abs_summable_summable by blast

  from bsum
  have (λy. b y) summable_on (-Y)
    by (simp add: Compl_eq_Diff_UNIV assms(4) summable_on_cofin_subset)
  then have (λy. cinner (a x) (b y)) summable_on (-Y) for x
    using summable_on_cinner_left by blast
  with finite X have 2: (λ(x, y). cinner (a x) (b y)) summable_on X×(-Y)
    by (force intro: summable_on_product_finite_left)

  from asum
  have (λx. a x) summable_on (-X)
    by (simp add: Compl_eq_Diff_UNIV assms(3) summable_on_cofin_subset)
  then have (λx. cinner (a x) (b y)) summable_on (-X) for y
    using summable_on_cinner_right by blast
  with finite Y have 3: (λ(x, y). cinner (a x) (b y)) summable_on (-X)×Y
    by (force intro: summable_on_product_finite_right)

  have 4: (λ(x, y). cinner (a x) (b y)) summable_on X×Y
    by (simp add: finite X finite Y)

  have §: "UNIV = ((-X) × -Y)  (X × -Y)  ((-X) × Y)  (X × Y)"
    by auto
  show ?thesis
    using 1 2 3 4 by (force simp: § intro!: summable_on_Un_disjoint) 
qed


text ‹A variant of @{thm [source] Series.Cauchy_product_sums} with term(*) replaced by termcinner.
   Differently from @{thm [source] Series.Cauchy_product_sums}, we do not require absolute summability
   of terma and termb individually but only unconditional summability of terma, termb, and their product.
   While on, e.g., reals, unconditional summability is equivalent to absolute summability, in
   general unconditional summability is a weaker requirement.

  Logically belong in theoryComplex_Bounded_Operators.Complex_Inner_Product
  but the proof uses facts from this theory.›
lemma 
  fixes a b :: "nat  'a::complex_inner"
  assumes asum: a summable_on UNIV
  assumes bsum: b summable_on UNIV
  assumes absum: (λ(x, y). cinner (a x) (b y)) summable_on UNIV
    (* ― ‹See @{thm [source] Cauchy_cinner_product_summable} or @{thm [source] Cauchy_cinner_product_summable'} for a way to rewrite this premise.› *)
  shows Cauchy_cinner_product_infsum: (k. ik. cinner (a i) (b (k - i))) = cinner (k. a k) (k. b k)
    and Cauchy_cinner_product_infsum_exists: (λk. ik. cinner (a i) (b (k - i))) summable_on UNIV
proof -
  have img: (λ(k::nat, i). (i, k - i)) ` {(k, i). i  k} = UNIV
    apply (auto simp: image_def)
    by (metis add.commute add_diff_cancel_right' diff_le_self)
  have inj: inj_on (λ(k::nat, i). (i, k - i)) {(k, i). i  k}
    by (smt (verit, del_insts) Pair_inject case_prodE case_prod_conv eq_diff_iff inj_onI mem_Collect_eq)
  have sigma: (SIGMA k:UNIV. {i. i  k}) = {(k, i). i  k}
    by auto

  from absum
  have §: (λ(x, y). cinner (a y) (b (x - y))) summable_on {(k, i). i  k}
    by (rule Cauchy_cinner_product_summable'[THEN iffD1])
  then have (λk. i|ik. cinner (a i) (b (k-i))) summable_on UNIV
    by (metis (mono_tags, lifting) sigma summable_on_Sigma_banach summable_on_cong)
  then show (λk. ik. cinner (a i) (b (k - i))) summable_on UNIV
    by (metis (mono_tags, lifting) atMost_def finite_Collect_le_nat infsum_finite summable_on_cong)

  have cinner (k. a k) (k. b k) = (k. l. cinner (a k) (b l))
    by (smt (verit, best) asum bsum infsum_cinner_left infsum_cinner_right infsum_cong)
  also have  = ((k,l). cinner (a k) (b l))
    by (smt (verit) UNIV_Times_UNIV infsum_Sigma'_banach infsum_cong local.absum)
  also have  = ((k, l)(λ(k, i). (i, k - i)) ` {(k, i). i  k}. cinner (a k) (b l))
    by (simp only: img)
  also have  = infsum ((λ(k, l). a k C b l)  (λ(k, i). (i, k - i))) {(k, i). i  k}
    using inj by (rule infsum_reindex)
  also have  = ((k,i)|ik. a i C b (k-i))
    by (simp add: o_def case_prod_unfold)
  also have  = (k. i|ik. a i C b (k-i))
    by (metis (no_types) § infsum_Sigma'_banach sigma)
  also have  = (k. ik. a i C b (k-i))
    by (simp add: atMost_def)
  finally show (k. ik. a i C b (k - i)) = (k. a k) C (k. b k)
    by simp
qed


lemma CBlinfun_plus: 
  assumes [simp]: bounded_clinear f bounded_clinear g
  shows CBlinfun (f + g) = CBlinfun f + CBlinfun g
  by (auto intro!: cblinfun_eqI simp: plus_fun_def bounded_clinear_add CBlinfun_inverse cblinfun.add_left)

lemma CBlinfun_scaleC:
  assumes bounded_clinear f
  shows CBlinfun (λy. c *C f y) = c *C CBlinfun f
  by (simp add: assms eq_onp_same_args scaleC_cblinfun.abs_eq)


lemma cinner_sup_norm_cblinfun:
  fixes A :: 'a::{complex_normed_vector,not_singleton} CL 'b::complex_inner
  shows norm A = (SUP (ψ,φ). cmod (cinner ψ (A *V φ)) / (norm ψ * norm φ))
  apply transfer
  apply (rule cinner_sup_onorm)
  by (simp add: bounded_clinear.bounded_linear)


lemma norm_cblinfun_Sup: norm A = (SUP ψ. norm (A *V ψ) / norm ψ)
  by (simp add: norm_cblinfun.rep_eq onorm_def)

lemma cblinfun_eq_on:
  fixes A B :: "'a::cbanach CL'b::complex_normed_vector"
  assumes "x. x  G  A *V x = B *V x" and t  closure (cspan G)
  shows "A *V t = B *V t"
  using assms
  apply transfer
  using bounded_clinear_eq_on_closure by blast

lemma cblinfun_eq_gen_eqI:
  fixes A B :: "'a::cbanach CL'b::complex_normed_vector"
  assumes "x. x  G  A *V x = B *V x" and ccspan G = 
  shows "A = B"
  by (metis assms cblinfun_eqI cblinfun_eq_on ccspan.rep_eq iso_tuple_UNIV_I top_ccsubspace.rep_eq)

declare cnj_bounded_antilinear[bounded_antilinear]

lemma Cblinfun_comp_bounded_cbilinear: bounded_clinear (CBlinfun o p) if bounded_cbilinear p
  by (metis bounded_cbilinear.bounded_clinear_prod_right bounded_cbilinear.prod_right_def comp_id map_fun_def that)

lemma Cblinfun_comp_bounded_sesquilinear: bounded_antilinear (CBlinfun o p) if bounded_sesquilinear p
  by (metis (mono_tags, opaque_lifting) bounded_clinear_CBlinfun_apply bounded_sesquilinear.bounded_clinear_right comp_apply that transfer_bounded_sesquilinear_bounded_antilinearI)

subsection ‹Relationship to real bounded operators (typ_ L _)›

instantiation blinfun :: (real_normed_vector, complex_normed_vector) "complex_normed_vector"
begin
lift_definition scaleC_blinfun :: complex 
 ('a::real_normed_vector, 'b::complex_normed_vector) blinfun 
 ('a, 'b) blinfun
  is λ c::complex. λ f::'a'b. (λ x. c *C (f x) )
proof
  fix c::complex and f :: 'a'b and b1::'a and b2::'a
  assume bounded_linear f
  show c *C f (b1 + b2) = c *C f b1 + c *C f b2
    by (simp add: bounded_linear f linear_simps scaleC_add_right)

  fix c::complex and f :: 'a'b and b::'a and r::real
  assume bounded_linear f
  show c *C f (r *R b) = r *R (c *C f b)
    by (simp add: bounded_linear f linear_simps(5) scaleR_scaleC)

  fix c::complex and f :: 'a'b
  assume bounded_linear f

  have  K.  x. norm (f x)  norm x * K
    using bounded_linear f
    by (simp add: bounded_linear.bounded)
  then obtain K where  x. norm (f x)  norm x * K
    by blast
  have cmod c  0
    by simp
  hence  x. (cmod c) * norm (f x)  (cmod c) * norm x * K
    using   x. norm (f x)  norm x * K
    by (metis ordered_comm_semiring_class.comm_mult_left_mono vector_space_over_itself.scale_scale)
  moreover have norm (c *C f x) = (cmod c) * norm (f x)
    for x
    by simp
  ultimately show K. x. norm (c *C f x)  norm x * K
    by (metis ab_semigroup_mult_class.mult_ac(1) mult.commute)
qed

instance
proof
  have "r *R x = complex_of_real r *C x"
    for x :: "('a, 'b) blinfun" and r
    by transfer (simp add: scaleR_scaleC)
  thus "((*R) r::'a L 'b  _) = (*C) (complex_of_real r)" for r
    by auto
  show "a *C (x + y) = a *C x + a *C y"
    for a :: complex and x y :: "'a L 'b"
    by transfer (simp add: scaleC_add_right)

  show "(a + b) *C x = a *C x + b *C x"
    for a b :: complex and x :: "'a L 'b"
    by transfer (simp add: scaleC_add_left)

  show "a *C b *C x = (a * b) *C x"
    for a b :: complex and x :: "'a L 'b"
    by transfer simp

  have 1 *C f x = f x
    for f :: 'a'b and x
    by auto
  thus "1 *C x = x"
    for x :: "'a L 'b"
    by (simp add: scaleC_blinfun.rep_eq blinfun_eqI)

  have onorm (λx. a *C f x) = cmod a * onorm f
    if bounded_linear f
    for f :: 'a  'b and a :: complex
  proof-
    have cmod a  0
      by simp
    have  K::real.  x. (¦ ereal ((norm (f x)) / (norm x)) ¦)  K
      using bounded_linear f le_onorm by fastforce
    then obtain K::real where  x. (¦ ereal ((norm (f x)) / (norm x)) ¦)  K
      by blast
    hence   x. (cmod a) *(¦ ereal ((norm (f x)) / (norm x)) ¦)  (cmod a) * K
      using cmod a  0
      by (metis abs_ereal.simps(1) abs_ereal_pos   abs_pos ereal_mult_left_mono  times_ereal.simps(1))
    hence   x.  (¦ ereal ((cmod a) * (norm (f x)) / (norm x)) ¦)  (cmod a) * K
      by simp
    hence bdd_above {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}
      by simp
    moreover have {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}  {}
      by auto
    ultimately have p1: (SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦)  cmod a * K
      using  x. ¦ ereal (cmod a * (norm (f x)) / (norm x)) ¦  cmod a * K
        Sup_least mem_Collect_eq
      by (simp add: SUP_le_iff)
    have  p2: i. i  UNIV  0  ereal (cmod a * norm (f i) / norm i)
      by simp
    hence ¦SUP x. ereal (cmod a * (norm (f x)) / (norm x))¦
               (SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦)
      using  bdd_above {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}
        {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}  {}
      by (metis (mono_tags, lifting) SUP_upper2 Sup.SUP_cong UNIV_I
          p2 abs_ereal_ge0 ereal_le_real)
    hence ¦SUP x. ereal (cmod a * (norm (f x)) / (norm x))¦  cmod a * K
      using  (SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦)  cmod a * K
      by simp
    hence ¦ ( SUP iUNIV::'a set. ereal ((λ x. (cmod a) * (norm (f x)) / norm x) i)) ¦  
      by auto
    hence w2: ( SUP iUNIV::'a set. ereal ((λ x. cmod a * (norm (f x)) / norm x) i))
             = ereal ( Sup ((λ x. cmod a * (norm (f x)) / norm x) ` (UNIV::'a set) ))
      by (simp add: ereal_SUP)
    have (UNIV::('a set))  {}
      by simp
    moreover have  i. i  (UNIV::('a set))  (λ x. (norm (f x)) / norm x :: ereal) i  0
      by simp
    moreover have cmod a  0
      by simp
    ultimately have (SUP i(UNIV::('a set)). ((cmod a)::ereal) * (λ x. (norm (f x)) / norm x :: ereal) i )
        = ((cmod a)::ereal) * ( SUP i(UNIV::('a set)). (λ x. (norm (f x)) / norm x :: ereal) i )
      by (simp add: Sup_ereal_mult_left')
    hence (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) )
        = ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) )
      by simp
    hence z1: real_of_ereal ( (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) ) )
        = real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
      by simp
    have z2: real_of_ereal (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) )
                  = (SUP x. cmod a * (norm (f x) / norm x))
      using w2
      by auto
    have real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
                =  (cmod a) * real_of_ereal ( SUP x. ( (norm (f x)) / norm x :: ereal) )
      by simp
    moreover have real_of_ereal ( SUP x. ( (norm (f x)) / norm x :: ereal) )
                  = ( SUP x. ((norm (f x)) / norm x) )
    proof-
      have ¦ ( SUP iUNIV::'a set. ereal ((λ x. (norm (f x)) / norm x) i)) ¦  
      proof-
        have  K::real.  x. (¦ ereal ((norm (f x)) / (norm x)) ¦)  K
          using bounded_linear f le_onorm by fastforce
        then obtain K::real where  x. (¦ ereal ((norm (f x)) / (norm x)) ¦)  K
          by blast
        hence bdd_above {ereal ((norm (f x)) / (norm x)) | x. True}
          by simp
        moreover have {ereal ((norm (f x)) / (norm x)) | x. True}  {}
          by auto
        ultimately have (SUP x. ¦ereal ((norm (f x)) / (norm x))¦)  K
          using  x. ¦ ereal ((norm (f x)) / (norm x)) ¦  K
            Sup_least mem_Collect_eq
          by (simp add: SUP_le_iff)
        hence ¦SUP x. ereal ((norm (f x)) / (norm x))¦
               (SUP x. ¦ereal ((norm (f x)) / (norm x))¦)
          using  bdd_above {ereal ((norm (f x)) / (norm x)) | x. True}
            {ereal ((norm (f x)) / (norm x)) | x. True}  {}
          by (metis (mono_tags, lifting) SUP_upper2 Sup.SUP_cong UNIV_I i. i  UNIV  0  ereal (norm (f i) / norm i) abs_ereal_ge0 ereal_le_real)
        hence ¦SUP x. ereal ((norm (f x)) / (norm x))¦  K
          using  (SUP x. ¦ereal ((norm (f x)) / (norm x))¦)  K
          by simp
        thus ?thesis
          by auto
      qed
      hence ( SUP iUNIV::'a set. ereal ((λ x. (norm (f x)) / norm x) i))
             = ereal ( Sup ((λ x. (norm (f x)) / norm x) ` (UNIV::'a set) ))
        by (simp add: ereal_SUP)
      thus ?thesis
        by simp
    qed
    have z3: real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
                = cmod a * (SUP x. norm (f x) / norm x)
      by (simp add: real_of_ereal (SUP x. ereal (norm (f x) / norm x)) = (SUP x. norm (f x) / norm x))
    hence w1: (SUP x. cmod a * (norm (f x) / norm x)) =
          cmod a * (SUP x. norm (f x) / norm x)
      using z1 z2 by linarith
    have v1: onorm (λx. a *C f x) = (SUP x. norm (a *C f x) / norm x)
      by (simp add: onorm_def)
    have v2: (SUP x. norm (a *C f x) / norm x) = (SUP x. ((cmod a) * norm (f x)) / norm x)
      by simp
    have v3: (SUP x. ((cmod a) * norm (f x)) / norm x) =  (SUP x. (cmod a) * ((norm (f x)) / norm x))
      by simp
    have v4: (SUP x. (cmod a) * ((norm (f x)) / norm x)) = (cmod a) *  (SUP x. ((norm (f x)) / norm x))
      using w1
      by blast
    show onorm (λx. a *C f x) = cmod a * onorm f
      using v1 v2 v3 v4
      by (metis (mono_tags, lifting) onorm_def)
  qed
  thus norm (a *C x) = cmod a * norm x
    for a::complex and x::('a, 'b) blinfun
    by transfer blast
qed
end

(* We do not have clinear_blinfun_compose_right *)
lemma clinear_blinfun_compose_left: clinear (λx. blinfun_compose x y)
  by (auto intro!: clinearI simp: blinfun_eqI scaleC_blinfun.rep_eq bounded_bilinear.add_left
                                  bounded_bilinear_blinfun_compose)

instance blinfun :: (real_normed_vector, cbanach) cbanach..

lemma blinfun_compose_assoc: "(A oL B) oL C = A oL (B  oL C)"
  by (simp add: blinfun_eqI)

lift_definition blinfun_of_cblinfun::'a::complex_normed_vector CL 'b::complex_normed_vector
   'a L 'b is "id"
  by transfer (simp add: bounded_clinear.bounded_linear)

lift_definition blinfun_cblinfun_eq ::
  'a L 'b  'a::complex_normed_vector CL 'b::complex_normed_vector  bool is "(=)" .

lemma blinfun_cblinfun_eq_bi_unique[transfer_rule]: bi_unique blinfun_cblinfun_eq
  unfolding bi_unique_def by transfer auto

lemma blinfun_cblinfun_eq_right_total[transfer_rule]: right_total blinfun_cblinfun_eq
  unfolding right_total_def by transfer (simp add: bounded_clinear.bounded_linear)

named_theorems cblinfun_blinfun_transfer

lemma cblinfun_blinfun_transfer_0[cblinfun_blinfun_transfer]:
  "blinfun_cblinfun_eq (0::(_,_) blinfun) (0::(_,_) cblinfun)"
  by transfer simp

lemma cblinfun_blinfun_transfer_plus[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (+) (+)"
  unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_minus[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (-) (-)"
  unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_uminus[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (uminus) (uminus)"
  unfolding rel_fun_def by transfer auto

definition "real_complex_eq r c  complex_of_real r = c"

lemma bi_unique_real_complex_eq[transfer_rule]: bi_unique real_complex_eq
  unfolding real_complex_eq_def bi_unique_def by auto

lemma left_total_real_complex_eq[transfer_rule]: left_total real_complex_eq
  unfolding real_complex_eq_def left_total_def by auto

lemma cblinfun_blinfun_transfer_scaleC[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(real_complex_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (scaleR) (scaleC)"
  unfolding rel_fun_def by transfer (simp add: real_complex_eq_def scaleR_scaleC)

lemma cblinfun_blinfun_transfer_CBlinfun[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(eq_onp bounded_clinear ===> blinfun_cblinfun_eq) Blinfun CBlinfun"
  unfolding rel_fun_def blinfun_cblinfun_eq.rep_eq eq_onp_def
  by (auto simp: CBlinfun_inverse Blinfun_inverse bounded_clinear.bounded_linear)

lemma cblinfun_blinfun_transfer_norm[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> (=)) norm norm"
  unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_dist[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> (=)) dist dist"
  unfolding rel_fun_def dist_norm by transfer auto

lemma cblinfun_blinfun_transfer_sgn[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) sgn sgn"
  unfolding rel_fun_def sgn_blinfun_def sgn_cblinfun_def by transfer (auto simp: scaleR_scaleC)

lemma cblinfun_blinfun_transfer_Cauchy[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(((=) ===> blinfun_cblinfun_eq) ===> (=)) Cauchy Cauchy"
proof -
  note cblinfun_blinfun_transfer[transfer_rule]
  show ?thesis
    unfolding Cauchy_def
    by transfer_prover
qed

lemma cblinfun_blinfun_transfer_tendsto[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) tendsto tendsto"
proof -
  note cblinfun_blinfun_transfer[transfer_rule]
  show ?thesis
    unfolding tendsto_iff
    by transfer_prover
qed

lemma cblinfun_blinfun_transfer_compose[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (oL) (oCL)"
  unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_apply[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> (=) ===> (=)) blinfun_apply cblinfun_apply"
  unfolding rel_fun_def by transfer auto

lemma blinfun_of_cblinfun_inj:
  blinfun_of_cblinfun f = blinfun_of_cblinfun g  f = g
  by (metis cblinfun_apply_inject blinfun_of_cblinfun.rep_eq)

lemma blinfun_of_cblinfun_inv:
  assumes "c. x. f *v (c *C x) = c *C (f *v x)"
  shows "g. blinfun_of_cblinfun g = f"
  using assms
proof transfer
  show "gCollect bounded_clinear. id g = f"
    if "bounded_linear f"
      and "c x. f (c *C x) = c *C f x"
    for f :: "'a  'b"
    using that bounded_linear_bounded_clinear by auto
qed

lemma blinfun_of_cblinfun_zero:
  blinfun_of_cblinfun 0 = 0
  by transfer simp

lemma blinfun_of_cblinfun_uminus:
  blinfun_of_cblinfun (- f) = - (blinfun_of_cblinfun f)
  by transfer auto

lemma blinfun_of_cblinfun_minus:
  blinfun_of_cblinfun (f - g) = blinfun_of_cblinfun f - blinfun_of_cblinfun g
  by transfer auto

lemma blinfun_of_cblinfun_scaleC:
  blinfun_of_cblinfun (c *C f) = c *C (blinfun_of_cblinfun f)
  by transfer auto

lemma blinfun_of_cblinfun_scaleR:
  blinfun_of_cblinfun (c *R f) = c *R (blinfun_of_cblinfun f)
  by transfer auto

lemma blinfun_of_cblinfun_norm:
  fixes f::'a::complex_normed_vector CL 'b::complex_normed_vector
  shows norm f = norm (blinfun_of_cblinfun f)
  by transfer auto

lemma blinfun_of_cblinfun_cblinfun_compose:
  fixes f::'b::complex_normed_vector CL 'c::complex_normed_vector
    and g::'a::complex_normed_vector CL 'b
  shows blinfun_of_cblinfun (f  oCL g) = (blinfun_of_cblinfun f) oL (blinfun_of_cblinfun g)
  by transfer auto

subsection ‹Composition›

lemma cblinfun_compose_assoc:
  shows "(A oCL B) oCL C = A oCL (B oCL C)"
  by (metis (no_types, lifting) cblinfun_apply_inject fun.map_comp cblinfun_compose.rep_eq)

lemma cblinfun_compose_zero_right[simp]: "U oCL 0 = 0"
  using bounded_cbilinear.zero_right bounded_cbilinear_cblinfun_compose by blast

lemma cblinfun_compose_zero_left[simp]: "0 oCL U = 0"
  using bounded_cbilinear.zero_left bounded_cbilinear_cblinfun_compose by blast

lemma cblinfun_compose_scaleC_left[simp]:
  fixes A::"'b::complex_normed_vector CL 'c::complex_normed_vector"
    and B::"'a::complex_normed_vector CL 'b"
  shows (a *C A) oCL B = a *C (A oCL B)
  by (simp add: bounded_cbilinear.scaleC_left bounded_cbilinear_cblinfun_compose)

lemma cblinfun_compose_scaleR_left[simp]:
  fixes A::"'b::complex_normed_vector CL 'c::complex_normed_vector"
    and B::"'a::complex_normed_vector CL 'b"
  shows (a *R A) oCL B = a *R (A oCL B)
  by (simp add: scaleR_scaleC)

lemma cblinfun_compose_scaleC_right[simp]:
  fixes A::"'b::complex_normed_vector CL 'c::complex_normed_vector"
    and B::"'a::complex_normed_vector CL 'b"
  shows A oCL (a *C B) = a *C (A oCL B)
  by transfer (auto intro!: ext bounded_clinear.clinear complex_vector.linear_scale)

lemma cblinfun_compose_scaleR_right[simp]:
  fixes A::"'b::complex_normed_vector CL 'c::complex_normed_vector"
    and B::"'a::complex_normed_vector CL 'b"
  shows A oCL (a *R B) = a *R (A oCL B)
  by (simp add: scaleR_scaleC)

lemma cblinfun_compose_id_right[simp]:
  shows "U oCL id_cblinfun = U"
  by transfer auto

lemma cblinfun_compose_id_left[simp]:
  shows "id_cblinfun oCL U  = U"
  by transfer auto

lemma cblinfun_compose_add_left: (a + b) oCL c = (a oCL c) + (b oCL c)
  by (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose)

lemma cblinfun_compose_add_right: a oCL (b + c) = (a oCL b) + (a oCL c)
  by (simp add: bounded_cbilinear.add_right bounded_cbilinear_cblinfun_compose)

lemma cbilinear_cblinfun_compose[simp]: "cbilinear cblinfun_compose"
  by (auto intro!: clinearI simp add: cbilinear_def bounded_cbilinear.add_left bounded_cbilinear.add_right bounded_cbilinear_cblinfun_compose)

lemma cblinfun_compose_sum_left: (iS. g i) oCL x = (iS. g i oCL x)
  by (induction S rule:infinite_finite_induct) (auto simp: cblinfun_compose_add_left)

lemma cblinfun_compose_sum_right: x oCL (iS. g i) = (iS. x oCL g i)
  by (induction S rule:infinite_finite_induct) (auto simp: cblinfun_compose_add_right)

lemma cblinfun_compose_minus_right: a oCL (b - c) = (a oCL b) - (a oCL c)
  by (simp add: bounded_cbilinear.diff_right bounded_cbilinear_cblinfun_compose)
lemma cblinfun_compose_minus_left: (a - b) oCL c = (a oCL c) - (b oCL c)
  by (simp add: bounded_cbilinear.diff_left bounded_cbilinear_cblinfun_compose)


lemma simp_a_oCL_b: a oCL b = c  a oCL (b oCL d) = c oCL d
  ― ‹A convenience lemma to transform simplification rules of the form terma oCL b = c.
     E.g., simp_a_oCL_b[OF isometryD, simp]› declares a simp-rule for simplifying termadj x oCL (x oCL y) = id_cblinfun oCL y.›
  by (auto simp: cblinfun_compose_assoc)

lemma simp_a_oCL_b': a oCL b = c  a *V (b *V d) = c *V d
  ― ‹A convenience lemma to transform simplification rules of the form terma oCL b = c.
     E.g., simp_a_oCL_b'[OF isometryD, simp]› declares a simp-rule for simplifying termadj x *V x *V y = id_cblinfun *V y.›
  by auto

lemma cblinfun_compose_uminus_left: (- a) oCL b = - (a oCL b)
  by (simp add: bounded_cbilinear.minus_left bounded_cbilinear_cblinfun_compose)

lemma cblinfun_compose_uminus_right: a oCL (- b) = - (a oCL b)
  by (simp add: bounded_cbilinear.minus_right bounded_cbilinear_cblinfun_compose)

lemma bounded_clinear_cblinfun_compose_left: bounded_clinear (λx. x oCL y)
  by (simp add: bounded_cbilinear.bounded_clinear_left bounded_cbilinear_cblinfun_compose)
lemma bounded_clinear_cblinfun_compose_right: bounded_clinear (λy. x oCL y)
  by (simp add: bounded_cbilinear.bounded_clinear_right bounded_cbilinear_cblinfun_compose)
lemma clinear_cblinfun_compose_left: clinear (λx. x oCL y)
  by (simp add: bounded_cbilinear.bounded_clinear_left bounded_cbilinear_cblinfun_compose bounded_clinear.clinear)
lemma clinear_cblinfun_compose_right: clinear (λy. x oCL y)
  by (simp add: bounded_clinear.clinear bounded_clinear_cblinfun_compose_right)

lemma additive_cblinfun_compose_left[simp]: Modules.additive (λx. x oCL a)
  by (simp add: Modules.additive_def cblinfun_compose_add_left)
lemma additive_cblinfun_compose_right[simp]: Modules.additive (λx. a oCL x)
  by (simp add: Modules.additive_def cblinfun_compose_add_right)
lemma isCont_cblinfun_compose_left: isCont (λx. x oCL a) y
  apply (rule clinear_continuous_at)
  by (rule bounded_clinear_cblinfun_compose_left)
lemma isCont_cblinfun_compose_right: isCont (λx. a oCL x) y
  apply (rule clinear_continuous_at)
  by (rule bounded_clinear_cblinfun_compose_right)

lemma cspan_compose_closed:
  assumes a b. a  A  b  A  a oCL b  A
  assumes a  cspan A and b  cspan A
  shows a oCL b  cspan A
proof -
  from a  cspan A
  obtain F f where finite F and F  A and a_def: a = (xF. f x *C x)
    by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
  from b  cspan A
  obtain G g where finite G and G  A and b_def: b = (xG. g x *C x)
    by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
  have a oCL b = ((x,y)F×G. (f x *C x) oCL (g y *C y))
    apply (simp add: a_def b_def cblinfun_compose_sum_left)
    by (auto intro!: sum.cong simp add: cblinfun_compose_sum_right scaleC_sum_right sum.cartesian_product case_prod_beta)
  also have  = ((x,y)F×G. (f x * g y) *C (x oCL y))
    by (metis (no_types, opaque_lifting) cblinfun_compose_scaleC_left cblinfun_compose_scaleC_right scaleC_scaleC)
  also have   cspan A
    using assms G  A F  A
    apply (auto intro!: complex_vector.span_sum complex_vector.span_scale 
        simp: complex_vector.span_clauses)
    using complex_vector.span_clauses(1) by blast
  finally show ?thesis
    by -
qed

subsection ‹Adjoint›

lift_definition
  adj :: "'a::chilbert_space CL 'b::complex_inner  'b CL 'a" ("_*" [99] 100)
  is cadjoint by (fact cadjoint_bounded_clinear)

definition selfadjoint :: ('a::chilbert_space CL 'a)  bool where
  selfadjoint a  a* = a

lemma id_cblinfun_adjoint[simp]: "id_cblinfun* = id_cblinfun"
  by (metis adj.rep_eq apply_id_cblinfun cadjoint_id cblinfun_apply_inject)

lemma double_adj[simp]: "(A*)* = A"
  apply transfer using double_cadjoint by blast

lemma adj_cblinfun_compose[simp]:
  fixes B::'a::chilbert_space CL 'b::chilbert_space
    and A::'b CL 'c::complex_inner
  shows "(A oCL B)* =  (B*) oCL (A*)"
proof transfer
  fix  A :: 'b  'c and B :: 'a  'b
  assume bounded_clinear A and bounded_clinear B
  hence bounded_clinear (A  B)
    by (simp add: comp_bounded_clinear)
  have ((A  B) u C v) = (u C (B  A) v)
    for u v
    by (metis (no_types, lifting) cadjoint_univ_prop bounded_clinear A bounded_clinear B cinner_commute' comp_def)
  thus (A  B) = B  A
    using bounded_clinear (A  B)
    by (metis cadjoint_eqI cinner_commute')
qed

lemma scaleC_adj[simp]: "(a *C A)* = (cnj a) *C (A*)"
  by transfer (simp add: bounded_clinear.bounded_linear bounded_clinear_def complex_vector.linear_scale scaleC_cadjoint)

lemma scaleR_adj[simp]: "(a *R A)* = a *R (A*)"
  by (simp add: scaleR_scaleC)

lemma adj_plus: (A + B)* = (A*) + (B*)
proof transfer
  fix A B::'b  'a
  assume a1: bounded_clinear A and a2: bounded_clinear B
  define F where F = (λx. (A) x + (B) x)
  define G where G = (λx. A x + B x)
  have bounded_clinear G
    unfolding G_def
    by (simp add: a1 a2 bounded_clinear_add)
  moreover have (F u C v) = (u C G v) for u v
    unfolding F_def G_def
    using cadjoint_univ_prop a1 a2 cinner_add_left
    by (simp add: cadjoint_univ_prop cinner_add_left cinner_add_right)
  ultimately have F = G
    using cadjoint_eqI by blast
  thus (λx. A x + B x) = (λx. (A) x + (B) x)
    unfolding F_def G_def
    by auto
qed

lemma cinner_adj_left:
  fixes G :: "'b::chilbert_space CL 'a::complex_inner"
  shows (G* *V x) C y = x C (G *V y)
  apply transfer using cadjoint_univ_prop by blast

lemma cinner_adj_right:
  fixes G :: "'b::chilbert_space CL 'a::complex_inner"
  shows x C (G* *V y) = (G *V x) C y
  apply transfer using cadjoint_univ_prop' by blast

lemma adj_0[simp]: 0* = 0
  by (metis add_cancel_right_left adj_plus)

lemma selfadjoint_0[simp]: selfadjoint 0
  by (simp add: selfadjoint_def)

lemma norm_adj[simp]: norm (A*) = norm A
  for A :: 'b::chilbert_space CL 'c::complex_inner
proof (cases (x y :: 'b. x  y)  (x y :: 'c. x  y))
  case True
  then have c1: class.not_singleton TYPE('b)
    by intro_classes simp
  from True have c2: class.not_singleton TYPE('c)
    by intro_classes simp
  have normA: norm A = (SUP (ψ, φ). cmod (ψ C (A *V φ)) / (norm ψ * norm φ))
    apply (rule cinner_sup_norm_cblinfun[internalize_sort 'a::{complex_normed_vector,not_singleton}])
     apply (rule complex_normed_vector_axioms)
    by (rule c1)
  have normAadj: norm (A*) = (SUP (ψ, φ). cmod (ψ C (A* *V φ)) / (norm ψ * norm φ))
    apply (rule cinner_sup_norm_cblinfun[internalize_sort 'a::{complex_normed_vector,not_singleton}])
     apply (rule complex_normed_vector_axioms)
    by (rule c2)

  have norm (A*) = (SUP (ψ, φ). cmod (φ C (A *V ψ)) / (norm ψ * norm φ))
    unfolding normAadj
    apply (subst cinner_adj_right)
    apply (subst cinner_commute)
    apply (subst complex_mod_cnj)
    by rule
  also have  = Sup ((λ(ψ, φ). cmod (φ C (A *V ψ)) / (norm ψ * norm φ)) ` prod.swap ` UNIV)
    by auto
  also have  = (SUP (φ, ψ). cmod (φ C (A *V ψ)) / (norm ψ * norm φ))
    apply (subst image_image)
    by auto
  also have  = norm A
    unfolding normA
    by (simp add: mult.commute)
  finally show ?thesis
    by -
next
  case False
  then consider (b) x::'b. x = 0 | (c) x::'c. x = 0
    by auto
  then have A = 0
    apply (cases; transfer)
     apply (metis (full_types) bounded_clinear_def complex_vector.linear_0)
    by auto
  then show norm (A*) = norm A
    by simp
qed


lemma antilinear_adj[simp]: antilinear adj
  by (simp add: adj_plus antilinearI)

lemma bounded_antilinear_adj[bounded_antilinear, simp]: bounded_antilinear adj
  by (auto intro!: antilinearI exI[of _ 1] simp: bounded_antilinear_def bounded_antilinear_axioms_def adj_plus)

lemma adjoint_eqI:
  fixes G:: 'b::chilbert_space CL 'a::complex_inner
    and F:: 'a CL 'b
  assumes x y. ((cblinfun_apply F) x C y) = (x C (cblinfun_apply G) y)
  shows F = G*
  using assms apply transfer using cadjoint_eqI by auto

lemma adj_uminus: (-A)* = - (A*)
  by (metis scaleR_adj scaleR_minus1_left scaleR_minus1_left)

lemma cinner_real_hermiteanI:
  ― ‹Prop. II.2.12 in citeconway2013course
  assumes ψ. ψ C (A *V ψ)  
  shows A* = A
proof -
  { fix g h :: 'a
    {
      fix α :: complex
      have