In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, defaults
from proveit.logic import NotEquals
from proveit.numbers import zero, one, two, pi, Abs, frac, Neg
from proveit.physics.quantum.QPE import (
_b_floor, _delta_b_floor_diff_in_interval,
_delta_b_not_eq_scaledNonzeroInt, _two_pow_t_minus_one_is_nat_pos)
In [2]:
%proving _scaled_abs_delta_b_floor_diff_interval
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_scaled_abs_delta_b_floor_diff_interval:
(see dependencies)
_scaled_abs_delta_b_floor_diff_interval:
(see dependencies)
In [3]:
defaults.assumptions = _scaled_abs_delta_b_floor_diff_interval.all_conditions()
defaults.assumptions: 
In [4]:
_two_pow_t_minus_one_is_nat_pos
In [5]:
defaults.assumptions[0].derive_element_in_integer()
In [6]:
_delta_b_floor_diff_in_interval
In [7]:
_delta_b_floor_diff_in_interval_inst = _delta_b_floor_diff_in_interval.instantiate()
_delta_b_floor_diff_in_interval_inst: 
⊢ 
⊢ 
In [8]:
delta_diff = _delta_b_floor_diff_in_interval_inst.element
delta_diff: 
In [9]:
_delta_b_floor_diff_in_interval_inst.domain.deduce_relaxed_membership(delta_diff)
In [10]:
# for convenience, label the abs value component
abs_val_delta_diff = Abs(delta_diff)
abs_val_delta_diff: 
In [11]:
abs_val_leq_one_half = abs_val_delta_diff.deduce_weak_upper_bound(frac(one, two))
abs_val_leq_one_half: ⊢ 
⊢ 
In [12]:
upper_bound = (
abs_val_leq_one_half.left_mult_both_sides(pi).
inner_expr().rhs.distribute())
upper_bound: ⊢ 
⊢ 
In [13]:
_delta_b_not_eq_scaledNonzeroInt.instantiate({b: _b_floor})
, 
⊢ 
In [14]:
NotEquals(delta_diff, zero).prove()
, ⊢ 
In [15]:
%qed
Out[15]:
