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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, l, m, defaults
from proveit.logic import InSet
from proveit.numbers import Abs, Integer, Real, subtract, Mult, Exp
from proveit.physics.quantum.QPE import ModAdd
from proveit.physics.quantum.QPE import (
        _alpha_are_complex, _alpha_summed,
        _b_floor, _best_floor_is_int, _delta_b_floor_diff_in_interval,
        _delta_b_is_real, _delta_b_not_eq_scaledNonzeroInt, _mod_add_closure,
        _scaled_abs_delta_b_floor_diff_interval, _scaled_delta_b_not_eq_nonzeroInt,
        _scaled_delta_b_floor_in_interval, _non_int_delta_b_diff,
        _t_in_natural_pos, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos)

%proving _alpha_sqrd_upper_bound

defaults.assumptions = _alpha_sqrd_upper_bound.all_conditions()

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

Exp.change_simplification_directives(factor_numeric_rational=True)

(1) Some basic domain information needed throughout the proof¶

_two_pow_t_minus_one_is_nat_pos

_scaled_delta_b_floor_in_interval

InSet(subtract(_scaled_delta_b_floor_in_interval.element, l), Real).prove()

_scaled_abs_delta_b_floor_diff_interval.instantiate()

_delta_b_not_eq_scaledNonzeroInt.instantiate({b: _b_floor})

_delta_b_floor_diff_in_interval.instantiate()

_scaled_delta_b_not_eq_nonzeroInt.instantiate({b: _b_floor})

_best_floor_is_int

_b_floor_plus_ell_in_interval = _mod_add_closure.instantiate({a: _b_floor, b:l})

_delta_b_is_real.instantiate({b: _b_floor})

_two_pow_t_is_nat_pos

_b_floor_plus_ell_in_interval.derive_element_in_integer()

_alpha_are_complex.instantiate({m: ModAdd(_b_floor, l)})

(2) Starting Point: `_alpha_summed`¶

_alpha_summed_inst = _alpha_summed.instantiate()

(3) Take Abs() of Both Sides & Allow Auto-Simplification of the Denominator¶

# We want to temporarily preserve the resulting numerator
# so it isn't auto-simplified, so we first give it a convenient label
numerator = Abs(_alpha_summed_inst.rhs.factors[1].numerator)

_non_int_delta_b_diff

_non_int_delta_b_diff.instantiate({b:_b_floor})

# In applying the Abs() to both sides, we avoid the auto-simplifying
# chord-length simplification in the numerator by using 'preserve_expr':
_alpha_summed_inst_abs = _alpha_summed_inst.abs_both_sides(preserve_expr=numerator)

_alpha_summed_inst_abs_dist = (
    _alpha_summed_inst_abs.inner_expr().rhs.distribute(preserve_expr=numerator))

(4) Bound the numerator and the denominator of the fraction.¶

4(a) Use a triangle inequality for the numerator.¶

numer_bound = numerator.deduce_triangle_bound()

4(b) Bound the $y = \sin(\theta)$ in the denominator by the chord $y = (\frac{2}{\pi}\theta)$¶

denom_sin = _alpha_summed_inst_abs_dist.rhs.denominator.factors[2]

denom_sin_bound = denom_sin.deduce_linear_bound()

sin_bound_is_positive = denom_sin_bound.rhs.deduce_positive()

denom_sin_is_positive = denom_sin_bound.apply_transitivity(sin_bound_is_positive)

denominator = _alpha_summed_inst_abs_dist.rhs.denominator

denom_bound = denominator.deduce_bound(denom_sin_bound)

denom_is_positive = denominator.deduce_bound(denom_sin_is_positive)

(5) Now we use the numerator and denominator bounds to bound $|\alpha_{b_{f}\oplus\ell}|$¶

# recall from earlier:
_alpha_summed_inst_abs_dist

rhs_bound = _alpha_summed_inst_abs_dist.rhs.deduce_bound([numer_bound, denom_bound])

alpha_upper_bound_01 = _alpha_summed_inst_abs_dist.apply_transitivity(rhs_bound)

(6) Simplify and square both sides¶

alpha_upper_bound_02 = alpha_upper_bound_01.inner_expr().rhs.denominator.associate(1, 2)

alpha_upper_bound_03 = (
    alpha_upper_bound_02.inner_expr().rhs.denominator.operands[1].distribute(1))

with Exp.temporary_simplification_directives() as tmp_directives:
    tmp_directives.distribute_exponent=True
    alpha_upper_bound_03.square_both_sides()

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	576, 2, 3	, ⊢
	: , : , :
2	instantiation	4, 684, 5, 6, 7, 8, 9^*	, ⊢
	: , : , :
3	instantiation	667, 10	⊢
	: , : , :
4	conjecture		⊢
	proveit.numbers.exponentiation.exp_pos_lesseq
5	instantiation	705, 500, 21	⊢
	: , : , :
6	instantiation	428, 657, 24, 16	, ⊢
	: , :
7	instantiation	343, 11, 12	, ⊢
	: , :
8	instantiation	13, 696	⊢
	:
9	instantiation	14, 642, 15, 696, 16, 17^, 18^	, ⊢
	: , : , :
10	instantiation	667, 19	⊢
	: , : , :
11	instantiation	20, 21	⊢
	:
12	instantiation	576, 22, 23	, ⊢
	: , : , :
13	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
14	conjecture		⊢
	proveit.numbers.exponentiation.posnat_power_of_quotient
15	instantiation	705, 683, 24	⊢
	: , : , :
16	instantiation	418, 704, 25, 611, 26	, ⊢
	: , :
17	instantiation	27, 677	⊢
	:
18	instantiation	28, 677, 29, 696, 30^, 31^	⊢
	: , : , :
19	instantiation	32, 413, 702, 668^, 33^	⊢
	: , :
20	conjecture		⊢

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

(1) Some basic domain information needed throughout the proof¶

(2) Starting Point: _alpha_summed¶

(3) Take Abs() of Both Sides & Allow Auto-Simplification of the Denominator¶

(4) Bound the numerator and the denominator of the fraction.¶

4(a) Use a triangle inequality for the numerator.¶

4(b) Bound the $y = \sin(\theta)$ in the denominator by the chord $y = (\frac{2}{\pi}\theta)$¶

(5) Now we use the numerator and denominator bounds to bound $|\alpha_{b_{f}\oplus\ell}|$¶

(6) Simplify and square both sides¶

(2) Starting Point: `_alpha_summed`¶