Theory Complex_L2
section ‹‹Complex_L2› -- Hilbert space of square-summable functions›
theory Complex_L2
imports
Complex_Bounded_Linear_Function
"HOL-Analysis.L2_Norm"
"HOL-Library.Rewrite"
"HOL-Analysis.Infinite_Sum"
begin
unbundle lattice_syntax
unbundle cblinfun_notation
unbundle no_notation_blinfun_apply
subsection ‹l2 norm of functions›
definition "has_ell2_norm (x::_⇒complex) ⟷ (λi. (x i)⇧2) abs_summable_on UNIV"
lemma has_ell2_norm_bdd_above: ‹has_ell2_norm x ⟷ bdd_above (sum (λxa. norm ((x xa)⇧2)) ` Collect finite)›
by (simp add: has_ell2_norm_def abs_summable_iff_bdd_above)
lemma has_ell2_norm_L2_set: "has_ell2_norm x = bdd_above (L2_set (norm o x) ` Collect finite)"
proof (rule iffI)
have ‹mono sqrt›
using monoI real_sqrt_le_mono by blast
assume ‹has_ell2_norm x›
then have *: ‹bdd_above (sum (λxa. norm ((x xa)⇧2)) ` Collect finite)›
by (subst (asm) has_ell2_norm_bdd_above)
have ‹bdd_above ((λF. sqrt (sum (λxa. norm ((x xa)⇧2)) F)) ` Collect finite)›
using bdd_above_image_mono[OF ‹mono sqrt› *]
by (auto simp: image_image)
then show ‹bdd_above (L2_set (norm o x) ` Collect finite)›
by (auto simp: L2_set_def norm_power)
next
define p2 where ‹p2 x = (if x < 0 then 0 else x^2)› for x :: real
have ‹mono p2›
by (simp add: monoI p2_def)
have [simp]: ‹p2 (L2_set f F) = (∑i∈F. (f i)⇧2)› for f and F :: ‹'a set›
by (smt (verit) L2_set_def L2_set_nonneg p2_def power2_less_0 real_sqrt_pow2 sum.cong sum_nonneg)
assume *: ‹bdd_above (L2_set (norm o x) ` Collect finite)›
have ‹bdd_above (p2 ` L2_set (norm o x) ` Collect finite)›
using bdd_above_image_mono[OF ‹mono p2› *]
by auto
then show ‹has_ell2_norm x›
apply (simp add: image_image has_ell2_norm_def abs_summable_iff_bdd_above)
by (simp add: norm_power)
qed
definition ell2_norm :: ‹('a ⇒ complex) ⇒ real› where ‹ell2_norm x = sqrt (∑⇩∞i. norm (x i)^2)›
lemma ell2_norm_SUP:
assumes ‹has_ell2_norm x›
shows "ell2_norm x = sqrt (SUP F∈{F. finite F}. sum (λi. norm (x i)^2) F)"
using assms apply (auto simp add: ell2_norm_def has_ell2_norm_def)
apply (subst infsum_nonneg_is_SUPREMUM_real)
by (auto simp: norm_power)
lemma ell2_norm_L2_set:
assumes "has_ell2_norm x"
shows "ell2_norm x = (SUP F∈{F. finite F}. L2_set (norm o x) F)"
proof-
have "sqrt (⨆ (sum (λi. (cmod (x i))⇧2) ` Collect finite)) =
(SUP F∈{F. finite F}. sqrt (∑i∈F. (cmod (x i))⇧2))"
proof (subst continuous_at_Sup_mono)
show "mono sqrt"
by (simp add: mono_def)
show "continuous (at_left (⨆ (sum (λi. (cmod (x i))⇧2) ` Collect finite))) sqrt"
using continuous_at_split isCont_real_sqrt by blast
show "sum (λi. (cmod (x i))⇧2) ` Collect finite ≠ {}"
by auto
show "bdd_above (sum (λi. (cmod (x i))⇧2) ` Collect finite)"
using has_ell2_norm_bdd_above[THEN iffD1, OF assms] by (auto simp: norm_power)
show "⨆ (sqrt ` sum (λi. (cmod (x i))⇧2) ` Collect finite) = (SUP F∈Collect finite. sqrt (∑i∈F. (cmod (x i))⇧2))"
by (metis image_image)
qed
thus ?thesis
using assms by (auto simp: ell2_norm_SUP L2_set_def)
qed
lemma has_ell2_norm_finite[simp]: "has_ell2_norm (x::'a::finite⇒_)"
unfolding has_ell2_norm_def by simp
lemma ell2_norm_finite:
"ell2_norm (x::'a::finite⇒complex) = sqrt (sum (λi. (norm(x i))^2) UNIV)"
by (simp add: ell2_norm_def)
lemma ell2_norm_finite_L2_set: "ell2_norm (x::'a::finite⇒complex) = L2_set (norm o x) UNIV"
by (simp add: ell2_norm_finite L2_set_def)
lemma ell2_ket:
fixes a
defines ‹f ≡ (λi. if a = i then 1 else 0)›
shows has_ell2_norm_ket: ‹has_ell2_norm f›
and ell2_norm_ket: ‹ell2_norm f = 1›
proof -
have ‹(λx. (f x)⇧2) abs_summable_on {a}›
apply (rule summable_on_finite) by simp
then show ‹has_ell2_norm f›
unfolding has_ell2_norm_def
apply (rule summable_on_cong_neutral[THEN iffD1, rotated -1])
unfolding f_def by auto
have ‹(∑⇩∞x∈{a}. (f x)⇧2) = 1›
apply (subst infsum_finite)
by (auto simp: f_def)
then show ‹ell2_norm f = 1›
unfolding ell2_norm_def
apply (subst infsum_cong_neutral[where T=‹{a}› and g=‹λx. (cmod (f x))⇧2›])
by (auto simp: f_def)
qed
lemma ell2_norm_geq0: ‹ell2_norm x ≥ 0›
by (auto simp: ell2_norm_def intro!: infsum_nonneg)
lemma ell2_norm_point_bound:
assumes ‹has_ell2_norm x›
shows ‹ell2_norm x ≥ cmod (x i)›
proof -
have ‹(cmod (x i))⇧2 = norm ((x i)⇧2)›
by (simp add: norm_power)
also have ‹norm ((x i)⇧2) = sum (λi. (norm ((x i)⇧2))) {i}›
by auto
also have ‹… = infsum (λi. (norm ((x i)⇧2))) {i}›
by (rule infsum_finite[symmetric], simp)
also have ‹… ≤ infsum (λi. (norm ((x i)⇧2))) UNIV›
apply (rule infsum_mono_neutral)
using assms by (auto simp: has_ell2_norm_def)
also have ‹… = (ell2_norm x)⇧2›
by (metis (no_types, lifting) ell2_norm_def ell2_norm_geq0 infsum_cong norm_power real_sqrt_eq_iff real_sqrt_unique)
finally show ?thesis
using ell2_norm_geq0 power2_le_imp_le by blast
qed
lemma ell2_norm_0:
assumes "has_ell2_norm x"
shows "(ell2_norm x = 0) = (x = (λ_. 0))"
proof
assume u1: "x = (λ_. 0)"
have u2: "(SUP x::'a set∈Collect finite. (0::real)) = 0"
if "x = (λ_. 0)"
by (metis cSUP_const empty_Collect_eq finite.emptyI)
show "ell2_norm x = 0"
unfolding ell2_norm_def
using u1 u2 by auto
next
assume norm0: "ell2_norm x = 0"
show "x = (λ_. 0)"
proof
fix i
have ‹cmod (x i) ≤ ell2_norm x›
using assms by (rule ell2_norm_point_bound)
also have ‹… = 0›
by (fact norm0)
finally show "x i = 0" by auto
qed
qed
lemma ell2_norm_smult:
assumes "has_ell2_norm x"
shows "has_ell2_norm (λi. c * x i)" and "ell2_norm (λi. c * x i) = cmod c * ell2_norm x"
proof -
have L2_set_mul: "L2_set (cmod ∘ (λi. c * x i)) F = cmod c * L2_set (cmod ∘ x) F" for F
proof-
have "L2_set (cmod ∘ (λi. c * x i)) F = L2_set (λi. (cmod c * (cmod o x) i)) F"
by (metis comp_def norm_mult)
also have "… = cmod c * L2_set (cmod o x) F"
by (metis norm_ge_zero L2_set_right_distrib)
finally show ?thesis .
qed
from assms obtain M where M: "M ≥ L2_set (cmod o x) F" if "finite F" for F
unfolding has_ell2_norm_L2_set bdd_above_def by auto
hence "cmod c * M ≥ L2_set (cmod o (λi. c * x i)) F" if "finite F" for F
unfolding L2_set_mul
by (simp add: ordered_comm_semiring_class.comm_mult_left_mono that)
thus has: "has_ell2_norm (λi. c * x i)"
unfolding has_ell2_norm_L2_set bdd_above_def using L2_set_mul[symmetric] by auto
have "ell2_norm (λi. c * x i) = (SUP F ∈ Collect finite. (L2_set (cmod ∘ (λi. c * x i)) F))"
by (simp add: ell2_norm_L2_set has)
also have "… = (SUP F ∈ Collect finite. (cmod c * L2_set (cmod ∘ x) F))"
using L2_set_mul by auto
also have "… = cmod c * ell2_norm x"
proof (subst ell2_norm_L2_set)
show "has_ell2_norm x"
by (simp add: assms)
show "(SUP F∈Collect finite. cmod c * L2_set (cmod ∘ x) F) = cmod c * ⨆ (L2_set (cmod ∘ x) ` Collect finite)"
proof (subst continuous_at_Sup_mono [where f = "λx. cmod c * x"])
show "mono ((*) (cmod c))"
by (simp add: mono_def ordered_comm_semiring_class.comm_mult_left_mono)
show "continuous (at_left (⨆ (L2_set (cmod ∘ x) ` Collect finite))) ((*) (cmod c))"
proof (rule continuous_mult)
show "continuous (at_left (⨆ (L2_set (cmod ∘ x) ` Collect finite))) (λx. cmod c)"
by simp
show "continuous (at_left (⨆ (L2_set (cmod ∘ x) ` Collect finite))) (λx. x)"
by simp
qed
show "L2_set (cmod ∘ x) ` Collect finite ≠ {}"
by auto
show "bdd_above (L2_set (cmod ∘ x) ` Collect finite)"
by (meson assms has_ell2_norm_L2_set)
show "(SUP F∈Collect finite. cmod c * L2_set (cmod ∘ x) F) = ⨆ ((*) (cmod c) ` L2_set (cmod ∘ x) ` Collect finite)"
by (metis image_image)
qed
qed
finally show "ell2_norm (λi. c * x i) = cmod c * ell2_norm x".
qed
lemma ell2_norm_triangle:
assumes "has_ell2_norm x" and "has_ell2_norm y"
shows "has_ell2_norm (λi. x i + y i)" and "ell2_norm (λi. x i + y i) ≤ ell2_norm x + ell2_norm y"
proof -
have triangle: "L2_set (cmod ∘ (λi. x i + y i)) F ≤ L2_set (cmod ∘ x) F + L2_set (cmod ∘ y) F"
(is "?lhs≤?rhs")
if "finite F" for F
proof -
have "?lhs ≤ L2_set (λi. (cmod o x) i + (cmod o y) i) F"
proof (rule L2_set_mono)
show "(cmod ∘ (λi. x i + y i)) i ≤ (cmod ∘ x) i + (cmod ∘ y) i"
if "i ∈ F"
for i :: 'a
using that norm_triangle_ineq by auto
show "0 ≤ (cmod ∘ (λi. x i + y i)) i"
if "i ∈ F"
for i :: 'a
using that
by simp
qed
also have "… ≤ ?rhs"
by (rule L2_set_triangle_ineq)
finally show ?thesis .
qed
obtain Mx My where Mx: "Mx ≥ L2_set (cmod o x) F" and My: "My ≥ L2_set (cmod o y) F"
if "finite F" for F
using assms unfolding has_ell2_norm_L2_set bdd_above_def by auto
hence MxMy: "Mx + My ≥ L2_set (cmod ∘ x) F + L2_set (cmod ∘ y) F" if "finite F" for F
using that by fastforce
hence bdd_plus: "bdd_above ((λxa. L2_set (cmod ∘ x) xa + L2_set (cmod ∘ y) xa) ` Collect finite)"
unfolding bdd_above_def by auto
from MxMy have MxMy': "Mx + My ≥ L2_set (cmod ∘ (λi. x i + y i)) F" if "finite F" for F
using triangle that by fastforce
thus has: "has_ell2_norm (λi. x i + y i)"
unfolding has_ell2_norm_L2_set bdd_above_def by auto
have SUP_plus: "(SUP x∈A. f x + g x) ≤ (SUP x∈A. f x) + (SUP x∈A. g x)"
if notempty: "A≠{}" and bddf: "bdd_above (f`A)"and bddg: "bdd_above (g`A)"
for f g :: "'a set ⇒ real" and A
proof-
have xleq: "x ≤ (SUP x∈A. f x) + (SUP x∈A. g x)" if x: "x ∈ (λx. f x + g x) ` A" for x
proof -
obtain a where aA: "a:A" and ax: "x = f a + g a"
using x by blast
have fa: "f a ≤ (SUP x∈A. f x)"
by (simp add: bddf aA cSUP_upper)
moreover have "g a ≤ (SUP x∈A. g x)"
by (simp add: bddg aA cSUP_upper)
ultimately have "f a + g a ≤ (SUP x∈A. f x) + (SUP x∈A. g x)" by simp
with ax show ?thesis by simp
qed
have "(λx. f x + g x) ` A ≠ {}"
using notempty by auto
moreover have "x ≤ ⨆ (f ` A) + ⨆ (g ` A)"
if "x ∈ (λx. f x + g x) ` A"
for x :: real
using that
by (simp add: xleq)
ultimately show ?thesis
by (meson bdd_above_def cSup_le_iff)
qed
have a2: "bdd_above (L2_set (cmod ∘ x) ` Collect finite)"
by (meson assms(1) has_ell2_norm_L2_set)
have a3: "bdd_above (L2_set (cmod ∘ y) ` Collect finite)"
by (meson assms(2) has_ell2_norm_L2_set)
have a1: "Collect finite ≠ {}"
by auto
have a4: "⨆ (L2_set (cmod ∘ (λi. x i + y i)) ` Collect finite)
≤ (SUP xa∈Collect finite.
L2_set (cmod ∘ x) xa + L2_set (cmod ∘ y) xa)"
by (metis (mono_tags, lifting) a1 bdd_plus cSUP_mono mem_Collect_eq triangle)
have "∀r. ⨆ (L2_set (cmod ∘ (λa. x a + y a)) ` Collect finite) ≤ r ∨ ¬ (SUP A∈Collect finite. L2_set (cmod ∘ x) A + L2_set (cmod ∘ y) A) ≤ r"
using a4 by linarith
hence "⨆ (L2_set (cmod ∘ (λi. x i + y i)) ` Collect finite)
≤ ⨆ (L2_set (cmod ∘ x) ` Collect finite) +
⨆ (L2_set (cmod ∘ y) ` Collect finite)"
by (metis (no_types) SUP_plus a1 a2 a3)
hence "⨆ (L2_set (cmod ∘ (λi. x i + y i)) ` Collect finite) ≤ ell2_norm x + ell2_norm y"
by (simp add: assms(1) assms(2) ell2_norm_L2_set)
thus "ell2_norm (λi. x i + y i) ≤ ell2_norm x + ell2_norm y"
by (simp add: ell2_norm_L2_set has)
qed
lemma ell2_norm_uminus:
assumes "has_ell2_norm x"
shows ‹has_ell2_norm (λi. - x i)› and ‹ell2_norm (λi. - x i) = ell2_norm x›
using assms by (auto simp: has_ell2_norm_def ell2_norm_def)
subsection ‹The type ‹ell2› of square-summable functions›
typedef 'a ell2 = "{x::'a⇒complex. has_ell2_norm x}"
unfolding has_ell2_norm_def by (rule exI[of _ "λ_.0"], auto)
setup_lifting type_definition_ell2
instantiation ell2 :: (type)complex_vector begin
lift_definition zero_ell2 :: "'a ell2" is "λ_. 0" by (auto simp: has_ell2_norm_def)
lift_definition uminus_ell2 :: "'a ell2 ⇒ 'a ell2" is uminus by (simp add: has_ell2_norm_def)
lift_definition plus_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ 'a ell2" is "λf g x. f x + g x"
by (rule ell2_norm_triangle)
lift_definition minus_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ 'a ell2" is "λf g x. f x - g x"
apply (subst add_uminus_conv_diff[symmetric])
apply (rule ell2_norm_triangle)
by (auto simp add: ell2_norm_uminus)
lift_definition scaleR_ell2 :: "real ⇒ 'a ell2 ⇒ 'a ell2" is "λr f x. complex_of_real r * f x"
by (rule ell2_norm_smult)
lift_definition scaleC_ell2 :: "complex ⇒ 'a ell2 ⇒ 'a ell2" is "λc f x. c * f x"
by (rule ell2_norm_smult)
instance
proof
fix a b c :: "'a ell2"
show "((*⇩R) r::'a ell2 ⇒ _) = (*⇩C) (complex_of_real r)" for r
apply (rule ext) apply transfer by auto
show "a + b + c = a + (b + c)"
by (transfer; rule ext; simp)
show "a + b = b + a"
by (transfer; rule ext; simp)
show "0 + a = a"
by (transfer; rule ext; simp)
show "- a + a = 0"
by (transfer; rule ext; simp)
show "a - b = a + - b"
by (transfer; rule ext; simp)
show "r *⇩C (a + b) = r *⇩C a + r *⇩C b" for r
apply (transfer; rule ext)
by (simp add: vector_space_over_itself.scale_right_distrib)
show "(r + r') *⇩C a = r *⇩C a + r' *⇩C a" for r r'
apply (transfer; rule ext)
by (simp add: ring_class.ring_distribs(2))
show "r *⇩C r' *⇩C a = (r * r') *⇩C a" for r r'
by (transfer; rule ext; simp)
show "1 *⇩C a = a"
by (transfer; rule ext; simp)
qed
end
instantiation ell2 :: (type)complex_normed_vector begin
lift_definition norm_ell2 :: "'a ell2 ⇒ real" is ell2_norm .
declare norm_ell2_def[code del]
definition "dist x y = norm (x - y)" for x y::"'a ell2"
definition "sgn x = x /⇩R norm x" for x::"'a ell2"
definition [code del]: "uniformity = (INF e∈{0<..}. principal {(x::'a ell2, y). norm (x - y) < e})"
definition [code del]: "open U = (∀x∈U. ∀⇩F (x', y) in INF e∈{0<..}. principal {(x, y). norm (x - y) < e}. x' = x ⟶ y ∈ U)" for U :: "'a ell2 set"
instance
proof
fix a b :: "'a ell2"
show "dist a b = norm (a - b)"
by (simp add: dist_ell2_def)
show "sgn a = a /⇩R norm a"
by (simp add: sgn_ell2_def)
show "uniformity = (INF e∈{0<..}. principal {(x, y). dist (x::'a ell2) y < e})"
unfolding dist_ell2_def uniformity_ell2_def by simp
show "open U = (∀x∈U. ∀⇩F (x', y) in uniformity. (x'::'a ell2) = x ⟶ y ∈ U)" for U :: "'a ell2 set"
unfolding uniformity_ell2_def open_ell2_def by simp_all
show "(norm a = 0) = (a = 0)"
apply transfer by (fact ell2_norm_0)
show "norm (a + b) ≤ norm a + norm b"
apply transfer by (fact ell2_norm_triangle)
show "norm (r *⇩R (a::'a ell2)) = ¦r¦ * norm a" for r
and a :: "'a ell2"
apply transfer
by (simp add: ell2_norm_smult(2))
show "norm (r *⇩C a) = cmod r * norm a" for r
apply transfer
by (simp add: ell2_norm_smult(2))
qed
end
lemma norm_point_bound_ell2: "norm (Rep_ell2 x i) ≤ norm x"
apply transfer
by (simp add: ell2_norm_point_bound)
lemma ell2_norm_finite_support:
assumes ‹finite S› ‹⋀ i. i ∉ S ⟹ Rep_ell2 x i = 0›
shows ‹norm x = sqrt ((sum (λi. (cmod (Rep_ell2 x i))⇧2)) S)›
proof (insert assms(2), transfer fixing: S)
fix x :: ‹'a ⇒ complex›
assume zero: ‹⋀i. i ∉ S ⟹ x i = 0›
have ‹ell2_norm x = sqrt (∑⇩∞i. (cmod (x i))⇧2)›
by (auto simp: ell2_norm_def)
also have ‹… = sqrt (∑⇩∞i∈S. (cmod (x i))⇧2)›
apply (subst infsum_cong_neutral[where g=‹λi. (cmod (x i))⇧2› and S=UNIV and T=S])
using zero by auto
also have ‹… = sqrt (∑i∈S. (cmod (x i))⇧2)›
using ‹finite S› by simp
finally show ‹ell2_norm x = sqrt (∑i∈S. (cmod (x i))⇧2)›
by -
qed
instantiation ell2 :: (type) complex_inner begin
lift_definition cinner_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ complex" is
"λx y. infsum (λi. (cnj (x i) * y i)) UNIV" .
declare cinner_ell2_def[code del]
instance
proof standard
fix x y z :: "'a ell2" fix c :: complex
show "cinner x y = cnj (cinner y x)"
proof transfer
fix x y :: "'a⇒complex" assume "has_ell2_norm x" and "has_ell2_norm y"
have "(∑⇩∞i. cnj (x i) * y i) = (∑⇩∞i. cnj (cnj (y i) * x i))"
by (metis complex_cnj_cnj complex_cnj_mult mult.commute)
also have "… = cnj (∑⇩∞i. cnj (y i) * x i)"
by (metis infsum_cnj)
finally show "(∑⇩∞i. cnj (x i) * y i) = cnj (∑⇩∞i. cnj (y i) * x i)" .
qed
show "cinner (x + y) z = cinner x z + cinner y z"
proof transfer
fix x y z :: "'a ⇒ complex"
assume "has_ell2_norm x"
hence cnj_x: "(λi. cnj (x i) * cnj (x i)) abs_summable_on UNIV"
by (simp del: complex_cnj_mult add: norm_mult[symmetric] complex_cnj_mult[symmetric] has_ell2_norm_def power2_eq_square)
assume "has_ell2_norm y"
hence cnj_y: "(λi. cnj (y i) * cnj (y i)) abs_summable_on UNIV"
by (simp del: complex_cnj_mult add: norm_mult[symmetric] complex_cnj_mult[symmetric] has_ell2_norm_def power2_eq_square)
assume "has_ell2_norm z"
hence z: "(λi. z i * z i) abs_summable_on UNIV"
by (simp add: norm_mult[symmetric] has_ell2_norm_def power2_eq_square)
have cnj_x_z:"(λi. cnj (x i) * z i) abs_summable_on UNIV"
using cnj_x z by (rule abs_summable_product)
have cnj_y_z:"(λi. cnj (y i) * z i) abs_summable_on UNIV"
using cnj_y z by (rule abs_summable_product)
show "(∑⇩∞i. cnj (x i + y i) * z i) = (∑⇩∞i. cnj (x i) * z i) + (∑⇩∞i. cnj (y i) * z i)"
apply (subst infsum_add [symmetric])
using cnj_x_z cnj_y_z
by (auto simp add: summable_on_iff_abs_summable_on_complex distrib_left mult.commute)
qed
show "cinner (c *⇩C x) y = cnj c * cinner x y"
proof transfer
fix x y :: "'a ⇒ complex" and c :: complex
assume "has_ell2_norm x"
hence cnj_x: "(λi. cnj (x i) * cnj (x i)) abs_summable_on UNIV"
by (simp del: complex_cnj_mult add: norm_mult[symmetric] complex_cnj_mult[symmetric] has_ell2_norm_def power2_eq_square)
assume "has_ell2_norm y"
hence y: "(λi. y i * y i) abs_summable_on UNIV"
by (simp add: norm_mult[symmetric] has_ell2_norm_def power2_eq_square)
have cnj_x_y:"(λi. cnj (x i) * y i) abs_summable_on UNIV"
using cnj_x y by (rule abs_summable_product)
thus "(∑⇩∞i. cnj (c * x i) * y i) = cnj c * (∑⇩∞i. cnj (x i) * y i)"
by (auto simp flip: infsum_cmult_right simp add: abs_summable_summable mult.commute vector_space_over_itself.scale_left_commute)
qed
show "0 ≤ cinner x x"
proof transfer
fix x :: "'a ⇒ complex"
assume "has_ell2_norm x"
hence "(λi. cmod (cnj (x i) * x i)) abs_summable_on UNIV"
by (simp add: norm_mult has_ell2_norm_def power2_eq_square)
hence "(λi. cnj (x i) * x i) abs_summable_on UNIV"
by auto
hence sum: "(λi. cnj (x i) * x i) abs_summable_on UNIV"
unfolding has_ell2_norm_def power2_eq_square.
have "0 = (∑⇩∞i::'a. 0)" by auto
also have "… ≤ (∑⇩∞i. cnj (x i) * x i)"
apply (rule infsum_mono_complex)
by (auto simp add: abs_summable_summable sum)
finally show "0 ≤ (∑⇩∞i. cnj (x i) * x i)" by assumption
qed
show "(cinner x x = 0) = (x = 0)"
proof (transfer, auto)
fix x :: "'a ⇒ complex"
assume "has_ell2_norm x"
hence "(λi::'a. cmod (cnj (x i) * x i)) abs_summable_on UNIV"
by (smt (verit, del_insts) complex_mod_mult_cnj has_ell2_norm_def mult.commute norm_ge_zero norm_power real_norm_def summable_on_cong)
hence cmod_x2: "(λi. cnj (x i) * x i) abs_summable_on UNIV"
unfolding has_ell2_norm_def power2_eq_square
by simp
assume eq0: "(∑⇩∞i. cnj (x i) * x i) = 0"
show "x = (λ_. 0)"
proof (rule ccontr)
assume "x ≠ (λ_. 0)"
then obtain i where "x i ≠ 0" by auto
hence "0 < cnj (x i) * x i"
by (metis le_less cnj_x_x_geq0 complex_cnj_zero_iff vector_space_over_itself.scale_eq_0_iff)
also have "… = (∑⇩∞i∈{i}. cnj (x i) * x i)" by auto
also have "… ≤ (∑⇩∞i. cnj (x i) * x i)"
apply (rule infsum_mono_neutral_complex)
by (auto simp add: abs_summable_summable cmod_x2)
also from eq0 have "… = 0" by assumption
finally show False by simp
qed
qed
show "norm x = sqrt (cmod (cinner x x))"
proof transfer
fix x :: "'a ⇒ complex"
assume x: "has_ell2_norm x"
have "(λi::'a. cmod (x i) * cmod (x i)) abs_summable_on UNIV ⟹
(λi::'a. cmod (cnj (x i) * x i)) abs_summable_on UNIV"
by (simp add: norm_mult has_ell2_norm_def power2_eq_square)
hence sum: "(λi. cnj (x i) * x i) abs_summable_on UNIV"
by (metis (no_types, lifting) complex_mod_mult_cnj has_ell2_norm_def mult.commute norm_power summable_on_cong x)
from x have "ell2_norm x = sqrt (∑⇩∞i. (cmod (x i))⇧2)"
unfolding ell2_norm_def by simp
also have "… = sqrt (∑⇩∞i. cmod (cnj (x i) * x i))"
unfolding norm_complex_def power2_eq_square by auto
also have "… = sqrt (cmod (∑⇩∞i. cnj (x i) * x i))"
by (auto simp: infsum_cmod abs_summable_summable sum)
finally show "ell2_norm x = sqrt (cmod (∑⇩∞i. cnj (x i) * x i))" by assumption
qed
qed
end
instance ell2 :: (type) chilbert_space
proof
fix X :: ‹nat ⇒ 'a ell2›
define x where ‹x n a = Rep_ell2 (X n) a› for n a
have [simp]: ‹has_ell2_norm (x n)› for n
using Rep_ell2 x_def[abs_def] by simp
assume ‹Cauchy X›
moreover have "dist (x n a) (x m a) ≤ dist (X n) (X m)" for n m a
by (metis Rep_ell2 x_def dist_norm ell2_norm_point_bound mem_Collect_eq minus_ell2.rep_eq norm_ell2.rep_eq)
ultimately have ‹Cauchy (λn. x n a)› for a
by (meson Cauchy_def le_less_trans)
then obtain l where x_lim: ‹(λn. x n a) ⇢ l a› for a
apply atomize_elim apply (rule choice)
by (simp add: convergent_eq_Cauchy)
define L where ‹L = Abs_ell2 l›
define normF where ‹normF F x = L2_set (cmod ∘ x) F› for F :: ‹'a set› and x
have normF_triangle: ‹normF F (λa. x a + y a) ≤ normF F x + normF F y› if ‹finite F› for F x y
proof -
have ‹normF F (λa. x a + y a) = L2_set (λa. cmod (x a + y a)) F›
by (metis (mono_tags, lifting) L2_set_cong comp_apply normF_def)
also have ‹… ≤ L2_set (λa. cmod (x a) + cmod (y a)) F›
by (meson L2_set_mono norm_ge_zero norm_triangle_ineq)
also have ‹… ≤ L2_set (λa. cmod (x a)) F + L2_set (λa. cmod (y a)) F›
by (simp add: L2_set_triangle_ineq)
also have ‹… ≤ normF F x + normF F y›
by (smt (verit, best) L2_set_cong normF_def comp_apply)
finally show ?thesis
by -
qed
have normF_negate: ‹normF F (λa. - x a) = normF F x› if ‹finite F› for F x
unfolding normF_def o_def by simp
have normF_ell2norm: ‹normF F x ≤ ell2_norm x› if ‹finite F› and ‹has_ell2_norm x› for F x
apply (auto intro!: cSUP_upper2[where x=F] simp: that normF_def ell2_norm_L2_set)
by (meson has_ell2_norm_L2_set that(2))
note Lim_bounded2[rotated, rule_format, trans]
from ‹Cauchy X›
obtain I where cauchyX: ‹norm (X n - X m) ≤ ε› if ‹ε>0› ‹n≥I ε› ‹m≥I ε› for ε n m
by (metis Cauchy_def dist_norm less_eq_real_def)
have normF_xx: ‹normF F (λa. x n a - x m a) ≤ ε› if ‹finite F› ‹ε>0› ‹n≥I ε› ‹m≥I ε› for ε n m F
apply (subst asm_rl[of ‹(λa. x n a - x m a) = Rep_ell2 (X n - X m)›])
apply (simp add: x_def minus_ell2.rep_eq)
using that cauchyX by (metis Rep_ell2 mem_Collect_eq normF_ell2norm norm_ell2.rep_eq order_trans)
have normF_xl_lim: ‹(λm. normF F (λa. x m a - l a)) ⇢ 0› if ‹finite F› for F
proof -
have ‹(λxa. cmod (x xa m - l m)) ⇢ 0› for m
using x_lim by (simp add: LIM_zero_iff tendsto_norm_zero)
then have ‹(λm. ∑i∈F. ((cmod ∘ (λa. x m a - l a)) i)⇧2) ⇢ 0›
by (auto intro: tendsto_null_sum)
then show ?thesis
unfolding normF_def L2_set_def
using tendsto_real_sqrt by force
qed
have normF_xl: ‹normF F (λa. x n a - l a) ≤ ε›
if ‹n ≥ I ε› and ‹ε > 0› and ‹finite F› for n ε F
proof -
have ‹normF F (λa. x n a - l a) - ε ≤ normF F (λa. x n a - x m a) + normF F (λa. x m a - l a) - ε› for m
using normF_triangle[OF ‹finite F›, where x=‹(λa. x n a - x m a)› and y=‹(λa. x m a - l a)›]
by auto
also have ‹… m ≤ normF F (λa. x m a - l a)› if ‹m ≥ I ε› for m
using normF_xx[OF ‹finite F› ‹ε>0› ‹n ≥ I ε› ‹m ≥ I ε›]
by auto
also have ‹(λm. … m) ⇢ 0›
using ‹finite F› by (rule normF_xl_lim)
finally show ?thesis
by auto
qed
have ‹normF F l ≤ 1 + normF F (x (I 1))› if [simp]: ‹finite F› for F
using normF_xl[where F=F and ε=1 and n=‹I 1›]
using normF_triangle[where F=F and x=‹x (I 1)› and y=‹λa. l a - x (I 1) a›]
using normF_negate[where F=F and x=‹(λa. x (I 1) a - l a)›]
by auto
also have ‹… F ≤ 1 + ell2_norm (x (I 1))› if ‹finite F› for F
using normF_ell2norm that by simp
finally have [simp]: ‹has_ell2_norm l›
unfolding has_ell2_norm_L2_set
by (auto intro!: bdd_aboveI simp flip: normF_def)
then have ‹l = Rep_ell2 L›
by (simp add: Abs_ell2_inverse L_def)
have [simp]: ‹has_ell2_norm (λa. x n a - l a)› for n
apply (subst diff_conv_add_uminus)
apply (rule ell2_norm_triangle)
by (auto intro!: ell2_norm_uminus)
from normF_xl have ell2norm_xl: ‹ell2_norm (λa. x n a - l a) ≤ ε›
if ‹n ≥ I ε› and ‹ε > 0› for n ε
apply (subst ell2_norm_L2_set)
using that by (auto intro!: cSUP_least simp: normF_def)
have ‹norm (X n - L) ≤ ε› if ‹n ≥ I ε› and ‹ε > 0› for n ε
using ell2norm_xl[OF that]
by (simp add: x_def norm_ell2.rep_eq ‹l = Rep_ell2 L› minus_ell2.rep_eq)
then have ‹X ⇢ L›
unfolding tendsto_iff
apply (auto simp: dist_norm eventually_sequentially)
by (meson field_lbound_gt_zero le_less_trans)
then show ‹convergent X›
by (rule convergentI)
qed
instantiation ell2 :: (CARD_1) complex_algebra_1
begin
lift_definition one_ell2 :: "'a ell2" is "λ_. 1" by simp
lift_definition times_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ 'a ell2" is "λa b x. a x * b x"
by simp
instance
proof
fix a b c :: "'a ell2" and r :: complex
show "a * b * c = a * (b * c)"
by (transfer, auto)
show "(a + b) * c = a * c + b * c"
apply (transfer, rule ext)
by (simp add: distrib_left mult.commute)
show "a * (b + c) = a * b + a * c"
apply transfer
by (simp add: ring_class.ring_distribs(1))
show "r *⇩C a * b = r *⇩C (a * b)"
by (transfer, auto)
show "(a::'a ell2) * r *⇩C b = r *⇩C (a * b)"
by (transfer, auto)
show "1 * a = a"
by (transfer, rule ext, auto)
show "a * 1 = a"
by (transfer, rule ext, auto)
show "(0::'a ell2) ≠ 1"
apply transfer
by (meson zero_neq_one)
qed
end
instantiation ell2 :: (CARD_1) field begin
lift_definition divide_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ 'a ell2" is "λa b x. a x / b x"
by simp
lift_definition inverse_ell2 :: "'a ell2 ⇒ 'a ell2" is "λa x. inverse (a x)"
by simp
instance
proof (intro_classes; transfer)
fix a :: "'a ⇒ complex"
assume "a ≠ (λ_. 0)"
then obtain y where ay: "a y ≠ 0"
by auto
show "(λx. inverse (a x) * a x) = (λ_. 1)"
proof (rule ext)
fix x
have "x = y"
by auto
with ay have "a x ≠ 0"
by metis
then show "inverse (a x) * a x = 1"
by auto
qed
qed (auto simp add: divide_complex_def mult.commute ring_class.ring_distribs)
end
subsection ‹Orthogonality›
lemma ell2_pointwise_ortho:
assumes ‹⋀ i. Rep_ell2 x i = 0 ∨ Rep_ell2 y i = 0›
shows ‹is_orthogonal x y›
using assms apply transfer
by (simp add: infsum_0)
subsection ‹Truncated vectors›
lift_definition trunc_ell2:: ‹'a set ⇒ 'a ell2 ⇒ 'a ell2›
is ‹λ S x. (λ i. (if i ∈ S then x i else 0))›
proof (rename_tac S x)
fix x :: ‹'a ⇒ complex› and S :: ‹'a set›
assume ‹has_ell2_norm x›
then have ‹(λi. (x i)⇧2) abs_summable_on UNIV›
unfolding has_ell2_norm_def by -
then have ‹(λi. (x i)⇧2) abs_summable_on S›
using summable_on_subset_banach by blast
then have ‹(λxa. (if xa ∈ S then x xa else 0)⇧2) abs_summable_on UNIV›
apply (rule summable_on_cong_neutral[THEN iffD1, rotated -1])
by auto
then show ‹has_ell2_norm (λi. if i ∈ S then x i else 0)›
unfolding has_ell2_norm_def by -
qed
lemma trunc_ell2_empty[simp]: ‹trunc_ell2 {} x = 0›
apply transfer by simp
lemma norm_id_minus_trunc_ell2:
‹(norm (x - trunc_ell2 S x))^2 = (norm x)^2 - (norm (trunc_ell2 S x))^2›
proof-
have ‹Rep_ell2 (trunc_ell2 S x) i = 0 ∨ Rep_ell2 (x - trunc_ell2 S x) i = 0› for i
apply transfer
by auto
hence ‹⟨ (trunc_ell2 S x), (x - trunc_ell2 S x) ⟩ = 0›
using ell2_pointwise_ortho by blast
hence ‹(norm x)^2 = (norm (trunc_ell2 S x))^2 + (norm (x - trunc_ell2 S x))^2›
using pythagorean_theorem by fastforce
thus ?thesis by simp
qed
lemma norm_trunc_ell2_finite:
‹finite S ⟹ (norm (trunc_ell2 S x)) = sqrt ((sum (λi. (cmod (Rep_ell2 x i))⇧2)) S)›
proof-
assume ‹finite S›
moreover have ‹⋀ i. i ∉ S ⟹ Rep_ell2 ((trunc_ell2 S x)) i = 0›
by (simp add: trunc_ell2.rep_eq)
ultimately have ‹(norm (trunc_ell2 S x)) = sqrt ((sum (λi. (cmod (Rep_ell2 ((trunc_ell2 S x)) i))⇧2)) S)›
using ell2_norm_finite_support
by blast
moreover have ‹⋀ i. i ∈ S ⟹ Rep_ell2 ((trunc_ell2 S x)) i = Rep_ell2 x i›
by (simp add: trunc_ell2.rep_eq)
ultimately show ?thesis by simp
qed
lemma trunc_ell2_lim_at_UNIV:
‹((λS. trunc_ell2 S ψ) ⤏ ψ) (finite_subsets_at_top UNIV)›
proof -
define f where ‹f i = (cmod (Rep_ell2 ψ i))⇧2› for i
have has: ‹has_ell2_norm (Rep_ell2 ψ)›
using Rep_ell2 by blast
then have summable: "f abs_summable_on UNIV"
by (smt (verit, del_insts) f_def has_ell2_norm_def norm_ge_zero norm_power real_norm_def summable_on_cong)
have ‹norm ψ = (ell2_norm (Rep_ell2 ψ))›
apply transfer by simp
also have ‹… = sqrt (infsum f UNIV)›
by (simp add: ell2_norm_def f_def[symmetric])
finally have normψ: ‹norm ψ = sqrt (infsum f UNIV)›
by -
have norm_trunc: ‹norm (trunc_ell2 S ψ) = sqrt (sum f S)› if ‹finite S› for S
using f_def that norm_trunc_ell2_finite by fastforce
have ‹(sum f ⤏ infsum f UNIV) (finite_subsets_at_top UNIV)›
using f_def[abs_def] infsum_tendsto local.summable by fastforce
then have ‹((λS. sqrt (sum f S)) ⤏ sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)›
using tendsto_real_sqrt by blast
then have ‹((λS. norm (trunc_ell2 S ψ)) ⤏ norm ψ) (finite_subsets_at_top UNIV)›
apply (subst tendsto_cong[where g=‹λS. sqrt (sum f S)›])
by (auto simp add: eventually_finite_subsets_at_top_weakI norm_trunc normψ)
then have ‹((λS. (norm (trunc_ell2 S ψ))⇧2) ⤏ (norm ψ)⇧2) (finite_subsets_at_top UNIV)›
by (simp add: tendsto_power)
then have ‹((λS. (norm ψ)⇧2 - (norm (trunc_ell2 S ψ))⇧2) ⤏ 0) (finite_subsets_at_top UNIV)›
apply (rule tendsto_diff[where a=‹(norm ψ)^2› and b=‹(norm ψ)^2›, simplified, rotated])
by auto
then have ‹((λS. (norm (ψ - trunc_ell2 S ψ))⇧2) ⤏ 0) (finite_subsets_at_top UNIV)›
unfolding norm_id_minus_trunc_ell2 by simp
then have ‹((λS. norm (ψ - trunc_ell2 S ψ)) ⤏ 0) (finite_subsets_at_top UNIV)›
by auto
then have ‹((λS. ψ - trunc_ell2 S ψ) ⤏ 0) (finite_subsets_at_top UNIV)›
by (rule tendsto_norm_zero_cancel)
then show ?thesis
apply (rule Lim_transform2[where f=‹λ_. ψ›, rotated])
by simp
qed
subsection ‹Kets and bras›
lift_definition ket :: "'a ⇒ 'a ell2" is "λx y. if x=y then 1 else 0"
by (rule has_ell2_norm_ket)
abbreviation bra :: "'a ⇒ (_,complex) cblinfun" where "bra i ≡ vector_to_cblinfun (ket i)*" for i
instance ell2 :: (type) not_singleton
proof standard
have "ket undefined ≠ (0::'a ell2)"
proof transfer
show "(λy. if (undefined::'a) = y then 1::complex else 0) ≠ (λ_. 0)"
by (meson one_neq_zero)
qed
thus ‹∃x y::'a ell2. x ≠ y›
by blast
qed
lemma cinner_ket_left: ‹⟨ket i, ψ⟩ = Rep_ell2 ψ i›
apply (transfer fixing: i)
apply (subst infsum_cong_neutral[where T=‹{i}›])
by auto
lemma cinner_ket_right: ‹⟨ψ, ket i⟩ = cnj (Rep_ell2 ψ i)›
apply (transfer fixing: i)
apply (subst infsum_cong_neutral[where T=‹{i}›])
by auto
lemma cinner_ket_eqI:
assumes ‹⋀i. cinner (ket i) ψ = cinner (ket i) φ›
shows ‹ψ = φ›
by (metis Rep_ell2_inject assms cinner_ket_left ext)
lemma norm_ket[simp]: "norm (ket i) = 1"
apply transfer by (rule ell2_norm_ket)
lemma cinner_ket_same[simp]:
‹⟨ket i, ket i⟩ = 1›
proof-
have ‹norm (ket i) = 1›
by simp
hence ‹sqrt (cmod ⟨ket i, ket i⟩) = 1›
by (metis norm_eq_sqrt_cinner)
hence ‹cmod ⟨ket i, ket i⟩ = 1›
using real_sqrt_eq_1_iff by blast
moreover have ‹⟨ket i, ket i⟩ = cmod ⟨ket i, ket i⟩›
proof-
have ‹⟨ket i, ket i⟩ ∈ ℝ›
by (simp add: cinner_real)
thus ?thesis
by (metis cinner_ge_zero complex_of_real_cmod)
qed
ultimately show ?thesis by simp
qed
lemma orthogonal_ket[simp]:
‹is_orthogonal (ket i) (ket j) ⟷ i ≠ j›
by (simp add: cinner_ket_left ket.rep_eq)
lemma cinner_ket: ‹⟨ket i, ket j⟩ = (if i=j then 1 else 0)›
by (simp add: cinner_ket_left ket.rep_eq)
lemma ket_injective[simp]: ‹ket i = ket j ⟷ i = j›
by (metis cinner_ket one_neq_zero)
lemma inj_ket[simp]: ‹inj ket›
by (simp add: inj_on_def)
lemma trunc_ell2_ket_cspan:
‹trunc_ell2 S x ∈ (cspan (range ket))› if ‹finite S›
proof (use that in induction)
case empty
then show ?case
by (auto intro: complex_vector.span_zero)
next
case (insert a F)
from insert.hyps have ‹trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *⇩C ket a›
apply (transfer fixing: F a)
by auto
with insert.IH
show ?case
by (simp add: complex_vector.span_add_eq complex_vector.span_base complex_vector.span_scale)
qed
lemma closed_cspan_range_ket[simp]:
‹closure (cspan (range ket)) = UNIV›
proof (intro set_eqI iffI UNIV_I closure_approachable[THEN iffD2] allI impI)
fix ψ :: ‹'a ell2›
fix e :: real assume ‹e > 0›
have ‹((λS. trunc_ell2 S ψ) ⤏ ψ) (finite_subsets_at_top UNIV)›
by (rule trunc_ell2_lim_at_UNIV)
then obtain F where ‹finite F› and ‹dist (trunc_ell2 F ψ) ψ < e›
apply (drule_tac tendstoD[OF _ ‹e > 0›])
by (auto dest: simp: eventually_finite_subsets_at_top)
moreover have ‹trunc_ell2 F ψ ∈ cspan (range ket)›
using ‹finite F› trunc_ell2_ket_cspan by blast
ultimately show ‹∃φ∈cspan (range ket). dist φ ψ < e›
by auto
qed
lemma ccspan_range_ket[simp]: "ccspan (range ket) = (top::('a ell2 ccsubspace))"
proof-
have ‹closure (complex_vector.span (range ket)) = (UNIV::'a ell2 set)›
using Complex_L2.closed_cspan_range_ket by blast
thus ?thesis
by (simp add: ccspan.abs_eq top_ccsubspace.abs_eq)
qed
lemma cspan_range_ket_finite[simp]: "cspan (range ket :: 'a::finite ell2 set) = UNIV"
by (metis closed_cspan_range_ket closure_finite_cspan finite_class.finite_UNIV finite_imageI)
instance ell2 :: (finite) cfinite_dim
proof
define basis :: ‹'a ell2 set› where ‹basis = range ket›
have ‹finite basis›
unfolding basis_def by simp
moreover have ‹cspan basis = UNIV›
by (simp add: basis_def)
ultimately show ‹∃basis::'a ell2 set. finite basis ∧ cspan basis = UNIV›
by auto
qed
instantiation ell2 :: (enum) onb_enum begin
definition "canonical_basis_ell2 = map ket Enum.enum"
instance
proof
show "distinct (canonical_basis::'a ell2 list)"
proof-
have ‹finite (UNIV::'a set)›
by simp
have ‹distinct (enum_class.enum::'a list)›
using enum_distinct by blast
moreover have ‹inj_on ket (set enum_class.enum)›
by (meson inj_onI ket_injective)
ultimately show ?thesis
unfolding canonical_basis_ell2_def
using distinct_map
by blast
qed
show "is_ortho_set (set (canonical_basis::'a ell2 list))"
apply (auto simp: canonical_basis_ell2_def enum_UNIV)
by (smt (z3) norm_ket f_inv_into_f is_ortho_set_def orthogonal_ket norm_zero)
show "cindependent (set (canonical_basis::'a ell2 list))"
apply (auto simp: canonical_basis_ell2_def enum_UNIV)
by (smt (verit, best) norm_ket f_inv_into_f is_ortho_set_def is_ortho_set_cindependent orthogonal_ket norm_zero)
show "cspan (set (canonical_basis::'a ell2 list)) = UNIV"
by (auto simp: canonical_basis_ell2_def enum_UNIV)
show "norm (x::'a ell2) = 1"
if "(x::'a ell2) ∈ set canonical_basis"
for x :: "'a ell2"
using that unfolding canonical_basis_ell2_def
by auto
qed
end
lemma canonical_basis_length_ell2[code_unfold, simp]:
"length (canonical_basis ::'a::enum ell2 list) = CARD('a)"
unfolding canonical_basis_ell2_def apply simp
using card_UNIV_length_enum by metis
lemma ket_canonical_basis: "ket x = canonical_basis ! enum_idx x"
proof-
have "x = (enum_class.enum::'a list) ! enum_idx x"
using enum_idx_correct[where i = x] by simp
hence p1: "ket x = ket ((enum_class.enum::'a list) ! enum_idx x)"
by simp
have "enum_idx x < length (enum_class.enum::'a list)"
using enum_idx_bound[where x = x].
hence "(map ket (enum_class.enum::'a list)) ! enum_idx x
= ket ((enum_class.enum::'a list) ! enum_idx x)"
by auto
thus ?thesis
unfolding canonical_basis_ell2_def using p1 by auto
qed
lemma clinear_equal_ket:
fixes f g :: ‹'a::finite ell2 ⇒ _›
assumes ‹clinear f›
assumes ‹clinear g›
assumes ‹⋀i. f (ket i) = g (ket i)›
shows ‹f = g›
apply (rule ext)
apply (rule complex_vector.linear_eq_on_span[where f=f and g=g and B=‹range ket›])
using assms by auto
lemma equal_ket:
fixes A B :: ‹('a ell2, 'b::complex_normed_vector) cblinfun›
assumes ‹⋀ x. cblinfun_apply A (ket x) = cblinfun_apply B (ket x)›
shows ‹A = B›
apply (rule cblinfun_eq_gen_eqI[where G=‹range ket›])
using assms by auto
lemma antilinear_equal_ket:
fixes f g :: ‹'a::finite ell2 ⇒ _›
assumes ‹antilinear f›
assumes ‹antilinear g›
assumes ‹⋀i. f (ket i) = g (ket i)›
shows ‹f = g›
proof -
have [simp]: ‹clinear (f ∘ from_conjugate_space)›
apply (rule antilinear_o_antilinear)
using assms by (simp_all add: antilinear_from_conjugate_space)
have [simp]: ‹clinear (g ∘ from_conjugate_space)›
apply (rule antilinear_o_antilinear)
using assms by (simp_all add: antilinear_from_conjugate_space)
have [simp]: ‹cspan (to_conjugate_space ` (range ket :: 'a ell2 set)) = UNIV›
by simp
have "f o from_conjugate_space = g o from_conjugate_space"
apply (rule ext)
apply (rule complex_vector.linear_eq_on_span[where f="f o from_conjugate_space" and g="g o from_conjugate_space" and B=‹to_conjugate_space ` range ket›])
apply (simp, simp)
using assms(3) by (auto simp: to_conjugate_space_inverse)
then show "f = g"
by (smt (verit) UNIV_I from_conjugate_space_inverse surj_def surj_fun_eq to_conjugate_space_inject)
qed
lemma cinner_ket_adjointI:
fixes F::"'a ell2 ⇒⇩C⇩L _" and G::"'b ell2 ⇒⇩C⇩L_"
assumes "⋀ i j. ⟨F *⇩V ket i, ket j⟩ = ⟨ket i, G *⇩V ket j⟩"
shows "F = G*"
proof -
from assms
have ‹(F *⇩V x) ∙⇩C y = x ∙⇩C (G *⇩V y)› if ‹x ∈ range ket› and ‹y ∈ range ket› for x y
using that by auto
then have ‹(F *⇩V x) ∙⇩C y = x ∙⇩C (G *⇩V y)› if ‹x ∈ range ket› for x y
apply (rule bounded_clinear_eq_on[where G=‹range ket› and t=y, rotated 2])
using that by (auto intro!: bounded_linear_intros)
then have ‹(F *⇩V x) ∙⇩C y = x ∙⇩C (G *⇩V y)› for x y
apply (rule bounded_antilinear_eq_on[where G=‹range ket› and t=x, rotated 2])
by (auto intro!: bounded_linear_intros)
then show ?thesis
by (rule adjoint_eqI)
qed
lemma ket_nonzero[simp]: "ket i ≠ 0"
using norm_ket[of i] by force
lemma cindependent_ket:
"cindependent (range (ket::'a⇒_))"
proof-
define S where "S = range (ket::'a⇒_)"
have "is_ortho_set S"
unfolding S_def is_ortho_set_def by auto
moreover have "0 ∉ S"
unfolding S_def
using ket_nonzero
by (simp add: image_iff)
ultimately show ?thesis
using is_ortho_set_cindependent[where A = S] unfolding S_def
by blast
qed
lemma cdim_UNIV_ell2[simp]: ‹cdim (UNIV::'a::finite ell2 set) = CARD('a)›
apply (subst cspan_range_ket_finite[symmetric])
by (metis card_image cindependent_ket complex_vector.dim_span_eq_card_independent inj_ket)
lemma is_ortho_set_ket[simp]: ‹is_ortho_set (range ket)›
using is_ortho_set_def by fastforce
subsection ‹Butterflies›
lemma cspan_butterfly_ket: ‹cspan {butterfly (ket i) (ket j)| (i::'b::finite) (j::'a::finite). True} = UNIV›
proof -
have *: ‹{butterfly (ket i) (ket j)| (i::'b::finite) (j::'a::finite). True} = {butterfly a b |a b. a ∈ range ket ∧ b ∈ range ket}›
by auto
show ?thesis
apply (subst *)
apply (rule cspan_butterfly_UNIV)
by auto
qed
lemma cindependent_butterfly_ket: ‹cindependent {butterfly (ket i) (ket j)| (i::'b) (j::'a). True}›
proof -
have *: ‹{butterfly (ket i) (ket j)| (i::'b) (j::'a). True} = {butterfly a b |a b. a ∈ range ket ∧ b ∈ range ket}›
by auto
show ?thesis
apply (subst *)
apply (rule cindependent_butterfly)
by auto
qed
lemma clinear_eq_butterfly_ketI:
fixes F G :: ‹('a::finite ell2 ⇒⇩C⇩L 'b::finite ell2) ⇒ 'c::complex_vector›
assumes "clinear F" and "clinear G"
assumes "⋀i j. F (butterfly (ket i) (ket j)) = G (butterfly (ket i) (ket j))"
shows "F = G"
apply (rule complex_vector.linear_eq_on_span[where f=F, THEN ext, rotated 3])
apply (subst cspan_butterfly_ket)
using assms by auto
lemma sum_butterfly_ket[simp]: ‹(∑(i::'a::finite)∈UNIV. butterfly (ket i) (ket i)) = id_cblinfun›
apply (rule equal_ket)
apply (subst complex_vector.linear_sum[where f=‹λy. y *⇩V ket _›])
apply (auto simp add: scaleC_cblinfun.rep_eq cblinfun.add_left clinearI butterfly_def cblinfun_compose_image cinner_ket)
apply (subst sum.mono_neutral_cong_right[where S=‹{_}›])
by auto
subsection ‹One-dimensional spaces›
instantiation ell2 :: ("{enum,CARD_1}") one_dim begin
text ‹Note: enum is not needed logically, but without it this instantiation
clashes with ‹instantiation ell2 :: (enum) onb_enum››
instance
proof
show "canonical_basis = [1::'a ell2]"
unfolding canonical_basis_ell2_def
apply transfer
by (simp add: enum_CARD_1[of undefined])
show "a *⇩C 1 * b *⇩C 1 = (a * b) *⇩C (1::'a ell2)" for a b
apply (transfer fixing: a b) by simp
show "x / y = x * inverse y" for x y :: "'a ell2"
by (simp add: divide_inverse)
show "inverse (c *⇩C 1) = inverse c *⇩C (1::'a ell2)" for c :: complex
apply transfer by auto
qed
end
subsection ‹Classical operators›
text ‹We call an operator mapping \<^term>‹ket x› to \<^term>‹ket (π x)› or \<^term>‹0› "classical".
(The meaning is inspired by the fact that in quantum mechanics, such operators usually correspond
to operations with classical interpretation (such as Pauli-X, CNOT, measurement in the computational
basis, etc.))›
definition classical_operator :: "('a⇒'b option) ⇒ 'a ell2 ⇒⇩C⇩L'b ell2" where
"classical_operator π =
(let f = (λt. (case π (inv (ket::'a⇒_) t)
of None ⇒ (0::'b ell2)
| Some i ⇒ ket i))
in
cblinfun_extension (range (ket::'a⇒_)) f)"
definition "classical_operator_exists π ⟷
cblinfun_extension_exists (range ket)
(λt. case π (inv ket t) of None ⇒ 0 | Some i ⇒ ket i)"
lemma classical_operator_existsI:
assumes "⋀x. B *⇩V (ket x) = (case π x of Some i ⇒ ket i | None ⇒ 0)"
shows "classical_operator_exists π"
unfolding classical_operator_exists_def
apply (rule cblinfun_extension_existsI[of _ B])
using assms
by (auto simp: inv_f_f[OF inj_ket])
lemma classical_operator_exists_inj:
assumes "inj_map π"
shows "classical_operator_exists π"
proof -
define f where ‹f t = (case π (inv ket t) of None ⇒ 0 | Some x ⇒ ket x)› for t
define g where ‹g = cconstruct (range ket) f›
have g_f: ‹g (ket x) = f (ket x)› for x
unfolding g_def apply (rule complex_vector.construct_basis)
using cindependent_ket by auto
have ‹clinear g›
unfolding g_def apply (rule complex_vector.linear_construct)
using cindependent_ket by blast
then have ‹g (x + y) = g x + g y› if ‹x ∈ cspan (range ket)› and ‹y ∈ cspan (range ket)› for x y
using clinear_iff by blast
moreover from ‹clinear g› have ‹g (c *⇩C x) = c *⇩C g x› if ‹x ∈ cspan (range ket)› for x c
by (simp add: complex_vector.linear_scale)
moreover have ‹norm (g x) ≤ norm x› if ‹x ∈ cspan (range ket)› for x
proof -
from that obtain t r where x_sum: ‹x = (∑a∈t. r a *⇩C a)› and ‹finite t› and ‹t ⊆ range ket›
unfolding complex_vector.span_explicit by auto
then obtain T where tT: ‹t = ket ` T› and [simp]: ‹finite T›
by (meson finite_subset_image)
define R where ‹R i = r (ket i)› for i
have x_sum: ‹x = (∑i∈T. R i *⇩C ket i)›
unfolding R_def tT x_sum
apply (rule sum.reindex_cong)
by (auto simp add: inj_on_def)
define T' π' πT πR where ‹T' = {i∈T. π i ≠ None}› and ‹π' = the o π› and ‹πT = π' ` T'› and ‹πR i = R (inv_into T' π' i)› for i
have ‹inj_on π' T'›
by (smt (z3) T'_def π'_def assms comp_apply inj_map_def inj_on_def mem_Collect_eq option.expand)
have [simp]: ‹finite πT›
by (simp add: T'_def πT_def)
have ‹g x = (∑i∈T. R i *⇩C g (ket i))›
by (smt (verit, ccfv_threshold) ‹clinear g› complex_vector.linear_scale complex_vector.linear_sum sum.cong x_sum)
also have ‹… = (∑i∈T. R i *⇩C f (ket i))›
using g_f by presburger
also have ‹… = (∑i∈T. R i *⇩C (case π i of None ⇒ 0 | Some x ⇒ ket x))›
unfolding f_def by auto
also have ‹… = (∑i∈T'. R i *⇩C ket (π' i))›
apply (rule sum.mono_neutral_cong_right)
unfolding T'_def π'_def
by auto
also have ‹… = (∑i∈π' ` T'. R (inv_into T' π' i) *⇩C ket i)›
apply (subst sum.reindex)
using ‹inj_on π' T'› apply assumption
apply (rule sum.cong)
using ‹inj_on π' T'› by auto
finally have gx_sum: ‹g x = (∑i∈πT. πR i *⇩C ket i)›
using πR_def πT_def by auto
have ‹(norm (g x))⇧2 = (∑a∈πT. (cmod (πR a))⇧2)›
unfolding gx_sum
apply (subst pythagorean_theorem_sum)
by auto
also have ‹… = (∑i∈T'. (cmod (R i))⇧2)›
unfolding πR_def πT_def
apply (subst sum.reindex)
using ‹inj_on π' T'› apply assumption
apply (rule sum.cong)
using ‹inj_on π' T'› by auto
also have ‹… ≤ (∑a∈T. (cmod (R a))⇧2)›
apply (rule sum_mono2)
using T'_def by auto
also have ‹… = (norm x)⇧2›
unfolding x_sum
apply (subst pythagorean_theorem_sum)
using ‹finite T› by auto
finally show ‹norm (g x) ≤ norm x›
by auto
qed
ultimately have ‹cblinfun_extension_exists (cspan (range ket)) g›
apply (rule_tac cblinfun_extension_exists_bounded_dense[where B=1])
by auto
then have ‹cblinfun_extension_exists (range ket) f›
by (metis (mono_tags, opaque_lifting) g_f cblinfun_extension_apply cblinfun_extension_existsI complex_vector.span_base rangeE)
then show ‹classical_operator_exists π›
unfolding classical_operator_exists_def f_def by simp
qed
lemma classical_operator_exists_finite[simp]: "classical_operator_exists (π :: _::finite ⇒ _)"
unfolding classical_operator_exists_def
apply (rule cblinfun_extension_exists_finite_dim)
using cindependent_ket apply blast
using finite_class.finite_UNIV finite_imageI closed_cspan_range_ket closure_finite_cspan by blast
lemma classical_operator_ket:
assumes "classical_operator_exists π"
shows "(classical_operator π) *⇩V (ket x) = (case π x of Some i ⇒ ket i | None ⇒ 0)"
unfolding classical_operator_def
using f_inv_into_f ket_injective rangeI
by (metis assms cblinfun_extension_apply classical_operator_exists_def)
lemma classical_operator_ket_finite:
"(classical_operator π) *⇩V (ket (x::'a::finite)) = (case π x of Some i ⇒ ket i | None ⇒ 0)"
by (rule classical_operator_ket, simp)
lemma classical_operator_adjoint[simp]:
fixes π :: "'a ⇒ 'b option"
assumes a1: "inj_map π"
shows "(classical_operator π)* = classical_operator (inv_map π)"
proof-
define F where "F = classical_operator (inv_map π)"
define G where "G = classical_operator π"
have "⟨F *⇩V ket i, ket j⟩ = ⟨ket i, G *⇩V ket j⟩" for i j
proof-
have w1: "(classical_operator (inv_map π)) *⇩V (ket i)
= (case inv_map π i of Some k ⇒ ket k | None ⇒ 0)"
by (simp add: classical_operator_ket classical_operator_exists_inj)
have w2: "(classical_operator π) *⇩V (ket j)
= (case π j of Some k ⇒ ket k | None ⇒ 0)"
by (simp add: assms classical_operator_ket classical_operator_exists_inj)
have "⟨F *⇩V ket i, ket j⟩ = ⟨classical_operator (inv_map π) *⇩V ket i, ket j⟩"
unfolding F_def by blast
also have "… = ⟨(case inv_map π i of Some k ⇒ ket k | None ⇒ 0), ket j⟩"
using w1 by simp
also have "… = ⟨ket i, (case π j of Some k ⇒ ket k | None ⇒ 0)⟩"
proof(induction "inv_map π i")
case None
hence pi1: "None = inv_map π i".
show ?case
proof (induction "π j")
case None
thus ?case
using pi1 by auto
next
case (Some c)
have "c ≠ i"
proof(rule classical)
assume "¬(c ≠ i)"
hence "c = i"
by blast
hence "inv_map π c = inv_map π i"
by simp
hence "inv_map π c = None"
by (simp add: pi1)
moreover have "inv_map π c = Some j"
using Some.hyps unfolding inv_map_def
apply auto
by (metis a1 f_inv_into_f inj_map_def option.distinct(1) rangeI)
ultimately show ?thesis by simp
qed
thus ?thesis
by (metis None.hyps Some.hyps cinner_zero_left orthogonal_ket option.simps(4)
option.simps(5))
qed
next
case (Some d)
hence s1: "Some d = inv_map π i".
show "⟨case inv_map π i of
None ⇒ 0
| Some a ⇒ ket a, ket j⟩ =
⟨ket i, case π j of
None ⇒ 0
| Some a ⇒ ket a⟩"
proof(induction "π j")
case None
have "d ≠ j"
proof(rule classical)
assume "¬(d ≠ j)"
hence "d = j"
by blast
hence "π d = π j"
by simp
hence "π d = None"
by (simp add: None.hyps)
moreover have "π d = Some i"
using Some.hyps unfolding inv_map_def
apply auto
by (metis f_inv_into_f option.distinct(1) option.inject)
ultimately show ?thesis
by simp
qed
thus ?case
by (metis None.hyps Some.hyps cinner_zero_right orthogonal_ket option.case_eq_if
option.simps(5))
next
case (Some c)
hence s2: "π j = Some c" by simp
have "⟨ket d, ket j⟩ = ⟨ket i, ket c⟩"
proof(cases "π j = Some i")
case True
hence ij: "Some j = inv_map π i"
unfolding inv_map_def apply auto
apply (metis a1 f_inv_into_f inj_map_def option.discI range_eqI)
by (metis range_eqI)
have "i = c"
using True s2 by auto
moreover have "j = d"
by (metis option.inject s1 ij)
ultimately show ?thesis
by (simp add: cinner_ket_same)
next
case False
moreover have "π d = Some i"
using s1 unfolding inv_map_def
by (metis f_inv_into_f option.distinct(1) option.inject)
ultimately have "j ≠ d"
by auto
moreover have "i ≠ c"
using False s2 by auto
ultimately show ?thesis
by (metis orthogonal_ket)
qed
hence "⟨case Some d of None ⇒ 0
| Some a ⇒ ket a, ket j⟩ =
⟨ket i, case Some c of None ⇒ 0 | Some a ⇒ ket a⟩"
by simp
thus "⟨case inv_map π i of None ⇒ 0
| Some a ⇒ ket a, ket j⟩ =
⟨ket i, case π j of None ⇒ 0 | Some a ⇒ ket a⟩"
by (simp add: Some.hyps s1)
qed
qed
also have "… = ⟨ket i, classical_operator π *⇩V ket j⟩"
by (simp add: w2)
also have "… = ⟨ket i, G *⇩V ket j⟩"
unfolding G_def by blast
finally show ?thesis .
qed
hence "G* = F"
using cinner_ket_adjointI
by auto
thus ?thesis unfolding G_def F_def .
qed
lemma
fixes π::"'b ⇒ 'c option" and ρ::"'a ⇒ 'b option"
assumes "classical_operator_exists π"
assumes "classical_operator_exists ρ"
shows classical_operator_exists_comp[simp]: "classical_operator_exists (π ∘⇩m ρ)"
and classical_operator_mult[simp]: "classical_operator π o⇩C⇩L classical_operator ρ = classical_operator (π ∘⇩m ρ)"
proof -
define Cπ Cρ Cπρ where "Cπ = classical_operator π" and "Cρ = classical_operator ρ"
and "Cπρ = classical_operator (π ∘⇩m ρ)"
have Cπx: "Cπ *⇩V (ket x) = (case π x of Some i ⇒ ket i | None ⇒ 0)" for x
unfolding Cπ_def using ‹classical_operator_exists π› by (rule classical_operator_ket)
have Cρx: "Cρ *⇩V (ket x) = (case ρ x of Some i ⇒ ket i | None ⇒ 0)" for x
unfolding Cρ_def using ‹classical_operator_exists ρ› by (rule classical_operator_ket)
have Cπρx': "(Cπ o⇩C⇩L Cρ) *⇩V (ket x) = (case (π ∘⇩m ρ) x of Some i ⇒ ket i | None ⇒ 0)" for x
apply (simp add: scaleC_cblinfun.rep_eq Cρx)
apply (cases "ρ x")
by (auto simp: Cπx)
thus ‹classical_operator_exists (π ∘⇩m ρ)›
by (rule classical_operator_existsI)
hence "Cπρ *⇩V (ket x) = (case (π ∘⇩m ρ) x of Some i ⇒ ket i | None ⇒ 0)" for x
unfolding Cπρ_def
by (rule classical_operator_ket)
with Cπρx' have "(Cπ o⇩C⇩L Cρ) *⇩V (ket x) = Cπρ *⇩V (ket x)" for x
by simp
thus "Cπ o⇩C⇩L Cρ = Cπρ"
by (simp add: equal_ket)
qed
lemma classical_operator_Some[simp]: "classical_operator (Some::'a⇒_) = id_cblinfun"
proof-
have "(classical_operator Some) *⇩V (ket i) = id_cblinfun *⇩V (ket i)"
for i::'a
apply (subst classical_operator_ket)
apply (rule classical_operator_exists_inj)
by auto
thus ?thesis
using equal_ket[where A = "classical_operator (Some::'a ⇒ _ option)"
and B = "id_cblinfun::'a ell2 ⇒⇩C⇩L _"]
by blast
qed
lemma isometry_classical_operator[simp]:
fixes π::"'a ⇒ 'b"
assumes a1: "inj π"
shows "isometry (classical_operator (Some o π))"
proof -
have b0: "inj_map (Some ∘ π)