src/HOL/Probability/Complete_Measure.thy
 changeset 40871 688f6ff859e1 parent 40859 de0b30e6c2d2 child 41023 9118eb4eb8dc
```     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Wed Dec 01 20:12:53 2010 +0100
1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Wed Dec 01 21:03:02 2010 +0100
1.3 @@ -189,56 +189,13 @@
1.4    qed
1.5  qed
1.6
1.7 -lemma (in sigma_algebra) simple_functionD':
1.8 -  assumes "simple_function f"
1.9 -  shows "f -` {x} \<inter> space M \<in> sets M"
1.10 -proof cases
1.11 -  assume "x \<in> f`space M" from simple_functionD(2)[OF assms this] show ?thesis .
1.12 -next
1.13 -  assume "x \<notin> f`space M" then have "f -` {x} \<inter> space M = {}" by auto
1.14 -  then show ?thesis by auto
1.15 -qed
1.16 -
1.17 -lemma (in sigma_algebra) simple_function_If:
1.18 -  assumes sf: "simple_function f" "simple_function g" and A: "A \<in> sets M"
1.19 -  shows "simple_function (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function ?IF")
1.20 -proof -
1.21 -  def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
1.22 -  show ?thesis unfolding simple_function_def
1.23 -  proof safe
1.24 -    have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
1.25 -    from finite_subset[OF this] assms
1.26 -    show "finite (?IF ` space M)" unfolding simple_function_def by auto
1.27 -  next
1.28 -    fix x assume "x \<in> space M"
1.29 -    then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
1.30 -      then ((F (f x) \<inter> A) \<union> (G (f x) - (G (f x) \<inter> A)))
1.31 -      else ((F (g x) \<inter> A) \<union> (G (g x) - (G (g x) \<inter> A))))"
1.32 -      using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
1.33 -    have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
1.34 -      unfolding F_def G_def using sf[THEN simple_functionD'] by auto
1.35 -    show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
1.36 -  qed
1.37 -qed
1.38 -
1.39 -lemma (in measure_space) null_sets_finite_UN:
1.40 -  assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
1.41 -  shows "(\<Union>i\<in>S. A i) \<in> null_sets"
1.42 -proof (intro CollectI conjI)
1.43 -  show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
1.44 -  have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
1.45 -    using assms by (intro measure_finitely_subadditive) auto
1.46 -  then show "\<mu> (\<Union>i\<in>S. A i) = 0"
1.47 -    using assms by auto
1.48 -qed
1.49 -
1.50  lemma (in completeable_measure_space) completion_ex_simple_function:
1.51    assumes f: "completion.simple_function f"
1.52    shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
1.53  proof -
1.54    let "?F x" = "f -` {x} \<inter> space M"
1.55    have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
1.56 -    using completion.simple_functionD'[OF f]
1.57 +    using completion.simple_functionD[OF f]
1.58        completion.simple_functionD[OF f] by simp_all
1.59    have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
1.60      using F null_part by auto
```