Theory "probability"

Signature

Definitions

PDF_def

⊢ ∀p X. PDF p X = distribution p X / lborel

absolute_moment_def

⊢ ∀p X a r. absolute_moment p X a r = expectation p (λx. abs (X x − a) pow r)

central_moment_def

⊢ ∀p X r. central_moment p X r = moment p X (expectation p X) r

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 ⇒
            (expectation p (λx. f x * 𝟙 g x) = expectation p (λx. X x * 𝟙 g x))

conditional_prob_def

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

covariance_def

⊢ ∀p X Y.
    covariance p X Y =
    expectation p (λx. (X x − expectation p X) * (Y x − expectation p Y))

distribution_def

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

distribution_function_def

⊢ ∀p X. distribution_function p X = (λx. prob p ({w | X w ≤ x} ∩ p_space p))

equivalent_def

⊢ ∀p X Y.
    equivalent p X Y ⇔
    suminf (λn. prob p {x | x ∈ p_space p ∧ X n x ≠ Y n x}) < +∞

events_def

⊢ events = measurable_sets

expectation_def

⊢ expectation = ∫

finite_second_moments_def

⊢ ∀p X. finite_second_moments p X ⇔ ∃a. second_moment p X a < +∞

identical_distribution_def

⊢ ∀p X E J.
    identical_distribution p X E J ⇔
    ∀i j s.
      s ∈ subsets E ∧ i ∈ J ∧ i ∈ J ⇒
      (distribution p (X i) s = distribution p (X j) s)

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_events_def

⊢ ∀p E J.
    indep_events p E J ⇔
    ∀N. N ⊆ J ∧ N ≠ ∅ ∧ FINITE N ⇒
        (prob p (BIGINTER (IMAGE E N)) = ∏ (prob p ∘ E) N)

indep_families_def

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

indep_function_def

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

indep_rv_def

⊢ ∀p X Y s t.
    indep_vars p X Y s t ⇔
    ∀a b.
      a ∈ subsets s ∧ b ∈ subsets t ⇒
      indep p (PREIMAGE X a ∩ p_space p) (PREIMAGE Y b ∩ p_space p)

indep_sets_def

⊢ ∀p A J.
    indep_sets p A J ⇔
    ∀N. N ⊆ J ∧ N ≠ ∅ ∧ FINITE N ⇒
        ∀E. E ∈ N ⟶ A ⇒ (prob p (BIGINTER (IMAGE E N)) = ∏ (prob p ∘ E) N)

indep_vars_def

⊢ ∀p X A J.
    indep_vars p X A J ⇔
    ∀E. E ∈ J ⟶ subsets ∘ A ⇒
        indep_events p (λn. PREIMAGE (X n) (E n) ∩ p_space p) J

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

moment_def

⊢ ∀p X a r. moment p X a r = expectation p (λx. (X x − a) pow r)

orthogonal_def

⊢ ∀p X Y.
    orthogonal p X Y ⇔
    finite_second_moments p X ∧ finite_second_moments p Y ∧
    (expectation p (λs. X s * Y s) = 0)

orthogonal_vars_def

⊢ ∀p X J.
    orthogonal_vars p X J ⇔
    ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ orthogonal p (X i) (X j)

p_space_def

⊢ p_space = m_space

pairwise_indep_events

⊢ ∀p E J. pairwise_indep_events p E J ⇔ pairwise (λi j. indep p (E i) (E j)) J

pairwise_indep_sets

⊢ ∀p A J.
    pairwise_indep_sets p A J ⇔ pairwise (λi j. indep_sets p (A i) (A j)) J

pairwise_indep_vars

⊢ ∀p X A J.
    pairwise_indep_vars p X A J ⇔
    pairwise (λi j. indep_vars p (X i) (X j) (A i) (A j)) J

pdf_def

⊢ ∀p X. pdf p X = distribution p X / ext_lborel

possibly_def

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

prob_def

⊢ prob = measure

prob_space_def

