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.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 +
```