Expression of type Forall ¶

from the theory of proveit.physics.quantum.algebra ¶

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import A, V, W, i, j, m, n
from proveit.core_expr_types import v_1_to_m, v_i, w_1_to_n, w_j
from proveit.linear_algebra import OrthoNormBases, VecSum
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Interval, NaturalPos, one
from proveit.physics.quantum import Bra, Ket, Qmult
from proveit.physics.quantum.algebra import v_1_to_m_kets, w_1_to_n_kets

# build up the expression from sub-expressions
expr = Forall(instance_param_or_params = [m, n], instance_expr = Forall(instance_param_or_params = [v_1_to_m], instance_expr = Forall(instance_param_or_params = [w_1_to_n], instance_expr = Equals(A, VecSum(index_or_indices = [i], summand = VecSum(index_or_indices = [j], summand = Qmult(Bra(w_j), A, Ket(v_i), Ket(w_j), Bra(v_i)), domain = Interval(one, n)), domain = Interval(one, m))), condition = InSet(w_1_to_n_kets, OrthoNormBases(W))).with_wrapping(), condition = InSet(v_1_to_m_kets, OrthoNormBases(V))).with_wrapping(), domain = NaturalPos)

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\forall_{m, n \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{v_{1}, v_{2}, \ldots, v_{m}~|~\left\{\lvert v_{1} \rangle, \lvert v_{2} \rangle, \ldots, \lvert v_{m} \rangle\right\} \in \textrm{O.N.Bases}\left(V\right)}~\\
\left[\begin{array}{l}\forall_{w_{1}, w_{2}, \ldots, w_{n}~|~\left\{\lvert w_{1} \rangle, \lvert w_{2} \rangle, \ldots, \lvert w_{n} \rangle\right\} \in \textrm{O.N.Bases}\left(W\right)}~\\
\left(A = \left(\sum_{i=1}^{m} \left(\sum_{j=1}^{n} \left(\langle w_{j} \rvert \thinspace A \thinspace \lvert v_{i} \rangle \thinspace \lvert w_{j} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\end{array}\right]\end{array}\right]

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

	core type	sub-expressions
0	Operation	operator: 22 operand: 2
1	ExprTuple	2
2	Lambda	parameters: 3 body: 4
3	ExprTuple	73, 94
4	Conditional	value: 5 condition: 6
5	Operation	operator: 22 operand: 10
6	Operation	operator: 8 operands: 9
7	ExprTuple	10
8	Literal
9	ExprTuple	11, 12
10	Lambda	parameters: 13 body: 14
11	Operation	operator: 77 operands: 15
12	Operation	operator: 77 operands: 16
13	ExprTuple	17
14	Conditional	value: 18 condition: 19
15	ExprTuple	73, 20
16	ExprTuple	94, 20
17	ExprRange	lambda_map: 21 start_index: 93 end_index: 73
18	Operation	operator: 22 operand: 25
19	Operation	operator: 77 operands: 24
20	Literal
21	Lambda	parameter: 74 body: 55
22	Literal
23	ExprTuple	25
24	ExprTuple	26, 27
25	Lambda	parameters: 28 body: 29
26	Operation	operator: 47 operands: 30
27	Operation	operator: 49 operand: 36
28	ExprTuple	32
29	Conditional	value: 33 condition: 34
30	ExprTuple	35
31	ExprTuple	36
32	ExprRange	lambda_map: 37 start_index: 93 end_index: 94
33	Operation	operator: 38 operands: 39
34	Operation	operator: 77 operands: 40
35	ExprRange	lambda_map: 41 start_index: 93 end_index: 73
36	Variable
37	Lambda	parameter: 74 body: 67
38	Literal
39	ExprTuple	80, 42
40	ExprTuple	43, 44
41	Lambda	parameter: 74 body: 45
42	Operation	operator: 61 operand: 52
43	Operation	operator: 47 operands: 48
44	Operation	operator: 49 operand: 54
45	Operation	operator: 85 operand: 55
46	ExprTuple	52
47	Literal
48	ExprTuple	53
49	Literal
50	ExprTuple	54
51	ExprTuple	55
52	Lambda	parameter: 100 body: 56
53	ExprRange	lambda_map: 57 start_index: 93 end_index: 94
54	Variable
55	IndexedVar	variable: 97 index: 74
56	Conditional	value: 58 condition: 59
57	Lambda	parameter: 74 body: 60
58	Operation	operator: 61 operand: 65
59	Operation	operator: 77 operands: 63
60	Operation	operator: 85 operand: 67
61	Literal
62	ExprTuple	65
63	ExprTuple	100, 66
64	ExprTuple	67
65	Lambda	parameter: 99 body: 68
66	Operation	operator: 89 operands: 69
67	IndexedVar	variable: 95 index: 74
68	Conditional	value: 71 condition: 72
69	ExprTuple	93, 73
70	ExprTuple	74
71	Operation	operator: 75 operands: 76
72	Operation	operator: 77 operands: 78
73	Variable
74	Variable
75	Literal
76	ExprTuple	79, 80, 81, 82, 83
77	Literal
78	ExprTuple	99, 84
79	Operation	operator: 87 operand: 91
80	Variable
81	Operation	operator: 85 operand: 92
82	Operation	operator: 85 operand: 91
83	Operation	operator: 87 operand: 92
84	Operation	operator: 89 operands: 90
85	Literal
86	ExprTuple	91
87	Literal
88	ExprTuple	92
89	Literal
90	ExprTuple	93, 94
91	IndexedVar	variable: 95 index: 99
92	IndexedVar	variable: 97 index: 100
93	Literal
94	Variable
95	Variable
96	ExprTuple	99
97	Variable
98	ExprTuple	100
99	Variable
100	Variable

Expression of type Forall¶

from the theory of proveit.physics.quantum.algebra¶

Expression of type Forall ¶

from the theory of proveit.physics.quantum.algebra ¶