author  hoelzl 
Tue, 17 May 2011 11:47:36 +0200  
changeset 42861  16375b493b64 
child 42981  fe7f5a26e4c6 
permissions  rwrr 
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

1 
(* Title: HOL/Probability/Independent_Family.thy 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

2 
Author: Johannes Hölzl, TU München 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

3 
*) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

4 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

5 
header {* Independent families of events, event sets, and random variables *} 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

6 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

7 
theory Independent_Family 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

8 
imports Probability_Measure 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

9 
begin 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

10 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

11 
definition (in prob_space) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

12 
"indep_events A I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

13 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

14 
definition (in prob_space) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

15 
"indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

16 
(\<forall>A\<in>(\<Pi> j\<in>J. F j). prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

17 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

18 
definition (in prob_space) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

19 
"indep_sets2 A B \<longleftrightarrow> indep_sets (bool_case A B) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

20 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

21 
definition (in prob_space) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

22 
"indep_rv M' X I \<longleftrightarrow> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

23 
(\<forall>i\<in>I. random_variable (M' i) (X i)) \<and> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

24 
indep_sets (\<lambda>i. sigma_sets (space M) { X i ` A \<inter> space M  A. A \<in> sets (M' i)}) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

25 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

26 
lemma (in prob_space) indep_sets_finite_index_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

27 
"indep_sets F I \<longleftrightarrow> (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

28 
proof (intro iffI allI impI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

29 
assume *: "\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> indep_sets F J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

30 
show "indep_sets F I" unfolding indep_sets_def 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

31 
proof (intro conjI ballI allI impI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

32 
fix i assume "i \<in> I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

33 
with *[THEN spec, of "{i}"] show "F i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

34 
by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

35 
qed (insert *, auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

36 
qed (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

37 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

38 
lemma (in prob_space) indep_sets_mono_index: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

39 
"J \<subseteq> I \<Longrightarrow> indep_sets F I \<Longrightarrow> indep_sets F J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

40 
unfolding indep_sets_def by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

41 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

42 
lemma (in prob_space) indep_sets_mono_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

43 
assumes indep: "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

44 
assumes mono: "\<And>i. i\<in>I \<Longrightarrow> G i \<subseteq> F i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

45 
shows "indep_sets G I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

46 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

47 
have "(\<forall>i\<in>I. F i \<subseteq> events) \<Longrightarrow> (\<forall>i\<in>I. G i \<subseteq> events)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

48 
using mono by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

49 
moreover have "\<And>A J. J \<subseteq> I \<Longrightarrow> A \<in> (\<Pi> j\<in>J. G j) \<Longrightarrow> A \<in> (\<Pi> j\<in>J. F j)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

50 
using mono by (auto simp: Pi_iff) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

51 
ultimately show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

52 
using indep by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

53 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

54 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

55 
lemma (in prob_space) indep_setsI: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

56 
assumes "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

57 
and "\<And>A J. J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> (\<forall>j\<in>J. A j \<in> F j) \<Longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

58 
shows "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

59 
using assms unfolding indep_sets_def by (auto simp: Pi_iff) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

60 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

61 
lemma (in prob_space) indep_setsD: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

62 
assumes "indep_sets F I" and "J \<subseteq> I" "J \<noteq> {}" "finite J" "\<forall>j\<in>J. A j \<in> F j" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

63 
shows "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

64 
using assms unfolding indep_sets_def by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

65 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

66 
lemma dynkin_systemI': 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

67 
assumes 1: "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

68 
assumes empty: "{} \<in> sets M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

69 
assumes Diff: "\<And> A. A \<in> sets M \<Longrightarrow> space M  A \<in> sets M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

70 
assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> sets M 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

71 
\<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

72 
shows "dynkin_system M" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

73 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

74 
from Diff[OF empty] have "space M \<in> sets M" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

75 
from 1 this Diff 2 show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

76 
by (intro dynkin_systemI) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

77 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

78 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

79 
lemma (in prob_space) indep_sets_dynkin: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

80 
assumes indep: "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

81 
shows "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

82 
(is "indep_sets ?F I") 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

83 
proof (subst indep_sets_finite_index_sets, intro allI impI ballI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

84 
fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

85 
with indep have "indep_sets F J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

86 
by (subst (asm) indep_sets_finite_index_sets) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

87 
{ fix J K assume "indep_sets F K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

88 
let "?G S i" = "if i \<in> S then ?F i else F i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

89 
assume "finite J" "J \<subseteq> K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

90 
then have "indep_sets (?G J) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

91 
proof induct 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

92 
case (insert j J) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

93 
moreover def G \<equiv> "?G J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

94 
ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

95 
by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

96 
let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

97 
{ fix X assume X: "X \<in> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

98 
assume indep: "\<And>J A. J \<noteq> {} \<Longrightarrow> J \<subseteq> K \<Longrightarrow> finite J \<Longrightarrow> j \<notin> J \<Longrightarrow> (\<forall>i\<in>J. A i \<in> G i) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

99 
\<Longrightarrow> prob ((\<Inter>i\<in>J. A i) \<inter> X) = prob X * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

100 
have "indep_sets (G(j := {X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

101 
proof (rule indep_setsI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

102 
fix i assume "i \<in> K" then show "(G(j:={X})) i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

103 
using G X by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

104 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

105 
fix A J assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "\<forall>i\<in>J. A i \<in> (G(j := {X})) i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

106 
show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

107 
proof cases 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

108 
assume "j \<in> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

109 
with J have "A j = X" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

110 
show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

111 
proof cases 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

112 
assume "J = {j}" then show ?thesis by simp 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

113 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

114 
assume "J \<noteq> {j}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

115 
have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J{j}. A i) \<inter> X)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

116 
using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

117 
also have "\<dots> = prob X * (\<Prod>i\<in>J{j}. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

118 
proof (rule indep) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

119 
show "J  {j} \<noteq> {}" "J  {j} \<subseteq> K" "finite (J  {j})" "j \<notin> J  {j}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

120 
using J `J \<noteq> {j}` `j \<in> J` by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

121 
show "\<forall>i\<in>J  {j}. A i \<in> G i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

122 
using J by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

123 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

124 
also have "\<dots> = prob (A j) * (\<Prod>i\<in>J{j}. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

125 
using `A j = X` by simp 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

126 
also have "\<dots> = (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

127 
unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob (A i)"] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

128 
using `j \<in> J` by (simp add: insert_absorb) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

129 
finally show ?thesis . 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

130 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

131 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

132 
assume "j \<notin> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

133 
with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

134 
with J show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

135 
by (intro indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

136 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

137 
qed } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

138 
note indep_sets_insert = this 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

139 
have "dynkin_system \<lparr> space = space M, sets = ?D \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

140 
proof (rule dynkin_systemI', simp_all, safe) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

141 
show "indep_sets (G(j := {{}})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

142 
by (rule indep_sets_insert) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

143 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

144 
fix X assume X: "X \<in> events" and G': "indep_sets (G(j := {X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

145 
show "indep_sets (G(j := {space M  X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

146 
proof (rule indep_sets_insert) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

147 
fix J A assume J: "J \<noteq> {}" "J \<subseteq> K" "finite J" "j \<notin> J" and A: "\<forall>i\<in>J. A i \<in> G i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

148 
then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

149 
using G by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

150 
have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

151 
prob ((\<Inter>j\<in>J. A j)  (\<Inter>i\<in>insert j J. (A(j := X)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

152 
using A_sets sets_into_space X `J \<noteq> {}` 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

153 
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

154 
also have "\<dots> = prob (\<Inter>j\<in>J. A j)  prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

155 
using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

156 
by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

157 
finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

158 
prob (\<Inter>j\<in>J. A j)  prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" . 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

159 
moreover { 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

160 
have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

161 
using J A `finite J` by (intro indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

162 
then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

163 
using prob_space by simp } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

164 
moreover { 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

165 
have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

166 
using J A `j \<in> K` by (intro indep_setsD[OF G']) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

167 
then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

168 
using `finite J` `j \<notin> J` by (auto intro!: setprod_cong) } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

169 
ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = (prob (space M)  prob X) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

170 
by (simp add: field_simps) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

171 
also have "\<dots> = prob (space M  X) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

172 
using X A by (simp add: finite_measure_compl) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

173 
finally show "prob ((\<Inter>j\<in>J. A j) \<inter> (space M  X)) = prob (space M  X) * (\<Prod>i\<in>J. prob (A i))" . 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

174 
qed (insert X, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

175 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

176 
fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F" and "range F \<subseteq> ?D" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

177 
then have F: "\<And>i. F i \<in> events" "\<And>i. indep_sets (G(j:={F i})) K" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

178 
show "indep_sets (G(j := {\<Union>k. F k})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

179 
proof (rule indep_sets_insert) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

180 
fix J A assume J: "j \<notin> J" "J \<noteq> {}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> G i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

181 
then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

182 
using G by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

183 
have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

184 
using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

185 
moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

186 
proof (rule finite_measure_UNION) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

187 
show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

188 
using disj by (rule disjoint_family_on_bisimulation) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

189 
show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

190 
using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

191 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

192 
moreover { fix k 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

193 
from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

194 
by (subst indep_setsD[OF F(2)]) (auto intro!: setprod_cong split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

195 
also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

196 
using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

197 
finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

198 
ultimately have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

199 
by simp 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

200 
moreover 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

201 
have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i\<in>J. A i))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

202 
using disj F(1) by (intro finite_measure_UNION sums_mult2) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

203 
then have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * (\<Prod>i\<in>J. prob (A i)))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

204 
using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

205 
ultimately 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

206 
show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

207 
by (auto dest!: sums_unique) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

208 
qed (insert F, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

209 
qed (insert sets_into_space, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

210 
then have mono: "sets (dynkin \<lparr>space = space M, sets = G j\<rparr>) \<subseteq> 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

211 
sets \<lparr>space = space M, sets = {E \<in> events. indep_sets (G(j := {E})) K}\<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

212 
proof (rule dynkin_system.dynkin_subset, simp_all, safe) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

213 
fix X assume "X \<in> G j" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

214 
then show "X \<in> events" using G `j \<in> K` by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

215 
from `indep_sets G K` 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

216 
show "indep_sets (G(j := {X})) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

217 
by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

218 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

219 
have "indep_sets (G(j:=?D)) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

220 
proof (rule indep_setsI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

221 
fix i assume "i \<in> K" then show "(G(j := ?D)) i \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

222 
using G(2) by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

223 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

224 
fix A J assume J: "J\<noteq>{}" "J \<subseteq> K" "finite J" and A: "\<forall>i\<in>J. A i \<in> (G(j := ?D)) i" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

225 
show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

226 
proof cases 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

227 
assume "j \<in> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

228 
with A have indep: "indep_sets (G(j := {A j})) K" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

229 
from J A show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

230 
by (intro indep_setsD[OF indep]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

231 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

232 
assume "j \<notin> J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

233 
with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

234 
with J show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

235 
by (intro indep_setsD[OF G(1)]) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

236 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

237 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

238 
then have "indep_sets (G(j:=sets (dynkin \<lparr>space = space M, sets = G j\<rparr>))) K" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

239 
by (rule indep_sets_mono_sets) (insert mono, auto) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

240 
then show ?case 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

241 
by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

242 
qed (insert `indep_sets F K`, simp) } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

243 
from this[OF `indep_sets F J` `finite J` subset_refl] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

244 
show "indep_sets (\<lambda>i. sets (dynkin \<lparr> space = space M, sets = F i \<rparr>)) J" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

245 
by (rule indep_sets_mono_sets) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

246 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

247 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

248 
lemma (in prob_space) indep_sets_sigma: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

249 
assumes indep: "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

250 
assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

251 
shows "indep_sets (\<lambda>i. sets (sigma \<lparr> space = space M, sets = F i \<rparr>)) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

252 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

253 
from indep_sets_dynkin[OF indep] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

254 
show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

255 
proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

256 
fix i assume "i \<in> I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

257 
with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

258 
with sets_into_space show "F i \<subseteq> Pow (space M)" by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

259 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

260 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

261 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

262 
lemma (in prob_space) indep_sets_sigma_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

263 
assumes "indep_sets F I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

264 
assumes "\<And>i. i \<in> I \<Longrightarrow> Int_stable \<lparr> space = space M, sets = F i \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

265 
shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

266 
using indep_sets_sigma[OF assms] by (simp add: sets_sigma) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

267 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

268 
lemma (in prob_space) indep_sets2_eq: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

269 
"indep_sets2 A B \<longleftrightarrow> A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

270 
unfolding indep_sets2_def 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

271 
proof (intro iffI ballI conjI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

272 
assume indep: "indep_sets (bool_case A B) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

273 
{ fix a b assume "a \<in> A" "b \<in> B" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

274 
with indep_setsD[OF indep, of UNIV "bool_case a b"] 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

275 
show "prob (a \<inter> b) = prob a * prob b" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

276 
unfolding UNIV_bool by (simp add: ac_simps) } 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

277 
from indep show "A \<subseteq> events" "B \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

278 
unfolding indep_sets_def UNIV_bool by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

279 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

280 
assume *: "A \<subseteq> events \<and> B \<subseteq> events \<and> (\<forall>a\<in>A. \<forall>b\<in>B. prob (a \<inter> b) = prob a * prob b)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

281 
show "indep_sets (bool_case A B) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

282 
proof (rule indep_setsI) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

283 
fix i show "(case i of True \<Rightarrow> A  False \<Rightarrow> B) \<subseteq> events" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

284 
using * by (auto split: bool.split) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

285 
next 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

286 
fix J X assume "J \<noteq> {}" "J \<subseteq> UNIV" and X: "\<forall>j\<in>J. X j \<in> (case j of True \<Rightarrow> A  False \<Rightarrow> B)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

287 
then have "J = {True} \<or> J = {False} \<or> J = {True,False}" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

288 
by (auto simp: UNIV_bool) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

289 
then show "prob (\<Inter>j\<in>J. X j) = (\<Prod>j\<in>J. prob (X j))" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

290 
using X * by auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

291 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

292 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

293 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

294 
lemma (in prob_space) indep_sets2_sigma_sets: 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

295 
assumes "indep_sets2 A B" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

296 
assumes A: "Int_stable \<lparr> space = space M, sets = A \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

297 
assumes B: "Int_stable \<lparr> space = space M, sets = B \<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

298 
shows "indep_sets2 (sigma_sets (space M) A) (sigma_sets (space M) B)" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

299 
proof  
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

300 
have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A  False \<Rightarrow> B)) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

301 
proof (rule indep_sets_sigma_sets) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

302 
show "indep_sets (bool_case A B) UNIV" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

303 
by (rule `indep_sets2 A B`[unfolded indep_sets2_def]) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

304 
fix i show "Int_stable \<lparr>space = space M, sets = case i of True \<Rightarrow> A  False \<Rightarrow> B\<rparr>" 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

305 
using A B by (cases i) auto 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

306 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

307 
then show ?thesis 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

308 
unfolding indep_sets2_def 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

309 
by (rule indep_sets_mono_sets) (auto split: bool.split) 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

310 
qed 
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

311 

16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
diff
changeset

312 
end 