Theory Complex_L2

section Complex_L2› -- Hilbert space of square-summable functions

(*
Authors:

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

*)

theory Complex_L2
  imports 
    Complex_Bounded_Linear_Function

    "HOL-Analysis.L2_Norm"
    "HOL-Library.Rewrite"
    "HOL-Analysis.Infinite_Sum"
begin

unbundle lattice_syntax
unbundle cblinfun_notation
unbundle no_notation_blinfun_apply

subsection l2 norm of functions

definition "has_ell2_norm (x::_complex)  (λi. (x i)2) abs_summable_on UNIV"

lemma has_ell2_norm_bdd_above: has_ell2_norm x  bdd_above (sum (λxa. norm ((x xa)2)) ` Collect finite)
  by (simp add: has_ell2_norm_def abs_summable_iff_bdd_above)

lemma has_ell2_norm_L2_set: "has_ell2_norm x = bdd_above (L2_set (norm o x) ` Collect finite)"
proof (rule iffI)
  have mono sqrt
    using monoI real_sqrt_le_mono by blast
  assume has_ell2_norm x
  then have *: bdd_above (sum (λxa. norm ((x xa)2)) ` Collect finite)
    by (subst (asm) has_ell2_norm_bdd_above)
  have bdd_above ((λF. sqrt (sum (λxa. norm ((x xa)2)) F)) ` Collect finite)
    using bdd_above_image_mono[OF mono sqrt *]
    by (auto simp: image_image)
  then show bdd_above (L2_set (norm o x) ` Collect finite)
    by (auto simp: L2_set_def norm_power)
next
  define p2 where p2 x = (if x < 0 then 0 else x^2) for x :: real
  have mono p2
    by (simp add: monoI p2_def)
  have [simp]: p2 (L2_set f F) = (iF. (f i)2) for f and F :: 'a set
    by (smt (verit) L2_set_def L2_set_nonneg p2_def power2_less_0 real_sqrt_pow2 sum.cong sum_nonneg)
  assume *: bdd_above (L2_set (norm o x) ` Collect finite)
  have bdd_above (p2 ` L2_set (norm o x) ` Collect finite)
    using bdd_above_image_mono[OF mono p2 *]
    by auto
  then show has_ell2_norm x
    apply (simp add: image_image has_ell2_norm_def abs_summable_iff_bdd_above)
    by (simp add: norm_power)
qed

