Theory "real_probability"

Parents real_lebesgue

Signature

Constant	Type
cond_prob	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> (α -> bool) -> real
conditional_distribution	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> β) -> (α -> γ) -> (β -> bool) -> (γ -> bool) -> real
conditional_expectation	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> ((α -> bool) -> bool) -> α -> real
conditional_prob	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> ((α -> bool) -> bool) -> α -> real
distribution	:(β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (β -> α) -> (α -> bool) -> real
events	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
expectation	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> real) -> real
indep	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> (α -> bool) -> bool
indep_families	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> ((α -> bool) -> bool) -> ((α -> bool) -> bool) -> bool
indep_function	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> β # α) -> bool
indep_rv	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> β) -> (α -> γ) -> β algebra -> γ algebra -> bool
joint_distribution	:(γ -> bool) # ((γ -> bool) -> bool) # ((γ -> bool) -> real) -> (γ -> α) -> (γ -> β) -> (α # β -> bool) -> real
joint_distribution3	:(δ -> bool) # ((δ -> bool) -> bool) # ((δ -> bool) -> real) -> (δ -> α) -> (δ -> β) -> (δ -> γ) -> (α # β # γ -> bool) -> real
p_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> α -> bool
possibly	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
prob	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> real
prob_preserving	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (α -> β) -> bool
prob_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
probably	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
random_variable	:(α -> β) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> β algebra -> bool
real_random_variable	:(α -> real) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
rv_conditional_expectation	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> β algebra -> (α -> real) -> (α -> β) -> α -> real
uniform_distribution	:β -> γ -> δ algebra -> (α -> bool) -> real

Definitions

cond_prob_def

⊢ ∀p e1 e2. cond_prob p e1 e2 = prob p (e1 ∩ e2) / prob p e2

conditional_distribution_def

⊢ ∀p X Y a b.
    conditional_distribution p X Y a b =
    joint_distribution p X Y (a × b) / distribution p Y b

conditional_expectation_def

⊢ ∀p X s.
    conditional_expectation p X s =
    @f. real_random_variable f p ∧
        ∀g. g ∈ s ⇒
            (integral p (λx. f x * 𝟙 g x) = integral p (λx. X x * 𝟙 g x))

conditional_prob_def

⊢ ∀p e1 e2. conditional_prob p e1 e2 = conditional_expectation p (𝟙 e1) e2

distribution_def

⊢ ∀p X. distribution p X = (λs. prob p (PREIMAGE X s ∩ p_space p))

events_def

⊢ events = measurable_sets

expectation_def

⊢ expectation = integral

indep_def

⊢ ∀p a b.
    indep p a b ⇔
    a ∈ events p ∧ b ∈ events p ∧ (prob p (a ∩ b) = prob p a * prob p b)

indep_families_def

⊢ ∀p q r. indep_families p q r ⇔ ∀s t. s ∈ q ∧ t ∈ r ⇒ indep p s t

indep_function_def

⊢ ∀p. indep_function p =
      {f |
       indep_families p (IMAGE (PREIMAGE (FST ∘ f)) 𝕌(:β -> bool))
         (IMAGE (PREIMAGE (SND ∘ f)) (events p))}

indep_rv_def

⊢ ∀p X Y s t.
    indep_rv p X Y s t ⇔
    ∀A B.
      A ∈ subsets s ∧ B ∈ subsets t ⇒ indep p (PREIMAGE X A) (PREIMAGE Y B)

joint_distribution3_def

⊢ ∀p X Y Z.
    joint_distribution3 p X Y Z =
    (λa. prob p (PREIMAGE (λx. (X x,Y x,Z x)) a ∩ p_space p))

joint_distribution_def

⊢ ∀p X Y.
    joint_distribution p X Y =
    (λa. prob p (PREIMAGE (λx. (X x,Y x)) a ∩ p_space p))

p_space_def

⊢ p_space = m_space

possibly_def

⊢ ∀p e. possibly p e ⇔ e ∈ events p ∧ prob p e ≠ 0

prob_def

⊢ prob = measure

prob_preserving_def

⊢ prob_preserving = measure_preserving

