summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Radon_Nikodym.thy

changeset 53374 | a14d2a854c02 |

parent 53015 | a1119cf551e8 |

child 54776 | db890d9fc5c2 |

1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy Tue Sep 03 00:51:08 2013 +0200 1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Sep 03 01:12:40 2013 +0200 1.3 @@ -412,14 +412,14 @@ 1.4 1.5 have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def 1.6 proof 1.7 - fix A assume A: "A \<in> null_sets M" 1.8 - with `absolutely_continuous M N` have "A \<in> null_sets N" 1.9 + fix A assume A_M: "A \<in> null_sets M" 1.10 + with `absolutely_continuous M N` have A_N: "A \<in> null_sets N" 1.11 unfolding absolutely_continuous_def by auto 1.12 - moreover with A have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def) 1.13 + moreover from A_M A_N have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def) 1.14 ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0" 1.15 using positive_integral_positive[of M] by (auto intro!: antisym) 1.16 then show "A \<in> null_sets ?M" 1.17 - using A by (simp add: emeasure_M null_sets_def sets_eq) 1.18 + using A_M by (simp add: emeasure_M null_sets_def sets_eq) 1.19 qed 1.20 have upper_bound: "\<forall>A\<in>sets M. ?M A \<le> 0" 1.21 proof (rule ccontr) 1.22 @@ -431,7 +431,7 @@ 1.23 using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq]) 1.24 finally have pos_t: "0 < ?M (space M)" by simp 1.25 moreover 1.26 - then have "emeasure M (space M) \<noteq> 0" 1.27 + from pos_t have "emeasure M (space M) \<noteq> 0" 1.28 using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def) 1.29 then have pos_M: "0 < emeasure M (space M)" 1.30 using emeasure_nonneg[of M "space M"] by (simp add: le_less) 1.31 @@ -594,12 +594,14 @@ 1.32 proof (rule disjCI, simp) 1.33 assume *: "0 < emeasure M A \<longrightarrow> N A \<noteq> \<infinity>" 1.34 show "emeasure M A = 0 \<and> N A = 0" 1.35 - proof cases 1.36 - assume "emeasure M A = 0" moreover with ac A have "N A = 0" 1.37 + proof (cases "emeasure M A = 0") 1.38 + case True 1.39 + with ac A have "N A = 0" 1.40 unfolding absolutely_continuous_def by auto 1.41 - ultimately show ?thesis by simp 1.42 + with True show ?thesis by simp 1.43 next 1.44 - assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto 1.45 + case False 1.46 + with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto 1.47 with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)" 1.48 using Q' by (auto intro!: plus_emeasure sets.countable_UN) 1.49 also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"