definition ell2_norm :: ('a  complex)  real where ell2_norm x = sqrt (i. norm (x i)^2)

lemma ell2_norm_SUP:
  assumes has_ell2_norm x
  shows "ell2_norm x = sqrt (SUP F{F. finite F}. sum (λi. norm (x i)^2) F)"
  using assms apply (auto simp add: ell2_norm_def has_ell2_norm_def)
  apply (subst infsum_nonneg_is_SUPREMUM_real)
  by (auto simp: norm_power)

lemma ell2_norm_L2_set: 
  assumes "has_ell2_norm x"
  shows "ell2_norm x = (SUP F{F. finite F}. L2_set (norm o x) F)"
proof-
  have "sqrt ( (sum (λi. (cmod (x i))2) ` Collect finite)) =
      (SUP F{F. finite F}. sqrt (iF. (cmod (x i))2))"
  proof (subst continuous_at_Sup_mono)
    show "mono sqrt"
      by (simp add: mono_def)      
    show "continuous (at_left ( (sum (λi. (cmod (x i))2) ` Collect finite))) sqrt"
      using continuous_at_split isCont_real_sqrt by blast    
    show "sum (λi. (cmod (x i))2) ` Collect finite  {}"
      by auto      
    show "bdd_above (sum (λi. (cmod (x i))2) ` Collect finite)"
      using has_ell2_norm_bdd_above[THEN iffD1, OF assms] by (auto simp: norm_power)
    show " (sqrt ` sum (λi. (cmod (x i))2) ` Collect finite) = (SUP FCollect finite. sqrt (iF. (cmod (x i))2))"
      by (metis image_image)      
  qed  
  thus ?thesis 
    using assms by (auto simp: ell2_norm_SUP L2_set_def)
qed

lemma has_ell2_norm_finite[simp]: "has_ell2_norm (x::'a::finite_)"
  unfolding has_ell2_norm_def by simp

lemma ell2_norm_finite: 
  "ell2_norm (x::'a::finitecomplex) = sqrt (sum (λi. (norm(x i))^2) UNIV)"
  by (simp add: ell2_norm_def)

lemma ell2_norm_finite_L2_set: "ell2_norm (x::'a::finitecomplex) = L2_set (norm o x) UNIV"
  by (simp add: ell2_norm_finite L2_set_def)

lemma ell2_ket:
  fixes a
  defines f  (λi. if a = i then 1 else 0)
  shows has_ell2_norm_ket: has_ell2_norm f
    and ell2_norm_ket: ell2_norm f = 1
proof -
  have (λx. (f x)2) abs_summable_on {a}
    apply (rule summable_on_finite) by simp
  then show has_ell2_norm f
    unfolding has_ell2_norm_def
    apply (rule summable_on_cong_neutral[THEN iffD1, rotated -1])
    unfolding f_def by auto

  have (x{a}. (f x)2) = 1
    apply (subst infsum_finite)
    by (auto simp: f_def)
  then show ell2_norm f = 1
    unfolding ell2_norm_def
    apply (subst infsum_cong_neutral[where T={a} and g=λx. (cmod (f x))2])
    by (auto simp: f_def)
qed

lemma ell2_norm_geq0: ell2_norm x  0
  by (auto simp: ell2_norm_def intro!: infsum_nonneg)

lemma ell2_norm_point_bound:
  assumes has_ell2_norm x
  shows ell2_norm x  cmod (x i)
proof -
  have (cmod (x i))2 = norm ((x i)2)
    by (simp add: norm_power)
  also have norm ((x i)2) = sum (λi. (norm ((x i)2))) {i}
    by auto
  also have  = infsum (λi. (norm ((x i)2))) {i}
    by (rule infsum_finite[symmetric], simp)
  also have   infsum (λi. (norm ((x i)2))) UNIV
    apply (rule infsum_mono_neutral)
    using assms by (auto simp: has_ell2_norm_def)
  also have  = (ell2_norm x)2
    by (metis (no_types, lifting) ell2_norm_def ell2_norm_geq0 infsum_cong norm_power real_sqrt_eq_iff real_sqrt_unique)
  finally show ?thesis
    using ell2_norm_geq0 power2_le_imp_le by blast
qed

lemma ell2_norm_0:
  assumes "has_ell2_norm x"
  shows "(ell2_norm x = 0) = (x = (λ_. 0))"
proof
  assume u1: "x = (λ_. 0)"
  have u2: "(SUP x::'a setCollect finite. (0::real)) = 0"
    if "x = (λ_. 0)"
    by (metis cSUP_const empty_Collect_eq finite.emptyI)
  show "ell2_norm x = 0"
    unfolding ell2_norm_def
    using u1 u2 by auto 
next
  assume norm0: "ell2_norm x = 0"
  show "x = (λ_. 0)"
  proof
    fix i
    have cmod (x i)  ell2_norm x
      using assms by (rule ell2_norm_point_bound)
    also have  = 0
      by (fact norm0)
    finally show "x i = 0" by auto
  qed
qed


lemma ell2_norm_smult:
  assumes "has_ell2_norm x"
  shows "has_ell2_norm (λi. c * x i)" and "ell2_norm (λi. c * x i) = cmod c * ell2_norm x"
proof -
  have L2_set_mul: "L2_set (cmod  (λi. c * x i)) F = cmod c * L2_set (cmod  x) F" for F
  proof-
    have "L2_set (cmod  (λi. c * x i)) F = L2_set (λi. (cmod c * (cmod o x) i)) F"
      by (metis comp_def norm_mult)
    also have " = cmod c * L2_set (cmod o x) F"
      by (metis norm_ge_zero L2_set_right_distrib)
    finally show ?thesis .
  qed

  from assms obtain M where M: "M  L2_set (cmod o x) F" if "finite F" for F
    unfolding has_ell2_norm_L2_set bdd_above_def by auto
  hence "cmod c * M  L2_set (cmod o (λi. c * x i)) F" if "finite F" for F
    unfolding L2_set_mul
    by (simp add: ordered_comm_semiring_class.comm_mult_left_mono that) 
  thus has: "has_ell2_norm (λi. c * x i)"
    unfolding has_ell2_norm_L2_set bdd_above_def using L2_set_mul[symmetric] by auto
  have "ell2_norm (λi. c * x i) = (SUP F  Collect finite. (L2_set (cmod  (λi. c * x i)) F))"
    by (simp add: ell2_norm_L2_set has)
  also have " = (SUP F  Collect finite. (cmod c * L2_set (cmod  x) F))"
    using L2_set_mul by auto   
  also have " = cmod c * ell2_norm x" 
  proof (subst ell2_norm_L2_set)
    show "has_ell2_norm x"
      by (simp add: assms)      
    show "(SUP FCollect finite. cmod c * L2_set (cmod  x) F) = cmod c *  (L2_set (cmod  x) ` Collect finite)"
    proof (subst continuous_at_Sup_mono [where f = "λx. cmod c * x"])
      show "mono ((*) (cmod c))"
        by (simp add: mono_def ordered_comm_semiring_class.comm_mult_left_mono)
      show "continuous (at_left ( (L2_set (cmod  x) ` Collect finite))) ((*) (cmod c))"
      proof (rule continuous_mult)
        show "continuous (at_left ( (L2_set (cmod  x) ` Collect finite))) (λx. cmod c)"
          by simp
        show "continuous (at_left ( (L2_set (cmod  x) ` Collect finite))) (λx. x)"
          by simp
      qed    
      show "L2_set (cmod  x) ` Collect finite  {}"
        by auto        
      show "bdd_above (L2_set (cmod  x) ` Collect finite)"
        by (meson assms has_ell2_norm_L2_set)        
      show "(SUP FCollect finite. cmod c * L2_set (cmod  x) F) =  ((*) (cmod c) ` L2_set (cmod  x) ` Collect finite)"
        by (metis image_image)        
    qed   
  qed     
  finally show "ell2_norm (λi. c * x i) = cmod c * ell2_norm x".
qed


lemma ell2_norm_triangle:
  assumes "has_ell2_norm x" and "has_ell2_norm y"
  shows "has_ell2_norm (λi. x i + y i)" and "ell2_norm (λi. x i + y i)  ell2_norm x + ell2_norm y"
proof -
  have triangle: "L2_set (cmod  (λi. x i + y i)) F  L2_set (cmod  x) F + L2_set (cmod  y) F" 
    (is "?lhs?rhs") 
    if "finite F" for F
  proof -
    have "?lhs  L2_set (λi. (cmod o x) i + (cmod o y) i) F"
    proof (rule L2_set_mono)
      show "(cmod  (λi. x i + y i)) i  (cmod  x) i + (cmod  y) i"
        if "i  F"
        for i :: 'a
        using that norm_triangle_ineq by auto 
      show "0  (cmod  (λi. x i + y i)) i"
        if "i  F"
        for i :: 'a
        using that
        by simp 
    qed
    also have "  ?rhs"
      by (rule L2_set_triangle_ineq)
    finally show ?thesis .
  qed
  obtain Mx My where Mx: "Mx  L2_set (cmod o x) F" and My: "My  L2_set (cmod o y) F" 
    if "finite F" for F
    using assms unfolding has_ell2_norm_L2_set bdd_above_def by auto
  hence MxMy: "Mx + My  L2_set (cmod  x) F + L2_set (cmod  y) F" if "finite F" for F
    using that by fastforce
  hence bdd_plus: "bdd_above ((λxa. L2_set (cmod  x) xa + L2_set (cmod  y) xa) ` Collect finite)"
    unfolding bdd_above_def by auto
  from MxMy have MxMy': "Mx + My  L2_set (cmod  (λi. x i + y i)) F" if "finite F" for F 
    using triangle that by fastforce
  thus has: "has_ell2_norm (λi. x i + y i)"
    unfolding has_ell2_norm_L2_set bdd_above_def by auto
  have SUP_plus: "(SUP xA. f x + g x)  (SUP xA. f x) + (SUP xA. g x)" 
    if notempty: "A{}" and bddf: "bdd_above (f`A)"and bddg: "bdd_above (g`A)"
    for f g :: "'a set  real" and A
  proof-
    have xleq: "x  (SUP xA. f x) + (SUP xA. g x)" if x: "x  (λx. f x + g x) ` A" for x
    proof -
      obtain a where aA: "a:A" and ax: "x = f a + g a"
        using x by blast
      have fa: "f a  (SUP xA. f x)"
        by (simp add: bddf aA cSUP_upper)
      moreover have "g a  (SUP xA. g x)"
        by (simp add: bddg aA cSUP_upper)
      ultimately have "f a + g a  (SUP xA. f x) + (SUP xA. g x)" by simp
      with ax show ?thesis by simp
    qed
    have "(λx. f x + g x) ` A  {}"
      using notempty by auto        
    moreover have "x   (f ` A) +  (g ` A)"
      if "x  (λx. f x + g x) ` A"
      for x :: real
      using that
      by (simp add: xleq) 
    ultimately show ?thesis
      by (meson bdd_above_def cSup_le_iff)      
  qed
  have a2: "bdd_above (L2_set (cmod  x) ` Collect finite)"
    by (meson assms(1) has_ell2_norm_L2_set)    
  have a3: "bdd_above (L2_set (cmod  y) ` Collect finite)"
    by (meson assms(2) has_ell2_norm_L2_set)    
  have a1: "Collect finite  {}"
    by auto    
  have a4: " (L2_set (cmod  (λi. x i + y i)) ` Collect finite)
     (SUP xaCollect finite.
           L2_set (cmod  x) xa + L2_set (cmod  y) xa)"
    by (metis (mono_tags, lifting) a1 bdd_plus cSUP_mono mem_Collect_eq triangle)    
  have "r.  (L2_set (cmod  (λa. x a + y a)) ` Collect finite)  r  ¬ (SUP ACollect finite. L2_set (cmod  x) A + L2_set (cmod  y) A)  r"
    using a4 by linarith
  hence " (L2_set (cmod  (λi. x i + y i)) ` Collect finite)
      (L2_set (cmod  x) ` Collect finite) +
        (L2_set (cmod  y) ` Collect finite)"
    by (metis (no_types) SUP_plus a1 a2 a3)
  hence " (L2_set (cmod  (λi. x i + y i)) ` Collect finite)  ell2_norm x + ell2_norm y"
    by (simp add: assms(1) assms(2) ell2_norm_L2_set)
  thus "ell2_norm (λi. x i + y i)  ell2_norm x + ell2_norm y"
    by (simp add: ell2_norm_L2_set has)  
qed

lemma ell2_norm_uminus:
  assumes "has_ell2_norm x"
  shows has_ell2_norm (λi. - x i) and ell2_norm (λi. - x i) = ell2_norm x
  using assms by (auto simp: has_ell2_norm_def ell2_norm_def)

subsection The type ell2› of square-summable functions

typedef 'a ell2 = "{x::'acomplex. has_ell2_norm x}"
  unfolding has_ell2_norm_def by (rule exI[of _ "λ_.0"], auto)
setup_lifting type_definition_ell2

instantiation ell2 :: (type)complex_vector begin
lift_definition zero_ell2 :: "'a ell2" is "λ_. 0" by (auto simp: has_ell2_norm_def)
lift_definition uminus_ell2 :: "'a ell2  'a ell2" is uminus by (simp add: has_ell2_norm_def)
lift_definition plus_ell2 :: "'a ell2  'a ell2  'a ell2" is "λf g x. f x + g x"
  by (rule ell2_norm_triangle) 
lift_definition minus_ell2 :: "'a ell2  'a ell2  'a ell2" is "λf g x. f x - g x"
  apply (subst add_uminus_conv_diff[symmetric])
  apply (rule ell2_norm_triangle)
  by (auto simp add: ell2_norm_uminus)
lift_definition scaleR_ell2 :: "real  'a ell2  'a ell2" is "λr f x. complex_of_real r * f x"
  by (rule ell2_norm_smult)
