author  hoelzl 
Tue, 19 Jul 2011 14:36:12 +0200  
changeset 43920  cedb5cb948fd 
parent 42984  43864e7475df 
child 44890  22f665a2e91c 
permissions  rwrr 
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

1 
(* Title: HOL/Probability/Binary_Product_Measure.thy 
42067  2 
Author: Johannes Hölzl, TU München 
3 
*) 

4 

42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

5 
header {*Binary product measures*} 
42067  6 

42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

7 
theory Binary_Product_Measure 
38656  8 
imports Lebesgue_Integration 
35833  9 
begin 
10 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42146
diff
changeset

11 
lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42146
diff
changeset

12 
by auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42146
diff
changeset

13 

40859  14 
lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" 
15 
by auto 

16 

17 
lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x ` (A \<times> B) = (if x \<in> A then B else {})" 

18 
by auto 

19 

20 
lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) ` (A \<times> B) = (if y \<in> B then A else {})" 

21 
by auto 

22 

23 
lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))" 

24 
by (cases x) simp 

25 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

26 
lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))" 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

27 
by (auto simp: fun_eq_iff) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

28 

40859  29 
section "Binary products" 
30 

31 
definition 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

32 
"pair_measure_generator A B = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

33 
\<lparr> space = space A \<times> space B, 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

34 
sets = {a \<times> b  a b. a \<in> sets A \<and> b \<in> sets B}, 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

35 
measure = \<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A \<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

36 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

37 
definition pair_measure (infixr "\<Otimes>\<^isub>M" 80) where 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

38 
"A \<Otimes>\<^isub>M B = sigma (pair_measure_generator A B)" 
40859  39 

40 
locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

41 
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

42 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

43 
abbreviation (in pair_sigma_algebra) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

44 
"E \<equiv> pair_measure_generator M1 M2" 
40859  45 

46 
abbreviation (in pair_sigma_algebra) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

47 
"P \<equiv> M1 \<Otimes>\<^isub>M M2" 
40859  48 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

49 
lemma sigma_algebra_pair_measure: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

50 
"sets M1 \<subseteq> Pow (space M1) \<Longrightarrow> sets M2 \<subseteq> Pow (space M2) \<Longrightarrow> sigma_algebra (pair_measure M1 M2)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

51 
by (force simp: pair_measure_def pair_measure_generator_def intro!: sigma_algebra_sigma) 
40859  52 

53 
sublocale pair_sigma_algebra \<subseteq> sigma_algebra P 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

54 
using M1.space_closed M2.space_closed 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

55 
by (rule sigma_algebra_pair_measure) 
40859  56 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

57 
lemma pair_measure_generatorI[intro, simp]: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

58 
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (pair_measure_generator A B)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

59 
by (auto simp add: pair_measure_generator_def) 
40859  60 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

61 
lemma pair_measureI[intro, simp]: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

62 
"x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

63 
by (auto simp add: pair_measure_def) 
40859  64 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

65 
lemma space_pair_measure: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

66 
"space (A \<Otimes>\<^isub>M B) = space A \<times> space B" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

67 
by (simp add: pair_measure_def pair_measure_generator_def) 
41095  68 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

69 
lemma sets_pair_measure_generator: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

70 
"sets (pair_measure_generator N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

71 
unfolding pair_measure_generator_def by auto 
41095  72 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

73 
lemma pair_measure_generator_sets_into_space: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

74 
assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

75 
shows "sets (pair_measure_generator M N) \<subseteq> Pow (space (pair_measure_generator M N))" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

76 
using assms by (auto simp: pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

77 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

78 
lemma pair_measure_generator_Int_snd: 
40859  79 
assumes "sets S1 \<subseteq> Pow (space S1)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

80 
shows "sets (pair_measure_generator S1 (algebra.restricted_space S2 A)) = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

81 
sets (algebra.restricted_space (pair_measure_generator S1 S2) (space S1 \<times> A))" 
40859  82 
(is "?L = ?R") 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

83 
apply (auto simp: pair_measure_generator_def image_iff) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

84 
using assms 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

85 
apply (rule_tac x="a \<times> xa" in exI) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

86 
apply force 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

87 
using assms 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

88 
apply (rule_tac x="a" in exI) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

89 
apply (rule_tac x="b \<inter> A" in exI) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

90 
apply auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

91 
done 
40859  92 

93 
lemma (in pair_sigma_algebra) 

94 
shows measurable_fst[intro!, simp]: 

95 
"fst \<in> measurable P M1" (is ?fst) 

96 
and measurable_snd[intro!, simp]: 

97 
"snd \<in> measurable P M2" (is ?snd) 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

98 
proof  
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

99 
{ fix X assume "X \<in> sets M1" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

100 
then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. fst ` X \<inter> space M1 \<times> space M2 = X1 \<times> X2" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

101 
apply  apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"]) 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

102 
using M1.sets_into_space by force+ } 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

103 
moreover 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

104 
{ fix X assume "X \<in> sets M2" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

105 
then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. snd ` X \<inter> space M1 \<times> space M2 = X1 \<times> X2" 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

106 
apply  apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X]) 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

107 
using M2.sets_into_space by force+ } 
40859  108 
ultimately have "?fst \<and> ?snd" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

109 
by (fastsimp simp: measurable_def sets_sigma space_pair_measure 
40859  110 
intro!: sigma_sets.Basic) 
111 
then show ?fst ?snd by auto 

112 
qed 

113 

41095  114 
lemma (in pair_sigma_algebra) measurable_pair_iff: 
40859  115 
assumes "sigma_algebra M" 
116 
shows "f \<in> measurable M P \<longleftrightarrow> 

117 
(fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2" 

118 
proof  

119 
interpret M: sigma_algebra M by fact 

120 
from assms show ?thesis 

121 
proof (safe intro!: measurable_comp[where b=P]) 

122 
assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

123 
show "f \<in> measurable M P" unfolding pair_measure_def 
40859  124 
proof (rule M.measurable_sigma) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

125 
show "sets (pair_measure_generator M1 M2) \<subseteq> Pow (space E)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

126 
unfolding pair_measure_generator_def using M1.sets_into_space M2.sets_into_space by auto 
40859  127 
show "f \<in> space M \<rightarrow> space E" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

128 
using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma pair_measure_generator_def) 
40859  129 
fix A assume "A \<in> sets E" 
130 
then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

131 
unfolding pair_measure_generator_def by auto 
40859  132 
moreover have "(fst \<circ> f) ` B \<inter> space M \<in> sets M" 
133 
using f `B \<in> sets M1` unfolding measurable_def by auto 

134 
moreover have "(snd \<circ> f) ` C \<inter> space M \<in> sets M" 

135 
using s `C \<in> sets M2` unfolding measurable_def by auto 

136 
moreover have "f ` A \<inter> space M = ((fst \<circ> f) ` B \<inter> space M) \<inter> ((snd \<circ> f) ` C \<inter> space M)" 

137 
unfolding `A = B \<times> C` by (auto simp: vimage_Times) 

138 
ultimately show "f ` A \<inter> space M \<in> sets M" by auto 

139 
qed 

140 
qed 

141 
qed 

142 

41095  143 
lemma (in pair_sigma_algebra) measurable_pair: 
40859  144 
assumes "sigma_algebra M" 
41095  145 
assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2" 
40859  146 
shows "f \<in> measurable M P" 
41095  147 
unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp 
40859  148 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

149 
lemma pair_measure_generatorE: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

