Theorem born_rule_on_qubit of type Forall

from the theory of proveit.physics.quantum.circuits

see dependencies

import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.circuits import born_rule_on_qubit

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

Passed sanity check: born_rule_on_qubit matches stored_expr

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

\forall_{\lvert \psi \rangle \in \mathbb{C}^{2}, b \in \left\{0, 1\right\}~|~\left \|\lvert \psi \rangle\right \| = 1}~\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert \psi \rangle} & \meter & \qout{\lvert b \rangle}
} \end{array}\right) = \left|\langle b \rvert \thinspace \lvert \psi \rangle\right|^{2}\right)

stored_expr.style_options()

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',)

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Operation	operator: 1 operand: 3
1	Literal
2	ExprTuple	3
3	Lambda	parameters: 4 body: 5
4	ExprTuple	60, 66
5	Conditional	value: 6 condition: 7
6	Operation	operator: 23 operands: 8
7	Operation	operator: 9 operands: 10
8	ExprTuple	11, 12
9	Literal
10	ExprTuple	13, 14, 15
11	Operation	operator: 16 operand: 25
12	Operation	operator: 18 operands: 19
13	Operation	operator: 21 operands: 20
14	Operation	operator: 21 operands: 22
15	Operation	operator: 23 operands: 24
16	Literal
17	ExprTuple	25
18	Literal
19	ExprTuple	26, 45
20	ExprTuple	60, 27
21	Literal
22	ExprTuple	66, 28
23	Literal
24	ExprTuple	29, 47
25	Operation	operator: 30 operands: 31
26	Operation	operator: 32 operand: 43
27	Operation	operator: 34 operands: 35
28	Operation	operator: 36 operands: 37
29	Operation	operator: 38 operand: 60
30	Literal
31	ExprTuple	40, 41, 42
32	Literal
33	ExprTuple	43
34	Literal
35	ExprTuple	44, 45
36	Literal
37	ExprTuple	46, 47
38	Literal
39	ExprTuple	60
40	ExprTuple	48
41	ExprTuple	49
42	ExprTuple	50
43	Operation	operator: 51 operands: 52
44	Literal
45	Literal
46	Literal
47	Literal
48	Operation	operator: 53 operands: 54
49	Operation	operator: 55 operands: 56
50	Operation	operator: 57 operands: 58
51	Literal
52	ExprTuple	59, 60
53	Literal
54	NamedExprs	state: 60
55	Literal
56	NamedExprs	basis: 61
57	Literal
58	NamedExprs	state: 62
59	Operation	operator: 63 operand: 66
60	Variable
61	Literal
62	Operation	operator: 64 operand: 66
63	Literal
64	Literal
65	ExprTuple	66
66	Variable