from proveit import Function, Literal, relation_prover, equality_prover
from proveit import a
from proveit.numbers import (deduce_number_set, NumberOperation,
readily_provable_number_set)
[docs]class Log(NumberOperation, Function):
# operator of the Log operation.
_operator_ = Literal(string_format='log', latex_format=r'\textrm{log}',
theory=__file__)
def __init__(self, base, antilog, *, styles=None):
Function.__init__(self, Log._operator_, (base, antilog),
styles=styles)
self.base = base
self.antilog = antilog
[docs] def string(self, **kwargs):
return Log._operator_.string() + "_%s(%s)"%(
self.base.string(), self.antilog.string())
[docs] def latex(self, **kwargs):
return Log._operator_.latex() + r"_%s\left(%s\right)"%(
self.base.latex(), self.antilog.latex())
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
if self.base == self.antilog:
from . import log_eq_1
return log_eq_1.instantiate({a:self.base})
return NumberOperation.shallow_simplification(
self, must_evaluate=must_evaluate)
@relation_prover
def deduce_in_number_set(self, number_set, **defaults_config):
'''
Attempt to prove that the logarithmic expression 'self' is
in the given number set 'number_set'. May require user to
previously show or assume that the Log base is not 1.
Currently implemented only for the general case, giving
Log_a(b) in Real when 'a' and 'b' both in RealPos and 'a' != 1.
This can be augmented in near future.
'''
from proveit import a, b
from proveit.logic import InSet, NotEquals
from proveit.numbers.logarithms import log_real_pos_real_closure
from proveit.numbers import zero, Real
if number_set == Real:
return log_real_pos_real_closure.instantiate(
{a: self.base, b: self.antilog})
# we can do more/better but that's enough for right now
raise NotImplementedError(
"'Log.deduce_in_number_set()' not implemented for the "
" number set {0}. Try deducing in Real instead?".
format(number_set))
@relation_prover
def bound_via_operand_bound(self, operand_relation, **defaults_config):
'''
For simple cases, deduce a bound on this Logarithmic (Log)
object given a bound on its operand. For example, suppose
x = Log(2, y) and we know that y >= 2. Then
x.bound_via_operand_bound(y >= 2) returns x >= Log(2, 2) = 1.
This method currently works MAINLY for expressions of the
form Log(a, b) where a > 1, where we know something of the
form b < y or b <= y or b > y or b >= y involving the 'antilog'
argument b. b itself will also need to be in RealPos, which
might need to be pre-proven or provided as an assumption.
Future development should address cases where 0 < a < 1,
which result in decreasing logarithmic functions.
Also see NumberOperation.deduce_bound() and compare to the
bound_via_operand_bound() method found in the Div, Neg, and
Exp classes.
'''
from proveit import Judgment
from proveit import a, x, y
from proveit.numbers import (
zero, one,
two, greater, greater_eq, Less, LessEq,
NumberOrderingRelation, RealNonNeg)
if isinstance(operand_relation, Judgment):
operand_relation = operand_relation.expr
if not isinstance(operand_relation, NumberOrderingRelation):
raise TypeError(
"In Exp.bound_via_operand_bound(), the "
"'operand_relation' argument is expected to be a number "
"relation (<, >, ≤, or ≥), but instead was {}.".
format(operand_relation))
lhs = operand_relation.lhs
# should be able to generalize this later
# no need to limit to just lhs, right?
if lhs != self.antilog:
raise ValueError(
"In Log.bound_via_operand_bound(), the left side of "
"the 'operand_relation' argument {0} is expected to "
"match the Log antilog operand {1}.".
format(operand_relation, self.antilog))
# assign x and y subs according to std Less or LessEq relations
_x_sub = operand_relation.normal_lhs
_y_sub = operand_relation.normal_rhs
_a_sub = self.base
# Multiple cases to eventually consider but for now
# we only consider four related Log(a, x) vs. Log(a, y)
# cases for the increasing (base a > 1) version of a Log fxn:
# (1) base a > 1, 0 < x < y
# (2) base a > 1, 0 < x <= y
# (3) base a > 1, 0 < y < x
# (4) base a > 1, 0 < y <= x
# Cases (1)-(4): 0 < x < y or 0 < y < x
if ( greater(_a_sub, one).readily_provable()
and greater(_x_sub, zero).readily_provable() ):
if isinstance(operand_relation, Less):
from proveit.numbers.logarithms import (
log_increasing_less)
bound = log_increasing_less.instantiate(
{x: _x_sub, y: _y_sub, a: _a_sub})
elif isinstance(operand_relation, LessEq):
from proveit.numbers.logarithms import (
log_increasing_less_eq)
bound = log_increasing_less_eq.instantiate(
{x: _x_sub, y: _y_sub, a: _a_sub})
else:
raise TypeError(
"In Log.bound_via_operand_bound(), the 'operand_relation' "
"argument is expected to be a 'Less', 'LessEq', 'greater', "
"or 'greater_eq' relation. Instead we have {}.".
format(operand_relation))
else:
raise ValueError(
"In calling Log.bound_via_operand_bound(), a "
"specific matching case was not found for {0}. "
"Check/confirm that {1} > 1 and {2} is a positive "
"Real".
format(self, _a_sub, _x_sub))
if bound.rhs == self:
return bound.with_direction_reversed()
return bound
def readily_provable_number_set(self):
'''
Return the most restrictive number set we can readily
prove contains the evaluation of this number operation.
'''
from proveit.numbers import Real, RealPos, Complex
base_ns = readily_provable_number_set(self.base)
antilog_ns = readily_provable_number_set(self.antilog)
if RealPos.readily_includes(base_ns) and (
RealPos.readily_includes(antilog_ns)):
return Real
if base_ns is None or antilog_ns is None: return None
return Complex