150 
assumes "X \<in> sets (pair_measure_generator M1 M2)" 
40859  151 
obtains A B where "X = A \<times> B" "A \<in> sets M1" "B \<in> sets M2" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

152 
using assms unfolding pair_measure_generator_def by auto 
40859  153 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

154 
lemma (in pair_sigma_algebra) pair_measure_generator_swap: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

155 
"(\<lambda>X. (\<lambda>(x,y). (y,x)) ` X \<inter> space M2 \<times> space M1) ` sets E = sets (pair_measure_generator M2 M1)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

156 
proof (safe elim!: pair_measure_generatorE) 
40859  157 
fix A B assume "A \<in> sets M1" "B \<in> sets M2" 
158 
moreover then have "(\<lambda>(x, y). (y, x)) ` (A \<times> B) \<inter> space M2 \<times> space M1 = B \<times> A" 

159 
using M1.sets_into_space M2.sets_into_space by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

160 
ultimately show "(\<lambda>(x, y). (y, x)) ` (A \<times> B) \<inter> space M2 \<times> space M1 \<in> sets (pair_measure_generator M2 M1)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

161 
by (auto intro: pair_measure_generatorI) 
40859  162 
next 
163 
fix A B assume "A \<in> sets M1" "B \<in> sets M2" 

164 
then show "B \<times> A \<in> (\<lambda>X. (\<lambda>(x, y). (y, x)) ` X \<inter> space M2 \<times> space M1) ` sets E" 

165 
using M1.sets_into_space M2.sets_into_space 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

166 
by (auto intro!: image_eqI[where x="A \<times> B"] pair_measure_generatorI) 
40859  167 
qed 
168 

169 
lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap: 

170 
assumes Q: "Q \<in> sets P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

171 
shows "(\<lambda>(x,y). (y, x)) ` Q \<in> sets (M2 \<Otimes>\<^isub>M M1)" (is "_ \<in> sets ?Q") 
40859  172 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

173 
let "?f Q" = "(\<lambda>(x,y). (y, x)) ` Q \<inter> space M2 \<times> space M1" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

174 
have *: "(\<lambda>(x,y). (y, x)) ` Q = ?f Q" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

175 
using sets_into_space[OF Q] by (auto simp: space_pair_measure) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

176 
have "sets (M2 \<Otimes>\<^isub>M M1) = sets (sigma (pair_measure_generator M2 M1))" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

177 
unfolding pair_measure_def .. 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

178 
also have "\<dots> = sigma_sets (space M2 \<times> space M1) (?f ` sets E)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

179 
unfolding sigma_def pair_measure_generator_swap[symmetric] 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

