Quantum algebra development

[wwitzel]

trafficstars

Make enhancements and fixes to the quantum algebra package, including the following as a first batch of updates:

1. Fix the bra_def axiom and KEEP the qmult_of_bra_as_map theorem. qmult_of_bra_as_map has the proper form (accounting for the different conventions between Physicists and Mathematicians as noted above qmult_of_bra_as_map).
   a) Replace bra_def with this form (and move the 'different conventions' comment to above 'bra_def') EXCEPT remove the Qmult(..) wrapper around Bra(varphi). b) KEEP qmult_of_bra_as_map in the quantum algebra theorems.
   c) RESTORE occurrences of 'qmult_of_bra_as_map' (e.g., in qmult.py).
2. Add a Qmult.projection method that will instantiate the bra_def a) Decorate this method with "@equality_prover('projected', 'project') b) Check that there are two operands we'll denote here as M and |ψ⟩. Otherwise, raise ValueError. c) Add the following lines near the top of Qmult.linmap_reduction: from proveit.physics.quantum import QmultCodomain # In the process of proving that 'self' is in QmultCodomain, # it will prove it is a linear map if it can. QmultCodomain.membership_object(self).conclude() d) Execute "linmap_eq = Qmult(M).linmap_reduction()" e) import and instantiate 'qmult_op_ket ' with {A:Qmult(<φ|), Hspace: known Hilbert space of |psi>, X: Complex, var_ket_psi: |ψ⟩}. Assign to 'qmult_eq'. NOTE CHANGE: where 'Qmult' now appears. f) return linmap_eq.sub_right_side_into(qmult_eq.inner_expr().rhs.operator) g) NOTE CHANGE: no bra_def instantiation. Test on the demonstrations page.
3. Add a theorem for that equates the self-projection to its norm: a) Something like: forall_{𝓗 in the class of Hilbert spaces} forall_{|ψ⟩ in 𝓗} ⟨ψ||ψ⟩ = || |ψ⟩ ||^2 b) Handle this special case in Qmult.projection c) As a bonus, prove this theorem via bra_def and norm_def (in proveit.linear_algebra.inner_products)
4. Implement and test Qmult.evaluation. a) In Qmult.shallow_simplification, insert an 'if' block before the return statement check if 'must_evaluate' is True. If so, b) If expr is an instance of ScalarMult, do expr = eq.update(expr.inner_expr().scaled.projection()) c) Otherwise do: expr = eq.update(expr.projection()) d) Then, either way, do "expr = eq.update(expr.evaluation())". e) Test on demonstration page.