⊢ ∀p. prob_space p ⇔ measure_space p ∧ (measure p (m_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 ⇔ X ∈ measurable (p_space p,events p) s

real_random_variable_def

⊢ ∀X p.
    real_random_variable X p ⇔
    random_variable X p Borel ∧ ∀x. X x ≠ −∞ ∧ X x ≠ +∞

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

second_moment_def

⊢ ∀p X a. second_moment p X a = moment p X a 2

standard_deviation_def

⊢ ∀p X. standard_deviation p X = sqrt (variance p X)

tail_algebra_def

⊢ ∀p E.
    tail_algebra p E =
    (p_space p,
     BIGINTER
       (IMAGE (λn. subsets (sigma (p_space p) (IMAGE E (from n)))) 𝕌(:num)))

tail_algebra_of_rv_def

⊢ ∀p X A.
    tail_algebra p X A =
    (p_space p,
     BIGINTER (IMAGE (λn. subsets (sigma (p_space p) A X (from n))) 𝕌(:num)))

uncorrelated_def

⊢ ∀p X Y.
    uncorrelated p X Y ⇔
    finite_second_moments p X ∧ finite_second_moments p Y ∧
    (expectation p (λs. X s * Y s) = expectation p X * expectation p Y)

uncorrelated_vars_def

⊢ ∀p X J.
    uncorrelated_vars p X J ⇔
    ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ uncorrelated p (X i) (X j)

uniform_distribution_def

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

variance_def

⊢ ∀p X. variance p X = central_moment p X 2

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 ∧ s ∪ t ∈ events p ⇒
        (prob p (s ∪ t) = prob p s + prob p t)

BAYES_RULE

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ prob p A ≠ 0 ∧ prob p B ≠ 0 ⇒
    (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 ∧ prob p A ≠ 0 ∧ FINITE s ∧
    (∀x. x ∈ s ⇒ B x ∈ events p ∧ prob p (B x) ≠ 0) ∧ 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)

Borel_0_1_Law

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ∧ pairwise_indep_events p E 𝕌(:num) ⇒
    (prob p (limsup E) = 0) ∨ (prob p (limsup E) = 1)

Borel_Cantelli_Lemma1

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ∧ suminf (prob p ∘ E) < +∞ ⇒
    (prob p (limsup E) = 0)

Borel_Cantelli_Lemma2

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ∧ indep_events p E 𝕌(:num) ∧
    (suminf (prob p ∘ E) = +∞) ⇒
    (prob p (limsup E) = 1)

Borel_Cantelli_Lemma2p

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ∧ pairwise_indep_events p E 𝕌(:num) ∧
    (suminf (prob p ∘ E) = +∞) ⇒
    (prob p (limsup E) = 1)

COND_PROB_ADDITIVE

⊢ ∀p A B s.
    prob_space p ∧ FINITE s ∧ B ∈ events p ∧ (∀x. x ∈ s ⇒ A x ∈ events p) ∧
    prob p B ≠ 0 ∧ (∀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 ∧ prob p B ≠ 0 ⇒
    0 ≤ cond_prob p A B ∧ cond_prob p A B ≤ 1

COND_PROB_COMPL

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ COMPL A ∈ events p ∧ B ∈ events p ∧
    prob p B ≠ 0 ⇒
    (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 ∧ prob p B ≠ 0 ⇒
    (cond_prob p (A1 DIFF A2) B = cond_prob p A1 B − cond_prob p (A1 ∩ A2) B)

COND_PROB_FINITE

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ prob p B ≠ 0 ⇒
    cond_prob p A B ≠ +∞ ∧ cond_prob p A 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))) ∧ prob p B ≠ 0 ∧
    (∀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

⊢ ∀p A B C.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ C ∈ events p ∧ prob p C ≠ 0 ⇒
    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 ∧
    prob p (B ∩ C) ≠ 0 ⇒
    (cond_prob p (A ∩ B) C = cond_prob p A (B ∩ C) * cond_prob p B C)

COND_PROB_ITSELF

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

COND_PROB_MUL_EQ

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ prob p A ≠ 0 ∧ prob p B ≠ 0 ⇒
    (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 B ≠ 0 ⇒
    (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 B ≠ 0 ⇒
    prob p (A ∩ B) ≠ 0

COND_PROB_SWAP

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

COND_PROB_UNION

⊢ ∀p A1 A2 B.
    prob_space p ∧ A1 ∈ events p ∧ A2 ∈ events p ∧ B ∈ events p ∧ prob p B ≠ 0 ⇒
    (cond_prob p (A1 ∪ A2) B =
     cond_prob p A1 B + cond_prob p A2 B − cond_prob p (A1 ∩ A2) B)

COND_PROB_ZERO

⊢ ∀p A B.
    prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ (prob p A = 0) ∧ 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) ∧
    prob p 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 (BIGUNION (IMAGE f 𝕌(:num))) = suminf (prob p ∘ f))

EVENTS

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

EVENTS_ALGEBRA

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

EVENTS_BIGINTER_FN

⊢ ∀p A J.
    prob_space p ∧ IMAGE A J ⊆ events p ∧ COUNTABLE J ∧ J ≠ ∅ ⇒
    BIGINTER (IMAGE A J) ∈ 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_LIMINF

⊢ ∀p E. prob_space p ∧ (∀n. E n ∈ events p) ⇒ liminf E ∈ events p

EVENTS_LIMSUP

⊢ ∀p E. prob_space p ∧ (∀n. E n ∈ events p) ⇒ limsup E ∈ 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

EXPECTATION_PDF_1

⊢ ∀p X.
    prob_space p ∧ random_variable X p borel ∧ distribution p X ≪ lborel ⇒
    (expectation lborel (PDF p X) = 1)

INCREASING_PROB

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

INDEP_COMPL

⊢ ∀p s t. prob_space p ∧ indep p s t ⇒ indep p s (p_space p DIFF t)

INDEP_COMPL2

⊢ ∀p s t.
    prob_space p ∧ indep p s t ⇒ indep p (p_space p DIFF s) (p_space p DIFF t)

INDEP_EMPTY

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

INDEP_FAMILIES_SIGMA

⊢ ∀p A M N.
    prob_space p ∧ IMAGE A (M ∪ N) ⊆ events p ∧ indep_events p A (M ∪ N) ∧
    DISJOINT M N ∧ M ≠ ∅ ∧ N ≠ ∅ ⇒
    indep_sets p (subsets (sigma (p_space p) (IMAGE A M)))
      (subsets (sigma (p_space p) (IMAGE A N)))

INDEP_FAMILIES_SYM

⊢ ∀p q r. indep_sets p q r ⇒ indep_sets p r q

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. indep p a b ⇒ indep p b a

INDEP_SYM_EQ

⊢ ∀p a b. indep p a b ⇔ indep p b a

INDICATOR_FN_REAL_RV

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ real_random_variable (𝟙 s) p

INTER_PSPACE

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

Kolmogorov_0_1_Law

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ∧ indep_events p E 𝕌(:num) ⇒
    ∀e. e ∈ subsets (tail_algebra p E) ⇒ (prob p e = 0) ∨ (prob p e = 1)

PDF_LE_POS

⊢ ∀p X.
    prob_space p ∧ random_variable X p borel ∧ distribution p X ≪ lborel ⇒
    ∀x. 0 ≤ PDF p X x

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 s = suminf (prob p ∘ f))

PROB_COUNTABLY_SUBADDITIVE

⊢ ∀p f.
    prob_space p ∧ IMAGE f 𝕌(:num) ⊆ events p ⇒
    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_DIFF_SUBSET

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

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 ∧ FINITE s ∧ s ∈ events p ∧ (∀x. x ∈ s ⇒ {x} ∈ events p) ∧
    (∀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_EXTREAL_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_EXTREAL_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_EXTREAL_SUM_IMAGE_SPACE

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

PROB_FINITE

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s ≠ −∞ ∧ 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_GSPEC

⊢ ∀P p s. prob p {x | x ∈ s ∧ P x} = prob p ({x | P x} ∩ 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 f.
    prob_space p ∧ f ∈ (𝕌(:num) → events p) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
    (sup (IMAGE (prob p ∘ f) 𝕌(:num)) = prob p (BIGUNION (IMAGE f 𝕌(:num))))

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 (B ∩ C) ≠ 0 ⇒
    (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_LIMINF

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ⇒
    (prob p (liminf E) =
     sup (IMAGE (λm. prob p (BIGINTER {E n | m ≤ n})) 𝕌(:num)))

PROB_LIMSUP

⊢ ∀p E.
    prob_space p ∧ (∀n. E n ∈ events p) ⇒
    (prob p (limsup E) =
     inf (IMAGE (λm. prob p (BIGUNION {E n | m ≤ n})) 𝕌(:num)))

PROB_LT_POSINF

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s < +∞

PROB_ONE_AE

⊢ ∀p E. prob_space p ∧ E ∈ events p ∧ (prob p E = 1) ⇒ AE x::p. x ∈ E

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_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_IN_PSPACE

⊢ ∀p E. prob_space p ∧ E ∈ events p ⇒ ∀x. x ∈ E ⇒ x ∈ p_space p

PROB_SPACE_POSITIVE

⊢ ∀p. prob_space p ⇒ positive p

PROB_SPACE_SIGMA_FINITE

⊢ ∀p. prob_space p ⇒ sigma_finite p

PROB_SPACE_SUBSET_PSPACE

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

PROB_SUBADDITIVE

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

PROB_UNDER_UNIV

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

PROB_UNIV

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

PROB_ZERO_AE

⊢ ∀p E. prob_space p ∧ E ∈ events p ∧ (prob p E = 0) ⇒ AE x::p. x ∉ E

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

SLLN_uncorrelated

⊢ ∀p X S M.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
    (∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
    (∀n x. S n x = ∑ (λi. X i x) (count n)) ∧ (∀n. M n = expectation p (S n)) ⇒
    ((λn x. (S (SUC n) x − M (SUC n)) / &SUC n) ⟶ (λx. 0))
      (almost_everywhere p)

SLLN_uncorrelated'

⊢ ∀p X S.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
    (∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
    (∀n x. S n x = ∑ (λi. X i x) (count n)) ⇒
    ((λn x. (S n x − expectation p (S n)) / &n) ⟶ (λx. 0))
      (almost_everywhere p)

TOTAL_PROB_SIGMA

⊢ ∀p A B s.
    prob_space p ∧ A ∈ events p ∧ FINITE s ∧
    (∀x. x ∈ s ⇒ B x ∈ events p ∧ prob p (B x) ≠ 0) ∧
    (∀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)

WLLN_uncorrelated

⊢ ∀p X S M.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
    (∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
    (∀n x. S n x = ∑ (λi. X i x) (count n)) ∧ (∀n. M n = expectation p (S n)) ⇒
    ((λn x. (S (SUC n) x − M (SUC n)) / &SUC n) ⟶ (λx. 0)) (in_probability p)

WLLN_uncorrelated'

⊢ ∀p X S.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
    (∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
    (∀n x. S n x = ∑ (λi. X i x) (count n)) ⇒
    ((λn x. (S n x − expectation p (S n)) / &n) ⟶ (λx. 0)) (in_probability p)

WLLN_uncorrelated_L2

⊢ ∀p X S M.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
    (∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
    (∀n x. S n x = ∑ (λi. X i x) (count n)) ∧ (∀n. M n = expectation p (S n)) ⇒
    ((λn x. (S (SUC n) x − M (SUC n)) / &SUC n) ⟶ (λx. 0)) (in_lebesgue 2 p)

chebyshev_ineq

⊢ ∀p X t c.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ∧
    0 < t ⇒
    prob p ({x | t ≤ abs (X x − Normal c)} ∩ p_space p) ≤
    t² ⁻¹ * expectation p (λx. (X x − Normal c)²)

chebyshev_ineq_variance

⊢ ∀p X t.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ∧
    0 < t ⇒
    prob p ({x | t ≤ abs (X x − expectation p X)} ∩ p_space p) ≤
    t² ⁻¹ * variance p X

chebyshev_inequality

⊢ ∀p X a t c.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ∧
    0 < t ∧ a ∈ events p ⇒
    prob p ({x | t ≤ abs (X x − Normal c)} ∩ a) ≤
    t² ⁻¹ * expectation p (λx. (X x − Normal c)² * 𝟙 a x)

conditional_distribution_le_1

⊢ ∀p X Y a b.
    prob_space p ∧ (events p = POW (p_space p)) ∧ distribution p Y b ≠ 0 ⇒
    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)) ∧ distribution p Y b ≠ 0 ⇒
    0 ≤ conditional_distribution p X Y a b

converge_AE_alt_inf

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (almost_everywhere p) ⇔
     ∀e. 0 < e ∧ e ≠ +∞ ⇒
         (inf
            (IMAGE
               (λm.
                    prob p
                      {x | x ∈ p_space p ∧ ∃n. m ≤ n ∧ e < abs (X n x − Y x)})
               𝕌(:num)) = 0))

converge_AE_alt_liminf

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (almost_everywhere p) ⇔
     ∀e. 0 < e ∧ e ≠ +∞ ⇒
         (prob p (liminf (λn. {x | x ∈ p_space p ∧ abs (X n x − Y x) ≤ e})) =
          1))

converge_AE_alt_limsup

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (almost_everywhere p) ⇔
     ∀e. 0 < e ∧ e ≠ +∞ ⇒
         (prob p (limsup (λn. {x | x ∈ p_space p ∧ e < abs (X n x − Y x)})) =
          0))

converge_AE_alt_sup

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (almost_everywhere p) ⇔
     ∀e. 0 < e ∧ e ≠ +∞ ⇒
         (sup
            (IMAGE
               (λm.
                    prob p
                      {x | x ∈ p_space p ∧ ∀n. m ≤ n ⇒ abs (X n x − Y x) ≤ e})
               𝕌(:num)) = 1))

converge_AE_def

⊢ ∀p X Y.
    (X ⟶ Y) (almost_everywhere p) ⇔
    AE x::p. ((λn. real (X n x)) ⟶ real (Y x)) sequentially

converge_AE_imp_PR

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    (X ⟶ Y) (almost_everywhere p) ⇒
    (X ⟶ Y) (in_probability p)

converge_AE_imp_PR'

⊢ ∀p X.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ⇒
    (X ⟶ (λx. 0)) (almost_everywhere p) ⇒
    (X ⟶ (λx. 0)) (in_probability p)

converge_AE_shift

⊢ ∀p X Y.
    ((λn. X (SUC n)) ⟶ Y) (almost_everywhere p) ⇒
    ((λn. X n) ⟶ Y) (almost_everywhere p)

converge_AE_to_zero

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (almost_everywhere p) ⇔
     ((λn x. X n x − Y x) ⟶ (λx. 0)) (almost_everywhere p))

converge_AE_to_zero'

⊢ ∀p X Y Z.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ∧ (∀n x. Z n x = X n x − Y x) ⇒
    ((X ⟶ Y) (almost_everywhere p) ⇔ (Z ⟶ (λx. 0)) (almost_everywhere p))

converge_LP_alt_absolute_moment

⊢ ∀p X Y k.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (in_lebesgue (&k) p) ⇔
     0 < k ∧ (∀n. expectation p (λx. abs (X n x) pow k) ≠ +∞) ∧
     expectation p (λx. abs (Y x) pow k) ≠ +∞ ∧
     ((λn. real (absolute_moment p (λx. X n x − Y x) 0 k)) ⟶ 0) sequentially)

converge_LP_alt_pow

⊢ ∀p X Y k.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (in_lebesgue (&k) p) ⇔
     0 < k ∧ (∀n. expectation p (λx. abs (X n x) pow k) ≠ +∞) ∧
     expectation p (λx. abs (Y x) pow k) ≠ +∞ ∧
     ((λn. real (expectation p (λx. abs (X n x − Y x) pow k))) ⟶ 0)
       sequentially)

