Theory probability

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

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

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

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

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

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

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

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

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

⊢ events = measurable_sets

⊢ expectation = ∫

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

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

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

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

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

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

⊢ ∀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

⊢ ∀p X A J.
    indep_vars p X A J ⇔
    ∀E N.
      N ⊆ J ∧ N ≠ ∅ ∧ FINITE N ∧ E ∈ N ⟶ subsets ∘ A ⇒
      prob p (BIGINTER (IMAGE (λn. PREIMAGE (X n) (E n) ∩ p_space p) N)) =
      ∏ (prob p ∘ (λn. PREIMAGE (X n) (E n) ∩ p_space p)) N

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

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

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

⊢ ∀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

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

⊢ p_space = m_space

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

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

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

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

⊢ prob = measure

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

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

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

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

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

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

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

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

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

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

⊢ ∀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

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

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

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

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

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

⊢ ∀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

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

⊢ ∀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

⊢ ∀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

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

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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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 ≠ −∞

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

⊢ ∀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

⊢ ∀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

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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

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

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

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

⊢ ∀p A J.
    prob_space p ∧ IMAGE A J ⊆ events p ∧ countable J ∧ J ≠ ∅ ⇒
    BIGINTER (IMAGE A J) ∈ events p

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

⊢ ∀p f.
    prob_space p ∧ f ∈ (𝕌(:num) → events p) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) ∈ events p

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

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

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

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

⊢ ∀p. prob_space p ⇒ ∅ ∈ events p

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀p A E.
    prob_space p ∧ E ∈ events p ∧ disjoint_family A ∧ (∀i. indep p E (A i)) ⇒
    indep p E (BIGUNION (IMAGE A 𝕌(:num)))

⊢ ∀p A E.
    prob_space p ∧ E ∈ events p ∧ disjoint_family A ∧ (∀i. indep p (A i) E) ⇒
    indep p (BIGUNION (IMAGE A 𝕌(:num))) E

⊢ ∀p A B C.
    prob_space p ∧ indep p A B ∧ indep p A C ∧ DISJOINT B C ⇒
    indep p A (B ∪ C)

⊢ ∀p A B C.
    prob_space p ∧ indep p A C ∧ indep p B C ∧ DISJOINT A B ⇒
    indep p (A ∪ B) C

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀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

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

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

⊢ ∀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

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

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

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

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

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

⊢ ∀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

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

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

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

⊢ ∀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}

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

⊢ ∀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

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

⊢ ∀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

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

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

⊢ ∀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

⊢ ∀P p s. prob p {x | x ∈ s ∧ P x} = prob p ({x | P x} ∩ s)

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

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

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

⊢ ∀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

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

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

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

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

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

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

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

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

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

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

⊢ ∀p. prob_space p ⇒ additive p

⊢ ∀p. prob_space p ⇒ countably_additive p

⊢ ∀p. prob_space p ⇒ increasing p

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

⊢ ∀p. prob_space p ⇒ p_space p ≠ ∅

⊢ ∀p. prob_space p ⇒ positive p

⊢ ∀p. (p_space p,events p,prob p) = p

⊢ ∀p. prob_space p ⇒ sigma_finite p

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

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

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

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

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

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

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

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

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

⊢ ∀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

⊢ ∀p X.
    prob_space p ∧ random_variable X p Borel ∧
    (∃r. ∀x. x ∈ p_space p ⇒ abs (X x) ≤ Normal r) ⇒
    finite_second_moments p X

⊢ ∀p X.
    prob_space p ∧ random_variable X p Borel ∧ integrable p X ∧
    (∃r. ∀x. x ∈ p_space p ⇒ abs (X x − expectation p X) ≤ Normal r) ⇒
    finite_second_moments p X

⊢ ∀p X.
    prob_space p ∧ random_variable X p Borel ∧
    (∃r. ∀x. x ∈ p_space p ⇒ abs (X x) ≤ Normal r) ⇒
    integrable p X

⊢ ∀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)²)