prob_space_def

⊢ ∀p. prob_space p ⇔ measure_space p ∧ (measure p (p_space p) = 1)

probably_def

⊢ ∀p e. probably p e ⇔ e ∈ events p ∧ (prob p e = 1)

random_variable_def

⊢ ∀X p s.
    random_variable X p s ⇔
    prob_space p ∧ X ∈ measurable (p_space p,events p) s

real_random_variable_def

⊢ ∀X p.
    real_random_variable X p ⇔
    prob_space p ∧ X ∈ borel_measurable (p_space p,events p)

rv_conditional_expectation_def

⊢ ∀p s X Y.
    rv_conditional_expectation p s X Y =
    conditional_expectation p X
      (IMAGE (λa. PREIMAGE Y a ∩ p_space p) (subsets s))

uniform_distribution_def

⊢ ∀p X s. uniform_distribution p X s = (λa. &CARD a / &CARD (space s))

Theorems

ABS_1_MINUS_PROB

⊢ ∀p s. prob_space p ∧ s ∈ events p ∧ prob p s ≠ 0 ⇒ abs (1 − prob p s) < 1

ABS_PROB

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ (abs (prob p s) = prob p s)

ADDITIVE_PROB

⊢ ∀p. additive p ⇔
      ∀s t.
        s ∈ events p ∧ t ∈ events p ∧ DISJOINT s t ⇒
        (prob p (s ∪ t) = prob p s + prob p t)

BAYES_RULE

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ⇒
    (cond_prob p B A = cond_prob p A B * prob p B / prob p A)

BAYES_RULE_GENERAL_SIGMA

⊢ ∀p A B s k.
    prob_space p ∧ A ∈ events p ∧ FINITE s ∧ (∀x. x ∈ s ⇒ B x ∈ events p) ∧
    k ∈ s ∧ (∀a b. a ∈ s ∧ b ∈ s ∧ a ≠ b ⇒ DISJOINT (B a) (B b)) ∧
    (BIGUNION (IMAGE B s) = p_space p) ⇒
    (cond_prob p (B k) A =
     cond_prob p A (B k) * prob p (B k) /
     ∑ (λi. prob p (B i) * cond_prob p A (B i)) s)

COND_PROB_ADDITIVE

⊢ ∀p A B s.
    prob_space p ∧ FINITE s ∧ B ∈ events p ∧ (∀x. x ∈ s ⇒ A x ∈ events p) ∧
    0 < prob p B ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ DISJOINT (A x) (A y)) ∧
    (BIGUNION (IMAGE A s) = p_space p) ⇒
    (∑ (λi. cond_prob p (A i) B) s = 1)

COND_PROB_BOUNDS

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ⇒
    0 ≤ cond_prob p A B ∧ cond_prob p A B ≤ 1

COND_PROB_COMPL

⊢ ∀A B p.
    prob_space p ∧ A ∈ events p ∧ COMPL A ∈ events p ∧ B ∈ events p ∧
    0 < prob p B ⇒
    (cond_prob p (COMPL A) B = 1 − cond_prob p A B)

COND_PROB_DIFF

⊢ ∀p A1 A2 B.
    prob_space p ∧ A1 ∈ events p ∧ A2 ∈ events p ∧ B ∈ events p ⇒
    (cond_prob p (A1 DIFF A2) B = cond_prob p A1 B − cond_prob p (A1 ∩ A2) B)

COND_PROB_FINITE_ADDITIVE

⊢ ∀p A B n s.
    prob_space p ∧ B ∈ events p ∧ A ∈ (count n → events p) ∧
    (s = BIGUNION (IMAGE A (count n))) ∧ (∀a b. a ≠ b ⇒ DISJOINT (A a) (A b)) ⇒
    (cond_prob p s B = ∑ (λi. cond_prob p (A i) B) (count n))

COND_PROB_INCREASING

⊢ ∀A B C p.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ C ∈ events p ⇒
    cond_prob p (A ∩ B) C ≤ cond_prob p A C

COND_PROB_INTER_SPLIT

