Theory Complex_Inner_Product

(*
Authors:

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

*)

section Complex_Inner_Product› -- Complex Inner Product Spaces›

theory Complex_Inner_Product
  imports
    Complex_Inner_Product0
begin

subsection ‹Complex inner product spaces›

unbundle cinner_syntax

lemma cinner_real: "cinner x x  "
  by (simp add: cdot_square_norm)

lemmas cinner_commute' [simp] = cinner_commute[symmetric]

lemma (in complex_inner) cinner_eq_flip: (cinner x y = cinner z w)  (cinner y x = cinner w z)
  by (metis cinner_commute)

lemma Im_cinner_x_x[simp]: "Im (x C x) = 0"
  using comp_Im_same[OF cinner_ge_zero] by simp


lemma of_complex_inner_1' [simp]:
  "cinner (1 :: 'a :: {complex_inner, complex_normed_algebra_1}) (of_complex x) = x"
  by (metis cinner_commute complex_cnj_cnj of_complex_inner_1)


class chilbert_space = complex_inner + complete_space
begin
subclass cbanach by standard
end

instantiation complex :: "chilbert_space" begin
instance ..
end

subsection ‹Misc facts›

lemma cinner_scaleR_left [simp]: "cinner (scaleR r x) y = of_real r * (cinner x y)"
  by (simp add: scaleR_scaleC)

lemma cinner_scaleR_right [simp]: "cinner x (scaleR r y) = of_real r * (cinner x y)"
  by (simp add: scaleR_scaleC)

text ‹This is a useful rule for establishing the equality of vectors›
lemma cinner_extensionality:
  assumes γ. γ C ψ = γ C φ
  shows ψ = φ
  by (metis assms cinner_eq_zero_iff cinner_simps(3) right_minus_eq)

lemma polar_identity:
  includes notation_norm
  shows x + y^2 = x^2 + y^2 + 2 * Re (x C y)
    ― ‹Shown in the proof of Corollary 1.5 in citeconway2013course
