Theory CO_Invariants
section ‹‹CO_Invariants› – Preservation of invariants under compressed oracle queries›
theory CO_Invariants imports
Invariant_Preservation
CO_Operations
begin
lemma function_oracle_ket_invariant: ‹function_oracle h *⇩S ket_invariant I = ket_invariant ((λ(x,y). (x,y + h x)) ` I)›
by (auto intro!: arg_cong[where f=‹λx. ccspan (x ` I)›] simp add: ket_invariant_def cblinfun_image_ccspan image_image function_oracle_apply)
lemma function_oracle_Snd_ket_invariant: ‹Snd (function_oracle h) *⇩S ket_invariant I = ket_invariant ((λ(w,x,y). (w,x,y+h x)) ` I)›
by (auto intro!: ext arg_cong[where f=‹λx. ccspan (x ` I)›]
simp add: Snd_def ket_invariant_def cblinfun_image_ccspan image_image function_oracle_apply tensor_op_ket tensor_ell2_ket)
context compressed_oracle begin
text ‹This lemma allows to simplify the preservation of invariants under invocations of the compressed oracle.
Given an invariant \<^term>‹I›, it can be split into many invariants \<^term>‹I1 z› for which preservation is shown
then with respect to a fixed oracle input \<^term>‹x z›, using the simpler oracle \<^const>‹query1› instead.
This allows to reduce complex cases to more elementary ones that talk about a single output of the oracle.
Lemmas ‹inv_split_reg_query› and ‹inv_split_reg_query'› are the specific instantiations of this for the
two compressed oracle variants \<^const>‹query› and \<^const>‹query'›.›
lemma inv_split_reg_query_generic:
fixes query query1
assumes query_local: ‹query = controlled_op (λx. (Fst; Snd o function_at x) query1)›
fixes X :: ‹'x update ⇒ 'm update›
and Y :: ‹'y update ⇒ 'm update›
and H :: ‹('x⇀'y) update ⇒ 'm update›
and K :: ‹'z ⇒ 'm ell2 ccsubspace›
and x :: ‹'z ⇒ 'x›
and M :: ‹'z set›
assumes XK: ‹⋀z. z∈M ⟹ K z ≤ lift_invariant X (ket_invariant {x z})›
assumes pres_I1: ‹⋀z. z∈M ⟹ preserves query1 (I1 z) (J1 z) ε›
assumes I_leq: ‹I ≤ (SUP z∈M. K z ⊓ lift_invariant (Y;H o function_at (x z)) (I1 z))›
assumes J_geq: ‹⋀z. z∈M ⟹ J ≥ K z ⊓ lift_invariant (Y;H o function_at (x z)) (J1 z)›
assumes YK: ‹⋀z. z∈M ⟹ compatible_register_invariant Y (K z)›
assumes HK: ‹⋀z. z∈M ⟹ compatible_register_invariant (H o function_at (x z)) (K z)›
assumes [simp]: ‹compatible X Y› ‹compatible X H› ‹compatible Y H›
assumes U: ‹U = ((X;(Y;H)) query)›
assumes orthoK: ‹⋀z z'. z∈M ⟹ z'∈M ⟹ z ≠ z' ⟹ orthogonal_spaces (K z) (K z')›
assumes ‹ε ≥ 0›
assumes ‹finite M›
shows ‹preserves U I J ε›
proof (rule inv_split_reg[where ?U1.0=‹λ_. query1› and ?I1.0=I1 and ?J1.0=J1
and Y=‹λz. (Y;H o function_at (x z))› and K=K])
show ‹(Y;H ∘ function_at (x z)) query1 *⇩V ψ = U *⇩V ψ›
if ‹z∈M› and ‹ψ ∈ space_as_set (K z)› for ψ z
proof -
from that(2) XK[OF ‹z∈M›] have ‹ψ ∈ space_as_set (lift_invariant X (ket_invariant {x z}))›
using less_eq_ccsubspace.rep_eq by blast
then have ψx: ‹ψ = X (Proj (ket_invariant {x z})) *⇩V ψ›
by (metis Proj_lift_invariant Proj_fixes_image ‹compatible X Y› compatible_register1)
have ‹U *⇩V ψ = (X;(Y;H)) query *⇩V ψ›
by (simp add: U)
also have ‹… = (X;(Y;H)) (controlled_op (λx. (Fst;Snd ∘ function_at x) query1)) *⇩V ψ›
by (simp add: query_local)
also have ‹… = (X;(Y;H)) (controlled_op (λx. (Fst;Snd ∘ function_at x) query1) o⇩C⇩L Fst (selfbutter (ket (x z)))) *⇩V ψ›
by (simp add: register_pair_apply Fst_def flip: register_mult Proj_ket_invariant_butterfly ψx)
also have ‹… = (X;(Y;H)) (Snd ((Fst;Snd ∘ function_at (x z)) query1) o⇩C⇩L Fst (selfbutter (ket (x z)))) *⇩V ψ›
by (simp add: controlled_op_comp_butter)
also have ‹… = (X;(Y;H)) (Snd ((Fst;Snd ∘ function_at (x z)) query1)) *⇩V ψ›
by (simp add: register_pair_apply Fst_def flip: register_mult Proj_ket_invariant_butterfly ψx)
also have ‹… = (((X;(Y;H)) o Snd o (Fst;Snd ∘ function_at (x z))) query1) *⇩V ψ›
by auto
also have ‹… = (Y;H ∘ function_at (x z)) query1 *⇩V ψ›
by (simp add: register_pair_Snd register_pair_Fst flip: register_comp_pair comp_assoc)
finally show ?thesis
by simp
qed
from pres_I1 show ‹preserves query1 (I1 z) (J1 z) ε› if ‹z∈M› for z
using that by -
from I_leq
show ‹I ≤ (SUP z∈M. K z ⊓ lift_invariant (Y;H o function_at (x z)) (I1 z))›
by -
from J_geq
show ‹J ≥ K z ⊓ lift_invariant (Y;H o function_at (x z)) (J1 z)› if ‹z∈M› for z
using that by -
show ‹compatible_register_invariant (Y;H ∘ function_at (x z)) (K z)› if ‹z∈M› for z
using YK[OF that] HK[OF that] by (rule compatible_register_invariant_pair)
from orthoK
show ‹orthogonal_spaces (K z) (K z')› if ‹z∈M› ‹z'∈M› ‹z ≠ z'› for z z'
using that by -
show ‹register (Y;H ∘ function_at (x z))› for z
by simp
from assms show ‹ε ≥ 0›
by -
from assms show ‹finite M›
by metis
qed
lemmas inv_split_reg_query = inv_split_reg_query_generic[OF query_local]
lemmas inv_split_reg_query' = inv_split_reg_query_generic[OF query'_local]
definition ‹num_queries q = {(x::'x, y::'y, D::'x⇀'y). card (dom D) ≤ q}›
definition ‹num_queries' q = {D::'x⇀'y. card (dom D) ≤ q}›
lemma num_queries_num_queries': ‹num_queries q = UNIV × UNIV × (num_queries' q)›
by (auto intro!: simp: num_queries_def num_queries'_def)
lemma ket_invariant_num_queries_num_queries': ‹ket_invariant (num_queries q) = ⊤ ⊗⇩S ⊤ ⊗⇩S ket_invariant (num_queries' q)›
by (auto simp: ket_invariant_tensor num_queries_num_queries' simp flip: ket_invariant_UNIV)
text ‹This lemma shows that the number of recorded queries (defined outputs in the oracle register)
increases at most by 1 upon each query of the compressed oracle.
The two instantiations for the two compressed oracle variants are given afterwards.›
lemma preserves_num_generic:
fixes query query1
assumes query_local: ‹query = controlled_op (λx. (Fst; Snd o function_at x) query1)›
shows ‹preserves_ket query (num_queries q) (num_queries (q+1)) 0›
proof -
define K where ‹K x = ket_invariant {(x::'x,y::'y,D::'x⇀'y) | y D. card (dom D - {x}) ≤ q}› for x
define Kd where ‹Kd x D0 = ket_invariant {(x::'x,y::'y,D::'x⇀'y) | y D. (∀x'≠x. D x' = D0 x')}› for x D0
have K: ‹K x = (SUP D0∈{D0. D0 x = None ∧ card (dom D0 - {x}) ≤ q}. Kd x D0)› for x
proof -
have aux1: ‹card (dom D - {x}) ≤ q ⟹
∃D'. D' x = None ∧ card (dom D' - {x}) ≤ q ∧ (∀x'. x' ≠ x ⟶ D x' = D' x')› for D
apply (rule exI[of _ ‹D(x:=None)›])
by auto
have aux2: ‹D' x = None ⟹
card (dom D' - {x}) ≤ q ⟹ ∀x'. x' ≠ x ⟶ D x' = D' x' ⟹ card (dom D - {x}) ≤ q› for D' D
by (smt (verit) DiffE Diff_empty card_mono domIff dom_minus dual_order.trans finite_class.finite_code singleton_iff subsetI)
show ?thesis
by (auto intro!: aux1 aux2 simp add: K_def Kd_def simp flip: ket_invariant_SUP)
qed
define Kdx where ‹Kdx x D0 x' = ket_invariant {(x::'x,y::'y,D::'x⇀'y) | y D. D x' = D0 x'}› for D0 x' x
have Kd: ‹Kd x D0 = (INF x'∈-{x}. Kdx x D0 x')› for x D0
unfolding Kd_def Kdx_def
apply (subst ket_invariant_INF[symmetric])
apply (rule arg_cong[where f=ket_invariant])
by auto
have Kdx: ‹Kdx x D0 x' = lift_invariant reg_1_3 (ket_invariant {x}) ⊓ lift_invariant (reg_3_3 o function_at x') (ket_invariant {D0 x'})› for D0 x' x
unfolding Kdx_def reg_3_3_def reg_1_3_def
apply (simp add: lift_invariant_comp)
apply (subst lift_invariant_function_at_ket_inv)
apply (subst lift_Snd_ket_inv)
apply (subst lift_Snd_ket_inv)
apply (subst lift_Fst_ket_inv)
apply (subst ket_invariant_inter)
apply (rule arg_cong[where f=ket_invariant])
by auto
show ?thesis
proof (rule inv_split_reg_query_generic[where X=‹reg_1_3› and Y=‹reg_2_3› and H=‹reg_3_3› and K=K
and x=‹λx. x› and ?I1.0=‹λ_. ⊤› and ?J1.0=‹λ_. ⊤›, OF query_local])
show ‹query = (reg_1_3;(reg_2_3;reg_3_3)) query›
by (auto simp add: pair_Fst_Snd reg_1_3_def reg_2_3_def reg_3_3_def)
show ‹compatible reg_1_3 reg_2_3› ‹compatible reg_1_3 reg_3_3› ‹compatible reg_2_3 reg_3_3›
by simp_all
show ‹compatible_register_invariant reg_2_3 (K x)› for x
unfolding K Kd Kdx
apply (rule compatible_register_invariant_SUP, simp)
apply (rule compatible_register_invariant_INF, simp)
apply (rule compatible_register_invariant_inter, simp)
apply (rule compatible_register_invariant_compatible_register)
apply simp
apply (rule compatible_register_invariant_compatible_register)
by simp
show ‹compatible_register_invariant (reg_3_3 o function_at x) (K x)› for x
unfolding K Kd Kdx
apply (rule compatible_register_invariant_SUP, simp)
apply (rule compatible_register_invariant_INF, simp)
apply (rule compatible_register_invariant_inter, simp)
apply (rule compatible_register_invariant_compatible_register)
apply simp
apply (rule compatible_register_invariant_compatible_register)
by simp
show ‹ket_invariant (num_queries q)
≤ (SUP x. K x ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) ⊤)›
by (auto intro!: card_Diff1_le[THEN order_trans]
simp: K_def lift_Fst_ket_inv reg_1_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
num_queries_def)
have *: ‹card (dom D) ≤ card (dom D - {x}) + 1› for D x
by (metis One_nat_def card.empty card.insert diff_card_le_card_Diff empty_not_insert finite.intros(1)
finite_insert insert_absorb le_diff_conv)
show ‹K x ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) ⊤
≤ ket_invariant (num_queries (q + 1))› for x
by (auto intro!: *[THEN order_trans]
simp add: num_queries_def K_def lift_Fst_ket_inv reg_1_3_def ket_invariant_inter ket_invariant_SUP[symmetric])
show ‹preserves query1 ⊤ ⊤ 0›
by simp
show ‹orthogonal_spaces (K x) (K x')› if ‹x ≠ x'› for x x'
unfolding K_def orthogonal_spaces_ket using that by auto
show ‹K x ≤ lift_invariant reg_1_3 (ket_invariant {x})› for x
by (auto simp add: K Kd_def reg_1_3_def lift_inv_prod' lift_Fst_ket_inv
simp flip: ket_invariant_SUP)
show ‹0 ≤ (0::real)›
by auto
show ‹finite (UNIV::'x set)›
by simp
qed
qed
lemmas preserves_num = preserves_num_generic[OF query_local]
lemmas preserves_num' = preserves_num_generic[OF query'_local]
text ‹We now present various lemmas that give concrete bounds for the preservation of invariants
under various conditions, for \<^const>‹query1› (and \<^const>‹query1'›).
The invariants are formulated specifically for an application of \<^const>‹query1› to a two-partite
system with query output register and oracle register only.
These can be applied to derive invariant preservation for full compressed oracle queries on arbitrary systems by
first splitting the invariant using @{thm [source] inv_split_reg_query}.›
text ‹The first bound is applicable for ket-invariants that do not put any conditions on the output register
and that not not require that the output register is defined (not \<^term>‹None›) after the query.
Lemmas ‹preserve_query1_bound› and ‹preserve_query1'_bound›; with slightly simplified bounds in
‹preserve_query1_simplified›, ‹preserve_query1'_simplified›.›
definition ‹preserve_query1_bound NoneI b⇩i b⇩j⇩0 = 4 * sqrt b⇩j⇩0 * sqrt b⇩i / N + 2 * of_bool NoneI * sqrt b⇩j⇩0 / sqrt N›
lemma preserve_query1:
assumes IJ: ‹I ⊆ J›
assumes [simp]: ‹None ∈ J›
assumes b⇩i: ‹card (Some -` I) ≤ b⇩i›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
assumes ε: ‹ε ≥ preserve_query1_bound (None∈I) b⇩i b⇩j⇩0›
shows ‹preserves_ket query1 (UNIV × I) (UNIV × J) ε›
proof (rule preservesI')
show ‹ε ≥ 0›
using _ ε apply (rule order.trans)
by (simp add: preserve_query1_bound_def)
fix ψ :: ‹('y × 'y option) ell2›
assume ψ': ‹ψ ∈ space_as_set (ket_invariant (UNIV × I))›
assume ‹norm ψ = 1›
define I' J' where ‹I' = Some -` I› and ‹J' = Some -` J›
from ψ' have ψ: ‹ψ ∈ space_as_set (ket_invariant (UNIV × ((Some ` I' ∪ {None}))))›
using I'_def less_eq_ccsubspace.rep_eq by fastforce
have [simp]: ‹I' ⊆ J'›
using I'_def J'_def IJ by blast
define β where ‹β = Rep_ell2 ψ›
then have β: ‹ψ = (∑yd∈UNIV×(Some ` I' ∪ {None}). β yd *⇩C ket yd)›
using ell2_sum_ket_ket_invariant[OF ψ] by auto
have βbound: ‹(∑yd∈UNIV×(Some ` I' ∪ {None}). (cmod (β yd))⇧2) ≤ 1› (is ‹?lhs ≤ 1›)
apply (subgoal_tac ‹(norm ψ)⇧2 = ?lhs›)
apply (simp add: ‹norm ψ = 1›)
by (simp add: β pythagorean_theorem_sum)
have βNone0: ‹β (y,None) = 0› if ‹None ∉ I› for y
using ψ' that by (simp add: β_def ket_invariant_Rep_ell2)
have [simp]: ‹Some -` insert None X = Some -` X› for X :: ‹'z option set›
by auto
have [simp]: ‹Some -` Some ` X = X› for X :: ‹'z set›
by auto
have [simp]: ‹Some x ∈ J ⟷ x ∈ J'› for x
by (simp add: J'_def)
have [simp]: ‹x ∈ I' ⟹ x ∈ J'› for x
using ‹I' ⊆ J'› by blast
have [simp]: ‹(∑x∈X. if x ∉ Y then f x else 0) = (∑x∈X-Y. f x)› if ‹finite X› for f :: ‹'y ⇒ 'z::ab_group_add› and X Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹(∑x∈X. ∑y∈Y. if x ∉ X' then f x y else 0) = (∑x∈X-X'. ∑y∈Y. f x y)› if ‹finite X›
for f :: ‹'x ⇒ 'y ⇒ 'z::ab_group_add› and X X' Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹β yd *⇩C a *⇩C b = a *⇩C β yd *⇩C b› for yd a and b :: ‹'z::complex_vector›
by auto
have [simp]: ‹cmod α = inverse (sqrt N)› ‹cmod (α⇧2) = inverse N› ‹cmod (α^3) = inverse (N * sqrt N)› ‹cmod (α^4) = inverse (N⇧2)›
by (auto simp: power4_eq_xxxx power2_eq_square norm_mult numeral_3_eq_3 α_def inverse_eq_divide norm_divide norm_power power_one_over)
have [simp]: ‹card (Some ` I') ≤ b⇩i›
by (metis I'_def b⇩i card_image inj_Some)
have bound_J'[simp]: ‹card (Some ` (- J')) ≤ b⇩j⇩0›
using b⇩j⇩0 unfolding J'_def by (simp add: card_image)
define φ and PJ :: ‹('y × 'y option) update› where
‹φ = query1 *⇩V ψ› and ‹PJ = Proj (ket_invariant (UNIV × -J))›
have [simp]: ‹PJ *⇩V ket (x,y) = (if y∈-J then ket (x,y) else 0)› for x y
by (simp add: Proj_ket_invariant_ket PJ_def)
have P0φ: ‹PJ *⇩V φ =
α^4 *⇩C (∑y∈UNIV. ∑d∈I'. ∑y'∈UNIV. ∑d'∈- J'. β (y, Some d) *⇩C ket (y', Some d')) -
α⇧2 *⇩C (∑y∈UNIV. ∑d∈I'. ∑d'∈- J'. β (y, Some d) *⇩C ket (y + d, Some d')) -
α⇧2 *⇩C (∑y∈UNIV. ∑d∈I'. ∑d'∈- J'. β (y, Some d) *⇩C ket (y + d', Some d')) +
α⇧2 *⇩C (∑y∈UNIV. ∑d∈I'. ∑d'∈- J'. β (y, Some d) *⇩C ket (y, Some d')) +
α *⇩C (∑y∈UNIV. ∑d'∈- J'. β (y, None) *⇩C ket (y + d', Some d')) -
α^3 *⇩C (∑y∈UNIV. ∑y'∈UNIV. ∑d'∈- J'. β (y, None) *⇩C ket (y', Some d'))›
(is ‹_ = ?t1 - ?t2 - ?t3 + ?t4 + ?t5 - ?t6›)
by (simp add: φ_def β query1 option_sum_split vimage_Compl
cblinfun.add_right cblinfun.diff_right if_distrib Compl_eq_Diff_UNIV
vimage_singleton_inj sum_sum_if_eq sum.distrib scaleC_diff_right scaleC_sum_right
sum_subtractf case_prod_beta sum.cartesian_product' scaleC_add_right add_diff_eq
cblinfun.scaleC_right cblinfun.sum_right
flip: sum.Sigma add.assoc scaleC_scaleC
cong del: option.case_cong if_cong)
have norm_t1: ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket y'd') ≤ sqrt (N * b⇩i)› for y'd' :: ‹'y × 'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
by (auto simp: N_def)
have ‹norm ?t1 = inverse (N⇧2) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). ∑yd∈UNIV × Some ` I'. β yd *⇩C ket y'd')›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap) apply (subst (2) sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N⇧2) * (N * sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def real_sqrt_mult algebra_simps real_sqrt_mult algebra_simps
sqrt_sqrt[THEN extend_mult_rule])
also have ‹… ≤ inverse (N⇧2) * (N * sqrt b⇩j⇩0 * sqrt b⇩i)›
by (metis bound_J' linordered_field_class.inverse_nonnegative_iff_nonnegative mult.commute mult_right_mono of_nat_0_le_iff of_nat_mono real_sqrt_ge_zero real_sqrt_le_iff)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (smt (verit) ab_semigroup_mult_class.mult_ac(1) divide_inverse_commute of_nat_power power2_eq_square real_divide_square_eq)
finally show ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t2: ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {y. δ = fst y + the (snd y) ∧ y ∈ UNIV × Some ` I'} ≤ card I'› for δ
apply (rule card_inj_on_le[where f=‹λy. the (snd y)›])
by (auto intro!: inj_onI)
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd + the (snd yd), d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t2 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd + the (snd yd), d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t3: ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {y. a = fst y ∧ y ∈ UNIV × (I ∩ range Some)} ≤ card I'› for a :: 'y
apply (rule card_inj_on_le[where f=‹λy. the (snd y)›])
by (auto intro!: inj_onI simp: I'_def)
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd + the d', d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t3 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × Some ` I'.
β yd *⇩C ket (fst yd + the d', d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t4: ‹norm ?t4 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {y. a = fst y ∧ y ∈ UNIV × (I ∩ range Some)} ≤ card I'› for a :: 'y
apply (rule card_inj_on_le[where f=‹λy. the (snd y)›])
by (auto intro!: inj_onI simp: I'_def)
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd, d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t4 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × Some ` I'.
β yd *⇩C ket (fst yd, d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t4 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t5: ‹norm ?t5 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
proof (cases ‹None∈I›)
case True
have *: ‹card {y. a = fst y ∧ y ∈ UNIV × {None :: 'y option}} ≤ card {()}› for a :: 'y
apply (rule card_inj_on_le[where f=‹λ_. undefined›])
by (auto intro!: inj_onI)
have *: ‹norm (∑yd∈UNIV × {None}. β yd *⇩C ket (fst yd + the d', d')) ≤ sqrt (1::nat)› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * by auto
have ‹norm ?t5 = inverse (sqrt N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × {None}.
β yd *⇩C ket (fst yd + the d', d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (sqrt N) * (sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse (sqrt N) * sqrt b⇩j⇩0›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by (simp add: True divide_inverse_commute)
finally show ?thesis
by -
next
case False
then show ?thesis
using βNone0 by auto
qed
have norm_t6: ‹norm ?t6 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
proof (cases ‹None∈I›)
case True
have *: ‹norm (∑yd∈UNIV × {None}. β yd *⇩C ket y'd') ≤ sqrt N› for y'd' :: ‹'y × 'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
by (auto simp: N_def)
have ‹norm ?t6 = inverse (N * sqrt N) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). ∑yd∈UNIV × {None}. β yd *⇩C ket y'd')›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N * sqrt N) * (N * sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def mult.commute real_sqrt_mult vector_space_over_itself.scale_scale)
also have ‹… ≤ inverse (N * sqrt N) * (N * sqrt b⇩j⇩0)›
by (simp add: N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
using True by (simp add: divide_inverse_commute less_eq_real_def N_def)
finally show ?thesis
by -
next
case False
then show ?thesis
using βNone0 by auto
qed
have ‹norm (PJ *⇩V φ) ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N + sqrt b⇩j⇩0 * sqrt b⇩i / N + sqrt b⇩j⇩0 * sqrt b⇩i / N
+ sqrt b⇩j⇩0 * sqrt b⇩i / N + of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N + of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
unfolding P0φ
apply (rule norm_triangle_le_diff norm_triangle_le, rule add_mono)+
apply (rule norm_t1)
apply (rule norm_t2)
apply (rule norm_t3)
apply (rule norm_t4)
apply (rule norm_t5)
by (rule norm_t6)
also have ‹… ≤ 4 * sqrt b⇩j⇩0 * sqrt b⇩i / N + 2 * of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by (simp add: mult.commute vector_space_over_itself.scale_left_commute)
also have ‹… ≤ ε›
using ε by (auto intro!: simp add: preserve_query1_bound_def)
finally show ‹norm (Proj (- ket_invariant (UNIV × J)) *⇩V φ) ≤ ε›
unfolding PJ_def
apply (subst ket_invariant_compl[symmetric])
by simp
qed
definition ‹preserve_query1'_bound NoneI b⇩i b⇩j⇩0 = 3 * sqrt b⇩j⇩0 * sqrt b⇩i / N + 2 * of_bool NoneI * sqrt b⇩j⇩0 / sqrt N›
lemma preserve_query1':
assumes IJ: ‹I ⊆ J›
assumes [simp]: ‹None ∈ J›
assumes b⇩i: ‹card (Some -` I) ≤ b⇩i›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
assumes ε: ‹ε ≥ preserve_query1'_bound (None∈I) b⇩i b⇩j⇩0›
shows ‹preserves_ket query1' (UNIV × I) (UNIV × J) ε›
proof (rule preservesI')
show ‹ε ≥ 0›
using _ ε apply (rule order.trans)
by (simp add: preserve_query1'_bound_def)
fix ψ :: ‹('y × 'y option) ell2›
assume ψ': ‹ψ ∈ space_as_set (ket_invariant (UNIV × I))›
assume ‹norm ψ = 1›
define I' J' where ‹I' = Some -` I› and ‹J' = Some -` J›
from ψ' have ψ: ‹ψ ∈ space_as_set (ket_invariant (UNIV × ((Some ` I' ∪ {None}))))›
using I'_def less_eq_ccsubspace.rep_eq by fastforce
have [simp]: ‹I' ⊆ J'›
using I'_def J'_def IJ by blast
define β where ‹β = Rep_ell2 ψ›
then have β: ‹ψ = (∑yd∈UNIV×(Some ` I' ∪ {None}). β yd *⇩C ket yd)›
using ell2_sum_ket_ket_invariant[OF ψ] by auto
have βbound: ‹(∑yd∈UNIV×(Some ` I' ∪ {None}). (cmod (β yd))⇧2) ≤ 1› (is ‹?lhs ≤ 1›)
apply (subgoal_tac ‹(norm ψ)⇧2 = ?lhs›)
apply (simp add: ‹norm ψ = 1›)
by (simp add: β pythagorean_theorem_sum)
have βNone0: ‹β (y,None) = 0› if ‹None ∉ I› for y
using ψ' that by (simp add: β_def ket_invariant_Rep_ell2)
have [simp]: ‹Some -` insert None X = Some -` X› for X :: ‹'z option set›
by auto
have [simp]: ‹Some -` Some ` X = X› for X :: ‹'z set›
by auto
have [simp]: ‹Some x ∈ J ⟷ x ∈ J'› for x
by (simp add: J'_def)
have [simp]: ‹x ∈ I' ⟹ x ∈ J'› for x
using ‹I' ⊆ J'› by blast
have [simp]: ‹(∑x∈X. if x ∉ Y then f x else 0) = (∑x∈X-Y. f x)› if ‹finite X› for f :: ‹'y ⇒ 'z::ab_group_add› and X Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹(∑x∈X. ∑y∈Y. if x ∉ X' then f x y else 0) = (∑x∈X-X'. ∑y∈Y. f x y)› if ‹finite X›
for f :: ‹'x ⇒ 'y ⇒ 'z::ab_group_add› and X X' Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹β yd *⇩C a *⇩C b = a *⇩C β yd *⇩C b› for yd a and b :: ‹'z::complex_vector›
by auto
have [simp]: ‹cmod α = inverse (sqrt N)› ‹cmod (α⇧2) = inverse N› ‹cmod (α^3) = inverse (N * sqrt N)› ‹cmod (α^4) = inverse (N⇧2)›
by (auto simp: norm_mult numeral_3_eq_3 α_def inverse_eq_divide norm_divide norm_power power_one_over power4_eq_xxxx power2_eq_square)
have [simp]: ‹card (Some ` I') ≤ b⇩i›
by (metis I'_def b⇩i card_image inj_Some)
have bound_J'[simp]: ‹card (Some ` (- J')) ≤ b⇩j⇩0›
using b⇩j⇩0 unfolding J'_def by (simp add: card_image)
define φ and PJ :: ‹('y * 'y option) update› where
‹φ = query1' *⇩V ψ› and ‹PJ = Proj (ket_invariant (UNIV × -J))›
have [simp]: ‹PJ *⇩V ket (x,y) = (if y∈-J then ket (x,y) else 0)› for x y
by (simp add: Proj_ket_invariant_ket PJ_def)
have P0φ: ‹PJ *⇩V φ =
α^4 *⇩C (∑y∈UNIV. ∑d∈I'. ∑y'∈UNIV. ∑d'∈- J'. β (y, Some d) *⇩C ket (y', Some d')) -
α⇧2 *⇩C (∑y∈UNIV. ∑d∈I'. ∑d'∈- J'. β (y, Some d) *⇩C ket (y + d, Some d')) -
α⇧2 *⇩C (∑y∈UNIV. ∑d∈I'. ∑d'∈- J'. β (y, Some d) *⇩C ket (y + d', Some d')) +
α *⇩C (∑y∈UNIV. ∑d'∈- J'. β (y, None) *⇩C ket (y + d', Some d')) -
α^3 *⇩C (∑y∈UNIV. ∑y'∈UNIV. ∑d'∈- J'. β (y, None) *⇩C ket (y', Some d'))›
(is ‹_ = ?t1 - ?t2 - ?t3 + ?t5 - ?t6›)
by (simp add: φ_def β query1' option_sum_split vimage_Compl cblinfun.scaleC_right
cblinfun.add_right cblinfun.diff_right if_distrib Compl_eq_Diff_UNIV
vimage_singleton_inj sum_sum_if_eq sum.distrib scaleC_diff_right scaleC_sum_right
sum_subtractf case_prod_beta sum.cartesian_product' scaleC_add_right add_diff_eq
cblinfun.sum_right
flip: sum.Sigma add.assoc scaleC_scaleC
cong del: option.case_cong if_cong)
have norm_t1: ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket y'd') ≤ sqrt (N * b⇩i)› for y'd' :: ‹'y × 'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
by (auto simp: N_def)
have ‹norm ?t1 = inverse (N⇧2) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). ∑yd∈UNIV × Some ` I'. β yd *⇩C ket y'd')›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap) apply (subst (2) sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N⇧2) * (N * sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def real_sqrt_mult algebra_simps
sqrt_sqrt[THEN extend_mult_rule])
also have ‹… ≤ inverse (N⇧2) * (N * sqrt b⇩j⇩0 * sqrt b⇩i)›
by (metis bound_J' linordered_field_class.inverse_nonnegative_iff_nonnegative mult.commute mult_right_mono of_nat_0_le_iff of_nat_mono real_sqrt_ge_zero real_sqrt_le_iff)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (smt (verit) ab_semigroup_mult_class.mult_ac(1) divide_inverse_commute of_nat_power power2_eq_square real_divide_square_eq)
finally show ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t2: ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {y. δ = fst y + the (snd y) ∧ y ∈ UNIV × Some ` I'} ≤ card I'› for δ
apply (rule card_inj_on_le[where f=‹λy. the (snd y)›])
by (auto intro!: inj_onI)
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd + the (snd yd), d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t2 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd + the (snd yd), d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t3: ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {y. a = fst y ∧ y ∈ UNIV × (I ∩ range Some)} ≤ card I'› for a :: 'y
apply (rule card_inj_on_le[where f=‹λy. the (snd y)›])
by (auto intro!: inj_onI simp: I'_def)
have *: ‹norm (∑yd∈UNIV × Some ` I'. β yd *⇩C ket (fst yd + the d', d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t3 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × Some ` I'.
β yd *⇩C ket (fst yd + the d', d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst (3) sum.swap)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t5: ‹norm ?t5 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
proof (cases ‹None∈I›)
case True
have *: ‹card {y. a = fst y ∧ y ∈ UNIV × {None :: 'y option}} ≤ card {()}› for a :: 'y
apply (rule card_inj_on_le[where f=‹λ_. undefined›])
by (auto intro!: inj_onI)
have *: ‹norm (∑yd∈UNIV × {None}. β yd *⇩C ket (fst yd + the d', d')) ≤ sqrt (1::nat)› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * by auto
have ‹norm ?t5 = inverse (sqrt N) * norm (∑d' ∈ Some ` (-J'). ∑yd∈UNIV × {None}.
β yd *⇩C ket (fst yd + the d', d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (sqrt N) * (sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse (sqrt N) * sqrt b⇩j⇩0›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
using True by (simp add: divide_inverse_commute)
finally show ?thesis
by -
next
case False
then show ?thesis
using βNone0 by auto
qed
have norm_t6: ‹norm ?t6 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
proof (cases ‹None∈I›)
case True
have *: ‹norm (∑yd∈UNIV × {None}. β yd *⇩C ket y'd') ≤ sqrt N› for y'd' :: ‹'y × 'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
by (auto simp: N_def)
have ‹norm ?t6 = inverse (N * sqrt N) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). ∑yd∈UNIV × {None}. β yd *⇩C ket y'd')›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N * sqrt N) * (N * sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def real_sqrt_mult algebra_simps
sqrt_sqrt[THEN extend_mult_rule])
also have ‹… ≤ inverse (N * sqrt N) * (N * sqrt b⇩j⇩0)›
by (simp add: N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
using True by (simp add: divide_inverse_commute less_eq_real_def N_def)
finally show ?thesis
by -
next
case False
then show ?thesis
using βNone0 by auto
qed
have ‹norm (PJ *⇩V φ) ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N + sqrt b⇩j⇩0 * sqrt b⇩i / N + sqrt b⇩j⇩0 * sqrt b⇩i / N
+ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N + of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
unfolding P0φ
apply (rule norm_triangle_le_diff norm_triangle_le, rule add_mono)+
apply (rule norm_t1)
apply (rule norm_t2)
apply (rule norm_t3)
apply (rule norm_t5)
by (rule norm_t6)
also have ‹… ≤ 3 * sqrt b⇩j⇩0 * sqrt b⇩i / N + 2 * of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by (simp add: mult.commute vector_space_over_itself.scale_left_commute)
also have ‹… ≤ ε›
using ε by (auto intro!: simp add: preserve_query1'_bound_def)
finally show ‹norm (Proj (- ket_invariant (UNIV × J)) *⇩V φ) ≤ ε›
unfolding PJ_def
apply (subst ket_invariant_compl[symmetric])
by simp
qed
lemma preserve_query1_simplified:
assumes ‹I ⊆ J›
assumes ‹None ∈ J›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
shows ‹preserves_ket query1 (UNIV × I) (UNIV × J) (6 * sqrt b⇩j⇩0 / sqrt N)›
apply (rule preserve_query1[where b⇩j⇩0=b⇩j⇩0 and b⇩i=N])
using assms by (auto intro!: divide_right_mono simp: preserve_query1_bound_def card_mono N_def)
lemma preserve_query1'_simplified:
assumes ‹I ⊆ J›
assumes ‹None ∈ J›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
shows ‹preserves_ket query1' (UNIV × I) (UNIV × J) (5 * sqrt b⇩j⇩0 / sqrt N)›
apply (rule preserve_query1'[where b⇩j⇩0=b⇩j⇩0 and b⇩i=N])
using assms by (auto intro!: divide_right_mono simp: preserve_query1'_bound_def card_mono N_def)
text ‹The next bound is applicable for ket-invariants assume the output register to have a specific value
\<^term>‹ket y⇩0› (typically \<^term>‹ket 0›) before the query and do not put any conditions on the output register after the query.
Lemmas ‹preserve_query1_fixY› and ‹preserve_query1'_fixY›.›
definition ‹preserve_query1_fixY_bound NoneI NoneJ b⇩i b⇩j⇩0 = sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)
+ 3 * sqrt b⇩j⇩0 * sqrt b⇩i / N + of_bool NoneI * sqrt b⇩j⇩0 / sqrt N + of_bool NoneI * sqrt b⇩j⇩0 / N
+ of_bool NoneJ / sqrt N + of_bool NoneJ * sqrt b⇩i / N + of_bool (NoneI ∧ NoneJ) / sqrt N›
lemma preserve_query1_fixY:
assumes IJ: ‹I ⊆ J›
assumes b⇩i: ‹card (Some -` I) ≤ b⇩i›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
assumes ε: ‹ε ≥ preserve_query1_fixY_bound (None∈I) (None∉J) b⇩i b⇩j⇩0›
shows ‹preserves_ket query1 ({y⇩0} × I) (UNIV × J) ε›
proof (rule preservesI')
show ‹ε ≥ 0›
using _ ε apply (rule order.trans)
by (simp add: preserve_query1_fixY_bound_def)
fix ψ :: ‹('y × 'y option) ell2›
assume ψ: ‹ψ ∈ space_as_set (ket_invariant ({y⇩0} × I))›
assume ‹norm ψ = 1›
define I' J' where ‹I' = Some -` I› and ‹J' = Some -` J›
then have ‹{y⇩0} × I ⊆ {y⇩0} × (Some ` I' ∪ {None})›
apply (rule_tac Sigma_mono)
by auto
with ψ have ψ': ‹ψ ∈ space_as_set (ket_invariant ({y⇩0} × ((Some ` I' ∪ {None}))))›
using less_eq_ccsubspace.rep_eq ket_invariant_le by fastforce
have [simp]: ‹I' ⊆ J'›
using I'_def J'_def IJ by blast
define β where ‹β d = Rep_ell2 ψ (y⇩0,d)› for d
then have β: ‹ψ = (∑d∈Some ` I' ∪ {None}. β d *⇩C ket (y⇩0,d))›
using ell2_sum_ket_ket_invariant[OF ψ']
by (auto simp: sum.cartesian_product')
have βbound: ‹(∑d∈(Some ` I' ∪ {None}). (cmod (β d))⇧2) ≤ 1› (is ‹?lhs ≤ 1›)
apply (subgoal_tac ‹(norm ψ)⇧2 = ?lhs›)
apply (simp add: ‹norm ψ = 1›)
by (simp add: β pythagorean_theorem_sum del: sum.insert)
have βNone: ‹cmod (β None) ≤ 1›
proof -
have ‹(cmod (β None))⇧2 = (∑d∈{None}. (cmod (β d))⇧2)›
by simp
also have ‹… ≤ (∑d∈(Some ` I' ∪ {None}). (cmod (β d))⇧2)›
apply (rule sum_mono2) by auto
also have ‹… ≤ 1›
by (rule βbound)
finally show ?thesis
by (simp add: power_le_one_iff)
qed
have βNone0: ‹β None = 0› if ‹None ∉ I›
using ψ that by (simp add: β_def ket_invariant_Rep_ell2)
have [simp]: ‹Some -` insert None X = Some -` X› for X :: ‹'z option set›
by auto
have [simp]: ‹Some -` Some ` X = X› for X :: ‹'z set›
by auto
have [simp]: ‹Some x ∈ J ⟷ x ∈ J'› for x
by (simp add: J'_def)
have [simp]: ‹x ∈ I' ⟹ x ∈ J'› for x
using ‹I' ⊆ J'› by blast
have [simp]: ‹(∑x∈X. if x ∉ Y then f x else 0) = (∑x∈X-Y. f x)› if ‹finite X› for f :: ‹'y ⇒ 'z::ab_group_add› and X Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹β yd *⇩C a *⇩C b = a *⇩C β yd *⇩C b› for yd a and b :: ‹'z::complex_vector›
by auto
have [simp]: ‹cmod α = inverse (sqrt N)› ‹cmod (α⇧2) = inverse N› ‹cmod (α^3) = inverse (N * sqrt N)› ‹cmod (α^4) = inverse (N⇧2)›
by (auto simp: norm_mult numeral_3_eq_3 α_def inverse_eq_divide norm_divide norm_power power_one_over power4_eq_xxxx power2_eq_square)
have [simp]: ‹card (Some ` I') ≤ b⇩i›
by (metis I'_def b⇩i card_image inj_Some)
have bound_J'[simp]: ‹card (Some ` (- J')) ≤ b⇩j⇩0›
using b⇩j⇩0 unfolding J'_def by (simp add: card_image)
define φ and PJ :: ‹('y * 'y option) update› where
‹φ = query1 *⇩V ψ› and ‹PJ = Proj (ket_invariant (UNIV × -J))›
have [simp]: ‹PJ *⇩V ket (x,y) = (if y∈-J then ket (x,y) else 0)› for x y
by (simp add: Proj_ket_invariant_ket PJ_def)
have P0φ: ‹PJ *⇩V φ =
α^4 *⇩C (∑d∈I'. ∑y'∈UNIV. ∑d'∈- J'. β (Some d) *⇩C ket (y', Some d'))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈- J'. β (Some d) *⇩C ket (y⇩0 + d, Some d'))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈- J'. β (Some d) *⇩C ket (y⇩0 + d', Some d'))
+ α⇧2 *⇩C (∑d∈I'. ∑d'∈- J'. β (Some d) *⇩C ket (y⇩0, Some d'))
+ α *⇩C (∑d'∈- J'. β (None) *⇩C ket (y⇩0 + d', Some d'))
- α^3 *⇩C (∑y'∈UNIV. ∑d'∈- J'. β (None) *⇩C ket (y', Some d'))
+ (of_bool (None ∉ J) * α) *⇩C (∑d∈I'. β (Some d) *⇩C ket (y⇩0 + d, None))
- (of_bool (None ∉ J) * α^3) *⇩C (∑d∈I'. ∑y'∈UNIV. β (Some d) *⇩C ket (y', None))
+ (of_bool (None ∉ J) * α⇧2) *⇩C (∑y'∈UNIV. β None *⇩C ket (y', None))
›
(is ‹_ = ?t1 - ?t2 - ?t3 + ?t4 + ?t5 - ?t6 + ?t7 - ?t8 + ?t9›)
by (simp add: φ_def β query1 option_sum_split vimage_Compl
cblinfun.add_right cblinfun.diff_right if_distrib Compl_eq_Diff_UNIV
vimage_singleton_inj sum_sum_if_eq sum.distrib scaleC_diff_right scaleC_sum_right
sum_subtractf case_prod_beta sum.cartesian_product' scaleC_add_right add_diff_eq
cblinfun.scaleC_right cblinfun.sum_right
flip: sum.Sigma add.assoc scaleC_scaleC
cong del: option.case_cong if_cong)
have norm_t1: ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)›
proof -
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket y'd') ≤ sqrt b⇩i› for y'd' :: ‹'y × 'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
have ‹norm ?t1 = inverse (N⇧2) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). ∑d∈Some ` I'. β d *⇩C ket y'd')›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst (3) sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N⇧2) * (sqrt N * sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def real_sqrt_mult)
also have ‹… ≤ inverse (N⇧2) * (sqrt N * sqrt b⇩j⇩0 * sqrt b⇩i)›
by (metis bound_J' linordered_field_class.inverse_nonnegative_iff_nonnegative mult.commute mult_right_mono of_nat_0_le_iff of_nat_mono real_sqrt_ge_zero real_sqrt_le_iff)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)›
by (smt (verit, del_insts) divide_divide_eq_left divide_inverse mult.commute of_nat_0_le_iff of_nat_power power2_eq_square real_divide_square_eq real_sqrt_pow2 times_divide_eq_left)
finally show ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)›
by -
qed
have norm_t2: ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {d. δ = the d ∧ d ∈ Some ` I'} ≤ card I'› for δ
apply (rule card_inj_on_le[where f=the])
by (auto intro!: inj_onI)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t2 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t3: ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have aux: ‹I' = Some -` I ⟹ card (Some -` I) ≤ b⇩i ⟹ Some x ∈ I ⟹ card {y ∈ I. y ∈ range Some} ≤ b⇩i› for x
by (smt (verit, ccfv_SIG) Collect_cong Int_iff card_image image_vimage_eq inf_set_def inj_Some mem_Collect_eq)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d', d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using I'_def b⇩i aux by auto
have ‹norm ?t3 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑d∈Some ` I'.
β d *⇩C ket (y⇩0 + the d', d'))›
apply (simp add: sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t4: ‹norm ?t4 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have aux: ‹I' = Some -` I ⟹
card (Some -` I) ≤ b⇩i ⟹ Some x ∈ I ⟹ card {y ∈ I. y ∈ range Some} ≤ b⇩i› for x
by (smt (verit) Collect_cong Int_iff card_image image_vimage_eq inf_set_def inj_Some mem_Collect_eq)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0, d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using I'_def b⇩i aux by auto
have ‹norm ?t4 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑d∈Some ` I'.
β d *⇩C ket (y⇩0, d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t4 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t5: ‹norm ?t5 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
proof (cases ‹None∈I›)
case True
have *: ‹norm (β None *⇩C ket (y⇩0 + the d', d')) ≤ sqrt (1::nat)› for d' :: ‹'y option›
using βNone by simp
have ‹norm ?t5 = inverse (sqrt N) * norm (∑d' ∈ Some ` (-J').
β None *⇩C ket (y⇩0 + the d', d'))›
by (simp add: sum.cartesian_product' sum.reindex)
also have ‹… ≤ inverse (sqrt N) * (sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse (sqrt N) * sqrt b⇩j⇩0›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by (simp add: divide_inverse_commute True)
finally show ‹norm ?t5 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by -
next
case False
then show ?thesis by (simp add: βNone0)
qed
have norm_t6: ‹norm ?t6 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / N›
proof (cases ‹None∈I›)
case True
have *: ‹norm (β None *⇩C ket y'd') ≤ 1› for y'd' :: ‹'y × 'y option›
using βNone by simp
have ‹norm ?t6 = inverse (N * sqrt N) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). β None *⇩C ket y'd')›
by (simp add: sum.cartesian_product' sum.reindex)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt N * sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def real_sqrt_mult)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt N * sqrt b⇩j⇩0)›
by (simp add: N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / N›
by (simp add: divide_inverse_commute less_eq_real_def True N_def)
finally show ‹norm ?t6 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / N›
by -
next
case False
then show ?thesis by (simp add: βNone0)
qed
have norm_t7: ‹norm ?t7 ≤ of_bool (None∉J) / sqrt N›
proof (cases ‹None∈J›)
assume ‹None ∉ J›
have ‹norm ?t7 = inverse (sqrt N) * norm (∑d∈I'. β (Some d) *⇩C ket (y⇩0 + d, None :: 'y option))›
using ‹None ∉ J› by simp
also have ‹… = inverse (sqrt N) * norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, None :: 'y option))›
apply (subst sum.reindex)
by auto
also have ‹… ≤ inverse (sqrt N) * (sqrt (real 1))›
proof -
have aux: ‹x ∈ I' ⟹ card {y. x = the y ∧ y ∈ Some ` I'} ≤ Suc 0› for x
by (smt (verit, del_insts) card_eq_Suc_0_ex1 dual_order.refl imageE imageI mem_Collect_eq option.sel)
show ?thesis
apply (rule mult_left_mono)
using _ _ βbound apply (rule bound_coeff_sum2)
using aux by auto
qed
also have ‹… = of_bool (None∉J) / sqrt N›
using ‹None ∉ J› inverse_eq_divide by auto
finally show ?thesis
by -
qed simp
have norm_t8: ‹norm ?t8 ≤ of_bool (None∉J) * sqrt b⇩i / N›
proof (cases ‹None∈J›)
assume ‹None ∉ J›
have aux: ‹I' = Some -` I ⟹
card (Some -` I) ≤ b⇩i ⟹ Some x ∈ I ⟹ card {y ∈ I. y ∈ range Some} ≤ b⇩i› for x
by (smt (verit, ccfv_SIG) Collect_cong Int_iff card_image image_vimage_eq inf_set_def inj_Some mem_Collect_eq)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y', None :: 'y option)) ≤ sqrt (real b⇩i)› for y' :: 'y
using _ _ βbound apply (rule bound_coeff_sum2)
using I'_def b⇩i aux by auto
have ‹norm ?t8 = inverse (N * sqrt N) * norm (∑y'::'y∈UNIV. ∑d∈Some ` I'. β d *⇩C ket (y', None :: 'y option))›
apply (simp add: sum.reindex ‹None ∉ J› N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt N * sqrt (real b⇩i))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def)
also have ‹… = of_bool (None∉J) * sqrt b⇩i / N›
using ‹None ∉ J› inverse_eq_divide
by (simp add: divide_inverse_commute N_def)
finally show ?thesis
by -
qed simp
have norm_t9: ‹norm ?t9 ≤ of_bool (None∈I ∧ None∉J) / sqrt N›
proof (cases ‹None∈I ∧ None∉J›)
case True
have ‹norm ?t9 = inverse N * norm (∑y'::'y∈UNIV. β None *⇩C ket (y', None :: 'y option))›
by (simp add: sum.reindex True)
also have ‹… ≤ inverse N * (sqrt N * sqrt 1)›
apply (rule mult_left_mono)
apply (rule norm_ortho_sum_bound[where b'=1])
using βNone by (auto simp: N_def)
also have ‹… = of_bool (None∈I ∧ None∉J) / sqrt N›
using True apply simp
by (metis divide_inverse_commute inverse_eq_divide of_nat_0_le_iff sqrt_divide_self_eq)
finally show ?thesis
by -
next
case False with βNone0
show ?thesis by auto
qed
have ‹norm (PJ *⇩V φ) ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N) + sqrt b⇩j⇩0 * sqrt b⇩i / N + sqrt b⇩j⇩0 * sqrt b⇩i / N
+ sqrt b⇩j⇩0 * sqrt b⇩i / N + of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N + of_bool (None∈I) * sqrt b⇩j⇩0 / N
+ of_bool (None∉J) / sqrt N + of_bool (None∉J) * sqrt b⇩i / N + of_bool (None∈I ∧ None∉J) / sqrt N›
unfolding P0φ
apply (rule norm_triangle_le_diff norm_triangle_le, rule add_mono)+
apply (rule norm_t1)
apply (rule norm_t2)
apply (rule norm_t3)
apply (rule norm_t4)
apply (rule norm_t5)
apply (rule norm_t6)
apply (rule norm_t7)
apply (rule norm_t8)
apply (rule norm_t9)
by -
also have ‹… ≤ preserve_query1_fixY_bound (None∈I) (None∉J) b⇩i b⇩j⇩0›
by (auto simp: preserve_query1_fixY_bound_def mult.commute mult.left_commute)
also have ‹… ≤ ε›
by (simp add: ε)
finally show ‹norm (Proj (- ket_invariant (UNIV × J)) *⇩V φ) ≤ ε›
unfolding PJ_def
apply (subst ket_invariant_compl[symmetric])
by simp
qed
definition ‹preserve_query1'_fixY_bound NoneI NoneJ b⇩i b⇩j⇩0 = sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)
+ 2 * sqrt b⇩j⇩0 * sqrt b⇩i / N + of_bool NoneI * sqrt b⇩j⇩0 / sqrt N + of_bool NoneI * sqrt b⇩j⇩0 / N
+ of_bool NoneJ / sqrt N + of_bool NoneJ * sqrt b⇩i / N + of_bool (NoneI ∧ NoneJ) / sqrt N›
lemma preserve_query1'_fixY:
assumes IJ: ‹I ⊆ J›
assumes b⇩i: ‹card (Some -` I) ≤ b⇩i›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
assumes ε: ‹ε ≥ preserve_query1'_fixY_bound (None∈I) (None∉J) b⇩i b⇩j⇩0›
shows ‹preserves_ket query1' ({y⇩0} × I) (UNIV × J) ε›
proof (rule preservesI')
show ‹ε ≥ 0›
using _ ε apply (rule order.trans)
by (simp add: preserve_query1'_fixY_bound_def)
fix ψ :: ‹('y × 'y option) ell2›
assume ψ: ‹ψ ∈ space_as_set (ket_invariant ({y⇩0} × I))›
assume ‹norm ψ = 1›
define I' J' where ‹I' = Some -` I› and ‹J' = Some -` J›
then have ‹{y⇩0} × I ⊆ {y⇩0} × (Some ` I' ∪ {None})›
apply (rule_tac Sigma_mono)
by auto
with ψ have ψ': ‹ψ ∈ space_as_set (ket_invariant ({y⇩0} × ((Some ` I' ∪ {None}))))›
using less_eq_ccsubspace.rep_eq ket_invariant_le by fastforce
have [simp]: ‹I' ⊆ J'›
using I'_def J'_def IJ by blast
define β where ‹β d = Rep_ell2 ψ (y⇩0,d)› for d
then have β: ‹ψ = (∑d∈Some ` I' ∪ {None}. β d *⇩C ket (y⇩0,d))›
using ell2_sum_ket_ket_invariant[OF ψ']
by (auto simp: sum.cartesian_product')
have βbound: ‹(∑d∈(Some ` I' ∪ {None}). (cmod (β d))⇧2) ≤ 1› (is ‹?lhs ≤ 1›)
apply (subgoal_tac ‹(norm ψ)⇧2 = ?lhs›)
apply (simp add: ‹norm ψ = 1›)
by (simp add: β pythagorean_theorem_sum del: sum.insert)
have βNone: ‹cmod (β None) ≤ 1›
proof -
have ‹(cmod (β None))⇧2 = (∑d∈{None}. (cmod (β d))⇧2)›
by simp
also have ‹… ≤ (∑d∈(Some ` I' ∪ {None}). (cmod (β d))⇧2)›
apply (rule sum_mono2) by auto
also have ‹… ≤ 1›
by (rule βbound)
finally show ?thesis
by (simp add: power_le_one_iff)
qed
have βNone0: ‹β None = 0› if ‹None ∉ I›
using ψ that by (simp add: β_def ket_invariant_Rep_ell2)
have [simp]: ‹Some -` insert None X = Some -` X› for X :: ‹'z option set›
by auto
have [simp]: ‹Some -` Some ` X = X› for X :: ‹'z set›
by auto
have [simp]: ‹Some x ∈ J ⟷ x ∈ J'› for x
by (simp add: J'_def)
have [simp]: ‹x ∈ I' ⟹ x ∈ J'› for x
using ‹I' ⊆ J'› by blast
have [simp]: ‹(∑x∈X. if x ∉ Y then f x else 0) = (∑x∈X-Y. f x)› if ‹finite X› for f :: ‹'y ⇒ 'z::ab_group_add› and X Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹β yd *⇩C a *⇩C b = a *⇩C β yd *⇩C b› for yd a and b :: ‹'z::complex_vector›
by auto
have [simp]: ‹cmod α = inverse (sqrt N)› ‹cmod (α⇧2) = inverse N› ‹cmod (α^3) = inverse (N * sqrt N)› ‹cmod (α^4) = inverse (N⇧2)›
by (auto simp: norm_mult numeral_3_eq_3 α_def inverse_eq_divide norm_divide norm_power power_one_over power2_eq_square power4_eq_xxxx)
have [simp]: ‹card (Some ` I') ≤ b⇩i›
by (metis I'_def b⇩i card_image inj_Some)
have bound_J'[simp]: ‹card (Some ` (- J')) ≤ b⇩j⇩0›
using b⇩j⇩0 unfolding J'_def by (simp add: card_image)
define φ and PJ :: ‹('y * 'y option) update› where
‹φ = query1' *⇩V ψ› and ‹PJ = Proj (ket_invariant (UNIV × -J))›
have [simp]: ‹PJ *⇩V ket (x,y) = (if y∈-J then ket (x,y) else 0)› for x y
by (simp add: Proj_ket_invariant_ket PJ_def)
have P0φ: ‹PJ *⇩V φ =
α^4 *⇩C (∑d∈I'. ∑y'∈UNIV. ∑d'∈- J'. β (Some d) *⇩C ket (y', Some d'))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈- J'. β (Some d) *⇩C ket (y⇩0 + d, Some d'))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈- J'. β (Some d) *⇩C ket (y⇩0 + d', Some d'))
+ α *⇩C (∑d'∈- J'. β (None) *⇩C ket (y⇩0 + d', Some d'))
- α^3 *⇩C (∑y'∈UNIV. ∑d'∈- J'. β (None) *⇩C ket (y', Some d'))
+ (of_bool (None ∉ J) * α) *⇩C (∑d∈I'. β (Some d) *⇩C ket (y⇩0 + d, None))
- (of_bool (None ∉ J) * α^3) *⇩C (∑d∈I'. ∑y'∈UNIV. β (Some d) *⇩C ket (y', None))
+ (of_bool (None ∉ J) * α⇧2) *⇩C (∑y'∈UNIV. β None *⇩C ket (y', None))
›
(is ‹_ = ?t1 - ?t2 - ?t3 + ?t5 - ?t6 + ?t7 - ?t8 + ?t9›)
by (simp add: φ_def β query1' option_sum_split vimage_Compl
cblinfun.add_right cblinfun.diff_right if_distrib Compl_eq_Diff_UNIV
vimage_singleton_inj sum_sum_if_eq sum.distrib scaleC_diff_right scaleC_sum_right
sum_subtractf case_prod_beta sum.cartesian_product' scaleC_add_right add_diff_eq
cblinfun.scaleC_right cblinfun.sum_right
flip: sum.Sigma add.assoc scaleC_scaleC
cong del: option.case_cong if_cong)
have norm_t1: ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)›
proof -
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket y'd') ≤ sqrt b⇩i› for y'd' :: ‹'y × 'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
have ‹norm ?t1 = inverse (N⇧2) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). ∑d∈Some ` I'. β d *⇩C ket y'd')›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst (3) sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N⇧2) * (sqrt N * sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def real_sqrt_mult)
also have ‹… ≤ inverse (N⇧2) * (sqrt N * sqrt b⇩j⇩0 * sqrt b⇩i)›
by (metis bound_J' linordered_field_class.inverse_nonnegative_iff_nonnegative mult.commute mult_right_mono of_nat_0_le_iff of_nat_mono real_sqrt_ge_zero real_sqrt_le_iff)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)›
by (smt (verit, del_insts) divide_divide_eq_left divide_inverse mult.commute of_nat_0_le_iff of_nat_power power2_eq_square real_divide_square_eq real_sqrt_pow2 times_divide_eq_left)
finally show ‹norm ?t1 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N)›
by -
qed
have norm_t2: ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have *: ‹card {d. δ = the d ∧ d ∈ Some ` I'} ≤ card I'› for δ
apply (rule card_inj_on_le[where f=the])
by (auto intro!: inj_onI)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using * I'_def b⇩i order.trans by auto
have ‹norm ?t2 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, d'))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t2 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t3: ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
proof -
have aux: ‹I' = Some -` I ⟹ card (Some -` I) ≤ b⇩i ⟹ card {y ∈ I. y ∈ range Some} ≤ b⇩i›
by (smt (verit, ccfv_SIG) Collect_cong Int_iff card_image image_vimage_eq inf_set_def inj_Some mem_Collect_eq)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d', d')) ≤ sqrt b⇩i› for d' :: ‹'y option›
using _ _ βbound apply (rule bound_coeff_sum2)
using I'_def b⇩i aux by auto
have ‹norm ?t3 = inverse (real N) * norm (∑d' ∈ Some ` (-J'). ∑d∈Some ` I'.
β d *⇩C ket (y⇩0 + the d', d'))›
apply (simp add: sum.reindex N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (real N) * (sqrt (card (Some ` (- J'))) * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by (simp add: divide_inverse_commute)
finally show ‹norm ?t3 ≤ sqrt b⇩j⇩0 * sqrt b⇩i / N›
by -
qed
have norm_t5: ‹norm ?t5 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
proof (cases ‹None∈I›)
case True
have *: ‹norm (β None *⇩C ket (y⇩0 + the d', d')) ≤ sqrt (1::nat)› for d' :: ‹'y option›
using βNone by simp
have ‹norm ?t5 = inverse (sqrt N) * norm (∑d' ∈ Some ` (-J').
β None *⇩C ket (y⇩0 + the d', d'))›
by (simp add: sum.cartesian_product' sum.reindex)
also have ‹… ≤ inverse (sqrt N) * (sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… ≤ inverse (sqrt N) * sqrt b⇩j⇩0›
by (simp add: mult_right_mono N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by (simp add: divide_inverse_commute True)
finally show ‹norm ?t5 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N›
by -
next
case False
then show ?thesis by (simp add: βNone0)
qed
have norm_t6: ‹norm ?t6 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / N›
proof (cases ‹None∈I›)
case True
have *: ‹norm (β None *⇩C ket y'd') ≤ 1› for y'd' :: ‹'y × 'y option›
using βNone by simp
have ‹norm ?t6 = inverse (N * sqrt N) * norm (∑y'd' ∈ (UNIV::'y set) × Some ` (-J'). β None *⇩C ket y'd')›
by (simp add: sum.cartesian_product' sum.reindex)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt N * sqrt (card (Some ` (- J'))))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left real_sqrt_mult N_def)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt N * sqrt b⇩j⇩0)›
by (simp add: N_def)
also have ‹… ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / N›
by (simp add: divide_inverse_commute less_eq_real_def True N_def)
finally show ‹norm ?t6 ≤ of_bool (None∈I) * sqrt b⇩j⇩0 / N›
by -
next
case False
then show ?thesis by (simp add: βNone0)
qed
have norm_t7: ‹norm ?t7 ≤ of_bool (None∉J) / sqrt N›
proof (cases ‹None∈J›)
assume ‹None ∉ J›
have ‹norm ?t7 = inverse (sqrt N) * norm (∑d∈I'. β (Some d) *⇩C ket (y⇩0 + d, None :: 'y option))›
using ‹None ∉ J› by simp
also have ‹… = inverse (sqrt N) * norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, None :: 'y option))›
apply (subst sum.reindex)
by auto
also have ‹… ≤ inverse (sqrt N) * (sqrt (real 1))›
proof -
have aux: ‹x ∈ I' ⟹ card {y. x = the y ∧ y ∈ Some ` I'} ≤ Suc 0› for x
by (smt (verit, del_insts) card_eq_Suc_0_ex1 dual_order.refl imageE imageI mem_Collect_eq option.sel)
show ?thesis
apply (rule mult_left_mono)
using _ _ βbound apply (rule bound_coeff_sum2)
using aux by auto
qed
also have ‹… = of_bool (None∉J) / sqrt N›
using ‹None ∉ J› inverse_eq_divide by auto
finally show ?thesis
by -
qed simp
have norm_t8: ‹norm ?t8 ≤ of_bool (None∉J) * sqrt b⇩i / N›
proof (cases ‹None∈J›)
assume ‹None ∉ J›
have aux: ‹card (Some -` I) ≤ b⇩i ⟹ card {y ∈ I. y ∈ range Some} ≤ b⇩i›
by (smt (verit, ccfv_SIG) Collect_cong Int_iff card_image image_vimage_eq inf_set_def inj_Some mem_Collect_eq)
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y', None :: 'y option)) ≤ sqrt (real b⇩i)› for y' :: 'y
using _ _ βbound apply (rule bound_coeff_sum2)
using I'_def b⇩i aux by auto
have ‹norm ?t8 = inverse (N * sqrt N) * norm (∑y'::'y∈UNIV. ∑d∈Some ` I'. β d *⇩C ket (y', None :: 'y option))›
apply (simp add: sum.reindex ‹None ∉ J› N_def)
apply (subst sum.swap) apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt N * sqrt (real b⇩i))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def)
also have ‹… = of_bool (None∉J) * sqrt b⇩i / N›
using ‹None ∉ J› inverse_eq_divide
by (simp add: divide_inverse_commute N_def)
finally show ?thesis
by -
qed simp
have norm_t9: ‹norm ?t9 ≤ of_bool (None∈I ∧ None∉J) / sqrt N›
proof (cases ‹None∈I ∧ None∉J›)
case True
have ‹norm ?t9 = inverse N * norm (∑y'::'y∈UNIV. β None *⇩C ket (y', None :: 'y option))›
by (simp add: sum.reindex True)
also have ‹… ≤ inverse N * (sqrt N * sqrt 1)›
apply (rule mult_left_mono)
apply (rule norm_ortho_sum_bound[where b'=1])
using βNone by (auto simp: N_def)
also have ‹… = of_bool (None∈I ∧ None∉J) / sqrt N›
using True apply simp
by (metis divide_inverse_commute inverse_eq_divide of_nat_0_le_iff sqrt_divide_self_eq)
finally show ?thesis
by -
next
case False with βNone0
show ?thesis by auto
qed
have ‹norm (PJ *⇩V φ) ≤ sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N) + sqrt b⇩j⇩0 * sqrt b⇩i / N + sqrt b⇩j⇩0 * sqrt b⇩i / N
+ of_bool (None∈I) * sqrt b⇩j⇩0 / sqrt N + of_bool (None∈I) * sqrt b⇩j⇩0 / N
+ of_bool (None∉J) / sqrt N + of_bool (None∉J) * sqrt b⇩i / N + of_bool (None∈I ∧ None∉J) / sqrt N›
unfolding P0φ
apply (rule norm_triangle_le_diff norm_triangle_le, rule add_mono)+
apply (rule norm_t1)
apply (rule norm_t2)
apply (rule norm_t3)
apply (rule norm_t5)
apply (rule norm_t6)
apply (rule norm_t7)
apply (rule norm_t8)
apply (rule norm_t9)
by -
also have ‹… ≤ preserve_query1'_fixY_bound (None∈I) (None∉J) b⇩i b⇩j⇩0›
by (auto simp: preserve_query1'_fixY_bound_def mult.commute mult.left_commute)
also have ‹… ≤ ε›
by (simp add: ε)
finally show ‹norm (Proj (- ket_invariant (UNIV × J)) *⇩V φ) ≤ ε›
unfolding PJ_def
apply (subst ket_invariant_compl[symmetric])
by simp
qed
text ‹The next bound is applicable for ket-invariants assume the output register to have a specific value
\<^term>‹ket y⇩0› (typically \<^term>‹ket 0›) before the query and require that after the query,
the oracle register is not \<^const>‹None› and the output register has the correct value given that
oracle register content.
Notice that this invariant is only available for \<^const>‹query1'›, not for \<^const>‹query1›!›
definition ‹preserve_query1'_fixY_bound_output b⇩i = 4 / sqrt N + 2 * sqrt b⇩i / N›
lemma preserve_query1'_fixY_output:
assumes b⇩i: ‹card (Some -` I) ≤ b⇩i›
assumes ε: ‹ε ≥ preserve_query1'_fixY_bound_output b⇩i›
shows ‹preserves_ket query1' ({y⇩0} × I) {(y⇩0+d, Some d)| d. True} ε›
proof (rule preservesI')
show ‹ε ≥ 0›
using _ ε apply (rule order.trans)
by (simp add: preserve_query1'_fixY_bound_output_def)
fix ψ :: ‹('y × 'y option) ell2›
assume ψ: ‹ψ ∈ space_as_set (ket_invariant ({y⇩0} × I))›
assume ‹norm ψ = 1›
define I' where ‹I' = Some -` I›
then have ‹{y⇩0} × I ⊆ {y⇩0} × (Some ` I' ∪ {None})›
apply (rule_tac Sigma_mono)
by auto
with ψ have ψ': ‹ψ ∈ space_as_set (ket_invariant ({y⇩0} × ((Some ` I' ∪ {None}))))›
using less_eq_ccsubspace.rep_eq ket_invariant_le by fastforce
define β where ‹β d = Rep_ell2 ψ (y⇩0,d)› for d
then have β: ‹ψ = (∑d∈Some ` I' ∪ {None}. β d *⇩C ket (y⇩0,d))›
using ell2_sum_ket_ket_invariant[OF ψ']
by (auto simp: sum.cartesian_product')
have βbound: ‹(∑d∈(Some ` I' ∪ {None}). (cmod (β d))⇧2) ≤ 1› (is ‹?lhs ≤ 1›)
apply (subgoal_tac ‹(norm ψ)⇧2 = ?lhs›)
apply (simp add: ‹norm ψ = 1›)
by (simp add: β pythagorean_theorem_sum del: sum.insert)
have βbound1[simp]: ‹cmod (β x) ≤ 1› for x
using norm_point_bound_ell2[of ψ] ‹norm ψ = 1› unfolding β_def by auto
have [simp]: ‹Some -` insert None X = Some -` X› for X :: ‹'z option set›
by auto
have [simp]: ‹Some -` Some ` X = X› for X :: ‹'z set›
by auto
have [simp]: ‹β yd *⇩C a *⇩C b = a *⇩C β yd *⇩C b› for yd a and b :: ‹'z::complex_vector›
by auto
have [simp]: ‹cmod α = inverse (sqrt N)› ‹cmod (α⇧2) = inverse N› ‹cmod (α^3) = inverse (N * sqrt N)› ‹cmod (α^4) = inverse (N⇧2)›
by (auto simp: norm_mult numeral_3_eq_3 α_def inverse_eq_divide norm_divide norm_power power_one_over power4_eq_xxxx power2_eq_square)
have [simp]: ‹card (Some ` I') ≤ b⇩i›
by (metis I'_def b⇩i card_image inj_Some)
define φ and PJ :: ‹('y * 'y option) update› where
‹φ = query1' *⇩V ψ› and ‹PJ = Proj (ket_invariant (- {(y⇩0+d, Some d)| d. True}))›
have aux: ‹∀d. y ≠ y⇩0 + d ⟹ d ≠ Some (y⇩0 + y)› for d y
by (metis add.right_neutral y_cancel ordered_field_class.sign_simps(1))
then have [simp]: ‹PJ *⇩V ket (y,d) = (if Some (y⇩0 + y) = d then 0 else ket (y,d))› for y d
by (auto simp add: Proj_ket_invariant_ket PJ_def)
have P0φ: ‹PJ *⇩V φ =
α *⇩C (∑d∈I'. β (Some d) *⇩C ket (y⇩0 + d, None))
- α^3 *⇩C (∑d∈I'. ∑y∈UNIV. β (Some d) *⇩C ket (y, None))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈UNIV. if d=d' then 0 else β (Some d) *⇩C ket (y⇩0 + d, Some d'))
+ α^4 *⇩C (∑d∈I'. ∑y∈UNIV. ∑d'∈UNIV. if y⇩0+y=d' then 0 else β (Some d) *⇩C ket (y, Some d'))
- α^3 *⇩C (∑y∈UNIV. ∑d'∈UNIV. if y⇩0+y=d' then 0 else β None *⇩C ket (y, Some d'))
+ α⇧2 *⇩C (∑y∈UNIV. β None *⇩C ket (y, None))›
(is ‹_ = ?t1 - ?t2 - ?t3 + ?t4 - ?t5 + ?t6›)
by (simp add: φ_def β query1' option_sum_split vimage_Compl of_bool_def cblinfun.sum_right
cblinfun.add_right cblinfun.diff_right if_distrib Compl_eq_Diff_UNIV cblinfun.scaleC_right
vimage_singleton_inj sum_sum_if_eq sum.distrib scaleC_diff_right scaleC_sum_right
sum_subtractf case_prod_beta sum.cartesian_product' scaleC_add_right add_diff_eq
flip: sum.Sigma add.assoc scaleC_scaleC
cong del: option.case_cong if_cong)
have norm_t1: ‹norm ?t1 ≤ 1 / sqrt N›
proof -
have ‹norm ?t1 = inverse (sqrt N) * norm (∑d∈Some ` I'. β d *⇩C ket (y⇩0 + the d, None :: 'y option))›
by (simp add: sum.reindex)
also have ‹… ≤ inverse (sqrt N) * sqrt (1::nat)›
proof -
have aux: ‹x ∈ I' ⟹ card {y. x = the y ∧ y ∈ Some ` I'} ≤ Suc 0› for x
by (smt (verit, del_insts) card_eq_Suc_0_ex1 imageE imageI le_refl mem_Collect_eq option.sel)
show ?thesis
apply (rule mult_left_mono)
using _ _ βbound apply (rule bound_coeff_sum2)
using aux by auto
qed
also have ‹… = 1 / sqrt N›
apply simp
using inverse_eq_divide by blast
finally show ‹norm ?t1 ≤ 1 / sqrt N›
by -
qed
have norm_t2: ‹norm ?t2 ≤ sqrt b⇩i / N›
proof -
have *: ‹norm (∑d∈Some ` I'. β d *⇩C ket (y, None :: 'y option)) ≤ sqrt b⇩i› for y :: 'y
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
have ‹norm ?t2 = inverse (N * sqrt N) * norm (∑y∈UNIV. ∑d∈Some ` I'. β d *⇩C ket (y :: 'y, None :: 'y option))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt (real N) * sqrt (real b⇩i))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def)
also have ‹… = sqrt b⇩i / N›
by (simp add: divide_inverse_commute N_def)
finally show ?thesis
by auto
qed
have norm_t3: ‹norm ?t3 ≤ 1 / sqrt N›
proof -
have aux: ‹card {y. x = the y ∧ y ∈ Some ` (I' - {d'})} ≤ Suc 0› for x d'
by (smt (verit, best) Collect_empty_eq bot_nat_0.not_eq_extremum card.empty card_eq_Suc_0_ex1 imageE le_simps(3) mem_Collect_eq nat_le_linear option.sel)
have *: ‹norm (∑d∈Some ` (I' - {d'}). β d *⇩C ket (y⇩0 + the d, Some d')) ≤ sqrt (1::nat)› for d'
using _ _ βbound apply (rule bound_coeff_sum2)
using aux[of _ d'] by auto
have ‹norm ?t3 = inverse N * norm (∑d'∈UNIV. ∑d∈Some ` (I'-{d'}). β d *⇩C ket (y⇩0 + the d, Some d'))›
apply (simp add: sum.cartesian_product' sum.reindex)
apply (subst sum.swap)
apply (simp add: sum_if_eq_else)
by -
also have ‹… ≤ inverse N * sqrt N›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def)
also have ‹… = 1 / sqrt N›
by (simp add: inverse_eq_divide sqrt_divide_self_eq)
finally show ?thesis
by -
qed
have norm_t4: ‹norm ?t4 ≤ sqrt (real b⇩i) / N›
proof -
have *: ‹norm (∑d∈Some ` I'. if y⇩0 + fst yd' = snd yd' then 0 else β d *⇩C ket (fst yd', Some (snd yd'))) ≤ sqrt b⇩i› for yd'
apply (cases ‹y⇩0 + fst yd' = snd yd'›)
apply simp
apply simp
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
note if_cong[cong del]
have ‹norm ?t4 = inverse (N⇧2) * norm (∑yd'∈UNIV. ∑d∈Some ` I'. if y⇩0 + fst yd' = snd yd' then 0 else β d *⇩C ket (fst yd', Some (snd yd')))›
apply (simp add: sum.cartesian_product' sum.reindex N_def flip: UNIV_Times_UNIV)
apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N⇧2) * (real N * sqrt (real b⇩i))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left cinner_ket N_def
if_distrib[where f=‹λx. cinner _ x›] if_distrib[where f=‹λx. cinner x _›])
also have ‹… ≤ sqrt (real b⇩i) / N›
by (metis divide_inverse_commute dual_order.refl of_nat_mult power2_eq_square real_divide_square_eq)
finally show ?thesis
by -
qed
have norm_t5: ‹norm ?t5 ≤ 1 / sqrt N›
proof -
have ‹norm ?t5 = inverse (N * sqrt N) * norm (∑yd∈UNIV. if y⇩0 + fst yd = snd yd then 0 else β None *⇩C ket (fst yd, Some (snd yd)))›
by (simp add: sum.cartesian_product' sum.reindex flip: UNIV_Times_UNIV cong del: if_cong)
also have ‹… ≤ inverse (N * sqrt N) * N›
apply (rule mult_left_mono)
apply (rule norm_ortho_sum_bound[where b'=1])
by (auto simp: N_def)
also have ‹… = 1 / sqrt N›
by (simp add: divide_inverse_commute N_def)
finally show ?thesis
by -
qed
have norm_t6: ‹norm ?t6 ≤ 1 / sqrt N›
proof -
have ‹norm ?t6 = inverse N * norm (∑y∈UNIV. β None *⇩C ket (y :: 'y, None :: 'y option))›
by simp
also have ‹… ≤ inverse N * sqrt N›
apply (rule mult_left_mono)
apply (rule norm_ortho_sum_bound[where b'=1])
by (auto simp: N_def)
also have ‹… = 1 / sqrt N›
by (simp add: inverse_eq_divide sqrt_divide_self_eq)
finally show ?thesis
by -
qed
have ‹norm (PJ *⇩V φ) ≤ 1 / sqrt N + sqrt b⇩i / N + 1 / sqrt N
+ sqrt (real b⇩i) / N + 1 / sqrt N + 1 / sqrt N›
unfolding P0φ
apply (rule norm_triangle_le_diff norm_triangle_le, rule add_mono)+
apply (rule norm_t1)
apply (rule norm_t2)
apply (rule norm_t3)
apply (rule norm_t4)
apply (rule norm_t5)
apply (rule norm_t6)
by -
also have ‹… ≤ preserve_query1'_fixY_bound_output b⇩i›
by (auto simp: preserve_query1'_fixY_bound_output_def mult.commute mult.left_commute)
also have ‹… ≤ ε›
by (simp add: ε)
finally show ‹norm (Proj (- ket_invariant {(y⇩0 + d, Some d) |d. True}) *⇩V φ) ≤ ε›
unfolding PJ_def
apply (subst ket_invariant_compl[symmetric])
by simp
qed
text ‹A simpler to understand (and sometimes simpler to use) special case of
@{thm [source] preserve_query1'_fixY_output} in terms of \<^const>‹query'› and ket-invariants.›
lemma (in compressed_oracle) preserves_ket_query'_output_simple:
‹preserves_ket query' {(x, y, D). y = 0} {(x, y, D). D x = Some y} (6 / sqrt N)›
proof -
define K :: ‹'x ⇒ ('x × 'y × ('x ⇒ 'y option)) ell2 ccsubspace› where ‹K x = lift_invariant reg_1_3 (ket_invariant {x})› for x
show ?thesis
proof (rule inv_split_reg_query'[where X=‹reg_1_3› and Y=‹reg_2_3› and H=‹reg_3_3› and K=K
and ?I1.0=‹λ_. ket_invariant ({0} × UNIV)› and ?J1.0=‹λ_. ket_invariant {(0+d, Some d)| d. True}›])
show ‹query' = (reg_1_3;(reg_2_3;reg_3_3)) query'›
by (auto simp add: pair_Fst_Snd reg_1_3_def reg_2_3_def reg_3_3_def)
show ‹compatible reg_1_3 reg_2_3› ‹compatible reg_1_3 reg_3_3› ‹compatible reg_2_3 reg_3_3›
by simp_all
show ‹compatible_register_invariant reg_2_3 (K x)› for x
by (auto intro!: compatible_register_invariant_compatible_register simp add: K_def)
show ‹compatible_register_invariant (reg_3_3 o function_at x) (K x)› for x
by (auto intro!: compatible_register_invariant_compatible_register simp add: K_def)
show ‹ket_invariant {(x, y, D). y = 0}
≤ (SUP x. K x ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) (ket_invariant ({0} × UNIV)))›
apply (simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod' lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv case_prod_unfold)
by force
show ‹K x ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) (ket_invariant {(0+d, Some d)| d. True})
≤ ket_invariant {(x, y, D). D x = Some y}› for x
apply (simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod' lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv
case_prod_unfold)
by fastforce
show ‹orthogonal_spaces (K x) (K x')› if ‹x ≠ x'› for x x'
using that by (auto simp add: K_def orthogonal_spaces_lift_invariant)
show ‹preserves_ket query1' ({0} × UNIV) {(0+d, Some d)| d. True} (6 / sqrt N)›
apply (rule preserve_query1'_fixY_output[where b⇩i=N])
by (auto intro!: simp: preserve_query1'_fixY_bound_output_def simp flip: N_def)
show ‹K x ≤ lift_invariant reg_1_3 (ket_invariant {x})› for x
by (simp add: K_def)
show ‹6 / sqrt N ≥ 0›
by simp
qed simp
qed
text ‹A strengthened form of @{thm [source] preserves_ket_query'_output_simple} that additionally maintains
a property \<^term>‹P› on the already existing oracle register (that can depend also on some auxiliary register
and on the query input register).
This comes with the condition on \<^term>‹P› that when \<^term>‹P› accepts some oracle function that is undefined
at the query input \<^term>‹x›, then it needs to accept the updated oracle function with any output at \<^term>‹x›.
And if \<^term>‹P› doesn't accept the oracle function to be undefined at \<^term>‹x›, then it must accept
either only a small amount of outputs or all but a small amount of outputs for \<^term>‹x›.›
lemma (in compressed_oracle) preserves_ket_query'_output:
fixes F :: ‹('x×'y×('x⇀'y)) update ⇒ 'mem update›
and P :: ‹'w::finite ⇒ 'x ⇒ ('x⇀'y) ⇒ bool›
and b :: nat
assumes [register]: ‹register G›
assumes ‹F = G o Snd›
assumes PNone: ‹⋀w x D. P w x (D(x:=None)) ⟹ P w x D›
assumes PSome: ‹⋀w x D. D x = None ⟹ ¬ P w x D ⟹ let c = card {y. P w x (D(x:=Some y))} in c*(N-c) ≤ b›
shows ‹preserves (F query') (lift_invariant G (ket_invariant {(w, x, y, D). y = 0 ∧ P w x D}))
(lift_invariant G (ket_invariant {(w, x, y, D). D x = Some y ∧ P w x D}))
(9 / sqrt N + 2 * sqrt b / N)›
proof -
define K :: ‹'w×'x×('x⇀'y) ⇒ 'mem ell2 ccsubspace› where
‹K = (λ(w,x,D). lift_invariant G (ket_invariant {(w, x, y, D') | y D'. D'(x:=None) = D}))›
define M :: ‹('w×'x×('x⇀'y)) set› where
‹M = {(w,x,D). D x = None}›
define I1 :: ‹'w×'x×('x⇀'y) ⇒ ('y × 'y option) ell2 ccsubspace› where
‹I1 = (λ(w,x,D). ket_invariant {(0, y) | y. P w x (D(x:=y))})›
define J1 :: ‹'w×'x×('x⇀'y) ⇒ ('y × 'y option) ell2 ccsubspace› where
‹J1 = (λ(w,x,D). ket_invariant {(y, Some y) | y. P w x (D(x:=Some y))})›
show ?thesis
proof (rule inv_split_reg_query'[where X=‹G o Snd o reg_1_3› and Y=‹G o Snd o reg_2_3› and H=‹G o Snd o reg_3_3›
and K=K and ?I1.0=I1 and ?J1.0=J1 and M=M])
show ‹F query' = (G ∘ Snd ∘ reg_1_3;(G ∘ Snd ∘ reg_2_3;G ∘ Snd ∘ reg_3_3)) query'›
unfolding reg_1_3_def reg_2_3_def reg_3_3_def assms
by (simp flip: comp_assoc)
show ‹compatible (G ∘ Snd ∘ reg_1_3) (G ∘ Snd ∘ reg_2_3)› ‹compatible (G ∘ Snd ∘ reg_1_3) (G ∘ Snd ∘ reg_3_3)› ‹compatible (G ∘ Snd ∘ reg_2_3) (G ∘ Snd ∘ reg_3_3)›
by simp_all
show ‹compatible_register_invariant (G ∘ Snd ∘ reg_2_3) (K wxD)› if ‹wxD ∈ M› for wxD
by (auto intro!: compatible_register_invariant_Snd_comp compatible_register_invariant_Fst
simp add: K_def assms compatible_register_invariant_chain reg_2_3_def
comp_assoc M_def split!: prod.split)
show ‹compatible_register_invariant ((G ∘ Snd o reg_3_3) o function_at (let (w,x,D) = wxD in x)) (K wxD)› if ‹wxD ∈ M› for wxD
by (auto intro!: compatible_register_invariant_Snd_comp compatible_register_invariant_function_at
simp add: K_def compatible_register_invariant_chain comp_assoc reg_3_3_def
split!: prod.split)
show ‹lift_invariant G (ket_invariant {(w, x, y, D). y = 0 ∧ P w x D})
≤ (⨆wxD∈M. K wxD ⊓ lift_invariant (G ∘ Snd ∘ reg_2_3;G ∘ Snd ∘ reg_3_3 ∘ function_at (let (w, x, D) = wxD in x)) (I1 wxD))›
by (auto intro!: lift_invariant_mono
simp add: K_def M_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric] register_comp_pair
comp_assoc I1_def
lift_inv_prod' lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv case_prod_unfold
simp flip: lift_invariant_inf lift_invariant_SUP
split!: prod.split)
have aux: ‹D'(fst (snd wxD) := None) = snd (snd wxD) ⟹
D' (fst (snd wxD)) = Some ya ⟹
P (fst wxD) (fst (snd wxD)) ((snd (snd wxD))(fst (snd wxD) ↦ ya)) ⟹
P (fst wxD) (fst (snd wxD)) D'› for wxD D' ya
by (metis fun_upd_triv fun_upd_upd)
show ‹K wxD ⊓ lift_invariant (G ∘ Snd ∘ reg_2_3;G ∘ Snd ∘ reg_3_3 ∘ function_at (let (w, x, D) = wxD in x)) (J1 wxD)
≤ lift_invariant G (ket_invariant {(w, x, y, D). D x = Some y ∧ P w x D})› if ‹wxD ∈ M› for wxD
using that
by (auto intro!: aux lift_invariant_mono
simp add: K_def J1_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod' Times_Int_Times lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv
lift_invariant_comp register_comp_pair lift_Snd_inv
comp_assoc case_prod_unfold ket_invariant_tensor
simp flip: lift_invariant_inf ket_invariant_SUP ket_invariant_UNIV
split!: prod.split)
show ‹orthogonal_spaces (K wxD) (K wxD')› if ‹wxD ∈ M› and ‹wxD' ∈ M› and ‹wxD ≠ wxD'› for wxD wxD'
using that
by (auto simp add: K_def orthogonal_spaces_lift_invariant M_def split!: prod.split)
show ‹preserves query1' (I1 wxD) (J1 wxD) (9 / sqrt N + 2 * sqrt b / N)› if ‹wxD ∈ M› for wxD
proof -
obtain w x D where wxD[simp]: ‹wxD = (w,x,D)›
by (simp add: prod_eq_iff)
from that
have Dx: ‹D x = None›
by (simp add: M_def)
have I1: ‹I1 (w,x,D) = ket_invariant ({0} × {y. P w x (D(x := y))})›
by (auto simp add: I1_def)
have presY: ‹preserves query1' (I1 wxD) (ket_invariant {(0+d, Some d)| d. True}) (6 / sqrt (real N))›
apply (simp only: wxD I1)
apply (rule preserve_query1'_fixY_output[where b⇩i=N])
apply (simp add: N_def card_mono)
using sqrt_divide_self_eq
by (simp add: preserve_query1'_fixY_bound_output_def divide_inverse flip: N_def)
have presP1: ‹preserves query1' (I1 wxD) (ket_invariant (UNIV × {y. P w x (D(x := y))})) (3 / sqrt N + 2 * sqrt b / N)›
if ‹¬ P w x D›
proof -
from that Dx PNone have NoneI: ‹(None ∈ {y. P w x (D(x := y))}) = False›
by auto
from that Dx PNone have NoneJ: ‹(None ∉ {y. P w x (D(x := y))}) = True›
by auto
define b⇩i where ‹b⇩i = card (Some -` {y. P w x (D(x := y))})›
define b⇩j⇩0 where ‹b⇩j⇩0 = card (- Some -` {y. P w x (D(x := y))})›
have ‹sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N) + 2 * sqrt b⇩j⇩0 * sqrt b⇩i / N + 1 / sqrt N + sqrt b⇩i / N
≤ 3 / sqrt N + 2 * sqrt b / N›
proof -
have ‹b⇩j⇩0 = N - b⇩i›
by (simp add: N_def b⇩i_def b⇩j⇩0_def card_complement)
then have ‹b⇩i * b⇩j⇩0 ≤ b›
using PSome[of D x w] that
by (auto intro!: simp: b⇩i_def Let_def Dx)
have ‹b⇩i ≤ N›
apply (simp add: b⇩i_def)
by (metis N_def card_complement diff_le_self double_complement)
have bbN: ‹sqrt b⇩j⇩0 * sqrt b⇩i ≤ N›
using ‹b⇩i ≤ N› ‹b⇩j⇩0 = N - b⇩i›
by (smt (verit, best) Extra_Ordered_Fields.sign_simps(5) of_nat_0_le_iff of_nat_diff
ordered_comm_semiring_class.comm_mult_left_mono real_sqrt_ge_0_iff sqrt_sqrt)
have bbb: ‹sqrt b⇩j⇩0 * sqrt b⇩i ≤ sqrt b›
using ‹b⇩i * b⇩j⇩0 ≤ b›
by (smt (verit) Num.of_nat_simps(5) cross3_simps(11) of_nat_mono real_sqrt_le_iff real_sqrt_mult)
have sqrtNN: ‹sqrt N / N = 1 / sqrt N›
by (metis div_by_1 inverse_divide of_nat_0_le_iff real_div_sqrt)
have ‹sqrt b⇩j⇩0 * sqrt b⇩i / (N * sqrt N) + 2 * sqrt b⇩j⇩0 * sqrt b⇩i / N + 1 / sqrt N + sqrt b⇩i / N
≤ N / (N * sqrt N) + 2 * sqrt b / N + 1 / sqrt N + sqrt N / N›
apply (intro add_mono divide_right_mono)
by (auto intro!: ‹b⇩i ≤ N› bbN bbb)
also have ‹… = 3 / sqrt N + 2 * sqrt b / N›
by (simp add: nonzero_divide_mult_cancel_left sqrtNN)
finally show ?thesis
by -
qed
then show ?thesis
apply (simp only: wxD I1)
apply (rule preserve_query1'_fixY[where b⇩i=b⇩i and b⇩j⇩0=b⇩j⇩0])
unfolding NoneI
by (simp_all add: b⇩i_def b⇩j⇩0_def preserve_query1'_fixY_bound_def)
qed
have presP2: ‹preserves query1' (I1 wxD) (ket_invariant (UNIV × {y. P w x (D(x := y))})) (3 / sqrt N + 2 * sqrt b / N)›
if ‹P w x D›
apply (rewrite at ‹{y. P w x (D(x := y))}› to UNIV DEADID.rel_mono_strong)
using that PNone Dx apply (metis UNIV_eq_I array_rules(5) fun_upd_triv mem_Collect_eq)
by auto
from presP1 presP2
have presP: ‹preserves query1' (I1 wxD) (ket_invariant (UNIV × {y. P w x (D(x := y))})) (3 / sqrt N + 2 * sqrt b / N)›
by auto
from preserves_intersect[OF _ presY presP]
have ‹preserves query1' (I1 wxD) (ket_invariant {(0 + d, Some d) |d. True} ⊓ ket_invariant (UNIV × {y. P w x (D(x := y))}))
((6 / sqrt N) + (3 / sqrt N + 2 * sqrt b / N))›
by auto
then show ?thesis
apply (rule arg_cong4[where f=preserves, THEN iffD1, rotated -1])
by (auto intro!: simp: ket_invariant_inter J1_def)
qed
show ‹K wxD ≤ lift_invariant (G ∘ Snd ∘ reg_1_3) (ket_invariant {let (w, x, D) = wxD in x})› for wxD
by (auto intro!: lift_invariant_mono
simp add: K_def lift_invariant_comp reg_1_3_def lift_Fst_ket_inv lift_Snd_ket_inv
split!: prod.split)
show ‹9 / sqrt N + 2 * sqrt b / N ≥ 0›
by simp
show ‹finite M›
by simp
qed
qed
text ‹This is an example of how @{thm [source] preserves_ket_query'_output} is used to deal with more complex query sequences.
It is also useful in its own right (we use it in ‹Collision.thy›).
It shows that if we make two queries, then the oracle function contains the outputs of both queries.
(In contrast, @{thm [source] preserves_ket_query'_output_simple} shows this only for a single query.)›
lemma dist_inv_double_query':
fixes X1 X2 Y1 Y2 H and state1 :: ‹'mem ell2›
defines ‹state2 ≡ (X1;(Y1;H)) query' *⇩V state1›
defines ‹state3 ≡ (X2;(Y2;H)) query' *⇩V state2›
assumes [register]: ‹mutually compatible (X1,X2,Y1,Y2,H)›
assumes [iff]: ‹norm state1 ≤ 1›
assumes dist1: ‹dist_inv ((X1;X2);((Y1;Y2);H)) (ket_invariant {((x1,x2),(y1,y2),D). y1 = 0 ∧ y2 = 0}) state1 ≤ ε›
shows ‹dist_inv ((X1;X2);((Y1;Y2);H)) (ket_invariant {((x1,x2),(y1,y2),D). D x1 = Some y1 ∧ D x2 = Some y2}) state3 ≤ ε + 20 / sqrt N›
proof -
have [iff]: ‹norm state2 ≤ 1›
by (auto intro!: norm_cblinfun_apply_leq1I simp add: state2_def register_norm)
have bound: ‹let c = card {y2. (x' = x2 ⟶ y2 = y') ∧ x' = x2} in c * (N - c) ≤ N› for x' x2 y'
by (cases ‹x' = x2›, auto)
from dist1 have ‹dist_inv ((X2; Y2); (X1;(Y1;H)))
(ket_invariant {(x2y2,(x1,y1,D)). y1 = 0 ∧ snd x2y2 = 0}) state1 ≤ ε›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite, simp, simp)
apply (rewrite at ‹((X2;Y2);(X1;(Y1;H)))› to ‹((X1;X2);((Y1;Y2);H)) o ((reg_1_3 o Snd; reg_2_3 o Snd); (reg_1_3 o Fst; (reg_2_3 o Fst; reg_3_3)))› DEADID.rel_mono_strong)
apply (simp add: register_pair_Snd register_pair_Fst flip: register_comp_pair comp_assoc)
apply (subst lift_invariant_comp, simp)
apply simp
by (auto intro!: simp: lift_inv_prod' reg_1_3_def reg_3_3_def reg_2_3_def lift_invariant_comp lift_Snd_ket_inv lift_Fst_ket_inv
ket_invariant_inter case_prod_unfold
simp flip: ket_invariant_SUP)
then have ‹dist_inv ((X2; Y2); (X1;(Y1;H)))
(ket_invariant {(x2y2,(x1,y1,D)). D x1 = Some y1 ∧ snd x2y2 = 0}) state2 ≤ ε + 9 / sqrt (real N)›
unfolding state2_def
apply (rule dist_inv_preservesI)
apply (rule preserves_ket_query'_output[where b=0])
by (auto intro!: simp: register_pair_Snd register_norm simp del: o_apply)
then have ‹dist_inv ((X1; Y1); (X2;(Y2;H)))
(ket_invariant {(x1y1,(x2,y2,D)). y2 = 0 ∧ D (fst x1y1) = Some (snd x1y1)}) state2 ≤ ε + 9 / sqrt (real N)›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite, simp, simp)
apply (rewrite at ‹((X1; Y1); (X2;(Y2;H)))› to ‹((X2; Y2); (X1;(Y1;H))) o ((Snd o reg_1_3; Snd o reg_2_3); (Fst o Fst; (Fst o Snd; Snd o reg_3_3)))› DEADID.rel_mono_strong)
apply (simp add: register_pair_Snd register_pair_Fst flip: register_comp_pair comp_assoc)
apply (subst lift_invariant_comp, simp)
apply simp
by (auto intro!: simp: lift_inv_prod' reg_1_3_def reg_3_3_def reg_2_3_def lift_invariant_comp lift_Snd_ket_inv lift_Fst_ket_inv
ket_invariant_inter case_prod_unfold
simp flip: ket_invariant_SUP)
then have ‹dist_inv ((X1; Y1); (X2;(Y2;H)))
(ket_invariant {(x1y1,(x2,y2,D)). D x2 = Some y2 ∧ D (fst x1y1) = Some (snd x1y1)}) state3 ≤ ε + 20 / sqrt N›
unfolding state3_def
apply (rule dist_inv_preservesI)
apply (rule preserves_ket_query'_output[where b=N])
by (auto intro!: bound simp: register_pair_Snd register_norm simp del: o_apply split!: if_split_asm)
then show ‹dist_inv ((X1;X2);((Y1;Y2);H)) (ket_invariant {((x1,x2),(y1,y2),D). D x1 = Some y1 ∧ D x2 = Some y2}) state3 ≤ ε + 20 / sqrt N›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite, simp, simp)
apply (rewrite at ‹((X1; Y1); (X2;(Y2;H)))› to ‹((X1;X2);((Y1;Y2);H)) o ((reg_1_3 o Fst; reg_2_3 o Fst); (reg_1_3 o Snd; (reg_2_3 o Snd; reg_3_3)))› DEADID.rel_mono_strong)
apply (simp add: register_pair_Snd register_pair_Fst flip: register_comp_pair comp_assoc)
apply (subst lift_invariant_comp, simp)
apply simp
by (auto intro!: simp: lift_inv_prod' reg_1_3_def reg_3_3_def reg_2_3_def lift_invariant_comp lift_Snd_ket_inv lift_Fst_ket_inv
ket_invariant_inter case_prod_unfold
simp flip: ket_invariant_SUP)
qed
text ‹The next bound is applicable for ket-invariants assume the output register to have a value
\<^term>‹ket d› that matches what is in the output register before the query and require that after the query,
the oracle register is not \<^const>‹None› and the output register has the correct value given that
oracle register content. (I.e., before an uncomputation step.)
Notice that this invariant is only available for \<^const>‹query1'›, not for \<^const>‹query1›!›
definition ‹preserve_query1'_uncompute_bound NoneJ b⇩i b⇩j⇩0 =
of_bool NoneJ * sqrt b⇩i / sqrt N + of_bool NoneJ * sqrt b⇩i / N
+ sqrt b⇩j⇩0 / N + sqrt b⇩i * sqrt b⇩j⇩0 / N + sqrt b⇩i * sqrt b⇩j⇩0 / (N * sqrt N)›
lemma preserve_query1'_uncompute:
assumes IJ: ‹I ⊆ J›
assumes b⇩i: ‹card (Some -` I) ≤ b⇩i›
assumes b⇩j⇩0: ‹card (- Some -` J) ≤ b⇩j⇩0›
assumes ε: ‹ε ≥ preserve_query1'_uncompute_bound (None∉J) b⇩i b⇩j⇩0›
shows ‹preserves_ket query1' ((UNIV × I) ∩ {(d, Some d)| d. True}) (UNIV × J) ε›
proof (rule preservesI')
show ‹ε ≥ 0›
using _ ε apply (rule order.trans)
by (simp add: preserve_query1'_uncompute_bound_def)
fix ψ :: ‹('y × 'y option) ell2›
assume ψ: ‹ψ ∈ space_as_set (ket_invariant ((UNIV × I) ∩ {(d, Some d)| d. True}))›
assume ‹norm ψ = 1›
define I' J' where ‹I' = Some -` I› and ‹J' = Some -` J›
then have ‹((UNIV × I) ∩ {(d, Some d)| d. True}) = (λd. (d, Some d)) ` I'›
by auto
with ψ have ψ': ‹ψ ∈ space_as_set (ket_invariant ((λd. (d, Some d)) ` I'))›
by fastforce
have [simp]: ‹I' ⊆ J'›
using I'_def J'_def IJ by blast
have card_minus_J': ‹card (- J') ≤ b⇩j⇩0›
using J'_def b⇩j⇩0 by force
define β where ‹β d = Rep_ell2 ψ (d, Some d)› for d
have β: ‹ψ = (∑d∈I'. β d *⇩C ket (d, Some d))›
using ell2_sum_ket_ket_invariant[OF ψ']
apply (subst (asm) infsum_reindex)
apply (simp add: inj_on_convol_ident)
by (auto simp: β_def)
have βbound: ‹(∑d∈I'. (cmod (β d))⇧2) ≤ 1› (is ‹?lhs ≤ 1›)
apply (subgoal_tac ‹(norm ψ)⇧2 = ?lhs›)
apply (simp add: ‹norm ψ = 1›)
by (simp add: β pythagorean_theorem_sum del: sum.insert)
have [simp]: ‹Some x ∈ J ⟷ x ∈ J'› for x
by (simp add: J'_def)
have [simp]: ‹x ∈ I' ⟹ x ∈ J'› for x
using ‹I' ⊆ J'› by blast
have [simp]: ‹(∑x∈X. if x ∉ Y then f x else 0) = (∑x∈X-Y. f x)› if ‹finite X› for f :: ‹'y ⇒ 'z::ab_group_add› and X Y
apply (rule sum.mono_neutral_cong_right)
using that by auto
have [simp]: ‹β yd *⇩C a *⇩C b = a *⇩C β yd *⇩C b› for yd a and b :: ‹'z::complex_vector›
by auto
have [simp]: ‹cmod α = inverse (sqrt N)› ‹cmod (α⇧2) = inverse N› ‹cmod (α^3) = inverse (N * sqrt N)› ‹cmod (α^4) = inverse (N⇧2)›
by (auto simp: norm_mult numeral_3_eq_3 α_def inverse_eq_divide norm_divide norm_power power_one_over power2_eq_square power4_eq_xxxx)
have [simp]: ‹card I' ≤ b⇩i›
by (metis I'_def b⇩i)
define φ and PJ :: ‹('y * 'y option) update› where
‹φ = query1' *⇩V ψ› and ‹PJ = Proj (ket_invariant (UNIV × -J))›
have [simp]: ‹PJ *⇩V ket (x,y) = (if y∈-J then ket (x,y) else 0)› for x y
by (simp add: Proj_ket_invariant_ket PJ_def)
have P0φ: ‹PJ *⇩V φ =
(of_bool (None∉J) * α) *⇩C (∑d∈I'. β d *⇩C ket (0, None))
- (of_bool (None∉J) * α^3) *⇩C (∑d∈I'. ∑y∈UNIV. β d *⇩C ket (y, None))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈-J'. β d *⇩C ket (d + d', Some d'))
- α⇧2 *⇩C (∑d∈I'. ∑d'∈-J'. β d *⇩C ket (0, Some d'))
+ α^4 *⇩C (∑d∈I'. ∑y∈UNIV. ∑d''∈-J'. β d *⇩C ket (y, Some d''))
›
(is ‹_ = ?t1 - ?t2 - ?t3 - ?t4 + ?t5›)
by (simp add: φ_def β query1' option_sum_split vimage_Compl
cblinfun.add_right cblinfun.diff_right if_distrib Compl_eq_Diff_UNIV
vimage_singleton_inj sum_sum_if_eq sum.distrib scaleC_diff_right scaleC_sum_right
sum_subtractf case_prod_beta sum.cartesian_product' scaleC_add_right add_diff_eq
cblinfun.scaleC_right cblinfun.sum_right
flip: sum.Sigma add.assoc scaleC_scaleC
cong del: option.case_cong if_cong)
have norm_t1: ‹norm ?t1 ≤ of_bool (None∉J) * sqrt b⇩i / sqrt N›
proof (cases ‹None ∈ J›)
case True
then show ?thesis
by simp
next
case False
then have ‹norm ?t1 = inverse (sqrt N) * norm (∑d∈I'. β d *⇩C ket (0 :: 'y, None :: 'y option))›
by simp
also have ‹… ≤ inverse (sqrt N) * sqrt b⇩i›
apply (rule mult_left_mono)
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
also have ‹… = of_bool (None∉J) * sqrt b⇩i / sqrt N›
using False by (simp add: divide_inverse_commute)
finally show ?thesis
by -
qed
have norm_t2: ‹norm ?t2 ≤ of_bool (None∉J) * sqrt b⇩i / N›
proof (cases ‹None ∈ J›)
case True
then show ?thesis
by simp
next
case False
have *: ‹norm (∑d∈I'. β d *⇩C ket (y, None :: 'y option)) ≤ sqrt b⇩i› for y :: 'y
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
have ‹norm ?t2 = inverse (N * sqrt N) * norm (∑y∈UNIV. ∑d∈I'. β d *⇩C ket (y :: 'y, None :: 'y option))›
apply (subst sum.swap) by (simp add: False)
also have ‹… ≤ inverse (N * sqrt N) * (sqrt (real N) * sqrt (real b⇩i))›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto simp add: cinner_sum_right cinner_sum_left N_def)
also have ‹… = of_bool (None∉J) * sqrt b⇩i / N›
using False by (simp add: divide_inverse_commute N_def)
finally show ?thesis
by -
qed
have norm_t3: ‹norm ?t3 ≤ sqrt b⇩j⇩0 / N›
proof -
have *: ‹norm (∑d∈I'. β d *⇩C ket (d + d', Some d')) ≤ sqrt (1::nat)› for d' :: 'y
using _ _ βbound apply (rule bound_coeff_sum2)
by (auto simp add: card_le_Suc0_iff_eq)
have ‹norm ?t3 = inverse N * norm (∑d'∈- J'. ∑d∈I'. β d *⇩C ket (d + d', Some d'))›
apply (subst sum.swap) by simp
also have ‹… ≤ inverse N * sqrt b⇩j⇩0›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
using card_minus_J' by (auto simp add: cinner_sum_right cinner_sum_left)
also have ‹… = sqrt b⇩j⇩0 / N›
by (simp add: divide_inverse_commute)
finally show ?thesis
by -
qed
have norm_t4: ‹norm ?t4 ≤ sqrt b⇩i * sqrt b⇩j⇩0 / N›
proof -
have *: ‹norm (∑d∈I'. β d *⇩C ket (0, Some d')) ≤ sqrt b⇩i› for d' :: 'y
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
have ‹norm ?t4 = inverse N * norm (∑d'∈- J'. ∑d∈I'. β d *⇩C ket (0 :: 'y, Some d' :: 'y option))›
apply (subst sum.swap) by simp
also have ‹… ≤ inverse N * (sqrt b⇩j⇩0 * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
by (auto intro!: card_minus_J' mult_right_mono simp add: cinner_sum_right cinner_sum_left)
also have ‹… = sqrt b⇩i * sqrt b⇩j⇩0 / N›
by (simp add: divide_inverse_commute)
finally show ?thesis
by -
qed
have norm_t5: ‹norm ?t5 ≤ sqrt b⇩i * sqrt b⇩j⇩0 / (N * sqrt N)›
proof -
have *: ‹norm (∑d∈I'. β d *⇩C ket (fst yd'', Some (snd yd''))) ≤ sqrt b⇩i› for yd'' :: ‹'y × 'y›
using _ _ βbound apply (rule bound_coeff_sum2)
by auto
have ‹norm ?t5 = inverse (N⇧2) * norm (∑yd''∈UNIV×-J'. ∑d∈I'. β d *⇩C ket (fst yd'' :: 'y, Some (snd yd'')))›
apply (simp add: sum.cartesian_product' sum.reindex N_def)
apply (subst (2) sum.swap) apply (subst sum.swap)
by (rule refl)
also have ‹… ≤ inverse (N⇧2) * (sqrt N * sqrt b⇩j⇩0 * sqrt b⇩i)›
apply (rule mult_left_mono)
using * apply (rule norm_ortho_sum_bound)
using card_minus_J' by (auto intro!: mult_right_mono simp add: cinner_sum_right cinner_sum_left cinner_ket real_sqrt_mult N_def)
also have ‹… = sqrt b⇩i * sqrt b⇩j⇩0 / (N * sqrt N)›
by (smt (verit, ccfv_threshold) field_class.field_divide_inverse mult.commute of_nat_0_le_iff of_nat_power power2_eq_square real_divide_square_eq real_sqrt_mult_self times_divide_times_eq)
finally show ?thesis
by -
qed
have ‹norm (PJ *⇩V φ) ≤ of_bool (None∉J) * sqrt b⇩i / sqrt N + of_bool (None∉J) * sqrt b⇩i / N
+ sqrt b⇩j⇩0 / N + sqrt b⇩i * sqrt b⇩j⇩0 / N + sqrt b⇩i * sqrt b⇩j⇩0 / (N * sqrt N)›
unfolding P0φ
apply (rule norm_triangle_le_diff norm_triangle_le, rule add_mono)+
apply (rule norm_t1)
apply (rule norm_t2)
apply (rule norm_t3)
apply (rule norm_t4)
by (rule norm_t5)
also have ‹… = preserve_query1'_uncompute_bound (None∉J) b⇩i b⇩j⇩0›
by (auto simp: preserve_query1'_uncompute_bound_def mult.commute mult.left_commute)
also have ‹… ≤ ε›
by (simp add: ε)
finally show ‹norm (Proj (- ket_invariant (UNIV × J)) *⇩V φ) ≤ ε›
unfolding PJ_def
apply (subst ket_invariant_compl[symmetric])
by simp
qed
end
end