tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
authorhoelzl
Wed Oct 10 12:12:15 2012 +0200 (2012-10-10)
changeset 4977316907431e477
parent 49772 75660d89c339
child 49774 dfa8ddb874ce
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Oct 10 12:12:14 2012 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Oct 10 12:12:15 2012 +0200
     1.3 @@ -9,12 +9,6 @@
     1.4    imports Measure_Space
     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  text {*
    1.14    Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
    1.15  *}
    1.16 @@ -684,146 +678,6 @@
    1.17  
    1.18  subsubsection {*Alternative instances of caratheodory*}
    1.19  
    1.20 -lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
    1.21 -  assumes f: "positive M f" "additive M f"
    1.22 -  shows "countably_additive M f \<longleftrightarrow>
    1.23 -    (\<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.24 -  unfolding countably_additive_def
    1.25 -proof safe
    1.26 -  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.27 -  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
    1.28 -  then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
    1.29 -  with count_sum[THEN spec, of "disjointed A"] A(3)
    1.30 -  have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
    1.31 -    by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
    1.32 -  moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    1.33 -    using f(1)[unfolded positive_def] dA
    1.34 -    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_ereal_pos)
    1.35 -  from LIMSEQ_Suc[OF this]
    1.36 -  have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    1.37 -    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
    1.38 -  moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
    1.39 -    using disjointed_additive[OF f A(1,2)] .
    1.40 -  ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
    1.41 -next
    1.42 -  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.43 -  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
    1.44 -  have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
    1.45 -  have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
    1.46 -  proof (unfold *[symmetric], intro cont[rule_format])
    1.47 -    show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> M"
    1.48 -      using A * by auto
    1.49 -  qed (force intro!: incseq_SucI)
    1.50 -  moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
    1.51 -    using A
    1.52 -    by (intro additive_sum[OF f, of _ A, symmetric])
    1.53 -       (auto intro: disjoint_family_on_mono[where B=UNIV])
    1.54 -  ultimately
    1.55 -  have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
    1.56 -    unfolding sums_def2 by simp
    1.57 -  from sums_unique[OF this]
    1.58 -  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
    1.59 -qed
    1.60 -
    1.61 -lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
    1.62 -  assumes f: "positive M f" "additive M f"
    1.63 -  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.64 -     \<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.65 -proof safe
    1.66 -  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.67 -  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.68 -  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
    1.69 -    using `positive M f`[unfolded positive_def] by auto
    1.70 -next
    1.71 -  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.72 -  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.73 -
    1.74 -  have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
    1.75 -    using additive_increasing[OF f] unfolding increasing_def by simp
    1.76 -
    1.77 -  have decseq_fA: "decseq (\<lambda>i. f (A i))"
    1.78 -    using A by (auto simp: decseq_def intro!: f_mono)
    1.79 -  have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
    1.80 -    using A by (auto simp: decseq_def)
    1.81 -  then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
    1.82 -    using A unfolding decseq_def by (auto intro!: f_mono Diff)
    1.83 -  have "f (\<Inter>x. A x) \<le> f (A 0)"
    1.84 -    using A by (auto intro!: f_mono)
    1.85 -  then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
    1.86 -    using A by auto
    1.87 -  { fix i
    1.88 -    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
    1.89 -    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
    1.90 -      using A by auto }
    1.91 -  note f_fin = this
    1.92 -  have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
    1.93 -  proof (intro cont[rule_format, OF _ decseq _ f_fin])
    1.94 -    show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
    1.95 -      using A by auto
    1.96 -  qed
    1.97 -  from INF_Lim_ereal[OF decseq_f this]
    1.98 -  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
    1.99 -  moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
   1.100 -    by auto
   1.101 -  ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
   1.102 -    using A(4) f_fin f_Int_fin
   1.103 -    by (subst INFI_ereal_add) (auto simp: decseq_f)
   1.104 -  moreover {
   1.105 -    fix n
   1.106 -    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.107 -      using A by (subst f(2)[THEN additiveD]) auto
   1.108 -    also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
   1.109 -      by auto
   1.110 -    finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
   1.111 -  ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
   1.112 -    by simp
   1.113 -  with LIMSEQ_ereal_INFI[OF decseq_fA]
   1.114 -  show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
   1.115 -qed
   1.116 -
   1.117 -lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
   1.118 -lemma positiveD2: "positive M f \<Longrightarrow> A \<in> M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
   1.119 -
   1.120 -lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
   1.121 -  assumes f: "positive M f" "additive M f" "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   1.122 -  assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.123 -  assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
   1.124 -  shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   1.125 -proof -
   1.126 -  have "\<forall>A\<in>M. \<exists>x. f A = ereal x"
   1.127 -  proof
   1.128 -    fix A assume "A \<in> M" with f show "\<exists>x. f A = ereal x"
   1.129 -      unfolding positive_def by (cases "f A") auto
   1.130 -  qed
   1.131 -  from bchoice[OF this] guess f' .. note f' = this[rule_format]
   1.132 -  from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
   1.133 -    by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
   1.134 -  moreover
   1.135 -  { fix i
   1.136 -    have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
   1.137 -      using A by (intro f(2)[THEN additiveD, symmetric]) auto
   1.138 -    also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
   1.139 -      by auto
   1.140 -    finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
   1.141 -      using A by (subst (asm) (1 2 3) f') auto
   1.142 -    then have "f ((\<Union>i. A i) - A i) = ereal (f' (\<Union>i. A i) - f' (A i))"
   1.143 -      using A f' by auto }
   1.144 -  ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
   1.145 -    by (simp add: zero_ereal_def)
   1.146 -  then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
   1.147 -    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
   1.148 -  then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   1.149 -    using A by (subst (1 2) f') auto
   1.150 -qed
   1.151 -
   1.152 -lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
   1.153 -  assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   1.154 -  assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.155 -  shows "countably_additive M f"
   1.156 -  using countably_additive_iff_continuous_from_below[OF f]
   1.157 -  using empty_continuous_imp_continuous_from_below[OF f fin] cont
   1.158 -  by blast
   1.159 -
   1.160  lemma (in ring_of_sets) caratheodory_empty_continuous:
   1.161    assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
   1.162    assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
     2.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:14 2012 +0200
     2.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:15 2012 +0200
     2.3 @@ -12,6 +12,12 @@
     2.4    "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
     2.5  begin
     2.6  
     2.7 +lemma sums_def2:
     2.8 +  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
     2.9 +  unfolding sums_def
    2.10 +  apply (subst LIMSEQ_Suc_iff[symmetric])
    2.11 +  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    2.12 +
    2.13  lemma suminf_cmult_indicator:
    2.14    fixes f :: "nat \<Rightarrow> ereal"
    2.15    assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
    2.16 @@ -90,6 +96,9 @@
    2.17  definition increasing where
    2.18    "increasing M \<mu> \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<subseteq> y \<longrightarrow> \<mu> x \<le> \<mu> y)"
    2.19  
    2.20 +lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
    2.21 +lemma positiveD2: "positive M f \<Longrightarrow> A \<in> M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
    2.22 +
    2.23  lemma positiveD_empty:
    2.24    "positive M f \<Longrightarrow> f {} = 0"
    2.25    by (auto simp add: positive_def)
    2.26 @@ -240,6 +249,143 @@
    2.27    finally show "(\<Sum>i. \<mu> (F i)) = \<mu> (\<Union>i. F i)" .
    2.28  qed
    2.29  
    2.30 +lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
    2.31 +  assumes f: "positive M f" "additive M f"
    2.32 +  shows "countably_additive M f \<longleftrightarrow>
    2.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))"
    2.34 +  unfolding countably_additive_def
    2.35 +proof safe
    2.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)"
    2.37 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
    2.38 +  then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
    2.39 +  with count_sum[THEN spec, of "disjointed A"] A(3)
    2.40 +  have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
    2.41 +    by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
    2.42 +  moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    2.43 +    using f(1)[unfolded positive_def] dA
    2.44 +    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_ereal_pos)
    2.45 +  from LIMSEQ_Suc[OF this]
    2.46 +  have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    2.47 +    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
    2.48 +  moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
    2.49 +    using disjointed_additive[OF f A(1,2)] .
    2.50 +  ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
    2.51 +next
    2.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)"
    2.53 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
    2.54 +  have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
    2.55 +  have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
    2.56 +  proof (unfold *[symmetric], intro cont[rule_format])
    2.57 +    show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> M"
    2.58 +      using A * by auto
    2.59 +  qed (force intro!: incseq_SucI)
    2.60 +  moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
    2.61 +    using A
    2.62 +    by (intro additive_sum[OF f, of _ A, symmetric])
    2.63 +       (auto intro: disjoint_family_on_mono[where B=UNIV])
    2.64 +  ultimately
    2.65 +  have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
    2.66 +    unfolding sums_def2 by simp
    2.67 +  from sums_unique[OF this]
    2.68 +  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
    2.69 +qed
    2.70 +
    2.71 +lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
    2.72 +  assumes f: "positive M f" "additive M f"
    2.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))
    2.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)"
    2.75 +proof safe
    2.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))"
    2.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>"
    2.78 +  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
    2.79 +    using `positive M f`[unfolded positive_def] by auto
    2.80 +next
    2.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"
    2.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>"
    2.83 +
    2.84 +  have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
    2.85 +    using additive_increasing[OF f] unfolding increasing_def by simp
    2.86 +
    2.87 +  have decseq_fA: "decseq (\<lambda>i. f (A i))"
    2.88 +    using A by (auto simp: decseq_def intro!: f_mono)
    2.89 +  have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
    2.90 +    using A by (auto simp: decseq_def)
    2.91 +  then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
    2.92 +    using A unfolding decseq_def by (auto intro!: f_mono Diff)
    2.93 +  have "f (\<Inter>x. A x) \<le> f (A 0)"
    2.94 +    using A by (auto intro!: f_mono)
    2.95 +  then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
    2.96 +    using A by auto
    2.97 +  { fix i
    2.98 +    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
    2.99 +    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
   2.100 +      using A by auto }
   2.101 +  note f_fin = this
   2.102 +  have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
   2.103 +  proof (intro cont[rule_format, OF _ decseq _ f_fin])
   2.104 +    show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
   2.105 +      using A by auto
   2.106 +  qed
   2.107 +  from INF_Lim_ereal[OF decseq_f this]
   2.108 +  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
   2.109 +  moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
   2.110 +    by auto
   2.111 +  ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
   2.112 +    using A(4) f_fin f_Int_fin
   2.113 +    by (subst INFI_ereal_add) (auto simp: decseq_f)
   2.114 +  moreover {
   2.115 +    fix n
   2.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))"
   2.117 +      using A by (subst f(2)[THEN additiveD]) auto
   2.118 +    also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
   2.119 +      by auto
   2.120 +    finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
   2.121 +  ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
   2.122 +    by simp
   2.123 +  with LIMSEQ_ereal_INFI[OF decseq_fA]
   2.124 +  show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
   2.125 +qed
   2.126 +
   2.127 +lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
   2.128 +  assumes f: "positive M f" "additive M f" "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   2.129 +  assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   2.130 +  assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
   2.131 +  shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   2.132 +proof -
   2.133 +  have "\<forall>A\<in>M. \<exists>x. f A = ereal x"
   2.134 +  proof
   2.135 +    fix A assume "A \<in> M" with f show "\<exists>x. f A = ereal x"
   2.136 +      unfolding positive_def by (cases "f A") auto
   2.137 +  qed
   2.138 +  from bchoice[OF this] guess f' .. note f' = this[rule_format]
   2.139 +  from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
   2.140 +    by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
   2.141 +  moreover
   2.142 +  { fix i
   2.143 +    have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
   2.144 +      using A by (intro f(2)[THEN additiveD, symmetric]) auto
   2.145 +    also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
   2.146 +      by auto
   2.147 +    finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
   2.148 +      using A by (subst (asm) (1 2 3) f') auto
   2.149 +    then have "f ((\<Union>i. A i) - A i) = ereal (f' (\<Union>i. A i) - f' (A i))"
   2.150 +      using A f' by auto }
   2.151 +  ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
   2.152 +    by (simp add: zero_ereal_def)
   2.153 +  then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
   2.154 +    by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
   2.155 +  then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   2.156 +    using A by (subst (1 2) f') auto
   2.157 +qed
   2.158 +
   2.159 +lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
   2.160 +  assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   2.161 +  assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   2.162 +  shows "countably_additive M f"
   2.163 +  using countably_additive_iff_continuous_from_below[OF f]
   2.164 +  using empty_continuous_imp_continuous_from_below[OF f fin] cont
   2.165 +  by blast
   2.166 +
   2.167  section {* Properties of @{const emeasure} *}
   2.168  
   2.169  lemma emeasure_positive: "positive (sets M) (emeasure M)"
   2.170 @@ -314,84 +460,21 @@
   2.171      using finite `0 \<le> emeasure M B` by auto
   2.172  qed
   2.173  
   2.174 -lemma emeasure_countable_increasing:
   2.175 -  assumes A: "range A \<subseteq> sets M"
   2.176 -      and A0: "A 0 = {}"
   2.177 -      and ASuc: "\<And>n. A n \<subseteq> A (Suc n)"
   2.178 -  shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   2.179 -proof -
   2.180 -  { fix n
   2.181 -    have "emeasure M (A n) = (\<Sum>i<n. emeasure M (A (Suc i) - A i))"
   2.182 -      proof (induct n)
   2.183 -        case 0 thus ?case by (auto simp add: A0)
   2.184 -      next
   2.185 -        case (Suc m)
   2.186 -        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
   2.187 -          by (metis ASuc Un_Diff_cancel Un_absorb1)
   2.188 -        hence "emeasure M (A (Suc m)) =
   2.189 -               emeasure M (A m) + emeasure M (A (Suc m) - A m)"
   2.190 -          by (subst plus_emeasure)
   2.191 -             (auto simp add: emeasure_additive range_subsetD [OF A])
   2.192 -        with Suc show ?case
   2.193 -          by simp
   2.194 -      qed }
   2.195 -  note Meq = this
   2.196 -  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
   2.197 -    proof (rule UN_finite2_eq [where k=1], simp)
   2.198 -      fix i
   2.199 -      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
   2.200 -        proof (induct i)
   2.201 -          case 0 thus ?case by (simp add: A0)
   2.202 -        next
   2.203 -          case (Suc i)
   2.204 -          thus ?case
   2.205 -            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
   2.206 -        qed
   2.207 -    qed
   2.208 -  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
   2.209 -    by (metis A Diff range_subsetD)
   2.210 -  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
   2.211 -    by (blast intro: range_subsetD [OF A])
   2.212 -  have "(SUP n. \<Sum>i<n. emeasure M (A (Suc i) - A i)) = (\<Sum>i. emeasure M (A (Suc i) - A i))"
   2.213 -    using A by (auto intro!: suminf_ereal_eq_SUPR[symmetric])
   2.214 -  also have "\<dots> = emeasure M (\<Union>i. A (Suc i) - A i)"
   2.215 -    by (rule suminf_emeasure)
   2.216 -       (auto simp add: disjoint_family_Suc ASuc A1 A2)
   2.217 -  also have "... =  emeasure M (\<Union>i. A i)"
   2.218 -    by (simp add: Aeq)
   2.219 -  finally have "(SUP n. \<Sum>i<n. emeasure M (A (Suc i) - A i)) = emeasure M (\<Union>i. A i)" .
   2.220 -  then show ?thesis by (auto simp add: Meq)
   2.221 -qed
   2.222 -
   2.223 -lemma SUP_emeasure_incseq:
   2.224 -  assumes A: "range A \<subseteq> sets M" and "incseq A"
   2.225 -  shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   2.226 -proof -
   2.227 -  have *: "(SUP n. emeasure M (nat_case {} A (Suc n))) = (SUP n. emeasure M (nat_case {} A n))"
   2.228 -    using A by (auto intro!: SUPR_eq exI split: nat.split)
   2.229 -  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
   2.230 -    by (auto simp add: split: nat.splits)
   2.231 -  have meq: "\<And>n. emeasure M (A n) = (emeasure M \<circ> nat_case {} A) (Suc n)"
   2.232 -    by simp
   2.233 -  have "(SUP n. emeasure M (nat_case {} A n)) = emeasure M (\<Union>i. nat_case {} A i)"
   2.234 -    using range_subsetD[OF A] incseq_SucD[OF `incseq A`]
   2.235 -    by (force split: nat.splits intro!: emeasure_countable_increasing)
   2.236 -  also have "emeasure M (\<Union>i. nat_case {} A i) = emeasure M (\<Union>i. A i)"
   2.237 -    by (simp add: ueq)
   2.238 -  finally have "(SUP n. emeasure M (nat_case {} A n)) = emeasure M (\<Union>i. A i)" .
   2.239 -  thus ?thesis unfolding meq * comp_def .
   2.240 -qed
   2.241 +lemma Lim_emeasure_incseq:
   2.242 +  "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   2.243 +  using emeasure_countably_additive
   2.244 +  by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive)
   2.245  
   2.246  lemma incseq_emeasure:
   2.247    assumes "range B \<subseteq> sets M" "incseq B"
   2.248    shows "incseq (\<lambda>i. emeasure M (B i))"
   2.249    using assms by (auto simp: incseq_def intro!: emeasure_mono)
   2.250  
   2.251 -lemma Lim_emeasure_incseq:
   2.252 +lemma SUP_emeasure_incseq:
   2.253    assumes A: "range A \<subseteq> sets M" "incseq A"
   2.254 -  shows "(\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   2.255 -  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A]
   2.256 -    SUP_emeasure_incseq[OF A] by simp
   2.257 +  shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   2.258 +  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
   2.259 +  by (simp add: LIMSEQ_unique)
   2.260  
   2.261  lemma decseq_emeasure:
   2.262    assumes "range B \<subseteq> sets M" "decseq B"
   2.263 @@ -548,66 +631,66 @@
   2.264    and A: "range A \<subseteq> E" "incseq A" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   2.265    shows "M = N"
   2.266  proof -
   2.267 -  let ?D = "\<lambda>F. {D. D \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)}"
   2.268 +  let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
   2.269    interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
   2.270 -  { fix F assume "F \<in> E" and "emeasure M F \<noteq> \<infinity>"
   2.271 +  { fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
   2.272      then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
   2.273 -    have "emeasure N F \<noteq> \<infinity>" using `emeasure M F \<noteq> \<infinity>` `F \<in> E` eq by simp
   2.274 -    interpret D: dynkin_system \<Omega> "?D F"
   2.275 +    let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}"
   2.276 +    have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
   2.277 +    interpret D: dynkin_system \<Omega> ?D
   2.278      proof (rule dynkin_systemI, simp_all)
   2.279 -      fix A assume "A \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> A) = emeasure N (F \<inter> A)"
   2.280 +      fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
   2.281        then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto
   2.282      next
   2.283        have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto
   2.284 -      then show "emeasure M (F \<inter> \<Omega>) = emeasure N (F \<inter> \<Omega>)"
   2.285 +      then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)"
   2.286          using `F \<in> E` eq by (auto intro: sigma_sets_top)
   2.287      next
   2.288 -      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> A) = emeasure N (F \<inter> A)"
   2.289 +      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
   2.290        then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
   2.291          and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
   2.292          using `F \<in> E` S.sets_into_space by auto
   2.293 -      have "emeasure N (F \<inter> A) \<le> emeasure N F" by (auto intro!: emeasure_mono simp: M N)
   2.294 -      then have "emeasure N (F \<inter> A) \<noteq> \<infinity>" using `emeasure N F \<noteq> \<infinity>` by auto
   2.295 -      have "emeasure M (F \<inter> A) \<le> emeasure M F" by (auto intro!: emeasure_mono simp: M N)
   2.296 -      then have "emeasure M (F \<inter> A) \<noteq> \<infinity>" using `emeasure M F \<noteq> \<infinity>` by auto
   2.297 -      then have "emeasure M (F \<inter> (\<Omega> - A)) = emeasure M F - emeasure M (F \<inter> A)" unfolding **
   2.298 +      have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
   2.299 +      then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
   2.300 +      have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
   2.301 +      then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
   2.302 +      then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
   2.303          using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
   2.304 -      also have "\<dots> = emeasure N F - emeasure N (F \<inter> A)" using eq `F \<in> E` * by simp
   2.305 -      also have "\<dots> = emeasure N (F \<inter> (\<Omega> - A))" unfolding **
   2.306 -        using `F \<inter> A \<in> sigma_sets \<Omega> E` `emeasure N (F \<inter> A) \<noteq> \<infinity>`
   2.307 +      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` * by simp
   2.308 +      also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
   2.309 +        using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
   2.310          by (auto intro!: emeasure_Diff[symmetric] simp: M N)
   2.311 -      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> emeasure M (F \<inter> (\<Omega> - A)) = emeasure N (F \<inter> (\<Omega> - A))"
   2.312 +      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega> - A)) = ?\<nu> (F \<inter> (\<Omega> - A))"
   2.313          using * by auto
   2.314      next
   2.315        fix A :: "nat \<Rightarrow> 'a set"
   2.316 -      assume "disjoint_family A" "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. emeasure M (F \<inter> X) = emeasure N (F \<inter> X)}"
   2.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)"
   2.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"
   2.319 -        by (auto simp: disjoint_family_on_def subset_eq)
   2.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))"
   2.321 -        by (auto simp: M N suminf_emeasure[symmetric] simp del: UN_simps)
   2.322 +      assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}"
   2.323 +      then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
   2.324 +        by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
   2.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))"
   2.326 +        by auto
   2.327      qed
   2.328 -    have *: "sigma_sets \<Omega> E = ?D F"
   2.329 +    have *: "sigma_sets \<Omega> E = ?D"
   2.330        using `F \<in> E` `Int_stable E`
   2.331        by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq)
   2.332 -    have "\<And>D. D \<in> sigma_sets \<Omega> E \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
   2.333 +    have "\<And>D. D \<in> sigma_sets \<Omega> E \<Longrightarrow> ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)"
   2.334        by (subst (asm) *) auto }
   2.335    note * = this
   2.336    show "M = N"
   2.337    proof (rule measure_eqI)
   2.338      show "sets M = sets N"
   2.339        using M N by simp
   2.340 -    fix X assume "X \<in> sets M"
   2.341 -    then have "X \<in> sigma_sets \<Omega> E"
   2.342 +    fix F assume "F \<in> sets M"
   2.343 +    then have "F \<in> sigma_sets \<Omega> E"
   2.344        using M by simp
   2.345 -    let ?A = "\<lambda>i. A i \<inter> X"
   2.346 +    let ?A = "\<lambda>i. A i \<inter> F"
   2.347      have "range ?A \<subseteq> sigma_sets \<Omega> E" "incseq ?A"
   2.348 -      using A(1,2) `X \<in> sigma_sets \<Omega> E` by (auto simp: incseq_def)
   2.349 +      using A(1,2) `F \<in> sigma_sets \<Omega> E` by (auto simp: incseq_def)
   2.350      moreover
   2.351 -    { fix i have "emeasure M (?A i) = emeasure N (?A i)"
   2.352 -        using *[of "A i" X] `X \<in> sigma_sets \<Omega> E` A finite by auto }
   2.353 -    ultimately show "emeasure M X = emeasure N X"
   2.354 -      using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `X \<in> sigma_sets \<Omega> E`
   2.355 +    { fix i have "?\<mu> (?A i) = ?\<nu> (?A i)"
   2.356 +        using *[of "A i" F] `F \<in> sigma_sets \<Omega> E` A finite by auto }
   2.357 +    ultimately show "?\<mu> F = ?\<nu> F"
   2.358 +      using SUP_emeasure_incseq[of ?A M] SUP_emeasure_incseq[of ?A N] A(3) `F \<in> sigma_sets \<Omega> E`
   2.359        by (auto simp: M N SUP_emeasure_incseq)
   2.360    qed
   2.361  qed
   2.362 @@ -1016,6 +1099,24 @@
   2.363         (auto simp: emeasure_distr measurable_def)
   2.364  qed
   2.365  
   2.366 +lemma AE_distr_iff:
   2.367 +  assumes f: "f \<in> measurable M N" and P: "{x \<in> space N. P x} \<in> sets N"
   2.368 +  shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   2.369 +proof (subst (1 2) AE_iff_measurable[OF _ refl])
   2.370 +  from P show "{x \<in> space (distr M N f). \<not> P x} \<in> sets (distr M N f)"
   2.371 +    by (auto intro!: sets_Collect_neg)
   2.372 +  moreover
   2.373 +  have "f -` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}"
   2.374 +    using f by (auto dest: measurable_space)
   2.375 +  then show "{x \<in> space M. \<not> P (f x)} \<in> sets M"
   2.376 +    using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg)
   2.377 +  moreover have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
   2.378 +    using f by (auto dest: measurable_space)
   2.379 +  ultimately show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
   2.380 +    (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
   2.381 +    using f by (simp add: emeasure_distr)
   2.382 +qed
   2.383 +
   2.384  lemma null_sets_distr_iff:
   2.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"
   2.386    by (auto simp add: null_sets_def emeasure_distr measurable_sets)
   2.387 @@ -1295,103 +1396,81 @@
   2.388      unfolding measurable_def by auto
   2.389  qed
   2.390  
   2.391 +lemma strict_monoI_Suc:
   2.392 +  assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
   2.393 +  unfolding strict_mono_def
   2.394 +proof safe
   2.395 +  fix n m :: nat assume "n < m" then show "f n < f m"
   2.396 +    by (induct m) (auto simp: less_Suc_eq intro: less_trans ord)
   2.397 +qed
   2.398 +
   2.399  lemma emeasure_count_space:
   2.400    assumes "X \<subseteq> A" shows "emeasure (count_space A) X = (if finite X then ereal (card X) else \<infinity>)"
   2.401      (is "_ = ?M X")
   2.402    unfolding count_space_def
   2.403  proof (rule emeasure_measure_of_sigma)
   2.404 +  show "X \<in> Pow A" using `X \<subseteq> A` by auto
   2.405    show "sigma_algebra A (Pow A)" by (rule sigma_algebra_Pow)
   2.406 -
   2.407 -  show "positive (Pow A) ?M"
   2.408 +  show positive: "positive (Pow A) ?M"
   2.409      by (auto simp: positive_def)
   2.410 +  have additive: "additive (Pow A) ?M"
   2.411 +    by (auto simp: card_Un_disjoint additive_def)
   2.412  
   2.413 -  show "countably_additive (Pow A) ?M"
   2.414 -  proof (unfold countably_additive_def, safe)
   2.415 -      fix F :: "nat \<Rightarrow> 'a set" assume disj: "disjoint_family F"
   2.416 -      show "(\<Sum>i. ?M (F i)) = ?M (\<Union>i. F i)"
   2.417 -      proof cases
   2.418 -        assume "\<forall>i. finite (F i)"
   2.419 -        then have finite_F: "\<And>i. finite (F i)" by auto
   2.420 -        have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto
   2.421 -        from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto
   2.422 +  interpret ring_of_sets A "Pow A"
   2.423 +    by (rule ring_of_setsI) auto
   2.424 +  show "countably_additive (Pow A) ?M" 
   2.425 +    unfolding countably_additive_iff_continuous_from_below[OF positive additive]
   2.426 +  proof safe
   2.427 +    fix F :: "nat \<Rightarrow> 'a set" assume "incseq F"
   2.428 +    show "(\<lambda>i. ?M (F i)) ----> ?M (\<Union>i. F i)"
   2.429 +    proof cases
   2.430 +      assume "\<exists>i. \<forall>j\<ge>i. F i = F j"
   2.431 +      then guess i .. note i = this
   2.432 +      { fix j from i `incseq F` have "F j \<subseteq> F i"
   2.433 +          by (cases "i \<le> j") (auto simp: incseq_def) }
   2.434 +      then have eq: "(\<Union>i. F i) = F i"
   2.435 +        by auto
   2.436 +      with i show ?thesis
   2.437 +        by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
   2.438 +    next
   2.439 +      assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
   2.440 +      then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
   2.441 +      moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
   2.442 +      ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
   2.443  
   2.444 -        have inj_f: "inj_on f {i. F i \<noteq> {}}"
   2.445 -        proof (rule inj_onI, simp)
   2.446 -          fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}"
   2.447 -          then have "f i \<in> F i" "f j \<in> F j" using f by force+
   2.448 -          with disj * show "i = j" by (auto simp: disjoint_family_on_def)
   2.449 -        qed
   2.450 -        have fin_eq: "finite (\<Union>i. F i) \<longleftrightarrow> finite {i. F i \<noteq> {}}"
   2.451 -        proof
   2.452 -          assume "finite (\<Union>i. F i)"
   2.453 -          show "finite {i. F i \<noteq> {}}"
   2.454 -          proof (rule finite_imageD)
   2.455 -            from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto
   2.456 -            then show "finite (f`{i. F i \<noteq> {}})"
   2.457 -              by (rule finite_subset) fact
   2.458 -          qed fact
   2.459 -        next
   2.460 -          assume "finite {i. F i \<noteq> {}}"
   2.461 -          with finite_F have "finite (\<Union>i\<in>{i. F i \<noteq> {}}. F i)"
   2.462 -            by auto
   2.463 -          also have "(\<Union>i\<in>{i. F i \<noteq> {}}. F i) = (\<Union>i. F i)"
   2.464 -            by auto
   2.465 -          finally show "finite (\<Union>i. F i)" .
   2.466 -        qed
   2.467 -        
   2.468 -        show ?thesis
   2.469 -        proof cases
   2.470 -          assume *: "finite (\<Union>i. F i)"
   2.471 -          with finite_F have "finite {i. ?M (F i) \<noteq> 0} "
   2.472 -            by (simp add: fin_eq)
   2.473 -          then have "(\<Sum>i. ?M (F i)) = (\<Sum>i | ?M (F i) \<noteq> 0. ?M (F i))"
   2.474 -            by (rule suminf_finite) auto
   2.475 -          also have "\<dots> = ereal (\<Sum>i | F i \<noteq> {}. card (F i))"
   2.476 -            using finite_F by simp
   2.477 -          also have "\<dots> = ereal (card (\<Union>i \<in> {i. F i \<noteq> {}}. F i))"
   2.478 -            using * finite_F disj
   2.479 -            by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def fin_eq)
   2.480 -          also have "\<dots> = ?M (\<Union>i. F i)"
   2.481 -            using * by (auto intro!: arg_cong[where f=card])
   2.482 -          finally show ?thesis .
   2.483 -        next
   2.484 -          assume inf: "infinite (\<Union>i. F i)"
   2.485 -          { fix i
   2.486 -            have "\<exists>N. i \<le> (\<Sum>i<N. card (F i))"
   2.487 -            proof (induct i)
   2.488 -              case (Suc j)
   2.489 -              from Suc obtain N where N: "j \<le> (\<Sum>i<N. card (F i))" by auto
   2.490 -              have "infinite ({i. F i \<noteq> {}} - {..< N})"
   2.491 -                using inf by (auto simp: fin_eq)
   2.492 -              then have "{i. F i \<noteq> {}} - {..< N} \<noteq> {}"
   2.493 -                by (metis finite.emptyI)
   2.494 -              then obtain i where i: "F i \<noteq> {}" "N \<le> i"
   2.495 -                by (auto simp: not_less[symmetric])
   2.496 +      have "incseq (\<lambda>i. ?M (F i))"
   2.497 +        using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
   2.498 +      then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
   2.499 +        by (rule LIMSEQ_ereal_SUPR)
   2.500  
   2.501 -              note N
   2.502 -              also have "(\<Sum>i<N. card (F i)) \<le> (\<Sum>i<i. card (F i))"
   2.503 -                by (rule setsum_mono2) (auto simp: i)
   2.504 -              also have "\<dots> < (\<Sum>i<i. card (F i)) + card (F i)"
   2.505 -                using finite_F `F i \<noteq> {}` by (simp add: card_gt_0_iff)
   2.506 -              finally have "j < (\<Sum>i<Suc i. card (F i))"
   2.507 -                by simp
   2.508 -              then show ?case unfolding Suc_le_eq by blast
   2.509 -            qed simp }
   2.510 -          with finite_F inf show ?thesis
   2.511 -            by (auto simp del: real_of_nat_setsum intro!: SUP_PInfty
   2.512 -                     simp add: suminf_ereal_eq_SUPR real_of_nat_setsum[symmetric])
   2.513 -        qed
   2.514 -      next
   2.515 -        assume "\<not> (\<forall>i. finite (F i))"
   2.516 -        then obtain j where j: "infinite (F j)" by auto
   2.517 -        then have "infinite (\<Union>i. F i)"
   2.518 -          using finite_subset[of "F j" "\<Union>i. F i"] by auto
   2.519 -        moreover have "\<And>i. 0 \<le> ?M (F i)" by auto
   2.520 -        ultimately show ?thesis
   2.521 -          using suminf_PInfty[of "\<lambda>i. ?M (F i)" j] j by auto
   2.522 +      moreover have "(SUP n. ?M (F n)) = \<infinity>"
   2.523 +      proof (rule SUP_PInfty)
   2.524 +        fix n :: nat show "\<exists>k::nat\<in>UNIV. ereal n \<le> ?M (F k)"
   2.525 +        proof (induct n)
   2.526 +          case (Suc n)
   2.527 +          then guess k .. note k = this
   2.528 +          moreover have "finite (F k) \<Longrightarrow> finite (F (f k)) \<Longrightarrow> card (F k) < card (F (f k))"
   2.529 +            using `F k \<subset> F (f k)` by (simp add: psubset_card_mono)
   2.530 +          moreover have "finite (F (f k)) \<Longrightarrow> finite (F k)"
   2.531 +            using `k \<le> f k` `incseq F` by (auto simp: incseq_def dest: finite_subset)
   2.532 +          ultimately show ?case
   2.533 +            by (auto intro!: exI[of _ "f k"])
   2.534 +        qed auto
   2.535        qed
   2.536 +
   2.537 +      moreover
   2.538 +      have "inj (\<lambda>n. F ((f ^^ n) 0))"
   2.539 +        by (intro strict_mono_imp_inj_on strict_monoI_Suc) (simp add: *)
   2.540 +      then have 1: "infinite (range (\<lambda>i. F ((f ^^ i) 0)))"
   2.541 +        by (rule range_inj_infinite)
   2.542 +      have "infinite (Pow (\<Union>i. F i))"
   2.543 +        by (rule infinite_super[OF _ 1]) auto
   2.544 +      then have "infinite (\<Union>i. F i)"
   2.545 +        by auto
   2.546 +      
   2.547 +      ultimately show ?thesis by auto
   2.548 +    qed
   2.549    qed
   2.550 -  show "X \<in> Pow A" using `X \<subseteq> A` by simp
   2.551  qed
   2.552  
   2.553  lemma emeasure_count_space_finite[simp]:
     3.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:14 2012 +0200
     3.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:15 2012 +0200
     3.3 @@ -1292,11 +1292,11 @@
     3.4  
     3.5  lemma measurable_If_set:
     3.6    assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
     3.7 -  assumes P: "A \<in> sets M"
     3.8 +  assumes P: "A \<inter> space M \<in> sets M"
     3.9    shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
    3.10  proof (rule measurable_If[OF measure])
    3.11 -  have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto
    3.12 -  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto
    3.13 +  have "{x \<in> space M. x \<in> A} = A \<inter> space M" by auto
    3.14 +  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<inter> space M \<in> sets M` by auto
    3.15  qed
    3.16  
    3.17  lemma measurable_ident[intro, simp]: "id \<in> measurable M M"