# Theorems (or conjectures) for the theory of proveit.numbers.integration¶

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, f, l, n, x, P, S, fx
from proveit.core_expr_types import (
x_1_to_n, f__x_1_to_n, P__x_1_to_n)
from proveit.logic import Forall, Implies, InSet
from proveit.numbers import (
one, two, NaturalPos, Real, RealNeg, RealNonPos, RealNonNeg, RealPos)
from proveit.numbers import (Exp, frac, Integrate, IntervalCC, LessEq)
In [2]:
%begin theorems
Defining theorems for theory 'proveit.numbers.integration'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
# Old version of the theorem (maintained temporarily for comparison)
# integration_closure = (
#     Forall((P, S),
#            Implies(Forall(x_etc, InSet(Px_etc, Real), domain=S),
#                    InSet(Integrate(x_etc, Px_etc, domain=S), Real))))
In [4]:
integration_closure = (
Forall(n,
Forall((P, S),
Implies(Forall(x_1_to_n, InSet(P__x_1_to_n, Real), domain=S),
InSet(Integrate(x_1_to_n, P__x_1_to_n, domain=S), Real))),
domain=NaturalPos))
integration_closure (conjecture without proof):

In [5]:
integration_real_neg_closure = (
Forall(n,
Forall((f, S),
Implies(Forall(x_1_to_n, InSet(f__x_1_to_n, RealNeg), domain=S),
InSet(Integrate(x_1_to_n, f__x_1_to_n, domain=S), RealNeg))),
domain=NaturalPos))
integration_real_neg_closure (conjecture without proof):

In [6]:
integration_real_non_pos_closure = (
Forall(n,
Forall((f, S),
Implies(Forall(x_1_to_n, InSet(f__x_1_to_n, RealNonPos), domain=S),
InSet(Integrate(x_1_to_n, f__x_1_to_n, domain=S), RealNonPos))),
domain=NaturalPos))
integration_real_non_pos_closure (conjecture without proof):

In [7]:
integration_real_non_neg_closure = (
Forall(n,
Forall((f, S),
Implies(Forall(x_1_to_n, InSet(f__x_1_to_n, RealNonNeg), domain=S),
InSet(Integrate(x_1_to_n, f__x_1_to_n, domain=S), RealNonNeg))),
domain=NaturalPos))
integration_real_non_neg_closure (conjecture without proof):

In [8]:
integration_real_pos_closure = (
Forall(n,
Forall((f, S),
Implies(Forall(x_1_to_n, InSet(f__x_1_to_n, RealPos), domain=S),
InSet(Integrate(x_1_to_n, f__x_1_to_n, domain=S), RealPos))),
domain=NaturalPos))
integration_real_pos_closure (conjecture without proof):

In [9]:
integration_real_closure = (
Forall(n,
Forall((f, S),
Implies(Forall(x_1_to_n, InSet(f__x_1_to_n, Real), domain=S),
InSet(Integrate(x_1_to_n, f__x_1_to_n, domain=S), Real))),
domain=NaturalPos))
integration_real_closure (conjecture without proof):

(alternate proof for integration_closure)
In [10]:
integration_real_closure_simple = (
Forall((f, S),
Implies(Forall(x, InSet(fx, Real), domain=S),
InSet(Integrate(x, fx, domain=S), Real))))
integration_real_closure_simple (conjecture without proof):

In [11]:
boundedInvSqrdIntegral = (
Forall((a, b),
LessEq(
Integrate(l, frac(one, Exp(l,two)), domain=IntervalCC(a, b)),
frac(one, a)),
domain=RealPos, conditions=[LessEq(a, b)]))
boundedInvSqrdIntegral (conjecture without proof):

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