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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, e, f, i, l, x, defaults, Lambda
from proveit.logic import Equals, InSet, NotEquals
from proveit.numbers import (
    zero, one, two, four, Add, Exp, frac, greater, greater_eq,
    Less, Mult, NaturalPos, Neg, Real, RealPos, subtract)
from proveit.numbers.functions import MonDecFuncs
from proveit.physics.quantum.QPE import (
    _t_in_natural_pos, _two_pow_t, _two_pow_t_minus_one_is_nat_pos, _phase_is_real,
    _mod_add_def, _b_floor, _best_floor_is_int, _delta_b_floor, _delta_b_is_real, 
    _scaled_delta_b_floor_in_interval, _diff_l_scaled_delta_floor)
from proveit.physics.quantum.QPE.phase_est_ops import Psuccess, Pfail, ModAdd

%proving _failure_upper_bound

defaults.assumptions = _failure_upper_bound.conditions

(1) Import & Instantiate the `_failure_upper_bound_lemma`¶

from proveit.physics.quantum.QPE import _failure_upper_bound_lemma
_failure_upper_bound_lemma

_failure_upper_bound_lemma_inst = (
        _failure_upper_bound_lemma.instantiate(preserve_expr=Neg(Add(e, one))))

(2) Establish some convenient labels for important expressions¶

first_sum = _failure_upper_bound_lemma_inst.rhs.operands[1].operands[0]

second_sum = _failure_upper_bound_lemma_inst.rhs.operands[1].operands[1]

the_summand = first_sum.summand

first_sum_conditions = first_sum.conditions[0]

second_sum_conditions = second_sum.conditions[0]

(3) Some Initial Bounding of the Summand Denominator and variables $\ell$ and $e$¶

_scaled_delta_b_floor_in_interval

_delta_b_is_real.instantiate({b:_b_floor})

# Automatic incidental derivation, but want to label the result for later use
scaled_delta_lower_bound = _scaled_delta_b_floor_in_interval.derive_element_lower_bound()

# Automatic incidental derivation, but want to label the result for later use
scaled_delta_upper_bound = _scaled_delta_b_floor_in_interval.derive_element_upper_bound()

neg_scaled_delta_lower_bound = scaled_delta_upper_bound.left_mult_both_sides(Neg(one))

neg_scaled_delta_upper_bound = scaled_delta_lower_bound.left_mult_both_sides(Neg(one))

_diff_l_scaled_delta_floor.deduce_bound(neg_scaled_delta_lower_bound,
        assumptions=defaults.assumptions + (first_sum_conditions,))

# For the 1st Summation
diff_l_scaled_delta_upper_bound = _diff_l_scaled_delta_floor.deduce_bound(
        neg_scaled_delta_upper_bound.reversed(),
        assumptions=defaults.assumptions + (first_sum_conditions,))

# For the 2nd Summation
diff_l_scaled_delta_upper_bound_2 = _diff_l_scaled_delta_floor.deduce_bound(
        neg_scaled_delta_lower_bound,
        assumptions=defaults.assumptions + (second_sum_conditions,))

(4) Bound on the First Summand and First Sum¶

We can find an $\ell$-dependent upper bound on the first summand, then an upper bound on the first summation.

first_summand_bound_02 = the_summand.deduce_bound(scaled_delta_lower_bound.reversed(),
        assumptions=defaults.assumptions + (first_sum_conditions,))

first_summand_bound_generalized = first_summand_bound_02.generalize((l), conditions=[first_sum_conditions])

first_sum_bound = first_sum.deduce_bound(first_summand_bound_generalized)

(5) Bound on the Second Summand and Second Sum¶

We can find an $\ell$-dependent upper bound on the second summand, then an upper bound on the second summation.

second_summand_bound_02 = the_summand.deduce_bound(diff_l_scaled_delta_upper_bound_2,
        assumptions=defaults.assumptions + (second_sum_conditions,))