180 
by (simp add: pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

181 
also have "\<dots> = ?f ` sigma_sets (space M1 \<times> space M2) (sets E)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

182 
using M1.sets_into_space M2.sets_into_space 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

183 
by (intro sigma_sets_vimage) (auto simp: pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

184 
also have "\<dots> = ?f ` sets P" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

185 
unfolding pair_measure_def pair_measure_generator_def sigma_def by simp 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

186 
finally show ?thesis 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

187 
using Q by (subst *) auto 
40859  188 
qed 
189 

190 
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

191 
shows "(\<lambda>(x,y). (y, x)) \<in> measurable P (M2 \<Otimes>\<^isub>M M1)" 
40859  192 
(is "?f \<in> measurable ?P ?Q") 
193 
unfolding measurable_def 

194 
proof (intro CollectI conjI Pi_I ballI) 

195 
fix x assume "x \<in> space ?P" then show "(case x of (x, y) \<Rightarrow> (y, x)) \<in> space ?Q" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

196 
unfolding pair_measure_generator_def pair_measure_def by auto 
40859  197 
next 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

198 
fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
40859  199 
interpret Q: pair_sigma_algebra M2 M1 by default 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

200 
with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`] 
40859  201 
show "?f ` A \<inter> space ?P \<in> sets ?P" by simp 
202 
qed 

203 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

204 
lemma (in pair_sigma_algebra) measurable_cut_fst[simp,intro]: 
40859  205 
assumes "Q \<in> sets P" shows "Pair x ` Q \<in> sets M2" 
206 
proof  

207 
let ?Q' = "{Q. Q \<subseteq> space P \<and> Pair x ` Q \<in> sets M2}" 

208 
let ?Q = "\<lparr> space = space P, sets = ?Q' \<rparr>" 

209 
interpret Q: sigma_algebra ?Q 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

210 
proof qed (auto simp: vimage_UN vimage_Diff space_pair_measure) 
40859  211 
have "sets E \<subseteq> sets ?Q" 
212 
using M1.sets_into_space M2.sets_into_space 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

213 
by (auto simp: pair_measure_generator_def space_pair_measure) 
40859  214 
then have "sets P \<subseteq> sets ?Q" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

215 
apply (subst pair_measure_def, intro Q.sets_sigma_subset) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

216 
by (simp add: pair_measure_def) 
40859  217 
with assms show ?thesis by auto 
218 
qed 

219 

220 
lemma (in pair_sigma_algebra) measurable_cut_snd: 

221 
assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) ` Q \<in> sets M1" (is "?cut Q \<in> sets M1") 

222 
proof  

223 
interpret Q: pair_sigma_algebra M2 M1 by default 

224 
with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

225 
show ?thesis by (simp add: vimage_compose[symmetric] comp_def) 
40859  226 
qed 
227 

228 
lemma (in pair_sigma_algebra) measurable_pair_image_snd: 

229 
assumes m: "f \<in> measurable P M" and "x \<in> space M1" 

230 
shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M" 

231 
unfolding measurable_def 

232 
proof (intro CollectI conjI Pi_I ballI) 

233 
fix y assume "y \<in> space M2" with `f \<in> measurable P M` `x \<in> space M1` 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

234 
show "f (x, y) \<in> space M" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

235 
unfolding measurable_def pair_measure_generator_def pair_measure_def by auto 
40859  236 
next 
237 
fix A assume "A \<in> sets M" 

238 
then have "Pair x ` (f ` A \<inter> space P) \<in> sets M2" (is "?C \<in> _") 

239 
using `f \<in> measurable P M` 

240 
by (intro measurable_cut_fst) (auto simp: measurable_def) 

241 
also have "?C = (\<lambda>y. f (x, y)) ` A \<inter> space M2" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

242 
using `x \<in> space M1` by (auto simp: pair_measure_generator_def pair_measure_def) 
40859  243 
finally show "(\<lambda>y. f (x, y)) ` A \<inter> space M2 \<in> sets M2" . 
244 
qed 

245 

246 
lemma (in pair_sigma_algebra) measurable_pair_image_fst: 

247 
assumes m: "f \<in> measurable P M" and "y \<in> space M2" 

248 
shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M" 

249 
proof  

250 
interpret Q: pair_sigma_algebra M2 M1 by default 

251 
from Q.measurable_pair_image_snd[OF measurable_comp `y \<in> space M2`, 

252 
OF Q.pair_sigma_algebra_swap_measurable m] 

253 
show ?thesis by simp 

254 
qed 

255 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

256 
lemma (in pair_sigma_algebra) Int_stable_pair_measure_generator: "Int_stable E" 
40859  257 
unfolding Int_stable_def 
258 
proof (intro ballI) 

259 
fix A B assume "A \<in> sets E" "B \<in> sets E" 

260 
then obtain A1 A2 B1 B2 where "A = A1 \<times> A2" "B = B1 \<times> B2" 

261 
"A1 \<in> sets M1" "A2 \<in> sets M2" "B1 \<in> sets M1" "B2 \<in> sets M2" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

262 
unfolding pair_measure_generator_def by auto 
40859  263 
then show "A \<inter> B \<in> sets E" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

264 
by (auto simp add: times_Int_times pair_measure_generator_def) 
40859  265 
qed 
266 

267 
lemma finite_measure_cut_measurable: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

268 
fixes M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

269 
assumes "sigma_finite_measure M1" "finite_measure M2" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

270 
assumes "Q \<in> sets (M1 \<Otimes>\<^isub>M M2)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

271 
shows "(\<lambda>x. measure M2 (Pair x ` Q)) \<in> borel_measurable M1" 
40859  272 
(is "?s Q \<in> _") 
273 
proof  

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

274 
interpret M1: sigma_finite_measure M1 by fact 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

275 
interpret M2: finite_measure M2 by fact 
40859  276 
interpret pair_sigma_algebra M1 M2 by default 
277 
have [intro]: "sigma_algebra M1" by fact 

278 
have [intro]: "sigma_algebra M2" by fact 

279 
let ?D = "\<lparr> space = space P, sets = {A\<in>sets P. ?s A \<in> borel_measurable M1} \<rparr>" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

280 
note space_pair_measure[simp] 
40859  281 
interpret dynkin_system ?D 
282 
proof (intro dynkin_systemI) 

283 
fix A assume "A \<in> sets ?D" then show "A \<subseteq> space ?D" 

284 
using sets_into_space by simp 

285 
next 

286 
from top show "space ?D \<in> sets ?D" 

287 
by (auto simp add: if_distrib intro!: M1.measurable_If) 

288 
next 

289 
fix A assume "A \<in> sets ?D" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

290 
with sets_into_space have "\<And>x. measure M2 (Pair x ` (space M1 \<times> space M2  A)) = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

291 
(if x \<in> space M1 then measure M2 (space M2)  ?s A x else 0)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

292 
by (auto intro!: M2.measure_compl simp: vimage_Diff) 
40859  293 
with `A \<in> sets ?D` top show "space ?D  A \<in> sets ?D" 
43920  294 
by (auto intro!: Diff M1.measurable_If M1.borel_measurable_ereal_diff) 
40859  295 
next 
296 
fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> sets ?D" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

297 
moreover then have "\<And>x. measure M2 (\<Union>i. Pair x ` F i) = (\<Sum>i. ?s (F i) x)" 
40859  298 
by (intro M2.measure_countably_additive[symmetric]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

299 
(auto simp: disjoint_family_on_def) 
40859  300 
ultimately show "(\<Union>i. F i) \<in> sets ?D" 
301 
by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf) 

302 
qed 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

303 
have "sets P = sets ?D" apply (subst pair_measure_def) 
40859  304 
proof (intro dynkin_lemma) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

305 
show "Int_stable E" by (rule Int_stable_pair_measure_generator) 
40859  306 
from M1.sets_into_space have "\<And>A. A \<in> sets M1 \<Longrightarrow> {x \<in> space M1. x \<in> A} = A" 
307 
by auto 

308 
then show "sets E \<subseteq> sets ?D" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

309 
by (auto simp: pair_measure_generator_def sets_sigma if_distrib 
40859  310 
intro: sigma_sets.Basic intro!: M1.measurable_If) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

311 
qed (auto simp: pair_measure_def) 
40859  312 
with `Q \<in> sets P` have "Q \<in> sets ?D" by simp 
313 
then show "?s Q \<in> borel_measurable M1" by simp 

314 
qed 

315 

316 
subsection {* Binary products of $\sigma$finite measure spaces *} 

317 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

318 
locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

319 
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
40859  320 

321 
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2 

322 
by default 

323 

324 
lemma (in pair_sigma_finite) measure_cut_measurable_fst: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

325 
assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x ` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _") 
40859  326 
proof  
327 
have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+ 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

328 
have M1: "sigma_finite_measure M1" by default 
40859  329 
from M2.disjoint_sigma_finite guess F .. note F = this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

330 
then have F_sets: "\<And>i. F i \<in> sets M2" by auto 
40859  331 
let "?C x i" = "F i \<inter> Pair x ` Q" 
332 
{ fix i 

333 
let ?R = "M2.restricted_space (F i)" 

334 
have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i" 

335 
using F M2.sets_into_space by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

336 
let ?R2 = "M2.restricted_space (F i)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

337 
have "(\<lambda>x. measure ?R2 (Pair x ` (space M1 \<times> space ?R2 \<inter> Q))) \<in> borel_measurable M1" 
40859  338 
proof (intro finite_measure_cut_measurable[OF M1]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

339 
show "finite_measure ?R2" 
40859  340 
using F by (intro M2.restricted_to_finite_measure) auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

341 
have "(space M1 \<times> space ?R2) \<inter> Q \<in> (op \<inter> (space M1 \<times> F i)) ` sets P" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

342 
using `Q \<in> sets P` by (auto simp: image_iff) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

343 
also have "\<dots> = sigma_sets (space M1 \<times> F i) ((op \<inter> (space M1 \<times> F i)) ` sets E)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

344 
unfolding pair_measure_def pair_measure_generator_def sigma_def 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

345 
using `F i \<in> sets M2` M2.sets_into_space 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

346 
by (auto intro!: sigma_sets_Int sigma_sets.Basic) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

347 
also have "\<dots> \<subseteq> sets (M1 \<Otimes>\<^isub>M ?R2)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

348 
using M1.sets_into_space 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

349 
apply (auto simp: times_Int_times pair_measure_def pair_measure_generator_def sigma_def 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

350 
intro!: sigma_sets_subseteq) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

351 
apply (rule_tac x="a" in exI) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

352 
apply (rule_tac x="b \<inter> F i" in exI) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

353 
by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

354 
finally show "(space M1 \<times> space ?R2) \<inter> Q \<in> sets (M1 \<Otimes>\<^isub>M ?R2)" . 
40859  355 
qed 
356 
moreover have "\<And>x. Pair x ` (space M1 \<times> F i \<inter> Q) = ?C x i" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

357 
using `Q \<in> sets P` sets_into_space by (auto simp: space_pair_measure) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

358 
ultimately have "(\<lambda>x. measure M2 (?C x i)) \<in> borel_measurable M1" 
40859  359 
by simp } 
360 
moreover 

361 
{ fix x 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

362 
have "(\<Sum>i. measure M2 (?C x i)) = measure M2 (\<Union>i. ?C x i)" 
40859  363 
proof (intro M2.measure_countably_additive) 
364 
show "range (?C x) \<subseteq> sets M2" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

365 
using F `Q \<in> sets P` by (auto intro!: M2.Int) 
40859  366 
have "disjoint_family F" using F by auto 
367 
show "disjoint_family (?C x)" 

368 
by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto 

369 
qed 

370 
also have "(\<Union>i. ?C x i) = Pair x ` Q" 

371 
using F sets_into_space `Q \<in> sets P` 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

372 
by (auto simp: space_pair_measure) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

373 
finally have "measure M2 (Pair x ` Q) = (\<Sum>i. measure M2 (?C x i))" 
40859  374 
by simp } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

375 
ultimately show ?thesis using `Q \<in> sets P` F_sets 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

376 
by (auto intro!: M1.borel_measurable_psuminf M2.Int) 
40859  377 
qed 
378 

379 
lemma (in pair_sigma_finite) measure_cut_measurable_snd: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

380 
assumes "Q \<in> sets P" shows "(\<lambda>y. M1.\<mu> ((\<lambda>x. (x, y)) ` Q)) \<in> borel_measurable M2" 
40859  381 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

382 
interpret Q: pair_sigma_finite M2 M1 by default 
40859  383 
note sets_pair_sigma_algebra_swap[OF assms] 
384 
from Q.measure_cut_measurable_fst[OF this] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

385 
show ?thesis by (simp add: vimage_compose[symmetric] comp_def) 
40859  386 
qed 
387 

388 
lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

389 
assumes "f \<in> measurable P M" shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (M2 \<Otimes>\<^isub>M M1) M" 
40859  390 
proof  
391 
interpret Q: pair_sigma_algebra M2 M1 by default 

392 
have *: "(\<lambda>(x,y). f (y, x)) = f \<circ> (\<lambda>(x,y). (y, x))" by (simp add: fun_eq_iff) 

393 
show ?thesis 

394 
using Q.pair_sigma_algebra_swap_measurable assms 

395 
unfolding * by (rule measurable_comp) 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

396 
qed 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

397 

40859  398 
lemma (in pair_sigma_finite) pair_measure_alt: 
399 
assumes "A \<in> sets P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

400 
shows "measure (M1 \<Otimes>\<^isub>M M2) A = (\<integral>\<^isup>+ x. measure M2 (Pair x ` A) \<partial>M1)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

401 
apply (simp add: pair_measure_def pair_measure_generator_def) 
40859  402 
proof (rule M1.positive_integral_cong) 
403 
fix x assume "x \<in> space M1" 

43920  404 
have *: "\<And>y. indicator A (x, y) = (indicator (Pair x ` A) y :: ereal)" 
40859  405 
unfolding indicator_def by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

406 
show "(\<integral>\<^isup>+ y. indicator A (x, y) \<partial>M2) = measure M2 (Pair x ` A)" 
40859  407 
unfolding * 
408 
apply (subst M2.positive_integral_indicator) 

409 
apply (rule measurable_cut_fst[OF assms]) 

410 
by simp 

411 
qed 

412 

413 
lemma (in pair_sigma_finite) pair_measure_times: 

414 
assumes A: "A \<in> sets M1" and "B \<in> sets M2" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

415 
shows "measure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = M1.\<mu> A * measure M2 B" 
40859  416 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

417 
have "measure (M1 \<Otimes>\<^isub>M M2) (A \<times> B) = (\<integral>\<^isup>+ x. measure M2 B * indicator A x \<partial>M1)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

418 
using assms by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt) 
40859  419 
with assms show ?thesis 
420 
by (simp add: M1.positive_integral_cmult_indicator ac_simps) 

421 
qed 

422 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

423 
lemma (in measure_space) measure_not_negative[simp,intro]: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

424 
assumes A: "A \<in> sets M" shows "\<mu> A \<noteq>  \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

425 
using positive_measure[OF A] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

426 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

427 
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_measure_generator: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

428 
"\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets E \<and> incseq F \<and> (\<Union>i. F i) = space E \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

429 
(\<forall>i. measure (M1 \<Otimes>\<^isub>M M2) (F i) \<noteq> \<infinity>)" 
40859  430 
proof  
431 
obtain F1 :: "nat \<Rightarrow> 'a set" and F2 :: "nat \<Rightarrow> 'b set" where 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

432 
F1: "range F1 \<subseteq> sets M1" "incseq F1" "(\<Union>i. F1 i) = space M1" "\<And>i. M1.\<mu> (F1 i) \<noteq> \<infinity>" and 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

433 
F2: "range F2 \<subseteq> sets M2" "incseq F2" "(\<Union>i. F2 i) = space M2" "\<And>i. M2.\<mu> (F2 i) \<noteq> \<infinity>" 
40859  434 
using M1.sigma_finite_up M2.sigma_finite_up by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

435 
then have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto 
40859  436 
let ?F = "\<lambda>i. F1 i \<times> F2 i" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

437 
show ?thesis unfolding space_pair_measure 
40859  438 
proof (intro exI[of _ ?F] conjI allI) 
439 
show "range ?F \<subseteq> sets E" using F1 F2 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

440 
by (fastsimp intro!: pair_measure_generatorI) 
40859  441 
next 
442 
have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)" 

443 
proof (intro subsetI) 

444 
fix x assume "x \<in> space M1 \<times> space M2" 

445 
then obtain i j where "fst x \<in> F1 i" "snd x \<in> F2 j" 

446 
by (auto simp: space) 

447 
then have "fst x \<in> F1 (max i j)" "snd x \<in> F2 (max j i)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

448 
using `incseq F1` `incseq F2` unfolding incseq_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

449 
by (force split: split_max)+ 
40859  450 
then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)" 
451 
by (intro SigmaI) (auto simp add: min_max.sup_commute) 

452 
then show "x \<in> (\<Union>i. ?F i)" by auto 

453 
qed 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

454 
then show "(\<Union>i. ?F i) = space E" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

455 
using space by (auto simp: space pair_measure_generator_def) 
40859  456 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

457 
fix i show "incseq (\<lambda>i. F1 i \<times> F2 i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

458 
using `incseq F1` `incseq F2` unfolding incseq_Suc_iff by auto 
40859  459 
next 
460 
fix i 

461 
from F1 F2 have "F1 i \<in> sets M1" "F2 i \<in> sets M2" by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

462 
with F1 F2 M1.positive_measure[OF this(1)] M2.positive_measure[OF this(2)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

463 
show "measure P (F1 i \<times> F2 i) \<noteq> \<infinity>" 
40859  464 
by (simp add: pair_measure_times) 
465 
qed 

466 
qed 

467 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

468 
sublocale pair_sigma_finite \<subseteq> sigma_finite_measure P 
40859  469 
proof 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

470 
show "positive P (measure P)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

471 
unfolding pair_measure_def pair_measure_generator_def sigma_def positive_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

472 
by (auto intro: M1.positive_integral_positive M2.positive_integral_positive) 
40859  473 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

474 
show "countably_additive P (measure P)" 
40859  475 
unfolding countably_additive_def 
476 
proof (intro allI impI) 

477 
fix F :: "nat \<Rightarrow> ('a \<times> 'b) set" 

478 
assume F: "range F \<subseteq> sets P" "disjoint_family F" 

479 
from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

480 
moreover from F have "\<And>i. (\<lambda>x. measure M2 (Pair x ` F i)) \<in> borel_measurable M1" 
40859  481 
by (intro measure_cut_measurable_fst) auto 
482 
moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x ` F i)" 

483 
by (intro disjoint_family_on_bisimulation[OF F(2)]) auto 

484 
moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> range (\<lambda>i. Pair x ` F i) \<subseteq> sets M2" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

485 
using F by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

486 
ultimately show "(\<Sum>n. measure P (F n)) = measure P (\<Union>i. F i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

487 
by (simp add: pair_measure_alt vimage_UN M1.positive_integral_suminf[symmetric] 
40859  488 
M2.measure_countably_additive 
489 
cong: M1.positive_integral_cong) 

490 
qed 

491 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

492 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

493 
show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets P \<and> (\<Union>i. F i) = space P \<and> (\<forall>i. measure P (F i) \<noteq> \<infinity>)" 
40859  494 
proof (rule exI[of _ F], intro conjI) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

495 
show "range F \<subseteq> sets P" using F by (auto simp: pair_measure_def) 
40859  496 
show "(\<Union>i. F i) = space P" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

497 
using F by (auto simp: pair_measure_def pair_measure_generator_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

498 
show "\<forall>i. measure P (F i) \<noteq> \<infinity>" using F by auto 
40859  499 
qed 
500 
qed 

39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

501 

41661  502 
lemma (in pair_sigma_algebra) sets_swap: 
503 
assumes "A \<in> sets P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

504 
shows "(\<lambda>(x, y). (y, x)) ` A \<inter> space (M2 \<Otimes>\<^isub>M M1) \<in> sets (M2 \<Otimes>\<^isub>M M1)" 
41661  505 
(is "_ ` A \<inter> space ?Q \<in> sets ?Q") 
506 
proof  

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

507 
have *: "(\<lambda>(x, y). (y, x)) ` A \<inter> space ?Q = (\<lambda>(x, y). (y, x)) ` A" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

508 
using `A \<in> sets P` sets_into_space by (auto simp: space_pair_measure) 
41661  509 
show ?thesis 
510 
unfolding * using assms by (rule sets_pair_sigma_algebra_swap) 

511 
qed 

512 

40859  513 
lemma (in pair_sigma_finite) pair_measure_alt2: 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

514 
assumes A: "A \<in> sets P" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

515 
shows "\<mu> A = (\<integral>\<^isup>+y. M1.\<mu> ((\<lambda>x. (x, y)) ` A) \<partial>M2)" 
40859  516 
(is "_ = ?\<nu> A") 
517 
proof  

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

518 
interpret Q: pair_sigma_finite M2 M1 by default 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

519 
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

520 
have [simp]: "\<And>m. \<lparr> space = space E, sets = sets (sigma E), measure = m \<rparr> = P\<lparr> measure := m \<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

521 
unfolding pair_measure_def by simp 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

522 

a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

523 
have "\<mu> A = Q.\<mu> ((\<lambda>(y, x). (x, y)) ` A \<inter> space Q.P)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

524 
proof (rule measure_unique_Int_stable_vimage[OF Int_stable_pair_measure_generator]) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

525 
show "measure_space P" "measure_space Q.P" by default 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

526 
show "(\<lambda>(y, x). (x, y)) \<in> measurable Q.P P" by (rule Q.pair_sigma_algebra_swap_measurable) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

527 
show "sets (sigma E) = sets P" "space E = space P" "A \<in> sets (sigma E)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

528 
using assms unfolding pair_measure_def by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

529 
show "range F \<subseteq> sets E" "incseq F" "(\<Union>i. F i) = space E" "\<And>i. \<mu> (F i) \<noteq> \<infinity>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

530 
using F `A \<in> sets P` by (auto simp: pair_measure_def) 
40859  531 
fix X assume "X \<in> sets E" 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

532 
then obtain A B where X[simp]: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

533 
unfolding pair_measure_def pair_measure_generator_def by auto 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

534 
then have "(\<lambda>(y, x). (x, y)) ` X \<inter> space Q.P = B \<times> A" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

535 
using M1.sets_into_space M2.sets_into_space by (auto simp: space_pair_measure) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

536 
then show "\<mu> X = Q.\<mu> ((\<lambda>(y, x). (x, y)) ` X \<inter> space Q.P)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

537 
using AB by (simp add: pair_measure_times Q.pair_measure_times ac_simps) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

538 
qed 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

539 
then show ?thesis 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

540 
using sets_into_space[OF A] Q.pair_measure_alt[OF sets_swap[OF A]] 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

541 
by (auto simp add: Q.pair_measure_alt space_pair_measure 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41705
diff
changeset

542 
intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

543 
qed 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

544 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

545 
lemma pair_sigma_algebra_sigma: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

546 
assumes 1: "incseq S1" "(\<Union>i. S1 i) = space E1" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

547 
assumes 2: "decseq S2" "(\<Union>i. S2 i) = space E2" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

548 
shows "sets (sigma (pair_measure_generator (sigma E1) (sigma E2))) = sets (sigma (pair_measure_generator E1 E2))" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

549 
(is "sets ?S = sets ?E") 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

550 
proof  
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

551 
interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

552 
interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

553 
have P: "sets (pair_measure_generator E1 E2) \<subseteq> Pow (space E1 \<times> space E2)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

554 
using E1 E2 by (auto simp add: pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

555 
interpret E: sigma_algebra ?E unfolding pair_measure_generator_def 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

556 
using E1 E2 by (intro sigma_algebra_sigma) auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

557 
{ fix A assume "A \<in> sets E1" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

558 
then have "fst ` A \<inter> space ?E = A \<times> (\<Union>i. S2 i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

559 
using E1 2 unfolding pair_measure_generator_def by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

560 
also have "\<dots> = (\<Union>i. A \<times> S2 i)" by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

561 
also have "\<dots> \<in> sets ?E" unfolding pair_measure_generator_def sets_sigma 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

562 
using 2 `A \<in> sets E1` 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

563 
by (intro sigma_sets.Union) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

564 
(force simp: image_subset_iff intro!: sigma_sets.Basic) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

565 
finally have "fst ` A \<inter> space ?E \<in> sets ?E" . } 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

566 
moreover 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

567 
{ fix B assume "B \<in> sets E2" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

568 
then have "snd ` B \<inter> space ?E = (\<Union>i. S1 i) \<times> B" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

569 
using E2 1 unfolding pair_measure_generator_def by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

570 
also have "\<dots> = (\<Union>i. S1 i \<times> B)" by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

571 
also have "\<dots> \<in> sets ?E" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

572 
using 1 `B \<in> sets E2` unfolding pair_measure_generator_def sets_sigma 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

573 
by (intro sigma_sets.Union) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

574 
(force simp: image_subset_iff intro!: sigma_sets.Basic) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

575 
finally have "snd ` B \<inter> space ?E \<in> sets ?E" . } 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

576 
ultimately have proj: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

577 
"fst \<in> measurable ?E (sigma E1) \<and> snd \<in> measurable ?E (sigma E2)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

578 
using E1 E2 by (subst (1 2) E.measurable_iff_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

579 
(auto simp: pair_measure_generator_def sets_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

580 
{ fix A B assume A: "A \<in> sets (sigma E1)" and B: "B \<in> sets (sigma E2)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

581 
with proj have "fst ` A \<inter> space ?E \<in> sets ?E" "snd ` B \<inter> space ?E \<in> sets ?E" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

582 
unfolding measurable_def by simp_all 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

583 
moreover have "A \<times> B = (fst ` A \<inter> space ?E) \<inter> (snd ` B \<inter> space ?E)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

584 
using A B M1.sets_into_space M2.sets_into_space 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

585 
by (auto simp: pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

586 
ultimately have "A \<times> B \<in> sets ?E" by auto } 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

587 
then have "sigma_sets (space ?E) (sets (pair_measure_generator (sigma E1) (sigma E2))) \<subseteq> sets ?E" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

588 
by (intro E.sigma_sets_subset) (auto simp add: pair_measure_generator_def sets_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

589 
then have subset: "sets ?S \<subseteq> sets ?E" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

590 
by (simp add: sets_sigma pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

591 
show "sets ?S = sets ?E" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

592 
proof (intro set_eqI iffI) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

593 
fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

594 
unfolding sets_sigma 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

595 
proof induct 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

596 
case (Basic A) then show ?case 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

597 
by (auto simp: pair_measure_generator_def sets_sigma intro: sigma_sets.Basic) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

598 
qed (auto intro: sigma_sets.intros simp: pair_measure_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

599 
next 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

600 
fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

601 
qed 
40859  602 
qed 
603 

604 
section "Fubinis theorem" 

605 

606 
lemma (in pair_sigma_finite) simple_function_cut: 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

607 
assumes f: "simple_function P f" "\<And>x. 0 \<le> f x" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

608 
shows "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

609 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  610 
proof  
611 
have f_borel: "f \<in> borel_measurable P" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

612 
using f(1) by (rule borel_measurable_simple_function) 
40859  613 
let "?F z" = "f ` {z} \<inter> space P" 
614 
let "?F' x z" = "Pair x ` ?F z" 

615 
{ fix x assume "x \<in> space M1" 

616 
have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y" 

617 
by (auto simp: indicator_def) 

618 
have "\<And>y. y \<in> space M2 \<Longrightarrow> (x, y) \<in> space P" using `x \<in> space M1` 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

619 
by (simp add: space_pair_measure) 
40859  620 
moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel 
621 
by (intro borel_measurable_vimage measurable_cut_fst) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

622 
ultimately have "simple_function M2 (\<lambda> y. f (x, y))" 
40859  623 
apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

624 
apply (rule simple_function_indicator_representation[OF f(1)]) 
40859  625 
using `x \<in> space M1` by (auto simp del: space_sigma) } 
626 
note M2_sf = this 

627 
{ fix x assume x: "x \<in> space M1" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

628 
then have "(\<integral>\<^isup>+y. f (x, y) \<partial>M2) = (\<Sum>z\<in>f ` space P. z * M2.\<mu> (?F' x z))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

629 
unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x] f(2)] 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

630 
unfolding simple_integral_def 
40859  631 
proof (safe intro!: setsum_mono_zero_cong_left) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

632 
from f(1) show "finite (f ` space P)" by (rule simple_functionD) 
40859  633 
next 
634 
fix y assume "y \<in> space M2" then show "f (x, y) \<in> f ` space P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

635 
using `x \<in> space M1` by (auto simp: space_pair_measure) 
40859  636 
next 
637 
fix x' y assume "(x', y) \<in> space P" 

638 
"f (x', y) \<notin> (\<lambda>y. f (x, y)) ` space M2" 

639 
then have *: "?F' x (f (x', y)) = {}" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

640 
by (force simp: space_pair_measure) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

641 
show "f (x', y) * M2.\<mu> (?F' x (f (x', y))) = 0" 
40859  642 
unfolding * by simp 
643 
qed (simp add: vimage_compose[symmetric] comp_def 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

644 
space_pair_measure) } 
40859  645 
note eq = this 
646 
moreover have "\<And>z. ?F z \<in> sets P" 

647 
by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

648 
moreover then have "\<And>z. (\<lambda>x. M2.\<mu> (?F' x z)) \<in> borel_measurable M1" 
40859  649 
by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

650 
moreover have *: "\<And>i x. 0 \<le> M2.\<mu> (Pair x ` (f ` {i} \<inter> space P))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

651 
using f(1)[THEN simple_functionD(2)] f(2) by (intro M2.positive_measure measurable_cut_fst) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

652 
moreover { fix i assume "i \<in> f`space P" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

653 
with * have "\<And>x. 0 \<le> i * M2.\<mu> (Pair x ` (f ` {i} \<inter> space P))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

654 
using f(2) by auto } 
40859  655 
ultimately 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

656 
show "(\<lambda>x. \<integral>\<^isup>+y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

657 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" using f(2) 
40859  658 
by (auto simp del: vimage_Int cong: measurable_cong 
43920  659 
intro!: M1.borel_measurable_ereal_setsum setsum_cong 
40859  660 
simp add: M1.positive_integral_setsum simple_integral_def 
661 
M1.positive_integral_cmult 

662 
M1.positive_integral_cong[OF eq] 

663 
positive_integral_eq_simple_integral[OF f] 

664 
pair_measure_alt[symmetric]) 

665 
qed 

666 

667 
lemma (in pair_sigma_finite) positive_integral_fst_measurable: 

668 
assumes f: "f \<in> borel_measurable P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

669 
shows "(\<lambda>x. \<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<in> borel_measurable M1" 
40859  670 
(is "?C f \<in> borel_measurable M1") 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

671 
and "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
40859  672 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

673 
from borel_measurable_implies_simple_function_sequence'[OF f] guess F . note F = this 
40859  674 
then have F_borel: "\<And>i. F i \<in> borel_measurable P" 
675 
by (auto intro: borel_measurable_simple_function) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

676 
note sf = simple_function_cut[OF F(1,5)] 
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

677 
then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1" 
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

678 
using F(1) by auto 
40859  679 
moreover 
680 
{ fix x assume "x \<in> space M1" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

681 
from F measurable_pair_image_snd[OF F_borel`x \<in> space M1`] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

682 
have "(\<integral>\<^isup>+y. (SUP i. F i (x, y)) \<partial>M2) = (SUP i. ?C (F i) x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

683 
by (intro M2.positive_integral_monotone_convergence_SUP) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

684 
(auto simp: incseq_Suc_iff le_fun_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

685 
then have "(SUP i. ?C (F i) x) = ?C f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

686 
unfolding F(4) positive_integral_max_0 by simp } 
40859  687 
note SUPR_C = this 
688 
ultimately show "?C f \<in> borel_measurable M1" 

41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

689 
by (simp cong: measurable_cong) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

690 
have "(\<integral>\<^isup>+x. (SUP i. F i x) \<partial>P) = (SUP i. integral\<^isup>P P (F i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

691 
using F_borel F 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

692 
by (intro positive_integral_monotone_convergence_SUP) auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

693 
also have "(SUP i. integral\<^isup>P P (F i)) = (SUP i. \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1)" 
40859  694 
unfolding sf(2) by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

695 
also have "\<dots> = \<integral>\<^isup>+ x. (SUP i. \<integral>\<^isup>+ y. F i (x, y) \<partial>M2) \<partial>M1" using F sf(1) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

696 
by (intro M1.positive_integral_monotone_convergence_SUP[symmetric]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

697 
(auto intro!: M2.positive_integral_mono M2.positive_integral_positive 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

698 
simp: incseq_Suc_iff le_fun_def) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

699 
also have "\<dots> = \<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. (SUP i. F i (x, y)) \<partial>M2) \<partial>M1" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

700 
using F_borel F(2,5) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

701 
by (auto intro!: M1.positive_integral_cong M2.positive_integral_monotone_convergence_SUP[symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

702 
simp: incseq_Suc_iff le_fun_def measurable_pair_image_snd) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

703 
finally show "(\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>P P f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

704 
using F by (simp add: positive_integral_max_0) 
40859  705 
qed 
706 

41831  707 
lemma (in pair_sigma_finite) measure_preserving_swap: 
708 
"(\<lambda>(x,y). (y, x)) \<in> measure_preserving (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)" 

709 
proof 

710 
interpret Q: pair_sigma_finite M2 M1 by default 

711 
show *: "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) (M2 \<Otimes>\<^isub>M M1)" 

712 
using pair_sigma_algebra_swap_measurable . 

713 
fix X assume "X \<in> sets (M2 \<Otimes>\<^isub>M M1)" 

714 
from measurable_sets[OF * this] this Q.sets_into_space[OF this] 

715 
show "measure (M1 \<Otimes>\<^isub>M M2) ((\<lambda>(x, y). (y, x)) ` X \<inter> space P) = measure (M2 \<Otimes>\<^isub>M M1) X" 

716 
by (auto intro!: M1.positive_integral_cong arg_cong[where f="M2.\<mu>"] 

717 
simp: pair_measure_alt Q.pair_measure_alt2 space_pair_measure) 

718 
qed 

719 

41661  720 
lemma (in pair_sigma_finite) positive_integral_product_swap: 
721 
assumes f: "f \<in> borel_measurable P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

722 
shows "(\<integral>\<^isup>+x. f (case x of (x,y)\<Rightarrow>(y,x)) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>P P f" 
41661  723 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

724 
interpret Q: pair_sigma_finite M2 M1 by default 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

725 
have "sigma_algebra P" by default 
41831  726 
with f show ?thesis 
727 
by (subst Q.positive_integral_vimage[OF _ Q.measure_preserving_swap]) auto 

41661  728 
qed 
729 

40859  730 
lemma (in pair_sigma_finite) positive_integral_snd_measurable: 
731 
assumes f: "f \<in> borel_measurable P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

732 
shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>P P f" 
40859  733 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

734 
interpret Q: pair_sigma_finite M2 M1 by default 
40859  735 
note pair_sigma_algebra_measurable[OF f] 
736 
from Q.positive_integral_fst_measurable[OF this] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

737 
have "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ (x, y). f (y, x) \<partial>Q.P)" 
40859  738 
by simp 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

739 
also have "(\<integral>\<^isup>+ (x, y). f (y, x) \<partial>Q.P) = integral\<^isup>P P f" 
41661  740 
unfolding positive_integral_product_swap[OF f, symmetric] 
741 
by (auto intro!: Q.positive_integral_cong) 

40859  742 
finally show ?thesis . 
743 
qed 

744 

745 
lemma (in pair_sigma_finite) Fubini: 

746 
assumes f: "f \<in> borel_measurable P" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

747 
shows "(\<integral>\<^isup>+ y. (\<integral>\<^isup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^isup>+ x. (\<integral>\<^isup>+ y. f (x, y) \<partial>M2) \<partial>M1)" 
40859  748 
unfolding positive_integral_snd_measurable[OF assms] 
749 
unfolding positive_integral_fst_measurable[OF assms] .. 

750 

751 
lemma (in pair_sigma_finite) AE_pair: 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

752 
assumes "AE x in P. Q x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

753 
shows "AE x in M1. (AE y in M2. Q (x, y))" 
40859  754 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

755 
obtain N where N: "N \<in> sets P" "\<mu> N = 0" "{x\<in>space P. \<not> Q x} \<subseteq> N" 
40859  756 
using assms unfolding almost_everywhere_def by auto 
757 
show ?thesis 

758 
proof (rule M1.AE_I) 

759 
from N measure_cut_measurable_fst[OF `N \<in> sets P`] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

760 
show "M1.\<mu> {x\<in>space M1. M2.\<mu> (Pair x ` N) \<noteq> 0} = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

761 
by (auto simp: pair_measure_alt M1.positive_integral_0_iff) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

762 
show "{x \<in> space M1. M2.\<mu> (Pair x ` N) \<noteq> 0} \<in> sets M1" 
43920  763 
by (intro M1.borel_measurable_ereal_neq_const measure_cut_measurable_fst N) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

764 
{ fix x assume "x \<in> space M1" "M2.\<mu> (Pair x ` N) = 0" 
40859  765 
have "M2.almost_everywhere (\<lambda>y. Q (x, y))" 
766 
proof (rule M2.AE_I) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

767 
show "M2.\<mu> (Pair x ` N) = 0" by fact 
40859  768 
show "Pair x ` N \<in> sets M2" by (intro measurable_cut_fst N) 
769 
show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x ` N" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

770 
using N `x \<in> space M1` unfolding space_sigma space_pair_measure by auto 
40859  771 
qed } 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

772 
then show "{x \<in> space M1. \<not> M2.almost_everywhere (\<lambda>y. Q (x, y))} \<subseteq> {x \<in> space M1. M2.\<mu> (Pair x ` N) \<noteq> 0}" 
40859  773 
by auto 
39088
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

774 
qed 
ca17017c10e6
Measurable on product space is equiv. to measurable components
hoelzl
parents:
39082
diff
changeset

775 
qed 
35833  776 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

777 
lemma (in pair_sigma_algebra) measurable_product_swap: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

778 
"f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable P M" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

779 
proof  
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

780 
interpret Q: pair_sigma_algebra M2 M1 by default 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

781 
show ?thesis 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

782 
using pair_sigma_algebra_measurable[of "\<lambda>(x,y). f (y, x)"] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

783 
by (auto intro!: pair_sigma_algebra_measurable Q.pair_sigma_algebra_measurable iffI) 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

784 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

785 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

786 
lemma (in pair_sigma_finite) integrable_product_swap: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

787 
assumes "integrable P f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

788 
shows "integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x))" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

789 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

790 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  791 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
792 
show ?thesis unfolding * 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

793 
using assms unfolding integrable_def 
41661  794 
apply (subst (1 2) positive_integral_product_swap) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

795 
using `integrable P f` unfolding integrable_def 
41661  796 
by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric]) 
797 
qed 

798 

799 
lemma (in pair_sigma_finite) integrable_product_swap_iff: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

800 
"integrable (M2 \<Otimes>\<^isub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable P f" 
41661  801 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

802 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  803 
from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f] 
804 
show ?thesis by auto 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

805 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

806 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

807 
lemma (in pair_sigma_finite) integral_product_swap: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

808 
assumes "integrable P f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

809 
shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^isub>M M1)) = integral\<^isup>L P f" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

810 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

811 
interpret Q: pair_sigma_finite M2 M1 by default 
41661  812 
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

813 
show ?thesis 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

814 
unfolding lebesgue_integral_def * 
41661  815 
apply (subst (1 2) positive_integral_product_swap) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

816 
using `integrable P f` unfolding integrable_def 
41661  817 
by (auto simp: *[symmetric] Q.measurable_product_swap[symmetric]) 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

818 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

819 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

820 
lemma (in pair_sigma_finite) integrable_fst_measurable: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

821 
assumes f: "integrable P f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

822 
shows "M1.almost_everywhere (\<lambda>x. integrable M2 (\<lambda> y. f (x, y)))" (is "?AE") 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

823 
and "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^isup>L P f" (is "?INT") 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

824 
proof  
43920  825 
let "?pf x" = "ereal (f x)" and "?nf x" = "ereal ( f x)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

826 
have 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

827 
borel: "?nf \<in> borel_measurable P""?pf \<in> borel_measurable P" and 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

828 
int: "integral\<^isup>P P ?nf \<noteq> \<infinity>" "integral\<^isup>P P ?pf \<noteq> \<infinity>" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

829 
using assms by auto 
43920  830 
have "(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>" 
831 
"(\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal ( f (x, y)) \<partial>M2) \<partial>M1) \<noteq> \<infinity>" 

41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

832 
using borel[THEN positive_integral_fst_measurable(1)] int 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

833 
unfolding borel[THEN positive_integral_fst_measurable(2)] by simp_all 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

834 
with borel[THEN positive_integral_fst_measurable(1)] 
43920  835 
have AE_pos: "AE x in M1. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<noteq> \<infinity>" 
836 
"AE x in M1. (\<integral>\<^isup>+y. ereal ( f (x, y)) \<partial>M2) \<noteq> \<infinity>" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

837 
by (auto intro!: M1.positive_integral_PInf_AE ) 
43920  838 
then have AE: "AE x in M1. \<bar>\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>" 
839 
"AE x in M1. \<bar>\<integral>\<^isup>+y. ereal ( f (x, y)) \<partial>M2\<bar> \<noteq> \<infinity>" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

840 
by (auto simp: M2.positive_integral_positive) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

841 
from AE_pos show ?AE using assms 
41705  842 
by (simp add: measurable_pair_image_snd integrable_def) 
43920  843 
{ fix f have "(\<integral>\<^isup>+ x.  \<integral>\<^isup>+ y. ereal (f x y) \<partial>M2 \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

844 
using M2.positive_integral_positive 
43920  845 
by (intro M1.positive_integral_cong_pos) (auto simp: ereal_uminus_le_reorder) 
846 
then have "(\<integral>\<^isup>+ x.  \<integral>\<^isup>+ y. ereal (f x y) \<partial>M2 \<partial>M1) = 0" by simp } 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

847 
note this[simp] 
43920  848 
{ fix f assume borel: "(\<lambda>x. ereal (f x)) \<in> borel_measurable P" 
849 
and int: "integral\<^isup>P P (\<lambda>x. ereal (f x)) \<noteq> \<infinity>" 

850 
and AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<noteq> \<infinity>)" 

851 
have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2))" (is "integrable M1 ?f") 

41705  852 
proof (intro integrable_def[THEN iffD2] conjI) 
853 
show "?f \<in> borel_measurable M1" 

43920  854 
using borel by (auto intro!: M1.borel_measurable_real_of_ereal positive_integral_fst_measurable) 
855 
have "(\<integral>\<^isup>+x. ereal (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. ereal (f (x, y)) \<partial>M2) \<partial>M1)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

856 
using AE M2.positive_integral_positive 
43920  857 
by (auto intro!: M1.positive_integral_cong_AE simp: ereal_real) 
858 
then show "(\<integral>\<^isup>+x. ereal (?f x) \<partial>M1) \<noteq> \<infinity>" 

41705  859 
using positive_integral_fst_measurable[OF borel] int by simp 
43920  860 
have "(\<integral>\<^isup>+x. ereal ( ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

861 
by (intro M1.positive_integral_cong_pos) 
43920  862 
(simp add: M2.positive_integral_positive real_of_ereal_pos) 
863 
then show "(\<integral>\<^isup>+x. ereal ( ?f x) \<partial>M1) \<noteq> \<infinity>" by simp 

41705  864 
qed } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

