Proof of proveit.physics.quantum.QPE._precision_guarantee_lemma_01 theorem¶

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit.logic import Equals
from proveit.numbers import two, Add, Exp, frac, Mult, Neg
from proveit.physics.quantum.QPE import (
        _e_value_ge_two, _eps, _eps_in_interval, _n,
        _n_in_natural_pos, _t, _t_in_natural_pos, _t_req )

%proving _precision_guarantee_lemma_01

(0) We acknowledge a few axioms critical for the development further below:¶

display(_eps_in_interval)
display(_t_req)
display(_e_value_ge_two)

(1) We first develop a lower bound on the difference $(t-n)$.¶

from proveit.numbers import one, greater_eq, subtract
_t_minus_n_lb_01 = greater_eq(subtract(_t, _n), _t_req.rhs.operands[1]).prove()

# follow up here with a Ceil method to perform this and next step
from proveit.numbers.rounding import ceil_x_ge_x
ceil_x_ge_x

from proveit import x
_x_sub = _t_minus_n_lb_01.rhs.operand
_t_minus_n_lb_02 = ceil_x_ge_x.instantiate({x: _x_sub})

_t_minus_n_lb_03 = _t_minus_n_lb_01.apply_transitivity(_t_minus_n_lb_02)

(2) We then use that lower bound on $(t-n)$ to deduce a lower bound for our original expression:¶

bound_03 = _precision_guarantee_lemma_01.lhs.deduce_bound(_t_minus_n_lb_03)

(3) Process the lower bound¶

Now we perform some algebraic manipulation of that lower bound, trying to rewrite the lower bound in the form $1 - \epsilon(\frac{f(\epsilon)}{g(\epsilon)})$. The steps are labeled as sub-scripts of bound_03 because we're not deriving a new bound, just processing the bound we already have.

bound_03_01 = bound_03.inner_expr().rhs.operands[1].operand.denominator.distribute(1)

bound_03_02 = (
    bound_03_01.inner_expr().rhs.operands[2].operand.denominator.
    operands[0].substitute(Exp(two, two)))

bound_03_03 = (
    bound_03_02.inner_expr().rhs.operands[2].operand.denominator.
    common_power_extract(exp_factor=two))

bound_03_04 = (
    bound_03_03.inner_expr().rhs.operands[2].operand.denominator.
    base.distribute(1))

temp_multiplier = bound_03_04.rhs.operands[1].operand.denominator
bound_03_05 = bound_03_04.inner_expr().rhs.operands[1].operand.top_and_bottom_multiply(temp_multiplier)

with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    bound_03_06 = bound_03_05.inner_expr().rhs.associate(1,2)

bound_03_07 = bound_03_06.inner_expr().rhs.operands[1].operand.simplify()

bound_03_08 = (bound_03_07.inner_expr().rhs.operands[1].
                  operand.top_and_bottom_multiply(Exp(_eps, two)))

bound_03_09 = bound_03_08.inner_expr().rhs.operands[1].operand.factor(_eps)

bound_03_10 = bound_03_09.inner_expr().rhs.operands[1].operand.operands[1].numerator.distribute(1)

bound_03_11 = bound_03_10.inner_expr().rhs.operands[1].operand.operands[1].denominator.common_power_extract(exp_factor=2)

bound_03_12 = bound_03_11.inner_expr().rhs.operands[1].operand.operands[1].denominator.base.distribute(1)

(4) Bound the fractional component¶

Now we focus on the fraction in the rhs of that bound, showing that the fraction is in fact positive and less than 1. Some of this section can eventually be replaced with a more general Add.factorization() case for the factoring of polynomial-like Add expressions.

from proveit.numbers import zero, four, greater
bound_04 = greater(Add(Mult(four, _eps), one), zero).prove()

bound_05 = greater(Mult(_eps, Add(Mult(four, _eps), one)), zero).prove()

bound_05_01 = bound_05.inner_expr().lhs.distribute(1)

from proveit.numbers import three
bound_06 = greater(Add(Mult(four, Exp(_eps, two)), Mult(four, _eps), one),
        Add(Mult(three, _eps), one)).prove()

equality_01 = (
    Mult(Add(Mult(two, _eps), one), Add(Mult(two, _eps), one)).
    simplification().reversed())

equality_02 = equality_01.inner_expr().rhs.distribute(1)

equality_03 = equality_02.inner_expr().rhs.operands[0].distribute(1)

bound_07 = bound_06.inner_expr().lhs.substitute(equality_03.lhs)

bound_08 = bound_07.divide_both_sides(bound_07.lhs)

(5) Finish up¶

Now we can feed that bound above into the deduce_bound() method to find a bound on the earlier-derived bound $1 - \epsilon(\frac{f(\epsilon)}{g(\epsilon)})$

bound_09 = bound_03_12.rhs.deduce_bound(bound_08.reversed())

_precision_guarantee_lemma_01 may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.physics.quantum.QPE._precision_guarantee_lemma_01 has been proven.

	step type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
2	instantiation	4, 570, 5, 6, 7	⊢
	: , : , :
3	instantiation	466, 8, 9	⊢
	: , : , :
4	conjecture		⊢
	proveit.numbers.addition.strong_bound_via_right_term_bound
5	instantiation	566, 556	⊢
	:
6	instantiation	566, 11	⊢
	:
7	instantiation	10, 11, 556, 12	⊢
	: , :
8	instantiation	200, 13, 14	⊢
	: , : , :
9	instantiation	248, 591, 588, 524, 150, 525, 543, 551, 313, 15^, 29^	⊢
	: , : , : , : , : , :
10	conjecture		⊢
	proveit.numbers.negation.negated_strong_bound
11	instantiation	323, 556, 17	⊢
	: , :
12	instantiation	16, 556, 17, 570, 18, 557, 164^*	⊢
	: , : , :
13	instantiation	466, 19, 20	⊢
	: , : , :
14	instantiation	203, 543, 277, 585	⊢
	: , : , :
15	instantiation	231, 543, 551	⊢
	: , :
16	conjecture		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
17	instantiation	351, 130, 49, 34	⊢
	: , :
18	instantiation	21, 49, 130, 22, 23, 24^*	⊢
	: , : , :
19	instantiation	466, 25, 26	⊢
	: , : , :