Theory Complex_Inner_Product
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)›
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 )›
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›
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)›
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
‹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:
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:
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:
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:
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 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. 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 - k∥⇧2 ≤ ∥h - f∥⇧2 ›
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]:
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
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 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)›
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
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 \<^cite>‹conway2013course››
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 \<^cite>‹conway2013course››
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 ‹∀ a∈A. ∀ b∈B. (a+b) ∙⇩C x = 0›
by (simp add: ‹∀y∈A. y ∙⇩C x = 0› ‹∀y∈B. (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 ⟷ (∀x∈space_as_set S. ∀y∈space_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. x∈F ⟹ 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: ‹(∀x∈S. ∀y∈T. 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 ‹∃B∈Collect 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 ‹x∈⋃C› ‹y∈⋃C› ‹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: ‹∀b∈B. 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 ‹x∈B'› ‹y∈B'› ‹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. x∈S ⟹ 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 ‹∀b∈B'. 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. b∈B ⟹ 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: ‹φ = (∑b∈G. f b *⇩C b)›
using complex_vector.span_finite[OF ‹finite G›]
by auto
have ‹sum (bb φ) G = (∑c∈G. ∑b∈G. 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 ‹… = (∑b∈G. 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 ‹(∑b∈G. 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 ‹… < e2⇧2›
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. b∈B ⟹ norm b = 1› and ‹ψ ∈ space_as_set (ccspan B)›
shows ‹(∑⇩∞b∈B. (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. b∈B ⟹ 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. b∈B ⟹ 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) (∑b∈F. (b ∙⇩C ψ) *⇩C b) = (∑b∈F. (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. ∑b∈F. (b ∙⇩C ψ) *⇩C b) ⤏ ψ) (finite_subsets_at_top B)›
by (simp add: has_sum_def)
then have ‹((λF. (λv. (norm v)⇧2) (∑b∈F. (b ∙⇩C ψ) *⇩C b)) ⤏ (norm ψ)⇧2) (finite_subsets_at_top B)›
apply (rule isCont_tendsto_compose[rotated])
by simp
then have ‹((λF. (∑b∈F. (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. b∈B ⟹ 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. b∈B ⟹ norm b = 1› and ‹ψ ∈ space_as_set (ccspan B)›
shows ‹(∑⇩∞b∈B. (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:
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:
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_name>‹is_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_name>‹is_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 ⟹ (∀x∈S. 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