Theorems (or conjectures) for the theory of proveit.statistics

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, g, x, y, A, B, C, Q, R, S, X, Y, fx, fy, gx, gy,
                     Qx, Rx, Ry, Omega, Function)
from proveit.relation import total_ordering
from proveit.logic import (Not, Forall, Implies, Equals, InSet, InClass, Union,
                           SubsetEq, SetOfAll, Difference, Disjoint, 
                           Functions, Injections, Bijections)
from proveit.numbers import (one, Add, subtract, LessEq, greater_eq, 
                             Real, Sum, Natural)
from proveit.statistics import (
    Prob, SampleSpaces, prob_domain, ProbOfAll)
In [2]:
%begin theorems
Defining theorems for theory 'proveit.statistics'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

If $X$ is a sample from a sample space, then its probability must be between zero and one, inclusively.

In [3]:
prob_in_interval = Forall(Omega, Forall(x, InSet(Prob(x), prob_domain),
prob_in_interval (conjecture without proof):

The sum of probabilities of samples over all of the samples in a sample space must equal to 1 by the definition of a sample space.

In [4]:
prob_sum_is_one = Forall(Omega, Equals(Sum(x, Prob(x), domain=Omega),
prob_sum_is_one (conjecture without proof):

The probability of an event (a set of samples) must be between 0 and 1.

In [5]:
event_prob_in_interval = Forall(Omega, Forall(X, InSet(Prob(X), prob_domain),
                                              condition=SubsetEq(X, Omega)),
event_prob_in_interval (conjecture without proof):

We can prove that something is a sample space via bijections. One bijection maps onto a known sample space and the other maps to something with equal probabilities as the first.

In [6]:
sample_space_via_bijections = Forall(
    Omega, Forall(
        (X, Y), Forall(
            (f, g),
            Implies(Forall(x, Equals(Prob(fx), Prob(gx)),
                    InClass(Y, SampleSpaces))
            domains=(Bijections(X, Omega), Bijections(X, Y)))),
sample_space_via_bijections (conjecture without proof):

We can bound an event probability via a subset event probability.

In [7]:
subset_event_prob_bound = Forall(
    Omega, Forall(
        (A, B), LessEq(Prob(A), Prob(B)),
        condition=total_ordering(SubsetEq(A, B), 
                                 SubsetEq(B, Omega))),
subset_event_prob_bound (conjecture without proof):

In [ ]:
In [8]:
prob_of_all_as_sum = Forall(
    Omega, Forall(
        X, Forall(
            f, Forall(
                Equals(ProbOfAll(x, fx, domain=X, condition=Qx),
                       Sum(x, Prob(fx), domain=X, condition=Qx))
            domain=Injections(X, Omega))),
prob_of_all_as_sum (conjecture without proof):

In [9]:
constrained_event_prob_bound = Forall(
    Omega, Forall(
        X, Forall(
                (Q, R), 
                    Forall(x, Rx, domain=X, condition=Qx),
                    LessEq(ProbOfAll(x, fx, domain=X,
                           ProbOfAll(x, fx, domain=X,
            domain=Functions(X, Omega)).with_wrapping()),
constrained_event_prob_bound (conjecture without proof):

In [ ]:
In [10]:
prob_of_all_events_transformation = Forall(
    Omega, Forall(
        (A, B, Q), Forall(
            (f, g), 
            Equals(ProbOfAll(x, fx, domain=A, condition=Qx),
                   ProbOfAll(y, Function(f, gy), domain=B,
                            condition=Function(Q, gy))),
            domains=[Injections(A, Omega), Bijections(B, A)])
prob_of_all_events_transformation (conjecture without proof):

If events are disjoint, the probability of the union event is the sum of the distinct events.

In [11]:
prob_of_disjoint_events_is_prob_sum = Forall(
    Omega, Forall(
        (A, B, C, X, Q), Forall(
            Equals(ProbOfAll(x, fx, domain=C, condition=Qx),
                   Add(ProbOfAll(x, fx, domain=A, condition=Qx),
                       ProbOfAll(x, fx, domain=B, condition=Qx))),
            domain=Injections(X, Omega)),
        conditions=[SubsetEq(C, X), Equals(C, Union(A, B)), Disjoint(A, B)])
prob_of_disjoint_events_is_prob_sum (conjecture without proof):

The probability of the complement of an event $E$ is 1 - $Prob(E)$.

In [12]:
complementary_event_prob = Forall(Omega, Forall(S, Equals(Prob(Difference(Omega, S)), 
                                                          subtract(one, Prob(S))),
                                                condition=SubsetEq(S, Omega)),
complementary_event_prob (conjecture without proof):

In [13]:
complementary_event_prob_of_all = Forall(
    Omega, Forall(
        X, Forall(
            f, Forall(
                (Q, R),
                Implies(Forall(x, Equals(Qx, Not(Rx)), domain=X),
                        Equals(ProbOfAll(x, fx, domain=X, condition=Qx), 
                               subtract(one, ProbOfAll(y, fy, domain=X, condition=Ry)))
            domain=Bijections(X, Omega))),
complementary_event_prob_of_all (conjecture without proof):

In [14]:
%end theorems
These theorems may now be imported from the theory package: proveit.statistics