src/HOL/Probability/Measure.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 33657 a4179bf442d1 child 35582 b16d99a72dc9 permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
```     1 header {*Measures*}
```
```     2
```
```     3 theory Measure
```
```     4   imports Caratheodory FuncSet
```
```     5 begin
```
```     6
```
```     7 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
```
```     8
```
```     9 definition prod_sets where
```
```    10   "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
```
```    11
```
```    12 lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
```
```    13   by (auto simp add: prod_sets_def)
```
```    14
```
```    15 definition
```
```    16   closed_cdi  where
```
```    17   "closed_cdi M \<longleftrightarrow>
```
```    18    sets M \<subseteq> Pow (space M) &
```
```    19    (\<forall>s \<in> sets M. space M - s \<in> sets M) &
```
```    20    (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
```
```    21         (\<Union>i. A i) \<in> sets M) &
```
```    22    (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
```
```    23
```
```    24
```
```    25 inductive_set
```
```    26   smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
```
```    27   for M
```
```    28   where
```
```    29     Basic [intro]:
```
```    30       "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
```
```    31   | Compl [intro]:
```
```    32       "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
```
```    33   | Inc:
```
```    34       "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
```
```    35        \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
```
```    36   | Disj:
```
```    37       "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
```
```    38        \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
```
```    39   monos Pow_mono
```
```    40
```
```    41
```
```    42 definition
```
```    43   smallest_closed_cdi  where
```
```    44   "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
```
```    45
```
```    46 definition
```
```    47   measurable  where
```
```    48   "measurable a b = {f . sigma_algebra a & sigma_algebra b &
```
```    49                          f \<in> (space a -> space b) &
```
```    50                          (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
```
```    51
```
```    52 definition
```
```    53   measure_preserving  where
```
```    54   "measure_preserving m1 m2 =
```
```    55      measurable m1 m2 \<inter>
```
```    56      {f . measure_space m1 & measure_space m2 &
```
```    57           (\<forall>y \<in> sets m2. measure m1 ((f -` y) \<inter> (space m1)) = measure m2 y)}"
```
```    58
```
```    59 lemma space_smallest_closed_cdi [simp]:
```
```    60      "space (smallest_closed_cdi M) = space M"
```
```    61   by (simp add: smallest_closed_cdi_def)
```
```    62
```
```    63
```
```    64 lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
```
```    65   by (auto simp add: smallest_closed_cdi_def)
```
```    66
```
```    67 lemma (in algebra) smallest_ccdi_sets:
```
```    68      "smallest_ccdi_sets M \<subseteq> Pow (space M)"
```
```    69   apply (rule subsetI)
```
```    70   apply (erule smallest_ccdi_sets.induct)
```
```    71   apply (auto intro: range_subsetD dest: sets_into_space)
```
```    72   done
```
```    73
```
```    74 lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
```
```    75   apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
```
```    76   apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
```
```    77   done
```
```    78
```
```    79 lemma (in algebra) smallest_closed_cdi3:
```
```    80      "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
```
```    81   by (simp add: smallest_closed_cdi_def smallest_ccdi_sets)
```
```    82
```
```    83 lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
```
```    84   by (simp add: closed_cdi_def)
```
```    85
```
```    86 lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
```
```    87   by (simp add: closed_cdi_def)
```
```    88
```
```    89 lemma closed_cdi_Inc:
```
```    90      "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
```
```    91         (\<Union>i. A i) \<in> sets M"
```
```    92   by (simp add: closed_cdi_def)
```
```    93
```
```    94 lemma closed_cdi_Disj:
```
```    95      "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
```
```    96   by (simp add: closed_cdi_def)
```
```    97
```
```    98 lemma closed_cdi_Un:
```
```    99   assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
```
```   100       and A: "A \<in> sets M" and B: "B \<in> sets M"
```
```   101       and disj: "A \<inter> B = {}"
```
```   102     shows "A \<union> B \<in> sets M"
```
```   103 proof -
```
```   104   have ra: "range (binaryset A B) \<subseteq> sets M"
```
```   105    by (simp add: range_binaryset_eq empty A B)
```
```   106  have di:  "disjoint_family (binaryset A B)" using disj
```
```   107    by (simp add: disjoint_family_def binaryset_def Int_commute)
```
```   108  from closed_cdi_Disj [OF cdi ra di]
```
```   109  show ?thesis
```
```   110    by (simp add: UN_binaryset_eq)
```
```   111 qed
```
```   112
```
```   113 lemma (in algebra) smallest_ccdi_sets_Un:
```
```   114   assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
```
```   115       and disj: "A \<inter> B = {}"
```
```   116     shows "A \<union> B \<in> smallest_ccdi_sets M"
```
```   117 proof -
```
```   118   have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
```
```   119     by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
```
```   120   have di:  "disjoint_family (binaryset A B)" using disj
```
```   121     by (simp add: disjoint_family_def binaryset_def Int_commute)
```
```   122   from Disj [OF ra di]
```
```   123   show ?thesis
```
```   124     by (simp add: UN_binaryset_eq)
```
```   125 qed
```
```   126
```
```   127
```
```   128
```
```   129 lemma (in algebra) smallest_ccdi_sets_Int1:
```
```   130   assumes a: "a \<in> sets M"
```
```   131   shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
```
```   132 proof (induct rule: smallest_ccdi_sets.induct)
```
```   133   case (Basic x)
```
```   134   thus ?case
```
```   135     by (metis a Int smallest_ccdi_sets.Basic)
```
```   136 next
```
```   137   case (Compl x)
```
```   138   have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
```
```   139     by blast
```
```   140   also have "... \<in> smallest_ccdi_sets M"
```
```   141     by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
```
```   142            Diff_disjoint Int_Diff Int_empty_right Un_commute
```
```   143            smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
```
```   144            smallest_ccdi_sets_Un)
```
```   145   finally show ?case .
```
```   146 next
```
```   147   case (Inc A)
```
```   148   have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
```
```   149     by blast
```
```   150   have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
```
```   151     by blast
```
```   152   moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
```
```   153     by (simp add: Inc)
```
```   154   moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
```
```   155     by blast
```
```   156   ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
```
```   157     by (rule smallest_ccdi_sets.Inc)
```
```   158   show ?case
```
```   159     by (metis 1 2)
```
```   160 next
```
```   161   case (Disj A)
```
```   162   have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
```
```   163     by blast
```
```   164   have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
```
```   165     by blast
```
```   166   moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
```
```   167     by (auto simp add: disjoint_family_def)
```
```   168   ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
```
```   169     by (rule smallest_ccdi_sets.Disj)
```
```   170   show ?case
```
```   171     by (metis 1 2)
```
```   172 qed
```
```   173
```
```   174
```
```   175 lemma (in algebra) smallest_ccdi_sets_Int:
```
```   176   assumes b: "b \<in> smallest_ccdi_sets M"
```
```   177   shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
```
```   178 proof (induct rule: smallest_ccdi_sets.induct)
```
```   179   case (Basic x)
```
```   180   thus ?case
```
```   181     by (metis b smallest_ccdi_sets_Int1)
```
```   182 next
```
```   183   case (Compl x)
```
```   184   have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
```
```   185     by blast
```
```   186   also have "... \<in> smallest_ccdi_sets M"
```
```   187     by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b
```
```   188            smallest_ccdi_sets.Compl smallest_ccdi_sets_Un)
```
```   189   finally show ?case .
```
```   190 next
```
```   191   case (Inc A)
```
```   192   have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
```
```   193     by blast
```
```   194   have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
```
```   195     by blast
```
```   196   moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
```
```   197     by (simp add: Inc)
```
```   198   moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
```
```   199     by blast
```
```   200   ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
```
```   201     by (rule smallest_ccdi_sets.Inc)
```
```   202   show ?case
```
```   203     by (metis 1 2)
```
```   204 next
```
```   205   case (Disj A)
```
```   206   have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
```
```   207     by blast
```
```   208   have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
```
```   209     by blast
```
```   210   moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
```
```   211     by (auto simp add: disjoint_family_def)
```
```   212   ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
```
```   213     by (rule smallest_ccdi_sets.Disj)
```
```   214   show ?case
```
```   215     by (metis 1 2)
```
```   216 qed
```
```   217
```
```   218 lemma (in algebra) sets_smallest_closed_cdi_Int:
```
```   219    "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
```
```   220     \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
```
```   221   by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def)
```
```   222
```
```   223 lemma algebra_iff_Int:
```
```   224      "algebra M \<longleftrightarrow>
```
```   225        sets M \<subseteq> Pow (space M) & {} \<in> sets M &
```
```   226        (\<forall>a \<in> sets M. space M - a \<in> sets M) &
```
```   227        (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
```
```   228 proof (auto simp add: algebra.Int, auto simp add: algebra_def)
```
```   229   fix a b
```
```   230   assume ab: "sets M \<subseteq> Pow (space M)"
```
```   231              "\<forall>a\<in>sets M. space M - a \<in> sets M"
```
```   232              "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
```
```   233              "a \<in> sets M" "b \<in> sets M"
```
```   234   hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
```
```   235     by blast
```
```   236   also have "... \<in> sets M"
```
```   237     by (metis ab)
```
```   238   finally show "a \<union> b \<in> sets M" .
```
```   239 qed
```
```   240
```
```   241 lemma (in algebra) sigma_property_disjoint_lemma:
```
```   242   assumes sbC: "sets M \<subseteq> C"
```
```   243       and ccdi: "closed_cdi (|space = space M, sets = C|)"
```
```   244   shows "sigma_sets (space M) (sets M) \<subseteq> C"
```
```   245 proof -
```
```   246   have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
```
```   247     apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int
```
```   248             smallest_ccdi_sets_Int)
```
```   249     apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets)
```
```   250     apply (blast intro: smallest_ccdi_sets.Disj)
```
```   251     done
```
```   252   hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
```
```   253     by auto
```
```   254        (metis sigma_algebra.sigma_sets_subset algebra.simps(1)
```
```   255           algebra.simps(2) subsetD)
```
```   256   also have "...  \<subseteq> C"
```
```   257     proof
```
```   258       fix x
```
```   259       assume x: "x \<in> smallest_ccdi_sets M"
```
```   260       thus "x \<in> C"
```
```   261         proof (induct rule: smallest_ccdi_sets.induct)
```
```   262           case (Basic x)
```
```   263           thus ?case
```
```   264             by (metis Basic subsetD sbC)
```
```   265         next
```
```   266           case (Compl x)
```
```   267           thus ?case
```
```   268             by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
```
```   269         next
```
```   270           case (Inc A)
```
```   271           thus ?case
```
```   272                by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
```
```   273         next
```
```   274           case (Disj A)
```
```   275           thus ?case
```
```   276                by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
```
```   277         qed
```
```   278     qed
```
```   279   finally show ?thesis .
```
```   280 qed
```
```   281
```
```   282 lemma (in algebra) sigma_property_disjoint:
```
```   283   assumes sbC: "sets M \<subseteq> C"
```
```   284       and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
```
```   285       and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
```
```   286                      \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n))
```
```   287                      \<Longrightarrow> (\<Union>i. A i) \<in> C"
```
```   288       and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M)
```
```   289                       \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
```
```   290   shows "sigma_sets (space M) (sets M) \<subseteq> C"
```
```   291 proof -
```
```   292   have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
```
```   293     proof (rule sigma_property_disjoint_lemma)
```
```   294       show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
```
```   295         by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
```
```   296     next
```
```   297       show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
```
```   298         by (simp add: closed_cdi_def compl inc disj)
```
```   299            (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
```
```   300              IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
```
```   301     qed
```
```   302   thus ?thesis
```
```   303     by blast
```
```   304 qed
```
```   305
```
```   306
```
```   307 (* or just countably_additiveD [OF measure_space.ca] *)
```
```   308 lemma (in measure_space) measure_countably_additive:
```
```   309     "range A \<subseteq> sets M
```
```   310      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M
```
```   311      \<Longrightarrow> (measure M o A)  sums  measure M (\<Union>i. A i)"
```
```   312   by (insert ca) (simp add: countably_additive_def o_def)
```
```   313
```
```   314 lemma (in measure_space) additive:
```
```   315      "additive M (measure M)"
```
```   316 proof (rule algebra.countably_additive_additive [OF _ _ ca])
```
```   317   show "algebra M"
```
```   318     by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms)
```
```   319   show "positive M (measure M)"
```
```   320     by (simp add: positive_def empty_measure positive)
```
```   321 qed
```
```   322
```
```   323 lemma (in measure_space) measure_additive:
```
```   324      "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}
```
```   325       \<Longrightarrow> measure M a + measure M b = measure M (a \<union> b)"
```
```   326   by (metis additiveD additive)
```
```   327
```
```   328 lemma (in measure_space) measure_compl:
```
```   329   assumes s: "s \<in> sets M"
```
```   330   shows "measure M (space M - s) = measure M (space M) - measure M s"
```
```   331 proof -
```
```   332   have "measure M (space M) = measure M (s \<union> (space M - s))" using s
```
```   333     by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
```
```   334   also have "... = measure M s + measure M (space M - s)"
```
```   335     by (rule additiveD [OF additive]) (auto simp add: s)
```
```   336   finally have "measure M (space M) = measure M s + measure M (space M - s)" .
```
```   337   thus ?thesis
```
```   338     by arith
```
```   339 qed
```
```   340
```
```   341 lemma disjoint_family_Suc:
```
```   342   assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
```
```   343   shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
```
```   344 proof -
```
```   345   {
```
```   346     fix m
```
```   347     have "!!n. A n \<subseteq> A (m+n)"
```
```   348     proof (induct m)
```
```   349       case 0 show ?case by simp
```
```   350     next
```
```   351       case (Suc m) thus ?case
```
```   352         by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
```
```   353     qed
```
```   354   }
```
```   355   hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
```
```   356     by (metis add_commute le_add_diff_inverse nat_less_le)
```
```   357   thus ?thesis
```
```   358     by (auto simp add: disjoint_family_def)
```
```   359       (metis insert_absorb insert_subset le_SucE le_antisym not_leE)
```
```   360 qed
```
```   361
```
```   362
```
```   363 lemma (in measure_space) measure_countable_increasing:
```
```   364   assumes A: "range A \<subseteq> sets M"
```
```   365       and A0: "A 0 = {}"
```
```   366       and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
```
```   367   shows "(measure M o A) ----> measure M (\<Union>i. A i)"
```
```   368 proof -
```
```   369   {
```
```   370     fix n
```
```   371     have "(measure M \<circ> A) n =
```
```   372           setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
```
```   373       proof (induct n)
```
```   374         case 0 thus ?case by (auto simp add: A0 empty_measure)
```
```   375       next
```
```   376         case (Suc m)
```
```   377         have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
```
```   378           by (metis ASuc Un_Diff_cancel Un_absorb1)
```
```   379         hence "measure M (A (Suc m)) =
```
```   380                measure M (A m) + measure M (A (Suc m) - A m)"
```
```   381           by (subst measure_additive)
```
```   382              (auto simp add: measure_additive range_subsetD [OF A])
```
```   383         with Suc show ?case
```
```   384           by simp
```
```   385       qed
```
```   386   }
```
```   387   hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
```
```   388     by (blast intro: ext)
```
```   389   have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
```
```   390     proof (rule UN_finite2_eq [where k=1], simp)
```
```   391       fix i
```
```   392       show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
```
```   393         proof (induct i)
```
```   394           case 0 thus ?case by (simp add: A0)
```
```   395         next
```
```   396           case (Suc i)
```
```   397           thus ?case
```
```   398             by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
```
```   399         qed
```
```   400     qed
```
```   401   have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
```
```   402     by (metis A Diff range_subsetD)
```
```   403   have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
```
```   404     by (blast intro: countable_UN range_subsetD [OF A])
```
```   405   have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
```
```   406     by (rule measure_countably_additive)
```
```   407        (auto simp add: disjoint_family_Suc ASuc A1 A2)
```
```   408   also have "... =  measure M (\<Union>i. A i)"
```
```   409     by (simp add: Aeq)
```
```   410   finally have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A i)" .
```
```   411   thus ?thesis
```
```   412     by (auto simp add: sums_iff Meq dest: summable_sumr_LIMSEQ_suminf)
```
```   413 qed
```
```   414
```
```   415 lemma (in measure_space) monotone_convergence:
```
```   416   assumes A: "range A \<subseteq> sets M"
```
```   417       and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
```
```   418   shows "(measure M \<circ> A) ----> measure M (\<Union>i. A i)"
```
```   419 proof -
```
```   420   have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
```
```   421     by (auto simp add: split: nat.splits)
```
```   422   have meq: "measure M \<circ> A = (\<lambda>n. (measure M \<circ> nat_case {} A) (Suc n))"
```
```   423     by (rule ext) simp
```
```   424   have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)"
```
```   425     by (rule measure_countable_increasing)
```
```   426        (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits)
```
```   427   also have "... = measure M (\<Union>i. A i)"
```
```   428     by (simp add: ueq)
```
```   429   finally have "(measure M \<circ> nat_case {} A) ---->  measure M (\<Union>i. A i)" .
```
```   430   thus ?thesis using meq
```
```   431     by (metis LIMSEQ_Suc)
```
```   432 qed
```
```   433
```
```   434 lemma measurable_sigma_preimages:
```
```   435   assumes a: "sigma_algebra a" and b: "sigma_algebra b"
```
```   436       and f: "f \<in> space a -> space b"
```
```   437       and ba: "!!y. y \<in> sets b ==> f -` y \<in> sets a"
```
```   438   shows "sigma_algebra (|space = space a, sets = (vimage f) ` (sets b) |)"
```
```   439 proof (simp add: sigma_algebra_iff2, intro conjI)
```
```   440   show "op -` f ` sets b \<subseteq> Pow (space a)"
```
```   441     by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI)
```
```   442 next
```
```   443   show "{} \<in> op -` f ` sets b"
```
```   444     by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty)
```
```   445 next
```
```   446   { fix y
```
```   447     assume y: "y \<in> sets b"
```
```   448     with a b f
```
```   449     have "space a - f -` y = f -` (space b - y)"
```
```   450       by (auto simp add: sigma_algebra_iff2) (blast intro: ba)
```
```   451     hence "space a - (f -` y) \<in> (vimage f) ` sets b"
```
```   452       by auto
```
```   453          (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
```
```   454                 sigma_sets.Compl)
```
```   455   }
```
```   456   thus "\<forall>s\<in>sets b. space a - f -` s \<in> (vimage f) ` sets b"
```
```   457     by blast
```
```   458 next
```
```   459   {
```
```   460     fix A:: "nat \<Rightarrow> 'a set"
```
```   461     assume A: "range A \<subseteq> (vimage f) ` (sets b)"
```
```   462     have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
```
```   463       proof -
```
```   464         def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
```
```   465         {
```
```   466           fix i
```
```   467           have "A i \<in> (vimage f) ` (sets b)" using A
```
```   468             by blast
```
```   469           hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
```
```   470             by blast
```
```   471           hence "B i \<in> sets b \<and> f -` B i = A i"
```
```   472             by (simp add: B_def) (erule someI_ex)
```
```   473         } note B = this
```
```   474         show ?thesis
```
```   475           proof
```
```   476             show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
```
```   477               by (simp add: vimage_UN B)
```
```   478            show "(\<Union>i. B i) \<in> sets b" using B
```
```   479              by (auto intro: sigma_algebra.countable_UN [OF b])
```
```   480           qed
```
```   481       qed
```
```   482   }
```
```   483   thus "\<forall>A::nat \<Rightarrow> 'a set.
```
```   484            range A \<subseteq> (vimage f) ` sets b \<longrightarrow> (\<Union>i. A i) \<in> (vimage f) ` sets b"
```
```   485     by blast
```
```   486 qed
```
```   487
```
```   488 lemma (in sigma_algebra) measurable_sigma:
```
```   489   assumes B: "B \<subseteq> Pow X"
```
```   490       and f: "f \<in> space M -> X"
```
```   491       and ba: "!!y. y \<in> B ==> (f -` y) \<inter> space M \<in> sets M"
```
```   492   shows "f \<in> measurable M (sigma X B)"
```
```   493 proof -
```
```   494   have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
```
```   495     proof clarify
```
```   496       fix x
```
```   497       assume "x \<in> sigma_sets X B"
```
```   498       thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
```
```   499         proof induct
```
```   500           case (Basic a)
```
```   501           thus ?case
```
```   502             by (auto simp add: ba) (metis B subsetD PowD)
```
```   503         next
```
```   504           case Empty
```
```   505           thus ?case
```
```   506             by auto
```
```   507         next
```
```   508           case (Compl a)
```
```   509           have [simp]: "f -` X \<inter> space M = space M"
```
```   510             by (auto simp add: funcset_mem [OF f])
```
```   511           thus ?case
```
```   512             by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
```
```   513         next
```
```   514           case (Union a)
```
```   515           thus ?case
```
```   516             by (simp add: vimage_UN, simp only: UN_extend_simps(4))
```
```   517                (blast intro: countable_UN)
```
```   518         qed
```
```   519     qed
```
```   520   thus ?thesis
```
```   521     by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
```
```   522        (auto simp add: sigma_def)
```
```   523 qed
```
```   524
```
```   525 lemma measurable_subset:
```
```   526      "measurable a b \<subseteq> measurable a (sigma (space b) (sets b))"
```
```   527   apply clarify
```
```   528   apply (rule sigma_algebra.measurable_sigma)
```
```   529   apply (auto simp add: measurable_def)
```
```   530   apply (metis algebra.sets_into_space subsetD sigma_algebra_iff)
```
```   531   done
```
```   532
```
```   533 lemma measurable_eqI:
```
```   534      "space m1 = space m1' \<Longrightarrow> space m2 = space m2'
```
```   535       \<Longrightarrow> sets m1 = sets m1' \<Longrightarrow> sets m2 = sets m2'
```
```   536       \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
```
```   537   by (simp add: measurable_def sigma_algebra_iff2)
```
```   538
```
```   539 lemma measure_preserving_lift:
```
```   540   fixes f :: "'a1 \<Rightarrow> 'a2"
```
```   541     and m1 :: "('a1, 'b1) measure_space_scheme"
```
```   542     and m2 :: "('a2, 'b2) measure_space_scheme"
```
```   543   assumes m1: "measure_space m1" and m2: "measure_space m2"
```
```   544   defines "m x \<equiv> (|space = space m2, sets = x, measure = measure m2, ... = more m2|)"
```
```   545   assumes setsm2: "sets m2 = sigma_sets (space m2) a"
```
```   546       and fmp: "f \<in> measure_preserving m1 (m a)"
```
```   547   shows "f \<in> measure_preserving m1 m2"
```
```   548 proof -
```
```   549   have [simp]: "!!x. space (m x) = space m2 & sets (m x) = x & measure (m x) = measure m2"
```
```   550     by (simp add: m_def)
```
```   551   have sa1: "sigma_algebra m1" using m1
```
```   552     by (simp add: measure_space_def)
```
```   553   show ?thesis using fmp
```
```   554     proof (clarsimp simp add: measure_preserving_def m1 m2)
```
```   555       assume fm: "f \<in> measurable m1 (m a)"
```
```   556          and mam: "measure_space (m a)"
```
```   557          and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
```
```   558       have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
```
```   559         by (rule subsetD [OF measurable_subset fm])
```
```   560       also have "... = measurable m1 m2"
```
```   561         by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def)
```
```   562       finally have f12: "f \<in> measurable m1 m2" .
```
```   563       hence ffn: "f \<in> space m1 \<rightarrow> space m2"
```
```   564         by (simp add: measurable_def)
```
```   565       have "space m1 \<subseteq> f -` (space m2)"
```
```   566         by auto (metis PiE ffn)
```
```   567       hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
```
```   568         by blast
```
```   569       {
```
```   570         fix y
```
```   571         assume y: "y \<in> sets m2"
```
```   572         have ama: "algebra (m a)"  using mam
```
```   573           by (simp add: measure_space_def sigma_algebra_iff)
```
```   574         have spa: "space m2 \<in> a" using algebra.top [OF ama]
```
```   575           by (simp add: m_def)
```
```   576         have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
```
```   577           by (simp add: m_def)
```
```   578         also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
```
```   579           proof (rule algebra.sigma_property_disjoint, auto simp add: ama)
```
```   580             fix x
```
```   581             assume x: "x \<in> a"
```
```   582             thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
```
```   583               by (simp add: meq)
```
```   584           next
```
```   585             fix s
```
```   586             assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
```
```   587                and s: "s \<in> sigma_sets (space m2) a"
```
```   588             hence s2: "s \<in> sets m2"
```
```   589               by (simp add: setsm2)
```
```   590             thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
```
```   591                   measure m2 (space m2 - s)" using f12
```
```   592               by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
```
```   593                     measure_space.measure_compl measurable_def)
```
```   594                  (metis fveq meq spa)
```
```   595           next
```
```   596             fix A
```
```   597               assume A0: "A 0 = {}"
```
```   598                  and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
```
```   599                  and rA1: "range A \<subseteq>
```
```   600                            {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
```
```   601                  and "range A \<subseteq> sigma_sets (space m2) a"
```
```   602               hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
```
```   603               have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
```
```   604                 using rA1 by blast
```
```   605               have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))"
```
```   606                 by (simp add: o_def eq1)
```
```   607               also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
```
```   608                 proof (rule measure_space.measure_countable_increasing [OF m1])
```
```   609                   show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
```
```   610                     using f12 rA2 by (auto simp add: measurable_def)
```
```   611                   show "f -` A 0 \<inter> space m1 = {}" using A0
```
```   612                     by blast
```
```   613                   show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
```
```   614                     using ASuc by auto
```
```   615                 qed
```
```   616               also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
```
```   617                 by (simp add: vimage_UN)
```
```   618               finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
```
```   619               moreover
```
```   620               have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
```
```   621                 by (rule measure_space.measure_countable_increasing
```
```   622                           [OF m2 rA2, OF A0 ASuc])
```
```   623               ultimately
```
```   624               show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
```
```   625                     measure m2 (\<Union>i. A i)"
```
```   626                 by (rule LIMSEQ_unique)
```
```   627           next
```
```   628             fix A :: "nat => 'a2 set"
```
```   629               assume dA: "disjoint_family A"
```
```   630                  and rA1: "range A \<subseteq>
```
```   631                            {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
```
```   632                  and "range A \<subseteq> sigma_sets (space m2) a"
```
```   633               hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
```
```   634               hence Um2: "(\<Union>i. A i) \<in> sets m2"
```
```   635                 by (metis range_subsetD setsm2 sigma_sets.Union)
```
```   636               have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
```
```   637                 using rA1 by blast
```
```   638               hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
```
```   639                 by (simp add: o_def)
```
```   640               also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)"
```
```   641                 proof (rule measure_space.measure_countably_additive [OF m1] )
```
```   642                   show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
```
```   643                     using f12 rA2 by (auto simp add: measurable_def)
```
```   644                   show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
```
```   645                     by (auto simp add: disjoint_family_def)
```
```   646                   show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
```
```   647                     proof (rule sigma_algebra.countable_UN [OF sa1])
```
```   648                       show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
```
```   649                         by (auto simp add: measurable_def)
```
```   650                     qed
```
```   651                 qed
```
```   652               finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
```
```   653               with measure_space.measure_countably_additive [OF m2 rA2 dA Um2]
```
```   654               have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
```
```   655                 by (metis sums_unique)
```
```   656
```
```   657               moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
```
```   658                 by (simp add: vimage_UN)
```
```   659               ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
```
```   660                     measure m2 (\<Union>i. A i)"
```
```   661                 by metis
```
```   662           qed
```
```   663         finally have "sigma_sets (space m2) a
```
```   664               \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
```
```   665         hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
```
```   666           by (force simp add: setsm2)
```
```   667       }
```
```   668       thus "f \<in> measurable m1 m2 \<and>
```
```   669        (\<forall>y\<in>sets m2.
```
```   670            measure m1 (f -` y \<inter> space m1) = measure m2 y)"
```
```   671         by (blast intro: f12)
```
```   672     qed
```
```   673 qed
```
```   674
```
```   675 lemma measurable_ident:
```
```   676      "sigma_algebra M ==> id \<in> measurable M M"
```
```   677   apply (simp add: measurable_def)
```
```   678   apply (auto simp add: sigma_algebra_def algebra.Int algebra.top)
```
```   679   done
```
```   680
```
```   681 lemma measurable_comp:
```
```   682   fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
```
```   683   shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
```
```   684   apply (auto simp add: measurable_def vimage_compose)
```
```   685   apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
```
```   686   apply force+
```
```   687   done
```
```   688
```
```   689  lemma measurable_strong:
```
```   690   fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
```
```   691   assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
```
```   692       and c: "sigma_algebra c"
```
```   693       and t: "f ` (space a) \<subseteq> t"
```
```   694       and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
```
```   695   shows "(g o f) \<in> measurable a c"
```
```   696 proof -
```
```   697   have a: "sigma_algebra a" and b: "sigma_algebra b"
```
```   698    and fab: "f \<in> (space a -> space b)"
```
```   699    and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
```
```   700      by (auto simp add: measurable_def)
```
```   701   have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
```
```   702     by force
```
```   703   show ?thesis
```
```   704     apply (auto simp add: measurable_def vimage_compose a c)
```
```   705     apply (metis funcset_mem fab g)
```
```   706     apply (subst eq, metis ba cb)
```
```   707     done
```
```   708 qed
```
```   709
```
```   710 lemma measurable_mono1:
```
```   711      "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
```
```   712       \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
```
```   713   by (auto simp add: measurable_def)
```
```   714
```
```   715 lemma measurable_up_sigma:
```
```   716    "measurable a b \<subseteq> measurable (sigma (space a) (sets a)) b"
```
```   717   apply (auto simp add: measurable_def)
```
```   718   apply (metis sigma_algebra_iff2 sigma_algebra_sigma)
```
```   719   apply (metis algebra.simps(2) sigma_algebra.sigma_sets_eq sigma_def)
```
```   720   done
```
```   721
```
```   722 lemma measure_preserving_up:
```
```   723    "f \<in> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 \<Longrightarrow>
```
```   724     measure_space m1 \<Longrightarrow> sigma_algebra m1 \<Longrightarrow> a \<subseteq> sets m1
```
```   725     \<Longrightarrow> f \<in> measure_preserving m1 m2"
```
```   726   by (auto simp add: measure_preserving_def measurable_def)
```
```   727
```
```   728 lemma measure_preserving_up_sigma:
```
```   729    "measure_space m1 \<Longrightarrow> (sets m1 = sets (sigma (space m1) a))
```
```   730     \<Longrightarrow> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2
```
```   731         \<subseteq> measure_preserving m1 m2"
```
```   732   apply (rule subsetI)
```
```   733   apply (rule measure_preserving_up)
```
```   734   apply (simp_all add: measure_space_def sigma_def)
```
```   735   apply (metis sigma_algebra.sigma_sets_eq subsetI sigma_sets.Basic)
```
```   736   done
```
```   737
```
```   738 lemma (in sigma_algebra) measurable_prod_sigma:
```
```   739   assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
```
```   740   shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))
```
```   741                           (prod_sets (sets a1) (sets a2)))"
```
```   742 proof -
```
```   743   from 1 have sa1: "sigma_algebra a1" and fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
```
```   744      and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
```
```   745     by (auto simp add: measurable_def)
```
```   746   from 2 have sa2: "sigma_algebra a2" and fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
```
```   747      and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
```
```   748     by (auto simp add: measurable_def)
```
```   749   show ?thesis
```
```   750     proof (rule measurable_sigma)
```
```   751       show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
```
```   752         by (force simp add: prod_sets_def sigma_algebra_iff algebra_def)
```
```   753     next
```
```   754       show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
```
```   755         by (rule prod_final [OF fn1 fn2])
```
```   756     next
```
```   757       fix z
```
```   758       assume z: "z \<in> prod_sets (sets a1) (sets a2)"
```
```   759       thus "f -` z \<inter> space M \<in> sets M"
```
```   760         proof (auto simp add: prod_sets_def vimage_Times)
```
```   761           fix x y
```
```   762           assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
```
```   763           have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
```
```   764                 ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
```
```   765             by blast
```
```   766           also have "...  \<in> sets M" using x y q1 q2
```
```   767             by blast
```
```   768           finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
```
```   769         qed
```
```   770     qed
```
```   771 qed
```
```   772
```
```   773
```
```   774 lemma (in measure_space) measurable_range_reduce:
```
```   775    "f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> \<Longrightarrow>
```
```   776     s \<noteq> {}
```
```   777     \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
```
```   778   by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
```
```   779
```
```   780 lemma (in measure_space) measurable_Pow_to_Pow:
```
```   781    "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
```
```   782   by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
```
```   783
```
```   784 lemma (in measure_space) measurable_Pow_to_Pow_image:
```
```   785    "sets M = Pow (space M)
```
```   786     \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
```
```   787   by (simp add: measurable_def sigma_algebra_Pow) intro_locales
```
```   788
```
```   789 lemma (in measure_space) measure_real_sum_image:
```
```   790   assumes s: "s \<in> sets M"
```
```   791       and ssets: "\<And>x. x \<in> s ==> {x} \<in> sets M"
```
```   792       and fin: "finite s"
```
```   793   shows "measure M s = (\<Sum>x\<in>s. measure M {x})"
```
```   794 proof -
```
```   795   {
```
```   796     fix u
```
```   797     assume u: "u \<subseteq> s & u \<in> sets M"
```
```   798     hence "finite u"
```
```   799       by (metis fin finite_subset)
```
```   800     hence "measure M u = (\<Sum>x\<in>u. measure M {x})" using u
```
```   801       proof (induct u)
```
```   802         case empty
```
```   803         thus ?case by simp
```
```   804       next
```
```   805         case (insert x t)
```
```   806         hence x: "x \<in> s" and t: "t \<subseteq> s"
```
```   807           by (simp_all add: insert_subset)
```
```   808         hence ts: "t \<in> sets M"  using insert
```
```   809           by (metis Diff_insert_absorb Diff ssets)
```
```   810         have "measure M (insert x t) = measure M ({x} \<union> t)"
```
```   811           by simp
```
```   812         also have "... = measure M {x} + measure M t"
```
```   813           by (simp add: measure_additive insert insert_disjoint ssets x ts
```
```   814                   del: Un_insert_left)
```
```   815         also have "... = (\<Sum>x\<in>insert x t. measure M {x})"
```
```   816           by (simp add: x t ts insert)
```
```   817         finally show ?case .
```
```   818       qed
```
```   819     }
```
```   820   thus ?thesis
```
```   821     by (metis subset_refl s)
```
```   822 qed
```
```   823
```
```   824 lemma (in sigma_algebra) sigma_algebra_extend:
```
```   825      "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
```
```   826    by unfold_locales (auto intro!: space_closed)
```
```   827
```
```   828 lemma (in sigma_algebra) finite_additivity_sufficient:
```
```   829   assumes fin: "finite (space M)"
```
```   830       and posf: "positive M f" and addf: "additive M f"
```
```   831   defines "Mf \<equiv> \<lparr>space = space M, sets = sets M, measure = f\<rparr>"
```
```   832   shows "measure_space Mf"
```
```   833 proof -
```
```   834   have [simp]: "f {} = 0" using posf
```
```   835     by (simp add: positive_def)
```
```   836   have "countably_additive Mf f"
```
```   837     proof (auto simp add: countably_additive_def positive_def)
```
```   838       fix A :: "nat \<Rightarrow> 'a set"
```
```   839       assume A: "range A \<subseteq> sets Mf"
```
```   840          and disj: "disjoint_family A"
```
```   841          and UnA: "(\<Union>i. A i) \<in> sets Mf"
```
```   842       def I \<equiv> "{i. A i \<noteq> {}}"
```
```   843       have "Union (A ` I) \<subseteq> space M" using A
```
```   844         by (auto simp add: Mf_def) (metis range_subsetD subsetD sets_into_space)
```
```   845       hence "finite (A ` I)"
```
```   846         by (metis finite_UnionD finite_subset fin)
```
```   847       moreover have "inj_on A I" using disj
```
```   848         by (auto simp add: I_def disjoint_family_def inj_on_def)
```
```   849       ultimately have finI: "finite I"
```
```   850         by (metis finite_imageD)
```
```   851       hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
```
```   852         proof (cases "I = {}")
```
```   853           case True thus ?thesis by (simp add: I_def)
```
```   854         next
```
```   855           case False
```
```   856           hence "\<forall>i\<in>I. i < Suc(Max I)"
```
```   857             by (simp add: Max_less_iff [symmetric] finI)
```
```   858           hence "\<forall>m \<ge> Suc(Max I). A m = {}"
```
```   859             by (simp add: I_def) (metis less_le_not_le)
```
```   860           thus ?thesis
```
```   861             by blast
```
```   862         qed
```
```   863       then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
```
```   864       hence "\<forall>m\<ge>N. (f o A) m = 0"
```
```   865         by simp
```
```   866       hence "(\<lambda>n. f (A n)) sums setsum (f o A) {0..<N}"
```
```   867         by (simp add: series_zero o_def)
```
```   868       also have "... = f (\<Union>i<N. A i)"
```
```   869         proof (induct N)
```
```   870           case 0 thus ?case by simp
```
```   871         next
```
```   872           case (Suc n)
```
```   873           have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
```
```   874             proof (rule Caratheodory.additiveD [OF addf])
```
```   875               show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
```
```   876                 by (auto simp add: disjoint_family_def nat_less_le) blast
```
```   877               show "A n \<in> sets M" using A
```
```   878                 by (force simp add: Mf_def)
```
```   879               show "(\<Union>i<n. A i) \<in> sets M"
```
```   880                 proof (induct n)
```
```   881                   case 0 thus ?case by simp
```
```   882                 next
```
```   883                   case (Suc n) thus ?case using A
```
```   884                     by (simp add: lessThan_Suc Mf_def Un range_subsetD)
```
```   885                 qed
```
```   886             qed
```
```   887           thus ?case using Suc
```
```   888             by (simp add: lessThan_Suc)
```
```   889         qed
```
```   890       also have "... = f (\<Union>i. A i)"
```
```   891         proof -
```
```   892           have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
```
```   893             by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
```
```   894           thus ?thesis by simp
```
```   895         qed
```
```   896       finally show "(\<lambda>n. f (A n)) sums f (\<Union>i. A i)" .
```
```   897     qed
```
```   898   thus ?thesis using posf
```
```   899     by (simp add: Mf_def measure_space_def measure_space_axioms_def sigma_algebra_extend positive_def)
```
```   900 qed
```
```   901
```
```   902 lemma finite_additivity_sufficient:
```
```   903      "sigma_algebra M
```
```   904       \<Longrightarrow> finite (space M)
```
```   905       \<Longrightarrow> positive M (measure M) \<Longrightarrow> additive M (measure M)
```
```   906       \<Longrightarrow> measure_space M"
```
```   907   by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto)
```
```   908
```
```   909 end
```
```   910
```