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