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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, m, theta, defaults
from proveit.logic import NotEquals, InSet
from proveit.numbers import (
        zero, one, two, pi, Abs, Add, Complex, frac, IntervalOC, Less, greater, Mult, Exp)
# QPE common exprs
from proveit.physics.quantum.QPE import _b_round, _delta_b_round, _t, _two_pow_t
 # QPE theorems
from proveit.physics.quantum.QPE import (
        _alpha_m_mod_as_geometric_sum, _alpha_are_complex, _best_round_is_int,
        _delta_b_is_real, _delta_b_is_zero_or_non_int,
        _phase_from_best_with_delta_b, _scaled_delta_b_round_in_interval,
        _t_in_natural_pos, _two_pow_t_is_nat_pos)
from proveit.trigonometry import Sin

%proving _best_guarantee_delta_nonzero

defaults.assumptions = [_best_guarantee_delta_nonzero.antecedent]

Keep the factor of $2$ from combining with $2^t$ in the steps below:

Exp.change_simplification_directives(factor_numeric_rational=True)

alpha_index = _best_guarantee_delta_nonzero.consequent.lhs.base.operand.index

Start from $\alpha_{m~\textrm{mod}~2^t}$ expressed as a geometric sum, instantiated with $m:b_r$¶

_alpha_m_mod_as_geometric_sum

_alpha_eq_01 = (
        _alpha_m_mod_as_geometric_sum.instantiate({m: _b_round}))

Put this in terms of $\delta_{b_r}$¶

_phase_from_best_with_delta_b

_phase_from_best_with_delta_b_inst = (
        _phase_from_best_with_delta_b.instantiate({b: _b_round}))

# We want to know that _delta_b_round and 2^t are real so that
# auto-simplification will manifest in the substitute() step further below
_delta_b_is_real

_delta_b_is_real.instantiate({b: _b_round})

with Exp.temporary_simplification_directives() as tmp_directives:
    tmp_directives.reduce_double_exponent = False # don't simplify k double-exponent
    _alpha_eq_02 = (
        _alpha_eq_01.inner_expr().rhs.factors[1].summand.base.exponent.
        factors[3].operands[0].substitute(_phase_from_best_with_delta_b_inst.rhs))

Evaluate the Finite Geometric Sum¶

To evaluate the summation as a finite geometric sum, we need to establish that the constant ratio $e^{2\pi i \delta_{b_r}} \neq 1$ which is automatically proven given $\delta_{b_r} \notin \mathbb{Z}$.

_delta_b_is_zero_or_non_int

_delta_b_is_zero_or_non_int_inst = _delta_b_is_zero_or_non_int.instantiate({b: _b_round})

_delta_b_round_non_int = _delta_b_is_zero_or_non_int_inst.derive_right_if_not_left()

We can then evaluate the sum using the standard formula for a finite geometric sum:

_alpha_eq_03 = _alpha_eq_02.inner_expr().rhs.factors[1].geom_sum_reduce()

Take the Magnitude (Abs) of Both Sides¶

Pre-requisites to allow auto-simplification to go through¶

Establish that the $\alpha$ expression is in the Complex numbers.

_alpha_are_complex.instantiate({m:alpha_index})

Prove that $\pi |\delta_{b_r}| \in \left(0, \frac{\pi}{2}\right)$ which is important to ensure the denominator is non-zero. Along the way, we prove $2^t \pi |\delta_{b_r}| \leq \frac{\pi}{2}$ which will be useful for bounding the numerator.

angle = Mult(pi, Abs(_delta_b_round))

Less(zero, angle).prove()

scaled_abs_bound = (Abs(_scaled_delta_b_round_in_interval.element).deduce_weak_upper_bound(frac(one, two))
         .inner_expr().lhs.simplify())

Close enough to $2^t \pi |\delta_{b_r}| \leq \frac{\pi}{2}$ (the translation occurs automatically via canonical forms):

two_pow_t_times_angle__bound = scaled_abs_bound.left_mult_both_sides(pi)

two_pow_t_bound = _two_pow_t.deduce_bound(_t_in_natural_pos.derive_element_lower_bound())

two_pow_t_times_angle__bound.lhs.deduce_bound(greater(_two_pow_t, one))

Less(angle, frac(pi, two)).prove()

Now take the absolute value on each side¶

with Mult.temporary_simplification_directives() as tmp_directives:
    # pull the 2^t to the front
    tmp_directives.order_key_fn = lambda factor : 0 if factor==_two_pow_t else 1
    _alpha_eq_04 = _alpha_eq_03.abs_both_sides()

Bound the numerator and the denominator¶

Bound the sin function in the denominator utilizing $\sin{\theta} < \theta$ for $\theta > 0$¶

denominator_sin_bound = _alpha_eq_04.rhs.factors[1].denominator.deduce_linear_upper_bound()

Bound the sin function in the numerator utilizing $\sin{\theta} \ge \frac{2}{\pi}(\theta)$ for $0 < \theta \le \frac{\pi}{2}$¶

numerator_sin_bound = _alpha_eq_04.rhs.factors[1].numerator.deduce_linear_lower_bound()

Apply these numerator and denominator bounds¶

rhs_bound = _alpha_eq_04.rhs.deduce_bound([numerator_sin_bound, denominator_sin_bound])

_alpha_ineq = _alpha_eq_04.apply_transitivity(rhs_bound)

Finally square both sides¶

_alpha_ineq.square_both_sides()

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

%qed

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

	step type	requirements	statement
0	deduction	1	⊢
1	instantiation	424, 2, 3	⊢
	: , : , :
2	instantiation	4, 622, 5, 6, 7, 8	⊢
	: , : , :
3	instantiation	466, 9, 10, 11	⊢
	: , : , : , :
4	conjecture		⊢
	proveit.numbers.exponentiation.exp_pos_less
5	instantiation	632, 538, 29	⊢
	: , : , :
6	instantiation	632, 333, 12	⊢
	: , : , :
7	instantiation	337, 13, 14	⊢
	: , :
8	instantiation	572, 627	⊢
	:
9	instantiation	280, 553, 15, 16, 17^*	⊢
	: , :
10	instantiation	566	⊢
	:
11	instantiation	409, 18	⊢
	: , :
12	instantiation	19, 35	⊢
	:
13	instantiation	20, 21	⊢
	:
14	instantiation	424, 22, 23	⊢
	: , : , :
15	instantiation	632, 621, 24	⊢
	: , : , :
16	instantiation	25, 479, 612, 420	⊢
	: , :
17	instantiation	62, 479, 622, 564, 420, 26^*	⊢
	: , : , :
18	instantiation	573, 27, 28	⊢
	: , : , :
19	conjecture		⊢
	proveit.numbers.absolute_value.abs_complex_closure
20	conjecture		⊢