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

import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults, Lambda
from proveit import a, b, c, e, f, l, m, x, y, A, B, C, N, Q, X, Omega
from proveit.logic import Or, Forall, InSet, Union, Disjoint
from proveit.logic.sets.functions.injections import subset_injection
from proveit.logic.sets.functions.bijections import bijection_transitivity
from proveit.numbers import (zero, one, Add, Neg, greater, Less)
from proveit.numbers.modular import interval_left_shift_bijection
from proveit.statistics import prob_of_disjoint_events_is_prob_sum
from proveit.physics.quantum import NumKet
from proveit.physics.quantum.QPE import (
    _t, _two_pow_t, _two_pow_t__minus_one,  _t_in_natural_pos,
    _two_pow_t_minus_one_is_nat_pos, _Omega,
    _b_floor, _best_floor_is_int, _best_floor_def,
    _alpha_m_def, _full_domain, _neg_domain, _pos_domain,
    _modabs_in_full_domain_simp, ModAdd, _sample_space_bijection,
    _Omega_is_sample_space, _outcome_prob, _fail_def,
    _fail_sum_prob_conds_equiv_lemma)

%proving _fail_sum

defaults.assumptions = _fail_sum.all_conditions()

e_in_domain = defaults.assumptions[0]

defaults.preserved_exprs = {e_in_domain.domain.upper_bound.operands[0]}

Start with the $P_{\textrm{fail}}$ definition¶

fail_def_inst = _fail_def.instantiate()

We will next translate from $m \in \{0~\ldotp \ldotp~2^{t} - 1\}$ to $b_f \oplus l$ with $l \in \{-2^{t-1} + 1 ~\ldotp \ldotp~2^{t-1}\}$¶

lower_bound = _neg_domain.lower_bound

upper_bound = _pos_domain.upper_bound

interval_left_shift_bijection

lambda_map_bijection = interval_left_shift_bijection.instantiate(
    {a:lower_bound, b:upper_bound, c:_b_floor, N:_two_pow_t, x:l})

Use the $\oplus$ notation within kets (but not otherwise, for simplification purposed):

b_modadd_l__def = ModAdd(_b_floor, l).definition(assumptions=[InSet(l, _full_domain)])

defaults.replacements = [b_modadd_l__def.derive_reversed().substitution(NumKet(b_modadd_l__def.rhs, _t))]

transformed_fail_def = fail_def_inst.inner_expr().rhs.transform(
    lambda_map_bijection.element, lambda_map_bijection.domain.domain, _Omega)

Proceed to split the probability of this event into the sum of two disjoint possibilities¶

Our goal will be to apply the following theorem:

prob_of_disjoint_events_is_prob_sum

Prove the $|l|_{\textrm{mod}~2^t} > e$ condition for either the positive or negative domain for simplification purposes¶

condition = transformed_fail_def.rhs.non_domain_condition()

neg_domain_assumptions = [InSet(l, _neg_domain), *_fail_sum.all_conditions()]

pos_domain_assumptions = [InSet(l, _pos_domain), *_fail_sum.all_conditions()]

_modabs_in_full_domain_simp

absmod_posdomain_simp = _modabs_in_full_domain_simp.instantiate(
    assumptions=pos_domain_assumptions)

absmod_negdomain_simp = _modabs_in_full_domain_simp.instantiate(
    assumptions=neg_domain_assumptions)

pos_cond_eval = absmod_posdomain_simp.sub_left_side_into(
    greater(l, e), assumptions=pos_domain_assumptions).evaluation()

neg_cond_eval = absmod_negdomain_simp.sub_left_side_into(
    greater(Neg(l), e), assumptions=neg_domain_assumptions).evaluation()

Prove the proper injective mapping condition then apply `prob_of_disjoint_events_is_prob_sum`¶

circuit_map = Lambda(l, transformed_fail_def.rhs.instance_expr)

lambda_map_bijection

_sample_space_bijection

trans_bijection = lambda_map_bijection.apply_transitivity(_sample_space_bijection)

prob_eq_sum1 = prob_of_disjoint_events_is_prob_sum.instantiate(
    {Omega:_Omega, A:_neg_domain, B:_pos_domain, C:Union(_neg_domain, _pos_domain), 
     X:_full_domain, f:circuit_map, Q:Lambda(l, condition), x:l},
    replacements=[pos_cond_eval, neg_cond_eval]).with_wrap_after_operator()

Compute the event probabilities in terms of summing outcome probabilities¶

outcome_prob_pos = _outcome_prob.instantiate({m:ModAdd(_b_floor, l)}, assumptions=pos_domain_assumptions)

outcome_prob_neg = _outcome_prob.instantiate({m:ModAdd(_b_floor, l)}, assumptions=neg_domain_assumptions)

subset_injection

subset_injection.instantiate({A:_pos_domain, B:_full_domain, C:_Omega, f:trans_bijection.element})

subset_injection.instantiate({A:_neg_domain, B:_full_domain, C:_Omega, f:trans_bijection.element})

prob_eq_sum2 = prob_eq_sum1.inner_expr().rhs.operands[0].compute(_Omega, replacements=[outcome_prob_neg])

prob_eq_sum3 = prob_eq_sum2.inner_expr().rhs.operands[1].compute(_Omega, replacements=[outcome_prob_pos])

That logical equivalence of conditions is handled in a separate lemma, _fail_sum_prob_conds_equiv_lemma:

_fail_sum_prob_conds_equiv_lemma

# Here we explicitly preserve the -(e+1) expression; otherwise it becomes (-e-1) and
# later won't match up with the expression to be substituted for
conditions_equiv = (
    _fail_sum_prob_conds_equiv_lemma.instantiate(preserve_expr=Neg(Add(e, one)))
    .instantiate(preserve_expr=Neg(Add(e, one)), sideeffect_automation=False))

prob_eq_sum4 = prob_eq_sum3.inner_expr().lhs.operand.body

prob_eq_sum4 = prob_eq_sum3.inner_expr().lhs.operand.body.substitute_condition(
    conditions_equiv, preserve_all=True, sideeffect_automation=False)

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

%qed

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

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	412, 2, 5	⊢
	: , : , :
2	instantiation	363, 3, 4, 5	⊢
	: , : , : , :
3	instantiation	337, 6, 7	⊢
	: , : , :
4	instantiation	337, 8, 9	⊢
	: , : , :
5	instantiation	378, 10	⊢
	: , : , :
6	instantiation	11, 428	⊢
	:
7	instantiation	12, 45, 13, 226, 224^, 14^	⊢
	: , : , : , : , : , : , : , :
8	instantiation	337, 15, 16	⊢
	: , : , :
9	modus ponens	17, 18	⊢
10	instantiation	378, 19	⊢
	: , : , :
11	axiom		⊢
	proveit.physics.quantum.QPE._fail_def
12	conjecture		⊢
	proveit.statistics.prob_of_all_events_transformation
13	instantiation	88, 20	⊢
	: , :
14	instantiation	21, 349, 446, 351, 22, 79, 23, 24^*	⊢
	: , : , : , : , : , :
15	instantiation	337, 25, 26	⊢
	: , : , :
16	instantiation	44, 45, 27, 28^, 43^, 29^*	⊢
	: , : , : , : , :
17	instantiation	53, 391	⊢
	: , : , : , : , : , :
18	generalization	30	⊢
19	modus ponens	31, 32	⊢
20	instantiation	118, 227	⊢
	: , : , :
21	conjecture		⊢
	proveit.numbers.modular.redundant_mod_elimination_in_sum_in_modabs