src/HOL/Probability/Measure_Space.thy

   from plus_emeasure[OF sets this] show ?thesis by simp
 qed
 
 lemma emeasure_insert_ne:
   "A \<noteq> {} \<Longrightarrow> {x} \<in> sets M \<Longrightarrow> A \<in> sets M \<Longrightarrow> x \<notin> A \<Longrightarrow> emeasure M (insert x A) = emeasure M {x} + emeasure M A"
-  by (rule emeasure_insert) 
+  by (rule emeasure_insert)
 
 lemma emeasure_eq_setsum_singleton:
   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
   shows "emeasure M S = (\<Sum>x\<in>S. emeasure M {x})"
   using setsum_emeasure[of "\<lambda>x. {x}" S M] assms

     using null_sets by auto
   with sets * show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
     by (auto intro!: antisym)
 qed
 
-lemma UN_from_nat_into: 
+lemma UN_from_nat_into:
   assumes I: "countable I" "I \<noteq> {}"
   shows "(\<Union>i\<in>I. N i) = (\<Union>i. N (from_nat_into I i))"
 proof -
   have "(\<Union>i\<in>I. N i) = \<Union>(N ` range (from_nat_into I))"
     using I by simp

     by (intro null_sets_UN) auto
   ultimately show "AE x in M. \<forall>i. P i x"
     unfolding eventually_ae_filter by auto
 qed auto
 
-lemma AE_ball_countable: 
+lemma AE_ball_countable:
   assumes [intro]: "countable X"
   shows "(AE x in M. \<forall>y\<in>X. P x y) \<longleftrightarrow> (\<forall>y\<in>X. AE x in M. P x y)"
 proof
   assume "\<forall>y\<in>X. AE x in M. P x y"
   from this[unfolded eventually_ae_filter Bex_def, THEN bchoice]

     unfolding eventually_ae_filter by auto
 qed auto
 
 lemma AE_discrete_difference:
   assumes X: "countable X"
-  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
+  assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
   assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   shows "AE x in M. x \<notin> X"
 proof -
   have "(\<Union>x\<in>X. {x}) \<in> null_sets M"
     using assms by (intro null_sets_UN') auto

   show thesis
   proof cases
     assume "A = {}" with `(\<Union>A) = space M` show thesis
       by (intro that[of "\<lambda>_. {}"]) auto
   next
-    assume "A \<noteq> {}" 
+    assume "A \<noteq> {}"
     show thesis
     proof
       show "range (from_nat_into A) \<subseteq> sets M"
         using `A \<noteq> {}` A by auto
       have "(\<Union>i. from_nat_into A i) = \<Union>A"

 lemma measure_distr:
   "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
   by (simp add: emeasure_distr measure_def)
 
 lemma distr_cong_AE:
-  assumes 1: "M = K" "sets N = sets L" and 
+  assumes 1: "M = K" "sets N = sets L" and
     2: "(AE x in M. f x = g x)" and "f \<in> measurable M N" and "g \<in> measurable K L"
   shows "distr M N f = distr K L g"
 proof (rule measure_eqI)
   fix A assume "A \<in> sets (distr M N f)"
   with assms show "emeasure (distr M N f) A = emeasure (distr K L g) A"

   have prob_some: "\<And> x. x \<in> s \<Longrightarrow> measure M {x} = measure M {SOME y. y \<in> s}" by blast
   have "measure M s = (\<Sum> x \<in> s. measure M {x})"
     using finite_measure_eq_setsum_singleton[OF s] by simp
   also have "\<dots> = (\<Sum> x \<in> s. measure M {SOME y. y \<in> s})" using prob_some by auto
   also have "\<dots> = real (card s) * measure M {(SOME x. x \<in> s)}"
-    using setsum_constant assms by (simp add: real_eq_of_nat)
+    using setsum_constant assms by simp
   finally show ?thesis by simp
 qed simp
 
 lemma (in finite_measure) measure_real_sum_image_fn:
   assumes "e \<in> sets M"

   assumes "A \<in> sets M" "B \<in> sets M"
   assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
   shows "measure M B = 0"
   using measure_space_inter[of B A] assms by (auto simp: ac_simps)
 lemma (in finite_measure) finite_measure_distr:
-  assumes f: "f \<in> measurable M M'" 
+  assumes f: "f \<in> measurable M M'"
   shows "finite_measure (distr M M' f)"
 proof (rule finite_measureI)
   have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
   with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
 qed

   have additive: "additive (Pow A) ?M"
     by (auto simp: card_Un_disjoint additive_def)
 
   interpret ring_of_sets A "Pow A"
     by (rule ring_of_setsI) auto
-  show "countably_additive (Pow A) ?M" 
+  show "countably_additive (Pow A) ?M"
     unfolding countably_additive_iff_continuous_from_below[OF positive additive]
   proof safe
     fix F :: "nat \<Rightarrow> 'a set" assume "incseq F"
     show "(\<lambda>i. ?M (F i)) ----> ?M (\<Union>i. F i)"
     proof cases

         by (rule range_inj_infinite)
       have "infinite (Pow (\<Union>i. F i))"
         by (rule infinite_super[OF _ 1]) auto
       then have "infinite (\<Union>i. F i)"
         by auto
-      
+
       ultimately show ?thesis by auto
     qed
   qed
 qed
 

   with assms show ?thesis
     unfolding eventually_ae_filter
     by (auto simp add: space_restrict_space null_sets_def sets_restrict_space_iff
                        emeasure_restrict_space cong: conj_cong
              intro!: ex_cong[where f="\<lambda>X. (\<Omega> \<inter> space M) \<inter> X"])
-qed  
+qed
 
 lemma restrict_restrict_space:
   assumes "A \<inter> space M \<in> sets M" "B \<inter> space M \<in> sets M"
   shows "restrict_space (restrict_space M A) B = restrict_space M (A \<inter> B)" (is "?l = ?r")
 proof (rule measure_eqI[symmetric])

   interpret finite_measure M by fact
   show ?thesis
     by(rule finite_measureI)(simp add: emeasure_restrict_space A space_restrict_space)
 qed
 
-lemma restrict_distr: 
+lemma restrict_distr:
   assumes [measurable]: "f \<in> measurable M N"
   assumes [simp]: "\<Omega> \<inter> space N \<in> sets N" and restrict: "f \<in> space M \<rightarrow> \<Omega>"
   shows "restrict_space (distr M N f) \<Omega> = distr M (restrict_space N \<Omega>) f"
   (is "?l = ?r")
 proof (rule measure_eqI)

 
 lemma measure_eqI_restrict_generator:
   assumes E: "Int_stable E" "E \<subseteq> Pow \<Omega>" "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X"
   assumes sets_eq: "sets M = sets N" and \<Omega>: "\<Omega> \<in> sets M"
   assumes "sets (restrict_space M \<Omega>) = sigma_sets \<Omega> E"
-  assumes "sets (restrict_space N \<Omega>) = sigma_sets \<Omega> E" 
+  assumes "sets (restrict_space N \<Omega>) = sigma_sets \<Omega> E"
   assumes ae: "AE x in M. x \<in> \<Omega>" "AE x in N. x \<in> \<Omega>"
   assumes A: "countable A" "A \<noteq> {}" "A \<subseteq> E" "\<Union>A = \<Omega>" "\<And>a. a \<in> A \<Longrightarrow> emeasure M a \<noteq> \<infinity>"
   shows "M = N"
 proof (rule measure_eqI)
   fix X assume X: "X \<in> sets M"

 definition "null_measure M = sigma (space M) (sets M)"
 
 lemma space_null_measure[simp]: "space (null_measure M) = space M"
   by (simp add: null_measure_def)
 
-lemma sets_null_measure[simp, measurable_cong]: "sets (null_measure M) = sets M" 
+lemma sets_null_measure[simp, measurable_cong]: "sets (null_measure M) = sets M"
   by (simp add: null_measure_def)
 
 lemma emeasure_null_measure[simp]: "emeasure (null_measure M) X = 0"
   by (cases "X \<in> sets M", rule emeasure_measure_of)
      (auto simp: positive_def countably_additive_def emeasure_notin_sets null_measure_def

   shows space_Sup: "space (Sup A) = space a"
     and sets_Sup: "sets (Sup A) = sets a"
 proof -
   have sets: "(SUP a:A. sets a) = sets a"
   proof (intro antisym SUP_least)
-    fix a' show "a' \<in> A \<Longrightarrow> sets a' \<subseteq> sets a" 
+    fix a' show "a' \<in> A \<Longrightarrow> sets a' \<subseteq> sets a"
       using a chainD[OF A, of a a'] by (auto elim!: less_eq_measure.cases)
   qed (insert \<open>a\<in>A\<close>, auto)
   have space: "(SUP a:A. space a) = space a"
   proof (intro antisym SUP_least)
-    fix a' show "a' \<in> A \<Longrightarrow> space a' \<subseteq> space a" 
+    fix a' show "a' \<in> A \<Longrightarrow> space a' \<subseteq> space a"
       using a chainD[OF A, of a a'] by (intro sets_le_imp_space_le) (auto elim!: less_eq_measure.cases)
   qed (insert \<open>a\<in>A\<close>, auto)
   show "space (Sup A) = space a"
     unfolding Sup_measure_def sets space sets.space_measure_of_eq ..
   show "sets (Sup A) = sets a"