⊢ ∀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

⊢ ∀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

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

⊢ ∀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

⊢ ∀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

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

⊢ ∀p X Y A B.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable A p ∧ (X ⟶ A) (almost_everywhere p) ∧
    (∀n. real_random_variable (Y n) p) ∧ real_random_variable B p ∧
    (Y ⟶ B) (almost_everywhere p) ⇒
    ((λn x. X n x + Y n x) ⟶ (λx. A x + B x)) (almost_everywhere p)

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

⊢ ∀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) ⟶ (λx. -Y x)) (almost_everywhere p)

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

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

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

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

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

⊢ ∀D p X Y.
    (X ⟶ Y) (almost_everywhere p) ⇔
    ((λn. X (n + D)) ⟶ Y) (almost_everywhere p)

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

⊢ ∀p X Y Z m.
    (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = Y n x) ⇒
    ((X ⟶ Z) (almost_everywhere p) ⇔ (Y ⟶ Z) (almost_everywhere p))

⊢ ∀p X Y A B m.
    (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = Y n x) ∧
    (∀x. x ∈ p_space p ⇒ A x = B x) ⇒
    ((X ⟶ A) (almost_everywhere p) ⇔ (Y ⟶ B) (almost_everywhere p))

⊢ ∀p c. prob_space p ⇒ ((λx n. c) ⟶ (λx. c)) (almost_everywhere p)

⊢ ∀p X m c.
    prob_space p ∧ (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = c) ⇒
    (X ⟶ (λx. c)) (almost_everywhere p)

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

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

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

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

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

⊢ ∀p X M m.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (M ⟶ m) sequentially ∧
    ((λn x. X n x − Normal (M n)) ⟶ (λx. 0)) (almost_everywhere p) ⇒
    (X ⟶ (λx. Normal m)) (almost_everywhere p)

⊢ ∀p X M m.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀n. M n ≠ +∞ ∧ M n ≠ −∞) ∧ m ≠ +∞ ∧ m ≠ −∞ ∧
    (real ∘ M ⟶ real m) sequentially ∧
    ((λn x. X n x − M n) ⟶ (λx. 0)) (almost_everywhere p) ⇒
    (X ⟶ (λx. m)) (almost_everywhere p)

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

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

⊢ ∀X Y r p.
    (X ⟶ Y) (in_lebesgue r p) ⇔
    (∀n. X n ∈ lp_space r p) ∧ Y ∈ lp_space r p ∧
    ((λn. expectation p (λx. abs (X n x − Y x) powr r)) ⟶ 0) sequentially

⊢ ∀p X Y k.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ∧ 0 < k ⇒
    ((X ⟶ Y) (in_lebesgue (&k) p) ⇔
     (∀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)

⊢ ∀p X Y k.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ∧ 0 < k ⇒
    ((X ⟶ Y) (in_lebesgue (&k) p) ⇔
     (∀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)

⊢ ∀p X Y Z r.
    prob_space p ∧ (∀n x. x ∈ p_space p ⇒ X n x = Y n x) ∧ 0 < r ∧ r ≠ +∞ ⇒
    ((X ⟶ Z) (in_lebesgue r p) ⇔ (Y ⟶ Z) (in_lebesgue r p))

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

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

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

⊢ ∀p X Y A B.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable A p ∧ (X ⟶ A) (in_probability p) ∧
    (∀n. real_random_variable (Y n) p) ∧ real_random_variable B p ∧
    (Y ⟶ B) (in_probability p) ⇒
    ((λn x. X n x + Y n x) ⟶ (λx. A x + B x)) (in_probability p)

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

⊢ ∀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) ⟶ (λx. -Y x)) (in_probability p)

⊢ ∀p X.
    (X ⟶ (λx. 0)) (in_probability p) ⇒
    ((λn x. -X n x) ⟶ (λx. 0)) (in_probability p)

⊢ ∀D p X Y.
    (X ⟶ Y) (in_probability p) ⇔ ((λn. X (n + D)) ⟶ Y) (in_probability p)

