Theorem Dependencies

proveit.physics.quantum.QPE._sample_space_bijection

see proof

import proveit
# Automation is not needed when querying dependencies:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
from proveit.physics.quantum.QPE import _sample_space_bijection

%dependencies _sample_space_bijection

Unproven conjectures required (directly or indirectly) to prove _sample_space_bijection

proveit.core_expr_types.expr_arrays.varray_neq_via_any_elem_neq

proveit.core_expr_types.operations.operands_substitution_via_tuple

proveit.core_expr_types.tuples.extended_range_from1_len_typical_eq

proveit.core_expr_types.tuples.general_len

proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1

proveit.core_expr_types.tuples.merge_extension

proveit.core_expr_types.tuples.range_from1_len

proveit.core_expr_types.tuples.range_from1_len_is_nat

proveit.core_expr_types.tuples.range_from1_len_typical_eq

proveit.core_expr_types.tuples.tuple_len_0_typical_eq

proveit.core_expr_types.tuples.tuple_neq_via_any_elem_neq

proveit.logic.booleans.conjunction.any_from_and

proveit.logic.booleans.conjunction.conjunction_from_quantification

proveit.logic.booleans.conjunction.some_from_and

proveit.logic.booleans.disjunction.any_if_all

proveit.logic.booleans.disjunction.disassociate

proveit.logic.booleans.disjunction.or_if_any

proveit.logic.booleans.quantification.universality.bundle

proveit.logic.equality.four_chain_transitivity

proveit.logic.sets.enumeration.unfold

proveit.logic.sets.functions.bijections.bijective_by_uniqueness

proveit.numbers.addition.add_complex_closure_bin

proveit.numbers.addition.add_nat_closure_bin

proveit.numbers.addition.add_nat_pos_closure_bin

proveit.numbers.addition.association

proveit.numbers.addition.disassociation

proveit.numbers.addition.leftward_commutation

proveit.numbers.addition.subtraction.add_cancel_general

proveit.numbers.addition.subtraction.add_cancel_triple_32

proveit.numbers.multiplication.distribute_through_sum

proveit.numbers.multiplication.elim_one_left

proveit.numbers.multiplication.mult_complex_closure_bin

proveit.numbers.negation.complex_closure

proveit.numbers.negation.distribute_neg_through_binary_sum

proveit.numbers.negation.int_closure

proveit.numbers.number_sets.complex_numbers.real_within_complex

proveit.numbers.number_sets.integers.int_interval_within_int

proveit.numbers.number_sets.integers.interval_lower_bound

proveit.numbers.number_sets.integers.nat_pos_within_int

proveit.numbers.number_sets.integers.nat_within_int

proveit.numbers.number_sets.integers.pos_int_is_natural_pos

proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos

proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat

proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound

proveit.numbers.number_sets.rational_numbers.int_within_rational

proveit.numbers.number_sets.real_numbers.nat_pos_within_real

proveit.numbers.number_sets.real_numbers.rational_within_real

proveit.numbers.numerals.decimals.add_1_1

proveit.numbers.numerals.decimals.add_2_1

proveit.numbers.numerals.decimals.add_3_1

proveit.numbers.numerals.decimals.less_0_1

proveit.numbers.numerals.decimals.nat3

proveit.numbers.numerals.decimals.nat4

proveit.numbers.numerals.decimals.nat5

proveit.numbers.numerals.decimals.nat8

proveit.numbers.numerals.decimals.posnat1

proveit.numbers.numerals.decimals.posnat2

proveit.numbers.numerals.decimals.posnat4

proveit.numbers.numerals.decimals.posnat8

proveit.numbers.numerals.decimals.tuple_len_2_typical_eq

proveit.numbers.numerals.decimals.tuple_len_3_typical_eq

proveit.numbers.numerals.decimals.tuple_len_4_typical_eq

proveit.numbers.numerals.decimals.tuple_len_5_typical_eq

proveit.numbers.numerals.decimals.tuple_len_8_typical_eq

proveit.physics.quantum.algebra.num_ket_neq

proveit.physics.quantum.circuits.qcircuit_neq

proveit.physics.quantum.circuits.qcircuit_output_part_neq

Axioms required (directly or indirectly) to prove _sample_space_bijection

proveit.core_expr_types.operations.operands_substitution

proveit.core_expr_types.tuples.range_extension_def

proveit.logic.booleans.bools_def

proveit.logic.booleans.conjunction.and_t_t

proveit.logic.booleans.disjunction.empty_disjunction

proveit.logic.booleans.disjunction.left_in_bool

proveit.logic.booleans.disjunction.multi_disjunction_def

proveit.logic.booleans.disjunction.or_f_f

proveit.logic.booleans.disjunction.or_f_t

proveit.logic.booleans.disjunction.or_t_f

proveit.logic.booleans.disjunction.or_t_t

proveit.logic.booleans.disjunction.right_in_bool

proveit.logic.booleans.eq_true_elim

proveit.logic.booleans.eq_true_intro

proveit.logic.booleans.false_not_true

proveit.logic.booleans.implication.affirmation_via_contradiction

proveit.logic.booleans.implication.denial_via_contradiction

proveit.logic.booleans.negation.negation_elim

proveit.logic.booleans.negation.not_f

proveit.logic.booleans.negation.not_t

proveit.logic.booleans.negation.operand_is_bool

proveit.logic.booleans.true_axiom

proveit.logic.equality.equality_in_bool

proveit.logic.equality.equals_reflexivity

proveit.logic.equality.equals_symmetry

proveit.logic.equality.equals_transitivity

proveit.logic.equality.not_equals_def

proveit.logic.equality.substitution

proveit.logic.sets.enumeration.enum_set_def

proveit.logic.sets.functions.images.set_image_def

proveit.logic.sets.inclusion.proper_subset_def

proveit.logic.sets.inclusion.subset_eq_def

proveit.numbers.number_sets.natural_numbers.successor_in_nats

proveit.numbers.number_sets.natural_numbers.zero_in_nats

proveit.numbers.numerals.decimals.one_def

proveit.numbers.ordering.less_eq_def

proveit.numbers.ordering.transitivity_less_less

proveit.physics.quantum.QPE._s_in_nat_pos

proveit.physics.quantum.QPE._t_in_natural_pos

Conservative definitions used (but not logically required) to prove _sample_space_bijection

proveit.physics.quantum.QPE._sample_space_def

Theorems/conjectures that depend directly on _sample_space_bijection

proveit.physics.quantum.QPE._Omega_is_sample_space

proveit.physics.quantum.QPE._fail_sum

proveit.physics.quantum.QPE._pfail_in_real

proveit.physics.quantum.QPE._precision_guarantee

proveit.physics.quantum.QPE._success_complements_failure