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