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