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