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

bundle cinner_bracket_notation begin
notation cinner ("_, _")
end
unbundle cinner_bracket_notation

bundle no_cinner_bracket_notation begin
no_notation cinner ("_, _")
end

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 , 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

text This is a useful rule for establishing the equality of vectors
lemma cinner_extensionality:
  assumes γ. γ, ψ = γ, φ
  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, y
    ― ‹Shown in the proof of Corollary 1.5 in @{cite conway2013course}
proof -
  have x , y + y , x = x , y + cnj x , y
    by simp
  hence x , y + y , x = 2 * Re x , y 
    using complex_add_cnj by presburger
  have x + y^2 = x+y, x+y
    by (simp add: cdot_square_norm)
  hence x + y^2 = x , x + x , y + y , x + y , y
    by (simp add: cinner_add_left cinner_add_right)
  thus ?thesis using  x , y + y , x = 2 * Re x , 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, y
proof-
  have x + (-y)^2 = x^2 + -y^2 + 2 * Re x , (-y)
    using polar_identity by blast
  hence x - y^2 = x^2 + y^2 - 2*Re x , 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 @{cite conway2013course}
  by (simp add: polar_identity_minus polar_identity)


theorem pythagorean_theorem:
  includes notation_norm
  shows x , y = 0   x + y ^2 =  x ^2 +  y ^2
    ― ‹Shown in the proof of Theorem 2.2 in @{cite conway2013course}
  by (simp add: polar_identity)

