In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit.physics.quantum.QPE import (
_b_floor,
_best_floor_def, _phase_in_interval, _phase_is_real, _two_pow_t_is_nat_pos)
In [2]:
%proving _best_floor_is_in_m_domain
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_best_floor_is_in_m_domain:
(see dependencies)
_best_floor_is_in_m_domain:
(see dependencies)
In [3]:
_best_floor_def
In [4]:
scaled_phase_floor = _best_floor_def.rhs
scaled_phase_floor: 
In [5]:
scaled_phase = _best_floor_def.rhs.operand
scaled_phase: 
In [6]:
from proveit.logic import InSet
from proveit.numbers import Integer
InSet(scaled_phase_floor, Integer).prove()
In [7]:
_phase_in_interval
In [8]:
_two_pow_t_is_nat_pos
In [9]:
_phase_upper_bound = _phase_in_interval.derive_element_upper_bound()
_phase_upper_bound: ⊢ 
In [10]:
_phase_lower_bound = _phase_in_interval.derive_element_lower_bound()
_phase_lower_bound: ⊢ 
In [11]:
scaled_phase_upper_bound = scaled_phase.deduce_bound([_phase_upper_bound])
scaled_phase_upper_bound: ⊢ 
In [12]:
scaled_phase_lower_bound = (
scaled_phase.deduce_bound(
[_phase_lower_bound.with_styles(direction='reversed')]))
scaled_phase_lower_bound: ⊢ 
In [13]:
scaled_phase_floor.deduce_bound([scaled_phase_upper_bound])
In [14]:
scaled_phase_floor.deduce_bound([scaled_phase_lower_bound])
In [15]:
%qed
Out[15]:
