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_families	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> ((α -> bool) -> bool) reln
indep_function	:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real) -> (α -> β # α) -> bool
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

indep_families_def

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

indep_function_def

⊢ ∀p.
      indep_function p =
      {f |
      indep_families p (IMAGE (PREIMAGE (FST ∘ f)) 𝕌(:β -> bool))
        (IMAGE (PREIMAGE (SND ∘ f)) (events p))}

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 ∘ 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 ∘ 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 ∘ 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 ∘ 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 ∘ f) ⇒
      prob p (BIGUNION (IMAGE f 𝕌(:num))) ≤ suminf (prob p ∘ 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))