converge_LP_def

⊢ ∀p X Y r.
    (X ⟶ Y) (in_lebesgue r p) ⇔
    0 < r ∧ r ≠ +∞ ∧ (∀n. expectation p (λx. abs (X n x) powr r) ≠ +∞) ∧
    expectation p (λx. abs (Y x) powr r) ≠ +∞ ∧
    ((λn. real (expectation p (λx. abs (X n x − Y x) powr r))) ⟶ 0)
      sequentially

converge_LP_imp_PR'

⊢ ∀p X k.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ⇒
    (X ⟶ (λx. 0)) (in_lebesgue (&k) p) ⇒
    (X ⟶ (λx. 0)) (in_probability p)

converge_PR_def

⊢ ∀p X Y.
    (X ⟶ Y) (in_probability p) ⇔
    ∀e. 0 < e ∧ e ≠ +∞ ⇒
        ((λn. real (prob p {x | x ∈ p_space p ∧ e < abs (X n x − Y x)})) ⟶ 0)
          sequentially

converge_PR_shift

⊢ ∀p X Y.
    ((λn. X (SUC n)) ⟶ Y) (in_probability p) ⇒
    ((λn. X n) ⟶ Y) (in_probability p)

converge_PR_to_zero

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((X ⟶ Y) (in_probability p) ⇔
     ((λn x. X n x − Y x) ⟶ (λx. 0)) (in_probability p))

