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"
"HOL-Library.Infinite_Typeclass"
begin
unbundle lattice_syntax and cblinfun_syntax and no blinfun_apply_syntax
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 f = sqrt (∑⇩∞x. norm (f x)^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 (f::'a::finite⇒_)"
unfolding has_ell2_norm_def by simp
lemma ell2_norm_finite:
"ell2_norm (f::'a::finite⇒complex) = sqrt (∑x∈UNIV. (norm (f x))^2)"
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_norm_square: ‹(ell2_norm x)⇧2 = (∑⇩∞i. (cmod (x i))⇧2)›
unfolding ell2_norm_def
apply (subst real_sqrt_pow2)
by (simp_all add: infsum_nonneg)
lemma ell2_ket:
fixes a
defines ‹f ≡ (λi. of_bool (a = i))›
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 = ‹{f::'a⇒complex. has_ell2_norm f}›
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 .
definition "dist x y = norm (x - y)" for x y::"'a ell2"
definition "sgn x = x /⇩R norm x" for x::"'a ell2"
definition "uniformity = (INF e∈{0<..}. principal {(x::'a ell2, y). norm (x - y) < e})"
definition "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
‹λf g. ∑⇩∞x. cnj (f x) * g x› .
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 intro_classes
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
lemma sum_ell2_transfer[transfer_rule]:
includes lifting_syntax
shows ‹(((=) ===> pcr_ell2 (=)) ===> rel_set (=) ===> pcr_ell2 (=))
(λf X x. sum (λy. f y x) X) sum›
proof (intro rel_funI, rename_tac f f' X X')
fix f and f' :: ‹'a ⇒ 'b ell2›
assume [transfer_rule]: ‹((=) ===> pcr_ell2 (=)) f f'›
fix X X' :: ‹'a set›
assume ‹rel_set (=) X X'›
then have [simp]: ‹X' = X›
by (simp add: rel_set_eq)
show ‹pcr_ell2 (=) (λx. ∑y∈X. f y x) (sum f' X')›
unfolding ‹X' = X›
proof (induction X rule: infinite_finite_induct)
case (infinite X)
show ?case
apply (simp add: infinite)
by transfer_prover
next
case empty
show ?case
apply (simp add: empty)
by transfer_prover
next
case (insert x F)
note [transfer_rule] = insert.IH
show ?case
apply (simp add: insert)
by transfer_prover
qed
qed
lemma clinear_Rep_ell2[simp]: ‹clinear (λψ. Rep_ell2 ψ i)›
by (simp add: clinearI plus_ell2.rep_eq scaleC_ell2.rep_eq)
lemma Abs_ell2_inverse_finite[simp]: ‹Rep_ell2 (Abs_ell2 ψ) = ψ› for ψ :: ‹_::finite ⇒ complex›
by (simp add: Abs_ell2_inverse)
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 trunc_ell2_UNIV[simp]: ‹trunc_ell2 UNIV ψ = ψ›
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) ∙⇩C (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
lemma trunc_ell2_lim_seq: ‹((λn. trunc_ell2 {..<n} ψ) ⇢ ψ)›
using trunc_ell2_lim_at_UNIV filterlim_lessThan_at_top
by (rule filterlim_compose)
lemma trunc_ell2_norm_mono: ‹M ⊆ N ⟹ norm (trunc_ell2 M ψ) ≤ norm (trunc_ell2 N ψ)›
proof (rule power2_le_imp_le[rotated], force, transfer)
fix M N :: ‹'a set› and ψ :: ‹'a ⇒ complex›
assume ‹M ⊆ N› and ‹has_ell2_norm ψ›
have ‹(ell2_norm (λi. if i ∈ M then ψ i else 0))⇧2 = (∑⇩∞i∈M. (cmod (ψ i))⇧2)›
unfolding ell2_norm_square
apply (rule infsum_cong_neutral)
by auto
also have ‹… ≤ (∑⇩∞i∈N. (cmod (ψ i))⇧2)›
apply (rule infsum_mono2)
using ‹has_ell2_norm ψ› ‹M ⊆ N›
by (auto simp add: ell2_norm_square has_ell2_norm_def simp flip: norm_power intro: summable_on_subset_banach)
also have ‹… = (ell2_norm (λi. if i ∈ N then ψ i else 0))⇧2›
unfolding ell2_norm_square
apply (rule infsum_cong_neutral)
by auto
finally show ‹(ell2_norm (λi. if i ∈ M then ψ i else 0))⇧2 ≤ (ell2_norm (λi. if i ∈ N then ψ i else 0))⇧2›
by -
qed
lemma trunc_ell2_reduces_norm: ‹norm (trunc_ell2 M ψ) ≤ norm ψ›
by (metis subset_UNIV trunc_ell2_UNIV trunc_ell2_norm_mono)
lemma trunc_ell2_twice[simp]: ‹trunc_ell2 M (trunc_ell2 N ψ) = trunc_ell2 (M∩N) ψ›
apply transfer by auto
lemma trunc_ell2_union: ‹trunc_ell2 (M ∪ N) ψ = trunc_ell2 M ψ + trunc_ell2 N ψ - trunc_ell2 (M∩N) ψ›
apply transfer by auto
lemma trunc_ell2_union_disjoint: ‹M ∩ N = {} ⟹ trunc_ell2 (M ∪ N) ψ = trunc_ell2 M ψ + trunc_ell2 N ψ›
by (simp add: trunc_ell2_union)
lemma trunc_ell2_union_Diff: ‹M ⊆ N ⟹ trunc_ell2 (N-M) ψ = trunc_ell2 N ψ - trunc_ell2 M ψ›
using trunc_ell2_union_disjoint[where M=‹N-M› and N=M and ψ=ψ]
by (simp add: Un_commute inf.commute le_iff_sup)
lemma trunc_ell2_add: ‹trunc_ell2 M (ψ + φ) = trunc_ell2 M ψ + trunc_ell2 M φ›
apply transfer by auto
lemma trunc_ell2_scaleC: ‹trunc_ell2 M (c *⇩C ψ) = c *⇩C trunc_ell2 M ψ›
apply transfer by auto
lemma bounded_clinear_trunc_ell2[bounded_clinear]: ‹bounded_clinear (trunc_ell2 M)›
by (auto intro!: bounded_clinearI[where K=1] trunc_ell2_reduces_norm
simp: trunc_ell2_add trunc_ell2_scaleC)
lemma trunc_ell2_lim: ‹((λS. trunc_ell2 S ψ) ⤏ trunc_ell2 M ψ) (finite_subsets_at_top M)›
proof -
have ‹((λS. trunc_ell2 S (trunc_ell2 M ψ)) ⤏ trunc_ell2 M ψ) (finite_subsets_at_top UNIV)›
using trunc_ell2_lim_at_UNIV by blast
then have ‹((λS. trunc_ell2 (S∩M) ψ) ⤏ trunc_ell2 M ψ) (finite_subsets_at_top UNIV)›
by simp
then show ‹((λS. trunc_ell2 S ψ) ⤏ trunc_ell2 M ψ) (finite_subsets_at_top M)›
unfolding filterlim_def
apply (subst (asm) filtermap_filtermap[where g=‹λS. S∩M›, symmetric])
apply (subst (asm) finite_subsets_at_top_inter[where A=M and B=UNIV])
by auto
qed
lemma trunc_ell2_lim_general:
assumes big: ‹⋀G. finite G ⟹ G ⊆ M ⟹ (∀⇩F H in F. H ⊇ G)›
assumes small: ‹∀⇩F H in F. H ⊆ M›
shows ‹((λS. trunc_ell2 S ψ) ⤏ trunc_ell2 M ψ) F›
proof (rule tendstoI)
fix e :: real assume ‹e > 0›
from trunc_ell2_lim[THEN tendsto_iff[THEN iffD1], rule_format, OF ‹e > 0›, where M=M and ψ=ψ]
obtain G where ‹finite G› and ‹G ⊆ M› and
close: ‹dist (trunc_ell2 G ψ) (trunc_ell2 M ψ) < e›
apply atomize_elim
unfolding eventually_finite_subsets_at_top
by blast
from ‹finite G› ‹G ⊆ M› and big
have ‹∀⇩F H in F. H ⊇ G›
by -
with small have ‹∀⇩F H in F. H ⊆ M ∧ H ⊇ G›
by (simp add: eventually_conj_iff)
then show ‹∀⇩F H in F. dist (trunc_ell2 H ψ) (trunc_ell2 M ψ) < e›
proof (rule eventually_mono)
fix H assume GHM: ‹H ⊆ M ∧ H ⊇ G›
have ‹dist (trunc_ell2 H ψ) (trunc_ell2 M ψ) = norm (trunc_ell2 (M-H) ψ)›
by (simp add: GHM dist_ell2_def norm_minus_commute trunc_ell2_union_Diff)
also have ‹… ≤ norm (trunc_ell2 (M-G) ψ)›
by (simp add: Diff_mono GHM trunc_ell2_norm_mono)
also have ‹… = dist (trunc_ell2 G ψ) (trunc_ell2 M ψ)›
by (simp add: ‹G ⊆ M› dist_ell2_def norm_minus_commute trunc_ell2_union_Diff)
also have ‹… < e›
using close by simp
finally show ‹dist (trunc_ell2 H ψ) (trunc_ell2 M ψ) < e›
by -
qed
qed
lemma norm_ell2_bound_trunc:
assumes ‹⋀M. finite M ⟹ norm (trunc_ell2 M ψ) ≤ B›
shows ‹norm ψ ≤ B›
proof -
note trunc_ell2_lim_at_UNIV[of ψ]
then have ‹((λS. norm (trunc_ell2 S ψ)) ⤏ norm ψ) (finite_subsets_at_top UNIV)›
using tendsto_norm by auto
then show ‹norm ψ ≤ B›
apply (rule tendsto_upperbound)
using assms apply (rule eventually_finite_subsets_at_top_weakI)
by auto
qed
lemma trunc_ell2_uminus: ‹trunc_ell2 (-M) ψ = ψ - trunc_ell2 M ψ›
by (metis Int_UNIV_left boolean_algebra_class.diff_eq subset_UNIV trunc_ell2_UNIV trunc_ell2_union_Diff)
subsection ‹Kets and bras›
lift_definition ket :: ‹'a ⇒ 'a ell2› is ‹λx y. of_bool (x=y)›
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. of_bool ((undefined::'a) = y)) ≠ (λ_. 0)›
by (metis (mono_tags) of_bool_eq(2) zero_neq_one)
qed
thus ‹∃x y::'a ell2. x ≠ y›
by blast
qed
lemma cinner_ket_left: ‹ket i ∙⇩C ψ = Rep_ell2 ψ i›
apply (transfer fixing: i)
apply (subst infsum_cong_neutral[where T=‹{i}›])
by auto
lemma cinner_ket_right: ‹(ψ ∙⇩C ket i) = cnj (Rep_ell2 ψ i)›
apply (transfer fixing: i)
apply (subst infsum_cong_neutral[where T=‹{i}›])
by auto
lemma bounded_clinear_Rep_ell2[simp, bounded_clinear]: ‹bounded_clinear (λψ. Rep_ell2 ψ x)›
apply (subst asm_rl[of ‹(λψ. Rep_ell2 ψ x) = (λψ. ket x ∙⇩C ψ)›])
apply (auto simp: cinner_ket_left)
by (simp add: bounded_clinear_cinner_right)
lemma cinner_ket_eqI:
assumes ‹⋀i. ket i ∙⇩C ψ = ket i ∙⇩C φ›
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 ∙⇩C ket i) = 1›
proof-
have ‹norm (ket i) = 1›
by simp
hence ‹sqrt (cmod (ket i ∙⇩C ket i)) = 1›
by (metis norm_eq_sqrt_cinner)
hence ‹cmod (ket i ∙⇩C ket i) = 1›
using real_sqrt_eq_1_iff by blast
moreover have ‹(ket i ∙⇩C ket i) = cmod (ket i ∙⇩C ket i)›
proof-
have ‹(ket i ∙⇩C ket i) ∈ ℝ›
by (simp add: cinner_real)
thus ?thesis
by (metis ‹norm (ket i) = 1› cnorm_eq norm_one of_real_1 one_cinner_one)
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 of_bool_def)
lemma cinner_ket: ‹(ket i ∙⇩C ket j) = of_bool (i=j)›
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 of_bool_def)
lemma inj_ket[simp]: ‹inj_on ket M›
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"
definition ‹canonical_basis_length_ell2 (_ :: 'a ell2 itself) = length (Enum.enum :: 'a list)›
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
show ‹canonical_basis_length TYPE('a ell2) = length (canonical_basis :: 'a ell2 list)›
by (simp add: canonical_basis_length_ell2_def canonical_basis_ell2_def)
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] card_UNIV_length_enum
by metis
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. A *⇩V ket x = B *⇩V 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) ∙⇩C ket j = ket i ∙⇩C (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_closure[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[simp]:
"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
lemma bounded_clinear_equal_ket:
fixes f g :: ‹'a ell2 ⇒ _›
assumes ‹bounded_clinear f›
assumes ‹bounded_clinear g›
assumes ‹⋀i. f (ket i) = g (ket i)›
shows ‹f = g›
apply (rule ext)
apply (rule bounded_clinear_eq_on_closure[of f g ‹range ket›])
using assms by auto
lemma bounded_antilinear_equal_ket:
fixes f g :: ‹'a ell2 ⇒ _›
assumes ‹bounded_antilinear f›
assumes ‹bounded_antilinear g›
assumes ‹⋀i. f (ket i) = g (ket i)›
shows ‹f = g›
apply (rule ext)
apply (rule bounded_antilinear_eq_on[of f g ‹range ket›])
using assms by auto
lemma is_onb_ket[simp]: ‹is_onb (range ket)›
by (auto simp: is_onb_def)
lemma ell2_sum_ket: ‹ψ = (∑i∈UNIV. Rep_ell2 ψ i *⇩C ket i)› for ψ :: ‹_::finite ell2›
apply transfer apply (rule ext)
apply (subst sum_single)
by auto
lemma trunc_ell2_singleton: ‹trunc_ell2 {x} ψ = Rep_ell2 ψ x *⇩C ket x›
apply transfer by auto
lemma trunc_ell2_insert: ‹trunc_ell2 (insert x M) φ = Rep_ell2 φ x *⇩C ket x + trunc_ell2 M φ›
if ‹x ∉ M›
using trunc_ell2_union_disjoint[where M=‹{x}› and N=M]
using that by (auto simp: trunc_ell2_singleton)
lemma trunc_ell2_finite_sum: ‹trunc_ell2 M ψ = (∑i∈M. Rep_ell2 ψ i *⇩C ket i)› if ‹finite M›
using that apply induction by (auto simp: trunc_ell2_insert)
lemma is_orthogonal_trunc_ell2: ‹is_orthogonal (trunc_ell2 M ψ) (trunc_ell2 N φ)› if ‹M ∩ N = {}›
proof -
have *: ‹cnj (if i ∈ M then a else 0) * (if i ∈ N then b else 0) = 0› for a b i
using that by auto
show ?thesis
apply (transfer fixing: M N)
by (simp add: * )
qed
lemma separating_set_ket: ‹separating_set bounded_clinear (range ket)›
by (simp add: bounded_clinear_equal_ket separating_setI)
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
lemma ell2_decompose_has_sum: ‹((λx. Rep_ell2 φ x *⇩C ket x) has_sum φ) UNIV›
proof (unfold has_sum_def)
have *: ‹trunc_ell2 M φ = (∑x∈M. Rep_ell2 φ x *⇩C ket x)› if ‹finite M› for M
using that apply induction
by (auto simp: trunc_ell2_insert)
show ‹(sum (λx. Rep_ell2 φ x *⇩C ket x) ⤏ φ) (finite_subsets_at_top UNIV)›
apply (rule Lim_transform_eventually)
apply (rule trunc_ell2_lim_at_UNIV)
using * by (rule eventually_finite_subsets_at_top_weakI)
qed
lemma ell2_decompose_infsum: ‹φ = (∑⇩∞x. Rep_ell2 φ x *⇩C ket x)›
by (metis ell2_decompose_has_sum infsumI)
lemma ell2_decompose_summable: ‹(λx. Rep_ell2 φ x *⇩C ket x) summable_on UNIV›
using ell2_decompose_has_sum summable_on_def by blast
lemma Rep_ell2_cblinfun_apply_sum: ‹Rep_ell2 (A *⇩V φ) y = (∑⇩∞x. Rep_ell2 φ x * Rep_ell2 (A *⇩V ket x) y)›
proof -
have 1: ‹bounded_linear (λz. Rep_ell2 (A *⇩V z) y)›
by (auto intro!: bounded_clinear_compose[unfolded o_def, OF bounded_clinear_Rep_ell2]
cblinfun.bounded_clinear_right bounded_clinear.bounded_linear)
have 2: ‹(λx. Rep_ell2 φ x *⇩C ket x) summable_on UNIV›
by (simp add: ell2_decompose_summable)
have ‹Rep_ell2 (A *⇩V φ) y = Rep_ell2 (A *⇩V (∑⇩∞x. Rep_ell2 φ x *⇩C ket x)) y›
by (simp flip: ell2_decompose_infsum)
also have ‹… = (∑⇩∞x. Rep_ell2 (A *⇩V (Rep_ell2 φ x *⇩C ket x)) y)›
apply (subst infsum_bounded_linear[symmetric, where h=‹λz. Rep_ell2 (A *⇩V z) y›])
using 1 2 by (auto simp: o_def)
also have ‹… = (∑⇩∞x. Rep_ell2 φ x * Rep_ell2 (A *⇩V ket x) y)›
by (simp add: cblinfun.scaleC_right scaleC_ell2.rep_eq)
finally show ?thesis
by -
qed
subsection ‹One-dimensional spaces›
instantiation ell2 :: (CARD_1) one begin
lift_definition one_ell2 :: "'a ell2" is "λ_. 1" by simp
instance..
end
lemma ket_CARD_1_is_1: ‹ket x = 1› for x :: ‹'a::CARD_1›
apply transfer by simp
instantiation ell2 :: (CARD_1) times begin
lift_definition times_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ 'a ell2" is "λa b x. a x * b x"
by simp
instance..
end
instantiation ell2 :: (CARD_1) divide begin
lift_definition divide_ell2 :: "'a ell2 ⇒ 'a ell2 ⇒ 'a ell2" is "λa b x. a x / b x"
by simp
instance..
end
instantiation ell2 :: (CARD_1) inverse begin
lift_definition inverse_ell2 :: "'a ell2 ⇒ 'a ell2" is "λa x. inverse (a x)"
by simp
instance..
end
instance ell2 :: ("{enum,CARD_1}") one_dim
text ‹Note: enum is not needed logically, but without it this instantiation
clashes with ‹instantiation ell2 :: (enum) onb_enum››
proof intro_classes
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"
apply transfer
by (simp add: divide_inverse)
show "inverse (c *⇩C 1) = inverse c *⇩C (1::'a ell2)" for c :: complex
apply transfer by auto
qed
subsection ‹Explicit bounded operators›
definition explicit_cblinfun :: ‹('a ⇒ 'b ⇒ complex) ⇒ ('b ell2, 'a ell2) cblinfun› where
‹explicit_cblinfun M = cblinfun_extension (range ket) (λa. Abs_ell2 (λj. M j (inv ket a)))›
definition explicit_cblinfun_exists :: ‹('a ⇒ 'b ⇒ complex) ⇒ bool› where
‹explicit_cblinfun_exists M ⟷
(∀a. has_ell2_norm (λj. M j a)) ∧
cblinfun_extension_exists (range ket) (λa. Abs_ell2 (λj. M j (inv ket a)))›
lemma explicit_cblinfun_exists_bounded:
assumes ‹⋀S T ψ. finite S ⟹ finite T ⟹ (⋀a. a∉T ⟹ ψ a = 0) ⟹
(∑b∈S. (cmod (∑a∈T. ψ a *⇩C M b a))⇧2) ≤ B * (∑a∈T. (cmod (ψ a))⇧2)›
shows ‹explicit_cblinfun_exists M›
proof -
define F f where ‹F = complex_vector.construct (range ket) f›
and ‹f = (λa. Abs_ell2 (λj. M j (inv ket a)))›
from assms[where S=‹{}› and T=‹{undefined}› and ψ=‹λx. of_bool (x=undefined)›]
have ‹B ≥ 0›
by auto
have has_norm: ‹has_ell2_norm (λb. M b a)› for a
proof (unfold has_ell2_norm_def, intro nonneg_bdd_above_summable_on bdd_aboveI)
show ‹0 ≤ cmod ((M x a)⇧2)› for x
by simp
fix B'
assume ‹B' ∈ sum (λx. cmod ((M x a)⇧2)) ` {F. F ⊆ UNIV ∧ finite F}›
then obtain S where [simp]: ‹finite S› and B'_def: ‹B' = (∑x∈S. cmod ((M x a)⇧2))›
by blast
from assms[where S=S and T=‹{a}› and ψ=‹λx. of_bool (x=a)›]
show ‹B' ≤ B›
by (simp add: norm_power B'_def)
qed
have ‹clinear F›
by (auto intro!: complex_vector.linear_construct simp: F_def)
have F_B: ‹norm (F ψ) ≤ (sqrt B) * norm ψ› if ψ_range_ket: ‹ψ ∈ cspan (range ket)› for ψ
proof -
from that
obtain T' where ‹finite T'› and ‹T' ⊆ range ket› and ψT': ‹ψ ∈ cspan T'›
by (meson vector_finitely_spanned)
then obtain T where T'_def: ‹T' = ket ` T›
by (meson subset_image_iff)
have ‹finite T›
by (metis T'_def ‹finite T'› finite_image_iff inj_ket inj_on_subset subset_UNIV)
have ψT: ‹ψ ∈ cspan (ket ` T)›
using T'_def ψT' by blast
have Rep_ψ: ‹Rep_ell2 ψ x = 0› if ‹x ∉ T› for x
using _ _ ψT apply (rule complex_vector.linear_eq_0_on_span)
apply auto
by (metis ket.rep_eq that of_bool_def)
have ‹norm (trunc_ell2 S (F ψ)) ≤ sqrt B * norm ψ› if ‹finite S› for S
proof -
have *: ‹cconstruct (range ket) f ψ = (∑x∈T. Rep_ell2 ψ x *⇩C f (ket x))›
proof (rule complex_vector.linear_eq_on[where x=ψ and B=‹ket ` T›])
show ‹clinear (cconstruct (range ket) f)›
using F_def ‹clinear F› by blast
show ‹clinear (λa. ∑x∈T. Rep_ell2 a x *⇩C f (ket x))›
by (auto intro!: clinear_compose[unfolded o_def, OF clinear_Rep_ell2] complex_vector.linear_compose_sum)
show ‹ψ ∈ cspan (ket ` T)›
by (simp add: ψT)
have ‹f b = (∑x∈T. Rep_ell2 b x *⇩C f (ket x))›
if ‹b ∈ ket ` T› for b
proof -
define b' where ‹b' = inv ket b›
have bb': ‹b = ket b'›
using b'_def that by force
show ?thesis
apply (subst sum_single[where i=b'])
using that by (auto simp add: ‹finite T› bb' ket.rep_eq)
qed
then show ‹cconstruct (range ket) f b = (∑x∈T. Rep_ell2 b x *⇩C f (ket x))›
if ‹b ∈ ket ` T› for b
apply (subst complex_vector.construct_basis)
using that by auto
qed
have ‹(norm (trunc_ell2 S (F ψ)))⇧2 = (norm (trunc_ell2 S (∑x∈T. Rep_ell2 ψ x *⇩C f (ket x))))⇧2›
apply (rule arg_cong[where f=‹λx. (norm (trunc_ell2 _ x))⇧2›])
by (simp add: F_def * )
also have ‹… = (norm (trunc_ell2 S (∑x∈T. Rep_ell2 ψ x *⇩C Abs_ell2 (λb. M b x))))⇧2›
by (simp add: f_def)
also have ‹… = (∑i∈S. (cmod (Rep_ell2 (∑x∈T. Rep_ell2 ψ x *⇩C Abs_ell2 (λb. M b x)) i))⇧2)›
by (simp add: that norm_trunc_ell2_finite real_sqrt_pow2 sum_nonneg)
also have ‹… = (∑i∈S. (cmod (∑x∈T. Rep_ell2 ψ x *⇩C Rep_ell2 (Abs_ell2 (λb. M b x)) i))⇧2)›
by (simp add: complex_vector.linear_sum[OF clinear_Rep_ell2]
clinear.scaleC[OF clinear_Rep_ell2])
also have ‹… = (∑i∈S. (cmod (∑x∈T. Rep_ell2 ψ x *⇩C M i x))⇧2)›
using has_norm by (simp add: Abs_ell2_inverse)
also have ‹… ≤ B * (∑x∈T. (cmod (Rep_ell2 ψ x))⇧2)›
using ‹finite S› ‹finite T› Rep_ψ by (rule assms)
also have ‹… = B * ((norm (trunc_ell2 T ψ))⇧2)›
by (simp add: ‹finite T› norm_trunc_ell2_finite sum_nonneg)
also have ‹… ≤ B * (norm ψ)⇧2›
by (simp add: mult_left_mono ‹B ≥ 0› trunc_ell2_reduces_norm)
finally show ?thesis
apply (rule_tac power2_le_imp_le)
by (simp_all add: ‹0 ≤ B› power_mult_distrib)
qed
then show ?thesis
by (rule norm_ell2_bound_trunc)
qed
then have ‹cblinfun_extension_exists (cspan (range ket)) F›
apply (rule cblinfun_extension_exists_hilbert[rotated -1])
by (auto intro: ‹clinear F› complex_vector.linear_add complex_vector.linear_scale)
then have ex: ‹cblinfun_extension_exists (range ket) f›
apply (rule cblinfun_extension_exists_restrict[rotated -1])
by (simp_all add: F_def complex_vector.span_superset complex_vector.construct_basis)
from ex has_norm
show ?thesis
using explicit_cblinfun_exists_def f_def by blast
qed
lemma explicit_cblinfun_exists_finite_dim[simp]: ‹explicit_cblinfun_exists m› for m :: "_::finite ⇒ _::finite ⇒ _"
by (auto simp: explicit_cblinfun_exists_def cblinfun_extension_exists_finite_dim)
lemma explicit_cblinfun_ket: ‹explicit_cblinfun M *⇩V ket a = Abs_ell2 (λb. M b a)› if ‹explicit_cblinfun_exists M›
using that by (auto simp: explicit_cblinfun_exists_def explicit_cblinfun_def cblinfun_extension_apply)
lemma Rep_ell2_explicit_cblinfun_ket[simp]: ‹Rep_ell2 (explicit_cblinfun M *⇩V ket a) b = M b a› if ‹explicit_cblinfun_exists M›
using that apply (simp add: explicit_cblinfun_ket)
by (simp add: Abs_ell2_inverse explicit_cblinfun_exists_def)
lemma bounded_extension_counterexample_1: ‹∃f. ∀x. f (ket x) = ket 0›
by auto
lemma bounded_extension_counterexample_2:
assumes ‹∀x::'a::infinite. f (ket x) = ket 0›
shows ‹¬ cblinfun_extension_exists (range ket) f›
proof (rule ccontr, unfold not_not)
assume ‹cblinfun_extension_exists (range ket) f›
moreover define F where ‹F = cblinfun_extension (range ket) f›
ultimately have F: ‹F (ket x) = ket 0› for x
by (simp add: assms cblinfun_extension_apply)
have F_geq: ‹norm F ≥ sqrt B› for B :: nat
proof -
obtain S :: ‹'a set› where card_S: ‹card S = B› and fin_S: ‹finite S›
using arb_finite_subset[of ‹{}› B]
by (meson finite.emptyI obtain_subset_with_card_n)
define ψ where ‹ψ = (∑i∈S. ket i)›
have ‹(norm ψ)⇧2 = B›
by (simp add: ψ_def pythagorean_theorem_sum card_S fin_S)
then have norm_ψ: ‹norm ψ = sqrt B›
by (smt (verit, best) norm_ge_zero real_sqrt_abs)
have ‹F ψ = B *⇩R ket 0›
by (simp add: ψ_def cblinfun.sum_right real_vector.sum_constant_scale F card_S)
then have ‹norm (F ψ) = B›
by simp
with norm_ψ have ‹norm F ≥ B / sqrt B›
using norm_cblinfun[of F ψ]
by (simp add: divide_le_eq)
then show ?thesis
by (simp add: real_div_sqrt)
qed
then show False
proof -
obtain B :: nat where B: ‹B > (norm F)⇧2›
apply atomize_elim
apply (rule exI[of _ ‹nat (ceiling ((norm F)⇧2 + 1))›])
by linarith
with F_geq show False
by (smt (verit, ccfv_threshold) B sqrt_le_D)
qed
qed
subsection ‹Diagonal operators›
definition diagonal_operator where ‹diagonal_operator f =
(if bdd_above (range (λx. cmod (f x))) then explicit_cblinfun (λx y. of_bool (x=y) * f x) else 0)›
lemma diagonal_operator_exists:
assumes ‹bdd_above (range (λx. cmod (f x)))›
shows ‹explicit_cblinfun_exists (λx y. of_bool (x = y) * f x)›
proof -
from assms obtain B where B: ‹cmod (f x) ≤ B› for x
by (auto simp: bdd_above_def)
show ?thesis
proof (rule explicit_cblinfun_exists_bounded)
fix S T :: ‹'a set› and ψ :: ‹'a ⇒ complex›
assume [simp]: ‹finite S› ‹finite T›
assume ‹ψ a = 0› if ‹a ∉ T› for a
have ‹(∑b∈S. (cmod (∑a∈T. ψ a *⇩C (of_bool (b = a) * f b)))⇧2)
= (∑b∈S. (cmod (of_bool (b ∈ T) * ψ b * f b))⇧2)›
apply (rule sum.cong[OF refl])
subgoal for b
apply (subst sum_single[where i=b])
by auto
by -
also have ‹… = (∑b∈S∩T. (cmod (ψ b * f b))⇧2)›
apply (rule sum.mono_neutral_cong_right)
by auto
also have ‹… ≤ (∑b∈T. (cmod (ψ b * f b))⇧2)›
by (simp add: sum_mono2)
also have ‹… ≤ (∑b∈T. B⇧2 * (cmod (ψ b))⇧2)›
by (rule sum_mono)
(auto intro!: mult_left_mono power_mono B
simp: norm_mult power_mult_distrib mult.commute[of "B ^ 2"])
also have ‹… = B⇧2 * (∑b∈T. (cmod (ψ b))⇧2)›
by (simp add: vector_space_over_itself.scale_sum_right)
finally
show ‹(∑b∈S. (cmod (∑a∈T. ψ a *⇩C (of_bool (b = a) * f b)))⇧2)
≤ B⇧2 * (∑a∈T. (cmod (ψ a))⇧2)› .
qed
qed
lemma diagonal_operator_ket:
assumes ‹bdd_above (range (λx. cmod (f x)))›
shows ‹diagonal_operator f (ket x) = f x *⇩C ket x›
proof -
have [simp]: ‹has_ell2_norm (λb. of_bool (b = x) * f b)›
by (auto intro!: finite_nonzero_values_imp_summable_on simp: has_ell2_norm_def)
have ‹Abs_ell2 (λb. of_bool (b = x) * f b) = f x *⇩C ket x›
by (rule Rep_ell2_inject[THEN iffD1])
(auto simp: Abs_ell2_inverse scaleC_ell2.rep_eq ket.rep_eq)
then show ?thesis
by (auto intro!: simp: diagonal_operator_def assms explicit_cblinfun_ket diagonal_operator_exists)
qed
lemma diagonal_operator_invalid:
assumes ‹¬ bdd_above (range (λx. cmod (f x)))›
shows ‹diagonal_operator f = 0›
by (simp add: assms diagonal_operator_def)
lemma diagonal_operator_adj: ‹diagonal_operator f* = diagonal_operator (λx. cnj (f x))›
by (cases ‹bdd_above (range (λx. cmod (f x)))›)
(auto intro!: equal_ket cinner_ket_eqI
simp: diagonal_operator_ket cinner_adj_right diagonal_operator_invalid)
lemma diagonal_operator_comp:
assumes ‹bdd_above (range (λx. cmod (f x)))›
assumes ‹bdd_above (range (λx. cmod (g x)))›
shows ‹diagonal_operator f o⇩C⇩L diagonal_operator g = diagonal_operator (λx. (f x * g x))›
proof -
have ‹bdd_above (range (λx. cmod (f x * g x)))›
proof -
from assms(1) obtain F where ‹cmod (f x) ≤ F› for x
by (auto simp: bdd_above_def)
moreover from assms(2) obtain G where ‹cmod (g x) ≤ G› for x
by (auto simp: bdd_above_def)
ultimately have ‹cmod (f x * g x) ≤ F * G› for x
by (smt (verit, del_insts) mult_right_mono norm_ge_zero norm_mult ordered_comm_semiring_class.comm_mult_left_mono)
then show ?thesis
by fast
qed
then show ?thesis
by (auto intro!: equal_ket simp: diagonal_operator_ket assms cblinfun.scaleC_right)
qed
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
assumes "inj_map π"
shows classical_operator_exists_inj: "classical_operator_exists π"
and classical_operator_norm_inj: ‹norm (classical_operator π) ≤ 1›
proof -
have ‹is_orthogonal (case π x of None ⇒ 0 | Some x' ⇒ ket x')
(case π y of None ⇒ 0 | Some y' ⇒ ket y')›
if ‹x ≠ y› for x y
apply (cases ‹π x›; cases ‹π y›)
using that assms
by (auto simp add: inj_map_def)
then have 1: ‹is_orthogonal (case π (inv ket x) of None ⇒ 0 | Some x' ⇒ ket x')
(case π (inv ket y) of None ⇒ 0 | Some y' ⇒ ket y')›
if ‹x ∈ range ket› and ‹y ∈ range ket› and ‹x ≠ y› for x y
using that by auto
have ‹norm (case π x of None ⇒ 0 | Some x ⇒ ket x) ≤ 1 * norm (ket x)› for x
apply (cases ‹π x›) by auto
then have 2: ‹norm (case π (inv ket x) of None ⇒ 0 | Some x ⇒ ket x) ≤ 1 * norm x›
if ‹x ∈ range ket› for x
using that by auto
show ‹classical_operator_exists π›
unfolding classical_operator_exists_def
using _ _ 1 2 apply (rule cblinfun_extension_exists_ortho)
by simp_all
show ‹norm (classical_operator π) ≤ 1›
unfolding classical_operator_def Let_def
using _ _ 1 2 apply (rule cblinfun_extension_exists_ortho_norm)
by simp_all
qed
lemma classical_operator_exists_finite[simp]: "classical_operator_exists (π :: _::finite ⇒ _)"
unfolding classical_operator_exists_def
using cindependent_ket cspan_range_ket_finite
by (rule cblinfun_extension_exists_finite_dim)
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) ∙⇩C ket j = ket i ∙⇩C (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) ∙⇩C ket j = (classical_operator (inv_map π) *⇩V ket i) ∙⇩C ket j"
unfolding F_def by blast
also have "… = ((case inv_map π i of Some k ⇒ ket k | None ⇒ 0) ∙⇩C ket j)"
using w1 by simp
also have "… = (ket i ∙⇩C (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) ∙⇩C ket j
= ket i ∙⇩C (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 ∙⇩C ket j) = (ket i ∙⇩C 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) ∙⇩C ket j
= ket i ∙⇩C (case Some c of None ⇒ 0 | Some a ⇒ ket a)"
by simp
thus "(case inv_map π i of None ⇒ 0 | Some a ⇒ ket a) ∙⇩C ket j
= ket i ∙⇩C (case π j of None ⇒ 0 | Some a ⇒ ket a)"
by (simp add: Some.hyps s1)
qed
qed
also have "… = ket i ∙⇩C (classical_operator π *⇩V ket j)"
by (simp add: w2)
also have "… = ket i ∙⇩C (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 ∘ π)"
by (simp add: a1)
have b0': "inj_map (inv_map (Some ∘ π))"
by simp
have b1: "inv_map (Some ∘ π) ∘⇩m (Some ∘ π) = Some"
apply (rule ext) unfolding inv_map_def o_def
using assms unfolding inj_def inv_def by auto
have b3: "classical_operator (inv_map (Some ∘ π)) o⇩C⇩L
classical_operator (Some ∘ π) = classical_operator (inv_map (Some ∘ π) ∘⇩m (Some ∘ π))"
by (metis b0 b0' b1 classical_operator_Some classical_operator_exists_inj
classical_operator_mult)
show ?thesis
unfolding isometry_def
apply (subst classical_operator_adjoint)
using b0 by (auto simp add: b1 b3)
qed
lemma unitary_classical_operator[simp]:
fixes π::"'a ⇒ 'b"
assumes a1: "bij π"
shows "unitary (classical_operator (Some o π))"
proof (unfold unitary_def, rule conjI)
have "inj π"
using a1 bij_betw_imp_inj_on by auto
hence "isometry (classical_operator (Some o π))"
by simp
hence "classical_operator (Some ∘ π)* o⇩C⇩L classical_operator (Some ∘ π) = id_cblinfun"
unfolding isometry_def by simp
thus ‹classical_operator (Some ∘ π)* o⇩C⇩L classical_operator (Some ∘ π) = id_cblinfun›
by simp
next
have "inj π"
by (simp add: assms bij_is_inj)
have comp: "Some ∘ π ∘⇩m inv_map (Some ∘ π) = Some"
apply (rule ext)
unfolding inv_map_def o_def map_comp_def
unfolding inv_def apply auto
apply (metis ‹inj π› inv_def inv_f_f)
using bij_def image_iff range_eqI
by (metis a1)
have "classical_operator (Some ∘ π) o⇩C⇩L classical_operator (Some ∘ π)*
= classical_operator (Some ∘ π) o⇩C⇩L classical_operator (inv_map (Some ∘ π))"
by (simp add: ‹inj π›)
also have "… = classical_operator ((Some ∘ π) ∘⇩m (inv_map (Some ∘ π)))"
by (simp add: ‹inj π› classical_operator_exists_inj)
also have "… = classical_operator (Some::'b⇒_)"
using comp
by simp
also have "… = (id_cblinfun:: 'b ell2 ⇒⇩C⇩L _)"
by simp
finally show "classical_operator (Some ∘ π) o⇩C⇩L classical_operator (Some ∘ π)* = id_cblinfun".
qed
unbundle no lattice_syntax and no cblinfun_syntax
end