logo

Demonstrations for the theory of proveit.numbers.logarithms

In [1]:
import proveit
from proveit import a, b
from proveit.logic import InSet, NotEquals
from proveit.numbers import (zero, one, two, five, greater, Less,
                             LessEq, Log, Real, RealPos)

%begin demonstrations
In [ ]:
 

Generate a few Log expressions for testing and some assumptions:

In [2]:
log_2_of_5, log_a_of_b = Log(two, five), Log(a, b)
Out[2]:
log_2_of_5:
log_a_of_b:
In [3]:
demo_assumptions = [InSet(a, RealPos), InSet(b, RealPos), NotEquals(a, one)]
Out[3]:
demo_assumptions:

Testing Log.deduce_in_number_set()

In [4]:
log_2_of_5.deduce_in_number_set(Real)
Out[4]:
In [5]:
log_a_of_b.deduce_in_number_set(Real, assumptions=demo_assumptions)
Out[5]:
, ,  ⊢  

Testing Log.bound_via_operand_bound()

In [6]:
log_a_of_b.bound_via_operand_bound(Less(b, five),
        assumptions=[InSet(a, RealPos), InSet(b, RealPos), greater(a, one), Less(b, five)])
Out[6]:
, , ,  ⊢  
In [7]:
log_a_of_b.bound_via_operand_bound(greater(b, five),
        assumptions=[InSet(a, RealPos), InSet(b, RealPos), greater(a, one), greater(b, five)])
Out[7]:
, , ,  ⊢  
In [8]:
%end demonstrations