author  hoelzl 
Mon, 08 Mar 2010 11:30:55 +0100  
changeset 35692  f1315bbf1bc9 
parent 35582  b16d99a72dc9 
child 35704  5007843dae33 
permissions  rwrr 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

1 
header {*Borel Sets*} 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

2 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

3 
theory Borel 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

4 
imports Measure 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

5 
begin 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

6 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

7 
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

8 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

9 
definition borel_space where 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

10 
"borel_space = sigma (UNIV::real set) (range (\<lambda>a::real. {x. x \<le> a}))" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

11 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

12 
definition borel_measurable where 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

13 
"borel_measurable a = measurable a borel_space" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

14 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

15 
definition indicator_fn where 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

16 
"indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

17 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

18 
lemma in_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

19 
"f \<in> borel_measurable M \<longleftrightarrow> 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

20 
sigma_algebra M \<and> 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

21 
(\<forall>s \<in> sets (sigma UNIV (range (\<lambda>a::real. {x. x \<le> a}))). 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

22 
f ` s \<inter> space M \<in> sets M)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

23 
apply (auto simp add: borel_measurable_def measurable_def borel_space_def) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

24 
apply (metis PowD UNIV_I Un_commute sigma_algebra_sigma subset_Pow_Union subset_UNIV subset_Un_eq) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

25 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

26 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

27 
lemma (in sigma_algebra) borel_measurable_const: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

28 
"(\<lambda>x. c) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

29 
by (auto simp add: in_borel_measurable prems) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

30 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

31 
lemma (in sigma_algebra) borel_measurable_indicator: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

32 
assumes a: "a \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

33 
shows "indicator_fn a \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

34 
apply (auto simp add: in_borel_measurable indicator_fn_def prems) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

35 
apply (metis Diff_eq Int_commute a compl_sets) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

36 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

37 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

38 
lemma Collect_eq: "{w \<in> X. f w \<le> a} = {w. f w \<le> a} \<inter> X" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

39 
by (metis Collect_conj_eq Collect_mem_eq Int_commute) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

40 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

41 
lemma (in measure_space) borel_measurable_le_iff: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

42 
"f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

43 
proof 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

44 
assume f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

45 
{ fix a 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

46 
have "{w \<in> space M. f w \<le> a} \<in> sets M" using f 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

47 
apply (auto simp add: in_borel_measurable sigma_def Collect_eq) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

48 
apply (drule_tac x="{x. x \<le> a}" in bspec, auto) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

49 
apply (metis equalityE rangeI subsetD sigma_sets.Basic) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

50 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

51 
} 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

52 
thus "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" by blast 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

53 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

54 
assume "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

55 
thus "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

56 
apply (simp add: borel_measurable_def borel_space_def Collect_eq) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

57 
apply (rule measurable_sigma, auto) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

58 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

59 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

60 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

61 
lemma Collect_less_le: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

62 
"{w \<in> X. f w < g w} = (\<Union>n. {w \<in> X. f w \<le> g w  inverse(real(Suc n))})" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

63 
proof auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

64 
fix w 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

65 
assume w: "f w < g w" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

66 
hence nz: "g w  f w \<noteq> 0" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

67 
by arith 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

68 
with w have "real(Suc(natceiling(inverse(g w  f w)))) > inverse(g w  f w)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

69 
by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff) hence "inverse(real(Suc(natceiling(inverse(g w  f w))))) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

70 
< inverse(inverse(g w  f w))" 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
33657
diff
changeset

71 
by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

72 
hence "inverse(real(Suc(natceiling(inverse(g w  f w))))) < g w  f w" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

73 
by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

74 
thus "\<exists>n. f w \<le> g w  inverse(real(Suc n))" using w 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

75 
by (rule_tac x="natceiling(inverse(g w  f w))" in exI, auto) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

76 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

77 
fix w n 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

78 
assume le: "f w \<le> g w  inverse(real(Suc n))" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

79 
hence "0 < inverse(real(Suc n))" 
35347  80 
by simp 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

81 
thus "f w < g w" using le 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

82 
by arith 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

83 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

84 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

85 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

86 
lemma (in sigma_algebra) sigma_le_less: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

87 
assumes M: "!!a::real. {w \<in> space M. f w \<le> a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

88 
shows "{w \<in> space M. f w < a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

89 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

90 
show ?thesis using Collect_less_le [of "space M" f "\<lambda>x. a"] 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

91 
by (auto simp add: countable_UN M) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

92 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

93 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

94 
lemma (in sigma_algebra) sigma_less_ge: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

95 
assumes M: "!!a::real. {w \<in> space M. f w < a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

96 
shows "{w \<in> space M. a \<le> f w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

97 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

98 
have "{w \<in> space M. a \<le> f w} = space M  {w \<in> space M. f w < a}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

99 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

100 
thus ?thesis using M 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

101 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

102 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

103 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

104 
lemma (in sigma_algebra) sigma_ge_gr: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

105 
assumes M: "!!a::real. {w \<in> space M. a \<le> f w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

106 
shows "{w \<in> space M. a < f w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

107 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

108 
show ?thesis using Collect_less_le [of "space M" "\<lambda>x. a" f] 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

109 
by (auto simp add: countable_UN le_diff_eq M) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

110 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

111 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

112 
lemma (in sigma_algebra) sigma_gr_le: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

113 
assumes M: "!!a::real. {w \<in> space M. a < f w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

114 
shows "{w \<in> space M. f w \<le> a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

115 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

116 
have "{w \<in> space M. f w \<le> a} = space M  {w \<in> space M. a < f w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

117 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

118 
thus ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

119 
by (simp add: M compl_sets) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

120 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

121 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

122 
lemma (in measure_space) borel_measurable_gr_iff: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

123 
"f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

124 
proof (auto simp add: borel_measurable_le_iff sigma_gr_le) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

125 
fix u 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

126 
assume M: "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

127 
have "{w \<in> space M. u < f w} = space M  {w \<in> space M. f w \<le> u}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

128 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

129 
thus "{w \<in> space M. u < f w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

130 
by (force simp add: compl_sets countable_UN M) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

131 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

132 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

133 
lemma (in measure_space) borel_measurable_less_iff: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

134 
"f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

135 
proof (auto simp add: borel_measurable_le_iff sigma_le_less) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

136 
fix u 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

137 
assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

138 
have "{w \<in> space M. f w \<le> u} = space M  {w \<in> space M. u < f w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

139 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

140 
thus "{w \<in> space M. f w \<le> u} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

141 
using Collect_less_le [of "space M" "\<lambda>x. u" f] 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

142 
by (force simp add: compl_sets countable_UN le_diff_eq sigma_less_ge M) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

143 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

144 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

145 
lemma (in measure_space) borel_measurable_ge_iff: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

146 
"f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

147 
proof (auto simp add: borel_measurable_less_iff sigma_le_less sigma_ge_gr sigma_gr_le) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

148 
fix u 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

149 
assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

150 
have "{w \<in> space M. u \<le> f w} = space M  {w \<in> space M. f w < u}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

151 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

152 
thus "{w \<in> space M. u \<le> f w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

153 
by (force simp add: compl_sets countable_UN M) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

154 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

155 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

156 
lemma (in measure_space) affine_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

157 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

158 
shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

159 
proof (cases rule: linorder_cases [of b 0]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

160 
case equal thus ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

161 
by (simp add: borel_measurable_const) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

162 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

163 
case less 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

164 
{ 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

165 
fix w c 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

166 
have "a + g w * b \<le> c \<longleftrightarrow> g w * b \<le> c  a" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

167 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

168 
also have "... \<longleftrightarrow> (ca)/b \<le> g w" using less 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

169 
by (metis divide_le_eq less less_asym) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

170 
finally have "a + g w * b \<le> c \<longleftrightarrow> (ca)/b \<le> g w" . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

171 
} 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

172 
hence "\<And>w c. a + g w * b \<le> c \<longleftrightarrow> (ca)/b \<le> g w" . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

173 
thus ?thesis using less g 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

174 
by (simp add: borel_measurable_ge_iff [of g]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

175 
(simp add: borel_measurable_le_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

176 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

177 
case greater 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

178 
hence 0: "\<And>x c. (g x * b \<le> c  a) \<longleftrightarrow> (g x \<le> (c  a) / b)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

179 
by (metis mult_imp_le_div_pos le_divide_eq) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

180 
have 1: "\<And>x c. (a + g x * b \<le> c) \<longleftrightarrow> (g x * b \<le> c  a)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

181 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

182 
from greater g 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

183 
show ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

184 
by (simp add: borel_measurable_le_iff 0 1) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

185 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

186 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

187 
definition 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

188 
nat_to_rat_surj :: "nat \<Rightarrow> rat" where 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

189 
"nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

190 
in Fract (nat_to_int_bij i) (nat_to_int_bij j))" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

191 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

192 
lemma nat_to_rat_surj: "surj nat_to_rat_surj" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

193 
proof (auto simp add: surj_def nat_to_rat_surj_def) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

194 
fix y 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

195 
show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

196 
proof (cases y) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

197 
case (Fract a b) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

198 
obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

199 
by (metis surj_def) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

200 
obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

201 
by (metis surj_def) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

202 
obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

203 
by (metis surj_def) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

204 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

205 
from Fract i j n show ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

206 
by (metis prod.cases prod_case_split) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

207 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

208 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

209 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

210 
lemma rats_enumeration: "\<rat> = range (of_rat o nat_to_rat_surj)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

211 
using nat_to_rat_surj 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

212 
by (auto simp add: image_def surj_def) (metis Rats_cases) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

213 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

214 
lemma (in measure_space) borel_measurable_less_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

215 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

216 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

217 
shows "{w \<in> space M. f w < g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

218 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

219 
have "{w \<in> space M. f w < g w} = 
33536  220 
(\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

221 
by (auto simp add: Rats_dense_in_real) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

222 
thus ?thesis using f g 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

223 
by (simp add: borel_measurable_less_iff [of f] 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

224 
borel_measurable_gr_iff [of g]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

225 
(blast intro: gen_countable_UN [OF rats_enumeration]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

226 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

227 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

228 
lemma (in measure_space) borel_measurable_leq_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

229 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

230 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

231 
shows "{w \<in> space M. f w \<le> g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

232 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

233 
have "{w \<in> space M. f w \<le> g w} = space M  {w \<in> space M. g w < f w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

234 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

235 
thus ?thesis using f g 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

236 
by (simp add: borel_measurable_less_borel_measurable compl_sets) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

237 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

238 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

239 
lemma (in measure_space) borel_measurable_eq_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

240 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

241 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

242 
shows "{w \<in> space M. f w = g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

243 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

244 
have "{w \<in> space M. f w = g w} = 
33536  245 
{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}" 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

246 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

247 
thus ?thesis using f g 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

248 
by (simp add: borel_measurable_leq_borel_measurable Int) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

249 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

250 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

251 
lemma (in measure_space) borel_measurable_neq_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

252 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

253 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

254 
shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

255 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

256 
have "{w \<in> space M. f w \<noteq> g w} = space M  {w \<in> space M. f w = g w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

257 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

258 
thus ?thesis using f g 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

259 
by (simp add: borel_measurable_eq_borel_measurable compl_sets) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

260 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

261 

33535  262 
lemma (in measure_space) borel_measurable_add_borel_measurable: 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

263 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

264 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

265 
shows "(\<lambda>x. f x + g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

266 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

267 
have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * 1 \<le> f w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

268 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

269 
have "!!a. (\<lambda>w. a + (g w) * 1) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

270 
by (rule affine_borel_measurable [OF g]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

271 
hence "!!a. {w \<in> space M. (\<lambda>w. a + (g w) * 1)(w) \<le> f w} \<in> sets M" using f 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

272 
by (rule borel_measurable_leq_borel_measurable) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

273 
hence "!!a. {w \<in> space M. a \<le> f w + g w} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

274 
by (simp add: 1) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

275 
thus ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

276 
by (simp add: borel_measurable_ge_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

277 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

278 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

279 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

280 
lemma (in measure_space) borel_measurable_square: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

281 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

282 
shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

283 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

284 
{ 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

285 
fix a 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

286 
have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

287 
proof (cases rule: linorder_cases [of a 0]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

288 
case less 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

289 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

290 
by auto (metis less order_le_less_trans power2_less_0) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

291 
also have "... \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

292 
by (rule empty_sets) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

293 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

294 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

295 
case equal 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

296 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

297 
{w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

298 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

299 
also have "... \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

300 
apply (insert f) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

301 
apply (rule Int) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

302 
apply (simp add: borel_measurable_le_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

303 
apply (simp add: borel_measurable_ge_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

304 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

305 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

306 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

307 
case greater 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

308 
have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = ( sqrt a \<le> f x & f x \<le> sqrt a)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

309 
by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

310 
real_sqrt_le_iff real_sqrt_power) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

311 
hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

312 
{w \<in> space M. (sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

313 
using greater by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

314 
also have "... \<in> sets M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

315 
apply (insert f) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

316 
apply (rule Int) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

317 
apply (simp add: borel_measurable_ge_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

318 
apply (simp add: borel_measurable_le_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

319 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

320 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

321 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

322 
} 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

323 
thus ?thesis by (auto simp add: borel_measurable_le_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

324 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

325 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

326 
lemma times_eq_sum_squares: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

327 
fixes x::real 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

328 
shows"x*y = ((x+y)^2)/4  ((xy)^ 2)/4" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

329 
by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

330 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

331 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

332 
lemma (in measure_space) borel_measurable_uminus_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

333 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

334 
shows "(\<lambda>x.  g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

335 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

336 
have "(\<lambda>x.  g x) = (\<lambda>x. 0 + (g x) * 1)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

337 
by simp 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

338 
also have "... \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

339 
by (fast intro: affine_borel_measurable g) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

340 
finally show ?thesis . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

341 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

342 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

343 
lemma (in measure_space) borel_measurable_times_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

344 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

345 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

346 
shows "(\<lambda>x. f x * g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

347 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

348 
have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

349 
by (fast intro: affine_borel_measurable borel_measurable_square 
33535  350 
borel_measurable_add_borel_measurable f g) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

351 
have "(\<lambda>x. ((f x + g x) ^ 2 * inverse 4)) = 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

352 
(\<lambda>x. 0 + ((f x + g x) ^ 2 * inverse 4))" 
35582  353 
by (simp add: minus_divide_right) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

354 
also have "... \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

355 
by (fast intro: affine_borel_measurable borel_measurable_square 
33535  356 
borel_measurable_add_borel_measurable 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

357 
borel_measurable_uminus_borel_measurable f g) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

358 
finally have 2: "(\<lambda>x. ((f x + g x) ^ 2 * inverse 4)) \<in> borel_measurable M" . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

359 
show ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

360 
apply (simp add: times_eq_sum_squares real_diff_def) 
33535  361 
using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

362 
done 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

363 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

364 

40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

365 
lemma (in measure_space) borel_measurable_diff_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

366 
assumes f: "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

367 
assumes g: "g \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

368 
shows "(\<lambda>x. f x  g x) \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

369 
unfolding real_diff_def 
33535  370 
by (fast intro: borel_measurable_add_borel_measurable 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

371 
borel_measurable_uminus_borel_measurable f g) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

372 

35692  373 
lemma (in measure_space) borel_measurable_setsum_borel_measurable: 
374 
assumes s: "finite s" 

375 
shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s 

376 
proof (induct s) 

377 
case empty 

378 
thus ?case 

379 
by (simp add: borel_measurable_const) 

380 
next 

381 
case (insert x s) 

382 
thus ?case 

383 
by (auto simp add: borel_measurable_add_borel_measurable) 

384 
qed 

385 

386 
lemma (in measure_space) borel_measurable_cong: 

387 
assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w" 

388 
shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M" 

389 
using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong) 

390 

391 
lemma (in measure_space) borel_measurable_inverse: 

392 
assumes "f \<in> borel_measurable M" 

393 
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M" 

394 
unfolding borel_measurable_ge_iff 

395 
proof (safe, rule linorder_cases) 

396 
fix a :: real assume "0 < a" 

397 
{ fix w 

398 
from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a" 

399 
by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le 

400 
linorder_not_le real_le_refl real_le_trans real_less_def 

401 
xt1(7) zero_less_divide_1_iff) } 

402 
hence "{w \<in> space M. a \<le> inverse (f w)} = 

403 
{w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto 

404 
with Int assms[unfolded borel_measurable_gr_iff] 

405 
assms[unfolded borel_measurable_le_iff] 

406 
show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp 

407 
next 

408 
fix a :: real assume "0 = a" 

409 
{ fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w" 

410 
unfolding `0 = a`[symmetric] by auto } 

411 
thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" 

412 
using assms[unfolded borel_measurable_ge_iff] by simp 

413 
next 

414 
fix a :: real assume "a < 0" 

415 
{ fix w 

416 
from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w" 

417 
apply (cases "0 \<le> f w") 

418 
apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9) 

419 
zero_le_divide_1_iff) 

420 
apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg 

421 
linorder_not_le real_le_refl real_le_trans) 

422 
done } 

423 
hence "{w \<in> space M. a \<le> inverse (f w)} = 

424 
{w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto 

425 
with Un assms[unfolded borel_measurable_ge_iff] 

426 
assms[unfolded borel_measurable_le_iff] 

427 
show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp 

428 
qed 

429 

430 
lemma (in measure_space) borel_measurable_divide: 

431 
assumes "f \<in> borel_measurable M" 

432 
and "g \<in> borel_measurable M" 

433 
shows "(\<lambda>x. f x / g x) \<in> borel_measurable M" 

434 
unfolding field_divide_inverse 

435 
by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+ 

436 

437 

438 
section "Monotone convergence" 

439 

440 
definition mono_convergent where 

441 
"mono_convergent u f s \<equiv> 

442 
(\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and> 

443 
(\<forall>x \<in> s. (\<lambda>i. u i x) > f x)" 

444 

445 
definition "upclose f g x = max (f x) (g x)" 

446 

447 
primrec mon_upclose where 

448 
"mon_upclose 0 u = u 0"  

449 
"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)" 

450 

451 
lemma mono_convergentD: 

452 
assumes "mono_convergent u f s" and "x \<in> s" 

453 
shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) > f x" 

454 
using assms unfolding mono_convergent_def by auto 

455 

456 
lemma mono_convergentI: 

457 
assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)" 

458 
assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) > f x" 

459 
shows "mono_convergent u f s" 

460 
using assms unfolding mono_convergent_def by auto 

461 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

462 
lemma (in measure_space) mono_convergent_borel_measurable: 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

463 
assumes u: "!!n. u n \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

464 
assumes mc: "mono_convergent u f (space M)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

465 
shows "f \<in> borel_measurable M" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

466 
proof  
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

467 
{ 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

468 
fix a 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

469 
have 1: "!!w. w \<in> space M & f w <= a \<longleftrightarrow> w \<in> space M & (\<forall>i. u i w <= a)" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

470 
proof safe 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

471 
fix w i 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

472 
assume w: "w \<in> space M" and f: "f w \<le> a" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

473 
hence "u i w \<le> f w" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

474 
by (auto intro: SEQ.incseq_le 
35582  475 
simp add: mc [unfolded mono_convergent_def]) 
33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

476 
thus "u i w \<le> a" using f 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

477 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

478 
next 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

479 
fix w 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

480 
assume w: "w \<in> space M" and u: "\<forall>i. u i w \<le> a" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

481 
thus "f w \<le> a" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

482 
by (metis LIMSEQ_le_const2 mc [unfolded mono_convergent_def]) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

483 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

484 
have "{w \<in> space M. f w \<le> a} = {w \<in> space M. (\<forall>i. u i w <= a)}" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

485 
by (simp add: 1) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

486 
also have "... = (\<Inter>i. {w \<in> space M. u i w \<le> a})" 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

487 
by auto 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

488 
also have "... \<in> sets M" using u 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

489 
by (auto simp add: borel_measurable_le_iff intro: countable_INT) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

490 
finally have "{w \<in> space M. f w \<le> a} \<in> sets M" . 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

491 
} 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

492 
thus ?thesis 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

493 
by (auto simp add: borel_measurable_le_iff) 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

494 
qed 
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

495 

35582  496 
lemma mono_convergent_le: 
497 
assumes "mono_convergent u f s" and "t \<in> s" 

498 
shows "u n t \<le> f t" 

499 
using mono_convergentD[OF assms] by (auto intro!: incseq_le) 

500 

501 
lemma mon_upclose_ex: 

502 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)" 

503 
shows "\<exists>n \<le> m. mon_upclose m u x = u n x" 

504 
proof (induct m) 

505 
case (Suc m) 

506 
then obtain n where "n \<le> m" and *: "mon_upclose m u x = u n x" by blast 

507 
thus ?case 

508 
proof (cases "u n x \<le> u (Suc m) x") 

509 
case True with min_max.sup_absorb1 show ?thesis 

510 
by (auto simp: * upclose_def intro!: exI[of _ "Suc m"]) 

511 
next 

512 
case False 

513 
with min_max.sup_absorb2 `n \<le> m` show ?thesis 

514 
by (auto simp: * upclose_def intro!: exI[of _ n] min_max.sup_absorb2) 

515 
qed 

516 
qed simp 

517 

518 
lemma mon_upclose_all: 

519 
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)" 

520 
assumes "m \<le> n" 

521 
shows "u m x \<le> mon_upclose n u x" 

522 
using assms proof (induct n) 

523 
case 0 thus ?case by auto 

524 
next 

525 
case (Suc n) 

526 
show ?case 

527 
proof (cases "m = Suc n") 

528 
case True thus ?thesis by (simp add: upclose_def) 

529 
next 

530 
case False 

531 
hence "m \<le> n" using `m \<le> Suc n` by simp 

532 
from Suc.hyps[OF this] 

533 
show ?thesis by (auto simp: upclose_def intro!: min_max.le_supI2) 

534 
qed 

535 
qed 

536 

537 
lemma mono_convergent_limit: 

538 
fixes f :: "'a \<Rightarrow> real" 

539 
assumes "mono_convergent u f s" and "x \<in> s" and "0 < r" 

540 
shows "\<exists>N. \<forall>n\<ge>N. f x  u n x < r" 

541 
proof  

542 
from LIMSEQ_D[OF mono_convergentD(2)[OF assms(1,2)] `0 < r`] 

543 
obtain N where "\<And>n. N \<le> n \<Longrightarrow> \<bar> u n x  f x \<bar> < r" by auto 

544 
with mono_convergent_le[OF assms(1,2)] `0 < r` 

545 
show ?thesis by (auto intro!: exI[of _ N]) 

546 
qed 

547 

548 
lemma mon_upclose_le_mono_convergent: 

549 
assumes mc: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s" and "x \<in> s" 

550 
and "incseq (\<lambda>n. f n x)" 

551 
shows "mon_upclose n (u n) x <= f n x" 

552 
proof  

553 
obtain m where *: "mon_upclose n (u n) x = u n m x" and "m \<le> n" 

554 
using mon_upclose_ex[of n "u n" x] by auto 

555 
note this(1) 

556 
also have "u n m x \<le> f m x" using mono_convergent_le[OF assms(1,2)] . 

557 
also have "... \<le> f n x" using assms(3) `m \<le> n` unfolding incseq_def by auto 

558 
finally show ?thesis . 

559 
qed 

560 

561 
lemma mon_upclose_mono_convergent: 

562 
assumes mc_u: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s" 

563 
and mc_f: "mono_convergent f h s" 

564 
shows "mono_convergent (\<lambda>n. mon_upclose n (u n)) h s" 

565 
proof (rule mono_convergentI) 

566 
fix x assume "x \<in> s" 

567 
show "incseq (\<lambda>n. mon_upclose n (u n) x)" unfolding incseq_def 

568 
proof safe 

569 
fix m n :: nat assume "m \<le> n" 

570 
obtain i where mon: "mon_upclose m (u m) x = u m i x" and "i \<le> m" 

571 
using mon_upclose_ex[of m "u m" x] by auto 

572 
hence "i \<le> n" using `m \<le> n` by auto 

573 

574 
note mon 

575 
also have "u m i x \<le> u n i x" 

576 
using mono_convergentD(1)[OF mc_u `x \<in> s`] `m \<le> n` 

577 
unfolding incseq_def by auto 

578 
also have "u n i x \<le> mon_upclose n (u n) x" 

579 
using mon_upclose_all[OF `i \<le> n`, of "u n" x] . 

580 
finally show "mon_upclose m (u m) x \<le> mon_upclose n (u n) x" . 

581 
qed 

582 

583 
show "(\<lambda>i. mon_upclose i (u i) x) > h x" 

584 
proof (rule LIMSEQ_I) 

585 
fix r :: real assume "0 < r" 

586 
hence "0 < r / 2" by auto 

587 
from mono_convergent_limit[OF mc_f `x \<in> s` this] 

588 
obtain N where f_h: "\<And>n. N \<le> n \<Longrightarrow> h x  f n x < r / 2" by auto 

589 

590 
from mono_convergent_limit[OF mc_u `x \<in> s` `0 < r / 2`] 

591 
obtain N' where u_f: "\<And>n. N' \<le> n \<Longrightarrow> f N x  u n N x < r / 2" by auto 

592 

593 
show "\<exists>N. \<forall>n\<ge>N. norm (mon_upclose n (u n) x  h x) < r" 

594 
proof (rule exI[of _ "max N N'"], safe) 

595 
fix n assume "max N N' \<le> n" 

596 
hence "N \<le> n" and "N' \<le> n" by auto 

597 
hence "u n N x \<le> mon_upclose n (u n) x" 

598 
using mon_upclose_all[of N n "u n" x] by auto 

599 
moreover 

600 
from add_strict_mono[OF u_f[OF `N' \<le> n`] f_h[OF order_refl]] 

601 
have "h x  u n N x < r" by auto 

602 
ultimately have "h x  mon_upclose n (u n) x < r" by auto 

603 
moreover 

604 
obtain i where "mon_upclose n (u n) x = u n i x" 

605 
using mon_upclose_ex[of n "u n"] by blast 

606 
with mono_convergent_le[OF mc_u `x \<in> s`, of n i] 

607 
mono_convergent_le[OF mc_f `x \<in> s`, of i] 

608 
have "mon_upclose n (u n) x \<le> h x" by auto 

609 
ultimately 

610 
show "norm (mon_upclose n (u n) x  h x) < r" by auto 

611 
qed 

612 
qed 

613 
qed 

614 

35692  615 
lemma mono_conv_outgrow: 
616 
assumes "incseq x" "x > y" "z < y" 

617 
shows "\<exists>b. \<forall> a \<ge> b. z < x a" 

618 
using assms 

619 
proof  

620 
from assms have "y  z > 0" by simp 

621 
hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m +  y \<bar> < y  z)" using assms 

622 
unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def 

623 
by simp 

624 
have "\<forall>m. x m \<le> y" using incseq_le assms by auto 

625 
hence B: "\<forall>m. \<bar> x m +  y \<bar> = y  x m" 

626 
by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def) 

627 
from A B show ?thesis by auto 

628 
qed 

629 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
diff
changeset

630 
end 