converge_PR_to_zero'

⊢ ∀p X Y Z.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ∧ (∀n x. Z n x = X n x − Y x) ⇒
    ((X ⟶ Y) (in_probability p) ⇔ (Z ⟶ (λx. 0)) (in_probability p))

covariance_self

⊢ ∀p X. covariance p X X = variance p X

distribution_distr

⊢ distribution = distr

distribution_function

⊢ ∀p X t. distribution_function p X t = distribution p X {x | x ≤ t}

distribution_le_1

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

distribution_lebesgue_thm1

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

distribution_lebesgue_thm2

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

distribution_not_infty

⊢ ∀p X a.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    distribution p X a ≠ −∞ ∧ distribution p X a ≠ +∞

distribution_partition

⊢ ∀p X.
    prob_space p ∧ (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ∧ FINITE (p_space p) ∧
    random_variable X p Borel ⇒
    (∑ (λx. distribution p X {x}) (IMAGE X (p_space p)) = 1)

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.
    prob_space p ∧ 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.
    prob_space p ∧
    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)

equivalent_lemma

⊢ ∀p X Y.
    prob_space p ∧ equivalent p X Y ∧ (∀n. real_random_variable (X n) p) ∧
    (∀n. real_random_variable (Y n) p) ⇒
    ∃N f.
      N ∈ null_set p ∧
      ∀x. x ∈ p_space p DIFF N ⇒ ∀n. f x ≤ n ⇒ (X n x − Y n x = 0)

