Axioms for the theory of proveit.statistics

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import f, x, Q, X, Omega, fx, Qx
from proveit.logic import (And, Forall, Equals, InSet, InClass,
                           SubsetEq, SetOfAll, Functions)
from proveit.numbers import zero, one, Sum
from proveit.statistics import (
    SampleSpaces, Prob, prob_domain, ProbOfAll)

%begin axioms

Defining axioms for theory 'proveit.statistics'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Define a sample space

A sample space is a set of samples whose probabilities are between 0 and 1 and whose sum of probabilities, over all samples, is equal to 1.

samples_space_def = Forall(
    Omega, 
    Equals(InClass(Omega, SampleSpaces),
           And(Forall(x, InSet(Prob(x), prob_domain),
                      domain=Omega),
               Equals(Sum(x, Prob(x), domain=Omega),
                      one))).with_wrap_after_operator())

samples_space_def:

An event is a subset of the sample space. The probability of the event is the sum of probabilities of the samples contained in the event.

event_prob_def = Forall(
    Omega, Forall(
        X, Equals(Prob(X), Sum(x, Prob(x), domain=X)),
        condition=SubsetEq(X, Omega)),
    domain=SampleSpaces)

event_prob_def:

ProbOfAll is the probability of an event (a sample space subset)

prob_of_all_def = Forall(
    Omega, Forall(
        X, Forall(
            f, Forall(
                Q, 
                Equals(ProbOfAll(x, fx, domain=X, condition=Qx),
                       Prob(SetOfAll(x, fx, domain=X, condition=Qx)))
                .with_wrap_after_operator()),
            domain=Functions(X, Omega))),
    domain=SampleSpaces)

prob_of_all_def:

%end axioms

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