Demonstrations for the theory of proveit.linear_algebra.scalar_multiplication

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

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)))))

example_scalar_mult_01:

example_scalar_mult_02:

example_scalar_mult_03:

ScalarMult.shallow_simplification()

example_scalar_mult_01.shallow_simplification()

 ⊢  

example_scalar_mult_02

temp_result = example_scalar_mult_02.shallow_simplification()

temp_result:  ⊢  

# Notice the result here is no longer a ScalarMult!
# Moral: simplification can change the type.
type(temp_result.rhs)

proveit.physics.quantum.algebra.bra_ket.Ket

temp_result.inner_expr().rhs.operands[0].simplify()

 ⊢  

# 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()

temp_result_02:  ⊢  

ScalarMult.scalar_one_elimination()

example_scalar_mult_01.scalar_one_elimination()

 ⊢  

example_scalar_mult_02.scalar_one_elimination()

 ⊢  

example_scalar_mult_03.scalar_one_elimination()

 ⊢  

ScalarMult.double_scaling_reduction()

# 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

example_scalar_mult_02.double_scaling_reduction(auto_simplify=False)

 ⊢  

example_scalar_mult_03.double_scaling_reduction(auto_simplify=False)

 ⊢  

%end demonstrations