logo

Demonstrations for the theory of proveit.numbers.exponentiation

In [1]:
import proveit
from proveit import Literal, used_vars, free_vars
from proveit import a, b, c, d, f, n, x, y
from proveit.logic import And, Boolean, InSet, Equals, NotEquals
from proveit.numbers import zero, one, two, three, four, five, six, frac, num
from proveit.numbers import (Integer, Natural, NaturalPos,
                             Rational, RationalNonZero, RationalPos, Real,
                             RealNonNeg, RealNonPos, RealPos, Complex, ComplexNonZero)
from proveit.numbers import Add, Neg, Div, Exp, greater, greater_eq, Mult, sqrt, subtract
from proveit.numbers.exponentiation import sqrt_of_prod
%begin demonstrations

Exponentiation (Exp) $x^{y}$

Introduction

The `Exp` class allows us to represent exponentiation expressions such as $2^3$, $x^y$, or $(x-3)^2$. This ``_demonstrations_`` notebook explores the `Exp` (exponentiation) class, its axioms and common theorems, and related methods.

Simple Expressions Involving Exponentiation $x^y$

It is straightforward to construct expressions involving exponentiation. Here are some basic examples of such expressions:

In [2]:
# basic expression with exponent
Exp(x, y)
In [3]:
# exponentials involving variables and numbers
example1, example2, example3 = Exp(x, two), Exp(two, three), subtract(one, Exp(a, two))
example1:
example2:
example3:
In [4]:
# A sqrt portrayed with a radical is produced using the special sqrt() call,
# which invokes the Exp() class behind the scenes with special formatting
sqrt(Add(x, two))

Common Attributes of a Subset expression

Let's define a simple example exponential expression, $(x-y)^2$, and look at some of its attributes.

In [5]:
x_minus_y_quantity_squared = Exp(subtract(x,y), two)
x_minus_y_quantity_squared:
In [6]:
x_minus_y_quantity_squared.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4
3Operationoperator: 5
operands: 6
4Literal
5Literal
6ExprTuple7, 8
7Variable
8Operationoperator: 9
operand: 11
9Literal
10ExprTuple11
11Variable

We can access the base and exponent separately, and identify the `Exp` operator as the outermost operation:

In [7]:
x_minus_y_quantity_squared.base
In [8]:
x_minus_y_quantity_squared.exponent
In [9]:
x_minus_y_quantity_squared.operator

We can grab all the components (base and exponent) of the expression simultaneously as a tuple of expressions. We can also get a list of the variables and a separate list of the *free* variables in the expression (of course, in this expression, all the variables are also free variables):

In [10]:
x_minus_y_quantity_squared.operands
In [11]:
used_vars(x_minus_y_quantity_squared)
In [12]:
free_vars(x_minus_y_quantity_squared)

Axioms

The ``axioms`` for the exponentiation theory establish the basic definitions of exponentiation … Actually, right now we have no separate axioms for the exponentiation theory.

Theorems

The ``theorems`` for the exponentiation theory establish many of the basic laws of exponentiation as well as some closure principles.

Demonstrations (TBA)

1. TBA.

We begin with something simple …


2. TBA.

Something else relatively simple …


3. TBA.

Something more complex …

Misc To Be Integrated Into the Demonstration Page

In [13]:
# Some example test expressions involving Exp or sqrt()
exp_test_01, exp_test_02, exp_test_03 = Exp(x, y), Exp(two, three), sqrt(two)
exp_test_01:
exp_test_02:
exp_test_03:

Evaluations

In [14]:
Exp(three, three).evaluation()
 ⊢  

Some testing of closure theorems.

