# HG changeset patch
# User hellerar
# Date 1283434298 -7200
# Node ID 67da17aced5aa3a94c8c09cc0dc1b50ec27c0ba7
# Parent  84af4fdc1a98b90047dedb94b3b07ec5efde2b04
measure unique

diff -r 84af4fdc1a98 -r 67da17aced5a src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Wed Sep 01 17:19:47 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 15:31:38 2010 +0200
@@ -5,13 +5,13 @@
 definition dynkin
 where "dynkin M =
       ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
-       space M \<in> sets M \<and> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
+       space M \<in> sets M \<and> (\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M) \<and>
        (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
              (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
 
 lemma dynkinI:
   assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
-  assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M"
+  assumes "space M \<in> sets M" and "\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M"
   assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
           \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
   shows "dynkin M"
@@ -29,13 +29,18 @@
 
 lemma dynkin_diff:
   assumes "dynkin M"
-  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
+  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M ; a \<subseteq> b \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
 using assms unfolding dynkin_def by auto
 
+lemma dynkin_empty:
+  assumes "dynkin M"
+  shows "{} \<in> sets M"
+using dynkin_diff[OF assms dynkin_space[OF assms] dynkin_space[OF assms]] by auto
+
 lemma dynkin_UN:
   assumes "dynkin M"
   assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
-  assumes "\<forall> i :: nat. a i \<in> sets M"
+  assumes "\<And> i :: nat. a i \<in> sets M"
   shows "UNION UNIV a \<in> sets M"
 using assms unfolding dynkin_def by auto
 
@@ -46,7 +51,7 @@
   shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
 by (rule dynkinI) auto
 
-lemma
+lemma dynkin_lemma:
   assumes stab: "Int_stable E"
   and spac: "space E = space D"
   and subsED: "sets E \<subseteq> sets D"
@@ -61,10 +66,8 @@
   hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
     using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified]
     by auto
-
-  have "sets_\<delta>E \<subseteq> sets D"
+  have \<delta>E_D: "sets_\<delta>E \<subseteq> sets D"
     unfolding sets_\<delta>E_def using assms by auto
-
   have \<delta>ynkin: "dynkin \<delta>E"
   proof (rule dynkinI, safe)
     fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
@@ -91,7 +94,7 @@
       unfolding \<delta>E_def sets_\<delta>E_def
       using dynkin_space by fastsimp
   next
-    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
+    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" "a \<subseteq> b"
     thus "b - a \<in> sets \<delta>E"
       unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
   next
@@ -142,21 +145,21 @@
           unfolding \<delta>E_def by auto
       qed
     next
-      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d"
+      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d" "a \<subseteq> b"
       hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
         unfolding Dy_def \<delta>E_def by auto
       hence *: "b - a \<in> sets \<delta>E"
-        using dynkin_diff[OF \<delta>ynkin] by auto
+        using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
       have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
         using absm unfolding Dy_def \<delta>E_def by auto
       hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
-        using dynkin_diff[OF \<delta>ynkin] by auto
+        using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
       hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
       thus "b - a \<in> Dy d"
         using * ** unfolding Dy_def \<delta>E_def by auto
     next
       fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d"
-      hence "\<forall> i. a i \<in> sets \<delta>E"
+      hence "\<And> i. a i \<in> sets \<delta>E"
         unfolding Dy_def \<delta>E_def by auto
       from dynkin_UN[OF \<delta>ynkin aasm(1) this]
       have *: "UNION UNIV a \<in> sets \<delta>E" by auto
@@ -228,24 +231,170 @@
     fix a assume aasm: "a \<in> sets \<delta>E"
     hence "a \<inter> d \<in> sets \<delta>E"
       using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
-  have "sigma_algebra D"
+  { fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets \<delta>E" "\<And>A. A \<in> sets \<delta>E \<Longrightarrow> A \<subseteq> space \<delta>E"
+      "\<And>a. a \<in> sets \<delta>E \<Longrightarrow> space \<delta>E - a \<in> sets \<delta>E"
+    "{} \<in> sets \<delta>E" "space \<delta>E \<in> sets \<delta>E"
+    let "?A i" = "A i \<inter> (\<Inter> j \<in> {..< i}. space \<delta>E - A j)"
+    { fix i :: nat
+      have *: "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<inter> space \<delta>E \<in> sets \<delta>E"
+        apply (induct i)
+        using lessThan_Suc Asm \<delta>E_stab apply fastsimp
+        apply (subst lessThan_Suc)
+        apply (subst INT_insert)
+        apply (subst Int_assoc)
+        apply (subst \<delta>E_stab)
+        using lessThan_Suc Asm \<delta>E_stab Asm
+        apply (fastsimp simp add:Int_assoc dynkin_diff[OF \<delta>ynkin])
+        prefer 2 apply simp
+        apply (rule dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]])
+        using Asm by auto
+      have **: "\<And> i. A i \<subseteq> space \<delta>E" using Asm by auto
+      have "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<subseteq> space \<delta>E \<or> (\<Inter> j \<in> {..< i}. A j) = UNIV \<and> i = 0"
+        apply (cases i)
+        using Asm ** dynkin_subset[OF \<delta>ynkin, of "A (i - 1)"]
+        by auto
+      hence Aisets: "?A i \<in> sets \<delta>E"
+        apply (cases i)
+        using Asm * apply fastsimp
+        apply (rule \<delta>E_stab)
+        using Asm * **
+        by (auto simp add:Int_absorb2)
+      have "?A i = disjointed A i" unfolding disjointed_def
+      atLeast0LessThan using Asm by auto
+      hence "?A i = disjointed A i" "?A i \<in> sets \<delta>E"
+        using Aisets by auto
+    } note Ai = this
+    from dynkin_UN[OF \<delta>ynkin _ this(2)] this disjoint_family_disjointed[of A]
+    have "(\<Union> i. ?A i) \<in> sets \<delta>E"
+      by (auto simp add:disjoint_family_on_def disjointed_def)
+    hence "(\<Union> i. A i) \<in> sets \<delta>E"
+      using Ai(1) UN_disjointed_eq[of A] by auto } note \<delta>E_UN = this
+  { fix a b assume asm: "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
+    let ?ab = "\<lambda> i. if (i::nat) = 0 then a else if i = 1 then b else {}"
+    have *: "(\<Union> i. ?ab i) \<in> sets \<delta>E"
+      apply (rule \<delta>E_UN)
+      using asm \<delta>E_UN dynkin_empty[OF \<delta>ynkin] 
+      dynkin_subset[OF \<delta>ynkin] 
+      dynkin_space[OF \<delta>ynkin]
+      dynkin_diff[OF \<delta>ynkin] by auto
+    have "(\<Union> i. ?ab i) = a \<union> b" apply auto
+      apply (case_tac "i = 0")
+      apply auto
+      apply (case_tac "i = 1")
+      by auto
+    hence "a \<union> b \<in> sets \<delta>E" using * by auto} note \<delta>E_Un = this
+  have "sigma_algebra \<delta>E"
     apply unfold_locales
