unierri

Description: If we approximate a chain of unitary transformations (quantum computer gates) F , G by other unitary transformations S , T , the error increases at most additively. Equation 4.73 of NielsenChuang p. 195. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	unierr.1	$⊢ F \in UniOp$
	unierr.2	$⊢ G \in UniOp$
	unierr.3	$⊢ S \in UniOp$
	unierr.4	$⊢ T \in UniOp$
Assertion	unierri	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T)$

Proof

Step	Hyp	Ref	Expression
1		unierr.1	$⊢ F \in UniOp$
2		unierr.2	$⊢ G \in UniOp$
3		unierr.3	$⊢ S \in UniOp$
4		unierr.4	$⊢ T \in UniOp$
5		unopbd	$⊢ F \in UniOp \to F \in BndLinOp$
6	1 5	ax-mp	$⊢ F \in BndLinOp$
7		bdopf	$⊢ F \in BndLinOp \to F : ℋ ⟶ ℋ$
8	6 7	ax-mp	$⊢ F : ℋ ⟶ ℋ$
9		unopbd	$⊢ G \in UniOp \to G \in BndLinOp$
10	2 9	ax-mp	$⊢ G \in BndLinOp$
11		bdopf	$⊢ G \in BndLinOp \to G : ℋ ⟶ ℋ$
12	10 11	ax-mp	$⊢ G : ℋ ⟶ ℋ$
13	8 12	hocofi	$⊢ (F \circ G) : ℋ ⟶ ℋ$
14		unopbd	$⊢ S \in UniOp \to S \in BndLinOp$
15	3 14	ax-mp	$⊢ S \in BndLinOp$
16		bdopf	$⊢ S \in BndLinOp \to S : ℋ ⟶ ℋ$
17	15 16	ax-mp	$⊢ S : ℋ ⟶ ℋ$
18		unopbd	$⊢ T \in UniOp \to T \in BndLinOp$
19	4 18	ax-mp	$⊢ T \in BndLinOp$
20		bdopf	$⊢ T \in BndLinOp \to T : ℋ ⟶ ℋ$
21	19 20	ax-mp	$⊢ T : ℋ ⟶ ℋ$
22	17 21	hocofi	$⊢ (S \circ T) : ℋ ⟶ ℋ$
23	13 22	hosubcli	$⊢ ((F \circ G) -_{op} (S \circ T)) : ℋ ⟶ ℋ$
24		nmop0h	$⊢ (ℋ = 0_{ℋ} \land ((F \circ G) -_{op} (S \circ T)) : ℋ ⟶ ℋ) \to {norm}_{op} ((F \circ G) -_{op} (S \circ T)) = 0$
25	23 24	mpan2	$⊢ ℋ = 0_{ℋ} \to {norm}_{op} ((F \circ G) -_{op} (S \circ T)) = 0$
26		0le0	$⊢ 0 \leq 0$
27		00id	$⊢ 0 + 0 = 0$
28	26 27	breqtrri	$⊢ 0 \leq 0 + 0$
29	8 17	hosubcli	$⊢ (F -_{op} S) : ℋ ⟶ ℋ$
30		nmop0h	$⊢ (ℋ = 0_{ℋ} \land (F -_{op} S) : ℋ ⟶ ℋ) \to {norm}_{op} (F -_{op} S) = 0$
31	29 30	mpan2	$⊢ ℋ = 0_{ℋ} \to {norm}_{op} (F -_{op} S) = 0$
32	12 21	hosubcli	$⊢ (G -_{op} T) : ℋ ⟶ ℋ$
33		nmop0h	$⊢ (ℋ = 0_{ℋ} \land (G -_{op} T) : ℋ ⟶ ℋ) \to {norm}_{op} (G -_{op} T) = 0$
34	32 33	mpan2	$⊢ ℋ = 0_{ℋ} \to {norm}_{op} (G -_{op} T) = 0$
35	31 34	oveq12d	$⊢ ℋ = 0_{ℋ} \to {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T) = 0 + 0$
36	28 35	breqtrrid	$⊢ ℋ = 0_{ℋ} \to 0 \leq {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T)$
37	25 36	eqbrtrd	$⊢ ℋ = 0_{ℋ} \to {norm}_{op} ((F \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T)$
38	17 12	hocofi	$⊢ (S \circ G) : ℋ ⟶ ℋ$
39	13 38 22	honpncani	$⊢ ((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T)) = (F \circ G) -_{op} (S \circ T)$
40	39	fveq2i	$⊢ {norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) = {norm}_{op} ((F \circ G) -_{op} (S \circ T))$
41	6 10	bdopcoi	$⊢ F \circ G \in BndLinOp$
42	15 10	bdopcoi	$⊢ S \circ G \in BndLinOp$
43	41 42	bdophdi	$⊢ (F \circ G) -_{op} (S \circ G) \in BndLinOp$
44	15 19	bdopcoi	$⊢ S \circ T \in BndLinOp$
45	42 44	bdophdi	$⊢ (S \circ G) -_{op} (S \circ T) \in BndLinOp$
46	43 45	nmoptrii	$⊢ {norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) \leq {norm}_{op} ((F \circ G) -_{op} (S \circ G)) + {norm}_{op} ((S \circ G) -_{op} (S \circ T))$
47	8 17 12	hocsubdiri	$⊢ (F -_{op} S) \circ G = (F \circ G) -_{op} (S \circ G)$
48	47	fveq2i	$⊢ {norm}_{op} ((F -_{op} S) \circ G) = {norm}_{op} ((F \circ G) -_{op} (S \circ G))$
49	6 15	bdophdi	$⊢ F -_{op} S \in BndLinOp$
50	49 10	nmopcoi	$⊢ {norm}_{op} ((F -_{op} S) \circ G) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G)$
51	48 50	eqbrtrri	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ G)) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G)$
52		bdopln	$⊢ S \in BndLinOp \to S \in LinOp$
53	15 52	ax-mp	$⊢ S \in LinOp$
54	53 12 21	hoddii	$⊢ S \circ (G -_{op} T) = (S \circ G) -_{op} (S \circ T)$
55	54	fveq2i	$⊢ {norm}_{op} (S \circ (G -_{op} T)) = {norm}_{op} ((S \circ G) -_{op} (S \circ T))$
56	10 19	bdophdi	$⊢ G -_{op} T \in BndLinOp$
57	15 56	nmopcoi	$⊢ {norm}_{op} (S \circ (G -_{op} T)) \leq {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
58	55 57	eqbrtrri	$⊢ {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
59		nmopre	$⊢ (F \circ G) -_{op} (S \circ G) \in BndLinOp \to {norm}_{op} ((F \circ G) -_{op} (S \circ G)) \in ℝ$
60	43 59	ax-mp	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ G)) \in ℝ$
61		nmopre	$⊢ (S \circ G) -_{op} (S \circ T) \in BndLinOp \to {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \in ℝ$
62	45 61	ax-mp	$⊢ {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \in ℝ$
63		nmopre	$⊢ F -_{op} S \in BndLinOp \to {norm}_{op} (F -_{op} S) \in ℝ$
64	49 63	ax-mp	$⊢ {norm}_{op} (F -_{op} S) \in ℝ$
65		nmopre	$⊢ G \in BndLinOp \to {norm}_{op} (G) \in ℝ$
66	10 65	ax-mp	$⊢ {norm}_{op} (G) \in ℝ$
67	64 66	remulcli	$⊢ {norm}_{op} (F -_{op} S) {norm}_{op} (G) \in ℝ$
68		nmopre	$⊢ S \in BndLinOp \to {norm}_{op} (S) \in ℝ$
69	15 68	ax-mp	$⊢ {norm}_{op} (S) \in ℝ$
70		nmopre	$⊢ G -_{op} T \in BndLinOp \to {norm}_{op} (G -_{op} T) \in ℝ$
71	56 70	ax-mp	$⊢ {norm}_{op} (G -_{op} T) \in ℝ$
72	69 71	remulcli	$⊢ {norm}_{op} (S) {norm}_{op} (G -_{op} T) \in ℝ$
73	60 62 67 72	le2addi	$⊢ ({norm}_{op} ((F \circ G) -_{op} (S \circ G)) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) \land {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (S) {norm}_{op} (G -_{op} T)) \to {norm}_{op} ((F \circ G) -_{op} (S \circ G)) + {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
74	51 58 73	mp2an	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ G)) + {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
75	43 45	bdophsi	$⊢ ((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T)) \in BndLinOp$
76		nmopre	$⊢ ((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T)) \in BndLinOp \to {norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) \in ℝ$
77	75 76	ax-mp	$⊢ {norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) \in ℝ$
78	60 62	readdcli	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ G)) + {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \in ℝ$
79	67 72	readdcli	$⊢ {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T) \in ℝ$
80	77 78 79	letri	$⊢ ({norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) \leq {norm}_{op} ((F \circ G) -_{op} (S \circ G)) + {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \land {norm}_{op} ((F \circ G) -_{op} (S \circ G)) + {norm}_{op} ((S \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T)) \to {norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
81	46 74 80	mp2an	$⊢ {norm}_{op} (((F \circ G) -_{op} (S \circ G)) +_{op} ((S \circ G) -_{op} (S \circ T))) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
82	40 81	eqbrtrri	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T)$
83		nmopun	$⊢ (ℋ \neq 0_{ℋ} \land G \in UniOp) \to {norm}_{op} (G) = 1$
84	2 83	mpan2	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (G) = 1$
85	84	oveq2d	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (F -_{op} S) {norm}_{op} (G) = {norm}_{op} (F -_{op} S) \cdot 1$
86	64	recni	$⊢ {norm}_{op} (F -_{op} S) \in ℂ$
87	86	mulid1i	$⊢ {norm}_{op} (F -_{op} S) \cdot 1 = {norm}_{op} (F -_{op} S)$
88	85 87	eqtrdi	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (F -_{op} S) {norm}_{op} (G) = {norm}_{op} (F -_{op} S)$
89		nmopun	$⊢ (ℋ \neq 0_{ℋ} \land S \in UniOp) \to {norm}_{op} (S) = 1$
90	3 89	mpan2	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (S) = 1$
91	90	oveq1d	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (S) {norm}_{op} (G -_{op} T) = 1 {norm}_{op} (G -_{op} T)$
92	71	recni	$⊢ {norm}_{op} (G -_{op} T) \in ℂ$
93	92	mulid2i	$⊢ 1 {norm}_{op} (G -_{op} T) = {norm}_{op} (G -_{op} T)$
94	91 93	eqtrdi	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (S) {norm}_{op} (G -_{op} T) = {norm}_{op} (G -_{op} T)$
95	88 94	oveq12d	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} (F -_{op} S) {norm}_{op} (G) + {norm}_{op} (S) {norm}_{op} (G -_{op} T) = {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T)$
96	82 95	breqtrid	$⊢ ℋ \neq 0_{ℋ} \to {norm}_{op} ((F \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T)$
97	37 96	pm2.61ine	$⊢ {norm}_{op} ((F \circ G) -_{op} (S \circ T)) \leq {norm}_{op} (F -_{op} S) + {norm}_{op} (G -_{op} T)$

Metamath Proof Explorer

Theorem unierri

Proof