In [15]:
InSet(exp_test_01, NaturalPos).prove(assumptions=[InSet(x, Natural), InSet(y, Natural)])
,  ⊢  
In [16]:
InSet(exp_test_01, Natural).prove(assumptions=[InSet(x, Natural), InSet(y, Natural)])
,  ⊢  
In [17]:
InSet(exp_test_01, Integer).prove(assumptions=[InSet(x, Integer), InSet(y, Natural)])
,  ⊢  
In [18]:
InSet(exp_test_01, Rational).prove(assumptions=[InSet(x, Rational), InSet(y, Natural)])
,  ⊢  
In [19]:
InSet(exp_test_01, Rational).prove(assumptions=[InSet(x, RationalNonZero), InSet(y, Integer)])
,  ⊢  
In [20]:
InSet(exp_test_01, RationalNonZero).prove(assumptions=[InSet(x, RationalNonZero), InSet(y, Integer)])
,  ⊢  
In [21]:
InSet(exp_test_01, RationalPos).prove(assumptions=[InSet(x, RationalPos), InSet(y, Integer)])
,  ⊢  
In [22]:
InSet(exp_test_01, Real).prove(assumptions=[InSet(x, Real), InSet(y, Natural)])
,  ⊢  
In [23]:
InSet(exp_test_01, Real).prove(assumptions=[InSet(x, RealPos), InSet(y, Integer)])
,  ⊢  
In [24]:
InSet(exp_test_01, RealPos).prove(assumptions=[InSet(x, RealPos), InSet(y, Integer)])
,  ⊢  
In [25]:
InSet(exp_test_01, RealNonNeg).prove(assumptions=[InSet(x, RealNonNeg), InSet(y, Integer)])
,  ⊢  
In [26]:
InSet(Exp(x, frac(one, two)), RealNonNeg).prove(assumptions=[InSet(x, RealNonNeg)])
 ⊢  
In [27]:
InSet(exp_test_01, Complex).prove(assumptions=[InSet(x, Complex), InSet(y, Complex)])
,  ⊢  
In [28]:
InSet(exp_test_01, ComplexNonZero).prove(assumptions=[InSet(x, ComplexNonZero), InSet(y, Complex)])
,  ⊢  
In [29]:
InSet(Exp(three, two), RealPos).prove()
 ⊢  
In [30]:
exp_test_03
In [31]:
InSet(exp_test_03, RealPos).prove()
 ⊢  
In [32]:
InSet(two, RealPos).prove()
 ⊢  
In [33]:
two_in_real_k_t = InSet(two, Real).prove()
two_in_real_k_t:  ⊢  
In [34]:
two_in_real_k_t.proof()
 step typerequirementsstatement
0instantiation1, 2, 3  ⊢  
  : , : , :
1reference6  ⊢  
2conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
3instantiation6, 4, 5  ⊢  
  : , : , :
4conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
5instantiation6, 7, 8  ⊢  
  : , : , :
6theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
7conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
8conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat2
In [35]:
sqrt2_is_complex = InSet(exp_test_03, Complex).prove()
sqrt2_is_complex:  ⊢  
In [36]:
t_ = Literal('t')
two_to_power_t = Exp(two, t_)
two_to_power_t:
In [37]:
InSet(two_to_power_t, NaturalPos).prove(assumptions=[InSet(t_, NaturalPos)])
 ⊢  

Testing the formatting of some Exp() and sqrt() outputs

In [38]:
InSet(exp_test_03, RealPos).prove()
 ⊢  
In [39]:
Exp(x, frac(one, two))
In [40]:
sqrt_test = sqrt(Add(one, frac(a, b)))
sqrt_test:
In [41]:
sqrt_test
In [42]:
Add(two, sqrt_test)

Testing the Mult.combining_exponents() method (after eliminating Sqrt class)

In [43]:
mult_of_exps_test_01 = Mult(Exp(a, b), Exp(a, c))
mult_of_exps_test_01:
In [44]:
mult_of_exps_test_02 = Mult(sqrt(two), sqrt(two))
mult_of_exps_test_02:
In [45]:
mult_of_exps_test_03 = Mult(Exp(two, b), sqrt(two))
mult_of_exps_test_03:
In [46]:
mult_of_exps_test_01.combining_exponents(assumptions=[InSet(a, RealPos), InSet(b, Complex), InSet(c, Complex), NotEquals(a, zero)])
, ,  ⊢  
In [47]:
mult_of_exps_test_02.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 3
3Operationoperator: 4
operands: 5
4Literal
5ExprTuple10, 6
6Operationoperator: 7
operands: 8
7Literal
8ExprTuple9, 10
9Literal
10Literal
In [48]:
mult_of_exps_test_02.combining_exponents(auto_simplify=False)
 ⊢  