equivalent_thm1

⊢ ∀p X Y Z.
    prob_space p ∧ equivalent p X Y ∧ (∀n. real_random_variable (X n) p) ∧
    (∀n. real_random_variable (Y n) p) ∧
    (∀n x. Z n x = ∑ (λn. X n x − Y n x) (count n)) ⇒
    ∃W. real_random_variable W p ∧ (Z ⟶ W) (almost_everywhere p)

equivalent_thm2

⊢ ∀p X Y a Z.
    prob_space p ∧ equivalent p X Y ∧ (∀n. real_random_variable (X n) p) ∧
    (∀n. real_random_variable (Y n) p) ∧ mono_increasing a ∧
    (sup (IMAGE a 𝕌(:num)) = +∞) ∧
    (∀n x. Z n x = ∑ (λn. X n x − Y n x) (count n) / a n) ⇒
    (Z ⟶ (λx. 0)) (almost_everywhere p)

expectation_bounds

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    suminf (λn. prob p {x | x ∈ p_space p ∧ &SUC n ≤ abs (X x)}) ≤
    expectation p (abs ∘ X) ∧
    expectation p (abs ∘ X) ≤
    1 + suminf (λn. prob p {x | x ∈ p_space p ∧ &SUC n ≤ abs (X x)})

expectation_const

