src/HOL/Analysis/Measure_Space.thy
changeset 63959 f77dca1abf1b
parent 63958 02de4a58e210
child 63968 4359400adfe7
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 13:54:57 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 18:52:34 2016 +0200
     1.3 @@ -1127,6 +1127,12 @@
     1.4      unfolding eventually_ae_filter by auto
     1.5  qed auto
     1.6  
     1.7 +lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
     1.8 +  by (auto simp add: pairwise_def)
     1.9 +
    1.10 +lemma AE_pairwise: "countable F \<Longrightarrow> pairwise (\<lambda>A B. AE x in M. R x A B) F \<longleftrightarrow> (AE x in M. pairwise (R x) F)"
    1.11 +  unfolding pairwise_alt by (simp add: AE_ball_countable)
    1.12 +
    1.13  lemma AE_discrete_difference:
    1.14    assumes X: "countable X"
    1.15    assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
    1.16 @@ -1453,6 +1459,12 @@
    1.17    by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top
    1.18             del: real_of_ereal_enn2ereal)
    1.19  
    1.20 +lemma measure_eq_AE:
    1.21 +  assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
    1.22 +  assumes A: "A \<in> sets M" and B: "B \<in> sets M"
    1.23 +  shows "measure M A = measure M B"
    1.24 +  using assms emeasure_eq_AE[OF assms] by (simp add: measure_def)
    1.25 +
    1.26  lemma measure_Union:
    1.27    "emeasure M A \<noteq> \<infinity> \<Longrightarrow> emeasure M B \<noteq> \<infinity> \<Longrightarrow> A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow>
    1.28      measure M (A \<union> B) = measure M A + measure M B"
    1.29 @@ -1554,6 +1566,12 @@
    1.30      done
    1.31  qed
    1.32  
    1.33 +lemma measure_Un_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A \<union> B) = measure M A"
    1.34 +  by (simp add: measure_def emeasure_Un_null_set)
    1.35 +
    1.36 +lemma measure_Diff_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A - B) = measure M A"
    1.37 +  by (simp add: measure_def emeasure_Diff_null_set)
    1.38 +
    1.39  lemma measure_eq_setsum_singleton:
    1.40    "finite S \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M) \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> emeasure M {x} \<noteq> \<infinity>) \<Longrightarrow>
    1.41      measure M S = (\<Sum>x\<in>S. measure M {x})"
    1.42 @@ -1595,6 +1613,9 @@
    1.43  lemma fmeasurableD[dest, measurable_dest]: "A \<in> fmeasurable M \<Longrightarrow> A \<in> sets M"
    1.44    by (auto simp: fmeasurable_def)
    1.45  
    1.46 +lemma fmeasurableD2: "A \<in> fmeasurable M \<Longrightarrow> emeasure M A \<noteq> top"
    1.47 +  by (auto simp: fmeasurable_def)
    1.48 +
    1.49  lemma fmeasurableI: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> A \<in> fmeasurable M"
    1.50    by (auto simp: fmeasurable_def)
    1.51  
    1.52 @@ -1648,6 +1669,86 @@
    1.53      using assms by (intro sets.countable_INT') auto
    1.54  qed
    1.55  
    1.56 +lemma measure_Un2:
    1.57 +  "A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
    1.58 +  using measure_Union[of M A "B - A"] by (auto simp: fmeasurableD2 fmeasurable.Diff)
    1.59 +
    1.60 +lemma measure_Un3:
    1.61 +  assumes "A \<in> fmeasurable M" "B \<in> fmeasurable M"
    1.62 +  shows "measure M (A \<union> B) = measure M A + measure M B - measure M (A \<inter> B)"
    1.63 +proof -
    1.64 +  have "measure M (A \<union> B) = measure M A + measure M (B - A)"
    1.65 +    using assms by (rule measure_Un2)
    1.66 +  also have "B - A = B - (A \<inter> B)"
    1.67 +    by auto
    1.68 +  also have "measure M (B - (A \<inter> B)) = measure M B - measure M (A \<inter> B)"
    1.69 +    using assms by (intro measure_Diff) (auto simp: fmeasurable_def)
    1.70 +  finally show ?thesis
    1.71 +    by simp
    1.72 +qed
    1.73 +
    1.74 +lemma measure_Un_AE:
    1.75 +  "AE x in M. x \<notin> A \<or> x \<notin> B \<Longrightarrow> A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow>
    1.76 +  measure M (A \<union> B) = measure M A + measure M B"
    1.77 +  by (subst measure_Un2) (auto intro!: measure_eq_AE)
    1.78 +
    1.79 +lemma measure_UNION_AE:
    1.80 +  assumes I: "finite I"
    1.81 +  shows "(\<And>i. i \<in> I \<Longrightarrow> F i \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>i j. AE x in M. x \<notin> F i \<or> x \<notin> F j) I \<Longrightarrow>
    1.82 +    measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
    1.83 +  unfolding AE_pairwise[OF countable_finite, OF I]
    1.84 +  using I
    1.85 +  apply (induction I rule: finite_induct)
    1.86 +   apply simp
    1.87 +  apply (simp add: pairwise_insert)
    1.88 +  apply (subst measure_Un_AE)
    1.89 +  apply auto
    1.90 +  done
    1.91 +
    1.92 +lemma measure_UNION':
    1.93 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>i j. disjnt (F i) (F j)) I \<Longrightarrow>
    1.94 +    measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
    1.95 +  by (intro measure_UNION_AE) (auto simp: disjnt_def elim!: pairwise_mono intro!: always_eventually)
    1.96 +
    1.97 +lemma measure_Union_AE:
    1.98 +  "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>S T. AE x in M. x \<notin> S \<or> x \<notin> T) F \<Longrightarrow>
    1.99 +    measure M (\<Union>F) = (\<Sum>S\<in>F. measure M S)"
   1.100 +  using measure_UNION_AE[of F "\<lambda>x. x" M] by simp
   1.101 +
   1.102 +lemma measure_Union':
   1.103 +  "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> fmeasurable M) \<Longrightarrow> pairwise disjnt F \<Longrightarrow> measure M (\<Union>F) = (\<Sum>S\<in>F. measure M S)"
   1.104 +  using measure_UNION'[of F "\<lambda>x. x" M] by simp
   1.105 +
   1.106 +lemma measure_Un_le:
   1.107 +  assumes "A \<in> sets M" "B \<in> sets M" shows "measure M (A \<union> B) \<le> measure M A + measure M B"
   1.108 +proof cases
   1.109 +  assume "A \<in> fmeasurable M \<and> B \<in> fmeasurable M"
   1.110 +  with measure_subadditive[of A M B] assms show ?thesis
   1.111 +    by (auto simp: fmeasurableD2)
   1.112 +next
   1.113 +  assume "\<not> (A \<in> fmeasurable M \<and> B \<in> fmeasurable M)"
   1.114 +  then have "A \<union> B \<notin> fmeasurable M"
   1.115 +    using fmeasurableI2[of "A \<union> B" M A] fmeasurableI2[of "A \<union> B" M B] assms by auto
   1.116 +  with assms show ?thesis
   1.117 +    by (auto simp: fmeasurable_def measure_def less_top[symmetric])
   1.118 +qed
   1.119 +
   1.120 +lemma measure_UNION_le:
   1.121 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M) \<Longrightarrow> measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
   1.122 +proof (induction I rule: finite_induct)
   1.123 +  case (insert i I)
   1.124 +  then have "measure M (\<Union>i\<in>insert i I. F i) \<le> measure M (F i) + measure M (\<Union>i\<in>I. F i)"
   1.125 +    by (auto intro!: measure_Un_le)
   1.126 +  also have "measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
   1.127 +    using insert by auto
   1.128 +  finally show ?case
   1.129 +    using insert by simp
   1.130 +qed simp
   1.131 +
   1.132 +lemma measure_Union_le:
   1.133 +  "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> sets M) \<Longrightarrow> measure M (\<Union>F) \<le> (\<Sum>S\<in>F. measure M S)"
   1.134 +  using measure_UNION_le[of F "\<lambda>x. x" M] by simp
   1.135 +
   1.136  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
   1.137  
   1.138  locale finite_measure = sigma_finite_measure M for M +