lift_definition scaleC_ell2 :: "complex  'a ell2  'a ell2" is "λc f x. c * f x"
  by (rule ell2_norm_smult)

instance
proof
  fix a b c :: "'a ell2"

  show "((*R) r::'a ell2  _) = (*C) (complex_of_real r)" for r
    apply (rule ext) apply transfer by auto
  show "a + b + c = a + (b + c)"
    by (transfer; rule ext; simp)
  show "a + b = b + a"
    by (transfer; rule ext; simp)
  show "0 + a = a"
    by (transfer; rule ext; simp)
  show "- a + a = 0"
    by (transfer; rule ext; simp)
  show "a - b = a + - b"
    by (transfer; rule ext; simp)
  show "r *C (a + b) = r *C a + r *C b" for r
    apply (transfer; rule ext)
    by (simp add: vector_space_over_itself.scale_right_distrib)
  show "(r + r') *C a = r *C a + r' *C a" for r r'
    apply (transfer; rule ext)
    by (simp add: ring_class.ring_distribs(2)) 
  show "r *C r' *C a = (r * r') *C a" for r r'
    by (transfer; rule ext; simp)
  show "1 *C a = a"
    by (transfer; rule ext; simp)
qed
end

instantiation ell2 :: (type)complex_normed_vector begin
lift_definition norm_ell2 :: "'a ell2  real" is ell2_norm .
declare norm_ell2_def[code del]
definition "dist x y = norm (x - y)" for x y::"'a ell2"
definition "sgn x = x /R norm x" for x::"'a ell2"
definition [code del]: "uniformity = (INF e{0<..}. principal {(x::'a ell2, y). norm (x - y) < e})"
definition [code del]: "open U = (xU. F (x', y) in INF e{0<..}. principal {(x, y). norm (x - y) < e}. x' = x  y  U)" for U :: "'a ell2 set"
instance
proof
  fix a b :: "'a ell2"
  show "dist a b = norm (a - b)"
    by (simp add: dist_ell2_def)    
  show "sgn a = a /R norm a"
    by (simp add: sgn_ell2_def)    
  show "uniformity = (INF e{0<..}. principal {(x, y). dist (x::'a ell2) y < e})"
    unfolding dist_ell2_def  uniformity_ell2_def by simp
  show "open U = (xU. F (x', y) in uniformity. (x'::'a ell2) = x  y  U)" for U :: "'a ell2 set"
    unfolding uniformity_ell2_def open_ell2_def by simp_all        
  show "(norm a = 0) = (a = 0)"
    apply transfer by (fact ell2_norm_0)    
  show "norm (a + b)  norm a + norm b"
    apply transfer by (fact ell2_norm_triangle)
  show "norm (r *R (a::'a ell2)) = ¦r¦ * norm a" for r
    and a :: "'a ell2"
    apply transfer
    by (simp add: ell2_norm_smult(2)) 
  show "norm (r *C a) = cmod r * norm a" for r
    apply transfer
    by (simp add: ell2_norm_smult(2)) 
qed  
end

lemma norm_point_bound_ell2: "norm (Rep_ell2 x i)  norm x"
  apply transfer
  by (simp add: ell2_norm_point_bound)

lemma ell2_norm_finite_support:
  assumes finite S  i. i  S  Rep_ell2 x i = 0
  shows norm x = sqrt ((sum (λi. (cmod (Rep_ell2 x i))2)) S)
proof (insert assms(2), transfer fixing: S)
  fix x :: 'a  complex
  assume zero: i. i  S  x i = 0
  have ell2_norm x = sqrt (i. (cmod (x i))2)
    by (auto simp: ell2_norm_def)
  also have  = sqrt (iS. (cmod (x i))2)
    apply (subst infsum_cong_neutral[where g=λi. (cmod (x i))2 and S=UNIV and T=S])
    using zero by auto
  also have  = sqrt (iS. (cmod (x i))2)
    using finite S by simp
  finally show ell2_norm x = sqrt (iS. (cmod (x i))2)
    by -
qed

instantiation ell2 :: (type) complex_inner begin
lift_definition cinner_ell2 :: "'a ell2  'a ell2  complex" is 
  "λx y. infsum (λi. (cnj (x i) * y i)) UNIV" .
declare cinner_ell2_def[code del]