second_summand_bound_02_relaxed = second_summand_bound_02.derive_relaxed()

second_summand_bound_generalized = second_summand_bound_02.generalize([l], conditions=[second_sum_conditions])

second_summand_bound_relaxed_generalized = second_summand_bound_02_relaxed.generalize([l], conditions=[second_sum_conditions])

second_sum_bound = second_sum.deduce_bound(second_summand_bound_relaxed_generalized)

(6) Bound on the Sum of Summations¶

Now we're ready to invoke our deduce_bound() method utilizing the bounds we've established on each separate summation.
The following three steps correspond to the transition from (5.30) to (5.31) in Nielsen & Chuang (pg 224):

_failure_upper_bound_lemma_inst_bound_01 = _failure_upper_bound_lemma_inst.rhs.deduce_bound(first_sum_bound)

_failure_upper_bound_lemma_inst_bound_02 = _failure_upper_bound_lemma_inst_bound_01.rhs.deduce_bound(second_sum_bound)

_failure_upper_bound_lemma_inst_bound_03 = (
    _failure_upper_bound_lemma_inst_bound_01.apply_transitivity(_failure_upper_bound_lemma_inst_bound_02))

Next, shift the index of the second summation to create identical summands in each of the summations:

_failure_upper_bound_lemma_inst_bound_04 = (
    _failure_upper_bound_lemma_inst_bound_03.inner_expr().rhs.operands[1].
    operands[1].shift(Neg(one)))

Then negate and flip the order of indices on the first summation (possible because the summand is an even function).

_failure_upper_bound_lemma_inst_bound_05 = (
    _failure_upper_bound_lemma_inst_bound_04.inner_expr().rhs.operands[1].
    operands[0].negate_index())

Now we're ready to split off the first element of the second summation.
Nielsen & Chuang originally split off the first element of the first summation, eventually leading to a bound requiring $e \ge 2$.
Instead, we split off the first term of the second summation, allowing us to eventually derive a bound valid for $e \ge 1$.
In doing so, the resulting expression is auto-simplified to combine the two resulting like-summations:

Mult.change_simplification_directives(distribute_numeric_rational=True)
bound_07 = _failure_upper_bound_lemma_inst_bound_05.inner_expr().rhs.factors[1].operands[1].split_first()

sum_bound_as_integral = bound_07.rhs.terms[0].factors[1].upper_bound_as_integral()

integral_bound = sum_bound_as_integral.rhs.bound_via_upper_limit_bound()

bound_07.rhs.deduce_bound(sum_bound_as_integral.apply_transitivity(integral_bound))

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	469, 2, 3	⊢
	: , : , :
2	instantiation	79, 4, 5	⊢
	: , : , :
3	instantiation	243, 525, 6, 7, 8, 9	⊢
	: , : , : , :
4	instantiation	79, 10, 11	⊢
	: , : , :
5	instantiation	147, 12, 13, 14, 15	⊢
	: , : , :
6	instantiation	459	⊢
	: , :
7	instantiation	459	⊢
	: , :
8	instantiation	205, 16	⊢
	: , :
9	instantiation	205, 17	⊢
	: , :
10	instantiation	18, 514	⊢
	:
11	instantiation	469, 19, 20, 21^*	⊢
	: , : , :
12	instantiation	22, 179, 204	⊢
	: , :
13	instantiation	22, 175, 314	⊢
	: , :
14	instantiation	22, 175, 23	⊢
	: , :
15	instantiation	114, 175, 314, 23, 24, 25	⊢
	: , : , :
16	instantiation	29, 26, 27, 28	⊢
	: , : , : , :
17	instantiation	29, 30, 31, 32	⊢
	: , : , : , :
18	conjecture		⊢
	proveit.physics.quantum.QPE._failure_upper_bound_lemma
19	instantiation	469, 33, 34	⊢
	: , : , :
20	instantiation	35, 497, 479, 133	⊢