⊢ ∀p A B C.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ C ∈ events p ⇒
    (cond_prob p (A ∩ B) C = cond_prob p A (B ∩ C) * cond_prob p B C)

COND_PROB_INTER_ZERO

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ (prob p A = 0) ⇒
    (cond_prob p A B = 0)

COND_PROB_ITSELF

⊢ ∀p B. prob_space p ∧ B ∈ events p ∧ 0 < prob p B ⇒ (cond_prob p B B = 1)

COND_PROB_MUL_EQ

⊢ ∀A B p.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ⇒
    (cond_prob p A B * prob p B = cond_prob p B A * prob p A)

COND_PROB_MUL_RULE

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ⇒
    (prob p (A ∩ B) = prob p B * cond_prob p A B)

COND_PROB_POS_IMP_PROB_NZ

⊢ ∀A B p.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ 0 < cond_prob p A B ⇒
    prob p (A ∩ B) ≠ 0

COND_PROB_SWAP

⊢ ∀p A B C.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ C ∈ events p ⇒
    (cond_prob p A (B ∩ C) * cond_prob p B C =
     cond_prob p B (A ∩ C) * cond_prob p A C)

COND_PROB_ZERO

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ (prob p B = 0) ⇒
    (cond_prob p A B = 0)

COND_PROB_ZERO_INTER

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ (prob p (A ∩ B) = 0) ⇒
    (cond_prob p A B = 0)

COUNTABLY_ADDITIVE_PROB

⊢ ∀p. countably_additive p ⇔
      ∀f. f ∈ (𝕌(:num) → events p) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) ∈ events p ⇒
          prob p ∘ f sums prob p (BIGUNION (IMAGE f 𝕌(:num)))

EVENTS

⊢ ∀a b c. events (a,b,c) = b

EVENTS_ALGEBRA

⊢ ∀p. prob_space p ⇒ algebra (p_space p,events p)

EVENTS_BIGUNION

⊢ ∀p f n.
    prob_space p ∧ f ∈ (count n → events p) ⇒
    BIGUNION (IMAGE f (count n)) ∈ events p

EVENTS_COMPL

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ p_space p DIFF s ∈ events p

EVENTS_COUNTABLE_INTER

⊢ ∀p c.
    prob_space p ∧ c ⊆ events p ∧ COUNTABLE c ∧ c ≠ ∅ ⇒ BIGINTER c ∈ events p

EVENTS_COUNTABLE_UNION

⊢ ∀p c. prob_space p ∧ c ⊆ events p ∧ COUNTABLE c ⇒ BIGUNION c ∈ events p

EVENTS_DIFF

⊢ ∀p s t. prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s DIFF t ∈ events p

EVENTS_EMPTY

⊢ ∀p. prob_space p ⇒ ∅ ∈ events p

EVENTS_INTER

⊢ ∀p s t. prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s ∩ t ∈ events p

EVENTS_SIGMA_ALGEBRA

⊢ ∀p. prob_space p ⇒ sigma_algebra (p_space p,events p)

EVENTS_SPACE

⊢ ∀p. prob_space p ⇒ p_space p ∈ events p

EVENTS_UNION

⊢ ∀p s t. prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s ∪ t ∈ events p

INCREASING_PROB

⊢ ∀p. increasing p ⇔
      ∀s t. s ∈ events p ∧ t ∈ events p ∧ s ⊆ t ⇒ prob p s ≤ prob p t

INDEP_EMPTY

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ indep p ∅ s

INDEP_REFL

⊢ ∀p a.
    prob_space p ∧ a ∈ events p ⇒
    (indep p a a ⇔ (prob p a = 0)) ∨ (prob p a = 1)

INDEP_SPACE

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ indep p (p_space p) s

INDEP_SYM

⊢ ∀p a b. prob_space p ∧ indep p a b ⇒ indep p b a

INTER_PSPACE

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ (p_space p ∩ s = s)

POSITIVE_PROB

⊢ ∀p. positive p ⇔ (prob p ∅ = 0) ∧ ∀s. s ∈ events p ⇒ 0 ≤ prob p s

PROB

⊢ ∀a b c. prob (a,b,c) = c

