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