Demonstrations for the theory of proveit.numbers.logarithms

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

Generate a few Log expressions for testing and some assumptions:

log_2_of_5, log_a_of_b = Log(two, five), Log(a, b)

log_2_of_5:

log_a_of_b:

demo_assumptions = [InSet(a, RealPos), InSet(b, RealPos), NotEquals(a, one)]

demo_assumptions:

Testing Log.deduce_in_number_set()

log_2_of_5.deduce_in_number_set(Real)

 ⊢  

log_a_of_b.deduce_in_number_set(Real, assumptions=demo_assumptions)

, ,  ⊢  

Testing Log.bound_via_operand_bound()

log_a_of_b.bound_via_operand_bound(Less(b, five),
        assumptions=[InSet(a, RealPos), InSet(b, RealPos), greater(a, one), Less(b, five)])

, , ,  ⊢  

log_a_of_b.bound_via_operand_bound(greater(b, five),
        assumptions=[InSet(a, RealPos), InSet(b, RealPos), greater(a, one), greater(b, five)])

, , ,  ⊢  

%end demonstrations