⊢ ∀p X Y Z m.
    (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = Y n x) ⇒
    ((X ⟶ Z) (in_probability p) ⇔ (Y ⟶ Z) (in_probability p))

⊢ ∀p X Y A B m.
    (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = Y n x) ∧
    (∀x. x ∈ p_space p ⇒ A x = B x) ⇒
    ((X ⟶ A) (in_probability p) ⇔ (Y ⟶ B) (in_probability p))

⊢ ∀p X Y.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    real_random_variable Y p ⇒
    ((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)

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

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

⊢ ∀p X M m.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (M ⟶ m) sequentially ∧
    ((λn x. X n x − Normal (M n)) ⟶ (λx. 0)) (in_probability p) ⇒
    (X ⟶ (λx. Normal m)) (in_probability p)

⊢ ∀p X M m.
    prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
    (∀n. M n ≠ +∞ ∧ M n ≠ −∞) ∧ m ≠ +∞ ∧ m ≠ −∞ ∧
    (real ∘ M ⟶ real m) sequentially ∧
    ((λn x. X n x − M n) ⟶ (λx. 0)) (in_probability p) ⇒
    (X ⟶ (λx. m)) (in_probability p)

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

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

⊢ ∀p X Y Z m.
    prob_space p ∧ (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = Y n x) ⇒
    ((X ⟶ Z) (in_distribution p) ⇔ (Y ⟶ Z) (in_distribution p))

⊢ ∀p X Y A B m.
    prob_space p ∧ (∀n x. m ≤ n ∧ x ∈ p_space p ⇒ X n x = Y n x) ∧
    (∀x. x ∈ p_space p ⇒ A x = B x) ⇒
    ((X ⟶ A) (in_distribution p) ⇔ (Y ⟶ B) (in_distribution p))

⊢ ∀X Y p.
    (X ⟶ Y) (in_distribution p) ⇔
    ∀f. f ∈ C_b ext_euclidean ⇒
        ((λn. expectation p (Normal ∘ f ∘ X n)) ⟶
         expectation p (Normal ∘ f ∘ Y)) sequentially

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

⊢ ∀s. distribution p X s = prob p {x | x ∈ p_space p ∧ X x ∈ s}

⊢ distribution = distr

⊢ ∀p X B s.
    prob_space p ∧ random_variable X p B ∧ sigma_algebra B ∧ s ∈ subsets B ⇒
    distribution p X s ≠ −∞ ∧ distribution p X s ≠ +∞

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

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

⊢ ∀p X B s.
    prob_space p ∧ random_variable X p B ∧ sigma_algebra B ∧ s ∈ subsets B ⇒
    distribution p X s ≤ 1

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

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

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

⊢ ∀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

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

⊢ ∀p X B s.
    prob_space p ∧ random_variable X p B ∧ sigma_algebra B ∧ s ∈ subsets B ⇒
    0 ≤ distribution p X s

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

⊢ ∀p X. prob_space p ⇒ distribution p X (IMAGE X (p_space p)) = 1

⊢ ∀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

⊢ ∀p1 p2.
    prob_space p1 ∧ prob_space p2 ⇒
    ∃p. p = p1 × p2 ∧ prob_space p ∧
        ∀e1 e2.
          e1 ∈ events p1 ∧ e2 ∈ events p2 ⇒
          e1 × e2 ∈ events p ∧ prob p (e1 × e2) = prob p1 e1 * prob p2 e2

⊢ ∀p f g.
    prob_space p ∧ integrable p f ∧ integrable p g ⇒
    expectation p (λx. f x + g x) = expectation p f + expectation p g

⊢ ∀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)})

⊢ ∀p X c.
    prob_space p ∧ integrable p X ∧ c ≠ 0 ⇒
    expectation p (λx. X x / Normal c) = expectation p X / Normal c

⊢ ∀p X c.
    prob_space p ∧ integrable p X ⇒
    expectation p (λx. Normal c * X x) = Normal c * expectation p X