PROB_ADDITIVE

⊢ ∀p s t u.
    prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ DISJOINT s t ∧ (u = s ∪ t) ⇒
    (prob p u = prob p s + prob p t)

PROB_COMPL

⊢ ∀p s.
    prob_space p ∧ s ∈ events p ⇒ (prob p (p_space p DIFF s) = 1 − prob p s)

PROB_COMPL_LE1

⊢ ∀p s r.
    prob_space p ∧ s ∈ events p ⇒
    (prob p (p_space p DIFF s) ≤ r ⇔ 1 − r ≤ prob p s)

PROB_COUNTABLY_ADDITIVE

⊢ ∀p s f.
    prob_space p ∧ f ∈ (𝕌(:num) → events p) ∧
    (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
    prob p ∘ f sums prob p s

PROB_COUNTABLY_SUBADDITIVE

⊢ ∀p f.
    prob_space p ∧ IMAGE f 𝕌(:num) ⊆ events p ∧ summable (prob p ∘ f) ⇒
    prob p (BIGUNION (IMAGE f 𝕌(:num))) ≤ suminf (prob p ∘ f)

PROB_COUNTABLY_ZERO

⊢ ∀p c.
    prob_space p ∧ COUNTABLE c ∧ c ⊆ events p ∧ (∀x. x ∈ c ⇒ (prob p x = 0)) ⇒
    (prob p (BIGUNION c) = 0)

PROB_DISCRETE_EVENTS

⊢ ∀p. prob_space p ∧ FINITE (p_space p) ∧ (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ⇒
      ∀s. s ⊆ p_space p ⇒ s ∈ events p

PROB_DISCRETE_EVENTS_COUNTABLE

⊢ ∀p. prob_space p ∧ COUNTABLE (p_space p) ∧
      (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ⇒
      ∀s. s ⊆ p_space p ⇒ s ∈ events p

PROB_EMPTY

⊢ ∀p. prob_space p ⇒ (prob p ∅ = 0)

PROB_EQUIPROBABLE_FINITE_UNIONS

⊢ ∀p s.
    prob_space p ∧ s ∈ events p ∧ (∀x. x ∈ s ⇒ {x} ∈ events p) ∧ FINITE s ∧
    (∀x y. x ∈ s ∧ y ∈ s ⇒ (prob p {x} = prob p {y})) ⇒
    (prob p s = &CARD s * prob p {CHOICE s})

PROB_EQ_BIGUNION_IMAGE

⊢ ∀p f g.
    prob_space p ∧ f ∈ (𝕌(:num) → events p) ∧ g ∈ (𝕌(:num) → events p) ∧
    (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
    (∀m n. m ≠ n ⇒ DISJOINT (g m) (g n)) ∧ (∀n. prob p (f n) = prob p (g n)) ⇒
    (prob p (BIGUNION (IMAGE f 𝕌(:num))) = prob p (BIGUNION (IMAGE g 𝕌(:num))))

PROB_EQ_COMPL

⊢ ∀p s t.
    prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧
    (prob p (p_space p DIFF s) = prob p (p_space p DIFF t)) ⇒
    (prob p s = prob p t)

PROB_FINITELY_ADDITIVE

⊢ ∀p s f n.
    prob_space p ∧ f ∈ (count n → events p) ∧
    (∀a b. a < n ∧ b < n ∧ a ≠ b ⇒ DISJOINT (f a) (f b)) ∧
    (s = BIGUNION (IMAGE f (count n))) ⇒
    (sum (0,n) (prob p ∘ f) = prob p s)

PROB_FINITE_ADDITIVE

⊢ ∀p s f t.
    prob_space p ∧ FINITE s ∧ (∀x. x ∈ s ⇒ f x ∈ events p) ∧
    (∀a b. a ∈ s ∧ b ∈ s ∧ a ≠ b ⇒ DISJOINT (f a) (f b)) ∧
    (t = BIGUNION (IMAGE f s)) ⇒
    (prob p t = ∑ (prob p ∘ f) s)

PROB_INCREASING

⊢ ∀p s t.
    prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ s ⊆ t ⇒ prob p s ≤ prob p t

PROB_INCREASING_UNION

⊢ ∀p s f.
    prob_space p ∧ f ∈ (𝕌(:num) → events p) ∧ (∀n. f n ⊆ f (SUC n)) ∧
    (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
    prob p ∘ f ⟶ prob p s

PROB_INDEP

⊢ ∀p s t u. indep p s t ∧ (u = s ∩ t) ⇒ (prob p u = prob p s * prob p t)

PROB_INTER_SPLIT

⊢ ∀p A B C.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ C ∈ events p ⇒
    (prob p (A ∩ B ∩ C) = cond_prob p A (B ∩ C) * cond_prob p B C * prob p C)

PROB_INTER_ZERO

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ (prob p B = 0) ⇒
    (prob p (A ∩ B) = 0)

PROB_LE_1

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s ≤ 1

PROB_ONE_INTER

⊢ ∀p s t.
    prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ (prob p t = 1) ⇒
    (prob p (s ∩ t) = prob p s)

PROB_POSITIVE

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ 0 ≤ prob p s

PROB_PRESERVING

⊢ ∀p1 p2.
    prob_preserving p1 p2 =
    {f |
     f ∈ measurable (p_space p1,events p1) (p_space p2,events p2) ∧
     measure_space p1 ∧ measure_space p2 ∧
     ∀s. s ∈ events p2 ⇒ (prob p1 (PREIMAGE f s ∩ p_space p1) = prob p2 s)}

PROB_PRESERVING_LIFT

⊢ ∀p1 p2 a f.
    prob_space p1 ∧ prob_space p2 ∧
    (events p2 = subsets (sigma (m_space p2) a)) ∧
    f ∈ prob_preserving p1 (m_space p2,a,prob p2) ⇒
    f ∈ prob_preserving p1 p2

PROB_PRESERVING_SUBSET

⊢ ∀p1 p2 a.
    prob_space p1 ∧ prob_space p2 ∧
    (events p2 = subsets (sigma (p_space p2) a)) ⇒
    prob_preserving p1 (p_space p2,a,prob p2) ⊆ prob_preserving p1 p2

PROB_PRESERVING_UP_LIFT

⊢ ∀p1 p2 f.
    prob_space p1 ∧ f ∈ prob_preserving (p_space p1,a,prob p1) p2 ∧
    sigma_algebra (p_space p1,events p1) ∧ a ⊆ events p1 ⇒
    f ∈ prob_preserving p1 p2

PROB_PRESERVING_UP_SIGMA

⊢ ∀p1 p2 a.
    prob_space p1 ∧ (events p1 = subsets (sigma (p_space p1) a)) ⇒
    prob_preserving (p_space p1,a,prob p1) p2 ⊆ prob_preserving p1 p2

PROB_PRESERVING_UP_SUBSET

⊢ ∀p1 p2.
    prob_space p1 ∧ a ⊆ events p1 ∧ sigma_algebra (p_space p1,events p1) ⇒
    prob_preserving (p_space p1,a,prob p1) p2 ⊆ prob_preserving p1 p2

PROB_REAL_SUM_IMAGE

⊢ ∀p s.
    prob_space p ∧ s ∈ events p ∧ (∀x. x ∈ s ⇒ {x} ∈ events p) ∧ FINITE s ⇒
    (prob p s = ∑ (λx. prob p {x}) s)

PROB_REAL_SUM_IMAGE_FN

⊢ ∀p f e s.
    prob_space p ∧ e ∈ events p ∧ (∀x. x ∈ s ⇒ e ∩ f x ∈ events p) ∧
    FINITE s ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ DISJOINT (f x) (f y)) ∧
    (BIGUNION (IMAGE f s) ∩ p_space p = p_space p) ⇒
    (prob p e = ∑ (λx. prob p (e ∩ f x)) s)

PROB_REAL_SUM_IMAGE_SPACE

⊢ ∀p. prob_space p ∧ (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ∧ FINITE (p_space p) ⇒
      (∑ (λx. prob p {x}) (p_space p) = 1)

PROB_SPACE

⊢ ∀p. prob_space p ⇔
      sigma_algebra (p_space p,events p) ∧ positive p ∧ countably_additive p ∧
      (prob p (p_space p) = 1)

PROB_SPACE_ADDITIVE

⊢ ∀p. prob_space p ⇒ additive p

PROB_SPACE_COUNTABLY_ADDITIVE

⊢ ∀p. prob_space p ⇒ countably_additive p

PROB_SPACE_INCREASING

⊢ ∀p. prob_space p ⇒ increasing p

PROB_SPACE_POSITIVE

⊢ ∀p. prob_space p ⇒ positive p

PROB_SUBADDITIVE

⊢ ∀p s t u.
    prob_space p ∧ t ∈ events p ∧ u ∈ events p ∧ (s = t ∪ u) ⇒
    prob p s ≤ prob p t + prob p u

PROB_UNIV

⊢ ∀p. prob_space p ⇒ (prob p (p_space p) = 1)

PROB_ZERO_INTER

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ (prob p A = 0) ⇒
    (prob p (A ∩ B) = 0)

PROB_ZERO_UNION

⊢ ∀p s t.
    prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ (prob p t = 0) ⇒
    (prob p (s ∪ t) = prob p s)

PSPACE

⊢ ∀a b c. p_space (a,b,c) = a

TOTAL_PROB_SIGMA

⊢ ∀p A B s.
    prob_space p ∧ A ∈ events p ∧ FINITE s ∧ (∀x. x ∈ s ⇒ B x ∈ events p) ∧
    (∀a b. a ∈ s ∧ b ∈ s ∧ a ≠ b ⇒ DISJOINT (B a) (B b)) ∧
    (BIGUNION (IMAGE B s) = p_space p) ⇒
    (prob p A = ∑ (λi. prob p (B i) * cond_prob p A (B i)) s)

conditional_distribution_le_1

⊢ ∀p X Y a b.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    conditional_distribution p X Y a b ≤ 1

conditional_distribution_pos

⊢ ∀p X Y a b.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    0 ≤ conditional_distribution p X Y a b

distribution_lebesgue_thm1

⊢ ∀X p s A.
    random_variable X p s ∧ A ∈ subsets s ⇒
    (distribution p X A = integral p (𝟙 (PREIMAGE X A ∩ p_space p)))

distribution_lebesgue_thm2

⊢ ∀X p s A.
    random_variable X p s ∧ A ∈ subsets s ⇒
    (distribution p X A = integral (space s,subsets s,distribution p X) (𝟙 A))

distribution_pos

⊢ ∀p X a. prob_space p ∧ (events p = POW (p_space p)) ⇒ 0 ≤ distribution p X a

distribution_prob_space

⊢ ∀p X s.
    random_variable X p s ⇒ prob_space (space s,subsets s,distribution p X)

distribution_x_eq_1_imp_distribution_y_eq_0

⊢ ∀X p x.
    random_variable X p (IMAGE X (p_space p),POW (IMAGE X (p_space p))) ∧
    (distribution p X {x} = 1) ⇒
    ∀y. y ≠ x ⇒ (distribution p X {y} = 0)

finite_expectation

⊢ ∀p X.
    FINITE (p_space p) ∧ real_random_variable X p ⇒
    (expectation p X = ∑ (λr. r * distribution p X {r}) (IMAGE X (p_space p)))

finite_expectation1

⊢ ∀p X.
    FINITE (p_space p) ∧ real_random_variable X p ⇒
    (expectation p X =
     ∑ (λr. r * prob p (PREIMAGE X {r} ∩ p_space p)) (IMAGE X (p_space p)))

finite_marginal_product_space_POW

⊢ ∀p X Y.
    (POW (p_space p) = events p) ∧
    random_variable X p (IMAGE X (p_space p),POW (IMAGE X (p_space p))) ∧
    random_variable Y p (IMAGE Y (p_space p),POW (IMAGE Y (p_space p))) ∧
    FINITE (p_space p) ⇒
    measure_space
      (IMAGE X (p_space p) × IMAGE Y (p_space p),
       POW (IMAGE X (p_space p) × IMAGE Y (p_space p)),
       (λa. prob p (PREIMAGE (λx. (X x,Y x)) a ∩ p_space p)))

finite_marginal_product_space_POW2

⊢ ∀p s1 s2 X Y.
    (POW (p_space p) = events p) ∧ random_variable X p (s1,POW s1) ∧
    random_variable Y p (s2,POW s2) ∧ FINITE (p_space p) ∧ FINITE s1 ∧
    FINITE s2 ⇒
    measure_space (s1 × s2,POW (s1 × s2),joint_distribution p X Y)

finite_marginal_product_space_POW3

⊢ ∀p s1 s2 s3 X Y Z.
    (POW (p_space p) = events p) ∧ random_variable X p (s1,POW s1) ∧
    random_variable Y p (s2,POW s2) ∧ random_variable Z p (s3,POW s3) ∧
    FINITE (p_space p) ∧ FINITE s1 ∧ FINITE s2 ∧ FINITE s3 ⇒
    measure_space
      (s1 × (s2 × s3),POW (s1 × (s2 × s3)),joint_distribution3 p X Y Z)

joint_conditional

⊢ ∀p X Y a b.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    (joint_distribution p X Y (a × b) =
     conditional_distribution p Y X b a * distribution p X a)

joint_distribution_le

⊢ ∀p X Y a b.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    joint_distribution p X Y (a × b) ≤ distribution p X a

joint_distribution_le2

⊢ ∀p X Y a b.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    joint_distribution p X Y (a × b) ≤ distribution p Y b

joint_distribution_le_1

⊢ ∀p X Y a.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    joint_distribution p X Y a ≤ 1

joint_distribution_pos

⊢ ∀p X Y a.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    0 ≤ joint_distribution p X Y a

joint_distribution_sum_mul1

⊢ ∀p X Y f.
    prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
    (∑ (λ(x,y). joint_distribution p X Y {(x,y)} * f x)
       (IMAGE X (p_space p) × IMAGE Y (p_space p)) =
     ∑ (λx. distribution p X {x} * f x) (IMAGE X (p_space p)))

joint_distribution_sums_1

⊢ ∀p X Y.
    prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
    (∑ (λ(x,y). joint_distribution p X Y {(x,y)})
       (IMAGE X (p_space p) × IMAGE Y (p_space p)) = 1)

joint_distribution_sym

⊢ ∀p X Y a b.
    prob_space p ⇒
    (joint_distribution p X Y (a × b) = joint_distribution p Y X (b × a))

marginal_distribution1

⊢ ∀p X Y a.
    prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
    (distribution p X a =
     ∑ (λx. joint_distribution p X Y (a × {x})) (IMAGE Y (p_space p)))

marginal_distribution2

⊢ ∀p X Y b.
    prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
    (distribution p Y b =
     ∑ (λx. joint_distribution p X Y ({x} × b)) (IMAGE X (p_space p)))

marginal_joint_zero

⊢ ∀p X Y s t.
    prob_space p ∧ (events p = POW (p_space p)) ∧
    ((distribution p X s = 0) ∨ (distribution p Y t = 0)) ⇒
    (joint_distribution p X Y (s × t) = 0)

marginal_joint_zero3

⊢ ∀p X Y Z s t u.
    prob_space p ∧ (events p = POW (p_space p)) ∧
    ((distribution p X s = 0) ∨ (distribution p Y t = 0) ∨
     (distribution p Z u = 0)) ⇒
    (joint_distribution3 p X Y Z (s × (t × u)) = 0)

prob_x_eq_1_imp_prob_y_eq_0

⊢ ∀p x.
    prob_space p ∧ {x} ∈ events p ∧ (prob p {x} = 1) ⇒
    ∀y. {y} ∈ events p ∧ y ≠ x ⇒ (prob p {y} = 0)

uniform_distribution_prob_space

⊢ ∀X p s.
    FINITE (p_space p) ∧ FINITE (space s) ∧ random_variable X p s ⇒
    prob_space (space s,subsets s,uniform_distribution p X s)