⊢ ∀p c. prob_space p ⇒ (expectation p (λx. Normal c) = Normal c)

expectation_converge

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (expectation p (abs ∘ X) < +∞ ⇔
     suminf (λn. prob p {x | x ∈ p_space p ∧ &SUC n ≤ abs (X x)}) < +∞)

expectation_converge'

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    ((expectation p (abs ∘ X) = +∞) ⇔
     (suminf (λn. prob p {x | x ∈ p_space p ∧ &SUC n ≤ abs (X x)}) = +∞))

expectation_distribution

⊢ ∀p X f.
    prob_space p ∧ random_variable X p Borel ∧ f ∈ Borel_measurable Borel ⇒
    (expectation p (f ∘ X) = ∫ (space Borel,subsets Borel,distribution p X) f) ∧
    (integrable p (f ∘ X) ⇔
     integrable (space Borel,subsets Borel,distribution p X) f)

expectation_finite

⊢ ∀p X.
    prob_space p ∧ integrable p X ⇒
    expectation p X ≠ +∞ ∧ expectation p X ≠ −∞

expectation_indicator

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

expectation_normal

⊢ ∀p X. prob_space p ∧ integrable p X ⇒ ∃r. expectation p X = Normal r

expectation_pdf_1

⊢ ∀p X.
    prob_space p ∧ random_variable X p Borel ∧ distribution p X ≪ ext_lborel ⇒
    (expectation ext_lborel (pdf p X) = 1)

expectation_posinf

⊢ ∀p. prob_space p ⇒ (expectation p (λx. +∞) = +∞)

expectation_real_affine

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ integrable p X ∧ c ≠ +∞ ∧ c ≠ −∞ ⇒
    (expectation p (λx. X x + c) = expectation p X + c)

finite_expectation

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

finite_expectation1

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

finite_expectation2