⊢ ∀p f g.
    prob_space p ∧ (∀x. x ∈ p_space p ⇒ f x = g x) ⇒
    expectation p f = expectation p g

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

⊢ ∀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)}) < +∞)

⊢ ∀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)}) = +∞)

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

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

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

⊢ ∀p f g.
    prob_space p ∧ integrable p f ∧ integrable p g ∧
    (∀x. x ∈ p_space p ⇒ f x ≤ g x) ⇒
    expectation p f ≤ expectation p g

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

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

⊢ ∀p X. prob_space p ∧ (∀x. x ∈ p_space p ⇒ 0 ≤ X x) ⇒ 0 ≤ expectation p X

⊢ ∀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

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

⊢ ∀p X J.
    FINITE J ∧ prob_space p ∧ (∀i. i ∈ J ⇒ integrable p (X i)) ∧
    (∀i. i ∈ J ⇒ real_random_variable (X i) p) ⇒
    expectation p (λx. ∑ (λi. X i x) J) = ∑ (λi. expectation p (X i)) J

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

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

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

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

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

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

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

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

⊢ ∀p X.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ⇒
    finite_second_moments p (λx. -X x)

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

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

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ∧
    c ≠ 0 ⇒
    finite_second_moments p (λx. X x / Normal c)

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ⇒
    finite_second_moments p (λx. Normal c * X x)

⊢ ∀p X Y.
    prob_space p ∧ (∀x. x ∈ p_space p ⇒ X x = Y x) ⇒
    (finite_second_moments p X ⇔ finite_second_moments p Y)

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

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

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

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

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

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ∧
    finite_second_moments p X ∧ finite_second_moments p Y ⇒
    integrable p (λx. X x * Y x)

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

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

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

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

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

⊢ ∀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

⊢ ∀p X J.
    prob_space p ∧ (∀n. n ∈ J ⇒ random_variable (X n) p Borel) ⇒
    (identical_distribution p X Borel J ⇔
     ∀f. f ∈ Borel_measurable Borel ⇒
         ∃c. ∀n. n ∈ J ⇒ expectation p (f ∘ X n) = c)

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

⊢ ∀p X E J i j s.
    identical_distribution p X E J ∧ s ∈ subsets E ∧ i ∈ J ∧ j ∈ J ⇒
    prob p {x | x ∈ p_space p ∧ X i x ∈ s} =
    prob p {x | x ∈ p_space p ∧ X j x ∈ s}

⊢ ∀p X f.
    prob_space p ∧ (∀n. random_variable (X n) p Borel) ∧
    identical_distribution p X Borel 𝕌(:num) ∧ f ∈ Borel_measurable Borel ⇒
    identical_distribution p (λn. f ∘ X n) Borel 𝕌(:num)

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

⊢ ∀p X J.
    prob_space p ∧ (∀n. n ∈ J ⇒ random_variable (X n) p Borel) ∧
    identical_distribution p X Borel J ⇒
    ∃e. ∀n. n ∈ J ⇒ expectation p (X n) = e

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

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

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

⊢ ∀p f g A B C D.
    prob_space p ∧ random_variable A p Borel ∧ random_variable B p Borel ∧
    random_variable C p Borel ∧ random_variable D p Borel ∧
    f ∈ Borel_measurable (Borel × Borel) ∧
    g ∈ Borel_measurable (Borel × Borel) ∧
    indep_vars p (λi. [A; B; C; D]❲i❳) (λn. Borel) (count 4) ⇒
    indep_vars p (λx. f (A x,B x)) (λx. g (C x,D x)) Borel Borel

⊢ ∀p X Y A B.
    random_variable X p A ∧ random_variable Y p B ⇒
    (indep_vars p X Y A B ⇔ indep_vars p (binary X Y) (binary A B) {0; 1})

