Linear algebra development

[wwitzel]

Make enhancements and fixes to the linear algebra package. For example, we currently don't even have a proper definition for a Unitary matrix to be able to declare
U^{-1} = U^{\dag}

One minor issue that comes up is notation. Physicists use 'dagger' for the adjoint (or conjugate transpose or Hermitian conjugate) but Mathematicians use '*' or 'H'. I try to use mathematician's notation in mathematics packages like linear algebra and reserve the quantum physics notation to the quantum packages. '*' is bad notation because of ambiguity, but we could use 'H' in the linear algebra package and switch the style to using 'dagger' in quantum packages. Let's worry about this later, but we may eventually want to add style options to Adj so we can use either style depending on where it is being used (e.g., 'adj' in the quantum package could create a linear algebra Adj object but change the style to use a 'dagger').

An even more tricky issue is the equivalence of linear maps (or linear operators) and matrices. See https://en.wikipedia.org/wiki/Hermitian_adjoint and https://en.wikipedia.org/wiki/Conjugate_transpose. They are equivalent, but they are different concepts. A linear map is an abstract concept that can be generalized while matrices are arrays of numbers. We have both concepts in Prove-It and need to be careful about the distinction. For example, we can take the adjoint of a linear operator or a matrix with the result being equivalent. The adjoint should arguably be defined for linear maps abstractly and then proven to take a concrete form with respect to matrices as the conjugate transpose.

It's easy for me to get lost in land of abstract Mathematics where I lack a strong background. Let's focus on our quantum mechanics needs but keep the abstract notions in mind so we leave room for a proper infrastructure that properly treats abstract Mathematics (being hopeful about the future of Prove-It). It can be useful to work backwards (from concrete applications to abstract foundations). In any case, here's a start:

1. We are going to need to make and define a matrix identity. Note that there is a linear map identity defined in proveit.linear_algebra.linear_maps (see 'identity_def' on the axioms page).
   a) First copy identity.py from 'linear_maps' to 'matrices' and modify it slightly. It won't take a 'vecspace' in init, it should take a size instead. Also, change the 'string_format' and set a 'latex_format' for the _operator_ to be an appropriate matrix identity (e.g., '1' and '\mathbb{1}) to distinguish matrix identities from linear map identities.
   b) Add 'from .identity import Identity' to init.py of the matrices package so it can be conveniently imported from 'matrices'.
   c) Add an 'identity_def' to the matrices axioms page to define the matrix identity according to the corresponding linear map identity: for any positive integer n (in NaturalPos) 1_n = I_{C^{n × n}}.
2. Add a sub-package to proveit.linear_algebra.matrices called transposition (to deal with transpose, conjugate transpose, unitarity, etc.)
3. Move 'unitary_group.py' from linear_algebra.matrices to linear_algebra.matrices.transposition and change the init.py files appropriately (copy 'from .unitary_group import Unitary, SpecialUnitary' from matrices/init.py to transposition/init.py and change it in matrices/init.py to 'from .transposition import Unitary, SpecialUnitary').
4. Move 'unitaries_are_matrices' and 'special_unitarities_are_matrices' from proveit.linear_algebra.matrices to proveit.linear_algebra.matrices.transposition. While we're at it, remove 'eigen_pow' from proveit.linear_algebra.matrices which is unused and obsolute (replaced by 'eigen_exp_application' in proveit.linear_algebra.matrices.exponentiation).
5. Add more theorems to matrices.transposition, particularly U U^{dag} = I_n and U^dag U = I_n for all n in NaturalPos and U in Unitary(n).
6. In the transposition demonstration page, test these theorems by importing them and instantiating them (under appropriate assumptions about U and n or whatever labels are used).

From here, we could go in the abstract direction and think about how unitarity is defined in the context of linear maps (e.g., when the inverse of the map is equal to the adjoint). We'd need the concept of function inversion (e.g., in proveit.logic.sets.functions) and we'd need to deal with the fact that the inverse only exists when a function is bijective (I'd need to think about that one). But we probably want to go in the direction of applications for now and think about multiplying unitary matrices and their adjoints with Qmult instead of MatrixMult, and then move on to quantum circuit inversion. But let's start with 1-6 above.

[vsprasannaa]

Thanks, I had a rather naive question regarding 1a. By size, is it N or N^2 for an NxN matrix? I've tentatively replaced 'vecspace' in two places with 'two' (assuming that we take a 2x2 matrix and size is N). Also, I've replaced the string format part with:
latex_format='\begin{pmatrix} 1\ 0 \ 0\ 1 \end{pmatrix}'
When I try to add 'identity_def' in the axioms ipynb file, I ran into this error:
TypeError: init() missing 1 required positional argument: 'string_format'

[vsprasannaa]

Sudhindu is running into the same error too. :-(

[wwitzel]

The size would be N. It isn't intended to display an actual NxN identity matrix but rather something like \mathbb{1}_N as a compact representative for an NxN identity matrix where N can be a variable (not necessarily a number).

[wwitzel]

In order to finish a proof we were working on with Sudhindu, we would like to automatically prove that the InnerProd of Hilbert space vectors is Complex (and more generally that the InnerProd of an inner product space over K is K). For convenience, we probably want to add the following two theorems to the linear_algebra.inner_products package. One would follow directly from inner_prod_space_def (just the second part of the conjunction in that theorem):

(sorry if this shows black-on-black for you -- it does in mine as well, it's always possible to temporarily change that setting in GitHub so you can read what I'm pasting)
The other theorem could be more specific to Hilbert spaces:

These would each be easy to prove, deriving easily from inner_prod_space_def and hilbert_space_def -- proving those would be good practice. The latter theorem could also use the former in its proof.

In addition to adding those theorems, we'll want to make a method for conveniently instantiating them. We can add a prover method to the InnerProd class. Specifically:

@relation_prover
def deduce_membership(self, K, **defaults_config):
   ...

This could instantiate the more specialized theorem for Hilbert spaces if K is Complex. Otherwise it would instantiate the more general theorem with K:K.

Let's also add another method which will help with automatically calling this when we wish to prove that the InnerProd is a member of some particular K.

def readily_provable_membership(self, K):
        '''
        Return True iff we can readily prove that this InnerProd
        evaluates to something in set K.
        '''

Iterate through the InnerProdSpaces to which both of the operands are known to belong via InnerProdSpaces.yield_known_inner_prod_spaces. If there aren't any, simply return False. If any have a "field" equal to the given K, return True. Otherwise, collect all of their fields into a set and then loop through these and check if any of these readily includes the set K as follows:

   for field in fields:
       if hasattr(field, 'readily_includes') and field.readily_includes(K):
           return True

Otherwise, return False.

But, sorry, there is one thing we need to do before implementing "readily_provable_membership". We need to make it convenient to obtain the "field" attribute of an InnerProdSpaces object. We need to do this for both the InnerProdSpaces class and HilbertSpacesLiteral class. For InnerProdSpaces, simply add "self.field = field" at the end of its "init" method. For the HilbertSpacesLiteral, let's add a "field" property:

@property
def field(self):
    return Complex

In the 'readily_provable_membership' method of InnerProd, but sure to check if each InnerProdSpace yielded by InnerProdSpaces.yield_known_inner_prod_spaces has a field attribute before getting it. If it doesn't have a field attribute, just skip it.

There is one thing I need to do before this automation will fully work. But I'll add that as an addendum to Issue #320 and take care of it myself.