In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, l, defaults
from proveit.logic import Forall, InSet, NotEquals, Set
from proveit.numbers import Integer, Mult
from proveit.physics.quantum.QPE import (
_b_floor, _best_floor_is_int, _b_round,
_best_round_def, _best_round_is_int, _delta_b,
_delta_b_is_real, _scaled_delta_b_not_eq_nonzeroInt,
_two_pow_t, _two_pow_t_is_nat_pos)
In [2]:
%proving _delta_b_not_eq_scaledNonzeroInt
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_delta_b_not_eq_scaledNonzeroInt:
(see dependencies)
_delta_b_not_eq_scaledNonzeroInt:
(see dependencies)
In [3]:
defaults.assumptions = _delta_b_not_eq_scaledNonzeroInt.all_conditions()
defaults.assumptions: 
In [4]:
_scaled_delta_b_not_eq_nonzeroInt
In [5]:
all_scaled_deltas_ne_ell_inst = (
_scaled_delta_b_not_eq_nonzeroInt.instantiate())
all_scaled_deltas_ne_ell_inst: 
, 
, 
⊢ 
, 
, 
⊢ 
In [6]:
_two_pow_t_is_nat_pos
In [7]:
_delta_b_is_real
In [8]:
_best_round_is_int
In [9]:
_best_floor_is_int
In [10]:
all_b_in_best_set_are_int = (
Forall(b, InSet(b, Integer),
domain=Set(_b_floor, _b_round)).prove())
all_b_in_best_set_are_int: ⊢ 
In [11]:
all_b_in_best_set_are_int.instantiate()
In [12]:
_delta_b_is_real.instantiate()
In [13]:
all_scaled_deltas_ne_ell_inst.divide_both_sides(_two_pow_t)
, , ⊢ 
In [14]:
%qed
Out[14]:
