equal
deleted
inserted
replaced
5 header {* Independent families of events, event sets, and random variables *} |
5 header {* Independent families of events, event sets, and random variables *} |
6 |
6 |
7 theory Independent_Family |
7 theory Independent_Family |
8 imports Probability_Measure Infinite_Product_Measure |
8 imports Probability_Measure Infinite_Product_Measure |
9 begin |
9 begin |
10 |
|
11 lemma INT_decseq_offset: |
|
12 assumes "decseq F" |
|
13 shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)" |
|
14 proof safe |
|
15 fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)" |
|
16 show "x \<in> F i" |
|
17 proof cases |
|
18 from x have "x \<in> F n" by auto |
|
19 also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i" |
|
20 unfolding decseq_def by simp |
|
21 finally show ?thesis . |
|
22 qed (insert x, simp) |
|
23 qed auto |
|
24 |
10 |
25 definition (in prob_space) |
11 definition (in prob_space) |
26 "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> |
12 "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and> |
27 (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))" |
13 (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))" |
28 |
14 |