865 
with this[OF borel(1) int(1) AE_pos(2)] this[OF borel(2) int(2) AE_pos(1)] 
41705  866 
show ?INT 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

867 
unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2] 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

868 
borel[THEN positive_integral_fst_measurable(2), symmetric] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

869 
using AE[THEN M1.integral_real] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

870 
by simp 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

871 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

872 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

873 
lemma (in pair_sigma_finite) integrable_snd_measurable: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

874 
assumes f: "integrable P f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

875 
shows "M2.almost_everywhere (\<lambda>y. integrable M1 (\<lambda>x. f (x, y)))" (is "?AE") 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

876 
and "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = integral\<^isup>L P f" (is "?INT") 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

877 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

878 
interpret Q: pair_sigma_finite M2 M1 by default 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

879 
have Q_int: "integrable Q.P (\<lambda>(x, y). f (y, x))" 
41661  880 
using f unfolding integrable_product_swap_iff . 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

881 
show ?INT 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

882 
using Q.integrable_fst_measurable(2)[OF Q_int] 
41661  883 
using integral_product_swap[OF f] by simp 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

884 
show ?AE 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

885 
using Q.integrable_fst_measurable(1)[OF Q_int] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

886 
by simp 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

887 
qed 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

888 

bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

889 
lemma (in pair_sigma_finite) Fubini_integral: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

890 
assumes f: "integrable P f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

891 
shows "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1)" 
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

892 
unfolding integrable_snd_measurable[OF assms] 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

893 
unfolding integrable_fst_measurable[OF assms] .. 
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset

894 

40859  895 
section "Products on finite spaces" 
896 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

897 
lemma sigma_sets_pair_measure_generator_finite: 
38656  898 
assumes "finite A" and "finite B" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

899 
shows "sigma_sets (A \<times> B) { a \<times> b  a b. a \<in> Pow A \<and> b \<in> Pow B} = Pow (A \<times> B)" 
40859  900 
(is "sigma_sets ?prod ?sets = _") 
38656  901 
proof safe 
902 
have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product) 

903 
fix x assume subset: "x \<subseteq> A \<times> B" 

904 
hence "finite x" using fin by (rule finite_subset) 

40859  905 
from this subset show "x \<in> sigma_sets ?prod ?sets" 
38656  906 
proof (induct x) 
907 
case empty show ?case by (rule sigma_sets.Empty) 

908 
next 

909 
case (insert a x) 

40859  910 
hence "{a} \<in> sigma_sets ?prod ?sets" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

911 
by (auto simp: pair_measure_generator_def intro!: sigma_sets.Basic) 
38656  912 
moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto 
913 
ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un) 

