logo

Demonstrations for the theory of proveit.linear_algebra.scalar_multiplication

In [1]:
import proveit
from proveit.linear_algebra import ScalarMult
from proveit.numbers import zero, one
from proveit.physics.quantum import Ket
%begin demonstrations

Some Example Simple ScalarMult Expressions for Demonstrations

In [2]:
example_scalar_mult_01, example_scalar_mult_02, example_scalar_mult_03 = (
        ScalarMult(one, Ket(one)),
        ScalarMult(one, ScalarMult(one, Ket(zero))),
        ScalarMult(one, ScalarMult(one, ScalarMult(one, Ket(zero)))))
Out[2]:
example_scalar_mult_01:
example_scalar_mult_02:
example_scalar_mult_03:

ScalarMult.shallow_simplification()

In [3]:
example_scalar_mult_01.shallow_simplification()
Out[3]:
In [4]:
example_scalar_mult_02
Out[4]:
In [5]:
temp_result = example_scalar_mult_02.shallow_simplification()
Out[5]:
temp_result:  ⊢  
In [6]:
# Notice the result here is no longer a ScalarMult!
# Moral: simplification can change the type.
type(temp_result.rhs)
Out[6]:
proveit.physics.quantum.algebra.bra_ket.Ket
In [7]:
temp_result.inner_expr().rhs.operands[0].simplify()
Out[7]:
In [8]:
# notice here we eliminate multiply-nested ScalarMults
# and multiplicative identity scalars
# with our shallow_simplification() method
temp_result_02 = example_scalar_mult_03.shallow_simplification()
Out[8]:
temp_result_02:  ⊢  

ScalarMult.scalar_one_elimination()

In [9]:
example_scalar_mult_01.scalar_one_elimination()
Out[9]:
In [10]:
example_scalar_mult_02.scalar_one_elimination()
Out[10]:
In [11]:
example_scalar_mult_03.scalar_one_elimination()
Out[11]:

ScalarMult.double_scaling_reduction()

In [12]:
# quite reasonably, the double-scaling_reduction() method
# only works for nested ScalarMults
try:
    example_scalar_mult_01.double_scaling_reduction(auto_simplify=False)
except ValueError as the_error:
    print("ValueError: {}".format(the_error))
ValueError: 'double_scaling_reduction' is only applicable for a doubly nested ScalarMult
In [13]:
example_scalar_mult_02.double_scaling_reduction(auto_simplify=False)
Out[13]:
In [14]:
example_scalar_mult_03.double_scaling_reduction(auto_simplify=False)
Out[14]:
In [15]:
%end demonstrations