author  hoelzl 
Mon, 19 Nov 2012 16:09:11 +0100  
changeset 50124  4161c834c2fd 
parent 50123  69b35a75caf3 
child 50244  de72bbe42190 
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))" 

50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50101
diff
changeset

47 
using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm) 
50087  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 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

60 
limP :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i set \<Rightarrow> ('i \<Rightarrow> 'a) measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

61 
"limP I M P = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i)) 
50039
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 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

66 
abbreviation "lim\<^isub>P \<equiv> limP" 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

67 

94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

68 
lemma space_limP[simp]: "space (limP I M P) = space (PiM I M)" 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

69 
by (auto simp add: limP_def space_PiM prod_emb_def intro!: space_extend_measure) 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

70 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

71 
lemma sets_limP[simp]: "sets (limP I M P) = sets (PiM I M)" 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

72 
by (auto simp add: limP_def sets_PiM prod_algebra_def prod_emb_def intro!: sets_extend_measure) 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

73 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

74 
lemma measurable_limP1[simp]: "measurable (limP I M P) M' = measurable (\<Pi>\<^isub>M i\<in>I. M i) M'" 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

75 
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

76 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

77 
lemma measurable_limP2[simp]: "measurable M' (limP I M P) = measurable M' (\<Pi>\<^isub>M i\<in>I. M i)" 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

78 
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

79 

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

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

81 
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

82 
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

83 
(P H) (prod_emb H M J X) = (P J) X" 
50101
a3bede207a04
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
hoelzl
parents:
50095
diff
changeset

84 
assumes proj_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

85 
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

86 
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

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

88 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

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

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

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

92 
assumes A: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> sets (M i)" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

93 
shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)" 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

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

95 
have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50101
diff
changeset

96 
using sets_into_space[OF A] by (auto simp: PiE_iff) blast 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

97 
hence "emeasure (limP J M P) (Pi\<^isub>E J A) = 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

98 
emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))" 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50101
diff
changeset

99 
using assms(13) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def) 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

100 
also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

101 
proof (rule emeasure_extend_measure_Pair[OF limP_def]) 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

102 
show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

103 
show "countably_additive (sets (limP 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

104 
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

105 
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

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

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

108 
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

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

110 
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

111 
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

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

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

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

115 
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

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

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

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

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

120 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

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

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

123 
assumes "J \<subseteq> I" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

124 
shows "limP J M P = P J" (is "?P = _") 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

125 
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

126 
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

127 
let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))" 
50101
a3bede207a04
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
hoelzl
parents:
50095
diff
changeset

128 
interpret prob_space "P J" using proj_prob_space `finite J` by simp 
50124  129 
show "emeasure ?P (\<Pi>\<^isub>E k\<in>J. space (M k)) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP) 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

130 
show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J" 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

131 
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

132 
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

133 
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 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

134 
with `finite J` have "X \<in> sets (limP J M P)" by simp 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

135 
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

136 
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

137 
by (auto intro!: prod_emb_PiE_same_index) 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

138 
show "emeasure (limP J M P) X = emeasure (P J) X" 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

139 
unfolding X using E 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

140 
by (intro emeasure_limP assms) simp 
50124  141 
qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE) 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

142 

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

143 
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

144 
assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

145 
shows "emeasure (limP L M P) (prod_emb L M J X) = emeasure (limP J M P) X" 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

146 
using assms 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

147 
by (subst limP_finite) (auto simp: limP_finite finite_subset projective) 
50039
bfd5198cbe40
added projective_family; generalized generator in product_prob_space to projective_family
immler@in.tum.de
parents:
diff
changeset

148 

50124  149 
abbreviation 
150 
"emb L K X \<equiv> prod_emb L M K X" 

151 

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

152 
lemma prod_emb_injective: 
50124  153 
assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)" 
154 
assumes "emb L J X = emb L J Y" 

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

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

156 
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

157 
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

158 
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

159 
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

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

161 
fix i assume "i \<in> L" 
50101
a3bede207a04
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
hoelzl
parents:
50095
diff
changeset

162 
interpret prob_space "P {i}" using proj_prob_space by simp 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

163 
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

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

165 
from bchoice[OF this] 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50101
diff
changeset

166 
show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def) 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

167 
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

168 
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

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

170 

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

171 
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

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

173 

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

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

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

176 
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

177 

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

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

179 
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

180 
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

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

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

183 
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

184 
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

185 
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

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

187 
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

188 
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

189 
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

190 
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

191 
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 
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

193 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 
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

201 
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

202 
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

203 
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

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

205 

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

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

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

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

209 
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

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

211 
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

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

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

214 
show ?thesis 
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 
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

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

218 
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

219 
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

220 
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

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

222 
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

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

224 

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

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

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

227 
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

228 

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

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

230 
"\<mu>G A = 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

231 
(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 (limP J M P) X))" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

232 

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

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

234 
assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

235 
shows "\<mu>G A = emeasure (limP J M P) X" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

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

237 
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

238 
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)" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

239 
have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

240 
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

241 
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

242 
using K J by (simp add: prod_emb_injective[of "K \<union> J" I]) 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

243 
also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

244 
using K J by simp 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

245 
finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" .. 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

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

247 

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

248 
lemma \<mu>G_eq: 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

249 
"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 (limP J M P) X" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

250 
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

251 

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

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

253 
assumes *: "A \<in> generator" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

254 
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 (limP J M P) X" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

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

256 
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

257 
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

258 
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

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

260 

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

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

262 
assumes A: "A \<in> generator" 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

263 
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 (limP J M P) X" 
50124  264 
using generator_Ex[OF A] by atomize_elim auto 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

265 

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

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

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

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

269 

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

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

271 
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

272 
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

273 
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

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

275 
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

276 
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

277 
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

278 
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

279 
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

280 
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

281 
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

282 
from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis 
50123
69b35a75caf3
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
hoelzl
parents:
50101
diff
changeset

283 
by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM) 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

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

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

286 

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

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

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

289 
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

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

291 
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

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

293 
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

294 
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

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

296 
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

297 
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

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

299 
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

300 
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

301 
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

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

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

304 

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

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

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

307 
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

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

309 
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

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

311 
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

312 
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

313 
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

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

315 
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

316 
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

317 
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

318 
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

319 
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

320 
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

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

322 
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

323 
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

324 
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

325 
by simp 
50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

326 
also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)" 
50042
6fe18351e9dd
moved lemmas into projective_family; added header for theory Projective_Family
immler@in.tum.de
parents:
50041
diff
changeset

327 
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

328 
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

329 
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

330 
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

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

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

333 

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

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

335 

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

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

339 
interpret f: finite_product_prob_space M J proof qed fact 

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

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

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

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

344 
by (auto simp add: sigma_finite_measure_def) 

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

346 
qed simp_all 

347 

50095
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

348 
lemma (in product_prob_space) limP_PiM_finite[simp]: 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

349 
assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "limP J M (\<lambda>J. PiM J M) = PiM J M" 
94d7dfa9f404
renamed to more appropriate lim_P for projective limit
immler
parents:
50087
diff
changeset

350 
using assms by (simp add: limP_finite) 
50087  351 

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

352 
end 