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

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)

%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.

prob_in_interval = Forall(Omega, Forall(x, InSet(Prob(x), prob_domain),
                                        domain=Omega),
                          domain=SampleSpaces)

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.

prob_sum_is_one = Forall(Omega, Equals(Sum(x, Prob(x), domain=Omega),
                                       one),
                         domain=SampleSpaces)

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

event_prob_in_interval = Forall(Omega, Forall(X, InSet(Prob(X), prob_domain),
                                              condition=SubsetEq(X, Omega)),
                                domain=SampleSpaces)

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.

sample_space_via_bijections = Forall(
    Omega, Forall(
        (X, Y), Forall(
            (f, g),
            Implies(Forall(x, Equals(Prob(fx), Prob(gx)),
                           domain=X),
                    InClass(Y, SampleSpaces))
            .with_wrap_before_operator(),
            domains=(Bijections(X, Omega), Bijections(X, Y)))),
    domain=SampleSpaces)

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

subset_event_prob_bound = Forall(
    Omega, Forall(
        (A, B), LessEq(Prob(A), Prob(B)),
        condition=total_ordering(SubsetEq(A, B), 
                                 SubsetEq(B, Omega))),
    domain=SampleSpaces)

prob_of_all_as_sum = Forall(
    Omega, Forall(
        X, Forall(
            f, Forall(
                Q, 
                Equals(ProbOfAll(x, fx, domain=X, condition=Qx),
                       Sum(x, Prob(fx), domain=X, condition=Qx))
                .with_wrap_after_operator()),
            domain=Injections(X, Omega))),
    domain=SampleSpaces)

constrained_event_prob_bound = Forall(
    Omega, Forall(
        X, Forall(
            f, 
            Forall(
                (Q, R), 
                Implies(
                    Forall(x, Rx, domain=X, condition=Qx),
                    LessEq(ProbOfAll(x, fx, domain=X,
                                     condition=Qx),
                           ProbOfAll(x, fx, domain=X,
                                     condition=Rx))
                    .with_wrap_after_operator()
                ).with_wrap_after_operator()),
            domain=Functions(X, Omega)).with_wrapping()),
    domain=SampleSpaces)

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)])
        .with_wrapping()),
    domain=SampleSpaces)

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

prob_of_disjoint_events_is_prob_sum = Forall(
    Omega, Forall(
        (A, B, C, X, Q), Forall(
            f, 
            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)])
        .with_wrapping(),
    domain=SampleSpaces)

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

complementary_event_prob = Forall(Omega, Forall(S, Equals(Prob(Difference(Omega, S)), 
                                                          subtract(one, Prob(S))),
                                                condition=SubsetEq(S, Omega)),
                                  domain=SampleSpaces)

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)))
                        .with_wrap_after_operator())
                .with_wrap_after_operator()),
            domain=Bijections(X, Omega))),
    domain=SampleSpaces)

%end theorems

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

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

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