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)
_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: ⊢ 
In [18]:
%qed
Out[18]:
