src/HOL/Probability/Measure_Space.thy
author hoelzl
Wed Dec 05 15:59:08 2012 +0100 (2012-12-05)
changeset 50387 3d8863c41fe8
parent 50244 de72bbe42190
child 50419 3177d0374701
permissions -rw-r--r--
Move the measurability prover to its own file
     1 (*  Title:      HOL/Probability/Measure_Space.thy
     2     Author:     Lawrence C Paulson
     3     Author:     Johannes Hölzl, TU München
     4     Author:     Armin Heller, TU München
     5 *)
     6 
     7 header {* Measure spaces and their properties *}
     8 
     9 theory Measure_Space
    10 imports
    11   Measurable
    12   "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
    13 begin
    14 
    15 lemma sums_def2:
    16   "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
    17   unfolding sums_def
    18   apply (subst LIMSEQ_Suc_iff[symmetric])
    19   unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    20 
    21 subsection "Relate extended reals and the indicator function"
    22 
    23 lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
    24   by (auto simp: indicator_def one_ereal_def)
    25 
    26 lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
    27   unfolding indicator_def by auto
    28 
    29 lemma LIMSEQ_indicator_UN:
    30   "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
    31 proof cases
    32   assume "\<exists>i. x \<in> A i" then guess i .. note i = this
    33   then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
    34     "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
    35   show ?thesis
    36     apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
    37 qed (auto simp: indicator_def)
    38 
    39 lemma indicator_add:
    40   "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
    41   unfolding indicator_def by auto
    42 
    43 lemma suminf_cmult_indicator:
    44   fixes f :: "nat \<Rightarrow> ereal"
    45   assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
    46   shows "(\<Sum>n. f n * indicator (A n) x) = f i"
    47 proof -
    48   have **: "\<And>n. f n * indicator (A n) x = (if n = i then f n else 0 :: ereal)"
    49     using `x \<in> A i` assms unfolding disjoint_family_on_def indicator_def by auto
    50   then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
    51     by (auto simp: setsum_cases)
    52   moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
    53   proof (rule ereal_SUPI)
    54     fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
    55     from this[of "Suc i"] show "f i \<le> y" by auto
    56   qed (insert assms, simp)
    57   ultimately show ?thesis using assms
    58     by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def)
    59 qed
    60 
    61 lemma suminf_indicator:
    62   assumes "disjoint_family A"
    63   shows "(\<Sum>n. indicator (A n) x :: ereal) = indicator (\<Union>i. A i) x"
    64 proof cases
    65   assume *: "x \<in> (\<Union>i. A i)"
    66   then obtain i where "x \<in> A i" by auto
    67   from suminf_cmult_indicator[OF assms(1), OF `x \<in> A i`, of "\<lambda>k. 1"]
    68   show ?thesis using * by simp
    69 qed simp
    70 
    71 text {*
    72   The type for emeasure spaces is already defined in @{theory Sigma_Algebra}, as it is also used to
    73   represent sigma algebras (with an arbitrary emeasure).
    74 *}
    75 
    76 section "Extend binary sets"
    77 
    78 lemma LIMSEQ_binaryset:
    79   assumes f: "f {} = 0"
    80   shows  "(\<lambda>n. \<Sum>i<n. f (binaryset A B i)) ----> f A + f B"
    81 proof -
    82   have "(\<lambda>n. \<Sum>i < Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
    83     proof
    84       fix n
    85       show "(\<Sum>i < Suc (Suc n). f (binaryset A B i)) = f A + f B"
    86         by (induct n)  (auto simp add: binaryset_def f)
    87     qed
    88   moreover
    89   have "... ----> f A + f B" by (rule tendsto_const)
    90   ultimately
    91   have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
    92     by metis
    93   hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) ----> f A + f B"
    94     by simp
    95   thus ?thesis by (rule LIMSEQ_offset [where k=2])
    96 qed
    97 
    98 lemma binaryset_sums:
    99   assumes f: "f {} = 0"
   100   shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
   101     by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan)
   102 
   103 lemma suminf_binaryset_eq:
   104   fixes f :: "'a set \<Rightarrow> 'b::{comm_monoid_add, t2_space}"
   105   shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
   106   by (metis binaryset_sums sums_unique)
   107 
   108 section {* Properties of a premeasure @{term \<mu>} *}
   109 
   110 text {*
   111   The definitions for @{const positive} and @{const countably_additive} should be here, by they are
   112   necessary to define @{typ "'a measure"} in @{theory Sigma_Algebra}.
   113 *}
   114 
   115 definition additive where
   116   "additive M \<mu> \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> \<mu> (x \<union> y) = \<mu> x + \<mu> y)"
   117 
   118 definition increasing where
   119   "increasing M \<mu> \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<subseteq> y \<longrightarrow> \<mu> x \<le> \<mu> y)"
   120 
   121 lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
   122 lemma positiveD2: "positive M f \<Longrightarrow> A \<in> M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
   123 
   124 lemma positiveD_empty:
   125   "positive M f \<Longrightarrow> f {} = 0"
   126   by (auto simp add: positive_def)
   127 
   128 lemma additiveD:
   129   "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) = f x + f y"
   130   by (auto simp add: additive_def)
   131 
   132 lemma increasingD:
   133   "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>M \<Longrightarrow> y\<in>M \<Longrightarrow> f x \<le> f y"
   134   by (auto simp add: increasing_def)
   135 
   136 lemma countably_additiveI[case_names countably]:
   137   "(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
   138   \<Longrightarrow> countably_additive M f"
   139   by (simp add: countably_additive_def)
   140 
   141 lemma (in ring_of_sets) disjointed_additive:
   142   assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" "incseq A"
   143   shows "(\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
   144 proof (induct n)
   145   case (Suc n)
   146   then have "(\<Sum>i\<le>Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))"
   147     by simp
   148   also have "\<dots> = f (A n \<union> disjointed A (Suc n))"
   149     using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq)
   150   also have "A n \<union> disjointed A (Suc n) = A (Suc n)"
   151     using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq)
   152   finally show ?case .
   153 qed simp
   154 
   155 lemma (in ring_of_sets) additive_sum:
   156   fixes A:: "'i \<Rightarrow> 'a set"
   157   assumes f: "positive M f" and ad: "additive M f" and "finite S"
   158       and A: "A`S \<subseteq> M"
   159       and disj: "disjoint_family_on A S"
   160   shows  "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)"
   161 using `finite S` disj A proof induct
   162   case empty show ?case using f by (simp add: positive_def)
   163 next
   164   case (insert s S)
   165   then have "A s \<inter> (\<Union>i\<in>S. A i) = {}"
   166     by (auto simp add: disjoint_family_on_def neq_iff)
   167   moreover
   168   have "A s \<in> M" using insert by blast
   169   moreover have "(\<Union>i\<in>S. A i) \<in> M"
   170     using insert `finite S` by auto
   171   moreover
   172   ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)"
   173     using ad UNION_in_sets A by (auto simp add: additive_def)
   174   with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
   175     by (auto simp add: additive_def subset_insertI)
   176 qed
   177 
   178 lemma (in ring_of_sets) additive_increasing:
   179   assumes posf: "positive M f" and addf: "additive M f"
   180   shows "increasing M f"
   181 proof (auto simp add: increasing_def)
   182   fix x y
   183   assume xy: "x \<in> M" "y \<in> M" "x \<subseteq> y"
   184   then have "y - x \<in> M" by auto
   185   then have "0 \<le> f (y-x)" using posf[unfolded positive_def] by auto
   186   then have "f x + 0 \<le> f x + f (y-x)" by (intro add_left_mono) auto
   187   also have "... = f (x \<union> (y-x))" using addf
   188     by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
   189   also have "... = f y"
   190     by (metis Un_Diff_cancel Un_absorb1 xy(3))
   191   finally show "f x \<le> f y" by simp
   192 qed
   193 
   194 lemma (in ring_of_sets) subadditive:
   195   assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" and S: "finite S"
   196   shows "f (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. f (A i))"
   197 using S
   198 proof (induct S)
   199   case empty thus ?case using f by (auto simp: positive_def)
   200 next
   201   case (insert x F)
   202   hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i) - A x \<in> M" using A by force+
   203   have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
   204   have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
   205   hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
   206     by simp
   207   also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
   208     using f(2) by (rule additiveD) (insert in_M, auto)
   209   also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
   210     using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
   211   also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
   212   finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
   213 qed
   214 
   215 lemma (in ring_of_sets) countably_additive_additive:
   216   assumes posf: "positive M f" and ca: "countably_additive M f"
   217   shows "additive M f"
   218 proof (auto simp add: additive_def)
   219   fix x y
   220   assume x: "x \<in> M" and y: "y \<in> M" and "x \<inter> y = {}"
   221   hence "disjoint_family (binaryset x y)"
   222     by (auto simp add: disjoint_family_on_def binaryset_def)
   223   hence "range (binaryset x y) \<subseteq> M \<longrightarrow>
   224          (\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
   225          f (\<Union>i. binaryset x y i) = (\<Sum> n. f (binaryset x y n))"
   226     using ca
   227     by (simp add: countably_additive_def)
   228   hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow>
   229          f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
   230     by (simp add: range_binaryset_eq UN_binaryset_eq)
   231   thus "f (x \<union> y) = f x + f y" using posf x y
   232     by (auto simp add: Un suminf_binaryset_eq positive_def)
   233 qed
   234 
   235 lemma (in algebra) increasing_additive_bound:
   236   fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> ereal"
   237   assumes f: "positive M f" and ad: "additive M f"
   238       and inc: "increasing M f"
   239       and A: "range A \<subseteq> M"
   240       and disj: "disjoint_family A"
   241   shows  "(\<Sum>i. f (A i)) \<le> f \<Omega>"
   242 proof (safe intro!: suminf_bound)
   243   fix N
   244   note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"]
   245   have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)"
   246     using A by (intro additive_sum [OF f ad _ _]) (auto simp: disj_N)
   247   also have "... \<le> f \<Omega>" using space_closed A
   248     by (intro increasingD[OF inc] finite_UN) auto
   249   finally show "(\<Sum>i<N. f (A i)) \<le> f \<Omega>" by simp
   250 qed (insert f A, auto simp: positive_def)
   251 
   252 lemma (in ring_of_sets) countably_additiveI_finite:
   253   assumes "finite \<Omega>" "positive M \<mu>" "additive M \<mu>"
   254   shows "countably_additive M \<mu>"
   255 proof (rule countably_additiveI)
   256   fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> M" "(\<Union>i. F i) \<in> M" and disj: "disjoint_family F"
   257 
   258   have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto
   259   from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto
   260 
   261   have inj_f: "inj_on f {i. F i \<noteq> {}}"
   262   proof (rule inj_onI, simp)
   263     fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}"
   264     then have "f i \<in> F i" "f j \<in> F j" using f by force+
   265     with disj * show "i = j" by (auto simp: disjoint_family_on_def)
   266   qed
   267   have "finite (\<Union>i. F i)"
   268     by (metis F(2) assms(1) infinite_super sets_into_space)
   269 
   270   have F_subset: "{i. \<mu> (F i) \<noteq> 0} \<subseteq> {i. F i \<noteq> {}}"
   271     by (auto simp: positiveD_empty[OF `positive M \<mu>`])
   272   moreover have fin_not_empty: "finite {i. F i \<noteq> {}}"
   273   proof (rule finite_imageD)
   274     from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto
   275     then show "finite (f`{i. F i \<noteq> {}})"
   276       by (rule finite_subset) fact
   277   qed fact
   278   ultimately have fin_not_0: "finite {i. \<mu> (F i) \<noteq> 0}"
   279     by (rule finite_subset)
   280 
   281   have disj_not_empty: "disjoint_family_on F {i. F i \<noteq> {}}"
   282     using disj by (auto simp: disjoint_family_on_def)
   283 
   284   from fin_not_0 have "(\<Sum>i. \<mu> (F i)) = (\<Sum>i | \<mu> (F i) \<noteq> 0. \<mu> (F i))"
   285     by (rule suminf_finite) auto
   286   also have "\<dots> = (\<Sum>i | F i \<noteq> {}. \<mu> (F i))"
   287     using fin_not_empty F_subset by (rule setsum_mono_zero_left) auto
   288   also have "\<dots> = \<mu> (\<Union>i\<in>{i. F i \<noteq> {}}. F i)"
   289     using `positive M \<mu>` `additive M \<mu>` fin_not_empty disj_not_empty F by (intro additive_sum) auto
   290   also have "\<dots> = \<mu> (\<Union>i. F i)"
   291     by (rule arg_cong[where f=\<mu>]) auto
   292   finally show "(\<Sum>i. \<mu> (F i)) = \<mu> (\<Union>i. F i)" .
   293 qed
   294 
   295 lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
   296   assumes f: "positive M f" "additive M f"
   297   shows "countably_additive M f \<longleftrightarrow>
   298     (\<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))"
   299   unfolding countably_additive_def
   300 proof safe
   301   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)"
   302   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
   303   then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
   304   with count_sum[THEN spec, of "disjointed A"] A(3)
   305   have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
   306     by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
   307   moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
   308     using f(1)[unfolded positive_def] dA
   309     by (auto intro!: summable_sumr_LIMSEQ_suminf summable_ereal_pos)
   310   from LIMSEQ_Suc[OF this]
   311   have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
   312     unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
   313   moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
   314     using disjointed_additive[OF f A(1,2)] .
   315   ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
   316 next
   317   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)"
   318   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
   319   have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
   320   have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
   321   proof (unfold *[symmetric], intro cont[rule_format])
   322     show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> M"
   323       using A * by auto
   324   qed (force intro!: incseq_SucI)
   325   moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
   326     using A
   327     by (intro additive_sum[OF f, of _ A, symmetric])
   328        (auto intro: disjoint_family_on_mono[where B=UNIV])
   329   ultimately
   330   have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
   331     unfolding sums_def2 by simp
   332   from sums_unique[OF this]
   333   show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
   334 qed
   335 
   336 lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
   337   assumes f: "positive M f" "additive M f"
   338   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))
   339      \<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)"
   340 proof safe
   341   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))"
   342   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>"
   343   with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
   344     using `positive M f`[unfolded positive_def] by auto
   345 next
   346   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"
   347   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>"
   348 
   349   have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
   350     using additive_increasing[OF f] unfolding increasing_def by simp
   351 
   352   have decseq_fA: "decseq (\<lambda>i. f (A i))"
   353     using A by (auto simp: decseq_def intro!: f_mono)
   354   have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
   355     using A by (auto simp: decseq_def)
   356   then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
   357     using A unfolding decseq_def by (auto intro!: f_mono Diff)
   358   have "f (\<Inter>x. A x) \<le> f (A 0)"
   359     using A by (auto intro!: f_mono)
   360   then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
   361     using A by auto
   362   { fix i
   363     have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
   364     then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
   365       using A by auto }
   366   note f_fin = this
   367   have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
   368   proof (intro cont[rule_format, OF _ decseq _ f_fin])
   369     show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
   370       using A by auto
   371   qed
   372   from INF_Lim_ereal[OF decseq_f this]
   373   have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
   374   moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
   375     by auto
   376   ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
   377     using A(4) f_fin f_Int_fin
   378     by (subst INFI_ereal_add) (auto simp: decseq_f)
   379   moreover {
   380     fix n
   381     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))"
   382       using A by (subst f(2)[THEN additiveD]) auto
   383     also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
   384       by auto
   385     finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
   386   ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
   387     by simp
   388   with LIMSEQ_ereal_INFI[OF decseq_fA]
   389   show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
   390 qed
   391 
   392 lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
   393   assumes f: "positive M f" "additive M f" "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   394   assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   395   assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
   396   shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   397 proof -
   398   have "\<forall>A\<in>M. \<exists>x. f A = ereal x"
   399   proof
   400     fix A assume "A \<in> M" with f show "\<exists>x. f A = ereal x"
   401       unfolding positive_def by (cases "f A") auto
   402   qed
   403   from bchoice[OF this] guess f' .. note f' = this[rule_format]
   404   from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
   405     by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
   406   moreover
   407   { fix i
   408     have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
   409       using A by (intro f(2)[THEN additiveD, symmetric]) auto
   410     also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
   411       by auto
   412     finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
   413       using A by (subst (asm) (1 2 3) f') auto
   414     then have "f ((\<Union>i. A i) - A i) = ereal (f' (\<Union>i. A i) - f' (A i))"
   415       using A f' by auto }
   416   ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
   417     by (simp add: zero_ereal_def)
   418   then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
   419     by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const])
   420   then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   421     using A by (subst (1 2) f') auto
   422 qed
   423 
   424 lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
   425   assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>M. f A \<noteq> \<infinity>"
   426   assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   427   shows "countably_additive M f"
   428   using countably_additive_iff_continuous_from_below[OF f]
   429   using empty_continuous_imp_continuous_from_below[OF f fin] cont
   430   by blast
   431 
   432 section {* Properties of @{const emeasure} *}
   433 
   434 lemma emeasure_positive: "positive (sets M) (emeasure M)"
   435   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
   436 
   437 lemma emeasure_empty[simp, intro]: "emeasure M {} = 0"
   438   using emeasure_positive[of M] by (simp add: positive_def)
   439 
   440 lemma emeasure_nonneg[intro!]: "0 \<le> emeasure M A"
   441   using emeasure_notin_sets[of A M] emeasure_positive[of M]
   442   by (cases "A \<in> sets M") (auto simp: positive_def)
   443 
   444 lemma emeasure_not_MInf[simp]: "emeasure M A \<noteq> - \<infinity>"
   445   using emeasure_nonneg[of M A] by auto
   446   
   447 lemma emeasure_countably_additive: "countably_additive (sets M) (emeasure M)"
   448   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
   449 
   450 lemma suminf_emeasure:
   451   "range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
   452   using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
   453   by (simp add: countably_additive_def)
   454 
   455 lemma emeasure_additive: "additive (sets M) (emeasure M)"
   456   by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)
   457 
   458 lemma plus_emeasure:
   459   "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
   460   using additiveD[OF emeasure_additive] ..
   461 
   462 lemma setsum_emeasure:
   463   "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
   464     (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
   465   by (metis sets.additive_sum emeasure_positive emeasure_additive)
   466 
   467 lemma emeasure_mono:
   468   "a \<subseteq> b \<Longrightarrow> b \<in> sets M \<Longrightarrow> emeasure M a \<le> emeasure M b"
   469   by (metis sets.additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
   470             emeasure_positive increasingD)
   471 
   472 lemma emeasure_space:
   473   "emeasure M A \<le> emeasure M (space M)"
   474   by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets.sets_into_space sets.top)
   475 
   476 lemma emeasure_compl:
   477   assumes s: "s \<in> sets M" and fin: "emeasure M s \<noteq> \<infinity>"
   478   shows "emeasure M (space M - s) = emeasure M (space M) - emeasure M s"
   479 proof -
   480   from s have "0 \<le> emeasure M s" by auto
   481   have "emeasure M (space M) = emeasure M (s \<union> (space M - s))" using s
   482     by (metis Un_Diff_cancel Un_absorb1 s sets.sets_into_space)
   483   also have "... = emeasure M s + emeasure M (space M - s)"
   484     by (rule plus_emeasure[symmetric]) (auto simp add: s)
   485   finally have "emeasure M (space M) = emeasure M s + emeasure M (space M - s)" .
   486   then show ?thesis
   487     using fin `0 \<le> emeasure M s`
   488     unfolding ereal_eq_minus_iff by (auto simp: ac_simps)
   489 qed
   490 
   491 lemma emeasure_Diff:
   492   assumes finite: "emeasure M B \<noteq> \<infinity>"
   493   and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
   494   shows "emeasure M (A - B) = emeasure M A - emeasure M B"
   495 proof -
   496   have "0 \<le> emeasure M B" using assms by auto
   497   have "(A - B) \<union> B = A" using `B \<subseteq> A` by auto
   498   then have "emeasure M A = emeasure M ((A - B) \<union> B)" by simp
   499   also have "\<dots> = emeasure M (A - B) + emeasure M B"
   500     by (subst plus_emeasure[symmetric]) auto
   501   finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
   502     unfolding ereal_eq_minus_iff
   503     using finite `0 \<le> emeasure M B` by auto
   504 qed
   505 
   506 lemma Lim_emeasure_incseq:
   507   "range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
   508   using emeasure_countably_additive
   509   by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
   510     emeasure_additive)
   511 
   512 lemma incseq_emeasure:
   513   assumes "range B \<subseteq> sets M" "incseq B"
   514   shows "incseq (\<lambda>i. emeasure M (B i))"
   515   using assms by (auto simp: incseq_def intro!: emeasure_mono)
   516 
   517 lemma SUP_emeasure_incseq:
   518   assumes A: "range A \<subseteq> sets M" "incseq A"
   519   shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
   520   using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
   521   by (simp add: LIMSEQ_unique)
   522 
   523 lemma decseq_emeasure:
   524   assumes "range B \<subseteq> sets M" "decseq B"
   525   shows "decseq (\<lambda>i. emeasure M (B i))"
   526   using assms by (auto simp: decseq_def intro!: emeasure_mono)
   527 
   528 lemma INF_emeasure_decseq:
   529   assumes A: "range A \<subseteq> sets M" and "decseq A"
   530   and finite: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   531   shows "(INF n. emeasure M (A n)) = emeasure M (\<Inter>i. A i)"
   532 proof -
   533   have le_MI: "emeasure M (\<Inter>i. A i) \<le> emeasure M (A 0)"
   534     using A by (auto intro!: emeasure_mono)
   535   hence *: "emeasure M (\<Inter>i. A i) \<noteq> \<infinity>" using finite[of 0] by auto
   536 
   537   have A0: "0 \<le> emeasure M (A 0)" using A by auto
   538 
   539   have "emeasure M (A 0) - (INF n. emeasure M (A n)) = emeasure M (A 0) + (SUP n. - emeasure M (A n))"
   540     by (simp add: ereal_SUPR_uminus minus_ereal_def)
   541   also have "\<dots> = (SUP n. emeasure M (A 0) - emeasure M (A n))"
   542     unfolding minus_ereal_def using A0 assms
   543     by (subst SUPR_ereal_add) (auto simp add: decseq_emeasure)
   544   also have "\<dots> = (SUP n. emeasure M (A 0 - A n))"
   545     using A finite `decseq A`[unfolded decseq_def] by (subst emeasure_Diff) auto
   546   also have "\<dots> = emeasure M (\<Union>i. A 0 - A i)"
   547   proof (rule SUP_emeasure_incseq)
   548     show "range (\<lambda>n. A 0 - A n) \<subseteq> sets M"
   549       using A by auto
   550     show "incseq (\<lambda>n. A 0 - A n)"
   551       using `decseq A` by (auto simp add: incseq_def decseq_def)
   552   qed
   553   also have "\<dots> = emeasure M (A 0) - emeasure M (\<Inter>i. A i)"
   554     using A finite * by (simp, subst emeasure_Diff) auto
   555   finally show ?thesis
   556     unfolding ereal_minus_eq_minus_iff using finite A0 by auto
   557 qed
   558 
   559 lemma Lim_emeasure_decseq:
   560   assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   561   shows "(\<lambda>i. emeasure M (A i)) ----> emeasure M (\<Inter>i. A i)"
   562   using LIMSEQ_ereal_INFI[OF decseq_emeasure, OF A]
   563   using INF_emeasure_decseq[OF A fin] by simp
   564 
   565 lemma emeasure_subadditive:
   566   assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
   567   shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
   568 proof -
   569   from plus_emeasure[of A M "B - A"]
   570   have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)" by simp
   571   also have "\<dots> \<le> emeasure M A + emeasure M B"
   572     using assms by (auto intro!: add_left_mono emeasure_mono)
   573   finally show ?thesis .
   574 qed
   575 
   576 lemma emeasure_subadditive_finite:
   577   assumes "finite I" "A ` I \<subseteq> sets M"
   578   shows "emeasure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. emeasure M (A i))"
   579 using assms proof induct
   580   case (insert i I)
   581   then have "emeasure M (\<Union>i\<in>insert i I. A i) = emeasure M (A i \<union> (\<Union>i\<in>I. A i))"
   582     by simp
   583   also have "\<dots> \<le> emeasure M (A i) + emeasure M (\<Union>i\<in>I. A i)"
   584     using insert by (intro emeasure_subadditive) auto
   585   also have "\<dots> \<le> emeasure M (A i) + (\<Sum>i\<in>I. emeasure M (A i))"
   586     using insert by (intro add_mono) auto
   587   also have "\<dots> = (\<Sum>i\<in>insert i I. emeasure M (A i))"
   588     using insert by auto
   589   finally show ?case .
   590 qed simp
   591 
   592 lemma emeasure_subadditive_countably:
   593   assumes "range f \<subseteq> sets M"
   594   shows "emeasure M (\<Union>i. f i) \<le> (\<Sum>i. emeasure M (f i))"
   595 proof -
   596   have "emeasure M (\<Union>i. f i) = emeasure M (\<Union>i. disjointed f i)"
   597     unfolding UN_disjointed_eq ..
   598   also have "\<dots> = (\<Sum>i. emeasure M (disjointed f i))"
   599     using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
   600     by (simp add:  disjoint_family_disjointed comp_def)
   601   also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))"
   602     using sets.range_disjointed_sets[OF assms] assms
   603     by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset)
   604   finally show ?thesis .
   605 qed
   606 
   607 lemma emeasure_insert:
   608   assumes sets: "{x} \<in> sets M" "A \<in> sets M" and "x \<notin> A"
   609   shows "emeasure M (insert x A) = emeasure M {x} + emeasure M A"
   610 proof -
   611   have "{x} \<inter> A = {}" using `x \<notin> A` by auto
   612   from plus_emeasure[OF sets this] show ?thesis by simp
   613 qed
   614 
   615 lemma emeasure_eq_setsum_singleton:
   616   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
   617   shows "emeasure M S = (\<Sum>x\<in>S. emeasure M {x})"
   618   using setsum_emeasure[of "\<lambda>x. {x}" S M] assms
   619   by (auto simp: disjoint_family_on_def subset_eq)
   620 
   621 lemma setsum_emeasure_cover:
   622   assumes "finite S" and "A \<in> sets M" and br_in_M: "B ` S \<subseteq> sets M"
   623   assumes A: "A \<subseteq> (\<Union>i\<in>S. B i)"
   624   assumes disj: "disjoint_family_on B S"
   625   shows "emeasure M A = (\<Sum>i\<in>S. emeasure M (A \<inter> (B i)))"
   626 proof -
   627   have "(\<Sum>i\<in>S. emeasure M (A \<inter> (B i))) = emeasure M (\<Union>i\<in>S. A \<inter> (B i))"
   628   proof (rule setsum_emeasure)
   629     show "disjoint_family_on (\<lambda>i. A \<inter> B i) S"
   630       using `disjoint_family_on B S`
   631       unfolding disjoint_family_on_def by auto
   632   qed (insert assms, auto)
   633   also have "(\<Union>i\<in>S. A \<inter> (B i)) = A"
   634     using A by auto
   635   finally show ?thesis by simp
   636 qed
   637 
   638 lemma emeasure_eq_0:
   639   "N \<in> sets M \<Longrightarrow> emeasure M N = 0 \<Longrightarrow> K \<subseteq> N \<Longrightarrow> emeasure M K = 0"
   640   by (metis emeasure_mono emeasure_nonneg order_eq_iff)
   641 
   642 lemma emeasure_UN_eq_0:
   643   assumes "\<And>i::nat. emeasure M (N i) = 0" and "range N \<subseteq> sets M"
   644   shows "emeasure M (\<Union> i. N i) = 0"
   645 proof -
   646   have "0 \<le> emeasure M (\<Union> i. N i)" using assms by auto
   647   moreover have "emeasure M (\<Union> i. N i) \<le> 0"
   648     using emeasure_subadditive_countably[OF assms(2)] assms(1) by simp
   649   ultimately show ?thesis by simp
   650 qed
   651 
   652 lemma measure_eqI_finite:
   653   assumes [simp]: "sets M = Pow A" "sets N = Pow A" and "finite A"
   654   assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
   655   shows "M = N"
   656 proof (rule measure_eqI)
   657   fix X assume "X \<in> sets M"
   658   then have X: "X \<subseteq> A" by auto
   659   then have "emeasure M X = (\<Sum>a\<in>X. emeasure M {a})"
   660     using `finite A` by (subst emeasure_eq_setsum_singleton) (auto dest: finite_subset)
   661   also have "\<dots> = (\<Sum>a\<in>X. emeasure N {a})"
   662     using X eq by (auto intro!: setsum_cong)
   663   also have "\<dots> = emeasure N X"
   664     using X `finite A` by (subst emeasure_eq_setsum_singleton) (auto dest: finite_subset)
   665   finally show "emeasure M X = emeasure N X" .
   666 qed simp
   667 
   668 lemma measure_eqI_generator_eq:
   669   fixes M N :: "'a measure" and E :: "'a set set" and A :: "nat \<Rightarrow> 'a set"
   670   assumes "Int_stable E" "E \<subseteq> Pow \<Omega>"
   671   and eq: "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X"
   672   and M: "sets M = sigma_sets \<Omega> E"
   673   and N: "sets N = sigma_sets \<Omega> E"
   674   and A: "range A \<subseteq> E" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   675   shows "M = N"
   676 proof -
   677   let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
   678   interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
   679   have "space M = \<Omega>"
   680     using sets.top[of M] sets.space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E`
   681     by blast
   682 
   683   { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
   684     then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
   685     have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
   686     assume "D \<in> sets M"
   687     with `Int_stable E` `E \<subseteq> Pow \<Omega>` have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
   688       unfolding M
   689     proof (induct rule: sigma_sets_induct_disjoint)
   690       case (basic A)
   691       then have "F \<inter> A \<in> E" using `Int_stable E` `F \<in> E` by (auto simp: Int_stable_def)
   692       then show ?case using eq by auto
   693     next
   694       case empty then show ?case by simp
   695     next
   696       case (compl A)
   697       then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
   698         and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
   699         using `F \<in> E` S.sets_into_space by (auto simp: M)
   700       have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
   701       then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
   702       have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
   703       then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
   704       then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
   705         using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
   706       also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` compl by simp
   707       also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
   708         using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
   709         by (auto intro!: emeasure_Diff[symmetric] simp: M N)
   710       finally show ?case
   711         using `space M = \<Omega>` by auto
   712     next
   713       case (union A)
   714       then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
   715         by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
   716       with A show ?case
   717         by auto
   718     qed }
   719   note * = this
   720   show "M = N"
   721   proof (rule measure_eqI)
   722     show "sets M = sets N"
   723       using M N by simp
   724     have [simp, intro]: "\<And>i. A i \<in> sets M"
   725       using A(1) by (auto simp: subset_eq M)
   726     fix F assume "F \<in> sets M"
   727     let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
   728     from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
   729       using `F \<in> sets M`[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
   730     have [simp, intro]: "\<And>i. ?D i \<in> sets M"
   731       using sets.range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
   732       by (auto simp: subset_eq)
   733     have "disjoint_family ?D"
   734       by (auto simp: disjoint_family_disjointed)
   735     moreover
   736     have "(\<Sum>i. emeasure M (?D i)) = (\<Sum>i. emeasure N (?D i))"
   737     proof (intro arg_cong[where f=suminf] ext)
   738       fix i
   739       have "A i \<inter> ?D i = ?D i"
   740         by (auto simp: disjointed_def)
   741       then show "emeasure M (?D i) = emeasure N (?D i)"
   742         using *[of "A i" "?D i", OF _ A(3)] A(1) by auto
   743     qed
   744     ultimately show "emeasure M F = emeasure N F"
   745       by (simp add: image_subset_iff `sets M = sets N`[symmetric] F_eq[symmetric] suminf_emeasure)
   746   qed
   747 qed
   748 
   749 lemma measure_of_of_measure: "measure_of (space M) (sets M) (emeasure M) = M"
   750 proof (intro measure_eqI emeasure_measure_of_sigma)
   751   show "sigma_algebra (space M) (sets M)" ..
   752   show "positive (sets M) (emeasure M)"
   753     by (simp add: positive_def emeasure_nonneg)
   754   show "countably_additive (sets M) (emeasure M)"
   755     by (simp add: emeasure_countably_additive)
   756 qed simp_all
   757 
   758 section "@{text \<mu>}-null sets"
   759 
   760 definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
   761   "null_sets M = {N\<in>sets M. emeasure M N = 0}"
   762 
   763 lemma null_setsD1[dest]: "A \<in> null_sets M \<Longrightarrow> emeasure M A = 0"
   764   by (simp add: null_sets_def)
   765 
   766 lemma null_setsD2[dest]: "A \<in> null_sets M \<Longrightarrow> A \<in> sets M"
   767   unfolding null_sets_def by simp
   768 
   769 lemma null_setsI[intro]: "emeasure M A = 0 \<Longrightarrow> A \<in> sets M \<Longrightarrow> A \<in> null_sets M"
   770   unfolding null_sets_def by simp
   771 
   772 interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
   773 proof (rule ring_of_setsI)
   774   show "null_sets M \<subseteq> Pow (space M)"
   775     using sets.sets_into_space by auto
   776   show "{} \<in> null_sets M"
   777     by auto
   778   fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
   779   then have "A \<in> sets M" "B \<in> sets M"
   780     by auto
   781   moreover then have "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
   782     "emeasure M (A - B) \<le> emeasure M A"
   783     by (auto intro!: emeasure_subadditive emeasure_mono)
   784   moreover have "emeasure M B = 0" "emeasure M A = 0"
   785     using sets by auto
   786   ultimately show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
   787     by (auto intro!: antisym)
   788 qed
   789 
   790 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
   791 proof -
   792   have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
   793     unfolding SUP_def image_compose
   794     unfolding surj_from_nat ..
   795   then show ?thesis by simp
   796 qed
   797 
   798 lemma null_sets_UN[intro]:
   799   assumes "\<And>i::'i::countable. N i \<in> null_sets M"
   800   shows "(\<Union>i. N i) \<in> null_sets M"
   801 proof (intro conjI CollectI null_setsI)
   802   show "(\<Union>i. N i) \<in> sets M" using assms by auto
   803   have "0 \<le> emeasure M (\<Union>i. N i)" by (rule emeasure_nonneg)
   804   moreover have "emeasure M (\<Union>i. N i) \<le> (\<Sum>n. emeasure M (N (Countable.from_nat n)))"
   805     unfolding UN_from_nat[of N]
   806     using assms by (intro emeasure_subadditive_countably) auto
   807   ultimately show "emeasure M (\<Union>i. N i) = 0"
   808     using assms by (auto simp: null_setsD1)
   809 qed
   810 
   811 lemma null_set_Int1:
   812   assumes "B \<in> null_sets M" "A \<in> sets M" shows "A \<inter> B \<in> null_sets M"
   813 proof (intro CollectI conjI null_setsI)
   814   show "emeasure M (A \<inter> B) = 0" using assms
   815     by (intro emeasure_eq_0[of B _ "A \<inter> B"]) auto
   816 qed (insert assms, auto)
   817 
   818 lemma null_set_Int2:
   819   assumes "B \<in> null_sets M" "A \<in> sets M" shows "B \<inter> A \<in> null_sets M"
   820   using assms by (subst Int_commute) (rule null_set_Int1)
   821 
   822 lemma emeasure_Diff_null_set:
   823   assumes "B \<in> null_sets M" "A \<in> sets M"
   824   shows "emeasure M (A - B) = emeasure M A"
   825 proof -
   826   have *: "A - B = (A - (A \<inter> B))" by auto
   827   have "A \<inter> B \<in> null_sets M" using assms by (rule null_set_Int1)
   828   then show ?thesis
   829     unfolding * using assms
   830     by (subst emeasure_Diff) auto
   831 qed
   832 
   833 lemma null_set_Diff:
   834   assumes "B \<in> null_sets M" "A \<in> sets M" shows "B - A \<in> null_sets M"
   835 proof (intro CollectI conjI null_setsI)
   836   show "emeasure M (B - A) = 0" using assms by (intro emeasure_eq_0[of B _ "B - A"]) auto
   837 qed (insert assms, auto)
   838 
   839 lemma emeasure_Un_null_set:
   840   assumes "A \<in> sets M" "B \<in> null_sets M"
   841   shows "emeasure M (A \<union> B) = emeasure M A"
   842 proof -
   843   have *: "A \<union> B = A \<union> (B - A)" by auto
   844   have "B - A \<in> null_sets M" using assms(2,1) by (rule null_set_Diff)
   845   then show ?thesis
   846     unfolding * using assms
   847     by (subst plus_emeasure[symmetric]) auto
   848 qed
   849 
   850 section "Formalize almost everywhere"
   851 
   852 definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
   853   "ae_filter M = Abs_filter (\<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
   854 
   855 abbreviation
   856   almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   857   "almost_everywhere M P \<equiv> eventually P (ae_filter M)"
   858 
   859 syntax
   860   "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
   861 
   862 translations
   863   "AE x in M. P" == "CONST almost_everywhere M (%x. P)"
   864 
   865 lemma eventually_ae_filter:
   866   fixes M P
   867   defines [simp]: "F \<equiv> \<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N" 
   868   shows "eventually P (ae_filter M) \<longleftrightarrow> F P"
   869   unfolding ae_filter_def F_def[symmetric]
   870 proof (rule eventually_Abs_filter)
   871   show "is_filter F"
   872   proof
   873     fix P Q assume "F P" "F Q"
   874     then obtain N L where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N"
   875       and L: "L \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> L"
   876       by auto
   877     then have "L \<union> N \<in> null_sets M" "{x \<in> space M. \<not> (P x \<and> Q x)} \<subseteq> L \<union> N" by auto
   878     then show "F (\<lambda>x. P x \<and> Q x)" by auto
   879   next
   880     fix P Q assume "F P"
   881     then obtain N where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N" by auto
   882     moreover assume "\<forall>x. P x \<longrightarrow> Q x"
   883     ultimately have "N \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> N" by auto
   884     then show "F Q" by auto
   885   qed auto
   886 qed
   887 
   888 lemma AE_I':
   889   "N \<in> null_sets M \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x in M. P x)"
   890   unfolding eventually_ae_filter by auto
   891 
   892 lemma AE_iff_null:
   893   assumes "{x\<in>space M. \<not> P x} \<in> sets M" (is "?P \<in> sets M")
   894   shows "(AE x in M. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets M"
   895 proof
   896   assume "AE x in M. P x" then obtain N where N: "N \<in> sets M" "?P \<subseteq> N" "emeasure M N = 0"
   897     unfolding eventually_ae_filter by auto
   898   have "0 \<le> emeasure M ?P" by auto
   899   moreover have "emeasure M ?P \<le> emeasure M N"
   900     using assms N(1,2) by (auto intro: emeasure_mono)
   901   ultimately have "emeasure M ?P = 0" unfolding `emeasure M N = 0` by auto
   902   then show "?P \<in> null_sets M" using assms by auto
   903 next
   904   assume "?P \<in> null_sets M" with assms show "AE x in M. P x" by (auto intro: AE_I')
   905 qed
   906 
   907 lemma AE_iff_null_sets:
   908   "N \<in> sets M \<Longrightarrow> N \<in> null_sets M \<longleftrightarrow> (AE x in M. x \<notin> N)"
   909   using Int_absorb1[OF sets.sets_into_space, of N M]
   910   by (subst AE_iff_null) (auto simp: Int_def[symmetric])
   911 
   912 lemma AE_not_in:
   913   "N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N"
   914   by (metis AE_iff_null_sets null_setsD2)
   915 
   916 lemma AE_iff_measurable:
   917   "N \<in> sets M \<Longrightarrow> {x\<in>space M. \<not> P x} = N \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> emeasure M N = 0"
   918   using AE_iff_null[of _ P] by auto
   919 
   920 lemma AE_E[consumes 1]:
   921   assumes "AE x in M. P x"
   922   obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
   923   using assms unfolding eventually_ae_filter by auto
   924 
   925 lemma AE_E2:
   926   assumes "AE x in M. P x" "{x\<in>space M. P x} \<in> sets M"
   927   shows "emeasure M {x\<in>space M. \<not> P x} = 0" (is "emeasure M ?P = 0")
   928 proof -
   929   have "{x\<in>space M. \<not> P x} = space M - {x\<in>space M. P x}" by auto
   930   with AE_iff_null[of M P] assms show ?thesis by auto
   931 qed
   932 
   933 lemma AE_I:
   934   assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
   935   shows "AE x in M. P x"
   936   using assms unfolding eventually_ae_filter by auto
   937 
   938 lemma AE_mp[elim!]:
   939   assumes AE_P: "AE x in M. P x" and AE_imp: "AE x in M. P x \<longrightarrow> Q x"
   940   shows "AE x in M. Q x"
   941 proof -
   942   from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
   943     and A: "A \<in> sets M" "emeasure M A = 0"
   944     by (auto elim!: AE_E)
   945 
   946   from AE_imp obtain B where imp: "{x\<in>space M. P x \<and> \<not> Q x} \<subseteq> B"
   947     and B: "B \<in> sets M" "emeasure M B = 0"
   948     by (auto elim!: AE_E)
   949 
   950   show ?thesis
   951   proof (intro AE_I)
   952     have "0 \<le> emeasure M (A \<union> B)" using A B by auto
   953     moreover have "emeasure M (A \<union> B) \<le> 0"
   954       using emeasure_subadditive[of A M B] A B by auto
   955     ultimately show "A \<union> B \<in> sets M" "emeasure M (A \<union> B) = 0" using A B by auto
   956     show "{x\<in>space M. \<not> Q x} \<subseteq> A \<union> B"
   957       using P imp by auto
   958   qed
   959 qed
   960 
   961 (* depricated replace by laws about eventually *)
   962 lemma
   963   shows AE_iffI: "AE x in M. P x \<Longrightarrow> AE x in M. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x in M. Q x"
   964     and AE_disjI1: "AE x in M. P x \<Longrightarrow> AE x in M. P x \<or> Q x"
   965     and AE_disjI2: "AE x in M. Q x \<Longrightarrow> AE x in M. P x \<or> Q x"
   966     and AE_conjI: "AE x in M. P x \<Longrightarrow> AE x in M. Q x \<Longrightarrow> AE x in M. P x \<and> Q x"
   967     and AE_conj_iff[simp]: "(AE x in M. P x \<and> Q x) \<longleftrightarrow> (AE x in M. P x) \<and> (AE x in M. Q x)"
   968   by auto
   969 
   970 lemma AE_impI:
   971   "(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x"
   972   by (cases P) auto
   973 
   974 lemma AE_measure:
   975   assumes AE: "AE x in M. P x" and sets: "{x\<in>space M. P x} \<in> sets M" (is "?P \<in> sets M")
   976   shows "emeasure M {x\<in>space M. P x} = emeasure M (space M)"
   977 proof -
   978   from AE_E[OF AE] guess N . note N = this
   979   with sets have "emeasure M (space M) \<le> emeasure M (?P \<union> N)"
   980     by (intro emeasure_mono) auto
   981   also have "\<dots> \<le> emeasure M ?P + emeasure M N"
   982     using sets N by (intro emeasure_subadditive) auto
   983   also have "\<dots> = emeasure M ?P" using N by simp
   984   finally show "emeasure M ?P = emeasure M (space M)"
   985     using emeasure_space[of M "?P"] by auto
   986 qed
   987 
   988 lemma AE_space: "AE x in M. x \<in> space M"
   989   by (rule AE_I[where N="{}"]) auto
   990 
   991 lemma AE_I2[simp, intro]:
   992   "(\<And>x. x \<in> space M \<Longrightarrow> P x) \<Longrightarrow> AE x in M. P x"
   993   using AE_space by force
   994 
   995 lemma AE_Ball_mp:
   996   "\<forall>x\<in>space M. P x \<Longrightarrow> AE x in M. P x \<longrightarrow> Q x \<Longrightarrow> AE x in M. Q x"
   997   by auto
   998 
   999 lemma AE_cong[cong]:
  1000   "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in M. Q x)"
  1001   by auto
  1002 
  1003 lemma AE_all_countable:
  1004   "(AE x in M. \<forall>i. P i x) \<longleftrightarrow> (\<forall>i::'i::countable. AE x in M. P i x)"
  1005 proof
  1006   assume "\<forall>i. AE x in M. P i x"
  1007   from this[unfolded eventually_ae_filter Bex_def, THEN choice]
  1008   obtain N where N: "\<And>i. N i \<in> null_sets M" "\<And>i. {x\<in>space M. \<not> P i x} \<subseteq> N i" by auto
  1009   have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. {x\<in>space M. \<not> P i x})" by auto
  1010   also have "\<dots> \<subseteq> (\<Union>i. N i)" using N by auto
  1011   finally have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. N i)" .
  1012   moreover from N have "(\<Union>i. N i) \<in> null_sets M"
  1013     by (intro null_sets_UN) auto
  1014   ultimately show "AE x in M. \<forall>i. P i x"
  1015     unfolding eventually_ae_filter by auto
  1016 qed auto
  1017 
  1018 lemma AE_finite_all:
  1019   assumes f: "finite S" shows "(AE x in M. \<forall>i\<in>S. P i x) \<longleftrightarrow> (\<forall>i\<in>S. AE x in M. P i x)"
  1020   using f by induct auto
  1021 
  1022 lemma AE_finite_allI:
  1023   assumes "finite S"
  1024   shows "(\<And>s. s \<in> S \<Longrightarrow> AE x in M. Q s x) \<Longrightarrow> AE x in M. \<forall>s\<in>S. Q s x"
  1025   using AE_finite_all[OF `finite S`] by auto
  1026 
  1027 lemma emeasure_mono_AE:
  1028   assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B"
  1029     and B: "B \<in> sets M"
  1030   shows "emeasure M A \<le> emeasure M B"
  1031 proof cases
  1032   assume A: "A \<in> sets M"
  1033   from imp obtain N where N: "{x\<in>space M. \<not> (x \<in> A \<longrightarrow> x \<in> B)} \<subseteq> N" "N \<in> null_sets M"
  1034     by (auto simp: eventually_ae_filter)
  1035   have "emeasure M A = emeasure M (A - N)"
  1036     using N A by (subst emeasure_Diff_null_set) auto
  1037   also have "emeasure M (A - N) \<le> emeasure M (B - N)"
  1038     using N A B sets.sets_into_space by (auto intro!: emeasure_mono)
  1039   also have "emeasure M (B - N) = emeasure M B"
  1040     using N B by (subst emeasure_Diff_null_set) auto
  1041   finally show ?thesis .
  1042 qed (simp add: emeasure_nonneg emeasure_notin_sets)
  1043 
  1044 lemma emeasure_eq_AE:
  1045   assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
  1046   assumes A: "A \<in> sets M" and B: "B \<in> sets M"
  1047   shows "emeasure M A = emeasure M B"
  1048   using assms by (safe intro!: antisym emeasure_mono_AE) auto
  1049 
  1050 section {* @{text \<sigma>}-finite Measures *}
  1051 
  1052 locale sigma_finite_measure =
  1053   fixes M :: "'a measure"
  1054   assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set.
  1055     range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. emeasure M (A i) \<noteq> \<infinity>)"
  1056 
  1057 lemma (in sigma_finite_measure) sigma_finite_disjoint:
  1058   obtains A :: "nat \<Rightarrow> 'a set"
  1059   where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "disjoint_family A"
  1060 proof atomize_elim
  1061   case goal1
  1062   obtain A :: "nat \<Rightarrow> 'a set" where
  1063     range: "range A \<subseteq> sets M" and
  1064     space: "(\<Union>i. A i) = space M" and
  1065     measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
  1066     using sigma_finite by auto
  1067   note range' = sets.range_disjointed_sets[OF range] range
  1068   { fix i
  1069     have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
  1070       using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
  1071     then have "emeasure M (disjointed A i) \<noteq> \<infinity>"
  1072       using measure[of i] by auto }
  1073   with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
  1074   show ?case by (auto intro!: exI[of _ "disjointed A"])
  1075 qed
  1076 
  1077 lemma (in sigma_finite_measure) sigma_finite_incseq:
  1078   obtains A :: "nat \<Rightarrow> 'a set"
  1079   where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
  1080 proof atomize_elim
  1081   case goal1
  1082   obtain F :: "nat \<Rightarrow> 'a set" where
  1083     F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
  1084     using sigma_finite by auto
  1085   then show ?case
  1086   proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
  1087     from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
  1088     then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
  1089       using F by fastforce
  1090   next
  1091     fix n
  1092     have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))" using F
  1093       by (auto intro!: emeasure_subadditive_finite)
  1094     also have "\<dots> < \<infinity>"
  1095       using F by (auto simp: setsum_Pinfty)
  1096     finally show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp
  1097   qed (force simp: incseq_def)+
  1098 qed
  1099 
  1100 section {* Measure space induced by distribution of @{const measurable}-functions *}
  1101 
  1102 definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
  1103   "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
  1104 
  1105 lemma
  1106   shows sets_distr[simp]: "sets (distr M N f) = sets N"
  1107     and space_distr[simp]: "space (distr M N f) = space N"
  1108   by (auto simp: distr_def)
  1109 
  1110 lemma
  1111   shows measurable_distr_eq1[simp]: "measurable (distr Mf Nf f) Mf' = measurable Nf Mf'"
  1112     and measurable_distr_eq2[simp]: "measurable Mg' (distr Mg Ng g) = measurable Mg' Ng"
  1113   by (auto simp: measurable_def)
  1114 
  1115 lemma emeasure_distr:
  1116   fixes f :: "'a \<Rightarrow> 'b"
  1117   assumes f: "f \<in> measurable M N" and A: "A \<in> sets N"
  1118   shows "emeasure (distr M N f) A = emeasure M (f -` A \<inter> space M)" (is "_ = ?\<mu> A")
  1119   unfolding distr_def
  1120 proof (rule emeasure_measure_of_sigma)
  1121   show "positive (sets N) ?\<mu>"
  1122     by (auto simp: positive_def)
  1123 
  1124   show "countably_additive (sets N) ?\<mu>"
  1125   proof (intro countably_additiveI)
  1126     fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets N" "disjoint_family A"
  1127     then have A: "\<And>i. A i \<in> sets N" "(\<Union>i. A i) \<in> sets N" by auto
  1128     then have *: "range (\<lambda>i. f -` (A i) \<inter> space M) \<subseteq> sets M"
  1129       using f by (auto simp: measurable_def)
  1130     moreover have "(\<Union>i. f -`  A i \<inter> space M) \<in> sets M"
  1131       using * by blast
  1132     moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
  1133       using `disjoint_family A` by (auto simp: disjoint_family_on_def)
  1134     ultimately show "(\<Sum>i. ?\<mu> (A i)) = ?\<mu> (\<Union>i. A i)"
  1135       using suminf_emeasure[OF _ **] A f
  1136       by (auto simp: comp_def vimage_UN)
  1137   qed
  1138   show "sigma_algebra (space N) (sets N)" ..
  1139 qed fact
  1140 
  1141 lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
  1142   by (rule measure_eqI) (auto simp: emeasure_distr)
  1143 
  1144 lemma measure_distr:
  1145   "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
  1146   by (simp add: emeasure_distr measure_def)
  1147 
  1148 lemma AE_distrD:
  1149   assumes f: "f \<in> measurable M M'"
  1150     and AE: "AE x in distr M M' f. P x"
  1151   shows "AE x in M. P (f x)"
  1152 proof -
  1153   from AE[THEN AE_E] guess N .
  1154   with f show ?thesis
  1155     unfolding eventually_ae_filter
  1156     by (intro bexI[of _ "f -` N \<inter> space M"])
  1157        (auto simp: emeasure_distr measurable_def)
  1158 qed
  1159 
  1160 lemma AE_distr_iff:
  1161   assumes f[measurable]: "f \<in> measurable M N" and P[measurable]: "{x \<in> space N. P x} \<in> sets N"
  1162   shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
  1163 proof (subst (1 2) AE_iff_measurable[OF _ refl])
  1164   have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
  1165     using f[THEN measurable_space] by auto
  1166   then show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
  1167     (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
  1168     by (simp add: emeasure_distr)
  1169 qed auto
  1170 
  1171 lemma null_sets_distr_iff:
  1172   "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"
  1173   by (auto simp add: null_sets_def emeasure_distr)
  1174 
  1175 lemma distr_distr:
  1176   "g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
  1177   by (auto simp add: emeasure_distr measurable_space
  1178            intro!: arg_cong[where f="emeasure M"] measure_eqI)
  1179 
  1180 section {* Real measure values *}
  1181 
  1182 lemma measure_nonneg: "0 \<le> measure M A"
  1183   using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
  1184 
  1185 lemma measure_empty[simp]: "measure M {} = 0"
  1186   unfolding measure_def by simp
  1187 
  1188 lemma emeasure_eq_ereal_measure:
  1189   "emeasure M A \<noteq> \<infinity> \<Longrightarrow> emeasure M A = ereal (measure M A)"
  1190   using emeasure_nonneg[of M A]
  1191   by (cases "emeasure M A") (auto simp: measure_def)
  1192 
  1193 lemma measure_Union:
  1194   assumes finite: "emeasure M A \<noteq> \<infinity>" "emeasure M B \<noteq> \<infinity>"
  1195   and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}"
  1196   shows "measure M (A \<union> B) = measure M A + measure M B"
  1197   unfolding measure_def
  1198   using plus_emeasure[OF measurable, symmetric] finite
  1199   by (simp add: emeasure_eq_ereal_measure)
  1200 
  1201 lemma measure_finite_Union:
  1202   assumes measurable: "A`S \<subseteq> sets M" "disjoint_family_on A S" "finite S"
  1203   assumes finite: "\<And>i. i \<in> S \<Longrightarrow> emeasure M (A i) \<noteq> \<infinity>"
  1204   shows "measure M (\<Union>i\<in>S. A i) = (\<Sum>i\<in>S. measure M (A i))"
  1205   unfolding measure_def
  1206   using setsum_emeasure[OF measurable, symmetric] finite
  1207   by (simp add: emeasure_eq_ereal_measure)
  1208 
  1209 lemma measure_Diff:
  1210   assumes finite: "emeasure M A \<noteq> \<infinity>"
  1211   and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
  1212   shows "measure M (A - B) = measure M A - measure M B"
  1213 proof -
  1214   have "emeasure M (A - B) \<le> emeasure M A" "emeasure M B \<le> emeasure M A"
  1215     using measurable by (auto intro!: emeasure_mono)
  1216   hence "measure M ((A - B) \<union> B) = measure M (A - B) + measure M B"
  1217     using measurable finite by (rule_tac measure_Union) auto
  1218   thus ?thesis using `B \<subseteq> A` by (auto simp: Un_absorb2)
  1219 qed
  1220 
  1221 lemma measure_UNION:
  1222   assumes measurable: "range A \<subseteq> sets M" "disjoint_family A"
  1223   assumes finite: "emeasure M (\<Union>i. A i) \<noteq> \<infinity>"
  1224   shows "(\<lambda>i. measure M (A i)) sums (measure M (\<Union>i. A i))"
  1225 proof -
  1226   from summable_sums[OF summable_ereal_pos, of "\<lambda>i. emeasure M (A i)"]
  1227        suminf_emeasure[OF measurable] emeasure_nonneg[of M]
  1228   have "(\<lambda>i. emeasure M (A i)) sums (emeasure M (\<Union>i. A i))" by simp
  1229   moreover
  1230   { fix i
  1231     have "emeasure M (A i) \<le> emeasure M (\<Union>i. A i)"
  1232       using measurable by (auto intro!: emeasure_mono)
  1233     then have "emeasure M (A i) = ereal ((measure M (A i)))"
  1234       using finite by (intro emeasure_eq_ereal_measure) auto }
  1235   ultimately show ?thesis using finite
  1236     unfolding sums_ereal[symmetric] by (simp add: emeasure_eq_ereal_measure)
  1237 qed
  1238 
  1239 lemma measure_subadditive:
  1240   assumes measurable: "A \<in> sets M" "B \<in> sets M"
  1241   and fin: "emeasure M A \<noteq> \<infinity>" "emeasure M B \<noteq> \<infinity>"
  1242   shows "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)"
  1243 proof -
  1244   have "emeasure M (A \<union> B) \<noteq> \<infinity>"
  1245     using emeasure_subadditive[OF measurable] fin by auto
  1246   then show "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)"
  1247     using emeasure_subadditive[OF measurable] fin
  1248     by (auto simp: emeasure_eq_ereal_measure)
  1249 qed
  1250 
  1251 lemma measure_subadditive_finite:
  1252   assumes A: "finite I" "A`I \<subseteq> sets M" and fin: "\<And>i. i \<in> I \<Longrightarrow> emeasure M (A i) \<noteq> \<infinity>"
  1253   shows "measure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. measure M (A i))"
  1254 proof -
  1255   { have "emeasure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. emeasure M (A i))"
  1256       using emeasure_subadditive_finite[OF A] .
  1257     also have "\<dots> < \<infinity>"
  1258       using fin by (simp add: setsum_Pinfty)
  1259     finally have "emeasure M (\<Union>i\<in>I. A i) \<noteq> \<infinity>" by simp }
  1260   then show ?thesis
  1261     using emeasure_subadditive_finite[OF A] fin
  1262     unfolding measure_def by (simp add: emeasure_eq_ereal_measure suminf_ereal measure_nonneg)
  1263 qed
  1264 
  1265 lemma measure_subadditive_countably:
  1266   assumes A: "range A \<subseteq> sets M" and fin: "(\<Sum>i. emeasure M (A i)) \<noteq> \<infinity>"
  1267   shows "measure M (\<Union>i. A i) \<le> (\<Sum>i. measure M (A i))"
  1268 proof -
  1269   from emeasure_nonneg fin have "\<And>i. emeasure M (A i) \<noteq> \<infinity>" by (rule suminf_PInfty)
  1270   moreover
  1271   { have "emeasure M (\<Union>i. A i) \<le> (\<Sum>i. emeasure M (A i))"
  1272       using emeasure_subadditive_countably[OF A] .
  1273     also have "\<dots> < \<infinity>"
  1274       using fin by simp
  1275     finally have "emeasure M (\<Union>i. A i) \<noteq> \<infinity>" by simp }
  1276   ultimately  show ?thesis
  1277     using emeasure_subadditive_countably[OF A] fin
  1278     unfolding measure_def by (simp add: emeasure_eq_ereal_measure suminf_ereal measure_nonneg)
  1279 qed
  1280 
  1281 lemma measure_eq_setsum_singleton:
  1282   assumes S: "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  1283   and fin: "\<And>x. x \<in> S \<Longrightarrow> emeasure M {x} \<noteq> \<infinity>"
  1284   shows "(measure M S) = (\<Sum>x\<in>S. (measure M {x}))"
  1285   unfolding measure_def
  1286   using emeasure_eq_setsum_singleton[OF S] fin
  1287   by simp (simp add: emeasure_eq_ereal_measure)
  1288 
  1289 lemma Lim_measure_incseq:
  1290   assumes A: "range A \<subseteq> sets M" "incseq A" and fin: "emeasure M (\<Union>i. A i) \<noteq> \<infinity>"
  1291   shows "(\<lambda>i. (measure M (A i))) ----> (measure M (\<Union>i. A i))"
  1292 proof -
  1293   have "ereal ((measure M (\<Union>i. A i))) = emeasure M (\<Union>i. A i)"
  1294     using fin by (auto simp: emeasure_eq_ereal_measure)
  1295   then show ?thesis
  1296     using Lim_emeasure_incseq[OF A]
  1297     unfolding measure_def
  1298     by (intro lim_real_of_ereal) simp
  1299 qed
  1300 
  1301 lemma Lim_measure_decseq:
  1302   assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
  1303   shows "(\<lambda>n. measure M (A n)) ----> measure M (\<Inter>i. A i)"
  1304 proof -
  1305   have "emeasure M (\<Inter>i. A i) \<le> emeasure M (A 0)"
  1306     using A by (auto intro!: emeasure_mono)
  1307   also have "\<dots> < \<infinity>"
  1308     using fin[of 0] by auto
  1309   finally have "ereal ((measure M (\<Inter>i. A i))) = emeasure M (\<Inter>i. A i)"
  1310     by (auto simp: emeasure_eq_ereal_measure)
  1311   then show ?thesis
  1312     unfolding measure_def
  1313     using Lim_emeasure_decseq[OF A fin]
  1314     by (intro lim_real_of_ereal) simp
  1315 qed
  1316 
  1317 section {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *}
  1318 
  1319 locale finite_measure = sigma_finite_measure M for M +
  1320   assumes finite_emeasure_space: "emeasure M (space M) \<noteq> \<infinity>"
  1321 
  1322 lemma finite_measureI[Pure.intro!]:
  1323   assumes *: "emeasure M (space M) \<noteq> \<infinity>"
  1324   shows "finite_measure M"
  1325 proof
  1326   show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. emeasure M (A i) \<noteq> \<infinity>)"
  1327     using * by (auto intro!: exI[of _ "\<lambda>_. space M"])
  1328 qed fact
  1329 
  1330 lemma (in finite_measure) emeasure_finite[simp, intro]: "emeasure M A \<noteq> \<infinity>"
  1331   using finite_emeasure_space emeasure_space[of M A] by auto
  1332 
  1333 lemma (in finite_measure) emeasure_eq_measure: "emeasure M A = ereal (measure M A)"
  1334   unfolding measure_def by (simp add: emeasure_eq_ereal_measure)
  1335 
  1336 lemma (in finite_measure) emeasure_real: "\<exists>r. 0 \<le> r \<and> emeasure M A = ereal r"
  1337   using emeasure_finite[of A] emeasure_nonneg[of M A] by (cases "emeasure M A") auto
  1338 
  1339 lemma (in finite_measure) bounded_measure: "measure M A \<le> measure M (space M)"
  1340   using emeasure_space[of M A] emeasure_real[of A] emeasure_real[of "space M"] by (auto simp: measure_def)
  1341 
  1342 lemma (in finite_measure) finite_measure_Diff:
  1343   assumes sets: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
  1344   shows "measure M (A - B) = measure M A - measure M B"
  1345   using measure_Diff[OF _ assms] by simp
  1346 
  1347 lemma (in finite_measure) finite_measure_Union:
  1348   assumes sets: "A \<in> sets M" "B \<in> sets M" and "A \<inter> B = {}"
  1349   shows "measure M (A \<union> B) = measure M A + measure M B"
  1350   using measure_Union[OF _ _ assms] by simp
  1351 
  1352 lemma (in finite_measure) finite_measure_finite_Union:
  1353   assumes measurable: "A`S \<subseteq> sets M" "disjoint_family_on A S" "finite S"
  1354   shows "measure M (\<Union>i\<in>S. A i) = (\<Sum>i\<in>S. measure M (A i))"
  1355   using measure_finite_Union[OF assms] by simp
  1356 
  1357 lemma (in finite_measure) finite_measure_UNION:
  1358   assumes A: "range A \<subseteq> sets M" "disjoint_family A"
  1359   shows "(\<lambda>i. measure M (A i)) sums (measure M (\<Union>i. A i))"
  1360   using measure_UNION[OF A] by simp
  1361 
  1362 lemma (in finite_measure) finite_measure_mono:
  1363   assumes "A \<subseteq> B" "B \<in> sets M" shows "measure M A \<le> measure M B"
  1364   using emeasure_mono[OF assms] emeasure_real[of A] emeasure_real[of B] by (auto simp: measure_def)
  1365 
  1366 lemma (in finite_measure) finite_measure_subadditive:
  1367   assumes m: "A \<in> sets M" "B \<in> sets M"
  1368   shows "measure M (A \<union> B) \<le> measure M A + measure M B"
  1369   using measure_subadditive[OF m] by simp
  1370 
  1371 lemma (in finite_measure) finite_measure_subadditive_finite:
  1372   assumes "finite I" "A`I \<subseteq> sets M" shows "measure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. measure M (A i))"
  1373   using measure_subadditive_finite[OF assms] by simp
  1374 
  1375 lemma (in finite_measure) finite_measure_subadditive_countably:
  1376   assumes A: "range A \<subseteq> sets M" and sum: "summable (\<lambda>i. measure M (A i))"
  1377   shows "measure M (\<Union>i. A i) \<le> (\<Sum>i. measure M (A i))"
  1378 proof -
  1379   from `summable (\<lambda>i. measure M (A i))`
  1380   have "(\<lambda>i. ereal (measure M (A i))) sums ereal (\<Sum>i. measure M (A i))"
  1381     by (simp add: sums_ereal) (rule summable_sums)
  1382   from sums_unique[OF this, symmetric]
  1383        measure_subadditive_countably[OF A]
  1384   show ?thesis by (simp add: emeasure_eq_measure)
  1385 qed
  1386 
  1387 lemma (in finite_measure) finite_measure_eq_setsum_singleton:
  1388   assumes "finite S" and *: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  1389   shows "measure M S = (\<Sum>x\<in>S. measure M {x})"
  1390   using measure_eq_setsum_singleton[OF assms] by simp
  1391 
  1392 lemma (in finite_measure) finite_Lim_measure_incseq:
  1393   assumes A: "range A \<subseteq> sets M" "incseq A"
  1394   shows "(\<lambda>i. measure M (A i)) ----> measure M (\<Union>i. A i)"
  1395   using Lim_measure_incseq[OF A] by simp
  1396 
  1397 lemma (in finite_measure) finite_Lim_measure_decseq:
  1398   assumes A: "range A \<subseteq> sets M" "decseq A"
  1399   shows "(\<lambda>n. measure M (A n)) ----> measure M (\<Inter>i. A i)"
  1400   using Lim_measure_decseq[OF A] by simp
  1401 
  1402 lemma (in finite_measure) finite_measure_compl:
  1403   assumes S: "S \<in> sets M"
  1404   shows "measure M (space M - S) = measure M (space M) - measure M S"
  1405   using measure_Diff[OF _ sets.top S sets.sets_into_space] S by simp
  1406 
  1407 lemma (in finite_measure) finite_measure_mono_AE:
  1408   assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" and B: "B \<in> sets M"
  1409   shows "measure M A \<le> measure M B"
  1410   using assms emeasure_mono_AE[OF imp B]
  1411   by (simp add: emeasure_eq_measure)
  1412 
  1413 lemma (in finite_measure) finite_measure_eq_AE:
  1414   assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
  1415   assumes A: "A \<in> sets M" and B: "B \<in> sets M"
  1416   shows "measure M A = measure M B"
  1417   using assms emeasure_eq_AE[OF assms] by (simp add: emeasure_eq_measure)
  1418 
  1419 lemma (in finite_measure) measure_increasing: "increasing M (measure M)"
  1420   by (auto intro!: finite_measure_mono simp: increasing_def)
  1421 
  1422 lemma (in finite_measure) measure_zero_union:
  1423   assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
  1424   shows "measure M (s \<union> t) = measure M s"
  1425 using assms
  1426 proof -
  1427   have "measure M (s \<union> t) \<le> measure M s"
  1428     using finite_measure_subadditive[of s t] assms by auto
  1429   moreover have "measure M (s \<union> t) \<ge> measure M s"
  1430     using assms by (blast intro: finite_measure_mono)
  1431   ultimately show ?thesis by simp
  1432 qed
  1433 
  1434 lemma (in finite_measure) measure_eq_compl:
  1435   assumes "s \<in> sets M" "t \<in> sets M"
  1436   assumes "measure M (space M - s) = measure M (space M - t)"
  1437   shows "measure M s = measure M t"
  1438   using assms finite_measure_compl by auto
  1439 
  1440 lemma (in finite_measure) measure_eq_bigunion_image:
  1441   assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
  1442   assumes "disjoint_family f" "disjoint_family g"
  1443   assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
  1444   shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
  1445 using assms
  1446 proof -
  1447   have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
  1448     by (rule finite_measure_UNION[OF assms(1,3)])
  1449   have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
  1450     by (rule finite_measure_UNION[OF assms(2,4)])
  1451   show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
  1452 qed
  1453 
  1454 lemma (in finite_measure) measure_countably_zero:
  1455   assumes "range c \<subseteq> sets M"
  1456   assumes "\<And> i. measure M (c i) = 0"
  1457   shows "measure M (\<Union> i :: nat. c i) = 0"
  1458 proof (rule antisym)
  1459   show "measure M (\<Union> i :: nat. c i) \<le> 0"
  1460     using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
  1461 qed (simp add: measure_nonneg)
  1462 
  1463 lemma (in finite_measure) measure_space_inter:
  1464   assumes events:"s \<in> sets M" "t \<in> sets M"
  1465   assumes "measure M t = measure M (space M)"
  1466   shows "measure M (s \<inter> t) = measure M s"
  1467 proof -
  1468   have "measure M ((space M - s) \<union> (space M - t)) = measure M (space M - s)"
  1469     using events assms finite_measure_compl[of "t"] by (auto intro!: measure_zero_union)
  1470   also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
  1471     by blast
  1472   finally show "measure M (s \<inter> t) = measure M s"
  1473     using events by (auto intro!: measure_eq_compl[of "s \<inter> t" s])
  1474 qed
  1475 
  1476 lemma (in finite_measure) measure_equiprobable_finite_unions:
  1477   assumes s: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> sets M"
  1478   assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> measure M {x} = measure M {y}"
  1479   shows "measure M s = real (card s) * measure M {SOME x. x \<in> s}"
  1480 proof cases
  1481   assume "s \<noteq> {}"
  1482   then have "\<exists> x. x \<in> s" by blast
  1483   from someI_ex[OF this] assms
  1484   have prob_some: "\<And> x. x \<in> s \<Longrightarrow> measure M {x} = measure M {SOME y. y \<in> s}" by blast
  1485   have "measure M s = (\<Sum> x \<in> s. measure M {x})"
  1486     using finite_measure_eq_setsum_singleton[OF s] by simp
  1487   also have "\<dots> = (\<Sum> x \<in> s. measure M {SOME y. y \<in> s})" using prob_some by auto
  1488   also have "\<dots> = real (card s) * measure M {(SOME x. x \<in> s)}"
  1489     using setsum_constant assms by (simp add: real_eq_of_nat)
  1490   finally show ?thesis by simp
  1491 qed simp
  1492 
  1493 lemma (in finite_measure) measure_real_sum_image_fn:
  1494   assumes "e \<in> sets M"
  1495   assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
  1496   assumes "finite s"
  1497   assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
  1498   assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
  1499   shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  1500 proof -
  1501   have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
  1502     using `e \<in> sets M` sets.sets_into_space upper by blast
  1503   hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
  1504   also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  1505   proof (rule finite_measure_finite_Union)
  1506     show "finite s" by fact
  1507     show "(\<lambda>i. e \<inter> f i)`s \<subseteq> sets M" using assms(2) by auto
  1508     show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
  1509       using disjoint by (auto simp: disjoint_family_on_def)
  1510   qed
  1511   finally show ?thesis .
  1512 qed
  1513 
  1514 lemma (in finite_measure) measure_exclude:
  1515   assumes "A \<in> sets M" "B \<in> sets M"
  1516   assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
  1517   shows "measure M B = 0"
  1518   using measure_space_inter[of B A] assms by (auto simp: ac_simps)
  1519 
  1520 section {* Counting space *}
  1521 
  1522 lemma strict_monoI_Suc:
  1523   assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
  1524   unfolding strict_mono_def
  1525 proof safe
  1526   fix n m :: nat assume "n < m" then show "f n < f m"
  1527     by (induct m) (auto simp: less_Suc_eq intro: less_trans ord)
  1528 qed
  1529 
  1530 lemma emeasure_count_space:
  1531   assumes "X \<subseteq> A" shows "emeasure (count_space A) X = (if finite X then ereal (card X) else \<infinity>)"
  1532     (is "_ = ?M X")
  1533   unfolding count_space_def
  1534 proof (rule emeasure_measure_of_sigma)
  1535   show "X \<in> Pow A" using `X \<subseteq> A` by auto
  1536   show "sigma_algebra A (Pow A)" by (rule sigma_algebra_Pow)
  1537   show positive: "positive (Pow A) ?M"
  1538     by (auto simp: positive_def)
  1539   have additive: "additive (Pow A) ?M"
  1540     by (auto simp: card_Un_disjoint additive_def)
  1541 
  1542   interpret ring_of_sets A "Pow A"
  1543     by (rule ring_of_setsI) auto
  1544   show "countably_additive (Pow A) ?M" 
  1545     unfolding countably_additive_iff_continuous_from_below[OF positive additive]
  1546   proof safe
  1547     fix F :: "nat \<Rightarrow> 'a set" assume "incseq F"
  1548     show "(\<lambda>i. ?M (F i)) ----> ?M (\<Union>i. F i)"
  1549     proof cases
  1550       assume "\<exists>i. \<forall>j\<ge>i. F i = F j"
  1551       then guess i .. note i = this
  1552       { fix j from i `incseq F` have "F j \<subseteq> F i"
  1553           by (cases "i \<le> j") (auto simp: incseq_def) }
  1554       then have eq: "(\<Union>i. F i) = F i"
  1555         by auto
  1556       with i show ?thesis
  1557         by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
  1558     next
  1559       assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
  1560       then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
  1561       moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
  1562       ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
  1563 
  1564       have "incseq (\<lambda>i. ?M (F i))"
  1565         using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
  1566       then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
  1567         by (rule LIMSEQ_ereal_SUPR)
  1568 
  1569       moreover have "(SUP n. ?M (F n)) = \<infinity>"
  1570       proof (rule SUP_PInfty)
  1571         fix n :: nat show "\<exists>k::nat\<in>UNIV. ereal n \<le> ?M (F k)"
  1572         proof (induct n)
  1573           case (Suc n)
  1574           then guess k .. note k = this
  1575           moreover have "finite (F k) \<Longrightarrow> finite (F (f k)) \<Longrightarrow> card (F k) < card (F (f k))"
  1576             using `F k \<subset> F (f k)` by (simp add: psubset_card_mono)
  1577           moreover have "finite (F (f k)) \<Longrightarrow> finite (F k)"
  1578             using `k \<le> f k` `incseq F` by (auto simp: incseq_def dest: finite_subset)
  1579           ultimately show ?case
  1580             by (auto intro!: exI[of _ "f k"])
  1581         qed auto
  1582       qed
  1583 
  1584       moreover
  1585       have "inj (\<lambda>n. F ((f ^^ n) 0))"
  1586         by (intro strict_mono_imp_inj_on strict_monoI_Suc) (simp add: *)
  1587       then have 1: "infinite (range (\<lambda>i. F ((f ^^ i) 0)))"
  1588         by (rule range_inj_infinite)
  1589       have "infinite (Pow (\<Union>i. F i))"
  1590         by (rule infinite_super[OF _ 1]) auto
  1591       then have "infinite (\<Union>i. F i)"
  1592         by auto
  1593       
  1594       ultimately show ?thesis by auto
  1595     qed
  1596   qed
  1597 qed
  1598 
  1599 lemma emeasure_count_space_finite[simp]:
  1600   "X \<subseteq> A \<Longrightarrow> finite X \<Longrightarrow> emeasure (count_space A) X = ereal (card X)"
  1601   using emeasure_count_space[of X A] by simp
  1602 
  1603 lemma emeasure_count_space_infinite[simp]:
  1604   "X \<subseteq> A \<Longrightarrow> infinite X \<Longrightarrow> emeasure (count_space A) X = \<infinity>"
  1605   using emeasure_count_space[of X A] by simp
  1606 
  1607 lemma emeasure_count_space_eq_0:
  1608   "emeasure (count_space A) X = 0 \<longleftrightarrow> (X \<subseteq> A \<longrightarrow> X = {})"
  1609 proof cases
  1610   assume X: "X \<subseteq> A"
  1611   then show ?thesis
  1612   proof (intro iffI impI)
  1613     assume "emeasure (count_space A) X = 0"
  1614     with X show "X = {}"
  1615       by (subst (asm) emeasure_count_space) (auto split: split_if_asm)
  1616   qed simp
  1617 qed (simp add: emeasure_notin_sets)
  1618 
  1619 lemma null_sets_count_space: "null_sets (count_space A) = { {} }"
  1620   unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0)
  1621 
  1622 lemma AE_count_space: "(AE x in count_space A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
  1623   unfolding eventually_ae_filter by (auto simp add: null_sets_count_space)
  1624 
  1625 lemma sigma_finite_measure_count_space:
  1626   fixes A :: "'a::countable set"
  1627   shows "sigma_finite_measure (count_space A)"
  1628 proof
  1629   show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (count_space A) \<and> (\<Union>i. F i) = space (count_space A) \<and>
  1630      (\<forall>i. emeasure (count_space A) (F i) \<noteq> \<infinity>)"
  1631      using surj_from_nat by (intro exI[of _ "\<lambda>i. {from_nat i} \<inter> A"]) (auto simp del: surj_from_nat)
  1632 qed
  1633 
  1634 lemma finite_measure_count_space:
  1635   assumes [simp]: "finite A"
  1636   shows "finite_measure (count_space A)"
  1637   by rule simp
  1638 
  1639 lemma sigma_finite_measure_count_space_finite:
  1640   assumes A: "finite A" shows "sigma_finite_measure (count_space A)"
  1641 proof -
  1642   interpret finite_measure "count_space A" using A by (rule finite_measure_count_space)
  1643   show "sigma_finite_measure (count_space A)" ..
  1644 qed
  1645 
  1646 end
  1647