instance
proof standard
  fix x y z :: "'a ell2" fix c :: complex
  show "cinner x y = cnj (cinner y x)"
  proof transfer
    fix x y :: "'acomplex" assume "has_ell2_norm x" and "has_ell2_norm y"
    have "(i. cnj (x i) * y i) = (i. cnj (cnj (y i) * x i))"
      by (metis complex_cnj_cnj complex_cnj_mult mult.commute)
    also have " = cnj (i. cnj (y i) * x i)"
      by (metis infsum_cnj) 
    finally show "(i. cnj (x i) * y i) = cnj (i. cnj (y i) * x i)" .
  qed

  show "cinner (x + y) z = cinner x z + cinner y z"
  proof transfer
    fix x y z :: "'a  complex"
    assume "has_ell2_norm x"
    hence cnj_x: "(λi. cnj (x i) * cnj (x i)) abs_summable_on UNIV"
      by (simp del: complex_cnj_mult add: norm_mult[symmetric] complex_cnj_mult[symmetric] has_ell2_norm_def power2_eq_square)
    assume "has_ell2_norm y"
    hence cnj_y: "(λi. cnj (y i) * cnj (y i)) abs_summable_on UNIV"
      by (simp del: complex_cnj_mult add: norm_mult[symmetric] complex_cnj_mult[symmetric] has_ell2_norm_def power2_eq_square)
    assume "has_ell2_norm z"
    hence z: "(λi. z i * z i) abs_summable_on UNIV" 
      by (simp add: norm_mult[symmetric] has_ell2_norm_def power2_eq_square)
    have cnj_x_z:"(λi. cnj (x i) * z i) abs_summable_on UNIV"
      using cnj_x z by (rule abs_summable_product) 
    have cnj_y_z:"(λi. cnj (y i) * z i) abs_summable_on UNIV"
      using cnj_y z by (rule abs_summable_product) 
    show "(i. cnj (x i + y i) * z i) = (i. cnj (x i) * z i) + (i. cnj (y i) * z i)"
      apply (subst infsum_add [symmetric])
      using cnj_x_z cnj_y_z 
      by (auto simp add: summable_on_iff_abs_summable_on_complex distrib_left mult.commute)
  qed

  show "cinner (c *C x) y = cnj c * cinner x y"
  proof transfer
    fix x y :: "'a  complex" and c :: complex
    assume "has_ell2_norm x"
    hence cnj_x: "(λi. cnj (x i) * cnj (x i)) abs_summable_on UNIV"
      by (simp del: complex_cnj_mult add: norm_mult[symmetric] complex_cnj_mult[symmetric] has_ell2_norm_def power2_eq_square)
    assume "has_ell2_norm y"
    hence y: "(λi. y i * y i) abs_summable_on UNIV" 
      by (simp add: norm_mult[symmetric] has_ell2_norm_def power2_eq_square)
    have cnj_x_y:"(λi. cnj (x i) * y i) abs_summable_on UNIV"
      using cnj_x y by (rule abs_summable_product) 
    thus "(i. cnj (c * x i) * y i) = cnj c * (i. cnj (x i) * y i)"
      by (auto simp flip: infsum_cmult_right simp add: abs_summable_summable mult.commute vector_space_over_itself.scale_left_commute)
  qed

  show "0  cinner x x"
  proof transfer
    fix x :: "'a  complex"
    assume "has_ell2_norm x"
    hence "(λi. cmod (cnj (x i) * x i)) abs_summable_on UNIV"
      by (simp add: norm_mult has_ell2_norm_def power2_eq_square)
    hence "(λi. cnj (x i) * x i) abs_summable_on UNIV"
      by auto
    hence sum: "(λi. cnj (x i) * x i) abs_summable_on UNIV"
      unfolding has_ell2_norm_def power2_eq_square.
    have "0 = (i::'a. 0)" by auto
    also have "  (i. cnj (x i) * x i)"
      apply (rule infsum_mono_complex)
      by (auto simp add: abs_summable_summable sum)
    finally show "0  (i. cnj (x i) * x i)" by assumption
  qed

  show "(cinner x x = 0) = (x = 0)"
  proof (transfer, auto)
    fix x :: "'a  complex"
    assume "has_ell2_norm x"
    hence "(λi::'a. cmod (cnj (x i) * x i)) abs_summable_on UNIV"
      by (smt (verit, del_insts) complex_mod_mult_cnj has_ell2_norm_def mult.commute norm_ge_zero norm_power real_norm_def summable_on_cong)
    hence cmod_x2: "(λi. cnj (x i) * x i) abs_summable_on UNIV"
      unfolding has_ell2_norm_def power2_eq_square
      by simp
    assume eq0: "(i. cnj (x i) * x i) = 0"
    show "x = (λ_. 0)"
    proof (rule ccontr)
      assume "x  (λ_. 0)"
      then obtain i where "x i  0" by auto
      hence "0 < cnj (x i) * x i"
        by (metis le_less cnj_x_x_geq0 complex_cnj_zero_iff vector_space_over_itself.scale_eq_0_iff)
      also have " = (i{i}. cnj (x i) * x i)" by auto
      also have "  (i. cnj (x i) * x i)"
        apply (rule infsum_mono_neutral_complex)
        by (auto simp add: abs_summable_summable cmod_x2)
      also from eq0 have " = 0" by assumption
      finally show False by simp
    qed
  qed

  show "norm x = sqrt (cmod (cinner x x))"
  proof transfer 
    fix x :: "'a  complex" 
    assume x: "has_ell2_norm x"
    have "(λi::'a. cmod (x i) * cmod (x i)) abs_summable_on UNIV 
    (λi::'a. cmod (cnj (x i) * x i)) abs_summable_on UNIV"
      by (simp add: norm_mult has_ell2_norm_def power2_eq_square)
    hence sum: "(λi. cnj (x i) * x i) abs_summable_on UNIV"
      by (metis (no_types, lifting) complex_mod_mult_cnj has_ell2_norm_def mult.commute norm_power summable_on_cong x)
    from x have "ell2_norm x = sqrt (i. (cmod (x i))2)"
      unfolding ell2_norm_def by simp
    also have " = sqrt (i. cmod (cnj (x i) * x i))"
      unfolding norm_complex_def power2_eq_square by auto
    also have " = sqrt (cmod (i. cnj (x i) * x i))"
      by (auto simp: infsum_cmod abs_summable_summable sum)
    finally show "ell2_norm x = sqrt (cmod (i. cnj (x i) * x i))" by assumption
  qed
qed
end

instance ell2 :: (type) chilbert_space
proof
  fix X :: nat  'a ell2
  define x where x n a = Rep_ell2 (X n) a for n a
  have [simp]: has_ell2_norm (x n) for n
    using Rep_ell2 x_def[abs_def] by simp

  assume Cauchy X
  moreover have "dist (x n a) (x m a)  dist (X n) (X m)" for n m a
    by (metis Rep_ell2 x_def dist_norm ell2_norm_point_bound mem_Collect_eq minus_ell2.rep_eq norm_ell2.rep_eq)
  ultimately have Cauchy (λn. x n a) for a
    by (meson Cauchy_def le_less_trans)
  then obtain l where x_lim: (λn. x n a)  l a for a
    apply atomize_elim apply (rule choice)
    by (simp add: convergent_eq_Cauchy)
  define L where L = Abs_ell2 l
  define normF where normF F x = L2_set (cmod  x) F for F :: 'a set and x
  have normF_triangle: normF F (λa. x a + y a)  normF F x + normF F y if finite F for F x y
  proof -
    have normF F (λa. x a + y a) = L2_set (λa. cmod (x a + y a)) F
      by (metis (mono_tags, lifting) L2_set_cong comp_apply normF_def)
    also have   L2_set (λa. cmod (x a) + cmod (y a)) F
      by (meson L2_set_mono norm_ge_zero norm_triangle_ineq)
    also have   L2_set (λa. cmod (x a)) F + L2_set (λa. cmod (y a)) F
      by (simp add: L2_set_triangle_ineq)
    also have   normF F x + normF F y
      by (smt (verit, best) L2_set_cong normF_def comp_apply)
    finally show ?thesis
      by -
  qed
  have normF_negate: normF F (λa. - x a) = normF F x if finite F for F x
    unfolding normF_def o_def by simp
  have normF_ell2norm: normF F x  ell2_norm x if finite F and has_ell2_norm x for F x
    apply (auto intro!: cSUP_upper2[where x=F] simp: that normF_def ell2_norm_L2_set)
    by (meson has_ell2_norm_L2_set that(2))

  note Lim_bounded2[rotated, rule_format, trans]

  from Cauchy X
  obtain I where cauchyX: norm (X n - X m)  ε if ε>0 nI ε mI ε for ε n m
    by (metis Cauchy_def dist_norm less_eq_real_def)
  have normF_xx: normF F (λa. x n a - x m a)  ε if finite F ε>0 nI ε mI ε for ε n m F
    apply (subst asm_rl[of (λa. x n a - x m a) = Rep_ell2 (X n - X m)])
     apply (simp add: x_def minus_ell2.rep_eq)
    using that cauchyX by (metis Rep_ell2 mem_Collect_eq normF_ell2norm norm_ell2.rep_eq order_trans)
  have normF_xl_lim: (λm. normF F (λa. x m a - l a))  0 if finite F for F
  proof -
    have (λxa. cmod (x xa m - l m))  0 for m
      using x_lim by (simp add: LIM_zero_iff tendsto_norm_zero)
    then have (λm. iF. ((cmod  (λa. x m a - l a)) i)2)  0
      by (auto intro: tendsto_null_sum)
    then show ?thesis
      unfolding normF_def L2_set_def
      using tendsto_real_sqrt by force
  qed
  have normF_xl: normF F (λa. x n a - l a)  ε
    if n  I ε and ε > 0 and finite F for n ε F
  proof -
    have normF F (λa. x n a - l a) - ε  normF F (λa. x n a - x m a) + normF F (λa. x m a - l a) - ε for m
      using normF_triangle[OF finite F, where x=(λa. x n a - x m a) and y=(λa. x m a - l a)]
      by auto
    also have  m  normF F (λa. x m a - l a) if m  I ε for m
      using normF_xx[OF finite F ε>0 n  I ε m  I ε]
      by auto
    also have (λm.  m)  0
      using finite F by (rule normF_xl_lim)
    finally show ?thesis
      by auto
  qed
  have normF F l  1 + normF F (x (I 1)) if [simp]: finite F for F
    using normF_xl[where F=F and ε=1 and n=I 1]
    using normF_triangle[where F=F and x=x (I 1) and y=λa. l a - x (I 1) a]
    using normF_negate[where F=F and x=(λa. x (I 1) a - l a)]
    by auto
  also have  F  1 + ell2_norm (x (I 1)) if finite F for F
    using normF_ell2norm that by simp
  finally have [simp]: has_ell2_norm l
    unfolding has_ell2_norm_L2_set
    by (auto intro!: bdd_aboveI simp flip: normF_def)
  then have l = Rep_ell2 L
    by (simp add: Abs_ell2_inverse L_def)
  have [simp]: has_ell2_norm (λa. x n a - l a) for n
    apply (subst diff_conv_add_uminus)
    apply (rule ell2_norm_triangle)
    by (auto intro!: ell2_norm_uminus)
  from normF_xl have ell2norm_xl: ell2_norm (λa. x n a - l a)  ε
    if n  I ε and ε > 0 for n ε
    apply (subst ell2_norm_L2_set)
    using that by (auto intro!: cSUP_least simp: normF_def)
  have norm (X n - L)  ε if n  I ε and ε > 0 for n ε
    using ell2norm_xl[OF that]
    by (simp add: x_def norm_ell2.rep_eq l = Rep_ell2 L minus_ell2.rep_eq)
  then have X  L
    unfolding tendsto_iff
    apply (auto simp: dist_norm eventually_sequentially)
    by (meson field_lbound_gt_zero le_less_trans)
  then show convergent X
    by (rule convergentI)
qed

instantiation ell2 :: (CARD_1) complex_algebra_1 
begin
lift_definition one_ell2 :: "'a ell2" is "λ_. 1" by simp
lift_definition times_ell2 :: "'a ell2  'a ell2  'a ell2" is "λa b x. a x * b x"
  by simp   
instance 
proof
  fix a b c :: "'a ell2" and r :: complex
  show "a * b * c = a * (b * c)"
    by (transfer, auto)
  show "(a + b) * c = a * c + b * c"
    apply (transfer, rule ext)
    by (simp add: distrib_left mult.commute)
  show "a * (b + c) = a * b + a * c"
    apply transfer
    by (simp add: ring_class.ring_distribs(1))
  show "r *C a * b = r *C (a * b)"
    by (transfer, auto)
  show "(a::'a ell2) * r *C b = r *C (a * b)"
    by (transfer, auto)
  show "1 * a = a"
    by (transfer, rule ext, auto)
  show "a * 1 = a"
    by (transfer, rule ext, auto)
  show "(0::'a ell2)  1"
    apply transfer
    by (meson zero_neq_one)
qed
end

instantiation ell2 :: (CARD_1) field begin
lift_definition divide_ell2 :: "'a ell2  'a ell2  'a ell2" is "λa b x. a x / b x"
  by simp   
lift_definition inverse_ell2 :: "'a ell2  'a ell2" is "λa x. inverse (a x)"
  by simp
instance
proof (intro_classes; transfer)
  fix a :: "'a  complex"
  assume "a  (λ_. 0)"
  then obtain y where ay: "a y  0"
    by auto
  show "(λx. inverse (a x) * a x) = (λ_. 1)"
  proof (rule ext)
    fix x
    have "x = y"
      by auto
    with ay have "a x  0"
      by metis
    then show "inverse (a x) * a x = 1"
      by auto
  qed
qed (auto simp add: divide_complex_def mult.commute ring_class.ring_distribs)
end


subsection Orthogonality

lemma ell2_pointwise_ortho:
  assumes  i. Rep_ell2 x i = 0  Rep_ell2 y i = 0
  shows is_orthogonal x y
  using assms apply transfer
  by (simp add: infsum_0)

subsection Truncated vectors

lift_definition trunc_ell2:: 'a set  'a ell2  'a ell2
  is λ S x. (λ i. (if i  S then x i else 0))
proof (rename_tac S x)
  fix x :: 'a  complex and S :: 'a set
  assume has_ell2_norm x
  then have (λi. (x i)2) abs_summable_on UNIV
    unfolding has_ell2_norm_def by -
  then have (λi. (x i)2) abs_summable_on S
    using summable_on_subset_banach by blast
  then have (λxa. (if xa  S then x xa else 0)2) abs_summable_on UNIV
    apply (rule summable_on_cong_neutral[THEN iffD1, rotated -1])
    by auto
  then show has_ell2_norm (λi. if i  S then x i else 0)
    unfolding has_ell2_norm_def by -
qed

lemma trunc_ell2_empty[simp]: trunc_ell2 {} x = 0
  apply transfer by simp

lemma norm_id_minus_trunc_ell2:
  (norm (x - trunc_ell2 S x))^2 = (norm x)^2 - (norm (trunc_ell2 S x))^2
proof-
  have Rep_ell2 (trunc_ell2 S x) i = 0  Rep_ell2 (x - trunc_ell2 S x) i = 0 for i
    apply transfer
    by auto
  hence  (trunc_ell2 S x), (x - trunc_ell2 S x)  = 0
    using ell2_pointwise_ortho by blast
  hence (norm x)^2 = (norm (trunc_ell2 S x))^2 + (norm (x - trunc_ell2 S x))^2
    using pythagorean_theorem by fastforce    
  thus ?thesis by simp
qed

lemma norm_trunc_ell2_finite:
  finite S  (norm (trunc_ell2 S x)) = sqrt ((sum (λi. (cmod (Rep_ell2 x i))2)) S)
proof-
  assume finite S
  moreover have  i. i  S  Rep_ell2 ((trunc_ell2 S x)) i = 0
    by (simp add: trunc_ell2.rep_eq)    
  ultimately have (norm (trunc_ell2 S x)) = sqrt ((sum (λi. (cmod (Rep_ell2 ((trunc_ell2 S x)) i))2)) S)
    using ell2_norm_finite_support
    by blast 
  moreover have  i. i  S  Rep_ell2 ((trunc_ell2 S x)) i = Rep_ell2 x i
    by (simp add: trunc_ell2.rep_eq)
  ultimately show ?thesis by simp
qed

lemma trunc_ell2_lim_at_UNIV:
  ((λS. trunc_ell2 S ψ)  ψ) (finite_subsets_at_top UNIV)
proof -
  define f where f i = (cmod (Rep_ell2 ψ i))2 for i

  have has: has_ell2_norm (Rep_ell2 ψ)
    using Rep_ell2 by blast
  then have summable: "f abs_summable_on UNIV"
    by (smt (verit, del_insts) f_def has_ell2_norm_def norm_ge_zero norm_power real_norm_def summable_on_cong)

  have norm ψ = (ell2_norm (Rep_ell2 ψ))
    apply transfer by simp
  also have  = sqrt (infsum f UNIV)
    by (simp add: ell2_norm_def f_def[symmetric])
  finally have normψ: norm ψ = sqrt (infsum f UNIV)
    by -

  have norm_trunc: norm (trunc_ell2 S ψ) = sqrt (sum f S) if finite S for S
    using f_def that norm_trunc_ell2_finite by fastforce

  have (sum f  infsum f UNIV) (finite_subsets_at_top UNIV)
    using f_def[abs_def] infsum_tendsto local.summable by fastforce
  then have ((λS. sqrt (sum f S))  sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)
    using tendsto_real_sqrt by blast
  then have ((λS. norm (trunc_ell2 S ψ))  norm ψ) (finite_subsets_at_top UNIV)
    apply (subst tendsto_cong[where g=λS. sqrt (sum f S)])
    by (auto simp add: eventually_finite_subsets_at_top_weakI norm_trunc normψ)
  then have ((λS. (norm (trunc_ell2 S ψ))2)  (norm ψ)2) (finite_subsets_at_top UNIV)
    by (simp add: tendsto_power)
  then have ((λS. (norm ψ)2 - (norm (trunc_ell2 S ψ))2)  0) (finite_subsets_at_top UNIV)
    apply (rule tendsto_diff[where a=(norm ψ)^2 and b=(norm ψ)^2, simplified, rotated])
    by auto
  then have ((λS. (norm (ψ - trunc_ell2 S ψ))2)  0) (finite_subsets_at_top UNIV)
    unfolding norm_id_minus_trunc_ell2 by simp
  then have ((λS. norm (ψ - trunc_ell2 S ψ))  0) (finite_subsets_at_top UNIV)
    by auto
  then have ((λS. ψ - trunc_ell2 S ψ)  0) (finite_subsets_at_top UNIV)
    by (rule tendsto_norm_zero_cancel)
  then show ?thesis
    apply (rule Lim_transform2[where f=λ_. ψ, rotated])
    by simp
qed

subsection Kets and bras

lift_definition ket :: "'a  'a ell2" is "λx y. if x=y then 1 else 0"
  by (rule has_ell2_norm_ket)

abbreviation bra :: "'a  (_,complex) cblinfun" where "bra i  vector_to_cblinfun (ket i)*" for i

instance ell2 :: (type) not_singleton
proof standard
  have "ket undefined  (0::'a ell2)"
  proof transfer
    show "(λy. if (undefined::'a) = y then 1::complex else 0)  (λ_. 0)"
      by (meson one_neq_zero)
  qed   
  thus x y::'a ell2. x  y
    by blast    
qed

lemma cinner_ket_left: ket i, ψ = Rep_ell2 ψ i
  apply (transfer fixing: i)
  apply (subst infsum_cong_neutral[where T={i}])
  by auto

lemma cinner_ket_right: ψ, ket i = cnj (Rep_ell2 ψ i)
  apply (transfer fixing: i)
  apply (subst infsum_cong_neutral[where T={i}])
  by auto

lemma cinner_ket_eqI:
  assumes i. cinner (ket i) ψ = cinner (ket i) φ
  shows ψ = φ
  by (metis Rep_ell2_inject assms cinner_ket_left ext)

lemma norm_ket[simp]: "norm (ket i) = 1"
  apply transfer by (rule ell2_norm_ket)

lemma cinner_ket_same[simp]:
  ket i, ket i = 1
proof-
  have norm (ket i) = 1
    by simp
  hence sqrt (cmod ket i, ket i) = 1
    by (metis norm_eq_sqrt_cinner)
  hence cmod ket i, ket i = 1
    using real_sqrt_eq_1_iff by blast
  moreover have ket i, ket i = cmod ket i, ket i
  proof-
    have ket i, ket i  
      by (simp add: cinner_real)      
    thus ?thesis 
      by (metis cinner_ge_zero complex_of_real_cmod) 
  qed
  ultimately show ?thesis by simp
qed

lemma orthogonal_ket[simp]:
  is_orthogonal (ket i) (ket j)  i  j
  by (simp add: cinner_ket_left ket.rep_eq)

lemma cinner_ket: ket i, ket j = (if i=j then 1 else 0)
  by (simp add: cinner_ket_left ket.rep_eq)

lemma ket_injective[simp]: ket i = ket j  i = j
  by (metis cinner_ket one_neq_zero)

lemma inj_ket[simp]: inj ket
  by (simp add: inj_on_def)


lemma trunc_ell2_ket_cspan:
  trunc_ell2 S x  (cspan (range ket)) if finite S
proof (use that in induction)
  case empty
  then show ?case 
    by (auto intro: complex_vector.span_zero)
next
  case (insert a F)
  from insert.hyps have trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *C ket a
    apply (transfer fixing: F a)
    by auto
  with insert.IH
  show ?case
    by (simp add: complex_vector.span_add_eq complex_vector.span_base complex_vector.span_scale)
qed

lemma closed_cspan_range_ket[simp]:
  closure (cspan (range ket)) = UNIV
proof (intro set_eqI iffI UNIV_I closure_approachable[THEN iffD2] allI impI)
  fix ψ :: 'a ell2
  fix e :: real assume e > 0
  have ((λS. trunc_ell2 S ψ)  ψ) (finite_subsets_at_top UNIV)
    by (rule trunc_ell2_lim_at_UNIV)
  then obtain F where finite F and dist (trunc_ell2 F ψ) ψ < e
    apply (drule_tac tendstoD[OF _ e > 0])
    by (auto dest: simp: eventually_finite_subsets_at_top)
  moreover have trunc_ell2 F ψ  cspan (range ket)
    using finite F trunc_ell2_ket_cspan by blast
  ultimately show φcspan (range ket). dist φ ψ < e
    by auto
qed

lemma ccspan_range_ket[simp]: "ccspan (range ket) = (top::('a ell2 ccsubspace))"
proof-
  have closure (complex_vector.span (range ket)) = (UNIV::'a ell2 set)
    using Complex_L2.closed_cspan_range_ket by blast
  thus ?thesis
    by (simp add: ccspan.abs_eq top_ccsubspace.abs_eq)
qed

lemma cspan_range_ket_finite[simp]: "cspan (range ket :: 'a::finite ell2 set) = UNIV"
  by (metis closed_cspan_range_ket closure_finite_cspan finite_class.finite_UNIV finite_imageI)

instance ell2 :: (finite) cfinite_dim
proof
  define basis :: 'a ell2 set where basis = range ket
  have finite basis
    unfolding basis_def by simp
  moreover have cspan basis = UNIV
    by (simp add: basis_def)
  ultimately show basis::'a ell2 set. finite basis  cspan basis = UNIV
    by auto
qed

instantiation ell2 :: (enum) onb_enum begin
definition "canonical_basis_ell2 = map ket Enum.enum"
instance
proof
  show "distinct (canonical_basis::'a ell2 list)"
  proof-
    have finite (UNIV::'a set)
      by simp
    have distinct (enum_class.enum::'a list)
      using enum_distinct by blast
    moreover have inj_on ket (set enum_class.enum)
      by (meson inj_onI ket_injective)         
    ultimately show ?thesis
      unfolding canonical_basis_ell2_def
      using distinct_map
      by blast
  qed    

  show "is_ortho_set (set (canonical_basis::'a ell2 list))"
    apply (auto simp: canonical_basis_ell2_def enum_UNIV)
    by (smt (z3) norm_ket f_inv_into_f is_ortho_set_def orthogonal_ket norm_zero)

  show "cindependent (set (canonical_basis::'a ell2 list))"
    apply (auto simp: canonical_basis_ell2_def enum_UNIV)
    by (smt (verit, best) norm_ket f_inv_into_f is_ortho_set_def is_ortho_set_cindependent orthogonal_ket norm_zero)

  show "cspan (set (canonical_basis::'a ell2 list)) = UNIV"
    by (auto simp: canonical_basis_ell2_def enum_UNIV)

  show "norm (x::'a ell2) = 1"
    if "(x::'a ell2)  set canonical_basis"
    for x :: "'a ell2"
    using that unfolding canonical_basis_ell2_def 
    by auto
qed

end

lemma canonical_basis_length_ell2[code_unfold, simp]:
  "length (canonical_basis ::'a::enum ell2 list) = CARD('a)"
  unfolding canonical_basis_ell2_def apply simp
  using card_UNIV_length_enum by metis

lemma ket_canonical_basis: "ket x = canonical_basis ! enum_idx x"
proof-
  have "x = (enum_class.enum::'a list) ! enum_idx x"
    using enum_idx_correct[where i = x] by simp
  hence p1: "ket x = ket ((enum_class.enum::'a list) ! enum_idx x)"
    by simp
  have "enum_idx x < length (enum_class.enum::'a list)"
    using enum_idx_bound[where x = x].
  hence "(map ket (enum_class.enum::'a list)) ! enum_idx x 
        = ket ((enum_class.enum::'a list) ! enum_idx x)"
    by auto      
  thus ?thesis
    unfolding canonical_basis_ell2_def using p1 by auto    
qed

lemma clinear_equal_ket:
  fixes f g :: 'a::finite ell2  _
  assumes clinear f
  assumes clinear g
  assumes i. f (ket i) = g (ket i)
  shows f = g
  apply (rule ext)
  apply (rule complex_vector.linear_eq_on_span[where f=f and g=g and B=range ket])
  using assms by auto

lemma equal_ket:
  fixes A B :: ('a ell2, 'b::complex_normed_vector) cblinfun
  assumes  x. cblinfun_apply A (ket x) = cblinfun_apply B (ket x)
  shows A = B
  apply (rule cblinfun_eq_gen_eqI[where G=range ket])
  using assms by auto

lemma antilinear_equal_ket:
  fixes f g :: 'a::finite ell2  _
  assumes antilinear f
  assumes antilinear g
  assumes i. f (ket i) = g (ket i)
  shows f = g
proof -
  have [simp]: clinear (f  from_conjugate_space)
    apply (rule antilinear_o_antilinear)
    using assms by (simp_all add: antilinear_from_conjugate_space)
  have [simp]: clinear (g  from_conjugate_space)
    apply (rule antilinear_o_antilinear)
    using assms by (simp_all add: antilinear_from_conjugate_space)
  have [simp]: cspan (to_conjugate_space ` (range ket :: 'a ell2 set)) = UNIV
    by simp
  have "f o from_conjugate_space = g o from_conjugate_space"
    apply (rule ext)
    apply (rule complex_vector.linear_eq_on_span[where f="f o from_conjugate_space" and g="g o from_conjugate_space" and B=to_conjugate_space ` range ket])
       apply (simp, simp)
    using assms(3) by (auto simp: to_conjugate_space_inverse)
  then show "f = g"
    by (smt (verit) UNIV_I from_conjugate_space_inverse surj_def surj_fun_eq to_conjugate_space_inject) 
qed

lemma cinner_ket_adjointI:
  fixes F::"'a ell2 CL _" and G::"'b ell2 CL_"
  assumes " i j. F *V ket i, ket j = ket i, G *V ket j"
  shows "F = G*"
proof -
  from assms
  have (F *V x) C y = x C (G *V y) if x  range ket and y  range ket for x y
    using that by auto
  then have (F *V x) C y = x C (G *V y) if x  range ket for x y
    apply (rule bounded_clinear_eq_on[where G=range ket and t=y, rotated 2])
    using that by (auto intro!: bounded_linear_intros)
  then have (F *V x) C y = x C (G *V y) for x y
    apply (rule bounded_antilinear_eq_on[where G=range ket and t=x, rotated 2])
    by (auto intro!: bounded_linear_intros)
  then show ?thesis
    by (rule adjoint_eqI)
qed

lemma ket_nonzero[simp]: "ket i  0"
  using norm_ket[of i] by force


lemma cindependent_ket:
  "cindependent (range (ket::'a_))"
proof-
  define S where "S = range (ket::'a_)"
  have "is_ortho_set S"
    unfolding S_def is_ortho_set_def by auto
  moreover have "0  S"
    unfolding S_def
    using ket_nonzero
    by (simp add: image_iff)
  ultimately show ?thesis
    using is_ortho_set_cindependent[where A = S] unfolding S_def 
    by blast
qed

lemma cdim_UNIV_ell2[simp]: cdim (UNIV::'a::finite ell2 set) = CARD('a)
  apply (subst cspan_range_ket_finite[symmetric])
  by (metis card_image cindependent_ket complex_vector.dim_span_eq_card_independent inj_ket)

lemma is_ortho_set_ket[simp]: is_ortho_set (range ket)
  using is_ortho_set_def by fastforce

subsection Butterflies

lemma cspan_butterfly_ket: cspan {butterfly (ket i) (ket j)| (i::'b::finite) (j::'a::finite). True} = UNIV
proof -
  have *: {butterfly (ket i) (ket j)| (i::'b::finite) (j::'a::finite). True} = {butterfly a b |a b. a  range ket  b  range ket}
    by auto
  show ?thesis
    apply (subst *)
    apply (rule cspan_butterfly_UNIV)
    by auto
qed

lemma cindependent_butterfly_ket: cindependent {butterfly (ket i) (ket j)| (i::'b) (j::'a). True}
proof -
  have *: {butterfly (ket i) (ket j)| (i::'b) (j::'a). True} = {butterfly a b |a b. a  range ket  b  range ket}
    by auto
  show ?thesis
    apply (subst *)
    apply (rule cindependent_butterfly)
    by auto
qed

lemma clinear_eq_butterfly_ketI:
  fixes F G :: ('a::finite ell2 CL 'b::finite ell2)  'c::complex_vector
  assumes "clinear F" and "clinear G"
  assumes "i j. F (butterfly (ket i) (ket j)) = G (butterfly (ket i) (ket j))"
  shows "F = G"
  apply (rule complex_vector.linear_eq_on_span[where f=F, THEN ext, rotated 3])
     apply (subst cspan_butterfly_ket)
  using assms by auto

lemma sum_butterfly_ket[simp]: ((i::'a::finite)UNIV. butterfly (ket i) (ket i)) = id_cblinfun
  apply (rule equal_ket)
  apply (subst complex_vector.linear_sum[where f=λy. y *V ket _])
   apply (auto simp add: scaleC_cblinfun.rep_eq cblinfun.add_left clinearI butterfly_def cblinfun_compose_image cinner_ket)
  apply (subst sum.mono_neutral_cong_right[where S={_}])
  by auto

subsection One-dimensional spaces

instantiation ell2 :: ("{enum,CARD_1}") one_dim begin
text Note: enum is not needed logically, but without it this instantiation
            clashes with instantiation ell2 :: (enum) onb_enum›
instance
proof
  show "canonical_basis = [1::'a ell2]"
    unfolding canonical_basis_ell2_def
    apply transfer
    by (simp add: enum_CARD_1[of undefined])
  show "a *C 1 * b *C 1 = (a * b) *C (1::'a ell2)" for a b
    apply (transfer fixing: a b) by simp
  show "x / y = x * inverse y" for x y :: "'a ell2"
    by (simp add: divide_inverse)
  show "inverse (c *C 1) = inverse c *C (1::'a ell2)" for c :: complex
    apply transfer by auto
qed
end


subsection Classical operators

text We call an operator mapping termket x to termket (π x) or term0 "classical".
(The meaning is inspired by the fact that in quantum mechanics, such operators usually correspond
to operations with classical interpretation (such as Pauli-X, CNOT, measurement in the computational
basis, etc.))

definition classical_operator :: "('a'b option)  'a ell2 CL'b ell2" where
  "classical_operator π = 
    (let f = (λt. (case π (inv (ket::'a_) t) 
                           of None  (0::'b ell2) 
                          | Some i  ket i))
     in
      cblinfun_extension (range (ket::'a_)) f)"


definition "classical_operator_exists π 
  cblinfun_extension_exists (range ket)
    (λt. case π (inv ket t) of None  0 | Some i  ket i)"

lemma classical_operator_existsI:
  assumes "x. B *V (ket x) = (case π x of Some i  ket i | None  0)"
  shows "classical_operator_exists π"
  unfolding classical_operator_exists_def
  apply (rule cblinfun_extension_existsI[of _ B])
  using assms 
  by (auto simp: inv_f_f[OF inj_ket])

lemma classical_operator_exists_inj:
  assumes "inj_map π"
  shows "classical_operator_exists π"
proof -
  define f where f t = (case π (inv ket t) of None  0 | Some x  ket x) for t
  define g where g = cconstruct (range ket) f
  have g_f: g (ket x) = f (ket x) for x
    unfolding g_def apply (rule complex_vector.construct_basis)
    using cindependent_ket by auto
  have clinear g
    unfolding g_def apply (rule complex_vector.linear_construct)
    using cindependent_ket by blast
  then have g (x + y) = g x + g y if x  cspan (range ket) and y  cspan (range ket) for x y
    using clinear_iff by blast
  moreover from clinear g have g (c *C x) = c *C g x if x  cspan (range ket) for x c
    by (simp add: complex_vector.linear_scale)
  moreover have norm (g x)  norm x if x  cspan (range ket) for x
  proof -
    from that obtain t r where x_sum: x = (at. r a *C a) and finite t and t  range ket
      unfolding complex_vector.span_explicit by auto
    then obtain T where tT: t = ket ` T and [simp]: finite T
      by (meson finite_subset_image)
    define R where R i = r (ket i) for i
    have x_sum: x = (iT. R i *C ket i)
      unfolding R_def tT x_sum
      apply (rule sum.reindex_cong)
      by (auto simp add: inj_on_def)

    define T' π' πT πR where T' = {iT. π i  None} and π' = the o π and πT = π' ` T' and πR i = R (inv_into T' π' i) for i
    have inj_on π' T'
      by (smt (z3) T'_def π'_def assms comp_apply inj_map_def inj_on_def mem_Collect_eq option.expand)
    have [simp]: finite πT
      by (simp add: T'_def πT_def)

    have g x = (iT. R i *C g (ket i))
      by (smt (verit, ccfv_threshold) clinear g complex_vector.linear_scale complex_vector.linear_sum sum.cong x_sum)
    also have  = (iT. R i *C f (ket i))
      using g_f by presburger
    also have  = (iT. R i *C (case π i of None  0 | Some x  ket x))
      unfolding f_def by auto
    also have  = (iT'. R i *C ket (π' i))
      apply (rule sum.mono_neutral_cong_right)
      unfolding T'_def π'_def
      by auto
    also have  = (iπ' ` T'. R (inv_into T' π' i) *C ket i)
      apply (subst sum.reindex)
      using inj_on π' T' apply assumption
      apply (rule sum.cong)
      using inj_on π' T' by auto
    finally have gx_sum: g x = (iπT. πR i *C ket i)
      using πR_def πT_def by auto

    have (norm (g x))2 = (aπT. (cmod (πR a))2)
      unfolding gx_sum 
      apply (subst pythagorean_theorem_sum)
      by auto
    also have  = (iT'. (cmod (R i))2)
      unfolding πR_def πT_def
      apply (subst sum.reindex)
      using inj_on π' T' apply assumption
      apply (rule sum.cong)
      using inj_on π' T' by auto
    also have   (aT. (cmod (R a))2)
      apply (rule sum_mono2)
      using T'_def by auto
    also have  = (norm x)2
      unfolding x_sum 
      apply (subst pythagorean_theorem_sum)
      using finite T by auto
    finally show norm (g x)  norm x
      by auto
  qed
  ultimately have cblinfun_extension_exists (cspan (range ket)) g
    apply (rule_tac cblinfun_extension_exists_bounded_dense[where B=1])
    by auto

  then have cblinfun_extension_exists (range ket) f
    by (metis (mono_tags, opaque_lifting) g_f cblinfun_extension_apply cblinfun_extension_existsI complex_vector.span_base rangeE)
  then show classical_operator_exists π
    unfolding classical_operator_exists_def f_def by simp
qed

lemma classical_operator_exists_finite[simp]: "classical_operator_exists (π :: _::finite  _)"
  unfolding classical_operator_exists_def
  apply (rule cblinfun_extension_exists_finite_dim)
  using cindependent_ket apply blast
  using finite_class.finite_UNIV finite_imageI closed_cspan_range_ket closure_finite_cspan by blast

lemma classical_operator_ket:
  assumes "classical_operator_exists π"
  shows "(classical_operator π) *V (ket x) = (case π x of Some i  ket i | None  0)"
  unfolding classical_operator_def 
  using f_inv_into_f ket_injective rangeI
  by (metis assms cblinfun_extension_apply classical_operator_exists_def)

lemma classical_operator_ket_finite:
  "(classical_operator π) *V (ket (x::'a::finite)) = (case π x of Some i  ket i | None  0)"
  by (rule classical_operator_ket, simp)

lemma classical_operator_adjoint[simp]:
  fixes π :: "'a  'b option"
  assumes a1: "inj_map π"
  shows  "(classical_operator π)* = classical_operator (inv_map π)"
proof-
  define F where "F = classical_operator (inv_map π)"
  define G where "G = classical_operator π"
  have "F *V ket i, ket j = ket i, G *V ket j" for i j
  proof-
    have w1: "(classical_operator (inv_map π)) *V (ket i)
     = (case inv_map π i of Some k  ket k | None  0)"
      by (simp add: classical_operator_ket classical_operator_exists_inj)
    have w2: "(classical_operator π) *V (ket j)
     = (case π j of Some k  ket k | None  0)"
      by (simp add: assms classical_operator_ket classical_operator_exists_inj)
    have "F *V ket i, ket j = classical_operator (inv_map π) *V ket i, ket j"
      unfolding F_def by blast
    also have " = (case inv_map π i of Some k  ket k | None  0), ket j"
      using w1 by simp
    also have " = ket i, (case π j of Some k  ket k | None  0)"
    proof(induction "inv_map π i")
      case None
      hence pi1: "None = inv_map π i".
      show ?case 
      proof (induction "π j")
        case None
        thus ?case
          using pi1 by auto
      next
        case (Some c)
        have "c  i"
        proof(rule classical)
          assume "¬(c  i)"
          hence "c = i"
            by blast
          hence "inv_map π c = inv_map π i"
            by simp
          hence "inv_map π c = None"
            by (simp add: pi1)
          moreover have "inv_map π c = Some j"
            using Some.hyps unfolding inv_map_def
            apply auto
            by (metis a1 f_inv_into_f inj_map_def option.distinct(1) rangeI)
          ultimately show ?thesis by simp
        qed
        thus ?thesis
          by (metis None.hyps Some.hyps cinner_zero_left orthogonal_ket option.simps(4) 
              option.simps(5)) 
      qed       
    next
      case (Some d)
      hence s1: "Some d = inv_map π i".
      show "case inv_map π i of 
            None  0
        | Some a  ket a, ket j =
       ket i, case π j of 
            None  0 
        | Some a  ket a" 
      proof(induction "π j")
        case None
        have "d  j"
        proof(rule classical)
          assume "¬(d  j)"
          hence "d = j"
            by blast
          hence "π d = π j"
            by simp
          hence "π d = None"
            by (simp add: None.hyps)
          moreover have "π d = Some i"
            using Some.hyps unfolding inv_map_def
            apply auto
            by (metis f_inv_into_f option.distinct(1) option.inject)
          ultimately show ?thesis 
            by simp
        qed
        thus ?case
          by (metis None.hyps Some.hyps cinner_zero_right orthogonal_ket option.case_eq_if 
              option.simps(5)) 
      next
        case (Some c)
        hence s2: "π j = Some c" by simp
        have "ket d, ket j = ket i, ket c"
        proof(cases "π j = Some i")
          case True
          hence ij: "Some j = inv_map π i"
            unfolding inv_map_def apply auto
             apply (metis a1 f_inv_into_f inj_map_def option.discI range_eqI)
            by (metis range_eqI)
          have "i = c"
            using True s2 by auto
          moreover have "j = d"
            by (metis option.inject s1 ij)
          ultimately show ?thesis
            by (simp add: cinner_ket_same) 
        next
          case False
          moreover have "π d = Some i"
            using s1 unfolding inv_map_def
            by (metis f_inv_into_f option.distinct(1) option.inject)            
          ultimately have "j  d"
            by auto            
          moreover have "i  c"
            using False s2 by auto            
          ultimately show ?thesis
            by (metis orthogonal_ket) 
        qed
        hence "case Some d of None  0
        | Some a  ket a, ket j =
       ket i, case Some c of None  0 | Some a  ket a"
          by simp          
        thus "case inv_map π i of None  0
        | Some a  ket a, ket j =
       ket i, case π j of None  0 | Some a  ket a"
          by (simp add: Some.hyps s1)          
      qed
    qed
    also have " = ket i, classical_operator π *V ket j"
      by (simp add: w2)
    also have " = ket i, G *V ket j"
      unfolding G_def by blast
    finally show ?thesis .
  qed
  hence "G* = F"
    using cinner_ket_adjointI
    by auto
  thus ?thesis unfolding G_def F_def .
qed

lemma
  fixes π::"'b  'c option" and ρ::"'a  'b option"
  assumes "classical_operator_exists π"
  assumes "classical_operator_exists ρ"
  shows classical_operator_exists_comp[simp]: "classical_operator_exists (π m ρ)"
    and classical_operator_mult[simp]: "classical_operator π oCL classical_operator ρ = classical_operator (π m ρ)"
proof -
  define   Cπρ where " = classical_operator π" and " = classical_operator ρ" 
    and "Cπρ = classical_operator (π m ρ)"
  have Cπx: " *V (ket x) = (case π x of Some i  ket i | None  0)" for x
    unfolding Cπ_def using classical_operator_exists π by (rule classical_operator_ket)
  have Cρx: " *V (ket x) = (case ρ x of Some i  ket i | None  0)" for x
    unfolding Cρ_def using classical_operator_exists ρ by (rule classical_operator_ket)
  have Cπρx': "( oCL ) *V (ket x) = (case (π m ρ) x of Some i  ket i | None  0)" for x
    apply (simp add: scaleC_cblinfun.rep_eq Cρx)
    apply (cases "ρ x")
    by (auto simp: Cπx)
  thus classical_operator_exists (π m ρ)
    by (rule classical_operator_existsI)
  hence "Cπρ *V (ket x) = (case (π m ρ) x of Some i  ket i | None  0)" for x
    unfolding Cπρ_def
    by (rule classical_operator_ket)
  with Cπρx' have "( oCL ) *V (ket x) = Cπρ *V (ket x)" for x
    by simp
  thus " oCL  = Cπρ"
    by (simp add: equal_ket)
qed

lemma classical_operator_Some[simp]: "classical_operator (Some::'a_) = id_cblinfun"
proof-
  have "(classical_operator Some) *V (ket i)  = id_cblinfun *V (ket i)"
    for i::'a
    apply (subst classical_operator_ket)
     apply (rule classical_operator_exists_inj)
    by auto
  thus ?thesis
    using equal_ket[where A = "classical_operator (Some::'a  _ option)"
        and B = "id_cblinfun::'a ell2 CL _"]
    by blast
qed

lemma isometry_classical_operator[simp]:
  fixes π::"'a  'b"
  assumes a1: "inj π"
  shows "isometry (classical_operator (Some o π))"
proof -
  have b0: "inj_map (Some  π)