Theorems (or conjectures) for the theory of proveit.numbers.logarithms

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b, x, y
from proveit.logic import Forall, InSet, Equals, NotEquals
from proveit.numbers import (one, Add, greater, greater_eq, Less,
                             LessEq, Log, Real, RealPos, RealNonNeg)
from proveit.numbers.ordering import number_ordering

%begin theorems

Defining theorems for theory 'proveit.numbers.logarithms'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

log_real_pos_real_closure = Forall((a,b),
       InSet(Log(a, b), Real),
       domain=RealPos,
       condition=NotEquals(a, one))

log_real_pos_real_closure (conjecture without proof):

log_eq_1 = Forall(a,
       Equals(Log(a, a), one),
       domain=RealPos)

log_eq_1 (conjecture without proof):

log_real_pos_from_gt_1 = Forall((a,b),
       InSet(Log(a, b), RealPos),
       domain=RealPos,
       condition=greater(a, one))

log_real_pos_from_gt_1 (conjecture without proof):

log_real_nonneg_from_geq_1 = Forall((a,b),
       InSet(Log(a, b), RealNonNeg),
       domain=RealPos,
       condition=greater_eq(a, one))

log_real_nonneg_from_geq_1 (conjecture without proof):

log_increasing_less = (
    Forall((a, x, y),
           Less(Log(a, x), Log(a, y)), 
           conditions=[Less(x, y), greater(a, one)],
           domain=RealPos))

log_increasing_less (conjecture without proof):

log_increasing_less_eq = (
    Forall((a, x, y),
           LessEq(Log(a, x), Log(a, y)), 
           conditions=[LessEq(x, y), greater(a, one)],
           domain=RealPos))

log_increasing_less_eq (conjecture without proof):

log_base_large_a_greater_one = (
    Forall((a,b),
       greater(Log(a, b), one),
       domain=RealPos,
       condition=number_ordering(Less(one, a), Less(a, b))))

log_base_large_a_greater_one (conjecture without proof):

log_base_large_a_greater_eq_one = (
    Forall((a,b),
       greater_eq(Log(a, b), one),
       domain=RealPos,
       condition=number_ordering(Less(one, a), LessEq(a, b))))

log_base_large_a_greater_eq_one (conjecture without proof):

Some other useful closure theorems should be added here. Notice the pattern of Logs, where all the Logs with positive base $a \ne 1$ go through $(1, 0)$ of course, but we have increasing functions when $a > 1$ and decreasing functions when $0 < a < 1$:

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.logarithms