src/HOL/Analysis/Measure_Space.thy
changeset 64283 979cdfdf7a79
parent 64267 b9a1486e79be
child 64320 ba194424b895
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Mon Oct 17 15:20:06 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Oct 13 18:36:06 2016 +0200
     1.3 @@ -1059,6 +1059,11 @@
     1.4    with AE_iff_null[of M P] assms show ?thesis by auto
     1.5  qed
     1.6  
     1.7 +lemma AE_E3:
     1.8 +  assumes "AE x in M. P x"
     1.9 +  obtains N where "\<And>x. x \<in> space M - N \<Longrightarrow> P x" "N \<in> null_sets M"
    1.10 +using assms unfolding eventually_ae_filter by auto
    1.11 +
    1.12  lemma AE_I:
    1.13    assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
    1.14    shows "AE x in M. P x"
    1.15 @@ -1087,6 +1092,10 @@
    1.16    qed
    1.17  qed
    1.18  
    1.19 +text {*The next lemma is convenient to combine with a lemma whose conclusion is of the
    1.20 +form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \verb+[symmetric]+ variant,
    1.21 +but using \<open>AE_symmetric[OF...]\<close> will replace it.*}
    1.22 +
    1.23  (* depricated replace by laws about eventually *)
    1.24  lemma
    1.25    shows AE_iffI: "AE x in M. P x \<Longrightarrow> AE x in M. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x in M. Q x"
    1.26 @@ -1096,6 +1105,11 @@
    1.27      and AE_conj_iff[simp]: "(AE x in M. P x \<and> Q x) \<longleftrightarrow> (AE x in M. P x) \<and> (AE x in M. Q x)"
    1.28    by auto
    1.29  
    1.30 +lemma AE_symmetric:
    1.31 +  assumes "AE x in M. P x = Q x"
    1.32 +  shows "AE x in M. Q x = P x"
    1.33 +  using assms by auto
    1.34 +
    1.35  lemma AE_impI:
    1.36    "(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x"
    1.37    by (cases P) auto
    1.38 @@ -1166,6 +1180,10 @@
    1.39      unfolding eventually_ae_filter by auto
    1.40  qed auto
    1.41  
    1.42 +lemma AE_ball_countable':
    1.43 +  "(\<And>N. N \<in> I \<Longrightarrow> AE x in M. P N x) \<Longrightarrow> countable I \<Longrightarrow> AE x in M. \<forall>N \<in> I. P N x"
    1.44 +  unfolding AE_ball_countable by simp
    1.45 +
    1.46  lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
    1.47    by (auto simp add: pairwise_def)
    1.48  
    1.49 @@ -1225,6 +1243,11 @@
    1.50    using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"]
    1.51    by (cases "{x\<in>space M. P x} \<in> sets M") (simp_all add: emeasure_notin_sets)
    1.52  
    1.53 +lemma emeasure_0_AE:
    1.54 +  assumes "emeasure M (space M) = 0"
    1.55 +  shows "AE x in M. P x"
    1.56 +using eventually_ae_filter assms by blast
    1.57 +
    1.58  lemma emeasure_add_AE:
    1.59    assumes [measurable]: "A \<in> sets M" "B \<in> sets M" "C \<in> sets M"
    1.60    assumes 1: "AE x in M. x \<in> C \<longleftrightarrow> x \<in> A \<or> x \<in> B"
    1.61 @@ -1328,6 +1351,40 @@
    1.62    qed
    1.63  qed
    1.64  
    1.65 +lemma (in sigma_finite_measure) approx_PInf_emeasure_with_finite:
    1.66 +  fixes C::real
    1.67 +  assumes W_meas: "W \<in> sets M"
    1.68 +      and W_inf: "emeasure M W = \<infinity>"
    1.69 +  obtains Z where "Z \<in> sets M" "Z \<subseteq> W" "emeasure M Z < \<infinity>" "emeasure M Z > C"
    1.70 +proof -
    1.71 +  obtain A :: "nat \<Rightarrow> 'a set"
    1.72 +    where A: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
    1.73 +    using sigma_finite_incseq by blast
    1.74 +  define B where "B = (\<lambda>i. W \<inter> A i)"
    1.75 +  have B_meas: "\<And>i. B i \<in> sets M" using W_meas `range A \<subseteq> sets M` B_def by blast
    1.76 +  have b: "\<And>i. B i \<subseteq> W" using B_def by blast
    1.77 +
    1.78 +  { fix i
    1.79 +    have "emeasure M (B i) \<le> emeasure M (A i)"
    1.80 +      using A by (intro emeasure_mono) (auto simp: B_def)
    1.81 +    also have "emeasure M (A i) < \<infinity>"
    1.82 +      using `\<And>i. emeasure M (A i) \<noteq> \<infinity>` by (simp add: less_top)
    1.83 +    finally have "emeasure M (B i) < \<infinity>" . }
    1.84 +  note c = this
    1.85 +
    1.86 +  have "W = (\<Union>i. B i)" using B_def `(\<Union>i. A i) = space M` W_meas by auto
    1.87 +  moreover have "incseq B" using B_def `incseq A` by (simp add: incseq_def subset_eq)
    1.88 +  ultimately have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> emeasure M W" using W_meas B_meas
    1.89 +    by (simp add: B_meas Lim_emeasure_incseq image_subset_iff)
    1.90 +  then have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> \<infinity>" using W_inf by simp
    1.91 +  from order_tendstoD(1)[OF this, of C]
    1.92 +  obtain i where d: "emeasure M (B i) > C"
    1.93 +    by (auto simp: eventually_sequentially)
    1.94 +  have "B i \<in> sets M" "B i \<subseteq> W" "emeasure M (B i) < \<infinity>" "emeasure M (B i) > C"
    1.95 +    using B_meas b c d by auto
    1.96 +  then show ?thesis using that by blast
    1.97 +qed
    1.98 +
    1.99  subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
   1.100  
   1.101  definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
   1.102 @@ -1824,6 +1881,88 @@
   1.103    then show ?fm ?m by auto
   1.104  qed
   1.105  
   1.106 +lemma suminf_exist_split2:
   1.107 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.108 +  assumes "summable f"
   1.109 +  shows "(\<lambda>n. (\<Sum>k. f(k+n))) \<longlonglongrightarrow> 0"
   1.110 +by (subst lim_sequentially, auto simp add: dist_norm suminf_exist_split[OF _ assms])
   1.111 +
   1.112 +lemma emeasure_union_summable:
   1.113 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
   1.114 +    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
   1.115 +  shows "emeasure M (\<Union>n. A n) < \<infinity>" "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
   1.116 +proof -
   1.117 +  define B where "B = (\<lambda>N. (\<Union>n\<in>{..<N}. A n))"
   1.118 +  have [measurable]: "B N \<in> sets M" for N unfolding B_def by auto
   1.119 +  have "(\<lambda>N. emeasure M (B N)) \<longlonglongrightarrow> emeasure M (\<Union>N. B N)"
   1.120 +    apply (rule Lim_emeasure_incseq) unfolding B_def by (auto simp add: SUP_subset_mono incseq_def)
   1.121 +  moreover have "emeasure M (B N) \<le> ennreal (\<Sum>n. measure M (A n))" for N
   1.122 +  proof -
   1.123 +    have *: "(\<Sum>n\<in>{..<N}. measure M (A n)) \<le> (\<Sum>n. measure M (A n))"
   1.124 +      using assms(3) measure_nonneg sum_le_suminf by blast
   1.125 +
   1.126 +    have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
   1.127 +      unfolding B_def by (rule emeasure_subadditive_finite, auto)
   1.128 +    also have "... = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
   1.129 +      using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
   1.130 +    also have "... = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
   1.131 +      by auto
   1.132 +    also have "... \<le> ennreal (\<Sum>n. measure M (A n))"
   1.133 +      using * by (auto simp: ennreal_leI)
   1.134 +    finally show ?thesis by simp
   1.135 +  qed
   1.136 +  ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
   1.137 +    by (simp add: Lim_bounded_ereal)
   1.138 +  then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
   1.139 +    unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
   1.140 +  then show "emeasure M (\<Union>n. A n) < \<infinity>"
   1.141 +    by (auto simp: less_top[symmetric] top_unique)
   1.142 +qed
   1.143 +
   1.144 +lemma borel_cantelli_limsup1:
   1.145 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
   1.146 +    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
   1.147 +  shows "limsup A \<in> null_sets M"
   1.148 +proof -
   1.149 +  have "emeasure M (limsup A) \<le> 0"
   1.150 +  proof (rule LIMSEQ_le_const)
   1.151 +    have "(\<lambda>n. (\<Sum>k. measure M (A (k+n)))) \<longlonglongrightarrow> 0" by (rule suminf_exist_split2[OF assms(3)])
   1.152 +    then show "(\<lambda>n. ennreal (\<Sum>k. measure M (A (k+n)))) \<longlonglongrightarrow> 0"
   1.153 +      unfolding ennreal_0[symmetric] by (intro tendsto_ennrealI)
   1.154 +    have "emeasure M (limsup A) \<le> (\<Sum>k. measure M (A (k+n)))" for n
   1.155 +    proof -
   1.156 +      have I: "(\<Union>k\<in>{n..}. A k) = (\<Union>k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce)
   1.157 +      have "emeasure M (limsup A) \<le> emeasure M (\<Union>k\<in>{n..}. A k)"
   1.158 +        by (rule emeasure_mono, auto simp add: limsup_INF_SUP)
   1.159 +      also have "... = emeasure M (\<Union>k. A (k+n))"
   1.160 +        using I by auto
   1.161 +      also have "... \<le> (\<Sum>k. measure M (A (k+n)))"
   1.162 +        apply (rule emeasure_union_summable)
   1.163 +        using assms summable_ignore_initial_segment[OF assms(3), of n] by auto
   1.164 +      finally show ?thesis by simp
   1.165 +    qed
   1.166 +    then show "\<exists>N. \<forall>n\<ge>N. emeasure M (limsup A) \<le> (\<Sum>k. measure M (A (k+n)))"
   1.167 +      by auto
   1.168 +  qed
   1.169 +  then show ?thesis using assms(1) measurable_limsup by auto
   1.170 +qed
   1.171 +
   1.172 +lemma borel_cantelli_AE1:
   1.173 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
   1.174 +    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
   1.175 +  shows "AE x in M. eventually (\<lambda>n. x \<in> space M - A n) sequentially"
   1.176 +proof -
   1.177 +  have "AE x in M. x \<notin> limsup A"
   1.178 +    using borel_cantelli_limsup1[OF assms] unfolding eventually_ae_filter by auto
   1.179 +  moreover
   1.180 +  {
   1.181 +    fix x assume "x \<notin> limsup A"
   1.182 +    then obtain N where "x \<notin> (\<Union>n\<in>{N..}. A n)" unfolding limsup_INF_SUP by blast
   1.183 +    then have "eventually (\<lambda>n. x \<notin> A n) sequentially" using eventually_sequentially by auto
   1.184 +  }
   1.185 +  ultimately show ?thesis by auto
   1.186 +qed
   1.187 +
   1.188  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
   1.189  
   1.190  locale finite_measure = sigma_finite_measure M for M +