author | immler@in.tum.de |
Fri, 09 Nov 2012 14:31:26 +0100 | |
changeset 50042 | 6fe18351e9dd |
parent 50041 | afe886a04198 |
child 50087 | 635d73673b5e |
permissions | -rw-r--r-- |
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
1 |
(* Title: HOL/Probability/Projective_Family.thy |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
2 |
Author: Fabian Immler, TU München |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
3 |
Author: Johannes Hölzl, TU München |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
4 |
*) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
5 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
6 |
header {*Projective Family*} |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
7 |
|
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
8 |
theory Projective_Family |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
9 |
imports Finite_Product_Measure Probability_Measure |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
10 |
begin |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
11 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
12 |
definition |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
13 |
PiP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
14 |
"PiP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i)) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
15 |
{(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
16 |
(\<lambda>(J, X). prod_emb I M J (\<Pi>\<^isub>E j\<in>J. X j)) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
17 |
(\<lambda>(J, X). emeasure (P J) (Pi\<^isub>E J X))" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
18 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
19 |
lemma space_PiP[simp]: "space (PiP I M P) = space (PiM I M)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
20 |
by (auto simp add: PiP_def space_PiM prod_emb_def intro!: space_extend_measure) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
21 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
22 |
lemma sets_PiP[simp]: "sets (PiP I M P) = sets (PiM I M)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
23 |
by (auto simp add: PiP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
24 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
25 |
lemma measurable_PiP1[simp]: "measurable (PiP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
26 |
unfolding measurable_def by auto |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
27 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
28 |
lemma measurable_PiP2[simp]: "measurable M' (PiP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
29 |
unfolding measurable_def by auto |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
30 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
31 |
locale projective_family = |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
32 |
fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
33 |
assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow> |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
34 |
(P H) (prod_emb H M J X) = (P J) X" |
50040
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
35 |
assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)" |
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
36 |
assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
37 |
assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
38 |
begin |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
39 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
40 |
lemma emeasure_PiP: |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
41 |
assumes "finite J" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
42 |
assumes "J \<subseteq> I" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
43 |
assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
44 |
shows "emeasure (PiP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
45 |
proof - |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
46 |
have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
47 |
proof safe |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
48 |
fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
49 |
hence "x j \<in> restrict A J j" by (auto simp: Pi_def) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
50 |
also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
51 |
finally show "x j \<in> space (M j)" . |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
52 |
qed |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
53 |
hence "emeasure (PiP J M P) (Pi\<^isub>E J A) = |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
54 |
emeasure (PiP J M P) (prod_emb J M J (Pi\<^isub>E J A))" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
55 |
using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
56 |
also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)" |
50040
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
57 |
proof (rule emeasure_extend_measure_Pair[OF PiP_def]) |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
58 |
show "positive (sets (PiP J M P)) (P J)" unfolding positive_def by auto |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
59 |
show "countably_additive (sets (PiP J M P)) (P J)" unfolding countably_additive_def |
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
60 |
by (auto simp: suminf_emeasure proj_sets[OF `finite J`]) |
50040
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
61 |
show "(J \<noteq> {} \<or> J = {}) \<and> finite J \<and> J \<subseteq> J \<and> A \<in> (\<Pi> j\<in>J. sets (M j))" |
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
62 |
using assms by auto |
50040
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
63 |
fix K and X::"'i \<Rightarrow> 'a set" |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
64 |
show "prod_emb J M K (Pi\<^isub>E K X) \<in> Pow (\<Pi>\<^isub>E i\<in>J. space (M i))" |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
65 |
by (auto simp: prod_emb_def) |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
66 |
assume JX: "(K \<noteq> {} \<or> J = {}) \<and> finite K \<and> K \<subseteq> J \<and> X \<in> (\<Pi> j\<in>K. sets (M j))" |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
67 |
thus "emeasure (P J) (prod_emb J M K (Pi\<^isub>E K X)) = emeasure (P K) (Pi\<^isub>E K X)" |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
68 |
using assms |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
69 |
apply (cases "J = {}") |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
70 |
apply (simp add: prod_emb_id) |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
71 |
apply (fastforce simp add: intro!: projective sets_PiM_I_finite) |
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset
|
72 |
done |
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
73 |
qed |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
74 |
finally show ?thesis . |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
75 |
qed |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
76 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
77 |
lemma PiP_finite: |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
78 |
assumes "finite J" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
79 |
assumes "J \<subseteq> I" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
80 |
shows "PiP J M P = P J" (is "?P = _") |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
81 |
proof (rule measure_eqI_generator_eq) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
82 |
let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
83 |
let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
84 |
let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
85 |
show "Int_stable ?J" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
86 |
by (rule Int_stable_PiE) |
50041
afe886a04198
removed redundant/unnecessary assumptions from projective_family
immler@in.tum.de
parents:
50040
diff
changeset
|
87 |
interpret prob_space "P J" using prob_space `finite J` by simp |
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
88 |
show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
89 |
show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
90 |
show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
91 |
using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
92 |
fix X assume "X \<in> ?J" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
93 |
then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
94 |
with `finite J` have "X \<in> sets (PiP J M P)" by simp |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
95 |
have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
96 |
using E sets_into_space |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
97 |
by (auto intro!: prod_emb_PiE_same_index) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
98 |
show "emeasure (PiP J M P) X = emeasure (P J) X" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
99 |
unfolding X using E |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
100 |
by (intro emeasure_PiP assms) simp |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
101 |
qed (insert `finite J`, auto intro!: prod_algebraI_finite) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
102 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
103 |
lemma emeasure_fun_emb[simp]: |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
104 |
assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
105 |
shows "emeasure (PiP L M P) (prod_emb L M J X) = emeasure (PiP J M P) X" |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
106 |
using assms |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
107 |
by (subst PiP_finite) (auto simp: PiP_finite finite_subset projective) |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
108 |
|
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
109 |
lemma prod_emb_injective: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
110 |
assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
111 |
assumes "prod_emb L M J X = prod_emb L M J Y" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
112 |
shows "X = Y" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
113 |
proof (rule injective_vimage_restrict) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
114 |
show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
115 |
using sets[THEN sets_into_space] by (auto simp: space_PiM) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
116 |
have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
117 |
proof |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
118 |
fix i assume "i \<in> L" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
119 |
interpret prob_space "P {i}" using prob_space by simp |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
120 |
from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
121 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
122 |
from bchoice[OF this] |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
123 |
show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
124 |
show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
125 |
using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
126 |
qed fact |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
127 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
128 |
abbreviation |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
129 |
"emb L K X \<equiv> prod_emb L M K X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
130 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
131 |
definition generator :: "('i \<Rightarrow> 'a) set set" where |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
132 |
"generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
133 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
134 |
lemma generatorI': |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
135 |
"J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> emb I J X \<in> generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
136 |
unfolding generator_def by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
137 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
138 |
lemma algebra_generator: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
139 |
assumes "I \<noteq> {}" shows "algebra (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" (is "algebra ?\<Omega> ?G") |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
140 |
unfolding algebra_def algebra_axioms_def ring_of_sets_iff |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
141 |
proof (intro conjI ballI) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
142 |
let ?G = generator |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
143 |
show "?G \<subseteq> Pow ?\<Omega>" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
144 |
by (auto simp: generator_def prod_emb_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
145 |
from `I \<noteq> {}` obtain i where "i \<in> I" by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
146 |
then show "{} \<in> ?G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
147 |
by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"] |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
148 |
simp: sigma_sets.Empty generator_def prod_emb_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
149 |
from `i \<in> I` show "?\<Omega> \<in> ?G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
150 |
by (auto intro!: exI[of _ "{i}"] image_eqI[where x="Pi\<^isub>E {i} (\<lambda>i. space (M i))"] |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
151 |
simp: generator_def prod_emb_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
152 |
fix A assume "A \<in> ?G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
153 |
then obtain JA XA where XA: "JA \<noteq> {}" "finite JA" "JA \<subseteq> I" "XA \<in> sets (Pi\<^isub>M JA M)" and A: "A = emb I JA XA" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
154 |
by (auto simp: generator_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
155 |
fix B assume "B \<in> ?G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
156 |
then obtain JB XB where XB: "JB \<noteq> {}" "finite JB" "JB \<subseteq> I" "XB \<in> sets (Pi\<^isub>M JB M)" and B: "B = emb I JB XB" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
157 |
by (auto simp: generator_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
158 |
let ?RA = "emb (JA \<union> JB) JA XA" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
159 |
let ?RB = "emb (JA \<union> JB) JB XB" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
160 |
have *: "A - B = emb I (JA \<union> JB) (?RA - ?RB)" "A \<union> B = emb I (JA \<union> JB) (?RA \<union> ?RB)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
161 |
using XA A XB B by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
162 |
show "A - B \<in> ?G" "A \<union> B \<in> ?G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
163 |
unfolding * using XA XB by (safe intro!: generatorI') auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
164 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
165 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
166 |
lemma sets_PiM_generator: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
167 |
"sets (PiM I M) = sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
168 |
proof cases |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
169 |
assume "I = {}" then show ?thesis |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
170 |
unfolding generator_def |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
171 |
by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
172 |
next |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
173 |
assume "I \<noteq> {}" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
174 |
show ?thesis |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
175 |
proof |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
176 |
show "sets (Pi\<^isub>M I M) \<subseteq> sigma_sets (\<Pi>\<^isub>E i\<in>I. space (M i)) generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
177 |
unfolding sets_PiM |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
178 |
proof (safe intro!: sigma_sets_subseteq) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
179 |
fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
180 |
by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
181 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
182 |
qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
183 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
184 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
185 |
lemma generatorI: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
186 |
"J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
187 |
unfolding generator_def by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
188 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
189 |
definition |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
190 |
"\<mu>G A = |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
191 |
(THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (PiP J M P) X))" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
192 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
193 |
lemma \<mu>G_spec: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
194 |
assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
195 |
shows "\<mu>G A = emeasure (PiP J M P) X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
196 |
unfolding \<mu>G_def |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
197 |
proof (intro the_equality allI impI ballI) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
198 |
fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
199 |
have "emeasure (PiP K M P) Y = emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) K Y)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
200 |
using K J by simp |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
201 |
also have "emb (K \<union> J) K Y = emb (K \<union> J) J X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
202 |
using K J by (simp add: prod_emb_injective[of "K \<union> J" I]) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
203 |
also have "emeasure (PiP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (PiP J M P) X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
204 |
using K J by simp |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
205 |
finally show "emeasure (PiP J M P) X = emeasure (PiP K M P) Y" .. |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
206 |
qed (insert J, force) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
207 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
208 |
lemma \<mu>G_eq: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
209 |
"J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (PiP J M P) X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
210 |
by (intro \<mu>G_spec) auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
211 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
212 |
lemma generator_Ex: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
213 |
assumes *: "A \<in> generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
214 |
shows "\<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A = emb I J X \<and> \<mu>G A = emeasure (PiP J M P) X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
215 |
proof - |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
216 |
from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
217 |
unfolding generator_def by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
218 |
with \<mu>G_spec[OF this] show ?thesis by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
219 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
220 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
221 |
lemma generatorE: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
222 |
assumes A: "A \<in> generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
223 |
obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (PiP J M P) X" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
224 |
proof - |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
225 |
from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
226 |
"\<mu>G A = emeasure (PiP J M P) X" by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
227 |
then show thesis by (intro that) auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
228 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
229 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
230 |
lemma merge_sets: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
231 |
"J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
232 |
by simp |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
233 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
234 |
lemma merge_emb: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
235 |
assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
236 |
shows "((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
237 |
emb I (K - J) ((\<lambda>x. merge J (K - J) (y, x)) -` emb (J \<union> K) K X \<inter> space (Pi\<^isub>M (K - J) M))" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
238 |
proof - |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
239 |
have [simp]: "\<And>x J K L. merge J K (y, restrict x L) = merge J (K \<inter> L) (y, x)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
240 |
by (auto simp: restrict_def merge_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
241 |
have [simp]: "\<And>x J K L. restrict (merge J K (y, x)) L = merge (J \<inter> L) (K \<inter> L) (y, x)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
242 |
by (auto simp: restrict_def merge_def) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
243 |
have [simp]: "(I - J) \<inter> K = K - J" using `K \<subseteq> I` `J \<subseteq> I` by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
244 |
have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
245 |
have [simp]: "(K - J) \<inter> K = K - J" by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
246 |
from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
247 |
by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
248 |
auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
249 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
250 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
251 |
lemma positive_\<mu>G: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
252 |
assumes "I \<noteq> {}" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
253 |
shows "positive generator \<mu>G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
254 |
proof - |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
255 |
interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
256 |
show ?thesis |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
257 |
proof (intro positive_def[THEN iffD2] conjI ballI) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
258 |
from generatorE[OF G.empty_sets] guess J X . note this[simp] |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
259 |
have "X = {}" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
260 |
by (rule prod_emb_injective[of J I]) simp_all |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
261 |
then show "\<mu>G {} = 0" by simp |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
262 |
next |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
263 |
fix A assume "A \<in> generator" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
264 |
from generatorE[OF this] guess J X . note this[simp] |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
265 |
show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
266 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
267 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
268 |
|
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
269 |
lemma additive_\<mu>G: |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
270 |
assumes "I \<noteq> {}" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
271 |
shows "additive generator \<mu>G" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
272 |
proof - |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
273 |
interpret G!: algebra "\<Pi>\<^isub>E i\<in>I. space (M i)" generator by (rule algebra_generator) fact |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
274 |
show ?thesis |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
275 |
proof (intro additive_def[THEN iffD2] ballI impI) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
276 |
fix A assume "A \<in> generator" with generatorE guess J X . note J = this |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
277 |
fix B assume "B \<in> generator" with generatorE guess K Y . note K = this |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
278 |
assume "A \<inter> B = {}" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
279 |
have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
280 |
using J K by auto |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
281 |
have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
282 |
apply (rule prod_emb_injective[of "J \<union> K" I]) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
283 |
apply (insert `A \<inter> B = {}` JK J K) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
284 |
apply (simp_all add: Int prod_emb_Int) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
285 |
done |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
286 |
have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
287 |
using J K by simp_all |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
288 |
then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
289 |
by simp |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
290 |
also have "\<dots> = emeasure (PiP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
291 |
using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
292 |
also have "\<dots> = \<mu>G A + \<mu>G B" |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
293 |
using J K JK_disj by (simp add: plus_emeasure[symmetric]) |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
294 |
finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" . |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
295 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
296 |
qed |
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset
|
297 |
|
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
298 |
end |
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
299 |
|
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset
|
300 |
end |