# 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