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 \<^cite>‹conway2013course››
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 \<^cite>‹conway2013course››
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 \<^cite>‹conway2013course››
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  (∑a∈t. f a))^2 = (∑a∈t.(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 = (∑a∈F. f a)"
by simp
hence s4: "f x ∙⇩C sum f F = f x ∙⇩C (∑a∈F. f a)"
by simp
also have s3: "… = (∑a∈F. f x ∙⇩C f a)"
using cinner_sum_right by auto
also have s2: "… = (∑a∈F. 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 + (∑a∈F.(norm (f a))^2)"
apply (subst insert.IH) using insert.prems by auto
also have "… = (∑a∈insert 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. ∀n≥N. ∀m≥N. norm (x n - x m) < e / (2*M)›
using a1
by (simp add: Cauchy_iff)
then obtain N1 where N1_def: ‹⋀n m. n≥N1 ⟹ m≥N1 ⟹ norm (x n - x m) < e / (2*M)›
by blast
have x1: ‹∃N. ∀ n≥N. ∀ m≥N. 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.  n≥N2 ⟹ m≥N2 ⟹ 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φ: ‹n = cmod (cinner φ ψ) / norm φ›
by auto
show ‹n ≤ norm ψ›
unfolding nφ
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 ‹∃b∈range (λ(ψ, φ). 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 ‹∃a∈range (λ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) = (∑i∈A. ∑j∈B. 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. ∀y∈S. 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  ‹∀ y∈A. (λ n. y ∙⇩C an n) ⇢  y ∙⇩C a›
by simp
hence  ‹∀ y∈A. (λ 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 "0∈M"
shows ‹M ∩ (orthogonal_complement M) = {0}›
proof -
have "x=0" if "x∈M" and "x∈orthogonal_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 \<^class>‹chilbert_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 ⟷ (∀x∈S. ∀y∈S. x ≠ y ⟶ (x ∙⇩C y) = 0) ∧ 0 ∉ S›

definition is_onb where ‹is_onb E ⟷ is_ortho_set E ∧ (∀b∈E. 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 ∧ (∑a∈t. 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: "(∑a∈t. r a *⇩C a) = x"
by blast
have x1: "is_orthogonal a i"
if "i∈t" for i
using b2 a1 that by blast
have  "a ∙⇩C x = a ∙⇩C (∑i∈t. r i *⇩C i)"
by (simp add: b3)
also have  "… = (∑i∈t. 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. s∈S ⟹ t∈T ⟹ 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 ∧ (∀x∈A. 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. x∈A ⟹ 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. x∈A ⟹ 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: "(∑v∈t. 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. t∈T ⟹ ∥t∥ = 1›
shows ‹x = (∑t∈T. (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 ‹{∑a∈t. r a *⇩C a |t r. finite t ∧ t ⊆ T} = {∑a∈T. 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) = (∑a∈Aa. f a *⇩C a) ∧ finite Aa ∧ Aa ⊆ A} = cspan A"
by (simp add: complex_vector.span_explicit)
have f2: "∀a. (∃f. a = (∑a∈T. f a *⇩C a)) ∨ (∀A. (∀f. a ≠ (∑a∈A. f a *⇩C a)) ∨ infinite A ∨ ¬ A ⊆ T)"
using ‹{∑a∈t. r a *⇩C a |t r. finite t ∧ t ⊆ T} = {∑a∈T. r a *⇩C a |r. True}› by auto
have f3: "∀A a. (∃Aa f. (a::'a) = (∑a∈Aa. 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 = (∑ a∈T. r a *⇩C a)›
using f3 f2 by blast
then obtain r where ‹x = (∑ a∈T. 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: ‹(∑ t∈T-{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 (∑ t∈T. r t *⇩C t)›
using ‹x = (∑ a∈T. r a *⇩C a)›
by simp
also have ‹… = (∑ t∈T. a ∙⇩C (r t *⇩C t))›
using cinner_sum_right by blast
also have ‹… = (∑ t∈T. r t * (a ∙⇩C t))›
by simp
also have ‹… = r a * (a ∙⇩C a) + (∑ t∈T-{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 = (∑ a∈T. 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 \<^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 ∙⇩C v) = ∥w∥⇧2 ∧ w ∈ M) ∨ v ∉ M"
by (metis (no_types) power2_norm_eq_cinner')
hence "Re (x ∙⇩C x) ∈ {∥v∥⇧2 |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 ≤ ∥x∥⇧2›)
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 ≤ ∥x∥⇧2›)
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 n∥⇧2 < 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 m∥⇧2 < 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 m∥⇧2›)
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 m∥⇧2 < 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 m∥⇧2 < 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 ≤ ∥x∥⇧2› ‹∀n. r n ∈ M ∧ ∥r n∥⇧2 < 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 ≤ ∥x∥⇧2› by auto
hence q1: ‹∃ k. is_arg_min (λ x. ∥x∥^2) (λ t. t ∈ M) k›
using ‹k ∈ M›
is_arg_min_def ‹d = ∥k∥⇧2›
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. x∈M) (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. x∈M) (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. x∈M) 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) ∙⇩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 * ∥f∥⇧2›
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 * ∥f∥⇧2)›
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) ≤ ∥f∥⇧2›)
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```