⊢ ∀p X.
    prob_space p ∧ FINITE (IMAGE X (p_space p)) ∧ real_random_variable X p ∧
    integrable p X ⇒
    (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.
    prob_space p ∧ FINITE (p_space p) ∧ (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))) ⇒
    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.
    prob_space p ∧ FINITE (p_space p) ∧ (POW (p_space p) = events p) ∧
    random_variable X p (s1,POW s1) ∧ random_variable Y p (s2,POW s2) ∧
    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.
    prob_space p ∧ FINITE (p_space p) ∧ (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 s1 ∧ FINITE s2 ∧ FINITE s3 ⇒
    measure_space
      (s1 × (s2 × s3),POW (s1 × (s2 × s3)),joint_distribution3 p X Y Z)

finite_second_moments_all

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (finite_second_moments p X ⇔ ∀r. second_moment p X (Normal r) < +∞)

finite_second_moments_alt

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (finite_second_moments p X ⇔ second_moment p X 0 < +∞)

finite_second_moments_eq_finite_variance

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (finite_second_moments p X ⇔ variance p X < +∞)

finite_second_moments_eq_integrable_square

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (finite_second_moments p X ⇔ integrable p (λx. (X x)²))

finite_second_moments_eq_integrable_squares

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (finite_second_moments p X ⇔ ∀c. integrable p (λx. (X x − Normal c)²))

finite_second_moments_imp_finite_expectation

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ⇒
    expectation p X ≠ +∞ ∧ expectation p X ≠ −∞

finite_second_moments_imp_integrable

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ⇒
    integrable p X

finite_second_moments_indicator_fn

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ finite_second_moments p (𝟙 s)

finite_second_moments_literally

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ⇒
    (finite_second_moments p X ⇔ expectation p (λx. (X x)²) < +∞)

finite_support_expectation

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

identical_distribution_expectation

⊢ ∀p X.
    prob_space p ∧ (∀n. random_variable (X n) p Borel) ∧
    identical_distribution p X Borel 𝕌(:num) ⇒
    ∀n. expectation p (X n) = expectation p (X 0)

identical_distribution_expectation_general

⊢ ∀p X J.
    prob_space p ∧ J ≠ ∅ ∧ (∀n. n ∈ J ⇒ random_variable (X n) p Borel) ∧
    identical_distribution p X Borel 𝕌(:'index) ⇒
    ∃e. ∀n. n ∈ J ⇒ (expectation p (X n) = e)

identical_distribution_integrable

⊢ ∀p X.
    prob_space p ∧ (∀n. random_variable (X n) p Borel) ∧
    identical_distribution p X Borel 𝕌(:num) ∧ integrable p (X 0) ⇒
    ∀n. integrable p (X n)

identical_distribution_integrable_general

⊢ ∀p X J.
    prob_space p ∧ (∀n. n ∈ J ⇒ random_variable (X n) p Borel) ∧
    identical_distribution p X Borel 𝕌(:'index) ∧
    (∃i. i ∈ J ∧ integrable p (X i)) ⇒
    ∀n. n ∈ J ⇒ integrable p (X n)

indep_vars_comm

⊢ ∀p X Y s t. indep_vars p X Y s t ⇒ indep_vars p Y X t s

integrable_absolute_moments

⊢ ∀p X n.
    prob_space p ∧ real_random_variable X p ∧
    integrable p (λx. abs (X x) pow n) ⇒
    ∀m. m ≤ n ⇒ integrable p (λx. abs (X x) pow m)

integrable_from_square

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ∧ integrable p (λx. (X x)²) ⇒
    integrable p X

integrable_imp_finite_expectation

⊢ ∀p X.
    prob_space p ∧ integrable p X ⇒
    expectation p X ≠ +∞ ∧ expectation p X ≠ −∞

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_not_infty

⊢ ∀p X Y a.
    prob_space p ∧ (events p = POW (p_space p)) ⇒
    joint_distribution p X Y a ≠ −∞ ∧ joint_distribution p X Y a ≠ +∞

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. f x ≠ +∞ ∧ f x ≠ −∞) ⇒
    (∑ (λ(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)

pairwise_indep_events_def

⊢ ∀p E J.
    pairwise_indep_events p E J ⇔
    ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ indep p (E i) (E j)

pairwise_indep_sets_def

⊢ ∀p A J.
    pairwise_indep_sets p A J ⇔
    ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ indep_sets p (A i) (A j)

pairwise_indep_vars_def

⊢ ∀p X A J.
    pairwise_indep_vars p X A J ⇔
    ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ indep_vars p (X i) (X j) (A i) (A j)

pdf_le_pos

⊢ ∀p X x.
    prob_space p ∧ random_variable X p Borel ∧ distribution p X ≪ ext_lborel ⇒
    0 ≤ pdf p X x

prob_markov_ineq

⊢ ∀p X c.
    prob_space p ∧ integrable p X ∧ 0 < c ⇒
    prob p ({x | c ≤ abs (X x)} ∩ p_space p) ≤ c⁻¹ * expectation p (abs ∘ X)

prob_markov_inequality

⊢ ∀p X a c.
    prob_space p ∧ integrable p X ∧ 0 < c ∧ a ∈ events p ⇒
    prob p ({x | c ≤ abs (X x)} ∩ a) ≤
    c⁻¹ * expectation p (λx. abs (X x) * 𝟙 a x)

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)

random_variable_compose

⊢ ∀p X f.
    prob_space p ∧ random_variable X p Borel ∧ f ∈ Borel_measurable Borel ⇒
    random_variable (f ∘ X) p Borel

random_variable_functional

⊢ ∀p X Y f.
    prob_space p ∧ random_variable X p Borel ∧ random_variable Y p Borel ∧
    f ∈ Borel_measurable (Borel × Borel) ⇒
    random_variable (λx. f (X x,Y x)) p Borel

real_random_variable

⊢ ∀X p.
    real_random_variable X p ⇔
    X ∈ Borel_measurable (p_space p,events p) ∧ ∀x. X x ≠ −∞ ∧ X x ≠ +∞

real_random_variable_sub

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ⇒
    real_random_variable (λx. X x − Y x) p

real_random_variable_zero

⊢ ∀p. prob_space p ⇒ real_random_variable (λx. 0) p

second_moment_alt

⊢ ∀p X. second_moment p X 0 = expectation p (λx. (X x)²)

second_moment_pos

⊢ ∀p X a. prob_space p ⇒ 0 ≤ second_moment p X a

total_imp_pairwise_indep_events

⊢ ∀p E J.
    (∀n. n ∈ J ⇒ E n ∈ events p) ∧ indep_events p E J ⇒
    pairwise_indep_events p E J

total_imp_pairwise_indep_sets

⊢ ∀p A J.
    (∀n. n ∈ J ⇒ A n ⊆ events p) ∧ indep_sets p A J ⇒
    pairwise_indep_sets p A J

total_imp_pairwise_indep_vars

⊢ ∀p X A J.
    (∀i. i ∈ J ⇒ random_variable (X i) p (A i)) ∧ indep_vars p X A J ⇒
    pairwise_indep_vars p X A J

uncorrelated_covariance

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ∧
    uncorrelated p X Y ⇒
    (covariance p X Y = 0)

uncorrelated_orthogonal

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ∧
    (expectation p X = 0) ∧ (expectation p Y = 0) ⇒
    (uncorrelated p X Y ⇔ orthogonal p X Y)

uncorrelated_thm

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ∧
    uncorrelated p X Y ⇒
    (expectation p (λs. (X s − expectation p X) * (Y s − expectation p Y)) = 0)

uniform_distribution_prob_space

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

variance_alt

⊢ ∀p X. variance p X = expectation p (λx. (X x − expectation p X)²)

variance_eq

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ∧ integrable p (λx. (X x)²) ⇒
    (variance p X = expectation p (λx. (X x)²) − (expectation p X)²)

variance_eq_indicator_fn

⊢ ∀p s.
    prob_space p ∧ s ∈ events p ⇒
    (variance p (𝟙 s) = expectation p (𝟙 s) − (expectation p (𝟙 s))²)

variance_le

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ∧ integrable p (λx. (X x)²) ⇒
    variance p X ≤ expectation p (λx. (X x)²)

variance_le_indicator_fn

⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ variance p (𝟙 s) ≤ expectation p (𝟙 s)

variance_pos

⊢ ∀p X. prob_space p ⇒ 0 ≤ variance p X

variance_real_affine

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ integrable p X ∧ c ≠ +∞ ∧ c ≠ −∞ ⇒
    (variance p (λx. X x + c) = variance p X)

variance_real_affine'

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ integrable p X ∧ c ≠ +∞ ∧ c ≠ −∞ ⇒
    (variance p (λx. X x − c) = variance p X)

variance_sum

⊢ ∀p X J.
    prob_space p ∧ FINITE J ∧ (∀i. i ∈ J ⇒ real_random_variable (X i) p) ∧
    uncorrelated_vars p X J ⇒
    (variance p (λx. ∑ (λn. X n x) J) = ∑ (λn. variance p (X n)) J)

variance_sum_indicator_fn

⊢ ∀p E J.
    prob_space p ∧ (∀n. n ∈ J ⇒ E n ∈ events p) ∧
    pairwise_indep_events p E J ∧ FINITE J ⇒
    (variance p (λx. ∑ (λn. (𝟙 ∘ E) n x) J) = ∑ (λn. variance p ((𝟙 ∘ E) n)) J)