src/HOL/Probability/Measure_Space.thy
 changeset 49789 e0a4cb91a8a9 parent 49784 5e5b2da42a69 child 50001 382bd3173584
```     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:26 2012 +0200
1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:27 2012 +0200
1.3 @@ -633,48 +633,45 @@
1.4  proof -
1.5    let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
1.6    interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
1.7 -  { fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
1.8 +  have "space M = \<Omega>"
1.9 +    using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
1.10 +
1.11 +  { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
1.12      then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
1.13 -    let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}"
1.14      have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
1.15 -    interpret D: dynkin_system \<Omega> ?D
1.16 -    proof (rule dynkin_systemI, simp_all)
1.17 -      fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
1.18 -      then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto
1.19 +    assume "D \<in> sets M"
1.20 +    with `Int_stable E` `E \<subseteq> Pow \<Omega>` have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
1.21 +      unfolding M
1.22 +    proof (induct rule: sigma_sets_induct_disjoint)
1.23 +      case (basic A)
1.24 +      then have "F \<inter> A \<in> E" using `Int_stable E` `F \<in> E` by (auto simp: Int_stable_def)
1.25 +      then show ?case using eq by auto
1.26      next
1.27 -      have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto
1.28 -      then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)"
1.29 -        using `F \<in> E` eq by (auto intro: sigma_sets_top)
1.30 +      case empty then show ?case by simp
1.31      next
1.32 -      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
1.33 +      case (compl A)
1.34        then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
1.35          and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
1.36 -        using `F \<in> E` S.sets_into_space by auto
1.37 +        using `F \<in> E` S.sets_into_space by (auto simp: M)
1.38        have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
1.39        then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
1.40        have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
1.41        then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
1.42        then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
1.43          using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
1.44 -      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` * by simp
1.45 +      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` compl by simp
1.46        also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
1.47          using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
1.48          by (auto intro!: emeasure_Diff[symmetric] simp: M N)
1.49 -      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega> - A)) = ?\<nu> (F \<inter> (\<Omega> - A))"
1.50 -        using * by auto
1.51 +      finally show ?case
1.52 +        using `space M = \<Omega>` by auto
1.53      next
1.54 -      fix A :: "nat \<Rightarrow> 'a set"
1.55 -      assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}"
1.56 +      case (union A)
1.57        then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
1.58          by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
1.59 -      with A show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Union>x. A x)) = ?\<nu> (F \<inter> (\<Union>x. A x))"
1.60 +      with A show ?case
1.61          by auto
1.62 -    qed
1.63 -    have *: "sigma_sets \<Omega> E = ?D"
1.64 -      using `F \<in> E` `Int_stable E`
1.65 -      by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq)
1.66 -    have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
1.67 -      unfolding M by (subst (asm) *) auto }
1.68 +    qed }
1.69    note * = this
1.70    show "M = N"
1.71    proof (rule measure_eqI)
1.72 @@ -684,9 +681,7 @@
1.73        using A(1) by (auto simp: subset_eq M)
1.74      fix F assume "F \<in> sets M"
1.75      let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
1.76 -    have "space M = \<Omega>"
1.77 -      using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
1.78 -    then have F_eq: "F = (\<Union>i. ?D i)"
1.79 +    from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
1.80        using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
1.81      have [simp, intro]: "\<And>i. ?D i \<in> sets M"
1.82        using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
```