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

In [1]:
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

In [2]:
%begin theorems

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

In [3]:
log_real_pos_real_closure = Forall((a,b),
InSet(Log(a, b), Real),
domain=RealPos,
condition=NotEquals(a, one))

Out[3]:
log_real_pos_real_closure (conjecture without proof):

In [4]:
log_eq_1 = Forall(a,
Equals(Log(a, a), one),
domain=RealPos)

Out[4]:
log_eq_1 (conjecture without proof):

In [5]:
log_real_pos_from_gt_1 = Forall((a,b),
InSet(Log(a, b), RealPos),
domain=RealPos,
condition=greater(a, one))

Out[5]:
log_real_pos_from_gt_1 (conjecture without proof):

In [6]:
log_real_nonneg_from_geq_1 = Forall((a,b),
InSet(Log(a, b), RealNonNeg),
domain=RealPos,
condition=greater_eq(a, one))

Out[6]:
log_real_nonneg_from_geq_1 (conjecture without proof):

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

Out[7]:
log_increasing_less (conjecture without proof):

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

Out[8]:
log_increasing_less_eq (conjecture without proof):

In [9]:
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))))

Out[9]:
log_base_large_a_greater_one (conjecture without proof):

In [10]:
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))))

Out[10]:
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$:

In [11]:
%end theorems

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