50530

1 
(* Title: HOL/Probability/Measurable.thy

50387

2 
Author: Johannes Hölzl <hoelzl@in.tum.de>


3 
*)


4 
theory Measurable


5 
imports Sigma_Algebra


6 
begin


7 


8 
subsection {* Measurability prover *}


9 


10 
lemma (in algebra) sets_Collect_finite_All:


11 
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"


12 
shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"


13 
proof 


14 
have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"


15 
by auto


16 
with assms show ?thesis by (auto intro!: sets_Collect_finite_All')


17 
qed


18 


19 
abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"


20 


21 
lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"


22 
proof


23 
assume "pred M P"


24 
then have "P ` {True} \<inter> space M \<in> sets M"


25 
by (auto simp: measurable_count_space_eq2)


26 
also have "P ` {True} \<inter> space M = {x\<in>space M. P x}" by auto


27 
finally show "{x\<in>space M. P x} \<in> sets M" .


28 
next


29 
assume P: "{x\<in>space M. P x} \<in> sets M"


30 
moreover


31 
{ fix X


32 
have "X \<in> Pow (UNIV :: bool set)" by simp


33 
then have "P ` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"


34 
unfolding UNIV_bool Pow_insert Pow_empty by auto


35 
then have "P ` X \<inter> space M \<in> sets M"


36 
by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }


37 
then show "pred M P"


38 
by (auto simp: measurable_def)


39 
qed


40 


41 
lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"


42 
by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)


43 


44 
lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"


45 
by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])


46 


47 
ML_file "measurable.ML"


48 


49 
attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"


50 
attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"


51 
attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"


52 
method_setup measurable = {* Measurable.method *} "measurability prover"


53 
simproc_setup measurable ("A \<in> sets M"  "f \<in> measurable M N") = {* K Measurable.simproc *}


54 


55 
declare


56 
measurable_compose_rev[measurable_dest]


57 
pred_sets1[measurable_dest]


58 
pred_sets2[measurable_dest]


59 
sets.sets_into_space[measurable_dest]


60 


61 
declare


62 
sets.top[measurable]


63 
sets.empty_sets[measurable (raw)]


64 
sets.Un[measurable (raw)]


65 
sets.Diff[measurable (raw)]


66 


67 
declare


68 
measurable_count_space[measurable (raw)]


69 
measurable_ident[measurable (raw)]


70 
measurable_ident_sets[measurable (raw)]


71 
measurable_const[measurable (raw)]


72 
measurable_If[measurable (raw)]


73 
measurable_comp[measurable (raw)]


74 
measurable_sets[measurable (raw)]


75 


76 
lemma predE[measurable (raw)]:


77 
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"


78 
unfolding pred_def .


79 


80 
lemma pred_intros_imp'[measurable (raw)]:


81 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"


82 
by (cases K) auto


83 


84 
lemma pred_intros_conj1'[measurable (raw)]:


85 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"


86 
by (cases K) auto


87 


88 
lemma pred_intros_conj2'[measurable (raw)]:


89 
"(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"


90 
by (cases K) auto


91 


92 
lemma pred_intros_disj1'[measurable (raw)]:


93 
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"


94 
by (cases K) auto


95 


96 
lemma pred_intros_disj2'[measurable (raw)]:


97 
"(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"


98 
by (cases K) auto


99 


100 
lemma pred_intros_logic[measurable (raw)]:


101 
"pred M (\<lambda>x. x \<in> space M)"


102 
"pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"


103 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"


104 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"


105 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"


106 
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"


107 
"pred M (\<lambda>x. f x \<in> UNIV)"


108 
"pred M (\<lambda>x. f x \<in> {})"


109 
"pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"


110 
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in>  (B x))"


111 
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x)  (B x))"


112 
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"


113 
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"


114 
"pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) ` (X x))"


115 
by (auto simp: iff_conv_conj_imp pred_def)


116 


117 
lemma pred_intros_countable[measurable (raw)]:


118 
fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"


119 
shows


120 
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"


