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