Structure probabilityTheory
signature probabilityTheory =
sig
type thm = Thm.thm
(* Definitions *)
val PDF_def : thm
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 equivalent_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 pdf_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 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 EXPECTATION_PDF_1 : thm
val INCREASING_PROB : 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 PDF_LE_POS : 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_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_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_INTER : thm
val PROB_ZERO_UNION : thm
val PSPACE : thm
val SLLN_uncorrelated : thm
val SLLN_uncorrelated' : thm
val TOTAL_PROB_SIGMA : thm
val WLLN_uncorrelated : thm
val WLLN_uncorrelated' : thm
val WLLN_uncorrelated_L2 : thm
val chebyshev_ineq : thm
val chebyshev_ineq_variance : thm
val chebyshev_inequality : thm
val conditional_distribution_le_1 : thm
val conditional_distribution_pos : thm
val converge_AE_alt_inf : thm
val converge_AE_alt_liminf : thm
val converge_AE_alt_limsup : thm
val converge_AE_alt_sup : 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_to_zero : thm
val converge_AE_to_zero' : thm
val converge_LP_alt_absolute_moment : thm
val converge_LP_alt_pow : thm
val converge_LP_def : thm
val converge_LP_imp_PR' : thm
val converge_PR_def : thm
val converge_PR_shift : 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_x_eq_1_imp_distribution_y_eq_0 : thm
val equivalent_lemma : thm
val equivalent_thm1 : thm
val equivalent_thm2 : thm
val expectation_bounds : 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_posinf : thm
val expectation_real_affine : 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_all : thm
val finite_second_moments_alt : 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_indicator_fn : thm
val finite_second_moments_literally : thm
val finite_support_expectation : 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_vars_comm : thm
val integrable_absolute_moments : thm
val integrable_from_square : thm
val integrable_imp_finite_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_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_def : thm
val pdf_le_pos : thm
val prob_markov_ineq : thm
val prob_markov_inequality : thm
val prob_x_eq_1_imp_prob_y_eq_0 : thm
val random_variable_compose : thm
val random_variable_functional : thm
val real_random_variable : thm
val real_random_variable_sub : 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_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_indicator_fn : thm
val probability_grammars : type_grammar.grammar * term_grammar.grammar
(*
[martingale] Parent theory of "probability"
[PDF_def] Definition
⊢ ∀p X. PDF p X = distribution p X / lborel
[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))
[equivalent_def] Definition
⊢ ∀p X Y.
equivalent p X Y ⇔
suminf (λn. prob p {x | x ∈ p_space p ∧ X n x ≠ Y n x}) < +∞
[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 ∧ i ∈ 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. E ∈ J --> subsets ∘ A ⇒
indep_events p (λn. PREIMAGE (X n) (E n) ∩ p_space p) J
[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 ⇔
pairwise (λi j. indep p (E i) (E j)) J
[pairwise_indep_sets] Definition
⊢ ∀p A J.
pairwise_indep_sets p A J ⇔
pairwise (λ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 ⇔
pairwise (λi j. indep_vars p (X i) (X j) (A i) (A j)) J
[pdf_def] Definition
⊢ ∀p X. pdf p X = distribution p X / ext_lborel
[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 (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 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
[EXPECTATION_PDF_1] Theorem
⊢ ∀p X.
prob_space p ∧ random_variable X p borel ∧
distribution p X ≪ lborel ⇒
expectation lborel (PDF p X) = 1
[INCREASING_PROB] Theorem
⊢ ∀p. increasing p ⇔
∀s t. s ∈ events p ∧ t ∈ events p ∧ s ⊆ t ⇒ prob p s ≤ prob p t
[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
[PDF_LE_POS] Theorem
⊢ ∀p X.
prob_space p ∧ random_variable X p borel ∧
distribution p X ≪ lborel ⇒
∀x. 0 ≤ PDF p X x
[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_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_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_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
[SLLN_uncorrelated] Theorem
⊢ ∀p X S M.
prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
(∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
(∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
(∀n x. S n x = ∑ (λi. X i x) (count n)) ∧
(∀n. M n = expectation p (S n)) ⇒
((λn x. (S (SUC n) x − M (SUC n)) / &SUC n) --> (λx. 0))
(almost_everywhere p)
[SLLN_uncorrelated'] Theorem
⊢ ∀p X S.
prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
(∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
(∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
(∀n x. S n x = ∑ (λi. X i x) (count n)) ⇒
((λn x. (S n x − expectation p (S n)) / &n) --> (λx. 0))
(almost_everywhere p)
[TOTAL_PROB_SIGMA] 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
[WLLN_uncorrelated] Theorem
⊢ ∀p X S M.
prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
(∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
(∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
(∀n x. S n x = ∑ (λi. X i x) (count n)) ∧
(∀n. M n = expectation p (S n)) ⇒
((λn x. (S (SUC n) x − M (SUC n)) / &SUC n) --> (λx. 0))
(in_probability p)
[WLLN_uncorrelated'] Theorem
⊢ ∀p X S.
prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
(∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
(∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
(∀n x. S n x = ∑ (λi. X i x) (count n)) ⇒
((λn x. (S n x − expectation p (S n)) / &n) --> (λx. 0))
(in_probability p)
[WLLN_uncorrelated_L2] Theorem
⊢ ∀p X S M.
prob_space p ∧ (∀n. real_random_variable (X n) p) ∧
(∀i j. i ≠ j ⇒ uncorrelated p (X i) (X j)) ∧
(∃c. c ≠ +∞ ∧ ∀n. variance p (X n) ≤ c) ∧
(∀n x. S n x = ∑ (λi. X i x) (count n)) ∧
(∀n. M n = expectation p (S n)) ⇒
((λn x. (S (SUC n) x − M (SUC n)) / &SUC n) --> (λx. 0))
(in_lebesgue 2 p)
[chebyshev_ineq] 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_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_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_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_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) ⇒
((λn. X n) --> Y) (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. Z n x = X n x − Y x) ⇒
((X --> Y) (almost_everywhere p) ⇔
(Z --> (λx. 0)) (almost_everywhere p))
[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_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_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) ⇒
((λn. X n) --> Y) (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. 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 ∧ 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 ∧ 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 ∧ 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.
prob_space p ∧
random_variable X p
(IMAGE X (p_space p),POW (IMAGE X (p_space p))) ∧
distribution p X {x} = 1 ⇒
∀y. y ≠ x ⇒ distribution p X {y} = 0
[equivalent_lemma] Theorem
⊢ ∀p X Y.
prob_space p ∧ equivalent p X Y ∧
(∀n. real_random_variable (X n) p) ∧
(∀n. real_random_variable (Y n) p) ⇒
∃N f.
N ∈ null_set p ∧
∀x. x ∈ p_space p DIFF N ⇒ ∀n. f x ≤ n ⇒ X n x − Y n x = 0
[equivalent_thm1] Theorem
⊢ ∀p X Y Z.
prob_space p ∧ equivalent p X Y ∧
(∀n. real_random_variable (X n) p) ∧
(∀n. real_random_variable (Y n) p) ∧
(∀n x. Z n x = ∑ (λn. X n x − Y n x) (count n)) ⇒
∃W. real_random_variable W p ∧ (Z --> W) (almost_everywhere p)
[equivalent_thm2] Theorem
⊢ ∀p X Y a Z.
prob_space p ∧ equivalent p X Y ∧
(∀n. real_random_variable (X n) p) ∧
(∀n. real_random_variable (Y n) p) ∧ mono_increasing a ∧
sup (IMAGE a 𝕌(:num)) = +∞ ∧
(∀n x. Z n x = ∑ (λn. X n x − Y n x) (count n) / a n) ⇒
(Z --> (λx. 0)) (almost_everywhere p)
[expectation_bounds] 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_const] Theorem
⊢ ∀p c. prob_space p ⇒ expectation p (λx. Normal c) = Normal 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_posinf] Theorem
⊢ ∀p. prob_space p ⇒ 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
[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_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_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_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_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))
[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 ∧ J ≠ ∅ ∧
(∀n. n ∈ J ⇒ random_variable (X n) p Borel) ∧
identical_distribution p X Borel 𝕌(:'index) ⇒
∃e. ∀n. n ∈ J ⇒ expectation p (X n) = e
[identical_distribution_integrable] 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 𝕌(:'index) ∧
(∃i. i ∈ J ∧ integrable p (X i)) ⇒
∀n. n ∈ J ⇒ integrable p (X n)
[indep_vars_comm] Theorem
⊢ ∀p X Y s t. indep_vars p X Y s t ⇒ indep_vars p Y X t 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_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_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)
[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_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_compose] Theorem
⊢ ∀p X f.
prob_space p ∧ random_variable X p Borel ∧
f ∈ Borel_measurable Borel ⇒
random_variable (f ∘ X) p Borel
[random_variable_functional] 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
[real_random_variable] Theorem
⊢ ∀X p.
real_random_variable X p ⇔
X ∈ Borel_measurable (p_space p,events p) ∧
∀x. X x ≠ −∞ ∧ X x ≠ +∞
[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_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.
(∀i. i ∈ J ⇒ random_variable (X i) p (A i)) ∧ indep_vars p X A J ⇒
pairwise_indep_vars p X A J
[uncorrelated_covariance] 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) ∧
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_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_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
*)
end
HOL 4, Kananaskis-14