⊢ ∀p X Y A B f g.
    indep_vars p X Y A B ∧ random_variable X p A ∧ random_variable Y p B ∧
    f ∈ measurable A A ∧ g ∈ measurable B B ⇒
    indep_vars p (f ∘ X) (g ∘ Y) A B

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

⊢ ∀p X A.
    prob_space p ∧ (∀n. sigma_algebra (A n)) ∧
    (∀n. random_variable (X n) p (A n)) ⇒
    (indep_vars p X A 𝕌(:num) ⇔
     ∀E n.
       E ∈ count1 n ⟶ subsets ∘ A ⇒
       prob p
         (BIGINTER
            (IMAGE (λn. PREIMAGE (X n) (E n) ∩ p_space p) (count1 n))) =
       ∏ (prob p ∘ (λn. PREIMAGE (X n) (E n) ∩ p_space p)) (count1 n))

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

⊢ ∀p X B J f.
    indep_vars p X B J ∧ (∀n. n ∈ J ⇒ random_variable (X n) p (B n)) ∧
    (∀n. n ∈ J ⇒ f n ∈ measurable (B n) (B n)) ⇒
    indep_vars p (λn. f n ∘ X n) B J

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ∧
    indep_vars p X Y Borel Borel ∧ integrable p X ∧ integrable p Y ⇒
    expectation p (λx. X x * Y x) = expectation p X * expectation p Y

⊢ ∀p X Y.
    prob_space p ∧ real_random_variable X p ∧ real_random_variable Y p ∧
    finite_second_moments p X ∧ finite_second_moments p Y ∧
    indep_vars p X Y Borel Borel ⇒
    uncorrelated p X Y

⊢ ∀p X A s t. indep_vars p X A t ∧ s ⊆ t ⇒ indep_vars p X A s

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

⊢ ∀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. X x pow m)

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

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

⊢ ∀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

⊢ ∀p X Y Z.
    joint_distribution3 p X Y Z = distribution p (λx. (X x,Y x,Z x))

⊢ ∀p X Y. joint_distribution p X Y = distribution p (λx. (X x,Y x))

⊢ ∀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

⊢ ∀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

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

⊢ ∀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 ≠ +∞

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

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

⊢ ∀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

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

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

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

⊢ ∀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

⊢ ∀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

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

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

⊢ ∀p X B J f.
    pairwise_indep_vars p X B J ∧
    (∀n. n ∈ J ⇒ random_variable (X n) p (B n)) ∧
    (∀n. n ∈ J ⇒ f n ∈ measurable (B n) (B n)) ⇒
    pairwise_indep_vars p (λn. f n ∘ X n) B J

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

⊢ ∀p X A J.
    prob_space p ∧ (∀i. i ∈ J ⇒ real_random_variable (X i) p) ∧
    (∀i. i ∈ J ⇒ finite_second_moments p (X i)) ∧
    pairwise_indep_vars p X (λn. Borel) J ⇒
    uncorrelated_vars p X J

⊢ ∀p X A s t.
    pairwise_indep_vars p X A t ∧ s ⊆ t ⇒ pairwise_indep_vars p X A s

⊢ ∀p X.
    prob_space p ∧ random_variable X p Borel ∧
    distribution p X ≪ ext_lborel ⇒
    pdf p X ∈ Borel_measurable Borel

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

⊢ ∀p A x.
    prob_space p ∧ A ∈ events p ∧ prob p A ≠ 0 ⇒
    x / prob p A * prob p A = x

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

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

⊢ ∀p. prob_space p ⇒
      ∀x. x ∈ events p ⇒ ∃r. prob p x = Normal r ∧ 0 ≤ r ∧ r ≤ 1

⊢ ∀p. FINITE (m_space p) ∧ measurable_sets p = POW (m_space p) ⇒
      (prob_space p ⇔ positive p ∧ prob p (p_space p) = 1 ∧ additive p)

⊢ ∀sp sts u v.
    (∀s. s ∈ sts ⇒ u s = v s) ⇒
    (prob_space (sp,sts,u) ⇔ prob_space (sp,sts,v))

