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

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)

%begin theorems

Defining theorems for theory 'proveit.numbers.integration'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

# 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))))

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):

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):

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):

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):

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):

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)

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):

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):

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.integration