Theory "probability"

Parents lebesgue

Signature

Constant	Type
conditional_distribution	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> β) -> (α -> γ) -> (β -> bool) -> (γ -> bool) -> real
conditional_expectation	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> ((α -> bool) -> bool) -> α -> extreal
conditional_prob	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> ((α -> bool) -> bool) -> α -> extreal
distribution	:(β -> bool) # ((β -> bool) -> bool) # ((β -> bool) -> real) -> (β -> α) -> (α -> bool) -> real
events	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
expectation	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> extreal) -> extreal
indep	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) reln
indep_rv	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> β) -> (α -> γ) -> (β -> bool) # ((β -> bool) -> bool) -> (γ -> bool) # ((γ -> bool) -> bool) -> bool
joint_distribution	:(γ -> bool) # ((γ -> bool) -> bool) # ((γ -> bool) -> real) -> (γ -> α) -> (γ -> β) -> (α # β -> bool) -> real
joint_distribution3	:(δ -> bool) # ((δ -> bool) -> bool) # ((δ -> bool) -> real) -> (δ -> α) -> (δ -> β) -> (δ -> γ) -> (α # β # γ -> bool) -> real
p_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> α -> bool
possibly	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
prob	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> real
prob_space	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
probably	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> bool) -> bool
random_variable	:(α -> β) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) -> bool
real_random_variable	:(α -> extreal) -> (α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> bool
rv_conditional_expectation	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (β -> bool) # ((β -> bool) -> bool) -> (α -> extreal) -> (α -> β) -> α -> extreal
uniform_distribution	:β -> γ -> (δ -> bool) # ((δ -> bool) -> bool) -> (α -> bool) -> real

Definitions

p_space_def

|- p_space = m_space

events_def

|- events = measurable_sets

prob_def

|- prob = measure

prob_space_def

|- ∀p. prob_space p ⇔ measure_space p ∧ (measure p (p_space p) = 1)

indep_def

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

probably_def

|- ∀p e. probably p e ⇔ e ∈ events p ∧ (prob p e = 1)

possibly_def

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

random_variable_def

|- ∀X p s.
     random_variable X p s ⇔
     prob_space p ∧ X ∈ measurable (p_space p,events p) s

real_random_variable_def

|- ∀X p.
     real_random_variable X p ⇔
     prob_space p ∧ (∀x. x ∈ p_space p ⇒ X x ≠ NegInf ∧ X x ≠ PosInf) ∧
     X ∈ measurable (p_space p,events p) Borel

distribution_def

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

joint_distribution_def

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

joint_distribution3_def

|- ∀p X Y Z.
     joint_distribution3 p X Y Z =
     (λa. prob p (PREIMAGE (λx. (X x,Y x,Z x)) a ∩ p_space p))

conditional_distribution_def

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

expectation_def

|- expectation = integral

conditional_expectation_def

|- ∀p X s.
     conditional_expectation p X s =
     @f.
       real_random_variable f p ∧
       ∀g.
         g ∈ s ⇒
         (integral p (λx. f x * indicator_fn g x) =
          integral p (λx. X x * indicator_fn g x))

conditional_prob_def

|- ∀p e1 e2.
     conditional_prob p e1 e2 = conditional_expectation p (indicator_fn e1) e2

rv_conditional_expectation_def

|- ∀p s X Y.
     rv_conditional_expectation p s X Y =
     conditional_expectation p X
       (IMAGE (λa. PREIMAGE Y a ∩ p_space p) (subsets s))

indep_rv_def

|- ∀p X Y s t.
     indep_rv p X Y s t ⇔
     ∀A B.
       A ∈ subsets s ∧ B ∈ subsets t ⇒ indep p (PREIMAGE X A) (PREIMAGE Y B)

uniform_distribution_def

|- ∀p X s. uniform_distribution p X s = (λa. &CARD a / &CARD (space s))

Theorems

POSITIVE_PROB

|- ∀p. positive p ⇔ (prob p ∅ = 0) ∧ ∀s. s ∈ events p ⇒ 0 ≤ prob p s

INCREASING_PROB

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

ADDITIVE_PROB

|- ∀p.
     additive p ⇔
     ∀s t.
       s ∈ events p ∧ t ∈ events p ∧ DISJOINT s t ⇒
       (prob p (s ∪ t) = prob p s + prob p t)

COUNTABLY_ADDITIVE_PROB

|- ∀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 o f sums prob p (BIGUNION (IMAGE f 𝕌(:num)))

PROB_SPACE

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

EVENTS_SIGMA_ALGEBRA

|- ∀p. prob_space p ⇒ sigma_algebra (p_space p,events p)

EVENTS_ALGEBRA

|- ∀p. prob_space p ⇒ algebra (p_space p,events p)

PROB_EMPTY

|- ∀p. prob_space p ⇒ (prob p ∅ = 0)

PROB_UNIV

|- ∀p. prob_space p ⇒ (prob p (p_space p) = 1)

PROB_SPACE_POSITIVE

|- ∀p. prob_space p ⇒ positive p

PROB_SPACE_COUNTABLY_ADDITIVE

|- ∀p. prob_space p ⇒ countably_additive p

PROB_SPACE_ADDITIVE

|- ∀p. prob_space p ⇒ additive p

PROB_SPACE_INCREASING

|- ∀p. prob_space p ⇒ increasing p

PROB_POSITIVE

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

PROB_INCREASING

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

PROB_ADDITIVE

|- ∀p s t u.
     prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧ DISJOINT s t ∧ (u = s ∪ t) ⇒
     (prob p u = prob p s + prob p t)

PROB_COUNTABLY_ADDITIVE

|- ∀p s f.
     prob_space p ∧ f ∈ (𝕌(:num) -> events p) ∧
     (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
     prob p o f sums prob p s

PROB_COMPL

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

PROB_INDEP

|- ∀p s t u. indep p s t ∧ (u = s ∩ t) ⇒ (prob p u = prob p s * prob p t)

PSPACE

|- ∀a b c. p_space (a,b,c) = a

EVENTS

|- ∀a b c. events (a,b,c) = b

PROB

|- ∀a b c. prob (a,b,c) = c

EVENTS_INTER

|- ∀p s t. prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s ∩ t ∈ events p

EVENTS_EMPTY

|- ∀p. prob_space p ⇒ ∅ ∈ events p

EVENTS_SPACE

|- ∀p. prob_space p ⇒ p_space p ∈ events p

EVENTS_UNION

|- ∀p s t. prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s ∪ t ∈ events p

INDEP_EMPTY

|- ∀p s. prob_space p ∧ s ∈ events p ⇒ indep p ∅ s

INTER_PSPACE

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

INDEP_SPACE

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

EVENTS_DIFF

|- ∀p s t. prob_space p ∧ s ∈ events p ∧ t ∈ events p ⇒ s DIFF t ∈ events p

EVENTS_COMPL

|- ∀p s. prob_space p ∧ s ∈ events p ⇒ p_space p DIFF s ∈ events p

EVENTS_COUNTABLE_UNION

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

PROB_ZERO_UNION

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

PROB_EQ_COMPL

|- ∀p s t.
     prob_space p ∧ s ∈ events p ∧ t ∈ events p ∧
     (prob p (p_space p DIFF s) = prob p (p_space p DIFF t)) ⇒
     (prob p s = prob p t)

PROB_ONE_INTER

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

EVENTS_COUNTABLE_INTER

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

ABS_PROB

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

PROB_COMPL_LE1

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

PROB_LE_1

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

PROB_EQ_BIGUNION_IMAGE

|- ∀p.
     prob_space p ∧ f ∈ (𝕌(:num) -> events p) ∧ g ∈ (𝕌(:num) -> events p) ∧
     (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ∧
     (∀m n. m ≠ n ⇒ DISJOINT (g m) (g n)) ∧
     (∀n. prob p (f n) = prob p (g n)) ⇒
     (prob p (BIGUNION (IMAGE f 𝕌(:num))) =
      prob p (BIGUNION (IMAGE g 𝕌(:num))))

PROB_FINITELY_ADDITIVE

|- ∀p s f n.
     prob_space p ∧ f ∈ (count n -> events p) ∧
     (∀a b. a < n ∧ b < n ∧ a ≠ b ⇒ DISJOINT (f a) (f b)) ∧
     (s = BIGUNION (IMAGE f (count n))) ⇒
     (sum (0,n) (prob p o f) = prob p s)

ABS_1_MINUS_PROB

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

PROB_INCREASING_UNION

|- ∀p s f.
     prob_space p ∧ f ∈ (𝕌(:num) -> events p) ∧ (∀n. f n ⊆ f (SUC n)) ∧
     (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
     prob p o f --> prob p s

PROB_SUBADDITIVE

|- ∀p s t u.
     prob_space p ∧ t ∈ events p ∧ u ∈ events p ∧ (s = t ∪ u) ⇒
     prob p s ≤ prob p t + prob p u

PROB_COUNTABLY_SUBADDITIVE

|- ∀p f.
     prob_space p ∧ IMAGE f 𝕌(:num) ⊆ events p ∧ summable (prob p o f) ⇒
     prob p (BIGUNION (IMAGE f 𝕌(:num))) ≤ suminf (prob p o f)

PROB_COUNTABLY_ZERO

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

INDEP_SYM

|- ∀p a b. prob_space p ∧ indep p a b ⇒ indep p b a

INDEP_REFL

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

PROB_REAL_SUM_IMAGE

|- ∀p s.
     prob_space p ∧ s ∈ events p ∧ (∀x. x ∈ s ⇒ {x} ∈ events p) ∧ FINITE s ⇒
     (prob p s = SIGMA (λx. prob p {x}) s)

PROB_EQUIPROBABLE_FINITE_UNIONS

|- ∀p s.
     prob_space p ∧ s ∈ events p ∧ (∀x. x ∈ s ⇒ {x} ∈ events p) ∧ FINITE s ∧
     (∀x y. x ∈ s ∧ y ∈ s ⇒ (prob p {x} = prob p {y})) ⇒
     (prob p s = &CARD s * prob p {CHOICE s})

PROB_REAL_SUM_IMAGE_FN

|- ∀p f e s.
     prob_space p ∧ e ∈ events p ∧ (∀x. x ∈ s ⇒ e ∩ f x ∈ events p) ∧
     FINITE s ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ DISJOINT (f x) (f y)) ∧
     (BIGUNION (IMAGE f s) ∩ p_space p = p_space p) ⇒
     (prob p e = SIGMA (λx. prob p (e ∩ f x)) s)

PROB_REAL_SUM_IMAGE_SPACE

|- ∀p.
     prob_space p ∧ (∀x. x ∈ p_space p ⇒ {x} ∈ events p) ∧
     FINITE (p_space p) ⇒
     (SIGMA (λx. prob p {x}) (p_space p) = 1)

PROB_DISCRETE_EVENTS

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

PROB_DISCRETE_EVENTS_COUNTABLE

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

marginal_joint_zero

|- ∀p X Y s t.
     prob_space p ∧ (events p = POW (p_space p)) ∧
     ((distribution p X s = 0) ∨ (distribution p Y t = 0)) ⇒
     (joint_distribution p X Y (s × t) = 0)

marginal_joint_zero3

|- ∀p X Y Z s t u.
     prob_space p ∧ (events p = POW (p_space p)) ∧
     ((distribution p X s = 0) ∨ (distribution p Y t = 0) ∨
      (distribution p Z u = 0)) ⇒
     (joint_distribution3 p X Y Z (s × (t × u)) = 0)

distribution_prob_space

|- ∀p X s.
     random_variable X p s ⇒ prob_space (space s,subsets s,distribution p X)

uniform_distribution_prob_space

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

distribution_partition

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

distribution_lebesgue_thm1

|- ∀X p s A.
     random_variable X p s ∧ A ∈ subsets s ⇒
     (Normal (distribution p X A) =
      integral p (indicator_fn (PREIMAGE X A ∩ p_space p)))

distribution_lebesgue_thm2

|- ∀X p s A.
     random_variable X p s ∧ A ∈ subsets s ⇒
     (Normal (distribution p X A) =
      integral (space s,subsets s,distribution p X) (indicator_fn A))

finite_expectation1

|- ∀p X.
     FINITE (p_space p) ∧ real_random_variable X p ⇒
     (expectation p X =
      SIGMA (λr. r * Normal (prob p (PREIMAGE X {r} ∩ p_space p)))
        (IMAGE X (p_space p)))

finite_expectation2

|- ∀p X.
     FINITE (IMAGE X (p_space p)) ∧ real_random_variable X p ⇒
     (expectation p X =
      SIGMA (λr. r * Normal (prob p (PREIMAGE X {r} ∩ p_space p)))
        (IMAGE X (p_space p)))

finite_expectation

|- ∀p X.
     FINITE (p_space p) ∧ real_random_variable X p ⇒
     (expectation p X =
      SIGMA (λr. r * Normal (distribution p X {r})) (IMAGE X (p_space p)))

finite_support_expectation

|- ∀p X.
     FINITE (IMAGE X (p_space p)) ∧ real_random_variable X p ⇒
     (expectation p X =
      SIGMA (λr. r * Normal (distribution p X {r})) (IMAGE X (p_space p)))

finite_marginal_product_space_POW

|- ∀p X Y.
     (POW (p_space p) = events p) ∧
     random_variable X p (IMAGE X (p_space p),POW (IMAGE X (p_space p))) ∧
     random_variable Y p (IMAGE Y (p_space p),POW (IMAGE Y (p_space p))) ∧
     FINITE (p_space p) ⇒
     measure_space
       (IMAGE X (p_space p) × IMAGE Y (p_space p),
        POW (IMAGE X (p_space p) × IMAGE Y (p_space p)),
        (λa. prob p (PREIMAGE (λx. (X x,Y x)) a ∩ p_space p)))

finite_marginal_product_space_POW2

|- ∀p s1 s2 X Y.
     (POW (p_space p) = events p) ∧ random_variable X p (s1,POW s1) ∧
     random_variable Y p (s2,POW s2) ∧ FINITE (p_space p) ∧ FINITE s1 ∧
     FINITE s2 ⇒
     measure_space (s1 × s2,POW (s1 × s2),joint_distribution p X Y)

finite_marginal_product_space_POW3

|- ∀p s1 s2 s3 X Y Z.
     (POW (p_space p) = events p) ∧ random_variable X p (s1,POW s1) ∧
     random_variable Y p (s2,POW s2) ∧ random_variable Z p (s3,POW s3) ∧
     FINITE (p_space p) ∧ FINITE s1 ∧ FINITE s2 ∧ FINITE s3 ⇒
     measure_space
       (s1 × (s2 × s3),POW (s1 × (s2 × s3)),joint_distribution3 p X Y Z)

prob_x_eq_1_imp_prob_y_eq_0

|- ∀p x.
     prob_space p ∧ {x} ∈ events p ∧ (prob p {x} = 1) ⇒
     ∀y. {y} ∈ events p ∧ y ≠ x ⇒ (prob p {y} = 0)

distribution_x_eq_1_imp_distribution_y_eq_0

|- ∀X p x.
     random_variable X p (IMAGE X (p_space p),POW (IMAGE X (p_space p))) ∧
     (distribution p X {x} = 1) ⇒
     ∀y. y ≠ x ⇒ (distribution p X {y} = 0)

joint_distribution_sym

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

joint_distribution_pos

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

joint_distribution_le_1

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

joint_distribution_le

|- ∀p X Y a b.
     prob_space p ∧ (events p = POW (p_space p)) ⇒
     joint_distribution p X Y (a × b) ≤ distribution p X a

joint_distribution_le2

|- ∀p X Y a b.
     prob_space p ∧ (events p = POW (p_space p)) ⇒
     joint_distribution p X Y (a × b) ≤ distribution p Y b

joint_conditional

|- ∀p X Y a b.
     prob_space p ∧ (events p = POW (p_space p)) ⇒
     (joint_distribution p X Y (a × b) =
      conditional_distribution p Y X b a * distribution p X a)

distribution_pos

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

conditional_distribution_pos

|- ∀p X Y a b.
     prob_space p ∧ (events p = POW (p_space p)) ⇒
     0 ≤ conditional_distribution p X Y a b

conditional_distribution_le_1

|- ∀p X Y a b.
     prob_space p ∧ (events p = POW (p_space p)) ⇒
     conditional_distribution p X Y a b ≤ 1

marginal_distribution1

|- ∀p X Y a.
     prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
     (distribution p X a =
      SIGMA (λx. joint_distribution p X Y (a × {x})) (IMAGE Y (p_space p)))

marginal_distribution2

|- ∀p X Y b.
     prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
     (distribution p Y b =
      SIGMA (λx. joint_distribution p X Y ({x} × b)) (IMAGE X (p_space p)))

joint_distribution_sums_1

|- ∀p X Y.
     prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
     (SIGMA (λ(x,y). joint_distribution p X Y {(x,y)})
        (IMAGE X (p_space p) × IMAGE Y (p_space p)) =
      1)

joint_distribution_sum_mul1

|- ∀p X Y f.
     prob_space p ∧ FINITE (p_space p) ∧ (events p = POW (p_space p)) ⇒
     (SIGMA (λ(x,y). joint_distribution p X Y {(x,y)} * f x)
        (IMAGE X (p_space p) × IMAGE Y (p_space p)) =
      SIGMA (λx. distribution p X {x} * f x) (IMAGE X (p_space p)))