Theory of proveit.physics.quantum

Provide description here.

import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

algebra	Linear algebra over Hilbert spaces and bra-ket notation
circuits	Quantum circuits as a representation of quantum operations and their applications
QFT	For work related to Nielsen & Chuang's quantum fourier transform (QFT) alg'm
QPE	For work related to Nielsen & Chuang's quantum phase estimation (QPE) alg'm

All axioms contained within this theory

proveit.physics.quantum.hadamard_on_zero

proveit.physics.quantum.substitution

proveit.physics.quantum.algebra

proveit.physics.quantum.algebra.ket_zero_def

proveit.physics.quantum.algebra.ket_one_def

proveit.physics.quantum.algebra.ket_plus_def

proveit.physics.quantum.algebra.ket_minus_def

proveit.physics.quantum.algebra.num_ket_def

proveit.physics.quantum.algebra.bra_def

proveit.physics.quantum.algebra.qmult_of_ket

proveit.physics.quantum.algebra.qmult_of_matrix

proveit.physics.quantum.algebra.qmult_of_linmap

proveit.physics.quantum.algebra.qmult_op_ket

proveit.physics.quantum.algebra.qmult_op_op

proveit.physics.quantum.algebra.qmult_ket_ket

proveit.physics.quantum.algebra.qmult_ket_bra

proveit.physics.quantum.algebra.qmult_complex_complex

proveit.physics.quantum.algebra.qmult_complex_left

proveit.physics.quantum.algebra.qmult_complex_right

proveit.physics.quantum.algebra.qmult_in_codomain_only_if_valid

proveit.physics.quantum.algebra.multi_qmult_def

proveit.physics.quantum.circuits

proveit.physics.quantum.circuits.qcircuit_eq_def

proveit.physics.quantum.circuits.qcircuit_input_eq_def

proveit.physics.quantum.circuits.qcircuit_output_eq_def

proveit.physics.quantum.circuits.qcircuit_input_part_eq_def

proveit.physics.quantum.circuits.qcircuit_output_part_eq_def

proveit.physics.quantum.QFT

This sub-theory contains no axioms.

proveit.physics.quantum.QPE

proveit.physics.quantum.QPE.QPE1_def

proveit.physics.quantum.QPE.QPE_def

proveit.physics.quantum.QPE._t_in_natural_pos

proveit.physics.quantum.QPE._s_in_nat_pos

proveit.physics.quantum.QPE._unitary_U

proveit.physics.quantum.QPE._u_ket_register

proveit.physics.quantum.QPE._normalized_ket_u

proveit.physics.quantum.QPE._phase_in_interval

proveit.physics.quantum.QPE._eigen_uu

proveit.physics.quantum.QPE._mod_add_def

proveit.physics.quantum.QPE._psi_t_def

proveit.physics.quantum.QPE._Psi_def

proveit.physics.quantum.QPE._sample_space_def

proveit.physics.quantum.QPE._alpha_m_def

proveit.physics.quantum.QPE._best_floor_def

proveit.physics.quantum.QPE._best_round_def

proveit.physics.quantum.QPE._delta_b_def

proveit.physics.quantum.QPE._success_def

proveit.physics.quantum.QPE._fail_def

proveit.physics.quantum.QPE._n_in_natural_pos

proveit.physics.quantum.QPE._n_ge_two

proveit.physics.quantum.QPE._eps_in_interval

proveit.physics.quantum.QPE._t_req