lemma pythagorean_theorem_sum:
  assumes q1: "a a'. a  t  a'  t  a  a'  f a, 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, 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, sum f F = f x, (aF. f a)"
    by simp
  also have s3: " = (aF. f x, 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, 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, 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, y i ) n -  (λ i.  x i, 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, y n  -  x m, y m  ) < e
      if n  N and m  N
      for n m
    proof -
      have  x n, y n  -  x m, y m  = ( x n, y n  -  x m, y n ) + ( x m, y n  -  x m, y m )
        by simp
      hence y1: norm ( x n, y n  -  x m, y m )  norm ( x n, y n  -  x m, y n )
           + norm ( x m, y n  -  x m, y m )
        by (metis norm_triangle_ineq)

      have  x n, y n  -  x m, y n  =  x n - x m, y n 
        by (simp add: cinner_diff_left)
      hence norm ( x n, y n  -  x m, y n ) = norm  x n - x m, y n 
        by simp
      moreover have norm  x n - x m, 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, y n  -  x m, 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, y n  -  x m, y n ) < e/2
        by simp
      hence y2: norm ( x n, y n  -  x m, y n ) < e/2
        by blast
      have  x m, y n  -  x m, y m  =  x m, y n - y m 
        by (simp add: cinner_diff_right)
      hence norm ( x m, y n  -  x m, y m ) = norm  x m, y n - y m 
        by simp
      moreover have norm  x m, 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, y n  -  x m, 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, y n  -  x m, y m ) < e/2
        by simp
      hence y3: norm ( x m, y n  -  x m, y m ) < e/2
        by blast
      show norm (  x n, y n  -  x m, 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


subsection Orthogonality


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

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

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

lemma orthogonal_complementI:
  (x. x  M   y, 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, 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 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.  y , an n  = 0
      using orthogonal_complement_orthoI'
      by (simp add: orthogonal_complement_orthoI' ortho)
    moreover have isCont (λ x.  y , 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 , v ) (an n))  (λ v.  y , v ) a for y
      using isCont_tendsto_compose
      by (simp add: isCont_tendsto_compose lim)
    hence   yA. (λ n.  y , an n   )    y , a 
      by simp
    hence   yA. (λ n. 0  )    y , a 
      using  y  A.  n.  y , an n  = 0
      by fastforce
    hence   y  A.  y , a  = 0
      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 " x, x  = 0"
      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[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


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


text Orthogonal set
definition is_ortho_set :: "'a::complex_inner set  bool" where
  is_ortho_set S = ((xS. yS. x  y  x, y = 0)  0  S)

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:  y, x  = 0
    if a1: "x  (orthogonal_complement A)"
      and a2: y  closure A
    for x y
  proof-
    have  y  A.  y , x  = 0
      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 , x ) y
      by simp
    hence (λ n.  yy n , x )    y , x 
      using yy  y isCont_tendsto_compose
      by fastforce
    hence (λ n. 0)    y , x 
      using  y  A.  y , x  = 0   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 "a, x = 0"
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: "a, i = 0"
    if "it" for i
    using b2 a1 that by blast
  have  "a, x = a, (it. r i *C i)"
    by (simp add: b3)
  also have  " = (it. r i *C a, 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).  x, y  = 0
    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 "v, v' = 0" 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, v') = 0"
      by simp
    have "v, (v't. u v' *C v') = (v't. u v' * v, v')"
      using b1
      by (metis (mono_tags, lifting) cinner_scaleC_right cinner_sum_right sum.cong)
    also have " = u v * v, v + (v't-{v}. u v' * v, v')"
      by (meson b1 b4 sum.remove)
    also have " = u v * v, v"
      using sum0 by simp
    finally have "v, (v't. u v' *C v') =  u v * v, v"
      by blast
    hence "u v * v, v = 0" using b3 by simp
    moreover have "v, 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, 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, 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, a)
      using norm_eq_sqrt_cinner by auto
    ultimately have sqrt (norm a, a) = 1
      by simp
    hence norm a, a = 1
      using real_sqrt_eq_1_iff by blast
    moreover have a, a  
      by (simp add: cinner_real)
    moreover have a, a  0
      using cinner_ge_zero by blast
    ultimately have w1: a, a = 1
      by (metis 0  a, a cmod a, a = 1 complex_of_real_cmod of_real_1)

    have r t * a, 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, t) = 0
      by (simp add: t. t  T - {a}  r t * a, t = 0)
    have a, x = a, ( tT. r t *C t)
      using x = ( aT. r a *C a)
      by simp
    also have  = ( tT. a, r t *C t)
      using cinner_sum_right by blast
    also have  = ( tT. r t * a, t)
      by simp
    also have  = r a * a, a + ( tT-{a}. r t * a, t)
      using a  T
      by (meson finite T sum.remove)
    also have  = r a * a, 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

subsection Projections

lemma smallest_norm_exists:
  ― ‹Theorem 2.5 in @{cite conway2013course} (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 , v ) = w2  w  M)  v  M"
      by (metis (no_types) power2_norm_eq_cinner')
    hence "Re (x , 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 @{cite conway2013course} (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 @{cite conway2013course}
  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 @{cite conway2013course}
  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 @{cite conway2013course}
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 , 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 , f )
      by (simp add: polar_identity_minus)
    finally have  (h - k) ^2   (h - k) ^2 +  f ^2 -  2 * Re ( h - k , f )
      by simp
    thus ?thesis by simp
  qed

  have q4:  c > 0.  2 * Re ( h - k , f )  c
    if  c>0. 2 * Re (h - k , f )  c * f2
    for f
  proof (cases  f ^2 > 0)
    case True
    hence  c > 0.  2 * Re ( h - k , 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 , f )  0
    if a3: f. f  M  (c>0. 2 * Re h - k , 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 , 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 , f )   f ^2
      using r1
      by (simp add: that)
    have  f. f   M 
                ( c::real.  2 * Re ( h - k , 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, f  f2)
    hence   f. f   M 
                ( c::real. c * (2 * Re ( h - k , 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 , f ))  ¦c¦^2* f ^2)
      by (simp add: power_mult_distrib)
    hence   f. f   M 
                ( c::real. c * (2 * Re ( h - k , f ))  c^2* f ^2)
      by auto
    hence   f. f   M 
                ( c::real. c > 0  c * (2 * Re ( h - k , f ))  c^2* f ^2)
      by simp
    hence   f. f   M 
                ( c::real. c > 0  c*(2 * Re ( h - k , f ))  c*(c* f ^2))
      by (simp add: power2_eq_square)
    hence  q4:  f. f   M 
                ( c::real. c > 0  2 * Re ( h - k , f )  c* f ^2)
      by simp
    have   f. f   M 
                ( c::real. c > 0  2 * Re ( h - k , f )  0)
      using q3
      by (simp add: q4 that)
    hence   f. f   M 
                ( c::real. c > 0  (2 * Re ( h - k , (-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 , f ))  0)
      by simp
    hence   f. f   M 
                ( c::real. c > 0  2 * Re ( h - k , f )  0)
      by simp
    hence  f. f   M 
                ( c::real. c > 0  2 * Re ( h - k , f ) = 0)
      using   f. f   M 
                ( c::real. c > 0  (2 * Re ( h - k , f ))  0)
      by fastforce

    have  f. f   M 
                 ((1::real) > 0  2 * Re ( h - k , f ) = 0)
      using f. f   M  (c>0. 2 * Re (h - k , f ) = 0) by blast
    hence  f. f   M  2 * Re ( h - k , f ) = 0
      by simp
    hence  f. f   M  Re ( h - k , f ) = 0
      by simp
    have   f. f   M  Re ( h - k , (Complex 0 (-1)) *C f ) = 0
      using assms  complex_vector.subspace_def csubspace M
      by (metis f. f  M  Re h - k, f = 0)
    hence   f. f   M  Re ( (Complex 0 (-1))*( h - k , f ) ) = 0
      by simp
    hence  f. f   M  Im ( h - k , 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 , f ) = 0
      using complex_eq_iff
      by (simp add: f. f  M  Im h - k, f = 0 f. f  M  Re h - k, 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 , 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,  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, 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