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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b, k, l, m, defaults
from proveit.logic import Forall, InSet, Set
from proveit.numbers import two, pi, i, Add, Integer, Mult, Exp
from proveit.physics.quantum.QPE import ModAdd
from proveit.physics.quantum.QPE import (
        _alpha_m_mod_as_geometric_sum,
        _b_floor, _best_floor_is_int, _non_int_delta_b_diff, _delta_b_is_real,
        _phase_from_best_with_delta_b, _phase_is_real, _t_in_natural_pos,
        _two_pow_t, _two_pow_t_is_nat_pos, _two_pow_t_minus_one_is_nat_pos)

%proving _alpha_summed

defaults.assumptions = _alpha_summed.all_conditions()

Disable reducing double exponents for now and keep a factor of $2$ from combining with $2^t$ in the steps below:

Exp.change_simplification_directives(reduce_double_exponent=False)
Exp.change_simplification_directives(factor_numeric_rational=True)

_t_in_natural_pos

_two_pow_t_is_nat_pos

_two_pow_t_minus_one_is_nat_pos

To instantiate the _alpha_m_mod_as_geometric_sum theorem, we want $\ell \mapsto (b_f + \ell)$, but this requires that we establish that $(b_f+\ell) \in \mathbb{Z}$. This we accomplish by noting that $b_f$ is an integer.

_best_floor_is_int

_alpha_m_mod_as_geometric_sum

alpha_l_eq_01_alt = _alpha_m_mod_as_geometric_sum.instantiate({m: Add(_b_floor, l)})

$(b+\ell)\,\text{mod}\,2^t$ is the definition of $b \oplus \ell$, so we can clean up the $\alpha$ subscript/indexing on the lhs:

b_modadd_l__def = ModAdd(_b_floor, l).definition()

alpha_l_eq_02_alt = alpha_l_eq_01_alt.inner_expr().lhs.index.substitute(
    b_modadd_l__def.derive_reversed())

Next we substitute in for the phase $\varphi$ in terms of $b$ and $\delta_{b}$.

_phase_from_best_with_delta_b

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

# proactively recall _delta_b is real, so auto simplification will work
# as expected in the in next major step or two
_delta_b_is_real

_delta_b_is_real.instantiate({b:_b_floor})

Now we're ready to substitute back into our summation formula:

alpha_l_eq_03_alt = (
        alpha_l_eq_02_alt.inner_expr().rhs.factors[1].summand.
        base.exponent.factors[3].operands[0].
        substitute(_phase_from_best_with_delta_b_inst.rhs))

alpha_l_eq_04_alt = (
        alpha_l_eq_03_alt.inner_expr().rhs.factors[1].summand.
        base.exponent.factors[3].operands[2].operand.distribute())

We want to evaluate the summation as a finite geometric sum, but we need to establish that our exponential base $e^{2\pi i (\delta_{b} - \ell/{2^t})}$ is not equal to 1, which can be proven automatically given $\delta_{b} - \ell/{2^t} \notin \mathbb{Z}$.

_non_int_delta_b_diff

_non_int_delta_b_diff.instantiate({b:_b_floor})

Now we're ready to evaluate the summation as a finite geometric sum, while we tweak the auto-simplification directives just a bit to keep things from being over-simplified:

# For this step, we re-enable the reduction of double exponentiation
# and disable combining exponents (to keep 2 and 2^t from combining into 2^{t+1}).
Exp.change_simplification_directives(reduce_double_exponent=True)
alpha_l_eq_05_alt = alpha_l_eq_04_alt.inner_expr().rhs.factors[1].geom_sum_reduce()

alpha_l_eq_06_alt = (
        alpha_l_eq_05_alt.inner_expr().rhs.factors[1].numerator.operands[1].
        operand.exponent.distribute(3, right_factors=[_two_pow_t]))

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	381, 2, 3	, ⊢
	: , : , :
2	instantiation	329, 4, 5	, ⊢
	: , : , :
3	instantiation	392, 6	⊢
	: , : , :
4	instantiation	329, 7, 8	, ⊢
	: , : , :
5	instantiation	292, 286, 428, 321, 9, 10, 322, 401, 362, 193, 151, 242, 11^*	⊢
	: , : , : , : , : , :
6	instantiation	392, 12	⊢
	: , : , :
7	instantiation	329, 13, 14, 15^*	⊢
	: , : , :
8	instantiation	16, 37, 17, 18, 19, 20, 21^, 22^	, ⊢
	: , : , : , :
9	instantiation	307	⊢
	: , : , :
10	instantiation	345	⊢
	: , :
11	instantiation	267, 321, 426, 322, 297, 207, 242, 23^*	⊢
	: , : , : , : , : , :
12	instantiation	392, 24	⊢
	: , : , :
13	instantiation	329, 25, 26, 27^*	⊢
	: , : , :
14	instantiation	28, 420, 29, 128, 324, 242, 233	⊢
	: , : , :
15	instantiation	381, 30, 31	⊢
	: , : , :
16	conjecture		⊢
	proveit.numbers.summation.gen_finite_geom_sum
17	instantiation	303, 32, 33	, ⊢
	: , : , :
18	conjecture		⊢
	proveit.numbers.number_sets.integers.zero_is_int
19	instantiation	416, 34, 370	⊢
	: , :
20	instantiation	35, 36	⊢