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.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.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.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.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.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.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.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.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]:
```