# Proof of proveit.physics.quantum.QPE._sample_space_bijection theorem¶

In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults
from proveit import f, m, n, x, y, A
from proveit.logic import InSet, NotEquals
from proveit.logic.sets.functions.bijections import bijective_by_uniqueness
from proveit.physics.quantum.QPE import (_t, _s, _t_in_natural_pos, _s_in_nat_pos,
_sample_space_def)

In [2]:
%proving _sample_space_bijection

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_sample_space_bijection:
(see dependencies)
In [3]:
_sample_space_def


We want to use $\Omega$ as our shorthand for the sample space:

In [4]:
defaults.replacements = set([_sample_space_def.derive_reversed()])

defaults.replacements:
In [5]:
lambda_map = _sample_space_bijection.element

lambda_map:
In [6]:
domain = _sample_space_bijection.domain.domain

domain:

In order to show that the image of the map is a bijection, we want to show that distinct elements of the domain map to distinct quantum circuits.

In [7]:
assumptions = [InSet(m, domain), InSet(n, domain), NotEquals(m, n)]

assumptions:
In [8]:
NotEquals(lambda_map.apply(m), lambda_map.apply(n)).prove(
assumptions=assumptions)

, ,  ⊢
In [9]:
bijective_by_uniqueness

In [10]:
bijective_by_uniqueness.instantiate(
{f:lambda_map, A:domain, x:m, y:n}).derive_consequent()

_sample_space_bijection has been proven.  Now simply execute "%qed".

In [11]:
%qed

proveit.physics.quantum.QPE._sample_space_bijection has been proven.

Out[11]:
step typerequirementsstatement
0modus ponens1, 2
1instantiation3, 4*, 5*
: , : , : , :
2generalization6
3conjecture
proveit.logic.sets.functions.bijections.bijective_by_uniqueness
4instantiation7, 8*, ,  ⊢
: , :
5instantiation9, 10*
: , :
6axiom
proveit.logic.booleans.true_axiom
7axiom
proveit.logic.equality.not_equals_def
8instantiation11, 12, ,  ⊢
:
9axiom
proveit.logic.sets.functions.images.set_image_def
10instantiation133, 13
: , :
11axiom
proveit.logic.booleans.eq_true_intro
12instantiation14, 15, ,  ⊢
: , :
13axiom
proveit.physics.quantum.QPE._sample_space_def
14theorem
proveit.logic.equality.unfold_not_equals
15modus ponens16, 17, ,  ⊢
16instantiation18, 69, 136, 19, 20, 21, 22, 23, 24, 25
: , : , : , :
17instantiation26, 69, 27, 28, 29, ,  ⊢
: , : , :
18conjecture
proveit.physics.quantum.circuits.qcircuit_neq
19instantiation117, 30, 32, 33
: , : , : , :
20instantiation117, 31, 32, 33
: , : , : , :
21instantiation117, 34, 77, 37
: , : , : , :
22instantiation117, 35, 77, 37
: , : , : , :
23instantiation117, 36, 77, 37
: , : , : , :
24instantiation117, 75, 77, 37
: , : , : , :
25instantiation117, 76, 77, 37
: , : , : , :
26conjecture
proveit.core_expr_types.expr_arrays.varray_neq_via_any_elem_neq
27instantiation179
: , : , : , :
28instantiation179
: , : , : , :
29instantiation38, 127, 200, 39, 201, 40, 41, 42, 43, 44, ,  ⊢
: , : , : , : , :
30instantiation89, 46, 45, 48, 49, 92, 93, 57, 50*
: , : , : , :
31instantiation89, 46, 47, 48, 49, 92, 93, 57, 50*
: , : , : , :
32instantiation133, 51
: , :
33instantiation133, 52
: , :
34instantiation89, 90, 53, 159, 148, 92, 93, 108*, 151*
: , : , : , :
35instantiation89, 90, 54, 55, 56, 92, 57, 108*, 84*
: , : , : , :
36instantiation89, 90, 58, 159, 148, 92, 93, 108*, 151*
: , : , : , :
37instantiation133, 59
: , :
38conjecture
proveit.logic.booleans.disjunction.or_if_any
39instantiation153
: , : , :
40instantiation207
: , :
41instantiation207
: , :
42instantiation207
: , :
43instantiation207
: , :
44instantiation60, 61, 62, 63, 64, 65, ,  ⊢
: , : , :
45instantiation97
: , : , : , : , : , : , : , :
46conjecture
proveit.numbers.numerals.decimals.posnat8
47instantiation97
: , : , : , : , : , : , : , :
48instantiation97
: , : , : , : , : , : , : , :
49instantiation97
: , : , : , : , : , : , : , :
50instantiation220, 66, 67
: , : , :
51instantiation156, 257, 255, 200, 148, 201, 132, 193, 181
: , : , : , : , : , :
52instantiation68, 69, 70, 111
: , : , :
53instantiation216
: , :
54instantiation216
: , :
55instantiation216
: , :
56instantiation216
: , :
57instantiation109, 163, 84
: , : , :
58instantiation216
: , :
59instantiation110, 111
: , :
60conjecture
proveit.core_expr_types.tuples.tuple_neq_via_any_elem_neq
61instantiation224, 71, 72
: , :
62instantiation220, 73, 74
: , : , :
63instantiation117, 75, 77, 78
: , : , : , :
64instantiation117, 76, 77, 78
: , : , : , :
65instantiation95, 167, 163, 200, 142, 139, 201, 79, ,  ⊢
: , : , : , : , : , :
66instantiation80, 81, 82, 83, 108, 151, 84
: , : , : , :
67instantiation117, 85, 86, 87
: , : , : , :
68conjecture
proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
69conjecture
proveit.numbers.numerals.decimals.posnat4
70instantiation166, 215
: , :
71instantiation109, 260, 108
: , : , :
72instantiation109, 223, 151
: , : , :
73instantiation239, 108
: , : , :
74instantiation239, 151
: ,