Theory Misc_Compressed_Oracle
section ‹‹Misc_Compressed_Oracle› -- Miscellaneous required theorems›
theory Misc_Compressed_Oracle
imports Registers.Quantum_Extra2
begin
declare [[simproc del: Laws_Quantum.compatibility_warn]]
unbundle cblinfun_syntax
unbundle register_syntax
subsection Misc
lemma assoc_ell2'_ket[simp]: ‹assoc_ell2* *⇩V ket (x,y,z) = ket ((x,y),z)›
by (metis assoc_ell2'_tensor tensor_ell2_ket)
lemma assoc_ell2_ket[simp]: ‹assoc_ell2 *⇩V ket ((x,y),z) = ket (x,y,z)›
by (metis assoc_ell2_tensor tensor_ell2_ket)
lemma sandwich_tensor:
fixes a :: ‹'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
assumes ‹unitary a› ‹unitary b›
shows "cblinfun_apply (sandwich (a ⊗⇩o b)) = cblinfun_apply (sandwich a) ⊗⇩r cblinfun_apply (sandwich b)"
apply (rule tensor_extensionality)
by (auto simp: unitary_sandwich_register assms sandwich_apply register_tensor_is_register comp_tensor_op tensor_op_adjoint unitary_tensor_op)
lemma sandwich_grow_left:
fixes a :: ‹'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2›
assumes "unitary a"
shows "sandwich a ⊗⇩r id = sandwich (a ⊗⇩o (id_cblinfun :: (_::finite ell2 ⇒⇩C⇩L _)))"
by (simp add: unitary_sandwich_register assms sandwich_tensor id_def)
lemma Snd_apply_tensor_ell2[simp]: ‹Snd a *⇩V (ψ ⊗⇩s φ) = ψ ⊗⇩s (a *⇩V φ)›
by (simp add: Snd_def tensor_op_ell2)
ML ‹
fun register_n_of_m n m = let
val _ = n > 0 orelse error "register_n_of_m: n<=0"
val _ = m >= n orelse error "register_n_of_m: n>m"
val id_op = Const(\<^const_name>‹id_cblinfun›,dummyT)
val tensor_op = Const(\<^const_name>‹tensor_op›,dummyT)
fun add_ids 0 t = t
| add_ids i t = tensor_op $ id_op $ add_ids (i-1) t
val body = if n=m then add_ids (n-1) (Bound 0)
else add_ids (n-1) (tensor_op $ Bound 0 $ add_ids (m-n-1) id_op)
in
Abs("a", dummyT, body)
end
;;
register_n_of_m 5 5 |> Syntax.string_of_term \<^context> |> writeln
›
ML ‹
fun dest_numeral_syntax (Const(\<^const_syntax>‹Num.num.One›, _)) = 1
| dest_numeral_syntax (Const(\<^const_syntax>‹Num.num.Bit0›, _) $ bs) = 2 * dest_numeral_syntax bs
| dest_numeral_syntax (Const (\<^const_syntax>‹Num.num.Bit1›, _) $ bs) = 2 * dest_numeral_syntax bs + 1
| dest_numeral_syntax (Const ("_constrain", _) $ t $ _) = dest_numeral_syntax t
| dest_numeral_syntax t = raise TERM ("dest_numeral_syntax", [t]);
fun dest_number_syntax (Const (\<^const_syntax>‹Groups.zero_class.zero›, _)) = 0
| dest_number_syntax (Const (\<^const_syntax>‹Groups.one_class.one›, _)) = 1
| dest_number_syntax (Const (\<^const_syntax>‹Num.numeral_class.numeral›, _) $ t) =
dest_numeral_syntax t
| dest_number_syntax (Const (\<^const_syntax>‹Groups.uminus_class.uminus›, _) $ t) =
~ (dest_number_syntax t)
| dest_number_syntax (Const ("_constrain", _) $ t $ _) = dest_number_syntax t
| dest_number_syntax t = raise TERM ("dest_number_syntax", [t])
›
syntax "_register_n_of_m" :: ‹'a ⇒ 'a ⇒ 'b› ("[_⇩_]")
parse_translation ‹[(\<^syntax_const>‹_register_n_of_m›, fn ctxt => fn [nt,mt] => let
val n = dest_number_syntax nt
val m = dest_number_syntax mt
in register_n_of_m n m end
)]›
ML ‹
Syntax.read_term \<^context> "[8⇩9]" |> Thm.cterm_of \<^context>
›
lemma sum_if: ‹(∑x∈X. P (if Q x then a x else b x)) = (∑x∈X. if Q x then P (a x) else P (b x))›
by (smt (verit) Finite_Cartesian_Product.sum_cong_aux)
lemma sum_if': ‹(∑x∈X. P (if Q x then a x else b x) x) = (∑x∈X. if Q x then P (a x) x else P (b x) x)›
by (smt (verit) Finite_Cartesian_Product.sum_cong_aux)
lemma bij_plus: ‹bij ((+) y)› for y :: ‹_::group_add›
by simp
lemma tensor_ell2_diff2: ‹tensor_ell2 a (b - c) = tensor_ell2 a b - tensor_ell2 a c›
by (metis add_diff_cancel_right' diff_add_cancel tensor_ell2_add2)
lemma tensor_ell2_diff1: ‹tensor_ell2 (a - b) c = tensor_ell2 a c - tensor_ell2 b c›
by (metis add_right_cancel diff_add_cancel tensor_ell2_add1)
lemma aminus_bminusc: ‹a - (b - c) = a - b + c› for a b c :: ‹_ :: ab_group_add›
by simp
lemma sum_case':
fixes a :: ‹_ ⇒ _ ⇒ _::ab_group_add›
assumes ‹finite X›
shows ‹(∑x∈X. P (case Q x of Some z ⇒ a z x | None ⇒ b x))
= (∑x∈X ∩ {x. Q x ≠ None}. P (a (the (Q x)) x)) + (∑x∈X ∩ {x. Q x = None}. P (b x))›
(is "?lhs=?rhs")
proof -
have ‹?lhs = (∑x∈X ∩ (Q -` Some ` UNIV). P (case Q x of Some z ⇒ a z x | None ⇒ b x)) + (∑x∈X ∩ (Q -` {None}). P (case Q x of Some z ⇒ a z x | None ⇒ b x))›
apply (subst sum.union_disjoint[symmetric])
using assms apply auto
by (metis Int_UNIV_right Int_Un_distrib UNIV_option_conv insert_union vimage_UNIV vimage_Un)
also have ‹… = ?rhs›
apply (rule arg_cong2[where f=plus])
apply (rule sum.cong)
apply auto[2]
apply (rule sum.cong)
by auto
finally show ?thesis
by -
qed
lemma register_isometry:
assumes "register F"
assumes "isometry a"
shows "isometry (F a)"
using assms by (smt (verit, best) register_def isometry_def)
lemma register_coisometry:
assumes "register F"
assumes "isometry (a*)"
shows "isometry (F a*)"
using assms by (smt (verit, best) register_def isometry_def)
lemma card_complement:
fixes M :: ‹'a::finite set›
shows ‹card (-M) = CARD('a) - card M›
by (simp add: Compl_eq_Diff_UNIV card_Diff_subset)
lemma register_minus: ‹register F ⟹ F (a - b) = F a - F b›
using clinear_register complex_vector.linear_diff by blast
lemma vimage_singleton_inj: ‹inj f ⟹ f -` {f x} = {x}›
using inj_vimage_singleton subset_singletonD by fastforce
lemma has_ell2_norm_0[iff]: ‹has_ell2_norm (λx. 0)›
by (metis eq_onp_same_args zero_ell2.rsp)
lemma ell2_norm_0I[simp]: ‹ell2_norm (λx. 0) = 0›
using ell2_norm_0 by blast
lemma ran_smaller_dom: ‹finite (dom m) ⟹ card (ran m) ≤ card (dom m)›
apply (rule surj_card_le[where f=‹the o m›], simp)
unfolding dom_def ran_def by force
lemma option_sum_split: ‹(∑x∈X. f x) = (∑x∈Some -` X. f (Some x)) + (if None ∈ X then f None else 0)› if ‹finite X› for f X
apply (subst asm_rl[of ‹X = (Some ` Some -` X) ∪ ({None} ∩ X)›])
apply auto[1]
apply (subst sum.union_disjoint)
apply (auto simp: that)[3]
apply (subst sum.reindex)
by auto
lemma sum_sum_if_eq: ‹(∑x∈X. ∑y∈Y x. if x=a then f x y else 0) = (if a∈X then (∑y∈Y a. f a y) else 0)› if ‹finite X› for X Y f
by (subst sum_single[where i=a], auto simp: that)
lemma sum_if_eq_else: ‹(∑x∈X. if x=a then 0 else f x) = (∑x∈X-{a}. f x)› for X f
apply (cases ‹finite X›)
apply (rule sum.mono_neutral_cong_right)
by auto
lemma fun_upd_comp_left:
assumes ‹inj g›
shows ‹(f ∘ g)(x := y) = f(g x := y) o g›
by (auto simp: fun_upd_def assms inj_eq)
definition reg_1_3 :: ‹_ ⇒ ('a::finite × 'b::finite × 'c::finite) ell2 ⇒⇩C⇩L ('a × 'b × 'c) ell2› where ‹reg_1_3 = Fst›
lemma register_1_3[simp]: ‹register reg_1_3›
by (simp add: reg_1_3_def)
lemma comp_reg_1_3[simp]: ‹(F;G) o reg_1_3 = F› if [register]: ‹compatible F G›
by (simp add: reg_1_3_def register_pair_Fst)
definition reg_2_3 :: ‹_ ⇒ ('a::finite × 'b::finite × 'c::finite) ell2 ⇒⇩C⇩L ('a × 'b × 'c) ell2› where ‹reg_2_3 = Snd o Fst›
lemma register_2_3[simp]: ‹register reg_2_3›
by (simp add: reg_2_3_def)
lemma comp_reg_2_3[simp]: ‹(F;(G;H)) o reg_2_3 = G› if [register]: ‹compatible F G› ‹compatible F H› ‹compatible G H›
by (simp add: reg_2_3_def register_pair_Fst register_pair_Snd flip: comp_assoc)
definition reg_3_3 :: ‹_ ⇒ ('a::finite × 'b::finite × 'c::finite) ell2 ⇒⇩C⇩L ('a × 'b × 'c) ell2› where ‹reg_3_3 = Snd o Snd›
lemma register_3_3[simp]: ‹register reg_3_3›
by (simp add: reg_3_3_def)
lemma comp_reg_3_3[simp]: ‹(F;(G;H)) o reg_3_3 = H› if [register]: ‹compatible F G› ‹compatible F H› ‹compatible G H›
by (simp add: reg_3_3_def register_pair_Snd flip: comp_assoc)
lemma [simp]: ‹mutually compatible (reg_1_3, reg_2_3, reg_3_3)›
by (auto simp add: reg_1_3_def reg_2_3_def reg_3_3_def)
lemma pair_o_tensor_right:
assumes [simp]: ‹compatible F G› ‹register H›
shows ‹(F; G o H) = (F; G) o (id ⊗⇩r H)›
by (auto simp: pair_o_tensor)
lemma register_tensor_distrib_right:
assumes [simp]: ‹register F› ‹register H› ‹register L›
shows ‹F ⊗⇩r (H o L) = (F ⊗⇩r H) o (id ⊗⇩r L)›
apply (subst register_tensor_distrib)
by auto
lemma sandwich_apply':
‹sandwich U A *⇩V ψ = U *⇩V A *⇩V U* *⇩V ψ›
unfolding sandwich_apply by simp
lemma csubspace_set_sum:
assumes ‹⋀x. x ∈ X ⟹ csubspace (A x)›
shows ‹csubspace (∑x∈X. A x)›
using assms
apply (induction X rule:infinite_finite_induct)
by (auto simp: csubspace_set_plus)
lemma Rep_ell2_vector_to_cblinfun_ket: ‹Rep_ell2 ψ x = bra x *⇩V ψ›
by (simp add: cinner_ket_left)
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 and ψ=ψ] that
by (auto simp: trunc_ell2_singleton)
lemma trunc_ell2_in_cspan:
assumes ‹finite S›
shows ‹trunc_ell2 S ψ ∈ cspan (ket ` S)›
using assms
proof induction
case empty
show ?case
by simp
next
case (insert x F)
then have ‹Rep_ell2 ψ x *⇩C ket x + trunc_ell2 F ψ ∈ cspan (insert (ket x) (ket ` F))›
by (metis add_diff_cancel_left' complex_vector.span_breakdown_eq)
with insert show ?case
by (auto simp: trunc_ell2_insert)
qed
lemma space_ccspan_ket: ‹space_as_set (ccspan (ket ` M)) = {ψ. ∀x ∈ -M. Rep_ell2 ψ x = 0}›
proof (intro Set.set_eqI iffI; rename_tac ψ)
fix ψ
assume ψ_in_ccspan: ‹ψ ∈ space_as_set (ccspan (ket ` M))›
have ‹Rep_ell2 ψ x = 0› if ‹x ∈ -M› for x
proof -
have ‹Rep_ell2 ψ x = vector_to_cblinfun (ket x)* *⇩V ψ›
by (simp add: Rep_ell2_vector_to_cblinfun_ket)
also have ‹… ∈ vector_to_cblinfun (ket x)* ` space_as_set (ccspan (ket ` M))›
using ψ_in_ccspan by blast
also have ‹… ⊆ space_as_set (vector_to_cblinfun (ket x)* *⇩S ccspan (ket ` M))›
by (simp add: cblinfun_image.rep_eq closure_subset)
also have ‹… = space_as_set (ccspan (vector_to_cblinfun (ket x)* ` ket ` M))›
by (simp add: cblinfun_image_ccspan)
also have ‹… = space_as_set (ccspan (if M={} then {} else {0}))›
apply (rule arg_cong[where f=‹λx. space_as_set (ccspan x)›])
using ‹x ∈ -M› apply auto
by (metis imageI orthogonal_ket)
also have ‹… = 0›
by simp
finally show ‹Rep_ell2 ψ x = 0›
by auto
qed
then show ‹ψ ∈ {ψ. ∀x∈- M. Rep_ell2 ψ x = 0}›
by simp
next
fix ψ
assume ‹ψ ∈ {ψ. ∀x∈- M. Rep_ell2 ψ x = 0}›
then have ‹ψ = trunc_ell2 M ψ›
by (auto intro!: Rep_ell2_inject[THEN iffD1] ext simp: trunc_ell2.rep_eq)
then have lim: ‹((λS. trunc_ell2 S ψ) ⤏ ψ) (finite_subsets_at_top M)›
using trunc_ell2_lim[of ψ M]
by auto
have ‹trunc_ell2 S ψ ∈ cspan (ket ` S)› if ‹finite S› for S
by (simp add: that trunc_ell2_in_cspan)
also have ‹…S ⊆ space_as_set (ccspan (ket ` M))› if ‹finite S› and ‹S ⊆ M› for S
by (metis ccspan.rep_eq closure_subset complex_vector.span_mono dual_order.trans image_mono that(2))
finally show ‹ψ ∈ space_as_set (ccspan (ket ` M))›
apply (rule_tac Lim_in_closed_set[OF _ _ _ lim])
by (auto intro!: eventually_finite_subsets_at_top_weakI)
qed
lemma space_as_set_ccspan_memberI: ‹ψ ∈ space_as_set (ccspan X)› if ‹ψ ∈ X›
using that apply transfer
by (meson closure_subset complex_vector.span_superset subset_iff)
lemma closure_subset_remove_closure: ‹X ⊆ closure Y ⟹ closure X ⊆ closure Y›
using closure_minimal by blast
lemma closure_cspan_closure: ‹closure (cspan (closure X)) = closure (cspan X)›
for X :: ‹'a::complex_normed_vector set›
apply (rule antisym)
apply (meson closure_subset_remove_closure closure_is_csubspace closure_mono complex_vector.span_minimal
complex_vector.span_superset complex_vector.subspace_span)
by (simp add: closure_mono closure_subset complex_vector.span_mono)
lemma closure_Sup_closure: ‹closure (Sup (closure ` X)) = closure (Sup X)›
by (auto simp: hull_def closure_hull)
lemma cspan_closure_cspan: ‹cspan (closure (cspan X)) = closure (cspan X)›
for X :: ‹'a::complex_normed_vector set›
by (metis (full_types) closure_cspan_closure closure_subset complex_vector.span_span complex_vector.span_superset subset_antisym)
lemma cblinfun_image_SUP: ‹A *⇩S (SUP x∈X. I x) = (SUP x∈X. A *⇩S I x)›
proof (rule antisym)
show ‹A *⇩S (SUP x∈X. I x) ≤ (SUP x∈X. A *⇩S I x)›
proof (transfer, rule closure_subset_remove_closure)
fix A :: ‹'b ⇒ 'a› and I :: ‹'c ⇒ 'b set› and X
assume [simp]: ‹bounded_clinear A›
assume ‹pred_fun top closed_csubspace I›
then have [simp]: ‹closed_csubspace (I x)› for x
by simp
have ‹A ` closure (cspan (⋃x∈X. I x)) ⊆ closure (A ` cspan (⋃x∈X. I x))›
apply (rule closure_bounded_linear_image_subset)
by (simp add: bounded_clinear.bounded_linear)
also have ‹… = closure (cspan (A ` (⋃x∈X. I x)))›
by (simp add: bounded_clinear.clinear complex_vector.linear_span_image)
also have ‹… = closure (cspan (⋃x∈X. A ` I x))›
by (metis image_UN)
also have ‹… = closure (cspan (closure (⋃x∈X. A ` I x)))›
using closure_cspan_closure by blast
also have ‹… = closure (cspan (closure (⋃x∈X. closure (A ` I x))))›
apply (subst closure_Sup_closure[symmetric])
by (simp add: image_image)
also have ‹… = closure (cspan (⋃x∈X. closure (A ` I x)))›
using closure_cspan_closure by blast
finally show ‹A ` closure (cspan (⋃ (I ` X))) ⊆ closure (cspan (⋃x∈X. closure (A ` I x)))›
by -
qed
show ‹(SUP x∈X. A *⇩S I x) ≤ A *⇩S (SUP x∈X. I x)›
by (simp add: SUP_least SUP_upper cblinfun_image_mono)
qed
lemma cspan_Sup_cspan: ‹cspan (Sup (cspan ` X)) = cspan (Sup X)›
by (auto simp: hull_def complex_vector.span_def)
lemma ccspan_Sup: ‹ccspan (⋃X) = Sup (ccspan ` X)›
proof (transfer fixing: X)
have ‹closure (cspan (⋃X)) = closure (cspan (⋃ (cspan ` X)))›
by (simp add: cspan_Sup_cspan)
also have ‹… = closure (cspan (closure (⋃ (cspan ` X))))›
using closure_cspan_closure by blast
also have ‹… = closure (cspan (closure (⋃ (closure ` cspan ` X))))›
by (metis closure_Sup_closure)
also have ‹… = closure (cspan (⋃ (closure ` cspan ` X)))›
by (meson closure_cspan_closure)
also have ‹… = closure (cspan (⋃G∈X. closure (cspan G)))›
by (metis image_image)
finally show ‹closure (cspan (⋃ X)) = closure (cspan (⋃G∈X. closure (cspan G)))›
by -
qed
lemma ccspan_space_as_set[simp]: ‹ccspan (space_as_set S) = S›
apply transfer
by (metis closed_csubspace_def closure_closed complex_vector.span_eq_iff)
lemma cblinfun_image_Sup: ‹A *⇩S Sup II = (SUP I∈II. A *⇩S I)›
using cblinfun_image_SUP[where X=II and I=id and A=A]
by simp
lemma space_as_set_mono: ‹I ≤ J ⟹ space_as_set I ≤ space_as_set J›
by (simp add: less_eq_ccsubspace.rep_eq)
lemma square_into_sum:
fixes X Y and f :: ‹_ ⇒ real›
assumes ‹⋀x. f x ≥ 0›
shows ‹(∑x∈X. f x)⇧2 ≤ card X * (∑x∈X. (f x)⇧2)›
proof -
have ‹(∑x∈X. f x)⇧2 = (∑x∈X. f x * 1)⇧2›
by simp
also have ‹… ≤ (∑x∈X. (f x)⇧2) * (∑x∈X. 1⇧2)›
by (rule Cauchy_Schwarz_ineq_sum)
also have ‹… = (∑x∈X. (f x)⇧2) * (card X)›
by simp
also have ‹… = card X * (∑x∈X. (f x)⇧2)›
by auto
finally show ?thesis
by -
qed
lemma bound_coeff_sum2:
fixes X Y and f :: ‹'a ⇒ complex›
assumes [simp]: ‹finite Y›
assumes XY: ‹X ⊆ Y›
assumes sum1: ‹(∑x∈Y. (cmod (f x))⇧2) ≤ 1›
assumes k: ‹⋀x. x ∈ X ⟹ card {y. g x = g y ∧ y ∈ X} ≤ k›
shows ‹norm (∑x∈X. f x *⇩C ket (g x)) ≤ sqrt k›
proof -
define eq where ‹eq = {(x,y). g x = g y ∧ x ∈ X ∧ y ∈ X}›
have [simp]: ‹equiv X eq›
by (auto simp: eq_def equiv_def refl_on_def sym_def trans_def)
have [simp]: ‹finite X›
using ‹finite Y› XY infinite_super by blast
then have [simp]: ‹finite (X // eq)›
by (simp add: equiv_type finite_quotient)
have [simp]: ‹x ∈ X // eq ⟹ finite x› for x
by (meson ‹equiv X eq› ‹finite X› equiv_def finite_equiv_class refl_on_def)
have card_c: ‹c ∈ X//eq ⟹ card c ≤ k› for c
using k
by (auto simp: Image_def quotient_def eq_def)
define g' where ‹g' c = g (SOME x. x∈c)› for c :: ‹'a set›
have g_g': ‹c ∈ X//eq ⟹ x ∈ c ⟹ g x = g' c› for x c
apply (simp add: g'_def quotient_def eq_def)
by (metis (mono_tags, lifting) mem_Collect_eq alethe_sko_ex)
have g'_inj: ‹c ∈ X//eq ⟹ d ∈ X//eq ⟹ g' c = g' d ⟹ c = d› (is ‹PROP ?goal›) for c d
proof -
have aux1: ‹⋀x xa xb.
g (SOME x. g xb = g x ∧ x ∈ X) = g (SOME x. g xa = g x ∧ x ∈ X) ⟹
xa ∈ X ⟹ xb ∈ X ⟹ g xa = g xb›
by (metis (mono_tags, lifting) alethe_sko_ex)
have aux2: ‹⋀x xa xb.
g (SOME xa. g x = g xa ∧ xa ∈ X) = g (SOME x. g xb = g x ∧ x ∈ X) ⟹
x ∈ X ⟹ xb ∈ X ⟹ g x = g xb›
by (metis (mono_tags, lifting) someI2)
show ‹PROP ?goal›
by (auto intro: aux1 aux2 simp add: g'_def quotient_def eq_def image_iff)
qed
have SIGMA: ‹(SIGMA x:X // eq. x) = (λx. (eq``{x},x)) ` X›
by (auto simp: quotient_def eq_def)
have ‹(norm (∑x∈X. f x *⇩C ket (g x)))⇧2 = (norm (∑c∈X//eq. ∑x∈c. f x *⇩C ket (g x)))⇧2›
apply (subst sum.Sigma)
apply auto[2]
apply (subst SIGMA)
apply (subst sum.reindex)
using inj_on_def by auto
also have ‹… = (norm (∑c∈X//eq. ∑x∈c. f x *⇩C ket (g' c)))⇧2›
by (simp add: g_g')
also have ‹… = (norm (∑c∈X//eq. (∑x∈c. f x) *⇩C ket (g' c)))⇧2›
by (simp add: scaleC_sum_left)
also have ‹… = (∑c∈X//eq. (norm ((∑x∈c. f x) *⇩C ket (g' c)))⇧2)›
apply (rule pythagorean_theorem_sum)
by (auto dest: g'_inj)
also have ‹… = (∑c∈X//eq. (cmod (∑x∈c. f x))⇧2)›
by force
also have ‹… ≤ (∑c∈X//eq. (∑x∈c. cmod (f x))⇧2)›
by (simp add: power_mono sum_mono sum_norm_le)
also have ‹… ≤ (∑c∈X//eq. card c * (∑x∈c. (cmod (f x))⇧2))›
apply (rule sum_mono)
apply (rule square_into_sum)
by simp
also have ‹… ≤ (∑c∈X//eq. k * (∑x∈c. (cmod (f x))⇧2))›
apply (rule sum_mono)
apply (rule mult_right_mono)
by (simp_all add: card_c sum_nonneg)
also have ‹… = k * (∑c∈X//eq. (∑x∈c. (cmod (f x))⇧2))›
by (rule sum_distrib_left[symmetric])
also have ‹… ≤ k * (∑x∈X. (cmod (f x))⇧2)›
apply (subst sum.Sigma)
apply auto[2]
apply (subst SIGMA)
apply (subst sum.reindex)
using inj_on_def by auto
also have ‹… ≤ k * (∑x∈Y. (cmod (f x))⇧2)›
apply (rule mult_left_mono)
apply (rule sum_mono2)
using XY by auto
also have ‹… ≤ k›
using sum1
by (metis mult.right_neutral mult_left_mono of_nat_0_le_iff)
finally show ?thesis
using real_le_rsqrt by blast
qed
lemma norm_ortho_sum_bound:
fixes X
assumes bound: ‹⋀x. x∈X ⟹ norm (ψ x) ≤ b'›
assumes b'geq0: ‹b' ≥ 0›
assumes ortho: ‹⋀x y. x∈X ⟹ y∈X ⟹ x≠y ⟹ is_orthogonal (ψ x) (ψ y)›
assumes b'b: ‹sqrt (card X) * b' ≤ b›
shows ‹norm (∑x∈X. ψ x) ≤ b›
proof (cases ‹finite X›)
case True
have ‹b ≥ 0›
by (metis b'b b'geq0 mult_nonneg_nonneg of_nat_0_le_iff order_trans real_sqrt_ge_0_iff)
have ‹(norm (∑x∈X. ψ x))⇧2 = (∑a∈X. (norm (ψ a))⇧2)›
apply (subst pythagorean_theorem_sum)
using assms True by auto
also have ‹… ≤ (∑a∈X. b'⇧2)›
by (meson bound norm_ge_zero power_mono sum_mono)
also have ‹… ≤ (sqrt (card X) * b')⇧2›
by (simp add: power_mult_distrib)
also have ‹… ≤ b⇧2›
by (meson b'b b'geq0 mult_nonneg_nonneg of_nat_0_le_iff power_mono real_sqrt_ge_0_iff)
finally show ?thesis
apply (rule_tac power2_le_imp_le)
apply force
using ‹0 ≤ b› by force
next
case False
then show ?thesis
using assms by auto
qed
lemma compatible_project1: ‹compatible F G›
if ‹compatible F (G;H)› and [register]: ‹compatible G H› for F G H
proof (rule compatibleI)
show ‹register F›
using compatible_register1 that(1) by blast
show ‹register G›
using compatible_register1 that(2) by blast
fix a b
from ‹compatible F (G;H)›
have ‹F a o⇩C⇩L (G;H) (b ⊗⇩o id_cblinfun) = (G;H) (b ⊗⇩o id_cblinfun) o⇩C⇩L F a›
using swap_registers by blast
then show ‹F a o⇩C⇩L G b = G b o⇩C⇩L F a›
by (simp add: register_pair_apply)
qed
lemma compatible_project2: ‹compatible F H›
if ‹compatible F (G;H)› and [register]: ‹compatible G H› for F G H
proof (rule compatibleI)
show ‹register F›
using compatible_register1 that(1) by blast
show ‹register H›
using compatible_register2 that(2) by blast
fix a b
from ‹compatible F (G;H)›
have ‹F a o⇩C⇩L (G;H) (id_cblinfun ⊗⇩o b) = (G;H) (id_cblinfun ⊗⇩o b) o⇩C⇩L F a›
using swap_registers by blast
then show ‹F a o⇩C⇩L H b = H b o⇩C⇩L F a›
by (simp add: register_pair_apply)
qed
lemma proj_ket_x_y: ‹proj (ket x) *⇩V (ket y) = 0› if ‹x ≠ y›
by (metis kernel_Proj kernel_memberD mem_ortho_ccspanI orthogonal_ket singletonD that)
lemma proj_ket_x_y_ofbool: ‹proj (ket x) *⇩V (ket y) = of_bool (x=y) *⇩C ket y›
by (simp add: Proj_fixes_image ccspan_superset' proj_ket_x_y)
lemma proj_x_x[simp]: ‹proj x *⇩V x = x›
by (meson Proj_fixes_image ccspan_superset insert_subset)
lemma in_ortho_ccspan: ‹y ∈ space_as_set (- ccspan X)› if ‹∀x∈X. is_orthogonal y x›
using that apply transfer
by (metis orthogonal_complementI orthogonal_complement_of_closure orthogonal_complement_of_cspan)
lemma swap_sandwich_swap_ell2: "swap = sandwich swap_ell2"
apply (rule tensor_extensionality)
apply (auto simp: sandwich_apply unitary_sandwich_register)[2]
apply (rule tensor_ell2_extensionality)
by simp
lemma is_Proj_sandwich: ‹is_Proj (sandwich U P)› if ‹isometry U› and ‹is_Proj P›
for P :: ‹'a::chilbert_space ⇒⇩C⇩L 'a› and U :: ‹'a ⇒⇩C⇩L 'b::chilbert_space›
using that
by (simp add: is_Proj_algebraic sandwich_apply
lift_cblinfun_comp[OF isometryD] lift_cblinfun_comp[OF is_Proj_idempotent]
flip: cblinfun_compose_assoc)
lemma is_Proj_swap[simp]: ‹is_Proj (swap P)› if ‹is_Proj P›
using that
by (simp add: swap_sandwich_swap_ell2 is_Proj_sandwich)
lemma iso_register_complement_pair: ‹iso_register (complement X; X)› if ‹register X›
using complement_is_complement complements_def complements_sym that by blast
lemma swap_Snd: ‹swap (Snd x) = Fst x›
by (simp add: Fst_def Snd_def)
lemma sandwich_butterfly: ‹sandwich a (butterfly g h) = butterfly (a g) (a h)›
by (simp add: butterfly_comp_cblinfun cblinfun_comp_butterfly sandwich_apply)
lemma register0:
assumes ‹register Q›
shows ‹Q a = 0 ⟷ a = 0›
by (metis assms norm_eq_zero register_norm)
lemma le_back_subst:
assumes ‹a ≤ c›
assumes ‹a = b›
shows ‹b ≤ c›
using assms by simp
lemma le_back_subst_le:
fixes a b c :: ‹_ :: order›
assumes ‹a ≤ c›
assumes ‹b ≤ a›
shows ‹b ≤ c›
using assms by order
lemma arg_cong4: ‹f a b c d = f a' b' c' d'› if ‹a = a'› and ‹b = b'› and ‹c = c'› and ‹d = d'›
using that by simp
subsection ‹Controlled operations›
definition controlled_op :: ‹('a ⇒ ('b ell2 ⇒⇩C⇩L 'c ell2)) ⇒ (('a×'b) ell2 ⇒⇩C⇩L ('a×'c) ell2)› where
‹controlled_op A = infsum_in cstrong_operator_topology (λx. selfbutter (ket x) ⊗⇩o A x) UNIV›
lemma trunc_ell2_prod_tensor: ‹trunc_ell2 (A×B) (g ⊗⇩s h) = trunc_ell2 A g ⊗⇩s trunc_ell2 B h›
apply transfer'
by auto
lemma trunc_ell2_ket: ‹trunc_ell2 S (ket x) = of_bool (x∈S) *⇩C ket x›
apply transfer'
by auto
lemma summable_on_in_0[iff]: ‹summable_on_in T (λx. 0) A› if ‹0 ∈ topspace T›
using has_sum_in_0[of T A ‹λ_. 0›] summable_on_in_def that by blast
lemma sum_of_bool_scaleC: ‹(∑x∈S. of_bool (x=a) *⇩C f x) = (if a∈S ∧ finite S then f a else 0)›
for f :: ‹_ ⇒ _::complex_vector›
apply (cases ‹finite S›)
apply (subst sum_single[where i=a])
by auto
lemma
fixes A :: ‹'x ⇒ ('a ell2 ⇒⇩C⇩L 'b ell2)›
assumes ‹⋀x. norm (A x) ≤ B›
shows controlled_op_has_sum_aux: ‹has_sum_in cstrong_operator_topology (λx. selfbutter (ket x) ⊗⇩o A x) UNIV (controlled_op A)›
and controlled_op_norm_leq: ‹norm (controlled_op A) ≤ B›
proof -
have [iff]: ‹B ≥ 0›
using assms[of undefined] norm_ge_zero[of ‹A undefined›]
by argo
define A' where ‹A' x = selfbutter (ket x) ⊗⇩o A x› for x
have A'summ: ‹(λx. A' x *⇩V h) summable_on UNIV› for h
proof -
wlog [iff]: ‹B ≠ 0›
using negation assms by (simp add: A'_def)
have ‹∃P. eventually P (finite_subsets_at_top UNIV) ∧ (∀F G. P F ∧ P G ⟶ dist (∑x∈F. A' x *⇩V h) (∑x∈G. A' x *⇩V h) < e)› if ‹e > 0› for e
proof -
have ‹((λS. trunc_ell2 S h) ⤏ h) (finite_subsets_at_top UNIV)›
by (rule trunc_ell2_lim_at_UNIV)
from tendsto_iff[THEN iffD1, OF this, rule_format, of ‹e/B›]
have ‹∀⇩F S in finite_subsets_at_top UNIV. dist (trunc_ell2 S h) h < e/B›
using ‹B ≠ 0› ‹B ≥ 0› that by force
then obtain S where [iff]: ‹finite S› and S_prop: ‹norm (trunc_ell2 S h - h) < e/B› for G
apply atomize_elim
by (force simp add: eventually_finite_subsets_at_top dist_norm)
define P :: ‹'x set ⇒ bool› where ‹P F ⟷ finite F ∧ F ⊇ fst ` S› for F
have evP: ‹eventually P (finite_subsets_at_top UNIV)›
by (auto intro!: exI[of _ ‹fst`S›] ‹finite S› simp add: eventually_finite_subsets_at_top P_def[abs_def])
have ‹dist (∑x∈F. A' x *⇩V h) (∑x∈G. A' x *⇩V h) < e› if ‹P F› and ‹P G› for F G
proof -
have [iff]: ‹finite F› ‹finite G›
using that by (simp_all add: P_def)
define FG where ‹FG = sym_diff F G›
then have [iff]: ‹finite FG›
by simp
define h' where ‹h' x = (tensor_ell2_left (ket x)*) h› for x
have A'h: ‹A' x *⇩V h = ket x ⊗⇩s (A x *⇩V h' x)› for x
unfolding h'_def
apply (rule fun_cong[of _ _ h])
apply (rule bounded_clinear_equal_ket)
apply (auto intro!: bounded_linear_intros)[2]
by (auto simp add: A'_def tensor_op_ket tensor_op_ell2 cinner_ket simp flip: tensor_ell2_ket)
have ‹(dist (∑x∈F. A' x *⇩V h) (∑x∈G. A' x *⇩V h))⇧2 = (norm ((∑x∈F. A' x *⇩V h) - (∑x∈G. A' x *⇩V h)))⇧2›
by (simp add: dist_norm)
also have ‹… = (norm ((∑x∈FG. (if x∈F then 1 else -1) *⇩C (A' x *⇩V h))))⇧2›
apply (rule arg_cong[where f=‹λx. (norm x)⇧2›])
apply (rewrite at F at ‹∑x∈⌑. _› to ‹(F-G)∪(F∩G)› DEADID.rel_mono_strong, blast)
apply (rewrite at G at ‹∑x∈⌑. _› to ‹(G-F)∪(F∩G)› DEADID.rel_mono_strong, blast)
apply (rewrite at FG at ‹∑x∈⌑. _› FG_def)
apply (subst sum_Un, simp, simp)
apply (subst sum_Un, simp, simp)
apply (subst sum_Un, simp, simp)
apply (rewrite at ‹(∑x∈F - G. (if x ∈ F then 1 else - 1) *⇩C (A' x *⇩V h))› to ‹(∑x∈F-G. A' x *⇩V h)› sum.cong, simp, simp)
apply (rewrite at ‹(∑x∈G - F. (if x ∈ F then 1 else - 1) *⇩C (A' x *⇩V h))› to ‹(∑x∈G-F. - (A' x *⇩V h))› sum.cong, simp, simp)
apply (rewrite at ‹(F - G) ∩ (G - F)› to ‹{}› DEADID.rel_mono_strong, blast)
apply (rewrite at ‹(F - G) ∩ (F ∩ G)› to ‹{}› DEADID.rel_mono_strong, blast)
apply (rewrite at ‹(G - F) ∩ (F ∩ G)› to ‹{}› DEADID.rel_mono_strong, blast)
by (simp add: sum_negf)
also have ‹… = (∑x∈FG. (norm ((if x ∈ F then 1 else - 1) *⇩C (A' x *⇩V h)))⇧2)›
apply (rule pythagorean_theorem_sum)
apply (simp add: A'_def butterfly_adjoint tensor_op_adjoint comp_tensor_op cinner_ket
flip: cinner_adj_right cblinfun_apply_cblinfun_compose)
by (simp add: FG_def)
also have ‹… = (∑x∈FG. (norm (A' x *⇩V h))⇧2)›
apply (rule sum.cong, simp)
by (simp add: norm_scaleC)
also have ‹… = (∑x∈FG. (norm (A x *⇩V h' x))⇧2)›
by (simp add: A'h norm_tensor_ell2)
also have ‹… ≤ (∑x∈FG. (B * norm (h' x))⇧2)›
using assms
by (auto intro!: sum_mono power_mono norm_cblinfun[THEN order_trans] mult_right_mono)
also have ‹… = B⇧2 * (∑x∈FG. (norm (h' x))⇧2)›
by (simp add: sum_distrib_left power_mult_distrib)
also have ‹… = B⇧2 * (∑x∈FG. (norm (ket x ⊗⇩s h' x))⇧2)›
by (simp add: norm_tensor_ell2 norm_ket)
also have ‹… = B⇧2 * (norm (∑x∈FG. ket x ⊗⇩s h' x))⇧2›
apply (subst pythagorean_theorem_sum)
by (simp_all add: FG_def)
also have ‹… = B⇧2 * (norm (trunc_ell2 (FG×UNIV) h))⇧2›
apply (rule arg_cong[where f=‹λx. _ * (norm x)⇧2›])
apply (rule cinner_ket_eqI)
apply (rename_tac ab)
proof -
fix ab :: ‹'x × 'a›
obtain a b where ab: ‹ab = (a,b)›
by (auto simp: prod_eq_iff)
have ‹ket ab ∙⇩C (∑x∈FG. ket x ⊗⇩s h' x) = (∑x∈FG. ket ab ∙⇩C (ket x ⊗⇩s h' x))›
using cinner_sum_right by blast
also have ‹… = of_bool (a∈FG) * (ket b ∙⇩C h' a)›
apply (subst sum_single[where i=a])
by (auto simp add: ab simp flip: tensor_ell2_ket)
also have ‹… = of_bool (a∈FG) * Rep_ell2 h (a, b)›
by (simp add: h'_def cinner_adj_right tensor_ell2_ket cinner_ket_left)
also have ‹… = ket ab ∙⇩C trunc_ell2 (FG × UNIV) h›
by (simp add: ab cinner_ket_left trunc_ell2.rep_eq)
finally show ‹ket ab ∙⇩C (∑x∈FG. ket x ⊗⇩s h' x) = ket ab ∙⇩C trunc_ell2 (FG × UNIV) h›
by -
qed
also have ‹… ≤ B⇧2 * (norm (trunc_ell2 (-S) h))⇧2›
apply (rule mult_left_mono[rotated], simp)
apply (rule power_mono[rotated], simp)
apply (rule trunc_ell2_norm_mono)
using ‹P F› ‹P G› by (force simp: P_def FG_def)
also have ‹… = B⇧2 * (norm (trunc_ell2 S h - h))⇧2›
by (smt (verit, best) norm_id_minus_trunc_ell2 norm_minus_commute trunc_ell2_uminus)
also have ‹… < B⇧2 * (e/B)⇧2›
apply (rule mult_strict_left_mono[rotated], simp)
apply (rule power_strict_mono[rotated], simp, simp)
by (rule S_prop)
also have ‹… = e⇧2›
by (simp add: power_divide)
finally show ?thesis
by (smt (verit, del_insts) ‹0 < e› power_mono)
qed
with evP show ?thesis
by blast
qed
then show ?thesis
unfolding summable_on_def has_sum_def filterlim_def
apply (rule_tac convergent_filter_iff[THEN iffD1])
apply (subst convergent_filter_iff_cauchy)
by (rule cauchy_filter_metric_filtermapI)
qed
define C where ‹C h = (∑⇩∞x. A' x *⇩V h)› for h
then have C_hassum: ‹((λx. A' x *⇩V h) has_sum (C h)) UNIV› for h
using A'summ by auto
have norm_C: ‹norm (C g) ≤ B * norm g› for g
proof -
define g' where ‹g' x = (tensor_ell2_left (ket x)*) g› for x
have A'g: ‹A' x *⇩V g = ket x ⊗⇩s (A x *⇩V g' x)› for x
unfolding g'_def
apply (rule fun_cong[of _ _ g])
apply (rule bounded_clinear_equal_ket)
apply (simp add: cblinfun.bounded_clinear_right)
apply (metis bounded_clinear_compose bounded_clinear_tensor_ell21 cblinfun.bounded_clinear_right)
by (auto simp add: A'_def tensor_op_ket tensor_op_ell2 cinner_ket simp flip: tensor_ell2_ket)
have norm_trunc: ‹norm (trunc_ell2 F (C g)) ≤ B * norm g› if ‹finite F› for F
proof -
define S where ‹S = fst ` F›
then have [iff]: ‹finite S›
using that by blast
have ‹(norm (trunc_ell2 F (C g)))⇧2 ≤ (norm (trunc_ell2 (S × UNIV) (C g)))⇧2›
apply (rule power_mono[rotated], simp)
apply (rule trunc_ell2_norm_mono)
by (force simp: S_def)
also have ‹… = (norm (∑x∈S. ket x ⊗⇩s (A x *⇩V g' x)))⇧2›
proof (rule arg_cong[where f=‹λx. (norm x)⇧2›])
have ‹trunc_ell2 (S×UNIV) (C g) = (∑⇩∞x. trunc_ell2 (S×UNIV) (A' x *⇩V g))›
apply (simp add: C_def)
apply (rule infsum_bounded_linear[symmetric])
apply (intro bounded_clinear.bounded_linear bounded_clinear_trunc_ell2)
using A'summ by -
also have ‹… = (∑⇩∞x∈S. ket x ⊗⇩s (A x *⇩V g' x))›
apply (rule infsum_cong_neutral)
by (auto simp add: A'g trunc_ell2_prod_tensor trunc_ell2_ket)
also have ‹… = (∑x∈S. ket x ⊗⇩s (A x *⇩V g' x))›
by (auto intro!: infsum_finite simp: that)
finally show ‹trunc_ell2 (S × UNIV) (C g) = (∑x∈S. ket x ⊗⇩s A x *⇩V g' x)›
by -
qed
also have ‹… = (∑x∈S. (norm (ket x ⊗⇩s A x *⇩V g' x))⇧2)›
apply (subst pythagorean_theorem_sum)
by auto
also have ‹… = (∑x∈S. (norm (A x *⇩V g' x))⇧2)›
by (simp add: norm_tensor_ell2)
also have ‹… ≤ (∑x∈S. (B * norm (g' x))⇧2)›
using assms
by (auto intro!: sum_mono power_mono norm_cblinfun[THEN order_trans] mult_right_mono)
also have ‹… = (∑x∈S. (norm (g' x))⇧2) * B⇧2›
by (simp add: power_mult_distrib mult.commute sum_distrib_left)
also have ‹… = (∑x∈S. (norm (ket x ⊗⇩s g' x))⇧2) * B⇧2›
by (simp add: norm_tensor_ell2)
also have ‹… = (norm (∑x∈S. ket x ⊗⇩s g' x))⇧2 * B⇧2›
apply (subst pythagorean_theorem_sum[symmetric])
by (auto simp add: g'_def)
also have ‹… ≤ (norm g)⇧2 * B⇧2›
proof -
have ‹(∑x∈S. ket x ⊗⇩s g' x) = trunc_ell2 (S×UNIV) g›
unfolding g'_def
apply (rule fun_cong[where x=g])
apply (rule bounded_clinear_equal_ket)
apply (auto intro!: bounded_linear_intros)[2]
by (auto intro!: simp: cinner_ket trunc_ell2_prod_tensor trunc_ell2_ket
tensor_ell2_scaleC2 sum_of_bool_scaleC
simp flip: tensor_ell2_ket
split!: if_split_asm)
then show ?thesis
by (auto intro!: trunc_ell2_reduces_norm mult_right_mono power_mono sum_nonneg norm_ge_zero zero_le_power2)
qed
also have ‹… ≤ (norm g * B)⇧2›
by (simp add: power_mult_distrib)
finally show ?thesis
by (metis Extra_Ordered_Fields.sign_simps(5) ‹0 ≤ B› norm_ge_zero power2_le_imp_le zero_compare_simps(4))
qed
have ‹((λF. trunc_ell2 F (C g)) ⤏ C g) (finite_subsets_at_top UNIV)›
by (rule trunc_ell2_lim_at_UNIV)
then have ‹((λF. norm (trunc_ell2 F (C g))) ⤏ norm (C g)) (finite_subsets_at_top UNIV)›
by (rule tendsto_norm)
then show ‹norm (C g) ≤ B * norm g›
apply (rule tendsto_upperbound)
using norm_trunc by (auto intro!: eventually_finite_subsets_at_top_weakI simp: )
qed
have ‹bounded_clinear C›
proof (intro bounded_clinearI allI)
fix g h :: ‹('x × 'a) ell2› and c :: complex
from C_hassum[of g] C_hassum[of h]
have ‹((λx. A' x *⇩V g + A' x *⇩V h) has_sum C g + C h) UNIV›
by (simp add: has_sum_add)
with C_hassum[of ‹g + h›]
show ‹C (g + h) = C g + C h›
by (metis (no_types, lifting) cblinfun.add_right has_sum_cong infsumI)
from C_hassum[of g]
have ‹((λx. c *⇩C (A' x *⇩V g)) has_sum c *⇩C C g) UNIV›
by (metis cblinfun_scaleC_right.rep_eq has_sum_cblinfun_apply)
with C_hassum[of ‹c *⇩C g›]
show ‹C (c *⇩C g) = c *⇩C C g›
by (metis (no_types, lifting) cblinfun.scaleC_right has_sum_cong infsumI)
from norm_C show ‹norm (C g) ≤ norm g * B›
by (simp add: sign_simps(5))
qed
define D where ‹D = CBlinfun C›
with ‹bounded_clinear C› have DC: ‹D *⇩V f = C f› for f
by (simp add: bounded_clinear_CBlinfun_apply)
have D_hassum: ‹has_sum_in cstrong_operator_topology A' UNIV D›
using C_hassum by (simp add: has_sum_in_cstrong_operator_topology DC)
then show ‹has_sum_in cstrong_operator_topology A' UNIV (controlled_op A)›
using controlled_op_def A'_def
by (metis (no_types, lifting) has_sum_in_infsum_in hausdorff_sot infsum_in_cong summable_on_in_def)
with D_hassum have DA: ‹D = controlled_op A›
apply (rule_tac has_sum_in_unique)
by auto
show ‹norm (controlled_op A) ≤ B›
apply (rule norm_cblinfun_bound, simp)
using norm_C by (simp add: DC flip: DA)
qed
lemma controlled_op_has_sum:
fixes A :: ‹'x ⇒ ('a ell2 ⇒⇩C⇩L 'b ell2)›
assumes ‹bdd_above (range (λx. norm (A x)))›
shows ‹has_sum_in cstrong_operator_topology (λx. selfbutter (ket x) ⊗⇩o A x) UNIV (controlled_op A)›
proof -
from assms obtain B where ‹norm (A x) ≤ B› for x
by (auto intro!: simp: bdd_above_def)
then show ?thesis
by (rule controlled_op_has_sum_aux)
qed
hide_fact controlled_op_has_sum_aux
lemma controlled_op_summable:
fixes A :: ‹'x ⇒ ('a ell2 ⇒⇩C⇩L 'b ell2)›
assumes ‹bdd_above (range (λx. norm (A x)))›
shows ‹summable_on_in cstrong_operator_topology (λx. selfbutter (ket x) ⊗⇩o A x) UNIV›
using controlled_op_has_sum[OF assms] summable_on_in_def by blast
lemma infsum_sot_cblinfun_apply:
assumes ‹summable_on_in cstrong_operator_topology f UNIV›
shows ‹infsum_in cstrong_operator_topology f UNIV *⇩V ψ = (∑⇩∞x. f x *⇩V ψ)›
by (metis assms has_sum_in_cstrong_operator_topology has_sum_in_infsum_in hausdorff_sot infsumI)
lemma controlled_op_ket[simp]:
assumes ‹bdd_above (range (λx. norm (A x)))›
shows ‹controlled_op A *⇩V (ket x ⊗⇩s ψ) = ket x ⊗⇩s (A x *⇩V ψ)›
proof -
have ‹controlled_op A *⇩V (ket x ⊗⇩s ψ) = (∑⇩∞y. (selfbutter (ket y) ⊗⇩o A y) *⇩V (ket x ⊗⇩s ψ))›
by (simp add: controlled_op_def assms infsum_sot_cblinfun_apply controlled_op_summable)
also have ‹… = ket x ⊗⇩s (A x *⇩V ψ)›
apply (subst infsum_single[where i=x])
by (simp_all add: tensor_op_ell2 cinner_ket)
finally show ?thesis
by -
qed
lemma controlled_op_ket'[simp]:
assumes ‹bdd_above (range (λx. norm (A x)))›
shows ‹controlled_op A *⇩V (ket (x, y)) = ket x ⊗⇩s (A x *⇩V ket y)›
by (metis assms controlled_op_ket tensor_ell2_ket)
lemma controlled_op_compose[simp]:
assumes [simp]: ‹bdd_above (range (λx. norm (A x)))›
assumes [simp]: ‹bdd_above (range (λx. norm (B x)))›
shows ‹controlled_op A o⇩C⇩L controlled_op B = controlled_op (λx. A x o⇩C⇩L B x)›
proof -
from assms(1) obtain a where ‹norm (A x) ≤ a› for x
by (auto simp: bdd_above_def)
moreover from assms(2) obtain b where ‹norm (B x) ≤ b› for x
by (auto simp: bdd_above_def)
ultimately have [simp]: ‹bdd_above (range (λx. norm (A x o⇩C⇩L B x)))›
apply (rule_tac bdd_aboveI[of _ ‹a*b›])
by (smt (verit, ccfv_SIG) Multiseries_Expansion_Bounds.mult_monos(1) imageE norm_cblinfun_compose
norm_ge_zero)
show ?thesis
apply (rule equal_ket)
apply (case_tac x)
by simp
qed
lemma controlled_op_adj[simp]:
assumes [simp]: ‹bdd_above (range (λx. norm (A x)))›
shows ‹(controlled_op A)* = controlled_op (λx. (A x)*)›
apply (rule cinner_ket_adjointI[symmetric])
by (auto intro!: simp: controlled_op_ket cinner_adj_left
simp flip: tensor_ell2_ket)
lemma controlled_op_id[simp]: ‹controlled_op (λ_. id_cblinfun) = id_cblinfun›
apply (rule equal_ket)
apply (case_tac x)
by (simp add: tensor_ell2_ket)
lemma controlled_op_unitary[simp]: ‹unitary (controlled_op U)› if [simp]: ‹⋀x. unitary (U x)›
proof -
have [iff]: ‹bdd_above (range (λx. norm (U x)))›
by (simp add: norm_isometry)
show ?thesis
unfolding unitary_def by auto
qed
lemma controlled_op_is_Proj[simp]: ‹is_Proj (controlled_op P)› if [simp]: ‹⋀x. is_Proj (P x)›
proof -
have [iff]: ‹bdd_above (range (λx. norm (P x)))›
using norm_is_Proj[OF that]
by (auto intro!: bdd_aboveI simp: )
show ?thesis
using that unfolding is_Proj_algebraic by auto
qed
lemma controlled_op_comp_butter:
assumes ‹bdd_above (range (λx. norm (A x)))›
shows ‹controlled_op A o⇩C⇩L Fst (selfbutter (ket x)) = Snd (A x) o⇩C⇩L Fst (selfbutter (ket x))›
using assms by (auto intro!: equal_ket simp: Fst_def tensor_op_ket cinner_ket)
lemma norm_ell2_finite: ‹norm ψ = sqrt (∑i∈UNIV. (cmod (Rep_ell2 ψ i))⇧2)› for ψ :: ‹_::finite ell2›
apply transfer
by (simp add: ell2_norm_finite)
lemma controlled_op_ket_swap[simp]:
assumes ‹bdd_above (range (λx. norm (U x)))›
shows ‹swap (controlled_op U) *⇩V (A ⊗⇩s ket x) = (U x *⇩V A) ⊗⇩s ket x›
by (simp add: assms swap_sandwich_swap_ell2 sandwich_apply)
lemma controlled_op_const: ‹controlled_op (λ_. P) = Snd P›
by (auto intro!: equal_ket simp: Snd_def tensor_op_ell2 simp flip: tensor_ell2_ket)
subsection ‹Superpositions›
lift_definition uniform_superpos :: ‹'a set ⇒ 'a ell2› is ‹λA x. complex_of_real (of_bool (x ∈ A) / sqrt (of_nat (card A)))›
proof (rename_tac A)
fix A :: ‹'a set›
show ‹has_ell2_norm (λx. complex_of_real (of_bool (x ∈ A) / sqrt (real (card A))))›
proof (cases ‹finite A›)
case True
show ?thesis
unfolding has_ell2_norm_def
apply (rule finite_nonzero_values_imp_summable_on)
using True by auto
next
case False
then show ?thesis
by simp
qed
qed
lemma norm_uniform_superpos: ‹norm (uniform_superpos A) = 1› if ‹finite A› and ‹A ≠ {}›
proof (transfer' fixing: A)
have ‹ell2_norm (λx. complex_of_real (of_bool (x ∈ A) / sqrt (real (card A))))
= sqrt (∑⇩∞x. (cmod (complex_of_real (of_bool (x ∈ A) / sqrt (real (card A)))))⇧2)›
by (simp add: ell2_norm_def)
also have ‹… = sqrt (∑⇩∞x∈A. (cmod (complex_of_real (1 / sqrt (real (card A)))))⇧2)›
apply (rule arg_cong[where f=sqrt])
apply (rule infsum_cong_neutral)
by auto
also have ‹… = sqrt (∑x∈A. (cmod (complex_of_real (1 / sqrt (real (card A)))))⇧2)›
by simp
also have ‹… = sqrt (real (card A) * (cmod (1 / complex_of_real (sqrt (real (card A)))))⇧2)›
by (simp add: that)
also have ‹… = sqrt (real (card A) * ((1 / sqrt (real (card A)))⇧2))›
by (simp add: cmod_def)
also have ‹… = 1›
using that
by (simp add: power_one_over)
finally show ‹ell2_norm (λx. complex_of_real (of_bool (x ∈ A) / sqrt (real (card A)))) = 1›
by -
qed
lemma uniform_superpos_infinite: ‹uniform_superpos A = 0› if ‹infinite A›
apply (transfer' fixing: A)
using that
by simp
lemma uniform_superpos_empty: ‹uniform_superpos A = 0› if ‹A = {}›
apply (transfer' fixing: A)
using that
by simp
text ‹Alternative definition.›
lemma uniform_superpos_def2: ‹uniform_superpos A = (∑f∈A. ket f /⇩C csqrt (card A))›
proof -
wlog [simp]: ‹finite A› ‹A ≠ {}›
using negation uniform_superpos_empty uniform_superpos_infinite by force
show ?thesis
proof (rule cinner_ket_eqI)
fix f
show ‹ket f ∙⇩C (uniform_superpos A) = ket f ∙⇩C (∑f∈A. ket f /⇩C csqrt (card A))›
proof (cases ‹f ∈ A›)
case True
then have ‹ket f ∙⇩C (uniform_superpos A) = 1 / csqrt (card A)›
apply (subst cinner_ket_left)
apply (transfer fixing: f)
by auto
moreover have ‹ket f ∙⇩C (∑f∈A. ket f /⇩C csqrt (card A)) = 1 / csqrt (card A)›
apply (subst cinner_sum_right)
apply (subst sum_single[where i=f])
using True by (auto simp: inverse_eq_divide)
finally show ?thesis
by simp
next
case False
then have ‹ket f ∙⇩C (uniform_superpos A) = 0›
apply (subst cinner_ket_left)
apply (transfer fixing: f)
by auto
moreover have ‹ket f ∙⇩C (∑f∈A. ket f /⇩C csqrt (card A)) = 0›
apply (subst cinner_sum_right)
apply (rule sum.neutral)
using False by auto
finally show ?thesis
by simp
qed
qed
qed
subsection ‹Lifting ell2 to option type›
lift_definition lift_ell2' :: ‹'a ell2 ⇒ 'a option ell2› is ‹λψ x. case x of Some x' ⇒ ψ x' | None ⇒ 0›
proof -
fix ψ :: ‹'a ⇒ complex›
assume ‹has_ell2_norm ψ›
then have ‹(λx. norm ((ψ x)⇧2)) summable_on UNIV›
by (simp add: has_ell2_norm_def)
then have ‹(λx. case x of Some x' ⇒ norm ((ψ x')⇧2) | None ⇒ 0) o Some summable_on UNIV›
by (metis comp_eq_dest_lhs option.simps(5) summable_on_cong)
then have ‹(λx. case x of Some x' ⇒ norm ((ψ x')⇧2) | None ⇒ 0) summable_on Some ` UNIV›
by (meson inj_Some summable_on_reindex)
then have ‹(λx. case x of Some x' ⇒ norm ((ψ x')⇧2) | None ⇒ 0) summable_on UNIV›
apply (rule summable_on_cong_neutral[THEN iffD1, rotated -1])
by (auto simp add: notin_range_Some)
then show ‹has_ell2_norm (case_option 0 ψ)›
apply (simp add: has_ell2_norm_def)
by (metis (mono_tags, lifting) norm_zero option.case_eq_if summable_on_cong zero_power2)
qed
lemma clinear_lift_ell2': ‹clinear lift_ell2'›
apply (rule clinearI; transfer)
by (auto intro!: ext simp add: option.case_eq_if)
lemma lift_ell2'_norm[simp]: ‹norm (lift_ell2' ψ) = norm ψ›
proof transfer
fix ψ :: ‹'a ⇒ complex›
have ‹(ell2_norm ψ)⇧2 = infsum (λx. (norm (ψ x))⇧2) UNIV›
apply (simp add: ell2_norm_def)
by (meson infsum_nonneg zero_le_power2)
also have ‹… = infsum ((λx. case x of Some x' ⇒ (norm (ψ x'))⇧2 | None ⇒ 0) o Some) UNIV›
apply (rule infsum_cong) by auto
also have ‹… = infsum (λx. case x of Some x' ⇒ (norm (ψ x'))⇧2 | None ⇒ 0) (Some ` UNIV)›
by (simp add: infsum_reindex)
also have ‹… = infsum (λx. case x of Some x' ⇒ (norm (ψ x'))⇧2 | None ⇒ 0) UNIV›
apply (rule infsum_cong_neutral)
by (auto simp add: notin_range_Some)
also have ‹… = (ell2_norm (case_option 0 ψ))⇧2›
apply (simp add: ell2_norm_def)
by (smt (verit, ccfv_SIG) infsum_nonneg infsum_cong norm_zero option.case_eq_if real_sqrt_pow2_iff zero_le_power2 zero_power2)
finally show ‹ell2_norm (case_option 0 ψ) = ell2_norm ψ›
by (simp add: ell2_norm_geq0)
qed
lemma bounded_clinear_lift_ell2'[bounded_clinear, simp]: ‹bounded_clinear lift_ell2'›
by (metis bounded_clinear.intro bounded_clinear_axioms.intro clinear_lift_ell2' lift_ell2'_norm mult.commute mult_1 order.refl)
lift_definition lift_ell2 :: ‹'a ell2 ⇒⇩C⇩L 'a option ell2› is lift_ell2'
by simp
definition lift_op :: ‹('a ell2 ⇒⇩C⇩L 'b ell2) ⇒ ('a option ell2 ⇒⇩C⇩L 'b option ell2)› where
‹lift_op A = (lift_ell2 o⇩C⇩L A o⇩C⇩L lift_ell2*) + butterfly (ket None) (ket None)›
lemma lift_ell2_ket[simp]: ‹lift_ell2 *⇩V ket x = ket (Some x)›
unfolding lift_ell2.rep_eq apply transfer
by (auto intro!: ext simp: of_bool_def split!: option.split if_split_asm)
lemma isometry_lift_ell2[simp]: ‹isometry lift_ell2›
apply (rule norm_preserving_isometry)
by (simp add: lift_ell2.rep_eq)
lemma lift_op_adj: ‹(lift_op A)* = lift_op (A*)›
unfolding lift_op_def
apply (simp add: adj_plus)
by (simp add: cblinfun_assoc_left(1))
lemma bra_None_lift_ell2: ‹bra None o⇩C⇩L lift_ell2 = 0›
apply (rule cblinfun_eqI)
apply (simp add: lift_ell2.rep_eq)
apply transfer
by (simp add: infsum_0)
lemma lift_op_mult: ‹lift_op A o⇩C⇩L lift_op B = lift_op (A o⇩C⇩L B)›
proof -
have ‹lift_op A o⇩C⇩L lift_op B =
(lift_ell2 o⇩C⇩L A o⇩C⇩L (lift_ell2* o⇩C⇩L lift_ell2) o⇩C⇩L B o⇩C⇩L lift_ell2*)
+ (lift_ell2 o⇩C⇩L A o⇩C⇩L (bra None o⇩C⇩L lift_ell2)* o⇩C⇩L bra None)
+ (vector_to_cblinfun (ket None) o⇩C⇩L (bra None o⇩C⇩L lift_ell2) o⇩C⇩L B o⇩C⇩L lift_ell2*)
+ butterfly (ket None) (ket None)›
unfolding lift_op_def
apply (simp add: adj_plus cblinfun_compose_add_right cblinfun_compose_add_left del: isometryD)
apply (simp add: butterfly_def cblinfun_compose_assoc del: isometryD)
by (metis butterfly_def cblinfun_comp_butterfly)
also have ‹… = (lift_ell2 o⇩C⇩L (A o⇩C⇩L B) o⇩C⇩L lift_ell2*) + butterfly (ket None) (ket None)›
by (simp add: bra_None_lift_ell2 cblinfun_compose_assoc)
also have ‹… = lift_op (A o⇩C⇩L B)›
by (simp add: lift_op_def)
finally show ?thesis
by -
qed
lemma lift_ell2_adj_None[simp]: ‹lift_ell2* *⇩V ket None = 0›
by (simp add: cinner_adj_right cinner_ket_eqI lift_ell2_ket)
lemma lift_ell2_adj_Some[simp]: ‹lift_ell2* *⇩V ket (Some x) = ket x›
by (simp add: cinner_adj_right cinner_ket cinner_ket_eqI lift_ell2_ket)
lemma lift_op_id[simp]: ‹lift_op id_cblinfun = id_cblinfun›
apply (rule equal_ket, case_tac x)
by (auto simp: lift_op_def cblinfun.add_left cblinfun_compose_add_right lift_ell2_adj_None lift_ell2_ket)
lemma isometry_lift_op[simp]: ‹isometry (lift_op A)› if ‹isometry A›
by (simp add: isometry_def lift_op_mult lift_op_adj isometryD[OF that])
lemma unitary_lift_op[simp]: ‹unitary (lift_op A)› if ‹unitary A›
by (metis isometry_lift_op lift_op_adj that unitary_twosided_isometry)
lemma lift_op_None[simp]: ‹lift_op A *⇩V ket None = ket None›
unfolding lift_op_def by (auto simp: cblinfun.add_left)
lemma lift_op_Some[simp]: ‹lift_op A *⇩V ket (Some x) = lift_ell2 *⇩V A *⇩V ket x›
unfolding lift_op_def by (auto simp: cblinfun.add_left)
declare register_tensor_is_register[simp]
lemma sum_sqrt: ‹(∑i<n. sqrt i) ≤ 2/3 * (sqrt n)^3› for n :: nat
proof (induction n)
case 0
show ?case
by simp
next
case (Suc n)
have ‹(∑i<Suc n. sqrt i) ≤ 2/3 * sqrt (real n) ^ 3 + sqrt n›
using Suc
by simp
also have ‹… ≤ 2/3 * sqrt (Suc n) ^ 3›
proof -
define x :: real where ‹x = n›
define f where ‹f z = 2/3 * (sqrt z)^3› for z
have f': ‹(f has_real_derivative sqrt z) (at z)› if ‹z > 0› for z
apply (rule ssubst[of ‹sqrt z›, rotated])
unfolding f_def
apply (rule that DERIV_real_sqrt derivative_eq_intros refl)+
using that
apply simp
by (smt (verit, del_insts) Extra_Ordered_Fields.sign_simps(5) nonzero_eq_divide_eq sqrt_divide_self_eq)
have cont: ‹continuous_on {x..x+1} f›
unfolding f_def
by (intro continuous_intros)
have ‹x ≥ 0›
using x_def by auto
obtain l z where ‹x < z› ‹z < x + 1› and f'l: ‹(f has_real_derivative l) (at z)› and fdelta: ‹f (x + 1) - f x = (x + 1 - x) * l›
apply atomize_elim
apply (subst ex_comm)
apply (rule MVT)
apply simp
apply (rule cont)
using f'
by (smt (verit, best) ‹0 ≤ x› real_differentiable_def)
then have ‹z > 0›
using ‹0 ≤ x› by linarith
from f'[OF this] f'l have [simp]: ‹l = sqrt z›
using DERIV_unique by blast
from fdelta
have ‹f (x + 1) - f x ≥ sqrt x›
using ‹x < z› by auto
then show ?thesis
unfolding x_def f_def
by (smt (verit, best) Num.of_nat_simps(3))
qed
finally show ?case
by -
qed
lemma register_inj':
assumes ‹register Q›
shows ‹Q a = Q b ⟷ a = b›
using register_inj[OF assms] by blast
lemma norm_cblinfun_apply_leq1I:
assumes ‹norm U ≤ 1›
assumes ‹norm ψ ≤ 1›
shows ‹norm (U *⇩V ψ) ≤ 1›
by (smt (verit, best) assms(1,2) mult_left_le_one_le norm_cblinfun norm_ge_zero)
lemma times_sqrtn_div_n[simp]:
assumes ‹n ≥ 0›
shows ‹a * sqrt n / n = a / sqrt n›
by (metis assms divide_divide_eq_right real_div_sqrt)
lemma Proj_tensor_Proj: ‹Proj I ⊗⇩o Proj J = Proj (I ⊗⇩S J)›
by (simp add: Proj_on_own_range is_Proj_tensor_op
tensor_ccsubspace_via_Proj)
lemma extend_mult_rule: ‹a * b = c ⟹ a * (b * d) = c * d› for a b c d :: ‹_::semigroup_mult›
by (metis Groups.mult_ac(1))
end