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 f = sqrt (x. norm (f x)^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 (f::'a::finite_)"
  unfolding has_ell2_norm_def by simp

lemma ell2_norm_finite: 
  "ell2_norm (f::'a::finitecomplex) = sqrt (xUNIV. (norm (f x))^2)"
  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_norm_square: (ell2_norm x)2 = (i. (cmod (x i))2)
  unfolding ell2_norm_def
  apply (subst real_sqrt_pow2)
  by (simp_all add: infsum_nonneg)

lemma ell2_ket:
  fixes a
  defines f  (λi. of_bool (a = i))
  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 = {f::'acomplex. has_ell2_norm f}
  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 
  λf g. x. (cnj (f x) * g x) .
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 intro_classes
  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

lemma sum_ell2_transfer[transfer_rule]:
  includes lifting_syntax
  shows (((=) ===> pcr_ell2 (=)) ===> rel_set (=) ===> pcr_ell2 (=)) 
          (λf X x. sum (λy. f y x) X) sum
proof (intro rel_funI, rename_tac f f' X X')
  fix f and f' :: 'a  'b ell2 
  assume [transfer_rule]: ((=) ===> pcr_ell2 (=)) f f'
  fix X X' :: 'a set
  assume rel_set (=) X X'
  then have [simp]: X' = X
    by (simp add: rel_set_eq)
  show pcr_ell2 (=) (λx. yX. f y x) (sum f' X')
    unfolding X' = X
  proof (induction X rule: infinite_finite_induct)
    case (infinite X)
    show ?case
      apply (simp add: infinite)
      by transfer_prover
  next
    case empty
    show ?case
      apply (simp add: empty)
      by transfer_prover
  next
    case (insert x F)
    note [transfer_rule] = insert.IH
    show ?case
      apply (simp add: insert)
      by transfer_prover
  qed
qed

lemma clinear_Rep_ell2[simp]: clinear (λψ. Rep_ell2 ψ i)
  by (simp add: clinearI plus_ell2.rep_eq scaleC_ell2.rep_eq)

lemma Abs_ell2_inverse_finite[simp]: Rep_ell2 (Abs_ell2 ψ) = ψ for ψ :: _::finite  complex
  by (simp add: Abs_ell2_inverse)


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 trunc_ell2_UNIV[simp]: trunc_ell2 UNIV ψ = ψ
  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) C (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

lemma trunc_ell2_norm_mono: M  N  norm (trunc_ell2 M ψ)  norm (trunc_ell2 N ψ)
proof (rule power2_le_imp_le[rotated], force, transfer)
  fix M N :: 'a set and ψ :: 'a  complex
  assume M  N and has_ell2_norm ψ
  have (ell2_norm (λi. if i  M then ψ i else 0))2 = (iM. (cmod (ψ i))2)
    unfolding ell2_norm_square
    apply (rule infsum_cong_neutral)
    by auto
  also have   (iN. (cmod (ψ i))2)
    apply (rule infsum_mono2)
    using has_ell2_norm ψ M  N
    by (auto simp add: ell2_norm_square has_ell2_norm_def simp flip: norm_power intro: summable_on_subset_banach)
  also have  = (ell2_norm (λi. if i  N then ψ i else 0))2
    unfolding ell2_norm_square
    apply (rule infsum_cong_neutral)
    by auto
  finally show (ell2_norm (λi. if i  M then ψ i else 0))2  (ell2_norm (λi. if i  N then ψ i else 0))2
    by -
qed

lemma trunc_ell2_reduces_norm: norm (trunc_ell2 M ψ)  norm ψ
  by (metis subset_UNIV trunc_ell2_UNIV trunc_ell2_norm_mono)

lemma trunc_ell2_twice[simp]: trunc_ell2 M (trunc_ell2 N ψ) = trunc_ell2 (MN) ψ
  apply transfer by auto

lemma trunc_ell2_union: trunc_ell2 (M  N) ψ = trunc_ell2 M ψ + trunc_ell2 N ψ - trunc_ell2 (MN) ψ
  apply transfer by auto

lemma trunc_ell2_union_disjoint: M  N = {}  trunc_ell2 (M  N) ψ = trunc_ell2 M ψ + trunc_ell2 N ψ
  by (simp add: trunc_ell2_union)

lemma trunc_ell2_union_Diff: M  N  trunc_ell2 (N-M) ψ = trunc_ell2 N ψ - trunc_ell2 M ψ
  using trunc_ell2_union_disjoint[where M=N-M and N=M and ψ=ψ]
  by (simp add: Un_commute inf.commute le_iff_sup)

lemma trunc_ell2_add: trunc_ell2 M (ψ + φ) = trunc_ell2 M ψ + trunc_ell2 M φ
  apply transfer by auto

lemma trunc_ell2_scaleC: trunc_ell2 M (c *C ψ) = c *C trunc_ell2 M ψ
  apply transfer by auto

lemma bounded_clinear_trunc_ell2[bounded_clinear]: bounded_clinear (trunc_ell2 M)
  by (auto intro!: bounded_clinearI[where K=1] trunc_ell2_reduces_norm
      simp: trunc_ell2_add trunc_ell2_scaleC)

lemma trunc_ell2_lim: ((λS. trunc_ell2 S ψ)  trunc_ell2 M ψ) (finite_subsets_at_top M)
proof -
  have ((λS. trunc_ell2 S (trunc_ell2 M ψ))  trunc_ell2 M ψ) (finite_subsets_at_top UNIV)
    using trunc_ell2_lim_at_UNIV by blast
  then have ((λS. trunc_ell2 (SM) ψ)  trunc_ell2 M ψ) (finite_subsets_at_top UNIV)
    by simp
  then show ((λS. trunc_ell2 S ψ)  trunc_ell2 M ψ) (finite_subsets_at_top M)
    unfolding filterlim_def
    apply (subst (asm) filtermap_filtermap[where g=λS. SM, symmetric])
    apply (subst (asm) finite_subsets_at_top_inter[where A=M and B=UNIV])
    by auto
qed

lemma trunc_ell2_lim_general:
  assumes big: G. finite G  G  M  (F H in F. H  G)
  assumes small: F H in F. H  M
  shows ((λS. trunc_ell2 S ψ)  trunc_ell2 M ψ) F
proof (rule tendstoI)
  fix e :: real assume e > 0
  from trunc_ell2_lim[THEN tendsto_iff[THEN iffD1], rule_format, OF e > 0, where M=M and ψ=ψ]
  obtain G where finite G and G  M and 
    close: dist (trunc_ell2 G ψ) (trunc_ell2 M ψ) < e
    apply atomize_elim
    unfolding eventually_finite_subsets_at_top
    by blast
  from finite G G  M and big
  have F H in F. H  G
    by -
  with small have F H in F. H  M  H  G
    by (simp add: eventually_conj_iff)
  then show F H in F. dist (trunc_ell2 H ψ) (trunc_ell2 M ψ) < e
  proof (rule eventually_mono)
    fix H assume GHM: H  M  H  G
    have dist (trunc_ell2 H ψ) (trunc_ell2 M ψ) = norm (trunc_ell2 (M-H) ψ)
      by (simp add: GHM dist_ell2_def norm_minus_commute trunc_ell2_union_Diff)
    also have   norm (trunc_ell2 (M-G) ψ)
      by (simp add: Diff_mono GHM trunc_ell2_norm_mono)
    also have   = dist (trunc_ell2 G ψ) (trunc_ell2 M ψ)
      by (simp add: G  M dist_ell2_def norm_minus_commute trunc_ell2_union_Diff)
    also have  < e
      using close by simp
    finally show dist (trunc_ell2 H ψ) (trunc_ell2 M ψ) < e
      by -
  qed
qed

lemma norm_ell2_bound_trunc:
  assumes M. finite M  norm (trunc_ell2 M ψ)  B
  shows norm ψ  B
proof -
  note trunc_ell2_lim_at_UNIV[of ψ]
  then have ((λS. norm (trunc_ell2 S ψ))  norm ψ) (finite_subsets_at_top UNIV)
    using tendsto_norm by auto
  then show norm ψ  B
    apply (rule tendsto_upperbound)
    using assms apply (rule eventually_finite_subsets_at_top_weakI)
    by auto
qed

lemma trunc_ell2_uminus: trunc_ell2 (-M) ψ = ψ - trunc_ell2 M ψ
  by (metis Int_UNIV_left boolean_algebra_class.diff_eq subset_UNIV trunc_ell2_UNIV trunc_ell2_union_Diff)

subsection ‹Kets and bras›

lift_definition ket :: 'a  'a ell2 is λx y. of_bool (x=y)
  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. of_bool ((undefined::'a) = y))  (λ_. 0)
      by (metis (mono_tags) of_bool_eq(2) zero_neq_one)
  qed   
  thus x y::'a ell2. x  y
    by blast    
qed

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

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

(* Doesn't really belong in this subsection but uses lemmas from this subsection for its proof. *)
lemma bounded_clinear_Rep_ell2[simp, bounded_clinear]: bounded_clinear (λψ. Rep_ell2 ψ x)
  apply (subst asm_rl[of (λψ. Rep_ell2 ψ x) = (λψ. ket x C ψ)])
   apply (auto simp: cinner_ket_left) 
  by (simp add: bounded_clinear_cinner_right)

lemma cinner_ket_eqI:
  assumes i. ket i C ψ = ket i C φ
  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 C ket i) = 1
proof-
  have norm (ket i) = 1
    by simp
  hence sqrt (cmod (ket i C ket i)) = 1
    by (metis norm_eq_sqrt_cinner)
  hence cmod (ket i C ket i) = 1
    using real_sqrt_eq_1_iff by blast
  moreover have (ket i C ket i) = cmod (ket i C ket i)
  proof-
    have (ket i C ket i)  
      by (simp add: cinner_real)      
    thus ?thesis 
      by (metis norm (ket i) = 1 cnorm_eq norm_one of_real_1 one_cinner_one)
  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 of_bool_def)

lemma cinner_ket: (ket i C ket j) = of_bool (i=j)
  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 of_bool_def)

lemma inj_ket[simp]: inj_on ket M
  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"
definition canonical_basis_length_ell2 (_ :: 'a ell2 itself) = length (Enum.enum :: 'a list)
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

  show canonical_basis_length TYPE('a ell2) = length (canonical_basis :: 'a ell2 list)
    by (simp add: canonical_basis_length_ell2_def canonical_basis_ell2_def)
  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] card_UNIV_length_enum
    by metis
  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. A *V ket x = B *V 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) C ket j = ket i C (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_closure[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[simp]:
  "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

lemma bounded_clinear_equal_ket:
  fixes f g :: 'a ell2  _
  assumes bounded_clinear f
  assumes bounded_clinear g
  assumes i. f (ket i) = g (ket i)
  shows f = g
  apply (rule ext)
  apply (rule bounded_clinear_eq_on_closure[of f g range ket])
  using assms by auto

lemma bounded_antilinear_equal_ket:
  fixes f g :: 'a ell2  _
  assumes bounded_antilinear f
  assumes bounded_antilinear g
  assumes i. f (ket i) = g (ket i)
  shows f = g
  apply (rule ext)
  apply (rule bounded_antilinear_eq_on[of f g range ket])
  using assms by auto

lemma is_onb_ket[simp]: is_onb (range ket)
  by (auto simp: is_onb_def)

lemma ell2_sum_ket: ψ = (iUNIV. Rep_ell2 ψ i *C ket i) for ψ :: _::finite ell2
  apply transfer apply (rule ext)
  apply (subst sum_single)
  by auto

lemma trunc_ell2_singleton: trunc_ell2 {x} ψ = Rep_ell2 ψ x *C ket x
  apply transfer by auto

lemma trunc_ell2_insert: trunc_ell2 (insert x M) φ = Rep_ell2 φ x *C ket x + trunc_ell2 M φ
  if x  M
  using trunc_ell2_union_disjoint[where M={x} and N=M]
  using that by (auto simp: trunc_ell2_singleton)

lemma trunc_ell2_finite_sum: trunc_ell2 M ψ = (iM. Rep_ell2 ψ i *C ket i) if finite M
  using that apply induction by (auto simp: trunc_ell2_insert)

lemma is_orthogonal_trunc_ell2: is_orthogonal (trunc_ell2 M ψ) (trunc_ell2 N φ) if M  N = {}
proof -
  have *: cnj (if i  M then a else 0) * (if i  N then b else 0) = 0 for a b i
    using that by auto
  show ?thesis
    apply (transfer fixing: M N)
    by (simp add: * )
qed

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

lemma ell2_decompose_has_sum: ((λx. Rep_ell2 φ x *C ket x) has_sum φ) UNIV
proof (unfold has_sum_def)
  have *: trunc_ell2 M φ = (xM. Rep_ell2 φ x *C ket x) if finite M for M
    using that apply induction
    by (auto simp: trunc_ell2_insert)
  show (sum (λx. Rep_ell2 φ x *C ket x)  φ) (finite_subsets_at_top UNIV)
    apply (rule Lim_transform_eventually)
     apply (rule trunc_ell2_lim_at_UNIV)
    using * by (rule eventually_finite_subsets_at_top_weakI)
qed

lemma ell2_decompose_infsum: φ = (x. Rep_ell2 φ x *C ket x)
  by (metis ell2_decompose_has_sum infsumI)

lemma ell2_decompose_summable: (λx. Rep_ell2 φ x *C ket x) summable_on UNIV
  using ell2_decompose_has_sum summable_on_def by blast

lemma Rep_ell2_cblinfun_apply_sum: Rep_ell2 (A *V φ) y = (x. Rep_ell2 φ x * Rep_ell2 (A *V ket x) y)
proof -
  have 1: bounded_linear (λz. Rep_ell2 (A *V z) y)
    by (auto intro!: bounded_clinear_compose[unfolded o_def, OF bounded_clinear_Rep_ell2]
        cblinfun.bounded_clinear_right bounded_clinear.bounded_linear)
  have 2: (λx. Rep_ell2 φ x *C ket x) summable_on UNIV
    by (simp add: ell2_decompose_summable)
  have Rep_ell2 (A *V φ) y = Rep_ell2 (A *V (x. Rep_ell2 φ x *C ket x)) y
    by (simp flip: ell2_decompose_infsum)
  also have  = (x. Rep_ell2 (A *V (Rep_ell2 φ x *C ket x)) y)
    apply (subst infsum_bounded_linear[symmetric, where h=λz. Rep_ell2 (A *V z) y])
    using 1 2 by (auto simp: o_def)
  also have  = (x. Rep_ell2 φ x * Rep_ell2 (A *V ket x) y)
    by (simp add: cblinfun.scaleC_right scaleC_ell2.rep_eq)
  finally show ?thesis
    by -
qed


subsection ‹One-dimensional spaces›

instantiation ell2 :: (CARD_1) one begin
lift_definition one_ell2 :: "'a ell2" is "λ_. 1" by simp
instance..
end

lemma ket_CARD_1_is_1: ket x = 1 for x :: 'a::CARD_1
  apply transfer by simp

instantiation ell2 :: (CARD_1) times begin
lift_definition times_ell2 :: "'a ell2  'a ell2  'a ell2" is "λa b x. a x * b x"
  by simp   
instance..
end

instantiation ell2 :: (CARD_1) divide begin
lift_definition divide_ell2 :: "'a ell2  'a ell2  'a ell2" is "λa b x. a x / b x"
  by simp   
instance..
end

instantiation ell2 :: (CARD_1) inverse begin
lift_definition inverse_ell2 :: "'a ell2  'a ell2" is "λa x. inverse (a x)"
  by simp
instance..
end

instance ell2 :: ("{enum,CARD_1}") one_dim
text ‹Note: enum is not needed logically, but without it this instantiation
            clashes with instantiation ell2 :: (enum) onb_enum›
proof intro_classes
  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"
    apply transfer
    by (simp add: divide_inverse)
  show "inverse (c *C 1) = inverse c *C (1::'a ell2)" for c :: complex
    apply transfer by auto
qed

subsection ‹Explicit bounded operators›

definition explicit_cblinfun :: ('a  'b  complex)  ('b ell2, 'a ell2) cblinfun where
  explicit_cblinfun M = cblinfun_extension (range ket) (λa. Abs_ell2 (λj. M j (inv ket a)))

definition explicit_cblinfun_exists :: ('a  'b  complex)  bool where
  explicit_cblinfun_exists M  
    (a. has_ell2_norm (λj. M j a))  
      cblinfun_extension_exists (range ket) (λa. Abs_ell2 (λj. M j (inv ket a)))

lemma explicit_cblinfun_exists_bounded:
  assumes S T ψ. finite S  finite T  (a. aT  ψ a = 0) 
            (bS. (cmod (aT. ψ a *C M b a))2)  B * (aT. (cmod (ψ a))2)
  shows explicit_cblinfun_exists M
proof -
  define F f where F = complex_vector.construct (range ket) f
    and f = (λa. Abs_ell2 (λj. M j (inv ket a)))
  from assms[where S={} and T={undefined} and ψ=λx. of_bool (x=undefined)]
  have B  0
    by auto
  have has_norm: has_ell2_norm (λb. M b a) for a
  proof (unfold has_ell2_norm_def, intro nonneg_bdd_above_summable_on bdd_aboveI)
    show 0  cmod ((M x a)2) for x
      by simp
    fix B'
    assume B'  sum (λx. cmod ((M x a)2)) ` {F. F  UNIV  finite F}
    then obtain S where [simp]: finite S and B'_def: B' = (xS. cmod ((M x a)2))
      by blast
    from assms[where S=S and T={a} and ψ=λx. of_bool (x=a)]
    show B'  B
      by (simp add: norm_power B'_def)
  qed
  have clinear F
    by (auto intro!: complex_vector.linear_construct simp: F_def)
  have F_B: norm (F ψ)  (sqrt B) * norm ψ if ψ_range_ket: ψ  cspan (range ket) for ψ
  proof -
    from that
    obtain T' where finite T' and T'  range ket and ψT': ψ  cspan T'
      by (meson vector_finitely_spanned)
        (*   from that
    obtain T' r where ‹finite T'› and ‹T' ⊆ range ket› and
      ψT': ‹ψ = (∑v∈T'. r v *C v)›
      unfolding complex_vector.span_explicit
      by blast *)
    then obtain T where T'_def: T' = ket ` T
      by (meson subset_image_iff)
    have finite T
      by (metis T'_def finite T' finite_image_iff inj_ket inj_on_subset subset_UNIV)
    have ψT: ψ  cspan (ket ` T)
      using T'_def ψT' by blast
    have Rep_ψ: Rep_ell2 ψ x = 0 if x  T for x
      using _ _ ψT apply (rule complex_vector.linear_eq_0_on_span)
       apply auto
      by (metis ket.rep_eq that of_bool_def)
    have norm (trunc_ell2 S (F ψ))  sqrt B * norm ψ if finite S for S
    proof -
      have *: cconstruct (range ket) f ψ = (xT. Rep_ell2 ψ x *C f (ket x))
      proof (rule complex_vector.linear_eq_on[where x=ψ and B=ket ` T])
        show clinear (cconstruct (range ket) f)
          using F_def clinear F by blast
        show clinear (λa. xT. Rep_ell2 a x *C f (ket x))
          by (auto intro!: clinear_compose[unfolded o_def, OF clinear_Rep_ell2] complex_vector.linear_compose_sum)
        show ψ  cspan (ket ` T)
          by (simp add: ψT)
        have f b = (xT. Rep_ell2 b x *C f (ket x)) 
          if b  ket ` T for b
        proof -
          define b' where b' = inv ket b
          have bb': b = ket b'
            using b'_def that by force
          show ?thesis
            apply (subst sum_single[where i=b'])
            using that by (auto simp add: finite T bb' ket.rep_eq)
        qed
        then show cconstruct (range ket) f b = (xT. Rep_ell2 b x *C f (ket x))
          if b  ket ` T for b
          apply (subst complex_vector.construct_basis)
          using that by auto
      qed
      have (norm (trunc_ell2 S (F ψ)))2 = (norm (trunc_ell2 S (xT. Rep_ell2 ψ x *C f (ket x))))2
        apply (rule arg_cong[where f=λx. (norm (trunc_ell2 _ x))2])
        by (simp add: F_def * )
      also have  = (norm (trunc_ell2 S (xT. Rep_ell2 ψ x *C Abs_ell2 (λb. M b x))))2
        by (simp add: f_def)
      also have  = (iS. (cmod (Rep_ell2 (xT. Rep_ell2 ψ x *C Abs_ell2 (λb. M b x)) i))2)
        by (simp add: that norm_trunc_ell2_finite real_sqrt_pow2 sum_nonneg)
      also have  = (iS. (cmod (xT. Rep_ell2 ψ x *C Rep_ell2 (Abs_ell2 (λb. M b x)) i))2)
        by (simp add: complex_vector.linear_sum[OF clinear_Rep_ell2]
            clinear.scaleC[OF clinear_Rep_ell2])
      also have  = (iS. (cmod (xT. Rep_ell2 ψ x *C M i x))2)
        using has_norm by (simp add: Abs_ell2_inverse)
      also have   B * (xT. (cmod (Rep_ell2 ψ x))2)
        using finite S finite T Rep_ψ by (rule assms)
      also have  = B * ((norm (trunc_ell2 T ψ))2)
        by (simp add: finite T norm_trunc_ell2_finite sum_nonneg)
      also have   B * (norm ψ)2
        by (simp add: mult_left_mono B  0 trunc_ell2_reduces_norm)
      finally show ?thesis
        apply (rule_tac power2_le_imp_le)
        by (simp_all add: 0  B power_mult_distrib)
    qed
    then show ?thesis
      by (rule norm_ell2_bound_trunc)
  qed
  then have cblinfun_extension_exists (cspan (range ket)) F
    apply (rule cblinfun_extension_exists_hilbert[rotated -1])
    by (auto intro: clinear F complex_vector.linear_add complex_vector.linear_scale)
  then have ex: cblinfun_extension_exists (range ket) f
    apply (rule cblinfun_extension_exists_restrict[rotated -1])
    by (simp_all add: F_def complex_vector.span_superset complex_vector.construct_basis)
  from ex has_norm
  show ?thesis
    using explicit_cblinfun_exists_def f_def by blast
qed

lemma explicit_cblinfun_exists_finite_dim[simp]: explicit_cblinfun_exists m for m :: "_::finite  _::finite  _"
  by (auto simp: explicit_cblinfun_exists_def cblinfun_extension_exists_finite_dim)

lemma explicit_cblinfun_ket: explicit_cblinfun M *V ket a = Abs_ell2 (λb. M b a) if explicit_cblinfun_exists M
  using that by (auto simp: explicit_cblinfun_exists_def explicit_cblinfun_def cblinfun_extension_apply)

lemma Rep_ell2_explicit_cblinfun_ket[simp]: Rep_ell2 (explicit_cblinfun M *V ket a) b = M b a if explicit_cblinfun_exists M
  using that apply (simp add: explicit_cblinfun_ket)
  by (simp add: Abs_ell2_inverse explicit_cblinfun_exists_def)

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 
  assumes "inj_map π"
  shows classical_operator_exists_inj: "classical_operator_exists π"
    and classical_operator_norm_inj: norm (classical_operator π)  1
proof -
  have is_orthogonal (case π x of None  0 | Some x'  ket x')
                      (case π y of None  0 | Some y'  ket y')
    if x  y for x y
    apply (cases π x; cases π y)
    using that assms
    by (auto simp add: inj_map_def)
  then have 1: is_orthogonal (case π (inv ket x) of None  0 | Some x'  ket x')
                      (case π (inv ket y) of None  0 | Some y'  ket y')
    if x  range ket and y  range ket and x  y for x y
    using that by auto

  have norm (case π x of None  0 | Some x  ket x)  1 * norm (ket x) for x
    apply (cases π x) by auto
  then have 2: norm (case π (inv ket x) of None  0 | Some x  ket x)  1 * norm x
    if x  range ket for x
    using that by auto

  show classical_operator_exists π
    unfolding classical_operator_exists_def
    using _ _ 1 2 apply (rule cblinfun_extension_exists_ortho)
    by simp_all

  show norm (classical_operator π)  1
    unfolding classical_operator_def Let_def
    using _ _ 1 2 apply (rule cblinfun_extension_exists_ortho_norm)
    by simp_all
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) C ket j = ket i C (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) C ket j = (classical_operator (inv_map π) *V ket i) C ket j"
      unfolding F_def by blast
    also have " = ((case inv_map π i of Some k  ket k | None  0) C ket j)"
      using w1 by simp
    also have " = (ket i C (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) C ket j
           = ket i C (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 C ket j) = (ket i C 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) C ket j
             = ket i C (case Some c of None  0 | Some a  ket a)"
          by simp          
        thus "(case inv_map π i of None  0 | Some a  ket a) C ket j
             = ket i C (case π j of None  0 | Some a  ket a)"
          by (simp add: Some.hyps s1)          
      qed
    qed
    also have " = ket i C (classical_operator π *V ket j)"
      by (simp add: w2)
    also have " = ket i C (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  π)"
    by (simp add: a1)
  have b0': "inj_map (inv_map (Some  π))"
    by simp
  have b1: "inv_map (Some  π) m (Some  π) = Some" 
    apply (rule ext) unfolding inv_map_def o_def 
    using assms unfolding inj_def inv_def by auto
  have b3: "classical_operator (inv_map (Some  π)) oCL
            classical_operator (Some  π) = classical_operator (inv_map (Some  π) m (Some  π))"
    by (metis b0 b0' b1 classical_operator_Some classical_operator_exists_inj 
        classical_operator_mult)
  show ?thesis
    unfolding isometry_def
    apply (subst classical_operator_adjoint)
    using b0 by (auto simp add: b1 b3)
qed

lemma unitary_classical_operator[simp]:
  fixes π::"'a  'b"
  assumes a1: "bij π"
  shows "unitary (classical_operator (Some o π))"
proof (unfold unitary_def, rule conjI)
  have "inj π"
    using a1 bij_betw_imp_inj_on by auto
  hence "isometry (classical_operator (Some o π))"
    by simp
  hence "classical_operator (Some  π)* oCL classical_operator (Some  π) = id_cblinfun"
    unfolding isometry_def by simp
  thus classical_operator (Some  π)* oCL classical_operator (Some  π) = id_cblinfun
    by simp 
next
  have "inj π"
    by (simp add: assms bij_is_inj)
  have comp: "Some  π m inv_map (Some  π) = Some"
    apply (rule ext)
    unfolding inv_map_def o_def map_comp_def
    unfolding inv_def apply auto
     apply (metis inj π inv_def inv_f_f)
    using bij_def image_iff range_eqI
    by (metis a1)
  have "classical_operator (Some  π) oCL classical_operator (Some  π)*
      = classical_operator (Some  π) oCL classical_operator (inv_map (Some  π))"
    by (simp add: inj π)
  also have " = classical_operator ((Some  π) m (inv_map (Some  π)))"
    by (simp add: inj π classical_operator_exists_inj)
  also have " = classical_operator (Some::'b_)"
    using comp
    by simp 
  also have " = (id_cblinfun:: 'b ell2 CL _)"
    by simp
  finally show "classical_operator (Some  π) oCL classical_operator (Some  π)* = id_cblinfun".
qed


unbundle no_lattice_syntax
unbundle no_cblinfun_notation

end