Structure probabilityTheory


Source File Identifier index Theory binding index

signature probabilityTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val absolute_moment_def : thm
    val central_moment_def : thm
    val cond_prob_def : thm
    val conditional_distribution_def : thm
    val conditional_expectation_def : thm
    val conditional_prob_def : thm
    val covariance_def : thm
    val distribution_def : thm
    val distribution_function_def : thm
    val events_def : thm
    val expectation_def : thm
    val finite_second_moments_def : thm
    val identical_distribution_def : thm
    val indep_def : thm
    val indep_events_def : thm
    val indep_families_def : thm
    val indep_function_def : thm
    val indep_rv_def : thm
    val indep_sets_def : thm
    val indep_vars_def : thm
    val joint_distribution3_def : thm
    val joint_distribution_def : thm
    val moment_def : thm
    val orthogonal_def : thm
    val orthogonal_vars_def : thm
    val p_space_def : thm
    val pairwise_indep_events : thm
    val pairwise_indep_sets : thm
    val pairwise_indep_vars : thm
    val possibly_def : thm
    val prob_def : thm
    val prob_density_function_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 second_moment_def : thm
    val standard_deviation_def : thm
    val tail_algebra_def : thm
    val tail_algebra_of_rv_def : thm
    val uncorrelated_def : thm
    val uncorrelated_vars_def : thm
    val uniform_distribution_def : thm
    val variance_def : thm
  
  (*  Theorems  *)
    val ABS_1_MINUS_PROB : thm
    val ABS_PROB : thm
    val ADDITIVE_PROB : thm
    val BAYES_RULE : thm
    val BAYES_RULE_GENERAL_SIGMA : thm
    val Borel_0_1_Law : thm
    val Borel_Cantelli_Lemma1 : thm
    val Borel_Cantelli_Lemma2 : thm
    val Borel_Cantelli_Lemma2p : thm
    val COND_PROB_ADDITIVE : thm
    val COND_PROB_BOUNDS : thm
    val COND_PROB_COMPL : thm
    val COND_PROB_DIFF : thm
    val COND_PROB_FINITE : thm
    val COND_PROB_FINITE_ADDITIVE : thm
    val COND_PROB_INCREASING : thm
    val COND_PROB_INTER_SPLIT : thm
    val COND_PROB_ITSELF : thm
    val COND_PROB_MUL_EQ : thm
    val COND_PROB_MUL_RULE : thm
    val COND_PROB_POS_IMP_PROB_NZ : thm
    val COND_PROB_SWAP : thm
    val COND_PROB_UNION : thm
    val COND_PROB_ZERO : thm
    val COND_PROB_ZERO_INTER : thm
    val COUNTABLY_ADDITIVE_PROB : thm
    val EVENTS : thm
    val EVENTS_ALGEBRA : thm
    val EVENTS_BIGINTER_FN : thm
    val EVENTS_BIGUNION : 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_LIMINF : thm
    val EVENTS_LIMSUP : thm
    val EVENTS_SIGMA_ALGEBRA : thm
    val EVENTS_SPACE : thm
    val EVENTS_UNION : thm
    val INCREASING_PROB : thm
    val INDEP : thm
    val INDEP_COMPL : thm
    val INDEP_COMPL2 : thm
    val INDEP_EMPTY : thm
    val INDEP_FAMILIES_SIGMA : thm
    val INDEP_FAMILIES_SYM : thm
    val INDEP_REFL : thm
    val INDEP_SPACE : thm
    val INDEP_SYM : thm
    val INDEP_SYM_EQ : thm
    val INDICATOR_FN_REAL_RV : thm
    val INTER_PSPACE : thm
    val Kolmogorov_0_1_Law : 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_DIFF_SUBSET : 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_EXTREAL_SUM_IMAGE : thm
    val PROB_EXTREAL_SUM_IMAGE_FN : thm
    val PROB_EXTREAL_SUM_IMAGE_SPACE : thm
    val PROB_FINITE : thm
    val PROB_FINITE_ADDITIVE : thm
    val PROB_GSPEC : thm
    val PROB_INCREASING : thm
    val PROB_INCREASING_UNION : thm
    val PROB_INDEP : thm
    val PROB_INTER_SPLIT : thm
    val PROB_INTER_ZERO : thm
    val PROB_LE_1 : thm
    val PROB_LIMINF : thm
    val PROB_LIMSUP : thm
    val PROB_LT_POSINF : thm
    val PROB_ONE_AE : thm
    val PROB_ONE_AE_EQ : thm
    val PROB_ONE_INTER : thm
    val PROB_POSITIVE : thm
    val PROB_SPACE : thm
    val PROB_SPACE_ADDITIVE : thm
    val PROB_SPACE_COUNTABLY_ADDITIVE : thm
    val PROB_SPACE_INCREASING : thm
    val PROB_SPACE_IN_PSPACE : thm
    val PROB_SPACE_NOT_EMPTY : thm
    val PROB_SPACE_POSITIVE : thm
    val PROB_SPACE_SIGMA_FINITE : thm
    val PROB_SPACE_SUBSET_PSPACE : thm
    val PROB_SUBADDITIVE : thm
    val PROB_UNDER_UNIV : thm
    val PROB_UNIV : thm
    val PROB_ZERO_AE : thm
    val PROB_ZERO_AE_EQ : thm
    val PROB_ZERO_INTER : thm
    val PROB_ZERO_UNION : thm
    val PSPACE : thm
    val TOTAL_PROB_SIGMA : thm
    val bounded_imp_finite_second_moments : thm
    val bounded_imp_finite_second_moments' : thm
    val bounded_imp_integrable : thm
    val chebyshev_ineq : thm
    val chebyshev_ineq_variance : thm
    val chebyshev_ineq_variance' : thm
    val chebyshev_inequality : thm
    val conditional_distribution_le_1 : thm
    val conditional_distribution_pos : thm
    val converge_AE : thm
    val converge_AE_add : thm
    val converge_AE_add_to_zero : thm
    val converge_AE_ainv : thm
    val converge_AE_ainv_to_zero : thm
    val converge_AE_alt_inf : thm
    val converge_AE_alt_liminf : thm
    val converge_AE_alt_limsup : thm
    val converge_AE_alt_limsup' : thm
    val converge_AE_alt_shift : thm
    val converge_AE_alt_sup : thm
    val converge_AE_cong : thm
    val converge_AE_cong_full : thm
    val converge_AE_def : thm
    val converge_AE_imp_PR : thm
    val converge_AE_imp_PR' : thm
    val converge_AE_shift : thm
    val converge_AE_sub : thm
    val converge_AE_to_limit : thm
    val converge_AE_to_limit' : thm
    val converge_AE_to_zero : thm
    val converge_AE_to_zero' : thm
    val converge_LP : thm
    val converge_LP_alt_absolute_moment : thm
    val converge_LP_alt_pow : thm
    val converge_LP_cong : thm
    val converge_LP_def : thm
    val converge_LP_imp_PR' : thm
    val converge_PR : thm
    val converge_PR_add : thm
    val converge_PR_add_to_zero : thm
    val converge_PR_ainv : thm
    val converge_PR_ainv_to_zero : thm
    val converge_PR_alt_shift : thm
    val converge_PR_cong : thm
    val converge_PR_cong_full : thm
    val converge_PR_def : thm
    val converge_PR_shift : thm
    val converge_PR_sub : thm
    val converge_PR_to_limit : thm
    val converge_PR_to_limit' : thm
    val converge_PR_to_zero : thm
    val converge_PR_to_zero' : thm
    val covariance_self : thm
    val distribution_distr : thm
    val distribution_function : thm
    val distribution_le_1 : thm
    val distribution_lebesgue_thm1 : thm
    val distribution_lebesgue_thm2 : thm
    val distribution_not_infty : thm
    val distribution_partition : thm
    val distribution_pos : thm
    val distribution_prob_space : thm
    val distribution_space_eq_1 : thm
    val distribution_x_eq_1_imp_distribution_y_eq_0 : thm
    val expectation_bounds : thm
    val expectation_cdiv : thm
    val expectation_cmul : thm
    val expectation_cong : thm
    val expectation_const : thm
    val expectation_converge : thm
    val expectation_converge' : thm
    val expectation_distribution : thm
    val expectation_finite : thm
    val expectation_indicator : thm
    val expectation_normal : thm
    val expectation_pdf_1 : thm
    val expectation_pos : thm
    val expectation_real_affine : thm
    val expectation_sum : thm
    val expectation_zero : 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_second_moments_add : thm
    val finite_second_moments_ainv : thm
    val finite_second_moments_all : thm
    val finite_second_moments_alt : thm
    val finite_second_moments_cdiv : thm
    val finite_second_moments_cmul : thm
    val finite_second_moments_cong : thm
    val finite_second_moments_eq_finite_variance : thm
    val finite_second_moments_eq_integrable_square : thm
    val finite_second_moments_eq_integrable_squares : thm
    val finite_second_moments_imp_finite_expectation : thm
    val finite_second_moments_imp_integrable : thm
    val finite_second_moments_imp_integrable_mul : thm
    val finite_second_moments_indicator_fn : thm
    val finite_second_moments_literally : thm
    val finite_second_moments_sub : thm
    val finite_second_moments_sum : thm
    val finite_support_expectation : thm
    val fundamental_theorem_of_random_vectors : thm
    val identical_distribution_alt : thm
    val identical_distribution_alt' : thm
    val identical_distribution_alt_prob : thm
    val identical_distribution_cong : thm
    val identical_distribution_expectation : thm
    val identical_distribution_expectation_general : thm
    val identical_distribution_integrable : thm
    val identical_distribution_integrable_general : thm
    val indep_alt_cond_prob : thm
    val indep_rv_alt_indep_vars : thm
    val indep_rv_cong : thm
    val indep_vars_alt_indep_events : thm
    val indep_vars_alt_univ : thm
    val indep_vars_comm : thm
    val indep_vars_cong : thm
    val indep_vars_expectation : thm
    val indep_vars_imp_uncorrelated : thm
    val indep_vars_subset : thm
    val integrable_absolute_moments : thm
    val integrable_from_square : thm
    val integrable_imp_finite_expectation : thm
    val joint_conditional : thm
    val joint_distribution3_alt : thm
    val joint_distribution_alt : thm
    val joint_distribution_le : thm
    val joint_distribution_le2 : thm
    val joint_distribution_le_1 : thm
    val joint_distribution_not_infty : 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 pairwise_indep_events_def : thm
    val pairwise_indep_sets_def : thm
    val pairwise_indep_vars_cong : thm
    val pairwise_indep_vars_def : thm
    val pairwise_indep_vars_imp_uncorrelated : thm
    val pairwise_indep_vars_subset : thm
    val pdf_le_pos : thm
    val prob_markov_ineq : thm
    val prob_markov_inequality : thm
    val prob_normal : thm
    val prob_on_finite_set : thm
    val prob_x_eq_1_imp_prob_y_eq_0 : thm
    val random_variable_comp : thm
    val random_variable_cong : thm
    val real_random_variable : thm
    val real_random_variable_add : thm
    val real_random_variable_ainv : thm
    val real_random_variable_cdiv : thm
    val real_random_variable_cmul : thm
    val real_random_variable_cong : thm
    val real_random_variable_const : thm
    val real_random_variable_fn_minus : thm
    val real_random_variable_fn_plus : thm
    val real_random_variable_mul_indicator : thm
    val real_random_variable_sub : thm
    val real_random_variable_sum : thm
    val real_random_variable_zero : thm
    val second_moment_alt : thm
    val second_moment_pos : thm
    val total_imp_pairwise_indep_events : thm
    val total_imp_pairwise_indep_sets : thm
    val total_imp_pairwise_indep_vars : thm
    val uncorrelated_covariance : thm
    val uncorrelated_orthogonal : thm
    val uncorrelated_thm : thm
    val uniform_distribution_prob_space : thm
    val variance_alt : thm
    val variance_cdiv : thm
    val variance_cmul : thm
    val variance_cong : thm
    val variance_const : thm
    val variance_eq : thm
    val variance_eq_indicator_fn : thm
    val variance_le : thm
    val variance_le_indicator_fn : thm
    val variance_pos : thm
    val variance_real_affine : thm
    val variance_real_affine' : thm
    val variance_sum : thm
    val variance_sum' : thm
    val variance_sum_indicator_fn : thm
    val variance_zero : thm
  
  val probability_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [martingale] Parent theory of "probability"
   
   [absolute_moment_def]  Definition
      
      ⊢ ∀p X a r.
          absolute_moment p X a r = expectation p (λx. abs (X x − a) pow r)
   
   [central_moment_def]  Definition
      
      ⊢ ∀p X r. central_moment p X r = moment p X (expectation p X) r
   
   [cond_prob_def]  Definition
      
      ⊢ ∀p e1 e2. cond_prob p e1 e2 = prob p (e1 ∩ e2) / prob p e2
   
   [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 ⇒
                  expectation p (λx. f x * 𝟙 g x) =
                  expectation p (λx. X x * 𝟙 g x)
   
   [conditional_prob_def]  Definition
      
      ⊢ ∀p e1 e2.
          conditional_prob p e1 e2 = conditional_expectation p (𝟙 e1) e2
   
   [covariance_def]  Definition
      
      ⊢ ∀p X Y.
          covariance p X Y =
          expectation p
            (λx. (X x − expectation p X) * (Y x − expectation p Y))
   
   [distribution_def]  Definition
      
      ⊢ ∀p X. distribution p X = (λs. prob p (PREIMAGE X s ∩ p_space p))
   
   [distribution_function_def]  Definition
      
      ⊢ ∀p X.
          distribution_function p X =
          (λx. prob p ({w | X w ≤ x} ∩ p_space p))
   
   [events_def]  Definition
      
      ⊢ events = measurable_sets
   
   [expectation_def]  Definition
      
      ⊢ expectation = ∫
   
   [finite_second_moments_def]  Definition
      
      ⊢ ∀p X. finite_second_moments p X ⇔ ∃a. second_moment p X a < +∞
   
   [identical_distribution_def]  Definition
      
      ⊢ ∀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
   
   [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_events_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀p q r. indep_sets p q r ⇔ ∀s t. s ∈ q ∧ t ∈ r ⇒ indep p s t
   
   [indep_function_def]  Definition
      
      ⊢ ∀p. indep_function p =
            {f |
             indep_sets p (IMAGE (PREIMAGE (FST ∘ f)) 𝕌(:β -> bool))
               (IMAGE (PREIMAGE (SND ∘ f)) (events p))}
   
   [indep_rv_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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
   
   [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))
   
   [moment_def]  Definition
      
      ⊢ ∀p X a r. moment p X a r = expectation p (λx. (X x − a) pow r)
   
   [orthogonal_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ p_space = m_space
   
   [pairwise_indep_events]  Definition
      
      ⊢ ∀p E J.
          pairwise_indep_events p E J ⇔
          pairwiseD (λi j. indep p (E i) (E j)) J
   
   [pairwise_indep_sets]  Definition
      
      ⊢ ∀p A J.
          pairwise_indep_sets p A J ⇔
          pairwiseD (λi j. indep_sets p (A i) (A j)) J
   
   [pairwise_indep_vars]  Definition
      
      ⊢ ∀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
   
   [possibly_def]  Definition
      
      ⊢ ∀p e. possibly p e ⇔ e ∈ events p ∧ prob p e ≠ 0
   
   [prob_def]  Definition
      
      ⊢ prob = measure
   
   [prob_density_function_def]  Definition
      
      ⊢ ∀p X. pdf p X = distribution p X / ext_lborel
   
   [prob_space_def]  Definition
      
      ⊢ ∀p. prob_space p ⇔ measure_space p ∧ measure p (m_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 ⇔ X ∈ measurable (p_space p,events p) s
   
   [real_random_variable_def]  Definition
      
      ⊢ ∀X p.
          real_random_variable X p ⇔
          random_variable X p Borel ∧
          ∀x. x ∈ p_space p ⇒ X x ≠ −∞ ∧ X x ≠ +∞
   
   [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))
   
   [second_moment_def]  Definition
      
      ⊢ ∀p X a. second_moment p X a = moment p X a 2
   
   [standard_deviation_def]  Definition
      
      ⊢ ∀p X. standard_deviation p X = sqrt (variance p X)
   
   [tail_algebra_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀s. uniform_distribution s = (λa. &CARD a / &CARD (space s))
   
   [variance_def]  Definition
      
      ⊢ ∀p X. variance p X = central_moment p X 2
   
   [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 ∧ s ∪ t ∈ events p ⇒
              prob p (s ∪ t) = prob p s + prob p t
   
   [BAYES_RULE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p E.
          prob_space p ∧ (∀n. E n ∈ events p) ∧ suminf (prob p ∘ E) < +∞ ⇒
          prob p (limsup E) = 0
   
   [Borel_Cantelli_Lemma2]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p B.
          prob_space p ∧ B ∈ events p ∧ prob p B ≠ 0 ⇒ cond_prob p B B = 1
   
   [COND_PROB_MUL_EQ]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  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 (BIGUNION (IMAGE f 𝕌(:num))) = suminf (prob p ∘ f)
   
   [EVENTS]  Theorem
      
      ⊢ ∀a b c. events (a,b,c) = b
   
   [EVENTS_ALGEBRA]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ algebra (p_space p,events p)
   
   [EVENTS_BIGINTER_FN]  Theorem
      
      ⊢ ∀p A J.
          prob_space p ∧ IMAGE A J ⊆ events p ∧ countable J ∧ J ≠ ∅ ⇒
          BIGINTER (IMAGE A J) ∈ events p
   
   [EVENTS_BIGUNION]  Theorem
      
      ⊢ ∀p f n.
          prob_space p ∧ f ∈ (count n → events p) ⇒
          BIGUNION (IMAGE f (count n)) ∈ 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_LIMINF]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ (∀n. E n ∈ events p) ⇒ liminf E ∈ events p
   
   [EVENTS_LIMSUP]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ (∀n. E n ∈ events p) ⇒ limsup E ∈ 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]  Theorem
      
      ⊢ ∀p a b.
          a ∈ events p ∧ b ∈ events p ∧
          prob p (a ∩ b) = prob p a * prob p b ⇒
          indep p a b
   
   [INDEP_COMPL]  Theorem
      
      ⊢ ∀p s t. prob_space p ∧ indep p s t ⇒ indep p s (p_space p DIFF t)
   
   [INDEP_COMPL2]  Theorem
      
      ⊢ ∀p s t.
          prob_space p ∧ indep p s t ⇒
          indep p (p_space p DIFF s) (p_space p DIFF t)
   
   [INDEP_EMPTY]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ indep p ∅ s
   
   [INDEP_FAMILIES_SIGMA]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p q r. indep_sets p q r ⇒ indep_sets p r q
   
   [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. indep p a b ⇒ indep p b a
   
   [INDEP_SYM_EQ]  Theorem
      
      ⊢ ∀p a b. indep p a b ⇔ indep p b a
   
   [INDICATOR_FN_REAL_RV]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ real_random_variable (𝟙 s) p
   
   [INTER_PSPACE]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ p_space p ∩ s = s
   
   [Kolmogorov_0_1_Law]  Theorem
      
      ⊢ ∀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
   
   [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 s = suminf (prob p ∘ f)
   
   [PROB_COUNTABLY_SUBADDITIVE]  Theorem
      
      ⊢ ∀p f.
          prob_space p ∧ IMAGE f 𝕌(:num) ⊆ events p ⇒
          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_DIFF_SUBSET]  Theorem
      
      ⊢ ∀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]  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 ∧ 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]  Theorem
      
      ⊢ ∀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]  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_EXTREAL_SUM_IMAGE]  Theorem
      
      ⊢ ∀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]  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 = ∑ (λx. prob p (e ∩ f x)) s
   
   [PROB_EXTREAL_SUM_IMAGE_SPACE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s ≠ −∞ ∧ prob p s ≠ +∞
   
   [PROB_FINITE_ADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀P p s. prob p {x | x ∈ s ∧ P x} = prob p ({x | P x} ∩ 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 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]  Theorem
      
      ⊢ ∀p s t u. indep p s t ∧ u = s ∩ t ⇒ prob p u = prob p s * prob p t
   
   [PROB_INTER_SPLIT]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p A B.
          prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ prob p B = 0 ⇒
          prob p (A ∩ B) = 0
   
   [PROB_LE_1]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s ≤ 1
   
   [PROB_LIMINF]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ prob p s < +∞
   
   [PROB_ONE_AE]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ E ∈ events p ∧ prob p E = 1 ⇒ AE x::p. x ∈ E
   
   [PROB_ONE_AE_EQ]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ E ∈ events p ⇒ (prob p E = 1 ⇔ AE x::p. x ∈ E)
   
   [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_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_IN_PSPACE]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ E ∈ events p ⇒ ∀x. x ∈ E ⇒ x ∈ p_space p
   
   [PROB_SPACE_NOT_EMPTY]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ p_space p ≠ ∅
   
   [PROB_SPACE_POSITIVE]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ positive p
   
   [PROB_SPACE_SIGMA_FINITE]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ sigma_finite p
   
   [PROB_SPACE_SUBSET_PSPACE]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ s ⊆ p_space p
   
   [PROB_SUBADDITIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s.
          prob_space p ∧ s ∈ events p ⇒ prob p (s ∩ p_space p) = prob p s
   
   [PROB_UNIV]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ prob p (p_space p) = 1
   
   [PROB_ZERO_AE]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ E ∈ events p ∧ prob p E = 0 ⇒ AE x::p. x ∉ E
   
   [PROB_ZERO_AE_EQ]  Theorem
      
      ⊢ ∀p E. prob_space p ∧ E ∈ events p ⇒ (prob p E = 0 ⇔ AE x::p. x ∉ E)
   
   [PROB_ZERO_INTER]  Theorem
      
      ⊢ ∀p A B.
          prob_space p ∧ A ∈ events p ∧ B ∈ events p ∧ prob p A = 0 ⇒
          prob p (A ∩ B) = 0
   
   [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
   
   [TOTAL_PROB_SIGMA]  Theorem
      
      ⊢ ∀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
   
   [bounded_imp_finite_second_moments]  Theorem
      
      ⊢ ∀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
   
   [bounded_imp_finite_second_moments']  Theorem
      
      ⊢ ∀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
   
   [bounded_imp_integrable]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ random_variable X p Borel ∧
          (∃r. ∀x. x ∈ p_space p ⇒ abs (X x) ≤ Normal r) ⇒
          integrable p X
   
   [chebyshev_ineq]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_ineq_variance']  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X Y.
          (∀n. real_random_variable (X n) p) ∧ real_random_variable Y p ⇒
          ((X --> Y) (almost_everywhere p) ⇔
           AE x::p. ((λn. X n x) --> Y x) sequentially)
   
   [converge_AE_add]  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_add_to_zero]  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_ainv]  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_ainv_to_zero]  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_alt_inf]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_limsup']  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_alt_shift]  Theorem
      
      ⊢ ∀D p X Y.
          (X --> Y) (almost_everywhere p) ⇔
          ((λn. X (n + D)) --> Y) (almost_everywhere p)
   
   [converge_AE_alt_sup]  Theorem
      
      ⊢ ∀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_cong]  Theorem
      
      ⊢ ∀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))
   
   [converge_AE_cong_full]  Theorem
      
      ⊢ ∀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))
   
   [converge_AE_def]  Theorem
      
      ⊢ ∀p X Y.
          (X --> Y) (almost_everywhere p) ⇔
          AE x::p. ((λn. real (X n x)) --> real (Y x)) sequentially
   
   [converge_AE_imp_PR]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X Y.
          ((λn. X (SUC n)) --> Y) (almost_everywhere p) ⇒
          (X --> Y) (almost_everywhere p)
   
   [converge_AE_sub]  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_to_limit]  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_to_limit']  Theorem
      
      ⊢ ∀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)
   
   [converge_AE_to_zero]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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))
   
   [converge_LP]  Theorem
      
      ⊢ ∀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. expectation p (λx. abs (X n x − Y x) powr r)) --> 0)
             sequentially)
   
   [converge_LP_alt_absolute_moment]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_cong]  Theorem
      
      ⊢ ∀p X Y Z k.
          prob_space p ∧ (∀n x. x ∈ p_space p ⇒ X n x = Y n x) ⇒
          ((X --> Z) (in_lebesgue k p) ⇔ (Y --> Z) (in_lebesgue k p))
   
   [converge_LP_def]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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. prob p {x | x ∈ p_space p ∧ e < abs (X n x − Y x)}) -->
                0) sequentially)
   
   [converge_PR_add]  Theorem
      
      ⊢ ∀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)
   
   [converge_PR_add_to_zero]  Theorem
      
      ⊢ ∀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)
   
   [converge_PR_ainv]  Theorem
      
      ⊢ ∀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)
   
   [converge_PR_ainv_to_zero]  Theorem
      
      ⊢ ∀p X.
          (X --> (λx. 0)) (in_probability p) ⇒
          ((λn x. -X n x) --> (λx. 0)) (in_probability p)
   
   [converge_PR_alt_shift]  Theorem
      
      ⊢ ∀D p X Y.
          (X --> Y) (in_probability p) ⇔
          ((λn. X (n + D)) --> Y) (in_probability p)
   
   [converge_PR_cong]  Theorem
      
      ⊢ ∀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))
   
   [converge_PR_cong_full]  Theorem
      
      ⊢ ∀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))
   
   [converge_PR_def]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X Y.
          ((λn. X (SUC n)) --> Y) (in_probability p) ⇒
          (X --> Y) (in_probability p)
   
   [converge_PR_sub]  Theorem
      
      ⊢ ∀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)
   
   [converge_PR_to_limit]  Theorem
      
      ⊢ ∀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)
   
   [converge_PR_to_limit']  Theorem
      
      ⊢ ∀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)
   
   [converge_PR_to_zero]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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))
   
   [covariance_self]  Theorem
      
      ⊢ ∀p X. covariance p X X = variance p X
   
   [distribution_distr]  Theorem
      
      ⊢ distribution = distr
   
   [distribution_function]  Theorem
      
      ⊢ ∀p X t. distribution_function p X t = distribution p X {x | x ≤ t}
   
   [distribution_le_1]  Theorem
      
      ⊢ ∀p X a.
          prob_space p ∧ events p = POW (p_space p) ⇒
          distribution p X a ≤ 1
   
   [distribution_lebesgue_thm1]  Theorem
      
      ⊢ ∀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))
   
   [distribution_lebesgue_thm2]  Theorem
      
      ⊢ ∀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)
   
   [distribution_not_infty]  Theorem
      
      ⊢ ∀p X a.
          prob_space p ∧ events p = POW (p_space p) ⇒
          distribution p X a ≠ −∞ ∧ distribution p X 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 ⇒
          ∑ (λ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.
          prob_space p ∧ sigma_algebra s ∧ random_variable X p s ⇒
          prob_space (space s,subsets s,distribution p X)
   
   [distribution_space_eq_1]  Theorem
      
      ⊢ ∀p X. prob_space p ⇒ distribution p X (IMAGE X (p_space p)) = 1
   
   [distribution_x_eq_1_imp_distribution_y_eq_0]  Theorem
      
      ⊢ ∀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
   
   [expectation_bounds]  Theorem
      
      ⊢ ∀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_cdiv]  Theorem
      
      ⊢ ∀p X c.
          prob_space p ∧ integrable p X ∧ c ≠ 0 ⇒
          expectation p (λx. X x / Normal c) = expectation p X / Normal c
   
   [expectation_cmul]  Theorem
      
      ⊢ ∀p X c.
          prob_space p ∧ integrable p X ⇒
          expectation p (λx. Normal c * X x) = Normal c * expectation p X
   
   [expectation_cong]  Theorem
      
      ⊢ ∀p f g.
          prob_space p ∧ (∀x. x ∈ p_space p ⇒ f x = g x) ⇒
          expectation p f = expectation p g
   
   [expectation_const]  Theorem
      
      ⊢ ∀p c. prob_space p ⇒ expectation p (λx. c) = c
   
   [expectation_converge]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ integrable p X ⇒
          expectation p X ≠ +∞ ∧ expectation p X ≠ −∞
   
   [expectation_indicator]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ expectation p (𝟙 s) = prob p s
   
   [expectation_normal]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ integrable p X ⇒ ∃r. expectation p X = Normal r
   
   [expectation_pdf_1]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ random_variable X p Borel ∧
          distribution p X ≪ ext_lborel ⇒
          expectation ext_lborel (pdf p X) = 1
   
   [expectation_pos]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ (∀x. x ∈ p_space p ⇒ 0 ≤ X x) ⇒
          0 ≤ expectation p X
   
   [expectation_real_affine]  Theorem
      
      ⊢ ∀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
   
   [expectation_sum]  Theorem
      
      ⊢ ∀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
   
   [expectation_zero]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ expectation p (λx. 0) = 0
   
   [finite_expectation]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_add]  Theorem
      
      ⊢ ∀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)
   
   [finite_second_moments_ainv]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ∧
          finite_second_moments p X ⇒
          finite_second_moments p (λx. -X x)
   
   [finite_second_moments_all]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ⇒
          (finite_second_moments p X ⇔ second_moment p X 0 < +∞)
   
   [finite_second_moments_cdiv]  Theorem
      
      ⊢ ∀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)
   
   [finite_second_moments_cmul]  Theorem
      
      ⊢ ∀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)
   
   [finite_second_moments_cong]  Theorem
      
      ⊢ ∀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)
   
   [finite_second_moments_eq_finite_variance]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ⇒
          (finite_second_moments p X ⇔ variance p X < +∞)
   
   [finite_second_moments_eq_integrable_square]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ∧
          finite_second_moments p X ⇒
          integrable p X
   
   [finite_second_moments_imp_integrable_mul]  Theorem
      
      ⊢ ∀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)
   
   [finite_second_moments_indicator_fn]  Theorem
      
      ⊢ ∀p s. prob_space p ∧ s ∈ events p ⇒ finite_second_moments p (𝟙 s)
   
   [finite_second_moments_literally]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ⇒
          (finite_second_moments p X ⇔ expectation p (λx. (X x)²) < +∞)
   
   [finite_second_moments_sub]  Theorem
      
      ⊢ ∀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)
   
   [finite_second_moments_sum]  Theorem
      
      ⊢ ∀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)
   
   [finite_support_expectation]  Theorem
      
      ⊢ ∀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))
   
   [fundamental_theorem_of_random_vectors]  Theorem
      
      ⊢ ∀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
   
   [identical_distribution_alt]  Theorem
      
      ⊢ ∀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)
   
   [identical_distribution_alt']  Theorem
      
      ⊢ ∀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))
   
   [identical_distribution_alt_prob]  Theorem
      
      ⊢ ∀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}
   
   [identical_distribution_cong]  Theorem
      
      ⊢ ∀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)
   
   [identical_distribution_expectation]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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
   
   [identical_distribution_integrable]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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)
   
   [indep_alt_cond_prob]  Theorem
      
      ⊢ ∀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)
   
   [indep_rv_alt_indep_vars]  Theorem
      
      ⊢ ∀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})
   
   [indep_rv_cong]  Theorem
      
      ⊢ ∀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
   
   [indep_vars_alt_indep_events]  Theorem
      
      ⊢ ∀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)
   
   [indep_vars_alt_univ]  Theorem
      
      ⊢ ∀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))
   
   [indep_vars_comm]  Theorem
      
      ⊢ ∀p X Y s t. indep_vars p X Y s t ⇒ indep_vars p Y X t s
   
   [indep_vars_cong]  Theorem
      
      ⊢ ∀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
   
   [indep_vars_expectation]  Theorem
      
      ⊢ ∀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
   
   [indep_vars_imp_uncorrelated]  Theorem
      
      ⊢ ∀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
   
   [indep_vars_subset]  Theorem
      
      ⊢ ∀p X A s t. indep_vars p X A t ∧ s ⊆ t ⇒ indep_vars p X A s
   
   [integrable_absolute_moments]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ∧
          integrable p (λx. (X x)²) ⇒
          integrable p X
   
   [integrable_imp_finite_expectation]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ integrable p X ⇒
          expectation p X ≠ +∞ ∧ expectation p X ≠ −∞
   
   [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_distribution3_alt]  Theorem
      
      ⊢ ∀p X Y Z.
          joint_distribution3 p X Y Z = distribution p (λx. (X x,Y x,Z x))
   
   [joint_distribution_alt]  Theorem
      
      ⊢ ∀p X Y. joint_distribution p X Y = distribution p (λx. (X x,Y x))
   
   [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_not_infty]  Theorem
      
      ⊢ ∀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]  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) ∧
          (∀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]  Theorem
      
      ⊢ ∀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]  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 =
          ∑ (λ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 =
          ∑ (λ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
   
   [pairwise_indep_events_def]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_cong]  Theorem
      
      ⊢ ∀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
   
   [pairwise_indep_vars_def]  Theorem
      
      ⊢ ∀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)
   
   [pairwise_indep_vars_imp_uncorrelated]  Theorem
      
      ⊢ ∀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
   
   [pairwise_indep_vars_subset]  Theorem
      
      ⊢ ∀p X A s t.
          pairwise_indep_vars p X A t ∧ s ⊆ t ⇒ pairwise_indep_vars p X A s
   
   [pdf_le_pos]  Theorem
      
      ⊢ ∀p X x.
          prob_space p ∧ random_variable X p Borel ∧
          distribution p X ≪ ext_lborel ⇒
          0 ≤ pdf p X x
   
   [prob_markov_ineq]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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_normal]  Theorem
      
      ⊢ ∀p. prob_space p ⇒
            ∀x. x ∈ events p ⇒ ∃r. prob p x = Normal r ∧ 0 ≤ r ∧ r ≤ 1
   
   [prob_on_finite_set]  Theorem
      
      ⊢ ∀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)
   
   [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
   
   [random_variable_comp]  Theorem
      
      ⊢ ∀p X A f.
          random_variable X p A ∧ f ∈ measurable A A ⇒
          random_variable (f ∘ X) p A
   
   [random_variable_cong]  Theorem
      
      ⊢ ∀p X Y A.
          (∀x. x ∈ p_space p ⇒ X x = Y x) ⇒
          (random_variable X p A ⇔ random_variable Y p A)
   
   [real_random_variable]  Theorem
      
      ⊢ ∀X p.
          real_random_variable X p ⇔
          X ∈ Borel_measurable (p_space p,events p) ∧
          ∀x. x ∈ p_space p ⇒ X x ≠ −∞ ∧ X x ≠ +∞
   
   [real_random_variable_add]  Theorem
      
      ⊢ ∀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_ainv]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ⇒
          real_random_variable (λx. -X x) p
   
   [real_random_variable_cdiv]  Theorem
      
      ⊢ ∀p X c.
          prob_space p ∧ real_random_variable X p ∧ c ≠ 0 ⇒
          real_random_variable (λx. X x / Normal c) p
   
   [real_random_variable_cmul]  Theorem
      
      ⊢ ∀p X r.
          prob_space p ∧ real_random_variable X p ⇒
          real_random_variable (λx. Normal r * X x) p
   
   [real_random_variable_cong]  Theorem
      
      ⊢ ∀p X Y.
          (∀x. x ∈ p_space p ⇒ X x = Y x) ⇒
          (real_random_variable X p ⇔ real_random_variable Y p)
   
   [real_random_variable_const]  Theorem
      
      ⊢ ∀p m.
          prob_space p ∧ m ≠ +∞ ∧ m ≠ −∞ ⇒ real_random_variable (λx. m) p
   
   [real_random_variable_fn_minus]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ⇒
          real_random_variable X⁻ p
   
   [real_random_variable_fn_plus]  Theorem
      
      ⊢ ∀p X.
          prob_space p ∧ real_random_variable X p ⇒
          real_random_variable X⁺ p
   
   [real_random_variable_mul_indicator]  Theorem
      
      ⊢ ∀p E X.
          prob_space p ∧ E ∈ events p ∧ real_random_variable X p ⇒
          real_random_variable (λx. X x * 𝟙 E x) p
   
   [real_random_variable_sub]  Theorem
      
      ⊢ ∀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_sum]  Theorem
      
      ⊢ ∀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
   
   [real_random_variable_zero]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ real_random_variable (λx. 0) p
   
   [second_moment_alt]  Theorem
      
      ⊢ ∀p X. second_moment p X 0 = expectation p (λx. (X x)²)
   
   [second_moment_pos]  Theorem
      
      ⊢ ∀p X a. prob_space p ⇒ 0 ≤ second_moment p X a
   
   [total_imp_pairwise_indep_events]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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
   
   [uncorrelated_covariance]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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)
   
   [variance_alt]  Theorem
      
      ⊢ ∀p X. variance p X = expectation p (λx. (X x − expectation p X)²)
   
   [variance_cdiv]  Theorem
      
      ⊢ ∀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²
   
   [variance_cmul]  Theorem
      
      ⊢ ∀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
   
   [variance_cong]  Theorem
      
      ⊢ ∀p f g.
          prob_space p ∧ (∀x. x ∈ p_space p ⇒ f x = g x) ⇒
          variance p f = variance p g
   
   [variance_const]  Theorem
      
      ⊢ ∀p c. prob_space p ⇒ variance p (λx. Normal c) = 0
   
   [variance_eq]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s.
          prob_space p ∧ s ∈ events p ⇒
          variance p (𝟙 s) = expectation p (𝟙 s) − (expectation p (𝟙 s))²
   
   [variance_le]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p s.
          prob_space p ∧ s ∈ events p ⇒
          variance p (𝟙 s) ≤ expectation p (𝟙 s)
   
   [variance_pos]  Theorem
      
      ⊢ ∀p X. prob_space p ⇒ 0 ≤ variance p X
   
   [variance_real_affine]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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
   
   [variance_sum_indicator_fn]  Theorem
      
      ⊢ ∀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
   
   [variance_zero]  Theorem
      
      ⊢ ∀p. prob_space p ⇒ variance p (λx. 0) = 0
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1