In [49]:
mult_of_exps_test_02.combining_exponents()
 ⊢  
In [50]:
mult_of_exps_test_03.combining_exponents(assumptions=[InSet(b, Complex), InSet(frac(one, two), Complex), NotEquals(two, zero)])
,  ⊢  

Testing Exp.exponent_separation()

In [51]:
expr_01, expr_02, expr_03, expr_04 = (
    Exp(a, b), Exp(a, Add(b, c)), Exp(a, Add(b, c, d)), Exp(two, Add(one, two, c)))
expr_01:
expr_02:
expr_03:
expr_04:
In [52]:
# some general assumptions
temp_assumptions = [InSet(a, RealPos), InSet(b, RealPos),
                    InSet(c, RealPos), InSet(d, RealPos)]
temp_assumptions:
In [53]:
# nothing to do if the exponent is not a sum:
try:
    expr_01.exponent_separation()
except Exception as the_exception:
    print("Error: {}".format(the_exception))

Error: 'Exp.exponent_separation()' implemented only for cases in which the exponent appears as a sum (i.e. in the Add class). The exponent in this case is b.
In [54]:
# a 2-addend exponent
expr_02.exponent_separation(assumptions=temp_assumptions)
, ,  ⊢  
In [55]:
# a 3-addend exponent
expr_03.exponent_separation(assumptions=temp_assumptions)
, , ,  ⊢  
In [56]:
# a 3-addend exponent
expr_04.exponent_separation(assumptions=temp_assumptions)
 ⊢  

Testing Exp.factorization()

In [57]:
factorization_assumptions = [InSet(a, Real), InSet(b, Real)]
factorization_assumptions:
In [58]:
exp_a_b = Exp(a, b)
exp_a_b:
In [59]:
# when the desired factor supplied is just the expression itself
exp_a_b.factorization(Exp(a, b), assumptions = factorization_assumptions)
 ⊢  
In [60]:
# when the desired factor supplied is just the base itself
# and the base is known to be a non-zero Real
exp_a_b.factorization(
        a,
        assumptions = [InSet(a, Real), InSet(b, Integer), NotEquals(a, zero)])
, ,  ⊢  
In [61]:
# when the desired factor supplied is just the base itself
# and the base is known to be in RealPos
exp_a_b.factorization(
        a,
        assumptions = [InSet(a, RealPos), InSet(b, Integer)])
,  ⊢  
In [62]:
# and a more concrete case, illustrating the simplification
# of the resulting exponent(s) in the factors. Yay!
Exp(a, four).factorization(
        a,
        assumptions = [InSet(a, RealPos)])
 ⊢  
In [63]:
# and a case like we encounter in the QPE package. Yay!
from proveit.physics.quantum.QPE import _t
Exp(two, _t).factorization(two, assumptions = [InSet(_t, NaturalPos)])
 ⊢  
In [64]:
# now we can do some simple Div.cancelation() involving Exp class
Div(Exp(two, _t), two).cancelation(two, assumptions = [InSet(_t, NaturalPos)])
 ⊢  
In [65]:
# and a special case
Exp(two, one).factorization(two)
 ⊢  
In [66]:
# more generally, factor out a^c from a^b
Exp(a, b).factorization(
        Exp(a, c),
        assumptions = [InSet(a, RealPos), InSet(b, Integer), InSet(c, Integer)])
, ,  ⊢  
In [67]:
# Even more generally, factor out a^d from (a*b)^c
Exp(Mult(a, b), c).factorization(
        a, pull='left',
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos)])
, ,  ⊢  
In [68]:
# Pull to the right
Exp(a, c).factorization(
        a, pull='right', group_remainder=True,
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos)])
,  ⊢  
In [69]:
Exp(Mult(a, b), c).factorization(
        a, pull='right', group_remainder=True,
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos)])
, ,  ⊢  
In [70]:
Exp(Mult(a, b), c).factorization(
        Exp(a, c),
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos), InSet(d, Integer)])
, ,  ⊢  
In [71]:
Exp(Mult(a, b), c).factorization(
        Exp(a, c), pull='right', group_remainder=True,
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos), InSet(d, Integer)])
, ,  ⊢  
In [72]:
Exp(Mult(a, b), c).factorization(
        Exp(a, d), pull='right',
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos), InSet(d, Integer)])
, , ,  ⊢  
In [73]:
Exp(Mult(a, b), c).factorization(
        Exp(a, d), group_remainder=True,
        assumptions = [InSet(a, RealPos), InSet(b, Integer), 
                       InSet(c, RealPos), InSet(d, Integer)])
, , ,  ⊢  

Testing Exp.distribution()

In [74]:
expr_mult_02, expr_mult_03 = (
    Exp(Mult(a, b), f),
    Exp(Mult(a, b, c), f))
expr_mult_02:
expr_mult_03:
In [75]:
# some general assumptions
temp_assumptions = [InSet(a, RealPos), InSet(b, NaturalPos), InSet(c, RealPos),
                    InSet(d, RealPos), InSet(f, Complex),
                    NotEquals(a, zero), NotEquals(b, zero), NotEquals(c, zero)]
temp_assumptions:
In [76]:
expr_mult_02.distribution(assumptions=temp_assumptions)
, ,  ⊢  
In [77]:
expr_mult_03.distribution(assumptions=temp_assumptions)
, , ,  ⊢  
In [78]:
expr_div_02 = Exp(Div(a, b), f)
expr_div_02:
In [79]:
expr_div_02.distribution(assumptions=temp_assumptions)
, ,  ⊢  
In [80]:
expr_exp_02 = Exp(Exp(a, b), f)
expr_exp_02:
In [81]:
expr_exp_02.distribution(assumptions=temp_assumptions)
 ⊢  

Testing Exp.bound_via_operand_bound() for $x^a$ where we know a relation for base $x$

In [82]:
from proveit import a, b, c, d, u, v, w, x, y, z, defaults
from proveit.numbers import greater, greater_eq, Less, LessEq, RealNeg, RealNonNeg
defaults.assumptions = [InSet(a, RealPos), InSet(b, RealNonNeg), InSet(c, RealNeg),
                        InSet(d, RealNonPos), InSet(u, RealNeg), InSet(v, RealNeg),
                        InSet(x, Real), InSet(y, Real), InSet(z, Real),
                        InSet(w, RealPos), Less(u, v), LessEq(u, c),
                        greater(x, zero), greater(y, x), LessEq(x, z)]
defaults.assumptions:
In [83]:
exp_x_a, exp_x_b, exp_x_c, exp_x_d, exp_u_2 = Exp(x, a), Exp(x, b), Exp(x, c), Exp(x, d), Exp(u, two)
exp_x_a:
exp_x_b:
exp_x_c:
exp_x_d:
exp_u_2:
In [84]:
# Case (1): pos exponent, Less relation
exp_x_a.bound_via_operand_bound(Less(x, y))
, , , ,  ⊢  
In [85]:
# Case (2): pos exponent, LessEq relation
exp_x_a.bound_via_operand_bound(LessEq(x, z))
, , , ,  ⊢  
In [86]:
# Case (3): non-neg exponent, Less relation
exp_x_b.bound_via_operand_bound(Less(x, y))
, , , ,  ⊢  
In [87]:
# Case (4): non-neg exponent, LessEq relation
exp_x_b.bound_via_operand_bound(LessEq(x, z))
, , , ,  ⊢  
In [88]:
# Case (5): neg exponent, Less relation
exp_x_c.bound_via_operand_bound(Less(x, y))
, , , ,  ⊢  
In [89]:
# Case (6): neg exponent, LessEq relation
exp_x_c.bound_via_operand_bound(LessEq(x, z))
, , , ,  ⊢  
In [90]:
# Case (7): non-pos exponent, Less relation
exp_x_d.bound_via_operand_bound(Less(x, y))
, , , ,  ⊢  
In [91]:
# Case (8): non-pos exponent, LessEq relation
exp_x_d.bound_via_operand_bound(LessEq(x, z))
, , , ,  ⊢  
In [92]:
# Case (9): exponent = 2, Less relation, negative base
exp_u_2.bound_via_operand_bound(Less(u, v))
, ,  ⊢  
In [93]:
# Case (10): exponent = 2, LessEq relation, negative base
exp_u_2.bound_via_operand_bound(LessEq(u, c))
, ,  ⊢  
In [94]:
# more concrete case
Exp(w, two).bound_via_operand_bound(LessEq(w, two),
            assumptions = defaults.assumptions + (LessEq(w, two),))
