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`