author hoelzl Wed Oct 10 12:12:15 2012 +0200 (2012-10-10) changeset 49773 16907431e477 parent 49772 75660d89c339 child 49774 dfa8ddb874ce
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
```     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.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.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"
```