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