QuantumLib.Measurement

• Probability of outcome ϕ given input ψ
• Probability of measuring ϕ on the first m qubits given (m + n) qubit input ψ

QuantumLib.DiscreteProb

• Definition of probability distribution
• Sample from a distribution
• Probability that a distribution satisfies a predicate (pr_outcome_sum)
• Probability that a distribution satisfies a predicate (pr_P)
• Distribution created by running a quantum program
• Uniform distribution
• Joint distribution
• Repeat independent runs

QuantumLib.Ctopology

QuantumLib.VectorStates

QuantumLib.Quantum

• Quantum basis states
• Unitaries
  • Rotation Matrices
  • Phase Lemmas

QuantumLib.Complex

• The set of complex numbers
  • Constants and usual functions
    • Arithmetic operations
• Showing that C is a field, and a vector space over itself
  • • Other usual functions
  • C is a field
• Content added as part of inQWIRE
• some C big_sum specific lemmas
• Lemmas about Cpow
• Lemmas about Cmod
• Lemmas about Cconj
• Lemmas about complex Square roots
• Complex exponentiation
• Automation

QuantumLib.Polar

QuantumLib.Proportional

QuantumLib.Permutations

• Permutations on (0,...,n-1)
• Permutation matrices

QuantumLib.Eigenvectors

• Proving some indentities
• Defining orthonormal matrix
• showing that all matrices have some eigenvector
• Lemmas relating to forming bases
• Defining and verifying the gram_schmidt algorythm and proving v can be part of an onb
• some useful facts about unitary matrices
• We now define diagonal matrices and diagonizable matrices, proving basic lemmas
• Defining Cprod, similar to big_sum
• Defining upper triangular matrix
• Defining eignestates to be used in type system
• Showing that certain types of matrices are equal when their eigenpairs are equal
• Some actual examples/lemmas

QuantumLib.Polynomial

QuantumLib.FTA

QuantumLib.VecSet

• some preliminary defs and lemmas
• Defining properties which are invarient under column operations, etc...
• Defining and proving lemmas relating to the determinant
• We can now define some invariants for Determinant
• Defining linear independence, and proving lemmas etc...
• defining a new type of matrix which we will show is the lin_indep/invertible matrices
• Now we prove more properties of invariants
• Inverses of square matrices
• We finish proving lemmas about invarients
• we define another set of invariants to help show that Det A × Det B = Det (A × B)

QuantumLib.Summation

QuantumLib.Pad

QuantumLib.FiniteGroups

QuantumLib.RealAux

• Basic lemmas
• Square roots
• Trigonometry
• glb support
• Showing that R is a field, and a vector space over itself
• some big_sum lemmas specific to R

QuantumLib.Prelim

QuantumLib.Matrix

• Matrix definitions and infrastructure
• Operands and operations
• Showing that M is a vector space
• Proofs about well-formedness
• Tactics for showing well-formedness
• Basic matrix lemmas
• Summation lemmas specific to matrices
• Defining matrix altering/col operations
• Some more lemmas with these new concepts
• Tactics