author  immler 
Thu, 15 Nov 2012 10:49:58 +0100  
changeset 50087  635d73673b5e 
parent 50042  6fe18351e9dd 
child 50095  94d7dfa9f404 
permissions  rwrr 
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 

50087  12 
lemma (in product_prob_space) distr_restrict: 
13 
assumes "J \<noteq> {}" "J \<subseteq> K" "finite K" 

14 
shows "(\<Pi>\<^isub>M i\<in>J. M i) = distr (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i) (\<lambda>f. restrict f J)" (is "?P = ?D") 

15 
proof (rule measure_eqI_generator_eq) 

16 
have "finite J" using `J \<subseteq> K` `finite K` by (auto simp add: finite_subset) 

17 
interpret J: finite_product_prob_space M J proof qed fact 

18 
interpret K: finite_product_prob_space M K proof qed fact 

19 

20 
let ?J = "{Pi\<^isub>E J E  E. \<forall>i\<in>J. E i \<in> sets (M i)}" 

21 
let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)" 

22 
let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))" 

23 
show "Int_stable ?J" 

24 
by (rule Int_stable_PiE) 

25 
show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>" 

26 
using `finite J` by (auto intro!: prod_algebraI_finite) 

27 
{ fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp } 

28 
show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space) 

29 
show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J" 

30 
using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff) 

31 

32 
fix X assume "X \<in> ?J" 

33 
then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto 

34 
with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)" 

35 
by simp 

36 

37 
have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))" 

38 
using E by (simp add: J.measure_times) 

39 
also have "\<dots> = (\<Prod> i\<in>J. emeasure (M i) (if i \<in> J then E i else space (M i)))" 

40 
by simp 

41 
also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))" 

42 
using `finite K` `J \<subseteq> K` 

43 
by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1) 

44 
also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))" 

45 
using E by (simp add: K.measure_times) 

