src/HOL/Probability/Measure_Space.thy
changeset 49773 16907431e477
parent 47762 d31085f07f60
child 49784 5e5b2da42a69
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:14 2012 +0200
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:15 2012 +0200
     1.3 @@ -12,6 +12,12 @@
     1.4    "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
     1.5  begin
     1.6  
     1.7 +lemma sums_def2:
     1.8 +  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
     1.9 +  unfolding sums_def
    1.10 +  apply (subst LIMSEQ_Suc_iff[symmetric])
    1.11 +  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    1.12 +
    1.13  lemma suminf_cmult_indicator:
    1.14    fixes f :: "nat \<Rightarrow> ereal"
    1.15    assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
    1.16 @@ -90,6 +96,9 @@
    1.17  definition increasing where
    1.18    "increasing M \<mu> \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<subseteq> y \<longrightarrow> \<mu> x \<le> \<mu> y)"
    1.19  
    1.20 +lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
    1.21 +lemma positiveD2: "positive M f \<Longrightarrow> A \<in> M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
    1.22 +
    1.23  lemma positiveD_empty:
    1.24    "positive M f \<Longrightarrow> f {} = 0"
    1.25    by (auto simp add: positive_def)
    1.26 @@ -240,6 +249,143 @@
    1.27    finally show "(\<Sum>i. \<mu> (F i)) = \<mu> (\<Union>i. F i)" .
    1.28  qed
    1.29  
    1.30 +lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
    1.31 +  assumes f: "positive M f" "additive M f"
    1.32 +  shows "countably_additive M f \<longleftrightarrow>
    1.33 +    (\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i))"
    1.34 +  unfolding countably_additive_def
    1.35 +proof safe
    1.36 +  assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
    1.37 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
    1.38 +  then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
    1.39 +  with count_sum[THEN spec, of "disjointed A"] A(3)
    1.40 +  have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
    1.41 +    by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
    1.42 +  moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    1.43 +    using f(1)[unfolded positive_def] dA
    1.44 +    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_ereal_pos)
    1.45 +  from LIMSEQ_Suc[OF this]
    1.46 +  have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    1.47 +    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
    1.48 +  moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
    1.49 +    using disjointed_additive[OF f A(1,2)] .
    1.50 +  ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
    1.51 +next
    1.52 +  assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
    1.53 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
    1.54 +  have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
    1.55 +  have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
    1.56 +  proof (unfold *[symmetric], intro cont[rule_format])
    1.57 +    show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> M"
    1.58 +      using A * by auto
    1.59 +  qed (force intro!: incseq_SucI)
    1.60 +  moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
    1.61 +    using A
    1.62 +    by (intro additive_sum[OF f, of _ A, symmetric])
    1.63 +       (auto intro: disjoint_family_on_mono[where B=UNIV])
    1.64 +  ultimately
    1.65 +  have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
    1.66 +    unfolding sums_def2 by simp
    1.67 +  from sums_unique[OF this]
    1.68 +  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
    1.69 +qed
    1.70 +
    1.71 +lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
    1.72 +  assumes f: "positive M f" "additive M f"
    1.73 +  shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))
    1.74 +     \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0)"
    1.75 +proof safe
    1.76 +  assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))"
    1.77 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
    1.78 +  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
    1.79 +    using `positive M f`[unfolded positive_def] by auto
    1.80 +next
    1.81 +  assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
    1.82 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
    1.83 +
    1.84 +  have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
    1.85 +    using additive_increasing[OF f] unfolding increasing_def by simp
    1.86 +
    1.87 +  have decseq_fA: "decseq (\<lambda>i. f (A i))"
    1.88 +    using A by (auto simp: decseq_def intro!: f_mono)
    1.89 +  have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
    1.90 +    using A by (auto simp: decseq_def)
    1.91 +  then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
    1.92 +    using A unfolding decseq_def by (auto intro!: f_mono Diff)
    1.93 +  have "f (\<Inter>x. A x) \<le> f (A 0)"
    1.94 +    using A by (auto intro!: f_mono)
    1.95 +  then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
    1.96 +    using A by auto
    1.97 +  { fix i
    1.98 +    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
    1.99 +    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
   1.100 +      using A by auto }
   1.101 +  note f_fin = this
   1.102 +  have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
   1.103 +  proof (intro cont[rule_format, OF _ decseq _ f_fin])
   1.104 +    show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
   1.105 +      using A by auto
   1.106 +  qed
   1.107 +  from INF_Lim_ereal[OF decseq_f this]
   1.108 +  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
   1.109 +  moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
   1.110 +    by auto
   1.111 +  ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
   1.112 +    using A(4) f_fin f_Int_fin
   1.113 +    by (subst INFI_ereal_add) (auto simp: decseq_f)
   1.114 +  moreover {
   1.115 +    fix n
   1.116 +    have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
   1.117 +      using A by (subst f(2)[THEN additiveD]) auto
   1.118 +    also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
   1.119 +      by auto
   1.120 +    finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
   1.121 +  ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
   1.122 +    by simp
   1.123 +  with LIMSEQ_ereal_INFI[OF decseq_fA]
   1.124 +  show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
   1.125 +qed
   1.126 +
   1.127 +lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
   1.128 +  assumes f: "positive M f" "additive M f" "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   1.129 +  assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.130 +  assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
   1.131 +  shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   1.132 +proof -
   1.133 +  have "\<forall>A\<in>M. \<exists>x. f A = ereal x"
   1.134 +  proof
   1.135 +    fix A assume "A \<in> M" with f show "\<exists>x. f A = ereal x"
   1.136 +      unfolding positive_def by (cases "f A") auto
   1.137 +  qed
   1.138 +  from bchoice[OF this] guess f' .. note f' = this[rule_format]
   1.139 +  from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
   1.140 +    by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
   1.141 +  moreover
   1.142 +  { fix i
   1.143 +    have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
   1.144 +      using A by (intro f(2)[THEN additiveD, symmetric]) auto
   1.145 +    also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
   1.146 +      by auto
   1.147 +    finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
   1.148 +      using A by (subst (asm) (1 2 3) f') auto
   1.149 +    then have "f ((\<Union>i. A i) - A i) = ereal (f' (\<Union>i. A i) - f' (A i))"
   1.150 +      using A f' by auto }
   1.151 +  ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
   1.152 +    by (simp add: zero_ereal_def)
   1.153 +  then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
   1.154 +    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
   1.155 +  then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   1.156 +    using A by (subst (1 2) f') auto
   1.157 +qed
   1.158 +
   1.159 +lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
   1.160 +  assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   1.161 +  assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.162 +  shows "countably_additive M f"
   1.163 +  using countably_additive_iff_continuous_from_below[OF f]
   1.164 +  using empty_continuous_imp_continuous_from_below[OF f fin] cont
   1.165 +  by blast
   1.166 +
   1.167  section {* Properties of @{const emeasure} *}
   1.168  
   1.169  lemma emeasure_positive: "positive (sets M) (emeasure M)"
   1.170 @@ -314,84 +460,21 @@
   1.171      using finite `0 \<le> emeasure M B` by auto
   1.172  qed
   1.173  
   1.174 -lemma emeasure_countable_increasing:
   1.175 -  assumes A: "range A \<subseteq> sets M"
   1.176 -      and A0: "A 0 = {}"
   1.177 -      and ASuc: "\<And>n. A n \<subseteq> A (Suc n)"
   1.178 -  shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   1.179 -proof -
   1.180 -  { fix n
   1.181 -    have "emeasure M (A n) = (\<Sum>i<n. emeasure M (A (Suc i) - A i))"
   1.182 -      proof (induct n)
   1.183 -        case 0 thus ?case by (auto simp add: A0)
   1.184 -      next
   1.185 -        case (Suc m)
   1.186 -        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
   1.187 -          by (metis ASuc Un_Diff_cancel Un_absorb1)
   1.188 -        hence "emeasure M (A (Suc m)) =
   1.189 -               emeasure M (A m) + emeasure M (A (Suc m) - A m)"
   1.190 -          by (subst plus_emeasure)
   1.191 -             (auto simp add: emeasure_additive range_subsetD [OF A])
   1.192 -        with Suc show ?case
   1.193 -          by simp
   1.194 -      qed }
   1.195 -  note Meq = this
   1.196 -  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
   1.197 -    proof (rule UN_finite2_eq [where k=1], simp)
   1.198 -      fix i
   1.199 -      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
   1.200 -        proof (induct i)
   1.201 -          case 0 thus ?case by (simp add: A0)
   1.202 -        next
   1.203 -          case (Suc i)
   1.204 -          thus ?case
   1.205 -            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
   1.206 -        qed
   1.207 -    qed
   1.208 -  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
   1.209 -    by (metis A Diff range_subsetD)
   1.210 -  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
   1.211 -    by (blast intro: range_subsetD [OF A])
   1.212 -  have "(SUP n. \<Sum>i<n. emeasure M (A (Suc i) - A i)) = (\<Sum>i. emeasure M (A (Suc i) - A i))"
   1.213 -    using A by (auto intro!: suminf_ereal_eq_SUPR[symmetric])
   1.214 -  also have "\<dots> = emeasure M (\<Union>i. A (Suc i) - A i)"
   1.215 -    by (rule suminf_emeasure)
   1.216 -       (auto simp add: disjoint_family_Suc ASuc A1 A2)
   1.217 -  also have "... =  emeasure M (\<Union>i. A i)"
   1.218 -    by (simp add: Aeq)
   1.219 -  finally have "(SUP n. \<Sum>i<n. emeasure M (A (Suc i) - A i)) = emeasure M (\<Union>i. A i)" .
   1.220 -  then show ?thesis by (auto simp add: Meq)
   1.221 -qed
   1.222 -
   1.223 -lemma SUP_emeasure_incseq:
   1.224 -  assumes A: "range A \<subseteq> sets M" and "incseq A"
   1.225 -  shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   1.226 -proof -
   1.227 -  have *: "(SUP n. emeasure M (nat_case {} A (Suc n))) = (SUP n. emeasure M (nat_case {} A n))"
   1.228 -    using A by (auto intro!: SUPR_eq exI split: nat.split)
   1.229 -  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
   1.230 -    by (auto simp add: split: nat.splits)
   1.231 -  have meq: "\<And>n. emeasure M (A n) = (emeasure M \<circ> nat_case {} A) (Suc n)"
   1.232 -    by simp
   1.233 -  have "(SUP n. emeasure M (nat_case {} A n)) = emeasure M (\<Union>i. nat_case {} A i)"
   1.234 -    using range_subsetD[OF A] incseq_SucD[OF `incseq A`]
   1.235 -    by (force split: nat.splits intro!: emeasure_countable_increasing)
   1.236 -  also have "emeasure M (\<Union>i. nat_case {} A i) = emeasure M (\<Union>i. A i)"
   1.237 -    by (simp add: ueq)
   1.238 -  finally have "(SUP n. emeasure M (nat_case {} A n)) = emeasure M (\<Union>i. A i)" .
   1.239 -  thus ?thesis unfolding meq * comp_def .
   1.240 -qed
   1.241 +lemma Lim_emeasure_incseq:
   1.242 +  "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   1.243 +  using emeasure_countably_additive
   1.244 +  by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive)
   1.245  
   1.246  lemma incseq_emeasure:
   1.247    assumes "range B \<subseteq> sets M" "incseq B"
   1.248    shows "incseq (\<lambda>i. emeasure M (B i))"
   1.249    using assms by (auto simp: incseq_def intro!: emeasure_mono)
   1.250  
   1.251 -lemma Lim_emeasure_incseq:
   1.252 +lemma SUP_emeasure_incseq:
   1.253    assumes A: "range A \<subseteq> sets M" "incseq A"
   1.254 -  shows "(\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   1.255 -  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A]
   1.256 -    SUP_emeasure_incseq[OF A] by simp
   1.257 +  shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   1.258 +  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
   1.259 +  by (simp add: LIMSEQ_unique)
   1.260  
   1.261  lemma decseq_emeasure:
   1.262    assumes "range B \<subseteq> sets M" "decseq B"
   1.263 @@ -548,66 +631,66 @@
   1.264    and A: "range A \<subseteq> E" "incseq A" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   1.265    shows "M = N"
   1.266  proof -
   1.267 -  let ?D = "\<lambda>F. {D. D \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)}"
   1.268 +  let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
   1.269    interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
   1.270 -  { fix F assume "F \<in> E" and "emeasure M F \<noteq> \<infinity>"
   1.271 +  { fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
   1.272      then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
   1.273 -    have "emeasure N F \<noteq> \<infinity>" using `emeasure M F \<noteq> \<infinity>` `F \<in> E` eq by simp
   1.274 -    interpret D: dynkin_system \<Omega> "?D F"
   1.275 +    let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}"
   1.276 +    have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
   1.277 +    interpret D: dynkin_system \<Omega> ?D
   1.278      proof (rule dynkin_systemI, simp_all)
   1.279 -      fix A assume "A \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> A) = emeasure N (F \<inter> A)"
   1.280 +      fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
   1.281        then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto
   1.282      next
   1.283        have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto
   1.284 -      then show "emeasure M (F \<inter> \<Omega>) = emeasure N (F \<inter> \<Omega>)"
   1.285 +      then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)"
   1.286          using `F \<in> E` eq by (auto intro: sigma_sets_top)
   1.287      next
   1.288 -      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> A) = emeasure N (F \<inter> A)"
   1.289 +      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
   1.290        then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
   1.291          and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
   1.292          using `F \<in> E` S.sets_into_space by auto
   1.293 -      have "emeasure N (F \<inter> A) \<le> emeasure N F" by (auto intro!: emeasure_mono simp: M N)
   1.294 -      then have "emeasure N (F \<inter> A) \<noteq> \<infinity>" using `emeasure N F \<noteq> \<infinity>` by auto
   1.295 -      have "emeasure M (F \<inter> A) \<le> emeasure M F" by (auto intro!: emeasure_mono simp: M N)
   1.296 -      then have "emeasure M (F \<inter> A) \<noteq> \<infinity>" using `emeasure M F \<noteq> \<infinity>` by auto
   1.297 -      then have "emeasure M (F \<inter> (\<Omega> - A)) = emeasure M F - emeasure M (F \<inter> A)" unfolding **
   1.298 +      have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
   1.299 +      then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
   1.300 +      have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
   1.301 +      then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
   1.302 +      then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
   1.303          using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
   1.304 -      also have "\<dots> = emeasure N F - emeasure N (F \<inter> A)" using eq `F \<in> E` * by simp
   1.305 -      also have "\<dots> = emeasure N (F \<inter> (\<Omega> - A))" unfolding **
   1.306 -        using `F \<inter> A \<in> sigma_sets \<Omega> E` `emeasure N (F \<inter> A) \<noteq> \<infinity>`
   1.307 +      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` * by simp
   1.308 +      also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
   1.309 +        using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
   1.310          by (auto intro!: emeasure_Diff[symmetric] simp: M N)
   1.311 -      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> (\<Omega> - A)) = emeasure N (F \<inter> (\<Omega> - A))"
   1.312 +      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega> - A)) = ?\<nu> (F \<inter> (\<Omega> - A))"
   1.313          using * by auto
   1.314      next
   1.315        fix A :: "nat \<Rightarrow> 'a set"
   1.316 -      assume "disjoint_family A" "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. emeasure M (F \<inter> X) = emeasure N (F \<inter> X)}"
   1.317 -      then have A: "range (\<lambda>i. F \<inter> A i) \<subseteq> sigma_sets \<Omega> E" "F \<inter> (\<Union>x. A x) = (\<Union>x. F \<inter> A x)"
   1.318 -        "disjoint_family (\<lambda>i. F \<inter> A i)" "\<And>i. emeasure M (F \<inter> A i) = emeasure N (F \<inter> A i)" "range A \<subseteq> sigma_sets \<Omega> E"
   1.319 -        by (auto simp: disjoint_family_on_def subset_eq)
   1.320 -      then show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> (\<Union>x. A x)) = emeasure N (F \<inter> (\<Union>x. A x))"
   1.321 -        by (auto simp: M N suminf_emeasure[symmetric] simp del: UN_simps)
   1.322 +      assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}"
   1.323 +      then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
   1.324 +        by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
   1.325 +      with A show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Union>x. A x)) = ?\<nu> (F \<inter> (\<Union>x. A x))"
   1.326 +        by auto
   1.327      qed
   1.328 -    have *: "sigma_sets \<Omega> E = ?D F"
   1.329 +    have *: "sigma_sets \<Omega> E = ?D"
   1.330        using `F \<in> E` `Int_stable E`
   1.331        by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq)
   1.332 -    have "\<And>D. D \<in> sigma_sets \<Omega> E \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
   1.333 +    have "\<And>D. D \<in> sigma_sets \<Omega> E \<Longrightarrow> ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)"
   1.334        by (subst (asm) *) auto }
   1.335    note * = this
   1.336    show "M = N"
   1.337    proof (rule measure_eqI)
   1.338      show "sets M = sets N"
   1.339        using M N by simp
   1.340 -    fix X assume "X \<in> sets M"
   1.341 -    then have "X \<in> sigma_sets \<Omega> E"
   1.342 +    fix F assume "F \<in> sets M"
   1.343 +    then have "F \<in> sigma_sets \<Omega> E"
   1.344        using M by simp
   1.345 -    let ?A = "\<lambda>i. A i \<inter> X"
   1.346 +    let ?A = "\<lambda>i. A i \<inter> F"
   1.347      have "range ?A \<subseteq> sigma_sets \<Omega> E" "incseq ?A"
   1.348 -      using A(1,2) `X \<in> sigma_sets \<Omega> E` by (auto simp: incseq_def)
   1.349 +      using A(1,2) `F \<in> sigma_sets \<Omega> E` by (auto simp: incseq_def)
   1.350      moreover
   1.351 -    { fix i have "emeasure M (?A i) = emeasure N (?A i)"
   1.352 -        using *[of "A i" X] `X \<in> sigma_sets \<Omega> E` A finite by auto }
   1.353 -    ultimately show "emeasure M X = emeasure N X"
   1.354 -      using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `X \<in> sigma_sets \<Omega> E`
   1.355 +    { fix i have "?\<mu> (?A i) = ?\<nu> (?A i)"
   1.356 +        using *[of "A i" F] `F \<in> sigma_sets \<Omega> E` A finite by auto }
   1.357 +    ultimately show "?\<mu> F = ?\<nu> F"
   1.358 +      using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `F \<in> sigma_sets \<Omega> E`
   1.359        by (auto simp: M N SUP_emeasure_incseq)
   1.360    qed
   1.361  qed
   1.362 @@ -1016,6 +1099,24 @@
   1.363         (auto simp: emeasure_distr measurable_def)
   1.364  qed
   1.365  
   1.366 +lemma AE_distr_iff:
   1.367 +  assumes f: "f \<in> measurable M N" and P: "{x \<in> space N. P x} \<in> sets N"
   1.368 +  shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   1.369 +proof (subst (1 2) AE_iff_measurable[OF _ refl])
   1.370 +  from P show "{x \<in> space (distr M N f). \<not> P x} \<in> sets (distr M N f)"
   1.371 +    by (auto intro!: sets_Collect_neg)
   1.372 +  moreover
   1.373 +  have "f -` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}"
   1.374 +    using f by (auto dest: measurable_space)
   1.375 +  then show "{x \<in> space M. \<not> P (f x)} \<in> sets M"
   1.376 +    using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg)
   1.377 +  moreover have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
   1.378 +    using f by (auto dest: measurable_space)
   1.379 +  ultimately show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
   1.380 +    (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
   1.381 +    using f by (simp add: emeasure_distr)
   1.382 +qed
   1.383 +
   1.384  lemma null_sets_distr_iff:
   1.385    "f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
   1.386    by (auto simp add: null_sets_def emeasure_distr measurable_sets)
   1.387 @@ -1295,103 +1396,81 @@
   1.388      unfolding measurable_def by auto
   1.389  qed
   1.390  
   1.391 +lemma strict_monoI_Suc:
   1.392 +  assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
   1.393 +  unfolding strict_mono_def
   1.394 +proof safe
   1.395 +  fix n m :: nat assume "n < m" then show "f n < f m"
   1.396 +    by (induct m) (auto simp: less_Suc_eq intro: less_trans ord)
   1.397 +qed
   1.398 +
   1.399  lemma emeasure_count_space:
   1.400    assumes "X \<subseteq> A" shows "emeasure (count_space A) X = (if finite X then ereal (card X) else \<infinity>)"
   1.401      (is "_ = ?M X")
   1.402    unfolding count_space_def
   1.403  proof (rule emeasure_measure_of_sigma)
   1.404 +  show "X \<in> Pow A" using `X \<subseteq> A` by auto
   1.405    show "sigma_algebra A (Pow A)" by (rule sigma_algebra_Pow)
   1.406 -
   1.407 -  show "positive (Pow A) ?M"
   1.408 +  show positive: "positive (Pow A) ?M"
   1.409      by (auto simp: positive_def)
   1.410 +  have additive: "additive (Pow A) ?M"
   1.411 +    by (auto simp: card_Un_disjoint additive_def)
   1.412  
   1.413 -  show "countably_additive (Pow A) ?M"
   1.414 -  proof (unfold countably_additive_def, safe)
   1.415 -      fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F"
   1.416 -      show "(\<Sum>i. ?M (F i)) = ?M (\<Union>i. F i)"
   1.417 -      proof cases
   1.418 -        assume "\<forall>i. finite (F i)"
   1.419 -        then have finite_F: "\<And>i. finite (F i)" by auto
   1.420 -        have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto
   1.421 -        from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto
   1.422 +  interpret ring_of_sets A "Pow A"
   1.423 +    by (rule ring_of_setsI) auto
   1.424 +  show "countably_additive (Pow A) ?M" 
   1.425 +    unfolding countably_additive_iff_continuous_from_below[OF positive additive]
   1.426 +  proof safe
   1.427 +    fix F :: "nat \<Rightarrow> 'a set" assume "incseq F"
   1.428 +    show "(\<lambda>i. ?M (F i)) ----> ?M (\<Union>i. F i)"
   1.429 +    proof cases
   1.430 +      assume "\<exists>i. \<forall>j\<ge>i. F i = F j"
   1.431 +      then guess i .. note i = this
   1.432 +      { fix j from i `incseq F` have "F j \<subseteq> F i"
   1.433 +          by (cases "i \<le> j") (auto simp: incseq_def) }
   1.434 +      then have eq: "(\<Union>i. F i) = F i"
   1.435 +        by auto
   1.436 +      with i show ?thesis
   1.437 +        by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
   1.438 +    next
   1.439 +      assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
   1.440 +      then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
   1.441 +      moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
   1.442 +      ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
   1.443  
   1.444 -        have inj_f: "inj_on f {i. F i \<noteq> {}}"
   1.445 -        proof (rule inj_onI, simp)
   1.446 -          fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}"
   1.447 -          then have "f i \<in> F i" "f j \<in> F j" using f by force+
   1.448 -          with disj * show "i = j" by (auto simp: disjoint_family_on_def)
   1.449 -        qed
   1.450 -        have fin_eq: "finite (\<Union>i. F i) \<longleftrightarrow> finite {i. F i \<noteq> {}}"
   1.451 -        proof
   1.452 -          assume "finite (\<Union>i. F i)"
   1.453 -          show "finite {i. F i \<noteq> {}}"
   1.454 -          proof (rule finite_imageD)
   1.455 -            from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto
   1.456 -            then show "finite (f`{i. F i \<noteq> {}})"
   1.457 -              by (rule finite_subset) fact
   1.458 -          qed fact
   1.459 -        next
   1.460 -          assume "finite {i. F i \<noteq> {}}"
   1.461 -          with finite_F have "finite (\<Union>i\<in>{i. F i \<noteq> {}}. F i)"
   1.462 -            by auto
   1.463 -          also have "(\<Union>i\<in>{i. F i \<noteq> {}}. F i) = (\<Union>i. F i)"
   1.464 -            by auto
   1.465 -          finally show "finite (\<Union>i. F i)" .
   1.466 -        qed
   1.467 -        
   1.468 -        show ?thesis
   1.469 -        proof cases
   1.470 -          assume *: "finite (\<Union>i. F i)"
   1.471 -          with finite_F have "finite {i. ?M (F i) \<noteq> 0} "
   1.472 -            by (simp add: fin_eq)
   1.473 -          then have "(\<Sum>i. ?M (F i)) = (\<Sum>i | ?M (F i) \<noteq> 0. ?M (F i))"
   1.474 -            by (rule suminf_finite) auto
   1.475 -          also have "\<dots> = ereal (\<Sum>i | F i \<noteq> {}. card (F i))"
   1.476 -            using finite_F by simp
   1.477 -          also have "\<dots> = ereal (card (\<Union>i \<in> {i. F i \<noteq> {}}. F i))"
   1.478 -            using * finite_F disj
   1.479 -            by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def fin_eq)
   1.480 -          also have "\<dots> = ?M (\<Union>i. F i)"
   1.481 -            using * by (auto intro!: arg_cong[where f=card])
   1.482 -          finally show ?thesis .
   1.483 -        next
   1.484 -          assume inf: "infinite (\<Union>i. F i)"
   1.485 -          { fix i
   1.486 -            have "\<exists>N. i \<le> (\<Sum>i<N. card (F i))"
   1.487 -            proof (induct i)
   1.488 -              case (Suc j)
   1.489 -              from Suc obtain N where N: "j \<le> (\<Sum>i<N. card (F i))" by auto
   1.490 -              have "infinite ({i. F i \<noteq> {}} - {..< N})"
   1.491 -                using inf by (auto simp: fin_eq)
   1.492 -              then have "{i. F i \<noteq> {}} - {..< N} \<noteq> {}"
   1.493 -                by (metis finite.emptyI)
   1.494 -              then obtain i where i: "F i \<noteq> {}" "N \<le> i"
   1.495 -                by (auto simp: not_less[symmetric])
   1.496 +      have "incseq (\<lambda>i. ?M (F i))"
   1.497 +        using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
   1.498 +      then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
   1.499 +        by (rule LIMSEQ_ereal_SUPR)
   1.500  
   1.501 -              note N
   1.502 -              also have "(\<Sum>i<N. card (F i)) \<le> (\<Sum>i<i. card (F i))"
   1.503 -                by (rule setsum_mono2) (auto simp: i)
   1.504 -              also have "\<dots> < (\<Sum>i<i. card (F i)) + card (F i)"
   1.505 -                using finite_F `F i \<noteq> {}` by (simp add: card_gt_0_iff)
   1.506 -              finally have "j < (\<Sum>i<Suc i. card (F i))"
   1.507 -                by simp
   1.508 -              then show ?case unfolding Suc_le_eq by blast
   1.509 -            qed simp }
   1.510 -          with finite_F inf show ?thesis
   1.511 -            by (auto simp del: real_of_nat_setsum intro!: SUP_PInfty
   1.512 -                     simp add: suminf_ereal_eq_SUPR real_of_nat_setsum[symmetric])
   1.513 -        qed
   1.514 -      next
   1.515 -        assume "\<not> (\<forall>i. finite (F i))"
   1.516 -        then obtain j where j: "infinite (F j)" by auto
   1.517 -        then have "infinite (\<Union>i. F i)"
   1.518 -          using finite_subset[of "F j" "\<Union>i. F i"] by auto
   1.519 -        moreover have "\<And>i. 0 \<le> ?M (F i)" by auto
   1.520 -        ultimately show ?thesis
   1.521 -          using suminf_PInfty[of "\<lambda>i. ?M (F i)" j] j by auto
   1.522 +      moreover have "(SUP n. ?M (F n)) = \<infinity>"
   1.523 +      proof (rule SUP_PInfty)
   1.524 +        fix n :: nat show "\<exists>k::nat\<in>UNIV. ereal n \<le> ?M (F k)"
   1.525 +        proof (induct n)
   1.526 +          case (Suc n)
   1.527 +          then guess k .. note k = this
   1.528 +          moreover have "finite (F k) \<Longrightarrow> finite (F (f k)) \<Longrightarrow> card (F k) < card (F (f k))"
   1.529 +            using `F k \<subset> F (f k)` by (simp add: psubset_card_mono)
   1.530 +          moreover have "finite (F (f k)) \<Longrightarrow> finite (F k)"
   1.531 +            using `k \<le> f k` `incseq F` by (auto simp: incseq_def dest: finite_subset)
   1.532 +          ultimately show ?case
   1.533 +            by (auto intro!: exI[of _ "f k"])
   1.534 +        qed auto
   1.535        qed
   1.536 +
   1.537 +      moreover
   1.538 +      have "inj (\<lambda>n. F ((f ^^ n) 0))"
   1.539 +        by (intro strict_mono_imp_inj_on strict_monoI_Suc) (simp add: *)
   1.540 +      then have 1: "infinite (range (\<lambda>i. F ((f ^^ i) 0)))"
   1.541 +        by (rule range_inj_infinite)
   1.542 +      have "infinite (Pow (\<Union>i. F i))"
   1.543 +        by (rule infinite_super[OF _ 1]) auto
   1.544 +      then have "infinite (\<Union>i. F i)"
   1.545 +        by auto
   1.546 +      
   1.547 +      ultimately show ?thesis by auto
   1.548 +    qed
   1.549    qed
   1.550 -  show "X \<in> Pow A" using `X \<subseteq> A` by simp
   1.551  qed
   1.552  
   1.553  lemma emeasure_count_space_finite[simp]: