In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit.physics.quantum.QPE import (
_Omega, _fail_def, _sample_space_def, _sample_space_bijection, _Omega_is_sample_space)
In [2]:
%proving _pfail_in_real
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_pfail_in_real:
(see dependencies)
_pfail_in_real:
(see dependencies)
In [3]:
defaults.assumptions = _pfail_in_real.conditions
defaults.assumptions: 
In [4]:
pfail = _fail_def.instantiate()
pfail: 
⊢ 
⊢ 
In [5]:
pfail_as_event_prob = pfail.inner_expr().rhs.define(_Omega)
pfail_as_event_prob: ⊢ 
⊢ 
In [6]:
fail_event = pfail_as_event_prob.rhs.operand
fail_event: 
In [7]:
_sample_space_def
In [8]:
from proveit.logic import SubsetEq
SubsetEq(fail_event, _sample_space_def.rhs).prove()
In [9]:
event_prob_in_domain = pfail_as_event_prob.rhs.deduce_in_prob_domain(_sample_space_def.rhs)
event_prob_in_domain: ⊢ 
In [10]:
pfail_as_event_prob.sub_left_side_into(event_prob_in_domain)
In [11]:
%qed
Out[11]:
