logo

Demonstrations for the theory of proveit.numbers.integration

In [1]:
import proveit
from proveit import f, x, y, S, fx, fy, Px, Py, defaults
from proveit.logic import And, Forall, InSet
from proveit.numbers import Integrate
from proveit.numbers import (
        zero, one, Real, RealNeg, RealNonNeg, RealNonPos, RealPos,
        IntervalCC, IntervalOC)
%begin demonstrations

Basic Testing: Creating Definite Integrals, Accessing Properties

In [2]:
integral_Px_over_S = Integrate(x, Px, domain=S)
integral_Px_over_S:
In [3]:
integral_Px_over_S.domain
In [4]:
integral_Px_over_S.index
In [5]:
integral_Px_over_S.integrand
In [6]:
# Utilizing pre-defined set for domain
for the_domain in [Real, RealNeg, RealNonNeg, RealNonPos, RealPos]:
    display(Integrate(x, Px, domain=the_domain))
In [7]:
# This is wrong! Should be expressed a limit.
Integrate(x, Px, domain=IntervalOC(zero, one))

Testing closure: deduce_in_number_set()

In [8]:
# some default assumptions to help with testing
defaults.assumptions = [InSet(x, S), InSet(x, Real), InSet(y, S)]
defaults.assumptions:
In [9]:
# define a few integrals
from proveit import a, b
from proveit.numbers import IntervalCC
integral_fx_over_S, integral_fy_over_S, integral_fx_over_real, integral_fx_over_interval = (
    Integrate(x, fx, domain=S),
    Integrate(y, fy, domain=S),
    Integrate(x, fx, domain=Real),
    Integrate(x, fx, domain=IntervalCC(a, b)))
integral_fx_over_S:
integral_fy_over_S:
integral_fx_over_real:
integral_fx_over_interval:
In [10]:
from proveit import e, l, t
from proveit.numbers import one, two, Exp, frac, subtract
integral_fx_over_fail_interval, integral_fofell_over_fail_interval = (
    Integrate(x, fx, domain=IntervalCC(e, subtract(Exp(two, subtract(t, one)), one))),
    Integrate(l, frac(one, Exp(l, two)), domain=IntervalCC(e, subtract(Exp(two, subtract(t, one)), one))))
integral_fx_over_fail_interval:
integral_fofell_over_fail_interval:
In [11]:
integral_fx_over_S.domain
In [12]:
integral_fx_over_S.instance_params

Working here on details of instantiation of the real_closure theorem

In [13]:
integral_fx_over_real
In [14]:
from proveit.logic import Equals
from proveit.numbers import infinity, Neg, IntervalOO
integral_fx_over_real.deduce_in_number_set(
    Real,
    assumptions=defaults.assumptions+(Equals(IntervalOO(Neg(infinity), infinity), Real), InSet(fx, Real), Forall(x, InSet(fx, Real), domain=Real),))
 ⊢  
In [15]:
integral_fx_over_S.deduce_in_number_set(
    Real,
    assumptions=defaults.assumptions+(Forall(x, InSet(fx, Real), conditions=[InSet(x, S)]),))
 ⊢  
In [16]:
from proveit.numbers.integration import integration_real_closure
integration_real_closure
 ⊢  
In [17]:
# experimenting with the instantiation --
from proveit import n, f, S, x
self = integral_fx_over_interval
_x_sub = self.instance_params
_f_sub = Lambda(_x_sub, self.instance_expr)
_S_sub = self.domain
_n_sub = _x_sub.num_elements()
integration_real_closure.instantiate(
        {n: _n_sub, f: _f_sub, S: _S_sub, x: _x_sub})
 ⊢  
In [18]:
# experimenting with the instantiation --
from proveit import n, f, S, x
self = integral_fofell_over_fail_interval
_x_sub = self.instance_params
_f_sub = Lambda(_x_sub, self.instance_expr)
_S_sub = self.domain
_n_sub = _x_sub.num_elements()
integration_real_closure.instantiate(
        {n: _n_sub, f: _f_sub, S: _S_sub, x: _x_sub})
 ⊢  
In [19]:
%end demonstrations