src/HOL/Probability/Measure.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 46731 5302e932d1e5
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     1 (*  Title:      HOL/Probability/Measure.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 {* Properties about measure spaces *}
     8 
     9 theory Measure
    10   imports Caratheodory
    11 begin
    12 
    13 lemma measure_algebra_more[simp]:
    14   "\<lparr> space = A, sets = B, \<dots> = algebra.more M \<rparr> \<lparr> measure := m \<rparr> =
    15    \<lparr> space = A, sets = B, \<dots> = algebra.more (M \<lparr> measure := m \<rparr>) \<rparr>"
    16   by (cases M) simp
    17 
    18 lemma measure_algebra_more_eq[simp]:
    19   "\<And>X. measure \<lparr> space = T, sets = A, \<dots> = algebra.more X \<rparr> = measure X"
    20   unfolding measure_space.splits by simp
    21 
    22 lemma measure_sigma[simp]: "measure (sigma A) = measure A"
    23   unfolding sigma_def by simp
    24 
    25 lemma algebra_measure_update[simp]:
    26   "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
    27   unfolding algebra_iff_Un by simp
    28 
    29 lemma sigma_algebra_measure_update[simp]:
    30   "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
    31   unfolding sigma_algebra_def sigma_algebra_axioms_def by simp
    32 
    33 lemma finite_sigma_algebra_measure_update[simp]:
    34   "finite_sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> finite_sigma_algebra M'"
    35   unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp
    36 
    37 lemma measurable_cancel_measure[simp]:
    38   "measurable M1 (M2\<lparr>measure := m2\<rparr>) = measurable M1 M2"
    39   "measurable (M2\<lparr>measure := m1\<rparr>) M1 = measurable M2 M1"
    40   unfolding measurable_def by auto
    41 
    42 lemma inj_on_image_eq_iff:
    43   assumes "inj_on f S"
    44   assumes "A \<subseteq> S" "B \<subseteq> S"
    45   shows "(f ` A = f ` B) \<longleftrightarrow> (A = B)"
    46 proof -
    47   have "inj_on f (A \<union> B)"
    48     using assms by (auto intro: subset_inj_on)
    49   from inj_on_Un_image_eq_iff[OF this]
    50   show ?thesis .
    51 qed
    52 
    53 lemma image_vimage_inter_eq:
    54   assumes "f ` S = T" "X \<subseteq> T"
    55   shows "f ` (f -` X \<inter> S) = X"
    56 proof (intro antisym)
    57   have "f ` (f -` X \<inter> S) \<subseteq> f ` (f -` X)" by auto
    58   also have "\<dots> = X \<inter> range f" by simp
    59   also have "\<dots> = X" using assms by auto
    60   finally show "f ` (f -` X \<inter> S) \<subseteq> X" by auto
    61 next
    62   show "X \<subseteq> f ` (f -` X \<inter> S)"
    63   proof
    64     fix x assume "x \<in> X"
    65     then have "x \<in> T" using `X \<subseteq> T` by auto
    66     then obtain y where "x = f y" "y \<in> S"
    67       using assms by auto
    68     then have "{y} \<subseteq> f -` X \<inter> S" using `x \<in> X` by auto
    69     moreover have "x \<in> f ` {y}" using `x = f y` by auto
    70     ultimately show "x \<in> f ` (f -` X \<inter> S)" by auto
    71   qed
    72 qed
    73 
    74 text {*
    75   This formalisation of measure theory is based on the work of Hurd/Coble wand
    76   was later translated by Lawrence Paulson to Isabelle/HOL. Later it was
    77   modified to use the positive infinite reals and to prove the uniqueness of
    78   cut stable measures.
    79 *}
    80 
    81 section {* Equations for the measure function @{text \<mu>} *}
    82 
    83 lemma (in measure_space) measure_countably_additive:
    84   assumes "range A \<subseteq> sets M" "disjoint_family A"
    85   shows "(\<Sum>i. \<mu> (A i)) = \<mu> (\<Union>i. A i)"
    86 proof -
    87   have "(\<Union> i. A i) \<in> sets M" using assms(1) by (rule countable_UN)
    88   with ca assms show ?thesis by (simp add: countably_additive_def)
    89 qed
    90 
    91 lemma (in sigma_algebra) sigma_algebra_cong:
    92   assumes "space N = space M" "sets N = sets M"
    93   shows "sigma_algebra N"
    94   by default (insert sets_into_space, auto simp: assms)
    95 
    96 lemma (in measure_space) measure_space_cong:
    97   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"
    98   shows "measure_space N"
    99 proof -
   100   interpret N: sigma_algebra N by (intro sigma_algebra_cong assms)
   101   show ?thesis
   102   proof
   103     show "positive N (measure N)" using assms by (auto simp: positive_def)
   104     show "countably_additive N (measure N)" unfolding countably_additive_def
   105     proof safe
   106       fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets N" "disjoint_family A"
   107       then have "\<And>i. A i \<in> sets M" "(UNION UNIV A) \<in> sets M" unfolding assms by auto
   108       from measure_countably_additive[of A] A this[THEN assms(1)]
   109       show "(\<Sum>n. measure N (A n)) = measure N (UNION UNIV A)"
   110         unfolding assms by simp
   111     qed
   112   qed
   113 qed
   114 
   115 lemma (in measure_space) additive: "additive M \<mu>"
   116   using ca by (auto intro!: countably_additive_additive simp: positive_def)
   117 
   118 lemma (in measure_space) measure_additive:
   119      "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}
   120       \<Longrightarrow> \<mu> a + \<mu> b = \<mu> (a \<union> b)"
   121   by (metis additiveD additive)
   122 
   123 lemma (in measure_space) measure_mono:
   124   assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
   125   shows "\<mu> a \<le> \<mu> b"
   126 proof -
   127   have "b = a \<union> (b - a)" using assms by auto
   128   moreover have "{} = a \<inter> (b - a)" by auto
   129   ultimately have "\<mu> b = \<mu> a + \<mu> (b - a)"
   130     using measure_additive[of a "b - a"] Diff[of b a] assms by auto
   131   moreover have "\<mu> a + 0 \<le> \<mu> a + \<mu> (b - a)" using assms by (intro add_mono) auto
   132   ultimately show "\<mu> a \<le> \<mu> b" by auto
   133 qed
   134 
   135 lemma (in measure_space) measure_top:
   136   "A \<in> sets M \<Longrightarrow> \<mu> A \<le> \<mu> (space M)"
   137   using sets_into_space[of A] by (auto intro!: measure_mono)
   138 
   139 lemma (in measure_space) measure_compl:
   140   assumes s: "s \<in> sets M" and fin: "\<mu> s \<noteq> \<infinity>"
   141   shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s"
   142 proof -
   143   have s_less_space: "\<mu> s \<le> \<mu> (space M)"
   144     using s by (auto intro!: measure_mono sets_into_space)
   145   from s have "0 \<le> \<mu> s" by auto
   146   have "\<mu> (space M) = \<mu> (s \<union> (space M - s))" using s
   147     by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
   148   also have "... = \<mu> s + \<mu> (space M - s)"
   149     by (rule additiveD [OF additive]) (auto simp add: s)
   150   finally have "\<mu> (space M) = \<mu> s + \<mu> (space M - s)" .
   151   then show ?thesis
   152     using fin `0 \<le> \<mu> s`
   153     unfolding ereal_eq_minus_iff by (auto simp: ac_simps)
   154 qed
   155 
   156 lemma (in measure_space) measure_Diff:
   157   assumes finite: "\<mu> B \<noteq> \<infinity>"
   158   and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
   159   shows "\<mu> (A - B) = \<mu> A - \<mu> B"
   160 proof -
   161   have "0 \<le> \<mu> B" using assms by auto
   162   have "(A - B) \<union> B = A" using `B \<subseteq> A` by auto
   163   then have "\<mu> A = \<mu> ((A - B) \<union> B)" by simp
   164   also have "\<dots> = \<mu> (A - B) + \<mu> B"
   165     using measurable by (subst measure_additive[symmetric]) auto
   166   finally show "\<mu> (A - B) = \<mu> A - \<mu> B"
   167     unfolding ereal_eq_minus_iff
   168     using finite `0 \<le> \<mu> B` by auto
   169 qed
   170 
   171 lemma (in measure_space) measure_countable_increasing:
   172   assumes A: "range A \<subseteq> sets M"
   173       and A0: "A 0 = {}"
   174       and ASuc: "\<And>n. A n \<subseteq> A (Suc n)"
   175   shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
   176 proof -
   177   { fix n
   178     have "\<mu> (A n) = (\<Sum>i<n. \<mu> (A (Suc i) - A i))"
   179       proof (induct n)
   180         case 0 thus ?case by (auto simp add: A0)
   181       next
   182         case (Suc m)
   183         have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
   184           by (metis ASuc Un_Diff_cancel Un_absorb1)
   185         hence "\<mu> (A (Suc m)) =
   186                \<mu> (A m) + \<mu> (A (Suc m) - A m)"
   187           by (subst measure_additive)
   188              (auto simp add: measure_additive range_subsetD [OF A])
   189         with Suc show ?case
   190           by simp
   191       qed }
   192   note Meq = this
   193   have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
   194     proof (rule UN_finite2_eq [where k=1], simp)
   195       fix i
   196       show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
   197         proof (induct i)
   198           case 0 thus ?case by (simp add: A0)
   199         next
   200           case (Suc i)
   201           thus ?case
   202             by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
   203         qed
   204     qed
   205   have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
   206     by (metis A Diff range_subsetD)
   207   have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
   208     by (blast intro: range_subsetD [OF A])
   209   have "(SUP n. \<Sum>i<n. \<mu> (A (Suc i) - A i)) = (\<Sum>i. \<mu> (A (Suc i) - A i))"
   210     using A by (auto intro!: suminf_ereal_eq_SUPR[symmetric])
   211   also have "\<dots> = \<mu> (\<Union>i. A (Suc i) - A i)"
   212     by (rule measure_countably_additive)
   213        (auto simp add: disjoint_family_Suc ASuc A1 A2)
   214   also have "... =  \<mu> (\<Union>i. A i)"
   215     by (simp add: Aeq)
   216   finally have "(SUP n. \<Sum>i<n. \<mu> (A (Suc i) - A i)) = \<mu> (\<Union>i. A i)" .
   217   then show ?thesis by (auto simp add: Meq)
   218 qed
   219 
   220 lemma (in measure_space) continuity_from_below:
   221   assumes A: "range A \<subseteq> sets M" and "incseq A"
   222   shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
   223 proof -
   224   have *: "(SUP n. \<mu> (nat_case {} A (Suc n))) = (SUP n. \<mu> (nat_case {} A n))"
   225     using A by (auto intro!: SUPR_eq exI split: nat.split)
   226   have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
   227     by (auto simp add: split: nat.splits)
   228   have meq: "\<And>n. \<mu> (A n) = (\<mu> \<circ> nat_case {} A) (Suc n)"
   229     by simp
   230   have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. nat_case {} A i)"
   231     using range_subsetD[OF A] incseq_SucD[OF `incseq A`]
   232     by (force split: nat.splits intro!: measure_countable_increasing)
   233   also have "\<mu> (\<Union>i. nat_case {} A i) = \<mu> (\<Union>i. A i)"
   234     by (simp add: ueq)
   235   finally have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. A i)" .
   236   thus ?thesis unfolding meq * comp_def .
   237 qed
   238 
   239 lemma (in measure_space) measure_incseq:
   240   assumes "range B \<subseteq> sets M" "incseq B"
   241   shows "incseq (\<lambda>i. \<mu> (B i))"
   242   using assms by (auto simp: incseq_def intro!: measure_mono)
   243 
   244 lemma (in measure_space) continuity_from_below_Lim:
   245   assumes A: "range A \<subseteq> sets M" "incseq A"
   246   shows "(\<lambda>i. (\<mu> (A i))) ----> \<mu> (\<Union>i. A i)"
   247   using LIMSEQ_ereal_SUPR[OF measure_incseq, OF A]
   248     continuity_from_below[OF A] by simp
   249 
   250 lemma (in measure_space) measure_decseq:
   251   assumes "range B \<subseteq> sets M" "decseq B"
   252   shows "decseq (\<lambda>i. \<mu> (B i))"
   253   using assms by (auto simp: decseq_def intro!: measure_mono)
   254 
   255 lemma (in measure_space) continuity_from_above:
   256   assumes A: "range A \<subseteq> sets M" and "decseq A"
   257   and finite: "\<And>i. \<mu> (A i) \<noteq> \<infinity>"
   258   shows "(INF n. \<mu> (A n)) = \<mu> (\<Inter>i. A i)"
   259 proof -
   260   have le_MI: "\<mu> (\<Inter>i. A i) \<le> \<mu> (A 0)"
   261     using A by (auto intro!: measure_mono)
   262   hence *: "\<mu> (\<Inter>i. A i) \<noteq> \<infinity>" using finite[of 0] by auto
   263 
   264   have A0: "0 \<le> \<mu> (A 0)" using A by auto
   265 
   266   have "\<mu> (A 0) - (INF n. \<mu> (A n)) = \<mu> (A 0) + (SUP n. - \<mu> (A n))"
   267     by (simp add: ereal_SUPR_uminus minus_ereal_def)
   268   also have "\<dots> = (SUP n. \<mu> (A 0) - \<mu> (A n))"
   269     unfolding minus_ereal_def using A0 assms
   270     by (subst SUPR_ereal_add) (auto simp add: measure_decseq)
   271   also have "\<dots> = (SUP n. \<mu> (A 0 - A n))"
   272     using A finite `decseq A`[unfolded decseq_def] by (subst measure_Diff) auto
   273   also have "\<dots> = \<mu> (\<Union>i. A 0 - A i)"
   274   proof (rule continuity_from_below)
   275     show "range (\<lambda>n. A 0 - A n) \<subseteq> sets M"
   276       using A by auto
   277     show "incseq (\<lambda>n. A 0 - A n)"
   278       using `decseq A` by (auto simp add: incseq_def decseq_def)
   279   qed
   280   also have "\<dots> = \<mu> (A 0) - \<mu> (\<Inter>i. A i)"
   281     using A finite * by (simp, subst measure_Diff) auto
   282   finally show ?thesis
   283     unfolding ereal_minus_eq_minus_iff using finite A0 by auto
   284 qed
   285 
   286 lemma (in measure_space) measure_insert:
   287   assumes sets: "{x} \<in> sets M" "A \<in> sets M" and "x \<notin> A"
   288   shows "\<mu> (insert x A) = \<mu> {x} + \<mu> A"
   289 proof -
   290   have "{x} \<inter> A = {}" using `x \<notin> A` by auto
   291   from measure_additive[OF sets this] show ?thesis by simp
   292 qed
   293 
   294 lemma (in measure_space) measure_setsum:
   295   assumes "finite S" and "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M"
   296   assumes disj: "disjoint_family_on A S"
   297   shows "(\<Sum>i\<in>S. \<mu> (A i)) = \<mu> (\<Union>i\<in>S. A i)"
   298 using assms proof induct
   299   case (insert i S)
   300   then have "(\<Sum>i\<in>S. \<mu> (A i)) = \<mu> (\<Union>a\<in>S. A a)"
   301     by (auto intro: disjoint_family_on_mono)
   302   moreover have "A i \<inter> (\<Union>a\<in>S. A a) = {}"
   303     using `disjoint_family_on A (insert i S)` `i \<notin> S`
   304     by (auto simp: disjoint_family_on_def)
   305   ultimately show ?case using insert
   306     by (auto simp: measure_additive finite_UN)
   307 qed simp
   308 
   309 lemma (in measure_space) measure_finite_singleton:
   310   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
   311   shows "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})"
   312   using measure_setsum[of S "\<lambda>x. {x}", OF assms]
   313   by (auto simp: disjoint_family_on_def)
   314 
   315 lemma finite_additivity_sufficient:
   316   assumes "sigma_algebra M"
   317   assumes fin: "finite (space M)" and pos: "positive M (measure M)" and add: "additive M (measure M)"
   318   shows "measure_space M"
   319 proof -
   320   interpret sigma_algebra M by fact
   321   show ?thesis
   322   proof
   323     show [simp]: "positive M (measure M)" using pos by (simp add: positive_def)
   324     show "countably_additive M (measure M)"
   325     proof (auto simp add: countably_additive_def)
   326       fix A :: "nat \<Rightarrow> 'a set"
   327       assume A: "range A \<subseteq> sets M"
   328          and disj: "disjoint_family A"
   329          and UnA: "(\<Union>i. A i) \<in> sets M"
   330       def I \<equiv> "{i. A i \<noteq> {}}"
   331       have "Union (A ` I) \<subseteq> space M" using A
   332         by auto (metis range_subsetD subsetD sets_into_space)
   333       hence "finite (A ` I)"
   334         by (metis finite_UnionD finite_subset fin)
   335       moreover have "inj_on A I" using disj
   336         by (auto simp add: I_def disjoint_family_on_def inj_on_def)
   337       ultimately have finI: "finite I"
   338         by (metis finite_imageD)
   339       hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
   340         proof (cases "I = {}")
   341           case True thus ?thesis by (simp add: I_def)
   342         next
   343           case False
   344           hence "\<forall>i\<in>I. i < Suc(Max I)"
   345             by (simp add: Max_less_iff [symmetric] finI)
   346           hence "\<forall>m \<ge> Suc(Max I). A m = {}"
   347             by (simp add: I_def) (metis less_le_not_le)
   348           thus ?thesis
   349             by blast
   350         qed
   351       then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
   352       then have "\<forall>m\<ge>N. measure M (A m) = 0" using pos[unfolded positive_def] by simp
   353       then have "(\<Sum>n. measure M (A n)) = (\<Sum>m<N. measure M (A m))"
   354         by (simp add: suminf_finite)
   355       also have "... = measure M (\<Union>i<N. A i)"
   356         proof (induct N)
   357           case 0 thus ?case using pos[unfolded positive_def] by simp
   358         next
   359           case (Suc n)
   360           have "measure M (A n \<union> (\<Union> x<n. A x)) = measure M (A n) + measure M (\<Union> i<n. A i)"
   361             proof (rule Caratheodory.additiveD [OF add])
   362               show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
   363                 by (auto simp add: disjoint_family_on_def nat_less_le) blast
   364               show "A n \<in> sets M" using A
   365                 by force
   366               show "(\<Union>i<n. A i) \<in> sets M"
   367                 proof (induct n)
   368                   case 0 thus ?case by simp
   369                 next
   370                   case (Suc n) thus ?case using A
   371                     by (simp add: lessThan_Suc Un range_subsetD)
   372                 qed
   373             qed
   374           thus ?case using Suc
   375             by (simp add: lessThan_Suc)
   376         qed
   377       also have "... = measure M (\<Union>i. A i)"
   378         proof -
   379           have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
   380             by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
   381           thus ?thesis by simp
   382         qed
   383       finally show "(\<Sum>n. measure M (A n)) = measure M (\<Union>i. A i)" .
   384     qed
   385   qed
   386 qed
   387 
   388 lemma (in measure_space) measure_setsum_split:
   389   assumes "finite S" and "A \<in> sets M" and br_in_M: "B ` S \<subseteq> sets M"
   390   assumes "(\<Union>i\<in>S. B i) = space M"
   391   assumes "disjoint_family_on B S"
   392   shows "\<mu> A = (\<Sum>i\<in>S. \<mu> (A \<inter> (B i)))"
   393 proof -
   394   have *: "\<mu> A = \<mu> (\<Union>i\<in>S. A \<inter> B i)"
   395     using assms by auto
   396   show ?thesis unfolding *
   397   proof (rule measure_setsum[symmetric])
   398     show "disjoint_family_on (\<lambda>i. A \<inter> B i) S"
   399       using `disjoint_family_on B S`
   400       unfolding disjoint_family_on_def by auto
   401   qed (insert assms, auto)
   402 qed
   403 
   404 lemma (in measure_space) measure_subadditive:
   405   assumes measurable: "A \<in> sets M" "B \<in> sets M"
   406   shows "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B"
   407 proof -
   408   from measure_additive[of A "B - A"]
   409   have "\<mu> (A \<union> B) = \<mu> A + \<mu> (B - A)"
   410     using assms by (simp add: Diff)
   411   also have "\<dots> \<le> \<mu> A + \<mu> B"
   412     using assms by (auto intro!: add_left_mono measure_mono)
   413   finally show ?thesis .
   414 qed
   415 
   416 lemma (in measure_space) measure_subadditive_finite:
   417   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
   418   shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
   419 using assms proof induct
   420   case (insert i I)
   421   then have "\<mu> (\<Union>i\<in>insert i I. A i) = \<mu> (A i \<union> (\<Union>i\<in>I. A i))"
   422     by simp
   423   also have "\<dots> \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
   424     using insert by (intro measure_subadditive finite_UN) auto
   425   also have "\<dots> \<le> \<mu> (A i) + (\<Sum>i\<in>I. \<mu> (A i))"
   426     using insert by (intro add_mono) auto
   427   also have "\<dots> = (\<Sum>i\<in>insert i I. \<mu> (A i))"
   428     using insert by auto
   429   finally show ?case .
   430 qed simp
   431 
   432 lemma (in measure_space) measure_eq_0:
   433   assumes "N \<in> sets M" and "\<mu> N = 0" and "K \<subseteq> N" and "K \<in> sets M"
   434   shows "\<mu> K = 0"
   435   using measure_mono[OF assms(3,4,1)] assms(2) positive_measure[OF assms(4)] by auto
   436 
   437 lemma (in measure_space) measure_finitely_subadditive:
   438   assumes "finite I" "A ` I \<subseteq> sets M"
   439   shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
   440 using assms proof induct
   441   case (insert i I)
   442   then have "(\<Union>i\<in>I. A i) \<in> sets M" by auto
   443   then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
   444     using insert by (simp add: measure_subadditive)
   445   also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
   446     using insert by (auto intro!: add_left_mono)
   447   finally show ?case .
   448 qed simp
   449 
   450 lemma (in measure_space) measure_countably_subadditive:
   451   assumes "range f \<subseteq> sets M"
   452   shows "\<mu> (\<Union>i. f i) \<le> (\<Sum>i. \<mu> (f i))"
   453 proof -
   454   have "\<mu> (\<Union>i. f i) = \<mu> (\<Union>i. disjointed f i)"
   455     unfolding UN_disjointed_eq ..
   456   also have "\<dots> = (\<Sum>i. \<mu> (disjointed f i))"
   457     using range_disjointed_sets[OF assms] measure_countably_additive
   458     by (simp add:  disjoint_family_disjointed comp_def)
   459   also have "\<dots> \<le> (\<Sum>i. \<mu> (f i))"
   460     using range_disjointed_sets[OF assms] assms
   461     by (auto intro!: suminf_le_pos measure_mono disjointed_subset)
   462   finally show ?thesis .
   463 qed
   464 
   465 lemma (in measure_space) measure_UN_eq_0:
   466   assumes "\<And>i::nat. \<mu> (N i) = 0" and "range N \<subseteq> sets M"
   467   shows "\<mu> (\<Union> i. N i) = 0"
   468 proof -
   469   have "0 \<le> \<mu> (\<Union> i. N i)" using assms by auto
   470   moreover have "\<mu> (\<Union> i. N i) \<le> 0"
   471     using measure_countably_subadditive[OF assms(2)] assms(1) by simp
   472   ultimately show ?thesis by simp
   473 qed
   474 
   475 lemma (in measure_space) measure_inter_full_set:
   476   assumes "S \<in> sets M" "T \<in> sets M" and fin: "\<mu> (T - S) \<noteq> \<infinity>"
   477   assumes T: "\<mu> T = \<mu> (space M)"
   478   shows "\<mu> (S \<inter> T) = \<mu> S"
   479 proof (rule antisym)
   480   show " \<mu> (S \<inter> T) \<le> \<mu> S"
   481     using assms by (auto intro!: measure_mono)
   482 
   483   have pos: "0 \<le> \<mu> (T - S)" using assms by auto
   484   show "\<mu> S \<le> \<mu> (S \<inter> T)"
   485   proof (rule ccontr)
   486     assume contr: "\<not> ?thesis"
   487     have "\<mu> (space M) = \<mu> ((T - S) \<union> (S \<inter> T))"
   488       unfolding T[symmetric] by (auto intro!: arg_cong[where f="\<mu>"])
   489     also have "\<dots> \<le> \<mu> (T - S) + \<mu> (S \<inter> T)"
   490       using assms by (auto intro!: measure_subadditive)
   491     also have "\<dots> < \<mu> (T - S) + \<mu> S"
   492       using fin contr pos by (intro ereal_less_add) auto
   493     also have "\<dots> = \<mu> (T \<union> S)"
   494       using assms by (subst measure_additive) auto
   495     also have "\<dots> \<le> \<mu> (space M)"
   496       using assms sets_into_space by (auto intro!: measure_mono)
   497     finally show False ..
   498   qed
   499 qed
   500 
   501 lemma measure_unique_Int_stable:
   502   fixes E :: "('a, 'b) algebra_scheme" and A :: "nat \<Rightarrow> 'a set"
   503   assumes "Int_stable E"
   504   and A: "range A \<subseteq> sets E" "incseq A" "(\<Union>i. A i) = space E"
   505   and M: "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<mu>\<rparr>" (is "measure_space ?M")
   506   and N: "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<nu>\<rparr>" (is "measure_space ?N")
   507   and eq: "\<And>X. X \<in> sets E \<Longrightarrow> \<mu> X = \<nu> X"
   508   and finite: "\<And>i. \<mu> (A i) \<noteq> \<infinity>"
   509   assumes "X \<in> sets (sigma E)"
   510   shows "\<mu> X = \<nu> X"
   511 proof -
   512   let ?D = "\<lambda>F. {D. D \<in> sets (sigma E) \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
   513   interpret M: measure_space ?M
   514     where "space ?M = space E" and "sets ?M = sets (sigma E)" and "measure ?M = \<mu>" by (simp_all add: M)
   515   interpret N: measure_space ?N
   516     where "space ?N = space E" and "sets ?N = sets (sigma E)" and "measure ?N = \<nu>" by (simp_all add: N)
   517   { fix F assume "F \<in> sets E" and "\<mu> F \<noteq> \<infinity>"
   518     then have [intro]: "F \<in> sets (sigma E)" by auto
   519     have "\<nu> F \<noteq> \<infinity>" using `\<mu> F \<noteq> \<infinity>` `F \<in> sets E` eq by simp
   520     interpret D: dynkin_system "\<lparr>space=space E, sets=?D F\<rparr>"
   521     proof (rule dynkin_systemI, simp_all)
   522       fix A assume "A \<in> sets (sigma E) \<and> \<mu> (F \<inter> A) = \<nu> (F \<inter> A)"
   523       then show "A \<subseteq> space E" using M.sets_into_space by auto
   524     next
   525       have "F \<inter> space E = F" using `F \<in> sets E` by auto
   526       then show "\<mu> (F \<inter> space E) = \<nu> (F \<inter> space E)"
   527         using `F \<in> sets E` eq by auto
   528     next
   529       fix A assume *: "A \<in> sets (sigma E) \<and> \<mu> (F \<inter> A) = \<nu> (F \<inter> A)"
   530       then have **: "F \<inter> (space (sigma E) - A) = F - (F \<inter> A)"
   531         and [intro]: "F \<inter> A \<in> sets (sigma E)"
   532         using `F \<in> sets E` M.sets_into_space by auto
   533       have "\<nu> (F \<inter> A) \<le> \<nu> F" by (auto intro!: N.measure_mono)
   534       then have "\<nu> (F \<inter> A) \<noteq> \<infinity>" using `\<nu> F \<noteq> \<infinity>` by auto
   535       have "\<mu> (F \<inter> A) \<le> \<mu> F" by (auto intro!: M.measure_mono)
   536       then have "\<mu> (F \<inter> A) \<noteq> \<infinity>" using `\<mu> F \<noteq> \<infinity>` by auto
   537       then have "\<mu> (F \<inter> (space (sigma E) - A)) = \<mu> F - \<mu> (F \<inter> A)" unfolding **
   538         using `F \<inter> A \<in> sets (sigma E)` by (auto intro!: M.measure_Diff)
   539       also have "\<dots> = \<nu> F - \<nu> (F \<inter> A)" using eq `F \<in> sets E` * by simp
   540       also have "\<dots> = \<nu> (F \<inter> (space (sigma E) - A))" unfolding **
   541         using `F \<inter> A \<in> sets (sigma E)` `\<nu> (F \<inter> A) \<noteq> \<infinity>` by (auto intro!: N.measure_Diff[symmetric])
   542       finally show "space E - A \<in> sets (sigma E) \<and> \<mu> (F \<inter> (space E - A)) = \<nu> (F \<inter> (space E - A))"
   543         using * by auto
   544     next
   545       fix A :: "nat \<Rightarrow> 'a set"
   546       assume "disjoint_family A" "range A \<subseteq> {X \<in> sets (sigma E). \<mu> (F \<inter> X) = \<nu> (F \<inter> X)}"
   547       then have A: "range (\<lambda>i. F \<inter> A i) \<subseteq> sets (sigma E)" "F \<inter> (\<Union>x. A x) = (\<Union>x. F \<inter> A x)"
   548         "disjoint_family (\<lambda>i. F \<inter> A i)" "\<And>i. \<mu> (F \<inter> A i) = \<nu> (F \<inter> A i)" "range A \<subseteq> sets (sigma E)"
   549         by (auto simp: disjoint_family_on_def subset_eq)
   550       then show "(\<Union>x. A x) \<in> sets (sigma E) \<and> \<mu> (F \<inter> (\<Union>x. A x)) = \<nu> (F \<inter> (\<Union>x. A x))"
   551         by (auto simp: M.measure_countably_additive[symmetric]
   552                        N.measure_countably_additive[symmetric]
   553             simp del: UN_simps)
   554     qed
   555     have *: "sets (sigma E) = sets \<lparr>space = space E, sets = ?D F\<rparr>"
   556       using `F \<in> sets E` `Int_stable E`
   557       by (intro D.dynkin_lemma)
   558          (auto simp add: sets_sigma Int_stable_def eq intro: sigma_sets.Basic)
   559     have "\<And>D. D \<in> sets (sigma E) \<Longrightarrow> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)"
   560       by (subst (asm) *) auto }
   561   note * = this
   562   let ?A = "\<lambda>i. A i \<inter> X"
   563   have A': "range ?A \<subseteq> sets (sigma E)" "incseq ?A"
   564     using A(1,2) `X \<in> sets (sigma E)` by (auto simp: incseq_def)
   565   { fix i have "\<mu> (?A i) = \<nu> (?A i)"
   566       using *[of "A i" X] `X \<in> sets (sigma E)` A finite by auto }
   567   with M.continuity_from_below[OF A'] N.continuity_from_below[OF A']
   568   show ?thesis using A(3) `X \<in> sets (sigma E)` by auto
   569 qed
   570 
   571 section "@{text \<mu>}-null sets"
   572 
   573 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
   574 
   575 sublocale measure_space \<subseteq> nullsets!: ring_of_sets "\<lparr> space = space M, sets = null_sets \<rparr>"
   576   where "space \<lparr> space = space M, sets = null_sets \<rparr> = space M"
   577   and "sets \<lparr> space = space M, sets = null_sets \<rparr> = null_sets"
   578 proof -
   579   { fix A B assume sets: "A \<in> sets M" "B \<in> sets M"
   580     moreover then have "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B" "\<mu> (A - B) \<le> \<mu> A"
   581       by (auto intro!: measure_subadditive measure_mono)
   582     moreover assume "\<mu> B = 0" "\<mu> A = 0"
   583     ultimately have "\<mu> (A - B) = 0" "\<mu> (A \<union> B) = 0"
   584       by (auto intro!: antisym) }
   585   note null = this
   586   show "ring_of_sets \<lparr> space = space M, sets = null_sets \<rparr>"
   587     by default (insert sets_into_space null, auto)
   588 qed simp_all
   589 
   590 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
   591 proof -
   592   have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
   593     unfolding SUP_def image_compose
   594     unfolding surj_from_nat ..
   595   then show ?thesis by simp
   596 qed
   597 
   598 lemma (in measure_space) null_sets_UN[intro]:
   599   assumes "\<And>i::'i::countable. N i \<in> null_sets"
   600   shows "(\<Union>i. N i) \<in> null_sets"
   601 proof (intro conjI CollectI)
   602   show "(\<Union>i. N i) \<in> sets M" using assms by auto
   603   then have "0 \<le> \<mu> (\<Union>i. N i)" by simp
   604   moreover have "\<mu> (\<Union>i. N i) \<le> (\<Sum>n. \<mu> (N (Countable.from_nat n)))"
   605     unfolding UN_from_nat[of N]
   606     using assms by (intro measure_countably_subadditive) auto
   607   ultimately show "\<mu> (\<Union>i. N i) = 0" using assms by auto
   608 qed
   609 
   610 lemma (in measure_space) null_set_Int1:
   611   assumes "B \<in> null_sets" "A \<in> sets M" shows "A \<inter> B \<in> null_sets"
   612 using assms proof (intro CollectI conjI)
   613   show "\<mu> (A \<inter> B) = 0" using assms by (intro measure_eq_0[of B "A \<inter> B"]) auto
   614 qed auto
   615 
   616 lemma (in measure_space) null_set_Int2:
   617   assumes "B \<in> null_sets" "A \<in> sets M" shows "B \<inter> A \<in> null_sets"
   618   using assms by (subst Int_commute) (rule null_set_Int1)
   619 
   620 lemma (in measure_space) measure_Diff_null_set:
   621   assumes "B \<in> null_sets" "A \<in> sets M"
   622   shows "\<mu> (A - B) = \<mu> A"
   623 proof -
   624   have *: "A - B = (A - (A \<inter> B))" by auto
   625   have "A \<inter> B \<in> null_sets" using assms by (rule null_set_Int1)
   626   then show ?thesis
   627     unfolding * using assms
   628     by (subst measure_Diff) auto
   629 qed
   630 
   631 lemma (in measure_space) null_set_Diff:
   632   assumes "B \<in> null_sets" "A \<in> sets M" shows "B - A \<in> null_sets"
   633 using assms proof (intro CollectI conjI)
   634   show "\<mu> (B - A) = 0" using assms by (intro measure_eq_0[of B "B - A"]) auto
   635 qed auto
   636 
   637 lemma (in measure_space) measure_Un_null_set:
   638   assumes "A \<in> sets M" "B \<in> null_sets"
   639   shows "\<mu> (A \<union> B) = \<mu> A"
   640 proof -
   641   have *: "A \<union> B = A \<union> (B - A)" by auto
   642   have "B - A \<in> null_sets" using assms(2,1) by (rule null_set_Diff)
   643   then show ?thesis
   644     unfolding * using assms
   645     by (subst measure_additive[symmetric]) auto
   646 qed
   647 
   648 section "Formalise almost everywhere"
   649 
   650 definition (in measure_space)
   651   almost_everywhere :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "AE " 10) where
   652   "almost_everywhere P \<longleftrightarrow> (\<exists>N\<in>null_sets. { x \<in> space M. \<not> P x } \<subseteq> N)"
   653 
   654 syntax
   655   "_almost_everywhere" :: "pttrn \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
   656 
   657 translations
   658   "AE x in M. P" == "CONST measure_space.almost_everywhere M (%x. P)"
   659 
   660 lemma (in measure_space) AE_cong_measure:
   661   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
   662   shows "(AE x in N. P x) \<longleftrightarrow> (AE x. P x)"
   663 proof -
   664   interpret N: measure_space N
   665     by (rule measure_space_cong) fact+
   666   show ?thesis
   667     unfolding N.almost_everywhere_def almost_everywhere_def
   668     by (auto simp: assms)
   669 qed
   670 
   671 lemma (in measure_space) AE_I':
   672   "N \<in> null_sets \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x. P x)"
   673   unfolding almost_everywhere_def by auto
   674 
   675 lemma (in measure_space) AE_iff_null_set:
   676   assumes "{x\<in>space M. \<not> P x} \<in> sets M" (is "?P \<in> sets M")
   677   shows "(AE x. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets"
   678 proof
   679   assume "AE x. P x" then obtain N where N: "N \<in> sets M" "?P \<subseteq> N" "\<mu> N = 0"
   680     unfolding almost_everywhere_def by auto
   681   have "0 \<le> \<mu> ?P" using assms by simp
   682   moreover have "\<mu> ?P \<le> \<mu> N"
   683     using assms N(1,2) by (auto intro: measure_mono)
   684   ultimately have "\<mu> ?P = 0" unfolding `\<mu> N = 0` by auto
   685   then show "?P \<in> null_sets" using assms by simp
   686 next
   687   assume "?P \<in> null_sets" with assms show "AE x. P x" by (auto intro: AE_I')
   688 qed
   689 
   690 lemma (in measure_space) AE_iff_measurable:
   691   "N \<in> sets M \<Longrightarrow> {x\<in>space M. \<not> P x} = N \<Longrightarrow> (AE x. P x) \<longleftrightarrow> \<mu> N = 0"
   692   using AE_iff_null_set[of P] by simp
   693 
   694 lemma (in measure_space) AE_True[intro, simp]: "AE x. True"
   695   unfolding almost_everywhere_def by auto
   696 
   697 lemma (in measure_space) AE_E[consumes 1]:
   698   assumes "AE x. P x"
   699   obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
   700   using assms unfolding almost_everywhere_def by auto
   701 
   702 lemma (in measure_space) AE_E2:
   703   assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
   704   shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
   705 proof -
   706   have "{x\<in>space M. \<not> P x} = space M - {x\<in>space M. P x}"
   707     by auto
   708   with AE_iff_null_set[of P] assms show ?thesis by auto
   709 qed
   710 
   711 lemma (in measure_space) AE_I:
   712   assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
   713   shows "AE x. P x"
   714   using assms unfolding almost_everywhere_def by auto
   715 
   716 lemma (in measure_space) AE_mp[elim!]:
   717   assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \<longrightarrow> Q x"
   718   shows "AE x. Q x"
   719 proof -
   720   from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
   721     and A: "A \<in> sets M" "\<mu> A = 0"
   722     by (auto elim!: AE_E)
   723 
   724   from AE_imp obtain B where imp: "{x\<in>space M. P x \<and> \<not> Q x} \<subseteq> B"
   725     and B: "B \<in> sets M" "\<mu> B = 0"
   726     by (auto elim!: AE_E)
   727 
   728   show ?thesis
   729   proof (intro AE_I)
   730     have "0 \<le> \<mu> (A \<union> B)" using A B by auto
   731     moreover have "\<mu> (A \<union> B) \<le> 0"
   732       using measure_subadditive[of A B] A B by auto
   733     ultimately show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B by auto
   734     show "{x\<in>space M. \<not> Q x} \<subseteq> A \<union> B"
   735       using P imp by auto
   736   qed
   737 qed
   738 
   739 lemma (in measure_space)
   740   shows AE_iffI: "AE x. P x \<Longrightarrow> AE x. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x. Q x"
   741     and AE_disjI1: "AE x. P x \<Longrightarrow> AE x. P x \<or> Q x"
   742     and AE_disjI2: "AE x. Q x \<Longrightarrow> AE x. P x \<or> Q x"
   743     and AE_conjI: "AE x. P x \<Longrightarrow> AE x. Q x \<Longrightarrow> AE x. P x \<and> Q x"
   744     and AE_conj_iff[simp]: "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
   745   by auto
   746 
   747 lemma (in measure_space) AE_measure:
   748   assumes AE: "AE x. P x" and sets: "{x\<in>space M. P x} \<in> sets M"
   749   shows "\<mu> {x\<in>space M. P x} = \<mu> (space M)"
   750 proof -
   751   from AE_E[OF AE] guess N . note N = this
   752   with sets have "\<mu> (space M) \<le> \<mu> ({x\<in>space M. P x} \<union> N)"
   753     by (intro measure_mono) auto
   754   also have "\<dots> \<le> \<mu> {x\<in>space M. P x} + \<mu> N"
   755     using sets N by (intro measure_subadditive) auto
   756   also have "\<dots> = \<mu> {x\<in>space M. P x}" using N by simp
   757   finally show "\<mu> {x\<in>space M. P x} = \<mu> (space M)"
   758     using measure_top[OF sets] by auto
   759 qed
   760 
   761 lemma (in measure_space) AE_space: "AE x. x \<in> space M"
   762   by (rule AE_I[where N="{}"]) auto
   763 
   764 lemma (in measure_space) AE_I2[simp, intro]:
   765   "(\<And>x. x \<in> space M \<Longrightarrow> P x) \<Longrightarrow> AE x. P x"
   766   using AE_space by auto
   767 
   768 lemma (in measure_space) AE_Ball_mp:
   769   "\<forall>x\<in>space M. P x \<Longrightarrow> AE x. P x \<longrightarrow> Q x \<Longrightarrow> AE x. Q x"
   770   by auto
   771 
   772 lemma (in measure_space) AE_cong[cong]:
   773   "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x. P x) \<longleftrightarrow> (AE x. Q x)"
   774   by auto
   775 
   776 lemma (in measure_space) AE_all_countable:
   777   "(AE x. \<forall>i. P i x) \<longleftrightarrow> (\<forall>i::'i::countable. AE x. P i x)"
   778 proof
   779   assume "\<forall>i. AE x. P i x"
   780   from this[unfolded almost_everywhere_def Bex_def, THEN choice]
   781   obtain N where N: "\<And>i. N i \<in> null_sets" "\<And>i. {x\<in>space M. \<not> P i x} \<subseteq> N i" by auto
   782   have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. {x\<in>space M. \<not> P i x})" by auto
   783   also have "\<dots> \<subseteq> (\<Union>i. N i)" using N by auto
   784   finally have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. N i)" .
   785   moreover from N have "(\<Union>i. N i) \<in> null_sets"
   786     by (intro null_sets_UN) auto
   787   ultimately show "AE x. \<forall>i. P i x"
   788     unfolding almost_everywhere_def by auto
   789 qed auto
   790 
   791 lemma (in measure_space) AE_finite_all:
   792   assumes f: "finite S" shows "(AE x. \<forall>i\<in>S. P i x) \<longleftrightarrow> (\<forall>i\<in>S. AE x. P i x)"
   793   using f by induct auto
   794 
   795 lemma (in measure_space) restricted_measure_space:
   796   assumes "S \<in> sets M"
   797   shows "measure_space (restricted_space S)"
   798     (is "measure_space ?r")
   799   unfolding measure_space_def measure_space_axioms_def
   800 proof safe
   801   show "sigma_algebra ?r" using restricted_sigma_algebra[OF assms] .
   802   show "positive ?r (measure ?r)" using `S \<in> sets M` by (auto simp: positive_def)
   803 
   804   show "countably_additive ?r (measure ?r)"
   805     unfolding countably_additive_def
   806   proof safe
   807     fix A :: "nat \<Rightarrow> 'a set"
   808     assume *: "range A \<subseteq> sets ?r" and **: "disjoint_family A"
   809     from restriction_in_sets[OF assms *[simplified]] **
   810     show "(\<Sum>n. measure ?r (A n)) = measure ?r (\<Union>i. A i)"
   811       using measure_countably_additive by simp
   812   qed
   813 qed
   814 
   815 lemma (in measure_space) AE_restricted:
   816   assumes "A \<in> sets M"
   817   shows "(AE x in restricted_space A. P x) \<longleftrightarrow> (AE x. x \<in> A \<longrightarrow> P x)"
   818 proof -
   819   interpret R: measure_space "restricted_space A"
   820     by (rule restricted_measure_space[OF `A \<in> sets M`])
   821   show ?thesis
   822   proof
   823     assume "AE x in restricted_space A. P x"
   824     from this[THEN R.AE_E] guess N' .
   825     then obtain N where "{x \<in> A. \<not> P x} \<subseteq> A \<inter> N" "\<mu> (A \<inter> N) = 0" "N \<in> sets M"
   826       by auto
   827     moreover then have "{x \<in> space M. \<not> (x \<in> A \<longrightarrow> P x)} \<subseteq> A \<inter> N"
   828       using `A \<in> sets M` sets_into_space by auto
   829     ultimately show "AE x. x \<in> A \<longrightarrow> P x"
   830       using `A \<in> sets M` by (auto intro!: AE_I[where N="A \<inter> N"])
   831   next
   832     assume "AE x. x \<in> A \<longrightarrow> P x"
   833     from this[THEN AE_E] guess N .
   834     then show "AE x in restricted_space A. P x"
   835       using null_set_Int1[OF _ `A \<in> sets M`] `A \<in> sets M`[THEN sets_into_space]
   836       by (auto intro!: R.AE_I[where N="A \<inter> N"] simp: subset_eq)
   837   qed
   838 qed
   839 
   840 lemma (in measure_space) measure_space_subalgebra:
   841   assumes "sigma_algebra N" and "sets N \<subseteq> sets M" "space N = space M"
   842   and measure[simp]: "\<And>X. X \<in> sets N \<Longrightarrow> measure N X = measure M X"
   843   shows "measure_space N"
   844 proof -
   845   interpret N: sigma_algebra N by fact
   846   show ?thesis
   847   proof
   848     from `sets N \<subseteq> sets M` have "\<And>A. range A \<subseteq> sets N \<Longrightarrow> range A \<subseteq> sets M" by blast
   849     then show "countably_additive N (measure N)"
   850       by (auto intro!: measure_countably_additive simp: countably_additive_def subset_eq)
   851     show "positive N (measure_space.measure N)"
   852       using assms(2) by (auto simp add: positive_def)
   853   qed
   854 qed
   855 
   856 lemma (in measure_space) AE_subalgebra:
   857   assumes ae: "AE x in N. P x"
   858   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A"
   859   and sa: "sigma_algebra N"
   860   shows "AE x. P x"
   861 proof -
   862   interpret N: measure_space N using measure_space_subalgebra[OF sa N] .
   863   from ae[THEN N.AE_E] guess N .
   864   with N show ?thesis unfolding almost_everywhere_def by auto
   865 qed
   866 
   867 section "@{text \<sigma>}-finite Measures"
   868 
   869 locale sigma_finite_measure = measure_space +
   870   assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)"
   871 
   872 lemma (in sigma_finite_measure) restricted_sigma_finite_measure:
   873   assumes "S \<in> sets M"
   874   shows "sigma_finite_measure (restricted_space S)"
   875     (is "sigma_finite_measure ?r")
   876   unfolding sigma_finite_measure_def sigma_finite_measure_axioms_def
   877 proof safe
   878   show "measure_space ?r" using restricted_measure_space[OF assms] .
   879 next
   880   obtain A :: "nat \<Rightarrow> 'a set" where
   881       "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. \<mu> (A i) \<noteq> \<infinity>"
   882     using sigma_finite by auto
   883   show "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets ?r \<and> (\<Union>i. A i) = space ?r \<and> (\<forall>i. measure ?r (A i) \<noteq> \<infinity>)"
   884   proof (safe intro!: exI[of _ "\<lambda>i. A i \<inter> S"] del: notI)
   885     fix i
   886     show "A i \<inter> S \<in> sets ?r"
   887       using `range A \<subseteq> sets M` `S \<in> sets M` by auto
   888   next
   889     fix x i assume "x \<in> S" thus "x \<in> space ?r" by simp
   890   next
   891     fix x assume "x \<in> space ?r" thus "x \<in> (\<Union>i. A i \<inter> S)"
   892       using `(\<Union>i. A i) = space M` `S \<in> sets M` by auto
   893   next
   894     fix i
   895     have "\<mu> (A i \<inter> S) \<le> \<mu> (A i)"
   896       using `range A \<subseteq> sets M` `S \<in> sets M` by (auto intro!: measure_mono)
   897     then show "measure ?r (A i \<inter> S) \<noteq> \<infinity>" using `\<mu> (A i) \<noteq> \<infinity>` by auto
   898   qed
   899 qed
   900 
   901 lemma (in sigma_finite_measure) sigma_finite_measure_cong:
   902   assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> measure M' A = \<mu> A" "sets M' = sets M" "space M' = space M"
   903   shows "sigma_finite_measure M'"
   904 proof -
   905   interpret M': measure_space M' by (intro measure_space_cong cong)
   906   from sigma_finite guess A .. note A = this
   907   then have "\<And>i. A i \<in> sets M" by auto
   908   with A have fin: "\<forall>i. measure M' (A i) \<noteq> \<infinity>" using cong by auto
   909   show ?thesis
   910     apply default
   911     using A fin cong by auto
   912 qed
   913 
   914 lemma (in sigma_finite_measure) disjoint_sigma_finite:
   915   "\<exists>A::nat\<Rightarrow>'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and>
   916     (\<forall>i. \<mu> (A i) \<noteq> \<infinity>) \<and> disjoint_family A"
   917 proof -
   918   obtain A :: "nat \<Rightarrow> 'a set" where
   919     range: "range A \<subseteq> sets M" and
   920     space: "(\<Union>i. A i) = space M" and
   921     measure: "\<And>i. \<mu> (A i) \<noteq> \<infinity>"
   922     using sigma_finite by auto
   923   note range' = range_disjointed_sets[OF range] range
   924   { fix i
   925     have "\<mu> (disjointed A i) \<le> \<mu> (A i)"
   926       using range' disjointed_subset[of A i] by (auto intro!: measure_mono)
   927     then have "\<mu> (disjointed A i) \<noteq> \<infinity>"
   928       using measure[of i] by auto }
   929   with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
   930   show ?thesis by (auto intro!: exI[of _ "disjointed A"])
   931 qed
   932 
   933 lemma (in sigma_finite_measure) sigma_finite_up:
   934   "\<exists>F. range F \<subseteq> sets M \<and> incseq F \<and> (\<Union>i. F i) = space M \<and> (\<forall>i. \<mu> (F i) \<noteq> \<infinity>)"
   935 proof -
   936   obtain F :: "nat \<Rightarrow> 'a set" where
   937     F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. \<mu> (F i) \<noteq> \<infinity>"
   938     using sigma_finite by auto
   939   then show ?thesis
   940   proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
   941     from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
   942     then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
   943       using F by fastforce
   944   next
   945     fix n
   946     have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F
   947       by (auto intro!: measure_finitely_subadditive)
   948     also have "\<dots> < \<infinity>"
   949       using F by (auto simp: setsum_Pinfty)
   950     finally show "\<mu> (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp
   951   qed (force simp: incseq_def)+
   952 qed
   953 
   954 section {* Measure preserving *}
   955 
   956 definition "measure_preserving A B =
   957     {f \<in> measurable A B. (\<forall>y \<in> sets B. measure B y = measure A (f -` y \<inter> space A))}"
   958 
   959 lemma measure_preservingI[intro?]:
   960   assumes "f \<in> measurable A B"
   961     and "\<And>y. y \<in> sets B \<Longrightarrow> measure A (f -` y \<inter> space A) = measure B y"
   962   shows "f \<in> measure_preserving A B"
   963   unfolding measure_preserving_def using assms by auto
   964 
   965 lemma (in measure_space) measure_space_vimage:
   966   fixes M' :: "('c, 'd) measure_space_scheme"
   967   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
   968   shows "measure_space M'"
   969 proof -
   970   interpret M': sigma_algebra M' by fact
   971   show ?thesis
   972   proof
   973     show "positive M' (measure M')" using T
   974       by (auto simp: measure_preserving_def positive_def measurable_sets)
   975 
   976     show "countably_additive M' (measure M')"
   977     proof (intro countably_additiveI)
   978       fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
   979       then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
   980       then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
   981         using T by (auto simp: measurable_def measure_preserving_def)
   982       moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
   983         using * by blast
   984       moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
   985         using `disjoint_family A` by (auto simp: disjoint_family_on_def)
   986       ultimately show "(\<Sum>i. measure M' (A i)) = measure M' (\<Union>i. A i)"
   987         using measure_countably_additive[OF _ **] A T
   988         by (auto simp: comp_def vimage_UN measure_preserving_def)
   989     qed
   990   qed
   991 qed
   992 
   993 lemma (in measure_space) almost_everywhere_vimage:
   994   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
   995     and AE: "measure_space.almost_everywhere M' P"
   996   shows "AE x. P (T x)"
   997 proof -
   998   interpret M': measure_space M' using T by (rule measure_space_vimage)
   999   from AE[THEN M'.AE_E] guess N .
  1000   then show ?thesis
  1001     unfolding almost_everywhere_def M'.almost_everywhere_def
  1002     using T(2) unfolding measurable_def measure_preserving_def
  1003     by (intro bexI[of _ "T -` N \<inter> space M"]) auto
  1004 qed
  1005 
  1006 lemma measure_unique_Int_stable_vimage:
  1007   fixes A :: "nat \<Rightarrow> 'a set"
  1008   assumes E: "Int_stable E"
  1009   and A: "range A \<subseteq> sets E" "incseq A" "(\<Union>i. A i) = space E" "\<And>i. measure M (A i) \<noteq> \<infinity>"
  1010   and N: "measure_space N" "T \<in> measurable N M"
  1011   and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
  1012   and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
  1013   assumes X: "X \<in> sets (sigma E)"
  1014   shows "measure M X = measure N (T -` X \<inter> space N)"
  1015 proof (rule measure_unique_Int_stable[OF E A(1,2,3) _ _ eq _ X])
  1016   interpret M: measure_space M by fact
  1017   interpret N: measure_space N by fact
  1018   let ?T = "\<lambda>X. T -` X \<inter> space N"
  1019   show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
  1020     by (rule M.measure_space_cong) (auto simp: M)
  1021   show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
  1022   proof (rule N.measure_space_vimage)
  1023     show "sigma_algebra ?E"
  1024       by (rule M.sigma_algebra_cong) (auto simp: M)
  1025     show "T \<in> measure_preserving N ?E"
  1026       using `T \<in> measurable N M` by (auto simp: M measurable_def measure_preserving_def)
  1027   qed
  1028   show "\<And>i. M.\<mu> (A i) \<noteq> \<infinity>" by fact
  1029 qed
  1030 
  1031 lemma (in measure_space) measure_preserving_Int_stable:
  1032   fixes A :: "nat \<Rightarrow> 'a set"
  1033   assumes E: "Int_stable E" "range A \<subseteq> sets E" "incseq A" "(\<Union>i. A i) = space E" "\<And>i. measure E (A i) \<noteq> \<infinity>"
  1034   and N: "measure_space (sigma E)"
  1035   and T: "T \<in> measure_preserving M E"
  1036   shows "T \<in> measure_preserving M (sigma E)"
  1037 proof
  1038   interpret E: measure_space "sigma E" by fact
  1039   show "T \<in> measurable M (sigma E)"
  1040     using T E.sets_into_space
  1041     by (intro measurable_sigma) (auto simp: measure_preserving_def measurable_def)
  1042   fix X assume "X \<in> sets (sigma E)"
  1043   show "\<mu> (T -` X \<inter> space M) = E.\<mu> X"
  1044   proof (rule measure_unique_Int_stable_vimage[symmetric])
  1045     show "sets (sigma E) = sets (sigma E)" "space E = space (sigma E)"
  1046       "\<And>i. E.\<mu> (A i) \<noteq> \<infinity>" using E by auto
  1047     show "measure_space M" by default
  1048   next
  1049     fix X assume "X \<in> sets E" then show "E.\<mu> X = \<mu> (T -` X \<inter> space M)"
  1050       using T unfolding measure_preserving_def by auto
  1051   qed fact+
  1052 qed
  1053 
  1054 section "Real measure values"
  1055 
  1056 lemma (in measure_space) real_measure_Union:
  1057   assumes finite: "\<mu> A \<noteq> \<infinity>" "\<mu> B \<noteq> \<infinity>"
  1058   and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}"
  1059   shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)"
  1060   unfolding measure_additive[symmetric, OF measurable]
  1061   using measurable(1,2)[THEN positive_measure]
  1062   using finite by (cases rule: ereal2_cases[of "\<mu> A" "\<mu> B"]) auto
  1063 
  1064 lemma (in measure_space) real_measure_finite_Union:
  1065   assumes measurable:
  1066     "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M" "disjoint_family_on A S"
  1067   assumes finite: "\<And>i. i \<in> S \<Longrightarrow> \<mu> (A i) \<noteq> \<infinity>"
  1068   shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
  1069   using finite measurable(2)[THEN positive_measure]
  1070   by (force intro!: setsum_real_of_ereal[symmetric]
  1071             simp: measure_setsum[OF measurable, symmetric])
  1072 
  1073 lemma (in measure_space) real_measure_Diff:
  1074   assumes finite: "\<mu> A \<noteq> \<infinity>"
  1075   and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
  1076   shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)"
  1077 proof -
  1078   have "\<mu> (A - B) \<le> \<mu> A" "\<mu> B \<le> \<mu> A"
  1079     using measurable by (auto intro!: measure_mono)
  1080   hence "real (\<mu> ((A - B) \<union> B)) = real (\<mu> (A - B)) + real (\<mu> B)"
  1081     using measurable finite by (rule_tac real_measure_Union) auto
  1082   thus ?thesis using `B \<subseteq> A` by (auto simp: Un_absorb2)
  1083 qed
  1084 
  1085 lemma (in measure_space) real_measure_UNION:
  1086   assumes measurable: "range A \<subseteq> sets M" "disjoint_family A"
  1087   assumes finite: "\<mu> (\<Union>i. A i) \<noteq> \<infinity>"
  1088   shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))"
  1089 proof -
  1090   have "\<And>i. 0 \<le> \<mu> (A i)" using measurable by auto
  1091   with summable_sums[OF summable_ereal_pos, of "\<lambda>i. \<mu> (A i)"]
  1092      measure_countably_additive[OF measurable]
  1093   have "(\<lambda>i. \<mu> (A i)) sums (\<mu> (\<Union>i. A i))" by simp
  1094   moreover
  1095   { fix i
  1096     have "\<mu> (A i) \<le> \<mu> (\<Union>i. A i)"
  1097       using measurable by (auto intro!: measure_mono)
  1098     moreover have "0 \<le> \<mu> (A i)" using measurable by auto
  1099     ultimately have "\<mu> (A i) = ereal (real (\<mu> (A i)))"
  1100       using finite by (cases "\<mu> (A i)") auto }
  1101   moreover
  1102   have "0 \<le> \<mu> (\<Union>i. A i)" using measurable by auto
  1103   then have "\<mu> (\<Union>i. A i) = ereal (real (\<mu> (\<Union>i. A i)))"
  1104     using finite by (cases "\<mu> (\<Union>i. A i)") auto
  1105   ultimately show ?thesis
  1106     unfolding sums_ereal[symmetric] by simp
  1107 qed
  1108 
  1109 lemma (in measure_space) real_measure_subadditive:
  1110   assumes measurable: "A \<in> sets M" "B \<in> sets M"
  1111   and fin: "\<mu> A \<noteq> \<infinity>" "\<mu> B \<noteq> \<infinity>"
  1112   shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)"
  1113 proof -
  1114   have "0 \<le> \<mu> (A \<union> B)" using measurable by auto
  1115   then show "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)"
  1116     using measure_subadditive[OF measurable] fin
  1117     by (cases rule: ereal3_cases[of "\<mu> (A \<union> B)" "\<mu> A" "\<mu> B"]) auto
  1118 qed
  1119 
  1120 lemma (in measure_space) real_measure_setsum_singleton:
  1121   assumes S: "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  1122   and fin: "\<And>x. x \<in> S \<Longrightarrow> \<mu> {x} \<noteq> \<infinity>"
  1123   shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))"
  1124   using measure_finite_singleton[OF S] fin
  1125   using positive_measure[OF S(2)]
  1126   by (force intro!: setsum_real_of_ereal[symmetric])
  1127 
  1128 lemma (in measure_space) real_continuity_from_below:
  1129   assumes A: "range A \<subseteq> sets M" "incseq A" and fin: "\<mu> (\<Union>i. A i) \<noteq> \<infinity>"
  1130   shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))"
  1131 proof -
  1132   have "0 \<le> \<mu> (\<Union>i. A i)" using A by auto
  1133   then have "ereal (real (\<mu> (\<Union>i. A i))) = \<mu> (\<Union>i. A i)"
  1134     using fin by (auto intro: ereal_real')
  1135   then show ?thesis
  1136     using continuity_from_below_Lim[OF A]
  1137     by (intro lim_real_of_ereal) simp
  1138 qed
  1139 
  1140 lemma (in measure_space) continuity_from_above_Lim:
  1141   assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. \<mu> (A i) \<noteq> \<infinity>"
  1142   shows "(\<lambda>i. (\<mu> (A i))) ----> \<mu> (\<Inter>i. A i)"
  1143   using LIMSEQ_ereal_INFI[OF measure_decseq, OF A]
  1144   using continuity_from_above[OF A fin] by simp
  1145 
  1146 lemma (in measure_space) real_continuity_from_above:
  1147   assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. \<mu> (A i) \<noteq> \<infinity>"
  1148   shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))"
  1149 proof -
  1150   have "0 \<le> \<mu> (\<Inter>i. A i)" using A by auto
  1151   moreover
  1152   have "\<mu> (\<Inter>i. A i) \<le> \<mu> (A 0)"
  1153     using A by (auto intro!: measure_mono)
  1154   ultimately have "ereal (real (\<mu> (\<Inter>i. A i))) = \<mu> (\<Inter>i. A i)"
  1155     using fin by (auto intro: ereal_real')
  1156   then show ?thesis
  1157     using continuity_from_above_Lim[OF A fin]
  1158     by (intro lim_real_of_ereal) simp
  1159 qed
  1160 
  1161 lemma (in measure_space) real_measure_countably_subadditive:
  1162   assumes A: "range A \<subseteq> sets M" and fin: "(\<Sum>i. \<mu> (A i)) \<noteq> \<infinity>"
  1163   shows "real (\<mu> (\<Union>i. A i)) \<le> (\<Sum>i. real (\<mu> (A i)))"
  1164 proof -
  1165   { fix i
  1166     have "0 \<le> \<mu> (A i)" using A by auto
  1167     moreover have "\<mu> (A i) \<noteq> \<infinity>" using A by (intro suminf_PInfty[OF _ fin]) auto
  1168     ultimately have "\<bar>\<mu> (A i)\<bar> \<noteq> \<infinity>" by auto }
  1169   moreover have "0 \<le> \<mu> (\<Union>i. A i)" using A by auto
  1170   ultimately have "ereal (real (\<mu> (\<Union>i. A i))) \<le> (\<Sum>i. ereal (real (\<mu> (A i))))"
  1171     using measure_countably_subadditive[OF A] by (auto simp: ereal_real)
  1172   also have "\<dots> = ereal (\<Sum>i. real (\<mu> (A i)))"
  1173     using A
  1174     by (auto intro!: sums_unique[symmetric] sums_ereal[THEN iffD2] summable_sums summable_real_of_ereal fin)
  1175   finally show ?thesis by simp
  1176 qed
  1177 
  1178 locale finite_measure = sigma_finite_measure +
  1179   assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<infinity>"
  1180 
  1181 lemma finite_measureI[Pure.intro!]:
  1182   assumes "measure_space M"
  1183   assumes *: "measure M (space M) \<noteq> \<infinity>"
  1184   shows "finite_measure M"
  1185 proof -
  1186   interpret measure_space M by fact
  1187   show "finite_measure M"
  1188   proof
  1189     show "measure M (space M) \<noteq> \<infinity>" by fact
  1190     show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)"
  1191       using * by (auto intro!: exI[of _ "\<lambda>x. space M"])
  1192   qed
  1193 qed
  1194 
  1195 lemma (in finite_measure) finite_measure[simp, intro]:
  1196   assumes "A \<in> sets M"
  1197   shows "\<mu> A \<noteq> \<infinity>"
  1198 proof -
  1199   from `A \<in> sets M` have "A \<subseteq> space M"
  1200     using sets_into_space by blast
  1201   then have "\<mu> A \<le> \<mu> (space M)"
  1202     using assms top by (rule measure_mono)
  1203   then show ?thesis
  1204     using finite_measure_of_space by auto
  1205 qed
  1206 
  1207 definition (in finite_measure)
  1208   "\<mu>' A = (if A \<in> sets M then real (\<mu> A) else 0)"
  1209 
  1210 lemma (in finite_measure) finite_measure_eq: "A \<in> sets M \<Longrightarrow> \<mu> A = ereal (\<mu>' A)"
  1211   by (auto simp: \<mu>'_def ereal_real)
  1212 
  1213 lemma (in finite_measure) positive_measure'[simp, intro]: "0 \<le> \<mu>' A"
  1214   unfolding \<mu>'_def by (auto simp: real_of_ereal_pos)
  1215 
  1216 lemma (in finite_measure) real_measure:
  1217   assumes A: "A \<in> sets M" shows "\<exists>r. 0 \<le> r \<and> \<mu> A = ereal r"
  1218   using finite_measure[OF A] positive_measure[OF A] by (cases "\<mu> A") auto
  1219 
  1220 lemma (in finite_measure) bounded_measure: "\<mu>' A \<le> \<mu>' (space M)"
  1221 proof cases
  1222   assume "A \<in> sets M"
  1223   moreover then have "\<mu> A \<le> \<mu> (space M)"
  1224     using sets_into_space by (auto intro!: measure_mono)
  1225   ultimately show ?thesis
  1226     by (auto simp: \<mu>'_def intro!: real_of_ereal_positive_mono)
  1227 qed (simp add: \<mu>'_def real_of_ereal_pos)
  1228 
  1229 lemma (in finite_measure) restricted_finite_measure:
  1230   assumes "S \<in> sets M"
  1231   shows "finite_measure (restricted_space S)"
  1232     (is "finite_measure ?r")
  1233 proof
  1234   show "measure_space ?r" using restricted_measure_space[OF assms] .
  1235   show "measure ?r (space ?r) \<noteq> \<infinity>" using finite_measure[OF `S \<in> sets M`] by auto
  1236 qed
  1237 
  1238 lemma (in measure_space) restricted_to_finite_measure:
  1239   assumes "S \<in> sets M" "\<mu> S \<noteq> \<infinity>"
  1240   shows "finite_measure (restricted_space S)"
  1241 proof
  1242   show "measure_space (restricted_space S)"
  1243     using `S \<in> sets M` by (rule restricted_measure_space)
  1244   show "measure (restricted_space S) (space (restricted_space S)) \<noteq> \<infinity>"
  1245     by simp fact
  1246 qed
  1247 
  1248 lemma (in finite_measure) finite_measure_Diff:
  1249   assumes sets: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
  1250   shows "\<mu>' (A - B) = \<mu>' A - \<mu>' B"
  1251   using sets[THEN finite_measure_eq]
  1252   using Diff[OF sets, THEN finite_measure_eq]
  1253   using measure_Diff[OF _ assms] by simp
  1254 
  1255 lemma (in finite_measure) finite_measure_Union:
  1256   assumes sets: "A \<in> sets M" "B \<in> sets M" and "A \<inter> B = {}"
  1257   shows "\<mu>' (A \<union> B) = \<mu>' A + \<mu>' B"
  1258   using measure_additive[OF assms]
  1259   using sets[THEN finite_measure_eq]
  1260   using Un[OF sets, THEN finite_measure_eq]
  1261   by simp
  1262 
  1263 lemma (in finite_measure) finite_measure_finite_Union:
  1264   assumes S: "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M"
  1265   and dis: "disjoint_family_on A S"
  1266   shows "\<mu>' (\<Union>i\<in>S. A i) = (\<Sum>i\<in>S. \<mu>' (A i))"
  1267   using measure_setsum[OF assms]
  1268   using finite_UN[of S A, OF S, THEN finite_measure_eq]
  1269   using S(2)[THEN finite_measure_eq]
  1270   by simp
  1271 
  1272 lemma (in finite_measure) finite_measure_UNION:
  1273   assumes A: "range A \<subseteq> sets M" "disjoint_family A"
  1274   shows "(\<lambda>i. \<mu>' (A i)) sums (\<mu>' (\<Union>i. A i))"
  1275   using real_measure_UNION[OF A]
  1276   using countable_UN[OF A(1), THEN finite_measure_eq]
  1277   using A(1)[THEN subsetD, THEN finite_measure_eq]
  1278   by auto
  1279 
  1280 lemma (in finite_measure) finite_measure_mono:
  1281   assumes B: "B \<in> sets M" and "A \<subseteq> B" shows "\<mu>' A \<le> \<mu>' B"
  1282 proof cases
  1283   assume "A \<in> sets M"
  1284   from this[THEN finite_measure_eq] B[THEN finite_measure_eq]
  1285   show ?thesis using measure_mono[OF `A \<subseteq> B` `A \<in> sets M` `B \<in> sets M`] by simp
  1286 next
  1287   assume "A \<notin> sets M" then show ?thesis
  1288     using positive_measure'[of B] unfolding \<mu>'_def by auto
  1289 qed
  1290 
  1291 lemma (in finite_measure) finite_measure_subadditive:
  1292   assumes m: "A \<in> sets M" "B \<in> sets M"
  1293   shows "\<mu>' (A \<union> B) \<le> \<mu>' A + \<mu>' B"
  1294   using measure_subadditive[OF m]
  1295   using m[THEN finite_measure_eq] Un[OF m, THEN finite_measure_eq] by simp
  1296 
  1297 lemma (in finite_measure) finite_measure_subadditive_finite:
  1298   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
  1299   shows "\<mu>' (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu>' (A i))"
  1300   using measure_subadditive_finite[OF assms] assms
  1301   by (simp add: finite_measure_eq finite_UN)
  1302 
  1303 lemma (in finite_measure) finite_measure_countably_subadditive:
  1304   assumes A: "range A \<subseteq> sets M" and sum: "summable (\<lambda>i. \<mu>' (A i))"
  1305   shows "\<mu>' (\<Union>i. A i) \<le> (\<Sum>i. \<mu>' (A i))"
  1306 proof -
  1307   note A[THEN subsetD, THEN finite_measure_eq, simp]
  1308   note countable_UN[OF A, THEN finite_measure_eq, simp]
  1309   from `summable (\<lambda>i. \<mu>' (A i))`
  1310   have "(\<lambda>i. ereal (\<mu>' (A i))) sums ereal (\<Sum>i. \<mu>' (A i))"
  1311     by (simp add: sums_ereal) (rule summable_sums)
  1312   from sums_unique[OF this, symmetric]
  1313        measure_countably_subadditive[OF A]
  1314   show ?thesis by simp
  1315 qed
  1316 
  1317 lemma (in finite_measure) finite_measure_finite_singleton:
  1318   assumes "finite S" and *: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  1319   shows "\<mu>' S = (\<Sum>x\<in>S. \<mu>' {x})"
  1320   using real_measure_setsum_singleton[OF assms]
  1321   using *[THEN finite_measure_eq]
  1322   using finite_UN[of S "\<lambda>x. {x}", OF assms, THEN finite_measure_eq]
  1323   by simp
  1324 
  1325 lemma (in finite_measure) finite_continuity_from_below:
  1326   assumes A: "range A \<subseteq> sets M" and "incseq A"
  1327   shows "(\<lambda>i. \<mu>' (A i)) ----> \<mu>' (\<Union>i. A i)"
  1328   using real_continuity_from_below[OF A, OF `incseq A` finite_measure] assms
  1329   using A[THEN subsetD, THEN finite_measure_eq]
  1330   using countable_UN[OF A, THEN finite_measure_eq]
  1331   by auto
  1332 
  1333 lemma (in finite_measure) finite_continuity_from_above:
  1334   assumes A: "range A \<subseteq> sets M" and "decseq A"
  1335   shows "(\<lambda>n. \<mu>' (A n)) ----> \<mu>' (\<Inter>i. A i)"
  1336   using real_continuity_from_above[OF A, OF `decseq A` finite_measure] assms
  1337   using A[THEN subsetD, THEN finite_measure_eq]
  1338   using countable_INT[OF A, THEN finite_measure_eq]
  1339   by auto
  1340 
  1341 lemma (in finite_measure) finite_measure_compl:
  1342   assumes S: "S \<in> sets M"
  1343   shows "\<mu>' (space M - S) = \<mu>' (space M) - \<mu>' S"
  1344   using measure_compl[OF S, OF finite_measure, OF S]
  1345   using S[THEN finite_measure_eq]
  1346   using compl_sets[OF S, THEN finite_measure_eq]
  1347   using top[THEN finite_measure_eq]
  1348   by simp
  1349 
  1350 lemma (in finite_measure) finite_measure_inter_full_set:
  1351   assumes S: "S \<in> sets M" "T \<in> sets M"
  1352   assumes T: "\<mu>' T = \<mu>' (space M)"
  1353   shows "\<mu>' (S \<inter> T) = \<mu>' S"
  1354   using measure_inter_full_set[OF S finite_measure]
  1355   using T Diff[OF S(2,1)] Diff[OF S, THEN finite_measure_eq]
  1356   using Int[OF S, THEN finite_measure_eq]
  1357   using S[THEN finite_measure_eq] top[THEN finite_measure_eq]
  1358   by simp
  1359 
  1360 lemma (in finite_measure) empty_measure'[simp]: "\<mu>' {} = 0"
  1361   unfolding \<mu>'_def by simp
  1362 
  1363 section "Finite spaces"
  1364 
  1365 locale finite_measure_space = finite_measure + finite_sigma_algebra
  1366 
  1367 lemma finite_measure_spaceI[Pure.intro!]:
  1368   assumes "finite (space M)"
  1369   assumes sets_Pow: "sets M = Pow (space M)"
  1370     and space: "measure M (space M) \<noteq> \<infinity>"
  1371     and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}"
  1372     and add: "\<And>A. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})"
  1373   shows "finite_measure_space M"
  1374 proof -
  1375   interpret finite_sigma_algebra M
  1376   proof
  1377     show "finite (space M)" by fact
  1378   qed (auto simp: sets_Pow)
  1379   interpret measure_space M
  1380   proof (rule finite_additivity_sufficient)
  1381     show "sigma_algebra M" by default
  1382     show "finite (space M)" by fact
  1383     show "positive M (measure M)"
  1384       by (auto simp: add positive_def intro!: setsum_nonneg pos)
  1385     show "additive M (measure M)"
  1386       using `finite (space M)`
  1387       by (auto simp add: additive_def add
  1388                intro!: setsum_Un_disjoint dest: finite_subset)
  1389   qed
  1390   interpret finite_measure M
  1391   proof
  1392     show "\<mu> (space M) \<noteq> \<infinity>" by fact
  1393   qed default
  1394   show "finite_measure_space M" 
  1395     by default
  1396 qed
  1397 
  1398 lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
  1399   using measure_setsum[of "space M" "\<lambda>i. {i}"]
  1400   by (simp add: disjoint_family_on_def finite_space)
  1401 
  1402 lemma (in finite_measure_space) finite_measure_singleton:
  1403   assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
  1404   using A finite_subset[OF A finite_space]
  1405   by (intro finite_measure_finite_singleton) auto
  1406 
  1407 lemma (in finite_measure_space) finite_measure_subadditive_setsum:
  1408   assumes "finite I"
  1409   shows "\<mu>' (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu>' (A i))"
  1410 proof cases
  1411   assume "(\<Union>i\<in>I. A i) \<subseteq> space M"
  1412   then have "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M" by auto
  1413   from finite_measure_subadditive_finite[OF `finite I` this]
  1414   show ?thesis by auto
  1415 next
  1416   assume "\<not> (\<Union>i\<in>I. A i) \<subseteq> space M"
  1417   then have "\<mu>' (\<Union>i\<in>I. A i) = 0"
  1418     by (simp add: \<mu>'_def)
  1419   also have "0 \<le> (\<Sum>i\<in>I. \<mu>' (A i))"
  1420     by (auto intro!: setsum_nonneg)
  1421   finally show ?thesis .
  1422 qed
  1423 
  1424 lemma suminf_cmult_indicator:
  1425   fixes f :: "nat \<Rightarrow> ereal"
  1426   assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
  1427   shows "(\<Sum>n. f n * indicator (A n) x) = f i"
  1428 proof -
  1429   have **: "\<And>n. f n * indicator (A n) x = (if n = i then f n else 0 :: ereal)"
  1430     using `x \<in> A i` assms unfolding disjoint_family_on_def indicator_def by auto
  1431   then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
  1432     by (auto simp: setsum_cases)
  1433   moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
  1434   proof (rule ereal_SUPI)
  1435     fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
  1436     from this[of "Suc i"] show "f i \<le> y" by auto
  1437   qed (insert assms, simp)
  1438   ultimately show ?thesis using assms
  1439     by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def)
  1440 qed
  1441 
  1442 lemma suminf_indicator:
  1443   assumes "disjoint_family A"
  1444   shows "(\<Sum>n. indicator (A n) x :: ereal) = indicator (\<Union>i. A i) x"
  1445 proof cases
  1446   assume *: "x \<in> (\<Union>i. A i)"
  1447   then obtain i where "x \<in> A i" by auto
  1448   from suminf_cmult_indicator[OF assms(1), OF `x \<in> A i`, of "\<lambda>k. 1"]
  1449   show ?thesis using * by simp
  1450 qed simp
  1451 
  1452 end