914 
qed 

915 
next 

916 
fix x a b 

40859  917 
assume "x \<in> sigma_sets ?prod ?sets" and "(a, b) \<in> x" 
38656  918 
from sigma_sets_into_sp[OF _ this(1)] this(2) 
40859  919 
show "a \<in> A" and "b \<in> B" by auto 
35833  920 
qed 
921 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

922 
locale pair_finite_sigma_algebra = M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

923 
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme" 
40859  924 

925 
sublocale pair_finite_sigma_algebra \<subseteq> pair_sigma_algebra by default 

926 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

927 
lemma (in pair_finite_sigma_algebra) finite_pair_sigma_algebra: 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

928 
shows "P = \<lparr> space = space M1 \<times> space M2, sets = Pow (space M1 \<times> space M2), \<dots> = algebra.more P \<rparr>" 
35977  929 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

930 
show ?thesis 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

931 
using sigma_sets_pair_measure_generator_finite[OF M1.finite_space M2.finite_space] 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

932 
by (intro algebra.equality) (simp_all add: pair_measure_def pair_measure_generator_def sigma_def) 
40859  933 
qed 
934 

935 
sublocale pair_finite_sigma_algebra \<subseteq> finite_sigma_algebra P 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

936 
apply default 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

937 
using M1.finite_space M2.finite_space 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

938 
apply (subst finite_pair_sigma_algebra) apply simp 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

939 
apply (subst (1 2) finite_pair_sigma_algebra) apply simp 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

940 
done 
35833  941 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

942 
locale pair_finite_space = M1: finite_measure_space M1 + M2: finite_measure_space M2 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

943 
for M1 M2 
40859  944 

945 
sublocale pair_finite_space \<subseteq> pair_finite_sigma_algebra 

946 
by default 

35833  947 

40859  948 
sublocale pair_finite_space \<subseteq> pair_sigma_finite 
949 
by default 

38656  950 

40859  951 
lemma (in pair_finite_space) pair_measure_Pair[simp]: 
952 
assumes "a \<in> space M1" "b \<in> space M2" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

953 
shows "\<mu> {(a, b)} = M1.\<mu> {a} * M2.\<mu> {b}" 
40859  954 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

955 
have "\<mu> ({a}\<times>{b}) = M1.\<mu> {a} * M2.\<mu> {b}" 
40859  956 
using M1.sets_eq_Pow M2.sets_eq_Pow assms 
957 
by (subst pair_measure_times) auto 

958 
then show ?thesis by simp 

38656  959 
qed 
960 

40859  961 
lemma (in pair_finite_space) pair_measure_singleton[simp]: 
962 
assumes "x \<in> space M1 \<times> space M2" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

963 
shows "\<mu> {x} = M1.\<mu> {fst x} * M2.\<mu> {snd x}" 
40859  964 
using pair_measure_Pair assms by (cases x) auto 
38656  965 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

966 
sublocale pair_finite_space \<subseteq> finite_measure_space P 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

967 
by default (auto simp: space_pair_measure) 
39097  968 

40859  969 
end 