46 
also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) ` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))" 

47 
using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff split: split_if_asm) 

48 
finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X" 

49 
using X `J \<subseteq> K` apply (subst emeasure_distr) 

50 
by (auto intro!: measurable_restrict_subset simp: space_PiM) 

51 
qed 

52 

53 
lemma (in product_prob_space) emeasure_prod_emb[simp]: 

54 
assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" and X: "X \<in> sets (Pi\<^isub>M J M)" 

55 
shows "emeasure (Pi\<^isub>M L M) (prod_emb L M J X) = emeasure (Pi\<^isub>M J M) X" 

56 
by (subst distr_restrict[OF L]) 

57 
(simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X) 

58 

50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

59 
definition 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

60 
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

61 
"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

62 
{(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

63 
(\<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

64 
(\<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

65 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

66 
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

67 
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

68 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

69 
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

70 
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

71 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

72 
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

73 
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

74 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

75 
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

76 
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

77 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

78 
locale projective_family = 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

79 
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

80 
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

81 
(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

82 
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

83 
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

84 
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

85 
begin 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

86 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

87 
lemma emeasure_PiP: 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

88 
assumes "finite J" 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

89 
assumes "J \<subseteq> I" 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

90 
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

91 
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

92 
proof  
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

93 
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

94 
proof safe 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

95 
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

96 
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

97 
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

98 
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

99 
qed 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

100 
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

101 
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

102 
using assms(13) 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

103 
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

104 
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

105 
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

106 
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

107 
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

108 
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

109 
using assms by auto 
50040
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset

110 
fix K and X::"'i \<Rightarrow> 'a set" 
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset

111 
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

112 
by (auto simp: prod_emb_def) 
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset

113 
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

114 
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

115 
using assms 
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset

116 
apply (cases "J = {}") 
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset

117 
apply (simp add: prod_emb_id) 
5da32dc55cd8
assume probability spaces; allow empty index set
immler@in.tum.de
parents:
50039
diff
changeset

118 
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

119 
done 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

120 
qed 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

121 
finally show ?thesis . 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

122 
qed 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

123 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

124 
lemma PiP_finite: 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

125 
assumes "finite J" 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

126 
assumes "J \<subseteq> I" 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

127 
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

128 
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

129 
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

130 
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

131 
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

132 
show "Int_stable ?J" 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

133 
by (rule Int_stable_PiE) 
50041
afe886a04198
removed redundant/unnecessary assumptions from projective_family
immler@in.tum.de
parents:
50040
diff
changeset

134 
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

135 
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

136 
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

137 
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

138 
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

139 
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

140 
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

141 
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

142 
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

143 
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

144 
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

145 
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

146 
unfolding X using E 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

147 
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

148 
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

149 

bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

150 
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

151 
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

152 
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

153 
using assms 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

154 
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

155 

50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

156 
lemma prod_emb_injective: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

157 
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

158 
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

159 
shows "X = Y" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

160 
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

161 
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

162 
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

163 
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

164 
proof 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

165 
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

166 
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

167 
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

168 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

169 
from bchoice[OF this] 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

170 
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

171 
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

172 
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

173 
qed fact 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

174 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

175 
abbreviation 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

176 
"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

177 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

178 
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

179 
"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

180 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

181 
lemma generatorI': 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

182 
"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

183 
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

184 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

185 
lemma algebra_generator: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

186 
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

187 
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

188 
proof (intro conjI ballI) 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

189 
let ?G = generator 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

190 
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

191 
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

192 
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

193 
then show "{} \<in> ?G" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 
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

201 
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

202 
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

203 
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

204 
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

205 
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

206 
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

207 
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

208 
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

209 
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

210 
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

211 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

212 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

213 
lemma sets_PiM_generator: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

214 
"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

215 
proof cases 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

216 
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

217 
unfolding generator_def 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

218 
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

219 
next 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

220 
assume "I \<noteq> {}" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

221 
show ?thesis 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

222 
proof 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

223 
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

224 
unfolding sets_PiM 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

225 
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

226 
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

227 
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

228 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

229 
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

230 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

231 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

232 
lemma generatorI: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

233 
"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

234 
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

235 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

236 
definition 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

237 
"\<mu>G A = 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

238 
(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

239 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

240 
lemma \<mu>G_spec: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

241 
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

242 
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

243 
unfolding \<mu>G_def 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

244 
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

245 
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

246 
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

247 
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

248 
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

249 
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

250 
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

251 
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

252 
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

253 
qed (insert J, force) 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

254 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

255 
lemma \<mu>G_eq: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

256 
"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

257 
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

258 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

259 
lemma generator_Ex: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

260 
assumes *: "A \<in> generator" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

261 
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

262 
proof  
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

263 
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

264 
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

265 
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

266 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

267 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

268 
lemma generatorE: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

269 
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

270 
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

271 
proof  
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

272 
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

273 
"\<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

274 
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

275 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

276 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

277 
lemma merge_sets: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

278 
"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

279 
by simp 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

280 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

281 
lemma merge_emb: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

282 
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

283 
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

284 
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

285 
proof  
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

286 
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

287 
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

288 
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

289 
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

290 
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

291 
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

292 
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

293 
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

294 
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

295 
auto 
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 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

298 
lemma positive_\<mu>G: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

299 
assumes "I \<noteq> {}" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

300 
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

301 
proof  
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

302 
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

303 
show ?thesis 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

304 
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

305 
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

306 
have "X = {}" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

307 
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

308 
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

309 
next 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

310 
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

311 
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

312 
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

313 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

314 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

315 

6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

316 
lemma additive_\<mu>G: 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

317 
assumes "I \<noteq> {}" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

318 
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

319 
proof  
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

320 
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

321 
show ?thesis 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

322 
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

323 
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

324 
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

325 
assume "A \<inter> B = {}" 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

326 
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

327 
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

328 
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

329 
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

330 
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

331 
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

332 
done 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

333 
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

334 
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

335 
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

336 
by simp 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

337 
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

338 
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

339 
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

340 
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

341 
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

342 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

343 
qed 
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

344 

50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

345 
end 
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

346 

50087  347 
sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M 
348 
proof 

349 
fix J::"'i set" assume "finite J" 

350 
interpret f: finite_product_prob_space M J proof qed fact 

351 
show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp 

352 
show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and> 

353 
(\<Union>i. A i) = space (Pi\<^isub>M J M) \<and> 

354 
(\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`] 

355 
by (auto simp add: sigma_finite_measure_def) 

356 
show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1) 

357 
qed simp_all 

358 

359 
lemma (in product_prob_space) PiP_PiM_finite[simp]: 

360 
assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "PiP J M (\<lambda>J. PiM J M) = PiM J M" 

361 
using assms by (simp add: PiP_finite) 

362 

50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

363 
end 