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

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

from proveit import defaults
from proveit import a, b, f, g, l, m, n, x, X, Y, Omega
from proveit.logic import InSet
from proveit.numbers import Natural
from proveit.statistics import sample_space_via_bijections
from proveit.physics.quantum import var_ket_psi, Ket
from proveit.physics.quantum.circuits import (
born_rule_on_register, register_meas_sample_space, register_meas_bijection)
from proveit.physics.quantum.QPE import (
_t, _t_in_natural_pos, _Psi_ket, _Psi_ket_is_normalized_vec,
_alpha_m_def,
_Omega, _sample_space_def, _sample_space_bijection, _outcome_prob)

In [2]:
%proving _Omega_is_sample_space

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

In [4]:
_outcome_prob

In [5]:
defaults.assumptions = _outcome_prob.conditions

defaults.assumptions:
In [6]:
_alpha_m_def

In [7]:
alpha_m_replacement = _alpha_m_def.instantiate().derive_reversed()

alpha_m_replacement:
In [8]:
born_rule_on_register

In [9]:
Psi_meas_prob = born_rule_on_register.instantiate({m:_t, var_ket_psi:_Psi_ket, n:m},
replacements=[alpha_m_replacement])

Psi_meas_prob:
In [10]:
Psi_meas_is_sample_space = register_meas_sample_space.instantiate({m:_t, var_ket_psi:_Psi_ket, n:m})

Psi_meas_is_sample_space:
In [11]:
Psi_meas_bijection = register_meas_bijection.instantiate({m:_t, var_ket_psi:_Psi_ket, n:m}).with_wrapping_at()

Psi_meas_bijection:
In [12]:
_sample_space_bijection

In [13]:
domain = _sample_space_bijection.domain.domain

domain:
In [14]:
_sample_space_def

In [15]:
sample_space_via_bijections

In [16]:
Psi_meas_prob

In [17]:
impl = sample_space_via_bijections.instantiate(
{Omega:Psi_meas_is_sample_space.element, X:domain, Y:_Omega,
f:Psi_meas_bijection.element, g:_sample_space_bijection.element, x:m},
replacements=[Psi_meas_prob, _outcome_prob.instantiate()],
assumptions=[])

impl:
_Omega_is_sample_space has been proven.  Now simply execute "%qed".

In [18]:
%qed

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

Out[18]:
step typerequirementsstatement
0modus ponens1, 2
1instantiation3, 4, 5, 6, 7*, 8*, 9*
: , : , : , : , : , :
2generalization10
3conjecture
proveit.statistics.sample_space_via_bijections
4instantiation11, 16, 13, 14
: , : , :
5instantiation12, 16, 13, 14
: , : , :
6conjecture
proveit.physics.quantum.QPE._sample_space_bijection
7instantiation15, 16, 28, 23, 17*
: , : , :
8instantiation18, 28
:
9instantiation19, 20
:
10axiom
proveit.logic.booleans.true_axiom
11conjecture
proveit.physics.quantum.circuits.register_meas_sample_space
12conjecture
proveit.physics.quantum.circuits.register_meas_bijection
13instantiation21, 23
: , :
14instantiation22, 23
: , :
15conjecture
proveit.physics.quantum.circuits.born_rule_on_register
16axiom
proveit.physics.quantum.QPE._t_in_natural_pos
17instantiation24, 25
: , :
18conjecture
proveit.physics.quantum.QPE._outcome_prob
19axiom
proveit.logic.booleans.eq_true_intro
20instantiation26
:
21theorem
proveit.logic.booleans.conjunction.left_from_and
22theorem
proveit.logic.booleans.conjunction.right_from_and
23conjecture
proveit.physics.quantum.QPE._Psi_ket_is_normalized_vec
24theorem
proveit.logic.equality.equals_reversal
25instantiation27, 28
:
26axiom
proveit.logic.equality.equals_reflexivity
27axiom
proveit.physics.quantum.QPE._alpha_m_def
28assumption
*equality replacement requirements