logo

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$: image.png

In [11]:
%end theorems
These theorems may now be imported from the theory package: proveit.numbers.logarithms