proof -
  have (x C y) + (y C x) = (x C y) + cnj (x C y)
    by simp
  hence (x C y) + (y C x) = 2 * Re (x C y)
    using complex_add_cnj by presburger
  have x + y^2 = (x+y) C (x+y)
    by (simp add: cdot_square_norm)
  hence x + y^2 = (x C x) + (x C y) + (y C x) + (y C y)
    by (simp add: cinner_add_left cinner_add_right)
  thus ?thesis using  (x C y) + (y C x) = 2 * Re (x C y)
    by (smt (verit, ccfv_SIG) Re_complex_of_real plus_complex.simps(1) power2_norm_eq_cinner')
qed

lemma polar_identity_minus:
  includes notation_norm
  shows x - y^2 = x^2 + y^2 - 2 * Re (x C y)
proof-
  have x + (-y)^2 = x^2 + -y^2 + 2 * Re (x C -y)
    using polar_identity by blast
  hence x - y^2 = x^2 + y^2 - 2*Re (x C y)
    by simp
  thus ?thesis
    by blast
qed

proposition parallelogram_law:
  includes notation_norm
  fixes x y :: "'a::complex_inner"
  shows x+y^2 + x-y^2 = 2*( x^2 + y^2 )
    ― ‹Shown in the proof of Theorem 2.3 in citeconway2013course
  by (simp add: polar_identity_minus polar_identity)


theorem pythagorean_theorem:
  includes notation_norm
  shows (x C y) = 0   x + y ^2 =  x ^2 +  y ^2
    ― ‹Shown in the proof of Theorem 2.2 in citeconway2013course
  by (simp add: polar_identity)

lemma pythagorean_theorem_sum:
  assumes q1: "a a'. a  t  a'  t  a  a'  f a C f a' = 0"
    and q2: "finite t"
  shows "(norm  (at. f a))^2 = (at.(norm (f a))^2)"
proof (insert q1, use q2 in induction)
  case empty
  show ?case
    by auto
next
  case (insert x F)
  have r1: "f x C f a = 0"
    if "a  F"
    for a
    using that insert.hyps(2) insert.prems by auto
  have "sum f F = (aF. f a)"
    by simp
  hence s4: "f x C sum f F = f x C (aF. f a)"
    by simp
  also have s3: " = (aF. f x C f a)"
    using cinner_sum_right by auto
  also have s2: " = (aF. 0)"
    using r1
    by simp
  also have s1: " = 0"
    by simp
  finally have xF_ortho: "f x C sum f F = 0"
    using s2 s3 by auto
  have "(norm (sum f (insert x F)))2 = (norm (f x + sum f F))2"
    by (simp add: insert.hyps(1) insert.hyps(2))
  also have " = (norm (f x))2 + (norm (sum f F))2"
    using xF_ortho by (rule pythagorean_theorem)
  also have " = (norm (f x))2 + (aF.(norm (f a))^2)"
    apply (subst insert.IH) using insert.prems by auto
  also have " = (ainsert x F.(norm (f a))^2)"
    by (simp add: insert.hyps(1) insert.hyps(2))
  finally show ?case
    by simp
qed


lemma Cauchy_cinner_Cauchy:
  fixes x y :: nat  'a::complex_inner
  assumes a1: Cauchy x and a2: Cauchy y
  shows Cauchy (λ n. x n C y n)
proof-
  have bounded (range x)
    using a1
    by (simp add: Elementary_Metric_Spaces.cauchy_imp_bounded)
  hence b1: M. n. norm (x n) < M
    by (meson bounded_pos_less rangeI)
  have bounded (range y)
    using a2
    by (simp add: Elementary_Metric_Spaces.cauchy_imp_bounded)
  hence b2:  M.  n. norm (y n) < M
    by (meson bounded_pos_less rangeI)
  have M. n. norm (x n) < M  norm (y n) < M
    using b1 b2
    by (metis dual_order.strict_trans linorder_neqE_linordered_idom)
  then obtain M where M1: n. norm (x n) < M and M2: n. norm (y n) < M
    by blast
  have M3: M > 0
    by (smt M2 norm_not_less_zero)
  have N. n  N. m  N. norm ( (λ i. x i C y i) n -  (λ i. x i C y i) m ) < e
    if "e > 0" for e
  proof-
    have e / (2*M) > 0
      using M3
      by (simp add: that)
    hence N. nN. mN. norm (x n - x m) < e / (2*M)
      using a1
      by (simp add: Cauchy_iff)
    then obtain N1 where N1_def: n m. nN1  mN1  norm (x n - x m) < e / (2*M)
      by blast
    have x1: N.  nN.  mN. norm (y n - y m) < e / (2*M)
      using a2 e / (2*M) > 0
      by (simp add: Cauchy_iff)
    obtain N2 where N2_def: n m.  nN2  mN2  norm (y n - y m) < e / (2*M)
      using x1
      by blast
    define N where N_def: N = N1 + N2
    hence N  N1
      by auto
    have N  N2
      using N_def
      by auto
    have norm (x n C y n - x m C y m) < e
      if n  N and m  N
      for n m
    proof -
      have x n C y n - x m C y m = (x n C y n - x m C y n) + (x m C y n - x m C y m)
        by simp
      hence y1: norm (x n C y n - x m C y m)  norm (x n C y n - x m C y n)
           + norm (x m C y n - x m C y m)
        by (metis norm_triangle_ineq)

      have x n C y n - x m C y n = (x n - x m) C y n
        by (simp add: cinner_diff_left)
      hence norm (x n C y n - x m C y n) = norm ((x n - x m) C y n)
        by simp
      moreover have norm ((x n - x m) C y n)  norm (x n - x m) * norm (y n)
        using complex_inner_class.Cauchy_Schwarz_ineq2 by blast
      moreover have norm (y n) < M
        by (simp add: M2)
      moreover have norm (x n - x m) < e/(2*M)
        using N  m N  n N1  N N1_def by auto
      ultimately have norm ((x n C y n) - (x m C y n)) < (e/(2*M)) * M
        by (smt linordered_semiring_strict_class.mult_strict_mono norm_ge_zero)
      moreover have (e/(2*M)) * M = e/2
        using M > 0 by simp
      ultimately have  norm ((x n C y n) - (x m C y n)) < e/2
        by simp
      hence y2: norm (x n C y n - x m C y n) < e/2
        by blast
      have x m C y n - x m C y m = x m C (y n - y m)
        by (simp add: cinner_diff_right)
      hence norm ((x m C y n) - (x m C y m)) = norm (x m C (y n - y m))
        by simp
      moreover have norm (x m C (y n - y m))  norm (x m) * norm (y n - y m)
        by (meson complex_inner_class.Cauchy_Schwarz_ineq2)
      moreover have norm (x m) < M
        by (simp add: M1)
      moreover have norm (y n - y m) < e/(2*M)
        using N  m N  n N2  N N2_def by auto
      ultimately have norm ((x m C y n) - (x m C y m)) < M * (e/(2*M))
        by (smt linordered_semiring_strict_class.mult_strict_mono norm_ge_zero)
      moreover have M * (e/(2*M)) = e/2
        using M > 0 by simp
      ultimately have  norm ((x m C y n) - (x m C y m)) < e/2
        by simp
      hence y3: norm ((x m C y n) - (x m C y m)) < e/2
        by blast
      show norm ( (x n C y n) - (x m C y m) ) < e
        using y1 y2 y3 by simp
    qed
    thus ?thesis by blast
  qed
  thus ?thesis
    by (simp add: CauchyI)
qed


lemma cinner_sup_norm: norm ψ = (SUP φ. cmod (cinner φ ψ) / norm φ)
proof (rule sym, rule cSup_eq_maximum)
  have norm ψ = cmod (cinner ψ ψ) / norm ψ
    by (metis norm_eq_sqrt_cinner norm_ge_zero real_div_sqrt)
  then show norm ψ  range (λφ. cmod (cinner φ ψ) / norm φ)
    by blast
next
  fix n assume n  range (λφ. cmod (cinner φ ψ) / norm φ)
  then obtain φ where : n = cmod (cinner φ ψ) / norm φ
    by auto
  show n  norm ψ
    unfolding 
    by (simp add: complex_inner_class.Cauchy_Schwarz_ineq2 divide_le_eq ordered_field_class.sign_simps(33))
qed

lemma cinner_sup_onorm:
  fixes A :: 'a::{real_normed_vector,not_singleton}  'b::complex_inner
  assumes bounded_linear A
  shows onorm A = (SUP (ψ,φ). cmod (cinner ψ (A φ)) / (norm ψ * norm φ))
proof (unfold onorm_def, rule cSup_eq_cSup)
  show bdd_above (range (λx. norm (A x) / norm x))
    by (meson assms bdd_aboveI2 le_onorm)
next
  fix a
  assume a  range (λφ. norm (A φ) / norm φ)
  then obtain φ where a = norm (A φ) / norm φ
    by auto
  then have a  cmod (cinner (A φ) (A φ)) / (norm (A φ) * norm φ)
    apply auto
    by (smt (verit) divide_divide_eq_left norm_eq_sqrt_cinner norm_imp_pos_and_ge real_div_sqrt)
  then show brange (λ(ψ, φ). cmod (cinner ψ (A φ)) / (norm ψ * norm φ)). a  b
    by force
next
  fix b
  assume b  range (λ(ψ, φ). cmod (cinner ψ (A φ)) / (norm ψ * norm φ))
  then obtain ψ φ where b: b = cmod (cinner ψ (A φ)) / (norm ψ * norm φ)
    by auto
  then have b  norm (A φ) / norm φ
    apply auto
    by (smt (verit, ccfv_threshold) complex_inner_class.Cauchy_Schwarz_ineq2 division_ring_divide_zero linordered_field_class.divide_right_mono mult_cancel_left1 nonzero_mult_divide_mult_cancel_left2 norm_imp_pos_and_ge ordered_field_class.sign_simps(33) zero_le_divide_iff)
  then show arange (λx. norm (A x) / norm x). b  a
    by auto
qed


lemma sum_cinner:
  fixes f :: "'a  'b::complex_inner"
  shows "cinner (sum f A) (sum g B) = (iA. jB. cinner (f i) (g j))"
  by (simp add: cinner_sum_right cinner_sum_left) (rule sum.swap)

lemma Cauchy_cinner_product_summable':
  fixes a b :: "nat  'a::complex_inner"
  shows (λ(x, y). cinner (a x) (b y)) summable_on UNIV  (λ(x, y). cinner (a y) (b (x - y))) summable_on {(k, i). i  k}
proof -
  have img: (λ(k::nat, i). (i, k - i)) ` {(k, i). i  k} = UNIV
    apply (auto simp: image_def)
    by (metis add.commute add_diff_cancel_right' diff_le_self)
  have inj: inj_on (λ(k::nat, i). (i, k - i)) {(k, i). i  k}
    by (smt (verit, del_insts) Pair_inject case_prodE case_prod_conv eq_diff_iff inj_onI mem_Collect_eq)

  have (λ(x, y). cinner (a x) (b y)) summable_on UNIV  (λ(k, l). cinner (a k) (b l)) summable_on (λ(k, i). (i, k - i)) ` {(k, i). i  k}
    by (simp only: img)
  also have   ((λ(k, l). cinner (a k) (b l))  (λ(k, i). (i, k - i))) summable_on {(k, i). i  k}
    using inj by (rule summable_on_reindex)
  also have   (λ(x, y). cinner (a y) (b (x - y))) summable_on {(k, i). i  k}
    by (simp add: o_def case_prod_unfold)
  finally show ?thesis
    by -
qed

instantiation prod :: (complex_inner, complex_inner) complex_inner
begin

definition cinner_prod_def:
  "cinner x y = cinner (fst x) (fst y) + cinner (snd x) (snd y)"

instance
proof
  fix r :: complex
  fix x y z :: "'a::complex_inner × 'b::complex_inner"
  show "cinner x y = cnj (cinner y x)"
    unfolding cinner_prod_def
    by simp
  show "cinner (x + y) z = cinner x z + cinner y z"
    unfolding cinner_prod_def
    by (simp add: cinner_add_left)
  show "cinner (scaleC r x) y = cnj r * cinner x y"
    unfolding cinner_prod_def
    by (simp add: distrib_left)
  show "0  cinner x x"
    unfolding cinner_prod_def
    by (intro add_nonneg_nonneg cinner_ge_zero)
  show "cinner x x = 0  x = 0"
    unfolding cinner_prod_def prod_eq_iff
    by (metis antisym cinner_eq_zero_iff cinner_ge_zero fst_zero le_add_same_cancel2 snd_zero verit_sum_simplify)
  show "norm x = sqrt (cmod (cinner x x))"
    unfolding norm_prod_def cinner_prod_def
    apply (simp add: norm_prod_def cinner_prod_def)
    by (metis (no_types, lifting) Complex_Inner_Product.cinner_prod_def Re_complex_of_real 0  x C x cmod_Re of_real_add of_real_power power2_norm_eq_cinner)
qed

end

lemma sgn_cinner[simp]: sgn ψ C ψ = norm ψ
  apply (cases ψ = 0)
   apply (auto simp: sgn_div_norm)
  by (metis (no_types, lifting) cdot_square_norm cinner_ge_zero cmod_Re divide_inverse mult.commute norm_eq_sqrt_cinner norm_ge_zero of_real_inverse of_real_mult power2_norm_eq_cinner' real_div_sqrt)

instance prod :: (chilbert_space, chilbert_space) chilbert_space..

subsection ‹Orthogonality›

definition "orthogonal_complement S = {x| x. yS. cinner x y = 0}"

lemma orthogonal_complement_orthoI:
  x  orthogonal_complement M  y  M  x C y = 0
  unfolding orthogonal_complement_def by auto

lemma orthogonal_complement_orthoI':
  x  M  y  orthogonal_complement M  x C y = 0
  by (metis cinner_commute' complex_cnj_zero orthogonal_complement_orthoI)

lemma orthogonal_complementI:
  (x. x  M  y C x = 0)  y  orthogonal_complement M
  unfolding orthogonal_complement_def
  by simp

abbreviation is_orthogonal::'a::complex_inner  'a  bool  where
  is_orthogonal x y  x C y = 0

bundle orthogonal_notation begin
notation is_orthogonal (infixl "" 69)
end

bundle no_orthogonal_notation begin
no_notation is_orthogonal (infixl "" 69)
end


lemma is_orthogonal_sym: "is_orthogonal ψ φ = is_orthogonal φ ψ"
  by (metis cinner_commute' complex_cnj_zero)

lemma is_orthogonal_sgn_right[simp]: is_orthogonal e (sgn f)  is_orthogonal e f
proof (cases f = 0)
  case True
  then show ?thesis
    by simp
next
  case False
  have cinner e (sgn f) = cinner e f / norm f
    by (simp add: sgn_div_norm divide_inverse scaleR_scaleC)
  moreover have norm f  0
    by (simp add: False)
  ultimately show ?thesis
    by force
qed

lemma is_orthogonal_sgn_left[simp]: is_orthogonal (sgn e) f  is_orthogonal e f
  by (simp add: is_orthogonal_sym)

lemma orthogonal_complement_closed_subspace[simp]:
  "closed_csubspace (orthogonal_complement A)"
  for A :: ('a::complex_inner) set
proof (intro closed_csubspace.intro complex_vector.subspaceI)
  fix x y and c
  show 0  orthogonal_complement A
    by (rule orthogonal_complementI, simp)
  show x + y  orthogonal_complement A
    if x  orthogonal_complement A and y  orthogonal_complement A
    using that by (auto intro!: orthogonal_complementI dest!: orthogonal_complement_orthoI
        simp add: cinner_add_left)
  show c *C x  orthogonal_complement A if x  orthogonal_complement A
    using that by (auto intro!: orthogonal_complementI dest!: orthogonal_complement_orthoI)

  show "closed (orthogonal_complement A)"
  proof (auto simp add: closed_sequential_limits, rename_tac an a)
    fix an a
    assume ortho: n::nat. an n  orthogonal_complement A
    assume lim: an  a

    have  y  A.  n. is_orthogonal y (an n)
      using orthogonal_complement_orthoI'
      by (simp add: orthogonal_complement_orthoI' ortho)
    moreover have isCont (λ x. y C x) a for y
      using bounded_clinear_cinner_right clinear_continuous_at
      by (simp add: clinear_continuous_at bounded_clinear_cinner_right)
    ultimately have (λ n. (λ v. y C v) (an n))  (λ v. y C v) a for y
      using isCont_tendsto_compose
      by (simp add: isCont_tendsto_compose lim)
    hence   yA. (λ n. y C an n)   y C a
      by simp
    hence   yA. (λ n. 0)   y C a
      using  y  A.  n. is_orthogonal y (an n)
      by fastforce
    hence   y  A. is_orthogonal y a
      using limI by fastforce
    then show a  orthogonal_complement A
      by (simp add: orthogonal_complementI is_orthogonal_sym)
  qed
qed

lemma orthogonal_complement_zero_intersection:
  assumes "0M"
  shows M  (orthogonal_complement M) = {0}
proof -
  have "x=0" if "xM" and "xorthogonal_complement M" for x
  proof -
    from that have "is_orthogonal x x"
      unfolding orthogonal_complement_def by auto
    thus "x=0"
      by auto
  qed
  with assms show ?thesis
    unfolding orthogonal_complement_def by auto
qed

lemma is_orthogonal_closure_cspan:
  assumes "x y. x  X  y  Y  is_orthogonal x y"
  assumes x  closure (cspan X) y  closure (cspan Y)
  shows "is_orthogonal x y"
proof -
  have *: cinner x y = 0 if y  Y for y
    using bounded_antilinear_cinner_left apply (rule bounded_antilinear_eq_on[where G=X])
    using assms that by auto
  show cinner x y = 0
    using bounded_clinear_cinner_right apply (rule bounded_clinear_eq_on_closure[where G=Y])
    using * assms by auto
qed


instantiation ccsubspace :: (complex_inner) "uminus"
begin
lift_definition uminus_ccsubspace::'a ccsubspace   'a ccsubspace
  is orthogonal_complement
  by simp

instance ..
end

lemma orthocomplement_top[simp]: - top = (bot :: 'a::complex_inner ccsubspace)
  ― ‹For typ'a of sort classchilbert_space, this is covered by @{thm [source] orthocomplemented_lattice_class.compl_top_eq} already.
      But here we give it a wider sort.›
  apply transfer
  by (metis Int_UNIV_left UNIV_I orthogonal_complement_zero_intersection)

instantiation ccsubspace :: (complex_inner) minus begin
lift_definition minus_ccsubspace :: "'a ccsubspace  'a ccsubspace  'a ccsubspace"
  is "λA B. A  (orthogonal_complement B)"
  by simp
instance..
end

definition is_ortho_set :: "'a::complex_inner set  bool" where
  ― ‹Orthogonal set›
  is_ortho_set S  (xS. yS. x  y  (x C y) = 0)  0  S

definition is_onb where is_onb E  is_ortho_set E  (bE. norm b = 1)  ccspan E = top

lemma is_ortho_set_empty[simp]: "is_ortho_set {}"
  unfolding is_ortho_set_def by auto

lemma is_ortho_set_antimono: A  B  is_ortho_set B  is_ortho_set A
  unfolding is_ortho_set_def by auto

lemma orthogonal_complement_of_closure:
  fixes A ::"('a::complex_inner) set"
  shows "orthogonal_complement A = orthogonal_complement (closure A)"
proof-
  have s1: is_orthogonal y x
    if a1: "x  (orthogonal_complement A)"
      and a2: y  closure A
    for x y
  proof-
    have  y  A. is_orthogonal y x
      by (simp add: a1 orthogonal_complement_orthoI')
    then obtain yy where  n. yy n  A and yy  y
      using a2 closure_sequential by blast
    have isCont (λ t. t C x) y
      by simp
    hence (λ n. yy n C x)  y C x
      using yy  y isCont_tendsto_compose
      by fastforce
    hence (λ n. 0)  y C x
      using  y  A. is_orthogonal y x   n. yy n  A by simp
    thus ?thesis
      using limI by force
  qed
  hence "x  orthogonal_complement (closure A)"
    if a1: "x  (orthogonal_complement A)"
    for x
    using that
    by (meson orthogonal_complementI is_orthogonal_sym)
  moreover have x  (orthogonal_complement A)
    if "x  (orthogonal_complement (closure A))"
    for x
    using that
    by (meson closure_subset orthogonal_complement_orthoI orthogonal_complementI subset_eq)
  ultimately show ?thesis by blast
qed


lemma is_orthogonal_closure:
  assumes s. s  S  is_orthogonal a  s
  assumes x  closure S
  shows is_orthogonal a x
  by (metis assms(1) assms(2) orthogonal_complementI orthogonal_complement_of_closure orthogonal_complement_orthoI)


lemma is_orthogonal_cspan:
  assumes a1: "s. s  S  is_orthogonal a s" and a3: "x  cspan S"
  shows "is_orthogonal a x"
proof-
  have "t r. finite t  t  S  (at. r a *C a) = x"
    using complex_vector.span_explicit
    by (smt a3 mem_Collect_eq)
  then obtain t r where b1: "finite t" and b2: "t  S" and b3: "(at. r a *C a) = x"
    by blast
  have x1: "is_orthogonal a i"
    if "it" for i
    using b2 a1 that by blast
  have  "a C x = a C (it. r i *C i)"
    by (simp add: b3)
  also have  " = (it. r i *C (a C i))"
    by (simp add: cinner_sum_right)
  also have  " = 0"
    using x1 by simp
  finally show ?thesis.
qed

lemma ccspan_leq_ortho_ccspan:
  assumes "s t. sS  tT  is_orthogonal s t"
  shows "ccspan S  - (ccspan T)"
  using assms apply transfer
  by (smt (verit, ccfv_threshold) is_orthogonal_closure is_orthogonal_cspan is_orthogonal_sym orthogonal_complementI subsetI)

lemma double_orthogonal_complement_increasing[simp]:
  shows "M  orthogonal_complement (orthogonal_complement M)"
proof (rule subsetI)
  fix x assume s1: "x  M"
  have  y  (orthogonal_complement M). is_orthogonal x y
    using s1 orthogonal_complement_orthoI' by auto
  hence x  orthogonal_complement (orthogonal_complement M)
    by (simp add: orthogonal_complement_def)
  then show "x  orthogonal_complement (orthogonal_complement M)"
    by blast
qed


lemma orthonormal_basis_of_cspan:
  fixes S::"'a::complex_inner set"
  assumes "finite S"
  shows "A. is_ortho_set A  (xA. norm x = 1)  cspan A = cspan S  finite A"
proof (use assms in induction)
  case empty
  show ?case
    apply (rule exI[of _ "{}"])
    by auto
next
  case (insert s S)
  from insert.IH
  obtain A where orthoA: "is_ortho_set A" and normA: "x. xA  norm x = 1" and spanA: "cspan A = cspan S" and finiteA: "finite A"
    by auto
  show ?case
  proof (cases s  cspan S)
    case True
    then have cspan (insert s S) = cspan S
      by (simp add: complex_vector.span_redundant)
    with orthoA normA spanA finiteA
    show ?thesis
      by auto
  next
    case False
    obtain a where a_ortho: x. xA  is_orthogonal x a and sa_span: s - a  cspan A
    proof (atomize_elim, use finite A is_ortho_set A in induction)
      case empty
      then show ?case
        by auto
    next
      case (insert x A)
      then obtain a where orthoA: x. x  A  is_orthogonal x a and sa: s - a  cspan A
        by (meson is_ortho_set_antimono subset_insertI)
      define a' where a' = a - cinner x a *C inverse (cinner x x) *C x
      have is_orthogonal x a'
        unfolding a'_def cinner_diff_right cinner_scaleC_right
        apply (cases cinner x x = 0)
        by auto
      have orthoA: is_orthogonal y a' if y  A for y
        unfolding a'_def cinner_diff_right cinner_scaleC_right
        apply auto by (metis insert.prems insertCI is_ortho_set_def mult_not_zero orthoA that)
      have s - a'  cspan (insert x A)
        unfolding a'_def apply auto
        by (metis (no_types, lifting) complex_vector.span_breakdown_eq diff_add_cancel diff_diff_add sa)
      with is_orthogonal x a' orthoA
      show ?case
        apply (rule_tac exI[of _ a'])
        by auto
    qed

    from False sa_span
    have a  0
      unfolding spanA by auto
    define a' where a' = inverse (norm a) *C a
    with a  0 have norm a' = 1
      by (simp add: norm_inverse)
    have a: a = norm a *C a'
      by (simp add: a  0 a'_def)

    from sa_span spanA
    have a'_span: a'  cspan (insert s S)
      unfolding a'_def
      by (metis complex_vector.eq_span_insert_eq complex_vector.span_scale complex_vector.span_superset in_mono insertI1)
    from sa_span
    have s_span: s  cspan (insert a' A)
      apply (subst (asm) a)
      using complex_vector.span_breakdown_eq by blast

    from a  0 a_ortho orthoA
    have ortho: "is_ortho_set (insert a' A)"
      unfolding is_ortho_set_def a'_def
      apply auto
      by (meson is_orthogonal_sym)

    have span: cspan (insert a' A) = cspan (insert s S)
      using a'_span s_span spanA apply auto
       apply (metis (full_types) complex_vector.span_breakdown_eq complex_vector.span_redundant insert_commute s_span)
      by (metis (full_types) complex_vector.span_breakdown_eq complex_vector.span_redundant insert_commute s_span)

    show ?thesis
      apply (rule exI[of _ insert a' A])
      by (simp add: ortho norm a' = 1 normA finiteA span)
  qed
qed

lemma is_ortho_set_cindependent:
  assumes "is_ortho_set A"
  shows "cindependent A"
proof -
  have "u v = 0"
    if b1: "finite t" and b2: "t  A" and b3: "(vt. u v *C v) = 0" and b4: "v  t"
    for t u v
  proof -
    have "is_orthogonal v v'" if c1: "v't-{v}" for v'
      by (metis DiffE assms b2 b4 insertI1 is_ortho_set_antimono is_ortho_set_def that)
    hence sum0: "(v't-{v}. u v' * (v C v')) = 0"
      by simp
    have "v C (v't. u v' *C v') = (v't. u v' * (v C v'))"
      using b1
      by (metis (mono_tags, lifting) cinner_scaleC_right cinner_sum_right sum.cong)
    also have " = u v * (v C v) + (v't-{v}. u v' * (v C v'))"
      by (meson b1 b4 sum.remove)
    also have " = u v * (v C v)"
      using sum0 by simp
    finally have "v C (v't. u v' *C v') =  u v * (v C v)"
      by blast
    hence "u v * (v C v) = 0" using b3 by simp
    moreover have "(v C v)  0"
      using assms is_ortho_set_def b2 b4 by auto
    ultimately show "u v = 0" by simp
  qed
  thus ?thesis using complex_vector.independent_explicit_module
    by (smt cdependent_raw_def)
qed


lemma onb_expansion_finite:
  includes notation_norm
  fixes T::'a::{complex_inner,cfinite_dim} set
  assumes a1: cspan T = UNIV and a3: is_ortho_set T
    and a4: t. tT  t = 1
  shows x = (tT. (t C x) *C t)
proof -
  have finite T
    apply (rule cindependent_cfinite_dim_finite)
    by (simp add: a3 is_ortho_set_cindependent)
  have closure (complex_vector.span T)  = complex_vector.span T
    by (simp add: a1)
  have {at. r a *C a |t r. finite t  t  T} = {aT. r a *C a |r. True}
    apply auto
     apply (rule_tac x=λa. if a  t then r a else 0 in exI)
     apply (simp add: finite T sum.mono_neutral_cong_right)
    using finite T by blast

  have f1: "A. {a. Aa f. (a::'a) = (aAa. f a *C a)  finite Aa  Aa  A} = cspan A"
    by (simp add: complex_vector.span_explicit)
  have f2: "a. (f. a = (aT. f a *C a))  (A. (f. a  (aA. f a *C a))  infinite A  ¬ A  T)"
    using {at. r a *C a |t r. finite t  t  T} = {aT. r a *C a |r. True} by auto
  have f3: "A a. (Aa f. (a::'a) = (aAa. f a *C a)  finite Aa  Aa  A)  a  cspan A"
    using f1 by blast
  have "cspan T = UNIV"
    by (metis (full_types, lifting)  complex_vector.span T = UNIV)
  hence  r. x = ( aT. r a *C a)
    using f3 f2 by blast
  then obtain r where x = ( aT. r a *C a)
    by blast

  have r a = a C x if a  T for a
  proof-
    have norm a = 1
      using a4
      by (simp add: a  T)
    moreover have norm a = sqrt (norm (a C a))
      using norm_eq_sqrt_cinner by auto
    ultimately have sqrt (norm (a C a)) = 1
      by simp
    hence norm (a C a) = 1
      using real_sqrt_eq_1_iff by blast
    moreover have (a C a)  
      by (simp add: cinner_real)
    moreover have (a C a)  0
      using cinner_ge_zero by blast
    ultimately have w1: (a C a) = 1
      using a = 1 cnorm_eq_1 by blast
    have r t * (a C t) = 0 if t  T-{a} for t
      by (metis DiffD1 DiffD2 a  T a3 is_ortho_set_def mult_eq_0_iff singletonI that)
    hence s1: ( tT-{a}. r t * (a C t)) = 0
      by (simp add: t. t  T - {a}  r t * (a C t) = 0)
    have (a C x) = a C ( tT. r t *C t)
      using x = ( aT. r a *C a)
      by simp
    also have  = ( tT. a C (r t *C t))
      using cinner_sum_right by blast
    also have  = ( tT. r t * (a C t))
      by simp
    also have  = r a * (a C a) + ( tT-{a}. r t * (a C t))
      using a  T
      by (meson finite T sum.remove)
    also have  = r a * (a C a)
      using s1
      by simp
    also have  = r a
      by (simp add: w1)
    finally show ?thesis by auto
  qed
  thus ?thesis
    using x = ( aT. r a *C a)
    by fastforce
qed

lemma is_ortho_set_singleton[simp]: is_ortho_set {x}  x  0
  by (simp add: is_ortho_set_def)

lemma orthogonal_complement_antimono[simp]:
  fixes  A B :: ('a::complex_inner) set
  assumes "A  B"
  shows orthogonal_complement A  orthogonal_complement B
  by (meson assms orthogonal_complementI orthogonal_complement_orthoI' subsetD subsetI)

lemma orthogonal_complement_UNIV[simp]:
  "orthogonal_complement UNIV = {0}"
  by (metis Int_UNIV_left complex_vector.subspace_UNIV complex_vector.subspace_def orthogonal_complement_zero_intersection)

lemma orthogonal_complement_zero[simp]:
  "orthogonal_complement {0} = UNIV"
  unfolding orthogonal_complement_def by auto

lemma mem_ortho_ccspanI:
  assumes y. y  S  is_orthogonal x y
  shows x  space_as_set (- ccspan S)
proof -
  have x  space_as_set (ccspan {x})
    using ccspan_superset by blast
  also have   space_as_set (- ccspan S)
    apply (simp add: flip: less_eq_ccsubspace.rep_eq)
    apply (rule ccspan_leq_ortho_ccspan)
    using assms by auto
  finally show ?thesis
    by -
qed


subsection ‹Projections›

lemma smallest_norm_exists:
  ― ‹Theorem 2.5 in citeconway2013course (inside the proof)›
  includes notation_norm
  fixes M :: 'a::chilbert_space set
  assumes q1: convex M and q2: closed M and q3: M  {}
  shows  k. is_arg_min (λ x. x) (λ t. t  M) k
proof -
  define d where d = Inf { x^2 | x. x  M }
  have w4: { x^2 | x. x  M }  {}
    by (simp add: assms(3))
  have  x. x^2  0
    by simp
  hence bdd_below1: bdd_below { x^2 | x. x  M }
    by fastforce
  have d  x^2 if a1: "x  M" for x
  proof-
    have "v. (w. Re (v C v) = w2  w  M)  v  M"
      by (metis (no_types) power2_norm_eq_cinner')
    hence "Re (x C x)  {v2 |v. v  M}"
      using a1 by blast
    thus ?thesis
      unfolding d_def
      by (metis (lifting) bdd_below1 cInf_lower power2_norm_eq_cinner')
  qed

  have  ε > 0.  t  { x^2 | x. x  M }.  t < d + ε
    unfolding d_def
    using w4  bdd_below1
    by (meson cInf_lessD less_add_same_cancel1)
  hence  ε > 0.  x  M.  x^2 < d + ε
    by auto
  hence  ε > 0.  x  M.  x^2 < d + ε
    by (simp add: x. x  M  d  x2)
  hence w1:  n::nat.  x  M.  x^2 < d + 1/(n+1) by auto

  then obtain r::nat  'a where w2:  n. r n  M    r n ^2 < d + 1/(n+1)
    by metis
  have w3:  n. r n  M
    by (simp add: w2)
  have  n.  r n ^2 < d + 1/(n+1)
    by (simp add: w2)
  have w5:  (r n) - (r m) ^2 < 2*(1/(n+1) + 1/(m+1))
    for m n
  proof-
    have w6:  r n ^2 < d + 1/(n+1)
      by (metis w2  of_nat_1 of_nat_add)
    have  r m ^2 < d + 1/(m+1)
      by (metis w2 of_nat_1 of_nat_add)
    have (r n)  M
      by (simp add: n. r n  M)
    moreover have (r m)  M
      by (simp add: n. r n  M)
    ultimately have (1/2) *R (r n) + (1/2) *R (r m)  M
      using convex M
      by (simp add: convexD)
    hence  (1/2) *R (r n) + (1/2) *R (r m) ^2  d
      by (simp add: x. x  M  d  x2)
    have  (1/2) *R (r n) - (1/2) *R (r m) ^2
              = (1/2)*(  r n ^2 +  r m ^2 ) -  (1/2) *R (r n) + (1/2) *R (r m) ^2
      by (smt (z3) div_by_1 field_sum_of_halves nonzero_mult_div_cancel_left parallelogram_law polar_identity power2_norm_eq_cinner' scaleR_collapse times_divide_eq_left)
    also have  ...
              < (1/2)*( d + 1/(n+1) +  r m ^2 ) -  (1/2) *R (r n) + (1/2) *R (r m) ^2
      using r n2 < d + 1 / real (n + 1) by auto
    also have  ...
              < (1/2)*( d + 1/(n+1) + d + 1/(m+1) ) -  (1/2) *R (r n) + (1/2) *R (r m) ^2
      using r m2 < d + 1 / real (m + 1) by auto
    also have  ...
               (1/2)*( d + 1/(n+1) + d + 1/(m+1) ) - d
      by (simp add: d  (1 / 2) *R r n + (1 / 2) *R r m2)
    also have  ...
               (1/2)*( 1/(n+1) + 1/(m+1) + 2*d ) - d
      by simp
    also have  ...
               (1/2)*( 1/(n+1) + 1/(m+1) ) + (1/2)*(2*d) - d
      by (simp add: distrib_left)
    also have  ...
               (1/2)*( 1/(n+1) + 1/(m+1) ) + d - d
      by simp
    also have  ...
               (1/2)*( 1/(n+1) + 1/(m+1) )
      by simp
    finally have (1 / 2) *R r n - (1 / 2) *R r m2 < 1 / 2 * (1 / real (n + 1) + 1 / real (m + 1))
      by blast
    hence (1 / 2) *R (r n - r m) 2 < (1 / 2) * (1 / real (n + 1) + 1 / real (m + 1))
      by (simp add: real_vector.scale_right_diff_distrib)
    hence ((1 / 2)* (r n - r m) )2 < (1 / 2) * (1 / real (n + 1) + 1 / real (m + 1))
      by simp
    hence (1 / 2)^2*( (r n - r m) )2 < (1 / 2) * (1 / real (n + 1) + 1 / real (m + 1))
      by (metis power_mult_distrib)
    hence (1 / 4) *( (r n - r m) )2 < (1 / 2) * (1 / real (n + 1) + 1 / real (m + 1))
      by (simp add: power_divide)
    hence  (r n - r m) 2 < 2 * (1 / real (n + 1) + 1 / real (m + 1))
      by simp
    thus ?thesis
      by (metis of_nat_1 of_nat_add)
  qed
  hence " N.  n m. n  N  m  N   (r n) - (r m) ^2 < ε^2"
    if "ε > 0"
    for ε
  proof-
    obtain N::nat where 1/(N + 1) < ε^2/4
      using LIMSEQ_ignore_initial_segment[OF lim_inverse_n', where k=1]
      by (metis Suc_eq_plus1 0 < ε nat_approx_posE zero_less_divide_iff zero_less_numeral
          zero_less_power )
    hence 4/(N + 1) < ε^2
      by simp
    have "2*(1/(n+1) + 1/(m+1)) < ε^2"
      if f1: "n  N" and f2: "m  N"
      for m n::nat
    proof-
      have 1/(n+1)  1/(N+1)
        by (simp add: f1 linordered_field_class.frac_le)
      moreover have 1/(m+1)  1/(N+1)
        by (simp add: f2 linordered_field_class.frac_le)
      ultimately have  2*(1/(n+1) + 1/(m+1))  4/(N+1)
        by simp
      thus ?thesis using 4/(N + 1) < ε^2
        by linarith
    qed
    hence " (r n) - (r m) ^2 < ε^2"
      if y1: "n  N" and y2: "m  N"
      for m n::nat
      using that
      by (smt n m. r n - r m2 < 2 * (1 / (real n + 1) + 1 / (real m + 1)) of_nat_1 of_nat_add)
    thus ?thesis
      by blast
  qed
  hence   ε > 0.  N::nat.  n m::nat. n  N  m  N   (r n) - (r m) ^2 < ε^2
    by blast
  hence   ε > 0.  N::nat.  n m::nat. n  N  m  N   (r n) - (r m)  < ε
    by (meson less_eq_real_def power_less_imp_less_base)
  hence Cauchy r
    using CauchyI by fastforce
  then obtain k where r  k
    using  convergent_eq_Cauchy by auto
  have k  M using closed M
    using n. r n  M r  k closed_sequentially by auto
  have  (λ n.   r n ^2)    k ^2
    by (simp add: r  k tendsto_norm tendsto_power)
  moreover  have  (λ n.   r n ^2)   d
  proof-
    have ¦ r n ^2 - d¦ < 1/(n+1) for n :: nat
      using x. x  M  d  x2 n. r n  M  r n2 < d + 1 / (real n + 1) of_nat_1 of_nat_add
      by smt
    moreover have (λn. 1 / real (n + 1))  0
      using  LIMSEQ_ignore_initial_segment[OF lim_inverse_n', where k=1] by blast
    ultimately have (λ n. ¦ r n ^2 - d¦ )  0
      by (simp add: LIMSEQ_norm_0)
    hence (λ n.  r n ^2 - d )  0
      by (simp add: tendsto_rabs_zero_iff)
    moreover have (λ n. d )  d
      by simp
    ultimately have (λ n. ( r n ^2 - d)+d )  0+d
      using tendsto_add by fastforce
    thus ?thesis by simp
  qed
  ultimately have d =  k ^2
    using LIMSEQ_unique by auto
  hence t  M   k ^2   t ^2 for t
    using x. x  M  d  x2 by auto
  hence q1:  k. is_arg_min (λ x. x^2) (λ t. t  M) k
    using k  M
      is_arg_min_def d = k2
    by smt
  thus  k. is_arg_min (λ x. x) (λ t. t  M) k
    by (smt is_arg_min_def norm_ge_zero power2_eq_square power2_le_imp_le)
qed


lemma smallest_norm_unique:
  ― ‹Theorem 2.5 in citeconway2013course (inside the proof)›
  includes notation_norm
  fixes M :: 'a::complex_inner set
  assumes q1: convex M
  assumes r: is_arg_min (λ x. x) (λ t. t  M) r
  assumes s: is_arg_min (λ x. x) (λ t. t  M) s
  shows r = s
proof -
  have r  M
    using is_arg_min (λx. x) (λ t. t  M) r
    by (simp add: is_arg_min_def)
  moreover have s  M
    using is_arg_min (λx. x) (λ t. t  M) s
    by (simp add: is_arg_min_def)
  ultimately have ((1/2) *R r + (1/2) *R s)  M using convex M
    by (simp add: convexD)
  hence r   (1/2) *R r + (1/2) *R s 
    by (metis is_arg_min_linorder r)
  hence u2: r^2   (1/2) *R r + (1/2) *R s ^2
    using norm_ge_zero power_mono by blast

  have r  s
    using r s is_arg_min_def
    by (metis is_arg_min_linorder)
  moreover have s  r
    using r s is_arg_min_def
    by (metis is_arg_min_linorder)
  ultimately have u3: r = s by simp

  have  (1/2) *R r - (1/2) *R s ^2  0
    using u2 u3 parallelogram_law
    by (smt (verit, ccfv_SIG) polar_identity_minus power2_norm_eq_cinner' scaleR_add_right scaleR_half_double)
  hence  (1/2) *R r - (1/2) *R s ^2 = 0
    by simp
  hence  (1/2) *R r - (1/2) *R s  = 0
    by auto
  hence (1/2) *R r - (1/2) *R s = 0
    using norm_eq_zero by blast
  thus ?thesis by simp
qed

theorem smallest_dist_exists:
  ― ‹Theorem 2.5 in citeconway2013course
  fixes M::'a::chilbert_space set and h
  assumes a1: convex M and a2: closed M and a3: M  {}
  shows  k. is_arg_min (λ x. dist x h) (λ x. x  M) k
proof -
  have *: "is_arg_min (λx. dist x h) (λx. xM) (k+h)  is_arg_min (λx. norm x) (λx. x(λx. x-h) ` M) k" for k
    unfolding dist_norm is_arg_min_def apply auto using add_implies_diff by blast
  have k. is_arg_min (λx. dist x h) (λx. xM) (k+h)
    apply (subst *)
    apply (rule smallest_norm_exists)
    using assms by (auto simp: closed_translation_subtract)
  then show k. is_arg_min (λ x. dist x h) (λ x. x  M) k
    by metis
qed

theorem smallest_dist_unique:
  ― ‹Theorem 2.5 in citeconway2013course
  fixes M::'a::complex_inner set and h
  assumes a1: convex M
  assumes is_arg_min (λ x. dist x h) (λ x. x  M) r
  assumes is_arg_min (λ x. dist x h) (λ x. x  M) s
  shows  r = s
proof-
  have *: "is_arg_min (λx. dist x h) (λx. xM) k  is_arg_min (λx. norm x) (λx. x(λx. x-h) ` M) (k-h)" for k
    unfolding dist_norm is_arg_min_def by auto
  have r - h = s - h
    using _ assms(2,3)[unfolded *] apply (rule smallest_norm_unique)
    by (simp add: a1)
  thus r = s
    by auto
qed


― ‹Theorem 2.6 in citeconway2013course
theorem smallest_dist_is_ortho:
  fixes M::'a::complex_inner set and h k::'a
  assumes b1: closed_csubspace M
  shows  (is_arg_min (λ x. dist x h) (λ x. x  M) k) 
          h - k  orthogonal_complement M  k  M
proof -
  include notation_norm
  have  csubspace M
    using closed_csubspace M unfolding closed_csubspace_def by blast
  have r1: 2 * Re ((h - k) C f)   f ^2
    if "f  M" and k  M and is_arg_min (λx. dist x h) (λ x. x  M) k
    for f
  proof-
    have k + f   M
      using csubspace M
      by (simp add:complex_vector.subspace_add that)
    have "f A a b. ¬ is_arg_min f (λ x. x  A) (a::'a)  (f a::real)  f b  b  A"
      by (metis (no_types) is_arg_min_linorder)
    hence "dist k h  dist (f + k) h"
      by (metis is_arg_min (λx. dist x h) (λ x. x  M) k k + f  M add.commute)
    hence dist h k  dist  h (k + f)
      by (simp add: add.commute dist_commute)
    hence  h - k    h - (k + f) 
      by (simp add: dist_norm)
    hence  h - k ^2   h - (k + f) ^2
      by (simp add: power_mono)
    also have ...   (h - k) - f ^2
      by (simp add: diff_diff_add)
    also have ...   (h - k) ^2 +  f ^2 -  2 * Re ((h - k) C f)
      by (simp add: polar_identity_minus)
    finally have  (h - k) ^2   (h - k) ^2 +  f ^2 -  2 * Re ((h - k) C f)
      by simp
    thus ?thesis by simp
  qed

  have q4:  c > 0.  2 * Re ((h - k) C f)  c
    if  c>0. 2 * Re ((h - k) C f)  c * f2
    for f
  proof (cases  f ^2 > 0)
    case True
    hence  c > 0.  2 * Re (((h - k) C f))  (c/ f ^2)* f ^2
      using that linordered_field_class.divide_pos_pos by blast
    thus ?thesis
      using True by auto
  next
    case False
    hence  f ^2 = 0
      by simp
    thus ?thesis
      by auto
  qed
  have q3:  c::real. c > 0  2 * Re (((h - k) C f))  0
    if a3: f. f  M  (c>0. 2 * Re ((h - k) C f)  c * f2)
      and a2: "f   M"
      and a1: "is_arg_min (λ x. dist x h) (λ x. x  M) k"
    for f
  proof-
    have  c > 0.  2 * Re (((h - k) C f))  c* f ^2
      by (simp add: that )
    thus ?thesis
      using q4 by smt
  qed
  have w2: "h - k  orthogonal_complement M  k  M"
    if a1: "is_arg_min (λ x. dist x h) (λ x. x  M) k"
  proof-
    have  k  M
      using is_arg_min_def that by fastforce
    hence  f. f   M  2 * Re (((h - k) C f))   f ^2
      using r1
      by (simp add: that)
    have  f. f   M 
                ( c::real.  2 * Re ((h - k) C (c *R f))   c *R f ^2)
      using  assms scaleR_scaleC complex_vector.subspace_def csubspace M
      by (metis f. f  M  2 * Re ((h - k) C f)  f2)
    hence   f. f   M 
                ( c::real. c * (2 * Re (((h - k) C f)))   c *R f ^2)
      by (metis Re_complex_of_real cinner_scaleC_right complex_add_cnj complex_cnj_complex_of_real
          complex_cnj_mult of_real_mult scaleR_scaleC semiring_normalization_rules(34))
    hence   f. f   M 
                ( c::real. c * (2 * Re (((h - k) C f)))  ¦c¦^2* f ^2)
      by (simp add: power_mult_distrib)
    hence   f. f   M 
                ( c::real. c * (2 * Re (((h - k) C f)))  c^2* f ^2)
      by auto
    hence   f. f   M 
                ( c::real. c > 0  c * (2 * Re (((h - k) C f)))  c^2* f ^2)
      by simp
    hence   f. f   M 
                ( c::real. c > 0  c*(2 * Re (((h - k) C f)))  c*(c* f ^2))
      by (simp add: power2_eq_square)
    hence  q4:  f. f   M 
                ( c::real. c > 0  2 * Re (((h - k) C f))  c* f ^2)
      by simp
    have   f. f   M 
                ( c::real. c > 0  2 * Re (((h - k) C f))  0)
      using q3
      by (simp add: q4 that)
    hence   f. f   M 
                ( c::real. c > 0  (2 * Re ((h - k) C (-1 *R f)))  0)
      using assms scaleR_scaleC complex_vector.subspace_def
      by (metis csubspace M)
    hence   f. f   M 
                ( c::real. c > 0  -(2 * Re (((h - k) C f)))  0)
      by simp
    hence   f. f   M 
                ( c::real. c > 0  2 * Re (((h - k) C f))  0)
      by simp
    hence  f. f   M 
                ( c::real. c > 0  2 * Re (((h - k) C f)) = 0)
      using   f. f   M 
                ( c::real. c > 0  (2 * Re (((h - k) C f)))  0)
      by fastforce

    have  f. f   M 
                 ((1::real) > 0  2 * Re (((h - k) C f)) = 0)
      using f. f   M  (c>0. 2 * Re (((h - k) C f) ) = 0) by blast
    hence  f. f   M  2 * Re (((h - k) C f)) = 0
      by simp
    hence  f. f   M  Re (((h - k) C f)) = 0
      by simp
    have   f. f   M  Re ((h - k) C ((Complex 0 (-1)) *C f)) = 0
      using assms  complex_vector.subspace_def csubspace M
      by (metis f. f  M  Re ((h - k) C f) = 0)
    hence   f. f   M  Re ( (Complex 0 (-1))*(((h - k) C f)) ) = 0
      by simp
    hence  f. f   M  Im (((h - k) C f)) = 0
      using Complex_eq_neg_1 Re_i_times cinner_scaleC_right complex_of_real_def by auto

    have  f. f   M  (((h - k) C f)) = 0
      using complex_eq_iff
      by (simp add: f. f  M  Im ((h - k) C f) = 0 f. f  M  Re ((h - k) C f) = 0)
    hence h - k  orthogonal_complement M  k  M
      by (simp add: k  M orthogonal_complementI)
    have   c. c *R f  M
      if "f  M"
      for f
      using that scaleR_scaleC  csubspace M complex_vector.subspace_def
      by (simp add: complex_vector.subspace_def scaleR_scaleC)
    have ((h - k) C f) = 0
      if "f  M"
      for f
      using h - k  orthogonal_complement M  k  M orthogonal_complement_orthoI that by auto
    hence h - k  orthogonal_complement M
      by (simp add: orthogonal_complement_def)
    thus ?thesis
      using k  M by auto
  qed

  have q1: dist h k  dist h f
    if "f  M" and  h - k  orthogonal_complement M  k  M
    for f
  proof-
    have (h - k) C (k - f) = 0
      by (metis (no_types, lifting) that
          cinner_diff_right diff_0_right orthogonal_complement_orthoI that)
    have  h - f ^2 =  (h - k) + (k - f) ^2
      by simp
    also have ... =  h - k ^2 +  k - f ^2
      using  ((h - k) C (k - f)) = 0 pythagorean_theorem by blast
    also have ...   h - k ^2
      by simp
    finally have h - k2  h - f2
      by blast
    hence h - k  h - f
      using norm_ge_zero power2_le_imp_le by blast
    thus ?thesis
      by (simp add: dist_norm)
  qed

  have  w1: "is_arg_min (λ x. dist x h) (λ x. x  M) k"
    if "h - k  orthogonal_complement M  k   M"
  proof-
    have h - k  orthogonal_complement M
      using that by blast
    have k  M using h - k  orthogonal_complement M  k   M
      by blast
    thus ?thesis
      by (metis (no_types, lifting) dist_commute is_arg_min_linorder q1 that)
  qed
  show ?thesis
    using w1 w2 by blast
qed

corollary orthog_proj_exists:
  fixes M :: 'a::chilbert_space set
  assumes closed_csubspace M
  shows  k. h - k  orthogonal_complement M  k  M
proof -
  from  closed_csubspace M
  have M  {}
    using closed_csubspace.subspace complex_vector.subspace_0 by blast
  have closed  M
    using  closed_csubspace M
    by (simp add: closed_csubspace.closed)
  have convex  M
    using  closed_csubspace M
    by (simp)
  have k.  is_arg_min (λ x. dist x h) (λ x. x  M) k
    by (simp add: smallest_dist_exists closed M convex M M  {})
  thus ?thesis
    by (simp add: assms smallest_dist_is_ortho)
qed

corollary orthog_proj_unique:
  fixes M :: 'a::complex_inner set
  assumes closed_csubspace M
  assumes h - r  orthogonal_complement M  r  M
  assumes h - s  orthogonal_complement M  s  M
  shows  r = s
  using _ assms(2,3) unfolding smallest_dist_is_ortho[OF assms(1), symmetric]
  apply (rule smallest_dist_unique)
  using assms(1) by (simp)

definition is_projection_on::('a  'a)  ('a::metric_space) set  bool where
  is_projection_on π M  (h. is_arg_min (λ x. dist x h) (λ x. x  M) (π h))

lemma is_projection_on_iff_orthog:
  closed_csubspace M  is_projection_on π M  (h. h - π h  orthogonal_complement M  π h  M)
  by (simp add: is_projection_on_def smallest_dist_is_ortho)

lemma is_projection_on_exists:
  fixes M :: 'a::chilbert_space set
  assumes convex M and closed M and M  {}
  shows "π. is_projection_on π M"
  unfolding is_projection_on_def apply (rule choice)
  using smallest_dist_exists[OF assms] by auto

lemma is_projection_on_unique:
  fixes M :: 'a::complex_inner set
  assumes convex M
  assumes "is_projection_on π1 M"
  assumes "is_projection_on π2 M"
  shows "π1 = π2"
  using smallest_dist_unique[OF assms(1)] using assms(2,3)
  unfolding is_projection_on_def by blast

definition projection :: 'a::metric_space set  ('a  'a) where
  projection M = (SOME π. is_projection_on π M)

lemma projection_is_projection_on:
  fixes M :: 'a::chilbert_space set
  assumes convex M and closed M and M  {}
  shows "is_projection_on (projection M) M"
  by (metis assms(1) assms(2) assms(3) is_projection_on_exists projection_def someI)

lemma projection_is_projection_on'[simp]:
  ― ‹Common special case of @{thm projection_is_projection_on}
  fixes M :: 'a::chilbert_space set
  assumes closed_csubspace M
  shows "is_projection_on (projection M) M"
  apply (rule projection_is_projection_on)
    apply (auto simp add: assms closed_csubspace.closed)
  using assms closed_csubspace.subspace complex_vector.subspace_0 by blast

lemma projection_orthogonal:
  fixes M :: 'a::chilbert_space set
  assumes "closed_csubspace M" and m  M
  shows is_orthogonal (h - projection M h) m
  by (metis assms(1) assms(2) closed_csubspace.closed closed_csubspace.subspace csubspace_is_convex empty_iff is_projection_on_iff_orthog orthogonal_complement_orthoI projection_is_projection_on)

lemma is_projection_on_in_image:
  assumes "is_projection_on π M"
  shows "π h  M"
  using assms
  by (simp add: is_arg_min_def is_projection_on_def)

lemma is_projection_on_image:
  assumes "is_projection_on π M"
  shows "range π = M"
  using assms
  apply (auto simp: is_projection_on_in_image)
  by (smt (verit, ccfv_threshold) dist_pos_lt dist_self is_arg_min_def is_projection_on_def rangeI)

lemma projection_in_image[simp]:
  fixes M :: 'a::chilbert_space set
  assumes convex M and closed M and M  {}
  shows projection M h  M
  by (simp add: assms(1) assms(2) assms(3) is_projection_on_in_image projection_is_projection_on)

lemma projection_image[simp]:
  fixes M :: 'a::chilbert_space set
  assumes convex M and closed M and M  {}
  shows range (projection M) = M
  by (simp add: assms(1) assms(2) assms(3) is_projection_on_image projection_is_projection_on)

lemma projection_eqI':
  fixes M :: 'a::complex_inner set
  assumes convex M
  assumes is_projection_on f M
  shows projection M = f
  by (metis assms(1) assms(2) is_projection_on_unique projection_def someI_ex)

lemma is_projection_on_eqI:
  fixes  M :: 'a::complex_inner set
  assumes a1: closed_csubspace M and a2: h - x  orthogonal_complement M and a3: x  M
    and a4: is_projection_on π M
  shows π h = x
  by (meson a1 a2 a3 a4 closed_csubspace.subspace csubspace_is_convex is_projection_on_def smallest_dist_is_ortho smallest_dist_unique)

lemma projection_eqI:
  fixes  M :: ('a::chilbert_space) set
  assumes  closed_csubspace M and h - x  orthogonal_complement M and x  M
  shows projection M h = x
  by (metis assms(1) assms(2) assms(3) is_projection_on_iff_orthog orthog_proj_exists projection_def is_projection_on_eqI tfl_some)

lemma is_projection_on_fixes_image:
  fixes M :: 'a::metric_space set
  assumes a1: "is_projection_on π M" and a3: "x  M"
  shows "π x = x"
  by (metis a1 a3 dist_pos_lt dist_self is_arg_min_def is_projection_on_def)

lemma projection_fixes_image:
  fixes M :: ('a::chilbert_space) set
  assumes "closed_csubspace M" and "x  M"
  shows "projection M x = x"
  using is_projection_on_fixes_image
    ― ‹Theorem 2.7 in citeconway2013course
  by (simp add: assms complex_vector.subspace_0 projection_eqI)

lemma is_projection_on_closed:
  assumes cont_f: x. x  closure M  isCont f x
  assumes is_projection_on f M
  shows closed M
proof -
  have x  M if s  x and range s  M for s x
  proof -
    from is_projection_on f M range s  M
    have s = (f o s)
      by (simp add: comp_def is_projection_on_fixes_image range_subsetD)
    also from cont_f s  x 
    have (f o s)  f x
      apply (rule continuous_imp_tendsto)
      using s  x range s  M
      by (meson closure_sequential range_subsetD)
    finally have x = f x
      using s  x
      by (simp add: LIMSEQ_unique)
    then have x  range f
      by simp
    with is_projection_on f M show x  M
      by (simp add: is_projection_on_image)
  qed
  then show ?thesis
    by (metis closed_sequential_limits image_subset_iff)
qed

proposition is_projection_on_reduces_norm:
  includes notation_norm
  fixes M :: ('a::complex_inner) set
  assumes is_projection_on π M and closed_csubspace M
  shows  π  h    h 
proof-
  have h - π h  orthogonal_complement M
    using assms is_projection_on_iff_orthog by blast
  hence  k  M. is_orthogonal (h - π h) k
    using orthogonal_complement_orthoI by blast
  also have π h   M
    using is_projection_on π M
    by (simp add: is_projection_on_in_image)
  ultimately have is_orthogonal (h - π h) (π h)
    by auto
  hence  π h ^2 +  h - π h ^2 =  h ^2
    using pythagorean_theorem by fastforce
  hence π h ^2   h ^2
    by (smt zero_le_power2)
  thus ?thesis
    using norm_ge_zero power2_le_imp_le by blast
qed

proposition projection_reduces_norm:
  includes notation_norm
  fixes M :: 'a::chilbert_space set
  assumes a1: "closed_csubspace M"
  shows  projection M h    h 
  using assms is_projection_on_iff_orthog orthog_proj_exists is_projection_on_reduces_norm projection_eqI by blast

― ‹Theorem 2.7 (version) in citeconway2013course
theorem is_projection_on_bounded_clinear:
  fixes M :: 'a::complex_inner set
  assumes a1: "is_projection_on π M" and a2: "closed_csubspace M"
  shows "bounded_clinear π"
proof
  have b1:  csubspace (orthogonal_complement M)
    by (simp add: a2)
  have f1: "a. a - π a  orthogonal_complement M  π a  M"
    using a1 a2 is_projection_on_iff_orthog by blast
  hence "c *C x - c *C π x  orthogonal_complement M"
    for c x
    by (metis (no_types) b1
        add_diff_cancel_right' complex_vector.subspace_def diff_add_cancel scaleC_add_right)
  thus r1: π (c *C x) = c *C (π x) for x c
    using f1 by (meson a2 a1 closed_csubspace.subspace
        complex_vector.subspace_def is_projection_on_eqI)
  show r2: π (x + y) =  (π x) + (π y)
    for x y
  proof-
    have "A. ¬ closed_csubspace (A::'a set)  csubspace A"
      by (metis closed_csubspace.subspace)
    hence "csubspace M"
      using a2 by auto
    hence π (x + y) - ( (π x) + (π y) )  M
      by (simp add: complex_vector.subspace_add complex_vector.subspace_diff f1)
    have closed_csubspace (orthogonal_complement M)
      using a2
      by simp
    have f1: "a b. (b::'a) + (a - b) = a"
      by (metis add.commute diff_add_cancel)
    have f2: "a b. (b::'a) - b = a - a"
      by auto
    hence f3: "a. a - a  orthogonal_complement M"
      by (simp add: complex_vector.subspace_0)
    have "a b. (a  orthogonal_complement M  a + b  orthogonal_complement M)
              b  orthogonal_complement M"
      using add_diff_cancel_right' b1 complex_vector.subspace_diff
      by metis
    hence "a b c. (a  orthogonal_complement M  c - (b + a)  orthogonal_complement M)
               c - b  orthogonal_complement M"
      using f1 by (metis diff_diff_add)
    hence f4: "a b f. (f a - b  orthogonal_complement M  a - b  orthogonal_complement M)
               ¬ is_projection_on f M"
      using f1
      by (metis a2 is_projection_on_iff_orthog)
    have f5: "a b c d. (d::'a) - (c + (b - a)) = d + (a - (b + c))"
      by auto
    have "x - π x  orthogonal_complement M"
      using a1 a2 is_projection_on_iff_orthog by blast
    hence q1: π (x + y) - ( (π x) + (π y) )  orthogonal_complement M
      using f5 f4 f3 by (metis csubspace (orthogonal_complement M)
          is_projection_on π M add_diff_eq complex_vector.subspace_diff diff_diff_add
          diff_diff_eq2)
    hence π (x + y) - ( (π x) + (π y) )  M  (orthogonal_complement M)
      by (simp add: π (x + y) - (π x + π y)  M)
    moreover have M  (orthogonal_complement M) = {0}
      by (simp add: closed_csubspace M complex_vector.subspace_0 orthogonal_complement_zero_intersection)
    ultimately have π (x + y) - ( (π x) + (π y) ) = 0
      by auto
    thus ?thesis by simp
  qed
  from is_projection_on_reduces_norm
  show t1:  K.  x. norm (π x)  norm x * K
    by (metis a1 a2 mult.left_neutral ordered_field_class.sign_simps(5))
qed

theorem projection_bounded_clinear:
  fixes M :: ('a::chilbert_space) set
  assumes a1: "closed_csubspace M"
  shows bounded_clinear (projection M)
    ― ‹Theorem 2.7 in citeconway2013course
  using assms is_projection_on_iff_orthog orthog_proj_exists is_projection_on_bounded_clinear projection_eqI by blast

proposition is_projection_on_idem:
  fixes M :: ('a::complex_inner) set
  assumes "is_projection_on π M"
  shows "π (π x) = π x"
  using is_projection_on_fixes_image is_projection_on_in_image assms by blast

proposition projection_idem:
  fixes M :: "'a::chilbert_space set"
  assumes a1: "closed_csubspace M"
  shows "projection M (projection M x) = projection M x"
  by (metis assms closed_csubspace.closed closed_csubspace.subspace complex_vector.subspace_0 csubspace_is_convex equals0D projection_fixes_image projection_in_image)


proposition is_projection_on_kernel_is_orthogonal_complement:
  fixes M :: 'a::complex_inner set
  assumes a1: "is_projection_on π M" and a2: "closed_csubspace M"
  shows "π -` {0} = orthogonal_complement M"
proof-
  have "x  (π -` {0})"
    if "x  orthogonal_complement M"
    for x
    by (smt (verit, ccfv_SIG) a1 a2 closed_csubspace_def complex_vector.subspace_def complex_vector.subspace_diff is_projection_on_eqI orthogonal_complement_closed_subspace that vimage_singleton_eq)
  moreover have "x  orthogonal_complement M"
    if s1: "x  π -` {0}" for x
    by (metis a1 a2 diff_zero is_projection_on_iff_orthog that vimage_singleton_eq)
  ultimately show ?thesis
    by blast
qed

― ‹Theorem 2.7 in citeconway2013course
proposition projection_kernel_is_orthogonal_complement:
  fixes M :: 'a::chilbert_space set
  assumes "closed_csubspace M"
  shows "(projection M) -` {0} = (orthogonal_complement M)"
  by (metis assms closed_csubspace_def complex_vector.subspace_def csubspace_is_convex insert_absorb insert_not_empty is_projection_on_kernel_is_orthogonal_complement projection_is_projection_on)

lemma is_projection_on_id_minus:
  fixes M :: 'a::complex_inner set
  assumes is_proj: "is_projection_on π M"
    and cc: "closed_csubspace M"
  shows "is_projection_on (id - π) (orthogonal_complement M)"
  using is_proj apply (simp add: cc is_projection_on_iff_orthog)
  using double_orthogonal_complement_increasing by blast


text ‹Exercise 2 (section 2, chapter I) in  citeconway2013course
lemma projection_on_orthogonal_complement[simp]:
  fixes M :: "'a::chilbert_space set"
  assumes a1: "closed_csubspace M"
  shows "projection (orthogonal_complement M) = id - projection M"
  apply (auto intro!: ext)
  by (smt (verit, ccfv_SIG) add_diff_cancel_left' assms closed_csubspace.closed closed_csubspace.subspace complex_vector.subspace_0 csubspace_is_convex diff_add_cancel double_orthogonal_complement_increasing insert_absorb insert_not_empty is_projection_on_iff_orthog orthogonal_complement_closed_subspace projection_eqI projection_is_projection_on subset_eq)

lemma is_projection_on_zero:
  "is_projection_on (λ_. 0) {0}"
  by (simp add: is_projection_on_def is_arg_min_def)

lemma projection_zero[simp]:
  "projection {0} = (λ_. 0)"
  using is_projection_on_zero
  by (metis (full_types) is_projection_on_in_image projection_def singletonD someI_ex)

lemma is_projection_on_rank1:
  fixes t :: 'a::complex_inner
  shows is_projection_on (λx. ((t C x) / (t C t)) *C t) (cspan {t})
proof (cases t = 0)
  case True
  then show ?thesis
    by (simp add: is_projection_on_zero)
next
  case False
  define P where P x = ((t C x) / (t C t)) *C t for x
  define t' where t' = t /C norm t
  with False have norm t' = 1
    by (simp add: norm_inverse)
  have P_def': P x = cinner t' x *C t' for x
    unfolding P_def t'_def apply auto
    by (metis divide_divide_eq_left divide_inverse mult.commute power2_eq_square power2_norm_eq_cinner)
  have spant': cspan {t} = cspan {t'}
    by (simp add: False t'_def)
  have cc: closed_csubspace (cspan {t})
    by (auto intro!: finite_cspan_closed closed_csubspace.intro)
  have ortho: h - P h  orthogonal_complement (cspan {t}) for h
    unfolding orthogonal_complement_def P_def' spant' apply auto
    by (smt (verit, ccfv_threshold) norm t' = 1 add_cancel_right_left cinner_add_right cinner_commute' cinner_scaleC_right cnorm_eq_1 complex_vector.span_breakdown_eq complex_vector.span_empty diff_add_cancel mult_cancel_left1 singletonD)
  have inspan: P h  cspan {t} for h
    unfolding P_def' spant'
    by (simp add: complex_vector.span_base complex_vector.span_scale)
  show is_projection_on P (cspan {t})
    apply (subst is_projection_on_iff_orthog)
    using cc ortho inspan by auto
qed

lemma projection_rank1:
  fixes t x :: 'a::complex_inner
  shows projection (cspan {t}) x = ((t C x) / (t C t)) *C t
  apply (rule fun_cong, rule projection_eqI', simp)
  by (rule is_projection_on_rank1)

subsection ‹More orthogonal complement›

text ‹The following lemmas logically fit into the "orthogonality" section but depend on projections for their proofs.›

text ‹Corollary 2.8 in citeconway2013course
theorem double_orthogonal_complement_id[simp]:
  fixes M :: 'a::chilbert_space set
  assumes a1: "closed_csubspace M"
  shows "orthogonal_complement (orthogonal_complement M) = M"
proof-
  have b2: "x  (id - projection M) -` {0}"
    if c1: "x  M" for x
    by (simp add: assms projection_fixes_image that)

  have b3: x  M
    if c1: x  (id - projection M) -` {0} for x
    by (metis assms closed_csubspace.closed closed_csubspace.subspace complex_vector.subspace_0 csubspace_is_convex eq_id_iff equals0D fun_diff_def projection_in_image right_minus_eq that vimage_singleton_eq)
  have x   M  x  (id - projection M) -` {0} for x
    using b2 b3 by blast
  hence b4: ( id - (projection M) ) -` {0} =  M
    by blast
  have b1: "orthogonal_complement (orthogonal_complement M)
          = (projection (orthogonal_complement M)) -` {0}"
    by (simp add: a1 projection_kernel_is_orthogonal_complement del: projection_on_orthogonal_complement)
  also have ... = ( id - (projection M) ) -` {0}
    by (simp add: a1)
  also have ... = M
    by (simp add: b4)
  finally show ?thesis by blast
qed

lemma orthogonal_complement_antimono_iff[simp]:
  fixes  A B :: ('a::chilbert_space) set
  assumes closed_csubspace A and  closed_csubspace B
  shows orthogonal_complement A  orthogonal_complement B  A  B
proof (rule iffI)
  show orthogonal_complement A  orthogonal_complement B if A  B
    using that by auto

  assume orthogonal_complement A  orthogonal_complement B
  then have orthogonal_complement (orthogonal_complement A)  orthogonal_complement (orthogonal_complement B)
    by simp
  then show A  B
    using assms by auto
qed

lemma de_morgan_orthogonal_complement_plus:
  fixes A B::"('a::complex_inner) set"
  assumes 0  A and 0  B
  shows orthogonal_complement (A +M B) = orthogonal_complement A  orthogonal_complement B
proof -
  have "x  (orthogonal_complement A)  (orthogonal_complement B)"
    if "x  orthogonal_complement (A +M B)" for x
  proof -
    have orthogonal_complement (A +M B) = orthogonal_complement (A + B)
      unfolding closed_sum_def by (subst orthogonal_complement_of_closure[symmetric], simp)
    hence x  orthogonal_complement (A + B)
      using that by blast
    hence t1: z  (A + B). (z C x) = 0
      by (simp add: orthogonal_complement_orthoI')
    have A  A + B
      using subset_iff add.commute set_zero_plus2 0  B
      by fastforce
    hence z  A. (z C x) = 0
      using t1 by auto
    hence w1: x  (orthogonal_complement A)
      by (smt mem_Collect_eq is_orthogonal_sym orthogonal_complement_def)
    have B  A + B
      using 0  A subset_iff set_zero_plus2 by blast
    hence  z  B. (z C x) = 0
      using t1 by auto
    hence x  (orthogonal_complement B)
      by (smt mem_Collect_eq is_orthogonal_sym orthogonal_complement_def)
    thus ?thesis
      using w1 by auto
  qed
  moreover have "x  (orthogonal_complement (A +M B))"
    if v1: "x  (orthogonal_complement A)  (orthogonal_complement B)"
    for x
  proof-
    have x  (orthogonal_complement A)
      using v1
      by blast
    hence y A. (y C x) = 0
      by (simp add: orthogonal_complement_orthoI')
    have x  (orthogonal_complement B)
      using v1
      by blast
    hence  y B. (y C x) = 0
      by (simp add: orthogonal_complement_orthoI')
    have  aA.  bB. (a+b) C x = 0
      by (simp add: yA. y C x = 0 yB. (y C x) = 0 cinner_add_left)
    hence  y  (A + B). y C x = 0
      using set_plus_elim by force
    hence x  (orthogonal_complement (A + B))
      by (smt mem_Collect_eq is_orthogonal_sym orthogonal_complement_def)
    moreover have (orthogonal_complement (A + B)) = (orthogonal_complement (A +M B))
      unfolding closed_sum_def by (subst orthogonal_complement_of_closure[symmetric], simp)
    ultimately have x  (orthogonal_complement (A +M B))
      by blast
    thus ?thesis
      by blast
  qed
  ultimately show ?thesis by blast
qed

lemma de_morgan_orthogonal_complement_inter:
  fixes A B::"'a::chilbert_space set"
  assumes a1: closed_csubspace A and a2: closed_csubspace B
  shows  orthogonal_complement (A  B) = orthogonal_complement A +M orthogonal_complement B
proof-
  have orthogonal_complement A +M orthogonal_complement B
    = orthogonal_complement (orthogonal_complement (orthogonal_complement A +M orthogonal_complement B))
    by (simp add: closed_subspace_closed_sum)
  also have  = orthogonal_complement (orthogonal_complement (orthogonal_complement A)  orthogonal_complement (orthogonal_complement B))
    by (simp add: de_morgan_orthogonal_complement_plus orthogonal_complementI)
  also have  = orthogonal_complement (A  B)
    by (simp add: a1 a2)
  finally show ?thesis
    by simp
qed

lemma orthogonal_complement_of_cspan: orthogonal_complement A = orthogonal_complement (cspan A)
  by (metis (no_types, opaque_lifting) closed_csubspace.subspace complex_vector.span_minimal complex_vector.span_superset double_orthogonal_complement_increasing orthogonal_complement_antimono orthogonal_complement_closed_subspace subset_antisym)

lemma orthogonal_complement_orthogonal_complement_closure_cspan:
  orthogonal_complement (orthogonal_complement S) = closure (cspan S) for S :: 'a::chilbert_space set
proof -
  have orthogonal_complement (orthogonal_complement S) = orthogonal_complement (orthogonal_complement (closure (cspan S)))
    by (simp flip: orthogonal_complement_of_closure orthogonal_complement_of_cspan)
  also have  = closure (cspan S)
    by simp
  finally show orthogonal_complement (orthogonal_complement S) = closure (cspan S)
    by -
qed

instance ccsubspace :: (chilbert_space) complete_orthomodular_lattice
proof
  fix X Y :: 'a ccsubspace

  show "inf X (- X) = bot"
    apply transfer
    by (simp add: closed_csubspace_def complex_vector.subspace_0 orthogonal_complement_zero_intersection)

  have t  M +M orthogonal_complement M
    if closed_csubspace M for t::'a and M
    by (metis (no_types, lifting) UNIV_I closed_csubspace.subspace complex_vector.subspace_def de_morgan_orthogonal_complement_inter double_orthogonal_complement_id orthogonal_complement_closed_subspace orthogonal_complement_zero orthogonal_complement_zero_intersection that)
  hence b1: M +M orthogonal_complement M = UNIV
    if closed_csubspace M for M :: 'a set
    using that by blast
  show "sup X (- X) = top"
    apply transfer
    using b1 by auto
  show "- (- X) = X"
    apply transfer by simp

  show "- Y  - X"
    if "X  Y"
    using that apply transfer by simp

  have c1: "M +M orthogonal_complement M  N  N"
    if "closed_csubspace M" and "closed_csubspace N" and "M  N"
    for M N :: "'a set"
    using that
    by (simp add: closed_sum_is_sup)

  have c2: u  M +M (orthogonal_complement M  N)
    if a1: "closed_csubspace M" and a2: "closed_csubspace N" and a3: "M  N" and x1: u  N
    for M :: "'a set" and N :: "'a set"  and u
  proof -
    have d4: (projection M) u  M
      by (metis a1 closed_csubspace_def csubspace_is_convex equals0D orthog_proj_exists projection_in_image)
    hence d2: (projection M) u  N
      using a3 by auto
    have d1: csubspace N
      by (simp add: a2)
    have u - (projection M) u  orthogonal_complement M
      by (simp add: a1 orthogonal_complementI projection_orthogonal)
    moreover have  u - (projection M) u  N
      by (simp add: d1 d2 complex_vector.subspace_diff x1)
    ultimately have d3: u - (projection M) u  ((orthogonal_complement M)  N)
      by simp
    hence  v  ((orthogonal_complement M)  N). u = (projection M) u + v
      by (metis d3 diff_add_cancel ordered_field_class.sign_simps(2))
    then obtain v where v  ((orthogonal_complement M)  N) and u = (projection M) u + v
      by blast
    hence u  M + ((orthogonal_complement M)  N)
      by (metis d4 set_plus_intro)
    thus ?thesis
      unfolding closed_sum_def
      using closure_subset by blast
  qed

  have c3: "N  M +M ((orthogonal_complement M)  N)"
    if "closed_csubspace M" and "closed_csubspace N" and "M  N"
    for M N :: "'a set"
    using c2 that by auto

  show "sup X (inf (- X) Y) = Y"
    if "X  Y"
    using that apply transfer
    using c1 c3
    by (simp add: subset_antisym)

  show "X - Y = inf X (- Y)"
    apply transfer by simp
qed

subsection ‹Orthogonal spaces›

definition orthogonal_spaces S T  (xspace_as_set S. yspace_as_set T. is_orthogonal x y)

lemma orthogonal_spaces_leq_compl: orthogonal_spaces S T  S  -T
  unfolding orthogonal_spaces_def apply transfer
  by (auto simp: orthogonal_complement_def)

lemma orthogonal_bot[simp]: orthogonal_spaces S bot
  by (simp add: orthogonal_spaces_def)

lemma orthogonal_spaces_sym: orthogonal_spaces S T  orthogonal_spaces T S
  unfolding orthogonal_spaces_def
  using is_orthogonal_sym by blast

lemma orthogonal_sup: orthogonal_spaces S T1  orthogonal_spaces S T2  orthogonal_spaces S (sup T1 T2)
  apply (rule orthogonal_spaces_sym)
  apply (simp add: orthogonal_spaces_leq_compl)
  using orthogonal_spaces_leq_compl orthogonal_spaces_sym by blast

lemma orthogonal_sum:
  assumes finite F and x. xF  orthogonal_spaces S (T x) 
  shows orthogonal_spaces S (sum T F)
  using assms
  apply induction
  by (auto intro!: orthogonal_sup)

lemma orthogonal_spaces_ccspan: (xS. yT. is_orthogonal x y)  orthogonal_spaces (ccspan S) (ccspan T)
  by (meson ccspan_leq_ortho_ccspan ccspan_superset orthogonal_spaces_def orthogonal_spaces_leq_compl subset_iff)

subsection ‹Orthonormal bases›

lemma ortho_basis_exists: 
  fixes S :: 'a::chilbert_space set
  assumes is_ortho_set S
  shows B. B  S  is_ortho_set B  closure (cspan B) = UNIV
proof -
  define on where on B  B  S  is_ortho_set B for B :: 'a set
  have BCollect on. B'Collect on. B  B'  B' = B
  proof (rule subset_Zorn_nonempty; simp)
    show S. on S
      apply (rule exI[of _ S])
      using assms on_def by fastforce
  next
    fix C :: 'a set set
    assume C  {}
    assume subset.chain (Collect on) C
    then have C_on: B  C  on B and C_order: B  C  B'  C  B  B'  B'  B for B B'
      by (auto simp: subset.chain_def)
    have is_orthogonal x y if xC yC x  y for x y
      by (smt (verit) UnionE C_order C_on on_def is_ortho_set_def subsetD that(1) that(2) that(3))
    moreover have 0   C
      by (meson UnionE C_on is_ortho_set_def on_def)
    moreover have C  S
      using C_on C  {} on_def by blast
    ultimately show on ( C)
      unfolding on_def is_ortho_set_def by simp
  qed
  then obtain B where on B and B_max: B'  B  on B'  B=B' for B'
    by auto
  have ψ = 0 if ψortho: bB. is_orthogonal ψ b for ψ :: 'a
  proof (rule ccontr)
    assume ψ  0
    define φ B' where φ = ψ /R norm ψ and B' = B  {φ}
    have [simp]: norm φ = 1
      using ψ  0 by (auto simp: φ_def)
    have φortho: is_orthogonal φ b if b  B for b
      using ψortho that φ_def  by auto
    have orthoB': is_orthogonal x y if xB' yB' x  y for x y
      using that on B φortho φortho[THEN is_orthogonal_sym[THEN iffD1]]
      by (auto simp: B'_def on_def is_ortho_set_def)
    have B'0: 0  B'
      using B'_def norm φ = 1 on B is_ortho_set_def on_def by fastforce
    have S  B'
      using B'_def on B on_def by auto
    from orthoB' B'0 S  B' have on B'
      by (simp add: on_def is_ortho_set_def)
    with B_max have B = B'
      by (metis B'_def Un_upper1)
    then have φ  B
      using B'_def by blast
    then have is_orthogonal φ φ
      using φortho by blast
    then show False
      using B'0 B = B' φ  B by fastforce
  qed 
  then have orthogonal_complement B = {0}
    by (auto simp: orthogonal_complement_def)
  then have UNIV = orthogonal_complement (orthogonal_complement B)
    by simp
  also have  = orthogonal_complement (orthogonal_complement (closure (cspan B)))
    by (metis (mono_tags, opaque_lifting) orthogonal_complement B = {0} cinner_zero_left complex_vector.span_superset empty_iff insert_iff orthogonal_complementI orthogonal_complement_antimono orthogonal_complement_of_closure subsetI subset_antisym)
  also have  = closure (cspan B)
    apply (rule double_orthogonal_complement_id)
    by simp
  finally have closure (cspan B) = UNIV
    by simp
  with on B show ?thesis
    by (auto simp: on_def)
qed

lemma orthonormal_basis_exists: 
  fixes S :: 'a::chilbert_space set
  assumes is_ortho_set S and x. xS  norm x = 1
  shows B. B  S  is_onb B
proof -
  from is_ortho_set S
  obtain B where is_ortho_set B and B  S and closure (cspan B) = UNIV
    using ortho_basis_exists by blast
  define B' where B' = (λx. x /R norm x) ` B
  have S = (λx. x /R norm x) ` S
    by (simp add: assms(2))
  then have B'  S
    using B'_def S  B by blast
  moreover 
  have ccspan B' = top
    apply (transfer fixing: B')
    apply (simp add: B'_def scaleR_scaleC)
    apply (subst complex_vector.span_image_scale')
    using is_ortho_set B closure (cspan B) = UNIV is_ortho_set_def 
    by auto
  moreover have is_ortho_set B'
    using is_ortho_set B by (auto simp: B'_def is_ortho_set_def)
  moreover have bB'. norm b = 1
    using is_ortho_set B apply (auto simp: B'_def is_ortho_set_def)
    by (metis field_class.field_inverse norm_eq_zero)
  ultimately show ?thesis
    by (auto simp: is_onb_def)
qed


definition some_chilbert_basis :: 'a::chilbert_space set where
  some_chilbert_basis = (SOME B::'a set. is_onb B)

lemma is_onb_some_chilbert_basis[simp]: is_onb (some_chilbert_basis :: 'a::chilbert_space set)
  using orthonormal_basis_exists[OF is_ortho_set_empty]
  by (auto simp add: some_chilbert_basis_def intro: someI2)

lemma is_ortho_set_some_chilbert_basis[simp]: is_ortho_set some_chilbert_basis
  using is_onb_def is_onb_some_chilbert_basis by blast

lemma is_normal_some_chilbert_basis: x. x  some_chilbert_basis  norm x = 1
  using is_onb_def is_onb_some_chilbert_basis by blast

lemma ccspan_some_chilbert_basis[simp]: ccspan some_chilbert_basis = top
  using is_onb_def is_onb_some_chilbert_basis by blast

lemma span_some_chilbert_basis[simp]: closure (cspan some_chilbert_basis) = UNIV
  by (metis ccspan.rep_eq ccspan_some_chilbert_basis top_ccsubspace.rep_eq)

lemma cindependent_some_chilbert_basis[simp]: cindependent some_chilbert_basis
  using is_ortho_set_cindependent is_ortho_set_some_chilbert_basis by blast

lemma finite_some_chilbert_basis[simp]: finite (some_chilbert_basis :: 'a :: {chilbert_space, cfinite_dim} set)
  apply (rule cindependent_cfinite_dim_finite)
  by simp

lemma some_chilbert_basis_nonempty: (some_chilbert_basis :: 'a::{chilbert_space, not_singleton} set)  {}
proof (rule ccontr, simp)
  define B :: 'a set where B = some_chilbert_basis
  assume [simp]: B = {}
  have UNIV = closure (cspan B)
    using B_def span_some_chilbert_basis by blast
  also have  = {0}
    by simp
  also have   UNIV
    using Extra_General.UNIV_not_singleton by blast
  finally show False
    by simp
qed

lemma basis_projections_reconstruct_has_sum:
  assumes is_ortho_set B and normB: b. bB  norm b = 1 and ψB: ψ  space_as_set (ccspan B)
  shows ((λb. (b C ψ) *C b) has_sum ψ) B
proof (rule has_sumI_metric)
  fix e :: real assume e > 0
  define e2 where e2 = e/2
  have [simp]: e2 > 0
    by (simp add: 0 < e e2_def)
  define bb where bb φ b = (b C φ) *C b for φ and b :: 'a
  have linear_bb: clinear (λφ. bb φ b) for b
    by (simp add: bb_def cinner_add_right clinear_iff scaleC_left.add)
  from ψB obtain φ where distφψ: dist φ ψ < e2 and φB: φ  cspan B
    apply atomize_elim apply (simp add: ccspan.rep_eq closure_approachable)
    using 0 < e2 by blast
  from φB obtain F where finite F and F  B and φF: φ  cspan F
    by (meson vector_finitely_spanned)
  have dist (sum (bb ψ) G) ψ < e 
    if finite G and F  G and G  B for G
  proof -
    have sumφ: sum (bb φ) G = φ
    proof -
      from φF F  G have φG: φ  cspan G
        using complex_vector.span_mono by blast
      then obtain f where φsum: φ = (bG. f b *C b)
        using complex_vector.span_finite[OF finite G] 
        by auto
      have sum (bb φ) G = (cG. bG. bb (f b *C b) c)
        apply (simp add: φsum)
        apply (rule sum.cong, simp)
        apply (rule complex_vector.linear_sum[where f=λx. bb x _])
        by (rule linear_bb)
      also have  = ((c,b)G×G. bb (f b *C b) c)
        by (simp add: sum.cartesian_product)
      also have  = (bG. f b *C b)
        apply (rule sym)
        apply (rule sum.reindex_bij_witness_not_neutral
            [where j=λb. (b,b) and i=fst and T'=G×G - (λb. (b,b)) ` G and S'={}])
        using finite G apply (auto simp: bb_def)
         apply (metis (no_types, lifting) assms(1) imageI is_ortho_set_antimono is_ortho_set_def that(3))
        using normB G  B cnorm_eq_1 by blast
      also have  = φ
        by (simp flip: φsum)
      finally show ?thesis
        by -
    qed
    have dist (sum (bb φ) G) (sum (bb ψ) G) < e2
    proof -
      define γ where γ = φ - ψ
      have (dist (sum (bb φ) G) (sum (bb ψ) G))2 = (norm (sum (bb γ) G))2
        by (simp add: dist_norm γ_def complex_vector.linear_diff[OF linear_bb] sum_subtractf)
      also have  = (norm (sum (bb γ) G))2 + (norm (γ - sum (bb γ) G))2 - (norm (γ - sum (bb γ) G))2
        by simp
      also have  = (norm (sum (bb γ) G + (γ - sum (bb γ) G)))2 - (norm (γ - sum (bb γ) G))2
      proof -
        have (bG. bb γ b C bb γ c) = bb γ c C γ if c  G for c
          apply (subst sum_single[where i=c])
          using that apply (auto intro!: finite G simp: bb_def)
           apply (metis G  B is_ortho_set B is_ortho_set_antimono is_ortho_set_def)
          using G  B normB cnorm_eq_1 by blast
        then have is_orthogonal (sum (bb γ) G) (γ - sum (bb γ) G)
          by (simp add: cinner_sum_left cinner_diff_right cinner_sum_right)
        then show ?thesis
          apply (rule_tac arg_cong[where f=λx. x - _])
          by (rule pythagorean_theorem[symmetric])
      qed
      also have  = (norm γ)2 - (norm (γ - sum (bb γ) G))2
        by simp
      also have   (norm γ)2
        by simp
      also have  = (dist φ ψ)2
        by (simp add: γ_def dist_norm)
      also have  < e22
        using distφψ apply (rule power_strict_mono)
        by auto
      finally show ?thesis
        by (smt (verit) 0 < e2 power_mono)
    qed
    with sumφ distφψ show dist (sum (bb ψ) G) ψ < e
      apply (rule_tac dist_triangle_lt[where z=φ])
      by (simp add: e2_def dist_commute)
  qed
  with finite F and F  B 
  show F. finite F 
             F  B  (G. finite G  F  G  G  B  dist (sum (bb ψ) G) ψ < e)
    by (auto intro!: exI[of _ F])
qed

lemma basis_projections_reconstruct:
  assumes is_ortho_set B and b. bB  norm b = 1 and ψ  space_as_set (ccspan B)
  shows (bB. (b C ψ) *C b) = ψ
  using assms basis_projections_reconstruct_has_sum infsumI by blast

lemma basis_projections_reconstruct_summable:
  assumes is_ortho_set B and b. bB  norm b = 1 and ψ  space_as_set (ccspan B)
  shows (λb. (b C ψ) *C b) summable_on B
  by (simp add: assms basis_projections_reconstruct basis_projections_reconstruct_has_sum summable_iff_has_sum_infsum)

lemma parseval_identity_has_sum:
  assumes is_ortho_set B and normB: b. bB  norm b = 1 and ψ  space_as_set (ccspan B)
  shows ((λb. (norm (b C ψ))2) has_sum (norm ψ)2) B
proof -
  have *: (λv. (norm v)2) (bF. (b C ψ) *C b) = (bF. (norm (b C ψ))2) if finite F and F  B for F
    apply (subst pythagorean_theorem_sum)
    using is_ortho_set B normB that
      apply (auto intro!: sum.cong[OF refl] simp: is_ortho_set_def)
    by blast
  
  from assms have ((λb. (b C ψ) *C b) has_sum ψ) B
    by (simp add: basis_projections_reconstruct_has_sum)
  then have ((λF. bF. (b C ψ) *C b)  ψ) (finite_subsets_at_top B)
    by (simp add: has_sum_def)
  then have ((λF. (λv. (norm v)2) (bF. (b C ψ) *C b))  (norm ψ)2) (finite_subsets_at_top B)
    apply (rule isCont_tendsto_compose[rotated])
    by simp
  then have ((λF. (bF. (norm (b C ψ))2))  (norm ψ)2) (finite_subsets_at_top B)
    apply (rule tendsto_cong[THEN iffD2, rotated])
    apply (rule eventually_finite_subsets_at_top_weakI)
    by (simp add: *)
  then show ((λb. (norm (b C ψ))2) has_sum (norm ψ)2) B
    by (simp add: has_sum_def)
qed

lemma parseval_identity_summable:
  assumes is_ortho_set B and b. bB  norm b = 1 and ψ  space_as_set (ccspan B)
  shows (λb. (norm (b C ψ))2) summable_on B
  using parseval_identity_has_sum[OF assms] has_sum_imp_summable by blast

lemma parseval_identity:
  assumes is_ortho_set B and b. bB  norm b = 1 and ψ  space_as_set (ccspan B)
  shows (bB. (norm (b C ψ))2) = (norm ψ)2
  using parseval_identity_has_sum[OF assms]
  using infsumI by blast


subsection ‹Riesz-representation theorem›

lemma orthogonal_complement_kernel_functional:
  fixes f :: 'a::complex_inner  complex
  assumes bounded_clinear f
  shows x. orthogonal_complement (f -` {0}) = cspan {x}
proof (cases orthogonal_complement (f -` {0}) = {0})
  case True
  then show ?thesis
    apply (rule_tac x=0 in exI) by auto
next
  case False
  then obtain x where xortho: x  orthogonal_complement (f -` {0}) and xnon0: x  0
    using complex_vector.subspace_def by fastforce

  from xnon0 xortho
  have r1: f x  0
    by (metis cinner_eq_zero_iff orthogonal_complement_orthoI vimage_singleton_eq)

  have  k. y = k *C x if y  orthogonal_complement (f -` {0}) for y
  proof (cases y = 0)
    case True
    then show ?thesis by auto
  next
    case False
    with that
    have f y  0
      by (metis cinner_eq_zero_iff orthogonal_complement_orthoI vimage_singleton_eq)
    then obtain k where k_def: f x = k * f y
      by (metis add.inverse_inverse minus_divide_eq_eq)
    with assms have f x = f (k *C y)
      by (simp add: bounded_clinear.axioms(1) clinear.scaleC)
    hence f x - f (k *C y) = 0
      by simp
    with assms have s1: f (x - k *C y) = 0
      by (simp add: bounded_clinear.axioms(1) complex_vector.linear_diff)
    from that have k *C y  orthogonal_complement (f -` {0})
      by (simp add: complex_vector.subspace_scale)
    with xortho have s2: x - (k *C y)  orthogonal_complement (f -` {0})
      by (simp add: complex_vector.subspace_diff)
    have s3: (x - (k *C y))  f -` {0}
      using s1 by simp
    moreover have (f -` {0})  (orthogonal_complement (f -` {0})) = {0}
      by (meson assms closed_csubspace_def complex_vector.subspace_def kernel_is_closed_csubspace
          orthogonal_complement_zero_intersection)
    ultimately have x - (k *C y) = 0
      using s2 by blast
    thus ?thesis
      by (metis ceq_vector_fraction_iff eq_iff_diff_eq_0 k_def r1 scaleC_scaleC)
  qed
  then have orthogonal_complement (f -` {0})  cspan {x}
    using complex_vector.span_superset complex_vector.subspace_scale by blast

  moreover from xortho have orthogonal_complement (f -` {0})  cspan {x}
    by (simp add: complex_vector.span_minimal)

  ultimately show ?thesis
    by auto
qed

lemma riesz_representation_existence:
  ― ‹Theorem 3.4 in citeconway2013course
  fixes f::'a::chilbert_space  complex
  assumes a1: bounded_clinear f
  shows t. x.  f x = t C x
proof(cases  x. f x = 0)
  case True
  thus ?thesis
    by (metis cinner_zero_left)
next
  case False
  obtain t where spant: orthogonal_complement (f -` {0}) = cspan {t}
    using orthogonal_complement_kernel_functional
    using assms by blast
  have projection (orthogonal_complement (f -` {0})) x = ((t C x)/(t C t)) *C t for x
    apply (subst spant) by (rule projection_rank1)
  hence f (projection (orthogonal_complement (f -` {0})) x) = (((t C x))/(t C t)) * (f t) for x
    using a1 unfolding bounded_clinear_def
    by (simp add: complex_vector.linear_scale)
  hence l2: f (projection (orthogonal_complement (f -` {0})) x) = ((cnj (f t)/(t C t)) *C t) C x for x
    using complex_cnj_divide by force
  have f (projection (f -` {0}) x) = 0 for x
    by (metis (no_types, lifting) assms bounded_clinear_def closed_csubspace.closed
        complex_vector.linear_subspace_vimage complex_vector.subspace_0 complex_vector.subspace_single_0
        csubspace_is_convex insert_absorb insert_not_empty kernel_is_closed_csubspace projection_in_image vimage_singleton_eq)
  hence "a b. f (projection (f -` {0}) a + b) = 0 + f b"
    using additive.add assms
    by (simp add: bounded_clinear_def complex_vector.linear_add)
  hence "a. 0 + f (projection (orthogonal_complement (f -` {0})) a) = f a"
    apply (simp add: assms)
    by (metis add.commute diff_add_cancel)
  hence f x = ((cnj (f t)/(t C t)) *C t) C x for x
    by (simp add: l2)
  thus ?thesis
    by blast
qed

lemma riesz_representation_unique:
  ― ‹Theorem 3.4 in citeconway2013course
  fixes f::'a::complex_inner  complex
  assumes x. f x = (t C x)
  assumes x. f x = (u C x)
  shows t = u
  by (metis add_diff_cancel_left' assms(1) assms(2) cinner_diff_left cinner_gt_zero_iff diff_add_cancel diff_zero)

subsection ‹Adjoints›

definition "is_cadjoint F G  (x. y. (F x C y) = (x C G y))"

lemma is_adjoint_sym:
  is_cadjoint F G  is_cadjoint G F
  unfolding is_cadjoint_def apply auto
  by (metis cinner_commute')

definition cadjoint G = (SOME F. is_cadjoint F G)
  for G :: "'b::complex_inner  'a::complex_inner"

lemma cadjoint_exists:
  fixes G :: "'b::chilbert_space  'a::complex_inner"
  assumes [simp]: bounded_clinear G
  shows F. is_cadjoint F G
proof -
  include notation_norm
  have [simp]: clinear G
    using assms unfolding bounded_clinear_def by blast
  define g :: 'a  'b  complex
    where g x y = (x C G y) for x y
  have bounded_clinear (g x) for x
  proof -
    have g x (a + b) = g x a + g x b for a b
      unfolding g_def
      using additive.add cinner_add_right clinear_def
      by (simp add: cinner_add_right complex_vector.linear_add)
    moreover have  g x (k *C a) = k *C (g x a)
      for a k
      unfolding g_def
      by (simp add: complex_vector.linear_scale)
    ultimately have clinear (g x)
      by (simp add: clinearI)
    moreover
    have  M.  y.  G y    y  * M
      using bounded_clinear G
      unfolding bounded_clinear_def bounded_clinear_axioms_def by blast
    then have M. y.  g x y    y  * M
      using g_def
      by (simp add: bounded_clinear.bounded bounded_clinear_cinner_right_comp)
    ultimately show ?thesis unfolding bounded_linear_def
      using bounded_clinear.intro
      using bounded_clinear_axioms_def by blast
  qed
  hence x. t. y.  g x y = (t C y)
    using riesz_representation_existence by blast
  then obtain F where x. y. g x y = (F x C y)
    by metis
  then have is_cadjoint F G
    unfolding is_cadjoint_def g_def by simp
  thus ?thesis
    by auto
qed

lemma cadjoint_is_cadjoint[simp]:
  fixes G :: "'b::chilbert_space  'a::complex_inner"
  assumes [simp]: bounded_clinear G
  shows is_cadjoint (cadjoint G) G
  by (metis assms cadjoint_def cadjoint_exists someI_ex)

lemma is_cadjoint_unique:
  assumes is_cadjoint F1 G
  assumes is_cadjoint F2 G
  shows F1 = F2
  by (metis (full_types) assms(1) assms(2) ext is_cadjoint_def riesz_representation_unique)

lemma cadjoint_univ_prop:
  fixes G :: "'b::chilbert_space  'a::complex_inner"
  assumes a1: bounded_clinear G
  shows cadjoint G x C y = x C G y
  using assms cadjoint_is_cadjoint is_cadjoint_def by blast

lemma cadjoint_univ_prop':
  fixes G :: "'b::chilbert_space  'a::complex_inner"
  assumes a1: bounded_clinear G
  shows x C cadjoint G y = G x C y
  by (metis cadjoint_univ_prop assms cinner_commute')

notation cadjoint ("_" [99] 100)

lemma cadjoint_eqI:
  fixes G:: 'b::complex_inner  'a::complex_inner
    and F:: 'a  'b
  assumes x y. (F x C y) = (x C G y)
  shows G = F
  by (metis assms cadjoint_def is_cadjoint_def is_cadjoint_unique someI_ex)

lemma cadjoint_bounded_clinear:
  fixes A :: "'a::chilbert_space  'b::complex_inner"
  assumes a1: "bounded_clinear A"
  shows bounded_clinear (A)
proof
  include notation_norm
  have b1: ((A) x C y) = (x C A y) for x y
    using cadjoint_univ_prop a1 by auto
  have is_orthogonal ((A) (x1 + x2) - ((A) x1 + (A) x2)) y for x1 x2 y
    by (simp add: b1 cinner_diff_left cinner_add_left)
  hence b2: (A) (x1 + x2) - ((A) x1 + (A) x2) = 0 for x1 x2
    using cinner_eq_zero_iff by blast
  thus z1: (A) (x1 + x2) = (A) x1 + (A) x2 for x1 x2
    by (simp add: b2 eq_iff_diff_eq_0)

  have f1: is_orthogonal ((A) (r *C x) - (r *C (A) x )) y for r x y
    by (simp add: b1 cinner_diff_left)
  thus z2: (A) (r *C x) = r *C (A) x for r x
    using cinner_eq_zero_iff eq_iff_diff_eq_0 by blast
  have  (A) x ^2 = ((A) x C (A) x) for x
    by (metis cnorm_eq_square)
  moreover have  (A) x ^2  0 for x
    by simp
  ultimately have  (A) x ^2 = ¦ ((A) x C (A) x) ¦ for x
    by (metis abs_pos cinner_ge_zero)
  hence  (A) x ^2 = ¦ (x C A ((A) x)) ¦ for x
    by (simp add: b1)
  moreover have  ¦(x C A ((A) x))¦  x *  A ((A) x) for x
    by (simp add: abs_complex_def complex_inner_class.Cauchy_Schwarz_ineq2 less_eq_complex_def)
  ultimately have b5:  (A) x ^2   x * A ((A) x) for x
    by (metis complex_of_real_mono_iff)
  have M. M  0  ( x. A ((A) x)  M *  (A) x)
    using a1
    by (metis (mono_tags, opaque_lifting) bounded_clinear.bounded linear mult_nonneg_nonpos
        mult_zero_right norm_ge_zero order.trans semiring_normalization_rules(7))
  then obtain M where q1: M  0 and q2:  x. A ((A) x)  M * (A) x
    by blast
  have  x::'b. x  0
    by simp
  hence b6: x * A ((A) x)   x * M * (A) x for x
    using q2
    by (smt ordered_comm_semiring_class.comm_mult_left_mono vector_space_over_itself.scale_scale)
  have z3:  (A) x   x * M for x
  proof(cases (A) x = 0)
    case True
    thus ?thesis
      by (simp add: 0  M)
  next
    case False
    have  (A) x ^2  x *  M *  (A) x
      by (smt b5 b6)
    thus ?thesis
      by (smt False mult_right_cancel mult_right_mono norm_ge_zero semiring_normalization_rules(29))
  qed
  thus K. x. (A) x  x * K
    by auto
qed

proposition double_cadjoint:
  fixes U :: 'a::chilbert_space  'b::complex_inner
  assumes a1: "bounded_clinear U"
  shows "U = U"
  by (metis assms cadjoint_def cadjoint_is_cadjoint is_adjoint_sym is_cadjoint_unique someI_ex)

lemma cadjoint_id[simp]: id = id
  by (simp add: cadjoint_eqI id_def)

lemma scaleC_cadjoint:
  fixes A::"'a::chilbert_space  'b::complex_inner"
  assumes "bounded_clinear A"
  shows (λt. a *C A t) = (λs. cnj a *C (A) s)
proof -
  have b3: ((λ s. (cnj a) *C ((A) s)) x C y) = (x C (λ t. a *C (A t)) y)
    for x y
    by (simp add: assms cadjoint_univ_prop)

  have "((λt. a *C A t)) b = cnj a *C (A) b"
    for b::'b
  proof-
    have "bounded_clinear (λt. a *C A t)"
      by (simp add: assms bounded_clinear_const_scaleC)
    thus ?thesis
      by (metis (no_types) cadjoint_eqI b3)
  qed
  thus ?thesis
    by blast
qed


lemma is_projection_on_is_cadjoint:
  fixes M :: 'a::complex_inner set
  assumes a1: is_projection_on π M and a2: closed_csubspace M
  shows is_cadjoint π π
  by (smt (verit, ccfv_threshold) a1 a2 cinner_diff_left cinner_eq_flip is_cadjoint_def is_projection_on_iff_orthog orthogonal_complement_orthoI right_minus_eq)

lemma is_projection_on_cadjoint:
  fixes M :: 'a::complex_inner set
  assumes is_projection_on π M and closed_csubspace M
  shows π = π
  using assms is_projection_on_is_cadjoint cadjoint_eqI is_cadjoint_def by blast

lemma projection_cadjoint:
  fixes M :: 'a::chilbert_space set
  assumes closed_csubspace M
  shows (projection M) = projection M
  using is_projection_on_cadjoint assms
  by (metis closed_csubspace.closed closed_csubspace.subspace csubspace_is_convex empty_iff orthog_proj_exists projection_is_projection_on)


subsection ‹More projections›

text ‹These lemmas logically belong in the "projections" section above but depend on lemmas developed later.›

lemma is_projection_on_plus:
  assumes "x y. x  A  y  B  is_orthogonal x y"
  assumes closed_csubspace A
  assumes closed_csubspace B
  assumes is_projection_on πA A
  assumes is_projection_on πB B
  shows is_projection_on (λx. πA x + πB x) (A +M B)
proof (rule is_projection_on_iff_orthog[THEN iffD2, rule_format])
  show clAB: closed_csubspace (A +M B)
    by (simp add: assms(2) assms(3) closed_subspace_closed_sum)
  fix h
  have 1: πA h + πB h  A +M B
    by (meson clAB assms(2) assms(3) assms(4) assms(5) closed_csubspace_def closed_sum_left_subset closed_sum_right_subset complex_vector.subspace_def in_mono is_projection_on_in_image)

  have πA (πB h) = 0
    by (smt (verit, del_insts) assms(1) assms(2) assms(4) assms(5) cinner_eq_zero_iff is_cadjoint_def is_projection_on_in_image is_projection_on_is_cadjoint)
  then have h - (πA h + πB h) = (h - πB h) - πA (h - πB h)
    by (smt (verit) add.right_neutral add_diff_cancel_left' assms(2) assms(4) closed_csubspace.subspace complex_vector.subspace_diff diff_add_eq_diff_diff_swap diff_diff_add is_projection_on_iff_orthog orthog_proj_unique orthogonal_complement_closed_subspace)
  also have   orthogonal_complement A
    using assms(2) assms(4) is_projection_on_iff_orthog by blast
  finally have orthoA: h - (πA h + πB h)  orthogonal_complement A
    by -

  have πB (πA h) = 0
    by (smt (verit, del_insts) assms(1) assms(3) assms(4) assms(5) cinner_eq_zero_iff is_cadjoint_def is_projection_on_in_image is_projection_on_is_cadjoint)
  then have h - (πA h + πB h) = (h - πA h) - πB (h - πA h)
    by (smt (verit) add.right_neutral add_diff_cancel assms(3) assms(5) closed_csubspace.subspace complex_vector.subspace_diff diff_add_eq_diff_diff_swap diff_diff_add is_projection_on_iff_orthog orthog_proj_unique orthogonal_complement_closed_subspace)
  also have   orthogonal_complement B
    using assms(3) assms(5) is_projection_on_iff_orthog by blast
  finally have orthoB: h - (πA h + πB h)  orthogonal_complement B
    by -

  from orthoA orthoB
  have 2: h - (πA h + πB h)  orthogonal_complement (A +M B)
    by (metis IntI assms(2) assms(3) closed_csubspace_def complex_vector.subspace_def de_morgan_orthogonal_complement_plus)

  from 1 2 show h - (πA h + πB h)  orthogonal_complement (A +M B)  πA h + πB h  A +M B
    by simp
qed

lemma projection_plus:
  fixes A B :: "'a::chilbert_space set"
  assumes "x y. x:A  y:B  is_orthogonal x y"
  assumes closed_csubspace A
  assumes closed_csubspace B
  shows projection (A +M B) = (λx. projection A x + projection B x)
proof -
  have is_projection_on (λx. projection A x + projection B x) (A +M B)
    apply (rule is_projection_on_plus)
    using assms by auto
  then show ?thesis
    by (meson assms(2) assms(3) closed_csubspace.subspace closed_subspace_closed_sum csubspace_is_convex projection_eqI')
qed

lemma is_projection_on_insert:
  assumes ortho: "s. s  S  is_orthogonal a s"
  assumes is_projection_on π (closure (cspan S))
  assumes is_projection_on πa (cspan {a})
  shows "is_projection_on (λx. πa x + π x) (closure (cspan (insert a S)))"
proof -
  from ortho
  have x  cspan {a}  y  closure (cspan S)  is_orthogonal x y for x y
    using is_orthogonal_cspan is_orthogonal_closure is_orthogonal_sym
    by (smt (verit, ccfv_threshold) empty_iff insert_iff)
  then have is_projection_on (λx. πa x + π x) (cspan {a} +M closure (cspan S))
    apply (rule is_projection_on_plus)
    using assms by (auto simp add: closed_csubspace.intro)
  also have  = closure (cspan (insert a S))
    using closed_sum_cspan[where X={a}] by simp
  finally show ?thesis
    by -
qed

lemma projection_insert:
  fixes a :: 'a::chilbert_space
  assumes a1: "s. s  S  is_orthogonal a s"
  shows "projection (closure (cspan (insert a S))) u
        = projection (cspan {a}) u + projection (closure (cspan S)) u"
  using is_projection_on_insert[where S=S, OF a1]
  by (metis (no_types, lifting) closed_closure closed_csubspace.intro closure_is_csubspace complex_vector.subspace_span csubspace_is_convex finite.intros(1) finite.intros(2) finite_cspan_closed_csubspace projection_eqI' projection_is_projection_on')

lemma projection_insert_finite:
  fixes S :: 'a::chilbert_space set
  assumes a1: "s. s  S  is_orthogonal a s" and a2: "finite S"
  shows "projection (cspan (insert a S)) u
        = projection (cspan {a}) u + projection (cspan S) u"
  using projection_insert
  by (metis a1 a2 closure_finite_cspan finite.insertI)

subsection ‹Canonical basis (onb_enum›)›

setup Sign.add_const_constraint (const_nameis_ortho_set, SOME typ'a set  bool)

class onb_enum = basis_enum + complex_inner +
  assumes is_orthonormal: "is_ortho_set (set canonical_basis)"
    and is_normal: "x. x  (set canonical_basis)  norm x = 1"

setup Sign.add_const_constraint (const_nameis_ortho_set, SOME typ'a::complex_inner set  bool)

lemma cinner_canonical_basis:
  assumes i < length (canonical_basis :: 'a::onb_enum list)
  assumes j < length (canonical_basis :: 'a::onb_enum list)
  shows cinner (canonical_basis!i :: 'a) (canonical_basis!j) = (if i=j then 1 else 0)
  by (metis assms(1) assms(2) distinct_canonical_basis is_normal is_ortho_set_def is_orthonormal nth_eq_iff_index_eq nth_mem of_real_1 power2_norm_eq_cinner power_one)

lemma canonical_basis_is_onb[simp]: is_onb (set canonical_basis :: 'a::onb_enum set)
  by (simp add: is_normal is_onb_def is_orthonormal)

instance onb_enum  chilbert_space
proof
  have complete (UNIV :: 'a set)
    using finite_cspan_complete[where B=set canonical_basis]
    by simp
  then show "convergent X" if "Cauchy X" for X :: "nat  'a"
    by (simp add: complete_def convergent_def that)
qed

subsection ‹Conjugate space›

instantiation conjugate_space :: (complex_inner) complex_inner begin
lift_definition cinner_conjugate_space :: "'a conjugate_space  'a conjugate_space  complex" is
  λx y. cinner y x.
instance
  apply (intro_classes; transfer)
       apply (simp_all add: )
    apply (simp add: cinner_add_right)
  using cinner_ge_zero norm_eq_sqrt_cinner by auto
end

instance conjugate_space :: (chilbert_space) chilbert_space..

subsection ‹Misc (ctd.)›


lemma separating_dense_span: 
  assumes F G :: 'a::chilbert_space  'b::{complex_normed_vector,not_singleton}. 
           bounded_clinear F  bounded_clinear G  (xS. F x = G x)  F = G
  shows closure (cspan S) = UNIV
proof -
  have ψ = 0 if ψ  orthogonal_complement S for ψ
  proof -
    obtain φ :: 'b where φ  0
      by fastforce
    have (λx. cinner ψ x *C φ) = (λ_. 0) 
      apply (rule assms[rule_format])
      using orthogonal_complement_orthoI that
      by (auto simp add: bounded_clinear_cinner_right bounded_clinear_scaleC_const)
    then have cinner ψ ψ = 0
      by (meson φ  0 scaleC_eq_0_iff)
    then show ψ = 0
      by auto
  qed
  then have orthogonal_complement (orthogonal_complement S) = UNIV
    by (metis UNIV_eq_I cinner_zero_right orthogonal_complementI)
  then show closure (cspan S) = UNIV
    by (simp add: orthogonal_complement_orthogonal_complement_closure_cspan)
qed

end