src/HOL/Analysis/Measure_Space.thy
 changeset 64008 17a20ca86d62 parent 63968 4359400adfe7 child 64267 b9a1486e79be
```     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Mon Oct 03 14:09:26 2016 +0100
1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Sep 30 16:08:38 2016 +0200
1.3 @@ -838,6 +838,38 @@
1.4    qed
1.5  qed
1.6
1.7 +lemma space_empty: "space M = {} \<Longrightarrow> M = count_space {}"
1.8 +  by (rule measure_eqI) (simp_all add: space_empty_iff)
1.9 +
1.10 +lemma measure_eqI_generator_eq_countable:
1.11 +  fixes M N :: "'a measure" and E :: "'a set set" and A :: "'a set set"
1.12 +  assumes E: "Int_stable E" "E \<subseteq> Pow \<Omega>" "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X"
1.13 +    and sets: "sets M = sigma_sets \<Omega> E" "sets N = sigma_sets \<Omega> E"
1.14 +  and A: "A \<subseteq> E" "(\<Union>A) = \<Omega>" "countable A" "\<And>a. a \<in> A \<Longrightarrow> emeasure M a \<noteq> \<infinity>"
1.15 +  shows "M = N"
1.16 +proof cases
1.17 +  assume "\<Omega> = {}"
1.18 +  have *: "sigma_sets \<Omega> E = sets (sigma \<Omega> E)"
1.19 +    using E(2) by simp
1.20 +  have "space M = \<Omega>" "space N = \<Omega>"
1.21 +    using sets E(2) unfolding * by (auto dest: sets_eq_imp_space_eq simp del: sets_measure_of)
1.22 +  then show "M = N"
1.23 +    unfolding \<open>\<Omega> = {}\<close> by (auto dest: space_empty)
1.24 +next
1.25 +  assume "\<Omega> \<noteq> {}" with \<open>\<Union>A = \<Omega>\<close> have "A \<noteq> {}" by auto
1.26 +  from this \<open>countable A\<close> have rng: "range (from_nat_into A) = A"
1.27 +    by (rule range_from_nat_into)
1.28 +  show "M = N"
1.29 +  proof (rule measure_eqI_generator_eq[OF E sets])
1.30 +    show "range (from_nat_into A) \<subseteq> E"
1.31 +      unfolding rng using \<open>A \<subseteq> E\<close> .
1.32 +    show "(\<Union>i. from_nat_into A i) = \<Omega>"
1.33 +      unfolding rng using \<open>\<Union>A = \<Omega>\<close> .
1.34 +    show "emeasure M (from_nat_into A i) \<noteq> \<infinity>" for i
1.35 +      using rng by (intro A) auto
1.36 +  qed
1.37 +qed
1.38 +
1.39  lemma measure_of_of_measure: "measure_of (space M) (sets M) (emeasure M) = M"
1.40  proof (intro measure_eqI emeasure_measure_of_sigma)
1.41    show "sigma_algebra (space M) (sets M)" ..
1.42 @@ -1097,6 +1129,9 @@
1.43    "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in M. Q x)"
1.44    by auto
1.45
1.46 +lemma AE_cong_strong: "M = N \<Longrightarrow> (\<And>x. x \<in> space N =simp=> P x = Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in N. Q x)"
1.47 +  by (auto simp: simp_implies_def)
1.48 +
1.49  lemma AE_all_countable:
1.50    "(AE x in M. \<forall>i. P i x) \<longleftrightarrow> (\<forall>i::'i::countable. AE x in M. P i x)"
1.51  proof
1.52 @@ -2135,9 +2170,6 @@
1.53    qed simp
1.54  qed (simp add: emeasure_notin_sets)
1.55
1.56 -lemma space_empty: "space M = {} \<Longrightarrow> M = count_space {}"
1.57 -  by (rule measure_eqI) (simp_all add: space_empty_iff)
1.58 -
1.59  lemma null_sets_count_space: "null_sets (count_space A) = { {} }"
1.60    unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0)
1.61
```