-    using dynkin_subset[OF dyn]
-    using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]]
-    using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]]
-    using dynkin_space[OF dyn]
-  proof auto
-    fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D"
-      "\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D"
-    "{} \<in> sets D" "space D \<in> sets D"
-    let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)"
-    { fix i :: nat assume "i > 0"
-      have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E"
-        apply (induct i)
-        apply auto
-    }
-    from dynkin_UN
+    using dynkin_subset[OF \<delta>ynkin]
+    using dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]]
+    using dynkin_diff[OF \<delta>ynkin, of "space \<delta>E" "space \<delta>E", OF dynkin_space[OF \<delta>ynkin] dynkin_space[OF \<delta>ynkin]]
+    using dynkin_space[OF \<delta>ynkin]
+    using \<delta>E_UN \<delta>E_Un
+    by auto
+  from sigma_algebra.sigma_subset[OF this E_\<delta>E] \<delta>E_D subsDE spac
+  show ?thesis by (auto simp add:\<delta>E_def sigma_def)
+qed
+
+lemma measure_eq:
+  assumes fin: "\<mu> (space M) = \<nu> (space M)" "\<nu> (space M) < \<omega>" 
+  assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
+  assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
+  assumes ms: "measure_space M \<mu>" "measure_space M \<nu>"
+  assumes A: "A \<in> sets M"
+  shows "\<mu> A = \<nu> A"
+proof -
+  interpret M: measure_space M \<mu>
+    using ms by simp
+  interpret M': measure_space M \<nu>
+    using ms by simp
+
+  let ?D_sets = "{A. A \<in> sets M \<and> \<mu> A = \<nu> A}"
+  have \<delta>: "dynkin \<lparr> space = space M , sets = ?D_sets \<rparr>"
+  proof (rule dynkinI, safe, simp_all)
+    fix A x assume "A \<in> sets M \<and> \<mu> A = \<nu> A" "x \<in> A"
+    thus "x \<in> space M" using assms M.sets_into_space by auto
+  next
+    show "\<mu> (space M) = \<nu> (space M)"
+      using fin by auto
+  next
+    fix a b
+    assume asm: "a \<in> sets M \<and> \<mu> a = \<nu> a"
+      "b \<in> sets M \<and> \<mu> b = \<nu> b" "a \<subseteq> b"
+    hence "a \<subseteq> space M"
+      using M.sets_into_space by auto
+    from M.measure_mono[OF this]
+    have "\<mu> a \<le> \<mu> (space M)"
+      using asm by auto
+    hence afin: "\<mu> a < \<omega>"
+      using fin by auto
+    have *: "b = b - a \<union> a" using asm by auto
+    have **: "(b - a) \<inter> a = {}" using asm by auto
+    have iv: "\<mu> (b - a) + \<mu> a = \<mu> b"
+      using M.measure_additive[of "b - a" a]
+        conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
+      by auto
+    have v: "\<nu> (b - a) + \<nu> a = \<nu> b"
+      using M'.measure_additive[of "b - a" a]
+        conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
+      by auto
+    from iv v have "\<mu> (b - a) = \<nu> (b - a)" using asm afin
+      pinfreal_add_cancel_right[of "\<mu> (b - a)" "\<nu> a" "\<nu> (b - a)"]
+      by auto
+    thus "b - a \<in> sets M \<and> \<mu> (b - a) = \<nu> (b - a)"
+      using asm by auto
+  next
+    fix a assume "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
+      "\<And>i. a i \<in> sets M \<and> \<mu> (a i) = \<nu> (a i)"
+    thus "(\<Union>x. a x) \<in> sets M \<and> \<mu> (\<Union>x. a x) = \<nu> (\<Union>x. a x)"
+      using M.measure_countably_additive
+        M'.measure_countably_additive
+        M.countable_UN
+      apply (auto simp add:disjoint_family_on_def image_def)
+      apply (subst M.measure_countably_additive[symmetric])
+      apply (auto simp add:disjoint_family_on_def)
+      apply (subst M'.measure_countably_additive[symmetric])
+      by (auto simp add:disjoint_family_on_def)
   qed
+  have *: "sets E \<subseteq> ?D_sets"
+    using eq E sigma_sets.Basic[of _ "sets E"]
+    by (auto simp add:sigma_def)
+  have **: "?D_sets \<subseteq> sets M" by auto
+  have "M = \<lparr> space = space M , sets = ?D_sets \<rparr>"
+    unfolding E(1)
+    apply (rule dynkin_lemma[OF E(2)])
+    using eq E space_sigma \<delta> sigma_sets.Basic
+    by (auto simp add:sigma_def)
+  from subst[OF this, of "\<lambda> M. A \<in> sets M", OF A]
+  show ?thesis by auto
+qed
+
+lemma
+  assumes sfin: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And> i :: nat. \<nu> (A i) < \<omega>"
+  assumes A: "\<And>  i. \<mu> (A i) = \<nu> (A i)" "\<And> i. A i \<subseteq> A (Suc i)"
+  assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
+  assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
+  assumes ms: "measure_space (M :: 'a algebra) \<mu>" "measure_space M \<nu>"
+  assumes B: "B \<in> sets M"
+  shows "\<mu> B = \<nu> B"
+proof -
+  interpret M: measure_space M \<mu> by (rule ms)
+  interpret M': measure_space M \<nu> by (rule ms)
+  have *: "M = \<lparr> space = space M, sets = sets M \<rparr>" by auto
+  { fix i :: nat
+    have **: "M\<lparr> space := A i, sets := op \<inter> (A i) ` sets M \<rparr> =
+      \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
+      by auto
+    have mu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<mu>"
+      using M.restricted_measure_space[of "A i", simplified **]
+        sfin by auto
+    have nu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<nu>"
+      using M'.restricted_measure_space[of "A i", simplified **]
+        sfin by auto
+    let ?M = "\<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
+    have "\<mu> (A i \<inter> B) = \<nu> (A i \<inter> B)"
+      apply (rule measure_eq[of \<mu> ?M \<nu> "\<lparr> space = space E \<inter> A i, sets = op \<inter> (A i) ` sets E\<rparr>" "A i \<inter> B", simplified])
+      using assms nu_i mu_i
+      apply (auto simp add:image_def) (* TODO *)
 qed
 
 lemma