Structure probabilityTheory

signature probabilityTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val conditional_distribution_def : thm
    val conditional_expectation_def : thm
    val conditional_prob_def : thm
    val distribution_def : thm
    val events_def : thm
    val expectation_def : thm
    val indep_def : thm
    val indep_families_def : thm
    val indep_function_def : thm
    val indep_rv_def : thm
    val joint_distribution3_def : thm
    val joint_distribution_def : thm
    val p_space_def : thm
    val possibly_def : thm
    val prob_def : thm
    val prob_space_def : thm
    val probably_def : thm
    val random_variable_def : thm
    val real_random_variable_def : thm
    val rv_conditional_expectation_def : thm
    val uniform_distribution_def : thm
  
  (*  Theorems  *)
    val ABS_1_MINUS_PROB : thm
    val ABS_PROB : thm
    val ADDITIVE_PROB : thm
    val COUNTABLY_ADDITIVE_PROB : thm
    val EVENTS : thm
    val EVENTS_ALGEBRA : thm
    val EVENTS_COMPL : thm
    val EVENTS_COUNTABLE_INTER : thm
    val EVENTS_COUNTABLE_UNION : thm
    val EVENTS_DIFF : thm
    val EVENTS_EMPTY : thm
    val EVENTS_INTER : thm
    val EVENTS_SIGMA_ALGEBRA : thm
    val EVENTS_SPACE : thm
    val EVENTS_UNION : thm
    val INCREASING_PROB : thm
    val INDEP_EMPTY : thm
    val INDEP_REFL : thm
    val INDEP_SPACE : thm
    val INDEP_SYM : thm
    val INTER_PSPACE : thm
    val POSITIVE_PROB : thm
    val PROB : thm
    val PROB_ADDITIVE : thm
    val PROB_COMPL : thm
    val PROB_COMPL_LE1 : thm
    val PROB_COUNTABLY_ADDITIVE : thm
    val PROB_COUNTABLY_SUBADDITIVE : thm
    val PROB_COUNTABLY_ZERO : thm
    val PROB_DISCRETE_EVENTS : thm
    val PROB_DISCRETE_EVENTS_COUNTABLE : thm
    val PROB_EMPTY : thm
    val PROB_EQUIPROBABLE_FINITE_UNIONS : thm
    val PROB_EQ_BIGUNION_IMAGE : thm
    val PROB_EQ_COMPL : thm
    val PROB_FINITELY_ADDITIVE : thm
    val PROB_INCREASING : thm
    val PROB_INCREASING_UNION : thm
    val PROB_INDEP : thm
    val PROB_LE_1 : thm
    val PROB_ONE_INTER : thm
    val PROB_POSITIVE : thm
    val PROB_REAL_SUM_IMAGE : thm
    val PROB_REAL_SUM_IMAGE_FN : thm
    val PROB_REAL_SUM_IMAGE_SPACE : thm
    val PROB_SPACE : thm
    val PROB_SPACE_ADDITIVE : thm
    val PROB_SPACE_COUNTABLY_ADDITIVE : thm
    val PROB_SPACE_INCREASING : thm
    val PROB_SPACE_POSITIVE : thm
    val PROB_SUBADDITIVE : thm
    val PROB_UNIV : thm
    val PROB_ZERO_UNION : thm
    val PSPACE : thm
    val conditional_distribution_le_1 : thm
    val conditional_distribution_pos : thm
    val distribution_lebesgue_thm1 : thm
    val distribution_lebesgue_thm2 : thm
    val distribution_partition : thm
    val distribution_pos : thm
    val distribution_prob_space : thm
    val distribution_x_eq_1_imp_distribution_y_eq_0 : thm
    val finite_expectation : thm
    val finite_expectation1 : thm
    val finite_expectation2 : thm
    val finite_marginal_product_space_POW : thm
    val finite_marginal_product_space_POW2 : thm
    val finite_marginal_product_space_POW3 : thm
    val finite_support_expectation : thm
    val joint_conditional : thm
    val joint_distribution_le : thm
    val joint_distribution_le2 : thm
    val joint_distribution_le_1 : thm
    val joint_distribution_pos : thm
    val joint_distribution_sum_mul1 : thm
    val joint_distribution_sums_1 : thm
    val joint_distribution_sym : thm
    val marginal_distribution1 : thm
    val marginal_distribution2 : thm
    val marginal_joint_zero : thm
    val marginal_joint_zero3 : thm
    val prob_x_eq_1_imp_prob_y_eq_0 : thm
    val uniform_distribution_prob_space : thm
  
  val probability_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [lebesgue] Parent theory of "probability"
   
   [conditional_distribution_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀p X s.
            conditional_expectation p X s =
            @f.
                real_random_variable f p ∧
                ∀g.
                    g ∈ s ⇒
                    (integral p (λx. f x * indicator_fn g x) =
                     integral p (λx. X x * indicator_fn g x))
   
   [conditional_prob_def]  Definition
      
      ⊢ ∀p e1 e2.
            conditional_prob p e1 e2 =
            conditional_expectation p (indicator_fn e1) e2
   
   [distribution_def]  Definition
      
      ⊢ ∀p X. distribution p X = (λs. prob p (PREIMAGE X s ∩ p_space p))
   
   [events_def]  Definition
      
      ⊢ events = measurable_sets
   
   [expectation_def]  Definition
      
      ⊢ expectation = integral
   
   [indep_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀p q r. indep_families p q r ⇔ ∀s t. s ∈ q ∧ t ∈ r ⇒ indep p s t
   
   [indep_function_def]  Definition
      
      ⊢ ∀p.
            indep_function p =
            {f |
             indep_families p (IMAGE (PREIMAGE (FST ∘ f)) 𝕌(:β -> bool))
               (IMAGE (PREIMAGE (SND ∘ f)) (events p))}
   
   [indep_rv_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀p X Y.
            joint_distribution p X Y =
            (λa. prob p (PREIMAGE (λx. (X x,Y x)) a ∩ p_space p))
   
   [p_space_def]  Definition
      
      ⊢ p_space = m_space
   
   [possibly_def]  Definition
      
      ⊢ ∀p e. possibly p e ⇔ e ∈ events p ∧ prob p e ≠ 0
   
   [prob_def]  Definition
      
      ⊢ prob = measure
   
   [prob_space_def]  Definition
      
      ⊢ ∀p. prob_space p ⇔ measure_space p ∧ (measure p (p_space p) = 1)
   
   [probably_def]  Definition
      
      ⊢ ∀p e. probably p e ⇔ e ∈ events p ∧ (prob p e = 1)
   
   [random_variable_def]  Definition
      
      ⊢ ∀X p s.
            random_variable X p s ⇔
            prob_space p ∧ X ∈ measurable (p_space p,events p) s
   
   [real_random_variable_def]  Definition
      
      ⊢ ∀X p.
            real_random_variable X p ⇔
            prob_space p ∧
            (∀x. x ∈ p_space p ⇒ X x ≠ NegInf ∧ X x ≠ PosInf) ∧
            X ∈ measurable (p_space p,events p) Borel
   
   [rv_conditional_expectation_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀p X s.
            uniform_distribution p X s = (λa. &CARD a / &CARD (space s))
   
   [ABS_1_MINUS_PROB]  Theorem
      
      ⊢ ∀p s.
            prob_space p ∧ s ∈ events p ∧ prob p s ≠ 0 ⇒
            abs (1 − prob p s) < 1
   
   [ABS_PROB]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ (abs (prob p s) = prob p s)
   
   [ADDITIVE_PROB]  Theorem
      
      ⊢ ∀p.
            additive p ⇔
            ∀s t.
                s ∈ events p ∧ t ∈ events p ∧ DISJOINT s t ⇒
                (prob p (s ∪ t) = prob p s + prob p t)
   
   [COUNTABLY_ADDITIVE_PROB]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a b c. events (a,b,c) = b
   
   [EVENTS_ALGEBRA]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ algebra (p_space p,events p)
   
   [EVENTS_COMPL]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ p_space p DIFF s ∈ events p
   
   [EVENTS_COUNTABLE_INTER]  Theorem
      
      ⊢ ∀p c.
            prob_space p ∧ c ⊆ events p ∧ countable c ∧ c ≠ ∅ ⇒
            BIGINTER c ∈ events p
   
   [EVENTS_COUNTABLE_UNION]  Theorem
      
      ⊢ ∀p c.
            prob_space p ∧ c ⊆ events p ∧ countable c ⇒
            BIGUNION c ∈ events p
   
   [EVENTS_DIFF]  Theorem
      
      ⊢ ∀p s t.
            prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒
            s DIFF t ∈ events p
   
   [EVENTS_EMPTY]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ ∅ ∈ events p
   
   [EVENTS_INTER]  Theorem
      
      ⊢ ∀p s t.
            prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s ∩ t ∈ events p
   
   [EVENTS_SIGMA_ALGEBRA]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ sigma_algebra (p_space p,events p)
   
   [EVENTS_SPACE]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ p_space p ∈ events p
   
   [EVENTS_UNION]  Theorem
      
      ⊢ ∀p s t.
            prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s ∪ t ∈ events p
   
   [INCREASING_PROB]  Theorem
      
      ⊢ ∀p.
            increasing p ⇔
            ∀s t. s ∈ events p ∧ t ∈ events p ∧ s ⊆ t ⇒ prob p s ≤ prob p t
   
   [INDEP_EMPTY]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ indep p ∅ s
   
   [INDEP_REFL]  Theorem
      
      ⊢ ∀p a.
            prob_space p ∧ a ∈ events p ⇒
            (indep p a a ⇔ (prob p a = 0) ∨ (prob p a = 1))
   
   [INDEP_SPACE]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ indep p (p_space p) s
   
   [INDEP_SYM]  Theorem
      
      ⊢ ∀p a b. prob_space p ∧ indep p a b ⇒ indep p b a
   
   [INTER_PSPACE]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ (p_space p ∩ s = s)
   
   [POSITIVE_PROB]  Theorem
      
      ⊢ ∀p. positive p ⇔ (prob p ∅ = 0) ∧ ∀s. s ∈ events p ⇒ 0 ≤ prob p s
   
   [PROB]  Theorem
      
      ⊢ ∀a b c. prob (a,b,c) = c
   
   [PROB_ADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s.
            prob_space p ∧ s ∈ events p ⇒
            (prob p (p_space p DIFF s) = 1 − prob p s)
   
   [PROB_COMPL_LE1]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ (prob p ∅ = 0)
   
   [PROB_EQUIPROBABLE_FINITE_UNIONS]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p.
            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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_INCREASING]  Theorem
      
      ⊢ ∀p s t.
            prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ s ⊆ t ⇒
            prob p s ≤ prob p t
   
   [PROB_INCREASING_UNION]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s t u.
            indep p s t ∧ (u = s ∩ t) ⇒ (prob p u = prob p s * prob p t)
   
   [PROB_LE_1]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s ≤ 1
   
   [PROB_ONE_INTER]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ 0 ≤ prob p s
   
   [PROB_REAL_SUM_IMAGE]  Theorem
      
      ⊢ ∀p s.
            prob_space p ∧ s ∈ events p ∧ (∀x. x ∈ s ⇒ {x} ∈ events p) ∧
            FINITE s ⇒
            (prob p s = SIGMA (λx. prob p {x}) s)
   
   [PROB_REAL_SUM_IMAGE_FN]  Theorem
      
      ⊢ ∀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 = SIGMA (λx. prob p (e ∩ f x)) s)
   
   [PROB_REAL_SUM_IMAGE_SPACE]  Theorem
      
      ⊢ ∀p.
            prob_space p ∧ (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ∧
            FINITE (p_space p) ⇒
            (SIGMA (λx. prob p {x}) (p_space p) = 1)
   
   [PROB_SPACE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ additive p
   
   [PROB_SPACE_COUNTABLY_ADDITIVE]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ countably_additive p
   
   [PROB_SPACE_INCREASING]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ increasing p
   
   [PROB_SPACE_POSITIVE]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ positive p
   
   [PROB_SUBADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ (prob p (p_space p) = 1)
   
   [PROB_ZERO_UNION]  Theorem
      
      ⊢ ∀p s t.
            prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ (prob p t = 0) ⇒
            (prob p (s ∪ t) = prob p s)
   
   [PSPACE]  Theorem
      
      ⊢ ∀a b c. p_space (a,b,c) = a
   
   [conditional_distribution_le_1]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀X p s A.
            random_variable X p s ∧ A ∈ subsets s ⇒
            (Normal (distribution p X A) =
             integral p (indicator_fn (PREIMAGE X A ∩ p_space p)))
   
   [distribution_lebesgue_thm2]  Theorem
      
      ⊢ ∀X p s A.
            random_variable X p s ∧ A ∈ subsets s ⇒
            (Normal (distribution p X A) =
             integral (space s,subsets s,distribution p X) (indicator_fn A))
   
   [distribution_partition]  Theorem
      
      ⊢ ∀p X.
            prob_space p ∧ (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ∧
            FINITE (p_space p) ∧ random_variable X p Borel ⇒
            (SIGMA (λx. distribution p X {x}) (IMAGE X (p_space p)) = 1)
   
   [distribution_pos]  Theorem
      
      ⊢ ∀p X a.
            prob_space p ∧ (events p = POW (p_space p)) ⇒
            0 ≤ distribution p X a
   
   [distribution_prob_space]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X.
            FINITE (p_space p) ∧ real_random_variable X p ⇒
            (expectation p X =
             SIGMA (λr. r * Normal (distribution p X {r}))
               (IMAGE X (p_space p)))
   
   [finite_expectation1]  Theorem
      
      ⊢ ∀p X.
            FINITE (p_space p) ∧ real_random_variable X p ⇒
            (expectation p X =
             SIGMA (λr. r * Normal (prob p (PREIMAGE X {r} ∩ p_space p)))
               (IMAGE X (p_space p)))
   
   [finite_expectation2]  Theorem
      
      ⊢ ∀p X.
            FINITE (IMAGE X (p_space p)) ∧ real_random_variable X p ⇒
            (expectation p X =
             SIGMA (λr. r * Normal (prob p (PREIMAGE X {r} ∩ p_space p)))
               (IMAGE X (p_space p)))
   
   [finite_marginal_product_space_POW]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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)
   
   [finite_support_expectation]  Theorem
      
      ⊢ ∀p X.
            FINITE (IMAGE X (p_space p)) ∧ real_random_variable X p ⇒
            (expectation p X =
             SIGMA (λr. r * Normal (distribution p X {r}))
               (IMAGE X (p_space p)))
   
   [joint_conditional]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X Y a.
            prob_space p ∧ (events p = POW (p_space p)) ⇒
            joint_distribution p X Y a ≤ 1
   
   [joint_distribution_pos]  Theorem
      
      ⊢ ∀p X Y a.
            prob_space p ∧ (events p = POW (p_space p)) ⇒
            0 ≤ joint_distribution p X Y a
   
   [joint_distribution_sum_mul1]  Theorem
      
      ⊢ ∀p X Y f.
            prob_space p ∧ FINITE (p_space p) ∧
            (events p = POW (p_space p)) ⇒
            (SIGMA (λ(x,y). joint_distribution p X Y {(x,y)} * f x)
               (IMAGE X (p_space p) × IMAGE Y (p_space p)) =
             SIGMA (λx. distribution p X {x} * f x) (IMAGE X (p_space p)))
   
   [joint_distribution_sums_1]  Theorem
      
      ⊢ ∀p X Y.
            prob_space p ∧ FINITE (p_space p) ∧
            (events p = POW (p_space p)) ⇒
            (SIGMA (λ(x,y). joint_distribution p X Y {(x,y)})
               (IMAGE X (p_space p) × IMAGE Y (p_space p)) = 1)
   
   [joint_distribution_sym]  Theorem
      
      ⊢ ∀p X Y a b.
            prob_space p ⇒
            (joint_distribution p X Y (a × b) =
             joint_distribution p Y X (b × a))
   
   [marginal_distribution1]  Theorem
      
      ⊢ ∀p X Y a.
            prob_space p ∧ FINITE (p_space p) ∧
            (events p = POW (p_space p)) ⇒
            (distribution p X a =
             SIGMA (λx. joint_distribution p X Y (a × {x}))
               (IMAGE Y (p_space p)))
   
   [marginal_distribution2]  Theorem
      
      ⊢ ∀p X Y b.
            prob_space p ∧ FINITE (p_space p) ∧
            (events p = POW (p_space p)) ⇒
            (distribution p Y b =
             SIGMA (λx. joint_distribution p X Y ({x} × b))
               (IMAGE X (p_space p)))
   
   [marginal_joint_zero]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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)
   
   
*)
end

HOL 4, Kananaskis-13