121 
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"


122 
by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)


123 


124 
lemma pred_intros_countable_bounded[measurable (raw)]:


125 
fixes X :: "'i :: countable set"


126 
shows


127 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"


128 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"


129 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"


130 
"(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"


131 
by (auto simp: Bex_def Ball_def)


132 


133 
lemma pred_intros_finite[measurable (raw)]:


134 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"


135 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"


136 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"


137 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"


138 
by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)


139 


140 
lemma countable_Un_Int[measurable (raw)]:


141 
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"


142 
"I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"


143 
by auto


144 


145 
declare


146 
finite_UN[measurable (raw)]


147 
finite_INT[measurable (raw)]


148 


149 
lemma sets_Int_pred[measurable (raw)]:


150 
assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"


151 
shows "A \<inter> B \<in> sets M"


152 
proof 


153 
have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto


154 
also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"


155 
using space by auto


156 
finally show ?thesis .


157 
qed


158 


159 
lemma [measurable (raw generic)]:


160 
assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"


161 
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"


162 
and pred_eq_const2: "pred M (\<lambda>x. c = f x)"


163 
proof 


164 
show "pred M (\<lambda>x. f x = c)"


165 
proof cases


166 
assume "c \<in> space N"


167 
with measurable_sets[OF f c] show ?thesis


168 
by (auto simp: Int_def conj_commute pred_def)


169 
next


170 
assume "c \<notin> space N"


171 
with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto


172 
then show ?thesis by (auto simp: pred_def cong: conj_cong)


173 
qed


174 
then show "pred M (\<lambda>x. c = f x)"


175 
by (simp add: eq_commute)


176 
qed


177 


178 
lemma pred_le_const[measurable (raw generic)]:


179 
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"


180 
using measurable_sets[OF f c]


181 
by (auto simp: Int_def conj_commute eq_commute pred_def)


182 


183 
lemma pred_const_le[measurable (raw generic)]:


184 
assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"


185 
using measurable_sets[OF f c]


186 
by (auto simp: Int_def conj_commute eq_commute pred_def)


187 


188 
lemma pred_less_const[measurable (raw generic)]:


189 
assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"


190 
using measurable_sets[OF f c]


191 
by (auto simp: Int_def conj_commute eq_commute pred_def)


192 


193 
lemma pred_const_less[measurable (raw generic)]:


194 
assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"


195 
using measurable_sets[OF f c]


196 
by (auto simp: Int_def conj_commute eq_commute pred_def)


197 


198 
declare


199 
sets.Int[measurable (raw)]


200 


201 
lemma pred_in_If[measurable (raw)]:


202 
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>


203 
pred M (\<lambda>x. x \<in> (if P then A x else B x))"


204 
by auto


205 


206 
lemma sets_range[measurable_dest]:


207 
"A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"


208 
by auto


209 


210 
lemma pred_sets_range[measurable_dest]:


211 
"A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"


212 
using pred_sets2[OF sets_range] by auto


213 


214 
lemma sets_All[measurable_dest]:


215 
"\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"


216 
by auto


217 


218 
lemma pred_sets_All[measurable_dest]:


219 
"\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"


220 
using pred_sets2[OF sets_All, of A N f] by auto


221 


222 
lemma sets_Ball[measurable_dest]:


223 
"\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"


224 
by auto


225 


226 
lemma pred_sets_Ball[measurable_dest]:


227 
"\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"


228 
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto


229 


230 
lemma measurable_finite[measurable (raw)]:


231 
fixes S :: "'a \<Rightarrow> nat set"


232 
assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"


233 
shows "pred M (\<lambda>x. finite (S x))"


234 
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)


235 


236 
lemma measurable_Least[measurable]:


237 
assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q


238 
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"


239 
unfolding measurable_def by (safe intro!: sets_Least) simp_all


240 


241 
lemma measurable_count_space_insert[measurable (raw)]:


242 
"s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"


243 
by simp


244 


245 
hide_const (open) pred


246 


247 
end