⊢ ∀p1 p2.
    prob_space p1 ∧ p_space p2 = p_space p1 ∧ events p2 = events p1 ∧
    (∀s. s ∈ events p2 ⇒ prob p2 s = prob p1 s) ⇒
    prob_space p2

⊢ prob_space (restrict_space ext_lborel {x | 0 ≤ x ∧ x ≤ 1})

⊢ prob_space (restrict_space ext_lborel {x | 0 < x ∧ x < 1})

⊢ prob_space (restrict_space lborel (interval [(0,1)]))

⊢ prob_space (restrict_space lborel (interval (0,1)))

⊢ ∀p. FINITE (p_space p) ∧ p_space p ≠ ∅ ∧ events p = POW (p_space p) ∧
      (∀s. s ∈ events p ⇒ prob p s = &CARD s / &CARD (p_space p)) ⇒
      prob_space p

⊢ ∀p. FINITE (p_space p) ∧ p_space p ≠ ∅ ∧ events p = POW (p_space p) ∧
      prob p = uniform_distribution (p_space p,events p) ⇒
      prob_space p

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

⊢ ∀p X A f.
    random_variable X p A ∧ f ∈ measurable A A ⇒
    random_variable (f ∘ X) p A

⊢ ∀p X Y A.
    (∀x. x ∈ p_space p ⇒ X x = Y x) ⇒
    (random_variable X p A ⇔ random_variable Y p A)

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

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

⊢ ∀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

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

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ c ≠ 0 ⇒
    real_random_variable (λx. X x / Normal c) p

⊢ ∀p X r.
    prob_space p ∧ real_random_variable X p ⇒
    real_random_variable (λx. Normal r * X x) p

⊢ ∀p X Y.
    (∀x. x ∈ p_space p ⇒ X x = Y x) ⇒
    (real_random_variable X p ⇔ real_random_variable Y p)

⊢ ∀p m. prob_space p ∧ m ≠ +∞ ∧ m ≠ −∞ ⇒ real_random_variable (λx. m) p

⊢ ∀p X.
    prob_space p ⇒
    (real_random_variable (Normal ∘ X) p ⇔ random_variable X p borel)

⊢ ∀p X r.
    prob_space p ∧ real_random_variable X p ⇒
    real_random_variable (λx. exp (X x)) p

⊢ ∀p X r s.
    prob_space p ∧ real_random_variable X p ⇒
    real_random_variable (λx. exp (Normal s * X x)) p

⊢ ∀p X. prob_space p ∧ real_random_variable X p ⇒ real_random_variable X⁻ p

⊢ ∀p X. prob_space p ∧ real_random_variable X p ⇒ real_random_variable X⁺ p

⊢ ∀p E X.
    prob_space p ∧ E ∈ events p ∧ real_random_variable X p ⇒
    real_random_variable (λx. X x * 𝟙 E x) p

⊢ ∀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

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

⊢ ∀p X s n.
    prob_space p ∧ (∀i. i ∈ count n ⇒ real_random_variable (X i) p) ∧
    0 < s n ∧ s n ≠ +∞ ∧ s n ≠ −∞ ⇒
    real_random_variable (λx. ∑ (λi. X i x) (count n) / s n) p

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

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

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

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

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

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

⊢ ∀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

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

⊢ ∀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

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

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

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ∧
    c ≠ 0 ⇒
    variance p (λx. X x / Normal c) = variance p X / Normal c²

⊢ ∀p X c.
    prob_space p ∧ real_random_variable X p ∧ finite_second_moments p X ⇒
    variance p (λx. Normal c * X x) = Normal c² * variance p X

⊢ ∀p f g.
    prob_space p ∧ (∀x. x ∈ p_space p ⇒ f x = g x) ⇒
    variance p f = variance p g

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

⊢ ∀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)²

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

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

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

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

⊢ ∀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

⊢ ∀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

⊢ ∀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

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

⊢ ∀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

⊢ ∀p. prob_space p ⇒ variance p (λx. 0) = 0