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
    Complex_Inner_Product One_Dimensional_Spaces
    Banach_Steinhaus.Banach_Steinhaus
    "HOL-Types_To_Sets.Types_To_Sets"
    Complex_Bounded_Linear_Function0
begin

unbundle lattice_syntax

subsection Misc basic facts and declarations

notation cblinfun_apply (infixr "*V" 70)

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

lemma isCont_cblinfun_apply[simp]: "isCont ((*V) A) ψ"
  apply transfer
  by (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 ψ. cinner ψ (A *V ψ) = cinner ψ (B *V ψ)
  shows A = B
proof -
  define C where C = A - B
  have C0[simp]: cinner ψ (C ψ) = 0 for ψ
    by (simp add: C_def 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 apply transfer
  by (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
  apply (rule complex_vector.linear_eq_0_on_span[where f=F])
  using bounded_clinear.axioms(1) cblinfun_apply assms by auto

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
  apply (rule complex_vector.linear_eq_on_span[where f=F])
  using bounded_clinear.axioms(1) cblinfun_apply assms by auto

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
proof-
  have "F - G = 0"
    apply (rule cblinfun_eq_0_on_UNIV_span[where basis=basis])
    using assms by (auto simp add: cblinfun.diff_left)
  thus ?thesis by simp
qed

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"
  apply (rule cblinfun_eq_on_UNIV_span[where basis=basis])
  using assms is_generator_set is_cindependent_set by auto

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  v, F *V u = 0"
  shows "F = 0"
proof-
  have "F *V u = 0"
    if "ubasisA" for u
  proof-
    have "v. vbasisB  v, F *V u = 0"
      by (simp add: assms(3) that)
    moreover have "(v. vbasisB  v, x = 0)  x = 0"
      for x
    proof-
      assume r1: "v. vbasisB  v, x = 0"
      have "v, x = 0" 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, x = (at. s a *C a), x"
          by (simp add: b1)
        also have " = (at. s a *C a, x)"
          using cinner_sum_left by blast
        also have " = (at. cnj (s a) * a, 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, 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, F *V u = v, G *V u"
  shows "F = G"
proof-
  define H where "H = F - G"
  have "u v. ubasisA  vbasisB  v, H *V u = 0"
    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, v = G *V u, v"
  shows "F = G"
  using cinner_canonical_basis_eq assms
  by (metis cinner_commute')

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: Complex_Vector_Spaces0.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
    apply auto
    by (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_to_CARD_1_0[simp]: (A :: _ CL _::CARD_1) = 0
  apply (rule cblinfun_eqI)
  by auto

lemma cblinfun_from_CARD_1_0[simp]: (A :: _::CARD_1 CL _) = 0
  apply (rule cblinfun_eqI)
  apply (subst CARD_1_vec_0)
  by auto


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 apply atomize_elim by 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, ccfv_threshold) complex_vector.span_base complex_vector.span_scale complex_vector.span_sum mem_Collect_eq subset_eq)
    moreover have G *V a' = (if a'=a then b else 0) if a'basisA' for a'
      apply (cases a'=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 apply (rule cblinfun_eq_on_UNIV_span)
      apply (auto simp: H'_def cblinfun.sum_left)
      apply (subst sum_single)
      by (auto simp: 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})
    using F_basis
    by (smt (z3) UN_subset_iff complex_vector.span_alt complex_vector.span_minimal complex_vector.subspace_span mem_Collect_eq subset_iff)

  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 cspan basis = UNIV
    apply (rule cblinfun_cspan_UNIV[where basisA=basisA and basisB=basisB])
      apply (auto simp: basis_def)
    by (metis F_apply f_a f_not_a)

  moreover have finite basis
    unfolding basis_def apply (rule finite_image_set2) by auto

  ultimately show S :: ('a CL 'b) set. finite S  cspan S = UNIV
    by auto
qed


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
    apply transfer
    by (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"
    apply transfer
    by (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"
    apply transfer
    by (simp add: scaleC_add_left)

  show "a *C b *C x = (a * b) *C x"
    for a b :: complex and x :: "'a L 'b"
    apply transfer
    by 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
    apply transfer
    by 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)

instantiation blinfun :: (real_normed_vector, cbanach) "cbanach"
begin
instance..
end

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"
  apply transfer by (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 apply transfer by auto

lemma blinfun_cblinfun_eq_right_total[transfer_rule]: right_total blinfun_cblinfun_eq
  unfolding right_total_def apply transfer
  by (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)"
  apply transfer by 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 apply transfer by 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 apply transfer by 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 apply transfer by 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 apply transfer
  by (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 apply transfer by 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 apply transfer by 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 apply transfer
  by (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 apply transfer by auto

lemma cblinfun_blinfun_transfer_apply[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(blinfun_cblinfun_eq ===> (=) ===> (=)) blinfun_apply cblinfun_apply"
  unfolding rel_fun_def apply transfer by 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
  apply transfer by simp

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

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

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

lemma blinfun_of_cblinfun_scaleR:
  blinfun_of_cblinfun (c *R f) = c *R (blinfun_of_cblinfun f)
  apply transfer by 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)
  apply transfer by auto

subsection Composition

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)
  apply transfer by auto

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)
  apply transfer by (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"
  apply transfer by auto

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

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 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"
  apply (rule cblinfun_eqI)
  apply (rule cblinfun_eq_on[where G=G])
  using assms apply auto
  by (metis ccspan.rep_eq iso_tuple_UNIV_I top_ccsubspace.rep_eq)

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)


subsection Adjoint

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

lemma id_cblinfun_adjoint[simp]: "id_cblinfun* = id_cblinfun"
  apply transfer using cadjoint_id
  by (metis eq_id_iff)

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, v  =  u, (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*)"
  apply transfer
  by (simp add: Complex_Vector_Spaces0.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,  v = u, 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_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 cinner_adj_left:
  fixes G :: "'b::chilbert_space CL 'a::complex_inner"
  shows G* *V x, y = x, 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, G* *V y = G *V x, y
  apply transfer using cadjoint_univ_prop' by blast

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

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)
    apply intro_classes by simp
  from True have c2: class.not_singleton TYPE('c)
    apply intro_classes by 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
  apply (rule antilinearI) by (auto simp add: adj_plus)

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::chilbert_space
    and F:: 'a CL 'b
  assumes x y. (cblinfun_apply F) x, y = x, (cblinfun_apply G) y
  shows F = G*
  using assms apply transfer using cadjoint_eqI by auto

lemma cinner_real_hermiteanI:
  ― ‹Prop. II.2.12 in @{cite conway2013course}
  assumes ψ. cinner ψ (A *V ψ)  
  shows A = A*
proof -
  { fix g h :: 'a
    {
      fix α :: complex
      have cinner h (A h) + cnj α *C cinner g (A h) + α *C cinner h (A g) + (abs α)2 * cinner g (A g)
        = cinner (h + α *C g) (A *V (h + α *C g)) (is ?sum4 = _)
        apply (auto simp: cinner_add_right cinner_add_left cblinfun.add_right cblinfun.scaleC_right ring_class.ring_distribs)
        by (metis cnj_x_x mult.commute)
      also have   
        using assms by auto
      finally have ?sum4 = cnj ?sum4
        using Reals_cnj_iff by fastforce
      then have cnj α *C cinner g (A h) + α *C cinner h (A g)
            = α *C cinner (A h) g + cnj α *C cinner (A g) h
        using Reals_cnj_iff abs_complex_real assms by force
      also have  = α *C cinner h (A* *V g) + cnj α *C cinner g (A* *V h)
        by (simp add: cinner_adj_right)
      finally have cnj α *C cinner g (A h) + α *C cinner h (A g) = α *C cinner h (A* *V g) + cnj α *C cinner g (A* *V h)
        by -
    }
    from this[where α2=1] this[where α2=𝗂]
    have 1: cinner g (A h) + cinner h (A g) = cinner h (A* *V g) + cinner g (A* *V h)
      and i: - 𝗂 * cinner g (A h) + 𝗂 *C cinner h (A g) =  𝗂 *C cinner h (A* *V g) - 𝗂 *C cinner g (A* *V h)
      by auto
    from arg_cong2[OF 1 arg_cong[OF i, where f=(*) (-𝗂)], where f=plus]
    have cinner h (A g) = cinner h (A* *V g)
      by (auto simp: ring_class.ring_distribs)
  }
  then show "A = A*"
    by (simp add: adjoint_eqI cinner_adj_right)
qed


lemma norm_AAadj[simp]: norm (A oCL A*) = (norm A)2 for A :: 'a::chilbert_space CL 'b::{complex_inner}
proof (cases class.not_singleton TYPE('b))
  case True
  then have [simp]: class.not_singleton TYPE('b)
    by -
  have 1: (norm A)2 * ε  norm (A oCL A*) if ε < 1 and ε  0 for ε
  proof -
    obtain ψ where ψ: norm ((A*) *V ψ)  norm (A*) * sqrt ε and [simp]: norm ψ = 1
      apply atomize_elim
      apply (rule cblinfun_norm_approx_witness_mult[internalize_sort' 'a])
      using ε < 1 by (auto intro: complex_normed_vector_class.complex_normed_vector_axioms)
    have complex_of_real ((norm A)2 * ε) = (norm (A*) * sqrt ε)2
      by (simp add: ordered_field_class.sign_simps(23) that(2))
    also have   (norm ((A* *V ψ)))2
      apply (rule complex_of_real_mono)
      using ψ apply (rule power_mono)
      using ε  0 by auto
    also have   cinner (A* *V ψ) (A* *V ψ)
      by (auto simp flip: power2_norm_eq_cinner)
    also have  = cinner ψ (A *V A* *V ψ)
      by (simp add: cinner_adj_left)
    also have  = cinner ψ ((A oCL A*) *V ψ)
      by auto
    also have   norm (A oCL A*)
      using norm ψ = 1
      by (smt (verit, best) Im_complex_of_real Re_complex_of_real (A* *V ψ) C (A* *V ψ) = ψ C (A *V A* *V ψ) ψ C (A *V A* *V ψ) = ψ C ((A oCL A*) *V ψ) cdot_square_norm cinner_ge_zero cmod_Re complex_inner_class.Cauchy_Schwarz_ineq2 less_eq_complex_def mult_cancel_left1 mult_cancel_right1 norm_cblinfun)
    finally show ?thesis
      by (auto simp: less_eq_complex_def)
  qed
  then have 1: (norm A)2  norm (A oCL A*)
    by (metis field_le_mult_one_interval less_eq_real_def ordered_field_class.sign_simps(5))

  have 2: norm (A oCL A*)  (norm A)2
  proof (rule norm_cblinfun_bound)
    show 0  (norm A)2 by simp
    fix ψ
    have norm ((A oCL A*) *V ψ) = norm (A *V A* *V ψ)
      by auto
    also have   norm A * norm (A* *V ψ)
      by (simp add: norm_cblinfun)
    also have   norm A * norm (A*) * norm ψ
      by (metis mult.assoc norm_cblinfun norm_imp_pos_and_ge ordered_comm_semiring_class.comm_mult_left_mono)
    also have  = (norm A)2 * norm ψ
      by (simp add: power2_eq_square)
    finally show norm ((A oCL A*) *V ψ)  (norm A)2 * norm ψ
      by -
  qed

  from 1 2 show ?thesis by simp
next
  case False
  then have [simp]: class.CARD_1 TYPE('b)
    by (rule not_singleton_vs_CARD_1)
  have A = 0
    apply (rule cblinfun_to_CARD_1_0[internalize_sort' 'b])
    by (auto intro: complex_normed_vector_class.complex_normed_vector_axioms)
  then show ?thesis
    by auto
qed

subsection Unitaries / isometries


definition isometry::'a::chilbert_space CL 'b::complex_inner  bool where
  isometry U  U* oCL U = id_cblinfun

definition unitary::'a::chilbert_space CL 'b::complex_inner  bool where
  unitary U  (U* oCL U  = id_cblinfun)  (U oCL U* = id_cblinfun)

lemma unitary_twosided_isometry: "unitary U  isometry U  isometry (U*)"
  unfolding unitary_def isometry_def by simp

lemma isometryD[simp]: "isometry U  U* oCL U = id_cblinfun"
  unfolding isometry_def by simp

(* Not [simp] because isometryD[simp] + unitary_isometry[simp] already have the same effect *)
lemma unitaryD1: "unitary U  U* oCL U = id_cblinfun"
  unfolding unitary_def by simp

lemma unitaryD2[simp]: "unitary U  U oCL U* = id_cblinfun"
  unfolding unitary_def by simp

lemma unitary_isometry[simp]: "unitary U  isometry U"
  unfolding unitary_def isometry_def by simp

lemma unitary_adj[simp]: "unitary (U*) = unitary U"
  unfolding unitary_def by auto

lemma isometry_cblinfun_compose[simp]:
  assumes "isometry A" and "isometry B"
  shows "isometry (A oCL B)"
proof-
  have "B* oCL A* oCL (A oCL B) = id_cblinfun" if "A* oCL A = id_cblinfun" and "B* oCL B = id_cblinfun"
    using that
    by (smt (verit, del_insts) adjoint_eqI cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply)
  thus ?thesis
    using assms unfolding isometry_def by simp
qed

lemma unitary_cblinfun_compose[simp]: "unitary (A oCL B)"
  if "unitary A" and "unitary B"
  using that
  by (smt (z3) adj_cblinfun_compose cblinfun_compose_assoc cblinfun_compose_id_right double_adj isometryD isometry_cblinfun_compose unitary_def unitary_isometry)

lemma unitary_surj:
  assumes "unitary U"
  shows "surj (cblinfun_apply U)"
  apply (rule surjI[where f=cblinfun_apply (U*)])
  using assms unfolding unitary_def apply transfer
  using comp_eq_dest_lhs by force

lemma unitary_id[simp]: "unitary id_cblinfun"
  by (simp add: unitary_def)

lemma orthogonal_on_basis_is_isometry:
  assumes spanB: ccspan B = 
  assumes orthoU: b c. bB  cB  cinner (U *V b) (U *V c) = cinner b c
  shows isometry U
proof -
  have [simp]: b  closure (cspan B) for b
    using spanB apply transfer by simp
  have *: cinner (U* *V U *V ψ) φ = cinner ψ φ if ψB and φB for ψ φ
    by (simp add: cinner_adj_left orthoU that(1) that(2))
  have *: cinner (U* *V U *V ψ) φ = cinner ψ φ if ψB for ψ φ
    apply (rule bounded_clinear_eq_on[where t=φ and G=B])
    using bounded_clinear_cinner_right *[OF that]
    by auto
  have U* *V U *V φ = φ if φB for φ
    apply (rule cinner_extensionality)
    apply (subst cinner_eq_flip)
    by (simp add: * that)
  then have U* oCL U = id_cblinfun
    by (metis cblinfun_apply_cblinfun_compose cblinfun_eq_gen_eqI cblinfun_id_cblinfun_apply spanB)
  then show isometry U
    using isometry_def by blast
qed



subsection Images


(* Closure is necessary. See email 47a3bb3d-3cc3-0934-36eb-3ef0f7b70a85@ut.ee *)
lift_definition cblinfun_image :: 'a::complex_normed_vector CL 'b::complex_normed_vector
 'a ccsubspace  'b ccsubspace  (infixr "*S" 70)
  is "λA S. closure (A ` S)"
  using  bounded_clinear_def closed_closure  closed_csubspace.intro
  by (simp add: bounded_clinear_def complex_vector.linear_subspace_image closure_is_closed_csubspace)

lemma cblinfun_image_mono:
  assumes a1: "S  T"
  shows "A *S S  A *S T"
  using a1
  by (simp add: cblinfun_image.rep_eq closure_mono image_mono less_eq_ccsubspace.rep_eq)

lemma cblinfun_image_0[simp]:
  shows "U *S 0 = 0"
  thm zero_ccsubspace_def
  apply transfer
  by (simp add: bounded_clinear_def complex_vector.linear_0)

lemma cblinfun_image_bot[simp]: "U *S bot = bot"
  using cblinfun_image_0 by auto

lemma cblinfun_image_sup[simp]:
  fixes A B :: 'a::chilbert_space ccsubspace and U :: "'a CL'b::chilbert_space"
  shows U *S (sup A B) = sup (U *S A) (U *S B)
  apply transfer using bounded_clinear.bounded_linear closure_image_closed_sum by blast

lemma scaleC_cblinfun_image[simp]:
  fixes A :: 'a::chilbert_space CL 'b :: chilbert_space
    and S :: 'a ccsubspace and α :: complex
  shows (α *C A) *S S  = α *C (A *S S)
proof-
  have closure ( ( ((*C) α)  (cblinfun_apply A) ) ` space_as_set S) =
   ((*C) α) ` (closure (cblinfun_apply A ` space_as_set S))
    by (metis closure_scaleC image_comp)
  hence (closure (cblinfun_apply (α *C A) ` space_as_set S)) =
   ((*C) α) ` (closure (cblinfun_apply A ` space_as_set S))
    by (metis (mono_tags, lifting) comp_apply image_cong scaleC_cblinfun.rep_eq)
  hence Abs_clinear_space (closure (cblinfun_apply (α *C A) ` space_as_set S)) =
            α *C Abs_clinear_space (closure (cblinfun_apply A ` space_as_set S))
    by (metis space_as_set_inverse cblinfun_image.rep_eq scaleC_ccsubspace.rep_eq)
  have x1: "Abs_clinear_space (closure ((*V) (α *C A) ` space_as_set S)) =
            α *C Abs_clinear_space (closure ((*V) A ` space_as_set S))"
    using Abs_clinear_space (closure (cblinfun_apply (α *C A) ` space_as_set S)) =
            α *C Abs_clinear_space (closure (cblinfun_apply A ` space_as_set S))
    by blast
  show ?thesis
    unfolding cblinfun_image_def using x1 by force
qed

lemma cblinfun_image_id[simp]:
  "id_cblinfun *S ψ = ψ"
  apply transfer
  by (simp add: closed_csubspace.closed)

lemma cblinfun_compose_image:
  (A oCL B) *S S =  A *S (B *S S)
  apply transfer unfolding image_comp[symmetric]
  apply (rule closure_bounded_linear_image_subset_eq[symmetric])
  by (simp add: bounded_clinear.bounded_linear)

lemmas cblinfun_assoc_left = cblinfun_compose_assoc[symmetric] cblinfun_compose_image[symmetric]
  add.assoc[where ?'a="'a::chilbert_space CL 'b::chilbert_space", symmetric]
lemmas cblinfun_assoc_right = cblinfun_compose_assoc cblinfun_compose_image
  add.assoc[where ?'a="'a::chilbert_space CL 'b::chilbert_space"]

lemma cblinfun_image_INF_leq[simp]:
  fixes U :: "'b::complex_normed_vector CL 'c::cbanach"
    and V :: "'a  'b ccsubspace"
  shows U *S (INF i. V i)  (INF i. U *S (V i))
  apply transfer
  by (simp add: INT_greatest Inter_lower closure_mono image_mono)

lemma isometry_cblinfun_image_inf_distrib':
  fixes U::'a::complex_normed_vector CL 'b::cbanach and B C::"'a ccsubspace"
  shows "U *S (inf B C)  inf (U *S B) (U *S C)"
proof -
  define V where V b = (if b then B else C) for b
  have U *S (INF i. V i)  (INF i. U *S (V i))
    by auto
  then show ?thesis
    unfolding V_def
    by (metis (mono_tags, lifting) INF_UNIV_bool_expand)
qed

lemma cblinfun_image_eq:
  fixes S :: "'a::cbanach ccsubspace"
    and A B :: "'a::cbanach CL'b::cbanach"
  assumes "x. x  G  A *V x = B *V x" and "ccspan G  S"
  shows "A *S S = B *S S"
proof (use assms in transfer)
  fix G :: "'a set" and A :: "'a  'b" and B :: "'a  'b" and S :: "'a set"
  assume a1: "bounded_clinear A"
  assume a2: "bounded_clinear B"
  assume a3: "x. x  G  A x = B x"
  assume a4: "S  closure (cspan G)"

  have "A ` closure S = B ` closure S"
    by (smt (verit, best) UnCI a1 a2 a3 a4 bounded_clinear_eq_on closure_Un closure_closure image_cong sup.absorb_iff1)
  then show "closure (A ` S) = closure (B ` S)"
    by (metis Complex_Vector_Spaces0.bounded_clinear.bounded_linear a1 a2 closure_bounded_linear_image_subset_eq)
qed

lemma cblinfun_fixes_range:
  assumes "A oCL B = B" and "ψ  space_as_set (B *S top)"
  shows "A *V ψ = ψ"
proof-
  define rangeB rangeB' where "rangeB = space_as_set (B *S top)"
    and "rangeB' = range (cblinfun_apply B)"
  from assms have "ψ  closure rangeB'"
    by (simp add: cblinfun_image.rep_eq rangeB'_def top_ccsubspace.rep_eq)

  then obtain ψi where ψi_lim: "ψi  ψ" and ψi_B: "ψi i  rangeB'" for i
    using closure_sequential by blast
  have A_invariant: "A *V ψi i = ψi i"
    for i
  proof-
    from ψi_B obtain φ where φ: "ψi i = B *V φ"
      using rangeB'_def by blast
    hence "A *V ψi i = (A oCL B) *V φ"
      by (simp add: cblinfun_compose.rep_eq)
    also have " = B *V φ"
      by (simp add: assms)
    also have " = ψi i"
      by (simp add: φ)
    finally show ?thesis.
  qed
  from ψi_lim have "(λi. A *V (ψi i))  A *V ψ"
    by (rule isCont_tendsto_compose[rotated], simp)
  with A_invariant have "(λi. ψi i)  A *V ψ"
    by auto
  with ψi_lim show "A *V ψ = ψ"
    using LIMSEQ_unique by blast
qed

lemma zero_cblinfun_image[simp]: "0 *S S = (0::_ ccsubspace)"
  apply transfer by (simp add: complex_vector.subspace_0 image_constant[where x=0])

lemma cblinfun_image_INF_eq_general:
  fixes V :: "'a  'b::chilbert_space ccsubspace"
    and U :: "'b CL'c::chilbert_space"
    and Uinv :: "'c CL'b"
  assumes UinvUUinv: "Uinv oCL U oCL Uinv = Uinv" and UUinvU: "U oCL Uinv oCL U = U"
    ― ‹Meaning: termUinv is a Pseudoinverse of termU
    and V: "i. V i  Uinv *S top"
  shows "U *S (INF i. V i) = (INF i. U *S V i)"
proof (rule antisym)
  show "U *S (INF i. V i)  (INF i. U *S V i)"
    by (rule cblinfun_image_INF_leq)
next
  define rangeU rangeUinv where "rangeU = U *S top" and "rangeUinv = Uinv *S top"
  define INFUV INFV where INFUV_def: "INFUV = (INF i. U *S V i)" and INFV_def: "INFV = (INF i. V i)"
  from assms have "V i  rangeUinv"
    for i
    unfolding rangeUinv_def by simp
  moreover have "(Uinv oCL U) *V ψ = ψ" if "ψ  space_as_set rangeUinv"
    for ψ
    using UinvUUinv cblinfun_fixes_range rangeUinv_def that by fastforce
  ultimately have "(Uinv oCL U) *V ψ = ψ" if "ψ  space_as_set (V i)"
    for ψ i
    using less_eq_ccsubspace.rep_eq that by blast
  hence d1: "(Uinv oCL U) *S (V i) = (V i)" for i
  proof transfer
    show "closure ((Uinv  U) ` V i) = V i"
      if "pred_fun  closed_csubspace V"
        and "bounded_clinear Uinv"
        and "bounded_clinear U"
        and "ψ i. ψ  V i  (Uinv  U) ψ = ψ"
      for V :: "'a  'b set"
        and Uinv :: "'c  'b"
        and U :: "'b  'c"
        and i :: 'a
      using that proof auto
      show "x  V i"
        if "x. closed_csubspace (V x)"
          and "bounded_clinear Uinv"
          and "bounded_clinear U"
          and "ψ i. ψ  V i  Uinv (U ψ) = ψ"
          and "x  closure (V i)"
        for x :: 'b
        using that
        by (metis orthogonal_complement_of_closure closed_csubspace.subspace double_orthogonal_complement_id closure_is_closed_csubspace)
      show "x  closure (V i)"
        if "x. closed_csubspace (V x)"
          and "bounded_clinear Uinv"
          and "bounded_clinear U"
          and "ψ i. ψ  V i  Uinv (U ψ) = ψ"
          and "x  V i"
        for x :: 'b
        using that
        using setdist_eq_0_sing_1 setdist_sing_in_set
        by blast
    qed
  qed
  have "U *S V i  rangeU" for i
    by (simp add: cblinfun_image_mono rangeU_def)
  hence "INFUV  rangeU"
    unfolding INFUV_def by (meson INF_lower UNIV_I order_trans)
  moreover have "(U oCL Uinv) *V ψ = ψ" if "ψ  space_as_set rangeU" for ψ
    using UUinvU cblinfun_fixes_range rangeU_def that by fastforce
  ultimately have x: "(U oCL Uinv) *V ψ = ψ" if "ψ  space_as_set INFUV" for ψ
    by (simp add: in_mono less_eq_ccsubspace.rep_eq that)

  have "closure ((U  Uinv) ` INFUV) = INFUV"
    if "closed_csubspace INFUV"
      and "bounded_clinear U"
      and "bounded_clinear Uinv"
      and "ψ. ψ  INFUV  (U  Uinv) ψ = ψ"
    for INFUV :: "'c set"
      and U :: "'b  'c"
      and Uinv :: "'c  'b"
    using that proof auto
    show "x  INFUV"
      if "closed_csubspace INFUV"
        and "bounded_clinear U"
        and "bounded_clinear Uinv"
        and "ψ. ψ  INFUV  U (Uinv ψ) = ψ"
        and "x  closure INFUV"
      for x :: 'c
      using that
      by (metis orthogonal_complement_of_closure closed_csubspace.subspace double_orthogonal_complement_id closure_is_closed_csubspace)
    show "x  closure INFUV"
      if "closed_csubspace INFUV"
        and "bounded_clinear U"
        and "bounded_clinear Uinv"
        and "ψ. ψ  INFUV  U (Uinv ψ) = ψ"
        and "x  INFUV"
      for x :: 'c
      using that
      using setdist_eq_0_sing_1 setdist_sing_in_set
      by (simp add: closed_csubspace.closed)
  qed
  hence "(U oCL Uinv) *S INFUV = INFUV"
    by (metis (mono_tags, opaque_lifting) x cblinfun_image.rep_eq cblinfun_image_id id_cblinfun_apply image_cong
        space_as_set_inject)
  hence "INFUV = U *S Uinv *S INFUV"
    by (simp add: cblinfun_compose_image)
  also have "  U *S (INF i. Uinv *S U *S V i)"
    unfolding INFUV_def
    by (metis cblinfun_image_mono cblinfun_image_INF_leq)
  also have " = U *S INFV"
    using d1
    by (metis (no_types, lifting) INFV_def cblinfun_assoc_left(2) image_cong)
  finally show "INFUV  U *S INFV".
qed

lemma unitary_range[simp]:
  assumes "unitary U"
  shows "U *S top = top"
  using assms unfolding unitary_def apply transfer
  by (metis closure_UNIV comp_apply surj_def)

lemma range_adjoint_isometry:
  assumes "isometry U"
  shows "U* *S top = top"
proof-
  from assms have "top = U* *S U *S top"
    by (simp add: cblinfun_assoc_left(2))
  also have "  U* *S top"
    by (simp add: cblinfun_image_mono)
  finally show ?thesis
    using top.extremum_unique by blast
qed

lemma cblinfun_image_INF_eq[simp]:
  fixes V :: "'a  'b::chilbert_space ccsubspace"
    and U :: "'b CL 'c::chilbert_space"
  assumes isometry U
  shows "U *S (INF i. V i) = (INF i. U *S V i)"
proof -
  from isometry U have "U* oCL U oCL U* = U*"
    unfolding isometry_def by simp
  moreover from isometry U have "U oCL U* oCL U = U"
    unfolding isometry_def
    by (