summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Analysis/Borel_Space.thy

changeset 64284 | f3b905b2eee2 |

parent 64283 | 979cdfdf7a79 |

child 64287 | d85d88722745 |

1.1 --- a/src/HOL/Analysis/Borel_Space.thy Thu Oct 13 18:36:06 2016 +0200 1.2 +++ b/src/HOL/Analysis/Borel_Space.thy Tue Oct 18 12:01:54 2016 +0200 1.3 @@ -1974,4 +1974,189 @@ 1.4 no_notation 1.5 eucl_less (infix "<e" 50) 1.6 1.7 +lemma borel_measurable_Max2[measurable (raw)]: 1.8 + fixes f::"_ \<Rightarrow> _ \<Rightarrow> 'a::{second_countable_topology, dense_linorder, linorder_topology}" 1.9 + assumes "finite I" 1.10 + and [measurable]: "\<And>i. f i \<in> borel_measurable M" 1.11 + shows "(\<lambda>x. Max{f i x |i. i \<in> I}) \<in> borel_measurable M" 1.12 +by (simp add: borel_measurable_Max[OF assms(1), where ?f=f and ?M=M] Setcompr_eq_image) 1.13 + 1.14 +lemma measurable_compose_n [measurable (raw)]: 1.15 + assumes "T \<in> measurable M M" 1.16 + shows "(T^^n) \<in> measurable M M" 1.17 +by (induction n, auto simp add: measurable_compose[OF _ assms]) 1.18 + 1.19 +lemma measurable_real_imp_nat: 1.20 + fixes f::"'a \<Rightarrow> nat" 1.21 + assumes [measurable]: "(\<lambda>x. real(f x)) \<in> borel_measurable M" 1.22 + shows "f \<in> measurable M (count_space UNIV)" 1.23 +proof - 1.24 + let ?g = "(\<lambda>x. real(f x))" 1.25 + have "\<And>(n::nat). ?g-`({real n}) \<inter> space M = f-`{n} \<inter> space M" by auto 1.26 + moreover have "\<And>(n::nat). ?g-`({real n}) \<inter> space M \<in> sets M" using assms by measurable 1.27 + ultimately have "\<And>(n::nat). f-`{n} \<inter> space M \<in> sets M" by simp 1.28 + then show ?thesis using measurable_count_space_eq2_countable by blast 1.29 +qed 1.30 + 1.31 +lemma measurable_equality_set [measurable]: 1.32 + fixes f g::"_\<Rightarrow> 'a::{second_countable_topology, t2_space}" 1.33 + assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 1.34 + shows "{x \<in> space M. f x = g x} \<in> sets M" 1.35 + 1.36 +proof - 1.37 + define A where "A = {x \<in> space M. f x = g x}" 1.38 + define B where "B = {y. \<exists>x::'a. y = (x,x)}" 1.39 + have "A = (\<lambda>x. (f x, g x))-`B \<inter> space M" unfolding A_def B_def by auto 1.40 + moreover have "(\<lambda>x. (f x, g x)) \<in> borel_measurable M" by simp 1.41 + moreover have "B \<in> sets borel" unfolding B_def by (simp add: closed_diagonal) 1.42 + ultimately have "A \<in> sets M" by simp 1.43 + then show ?thesis unfolding A_def by simp 1.44 +qed 1.45 + 1.46 +lemma measurable_inequality_set [measurable]: 1.47 + fixes f g::"_ \<Rightarrow> 'a::{second_countable_topology, linorder_topology}" 1.48 + assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 1.49 + shows "{x \<in> space M. f x \<le> g x} \<in> sets M" 1.50 + "{x \<in> space M. f x < g x} \<in> sets M" 1.51 + "{x \<in> space M. f x \<ge> g x} \<in> sets M" 1.52 + "{x \<in> space M. f x > g x} \<in> sets M" 1.53 +proof - 1.54 + define F where "F = (\<lambda>x. (f x, g x))" 1.55 + have * [measurable]: "F \<in> borel_measurable M" unfolding F_def by simp 1.56 + 1.57 + have "{x \<in> space M. f x \<le> g x} = F-`{(x, y) | x y. x \<le> y} \<inter> space M" unfolding F_def by auto 1.58 + moreover have "{(x, y) | x y. x \<le> (y::'a)} \<in> sets borel" using closed_subdiagonal borel_closed by blast 1.59 + ultimately show "{x \<in> space M. f x \<le> g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets) 1.60 + 1.61 + have "{x \<in> space M. f x < g x} = F-`{(x, y) | x y. x < y} \<inter> space M" unfolding F_def by auto 1.62 + moreover have "{(x, y) | x y. x < (y::'a)} \<in> sets borel" using open_subdiagonal borel_open by blast 1.63 + ultimately show "{x \<in> space M. f x < g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets) 1.64 + 1.65 + have "{x \<in> space M. f x \<ge> g x} = F-`{(x, y) | x y. x \<ge> y} \<inter> space M" unfolding F_def by auto 1.66 + moreover have "{(x, y) | x y. x \<ge> (y::'a)} \<in> sets borel" using closed_superdiagonal borel_closed by blast 1.67 + ultimately show "{x \<in> space M. f x \<ge> g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets) 1.68 + 1.69 + have "{x \<in> space M. f x > g x} = F-`{(x, y) | x y. x > y} \<inter> space M" unfolding F_def by auto 1.70 + moreover have "{(x, y) | x y. x > (y::'a)} \<in> sets borel" using open_superdiagonal borel_open by blast 1.71 + ultimately show "{x \<in> space M. f x > g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets) 1.72 +qed 1.73 + 1.74 +lemma measurable_limit [measurable]: 1.75 + fixes f::"nat \<Rightarrow> 'a \<Rightarrow> 'b::first_countable_topology" 1.76 + assumes [measurable]: "\<And>n::nat. f n \<in> borel_measurable M" 1.77 + shows "Measurable.pred M (\<lambda>x. (\<lambda>n. f n x) \<longlonglongrightarrow> c)" 1.78 +proof - 1.79 + obtain A :: "nat \<Rightarrow> 'b set" where A: 1.80 + "\<And>i. open (A i)" 1.81 + "\<And>i. c \<in> A i" 1.82 + "\<And>S. open S \<Longrightarrow> c \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially" 1.83 + by (rule countable_basis_at_decseq) blast 1.84 + 1.85 + have [measurable]: "\<And>N i. (f N)-`(A i) \<inter> space M \<in> sets M" using A(1) by auto 1.86 + then have mes: "(\<Inter>i. \<Union>n. \<Inter>N\<in>{n..}. (f N)-`(A i) \<inter> space M) \<in> sets M" by blast 1.87 + 1.88 + have "(u \<longlonglongrightarrow> c) \<longleftrightarrow> (\<forall>i. eventually (\<lambda>n. u n \<in> A i) sequentially)" for u::"nat \<Rightarrow> 'b" 1.89 + proof 1.90 + assume "u \<longlonglongrightarrow> c" 1.91 + then have "eventually (\<lambda>n. u n \<in> A i) sequentially" for i using A(1)[of i] A(2)[of i] 1.92 + by (simp add: topological_tendstoD) 1.93 + then show "(\<forall>i. eventually (\<lambda>n. u n \<in> A i) sequentially)" by auto 1.94 + next 1.95 + assume H: "(\<forall>i. eventually (\<lambda>n. u n \<in> A i) sequentially)" 1.96 + show "(u \<longlonglongrightarrow> c)" 1.97 + proof (rule topological_tendstoI) 1.98 + fix S assume "open S" "c \<in> S" 1.99 + with A(3)[OF this] obtain i where "A i \<subseteq> S" 1.100 + using eventually_False_sequentially eventually_mono by blast 1.101 + moreover have "eventually (\<lambda>n. u n \<in> A i) sequentially" using H by simp 1.102 + ultimately show "\<forall>\<^sub>F n in sequentially. u n \<in> S" 1.103 + by (simp add: eventually_mono subset_eq) 1.104 + qed 1.105 + qed 1.106 + then have "{x. (\<lambda>n. f n x) \<longlonglongrightarrow> c} = (\<Inter>i. \<Union>n. \<Inter>N\<in>{n..}. (f N)-`(A i))" 1.107 + by (auto simp add: atLeast_def eventually_at_top_linorder) 1.108 + then have "{x \<in> space M. (\<lambda>n. f n x) \<longlonglongrightarrow> c} = (\<Inter>i. \<Union>n. \<Inter>N\<in>{n..}. (f N)-`(A i) \<inter> space M)" 1.109 + by auto 1.110 + then have "{x \<in> space M. (\<lambda>n. f n x) \<longlonglongrightarrow> c} \<in> sets M" using mes by simp 1.111 + then show ?thesis by auto 1.112 +qed 1.113 + 1.114 +lemma measurable_limit2 [measurable]: 1.115 + fixes u::"nat \<Rightarrow> 'a \<Rightarrow> real" 1.116 + assumes [measurable]: "\<And>n. u n \<in> borel_measurable M" "v \<in> borel_measurable M" 1.117 + shows "Measurable.pred M (\<lambda>x. (\<lambda>n. u n x) \<longlonglongrightarrow> v x)" 1.118 +proof - 1.119 + define w where "w = (\<lambda>n x. u n x - v x)" 1.120 + have [measurable]: "w n \<in> borel_measurable M" for n unfolding w_def by auto 1.121 + have "((\<lambda>n. u n x) \<longlonglongrightarrow> v x) \<longleftrightarrow> ((\<lambda>n. w n x) \<longlonglongrightarrow> 0)" for x 1.122 + unfolding w_def using Lim_null by auto 1.123 + then show ?thesis using measurable_limit by auto 1.124 +qed 1.125 + 1.126 +lemma measurable_P_restriction [measurable (raw)]: 1.127 + assumes [measurable]: "Measurable.pred M P" "A \<in> sets M" 1.128 + shows "{x \<in> A. P x} \<in> sets M" 1.129 +proof - 1.130 + have "A \<subseteq> space M" using sets.sets_into_space[OF assms(2)]. 1.131 + then have "{x \<in> A. P x} = A \<inter> {x \<in> space M. P x}" by blast 1.132 + then show ?thesis by auto 1.133 +qed 1.134 + 1.135 +lemma measurable_sum_nat [measurable (raw)]: 1.136 + fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> nat" 1.137 + assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> measurable M (count_space UNIV)" 1.138 + shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> measurable M (count_space UNIV)" 1.139 +proof cases 1.140 + assume "finite S" 1.141 + then show ?thesis using assms by induct auto 1.142 +qed simp 1.143 + 1.144 + 1.145 +lemma measurable_abs_powr [measurable]: 1.146 + fixes p::real 1.147 + assumes [measurable]: "f \<in> borel_measurable M" 1.148 + shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M" 1.149 +unfolding powr_def by auto 1.150 + 1.151 +text {* The next one is a variation around \verb+measurable_restrict_space+.*} 1.152 + 1.153 +lemma measurable_restrict_space3: 1.154 + assumes "f \<in> measurable M N" and 1.155 + "f \<in> A \<rightarrow> B" 1.156 + shows "f \<in> measurable (restrict_space M A) (restrict_space N B)" 1.157 +proof - 1.158 + have "f \<in> measurable (restrict_space M A) N" using assms(1) measurable_restrict_space1 by auto 1.159 + then show ?thesis by (metis Int_iff funcsetI funcset_mem 1.160 + measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space) 1.161 +qed 1.162 + 1.163 +text {* The next one is a variation around \verb+measurable_piecewise_restrict+.*} 1.164 + 1.165 +lemma measurable_piecewise_restrict2: 1.166 + assumes [measurable]: "\<And>n. A n \<in> sets M" 1.167 + and "space M = (\<Union>(n::nat). A n)" 1.168 + "\<And>n. \<exists>h \<in> measurable M N. (\<forall>x \<in> A n. f x = h x)" 1.169 + shows "f \<in> measurable M N" 1.170 +proof (rule measurableI) 1.171 + fix B assume [measurable]: "B \<in> sets N" 1.172 + { 1.173 + fix n::nat 1.174 + obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast 1.175 + then have *: "f-`B \<inter> A n = h-`B \<inter> A n" by auto 1.176 + have "h-`B \<inter> A n = h-`B \<inter> space M \<inter> A n" using assms(2) sets.sets_into_space by auto 1.177 + then have "h-`B \<inter> A n \<in> sets M" by simp 1.178 + then have "f-`B \<inter> A n \<in> sets M" using * by simp 1.179 + } 1.180 + then have "(\<Union>n. f-`B \<inter> A n) \<in> sets M" by measurable 1.181 + moreover have "f-`B \<inter> space M = (\<Union>n. f-`B \<inter> A n)" using assms(2) by blast 1.182 + ultimately show "f-`B \<inter> space M \<in> sets M" by simp 1.183 +next 1.184 + fix x assume "x \<in> space M" 1.185 + then obtain n where "x \<in> A n" using assms(2) by blast 1.186 + obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast 1.187 + then have "f x = h x" using `x \<in> A n` by blast 1.188 + moreover have "h x \<in> space N" by (metis measurable_space `x \<in> space M` `h \<in> measurable M N`) 1.189 + ultimately show "f x \<in> space N" by simp 1.190 +qed 1.191 + 1.192 end