,  ⊢  
In [95]:
# more concrete case
from proveit.numbers import four
Exp(w, frac(one, two)).bound_via_operand_bound(LessEq(w, four),
            assumptions = defaults.assumptions + 
                (LessEq(w, four), greater(frac(one, two), zero)))
, ,  ⊢  
In [96]:
# more concrete case
from proveit.numbers import four
Exp(w, three).bound_via_operand_bound(greater(w, four),
            assumptions = defaults.assumptions + 
                (greater(w, four),))
,  ⊢  

Testing Exp.bound_via_operand_bound() for $a^x$ where we know a relation for exponent $x$

In [97]:
from proveit import a, b, c, d, u, v, w, x, y, z, defaults
from proveit.numbers import greater, greater_eq, Less, LessEq, RealNeg, RealNonNeg
defaults.assumptions = [greater(a, one), greater(b, one), greater(c, one), greater(d, one),
                        InSet(a, Real), InSet(b, Real), InSet(c, Real),
                        InSet(d, Real), InSet(u, Real), InSet(v, Real), InSet(w, Real),
                        InSet(x, Real), InSet(y, Real), InSet(z, Real),
                        Less(x, y), LessEq(x, z), greater(x, v), greater_eq(x, w)]
defaults.assumptions:
In [98]:
exp_a_x, exp_b_x, exp_c_x, exp_d_x, exp_2_u = Exp(a, x), Exp(b, y), Exp(c, z), Exp(d, x), Exp(two, u)
exp_a_x:
exp_b_x:
exp_c_x:
exp_d_x:
exp_2_u:
In [99]:
# Case (1): base > 1, Less relation
exp_a_x.bound_via_operand_bound(Less(x, y))
, , , ,  ⊢  
In [100]:
# Case (2): base > 1, LessEq relation
exp_a_x.bound_via_operand_bound(LessEq(x, z))
, , , ,  ⊢  
In [101]:
# Case (3): base > 1, greater relation
exp_a_x.bound_via_operand_bound(greater(x, v))
, , , ,  ⊢  
In [102]:
# Case (4): base > 1, greater_eq relation
exp_a_x.bound_via_operand_bound(greater_eq(x, w))
, , , ,  ⊢  

Testing Exp.power_of_log_reduction()

In [103]:
from proveit.numbers import Log
Exp(a, Log(a,x)).power_of_log_reduction(assumptions=[InSet(a, RealPos), InSet(x, RealPos), NotEquals(a, one)])
, ,  ⊢  
In [104]:
Exp(two, Log(two, Add(x, two))).power_of_log_reduction(
    assumptions=[InSet(x, Real), greater(x, two)])
,  ⊢  

Testing Exp.shallow_simplification()

In [105]:
Exp(two, Add(x, y, Neg(two))).canonical_form()
In [106]:
Exp(two, Add(x, y, Neg(two))).shallow_simplification(assumptions=[InSet(x, Complex), InSet(y, Complex)])
 ⊢  
In [107]:
Exp(a, Log(a,x)).shallow_simplification(assumptions=[InSet(a, RealPos), InSet(x, RealPos), NotEquals(a, one)])
, ,  ⊢  
In [108]:
Exp(two, Log(two, Add(x, two))).shallow_simplification(
    assumptions=[InSet(x, Real), greater(x, two)])
,  ⊢  

Even power exponentiation is an even function which is exploited in canonical forms

In [109]:
Exp(Add(a, Neg(b), Neg(c)), four).canonical_form() == Exp(Add(b, c, Neg(a)), four).canonical_form() 

True
In [110]:
Equals(Exp(Add(a, Neg(b), Neg(c)), four), Exp(Add(b, c, Neg(a)), four)).prove(
    assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
, ,  ⊢  
In [111]:
%end demonstrations